Lab test for EECS 4315
Question
Consider the following Java application.
package example;
public class Main {
private static int count = 0;
private static int dummy = 0;
public static void main(String[] args) {
count = count + 2;
count = count + 1;
}
}
You will develop a listener, named StaticIntFieldListener, which is part of the package listener, in several steps. Try to complete as many steps as possible within the given time. You may "skip" steps. For example, if you cannot solve step 2, you are encouraged to try step 3. Remember though that not only correctness but also design and style will be considered when evaluating your work.
Step 1
Create a listener, named listener.StaticIntFieldListener, that prints all the instructions manipulating static fields. For the above application, it should produce output like
JavaPathfinder core system v8.0 (rev 121f36476db0a420769058fa7ce56554cb6869c7) - (C) 2005-2014 United States Government. All rights reserved.
====================================================== system under test
example.Main.main()
====================================================== search started: 4/5/22 6:25 PM
putstatic java.lang.Boolean.TRUE
putstatic java.lang.Boolean.FALSE
putstatic java.lang.Boolean.TYPE
putstatic java.lang.Short.TYPE
putstatic java.lang.Integer.TYPE
putstatic java.lang.Integer.digits
putstatic java.lang.Integer.DigitTens
putstatic java.lang.Integer.DigitOnes
putstatic java.lang.Integer.sizeTable
putstatic java.lang.Long.TYPE
putstatic java.lang.Float.TYPE
putstatic java.lang.Double.TYPE
putstatic java.lang.Byte.TYPE
putstatic java.lang.String.serialPersistentFields
putstatic java.lang.String.CASE_INSENSITIVE_ORDER
putstatic java.lang.Thread$State.BLOCKED
putstatic java.lang.Thread$State.NEW
putstatic java.lang.Thread$State.RUNNABLE
putstatic java.lang.Thread$State.TERMINATED
putstatic java.lang.Thread$State.TIMED_WAITING
putstatic java.lang.Thread$State.WAITING
getstatic java.lang.Thread$State.BLOCKED
getstatic java.lang.Thread$State.NEW
getstatic java.lang.Thread$State.RUNNABLE
getstatic java.lang.Thread$State.TERMINATED
getstatic java.lang.Thread$State.TIMED_WAITING
getstatic java.lang.Thread$State.WAITING
putstatic java.lang.Thread$State.$VALUES
putstatic java.lang.System.in
putstatic java.lang.System.out
putstatic java.lang.System.err
putstatic java.util.Properties.hexDigit
putstatic java.lang.Math.$assertionsDisabled
putstatic java.lang.Math.negativeZeroFloatBits
putstatic java.lang.Math.negativeZeroDoubleBits
getstatic java.lang.Math.$assertionsDisabled
putstatic java.lang.Math.twoToTheDoubleScaleUp
getstatic java.lang.Math.$assertionsDisabled
putstatic java.lang.Math.twoToTheDoubleScaleDown
putstatic java.lang.System.properties
getstatic java.lang.System.properties
getstatic java.lang.System.properties
getstatic java.lang.System.properties
getstatic java.lang.System.properties
getstatic java.lang.System.properties
getstatic java.lang.System.properties
getstatic java.lang.System.properties
getstatic java.lang.System.properties
getstatic java.lang.System.properties
getstatic java.lang.System.properties
getstatic java.lang.System.properties
putstatic sun.misc.Unsafe.theUnsafe
putstatic sun.misc.SharedSecrets.unsafe
putstatic sun.misc.SharedSecrets.javaLangAccess
putstatic example.Main.count
putstatic example.Main.dummy
getstatic example.Main.count
putstatic example.Main.count
getstatic example.Main.count
putstatic example.Main.count
====================================================== results
no errors detected
====================================================== statistics
elapsed time: 00:00:00
states: new=1,visited=0,backtracked=1,end=1
search: maxDepth=1,constraints=0
choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
heap: new=350,released=11,maxLive=0,gcCycles=1
instructions: 3183
max memory: 240MB
loaded code: classes=61,methods=1330
====================================================== search finished: 4/5/22 6:25 PM
Step 2
Modify your listener so that it only prints the instructions manipulating static fields with type int, that is, the type of the field of the instruction is int. For the above application, it should produce output like
JavaPathfinder core system v8.0 (rev 121f36476db0a420769058fa7ce56554cb6869c7) - (C) 2005-2014 United States Government. All rights reserved.
====================================================== system under test
example.Main.main()
====================================================== search started: 4/5/22 6:31 PM
putstatic example.Main.count
putstatic example.Main.dummy
getstatic example.Main.count
putstatic example.Main.count
getstatic example.Main.count
putstatic example.Main.count
====================================================== results
no errors detected
====================================================== statistics
elapsed time: 00:00:00
states: new=1,visited=0,backtracked=1,end=1
search: maxDepth=1,constraints=0
choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
heap: new=350,released=11,maxLive=0,gcCycles=1
instructions: 3183
max memory: 240MB
loaded code: classes=61,methods=1330
====================================================== search finished: 4/5/22 6:31 PM
Step 3
Modify your listener so that it only prints the instructions manipulating static fields with type int whose fully qualified name (packageName.className.fieldName) matches the value of the property field.name set in the application properties file. For the application properties file
target = example.Main
listener = listener.StaticIntFieldListener
field.name = example.Main.count
classpath = ...
native_classpath = ...
and the above application, it should produce output like
JavaPathfinder core system v8.0 (rev 121f36476db0a420769058fa7ce56554cb6869c7) - (C) 2005-2014 United States Government. All rights reserved.
====================================================== system under test
example.Main.main()
====================================================== search started: 4/5/22 6:37 PM
putstatic example.Main.count
getstatic example.Main.count
putstatic example.Main.count
getstatic example.Main.count
putstatic example.Main.count
====================================================== results
no errors detected
====================================================== statistics
elapsed time: 00:00:00
states: new=1,visited=0,backtracked=1,end=1
search: maxDepth=1,constraints=0
choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
heap: new=350,released=11,maxLive=0,gcCycles=1
instructions: 3185
max memory: 240MB
loaded code: classes=61,methods=1330
====================================================== search finished: 4/5/22 6:37 PM
Step 4
Modify your listener so that it only prints information (see sample below for details) about all the instructions manipulating static fields with type int whose fully qualified name (packageName.className.fieldName) matches the value of the property field.name set in the application properties file. For the above application properties file and application, it should produce output like
JavaPathfinder core system v8.0 (rev 121f36476db0a420769058fa7ce56554cb6869c7) - (C) 2005-2014 United States Government. All rights reserved.
====================================================== system under test
example.Main.main()
====================================================== search started: 4/5/22 8:36 PM
The value of the static int field example.Main.count is 0
The value of the static int field example.Main.count is 0
The value of the static int field example.Main.count is 2
The value of the static int field example.Main.count is 2
The value of the static int field example.Main.count is 3
====================================================== results
no errors detected
====================================================== statistics
elapsed time: 00:00:00
states: new=1,visited=0,backtracked=1,end=1
search: maxDepth=1,constraints=0
choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
heap: new=350,released=11,maxLive=0,gcCycles=1
instructions: 3185
max memory: 240MB
loaded code: classes=61,methods=1330
====================================================== search finished: 4/5/22 8:36 PM
Solution
package listener;
import gov.nasa.jpf.Config;
import gov.nasa.jpf.ListenerAdapter;
import gov.nasa.jpf.vm.FieldInfo;
import gov.nasa.jpf.vm.Instruction;
import gov.nasa.jpf.vm.ThreadInfo;
import gov.nasa.jpf.vm.VM;
import gov.nasa.jpf.vm.bytecode.StaticFieldInstruction;
/**
* Prints the name and value of all the instructions manipulating static fields with type int
* whose fully qualified name matches the value of the property field.name set in the
* application properties file.
*
* @author Franck van Breugel
*/
public class StaticIntFieldListener extends ListenerAdapter {
private String name; // name of the field
/**
* Initializes this listener.
*
* @param config JPF's configuration
*/
public StaticIntFieldListener(Config config) {
this.name = config.getString("field.name");
}
/**
* Prints the name and value of the just executed instruction if it manipulates a static
* field with type int whose fully qualified name matches the value of the property
* field.name set in the application properties file.
*
* @param vm JPF's virtual machine
* @param currentThread the thread currently executing
* @param nextInstruction the next instruction to be executed
* @param executedInstruction the instruction just executed
*/
public void instructionExecuted(VM vm, ThreadInfo currentThread, Instruction nextInstruction, Instruction executedInstruction) {
if (executedInstruction instanceof StaticFieldInstruction) {
StaticFieldInstruction instruction = (StaticFieldInstruction) executedInstruction;
FieldInfo field = instruction.getFieldInfo();
String type = field.getType();
String name = instruction.getClassName() + "." + instruction.getFieldName();
if (this.name.equals(name) && type.equals("int")) {
long value = instruction.getLastValue();
System.out.println("The value of the static int field " + name + " is " + value);
}
}
}
}