Merge pull request #7846 from esteffin/esteffin/shadow-memory-set-field-op

NlightNFotis · web-flow · commit 79186c402ac4 · 2023-08-22T20:01:34.000+01:00
Add shadow memory set_field operation
diff --git a/regression/cbmc-shadow-memory/char1/test.desc b/regression/cbmc-shadow-memory/char1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+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
@@ -1,4 +1,4 @@
-FUTURE
+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
@@ -1,4 +1,4 @@
-FUTURE
+KNOWNBUG
 main.c
 --unwind 11
 ^EXIT=0$
diff --git 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
@@ -1,4 +1,4 @@
-FUTURE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/getenv1/test.desc b/regression/cbmc-shadow-memory/getenv1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/global1/test.desc b/regression/cbmc-shadow-memory/global1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+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
@@ -1,4 +1,4 @@
-FUTURE
+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
@@ -1,4 +1,4 @@
-FUTURE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/local1/test.desc b/regression/cbmc-shadow-memory/local1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git 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
@@ -1,4 +1,4 @@
-FUTURE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git 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
@@ -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
@@ -1,4 +1,4 @@
-FUTURE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/param1/test.desc b/regression/cbmc-shadow-memory/param1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -1,4 +1,4 @@
-FUTURE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/struct-set2/main.c 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;
+}
diff --git a/regression/cbmc-shadow-memory/struct-set2/test.desc b/regression/cbmc-shadow-memory/struct-set2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/taint-example1/test.desc b/regression/cbmc-shadow-memory/taint-example1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+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
@@ -1,4 +1,4 @@
-FUTURE
+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
@@ -1,4 +1,4 @@
-FUTURE
+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
@@ -1,4 +1,4 @@
-FUTURE
+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
@@ -1,4 +1,4 @@
-FUTURE
+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
@@ -1,4 +1,4 @@
-FUTURE
+KNOWNBUG
 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
@@ -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
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/src/goto-symex/shadow_memory.cpp b/src/goto-symex/shadow_memory.cpp
@@ -90,7 +90,98 @@ 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());
+    }
+
+    // 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, casted_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
diff --git a/src/goto-symex/shadow_memory_util.h b/src/goto-symex/shadow_memory_util.h

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-FUTURE`
	`1`	`+KNOWNBUG`
`2`	`2`	`main.c`
`3`	`3`
`4`	`4`	`^EXIT=0$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-FUTURE`
	`1`	`+CORE`
`2`	`2`	`main.c`
`3`	`3`
`4`	`4`	`^EXIT=0$`