Skip to content

Commit 92af47a

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 2e6200a commit 92af47a

File tree

5 files changed

+30
-29
lines changed

5 files changed

+30
-29
lines changed

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

Lines changed: 3 additions & 3 deletions
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

Lines changed: 19 additions & 19 deletions
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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ CORE paths-lifo-expected-failure
22
test.c
33
--show-vcc --verbosity 8
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

Lines changed: 1 addition & 1 deletion
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

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -328,12 +328,11 @@ void goto_symext::symex_goto(statet &state)
328328
{
329329
symbol_exprt guard_symbol_expr =
330330
symbol_exprt(statet::guard_identifier(), bool_typet());
331-
exprt new_rhs = boolean_negate(new_guard);
332331

333332
ssa_exprt new_lhs =
334333
state.rename_ssa<L1>(ssa_exprt{guard_symbol_expr}, ns).get();
335334
new_lhs =
336-
state.assignment(std::move(new_lhs), new_rhs, ns, true, false).get();
335+
state.assignment(std::move(new_lhs), new_guard, ns, true, false).get();
337336

338337
guardt guard{true_exprt{}, guard_manager};
339338

@@ -347,12 +346,14 @@ void goto_symext::symex_goto(statet &state)
347346

348347
target.assignment(
349348
guard.as_expr(),
350-
new_lhs, new_lhs, guard_symbol_expr,
351-
new_rhs,
349+
new_lhs,
350+
new_lhs,
351+
guard_symbol_expr,
352+
new_guard,
352353
original_source,
353354
symex_targett::assignment_typet::GUARD);
354355

355-
guard_expr = state.rename(boolean_negate(guard_symbol_expr), ns).get();
356+
guard_expr = state.rename(guard_symbol_expr, ns).get();
356357
}
357358

358359
if(state.has_saved_jump_target)

0 commit comments

Comments
 (0)