From f553b83dd527f08f06d0ec4c96162a53cdc2e600 Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Wed, 9 Aug 2023 17:20:38 +0100
Subject: [PATCH 1/5] Add implementation of `symex_set_field`.

---
 src/goto-symex/shadow_memory.cpp      |  86 ++++++++-
 src/goto-symex/shadow_memory_util.cpp | 263 +++++++++++++++++++++++++-
 src/goto-symex/shadow_memory_util.h   |  29 +++
 3 files changed, 376 insertions(+), 2 deletions(-)

diff --git a/src/goto-symex/shadow_memory.cpp b/src/goto-symex/shadow_memory.cpp
index 558ab5c0385..5d12c3bb8bd 100644
--- a/src/goto-symex/shadow_memory.cpp
+++ b/src/goto-symex/shadow_memory.cpp
@@ -90,7 +90,91 @@ void shadow_memoryt::symex_set_field(
   goto_symex_statet &state,
   const exprt::operandst &arguments)
 {
-  // To be implemented
+  // parse set_field call
+  INVARIANT(
+    arguments.size() == 3, CPROVER_PREFIX "set_field requires 3 arguments");
+  irep_idt field_name = extract_field_name(arguments[1]);
+
+  exprt expr = arguments[0];
+  typet expr_type = expr.type();
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    expr_type.id() == ID_pointer,
+    "shadow memory requires a pointer expression",
+    irep_pretty_diagnosticst{expr_type});
+
+  exprt value = arguments[2];
+  log_set_field(ns, log, field_name, expr, value);
+  INVARIANT(
+    state.shadow_memory.address_fields.count(field_name) == 1,
+    id2string(field_name) + " should exist");
+  const auto &addresses = state.shadow_memory.address_fields.at(field_name);
+
+  // get value set
+  replace_invalid_object_by_null(expr);
+#ifdef DEBUG_SM
+  log_set_field(ns, log, field_name, expr, value);
+#endif
+  std::vector<exprt> value_set = state.value_set.get_value_set(expr, ns);
+  log_value_set(ns, log, value_set);
+  if(set_field_check_null(ns, log, value_set, expr))
+  {
+    log.warning() << "Shadow memory: cannot set shadow memory of NULL"
+                  << messaget::eom;
+    return;
+  }
+
+  // build lhs
+  const exprt &rhs = value;
+  size_t mux_size = 0;
+  optionalt<exprt> maybe_lhs =
+    get_shadow_memory(expr, value_set, addresses, ns, log, mux_size);
+
+  // add to equation
+  if(maybe_lhs.has_value())
+  {
+    if(mux_size >= 10)
+    {
+      log.warning() << "Shadow memory: mux size set_field: " << mux_size
+                    << messaget::eom;
+    }
+    else
+    {
+      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: " << 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 "
+        << format(expr)
+        << ". Insert a cast to the type that you want to access.";
+      throw invalid_input_exceptiont(s.str());
+    }
+    // We replicate the rhs value on each byte of the value that we set.
+    // This allows the get_field or/max semantics to operate correctly
+    // on unions.
+    const auto per_byte_rhs =
+      expr_initializer(lhs.type(), expr.source_location(), ns, rhs);
+    CHECK_RETURN(per_byte_rhs.has_value());
+
+#ifdef DEBUG_SM
+    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 " << format(expr)
+                  << messaget::eom;
+  }
 }
 
 // Function synopsis
diff --git a/src/goto-symex/shadow_memory_util.cpp b/src/goto-symex/shadow_memory_util.cpp
index 5115b20141e..a00f212813c 100644
--- a/src/goto-symex/shadow_memory_util.cpp
+++ b/src/goto-symex/shadow_memory_util.cpp
@@ -18,7 +18,7 @@ Author: Peter Schrammel
 #include <util/format_expr.h>
 #include <util/invariant.h>
 #include <util/namespace.h>
-#include <util/pointer_expr.h>
+#include <util/pointer_offset_size.h>
 #include <util/ssa_expr.h>
 #include <util/std_expr.h>
 
@@ -54,6 +54,16 @@ static void remove_array_type_l2(typet &type)
   size.remove_level_2();
 }
 
