M Duval
email: mduval@insa-toulouse.fr

J C Passieux
email: passieux]@insa-toulouse.fr

M Salaün

S Guinard

LOCAL/GLOBAL NON-INTRUSIVE PARALLEL COUPLING FOR LARGE SCALE MECHANICAL ANALYSIS

Keywords: Finite Element Method, X-FEM, Multi-scale, Coupling Algorithms, MPI

The permanent increase in available computing resources can achieve more

and more ambitious numerical simulations (most of the time using the finite element method). When dealing with non-linear complex models on large 3D structures, the computational cost becomes prohibitive. In this paper, we present the recent developments linked to an innovative computing method: non-intrusive coupling. Such a method allows to efficiently take into account local modifications on an initial existing model in a non-intrusive way: the previously computed analysis is left unchanged. Large scale linear models can thus be easily computed, then localised non-linear complex models can be used to pinpoint the analysis where required on the structure. After a presentation of the scientific context and a description of non-intrusive coupling methods, we will present its application to crack growth simulation and parallel structure analysis.

CONTEXT AND INDUSTRIAL ISSUES

Every time one wants to create a new mechanical object, a conception cycle has to be respected, involving Computer Aided Design (CAD) and Finite Element Analysis (FEA). When dealing with a critical part of a mechanical product, a particular attention should be paid to the FEA. This is the point we will focus on in this paper. Indeed, in order to perform a mechanical simulation, one needs both a geometrical and a mechanical model. Some cases require a complex mechanical model, and some other a detailed geometry. The works which will be presented in this paper try to bring a solution to a recurrent FEA problem: how to compute a complex mechanical problem in a way requiring the least effort? There are two main problems which need to be addressed: geometric complexity and mechanical behaviour complexity.

Geometric modifications in Finite Element Analysis

The most direct way to perform a structural analysis via numerical simulation is to use the CAD model as the geometric model for the simulation. Indeed, the creation of a structure geometric model can be very time consuming. Moreover, for some critical parts, the mesh has to be certified before being used (aeronautical parts for instance). All in all, the fact is that we cannot afford to create a new geometric model or a new mesh each time we need to perform a simulation. Moreover, it appears that in the life cycle of a product, its geometric specifications can change (a crack can appear, some holes can be drilled). One objective of the computing method presented here is to bring a way to reuse an initial geometric model and its finite element mesh to compute structural analysis involving local details.

Localised complex mechanical behaviour

Another class of complex problems involves mechanical behaviour of the structure we analyse. Indeed, in structural analysis, two types of models have to be considered: linear and non-linear ones. Of course, the time required to complete the analysis will depend on the type of model. The use of certain complex non-linear models on very large structures fatally leads to considerable cost in terms of computer resources, often beyond what is currently available. The fact is that most of time, a non-linear model is useful only on a small part of the structure, which can be represented elsewhere with a linear model. Again it is possible to save a lot of computation time by reusing an existing linear model (and the corresponding solution) on a full structure: a non-linear model will thus be considered only on localised areas (see [START_REF] Akgün | Fast exact linear and non-linear structural reanalysis and the Sherman-Morrison-Woodbury formulas[END_REF]). The objective of non-intrusive coupling is here to make us able to merge several local complex non-linear models with a global linear one, without modifying this last one. In other words, if we need to perform several analysis of a large scale structure, the linear model will be assembled on the full structure only once, whereas the localised analysis will be performed as many times as necessary.

MODEL COUPLING METHOD AND ALGORITHM

As said previously, the non-intrusive coupling algorithm (see [START_REF] Gendre | Non-intrusive and exact global/local techniques for structural problems with local plasticity[END_REF] and [START_REF] Whitcomb | Iterative global/local finite element analysis[END_REF]) aims to perform a structural analysis using two separate models:

-a pre-existing simple model involving the full structure, which will represent the global mechanical behaviour (linear elasticity), -an ad-hoc complex model involving only a small part of the structure, representing the local mechanical behaviour (plasticity for example).

Coupling algorithm

In this paper, a two scale finite element method is considered. We will denote with the letter Ω the geometric domains and with the letter M the mechanical behaviour models.

Two coupled overlapping models are considered (see Fig. 1): a global one M = M 1 ∪ M 2 (involving the full structure Ω = Ω 1 ∪ Ω 2 , i.e. including a large number of nodes) and a local one M2 (involving only Ω2 ). Thus the global model will be treated as a coarse linear one, whereas the local one will take into account the localised (potentially non-linear) behaviour. Basically, the idea is to reach the equilibrium between the global M 1 and the local M2 models at the interface by the mean of an iterative algorithm, similar to those used in domain decomposition methods, i.e. solving alternately the Dirichlet (resp. Neumann) problem on the local (resp. global) model until convergence. Actually, we seek to replace the global solution of M 2 on Ω 2 by the one we would get with M2 . Let us consider domain decomposition in the linear case involving M 1 and M2 : we then get a monolithic coupling system (see Eq. ( 1)).

  K 1 0 C T 1 0 K2 -CT 2 C 1 -C2 0     U 1 Ũ2 Λ   =   F 0 0   (1)
Here K stands for the stiffness matrix, F for the load vector, U for the displacement field, C for the interface coupling matrices and Λ for the Lagrange multipliers vector (allowing for non-conforming meshes at the interface, using a mortar method). An iterative algorithm is then set up in order to dissociate the two models when solving the linear system.

Algorithm 1: Global/local domain decomposition -Iterative solver Data:

Λ 0 , ǫ k = 0 while η > ǫ do Global problem computation (Neumann problem) K 1 U k+1 1 = F -C T 1 Λ k Local problem computation (Dirichlet problem) K2 -CT 2 -C2 0 Ũ k+1 2 Λ k+1 = 0 -C 1 U k+1 1 Convergence test η = F Ω 1 / Ω2 + F Ω2 /Ω 1 / F k = k+1 end
The convergence test used here relies on the equilibrium between the two domains Ω 1 and Ω2 . We give below the corresponding equality in terms of finite elements objects at iteration k.

F

Ω 1 / Ω2 + F Ω2 /Ω 1 = (K 1 U k 1 + C T 1 Λ k ) Γ (2)
Here, the non-intrusiveness of the method comes from a fictitious prolongation of the solution from Ω 1 to the full global domain Ω. We then definite U so that

U | Ω 1 = U 1 and U | Ω 2 = U 2 . KU = K 1 U 1 + K 2 U 2 (3)
Using this equality at the global computation step gives us the expression of the equation standing for the prolonged global model at each iteration k.

KU k+1 = F -C T 1 Λ k + K 2 U k 2 (4)
Actually, the iterative algorithm tends to replace the global stiffness on Ω 2 by the local one, through an additional right hand side load vector. The coupled equations system in the non-intrusive case then rewrites into the following form.

KU k+1 = F -C T 1 Λ k + K 2 U k 2 (5) K2 -CT 2 C2 0 Ũ k+1 2 Λ k+1 = 0 -C 1 U k+1 1
In a few words, the global and the local models are coupled via displacement and effort swap at the interface. The computational cost involved by the algorithm can be significantly smaller than the one involved by a full scale nonlinear complex computation. Still, it may be noted that, as such, the performance of the method is dependent on the stiffness gap between the two models M 2 and M2 . Indeed, the more the stiffness gap is important, the more the algorithm will require a large number of iterations to converge. This is very inconvenient for crack propagation simulation: the stiffness gap increases as the crack growths. Hopefully, a Quasi-Newton correction (see [START_REF] Gendre | Non-intrusive and exact global/local techniques for structural problems with local plasticity[END_REF]) allows to get rid of that problem: thanks to the Sherman-Morrison-Woodbury formula, it is possible to modify the tangent stiffness of the global model in a non-intrusive way (see [START_REF] Akgün | Fast exact linear and non-linear structural reanalysis and the Sherman-Morrison-Woodbury formulas[END_REF]). First of all, let us remark the following equalities arising from the coupling formulation:

