Use format instead of from_expr

Author: peterschrammel

regression/cbmc-shadow-memory/void-ptr-param-get1/test.desc

@@ -3,6 +3,6 @@ main.c
 --verbosity 10
 ^EXIT=6$
 ^SIGNAL=0$
-Shadow memory: cannot get shadow memory via type void\* for s
+Shadow memory: cannot get shadow memory via type void\* for f_void_ptr::s
 --
 ^warning: ignoring

regression/cbmc-shadow-memory/void-ptr-param-set1/test.desc

@@ -3,6 +3,6 @@ main.c
 --verbosity 10
 ^EXIT=6$
 ^SIGNAL=0$
-Shadow memory: cannot set shadow memory via type void\* for s
+Shadow memory: cannot set shadow memory via type void\* for f_void_ptr::s
 --
 ^warning: ignoring

src/goto-symex/symex_shadow_memory.cpp

@@ -18,6 +18,7 @@ Author: Peter Schrammel
 #include <util/cprover_prefix.h>
 #include <util/expr_initializer.h>
 #include <util/find_symbols.h>
+#include <util/format_expr.h>
 #include <util/fresh_symbol.h>
 #include <util/invariant.h>
 #include <util/message.h>
@@ -94,10 +95,10 @@ void goto_symext::initialize_shadow_memory(
 
     log.conditional_output(
       log.debug(),
-      [field, field_pair, this, address_expr](messaget::mstreamt &mstream) {
+      [field, field_pair, address_expr](messaget::mstreamt &mstream) {
         mstream << "Shadow memory: initialize field " << id2string(field.get_identifier())
-                << " for " << from_expr(ns, "", address_expr)
-                << " with initial value " << from_expr(ns, "", field_pair.second)
+                << " for " << format(address_expr)
+                << " with initial value " << format(field_pair.second)
                 << messaget::eom;
       });
   }
@@ -113,7 +114,7 @@ symbol_exprt goto_symext::add_field(
   symbolt &new_symbol = get_fresh_aux_symbol(
     field_type,
     id2string(state.source.function_id),
-    "SM__" + from_expr(ns, "", expr) + "__" + id2string(field_name),
+    "SM__" + from_expr(expr) + "__" + id2string(field_name),
     state.source.pc->source_location(),
     ID_C,
     state.symbol_table);
@@ -136,8 +137,8 @@ static bool set_field_check_null(
 #ifdef DEBUG_SM
     log.conditional_output(
       log.debug(), [ns, null_pointer, expr](messaget::mstreamt &mstream) {
-        mstream << "Shadow memory: value set match: " << from_expr(ns, "", null_pointer)
-                << " <-- " << from_expr(ns, "", expr) << messaget::eom;
+        mstream << "Shadow memory: value set match: " << format(null_pointer)
+                << " <-- " << format(expr) << messaget::eom;
         mstream << "Shadow memory: ignoring set field on NULL object" << messaget::eom;
       });
 #endif
@@ -158,7 +159,7 @@ static value_set_dereferencet::valuet get_shadow(
   value_set_dereferencet::valuet shadow_dereference =
       value_set_dereferencet::build_reference_to(shadowed_object, expr, ns);
 #ifdef DEBUG_SM
-  log.debug() << "Shadow memory: shadow-deref: " << from_expr(ns, "", shadow_dereference.value) << messaget::eom;
+  log.debug() << "Shadow memory: shadow-deref: " << format(shadow_dereference.value) << messaget::eom;
 #endif
   return shadow_dereference;
 }
@@ -466,23 +467,23 @@ static optionalt<exprt> get_shadow_memory(
     {
       log.warning()
           << "Shadow memory: value set contains unknown for "
-          << from_expr(ns, "", expr)
+          << format(expr)
           << messaget::eom;
       continue;
     }
     if(to_object_descriptor_expr(matched_object).root_object().id() == ID_integer_address)
     {
       log.warning()
           << "Shadow memory: value set contains integer_address for "
-          << from_expr(ns, "", expr)
+          << format(expr)
           << messaget::eom;
       continue;
     }
     if(matched_object.type().get_bool(ID_C_is_failed_symbol))
     {
       log.warning()
           << "Shadow memory: value set contains failed symbol for "
-          << from_expr(ns, "", expr)
+          << format(expr)
           << messaget::eom;
       continue;
     }
@@ -604,10 +605,10 @@ void goto_symext::symex_shadow_memory_copy(
     return;
   }
   log.conditional_output(
-      log.debug(), [this, dest_expr, src_expr](messaget::mstreamt &mstream) {
+      log.debug(), [dest_expr, src_expr](messaget::mstreamt &mstream) {
         mstream << "Shadow memory: copy from "
-                << from_expr(ns, "", src_expr.object())
-                << " to " << from_expr(ns, "", dest_expr.object())
+                << format(src_expr.object())
+                << " to " << format(dest_expr.object())
                 << messaget::eom;
       });
   for(const auto &entry : state.address_fields)
@@ -625,7 +626,7 @@ void goto_symext::symex_shadow_memory_copy(
     {
       log.warning()
           << "Shadow memory: cannot copy shadow memory to "
-          << from_expr(ns, "", dest_expr)
+          << format(dest_expr)
           << messaget::eom;
       continue;
     }
@@ -641,17 +642,17 @@ void goto_symext::symex_shadow_memory_copy(
     {
       log.warning()
           << "Shadow memory: cannot copy shadow memory from "
-          << from_expr(ns, "", src_expr)
+          << format(src_expr)
           << messaget::eom;
       continue;
     }
     if(maybe_lhs->id() == ID_address_of && maybe_rhs->id() == ID_address_of)
     {
       log.warning()
         << "Shadow memory: copied shadow memory from "
-        << from_expr(src_expr)
+        << format(src_expr)
         << " to "
-        << from_expr(dest_expr)
+        << format(dest_expr)
         << messaget::eom;
       symex_assign(
           state,
@@ -662,9 +663,9 @@ void goto_symext::symex_shadow_memory_copy(
     {
       log.warning()
           << "Shadow memory: failed to copy shadow memory from "
-          << from_expr(ns, "", src_expr)
+          << format(src_expr)
           << " to "
-          << from_expr(ns, "", dest_expr)
+          << format(dest_expr)
           << messaget::eom;
     }
   }
@@ -736,7 +737,7 @@ static std::vector<exprt::operandst> get_field(
     {
       std::stringstream s;
       s << "Shadow memory: cannot get shadow memory via type void* for "
-        << from_expr(ns, "", expr)
+        << format(expr)
         << ". Insert a cast to the type that you want to access.";
       throw invalid_input_exceptiont(s.str());
     }
@@ -857,13 +858,13 @@ void goto_symext::symex_set_field(
     log.debug() << "Shadow memory: mux size set_field: " << mux_size << messaget::eom;
     const exprt lhs = deref_expr(*maybe_lhs);
 #ifdef DEBUG_SM
-    log.debug() << "Shadow memory: LHS: " << from_expr(ns, "", lhs) << messaget::eom;
+    log.debug() << "Shadow memory: LHS: " << format(lhs) << messaget::eom;
 #endif
     if(lhs.type().id() == ID_empty)
     {
       std::stringstream s;
       s << "Shadow memory: cannot set shadow memory via type void* for "
-        << from_expr(ns, "", expr)
+        << format(expr)
         << ". Insert a cast to the type that you want to access.";
       throw invalid_input_exceptiont(s.str());
     }
@@ -875,15 +876,15 @@ void goto_symext::symex_set_field(
     CHECK_RETURN(per_byte_rhs.has_value());
 
 #ifdef DEBUG_SM
-    log.debug() << "Shadow memory: RHS: " << from_expr(ns, "", per_byte_rhs) << messaget::eom;
+    log.debug() << "Shadow memory: RHS: " << format(per_byte_rhs.value()) << messaget::eom;
 #endif
     symex_assign(state, lhs, typecast_exprt::conditional_cast(per_byte_rhs.value(), lhs.type()));
   }
   else
   {
     log.warning()
       << "Shadow memory: cannot set_field for "
-      << from_expr(ns, "", expr)
+      << format(expr)
       << messaget::eom;
   }
 }
@@ -932,23 +933,23 @@ void goto_symext::symex_get_field(
     {
       log.warning()
           << "Shadow memory: value set contains unknown for "
-          << from_expr(ns, "", expr)
+          << format(expr)
           << messaget::eom;
       continue;
     }
     if(to_object_descriptor_expr(matched_object).root_object().id() == ID_integer_address)
     {
       log.warning()
           << "Shadow memory: value set contains integer_address for "
-          << from_expr(ns, "", expr)
+          << format(expr)
           << messaget::eom;
       continue;
     }
     if(matched_object.type().get_bool(ID_C_is_failed_symbol))
     {
       log.warning()
           << "Shadow memory: value set contains failed symbol for "
-          << from_expr(ns, "", expr)
+          << format(expr)
           << messaget::eom;
       continue;
     }
@@ -972,7 +973,7 @@ void goto_symext::symex_get_field(
     const size_t mux_size = rhs_conds_values.size() - 1;
     log.debug() << "Shadow memory: mux size get_field: " << mux_size << messaget::eom;
 #ifdef DEBUG_SM
-    log.debug() << "Shadow memory: RHS: " << from_expr(ns, "", rhs) << messaget::eom;
+    log.debug() << "Shadow memory: RHS: " << format(rhs) << messaget::eom;
 #endif
     symex_assign(
       state, lhs, typecast_exprt::conditional_cast(rhs, lhs.type()));
@@ -981,7 +982,7 @@ void goto_symext::symex_get_field(
   {
     log.warning()
       << "Shadow memory: cannot get_field for "
-      << from_expr(ns, "", expr)
+      << format(expr)
       << messaget::eom;
     symex_assign(
         state, lhs, typecast_exprt::conditional_cast(field_init_expr, lhs.type()));

src/goto-symex/symex_shadow_memory_util.cpp

@@ -5,6 +5,7 @@
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/c_types.h>
+#include <util/format_expr.h>
 #include <util/pointer_expr.h>
 #include <util/expr_initializer.h>
 
@@ -19,8 +20,8 @@ void log_exact_match(
     log.debug(),
     [ns, shadowed_address, resolved_expr](messaget::mstreamt &mstream) {
       mstream << "Shadow memory: exact match: "
-              << from_expr(ns, "", shadowed_address.address)
-              << " == " << from_expr(ns, "", resolved_expr) << messaget::eom;
+              << format(shadowed_address.address)
+              << " == " << format(resolved_expr) << messaget::eom;
     });
 #endif
 }
@@ -36,8 +37,8 @@ void log_value_set_match(
     log.debug(),
     [ns, shadowed_address, expr](messaget::mstreamt &mstream) {
       mstream << "Shadow memory: value set match: "
-              << from_expr(ns, "", shadowed_address.address)
-              << " == " << from_expr(ns, "", expr) << messaget::eom;
+              << format(shadowed_address.address)
+              << " == " << format(expr) << messaget::eom;
     });
 #endif
 }
@@ -57,14 +58,14 @@ void log_value_set_match(
     [ns, shadowed_address, expr, dereference, matched_base_address, shadow_dereference](
       messaget::mstreamt &mstream) {
       mstream << "Shadow memory: value set match: " << messaget::eom;
-      mstream << "Shadow memory:   base: " << from_expr(ns, "", shadowed_address.address)
-              << " <-- " << from_expr(ns, "", matched_base_address) << messaget::eom;
-      mstream << "Shadow memory:   cell: " << from_expr(ns, "", dereference.pointer) << " <-- "
-              << from_expr(ns, "", expr) << messaget::eom;
+      mstream << "Shadow memory:   base: " << format(shadowed_address.address)
+              << " <-- " << format(matched_base_address) << messaget::eom;
+      mstream << "Shadow memory:   cell: " << format(dereference.pointer) << " <-- "
+              << format(expr) << messaget::eom;
       mstream << "Shadow memory:   shadow ptr: "
-              << from_expr(ns, "", shadow_dereference.pointer) << messaget::eom;
+              << format(shadow_dereference.pointer) << messaget::eom;
       mstream << "Shadow memory:   shadow val: "
-              << from_expr(ns, "", shadow_dereference.value) << messaget::eom;
+              << format(shadow_dereference.value) << messaget::eom;
     });
 #endif
 }
@@ -78,8 +79,8 @@ void log_value_set_match(
 #ifdef DEBUG_SM
   log.conditional_output(
     log.debug(), [ns, address, expr](messaget::mstreamt &mstream) {
-      mstream << "Shadow memory: value set match: " << from_expr(ns, "", address)
-              << " <-- " << from_expr(ns, "", expr) << messaget::eom;
+      mstream << "Shadow memory: value set match: " << format(address)
+              << " <-- " << format(expr) << messaget::eom;
     });
 #endif
 }
@@ -93,7 +94,7 @@ void log_cond(
 #ifdef DEBUG_SM
   log.conditional_output(
     log.debug(), [ns, cond_text, cond](messaget::mstreamt &mstream) {
-      mstream << "Shadow memory: " << cond_text << ": " << from_expr(ns, "", cond)
+      mstream << "Shadow memory: " << cond_text << ": " << format(cond)
               << messaget::eom;
     });
 #endif
@@ -109,7 +110,7 @@ void log_value_set(
   log.debug(), [ns, value_set](messaget::mstreamt &mstream) {
     for(const auto &e : value_set)
     {
-      mstream << "Shadow memory: value set: " << from_expr(ns, "", e) << messaget::eom;
+      mstream << "Shadow memory: value set: " << format(e) << messaget::eom;
     }
   });
 #endif
@@ -124,7 +125,7 @@ void log_try_shadow_address(
   log.conditional_output(
     log.debug(), [ns, shadowed_address](messaget::mstreamt &mstream) {
       mstream << "Shadow memory: trying shadowed address: "
-              << from_expr(ns, "", shadowed_address.address)
+              << format(shadowed_address.address)
               << messaget::eom;
     });
 #endif
@@ -140,7 +141,7 @@ void log_set_field(
   log.conditional_output(
     log.debug(), [field_name, ns, expr, value](messaget::mstreamt &mstream) {
       mstream << "Shadow memory: set_field: " << id2string(field_name) << " for "
-              << from_expr(ns, "", expr) << " to " << from_expr(ns, "", value)
+              << format(expr) << " to " << format(value)
               << messaget::eom;
     });
 }
@@ -154,7 +155,7 @@ void log_get_field(
   log.conditional_output(
     log.debug(), [ns, field_name, expr](messaget::mstreamt &mstream) {
       mstream << "Shadow memory: get_field: " << id2string(field_name) << " for "
-              << from_expr(ns, "", expr) << messaget::eom;
+              << format(expr) << messaget::eom;
     });
 }
 
@@ -427,7 +428,7 @@ exprt compute_max_over_cells(
     {
       log.warning()
         << "Shadow memory: cannot compute max over variable-size array "
-        << from_expr(ns, "", expr)
+        << format(expr)
         << messaget::eom;
     }
   }
@@ -542,7 +543,7 @@ exprt compute_or_over_cells(
     {
       log.warning()
           << "Shadow memory: cannot compute or over variable-size array "
-          << from_expr(ns, "", expr)
+          << format(expr)
           << messaget::eom;
     }
   }
@@ -580,4 +581,4 @@ void replace_invalid_object_by_null(exprt &expr)
   {
     replace_invalid_object_by_null(*it);
   }
-}
+}