Feature to initialize symex with memory snapshot and start from given location

This adds a feature to load a concrete memory snapshot (represented as a JSON
symbol table) into cbmc to initialize goto symex with, and then start symex from
a given program location. The path to the snapshot must be passed to
--memory-snapshot and the initial program location must be specified via
--initial-location. This is a basic first version that only supports the
initialisation of global variables. Moreover, the concrete memory snapshot does
not contain a representation of the stack of the program, hence symex must stop
when it reaches the end of the function in which it was started (but it can go
into callees and return from them).

Author: danpoe

src/cbmc/bmc.cpp

@@ -22,11 +22,18 @@ Author: Daniel Kroening, [email protected]
 #include <goto-symex/show_program.h>
 #include <goto-symex/show_vcc.h>
 
+#include <json/json_parser.h>
+
+#include <json-symtab-language/json_symbol_table.h>
+
 #include <linking/static_lifetime_init.h>
 
 #include <goto-checker/bmc_util.h>
 #include <goto-checker/solver_factory.h>
 
+#include <util/string2int.h>
+#include <util/string_utils.h>
+
 #include "counterexample_beautification.h"
 #include "fault_localization.h"
 
@@ -403,7 +410,94 @@ int bmct::do_language_agnostic_bmc(
 void bmct::perform_symbolic_execution(
   goto_symext::get_goto_functiont get_goto_function)
 {
-  symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table);
+  if(options.is_set("memory-snapshot"))
+  {
+    // start symex from given program location and memory snapshot
+
+    INVARIANT(
+      options.is_set("initial-location"),
+      "during option parsing it should be checked that --initial-location is "
+      "provided when --memory-snapshot is given");
+
+    jsont json;
+    {
+      const bool r = parse_json(
+        options.get_option("memory-snapshot"), ui_message_handler, json);
+
+      if(r)
+      {
+        throw deserialization_exceptiont("failed to read JSON memory snapshot");
+      }
+    }
+
+    symbol_tablet snapshot;
+
+    // throws a deserialization_exceptiont on failure to read JSON symbol table
+    symbol_table_from_json(json, snapshot);
+
+    std::vector<std::string> start;
+    split_string(options.get_option("initial-location"), ':', start, true);
+
+    CHECK_RETURN(start.size() > 0);
+
+    if(start.front().empty() || start.size() > 2)
+    {
+      throw invalid_command_line_argument_exceptiont(
+        "invalid initial location specification", "--initial-location");
+    }
+
+    INVARIANT(
+      !start.back().empty(),
+      "component of initial location specification should not be empty");
+
+    const irep_idt function_id(start.front());
+
+    const goto_functionst::goto_functiont &goto_function =
+      get_goto_function(function_id);
+
+    if(!goto_function.body_available())
+    {
+      throw invalid_command_line_argument_exceptiont(
+        "starting function must have a body", "--initial-location");
+    }
+
+    const goto_programt::instructionst &instructions =
+      goto_function.body.instructions;
+
+    goto_programt::const_targett it = instructions.begin();
+
+    if(start.size() == 2)
+    {
+      // the initial location specification includes a location number
+
+      const unsigned location_number = safe_string2unsigned(start.back());
+
+      const unsigned start_location_number = it->location_number;
+      const unsigned end_location_number =
+        std::prev(instructions.end())->location_number;
+
+      INVARIANT(
+        start_location_number <= end_location_number,
+        "location numbers should be increasing in goto program");
+
+      if(
+        location_number < start_location_number ||
+        location_number > end_location_number)
+      {
+        throw invalid_command_line_argument_exceptiont(
+          "location number does not exist in function", "--initial-location");
+      }
+
+      std::advance(it, location_number - start_location_number);
+    }
+
+    symex.symex_from_instruction_with_snapshot(
+      get_goto_function, symex_symbol_table, snapshot, it);
+  }
+  else
+  {
+    symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table);
+  }
 
   if(options.get_bool_option("validate-ssa-equation"))
   {

src/cbmc/cbmc_parse_options.cpp

@@ -413,6 +413,33 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("validate-goto-model", true);
   }
 
