unl-pal / argv-transformer

ARG-V automated program transformer
https://www.arg-v.dev/
Apache License 2.0
0 stars 1 forks source link

PAClab Automated Program Transformations

Main Classes

filter.Main.java This program filters a directory of repositories for java files suitable for symbolic execution.

(Suitability is defined in sourceAnalysis.AnalyzedMethod.java by isSymbolicSuitable() method. A java file is suitable if at least one of its methods is suitable.)

Input:

Output:

transform.Main.java Given a directory of suitable java files, this program attempts to transform each into a compilable benchmark.

A directory of benchmarks is created, containing the programs that would successfully compile in their original directory structure.

Input:

Output:

full.Main.java Given a CSV of GitHub repositories (as gathered by RepoReaper), this program will select suitable repositories, download them, search for classes containing SPF-suitable methods, and transform suitable classes into compilable, benchmark programs.

Input:

Output:

PACKAGES

ADDITIONAL FILES

RUNNING WITH SPF

The paths for rt.jar and jfxrt.jar need to be added to Soot's classpath in jpf.ProgramUnderTest.java. (Soot is used for loop detection in class file).

The path for jpf-symbc/build needs to be added to classpath in the compile() methods. (For transformations specific to SPF, i.e. using Debug.makeSymbolicInteger() in place of rand.nextInt().)

For SPF, the environment variable LD_LIBRARY_PATH needs to be set (in Eclipse, Run configurations -> Environment). LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/home/MariaPaquin/pathfinder/jpf-symbc/lib/64bit:/home/MariaPaquin/pathfinder/jpf-symbc/lib

TROUBLESHOOTING

The javac version (used in main.MainTransform.java and mainFullFramework.MainAnalysis.java to compile benchmarks) needs to be the same version as JDK for rt.jar set in Soot classpath (in jpf.ProgramUnderTest.java, used for loop detection).

DEV BRANCH ADD ONS

config file has extended configurations

exprType:

minExpr:

ifStmt: