diff --git a/bin/deepstate/main_angr.py b/bin/deepstate/main_angr.py index b122d49..a35bd58 100644 --- a/bin/deepstate/main_angr.py +++ b/bin/deepstate/main_angr.py @@ -281,6 +281,10 @@ def do_run_test(project, test, apis, run_state, should_call_state): test_state = run_state mc = DeepAngr(state=test_state) + + # Tell the system that we're using symbolic execution. + mc.write_uint32_t(apis["UsingSymExec"], 8589934591) + mc.begin_test(test) del mc @@ -340,9 +344,6 @@ def hook_apis(args, project, run_state): mc = DeepAngr(state=run_state) apis = mc.read_api_table(ea_of_api_table) - # Tell the system that we're using symbolic execution. - mc.write_uint32_t(apis["UsingSymExec"], 1) - # Hook various functions. hook_function(project, apis['IsSymbolicUInt'], IsSymbolicUInt) hook_function(project, apis['ConcretizeData'], ConcretizeData) diff --git a/bin/deepstate/main_manticore.py b/bin/deepstate/main_manticore.py index b7de01d..26d6672 100644 --- a/bin/deepstate/main_manticore.py +++ b/bin/deepstate/main_manticore.py @@ -335,6 +335,10 @@ def do_run_test(state, apis, test, hook_test=False): state = m.initial_state mc = DeepManticore(state) + + # Tell the system that we're using symbolic execution. + mc.write_uint32_t(apis["UsingSymExec"], 8589934591) + mc.begin_test(test) del mc @@ -423,9 +427,6 @@ def main_takeover(m, args, takeover_symbol): base = get_base(m) apis = mc.read_api_table(ea_of_api_table, base) - # Tell the system that we're using symbolic execution. - mc.write_uint32_t(apis["UsingSymExec"], 1) - del mc fake_test = TestInfo(takeover_ea, '_takeover_test', '_takeover_file', 0) diff --git a/src/include/deepstate/DeepState.h b/src/include/deepstate/DeepState.h index fd61563..c103a72 100644 --- a/src/include/deepstate/DeepState.h +++ b/src/include/deepstate/DeepState.h @@ -232,23 +232,8 @@ DEEPSTATE_INLINE static void DeepState_Check(int expr) { } } -/* Return a symbolic value in a the range `[low_inc, high_inc]`. - * - * Current implementation saturates values. An alternative implementation - * worth exploring, and perhaps supporting in addition to saturation, is - * something like: - * - * x = symbolic_value; - * size = (high - low) + 1 - * if (symbolic mode) { - * assume 0 <= x and x < size - * return low + x - * } else { - * return low + (x % size) - * } - * - * This type of version lets a reducer drive toward zero. - */ +/* Return a symbolic value in a the range `[low_inc, high_inc]`. */ +/* Saturating version here is an alternative, but worse for fuzzing: #define DEEPSTATE_MAKE_SYMBOLIC_RANGE(Tname, tname) \ DEEPSTATE_INLINE static tname DeepState_ ## Tname ## InRange( \ tname low, tname high) { \ @@ -268,6 +253,24 @@ DEEPSTATE_INLINE static void DeepState_Check(int expr) { return x; \ } \ } +*/ +#define DEEPSTATE_MAKE_SYMBOLIC_RANGE(Tname, tname) \ + DEEPSTATE_INLINE static tname DeepState_ ## Tname ## InRange( \ + tname low, tname high) { \ + if (low > high) { \ + return DeepState_ ## Tname ## InRange(high, low); \ + } \ + const tname x = DeepState_ ## Tname(); \ + if (DeepState_UsingSymExec) { \ + (void) DeepState_Assume(low <= x && x <= high); \ + return x; \ + } \ + if ((x < low) || (x > high)) { \ + const tname size = (high - low) + 1; \ + return low + (x % size); \ + } \ + return x; \ + } DEEPSTATE_MAKE_SYMBOLIC_RANGE(Size, size_t) DEEPSTATE_MAKE_SYMBOLIC_RANGE(Int64, int64_t)