+  {
+    const bool memory_snapshot = cmdline.isset("memory-snapshot");
+    const bool initial_location = cmdline.isset("initial-location");
+
+    if(memory_snapshot || initial_location)
+    {
+      if(!memory_snapshot)
+      {
+        throw invalid_command_line_argument_exceptiont(
+          "--initial-location also requires --memory-snapshot",
+          "--initial-location");
+      }
+      else if(!initial_location)
+      {
+        throw invalid_command_line_argument_exceptiont(
+          "--memory-snapshot also requires --initial-location",
+          "--memory-snapshot");
+      }
+
+      options.set_option(
+        "memory-snapshot", cmdline.get_value("memory-snapshot"));
+
+      options.set_option(
+        "initial-location", cmdline.get_value("initial-location"));
+    }
+  }
+
   PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
 }
 

src/goto-checker/bmc_util.h

@@ -87,7 +87,9 @@ void slice(
   "(unwind):" \
   "(unwindset):" \
   "(graphml-witness):" \
-  "(unwindset):"
+  "(unwindset):" \
+  "(memory-snapshot):" \
+  "(initial-location):"
 
 #define HELP_BMC \
   " --paths [strategy]           explore paths one at a time\n" \
@@ -106,7 +108,13 @@ void slice(
   " --no-self-loops-to-assumptions\n" \
   "                              do not simplify while(1){} to assume(0)\n" \
   " --no-pretty-names            do not simplify identifiers\n" \
-  " --graphml-witness filename   write the witness in GraphML format to filename\n" // NOLINT(*)
+  " --graphml-witness filename   write the witness in GraphML format to " \
+  "filename\n" \
+  " --memory-snapshot <file>     initialize memory from given JSON memory " \
+  "snapshot\n" \
+  " --initial-location <func[:<n>]\n" \
+  "                              start symex from given function and " \
+  "location\n number (use with --memory-snapshot)\n"
 // clang-format on
 
 #endif // CPROVER_GOTO_CHECKER_BMC_UTIL_H

src/goto-symex/goto_symex.h

@@ -118,6 +118,22 @@ class goto_symext
     const get_goto_functiont &get_goto_function,
     symbol_tablet &new_symbol_table);
 
+  /// Symex program starting from given instruction and initialize the memory
+  /// with the given snapshot
+  ///
+  /// \param get_goto_function mapping from function ids to goto functions
+  /// \param new_symbol_table symbol table to which to add symbols generated
+  ///   during symex
+  /// \param snapshot memory snapshot represented as a symbol table, the `value`
+  ///   field of each symbol holds the value to initialize the corresponding
+  ///   symbol expression with
+  /// \param it iterator to goto instruction to start symex from
+  virtual void symex_from_instruction_with_snapshot(
+    const get_goto_functiont &get_goto_function,
+    symbol_tablet &new_symbol_table,
+    const symbol_tablet &snapshot,
+    goto_programt::const_targett it);
+
   /// Performs symbolic execution using a state and equation that have
   /// already been used to symex part of the program. The state is not
   /// re-initialized; instead, symbolic execution resumes from the program

src/goto-symex/symex_main.cpp

@@ -23,6 +23,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <analyses/dirty.h>
 
+#include <iostream>
+
 symex_configt::symex_configt(const optionst &options)
   : max_depth(options.get_unsigned_int_option("depth")),
     doing_path_exploration(options.is_set("paths")),
@@ -321,6 +323,47 @@ void goto_symext::symex_from_entry_point_of(
     state, get_goto_function, new_symbol_table);
 }
 
+void goto_symext::symex_from_instruction_with_snapshot(
+  const get_goto_functiont &get_goto_function,
+  symbol_tablet &new_symbol_table,
+  const symbol_tablet &snapshot,
+  goto_programt::const_targett pc)
+{
+  statet state;
+
+  // First initialize state from snapshot
+
+  state.symex_target = &target;
+  state.source.pc = pc;
+
+  for(const auto &pair : snapshot)
+  {
+    const symbolt &symbol = pair.second;
+
+    if(!symbol.is_static_lifetime)
+      continue;
+
+    symex_assign(state, code_assignt(symbol.symbol_expr(), symbol.value));
+  }
+
+  // Now do actual program
+
+  const irep_idt id = goto_programt::get_function_id(pc);
+  const goto_functionst::goto_functiont &goto_function = get_goto_function(id);
+
+  INVARIANT(
+    goto_function.body_available(), "starting function should have a body");
+
+  initialize_entry_point(
+    state,
+    get_goto_function,
+    id,
+    pc,
+    prev(goto_function.body.instructions.end()));
+
+  symex_with_state(state, get_goto_function, new_symbol_table);
+}
+
 /// do just one step
 void goto_symext::symex_step(
   const get_goto_functiont &get_goto_function,