Skip to content

Commit 150402c

Browse files
tautschnigtautschnig
committed
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.
1 parent 2d63a71 commit 150402c

File tree

5 files changed

+30
-29
lines changed

5 files changed

+30
-29
lines changed

‎jbmc/regression/jbmc/symex_complexity/process.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
ComplexClass
3-
--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`
4-
^\[symex-complexity\] Branch considered too complex|\[symex-complexity\] Trying to enter blacklisted loop|\[symex-complexity\] Loop operations considered too complex$
3+
--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`
4+
^\[symex-complexity\] Branch considered too complex|\[symex-complexity\] Trying to enter blacklisted loop|\[symex-complexity\] Loop operations considered too complex
55
^EXIT=10$
66
^SIGNAL=0$
77
^VERIFICATION FAILED$
@@ -15,4 +15,4 @@ Loop blacklisting.
1515

1616
When these don't work this test may take some time to run (and then fail), which is hard to
1717
restrict because this is the problem this feature is meant to solve. If this test is running
18-
slowly, high chance something has gone wrong.
18+
slowly, high chance something has gone wrong.

‎regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc

+19-19
Original file line numberDiff line numberDiff line change
@@ -13,26 +13,26 @@ test::1::unconditionally_reachable_7[^\s]+ = 7$
1313
test::1::unconditionally_reachable_8[^\s]+ = 7$
1414
test::1::unconditionally_reachable_9[^\s]+ = 7$
1515
test::1::unconditionally_reachable_10[^\s]+ = 7$
16-
test::1::possibly_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_1[^\s]+\)$
17-
test::1::possibly_reachable_2[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_2[^\s]+\)$
18-
test::1::possibly_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_3[^\s]+\)$
19-
test::1::possibly_reachable_4[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_4[^\s]+\)$
20-
test::1::possibly_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_5[^\s]+\)$
21-
test::1::possibly_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_6[^\s]+\)$
22-
test::1::possibly_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_7[^\s]+\)$
16+
test::1::possibly_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_1[^\s]+ : 7\)$
17+
test::1::possibly_reachable_2[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_2[^\s]+ : 7\)$
18+
test::1::possibly_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_3[^\s]+ : 7\)$
19+
test::1::possibly_reachable_4[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_4[^\s]+ : 7\)$
20+
test::1::possibly_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_5[^\s]+ : 7\)$
21+
test::1::possibly_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_6[^\s]+ : 7\)$
22+
test::1::possibly_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_7[^\s]+ : 7\)$
2323
--
24-
test::1::unconditionally_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_1[^\s]+\)$
25-
test::1::unconditionally_reachable_2[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_2[^\s]+\)$
26-
test::1::unconditionally_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_3[^\s]+\)$
27-
test::1::unconditionally_reachable_4[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_4[^\s]+\)$
28-
test::1::unconditionally_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_5[^\s]+\)$
29-
test::1::unconditionally_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_6[^\s]+\)$
30-
test::1::unconditionally_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_7[^\s]+\)$
31-
test::1::unconditionally_reachable_8[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_8[^\s]+\)$
32-
test::1::unconditionally_reachable_9[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_9[^\s]+\)$
33-
test::1::unconditionally_reachable_10[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_10[^\s]+\)$
34-
test::1::unconditionally_reachable_11[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_11[^\s]+\)$
35-
test::1::unconditionally_reachable_12[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_12[^\s]+\)$
24+
test::1::unconditionally_reachable_1[^\s]+ = .+ \?
25+
test::1::unconditionally_reachable_2[^\s]+ = .+ \?
26+
test::1::unconditionally_reachable_3[^\s]+ = .+ \?
27+
test::1::unconditionally_reachable_4[^\s]+ = .+ \?
28+
test::1::unconditionally_reachable_5[^\s]+ = .+ \?
29+
test::1::unconditionally_reachable_6[^\s]+ = .+ \?
30+
test::1::unconditionally_reachable_7[^\s]+ = .+ \?
31+
test::1::unconditionally_reachable_8[^\s]+ = .+ \?
32+
test::1::unconditionally_reachable_9[^\s]+ = .+ \?
33+
test::1::unconditionally_reachable_10[^\s]+ = .+ \?
34+
test::1::unconditionally_reachable_11[^\s]+ = .+ \?
35+
test::1::unconditionally_reachable_12[^\s]+ = .+ \?
3636
test::1::unreachable_1[^\s]+ = 7$
3737
test::1::unreachable_2[^\s]+ = 7$
3838
test::1::unreachable_3[^\s]+ = 7$

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ CORE paths-lifo-expected-failure
22
test.c
33
--show-vcc
44
^Generated 1 VCC\(s\), 1 remaining after simplification$
5-
^\{1\} goto_symex::\\guard#1$
5+
^\{1\} ¬goto_symex::\\guard#1$
66
^EXIT=0$
77
^SIGNAL=0$
88
--

‎regression/solver-hardness/guards/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ main.c
55
^SIGNAL=0$
66
^\[main.assertion.1\] line 12 should fail: FAILURE$
77
^VERIFICATION FAILED$
8-
\{"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":".*"\}\}
8+
\{"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":".*"\}\}
99
--
1010
^warning: ignoring
1111
\{"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":".*"\}\}

‎src/goto-symex/symex_goto.cpp

+6-5
Original file line numberDiff line numberDiff line change
@@ -490,12 +490,11 @@ void goto_symext::symex_goto(statet &state)
490490
{
491491
symbol_exprt guard_symbol_expr =
492492
symbol_exprt(statet::guard_identifier(), bool_typet());
493-
exprt new_rhs = boolean_negate(new_guard);
494493

495494
ssa_exprt new_lhs =
496495
state.rename_ssa<L1>(ssa_exprt{guard_symbol_expr}, ns).get();
497496
new_lhs =
498-
state.assignment(std::move(new_lhs), new_rhs, ns, true, false).get();
497+
state.assignment(std::move(new_lhs), new_guard, ns, true, false).get();
499498

500499
guardt guard{true_exprt{}, guard_manager};
501500

@@ -509,12 +508,14 @@ void goto_symext::symex_goto(statet &state)
509508

510509
target.assignment(
511510
guard.as_expr(),
512-
new_lhs, new_lhs, guard_symbol_expr,
513-
new_rhs,
511+
new_lhs,
512+
new_lhs,
513+
guard_symbol_expr,
514+
new_guard,
514515
original_source,
515516
symex_targett::assignment_typet::GUARD);
516517

517-
guard_expr = state.rename(boolean_negate(guard_symbol_expr), ns).get();
518+
guard_expr = state.rename(guard_symbol_expr, ns).get();
518519
}
519520

520521
if(state.has_saved_jump_target)

0 commit comments

Comments
 (0)