# Incremental Formula-Based Fix Localization
## 3 Proposed Method
### On-Demand Program Explorer and Incremental Formula Encoder  
_On-demand Program Explorer and Encoder_ (OPEE) is responsible for dynamically constructing and refining the angelic program, as well as the angelic formula in an incremental and on-demand manner. Algorithm 2 shows its details. It takes as input a program \(P\), a concrete input \(inp\), a set of angelic modifications \(mcs\), and an angelic execution path \(\Pi\) that contains angelic-branches. Each angelic modification, \(m\in mcs\), specifies a statement instance \(st\) and a value \(val\), called the angelic value. \(mcs[st]\) represents the angelic value of statement instance \(st\). The abstract execution path \(\Pi\) contains a sequence of branch decisions. \(\Pi[st]\) represents the decision at branch instance \(st\). The procedure _AngelicRefinement( )_ in Algorithm 2 describes how our the on-demand program explorer works. The OPEE component runs the program with the given test input and dynamically substitutes the value produced by statement \(st\in mcs\) with its corresponding angelic value \(mcs[st]\) to explore the program execution path specified in the abstract path \(\Pi\). During program execution, it treats each statement instance, \(st\), differently, depending on whether \(st\) corresponds to a non-deterministic or concrete statement instance in the angelic program \(P_{qgx}\). If \(st\) corresponds to a concrete statement instance of \(P_{qgx}\), the condition at line 2 is true. If \(st\) is an angelic location, then the execution engine perturbs the program memory \(M\) such that the output of \(st\) is replaced with its corresponding angelic value (line 2). In addition, the execution engine also checks whether the current execution has diverted from the expected abstract path by comparing the actual branch decision with the angelic branch decision (line 2). If the diversion happens, then the execution stops. If \(st\) corresponds to a nondeterminism statement in \(P_{qgx}\) (i.e., the condition at line 2 is false), the angelic program is refined by making this statement instance concrete (line 2), and the angelic formula is simultaneously updated to encode this statement instance (line 2). Let \(st\) be the statement instance that is being encoded into the angelic formula. Depending on the type of \(st\), it is encoded in the angelic formula differently. The procedure _UpdateFormula( )_ in Algorithm 2 shows the details. Specifically, if \(st\) is an assignment statement \([v=expr]\), we represent \(st\) as an equivalence relation between variable \(v\) on the right-hand side and expression \(expr\) on the left-hand side (line 4). For a conditional statement, \([if\ cond]\), we add an extra variable \(guard\) to represent the branch predicate, and we represent the conditional statement as an equivalence relation be tween the _guard_ variable and the conditional predicate expression (line 45). If \(st\) is a phi statement instance, \([v=\Phi(guard_{cs},expr)]\), it is presented as an implication constraint \((guard_{cs}\implies(v=expr))\). This implication constraint essentially states that, if the execution trace reaches the statement \(st\) by going through the branch \(guard_{cs}\) of the conditional statement, then the value of variable \(v\) is equal to \(expr\); otherwise, the value of \(v\) is unconstrained. By encoding Phi statements as implication constraints, it allows tightening the constraints of the joined variable by additional constraints when executing other branches of the conditional statement.