From 2bc9b22b2539d9ece47e298dd1b05433ee9500ff Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 19 Aug 2024 18:58:14 +0000 Subject: [PATCH 1/2] Maintain loop invariant annotation when converting do .. while With the changes in bbd9de4c9f6f7 we newly made do .. while converted instructions subject to `optimize_guarded_gotos`, which previously rewrote conditions without retaining annotations related to loop invariants. The included tests now show that the annotations are preserved, but still fail for an unrelated bug in how do .. while loops are instrumented. --- .../loop_contracts_do_while/assigns.c | 19 +++++++++++++++ .../loop_contracts_do_while/assigns.desc | 9 +++++++ .../loop_contracts_do_while/main.c | 2 +- .../loop_contracts_do_while/side_effect.c | 24 +++++++++++++++++++ .../loop_contracts_do_while/side_effect.desc | 9 +++++++ .../loop_contracts_do_while/test.desc | 2 +- .../loop_contracts_do_while/test.desc | 3 ++- src/ansi-c/goto-conversion/goto_convert.cpp | 21 ++++++++++++++-- 8 files changed, 84 insertions(+), 5 deletions(-) create mode 100644 regression/contracts-dfcc/loop_contracts_do_while/assigns.c create mode 100644 regression/contracts-dfcc/loop_contracts_do_while/assigns.desc create mode 100644 regression/contracts-dfcc/loop_contracts_do_while/side_effect.c create mode 100644 regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc diff --git a/regression/contracts-dfcc/loop_contracts_do_while/assigns.c b/regression/contracts-dfcc/loop_contracts_do_while/assigns.c new file mode 100644 index 00000000000..982f5dd55f3 --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_do_while/assigns.c @@ -0,0 +1,19 @@ +int global; + +int main() +{ + global = 0; + int argc = 1; + if(argc > 1) + { + do + __CPROVER_assigns(global) + { + global = 1; + } + while(0); + } + __CPROVER_assert(global == 0, "should be zero"); + + return 0; +} diff --git a/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc b/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc new file mode 100644 index 00000000000..7149815c6d9 --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc @@ -0,0 +1,9 @@ +KNOWNBUG +assigns.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that loop contracts work correctly on do/while loops. diff --git a/regression/contracts-dfcc/loop_contracts_do_while/main.c b/regression/contracts-dfcc/loop_contracts_do_while/main.c index 8519d3953fb..6cdce8ce510 100644 --- a/regression/contracts-dfcc/loop_contracts_do_while/main.c +++ b/regression/contracts-dfcc/loop_contracts_do_while/main.c @@ -5,7 +5,7 @@ int main() int x = 0; do - __CPROVER_loop_invariant(0 <= x && x <= 10) + __CPROVER_loop_invariant(0 <= x && x < 10) { x++; } diff --git a/regression/contracts-dfcc/loop_contracts_do_while/side_effect.c b/regression/contracts-dfcc/loop_contracts_do_while/side_effect.c new file mode 100644 index 00000000000..2413640f98c --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_do_while/side_effect.c @@ -0,0 +1,24 @@ +int global; + +int foo() +{ + return 0; +} + +int main() +{ + global = 0; + int argc = 1; + if(argc > 1) + { + do + __CPROVER_assigns(global) + { + global = 1; + } + while(foo()); + } + __CPROVER_assert(global == 0, "should be zero"); + + return 0; +} diff --git a/regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc b/regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc new file mode 100644 index 00000000000..6f9b34dd89c --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc @@ -0,0 +1,9 @@ +KNOWNBUG +side_effect.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that loop contracts work correctly on do/while loops. diff --git a/regression/contracts-dfcc/loop_contracts_do_while/test.desc b/regression/contracts-dfcc/loop_contracts_do_while/test.desc index dbe8bafe65d..a5c1706022a 100644 --- a/regression/contracts-dfcc/loop_contracts_do_while/test.desc +++ b/regression/contracts-dfcc/loop_contracts_do_while/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE dfcc-only main.c --dfcc main --apply-loop-contracts ^EXIT=0$ diff --git a/regression/contracts/loop_contracts_do_while/test.desc b/regression/contracts/loop_contracts_do_while/test.desc index 9c52a782fea..b48cda7c0d9 100644 --- a/regression/contracts/loop_contracts_do_while/test.desc +++ b/regression/contracts/loop_contracts_do_while/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --apply-loop-contracts ^EXIT=0$ @@ -7,3 +7,4 @@ main.c -- -- This test checks that loop contracts work correctly on do/while loops. +Fails because contracts are not yet supported on do while loops. diff --git a/src/ansi-c/goto-conversion/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp index c2a2e86ca1d..793fba651c3 100644 --- a/src/ansi-c/goto-conversion/goto_convert.cpp +++ b/src/ansi-c/goto-conversion/goto_convert.cpp @@ -432,8 +432,25 @@ void goto_convertt::optimize_guarded_gotos(goto_programt &dest) // cannot compare iterators, so compare target number instead if(it->get_target()->target_number == it_z->target_number) { + DATA_INVARIANT( + it->condition().find(ID_C_spec_assigns).is_nil() && + it->condition().find(ID_C_spec_loop_invariant).is_nil() && + it->condition().find(ID_C_spec_decreases).is_nil(), + "no loop invariant expected"); + irept y_assigns = it_goto_y->condition().find(ID_C_spec_assigns); + irept y_loop_invariant = + it_goto_y->condition().find(ID_C_spec_loop_invariant); + irept y_decreases = it_goto_y->condition().find(ID_C_spec_decreases); + it->set_target(it_goto_y->get_target()); - it->condition_nonconst() = boolean_negate(it->condition()); + exprt updated_condition = boolean_negate(it->condition()); + if(y_assigns.is_not_nil()) + updated_condition.add(ID_C_spec_assigns).swap(y_assigns); + if(y_loop_invariant.is_not_nil()) + updated_condition.add(ID_C_spec_loop_invariant).swap(y_loop_invariant); + if(y_decreases.is_not_nil()) + updated_condition.add(ID_C_spec_decreases).swap(y_decreases); + it->condition_nonconst() = updated_condition; it_goto_y->turn_into_skip(); } } @@ -1301,7 +1318,7 @@ void goto_convertt::convert_dowhile( W->complete_goto(w); // assigns_clause, loop invariant and decreases clause - convert_loop_contracts(code, y); + convert_loop_contracts(code, W); dest.destructive_append(tmp_w); dest.destructive_append(side_effects.side_effects); From 6009066d46d6ce400cefaff99937055846521732 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 20 Aug 2024 07:18:38 +0000 Subject: [PATCH 2/2] Contracts/insert_before_and_update_jumps: only update jump edge The incoming edge from a `goto` instruction may also be the non-branching case, which must not result in redirecting this goto. --- regression/contracts-dfcc/loop_contracts_do_while/assigns.desc | 2 +- .../contracts-dfcc/loop_contracts_do_while/side_effect.desc | 2 +- src/goto-instrument/contracts/utils.cpp | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc b/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc index 7149815c6d9..4fe2cf25dde 100644 --- a/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc +++ b/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE dfcc-only assigns.c --dfcc main --apply-loop-contracts ^EXIT=0$ diff --git a/regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc b/regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc index 6f9b34dd89c..6306416f3bf 100644 --- a/regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc +++ b/regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE dfcc-only side_effect.c --dfcc main --apply-loop-contracts ^EXIT=0$ diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 803cf47eb6a..6dd6cf7e681 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -250,7 +250,7 @@ void insert_before_and_update_jumps( const auto new_target = destination.insert_before(target, i); for(auto it : target->incoming_edges) { - if(it->is_goto()) + if(it->is_goto() && it->get_target() == target) it->set_target(new_target); } }