Merge pull request #3221 from karkhaz/kk-goto-symex-member-cleanup

goto symex member cleanup

Author: tautschnig

src/cbmc/bmc.h

@@ -86,11 +86,6 @@ class bmct:public safety_checkert
       ui_message_handler(_message_handler),
       driver_callback_after_symex(callback_after_symex)
   {
-    symex.constant_propagation=options.get_bool_option("propagation");
-    symex.record_coverage=
-      !options.get_option("symex-coverage-report").empty();
-    symex.self_loops_to_assumptions =
-      options.get_bool_option("self-loops-to-assumptions");
   }
 
   virtual resultt run(const goto_functionst &goto_functions)
@@ -162,9 +157,6 @@ class bmct:public safety_checkert
       ui_message_handler(_message_handler),
       driver_callback_after_symex(callback_after_symex)
   {
-    symex.constant_propagation = options.get_bool_option("propagation");
-    symex.record_coverage =
-      !options.get_option("symex-coverage-report").empty();
     INVARIANT(
       options.get_bool_option("paths"),
       "Should only use saved equation & goto_state constructor "

src/cbmc/symex_bmc.cpp

@@ -25,7 +25,7 @@ symex_bmct::symex_bmct(
   const optionst &options,
   path_storaget &path_storage)
   : goto_symext(mh, outer_symbol_table, _target, options, path_storage),
-    record_coverage(false),
+    record_coverage(!options.get_option("symex-coverage-report").empty()),
     symex_coverage(ns)
 {
 }

src/cbmc/symex_bmc.h

@@ -80,7 +80,7 @@ class symex_bmct: public goto_symext
     return symex_coverage.generate_report(goto_functions, path);
   }
 
-  bool record_coverage;
+  const bool record_coverage;
 
   unwindsett unwindset;
 

src/goto-instrument/accelerate/scratch_program.cpp

@@ -35,7 +35,6 @@ bool scratch_programt::check_sat(bool do_slice)
   output(ns, "scratch", std::cout);
 #endif
 
-  symex.constant_propagation=constant_propagation;
   goto_symex_statet::propagationt::valuest constants;
 
   symex.symex_with_state(symex_state, functions, symex_symbol_table);
@@ -203,3 +202,10 @@ void scratch_programt::append_loop(
     }
   }
 }
+
+optionst scratch_programt::get_default_options()
+{
+  optionst ret;
+  ret.set_option("simplify", true);
+  return ret;
+}

src/goto-instrument/accelerate/scratch_program.h

@@ -43,16 +43,13 @@ class scratch_programt:public goto_programt
       ns(symbol_table, symex_symbol_table),
       equation(),
       path_storage(),
-      options(),
+      options(get_default_options()),
       symex(mh, symbol_table, equation, options, path_storage),
       satcheck(util_make_unique<satcheckt>()),
       satchecker(ns, *satcheck),
       z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
       checker(&z3) // checker(&satchecker)
   {
-    // Unconditionally set for performance reasons. This option setting applies
-    // only to this program.
-    options.set_option("simplify", true);
   }
 
   void append(goto_programt::instructionst &instructions);
@@ -91,6 +88,7 @@ class scratch_programt:public goto_programt
   bv_pointerst satchecker;
   smt2_dect z3;
   prop_convt *checker;
+  static optionst get_default_options();
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H

src/goto-symex/goto_symex.cpp

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

src/goto-symex/goto_symex.h

@@ -55,14 +55,18 @@ class goto_symext
     const optionst &options,
     path_storaget &path_storage)
     : should_pause_symex(false),
-      options(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(true),
-      self_loops_to_assumptions(true),
       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),
@@ -200,8 +204,6 @@ class goto_symext
     const get_goto_functiont &,
     statet &);
 
-  const optionst &options;
-
   const unsigned max_depth;
   const bool doing_path_exploration;
   const bool allow_pointer_unsoundness;
@@ -210,14 +212,18 @@ class goto_symext
   // these bypass the target maps
   virtual void symex_step_goto(statet &, bool taken);
 
