From 1f977102977777f78eb36109401c1eb616ceb0ee Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 30 Jan 2022 21:46:33 +0000 Subject: [PATCH 1/3] C front-end: pragma conflict checking must handle empty stack We do not necessarily have any pragmas set, and therefore must be able to handle an empty stack. Surprisingly, this only seg faulted when building in exactly the way check-ubuntu-20_04-make-gcc is doing this in CI, and only on one test added in the next commit. --- src/ansi-c/ansi_c_parser.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ansi-c/ansi_c_parser.cpp b/src/ansi-c/ansi_c_parser.cpp index 5e90ccbf56a..ad88cb68841 100644 --- a/src/ansi-c/ansi_c_parser.cpp +++ b/src/ansi-c/ansi_c_parser.cpp @@ -203,6 +203,9 @@ void ansi_c_parsert::pragma_cprover_add_check( bool ansi_c_parsert::pragma_cprover_clash(const irep_idt &name, bool enabled) { + if(pragma_cprover_stack.empty()) + return false; + auto top = pragma_cprover_stack.back(); auto found = top.find(name); return found != top.end() && found->second != enabled; From f38294f4f3719a136cc9a28e9fc43e26f64ac01d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 30 Jan 2022 16:58:52 +0000 Subject: [PATCH 2/3] goto_check_c: observe check pragmas annotated to individual expressions This is required to make the conversion of __builtin_X_overflow not generate spurious conversion checks. Fixes: #6452 --- .../conversion-check.c | 10 +++++++ .../conversion-check.desc | 10 +++++++ regression/cbmc/pragma_cprover4/main.c | 22 +++++++++++++++ regression/cbmc/pragma_cprover4/test.desc | 13 +++++++++ src/analyses/goto_check_c.cpp | 27 +++++++++++++++++++ .../goto_convert_side_effect.cpp | 9 ++++--- 6 files changed, 88 insertions(+), 3 deletions(-) create mode 100644 regression/cbmc/gcc_builtin_add_overflow/conversion-check.c create mode 100644 regression/cbmc/gcc_builtin_add_overflow/conversion-check.desc create mode 100644 regression/cbmc/pragma_cprover4/main.c create mode 100644 regression/cbmc/pragma_cprover4/test.desc diff --git a/regression/cbmc/gcc_builtin_add_overflow/conversion-check.c b/regression/cbmc/gcc_builtin_add_overflow/conversion-check.c new file mode 100644 index 00000000000..0d03e24fb56 --- /dev/null +++ b/regression/cbmc/gcc_builtin_add_overflow/conversion-check.c @@ -0,0 +1,10 @@ +#ifndef __GNUC__ +_Bool __builtin_add_overflow(); +#endif + +int main() +{ + unsigned a, b, c; + if(__builtin_add_overflow(a, b, &c)) + return 0; +} diff --git a/regression/cbmc/gcc_builtin_add_overflow/conversion-check.desc b/regression/cbmc/gcc_builtin_add_overflow/conversion-check.desc new file mode 100644 index 00000000000..d601d8b4c24 --- /dev/null +++ b/regression/cbmc/gcc_builtin_add_overflow/conversion-check.desc @@ -0,0 +1,10 @@ +CORE +conversion-check.c +--conversion-check --unsigned-overflow-check --signed-overflow-check +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^Generated [1-9]\d* VCC\(s\) +-- +Zero VCCs should be generated. diff --git a/regression/cbmc/pragma_cprover4/main.c b/regression/cbmc/pragma_cprover4/main.c new file mode 100644 index 00000000000..193dfd9d986 --- /dev/null +++ b/regression/cbmc/pragma_cprover4/main.c @@ -0,0 +1,22 @@ +#include + +int nondet_int(); + +void main() +{ + int a = nondet_int(); + int b = nondet_int(); + int c = a + +#pragma CPROVER check disable "signed-overflow" + (a + b); +#pragma CPROVER check pop + +#pragma CPROVER check disable "signed-overflow" + for(int i = 0; i < 10; ++i) + { + int temp = a + b; +#pragma CPROVER check pop + int foo = temp + a; + assert(foo > 2); + } +} diff --git a/regression/cbmc/pragma_cprover4/test.desc b/regression/cbmc/pragma_cprover4/test.desc new file mode 100644 index 00000000000..45d63b42913 --- /dev/null +++ b/regression/cbmc/pragma_cprover4/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--signed-overflow-check +^\[main.overflow.1\] line 9 arithmetic overflow on signed \+ in a \+ a \+ b: FAILURE$ +^\[main.overflow.2\] line 19 arithmetic overflow on signed \+ in temp \+ a: FAILURE$ +^\[main.assertion.1\] line 20 assertion foo > 2: FAILURE$ +^\*\* 3 of 3 failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +No assertions other than the above three are expected. diff --git a/src/analyses/goto_check_c.cpp b/src/analyses/goto_check_c.cpp index d07bbbd7b34..0b4afc6f315 100644 --- a/src/analyses/goto_check_c.cpp +++ b/src/analyses/goto_check_c.cpp @@ -1895,6 +1895,33 @@ void goto_check_ct::check_rec_arithmetic_op( void goto_check_ct::check_rec(const exprt &expr, const guardt &guard) { + flag_overridet resetter(expr.source_location()); + const auto &pragmas = expr.source_location().get_pragmas(); + for(const auto &d : pragmas) + { + // match named-check related pragmas + auto matched = match_named_check(d.first); + if(matched.has_value()) + { + auto named_check = matched.value(); + auto name = named_check.first; + auto status = named_check.second; + bool *flag = name_to_flag.find(name)->second; + switch(status) + { + case check_statust::ENABLE: + resetter.set_flag(*flag, true, name); + break; + case check_statust::DISABLE: + resetter.set_flag(*flag, false, name); + break; + case check_statust::CHECKED: + resetter.disable_flag(*flag, name); + break; + } + } + } + if(expr.id() == ID_exists || expr.id() == ID_forall) { // the scoped variables may be used in the assertion diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index 2a5785b1eb9..e88ea5c692a 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -656,9 +656,12 @@ void goto_convertt::remove_overflow( if(result.type().id() == ID_pointer) { result_type = to_pointer_type(result.type()).base_type(); - code_assignt result_assignment{dereference_exprt{result}, - typecast_exprt{operation, *result_type}, - expr.source_location()}; + source_locationt source_location_annotated = expr.source_location(); + source_location_annotated.add_pragma("disable:conversion-check"); + code_assignt result_assignment{ + dereference_exprt{result}, + typecast_exprt{operation, *result_type}, + source_location_annotated}; convert_assign(result_assignment, dest, mode); } else From 29d63d3e73356b8f9dab348fed10dfc9034f2aff Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 10 Feb 2022 14:58:01 +0000 Subject: [PATCH 3/3] Expanding __CPROVER_{r,w,rw}_ok must not introduce overflow Distributing signed-to-unsigned type casts over addition can result in an unsigned overflow where previously there was no overflow. That's ok at the logic level for any expressions yield the same models. We just need to make sure that expressions generated are not subject to goto_check_ct generating additional checks: goto_check_ct generates C language checks, not ones for internally generated expressions. --- regression/contracts/simplify-overflow/main.c | 9 +++++++++ regression/contracts/simplify-overflow/test.desc | 13 +++++++++++++ src/analyses/goto_check_c.cpp | 4 ++++ 3 files changed, 26 insertions(+) create mode 100644 regression/contracts/simplify-overflow/main.c create mode 100644 regression/contracts/simplify-overflow/test.desc diff --git a/regression/contracts/simplify-overflow/main.c b/regression/contracts/simplify-overflow/main.c new file mode 100644 index 00000000000..4929b9e9c56 --- /dev/null +++ b/regression/contracts/simplify-overflow/main.c @@ -0,0 +1,9 @@ +int main() +{ + char buf[10]; + __CPROVER_size_t max = 9; + __CPROVER_size_t start = 1; + + __CPROVER_assert( + __CPROVER_r_ok(buf + start, max - start), "array is readable"); +} diff --git a/regression/contracts/simplify-overflow/test.desc b/regression/contracts/simplify-overflow/test.desc new file mode 100644 index 00000000000..fe21afc0216 --- /dev/null +++ b/regression/contracts/simplify-overflow/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--nan-check _ --signed-overflow-check --unsigned-overflow-check +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This test doesn't actually use contracts, but rather demonstrates the workflow +of having goto-instrument expand __CPROVER_r_ok (but really doing nothing else) +before CBMC when may add (overflow) checks. Doing so must not result in failing +assertions that would not have failed on the original input. diff --git a/src/analyses/goto_check_c.cpp b/src/analyses/goto_check_c.cpp index 0b4afc6f315..fbb1bf5c9e8 100644 --- a/src/analyses/goto_check_c.cpp +++ b/src/analyses/goto_check_c.cpp @@ -2047,6 +2047,10 @@ optionalt goto_check_ct::rw_ok_check(exprt expr) exprt c = conjunction(conjuncts); if(enable_simplify) simplify(c, ns); + + // this is a logic expression, C language checks no longer apply + add_all_disable_named_check_pragmas(c.add_source_location()); + return c; } else if(modified)