Nadjib Lazaar
email: lazaar.nadjib@irisa.fr

Arnaud Gotlieb
email: arnaud.gotlieb@irisa.fr

Yahia Lebbah
email: ylebbah@gmail.com

On Testing Constraint Programs

The success of several constraint-based modeling languages such as OPL, ZINC, or COMET, appeals for better software engineering practices, particularly in the testing phase. This paper introduces a testing framework enabling automated test case generation for constraint programming. We propose a general framework of constraint program development which supposes that a first declarative and simple constraint model is available from the problem specifications analysis. Then, this model is refined using classical techniques such as constraint reformulation, surrogate and global constraint addition, or symmetry-breaking to form an improved constraint model that must be thoroughly tested before being used to address real-sized problems. We think that most of the faults are introduced in this refinement step and propose a process which takes the first declarative model as an oracle for detecting non-conformities. We derive practical test purposes from this process to generate automatically test data that exhibit non-conformities. We implemented this approach in a new tool called CPTEST that was used to automatically detect non-conformities on two classical benchmark programs, namely the Golomb rulers and the car-sequencing problem.

Introduction

Constraint programs such as those written in modern Constraint Programming languages and platforms (e.g. OPL [START_REF] Flener | Air-traffic complexity resolution in multi-sector planning[END_REF] , COMET [START_REF] Gotlieb | Tcas software verification using constraint programming[END_REF] , ZINC [START_REF] Holland | Robust solutions for combinatorial auctions[END_REF] , CHOCO 6 , GECODE 7 , ...), aim at solving industrial combinatorial problems that arise in optimization, planning, or scheduling. Recently, a new trend has emerged that propose also to use CP programs to address critical applications in e-Commerce [?], airtraffic control and management [?,?], and critical software development [?,?]. While constraint program debugging drew the attention of some researchers, few supports in terms of software engineering and testing have been proposed to help verify critical constraint programs. Automatic debugging of constraints programs has been an important topic of the OADymPPaC 8 project, that resulted in the definition of generic trace models [?,?], the development of post-mortem trace analyzers, such as Codeine for Prolog, Morphine [?] for Mercury, ILOG Gentra4CP, or JPalm/JChoco. These models and tools help understand constraint programs and contribute to their optimization and correction, but they are not dedicated to systematic fault detection. Indeed, functional fault detection requires the definition of a reference (called an oracle in software testing) in order to check the conformity between an implementation and its reference [?]. Automatic fault detection also requires the definition of test purpose to decide when to stop testing [?]. Whereas conventional software development benefits from research advances in software verification (including static analysis, model checking or automated test data generation), developers of constraint programs are still confined to perform systematic verification by hand.

Automatic constraint program testing cannot be easily handled by existing testing approaches because of the two following reasons: firstly, constraint programs are intrinsically non-deterministic as they represent sets of solutions and conventional definitions of conformity do not apply ; secondly, the refinement process of constraint programs is specific to CP. Indeed, developers usually start with an initial declarative constraint model of the problem, which faithfully translates the problem specifications, without granting interest to its performances. As this model cannot handle large-sized instances of the problem, they exploit several refinement techniques to build an improved model. For example, usual refinement techniques include the use of dedicated data structures, constraint reformulation, global constraints addition, redundant and surrogate constraint addition, as well as constraints which break symmetries (these constraints usually improve considerably the effectiveness of the solving process). The refinement process, carried out by the developer, is an error-prone process and we believe that most of the faults are introduced during this step.

In this article, we propose a testing framework for checking the correctness of a constraint program implementation. The oracle for the constraint program under test is an initial declarative model considered to be valid w.r.t. the user requirements. Our framework is based on the definition of four distinct conformity relations to handle constraint satisfaction problems as well as optimization problems. A practical consequence of these definitions is the proposal of test purposes for evaluating the conformance of constraint programs. Note that this paper does not address another essential topic of CP verification which is the correction of solvers or optimizers. We propose an algorithm for checking the correction of the CP program under test that solves a set of derived constraint problems able to exhibit non-conformities. We implemented our approach in a tool called CPTEST that seeks non-conformities in OPL programs. For evaluating the proposed testing process, CPTEST was used to find non-conformities in various faulty OPL constraint programs of the Golomb rulers and the car-8 contraintes/OADymPPaC/ sequencing problem. It was also used to assess the conformity for small instances of the problem.

The rest of the paper is organized as follows: Sec. ?? illustrates our testing framework on a simple case in order to show a typical non-conformity case. Sec. ?? gives the definition of conformity relations required in the framework. In Sec. ??, the testing process we derive from these definitions is introduced and illustrated on a simple example. Sec. ?? presents the CPTEST tool and details our experimental evaluation. Finally, Sec. ?? concludes the paper and draws some perspectives to this work.

An illustrative example

Let us illustrate some of the refinement techniques on the classical problem of the Golomb rulers, which has various applications in fields such as Radio communications or X-Ray crystallography.

A Golomb ruler [?] is a set of m marks 0 = 3 Testing constraint programs

x 1 < x 2 < ... < x m such as m(m -1)/2 distances {x j -x i | 1 ≤ i < j ≤ m} are distinct. A
(i < j && k < l && cc1: forall (i in 1..m-1) (i != k || j != l))) x[i] < x[i+1]; x[j] -x[i] != x[l] -x[k]; cc2: forall(ind in indexes) } d[ind] == x[ind.i]-x[ind.j]; cc3: x[1]=0; cc4: x[m] >= (m * (m -1)) / 2; // cc5: allDifferent(all(ind in indexes ) d[ind]); cc6: x[2] <= x[m]-x[m-1]; cc7: forall(ind1 in indexes, ind2 in indexes, ind3 in indexes: (ind1.i==ind2.i)&& (ind2.j==ind3.j) &&(ind1.j==ind3.j)&& (ind1.i<ind2.j < ind1.j)) d[ind1]==d[ind2]+d[ind3]; cc8: forall(ind1,ind2,ind3,ind4 in indexes: (ind1.i==ind2.i)&&(ind1.j==ind3.j)&& (ind2.j==ind4.j)&&(ind3.i==ind4.i)&&(ind1.i<m-1) &&(3<ind1.j<m+1)&&(2<ind2.j<m)&&(1<ind3.i<m-1)&& (ind1.i < ind3.i < ind2.j < ind1.j)) d[ind1]==d[ind2]+d[ind3]-d[ind4]; cc9: forall(i in 2..m, j in 2..m, k in 1..m : i < j) x[i]=x[i-1]+k => x[j] != x[j-1]+k; } -A - -B -

Notations

In the rest of the paper, x denotes a vector of variables and (x\x i ) stands for substituting x by the valuation x i .

Model Mx(k)      C1(x) ... Cn(x) Solve()
A constraint program includes a constraint model M x (k), which is a conjunction of constraints C i (x) over variables x parameterized by k, the parameters vector of the model. Note that x may depend on k. For the Golomb rulers, k is the order of the ruler while x represents the vector of marks. If k = 3 then one seeks for a ruler with 3 marks (e.g., x=[0 1 3]) while if k = 4 one seeks for a ruler with 4 marks (e.g., x=[0 1 4 6]). Solve() is a generic procedure representing either the call to a constraint solver in the case of constraint satisfaction problem or the call to an optimization procedure. In this latter case, we note f the cost function (for the sake of clarity, f will be a minimization function but maximization problems can be tackled as well). We consider that k belongs to K the set of possible values of the parameters for which M x (k) has at least one solution. sol(M x (k)) denotes the set of solutions of M x (k) and while P roj y (sol(M x (k))) expresses the projection of sol(M x (k)) on the set y when y ⊆ x. In optimization problems, one usually starts with feasible solutions ranging in a cost interval [l, u]. Therefore, we introduce the set

Bounds f,l,u (M x (k)) = {x|x ∈ sol(M x (k)), f (x) ∈ [l, u]}
To clarify these notations, Fig. ?? shows an example of a real objective function where point x 1 is a global minimum with a cost f (x 1 ) = b and points x 0 , x 3 belongs to Bounds f,l,u (M x (k)). Note that x 1 as well as x 2 do not necessarily belong to Bounds f,l,u (M x (k)). In our framework, we consider the initial declarative constraint model to be a testing oracle, called the Model -Oracle , and noted M x (k). M x (k) represents all the solutions of the problem and strictly conforms the problem specifications. We suppose that, for any parameter instantiation, M x (k) possesses at least one solution. Considering unsatisfiable Model-Oracles could be interesting for some applications (such as software verification [?]) but we excluded these cases in order to avoid considering equivalence of unsatisfiable models. The Constraint Program Under Test (CPUT) is a constraint model P z (k) (possibly unsatisfiable) which has to be tested for correction against the Model-Oracle. P z (k) is intended to solve difficult instances of the problem. We built our framework on the hypothesis that checking whether M (x\x0) (k 0 ) is true where x 0 is a point of the search space is not hard, while finding such an x 0 satisfying the constraints may be hard. Given a CPUT P z (k) and its Model-Oracle M x (k), we suppose that x ⊆ z as P z (k) was obtained by refining M x (k). Hence, the set of variables in z distinct of x are dependant variables that are automatically instantiated when x is instantiated.

