Lab test for EECS 4315

Question

Consider the following Java application. 
import java.util.ArrayList;
import java.util.List;

public class Main {
    public static void main(String[] args) {
	List list = new ArrayList();
	list.add(1);
        System.out.println("In the middle");
	list.add(null);
	list.set(0, list.get(1));
    }
}
You will develop a listener, named NullArgumentListener, 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.NullArgumentListener, that prints the name of all the methods that are invoked. 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
Main.main()

====================================================== search started: 4/4/22 1:10 PM
java.lang.Boolean.
java.lang.Boolean.
java.lang.Object.
java.lang.Boolean.
java.lang.Object.
java.lang.Class.getPrimitiveClass
java.lang.Character.
java.lang.Short.
java.lang.Class.getPrimitiveClass
java.lang.Integer.
java.lang.Class.getPrimitiveClass
java.lang.Long.
java.lang.Class.getPrimitiveClass
java.lang.Float.
java.lang.Class.getPrimitiveClass
java.lang.Double.
java.lang.Class.getPrimitiveClass
java.lang.Byte.
java.lang.Class.getPrimitiveClass
java.lang.String.
java.lang.String$CaseInsensitiveComparator.
java.lang.String$CaseInsensitiveComparator.
java.lang.Object.
java.lang.Thread$State.
java.lang.Thread$State.
java.lang.Enum.
java.lang.Object.
java.lang.Thread$State.
java.lang.Enum.
java.lang.Object.
java.lang.Thread$State.
java.lang.Enum.
java.lang.Object.
java.lang.Thread$State.
java.lang.Enum.
java.lang.Object.
java.lang.Thread$State.
java.lang.Enum.
java.lang.Object.
java.lang.Thread$State.
java.lang.Enum.
java.lang.Object.
java.lang.System.
java.lang.System$1.
java.io.InputStream.
java.lang.Object.
java.lang.System.createSystemOut
java.lang.System.createSystemErr
java.util.Properties.
java.util.Properties.
java.util.Properties.
java.util.Hashtable.
java.util.Hashtable.
java.util.Dictionary.
java.lang.Object.
java.lang.Float.isNaN
java.lang.Math.
java.lang.Class.desiredAssertionStatus
java.lang.Float.floatToRawIntBits
java.lang.Double.doubleToRawLongBits
java.lang.Math.powerOfTwoD
java.lang.Double.longBitsToDouble
java.lang.Math.powerOfTwoD
java.lang.Double.longBitsToDouble
java.lang.Math.min
java.lang.System.getKeyValuePairs
java.util.Hashtable.put
java.lang.String.hashCode
java.util.Hashtable.addEntry
java.util.Hashtable$Entry.
java.lang.Object.
java.util.Hashtable.put
java.lang.String.hashCode
java.util.Hashtable.addEntry
java.util.Hashtable$Entry.
java.lang.Object.
java.util.Hashtable.put
java.lang.String.hashCode
java.util.Hashtable.addEntry
java.util.Hashtable$Entry.
java.lang.Object.
java.util.Hashtable.put
java.lang.String.hashCode
java.util.Hashtable.addEntry
java.util.Hashtable$Entry.
java.lang.Object.
java.util.Hashtable.put
java.lang.String.hashCode
java.util.Hashtable.addEntry
java.util.Hashtable$Entry.
java.lang.Object.
java.util.Hashtable.put
java.lang.String.hashCode
java.util.Hashtable.addEntry
java.util.Hashtable$Entry.
java.lang.Object.
java.util.Hashtable.put
java.lang.String.hashCode
java.util.Hashtable.addEntry
java.util.Hashtable$Entry.
java.lang.Object.
java.util.Hashtable.put
java.lang.String.hashCode
java.util.Hashtable.addEntry
java.util.Hashtable$Entry.
java.lang.Object.
java.util.Hashtable.put
java.lang.String.hashCode
java.util.Hashtable.addEntry
java.util.Hashtable.rehash
java.lang.Math.min
java.lang.String.hashCode
java.util.Hashtable$Entry.
java.lang.Object.
java.util.Hashtable.put
java.lang.String.hashCode
java.util.Hashtable.addEntry
java.util.Hashtable$Entry.
java.lang.Object.
java.util.Hashtable.put
java.lang.String.hashCode
java.util.Hashtable.addEntry
java.util.Hashtable$Entry.
java.lang.Object.
java.lang.System.createJavaLangAccess
java.lang.System$2.
java.lang.Object.
sun.misc.SharedSecrets.
sun.misc.Unsafe.
sun.misc.Unsafe.
java.lang.Object.
sun.misc.Unsafe.getUnsafe
sun.misc.SharedSecrets.setJavaLangAccess
Main.main
java.util.ArrayList.
java.util.ArrayList.
java.util.AbstractList.
java.util.AbstractCollection.
java.lang.Object.
java.lang.Integer.valueOf
java.util.ArrayList.add
java.util.ArrayList.ensureCapacityInternal
java.util.ArrayList.calculateCapacity
java.lang.Math.max
java.util.ArrayList.ensureExplicitCapacity
java.util.ArrayList.grow
java.util.Arrays.
java.lang.Class.desiredAssertionStatus
java.util.Arrays.copyOf
java.lang.Object.getClass
java.util.Arrays.copyOf
java.lang.Math.min
java.lang.System.arraycopy
gov.nasa.jpf.ConsoleOutputStream.println
In the middle
java.util.ArrayList.add
java.util.ArrayList.ensureCapacityInternal
java.util.ArrayList.calculateCapacity
java.util.ArrayList.ensureExplicitCapacity
java.util.ArrayList.get
java.util.ArrayList.rangeCheck
java.util.ArrayList.elementData
java.util.ArrayList.set
java.util.ArrayList.rangeCheck
java.util.ArrayList.elementData

