204 on dfs scan violation discovery return better options

README.md

@@ -53,6 +53,7 @@ If you use BPjs in an academic work, please consider citing it as:
 ## Change Log for the BPjs Library.
 
 ### 2023-09
+* :arrow_up: `DfsBProgramVerifier.ProgressListener::violationFound` now returns a `ViolenceResponse` object, instead of a `bool`, and now supporting the option of pruning the trace tree when violation happened ([#204](https://github.com/bThink-BGU/BPjs/issues/204)).
 * :sparkles: EventSets now have an `except` method, that allows removal of events from the set. e.g. `allMotionEvents.except(moveDownEvent)`. ([#218](https://github.com/bThink-BGU/BPjs/issues/218))
 * :arrow_up: Improved error messages when composing event sets.
 

src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java

@@ -100,17 +100,29 @@ public static interface ProgressListener {
          * 
          * @param aViolation the violation found
          * @param vfr the verifier that found the violation
-         * @return {@code true} for the verifier to continue the search, {@code false} otherwise.
+         * @return {@code CONTINUE} for the verifier to continue the search, {@code HALT} for the verifier to halt the search and {@code PRUNE} for pruning the node ans continue the search from other node.
          */
-        boolean violationFound( Violation aViolation, DfsBProgramVerifier vfr );
+        ViolenceResponse violationFound( Violation aViolation, DfsBProgramVerifier vfr );
 
         /**
          * The verifier {@code vfr} has finished the verification process.
          * @param vfr the verifier that found the violation
          */
         void done(DfsBProgramVerifier vfr);
     }
-
+
+
+    /**
+     *Effect of the return values:
+     * CONTINUE - mark current node as having a violation, go deeper into the graph.
+     * PRUNE - mark current node as having a violation, pop it (as in - go back and don't DFS into its descendants)
+     * HALT - mark current node as having a violation and stop the verification.
+     */
+    public enum ViolenceResponse {
+        CONTINUE,
+        PRUNE,
+        HALT
+    }
     private static class ViolatingPathFoundException extends Exception {
         final Violation v;
 
@@ -130,8 +142,8 @@ public ViolatingPathFoundException(Violation v) {
         @Override public void done(DfsBProgramVerifier vfr) {}
 
         @Override
-        public boolean violationFound(Violation aViolation, DfsBProgramVerifier vfr) {
-            return false;
+        public ViolenceResponse violationFound(Violation aViolation, DfsBProgramVerifier vfr) {
+            return ViolenceResponse.HALT;
         }
     };
 
@@ -262,9 +274,15 @@ protected DfsTraversalNode getUnvisitedNextNode(DfsTraversalNode src, ExecutorSe
                         .filter(o->o.isPresent()).map(Optional::get).collect(toSet());
 
                     for ( Violation v : res ) {
-                        if ( ! listener.violationFound(v, this)) {
+                        ViolenceResponse tmp =listener.violationFound(v, this);
+                        if ( tmp == ViolenceResponse.HALT ) {
                             throw new ViolatingPathFoundException(v);
                         }
+                        else if ( tmp == ViolenceResponse.PRUNE ) {
+                            trace.pop();
+                            return null;
+                        }
+
                     }
 
                 } else if ( visited.isVisited(pns) ) {
@@ -275,13 +293,19 @@ protected DfsTraversalNode getUnvisitedNextNode(DfsTraversalNode src, ExecutorSe
                             .filter(o->o.isPresent()).map(Optional::get).collect(toSet());
                     if ( res.size() > 0  ) {
                         for ( Violation v : res ) {
-                            if ( ! listener.violationFound(v, this) ) {
+                            ViolenceResponse tmp =listener.violationFound(v, this);
+                            if ( tmp == ViolenceResponse.HALT ) {
                                 throw new ViolatingPathFoundException(v);
                             }
+                            else if ( tmp == ViolenceResponse.PRUNE ) {
+                                trace.pop();
+                                return null;
+                            }
+
                         }
                     }
                     trace.pop();
-                    
+
                 } else {
                     // advance to this newly discovered node
                     return possibleNextNode;
@@ -290,10 +314,14 @@ protected DfsTraversalNode getUnvisitedNextNode(DfsTraversalNode src, ExecutorSe
             } catch ( BPjsRuntimeException bprte ) {
                 trace.advance(nextEvent, null);
                 Violation jsev = new JsErrorViolation(trace, bprte);
-                if ( ! listener.violationFound(jsev, this) ) {
+                ViolenceResponse tmp =listener.violationFound(jsev, this);
+                if ( tmp == ViolenceResponse.HALT ) {
                     throw new ViolatingPathFoundException(jsev);
                 }
                 trace.pop();
+                if ( tmp == ViolenceResponse.PRUNE ) {
+                    return null;
+                }
             }
         }
         return null;
@@ -344,14 +372,19 @@ private Violation inspectCurrentTrace() {
                                     .collect(toSet());
         if ( res.size() > 0  ) {
             for ( Violation v : res ) {
-                if ( ! listener.violationFound(v, this) ) {
+                ViolenceResponse tmp =listener.violationFound(v, this);
+                if ( tmp == ViolenceResponse.HALT) {
                     return v;
                 }
+                else if ( tmp == ViolenceResponse.PRUNE ) {
+                    if (isDebugMode()) {
+                        System.out.println("(violation) Prune:" +v.decsribe());
+                    }
+                    pop();
+                    return null;
+                }
             }
-            if (isDebugMode()) {
-                System.out.println("-pop! (violation)-");
-            }
-            pop();
+
         }
         return null;
     }

src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/listeners/PrintDfsVerifierListener.java

@@ -66,9 +66,9 @@ public void done(DfsBProgramVerifier v) {
     }
 
     @Override
-    public boolean violationFound(Violation aViolation, DfsBProgramVerifier vfr) {
+    public DfsBProgramVerifier.ViolenceResponse violationFound(Violation aViolation, DfsBProgramVerifier vfr) {
         out.println("/v/ Violation found: " + aViolation.decsribe() );
-        return false;
+        return DfsBProgramVerifier.ViolenceResponse.HALT;
     }
 
 }

src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifierTest.java

@@ -26,9 +26,8 @@
 import il.ac.bgu.cs.bp.bpjs.TestUtils;
 import static il.ac.bgu.cs.bp.bpjs.TestUtils.eventNamesString;
 
-import il.ac.bgu.cs.bp.bpjs.model.BProgram;
+import il.ac.bgu.cs.bp.bpjs.model.*;
 import il.ac.bgu.cs.bp.bpjs.execution.BProgramRunner;
-import il.ac.bgu.cs.bp.bpjs.model.ResourceBProgram;
 import il.ac.bgu.cs.bp.bpjs.execution.listeners.InMemoryEventLoggingListener;
 import il.ac.bgu.cs.bp.bpjs.execution.listeners.PrintBProgramRunnerListener;
 
@@ -37,13 +36,12 @@
 import static il.ac.bgu.cs.bp.bpjs.TestUtils.traceEventNamesString;
 import static org.junit.Assert.*;
 
-import il.ac.bgu.cs.bp.bpjs.model.StringBProgram;
 import il.ac.bgu.cs.bp.bpjs.analysis.listeners.PrintDfsVerifierListener;
 import il.ac.bgu.cs.bp.bpjs.analysis.violations.DeadlockViolation;
 import il.ac.bgu.cs.bp.bpjs.analysis.violations.DetectedSafetyViolation;
 import il.ac.bgu.cs.bp.bpjs.analysis.violations.JsErrorViolation;
 import il.ac.bgu.cs.bp.bpjs.analysis.violations.Violation;
-import il.ac.bgu.cs.bp.bpjs.model.BEvent;
+
 import java.util.Arrays;
 import java.util.HashSet;
 import java.util.Optional;
@@ -491,12 +489,12 @@ public void testJavaScriptError() throws Exception {
             @Override public void done(DfsBProgramVerifier vfr) {}
 
             @Override
-            public boolean violationFound(Violation aViolation, DfsBProgramVerifier vfr) {
+            public DfsBProgramVerifier.ViolenceResponse violationFound(Violation aViolation, DfsBProgramVerifier vfr) {
                 errorCalled.set(aViolation instanceof JsErrorViolation );
                 JsErrorViolation jsev = (JsErrorViolation) aViolation;
                 errorMadeSense.set(jsev.decsribe().contains("isNullAndSoThisInvocationShouldCrash"));
                 System.out.println(jsev.getThrownException().getMessage());
-                return true;
+                return DfsBProgramVerifier.ViolenceResponse.CONTINUE;
             }
         });
 
@@ -556,4 +554,40 @@ public void testThreadStorageEquality() throws Exception {
         assertEquals( 9, res.getScannedStatesCount() );
         assertEquals( 9, stateStore.getVisitedStateCount() );
     }
+
+    @Test
+    public void testPruneABAA() throws Exception {
+        BProgram program = new ResourceBProgram("DFSVerifierTests/AAAA_withBnoice.js");
+        DfsBProgramVerifier sut = new DfsBProgramVerifier();
+        sut.setDebugMode(true);
+        VisitedStateStore stateStore = new BThreadSnapshotVisitedStateStore();
+        sut.setVisitedStateStore(stateStore);
+        //add violation  on event "B"
+
+        sut.setProgressListener(new PrintDfsVerifierListener() {
+
+            @Override
+            public DfsBProgramVerifier.ViolenceResponse violationFound(Violation aViolation, DfsBProgramVerifier vfr) {
+
+                System.out.println( aViolation.decsribe() +": "+ aViolation.getCounterExampleTrace().getNodes().stream().filter(e->e.getEvent().isPresent()).map(e->e.getEvent().get().name).reduce("", String::concat));
+                return DfsBProgramVerifier.ViolenceResponse.PRUNE;
+            }
+
+        });
+
+        VerificationResult res = sut.verify(program);
+
+        /*
+        sould be
+              +---- B (pruned)
+            --|       + ---- B (pruned)
+              +---- A |       + ---- B (pruned)
+                      +---- A |       + ---- B (pruned)
+                              +---- A |
+                                      +---- A (stoped)
+         */
+
+        assertEquals( 9, res.getScannedStatesCount());
+        assertEquals( 8, res.getScannedEdgesCount());
+    }
 }

src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/MultipleViolationsTest.java

@@ -62,11 +62,11 @@ public void maxTraceLengthHit(ExecutionTrace aTrace, DfsBProgramVerifier vfr) {
             }
 
             @Override
-            public boolean violationFound(Violation aViolation, DfsBProgramVerifier vfr) {
+            public DfsBProgramVerifier.ViolenceResponse violationFound(Violation aViolation, DfsBProgramVerifier vfr) {
                 int num = violationCount.incrementAndGet();
                 System.out.println("Violation " + num + ": " + aViolation.decsribe() );
                 violations.add(aViolation);
-                return true;
+                return DfsBProgramVerifier.ViolenceResponse.PRUNE;
             }
 
             @Override public void done(DfsBProgramVerifier vfr) {}
@@ -104,10 +104,10 @@ public void maxTraceLengthHit(ExecutionTrace aTrace, DfsBProgramVerifier vfr) {
             }
 
             @Override
-            public boolean violationFound(Violation aViolation, DfsBProgramVerifier vfr) {
+            public DfsBProgramVerifier.ViolenceResponse violationFound(Violation aViolation, DfsBProgramVerifier vfr) {
                 int num = violationCount.incrementAndGet();
                 System.out.println("Violation " + num + ": " + aViolation.decsribe() );
-                return true;
+                return DfsBProgramVerifier.ViolenceResponse.CONTINUE;
             }
 
             @Override public void done(DfsBProgramVerifier vfr) {}
@@ -136,10 +136,10 @@ public void testMultipleHotTerminations() throws Exception {
             public void maxTraceLengthHit(ExecutionTrace aTrace, DfsBProgramVerifier vfr) {}
 
             @Override
-            public boolean violationFound(Violation aViolation, DfsBProgramVerifier vfr) {
+            public DfsBProgramVerifier.ViolenceResponse violationFound(Violation aViolation, DfsBProgramVerifier vfr) {
                 int num = violationCount.incrementAndGet();
                 System.out.println("Violation " + num + ": " + aViolation.decsribe() );
-                return true;
+                return DfsBProgramVerifier.ViolenceResponse.CONTINUE;
             }
 
             @Override public void done(DfsBProgramVerifier vfr) {}

src/test/resources/DFSVerifierTests/AAAA_withBnoice.js

@@ -0,0 +1,48 @@
+/* global bp
+ * The MIT License
+ *
+ * Copyright 2017 michael.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in
+ * all copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+ * THE SOFTWARE.
+ */
+
+
+/**
+ * Simple program whose trace is "A" 4 times.
+ */
+
+bp.registerBThread(function(){
+    for ( var i=0; i<4; i++ ) {
+        bp.sync({request:bp.Event("A")});
+    }
+});
+
+bp.registerBThread(function(){
+//     wait for A and then request A or B
+    bp.sync({request:bp.Event("B"), waitFor:bp.Event("A")});
+    bp.sync({request:bp.Event("B"), waitFor:bp.Event("A")});
+    bp.sync({request:bp.Event("B"), waitFor:bp.Event("A")});
+    bp.sync({request:bp.Event("B"), waitFor:bp.Event("A")});
+});
+
+bp.registerBThread(function(){
+    //wait for B and then assert error
+    bp.sync({waitFor:bp.Event("B")});
+    bp.ASSERT(false, "B should not be requested");
+});