Nadjib Lazaar
email: nadjib.lazaar@inria.fr

Arnaud Gotlieb
email: arnaud.gotlieb@inria.fr

Yahia Lebbah
email: ylebbah@gmail.com

Fault localization in constraint programs

. In this paper, we enhance this framework to introduce automatic fault localization in constraint programs. Our approach is based on constraint relaxation to identify the constraint that is responsible of a given fault. CPTEST is henceforth able to automatically localize faults in optimized OPL programs. We provide empirical evidence of the effectiveness of this approach on classical benchmark problems, namely Golomb rulers, n-queens, social golfer and car sequencing.

I. INTRODUCTION

These last years have seen the explosion of high-level constraint modeling languages, including OPL [START_REF] Van Hentenryck | The OPL optimization programming language[END_REF], COMET [START_REF] Van | Constraint-Based Local Search[END_REF], ZINC [START_REF] Marriott | The design of the zinc modelling language[END_REF], or Essence [START_REF] Frisch | The design of essence: a constraint language for specifying combinatorial problems[END_REF]. In parallel, several propositions were made to use constraint programs in critical applications. For example, constraint programs were developed for e-commerce [START_REF] Holland | Robust solutions for combinatorial auctions[END_REF], air-traffic control and management [START_REF] Flener | Air-traffic complexity resolution in multi-sector planning[END_REF], [START_REF] Junker | Air traffic flow management with ilog cp optimizer[END_REF] or critical software development [START_REF] Collavizza | Cpbpv: A constraintprogramming framework for bounded program verification[END_REF], [START_REF] Gotlieb | Tcas software verification using constraint programming[END_REF]. As any other programs, constraint programs written in high-level modeling languages must be thoroughly verified before being used on real-size instances of satisfaction or optimization problems. In [START_REF] Lazaar | On testing constraint programs[END_REF], we introduced a testing framework where a first highly declarative constraint model is took as a reference to detect non-conformities within a refined and optimized constraint program solving the same problem. These non-conformities result from faults introduced during the refinement process, coming either from the absence or the bad formulation of constraints. Our testing framework was shown useful to detect non-conformities but it reveals itself poor at identifying the constraint responsible of the fault. In fact, the user resorts to explore manually one by one each of the constraints of its constraint model, which can be cumbersome even for small programs. For example, consider the N-queens problem solved by the OPL program of Fig. 1. When N = 30, using a simple declarative model of N-queens, the testing framework of [START_REF] Lazaar | On testing constraint programs[END_REF] reports a non-conformity: [30 29 28 .. .1]. Although this vector indeed solves all the constraints of Fig. 1, it shows a fault in the OPL program which obviously places many queens on the same diagonal. Therefore, at least one constraint of the model is incorrectly formulated. In this paper, we address the problem of automatically locating the constraint that is responsible of such a non-conformity. Automatic fault localization is a difficult problem, even for conventional programs. The most successful approach in the Software Engineering community is the Jones, Statsko and Harrold's algorithm [START_REF] Jones | Visualization of test information to assist fault localization[END_REF] that compares execution traces in order to guess the source code statements that are more likely to contain a fault. Their implementation called Tarantula takes both successful and unsuccessful execution traces of a sequential program as inputs, and by crossing these traces, it ranks the statements from the most suspicious to the less suspicious. The idea of the ranking algorithm is that faulty statements more frequently appear on unsuccessful traces. A related approach proposed by Cleve and Zeller aims at tracing back the causes of fault introduction [START_REF] Cleve | Locating causes of program failures[END_REF], which is the ultimate goal of fault localization. Recently, it has been shown that the Jones, Statsko and Harrold's algorithm can be rephrased by using classical data mining indicators [START_REF] Cellier | Dellis: A data mining process for fault localization[END_REF] leading to possible generalization to multi-faults localization. These approaches are well suited for sequential programs as the control flow is data-driven, i.e., any execution trace depends on the values of input variables. However, they are not suited for constraint programs as the control flow is constraint-driven in this case, i.e., the order on which constraints are considered by the language interpreter is usually not determined by input values. In other words, comparing traces on distinct instances does not help to localize faults. A trend in constraint program debugging has been to analyze a single trace via generic trace models [START_REF] Deransart | Analysis and Visualization Tools for Constraint Programming, Constrain Debugging[END_REF], [START_REF] Langevine | Prototyping clp(fd) tracers: a trace model and an experimental validation environment[END_REF]. In the context of the OADymPPaC 1 project, several post-mortem trace analyzers such as Codeine for Prolog and Morphine [START_REF] Langevine | Prototyping clp(fd) tracers: a trace model and an experimental validation environment[END_REF] for Mercury, ILOG Gentra4CP, and JPalm/JChoco have been developed. All these tools can help the developer to understand and optimize his constraint program, but they are not dedicated to automatic fault localization. Following the Shapiro's algorithmic debugging approach, the user still has to query the trace and user interaction during the debugging process is mandatory.

In this paper, we introduce a fault localization approach that is fully automated for OPL programs. This approach is based on systematic constraint relaxation by making use of the ILOG CP constraint solver. The idea is to solve auxiliary constraint programs built over the OPL constraint program under test and the reference model used to specify the problem. We provide an algorithm that takes the faulty constraint program and a non-conformity as inputs and returns either a single constraint or a set of constraints that are responsible of the fault. For example, in the OPL program of Fig. 1, our algorithm reports constraint d as responsible of the given non-conformity. Looking at constraint d permits to spot that operator =< should be replaced by !=. We present our implementation called CPTEST enabling automatic fault localization. We provide empirical evidence on classical benchmark problems, namely golomb rulers, n-queens, social golfer and car sequencing that our approach is not only applicable but also efficient to localize faults in OPL programs.

The rest of the paper is organized as follows: Section II gives an overview of the constraint programs testing framework of [START_REF] Lazaar | On testing constraint programs[END_REF] and introduces some notations. Section III presents our automatic fault localization algorithm. Section IV presents CPTEST and the empirical results we got on n-queens, golomb rulers, social golfers and car sequencing. Section V concludes this paper and draws some perspectives to this work.

II. BACKGROUND

CP aims at solving satisfaction or optimization problems. When one faces a problem specification, one usually writes down a first declarative constraint model that faithfully represents the problem. We have high confidence in this model but playing with it rapidly shows that it cannot solve large instances of the problem. Then, this model is refined using classical techniques such as constraint reformulation, redundant and surrogate constraint addition, global constraint replacement, or static symmetry-breaking constraints. This refinement leads to have an optimized constraint model tuned to address difficult instances. We think that most of the faults are introduced in this refinement step. In our previous work [START_REF] Lazaar | On testing constraint programs[END_REF], we introduced a testing framework taking the first declarative model as an oracle for detecting non-conformities in the optimized model. We defined various formal conformity relations handling the cases where a single solution is found, all the solutions are found or a cost function has to be optimized.

A. Notations

In this section, we briefly give the necessary notations to understand the rest of the paper. M denotes the initial declarative model called the Model-Oracle and P denotes the Constraint Program Under Test (CPUT). Sol(M ) (resp. sol(P )) denotes the set of solutions of the model-oracle (resp. CPUT) where M possesses at least one solution(sol(M ) = ∅). Considering unsatisfiable model-oracles could be interesting for some applications but we excluded these cases in order to avoid considering equivalence of unsatisfiable models. The difference of two sets E and

F is noted E\F {x/(x ∈ E) ∧ (x / ∈ F )}.
The general conformity relation between the model-oracle M and the CPUT P is given by the following definition:

Definition 1 (conf ):

P conf M ⇔ sol(P ) = ∅ ∧ sol(P ) ⊆ sol(M )

B. Non-conformity detection

As proving conformity on any instance of a problem is undecidable in the general case, we have proposed in [START_REF] Lazaar | On testing constraint programs[END_REF], test algorithms aiming at detecting non-conformities. For a given instance, a non-conformity is either a solution of the CPUT P that is not a solution of the model-oracle M , or P is reduced to fail (i.e., sol(P ) = ∅). Systematic non-conformities detection can be performed by combining the negation of a constraint of the model-oracle with the constraints of P (i.e., P ∧ ¬C i where C i ∈ M ). Badly formulating a constraint in P can remove and/or add solutions.

III. FAULT LOCALIZATION