Constraint models and programs

Conformity relations

The correction of a CPUT w.r.t. a Model-Oracle can be approached through the usage of conformity relations. These relations aim at assessing the correction of the CPUT, a notion that can be expressed with various levels of depth. We propose four set-based definition of conformity divided on two groups: conformity relations adapted to constraint satisfaction problems and conformity relations for optimization problems.

Conformity relations for constraint satisfaction problems

The simplest definition of correction, well-adapted for problems where a single solution is sought, is given by the following conformity relation:

Definition 1 (conf one ) P conf k one M ⇔ P roj x (sol(P z (k))) = ∅ ∧ P roj x (sol(P z (k))) ⊆ sol(M x (k)) P conf one M ⇔ (∀k ∈ K, P conf k one M )
Roughly speaking, for a given instance k, conf k one asks the solutions of the CPUT to be included in the solutions of the Model-Oracle. As an example, Unfortunately, such a proof would require not only to find all the solutions of the CPUT which is an NP-hard problem for some constraint languages (e.g., the finite domains constraint language), but also to perform this for any value of k. This seems to be intractable in general (probably undecidable) and then we will confine ourselves to the search of non-conformities within finite resources. Conformity relations for optimization problems Conformity relations for optimization problems is harder to define, as practicians usually start their refinement process by the definition of bounds for the optimal case [?] . Note also that non-conformities may arise in the cost function itself and we wanted our conformity relations to be able to tackle those cases.

P conf k bounds M ⇔ P roj x (bounds f ,l ,u (P z (k))) = ∅ ∧ P roj x (bounds f ,l ,u (P z (k))) ⊆ bounds f,l,u (M x (k))
Note that the definition of conf bounds does not require that f = f and then cases where the cost function has been refined can also be handled. This conformity relation is useful for addressing hard optimization problems as it does not require the computation of global minima. As a result, it can be used to assess the correction of models on relaxed instances of the global optimization problems. We will come back on this advantage in the experimental validation section. However, for some problems, it may be useful to assess not only the correction but also the fact that the CPUT actually computes optimal solutions. This can be performed by using the following definition which ensures that the global optimum belongs to [l , u ].

Definition 4 (conf best )

P conf k best M ⇔      P conf k bounds M, bounds f,-∞,l (M x (k)) = ∅, bounds f ,-∞,l (P z (k)) = ∅

A CP testing framework

Testing a CPUT w.r.t. an model-oracle requires to select test data. In this context, a test datum defines an instance of the CPUT and a point of the search space.

Definition 5 (Test datum) Given a CPUT P z (k) and a Model-Oracle M x (k), a test datum is an instantiated pair (k 0 , x 0 ) of parameters and variables.

Note that evaluating M k (x) on the test datum (k 0 , x 0 ) results true when x 0 is a solution of the model and false otherwise. Test execution is realized by evaluating both P z\z0 (k 0 ) and M x\x0 (k 0 ) 9 and checks whether the results (either true or false) are the same. Depending on the selected conformity relation, a test verdict can be issued. This elementary process can be repeated as long as one wishes, but it is more interesting to guide the test data generation process by the use of test purposes. Seeking non-conformities implies finding test data such as the CPUT is satisfied and the Model-Oracle is violated. This enables to detect faults in CPUT, and helps the constraint programmer to revisit its refinements. Based on the selection of a conformity relation, non-conformities can be sought with the following test purposes: conf one Given k, find a solution to P z (k) ∧ ¬C i where C i is a constraint of the Model-Oracle M x (k). The idea here is to isolate a non-conformity by looking independently at each constraint of the model-oracle. Considering all the constraints of the model-oracle would also be possible but less efficient to detect non-conformities as more constraints would be involved. Note that heuristics can be defined on the order of constraints to consider first. Note also that proving the unsatisfiability of P z (k) ∧ ¬C i for all C i ∈ M x (k) permits to issue a conformity certificate saying that P conf k one M . conf all Given k, find a solution to (M x (k)∧¬C i )∨(P z (k)∧¬C i ) where C i (resp.

C i ) is a constraint of the Model-Oracle M x (k) (resp. P z (k)). In this case, proving the unsatisfiability of these constraints permits to issue the conformity certificate P conf k all M , but this is not often desirable as constraint solving usually requires to issue a single solution instead of all solutions. conf bounds Given k and [l , u ], find a solution to P z (k)

∧ ¬C i ∧ f (z) ∈ [l , u ] ∧ f (x) ∈ [l, u]
where f, f are the cost functions of the Model-Oracle M x (k) and the CPUT P z (k). Proving that these constraints are unsatisfiable permits to issue a certificate P conf k bounds M . conf best Given k, find a solution to (P ¬conf k bounds M ) ∨ bounds f,-∞,l (M x (k)) = ∅ ∨ bounds f ,-∞,l (P z (k)) = ∅. Proving that these constraints are unsatisfiable permits to issue a conformity certificate P conf k best M .

Interestingly, any solution found by the guidance of one of these test purposes can be stored for further investigations. Indeed, it can be used to debug the CPUT by looking at the violated constraint and it can also enrich a test set that will serve to assess the correction of future versions of the CPUT. In addition, conformity certificates are essential for those who want to convince third-party certification authorities that their CP programs can be used in critical systems [?,?]. So, the proposed testing framework has a role to play in various phases of the constraint program development.

We now propose a simple but generic algorithm for searching non-conformities:

Algorithm 1: one negated(B, {C 1 , ...C n }) Input : B, {C1, ...Cn} sets of constraints. Output: conf when {C1, ...Cn} conform B, ¬conf (+ non-conformity point) otherwise nc ← ∅ X ← vars(B) foreach Ci ∈ {C1, ..., Cn} do V ← vars(Ci)/X if V = ∅ then nc ← Solve(B ∧ ¬Ci) else nc ← Solve(B ∧ ¬P roj X (Ci)) if nc then return ¬conf (nc) end return conf
where Solve(B) denotes the algorithm to find the first solution of the constraints B, vars(B) denotes the set of variables in B and P roj X (C) denotes the constraint projection on variables X.

Algorithm ?? takes two constraint sets as input and returns either conf when both sets conform with relation conf one or ¬conf (non-conformity point) where a non-conformity point has been found. Note that the other conformity relations can easily be implemented using this algorithm just by adjusting the call parameters. Special care has to be taken when building the negation of a model. For example, consider a Model-Oracle M with x-y!=x-z; x-y!=y-z; x-z!=y-z; and a CPUT P with c1: x-y=d1; c2: x-z=d2; c3: y-z=d3; c4: allDiff(d1,d2,d3);. Here, it is trivial to see that P conf all M but if c1 is selected for negation, M ∧ ¬c1 has solutions as d1 is out of the scope of M. In the definitions of the conformity relations, these cases were discarded by the use of projections on the variables of the model-oracle. As computing general projections is expensive, pragmatic solutions have been found that are discussed in the experimental section of the paper (Sec.??).

Providing that the underlying constraint solver is sound and complete, this algorithm is sound as it cannot report conf if there exists a non-conformity point. Indeed, given k, upon completion of the algorithm the unsatisfiability of P z (k) ∧ ¬M x (k) is demonstrated showing that both models conform with the A keypoint of our approach is that test data can be automatically generated using the same constraint solver as the one used for solving the CPUT. Recall that we rely on the solver and we are only interested in detecting nonconformities in models.

Experimental validation

Implementation

We implemented the testing framework shown above in a tool called CPTEST for OPL (Optimization Programming Language [?]). We chose OPL because it is one of the main programming environments for developing constraint programs and also critical constraint programs [?]. CPTEST is based on ILOG CP Optimizer 2.1 from ILOG OPL 6.1.1 Development Studio. All our experiments were performed on Quadcore IntelXeon 3.16Ghz machine with 16GB of RAM and all the models we used to perform these experiments are available online at www.irisa.fr/celtique/lazaar/CPTEST.

