From 547c2a9bc542e382aa6469b782bb41d030346614 Mon Sep 17 00:00:00 2001 From: Michael Bar-Sinai Date: Mon, 18 Feb 2019 01:42:56 +0200 Subject: [PATCH] MOAR TESTSTS --- .../bp/bpjs/analysis/DfsBProgramVerifier.java | 1 - .../bpjs/analysis/violations/Violation.java | 7 +--- .../bp/bpjs/model/BProgramSyncSnapshot.java | 42 ++++++++----------- .../il/ac/bgu/cs/bp/bpjs/GeneralTest.java | 2 + .../analysis/DfsBProgramVerifierTest.java | 11 +++++ .../bpjs/analysis/MultipleViolationsTest.java | 8 ++++ .../cs/bp/bpjs/analysis/NodeEqualsTest.java | 6 +++ .../cs/bp/bpjs/analysis/StateStoreTests.java | 8 +++- .../BProgramSyncSnapshotClonerTest.java | 2 + .../cs/bp/bpjs/mains/ContinuationGames.java | 7 ++-- .../bpjs/model/BThreadSyncSnapshotTest.java | 2 +- 11 files changed, 60 insertions(+), 36 deletions(-) diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java index 7c69e499..3b7d006b 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java @@ -25,7 +25,6 @@ import il.ac.bgu.cs.bp.bpjs.analysis.violations.Violation; import java.util.ArrayList; -import java.util.Collections; import java.util.List; import il.ac.bgu.cs.bp.bpjs.model.BProgram; diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/Violation.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/Violation.java index 8a01b3c7..72c5dca2 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/Violation.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/Violation.java @@ -33,7 +33,7 @@ */ public abstract class Violation { - private ExecutionTrace counterExampleTrace; + private final ExecutionTrace counterExampleTrace; public Violation(ExecutionTrace counterExampleTrace) { this.counterExampleTrace = counterExampleTrace; @@ -50,10 +50,5 @@ public Violation(ExecutionTrace counterExampleTrace) { public ExecutionTrace getCounterExampleTrace() { return counterExampleTrace; } - - public void setCounterExampleTrace(ExecutionTrace counterExampleTrace) { - this.counterExampleTrace = counterExampleTrace; - } - } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java index 64ac2a0e..acd3c2fc 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java @@ -145,36 +145,30 @@ public BProgramSyncSnapshot triggerEvent(BEvent anEvent, ExecutorService exSvc, } BPEngineTask.Listener halter = new ViolationRecorder(bprog, violationRecord); - - try { - // add the run results of all those who advance this stage - nextRound.addAll(exSvc.invokeAll( - resumingThisRound.stream() - .map(bt -> new ResumeBThread(bt, anEvent, halter)) - .collect(toList()) - ).stream().map(f -> safeGet(f)).filter(Objects::nonNull).collect(toList()) - ); - // inform listeners which b-threads completed - Set nextRoundIds = nextRound.stream().map(t->t.getName()).collect(toSet()); - resumingThisRound.stream() - .filter(t->!nextRoundIds.contains(t.getName())) - .forEach(t->listeners.forEach(l->l.bthreadDone(bprog, t))); + // add the run results of all those who advance this stage + nextRound.addAll(exSvc.invokeAll( + resumingThisRound.stream() + .map(bt -> new ResumeBThread(bt, anEvent, halter)) + .collect(toList()) + ).stream().map(f -> safeGet(f)).filter(Objects::nonNull).collect(toList()) + ); - executeAllAddedBThreads(nextRound, exSvc, halter); - nextExternalEvents.addAll( bprog.drainEnqueuedExternalEvents() ); + // inform listeners which b-threads completed + Set nextRoundIds = nextRound.stream().map(t->t.getName()).collect(toSet()); + resumingThisRound.stream() + .filter(t->!nextRoundIds.contains(t.getName())) + .forEach(t->listeners.forEach(l->l.bthreadDone(bprog, t))); - // carry over BThreads that did not advance this round to next round. - nextRound.addAll(sleepingThisRound); + executeAllAddedBThreads(nextRound, exSvc, halter); + nextExternalEvents.addAll( bprog.drainEnqueuedExternalEvents() ); + // carry over BThreads that did not advance this round to next round. + nextRound.addAll(sleepingThisRound); - return new BProgramSyncSnapshot(bprog, nextRound, nextExternalEvents, violationRecord.get()); + + return new BProgramSyncSnapshot(bprog, nextRound, nextExternalEvents, violationRecord.get()); - } catch ( RejectedExecutionException ree ) { - // The executor thread pool must have been shut down, e.g. due to program violation. - return new BProgramSyncSnapshot(bprog, Collections.emptySet(), nextExternalEvents, violationRecord.get()); - - } } private void handleInterrupts(BEvent anEvent, Iterable listeners, BProgram bprog, Context ctxt) { diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/GeneralTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/GeneralTest.java index 77690357..634f8450 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/GeneralTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/GeneralTest.java @@ -116,6 +116,8 @@ public void ended(BProgram bp) { actualFinalEventNames.stream().sorted().forEach( System.out::println ); } + svc.shutdown(); + } } diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifierTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifierTest.java index 1e361654..36f5a729 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifierTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifierTest.java @@ -45,6 +45,17 @@ * @author michael */ public class DfsBProgramVerifierTest { + + @Test + public void sanity() throws Exception { + BProgram program = new ResourceBProgram("DFSVerifierTests/AAABTrace.js"); + DfsBProgramVerifier sut = new DfsBProgramVerifier(); + sut.setDebugMode(true); + sut.setMaxTraceLength(3); + sut.setIterationCountGap(1); + sut.verify(program); + assertEquals( ExecutionTraceInspections.DEFAULT_SET, sut.getInspections() ); + } @Test public void simpleAAABTrace_forgetfulStore() throws Exception { diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/MultipleViolationsTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/MultipleViolationsTest.java index b1ee635b..7aa20bc2 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/MultipleViolationsTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/MultipleViolationsTest.java @@ -25,7 +25,9 @@ import il.ac.bgu.cs.bp.bpjs.analysis.violations.Violation; import il.ac.bgu.cs.bp.bpjs.model.ResourceBProgram; +import java.util.HashSet; import java.util.List; +import java.util.Set; import java.util.concurrent.atomic.AtomicBoolean; import java.util.concurrent.atomic.AtomicInteger; import static org.junit.Assert.assertEquals; @@ -44,6 +46,7 @@ public void testMultipleFailedAssertions() throws Exception { final ResourceBProgram bprog = new ResourceBProgram("DFSVerifierTests/MultipleFailedAssertions.js"); AtomicInteger violationCount = new AtomicInteger(); AtomicBoolean maxLengthHit = new AtomicBoolean(false); + final Set violations = new HashSet<>(); DfsBProgramVerifier vfr = new DfsBProgramVerifier(); vfr.setMaxTraceLength(6); @@ -62,6 +65,7 @@ public void maxTraceLengthHit(List aTrace, DfsBProgramVerifier public boolean violationFound(Violation aViolation, DfsBProgramVerifier vfr) { int num = violationCount.incrementAndGet(); System.out.println("Violation " + num + ": " + aViolation.decsribe() ); + violations.add(aViolation); return true; } @@ -72,7 +76,11 @@ public boolean violationFound(Violation aViolation, DfsBProgramVerifier vfr) { assertFalse( res.isViolationFound() ); assertEquals( 3, violationCount.get() ); + assertEquals( 3, violations.size() ); assertTrue( maxLengthHit.get() ); + Violation v = violations.iterator().next(); + assertFalse( v.equals(null) ); + assertFalse( v.equals("Not a Violation") ); } @Test diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/NodeEqualsTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/NodeEqualsTest.java index e28e88ec..e3e6fb6d 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/NodeEqualsTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/NodeEqualsTest.java @@ -11,6 +11,7 @@ import il.ac.bgu.cs.bp.bpjs.model.StringBProgram; import il.ac.bgu.cs.bp.bpjs.model.BEvent; import java.util.concurrent.ExecutorService; +import org.junit.After; import org.junit.Before; public class NodeEqualsTest { @@ -96,4 +97,9 @@ public void basicsTest() throws Exception { public void setup() { exSvc = ExecutorServiceMaker.makeWithName("Test"); } + + @After + public void teardown() { + exSvc.shutdown(); + } } diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/StateStoreTests.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/StateStoreTests.java index 69bfc0a0..55896a19 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/StateStoreTests.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/StateStoreTests.java @@ -24,6 +24,8 @@ public void ForgetfulStore() throws Exception { DfsTraversalNode next = sut.getUnvisitedNextNode(initial, execSvc); assertFalse(forgetful.isVisited(next.getSystemState())); + + execSvc.shutdown(); } @Test @@ -54,6 +56,7 @@ private void TestAAABTraceStore(VisitedStateStore storeToUse) throws Exception { storeToUse.clear(); assertFalse(storeToUse.isVisited(next.getSystemState())); assertFalse(storeToUse.isVisited(initial.getSystemState())); + execSvc.shutdown(); } @Test @@ -103,6 +106,7 @@ private void TestDiffJSVar(VisitedStateStore storeToUse) throws Exception { BProgramSyncSnapshot state1 = snapshots.get(1).getSystemState(); BProgramSyncSnapshot state2 = snapshots.get(2).getSystemState(); assertNotEquals(state1, state2); + execSvc.shutdown(); } @Test @@ -153,6 +157,7 @@ private void TestEqualJSVar(VisitedStateStore storeToUse) throws Exception { BProgramSyncSnapshot state1 = snapshots.get(1).getSystemState(); BProgramSyncSnapshot state2 = snapshots.get(2).getSystemState(); assertEquals(state1, state2); + execSvc.shutdown(); } /* @@ -198,6 +203,7 @@ private void testEqualRuns(VisitedStateStore storeToUse) throws Exception { storeToUse.store(next1.getSystemState()); assertTrue(storeToUse.isVisited(next2.getSystemState())); } + execSvc.shutdown(); } @Test @@ -242,7 +248,7 @@ private void testStateStoreJavaVars(VisitedStateStore storeToUse) throws Excepti //and now we should see the node next = sut.getUnvisitedNextNode(next, execSvc); assertTrue(storeToUse.isVisited(next.getSystemState())); - + execSvc.shutdown(); } } diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/bprogramio/BProgramSyncSnapshotClonerTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/bprogramio/BProgramSyncSnapshotClonerTest.java index e9e64952..757c7182 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/bprogramio/BProgramSyncSnapshotClonerTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/bprogramio/BProgramSyncSnapshotClonerTest.java @@ -73,6 +73,7 @@ public void testSerialization() throws Exception { BProgramSyncSnapshotIO io = new BProgramSyncSnapshotIO(bprog); byte[] out = io.serialize(cur); io.deserialize(out); + exSvc.shutdown(); } @Test @@ -92,6 +93,7 @@ public void testSerializatioWithExternals() throws Exception { BProgramSyncSnapshot deserialized = io.deserialize(out); assertEquals( Arrays.asList(new BEvent("External1"), new BEvent("External2")), deserialized.getExternalEvents()); + exSvc.shutdown(); } @Test diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/ContinuationGames.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/ContinuationGames.java index 2af80bfb..5baa1db8 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/ContinuationGames.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/ContinuationGames.java @@ -41,6 +41,7 @@ import il.ac.bgu.cs.bp.bpjs.model.BEvent; import java.util.HashMap; import java.util.Map; +import java.util.concurrent.ExecutorService; import org.mozilla.javascript.NativeContinuation; import org.mozilla.javascript.ScriptRuntime; @@ -70,9 +71,10 @@ public static void main(String[] args) throws Exception { // Run the top-level code (b-threads are registered but not yet run) BProgramSyncSnapshot cur = bprog.setup(); + ExecutorService execSvc = ExecutorServiceMaker.makeWithName("TEST"); // Run to first bp.sync - cur = cur.start( ExecutorServiceMaker.makeWithName("TEST")); + cur = cur.start(execSvc); // Get a snapshot final BThreadSyncSnapshot snapshot = cur.getBThreadSnapshots().iterator().next(); @@ -80,7 +82,6 @@ public static void main(String[] args) throws Exception { // Serialize snapshot byte[] serializedContinuationAndScope = null; - Object bp = null; try { Context ctxt = Context.enter(); // need Javascript environment for this, even though we're not executing code per se. @@ -91,7 +92,6 @@ public static void main(String[] args) throws Exception { for ( Scriptable sc=scope; sc!=null; sc = sc.getParentScope() ) { System.out.println("SCOPE START"); if ( sc.has("bp", sc) ) { - bp = sc.get("bp", sc); sc.delete("bp"); System.out.println("bp deleted."); } @@ -111,6 +111,7 @@ public static void main(String[] args) throws Exception { } System.out.println("Seriazlied to " + serializedContinuationAndScope.length + " bytes."); } finally { + execSvc.shutdown(); Context.exit(); } diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/model/BThreadSyncSnapshotTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/model/BThreadSyncSnapshotTest.java index 517f0002..eeaab499 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/model/BThreadSyncSnapshotTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/model/BThreadSyncSnapshotTest.java @@ -92,7 +92,7 @@ public void testJavaVarState() throws InterruptedException { EventSelectionResult esr = bprog.getEventSelectionStrategy().select(postSync1, possibleEvents).get(); BProgramSyncSnapshot postSync2 = postSync1.triggerEvent(esr.getEvent(), execSvcA, listeners); assertNotEquals(postSync1.getBThreadSnapshots(), postSync2.getBThreadSnapshots()); - execSvcA.shutdown();; + execSvcA.shutdown(); }