Merge pull request #7218 from diffblue/chc_trace_rhs

CHC solver: use address_of on RHS in counterexample traces

Author: kroening

regression/cprover/trace/trace_malloc1.desc

@@ -4,7 +4,7 @@ trace_malloc1.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^Trace for main\.assertion\.1:$
-^   5 main::\$tmp::return_value_malloc := ❝heap-1❞$
+^   5 main::\$tmp::return_value_malloc := address_of\(heap-1\)$
 ^   5 main::1::p := cast\(❝heap-1❞, signedbv\[32\]\*\)$
 ^   7 \[cast\(❝heap-1❞, signedbv\[32\]\*\) \+ 10\] := 1$
 ^   8 \[cast\(❝heap-1❞, signedbv\[32\]\*\) \+ 20\] := 2$

regression/cprover/trace/trace_pointer2.desc

@@ -4,6 +4,6 @@ trace_pointer2.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^Trace for main\.assertion\.1:$
-^   6 main::1::x := element_address\(❝main::1::array❞, 0\)$
+^   6 main::1::x := address_of\(main::1::array\[0\]\)$
 ^   7 main::1::array\[2\] := 123$
 --

regression/cprover/trace/trace_pointer3.desc

@@ -4,6 +4,6 @@ trace_pointer3.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^Trace for main\.assertion\.1:$
-^   8 main::1::p := ❝x❞$
+^   8 main::1::p := address_of\(x\)$
 ^   9 x\.b := 123$
 --

regression/cprover/trace/trace_struct1.desc

@@ -4,6 +4,6 @@ trace_struct1.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^Trace for main\.assertion\.1:$
-^  10 main::1::p := ❝x❞\.❝c❞$
+^  10 main::1::p := address_of\(x\.c\)$
 ^  11 x\.c := 789$
 --

src/cprover/report_traces.cpp

@@ -61,6 +61,15 @@ optionalt<exprt> address_to_lvalue(exprt src)
     return {};
 }
 
+static exprt use_address_of(exprt src)
+{
+  auto src_lvalue_opt = address_to_lvalue(src);
+  if(src_lvalue_opt.has_value())
+    return address_of_exprt(*src_lvalue_opt);
+  else
+    return src;
+}
+
 void show_trace(
   const std::vector<framet> &frames,
   const propertyt &property,
@@ -123,13 +132,17 @@ void show_trace(
           consolet::out() << std::setw(4) << ' ';
         }
 
-        auto lvalue_opt = address_to_lvalue(update.address);
-        if(lvalue_opt.has_value())
-          consolet::out() << format(*lvalue_opt);
+        // use an l-value expression for better readability, if possible
+        auto lhs_lvalue_opt = address_to_lvalue(update.address);
+        if(lhs_lvalue_opt.has_value())
+          consolet::out() << format(*lhs_lvalue_opt);
         else
           consolet::out() << '[' << format(update.address) << ']';
 
-        consolet::out() << " := " << format(update.value);
+        // use address_of for better readability
+        auto value_with_address_of = use_address_of(update.value);
+
+        consolet::out() << " := " << format(value_with_address_of);
         consolet::out() << '\n';
       }
     }