Skip to content

Commit

Permalink
[PEx] Refactoring and formatting changes
Browse files Browse the repository at this point in the history
  • Loading branch information
@aman-goel
aman-goel committed Sep 9, 2024
1 parent 2aa8b5f commit e55fe1d
Show file tree
Hide file tree
Showing 9 changed files with 25 additions and 161 deletions.
6 changes: 3 additions & 3 deletions Src/PRuntimes/PExRuntime/src/main/java/pex/RuntimeExecutor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)");
}
Expand Down Expand Up @@ -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)");
}
Expand Down
18 changes: 9 additions & 9 deletions Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/PExGlobal.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -332,20 +332,20 @@ 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(
// "%d (%.0f %% data)", getNumUnexploredChoices(), getUnexploredDataChoicesPercent()),
// 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);
Expand Down Expand Up @@ -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;
}
Expand Down
13 changes: 5 additions & 8 deletions Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/PExLogger.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
*/
Expand Down Expand Up @@ -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");
}
Expand Down
10 changes: 5 additions & 5 deletions Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/SchedulerLogger.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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));
}
}

Expand All @@ -121,7 +121,7 @@ public void logNextTask(SearchTask task) {

public void logNewTasks(List<SearchTask> 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) {
Expand Down Expand Up @@ -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<PValue<?>> choices) {
Expand Down
134 changes: 0 additions & 134 deletions Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/TraceLogger.java
View file

This file was deleted.

2 changes: 1 addition & 1 deletion ...Runtimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/SchedulerStatistics.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ public class SchedulerStatistics {
/**
* Total steps
*/
public int totalSteps = 0;
public long totalSteps = 0;

/**
* Total number of states visited
Expand Down
1 change: 0 additions & 1 deletion Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/StepState.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
1 change: 1 addition & 0 deletions Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/replay/ReplayScheduler.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@
public class ReplayScheduler extends Scheduler {
@Getter
BugFoundException bugFoundException = null;

public ReplayScheduler(Schedule sch, BugFoundException e) {
super(0, sch);
bugFoundException = e;
Expand Down
1 change: 1 addition & 0 deletions Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/TooManyChoicesException.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
*
Expand Down

0 comments on commit e55fe1d

Please sign in to comment.