diff --git a/bin/deepstate/common.py b/bin/deepstate/common.py index c7e2c12..59c2a94 100644 --- a/bin/deepstate/common.py +++ b/bin/deepstate/common.py @@ -93,6 +93,9 @@ class DeepState(object): def concretize_min(self, val, constrain=False): raise NotImplementedError("Must be implemented by engine.") + def concretize_max(self, val, constrain=False): + raise NotImplementedError("Must be implemented by engine.") + def concretize_many(self, val, max_num): raise NotImplementedError("Must be implemented by engine.") @@ -383,10 +386,10 @@ class DeepState(object): minimum satisfiable value for `arg`.""" return self.concretize_min(arg, constrain=False) - def api_min_int(self, arg): - """Implements the `DeepState_MinInt` API function, which returns the + def api_max_uint(self, arg): + """Implements the `DeepState_MaxUInt` API function, which returns the minimum satisfiable value for `arg`.""" - return self.concretize_min(arg + 2**31, constrain=False) + return self.concretize_max(arg, constrain=False) def api_is_symbolic_uint(self, arg): """Implements the `DeepState_IsSymbolicUInt` API, which returns whether or diff --git a/bin/deepstate/main_angr.py b/bin/deepstate/main_angr.py index 174d4d0..f4e5017 100644 --- a/bin/deepstate/main_angr.py +++ b/bin/deepstate/main_angr.py @@ -107,6 +107,14 @@ class DeepAngr(DeepState): self.add_constraint(val == concrete_val) return concrete_val + def concretize_max(self, val, constrain=False): + if isinstance(val, (int, long)): + return val + concrete_val = self.state.solver.max(val) + if constrain: + self.add_constraint(val == concrete_val) + return concrete_val + def concretize_many(self, val, max_num): assert 0 < max_num if isinstance(val, (int, long)): @@ -197,11 +205,11 @@ class MinUInt(angr.SimProcedure): return DeepAngr(procedure=self).api_min_uint(val) -class MinInt(angr.SimProcedure): - """Implements the `Deeptate_MinUInt` API function, which lets the +class MaxUInt(angr.SimProcedure): + """Implements the `Deeptate_MaxUInt` API function, which lets the programmer ask for the minimum satisfiable value of a signed integer.""" def run(self, val): - return DeepAngr(procedure=self).api_min_int(val) + return DeepAngr(procedure=self).api_max_uint(val) class StreamInt(angr.SimProcedure): @@ -340,7 +348,7 @@ def main(): hook_function(project, apis['ConcretizeData'], ConcretizeData) hook_function(project, apis['ConcretizeCStr'], ConcretizeCStr) hook_function(project, apis['MinUInt'], MinUInt) - hook_function(project, apis['MinInt'], MinInt) + hook_function(project, apis['MaxUInt'], MaxUInt) hook_function(project, apis['Assume'], Assume) hook_function(project, apis['Pass'], Pass) hook_function(project, apis['Fail'], Fail) diff --git a/bin/deepstate/main_manticore.py b/bin/deepstate/main_manticore.py index 1a85daa..0caf585 100644 --- a/bin/deepstate/main_manticore.py +++ b/bin/deepstate/main_manticore.py @@ -106,6 +106,14 @@ class DeepManticore(DeepState): self.add_constraint(val == concrete_val) return concrete_val + def concretize_max(self, val, constrain=False): + if isinstance(val, (int, long)): + return val + concrete_val = max(self.state.concretize(val, policy='MINMAX')) + if constrain: + self.add_constraint(val == concrete_val) + return concrete_val + def concretize_many(self, val, max_num): assert 0 < max_num if isinstance(val, (int, long)): @@ -212,10 +220,10 @@ def hook_MinUInt(self, val): return DeepAngr(procedure=self).api_min_uint(val) -def hook_MinInt(self, val): - """Implements the `Deeptate_MinUInt` API function, which lets the +def hook_MaxUInt(self, val): + """Implements the `Deeptate_MaxUInt` API function, which lets the programmer ask for the minimum satisfiable value of a signed integer.""" - return DeepAngr(procedure=self).api_min_int(val) + return DeepAngr(procedure=self).api_max_uint(val) def hook_Log(state, level, ea): @@ -253,7 +261,7 @@ def do_run_test(state, apis, test): m.add_hook(apis['ConcretizeData'], hook(hook_ConcretizeData)) m.add_hook(apis['ConcretizeCStr'], hook(hook_ConcretizeCStr)) m.add_hook(apis['MinUInt'], hook(hook_MinUInt)) - m.add_hook(apis['MinInt'], hook(hook_MinInt)) + m.add_hook(apis['MaxUInt'], hook(hook_MaxUInt)) m.add_hook(apis['Assume'], hook(hook_Assume)) m.add_hook(apis['Pass'], hook(hook_Pass)) m.add_hook(apis['Fail'], hook(hook_Fail)) diff --git a/src/include/deepstate/DeepState.h b/src/include/deepstate/DeepState.h index 9cc9120..57f191e 100644 --- a/src/include/deepstate/DeepState.h +++ b/src/include/deepstate/DeepState.h @@ -64,20 +64,39 @@ extern int8_t DeepState_Char(void); extern uint32_t DeepState_MinUInt(uint32_t); extern int32_t DeepState_MinInt(int32_t); +extern uint32_t DeepState_MaxUInt(uint32_t); +extern int32_t DeepState_MaxInt(int32_t); + DEEPSTATE_INLINE static uint16_t DeepState_MinUShort(uint16_t v) { return DeepState_MinUInt(v); } DEEPSTATE_INLINE static uint8_t DeepState_MinUChar(uint8_t v) { - return DeepState_MinUInt(v); + return (uint8_t) DeepState_MinUInt(v); } DEEPSTATE_INLINE static int16_t DeepState_MinShort(int16_t v) { - return DeepState_MinInt(v); + return (int16_t) DeepState_MinInt(v); } DEEPSTATE_INLINE static int8_t DeepState_MinChar(int8_t v) { - return DeepState_MinInt(v); + return (int8_t) DeepState_MinInt(v); +} + +DEEPSTATE_INLINE static uint16_t DeepState_MaxUShort(uint16_t v) { + return (uint16_t) DeepState_MaxUInt(v); +} + +DEEPSTATE_INLINE static uint8_t DeepState_MaxUChar(uint8_t v) { + return (uint8_t) DeepState_MaxUInt(v); +} + +DEEPSTATE_INLINE static int16_t DeepState_MaxShort(int16_t v) { + return (int16_t) DeepState_MaxInt(v); +} + +DEEPSTATE_INLINE static int8_t DeepState_MaxChar(int8_t v) { + return (int8_t) DeepState_MaxInt(v); } /* Returns `1` if `expr` is true, and `0` otherwise. This is kind of an indirect diff --git a/src/include/deepstate/DeepState.hpp b/src/include/deepstate/DeepState.hpp index ce8fa06..1a6852f 100644 --- a/src/include/deepstate/DeepState.hpp +++ b/src/include/deepstate/DeepState.hpp @@ -258,6 +258,9 @@ using symbolic_uint64_t = Symbolic; #define MAKE_MINIMIZER(Type, type) \ DEEPSTATE_INLINE static type Minimize(type val) { \ return DeepState_Min ## Type(val); \ + } \ + DEEPSTATE_INLINE static type Maximize(type val) { \ + return DeepState_Max ## Type(val); \ } MAKE_MINIMIZER(UInt, uint32_t) diff --git a/src/lib/DeepState.c b/src/lib/DeepState.c index ffa17cc..fa47446 100644 --- a/src/lib/DeepState.c +++ b/src/lib/DeepState.c @@ -204,9 +204,21 @@ uint32_t DeepState_MinUInt(uint32_t v) { } int32_t DeepState_MinInt(int32_t v) { + return (int32_t) (DeepState_MinUInt(((uint32_t) v) + 0x80000000U) - + 0x80000000U); +} + +/* Returns the maximum satisfiable value for a given symbolic value, given + * the constraints present on that value. */ +uint32_t DeepState_MaxUInt(uint32_t v) { return v; } +int32_t DeepState_MaxInt(int32_t v) { + return (int32_t) (DeepState_MaxUInt(((uint32_t) v) + 0x80000000U) - + 0x80000000U); +} + void _DeepState_Assume(int expr, const char *expr_str, const char *file, unsigned line) { if (!expr) { @@ -263,7 +275,7 @@ const struct DeepState_IndexEntry DeepState_API[] = { {"ConcretizeData", (void *) DeepState_ConcretizeData}, {"ConcretizeCStr", (void *) DeepState_ConcretizeCStr}, {"MinUInt", (void *) DeepState_MinUInt}, - {"MinInt", (void *) DeepState_MinInt}, + {"MaxUInt", (void *) DeepState_MaxUInt}, /* Logging API. */ {"Log", (void *) DeepState_Log},