Skip to content

Commit 4adfce8

Browse files
WohopsWohops
committed
SONARJAVA-1465 Handle explosion of nested states
1 parent c2ddc76 commit 4adfce8

4 files changed

Lines changed: 99 additions & 32 deletions

File tree

‎java-squid/src/main/java/org/sonar/java/se/ExplodedGraphWalker.java‎

Lines changed: 28 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@
2626
import com.google.common.collect.ImmutableSet;
2727
import com.google.common.collect.Iterables;
2828
import com.google.common.collect.Lists;
29+
2930
import org.slf4j.Logger;
3031
import org.slf4j.LoggerFactory;
3132
import org.sonar.java.cfg.CFG;
@@ -81,6 +82,7 @@ public class ExplodedGraphWalker extends BaseTreeVisitor {
8182
* Arbitrary number to limit symbolic execution.
8283
*/
8384
private static final int MAX_STEPS = 10000;
85+
public static final int MAX_NESTED_BOOLEAN_STATES = 10000;
8486
private static final Logger LOG = LoggerFactory.getLogger(ExplodedGraphWalker.class);
8587
private static final Set<String> THIS_SUPER = ImmutableSet.of("this", "super");
8688

@@ -112,6 +114,13 @@ public static class MaximumStepsReachedException extends RuntimeException {
112114
public MaximumStepsReachedException(String s) {
113115
super(s);
114116
}
117+
118+
public MaximumStepsReachedException(String s, TooManyNestedBooleanStatesException e) {
119+
super(s, e);
120+
}
121+
}
122+
123+
public static class TooManyNestedBooleanStatesException extends RuntimeException {
115124
}
116125

117126
public ExplodedGraphWalker(JavaFileScannerContext context) {
@@ -163,20 +172,25 @@ private void execute(MethodTree tree) {
163172
LOG.debug("End of potential path reached!");
164173
continue;
165174
}
166-
if (programPosition.i < programPosition.block.elements().size()) {
167-
// process block element
168-
visit(programPosition.block.elements().get(programPosition.i), programPosition.block.terminator());
169-
} else if (programPosition.block.terminator() == null) {
170-
// process block exit, which is unconditional jump such as goto-statement or return-statement
171-
handleBlockExit(programPosition);
172-
} else if (programPosition.i == programPosition.block.elements().size()) {
173-
// process block exist, which is conditional jump such as if-statement
174-
checkerDispatcher.executeCheckPostStatement(programPosition.block.terminator());
175-
} else {
176-
// process branch
177-
// process block exist, which is conditional jump such as if-statement
178-
checkerDispatcher.executeCheckPreStatement(programPosition.block.terminator());
179-
handleBlockExit(programPosition);
175+
try {
176+
if (programPosition.i < programPosition.block.elements().size()) {
177+
// process block element
178+
visit(programPosition.block.elements().get(programPosition.i), programPosition.block.terminator());
179+
} else if (programPosition.block.terminator() == null) {
180+
// process block exit, which is unconditional jump such as goto-statement or return-statement
181+
handleBlockExit(programPosition);
182+
} else if (programPosition.i == programPosition.block.elements().size()) {
183+
// process block exist, which is conditional jump such as if-statement
184+
checkerDispatcher.executeCheckPostStatement(programPosition.block.terminator());
185+
} else {
186+
// process branch
187+
// process block exist, which is conditional jump such as if-statement
188+
checkerDispatcher.executeCheckPreStatement(programPosition.block.terminator());
189+
handleBlockExit(programPosition);
190+
}
191+
} catch (ExplodedGraphWalker.TooManyNestedBooleanStatesException e) {
192+
throw new MaximumStepsReachedException(
193+
"reached maximum number of " + MAX_NESTED_BOOLEAN_STATES + " branched states for method " + tree.simpleName().name() + " in class " + tree.symbol().owner().name(), e);
180194
}
181195
}
182196

@@ -609,7 +623,6 @@ public void enqueue(ExplodedGraph.ProgramPoint programPoint, ProgramState progra
609623
}
610624

611625
public void enqueue(ExplodedGraph.ProgramPoint programPoint, ProgramState programState, boolean exitPath) {
612-
checkMaxStepsWhileEnqueuing();
613626
int nbOfExecution = programState.numberOfTimeVisited(programPoint);
614627
if (nbOfExecution > MAX_EXEC_PROGRAM_POINT) {
615628
debugPrint(programState);
@@ -625,13 +638,6 @@ public void enqueue(ExplodedGraph.ProgramPoint programPoint, ProgramState progra
625638
workList.addFirst(cachedNode);
626639
}
627640

628-
private void checkMaxStepsWhileEnqueuing() {
629-
if (steps + workList.size() + 1 > MAX_STEPS) {
630-
throw new MaximumStepsReachedException("reached limit of " + MAX_STEPS +
631-
" steps for method " + methodTree.simpleName().name() + " in class " + methodTree.symbol().owner().name() +" while enqueuing program states.");
632-
}
633-
}
634-
635641
private void checkExplodedGraphTooBig(ProgramState programState) {
636642
// Arbitrary formula to avoid out of memory errors
637643
if (steps + workList.size() > MAX_STEPS / 2 && programState.constraintsSize() > 75) {

‎java-squid/src/main/java/org/sonar/java/se/symbolicvalues/SymbolicValue.java‎

Lines changed: 18 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -21,10 +21,12 @@
2121

2222
import com.google.common.base.Preconditions;
2323
import com.google.common.collect.ImmutableList;
24+
25+
import org.sonar.java.se.ExplodedGraphWalker;
26+
import org.sonar.java.se.ProgramState;
2427
import org.sonar.java.se.constraint.BooleanConstraint;
2528
import org.sonar.java.se.constraint.Constraint;
2629
import org.sonar.java.se.constraint.ObjectConstraint;
27-
import org.sonar.java.se.ProgramState;
2830
import org.sonar.java.se.constraint.TypedConstraint;
2931

3032
import javax.annotation.CheckForNull;
@@ -226,6 +228,13 @@ protected BooleanExpressionSymbolicValue(int id) {
226228
public BooleanConstraint shouldNotInverse() {
227229
return BooleanConstraint.TRUE;
228230
}
231+
232+
protected static void addStates(List<ProgramState> states, List<ProgramState> newStates) {
233+
if (states.size() > ExplodedGraphWalker.MAX_NESTED_BOOLEAN_STATES || newStates.size() > ExplodedGraphWalker.MAX_NESTED_BOOLEAN_STATES) {
234+
throw new ExplodedGraphWalker.TooManyNestedBooleanStatesException();
235+
}
236+
states.addAll(newStates);
237+
}
229238
}
230239

231240
public static class AndSymbolicValue extends BooleanExpressionSymbolicValue {
@@ -240,13 +249,13 @@ public List<ProgramState> setConstraint(ProgramState programState, BooleanConstr
240249
if (booleanConstraint.isFalse()) {
241250
List<ProgramState> falseFirstOp = leftOp.setConstraint(programState, BooleanConstraint.FALSE);
242251
for (ProgramState ps : falseFirstOp) {
243-
states.addAll(rightOp.setConstraint(ps, BooleanConstraint.TRUE));
244-
states.addAll(rightOp.setConstraint(ps, BooleanConstraint.FALSE));
252+
addStates(states, rightOp.setConstraint(ps, BooleanConstraint.TRUE));
253+
addStates(states, rightOp.setConstraint(ps, BooleanConstraint.FALSE));
245254
}
246255
}
247256
List<ProgramState> trueFirstOp = leftOp.setConstraint(programState, BooleanConstraint.TRUE);
248257
for (ProgramState ps : trueFirstOp) {
249-
states.addAll(rightOp.setConstraint(ps, booleanConstraint));
258+
addStates(states, rightOp.setConstraint(ps, booleanConstraint));
250259
}
251260
return states;
252261
}
@@ -269,13 +278,13 @@ public List<ProgramState> setConstraint(ProgramState programState, BooleanConstr
269278
if (booleanConstraint.isTrue()) {
270279
List<ProgramState> trueFirstOp = leftOp.setConstraint(programState, BooleanConstraint.TRUE);
271280
for (ProgramState ps : trueFirstOp) {
272-
states.addAll(rightOp.setConstraint(ps, BooleanConstraint.TRUE));
273-
states.addAll(rightOp.setConstraint(ps, BooleanConstraint.FALSE));
281+
addStates(states, rightOp.setConstraint(ps, BooleanConstraint.TRUE));
282+
addStates(states, rightOp.setConstraint(ps, BooleanConstraint.FALSE));
274283
}
275284
}
276285
List<ProgramState> falseFirstOp = leftOp.setConstraint(programState, BooleanConstraint.FALSE);
277286
for (ProgramState ps : falseFirstOp) {
278-
states.addAll(rightOp.setConstraint(ps, booleanConstraint));
287+
addStates(states, rightOp.setConstraint(ps, booleanConstraint));
279288
}
280289
return states;
281290
}
@@ -297,11 +306,11 @@ public List<ProgramState> setConstraint(ProgramState programState, BooleanConstr
297306
List<ProgramState> states = new ArrayList<>();
298307
List<ProgramState> trueFirstOp = leftOp.setConstraint(programState, BooleanConstraint.TRUE);
299308
for (ProgramState ps : trueFirstOp) {
300-
states.addAll(rightOp.setConstraint(ps, booleanConstraint.inverse()));
309+
addStates(states, rightOp.setConstraint(ps, booleanConstraint.inverse()));
301310
}
302311
List<ProgramState> falseFirstOp = leftOp.setConstraint(programState, BooleanConstraint.FALSE);
303312
for (ProgramState ps : falseFirstOp) {
304-
states.addAll(rightOp.setConstraint(ps, booleanConstraint));
313+
addStates(states, rightOp.setConstraint(ps, booleanConstraint));
305314
}
306315
return states;
307316
}

‎java-squid/src/test/files/se/MaxNestedStates.java‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
class A {
2+
void plop() {
3+
boolean a = true;
4+
a &= (b1() == C);
5+
a &= (b2() == C);
6+
a &= (b3() == C);
7+
a &= (b4() == C);
8+
a &= (b5() == C);
9+
a &= (b6() == C);
10+
a &= (b7() == C);
11+
a &= (b8() == C);
12+
a &= (b9() == C);
13+
a &= (b10() == C);
14+
a &= (b11() == C);
15+
a &= (b12() == C);
16+
a &= (b13() == C);
17+
a &= (b14() == C);
18+
a &= (b15() == C);
19+
a &= (b16() == C);
20+
a &= (b17() == C);
21+
a &= (b18() == C);
22+
a &= (b19() == C);
23+
a &= (b20() == C);
24+
a &= (b21() == C);
25+
a &= (b22() == C);
26+
a &= (b23() == C);
27+
a &= (b24() == C);
28+
a &= (b25() == C);
29+
a &= (b26() == C);
30+
a &= (b27() == C);
31+
a &= (b28() == C);
32+
33+
if (a) { //BOOM : 2^n -1 states are generated (where n is the number of lines of &= assignements in the above code) -> fail fast by not even enqueuing nodes
34+
}
35+
}
36+
}

‎java-squid/src/test/java/org/sonar/java/se/ExplodedGraphWalkerTest.java‎

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@
2020
package org.sonar.java.se;
2121

2222
import com.google.common.collect.Multimap;
23+
2324
import org.junit.Test;
2425
import org.sonar.java.model.DefaultJavaFileScannerContext;
2526
import org.sonar.java.se.checks.ConditionAlwaysTrueOrFalseCheck;
@@ -95,7 +96,22 @@ public void visitNode(Tree tree) {
9596
tree.accept(new ExplodedGraphWalker(context));
9697
fail("Too many states were processed !");
9798
} catch (ExplodedGraphWalker.MaximumStepsReachedException exception) {
98-
assertThat(exception.getMessage()).endsWith("while enqueuing program states.");
99+
assertThat(exception.getMessage()).startsWith("reached limit of 10000 steps for method");
100+
}
101+
}
102+
});
103+
}
104+
105+
@Test
106+
public void test_maximum_number_nested_states() throws Exception {
107+
JavaCheckVerifier.verifyNoIssue("src/test/files/se/MaxNestedStates.java", new SymbolicExecutionVisitor() {
108+
@Override
109+
public void visitNode(Tree tree) {
110+
try {
111+
tree.accept(new ExplodedGraphWalker(context));
112+
fail("Too many states were processed !");
113+
} catch (ExplodedGraphWalker.MaximumStepsReachedException exception) {
114+
assertThat(exception.getMessage()).startsWith("reached maximum number of 10000 branched states");
99115
}
100116
}
101117
});

0 commit comments

Comments
 (0)