Merge pull request #3431 from romainbrenguier/refactor/symex-config

Group symex options into symex_config structure

Author: tautschnig

src/goto-symex/goto_symex.cpp

@@ -17,7 +17,7 @@ unsigned goto_symext::dynamic_counter=0;
 
 void goto_symext::do_simplify(exprt &expr)
 {
-  if(simplify_opt)
+  if(symex_config.simplify_opt)
     simplify(expr, ns);
 }
 

src/goto-symex/goto_symex.h

@@ -48,6 +48,22 @@ class symex_nondet_generatort
   unsigned nondet_count = 0;
 };
 
+/// Configuration of the symbolic execution
+struct symex_configt final
+{
+  unsigned max_depth;
+  bool doing_path_exploration;
+  bool allow_pointer_unsoundness;
+  bool constant_propagation;
+  bool self_loops_to_assumptions;
+  bool simplify_opt;
+  bool unwinding_assertions;
+  bool partial_loops;
+  mp_integer debug_level;
+
+  explicit symex_configt(const optionst &options);
+};
+
 /// \brief The main class for the forward symbolic simulator
 ///
 /// Higher-level architectural information on symbolic execution is
@@ -65,18 +81,8 @@ class goto_symext
     const optionst &options,
     path_storaget &path_storage)
     : should_pause_symex(false),
-      max_depth(options.get_unsigned_int_option("depth")),
-      doing_path_exploration(options.is_set("paths")),
-      allow_pointer_unsoundness(
-        options.get_bool_option("allow-pointer-unsoundness")),
+      symex_config(options),
       language_mode(),
-      constant_propagation(options.get_bool_option("propagation")),
-      self_loops_to_assumptions(
-        options.get_bool_option("self-loops-to-assumptions")),
-      simplify_opt(options.get_bool_option("simplify")),
-      unwinding_assertions(options.get_bool_option("unwinding-assertions")),
-      partial_loops(options.get_bool_option("partial-loops")),
-      debug_level(options.get_option("debug-level")),
       outer_symbol_table(outer_symbol_table),
       ns(outer_symbol_table),
       target(_target),
@@ -150,6 +156,8 @@ class goto_symext
   bool should_pause_symex;
 
 protected:
+  const symex_configt symex_config;
+
   /// Initialise the symbolic execution and the given state with <code>pc</code>
   /// as entry point.
   /// \param state Symex state to initialise.
@@ -176,23 +184,13 @@ class goto_symext
     const get_goto_functiont &,
     statet &);
 
-  const unsigned max_depth;
-  const bool doing_path_exploration;
-  const bool allow_pointer_unsoundness;
-
 public:
 
   /// language_mode: ID_java, ID_C or another language identifier
   /// if we know the source language in use, irep_idt() otherwise.
   irep_idt language_mode;
 
 protected:
-  const bool constant_propagation;
-  const bool self_loops_to_assumptions;
-  const bool simplify_opt;
-  const bool unwinding_assertions;
-  const bool partial_loops;
-  const std::string debug_level;
 
   /// The symbol table associated with the goto-program that we're
   /// executing. This symbol table will not additionally contain objects

src/goto-symex/symex_assign.cpp

@@ -247,9 +247,9 @@ void goto_symext::symex_assign_symbol(
     ssa_lhs,
     ssa_rhs,
     ns,
-    simplify_opt,
-    constant_propagation,
-    allow_pointer_unsoundness);
+    symex_config.simplify_opt,
+    symex_config.constant_propagation,
+    symex_config.allow_pointer_unsoundness);
 
   exprt ssa_full_lhs=full_lhs;
   ssa_full_lhs=add_to_lhs(ssa_full_lhs, ssa_lhs);

src/goto-symex/symex_builtin_functions.cpp

