From c7b7bdc4200fed94ddd18b613cc10e23fe67ed7f Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 25 Aug 2023 11:55:24 +0100 Subject: [PATCH 1/5] Shadow memory implementation refactor and doxygen --- src/goto-symex/shadow_memory_util.cpp | 30 +++++++++++++++++---------- src/goto-symex/shadow_memory_util.h | 13 +++++++----- 2 files changed, 27 insertions(+), 16 deletions(-) diff --git a/src/goto-symex/shadow_memory_util.cpp b/src/goto-symex/shadow_memory_util.cpp index a7ee7502652..80764335641 100644 --- a/src/goto-symex/shadow_memory_util.cpp +++ b/src/goto-symex/shadow_memory_util.cpp @@ -22,17 +22,16 @@ Author: Peter Schrammel #include #include -#include // 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(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(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(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(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(type) && can_cast_expr(expr) && to_array_type(type).size().get_bool(ID_C_SSA_symbol)) { remove_array_type_l2(expr.type()); @@ -80,7 +79,7 @@ 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(expr)) { expr = to_dereference_expr(expr).pointer(); } @@ -88,7 +87,7 @@ void clean_pointer_expr(exprt &expr, const typet &type) { expr = address_of_exprt(expr); } - POSTCONDITION(expr.type().id() == ID_pointer); + POSTCONDITION(can_cast_type(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 index f2bd5db1a60..e7a89f4c930 100644 --- a/src/goto-symex/shadow_memory_util.h +++ b/src/goto-symex/shadow_memory_util.h @@ -37,10 +37,11 @@ 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, @@ -48,20 +49,22 @@ void log_set_field( 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 &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, From 46135dadbc9d9fe70d030023b58253065adc4b09 Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Fri, 25 Aug 2023 14:59:48 +0100 Subject: [PATCH 2/5] Fix SAT failure when bit-or-ing pointers When setting shadow memory for pointer types the value is replicated by applying left shift and combining the shifted values with bitwise-or. However the SAT solver does not support bitwise-or for pointer types. This commit changes the way the replication is done for pointer types by converting them to an unsigned bitvector of the pointer type size, performing the shift and bitwise-or on this bitvector type and then casting it to pointer at the end. --- src/util/expr_initializer.cpp | 14 +++++-- unit/util/expr_initializer.cpp | 74 ++++++++++++++++++++++++++++++++++ 2 files changed, 85 insertions(+), 3 deletions(-) diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index 4804fbfcdb7..241aab55b83 100644 --- 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(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 index f5f2d5e990c..28663679ac2 100644 --- 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]") From 1d4a8d11895e169cea215757b95a5cec3e598eb1 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 13 Mar 2021 21:58:59 +0000 Subject: [PATCH 3/5] Correctly set value-set dereference pointer --- src/pointer-analysis/value_set_dereference.cpp | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index fafe7cad353..924480fbe25 100644 --- 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 #include +#include #include #include #include @@ -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; } From 4655ef4afd397fecd14b29caeb03aff350c22837 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 29 Aug 2023 16:02:36 +0100 Subject: [PATCH 4/5] Marking CORE more Shadow Memory regression tests Marking as CORE all the shadow memory regression tests that are now passing. The remaining regression tests that are still marked as KNOWNBUG will be added as soon as the implementation will be fixed. --- regression/cbmc-shadow-memory/char1/test.desc | 2 +- regression/cbmc-shadow-memory/constchar-pointers1/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/maybe-null1/test.desc | 2 +- regression/cbmc-shadow-memory/nondet-size-arrays1/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/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 +- 11 files changed, 11 insertions(+), 11 deletions(-) diff --git a/regression/cbmc-shadow-memory/char1/test.desc b/regression/cbmc-shadow-memory/char1/test.desc index 52168c7eba4..9efefbc7362 100644 --- 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 index dbd7c3b8a09..e21095fda9d 100644 --- 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 index 52168c7eba4..9efefbc7362 100644 --- 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 index 52168c7eba4..9efefbc7362 100644 --- 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 index 52168c7eba4..9efefbc7362 100644 --- 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/test.desc b/regression/cbmc-shadow-memory/nondet-size-arrays1/test.desc index 52168c7eba4..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 @@ -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 index 52168c7eba4..9efefbc7362 100644 --- 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 index b35013bafd6..dc9fb11329e 100644 --- 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 index dbb3109cc02..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 @@ -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 index dcb960a7ae2..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 @@ -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 index 52168c7eba4..9efefbc7362 100644 --- 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$ From 7417bef4405e81eccc43b21803acda3e5f8f8cba Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Wed, 30 Aug 2023 12:14:07 +0100 Subject: [PATCH 5/5] Fix missing alloca definition on regression test Windows requires alloca to be defined otherwise an invariant will be violated (the invariant violation will be changed in another subsequent PR). --- regression/cbmc-shadow-memory/nondet-size-arrays1/main.c | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/regression/cbmc-shadow-memory/nondet-size-arrays1/main.c b/regression/cbmc-shadow-memory/nondet-size-arrays1/main.c index c462d2ff30d..82446d1a335 100644 --- 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 #include +#ifdef _WIN32 +void *alloca(size_t alloca_size); +#endif + int main() { __CPROVER_field_decl_local("field1", (char)0);