A model checker can generate a lengthy and complicated trace of counterexamples for an erroneous program, with the loop instructions being the largest part of this trace. Consequently, the location of errors in loops is critical to analyzing the overall program. In this paper, we delve into the scalability potential of LocFaults, our error localization approach that utilizes Control Flow Graph (CFG) paths from counterexamples to calculate the Minimal Correction Deviations (MCDs) and Minimal Correction Subsets (MCSs) for each MCD found. The study presents the eficiency of LocFaults on programs with While-loops unfolded b times and deviated conditions ranging from 0 to n. Preliminary results show that LocFaults, constraint-based and flow-driven, is faster and provides more expressive information for the user compared to BugAssist, which is based on SAT and transforms the entire program into a Boolean formula.
Several statistical approaches for error localization have been proposed, such as Tarantula [
Our approach aims to simplify the problem of error localization by reducing it to computing
a minimal set that explains why a Constraint Satisfaction Problem (CSP) is infeasible. The CSP
represents the constraints of the program, counterexample, and the assertion or postcondition
violated. The calculated set can be either a Minimal Correction Subset (MCS) or a Minimal
Unsatisfiable Subset (MUS). Generally, testing the feasibility of a CSP over a finite domain is an
NP-complete problem, which is one of the most dificult NP problems. Thus, explaining the
infeasibility in a CSP is equally challenging, if not harder, and can be classified as an NP-hard
problem. While BugAssist [
In this paper, we investigate the scalability of LocFaults on programs with While-loops that are unfolded b times, and a number of deviated conditions ranging from 0 to 3. Our approach contributes in the following ways compared to BugAssist: • We avoid transforming the entire program into a system of constraints. Instead, we use the CFG (Control Flow Graph) of the program to gather the constraints of the counterexample path and paths derived from it. We assume that at most k conditionals may contain errors, and we calculate MCSs only on the counterexample path and paths that correct the program. • We do not convert program instructions into a SAT (Boolean satisfiability) formula.
Instead, we use numerical constraints that will be handled by constraint solvers. • We do not rely on MaxSAT solvers as black boxes. Instead, we use a generic algorithm that uses a constraint solver to calculate MCSs. • We limit the size of the generated MCSs and the number of deviated conditions. • We can work together multiple solvers during the localization process and choose the most eficient one according to the category of the CSP (Constraint Satisfaction Problem) constructed. For example, if the CSP of the detected path is linear over integers, we use a MIP (Mixed Integer Programming) solver. If it is nonlinear, we use a CP (Constraint Programming) and/or MINLP (Mixed Integer Nonlinear Programming) solver.
Based on our practical experience, as demonstrated in Section 5, we have found that the restrictions and distinctions employed by LocFaults make it faster and more expressive.
The paper is organized as follows. Section 2 introduces the definition of MUS and MCS. In Section 3, we define the ≤ k-MCD problem. In section 4, we describe our contribution to treating erroneous loops, including the Of-by-one bug. The results of our experimental evaluation are presented in Section 5. Section 6 includes the conclusion and discussion of future work.
In this section, we introduce the definition of an IIS/MUS and MCS.
CSP.
A CSP (Constraint Satisfaction Problem) is defined as a triple < , , >, where: • : a set of variables 1, 2, ..., . • = {1, 2, ..., } is the set of constraints.
• : the tuple < 1 , 2 , ..., >. The set contains the values of the variable .
A solution for is an instantiation of the variables ∈ that satisfies all the constraints in . is infeasible if it has no solutions. A sub-set of constraints ′ in is also said infeasible for the same reason except that it is limited to the constraints in ′.
We denote as: • (< , ′, >) = ∅, to specify that ′ has no solutions, so it is infeasible. • (< , ′, >) ̸= ∅, to specify that ′ has at least one solution, so it is feasible.
A Linear Program, denoted as LP, is said to be linear if all the constraints in the set are expressed as linear equations or inequalities. It is considered continuous if the domain of all variables is real. If at least one variable in the set is an integer or a binary (which is a special case of an integer), and the constraints are linear, then is referred to as a Mixed-Integer Linear Program (MIP). If the constraints are expressed as nonlinear equations or inequalities, then is referred to as a Nonlinear Program (NLP).
Let =< , , > an infeasible CSP, we define for : IS. An IS (Inconsistent Set) is an infeasible subset of constraints in the constraint set infeasible . ′ is an IS if: • ′ ⊆ .
• (< , ′, >) = ∅.
IIS or MUS. An IIS (Irreducible Inconsistent Set) or MUS (Minimal Unsatisfiable Subset) is an infeasible subset of constraints of , and all its strict subsets are feasible. ′ is an IIS if : • ′ is an IS. • ∀′′ ⊂ ′.(< , ′′, >) ̸= ∅, (each of its parts contributes to the infeasibility), ′ is called irreducible.
MCS. ′ is a MCS (Minimal Correction Set) if : • ′ ⊆ . • (< , ∖′, >) ̸= ∅.
• ∄ ′′ ⊂ ′ such as (< , ∖′′, >) = ∅. 3. The problem ≤ k-MCD Given an erroneous program modeled in a CFG1 = (, , ), where is the set of conditional nodes, is the set of assignment blocks, and is the set of arcs, along with a counterexample, a Minimal Correction Deviation (MCD) is a set ⊆ such that propagating the counterexample on all the instructions of from the root, while having negated each condition2 in , allows the output to satisfy the postcondition. A MCD is called minimal (or irreducible) if no element can be removed from without losing this property. In other words, is a minimal program correctness in the set of conditions. The size of the minimal deviation is its cardinality. The problem of finding all MCDs of size smaller or equal to is denoted as ≤ k-MCD.
As an illustration (refer to Fig. 1), consider the CFG of the program AbsMinus (refer to Fig. 1b). When provided with the counterexample { = 0, = 1}, this program has one minimal deviation of size 1. While the deviation {0 ≤ 0, 1 = 1 ∧ 0 ̸= 0} does correct the program, it is not minimal. In fact, the only minimal correction deviation for this program is {1 = 1 ∧ 0 ̸= 0}.
In the context of Bounded Model Checking (BMC) for programs, unfolding can be applied to the
entire program or to loops separately [
)) && 4 @ ((i >= j) ==> (\result == i
j)); */ 5 int AbsMinus (int i, int j) { 6 int result; 7 int k = 0; 8 if (i <= j) { 9 k = k+2; } // error : k = k
+2 instead of k=k+1 10 if (k == 1 && i != j) { 11 result = j-i; } 12 else { 13 result = i-j; } 14 return result; } } (a) The program AbsMinus
0 = 0 If If 0 ≤ 0 Else 1 = 1 && 0! = 0
Else
POST:{1 = |0 − 0|} is UNSAT
If If follows the latter approach, where we use a bound to unfold loops by replacing them with nested conditional statements of depth . For example, consider the program Minimum (refer to Fig. 2), which contains a single loop that calculates the minimum value in an array of integers. The efect on the control flow graph of the program Minimum before and after unfolding is illustrated in Figures 2 and 3, respectively. The while-loop is unfolded three times, since three iterations are required to calculate the minimum value for an array of size 4.
LocFaults takes the CFG of the erroneous program, (a counterexample), (a bound on the number of deviated conditions), and (a bound on the size of calculated MCSs) as input. It enables us to explore the CFG in depth by diverting a maximum of conditions from the counterexample’s path by performing the following steps:
• Propagating CE on the CFG until the postcondition is reached. Then, it calculates the 2 /*The minimum in an array of n integers
*/
length) ; tab[k]>=min); 6 int Minimum(int[] tab){ int min=tab[0]; int i=1; while(i<tab.length-1){ /*error, the condition should be (i<tab.
length)*/ if(tab[i]<min){
min=tab[i]; } i=i+1; } return min; 7 8 9 10 11 12 13 14 15 16 } 17 } ; (
≥ 2 = } ] 0 1 [ = 0 ] 3 [ 0 ∧ 3
∧ = ] 1 0 [ = 0 ] 2 [ 0 { :
∧ ] 0 [ 0 1 =
0 0 = highlighted path of a counterexample in dashed lines and a deviation that satisfies the postcondition in dotted lines.
Of-by-one bugs are among the most common errors associated with loops. These bugs cause loops to iterate one too many or one too few times. The cause of these bugs can be ∧ 0 < .ℎ); [] ≥
}
. For each found MCD, it calculates the MCSs on the path that reaches the last deviated condition and allows for taking the path of the deviation.
ℎ < 1 0 . 0
0 lse 4 4 E lse 1 E ] 0 f [ I 0 ] 0 0 [ 0 0 1 ℎ < 1 1 . 0
1 lse 4 4 E lse 2 E ] 1 f [ I 0 ] 1 1 [ 0 1 2 0 1
2
0
1
2
traced back to improper initialization of loop control variables or an erroneous loop condition.
The program Minimum provides an example of this type of error. The error occurs due to
a falsified instruction in the loop condition (line 9) of the While loop. The correct condition
should be (i < tab.length), where tab.length is the number of elements in the table tab. Using
the counterexample {[0] = 3, [
Table 2 shows the erroneous paths generated (column PATH) and the corresponding MCSs calculated (column MCSs) for at most one deviated condition from the execution of the counterexample. The first row pertains to the path of the counterexample, while the second row corresponds to the path obtained by deviating the condition {2 ≤ 0.ℎ − 1}.
LocFaults identifies a single MCS on the path of the counterexample that includes the
constraint 2 = 0[1]. This constraint arises from the instruction on line 11 in the second
iteration of the unfolded loop. When a condition is deviated, the algorithm suspects the third
condition of the unfolded loop, i.e., 2 < 0.ℎ − 1. This deviation implies that we need
to execute a new iteration to satisfy the postcondition.
{ : [0[0] = 3 ∧ 0[
MCSs {2 = 0[1]}
{0 = 1}, {1 = 0 + 1}, {2 = 1 + 1}
This example illustrates a case of a program with an incorrect loop. The error lies in the stopping criterion, which prevents the program from iterating until the last element of the input array. LocFaults, with its deviation mechanism, is capable of accurately locating this type of error. It not only identifies suspicious instructions in the unfolded loop that were not present in the original program, but also provides information about the iterations in which they occur. This information could be extremely useful for programmers to identify errors in the loop.
To evaluate the scalability of our method, we compared its performance with that of BugAssist3 using a benchmark set that we created4. The benchmark set comprises various implementations 3The tool BugAssist can be accessed at http://bugassist.mpi-sws.org/. 4The source code for all programs is available at http://capv.toile-libre.org/Benchs_Mohammed.html of BubbleSort, Sum, and SquareRoot programs, consisting of 19, 48, and 91 variations, respectively. These programs incorporate loops, enabling us to study the scalability of our approach compared to BugAssist. To increase the program’s complexity, we augmented the number of loop iterations in the execution of each tool. Both LocFaults and BugAssist were subjected to the same bound of unfolding loops.
To generate the CFG and counterexample, we employed the tool CPBPV [17], which stands for Constraint-Programming Framework for Bounded Program Verification. LocFaults and BugAssist are designed to operate on Java and C programs, respectively. To enable a fair comparison, we created two equivalent versions for each program: • one version annotated with a JML specification in Java, • another version annotated with the same specification in ACSL, using ANSI-C. Both versions consist of an identical number of lines of instructions, including errors. The precondition defines the counterexample used for the program.
For computing the MCSs, we employed the CPLEX solvers of IBM ILOG, encompassing both MIP and CP solvers. We have implemented the algorithm proposed by Lifiton and Sakallah [ 18]. This implementation requires as input the infeasible set of constraints that correspond to the identified path and a bound on the size of calculated MCSs.
BugAssist leverages the CBMC tool [19] to generate erroneous traces and input data. We utilized MSUnCore2 [20] as the Max-SAT solver (used by BugAssist).
The experiments were conducted on an Intel Core i7-3720QM 2.60 GHz processor with 8 GB of RAM. 5.1. Benchmarks with loops These benchmarks are utilized to evaluate the scalability of LocFaults in comparison to BugAssist for programs with loops, based on the increase of unfolding . We selected three programs with loops: BubbleSort, Sum, and SquareRoot, and introduced an Of-by-one bug in each of them. The benchmark for each program is generated by increasing the number of unfolding , where represents the number of iterations through the loop in the worst case. Additionally, we vary the number of deviated conditions for LocFaults from 0 to 3.
We utilized the MIP solver of CPLEX for BubbleSort. For Sum and SquareRoot, we integrated the two solvers of CPLEX, CP and MIP, during the localization process. Specifically, during the collection of constraints, we employ a variable to store information on the type of CSP being constructed. When LocFaults identifies an erroneous path 5 and before calculating MCSs, it selects the appropriate solver based on the type of CSP associated with that path. If the CSP is non-linear, it uses the CP OPTIMIZER solver; otherwise, it uses the MIP solver.
For each benchmark, we provided an excerpt from the table containing the computation time6. Columns P and L represent the time of pretreatment and calculation of MCSs, respectively. 5An erroneous path is one on which we identify MCSs. 6The complete tables can be found at http://www.capv.toile-libre.org/Benchs_Mohammed.html#ravb, and the sources of these results are available at http://www.capv.toile-libre.org/Benchs_Mohammed.html#sr. 6,000 ) s d n o c se4,000 n i ( s e m iT2,000
0
BubbleSort is an implementation of the bubble sort algorithm. The erroneous statement in the program causes the program to sort the input array by considering only its − 1 first elements, leading to incorrect results. The malfunction of BubbleSort is due to the insuficient number of iterations performed by the loop, which is caused by the faulty initialization of the variable as = .ℎ − 1; the correct instruction should be = .ℎ.
The graph in Figure 4 depicts the variation in computation times for diferent versions of LocFaults and BugAssist, based on the number of unfoldings.
LocFaults (= 0) LocFaults (≤ 1) LocFaults (≤ 2) LocFaults (≤ 3)
BugAssist
The runtime of LocFaults and BugAssist shows exponential growth with the number of unfoldings, with BugAssist consistently having the highest computation times. BugAssist may not be efective for this benchmark. Among the diferent versions of LocFaults (with up to 3, 2, 1, or 0 conditions deviated), all remain usable up to a certain unfolding threshold. The number of unfoldings at which the computation time of BugAssist becomes prohibitively high is lower compared to LocFaults. Additionally, the computation time of LocFaults with up to 3 conditions deviated is lower than that of LocFaults with up to 2 conditions deviated, which is also lower than that of LocFaults with up to 1 condition deviated. The computation times of LocFaults with up to 1 and 0 conditions deviated are nearly identical.
The SquareRoot program (refer to Figure 5) is designed to find the integer part of the square root of the integer 50. An error is injected at line 13, resulting in the incorrect return value of 8, whereas the correct value should be 7. This program has been previously used in the paper describing the BugAssist approach. It contains a linear numerical calculation in its loop and non-linear calculation in its postcondition.
With an unwinding limit of 50, BugAssist identifies the following suspicious instructions for this program: {9, 10, 11, 13}. The localization time is 36.16 and the pre-treatment time is 0.12.
LocFaults identifies suspicious instructions by providing their location in the program (instruction line), as well as the line of the condition and the iteration number of the loop leading to that instruction. For example, {9 : 2.11} indicates that the suspicious instruction is on line 11 of the program, which is inside a loop with the stop condition at line 9 and the iteration number is 2. The sets of suspected instructions identified by LocFaults are listed in Table 3. The pretreatment time is 0.769s. The time for exploring the CFG and calculating MCSs is 1.299s.
We conducted a study of the times for LocFaults and BugAssist with values of "val" ranging from 10 to 100 (where the number of unfoldings "b" used is equal to "val"), in order to analyze the combinatorial behavior of each tool for this program.
The Sum program receives a positive integer from the user and calculates the value of ∑︀=1 as per the postcondition. The error in Sum lies in the condition of its loop, causing it to calculate the sum ∑︀ =1 . The program contains linear numerical instructions =−11 instead of ∑︀ within the core of the loop, along with a nonlinear postcondition.
The time results for the SquareRoot and Sum benchmarks are presented in Tables 4 and 5, respectively. It is observed that the execution time of BugAssist increases rapidly, while the times of LocFaults remain relatively constant. Furthermore, the times of LocFaults with at most 0, 1, and 2 conditions deviated are comparable to those of LocFaults with at most 3 conditions deviated.
The LocFaults method detects suspicious subsets by analyzing the paths of the CFG to identify the MCDs and MCSs from each MCD, utilizing constraint solvers. On the other hand, the BugAssist method calculates the merger of MCSs by transforming the entire program into a Boolean formula and leveraging Max-SAT solvers. Both methods start from a counterexample to identify potential issues. In this paper, we have presented a scalability exploration of LocFaults, with a focus on handling loops with the Of-by-one bug. The initial results indicate that LocFaults is more efective than BugAssist for programs with loops. The execution times of BugAssist tend to rapidly increase with the number of loop unfoldings, while LocFaults shows better scalability in this aspect.
As part of our future work, we plan to validate our results on programs with more complex loops. We also intend to compare the performance of LocFaults with existing statistical methods. To further enhance our tool, we are developing an interactive version that presents suspect subsets one by one, leveraging the user’s knowledge to select the conditions that should be deviated. Additionally, we are considering ways to extend our method to handle numerical instructions involving calculations on floating-point [16] M. Barnett, K. R. M. Leino, Weakest-precondition of unstructured programs, in: Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, 2005, pp. 82–87. [17] H. Collavizza, M. Rueher, P. Van Hentenryck, Cpbpv: a constraint-programming framework for bounded program verification, Constraints 15 (2010) 238–264. [18] M. H. Lifiton, K. A. Sakallah, Algorithms for computing minimal unsatisfiable subsets of constraints, Journal of Automated Reasoning 40 (2008) 1. [19] E. Clarke, D. Kroening, F. Lerda, A tool for checking ansi-c programs, in: Tools and Algorithms for the Construction and Analysis of Systems: 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29-April 2, 2004. Proceedings 10, Springer, 2004, pp. 168–176. [20] J. Marques-Silva, The msuncore maxsat solver, SAT (2009) 151.