This is an old revision of the document!

LAB 4

Listeners

Choose one of the following listeners (please don't all choose the first one). Write one or more sample programs to illustrate the use of the listener. Some listeners have associated properties. Illustrate their use as well. Describe the listener and its properties. The source code of the listeners can be found in jpf-core/src/main/gov/nasa/jpf/listener/

gov.nasa.jpf.listener.CoverageAnalyzer
gov.nasa.jpf.listener.EndlessLoopDetector
gov.nasa.jpf.listener.InsnCounter
gov.nasa.jpf.listener.MethodTracker
gov.nasa.jpf.listener.NoStateCycles
gov.nasa.jpf.listener.NumericValueChecker
- range.fields=speed,..
- range.speed.field=x.y.SomeClass.velocity
- range.speed.min=300
- range.speed.max=500
- range.vars=altitude,..
- range.altitude.var=x.y.SomeClass.computeTrajectory(int):a
- range.altitude.min=125000
gov.nasa.jpf.listener.ObjectTracker
- ot.include
- ot.exclude
- ot.refs
- ot.log_calls
- ot.log_fields
gov.nasa.jpf.listener.OOMEInjector
- oome.locations
- oome.types
gov.nasa.jpf.listener.PathOutputMonitor
- perturb.fields = altitude,…
- perturb.altitude.field = x.y.MyClass.alt
- perturb.altitude.class = .perturb.IntOverUnder
- perturb.altitude.location = MyClass.java:42
- perturb.altitude.delta = 1
- perturb.returns = velocity,…
- perturb.velocity.method = x.y.MyClass.computeVelocity()
- perturb.velocity.class = .perturb.IntOverUnder
- perturb.velocity.delta = 50
- perturb.params = foo, …
- perturb.foo.method = x.y.MyClass.send(int, float, boolean)
- perturb.foo.location = MyClass.java:42
- perturb.class = .perturb.dataAbstractor
gov.nasa.jpf.listener.ReferenceLocator
- refloc.create
- refloc.release
- refloc.use
gov.nasa.jpf.listener.SearchStats
gov.nasa.jpf.listener.StackDepthChecker
- sdc.max_stack_depth
gov.nasa.jpf.listener.StackTracker
- jpf.stack_tracker.log_period
gov.nasa.jpf.listener.StateCountEstimator
- jpf.state_count_estimator.log_period
gov.nasa.jpf.listener.StateTracker
- jpf.state_tracker.log_period
gov.nasa.jpf.listener.VarRecorder
- var_recorder.include
- var_recorder.exclude
- var_recorder.fields
- var_recorder.locals
- var_recorder.arrays
gov.nasa.jpf.listener.VarTracker
- vt.include
- vt.exclude
- vt.max_vars
- vt.methods

To receive feedback, submit your work as a text file using the submit command before Tuesday January 31: submit 4315 lab4 <name of the listener>

Sample

The listener BudgetChecker, which is part of the package gov.nasa.jpf.listener, allows us to set constraints for JPF. For example, one can set the maximum number of milliseconds used by JPF. If JPF takes more time than this maximum when using this listener, JPF will terminate and will report that it took more than the set maximum. Apart from the amount time used, we can also constrain the amount of heap space used, the number of instructions executed, the depth of the search, the number of new states, and the number of non-replayed new states. To specify these constraints, the listener has several properties that can be set in the application properties file, as we will show below.

To illustrate the BudgetChecker listener, we consider the following app.

import java.util.ArrayList;
import java.util.List;
import java.util.Random;
 
public class Constraints {
    public static void main(String[] args) {
        Random random = new Random();
        List<Integer> list = new ArrayList<Integer>();
        for (int i = 0; random.nextBoolean(); i++) {
            list.add(new Integer(i));
        }
    }
}

We can run the listener BudgetChecker without setting any of its properties and, hence, not setting any constraints, as shown in the application properties file below.

target=Constraints 
classpath=.
cg.enumerate_random=true
listener=gov.nasa.jpf.listener.BudgetChecker

In this case, no constraints are set. As a result, JPF will run out of memory producing the following output

JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
Constraints.main()

====================================================== search started: 1/27/17 1:01 PM
[SEVERE] JPF out of memory
...

We can constrain the maximum amount time used by JPF to 1000 milliseconds as follows. We can assign any long value to the property budget.max_time.

target=Constraints
classpath=.
cg.enumerate_random=true
listener=gov.nasa.jpf.listener.BudgetChecker
budget.max_time=1000

Since JPF cannot complete within one second, it stops after one second and produces the following output.

JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
Constraint.main()

====================================================== search started: 1/27/17 1:22 PM

====================================================== search constraint
max time exceeded: 00:00:01 >= 00:00:01
...

The amount heap space used by JPF can be constrained to a maximum number of bits as follows. We can assign any long value to the property budget.max_heap.

target=Constraints classpath=. cg.enumerate_random=true listener=gov.nasa.jpf.listener.BudgetChecker budget.max_heap=10000000

Note that 10000000 bits = 10000000 / (1024 * 1024) megabytes = 9.5 megabytes. Since JPF needs more heap space, it stops and produces the following output.

====================================================== system under test Constraints.main()

====================================================== search started: 1/27/17 1:36 PM

====================================================== search constraint max heap exceeded: 10MB >= 9MB

One can constrain JPF from checking more than 100 bytecode instructions as follows. We can assign any int value to the property budget.max_insn.

target=Constraints classpath=. cg.enumerate_random=true listener=gov.nasa.jpf.listener.BudgetChecker budget.max_insn=100

Since this constraint is violated, JPF produces the following output.

====================================================== system under test Constraints.main()

====================================================== search started: 1/27/17 1:47 PM

====================================================== search constraint max instruction count exceeded: 100

target=Constraints classpath=. cg.enumerate_random=true listener=gov.nasa.jpf.listener.BudgetChecker budget.max_state=100

====================================================== system under test Constraints.main()

====================================================== search started: 1/27/17 1:48 PM

====================================================== search constraint max states exceeded: 100

target=Constraints classpath=. cg.enumerate_random=true listener=gov.nasa.jpf.listener.BudgetChecker budget.max_depth=100

====================================================== system under test Constraints.main()

====================================================== search started: 1/27/17 1:53 PM

====================================================== search constraint max search depth exceeded: 100

EECS4315

Table of Contents

LAB 4

Listeners

Sample