From 3fd4c1d647c31f989863113ebdb4ed3680203e40 Mon Sep 17 00:00:00 2001 From: Michael Bar-Sinai Date: Sun, 24 Mar 2019 16:08:43 +0200 Subject: [PATCH] Finalizing towards 0.10.2 --- README.md | 3 +++ dependency-reduced-pom.xml | 4 ++-- pom.xml | 20 +++++++++++++++---- .../bp/bpjs/analysis/DfsBProgramVerifier.java | 6 +++--- .../bpjs/analysis/HashVisitedStateStore.java | 17 ++++------------ .../bp/bpjs/analysis/VerificationResult.java | 2 +- .../bgu/cs/bp/bpjs/mains/BPJsCliRunner.java | 4 ++-- .../bp/bpjs/model/BProgramSyncSnapshot.java | 6 +++++- .../cs/bp/bpjs/model/eventsets/EventSets.java | 5 +++-- .../TicTacToe/TicTacToeVerificationMain.java | 2 +- .../analysis/ArrayExecutionTraceTest.java | 7 ------- .../analysis/DfsBProgramVerifierTest.java | 16 +++++++-------- .../bp/bpjs/analysis/SnapshotBenchmarks.java | 10 +++++----- .../TemperatureVerificationsTest.java | 2 +- .../cs/bp/bpjs/analysis/examples/Mazes.java | 4 ++-- .../jsproxy/BProgramJsProxyTest.java | 2 +- .../bpjs/mains/CaseofTheHotFruitBProgram.java | 2 +- .../StateStorePerformanceComparison.java | 8 ++++---- 18 files changed, 62 insertions(+), 58 deletions(-) diff --git a/README.md b/README.md index 7b1e85d5..5f63f04c 100644 --- a/README.md +++ b/README.md @@ -44,6 +44,9 @@ a link to this page somewhere in the documentation/system about section. ## Change Log for the BPjs Library. +### 2019-03-10 +* :put_litter_in_its_place: Code cleanup. + ### 2019-03-05 * :sparkles: Serious makeover for the composable event suite. Users can no compose event sets using `or`,`and`, and `not` (and even `xor`, `nor` and `nand`) and get semantically correct sets that support verification. for example, this works: diff --git a/dependency-reduced-pom.xml b/dependency-reduced-pom.xml index dbaf3604..f0248645 100644 --- a/dependency-reduced-pom.xml +++ b/dependency-reduced-pom.xml @@ -4,7 +4,7 @@ com.github.bthink-bgu BPjs BPjs - 0.10.1-SNAPSHOT + 0.10.1 Provides a runtime for behavioral programs written in Javascript. It can run stand-alone (from the commmandline) or be embedded in larger JVM-based systems. @@ -260,8 +260,8 @@ - il.ac.bgu.cs.bp.bpjs.mains.BPJsCliRunner 1.8 + il.ac.bgu.cs.bp.bpjs.mains.BPJsCliRunner UTF-8 diff --git a/pom.xml b/pom.xml index d747d2d8..9f0d3bba 100644 --- a/pom.xml +++ b/pom.xml @@ -5,15 +5,15 @@ com.github.bthink-bgu BPjs - 0.10.1-SNAPSHOT + 0.10.2-SNAPSHOT jar BPjs https://github.com/bThink-BGU/ - Provides a runtime for behavioral programs written in Javascript. It can - run stand-alone (from the commmandline) or be embedded in larger - JVM-based systems. + Provides runtime and analysis for behavioral programs written in + JavaScript. It can run stand-alone (from the commmandline) or be + embedded in larger JVM-based systems. @@ -144,6 +144,18 @@ + + org.apache.maven.plugins + maven-jar-plugin + 3.1.1 + + + + il.ac.bgu.cs.bp.bpjs.mains.BPJsCliRunner + + + + 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 6fa1a2d7..9a49e804 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 @@ -265,11 +265,11 @@ public long getMaxTraceLength() { return maxTraceLength; } - public void setVisitedNodeStore(VisitedStateStore aVisitedNodeStore) { - visited = aVisitedNodeStore; + public void setVisitedStateStore(VisitedStateStore aVisitedStateStore) { + visited = aVisitedStateStore; } - public VisitedStateStore getVisitedNodeStore() { + public VisitedStateStore getVisitedStateStore() { return visited; } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/HashVisitedStateStore.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/HashVisitedStateStore.java index 04f40857..49979a3a 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/HashVisitedStateStore.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/HashVisitedStateStore.java @@ -24,35 +24,26 @@ package il.ac.bgu.cs.bp.bpjs.analysis; import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; -import il.ac.bgu.cs.bp.bpjs.model.BThreadSyncSnapshot; +import java.util.HashSet; import java.util.Set; -import java.util.TreeSet; /** * A {@link VisitedStateStore} that uses a hash function over the BProgram's states. * @author michael */ public class HashVisitedStateStore implements VisitedStateStore { - private final Set visited = new TreeSet<>(); + private final Set visited = new HashSet<>(); @Override public void store(BProgramSyncSnapshot bss) { - visited.add( hash(bss.getBThreadSnapshots()) ); + visited.add( bss.hashCode() ); } @Override public boolean isVisited(BProgramSyncSnapshot bss) { - return visited.contains( hash(bss.getBThreadSnapshots()) ); + return visited.contains( bss.hashCode() ); } - private long hash( Set snapshots ) { - long hash = 1; - for ( BThreadSyncSnapshot snp : snapshots ) { - hash = hash * snp.getContinuationProgramState().hashCode();// * (snp.getName().hashCode()+1); - } - return hash; - } - @Override public long getVisitedStateCount() { return visited.size(); diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/VerificationResult.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/VerificationResult.java index bd2cb29a..5556f879 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/VerificationResult.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/VerificationResult.java @@ -62,7 +62,7 @@ public long getScannedStatesCount() { return statesScanned; } - public long getEdgesScanned() { + public long getScannedEdgesCount() { return edgesScanned; } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/mains/BPJsCliRunner.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/mains/BPJsCliRunner.java index 815409e9..8edd4c68 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/mains/BPJsCliRunner.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/mains/BPJsCliRunner.java @@ -117,9 +117,9 @@ private void logScriptExceptionAndQuit(EvaluatorException ee, String arg) { if ( switchPresent("--full-state-storage", args) ) { println("Using full state storage"); - vfr.setVisitedNodeStore( new BThreadSnapshotVisitedStateStore() ); + vfr.setVisitedStateStore( new BThreadSnapshotVisitedStateStore() ); } else { - vfr.setVisitedNodeStore( new HashVisitedStateStore() ); + vfr.setVisitedStateStore( new HashVisitedStateStore() ); } if ( switchPresent("--liveness", args) ) { vfr.addInspection(ExecutionTraceInspections.HOT_BPROGRAM_CYCLES); 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 b8658652..12800eac 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 @@ -49,6 +49,7 @@ public class BProgramSyncSnapshot { private final List externalEvents; private final BProgram bprog; private final AtomicReference violationRecord = new AtomicReference<>(); + private transient int hashCodeCache = Integer.MIN_VALUE; /** A flag to ensure the snapshot is only triggered once. */ private boolean triggered=false; @@ -327,7 +328,10 @@ Stream convertToTasks(ForkStatement fkStmt, BPEngineTask.Listener lis @Override public int hashCode() { - return Objects.hash(threadSnapshots, externalEvents); + if ( hashCodeCache == Integer.MIN_VALUE ) { + hashCodeCache = Objects.hash(threadSnapshots, externalEvents); + } + return hashCodeCache; } @Override diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventsets/EventSets.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventsets/EventSets.java index dcd20877..d5fd57e1 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventsets/EventSets.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventsets/EventSets.java @@ -1,6 +1,7 @@ package il.ac.bgu.cs.bp.bpjs.model.eventsets; import il.ac.bgu.cs.bp.bpjs.model.BEvent; +import java.io.ObjectStreamException; /** * Utility class for commonly used event sets. @@ -27,7 +28,7 @@ public String toString() { return ("{all}"); } - private Object readResolve() { + private Object readResolve() throws ObjectStreamException { return all; } }; @@ -47,7 +48,7 @@ public String toString() { return "{none}"; } - private Object readResolve() { + private Object readResolve() throws ObjectStreamException { return none; } }; diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/TicTacToe/TicTacToeVerificationMain.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/TicTacToe/TicTacToeVerificationMain.java index d020c51a..92f8722d 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/TicTacToe/TicTacToeVerificationMain.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/TicTacToe/TicTacToeVerificationMain.java @@ -46,7 +46,7 @@ public static void main(String[] args) throws InterruptedException { vfr.setMaxTraceLength(70); // vfr.setDebugMode(true); - vfr.setVisitedNodeStore(new BThreadSnapshotVisitedStateStore()); + vfr.setVisitedStateStore(new BThreadSnapshotVisitedStateStore()); vfr.setProgressListener(new PrintDfsVerifierListener() ); final VerificationResult res = vfr.verify(bprog); diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/ArrayExecutionTraceTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/ArrayExecutionTraceTest.java index af3d8ba8..f803e402 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/ArrayExecutionTraceTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/ArrayExecutionTraceTest.java @@ -26,15 +26,8 @@ import static il.ac.bgu.cs.bp.bpjs.TestUtils.makeBPSS; import il.ac.bgu.cs.bp.bpjs.mocks.MockBThreadSyncSnapshot; import il.ac.bgu.cs.bp.bpjs.model.BEvent; -import il.ac.bgu.cs.bp.bpjs.model.BProgram; -import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; import il.ac.bgu.cs.bp.bpjs.model.StringBProgram; import il.ac.bgu.cs.bp.bpjs.model.SyncStatement; -import java.util.List; -import org.junit.After; -import org.junit.AfterClass; -import org.junit.Before; -import org.junit.BeforeClass; import org.junit.Test; import static org.junit.Assert.*; 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 36f5a729..e5c51511 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 @@ -63,7 +63,7 @@ public void simpleAAABTrace_forgetfulStore() throws Exception { DfsBProgramVerifier sut = new DfsBProgramVerifier(); sut.setProgressListener(new PrintDfsVerifierListener()); program.appendSource(Requirements.eventNotSelected("B")); - sut.setVisitedNodeStore(new ForgetfulVisitedStateStore()); + sut.setVisitedStateStore(new ForgetfulVisitedStateStore()); VerificationResult res = sut.verify(program); assertTrue(res.isViolationFound()); assertEquals("AAAB", traceEventNamesString(res, "")); @@ -77,7 +77,7 @@ public void simpleAAABTrace() throws Exception { sut.setProgressListener(new PrintDfsVerifierListener()); program.appendSource(Requirements.eventNotSelected("B")); - sut.setVisitedNodeStore(new BThreadSnapshotVisitedStateStore()); + sut.setVisitedStateStore(new BThreadSnapshotVisitedStateStore()); VerificationResult res = sut.verify(program); assertTrue(res.isViolationFound()); assertEquals("AAAB", traceEventNamesString(res, "")); @@ -91,12 +91,12 @@ public void simpleAAABTrace_hashedNodeStore() throws Exception { sut.setProgressListener(new PrintDfsVerifierListener()); program.appendSource(Requirements.eventNotSelected("B")); VisitedStateStore stateStore = new HashVisitedStateStore(); - sut.setVisitedNodeStore(stateStore); + sut.setVisitedStateStore(stateStore); VerificationResult res = sut.verify(program); assertTrue(res.isViolationFound()); assertEquals("AAAB", traceEventNamesString(res, "")); //Add trivial getter check - VisitedStateStore retStore = sut.getVisitedNodeStore(); + VisitedStateStore retStore = sut.getVisitedStateStore(); assertSame(retStore, stateStore); } @@ -117,7 +117,7 @@ public void testAAABRun() { public void deadlockTrace() throws Exception { BProgram program = new ResourceBProgram("DFSVerifierTests/deadlocking.js"); DfsBProgramVerifier sut = new DfsBProgramVerifier(); - sut.setVisitedNodeStore(new ForgetfulVisitedStateStore()); + sut.setVisitedStateStore(new ForgetfulVisitedStateStore()); VerificationResult res = sut.verify(program); assertTrue(res.isViolationFound()); @@ -163,7 +163,7 @@ public void testTwoSimpleBThreads() throws Exception { assertFalse(res.isViolationFound()); assertEquals(4, res.getScannedStatesCount()); - assertEquals(4, res.getEdgesScanned()); + assertEquals(4, res.getScannedEdgesCount()); } @Test(timeout = 2000) @@ -236,7 +236,7 @@ public void testVariablesEquailtyInBT() throws Exception { assertEquals(5, res.getScannedStatesCount()); // in this case only one option per state - assertEquals(5, res.getEdgesScanned()); + assertEquals(5, res.getScannedEdgesCount()); } @@ -299,7 +299,7 @@ public void testJavaVariablesInBT() throws Exception { assertTrue(res.isViolationFound()); assertTrue(res.getViolation().get() instanceof FailedAssertionViolation); assertEquals(2, res.getScannedStatesCount()); - assertEquals(1, res.getEdgesScanned()); + assertEquals(1, res.getScannedEdgesCount()); } } diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/SnapshotBenchmarks.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/SnapshotBenchmarks.java index 5d5a52e1..5dc12af1 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/SnapshotBenchmarks.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/SnapshotBenchmarks.java @@ -152,9 +152,9 @@ private static BenchmarkResult measureProgram(int object_type) throws Exception System.gc(); snapshotSet[i] = getStateSizes(makeBProgram(IMPLEMENTATION, valueMap), NUM_STEPS); System.gc(); - verifier.setVisitedNodeStore(store); + verifier.setVisitedStateStore(store); verificationTimes[i] = getVerification(verifier, IMPLEMENTATION, valueMap, ITERATIONS); - verifier.setVisitedNodeStore(storeHash); + verifier.setVisitedStateStore(storeHash); verificationTimesHash[i] = getVerification(verifier, IMPLEMENTATION, valueMap, ITERATIONS); System.gc(); @@ -229,9 +229,9 @@ private static BenchmarkResult measureProgram(EventSelectionStrategy strategy, i System.gc(); snapshotSet[i] = getStateSizes(makeBProgram(IMPLEMENTATION, valueMap, strategy), NUM_STEPS); System.gc(); - verifier.setVisitedNodeStore(store); + verifier.setVisitedStateStore(store); verificationTimes[i] = getVerificationTime(verifier, IMPLEMENTATION, valueMap, ITERATIONS, strategy); - verifier.setVisitedNodeStore(storeHash); + verifier.setVisitedStateStore(storeHash); verificationTimesHash[i] = getVerificationTime(verifier, IMPLEMENTATION, valueMap, ITERATIONS, strategy); System.gc(); @@ -252,7 +252,7 @@ private static BProgram makeBProgram(String programPath, Map val } static VerificationResult[] getVerificationTime(DfsBProgramVerifier vfr, String programPath, Map valueMap, int iteration_count, EventSelectionStrategy strategy) { - String res = String.format("Measuring Verification time with %s store", vfr.getVisitedNodeStore().getClass().getName()); + String res = String.format("Measuring Verification time with %s store", vfr.getVisitedStateStore().getClass().getName()); LOGGER.info(res); return LongStream.range(0, iteration_count).mapToObj(i -> { try { diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/TemperatureVerificationsTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/TemperatureVerificationsTest.java index 53834131..4653d956 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/TemperatureVerificationsTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/TemperatureVerificationsTest.java @@ -93,7 +93,7 @@ public void testHotBProgramCycle_withJsEventSets() throws Exception { DfsBProgramVerifier vfr = new DfsBProgramVerifier(); // Adding the inspector means it will be the only inspector run, as the default set will not be used. vfr.addInspection(ExecutionTraceInspections.HOT_BPROGRAM_CYCLES); - vfr.setVisitedNodeStore( new BThreadSnapshotVisitedStateStore() ); + vfr.setVisitedStateStore( new BThreadSnapshotVisitedStateStore() ); final VerificationResult res = vfr.verify(bprog); assertTrue(res.isViolationFound()); diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/Mazes.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/Mazes.java index 454136e5..aa7a30bc 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/Mazes.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/Mazes.java @@ -87,8 +87,8 @@ public void verify() throws InterruptedException { vfr.setProgressListener(new PrintDfsVerifierListener()); vfr.setIterationCountGap(10); - vfr.setVisitedNodeStore(new BThreadSnapshotVisitedStateStore()); -// vfr.setVisitedNodeStore(new ForgetfulVisitedStateStore()); + vfr.setVisitedStateStore(new BThreadSnapshotVisitedStateStore()); +// vfr.setVisitedStateStore(new ForgetfulVisitedStateStore()); vfr.addInspection(ExecutionTraceInspections.FAILED_ASSERTIONS); // We only want failed assertions, deadlocks are OK here, in the greateer program(!) final VerificationResult res = vfr.verify(bprog); diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/execution/jsproxy/BProgramJsProxyTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/execution/jsproxy/BProgramJsProxyTest.java index e11b0707..66fc7d5c 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/execution/jsproxy/BProgramJsProxyTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/execution/jsproxy/BProgramJsProxyTest.java @@ -100,7 +100,7 @@ public void testEquality() { public void DeadlockSameThread() throws Exception{ BProgram bpr = new ResourceBProgram("bpsync-blockrequest.js"); DfsBProgramVerifier sut = new DfsBProgramVerifier(); - sut.setVisitedNodeStore(new BThreadSnapshotVisitedStateStore()); + sut.setVisitedStateStore(new BThreadSnapshotVisitedStateStore()); VerificationResult res = sut.verify(bpr); assertTrue(res.isViolationFound()); assertTrue(res.getViolation().get() instanceof DeadlockViolation); diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/CaseofTheHotFruitBProgram.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/CaseofTheHotFruitBProgram.java index fb780949..1fe51a3d 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/CaseofTheHotFruitBProgram.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/CaseofTheHotFruitBProgram.java @@ -60,7 +60,7 @@ public static void verify(BProgram bprog) throws Exception { DfsBProgramVerifier vfr = new DfsBProgramVerifier(); // Adding the inspector means it will be the only inspector run, as the default set will not be used. vfr.addInspection(ExecutionTraceInspections.HOT_BPROGRAM_CYCLES); - vfr.setVisitedNodeStore( new BThreadSnapshotVisitedStateStore() ); + vfr.setVisitedStateStore( new BThreadSnapshotVisitedStateStore() ); final VerificationResult res = vfr.verify(bprog); System.out.println("Violation found: " + res.isViolationFound()); diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/StateStorePerformanceComparison.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/StateStorePerformanceComparison.java index 6677febb..dd69b35d 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/StateStorePerformanceComparison.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/StateStorePerformanceComparison.java @@ -61,11 +61,11 @@ public static void main(String[] args) throws Exception { verifier.addInspection(ExecutionTraceInspections.FAILED_ASSERTIONS); // test - verifier.setVisitedNodeStore(new BThreadSnapshotVisitedStateStore()); + verifier.setVisitedStateStore(new BThreadSnapshotVisitedStateStore()); runVerifier(verifier); - verifier.setVisitedNodeStore(new HashVisitedStateStore()); + verifier.setVisitedStateStore(new HashVisitedStateStore()); runVerifier(verifier); - verifier.setVisitedNodeStore(new ForgetfulVisitedStateStore()); + verifier.setVisitedStateStore(new ForgetfulVisitedStateStore()); runVerifier(verifier); } @@ -80,7 +80,7 @@ private static BProgram makeBProgram() { } private static void runVerifier(DfsBProgramVerifier vfr) throws Exception { - System.out.println("Testing " + vfr.getVisitedNodeStore()); + System.out.println("Testing " + vfr.getVisitedStateStore()); System.out.println("Heating up"); for (int i = 0; i < HEAT_UP_ITERATIONS; i++) { vfr.verify(makeBProgram());