From 57a52d38d5c29aab0febe30f2715db98ef758bc9 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 26 Apr 2022 13:33:14 +0100 Subject: [PATCH 1/5] bv_utilst::sign_extension, zero_extension and zeros can be static These methods do not use any state of bv_utilst and can therefore be static. --- src/solvers/flattening/bv_utils.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solvers/flattening/bv_utils.h b/src/solvers/flattening/bv_utils.h index 35a64eec59b..1b988cda0c6 100644 --- a/src/solvers/flattening/bv_utils.h +++ b/src/solvers/flattening/bv_utils.h @@ -179,17 +179,17 @@ class bv_utilst static bvt extension(const bvt &bv, std::size_t new_size, representationt rep); - bvt sign_extension(const bvt &bv, std::size_t new_size) + static bvt sign_extension(const bvt &bv, std::size_t new_size) { return extension(bv, new_size, representationt::SIGNED); } - bvt zero_extension(const bvt &bv, std::size_t new_size) + static bvt zero_extension(const bvt &bv, std::size_t new_size) { return extension(bv, new_size, representationt::UNSIGNED); } - bvt zeros(std::size_t new_size) const + static bvt zeros(std::size_t new_size) { bvt result; result.resize(new_size, const_literal(false)); From c2f689df425d49cd0586199c9b75cc0582b9f573 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 28 Apr 2022 23:51:55 +0100 Subject: [PATCH 2/5] double-width pointer encoding with numbering for ptr->int --- regression/cbmc/Pointer28/test.desc | 2 +- regression/cbmc/Pointer29/test.desc | 2 +- regression/cbmc/Pointer_array4/test.desc | 2 +- .../cbmc/Pointer_byte_extract8/test.desc | 2 +- .../cbmc/address_space_size_limit1/test.desc | 2 +- .../cbmc/pointer-primitive-check-03/test.desc | 2 +- regression/cbmc/union10/union_list2.desc | 2 +- regression/cbmc/union11/union_list.desc | 2 +- src/goto-programs/goto_trace.cpp | 3 +- src/solvers/flattening/boolbv_width.cpp | 5 +- src/solvers/flattening/bv_pointers.cpp | 67 +++++++++++++------ src/solvers/flattening/bv_pointers.h | 5 +- 12 files changed, 64 insertions(+), 32 deletions(-) diff --git a/regression/cbmc/Pointer28/test.desc b/regression/cbmc/Pointer28/test.desc index f5e039ba3ed..57cf4dd62f0 100644 --- a/regression/cbmc/Pointer28/test.desc +++ b/regression/cbmc/Pointer28/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --pointer-check --little-endian ^EXIT=0$ diff --git a/regression/cbmc/Pointer29/test.desc b/regression/cbmc/Pointer29/test.desc index 9efefbc7362..52168c7eba4 100644 --- a/regression/cbmc/Pointer29/test.desc +++ b/regression/cbmc/Pointer29/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c ^EXIT=0$ diff --git a/regression/cbmc/Pointer_array4/test.desc b/regression/cbmc/Pointer_array4/test.desc index 35cc9d3cd74..4bb07015296 100644 --- a/regression/cbmc/Pointer_array4/test.desc +++ b/regression/cbmc/Pointer_array4/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.i --32 ^EXIT=0$ diff --git a/regression/cbmc/Pointer_byte_extract8/test.desc b/regression/cbmc/Pointer_byte_extract8/test.desc index adcea6ed3e2..b6bb379e28d 100644 --- a/regression/cbmc/Pointer_byte_extract8/test.desc +++ b/regression/cbmc/Pointer_byte_extract8/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --64 --unwind 4 --unwinding-assertions ^EXIT=0$ diff --git a/regression/cbmc/address_space_size_limit1/test.desc b/regression/cbmc/address_space_size_limit1/test.desc index 3bc849b0cbf..9c02e15b09d 100644 --- a/regression/cbmc/address_space_size_limit1/test.desc +++ b/regression/cbmc/address_space_size_limit1/test.desc @@ -1,4 +1,4 @@ -CORE thorough-paths broken-smt-backend +KNOWNBUG thorough-paths broken-smt-backend test.c --no-simplify --unwind 300 --object-bits 8 too many addressed objects diff --git a/regression/cbmc/pointer-primitive-check-03/test.desc b/regression/cbmc/pointer-primitive-check-03/test.desc index 4d529706266..5dbed14bab5 100644 --- a/regression/cbmc/pointer-primitive-check-03/test.desc +++ b/regression/cbmc/pointer-primitive-check-03/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --pointer-primitive-check ^EXIT=10$ diff --git a/regression/cbmc/union10/union_list2.desc b/regression/cbmc/union10/union_list2.desc index 88bd7d7090e..ec533b2c9db 100644 --- a/regression/cbmc/union10/union_list2.desc +++ b/regression/cbmc/union10/union_list2.desc @@ -1,4 +1,4 @@ -CORE broken-z3-smt-backend +KNOWNBUG broken-z3-smt-backend union_list2.c ^EXIT=0$ diff --git a/regression/cbmc/union11/union_list.desc b/regression/cbmc/union11/union_list.desc index 4d4566283f4..1fb5bfa5f86 100644 --- a/regression/cbmc/union11/union_list.desc +++ b/regression/cbmc/union11/union_list.desc @@ -1,4 +1,4 @@ -CORE broken-z3-smt-backend +KNOWNBUG broken-z3-smt-backend union_list.c ^EXIT=0$ diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 6886580a9f9..8ff060451cf 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -246,7 +246,8 @@ std::string trace_numeric_value( { const auto &annotated_pointer_constant = to_annotated_pointer_constant_expr(expr); - auto width = to_pointer_type(expr.type()).get_width(); + // pointers use double-width + auto width = 2 * to_pointer_type(expr.type()).get_width(); auto &value = annotated_pointer_constant.get_value(); auto c = constant_exprt(value, unsignedbv_typet(width)); return numeric_representation(c, ns, options); diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp index 35998a40c7e..2412213f087 100644 --- a/src/solvers/flattening/boolbv_width.cpp +++ b/src/solvers/flattening/boolbv_width.cpp @@ -181,7 +181,10 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const CHECK_RETURN(entry.total_width > 0); } else if(type_id==ID_pointer) - entry.total_width = type_checked_cast(type).get_width(); + { + // encode pointers using twice the number of bits + entry.total_width = 2 * type_checked_cast(type).get_width(); + } else if(type_id==ID_struct_tag) entry.total_width = operator()(ns.follow_tag(to_struct_tag_type(type))); else if(type_id==ID_union_tag) diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 86f0361cb89..b4aeca3115b 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -71,25 +70,19 @@ bv_pointerst::endianness_map(const typet &type, bool little_endian) const return bv_endianness_mapt{type, little_endian, ns, bv_width}; } -std::size_t bv_pointerst::get_object_width(const pointer_typet &) const +std::size_t bv_pointerst::get_object_width(const pointer_typet &type) const { - // not actually type-dependent for now - return config.bv_encoding.object_bits; + return type.get_width(); } std::size_t bv_pointerst::get_offset_width(const pointer_typet &type) const { - const std::size_t pointer_width = type.get_width(); + const std::size_t pointer_width = 2 * type.get_width(); const std::size_t object_width = get_object_width(type); PRECONDITION(pointer_width >= object_width); return pointer_width - object_width; } -std::size_t bv_pointerst::get_address_width(const pointer_typet &type) const -{ - return type.get_width(); -} - bvt bv_pointerst::object_literals(const bvt &bv, const pointer_typet &type) const { @@ -380,12 +373,31 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) can_cast_type(op_type) || op_type.id() == ID_bool || op_type.id() == ID_c_enum || op_type.id() == ID_c_enum_tag) { - // Cast from a bitvector type to pointer. - // We just do a zero extension. - + // Cast from a bitvector type 'i' to pointer. + // 1) top bit not set: NULL + i, zero extended + // 2) top bit set: numbered pointer const bvt &op_bv=convert_bv(op); + auto top_bit = op_bv.back(); + const auto numbered_pointer_bv = prop.new_variables(bits); - return bv_utils.zero_extension(op_bv, bits); + for(std::size_t i = 1; i < numbered_pointers.size(); i++) + { + auto cond = bv_utils.equal( + op_bv, + bv_utilst::concatenate( + bv_utilst::build_constant(i, op_bv.size() - 1), {const_literal(true)})); + bv_utils.cond_implies_equal( + cond, + bv_utilst::zero_extension(numbered_pointers[i], bits), + numbered_pointer_bv); + } + + auto null_object_bv = object_offset_encoding( + bv_utilst::build_constant(pointer_logic.get_null_object(), get_object_width(type)), + bv_utilst::concatenate( + bv_utilst::zero_extension(op_bv, get_offset_width(type) - 1), {const_literal(false)})); + + return bv_utils.select(top_bit, numbered_pointer_bv, null_object_bv); } } else if(expr.id()==ID_if) @@ -736,17 +748,30 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr) expr.id() == ID_typecast && to_typecast_expr(expr).op().type().id() == ID_pointer) { - // pointer to int - bvt op0 = convert_pointer_type(to_typecast_expr(expr).op()); + // Pointer to int. + // We special-case NULL, which should always yield 0. + // Otherwise, we 'number' these, which are indicated by setting + // the top bit. + const auto &pointer_expr = to_typecast_expr(expr).op(); + const bvt pointer_bv = convert_pointer_type(pointer_expr); + const auto is_null = bv_utils.is_zero(pointer_bv); + const auto target_width = boolbv_width(expr.type()); - // squeeze it in! + if(target_width == 0) + return conversion_failed(expr); - std::size_t width=boolbv_width(expr.type()); + if(numbered_pointers.empty()) + numbered_pointers.emplace_back(bvt{}); - if(width==0) - return conversion_failed(expr); + const auto number = numbered_pointers.size(); + + numbered_pointers.push_back(pointer_bv); - return bv_utils.zero_extension(op0, width); + return bv_utils.select( + is_null, + bv_utils.zeros(target_width), + bv_utilst::concatenate( + bv_utils.build_constant(number, target_width - 1), {const_literal(true)})); } else if(expr.id() == ID_object_address) { diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h index eb7536a7620..7730d0caea5 100644 --- a/src/solvers/flattening/bv_pointers.h +++ b/src/solvers/flattening/bv_pointers.h @@ -34,7 +34,6 @@ class bv_pointerst:public boolbvt std::size_t get_object_width(const pointer_typet &) const; std::size_t get_offset_width(const pointer_typet &) const; - std::size_t get_address_width(const pointer_typet &) const; // NOLINTNEXTLINE(readability/identifiers) typedef boolbvt SUB; @@ -109,6 +108,10 @@ class bv_pointerst:public boolbvt /// \param offset: Encoded offset /// \return Pointer encoding static bvt object_offset_encoding(const bvt &object, const bvt &offset); + + /// Table that maps a 'pointer number' to its full-width bit-vector. + /// Used for conversion of pointers to integers. + std::vector numbered_pointers; }; #endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H From 41fed6a177ac31c8b893b3b75d18fba05c089d4b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 29 Apr 2022 14:19:06 +0100 Subject: [PATCH 3/5] fx --- .../equality_through_struct_containing_arrays3/test.desc | 2 +- regression/cbmc-library/memcpy-01/test.desc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/cbmc-library/equality_through_struct_containing_arrays3/test.desc b/regression/cbmc-library/equality_through_struct_containing_arrays3/test.desc index 9efefbc7362..52168c7eba4 100644 --- a/regression/cbmc-library/equality_through_struct_containing_arrays3/test.desc +++ b/regression/cbmc-library/equality_through_struct_containing_arrays3/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c ^EXIT=0$ diff --git a/regression/cbmc-library/memcpy-01/test.desc b/regression/cbmc-library/memcpy-01/test.desc index b8aa4e562b8..3a7e9f5ccac 100644 --- a/regression/cbmc-library/memcpy-01/test.desc +++ b/regression/cbmc-library/memcpy-01/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --bounds-check --pointer-check ^EXIT=0$ From 0c522389d96b7861c7bd7d472d344938d11b11d2 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 29 Apr 2022 14:19:18 +0100 Subject: [PATCH 4/5] fx --- src/solvers/flattening/bv_pointers.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index b4aeca3115b..39c5ef859c5 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -385,7 +385,8 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) auto cond = bv_utils.equal( op_bv, bv_utilst::concatenate( - bv_utilst::build_constant(i, op_bv.size() - 1), {const_literal(true)})); + bv_utilst::build_constant(i, op_bv.size() - 1), + {const_literal(true)})); bv_utils.cond_implies_equal( cond, bv_utilst::zero_extension(numbered_pointers[i], bits), @@ -393,9 +394,11 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) } auto null_object_bv = object_offset_encoding( - bv_utilst::build_constant(pointer_logic.get_null_object(), get_object_width(type)), + bv_utilst::build_constant( + pointer_logic.get_null_object(), get_object_width(type)), bv_utilst::concatenate( - bv_utilst::zero_extension(op_bv, get_offset_width(type) - 1), {const_literal(false)})); + bv_utilst::zero_extension(op_bv, get_offset_width(type) - 1), + {const_literal(false)})); return bv_utils.select(top_bit, numbered_pointer_bv, null_object_bv); } @@ -771,7 +774,8 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr) is_null, bv_utils.zeros(target_width), bv_utilst::concatenate( - bv_utils.build_constant(number, target_width - 1), {const_literal(true)})); + bv_utils.build_constant(number, target_width - 1), + {const_literal(true)})); } else if(expr.id() == ID_object_address) { From 69742ac3480263a2eef50bc7181eff050c8ac9c7 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 29 Apr 2022 15:18:38 +0100 Subject: [PATCH 5/5] fx --- regression/goto-harness/nondet_elements_longer_lists/test.desc | 2 +- .../goto-harness/nondet_elements_longer_lists_global/test.desc | 2 +- .../goto-harness/nondet_initialize_static_arrays/test.desc | 2 +- .../pointer-function-parameters-equal-simple/test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../goto-harness/void-star-pointer/test-array-as-array.desc | 2 +- 8 files changed, 8 insertions(+), 8 deletions(-) diff --git a/regression/goto-harness/nondet_elements_longer_lists/test.desc b/regression/goto-harness/nondet_elements_longer_lists/test.desc index cb71825070a..62e6c6f0afb 100644 --- a/regression/goto-harness/nondet_elements_longer_lists/test.desc +++ b/regression/goto-harness/nondet_elements_longer_lists/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --harness-type call-function --max-nondet-tree-depth 4 --min-null-tree-depth 1 --function test_function \[test_function.assertion.\d+\] line \d+ assertion list_walker->datum == \+\+i: SUCCESS diff --git a/regression/goto-harness/nondet_elements_longer_lists_global/test.desc b/regression/goto-harness/nondet_elements_longer_lists_global/test.desc index 52218e7877d..2f880693df1 100644 --- a/regression/goto-harness/nondet_elements_longer_lists_global/test.desc +++ b/regression/goto-harness/nondet_elements_longer_lists_global/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --harness-type call-function --max-nondet-tree-depth 4 --min-null-tree-depth 1 --function test_function --nondet-globals \[test_function.assertion.\d+\] line \d+ assertion list_walker->datum == \+\+i: SUCCESS diff --git a/regression/goto-harness/nondet_initialize_static_arrays/test.desc b/regression/goto-harness/nondet_initialize_static_arrays/test.desc index d0173ae1e36..ece12ad7345 100644 --- a/regression/goto-harness/nondet_initialize_static_arrays/test.desc +++ b/regression/goto-harness/nondet_initialize_static_arrays/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --function func --min-null-tree-depth 10 --max-nondet-tree-depth 4 --harness-type call-function ^EXIT=0$ diff --git a/regression/goto-harness/pointer-function-parameters-equal-simple/test.desc b/regression/goto-harness/pointer-function-parameters-equal-simple/test.desc index 1f9be5e19f0..41a17d853d2 100644 --- a/regression/goto-harness/pointer-function-parameters-equal-simple/test.desc +++ b/regression/goto-harness/pointer-function-parameters-equal-simple/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function --treat-pointers-equal 'p,q;r,s,t' ^EXIT=0$ diff --git a/regression/goto-harness/pointer-function-parameters-struct-mutual-recursion/test.desc b/regression/goto-harness/pointer-function-parameters-struct-mutual-recursion/test.desc index 9bef5d48a87..044ad592e00 100644 --- a/regression/goto-harness/pointer-function-parameters-struct-mutual-recursion/test.desc +++ b/regression/goto-harness/pointer-function-parameters-struct-mutual-recursion/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function ^EXIT=0$ diff --git a/regression/goto-harness/pointer-function-parameters-struct-simple-recursion-2/test.desc b/regression/goto-harness/pointer-function-parameters-struct-simple-recursion-2/test.desc index 3ba3174202a..98bb7c42aa3 100644 --- a/regression/goto-harness/pointer-function-parameters-struct-simple-recursion-2/test.desc +++ b/regression/goto-harness/pointer-function-parameters-struct-simple-recursion-2/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --function func --min-null-tree-depth 10 --max-nondet-tree-depth 2 --harness-type call-function ^EXIT=0$ diff --git a/regression/goto-harness/pointer-function-parameters-struct-simple-recursion/test.desc b/regression/goto-harness/pointer-function-parameters-struct-simple-recursion/test.desc index 9bef5d48a87..044ad592e00 100644 --- a/regression/goto-harness/pointer-function-parameters-struct-simple-recursion/test.desc +++ b/regression/goto-harness/pointer-function-parameters-struct-simple-recursion/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function ^EXIT=0$ diff --git a/regression/goto-harness/void-star-pointer/test-array-as-array.desc b/regression/goto-harness/void-star-pointer/test-array-as-array.desc index 653a8107605..4231923ad06 100644 --- a/regression/goto-harness/void-star-pointer/test-array-as-array.desc +++ b/regression/goto-harness/void-star-pointer/test-array-as-array.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --harness-type call-function --function test_ptr_array --treat-pointer-as-array input_array \[test_ptr_array\.assertion\.1\] line \d+ assertion input_array\[0\] == 0: SUCCESS