import gov.nasa.jpf.vm.bytecode.StoreInstruction;
import gov.nasa.jpf.vm.bytecode.WriteInstruction;
-import java.util.HashMap;
-import java.util.HashSet;
-import java.util.List;
+import java.util.*;
// TODO: Fix for Groovy's model-checking
// TODO: This is a listener created to detect device conflicts and global variable conflicts
private final HashSet<String> conflictSet = new HashSet<>();
private final HashSet<String> appSet = new HashSet<>();
private boolean trackLocationVar;
+ private long timeout;
+ private long startTime;
private final String SET_LOCATION_METHOD = "setLocationMode";
private final String LOCATION_VAR = "location.mode";
}
}
trackLocationVar = config.getBoolean("track_location_var_conflict", false);
+ // Timeout input from config is in minutes, so we need to convert into millis
+ timeout = config.getInt("timeout", 0) * 60 * 1000;
+ startTime = System.currentTimeMillis();
}
@Override
public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
+ // Instantiate timeoutTimer
+ if (timeout > 0) {
+ if (System.currentTimeMillis() - startTime > timeout) {
+ StringBuilder sb = new StringBuilder();
+ sb.append("Execution timeout: " + (timeout / (60 * 1000)) + " minutes have passed!");
+ Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
+ ti.setNextPC(nextIns);
+ }
+ }
// CASE #1: Detecting variable write-after-write conflict
if (executedInsn instanceof WriteInstruction) {
// Get variable info
byte type = getType(ti, executedInsn);
String value = getValue(ti, executedInsn, type);
- String writer = getWriter(ti.getStack());
+ //System.out.println("\n\n" + ti.getStackTrace() + "\n\n");
+ String writer = getWriter(ti.getStack());
// Just return if the writer is not one of the listed apps in the .jpf file
if (writer == null)
return;
}
}
}
-
+
private void checkWriteMapAndThrowError(String var, String value, String writer, ThreadInfo ti) {
-
+
if (writeMap.containsKey(var)) {
// Subsequent writes to the variable
VarChange current = writeMap.get(var);
// Conflict is declared when:
// 1) Current writer != previous writer, e.g., App1 vs. App2
// 2) Current value != previous value, e.g., "locked" vs. "unlocked"
+ if (current.value == null) {
+
+ StringBuilder sb = new StringBuilder();
+ sb.append("Conflict between apps " + current.writer + " and " + writer + ": ");
+ sb.append("Current value cannot be read (null value)... Please double check with your app output!");
+ Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
+ ti.setNextPC(nextIns);
+ }
if (!current.value.equals(value)) {
StringBuilder sb = new StringBuilder();
// Find the variable writer
// It should be one of the apps listed in the .jpf file
private String getWriter(List<StackFrame> sfList) {
-
- for(StackFrame sf : sfList) {
- MethodInfo mi = sf.getMethodInfo();
+ // Start looking from the top of the stack backward
+ for(int i=sfList.size()-1; i>=0; i--) {
+ MethodInfo mi = sfList.get(i).getMethodInfo();
if(!mi.isJPFInternal()) {
String method = mi.getStackTraceName();
// Check against the apps in the appSet
for(String app : appSet) {
+ // There is only one writer at a time but we need to always
+ // check all the potential writers in the list
if (method.contains(app)) {
return app;
}
}
}
+ private String getName(ThreadInfo ti, Instruction inst, byte type) {
+ String name;
+ int index;
+ boolean store;
+
+ if ((inst instanceof JVMLocalVariableInstruction) ||
+ (inst instanceof JVMFieldInstruction)) {
+ name = ((LocalVariableInstruction) inst).getVariableId();
+ name = name.substring(name.lastIndexOf('.') + 1);
+
+ return(name);
+ }
+
+ if (inst instanceof JVMArrayElementInstruction) {
+ store = inst instanceof StoreInstruction;
+ name = getArrayName(ti, type, store);
+ index = getArrayIndex(ti, type, store);
+ return(name + '[' + index + ']');
+ }
+
+ return(null);
+ }
+
private String getValue(ThreadInfo ti, Instruction inst, byte type) {
StackFrame frame;
int lo, hi;
return(decodeValue(type, lo, hi));
}
+ if (inst instanceof JVMArrayElementInstruction)
+ return(getArrayValue(ti, type));
+
return(null);
}
+ private String getArrayName(ThreadInfo ti, byte type, boolean store) {
+ String attr;
+ int offset;
+
+ offset = calcOffset(type, store) + 1;
+ // <2do> String is really not a good attribute type to retrieve!
+ StackFrame frame = ti.getTopFrame();
+ attr = frame.getOperandAttr( offset, String.class);
+
+ if (attr != null) {
+ return(attr);
+ }
+
+ return("?");
+ }
+
+ private int getArrayIndex(ThreadInfo ti, byte type, boolean store) {
+ int offset;
+
+ offset = calcOffset(type, store);
+
+ return(ti.getTopFrame().peek(offset));
+ }
+
+ private final static int calcOffset(byte type, boolean store) {
+ if (!store)
+ return(0);
+
+ return(Types.getTypeSize(type));
+ }
+
+ private String getArrayValue(ThreadInfo ti, byte type) {
+ StackFrame frame;
+ int lo, hi;
+
+ frame = ti.getTopFrame();
+ lo = frame.peek();
+ hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
+
+ return(decodeValue(type, lo, hi));
+ }
+
private final static String decodeValue(byte type, int lo, int hi) {
switch (type) {
case Types.T_ARRAY: return(null);
projects / jpf-core.git / blobdiff