Introduction
In this assignment, you need to implement a test input generation tool, similar to DART and CUTE. The details follow. Please contact Prof. Koushik Sen with any questions. The slides explaining the assignment can be found at http://srl.cs.berkeley.edu/~ksen/Assignment.ppt .
Requirement
Windows or Linux or Mac OS X. Latest version of Sun's JDK and ant (http://ant.apache.org/).
Installation
The infrastructure required to implement the tool can be downloaded from http://srl.cs.berkeley.edu/~ksen/hw1.tar.gz . Invoke the following commands to install the infrastructure.
tar zxvf hw1.tar.gz
cd hw1
ant
ant instrument-benchmarks
Description
Input: A Java program, say Testme.java. The following library functions can used to provide primitive inputs to a Java program
int edu.berkeley.cs.wise.concolic.Concolic.input.Integer()
long edu.berkeley.cs.wise.concolic.Concolic.input.Long()
short edu.berkeley.cs.wise.concolic.Concolic.input.Short()
byte edu.berkeley.cs.wise.concolic.Concolic.input.Byte()
char edu.berkeley.cs.wise.concolic.Concolic.input.Character()
boolean edu.berkeley.cs.wise.concolic.Concolic.input.Boolean()
See the Java files in the directory benchmarks/edu/berkeley/cs/wise/benchmarks/ to understand the usage of these functions. In this assignment, we will assume that inputs can only be of integral primitive types, such as int, char, long, short, byte, long.
Given a Java program, we want to generate inputs using concolic execution. The generated inputs should explore all feasible execution paths of the program. The infrastructure provides two scripts: run-jcute.sh and runall.sh. Run "ant instrument-benchmarks" to instrument all Java files under the directory benchmarks/. The instrumented classes are generated in the tmpclasses/ directory.
If we execute an instrumented Java class, it generates a file called “trace”. Try the following commands to see the trace file.
java -cp tmpclasses:classes edu.berkeley.cs.wise.benchmarks.Testme
cat trace
An execution of the instrumented executable file reads a special file “input”, if present, to initialize the inputs. If the input file is absent, then all the inputs are initialized to 0 during the execution. A complete snapshot of the above 3 commands is given below.
Koushik-Sens-MacBook-Pro:hw1 ksen$ ant instrument-benchmarks
Buildfile: /Users/ksen/hw1/build.xml
init:
build-project:
[echo] wise: /Users/ksen/hw1/build.xml
build-benchmarks:
[echo] wise: /Users/ksen/hw1/build.xml
build:
instrument-benchmarks-clean:
[delete] Deleting: /Users/ksen/hw1/iidToLine.map
[delete] Deleting: /Users/ksen/hw1/iidToLine.map.html
instrument-benchmarks:
[java] Soot started on Wed Sep 07 22:10:53 PDT 2011
[java] No main class given. Inferred 'edu.berkeley.cs.wise.benchmarks.BellmanFord' as main class.
[java] Transforming edu.berkeley.cs.wise.benchmarks.BellmanFord...
[java] Transforming edu.berkeley.cs.wise.benchmarks.BinaryTreeSearch$1...
[java] Transforming edu.berkeley.cs.wise.benchmarks.BinaryTreeSearch$BinaryTree$Node...
[java] Transforming edu.berkeley.cs.wise.benchmarks.BinaryTreeSearch$BinaryTree...
[java] Transforming edu.berkeley.cs.wise.benchmarks.BinaryTreeSearch...
[java] Transforming edu.berkeley.cs.wise.benchmarks.BuggyDijkstra...
[java] Transforming edu.berkeley.cs.wise.benchmarks.Dijkstra...
[java] Transforming edu.berkeley.cs.wise.benchmarks.HeapInsertJDK15...
[java] Transforming edu.berkeley.cs.wise.benchmarks.InsertionSort...
[java] Transforming edu.berkeley.cs.wise.benchmarks.java15.lang.Math...
[java] Transforming edu.berkeley.cs.wise.benchmarks.java15.util.AbstractCollection...
[java] Transforming edu.berkeley.cs.wise.benchmarks.java15.util.AbstractQueue...
[java] Transforming edu.berkeley.cs.wise.benchmarks.java15.util.Arrays...
[java] Transforming edu.berkeley.cs.wise.benchmarks.java15.util.PriorityQueue$1...
[java] Transforming edu.berkeley.cs.wise.benchmarks.java15.util.PriorityQueue$Itr...
[java] Transforming edu.berkeley.cs.wise.benchmarks.java15.util.PriorityQueue...
[java] Transforming edu.berkeley.cs.wise.benchmarks.Linear...
[java] Transforming edu.berkeley.cs.wise.benchmarks.MergeSortJDK15...
[java] Transforming edu.berkeley.cs.wise.benchmarks.QuickSortJDK15...
[java] Transforming edu.berkeley.cs.wise.benchmarks.rbtree.Node...
[java] Transforming edu.berkeley.cs.wise.benchmarks.rbtree.RedBlackTree...
[java] Transforming edu.berkeley.cs.wise.benchmarks.rbtree.RedBlackTreeNode...
[java] Transforming edu.berkeley.cs.wise.benchmarks.RedBlackTreeSearch...
[java] Transforming edu.berkeley.cs.wise.benchmarks.SimpleObject...
[java] Transforming edu.berkeley.cs.wise.benchmarks.SortedListInsert$List...
[java] Transforming edu.berkeley.cs.wise.benchmarks.SortedListInsert...
[java] Transforming edu.berkeley.cs.wise.benchmarks.Testme...
[java] Transforming edu.berkeley.cs.wise.benchmarks.Tsp$TspSolver...
[java] Transforming edu.berkeley.cs.wise.benchmarks.Tsp...
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/BellmanFord.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/BinaryTreeSearch$1.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/BinaryTreeSearch$BinaryTree$Node.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/BinaryTreeSearch$BinaryTree.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/BinaryTreeSearch.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/BuggyDijkstra.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/Dijkstra.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/HeapInsertJDK15.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/InsertionSort.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/java15/lang/Math.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/java15/util/AbstractCollection.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/java15/util/AbstractQueue.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/java15/util/Arrays.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/java15/util/PriorityQueue$1.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/java15/util/PriorityQueue$Itr.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/java15/util/PriorityQueue.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/Linear.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/MergeSortJDK15.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/QuickSortJDK15.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/rbtree/Node.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/rbtree/RedBlackTree.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/rbtree/RedBlackTreeNode.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/RedBlackTreeSearch.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/SimpleObject.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/SortedListInsert$List.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/SortedListInsert.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/Testme.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/Tsp$TspSolver.class
[java] Writing to tmpclasses/edu/berkeley/cs/wise/benchmarks/Tsp.class
[java] Soot finished on Wed Sep 07 22:11:03 PDT 2011
[java] Soot has run for 0 min. 9 sec.
[java] Java2HTML Version 1.5
[java] Copyright (c) 1999-2007, Enterprise Solution Consultants Limited, All Rights Reserved.
[java] New Versions available from http://www.java2html.com
[java] (type j2h with no arguments to get help)
[java] Created /Users/ksen/hw1/tmpclasses/stylesheet.css
[java] Created /Users/ksen/hw1/tmpclasses/front.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/SimpleObject.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/Testme.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/rbtree/Node.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/BinaryTreeSearch.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/MergeSortJDK15.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/QuickSortJDK15.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/java15/util/AbstractQueue.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/rbtree/RedBlackTree.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/Linear.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/RedBlackTreeSearch.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/Dijkstra.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/Tsp.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/SortedListInsert.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/java15/util/AbstractCollection.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/HeapInsertJDK15.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/java15/lang/Math.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/InsertionSort.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/java15/util/PriorityQueue.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/BellmanFord.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/java15/util/Arrays.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/BuggyDijkstra.java.html
[java] Created: /Users/ksen/hw1/tmpclasses/edu/berkeley/cs/wise/benchmarks/rbtree/RedBlackTreeNode.java.html
BUILD SUCCESSFUL
Total time: 12 seconds
Koushik-Sens-MacBook-Pro:hw1 ksen$ java -cp tmpclasses:classes edu.berkeley.cs.wise.benchmarks.Testme
0 0 x=0 y=0
I am fine here
Koushik-Sens-MacBook-Pro:hw1 ksen$ cat trace
(65537,_) = (int)(x1,_)
(65538,_) = (int)(x2,_)
(131073,_) = (65537,_)
(131091,_) = (0,2) * (131073,0)
(65539,_) = (131091,_)
else:537 (65539,0) != (65538,0)
(65553,_) = (65538,0) + (0,10)
else:539 (65537,0) == (65553,10)
Koushik-Sens-MacBook-Pro:hw1 ksen$
A trace gives a sequence of instructions executed by the program. Instructions can be of three types: assignments or conditionals or error. We next describe these three types of instructions in details.
An error instruction is simply the string
error
An error instruction appears at the end of a trace if the program execution does not reach the end of the main method.
An assignment instruction can be of the following form:
lvalue = rvalue + rvalue
lvalue = rvalue - rvalue
lvalue = rvalue * rvalue
lvalue = rvalue / rvalue
lvalue = rvalue % rvalue
lvalue = rvalue op rvalue
lvalue = rvalue
lvalue = - rvalue
lvalue = op rvalue
where op could be any arbitrary operator (i.e. an operator that we cannot handle in our decision procedure), an lvalue or a rvlaue is a pair of memory address and the value stored at the memory address. Thus a lvalue or a rvalue can be of the form
(m,*m)
If the memory address m is 0, then the pair represents a constant. If the value *m is _, then the value of *m is not required for the symbolic execution and we can ignore it. The value stored at a memory address, i.e. *m, is used if the symbolic state has no mapping for m during concolic execution. A special kind of assignment statement is of the following form.
(m,_) = (type)(xn,_)
This statement assigns the symbolic input value xn to the memory location m. An example of such an instruction is
(2280636,_) = (int)(x2,_)
A conditional instruction is always of the following forms.
then:branchid true
then:branchid rvalue < rvalue
then:branchid rvalue <= rvalue
then:branchid rvalue > rvalue
then:branchid rvalue >= rvalue
then:branchid rvalue == rvalue
then:branchid rvalue != rvalue
then:branchid rvalue op rvalue
then:branchid op rvalue
else:branchid true
else:branchid rvalue < rvalue
else:branchid rvalue <= rvalue
else:branchid rvalue > rvalue
else:branchid rvalue >= rvalue
else:branchid rvalue == rvalue
else:branchid rvalue != rvalue
else:branchid rvalue op rvalue
else:branchid op rvalue
where the prefix then:branchid means that we have taken the “then” branch of some “if-then-else” statement in the execution and the prefix else:branchid means that the execution has taken the “else” branch of some “if-then-else” statement. The “branchid” statically identifies the “then” or “else” branch---each “then” or “else” branch in the program has a unique branch id. The suffix gives the actual instruction executed during the execution. A suffix “true” means that the execution of the conditional generates the trivial symbolic constraint “true”.
Problem
You need to write a program (in any language such as Java, C, C++, Perl, or Python), say mycute, which will take a trace file and generate an input file. A sample input file is shown below. An input file gives a mapping from symbolic input values to concrete values.
sat
(= x1 -10)
(= x2 -20)
where each xi is a symbolic input value encountered during the execution and each integer is the concrete value that should be used in the next execution. Once you have produced a file “input”, if you re-execute the instrumented executable, then the program will take input values from the “input” file. Note that during the first execution of the instrumented executable, the input file should not be present. In the first execution, the program will initialize all inputs with 0. In subsequent executions, the instrumented executable will use inputs from the file “input”.
Your program will thus take a “trace” file and use it to perform concolic execution and generate the file “input” that will force the program to take a different path in the next execution. Like DART, you need to only worry about linear arithmetic and you should use the yices 1.0.29 theorem prover for constraint solving. The details on how to use yices can be found at http://yices.csl.sri.com/. The following guidelines must be followed to get full points.
1. The search must be DFS; so you may need to maintain extra files between executions. Specifically, your algorithm should maintain the “stack” data structure (see Figure 3, 4, 5 of the DART paper) across executions.
2. Symbolic execution of statements and predicates should be done according to Figure 5 and 6 of the CUTE paper. If a memory location maps to a constant, the mapping should be removed from the symbolic state. This helps to save memory.
3. For every statement of the form (m,_) = (type)(xi,_), you must generate a couple of symbolic constraints: (xi <= MAX_type) and (xi >= MIN_type), where MIN_type and MAX_type are minimum and maximum values that a variable of “type” can store, respectively.
4. Your program “mycute” must return 1, when it has explored all paths in the program and 0, otherwise.
5. You should report the total number of unique branches covered, total number of paths explored, and total number of erroneous paths (i.e. paths that throw an exception) for each benchmark.
6. You should implement the three optimizations mentioned in the CUTE paper to get bonus points.
A sample sequence of commands to test Testme.java would be the following.
rm input
java -cp tmpclasses:classes edu.berkeley.cs.wise.benchmarks.Testme
./mycute
java -cp tmpclasses:classes edu.berkeley.cs.wise.benchmarks.Testme
./mycute
java -cp tmpclasses:classes edu.berkeley.cs.wise.benchmarks.Testme
./mycute
After the last call to mycute, you should notify that a complete search has been done (since Testme.java has 3 execution paths.) Note that we invoke the two commands
java -cp tmpclasses:classes edu.berkeley.cs.wise.benchmarks.Testme
./mycute
iteratively to generate inputs one by one. The script run-jcute.sh can be used to automatically perform this iteration. Therefore, if you do not want to invoke the commands automatically, you can call
./run-jcute.sh ./mycute edu.berkeley.cs.wise.benchmarks.Testme -i 3
where -i 3 says that we want to generate 3 inputs. Your program mycute must return 1 when a complete exploration of the computation tree is over; otherwise, it should return 0.
The directory benchmarks/edu/berkeley/cs/wise/benchmarks/ has a number of sample Java programs that you need to test. A script runall.sh is provided to perform these tests in a batch.
CUTE Homework Part 2
In part 1, you implemented a depth first search (DFS) of the path space. However, DFS is not quite efficient in quickly achieving high branch coverage. In part 2, you need to implement your own search algorithm so that you can quickly achieve high branch coverage. Specifically, in each iteration, you need to pick a branch to negate according to some different strategy. You need to run your implementation on edu.berkeley.cs.wise.benchmarks.Replace and report the number of branches covered, number of iterations performed, and number of erroneous paths. The fewer the number of iterations and the higher the number of branches covered, the better is your algorithm.
Due Date
September 22, 2011.
How to submit?
You should email me a link to the entire archive before 11:59 pm on September 22, 2011 along with instructions to run it. Ideally, I will run the runall.sh script and see if your implementation generates exactly the same set of inputs as CUTE. Please come to my office on September 23, 2011 afternoon to give me a demo.
Comments (0)
You don't have permission to comment on this page.