Search node comparison uses source rather than objects for compiled f…

…unctions.
bThink-BGU · Aug 20, 2017 · 2c761ab · 2c761ab
1 parent 2f20b6c
commit 2c761ab
Show file tree

Hide file tree

Showing 12 changed files with 129 additions and 72 deletions.
diff --git a/pom.xml b/pom.xml
@@ -74,6 +74,24 @@
             <artifactId>rhino</artifactId>
             <version>1.7.7.1</version>
         </dependency>
+        <dependency>
+            <groupId>org.seleniumhq.selenium</groupId>
+            <artifactId>selenium-java</artifactId>
+            <scope>test</scope>
+            <version>2.44.0</version>
+        </dependency>
+        <dependency>
+            <groupId>com.opera</groupId>
+            <artifactId>operadriver</artifactId>
+            <scope>test</scope>
+            <version>1.5</version>
+            <exclusions>
+                <exclusion>
+                    <groupId>org.seleniumhq.selenium</groupId>
+                    <artifactId>selenium-remote-driver</artifactId>
+                </exclusion>
+            </exclusions>
+        </dependency>
     </dependencies>
 
     <build>

diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/bprogram/runtimeengine/BProgramSyncSnapshot.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/bprogram/runtimeengine/BProgramSyncSnapshot.java
@@ -238,12 +238,7 @@ public boolean equals(Object obj) {
 		if (getClass() != obj.getClass())
 			return false;
 		BProgramSyncSnapshot other = (BProgramSyncSnapshot) obj;
-		if (threadSnapshots == null) {
-			if (other.threadSnapshots != null)
-				return false;
-		} else if (!threadSnapshots.equals(other.threadSnapshots))
-			return false;
-		return true;
+		return Objects.equals(threadSnapshots, other.threadSnapshots);
 	}
 
 

diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/bprogram/runtimeengine/jsproxy/BProgramJsProxy.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/bprogram/runtimeengine/jsproxy/BProgramJsProxy.java
@@ -42,7 +42,7 @@ public static class BpLog implements java.io.Serializable {
 
         public void log( LogLevel lvl, String msg ) {
             if ( level.compareTo(lvl) >= 0) {
-                System.out.println("[JS][" + lvl.name() + "] " + msg );
+                System.out.println("[BP][" + lvl.name() + "] " + msg );
             }
         }
 

diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/search/ContinuationProgramState.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/search/ContinuationProgramState.java
@@ -28,7 +28,9 @@
 import java.util.Map;
 import java.util.Objects;
 import org.mozilla.javascript.NativeContinuation;
+import org.mozilla.javascript.NativeFunction;
 import org.mozilla.javascript.ScriptableObject;
+import org.mozilla.javascript.Undefined;
 import org.mozilla.javascript.UniqueTag;
 
 /**
@@ -62,7 +64,12 @@ private void collectScopeValues(NativeContinuation nc ){
         while ( current != null ) {
             for ( Object o : current.getIds() ) {
                 if ( ! variables.containsKey(o) && o != "bp" ) {
-                    variables.put(o, current.get(o));
+                    Object variableContent = current.get(o);
+                    if ( variableContent instanceof Undefined ) continue;
+                    if ( variableContent instanceof NativeFunction ) {
+                        variableContent = ((NativeFunction)variableContent).getEncodedSource();
+                    }
+                    variables.put(o, variableContent);
                 }
             }
             if ( current.getPrototype() != null ) {
@@ -94,8 +101,13 @@ private void collectStatus( Object stackFrame ) {
 
             //  - 3: Now get the correct value for the name.
             for ( int i=0; i<argNames.length; i++ ) {
-                variables.put( argNames[i],
-                        objectsStack[i]==UniqueTag.DOUBLE_MARK ? doublesStack[i] : objectsStack[i]);
+                if ( objectsStack[i] instanceof Undefined ) continue;
+                Object variableContent = objectsStack[i]==UniqueTag.DOUBLE_MARK ? doublesStack[i] : objectsStack[i];
+                if ( variableContent instanceof NativeFunction ) {
+                    variableContent = ((NativeFunction)variableContent).getEncodedSource();
+                    System.out.println("variableContent = " + variableContent);
+                }
+                variables.put(argNames[i], variableContent);
             }
 
         } catch (NoSuchFieldException | SecurityException | IllegalAccessException ex) {
@@ -141,7 +153,7 @@ public boolean equals(Object obj) {
 
     @Override
     public String toString() {
-        return "[ActivationFrameStatus pc:" + programCounter + " stackHeight:" + frameIndex + " vars:" + variables + ']';
+        return "[ContinuationProgramState pc:" + programCounter + " stackHeight:" + frameIndex + " vars:" + variables + ']';
     }
 
     public Map<Object, Object> getVisibleVariables() {

diff --git a/...js/search/FullNodeVisitedNodeStorage.java → ...bpjs/search/FullNodeVisitedNodeStore.java b/...js/search/FullNodeVisitedNodeStorage.java → ...bpjs/search/FullNodeVisitedNodeStore.java
@@ -31,7 +31,7 @@
  * 
  * @author michael
  */
-public class FullNodeVisitedNodeStorage  implements VisitedNodeStorage {
+public class FullNodeVisitedNodeStore  implements VisitedNodeStore {
     private final Set<Node> visited = new HashSet<>();
 
     @Override

diff --git a/...p/bpjs/search/HashVisitedNodeStorage.java → .../bp/bpjs/search/HashVisitedNodeStore.java b/...p/bpjs/search/HashVisitedNodeStorage.java → .../bp/bpjs/search/HashVisitedNodeStore.java
@@ -28,13 +28,13 @@
 
 /**
  *
- * A {@link VisitedNodeStorage} that stores the hashcode of a {@link Node}, rather
+ * A {@link VisitedNodeStore} that stores the hashcode of a {@link Node}, rather
  * than the node itself. Far more memory efficient, but runs a (slim) risk of
  * hash collisions.
  * 
  * @author michael
  */
-public class HashVisitedNodeStorage implements VisitedNodeStorage {
+public class HashVisitedNodeStore implements VisitedNodeStore {
     private final Set<Integer> visited = new TreeSet<>();
 
     @Override

diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/search/Node.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/search/Node.java
@@ -1,13 +1,14 @@
 package il.ac.bgu.cs.bp.bpjs.search;
 
 import java.util.Iterator;
-import java.util.Set;
 
 import il.ac.bgu.cs.bp.bpjs.bprogram.runtimeengine.BProgram;
 import il.ac.bgu.cs.bp.bpjs.bprogram.runtimeengine.BProgramSyncSnapshot;
 import il.ac.bgu.cs.bp.bpjs.events.BEvent;
-import il.ac.bgu.cs.bp.bpjs.eventselection.EventSelectionStrategy;
-import il.ac.bgu.cs.bp.bpjs.eventselection.SimpleEventSelectionStrategy;
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Objects;
+import java.util.Set;
 
 /**
  * A single node in a program's execution tree. Contains the program's state, and
@@ -19,8 +20,6 @@
  */
 public class Node {
 
-	private static final EventSelectionStrategy ess = new SimpleEventSelectionStrategy();
-
 	private final BProgramSyncSnapshot systemState;
 	private final BProgram bp;
 	private final Set<BEvent> possibleEvents;
@@ -32,7 +31,7 @@ protected Node(BProgram bp, BProgramSyncSnapshot systemState, BEvent e) {
 		this.systemState = systemState;
 		this.lastEvent = e;
 
-		possibleEvents = ess.selectableEvents(systemState.getStatements(), systemState.getExternalEvents());
+		possibleEvents = bp.getEventSelectionStrategy().selectableEvents(systemState.getStatements(), systemState.getExternalEvents());
 		iterator = possibleEvents.iterator();
 	}
 
@@ -71,7 +70,8 @@ public Set<BEvent> getPossibleEvents() {
 	 * the given event.
 	 * 
 	 * @param e
-	 * @return
+	 * @return State of the BProgram after event {@code e} was selected while the 
+     *         program was at {@code this} node's state.
 	 * @throws InterruptedException
 	 */
 	public Node getNextNode(BEvent e) throws Exception {
@@ -108,7 +108,8 @@ public BProgramSyncSnapshot getSystemState() {
 	public int hashCode() {
 		final int prime = 31;
 		int result = 1;
-		result = prime * result + ((systemState == null) ? 0 : systemState.hashCode());
+		result = prime * result + Objects.hash(systemState);
+		result = prime * result + Objects.hash(lastEvent);
 		return result;
 	}
 

diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/search/StateHashVisitedNodeStore.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/search/StateHashVisitedNodeStore.java
@@ -37,7 +37,7 @@
  * 
  * @author michael
  */
-public class StateHashVisitedNodeStore implements VisitedNodeStorage {
+public class StateHashVisitedNodeStore implements VisitedNodeStore {
     private final Set<Integer> visited = new TreeSet<>();
 
     @Override

diff --git a/...cs/bp/bpjs/search/VisitedNodeStorage.java → ...u/cs/bp/bpjs/search/VisitedNodeStore.java b/...cs/bp/bpjs/search/VisitedNodeStorage.java → ...u/cs/bp/bpjs/search/VisitedNodeStore.java
@@ -28,7 +28,7 @@
  * 
  * @author michael
  */
-public interface VisitedNodeStorage {
+public interface VisitedNodeStore {
     void store( Node nd );
     boolean isVisited( Node nd );
 }
diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/verification/DfsBProgramVerifier.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/verification/DfsBProgramVerifier.java
@@ -25,13 +25,16 @@
 
 import il.ac.bgu.cs.bp.bpjs.bprogram.runtimeengine.BProgram;
 import il.ac.bgu.cs.bp.bpjs.events.BEvent;
+import il.ac.bgu.cs.bp.bpjs.search.ContinuationProgramState;
 import il.ac.bgu.cs.bp.bpjs.search.Node;
 import il.ac.bgu.cs.bp.bpjs.search.StateHashVisitedNodeStore;
-import il.ac.bgu.cs.bp.bpjs.search.VisitedNodeStorage;
 import java.util.ArrayDeque;
 import java.util.ArrayList;
 import java.util.Arrays;
+import java.util.Collections;
 import java.util.List;
+import il.ac.bgu.cs.bp.bpjs.search.VisitedNodeStore;
+import org.mozilla.javascript.NativeContinuation;
 
 /**
  * 
@@ -49,7 +52,7 @@ public class DfsBProgramVerifier {
 
 	private long visitedStatesCount;
 
-    private final VisitedNodeStorage visited = new StateHashVisitedNodeStore();
+    private final VisitedNodeStore visited = new StateHashVisitedNodeStore();
     private long maxTraceLength = DEFAULT_MAX_TRACE;
 
     public VerificationResult verify( BProgram aBp ) throws Exception {
@@ -60,52 +63,62 @@ public VerificationResult verify( BProgram aBp ) throws Exception {
         return new VerificationResult(counterEx, end-start, visitedStatesCount);
     }
 
-    protected List<Node> dfsUsingStack(Node node) throws Exception {
-		ArrayDeque<Node> pathNodes = new ArrayDeque<>(); // Current program stack.
+    protected List<Node> dfsUsingStack(Node aStartNode) throws Exception {
+		ArrayDeque<Node> pathNodes = new ArrayDeque<>(); // Current execution stack.
 
-		visited.store(node);
-		pathNodes.add(node);
-
         long iterationCount = 0;
-		while (!pathNodes.isEmpty()) {
+		visited.store(aStartNode);
+		pathNodes.push(aStartNode);
+
+		while ( !pathNodes.isEmpty() ) {
             iterationCount++;
-			node = pathNodes.peek();
-
-			boolean canGoForward = false;
-
-			while (node.getEventIterator().hasNext()) {
-
-				BEvent e = node.getEventIterator().next();
-
-				Node nextNode = node.getNextNode(e);
-
-				if (!visited.isVisited(nextNode) ) {
-					visitedStatesCount++;
-					canGoForward = true;
+			Node curNode = pathNodes.peek();
+
+            if ( ! curNode.check() ) {
+                // Found a problematic path :-)
+                final ArrayList<Node> counterExampleTrace = new ArrayList<>(Arrays.asList(pathNodes.toArray(new Node[0])));
+                Collections.reverse(counterExampleTrace);
+                return counterExampleTrace;
+            }            
+
+            if ( pathNodes.size() == maxTraceLength ) {
+                // fold stack;
+                pathNodes.pop();
+
+            } else {
+                Node nextNode = getUnvisitedNextNode(curNode);
+                if ( nextNode == null ) {
+                    // fold stack, retry next iteration;
+                    pathNodes.pop();
 
-					visited.store(nextNode);
-					pathNodes.add(nextNode);
-
-					if (!nextNode.check()) {
-						// Found a problematic path :-)
-						return new ArrayList<>(Arrays.asList(pathNodes.toArray(new Node[0])));
-					}
-
-					break;
-				}
-			}
-
+                } else {
+                    // go deeper 
+                    visited.store(nextNode);
+                    pathNodes.push(nextNode);
+                    visitedStatesCount++;
+                }
+            }
+
             if ( iterationCount%1000==0 ) {
                 // TODO - switch to listener architecture.
                 System.out.printf("~ %,d states scanned (iteration %,d)\n", visitedStatesCount, iterationCount);
             }
-			if (!canGoForward || pathNodes.size() >= maxTraceLength) {
-				pathNodes.pop();
-			}
 		}
+
         return null;
 	}
-
+
+    protected Node getUnvisitedNextNode(Node src) throws Exception {
+        while ( src.getEventIterator().hasNext() ) {
+            final BEvent nextEvent = src.getEventIterator().next();
+            Node possibleNextNode = src.getNextNode(nextEvent);
+            if ( ! visited.isVisited(possibleNextNode) ) {
+                return possibleNextNode;
+            }
+        }
+        return null;
+    }
+
     public void setMaxTraceLength(long maxTraceLength) {
         this.maxTraceLength = maxTraceLength;
     }

diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/diningphil/DiningPhilMain.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/diningphil/DiningPhilMain.java
@@ -1,8 +1,20 @@
 package il.ac.bgu.cs.bp.bpjs.diningphil;
 
 import il.ac.bgu.cs.bp.bpjs.bprogram.runtimeengine.SingleResourceBProgram;
+import il.ac.bgu.cs.bp.bpjs.events.BEvent;
+import il.ac.bgu.cs.bp.bpjs.search.Node;
 import il.ac.bgu.cs.bp.bpjs.verification.DfsBProgramVerifier;
 import il.ac.bgu.cs.bp.bpjs.verification.VerificationResult;
+import java.util.Arrays;
+import java.util.List;
+import il.ac.bgu.cs.bp.bpjs.bprogram.runtimeengine.BProgramRunner;
+import il.ac.bgu.cs.bp.bpjs.bprogram.runtimeengine.BThreadSyncSnapshot;
+import il.ac.bgu.cs.bp.bpjs.bprogram.runtimeengine.listeners.StreamLoggerListener;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Set;
+import static java.util.function.Function.identity;
+import java.util.stream.Collectors;
 
 public class DiningPhilMain {
 
@@ -16,13 +28,18 @@ public static void main(String[] args) throws InterruptedException {
         }
         bprog.putInGlobalScope("PHILOSOPHER_COUNT", philosopherCount);
 
+//        BProgramRunner rnr = new BProgramRunner(bprog);
+//        rnr.addListener( new StreamLoggerListener() );
+//        rnr.start();
+
 		try {
             DfsBProgramVerifier vfr = new DfsBProgramVerifier();
             vfr.setMaxTraceLength(50);
             final VerificationResult res = vfr.verify(bprog);
             if ( res.isCounterExampleFound() ) {
                 System.out.println("Found a counterexample");
                 res.getCounterExampleTrace().forEach( nd -> System.out.println(" " + nd.getLastEvent()));
+
             } else {
                 System.out.println("No counterexample found.");
             }