HTTPS SSH
Tree Dependence Analysis uses Apache Ant to facilitate building and testing.

Type 'ant' at the Tree Dependence Analysis folder to see use cases of the ant build file.

'ant analyze-app -Dapp=skewheap’ will analyze the skewheap app to check point blocking legality.

Tree Dependence Analysis relies on the z3 theorem prover (https://github.com/Z3Prover/z3). Please
be sure that z3 is installed and part of your path to run Tree Dependence Analysis.

The original source code is in apps/base/skewheap. Refer to that to see what kind of function
the dependence analysis looks at and what kind of accesses it looks for.

Buildfile: build.xml

compile:

mkappsdir:

check-app:

analyze-app:
     [java] TreeSplicer args: --indir base --outdir block --nosplice --utilstats skewheap util 
     [java] Method name: reset
     [java] Falling through because not enough parameters.
     [java] Method name: touch
     [java] Method name: startSystem
     [java] Falling through because not enough parameters.
     [java] Method name: effectiveBlock
     [java] Falling through because not enough parameters.
     [java] Method name: reset
     [java] Falling through because not enough parameters.
     [java] Method name: elapsedTime
     [java] Falling through because not enough parameters.
     [java] Method name: traversal_transform
     [java] Recursive structure is being modified.
     [java] 	 candidate recursive method: traversal_transform
     [java] 		 selected for transformation
     [java] Condition set 0
     [java] 
     [java] *--------------------------------------------------------------
     [java] *	All sets of collisions returned unsat. Transformation was determined SAFE!
     [java] *--------------------------------------------------------------
     [java] *	Total number of actual z3 calls: 32
     [java] *	Total time spent in z3 calls: 649.49
     [java] *--------------------------------------------------------------
     [java] 
     [java] total time (ms): 2480.98
     [java] analysis time (ms): 1660.71
     [java] 
     [java]

It can be seen that for skewheap about 1/3 of the analysis time is spent in z3 calls.
This number goes up significantly for the more complicated benchmarks.

The AST structure of the function being analyzed, the list of accesses in the function,
and a list of collisions that could preclude point blocking are also saved in the out directory.
Method names that are listed by the analysis are ones that were determined to be recursive
because a contained function call matching the name of the method was found.
This can be modified to only look for functions named ‘traversal_transform’ by changing
the ‘annotations’ flag in src/transform/RecursiveStructureAnalysis.java.