From 120f525304825c44ea6ce022eb2fb7316c250388 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 30 Jan 2022 21:46:33 +0000 Subject: [PATCH 1/2] 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 25d3a9c2b4955c59111bb1d58b34fef132bd57ea Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 30 Jan 2022 16:58:52 +0000 Subject: [PATCH 2/2] 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