SMT back-end: Extend trace value evaluation

We record the values of expressions by adding `expr == expr`
as constraints in order to be able to fetch and display them in the GOTO
trace (for declaration; we presently also introduce new symbols in other
cases). Constructing a trace then requires the ability to evaluate all
kinds of expressions to obtain the value for those expressions.

Fixes: #7308

Author: tautschnig

regression/cbmc/Empty_struct3/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+struct Unit
+{
+};
+
+int main()
+{
+  struct Unit var_0;
+  int x;
+  int y = x;
+  assert(0);
+  assert(y == x);
+  return 0;
+}

regression/cbmc/Empty_struct3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--json-ui
+VERIFICATION FAILED
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/trace-values/trace-values.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 trace-values.c
 --trace
 ^EXIT=10$

regression/cbmc/trace_options_json_extended/extended.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 test.c
 --trace --json-ui --trace-json-extended
 ^EXIT=10$

regression/cbmc/trace_options_json_extended/non-extended.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 test.c
 --trace --json-ui
 ^EXIT=10$

regression/validate-trace-xml-schema/check.py

@@ -56,6 +56,7 @@
     # this uses json-ui (fails for a different reason actually, but should also
     #   fail because of command line incompatibility)
     ['json1', 'test.desc'],
+    ['Empty_struct3', 'test.desc'],
     # uses show-goto-functions
     ['reachability-slice', 'test.desc'],
     ['reachability-slice', 'test2.desc'],

src/solvers/smt2/smt2_conv.cpp

@@ -297,14 +297,6 @@ exprt smt2_convt::get(const exprt &expr) const
     if(it!=identifier_map.end())
       return it->second.value;
   }
-  else if(expr.id()==ID_member)
-  {
-    const member_exprt &member_expr=to_member_expr(expr);
-    exprt tmp=get(member_expr.struct_op());
-    if(tmp.is_nil())
-      return nil_exprt();
-    return member_exprt(tmp, member_expr.get_component_name(), expr.type());
-  }
   else if(expr.id() == ID_literal)
   {
     auto l = to_literal_expr(expr).get_literal();
@@ -321,16 +313,23 @@ exprt smt2_convt::get(const exprt &expr) const
     else if(op.is_false())
       return true_exprt();
   }
-  else if(expr.is_constant())
+  else if(
+    expr.is_constant() || expr.id() == ID_empty_union ||
+    (!expr.has_operands() && (expr.id() == ID_struct || expr.id() == ID_array)))
+  {
     return expr;
-  else if(const auto &array = expr_try_dynamic_cast<array_exprt>(expr))
+  }
+  else if(expr.has_operands())
   {
-    exprt array_copy = *array;
-    for(auto &element : array_copy.operands())
+    exprt copy = expr;
+    for(auto &op : copy.operands())
     {
-      element = get(element);
+      exprt eval_op = get(op);
+      if(eval_op.is_nil())
+        return nil_exprt{};
+      op = std::move(eval_op);
     }
-    return array_copy;
+    return copy;
   }
 
   return nil_exprt();
@@ -4780,7 +4779,9 @@ void smt2_convt::set_to(const exprt &expr, bool value)
       const irep_idt &identifier=
         to_symbol_expr(equal_expr.lhs()).get_identifier();
 
-      if(identifier_map.find(identifier)==identifier_map.end())
+      if(
+        identifier_map.find(identifier) == identifier_map.end() &&
+        equal_expr.lhs() != equal_expr.rhs())
       {
         identifiert &id=identifier_map[identifier];
         CHECK_RETURN(id.type.is_nil());