Skip to content

Commit

Permalink
SONARJAVA-1465 Handle explosion of nested states
Browse files Browse the repository at this point in the history
  • Loading branch information
@Wohops
Wohops committed Feb 23, 2016
1 parent c2ddc76 commit 4adfce8
Show file tree
Hide file tree
Showing 4 changed files with 99 additions and 32 deletions.
50 changes: 28 additions & 22 deletions java-squid/src/main/java/org/sonar/java/se/ExplodedGraphWalker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@
import com.google.common.collect.ImmutableSet;
import com.google.common.collect.Iterables;
import com.google.common.collect.Lists;

import org.slf4j.Logger;
import org.slf4j.LoggerFactory;
import org.sonar.java.cfg.CFG;
Expand Down Expand Up @@ -81,6 +82,7 @@ public class ExplodedGraphWalker extends BaseTreeVisitor {
* Arbitrary number to limit symbolic execution.
*/
private static final int MAX_STEPS = 10000;
public static final int MAX_NESTED_BOOLEAN_STATES = 10000;
private static final Logger LOG = LoggerFactory.getLogger(ExplodedGraphWalker.class);
private static final Set<String> THIS_SUPER = ImmutableSet.of("this", "super");

Expand Down Expand Up @@ -112,6 +114,13 @@ public static class MaximumStepsReachedException extends RuntimeException {
public MaximumStepsReachedException(String s) {
super(s);
}

public MaximumStepsReachedException(String s, TooManyNestedBooleanStatesException e) {
super(s, e);
}
}

public static class TooManyNestedBooleanStatesException extends RuntimeException {
}

public ExplodedGraphWalker(JavaFileScannerContext context) {
Expand Down Expand Up @@ -163,20 +172,25 @@ private void execute(MethodTree tree) {
LOG.debug("End of potential path reached!");
continue;
}
if (programPosition.i < programPosition.block.elements().size()) {
// process block element
visit(programPosition.block.elements().get(programPosition.i), programPosition.block.terminator());
} else if (programPosition.block.terminator() == null) {
// process block exit, which is unconditional jump such as goto-statement or return-statement
handleBlockExit(programPosition);
} else if (programPosition.i == programPosition.block.elements().size()) {
// process block exist, which is conditional jump such as if-statement
checkerDispatcher.executeCheckPostStatement(programPosition.block.terminator());
} else {
// process branch
// process block exist, which is conditional jump such as if-statement
checkerDispatcher.executeCheckPreStatement(programPosition.block.terminator());
handleBlockExit(programPosition);
try {
if (programPosition.i < programPosition.block.elements().size()) {
// process block element
visit(programPosition.block.elements().get(programPosition.i), programPosition.block.terminator());
} else if (programPosition.block.terminator() == null) {
// process block exit, which is unconditional jump such as goto-statement or return-statement
handleBlockExit(programPosition);
} else if (programPosition.i == programPosition.block.elements().size()) {
// process block exist, which is conditional jump such as if-statement
checkerDispatcher.executeCheckPostStatement(programPosition.block.terminator());
} else {
// process branch
// process block exist, which is conditional jump such as if-statement
checkerDispatcher.executeCheckPreStatement(programPosition.block.terminator());
handleBlockExit(programPosition);
}
} catch (ExplodedGraphWalker.TooManyNestedBooleanStatesException e) {
throw new MaximumStepsReachedException(
"reached maximum number of " + MAX_NESTED_BOOLEAN_STATES + " branched states for method " + tree.simpleName().name() + " in class " + tree.symbol().owner().name(), e);
}
}

Expand Down Expand Up @@ -609,7 +623,6 @@ public void enqueue(ExplodedGraph.ProgramPoint programPoint, ProgramState progra
}

public void enqueue(ExplodedGraph.ProgramPoint programPoint, ProgramState programState, boolean exitPath) {
checkMaxStepsWhileEnqueuing();
int nbOfExecution = programState.numberOfTimeVisited(programPoint);
if (nbOfExecution > MAX_EXEC_PROGRAM_POINT) {
debugPrint(programState);
Expand All @@ -625,13 +638,6 @@ public void enqueue(ExplodedGraph.ProgramPoint programPoint, ProgramState progra
workList.addFirst(cachedNode);
}

private void checkMaxStepsWhileEnqueuing() {
if (steps + workList.size() + 1 > MAX_STEPS) {
throw new MaximumStepsReachedException("reached limit of " + MAX_STEPS +
" steps for method " + methodTree.simpleName().name() + " in class " + methodTree.symbol().owner().name() +" while enqueuing program states.");
}
}

private void checkExplodedGraphTooBig(ProgramState programState) {
// Arbitrary formula to avoid out of memory errors
if (steps + workList.size() > MAX_STEPS / 2 && programState.constraintsSize() > 75) {
Expand Down
27 changes: 18 additions & 9 deletions java-squid/src/main/java/org/sonar/java/se/symbolicvalues/SymbolicValue.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,10 +21,12 @@

import com.google.common.base.Preconditions;
import com.google.common.collect.ImmutableList;

import org.sonar.java.se.ExplodedGraphWalker;
import org.sonar.java.se.ProgramState;
import org.sonar.java.se.constraint.BooleanConstraint;
import org.sonar.java.se.constraint.Constraint;
import org.sonar.java.se.constraint.ObjectConstraint;
import org.sonar.java.se.ProgramState;
import org.sonar.java.se.constraint.TypedConstraint;

import javax.annotation.CheckForNull;
Expand Down Expand Up @@ -226,6 +228,13 @@ protected BooleanExpressionSymbolicValue(int id) {
public BooleanConstraint shouldNotInverse() {
return BooleanConstraint.TRUE;
}

protected static void addStates(List<ProgramState> states, List<ProgramState> newStates) {
if (states.size() > ExplodedGraphWalker.MAX_NESTED_BOOLEAN_STATES || newStates.size() > ExplodedGraphWalker.MAX_NESTED_BOOLEAN_STATES) {
throw new ExplodedGraphWalker.TooManyNestedBooleanStatesException();
}
states.addAll(newStates);
}
}

public static class AndSymbolicValue extends BooleanExpressionSymbolicValue {
Expand All @@ -240,13 +249,13 @@ public List<ProgramState> setConstraint(ProgramState programState, BooleanConstr
if (booleanConstraint.isFalse()) {
List<ProgramState> falseFirstOp = leftOp.setConstraint(programState, BooleanConstraint.FALSE);
for (ProgramState ps : falseFirstOp) {
states.addAll(rightOp.setConstraint(ps, BooleanConstraint.TRUE));
states.addAll(rightOp.setConstraint(ps, BooleanConstraint.FALSE));
addStates(states, rightOp.setConstraint(ps, BooleanConstraint.TRUE));
addStates(states, rightOp.setConstraint(ps, BooleanConstraint.FALSE));
}
}
List<ProgramState> trueFirstOp = leftOp.setConstraint(programState, BooleanConstraint.TRUE);
for (ProgramState ps : trueFirstOp) {
states.addAll(rightOp.setConstraint(ps, booleanConstraint));
addStates(states, rightOp.setConstraint(ps, booleanConstraint));
}
return states;
}
Expand All @@ -269,13 +278,13 @@ public List<ProgramState> setConstraint(ProgramState programState, BooleanConstr
if (booleanConstraint.isTrue()) {
List<ProgramState> trueFirstOp = leftOp.setConstraint(programState, BooleanConstraint.TRUE);
for (ProgramState ps : trueFirstOp) {
states.addAll(rightOp.setConstraint(ps, BooleanConstraint.TRUE));
states.addAll(rightOp.setConstraint(ps, BooleanConstraint.FALSE));
addStates(states, rightOp.setConstraint(ps, BooleanConstraint.TRUE));
addStates(states, rightOp.setConstraint(ps, BooleanConstraint.FALSE));
}
}
List<ProgramState> falseFirstOp = leftOp.setConstraint(programState, BooleanConstraint.FALSE);
for (ProgramState ps : falseFirstOp) {
states.addAll(rightOp.setConstraint(ps, booleanConstraint));
addStates(states, rightOp.setConstraint(ps, booleanConstraint));
}
return states;
}
Expand All @@ -297,11 +306,11 @@ public List<ProgramState> setConstraint(ProgramState programState, BooleanConstr
List<ProgramState> states = new ArrayList<>();
List<ProgramState> trueFirstOp = leftOp.setConstraint(programState, BooleanConstraint.TRUE);
for (ProgramState ps : trueFirstOp) {
states.addAll(rightOp.setConstraint(ps, booleanConstraint.inverse()));
addStates(states, rightOp.setConstraint(ps, booleanConstraint.inverse()));
}
List<ProgramState> falseFirstOp = leftOp.setConstraint(programState, BooleanConstraint.FALSE);
for (ProgramState ps : falseFirstOp) {
states.addAll(rightOp.setConstraint(ps, booleanConstraint));
addStates(states, rightOp.setConstraint(ps, booleanConstraint));
}
return states;
}
Expand Down
36 changes: 36 additions & 0 deletions java-squid/src/test/files/se/MaxNestedStates.java
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
class A {
void plop() {
boolean a = true;
a &= (b1() == C);
a &= (b2() == C);
a &= (b3() == C);
a &= (b4() == C);
a &= (b5() == C);
a &= (b6() == C);
a &= (b7() == C);
a &= (b8() == C);
a &= (b9() == C);
a &= (b10() == C);
a &= (b11() == C);
a &= (b12() == C);
a &= (b13() == C);
a &= (b14() == C);
a &= (b15() == C);
a &= (b16() == C);
a &= (b17() == C);
a &= (b18() == C);
a &= (b19() == C);
a &= (b20() == C);
a &= (b21() == C);
a &= (b22() == C);
a &= (b23() == C);
a &= (b24() == C);
a &= (b25() == C);
a &= (b26() == C);
a &= (b27() == C);
a &= (b28() == C);

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
}
}
}
18 changes: 17 additions & 1 deletion java-squid/src/test/java/org/sonar/java/se/ExplodedGraphWalkerTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@
package org.sonar.java.se;

import com.google.common.collect.Multimap;

import org.junit.Test;
import org.sonar.java.model.DefaultJavaFileScannerContext;
import org.sonar.java.se.checks.ConditionAlwaysTrueOrFalseCheck;
Expand Down Expand Up @@ -95,7 +96,22 @@ public void visitNode(Tree tree) {
tree.accept(new ExplodedGraphWalker(context));
fail("Too many states were processed !");
} catch (ExplodedGraphWalker.MaximumStepsReachedException exception) {
assertThat(exception.getMessage()).endsWith("while enqueuing program states.");
assertThat(exception.getMessage()).startsWith("reached limit of 10000 steps for method");
}
}
});
}

@Test
public void test_maximum_number_nested_states() throws Exception {
JavaCheckVerifier.verifyNoIssue("src/test/files/se/MaxNestedStates.java", new SymbolicExecutionVisitor() {
@Override
public void visitNode(Tree tree) {
try {
tree.accept(new ExplodedGraphWalker(context));
fail("Too many states were processed !");
} catch (ExplodedGraphWalker.MaximumStepsReachedException exception) {
assertThat(exception.getMessage()).startsWith("reached maximum number of 10000 branched states");
}
}
});
Expand Down

0 comments on commit 4adfce8

Please sign in to comment.