Symex guards: avoid unnecessary duplicate negation

We negated the right-hand side assigned to a guard symbol just so as to
then negate the use of the guard symbol. Remove this duplicate negation.

Author: tautschnig

regression/cbmc-cover/pointer-function-parameters/test.desc

@@ -5,7 +5,7 @@ main.c
 ^Test suite:$
 ^(tmp(\$\d+)?=[^,]*, a=\(\(signed int \*\)NULL\))|(a=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*)$
 ^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=4)|(tmp(\$\d+)?=4, a=&tmp(\$\d+)?!0@1)$
-^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+))|(tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+), a=&tmp(\$\d+)?!0@1)$
+^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=(-?[012356789][0-9]*|4[0-9]+))|(tmp(\$\d+)?=(-?[012356789][0-9]*|4[0-9]+), a=&tmp(\$\d+)?!0@1)$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc

@@ -13,26 +13,26 @@ test::1::unconditionally_reachable_7[^\s]+ = 7$
 test::1::unconditionally_reachable_8[^\s]+ = 7$
 test::1::unconditionally_reachable_9[^\s]+ = 7$
 test::1::unconditionally_reachable_10[^\s]+ = 7$
-test::1::possibly_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_1[^\s]+\)$
-test::1::possibly_reachable_2[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_2[^\s]+\)$
-test::1::possibly_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_3[^\s]+\)$
-test::1::possibly_reachable_4[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_4[^\s]+\)$
-test::1::possibly_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_5[^\s]+\)$
-test::1::possibly_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_6[^\s]+\)$
-test::1::possibly_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_7[^\s]+\)$
+test::1::possibly_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_1[^\s]+ : 7\)$
+test::1::possibly_reachable_2[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_2[^\s]+ : 7\)$
+test::1::possibly_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_3[^\s]+ : 7\)$
+test::1::possibly_reachable_4[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_4[^\s]+ : 7\)$
+test::1::possibly_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_5[^\s]+ : 7\)$
+test::1::possibly_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_6[^\s]+ : 7\)$
+test::1::possibly_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_7[^\s]+ : 7\)$
 --
-test::1::unconditionally_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_1[^\s]+\)$
-test::1::unconditionally_reachable_2[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_2[^\s]+\)$
-test::1::unconditionally_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_3[^\s]+\)$
-test::1::unconditionally_reachable_4[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_4[^\s]+\)$
-test::1::unconditionally_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_5[^\s]+\)$
-test::1::unconditionally_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_6[^\s]+\)$
-test::1::unconditionally_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_7[^\s]+\)$
-test::1::unconditionally_reachable_8[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_8[^\s]+\)$
-test::1::unconditionally_reachable_9[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_9[^\s]+\)$
-test::1::unconditionally_reachable_10[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_10[^\s]+\)$
-test::1::unconditionally_reachable_11[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_11[^\s]+\)$
-test::1::unconditionally_reachable_12[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_12[^\s]+\)$
+test::1::unconditionally_reachable_1[^\s]+ = .+ \?
+test::1::unconditionally_reachable_2[^\s]+ = .+ \?
+test::1::unconditionally_reachable_3[^\s]+ = .+ \?
+test::1::unconditionally_reachable_4[^\s]+ = .+ \?
+test::1::unconditionally_reachable_5[^\s]+ = .+ \?
+test::1::unconditionally_reachable_6[^\s]+ = .+ \?
+test::1::unconditionally_reachable_7[^\s]+ = .+ \?
+test::1::unconditionally_reachable_8[^\s]+ = .+ \?
+test::1::unconditionally_reachable_9[^\s]+ = .+ \?
+test::1::unconditionally_reachable_10[^\s]+ = .+ \?
+test::1::unconditionally_reachable_11[^\s]+ = .+ \?
+test::1::unconditionally_reachable_12[^\s]+ = .+ \?
 test::1::unreachable_1[^\s]+ = 7$
 test::1::unreachable_2[^\s]+ = 7$
 test::1::unreachable_3[^\s]+ = 7$

regression/cbmc/unreachable-goto2/test-vccs.desc

@@ -2,7 +2,7 @@ CORE paths-lifo-expected-failure
 test.c
 --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
-^\{1\} goto_symex::\\guard#1$
+^\{1\} ¬goto_symex::\\guard#1$
 ^EXIT=0$
 ^SIGNAL=0$
 --

src/goto-symex/symex_goto.cpp

@@ -490,12 +490,11 @@ void goto_symext::symex_goto(statet &state)
     {
       symbol_exprt guard_symbol_expr =
         symbol_exprt(statet::guard_identifier(), bool_typet());
-      exprt new_rhs = boolean_negate(new_guard);
 
       ssa_exprt new_lhs =
         state.rename_ssa<L1>(ssa_exprt{guard_symbol_expr}, ns).get();
       new_lhs =
-        state.assignment(std::move(new_lhs), new_rhs, ns, true, false).get();
+        state.assignment(std::move(new_lhs), new_guard, ns, true, false).get();
 
       guardt guard{true_exprt{}, guard_manager};
 
@@ -509,12 +508,14 @@ void goto_symext::symex_goto(statet &state)
 
       target.assignment(
         guard.as_expr(),
-        new_lhs, new_lhs, guard_symbol_expr,
-        new_rhs,
+        new_lhs,
+        new_lhs,
+        guard_symbol_expr,
+        new_guard,
         original_source,
         symex_targett::assignment_typet::GUARD);
 
-      guard_expr = state.rename(boolean_negate(guard_symbol_expr), ns).get();
+      guard_expr = state.rename(guard_symbol_expr, ns).get();
     }
 
     if(state.has_saved_jump_target)