Merge pull request #2262 from karkhaz/kk-rm-noop-depth-lookup

Don't do string lookups in symex main loop

Author: tautschnig

src/cbmc/bmc.cpp

@@ -305,7 +305,6 @@ void bmct::get_memory_model()
 void bmct::setup()
 {
   get_memory_model();
-  symex.options=options;
 
   {
     const symbolt *init_symbol;

src/cbmc/bmc.h

@@ -76,7 +76,12 @@ class bmct:public safety_checkert
       ns(outer_symbol_table, symex_symbol_table),
       equation(),
       path_storage(_path_storage),
-      symex(_message_handler, outer_symbol_table, equation, path_storage),
+      symex(
+        _message_handler,
+        outer_symbol_table,
+        equation,
+        options,
+        path_storage),
       prop_conv(_prop_conv),
       ui(ui_message_handlert::uit::PLAIN),
       driver_callback_after_symex(callback_after_symex)
@@ -150,7 +155,12 @@ class bmct:public safety_checkert
       ns(outer_symbol_table),
       equation(_equation),
       path_storage(_path_storage),
-      symex(_message_handler, outer_symbol_table, equation, path_storage),
+      symex(
+        _message_handler,
+        outer_symbol_table,
+        equation,
+        options,
+        path_storage),
       prop_conv(_prop_conv),
       ui(ui_message_handlert::uit::PLAIN),
       driver_callback_after_symex(callback_after_symex)

src/cbmc/symex_bmc.cpp

@@ -22,8 +22,9 @@ symex_bmct::symex_bmct(
   message_handlert &mh,
   const symbol_tablet &outer_symbol_table,
   symex_target_equationt &_target,
+  const optionst &options,
   path_storaget &path_storage)
-  : goto_symext(mh, outer_symbol_table, _target, path_storage),
+  : goto_symext(mh, outer_symbol_table, _target, options, path_storage),
     record_coverage(false),
     symex_coverage(ns)
 {

src/cbmc/symex_bmc.h

@@ -29,6 +29,7 @@ class symex_bmct: public goto_symext
     message_handlert &mh,
     const symbol_tablet &outer_symbol_table,
     symex_target_equationt &_target,
+    const optionst &options,
     path_storaget &path_storage);
 
   // To show progress

src/goto-instrument/accelerate/scratch_program.h

@@ -43,12 +43,16 @@ class scratch_programt:public goto_programt
       ns(symbol_table, symex_symbol_table),
       equation(),
       path_storage(),
-      symex(mh, symbol_table, equation, path_storage),
+      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);
@@ -80,6 +84,7 @@ class scratch_programt:public goto_programt
   namespacet ns;
   symex_target_equationt equation;
   path_fifot path_storage;
+  optionst options;
   goto_symext symex;
 
   std::unique_ptr<propt> satcheck;

src/goto-symex/goto_symex.h

@@ -52,8 +52,12 @@ class goto_symext
     message_handlert &mh,
     const symbol_tablet &outer_symbol_table,
     symex_target_equationt &_target,
+    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")),
       total_vccs(0),
       remaining_vccs(0),
       constant_propagation(true),
@@ -67,8 +71,6 @@ class goto_symext
       guard_identifier("goto_symex::\\guard"),
       path_storage(path_storage)
   {
-    options.set_option("simplify", true);
-    options.set_option("assertions", true);
   }
 
   virtual ~goto_symext()
@@ -195,6 +197,11 @@ class goto_symext
     const get_goto_functiont &,
     statet &);
 
+  const optionst &options;
+
+  const unsigned max_depth;
+  const bool doing_path_exploration;
+
 public:
   // these bypass the target maps
   virtual void symex_step_goto(statet &, bool taken);
@@ -205,8 +212,6 @@ class goto_symext
   bool constant_propagation;
   bool self_loops_to_assumptions;
 
-  optionst options;
-
   /// 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;

src/goto-symex/symex_goto.cpp

@@ -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.
-     options.get_bool_option("paths")))
+     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(options.get_bool_option("paths"))
+  else if(doing_path_exploration)
   {
     // We should save both the instruction after this goto, and the target of
     // the goto.

src/goto-symex/symex_main.cpp

@@ -308,16 +308,13 @@ void goto_symext::symex_step(
 
   const goto_programt::instructiont &instruction=*state.source.pc;
 
-  if(!options.get_bool_option("paths"))
+  if(!doing_path_exploration)
     merge_gotos(state);
 
   // depth exceeded?
-  {
-    unsigned max_depth=options.get_unsigned_int_option("depth");
-    if(max_depth!=0 && state.depth>max_depth)
-      state.guard.add(false_exprt());
-    state.depth++;
-  }
+  if(max_depth != 0 && state.depth > max_depth)
+    state.guard.add(false_exprt());
+  state.depth++;
 
   // actually do instruction
   switch(instruction.type)