# Link

Zenodo Link:

https://zenodo.org/record/4741399#.YJSQKCYRWHs

# Introduction

The artifact is in the directory '/home/artifact/'.

The password of the VM is 123456



As presented in Section 4.1, our implementation is multi-threaded and the time budget is one hour.  Therefore, it is hard to reproduce some of our experimental results on a different machine, especially a virtual machine. For example, it may take DFASy longer to solve a problem on the virtual machine and fewer candidates are validated in an hour. 



It takes about 2 days to run all the experiments completely. We provide scripts to run all experiments, as well as some or a single experiment. We run the experiment once in advance and save the results in the folder ./result/. Fortunately, DFASy successfully solves all 14 problems. We provide the python scripts to print synthesized DFAs, as well as Table2 and Fig7 in our paper. 



# File Structure

dlp.jar: 

​	bytecode of our implementation.

./jre/ & ./target/: 

​	dependencies.

./result/: 

​	experimental results

*.py

​	scripts for print results in our paper

*.sh

​	scripts for rerun all the experiments

# How to print synthesized DFAs

`python3 prettyPrint.py [TOOL] [Problem]`
`tool=
		naive 	print results of DFASY-Naive
		ab 	print results of DFASY-Ab
		br 	print results of DFASY-Br
		dfasy 	print results of DFASY
	problem=
		reachdef 		for the problem [ReachDef]
		livevar 		for the problem [LiveVar]
		avblexpr 		for the problem [AvailExpr]
		busyexpr 		for the problem [BusyExpr]
		nulldetect 		for the problem [NullCheck]
		nullverify 		for the problem [NonullCheck]
		initvar 		for the problem [InitVar]
		derefobj 		for the problem [DerefObj]
		avblexprconst 		for the problem [AE-Const]
		avblexprnoconst 	for the problem [AE-Noconst]
		busyexprconst 		for the problem [BE-Const]
		busyexprnoconst 	for the problem [BE-Noconst]
		reachdefexpr 		for the problem [RF-Expr]
		reachdefconst 		for the problem [RF-Const]
`

A png file will be saved in the working directory.

For example, you can print reaching definition synthesized  by DFASy  using:

`python3 prettyPrint.py dfasy reachdef`

and a file named dfasy-reachdef.png will be produced.

# How to print Table 2

`python3 printTable2.py [TOOL]`

where  [TOOL] is dfasy (for DFASy), naive (for DFASyNaive), ab (for DFASyAb) or br (for DFASyBr)



For example, you can print results of DFASy using:

`python3 printTable2.py dfasy`

# How to print Fig 7

`python3 printFig7.py`

Note that we only print the data in text.



# How to rerun all the experiments

It takes about 2 days to run all the experiments completely. We provide scripts to rerun all experiments, as well as some or a single experiment.



## Solve a single problem (10s ~ 1h)

`java -cp dlp.jar com.dlp.dfa.derive.[TOOL] -help`

where [TOOL] is DFASy, DFASyNaive, DFASyAb or DFASyBr



For example, you can run DFASy to solve reaching definition using:

`java -cp dlp.jar com.dlp.dfa.derive.DFASy -reachdef`



## Solve all the problems with a single tool (20m ~14h)



`./run-[TOOL].sh`

where  [TOOL] is dfasy (for DFASy), naive (for DFASyNaive), ab (for DFASyAb) or br (for DFASyBr)



## Rerun all the experiments (about 2 days)

`./run-all.sh`