From e55fe1d5e8fbad087d850fdb1865dc6c7d77db9d Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Mon, 9 Sep 2024 23:35:29 +0000 Subject: [PATCH] [PEx] Refactoring and formatting changes --- .../src/main/java/pex/RuntimeExecutor.java | 6 +- .../src/main/java/pex/runtime/PExGlobal.java | 18 +-- .../java/pex/runtime/logger/PExLogger.java | 13 +- .../pex/runtime/logger/SchedulerLogger.java | 10 +- .../java/pex/runtime/logger/TraceLogger.java | 134 ------------------ .../explicit/SchedulerStatistics.java | 2 +- .../runtime/scheduler/explicit/StepState.java | 1 - .../scheduler/replay/ReplayScheduler.java | 1 + .../exceptions/TooManyChoicesException.java | 1 + 9 files changed, 25 insertions(+), 161 deletions(-) delete mode 100644 Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/TraceLogger.java diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/RuntimeExecutor.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/RuntimeExecutor.java index 236c76aa5c..9dd5ccdf42 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/RuntimeExecutor.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/RuntimeExecutor.java @@ -157,7 +157,7 @@ private static void process() throws Exception { throw new Exception("MEMOUT", e); } catch (BugFoundException e) { PExGlobal.setStatus(STATUS.BUG_FOUND); - PExGlobal.setResult(String.format("found cex of length %d", e.getScheduler().getStepNumber())); + PExGlobal.setResult(String.format("found cex of length %,d", e.getScheduler().getStepNumber())); if (e instanceof TooManyChoicesException) { PExGlobal.setResult(PExGlobal.getResult() + " (too many choices)"); } @@ -229,13 +229,13 @@ private static void replaySchedule(String fileName) throws Exception { replayer.run(); } catch (NullPointerException | StackOverflowError | ClassCastException replayException) { PExGlobal.setStatus(STATUS.BUG_FOUND); - PExGlobal.setResult(String.format("found cex of length %d", replayer.getStepNumber())); + PExGlobal.setResult(String.format("found cex of length %,d", replayer.getStepNumber())); replayer.getLogger().logStackTrace((Exception) replayException); PExLogger.logTrace((Exception) replayException); throw new BugFoundException(replayException.getMessage(), replayException); } catch (BugFoundException replayException) { PExGlobal.setStatus(STATUS.BUG_FOUND); - PExGlobal.setResult(String.format("found cex of length %d", replayer.getStepNumber())); + PExGlobal.setResult(String.format("found cex of length %,d", replayer.getStepNumber())); if (replayException instanceof TooManyChoicesException) { PExGlobal.setResult(PExGlobal.getResult() + " (too many choices)"); } diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/PExGlobal.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/PExGlobal.java index c5eda8a838..51d4047a2f 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/PExGlobal.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/PExGlobal.java @@ -245,13 +245,13 @@ public static void updateResult() { if (numUnexplored == 0) { resultString += "correct for any depth"; } else { - resultString += String.format("partially correct with %d choices remaining", numUnexplored); + resultString += String.format("partially correct with %,d choices remaining", numUnexplored); } } else { if (numUnexplored == 0) { - resultString += String.format("correct up to step %d", getMaxSteps()); + resultString += String.format("correct up to step %,d", getMaxSteps()); } else { - resultString += String.format("partially correct up to step %d with %d choices remaining", getMaxSteps(), numUnexplored); + resultString += String.format("partially correct up to step %,d with %,d choices remaining", getMaxSteps(), numUnexplored); } } result = resultString; @@ -332,12 +332,12 @@ public static void printProgress(boolean forcePrint) { s.append(StringUtils.center(String.format("%s", runtimeHms), 11)); s.append( StringUtils.center(String.format("%.1f GB", MemoryMonitor.getMemSpent() / 1024), 9)); - s.append(StringUtils.center(String.format("%d / %d / %d", + s.append(StringUtils.center(String.format("%,d / %,d / %,d", runningTasks.size(), finishedTasks.size(), pendingTasks.size()), 24)); - s.append(StringUtils.center(String.format("%d", getTotalSchedules()), 12)); - s.append(StringUtils.center(String.format("%d", timelines.size()), 12)); + s.append(StringUtils.center(String.format("%,d", getTotalSchedules()), 12)); + s.append(StringUtils.center(String.format("%,d", timelines.size()), 12)); // s.append( // StringUtils.center( // String.format( @@ -345,7 +345,7 @@ public static void printProgress(boolean forcePrint) { // 24)); if (config.getStateCachingMode() != StateCachingMode.None) { - s.append(StringUtils.center(String.format("%d", stateCache.size()), 12)); + s.append(StringUtils.center(String.format("%,d", stateCache.size()), 12)); } System.out.print(s); @@ -380,8 +380,8 @@ public static int getMaxSteps() { return result; } - public static int getTotalSteps() { - int result = 0; + public static long getTotalSteps() { + long result = 0; for (ExplicitSearchScheduler sch : searchSchedulers.values()) { result += sch.getStats().totalSteps; } diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/PExLogger.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/PExLogger.java index a351137461..1acdbe28ff 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/PExLogger.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/PExLogger.java @@ -13,9 +13,6 @@ import pex.runtime.scheduler.explicit.strategy.SearchStrategyMode; import pex.utils.monitor.MemoryMonitor; -import java.io.PrintWriter; -import java.io.StringWriter; - /** * Represents the main PEx logger */ @@ -78,16 +75,16 @@ public static void logEndOfRun(long timeSpent) { if (PExGlobal.getConfig().getSearchStrategyMode() != SearchStrategyMode.Replay) { log.info("... Search statistics:"); if (PExGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) { - log.info(String.format("..... Explored %d distinct states over %d timelines", + log.info(String.format("..... Explored %,d distinct states over %,d timelines", PExGlobal.getStateCache().size(), PExGlobal.getTimelines().size())); } - log.info(String.format("..... Explored %d distinct schedules", PExGlobal.getTotalSchedules())); - log.info(String.format("..... Finished %d search tasks (%d pending)", + log.info(String.format("..... Explored %,d distinct schedules", PExGlobal.getTotalSchedules())); + log.info(String.format("..... Finished %,d search tasks (%,d pending)", PExGlobal.getFinishedTasks().size(), PExGlobal.getPendingTasks().size())); - log.info(String.format("..... Number of steps explored: %d (min), %d (avg), %d (max).", + log.info(String.format("..... Number of steps explored: %,d (min), %,d (avg), %,d (max).", PExGlobal.getMinSteps(), (PExGlobal.getTotalSteps() / PExGlobal.getTotalSchedules()), PExGlobal.getMaxSteps())); } - log.info(String.format("... Elapsed %d seconds and used %.1f GB", timeSpent, MemoryMonitor.getMaxMemSpent() / 1000.0)); + log.info(String.format("... Elapsed %,d seconds and used %.1f GB", timeSpent, MemoryMonitor.getMaxMemSpent() / 1000.0)); log.info(String.format(".. \033[0;30;47m Result: %s \033[m", PExGlobal.getResult())); log.info(". Done"); } diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/SchedulerLogger.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/SchedulerLogger.java index 37d86f0a03..f8d70b0115 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/SchedulerLogger.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/SchedulerLogger.java @@ -104,7 +104,7 @@ public void logStartTask(SearchTask task) { */ public void logEndTask(SearchTask task, int numSchedules) { if (verbosity > 0) { - log.info(String.format(" Finished %s after exploring %d schedules", task, numSchedules)); + log.info(String.format(" Finished %s after exploring %,d schedules", task, numSchedules)); } } @@ -121,7 +121,7 @@ public void logNextTask(SearchTask task) { public void logNewTasks(List tasks) { if (verbosity > 0) { - log.info(String.format(" Added %d new tasks", tasks.size())); + log.info(String.format(" Added %,d new tasks", tasks.size())); } if (verbosity > 1) { for (SearchTask task : tasks) { @@ -419,9 +419,9 @@ public void logStackTrace(Exception e) { /** * Print choice loc * - * @param step Step number - * @param idx Choice number - * @param loc choose(.) location + * @param step Step number + * @param idx Choice number + * @param loc choose(.) location * @param choices Data choices */ public void logDataChoiceLoc(int step, int idx, String loc, List> choices) { diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/TraceLogger.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/TraceLogger.java deleted file mode 100644 index 12e026da31..0000000000 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/TraceLogger.java +++ /dev/null @@ -1,134 +0,0 @@ -package pex.runtime.logger; - -import lombok.Getter; -import lombok.Setter; -import org.apache.logging.log4j.Level; -import org.apache.logging.log4j.LogManager; -import org.apache.logging.log4j.Logger; -import org.apache.logging.log4j.core.Appender; -import org.apache.logging.log4j.core.LoggerContext; -import org.apache.logging.log4j.core.appender.ConsoleAppender; -import org.apache.logging.log4j.core.appender.OutputStreamAppender; -import org.apache.logging.log4j.core.config.Configurator; -import org.apache.logging.log4j.core.layout.PatternLayout; -import pex.runtime.machine.PMachine; -import pex.values.PMessage; - -import java.io.File; -import java.io.FileOutputStream; -import java.io.IOException; -import java.util.Date; - -/** - * Represents the trace logger that logs on every schedule step. - */ -public class TraceLogger { - static Logger log = null; - static LoggerContext context = null; - - @Getter - @Setter - static int verbosity; - - /** - * Initialize the logger - * - * @param verb Verbosity level - * @param outputFolder Output folder where trace log file resides - */ - public static void Initialize(int verb, String outputFolder) { - verbosity = verb; - log = Log4JConfig.getContext().getLogger(TraceLogger.class.getName()); - org.apache.logging.log4j.core.Logger coreLogger = - (org.apache.logging.log4j.core.Logger) LogManager.getLogger(TraceLogger.class.getName()); - context = coreLogger.getContext(); - - try { - // get new file name - Date date = new Date(); - String fileName = outputFolder + "/trace-" + date + ".log"; - File file = new File(fileName); - file.getParentFile().mkdirs(); - file.createNewFile(); - - // Define new file printer - FileOutputStream fout = new FileOutputStream(fileName, false); - - PatternLayout layout = Log4JConfig.getPatternLayout(); - Appender fileAppender = - OutputStreamAppender.createAppender(layout, null, fout, fileName, false, true); - ConsoleAppender consoleAppender = ConsoleAppender.createDefaultAppenderForLayout(layout); - fileAppender.start(); - consoleAppender.start(); - - context.getConfiguration().addLoggerAppender(coreLogger, fileAppender); - context.getConfiguration().addLoggerAppender(coreLogger, consoleAppender); - } catch (IOException e) { - System.out.println("Failed to set printer to the TraceLogger!!"); - } - } - - /** - * Disable the logger - */ - public static void disable() { - Configurator.setLevel(TraceLogger.class.getName(), Level.OFF); - } - - /** - * Enable the logger - */ - public static void enable() { - Configurator.setLevel(TraceLogger.class.getName(), Level.INFO); - } - - /** - * Log when a machine sends an event to another machine. - * - * @param message Message that is sent - */ - - public static void send(PMessage message) { - if (verbosity > 3) { - String msg = String.format("Send %s to %s", message.getEvent(), message.getTarget()); - log.info(msg); - } - } - - /** - * Log when a machine unblocks on receiving an event - * - * @param message - */ - public static void unblock(PMessage message) { - if (verbosity > 3) { - String msg = String.format("Unblock %s on receiving %s", message.getTarget(), message.getEvent()); - log.info(msg); - } - } - - /** - * Log when a machine schedules an event. - * - * @param depth Schedule depth - * @param message Message that is scheduled - * @param sender Sender machine - */ - - public static void schedule(int depth, PMessage message, PMachine sender) { - if (verbosity > 0) { - String msg = - String.format(" Depth %d: %s sent %s to %s", depth, sender, message.getEvent(), message.getTarget()); - log.info(msg); - } - } - - /** - * Log at the start of replaying a counterexample - */ - public static void logStartReplayCex() { - log.info("------------------------"); - log.info("Replaying Counterexample"); - log.info("-----------------------"); - } -} diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/SchedulerStatistics.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/SchedulerStatistics.java index 85e26a4c03..8476417944 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/SchedulerStatistics.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/SchedulerStatistics.java @@ -19,7 +19,7 @@ public class SchedulerStatistics { /** * Total steps */ - public int totalSteps = 0; + public long totalSteps = 0; /** * Total number of states visited diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/StepState.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/StepState.java index e2a8b7810d..4f021cd9ea 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/StepState.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/StepState.java @@ -5,7 +5,6 @@ import pex.runtime.machine.MachineLocalState; import pex.runtime.machine.PMachine; import pex.runtime.scheduler.Scheduler; -import pex.runtime.scheduler.replay.ReplayScheduler; import pex.utils.exceptions.TooManyChoicesException; import java.io.Serializable; diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/replay/ReplayScheduler.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/replay/ReplayScheduler.java index 6feda3a536..dd4a66461c 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/replay/ReplayScheduler.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/replay/ReplayScheduler.java @@ -19,6 +19,7 @@ public class ReplayScheduler extends Scheduler { @Getter BugFoundException bugFoundException = null; + public ReplayScheduler(Schedule sch, BugFoundException e) { super(0, sch); bugFoundException = e; diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/TooManyChoicesException.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/TooManyChoicesException.java index 22f7cd9d80..c2ba4b4522 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/TooManyChoicesException.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/TooManyChoicesException.java @@ -6,6 +6,7 @@ public class TooManyChoicesException extends BugFoundException { @Getter String loc = ""; + /** * Constructs a new TooManyChoicesException for choose(.) with too choices in a single call. *