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

Backtracker Stack Output #1

Open
wants to merge 1 commit into
base: parallel-search
Choose a base branch
from
Open

Backtracker Stack Output #1

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
230 changes: 115 additions & 115 deletions src/main/gov/nasa/jpf/listener/ExecTracker.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,51 +89,51 @@ public ExecTracker (Config config) {

@Override
public void stateRestored(Search search) {
int id = search.getStateId();
out.println("----------------------------------- [" +
search.getDepth() + "] restored: " + id);
// int id = search.getStateId();
// out.println("----------------------------------- [" +
// search.getDepth() + "] restored: " + id);
}

//--- the ones we are interested in
@Override
public void searchStarted(Search search) {
out.println("----------------------------------- search started");
if (skipInit) {
ThreadInfo tiCurrent = ThreadInfo.getCurrentThread();
miMain = tiCurrent.getEntryMethod();
out.println(" [skipping static init instructions]");
}
// if (skipInit) {
// ThreadInfo tiCurrent = ThreadInfo.getCurrentThread();
// miMain = tiCurrent.getEntryMethod();
//
// out.println(" [skipping static init instructions]");
// }
}

@Override
public void stateAdvanced(Search search) {
int id = search.getStateId();
out.print("----------------------------------- [" +
search.getDepth() + "] forward: " + id);
if (search.isNewState()) {
out.print(" new");
} else {
out.print(" visited");
}
if (search.isEndState()) {
out.print(" end");
}
out.println();
lastLine = null; // in case we report by source line
lastMi = null;
linePrefix = null;
// int id = search.getStateId();
//
// out.print("----------------------------------- [" +
// search.getDepth() + "] forward: " + id);
// if (search.isNewState()) {
// out.print(" new");
// } else {
// out.print(" visited");
// }
//
// if (search.isEndState()) {
// out.print(" end");
// }
//
// out.println();
//
// lastLine = null; // in case we report by source line
// lastMi = null;
// linePrefix = null;
}

@Override
public void stateProcessed (Search search) {
int id = search.getStateId();
out.println("----------------------------------- [" +
search.getDepth() + "] done: " + id);
// int id = search.getStateId();
// out.println("----------------------------------- [" +
// search.getDepth() + "] done: " + id);
}

@Override
Expand All @@ -156,90 +156,90 @@ public void searchFinished(Search search) {

@Override
public void gcEnd(VM vm) {
out.println("\t\t # garbage collection");
// out.println("\t\t # garbage collection");
}

//--- the ones we are interested in
@Override
public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
if (skip) {
MethodInfo mi = executedInsn.getMethodInfo();
if (mi == miMain) {
skip = false; // start recording
} else {
return; // skip
}
}

int nNoSrc = 0;
if (linePrefix == null) {
linePrefix = Integer.toString( ti.getId()) + " : ";
}
// that's pretty redundant to what is done in the ConsolePublisher, but we don't want
// presentation functionality in Step anymore
if (printSrc) {
String line = executedInsn.getSourceLine();
if (line != null){
if (nNoSrc > 0) {
out.println(" [" + nNoSrc + " insn w/o sources]");
}

if (!line.equals(lastLine)) {
out.print(" [");
out.print(executedInsn.getFileLocation());
out.print("] : ");
out.println(line.trim());
}
nNoSrc = 0;
} else { // no source
nNoSrc++;
}
lastLine = line;
}
if (printInsn) {
if (printMth) {
MethodInfo mi = executedInsn.getMethodInfo();
if (mi != lastMi){
ClassInfo mci = mi.getClassInfo();
out.print(" ");
if (mci != null) {
out.print(mci.getName());
out.print(".");
}
out.println(mi.getUniqueName());
lastMi = mi;
}
}
out.print( linePrefix);
out.printf("[%04x] ", executedInsn.getPosition());
out.println( executedInsn.toPostExecString());
}
//
// if (skip) {
// MethodInfo mi = executedInsn.getMethodInfo();
// if (mi == miMain) {
// skip = false; // start recording
// } else {
// return; // skip
// }
// }
//
// int nNoSrc = 0;
//
// if (linePrefix == null) {
// linePrefix = Integer.toString( ti.getId()) + " : ";
// }
//
// // that's pretty redundant to what is done in the ConsolePublisher, but we don't want
// // presentation functionality in Step anymore
// if (printSrc) {
// String line = executedInsn.getSourceLine();
// if (line != null){
// if (nNoSrc > 0) {
// out.println(" [" + nNoSrc + " insn w/o sources]");
// }
//
// if (!line.equals(lastLine)) {
// out.print(" [");
// out.print(executedInsn.getFileLocation());
// out.print("] : ");
// out.println(line.trim());
// }
//
// nNoSrc = 0;
//
// } else { // no source
// nNoSrc++;
// }
//
// lastLine = line;
// }
//
// if (printInsn) {
// if (printMth) {
// MethodInfo mi = executedInsn.getMethodInfo();
// if (mi != lastMi){
// ClassInfo mci = mi.getClassInfo();
// out.print(" ");
// if (mci != null) {
// out.print(mci.getName());
// out.print(".");
// }
// out.println(mi.getUniqueName());
// lastMi = mi;
// }
// }
//
// out.print( linePrefix);
//
// out.printf("[%04x] ", executedInsn.getPosition());
//
// out.println( executedInsn.toPostExecString());
// }
}

@Override
public void threadStarted(VM vm, ThreadInfo ti) {
out.println( "\t\t # thread started: " + ti.getName() + " index: " + ti.getId());
// out.println( "\t\t # thread started: " + ti.getName() + " index: " + ti.getId());
}

@Override
public void threadTerminated(VM vm, ThreadInfo ti) {
out.println( "\t\t # thread terminated: " + ti.getName() + " index: " + ti.getId());
// out.println( "\t\t # thread terminated: " + ti.getName() + " index: " + ti.getId());
}

@Override
public void exceptionThrown (VM vm, ThreadInfo ti, ElementInfo ei) {
MethodInfo mi = ti.getTopFrameMethodInfo();
out.println("\t\t\t\t # exception: " + ei + " in " + mi);
// MethodInfo mi = ti.getTopFrameMethodInfo();
// out.println("\t\t\t\t # exception: " + ei + " in " + mi);
}

@Override
Expand All @@ -251,27 +251,27 @@ public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {

@Override
public void objectExposed (VM vm, ThreadInfo currentThread, ElementInfo fieldOwnerObject, ElementInfo exposedObject) {
if (showShared){
String msg = "\t\t # exposed " + exposedObject;
if (fieldOwnerObject != null){
String ownerStatus = "";
if (fieldOwnerObject.isShared()){
ownerStatus = "shared ";
} else if (fieldOwnerObject.isExposed()){
ownerStatus = "exposed ";
}
msg += " through " + ownerStatus + fieldOwnerObject;
}
out.println(msg);
}
// if (showShared){
// String msg = "\t\t # exposed " + exposedObject;
// if (fieldOwnerObject != null){
// String ownerStatus = "";
// if (fieldOwnerObject.isShared()){
// ownerStatus = "shared ";
// } else if (fieldOwnerObject.isExposed()){
// ownerStatus = "exposed ";
// }
//
// msg += " through " + ownerStatus + fieldOwnerObject;
// }
// out.println(msg);
// }
}

@Override
public void objectShared (VM vm, ThreadInfo currentThread, ElementInfo sharedObject) {
if (showShared){
out.println("\t\t # shared " + sharedObject);
}
// if (showShared){
// out.println("\t\t # shared " + sharedObject);
// }
}


Expand Down
1 change: 1 addition & 0 deletions src/main/gov/nasa/jpf/search/Search.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -949,6 +949,7 @@ protected boolean concurrentForward () {
currentError = null;

boolean ret = vm.concurrentForwardWithSystemStateClone();
//boolean ret = vm.forward();

checkPropertyViolation();
return ret;
Expand Down
15 changes: 15 additions & 0 deletions src/main/gov/nasa/jpf/vm/DefaultBacktracker.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,8 @@ protected void backtrackSystemState() {
*/
@Override
public boolean backtrack () {
printStack();

if (sstack != null) {

backtrackKernelState();
Expand All @@ -71,6 +73,19 @@ public boolean backtrack () {
return false;
}
}

private void printStack() {
StringBuilder result = new StringBuilder("Stack: ");
if (sstack == null) {
result.append("EMPTY");
} else {
for (Object obj : sstack) {
SystemState.Memento memento = (SystemState.Memento) obj;
result.append(" ").append(memento.id);
}
}
System.out.println(result);
}

/**
* Saves the state of the system.
Expand Down