KU k = K 1 U k 1 + K 2 U k 2 (6) (K 1 U k 1 ) Γ N = F (7)
It is possible to reformulate Eq. ( 5) into a Newton algorithm (i.e. in an incremental formulation) by adding -KU k both on the left and right sides of the full domain equation

at iteration k. K U k+1 -U k = F -C T 1 Λ k + K 2 U k 2 -KU k (8)
Indeed, making use of Eq. ( 6) and ( 7) into Eq. ( 8), one can give the following formulation:

U k+1 = U k -K -1 f (U k ) ( 9
)
where f is the finite element operator computing the forces equilibrium residual on Γ between Ω 1 and Ω2 given the full displacement U k at iteration k.

f (U k ) = (K 1 U k 1 + C T 1 Λ k ) Γ = F Ω 1 / Ω2 + F Ω2 /Ω 1 (10)
In practice matrix K is a bad approximation of the true gradient ∇f . Thus, the Newton scheme given at Eq. ( 9) cannot be used as such, as it would lead to tremendous number of iterations when the stiffness gap between the local and the global model is important.

Instead, one can rely on Quasi-Newton methods to update the matrix K. The Symmetric Rank One (SR1) update is an easy-to-implement and efficient way to build a sequence of matrices K k convergent toward ∇f (we will assume K 0 = K when initialising the algorithm).

Let us define

d k = U k+1 -U k and y k = f (U k+1 ) -f (U k ).
At iteration k, we seek to update K k into K k+1 with the SR1 formula, i.e. with an update rank-one symmetric update, while verifying the secant equation for each iteration k > 1:

K k+1 = K k + (y k -K k d k )(y k -K k d k ) T d T k (y k -K k d k ) (11)
Note that in the context of the SR1 update, Eq. ( 9) rewrites K k d k = -f k , so that Eq. ( 11) can be given in a simplified form (where

f k = f (U k )). K k+1 = K k + f k+1 f T k+1 d T k f k+1 (12)
Nevertheless, one has to keep in mind the non-intrusiveness constraint of the coupling algorithm, i.e. do not modify the full stiffness matrix K. This can be achieved using the Sherman-Morrison formula on Eq. ( 12), leaving us with the following relation which can be used in order to compute K -1 k f k in a iterative manner based upon the knowledge of

K -1 0 f k . K -1 k+1 = K -1 k -K -1 k f k+1 f T k+1 K -1 k f k+1 (d k + K -1 k f k+1 ) (13)

Connections with standard methods

For several years, model coupling is used in nearly all the engineering departments. One can cite two main classes of method:

