From: rtrimana Date: Fri, 26 Jun 2020 22:30:12 +0000 (-0700) Subject: Adding debug mode guards for all main methods. X-Git-Url: http://demsky.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=02c81b42dfad69b9c2b36ec20650be4cd4d877f1 Adding debug mode guards for all main methods. --- diff --git a/src/main/gov/nasa/jpf/listener/ConflictTrackerOld.java b/src/main/gov/nasa/jpf/listener/ConflictTrackerOld.java index fc6b6de..528b3b4 100644 --- a/src/main/gov/nasa/jpf/listener/ConflictTrackerOld.java +++ b/src/main/gov/nasa/jpf/listener/ConflictTrackerOld.java @@ -67,18 +67,20 @@ public class ConflictTrackerOld extends ListenerAdapter { out = new PrintWriter(System.out, true); debugMode = config.getBoolean("debug_mode", false); - String[] conflictVars = config.getStringArray("variables"); - // We are not tracking anything if it is null - if (conflictVars != null) { - for (String var : conflictVars) { - conflictSet.add(var); + if (!debugMode) { + String[] conflictVars = config.getStringArray("variables"); + // We are not tracking anything if it is null + if (conflictVars != null) { + for (String var : conflictVars) { + conflictSet.add(var); + } } - } - String[] apps = config.getStringArray("apps"); - // We are not tracking anything if it is null - if (apps != null) { - for (String var : apps) { - appSet.add(var); + String[] apps = config.getStringArray("apps"); + // We are not tracking anything if it is null + if (apps != null) { + for (String var : apps) { + appSet.add(var); + } } } @@ -130,8 +132,7 @@ public class ConflictTrackerOld extends ListenerAdapter { } //Check for conflict with the appropriate update set if we are not a manual transition - //If this is debug mode, then we do not report any conflicts - if (!debugMode && confupdates != null && !u.isManual()) { + if (confupdates != null && !u.isManual()) { for(Update u2: confupdates) { if (conflicts(u, u2)) { //throw new RuntimeException(createErrorMessage(u, u2)); @@ -345,7 +346,9 @@ public class ConflictTrackerOld extends ListenerAdapter { out.println("The state is restored to state with id: "+id+", depth: "+depth); // Update the parent node - parentNode = getNode(id); + if (!debugMode) { + parentNode = getNode(id); + } } @Override @@ -386,9 +389,11 @@ public class ConflictTrackerOld extends ListenerAdapter { @Override public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator currentCG) { - if (currentCG instanceof IntChoiceFromSet) { - IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG; - currentEvent = icsCG.getNextChoice(); + if (!debugMode) { + if (currentCG instanceof IntChoiceFromSet) { + IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG; + currentEvent = icsCG.getNextChoice(); + } } } @@ -400,35 +405,37 @@ public class ConflictTrackerOld extends ListenerAdapter { depth = search.getDepth(); operation = "forward"; - // Add the node to the list of nodes - Node currentNode = getNode(id); + if (!debugMode) { + // Add the node to the list of nodes + Node currentNode = getNode(id); - // Create an edge based on the current transition - Edge newEdge = createEdge(parentNode, currentNode, transition, currentEvent); + // Create an edge based on the current transition + Edge newEdge = createEdge(parentNode, currentNode, transition, currentEvent); - // Reset the temporary variables and flags - currUpdates.clear(); - manual = false; + // Reset the temporary variables and flags + currUpdates.clear(); + manual = false; - // If we have a new Edge, check for conflicts - if (newEdge != null) - propagateChange(newEdge); + // If we have a new Edge, check for conflicts + if (newEdge != null) + propagateChange(newEdge); - if (search.isNewState()) { - detail = "new"; - } else { - detail = "visited"; - } + if (search.isNewState()) { + detail = "new"; + } else { + detail = "visited"; + } - if (search.isEndState()) { - out.println("This is the last state!"); - theEnd = "end"; - } + if (search.isEndState()) { + out.println("This is the last state!"); + theEnd = "end"; + } - out.println("The state is forwarded to state with id: "+id+", depth: "+depth+" which is "+detail+" state: "+"% "+theEnd); + out.println("The state is forwarded to state with id: "+id+", depth: "+depth+" which is "+detail+" state: "+"% "+theEnd); - // Update the parent node - parentNode = currentNode; + // Update the parent node + parentNode = currentNode; + } } @Override @@ -440,16 +447,20 @@ public class ConflictTrackerOld extends ListenerAdapter { out.println("The state is backtracked to state with id: "+id+", depth: "+depth); - // Update the parent node - parentNode = getNode(id); + if (!debugMode) { + // Update the parent node + parentNode = getNode(id); + } } @Override public void searchFinished(Search search) { out.println("----------------------------------- search finished"); - //Comment out the following line to print the explored graph - printGraph(); + if (!debugMode) { + //Comment out the following line to print the explored graph + printGraph(); + } } private String getValue(ThreadInfo ti, Instruction inst, byte type) { @@ -612,36 +623,38 @@ public class ConflictTrackerOld extends ListenerAdapter { } } - if (conflictFound) { + if (!debugMode) { + if (conflictFound) { - StringBuilder sb = new StringBuilder(); - sb.append(errorMessage); - Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString()); - ti.setNextPC(nextIns); - } else { + StringBuilder sb = new StringBuilder(); + sb.append(errorMessage); + Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString()); + ti.setNextPC(nextIns); + } else { - if (executedInsn instanceof WriteInstruction) { - String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName(); - // Check if we have an update to isManualTransaction to update manual field - if (varId.contains("isManualTransaction")) { - byte type = getType(ti, executedInsn); - String value = getValue(ti, executedInsn, type); - System.out.println(); - manual = (value.equals("true"))?true:false; - } - for (String var : conflictSet) { - if (varId.contains(var)) { - // Get variable info + if (executedInsn instanceof WriteInstruction) { + String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName(); + // Check if we have an update to isManualTransaction to update manual field + if (varId.contains("isManualTransaction")) { byte type = getType(ti, executedInsn); String value = getValue(ti, executedInsn, type); - String writer = getWriter(ti.getStack(), appSet); - - // Just return if the writer is not one of the listed apps in the .jpf file - if (writer == null) - return; - - // Update the current updates - writeWriterAndValue(writer, var, value); + System.out.println(); + manual = (value.equals("true"))?true:false; + } + for (String var : conflictSet) { + if (varId.contains(var)) { + // Get variable info + byte type = getType(ti, executedInsn); + String value = getValue(ti, executedInsn, type); + String writer = getWriter(ti.getStack(), appSet); + + // Just return if the writer is not one of the listed apps in the .jpf file + if (writer == null) + return; + + // Update the current updates + writeWriterAndValue(writer, var, value); + } } } }