From bbd9de4c9f6f70c1be3712fb71f0d0cadf725475 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 28 Jun 2024 15:29:37 +0000 Subject: [PATCH 1/2] GOTO conversion: create temporaries with minimal scope GOTO conversion introduces temporaries when cleaning expression, e.g., removing side effects. We previously considered them to have block scope as they only were marked dead when the block containing them was left. This, however, can be a much larger range of instructions than for what instructions they actually need to be live for. As a consequence, GOTO conversion frequently deemed it necessary to introduce declaration hops for we had goto instructions that would jump over the declaration of the temporary, but still within the block that contained that temporary (and well after the last actual use of that temporary). This PR now largely (with the exception of compound literals, which yield temporaries that must have block scope) removes the side effect that creating temporaries had on scope tracking. Instead, methods explicitly return the list of temporaries in need of cleanup. This avoids performance penalties seen when trying to upgrade Kani to CBMC version 6. Kani makes extensive use of statement expressions, which are one case of instructions that yield a temporary that needs to be cleaned up as soon as possible. --- regression/cbmc-cover/location14/test.desc | 5 +- .../loop_contracts_do_while/test.desc | 3 +- .../cprover/safety/use_after_free1.desc | 2 +- .../branching-ge/test-always-constants.desc | 4 +- .../branching-ge/test-always-intervals.desc | 4 +- .../branching-ge/test-always-value-set.desc | 4 +- .../test-indeterminate-constants.desc | 4 +- .../test-indeterminate-intervals.desc | 4 +- .../test-indeterminate-value-set.desc | 4 +- .../branching-ge/test-never-constants.desc | 4 +- .../branching-ge/test-never-intervals.desc | 4 +- .../branching-ge/test-never-value-set.desc | 4 +- .../branching-gt/test-always-constants.desc | 4 +- .../branching-gt/test-always-intervals.desc | 4 +- .../branching-gt/test-always-value-set.desc | 4 +- .../test-indeterminate-constants.desc | 4 +- .../test-indeterminate-intervals.desc | 4 +- .../test-indeterminate-value-set.desc | 4 +- .../branching-gt/test-never-constants.desc | 4 +- .../branching-gt/test-never-intervals.desc | 4 +- .../branching-gt/test-never-value-set.desc | 4 +- .../branching-le/test-always-constants.desc | 4 +- .../branching-le/test-always-intervals.desc | 4 +- .../branching-le/test-always-value-set.desc | 4 +- .../test-indeterminate-constants.desc | 4 +- .../test-indeterminate-intervals.desc | 4 +- .../test-indeterminate-value-set.desc | 4 +- .../branching-le/test-never-constants.desc | 4 +- .../branching-le/test-never-intervals.desc | 4 +- .../branching-le/test-never-value-set.desc | 4 +- .../branching-lt/test-always-constants.desc | 4 +- .../branching-lt/test-always-intervals.desc | 4 +- .../branching-lt/test-always-value-set.desc | 4 +- .../test-indeterminate-constants.desc | 4 +- .../test-indeterminate-intervals.desc | 4 +- .../test-indeterminate-value-set.desc | 4 +- .../branching-lt/test-never-constants.desc | 4 +- .../branching-lt/test-never-intervals.desc | 4 +- .../branching-lt/test-never-value-set.desc | 4 +- .../with-transform.desc | 2 +- .../without-transform.desc | 2 +- .../region-analysis-14/test.desc | 2 +- .../region-analysis-15/test.desc | 4 +- .../region-analysis-16/test.desc | 2 +- .../abstract_value_object.cpp | 2 +- .../goto-conversion/builtin_functions.cpp | 13 +- src/ansi-c/goto-conversion/destructor.cpp | 34 ++++- src/ansi-c/goto-conversion/destructor.h | 10 ++ .../goto-conversion/goto_clean_expr.cpp | 108 ++++++++----- src/ansi-c/goto-conversion/goto_convert.cpp | 141 ++++++++++++----- .../goto-conversion/goto_convert_class.h | 47 ++++-- .../goto_convert_function_call.cpp | 12 +- .../goto_convert_side_effect.cpp | 142 +++++++++++++----- src/cprover/simplify_state_expr.cpp | 4 + src/goto-instrument/contracts/contracts.cpp | 9 +- .../dfcc_contract_clauses_codegen.cpp | 11 +- .../contracts/instrument_spec_assigns.cpp | 6 +- src/goto-instrument/contracts/utils.h | 5 +- 58 files changed, 484 insertions(+), 226 deletions(-) diff --git a/regression/cbmc-cover/location14/test.desc b/regression/cbmc-cover/location14/test.desc index 7c95cd977c4..f2ffb5c4d1e 100644 --- a/regression/cbmc-cover/location14/test.desc +++ b/regression/cbmc-cover/location14/test.desc @@ -6,8 +6,9 @@ main.c ^\[main.coverage.1\] file main.c line 8 function main block 1.*: SATISFIED$ ^\[main.coverage.2\] file main.c line 12 function main block 2.*: FAILED$ ^\[main.coverage.3\] file main.c line 12 function main block 3.*: FAILED$ -^\[main.coverage.4\] file main.c line 13 function main block 4.*: SATISFIED$ +^\[main.coverage.4\] file main.c line 12 function main block 4.*: FAILED$ +^\[main.coverage.5\] file main.c line 13 function main block 5.*: SATISFIED$ ^\[foo.coverage.1\] file main.c line 3 function foo block 1.*: FAILED$ -^\*\* 2 of 5 covered \(40.0%\) +^\*\* 2 of 6 covered \(33.3%\) -- ^warning: ignoring diff --git a/regression/contracts/loop_contracts_do_while/test.desc b/regression/contracts/loop_contracts_do_while/test.desc index b48cda7c0d9..9c52a782fea 100644 --- a/regression/contracts/loop_contracts_do_while/test.desc +++ b/regression/contracts/loop_contracts_do_while/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --apply-loop-contracts ^EXIT=0$ @@ -7,4 +7,3 @@ 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/regression/cprover/safety/use_after_free1.desc b/regression/cprover/safety/use_after_free1.desc index a2f4b160356..e6cd066a3cd 100644 --- a/regression/cprover/safety/use_after_free1.desc +++ b/regression/cprover/safety/use_after_free1.desc @@ -4,5 +4,5 @@ use_after_free1.c ^EXIT=0$ ^SIGNAL=0$ ^\(\d+\) ∀ ς : state . S11\(ς\) ⇒ S12\(ς\[❝main::\$tmp::return_value_malloc❞:=allocate\(ς, 4\)\]\)$ -^\(\d+\) ∀ ς : state . S15\(ς\) ⇒ S16\(deallocate_state\(ς, cast\(ς\(❝main::1::p❞\), empty\*\)\)\)$ +^\(\d+\) ∀ ς : state . S16\(ς\) ⇒ S17\(deallocate_state\(ς, cast\(ς\(❝main::1::p❞\), empty\*\)\)\)$ -- diff --git a/regression/goto-analyzer/branching-ge/test-always-constants.desc b/regression/goto-analyzer/branching-ge/test-always-constants.desc index fe7cc203863..73167c183a9 100644 --- a/regression/goto-analyzer/branching-ge/test-always-constants.desc +++ b/regression/goto-analyzer/branching-ge/test-always-constants.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[17, 19\] -^main::1::p .* TOP @ \[3, 8, 14\] +^main::1::i .* TOP @ \[23, 25\] +^main::1::p .* TOP @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-ge/test-always-intervals.desc b/regression/goto-analyzer/branching-ge/test-always-intervals.desc index 9a781120569..e35fdffedda 100644 --- a/regression/goto-analyzer/branching-ge/test-always-intervals.desc +++ b/regression/goto-analyzer/branching-ge/test-always-intervals.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[5, 5\] @ \[17\] -^main::1::p .* \[0, A\] @ \[3, 8, 14\] +^main::1::i .* \[5, 5\] @ \[23\] +^main::1::p .* \[0, A\] @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-ge/test-always-value-set.desc b/regression/goto-analyzer/branching-ge/test-always-value-set.desc index 656e57f9b4d..6fa9bae0c29 100644 --- a/regression/goto-analyzer/branching-ge/test-always-value-set.desc +++ b/regression/goto-analyzer/branching-ge/test-always-value-set.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: 5 :value-set-end @ \[17\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\] +^main::1::i .* value-set-begin: 5 :value-set-end @ \[23\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-ge/test-indeterminate-constants.desc b/regression/goto-analyzer/branching-ge/test-indeterminate-constants.desc index 796fb44c24f..c23c3655f5f 100644 --- a/regression/goto-analyzer/branching-ge/test-indeterminate-constants.desc +++ b/regression/goto-analyzer/branching-ge/test-indeterminate-constants.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[17, 19\] -^main::1::p .* TOP @ \[3, 8, 14\] +^main::1::i .* TOP @ \[23, 25\] +^main::1::p .* TOP @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-ge/test-indeterminate-intervals.desc b/regression/goto-analyzer/branching-ge/test-indeterminate-intervals.desc index 1cd97258e06..5313cd50951 100644 --- a/regression/goto-analyzer/branching-ge/test-indeterminate-intervals.desc +++ b/regression/goto-analyzer/branching-ge/test-indeterminate-intervals.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[FFFFFFFB, 5\] @ \[17, 19\] -^main::1::p .* \[0, A\] @ \[3, 8, 14\] +^main::1::i .* \[FFFFFFFB, 5\] @ \[23, 25\] +^main::1::p .* \[0, A\] @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-ge/test-indeterminate-value-set.desc b/regression/goto-analyzer/branching-ge/test-indeterminate-value-set.desc index a6dc611327e..406cd930231 100644 --- a/regression/goto-analyzer/branching-ge/test-indeterminate-value-set.desc +++ b/regression/goto-analyzer/branching-ge/test-indeterminate-value-set.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[17, 19\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\] +^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[23, 25\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-ge/test-never-constants.desc b/regression/goto-analyzer/branching-ge/test-never-constants.desc index c0648a45058..2d1d6df13a0 100644 --- a/regression/goto-analyzer/branching-ge/test-never-constants.desc +++ b/regression/goto-analyzer/branching-ge/test-never-constants.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[17, 19\] -^main::1::p .* TOP @ \[3, 8, 14\] +^main::1::i .* TOP @ \[23, 25\] +^main::1::p .* TOP @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-ge/test-never-intervals.desc b/regression/goto-analyzer/branching-ge/test-never-intervals.desc index 3918aa7b40f..9c31600de4f 100644 --- a/regression/goto-analyzer/branching-ge/test-never-intervals.desc +++ b/regression/goto-analyzer/branching-ge/test-never-intervals.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[19\] -^main::1::p .* \[0, A\] @ \[3, 8, 14\] +^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[25\] +^main::1::p .* \[0, A\] @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-ge/test-never-value-set.desc b/regression/goto-analyzer/branching-ge/test-never-value-set.desc index 281a3a3aedb..f8f2a0aa278 100644 --- a/regression/goto-analyzer/branching-ge/test-never-value-set.desc +++ b/regression/goto-analyzer/branching-ge/test-never-value-set.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: -5 :value-set-end @ \[19\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\] +^main::1::i .* value-set-begin: -5 :value-set-end @ \[25\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-gt/test-always-constants.desc b/regression/goto-analyzer/branching-gt/test-always-constants.desc index fe7cc203863..73167c183a9 100644 --- a/regression/goto-analyzer/branching-gt/test-always-constants.desc +++ b/regression/goto-analyzer/branching-gt/test-always-constants.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[17, 19\] -^main::1::p .* TOP @ \[3, 8, 14\] +^main::1::i .* TOP @ \[23, 25\] +^main::1::p .* TOP @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-gt/test-always-intervals.desc b/regression/goto-analyzer/branching-gt/test-always-intervals.desc index 9a781120569..e35fdffedda 100644 --- a/regression/goto-analyzer/branching-gt/test-always-intervals.desc +++ b/regression/goto-analyzer/branching-gt/test-always-intervals.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[5, 5\] @ \[17\] -^main::1::p .* \[0, A\] @ \[3, 8, 14\] +^main::1::i .* \[5, 5\] @ \[23\] +^main::1::p .* \[0, A\] @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-gt/test-always-value-set.desc b/regression/goto-analyzer/branching-gt/test-always-value-set.desc index 656e57f9b4d..6fa9bae0c29 100644 --- a/regression/goto-analyzer/branching-gt/test-always-value-set.desc +++ b/regression/goto-analyzer/branching-gt/test-always-value-set.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: 5 :value-set-end @ \[17\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\] +^main::1::i .* value-set-begin: 5 :value-set-end @ \[23\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-gt/test-indeterminate-constants.desc b/regression/goto-analyzer/branching-gt/test-indeterminate-constants.desc index 796fb44c24f..c23c3655f5f 100644 --- a/regression/goto-analyzer/branching-gt/test-indeterminate-constants.desc +++ b/regression/goto-analyzer/branching-gt/test-indeterminate-constants.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[17, 19\] -^main::1::p .* TOP @ \[3, 8, 14\] +^main::1::i .* TOP @ \[23, 25\] +^main::1::p .* TOP @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-gt/test-indeterminate-intervals.desc b/regression/goto-analyzer/branching-gt/test-indeterminate-intervals.desc index 1cd97258e06..5313cd50951 100644 --- a/regression/goto-analyzer/branching-gt/test-indeterminate-intervals.desc +++ b/regression/goto-analyzer/branching-gt/test-indeterminate-intervals.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[FFFFFFFB, 5\] @ \[17, 19\] -^main::1::p .* \[0, A\] @ \[3, 8, 14\] +^main::1::i .* \[FFFFFFFB, 5\] @ \[23, 25\] +^main::1::p .* \[0, A\] @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-gt/test-indeterminate-value-set.desc b/regression/goto-analyzer/branching-gt/test-indeterminate-value-set.desc index a6dc611327e..406cd930231 100644 --- a/regression/goto-analyzer/branching-gt/test-indeterminate-value-set.desc +++ b/regression/goto-analyzer/branching-gt/test-indeterminate-value-set.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[17, 19\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\] +^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[23, 25\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-gt/test-never-constants.desc b/regression/goto-analyzer/branching-gt/test-never-constants.desc index c0648a45058..2d1d6df13a0 100644 --- a/regression/goto-analyzer/branching-gt/test-never-constants.desc +++ b/regression/goto-analyzer/branching-gt/test-never-constants.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[17, 19\] -^main::1::p .* TOP @ \[3, 8, 14\] +^main::1::i .* TOP @ \[23, 25\] +^main::1::p .* TOP @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-gt/test-never-intervals.desc b/regression/goto-analyzer/branching-gt/test-never-intervals.desc index 3918aa7b40f..9c31600de4f 100644 --- a/regression/goto-analyzer/branching-gt/test-never-intervals.desc +++ b/regression/goto-analyzer/branching-gt/test-never-intervals.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[19\] -^main::1::p .* \[0, A\] @ \[3, 8, 14\] +^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[25\] +^main::1::p .* \[0, A\] @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-gt/test-never-value-set.desc b/regression/goto-analyzer/branching-gt/test-never-value-set.desc index 281a3a3aedb..f8f2a0aa278 100644 --- a/regression/goto-analyzer/branching-gt/test-never-value-set.desc +++ b/regression/goto-analyzer/branching-gt/test-never-value-set.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: -5 :value-set-end @ \[19\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\] +^main::1::i .* value-set-begin: -5 :value-set-end @ \[25\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-le/test-always-constants.desc b/regression/goto-analyzer/branching-le/test-always-constants.desc index fe7cc203863..73167c183a9 100644 --- a/regression/goto-analyzer/branching-le/test-always-constants.desc +++ b/regression/goto-analyzer/branching-le/test-always-constants.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[17, 19\] -^main::1::p .* TOP @ \[3, 8, 14\] +^main::1::i .* TOP @ \[23, 25\] +^main::1::p .* TOP @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-le/test-always-intervals.desc b/regression/goto-analyzer/branching-le/test-always-intervals.desc index 9a781120569..e35fdffedda 100644 --- a/regression/goto-analyzer/branching-le/test-always-intervals.desc +++ b/regression/goto-analyzer/branching-le/test-always-intervals.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[5, 5\] @ \[17\] -^main::1::p .* \[0, A\] @ \[3, 8, 14\] +^main::1::i .* \[5, 5\] @ \[23\] +^main::1::p .* \[0, A\] @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-le/test-always-value-set.desc b/regression/goto-analyzer/branching-le/test-always-value-set.desc index 656e57f9b4d..6fa9bae0c29 100644 --- a/regression/goto-analyzer/branching-le/test-always-value-set.desc +++ b/regression/goto-analyzer/branching-le/test-always-value-set.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: 5 :value-set-end @ \[17\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\] +^main::1::i .* value-set-begin: 5 :value-set-end @ \[23\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-le/test-indeterminate-constants.desc b/regression/goto-analyzer/branching-le/test-indeterminate-constants.desc index 796fb44c24f..c23c3655f5f 100644 --- a/regression/goto-analyzer/branching-le/test-indeterminate-constants.desc +++ b/regression/goto-analyzer/branching-le/test-indeterminate-constants.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[17, 19\] -^main::1::p .* TOP @ \[3, 8, 14\] +^main::1::i .* TOP @ \[23, 25\] +^main::1::p .* TOP @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-le/test-indeterminate-intervals.desc b/regression/goto-analyzer/branching-le/test-indeterminate-intervals.desc index 1cd97258e06..5313cd50951 100644 --- a/regression/goto-analyzer/branching-le/test-indeterminate-intervals.desc +++ b/regression/goto-analyzer/branching-le/test-indeterminate-intervals.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[FFFFFFFB, 5\] @ \[17, 19\] -^main::1::p .* \[0, A\] @ \[3, 8, 14\] +^main::1::i .* \[FFFFFFFB, 5\] @ \[23, 25\] +^main::1::p .* \[0, A\] @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-le/test-indeterminate-value-set.desc b/regression/goto-analyzer/branching-le/test-indeterminate-value-set.desc index a6dc611327e..406cd930231 100644 --- a/regression/goto-analyzer/branching-le/test-indeterminate-value-set.desc +++ b/regression/goto-analyzer/branching-le/test-indeterminate-value-set.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[17, 19\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\] +^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[23, 25\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-le/test-never-constants.desc b/regression/goto-analyzer/branching-le/test-never-constants.desc index c0648a45058..2d1d6df13a0 100644 --- a/regression/goto-analyzer/branching-le/test-never-constants.desc +++ b/regression/goto-analyzer/branching-le/test-never-constants.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[17, 19\] -^main::1::p .* TOP @ \[3, 8, 14\] +^main::1::i .* TOP @ \[23, 25\] +^main::1::p .* TOP @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-le/test-never-intervals.desc b/regression/goto-analyzer/branching-le/test-never-intervals.desc index 3918aa7b40f..9c31600de4f 100644 --- a/regression/goto-analyzer/branching-le/test-never-intervals.desc +++ b/regression/goto-analyzer/branching-le/test-never-intervals.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[19\] -^main::1::p .* \[0, A\] @ \[3, 8, 14\] +^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[25\] +^main::1::p .* \[0, A\] @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-le/test-never-value-set.desc b/regression/goto-analyzer/branching-le/test-never-value-set.desc index 281a3a3aedb..f8f2a0aa278 100644 --- a/regression/goto-analyzer/branching-le/test-never-value-set.desc +++ b/regression/goto-analyzer/branching-le/test-never-value-set.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: -5 :value-set-end @ \[19\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\] +^main::1::i .* value-set-begin: -5 :value-set-end @ \[25\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-lt/test-always-constants.desc b/regression/goto-analyzer/branching-lt/test-always-constants.desc index fe7cc203863..73167c183a9 100644 --- a/regression/goto-analyzer/branching-lt/test-always-constants.desc +++ b/regression/goto-analyzer/branching-lt/test-always-constants.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[17, 19\] -^main::1::p .* TOP @ \[3, 8, 14\] +^main::1::i .* TOP @ \[23, 25\] +^main::1::p .* TOP @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-lt/test-always-intervals.desc b/regression/goto-analyzer/branching-lt/test-always-intervals.desc index 9a781120569..e35fdffedda 100644 --- a/regression/goto-analyzer/branching-lt/test-always-intervals.desc +++ b/regression/goto-analyzer/branching-lt/test-always-intervals.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[5, 5\] @ \[17\] -^main::1::p .* \[0, A\] @ \[3, 8, 14\] +^main::1::i .* \[5, 5\] @ \[23\] +^main::1::p .* \[0, A\] @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-lt/test-always-value-set.desc b/regression/goto-analyzer/branching-lt/test-always-value-set.desc index 656e57f9b4d..6fa9bae0c29 100644 --- a/regression/goto-analyzer/branching-lt/test-always-value-set.desc +++ b/regression/goto-analyzer/branching-lt/test-always-value-set.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: 5 :value-set-end @ \[17\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\] +^main::1::i .* value-set-begin: 5 :value-set-end @ \[23\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-lt/test-indeterminate-constants.desc b/regression/goto-analyzer/branching-lt/test-indeterminate-constants.desc index 796fb44c24f..c23c3655f5f 100644 --- a/regression/goto-analyzer/branching-lt/test-indeterminate-constants.desc +++ b/regression/goto-analyzer/branching-lt/test-indeterminate-constants.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[17, 19\] -^main::1::p .* TOP @ \[3, 8, 14\] +^main::1::i .* TOP @ \[23, 25\] +^main::1::p .* TOP @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-lt/test-indeterminate-intervals.desc b/regression/goto-analyzer/branching-lt/test-indeterminate-intervals.desc index 1cd97258e06..5313cd50951 100644 --- a/regression/goto-analyzer/branching-lt/test-indeterminate-intervals.desc +++ b/regression/goto-analyzer/branching-lt/test-indeterminate-intervals.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[FFFFFFFB, 5\] @ \[17, 19\] -^main::1::p .* \[0, A\] @ \[3, 8, 14\] +^main::1::i .* \[FFFFFFFB, 5\] @ \[23, 25\] +^main::1::p .* \[0, A\] @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-lt/test-indeterminate-value-set.desc b/regression/goto-analyzer/branching-lt/test-indeterminate-value-set.desc index a6dc611327e..406cd930231 100644 --- a/regression/goto-analyzer/branching-lt/test-indeterminate-value-set.desc +++ b/regression/goto-analyzer/branching-lt/test-indeterminate-value-set.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[17, 19\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\] +^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[23, 25\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-lt/test-never-constants.desc b/regression/goto-analyzer/branching-lt/test-never-constants.desc index c0648a45058..2d1d6df13a0 100644 --- a/regression/goto-analyzer/branching-lt/test-never-constants.desc +++ b/regression/goto-analyzer/branching-lt/test-never-constants.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[17, 19\] -^main::1::p .* TOP @ \[3, 8, 14\] +^main::1::i .* TOP @ \[23, 25\] +^main::1::p .* TOP @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-lt/test-never-intervals.desc b/regression/goto-analyzer/branching-lt/test-never-intervals.desc index 3918aa7b40f..9c31600de4f 100644 --- a/regression/goto-analyzer/branching-lt/test-never-intervals.desc +++ b/regression/goto-analyzer/branching-lt/test-never-intervals.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[19\] -^main::1::p .* \[0, A\] @ \[3, 8, 14\] +^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[25\] +^main::1::p .* \[0, A\] @ \[3, 9, 18\] -- diff --git a/regression/goto-analyzer/branching-lt/test-never-value-set.desc b/regression/goto-analyzer/branching-lt/test-never-value-set.desc index 281a3a3aedb..f8f2a0aa278 100644 --- a/regression/goto-analyzer/branching-lt/test-never-value-set.desc +++ b/regression/goto-analyzer/branching-lt/test-never-value-set.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: -5 :value-set-end @ \[19\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\] +^main::1::i .* value-set-begin: -5 :value-set-end @ \[25\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] -- diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/with-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/with-transform.desc index cce4bb55b58..4df83b91759 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/with-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/with-transform.desc @@ -2,6 +2,6 @@ CORE main.c --ensure-one-backedge-per-target --show-lexical-loops ^3 is head of \{ 3, 4, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26 \(backedge\) \}$ -^16 is head of \{ 16, 17, 22, 23, 24, 25 \(backedge\) \}$ +^17 is head of \{ 17, 18, 22, 23, 24, 25 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/without-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/without-transform.desc index 6a808e9a0e2..3c75bba4947 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/without-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/without-transform.desc @@ -1,7 +1,7 @@ CORE main.c --show-lexical-loops -^16 is head of \{ 16, 17, 22, 23, 24, 25 \(backedge\) \}$ +^17 is head of \{ 17, 18, 22, 23, 24, 25 \(backedge\) \}$ Note not all loops were in lexical loop form ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/region-analysis-14/test.desc b/regression/goto-instrument/region-analysis-14/test.desc index ff87ce2a2e6..a689de8ff78 100644 --- a/regression/goto-instrument/region-analysis-14/test.desc +++ b/regression/goto-instrument/region-analysis-14/test.desc @@ -3,6 +3,6 @@ test.c --show-sese-regions ^Function contains 2 single-entry, single-exit regions:$ ^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(5, [0-9]+\) SKIP$ -^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 2 ends at \(9, [0-9]+\) 3: SKIP$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 2 ends at \(10, [0-9]+\) 3: SKIP$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/region-analysis-15/test.desc b/regression/goto-instrument/region-analysis-15/test.desc index 910291e08be..214c3e45004 100644 --- a/regression/goto-instrument/region-analysis-15/test.desc +++ b/regression/goto-instrument/region-analysis-15/test.desc @@ -2,7 +2,7 @@ CORE test.c --show-sese-regions ^Function contains 2 single-entry, single-exit regions:$ -^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(8, [0-9]+\) 2: SKIP$ -^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(12, [0-9]+\) 4: SKIP$ +^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(9, [0-9]+\) 2: SKIP$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(13, [0-9]+\) 4: SKIP$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/region-analysis-16/test.desc b/regression/goto-instrument/region-analysis-16/test.desc index 92d06f8055b..0ab1668f9bc 100644 --- a/regression/goto-instrument/region-analysis-16/test.desc +++ b/regression/goto-instrument/region-analysis-16/test.desc @@ -3,7 +3,7 @@ test.c --show-sese-regions ^Function contains 3 single-entry, single-exit regions:$ ^Region starting at \(3, [0-9]+\) 1: IF .*7.* THEN GOTO 2 ends at \(8, [0-9]+\) 3: IF .*::x < 10 THEN GOTO 1$ -^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 4 ends at \(13, [0-9]+\) 5: SKIP$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 4 ends at \(14, [0-9]+\) 5: SKIP$ ^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(9, [0-9]+\) SKIP$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/src/analyses/variable-sensitivity/abstract_value_object.cpp b/src/analyses/variable-sensitivity/abstract_value_object.cpp index aa4c94c21c9..2b339a3f5f3 100644 --- a/src/analyses/variable-sensitivity/abstract_value_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_value_object.cpp @@ -438,7 +438,7 @@ class interval_evaluator } INVARIANT( - result.type() == expression.type(), + result.is_top() || result.type() == expression.type(), "Type of result interval should match expression type"); return make_interval(result); } diff --git a/src/ansi-c/goto-conversion/builtin_functions.cpp b/src/ansi-c/goto-conversion/builtin_functions.cpp index dc944e3d964..ea6c30d173d 100644 --- a/src/ansi-c/goto-conversion/builtin_functions.cpp +++ b/src/ansi-c/goto-conversion/builtin_functions.cpp @@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "destructor.h" #include "format_strings.h" void goto_convertt::do_prob_uniform( @@ -400,6 +401,7 @@ void goto_convertt::do_cpp_new( bool new_array = rhs.get(ID_statement) == ID_cpp_new_array; exprt count; + needs_destructiont new_vars; if(new_array) { @@ -407,7 +409,7 @@ void goto_convertt::do_cpp_new( static_cast(rhs.find(ID_size)), object_size.type()); // might have side-effect - clean_expr(count, dest, ID_cpp); + new_vars.add(clean_expr(count, dest, ID_cpp)); } exprt tmp_symbol_expr; @@ -493,6 +495,10 @@ void goto_convertt::do_cpp_new( typecast_exprt(tmp_symbol_expr, lhs.type()), rhs.find_source_location())); + new_vars.minimal_scope.push_front( + to_symbol_expr(tmp_symbol_expr).get_identifier()); + destruct_locals(new_vars.minimal_scope, dest, ns); + // grab initializer goto_programt tmp_initializer; cpp_new_initializer(lhs, rhs, tmp_initializer); @@ -685,6 +691,8 @@ void goto_convertt::do_havoc_slice( codet array_replace(ID_array_replace, {arg0, arg1}, source_location); dest.add(goto_programt::make_other(array_replace, source_location)); + + destruct_locals({nondet_contents.name}, dest, ns); } /// alloca allocates memory that is freed when leaving the function (and not the @@ -773,6 +781,9 @@ void goto_convertt::do_alloca( dest.add(goto_programt::make_assignment( this_alloca_ptr, std::move(rhs), source_location)); + if(lhs.is_nil()) + destruct_locals({to_symbol_expr(new_lhs).get_identifier()}, dest, ns); + // mark pointer to alloca result as dead, unless the alloca result (in // this_alloca_ptr) is still NULL symbol_exprt dead_object_sym = diff --git a/src/ansi-c/goto-conversion/destructor.cpp b/src/ansi-c/goto-conversion/destructor.cpp index e8ce48211c0..330b11003c2 100644 --- a/src/ansi-c/goto-conversion/destructor.cpp +++ b/src/ansi-c/goto-conversion/destructor.cpp @@ -11,10 +11,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "destructor.h" +#include #include #include +#include -#include +#include code_function_callt get_destructor(const namespacet &ns, const typet &type) { @@ -56,3 +58,33 @@ code_function_callt get_destructor(const namespacet &ns, const typet &type) return static_cast(get_nil_irep()); } + +void destruct_locals( + const std::list &vars, + goto_programt &dest, + const namespacet &ns) +{ + for(const auto &id : vars) + { + const symbolt &symbol = ns.lookup(id); + + // do destructor + code_function_callt destructor = get_destructor(ns, symbol.type); + + if(destructor.is_not_nil()) + { + // add "this" + address_of_exprt this_expr( + symbol.symbol_expr(), pointer_type(symbol.type)); + destructor.arguments().push_back(this_expr); + + dest.add(goto_programt::make_function_call( + destructor, destructor.source_location())); + } + + // now create a 'dead' instruction -- will be added after the + // destructor created below as unwind_destructor_stack pops off the + // top of the destructor stack + dest.add(goto_programt::make_dead(symbol.symbol_expr(), symbol.location)); + } +} diff --git a/src/ansi-c/goto-conversion/destructor.h b/src/ansi-c/goto-conversion/destructor.h index 7cfbb594a61..d362135e7d0 100644 --- a/src/ansi-c/goto-conversion/destructor.h +++ b/src/ansi-c/goto-conversion/destructor.h @@ -12,10 +12,20 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H #define CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H +#include + +#include + +class goto_programt; class namespacet; class typet; class code_function_callt get_destructor(const namespacet &ns, const typet &type); +void destruct_locals( + const std::list &vars, + goto_programt &dest, + const namespacet &ns); + #endif // CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp index f8de1cff1ed..d5569bb4b33 100644 --- a/src/ansi-c/goto-conversion/goto_clean_expr.cpp +++ b/src/ansi-c/goto-conversion/goto_clean_expr.cpp @@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "destructor.h" + symbol_exprt goto_convertt::make_compound_literal( const exprt &expr, goto_programt &dest, @@ -164,7 +166,7 @@ void goto_convertt::rewrite_boolean(exprt &expr) expr.swap(tmp); } -void goto_convertt::clean_expr( +goto_convertt::needs_destructiont goto_convertt::clean_expr( exprt &expr, goto_programt &dest, const irep_idt &mode, @@ -179,7 +181,7 @@ void goto_convertt::clean_expr( // compound literals if(!needs_cleaning(expr)) - return; + return {}; if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies) { @@ -187,19 +189,21 @@ void goto_convertt::clean_expr( rewrite_boolean(expr); // recursive call - clean_expr(expr, dest, mode, result_is_used); - return; + return clean_expr(expr, dest, mode, result_is_used); } else if(expr.id() == ID_if) { // first clean condition - clean_expr(to_if_expr(expr).cond(), dest, mode, true); + needs_destructiont new_vars = + clean_expr(to_if_expr(expr).cond(), dest, mode, true); // possibly done now if( !needs_cleaning(to_if_expr(expr).true_case()) && !needs_cleaning(to_if_expr(expr).false_case())) - return; + { + return new_vars; + } // copy expression if_exprt if_expr = to_if_expr(expr); @@ -233,10 +237,12 @@ void goto_convertt::clean_expr( #endif goto_programt tmp_true; - clean_expr(if_expr.true_case(), tmp_true, mode, result_is_used); + new_vars.add( + clean_expr(if_expr.true_case(), tmp_true, mode, result_is_used)); goto_programt tmp_false; - clean_expr(if_expr.false_case(), tmp_false, mode, result_is_used); + new_vars.add( + clean_expr(if_expr.false_case(), tmp_false, mode, result_is_used)); if(result_is_used) { @@ -293,10 +299,18 @@ void goto_convertt::clean_expr( dest, mode); - return; + destruct_locals(new_vars.minimal_scope, dest, ns); + new_vars.minimal_scope.clear(); + + if(expr.is_not_nil()) + new_vars.minimal_scope.push_front(to_symbol_expr(expr).get_identifier()); + + return new_vars; } else if(expr.id() == ID_comma) { + needs_destructiont new_vars; + if(result_is_used) { exprt result; @@ -309,11 +323,11 @@ void goto_convertt::clean_expr( if(last) { result.swap(*it); - clean_expr(result, dest, mode, true); + new_vars.add(clean_expr(result, dest, mode, true)); } else { - clean_expr(*it, dest, mode, false); + new_vars.add(clean_expr(*it, dest, mode, false)); // remember these for later checks if(it->is_not_nil()) @@ -327,7 +341,7 @@ void goto_convertt::clean_expr( { Forall_operands(it, expr) { - clean_expr(*it, dest, mode, false); + new_vars.add(clean_expr(*it, dest, mode, false)); // remember as expression statement for later checks if(it->is_not_nil()) @@ -337,19 +351,20 @@ void goto_convertt::clean_expr( expr = nil_exprt(); } - return; + return new_vars; } else if(expr.id() == ID_typecast) { typecast_exprt &typecast = to_typecast_expr(expr); // preserve 'result_is_used' - clean_expr(typecast.op(), dest, mode, result_is_used); + needs_destructiont new_vars = + clean_expr(typecast.op(), dest, mode, result_is_used); if(typecast.op().is_nil()) expr.make_nil(); - return; + return new_vars; } else if(expr.id() == ID_side_effect) { @@ -359,16 +374,14 @@ void goto_convertt::clean_expr( if(statement == ID_gcc_conditional_expression) { // need to do separately - remove_gcc_conditional_expression(expr, dest, mode); - return; + return remove_gcc_conditional_expression(expr, dest, mode); } else if(statement == ID_statement_expression) { // need to do separately to prevent that // the operands of expr get 'cleaned' - remove_statement_expression( + return remove_statement_expression( to_side_effect_expr(expr), dest, mode, result_is_used); - return; } else if(statement == ID_assign) { @@ -384,17 +397,18 @@ void goto_convertt::clean_expr( to_side_effect_expr(side_effect_assign.rhs()).get_statement() == ID_function_call) { - clean_expr(side_effect_assign.lhs(), dest, mode); + needs_destructiont new_vars = + clean_expr(side_effect_assign.lhs(), dest, mode); exprt lhs = side_effect_assign.lhs(); const bool must_use_rhs = assignment_lhs_needs_temporary(lhs); if(must_use_rhs) { - remove_function_call( + new_vars.add(remove_function_call( to_side_effect_expr_function_call(side_effect_assign.rhs()), dest, mode, - true); + true)); } // turn into code @@ -409,7 +423,8 @@ void goto_convertt::clean_expr( expr = must_use_rhs ? new_rhs : lhs; else expr.make_nil(); - return; + + return new_vars; } } } @@ -422,19 +437,20 @@ void goto_convertt::clean_expr( else if(expr.id() == ID_address_of) { address_of_exprt &addr = to_address_of_expr(expr); - clean_expr_address_of(addr.object(), dest, mode); - return; + return clean_expr_address_of(addr.object(), dest, mode); } + needs_destructiont new_vars; + // TODO: evaluation order Forall_operands(it, expr) - clean_expr(*it, dest, mode); + new_vars.add(clean_expr(*it, dest, mode)); if(expr.id() == ID_side_effect) { - remove_side_effect( - to_side_effect_expr(expr), dest, mode, result_is_used, false); + new_vars.add(remove_side_effect( + to_side_effect_expr(expr), dest, mode, result_is_used, false)); } else if(expr.id() == ID_compound_literal) { @@ -443,13 +459,17 @@ void goto_convertt::clean_expr( expr.operands().size() == 1, "ID_compound_literal has a single operand"); expr = to_unary_expr(expr).op(); } + + return new_vars; } -void goto_convertt::clean_expr_address_of( +goto_convertt::needs_destructiont goto_convertt::clean_expr_address_of( exprt &expr, goto_programt &dest, const irep_idt &mode) { + needs_destructiont new_vars; + // The address of object constructors can be taken, // which is re-written into the address of a variable. @@ -457,7 +477,7 @@ void goto_convertt::clean_expr_address_of( { DATA_INVARIANT( expr.operands().size() == 1, "ID_compound_literal has a single operand"); - clean_expr(to_unary_expr(expr).op(), dest, mode); + new_vars.add(clean_expr(to_unary_expr(expr).op(), dest, mode)); expr = make_compound_literal(to_unary_expr(expr).op(), dest, mode); } else if(expr.id() == ID_string_constant) @@ -468,13 +488,13 @@ void goto_convertt::clean_expr_address_of( else if(expr.id() == ID_index) { index_exprt &index_expr = to_index_expr(expr); - clean_expr_address_of(index_expr.array(), dest, mode); - clean_expr(index_expr.index(), dest, mode); + new_vars.add(clean_expr_address_of(index_expr.array(), dest, mode)); + new_vars.add(clean_expr(index_expr.index(), dest, mode)); } else if(expr.id() == ID_dereference) { dereference_exprt &deref_expr = to_dereference_expr(expr); - clean_expr(deref_expr.pointer(), dest, mode); + new_vars.add(clean_expr(deref_expr.pointer(), dest, mode)); } else if(expr.id() == ID_comma) { @@ -492,7 +512,7 @@ void goto_convertt::clean_expr_address_of( result.swap(*it); else { - clean_expr(*it, dest, mode, false); + new_vars.add(clean_expr(*it, dest, mode, false)); // get any side-effects if(it->is_not_nil()) @@ -503,27 +523,33 @@ void goto_convertt::clean_expr_address_of( expr.swap(result); // do again - clean_expr_address_of(expr, dest, mode); + new_vars.add(clean_expr_address_of(expr, dest, mode)); } else if(expr.id() == ID_side_effect) { - remove_side_effect(to_side_effect_expr(expr), dest, mode, true, true); + new_vars.add( + remove_side_effect(to_side_effect_expr(expr), dest, mode, true, true)); } else Forall_operands(it, expr) - clean_expr_address_of(*it, dest, mode); + new_vars.add(clean_expr_address_of(*it, dest, mode)); + + return new_vars; } -void goto_convertt::remove_gcc_conditional_expression( +goto_convertt::needs_destructiont +goto_convertt::remove_gcc_conditional_expression( exprt &expr, goto_programt &dest, const irep_idt &mode) { + needs_destructiont new_vars; + { auto &binary_expr = to_binary_expr(expr); // first remove side-effects from condition - clean_expr(to_binary_expr(expr).op0(), dest, mode); + new_vars = clean_expr(to_binary_expr(expr).op0(), dest, mode); // now we can copy op0 safely if_exprt if_expr( @@ -537,5 +563,7 @@ void goto_convertt::remove_gcc_conditional_expression( } // there might still be junk in expr.op2() - clean_expr(expr, dest, mode); + new_vars.add(clean_expr(expr, dest, mode)); + + return new_vars; } diff --git a/src/ansi-c/goto-conversion/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp index 4c2f8960ed8..ebe6286b6cd 100644 --- a/src/ansi-c/goto-conversion/goto_convert.cpp +++ b/src/ansi-c/goto-conversion/goto_convert.cpp @@ -760,7 +760,8 @@ void goto_convertt::convert_expression( } else { - clean_expr(expr, dest, mode, false); // result _not_ used + // result _not_ used + needs_destructiont new_vars = clean_expr(expr, dest, mode, false); // Any residual expression? // We keep it to add checks later. @@ -771,6 +772,8 @@ void goto_convertt::convert_expression( tmp.add_source_location() = expr.source_location(); copy(tmp, OTHER, dest); } + + destruct_locals(new_vars.minimal_scope, dest, ns); } } @@ -806,7 +809,7 @@ void goto_convertt::convert_frontend_decl( const auto declaration_iterator = std::prev(dest.instructions.end()); auto initializer_location = initializer.find_source_location(); - clean_expr(initializer, dest, mode); + needs_destructiont new_vars = clean_expr(initializer, dest, mode); if(initializer.is_not_nil()) { @@ -816,6 +819,8 @@ void goto_convertt::convert_frontend_decl( convert_assign(assign, dest, mode); } + destruct_locals(new_vars.minimal_scope, dest, ns); + return declaration_iterator; }(); @@ -855,7 +860,7 @@ void goto_convertt::convert_assign( { exprt lhs = code.lhs(), rhs = code.rhs(); - clean_expr(lhs, dest, mode); + needs_destructiont new_vars = clean_expr(lhs, dest, mode); if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_function_call) { @@ -867,7 +872,7 @@ void goto_convertt::convert_assign( rhs.find_source_location()); Forall_operands(it, rhs) - clean_expr(*it, dest, mode); + new_vars.add(clean_expr(*it, dest, mode)); do_function_call( lhs, @@ -881,7 +886,7 @@ void goto_convertt::convert_assign( rhs.get(ID_statement) == ID_cpp_new_array)) { Forall_operands(it, rhs) - clean_expr(*it, dest, mode); + new_vars.add(clean_expr(*it, dest, mode)); // TODO: This should be done in a separate pass do_cpp_new(lhs, to_side_effect_expr(rhs), dest); @@ -895,7 +900,7 @@ void goto_convertt::convert_assign( rhs.get(ID_statement) == ID_gcc_conditional_expression)) { // handle above side effects - clean_expr(rhs, dest, mode); + new_vars.add(clean_expr(rhs, dest, mode)); code_assignt new_assign(code); new_assign.lhs() = lhs; @@ -908,7 +913,7 @@ void goto_convertt::convert_assign( // preserve side effects that will be handled at later stages, // such as allocate, new operators of other languages, e.g. java, etc Forall_operands(it, rhs) - clean_expr(*it, dest, mode); + new_vars.add(clean_expr(*it, dest, mode)); code_assignt new_assign(code); new_assign.lhs() = lhs; @@ -919,7 +924,7 @@ void goto_convertt::convert_assign( else { // do everything else - clean_expr(rhs, dest, mode); + new_vars.add(clean_expr(rhs, dest, mode)); code_assignt new_assign(code); new_assign.lhs() = lhs; @@ -927,6 +932,8 @@ void goto_convertt::convert_assign( copy(new_assign, ASSIGN, dest); } + + destruct_locals(new_vars.minimal_scope, dest, ns); } void goto_convertt::convert_cpp_delete(const codet &code, goto_programt &dest) @@ -938,7 +945,7 @@ void goto_convertt::convert_cpp_delete(const codet &code, goto_programt &dest) exprt tmp_op = code.op0(); - clean_expr(tmp_op, dest, ID_cpp); + needs_destructiont new_vars = clean_expr(tmp_op, dest, ID_cpp); // we call the destructor, and then free const exprt &destructor = @@ -987,6 +994,8 @@ void goto_convertt::convert_cpp_delete(const codet &code, goto_programt &dest) delete_call.add_source_location() = code.source_location(); convert(delete_call, dest, ID_cpp); + + destruct_locals(new_vars.minimal_scope, dest, ns); } void goto_convertt::convert_assert( @@ -996,11 +1005,13 @@ void goto_convertt::convert_assert( { exprt cond = code.assertion(); - clean_expr(cond, dest, mode); + needs_destructiont new_vars = clean_expr(cond, dest, mode); source_locationt annotated_location = code.source_location(); annotated_location.set("user-provided", true); dest.add(goto_programt::make_assertion(cond, annotated_location)); + + destruct_locals(new_vars.minimal_scope, dest, ns); } void goto_convertt::convert_skip(const codet &code, goto_programt &dest) @@ -1016,9 +1027,11 @@ void goto_convertt::convert_assume( { exprt op = code.assumption(); - clean_expr(op, dest, mode); + needs_destructiont new_vars = clean_expr(op, dest, mode); dest.add(goto_programt::make_assumption(op, code.source_location())); + + destruct_locals(new_vars.minimal_scope, dest, ns); } void goto_convertt::convert_loop_contracts( @@ -1072,10 +1085,12 @@ void goto_convertt::convert_for( //----------------------------- // A; // u: sideeffects in c - // v: if(!c) goto z; + // v: if(!c) goto Z; + // cleanup-loop; // w: P; // x: B; <-- continue target // y: goto u; + // Z: cleanup-out; // z: ; <-- break target // A; @@ -1085,7 +1100,7 @@ void goto_convertt::convert_for( exprt cond = code.cond(); goto_programt sideeffects; - clean_expr(cond, sideeffects, mode); + needs_destructiont new_vars = clean_expr(cond, sideeffects, mode); // save break/continue targets break_continue_targetst old_targets(targets); @@ -1096,11 +1111,14 @@ void goto_convertt::convert_for( // do the v label goto_programt tmp_v; goto_programt::targett v = tmp_v.add(goto_programt::instructiont()); + destruct_locals(new_vars.minimal_scope, tmp_v, ns); - // do the z label + // do the z and Z labels goto_programt tmp_z; + destruct_locals(new_vars.minimal_scope, tmp_z, ns); goto_programt::targett z = tmp_z.add(goto_programt::make_skip(code.source_location())); + goto_programt::targett Z = tmp_z.instructions.begin(); // do the x label goto_programt tmp_x; @@ -1113,7 +1131,8 @@ void goto_convertt::convert_for( { exprt tmp_B = code.iter(); - clean_expr(tmp_B, tmp_x, mode, false); + needs_destructiont new_vars_iter = clean_expr(tmp_B, tmp_x, mode, false); + destruct_locals(new_vars_iter.minimal_scope, tmp_x, ns); if(tmp_x.instructions.empty()) tmp_x.add(goto_programt::make_skip(code.source_location())); @@ -1127,9 +1146,9 @@ void goto_convertt::convert_for( targets.set_break(z); targets.set_continue(tmp_x.instructions.begin()); - // v: if(!c) goto z; + // v: if(!c) goto Z; *v = - goto_programt::make_goto(z, boolean_negate(cond), cond.source_location()); + goto_programt::make_goto(Z, boolean_negate(cond), cond.source_location()); // do the w label goto_programt tmp_w; @@ -1226,13 +1245,16 @@ void goto_convertt::convert_dowhile( exprt cond = code.cond(); goto_programt sideeffects; - clean_expr(cond, sideeffects, mode); + needs_destructiont new_vars = clean_expr(cond, sideeffects, mode); // do P while(c); //-------------------- // w: P; // x: sideeffects in c <-- continue target - // y: if(c) goto w; + // y: if(!c) goto C; + // cleanup-loop; + // W: goto w; + // C: cleanup-out; // z: ; <-- break target // save break/continue targets @@ -1240,13 +1262,21 @@ void goto_convertt::convert_dowhile( // do the y label goto_programt tmp_y; - goto_programt::targett y = - tmp_y.add(goto_programt::make_incomplete_goto(cond, condition_location)); + goto_programt::targett y = tmp_y.add(goto_programt::make_incomplete_goto( + boolean_negate(cond), condition_location)); + destruct_locals(new_vars.minimal_scope, tmp_y, ns); + goto_programt::targett W = tmp_y.add( + goto_programt::make_incomplete_goto(true_exprt{}, condition_location)); - // do the z label + // do the z label and C labels goto_programt tmp_z; + destruct_locals(new_vars.minimal_scope, tmp_z, ns); goto_programt::targett z = tmp_z.add(goto_programt::make_skip(code.source_location())); + goto_programt::targett C = tmp_z.instructions.begin(); + + // y: if(!c) goto C; + y->complete_goto(C); // do the x label goto_programt::targett x; @@ -1264,8 +1294,8 @@ void goto_convertt::convert_dowhile( convert(code.body(), tmp_w, mode); goto_programt::targett w = tmp_w.instructions.begin(); - // y: if(c) goto w; - y->complete_goto(w); + // W: goto w; + W->complete_goto(w); // assigns_clause, loop invariant and decreases clause convert_loop_contracts(code, y); @@ -1344,7 +1374,7 @@ void goto_convertt::convert_switch( exprt argument = code.value(); goto_programt sideeffects; - clean_expr(argument, sideeffects, mode); + needs_destructiont new_vars = clean_expr(argument, sideeffects, mode); // Avoid potential performance penalties caused by evaluating the value // multiple times (as the below chain-of-ifs does). "needs_cleaning" isn't @@ -1365,6 +1395,8 @@ void goto_convertt::convert_switch( convert(copy_value, sideeffects, mode); argument = new_symbol.symbol_expr(); + new_vars.minimal_scope.push_front( + to_symbol_expr(argument).get_identifier()); } // save break/default/cases targets @@ -1411,10 +1443,29 @@ void goto_convertt::convert_switch( source_locationt source_location = case_ops.front().find_source_location(); source_location.set_case_number(std::to_string(case_number)); case_number++; - guard_expr.add_source_location() = source_location; - tmp_cases.add(goto_programt::make_goto( - case_pair.first, std::move(guard_expr), source_location)); + if(new_vars.minimal_scope.empty()) + { + guard_expr.add_source_location() = source_location; + + tmp_cases.add(goto_programt::make_goto( + case_pair.first, std::move(guard_expr), source_location)); + } + else + { + guard_expr = boolean_negate(guard_expr); + guard_expr.add_source_location() = source_location; + + goto_programt::targett try_next = + tmp_cases.add(goto_programt::make_incomplete_goto( + std::move(guard_expr), source_location)); + destruct_locals(new_vars.minimal_scope, tmp_cases, ns); + tmp_cases.add(goto_programt::make_goto( + case_pair.first, true_exprt{}, source_location)); + goto_programt::targett next_case = + tmp_cases.add(goto_programt::make_skip(source_location)); + try_next->complete_goto(next_case); + } } tmp_cases.add(goto_programt::make_goto( @@ -1463,13 +1514,15 @@ void goto_convertt::convert_return( code.find_source_location()); code_frontend_returnt new_code(code); + needs_destructiont new_vars; if(new_code.has_return_value()) { bool result_is_used = new_code.return_value().type().id() != ID_empty; goto_programt sideeffects; - clean_expr(new_code.return_value(), sideeffects, mode, result_is_used); + new_vars = + clean_expr(new_code.return_value(), sideeffects, mode, result_is_used); dest.destructive_append(sideeffects); // remove void-typed return value @@ -1487,6 +1540,7 @@ void goto_convertt::convert_return( // Now add a 'set return value' instruction to set the return value. dest.add(goto_programt::make_set_return_value( new_code.return_value(), new_code.source_location())); + destruct_locals(new_vars.minimal_scope, dest, ns); } else { @@ -1619,10 +1673,11 @@ void goto_convertt::convert_ifthenelse( } exprt tmp_guard = code.cond(); - clean_expr(tmp_guard, dest, mode); + needs_destructiont new_vars = clean_expr(tmp_guard, dest, mode); // convert 'then'-branch goto_programt tmp_then; + destruct_locals(new_vars.minimal_scope, tmp_then, ns); convert(code.then_case(), tmp_then, mode); source_locationt then_end_location = code.then_case().get_statement() == ID_block @@ -1630,6 +1685,7 @@ void goto_convertt::convert_ifthenelse( : code.then_case().source_location(); goto_programt tmp_else; + destruct_locals(new_vars.minimal_scope, tmp_else, ns); source_locationt else_end_location; if(has_else) @@ -1882,9 +1938,13 @@ void goto_convertt::generate_conditional_branch( { // simple branch exprt cond = guard; - clean_expr(cond, dest, mode); + needs_destructiont new_vars = clean_expr(cond, dest, mode); dest.add(goto_programt::make_goto(target_true, cond, source_location)); + goto_programt tmp_destruct; + destruct_locals(new_vars.minimal_scope, tmp_destruct, ns); + dest.insert_before_swap(target_true, tmp_destruct); + destruct_locals(new_vars.minimal_scope, dest, ns); } } @@ -1954,13 +2014,18 @@ void goto_convertt::generate_conditional_branch( } exprt cond = guard; - clean_expr(cond, dest, mode); + needs_destructiont new_vars = clean_expr(cond, dest, mode); // true branch dest.add(goto_programt::make_goto(target_true, cond, source_location)); + goto_programt tmp_destruct; + destruct_locals(new_vars.minimal_scope, tmp_destruct, ns); + dest.insert_before_swap(target_true, tmp_destruct); // false branch dest.add(goto_programt::make_goto(target_false, source_location)); + destruct_locals(new_vars.minimal_scope, tmp_destruct, ns); + dest.insert_before_swap(target_false, tmp_destruct); } bool goto_convertt::get_string_constant(const exprt &expr, irep_idt &value) @@ -2065,14 +2130,16 @@ symbolt &goto_convertt::new_tmp_symbol( mode, symbol_table); - code_frontend_declt decl(new_symbol.symbol_expr()); - decl.add_source_location() = source_location; - convert_frontend_decl(decl, dest, mode); + if(type.id() != ID_code) + { + dest.add( + goto_programt::make_decl(new_symbol.symbol_expr(), source_location)); + } return new_symbol; } -void goto_convertt::make_temp_symbol( +irep_idt goto_convertt::make_temp_symbol( exprt &expr, const std::string &suffix, goto_programt &dest, @@ -2091,6 +2158,8 @@ void goto_convertt::make_temp_symbol( convert(assignment, dest, mode); expr = new_symbol.symbol_expr(); + + return to_symbol_expr(expr).get_identifier(); } void goto_convert( diff --git a/src/ansi-c/goto-conversion/goto_convert_class.h b/src/ansi-c/goto-conversion/goto_convert_class.h index 1256d10ad41..750eb2a07ac 100644 --- a/src/ansi-c/goto-conversion/goto_convert_class.h +++ b/src/ansi-c/goto-conversion/goto_convert_class.h @@ -56,6 +56,22 @@ class goto_convertt : public messaget std::string tmp_symbol_prefix; lifetimet lifetime = lifetimet::STATIC_GLOBAL; + struct needs_destructiont + { + std::list minimal_scope; + + needs_destructiont() = default; + + explicit needs_destructiont(irep_idt id) : minimal_scope({id}) + { + } + + void add(needs_destructiont &&other) + { + minimal_scope.splice(minimal_scope.begin(), other.minimal_scope); + } + }; + void goto_convert_rec( const codet &code, goto_programt &dest, @@ -64,7 +80,7 @@ class goto_convertt : public messaget // // tools for symbols // - symbolt &new_tmp_symbol( + [[nodiscard]] symbolt &new_tmp_symbol( const typet &type, const std::string &suffix, goto_programt &dest, @@ -81,13 +97,13 @@ class goto_convertt : public messaget // into the program logic // - void clean_expr( + [[nodiscard]] needs_destructiont clean_expr( exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used = true); - void + [[nodiscard]] needs_destructiont clean_expr_address_of(exprt &expr, goto_programt &dest, const irep_idt &mode); static bool needs_cleaning(const exprt &expr); @@ -101,7 +117,7 @@ class goto_convertt : public messaget return lhs.id() != ID_symbol; } - void make_temp_symbol( + [[nodiscard]] irep_idt make_temp_symbol( exprt &expr, const std::string &suffix, goto_programt &, @@ -109,55 +125,56 @@ class goto_convertt : public messaget void rewrite_boolean(exprt &dest); - void remove_side_effect( + [[nodiscard]] needs_destructiont remove_side_effect( side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used, bool address_taken); - void remove_assignment( + [[nodiscard]] needs_destructiont remove_assignment( side_effect_exprt &expr, goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode); - void remove_pre( + [[nodiscard]] needs_destructiont remove_pre( side_effect_exprt &expr, goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode); - void remove_post( + [[nodiscard]] needs_destructiont remove_post( side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used); - void remove_function_call( + [[nodiscard]] needs_destructiont remove_function_call( side_effect_expr_function_callt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used); - void remove_cpp_new( + [[nodiscard]] needs_destructiont remove_cpp_new( side_effect_exprt &expr, goto_programt &dest, bool result_is_used); void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest); - void remove_malloc( + [[nodiscard]] needs_destructiont remove_malloc( side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used); - void remove_temporary_object(side_effect_exprt &expr, goto_programt &dest); - void remove_statement_expression( + [[nodiscard]] needs_destructiont + remove_temporary_object(side_effect_exprt &expr, goto_programt &dest); + [[nodiscard]] needs_destructiont remove_statement_expression( side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used); - void remove_gcc_conditional_expression( + [[nodiscard]] needs_destructiont remove_gcc_conditional_expression( exprt &expr, goto_programt &dest, const irep_idt &mode); - void remove_overflow( + [[nodiscard]] needs_destructiont remove_overflow( side_effect_expr_overflowt &expr, goto_programt &dest, bool result_is_used, diff --git a/src/ansi-c/goto-conversion/goto_convert_function_call.cpp b/src/ansi-c/goto-conversion/goto_convert_function_call.cpp index 062d56a9681..badf8384a26 100644 --- a/src/ansi-c/goto-conversion/goto_convert_function_call.cpp +++ b/src/ansi-c/goto-conversion/goto_convert_function_call.cpp @@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "destructor.h" + void goto_convertt::convert_function_call( const code_function_callt &function_call, goto_programt &dest, @@ -41,13 +43,15 @@ void goto_convertt::do_function_call( exprt::operandst new_arguments = arguments; + needs_destructiont new_vars; + if(!new_lhs.is_nil()) - clean_expr(new_lhs, dest, mode); + new_vars.add(clean_expr(new_lhs, dest, mode)); - clean_expr(new_function, dest, mode); + new_vars.add(clean_expr(new_function, dest, mode)); for(auto &new_argument : new_arguments) - clean_expr(new_argument, dest, mode); + new_vars.add(clean_expr(new_argument, dest, mode)); // split on the function @@ -78,6 +82,8 @@ void goto_convertt::do_function_call( new_function.id(), function.find_source_location()); } + + destruct_locals(new_vars.minimal_scope, dest, ns); } void goto_convertt::do_function_call_if( diff --git a/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp b/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp index b5720722e68..61a8587fe0a 100644 --- a/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp +++ b/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp @@ -22,7 +22,9 @@ Author: Daniel Kroening, kroening@kroening.com #include -void goto_convertt::remove_assignment( +#include "destructor.h" + +goto_convertt::needs_destructiont goto_convertt::remove_assignment( side_effect_exprt &expr, goto_programt &dest, bool result_is_used, @@ -33,6 +35,8 @@ void goto_convertt::remove_assignment( std::optional replacement_expr_opt; + needs_destructiont new_vars; + if(statement == ID_assign) { auto &old_assignment = to_side_effect_expr_assign(expr); @@ -43,7 +47,10 @@ void goto_convertt::remove_assignment( assignment_lhs_needs_temporary(old_assignment.lhs())) { if(!old_assignment.rhs().is_constant()) - make_temp_symbol(old_assignment.rhs(), "assign", dest, mode); + { + new_vars.minimal_scope.push_front( + make_temp_symbol(old_assignment.rhs(), "assign", dest, mode)); + } replacement_expr_opt = typecast_exprt::conditional_cast(old_assignment.rhs(), new_lhs.type()); @@ -113,7 +120,8 @@ void goto_convertt::remove_assignment( result_is_used && !address_taken && assignment_lhs_needs_temporary(binary_expr.op0())) { - make_temp_symbol(rhs, "assign", dest, mode); + new_vars.minimal_scope.push_front( + make_temp_symbol(rhs, "assign", dest, mode)); replacement_expr_opt = typecast_exprt::conditional_cast(rhs, new_lhs.type()); } @@ -134,8 +142,13 @@ void goto_convertt::remove_assignment( exprt new_lhs = typecast_exprt::conditional_cast(*replacement_expr_opt, expr.type()); expr.swap(new_lhs); + + return new_vars; } - else if(result_is_used) + + destruct_locals(new_vars.minimal_scope, dest, ns); + + if(result_is_used) { exprt lhs = to_binary_expr(expr).op0(); // assign_* statements can have an lhs operand with a different type than @@ -159,9 +172,11 @@ void goto_convertt::remove_assignment( } else expr.make_nil(); + + return {}; } -void goto_convertt::remove_pre( +goto_convertt::needs_destructiont goto_convertt::remove_pre( side_effect_exprt &expr, goto_programt &dest, bool result_is_used, @@ -227,8 +242,9 @@ void goto_convertt::remove_pre( const bool cannot_use_lhs = result_is_used && !address_taken && assignment_lhs_needs_temporary(lhs); + needs_destructiont new_vars; if(cannot_use_lhs) - make_temp_symbol(rhs, "pre", dest, mode); + new_vars.minimal_scope.push_front(make_temp_symbol(rhs, "pre", dest, mode)); code_assignt assignment(lhs, rhs); assignment.add_source_location() = expr.find_source_location(); @@ -251,9 +267,11 @@ void goto_convertt::remove_pre( } else expr.make_nil(); + + return new_vars; } -void goto_convertt::remove_post( +goto_convertt::needs_destructiont goto_convertt::remove_post( side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, @@ -316,6 +334,8 @@ void goto_convertt::remove_post( // fix up the expression, if needed + needs_destructiont new_vars; + if(result_is_used) { exprt tmp = op; @@ -326,7 +346,8 @@ void goto_convertt::remove_post( suffix += "_" + id2string(base_name); } - make_temp_symbol(tmp, suffix, dest, mode); + new_vars.minimal_scope.push_front( + make_temp_symbol(tmp, suffix, dest, mode)); expr.swap(tmp); } else @@ -334,9 +355,11 @@ void goto_convertt::remove_post( dest.destructive_append(tmp1); dest.destructive_append(tmp2); + + return new_vars; } -void goto_convertt::remove_function_call( +goto_convertt::needs_destructiont goto_convertt::remove_function_call( side_effect_expr_function_callt &expr, goto_programt &dest, const irep_idt &mode, @@ -348,7 +371,7 @@ void goto_convertt::remove_function_call( call.add_source_location() = expr.source_location(); convert_function_call(call, dest, mode); expr.make_nil(); - return; + return {}; } // get name of function, if available @@ -374,11 +397,9 @@ void goto_convertt::remove_function_call( new_symbol_mode, symbol_table); - { - code_frontend_declt decl(new_symbol.symbol_expr()); - decl.add_source_location() = new_symbol.location; - convert_frontend_decl(decl, dest, mode); - } + PRECONDITION(expr.type().id() != ID_code); + dest.add( + goto_programt::make_decl(new_symbol.symbol_expr(), new_symbol.location)); { goto_programt tmp_program2; @@ -389,6 +410,8 @@ void goto_convertt::remove_function_call( } static_cast(expr) = new_symbol.symbol_expr(); + + return needs_destructiont{to_symbol_expr(expr).get_identifier()}; } void goto_convertt::replace_new_object(const exprt &object, exprt &dest) @@ -400,7 +423,7 @@ void goto_convertt::replace_new_object(const exprt &object, exprt &dest) replace_new_object(object, *it); } -void goto_convertt::remove_cpp_new( +goto_convertt::needs_destructiont goto_convertt::remove_cpp_new( side_effect_exprt &expr, goto_programt &dest, bool result_is_used) @@ -413,18 +436,24 @@ void goto_convertt::remove_cpp_new( ID_cpp, symbol_table); - code_frontend_declt decl(new_symbol.symbol_expr()); - decl.add_source_location() = new_symbol.location; - convert_frontend_decl(decl, dest, ID_cpp); + PRECONDITION(expr.type().id() != ID_code); + dest.add( + goto_programt::make_decl(new_symbol.symbol_expr(), new_symbol.location)); const code_assignt call(new_symbol.symbol_expr(), expr); + convert(call, dest, ID_cpp); + if(result_is_used) + { static_cast(expr) = new_symbol.symbol_expr(); + return needs_destructiont{to_symbol_expr(expr).get_identifier()}; + } else + { expr.make_nil(); - - convert(call, dest, ID_cpp); + return {}; + } } void goto_convertt::remove_cpp_delete( @@ -443,7 +472,7 @@ void goto_convertt::remove_cpp_delete( expr.make_nil(); } -void goto_convertt::remove_malloc( +goto_convertt::needs_destructiont goto_convertt::remove_malloc( side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, @@ -469,14 +498,18 @@ void goto_convertt::remove_malloc( static_cast(expr) = new_symbol.symbol_expr(); convert(call, dest, mode); + + return needs_destructiont{to_symbol_expr(expr).get_identifier()}; } else { convert(code_expressiont(std::move(expr)), dest, mode); + + return {}; } } -void goto_convertt::remove_temporary_object( +goto_convertt::needs_destructiont goto_convertt::remove_temporary_object( side_effect_exprt &expr, goto_programt &dest) { @@ -510,9 +543,11 @@ void goto_convertt::remove_temporary_object( } static_cast(expr) = new_symbol.symbol_expr(); + + return needs_destructiont{to_symbol_expr(expr).get_identifier()}; } -void goto_convertt::remove_statement_expression( +goto_convertt::needs_destructiont goto_convertt::remove_statement_expression( side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, @@ -529,7 +564,7 @@ void goto_convertt::remove_statement_expression( { convert(code, dest, mode); expr.make_nil(); - return; + return {}; } INVARIANT_WITH_DIAGNOSTICS( @@ -579,9 +614,11 @@ void goto_convertt::remove_statement_expression( } static_cast(expr) = tmp_symbol_expr; + + return needs_destructiont{to_symbol_expr(expr).get_identifier()}; } -void goto_convertt::remove_overflow( +goto_convertt::needs_destructiont goto_convertt::remove_overflow( side_effect_expr_overflowt &expr, goto_programt &dest, bool result_is_used, @@ -592,12 +629,14 @@ void goto_convertt::remove_overflow( const exprt &rhs = expr.rhs(); const exprt &result = expr.result(); + needs_destructiont new_vars; + if(result.type().id() != ID_pointer) { // result of the arithmetic operation is _not_ used, just evaluate side // effects exprt tmp = result; - clean_expr(tmp, dest, mode, false); + new_vars.add(clean_expr(tmp, dest, mode, false)); // the is-there-an-overflow result may be used if(result_is_used) @@ -627,7 +666,10 @@ void goto_convertt::remove_overflow( overflow_with_result.add_source_location() = expr.source_location(); if(result_is_used) - make_temp_symbol(overflow_with_result, "overflow_result", dest, mode); + { + new_vars.minimal_scope.push_front( + make_temp_symbol(overflow_with_result, "overflow_result", dest, mode)); + } const struct_typet::componentst &result_comps = to_struct_type(overflow_with_result.type()).components(); @@ -649,9 +691,11 @@ void goto_convertt::remove_overflow( else expr.make_nil(); } + + return new_vars; } -void goto_convertt::remove_side_effect( +goto_convertt::needs_destructiont goto_convertt::remove_side_effect( side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, @@ -661,8 +705,10 @@ void goto_convertt::remove_side_effect( const irep_idt &statement = expr.get_statement(); if(statement == ID_function_call) - remove_function_call( + { + return remove_function_call( to_side_effect_expr_function_call(expr), dest, mode, result_is_used); + } else if( statement == ID_assign || statement == ID_assign_plus || statement == ID_assign_minus || statement == ID_assign_mult || @@ -670,28 +716,47 @@ void goto_convertt::remove_side_effect( statement == ID_assign_bitxor || statement == ID_assign_bitand || statement == ID_assign_lshr || statement == ID_assign_ashr || statement == ID_assign_shl || statement == ID_assign_mod) - remove_assignment(expr, dest, result_is_used, address_taken, mode); + { + return remove_assignment(expr, dest, result_is_used, address_taken, mode); + } else if(statement == ID_postincrement || statement == ID_postdecrement) - remove_post(expr, dest, mode, result_is_used); + { + return remove_post(expr, dest, mode, result_is_used); + } else if(statement == ID_preincrement || statement == ID_predecrement) - remove_pre(expr, dest, result_is_used, address_taken, mode); + { + return remove_pre(expr, dest, result_is_used, address_taken, mode); + } else if(statement == ID_cpp_new || statement == ID_cpp_new_array) - remove_cpp_new(expr, dest, result_is_used); + { + return remove_cpp_new(expr, dest, result_is_used); + } else if(statement == ID_cpp_delete || statement == ID_cpp_delete_array) + { remove_cpp_delete(expr, dest); + return {}; + } else if(statement == ID_allocate) - remove_malloc(expr, dest, mode, result_is_used); + { + return remove_malloc(expr, dest, mode, result_is_used); + } else if(statement == ID_temporary_object) - remove_temporary_object(expr, dest); + { + return remove_temporary_object(expr, dest); + } else if(statement == ID_statement_expression) - remove_statement_expression(expr, dest, mode, result_is_used); + { + return remove_statement_expression(expr, dest, mode, result_is_used); + } else if(statement == ID_nondet) { // these are fine + return {}; } else if(statement == ID_skip) { expr.make_nil(); + return {}; } else if(statement == ID_throw) { @@ -704,12 +769,13 @@ void goto_convertt::remove_side_effect( // the result can't be used, these are void expr.make_nil(); + return {}; } else if( statement == ID_overflow_plus || statement == ID_overflow_minus || statement == ID_overflow_mult) { - remove_overflow( + return remove_overflow( to_side_effect_expr_overflow(expr), dest, result_is_used, mode); } else diff --git a/src/cprover/simplify_state_expr.cpp b/src/cprover/simplify_state_expr.cpp index 44700528df2..d11f031a8b5 100644 --- a/src/cprover/simplify_state_expr.cpp +++ b/src/cprover/simplify_state_expr.cpp @@ -517,6 +517,10 @@ exprt simplify_object_size_expr( { return src.with_state(to_update_state_expr(src.state()).state()); } + else if(src.state().id() == ID_exit_scope_state) + { + return src.with_state(to_exit_scope_state_expr(src.state()).state()); + } return std::move(src); } diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 36eff629528..15f83a46504 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -581,13 +581,16 @@ static void generate_contract_constraints( goto_programt constraint; if(location.get_property_class() == ID_assume) { - converter.goto_convert(code_assumet(instantiated_clause), constraint, mode); + code_assumet assumption(instantiated_clause); + assumption.add_source_location() = location; + converter.goto_convert(assumption, constraint, mode); } else { - converter.goto_convert(code_assertt(instantiated_clause), constraint, mode); + code_assertt assertion(instantiated_clause); + assertion.add_source_location() = location; + converter.goto_convert(assertion, constraint, mode); } - constraint.instructions.back().source_location_nonconst() = location; is_fresh_update(constraint); throw_on_unsupported(constraint); program.destructive_append(constraint); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp index 6c0d8baf321..8a97ef48fd0 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp @@ -21,6 +21,7 @@ Date: February 2023 #include #include +#include #include #include @@ -104,8 +105,9 @@ void dfcc_contract_clauses_codegent::encode_assignable_target_group( // clean up side effects from the condition expression if needed cleanert cleaner(goto_model.symbol_table, log.get_message_handler()); exprt condition(group.condition()); + std::list new_vars; if(has_subexpr(condition, ID_side_effect)) - cleaner.clean(condition, dest, language_mode); + new_vars = cleaner.clean(condition, dest, language_mode); // Jump target if condition is false auto goto_instruction = dest.add( @@ -116,6 +118,8 @@ void dfcc_contract_clauses_codegent::encode_assignable_target_group( auto label_instruction = dest.add(goto_programt::make_skip(source_location)); goto_instruction->complete_goto(label_instruction); + + destruct_locals(new_vars, dest, ns); } void dfcc_contract_clauses_codegent::encode_assignable_target( @@ -190,8 +194,9 @@ void dfcc_contract_clauses_codegent::encode_freeable_target_group( // clean up side effects from the condition expression if needed cleanert cleaner(goto_model.symbol_table, log.get_message_handler()); exprt condition(group.condition()); + std::list new_vars; if(has_subexpr(condition, ID_side_effect)) - cleaner.clean(condition, dest, language_mode); + new_vars = cleaner.clean(condition, dest, language_mode); // Jump target if condition is false auto goto_instruction = dest.add( @@ -202,6 +207,8 @@ void dfcc_contract_clauses_codegent::encode_freeable_target_group( auto label_instruction = dest.add(goto_programt::make_skip(source_location)); goto_instruction->complete_goto(label_instruction); + + destruct_locals(new_vars, dest, ns); } void dfcc_contract_clauses_codegent::encode_freeable_target( diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp index 5f975e4cbb7..fc273e46259 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -23,6 +23,7 @@ Date: January 2022 #include #include +#include #include #include "cfg_info.h" @@ -419,8 +420,9 @@ void instrument_spec_assignst::track_spec_target_group( // clean up side effects from the guard expression if needed cleanert cleaner(st, log.get_message_handler()); exprt condition(group.condition()); + std::list new_vars; if(has_subexpr(condition, ID_side_effect)) - cleaner.clean(condition, dest, mode); + new_vars = cleaner.clean(condition, dest, mode); // create conditional address ranges by distributing the condition for(const auto &target : group.targets()) @@ -434,6 +436,8 @@ void instrument_spec_assignst::track_spec_target_group( // generate snapshot instructions for this target. create_snapshot(car, dest); } + + destruct_locals(new_vars, dest, ns); } void instrument_spec_assignst::track_plain_spec_target( diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 0dd802bab18..b25f43467d8 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -43,9 +43,10 @@ class cleanert : public goto_convertt { } - void clean(exprt &guard, goto_programt &dest, const irep_idt &mode) + [[nodiscard]] std::list + clean(exprt &guard, goto_programt &dest, const irep_idt &mode) { - goto_convertt::clean_expr(guard, dest, mode, true); + return goto_convertt::clean_expr(guard, dest, mode, true).minimal_scope; } void do_havoc_slice( From cb2e20c2f3d49642ec9d34544577a616344f273b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 9 Jul 2024 12:24:48 +0000 Subject: [PATCH 2/2] GOTO conversion: move out-only clean_expr parameter to return value Removes one side-effect of invoking clean_expr and instead expands on the return-value type. --- .../goto-conversion/builtin_functions.cpp | 10 +- .../goto-conversion/goto_clean_expr.cpp | 144 ++++++------ src/ansi-c/goto-conversion/goto_convert.cpp | 129 ++++++----- .../goto-conversion/goto_convert_class.h | 79 +++---- .../goto_convert_function_call.cpp | 12 +- .../goto_convert_side_effect.cpp | 210 ++++++++++-------- src/goto-instrument/contracts/utils.h | 4 +- 7 files changed, 308 insertions(+), 280 deletions(-) diff --git a/src/ansi-c/goto-conversion/builtin_functions.cpp b/src/ansi-c/goto-conversion/builtin_functions.cpp index ea6c30d173d..bf864fcdb1e 100644 --- a/src/ansi-c/goto-conversion/builtin_functions.cpp +++ b/src/ansi-c/goto-conversion/builtin_functions.cpp @@ -401,7 +401,7 @@ void goto_convertt::do_cpp_new( bool new_array = rhs.get(ID_statement) == ID_cpp_new_array; exprt count; - needs_destructiont new_vars; + clean_expr_resultt side_effects; if(new_array) { @@ -409,7 +409,8 @@ void goto_convertt::do_cpp_new( static_cast(rhs.find(ID_size)), object_size.type()); // might have side-effect - new_vars.add(clean_expr(count, dest, ID_cpp)); + side_effects.add(clean_expr(count, ID_cpp)); + dest.destructive_append(side_effects.side_effects); } exprt tmp_symbol_expr; @@ -495,9 +496,8 @@ void goto_convertt::do_cpp_new( typecast_exprt(tmp_symbol_expr, lhs.type()), rhs.find_source_location())); - new_vars.minimal_scope.push_front( - to_symbol_expr(tmp_symbol_expr).get_identifier()); - destruct_locals(new_vars.minimal_scope, dest, ns); + side_effects.add_temporary(to_symbol_expr(tmp_symbol_expr).get_identifier()); + destruct_locals(side_effects.temporaries, dest, ns); // grab initializer goto_programt tmp_initializer; diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp index d5569bb4b33..c015c1fe414 100644 --- a/src/ansi-c/goto-conversion/goto_clean_expr.cpp +++ b/src/ansi-c/goto-conversion/goto_clean_expr.cpp @@ -166,9 +166,8 @@ void goto_convertt::rewrite_boolean(exprt &expr) expr.swap(tmp); } -goto_convertt::needs_destructiont goto_convertt::clean_expr( +goto_convertt::clean_expr_resultt goto_convertt::clean_expr( exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used) { @@ -189,20 +188,20 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( rewrite_boolean(expr); // recursive call - return clean_expr(expr, dest, mode, result_is_used); + return clean_expr(expr, mode, result_is_used); } else if(expr.id() == ID_if) { // first clean condition - needs_destructiont new_vars = - clean_expr(to_if_expr(expr).cond(), dest, mode, true); + clean_expr_resultt side_effects = + clean_expr(to_if_expr(expr).cond(), mode, true); // possibly done now if( !needs_cleaning(to_if_expr(expr).true_case()) && !needs_cleaning(to_if_expr(expr).false_case())) { - return new_vars; + return side_effects; } // copy expression @@ -236,30 +235,32 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( } #endif - goto_programt tmp_true; - new_vars.add( - clean_expr(if_expr.true_case(), tmp_true, mode, result_is_used)); + clean_expr_resultt tmp_true( + clean_expr(if_expr.true_case(), mode, result_is_used)); - goto_programt tmp_false; - new_vars.add( - clean_expr(if_expr.false_case(), tmp_false, mode, result_is_used)); + clean_expr_resultt tmp_false( + clean_expr(if_expr.false_case(), mode, result_is_used)); if(result_is_used) { - symbolt &new_symbol = - new_tmp_symbol(expr.type(), "if_expr", dest, source_location, mode); + symbolt &new_symbol = new_tmp_symbol( + expr.type(), + "if_expr", + side_effects.side_effects, + source_location, + mode); code_assignt assignment_true; assignment_true.lhs() = new_symbol.symbol_expr(); assignment_true.rhs() = if_expr.true_case(); assignment_true.add_source_location() = source_location; - convert(assignment_true, tmp_true, mode); + convert(assignment_true, tmp_true.side_effects, mode); code_assignt assignment_false; assignment_false.lhs() = new_symbol.symbol_expr(); assignment_false.rhs() = if_expr.false_case(); assignment_false.add_source_location() = source_location; - convert(assignment_false, tmp_false, mode); + convert(assignment_false, tmp_false.side_effects, mode); // overwrites expr expr = new_symbol.symbol_expr(); @@ -273,7 +274,7 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( // expression is just a constant code_expressiont code_expression( typecast_exprt(if_expr.true_case(), empty_typet())); - convert(code_expression, tmp_true, mode); + convert(code_expression, tmp_true.side_effects, mode); } if(if_expr.false_case().is_not_nil()) @@ -282,7 +283,7 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( // expression is just a constant code_expressiont code_expression( typecast_exprt(if_expr.false_case(), empty_typet())); - convert(code_expression, tmp_false, mode); + convert(code_expression, tmp_false.side_effects, mode); } expr = nil_exprt(); @@ -292,24 +293,26 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( generate_ifthenelse( if_expr.cond(), source_location, - tmp_true, + tmp_true.side_effects, if_expr.true_case().source_location(), - tmp_false, + tmp_false.side_effects, if_expr.false_case().source_location(), - dest, + side_effects.side_effects, mode); - destruct_locals(new_vars.minimal_scope, dest, ns); - new_vars.minimal_scope.clear(); + destruct_locals(tmp_false.temporaries, side_effects.side_effects, ns); + destruct_locals(tmp_true.temporaries, side_effects.side_effects, ns); + destruct_locals(side_effects.temporaries, side_effects.side_effects, ns); + side_effects.temporaries.clear(); if(expr.is_not_nil()) - new_vars.minimal_scope.push_front(to_symbol_expr(expr).get_identifier()); + side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); - return new_vars; + return side_effects; } else if(expr.id() == ID_comma) { - needs_destructiont new_vars; + clean_expr_resultt side_effects; if(result_is_used) { @@ -323,15 +326,15 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( if(last) { result.swap(*it); - new_vars.add(clean_expr(result, dest, mode, true)); + side_effects.add(clean_expr(result, mode, true)); } else { - new_vars.add(clean_expr(*it, dest, mode, false)); + side_effects.add(clean_expr(*it, mode, false)); // remember these for later checks if(it->is_not_nil()) - convert(code_expressiont(*it), dest, mode); + convert(code_expressiont(*it), side_effects.side_effects, mode); } } @@ -341,30 +344,30 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( { Forall_operands(it, expr) { - new_vars.add(clean_expr(*it, dest, mode, false)); + side_effects.add(clean_expr(*it, mode, false)); // remember as expression statement for later checks if(it->is_not_nil()) - convert(code_expressiont(*it), dest, mode); + convert(code_expressiont(*it), side_effects.side_effects, mode); } expr = nil_exprt(); } - return new_vars; + return side_effects; } else if(expr.id() == ID_typecast) { typecast_exprt &typecast = to_typecast_expr(expr); // preserve 'result_is_used' - needs_destructiont new_vars = - clean_expr(typecast.op(), dest, mode, result_is_used); + clean_expr_resultt side_effects = + clean_expr(typecast.op(), mode, result_is_used); if(typecast.op().is_nil()) expr.make_nil(); - return new_vars; + return side_effects; } else if(expr.id() == ID_side_effect) { @@ -374,14 +377,14 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( if(statement == ID_gcc_conditional_expression) { // need to do separately - return remove_gcc_conditional_expression(expr, dest, mode); + return remove_gcc_conditional_expression(expr, mode); } else if(statement == ID_statement_expression) { // need to do separately to prevent that // the operands of expr get 'cleaned' return remove_statement_expression( - to_side_effect_expr(expr), dest, mode, result_is_used); + to_side_effect_expr(expr), mode, result_is_used); } else if(statement == ID_assign) { @@ -397,16 +400,15 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( to_side_effect_expr(side_effect_assign.rhs()).get_statement() == ID_function_call) { - needs_destructiont new_vars = - clean_expr(side_effect_assign.lhs(), dest, mode); + clean_expr_resultt side_effects = + clean_expr(side_effect_assign.lhs(), mode); exprt lhs = side_effect_assign.lhs(); const bool must_use_rhs = assignment_lhs_needs_temporary(lhs); if(must_use_rhs) { - new_vars.add(remove_function_call( + side_effects.add(remove_function_call( to_side_effect_expr_function_call(side_effect_assign.rhs()), - dest, mode, true)); } @@ -417,14 +419,14 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( side_effect_assign.rhs(), new_lhs.type()); code_assignt assignment(std::move(new_lhs), new_rhs); assignment.add_source_location() = expr.source_location(); - convert_assign(assignment, dest, mode); + convert_assign(assignment, side_effects.side_effects, mode); if(result_is_used) expr = must_use_rhs ? new_rhs : lhs; else expr.make_nil(); - return new_vars; + return side_effects; } } } @@ -437,20 +439,20 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( else if(expr.id() == ID_address_of) { address_of_exprt &addr = to_address_of_expr(expr); - return clean_expr_address_of(addr.object(), dest, mode); + return clean_expr_address_of(addr.object(), mode); } - needs_destructiont new_vars; + clean_expr_resultt side_effects; // TODO: evaluation order Forall_operands(it, expr) - new_vars.add(clean_expr(*it, dest, mode)); + side_effects.add(clean_expr(*it, mode)); if(expr.id() == ID_side_effect) { - new_vars.add(remove_side_effect( - to_side_effect_expr(expr), dest, mode, result_is_used, false)); + side_effects.add(remove_side_effect( + to_side_effect_expr(expr), mode, result_is_used, false)); } else if(expr.id() == ID_compound_literal) { @@ -460,15 +462,13 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( expr = to_unary_expr(expr).op(); } - return new_vars; + return side_effects; } -goto_convertt::needs_destructiont goto_convertt::clean_expr_address_of( - exprt &expr, - goto_programt &dest, - const irep_idt &mode) +goto_convertt::clean_expr_resultt +goto_convertt::clean_expr_address_of(exprt &expr, const irep_idt &mode) { - needs_destructiont new_vars; + clean_expr_resultt side_effects; // The address of object constructors can be taken, // which is re-written into the address of a variable. @@ -477,8 +477,9 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr_address_of( { DATA_INVARIANT( expr.operands().size() == 1, "ID_compound_literal has a single operand"); - new_vars.add(clean_expr(to_unary_expr(expr).op(), dest, mode)); - expr = make_compound_literal(to_unary_expr(expr).op(), dest, mode); + side_effects.add(clean_expr(to_unary_expr(expr).op(), mode)); + expr = make_compound_literal( + to_unary_expr(expr).op(), side_effects.side_effects, mode); } else if(expr.id() == ID_string_constant) { @@ -488,13 +489,13 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr_address_of( else if(expr.id() == ID_index) { index_exprt &index_expr = to_index_expr(expr); - new_vars.add(clean_expr_address_of(index_expr.array(), dest, mode)); - new_vars.add(clean_expr(index_expr.index(), dest, mode)); + side_effects.add(clean_expr_address_of(index_expr.array(), mode)); + side_effects.add(clean_expr(index_expr.index(), mode)); } else if(expr.id() == ID_dereference) { dereference_exprt &deref_expr = to_dereference_expr(expr); - new_vars.add(clean_expr(deref_expr.pointer(), dest, mode)); + side_effects.add(clean_expr(deref_expr.pointer(), mode)); } else if(expr.id() == ID_comma) { @@ -512,44 +513,43 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr_address_of( result.swap(*it); else { - new_vars.add(clean_expr(*it, dest, mode, false)); + side_effects.add(clean_expr(*it, mode, false)); // get any side-effects if(it->is_not_nil()) - convert(code_expressiont(*it), dest, mode); + convert(code_expressiont(*it), side_effects.side_effects, mode); } } expr.swap(result); // do again - new_vars.add(clean_expr_address_of(expr, dest, mode)); + side_effects.add(clean_expr_address_of(expr, mode)); } else if(expr.id() == ID_side_effect) { - new_vars.add( - remove_side_effect(to_side_effect_expr(expr), dest, mode, true, true)); + side_effects.add( + remove_side_effect(to_side_effect_expr(expr), mode, true, true)); } else Forall_operands(it, expr) - new_vars.add(clean_expr_address_of(*it, dest, mode)); + side_effects.add(clean_expr_address_of(*it, mode)); - return new_vars; + return side_effects; } -goto_convertt::needs_destructiont +goto_convertt::clean_expr_resultt goto_convertt::remove_gcc_conditional_expression( exprt &expr, - goto_programt &dest, const irep_idt &mode) { - needs_destructiont new_vars; + clean_expr_resultt side_effects; { auto &binary_expr = to_binary_expr(expr); // first remove side-effects from condition - new_vars = clean_expr(to_binary_expr(expr).op0(), dest, mode); + side_effects = clean_expr(to_binary_expr(expr).op0(), mode); // now we can copy op0 safely if_exprt if_expr( @@ -563,7 +563,7 @@ goto_convertt::remove_gcc_conditional_expression( } // there might still be junk in expr.op2() - new_vars.add(clean_expr(expr, dest, mode)); + side_effects.add(clean_expr(expr, mode)); - return new_vars; + return side_effects; } diff --git a/src/ansi-c/goto-conversion/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp index ebe6286b6cd..d8b0db12aa8 100644 --- a/src/ansi-c/goto-conversion/goto_convert.cpp +++ b/src/ansi-c/goto-conversion/goto_convert.cpp @@ -761,7 +761,8 @@ void goto_convertt::convert_expression( else { // result _not_ used - needs_destructiont new_vars = clean_expr(expr, dest, mode, false); + clean_expr_resultt side_effects = clean_expr(expr, mode, false); + dest.destructive_append(side_effects.side_effects); // Any residual expression? // We keep it to add checks later. @@ -773,7 +774,7 @@ void goto_convertt::convert_expression( copy(tmp, OTHER, dest); } - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, dest, ns); } } @@ -809,7 +810,8 @@ void goto_convertt::convert_frontend_decl( const auto declaration_iterator = std::prev(dest.instructions.end()); auto initializer_location = initializer.find_source_location(); - needs_destructiont new_vars = clean_expr(initializer, dest, mode); + clean_expr_resultt side_effects = clean_expr(initializer, mode); + dest.destructive_append(side_effects.side_effects); if(initializer.is_not_nil()) { @@ -819,7 +821,7 @@ void goto_convertt::convert_frontend_decl( convert_assign(assign, dest, mode); } - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, dest, ns); return declaration_iterator; }(); @@ -860,7 +862,8 @@ void goto_convertt::convert_assign( { exprt lhs = code.lhs(), rhs = code.rhs(); - needs_destructiont new_vars = clean_expr(lhs, dest, mode); + clean_expr_resultt side_effects = clean_expr(lhs, mode); + dest.destructive_append(side_effects.side_effects); if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_function_call) { @@ -872,7 +875,10 @@ void goto_convertt::convert_assign( rhs.find_source_location()); Forall_operands(it, rhs) - new_vars.add(clean_expr(*it, dest, mode)); + { + side_effects.add(clean_expr(*it, mode)); + dest.destructive_append(side_effects.side_effects); + } do_function_call( lhs, @@ -886,7 +892,10 @@ void goto_convertt::convert_assign( rhs.get(ID_statement) == ID_cpp_new_array)) { Forall_operands(it, rhs) - new_vars.add(clean_expr(*it, dest, mode)); + { + side_effects.add(clean_expr(*it, mode)); + dest.destructive_append(side_effects.side_effects); + } // TODO: This should be done in a separate pass do_cpp_new(lhs, to_side_effect_expr(rhs), dest); @@ -900,7 +909,8 @@ void goto_convertt::convert_assign( rhs.get(ID_statement) == ID_gcc_conditional_expression)) { // handle above side effects - new_vars.add(clean_expr(rhs, dest, mode)); + side_effects.add(clean_expr(rhs, mode)); + dest.destructive_append(side_effects.side_effects); code_assignt new_assign(code); new_assign.lhs() = lhs; @@ -913,7 +923,10 @@ void goto_convertt::convert_assign( // preserve side effects that will be handled at later stages, // such as allocate, new operators of other languages, e.g. java, etc Forall_operands(it, rhs) - new_vars.add(clean_expr(*it, dest, mode)); + { + side_effects.add(clean_expr(*it, mode)); + dest.destructive_append(side_effects.side_effects); + } code_assignt new_assign(code); new_assign.lhs() = lhs; @@ -924,7 +937,8 @@ void goto_convertt::convert_assign( else { // do everything else - new_vars.add(clean_expr(rhs, dest, mode)); + side_effects.add(clean_expr(rhs, mode)); + dest.destructive_append(side_effects.side_effects); code_assignt new_assign(code); new_assign.lhs() = lhs; @@ -933,7 +947,7 @@ void goto_convertt::convert_assign( copy(new_assign, ASSIGN, dest); } - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, dest, ns); } void goto_convertt::convert_cpp_delete(const codet &code, goto_programt &dest) @@ -945,7 +959,8 @@ void goto_convertt::convert_cpp_delete(const codet &code, goto_programt &dest) exprt tmp_op = code.op0(); - needs_destructiont new_vars = clean_expr(tmp_op, dest, ID_cpp); + clean_expr_resultt side_effects = clean_expr(tmp_op, ID_cpp); + dest.destructive_append(side_effects.side_effects); // we call the destructor, and then free const exprt &destructor = @@ -995,7 +1010,7 @@ void goto_convertt::convert_cpp_delete(const codet &code, goto_programt &dest) convert(delete_call, dest, ID_cpp); - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, dest, ns); } void goto_convertt::convert_assert( @@ -1005,13 +1020,14 @@ void goto_convertt::convert_assert( { exprt cond = code.assertion(); - needs_destructiont new_vars = clean_expr(cond, dest, mode); + clean_expr_resultt side_effects = clean_expr(cond, mode); + dest.destructive_append(side_effects.side_effects); source_locationt annotated_location = code.source_location(); annotated_location.set("user-provided", true); dest.add(goto_programt::make_assertion(cond, annotated_location)); - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, dest, ns); } void goto_convertt::convert_skip(const codet &code, goto_programt &dest) @@ -1027,11 +1043,12 @@ void goto_convertt::convert_assume( { exprt op = code.assumption(); - needs_destructiont new_vars = clean_expr(op, dest, mode); + clean_expr_resultt side_effects = clean_expr(op, mode); + dest.destructive_append(side_effects.side_effects); dest.add(goto_programt::make_assumption(op, code.source_location())); - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, dest, ns); } void goto_convertt::convert_loop_contracts( @@ -1099,23 +1116,22 @@ void goto_convertt::convert_for( exprt cond = code.cond(); - goto_programt sideeffects; - needs_destructiont new_vars = clean_expr(cond, sideeffects, mode); + clean_expr_resultt side_effects = clean_expr(cond, mode); // save break/continue targets break_continue_targetst old_targets(targets); // do the u label - goto_programt::targett u = sideeffects.instructions.begin(); + goto_programt::targett u = side_effects.side_effects.instructions.begin(); // do the v label goto_programt tmp_v; goto_programt::targett v = tmp_v.add(goto_programt::instructiont()); - destruct_locals(new_vars.minimal_scope, tmp_v, ns); + destruct_locals(side_effects.temporaries, tmp_v, ns); // do the z and Z labels goto_programt tmp_z; - destruct_locals(new_vars.minimal_scope, tmp_z, ns); + destruct_locals(side_effects.temporaries, tmp_z, ns); goto_programt::targett z = tmp_z.add(goto_programt::make_skip(code.source_location())); goto_programt::targett Z = tmp_z.instructions.begin(); @@ -1131,15 +1147,16 @@ void goto_convertt::convert_for( { exprt tmp_B = code.iter(); - needs_destructiont new_vars_iter = clean_expr(tmp_B, tmp_x, mode, false); - destruct_locals(new_vars_iter.minimal_scope, tmp_x, ns); + clean_expr_resultt side_effects_iter = clean_expr(tmp_B, mode, false); + tmp_x.destructive_append(side_effects_iter.side_effects); + destruct_locals(side_effects_iter.temporaries, tmp_x, ns); if(tmp_x.instructions.empty()) tmp_x.add(goto_programt::make_skip(code.source_location())); } // optimize the v label - if(sideeffects.instructions.empty()) + if(side_effects.side_effects.instructions.empty()) u = v; // set the targets @@ -1162,7 +1179,7 @@ void goto_convertt::convert_for( // assigns clause, loop invariant and decreases clause convert_loop_contracts(code, y); - dest.destructive_append(sideeffects); + dest.destructive_append(side_effects.side_effects); dest.destructive_append(tmp_v); dest.destructive_append(tmp_w); dest.destructive_append(tmp_x); @@ -1244,8 +1261,7 @@ void goto_convertt::convert_dowhile( exprt cond = code.cond(); - goto_programt sideeffects; - needs_destructiont new_vars = clean_expr(cond, sideeffects, mode); + clean_expr_resultt side_effects = clean_expr(cond, mode); // do P while(c); //-------------------- @@ -1264,13 +1280,13 @@ void goto_convertt::convert_dowhile( goto_programt tmp_y; goto_programt::targett y = tmp_y.add(goto_programt::make_incomplete_goto( boolean_negate(cond), condition_location)); - destruct_locals(new_vars.minimal_scope, tmp_y, ns); + destruct_locals(side_effects.temporaries, tmp_y, ns); goto_programt::targett W = tmp_y.add( goto_programt::make_incomplete_goto(true_exprt{}, condition_location)); // do the z label and C labels goto_programt tmp_z; - destruct_locals(new_vars.minimal_scope, tmp_z, ns); + destruct_locals(side_effects.temporaries, tmp_z, ns); goto_programt::targett z = tmp_z.add(goto_programt::make_skip(code.source_location())); goto_programt::targett C = tmp_z.instructions.begin(); @@ -1280,10 +1296,10 @@ void goto_convertt::convert_dowhile( // do the x label goto_programt::targett x; - if(sideeffects.instructions.empty()) + if(side_effects.side_effects.instructions.empty()) x = y; else - x = sideeffects.instructions.begin(); + x = side_effects.side_effects.instructions.begin(); // set the targets targets.set_break(z); @@ -1301,7 +1317,7 @@ void goto_convertt::convert_dowhile( convert_loop_contracts(code, y); dest.destructive_append(tmp_w); - dest.destructive_append(sideeffects); + dest.destructive_append(side_effects.side_effects); dest.destructive_append(tmp_y); dest.destructive_append(tmp_z); @@ -1373,8 +1389,7 @@ void goto_convertt::convert_switch( // do the value we switch over exprt argument = code.value(); - goto_programt sideeffects; - needs_destructiont new_vars = clean_expr(argument, sideeffects, mode); + clean_expr_resultt side_effects = clean_expr(argument, mode); // Avoid potential performance penalties caused by evaluating the value // multiple times (as the below chain-of-ifs does). "needs_cleaning" isn't @@ -1386,17 +1401,16 @@ void goto_convertt::convert_switch( symbolt &new_symbol = new_tmp_symbol( argument.type(), "switch_value", - sideeffects, + side_effects.side_effects, code.source_location(), mode); code_assignt copy_value{ new_symbol.symbol_expr(), argument, code.source_location()}; - convert(copy_value, sideeffects, mode); + convert(copy_value, side_effects.side_effects, mode); argument = new_symbol.symbol_expr(); - new_vars.minimal_scope.push_front( - to_symbol_expr(argument).get_identifier()); + side_effects.add_temporary(to_symbol_expr(argument).get_identifier()); } // save break/default/cases targets @@ -1444,7 +1458,7 @@ void goto_convertt::convert_switch( source_location.set_case_number(std::to_string(case_number)); case_number++; - if(new_vars.minimal_scope.empty()) + if(side_effects.temporaries.empty()) { guard_expr.add_source_location() = source_location; @@ -1459,7 +1473,7 @@ void goto_convertt::convert_switch( goto_programt::targett try_next = tmp_cases.add(goto_programt::make_incomplete_goto( std::move(guard_expr), source_location)); - destruct_locals(new_vars.minimal_scope, tmp_cases, ns); + destruct_locals(side_effects.temporaries, tmp_cases, ns); tmp_cases.add(goto_programt::make_goto( case_pair.first, true_exprt{}, source_location)); goto_programt::targett next_case = @@ -1471,7 +1485,7 @@ void goto_convertt::convert_switch( tmp_cases.add(goto_programt::make_goto( targets.default_target, targets.default_target->source_location())); - dest.destructive_append(sideeffects); + dest.destructive_append(side_effects.side_effects); dest.destructive_append(tmp_cases); dest.destructive_append(tmp); dest.destructive_append(tmp_z); @@ -1514,16 +1528,14 @@ void goto_convertt::convert_return( code.find_source_location()); code_frontend_returnt new_code(code); - needs_destructiont new_vars; + clean_expr_resultt side_effects; if(new_code.has_return_value()) { bool result_is_used = new_code.return_value().type().id() != ID_empty; - goto_programt sideeffects; - new_vars = - clean_expr(new_code.return_value(), sideeffects, mode, result_is_used); - dest.destructive_append(sideeffects); + side_effects = clean_expr(new_code.return_value(), mode, result_is_used); + dest.destructive_append(side_effects.side_effects); // remove void-typed return value if(!result_is_used) @@ -1540,7 +1552,7 @@ void goto_convertt::convert_return( // Now add a 'set return value' instruction to set the return value. dest.add(goto_programt::make_set_return_value( new_code.return_value(), new_code.source_location())); - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, dest, ns); } else { @@ -1673,11 +1685,12 @@ void goto_convertt::convert_ifthenelse( } exprt tmp_guard = code.cond(); - needs_destructiont new_vars = clean_expr(tmp_guard, dest, mode); + clean_expr_resultt side_effects = clean_expr(tmp_guard, mode); + dest.destructive_append(side_effects.side_effects); // convert 'then'-branch goto_programt tmp_then; - destruct_locals(new_vars.minimal_scope, tmp_then, ns); + destruct_locals(side_effects.temporaries, tmp_then, ns); convert(code.then_case(), tmp_then, mode); source_locationt then_end_location = code.then_case().get_statement() == ID_block @@ -1685,7 +1698,7 @@ void goto_convertt::convert_ifthenelse( : code.then_case().source_location(); goto_programt tmp_else; - destruct_locals(new_vars.minimal_scope, tmp_else, ns); + destruct_locals(side_effects.temporaries, tmp_else, ns); source_locationt else_end_location; if(has_else) @@ -1938,13 +1951,14 @@ void goto_convertt::generate_conditional_branch( { // simple branch exprt cond = guard; - needs_destructiont new_vars = clean_expr(cond, dest, mode); + clean_expr_resultt side_effects = clean_expr(cond, mode); + dest.destructive_append(side_effects.side_effects); dest.add(goto_programt::make_goto(target_true, cond, source_location)); goto_programt tmp_destruct; - destruct_locals(new_vars.minimal_scope, tmp_destruct, ns); + destruct_locals(side_effects.temporaries, tmp_destruct, ns); dest.insert_before_swap(target_true, tmp_destruct); - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, dest, ns); } } @@ -2014,17 +2028,18 @@ void goto_convertt::generate_conditional_branch( } exprt cond = guard; - needs_destructiont new_vars = clean_expr(cond, dest, mode); + clean_expr_resultt side_effects = clean_expr(cond, mode); + dest.destructive_append(side_effects.side_effects); // true branch dest.add(goto_programt::make_goto(target_true, cond, source_location)); goto_programt tmp_destruct; - destruct_locals(new_vars.minimal_scope, tmp_destruct, ns); + destruct_locals(side_effects.temporaries, tmp_destruct, ns); dest.insert_before_swap(target_true, tmp_destruct); // false branch dest.add(goto_programt::make_goto(target_false, source_location)); - destruct_locals(new_vars.minimal_scope, tmp_destruct, ns); + destruct_locals(side_effects.temporaries, tmp_destruct, ns); dest.insert_before_swap(target_false, tmp_destruct); } diff --git a/src/ansi-c/goto-conversion/goto_convert_class.h b/src/ansi-c/goto-conversion/goto_convert_class.h index 750eb2a07ac..600938751f3 100644 --- a/src/ansi-c/goto-conversion/goto_convert_class.h +++ b/src/ansi-c/goto-conversion/goto_convert_class.h @@ -56,19 +56,29 @@ class goto_convertt : public messaget std::string tmp_symbol_prefix; lifetimet lifetime = lifetimet::STATIC_GLOBAL; - struct needs_destructiont + struct clean_expr_resultt { - std::list minimal_scope; - - needs_destructiont() = default; - - explicit needs_destructiont(irep_idt id) : minimal_scope({id}) + /// Identifiers of temporaries introduced while cleaning an expression. The + /// caller needs to add destructors for these (via `destruct_locals`) on all + /// control-flow paths as soon as the temporaries are no longer needed. + std::list temporaries; + /// Statements implementing side effects of the expression that was subject + /// to cleaning. The caller needs to merge (typically via + /// `destructive_append`) these statements into the destination GOTO + /// program. + goto_programt side_effects; + + clean_expr_resultt() = default; + + void add(clean_expr_resultt &&other) { + temporaries.splice(temporaries.begin(), other.temporaries); + side_effects.destructive_append(other.side_effects); } - void add(needs_destructiont &&other) + void add_temporary(const irep_idt &id) { - minimal_scope.splice(minimal_scope.begin(), other.minimal_scope); + temporaries.push_front(id); } }; @@ -97,14 +107,11 @@ class goto_convertt : public messaget // into the program logic // - [[nodiscard]] needs_destructiont clean_expr( - exprt &expr, - goto_programt &dest, - const irep_idt &mode, - bool result_is_used = true); + [[nodiscard]] clean_expr_resultt + clean_expr(exprt &expr, const irep_idt &mode, bool result_is_used = true); - [[nodiscard]] needs_destructiont - clean_expr_address_of(exprt &expr, goto_programt &dest, const irep_idt &mode); + [[nodiscard]] clean_expr_resultt + clean_expr_address_of(exprt &expr, const irep_idt &mode); static bool needs_cleaning(const exprt &expr); @@ -125,58 +132,46 @@ class goto_convertt : public messaget void rewrite_boolean(exprt &dest); - [[nodiscard]] needs_destructiont remove_side_effect( + [[nodiscard]] clean_expr_resultt remove_side_effect( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used, bool address_taken); - [[nodiscard]] needs_destructiont remove_assignment( + [[nodiscard]] clean_expr_resultt remove_assignment( side_effect_exprt &expr, - goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode); - [[nodiscard]] needs_destructiont remove_pre( + [[nodiscard]] clean_expr_resultt remove_pre( side_effect_exprt &expr, - goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode); - [[nodiscard]] needs_destructiont remove_post( + [[nodiscard]] clean_expr_resultt remove_post( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used); - [[nodiscard]] needs_destructiont remove_function_call( + [[nodiscard]] clean_expr_resultt remove_function_call( side_effect_expr_function_callt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used); - [[nodiscard]] needs_destructiont remove_cpp_new( + [[nodiscard]] clean_expr_resultt + remove_cpp_new(side_effect_exprt &expr, bool result_is_used); + [[nodiscard]] clean_expr_resultt remove_cpp_delete(side_effect_exprt &expr); + [[nodiscard]] clean_expr_resultt remove_malloc( side_effect_exprt &expr, - goto_programt &dest, - bool result_is_used); - void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest); - [[nodiscard]] needs_destructiont remove_malloc( - side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used); - [[nodiscard]] needs_destructiont - remove_temporary_object(side_effect_exprt &expr, goto_programt &dest); - [[nodiscard]] needs_destructiont remove_statement_expression( + [[nodiscard]] clean_expr_resultt + remove_temporary_object(side_effect_exprt &expr); + [[nodiscard]] clean_expr_resultt remove_statement_expression( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used); - [[nodiscard]] needs_destructiont remove_gcc_conditional_expression( - exprt &expr, - goto_programt &dest, - const irep_idt &mode); - [[nodiscard]] needs_destructiont remove_overflow( + [[nodiscard]] clean_expr_resultt + remove_gcc_conditional_expression(exprt &expr, const irep_idt &mode); + [[nodiscard]] clean_expr_resultt remove_overflow( side_effect_expr_overflowt &expr, - goto_programt &dest, bool result_is_used, const irep_idt &mode); diff --git a/src/ansi-c/goto-conversion/goto_convert_function_call.cpp b/src/ansi-c/goto-conversion/goto_convert_function_call.cpp index badf8384a26..2fdc5c3e616 100644 --- a/src/ansi-c/goto-conversion/goto_convert_function_call.cpp +++ b/src/ansi-c/goto-conversion/goto_convert_function_call.cpp @@ -43,15 +43,17 @@ void goto_convertt::do_function_call( exprt::operandst new_arguments = arguments; - needs_destructiont new_vars; + clean_expr_resultt side_effects; if(!new_lhs.is_nil()) - new_vars.add(clean_expr(new_lhs, dest, mode)); + side_effects.add(clean_expr(new_lhs, mode)); - new_vars.add(clean_expr(new_function, dest, mode)); + side_effects.add(clean_expr(new_function, mode)); for(auto &new_argument : new_arguments) - new_vars.add(clean_expr(new_argument, dest, mode)); + side_effects.add(clean_expr(new_argument, mode)); + + dest.destructive_append(side_effects.side_effects); // split on the function @@ -83,7 +85,7 @@ void goto_convertt::do_function_call( function.find_source_location()); } - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, dest, ns); } void goto_convertt::do_function_call_if( diff --git a/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp b/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp index 61a8587fe0a..28943332d12 100644 --- a/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp +++ b/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp @@ -24,9 +24,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "destructor.h" -goto_convertt::needs_destructiont goto_convertt::remove_assignment( +goto_convertt::clean_expr_resultt goto_convertt::remove_assignment( side_effect_exprt &expr, - goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode) @@ -35,7 +34,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment( std::optional replacement_expr_opt; - needs_destructiont new_vars; + clean_expr_resultt side_effects; if(statement == ID_assign) { @@ -48,8 +47,8 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment( { if(!old_assignment.rhs().is_constant()) { - new_vars.minimal_scope.push_front( - make_temp_symbol(old_assignment.rhs(), "assign", dest, mode)); + side_effects.add_temporary(make_temp_symbol( + old_assignment.rhs(), "assign", side_effects.side_effects, mode)); } replacement_expr_opt = @@ -61,7 +60,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment( code_assignt new_assignment(std::move(new_lhs), std::move(new_rhs)); new_assignment.add_source_location() = expr.source_location(); - convert_assign(new_assignment, dest, mode); + convert_assign(new_assignment, side_effects.side_effects, mode); } else if( statement == ID_assign_plus || statement == ID_assign_minus || @@ -120,8 +119,8 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment( result_is_used && !address_taken && assignment_lhs_needs_temporary(binary_expr.op0())) { - new_vars.minimal_scope.push_front( - make_temp_symbol(rhs, "assign", dest, mode)); + side_effects.add_temporary( + make_temp_symbol(rhs, "assign", side_effects.side_effects, mode)); replacement_expr_opt = typecast_exprt::conditional_cast(rhs, new_lhs.type()); } @@ -131,7 +130,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment( code_assignt assignment(new_lhs, rhs); assignment.add_source_location() = expr.source_location(); - convert(assignment, dest, mode); + convert(assignment, side_effects.side_effects, mode); } else UNREACHABLE; @@ -143,10 +142,11 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment( typecast_exprt::conditional_cast(*replacement_expr_opt, expr.type()); expr.swap(new_lhs); - return new_vars; + return side_effects; } - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, side_effects.side_effects, ns); + side_effects.temporaries.clear(); if(result_is_used) { @@ -173,12 +173,11 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment( else expr.make_nil(); - return {}; + return side_effects; } -goto_convertt::needs_destructiont goto_convertt::remove_pre( +goto_convertt::clean_expr_resultt goto_convertt::remove_pre( side_effect_exprt &expr, - goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode) @@ -242,14 +241,15 @@ goto_convertt::needs_destructiont goto_convertt::remove_pre( const bool cannot_use_lhs = result_is_used && !address_taken && assignment_lhs_needs_temporary(lhs); - needs_destructiont new_vars; + clean_expr_resultt side_effects; if(cannot_use_lhs) - new_vars.minimal_scope.push_front(make_temp_symbol(rhs, "pre", dest, mode)); + side_effects.add_temporary( + make_temp_symbol(rhs, "pre", side_effects.side_effects, mode)); code_assignt assignment(lhs, rhs); assignment.add_source_location() = expr.find_source_location(); - convert(assignment, dest, mode); + convert(assignment, side_effects.side_effects, mode); if(result_is_used) { @@ -268,12 +268,11 @@ goto_convertt::needs_destructiont goto_convertt::remove_pre( else expr.make_nil(); - return new_vars; + return side_effects; } -goto_convertt::needs_destructiont goto_convertt::remove_post( +goto_convertt::clean_expr_resultt goto_convertt::remove_post( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used) { @@ -334,7 +333,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_post( // fix up the expression, if needed - needs_destructiont new_vars; + clean_expr_resultt side_effects; if(result_is_used) { @@ -346,32 +345,33 @@ goto_convertt::needs_destructiont goto_convertt::remove_post( suffix += "_" + id2string(base_name); } - new_vars.minimal_scope.push_front( - make_temp_symbol(tmp, suffix, dest, mode)); + side_effects.add_temporary( + make_temp_symbol(tmp, suffix, side_effects.side_effects, mode)); expr.swap(tmp); } else expr.make_nil(); - dest.destructive_append(tmp1); - dest.destructive_append(tmp2); + side_effects.side_effects.destructive_append(tmp1); + side_effects.side_effects.destructive_append(tmp2); - return new_vars; + return side_effects; } -goto_convertt::needs_destructiont goto_convertt::remove_function_call( +goto_convertt::clean_expr_resultt goto_convertt::remove_function_call( side_effect_expr_function_callt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used) { + clean_expr_resultt side_effects; + if(!result_is_used) { code_function_callt call(expr.function(), expr.arguments()); call.add_source_location() = expr.source_location(); - convert_function_call(call, dest, mode); + convert_function_call(call, side_effects.side_effects, mode); expr.make_nil(); - return {}; + return side_effects; } // get name of function, if available @@ -398,7 +398,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_function_call( symbol_table); PRECONDITION(expr.type().id() != ID_code); - dest.add( + side_effects.side_effects.add( goto_programt::make_decl(new_symbol.symbol_expr(), new_symbol.location)); { @@ -406,12 +406,14 @@ goto_convertt::needs_destructiont goto_convertt::remove_function_call( code_function_callt call( new_symbol.symbol_expr(), expr.function(), expr.arguments()); call.add_source_location() = new_symbol.location; - convert_function_call(call, dest, mode); + convert_function_call(call, side_effects.side_effects, mode); } static_cast(expr) = new_symbol.symbol_expr(); - return needs_destructiont{to_symbol_expr(expr).get_identifier()}; + side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); + + return side_effects; } void goto_convertt::replace_new_object(const exprt &object, exprt &dest) @@ -423,10 +425,8 @@ void goto_convertt::replace_new_object(const exprt &object, exprt &dest) replace_new_object(object, *it); } -goto_convertt::needs_destructiont goto_convertt::remove_cpp_new( - side_effect_exprt &expr, - goto_programt &dest, - bool result_is_used) +goto_convertt::clean_expr_resultt +goto_convertt::remove_cpp_new(side_effect_exprt &expr, bool result_is_used) { const symbolt &new_symbol = get_fresh_aux_symbol( expr.type(), @@ -436,29 +436,29 @@ goto_convertt::needs_destructiont goto_convertt::remove_cpp_new( ID_cpp, symbol_table); + clean_expr_resultt side_effects; + PRECONDITION(expr.type().id() != ID_code); - dest.add( + side_effects.side_effects.add( goto_programt::make_decl(new_symbol.symbol_expr(), new_symbol.location)); const code_assignt call(new_symbol.symbol_expr(), expr); - convert(call, dest, ID_cpp); + convert(call, side_effects.side_effects, ID_cpp); if(result_is_used) { static_cast(expr) = new_symbol.symbol_expr(); - return needs_destructiont{to_symbol_expr(expr).get_identifier()}; + side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); } else - { expr.make_nil(); - return {}; - } + + return side_effects; } -void goto_convertt::remove_cpp_delete( - side_effect_exprt &expr, - goto_programt &dest) +goto_convertt::clean_expr_resultt +goto_convertt::remove_cpp_delete(side_effect_exprt &expr) { DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expects one operand"); @@ -467,17 +467,21 @@ void goto_convertt::remove_cpp_delete( tmp.copy_to_operands(to_unary_expr(expr).op()); tmp.set(ID_destructor, expr.find(ID_destructor)); - convert_cpp_delete(tmp, dest); + clean_expr_resultt side_effects; + convert_cpp_delete(tmp, side_effects.side_effects); expr.make_nil(); + + return side_effects; } -goto_convertt::needs_destructiont goto_convertt::remove_malloc( +goto_convertt::clean_expr_resultt goto_convertt::remove_malloc( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used) { + clean_expr_resultt side_effects; + if(result_is_used) { const symbolt &new_symbol = get_fresh_aux_symbol( @@ -490,44 +494,47 @@ goto_convertt::needs_destructiont goto_convertt::remove_malloc( code_frontend_declt decl(new_symbol.symbol_expr()); decl.add_source_location() = new_symbol.location; - convert_frontend_decl(decl, dest, mode); + convert_frontend_decl(decl, side_effects.side_effects, mode); code_assignt call(new_symbol.symbol_expr(), expr); call.add_source_location() = expr.source_location(); static_cast(expr) = new_symbol.symbol_expr(); - convert(call, dest, mode); + convert(call, side_effects.side_effects, mode); - return needs_destructiont{to_symbol_expr(expr).get_identifier()}; + side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); } else - { - convert(code_expressiont(std::move(expr)), dest, mode); + convert(code_expressiont(std::move(expr)), side_effects.side_effects, mode); - return {}; - } + return side_effects; } -goto_convertt::needs_destructiont goto_convertt::remove_temporary_object( - side_effect_exprt &expr, - goto_programt &dest) +goto_convertt::clean_expr_resultt +goto_convertt::remove_temporary_object(side_effect_exprt &expr) { + clean_expr_resultt side_effects; + const irep_idt &mode = expr.get(ID_mode); INVARIANT_WITH_DIAGNOSTICS( expr.operands().size() <= 1, "temporary_object takes zero or one operands", expr.find_source_location()); - symbolt &new_symbol = - new_tmp_symbol(expr.type(), "obj", dest, expr.find_source_location(), mode); + symbolt &new_symbol = new_tmp_symbol( + expr.type(), + "obj", + side_effects.side_effects, + expr.find_source_location(), + mode); if(expr.operands().size() == 1) { const code_assignt assignment( new_symbol.symbol_expr(), to_unary_expr(expr).op()); - convert(assignment, dest, mode); + convert(assignment, side_effects.side_effects, mode); } if(expr.find(ID_initializer).is_not_nil()) @@ -539,20 +546,23 @@ goto_convertt::needs_destructiont goto_convertt::remove_temporary_object( exprt initializer = static_cast(expr.find(ID_initializer)); replace_new_object(new_symbol.symbol_expr(), initializer); - convert(to_code(initializer), dest, mode); + convert(to_code(initializer), side_effects.side_effects, mode); } static_cast(expr) = new_symbol.symbol_expr(); - return needs_destructiont{to_symbol_expr(expr).get_identifier()}; + side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); + + return side_effects; } -goto_convertt::needs_destructiont goto_convertt::remove_statement_expression( +goto_convertt::clean_expr_resultt goto_convertt::remove_statement_expression( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used) { + clean_expr_resultt side_effects; + // This is a gcc extension of the form ({ ....; expr; }) // The value is that of the final expression. // The expression is copied into a temporary before the @@ -562,9 +572,9 @@ goto_convertt::needs_destructiont goto_convertt::remove_statement_expression( if(!result_is_used) { - convert(code, dest, mode); + convert(code, side_effects.side_effects, mode); expr.make_nil(); - return {}; + return side_effects; } INVARIANT_WITH_DIAGNOSTICS( @@ -583,7 +593,11 @@ goto_convertt::needs_destructiont goto_convertt::remove_statement_expression( source_locationt source_location = last.find_source_location(); symbolt &new_symbol = new_tmp_symbol( - expr.type(), "statement_expression", dest, source_location, mode); + expr.type(), + "statement_expression", + side_effects.side_effects, + source_location, + mode); symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type); tmp_symbol_expr.add_source_location() = source_location; @@ -607,20 +621,17 @@ goto_convertt::needs_destructiont goto_convertt::remove_statement_expression( UNREACHABLE; } - { - goto_programt tmp; - convert(code, tmp, mode); - dest.destructive_append(tmp); - } + convert(code, side_effects.side_effects, mode); static_cast(expr) = tmp_symbol_expr; - return needs_destructiont{to_symbol_expr(expr).get_identifier()}; + side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); + + return side_effects; } -goto_convertt::needs_destructiont goto_convertt::remove_overflow( +goto_convertt::clean_expr_resultt goto_convertt::remove_overflow( side_effect_expr_overflowt &expr, - goto_programt &dest, bool result_is_used, const irep_idt &mode) { @@ -629,14 +640,14 @@ goto_convertt::needs_destructiont goto_convertt::remove_overflow( const exprt &rhs = expr.rhs(); const exprt &result = expr.result(); - needs_destructiont new_vars; + clean_expr_resultt side_effects; if(result.type().id() != ID_pointer) { // result of the arithmetic operation is _not_ used, just evaluate side // effects exprt tmp = result; - new_vars.add(clean_expr(tmp, dest, mode, false)); + side_effects.add(clean_expr(tmp, mode, false)); // the is-there-an-overflow result may be used if(result_is_used) @@ -667,8 +678,11 @@ goto_convertt::needs_destructiont goto_convertt::remove_overflow( if(result_is_used) { - new_vars.minimal_scope.push_front( - make_temp_symbol(overflow_with_result, "overflow_result", dest, mode)); + side_effects.add_temporary(make_temp_symbol( + overflow_with_result, + "overflow_result", + side_effects.side_effects, + mode)); } const struct_typet::componentst &result_comps = @@ -679,7 +693,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_overflow( typecast_exprt::conditional_cast( member_exprt{overflow_with_result, result_comps[0]}, arith_type), expr.source_location()}; - convert_assign(result_assignment, dest, mode); + convert_assign(result_assignment, side_effects.side_effects, mode); if(result_is_used) { @@ -692,12 +706,11 @@ goto_convertt::needs_destructiont goto_convertt::remove_overflow( expr.make_nil(); } - return new_vars; + return side_effects; } -goto_convertt::needs_destructiont goto_convertt::remove_side_effect( +goto_convertt::clean_expr_resultt goto_convertt::remove_side_effect( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used, bool address_taken) @@ -707,7 +720,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_side_effect( if(statement == ID_function_call) { return remove_function_call( - to_side_effect_expr_function_call(expr), dest, mode, result_is_used); + to_side_effect_expr_function_call(expr), mode, result_is_used); } else if( statement == ID_assign || statement == ID_assign_plus || @@ -717,36 +730,35 @@ goto_convertt::needs_destructiont goto_convertt::remove_side_effect( statement == ID_assign_lshr || statement == ID_assign_ashr || statement == ID_assign_shl || statement == ID_assign_mod) { - return remove_assignment(expr, dest, result_is_used, address_taken, mode); + return remove_assignment(expr, result_is_used, address_taken, mode); } else if(statement == ID_postincrement || statement == ID_postdecrement) { - return remove_post(expr, dest, mode, result_is_used); + return remove_post(expr, mode, result_is_used); } else if(statement == ID_preincrement || statement == ID_predecrement) { - return remove_pre(expr, dest, result_is_used, address_taken, mode); + return remove_pre(expr, result_is_used, address_taken, mode); } else if(statement == ID_cpp_new || statement == ID_cpp_new_array) { - return remove_cpp_new(expr, dest, result_is_used); + return remove_cpp_new(expr, result_is_used); } else if(statement == ID_cpp_delete || statement == ID_cpp_delete_array) { - remove_cpp_delete(expr, dest); - return {}; + return remove_cpp_delete(expr); } else if(statement == ID_allocate) { - return remove_malloc(expr, dest, mode, result_is_used); + return remove_malloc(expr, mode, result_is_used); } else if(statement == ID_temporary_object) { - return remove_temporary_object(expr, dest); + return remove_temporary_object(expr); } else if(statement == ID_statement_expression) { - return remove_statement_expression(expr, dest, mode, result_is_used); + return remove_statement_expression(expr, mode, result_is_used); } else if(statement == ID_nondet) { @@ -760,23 +772,25 @@ goto_convertt::needs_destructiont goto_convertt::remove_side_effect( } else if(statement == ID_throw) { + clean_expr_resultt side_effects; + codet code = code_expressiont(side_effect_expr_throwt( expr.find(ID_exception_list), expr.type(), expr.source_location())); code.op0().operands().swap(expr.operands()); code.add_source_location() = expr.source_location(); - dest.add(goto_programt::instructiont( + side_effects.side_effects.add(goto_programt::instructiont( std::move(code), expr.source_location(), THROW, nil_exprt(), {})); // the result can't be used, these are void expr.make_nil(); - return {}; + return side_effects; } else if( statement == ID_overflow_plus || statement == ID_overflow_minus || statement == ID_overflow_mult) { return remove_overflow( - to_side_effect_expr_overflow(expr), dest, result_is_used, mode); + to_side_effect_expr_overflow(expr), result_is_used, mode); } else { diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index b25f43467d8..b6e859c1fdc 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -46,7 +46,9 @@ class cleanert : public goto_convertt [[nodiscard]] std::list clean(exprt &guard, goto_programt &dest, const irep_idt &mode) { - return goto_convertt::clean_expr(guard, dest, mode, true).minimal_scope; + auto clean_result = goto_convertt::clean_expr(guard, mode, true); + dest.destructive_append(clean_result.side_effects); + return clean_result.temporaries; } void do_havoc_slice(