CPTEST includes a complete OPL parser and a backend process that produces dedicated OPL programs as output. These OPL programs must be solved in order to find non-conformities. If a solution is found, then CPTEST stops and reports the non-conformity to the user. Whenever all these OPL programs are shown to be inconsistent, then a conformity certificate is issued. The tool is parameterized by several options, including the chosen conformity relation, the instance of the problem, etc. CPTEST handles the overall OPL language and can negate most of the constraints that can be expressed in OPL. However, it cannot negate all the global constraints available, such as the cumulative or circuit global constraint. Tab.?? summarizes the syntax of OPL constraints handled by CPTEST. OPL includes two aggregators, namely forall and or. The universal qualifier forall is used to declare a collection of closely related constraints and to build global constraints. Interestingly, the or aggregator can be used to negate forall, as or implements existential quantification. The OPL If-then-else statement is less general than it may appear as its condition cannot contain decision variables. Its negation can be computed by negating the Then-part and Else-part without any loss of generality, as our goal is only to find nonconformities instead of computing the negation of a general model. Our CPTEST tool handles several global constraints over discrete values, namely allDifferent, allMinDistance, inverse, forbiddenAssignments, allowedAssignments and pack. These constraints can be represented as an aggregation of constraints and then computing their negation becomes trivial with the rules presented above and using the other global constraints. For example, the negation ofC: allDifferent( all

(i in R) x[i]) is or(ordered i,j in R) x[i] = x[j] as C rewrites to forall(ordered i,j in R) x[i] != x[j]
, and the negation of forbiddenAssignments is simply allowedAssignments.

We implemented algorithm ?? in CPTEST with several improvements. In particular, by noticing that it is unnecessary to search for non-conformities on constraints that are included in both the CPUT and the Model-Oracle, we implemented a simple rewriting system to check equality modulo Associativity-Commutativity (≡ AC ). The system implements the following rules:

   x • y → y • x, (x • y) • z → x • (y • z), x + 0 → x, x * 1 → x, x * 0 → 0, x × (y • z) → (x × y) • (x × z), x < y ↔ y > x, x ≤ y ↔ y ≥ x, x -0 → x,  
 where • ∈ {+, * , ∧, ∨}, × ∈ { * , ∧, ∨} and • ∈ {+, ∧, ∨}. In algorithm ??, the constraint C i is discarded whenever there exists C i in D such as

C i ≡ AC (C i ).
In addition, practical solutions for the handling of local variables and the computation of constraint projection exist: (a) Annotating the CPUT with constraints that define local variables ; (b) Computing constraint projection with Fourier's elimination in the case of linear constraints ; (c) Eliminating false alarms with constraint checking. In CPTEST, we implemented (a) and (c).

The goal of our experimental evaluation was to check that CPTEST is able to detect faults in OPL programs. We fed CPTEST with faulty models coming from initial constraint program development. Indeed, we developed optimized models of two well-known CP problems, namely the Golomb rulers and the car sequencing problem, and we kept first versions of these models for which faults were found.

The Golomb ruler problem

The model-oracle of the Golomb rulers is given in part A of Fig. ?? while part B contains a conform version of an optimized version of the model when the comment on constraint cc5 is removed. Let us call P this version. The four intermediate versions of the Golomb rulers we kept from our initial program development contain realistic faults, not invented for the experiment. Tab.?? shows the four faulty versions expressed with the constraints of P. Note that constraint cc6 breaks symmetries in the problem and then it removes solutions (valid Golomb rulers) w.r.t. the model-oracle. Constraint cc10 is not documented in P, it corresponds to forall( i in m..3*m) count(all(j in indexes)d[j],i)==1. For each CPUT, we studied its conformity w.r.t. the model-oracle (part A) using the four conformity relations. The results we got for an instance parameter m = 8 are given in Tab.??. For the conf bounds relation, the interval [50, 100] was used to feed the relation, knowing that the global minimum is x m = 34 when m = 8. Each time a non-confirmity was found, it was reported with the CPU time required to find it. Firstly, the four faulty CPUT were reported as being non-conforms and the time required for finding these non-conformities is acceptable (less than a few minutes in the worst case). Secondly, this experiment shows that the most practical conformance relations (i.e., conf one and conf bounds ) are preferable to the other ones for efficiency reason. Indeed, for the first three CPUT, these relations gave results less than 10sec. Note that non-conformities are represented either by invalid Golomb rulers (e.g., 44-35 = 35-26 = 9 in the CPUT1/conf one case) or by valid Golomb rulers (e.g., CPUT1/conf all case). In fact, a valid Golomb ruler r can be produced when the model-oracle is satisfied by r while the CPUT is refuted by r. These non-conformities correspond to cases where the CPUT misses solutions of the problem. Interestingly, P is shown as being non-conform with the conf All relation and the non-conformity that is found represent a valid Golomb ruler (i.e., [0 7 9 12 37 54 58 64]). In fact, recalling that P includes constraints that break the symmetries, this result was expected. Finally, note that conformity of P when conf best is selected was impossible to assess within the allocated time (timeout=5 400s). In fact, computing the global minimum of the Golomb ruler rapidly becomes hard even for small values of m (e.g., CPUT3/conf best ). Our experimental evaluation also had the goal to check that computing nonconformities with CPTEST was less hard than computing solutions. For that, Fig. ?? shows: A) the CPU time required to find a global optimum for instances of the Golomb rulers (red line) and B) the CPU time required to find nonconformities with CPTEST with the conf bounds conformity relation (blue line). The search heurisitic used in both cases is the default heuristic of OPL, i.e. depth-first search with restarts, and branch-and-bound for the global optimization problem. CPTEST can find non-conformities when m < 22 in a reasonable amount of time because the hard global optimization problem has been relaxed in a simpler satisfaction problem, in order to deal with larger instances. This is the essence of the conf bounds conformity relation.

The car sequencing problem

The car sequencing problem (CSeq) illustrates interesting features of CP including wide parameter settings, redundant, surrogate and global constraints addition, and specialized data structures definition. This is a constraint satisfaction problem that amounts to find an assignment of cars to the slots of a car-production company, which satisfies capacity constraints.

As a model-oracle of this problem, we took the model given in the OPL book [?]. In this model, capacity constraints are formalized by using constraints r outof s, saying that from each sub-sequence of s cars, a unit can produce at most r cars with a given option. Starting from this model, we built an optimized model by introducing several refinements, including a new data structure setup[o,s] which takes value 1 if option o is installed on slot s, redundant and global constraint addition (e.g., pack constraint). When building our improved model of car sequencing, we recorded four faulty constraint models that are used for experiments. Here again, the idea was to keep models that represent realistic faults instead of a posteriori injected faults. These four models are available online on the site mentioned above.

Tab.?? gives the results of CPTEST on two instances of the problem: an assembly line of 10 cars, 6 classes and 5 options ; an assembly line with 55 cars, 7 classes and 5 options. Using conf one , CPTEST reports non-conformities for the three first CPUT in less than 1sec for both instances. CPUT4 has no solution as the fault introduced on the pack constraint prunes dramatically the search space. This case is interesting as detecting this fault is really uneasy. With the conf all relation, the results are balanced as three instances were not detected as nonconformant within the allocated time slot. For example, in CPUT2, the capacity constraint of the first option is violated (1 out of 2). This fault results from a bad formulation but it is quickly detected with conf one . When conf all is selected, more constraints have to be negated and then our algorithm has to backtrack a lot, which explains the failure. The non-conformity reached in this case satisfies the model-oracle and violates CPUT2, so it represents a correct assembly line that CPUT2 excludes from its solutions. Therefore, we can conclude that CPUT2 adds and removes solutions which make it difficult to detect as non-conform.

Conclusion

In this paper, we introduced for the first time a testing framework that is adapted to standard CP development processes. The framework is built on solid notions such as conformity relations, oracles and test purposes that are specific to CP. We also presented CPTEST an implementation of our framework dedicated to the testing of OPL programs and evaluated it on difficult instances of two well-known constraint problems, namely the Golomb ruler and car-sequencing problem. Our experimental evaluation shows that CPTEST can efficiently detect non-trivial faults in faulty versions of those two problems. A desirable extension of our framework and tool concerns its application to other more open CP plateforms.

In particular, we would like to apply our conformity relations, oracles and testing notions to GECODE or CHOCO programs as we could intervene on the core constraint solver of these systems. Developing notions of test coverage similar of those that can be found in conventional programming requires instrumenting the solver, something that was just not possible with the black-box solver of OPL.

Fig. 1 .

 1 Fig. 1. Mx(k) and Px(k) of Golomb rulers problem in OPL.

Fig. 2 .

 2 Fig. 2. Objective solutions.

  Fig.?? presents both the sets sol(M x (k)) noted M and sol x (P z (k)) noted P, where points in red x raise non-conformities (i.e., faults in the CPUT) while points in green o are conform w.r.t. the Model-Oracle. Parts (a)(b)(c) of Fig.?? exhibit non-conformities as solving P z (k) can lead to solutions which do not satisfy M x (k). Part (d) does not exhibit any non-conformity but, as P does not contain any solution, it does not conform the Model-Oracle for conf one . This example also shows that unsatisfiable models must be considered as non-conform w.r.t. Model-Oracles, in order to tackle faulty unsatisfiable CPUTs. On the contrary, part (e) of Fig.?? shows that P z (k) conforms M x (k) for conf one , as P cannot contain any non-conformity points.

