Interpreter: de-duplicate code and make it not fail for unions

evaluate_address(byte_extract) and evaluate(byte_extract) had almost the
same implementation. Instead of the duplication, use `evaluate_address`
to implement `evaluate` and just handle the remaining bits in
`evaluate`.

byte_extract still has a number of problems, as the regression test
shows: addressing works at the object level, not at the level of
individual bytes. Thus we can compute the correct address, but still
wouldn't access the right bytes.

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.

regression/goto-interpreter/byte_extract/union.desc

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

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_evaluate.cpp

@@ -857,41 +857,11 @@ void interpretert::evaluate(
     }
     return;
   }
-  else if(expr.id()==ID_byte_extract_little_endian ||
-          expr.id()==ID_byte_extract_big_endian)
-  {
-    const auto &byte_extract_expr = to_byte_extract_expr(expr);
-
-    mp_vectort extract_offset;
-    evaluate(byte_extract_expr.op1(), extract_offset);
-    mp_vectort extract_from;
-    evaluate(byte_extract_expr.op0(), extract_from);
-
-    if(extract_offset.size()==1 && extract_from.size()!=0)
-    {
-      const typet &target_type=expr.type();
-      mp_integer memory_offset;
-      // If memory offset is found (which should normally be the case)
-      // extract the corresponding data from the appropriate memory location
-      if(!byte_offset_to_memory_offset(
-           byte_extract_expr.op0().type(), extract_offset[0], memory_offset))
-      {
-        mp_integer target_type_leaves;
-        if(!count_type_leaves(target_type, target_type_leaves) &&
-           target_type_leaves>0)
-        {
-          dest.insert(dest.end(),
-            extract_from.begin()+memory_offset.to_long(),
-            extract_from.begin()+(memory_offset+target_type_leaves).to_long());
-          return;
-        }
-      }
-    }
-  }
-  else if(expr.id()==ID_dereference ||
-          expr.id()==ID_index ||
-          expr.id()==ID_symbol ||
-          expr.id()==ID_member)
+  else if(
+    expr.id() == ID_dereference || expr.id() == ID_index ||
+    expr.id() == ID_symbol || expr.id() == ID_member ||
+    expr.id() == ID_byte_extract_little_endian ||
+    expr.id() == ID_byte_extract_big_endian)
   {
     mp_integer address=evaluate_address(
       expr,
@@ -932,16 +902,45 @@ void interpretert::evaluate(
     }
     else if(!address.is_zero())
     {
-      if(!unbounded_size(expr.type()))
+      if(
+        expr.id() == ID_byte_extract_little_endian ||
+        expr.id() == ID_byte_extract_big_endian)
+      {
+        const auto &byte_extract_expr = to_byte_extract_expr(expr);
+
+        mp_vectort extract_from;
+        evaluate(byte_extract_expr.op(), extract_from);
+        INVARIANT(
+          !extract_from.empty(),
+          "evaluate_address should have returned address == 0");
+        const mp_integer memory_offset =
+          address - evaluate_address(byte_extract_expr.op(), true);
+        const typet &target_type = expr.type();
+        mp_integer target_type_leaves;
+        if(
+          !count_type_leaves(target_type, target_type_leaves) &&
+          target_type_leaves > 0)
+        {
+          dest.insert(
+            dest.end(),
+            extract_from.begin() + numeric_cast_v<std::size_t>(memory_offset),
+            extract_from.begin() +
+              numeric_cast_v<std::size_t>(memory_offset + target_type_leaves));
+          return;
+        }
+        // we fail
+      }
+      else if(!unbounded_size(expr.type()))
       {
         dest.resize(numeric_cast_v<std::size_t>(get_size(expr.type())));
         read(address, dest);
+        return;
       }
       else
       {
         read_unbounded(address, dest);
+        return;
       }
-      return;
     }
   }
   else if(expr.id()==ID_typecast)