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/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/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index eb519905b70..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 @@ -86,23 +87,34 @@ class goto_checkt bool address); void check(const exprt &expr); - 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 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); - - std::string array_name(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 &, 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 &, 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 &); void add_guarded_claim( const exprt &expr, @@ -139,6 +151,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; @@ -918,177 +932,137 @@ 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())); + const exprt &pointer=expr.pointer(); + + auto conditions = + address_check(pointer, size_of_expr(expr.type(), ns)); + + for(const auto &c : conditions) + { + add_guarded_claim( + c.assertion, + "dereference failure: "+c.description, + "pointer dereference", + expr.find_source_location(), + expr, + guard); + } +} + +goto_checkt::conditionst +goto_checkt::address_check(const exprt &address, const exprt &size) +{ + if(!enable_pointer_check) + return {}; - assert(base_type_eq(pointer_type.subtype(), expr.type(), ns)); + 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, pointer); + 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(mode == ID_java) { if(flags.is_unknown() || flags.is_null()) { - notequal_exprt not_eq_null(pointer, null_pointer_exprt(pointer_type)); + notequal_exprt not_eq_null(address, null_pointer_exprt(pointer_type)); - add_guarded_claim( - not_eq_null, - "reference is null", - "pointer dereference", - expr.find_source_location(), - expr, - guard); + return {conditiont(not_eq_null, "reference is null")}; } + else + return {}; } else { - exprt allocs=false_exprt(); + conditionst conditions; + exprt::operandst alloc_disjuncts; - if(!allocations.empty()) + for(const auto &a : allocations) { - 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); - } + typecast_exprt int_ptr(address, a.first.type()); - 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 lb_check(a.first, ID_le, int_ptr); - binary_relation_exprt ub_check( - ub, ID_le, plus_exprt(a.first, a.second)); + plus_exprt ub(int_ptr, size, int_ptr.type()); - disjuncts.push_back(and_exprt(lb_check, ub_check)); - } + binary_relation_exprt ub_check(ub, ID_le, plus_exprt(a.first, a.second)); - allocs=disjunction(disjuncts); + alloc_disjuncts.push_back(and_exprt(lb_check, ub_check)); } - if(flags.is_unknown() || - flags.is_null()) + const exprt allocs = disjunction(alloc_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); + conditions.push_back(conditiont( + or_exprt(allocs, not_exprt(null_pointer(address))), "pointer NULL")); } 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); + { + conditions.push_back(conditiont( + not_exprt(invalid_pointer(address)), + "pointer invalid")); + } 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); + { + conditions.push_back(conditiont( + or_exprt(allocs, not_exprt(invalid_pointer(address))), + "pointer uninitialized")); + } - 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_heap()) + { + conditions.push_back(conditiont( + not_exprt(deallocated(address, ns)), + "deallocated dynamic object")); + } - 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_local()) + { + conditions.push_back(conditiont( + not_exprt(dead_object(address, ns)), "dead object")); + } - if(flags.is_unknown() || - flags.is_dynamic_heap()) + 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)); + const or_exprt dynamic_bounds_violation( + dynamic_object_lower_bound(address, ns, nil_exprt()), + dynamic_object_upper_bound(address, ns, size)); - 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); + 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()) + 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)); + const or_exprt object_bounds_violation( + object_lower_bound(address, ns, nil_exprt()), + object_upper_bound(address, ns, size)); - 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); + conditions.push_back(conditiont( + implies_exprt(not_exprt(dynamic_object(address)), not_exprt(object_bounds_violation)), + "pointer outside object bounds")); } - if(flags.is_unknown() || - flags.is_integer_address()) + 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); + conditions.push_back(conditiont( + implies_exprt(integer_address(address), allocs), + "invalid integer address")); } + + return conditions; } } @@ -1418,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) @@ -1497,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) @@ -1510,6 +1497,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 +1667,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)) 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/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--) { 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