+exprt deref_expr(const exprt &expr)
+{
+  if(expr.id() == ID_address_of)
+  {
+    return to_address_of_expr(expr).object();
+  }
+
+  return dereference_exprt(expr);
+}
+
 void clean_pointer_expr(exprt &expr, const typet &type)
 {
   if(
@@ -81,6 +91,21 @@ void clean_pointer_expr(exprt &expr, const typet &type)
   POSTCONDITION(expr.type().id() == ID_pointer);
 }
 
+void log_set_field(
+  const namespacet &ns,
+  const messaget &log,
+  const irep_idt &field_name,
+  const exprt &expr,
+  const exprt &value)
+{
+  log.conditional_output(
+    log.debug(), [field_name, ns, expr, value](messaget::mstreamt &mstream) {
+      mstream << "Shadow memory: set_field: " << id2string(field_name)
+              << " for " << format(expr) << " to " << format(value)
+              << messaget::eom;
+    });
+}
+
 void log_get_field(
   const namespacet &ns,
   const messaget &log,
@@ -828,3 +853,239 @@ std::vector<std::pair<exprt, exprt>> get_shadow_dereference_candidates(
   }
   return result;
 }
+
+// TODO: doxygen?
+// Unfortunately.
+static object_descriptor_exprt
+normalize(const object_descriptor_exprt &expr, const namespacet &ns)
+{
+  if(expr.object().id() == ID_symbol)
+  {
+    return expr;
+  }
+  if(expr.offset().id() == ID_unknown)
+  {
+    return expr;
+  }
+
+  object_descriptor_exprt result = expr;
+  mp_integer offset =
+    numeric_cast_v<mp_integer>(to_constant_expr(expr.offset()));
+  exprt object = expr.object();
+
+  while(true)
+  {
+    if(object.id() == ID_index)
+    {
+      const index_exprt &index_expr = to_index_expr(object);
+      mp_integer index =
+        numeric_cast_v<mp_integer>(to_constant_expr(index_expr.index()));
+
+      offset += *pointer_offset_size(index_expr.type(), ns) * index;
+      object = index_expr.array();
+    }
+    else if(object.id() == ID_member)
+    {
+      const member_exprt &member_expr = to_member_expr(object);
+      const struct_typet &struct_type =
+        to_struct_type(ns.follow(member_expr.struct_op().type()));
+      offset +=
+        *member_offset(struct_type, member_expr.get_component_name(), ns);
+      object = member_expr.struct_op();
+    }
+    else
+    {
+      break;
+    }
+  }
+  result.object() = object;
+  result.offset() = from_integer(offset, expr.offset().type());
+  return result;
+}
+
+bool set_field_check_null(
+  const namespacet &ns,
+  const messaget &log,
+  const std::vector<exprt> &value_set,
+  const exprt &expr)
+{
+  const null_pointer_exprt null_pointer(to_pointer_type(expr.type()));
+  if(value_set.size() == 1 && contains_null_or_invalid(value_set, null_pointer))
+  {
+    // TODO: duplicated in log_value_set_match
+#ifdef DEBUG_SM
+    log.conditional_output(
+      log.debug(), [ns, null_pointer, expr](messaget::mstreamt &mstream) {
+        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
+    return true;
+  }
+  return false;
+}
+
+/// Used for set_field and shadow memory copy
+static std::vector<std::pair<exprt, exprt>>
+get_shadow_memory_for_matched_object(
+  const exprt &expr,
+  const exprt &matched_object,
+  const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
+  const namespacet &ns,
+  const messaget &log,
+  bool &exact_match)
+{
+  std::vector<std::pair<exprt, exprt>> result;
+  for(const auto &shadowed_address : addresses)
+  {
+    log_try_shadow_address(ns, log, shadowed_address);
+
+    if(!are_types_compatible(expr.type(), shadowed_address.address.type()))
+    {
+#ifdef DEBUG_SM
+      log.debug() << "Shadow memory: incompatible types "
+                  << from_type(ns, "", expr.type()) << ", "
+                  << from_type(ns, "", shadowed_address.address.type())
+                  << messaget::eom;
+#endif
+      continue;
+    }
+
+    object_descriptor_exprt matched_base_descriptor =
+      normalize(to_object_descriptor_expr(matched_object), ns);
+
+    value_set_dereferencet::valuet dereference =
+      value_set_dereferencet::build_reference_to(
+        matched_base_descriptor, expr, ns);
+
+    exprt matched_base_address =
+      address_of_exprt(matched_base_descriptor.object());
+    clean_string_constant(to_address_of_expr(matched_base_address).op());
+
+    // NULL has already been handled in the caller; skip.
+    if(matched_base_descriptor.object().id() == ID_null_object)
+    {
+      continue;
+    }
+    const value_set_dereferencet::valuet shadow_dereference =
+      get_shadow_dereference(
+        shadowed_address.shadow, matched_base_descriptor, expr, ns, log);
+    log_value_set_match(
+      ns,
+      log,
+      shadowed_address,
+      matched_base_address,
+      dereference,
+      expr,
+      shadow_dereference);
+
+    const exprt base_cond = get_matched_base_cond(
+      shadowed_address.address, matched_base_address, ns, log);
+    log_cond(ns, log, "base_cond", base_cond);
+    if(base_cond.is_false())
+    {
+      continue;
+    }
+
+    const exprt expr_cond =
+      get_matched_expr_cond(dereference.pointer, expr, ns, log);
+    if(expr_cond.is_false())
+    {
+      continue;
+    }
+
+    if(base_cond.is_true() && expr_cond.is_true())
+    {
+#ifdef DEBUG_SM
+      log.debug() << "exact match" << messaget::eom;
+#endif
+      exact_match = true;
+      result.clear();
+      result.push_back({base_cond, shadow_dereference.pointer});
+      break;
+    }
+
+    if(base_cond.is_true())
+    {
+      // No point looking at further shadow addresses
+      // as only one of them can match.
+#ifdef DEBUG_SM
+      log.debug() << "base match" << messaget::eom;
+#endif
+      result.clear();
+      result.emplace_back(expr_cond, shadow_dereference.pointer);
+      break;
+    }
+    else
+    {
+#ifdef DEBUG_SM
+      log.debug() << "conditional match" << messaget::eom;
+#endif
+      result.emplace_back(
+        and_exprt(base_cond, expr_cond), shadow_dereference.pointer);
+    }
+  }
+  return result;
+}
+
+optionalt<exprt> get_shadow_memory(
+  const exprt &expr,
+  const std::vector<exprt> &value_set,
+  const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
+  const namespacet &ns,
+  const messaget &log,
+  size_t &mux_size)
+{
+  std::vector<std::pair<exprt, exprt>> conds_values;
+  for(const auto &matched_object : value_set)
+  {
+    if(matched_object.id() != ID_object_descriptor)
+    {
+      log.warning() << "Shadow memory: value set contains unknown for "
+                    << 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 "
+                    << 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 "
+                    << format(expr) << messaget::eom;
+      continue;
+    }
+
+    bool exact_match = false;
+    auto per_value_set_conds_values = get_shadow_memory_for_matched_object(
+      expr, matched_object, addresses, ns, log, exact_match);
+
+    if(!per_value_set_conds_values.empty())
+    {
+      if(exact_match)
+      {
+        conds_values.clear();
+      }
+      conds_values.insert(
+        conds_values.begin(),
+        per_value_set_conds_values.begin(),
+        per_value_set_conds_values.end());
+      mux_size += conds_values.size() - 1;
+      if(exact_match)
+      {
+        break;
+      }
+    }
+  }
+  if(!conds_values.empty())
+  {
+    return build_if_else_expr(conds_values);
+  }
+  return {};
+}
diff --git a/src/goto-symex/shadow_memory_util.h b/src/goto-symex/shadow_memory_util.h
index dab899332c7..546ac65bd5e 100644
--- a/src/goto-symex/shadow_memory_util.h
+++ b/src/goto-symex/shadow_memory_util.h
@@ -37,6 +37,17 @@ 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);
 
+// TODO: Daxygen
+exprt deref_expr(const exprt &expr);
+
+// TODO: DOxYGEN
+void log_set_field(
+  const namespacet &ns,
+  const messaget &log,
+  const irep_idt &field_name,
+  const exprt &expr,
+  const exprt &value);
+
 // TODO: doxygen
 void log_get_field(
   const namespacet &ns,
@@ -123,4 +134,22 @@ exprt compute_max_over_cells(
 exprt build_if_else_expr(
   const std::vector<std::pair<exprt, exprt>> &conds_values);
 
+// TODO: improve?
+/// returns true if we attempt to set/get a field on a NULL pointer
+bool set_field_check_null(
+  const namespacet &ns,
+  const messaget &log,
+  const std::vector<exprt> &value_set,
+  const exprt &expr);
+
+// TODO: improve?
+/// Used for set_field and shadow memory copy
+optionalt<exprt> get_shadow_memory(
+  const exprt &expr,
+  const std::vector<exprt> &value_set,
+  const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
+  const namespacet &ns,
+  const messaget &log,
+  size_t &mux_size);
+
 #endif // CPROVER_GOTO_SYMEX_SHADOW_MEMORY_UTIL_H

From 61262eb224d74fc6f752164e3293574360251934 Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Wed, 9 Aug 2023 17:21:37 +0100
Subject: [PATCH 2/5] Enable all shadow memory regression tests

---
 regression/cbmc-shadow-memory/char1/test.desc                   | 2 +-
 regression/cbmc-shadow-memory/constchar-param1/test.desc        | 2 +-
 regression/cbmc-shadow-memory/constchar-pointers1/test.desc     | 2 +-
 regression/cbmc-shadow-memory/errno1/test.desc                  | 2 +-
 regression/cbmc-shadow-memory/float1/test.desc                  | 2 +-
 regression/cbmc-shadow-memory/getenv1/test.desc                 | 2 +-
 regression/cbmc-shadow-memory/global1/test.desc                 | 2 +-
 regression/cbmc-shadow-memory/linked-list1/test.desc            | 2 +-
 regression/cbmc-shadow-memory/linked-list2/test.desc            | 2 +-
 regression/cbmc-shadow-memory/local1/test.desc                  | 2 +-
 regression/cbmc-shadow-memory/malloc1/test.desc                 | 2 +-
 regression/cbmc-shadow-memory/maybe-null1/test.desc             | 2 +-
 regression/cbmc-shadow-memory/memcpy1/test.desc                 | 2 +-
 .../cbmc-shadow-memory/nondet-pointer-into-struct1/test.desc    | 2 +-
 regression/cbmc-shadow-memory/nondet-size-arrays1/test.desc     | 2 +-
 regression/cbmc-shadow-memory/param1/test.desc                  | 2 +-
 regression/cbmc-shadow-memory/static1/test.desc                 | 2 +-
 regression/cbmc-shadow-memory/strdup1/test.desc                 | 2 +-
 regression/cbmc-shadow-memory/struct-get-max1/test.desc         | 2 +-
 regression/cbmc-shadow-memory/struct-get-or1/test.desc          | 2 +-
 regression/cbmc-shadow-memory/struct-set1/test.desc             | 2 +-
 regression/cbmc-shadow-memory/taint-example1/test.desc          | 2 +-
 regression/cbmc-shadow-memory/trace1/test.desc                  | 2 +-
 regression/cbmc-shadow-memory/union-get-max1/test.desc          | 2 +-
 regression/cbmc-shadow-memory/union-get-or1/test.desc           | 2 +-
 regression/cbmc-shadow-memory/union-set1/test.desc              | 2 +-
 regression/cbmc-shadow-memory/var-assign1/test.desc             | 2 +-
 regression/cbmc-shadow-memory/void-ptr-param-set1/test.desc     | 2 +-
 regression/cbmc-shadow-memory/void-ptr-param2/test.desc         | 2 +-
 29 files changed, 29 insertions(+), 29 deletions(-)

diff --git a/regression/cbmc-shadow-memory/char1/test.desc b/regression/cbmc-shadow-memory/char1/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/char1/test.desc
+++ b/regression/cbmc-shadow-memory/char1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/constchar-param1/test.desc b/regression/cbmc-shadow-memory/constchar-param1/test.desc
index 482449453e2..2e20debe101 100644
--- a/regression/cbmc-shadow-memory/constchar-param1/test.desc
+++ b/regression/cbmc-shadow-memory/constchar-param1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 --unwind 11
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/constchar-pointers1/test.desc b/regression/cbmc-shadow-memory/constchar-pointers1/test.desc
index f3ae1d03751..e21095fda9d 100644
--- a/regression/cbmc-shadow-memory/constchar-pointers1/test.desc
+++ b/regression/cbmc-shadow-memory/constchar-pointers1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 --unwind 11
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/errno1/test.desc b/regression/cbmc-shadow-memory/errno1/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/errno1/test.desc
+++ b/regression/cbmc-shadow-memory/errno1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/float1/test.desc b/regression/cbmc-shadow-memory/float1/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/float1/test.desc
+++ b/regression/cbmc-shadow-memory/float1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/getenv1/test.desc b/regression/cbmc-shadow-memory/getenv1/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/getenv1/test.desc
+++ b/regression/cbmc-shadow-memory/getenv1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/global1/test.desc b/regression/cbmc-shadow-memory/global1/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/global1/test.desc
+++ b/regression/cbmc-shadow-memory/global1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/linked-list1/test.desc b/regression/cbmc-shadow-memory/linked-list1/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/linked-list1/test.desc
+++ b/regression/cbmc-shadow-memory/linked-list1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/linked-list2/test.desc b/regression/cbmc-shadow-memory/linked-list2/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/linked-list2/test.desc
+++ b/regression/cbmc-shadow-memory/linked-list2/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/local1/test.desc b/regression/cbmc-shadow-memory/local1/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/local1/test.desc
+++ b/regression/cbmc-shadow-memory/local1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/malloc1/test.desc b/regression/cbmc-shadow-memory/malloc1/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/malloc1/test.desc
+++ b/regression/cbmc-shadow-memory/malloc1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/maybe-null1/test.desc b/regression/cbmc-shadow-memory/maybe-null1/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/maybe-null1/test.desc
+++ b/regression/cbmc-shadow-memory/maybe-null1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/memcpy1/test.desc b/regression/cbmc-shadow-memory/memcpy1/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/memcpy1/test.desc
+++ b/regression/cbmc-shadow-memory/memcpy1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/nondet-pointer-into-struct1/test.desc b/regression/cbmc-shadow-memory/nondet-pointer-into-struct1/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/nondet-pointer-into-struct1/test.desc
+++ b/regression/cbmc-shadow-memory/nondet-pointer-into-struct1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/nondet-size-arrays1/test.desc b/regression/cbmc-shadow-memory/nondet-size-arrays1/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/nondet-size-arrays1/test.desc
+++ b/regression/cbmc-shadow-memory/nondet-size-arrays1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/param1/test.desc b/regression/cbmc-shadow-memory/param1/test.desc
index 3ab59a8d649..a4f81a33666 100644
--- a/regression/cbmc-shadow-memory/param1/test.desc
+++ b/regression/cbmc-shadow-memory/param1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/static1/test.desc b/regression/cbmc-shadow-memory/static1/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/static1/test.desc
+++ b/regression/cbmc-shadow-memory/static1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/strdup1/test.desc b/regression/cbmc-shadow-memory/strdup1/test.desc
index 438d68ba0b0..831280dc5ef 100644
--- a/regression/cbmc-shadow-memory/strdup1/test.desc
+++ b/regression/cbmc-shadow-memory/strdup1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 --unwind 4
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/struct-get-max1/test.desc b/regression/cbmc-shadow-memory/struct-get-max1/test.desc
index 29c4483cdfb..67cb3bf2767 100644
--- a/regression/cbmc-shadow-memory/struct-get-max1/test.desc
+++ b/regression/cbmc-shadow-memory/struct-get-max1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/struct-get-or1/test.desc b/regression/cbmc-shadow-memory/struct-get-or1/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/struct-get-or1/test.desc
+++ b/regression/cbmc-shadow-memory/struct-get-or1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/struct-set1/test.desc b/regression/cbmc-shadow-memory/struct-set1/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/struct-set1/test.desc
+++ b/regression/cbmc-shadow-memory/struct-set1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/taint-example1/test.desc b/regression/cbmc-shadow-memory/taint-example1/test.desc
index cb611a28bb6..dc9fb11329e 100644
--- a/regression/cbmc-shadow-memory/taint-example1/test.desc
+++ b/regression/cbmc-shadow-memory/taint-example1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 --unwind 15
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/trace1/test.desc b/regression/cbmc-shadow-memory/trace1/test.desc
index d717cd26938..9175c81af34 100644
--- a/regression/cbmc-shadow-memory/trace1/test.desc
+++ b/regression/cbmc-shadow-memory/trace1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 --stop-on-fail --unwind 5
 ^EXIT=10$
diff --git a/regression/cbmc-shadow-memory/union-get-max1/test.desc b/regression/cbmc-shadow-memory/union-get-max1/test.desc
index a7f9f044e8e..49bbf7d5ebc 100644
--- a/regression/cbmc-shadow-memory/union-get-max1/test.desc
+++ b/regression/cbmc-shadow-memory/union-get-max1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/union-get-or1/test.desc b/regression/cbmc-shadow-memory/union-get-or1/test.desc
index 20cb1b9a001..9b5611604ee 100644
--- a/regression/cbmc-shadow-memory/union-get-or1/test.desc
+++ b/regression/cbmc-shadow-memory/union-get-or1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/union-set1/test.desc b/regression/cbmc-shadow-memory/union-set1/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/union-set1/test.desc
+++ b/regression/cbmc-shadow-memory/union-set1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/var-assign1/test.desc b/regression/cbmc-shadow-memory/var-assign1/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/var-assign1/test.desc
+++ b/regression/cbmc-shadow-memory/var-assign1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/void-ptr-param-set1/test.desc b/regression/cbmc-shadow-memory/void-ptr-param-set1/test.desc
index bde0b0f48e5..c20d63ac953 100644
--- a/regression/cbmc-shadow-memory/void-ptr-param-set1/test.desc
+++ b/regression/cbmc-shadow-memory/void-ptr-param-set1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=6$
diff --git a/regression/cbmc-shadow-memory/void-ptr-param2/test.desc b/regression/cbmc-shadow-memory/void-ptr-param2/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc-shadow-memory/void-ptr-param2/test.desc
+++ b/regression/cbmc-shadow-memory/void-ptr-param2/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$

From c6999d167ecd4b6d9b708206439a05c1a99d6fc2 Mon Sep 17 00:00:00 2001
From: Enrico Steffinlongo <enrico.steffinlongo@diffblue.com>
Date: Thu, 10 Aug 2023 15:21:19 +0100
Subject: [PATCH 3/5] Fix issue with set and non-bit-sized value

---
 src/goto-symex/shadow_memory.cpp      | 9 ++++++++-
 src/goto-symex/shadow_memory_util.cpp | 7 +++++++
 src/goto-symex/shadow_memory_util.h   | 4 ++++
 3 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/goto-symex/shadow_memory.cpp b/src/goto-symex/shadow_memory.cpp
index 5d12c3bb8bd..0be0410edfd 100644
--- a/src/goto-symex/shadow_memory.cpp
+++ b/src/goto-symex/shadow_memory.cpp
@@ -154,11 +154,18 @@ void shadow_memoryt::symex_set_field(
         << ". Insert a cast to the type that you want to access.";
       throw invalid_input_exceptiont(s.str());
     }
+
+    // Get the type of the shadow memory for this field
+    const typet &sm_field_type = get_field_init_type(field_name, state);
+    // Add a conditional cast to the shadow memory field type if `rhs` is not of
+    // the expected type
+    const exprt casted_rhs =
+      typecast_exprt::conditional_cast(rhs, sm_field_type);
     // We replicate the rhs value on each byte of the value that we set.
     // This allows the get_field or/max semantics to operate correctly
     // on unions.
     const auto per_byte_rhs =
-      expr_initializer(lhs.type(), expr.source_location(), ns, rhs);
+      expr_initializer(lhs.type(), expr.source_location(), ns, casted_rhs);
     CHECK_RETURN(per_byte_rhs.has_value());
 
 #ifdef DEBUG_SM
diff --git a/src/goto-symex/shadow_memory_util.cpp b/src/goto-symex/shadow_memory_util.cpp
index a00f212813c..a7ee7502652 100644
--- a/src/goto-symex/shadow_memory_util.cpp
+++ b/src/goto-symex/shadow_memory_util.cpp
@@ -256,6 +256,13 @@ get_field_init_expr(const irep_idt &field_name, const goto_symex_statet &state)
   return field_type_it->second;
 }
 
+const typet &
+get_field_init_type(const irep_idt &field_name, const goto_symex_statet &state)
+{
+  const exprt &field_init_expr = get_field_init_expr(field_name, state);
+  return field_init_expr.type();
+}
+
 /// Given a pointer expression `address` checks if any expr in value_set is
 /// compatible
 bool contains_null_or_invalid(
diff --git a/src/goto-symex/shadow_memory_util.h b/src/goto-symex/shadow_memory_util.h
index 546ac65bd5e..f2bd5db1a60 100644
--- a/src/goto-symex/shadow_memory_util.h
+++ b/src/goto-symex/shadow_memory_util.h
@@ -109,6 +109,10 @@ std::vector<std::pair<exprt, exprt>> get_shadow_dereference_candidates(
   const typet &lhs_type,
   bool &exact_match);
 
+// TODO: doxygen
+const typet &
+get_field_init_type(const irep_idt &field_name, const goto_symex_statet &state);
+
 // TODO: doxygen
 bool contains_null_or_invalid(
   const std::vector<exprt> &value_set,

From e86e34a18ea045b58e75b01adba35aa7ab07f349 Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Tue, 22 Aug 2023 11:14:33 +0100
Subject: [PATCH 4/5] Add extra regression test for `set_field`.

---
 .../cbmc-shadow-memory/struct-set2/main.c     | 56 +++++++++++++++++++
 .../cbmc-shadow-memory/struct-set2/test.desc  |  8 +++
 2 files changed, 64 insertions(+)
 create mode 100644 regression/cbmc-shadow-memory/struct-set2/main.c
 create mode 100644 regression/cbmc-shadow-memory/struct-set2/test.desc

diff --git a/regression/cbmc-shadow-memory/struct-set2/main.c b/regression/cbmc-shadow-memory/struct-set2/main.c
new file mode 100644
index 00000000000..07a67b5ecef
--- /dev/null
+++ b/regression/cbmc-shadow-memory/struct-set2/main.c
@@ -0,0 +1,56 @@
+#include <assert.h>
+
+struct S
+{
+  short x[3];
+  char c;
+};
+
+int main(void)
+{
+  __CPROVER_field_decl_local("f", (char)0);
+
+  struct S s;
+
+  // Setting the struct recursively set all its fields
+  __CPROVER_set_field(&s, "f", 1);
+
+  assert(__CPROVER_get_field(&s.x[0], "f") == 1);
+  assert(__CPROVER_get_field(&s.x[1], "f") == 1);
+  assert(__CPROVER_get_field(&s.x[2], "f") == 1);
+  assert(__CPROVER_get_field(&s.c, "f") == 1);
+  assert(__CPROVER_get_field(&s, "f") == 1);
+
+  // Setting the struct recursively set all its fields
+  __CPROVER_set_field(&s, "f", 0);
+
+  assert(__CPROVER_get_field(&s.x[0], "f") == 0);
+  assert(__CPROVER_get_field(&s.x[1], "f") == 0);
+  assert(__CPROVER_get_field(&s.x[2], "f") == 0);
+  assert(__CPROVER_get_field(&s.c, "f") == 0);
+  assert(__CPROVER_get_field(&s, "f") == 0);
+
+  // Setting a field of the struct changes its values ad after aggregation the whole struct value
+  __CPROVER_set_field(&s.x[1], "f", 2);
+
+  assert(__CPROVER_get_field(&s.x[0], "f") == 0);
+  assert(__CPROVER_get_field(&s.x[1], "f") == 2);
+  assert(__CPROVER_get_field(&s.x[2], "f") == 0);
+  assert(__CPROVER_get_field(&s.c, "f") == 0);
+  assert(__CPROVER_get_field(&s, "f") == 2);
+
+  // Rest shadow memory
+  __CPROVER_set_field(&s, "f", 0);
+
+  // Changing ONLY first cell of S array at field x by using offset with pointer arithmetics
+  short *p = ((short *)&s) + 1;
+  __CPROVER_set_field(p, "f", 3);
+
+  assert(__CPROVER_get_field(&s.x[0], "f") == 0);
+  assert(__CPROVER_get_field(&s.x[1], "f") == 3);
+  assert(__CPROVER_get_field(&s.x[2], "f") == 0);
+  assert(__CPROVER_get_field(&s.c, "f") == 0);
+  assert(__CPROVER_get_field(&s, "f") == 3);
+
+  return 0;
+}
\ No newline at end of file
diff --git a/regression/cbmc-shadow-memory/struct-set2/test.desc b/regression/cbmc-shadow-memory/struct-set2/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc-shadow-memory/struct-set2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

From a3964fe0f77a9d847fc70b1a0914d5d26d1833a9 Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Tue, 22 Aug 2023 11:21:02 +0100
Subject: [PATCH 5/5] Mark regression tests failing as `KNOWNBUG` (they are
 going to be fixed and reactivated as part of another PR).

---
 regression/cbmc-shadow-memory/char1/test.desc               | 2 +-
 regression/cbmc-shadow-memory/constchar-param1/test.desc    | 2 +-
 regression/cbmc-shadow-memory/constchar-pointers1/test.desc | 2 +-
 regression/cbmc-shadow-memory/float1/test.desc              | 2 +-
 regression/cbmc-shadow-memory/getenv1/test.desc             | 2 +-
 regression/cbmc-shadow-memory/global1/test.desc             | 2 +-
 regression/cbmc-shadow-memory/linked-list1/test.desc        | 2 +-
 regression/cbmc-shadow-memory/linked-list2/test.desc        | 2 +-
 regression/cbmc-shadow-memory/local1/test.desc              | 2 +-
 regression/cbmc-shadow-memory/maybe-null1/test.desc         | 2 +-
 regression/cbmc-shadow-memory/nondet-size-arrays1/test.desc | 2 +-
 regression/cbmc-shadow-memory/param1/test.desc              | 2 +-
 regression/cbmc-shadow-memory/struct-set1/test.desc         | 2 +-
 regression/cbmc-shadow-memory/taint-example1/test.desc      | 2 +-
 regression/cbmc-shadow-memory/trace1/test.desc              | 2 +-
 regression/cbmc-shadow-memory/union-get-max1/test.desc      | 2 +-
 regression/cbmc-shadow-memory/union-get-or1/test.desc       | 2 +-
 regression/cbmc-shadow-memory/union-set1/test.desc          | 2 +-
 regression/cbmc-shadow-memory/var-assign1/test.desc         | 2 +-
 19 files changed, 19 insertions(+), 19 deletions(-)

diff --git a/regression/cbmc-shadow-memory/char1/test.desc b/regression/cbmc-shadow-memory/char1/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc-shadow-memory/char1/test.desc
+++ b/regression/cbmc-shadow-memory/char1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/constchar-param1/test.desc b/regression/cbmc-shadow-memory/constchar-param1/test.desc
index 2e20debe101..c2fd69bd289 100644
--- a/regression/cbmc-shadow-memory/constchar-param1/test.desc
+++ b/regression/cbmc-shadow-memory/constchar-param1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --unwind 11
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/constchar-pointers1/test.desc b/regression/cbmc-shadow-memory/constchar-pointers1/test.desc
index e21095fda9d..dbd7c3b8a09 100644
--- a/regression/cbmc-shadow-memory/constchar-pointers1/test.desc
+++ b/regression/cbmc-shadow-memory/constchar-pointers1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --unwind 11
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/float1/test.desc b/regression/cbmc-shadow-memory/float1/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc-shadow-memory/float1/test.desc
+++ b/regression/cbmc-shadow-memory/float1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/getenv1/test.desc b/regression/cbmc-shadow-memory/getenv1/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc-shadow-memory/getenv1/test.desc
+++ b/regression/cbmc-shadow-memory/getenv1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/global1/test.desc b/regression/cbmc-shadow-memory/global1/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc-shadow-memory/global1/test.desc
+++ b/regression/cbmc-shadow-memory/global1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/linked-list1/test.desc b/regression/cbmc-shadow-memory/linked-list1/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc-shadow-memory/linked-list1/test.desc
+++ b/regression/cbmc-shadow-memory/linked-list1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/linked-list2/test.desc b/regression/cbmc-shadow-memory/linked-list2/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc-shadow-memory/linked-list2/test.desc
+++ b/regression/cbmc-shadow-memory/linked-list2/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/local1/test.desc b/regression/cbmc-shadow-memory/local1/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc-shadow-memory/local1/test.desc
+++ b/regression/cbmc-shadow-memory/local1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/maybe-null1/test.desc b/regression/cbmc-shadow-memory/maybe-null1/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc-shadow-memory/maybe-null1/test.desc
+++ b/regression/cbmc-shadow-memory/maybe-null1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/nondet-size-arrays1/test.desc b/regression/cbmc-shadow-memory/nondet-size-arrays1/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc-shadow-memory/nondet-size-arrays1/test.desc
+++ b/regression/cbmc-shadow-memory/nondet-size-arrays1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/param1/test.desc b/regression/cbmc-shadow-memory/param1/test.desc
index a4f81a33666..c8c38b7af5e 100644
--- a/regression/cbmc-shadow-memory/param1/test.desc
+++ b/regression/cbmc-shadow-memory/param1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/struct-set1/test.desc b/regression/cbmc-shadow-memory/struct-set1/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc-shadow-memory/struct-set1/test.desc
+++ b/regression/cbmc-shadow-memory/struct-set1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/taint-example1/test.desc b/regression/cbmc-shadow-memory/taint-example1/test.desc
index dc9fb11329e..b35013bafd6 100644
--- a/regression/cbmc-shadow-memory/taint-example1/test.desc
+++ b/regression/cbmc-shadow-memory/taint-example1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --unwind 15
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/trace1/test.desc b/regression/cbmc-shadow-memory/trace1/test.desc
index 9175c81af34..6cb8815a7e6 100644
--- a/regression/cbmc-shadow-memory/trace1/test.desc
+++ b/regression/cbmc-shadow-memory/trace1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --stop-on-fail --unwind 5
 ^EXIT=10$
diff --git a/regression/cbmc-shadow-memory/union-get-max1/test.desc b/regression/cbmc-shadow-memory/union-get-max1/test.desc
index 49bbf7d5ebc..dbb3109cc02 100644
--- a/regression/cbmc-shadow-memory/union-get-max1/test.desc
+++ b/regression/cbmc-shadow-memory/union-get-max1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/union-get-or1/test.desc b/regression/cbmc-shadow-memory/union-get-or1/test.desc
index 9b5611604ee..dcb960a7ae2 100644
--- a/regression/cbmc-shadow-memory/union-get-or1/test.desc
+++ b/regression/cbmc-shadow-memory/union-get-or1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/union-set1/test.desc b/regression/cbmc-shadow-memory/union-set1/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc-shadow-memory/union-set1/test.desc
+++ b/regression/cbmc-shadow-memory/union-set1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/var-assign1/test.desc b/regression/cbmc-shadow-memory/var-assign1/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc-shadow-memory/var-assign1/test.desc
+++ b/regression/cbmc-shadow-memory/var-assign1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$