Fig. 3 .

 3 Fig. 3. confone on Pz(k) and Mx(k). Whenever all the solutions are sought, another definition of conformity is useful: Definition 2 (conf all ) P conf k all M ⇔ P roj x (sol(P z (k))) = sol(M x (k)) ( = ∅) P conf all M ⇔ (∀k ∈ K, P conf k all M ) Roughly speaking, conf all asks for both set of solutions to be the same. Satisfying this conformity relation is very demanding and not always pertinent. For instance, the CPUT in part B of Fig.?? includes constraints that break symmetries of the problem (e.g., cc6), which yields to lose solutions from the Model-Oracle. As a result, those two models cannot be conform w.r.t. conf all . In Fig. ??, parts (a)(b)(c) and (d) exhibit non-conformities. Part (d) shows a solution of the Model-Oracle which is not solution of the CPUT ; therefore, the CPUT is a faulty over-constrained model. Part (c) exhibits the opposite case where the CPUT is a faulty under-constrained model. Proving that P z (k) conforms M x (k) for one of these two conformity relations is highly desirable.Unfortunately, such a proof would require not only to find all the solutions of the CPUT which is an NP-hard problem for some constraint languages (e.g., the finite domains constraint language), but also to perform this for any value of k. This seems to be intractable in general (probably undecidable) and then we will confine ourselves to the search of non-conformities within finite resources.

Fig. 4 .

 4 Fig. 4. conf all on Pz(k) and Mx(k).

Fig. 5 .

 5 Fig. 5. conf bounds on Px(k) and Mx(k).

Fig

  Fig.?? presents the conformity relation where feasible solutions of the CPUT are sought in [l , u ]. B P denotes the set Bounds f ,l ,u (P x (k)), B M denotes the set Bounds f,l,u (M x (k)) while B is the set of global minima of M x (k). Part (a) exhibits four non-conformities as these points are not feasible solutions of the Model-Oracle M x (k) in [l, u]. For the same reason, Part (b) exhibits two nonconformities as two feasible solutions of B P with cost in [l , u ] do not belong to B M . Part (c) presents also a non-conformity as B P does not contain any feasible point meaning that the minimization problem cannot find a feasible solution with cost in [l , u ]. On the contrary, part (d) shows conformity because solutions of B P belong to B M . Formaly speaking, Definition 3 (conf bounds )

