Skip to content

Commit ad66ede

Browse files
aman-goelaman-goel
authored
[PEx] Minor updates and cleanup (#775)
* [PEx] Several updates to logging, PEx config Changes default max choices limit to 20 per call and 250 per schedule (to account for open-source protocols with monolithic transition relation modeled as single action) Adds logging support to print choose(.) location info for easy debugging TooManyChoicesException via replayer log Minor correction * [PEx] Refactoring and formatting changes * [PEx] Update cli default Change each task to 2K schedules by default
1 parent 5c8abf0 commit ad66ede

File tree

12 files changed

+118
-198
lines changed

12 files changed

+118
-198
lines changed

‎Src/PRuntimes/PExRuntime/src/main/java/pex/RuntimeExecutor.java

Lines changed: 20 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -157,29 +157,33 @@ private static void process() throws Exception {
157157
throw new Exception("MEMOUT", e);
158158
} catch (BugFoundException e) {
159159
PExGlobal.setStatus(STATUS.BUG_FOUND);
160-
PExGlobal.setResult(String.format("found cex of length %d", e.getScheduler().getStepNumber()));
160+
PExGlobal.setResult(String.format("found cex of length %,d", e.getScheduler().getStepNumber()));
161161
if (e instanceof TooManyChoicesException) {
162162
PExGlobal.setResult(PExGlobal.getResult() + " (too many choices)");
163163
}
164164
e.getScheduler().getLogger().logStackTrace(e);
165165
PExLogger.logBugFoundInfo(e.getScheduler());
166166

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

171-
ReplayScheduler replayer = new ReplayScheduler(e.getScheduler().getSchedule());
171+
ReplayScheduler replayer = new ReplayScheduler(e.getScheduler().getSchedule(), e);
172172
PExGlobal.setReplayScheduler(replayer);
173+
PExLogger.logReplayerInfo(replayer);
173174
try {
174175
replayer.run();
175176
} catch (NullPointerException | StackOverflowError | ClassCastException replayException) {
176-
PExLogger.logStackTrace((Exception) replayException);
177+
replayer.getLogger().logStackTrace((Exception) replayException);
178+
PExLogger.logTrace((Exception) replayException);
177179
throw new BugFoundException(replayException.getMessage(), replayException);
178180
} catch (BugFoundException replayException) {
179-
PExLogger.logStackTrace(replayException);
181+
replayer.getLogger().logStackTrace(replayException);
182+
PExLogger.logTrace(replayException);
180183
throw replayException;
181184
} catch (Exception replayException) {
182-
PExLogger.logStackTrace(replayException);
185+
replayer.getLogger().logStackTrace(replayException);
186+
PExLogger.logTrace(replayException);
183187
throw new Exception("Error when replaying the bug", replayException);
184188
}
185189
throw new Exception("Failed to replay bug", e);
@@ -218,25 +222,29 @@ public static void runSearch() throws Exception {
218222
private static void replaySchedule(String fileName) throws Exception {
219223
PExLogger.logInfo(String.format("... Reading buggy trace from %s", fileName));
220224

221-
ReplayScheduler replayer = new ReplayScheduler(Schedule.readFromFile(fileName));
225+
ReplayScheduler replayer = new ReplayScheduler(Schedule.readFromFile(fileName), null);
222226
PExGlobal.setReplayScheduler(replayer);
227+
PExLogger.logReplayerInfo(replayer);
223228
try {
224229
replayer.run();
225230
} catch (NullPointerException | StackOverflowError | ClassCastException replayException) {
226231
PExGlobal.setStatus(STATUS.BUG_FOUND);
227-
PExGlobal.setResult(String.format("found cex of length %d", replayer.getStepNumber()));
228-
PExLogger.logStackTrace((Exception) replayException);
232+
PExGlobal.setResult(String.format("found cex of length %,d", replayer.getStepNumber()));
233+
replayer.getLogger().logStackTrace((Exception) replayException);
234+
PExLogger.logTrace((Exception) replayException);
229235
throw new BugFoundException(replayException.getMessage(), replayException);
230236
} catch (BugFoundException replayException) {
231237
PExGlobal.setStatus(STATUS.BUG_FOUND);
232-
PExGlobal.setResult(String.format("found cex of length %d", replayer.getStepNumber()));
238+
PExGlobal.setResult(String.format("found cex of length %,d", replayer.getStepNumber()));
233239
if (replayException instanceof TooManyChoicesException) {
234240
PExGlobal.setResult(PExGlobal.getResult() + " (too many choices)");
235241
}
236-
PExLogger.logStackTrace(replayException);
242+
replayer.getLogger().logStackTrace(replayException);
243+
PExLogger.logTrace(replayException);
237244
throw replayException;
238245
} catch (Exception replayException) {
239-
PExLogger.logStackTrace(replayException);
246+
replayer.getLogger().logStackTrace(replayException);
247+
PExLogger.logTrace(replayException);
240248
throw new Exception("Error when replaying the bug", replayException);
241249
} finally {
242250
printStats();

‎Src/PRuntimes/PExRuntime/src/main/java/pex/commandline/PExConfig.java

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -71,14 +71,14 @@ public class PExConfig {
7171
ChoiceSelectorMode choiceSelectorMode = ChoiceSelectorMode.Random;
7272
// max number of schedules per search task
7373
@Setter
74-
int maxSchedulesPerTask = 500;
74+
int maxSchedulesPerTask = 2000;
7575
//max number of children search tasks
7676
@Setter
7777
int maxChildrenPerTask = 2;
7878
//max number of choices per choose(.) operation per call
7979
@Setter
80-
int maxChoicesPerStmtPerCall = 10;
80+
int maxChoicesPerStmtPerCall = 20;
8181
//max number of choices per choose(.) operation in total
8282
@Setter
83-
int maxChoicesPerStmtPerSchedule = 100;
83+
int maxChoicesPerStmtPerSchedule = 250;
8484
}

‎Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/PExGlobal.java

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -245,13 +245,13 @@ public static void updateResult() {
245245
if (numUnexplored == 0) {
246246
resultString += "correct for any depth";
247247
} else {
248-
resultString += String.format("partially correct with %d choices remaining", numUnexplored);
248+
resultString += String.format("partially correct with %,d choices remaining", numUnexplored);
249249
}
250250
} else {
251251
if (numUnexplored == 0) {
252-
resultString += String.format("correct up to step %d", getMaxSteps());
252+
resultString += String.format("correct up to step %,d", getMaxSteps());
253253
} else {
254-
resultString += String.format("partially correct up to step %d with %d choices remaining", getMaxSteps(), numUnexplored);
254+
resultString += String.format("partially correct up to step %,d with %,d choices remaining", getMaxSteps(), numUnexplored);
255255
}
256256
}
257257
result = resultString;
@@ -332,20 +332,20 @@ public static void printProgress(boolean forcePrint) {
332332
s.append(StringUtils.center(String.format("%s", runtimeHms), 11));
333333
s.append(
334334
StringUtils.center(String.format("%.1f GB", MemoryMonitor.getMemSpent() / 1024), 9));
335-
s.append(StringUtils.center(String.format("%d / %d / %d",
335+
s.append(StringUtils.center(String.format("%,d / %,d / %,d",
336336
runningTasks.size(), finishedTasks.size(), pendingTasks.size()),
337337
24));
338338

339-
s.append(StringUtils.center(String.format("%d", getTotalSchedules()), 12));
340-
s.append(StringUtils.center(String.format("%d", timelines.size()), 12));
339+
s.append(StringUtils.center(String.format("%,d", getTotalSchedules()), 12));
340+
s.append(StringUtils.center(String.format("%,d", timelines.size()), 12));
341341
// s.append(
342342
// StringUtils.center(
343343
// String.format(
344344
// "%d (%.0f %% data)", getNumUnexploredChoices(), getUnexploredDataChoicesPercent()),
345345
// 24));
346346

347347
if (config.getStateCachingMode() != StateCachingMode.None) {
348-
s.append(StringUtils.center(String.format("%d", stateCache.size()), 12));
348+
s.append(StringUtils.center(String.format("%,d", stateCache.size()), 12));
349349
}
350350

351351
System.out.print(s);
@@ -380,8 +380,8 @@ public static int getMaxSteps() {
380380
return result;
381381
}
382382

383-
public static int getTotalSteps() {
384-
int result = 0;
383+
public static long getTotalSteps() {
384+
long result = 0;
385385
for (ExplicitSearchScheduler sch : searchSchedulers.values()) {
386386
result += sch.getStats().totalSteps;
387387
}

‎Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/PExLogger.java

Lines changed: 22 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,6 @@
1313
import pex.runtime.scheduler.explicit.strategy.SearchStrategyMode;
1414
import pex.utils.monitor.MemoryMonitor;
1515

16-
import java.io.PrintWriter;
17-
import java.io.StringWriter;
18-
1916
/**
2017
* Represents the main PEx logger
2118
*/
@@ -65,7 +62,7 @@ public static void logVerbose(String message) {
6562
* @param timeSpent Time spent in seconds
6663
*/
6764
public static void logEndOfRun(long timeSpent) {
68-
if (verbosity == 0) {
65+
if (verbosity == 0 && PExGlobal.getStatus() != STATUS.BUG_FOUND) {
6966
log.info("");
7067
}
7168
log.info("--------------------");
@@ -78,16 +75,16 @@ public static void logEndOfRun(long timeSpent) {
7875
if (PExGlobal.getConfig().getSearchStrategyMode() != SearchStrategyMode.Replay) {
7976
log.info("... Search statistics:");
8077
if (PExGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) {
81-
log.info(String.format("..... Explored %d distinct states over %d timelines",
78+
log.info(String.format("..... Explored %,d distinct states over %,d timelines",
8279
PExGlobal.getStateCache().size(), PExGlobal.getTimelines().size()));
8380
}
84-
log.info(String.format("..... Explored %d distinct schedules", PExGlobal.getTotalSchedules()));
85-
log.info(String.format("..... Finished %d search tasks (%d pending)",
81+
log.info(String.format("..... Explored %,d distinct schedules", PExGlobal.getTotalSchedules()));
82+
log.info(String.format("..... Finished %,d search tasks (%,d pending)",
8683
PExGlobal.getFinishedTasks().size(), PExGlobal.getPendingTasks().size()));
87-
log.info(String.format("..... Number of steps explored: %d (min), %d (avg), %d (max).",
84+
log.info(String.format("..... Number of steps explored: %,d (min), %,d (avg), %,d (max).",
8885
PExGlobal.getMinSteps(), (PExGlobal.getTotalSteps() / PExGlobal.getTotalSchedules()), PExGlobal.getMaxSteps()));
8986
}
90-
log.info(String.format("... Elapsed %d seconds and used %.1f GB", timeSpent, MemoryMonitor.getMaxMemSpent() / 1000.0));
87+
log.info(String.format("... Elapsed %,d seconds and used %.1f GB", timeSpent, MemoryMonitor.getMaxMemSpent() / 1000.0));
9188
log.info(String.format(".. \033[0;30;47m Result: %s \033[m", PExGlobal.getResult()));
9289
log.info(". Done");
9390
}
@@ -97,12 +94,12 @@ public static void logEndOfRun(long timeSpent) {
9794
*
9895
* @param e Exception object
9996
*/
100-
public static void logStackTrace(Exception e) {
101-
StringWriter sw = new StringWriter();
102-
PrintWriter pw = new PrintWriter(sw);
103-
e.printStackTrace(pw);
104-
log.info("--------------------");
105-
log.info(sw.toString());
97+
public static void logTrace(Exception e) {
98+
// StringWriter sw = new StringWriter();
99+
// PrintWriter pw = new PrintWriter(sw);
100+
// e.printStackTrace(pw);
101+
// log.info("--------------------");
102+
log.info(String.format(".... \033[31m %s \033[0m", e));
106103
}
107104

108105
/**
@@ -112,6 +109,15 @@ public static void logStackTrace(Exception e) {
112109
*/
113110
public static void logBugFoundInfo(Scheduler sch) {
114111
log.info("--------------------");
115-
log.info(String.format("Thread %d found a bug. Details in %s", sch.getSchedulerId(), sch.getLogger().getFileName()));
112+
log.info(String.format("... Thread %d found a bug. Details in %s", sch.getSchedulerId(), sch.getLogger().getFileName()));
113+
}
114+
115+
/**
116+
* Prints replayer info
117+
*
118+
* @param sch Replay scheduler
119+
*/
120+
public static void logReplayerInfo(Scheduler sch) {
121+
log.info(String.format("... Replaying bug. Details in %s", sch.getLogger().getFileName()));
116122
}
117123
}

‎Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/SchedulerLogger.java

Lines changed: 26 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,10 @@ public class SchedulerLogger {
4444
*/
4545
public SchedulerLogger(int schId) {
4646
verbosity = PExGlobal.getConfig().getVerbosity();
47+
if (schId == 0 && verbosity == 0) {
48+
// set minimum verbosity to 1 for replay scheduler
49+
verbosity = 1;
50+
}
4751
log = Log4JConfig.getContext().getLogger(SchedulerLogger.class.getName() + schId);
4852
org.apache.logging.log4j.core.Logger coreLogger =
4953
(org.apache.logging.log4j.core.Logger) LogManager.getLogger(SchedulerLogger.class.getName() + schId);
@@ -100,7 +104,7 @@ public void logStartTask(SearchTask task) {
100104
*/
101105
public void logEndTask(SearchTask task, int numSchedules) {
102106
if (verbosity > 0) {
103-
log.info(String.format(" Finished %s after exploring %d schedules", task, numSchedules));
107+
log.info(String.format(" Finished %s after exploring %,d schedules", task, numSchedules));
104108
}
105109
}
106110

@@ -117,7 +121,7 @@ public void logNextTask(SearchTask task) {
117121

118122
public void logNewTasks(List<SearchTask> tasks) {
119123
if (verbosity > 0) {
120-
log.info(String.format(" Added %d new tasks", tasks.size()));
124+
log.info(String.format(" Added %,d new tasks", tasks.size()));
121125
}
122126
if (verbosity > 1) {
123127
for (SearchTask task : tasks) {
@@ -207,9 +211,9 @@ public void logNewScheduleChoice(List<PMachineId> choices, int step, int idx) {
207211
}
208212
}
209213

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

@@ -225,15 +229,15 @@ public void logCurrentScheduleChoice(PMachine choice, int step, int idx) {
225229
}
226230
}
227231

228-
public void logRepeatDataChoice(PValue<?> choice, int step, int idx) {
232+
public void logRepeatDataChoice(String loc, PValue<?> choice, int step, int idx) {
229233
if (verbosity > 2) {
230-
log.info(String.format(" @%d::%d %s (repeat)", step, idx, choice));
234+
log.info(String.format(" @%d::%d %s (repeat) from %s", step, idx, choice, loc));
231235
}
232236
}
233237

234-
public void logCurrentDataChoice(PValue<?> choice, int step, int idx) {
238+
public void logCurrentDataChoice(String loc, PValue<?> choice, int step, int idx) {
235239
if (verbosity > 2) {
236-
log.info(String.format(" @%d::%d %s", step, idx, choice));
240+
log.info(String.format(" @%d::%d %s from %s", step, idx, choice, loc));
237241
}
238242
}
239243

@@ -411,4 +415,18 @@ public void logStackTrace(Exception e) {
411415
log.info("--------------------");
412416
log.info(sw.toString());
413417
}
418+
419+
/**
420+
* Print choice loc
421+
*
422+
* @param step Step number
423+
* @param idx Choice number
424+
* @param loc choose(.) location
425+
* @param choices Data choices
426+
*/
427+
public void logDataChoiceLoc(int step, int idx, String loc, List<PValue<?>> choices) {
428+
if (verbosity > 0) {
429+
log.info(String.format(" @%d::%d %d new data choices from %s - %s", step, idx, choices.size(), loc, choices));
430+
}
431+
}
414432
}

0 commit comments

Comments
 (0)