-First, when dealing with large mechanical structures, one often needs a very precise analysis on localised small parts. As said before, we cannot afford to use a fine mesh and a precise model on the whole structure. Instead, structural zooming is often a solution (see [START_REF] Daridon | Changement d'chelles et zoom structural[END_REF]). It consists on computing a precise solution on a small area of a structure, using the pre-computed coarse solution on the full structure as boundary conditions. No iteration is applied in such methods.

-Then, one can cite domain decomposition method. These methods allow to efficiently couple models and meshes; nevertheless it requires significant efforts in order to make interconnections between the models (see e.g. [START_REF] Dhia | The arlequin method as a flexible engineering design tool[END_REF], [START_REF] Brezzi | The three-field formulation for elasticity problems[END_REF] and [START_REF] Farhat | A method of finite element tearing and interconnecting and its parallel solution algorithm[END_REF]). Moreover, no pre-computed solution can be reused, resulting on very large computing resource needs.

In fact, the non-intrusive coupling algorithm provides a generic method which allows coupling several models with the least effort, while preserving the inherent advantages of the methods presented above:

-The global pre-existing model is unmodified.

-Incompatible meshes can be interconnected via a mortar-like method, for example.

-Parallel resolution can reduce the computation time in case of multiple local models.

APPLICATION TO CRACK GROWTH SIMULATION

The main application we focus on in this paper is crack growth simulation. For a lot of engineers, sustainability in construction (aeronautical, naval) is a priority. Indeed, during the life cycle of a mechanical structure (steel, concrete), cracks can appear, endangering the integrity of the structure. Thus, forecasting the propagation path of such cracks is a major issue for engineers. Nevertheless cracks locations cannot be known a priori when designing a structure or setting up a finite element mesh for initial structural analysis. Using the common FEA tools, when one needs to simulate crack propagation, two main solutions are available:

-Set up a crack conforming mesh (see [START_REF] Bittencourt | Quasi-automatic simulation of crack propagation for 2D LEFM problems[END_REF] and [START_REF] Chiaruttini | Advanced remeshing techniques for complex 3D crack propagation[END_REF]) at each step of the propagation.

When combined to an adapted mesh refinement at crack tip, it leads to accurate results. The main drawback of conforming meshing is the substantial computational resulting cost. For that reason, direct crack meshing is rarely used as such, unless a very fast and efficient remeshing algorithm is set up.

-Use X-FEM method (see [START_REF] Moës | A finite element method for crack growth without remeshing[END_REF]) on an existing mesh. Theoretically, such a method allows the mesh to be not conforming to the crack faces. Nevertheless, most of time, remeshing is necessary at crack tip if one wants to get an accurate enough solution.

All in all, common methods do not allow reuse of existing meshes without (at least local) modifications, resulting in an extra computational cost. Instead, another possibility is to consider two different models, standing for different scales: a global linear elastic model, representing the full structure (healthy structure) and a local (potentially nonlinear and/or XFEM) model for the cracked domain (see Fig. 2). Using the non-intrusive algorithm for crack propagation simulation (see [START_REF] Gupta | Analysis of threedimensional fracture mechanics problems: A non-intrusive approach using a generalized finite element method[END_REF] and [START_REF] Passieux | Local/global nonintrusive crack propagation simulation using a multigrid X-FEM solver[END_REF]) will provide the following advantages:

-Remeshing will be necessary only on the local model.

-Non-linear behaviour will be used only on the local model.

-The global linear model will be assembled once and the stiffness matrix will be factorised only once too.

Altogether, the non-intrusive coupling algorithm allows reusing a pre-existing mesh and linear elastic model (i.e. stiffness matrix) in order to perform computationally cheap crack growth simulation. The results presented in this paper have been computed using Code Aster, a structural engineering software developed by Électricité de France. Both global and local models have been computed as a black box using this software, whereas the coupling (i.e. interface data exchange) has been done using a Python code developed for that purpose.

PARALLEL COMPUTING, DISTRIBUTED MICRO MODELS

The two main features of the non-intrusive coupling algorithm are: "non-intrusive" which is the possibility to locally modify an initial model, and "coupling" which is the possibility to use different models to compute a single structure. This last feature will be developed now more in details. Indeed, it is possible to consider several non-overlapping local models (for example if we want to represent several cracks on the same structure). Each local model will be completely independent from the others, allowing for an efficient parallel solver to be set up, using for instance MPI communications. When dealing with non-linear local models, parallelism is often the only possibility making FEA possible. We want to draw the readers attention here on an important detail: unlike domain decomposition methods (e.g. FETI method, see [START_REF] Farhat | A method of finite element tearing and interconnecting and its parallel solution algorithm[END_REF]), each local analysis can be carried out independently from the others. An application of this property is assemblies analysis. Indeed, for very large structures, simulation of assemblies is computationally very expensive. Moreover, if the model contains too much contact areas, it becomes difficult to make the analysis possible because of the high complexity of the non-linear behaviour. Thanks to non-intrusive coupling, it is possible to compute each junction assembly separately: common contact algorithms will be able to perform the computation easily. We present here another application of parallel computing applied to non-intrusive coupling: a multi-cracked plate (see Fig. 3). We consider here, as an academic test case, three disjoint cracks. From a global coarse mesh, we generate three local refined patches on which an X-FEM model is applied. For a given iteration of the coupling algorithm, the three local models are computed in parallel, thanks to the MPI communication. The important point here is that there is no direct communication between the local patches. Every interface data exchange (displacement and effort) takes place between the global and one local model, through a coupling engine. It may also be noted that, in that example, no load is applied to the global model; we constrained only three degrees of freedom in order to disable rigid body motions. The only load applied is a hydrostatic pressure on the crack lips. Then, the local loading spreads to the global model only through the additional global right hand side load vector. Moreover, the stiffness gap between the global and the local models is very important here, as we considered three cracks. Still, the Quasi-Newton method allows for an important speed-up (see Fig. 4).

INTEGRATION OF RESEARCH CODES INTO COMMERCIAL SOFT-WARE

Finally, the last interest of non-intrusive coupling we will develop is the possibility to easily merge research codes and commercial softwares. Indeed, as presented previously, the only data exchange occurring between the global and the local models is interface displacements and forces. Thus it is possible to compute the global solution from a commercial software using the existing models and solvers, and compute the local solution using an ad-hoc model developed with any code. Using a MPI communication between the two codes (i.e. between the two models, global and local) makes the communication straightforward: we only have to focus about the data we need to exchange, as MPI will provide his own standard for language compatibility. For instance we can cite [START_REF] Gendre | Non-intrusive and exact global/local techniques for structural problems with local plasticity[END_REF] which compute an aeronautical structure analysis with localised plasticity within a linear model from Abaqus/Standard. If we focus our interest on crack growth simulation, we can cite [START_REF] Chahine | Spider-xfem, an extended finite element variant for partially unknown crack-tip displacement[END_REF] and [START_REF] Passieux | Direct estimation of generalized stress intensity factors using a three-scale concurrent multigrid X-FEM[END_REF] which propose a special treatment for crack tip displacement singular field (analytical solution, adapted radiating mesh) within an elastic linear model.

CONCLUSION

In this paper, a non-intrusive coupling approach has been presented. This method allows to take into account local features in existing FEA models without actually modifying it. The main purpose of the method is to make FEA easier, as finite element models preparation can sometimes be more time consuming than the computation itself. Thanks to this algorithm, we have been able to set up a two and three dimensional crack growth simulation, using Code Aster for the mechanical computations and MPI based communications for the interface coupling. All of the process is wrapped into a Python API. The distributed implementation of the algorithm we proposed here allows for high performance multi-patch parallel computations. In a near future, we seek to make the method even more flexible by extending it to non-coincident patches (see [START_REF] Pironneau | Numerical zoom for localized multiscales[END_REF]). It may be noted that the algorithm can also be used to couple different mechanical representations (e.g. 2D/3D coupling, see [START_REF] Guguin | Nonintrusive coupling of 3D and 2D laminated composite models based on finite element 3D recovery[END_REF]) or to couple different analysis methods (deterministic/stochastic models, see [START_REF] Chevreuil | A multiscale method with patch for the solution of stochastic partial differential equations with localized uncertainties[END_REF]) in a non-intrusive way. This work is supported by the French National Research Agency (Grant ANR-12-MONU-0002 ICARE).

Figure 1 :

 1 Figure 1: Non-intrusive coupling -Situation overview

Figure 2 :

 2 Figure 2: Non-intrusive FEM/X-FEM coupling

Figure 3 :

 3 Figure 3: Multi-crack distributed patches

Figure 4 :

 4 Figure 4: Convergence of the algorithm


Ben Spencer

Michael Benedikt

Pierre Senellart

Form Filling based on Constraint Solving

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Finding data on the Web is useful for search, information extraction, and aggregation. The massive scale of the Web and the data itself means these tasks must necessarily be automated. Interesting data is often hidden behind user interfaces, and in particular Web forms. For example, airline or real-estate websites provide free access to their data via search forms, but there is no public API or standard way to access this information. This data is "hidden" from Web search engines and other automated tools, and makes up the deep or hidden Web [START_REF] Michael | The deep Web: Surfacing hidden value[END_REF][START_REF] He | Accessing the deep Web[END_REF].

An automated tool accessing Web forms must find some sequence of user actions (for example clicking buttons or filling input fields) which leads to a successful form submission: one that leads to the target data. These actions might involve complex interactive user-interface elements such as drop-down lists, date pickers, and tabs. In addition, they must satisfy certain restrictions on the actions and inputs given such as mandatory and optional fields, and validation rules for input values. This combination of actions and input values creates a huge search space for form filling tools to consider. The restrictions on input actions and values are normally enforced in the browser directly with client-side JavaScript (for usability) and again on the server when the query is received (for security). Human-focused interfaces and input validation rules make it difficult for automated tools to correctly fill and submit the forms.

Much research has been devoted to effective, automatic form-filling [START_REF] Barbosa | Siphoning hidden-Web data through keyword-based interfaces[END_REF][START_REF] Jiang | Efficient deep Web crawling using reinforcement learning[END_REF][START_REF] Zanini Kantorski | Choosing values for text fields in Web forms[END_REF][START_REF] Liakos | Focused crawling for the hidden Web[END_REF][START_REF] Lu | An approach to deep Web crawling by sampling[END_REF][START_REF] Wang | Discover hidden Web properties by random walk on bipartite graph[END_REF], or even further, to generating wrappers which use the form to look up and extract data [START_REF] Furche | DIADEM: thousands of websites to a single database[END_REF][START_REF] Raghavan | Crawling the hidden Web[END_REF][START_REF] Senellart | Automatic wrapper induction from hidden-Web sources with domain knowledge[END_REF]. A common target is search fields, which generally have no validation constraints [START_REF] Barbosa | Siphoning hidden-Web data through keyword-based interfaces[END_REF][START_REF] Zanini Kantorski | Choosing values for text fields in Web forms[END_REF][START_REF] Ntoulas | Downloading textual hidden Web content through keyword queries[END_REF]. Other work assumes domain knowledge, encoded in heuristics or rules [START_REF] Furche | DIADEM: thousands of websites to a single database[END_REF]. For complex fields in the absence of domain knowledge, approaches to finding field values include sampling text on the page [START_REF] Palmieri Lage | Automatic generation of agents for collecting hidden Web pages for data extraction[END_REF], and the application of machine Listing 1 Validation code for the example airline form.

function validate to() { var from = document.getElementById("from").value; var to = document.getElementById("to").value; return validate aux(from, to); } function validate aux(from, to) { if (from.length == 0) { alert("Error: Departure airport must be set"); return false; } if (from == to) { alert("Error: Departure must differ from Destination"); return false; } return true; } function validate date() { var to = document.getElementById("from").value; var date = document.getElementById("date").value; if (to.length == 0) { alert("Error: Destination Airport must be set"); return false; } var day = parseInt(date.substr(0, 2), 10), month = parseInt(date.substr [START_REF] Artzi | A framework for automated testing of JavaScript Web applications[END_REF][START_REF] Barbosa | Siphoning hidden-Web data through keyword-based interfaces[END_REF], 10); var now = new Date(); var valid = (month>=now.getMonth()+1 && (month!=now.getMonth()+1 || day>=now.getDate())); if (!valid) { alert("Error: date cannot be before today"); return false; } return true; } learning techniques [START_REF] Jiang | Efficient deep Web crawling using reinforcement learning[END_REF][START_REF] Madhavan | Google's deep-Web crawl[END_REF]. Without both domain knowledge and a corpus of examples, these approaches cannot infer constraints enforced by client side code, and thus cannot find satisfying values. We aim to supplement these approaches with constraint-driven form filling, which analyzes client-side code to determine constraints being enforced on form actions and values, and solves these constraints to yield successful submissions. Constraint-driven form filling allows form exploration tools to exploit the rapid advances in constraint-solving technology [START_REF] Barrett | The SMT-LIB initiative and the rise of SMT[END_REF][START_REF] De | Satisfiability modulo theories: Introduction and applications[END_REF][START_REF] Kroening | Decision Procedures: An Algorithmic Point of View[END_REF].

Example 1. Consider an airport form, which includes fields From and To (with identifiers "from" and "to", respectively) with values populated from a drop-down list, along with field Date (with identifier "date") populated by a date picker. A snippet of the form's validation code is shown in Listing 1, where validate to is attached to the To field, and validate date is attached to the Date field. For To, the code checks that the From field has already been filled and that it is not equal to To. For Date it checks that To is already filled and that the date entered is later than today's date (for simplicity, all dates are assumed to be in the current year).

Note that the validation code involves restrictions on both the values of the fields, and on the order in which they are filled. In addition to the constraints explicitly enforced by the event handlers, there are a number of implicit constraints on the field: for example, From and To are implemented by drop-down lists, so the values can only be chosen from a certain pre-determined set. A form-filling or wrapper-generation tool must find values that satisfy all of these constraints.

Static analysis of the underlying code can in principle determine the set of restrictions enforced by the code (and thus values leading to form submission). Unfortunately, analyzing JavaScript code used on the Web is notoriously difficult [START_REF] Benedikt | ProFoUnd: Program-analysis-based form understanding[END_REF]. Thus a popular intermediate position in testing JavaScript code is dynamic analysis, with a well-known approach being concolic testing [START_REF] Godefroid | DART: directed automated random testing[END_REF][START_REF] Sen | CUTE: a concolic unit testing engine for C[END_REF]. Concolic testing combines concrete and symbolic execution, using the symbolic analysis and constraint solving to generate new concrete input values to test. The goal is to generate test inputs which cover each distinct code path in the program or function being tested.

We introduce FormSolve, which applies the idea of mixing execution, symbolic tracing, and constraint solving to the exploration of Web forms. FormSolve will generate input actions and values for Web forms, symbolically trace the code executed with these inputs, and solve constraints that will lead to new inputs which reach new code paths.

We propose a refinement of concolic testing tuned for Web forms. This involves many challenges that are not encountered in concolic testing of standalone code. Instead of using a constraint solver to find input values for a single function, our concolic testing algorithm explores sequences of user input events, along with their corresponding values, that may trigger a set of event-handling functions. Our browser infrastructure allows the symbolic tracing of this event-handling code, which can be written either directly in pure JavaScript or using popular libraries such as jQuery. It also provides fine control over the browser, which is necessary for faithfully-and deterministically-emulating user form-filling actions, as well as for controlling and monitoring the browser's behavior. In order to get interesting output, our goal is not to generate arbitrary input values (as in exhaustive testing), or interesting corner cases (as in functional testing), but rather values that a typical user might provide via the interface. Our constraint generation allows us to focus on user-realizable values, thus accelerating the discovery of interesting form submissions. We evaluate our technique on both synthetic and real-world forms, and compare it to alternative approaches to Web form filling.

Related work.

Indexing and extraction from the deep Web involves a number of tasks, including entry point finding [START_REF] Barbosa | An adaptive crawler for locating hidden-Web entry points[END_REF][START_REF] Lu | Annotating structured data of the deep Web[END_REF][START_REF] Madhavan | Google's deep-Web crawl[END_REF], form label identification [START_REF] Furche | OPAL: Automated form understanding for the deep Web[END_REF][START_REF] Nguyen | Learning to extract form labels[END_REF][START_REF] Wu | Modeling and extracting deep-Web query interfaces[END_REF], form-filling [START_REF] Barbosa | Siphoning hidden-Web data through keyword-based interfaces[END_REF][START_REF] Jiang | Efficient deep Web crawling using reinforcement learning[END_REF][START_REF] Zanini Kantorski | Choosing values for text fields in Web forms[END_REF][START_REF] Liakos | Focused crawling for the hidden Web[END_REF][START_REF] Lu | An approach to deep Web crawling by sampling[END_REF][START_REF] Wang | Discover hidden Web properties by random walk on bipartite graph[END_REF], and result page analysis [START_REF] Valter Crescenzi | RoadRunner: Towards automatic data extraction from large Web sites[END_REF][START_REF] Zhao | Fully automatic wrapper generation for search engines[END_REF]. Work on form-filling is focused on finding values that extract a good set of results. For example, some work attempts to choose keywords for a text field which return relevant results [START_REF] Barbosa | Siphoning hidden-Web data through keyword-based interfaces[END_REF]. Tools such as Crawljax [START_REF] Mesbah | Crawling Ajax-based Web applications through dynamic analysis of user interface state changes[END_REF] and AJAX Crawl [START_REF] Duda | AJAX crawl: Making AJAX applications searchable[END_REF] take into account the state of the user interface while crawling. The emphasis there is in identifying changes in the DOM (Document Object Model, the tree structure representing the content and structure of a Web page) caused by user actions and events, not on getting through forms. Our work is on form-filling, but the focus is only on getting results that satisfy validation rules. Additional desired properties can be overlaid on top of this. One of our challenges is choosing an interesting ordering for the form filling events. This challenge also arises in the analysis of other event-driven systems, such as Android apps [START_REF] Anand | Automated concolic testing of smartphone apps[END_REF][START_REF] Hu | Efficiently, effectively detecting mobile app bugs with AppDoctor[END_REF][START_REF] Jensen | Automated testing with targeted event sequence generation[END_REF].

Concolic testing is a well-established topic, applied to many programming languages, including JavaScript. Yet there are few attempts to apply it to the Web. SymJS [START_REF] Li | SymJS: Automatic symbolic testing of JavaScript Web applications[END_REF] uses concolic testing, but is based on the Rhino JavaScript engine, which can parse only a small fraction of real-world Web JavaScript. Jalangi [START_REF] Sen | Jalangi: a tool framework for concolic testing, selective record-replay, and dynamic analysis of JavaScript[END_REF] is a framework allowing instrumentation and runtime monitoring of JavaScript. Neither SymJS nor Jalangi support Web forms. The only systems we know of for exploring forms via JavaScript analysis are the demonstration systems ProFoUnd [START_REF] Benedikt | ProFoUnd: Program-analysis-based form understanding[END_REF] and ArtForm [START_REF] Spencer | ArtForm: A tool for exploring the codebase of form-based websites[END_REF] (precursor to this work).

Concolic testing for Web form exploration

Concolic testing, or directed automated random testing [START_REF] Godefroid | DART: directed automated random testing[END_REF][START_REF] Sen | CUTE: a concolic unit testing engine for C[END_REF], is a testing technique which uses concrete executions of a program to drive a symbolic analysis. The symbolic analysis guides the automated tester and suggests specific inputs which reach new parts of the program which would be difficult for traditional test-generation approaches to Algorithm 1 High-level algorithm for concolic testing. path-tree ← Init-Tree(trace) 5:

while path-tree is not fully explored do 6:

target-path ← Search(path-tree) 7:

values ← Solve-Path-Constraint(target-path) 8:

if target-path was successfully solved then 9:

trace ← Execute-And-Record(program, values) 10:

Extend-Tree(path-tree, trace) 11: else 12:

Mark-Unreachable(path-tree, target-path) 13:

end if 14:

end while 15: end procedure discover. Conversely, the concrete executions allow exploration through parts of the program which are not fully understood by the symbolic analysis alone.

A generic concolic testing algorithm is given in Algorithm 1. Concolic testing begins by choosing some default starting values for the variables. The function is then executed concretely (that is, using a real interpreter) and symbolic information is recorded about how the inputs are modified and when they occur in branch conditions. Thus each trace is associated with a path condition: the set of individual branch conditions (expressed in terms of the input values) which must be satisfied or unsatisfied in order for the program execution to follow that particular path. Each path condition is a logical formula describing an equivalence class of input values, with equivalent values resulting in the same execution path in the program. Thus the state of the exploration can be characterized by the set of path conditions of explored traces, which form a tree. The testing algorithm proceeds in an execute-and-analyze loop. After execution of a trace, the new information gathered during that trace is added to the tree. In order to find set a of input values that reaches a new path, the algorithm chooses a sequence of branch conditions that has not been explored, generates the corresponding path condition, and sends it to a constraint solver. If the solver can satisfy the constraint, a solution is chosen as the next set of input values. If the solver cannot, the path is marked as unreachable. This process is repeated to cover progressively more code on each new iteration.

Example 2. Consider the function validate aux(from,to) from the running example. Concolic testing would first execute the program on random values for the arguments from and to, say empty strings for both. This would bring the program to a trace that terminates after the first alert. Tracing this path symbolically, the algorithm identifies the constraint from.length = 0, which is the first path added to the tree (line 4). The search command on line 6 will isolate the path consisting of the single constraint ¬(from.length = 0) as an unexplored path in the code, and this will be sent to a constraint solver (line 7), which will return values for from and to that satisfy it. For example, the solver might return the values from = 'a' and to = 'a'. These values are used to execute the function in the next iteration, which drives the code to the second alert. This second execution is symbolically traced, with the path ¬(from.length = 0) ∧ from = to. The search procedure on line 6 now selects ¬(from.length = 0) ∧ ¬(from = to) as an unexplored path to target. Solving this constraint will give values that drive the execution to avoid each alert.

Note that concolic testing normally includes classification of a trace-in the context of testing, this would be determining whether an error occurs in it. In Algorithm 1, we assume this is done within Execute-and-Record. For our form crawling application, the classifier determines whether the result of a trace is a successful submission (leading to a new page) or not. We can detect this by checking for page loads, alert messages, or certain modifications to the DOM.

Adaptation to form exploration. In adapting concolic testing to the exploration of Web forms, a tempting analogy is that the form represents a "virtual function", whose arguments are the form fields. However, a function takes its arguments all at once, whereas a Web form takes inputs one at a time interactively. The code which responds to a form filling can be triggered by a number of events, such as filling fields or hovering over them. These event handlers may interact, and the order in which they are fired can affect the output. Thus a more realistic model of a form is as an association of each field f with one or more actions Act f , where an action writes the input value v f into the field and executes some program code. In using concolic testing to explore a form, we must discover both the values to fill into form fields and also the ordering of these actions.

Our algorithm is shown in Algorithm 2. We explain the details, and in particular the constraint solving call on line 12, below. It is similar in structure to a classic concolic algorithm, with the high-level distinction that we explore a tree of paths for each action. At each iteration we choose an action with unexplored code, and generate both a value for each form field and an action ordering.

We now formalize the problem of simultaneous detection of input values and the ordering of actions using an extremely idealized model Although the model's assumptions do not hold on real Web forms, the approach is still effective.

In the model we have a set of form actions, each with a corresponding program which manipulates a set of variables v, including one distinguished variable v, the input variable of the form action. Informally this is the value supplied by the user when invoking this action. Each variable v has a default value D (provided by the Web page's HTML) which it holds until the action is run. In our basic model, we assume program code in a simple procedural language built up from the following grammar:

x := τ ( y) if ϕ( y) then E 1 else E 2 E 1 ; E 2 Abort do C
Above τ ranges over terms built up from set of atomic functions (e.g., +, ×) from variables and constants, while ϕ ranges over some set of conditions (e.g., Boolean combinations of atomic conditions τ 1 { , =, =} τ 2 , where τ i are terms). C in do C ranges over some set of commands that do not impact submission or control flow. A condition ϕ is ground if it contains no free variables.

A variable is assigned in expression E if it occurs on the left side of some assignment statement and otherwise is free. The semantics of the language are standard. Given an expression E and a binding σ for the free variables of E, the semantic function returns the sequence of ground conditions and atomic actions Abort and do C that are generated during an execution. We will be particularly interested in the truth values of conditions and whether or not Abort is encountered. Given a condition ϕ and a binding σ for the Algorithm 2 The high-level algorithm for form exploration. end while 25: end procedure variables in ϕ, the value of ϕ, denoted Val(ϕ, σ), is true if ϕ holds when the variables appearing in ϕ are replaced with their valuation by σ. The trace of E on an assignment σ to the free variables of E is the sequence of conditions encountered and their values. If E executes Abort at any point when running on σ it is said to abort on σ, while otherwise we say it terminates on σ.

We name our actions by numbers, with Act i denoting the program associated with action i, while v i and D i denote the distinguished input variable and default value of Act i , respectively. A set of such indexed actions Act 1 . . . Act n has restricted global state if for every Act i , each free variable v occurring in it's program expression is one of the input variables v j and no input variable is ever assigned. That is, the actions have no shared global state except the input variables, which are set as each action is executed.

The trace of an action on a binding σ is simply the trace of its program code expression. The behavior of a single expression is well-defined given a binding for all variables. We now need to explain the outcome of a sequence of form actions, which involves binding each free variable v encountered in conditions to either the user-specified input value of v or to its default value.

A bound form action is a pairing of a form action Act i with a value c i for its input variable v i , while a form input is a sequence of bound form actions. We define the unfolding of a form input (Act 1 , c 1 ) . . . (Act n , c n ) as the sequence (E 1 , σ 1 ), . . . , (E n , σ n ), where σ i is the order-modified assignment mapping v j to c j if j i and to D j otherwise. We can extend our semantics to form inputs via unfoldings. The trace of a form input is the concatenation of the traces in its unfolding. A form input is said to abort if some E i aborts on σ i ; otherwise we say it terminates.

We now extend our discussion from traces to symbolic descriptions of these traces, starting with the "local behavior" within a form action, given a binding for all variables. For binding σ to the free variables of expression E, the local symbolic path of E(σ) is a formula describing the values of conditions in the trace of E(σ). That is, the conjunction Val(ϕi,σ)= ϕ i ∧ Val(ϕi,σ)=⊥ ¬ϕ i where ϕ 1 . . . ϕ k is the sequence of conditions encountered in executing E on σ.

We have just discussed the symbolic paths that emerge from concrete traces. We now describe formulas that represent possible concrete traces for future exploration. Given a trace t = (ϕ 1 , TVal 1 ) . . . (ϕ k , TVal k ) for an action, consisting of conditions ϕ i and their truth values TVal i , a symbolic modification is a local symbolic path of the form (ϕ 1 , TVal 1 ) . . . (ϕ p , TVal p ), (ϕ p+1 , ¬TVal p+1 ) where p < k. That is, we take a prefix of t, and negate its last element. Given a set of traces T , a symbolic modification is unexplored if no trace in T satisfies this condition. Given set of traces T and action A, Unexplored A (T ) is the set of symbolic modifications of traces in A that are unexplored.

We can lift the classification of traces as aborting or terminating to the symbolic level. Given a set of traces T and a form action A, let T (A) be the restriction of the trace to A. Let Abort A (T ) be the traces in T (A) that are aborting, and Terminate A (T ) the set of traces that are terminating. By Symbolic(Abort A (T )) we denote the set of local symbolic paths of traces in T that are aborting in A, and similarly for Symbolic(Terminate A (T )).

Above we have a symbolic version of the behavior of a single form action A, describing it via conditions. We now need to lift this to a sequence of form actions. In doing this we have to take into account the role of the ordering in determining whether we use the default value or the user-supplied value. Further, since we are interested in whether a path is explored in a terminating trace, we also need to track symbolically whether other actions abort.

Given a local symbolic path ψ( v) of a trace for Act i , the ordered version of ψ, Ord i (ψ), is the formula ψ with each variable v j replaced by v j and conjoined with the constraint (j i → v j = v j ) ∧ (j i → v j = D j ) using an additional relation . That is, Ord i (ψ) is a symbolic representation of an ordering and a binding σ such that ψ holds on the order-modified assignment σ i defined above.

Given a path sympth for action Act i , and a set of traces T , let OverApprox i (sympth) to be Ord i (sympth) ∧ OrderAx ∧ j =i MayTerminate j , where MayTerminate j is defined as sympth j ∈Symbolic(Abort Act j (T )) ¬Ord j (sympth j ) and OrderAx is a formula asserting that is a linear order on the indices of actions 1 . . . n. That is, the formula OverApprox i (sympth) symbolically represents the orderings and values that will achieve the behavior sympth in action Act i and will not drive any other action to a known-aborting trace of T . Informally, it describes form inputs that may explore sympth without aborting in any action, based on the current knowledge of aborts in T .

Similarly, UnderApprox i (sympth) is Ord i (sympth) ∧ OrderAx ∧ j =i MustTerminate j , where MustTerminate j is sympth j ∈Symbolic(Terminate Act j (T )) Ord j (sympth j ). This formula represents orderings and values which achieve the behavior sympth in action Act i and drive every other action to known-terminating trace of T . Informally, this describes inputs and orderings that we are sure will explore sympth based on what we know about aborts in T . The following two lemmas give the critical properties of these symbolic descriptions. Lemma 1. If UnderApprox i (sympth) is satisfiable by input values c 1 . . . c n and ordering j 1 . . . j n , then the form input (Act j1 , c j1 ) . . . (Act jn , c jn ) gives a trace that does not abort outside of action Act i and extends sympth. Lemma 2. If sympth is a symbolic modification for action Act i , and the form input (Act j1 , c j1 ) . . . (Act jn , c jn ) generates a trace extending sympth that does not abort outside of Act i , then c 1 . . . c n and j 1 . . . j n satisfy OverApprox i (sympth).

Lemmas 1 and 2 form the basis of Algorithm 2. We maintain a set of traces and corresponding symbolic paths which, along with their symbolic modifications, form a tree. We also classify the symbolic paths and their modifications. We distinguish the known-extendible paths, those which are known to have an extension that is terminating, and the known-unextendible ones, where it is known that there is no such extension. The paths which are neither known-extendible or known-unextendable are said to be unresolved. The set Unresolved A (T ) contains the local symbolic paths from T which are neither known-extendible or known-unextendible, as well as the symbolic modifications of local symbolic paths in T which have not yet been considered by the algorithm.

At any step of the algorithm we choose an unresolved path sympth and check whether OverApprox i (sympth) is satisfiable. If the formula is not satisfiable, we mark sympth as known-unextendible (that is, no terminating trace extends sympth, which we know from Lemma 2). Otherwise we take a satisfying assignment consisting of c 1 . . . c n and ordering j 1 . . . j n , and use it in a new execution, giving trace t. We add the new trace t to our set of traces and iterate.

If t terminates, then it acts as a witness that each restriction of t to action Act i can be extended by a terminating trace. Thus, we mark all the local symbolic paths in t as known-extendible. If t aborts, then by Lemma 1 we know that either Act i aborted, or c 1 . . . c n and j 1 . . . j n did not satisfy UnderApprox i (sympth). In either case, there must be some action Act j for which t does not extend an explored branch, and where t aborts. That is, in Act j , t follows a previously unexplored path and discovers an abort. Thus one local symbolic modification is resolved in Act j (even if it had not been a known modification until now).

It is possible for a newly recorded trace to give rise to new symbolic modifications, so the total number of unresolved traces does not necessarily decrease at each iteration. However, each action's program code has a finite number of symbolic branches, so the number of symbolic paths available to explore is limited. Because at least one local symbolic path is resolved in each iteration, i∈{1..n} Unresolved Acti (T ) must eventually become empty, and this guarantees termination. Proposition 1. Algorithm 2 is complete. Assuming completeness of the solver, on termination the path tree will have the property that for every local symbolic path sympth which has any extension which terminates overall, then at least one such extension is explored by the algorithm. In other words, every local symbolic path which is reachable on a terminating trace is explored. Example 3. Let us illustrate Algorithm 2 on Example 1. Assume that we have identified the form actions as Act From , Act To , and Act Date for entering values into the departure airport, arrival airport, and departure date fields. Algorithm 2 will choose an arbitrary default initial order and values for these fields: for example empty strings for the airports and "01/01" for the date. The code is executed on these values, and reaches the first alert message in validate aux, and the first alert in validate date, both classified as aborts. The corresponding local symbolic path for Act To is the single constraint from.length = 0, and for Act Date it is to.length = 0. These constraints are added to the corresponding path trees for each action. The command on line 11 will then choose an unexplored path to target, suppose it is ¬(to.length = 0) in Act Date . Assuming the default value D To is the empty string, the corresponding ordered constraint Ord Date simplifies to: (Act To ≺ Act Date ∧ ¬(to.length = 0)). To form the full over-approximation constraint, we also include the linear order axioms, and MayTerminate, which in this case (when simplified) is simply the negation of the single abort trace in Act To : (Act From ≺ Act To ∧ ¬(from.length = 0)).

The call on line 12 will solve this combined constraint for both an order and values. The only valid order is From ≺ To ≺ Date. Suppose the returned values are To 1 = "A", From 1 = "A", and Date 1 = "01/01". The code is re-tested with these values, and symbolically traced, leading to the second alerts in both validate aux and validate date. This second trace is associated with local symbolic paths for each action, for example ¬(from.length = 0) ∧ from = to for Act To , which are added to the corresponding trees on line 15. In the second iteration of the while loop we would choose another unexplored path (line 11), and this would return, for example, the path ¬(from.length = 0)∧¬(from = to) from Act To . The ordered version of this path simplifies to: (Act From ≺ Act To ∧ ¬(from.length = 0) ∧ ¬(from = to)). This time, the MayTerminate constraint is required to avoid both aborts in Act Date . Thus, the full over-approximation constraint, omitting the linear order constraints, simplifies to:

[Act From ≺ Act To ∧ ¬(from.length = 0) ∧ ¬(from = to)] ∧ [Act To ≺ Act Date ∧ ¬(to.length = 0)] ∧ int(substr(date, 3, 5)) m 1 ∧ ∨ int(substr(date, 3, 5)) = m 1 int(substr(date, 0, 2)) d 1
where m 1 and d 1 are the concrete date and month observed during the execution.

A second call to the solver returns the ordering From ≺ To ≺ Date and values From 2 , To 2 , Date 2 , where From 2 and To 2 are distinct and non-empty, and Date 2 is later than the current date. These new values are tested, this time producing a trace which terminates in every action and successfully submits the form.

The completeness result is based on strong assumptions. It requires completeness of the solver, and requires the analysis to track all conditions symbolically. The code must also conform to the simple structure where form actions set their input variables but otherwise do not communicate with other actions. Real-world code does not obey these assumptions, but we can still apply Algorithm 2 to arbitrary code, tracking only the input fields symbolically across actions, while dropping the completeness guarantees.

Implementing concolic testing for form exploration

Implementing concolic testing in the Web context is challenging. First, one needs to control the browser, both to simulate user actions faithfully and ensure that the browser behaves deterministically from one iteration to the next. Frameworks such as Selenium WebDriver support this, but give limited control over certain low-level events such as timers and AJAX events. Second, we need to get information from the browser, and in particular need to analyze the executed code to record the symbolic paths taken. There are frameworks which can be used for symbolic tracing of stand-alone JavaScript, with the goal to help testing and debugging [START_REF] Sen | Jalangi: a tool framework for concolic testing, selective record-replay, and dynamic analysis of JavaScript[END_REF]. However, applying these to third-party JavaScript on the Web can be problematic, since they require instrumentation of the JavaScript source, which can be problematic when crawling third-party sites.

FormSolve's approach works directly with a browser engine. We build on top of WebKit, an open-source production Web browser engine, used by Apple's Safari browser. The browser engine includes page fetching, HTML and CSS rendering, and a JavaScript interpreter, but excludes the browser's user-interface. We instrument the source code to add hooks to control the browser, and we instrument the interpreter to perform symbolictracing, extending the WebKit interpreter to track a symbolic value with every concrete value. WebKit's JavaScript interpreter uses an internal JavaScript bytecode language, so our symbolic tracing works at the byte-code level, rather than the JavaScript source level. This simplifies the generated constraints.

The symbolic interpreter runs alongside WebKit's existing JavaScript interpreter and computes the symbolic values used in the analysis. When values are read from form fields, they are tagged as symbolic, and these symbolic values are propagated by the symbolic interpreter as the values are processed. A branch instruction is called symbolic if its branch condition uses any symbolic value. When a symbolic branch is encountered, its condition is recorded in the trace.

Symbolic values are created when certain properties of DOM objects are accessed by the site's JavaScript code. For example the value property of text fields, the checked property of checkboxes and radio buttons, or the value or selectedIndex properties of dropdown boxes. To make these DOM properties symbolic, WebKit's internal implementation of the DOM API is instrumented.

As well as the bytecode interpreter, JavaScript's built-in methods must also be instrumented. These are implemented by C++ methods in WebKit, which are modified in FormSolve to add an appropriate symbolic tag to the return value. We have only instrumented the functions which were most commonly used on the sites we were analysing. This reduces the implementation complexity, but also simplifies the generated constraints. Branch conditions which cannot easily be encoded as SMT constraints are dropped to make the analysis more concrete, thus allowing the analysis to continue past certain difficult functions or patterns.

Note that JavaScript library functions (such as from jQuery) are not built-ins and are implemented in JavaScript, so they are executed along with any other JavaScript code. They do not require special handling by the interpreter.

Example 4. We explain our symbolic tracing on this snippet from Example 1:

var from = document.getElementById("From").value; if (from.length == 0) { alert("Error: Departure Airport must be set"); } Table 1 shows the corresponding bytecode, the resulting register-level state change, and the changes in the symbolic state generated by the symbolic interpreter. For example, the first line of the table shows that the initial JavaScript command generates two bytecode instructions: op call r1 getElementById "from", which calls getElementById to look up the DOM node with identifier "from" (the From field) and store it in the register r1, followed by op get by id r2 r1 "value", which fetches the "value" property of that DOM for standalone (that is, not Web-based) JavaScript. We compared the tools on 1000 synthetic, randomly-generated standalone JavaScript programs. To generate the examples, we began with a context-free grammar for the program expressions, and then used a standard CFG-sampling algorithm [START_REF] Mckenzie | The generation of strings from a CFG using a functional language[END_REF] to generate random expressions from it. We then choose a random implementation for each operation in the generated program skeleton, choosing from a fixed set of simple JavaScript implementations. For example, for a term a ∧ b, we choose between a single-expression implementation combining the two child expressions, one which uses intermediate variables, and one using conditionals.

The aggregate results are shown in Table 2. We see that FormSolve explores many more paths than Jalangi. FormSolve benefits from symbolic instrumentation of a number of built-ins, native string operations, and datatype coercions which are not supported (and may be difficult to support) at the source level in Jalangi. There is also some benefit from FormSolve using CVC4, over the earlier version of CVC used by Jalangi.

Synthetic Web forms. The second goal was to test FormSolve's ability to deal with complex Web forms. We ran FormSolve on a suite of 1000 randomly generated test forms. The generator first produces a random form, and then supplements it with validation code using the JavaScript generator described above. Each field's validation code uses the value of its own field, and optionally those of other fields. The generated forms use an average of 8.57 form fields and 47.16 lines of JavaScript validation code. We compared FormSolve with two alternative approaches. Crawljax [10,[START_REF] Mesbah | Crawling Ajax-based Web applications through dynamic analysis of user interface state changes[END_REF] is an automatic crawler for dynamic websites which is based on a dynamic analysis of the Web application. In particular, Crawljax tracks changes to the state of the DOM, and explores user events until no more states can be discovered. In the absence of any domain knowledge, Crawljax can be seen as a state-of-the art approach to crawling complex websites, including Web forms. Artemis [START_REF]Artemis[END_REF][START_REF] Artzi | A framework for automated testing of JavaScript Web applications[END_REF] is a tool that does feedback-directing testing of websites. In each iteration, Artemis generates DOM and JavaScript events as well as values to enter in form fields. It uses metrics like line coverage to rank actions that are most promising for use in the next iteration. Each tool (FormSolve, Crawljax, Artemis) is run for a maximum of 50 iterations: for FormSolve, an iteration is defined as in Alg. 2; for Crawljax, it is a full run of the tool, until no new state is discovered-different iterations use different random seeds; for Artemis, an iteration is a predefined sequence of actions that is run in the browser. Iterations in Crawljax take a large amount of time and involve many browser interactions, while they are comparatively short in FormSolve and Artemis.

The results are shown in Table 3. The table includes line coverage of the eventhandling code, measured at the JavaScript source level, for all tools except Crawljax, which does not record this. The number of iterations for each example is taken to be that of the first submission, or the total if no submission was found. While not truly representative of the kinds of constraints found on real websites, these results do indicate that FormSolve can deal with complex constraints that do not obey the restricted global state assumptions our completeness result relies on, while also showing that prior methods do not suffice for complex constraints.

Real-world form validation. A more interesting benchmark is given by a set of simple real-world examples of Web forms. We used JSFiddle, a code-sharing website for Web-based code. Since form-related examples are not easily isolated in JSFiddle, we performed a Google search for "JSFiddle form validation". We extracted 18 examples, after removing those which did not perform JavaScript form validation. The examples were modified where necessary to allow them to be run in the tools with common submission and error behaviors. These test cases represent real-world forms; they use common JavaScript libraries and use complex constraints, but do not include the full complexity of real sites. There is no other content to contend with than the forms themselves.

We again compared FormSolve with Crawljax and Artemis, with results shown in Table 4. Some examples required only non-empty inputs; Artemis still has difficulty handling some of these, since it does not faithfully simulate the form-filling events triggered by a real user. FormSolve has a modest gain over Crawljax, handling several of the examples that require string comparisons.

The running time for FormSolve is dominated by a single example which uses string functions to parse an ID number, including a checksum; which took 30 minutes 45 seconds out of the total analysis time for all 18 examples of 37 minutes 25 seconds. This example (named VSKNx in our test data [START_REF]FormSolve test data[END_REF]) requires solving many difficult constraints over both strings and integers. At one point characters from the ID are converted to integers, multiplied by a constant, converted back to strings to extract the digits, which are then converted to integers and summed; and the analysis must solve a final integer constraint on the cumulative total of these sums. As such, FormSolve does not find a submission within 50 iterations. If left to run with no iteration limit, it is eventually able to find a valid ID number and successfully submit the form. In total, there were three examples which ran to the iteration limit, all of which can be solved with enough time.

Including those examples would bring FormSolve's successful submissions to 77.8%.

Impact of dynamic re-ordering. We compared Algorithm 2 to a variant of the algorithm where a fixed field order (taken from the field ordering in the DOM) is used. The experiments were conducted on the same set of 1000 synthetic forms described above. The JSFiddle examples are not tested, because they do not include interesting interactions between different fields' event handlers. For each configuration, we measured the line coverage as before, and also tracked whether we were able to generate a successful form submission. Note that as the examples are randomly generated, some of them have no valid inputs, and submission really is impossible. The results are shown in Table 5.

We observe that the big advantage of Algorithm 2 over a static ordering is pruning out explorations in one event handler which are known to abort in a later handler. The algorithm is able to prove that certain unexplored paths must later lead to abort actions, and therefore avoid wasted iterations. Trace execution is very expensive when testing real sites, so this is a significant advantage.

An example of this can be seen in the second part of the table. Algorithm 2 only attempted to explore 46.8% of the examples, compared to 69.8% for the static-ordering variant. In the cases explored by the static ordering algorithm but rejected by Algorithm 2 (23.0% of the total), the static ordering algorithm spent time exploring branches in certain event handlers which would all eventually lead to an abort action in a later handler. In contrast, Algorithm 2's calls to the constraint solver showed these branches to be futile, allowing the algorithm to ignore them. This explains the dramatic difference in the number of successful form submissions found in examples where multiple traces were explored (34.0% for the static order and 66.2% for Algorithm 2).

Real websites. Finally we experimented with 4 real airline websites that included complex validation rules. We report the numbers for the single-order mode discussed above. In that mode, FormSolve was able to find correct submissions while Crawljax could not (despite taking more than 16 hours in total) and Artemis could find only 2. An illuminating example is the archived website of AirTran Airways. The validation rules include that origin and destination must be entered, that there must be valid combinations of the number of children and adults (e.g., not more infants than adults), and that the departure and return dates must be ordered correctly and be no earlier than today's date. FormSolve finds 10 successes while exploring 207 code paths. Handling of the date and passenger constraints exercises the support for integer arithmetic in the solver. The Australian airline Rex has similar passenger restrictions, but in addition each departure airport allows a different set of arrival airports. FormSolve can find 458 distinct successful paths to submission, of a total of 1539 paths explored.

The real-world set is only anecdotal, due to our prototype's basis in the development version of WebKit, which limits its ability to run on recently-updated websites. Further, the dynamic reordering-mode has not yet been made sufficiently robust-for example, it has weaker support for restricting to user-realisable values. This causes it to miss half of the submissions found by the single-order mode on our small set of real-world sites. More thorough experiments with a more modern browser codebase will be needed to draw firm quantitative conclusions about the general applicability of our approach.

Conclusion

In this paper we make the first step at applying constraint-solving technology to finding valid submissions for Web forms. The approach has the advantage that it can be used not just to find single submissions but a representation of all valid submissions, in terms of a constraint; this is particularly relevant for wrapper-generation. Clearly this approach does not replace prior techniques of form-filling and wrapper generation, particularly in the presence of domain knowledge or a corpus of examples. Preliminary results with the FormSolve prototype show that the high-level approach, along with our bytecode-based implementation, has promise in practice. A full-featured implementation of bytecode-based symbolic tracing in a state-of-the-art browser remains a major engineering challenge. In the future we will look at variants of our approach with symbolic tracing at the JavaScript level, working with the code on-the-fly. Our benchmark generators and evaluation data are available on GitHub [START_REF]FormSolve test data[END_REF].

Table 2 .

 2 Comparing FormSolve with Jalangi on 1000 synthetic programs.

		FormSolve Jalangi
	Avg. distinct paths	5.75	2.54
	Avg. line coverage	91.49% 87.69%
	No. with full coverage	46.44% 37.05%

Table 3 .

 3 Results of FormSolve, Crawljax andArtemis on 1000 synthetic forms.

		FS	CJ	Ar
	Analysis time (s)	969 272 153 2 206
	Avg. iterations	1.86 40.95 43.29
	No. with full cov.	10.4%	-0.7%
	Forms submitted	31.4% 19.8% 17.7%

Table 4 .

 4 Results of FormSolve, Crawljax and Artemis on 18 JSFiddle examples.

		FS	CJ	Ar
	Analysis time (s)	2 245 6 509 319
	Avg. iterations	26.17 33.67 45.94
	Forms submitted	61.1% 33.3% 11.1%

Table 5 .

 5 Comparing Alg. 2 with single-order testing on 1000 synthetic forms.

		Single-order Alg. 2
	Analysis time (s)	585 969
	Avg. iterations	3.04 1.86
	No. with full coverage	4.7% 10.4%
	Forms submitted	24.1% 31.4%
	Multiple traces explored	69.8% 46.8%
	average line coverage	90.6% 95.5%
	no. with full coverage	6.7% 22.2%
	forms submitted	34.0% 66.2%

Table 1. JavaScript level, bytecode-level, and symbolic execution.

JavaScript code

WebKit bytecode Concrete state Symbolic state var from = document. getElementById("from").value;

op call r1 getElementById "from" r1 := DOM node From (none) op get by id r2 r1 "value" r2 := "" [value of From] r2 := SymStr("from") if (from.length == 0) op get by id r3 r2 "length" r3 := 0 [length of ""] r3 := StrLen(r2) op eq r4 r3 0 r4 := true [length is 0] r4 := IntOp(r3, I EQ, ConstInt(0)) op jfalse r4 else label [r4 is true; so no jump] b := BoolOp(r4, B EQ, ConstBool(false))

object (the empty string) and stores it in register r2. The symbolic instrumentation sets r2 to the symbolic value of the property lookup, which will be SymStr("from"), representing a symbolic input originating from a field with identifier "from".

Finding user-realizable values. Line 12 of Algorithm 2 uses the constraint solver to generate new input values. In the context of form filling, we want to avoid inputs that a user could not perform at the interface, since these are unlikely to produce a useful output.

We thus add additional constraints on the value space that enforce user realizability. HTML permits various types of input fields, each with their own restrictions on which values can be input. For example a select element produces a drop-down list with fixed options for the user to select from. To produce user-realizable input values, the analysis models these input fields to only generate values a user would be able to provide using a normal Web browser. This is done by encoding DOM facts as extra constraints which are included with each path condition.

Example 5. In the running example, the To field is implemented by a drop-down to choose between a set of airport codes: JFK, ORD, etc. In any constraint involving the corresponding variable to, we add a constraint saying to = JFK ∨ to = ORD ∨ . . ., where the list of codes is populated from the DOM. The client-side code may also check the index of the selected item, rather than its value. In this case, we add a variable to index to represent this index, which must correspond to the main to variable. In our example, the constraint would become (to = JFK∧to index = 1)∨(to = ORD∧to index = 2)∨. . ., forcing the solver to choose a matching index and value together.

Constraint solving. A critical component in the architecture is the constraint solver. In general, concolic testing requires a high-performance solver which supports standard program variable types: integers, Booleans, reals, bit-vectors, and arrays. Examples of solvers used for concolic testing or symbolic execution include Boolector [START_REF] Niemetz | Boolector 2.0 system description[END_REF], STP [START_REF] Ganesh | A decision procedure for bit-vectors and arrays[END_REF], Yices [START_REF] Dutertre | Yices 2.2[END_REF], and Z3 [START_REF] De | Z3: an efficient SMT solver[END_REF]. JavaScript requires very strong support for reasoning about strings. In particular, transformations between strings and other data types are common, so it is very useful if the solver supports these datatype coercions. We make use of CVC4, which supports a wide variety of theories compared with other solvers [START_REF] Cok | The 2014 SMT competition[END_REF], strong string support [START_REF] Liang | A DPLL(T) theory solver for a theory of strings and regular expressions[END_REF], as well as support for coercions between different theories.

Experimental Evaluation

Standalone JavaScript code. The first goal of our evaluation is to compare our bytecodebased code exploration with alternatives based on JavaScript source. We compared against Jalangi [START_REF] Jalangi | [END_REF][START_REF] Sen | Jalangi: a tool framework for concolic testing, selective record-replay, and dynamic analysis of JavaScript[END_REF], a framework for JavaScript testing that includes concolic testing