Differences

This shows you the differences between two versions of the page.

--- lab4 [2016/01/27 22:02] – franck
+++ lab4 [2017/01/30 13:56] (current) – franck
@@ Line 1: / Line 1: @@
-JPF in its basic form is a state exploring Java virtual machine (JVM) which can systematically explore all potential executions of Java code. There are many different ways to explore the executions.  For example, JPF can use different search strategies such as breadth-first search (BFS) and depth-first search (DFS). Consider a Java code that gives rise to the following state space diagram.
+~~NOTOC~~
-{{:public:statespace.png|}}
+====== LAB 4 ======
-If we run JPF with the search strategy BFS, the states are explored in the following order: s0, s1, s2, s3, s4; with DFS, the order is : s0, s1, s3, s4, s2.
+====== Listeners ======
-JPF also contains a search strategy which is called random search (RS).  The strategy will start with the initial state (s0 in our example) and follow one path of the execution until there is no next state and then it continues its search from the initial state. Two possible paths explored by RS are: s0, s2 and s0, s1, s_3.
-**Task 1.** Develop a Java app that prints output.  When checking the Java app by JPF with DFS the output should be different from the output for BFS.
+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/
-**Task 2.** Verify your program using JPF with BFS, DFS. To do that, you need to create an application properties file (.jpf file) for your Java app developed in Task 1. Configure the search property to be gov.nasa.jpf.search.heuristic.BFSHeuristic or gov.nasa.jpf.search.heuristic.DFSHeuristic.
+  * 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.
+<code java>
+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));
+        }
+    }
+}
+</code>
+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.
+<code>
+target=Constraints
+classpath=.
+cg.enumerate_random=true
+listener=gov.nasa.jpf.listener.BudgetChecker
+</code>
+In this case, no constraints are set.  As a result, JPF will run out of memory producing
+the following output
+<code>
+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
+...
+</code>
+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.
+<code>
+target=Constraints
+classpath=.
+cg.enumerate_random=true
+listener=gov.nasa.jpf.listener.BudgetChecker
+budget.max_time=1000
+</code>
+Since JPF cannot complete within one second, it stops after one second and produces the following output.
+<code>
+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
+...
+</code>
+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.
+<code>
+target=Constraints
+classpath=.
+cg.enumerate_random=true
+listener=gov.nasa.jpf.listener.BudgetChecker
+budget.max_heap=10000000
+</code>
+Note that 10000000 bits = 10000000 / (1024 * 1024) megabytes = 9.5 megabytes.  Since
+JPF needs more heap space, it stops and produces the following output.
+<code>
+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:36 PM
+====================================================== search constraint
+max heap exceeded: 10MB >= 9MB
+...
+</code>
+One can constrain JPF from checking more than 100 bytecode instructions as follows.
+We can assign any long value to the property budget.max_insn.
+<code>
+target=Constraints
+classpath=.
+cg.enumerate_random=true
+listener=gov.nasa.jpf.listener.BudgetChecker
+budget.max_insn=100
+</code>
+Since this constraint is violated, JPF produces the following output.
+<code>
+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:47 PM
+====================================================== search constraint
+max instruction count exceeded: 100
+...
+</code>
+We can also limit the number of states that JPF explores by setting the property budget.max_state.  We can assign any int value to this property.
+<code>
+target=Constraints
+classpath=.
+cg.enumerate_random=true
+listener=gov.nasa.jpf.listener.BudgetChecker
+budget.max_state=100
+</code>
+Since the statespace of this app consists of more than 100 states, JPF stops and produces the following output.
+<code>
+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:48 PM
+====================================================== search constraint
+max states exceeded: 100
+...
+</code>
+We can also constrain the depth of the search.  The corresponding property, budget.max_depth, can take any int value.
+<code>
+target=Constraints
+classpath=.
+cg.enumerate_random=true
+listener=gov.nasa.jpf.listener.BudgetChecker
+budget.max_depth=100
+</code>
+Since the depth of the search is greater than 100 for this app, JPF stops and produces the following output.
+<code>
+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:53 PM
+====================================================== search constraint
+max search depth exceeded: 100
+...
+</code>
-**Task 3.** Generate the state space diagram for BFS and DFS. To do this you need to set  the listener to StateSpaceDot.
-**Task 4.** Verify your program using RS. RS can explore several random executions and in JPF you have the freedom to set the maximum number of executions you would like RS to explore. Firstly, set your search strategy to gov.nasa.jpf.search.RandomSearch. Secondly, set the search.RandomSearch.path_limit property to be any integer larger than 0.  Compare the resulting state space diagrams.