A Tool Set for Statement Coverage and Invariant Inference

1. Build Project

Build the project by using mvn install. Four artifacts shall be generated in their corresponding directiories:

• Agent-1.0-SNAPSHOT.jar under agent\target
• AutoCoverageAgent-1.0-SNAPSHOT.jar under autocoverageagent\target
• TraceAgent-1.0-SNAPSHOT.jar under traceagent\target
• AutoTraceAgent-1.0-SNAPSHOT.jar under autotraceagent\target

2. Statement Coverage

2.1 Agent

Agent is the driver that launches the statement coverage. To run it, manually updating the pom.xml with statement coverage JavaAgent and RunListener are required. Once the pom.xml is updated, use mvn test on the target project, the statement coverage shall be collected.

2.2 AutoCoverageAgent

AutoCoverageAgent hides the tedious pom.xml, thus simplifying the process. The AutoCoverageAgent automatically downloads the project from GitHub, updates pom.xml, invoke mvn test on the target program, and collects the coverage with a single command listed below. Note: the artifacts of Agent and AutoCoverageAgent are required to put into the same directory

 java -jar AutoCoverageAgent-1.0-SNAPSHOT.jar <GitHub Repo of Target Project>

2.3 Results

The collected data can be found in TargetProjectRoot/logs/ folder. For example: commons-lang/logs

3. Invariant Inference

3.1 Trace Agent

Similar to statement coverage agent, trace agent is the driver that launches the trace of internal state of variables. To run it, manually updating the pom.xml with trace JavaAgent and RunListener values are required. Once the pom.xml is updated, use mvn test on the target project, the trace data of variables shall be collected.

3.2 AutoTraceAgent

AutoTraceAgent hides the tedious pom.xml, thus simplifying the process. The AutoTraceAgent automatically downloads the project from GitHub, updates pom.xml, invoke mvn test on the target program, and collects variable trace with a single command listed below. Note: the artifacts of TraceAgent and AutoTraceAgent are required to put into the same directory

 java -jar AutoTraceAgent-1.0-SNAPSHOT.jar <GitHub Repo of Target Project>

2.3 Results

The collected data can be found in TargetProjectRoot/logs/ folder. For example: commons-lang/logs

2.4 Inferring Invariants

Once the trace data are collected, copy the Python code under backend folder (backend/trace_infer.py) to the folder where the trace data are located at (TargetProjectRoot/logs/), and enter the following command

python trace_infer.py

The results of inferred invariants are written to log file under the same folder with trace_infer.py