LFA Checker

LFA checker is a typestate analysis tool implemented in Infer. LFA checker provides lightweight typestate annotations and it is based on strict sub-class of DFA, which we call BFA. It supports Java and C++ programs analysis.

This repository contains Infer sources with TOPL and our additional checkers enabled:

• LFA checker is a lightweight typestate analysis based on the strict sub-class of DFA, which we call BFA. The sources are in in /lfa-checker/infer/src/checkers/: LfaChecker.ml and LfaCheckerDomain.ml .
• DFA checker is a basic typestate analysis based on DFA. The sources are in /infer/src/checkers/:DfaChecker.ml and DfaCheckerDomain.ml .

Installation

To install follow Infer instructions using sources from this repository. This will compile and setup Infer with LFA, DFA, and TOPL checkers enabled.

Docker image

We also provide Docker image with compiled Infer with LFA, DFA, and TOPL checkers. See README in /docker for installation and usage instructions.

Running Experiments

• Prerequisites: python 3, matplotlib, gnu-time, and bc

• Note: Update TIMECMD to point to gnu-time in /examples/lfa-experiments/lfa.sh

• Experiments are performed by script ./lfa.sh in /examples/lfa-experiments with the following flags:

  • -a - LFA vs DFA: analyze Java test programs using contracts with 5-85 states (LoC ~15k) by LFA and DFA checker and produces execution time and memory usage comparison graphs (time-dfa.png and mem-dfa.png) in /graphs
  • -t - LFA vs TOPL: same as above but makes a comparison to TOPL checker
  • -ak - LFA vs DFA: analyze Java test programs using contracts with 100-4000 states (LoC 500-1k) and produces execution time and memory usage comparison graphs (kstates-time-dfa.png and kstates-mem-dfa.png) in /graphs
  • -tk - LFA vs TOPL: same as above but makes a comparison with TOPL checker

Using LFA and DFA checkers

LFA checker

• LFA checker is invoked by specifying LFA contract (e.g., lfa-cr.json) by an option --lfa-properties lfa-cr.json
• to only invoke LFA checker use option --lfachecker-only
• the sample command to analyze Test.java file with lfa-cr.json is as follows:

infer --lfachecker-only --lfa-properties lfa-contract.json -- javac capture Test.java

• LFA contract (lfa-cr.json in the command above) should be formatted following contract's examples given in /examples/lfa-experiments/cr/ with suffix -lfa.json

DFA checker

• DFA checker is invoked by specifying DFA contract (e.g., dfa-cr.json) by an option --dfa-properties dfa-cr.json
• to only invoke DFA checker use option --dfachecker-only
• the sample command to analyze Test.java file with dfa-contract.json is as follows:

infer --dfachecker-only --dfa-properties dfa-cr.json -- javac capture Test.java

• DFA contract (dfa-cr.json in the command above) should be formatted following contract's examples given in /examples/lfa-experiments/cr/ with suffix -dfa.json