ExplodedGraphWalker { public MethodBehavior visitMethod(MethodTree tree) { return visitMethod(tree, null); } @VisibleForTesting  ExplodedGraphWalker(BehaviorCache behaviorCache, Sema semanticModel); @VisibleForTesting  ExplodedGraphWalker(BehaviorCache behaviorCache, Sema semanticModel, boolean cleanup); @VisibleForTesting protected  ExplodedGraphWalker(List<SECheck> seChecks, BehaviorCache behaviorCache, Sema semanticModel); MethodBehavior visitMethod(MethodTree tree); MethodBehavior visitMethod(MethodTree tree, @Nullable MethodBehavior methodBehavior); void addExceptionalYield(SymbolicValue target, ProgramState exceptionalState, String exceptionFullyQualifiedName, SECheck check); void clearStack(Tree tree); void enqueue(ProgramPoint programPoint, ProgramState programState); void enqueue(ProgramPoint programPoint, ProgramState programState, @Nullable MethodYield methodYield); void enqueue(ProgramPoint newProgramPoint, ProgramState programState, boolean exitPath); void enqueue(ProgramPoint newProgramPoint, ProgramState programState, boolean exitPath, @Nullable MethodYield methodYield); static final int MAX_NESTED_BOOLEAN_STATES; static final MethodMatchers EQUALS_METHODS; }
@Test void test_cleanup_state() { final int[] steps = new int[2]; CheckVerifier.newVerifier() .onFile("src/test/files/se/SeEngineTestCleanupState.java") .withCheck(new SymbolicExecutionVisitor(Collections.emptyList(), new BehaviorCache()) { @Override public void visitNode(Tree tree) { ExplodedGraphWalker explodedGraphWalker = new ExplodedGraphWalker(this.behaviorCache, (Sema) context.getSemanticModel(), false); explodedGraphWalker.visitMethod((MethodTree) tree, methodBehaviorForSymbol(((MethodTree) tree).symbol())); steps[0] += explodedGraphWalker.steps; } }) .withClassPath(SETestUtils.CLASS_PATH) .verifyNoIssues(); CheckVerifier.newVerifier() .onFile("src/test/files/se/SeEngineTestCleanupState.java") .withCheck(new SymbolicExecutionVisitor(Collections.emptyList(), new BehaviorCache()) { @Override public void visitNode(Tree tree) { ExplodedGraphWalker explodedGraphWalker = new ExplodedGraphWalker(this.behaviorCache, (Sema) context.getSemanticModel()); MethodTree methodTree = (MethodTree) tree; explodedGraphWalker.visitMethod(methodTree, methodBehaviorForSymbol(methodTree.symbol())); steps[1] += explodedGraphWalker.steps; } }) .withClassPath(SETestUtils.CLASS_PATH) .verifyNoIssues(); assertThat(steps[0]) .isPositive() .isGreaterThan(steps[1]); }
@Test void test_limited_loop_execution() throws Exception { CheckVerifier.newVerifier() .onFile("src/test/files/se/SeEngineTestCase.java") .withCheck(new SymbolicExecutionVisitor(Collections.emptyList(), new BehaviorCache()) { @Override public void visitNode(Tree tree) { try { MethodTree methodTree = (MethodTree) tree; new ExplodedGraphWalker(this.behaviorCache, (Sema) context.getSemanticModel()).visitMethod(methodTree, methodBehaviorForSymbol(methodTree.symbol())); } catch (ExplodedGraphWalker.MaximumStepsReachedException exception) { fail("loop execution should be limited"); } } }) .withClassPath(SETestUtils.CLASS_PATH) .verifyNoIssues(); }
@Test void test_max_number_starting_states() throws Exception { CheckVerifier.newVerifier() .onFile("src/test/files/se/MaxStartingStates.java") .withCheck(new SymbolicExecutionVisitor(Collections.emptyList(), new BehaviorCache()) { @Override public void visitNode(Tree tree) { MethodTree methodTree = (MethodTree) tree; ExplodedGraphWalker explodedGraphWalker = new ExplodedGraphWalker(this.behaviorCache, (Sema) context.getSemanticModel()); MethodBehavior methodBehavior = methodBehaviorForSymbol(methodTree.symbol()); try { explodedGraphWalker.visitMethod(methodTree, methodBehavior); fail("Too many starting states were generated!!"); } catch (ExplodedGraphWalker.MaximumStartingStatesException exception) { assertThat(exception.getMessage()).startsWith("reached maximum number of 1024 starting states for method"); } } }) .withClassPath(SETestUtils.CLASS_PATH) .verifyNoIssues(); }
@Test void test_max_number_starting_states_boundaries() throws Exception { CheckVerifier.newVerifier() .onFile("src/test/files/se/StartingStates1024.java") .withCheck(new SymbolicExecutionVisitor(Collections.emptyList(), new BehaviorCache()) { @Override public void visitNode(Tree tree) { MethodTree methodTree = (MethodTree) tree; ExplodedGraphWalker explodedGraphWalker = new ExplodedGraphWalker(this.behaviorCache, (Sema) context.getSemanticModel()); MethodBehavior methodBehavior = methodBehaviorForSymbol(methodTree.symbol()); try { explodedGraphWalker.visitMethod(methodTree, methodBehavior); } catch (ExplodedGraphWalker.MaximumStartingStatesException exception) { fail("Should have been able to generate 1024 states!"); } } }) .withClassPath(SETestUtils.CLASS_PATH) .verifyNoIssues(); }
@Test void test_maximum_steps_reached() throws Exception { CheckVerifier.newVerifier() .onFile("src/test/files/se/MaxSteps.java") .withCheck(new SymbolicExecutionVisitor(Collections.emptyList(), new BehaviorCache()) { @Override public void visitNode(Tree tree) { MethodTree methodTree = (MethodTree) tree; ExplodedGraphWalker explodedGraphWalker = new ExplodedGraphWalker(this.behaviorCache, (Sema) context.getSemanticModel()); MethodBehavior methodBehavior = methodBehaviorForSymbol(methodTree.symbol()); try { explodedGraphWalker.visitMethod(methodTree, methodBehavior); fail("Too many states were processed !"); } catch (ExplodedGraphWalker.MaximumStepsReachedException exception) { assertThat(exception.getMessage()).startsWith("reached limit of 16000 steps for method"); } } }) .withClassPath(SETestUtils.CLASS_PATH) .verifyNoIssues(); }
@Test void test_maximum_number_nested_states() throws Exception { CheckVerifier.newVerifier() .onFile("src/test/files/se/MaxNestedStates.java") .withCheck(new SymbolicExecutionVisitor(Collections.emptyList(), new BehaviorCache()) { @Override public void visitNode(Tree tree) { MethodTree methodTree = (MethodTree) tree; ExplodedGraphWalker explodedGraphWalker = new ExplodedGraphWalker(this.behaviorCache, (Sema) context.getSemanticModel()); MethodBehavior methodBehavior = methodBehaviorForSymbol(methodTree.symbol()); try { explodedGraphWalker.visitMethod(methodTree, methodBehavior); fail("Too many states were processed !"); } catch (ExplodedGraphWalker.MaximumStepsReachedException exception) { assertThat(exception.getMessage()).startsWith("reached maximum number of 10000 branched states"); } } }) .withClassPath(SETestUtils.CLASS_PATH) .verifyNoIssues(); }
@Test void xproc_keep_yield_for_reporting() throws Exception { CheckVerifier.newVerifier() .onFile("src/test/files/se/YieldReporting.java") .withCheck(new SymbolicExecutionVisitor(Collections.emptyList(), new BehaviorCache()) { @Override public void visitNode(Tree tree) { MethodTree methodTree = (MethodTree) tree; if ("test".equals(methodTree.symbol().name())) { ExplodedGraphWalker egw = new ExplodedGraphWalker(this.behaviorCache, (Sema) context.getSemanticModel()); egw.visitMethod(methodTree, null); assertThat(egw.checkerDispatcher.methodYield).isNull(); } } }) .withClassPath(SETestUtils.CLASS_PATH) .verifyNoIssues(); }