Add shadow memory logging functions

Add a set of functions to shadow_memory_util.{h,cpp} that will be used
for logging purposes by `shadow_memory::symex_get_field` and its
subfunctions.

Author: Enrico Steffinlongo

src/goto-symex/shadow_memory_util.cpp

@@ -11,12 +11,21 @@ Author: Peter Schrammel
 
 #include "shadow_memory_util.h"
 
+#include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
+#include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/format_expr.h>
 #include <util/invariant.h>
+#include <util/namespace.h>
 #include <util/pointer_expr.h>
 #include <util/ssa_expr.h>
 #include <util/std_expr.h>
 
+#include <langapi/language_util.h> // IWYU pragma: keep
+
+// TODO: change DEBUG_SM to DEBUG_SHADOW_MEMORY (it also appears in other files)
+
 irep_idt extract_field_name(const exprt &string_expr)
 {
   if(string_expr.id() == ID_typecast)
@@ -71,3 +80,122 @@ void clean_pointer_expr(exprt &expr, const typet &type)
   }
   POSTCONDITION(expr.type().id() == ID_pointer);
 }
+
+void log_get_field(
+  const namespacet &ns,
+  const messaget &log,
+  const irep_idt &field_name,
+  const exprt &expr)
+{
+  log.conditional_output(
+    log.debug(), [ns, field_name, expr](messaget::mstreamt &mstream) {
+      mstream << "Shadow memory: get_field: " << id2string(field_name)
+              << " for " << format(expr) << messaget::eom;
+    });
+}
+
+void log_value_set(
+  const namespacet &ns,
+  const messaget &log,
+  const std::vector<exprt> &value_set)
+{
+#ifdef DEBUG_SM
+  log.conditional_output(
+    log.debug(), [ns, value_set](messaget::mstreamt &mstream) {
+      for(const auto &e : value_set)
+      {
+        mstream << "Shadow memory: value_set: " << format(e) << messaget::eom;
+      }
+    });
+#endif
+}
+
+void log_value_set_match(
+  const namespacet &ns,
+  const messaget &log,
+  const shadow_memory_statet::shadowed_addresst &shadowed_address,
+  const exprt &matched_base_address,
+  const value_set_dereferencet::valuet &dereference,
+  const exprt &expr,
+  const value_set_dereferencet::valuet &shadow_dereference)
+{
+#ifdef DEBUG_SM
+  log.conditional_output(
+    log.debug(),
+    [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: " << 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: "
+              << format(shadow_dereference.pointer) << messaget::eom;
+      mstream << "Shadow memory:   shadow_val: "
+              << format(shadow_dereference.value) << messaget::eom;
+    });
+#endif
+}
+
+void log_value_set_match(
+  const namespacet &ns,
+  const messaget &log,
+  const exprt &address,
+  const exprt &expr)
+{
+  // Leave guards rename to DEBUG_SHADOW_MEMORY
+#ifdef DEBUG_SM
+  log.conditional_output(
+    log.debug(), [ns, address, expr](messaget::mstreamt &mstream) {
+      mstream << "Shadow memory: value_set_match: " << format(address)
+              << " <-- " << format(expr) << messaget::eom;
+    });
+#endif
+}
+
+void log_try_shadow_address(
+  const namespacet &ns,
+  const messaget &log,
+  const shadow_memory_statet::shadowed_addresst &shadowed_address)
+{
+#ifdef DEBUG_SM
+  log.conditional_output(
+    log.debug(), [ns, shadowed_address](messaget::mstreamt &mstream) {
+      mstream << "Shadow memory: trying shadowed address: "
+              << format(shadowed_address.address) << messaget::eom;
+    });
+#endif
+}
+
+void log_cond(
+  const namespacet &ns,
+  const messaget &log,
+  const char *cond_text,
+  const exprt &cond)
+{
+#ifdef DEBUG_SM
+  log.conditional_output(
+    log.debug(), [ns, cond_text, cond](messaget::mstreamt &mstream) {
+      mstream << "Shadow memory: " << cond_text << ": " << format(cond)
+              << messaget::eom;
+    });
+#endif
+}
+
+static void log_are_types_incompatible(
+  const namespacet &ns,
+  const exprt &expr,
+  const shadow_memory_statet::shadowed_addresst &shadowed_address,
+  const messaget &log)
+{
+#ifdef DEBUG_SM
+  log.debug() << "Shadow memory: incompatible types "
+              << from_type(ns, "", expr.type()) << ", "
+              << from_type(ns, "", shadowed_address.address.type())
+              << messaget::eom;
+#endif
+}

src/goto-symex/shadow_memory_util.h

@@ -13,6 +13,11 @@ Author: Peter Schrammel
 #define CPROVER_GOTO_SYMEX_SHADOW_MEMORY_UTIL_H
 
 #include <util/irep.h>
+#include <util/message.h> // IWYU pragma: keep
+
+#include <pointer-analysis/value_set_dereference.h>
+
+#include "goto_symex_state.h" // IWYU pragma: keep
 
 class exprt;
 class typet;
@@ -32,4 +37,47 @@ irep_idt extract_field_name(const exprt &string_expr);
 /// \param type The followed type of expr.
 void clean_pointer_expr(exprt &expr, const typet &type);
 
-#endif // CPROVER_GOTO_SYMEX_SHADOW_MEMORY_STATE_H
+// TODO: doxygen
+void log_get_field(
+  const namespacet &ns,
+  const messaget &log,
+  const irep_idt &field_name,
+  const exprt &expr);
+
+// TODO: doxygen
+void log_value_set(
+  const namespacet &ns,
+  const messaget &log,
+  const std::vector<exprt> &value_set);
+
+// TODO: doxygen
+void log_value_set_match(
+  const namespacet &ns,
+  const messaget &log,
+  const shadow_memory_statet::shadowed_addresst &shadowed_address,
+  const exprt &matched_base_address,
+  const value_set_dereferencet::valuet &dereference,
+  const exprt &expr,
+  const value_set_dereferencet::valuet &shadow_dereference);
+
+// TODO: doxygen
+void log_value_set_match(
+  const namespacet &ns,
+  const messaget &log,
+  const exprt &address,
+  const exprt &expr);
+
+// TODO: doxygen
+void log_try_shadow_address(
+  const namespacet &ns,
+  const messaget &log,
+  const shadow_memory_statet::shadowed_addresst &shadowed_address);
+
+// TODO: doxygen
+void log_cond(
+  const namespacet &ns,
+  const messaget &log,
+  const char *cond_text,
+  const exprt &cond);
+
+#endif // CPROVER_GOTO_SYMEX_SHADOW_MEMORY_UTIL_H