Don't generate unnecessary fresh symbols for the GOTO trace

We can safely 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. This was already being done for declarations. Introducing new
symbols just adds unnecessary variables to the formula.

Author: tautschnig

regression/cbmc-incr-smt2/pointers-conversions/pointer_to_int.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 pointer_to_int.c
 --trace
 \[main\.assertion\.1\] line \d+ expected result == -1: success: SUCCESS

src/goto-symex/build_goto_trace.cpp

@@ -351,10 +351,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);
@@ -391,15 +393,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/goto-symex/symex_target_equation.cpp

@@ -620,33 +620,18 @@ void symex_target_equationt::convert_function_calls(
   {
     if(!step.ignore)
     {
-      and_exprt::operandst conjuncts;
       step.converted_function_arguments.reserve(step.ssa_function_arguments.size());
 
       for(const auto &arg : step.ssa_function_arguments)
       {
-        if(arg.is_constant() ||
-           arg.id()==ID_string_constant)
-          step.converted_function_arguments.push_back(arg);
-        else
+        if(!arg.is_constant() && arg.id() != ID_string_constant)
         {
-          const irep_idt identifier="symex::args::"+std::to_string(argument_count++);
-          symbol_exprt symbol(identifier, arg.type());
-
-          equal_exprt eq(arg, symbol);
+          equal_exprt eq{arg, arg};
           merge_irep(eq);
-
-          decision_procedure.set_to(eq, true);
-          conjuncts.push_back(eq);
-          step.converted_function_arguments.push_back(symbol);
+          decision_procedure.set_to_true(eq);
         }
+        step.converted_function_arguments.push_back(arg);
       }
-      with_solver_hardness(
-        decision_procedure,
-        [step_index, &conjuncts, &step](solver_hardnesst &hardness) {
-          hardness.register_ssa(
-            step_index, conjunction(conjuncts), step.source.pc);
-        });
     }
     ++step_index;
   }
@@ -659,32 +644,16 @@ void symex_target_equationt::convert_io(decision_proceduret &decision_procedure)
   {
     if(!step.ignore)
     {
-      and_exprt::operandst conjuncts;
       for(const auto &arg : step.io_args)
       {
-        if(arg.is_constant() ||
-           arg.id()==ID_string_constant)
-          step.converted_io_args.push_back(arg);
-        else
+        if(!arg.is_constant() && arg.id() != ID_string_constant)
         {
-          const irep_idt identifier =
-            "symex::io::" + std::to_string(io_count++);
-          symbol_exprt symbol(identifier, arg.type());
-
-          equal_exprt eq(arg, symbol);
+          equal_exprt eq{arg, arg};
           merge_irep(eq);
-
-          decision_procedure.set_to(eq, true);
-          conjuncts.push_back(eq);
-          step.converted_io_args.push_back(symbol);
+          decision_procedure.set_to_true(eq);
         }
+        step.converted_io_args.push_back(arg);
       }
-      with_solver_hardness(
-        decision_procedure,
-        [step_index, &conjuncts, &step](solver_hardnesst &hardness) {
-          hardness.register_ssa(
-            step_index, conjunction(conjuncts), step.source.pc);
-        });
     }
     ++step_index;
   }

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();
@@ -323,14 +315,17 @@ exprt smt2_convt::get(const exprt &expr) const
   }
   else if(expr.is_constant())
     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();
@@ -4641,7 +4636,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());