Merge pull request #7868 from NlightNFotis/shadow_mem_rev

Enrico Steffinlongo · web-flow · commit decd2839c2f5 · 2023-08-30T16:31:51.000+03:00
Shadow Memory: Refactoring, enabling tests and minor doxygen improvements.
diff --git a/regression/cbmc-shadow-memory/char1/test.desc b/regression/cbmc-shadow-memory/char1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^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 @@
-KNOWNBUG
+CORE
 main.c
 --unwind 11
 ^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 @@
-KNOWNBUG
+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
@@ -1,4 +1,4 @@
-KNOWNBUG
+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 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/nondet-size-arrays1/main.c b/regression/cbmc-shadow-memory/nondet-size-arrays1/main.c
@@ -1,6 +1,10 @@
 #include <assert.h>
 #include <stdlib.h>
 
+#ifdef _WIN32
+void *alloca(size_t alloca_size);
+#endif
+
 int main()
 {
   __CPROVER_field_decl_local("field1", (char)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 @@
-KNOWNBUG
+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 @@
-KNOWNBUG
+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
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --unwind 15
 ^EXIT=0$
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 @@
-KNOWNBUG
+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
@@ -1,4 +1,4 @@
-KNOWNBUG
+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
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/src/goto-symex/shadow_memory_util.cpp b/src/goto-symex/shadow_memory_util.cpp
@@ -22,17 +22,16 @@ Author: Peter Schrammel
 #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)
+  if(can_cast_expr<typecast_exprt>(string_expr))
     return extract_field_name(to_typecast_expr(string_expr).op());
-  else if(string_expr.id() == ID_address_of)
+  else if(can_cast_expr<address_of_exprt>(string_expr))
     return extract_field_name(to_address_of_expr(string_expr).object());
-  else if(string_expr.id() == ID_index)
+  else if(can_cast_expr<index_exprt>(string_expr))
     return extract_field_name(to_index_expr(string_expr).array());
   else if(string_expr.id() == ID_string_constant)
   {
@@ -42,8 +41,8 @@ irep_idt extract_field_name(const exprt &string_expr)
     UNREACHABLE;
 }
 
-/// If the given type is an array type, then remove the L2 level
-/// renaming from its size.
+/// If the given type is an array type, then remove the L2 level renaming
+/// from its size.
 /// \param type Type to be modified
 static void remove_array_type_l2(typet &type)
 {
@@ -56,7 +55,7 @@ static void remove_array_type_l2(typet &type)
 
 exprt deref_expr(const exprt &expr)
 {
-  if(expr.id() == ID_address_of)
+  if(can_cast_expr<address_of_exprt>(expr))
   {
     return to_address_of_expr(expr).object();
   }
@@ -67,7 +66,7 @@ exprt deref_expr(const exprt &expr)
 void clean_pointer_expr(exprt &expr, const typet &type)
 {
   if(
-    type.id() == ID_array && expr.id() == ID_symbol &&
+    can_cast_type<array_typet>(type) && can_cast_expr<symbol_exprt>(expr) &&
     to_array_type(type).size().get_bool(ID_C_SSA_symbol))
   {
     remove_array_type_l2(expr.type());
@@ -80,15 +79,15 @@ void clean_pointer_expr(exprt &expr, const typet &type)
     expr = address_of_exprt(expr);
     expr.type() = pointer_type(char_type());
   }
-  else if(expr.id() == ID_dereference)
+  else if(can_cast_expr<dereference_exprt>(expr))
   {
     expr = to_dereference_expr(expr).pointer();
   }
   else
   {
     expr = address_of_exprt(expr);
   }
-  POSTCONDITION(expr.type().id() == ID_pointer);
+  POSTCONDITION(can_cast_type<pointer_typet>(expr.type()));
 }
 
 void log_set_field(
@@ -691,7 +690,16 @@ static exprt get_matched_expr_cond(
   return expr_cond;
 }
 
-// TODO: doxygen?
+/// Retrieve the shadow value a pointer expression may point to.
+/// \param shadow The shadow expression.
+/// \param matched_base_descriptor The base descriptor for the shadow object.
+/// \param expr The pointer expression.
+/// \param ns The namespace within which we're going to perform symbol lookups.
+/// \param log The message log to which we're going to print debugging messages,
+///   if debugging is set.
+/// \returns A `valuet` object denoting the dereferenced object within shadow
+///   memory, guarded by a appropriate condition (of the form
+///   pointer == &shadow_object).
 static value_set_dereferencet::valuet get_shadow_dereference(
   const exprt &shadow,
   const object_descriptor_exprt &matched_base_descriptor,
diff --git a/src/goto-symex/shadow_memory_util.h b/src/goto-symex/shadow_memory_util.h
@@ -37,31 +37,34 @@ 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
+/// Converts a given expression into a dereference_exprt.
 exprt deref_expr(const exprt &expr);
 
-// TODO: DOxYGEN
+/// Logs setting a value to a given shadow field. Mainly for use for
+/// debugging purposes.
 void log_set_field(
   const namespacet &ns,
   const messaget &log,
   const irep_idt &field_name,
   const exprt &expr,
   const exprt &value);
 
-// TODO: doxygen
+/// Logs setting a value to a given shadow field. Mainly for use for
+/// debugging purposes.
 void log_get_field(
   const namespacet &ns,
   const messaget &log,
   const irep_idt &field_name,
   const exprt &expr);
 
-// TODO: doxygen
+/// Logs the retrieval of the value associated with a given shadow
+/// memory field. Mainly for use for debugging purposes. Dual to log_get_field.
 void log_value_set(
   const namespacet &ns,
   const messaget &log,
   const std::vector<exprt> &value_set);
 
-// TODO: doxygen
+/// Log a match between a value in the value set of a given expression, and
 void log_value_set_match(
   const namespacet &ns,
   const messaget &log,
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_iterator.h>
@@ -661,8 +662,21 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     result.pointer = typecast_exprt::conditional_cast(
       address_of_exprt{skip_typecast(o.root_object())}, pointer_type);
 
-    if(!memory_model(result.value, dereference_type, offset, ns))
+    if(memory_model(result.value, dereference_type, offset, ns))
+    {
+      // set pointer correctly
+      result.pointer = typecast_exprt::conditional_cast(
+        plus_exprt(
+          typecast_exprt(
+            result.pointer,
+            pointer_typet(char_type(), pointer_type.get_width())),
+          offset),
+        pointer_type);
+    }
+    else
+    {
       return {}; // give up, no way that this is ok
+    }
 
     return result;
   }
diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp
@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "magic.h"
 #include "namespace.h" // IWYU pragma: keep
 #include "std_code.h"
+#include "symbol_table.h"
 
 class expr_initializert
 {
@@ -393,9 +394,15 @@ exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type)
 
     // We haven't got a constant. So, build the expression using shift-and-or.
     exprt::operandst values;
+
+    typet operation_type = output_type;
+    if(const auto ptr_type = type_try_dynamic_cast<pointer_typet>(output_type))
+    {
+      operation_type = unsignedbv_typet{ptr_type->get_width()};
+    }
     // Let's cast init_byte_expr to output_type.
     const exprt casted_init_byte_expr =
-      typecast_exprt::conditional_cast(init_byte_expr, output_type);
+      typecast_exprt::conditional_cast(init_byte_expr, operation_type);
     values.push_back(casted_init_byte_expr);
     for(size_t i = 1; i < size; ++i)
     {
@@ -404,8 +411,9 @@ exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type)
         from_integer(config.ansi_c.char_width * i, size_type())));
     }
     if(values.size() == 1)
-      return values[0];
-    return multi_ary_exprt(ID_bitor, values, output_type);
+      return typecast_exprt::conditional_cast(values[0], output_type);
+    return typecast_exprt::conditional_cast(
+      multi_ary_exprt(ID_bitor, values, operation_type), output_type);
   }
 
   // Anything else. We don't know what to do with it. So, just cast.
diff --git a/unit/util/expr_initializer.cpp b/unit/util/expr_initializer.cpp
@@ -177,6 +177,18 @@ TEST_CASE(
       from_integer(init_expr_value, signedbv_typet{init_expr_size}),
       output_type);
     REQUIRE(result_with_signed_init_type == result);
+
+    // Check that replicating a pointer_value is same as unsigned_bv.
+    const pointer_typet pointer_type{bool_typet{}, output_size};
+    const auto result_with_pointer_type = duplicate_per_byte(
+      from_integer(init_expr_value, signedbv_typet{init_expr_size}),
+      pointer_type);
+    auto pointer_typed_expected =
+      from_integer(output_expected_value, unsignedbv_typet{output_size});
+    // Forcing the type to be pointer_typet otherwise from_integer fails when
+    // the init value is not 0 (NULL).
+    pointer_typed_expected.type() = pointer_type;
+    REQUIRE(result_with_pointer_type == pointer_typed_expected);
   }
 }
 
