weaken goto_convertt::needs_cleaning

Both dereference and index expressions are no longer lifted out of
expressions using temporaries during conversion into the goto program.

Author: kroening

regression/cbmc-cover/Quantifiers-not-exists/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover location
 ^\*\* 1 of 46 covered \(2.2%\)

regression/cbmc/Quantifiers-not-exists/fixed.desc

@@ -3,11 +3,11 @@ fixed.c
 
 ^\*\* Results:$
 ^\[main.assertion.5\] line 31 assertion a\[.*\]\[.*\] > 10: SUCCESS$
-^\[main.assertion.6\] line 33 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.7\] line 34 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.8\] line 36 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.9\] line 38 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.10\] line 39 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.6\] line 33 assertion .*: SUCCESS$
+^\[main.assertion.7\] line 34 assertion .*: SUCCESS$
+^\[main.assertion.8\] line 36 assertion .*: SUCCESS$
+^\[main.assertion.9\] line 38 assertion .*: SUCCESS$
+^\[main.assertion.10\] line 39 assertion .*: SUCCESS$
 ^\*\* 4 of 10 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$

regression/cbmc/Quantifiers-two-dimension-array/fixed.desc

@@ -6,7 +6,7 @@ fixed.c
 ^\[main.assertion.2\] line 15 assertion a\[.*\]\[.*\] == 1: SUCCESS$
 ^\[main.assertion.3\] line 16 assertion a\[.*\]\[.*\] == 1: SUCCESS$
 ^\[main.assertion.4\] line 17 assertion a\[.*\]\[.*\] == 2: SUCCESS$
-^\[main.assertion.5\] line 18 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.5\] line 18 assertion .*: SUCCESS$
 ^\*\* 0 of 5 failed
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$

regression/cbmc/Quantifiers-two-dimension-array/test.desc

@@ -6,7 +6,7 @@ main.c
 ^\[main.assertion.2\] line 13 assertion a\[.*\]\[.*\] == 1: SUCCESS$
 ^\[main.assertion.3\] line 14 assertion a\[.*\]\[.*\] == 1: SUCCESS$
 ^\[main.assertion.4\] line 15 assertion a\[.*\]\[.*\] == 2: SUCCESS$
-^\[main.assertion.5\] line 16 assertion tmp_if_expr\$\d+: FAILURE$
+^\[main.assertion.5\] line 16 assertion .*: FAILURE$
 ^\*\* 1 of 5 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$

regression/cbmc/Quantifiers-type2/test.desc

@@ -2,8 +2,8 @@ CORE
 main.c
 
 ^\*\* Results:$
-^\[main.assertion.1\] line 12 assertion tmp_if_expr(\$\d+)?: SUCCESS$
-^\[main.assertion.2\] line 13 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.1\] line 12 assertion b\[.*0\] == 10 && b\[.*1\] == 10: SUCCESS$
+^\[main.assertion.2\] line 13 assertion c\[.*0\] == 10 && c\[.*1\] == 10: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

regression/contracts/assigns_validity_pointer_01/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz
 ^EXIT=0$

regression/contracts/assigns_validity_pointer_04/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz _ --pointer-primitive-check
 ^EXIT=10$

regression/contracts/history-pointer-enforce-03/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --enforce-contract foo
 ^EXIT=0$

regression/contracts/history-pointer-enforce-04/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --enforce-contract foo
 ^EXIT=0$

regression/contracts/history-pointer-enforce-05/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --enforce-contract foo
 ^EXIT=10$

regression/goto-analyzer/constant_propagation_08/test-vsd.desc

@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --vsd-arrays every-element --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 2, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 3, assigns: 14, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 2, assigns: 12, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/pointer-comparison-same-target-non-det/test-value-set.desc

@@ -4,20 +4,20 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* assertion p == q: FAILURE
-^\[main.assertion.2\] .* assertion p == r: FAILURE
+^\[main.assertion.2\] .* assertion p == r: UNKNOWN
 ^\[main.assertion.3\] .* assertion q == r: UNKNOWN
 ^\[main.assertion.4\] .* assertion p != q: SUCCESS
-^\[main.assertion.5\] .* assertion p != r: SUCCESS
+^\[main.assertion.5\] .* assertion p != r: UNKNOWN
 ^\[main.assertion.6\] .* assertion q != r: UNKNOWN
 ^\[main.assertion.7\] .* assertion p < q: SUCCESS
-^\[main.assertion.8\] .* assertion p < r: SUCCESS
+^\[main.assertion.8\] .* assertion p < r: UNKNOWN
 ^\[main.assertion.9\] .* assertion q < r: UNKNOWN
 ^\[main.assertion.10\] .* assertion p <= q: SUCCESS
-^\[main.assertion.11\] .* assertion p <= r: SUCCESS
-^\[main.assertion.12\] .* assertion q <= r: SUCCESS
+^\[main.assertion.11\] .* assertion p <= r: UNKNOWN
+^\[main.assertion.12\] .* assertion q <= r: UNKNOWN
 ^\[main.assertion.13\] .* assertion p > q: FAILURE
-^\[main.assertion.14\] .* assertion p > r: FAILURE
-^\[main.assertion.15\] .* assertion q > r: FAILURE
+^\[main.assertion.14\] .* assertion p > r: UNKNOWN
+^\[main.assertion.15\] .* assertion q > r: UNKNOWN
 ^\[main.assertion.16\] .* assertion p >= q: FAILURE
-^\[main.assertion.17\] .* assertion p >= r: FAILURE
+^\[main.assertion.17\] .* assertion p >= r: UNKNOWN
 ^\[main.assertion.18\] .* assertion q >= r: UNKNOWN

src/goto-programs/goto_clean_expr.cpp

@@ -59,23 +59,17 @@ symbol_exprt goto_convertt::make_compound_literal(
   return result;
 }
 
+/// Returns 'true' for expressions that may change the program
+/// state.
+/// Expressions that may trigger undefined behavior
+/// (e.g., dereference, index, division) are deliberately not
+/// included.
 bool goto_convertt::needs_cleaning(const exprt &expr)
 {
-  if(expr.id()==ID_dereference ||
-     expr.id()==ID_side_effect ||
-     expr.id()==ID_compound_literal ||
-     expr.id()==ID_comma)
-    return true;
-
-  if(expr.id()==ID_index)
+  if(
+    expr.id() == ID_side_effect || expr.id() == ID_compound_literal ||
+    expr.id() == ID_comma)
   {
-    // Will usually clean index expressions because of possible
-    // memory violation in case of out-of-bounds indices.
-    // We do an exception for "string-lit"[0], which is safe.
-    if(to_index_expr(expr).array().id()==ID_string_constant &&
-       to_index_expr(expr).index().is_zero())
-      return false;
-
     return true;
   }