Interpreter: de-duplicate code

regression/CMakeLists.txt

@@ -61,6 +61,7 @@ add_subdirectory(linking-goto-binaries)
 add_subdirectory(symtab2gb)
 add_subdirectory(validate-trace-xml-schema)
 add_subdirectory(cbmc-primitives)
+add_subdirectory(goto-interpreter)
 add_subdirectory(cbmc-sequentialization)
 
 if(WITH_MEMORY_ANALYZER)

regression/Makefile

@@ -35,6 +35,7 @@ DIRS = cbmc \
        goto-ld \
        validate-trace-xml-schema \
        cbmc-primitives \
+       goto-interpreter \
        # Empty last line
 
 ifeq ($(OS),Windows_NT)

regression/goto-interpreter/CMakeLists.txt

@@ -0,0 +1,9 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> ${is_windows}"
+)

regression/goto-interpreter/Makefile

@@ -0,0 +1,35 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows=true
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows=false
+endif
+
+test:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)'
+
+tests.log:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)'
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done

regression/goto-interpreter/byte_extract/main.c

@@ -0,0 +1,20 @@
+union U {
+  int x;
+  char c[sizeof(int)];
+};
+
+int main()
+{
+  union U u;
+  // make the lowest and highest byte 1
+  u.x = 1 | (1 << (sizeof(int) * 8 - 8));
+  int i = u.x;
+  char c0 = u.c[0];
+  char c1 = u.c[1];
+  char c2 = u.c[2];
+  char c3 = u.c[3];
+
+  __CPROVER_assert(u.c[0] == 1, "");
+
+  return 0;
+}

regression/goto-interpreter/byte_extract/test.desc

@@ -0,0 +1,13 @@
+KNOWNBUG
+main.c
+se
+^Starting interpreter$
+^\d+- Program End\.$
+^EXIT=0$
+^SIGNAL=0$
+--
+^assertion failed at \d+$
+--
+The memory model of the interpreter does not record individual bytes. Therefore,
+an access to individual bytes still yields the full object, making the assertion
+in this test spuriously fail.

regression/goto-interpreter/byte_extract/union.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+se
+^Starting interpreter$
+^\d+- Program End\.$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-interpreter/chain.sh