====================================================== 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=643,released=13,maxLive=0,gcCycles=1
instructions:       3429
max memory:         57MB
loaded code:        classes=69,methods=1645

====================================================== search finished: 4/4/22 1:10 PM

Step 2

Modify your listener so that it only prints the name of all the methods that are invoked within the main method. 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
Main.main()

====================================================== search started: 4/4/22 1:09 PM
Main.main
java.util.ArrayList.
java.util.ArrayList.
java.util.AbstractList.
java.util.AbstractCollection.
java.lang.Object.
java.lang.Integer.valueOf
java.util.ArrayList.add
java.util.ArrayList.ensureCapacityInternal
java.util.ArrayList.calculateCapacity
java.lang.Math.max
java.util.ArrayList.ensureExplicitCapacity
java.util.ArrayList.grow
java.util.Arrays.
java.lang.Class.desiredAssertionStatus
java.util.Arrays.copyOf
java.lang.Object.getClass
java.util.Arrays.copyOf
java.lang.Math.min
java.lang.System.arraycopy
gov.nasa.jpf.ConsoleOutputStream.println
In the middle
java.util.ArrayList.add
java.util.ArrayList.ensureCapacityInternal
java.util.ArrayList.calculateCapacity
java.util.ArrayList.ensureExplicitCapacity
java.util.ArrayList.get
java.util.ArrayList.rangeCheck
java.util.ArrayList.elementData
java.util.ArrayList.set
java.util.ArrayList.rangeCheck
java.util.ArrayList.elementData

====================================================== 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=643,released=13,maxLive=0,gcCycles=1
instructions:       3429
max memory:         57MB
loaded code:        classes=69,methods=1645

====================================================== search finished: 4/4/22 1:09 PM

Step 3

Modify your listener so that it only prints the name of all the methods that are invoked within the main method after all output produced by the application. 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
Main.main()

