No logs during verification (closes #160)

Author: michbarsinai

README.md

@@ -63,7 +63,7 @@ If you use BPjs in an academic work, please consider citing it as:
 * :bug: Verification stops on ECMAScript errors ([#49](https://github.com/bThink-BGU/BPjs/issues/49)).
 * :bug: Improved error reporting when trying to sync outside of a b-thread ([#174](https://github.com/bThink-BGU/BPjs/issues/174)).
 * :arrow_up: Informative error message when requesting a list of events and one of the events is `null` ([#184](https://github.com/bThink-BGU/BPjs/issues/184)).
-
+* :arrow_up: Loggins is turned off by default during verification. Call `BPjs.setLogDuringVerification(true)` to enable them again ([#160](https://github.com/bThink-BGU/BPjs/issues/160)).
 
 ### 2022-02 (Including the 1st BP Day Hackathon)
 * :part_alternation_mark: Calling `bp.sync` from global scope during runtime does not cause an ugly exception anymore ([#174](https://github.com/bThink-BGU/BPjs/issues/174)). The error is reported to the listeners.

src/main/java/il/ac/bgu/cs/bp/bpjs/BPjs.java

@@ -45,6 +45,8 @@ public class BPjs {
     private static ScriptableObject BPJS_SCOPE;
 
     private static ExecutorServiceMaker executorServiceMaker = new ExecutorServiceMaker();
+    
+    private static boolean logDuringVerification = false;
 
     static {
         ContextFactory.initGlobal( new BPjsRhinoContextFactory()) ;
@@ -124,6 +126,23 @@ public static ExecutorServiceMaker getExecutorServiceMaker() {
     public static void setExecutorServiceMaker(ExecutorServiceMaker executorServiceMaker) {
         BPjs.executorServiceMaker = executorServiceMaker;
     }
+
+    /**
+     * When set to {@code false}, calls to {@code bp.log} during verifications will
+     * be ignored. Defaults to {@code false}.
+     * @return Should the system honor logging calls during verifications.
+     */
+    public static boolean isLogDuringVerification() {
+        return logDuringVerification;
+    }
+
+    /**
+     * Sets whether calls to the logger should be respected during verification.
+     * @param logDuringVerification 
+     */
+    public static void setLogDuringVerification(boolean logDuringVerification) {
+        BPjs.logDuringVerification = logDuringVerification;
+    }
 
 
 }

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

@@ -27,6 +27,7 @@
 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.exceptions.BPjsRuntimeException;
+import il.ac.bgu.cs.bp.bpjs.execution.jsproxy.BpLog;
 import java.util.ArrayList;
 import java.util.List;
 
@@ -169,6 +170,10 @@ public VerificationResult verify(BProgram aBp) throws Exception {
 
         ExecutorService execSvc = BPjs.getExecutorServiceMaker().makeWithName("DfsBProgramRunner-" + INSTANCE_COUNTER.incrementAndGet());
 
+        BpLog.LogLevel prevLevel = currentBProgram.getLogLevel();
+        if ( ! BPjs.isLogDuringVerification() ) {
+            currentBProgram.setLogLevel(BpLog.LogLevel.Off);
+        }
         long start = System.currentTimeMillis();
         listener.started(this);
         try {
@@ -183,6 +188,9 @@ public VerificationResult verify(BProgram aBp) throws Exception {
         } finally {            
             listener.done(this);
             execSvc.shutdown();
+            if ( ! BPjs.isLogDuringVerification() ) {
+                currentBProgram.setLogLevel(prevLevel);
+            }
         }
     }
 

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

@@ -52,15 +52,15 @@
 public class ExecutionTraceInspections {
 
     /**
-     * Detects a deadlock in a b-program: where there are requested events, but
-     * non of them is selectable.
+     * Detects a deadlock in a b-program: where there are requested events,
+     * and none of them is selectable.
      */
     public static final ExecutionTraceInspection DEADLOCKS = ExecutionTraceInspection.named(
         "Deadlocks",
         trace -> {
             if ( trace.isCyclic() ) return Optional.empty(); 
             BProgramSyncSnapshot curState = trace.getLastState();
-            if (hasRequestedEvents(curState) &&
+            if (hasRequestedEvents(curState) && 
                 trace.getBProgram().getEventSelectionStrategy().selectableEvents(curState).isEmpty()) {
                 return Optional.of(new DeadlockViolation(trace));
             } else return Optional.empty();

src/main/java/il/ac/bgu/cs/bp/bpjs/execution/jsproxy/BpLog.java

@@ -30,19 +30,22 @@
 import java.text.MessageFormat;
 import java.util.Arrays;
 import java.util.Set;
-import org.mozilla.javascript.NativeArray;
 
 /**
  * Simple logging mechanism for {@link BProgram}s.
  * 
  * @author michael
  */
 public class BpLog implements java.io.Serializable {
-    private PrintStream out;
+    
     public enum LogLevel {
         Off, Warn, Info, Fine
     }
-    LogLevel level = LogLevel.Info;
+    
+    public static final LogLevel DEFAULT_LOG_LEVEL = LogLevel.Info;
+    
+    LogLevel level = DEFAULT_LOG_LEVEL;
+    private PrintStream out;
 
     public BpLog( PrintStream aStream ){
         out = aStream;

src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgram.java

@@ -519,7 +519,9 @@ public void setLoggerOutputStreamer(PrintStream printStream){
     }
 
     public BpLog.LogLevel getLogLevel() {
-        return (jsProxy != null ) ? BpLog.LogLevel.valueOf(jsProxy.log.getLevel()) : null;
+        return (jsProxy != null ) 
+            ? BpLog.LogLevel.valueOf(jsProxy.log.getLevel()) 
+            : BpLog.DEFAULT_LOG_LEVEL;
     }
 
     public StorageModificationStrategy getStorageModificationStrategy() {