goto-program interpreter: test byte_extract handling

Fix basic execution as sparse vectors do not (yet) support resizing to
smaller sizes (performing a clear+resize instead), and perform goto
program rewrites before starting the interpreter.

Author: tautschnig

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.

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

@@ -860,6 +860,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] = {};
 

src/util/sparse_vector.h

@@ -51,6 +51,12 @@ template<class T> class sparse_vectort
     _size=new_size;
   }
 
+  void clear()
+  {
+    underlying.clear();
+    _size = 0;
+  }
+
   typedef typename underlyingt::iterator iteratort;
   typedef typename underlyingt::const_iterator const_iteratort;