Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[PEx] Minor updates and cleanup #775

Merged
merged 3 commits into from
Sep 25, 2024
Merged

[PEx] Minor updates and cleanup #775

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
2aa8b5f
[PEx] Several updates to logging, PEx config
aman-goel Sep 9, 2024
e55fe1d
[PEx] Refactoring and formatting changes
aman-goel Sep 9, 2024
1e8aec7
[PEx] Update cli default
aman-goel Sep 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 20 additions & 12 deletions Src/PRuntimes/PExRuntime/src/main/java/pex/RuntimeExecutor.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -157,29 +157,33 @@ 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)");
}
e.getScheduler().getLogger().logStackTrace(e);
PExLogger.logBugFoundInfo(e.getScheduler());

String schFile = PExGlobal.getConfig().getOutputFolder() + "/" + PExGlobal.getConfig().getProjectName() + "_0_0.schedule";
PExLogger.logInfo(String.format("Writing buggy trace in %s", schFile));
PExLogger.logInfo(String.format("... Writing buggy trace in %s", schFile));
e.getScheduler().getSchedule().writeToFile(schFile);

ReplayScheduler replayer = new ReplayScheduler(e.getScheduler().getSchedule());
ReplayScheduler replayer = new ReplayScheduler(e.getScheduler().getSchedule(), e);
PExGlobal.setReplayScheduler(replayer);
PExLogger.logReplayerInfo(replayer);
try {
replayer.run();
} catch (NullPointerException | StackOverflowError | ClassCastException replayException) {
PExLogger.logStackTrace((Exception) replayException);
replayer.getLogger().logStackTrace((Exception) replayException);
PExLogger.logTrace((Exception) replayException);
throw new BugFoundException(replayException.getMessage(), replayException);
} catch (BugFoundException replayException) {
PExLogger.logStackTrace(replayException);
replayer.getLogger().logStackTrace(replayException);
PExLogger.logTrace(replayException);
throw replayException;
} catch (Exception replayException) {
PExLogger.logStackTrace(replayException);
replayer.getLogger().logStackTrace(replayException);
PExLogger.logTrace(replayException);
throw new Exception("Error when replaying the bug", replayException);
}
throw new Exception("Failed to replay bug", e);
Expand Down Expand Up @@ -218,25 +222,29 @@ public static void runSearch() throws Exception {
private static void replaySchedule(String fileName) throws Exception {
PExLogger.logInfo(String.format("... Reading buggy trace from %s", fileName));

ReplayScheduler replayer = new ReplayScheduler(Schedule.readFromFile(fileName));
ReplayScheduler replayer = new ReplayScheduler(Schedule.readFromFile(fileName), null);
PExGlobal.setReplayScheduler(replayer);
PExLogger.logReplayerInfo(replayer);
try {
replayer.run();
} catch (NullPointerException | StackOverflowError | ClassCastException replayException) {
PExGlobal.setStatus(STATUS.BUG_FOUND);
PExGlobal.setResult(String.format("found cex of length %d", replayer.getStepNumber()));
PExLogger.logStackTrace((Exception) replayException);
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)");
}
PExLogger.logStackTrace(replayException);
replayer.getLogger().logStackTrace(replayException);
PExLogger.logTrace(replayException);
throw replayException;
} catch (Exception replayException) {
PExLogger.logStackTrace(replayException);
replayer.getLogger().logStackTrace(replayException);
PExLogger.logTrace(replayException);
throw new Exception("Error when replaying the bug", replayException);
} finally {
printStats();
Expand Down
6 changes: 3 additions & 3 deletions Src/PRuntimes/PExRuntime/src/main/java/pex/commandline/PExConfig.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,14 +71,14 @@ public class PExConfig {
ChoiceSelectorMode choiceSelectorMode = ChoiceSelectorMode.Random;
// max number of schedules per search task
@Setter
int maxSchedulesPerTask = 500;
int maxSchedulesPerTask = 2000;
//max number of children search tasks
@Setter
int maxChildrenPerTask = 2;
//max number of choices per choose(.) operation per call
@Setter
int maxChoicesPerStmtPerCall = 10;
int maxChoicesPerStmtPerCall = 20;
//max number of choices per choose(.) operation in total
@Setter
int maxChoicesPerStmtPerSchedule = 100;
int maxChoicesPerStmtPerSchedule = 250;
}
18 changes: 9 additions & 9 deletions Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/PExGlobal.java
View file
Open in desktop
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
38 changes: 22 additions & 16 deletions Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/PExLogger.java
View file
Open in desktop
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 @@ -65,7 +62,7 @@ public static void logVerbose(String message) {
* @param timeSpent Time spent in seconds
*/
public static void logEndOfRun(long timeSpent) {
if (verbosity == 0) {
if (verbosity == 0 && PExGlobal.getStatus() != STATUS.BUG_FOUND) {
log.info("");
}
log.info("--------------------");
Expand All @@ -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 All @@ -97,12 +94,12 @@ public static void logEndOfRun(long timeSpent) {
*
* @param e Exception object
*/
public static void logStackTrace(Exception e) {
StringWriter sw = new StringWriter();
PrintWriter pw = new PrintWriter(sw);
e.printStackTrace(pw);
log.info("--------------------");
log.info(sw.toString());
public static void logTrace(Exception e) {
// StringWriter sw = new StringWriter();
// PrintWriter pw = new PrintWriter(sw);
// e.printStackTrace(pw);
// log.info("--------------------");
log.info(String.format(".... \033[31m %s \033[0m", e));
}

/**
Expand All @@ -112,6 +109,15 @@ public static void logStackTrace(Exception e) {
*/
public static void logBugFoundInfo(Scheduler sch) {
log.info("--------------------");
log.info(String.format("Thread %d found a bug. Details in %s", sch.getSchedulerId(), sch.getLogger().getFileName()));
log.info(String.format("... Thread %d found a bug. Details in %s", sch.getSchedulerId(), sch.getLogger().getFileName()));
}

/**
* Prints replayer info
*
* @param sch Replay scheduler
*/
public static void logReplayerInfo(Scheduler sch) {
log.info(String.format("... Replaying bug. Details in %s", sch.getLogger().getFileName()));
}
}
34 changes: 26 additions & 8 deletions Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/SchedulerLogger.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,10 @@ public class SchedulerLogger {
*/
public SchedulerLogger(int schId) {
verbosity = PExGlobal.getConfig().getVerbosity();
if (schId == 0 && verbosity == 0) {
// set minimum verbosity to 1 for replay scheduler
verbosity = 1;
}
log = Log4JConfig.getContext().getLogger(SchedulerLogger.class.getName() + schId);
org.apache.logging.log4j.core.Logger coreLogger =
(org.apache.logging.log4j.core.Logger) LogManager.getLogger(SchedulerLogger.class.getName() + schId);
Expand Down Expand Up @@ -100,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 @@ -117,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 @@ -207,9 +211,9 @@ public void logNewScheduleChoice(List<PMachineId> choices, int step, int idx) {
}
}

public void logNewDataChoice(List<PValue<?>> choices, int step, int idx) {
public void logNewDataChoice(String loc, List<PValue<?>> choices, int step, int idx) {
if (verbosity > 1) {
log.info(String.format(" @%d::%d new data choice: %s", step, idx, choices));
log.info(String.format(" @%d::%d %d new data choices from %s - %s", step, idx, choices.size(), loc, choices));
}
}

Expand All @@ -225,15 +229,15 @@ public void logCurrentScheduleChoice(PMachine choice, int step, int idx) {
}
}

public void logRepeatDataChoice(PValue<?> choice, int step, int idx) {
public void logRepeatDataChoice(String loc, PValue<?> choice, int step, int idx) {
if (verbosity > 2) {
log.info(String.format(" @%d::%d %s (repeat)", step, idx, choice));
log.info(String.format(" @%d::%d %s (repeat) from %s", step, idx, choice, loc));
}
}

public void logCurrentDataChoice(PValue<?> choice, int step, int idx) {
public void logCurrentDataChoice(String loc, PValue<?> choice, int step, int idx) {
if (verbosity > 2) {
log.info(String.format(" @%d::%d %s", step, idx, choice));
log.info(String.format(" @%d::%d %s from %s", step, idx, choice, loc));
}
}

Expand Down Expand Up @@ -411,4 +415,18 @@ public void logStackTrace(Exception e) {
log.info("--------------------");
log.info(sw.toString());
}

/**
* Print choice loc
*
* @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) {
if (verbosity > 0) {
log.info(String.format(" @%d::%d %d new data choices from %s - %s", step, idx, choices.size(), loc, choices));
}
}
}
Loading
Loading