@@ -458,8 +458,6 @@ void goto_symext::symex_trace(
 {
   PRECONDITION(code.arguments().size() >= 2);
 
-  int debug_thresh = unsafe_string2int(debug_level);
-
   mp_integer debug_lvl;
   optionalt<mp_integer> maybe_debug =
     numeric_cast<mp_integer>(code.arguments()[0]);
@@ -473,7 +471,7 @@ void goto_symext::symex_trace(
       code.arguments()[1].op0().id() == ID_string_constant,
     "CBMC_trace expects string constant as second argument");
 
-  if(mp_integer(debug_thresh)>=debug_lvl)
+  if(symex_config.debug_level >= debug_lvl)
   {
     std::list<exprt> vars;
 

src/goto-symex/symex_function_call.cpp

@@ -236,13 +236,13 @@ void goto_symext::symex_function_call_code(
   // see if it's too much
   if(stop_recursing)
   {
-    if(partial_loops)
+    if(symex_config.partial_loops)
     {
       // it's ok, ignore
     }
     else
     {
-      if(unwinding_assertions)
+      if(symex_config.unwinding_assertions)
         vcc(false_exprt(), "recursion unwinding assertion", state);
 
       // add to state guard to prevent further assignments

src/goto-symex/symex_goto.cpp

@@ -66,7 +66,7 @@ void goto_symext::symex_goto(statet &state)
   {
     // is it label: goto label; or while(cond); - popular in SV-COMP
     if(
-      self_loops_to_assumptions &&
+      symex_config.self_loops_to_assumptions &&
       (goto_target == state.source.pc ||
        (instruction.incoming_edges.size() == 1 &&
         *instruction.incoming_edges.begin() == goto_target)))
@@ -114,7 +114,7 @@ void goto_symext::symex_goto(statet &state)
     (simpl_state_guard.is_true() ||
      // or there is another block, but we're doing path exploration so
      // we're going to skip over it for now and return to it later.
-     doing_path_exploration))
+     symex_config.doing_path_exploration))
   {
     DATA_INVARIANT(
       instruction.targets.size() > 0,
@@ -181,7 +181,7 @@ void goto_symext::symex_goto(statet &state)
     log.debug() << "Resuming from next instruction '"
                 << state_pc->source_location << "'" << log.eom;
   }
-  else if(doing_path_exploration)
+  else if(symex_config.doing_path_exploration)
   {
     // We should save both the instruction after this goto, and the target of
     // the goto.
@@ -495,9 +495,9 @@ void goto_symext::loop_bound_exceeded(
   else
     negated_cond=not_exprt(guard);
 
-  if(!partial_loops)
+  if(!symex_config.partial_loops)
   {
-    if(unwinding_assertions)
+    if(symex_config.unwinding_assertions)
     {
       // Generate VCC for unwinding assertion.
       vcc(negated_cond,

src/goto-symex/symex_main.cpp

@@ -18,10 +18,26 @@ Author: Daniel Kroening, [email protected]
 #include <util/make_unique.h>
 #include <util/replace_symbol.h>
 #include <util/std_expr.h>
+#include <util/string2int.h>
 #include <util/symbol_table.h>
 
 #include <analyses/dirty.h>
 
+symex_configt::symex_configt(const optionst &options)
+  : max_depth(options.get_unsigned_int_option("depth")),
+    doing_path_exploration(options.is_set("paths")),
+    allow_pointer_unsoundness(
+      options.get_bool_option("allow-pointer-unsoundness")),
+    constant_propagation(options.get_bool_option("propagation")),
+    self_loops_to_assumptions(
+      options.get_bool_option("self-loops-to-assumptions")),
+    simplify_opt(options.get_bool_option("simplify")),
+    unwinding_assertions(options.get_bool_option("unwinding-assertions")),
+    partial_loops(options.get_bool_option("partial-loops")),
+    debug_level(unsafe_string2int(options.get_option("debug-level")))
+{
+}
+
 void symex_transition(
   goto_symext::statet &state,
   goto_programt::const_targett to,
@@ -317,11 +333,11 @@ void goto_symext::symex_step(
 
   const goto_programt::instructiont &instruction=*state.source.pc;
 
-  if(!doing_path_exploration)
+  if(!symex_config.doing_path_exploration)
     merge_gotos(state);
 
   // depth exceeded?
-  if(max_depth != 0 && state.depth > max_depth)
+  if(symex_config.max_depth != 0 && state.depth > symex_config.max_depth)
     state.guard.add(false_exprt());
   state.depth++;