From d70c7c79825d06d07801584829d7acd2de1194a9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 24 May 2022 12:56:47 +0000 Subject: [PATCH] Support overflow plus/minus expressions over pointers We did not specify that using overflow+/overflow- for pointer +/- integer was unsupported. The translation via regular arithmetic overflow, however, would produce results that did not take into account the peculiarities of pointer arithmetic. Fixing this now also makes it possible to take into account the implementation details of the object/offset encoding, which would result in overflows even when full-width addition/subtraction would not have overflowed. Fixes: #6842 --- .../cbmc/pointer-overflow3/no-simplify.desc | 4 +- regression/cbmc/pointer-overflow3/test.desc | 4 +- regression/cbmc/pointer-overflow4/test.desc | 2 +- .../contracts/no_redudant_checks/test.desc | 6 +- src/ansi-c/goto_check_c.cpp | 41 +++------- src/ansi-c/library/stdlib.c | 1 + src/solvers/flattening/bv_pointers.cpp | 74 +++++++++++++++++++ src/solvers/smt2/smt2_conv.cpp | 50 ++++++++++++- 8 files changed, 143 insertions(+), 39 deletions(-) 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 << "(= ";