From 4adfce80a60a1feb2f5f729aae9edb34a103bb13 Mon Sep 17 00:00:00 2001 From: Michael Gumowski Date: Tue, 23 Feb 2016 10:35:03 +0100 Subject: [PATCH] SONARJAVA-1465 Handle explosion of nested states --- .../sonar/java/se/ExplodedGraphWalker.java | 50 +++++++++++-------- .../java/se/symbolicvalues/SymbolicValue.java | 27 ++++++---- .../src/test/files/se/MaxNestedStates.java | 36 +++++++++++++ .../java/se/ExplodedGraphWalkerTest.java | 18 ++++++- 4 files changed, 99 insertions(+), 32 deletions(-) create mode 100644 java-squid/src/test/files/se/MaxNestedStates.java diff --git a/java-squid/src/main/java/org/sonar/java/se/ExplodedGraphWalker.java b/java-squid/src/main/java/org/sonar/java/se/ExplodedGraphWalker.java index 15664fca637..9113cab55f6 100644 --- a/java-squid/src/main/java/org/sonar/java/se/ExplodedGraphWalker.java +++ b/java-squid/src/main/java/org/sonar/java/se/ExplodedGraphWalker.java @@ -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; @@ -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 THIS_SUPER = ImmutableSet.of("this", "super"); @@ -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) { @@ -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); } } @@ -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); @@ -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) { diff --git a/java-squid/src/main/java/org/sonar/java/se/symbolicvalues/SymbolicValue.java b/java-squid/src/main/java/org/sonar/java/se/symbolicvalues/SymbolicValue.java index 20f939b796d..efda5a3bc56 100644 --- a/java-squid/src/main/java/org/sonar/java/se/symbolicvalues/SymbolicValue.java +++ b/java-squid/src/main/java/org/sonar/java/se/symbolicvalues/SymbolicValue.java @@ -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; @@ -226,6 +228,13 @@ protected BooleanExpressionSymbolicValue(int id) { public BooleanConstraint shouldNotInverse() { return BooleanConstraint.TRUE; } + + protected static void addStates(List states, List 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 { @@ -240,13 +249,13 @@ public List setConstraint(ProgramState programState, BooleanConstr if (booleanConstraint.isFalse()) { List 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 trueFirstOp = leftOp.setConstraint(programState, BooleanConstraint.TRUE); for (ProgramState ps : trueFirstOp) { - states.addAll(rightOp.setConstraint(ps, booleanConstraint)); + addStates(states, rightOp.setConstraint(ps, booleanConstraint)); } return states; } @@ -269,13 +278,13 @@ public List setConstraint(ProgramState programState, BooleanConstr if (booleanConstraint.isTrue()) { List 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 falseFirstOp = leftOp.setConstraint(programState, BooleanConstraint.FALSE); for (ProgramState ps : falseFirstOp) { - states.addAll(rightOp.setConstraint(ps, booleanConstraint)); + addStates(states, rightOp.setConstraint(ps, booleanConstraint)); } return states; } @@ -297,11 +306,11 @@ public List setConstraint(ProgramState programState, BooleanConstr List states = new ArrayList<>(); List 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 falseFirstOp = leftOp.setConstraint(programState, BooleanConstraint.FALSE); for (ProgramState ps : falseFirstOp) { - states.addAll(rightOp.setConstraint(ps, booleanConstraint)); + addStates(states, rightOp.setConstraint(ps, booleanConstraint)); } return states; } diff --git a/java-squid/src/test/files/se/MaxNestedStates.java b/java-squid/src/test/files/se/MaxNestedStates.java new file mode 100644 index 00000000000..d3e251c9232 --- /dev/null +++ b/java-squid/src/test/files/se/MaxNestedStates.java @@ -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 + } + } +} diff --git a/java-squid/src/test/java/org/sonar/java/se/ExplodedGraphWalkerTest.java b/java-squid/src/test/java/org/sonar/java/se/ExplodedGraphWalkerTest.java index 1764ee8a0db..1933f760128 100644 --- a/java-squid/src/test/java/org/sonar/java/se/ExplodedGraphWalkerTest.java +++ b/java-squid/src/test/java/org/sonar/java/se/ExplodedGraphWalkerTest.java @@ -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; @@ -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"); } } });