goto-program interpreter: test and fix stepping commands

"s" without a suffix or with a suffix that is not one of [aeo0-9]
previously resulted in an invariant violation. Also make "r0" actually
work by fixing the assumptions about the structure of the top-level
function.

Author: tautschnig

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

@@ -1,6 +1,6 @@
 CORE
 main.c
-s1,so,m
+m
 ^Starting interpreter$
 ^__CPROVER_rounding_mode\[0\]=0$
 ^\d+- Program End\.$

regression/goto-interpreter/step/main.c

@@ -1,5 +1,10 @@
 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/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-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();
+    }
+    // initialization
+    while(!done && call_stack.size() > 0)
     {
       show_state();
       step();
     }
-    while(!done && (call_stack.size()==0))
+    // invoke the user entry point
+    while(!done && call_stack.size() == 0)
     {
       show_state();
       step();
@@ -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;
     }

src/goto-programs/interpreter_class.h

@@ -274,7 +274,6 @@ class interpretert:public messaget
 
   dynamic_typest dynamic_types;
   int num_dynamic_objects;
-  mp_integer stack_depth;
   unsigned thread_id;
 
   bool evaluate_boolean(const exprt &expr)