# Incremental Formula-Based Fix Localization
## 4 Evaluation Setup
### Implementation  
We have implemented our approach in a prototype tool, named AgxFaults, that automatically localize faults for Java programs. Unfortunately, all the formula-based fault localization techniques, which provide tools or source-code online, are targeting C programs. Thus, for comparison, we also implemented three different existing formula-based fault localization techniques into the tool AgxFaults, specifically, the program-formula (PF) approach used in Reference [12; 14], the flow-insensitive trace formula (FI)-based approach used in Reference [17], and the flow-sensitive trace formula (FS) used in Reference [18] are implemented into AgxFaults.  
We implemented the AgxFaults tool as an extension of NASA's model checker Java-Path-Finder (JPF). The inputs of AgxFaults are a buggy program and a failing test case (given as a JUnit test method or a pair of input and expected post-condition in a configuration file). The output is a list of minimal angelic fix candidate (MFCs), where each MFC contains (1) a set of _suspicious statements_, together with (2) _angelic values_ that these statements should have produced to make the test execution, which originally fails, become a success. AgxFaults includes in itself a customizable formula-builder and a constraint solver for solving formulas. We implement the formula-builder by using extension mechanisms of the JPF and adapted from the implementation of jDart [25], a concolic execution engine for Java programs. Specifically, we use the bytecode factories and listeners extension mechanisms of JPF to (1) create fresh symbolic variables on-the-fly when executing assignments and branch conditions instructions, (2) dynamically perturb concrete program state and force the program execution to follow a specific path, and (3) manipulate and propagate symbolic values along different program execution paths and collect constraints for building error trace formulas. As inherited from jDart, AgxFaults also uses the constraints library jConstraints [26] as an abstraction layer for constraint solvers. Since the jConstraint does not support solving pMaxSMT/MaxSMT and sequential MaxSMT problems, we implemented the [PERSON] & Malik's core-guided max-sat algorithm [27] and the incremental core-guided MaxSMT solving algorithm [20] into the jConstraint library. We use the Z3 ([[https://github.com/Z3](https://github.com/Z3) Prover/z3]([https://github.com/Z3](https://github.com/Z3) Prover/z3)) SMT solver as our back-end constraint solver.  
We implemented the program-formula approach (PF) following the full-flow sensitive formula encoding approaches in Sniper [14] because it was experimentally showed more effective than Bug-Assist. To construct a program-formula, we force the on-demand program explorer and formula builder to explore all paths up a certain bound in the program and encode all of them into the formula, instead of operating on demand. We  
Figure 7: Constraints added in the fourth iteration.  
implemented the single-path flow-insensitive formula approaches by following error trace formula encoding described in Reference [17]. The single-path flow-sensitive formula approach is implemented by following the error trace formula encoding described in Reference [18]. The source code of AgxFaults, which contain our implementation of all above techniques, as well as our benchmark programs, are available online for open access at [[http://bit.ly/agxfaults](http://bit.ly/agxfaults)]([http://bit.ly/agxfaults](http://bit.ly/agxfaults)).