Fig. 6 .

 6 Fig. 6. Testing time and solving time comparison on the Golomb rulers.

  ruler is of order m if it contains m marks, and it is of length x m . The goal is to find a ruler of order m with minimal length (minimize x m ). A declarative model of

	int m=...;	int m=...;
	dvar int+ x[1..m];	dvar int x[1..m] in 0..m*m;
	minimize x[m];	tuple indexerTuple { int i; int j;}
	subject to {	{indexerTuple} indexes={<i,j>|i,j in 1..m: i < j};
	c1: forall (i in 1..m-1)	dvar int d[indexes];
	x[i] < x[i+1];	minimize x[m];
	c2: forall (i,j,k,l in 1..m :	subject to {

Table 1 .

 1 Syntax of OPL expressions handled by CPTEST Ctrs| or( rel ) Ctrs | if( rel ) Ctrs else Ctrs | allDifferent(rel) | allMinDistance(rel) | inverse(rel)| forbiddenAssignments(rel) | allowedAssignments(rel)| pack(rel) selection conformity relation. It is also complete as it cannot report false nonconformities.

	Ctrs ::=	Ctr | Ctrs
	Ctr ::=	rel | forall( rel )

Table 2 .

 2 Faulty versions of the Golomb Ruler

	constraints of P present in the CPUT
	CPUT1 cc1, cc9
	CPUT2 cc1, cc2, cc7, cc9
	CPUT3 cc1, cc2, cc7, cc8, cc9
	CPUT4 cc1, cc2, cc3, cc4, cc6, cc7, cc8, cc9, cc10

Table 3 .

 3 Non-conformities found by CPTEST in various CPUTs of the Golomb rulers problem (timeout = 5 400s).

	m = 8	confone	conf all	conf bounds	conf best
	Non-conf points	[0 7 8 18 24 26 35 44] [17 18 20 25 34 45 49 55]	[0 2 3 6 11 58 72 86]	[0 1 3 6 10 15 24 33]
	CPUT1 T(s)	4.29s	21.45s	5.64s	7.31s
	Non-conf points	[0 4 5 26 28 31 47 63] [17 18 20 25 34 45 49 55] [0 18 39 43 45 46 55 64] [0 3 4 9 13 15 24 33]
	CPUT2 T(s)	5.62s	40.78s	4.64s	174.43s
	Non-conf points	[0 4 5 26 28 31 47 63]	[0 4 5 26 28 31 47 63]	[0 18 39 43 45 46 55 64] [0 3 4 9 13 15 24 33]
	CPUT3 T(s)	9.53s	45.78s	7.15s	389.04s
	Non-conf points [0 12 18 20 29 33 34 39] [1 2 10 22 33 55 57 60]	[0 21 30 32 42 45 46 50] [0 6 13 21 22 25 27 32]
	CPUT4 T(s)	12.60s	0.15s	9.01s	12.53s
	Non-conf points	conf	[0 7 9 12 37 54 58 64]	conf	-
	P	T(s)	3 448.46s	0.18s	3 658.13s	timeout

Table 4 .

 4 Non-conformities found by CPTEST in various CPUTs of the car sequencing problem (timeout = 5 400s).

	Confone	Conf all
	10 slots	55 slots	10 slots	55 slots

www.ilog.com/products/oplstudio/

www.dynadec.com/support/downloads/

www.g12.cs.mu.oz.au/

choco.sourceforge.net

www.gecode.org

Acknowledgment

We are very grateful to Olivier Lhomme who pointed us the problem of out-ofscope variables. Many thanks also to Michel Rueher, Laurent Granvilliers and Nicolas Beldiceanu for helpful comments on early presentations.


Mickaël Delahaye
email: mickael.delahaye@cea.fr

Bernard Botella
email: bernard.botella@cea.fr

Arnaud Gotlieb
email: arnaud.gotlieb@inria.fr

Explanation-based generalization of infeasible path

Keywords: Dynamic symbolic execution, constraint-based explanation, test input generation

Recent code-based test input generators based on dynamic symbolic execution increase path coverage by solving path condition with a constraint or an SMT solver. When the solver considers path condition produced from an infeasible path, it tries to show unsatisfiability, which is a useless timeconsuming process. In this paper, we propose a new method that takes opportunity of the detection of a single infeasible path to generalize to a (possibly infinite) family of infeasible paths, which will not have to be considered in further path conditions solving. The method exploits non-intrusive constraint-based explanations, a technique developed in Constraint Programming to explain unsatisfiability. Experimental results obtained with our prototype tool IPEG show that, whatever is the underlying constraint solving procedure (IC, Colibri and the SMT solver Z3), this approach can save considerable computational time.

I. INTRODUCTION

Recent development in automatic test input generation have seen the emergence of dynamic symbolic execution tools such as DART [START_REF] Godefroid | DART: directed automated random testing[END_REF], PathCrawler [START_REF] Williams | Pathcrawler: Automatic generation of path tests by combining static and dynamic analysis[END_REF], CUTE [START_REF] Sen | CUTE: a concolic unit testing engine for c[END_REF] or Pex [START_REF] Tillmann | Pex: White box test generation for .net[END_REF]. These tools dynamically select a feasible path by picking up a test input and observing which instructions are activated. Then, they report path condition by symbolically evaluating the instructions along this path. By refuting a decision (usually the last decision of path condition) and submitting the corresponding system to a constraint or SMT1 solver, they try to infer another test input covering a distinct path in order to increase path coverage. Whenever the path is infeasible, the tools face the problem of proving unsatisfiability, which can be timeconsuming. As the goal of dynamic symbolic execution tools is to find new test inputs instead of reporting path infeasibility, this process corresponds to a useless waste of time. One could argue that detecting all the infeasible paths of a program is impossible anyway2 but studies have pointed out that although infeasible paths are ubiquitous in program [START_REF] Yates | Reducing the effects of infeasible paths in branch testing[END_REF], finding ways to avoid useless infeasible path exploration is highly desirable [START_REF] Ngo | Heuristics-based infeasible path detection for dynamic test data generation[END_REF].

In this paper, we introduce a new technique that takes opportunity of the detection of a single infeasible path to generalize to a (possibly infinite) family of infeasible paths.

The method exploits non-intrusive constraint-based explanations, a technique developed in Constraint Programming. The underlying idea consists first in finding a minimal set of constraints explaining the unsatisfiability and second in generalizing to all the infeasible paths whose infeasibility has the same explanation. This generalizing is based on finite automata operations and approximate data flow computations that are able to capture the "essence" of infeasible paths. As a simple introductory example, consider the C program and the infeasible path of Fig. 1. Explaining the unsatisfiability leads to determine that pair (2 < x, x < 2) is a minimal (but not unique) explanation of this infeasibility. Then, by generalizing this constraint-based explanation with our method, we obtain the automaton of Fig. 2 that recognizes an infinite family of infeasible paths. Hence, any further path condition solving will benefit from this automaton to avoid trying to determine the feasibility of these paths. Our method is correct, meaning that it only generalizes to provable infeasible paths, but it is incomplete meaning that it usually cannot find all the infeasible paths. We implemented our approach in a tool called IPEG (Infeasible Path Explanation and Generalization), which can be parameterized by any satisfiability test. In our experiments, we used three constraint solving procedures that are used in symbolic-execution based test input generators: IC, Colibri and the SMT solver Z3 [START_REF] Moura | Z3: An efficient SMT solver[END_REF]. We compared IPEG against an approach that would not benefit from the automatic detection of infeasible paths on several benchmark programs. These experiments show that our approach can save considerable computational time.

The rest of the paper is organized as follows. Section II presents the indispensable background on constraint-based explanation to understand our generalization method. Section III details the explanation and generalization algorithms of the method, while Section IV evaluates the method through experiments. Section V places this work into the state of the art. Finally, Section VI concludes the paper.

II. BACKGROUND

This section first gives the notations and definitions about infeasible program paths and dependencies. Then, it introduces and reviews the notion of constraint-based explanations.

Corresponding constraints

Origin Constraint

3 t x ≥ 0 7 t y = 0 11 t (1) 2 < x 11 t (2) 3 < x 11 f (3) 4 ≥ x 13 t x < 2

A. Notations and definitions

A program path π is a sequence of successive statements (π i ) i∈{1,...,n} that can flow throughout the program. For simplicity's sake, we suppose each element of the sequence is unique by numbering multiple occurrences of the same statement when necessary. node(π i ) gives the program statement at π i without numbering. We also explicitly write for each branching statement the decision (t or f). decision(π i ) indicates the decision taken at π i if appropriate, ε otherwise. At a program statement n, maywrite(n) denotes the set of variables that may be written in n. This set is usually an overapproximation of the variable actually written in n as it is statically computed on all the program paths that led to n. A program path π is said to be infeasible if there is no program input able to execute the statements along π. Conversely, π is feasible if there is an input that can drive the computation along π .

A definition-clear path (def-clear) from statement n to statement m with respect to a set of variables V is a path that goes from n to m without modifying any variable of V .

We introduce here the notion of consistency check which is a predicate that can check the consistency, or satisfiability, of a given constraint system. It is noted Γ(C) for a constraint system C, and it can return either true, false or inconclusive. If Γ(C) = true, C is consistent, or satisfiable. If Γ(C) = false, C is inconsistent, or unsatisfiable. The latter case, Γ(C) = inconclusive, occurs when the underlying computation theory is undecidable (e.g., non-linear integer arithmetic) or when the consistency check takes too long time and has to be interrupted. For shortness' sake, in the paper, Γ-consistent (resp. Γ-inconsistent) means consistent (resp. inconsistent) according to the consistency check Γ.

The path condition of a program path π is a conjunction of constraints on the input symbolic variables of the program that characterizes π's execution. Let us note C π the path condition associated to program path π. Given a consistency check Γ, we have the following property: if C π is Γ-inconsistent, then π is infeasible and conversely if C π is Γ-consistent then π is feasible. But, there is no equivalence as the consistency check Γ can be partial.

B. Explanations

An important part in the method presented here is to determine the reason why a constraint system is inconsistent. More precisely the method needs to know what part of a constraint system is fundamentally false, that is, to find an explanation.

An explanation, or unsatisfiable core, is a subsystem of an inconsistent constraint system that is inconsistent by itself. An explanation is minimal, or irreducible, if no subsystem of the explanation is also an explanation, that is, if all parts of the explanation are essential to the inconsistency.

Formally, given a partial consistency check Γ, a Γ-minimal explanation K of a constraint set C is a subset of C such that, for all constraint c of K, Γ(K {c}) is true or inconclusive. Consequently, a Γ-minimal explanation is not necessarily minimal when Γ is partial. Also, two distinct consistency checks can lead to distinct Γ-minimal explanations.

There is at least two ways to find an explanation: first, the intrusive way, which consists in intrusively tracing back the solving process to the parts of the constraint system that lead to inconsistency; second, the non-intrusive techniques which consider the constraint system as a conjunction of individual constraints and tries to identify the ones that lead to inconsistency by successive external tests.

1) Intrusive methods: These methods extract an explanation from the constraints used by the solver's reasoning. Constraint programming tries to learn from failure since the late 70s by keeping track of nogoods. A nogood, or elimination explanation, consists of a partial assignment of variables and a subset of the considered constraint system justifying this assignment is inconsistent. More recently, Jussien et al. [START_REF] Jussien | Maintaining arcconsistency within dynamic backtracking[END_REF], adapted the recording of such elimination explanation to constraint propagation algorithms. Constraint propagation finds a constraint system unsatisfiable if any variable domain is empty. Therefore, when recorded, the conjunction of explanations for eliminating values from domain forms an explanation of the overall constraint system. For instance, consider the inconsistent constraint system x = y = z = t for x, y, z, and t in {1, 2}. Its inconsistency can be proved by the solver with the following case-based reasoning:

• x = 1 x =y ⇒ y = 2 y =z ⇒ z = 1 x =z ⇒ ⊥ • x = 2 x =y ⇒ y = 1 y =z ⇒ z = 2 x =z ⇒ ⊥
As the domain of x has been entirely explored, we get an explanation of the inconsistency of the overall constraint system. Note however that explanations obtained this way will not usually be minimal, or even Γ-minimal, because an automatic reasoning can be terribly convoluted.

2) Non-intrusive methods: The main idea of non-intrusive methods is to iteratively test the consistency of subsystems of the constraint system until a minimal explanation is found. For instance, an explanation of the above constraint system x = y = z = t, for x, y, z, and t in {1, 2}, can be found by successively checking the consistency of its subsystems: x = y, x = y ∧ x = z, etc. Here x, y, z ∈ {1, 2}, x = y = z is a minimal explanation. Note that this explanation is not unique as one could replace z by t and obtain another minimal explanation.

Several non-intrusive algorithms have been proposed but the recursive dichotomic Junker's algorithm [START_REF] Junker | QuickXplain: Conflict detection for arbitrary constraint propagation algorithms[END_REF] is considered to be the most efficient as it runs in O(n log (k + 1) + k 2 ) in the worst case instead of O(nk) where is n is the size of the constraint system and k the size of the explanation to be found.

For a partial consistency check Γ, Junker's algorithm tries to find a Γ-minimal explanation to an input constraint set. At each recursion step, the algorithm tries to identify one constraint of the explanation in a given partition, initially the input constraint set. If it is possible, the other constraints that may be involved in the inconsitency are partitioned into two groups and fed to the same algorithm. If it is not, all the constraints in the input partition are skipped. Table I presents a run of Junker's algorithm on an hypothetic inconsistent constraint system {c 1 , c 2 , c 3 , c 4 , c 5 , c 7 , c 8 } with one Γ-minimal explanation {c 4 , c 7 , c 8 }. In this table, not false actually means true or inconclusive.

Iterative methods are very susceptible to the iteration order. Partitioning allows Junker's method to counteract the phenomenon and to actually be more efficient under the hypothesis that the considered constraint set have a small explanation. Note also that Junker's algorithm does not take into account the input system is indeed inconsistent. If it can be appreciable for the outer call, it causes some superfluous tests in the inner recursive calls (e.g., Steps 12 and 20 of Table I).

TABLE I: A run of Junker's algorithm

Step Constraints Γ Explanation

1 c 1 not false ∅ 2 c 1 c 2 not false ∅ • • • 8 c 1 c 2 c 3 c 4 c 5 c 6 c 7 c 8 false {c 8 } 9 c 1 c 2 c 3 c 4 c 8 not false {c 8 } 10 c 1 c 2 c 3 c 4 c 8 c 5 not false {c 8 } • • • 12 c 1 c 2 c 3 c 4 c 8 c 5 c 6 c 7 false {c 7 , c 8 } 13 c 1 c 2 c 3 c 4 c 8 c 5 c 7 false {c 7 , c 8 } 14 c 1 c 2 c 3 c 4 c 8 c 7 false {c 7 , c 8 } 15 c 7 not false {c 7 , c 8 } 16 c 7 c 8 not false {c 7 , c 8 } 17 c 7 c 8 c 1 not false {c 7 , c 8 } • • • 20 c 7 c 8 c 1 c 2 c 3 c 4 false {c 4 , c 7 , c 8 } 21 c 7 c 8 c 1 c 2 c 4 false {c 4 , c 7 , c 8 } 22 c 7 c 8 c 4 false {c 4 , c 7 , c 8 }
In this paper, we chose to explore a non-intrusive method to compute Γ-minimal explanations in order to be as independent as possible of the constraint or SMT solver. Indeed, intrusive methods usually require intimate knowledge of and heavy modifications of the selected underlying constraint solver.

III. METHOD

This section details a complete method of infeasible path generalization. The inputs of the method consists of:

• an imperative program under test,

• a consistency check Γ,

• an infeasible path π,

• and the corresponding Γ-inconsistent path condition C π .

In addition, the method uses approximate dataflow informations with the set maywrite(n). Note that computing a tight over-approximate set maywrite(n) may be hard in the presence of arrays and pointers.

Infeasible path generalization tends to compute a set of infeasible paths defined as follows:

Definition 1. Given an explanation K of C π , the K-general infeasible path set, noted I K , is the set of every program path p such that their path condition C p includes K.

Our method approaches this goal without requiring any additional symbolic execution by constructing a deterministic finite automaton A accepting only paths p such that the path condition C p contains K, i.e., L (A) ⊂ I K .

Fig. 3 gives the general sketch of the method. It may be split into two steps:

1) Explaining the infeasibility by an Γ-minimal explanation 2) Determining a family of paths whose path condition contains this explanation