====================================================== search started: 4/4/22 1:14 PM
In the middle
Main.main
java.util.ArrayList.
java.util.ArrayList.
java.util.AbstractList.
java.util.AbstractCollection.
java.lang.Object.
java.lang.Integer.valueOf
java.util.ArrayList.add
java.util.ArrayList.ensureCapacityInternal
java.util.ArrayList.calculateCapacity
java.lang.Math.max
java.util.ArrayList.ensureExplicitCapacity
java.util.ArrayList.grow
java.util.Arrays.
java.lang.Class.desiredAssertionStatus
java.util.Arrays.copyOf
java.lang.Object.getClass
java.util.Arrays.copyOf
java.lang.Math.min
java.lang.System.arraycopy
gov.nasa.jpf.ConsoleOutputStream.println
java.util.ArrayList.add
java.util.ArrayList.ensureCapacityInternal
java.util.ArrayList.calculateCapacity
java.util.ArrayList.ensureExplicitCapacity
java.util.ArrayList.get
java.util.ArrayList.rangeCheck
java.util.ArrayList.elementData
java.util.ArrayList.set
java.util.ArrayList.rangeCheck
java.util.ArrayList.elementData

====================================================== 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=643,released=13,maxLive=0,gcCycles=1
instructions:       3429
max memory:         57MB
loaded code:        classes=69,methods=1645

====================================================== search finished: 4/4/22 1:14 PM

Step 4

Modify your listener so that it only prints information (see sample below for details) about all the methods that are invoked within the main method of which at least one argument is null after all output produced by the application. 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
Main.main()

====================================================== search started: 4/4/22 1:16 PM
In the middle
Argument with index 0 of method java.util.ArrayList.add is null
Argument with index 1 of method java.util.ArrayList.set is null

====================================================== 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=643,released=13,maxLive=0,gcCycles=1
instructions:       3429
max memory:         57MB
loaded code:        classes=69,methods=1645

====================================================== search finished: 4/4/22 1:16 PM

Solution

package listener;

import gov.nasa.jpf.ListenerAdapter;
import gov.nasa.jpf.search.Search;
import gov.nasa.jpf.vm.MethodInfo;
import gov.nasa.jpf.vm.StackFrame;
import gov.nasa.jpf.vm.ThreadInfo;
import gov.nasa.jpf.vm.VM;

/**
 * Prints for each method that is invoked within the main method 
 * the arguments of that method invocation that are null.
 * 
 * @author Franck van Breugel
 */
public class NullArgumentListener extends ListenerAdapter {
  private boolean inMain; // in the main method
  private StringBuffer report; // report to be printed at the end of the search

  /**
   * Initializes this listener.
   */
  public NullArgumentListener() {
    this.inMain = false;
    this.report = new StringBuffer();
  }

  /**
   * The method method.
   */
  private static final String MAIN = "main([Ljava/lang/String;)V";

  /**
   * Checks whether the main method is entered.  If within the main method,
   * records the arguments of the method invocation that are null.
   * 
   * @param vm JPF's virtual machine
   * @param currentThread the thread currently executing
   * @param enteredMethod the method entered
   */
  public void methodEntered(VM vm, ThreadInfo currentThread, MethodInfo enteredMethod) {
    String name = enteredMethod.getFullName(); 

    if (name.endsWith(MAIN)) {
      this.inMain = true;
    }

    if (this.inMain) {
      name = enteredMethod.getBaseName();
      StackFrame frame = currentThread.getTopFrame();
      Object[] arguments = frame.getArgumentValues(currentThread);
      int index = 0;
      for (Object argument : arguments) {
        if (argument == null) {
          this.report.append(String.format("Argument with index %d of method %s is null\n", index, name));
        }
        index++;
      }
    }
  }

  /**
   * Checks whether the main method is exited.
   * 
   * @param vm JPF's virtual machine
   * @param currentThread the thread currently executing
   * @param exitedMethod the method entered
   */
  public void methodExited(VM vm, ThreadInfo currentThread, MethodInfo exitedMethod) {
    String name = exitedMethod.getFullName(); 

    if (name.endsWith(MAIN)) {
      this.inMain = false;
    }
  }

  /**
   * Prints the report.
   * 
   * @param search JPF's search
   */
  public void searchFinished(Search search) {
    System.out.print(this.report);
  }
}