diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/PExplicit.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/PExplicit.java index e76b4d61f..8e3f64e78 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/PExplicit.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/PExplicit.java @@ -8,7 +8,6 @@ import pexplicit.runtime.logger.PExplicitLogger; import pexplicit.runtime.logger.StatWriter; import pexplicit.runtime.machine.PTestDriver; -import pexplicit.runtime.scheduler.explicit.strategy.SearchTask; import pexplicit.utils.exceptions.BugFoundException; import pexplicit.utils.monitor.MemoryMonitor; import pexplicit.utils.monitor.TimeMonitor; @@ -35,7 +34,6 @@ public static void main(String[] args) { PExplicitGlobal.setConfig(PExplicitOptions.ParseCommandlineArgs(args)); PExplicitLogger.Initialize(PExplicitGlobal.getConfig().getVerbosity()); ComputeHash.Initialize(); - SearchTask.Initialize(); // get reflections corresponding to the model Reflections reflections = new Reflections("pexplicit.model"); diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java index 59dd6f8aa..78a73aec9 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java @@ -3,8 +3,12 @@ import pexplicit.runtime.PExplicitGlobal; import pexplicit.runtime.STATUS; import pexplicit.runtime.logger.PExplicitLogger; +import pexplicit.runtime.logger.ScratchLogger; import pexplicit.runtime.logger.StatWriter; +import pexplicit.runtime.scheduler.Schedule; import pexplicit.runtime.scheduler.explicit.ExplicitSearchScheduler; +import pexplicit.runtime.scheduler.explicit.SearchStatistics; +import pexplicit.runtime.scheduler.explicit.strategy.SearchStrategyMode; import pexplicit.runtime.scheduler.explicit.strategy.SearchTask; import pexplicit.runtime.scheduler.replay.ReplayScheduler; import pexplicit.utils.exceptions.BugFoundException; @@ -55,14 +59,22 @@ private static void runWithTimeout(long timeLimit) } private static void printStats() { - double searchTime = TimeMonitor.stopInterval(); - scheduler.recordStats(); - if (PExplicitGlobal.getResult().equals("correct for any depth")) { - PExplicitGlobal.setStatus(STATUS.VERIFIED); - } else if (PExplicitGlobal.getResult().startsWith("correct up to step")) { - PExplicitGlobal.setStatus(STATUS.VERIFIED_UPTO_MAX_STEPS); + double timeUsed = (Duration.between(TimeMonitor.getStart(), Instant.now()).toMillis() / 1000.0); + double memoryUsed = MemoryMonitor.getMemSpent(); + + StatWriter.log("time-seconds", String.format("%.1f", timeUsed)); + StatWriter.log("memory-max-MB", String.format("%.1f", MemoryMonitor.getMaxMemSpent())); + StatWriter.log("memory-current-MB", String.format("%.1f", memoryUsed)); + + if (PExplicitGlobal.getConfig().getSearchStrategyMode() != SearchStrategyMode.Replay) { + StatWriter.log("max-depth-explored", String.format("%d", SearchStatistics.maxSteps)); + scheduler.recordStats(); + if (PExplicitGlobal.getResult().equals("correct for any depth")) { + PExplicitGlobal.setStatus(STATUS.VERIFIED); + } else if (PExplicitGlobal.getResult().startsWith("correct up to step")) { + PExplicitGlobal.setStatus(STATUS.VERIFIED_UPTO_MAX_STEPS); + } } - StatWriter.log("time-search-seconds", String.format("%.1f", searchTime)); } private static void preprocess() { @@ -70,24 +82,19 @@ private static void preprocess() { PExplicitLogger.logInfo(String.format("... Checker is using '%s' strategy (seed:%s)", PExplicitGlobal.getConfig().getSearchStrategyMode(), PExplicitGlobal.getConfig().getRandomSeed())); - executor = Executors.newSingleThreadExecutor(); - PExplicitGlobal.setResult("error"); - double preSearchTime = - TimeMonitor.findInterval(TimeMonitor.getStart()); StatWriter.log("project-name", String.format("%s", PExplicitGlobal.getConfig().getProjectName())); StatWriter.log("strategy", String.format("%s", PExplicitGlobal.getConfig().getSearchStrategyMode())); StatWriter.log("time-limit-seconds", String.format("%.1f", PExplicitGlobal.getConfig().getTimeLimit())); StatWriter.log("memory-limit-MB", String.format("%.1f", PExplicitGlobal.getConfig().getMemLimit())); - StatWriter.log("time-pre-seconds", String.format("%.1f", preSearchTime)); } private static void process(boolean resume) throws Exception { + executor = Executors.newSingleThreadExecutor(); try { TimedCall timedCall = new TimedCall(scheduler, resume); future = executor.submit(timedCall); - TimeMonitor.startInterval(); runWithTimeout((long) PExplicitGlobal.getConfig().getTimeLimit()); } catch (TimeoutException e) { PExplicitGlobal.setStatus(STATUS.TIMEOUT); @@ -135,7 +142,10 @@ private static void process(boolean resume) throws Exception { } } - public static void run() throws Exception { + public static void runSearch() throws Exception { + SearchTask.Initialize(); + ScratchLogger.Initialize(); + scheduler = new ExplicitSearchScheduler(); PExplicitGlobal.setScheduler(scheduler); @@ -143,4 +153,45 @@ public static void run() throws Exception { process(false); } + private static void replaySchedule(String fileName) throws Exception { + PExplicitLogger.logInfo(String.format("... Reading buggy trace from %s", fileName)); + + ReplayScheduler replayer = new ReplayScheduler(Schedule.readFromFile(fileName)); + PExplicitGlobal.setScheduler(replayer); + try { + replayer.run(); + } catch (NullPointerException | StackOverflowError | ClassCastException replayException) { + PExplicitGlobal.setStatus(STATUS.BUG_FOUND); + PExplicitGlobal.setResult(String.format("found cex of length %d", replayer.getStepNumber())); + PExplicitLogger.logStackTrace((Exception) replayException); + throw new BugFoundException(replayException.getMessage(), replayException); + } catch (BugFoundException replayException) { + PExplicitGlobal.setStatus(STATUS.BUG_FOUND); + PExplicitGlobal.setResult(String.format("found cex of length %d", replayer.getStepNumber())); + PExplicitLogger.logStackTrace(replayException); + throw replayException; + } catch (Exception replayException) { + PExplicitLogger.logStackTrace(replayException); + throw new Exception("Error when replaying the bug", replayException); + } finally { + printStats(); + PExplicitLogger.logEndOfRun(null, Duration.between(TimeMonitor.getStart(), Instant.now()).getSeconds()); + } + } + + public static void replay() throws Exception { + preprocess(); + replaySchedule(PExplicitGlobal.getConfig().getReplayFile()); + } + + public static void run() throws Exception { + // initialize stats writer + StatWriter.Initialize(); + + if (PExplicitGlobal.getConfig().getSearchStrategyMode() == SearchStrategyMode.Replay) { + replay(); + } else { + runSearch(); + } + } } \ No newline at end of file diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitConfig.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitConfig.java index 95c45f1e2..1c4d4748d 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitConfig.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitConfig.java @@ -44,6 +44,9 @@ public class PExplicitConfig { // random seed @Setter long randomSeed = System.currentTimeMillis(); + // name of the replay file + @Setter + String replayFile = ""; // max number of logs (i.e., internal steps) within a single schedule step @Setter int maxStepLogBound = 1000; diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitOptions.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitOptions.java index 8d9a6d8b6..cacc25bae 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitOptions.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitOptions.java @@ -149,6 +149,22 @@ public class PExplicitOptions { .build(); addOption(randomSeed); + /* + * Replay options + */ + + // replay file + Option replayFile = + Option.builder("r") + .longOpt("replay") + .desc("Schedule file to replay") + .numberOfArgs(1) + .hasArg() + .argName("File Name (string)") + .build(); + addOption(replayFile); + + /* * Invisible/expert options @@ -339,6 +355,12 @@ public static PExplicitConfig ParseCommandlineArgs(String[] args) { option, String.format("Expected an integer value, got %s", option.getValue())); } break; + // replay options + case "r": + case "replay": + config.setReplayFile(option.getValue()); + config.setSearchStrategyMode(SearchStrategyMode.Replay); + break; // invisible expert options case "state-caching": switch (option.getValue()) { @@ -427,6 +449,15 @@ public static PExplicitConfig ParseCommandlineArgs(String[] args) { config.setMaxSchedulesPerTask(0); } + if (config.getSearchStrategyMode() == SearchStrategyMode.Replay) { + if (config.getVerbosity() == 0) { + config.setVerbosity(1); + } + if (config.getReplayFile().startsWith(config.getOutputFolder())) { + config.setOutputFolder(config.getOutputFolder() + "Replay"); + } + } + return config; } diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/PExplicitLogger.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/PExplicitLogger.java index d0a35d13d..0496cd5b5 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/PExplicitLogger.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/PExplicitLogger.java @@ -58,10 +58,6 @@ public static void Initialize(int verb) { consoleAppender.start(); context.getConfiguration().addLoggerAppender(coreLogger, consoleAppender); - - // initialize all loggers and writers - StatWriter.Initialize(); - ScratchLogger.Initialize(); } public static void logInfo(String message) { @@ -96,15 +92,17 @@ public static void logEndOfRun(ExplicitSearchScheduler scheduler, long timeSpent } else { log.info("..... Found 0 bugs."); } - log.info("... Scheduling statistics:"); - if (PExplicitGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) { - log.info(String.format("..... Explored %d distinct states", SearchStatistics.totalDistinctStates)); + if (scheduler != null) { + log.info("... Scheduling statistics:"); + if (PExplicitGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) { + log.info(String.format("..... Explored %d distinct states", SearchStatistics.totalDistinctStates)); + } + log.info(String.format("..... Explored %d distinct schedules", SearchStatistics.iteration)); + log.info(String.format("..... Finished %d search tasks (%d pending)", + scheduler.getSearchStrategy().getFinishedTasks().size(), scheduler.getSearchStrategy().getPendingTasks().size())); + log.info(String.format("..... Number of steps explored: %d (min), %d (avg), %d (max).", + SearchStatistics.minSteps, (SearchStatistics.totalSteps / SearchStatistics.iteration), SearchStatistics.maxSteps)); } - log.info(String.format("..... Explored %d distinct schedules", SearchStatistics.iteration)); - log.info(String.format("..... Finished %d search tasks (%d pending)", - scheduler.getSearchStrategy().getFinishedTasks().size(), scheduler.getSearchStrategy().getPendingTasks().size())); - log.info(String.format("..... Number of steps explored: %d (min), %d (avg), %d (max).", - SearchStatistics.minSteps, (SearchStatistics.totalSteps / SearchStatistics.iteration), SearchStatistics.maxSteps)); log.info(String.format("... Elapsed %d seconds and used %.1f GB", timeSpent, MemoryMonitor.getMaxMemSpent() / 1000.0)); log.info(String.format(".. Result: " + PExplicitGlobal.getResult())); log.info(". Done"); @@ -172,7 +170,7 @@ public static void logNewTasks(List tasks) { * Log when serializing a schedule * * @param schedule Schedule to serialize - * @param szBytes Bytes written + * @param szBytes Bytes written */ public static void logSerializeSchedule(Schedule schedule, String fileName, long szBytes) { if (verbosity > 1) { diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java index e884c892c..f790525db 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java @@ -3,7 +3,6 @@ import lombok.Getter; import lombok.Setter; import pexplicit.runtime.PExplicitGlobal; -import pexplicit.runtime.logger.PExplicitLogger; import pexplicit.runtime.machine.PMachineId; import pexplicit.runtime.scheduler.choice.Choice; import pexplicit.runtime.scheduler.choice.DataChoice; @@ -12,12 +11,7 @@ import pexplicit.runtime.scheduler.explicit.StepState; import pexplicit.values.PValue; -import java.io.FileOutputStream; -import java.io.IOException; -import java.io.ObjectOutputStream; -import java.io.Serializable; -import java.nio.file.Files; -import java.nio.file.Paths; +import java.io.*; import java.util.ArrayList; import java.util.List; @@ -45,6 +39,22 @@ public class Schedule implements Serializable { public Schedule() { } + public static Schedule readFromFile(String fileName) { + assert (fileName != null); + Schedule result = null; + + try { + FileInputStream fis; + fis = new FileInputStream(fileName); + ObjectInputStream ois = new ObjectInputStream(fis); + result = (Schedule) ois.readObject(); + } catch (IOException | ClassNotFoundException e) { + throw new RuntimeException("Failed to read schedule from file " + fileName, e); + } + + return result; + } + /** * Get the choice at a choice depth * diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java index a305f1534..348983455 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java @@ -22,7 +22,6 @@ import pexplicit.values.ComputeHash; import pexplicit.values.PValue; -import java.time.Duration; import java.time.Instant; import java.util.*; import java.util.concurrent.TimeUnit; @@ -597,22 +596,15 @@ public void updateResult() { } public void recordStats() { - double timeUsed = (Duration.between(TimeMonitor.getStart(), Instant.now()).toMillis() / 1000.0); - double memoryUsed = MemoryMonitor.getMemSpent(); - printProgress(true); // print basic statistics - StatWriter.log("time-seconds", String.format("%.1f", timeUsed)); - StatWriter.log("memory-max-MB", String.format("%.1f", MemoryMonitor.getMaxMemSpent())); - StatWriter.log("memory-current-MB", String.format("%.1f", memoryUsed)); StatWriter.log("#-executions", String.format("%d", SearchStatistics.iteration)); if (PExplicitGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) { StatWriter.log("#-states", String.format("%d", SearchStatistics.totalStates)); StatWriter.log("#-distinct-states", String.format("%d", SearchStatistics.totalDistinctStates)); } StatWriter.log("steps-min", String.format("%d", SearchStatistics.minSteps)); - StatWriter.log("max-depth-explored", String.format("%d", SearchStatistics.maxSteps)); StatWriter.log("steps-avg", String.format("%d", SearchStatistics.totalSteps / SearchStatistics.iteration)); StatWriter.log("#-choices-unexplored", String.format("%d", getNumUnexploredChoices())); StatWriter.log("%-choices-unexplored-data", String.format("%.1f", getUnexploredDataChoicesPercent())); diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchStrategyMode.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchStrategyMode.java index a6d97dee2..222b21361 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchStrategyMode.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchStrategyMode.java @@ -3,7 +3,8 @@ public enum SearchStrategyMode { DepthFirst("dfs"), Random("random"), - Astar("astar"); + Astar("astar"), + Replay("replay"); private String name; diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchTask.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchTask.java index b87a02884..1d81780cd 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchTask.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchTask.java @@ -43,6 +43,24 @@ public SearchTask(int id, SearchTask parentTask) { this.parentTask = parentTask; } + public static void Initialize() { + String taskPath = PExplicitGlobal.getConfig().getOutputFolder() + "/tasks/"; + try { + Files.createDirectories(Paths.get(taskPath)); + } catch (IOException e) { + throw new RuntimeException("Failed to initialize tasks at " + taskPath, e); + } + } + + public static void Cleanup() { + String taskPath = PExplicitGlobal.getConfig().getOutputFolder() + "/tasks/"; + try { + FileUtils.deleteDirectory(new File(taskPath)); + } catch (IOException e) { + throw new RuntimeException("Failed to cleanup tasks at " + taskPath, e); + } + } + public boolean isInitialTask() { return id == 0; } @@ -111,7 +129,6 @@ public List getSearchUnitKeys(boolean reversed) { return keys; } - /** * Get the number of search units in the task * @@ -211,7 +228,6 @@ public int getCurrentNumUnexploredDataChoices() { return numUnexplored; } - /** * Clear search unit at a choice depth * @@ -221,24 +237,6 @@ public void clearSearchUnit(int choiceNum) { searchUnits.remove(choiceNum); } - public static void Initialize() { - String taskPath = PExplicitGlobal.getConfig().getOutputFolder() + "/tasks/"; - try { - Files.createDirectories(Paths.get(taskPath)); - } catch (IOException e) { - throw new RuntimeException("Failed to initialize tasks at " + taskPath, e); - } - } - - public static void Cleanup() { - String taskPath = PExplicitGlobal.getConfig().getOutputFolder() + "/tasks/"; - try { - FileUtils.deleteDirectory(new File(taskPath)); - } catch (IOException e) { - throw new RuntimeException("Failed to cleanup tasks at " + taskPath, e); - } - } - public void writeToFile() { assert (serializeFile == null); assert (prefixChoices != null);