function generalize(π,C π ) K ← explain(Cπ, ∅); N ← onpath π (K); D ← pathdependencies(π); return extendpath(π, N, D); Fig. 3: Method algorithm Input: C, A two constraint sets such as C ∪ A is Γ-inconsistent Output: a minimal subset X of C such that X ∪ A is Γ-inconsistent function explain(C = {c 1 , . . . , c n }, A) i ← 0; b ← true; while b ∧ i < n -1 do i ← i + 1; b ← Γ(A ∪ {c 1 , . . . , c i }) = false; if ¬b ∧ i = n -1 then i ← i + 1; // Skips redondant check X ← {c i }; m ← ⌊(i -1)/2⌋ + 1; U ← {c 1 , . . . , c m-1 }; V ← {c m , . . . , c i-1 }; if V = ∅ ∧ Γ(A ∪U ∪ X) = false then X ← X ∪ explain(V, A ∪U ∪ X); if U = ∅ ∧ Γ(A ∪ X) = false then X ← X ∪ explain(U, A ∪ X); return X;

A. Explaining the infeasibility

The first phase consists in the line 1 of Fig. 3. The idea is that the smaller the explanation the more the chances are to find infeasible paths with the same constraints.

We propose here to use a variation of the dichotomic method of Junker [START_REF] Junker | QuickXplain: Conflict detection for arbitrary constraint propagation algorithms[END_REF] to find a Γ-minimal explanation. Fig. 4 gives the pseudocode of the function explain(C, A). This function takes two constraint sets, C and A, as inputs, such that

C ∪ A is Γ-inconsistent. This function computes a minimal subset X of C such that X ∪ A is Γ-inconsistent. That is why explain(C π , ∅) returns a Γ-minimal explanation of the Γ-inconsistent constraint system C π .
At each step, the method determines an additional constraint of the explanation. It checks iteratively the Γ-consistency of the union of the already detected constraints A and a growing subset C ′ of C. Consequently, when the consistency check fails, the last added constraint is a constraint of the Γ-minimal explanation of C ∪ A. Then, the remaining constraints of C are discarded and the constraints added to C ′ except the last one, are split in two groups U and V . Finally, the method calls itself recursively on the two groups. The returned subset contains the last added constraint and the return values of the recursive calls. Unlike Junker's, this algorithm also uses the fact C ∪ A is indeed inconsistent to skip redondant consistency checks.

In the example of Fig. 1, given a consistency check Γ, two Γ-minimal explanations can be found: (2 < x ∧ x < 2 and 3 < x ∧ x < 2). By considering the constraints in the order they are computed along the initial path, the method selects the former Γ-minimal explanation: 2 < x ∧ x < 2.

B. Determining the family

As each constraint comes from a given program statement, it is quite natural to translate the explanation expressed in terms of constraints to an expression in terms of statements.

However, it is not enough to characterize infeasible paths. Indeed, there may exist feasible paths that pass through all the statements corresponding to some explanation's constraints. Indeed, in two different paths the same instruction can be interpreted into two different ways. In the example of Fig. 1, the computed explanation 2 < x ∧ x < 2 corresponds to the control points 11 t and 13 t . Although the path 1.2.3 f .6.7 t .8.11 t .12. 11 f .13 t shared the same control points, it is not infeasible. For example, x = -3 activates this path. Indeed, the first of these two control points is interpreted in another way (2 < -x instead of 2 < x).

Translating to instructions: Function onpath π , used at line 2 in Fig. 3, keeps track of the association between constraints and statements during the symbolic execution. This function computes the actual set N of path statements corresponding to the explanation K.

Ensuring the explanation: One way to ensure that the constraints in the explanation are actually posted "as is" is to ensure the read values at the selected statements originates from the same assignments as in the input paths. We introduce the following definition to keep track of this kind of dependencies.

Definition 2. On a program path π, a path flow dependency π i v -→ π j occurs between two statements π i and π j for the variable v if:

• i > j, • π i reads v, • π j writes v,
• and there is no statement π k for i > k > j such that π k writes v; in other words, the subpath (π j+1 , ..,

π i-1 ) is a def-clear path for variable v.
This definition is special in two ways: first, the dependency is considered on a single path (that may be infeasible) and second, it is defined in the reverse order of the execution. This will simplify the presentation of the generalization algorithm.

As the set of variables read or written at a given statement cannot be known exactly in the presence of indirection (arrays, pointers), the algorithm of Fig. 3 at line 3 only computes an (over-)approximation of the path flow dependencies D on π.

In the example of Fig. 1, the path statements 11 1 and 13 can be identified as the origin of the selected explanation. Fig. 5 gives a graphical representation of the path flow dependencies related to these statements. Extending the possibilities around the path: After translating the explanation to a set N of path statements and finding the path flow dependencies, the method finds a (possibly infinite) family of paths containing N and enforcing the same path flow dependencies that the ones observed in the original infeasible path. The following definition helps clarifying this notion.

Definition 3. Given S the subset of path flow dependencies linked to N, a (K, D)-general infeasible path is a program path that contains every program statements of N and S in the same order than π and such that every subpath between these statements is def-clear w.r.t. the path flow dependencies in S.

This definition enforces that the statements N are actually interpreted exactly as they were in π. Consequently, (K, D)-general infeasible paths are guaranteed to include the explanation K in their path condition and to be infeasible.

Fig. 6 gives an algorithm to construct an automaton accepting (K, D)-general infeasible paths. This algorithm starts from the infeasible path π and adds all the possible variations that cannot affect the set of path statements N corresponding to the explanation. This algorithm uses the path dependencies D to identify these variations.

It maintains the last seen indispensable elements k, a set L of active path flow dependencies, i.e., a pair of a variable and an index in the path prefix, and δ a set of transitions. A path statement is indispensable if it belongs to N or is directly or indirectly linked to a path statement of N in the path dependency graph D. The active path dependencies L allow the algorithm to efficiently identify indispensable statements and variables whose values are important to the explanation.

Initially, k indicates the last element of the path prefix contained in N, L gives the path dependencies of this element and δ contains one transition from π k to the final state ω.

Then, it considers each element of the path prefix from the next to last:

• First, adds a transition to δ corresponding to the transition observed on the path from the previous element to this element. • Then, if the element is indispensable (that is, in N or in L for any variable), keeps it and update k and L accordingly. Otherwise, adds transitions corresponding to the alternative definition-clear paths between this node and the node at k w.r.t. the variables L, by calling extension.

Input: π an infeasible path, N the projection of the unsatisfiable core on π and D the path dependencies observed on π Output: an infeasible path automaton δ , i, f where δ is the transition set, i the initial state and f the unique accepting state Computing the extensions: Function extension(s, d,V ) computes an automaton recognizing a safe under-approximation of the paths between the source s and the destination d that do not modify any variable of the variable set V (i.e., def-clear paths). Fig. 7 gives a simple algorithm for extension(s, d,V ). First, it considers the program as an automaton from s to d and removes all statements which may write V from this automaton. Second, it trims the automaton for efficency, keeping only useful states (e.g., accessible and coaccessible). The recognized infeasible path families can also be written as a regular expression. For instance, the automaton of Fig. 2 can be translated to the following regular expression: 1.2.3 t .4.(7 t .8|7 f .10).11 t .12.(11 t .12) ⋆ .11 f .13 t .

function extendpath(π, N, D) m ← max{i|π i ∈ N} ; δ ← {π m decision(π m ) -------→ ω}; L ← {(x, j)|(π m x - → π j ) ∈ D}; k ← m; for i = m -1 à 1 do d ← decision(π i ); δ ← δ ∪ {π i d -→ π i+1 }; if π i ∈ N ∨ ∃x, (x, π i ) ∈ L then L ← {(x, j) ∈ L| j < i} ∪ {(x, j)|(π i x - → π j ) ∈ D}; k ← i; else if d = ε then let n be the statement such that node(π i ) ¬d -→ n ∈ Program, A ← extension(n, node(π k ), {x|∃ j, (x, j) ∈ L}); if L (A) = ∅ then δ ′ , s, d ← safeRenaming(A); δ ← δ ∪ δ ′ ∪ {π i ¬d -→ s, d → π k }; return δ , π 1 , ω ;

