Simplify single-path symex checker

Instead of handling the first symex run differently:
Push initial state into the worklist,
then iterate symex until done.

Author: peterschrammel

src/goto-checker/single_path_symex_checker.cpp

@@ -30,44 +30,10 @@ operator()(propertiest &properties)
 {
   resultt result(resultt::progresst::DONE);
 
-  // Unfortunately, the initial symex run is currently handled differently
-  // from the subsequent runs
-  if(!initial_symex_has_run)
-  {
-    initial_symex_has_run = true;
-    first_equation = symex_target_equationt();
-    symex_bmct symex(
-      ui_message_handler,
-      goto_model.get_symbol_table(),
-      first_equation.value(),
-      options,
-      *worklist);
-
-    setup_symex(symex);
-    perform_symex(
-      goto_model,
-      symex,
-      symex_symbol_table,
-      first_equation.value(),
-      options,
-      ns,
-      ui_message_handler);
-
-    output_coverage_report(
-      options.get_option("symex-coverage-report"),
-      goto_model,
-      symex,
-      ui_message_handler);
-
-    if(symex.get_remaining_vccs() > 0)
-    {
-      prepare(result, properties, first_equation.value());
-      decide(result, properties);
-
-      if(result.progress == resultt::progresst::FOUND_FAIL)
-        return result;
-    }
-  }
+  auto get_goto_function =
+    [this](const irep_idt &id) -> const goto_functionst::goto_functiont & {
+    return goto_model.get_goto_function(id);
+  };
 
   // There might be more solutions from the previous equation.
   if(property_decider)
@@ -77,24 +43,28 @@ operator()(propertiest &properties)
       return result;
   }
 
-  if(first_equation.has_value())
+  if(!worklist->empty())
   {
-    // We are in the second iteration. We don't need the equation
-    // from the first iteration anymore.
-    first_equation = {};
+    // We pop the item processed in the previous iteration.
+    worklist->pop();
   }
-  else
+
+  if(!symex_initialized)
   {
-    if(!worklist->empty())
-    {
-      // We are in iteration 3 or later; we pop the item processed
-      // in the previous iteration.
-      worklist->pop();
-    }
-    else
-    {
-      // We are already done.
-    }
+    symex_initialized = true;
+
+    // Put initial state into the work list
+    symex_target_equationt equation;
+    symex_bmct symex(
+      ui_message_handler,
+      goto_model.get_symbol_table(),
+      equation,
+      options,
+      *worklist);
+    setup_symex(symex);
+
+    symex.initialize_path_storage_from_entry_point_of(
+      get_goto_function, symex_symbol_table);
   }
 
   while(!worklist->empty())
@@ -106,16 +76,12 @@ operator()(propertiest &properties)
       resume.equation,
       options,
       *worklist);
-
     setup_symex(symex);
-    perform_symex(
-      goto_model,
-      symex,
-      resume,
-      symex_symbol_table,
-      options,
-      ns,
-      ui_message_handler);
+
+    symex.resume_symex_from_saved_state(
+      get_goto_function, resume.state, &resume.equation, symex_symbol_table);
+    postprocess_equation(
+      symex, resume.equation, options, ns, ui_message_handler);
 
     output_coverage_report(
       options.get_option("symex-coverage-report"),

src/goto-checker/single_path_symex_checker.h

@@ -43,8 +43,7 @@ class single_path_symex_checkert : public single_path_symex_only_checkert,
   virtual ~single_path_symex_checkert() = default;
 
 protected:
-  bool initial_symex_has_run = false;
-  optionalt<symex_target_equationt> first_equation; // for building traces
+  bool symex_initialized = false;
   std::unique_ptr<goto_symex_property_decidert> property_decider;
 
   void prepare(

src/goto-checker/single_path_symex_only_checker.cpp

@@ -37,29 +37,24 @@ operator()(propertiest &properties)
 {
   resultt result(resultt::progresst::DONE);
 
-  // First run goto-symex from entry point to initialize worklist
+  auto get_goto_function =
+    [this](const irep_idt &id) -> const goto_functionst::goto_functiont & {
+    return goto_model.get_goto_function(id);
+  };
+
   {
-    symex_target_equationt first_equation;
+    // Put initial state into the work list
+    symex_target_equationt equation;
     symex_bmct symex(
       ui_message_handler,
       goto_model.get_symbol_table(),
-      first_equation,
+      equation,
       options,
       *worklist);
-
     setup_symex(symex);
-    perform_symex(
-      goto_model,
-      symex,
-      symex_symbol_table,
-      first_equation,
-      options,
-      ns,
-      ui_message_handler);
 
-    equation_output(symex, first_equation);
-    update_properties_status_from_symex_target_equation(
-      properties, result.updated_properties, first_equation);
+    symex.initialize_path_storage_from_entry_point_of(
+      get_goto_function, symex_symbol_table);
   }
 
   while(!worklist->empty())
@@ -71,17 +66,15 @@ operator()(propertiest &properties)
       resume.equation,
       options,
       *worklist);
-
     setup_symex(symex);
-    perform_symex(
-      goto_model,
-      symex,
-      resume,
-      symex_symbol_table,
-      options,
-      ns,
-      ui_message_handler);
+
+    symex.resume_symex_from_saved_state(
+      get_goto_function, resume.state, &resume.equation, symex_symbol_table);
+    postprocess_equation(
+      symex, resume.equation, options, ns, ui_message_handler);
+
     equation_output(symex, resume.equation);
+
     update_properties_status_from_symex_target_equation(
       properties, result.updated_properties, resume.equation);