@@ -212,6 +224,21 @@ TEST_CASE(
       replicate_expression(casted_init_expr, output_type, replication_count);
 
     REQUIRE(result == expected);
+
+    // Check that replicating a pointer_value is same as unsigned_bv modulo a
+    // typecast outside.
+    const pointer_typet pointer_type{bool_typet{}, output_size};
+    const auto pointer_typed_result =
+      duplicate_per_byte(init_expr, pointer_type);
+    const auto pointer_unsigned_corr_type = unsignedbv_typet{output_size};
+    const auto pointer_init_expr =
+      typecast_exprt::conditional_cast(init_expr, pointer_unsigned_corr_type);
+    const auto pointer_expected = typecast_exprt::conditional_cast(
+      replicate_expression(
+        pointer_init_expr, pointer_unsigned_corr_type, replication_count),
+      pointer_type);
+
+    REQUIRE(pointer_typed_result == pointer_expected);
   }
 }
 
@@ -312,6 +339,53 @@ TEST_CASE(
   }
 }
 
+TEST_CASE(
+  "expr_initializer on variable-bit pointer type",
+  "[core][util][expr_initializer]")
+{
+  auto test = expr_initializer_test_environmentt::make();
+  const std::size_t input_type_size = GENERATE(3, 8, 16, 20);
+  SECTION(
+    "Testing with expected type as unsigned_bv of size " +
+    std::to_string(input_type_size))
+  {
+    typet input_type = pointer_typet{bool_typet{}, input_type_size};
+    SECTION("nondet_initializer works")
+    {
+      const auto result = nondet_initializer(input_type, test.loc, test.ns);
+      REQUIRE(result.has_value());
+      const auto expected = side_effect_expr_nondett{
+        pointer_typet{bool_typet{}, input_type_size}, test.loc};
+      REQUIRE(result.value() == expected);
+      const auto expr_result =
+        expr_initializer(input_type, test.loc, test.ns, exprt(ID_nondet));
+      REQUIRE(expr_result == result);
+    }
+    SECTION("zero_initializer works")
+    {
+      const auto result = zero_initializer(input_type, test.loc, test.ns);
+      REQUIRE(result.has_value());
+      auto expected =
+        from_integer(0, pointer_typet{bool_typet{}, input_type_size});
+      REQUIRE(result.value() == expected);
+      const auto expr_result = expr_initializer(
+        input_type, test.loc, test.ns, constant_exprt(ID_0, char_type()));
+      REQUIRE(expr_result == result);
+    }
+    SECTION("expr_initializer calls duplicate_per_byte")
+    {
+      const exprt init_value =
+        from_integer(0x0A, unsignedbv_typet{config.ansi_c.char_width});
+      const auto result =
+        expr_initializer(input_type, test.loc, test.ns, init_value);
+      REQUIRE(result.has_value());
+      const auto expected = duplicate_per_byte(
+        init_value, pointer_typet{bool_typet{}, input_type_size});
+      REQUIRE(result.value() == expected);
+    }
+  }
+}
+
 TEST_CASE(
   "expr_initializer on c_enum and c_enum_tag",
   "[core][util][expr_initializer]")

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