From 150402c70364980f420906c1bb057ed475939c7e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 7 Nov 2023 09:39:11 +0000 Subject: [PATCH] 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. --- .../jbmc/symex_complexity/process.desc | 6 +-- .../test.desc | 38 +++++++++---------- .../cbmc/unreachable-goto2/test-vccs.desc | 2 +- regression/solver-hardness/guards/test.desc | 2 +- src/goto-symex/symex_goto.cpp | 11 +++--- 5 files changed, 30 insertions(+), 29 deletions(-) diff --git a/jbmc/regression/jbmc/symex_complexity/process.desc b/jbmc/regression/jbmc/symex_complexity/process.desc index 4a915b7fce1..da27a208408 100644 --- a/jbmc/regression/jbmc/symex_complexity/process.desc +++ b/jbmc/regression/jbmc/symex_complexity/process.desc @@ -1,7 +1,7 @@ CORE ComplexClass ---function ComplexClass.process --symex-complexity-limit 2 --verbosity 9 --unwind 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` -^\[symex-complexity\] Branch considered too complex|\[symex-complexity\] Trying to enter blacklisted loop|\[symex-complexity\] Loop operations considered too complex$ +--function ComplexClass.process --symex-complexity-limit 1 --verbosity 9 --unwind 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^\[symex-complexity\] Branch considered too complex|\[symex-complexity\] Trying to enter blacklisted loop|\[symex-complexity\] Loop operations considered too complex ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ @@ -15,4 +15,4 @@ Loop blacklisting. When these don't work this test may take some time to run (and then fail), which is hard to restrict because this is the problem this feature is meant to solve. If this test is running -slowly, high chance something has gone wrong. \ No newline at end of file +slowly, high chance something has gone wrong. diff --git a/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc b/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc index d8f0a0e31c7..5be6851caf3 100644 --- a/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc +++ b/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$ diff --git a/regression/cbmc/unreachable-goto2/test-vccs.desc b/regression/cbmc/unreachable-goto2/test-vccs.desc index d18e596fd5f..441a0303e48 100644 --- a/regression/cbmc/unreachable-goto2/test-vccs.desc +++ b/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$ -- diff --git a/regression/solver-hardness/guards/test.desc b/regression/solver-hardness/guards/test.desc index 6eac38ac4c8..a4b68755f03 100644 --- a/regression/solver-hardness/guards/test.desc +++ b/regression/solver-hardness/guards/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^\[main.assertion.1\] line 12 should fail: FAILURE$ ^VERIFICATION FAILED$ -\{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"goto_symex::\\\\guard#1 ∧ goto_symex::\\\\guard#2","Source":\{"file":"main.c","function":"main","line":"\d+","workingDirectory":".*"\}\} +\{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"¬goto_symex::\\\\guard#1 ∧ ¬goto_symex::\\\\guard#2","Source":\{"file":"main.c","function":"main","line":"\d+","workingDirectory":".*"\}\} -- ^warning: ignoring \{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"true","Source":\{"file":"main.c","function":"main","line":"\d+","workingDirectory":".*"\}\} diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 404f04fec72..b964503bb7f 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/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(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)