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/goto-symex/build_goto_trace.cpp

@@ -353,10 +353,12 @@ void build_goto_trace(
       goto_trace_step.io_id = SSA_step.io_id;
       goto_trace_step.formatted = SSA_step.formatted;
       goto_trace_step.called_function = SSA_step.called_function;
-      goto_trace_step.function_arguments = SSA_step.converted_function_arguments;
 
-      for(auto &arg : goto_trace_step.function_arguments)
-        arg = decision_procedure.get(arg);
+      for(const auto &arg : SSA_step.converted_function_arguments)
+      {
+        goto_trace_step.function_arguments.push_back(
+          simplify_expr(decision_procedure.get(arg), ns));
+      }
 
       // update internal field for specific variables in the counterexample
       update_internal_field(SSA_step, goto_trace_step, ns);
@@ -394,15 +396,8 @@ void build_goto_trace(
 
       for(const auto &j : SSA_step.converted_io_args)
       {
-        if(j.is_constant() || j.id() == ID_string_constant)
-        {
-          goto_trace_step.io_args.push_back(j);
-        }
-        else
-        {
-          exprt tmp = decision_procedure.get(j);
-          goto_trace_step.io_args.push_back(tmp);
-        }
+        goto_trace_step.io_args.push_back(
+          simplify_expr(decision_procedure.get(j), ns));
       }
 
       if(SSA_step.is_assert() || SSA_step.is_assume() || SSA_step.is_goto())

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());