Remove string lookups from goto_symext main loop

Lookups into goto_symext's options member have been replaced by accesses
to instance members that are initialized from the optionst reference by
goto_symext's constructor.

This commit fixes diffblue#2050.

Author: karkhaz

src/goto-symex/goto_symex.h

@@ -56,6 +56,8 @@ class goto_symext
     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),
@@ -197,6 +199,9 @@ class goto_symext
 
   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);

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)