Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit bc3bad6

Browse files
tautschnigtautschnig
committedNov 17, 2023
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 74075ec commit bc3bad6

File tree

7 files changed

+31
-32
lines changed

7 files changed

+31
-32
lines changed
 

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
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`
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`
44
^\[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$
@@ -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-cover/pointer-function-parameters/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ main.c
55
^Test suite:$
66
^(tmp(\$\d+)?=[^,]*, a=\(\(signed int \*\)NULL\))|(a=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*)$
77
^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=4)|(tmp(\$\d+)?=4, a=&tmp(\$\d+)?!0@1)$
8-
^(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)$
8+
^(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)$
99
^EXIT=0$
1010
^SIGNAL=0$
1111
--

‎regression/cbmc/fault_localization-all_properties2/test.desc

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE paths-lifo-expected-failure broken-smt-backend no-new-smt
22
main.c
33
--localize-faults
44
^EXIT=10$
@@ -7,5 +7,3 @@ line 9 function main$
77
^VERIFICATION FAILED$
88
--
99
--
10-
CBMC wrongly reports line 7 as the faulty statement when instead it should be
11-
line 9.

‎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
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
@@ -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)
Please sign in to comment.