Value-set-dereference: generate let expressions for complex pointers

For the time being symex always lifts these immediately, to avoid having to teach all elements
of cbmc about the let expression.

Author: smowton

src/goto-symex/symex_clean_expr.cpp

@@ -128,6 +128,7 @@ void goto_symext::process_array_expr(statet &state, exprt &expr)
     ns, state.symbol_table, symex_dereference_state, language_mode, false);
 
   expr = dereference.dereference(expr);
+  lift_lets(state, expr, symex_targett::assignment_typet::STATE);
 
   ::process_array_expr(expr, symex_config.simplify_opt, ns);
 }
@@ -222,6 +223,7 @@ void goto_symext::clean_expr(
 {
   replace_nondet(expr, path_storage.build_symex_nondet);
   dereference(expr, state, write);
+  lift_lets(state, expr, symex_targett::assignment_typet::STATE);
 
   // make sure all remaining byte extract operations use the root
   // object to avoid nesting of with/update and byte_update when on

src/pointer-analysis/value_set_dereference.cpp

@@ -76,9 +76,24 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
 
   std::list<valuet> values;
 
+  exprt compare_against_pointer = pointer;
+
+  if(pointer.id() != ID_symbol && retained_values.size() >= 2)
+  {
+    symbolt fresh_binder = get_fresh_aux_symbol(
+      pointer.type(),
+      "derefd_pointer",
+      "derefd_pointer",
+      source_locationt(),
+      language_mode,
+      new_symbol_table);
+
+    compare_against_pointer = fresh_binder.symbol_expr();
+  }
+
   for(const auto &value : retained_values)
   {
-    values.push_back(build_reference_to(value, pointer, ns));
+    values.push_back(build_reference_to(value, compare_against_pointer, ns));
 #if 0
     std::cout << "V: " << format(value.pointer_guard) << " --> ";
     std::cout << format(value.value);
@@ -160,9 +175,12 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
     }
   }
 
-  #if 0
+  if(compare_against_pointer != pointer)
+    value = let_exprt(to_symbol_expr(compare_against_pointer), pointer, value);
+
+#if 0
   std::cout << "R: " << format(value) << "\n\n";
-  #endif
+#endif
 
   return value;
 }