# HG changeset patch # User Peter Mehlitz # Date 1429743266 25200 # Node ID 3517702bd76802e09e747ca0469f9dca27a925cc # Parent 6774e2e08d377af16d070ed6c537bf3f5ae4808d added class name to warning for ambiguous native methods (without MJI signatures) fixed VarTracker, which was utterly unaware of new instruction type hierarchy. added JVMArrayElementInstruction.get{Array/Index}Attr(ti) since listeners most likely use attrs which otherwise would have to be retrieved/cached in executeInstruction() notifications (e.g. variable name for array) fixed ReadInstruction, which somehow extended StoreInstruction diff -r 6774e2e08d37 -r 3517702bd768 src/main/gov/nasa/jpf/jvm/bytecode/ArrayLoadInstruction.java --- a/src/main/gov/nasa/jpf/jvm/bytecode/ArrayLoadInstruction.java Tue Apr 21 00:34:15 2015 -0700 +++ b/src/main/gov/nasa/jpf/jvm/bytecode/ArrayLoadInstruction.java Wed Apr 22 15:54:26 2015 -0700 @@ -41,9 +41,12 @@ arrayRef = frame.peek(1); // ..,arrayRef,idx if (arrayRef == MJIEnv.NULL) { return ti.createAndThrowException("java.lang.NullPointerException"); - } + } ElementInfo eiArray = ti.getElementInfo(arrayRef); - + + indexOperandAttr = peekIndexAttr(ti); + arrayOperandAttr = peekArrayAttr(ti); + Scheduler scheduler = ti.getScheduler(); if (scheduler.canHaveSharedArrayCG( ti, this, eiArray, index)){ // don't modify the frame before this eiArray = scheduler.updateArraySharedness(ti, eiArray, index); @@ -85,6 +88,11 @@ return ti.getTopFrame().peek(1); } + @Override + public Object peekArrayAttr (ThreadInfo ti){ + return ti.getTopFrame().getOperandAttr(1); + } + // wouldn't really be required for loads, but this is a general // ArrayInstruction API @Override @@ -92,6 +100,11 @@ return ti.getTopFrame().peek(); } + @Override + public Object peekIndexAttr (ThreadInfo ti){ + return ti.getTopFrame().getOperandAttr(); + } + protected abstract void push (StackFrame frame, ElementInfo e, int index) throws ArrayIndexOutOfBoundsExecutiveException; diff -r 6774e2e08d37 -r 3517702bd768 src/main/gov/nasa/jpf/jvm/bytecode/ArrayStoreInstruction.java --- a/src/main/gov/nasa/jpf/jvm/bytecode/ArrayStoreInstruction.java Tue Apr 21 00:34:15 2015 -0700 +++ b/src/main/gov/nasa/jpf/jvm/bytecode/ArrayStoreInstruction.java Wed Apr 22 15:54:26 2015 -0700 @@ -34,13 +34,17 @@ */ public abstract class ArrayStoreInstruction extends JVMArrayElementInstruction implements StoreInstruction, JVMInstruction { + @Override public Instruction execute (ThreadInfo ti) { StackFrame frame = ti.getModifiableTopFrame(); int idx = peekIndex(ti); int aref = peekArrayRef(ti); // need to be polymorphic, could be LongArrayStore ElementInfo eiArray = ti.getElementInfo(aref); - + + arrayOperandAttr = peekArrayAttr(ti); + indexOperandAttr = peekIndexAttr(ti); + if (!ti.isFirstStepInsn()){ // first execution, top half //--- runtime exceptions if (aref == MJIEnv.NULL) { @@ -93,6 +97,18 @@ return ti.getTopFrame().peek(1); } + // override in LongArrayStoreInstruction + @Override + public Object peekArrayAttr (ThreadInfo ti){ + return ti.getTopFrame().getOperandAttr(2); + } + + @Override + public Object peekIndexAttr (ThreadInfo ti){ + return ti.getTopFrame().getOperandAttr(1); + } + + protected abstract void popValue(StackFrame frame); protected abstract void setField (ElementInfo e, int index) diff -r 6774e2e08d37 -r 3517702bd768 src/main/gov/nasa/jpf/jvm/bytecode/JVMArrayElementInstruction.java --- a/src/main/gov/nasa/jpf/jvm/bytecode/JVMArrayElementInstruction.java Tue Apr 21 00:34:15 2015 -0700 +++ b/src/main/gov/nasa/jpf/jvm/bytecode/JVMArrayElementInstruction.java Wed Apr 22 15:54:26 2015 -0700 @@ -29,13 +29,20 @@ protected int arrayRef; protected int index; // the accessed element + + // we cache these to avoid the need for executeInstruction() listening + // if attrs are processed in instructionExecuted() + protected Object arrayOperandAttr; + protected Object indexOperandAttr; // we need this to be abstract because of the LongArrayStore insns @Override abstract public int peekIndex (ThreadInfo ti); - - abstract protected int peekArrayRef (ThreadInfo ti); - + abstract public int peekArrayRef (ThreadInfo ti); + + abstract public Object peekIndexAttr (ThreadInfo ti); + abstract public Object peekArrayAttr (ThreadInfo ti); + public boolean isReferenceArray() { return false; } @@ -62,6 +69,23 @@ } } + public Object getArrayOperandAttr (ThreadInfo ti){ + if (ti.isPreExec()) { + return peekArrayAttr(ti); + } else { + return arrayOperandAttr; + } + } + + public Object getIndexOperandAttr (ThreadInfo ti){ + if (ti.isPreExec()) { + return peekIndexAttr(ti); + } else { + return indexOperandAttr; + } + } + + @Override public ElementInfo peekArrayElementInfo (ThreadInfo ti){ int aref = getArrayRef(ti); diff -r 6774e2e08d37 -r 3517702bd768 src/main/gov/nasa/jpf/jvm/bytecode/LongArrayStoreInstruction.java --- a/src/main/gov/nasa/jpf/jvm/bytecode/LongArrayStoreInstruction.java Tue Apr 21 00:34:15 2015 -0700 +++ b/src/main/gov/nasa/jpf/jvm/bytecode/LongArrayStoreInstruction.java Wed Apr 22 15:54:26 2015 -0700 @@ -54,7 +54,18 @@ public int peekIndex(ThreadInfo ti){ return ti.getTopFrame().peek(2); } - + + @Override + public Object peekArrayAttr (ThreadInfo ti){ + return ti.getTopFrame().getOperandAttr(3); + } + + @Override + public Object peekIndexAttr (ThreadInfo ti){ + return ti.getTopFrame().getOperandAttr(2); + } + + @Override public void accept(JVMInstructionVisitor insVisitor) { insVisitor.visit(this); diff -r 6774e2e08d37 -r 3517702bd768 src/main/gov/nasa/jpf/listener/VarTracker.java --- a/src/main/gov/nasa/jpf/listener/VarTracker.java Tue Apr 21 00:34:15 2015 -0700 +++ b/src/main/gov/nasa/jpf/listener/VarTracker.java Wed Apr 22 15:54:26 2015 -0700 @@ -25,6 +25,7 @@ import gov.nasa.jpf.jvm.bytecode.JVMFieldInstruction; import gov.nasa.jpf.jvm.bytecode.GETFIELD; import gov.nasa.jpf.jvm.bytecode.GETSTATIC; +import gov.nasa.jpf.vm.bytecode.ReadInstruction; import gov.nasa.jpf.vm.bytecode.StoreInstruction; import gov.nasa.jpf.vm.bytecode.LocalVariableInstruction; import gov.nasa.jpf.report.ConsolePublisher; @@ -39,6 +40,7 @@ import gov.nasa.jpf.vm.MethodInfo; import gov.nasa.jpf.vm.StackFrame; import gov.nasa.jpf.vm.ThreadInfo; +import gov.nasa.jpf.vm.bytecode.WriteInstruction; import java.io.PrintWriter; import java.util.ArrayList; @@ -159,17 +161,14 @@ queue.clear(); } - - + // <2do> - general purpose listeners should not use types such as String for storing // attributes, there is no good way to make sure you retrieve your own attributes @Override public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { String varId; - - if ( ((((executedInsn instanceof GETFIELD) || (executedInsn instanceof GETSTATIC))) - && ((JVMFieldInstruction)executedInsn).isReferenceField()) || - (executedInsn instanceof ALOAD)) { + + if (executedInsn instanceof ALOAD) { // a little extra work - we need to keep track of variable names, because // we cannot easily retrieve them in a subsequent xASTORE, which follows // a pattern like: ..GETFIELD.. some-stack-operations .. xASTORE @@ -178,27 +177,34 @@ if (objRef != MJIEnv.NULL) { ElementInfo ei = ti.getElementInfo(objRef); if (ei.isArray()) { - varId = ((LocalVariableInstruction)executedInsn).getVariableId(); - + varId = ((LocalVariableInstruction) executedInsn).getVariableId(); + // <2do> unfortunately, we can't filter here because we don't know yet // how the array ref will be used (we would only need the attr for // subsequent xASTOREs) frame = ti.getModifiableTopFrame(); - frame.addOperandAttr( varId); + frame.addOperandAttr(varId); } } - } + + } else if ((executedInsn instanceof ReadInstruction) && ((JVMFieldInstruction)executedInsn).isReferenceField()){ + varId = ((JVMFieldInstruction)executedInsn).getFieldName(); + + StackFrame frame = ti.getModifiableTopFrame(); + frame.addOperandAttr(varId); + + // here come the changes - note that we can't update the stats right away, // because we don't know yet if the state this leads into has already been // visited, and we want to detect only var changes that lead to *new* states - // (objective is to find out why we have new states) - else if (executedInsn instanceof StoreInstruction) { + // (objective is to find out why we have new states). Note that variable + // changes do not necessarily contribute to the state hash (@FilterField) + } else if (executedInsn instanceof StoreInstruction) { if (executedInsn instanceof ArrayStoreInstruction) { // did we have a name for the array? // stack is ".. ref idx [l]value => .." // <2do> String is not a good attribute type to retrieve - StackFrame frame = ti.getTopFrame(); - String attr = frame.getOperandAttr(1, String.class); + Object attr = ((ArrayStoreInstruction)executedInsn).getArrayOperandAttr(ti); if (attr != null) { varId = attr + "[]"; } else { @@ -207,11 +213,18 @@ } else { varId = ((LocalVariableInstruction)executedInsn).getVariableId(); } - - if (isMethodRelevant(executedInsn.getMethodInfo()) && isVarRelevant(varId)) { - queue.add(new VarChange(varId)); - lastThread = ti; - } + queueIfRelevant(ti, executedInsn, varId); + + } else if (executedInsn instanceof WriteInstruction){ + varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName(); + queueIfRelevant(ti, executedInsn, varId); + } + } + + void queueIfRelevant(ThreadInfo ti, Instruction insn, String varId){ + if (isMethodRelevant(insn.getMethodInfo()) && isVarRelevant(varId)) { + queue.add(new VarChange(varId)); + lastThread = ti; } } diff -r 6774e2e08d37 -r 3517702bd768 src/main/gov/nasa/jpf/vm/NativePeer.java --- a/src/main/gov/nasa/jpf/vm/NativePeer.java Tue Apr 21 00:34:15 2015 -0700 +++ b/src/main/gov/nasa/jpf/vm/NativePeer.java Wed Apr 22 15:54:26 2015 -0700 @@ -407,7 +407,7 @@ return annotation.noOrphanWarning(); } - private static MethodInfo searchMethod (String mname, MethodInfo[] methods) { + private MethodInfo searchMethod (String mname, MethodInfo[] methods) { int idx = -1; for (int j = 0; j < methods.length; j++) { @@ -419,7 +419,7 @@ if (idx == -1) { idx = j; } else { - throw new JPFException("overloaded native method without signature: " + mname); + throw new JPFException("overloaded native method without signature: " + ci.getName() + '.' + mname); } } } diff -r 6774e2e08d37 -r 3517702bd768 src/main/gov/nasa/jpf/vm/StackFrame.java --- a/src/main/gov/nasa/jpf/vm/StackFrame.java Tue Apr 21 00:34:15 2015 -0700 +++ b/src/main/gov/nasa/jpf/vm/StackFrame.java Wed Apr 22 15:54:26 2015 -0700 @@ -499,7 +499,7 @@ assert (top >= stackBase); if ((attrs != null)){ - return ObjectList.getFirst( attrs[top], attrType); + return ObjectList.getFirst(attrs[top], attrType); } return null; } @@ -604,9 +604,9 @@ */ public T getOperandAttr (int offset, Class attrType){ int i = top-offset; - assert (i >= stackBase); + assert (i >= stackBase) : this; if (attrs != null){ - return ObjectList.getFirst( attrs[i], attrType); + return ObjectList.getFirst(attrs[i], attrType); } return null; } diff -r 6774e2e08d37 -r 3517702bd768 src/main/gov/nasa/jpf/vm/bytecode/ReadInstruction.java --- a/src/main/gov/nasa/jpf/vm/bytecode/ReadInstruction.java Tue Apr 21 00:34:15 2015 -0700 +++ b/src/main/gov/nasa/jpf/vm/bytecode/ReadInstruction.java Wed Apr 22 15:54:26 2015 -0700 @@ -19,9 +19,9 @@ package gov.nasa.jpf.vm.bytecode; /** - * common type for all xGET insns + * common type for all GETx insns * This has to be an interface since implementors have to be derived from the abstract FieldInstruction */ -public interface ReadInstruction extends ReadOrWriteInstruction, StoreInstruction { +public interface ReadInstruction extends ReadOrWriteInstruction { // nothing here yet }