Once a non-conformity is detected, one faces the problem of localizing the faulty constraint. The major requirement on which our approach is based is the single fault hypothesis, i.e., there is only one constraint that is faulty in P . This requirement might appear as being restrictive but it has been shown that complex faults usually result from the coupling of single faults (a.k.a. the coupling effect [START_REF] Jones | Visualization of test information to assist fault localization[END_REF]). In other words, faults that come from the interaction of several constraints are less likely to appear than single faulty constraint. Therefore, in our approach, when a non-conformity is found, we suppose that the CPUT P misses a single constraint or has only one faulty constraint in it. • Part(a) exhibits a set of non-conformities (i.e., solutions of P but not of M ) where P shares solutions with M (i.e., sol(M )∩sol(P ) = ∅). P is faulty as it contains C 3 a badly formulated constraint such that sol(P )\sol(M ) = ∅. In fact, after having localized C 3 , this model could be corrected as shown in part(a'). • Part(b) exhibits another set of non-conformities where sol(P )\sol(M ) = ∅ and sol(M ) ∩ sol(P ) = ∅. In this example, we have

A. Intuitions

       sol(M ) ∩ sol(C 1 ) ∩ sol(C 2 ) = ∅ sol(M ) ∩ sol(C 1 ) ∩ sol(C 3 ) = ∅ sol(M ) ∩ sol(C 2 ) ∩ sol(C 3 ) = ∅
hence, the faulty constraint can be localized as being C 3 .

Part(b') shows a possible correction of P by revising C 3 . • Part(c) exhibits a case where P is unsatisfiable. Here again, we have

       sol(M ) ∩ sol(C 1 ) ∩ sol(C 2 ) = ∅ sol(M ) ∩ sol(C 1 ) ∩ sol(C 3 ) = ∅ sol(M ) ∩ sol(C 2 ) ∩ sol(C 3 ) = ∅
hence C 3 is localized as the faulty constraint and should be revised as proposed in part(c'). • Finally, Part(d) shows a case where P is unsatisfiable but differs from the previous one as

       sol(M ) ∩ sol(C 1 ) ∩ sol(C 2 ) = ∅ ⇒ C 3 may be faulty sol(M ) ∩ sol(C 1 ) ∩ sol(C 3 ) = ∅ ⇒ C 2 may be faulty sol(M ) ∩ sol(C 2 ) ∩ sol(C 3 ) = ∅ ⇒ C 1 may be faulty
In this case, the faulty constraint cannot be localized and the set {C 1 , C 2 , C 3 } is returned as an overapproximation. In part(d'), we chose C 3 as a possible correction. There are three distinct cases when considering nonconformities within P w.r.t. M : if C' is a faulty version of a given constraint C, then C' can either removes actual solutions (such as in part(a) in Fig. 3), either add "new solutions" (part(b) in Fig. 3) or both (part(c) in Fig. 3).

B. The fault localization process

Our fault localization process is based on the following definitions and property. Formally speaking, given a CPUT P formed of {C 1 , C 2 , ...C n } constraints that are not conform w.r.t. its Model-Oracle M , then we introduce the notion of suspicious constraint as follows:

Definition 2 (Suspicious constraint):

C i is suspicious in P w.r.t. M ≡ M ∧ {C 1 , C 2 ..., C i-1 , C i+1 ...C n } is satisfiable.
P does not conform M iff either P is unsatisfiable or there exists a non-conformity test case nc such as nc ∈ sol(P )\sol(M ). Our fault localization process aims at reporting the set of suspicious constraints: Definition 3 (SuspiciousSet): SuspiciousSet(P ) ≡ {C ∈ P : C is suspicious in P w.r.t. M } In the example of Fig. 2, the fault localization process will return Suspicious(P ) = {C 1 , C 2 , C 3 } for part(a) and part(d) as no one of these three constraints may be faulty while it will return singleton {C 3 } for both part(b) and part(c), showing that the faulty constraint is actually C 3 . Note that, by construction, the set Suspicious(P ) is the smallest set containing all the suspicious constraints and then the overapproximation provided by this approach is also the more precise.

C. Algorithm

Based on the previous definitions, we propose an algorithm called locate that automatically localize suspicious constraints in P . Algo.1 takes as inputs the Model-Oracle M , the CPUT P and a non-conformity nc that has been automatically detected by other means [START_REF] Lazaar | On testing constraint programs[END_REF]. The special case where P is unsatisfiable and then there is no nc is handled by a special tag. This algorithm returns SuspiciousSet(P ) noted rev({C 1 , .., C m }) that may be a singleton in the most favorable case or all the constraints of P in the worst case. The algorithm returns also a second set addSet for the special case where all the constraints of P are suspicious, and a nonconformity point nc exists. In this case, nc satisfies P , but does not satisfy some single constraint in M , according to the testing process [START_REF] Lazaar | On testing constraint programs[END_REF]. The checking algorithm computes addSet, the subset of M constraints that does not satisfy nc: some of these constraints could be caught in P in order to eliminate this non-conformity point. end for 25: end if

D. Correctness and completeness

Providing that the underlying constraint solver is correct and complete, Algo.1 is correct as it will necessary return the faulty constraint within SuspiciousSet(P ). As sol(M ∧P \{C i }) = ∅ is a sufficient condition for assessing that C i is actually a faulty constraint and Algo.1 loops on all the constraints, no suspicious constraint can be missed. But, this condition is not necessary as, by hypothesis, only a single constraint is faulty. Thus, algo.1 is not complete and can return an over-approximation under the form of a set of suspicious constraints. Roughly speaking, algo.1 can return false alarms even in the case where a correct version of P is submitted for fault localization. Note also that Algo.1 can return all the constraints of P making the fault localization totally useless. Hopefully, case is not frequent as it requires the conjunction of many unlikely events such as shown in Fig. 4. In this example, there are three constraints where each pair of constraints shares common solutions.

IV. EXPERIMENTS

All our experiments were performed on Intel Core2 Duo CPU 2.40Ghz machine with 2.00 GB of RAM and all the models we used to perform these experiments are available online at (www.irisa.fr/celtique/lazaar/CPTEST).

A. CPTEST

In this section, we give a brief overview of CPTEST, a first testing framework for constraint programs written on Fig. 4: Pathologic case OPL. CPTEST includes a complete OPL parser and a backend process that produces dedicated OPL programs as output that have to be solved to detect and localize faults. The tool implements a process to detect fault and Algo.1 to localize this fault. CPTEST is based on ILOG CP optimizer 2.1.

The objective of our current experiment was to check that CPTEST can automatically detect and localize fault, using standard a fault injection process [START_REF] Clark | Fault injection[END_REF]. Then, we fed CPTEST with faulty CPUTs of four well-known CP problems, namely n-queens, social golfer, golomb rulers and car sequencing problems and we tried to localize faults by working on several instances from the easiest to the hardest.

B. n-queens problem

The problem of placing n queens on an n × n chessboard is a classical problem where the model-oracle can be given by three constraints (noted m_ct1,m_ct2 and m_ct3), the first one insures that all queens are placed differently on their column, the second and the third constraint insure that no two queens are placed on the same upper or lower-diagonal on the chessboard. We improved this model by adding new data structures, redundant, surrogate and global constraints. We have produced 7 different faulty CPUTs (P1 to P7) 2 for n-queens using fault injection.

Tab.I shows the results given by CPTEST on each faulty n-queens CPUT (n = 8). It shows the number of constraints and where fault was injected (e.g. p5_ct3 for P5), P6 and P7 are messing a part of n-queens specification where the fault injected respectively in p6_ct3 and p7_ct1 leads the CPUTs to accept new solutions. (part(b) Fig. 3).

Tab.I shows also the non-conformity detected after the testing phase, the results of localization phase and its time consumption. P1, P2, P3 and P4 have no solution (sol(P i) = ∅) where the fault injected reduces them to fail. For instance let us take P3, the fault injected in is as follows: CPTEST returns (rev(p3_ct11),∅) , here the set of suspicious constraint is the singleton p3_ct11 the faulty constraint that has to be revised. The faults are localized for the four first programs in few seconds by pointing each time the faulty constraint that has to be revised.

The fault injected in P5 leads it to have bad n-queens solutions, testing phase highlights this non-conformity ([1 5 1 1 4 8 8 4]). For localization phase, CPTEST points the faulty constraint in less than a second and returns p5_ct3 to be revised.

For P6 and P7 the fault is that, respectively, p6_ct3 and p7_ct1 do not catch a part of n-queens specification. The two CPUTs accept consequently new solutions. CPTEST detects non-conformities that are bad solutions revealing faults in P6 and P7. For localization, let us take P6, CPTEST returns (rev(P6),(m_ct2,m_ct3)) , in less than five seconds. The set of suspicious constraint is here equals to P6, CPTEST returns also a set of M constraints (m_ct2, m_ct3) that should be considered in P6.

C. Social golfer problem

Social golfer is one of the famous problems in the CSPLib (prob010). We have m social golfers, n weeks and k groups of l size. Each golfer plays once a week in groups of l golfers. The problem is to build a schedule of play for all golfers over the n weeks such that no golfer plays in the same group as any other golfer more than one time.

The model-oracle can be built by two constraints ( m_ct1 and m_ct2 ), the first one to specify that each group has exactly l golfers (group size). The second one to say that each pair of golfers meets only at most once.

The model-oracle can after be improved using static symmetry breaking. The symmetry can be broken by selective assignment. We get a model with five constraints, we inject

P 1) = ∅ P2 5 p2_ct2 nc1 P3 5 p3_ct3 sol(P 3) = ∅ P4 5 p4_ct4 sol(P 4) = ∅ P5 5 p5_ct5 sol(P 5) = ∅ non-conformity nc1= [[1 1 1 1][1 2 2 2][1 3 3 3] [2 1 3 3][2 2 2 1][2 2 1 1][3 3 3 2][3 1 1 2][3 3 2 3]]

Localization

social golfer fault localized time P1

(rev(p1_ct1),∅)

1.04s P2 (rev(P2), ( m_ct2
)) 0.18s P3 (rev(p3_ct3),∅) 1.05s P4 (rev(p4_ct4,p4_ct5),∅) 1.03s P5 (rev(p5_ct5),∅) 1.15s
in each constraint a fault to get at the end five faulty CPUTs (P1 to P5). We launch CPTEST on these faulty CPUTs to first detect fault and after localize them. We take an instance of the problem with 9 golfers (3 groups of 3 golfers) playing during 4 weeks.

Tab.II shows the results given by CPTEST on each faulty CPUT. The fault injected in P1, P3 and P5 are respectively on p1_ct1 , p3_ct3 and p5_ct5 . These faults reduce the solution space to empty for the three CPUTs, so there are non-conform to the model-oracle. For instance, let us take P5, the fault in p5_ct5 is: p5_ct5: forall (g in 1..golfers, w in 1..weeks: w >= 2 && g <= groupSize ) assign[g,w] == g; turned to p5_ct5: forall (g in 1..golfers, w in 1..weeks: w >= 2 && g <= groupSize ) assign[g,g] == w;

CPTEST localizes the fault (in 1s) and returns the singleton p5_ct5 the constraint to be revised.

The fault injected in p2_ct2 leads P2 to accept new solutions. In this case, P2 can return bad solutions. CPTEST detects one of them by testing, nc1 is a non-conformity (a bad solution of social golfer) where golfer 3 and golfer 4 play in the same group (group3) over 2 weeks (3rd and 4th week). CPTEST returns (rev(P2),(m_ct2)) that the developer has to reformulate a constraint in P2 to catch (m_ct2) the second constraint of the model-oracle.

P4 is a case where CPTEST returns a set of suspicious constraint. The fault is injected in p4_ct4 and CPTEST returns (p4_ct4, p4_ct5) an over-approximation of constraints. The two constraints in P4 break symmetries. Let us imagine that the search space SR can be divided in two symmetric sets: SR ≡ S 1 ∪ S 2 where p4_ct5 removes S 2 . p4_ct4 divides S 1 in two symmetric sets (S 1 ≡ S 3 ∪ S 4 ) and removes S 4 . By adding the two constraints, the search space is reduced to S 3 . The fault injected to p4_ct4 removes S 1 where p4_ct5 removes S 2 , in this case the search space is reduced to empty and either p4_ct4 or p4_ct5 can be revised.

D. Golomb rulers

A Golomb ruler is a set of m marks ( 0 = x 1 < x 2 ... < x m ) where the m(m -1)/2 distances {x j -x i |1 ≤ i < j ≤ m} are distinct. A ruler is of order m and its length is x m . The objective is to find an optimal ruler (minimal length) of order m. A first declarative model (model-oracle) includes two constraints. m_ct1 to order the marks and m_ct2 to have different distances between these marks.

We improve this model using different techniques, the use of new data structure (e.g. d for distances), the addition of a global constraint (allDifferent(d)), the addition of surrogate and redundant constraints. We also break symmetry by adding specific constraints. We obtain at the end 7 faulty CPUT by fault injection.

We take a small instance of Golomb rulers (m = 4). We launch CPTEST on these faulty CPUTs where Tab.III shows the results. The three first CPUTs accept new solutions where the fault injected is of type part(b) Fig. 3. For each of these three CPUTs a non-conformity is reached. For example, if we take P2, CPTEST returns after testing [0 1 6 11] that is a bad Golomb ruler where 6-1=11-6. CPTEST returns after localization (rev(P2),(m_ct2)), here P2 has to catch the second constraint of the model-oracle by reformulating one of its constraints. P4 and P5 are also non-conform to the model-oracle where sol(P i) = ∅. The faults are respectively in p4_ct5 and p5_ct1. Let us take P4 to show the injected fault: CPTEST returns a singleton as suspecious constraints set for P4 and P5 (resp. p4_ct5 and p5_ct1) in a reasonable time consumption.

P6 have a bad formulation on p6_ct2 and CPTEST returns a non-conformity. For localization, CPTEST returns m_ct2 to be caught in P6.

On P7, we injected one fault at p7_ct9 ( = turned to =). This fault reduces sol(P 7) to empty. CPTEST returns two suspicious constraints (p7_ct6 and p7_ct9). This is due to the interference created by the injected fault between the faulty p7_ct9 and p7_ct6 where the two constraints are dedicated to a static symmetry breaking.

E. Car sequencing

Car sequencing is an interesting CP problem that tries to find an assembly line of cars for a car-production company where cars are grouped on classes. Each class represents cars with some specific options. The assembly line must satisfy some option capacity constraints.

The model-oracle of car sequencing is taken from the OPL book [START_REF] Van Hentenryck | The OPL optimization programming language[END_REF]. The model-oracle is composed of two constraints (m_ct1 and m_ct2). The first one expresses demand constraints for how many cars of a given class have to be produced. The second one expresses capacity constraints of the form l outof u for: Each sub-sequence of u cars, a unit can produce at most l cars with a given option.

We improve the original model and we follow the same approach as for the precedent problems by injecting faults. We have at the end 7 faulty CPUTs.

We took an instance of the problem with an assembly line of 10 cars, 6 classes and 5 options. Tab.IV shows the results of CPTEST for fault detection and localization on car sequencing problem. The three first CPUTs (P1, P2 and P3) have the same characteristics that accept new solutions and are non-conform to the model-oracle, the faults are injected respectively in p1_ct2, p2_ct3 and p3_ct2. CPTEST returns a nonconformity point for the three first CPUTs (resp. slots1, slots2 and slots3) that are bad assembly lines. To localize faults, CPTEST returns all constraints as an overapproximation. It proposes a model-oracle constraint m_ct2 to be caught in the CPUTs. P4, P5 and P6 have a faulty constraint (resp. p4_ct2, p5_ct1 and p6_ct6). The faults injected in these CPUTs reduce the set of solutions to empty and CPTEST detects this non-conformity. If we take P5, the fault injected is a bad formulation as: This constraint is returned by CPTEST ((rev(ct1),∅) in 1.29s.

In P7, the fault is injected in p7_ct5 where P7 is nonconform to the model-oracle. CPTEST returns in localization a set of suspicious constraints (p7_ct5, p7_ct6).

V. CONCLUSION

In this paper, we introduced a novel approach for automatic fault localization in constraint programs. According to our knowledge, this is the first time an approach that is not based on post-mortem trace analysis is proposed: the advantage being that our approach does not require any user interaction. We enhanced CPTEST, our CP testing framework for OPL programs, with automatic fault localization. And we got empirical evidence that shows our approach is efficient to localize fault in OPL programs. The experimental evaluation was performed on classical benchmarks such as Golomb rulers, n-queens, social golfers and car sequencing. In many cases, CPTEST can localize exactly the constraint responsible of a reported non-conformity efficiently. In a few cases, several constraints are proposed among which the faulty constraint is necessarily included. However, our approach is currently built on the hypothesis that a single constraint is responsible of the nonconformity which is a limitation. Further work includes the removal of this limitation as well as the extension of CPTEST to automatic correction of faulty constraints.

Fig. 1 :

 1 Fig. 1: N-queens problem in OPL.

  1 http://contraintes.inria.fr/OADymPPaC/

Fig. 2 :

 2 Fig. 2: Fault localization cases.

Fig. 2

 2 Fig.2 depicts four distinct cases where the CPUT P does not conform the model oracle M (P ¬conf M ), i.e., there is a solution of P and not of M (part (a, b)) or sol(P ) = ∅ (part (c, d)), where P is a conjunction of three constraints C 1 ∧ C 2 ∧ C 3 . In Fig.2, P is represented by the intersection of the three constraints and possible corrections are shown in blue.

Fig. 3 :

 3 Fig. 3: Faulty constraint.

Algorithm 1

 1 locate(M, P, nc) 1: set ← ∅ 2: addSet ← ∅ 3: for each C i ∈ P do 4: if sol(M ∧ P \{C i }) = ∅ then 5: set ← set ∪ {C i } 6: end if 7: end for 8: if (set = P ) ∧ (nc = ∅) then 9: addSet ← checking(M, nc) 10: end if 11: return (rev(set), addSet) checking(B, nc): 15: if B = ∅ then 16: return ∅ 17: else 18: for each C i ∈ B do 19: if nc |= C i then 20: return checking(M \{C i }, nc) 21: else 22:return {C i }∪ checking(M \{C i }, nc)

  p3_ct11: sum(i in Domain) queens[i]==(n * (n+1)/2); turned to p3_ct11: sum(i in Domain) queens[i]==(n+(n+1)/2);

  p4_ct5: allDifferent(all(ind in indexes ) d[ind]); turned to p4_ct5: forall(i in m..2 * m) count(all(j in indexes) d[j],i)==1;

  p5_ct1: forall(i in Cars) sum(j in Slots) ((slot[j]==i) * (one[j]))==demandV[i];turned to p5_ct1: pack(slot, slot, one);

TABLE I :

 I Fault detection and localization of n-queens problem

		8-queens	#	fault	non-conformity
			consts.	injected	detected
		P1	12	p1_ct11	sol(P 1) = ∅
	Test	P2 P3	12 12	p2_ct12 p3_ct11	sol(P 2) = ∅ sol(P 3) = ∅
		P4	12	p4_ct12	sol(P 4) = ∅
		P5	5	p5_ct3	q1
		P6	3	p6_ct3	q2
		P7	2	p7_ct1	q3
	non-conformity		q1= [1 5 1 1 4 8 8 4]
		q2= [7 8 3 2 4 1 5 6], q3= [8 4 3 6 5 7 2 1]
		8-queens		fault localized	time
	Localization	P1 P2 P3 P4 P5	(rev(p1_ct11),∅) (rev(p2_ct12),∅) (rev(p3_ct11),∅) (rev(p4_ct12),∅) (rev(p5_ct3),∅)	2.09s 1.64s 1.57s 1.59s 0.62s
		P6	(rev(P6), (m_ct2,m_ct3))	4.12s
		P7	(rev(P7), (m_ct2,m_ct3))	3.01s

TABLE II :

 II Fault detection and localization of social golfer problem

		social	#	fault	non-conformity
		golfer	constrs.	injected	detected
	Test	P1	5	p1_ct1	sol(

TABLE III :

 III Fault detection and localization of Golomb rulers problem

		Golomb	#	fault	non-conformity
		rulers	consts	injected	detected
		P1	2	p1_ct2	[0 1 3 6]
	Test	P2 P3	4 5	p2_ct3 p3_ct3	[0 1 6 11] [0 5 6 11]
		P4	9	p4_ct5	sol(P 4) = ∅
		P5	9	p5_ct1	sol(P 5) = ∅
		P6	9	p6_ct2	[0 1 6 11]
		P7	9	p7_ct9	sol(P 7) = ∅
		Golomb rulers		fault localized	time
	Localization	P1 P2 P3 P4 P5	(rev(P1), (m_ct2)) (rev(P2), (m_ct2)) (rev(P3), (m_ct2)) (rev(p4_ct5),∅) (rev(p5_ct1),∅)	0.32s 0.82s 1.15s 1.87s 1.62s
		P6	(rev(P6), (m_ct2))	2.14s
		P7	(rev(p7_ct6,p7_ct9),∅)	1.92s

TABLE IV :

 IV Fault detection and localization of car sequencing problem

		car	# constraints	fault	non-conformity
		sequencing		injected	detected
		P1	2	p1_ct2	slots1
	Test	P2 P3	3 3	p2_ct3 p3_ct2	slots2 slots3
		P4	3	p4_ct2	sol(P 4) = ∅
		P5	6	p5_ct1	sol(P 5) = ∅
		P6	6	p6_ct6	sol(P 6) = ∅
		P7	6	p7_ct5	sol(P 7) = ∅
			slots1= [4 5 3 6 4 6 5 1 3 2]
			slots2= [4 6 3 1 5 2 3 5 4 6]
			slots3= [5 2 3 6 1 4 3 6 4 5]
		cSeq	fault localized	time
	Localization	P1 P2 P3 P4 P5	(rev(P1), (m_ct2)) (rev(P2), (m_ct2)) (rev(P3), (m_ct2)) (rev(p4_ct2),∅) (rev(p5_ct1),∅)	0.46s 0.23s 0.67s 0.87s 1.29s
		P6	(rev(p6_ct6),∅)	1.34s
		P7	(rev(p7_ct5, p7_ct6),∅)	1.28s

We recall that all models and CPUTs are available on (www.irisa.fr/celtique/lazaar/CPTEST).


Florence Charreteur
email: florence.charreteur@irisa.fr

Arnaud Gotlieb
email: arnaud.gotlieb@irisa.fr

Constraint-based test input generation for java bytecode

In this paper, we introduce a constraint-based reasoning approach to automatically generate test input for Java bytecode programs. Our goal-oriented method aims at building an input state of the Java Virtual Machine (JVM) that can drive program execution towards a given location within the bytecode. An innovative aspect of the method is the definition of a constraint model for each bytecode that allows backward exploration of the bytecode program, and permits to solve complex constraints over the memory shape (e.g., p == p.next enforces the creation of a cyclic data structure referenced by p). We implemented this constraint-based approach in a prototype tool called JAUT, that can generate input states for programs written in a subset of JVM including integers and references, dynamic-allocated structures, objects inheritance and polymorphism by virtual method call, conditional and backward jumps. Experimental results show that JAUT generate test input for executing locations not reached by other state-of-the-art code-based test input generators such as jCUTE, JTEST and Pex.

I. INTRODUCTION

As integrated within current development environments, automatic test input generation is a promising approach for reducing the cost of software unit testing. In particular, having an approach able to generate and check 100% code coverage of a unit under test is highly desirable for increasing our confidence in the program correctness. However, current realistic solutions for this problem do not achieve complete coverage of usual structural criteria such as all statements or all branches. In fact, modern automatic test input generators adequately sacrifice completeness for efficiency. They are able to generate test inputs for programs containing hundreds of thousands lines of code in a couple of minutes but they fail to generate complete statement coverage on simple Java methods that contain cyclic data structures, multi-level dereference aliasing problems, inter-dependent loop statements or non-linear decisions.

Although the underlying reachability problem is undecidable in the general case, it seems that there is room for code-based test input generators applying more costly methods and having the goal of completeness. Constraint-based testing, as introduced by Offutt in 1991 [START_REF] Demillo | Constraint-based automatic test data generation[END_REF], combined symbolic execution and dynamic constraint solving [START_REF] Offut | The dynamic domain reduction procedure for test data generation[END_REF] to generate test inputs able to execute specific paths in the code. It was then adapted for C programs and refined with standard constraint programming techniques to target specific locations in the code regardless of the particular path executed [START_REF] Gotlieb | Automatic test data generation using constraint solving techniques[END_REF], [START_REF] Gotlieb | Goal-oriented test data generation for pointer programs[END_REF]. Constraint-based testing was extended to the exhaustive generation of structured inputs for Java programs [START_REF] Marinov | Testera: A novel framework for automated testing of java programs[END_REF], [START_REF] Boyapati | Korat: automated testing based on java predicates[END_REF] and the constraint solving of structurally complex constraints [START_REF] Elkarablieh | Efficient solving of structural constraints[END_REF]. An important work in the area is also the symbolic execution approach of Java PathFinder [START_REF] Visser | Test input generation in java pathfinder[END_REF] where "lazy initialization" was proposed [START_REF] Pasareanu | A survey of new trends in symbolic execution for software testing and analysis[END_REF].

Recent code-based test input generators 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 and jCUTE [START_REF] Sen | Cute: a concolic unit testing engine for c[END_REF], [START_REF] Sen | Cute and jcute: Concolic unit testing and explicit path model-checking tools[END_REF] or Pex [START_REF] Tillmann | Pex: White box test generation for .net[END_REF] are based on dynamic symbolic execution. They dynamically select a feasible path by picking up a test input and by observing which instructions are executed ; then, they report path conditions by symbolically evaluating the instructions along the path. Finally, by negating the last decision of path conditions and submitting the corresponding system to a constraint or an SMT1 solver, they try to infer another test input covering a distinct path. When such a test input is found, path coverage of the program is necessarily increased. Whenever path conditions are unsatisfiable, the process backtracks and selects another path to execute. Dynamic symbolic execution performs forward exploration as it visits the paths from the entry to the exit and this works fine for quickly exploring a few paths. However, when the goal is to complement an existing test set in order to increase code or branch coverage, this approach is less adapted as forward exploration can be trapped in large subspaces of the path search space. In this paper, we introduce a new constraint-based approach to generate automatically test inputs for Java bytecode programs. Our approach generates a test input under the form of a concrete state of a JVM memory, that can drive the program execution towards a selected bytecode instruction. In the context of unit testing, our approach is made to improve the statements coverage of each method under test thanks to a contextfree test case generation. This paper contains two contributions:

1) unlike other approaches [START_REF] Godefroid | Dart: directed automated random testing[END_REF], [START_REF] Sen | Cute: a concolic unit testing engine for c[END_REF], [START_REF] Williams | Pathcrawler: Automatic generation of path tests by combining static and dynamic analysis[END_REF], [START_REF] Cadar | Exe: automatically generating inputs of death[END_REF], [START_REF] Tillmann | Pex: White box test generation for .net[END_REF], our framework explores program paths from the target location towards the program entry point. Backward exploration at the bytecode level is not trivial as it requires the development of a kind of inverse reasoning on each bytecode instruction, that is neither available in the SUN's JVM specifications nor in the literature. For that, we developed constraint reasoning on partial abstract memory states. For backward exploration, we also developed a depth-first strategy which takes advantage of early detection of infeasible parts of paths to prune the search space of feasible paths ; 2) a new constraint-based model of the JVM is defined with the notion of constrained memory variable. This notion captures abstract memory states and permits to implement deductive rules for a meaningful subset of Java bytecode, including those dealing with objects, inheritance, polymorphism and dynamic memory management. In this model, each bytecode expresses a relation between two constrained memory variables, which contain unknown or only partially known variables associated to registers, operands stack or heap.

Using constraint propagation and an existing finite domain constraint solver, this model allows decisions that involve cyclic data structures and reference aliasing problems such as if( p == p.next ) to be effectively solved. We implemented our approach in a tool called JAUT (Java Automatic Unit Testing) that can generate input memory states for reaching specific locations within Java bytecode programs. Experimental results on small-sized benchmark programs, including the TreeMap Java library of red-black trees, show that JAUT2 can complement an existing test set with test inputs for locations not covered by other code-based test input generators such as jCUTE [START_REF] Sen | Cute: a concolic unit testing engine for c[END_REF], [START_REF] Sen | Cute and jcute: Concolic unit testing and explicit path model-checking tools[END_REF], JTEST [START_REF] Grehan | Jtest continues its trek toward code-testing supremacy[END_REF] and Pex [START_REF] Tillmann | Pex: White box test generation for .net[END_REF].

The rest of the paper is organized as follows: section 2 introduces our method on a simple example, section 3 presents the memory model we defined to generate test inputs for the JVM, section 4 explains constraint generation and constraint solving for a few bytecodes, section 5 presents the test input generation process which performs backward search across Java bytecode programs, section 6 is dedicated to our experimental validation and discussion of related work, while section 7 concludes and draws perspectives to this work. Consider the Java program of Fig. 1 that implements the class Coord standing for the Cartesian coordinates in a 2D-space. We selected this simple example just to illustrate the memory model of our constraint-based test input generation approach. Let our test objective be the generation of an input JVM state for method moveY that reaches the bytecode corresponding to the instruction i in the source code. Note that we do not pay attention to how the methods of class Coord can build such an input state that may be "invalid" if it cannot be reached from other method calls. Objectoriented languages offer ways to directly manipulate the object receiver state without using constructors and accessors (e.g., using Java reflection with setAccessible or bytecode translation) and nothing can guarantee, without additional information, that a given method will not be called from an "invalid input state". Hence testing a program with states that may be invalid is equally important.

II. DETAILED EXAMPLE

The bytecode program shown in Fig. 2 corresponds to method moveY where bytecode 51 corresponds to the selected test objective. Our memory model is based on the notion of constrained memory variables (CMV) which capture JVM states. It contains abstract information on the registers, the operand stack and the heap of the JVM, which can be used to fill in a test script for the method under test.

Our prototype tool JAUT manipulates CMVs and can output, at any moment of the constraint solving process, an excerpt of the CMV associated to moveY input JVM state: Before launching the constraint solving process, the CMV containing the input parameters lin and the heap hin is automatically generated. lin contains two references (this and chrono) and an integer (speed). The object referenced by this has already been created on the heap (noted 0::), as invoking method moveY requires a Coord object being created. this refers to this object as its domain contains a single address (dom=[0]). On the contrary, chrono does not reference any object for the moment as it can still be null or points to any object of the heap (dom=all). ndom denotes a set of impossible adresses for a heap reference. Note that references (0, 1 and so on) do not reflect any physical counterpart, as our model is abstract and not designed for bytecode execution. Integer variables such as speed, this.x and this.y, that are 32-bits integers in the Java bytecode program, currently have type intFD, with domain3 [-268435456..268435455].

lin: this -<[Coord], dom=[0] ndom=[]>, chrono-<[Chrono],
The constraint generation and solving process of our test input generation method aims at refining this input CMV for method moveY by finding values for each variable. We illustrate this process below by showing how this input CMV is successively refined to satisfy the test objective.

Our constraint solving examines each bytecode one by one in a backward fashion. On this program, there is no choice point on the backward exploration as there is only a single path going towards the program entry point. Constraint solving operates with two interleaved processes: constraint propagation which uses each constraint to prune the domain of CMV of their inconstistent values and labeling, which enumerates the possible values of CMV and launches constraint propagation until no more deduction is possible. Those processes are not new and form the basis of finite domain constraint solving [START_REF] Marriott | Programming with Constraints : An Introduction[END_REF]. Let us just recall that all the constraints are added to a constraint propagation queue that iteratively manages each constraint one by one, and each constraint is used to prune the variation domain of its variables. At a given step of the constraint solving process, the following input CMV is produced: The ndom set of reference chrono has increased to [null, 0], meaning that chrono can neither be null nor points to the object pointed by this. These deductions come from the fact that 1) reaching location 51 in the bytecode program requires a nonnull value for chrono as it is dereferenced several times and 2) chrono has to point to a Chrono object and not a Coord object. The domain of speed has been pruned during initial constraint propagation as constraint speed > 0 was considered.

lin: this -<[Coord], dom=[0] ndom=[]>, chrono-<[Chrono], dom=all ndom=[null,0]>, speed -< intFD, [ 1
Next steps include the creation of object Chrono and the start of the labeling process for producing a completely instantiated CMV, suitable for test script generation. Suppose that the labeling process has instantiated speed to 363 and this.y to 5206 using a random labeling heuristic, then we get the following refined input CMV: This CMV characterizes an input JVM state that satisfies the test objective of reaching bytecode numbered 51 in method moveY. Submitting a test script derived from this state shows that the fault on the converted parameters of new Coord(ytemp, x) can be detected.

lin: this -<[Coord], dom=[0] ndom=[]>, chrono-<[Chrono], dom=[1] ndom=[]>, speed -< intFD, [ 363

III. MEMORY MODEL

Java virtual machine states represent runtime data storage locations such as registers 4 , operand stacks and heap data. This section details the representation of data types and data storage locations in our memory model. Note that our framework handles a meaningful subset of Java bytecodes, including integers and references, dynamic allocation and heap-allocated structures, objects inheritance and polymorphism, static and dynamic method invocations, conditional jumps and backward jumps. Arrays accesses and updates are only partially supported and floating-point computations, exceptions, native methods and multithreading are currently left apart.

A. Constraint memory variable

In our memory model, constrained memory variables (CMV) are used to represent JVM states. A CMV contains data storage locations where data can be represented by variables along with a domain. Formally, a CMV M is a tuple (F, S, H) where F denotes the set of registers, S denotes the operand stack and H denotes the heap. Note that several distinct CMV M can be created at the same instruction number when loops are present in the bytecode. Each Java bytecode will then be seen as a relation among two CMVs: the CMV Mj before activation of bytecode and the CMV M k after its activation and before the activation of the following bytecode in the considered sequance of instructions. The tuple (F, S, H) contains variables and domains that are described in the rest of the section.

B. Integer and reference variables

Finite domain variables model integer and reference variables of the program. Their default variation domain depends on the size of their precise type. For instance, the domain -2 31 ..2 31 -1 is associated to an int variable. Other integer types are treated accordingly. The default domain of a reference is the all symbolic value. This means that the reference can point to every object of the heap. When the solving process prunes the domain of the reference variable, then the domain is composed of a set of integer values, which represent all the heap addresses the reference can point to. Note that the null value can also be part of the domain.

C. Objects

Each object of the heap is modeled by a pair of elements. The first one, called type variable, represents the class of the object, the domain of which is a set of possible classes. This allows to properly handle inheritance and polymorphism. The second element is a mapping associating an integer or a reference variable to each attribute, which corresponds to the value of the attribute. Note that when the domain of the type variable contains more than one class, all the possible attributes have to be in the mapping.

For example, if a program defines two classes A and B where B inherits from A, and A defines attribute t1 and B defines attribute t2, then

([A,B],[t1-<intFD,[2..5]>,t2-<intFD,[15..17]>])
represents an object of class either A or B, with attribute t1 necessarily in 2..5. If the object happens to be of class B during the solving process, then its t2 attribute will belong to 15..17.

D. Registers and operand stack

In a JVM state, registers are used to store the parameters and the local variables of a method. When the method is dynamic (as opposed to static methods), the first register contains the reference to the object (this) that calls the method. The operand stack is used to perform the calculations of the method. In a CMV, we use two sequences of variables to represent registers and operand stack. As registers are numbered, the first sequence is a convenient way of implementing an indexed array. On the contrary, the sequence used for representing operand stack is accessed with stack operations. Its first element is considered as its top.

E. Heap

In a CMV, the JVM's heap corresponds to a mapping from a set of addresses to a set of objects, possibly stored at these addresses. We associated a unique integer to each address without taking into consideration the actual physical addresses in the JVM. The domain of a variable H that models the heap is composed of a set of pairs, representing the mapping, and a status. 1) The set of pairs (address,object), denoted by CH , contains the objects necessarily present in the heap. During the solving process, new pairs can be added to CH when a dynamic memory allocation bytecode is encountered (i.e., new). As our model does not model garbage collection, CH can only be enriched, reducing the possible states of the heap. 2) The status is either closed or unclosed. A closed status of the heap denotes a set of addresses entirely known, even if some objects can still be unknown or only partially known through their domain. On the contrary, an unclosed status denotes states where memory allocation can still enrich the CMV. During the constraint solving process, status can only move from unclosed to closed. This notion is introduced to tackle cases where the input memory shape is unknown and we will have to explore the input space during labelling to find it.

IV. CONSTRAINT GENERATION AND SOLVING

In our framework, constraint generation and solving are performed altogether. This has similarities with the on-the-fly generation of paths of [START_REF] Williams | Pathcrawler: Automatic generation of path tests by combining static and dynamic analysis[END_REF] and [START_REF] Tillmann | Pex: White box test generation for .net[END_REF] where path conditions are incrementally tested for satisfiability. We first detail the specification of test objective (Sec. IV-A), and then we present the constraint generation and solving process (Sec. IV-B). We illustrate the constraint generation on an example (Sec. IV-C) and we explain the deduction capabilities of the constraints we have defined to model dynamic memory management (Sec. IV-D).

A. Test objective

Test input generation aims at finding an input CMV that satisfies a given test objective in a Java bytecode method. In our framework, test objectives are specified with the bytecode instruction number that corresponds to a bytecode program location. In general, for a given test objective, there are many feasible or infeasible paths that can reach the target locations. Our goal is just to find one input CMV that will drive the computation towards the selected location, whatever is the feasible path executed. Note that such a test objective potentially specifies an infinite set of dynamic locations when the bytecode instruction number is located within loops.

B. Constraint generation from the bytecode

Initially, the input CMV of the method is an unconstrained variable and the constraint generation process will accumulate and solve the constraints, for the current selected path, from the test objective to the program entry point. These constraints capture the pah condition that must be satisfied to follow the current selected path and are used to prune the possible values of the input CMV. Each bytecode can potentially constrain the input CMV variable or intermediate CMV variables, throughout its behavior on the registers, operand stack or heap variables. Based on the semantics of each bytecode as defined in the SUN's specification, we build constraints that implement deductive rules on the CMVs.

Arithmetic bytecodes such as iadd, ladd, isub, imul, idiv, irem, ineg,... and comparison bytecodes if_icmp, if_acmp, lcmp, ..., act directly on logical variables associated with integers or references, and the elements of the operand stack. They generate arithmetical constraints on the finite domain constraint solver, depending on the type of the operands and the operator. For example, iadd generates a relation V temp = V a + V b over two CMVs M 1 and M 2, where V temp is a fresh finite domain variable associated to the top of the operand stack of M 2, while V a and V b are the two finite domain variable associated with the integers on the top of the stack of M 1. Other arithmetic bytecodes generate similar constraints according to the considered integer type (int or long) and operator. Comparison bytecodes are handled in a similar way by considering the arithmetic constraint extracted from the condition or from the negation of the condition. This will be made clearer in section V.

Bytecodes for simple constant pool accesses (ldc, bipush, ...) or register accesses iload, aload, iload_<n>, aload_<n>, ... or register updates istore, astore, istore_<n>, astore_<n>, ..., generate equality constraints between the top of the operand stack and registers, depending on the type of the register variable. Equality on reference variables (when aload or astore is considered) generates a finite domain equality, as well.

To deal with bytecodes for dynamic memory management new, newarray, ... and accesses and updates of object fields getfield, putfield, ..., special constraints have to be built. Indeed, these operations maintain complex relations between the CMVs. They can constrain the shapes of heap-allocated data structures and the contents of registers and operand stack. We detail the relations we built for only three of them, as the other can easily be deduced from these ones: new(class, H0, H1, A) maintains the relation between H0 the heap of the CMV before execution and H1 the CMV after execution, and A a fresh address for the newly created object of type class. The relation says that H1 is the updated heap H0 where reference A points to a newly allocated object. getfield(A, Id, H, V al) maintains the relation between the heap H, from which an access to an attribute Id of the object designated by reference A is performed and V al a finite domain variable. When reference A has for domain a set of possible references, special deductions can be performed on the possible values for V al. Conversely, using the possible values of V al, special deductions on reference A can be performed. In addition, information on the domains of variables in H allows for deductions on the domains of A and V al. This permits the implementation of powerful forward and backward constraint reasoning. putf ield(A, Id, V al, H0, H1) is more complex as it maintains a relation between H0 and H1 the heaps of both CMVs, reference A and V al. H1 is similar to H0 except for object referenced by A where the field Id has been modified to value V al. Possible deductions with this relation are illustrated below. Bytecodes for arrays manipulation baload, iaload, iastore, ... and method invocations invokespecial, invokevirtual, invokestatic are taken into account but they are not described here as we considered they were outside the scope of the paper.

C. Example

From the moveY method of Fig. 2 and the test objective which consists to reach bytecode numbered 51, we get the following constraint system (omitting some details about the calls to constructors). For this example, Mi denotes the memory state before the bytecode instruction number i.

{ F 1 = T his.Chrono.Speed.Y temp, T his = null M51 = (F 1, S1, H1), M48 = (F 1, X.Y.A1.S1, H2), invokespecial(Coord, init, [A1, Y, X], H2, H1), M45 = (F 1, A2.Y.A1.S1, H2), A2 = null, getf ield(A2, x, H2, X) M44 = (F 1, Y.A1.S1, H2), A2 = this, M43 = (F 1, A1.S1, H2), Y = Y temp, M42 = (F 1, A1.S2, H2), S1 = A1.S2, M39 = (F 1, S2, H3), A = null, new(Coord, H3, H2, A1), M38 = (F 2, Y temp.S2, H3), F2 = T his.Chrono.Speed.Y temp2, M36 = (F 2, S2, H3), Y temp = 65536, M33 = (F 2, V al1.V al2.S2, H3), V al2 > V al1, M31 = (F 2, V al2.S2, H3), V al1 = 65636, M30 = (F 2, S2, H3), V al2 = Y temp2, M27 = (F 2, V al3.A3.S2, H4), A3 = null, putf ield(A3, time, V al3, H4, H3), M26 = (F 2, A3.S2, H4), V al3 = 0, M25 = (F 2, S2, H4), A3 = Chrono, M24 = (F 3, Y temp2.S2, H4), F3 = T his.Chrono.Speed.Y temp3, M23 = (F 3, V al4.V al5.S2, H4), Y temp2 = V al4 + V al5, M22 = (F 3, V al6.V al7.V al5.S2, H4), V al4 = V al6 * V al7, M21 = (F 3, V al7.V al5.S2, H4), V al6 = Speed, M18 = (F 3, A4.V al5.S2, H4), A4 = null, getf ield(A4, time, H4, V al7), M17 = (F 3, V al5.S2, H4), A4 = Chrono, M14 = (F 3, A5.S2, H4), A5 = null, getf ield(A5, y, H4, V al5), M13 = (F 3, S2, H4), A5 = T his, M8 = (F 3, V al8.S2, H4), V al8 > 0, M7 = (F 3, S2, H4), V al8 = Speed, M4 = (F 3, V al9.S2, H4), V al9 > 0, M1 = (F 3, A6.S2, H4), A6 = null, getf ield(A6, time, H4, V al9), M0 = (F 3, S2, H4), A6 = Chrono, S2 = }
is the empty sequence, while v.s denotes the stack s where v is pushed. The elements of the sequence F 2 represent the parameters and the local variables at the bytecode instruction 51. Instruction 48 calls a constructor and links both CMVs M48 and M51. The elements on the top of the stack before instruction are the parameters Y and X as well as the reference A1 to the object that calls the method. The heaps H2 and H1 are linked by the constructor call effect, represented here by a relation invokespecial.

The top of the stack before the instruction getfield 45 is a reference A2, while the top of stack X after the instruction is the value of the attribute x of the object referenced by A3 in the heap H1. The relation is maintained by a constraint getfield(A3, x, H2, X). The instruction 39 allocates memory to store a new object of type Coord. The relation new(Coord, H3, H2, A1) states that the heap H2 contains one added object of type Coord. A1 is pushed on top of the stack after the instruction. As the only instruction that permits to reach 51 after the conditional instruction 33 is 36, then the top of the stack A.B before the instruction 33 constrains B to be greater than A. The top of the stack before the instruction 27 contains the value V al3 and the reference A4. The instruction putf ield updates the value of the attribute time with the value V al3, for the object referenced by A3. H4 is the heap before the instruction while H3 is the heap after instruction and the constraint putf ield(A3, time, V al3, H4, H3) maintains this relation. Finally, the values of the registers F 3, and the heap H4, of the memory M0, describe a possible test input to reach our test objective 51.

D. Possible deductions with operator putfield

In order to illustrate the behavior of a complex constraint, we show the possible deductions by putf ield on a simple example. Consider the heap and suppose that status of H0 is unclosed and status of H1 is closed. Using the relation putf ield(A, t1, V al, H0, H1), several deductions can be performed. 1) As the relation operates on attribute t1, one deduces that dom(A) = all -{3} as object 3 has only attribute t3 and its class b does not inherit from a. Consequently, the following equalities can be added V 2 = V 7, V 4 = V 9 and V 5 = V 10 as the relation does not modify variables associated with the attributes t2 and t3 . 2)Considering variables V 3 and V 8, we see that dom(V 3) ∩ dom(V 8) = ∅ then one deduces that A refers necessarily to object 2 in the heaps H0 and H1: A = 2. Consequently, V 1 = V 6 is added as the object at the address 1 is not modified and V 8 = V al leading to 3) Finally, the closed status of H1 is propagated to H0 as putf ield does not add any new object on the heap. So, all the addresses of both heaps are known.

H0 = {(1, (a, [t1 → V 1, t2 → V 2])), (2, (a, [t1 → V 3, t2 → V 4])), (3, (b, [t3 → V 5]))} and the heap H1 = {(1, (a, [t1 → V 6, t2 → V 7])), (2, (a, [t1 → V 8, t2 → V 9]), ( 3

V. TEST INPUT GENERATION

A. Backward search

Backward search relies on constraint block accumulation and solving. A constraint block in a bytecode program is a set of instructions that is submitted to constraint propagation. The test objective specifies a bytecode to reach, which corresponds to a specific constraint block. So, starting from this block, backward search incrementally accumulates other constraint blocks by trying to find a path towards the program entry point. It is worth noticing that constraint consistency is tested on the fly, each time a new constraint block is added to the constraint system. This permits to quickly detect infeasible parts of program paths. These subpaths should not be confounded with path prefix as they do not begin by the method entry point. When a constraint block has several parent blocks in the control-flow graph, then a choice point is created. Each choice is then explored in a depth-first search until one of them gets to the program entry point. If a choice is shown as being incoherent with the rest of the constraint system, then the process backtracks to the first ancestor choice point and takes an alternative. The strategy gives priorities to shortest intraprocedural subpaths towards the program entry points (i.e., in presence of loops, targeting exit loop constraint blocks). Note however that a parameter has to be set to prevent the process from iterating without terminating in presence of loops.

Let us illustrate why backward search can be interesting w.r.t. forward exploration on the simple example of Fig. 3, where the test objective is to reach constraint block g. Suppose also that block e and block g contain contradictory conditions. For example, e contains assignment i = 1 while condition to go from block e to block g is i > 2. Starting from block g, backward search will first explore subpath ge by positioning a choice point. As constraint consistency is tested on the fly, the process fails and backtracks to the choice point without exploring the other backward paths starting by ge. Subpath gfa -... is then considered without failing. Constraint inconsistency detection is possible as our framework can reason both in a forward and backward manner, thanks to the use of contraint programming to express relations between CMV. Moreover, our framework implements a precise memory model able to deal with partially known memory states. On this example, forward exploration such as implemented in several dynamic symbolic execution tools would have first considered abceg and failed. Then, backtracking at point b, depthfirst forward exploration would have considered abdeg and failed again before finding afg. To be fair, similar poor behavior can be found for backward exploration as well just by considering incoherent subpaths near the program entry point. We are not saying that backward exploration is better than forward, we just say that both approaches complement each other. Our backward search approach is useful to complement an existing test set by looking at not-covered locations.

B. Test input labeling

When a set of consistent constraint blocks has been found to flow backward from the test objective to the program entry point, every variable of the input CMV has not necessarily been instantiated. A labeling step on the input CMV has then to be launched in order to complement the CMV. The process is recursive and tries to select the best option at each step. It starts by labeling the input formal parameters of the method under test. For references, it first tries null, then it tries the addresses of objects in the heap that have compatible type and finally, upon failure, it creates a new object that has a compatible type. Each time a value is assigned to a variable from its domain, the constraints that operate on this variable are awaked and constraint propagation is relaunched. This process can efficiently prune the domain of other variables. When all the input parameter values are fixed, the values of the object attributes have to be labeled in order to build a complete CMV. The process labels first the object attributes that are reachable from the parameters with a single dereferencing level. If the corresponding input state satisfies the test objective, then we get a solution of the problem. On the contrary, upon failure, the process backtracks and the dereferencing level is increased until a given bound, defined by the user. The status is also labeled to the "closed" value in order to indicate that no more object can be added to the input memory state. When the labeling process is finished, then either a complete input CMV is found that reaches the test objective or a failure is reported. Failure may be provoked by several causes, including unreachable test objective, bounds on backward search or dereferencing level, or timeout. Hence, the method is incomplete but note that it can find input cyclic data structures when necessary.

VI. EXPERIMENTAL VALIDATION

A. Implementation

Our prototype tool JAUT (Java Automatic Unit Tesing) takes as inputs a bytecode program given under textual form, obtained with SUN's command javap which decompiles the binary bytecode, and a test objective composed of the method name and bytecode instruction number. It reports as output an input CMV, excerpts of which have been presented in Sec. 2 of the paper. JAUT includes 1) a bytecode analysis module that generates a prolog-based internal structure that can be efficiently explored with backtracks and unification ; 2) a backward search module which is parameterized by: a bound on the number of times certain branches are executed, a bound on the length of paths to be explored, a bound on the dereferencing level and a timeout ; 3) a constraint solver which implements constraint generation and deduction rules for the constraints associated with bytecodes. The constraint solver implements its own constraint propagation queue and its own memory labeling strategy, but it calls the SICStus Prolog clpfd library for solving arithmetical constraints.

JAUT handles a meaningful subset of bytecodes, as discussed earlier, but as a research prototype tool, it handles only about a third of the one hundred or so bytecodes of the SUN's JVM specification. Bytecodes that were left apart include bytecodes for integer conversions and low-level shifting, bytecodes for floatingpoint computations. Note that, for each bytecode, a specific constraint model was developed and deduction rules that captures the operational semantics of the JVM were implemented.

B. Experiments

All the results were computed on a standard single-core machine: an Intel Pentium, 2.16GHZ machine running Windows XP with 2.0GB of RAM. Our experiments aimed at evaluating the capabilities of JAUT to complement an existing test set, obtained by another forward path-exploration test data generator. We selected three such white-box test data generation tools: jCUTE, JTEST version 8.0 and Pex version 0.15.40714.1. Pex is dedicated to .NET but the programs considered in our experiments can easily be compiled to .NET bytecodes 5 Other available test data generators are discussed in the related work section. The goal of the experimental settings was to evaluate the capabilities of JAUT to cover instructions not covered by the three test input generators jCUTE, JTEST and Pex.

Simple programs are used in our experiments: versions of the classical trityp and josephus programs in bytecodes, methods of the DoublyLinkedList and TreeMap Java classes. Trityp has many infeasible paths while josephus [START_REF] Charreteur | Modelling dynamic memory management in constraint-based testing[END_REF] manages a cyclic dynamic data structure. We also considered a modified version of this program, called josephus/m, where the hard-to-reach decision ndeEnd.key==41 && nde.key==31 is inserted at the end of the program. The DoublyLinkedList class also implements dynamic data structures management and contains input object references and method calls in its code. The TreeMap class implements red-black trees which are cyclic structures. The source code of these programs, the source code of JAUT, as well as all the test drivers used for Pex and jCUTE can be found online at www.irisa.fr/lande/gotlieb/resources/jaut.html. In all the programs, private fields have been turned into public ones in order, for the three tools, to equally generate valid and invalid input states. For the depth-first backward exploration of JAUT, a bound of 150 bytecodes on the length of path and a bound of 10 for the maximum dereferecing level have been set.

In addition, we considered the following program (in bytecodes) that illustrates a problem related to forward exploration: static int a=1; 5 In our results, difference of the .NET runtime cost vs. JVM runtime have been considered neglectible.

public static int foo(int i){ int j = 10 ; while (i > 1){ j++; i--; } if (j > 50 * a) return 1; // test objective I return 0; } Reaching the test objective I implicitely constrains the number of iterations within the loop. On this example, forward exploration will unroll the loop without taking into account the test objective. The parameter a can be increased to study the scaling effect of the underlying problem.

C. Results and analysis

On the foo program, both JTEST and Pex fail to reach the test objective I. Unlike these tools, jCUTE covers every instructions of the foo method, including instruction I, but it takes 10.9sec of CPU time. JAUT also generated an input CMV (corresponding to i = 42) that reaches I in 0.15sec of CPU time. Its backward exploration strategy is useful on this example.

We studied the behavior of both jCUTE and JAUT on the foo example by increasing the value of a. Fig. 4 shows the results of this experiment. The time required by jCUTE increases dramatically on this example as the tool requires an increasing number of trials to satisfy this hard-to-reach test objective. As jCUTE compiles and executes programs to perform dynamic symbolic execution, the CPU time increases accordingly. The JAUT approach is better on this example as constraints are directly handled in the constraint solver and backtracking is hard-coded in Prolog. For other experiments, results are shown in Fig. 5 where #Bc is the number of bytecode instructions, #To is the number of test objectives. We report the results of jCUTE, Pex, and JAUT to get complete bytecode instructions coverage and the results of JAUT to complement the test sets produced by Pex. The fourth tool JTEST reveals itself too poor on this task. In fact, its test input generation strategy is based on the analysis of constants in the program, which prevents many symbolic decisions to be covered. jCUTE and Pex have the primary goal of covering all the feasible paths of the program while JAUT is designed to reach a single instruction in the program. Hence, none of these three tools is optimized to efficiently get complete bytecode instruction coverage. However, in all the cases, there are claims on their to reach instruction coverage. For JAUT, instruction coverage can be automatically reached by launching incrementally requests on not-covered instructions in a script. For the three tools, we report coverage percentage, which we have computed ourselves on a common basis. Indeed, Pex reports dynamic bytecode coverage which does not necessarily correspond to bytecode instruction coverage. So, we computed the coverage by looking at the covered portions of code, rather than taking into account the numbers provided by the tools. We selected two search modes for jCUTE: the former corresponds to depth-first search on the execution tree (both columns noted jCUTE) while the second corresponds to random path exploration (both columns noted jCUTEr). We measured the CPU time required by JAUT to complement the test set generated by Pex (column compl. JAUT) when it was incomplete. When this measure was unnecessary, n/a was reported.

For the trityp method, experiments show that, unlike jCUTE in both versions, Pex and JAUT succeed to get complete coverage. However, the CPU time required to get this result for JAUT is very long (almost one hour). Indeed, SICStus Prolog needs a long time to demonstrate the insatisfiability of some path condition, as i + j > k, j k > i, i + j > k, j = k, i = k, i = j, k = 0, j = 0, i = 0 where i, j, k denote three 32-bit integers, because it requires long-term labeling. Note that another approach would be to use dedicated SMT solver such as Z3 [START_REF] De Moura | Z3: An efficient smt solver[END_REF] in JAUT to avoid these problems.

Program josephus in both versions is hard to cover. The program computes first a dynamic cyclic chain in function of input parameters and then it eliminates one by one the elements by cycling around the chain. Satisfying all the test objectives require unrolling each of the loops 40 times which is not easy to deduce from code analysis only. On this example, Pex obtains very good results by generating 19 test cases while other tools, including JAUT, fail to get complete coverage. Our analysis of the JAUT failure indicates that our depth-first backward search is trapped by the second loop and that it should be refined. This leaves room for improvments.

For the DoublyLinkedList class, the three tools succeed to generate complete test sets but JAUT obtains the best CPU time results. Upon analysis of the results for the add method, we saw that backward exploration is useful on this example, as forward search requires many paths to be explored. To be fair, it is worth noticing that Pex also tries to cover paths of the called methods while JAUT only considers test objectives within the method under test. In addition jCUTE and Pex also generate test scripts during test input generation, while JAUT do not perform similar generation. On short periods of time, this can have an non-neglectible impact on the results. We did not implement this feature in JAUT as our primary goal was only to demonstrate the interest of fine-grain memory model and backward exploration in constraint-based test input generation.

For the TreeMap class, both coverage and CPU time results with JAUT outperform the results of other tools, including Pex. On the rotateLeft method, both versions of jCUTE obtained only 20% of bytecode coverage while Pex obtained 88.9%. In fact, covering all the instructions of the method requires explicit solving of the decision if(p == p.left.parent) in a certain context, which corresponds to a complex pointer aliasing relation. Note that the time required by JAUT to complement the test set of Pex when covering this decision is very low: 0.05sec. This shows that such decision does not require heavy constraint solving effort. The results obtained for method fixAfterInsertion are the most interesting. Both modes of jCUTE cover only about 20% of the method while Pex covers about 45%. The CPU times required to get these results is rather long for jCUTEr and Pex (resp. 28.30 and 120.00sec). On the contrary, JAUT covers 100% of the method in 22.18sec. When used to complement the Pex test set, it takes 15.49sec, showing that not-covered bytecode instructions are indeed hard to reach. So, JAUT performs well on the methods of the TreeMap class as it contains many hard test input generation problems. We interpret this result as a confirmation that using a precise memory model, which in particular deals with reference aliasing, is advantageous for completing an existing test set.

D. Related work

Test input generation at the Bytecode level. JAUT performs constraint-based test input generation from Java bytecode. Therefore, it is mainly related to JPF [START_REF] Visser | Test input generation in java pathfinder[END_REF], jCUTE [START_REF] Sen | Cute: a concolic unit testing engine for c[END_REF], [START_REF] Sen | Cute and jcute: Concolic unit testing and explicit path model-checking tools[END_REF], and Pex [START_REF] Tillmann | Pex: White box test generation for .net[END_REF]. Unlike these three tools, JAUT implements backward exploration, meaning that it starts from a target bytecode location and incrementally discovers a feasible path towards the entry. Indeed, JPF, jCUTE and Pex are based on forward symbolic execution which consists to evaluate symbolically the instructions along a path in the same order as execution. Improvements on the search strategy of Pex have been proposed [START_REF] Xie | Fitnessguided path exploration in dynamic symbolic execution[END_REF] to leverage some of the problems of forward exploration. Note that backward symbolic execution exists for a long time [START_REF] Muchnick | Program Flow Analysis: Theory and Applications -Chapter 9[END_REF], but our approach extends and generalizes this idea to programs containing references on the stack and the heap, as well possibly cyclic dynamic data structures. Reasonning backward at the bytecode level requires a precise memory model to be defined. Our memory model has similarities with those of JPF [START_REF] Visser | Test input generation in java pathfinder[END_REF], [START_REF] Pasareanu | A survey of new trends in symbolic execution for software testing and analysis[END_REF] in that it also implements a form of "lazy initialization". In our approach, decisions such if( p.next == p ) constrains two variables to be equal and non null without instantiating them. Unlike lazy initialization which makes choices during constraint solving, JAUT reports the choice to the labeling phase. Our memory model also has similarities with the constraint-based models of CUTE [START_REF] Sen | Cute: a concolic unit testing engine for c[END_REF] and Pex [START_REF] Tillmann | Pex: White box test generation for .net[END_REF] that can deal with symbolic pointer equalities and inequalities, dynamic memory allocation and input data structures. We argued below that JAUT can complement an existing test set produced by one of these tools by applying more costly analysis for specific unreached locations within the bytecode. In fact, the constraint-based reasoning step of JAUT defines precise relations between two CMVs (constraint memory variables) for each bytecode. Of course, the scope of JAUT is currently too restricted (a meaningful subset of JVM bytecodes) to compete with the industrial development of Pex, but we believe that both approaches could complement each other in the long term. Test input generation for binary programs. OSMOSE [START_REF] Bardin | Structural testing of executables[END_REF] and SAGE [START_REF] Elkarablieh | Precise pointer reasoning for dynamic test generation[END_REF] both implement forward dynamic symbolic execution for binary programs. They handle dynamic jumps and use an untyped memory model able to deal with pointer arithmetic, type casting and multiple dereferencing levels. SAGE builds path conditions that are submitted to the SMT solver Z3 [START_REF] De Moura | Z3: An efficient smt solver[END_REF]. Unlike SAGE [START_REF] Elkarablieh | Precise pointer reasoning for dynamic test generation[END_REF], JAUT is based on a constraint propagation and labeling solver. Such solvers are used with success in the context of combinatorial optimization problems as they can solve linear as well as non-linear problems over the reals or the integers. Variable multiplication or divisions are typical examples of non-linear constraints that are efficiently handled by these solvers. Another advantage of constraint propagation relies on its flexibility to add new userdefined constraints. For JAUT, we built several constraint operators that apply deduction rules to reason over the memory shapes. These operators captures both forward and backward exploration at the same time and propagates domain reductions without instantiating any variable or equality. However, using a SMT-solver such as Z3 [START_REF] De Moura | Z3: An efficient smt solver[END_REF] to solve arithmetical constraints over fixed-length integer variables would be very interesting to replace clpfd in JAUT. Note also that test input generation for binary programs is harder than at the bytecode level as the control flow cannot easily be recovered and variable types are unknown which makes the building of constrained input memory states more complex.

Test input generation from C and Java source code. There are many approaches of automatic test input generation from source code. In our previous works [START_REF] Gotlieb | Goal-oriented test data generation for pointer programs[END_REF], [START_REF] Charreteur | Modelling dynamic memory management in constraint-based testing[END_REF], we built memory models for constraint-based test data generator of C programs. Our previous model handled pointers toward named locations of the memory and dynamically allocated structures but they were limited in their scope. Unlike JAUT, the model of [START_REF] Gotlieb | Goal-oriented test data generation for pointer programs[END_REF] did not contain representation of the heap and then it was unable to deal with dynamic memory allocation. The model of [START_REF] Charreteur | Modelling dynamic memory management in constraint-based testing[END_REF] was very complex and the generation took too much time. Furthermore, in these preliminary memory models, backward exploration has not been implemented. PathCrawler [START_REF] Williams | Pathcrawler: Automatic generation of path tests by combining static and dynamic analysis[END_REF], DART [START_REF] Godefroid | Dart: directed automated random testing[END_REF], CUTE [START_REF] Sen | Cute: a concolic unit testing engine for c[END_REF] implement dynamic symbolic execution for C source code. On the contrary, JAUT implements static backward exploration These two approaches complement each other as dynamic symbolic execution rapidely covers many feasible paths while static backward exploration focusses on hard-to-reach instructions. One advantage of dynamic symbolic execution is that it can deal with third-party libraries or calls to native methods while static backward exploration cannot as there is no available constraint model. Another difference concerns the capabilities of dynamic symbolic exploration to use concrete value instead of symbolic ones for simplifying constraint solving. Note that the constraint reasonning model of JAUT handles complex constraints and just reports value choices to the labeling phase. EXE [START_REF] Cadar | Exe: automatically generating inputs of death[END_REF] implements global symbolic evaluation by launching an eager path exploration of the C program under test. Although this approach is appealing if implemented on a grid platform, it can reveal disastrous for programs that contain a huge number of paths. As soon as a program contains a loop, its number of paths is unbounded and even when it contains only conditionals, its number of path grows exponentially with the number of decisions in the worst case. Unlike JAUT, EXE does not use incremental constraint solving, so inconsistencies due to infeasible paths may be lately discovered and this could penalize the test input generation if implemented on a single machine. Note that EXE uses the STP SMT-solver which won several competitions and that it implements nice optimizations such as constraint caching and symbolic memory accesses tracking. However, as pointed out by the authors, its memory model does not handle double pointer dereferencing levels. The memory model of JAUT handles multiple dereferencing levels, up to a user-defined bound. Exhaustive bounded testing of Java programs as implemented in TestEra [START_REF] Marinov | Testera: A novel framework for automated testing of java programs[END_REF] and KORAT [START_REF] Boyapati | Korat: automated testing based on java predicates[END_REF] is a test input generation method that exhaustively explores the input search space. The approach can generate a large number of dynamically allocated structures but, unlike JAUT, it does not target specific locations or paths in the code. In fact, these constraintbased approaches have developed complex strategies to efficiently generate test inputs [START_REF] Elkarablieh | Efficient solving of structural constraints[END_REF] but they cannot solve path constraints extracted from programs.

Counter-example generation. Software model-checkers such as Save [START_REF] Coen-Porisini | Using symbolic execution for verifying safety-critical systems[END_REF], Blast [START_REF] Henzinger | Software verification with blast[END_REF], Magic [START_REF] Chaki | Modular verification of software components in C[END_REF] or Cbmc [START_REF] Clarke | Hardware verification using ANSI-C programs as a reference[END_REF] explore the paths of a bounded model of C programs in order to find a counter-example path to a temporal property. Some of them also address statement reacheability by generating test inputs to reach specific locations within the source code [START_REF] Visser | Test input generation in java pathfinder[END_REF]. Some of them exploit predicate abstraction to boost the exploration in the context of CEGAR that stands for (Counter-Example Generation through Abstraction Refinement). JAUT contrasts with these model-checkers and CEGAR as it does not abstract the program and does not generate spurious counter-example paths. In particular JAUT builds a constraint model of bytecode program by capturing an error-free concrete semantics without considering a boolean abstraction of the program structure. On the one hand, this allows for precise input memory state to be built but, on the other hand, requires costly analysis to be implemented.

VII. CONCLUSIONS AND FURTHER WORK

In this paper, we proposed a new constraint-based test input generation approach for testing Java programs at the bytecode level. We developed a logical memory model for a meaningful subset of bytecodes and proposed deductive rules to solve complex constraints such as p == p.next. Unlike other approaches, our prototype tool JAUT implements depth-first backward search and our experimental results indicate that this strategy complements forward search test data generation. Several short term improvements include the use of more dedicated constraint solvers to solve arithmetical constraints of the path conditions (e.g., Z3). Backward search could also be refined with an iterative bounded depth-first strategy to improve our handling of nested and sequential loop computations. Finally, our memory model could be improved by considering more fine-tuned awakening conditions. In the long term, our memory model could be completed to deal with exceptions as they just represent new control flow structures. Multithreading also appears as an essential topic in Java programming and implementing a backward search strategy for test input generation of multi-threaded bytecode programs would certainly be beneficial to the community.

Figure 2 .

 2 Figure 2. Example in Bytecodes

  , (b, [t3 → V 10]), which both contain two objects of class a and one object of class b, and the relation putf ield(A, t1, V al, H0, H1) where t1 is the first of the two attributes of the class a. Class b, which does not inherit from a, has only a single attribute. Suppose that dom(V 1) = [0..10], dom(V 3) = [1..3], dom(V 8) = 15..2 31 -1 while other domains are unconstrained, let dom(A) = {all} and dom(V al) = [10..40],

Figure 3 .

 3 Figure 3. Constraint blocks

Figure 4 .

 4 Figure 4. CPU Time to generate input for I in function of a, for method foo

Figure 5 .

 5 Figure 5. Time and coverage with jCUTE, Pex and JAUT (**: timeout of 3600sec)

Satisfiability Modulo Theories.

JAUT and all our experiments are freely accessible at http://www.irisa.fr/lande/gotlieb/resources/jaut.html .

There is a current 28-bits limitation for integers in our implementation, due to the use of the SICStus prolog clpfd library, but this is not a restriction of the model.

a.k.a. local variables in the SUN JVM specifications.