C. Correctness and completness

This infeasible path generalization method is correct, that is, it finds only infeasible paths. Indeed, one can prove the following theorem: Theorem (Correctness). For any path infeasible π (according to Γ), the method generalize(π,C π ) returns an automaton accepting only infeasible paths. Sketch of proof: After proving explain(C, ∅) computes an explanation of C (see [START_REF] Junker | QuickXplain: Conflict detection for arbitrary constraint propagation algorithms[END_REF]), it is equivalent to say that extendpath(π, N, D) returns an automaton accepting only K-general infeasible paths. First, extension(s, d,V ) computes an automaton accepting only def-clear paths for all s, d and V , because the algorithm explicity removes statements that may modify any variable of V . Then, we can show extendpath(π, N, D) returns an automaton accepting only (K, D)-general infeasible path. Finally, it remains to formally prove (K, D)-general infeasible path are indeed K-general infeasible.

However, the method presented here is not complete. Some infeasible paths may be not generalized from π, for at least the following reasons:

• It considers only one Γ-minimal explanation.

• Other statements than N may results in the same constraints. • Syntax-based dependencies are overprotective. For instance, on two distinct paths, the execution may compute differently the same value for a statement involved in the explanation K.

IV. EXPERIMENTAL EVALUATION

A. Implementation

We implemented our method in a prototype tool called IPEG. The tool can be parameterized by any constraint or SMT solving procedure and we evaluated three distincts constraint solvers:

• IC, a constraint library provided by the ECLiPSe Prolog environment. IC implements constraint propagation and labelling over finite domains for solving integer constraint systems. This library is used in the tool TestGen [START_REF] Meudec | ATGen: automatic test data generation using constraint logic programming and symbolic execution[END_REF] which generates test data for ADA programs using symbolic execution. • Colibri, a home-made constraint solver developped at the CEA which is tuned to address dynamic symbolic execution requests from at least three test data generation tools: PathCrawler [START_REF] Williams | Pathcrawler: Automatic generation of path tests by combining static and dynamic analysis[END_REF], OSMOSE [START_REF] Bardin | Structural testing of executables[END_REF] and GATEL [START_REF] Marre | Test sequences generation from lustre descriptions: Gatel[END_REF]. • Z3, the SMT solver developped at Microsoft Research [START_REF] Moura | Z3: An efficient SMT solver[END_REF] and used in the Pex automatic test data generator for .NET [START_REF] Tillmann | Pex: White box test generation for .net[END_REF]. As these solvers implement three distincts constraint solving procedures, the notion of consistency check used to compute explanation slightly differs:

• For IC, the test is based on interval-based consistency checking meaning that constraint propagation just considers the bounds of variation domains to establish partial consistency. • For Colibri, the test is also based on interval-based consistency checking apart the fact that the solver maintains an internal structure of bounded unions of intervals. In addition, the solver implements two add-ons dedicated to consistency checking based on a closure test for distance constraints and consistent congruential properties. • For Z3, the test is based on a combination of techniques from SAT-solving, closure algorithms for binary constraints, simplex-based consistency check and so on. Our prototype IPEG handles a meaningful subset of the C language, including integers, arrays, structures, control statements (conditionals, loops, switch, continue, break and goto) and most C operators, but it has also some restrictions as it currently does not support function calls, pointer variables, floating-point computations, bit-wise operators and integer overflows.

B. Benchmarks

To evaluate our method, we applied it on about two thousand paths from eight small-sized C programs extracted from classical software testing benchmarks. The function erfill takes an array and two integers as inputs and implements two related operations. First all occurences of the first integer input in the array is removed and second the free space is filled with the second integer. The program tcas is a small set of C functions that are part of the Traffic Alert and Collision Avoidance System embedded on commercial aircrafts. This program can be found in the Software-Artifact Infrastructure Repository [START_REF] Do | Supporting controlled experimentation with testing techniques: An infrastructure and its potential impact[END_REF]. The function merge takes two arrays of 5 integers as inputs and puts them in a third array of 10 integers. If both input arrays are sorted, the resulting array should be sorted as well. The function selection sorts an array of 5 integers using a classical selection algorithm. The function tritype gives the type of a triangle given the length of each side. The function gcd computes the greater common divisor of two integers. Finally, functions f1 and f2 are homemade examples based on an iterative factorial algorithm. The source code of some of these functions is given in appendix. Also, the maywrite sets were manually provided for each function.

Input infeasible paths: Our goal is to apply our method to every infeasible path that an exhaustive test input generation tool based on dynamic symbolic execution would stumble upon. We used a dedicated module of IPEG to incrementally search the program's execution tree for infeasible paths using the selected constraint solver. As these solvers implement partial consistency checks, the detected infeasible paths may vary from one solver to another. Because the execution tree may be infinite, and like most path-oriented test input generator, a generic limit is put on the number of instructions of the considered paths. For this experiment, the limit was 50 instructions, that is, no infeasible path containing more than 50 instructions was considered.

Comparison method: We compared our generalization method with an approach which would have proved the infeasibility of each path of the automaton. Let us call this method: the exhaustive method. To be fair, we used the same constraint solver in both cases. Also, as most dynamic symbolic execution tools (e.g., PathCrawler) adopt an incremental path verification, this exhaustive method also verifies path infeasibility incrementally. Consequently, if multiple paths of the automaton can be proved infeasible by a single path prefix, only the time needed to prove the infeasibibility of the prefix will be counted and that only once.

The experimental protocol was as follows. First, we seeded IPEG with the input infeasible paths. For each of them, an automaton is built that recognizes generalized infeasible paths. The time T gen needed to generate the automaton was recorded. Second, for each automaton, we used the exhaustive method to prove the infeasibility of all paths recognized by the automaton that contains 50 instructions or less. In each case, the total time T exh needed to prove their inconsistency was recorded. Although our automaton may accept infeasible paths of more than 50 instructions and in some case of any length, we chose to put this limit to stay fair with other methods and to be consistent with the considered input paths. All the computations were performed on a Linux machine equipped with an Intel Core 2 Duo P9600 processor at 2.53GHz and 2Go RAM. We used Z3 2.0, IC as provided with ECLiPSe 5.10, and the latest version of Colibri as of October 1st, 2009.

Results: Table II presents the results of our comparison in terms of number of paths explored during the experiment. For each program, the table reports the number of input infeasible paths seeded and the number of paths which have been generalized, i.e., paths from an automaton, in terms of average and maximum over the overall set of input paths.

Table III reports the results of our comparison in terms of CPU time and memory usage. The first two columns report the average CPU time required by IPEG to generalize infeasible paths for each automaton and the maximum time. The next two columns report average and maximum time to prove with the exhaustive method that each path is actually infeasible. Hence, by relating the two average values, we get in the third column the speedup our generalization method offers (> 1 is good). The four last columns of the table perform the same comparison in terms of memory usage.

Note that solver IC was incapable to prove the infeasibility of most paths in selection and tcas as the path conditions they contain lead the solver in a too long computation (they were allocated 5 seconds per path).

At first glance, Table II shows the method did generalize input paths to substantial families of infeasible paths, except for some programs (gcd and tritype). Table III gives the speedup that our generalization approach can reach in average. In most cases, the generalization is interesting, except for the few cases where the speedup slips below 1. Table III also shows the generalization uses more memory than the exhaustive approach but its memory need stays reasonable. As these results show the method is not always profitable, one important question is how do we determine when to use the method. The three following points face this problem from different angles.

First, we wanted to analyze the influence of the solver on the method. As shown in Table II, there is few differences between the input feasible paths for each solver. For instance, Z3 was able to detect shorter infeasible paths than the propagation of Colibri on tcas. Table III shows the observed speedups are better with Colibri or IC. Note however this study does not intend to compare solvers between each others. This is mostly due to the fact that the consistency check of Z3 is stronger than the propagation of Colibri and IC. Another more marginal reason is the implementation, namely a looser binding with Z3.

Second, we were interested in the type of programs that could benefit from this method. Generalization was poor in two cases (gcd and tritype) as these programs have been so studied that they do not contain any superfluous dependency anymore. Hence, generalization is harder in these cases. The results are particularly good for merge, f1, f2, selection and tcas. Indeed, merge and selection have tightly dependent loops for which the generalization finds several infeasible combinations of iterations. On the contrary, for f1 and f2 it is due to the fact that the loop does not intervene in most infeasible paths. In tcas, which is mostly a sequence of very related conditional statements, our method limits the combinatorial explosion of infeasible paths.

Third, we wanted to study the impact of the length of the input feasible path on the generalization. In fact, we remarked that the longer the input the more likely the method is advantageous. Fig. 9 shows six diagrams giving the speedup in function of the length of the input path for the three solvers and two programs (merge and erfill). These diagrams show the generalization is better in terms of CPU time when longer paths are seeded to the method. However, these diagrams also highlight the strong dispersion of the speepdup.

