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.

Author: tautschnig

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

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.

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\*\)\)\)$
 --

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\]
 --

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\]
 --

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\]
 --

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\]
 --

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\]
 --

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\]
 --

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\]
 --