# Incremental Formula-Based Fix Localization
## 2 Background
### MaxSAT-Based Fault Localization  
MaxSAT-based fault localization approaches [12; 14; 15; 19; 22] reduce the fault localization to the maximal satisfiability problem, which finds a variable assignment for a logic formula such that the number of satisfied clauses is maximized. Given a buggy program \(P\) and a failing test case \(T(inp,as)\) that exposes a bug in the program, these approaches perform as follows. First, they use a bounded model checking or symbolic execution tool to construct a logical formula, called _error trace formula_, that semantically represents the error execution of the buggy program and the failing test case. Essentially, this error trace formula is the conjunction \(\Phi\equiv\varphi_{inp}\wedge\varphi_{tf}\wedge\varphi_{as}\), where \(\varphi_{inp}\) encodes the test input, \(\varphi_{tf}\) is called _trace formula_ encoding the semantics of program execution trace induced by the given input, and \(\varphi_{as}\) encodes the test assertion that the program must be satisfied (or the expected output that the program must produce for the given test input). Since the program fails the test, thus, obviously, this error trace formula is logically unsatisfiable. Because the test input and the test assertion are correct by definition, thus, the clauses encoding test input and assertion are not responsible for the unsatisfiability of the error trace formula. Therefore, the causes of this formula unsatisfiability are account for clauses in the trace formula \(\varphi_{tf}\). It is exactly the situation that faulty statements in the program are responsible for the test failure. Second, they treat the constructed error trace formula as an instance of a partial MaxSAT problem, in which the clauses encoding the test input \(\varphi_{inp}\) and test assertions \(\varphi_{as}\) are marked \"hard\", and the clauses encoding program statements in the formula \(\varphi_{TF}\) are marked \"soft\". They then feed the formula into a pMaxSAT solver to obtain a set of MCSs of the formula. Intuitively, the set of clauses in an MCS indicates a corresponding set of minimal fix locations set, and the maximum satisfiability model of the MCS provides angelic values for these fix locations. Thus, as a result, they can produce a set of minimal fix candidates that can make the given test execution become a success. Consider our example in Figure 1. Program-formula-based approaches, such as Bug-Assist [12] and SNIPER [14; 15], first inline all function calls and unwind all loops in the program _foo_ up to a given bound to obtain a loop-free and function-call-free program. They then transform the flatted program into a semantically equal program in the static single assignment form (SSA) [23], in which each variable in the program is assigned, at most, one time. Figure 2 shows the SSA form of the method _foo_ where the number of loop unwinding is two. Each statement in the SSA program is then represented as a logic clause. These clauses are then conjoined to form a _program-formula_, the formula _TF_ shown in Figure 3. This program-formula is semantically equal to the original program with respect to a specific unwinding bound. Specifically, every satisfiable assignment to the program-formula corresponds to a feasible execution in the program, and, vice versa, every program execution (with regard to the unwinding bound) corresponds to a satisfiable assignment of the program-formula. The program-formula is then extended in conjunction with clauses encoding the test input values and clauses encoding the test assertions of the failing test case to form an error trace formula \(1N\wedge TF\wedge AS\), shown in Figure 3. By applying a pMaxSAT solver to this error trace formula, they obtain, totally, five minimal correction subsets: \(mcs_{1}=\{c_{9}\}\), \(mcs_{2}=\{c_{6}\}\), \(mcs_{3}=\{c_{3}\}\), \(mcs_{4}=\{c_{1}\}\), \(mcs_{5}=\{c_{2},c_{4}\}\). Each MCS indicates a corresponding set of minimal fix locations set, and the maximum satisfiability model of the MCS provides angelic values for these fix locations.