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
underagent\target
AutoCoverageAgent-1.0-SNAPSHOT.jar
underautocoverageagent\target
TraceAgent-1.0-SNAPSHOT.jar
undertraceagent\target
AutoTraceAgent-1.0-SNAPSHOT.jar
underautotraceagent\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