Merge pull request #7051 from diffblue/shortcircuit2

Simplify goto-program generated for short-circuit operators

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;
   }
 
@@ -384,7 +378,7 @@ void goto_convertt::clean_expr(
         clean_expr(side_effect_assign.lhs(), dest, mode);
         exprt lhs = side_effect_assign.lhs();
 
-        const bool must_use_rhs = needs_cleaning(lhs);
+        const bool must_use_rhs = assignment_lhs_needs_temporary(lhs);
         if(must_use_rhs)
         {
           remove_function_call(

src/goto-programs/goto_convert_class.h

@@ -89,6 +89,15 @@ class goto_convertt:public messaget
 
   static bool needs_cleaning(const exprt &expr);
 
+  // Do we need to introduce a temporary for the value of an assignment
+  // to the given lhs? E.g., a[i] needs a temporary as its value may change
+  // when i is changed; likewise, *p needs a temporary as its value may change
+  // when p is changed.
+  static bool assignment_lhs_needs_temporary(const exprt &lhs)
+  {
+    return lhs.id() != ID_symbol;
+  }
+
   void make_temp_symbol(
     exprt &expr,
     const std::string &suffix,

src/goto-programs/goto_convert_side_effect.cpp

@@ -50,7 +50,9 @@ void goto_convertt::remove_assignment(
   {
     auto &old_assignment = to_side_effect_expr_assign(expr);
 
-    if(result_is_used && !address_taken && needs_cleaning(old_assignment.lhs()))
+    if(
+      result_is_used && !address_taken &&
+      assignment_lhs_needs_temporary(old_assignment.lhs()))
     {
       if(!old_assignment.rhs().is_constant())
         make_temp_symbol(old_assignment.rhs(), "assign", dest, mode);
@@ -122,7 +124,9 @@ void goto_convertt::remove_assignment(
     exprt rhs = binary_exprt{binary_expr.op0(), new_id, binary_expr.op1()};
     rhs.add_source_location() = expr.source_location();
 
-    if(result_is_used && !address_taken && needs_cleaning(binary_expr.op0()))
+    if(
+      result_is_used && !address_taken &&
+      assignment_lhs_needs_temporary(binary_expr.op0()))
     {
       make_temp_symbol(rhs, "assign", dest, mode);
       replacement_expr_opt = rhs;
@@ -237,7 +241,7 @@ void goto_convertt::remove_pre(
   }
 
   const bool cannot_use_lhs =
-    result_is_used && !address_taken && needs_cleaning(lhs);
+    result_is_used && !address_taken && assignment_lhs_needs_temporary(lhs);
   if(cannot_use_lhs)
     make_temp_symbol(rhs, "pre", dest, mode);