From acfea65cba6a098e501edf2b32423db364a96453 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 28 Apr 2018 14:14:17 +0100 Subject: [PATCH 1/4] __CPROVER_r_ok and __CPROVER_w_ok added to ANSI-C front-end --- doc/cbmc-user-manual.md | 9 +++++++++ src/ansi-c/c_typecheck_expr.cpp | 17 +++++++++++++++++ src/ansi-c/cprover_builtin_headers.h | 2 ++ src/ansi-c/expr2c.cpp | 6 ++++++ src/ansi-c/library/cprover.h | 2 ++ src/util/irep_ids.def | 2 ++ 6 files changed, 38 insertions(+) diff --git a/doc/cbmc-user-manual.md b/doc/cbmc-user-manual.md index 94b27408feb..6a64b80ff86 100644 --- a/doc/cbmc-user-manual.md +++ b/doc/cbmc-user-manual.md @@ -2190,6 +2190,15 @@ to the program. If the expression evaluates to false, the execution aborts without failure. More detail on the use of assumptions is in the section on [Assumptions and Assertions](modeling-assertions.shtml). +#### \_\_CPROVER\_r_ok, \_\_CPROVER\_w_ok + + void __CPROVER_r_ok(const void *, size_t size); + void __CPROVER_w_ok(cosnt void *, size_t size); + +The function **\_\_CPROVER\_r_ok** returns true if reading the piece of +memory starting at the given pointer with the given size is safe. +**\_\_CPROVER\_w_ok** does the same with writing. + #### \_\_CPROVER\_same\_object, \_\_CPROVER\_POINTER\_OBJECT, \_\_CPROVER\_POINTER\_OFFSET, \_\_CPROVER\_DYNAMIC\_OBJECT _Bool __CPROVER_same_object(const void *, const void *); diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 8a93f58d6d4..26091bb88ca 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2334,6 +2334,23 @@ exprt c_typecheck_baset::do_special_functions( return malloc_expr; } + else if( + identifier == CPROVER_PREFIX "r_ok" || identifier == CPROVER_PREFIX "w_ok") + { + if(expr.arguments().size() != 2) + { + err_location(f_op); + error() << identifier << " expects two operands" << eom; + throw 0; + } + + irep_idt id = identifier == CPROVER_PREFIX "r_ok" ? ID_r_ok : ID_w_ok; + + predicate_exprt ok_expr(id, expr.arguments()[0], expr.arguments()[1]); + ok_expr.add_source_location() = source_location; + + return ok_expr; + } else if(identifier==CPROVER_PREFIX "isinff" || identifier==CPROVER_PREFIX "isinfd" || identifier==CPROVER_PREFIX "isinfld" || diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index 0b05aa245e7..7838b138e45 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -9,6 +9,8 @@ __CPROVER_bool __CPROVER_invalid_pointer(const void *); __CPROVER_bool __CPROVER_is_zero_string(const void *); __CPROVER_size_t __CPROVER_zero_string_length(const void *); __CPROVER_size_t __CPROVER_buffer_size(const void *); +__CPROVER_bool __CPROVER_r_ok(const void *, __CPROVER_size_t); +__CPROVER_bool __CPROVER_w_ok(const void *, __CPROVER_size_t); // bitvector analysis __CPROVER_bool __CPROVER_get_flag(const void *, const char *); diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 2f91ac42e00..80b5515dd0f 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3515,6 +3515,12 @@ std::string expr2ct::convert_with_precedence( return convert_function(src, "__builtin_popcount", precedence=16); } + else if(src.id() == ID_r_ok) + return convert_function(src, "R_OK", precedence = 16); + + else if(src.id() == ID_w_ok) + return convert_function(src, "W_OK", precedence = 16); + else if(src.id()==ID_invalid_pointer) return convert_function(src, "INVALID-POINTER", precedence=16); diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index ab68bbcbe68..67d8ad0b207 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -24,6 +24,8 @@ void __CPROVER_precondition(__CPROVER_bool assertion, const char *description); __CPROVER_bool __CPROVER_is_zero_string(const void *); __CPROVER_size_t __CPROVER_zero_string_length(const void *); __CPROVER_size_t __CPROVER_buffer_size(const void *); +__CPROVER_bool __CPROVER_r_ok(const void *, __CPROVER_size_t); +__CPROVER_bool __CPROVER_w_ok(const void *, __CPROVER_size_t); #if 0 __CPROVER_bool __CPROVER_equal(); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index fcda57ce383..fbba1b6b2e6 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -691,6 +691,8 @@ IREP_ID_TWO(C_unnamed_object, #unnamed_object) IREP_ID_TWO(C_temporary_avoided, #temporary_avoided) IREP_ID_TWO(C_qualifier, #qualifier) IREP_ID_TWO(C_array_ini, #array_ini) +IREP_ID_ONE(r_ok) +IREP_ID_ONE(w_ok) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.def in their source tree From 732ce2aee6a2e61b6855cfc88bdac43c3e14f0be Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 6 Jun 2018 09:54:46 +0100 Subject: [PATCH 2/4] expand __CPROVER_r/w_ok in goto_check --- src/analyses/goto_check.cpp | 153 ++++++++++++++++++++++++++++++++++++ 1 file changed, 153 insertions(+) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index eb519905b70..e88374ed503 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -86,6 +86,19 @@ class goto_checkt bool address); void check(const exprt &expr); + struct conditiont + { + conditiont(const exprt &_assertion, const std::string &_description) + : assertion(_assertion), description(_description) + { + } + + exprt assertion; + std::string description; + }; + + using conditionst = std::list; + void bounds_check(const index_exprt &expr, const guardt &guard); void div_by_zero_check(const div_exprt &expr, const guardt &guard); void mod_by_zero_check(const mod_exprt &expr, const guardt &guard); @@ -97,10 +110,12 @@ class goto_checkt const guardt &guard, const exprt &access_lb, const exprt &access_ub); + conditionst address_check(const exprt &address, const exprt &size); void integer_overflow_check(const exprt &expr, const guardt &guard); void conversion_check(const exprt &expr, const guardt &guard); void float_overflow_check(const exprt &expr, const guardt &guard); void nan_check(const exprt &expr, const guardt &guard); + void rw_ok_check(exprt &expr); std::string array_name(const exprt &expr); @@ -139,6 +154,8 @@ class goto_checkt typedef optionst::value_listt error_labelst; error_labelst error_labels; + // the first element of the pair is the base address, + // and the second is the size of the region typedef std::pair allocationt; typedef std::list allocationst; allocationst allocations; @@ -1092,6 +1109,118 @@ void goto_checkt::pointer_validity_check( } } +goto_checkt::conditionst +goto_checkt::address_check(const exprt &address, const exprt &size) +{ + if(!enable_pointer_check) + return {}; + + PRECONDITION(address.type().id() == ID_pointer); + const auto &pointer_type = to_pointer_type(address.type()); + + local_bitvector_analysist::flagst flags = + local_bitvector_analysis->get(t, address); + + // For Java, we only need to check for null + if(mode == ID_java) + { + if(flags.is_unknown() || flags.is_null()) + { + notequal_exprt not_eq_null(address, null_pointer_exprt(pointer_type)); + + return {conditiont(not_eq_null, "reference is null")}; + } + else + return {}; + } + else + { + conditionst conditions; + exprt::operandst alloc_disjuncts; + + for(const auto &a : allocations) + { + typecast_exprt int_ptr(address, a.first.type()); + + binary_relation_exprt lb_check(a.first, ID_le, int_ptr); + + plus_exprt ub(int_ptr, size, int_ptr.type()); + + binary_relation_exprt ub_check(ub, ID_le, plus_exprt(a.first, a.second)); + + alloc_disjuncts.push_back(and_exprt(lb_check, ub_check)); + } + + const exprt allocs = disjunction(alloc_disjuncts); + + if(flags.is_unknown() || flags.is_null()) + { + conditions.push_back(conditiont( + or_exprt(allocs, not_exprt(null_pointer(address))), "pointer NULL")); + } + + if(flags.is_unknown()) + { + conditions.push_back(conditiont( + not_exprt(invalid_pointer(address)), + "pointer invalid")); + } + + if(flags.is_uninitialized()) + { + conditions.push_back(conditiont( + or_exprt(allocs, not_exprt(invalid_pointer(address))), + "pointer uninitialized")); + } + + if(flags.is_unknown() || flags.is_dynamic_heap()) + { + conditions.push_back(conditiont( + not_exprt(deallocated(address, ns)), + "deallocated dynamic object")); + } + + if(flags.is_unknown() || flags.is_dynamic_local()) + { + conditions.push_back(conditiont( + not_exprt(dead_object(address, ns)), "dead object")); + } + + if(flags.is_unknown() || flags.is_dynamic_heap()) + { + const or_exprt dynamic_bounds_violation( + dynamic_object_lower_bound(address, ns, nil_exprt()), + dynamic_object_upper_bound(address, ns, size)); + + conditions.push_back(conditiont( + implies_exprt(malloc_object(address, ns), not_exprt(dynamic_bounds_violation)), + "pointer outside dynamic object bounds")); + } + + if( + flags.is_unknown() || flags.is_dynamic_local() || + flags.is_static_lifetime()) + { + const or_exprt object_bounds_violation( + object_lower_bound(address, ns, nil_exprt()), + object_upper_bound(address, ns, size)); + + conditions.push_back(conditiont( + implies_exprt(not_exprt(dynamic_object(address)), not_exprt(object_bounds_violation)), + "dereference failure: pointer outside object bounds")); + } + + if(flags.is_unknown() || flags.is_integer_address()) + { + conditions.push_back(conditiont( + implies_exprt(integer_address(address), allocs), + "invalid integer address")); + } + + return conditions; + } +} + std::string goto_checkt::array_name(const exprt &expr) { return ::array_name(ns, expr); @@ -1510,6 +1639,27 @@ void goto_checkt::check(const exprt &expr) check_rec(expr, guard, false); } +/// expand the r_ok and w_ok predicates +void goto_checkt::rw_ok_check(exprt &expr) +{ + for(auto &op : expr.operands()) + rw_ok_check(op); + + if(expr.id() == ID_r_ok || expr.id() == ID_w_ok) + { + // these get an address as first argument and a size as second + DATA_INVARIANT( + expr.operands().size() == 2, "r/w_ok must have two operands"); + + const auto conditions = address_check(expr.op0(), expr.op1()); + exprt::operandst conjuncts; + for(const auto &c : conditions) + conjuncts.push_back(c.assertion); + + expr = conjunction(conjuncts); + } +} + void goto_checkt::goto_check( goto_functiont &goto_function, const irep_idt &_mode) @@ -1659,6 +1809,9 @@ void goto_checkt::goto_check( else if(i.is_assert()) { bool is_user_provided=i.source_location.get_bool("user-provided"); + + rw_ok_check(i.guard); + if((is_user_provided && !enable_assertions && i.source_location.get_property_class()!="error label") || (!is_user_provided && !enable_built_in_assertions)) From 4a24ad40c7b30a1fff6937dad8a4fe0430726901 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 6 Jun 2018 09:54:24 +0100 Subject: [PATCH 3/4] use __CPROVER_r/w_ok in string.c library --- regression/cbmc/memcpy1/test.desc | 2 +- regression/cbmc/memset1/test.desc | 4 +-- regression/cbmc/memset3/test.desc | 4 +-- src/ansi-c/library/string.c | 49 +++++++++++++++++-------------- 4 files changed, 32 insertions(+), 27 deletions(-) diff --git a/regression/cbmc/memcpy1/test.desc b/regression/cbmc/memcpy1/test.desc index 12892942e7b..611ab02bbce 100644 --- a/regression/cbmc/memcpy1/test.desc +++ b/regression/cbmc/memcpy1/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -\[(__builtin___memcpy_chk|memcpy)\.pointer_dereference\.[0-9]+\] dereference failure: pointer outside object bounds in \*\(\(\(const char \*\)src \+ \(signed (long (long )?)?int\)n\) - (\(signed long (long )?int\))?1\): FAILURE$ +^\[main\.precondition_instance\..*\] memcpy source region readable: FAILURE$ \*\* 1 of [0-9]+ failed -- ^warning: ignoring diff --git a/regression/cbmc/memset1/test.desc b/regression/cbmc/memset1/test.desc index 2473a80a95e..601660aa402 100644 --- a/regression/cbmc/memset1/test.desc +++ b/regression/cbmc/memset1/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -\[main.assertion.7\] assertion A\[1\]==0x01010111: FAILURE -\*\* 1 of 12 failed +^\[main.assertion.7\] assertion A\[1\]==0x01010111: FAILURE$ +\*\* 1 of [0-9]+ failed -- ^warning: ignoring diff --git a/regression/cbmc/memset3/test.desc b/regression/cbmc/memset3/test.desc index 9cb43afa709..1f8018852c5 100644 --- a/regression/cbmc/memset3/test.desc +++ b/regression/cbmc/memset3/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -\[.*] dereference failure: pointer outside dynamic object bounds in .*: FAILURE -\*\* 2 of .* failed \(.*\) +^\[main\.precondition_instance\..*] memset destination region writeable: FAILURE$ +\*\* 1 of [0-9]+ failed \(.*\) -- ^warning: ignoring diff --git a/src/ansi-c/library/string.c b/src/ansi-c/library/string.c index d001a5f4fef..61c0fb8549e 100644 --- a/src/ansi-c/library/string.c +++ b/src/ansi-c/library/string.c @@ -597,13 +597,13 @@ void *memcpy(void *dst, const void *src, size_t n) __CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!= __CPROVER_POINTER_OBJECT(src), "memcpy src/dst overlap"); + __CPROVER_precondition(__CPROVER_r_ok(src, n), + "memcpy source region readable"); + __CPROVER_precondition(__CPROVER_w_ok(dst, n), + "memcpy destination region writeable"); if(n > 0) { - (void)*(char *)dst; // check that the memory is accessible - (void)*(const char *)src; // check that the memory is accessible - (void)*(((char *)dst) + n - 1); // check that the memory is accessible - (void)*(((const char *)src) + n - 1); // check that the memory is accessible //for(__CPROVER_size_t i=0; i 0) { - (void)*(char *)dst; // check that the memory is accessible - (void)*(const char *)src; // check that the memory is accessible - (void)*(((char *)dst) + n - 1); // check that the memory is accessible - (void)*(((const char *)src) + n - 1); // check that the memory is accessible //for(__CPROVER_size_t i=0; i 0) { - (void)*(char *)s; // check that the memory is accessible - (void)*(((char *)s) + n - 1); // check that the memory is accessible //char *sp=s; //for(__CPROVER_size_t i=0; i 0) { - (void)*(char *)s; // check that the memory is accessible - (void)*(((char *)s) + n - 1); // check that the memory is accessible //char *sp=s; //for(__CPROVER_size_t i=0; i 0) { - (void)*(char *)s; // check that the memory is accessible - (void)*(((char *)s) + n - 1); // check that the memory is accessible //char *sp=s; //for(__CPROVER_size_t i=0; i 0) { - (void)*(char *)dest; // check that the memory is accessible - (void)*(const char *)src; // check that the memory is accessible - (void)*(((char *)dest) + n - 1); // check that the memory is accessible - (void)*(((const char *)src) + n - 1); // check that the memory is accessible char src_n[n]; __CPROVER_array_copy(src_n, (char *)src); __CPROVER_array_replace((char *)dest, src_n); @@ -848,14 +848,14 @@ void *__builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_s __CPROVER_is_zero_string(dest)=0; } #else + __CPROVER_precondition(__CPROVER_r_ok(src, n), + "memmove source region readable"); + __CPROVER_precondition(__CPROVER_w_ok(dest, n), + "memmove destination region writeable"); (void)size; if(n > 0) { - (void)*(char *)dest; // check that the memory is accessible - (void)*(const char *)src; // check that the memory is accessible - (void)*(((char *)dest) + n - 1); // check that the memory is accessible - (void)*(((const char *)src) + n - 1); // check that the memory is accessible char src_n[n]; __CPROVER_array_copy(src_n, (char *)src); __CPROVER_array_replace((char *)dest, src_n); @@ -883,6 +883,11 @@ inline int memcmp(const void *s1, const void *s2, size_t n) __CPROVER_precondition(__CPROVER_buffer_size(s2)>=n, "memcmp buffer overflow of 2nd argument"); #else + __CPROVER_precondition(__CPROVER_r_ok(s1, n), + "memcmp region 1 readable"); + __CPROVER_precondition(__CPROVER_r_ok(s2, n), + "memcpy region 2 readable"); + const unsigned char *sc1=s1, *sc2=s2; for(; n!=0; n--) { From 0202f34620e27bc3a679b0c720e978d7afe75d99 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 30 Jul 2018 21:33:28 +0100 Subject: [PATCH 4/4] refactor pointer_validity_check using address_check --- src/analyses/goto_check.cpp | 262 +++++++++--------------------------- 1 file changed, 60 insertions(+), 202 deletions(-) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index e88374ed503..8c039f23c0a 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -13,20 +13,21 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include -#include -#include #include +#include +#include +#include +#include #include #include -#include -#include #include -#include +#include +#include #include #include -#include -#include +#include +#include +#include #include #include @@ -99,25 +100,21 @@ class goto_checkt using conditionst = std::list; - void bounds_check(const index_exprt &expr, const guardt &guard); - void div_by_zero_check(const div_exprt &expr, const guardt &guard); - void mod_by_zero_check(const mod_exprt &expr, const guardt &guard); - void undefined_shift_check(const shift_exprt &expr, const guardt &guard); - void pointer_rel_check(const exprt &expr, const guardt &guard); - void pointer_overflow_check(const exprt &expr, const guardt &guard); - void pointer_validity_check( - const dereference_exprt &expr, - const guardt &guard, - const exprt &access_lb, - const exprt &access_ub); + void bounds_check(const index_exprt &, const guardt &); + void div_by_zero_check(const div_exprt &, const guardt &); + void mod_by_zero_check(const mod_exprt &, const guardt &); + void undefined_shift_check(const shift_exprt &, const guardt &); + void pointer_rel_check(const exprt &, const guardt &); + void pointer_overflow_check(const exprt &, const guardt &); + void pointer_validity_check(const dereference_exprt &, const guardt &); conditionst address_check(const exprt &address, const exprt &size); - void integer_overflow_check(const exprt &expr, const guardt &guard); - void conversion_check(const exprt &expr, const guardt &guard); - void float_overflow_check(const exprt &expr, const guardt &guard); - void nan_check(const exprt &expr, const guardt &guard); - void rw_ok_check(exprt &expr); + void integer_overflow_check(const exprt &, const guardt &); + void conversion_check(const exprt &, const guardt &); + void float_overflow_check(const exprt &, const guardt &); + void nan_check(const exprt &, const guardt &); + void rw_ok_check(exprt &); - std::string array_name(const exprt &expr); + std::string array_name(const exprt &); void add_guarded_claim( const exprt &expr, @@ -935,177 +932,25 @@ void goto_checkt::pointer_overflow_check( void goto_checkt::pointer_validity_check( const dereference_exprt &expr, - const guardt &guard, - const exprt &access_lb, - const exprt &access_ub) + const guardt &guard) { if(!enable_pointer_check) return; - const exprt &pointer=expr.op0(); - const pointer_typet &pointer_type= - to_pointer_type(ns.follow(pointer.type())); - - assert(base_type_eq(pointer_type.subtype(), expr.type(), ns)); + const exprt &pointer=expr.pointer(); - local_bitvector_analysist::flagst flags= - local_bitvector_analysis->get(t, pointer); - - // For Java, we only need to check for null - if(mode==ID_java) - { - if(flags.is_unknown() || flags.is_null()) - { - notequal_exprt not_eq_null(pointer, null_pointer_exprt(pointer_type)); + auto conditions = + address_check(pointer, size_of_expr(expr.type(), ns)); - add_guarded_claim( - not_eq_null, - "reference is null", - "pointer dereference", - expr.find_source_location(), - expr, - guard); - } - } - else + for(const auto &c : conditions) { - exprt allocs=false_exprt(); - - if(!allocations.empty()) - { - exprt::operandst disjuncts; - - for(const auto &a : allocations) - { - typecast_exprt int_ptr(pointer, a.first.type()); - - exprt lb(int_ptr); - if(access_lb.is_not_nil()) - { - if(!base_type_eq(lb.type(), access_lb.type(), ns)) - lb=plus_exprt(lb, typecast_exprt(access_lb, lb.type())); - else - lb=plus_exprt(lb, access_lb); - } - - binary_relation_exprt lb_check(a.first, ID_le, lb); - - exprt ub(int_ptr); - if(access_ub.is_not_nil()) - { - if(!base_type_eq(ub.type(), access_ub.type(), ns)) - ub=plus_exprt(ub, typecast_exprt(access_ub, ub.type())); - else - ub=plus_exprt(ub, access_ub); - } - - binary_relation_exprt ub_check( - ub, ID_le, plus_exprt(a.first, a.second)); - - disjuncts.push_back(and_exprt(lb_check, ub_check)); - } - - allocs=disjunction(disjuncts); - } - - if(flags.is_unknown() || - flags.is_null()) - { - add_guarded_claim( - or_exprt(allocs, not_exprt(null_pointer(pointer))), - "dereference failure: pointer NULL", - "pointer dereference", - expr.find_source_location(), - expr, - guard); - } - - if(flags.is_unknown()) - add_guarded_claim( - or_exprt(allocs, not_exprt(invalid_pointer(pointer))), - "dereference failure: pointer invalid", - "pointer dereference", - expr.find_source_location(), - expr, - guard); - - if(flags.is_uninitialized()) - add_guarded_claim( - or_exprt(allocs, not_exprt(invalid_pointer(pointer))), - "dereference failure: pointer uninitialized", - "pointer dereference", - expr.find_source_location(), - expr, - guard); - - if(flags.is_unknown() || - flags.is_dynamic_heap()) - add_guarded_claim( - or_exprt(allocs, not_exprt(deallocated(pointer, ns))), - "dereference failure: deallocated dynamic object", - "pointer dereference", - expr.find_source_location(), - expr, - guard); - - if(flags.is_unknown() || - flags.is_dynamic_local()) - add_guarded_claim( - or_exprt(allocs, not_exprt(dead_object(pointer, ns))), - "dereference failure: dead object", - "pointer dereference", - expr.find_source_location(), - expr, - guard); - - if(flags.is_unknown() || - flags.is_dynamic_heap()) - { - const or_exprt dynamic_bounds( - dynamic_object_lower_bound(pointer, ns, access_lb), - dynamic_object_upper_bound(pointer, ns, access_ub)); - - add_guarded_claim( - or_exprt( - allocs, - implies_exprt( - malloc_object(pointer, ns), - not_exprt(dynamic_bounds))), - "dereference failure: pointer outside dynamic object bounds", - "pointer dereference", - expr.find_source_location(), - expr, - guard); - } - - if(flags.is_unknown() || - flags.is_dynamic_local() || - flags.is_static_lifetime()) - { - const or_exprt object_bounds( - object_lower_bound(pointer, ns, access_lb), - object_upper_bound(pointer, ns, access_ub)); - - add_guarded_claim( - or_exprt(allocs, dynamic_object(pointer), not_exprt(object_bounds)), - "dereference failure: pointer outside object bounds", - "pointer dereference", - expr.find_source_location(), - expr, - guard); - } - - if(flags.is_unknown() || - flags.is_integer_address()) - { - add_guarded_claim( - implies_exprt(integer_address(pointer), allocs), - "dereference failure: invalid integer address", - "pointer dereference", - expr.find_source_location(), - expr, - guard); - } + add_guarded_claim( + c.assertion, + "dereference failure: "+c.description, + "pointer dereference", + expr.find_source_location(), + expr, + guard); } } @@ -1207,7 +1052,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size) conditions.push_back(conditiont( implies_exprt(not_exprt(dynamic_object(address)), not_exprt(object_bounds_violation)), - "dereference failure: pointer outside object bounds")); + "pointer outside object bounds")); } if(flags.is_unknown() || flags.is_integer_address()) @@ -1547,24 +1392,39 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address) const dereference_exprt &deref= to_dereference_expr(member.struct_op()); - check_rec(deref.op0(), guard, false); + check_rec(deref.pointer(), guard, false); // avoid building the following expressions when pointer_validity_check // would return immediately anyway if(!enable_pointer_check) return; - exprt access_ub=nil_exprt(); + // we rewrite s->member into *(s+member_offset) + // to avoid requiring memory safety of the entire struct exprt member_offset=member_offset_expr(member, ns); - exprt size=size_of_expr(expr.type(), ns); - if(member_offset.is_not_nil() && size.is_not_nil()) - access_ub=plus_exprt(member_offset, size); + if(member_offset.is_not_nil()) + { + pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type()); + new_pointer_type.subtype() = expr.type(); - pointer_validity_check(deref, guard, member_offset, access_ub); + const exprt char_pointer = + typecast_exprt::conditional_cast( + deref.pointer(), pointer_type(char_type())); - return; + const exprt new_address = typecast_exprt( + plus_exprt(char_pointer, member_offset), char_pointer.type()); + + const exprt new_address_casted = + typecast_exprt::conditional_cast(new_address, new_pointer_type); + + dereference_exprt new_deref(new_address_casted, expr.type()); + new_deref.add_source_location() = deref.source_location(); + pointer_validity_check(new_deref, guard); + + return; + } } forall_operands(it, expr) @@ -1626,11 +1486,9 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address) expr.id()==ID_ge || expr.id()==ID_gt) pointer_rel_check(expr, guard); else if(expr.id()==ID_dereference) - pointer_validity_check( - to_dereference_expr(expr), - guard, - nil_exprt(), - size_of_expr(expr.type(), ns)); + { + pointer_validity_check(to_dereference_expr(expr), guard); + } } void goto_checkt::check(const exprt &expr)