Group symex options into symex_config structure

This makes it easy to separate the constant parameters of that class
from the other fields.

Author: romainbrenguier

src/goto-symex/goto_symex.cpp

@@ -18,7 +18,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

@@ -38,6 +38,37 @@ class namespacet;
 class side_effect_exprt;
 class typecast_exprt;
 
+/// 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;
+  std::string debug_level;
+};
+
+symex_configt symex_config(const optionst &options)
+{
+  symex_configt config;
+  config.max_depth = options.get_unsigned_int_option("depth");
+  config.doing_path_exploration = options.is_set("paths");
+  config.allow_pointer_unsoundness =
+    options.get_bool_option("allow-pointer-unsoundness");
+  config.constant_propagation = options.get_bool_option("propagation");
+  config.self_loops_to_assumptions =
+    options.get_bool_option("self-loops-to-assumptions");
+  config.simplify_opt = options.get_bool_option("simplify");
+  config.unwinding_assertions = options.get_bool_option("unwinding-assertions");
+  config.partial_loops = options.get_bool_option("partial-loops");
+  config.debug_level = options.get_option("debug-level");
+  return config;
+}
+
 /// \brief The main class for the forward symbolic simulator
 ///
 /// Higher-level architectural information on symbolic execution is
@@ -55,18 +86,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(::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),
@@ -140,6 +161,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.
@@ -166,23 +189,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,7 +458,7 @@ void goto_symext::symex_trace(
 {
   PRECONDITION(code.arguments().size() >= 2);
 
-  int debug_thresh = unsafe_string2int(debug_level);
+  int debug_thresh = unsafe_string2int(symex_config.debug_level);
 
   mp_integer debug_lvl;
   optionalt<mp_integer> maybe_debug =

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

@@ -61,7 +61,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)))
@@ -109,7 +109,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,
@@ -176,7 +176,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.
@@ -494,9 +494,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

@@ -292,11 +292,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++;