diff --git a/regression/cbmc/pointer-overflow3/no-simplify.desc b/regression/cbmc/pointer-overflow3/no-simplify.desc index 6a6134eb02b..8fe7cdb48f8 100644 --- a/regression/cbmc/pointer-overflow3/no-simplify.desc +++ b/regression/cbmc/pointer-overflow3/no-simplify.desc @@ -5,7 +5,9 @@ main.c ^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside object bounds in p - \(signed (long (long )?)?int\)10: FAILURE ^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ \(signed (long (long )?)?int\)10: FAILURE ^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr - \(signed (long (long )?)?int\)10: FAILURE -^\*\* 4 of \d+ failed +^\[main.overflow.\d+\] line 7 arithmetic overflow on pointer \- in p \- \(signed (long (long )?)?int\)10: FAILURE +^\[main.overflow.\d+\] line 11 arithmetic overflow on pointer \- in arr \- \(signed (long (long )?)?int\)10: FAILURE +^\*\* 6 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/pointer-overflow3/test.desc b/regression/cbmc/pointer-overflow3/test.desc index a82964bcaa3..29faa065b45 100644 --- a/regression/cbmc/pointer-overflow3/test.desc +++ b/regression/cbmc/pointer-overflow3/test.desc @@ -5,7 +5,9 @@ main.c ^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside object bounds in p - \(signed (long (long )?)?int\)10: FAILURE ^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ \(signed (long (long )?)?int\)10: FAILURE ^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr - \(signed (long (long )?)?int\)10: FAILURE -^\*\* 4 of \d+ failed +^\[main.overflow.\d+\] line 7 arithmetic overflow on pointer \- in p \- \(signed (long (long )?)?int\)10: FAILURE +^\[main.overflow.\d+\] line 11 arithmetic overflow on pointer \- in arr \- \(signed (long (long )?)?int\)10: FAILURE +^\*\* 6 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/pointer-overflow4/test.desc b/regression/cbmc/pointer-overflow4/test.desc index 0c24bc9b6df..eb04ae28e5e 100644 --- a/regression/cbmc/pointer-overflow4/test.desc +++ b/regression/cbmc/pointer-overflow4/test.desc @@ -1,7 +1,7 @@ CORE main.c --pointer-overflow-check -^\[main.overflow.1\] line 10 arithmetic overflow on signed \* in (0x)?[0-9a-fA-F]+l* \* \(signed (long (long )?)?int\)4ul*: FAILURE$ +^\[main.overflow.1\] line 10 arithmetic overflow on pointer \+ in p \+ (0x)?[0-9a-fA-F]+l*: FAILURE$ ^\*\* 1 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ diff --git a/regression/contracts/no_redudant_checks/test.desc b/regression/contracts/no_redudant_checks/test.desc index c2100ee2a71..34a7df2ea02 100644 --- a/regression/contracts/no_redudant_checks/test.desc +++ b/regression/contracts/no_redudant_checks/test.desc @@ -23,7 +23,7 @@ main.c ^\[main.pointer_arithmetic.15\].*: SUCCESS ^\[main.pointer_arithmetic.16\].*: SUCCESS ^\[main.pointer_arithmetic.17\].*: SUCCESS -^\*\* 0 of 20 failed \(1 iterations\) +^\*\* 0 of 23 failed \(1 iterations\) ^VERIFICATION SUCCESSFUL$ -- ^\[main.overflow.\d+\].*: FAILURE @@ -32,10 +32,10 @@ Checks that assertions generated by the first --pointer-overflow-check: - do not get duplicated by the second --unsigned-overflow-check - do not get instrumented with --unsigned-overflow-check (would fail the proof) -We expect 20 assertions to be generated: +We expect 23 assertions to be generated: In the goto-instrument run: - 2 for using malloc -- 17 caused by --pointer-overflow-check +- 20 caused by --pointer-overflow-check In the final cbmc run: - 0 caused by --pointer-overflow-check diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 7a3762c1a04..76c2f1bf6c2 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -819,9 +819,6 @@ void goto_check_ct::integer_overflow_check( const exprt &expr, const guardt &guard) { - if(!enable_signed_overflow_check && !enable_unsigned_overflow_check) - return; - // First, check type. const typet &type = expr.type(); @@ -831,6 +828,9 @@ void goto_check_ct::integer_overflow_check( if(type.id() == ID_unsignedbv && !enable_unsigned_overflow_check) return; + if(type.id() == ID_pointer && !enable_pointer_overflow_check) + return; + // add overflow subgoal if(expr.id() == ID_div) @@ -1021,7 +1021,10 @@ void goto_check_ct::integer_overflow_check( tmp.operands().resize(i); } - std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed"; + std::string kind = + type.id() == ID_pointer + ? "pointer" + : (type.id() == ID_unsignedbv ? "unsigned" : "signed"); add_guarded_property( not_exprt{binary_overflow_exprt{tmp, expr.id(), expr.operands()[i]}}, @@ -1034,7 +1037,9 @@ void goto_check_ct::integer_overflow_check( } else if(expr.operands().size() == 2) { - std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed"; + std::string kind = type.id() == ID_pointer + ? "pointer" + : (type.id() == ID_unsignedbv ? "unsigned" : "signed"); const binary_exprt &bexpr = to_binary_expr(expr); add_guarded_property( @@ -1335,31 +1340,7 @@ void goto_check_ct::pointer_overflow_check( expr.operands().size() == 2, "pointer arithmetic expected to have exactly 2 operands"); - // multiplying the offset by the object size must not result in arithmetic - // overflow - const typet &object_type = to_pointer_type(expr.type()).base_type(); - if(object_type.id() != ID_empty) - { - auto size_of_expr_opt = size_of_expr(object_type, ns); - CHECK_RETURN(size_of_expr_opt.has_value()); - exprt object_size = size_of_expr_opt.value(); - - const binary_exprt &binary_expr = to_binary_expr(expr); - exprt offset_operand = binary_expr.lhs().type().id() == ID_pointer - ? binary_expr.rhs() - : binary_expr.lhs(); - mult_exprt mul{ - offset_operand, - typecast_exprt::conditional_cast(object_size, offset_operand.type())}; - mul.add_source_location() = offset_operand.source_location(); - - flag_overridet override_overflow(offset_operand.source_location()); - override_overflow.set_flag( - enable_signed_overflow_check, true, "signed_overflow_check"); - override_overflow.set_flag( - enable_unsigned_overflow_check, true, "unsigned_overflow_check"); - integer_overflow_check(mul, guard); - } + integer_overflow_check(expr, guard); // the result must be within object bounds or one past the end const auto size = from_integer(0, size_type()); diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index dbe0fb43f75..ef5f008c3e8 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -449,6 +449,7 @@ inline char *getenv(const char *name) // the range. __CPROVER_assume(buf_size >= 1); + __CPROVER_assume((__CPROVER_size_t)buf_size <= __CPROVER_max_malloc_size); char *buffer = (char *)__CPROVER_allocate(buf_size * sizeof(char), 0); buffer[buf_size-1]=0; diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 86f0361cb89..2bf32873fe7 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "bv_pointers.h" #include +#include #include #include #include @@ -204,6 +205,79 @@ literalt bv_pointerst::convert_rest(const exprt &expr) bv_utilst::representationt::SIGNED)); } } + else if( + (expr.id() == ID_overflow_plus || expr.id() == ID_overflow_minus) && + operands.size() == 2 && + (operands[0].type().id() == ID_pointer) != + (operands[1].type().id() == ID_pointer)) + { + // this has to be pointer plus/minus integer + const exprt &pointer_op = + operands[0].type().id() == ID_pointer ? operands[0] : operands[1]; + const pointer_typet &pointer_type = to_pointer_type(pointer_op.type()); + const typet &object_type = pointer_type.base_type(); + + const exprt &offset_op = + operands[0].type().id() == ID_pointer ? operands[1] : operands[0]; + if( + offset_op.type().id() != ID_unsignedbv && + offset_op.type().id() != ID_signedbv) + { + return SUB::convert_rest(expr); + } + exprt offset_bytes = offset_op; + literalt offset_overflow = const_literal(false); + + // Arithmetic over void* is a gcc extension. + // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html + if(object_type.id() != ID_empty) + { + auto object_size_opt = size_of_expr(object_type, ns); + CHECK_RETURN(object_size_opt.has_value()); + + offset_bytes = mult_exprt{ + offset_op, + typecast_exprt::conditional_cast(*object_size_opt, offset_op.type())}; + + // multiplying the offset by the object size may result in arithmetic + // overflow + mult_overflow_exprt of{ + to_mult_expr(offset_bytes).op0(), to_mult_expr(offset_bytes).op1()}; + offset_overflow = convert(of); + } + + const std::size_t full_width = pointer_type.get_width(); + + bv_utilst::representationt rep = offset_bytes.type().id() == ID_signedbv + ? bv_utilst::representationt::SIGNED + : bv_utilst::representationt::UNSIGNED; + bvt offset_bv = convert_bv(offset_bytes); + CHECK_RETURN(!offset_bv.empty()); + offset_bv = bv_utils.extension(offset_bv, full_width, rep); + if(expr.id() == ID_overflow_minus) + offset_bv = bv_utils.negate(offset_bv); + + bvt pointer_offset_bv = bv_utils.sign_extension( + offset_literals(convert_bv(pointer_op), pointer_type), full_width); + + // add and determine (signed) overflow of this addition + bvt offset_sum = bv_utils.add(pointer_offset_bv, offset_bv); + literalt addition_overflow = prop.land( + prop.lequal( + bv_utils.sign_bit(pointer_offset_bv), bv_utils.sign_bit(offset_bv)), + prop.lxor( + bv_utils.sign_bit(offset_sum), bv_utils.sign_bit(pointer_offset_bv))); + + // there is an overflow iff any of [offset width - 1 .. full_width - 1] bits + // are non-zero or there was an overflow in the addition or the earlier + // multiplication + const std::size_t offset_bits = get_offset_width(pointer_type); + CHECK_RETURN(offset_bits > 0); + offset_sum.erase(offset_sum.begin(), offset_sum.begin() + offset_bits - 1); + offset_sum.push_back(addition_overflow); + offset_sum.push_back(offset_overflow); + return prop.lor(offset_sum); + } return SUB::convert_rest(expr); } diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 874ad8fb05c..54d351147c9 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1878,7 +1878,52 @@ void smt2_convt::convert_expr(const exprt &expr) const typet &op_type = op0.type(); std::size_t width=boolbv_width(op_type); - if(op_type.id()==ID_signedbv) + if(op0.type().id() == ID_pointer || op1.type().id() == ID_pointer) + { + exprt p = op0, i = op1; + + if(p.type().id() != ID_pointer) + p.swap(i); + + const auto &object_type = to_pointer_type(p.type()).base_type(); + exprt offset_bytes = i; + exprt::operandst disjuncts; + + // Arithmetic over void* is a gcc extension. + // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html + if(object_type.id() != ID_empty) + { + auto object_size_opt = size_of_expr(object_type, ns); + CHECK_RETURN(object_size_opt.has_value()); + + offset_bytes = mult_exprt{ + i, typecast_exprt::conditional_cast(*object_size_opt, i.type())}; + + // multiplying the offset by the object size may result in arithmetic + // overflow + disjuncts.push_back(mult_overflow_exprt{ + to_mult_expr(offset_bytes).op0(), to_mult_expr(offset_bytes).op1()}); + } + + exprt pointer_offset_op = pointer_offset(p); + offset_bytes = typecast_exprt::conditional_cast( + offset_bytes, pointer_offset_op.type()); + + if(can_cast_expr(expr)) + offset_bytes = unary_minus_exprt{offset_bytes}; + + disjuncts.push_back(plus_overflow_exprt{pointer_offset_op, offset_bytes}); + + plus_exprt sum{pointer_offset_op, offset_bytes}; + exprt pointer_offset_sum = pointer_offset(typecast_exprt{sum, p.type()}); + + disjuncts.push_back(binary_relation_exprt{ + pointer_offset_sum, ID_lt, from_integer(0, pointer_offset_sum.type())}); + disjuncts.push_back(notequal_exprt{pointer_offset_sum, sum}); + + convert_expr(disjunction(disjuncts)); + } + else if(op_type.id() == ID_signedbv) { // an overflow occurs if the top two bits of the extended sum differ out << "(let ((?sum ("; @@ -1894,8 +1939,7 @@ void smt2_convt::convert_expr(const exprt &expr) "((_ extract " << (width-1) << " " << (width-1) << ") ?sum)"; out << ")))"; // =, not, let } - else if(op_type.id()==ID_unsignedbv || - op_type.id()==ID_pointer) + else if(op_type.id() == ID_unsignedbv) { // overflow is simply carry-out out << "(= ";