@@ -0,0 +1,20 @@
+#!/usr/bin/env bash
+
+set -e
+
+goto_cc=$1
+goto_instrument=$2
+is_windows=$3
+
+options=${*:4:$#-4}
+name=${*:$#}
+base_name=${name%.c}
+
+if [[ "${is_windows}" == "true" ]]; then
+  "${goto_cc}" "${name}"
+  mv "${base_name}.exe" "${base_name}.gb"
+else
+  "${goto_cc}" "${name}" -o "${base_name}.gb"
+fi
+
+echo ${options} | tr , '\n' | "${goto_instrument}" --interpreter "${base_name}.gb"

regression/goto-interpreter/help-output/main.c

@@ -0,0 +1,4 @@
+int main()
+{
+  return 0;
+}

regression/goto-interpreter/help-output/test.desc

@@ -0,0 +1,19 @@
+CORE
+main.c
+h,q
+^Starting interpreter$
+^Interpreter help$
+^h: display this menu$
+^j: output json trace$
+^m: output memory dump$
+^o: output goto trace$
+^q: quit$
+^r: run up to entry point$
+^s#: step a number of instructions$
+^sa: step across a function$
+^so: step out of a function$
+^se: step until end of program$
+^\d+- Program End\.$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-interpreter/memory-dump/main.c

@@ -0,0 +1,4 @@
+int main()
+{
+  return 0;
+}

regression/goto-interpreter/memory-dump/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+m
+^Starting interpreter$
+^__CPROVER_rounding_mode\[0\]=0$
+^\d+- Program End\.$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-interpreter/step/main.c

@@ -0,0 +1,11 @@
+int main()
+{
+  __CPROVER_rounding_mode = 1;
+  // test single stepping
+  int i = 1;
+  i = 2;
+  i = 3;
+  int x;
+  __CPROVER_assert(x == 42, "should fail");
+  return 0;
+}

regression/goto-interpreter/step/r.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+r,q
+^Starting interpreter$
+^\d+- Program End\.$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-interpreter/step/test.desc

@@ -0,0 +1,20 @@
+CORE
+main.c
+r0,s,sa,m,s2,m,s2,m,so,m,se
+^Starting interpreter$
+^__CPROVER_rounding_mode\[0\]=0$
+^__CPROVER_rounding_mode\[0\]=1$
+^main::1::i\[0\]=1$
+^\d+- Program End\.$
+^EXIT=0$
+^SIGNAL=0$
+--
+^main::1::i\[0\]=2$
+--
+Use the various step instructions: restart execution without running
+initialization (r0), execute one step (s), step over __CPROVER_initialize (sa),
+generate the first memory dump (__CPROVER_rounding_mode set to 0), step into
+main and execute the first assignment (__CPROVER_rounding_mode set to 1),
+execute two steps (s2) to declare i and assign 1 to i, step to the end of the
+function (so) without dumping intermittent values, thus never dumping i==2. The
+execute to the end of the program (se).

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -41,6 +41,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/restrict_function_pointers.h>
+#include <goto-programs/rewrite_union.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/show_symbol_table.h>
@@ -599,6 +600,9 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("interpreter"))
     {
+      do_indirect_call_and_rtti_removal();
+      rewrite_union(goto_model);
+
       log.status() << "Starting interpreter" << messaget::eom;
       interpreter(goto_model, ui_message_handler);
       return CPROVER_EXIT_SUCCESS;

src/goto-programs/interpreter.cpp

@@ -64,6 +64,8 @@ void interpretert::operator()()
 void interpretert::initialize(bool init)
 {
   build_memory_map();
+  // reset the call stack
+  call_stack = call_stackt{};
 
   total_steps=0;
   const goto_functionst::function_mapt::const_iterator
@@ -83,15 +85,20 @@ void interpretert::initialize(bool init)
   done=false;
   if(init)
   {
-    stack_depth=call_stack.size()+1;
-    show_state();
-    step();
-    while(!done && (stack_depth<=call_stack.size()) && (stack_depth!=npos))
+    // execute instructions up to and including __CPROVER_initialize()
+    while(!done && call_stack.size() == 0)
     {
       show_state();
       step();
     }
-    while(!done && (call_stack.size()==0))
+    // initialization
+    while(!done && call_stack.size() > 0)
+    {
+      show_state();
+      step();
+    }
+    // invoke the user entry point
+    while(!done && call_stack.size() == 0)
     {
       show_state();
       step();
@@ -140,18 +147,18 @@ void interpretert::command()
     done=true;
   else if(ch=='h')
   {
-    status()
-      << "Interpreter help\n"
-      << "h: display this menu\n"
-      << "j: output json trace\n"
-      << "m: output memory dump\n"
-      << "o: output goto trace\n"
-      << "q: quit\n"
-      << "r: run until completion\n"
-      << "s#: step a number of instructions\n"
-      << "sa: step across a function\n"
-      << "so: step out of a function\n"
-      << eom;
+    status() << "Interpreter help\n"
+             << "h: display this menu\n"
+             << "j: output json trace\n"
+             << "m: output memory dump\n"
+             << "o: output goto trace\n"
+             << "q: quit\n"
+             << "r: run up to entry point\n"
+             << "s#: step a number of instructions\n"
+             << "sa: step across a function\n"
+             << "so: step out of a function\n"
+             << "se: step until end of program\n"
+             << eom;
   }
   else if(ch=='j')
   {
@@ -200,7 +207,7 @@ void interpretert::command()
   else if((ch=='s') || (ch==0))
   {
     num_steps=1;
-    stack_depth=npos;
+    std::size_t stack_depth = npos;
     ch=tolower(command[1]);
     if(ch=='e')
       num_steps=npos;
@@ -210,7 +217,7 @@ void interpretert::command()
       stack_depth=call_stack.size()+1;
     else
     {
-      num_steps=safe_string2size_t(command+1);
+      num_steps = unsafe_string2size_t(command + 1);
       if(num_steps==0)
         num_steps=1;
     }
@@ -742,9 +749,7 @@ void interpretert::execute_assert()
 {
   if(!evaluate_boolean(pc->get_condition()))
   {
-    if((target_assert==pc) || stop_on_assertion)
-      throw "program assertion reached";
-    else if(show)
+    if(show)
       error() << "assertion failed at " << pc->location_number
               << "\n" << eom;
   }
@@ -860,6 +865,7 @@ void interpretert::execute_function_call()
 void interpretert::build_memory_map()
 {
   // put in a dummy for NULL
+  memory.clear();
   memory.resize(1);
   inverse_memory_map[0] = {};
 
@@ -1071,12 +1077,11 @@ void interpretert::print_memory(bool input_flags)
     const memory_cellt &cell=cell_address.second;
     const auto identifier = address_to_symbol(i).get_identifier();
     const auto offset=address_to_offset(i);
-    debug() << identifier << "[" << offset << "]"
-            << "=" << cell.value << eom;
+    status() << identifier << "[" << offset << "]"
+             << "=" << cell.value << eom;
     if(input_flags)
-      debug() << "(" << static_cast<int>(cell.initialized) << ")"
-              << eom;
-    debug() << eom;
+      status() << "(" << static_cast<int>(cell.initialized) << ")" << eom;
+    status() << eom;
   }
 }
 

src/goto-programs/interpreter_class.h

@@ -30,14 +30,13 @@ class interpretert:public messaget
   interpretert(
     const symbol_tablet &_symbol_table,
     const goto_functionst &_goto_functions,
-    message_handlert &_message_handler):
-    messaget(_message_handler),
-    symbol_table(_symbol_table),
-    ns(_symbol_table),
-    goto_functions(_goto_functions),
-    stack_pointer(0),
-    done(false),
-    stop_on_assertion(false)
+    message_handlert &_message_handler)
+    : messaget(_message_handler),
+      symbol_table(_symbol_table),
+      ns(_symbol_table),
+      goto_functions(_goto_functions),
+      stack_pointer(0),
+      done(false)
   {
     show=true;
   }
@@ -265,18 +264,16 @@ class interpretert:public messaget
   list_input_varst function_input_vars;
 
   goto_functionst::function_mapt::const_iterator function;
-  goto_programt::const_targett pc, next_pc, target_assert;
+  goto_programt::const_targett pc, next_pc;
   goto_tracet steps;
   bool done;
   bool show;
-  bool stop_on_assertion;
   static const size_t npos;
   size_t num_steps;
   size_t total_steps;
 
   dynamic_typest dynamic_types;
   int num_dynamic_objects;
-  mp_integer stack_depth;
   unsigned thread_id;
 
   bool evaluate_boolean(const exprt &expr)