Finally, we tried to extend the use of the previously generated automata beyond the limit of 50 instructions. Given the previously computed automata for three programs erfill, merge and tcas, the chart of Fig. 10 gives for Colibri and Z3 the variation of the average speedup (first over the automata and then over the three programs) between the previous generalization (on input paths of less than 50 instructions) and the exhaustive method on all generalized paths of less than s instructions, in function of this bound s. This chart shows the generated automata are rarely useful to skip smaller paths, but can really be used for longer paths.

V. RELATED WORK

Using unsatisfiable core to prune a search space is not a new idea in SAT solving. Under the generic terminology of clause learning, SAT solvers exploit unsatisfiable cores to speed up the unit propagation of the DPLL algorithm. For instance, Zhang and Malik in [START_REF] Zhang | Extracting small unsatisfiable cores from unsatisfiable boolean formulas[END_REF] shown that an explanation can be computed as a by-product of a DPLL-based procedure, where the unsatisfiable core consists of all the clauses used by the DPLL solver. Note just that, unlike our approach, clause learning can be considered as an intrusive method as it requires deep interactions with the SAT solver. In the context of the automatic test data generator Pex [START_REF] Tillmann | Pex: White box test generation for .net[END_REF], the SMT solver Z3 [START_REF] Moura | Z3: An efficient SMT solver[END_REF] is used and apart from the work of Cimatti et al. [START_REF] Cimatti | A simple and flexible way of computing small unsatisfiable cores in sat modulo theories[END_REF] who proposed using external SAT-based unsatisfiable cores, we are not aware of any work consisting in computing unsatisfiable core on dedicated decision procedures of SMT solvers.

The only work in software testing that tries to generalize infeasible paths we are aware of, is the work of Ngo and Tan [START_REF] Ngo | Detecting large number of infeasible paths through recognizing their patterns[END_REF]. They propose to detect the infeasibility of a path by statically recognizing four known code patterns leading to infeasible paths. For instance, their method detects infeasible paths where two conditional statements have the same condition (e.g. if( x > y ) . . . ; if( x > y) . . . ). As the pattern recognition are sound, all the detected paths are indeed infeasible. Given 5963 paths (2276 of which are infeasible) on six Java programs (from 6 to 220 KLOC), their method recognizes 82.3% of all infeasible paths. In [START_REF] Ngo | Heuristics-based infeasible path detection for dynamic test data generation[END_REF], Ngo and Tan extended their approach to empirical properties instead of patterns to automatically detect non-feasible paths. They implemented the approach in a tool called jTGEN that was used to generate test data for Java programs. Our approach distinguishes from these works on two main points. First, our method to generalize infeasible paths is based on a sound and minimal explanation detection as it computes Γ-minimal explanation. Hence, the explanation we compute is more general than the patterns of the work of Ngo and Tan. Second, unlike their approach which has no generalization part, our generalization algorithm is built on automata operations and approximate data flow computations. Experimental comparison between our approaches is not possible as our tool IPEG is dedicated to C programs, but we are confident in the capability of IPEG to detect more infeasible paths than jTGEN.

VI. CONCLUSION In this paper, we developed a novel method to generalize infeasible paths from the detection of a single infeasible path. Our approach relies first on the computation of non-intrusive constraint-based explanation and second on automata operations and approximate data flow computations. The experimental results we obtain with a prototype tool implementation show that, whatever is the consistency check (IC, Colibri and the SMT solver Z3), our approach can save considerable time over an approach that does not make use of the generalization algorithm. Perspectives of this work include the improvement of the generalization algorithm with "semantics information" about parts of the program not related to the Γ-minimal explanation. We plan to exploit the underlying constraint or SMT solver to find improved ways to generalize the infeasibility. Another line of work concerns the usage of the automaton of infeasible paths in automatic test data generators and other applications. We plan first to integrate our tool IPEG into PathCrawler [START_REF] Williams | Pathcrawler: Automatic generation of path tests by combining static and dynamic analysis[END_REF] in order to speed up its path-oriented test data generation process and then we will study its potential usage in static analysis approaches.

  int f2(int x,int y){ int a, res, i=2;

Fig. 1 :Fig. 2 :

 12 Fig. 1: An example function and an infeasible path

Fig. 4 :

 4 Fig. 4: Dichotomic extraction of explanation

Fig. 5 :

 5 Fig. 5: Path flow dependencies linked to the path statements 11 1 and 13

Fig. 6 :Fig. 7 :

 67 Fig. 6: extendpath algorithm Input: s and d two program statements and V a set of variables Output: an automaton accepting only def-clear paths from s to d w.r.t. the variables V function extension(s, d,V ) /* Considering the program as a transition set, Program, s, d is an automaton accepting all program paths from s to d */ δ ← Program; /* Removes statements writing any variable of V */ foreach statement n do if maywrite(n) ∩V = ∅ then δ ← δ \ {a d -→ b ∈ δ |a = n ∨ b = n}; /* Keeps only accessible and coaccessible states and transitions */ return trim( δ , s, d ) Fig. 7: extension algorithm

Fig. 8 Fig. 8 :

 88 Fig.8shows the automaton generated for the infeasible path of Fig.1. As shown on Fig.8in dotted stroke, the path has been extended from 11 3 to 13, adding any number of loop

Fig. 9 :Fig. 10 :

 910 Fig. 9: Speedup in computation time in function of the input infeasible path's length

  Infeasible path 1.2.3 t .4.7 t .8.11 t .12. 11 t .12.11 f .13 t

	13	if (x < 2)
	14	res += 5;
		return res;

16

}

TABLE II :

 II Path results on the example programs

	Program	Solver	Input paths	Generalized paths
				Average	Maximum
	erfill	Colibri	211	15	148
		IC	211	15	148
		Z3	211	15	148
	f1	Colibri	440	61	240
		IC	440	61	240
		Z3	440	61	240
	f2	Colibri	58	16	30
		IC	58	16	30
		Z3	58	16	30
	gcd	Colibri	4	2	2
		IC	4	2	2
		Z3	4	2	2
	merge	Colibri	504	43	121
		IC	504	43	121
		Z3	504	43	121
	selection	Colibri	460	157	385
		IC	-	-	-
		Z3	460	157	385
	tcas	Colibri	692	230	550
		IC	-	-	-
		Z3	532	168	446
	tritype	Colibri	15	2	5
		IC	22	2	3
		Z3	15	2	5

TABLE III :

 III Time and memory results on the example programs

	Program	Solver	Gen. time (ms)	Exh. time (ms)	Speedup	Gen. MU (Kb)	Exh. MU (Kb)
			Avg.	Max.	Avg.	Max.		Avg.	Max. Avg.	Max.
	erfill	Colibri	2	7	37	399	14.8	197	550	108	142
		IC	2	7	35	374	15.0	232	610	131	173
		Z3	8	18	48	524	6.0	564	942	431	473
	f1	Colibri	3	7	229	844	77.1	199	586	92	114
		IC	3	7	224	851	80.8	229	645	112	138
		Z3	19	66	189	840	9.8	531	964	409	436
	f2	Colibri	2	3	32	61	17.2	145	235	115	115
		IC	2	7	29	58	17.0	168	273	139	139
		Z3	9	13	38	70	4.4	465	571	439	440
	gcd	Colibri	0	0	0	1	0.7	33	37	18	19
		IC	0	0	2	2	0.2	38	43	21	22
		Z3	8	9	5	8	0.6	336	340	313	315
	merge	Colibri	5	10	163	523	31.9	402	703	135	142
		IC	5	10	171	510	37.5	449	770	165	173
		Z3	9	21	175	516	18.8	774	1095	463	472
	selection	Colibri	4	7	520	1406	141.7	483	893	108	133
		IC	-	-	-	-	-	-	-	-	-
		Z3	11	66	459	1256	43.6	840	1278	429	467
	tcas	Colibri	16	23 1159	2687	74.3 1478	2308	82	93
		IC	-	-	-	-	-	-	-	-	-
		Z3	46	303	763	2035	16.6 1808	2654	423	447
	tritype	Colibri	1	3	1	4	1.3	50	213	26	37
		IC	1	3	2	5	2.2	48	82	31	41
		Z3	6	34	4	8	0.7	359	541	324	344

Satisfiability Modulo Theory

As this problem was proved undecidable in the general case[START_REF] Weyuker | The applicability of program schema results to program[END_REF]

ACKNOWLEDGMENT

We thank Bruno Marre and Benjamin Blanc for providing the Colibri solver and useful discussions about explanation, Nicky Williams for preliminary discussions on this work and Phillipe Herrmann for pertinent inputs on SMT formula formats.

APPENDIX

#define N 5 int erfill(int a [N],int e,int f) { int i, j, l; l = N; i = 0;

int a, p, i; a = (x != 0) ? 5 : 6; for (i=1; i < y; i++)