-  bool constant_propagation;
-  bool self_loops_to_assumptions;
-
   /// 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
   /// that are dynamically created as part of symbolic execution; the
@@ -274,7 +280,7 @@ class goto_symext
 
   // guards
 
-  irep_idt guard_identifier;
+  const irep_idt guard_identifier;
 
   // symex
   virtual void symex_transition(

src/goto-symex/symex_assign.cpp

@@ -247,7 +247,7 @@ void goto_symext::symex_assign_symbol(
     ssa_lhs,
     ssa_rhs,
     ns,
-    options.get_bool_option("simplify"),
+    simplify_opt,
     constant_propagation,
     allow_pointer_unsoundness);
 

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(options.get_option("debug-level"));
+  int debug_thresh = unsafe_string2int(debug_level);
 
   mp_integer debug_lvl;
   optionalt<mp_integer> maybe_debug =

src/goto-symex/symex_dereference.cpp

@@ -281,7 +281,6 @@ void goto_symext::dereference_rec(
     value_set_dereferencet dereference(
       ns,
       state.symbol_table,
-      options,
       symex_dereference_state,
       language_mode,
       expr_is_not_null);

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(options.get_bool_option("partial-loops"))
+    if(partial_loops)
     {
       // it's ok, ignore
     }
     else
     {
-      if(options.get_bool_option("unwinding-assertions"))
+      if(unwinding_assertions)
         vcc(false_exprt(), "recursion unwinding assertion", state);
 
       // add to state guard to prevent further assignments

src/goto-symex/symex_goto.cpp

@@ -515,12 +515,6 @@ void goto_symext::loop_bound_exceeded(
   else
     negated_cond=not_exprt(guard);
 
-  bool unwinding_assertions=
-    options.get_bool_option("unwinding-assertions");
-
-  bool partial_loops=
-    options.get_bool_option("partial-loops");
-
   if(!partial_loops)
   {
     if(unwinding_assertions)

src/pointer-analysis/goto_program_dereference.h

@@ -30,13 +30,13 @@ class goto_program_dereferencet:protected dereference_callbackt
     const namespacet &_ns,
     symbol_tablet &_new_symbol_table,
     const optionst &_options,
-    value_setst &_value_sets):
-    options(_options),
-    ns(_ns),
-    value_sets(_value_sets),
-    dereference(_ns, _new_symbol_table, _options, *this, ID_nil, false)
-    {
-    }
+    value_setst &_value_sets)
+    : options(_options),
+      ns(_ns),
+      value_sets(_value_sets),
+      dereference(_ns, _new_symbol_table, *this, ID_nil, false)
+  {
+  }
 
   void dereference_program(
     goto_programt &goto_program,

src/pointer-analysis/value_set_dereference.h

@@ -32,8 +32,6 @@ class value_set_dereferencet
   /*! \brief Constructor
    * \param _ns Namespace
    * \param _new_symbol_table A symbol_table to store new symbols in
-   * \param _options Options, in particular whether pointer checks are
-            to be performed
    * \param _dereference_callback Callback object for error reporting
    * \param _language_mode Mode for any new symbols created to represent
             a dereference failure
@@ -43,13 +41,11 @@ class value_set_dereferencet
   value_set_dereferencet(
     const namespacet &_ns,
     symbol_tablet &_new_symbol_table,
-    const optionst &_options,
     dereference_callbackt &_dereference_callback,
     const irep_idt _language_mode,
     bool _exclude_null_derefs):
     ns(_ns),
     new_symbol_table(_new_symbol_table),
-    options(_options),
     dereference_callback(_dereference_callback),
     language_mode(_language_mode),
     exclude_null_derefs(_exclude_null_derefs)
@@ -83,7 +79,6 @@ class value_set_dereferencet
 private:
   const namespacet &ns;
   symbol_tablet &new_symbol_table;
-  const optionst &options;
   dereference_callbackt &dereference_callback;
   /// language_mode: ID_java, ID_C or another language identifier
   /// if we know the source language in use, irep_idt() otherwise.