# Incremental Formula-Based Fix Localization
## 3 Proposed Method
### On-Demand Program Explorer and Incremental Formula Encoder
```
16 procedureAngelicRefinement(\(mcs,\Pi_{qgx},P_{qgx}\))
17:\(\Phi_{hard},\Phi_{soft}\leftarrow\emptyset,\emptyset\)
18:\(M\gets initialize(P,inp);st\gets st_{entry}\);
19:while\(st\
eq null\)do
20:\((st_{ssa},\pi_{ssa})=convertToSSA(st,\pi_{ssa})\)
21:if\(st_{ssa}\in P_{qgx}\)then
22:if\(st_{ssa}\in mcs\)then
23:\(M\gets perturb(st_{ssa},\Pi_{qgx}[st_{ssa}])\)
24:endif
25:if\((st_{ssa}\) is \([if\ cond])\)then
26:if\(M[guard_{st}])\
eq\Pi_{qgx}[guard_{st}]\)then
27:breakable\(\triangleright\) execution is diverted from the angelic path \(\Pi_{qgx}\)
28:endif
29:endif
30:else\(//\ st_{ssa}\
otin P_{qgx}\)
31:\(P_{qgx}\gets P_{qgx}\cup\{st_{ssa}\}\)\(\triangleright\) refine the angelic program
32:updateFormula(\(st_{ssa},\Phi_{hard},\Phi_{soft}\))\(\triangleright\) refine the angelic formula
33:endif
34:\((st,M)\gets executeStatement(P,M)\)
35:endwhile
36:return(\(P_{qgx},\Phi_{hard},\Phi_{soft}\))
37:endprocedure
38:procedureupdateFormula(\(st_{ssa},\Phi_{hard},\Phi_{soft}\))
39:if\((st_{ssa}\) is \([v=\Phi(guard_{cs},expr)])\)then
40:\(\varphi_{val}\leftarrow(guard_{cs}\implies(v=expr))\)
41:\(\[PERSON]_{hard}\leftarrow\[PERSON]_{hard}\cup\{\varphi_{val}\}\)
42:else
43:if\(st_{ssa}\) is \([if\ cond]\)then
44:\(cond\leftarrow\) conditional expression of \(st_{ssa}\)
45:\(\varphi_{val}\leftarrow(guard_{st}=cond)\)
46:else
47:\(\varphi_{val}\leftarrow(v=expr))\)
48:endif
49:\(ab\leftarrow\) fault predicate of original \(st\)
50:\(\Phi_{hard}\leftarrow\Phi_{hard}\cup\{ab\vee\varphi_{val}\}\)
51:\(\Phi_{soft}\leftarrow\Phi_{soft}\cup\{\
eg ab\}\)
52:endif
53:endprocedure
```  
**Algorithm 2** On-demand Program Explorer and Formula Encoder  
Because if a statement \(st\) is faulty, it would be replaced by a different statement. Thus, in that case, the constraints that constrain the value of variables in \(st\) is invalid and should be relaxed. To reasoning on the faultiness of program statements, we associate with each statement \(st\) in the original program a boolean variable \(ab_{st}\) as a fault predicate. Specifically, the variable \(ab_{st}\) indicates that the statement \(st\) is faulty (or correct) if it is evaluated to \(true\) (or \(false\), otherwise). We encode each conditional and each assignment statement instance \(st\) into the angelic formula by adding a clause \((ab_{st}\vee\varphi_{pal})\) to the hard constraints set and adding a clause \(\
eg ab_{st}\) to the soft constraints set (line 49-51), where \(\varphi_{val}\) is the constraint representation of the statement instance. Since phi statements are fake statements that are introduced to explicitly represent the dependence of variables on branch decisions in the execution trace, the faultiness of a phi statement instance may account for faults in its preceding assignment or conditional statement instances. Thus, we add the constraint representing a phi statement instance into the angelic formula as a hard constraint (line 41). To summarize, the constructed angelic formula is an instance of a partial maximum satisfiability problem in which the hard constraints represent semantic of the input and assertions of a test case and the constructed angelic program; the soft constraints contain a set of fault predicate of statements in the buggy program that have been represented in the angelic program. Each MCS of this angelic error trace formula indicates a minimal set of program statement \(stmt\), in which its corresponding fault predicate \(ab\) is evaluated to \(true\).