Ahmad Salim

Thomas P Jensen

Aleksandar S Dimovski

Andrzej Wąsowski

Ahmad Salim Al-Sibahi

Verification of Program Transformations with Inductive Refinement Types *

Keywords: CCS Concepts:, Theory of computation → Program verification, Program analysis, Abstraction, Functional constructs, Program schemes, Operational semantics, Control primitives, • Software and its engineering → Translator writing systems and compiler generators, Semantics, transformation languages, abstract interpretation, static analysis

High-level transformation languages like Rascal include expressive features for manipulating large abstract syntax trees: first-class traversals, expressive pattern matching, backtracking and generalized iterators. We present the design and implementation of an abstract interpretation tool, Rabit, for verifying inductive type and shape properties for transformations written in such languages. We describe how to perform abstract interpretation based on operational semantics, specifically focusing on the challenges arising when analyzing the expressive traversals and pattern matching. Finally, we evaluate Rabit on a series of transformations (normalization, desugaring, refactoring, code generators, type inference, etc.) showing that we can effectively verify stated properties.

INTRODUCTION

Transformations play a central role in software development. Examples include desugaring, model transformations, refactoring, and code generation. The artifacts involved in transformations-e.g., structured data, domain-specific models, and code-often have large abstract syntax, spanning hundreds of syntactic elements, and a correspondingly rich semantics. Writing transformations is thus a tedious and error-prone process. Specialized languages and frameworks with high-level features have been developed to address this challenge of writing and maintaining transformations. These languages include Rascal [START_REF] Klint | EASY Meta-programming with Rascal[END_REF], Stratego/XT [START_REF] Bravenboer | [END_REF], TXL [START_REF] Cordy | The TXL source transformation language[END_REF], Uniplate [START_REF] Mitchell | Uniform boilerplate and list processing[END_REF] for Haskell, and Kiama [START_REF] Anthonym | Lightweight Language Processing in Kiama[END_REF] for Scala. For example, Rascal combines a functional core language supporting state and exceptions, with constructs for processing of large structures. Figure 1 shows an example Rascal transformation program taken from a PHP analyzer. 1 This transformation program recursively flattens all blocks in a list of statements. The program uses the following core Rascal features: • A visitor (visit) to traverse and rewrite all statement lists containing a block to a flat list of statements. Visitors support various strategies, like the bottom-up strategy that traverses the abstract syntax tree starting from leaves toward the root. • An expressive pattern matching language is used to non-deterministically find blocks inside a list of statements. The starred variable patterns *xs and *zs match arbitrary number of elements in the list, respectively before and after the block(ys) element. Rascal supports non-linear matching, negative matching and specifying patterns that match deeply nested values. • The solve-loop (solve) performing the rewrite until a fixed point is reached (the value of 𝑠 stops changing).

To rule out errors in transformations, we propose a static analysis for enforcing type and shape properties, so that target transformations produce output adhering to particular shape constraints.

For our PHP example, this would include:

• The transformation preserves the constructors used in the input: does not add or remove new types of PHP statements. • The transformation produces flat statement lists, i.e., lists that do not recursively contain any block.

To ensure such properties, a verification technique must reason about shapes of inductive dataalso inside collections such as sets and maps-while still maintaining soundness and precision. It must also track other important aspects, like cardinality of collections, which interact with target language operations including pattern matching and iteration.

In this paper, we address the problem of verifying type and shape properties for high-level transformations written in Rascal and similar languages. We show how to design and implement a static analysis based on abstract interpretation. Concretely, our contributions are:

(1) An abstract interpretation-based static analyzer-Rascal ABstract Interpretation Tool (Rabit)that supports inferring types and inductive shapes for a large subset of Rascal. (2) An evaluation of Rabit on several program transformations: two refactorings, desugaring, two normalization procedures, derivative calculator, modernization transformation, code generator, and language implementation of an expression language. (3) A modular design for abstract shape domains, that allows extending and replacing abstractions for concrete element types, e.g. extending the abstraction for lists to include length in addition to shape of contents. (4) Schmidt-style abstract operational semantics [START_REF] Schmidt | Trace-Based Abstract Interpretation of Operational Semantics[END_REF] for a significant subset of Rascal adapting the idea of trace memoization to support arbitrary recursive calls with input from infinite domains. The main changes in our contributions in this journal extension are [START_REF] Salim | Verification of high-level transformations with inductive refinement types[END_REF]:

(1) A significant extension of the number of evaluation cases (from 5 to 9) and properties (from 15 to 24). The new properties explore better interactions with abstractions on integers, iteration, conditioning using if-statements and maps. (2) An explication of the effect of pragmatic choices regarding trace partitioning and trace memoization in our implementation. We now run our evaluation under 2 × 3 configurations exploring choices on trace partitioning (on/off) and widening domain for trace memoization (simple/type-based/constructor-based). We further provide a new extended discussion on these effects in the evaluation. [START_REF] Salim | Symbolic execution of high-level transformations[END_REF] We now look into the statistics of the operations of trace memoization (hit/miss/widen) during execution. We compare the effects to the execution time and configuration choice. Together, these contributions show feasibility of applying abstract interpretation for constructing analyses for expressive transformation languages and properties.

We proceed by presenting a running example in Sect. 2. We introduce the key constructs of Rascal in Sect. [START_REF] Salim | Symbolic execution of high-level transformations[END_REF]. Section 4 describes the modular construction of abstract domains. Sections 5 to 8 describe abstract semantics. We evaluate the analyzer on realistic transformations, reporting results in Sect. 9. Sections 10 and 11 discuss related papers and conclude.

MOTIVATION AND OVERVIEW

Verifying types and state properties such as the ones stated for the program of Fig. 1 poses the following key challenges:

• The programs use heterogeneous inductive data types that can contain collections (lists, maps and sets), and basic data (integers, strings, etc.). Modelling these types precisely requires us to construct sophisticated abstract domains that capture the mutual interaction between the different types. • The traversal of syntax trees depends heavily on the type and shape of input, on a complex program state, and involves unbounded recursion. This makes it challenging to approximate required invariants in a away that is both sufficiently precise and terminating. • Backtracking and exceptions in large programs introduce the possibility of state-dependent non-local jumps. This makes it difficult to statically calculate the control flow of target programs and have a compositional denotational semantics, instead of an operational one.

Figure 2 presents a small pedagogical example using visitors. The program performs expression simplification by traversing a syntax tree bottom-up and reducing multiplications by constant zero. We use this example to explain the analysis techniques contributed in this paper.

Inductive Refinement Types. Rabit is a static analysis tool that given the shape of possible inputs (any expression of type Expr in this case), infers the shape of possible outputs. It infers inductive refinement types by interpreting the simplification program abstractly, considering all possible paths the program can take. The result of running Rabit on this case is:

success cst (Nat) ≀ var (str) ≀ mult (Expr ′ , Expr ′ ) fail cst (Nat) ≀ var (str) ≀ mult (Expr ′ , Expr ′ )
where Expr ′ = cst (suc (Nat)) ≀ var (str) ≀ mult (Expr ′ , Expr ′ ).

We briefly interpret how to read this type. The bar ≀ denotes a choice between alternative constructors. If the input was rewritten during traversal (success, the first line) then the resulting syntax tree contains no multiplications by zero. Observe how the last alternative mult (Expr ′ , Expr ′ ) contains only expressions of type Expr ′ , which in turn only allows multiplications by constants constructed using suc (Nat) (that is ≥ 1). If the traversal failed to match (fail, the second line), then the input did not contain any multiplication by zero to begin with and so does not the output, which has not been rewritten.

The success and failure cases happen to be the same for our example, but this is not necessarily always the case. Keeping separate result values allows retaining precision throughout the traversal, and better reflects concrete execution paths. We now proceed discussing how Rabit can infer this shape using abstract interpretation.

Abstractly Interpreting Traversals. The core idea of abstractly executing a traversal is similar to concrete execution: we recursively traverse the input structure and rewrite the values that match target patterns. However, because the input is abstracted, we must make sure to take into account all applicable paths. Figure 3 shows the execution tree of the traversal on the simplification example (Fig. 2) when it starts with shape mult (cst (Nat) , cst (Nat)). Since there is only one constructor, it will initially recurse down to traverse the contained values (children) creating a new recursion node (yellow, light shaded) in the figure (ii) containing the left child cst (Nat), and then recurse again to create a node (iii) containing Nat. Observe here that Nat is an abstract type with two possible constructors (zero, suc (•)), and it is unknown at time of abstract interpretation, which of these constructors we have. When Rabit hits a choice between alternative constructors, it explores each alternative separately creating new partition nodes (blue, darker). In our example we partition the Nat type into its constructors zero (node iv) and suc (Nat) (node v). The zero case now represents the first case without children and we can run the visitor operations on it. Since no pattern matches zero it will return a fail zero result indicating that it has not been rewritten. For the suc (Nat) case it will try to recurse down to Nat (node vi) which is equal to (node iii). We observe a problem: if we continue our traversal algorithm as is, we will not terminate and get a result. To provide a terminating algorithm we will resort to using trace memoization.

Partition-driven Trace Memoization. The idea is to detect paths where execution recursively meets similar input, merging the new recursive node with the similar previous one, thus creating a loop in the execution graph [START_REF] Rosendahl | Abstract Interpretation as a Programming Language[END_REF][START_REF] Schmidt | Trace-Based Abstract Interpretation of Operational Semantics[END_REF]. This loop is then resolved by a fixed-point iteration.

In Rabit, we propose partition-driven trace memoization, which works with potentially unbounded input like the inductive type refinements. We detect cycles by maintaining a memoization map which for each type-used for partitioning-stores the last traversed value (input) and the last result produced for this value (output). This memoization map is initialized to map all types to the bottom element (⊥) for both input and output. The evaluation is modified to use the memoization map, so it checks on each iteration the input 𝑖 against the map:

• If the last processed refinement type representing the input 𝑖 ′ is greater than the current input (𝑖 ′ ⊒ 𝑖), then it uses the corresponding output; i.e., we found a hit in the memoization map. • Otherwise, it will merge the last processed and current input refinement types to a new value 𝑖 ′′ = 𝑖 ′ ∇𝑖, update the memoization map and continue execution with 𝑖 ′′ . The operation ∇ is called a widening; it ensures that the result is an upper bound of its inputs, i.e., 𝑖 ′ ⊑ 𝑖 ′′ ⊒ 𝑖 and that the merging will eventually terminate for the increasing chain of values. The memoization map is updated to map the general type of 𝑖 ′′ (not refined, for instance Nat) to map to a pair (𝑖 ′′ , 𝑜), where the first component denotes the new input 𝑖 ′′ refinement type and the second component denotes the corresponding output 𝑜 refinement type; initially, 𝑜 is set to ⊥ and then changed to the result of executing input 𝑖 ′′ repeatedly until a fixed-point is reached.

We demonstrate the trace memoization and fixed-point iteration procedures on Nat in Fig. 4, beginning with the leftmost tree. The expected result is fail Nat, meaning that no pattern has matched, no rewrite has happened, and a value of type Nat is returned, since the simplification program only introduces changes to values of type Expr.

We show the memoization map inside a framed orange box. The result of the widening is presented below the memoization map. In all cases the widening in Fig. 4 is trivial, as it happens against ⊥. The final line in node 1 stores the value 𝑜 prev produced by the previous iteration of the traversal, to establish whether a fixed point has been reached (⊥ initially).

Trace Partitioning. We partition [START_REF] Rival | The trace partitioning abstract domain[END_REF] the abstract value Nat along its constructors: zero and suc (•) (Fig. 4). This partitioning is key to maintain precision during the abstract interpretation. As in Fig. 3, the left branch fails immediately, since no pattern in Fig. 2 matches zero. The right branch descends into a new recursion over Nat, with an updated memoization table. This run terminates, due to a hit in the memoization map, returning ⊥. After returning, the value of suc (Nat) should be reconstructed with the result of traversing the child Nat, but since the result is ⊥ there is no value to reconstruct with, so ⊥ is just propagated upwards. At the return to the last widening node, the values are joined, and widen the previous iteration result 𝑜 prev (the dotted arrow on top). This process repeats in the second and third iterations, but now the reconstruction in node 3 succeeds: the child Nat is replaced by zero and fail suc (zero) is returned (dashed arrow from 3 to 1). In the third iteration, we join and widen the following components (cf. 𝑜 prev and the dashed arrows incoming into node 1 in the rightmost column):

Expr ↦ →𝑒 ≀ cst (Nat) , fail cst (Nat) Nat ↦ → ⊥, ⊥ 8 input: cst (Nat) Expr ↦ →𝑒 ≀ cst (Nat) , fail cst (Nat) Nat ↦ → ⊥, ⊥
[zero ≀ suc (zero) ∇ (zero ⊔ suc (zero≀suc (zero)))] = Nat
Here, the used widening operator [START_REF] Cousot | Formal Language, Grammar and Set-Constraint-Based Program Analysis by Abstract Interpretation[END_REF] accelerates the convergence by increasing the value to represent the entire type Nat. It is easy to convince yourself, by following the same recursion steps as in the figure, that the next iteration, using 𝑜 prev = Nat will produce Nat again, arriving at a fixed point. Observe, how consulting the memoization map, and widening the current value accordingly, allowed us to avoid infinite recursion over unfoldings of Nat.

Nesting Fixed Point Iterations. When inductive shapes (e.g., Expr) refer to other inductive shapes (e.g., Nat), it is necessary to run nested fixed-point iterations to solve recursion at each level. Figure 5 returns to the more high-level fragment of the traversal of Expr starting with mult (cst (Nat) , cst (Nat)) as in Fig. 3. We follow the recursion tree along nodes 5, 6, 7, 8, 9, 10, 9, 6 with the same rules as in Fig. 4. In node 10 we run a nested fixed point iteration on Nat, already discussed in Fig. 4, so we just include the final result.

Type Refinement. The output of the first iteration in node 6 is fail cst (Nat), which becomes the new 𝑜 prev , and the second iteration begins (to the right). After the widening the input is partitioned into 𝑒 (node 7) and cst (Nat)(node elided). When the second iteration returns to node 7 we have the following reconstructed value: mult (cst (Nat) , cst (Nat)). Contrast this with lines 6-7 in Fig. 2, to see that running the abstract value against this pattern might actually produce success. In order to obtain precise result shapes, we refine the input values when they fail to match a pattern. Our abstract interpreter produces a refinement of the type, by running it through the pattern matching, giving:

success cst (Nat) fail mult (cst (suc (Nat)) , cst (suc (Nat)))
The result means, that if the pattern match succeeds then it produces an expression of type cst (Nat). More interestingly, if the matching failed neither the left nor the right argument of mult (•, •) could have contained the constant zero-the interpreter captured some aspect of the semantics of the program by refining the input type. Naturally, from this point on the recursion and iteration continues, but we shall abandon the example, and move on to formal developments.

FORMAL LANGUAGE

The presented technique is meant to be general and applicable to many high-level transformation languages. To keep the presentation concise, we focus on few key constructs from Rascal [START_REF] Klint | EASY Meta-programming with Rascal[END_REF], relying on the concrete semantics from Rascal Light [START_REF] Salim | The Formal Semantics of Rascal Light[END_REF].

We consider algebraic data types (at) and finite sets (set⟨𝑡⟩) of elements of type 𝑡. Each algebraic data type at has a set of unique constructors. Each constructor 𝑘 (𝑡) has a fixed set of typed parameters. The language includes sub-typing, with void and value as bottom and top types respectively.

𝑡 ∈ Type void | set⟨𝑡⟩ | at | value
We consider the following subset of Rascal expressions: From left to right we have: variable access, assignments, sequencing, constructor expressions, set literal expressions, matching failure expression, and bottom-up visitors:

𝑒 𝑥 ∈ Var | 𝑥 = 𝑒 | 𝑒; 𝑒 | 𝑘 (𝑒) | {𝑒} | fail | visit 𝑒 cs cs case 𝑝 ⇒ 𝑒
Visitors are a key construct in Rascal. A visitor visit 𝑒 cs traverses recursively the value obtained by evaluating 𝑒 (any combination of simple values, data type values and collections). During the traversal, case expression cs are applied to the nodes, and the values matching target patterns are rewritten. We will discuss a concrete subset of patterns 𝑝 further in Sect. 6. For brevity, we only discuss bottom-up visitors, but Rabit (Sect. 9) supports all strategies of Rascal.

Notation. We write (𝑥, 𝑦) ∈ 𝑓 to denote the pair (𝑥, 𝑦) such that 𝑥 ∈ dom 𝑓 and 𝑦 = 𝑓 (𝑥). Abstract semantic components, sets, and operations are marked with a hat: 𝑎. A sequence of 𝑒 1 , . . . , 𝑒 𝑛 is contracted using an underlining 𝑒. The empty sequence is written by 𝜀, and concatenation of sequences 𝑒 1 and 𝑒 2 is written 𝑒 1 , 𝑒 2 . Notation is lifted to sequences in an intuitive manner: for example given a sequence 𝑣, the value 𝑣 𝑖 denotes the 𝑖th element in the sequence, and 𝑣 :𝑡 denotes the sequence 𝑣 1 :𝑡 1 , . . . , 𝑣 𝑛 :𝑡 𝑛 .

ABSTRACT DOMAINS

Our abstract domains are designed to compose modularly. Modularity is important for transformation languages, which manipulate a large variety of values. The design allows easily replacing abstract domains for particular types of values, as well as adding support for new types. We want to construct an abstract value domain vs ∈ ValueShape which captures inductive refinement types of form:

at 𝑟 = 𝑘 1 ( vs 1 ) ≀ • • • ≀ 𝑘 n ( vs n )
where each value vs 𝑖 can possibly recursively refer to at 𝑟 . Below, we define abstract domains for sets, data types and recursively defined domains. The modular domain design generalizes parameterized domains [START_REF] Cousot | Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday[END_REF] to follow a design inspired by the modular construction of types and domains [START_REF] Benke | Universes for Generic Programs and Proofs in Dependent Type Theory[END_REF][START_REF] Chapman | The gentle art of levitation[END_REF][START_REF] Scott | Data Types as Lattices[END_REF]. The idea is to define domains parametrically-i.e. in the form F( E)-so that abstract domains for subcomponents are taken as parameters, and explicit recursion is handled separately. We use standard domain combinators [START_REF] Winskel | Information Systems[END_REF] to combine individual domains into the abstract value domain.

Set Shape Domain. Let Set(E) denote the domain of finite sets consisting of elements taken from E. We define abstract finite sets using abstract elements { 𝑒} [𝑙;𝑢 ] from a parameterized domain SetShape( E). The component from the parameter domain ( 𝑒 ∈ E) represents the abstraction of the shape of elements, and a non-negative interval component [𝑙; 𝑢] ∈ Interval + is used to abstract over the cardinality (so 𝑙, 𝑢 ∈ R + and 𝑙 ≤ 𝑢). The abstract set element acts as a reduced product between 𝑒 and [𝑙; 𝑢] and the lattice operations follow directly.

Given a concretization function for the abstract content domain 𝛾 E ∈ E → ℘ (E), we can define a concretization function for the abstract set shape domain to possible finite sets of concrete elements

𝛾 SS ∈ SetShape( E) → ℘ (Set (E)): 𝛾 SS ({ 𝑒} [𝑙;𝑢 ] ) = es es ⊆ 𝛾 E ( 𝑒) ∧ |es| ∈ 𝛾 I ( [𝑙; 𝑢]) Example 4.1.
Let Interval be a domain of intervals of integers (a standard abstraction over integers). We can concretize abstract elements from SetShape( Interval) to a set of possible sets of integers from ℘ (Set (Z)) as follows:

𝛾 SS ({[42; 43]} [1;2] ) = {{42}, {43}, {42, 43}}
Data Shape Domain. Inductive refinement types are defined as a generalization of refinement types [START_REF] Freeman | Refinement Types for ML[END_REF][START_REF] Rushby | Subtypes for Specifications: Predicate Subtyping in PVS[END_REF][START_REF] Xi | Eliminating Array Bound Checking Through Dependent Types[END_REF] that inductively constrain the possible constructors and the content in a data structure. We use a parameterized abstraction of data types DataShape( E), whose parameter E abstracts over the shape of constructor arguments:

𝑑∈ DataShape( E) = {⊥ DS } ∪ {𝑘 1 (𝑒 1 )≀ . . . ≀𝑘 n (𝑒 n ) | 𝑒 𝑖 ∈ E} ∪ {⊤ DS }
We have the least element ⊥ DS and top element ⊤ DS elements-respectively representing no data types value and all data type values-and otherwise a non-empty choice between unique (all different) constructors of the same algebraic data type

𝑘 1 (𝑒 1 ) ≀ • • • ≀ 𝑘 n (𝑒 n ) (shortened 𝑘 (𝑒)).
We can treat the constructor choice as a finite map [𝑘 1 ↦ → 𝑒 1 , . . . , 𝑘 n ↦ → 𝑒 n ], and then directly define our lattice operations point-wise.

Given a concretization function for the concrete content domain 𝛾 E ∈ E → ℘ (E), we can create a concretization function for the data shape domain

𝛾 DS ∈ DataShape( E) → ℘ (Data(E))
where Data(E) = 𝑘 (𝑣) ∃ a type at. 𝑘 (𝑣) ∈ at ∧ 𝑣 ∈ E . The concretization is defined as follows:

𝛾 DS (⊥ DS ) = ∅ 𝛾 DS (⊤ DS ) = Data(E) 𝛾 DS (𝑘 1 (𝑒 1 ) ≀ • • • ≀ 𝑘 n (𝑒 n )) = 𝑘 𝑖 (𝑣) 𝑖 ∈ [1, n] ∧ 𝑣 ∈ 𝛾 E (𝑒 𝑖 ) Example 4.2.
We can concretize abstract data elements DataShape( Interval) to a set of possible concrete data values ℘ (Data(Z)). Consider values from the algebraic data type:

data errorloc = repl() | linecol(int, int)
We can concretize abstracting elements as follows:

𝛾 DS (repl() ≀ linecol( [1; 1], [3; 4])) = {repl(), linecol(1, 3), linecol(1, 4)}
Recursive shapes. We extend our abstract domains to cover recursive structures such as lists and trees. Given a type expression F(𝑋 ) with a variable 𝑋 , we construct the abstract domain as the solution to the recursive equation 𝑋 = F(𝑋 ) [START_REF] Scott | Data Types as Lattices[END_REF][START_REF] Michael | The Category-Theoretic Solution of Recursive Domain Equations[END_REF][START_REF] Winskel | Information Systems[END_REF], obtained by iterating the induced map F over the singleton domain 1 = {⊥}. The concretization function of the recursive domain follows from the concretization function of the underlying functor domain. A detailed exposition of how to solve recursive equations over abstract domains is presented in Al-Sibahi et al. [START_REF] Salim | Galois Connections for Recursive Types[END_REF].

Example 4.3. We can concretize abstract elements of the refinement type from our running example:

𝛾 DS (Expr 𝑒 ) =          2 cst(suc(suc(zero))), mult(2, 2), mult(mult(2, 2), 2), . . .         
where Expr 𝑒 = cst(suc(suc(zero))) ≀ mult(Expr 𝑒 , Expr 𝑒 ) In particular, our abstract element represents the set of all multiplications of the constant 2.

Value Domains. We presented the required components for abstracting individual types, and now all that is left is putting everything together. We construct our value shape domain using choice and recursive domain equations:

ValueShape = SetShape( ValueShape) ⊕ DataShape( ValueShape)
Similarly, we have the corresponding concrete shape domain:

Value = Set (Value) ⊎ Data(Value)
We then have a concretization function 𝛾 VS ∈ ValueShape → ℘ (Value), which follows directly from the previously defined concretization functions.

Abstract State Domains

We now explain how to construct abstractions of states and results when executing Rascal programs. Abstract Store Domain. Tracking assignments of variables is important since matching variable patterns depends on the value being assigned in the store:

𝜎 ∈ Store = Var → {ff, tt} × ValueShape
For a variable 𝑥 we get 𝜎 (𝑥) = (𝑏, vs) where 𝑏 is true if 𝑥 might be unassigned, and false otherwise (when 𝑥 is definitely assigned). The second component, vs is a shape approximating a possible value of 𝑥.

We lift the orderings and lattice operations point-wise from the value shape domain to abstract stores. We define the concretization function 𝛾 Store ∈ Store → ℘ (Store) as:

𝛾 Store ( 𝜎) = 𝜎 ∀𝑥, 𝑏, vs. 𝜎 (𝑥) = (𝑏, vs) ⇒ (¬𝑏 ⇒ 𝑥 ∈ dom 𝜎) ∧ (𝑥 ∈ dom 𝜎 ⇒ 𝜎 (𝑥) ∈ 𝛾 V ( vs))
Abstract Result Domain. Traditionally, abstract control flow is handled using a collecting denotational semantics with continuations, or by explicitly constructing a control flow graph. These methods are non-trivial to apply for a rich language like Rascal, especially considering backtracking, exceptions and data-dependent control flow introduced by visitors. A nice side-effect of Schmidt-style abstract interpretation is that it allows abstracting control flow directly.

We model different type of results-successes, pattern match failures, errors directly in a ResSet domain which keeps track of possible results with each its own separate store. Keeping separate stores is important to maintain precision around different paths:

rest ∈ ResType success | exres exres fail | error resv ∈ ResVal • | vs Res ∈ ResSet = ResType ⇀ ResVal × Store
The lattice operations are lifted directly from the target value domains and store domains. We define the concretization function

𝛾 RS ∈ ResultSet → ℘ (Result × Store): 𝛾 RS ( Res) = (rest resv, 𝜎) (rest, ( resv, 𝜎)) ∈ Res ∧ resv ∈ 𝛾 RV ( resv) ∧ 𝜎 ∈ 𝛾 Store ( 𝜎)

ABSTRACT SEMANTICS

A distinguishing feature of Schmidt-style abstract interpretation is that the derivation of abstract operational rules from a given concrete operational semantics is systematic and to a large extent mechanisable [START_REF] Bodin | Certified Abstract Interpretation with Pretty-Big-Step Semantics[END_REF][START_REF] Schmidt | Trace-Based Abstract Interpretation of Operational Semantics[END_REF]. The creative work is largely (1) providing abstract definitions for conditions, (2) abstract semantic operations like pattern matching, and (3) defining trace memoization strategies for non-structurally recursive operational rules. Figure 6 relates the concrete evaluation judgment (left) to the abstract evaluation judgment (right) for Rascal expressions. Both judgements evaluate the same expression 𝑒. The abstract evaluation judgment abstracts the initial concrete store 𝜎 with an abstract store 𝜎. The result of the abstract evaluation is a finite result set Res, abstracting over possibly infinitely many concrete result values rest resv and stores 𝜎 ′ . Res maps each result type rest to a pair of abstract result value resv and abstract result store 𝜎 ′ , i.e.:

Res = [rest 1 ↦ → ( resv 1 , 𝜎 1 ), . . . , rest n ↦ → ( resv n , 𝜎 n )]
There is an important difference in how the concrete and abstract semantic rules are used. In a concrete operational semantics a language construct is usually evaluated as soon as the premises of a rule are satisfied. When evaluating abstractly, we must consider all applicable rules, to soundly over-approximate the possible concrete executions. To this end, we introduce a special notation to collect all derivations with the same input 𝑖 into a single derivation with output 𝑂 equal to the join of the individual outputs:

{|𝑖 ⇒ 𝑂| } ≜ 𝑂 = {𝑜 |𝑖 ⇒ 𝑜}
Let's use the operational rules for variable accesses to illustrate the steps in Schmidt-style translation of operational rules. The concrete semantics contains two rules for variable accesses, E-V-S for successful lookup, and E-V-Er for producing errors when accessing unassigned variables:

E-V-S 𝑥 ∈ dom 𝜎 𝑥; 𝜎 = == ⇒ expr success 𝜎 (𝑥); 𝜎 E-V-Er 𝑥 ∉ dom 𝜎 𝑥; 𝜎 = == ⇒ expr error; 𝜎
We follow three steps, to translate the concrete rules to abstract operational rules:

(1) For each concrete rule, create an abstract rule that uses a judgment for evaluation of a syntactic form, e.g., AE-V-S and AE-V-Er for variables. (2) Replace the concrete conditions and semantic operations with the equivalent abstract conditions and semantic operations for target abstract values, e.g. 𝑥 ∈ dom 𝜎 with 𝜎 (𝑥) = (𝑏, 𝑣𝑠) and a check on 𝑏. We obtain two execution rules:

AE-V-S 𝜎 (𝑥) = (𝑏, vs) 𝑥; 𝜎 = ===== ⇒ a-expr-v [success ↦ → ( vs, 𝜎)] AE-V-ER 𝜎 (𝑥) = (tt, vs) 𝑥; 𝜎 = ===== ⇒ a-expr-v [error ↦ → (•, 𝜎)]
Observe when 𝑏 is true, both a success and failure may occur, and we need rules to cover both cases. (3) Create a rule that collects all possible evaluations of the syntax-specific judgment rules, e.g. AE-V for variables:

AE-V {|𝑥; 𝜎 = ===== ⇒ a-expr-v Res ′ | } 𝑥; 𝜎 = === ⇒ a-expr Res ′
The possible shapes of the result value depend on the pair assigned to 𝑥 in the abstract store. If the value shape of 𝑥 is ⊥, we drop the success result from the result set. The following examples illustrate the possible outcome result shapes:

Assigned Value Result Set Rules 𝜎 (𝑥) = (ff, ⊥ VS ) [] AE-V-S 𝜎 (𝑥) = (ff, [1; 3]) [success ↦ → ([1; 3], 𝜎)] AE-V-S 𝜎 (𝑥) = (tt, ⊥ VS ) [error ↦ → (•, 𝜎)] AE-V-S, AE-V-Er 𝜎 (𝑥) = (tt, [1; 3]) [success ↦ → ([1; 3], 𝜎), error ↦ → (•, 𝜎)] AE-V-S, AE-V-Er , Vol. 1, No. 1, Article . Publication date: March 2020.
It is possible to translate the operational semantics rules for other basic expressions using the presented steps (see Appendix B). The core changes are the ones moving from checks of definiteness to checks of possibility. For example:

• Checking that evaluation of 𝑒 has succeeded, requires that the abstract semantics uses

𝑒; 𝜎 = === ⇒ a-expr
Res and (success, ( vs, 𝜎 ′ )) ∈ Res, as compared to 𝑒; 𝜎 = == ⇒ expr success 𝑣; 𝜎 ′ in the concrete semantics.

• Typing is now done using abstract judgments vs : 𝑡 and 𝑡 <: 𝑡 ′ . In particular, type 𝑡 is an abstract subtype of type 𝑡 ′ (𝑡 <: 𝑡 ′ ) if there is a subtype 𝑡 ′′ of 𝑡 (𝑡 ′′ <: 𝑡) that is also a subtype of 𝑡 ′ (𝑡 ′′ <: 𝑡 ′ ). This implies that 𝑡 <: 𝑡 ′ and 𝑡 ≮: 𝑡 ′ are non-exclusive.

• To check whether a result contains a particular constructor, we use the abstract function unfold( vs, 𝑡). unfold( vs, 𝑡) will produces a refined set of abstract values of type 𝑡 based on vs, splitting alternative constructors. Additionally, it produces error if the value is possibly not an element of 𝑡.

PATTERN MATCHING

Expressive pattern matching is a key feature of Rascal, and Rabit handles the full pattern language of Rascal. For brevity, we discuss a subset, including variables 𝑥, constructor patterns 𝑘 (𝑝), and set patterns {★𝑝}:

𝑝 𝑥 | 𝑘 (𝑝) | {★𝑝} ★𝑝 𝑝 | ★𝑥
Rascal allows non-linear matching where the same variable 𝑥 can be mentioned more than once: all values matched against 𝑥 must have equal values for the match to succeed. Each set pattern contains a sequence of sub-patterns ★𝑝; each sub-pattern in the sequence is either an ordinary pattern 𝑝 matched against a single set element, or a star pattern ★𝑥 to be matched against a subset of elements. Star patterns can backtrack when pattern matching fails because of non-linear variables, or when explicitly triggered by the fail expression. This expressiveness poses challenges for developing an abstract interpreter that is both sound and sufficiently precise. The key aspects of Rabit in handling pattern matching is how we maintain precision by refining input values on pattern matching successes and failures.

Satisfiability Semantics for Patterns

We begin by defining what it means that a (concrete/abstract) value matches a pattern. Figure 7a shows the concrete semantics for patterns. In the figure, 𝜌 is a binding environment:

𝜌 ∈ BindingEnv = Var ⇀ Value
A value 𝑣 matches a pattern 𝑝 (𝑣 |= 𝑝) iff 𝑣 is accepted by the satisfiability semantics (defined in Fig. 7a) give a binding environment 𝜌 that maps the variables in the pattern to values in dom 𝜌 = vars(𝑝).

Constructor patterns 𝑘 (𝑝) accept any well-typed value 𝑘 (𝑣) of the same constructor, and whose subcomponents 𝑣 match the sub-patterns 𝑝 in a consistent fashion using the same binding environment 𝜌. A variable 𝑥 matches exactly the value it is bound to in the binding environment 𝜌. A set pattern {★𝑝} accepts any set of values {𝑣 } such that an associative-commutative arrangement of the sub-values 𝑣 matches the sequence of sub-patterns ★𝑝 under 𝜌.

A value sequence 𝑣 matches a pattern sequence ★𝑝 (𝑣 |= ★ ★𝑝) if there exists a binding environment 𝜌 such that dom 𝜌 = vars(★𝑝) and 𝑣 |= ★ 𝜌 ★𝑝. An empty sequence of patterns 𝜀 accepts an empty sequence of values 𝜀. A sequence starting 𝑝, ★𝑝 ′ with an ordinary pattern 𝑝 matches any non-empty sequence of values 𝑣, 𝑣 ′ where 𝑣 matches 𝑝 and 𝑣 ′ matches ★𝑝 ′ in a consistent fashion using the We see that the first conjunct matches as follows:

mult (cst (zero) , cst (suc (zero))) |= 𝜌 mult (𝑥, 𝑦) iff cst (zero) , cst (suc (zero)) |= ★ 𝜌 𝑥, 𝑦 iff 𝜌 (𝑥) = cst (zero) and 𝜌 (𝑦) = cst (suc (zero))
Similarly, the second matches as follows:

cst (zero) |= ★ 𝜌 ★𝑤, 𝑥 iff 𝜌 (𝑤) = {} and 𝜌 (𝑥) = cst (zero)
The abstract pattern matching semantics (Fig. 7b) is analogous, but with a few noticeable differences. First, an abstract value vs matches a pattern 𝑝 ( vs |= 𝑝) if there exists a more precise value vs ′ (so vs ′ ⊑ vs) and an abstract binding environment 𝜌 with dom 𝜌 = vars(𝑝) so that vs ′ |= 𝜌 𝑝. The reason for using a more precise shape is the potential loss of information during over-approximation-a more precise value might have matched the pattern, even if the relaxed value does not necessarily. Second, sequences are abstracted by shape-lengths pairs, which needs to be taken into account by sequence matching rules. This is most visible in the very last rule, with a star pattern ★𝑥, where we accept any assignment to a set abstraction vs which has a more precise shape and a smaller length.

Computing Pattern Matches

Albeit clean, the declarative satisfiability semantics of patterns is not directly computable. In Rabit, we rely on an abstract operational semantics based on the concrete operational pattern matching semantics [START_REF] Salim | The Formal Semantics of Rascal Light[END_REF]. This semantics is translated using the technique presented in Sect. 5.

The operational judgements are presented in Fig. 8 for both the concrete and abstract rules. Consider the concrete (top-left) judgement: a value 𝑣 matches a pattern 𝑝, given a store 𝜎, producing a sequence of binding environments 𝜌. The binding environments form a sequence, since multiple concrete environments, say 𝜌 1 and 𝜌 2 , can make 𝑣 match against 𝑝, i.e., 𝑣 |= 𝜌 1 𝑝 and 𝑣 |= 𝜌 2 𝑝. Backtracking using the fail-expression, allows the programmer to explore a different assignment from the sequence of environments, until no possible assignment is left. A concrete discussion of the operational rules is available in appendix A. The interesting ideas are mainly in the refining semantic operators, which we now discuss.

Semantic Operators with Refinement. Non-linear matching in Rascal requires values assigned to the same variable to be equal. We must therefore merge environments computed when matching sub-patterns to check whether a match succeeds or not. In abstract interpretation, we can refine the abstract environments when merging for each possibility. Consider when merging two abstract environments, where some variable 𝑥 is assigned to vs in one, and vs ′ in the other. If vs ′ is possibly equal to vs, we refine both values using this equality assumption vs = vs ′

. Here, we have that abstract equality is defined as the greatest lower bound if the value is non-bottom, i.e. vs = vs ′ ≜ { vs ′′ | vs ′′ = vs ⊓ vs ′ ≠ ⊥}. Similarly, we can also refine both values if they are possibly non-equal vs ≠ vs ′ . Here, abstract inequality is defined using relative complements:

vs ≠ vs ′ ≜ ( vs ′′ , vs ′ )| vs ′′ = vs \ ( vs ⊓ vs ′ ) ≠ ⊥ ∪ ( vs, vs ′′ )| vs ′′ = vs ′ \ ( vs ⊓ vs ′ ) ≠ ⊥
In our abstract domains, the relative complement (\) is limited 2 . We heuristically define it for interesting cases, and otherwise it degrades to identity in the first argument (no refinement). There are however useful cases, e.g., for excluding unary constructors suc (Nat) ≀ zero \ zero = suc (Nat) or at the end points of a lattice

[1; 10] \ [1; 2] = [3; 10].
Similarly, for matching against a constructor pattern 𝑘 (𝑝), the core idea is that we should be able to partition our value space into two: the abstract values that match the constructor and those that do not. For those values that possibly match 𝑘 (𝑝), we produce a refined value with 𝑘 as the only choice, making sure that the sub-values in the result are refined by the sub-patterns 𝑝.

Otherwise, we exclude 𝑘 from the refined value. For a data type abstraction exclusion removes the pattern constructor from the possible choices

exclude(𝑘 ( vs) ≀ 𝑘 1 ( vs 1 ) ≀ • • • ≀ 𝑘 n ( vs n ), 𝑘) = 𝑘 1 ( vs 1 ) ≀ . . . ≀ 𝑘 n ( vs n )
and does not change the input shape otherwise.

TRAVERSALS

First-class traversals are a key feature of high-level transformation languages, since they enable effectively transforming large abstract syntax trees. We will focus on the challenges for bottomup traversals, but they are shared amongst all strategies supported in Rascal. The core idea of a bottom-up traversal of an abstract value vs, is to first traverse children of the value children( vs) possibly rewriting them, then reconstruct a new value using the rewritten children and finally traversing the reconstructed value. The main challenge is handling traversal of children, whose representation and thus execution rules depend on the particular abstract value.

Concretely, the children( vs) function returns a set of pairs ( vs ′ , cvs) where the first component vs ′ is a refinement of vs that matches the shape of children cvs in the second component. Traversing Children. The shape of execution rules depend on the representation of children; this is consistent with the requirements imposed by Schmidt [START_REF] Schmidt | Trace-Based Abstract Interpretation of Operational Semantics[END_REF]. For heterogeneous sequences of value shapes vs, the execution rules iterate through the sequence recursively traversing each element. Due to over-approximation we may re-traverse the same or a more precise value on recursion, and so we need to use trace memoization (Sect. 8) to terminate. For example the children of an expression Expr refer to itself: children(Expr) = {(mult (Expr, Expr) , (Expr, Expr)), (cst (Nat) , Nat), (var (str) , str)} Traversing children represented by a shape-length pair, is directed by the length interval [𝑙; 𝑢]. If 0 is a possible value of the length interval, then traversal can finish, refining the input shape to be empty. Otherwise, we perform another traversal recursively on the shape of elements and recursively on a new shape-length pair which decreases the length, finally combining their values. Note, that if the length is unbounded, e.g. [0; ∞], then the value can be decreased forever and trace memoization is also needed here for termination. This means that trace memoization must here be nested breadth-wise (when recursing on an unbounded sequence of children), in addition to depth-wise (when recursing on children); this can be computationally expensive, and we will discuss in Sect. 9 how our implementation handles that.

TRACE MEMOIZATION

Abstract interpretation and static program analysis in general perform fixed-point calculation for analysing unbounded loops and recursion. In Schmidt-style abstract interpretation, the main technique to handle recursion is trace memoization [START_REF] Rosendahl | Abstract Interpretation as a Programming Language[END_REF][START_REF] Schmidt | Trace-Based Abstract Interpretation of Operational Semantics[END_REF]. The core idea of trace memoization is to detect non-structural re-evaluation of the same program element, i.e., when the evaluation of a program element is recursively dependent on itself, like a while-loop or traversal.

The main challenge when recursing over inputs from infinite domains, is to determine when to merge recursive paths together to correctly over-approximate concrete executions. We present an extension that is still terminating, sound and, additionally, allows calculating results with good precision. The core idea is to partition the infinite input domain using a finite domain of elements, and on recursion degrade input values using previously met input values from the same partition. We assume that all our domains are lattices with a widening operator. Consider a recursive operational semantics judgment 𝑖 =⇒ 𝑜, with 𝑖 being an input from domain Input, and 𝑜 being the output from domain Output. For this judgment, we associate a memoization map 𝑀 ∈ PInput → Input × Output where PInput is a finite partitioning domain that has a Galois connection with our actual input, i.e. Input -----→ ← -----

𝛼 𝑃𝐼 𝛾 𝑃𝐼 PInput.
The memoization map keeps track of the previously seen input and corresponding output for values in the partition domain. For example, for input from our value domain Value we can use the corresponding type from the domain Type as input to the memoization map. 3 So for values 1 and [2; 3] we would use int, while for mult(Expr, Expr) we would use the defining data type Expr.

We perform a fixed-point calculation over the evaluation of input 𝑖. Initially, the memoization map 𝑀 is 𝜆pi.(⊥, ⊥), and during evaluation we check whether there was already a value from the same partition as 𝑖, i.e., 𝛼 𝑃𝐼 (𝑖) ∈ dom 𝑀. At each iteration, there are then two possibilities: Hit The corresponding input partition key is in the memoization map and a less precise input is stored, so 𝑀 (𝛼 𝑃𝐼 (𝑖)) = (𝑖 ′ , 𝑜 ′ ) where 𝑖 ⊑ Input 𝑖 ′ . Here, the output value 𝑜 ′ that is stored in the memoization map is returned as result.

Widen The corresponding input partition key is in the memoization map, but an unrelated or more precise input is stored, i.e., 𝑀 (𝛼 𝑃𝐼 (𝑖)) = (𝑖 ′′ , 𝑜 ′′ ) where 𝑖 Input 𝑖 ′′ . In this case we continue evaluation but with a widened input 𝑖 ′ = 𝑖 ′′ ∇ Input (𝑖 ′′ ⊔ 𝑖) and an updated map

𝑀 ′ = [𝛼 𝑃𝐼 (𝑖) ↦ → (𝑖 ′ , 𝑜 prev )].
Here, 𝑜 prev is the output of the last iteration for the fixed-point calculation for input 𝑖 ′ . On the initial iteration, 𝑜 prev is assigned ⊥. Intuitively, the technique is terminating because the partitioning is finite, and widening ensures that we reach an upper bound of possible inputs in a finite number of steps, eventually getting a hit. The fixed-point iteration also uses widening to calculate an upper bound, which similarly finishes in a number of steps. The technique is sound because we only use output for previous input that is less precise; therefore our function is continuous and a fixed-point exists.

EXPERIMENTAL EVALUATION

We demonstrate the ability of Rabit to verify inductive shape properties, using nine transformation programs, where five are classical and four are extracted from open source projects.

Negation Normal Form. (NNF) transformation [30, Section 2.5] is a classical rewrite of a propositional formula to combination of conjunctions and disjunctions of literals, so negations appear only next to atoms. An implementation of this transformation should guarantee the following: P1 Implication is not used as a connective in the result P2 All negations in the result are in front of atoms Rename Struct Field. (RSF) refactoring [START_REF] Fowler | Refactoring -Improving the Design of Existing Code[END_REF] changes the name of a field in a struct, and that all corresponding field access expressions are renamed correctly as well: P3 Structure should not define a field with the old field name P4 No field access expression to the old field Desugar Oberon-0. (DSO) transformation, translates for-loops and switch-statements to whileloops and nested if-statements, respectively. The transformation is part of the Oberon-0 [START_REF] Wirth | Compiler Construction[END_REF] implementation in Rascal [START_REF] Basten | Modular language implementation in Rascal -Experience Report[END_REF], containing all the necessary stages for compiling a structured imperative programming language. P5 for should be correctly desugared to while P6 switch should be correctly desugared to if P7 No auxiliary data in output Code Generation for Glagol. (G2P) a DSL for REST-like web development, translated to PHP for execution. 4 We are interested in the part of the generator that translates Glagol expressions to PHP, and the following properties: P8 Output only simple PHP expressions for simple Glagol expression inputs P9 No unary PHP expressions if no sign marks or negations in Glagol input Mini Calculational Language. (MCL) a programming language text-book [START_REF] Sestoft | Programming language concepts[END_REF] implementation of a small expression language, with arithmetic and logical expressions, variables, if-expressions, and let-bindings. The implementation contains an expression simplifier (larger version of running example), type inference, an interpreter and a compiler. P10 Simplification procedure produces an expression with no additions with 0, multiplications with 1 or 0, subtractions with 0, logical expressions with constant operands, and if-expressions with constant conditions. (MCM) a modernization transformation designed to migrate an imperative configuration system to a declarative constraint-based one. The transformation is inspired by a realistic case given by Danfoss [START_REF] Florin Iosif-Lazăr | Experiences from Designing and Validating a Software Modernization Transformation (E)[END_REF], which is a company specialized in producing power electronics. P15 Statements which consist only of if-else conditionals and return statements should not possibly violate the post-condition stating that all statements that can be modernized. P16 Statements which consist only of if-else conditionals and return statements, should produce output expression consisting of only contain relevant input expressions and the ternary expression (𝑒 1 ?𝑒 2 : 𝑒 3 ).

Extract Superclass. (ESC) refactoring [START_REF] Fowler | Refactoring -Improving the Design of Existing Code[END_REF] takes two classes and extract a new superclass for them that contains the field definitions they have in common. P17 The new superclass has the common fields of the two subclasses. P18 The new superclass has no superclass itself. P19 The two subclasses do not have the fields of the new superclass in their definition. P20 The two subclasses have the new superclass as their superclass.

Derivative. (DER) computes the derivative5 of an additive-multiplicative expression w.r.t. a particular variable 𝑥. P21 Additive expressions containing variables 𝑦 ≠ 𝑥 and constants should produce a constant 0 when differentiated. P22 Expressions containing only linear multiplication should produce expressions with only constant leafs when differentiated.

Normalize PHP script. (NPS) transforms PHP fragments into a standardized format. 6P23 The discardHTML function should remove all contained HTML values from a PHP script. P24 The useBuiltin function should replace calls to built-in functions with the functions themselves for a PHP script. All these transformations satisfy the following criteria:

(1) They are formulated by an independent source, (2) They can be translated in relatively straightforward manner to our subset of Rascal, and

(3) They exercise important constructs, including visitors and the expressive pattern matching We have ported all these programs to Rascal Light.

Experimental Configuration. To evaluate the effect of our pragmatic design choices, we run our evaluation using different configurations. We test out two types of configuration options: one regarding the effect of using trace partitioning and one regarding the choice trace memoization domain. For the trace partitioning, we have two configurations: N representing no trace partitioning, and T representing use of trace partitioning. For the domain used for widening in trace memoization, we have three configurations: S representing always widening on recursion, T representing Threats to Validity. The programs are not selected randomly, thus it can be hard to generalize the results. We mitigated this by selecting transformations that are realistic and vary in authors and purpose. While translating the programs to Rascal Light, we have striven to minimize the amount of changes, but bias cannot be ruled out entirely.

Implementation. We have implemented the abstract interpreter in a prototype tool, Rabit 7 , for all of Rascal Light following the process described in sections 5 to 8. This required handling additional aspects, not discussed in the paper:

(1) Possibly undefined values (2) Extended result state with more Control flow constructs, backtracking, exceptions, loop control, and (3) Fine-tuning memoization strategies to the different looping constructs and recursive calls By default, we use the top element ⊤ specified as input, but the user can specify the initial data-type refinements, store and parameters, to get more precise results. The output of the tool is the abstract result value set of abstractly interpreting target function, the resulting store state and the set of relevant inferred data-type refinements.

The implementation extends standard regular tree grammar operations [START_REF] Aiken | Implementing Regular Tree Expressions[END_REF][START_REF] Cousot | Formal Language, Grammar and Set-Constraint-Based Program Analysis by Abstract Interpretation[END_REF], to handle the recursive equations for the expressive abstract domains, including base values, collections and heterogeneous data types. We use a more precise partitioning strategy for trace memoization when needed, which also takes the set of available constructors into account for data types.

Results. We ran the experiments using Scala 2.12.2 on a 10-core Xeon W-2155 Dell Workstation. Table 1 summarizes the size of the programs, the runtime of Rabit, and whether the properties have been verified. Since we verify the results on the abstract shapes, the programs are shown to be correct for all possible concrete inputs satisfying the given properties. We remark that all programs use the high-level expressive features of Rascal and are succinct compared to general purpose code.

The runtime is reasonable, and varies from less than a seconds to around a minute in most cases. All, but three, properties were successfully verified. The reason that our tool runs slower on the DSO and MCM transformations is that they contain function calls and we rely on inlining for interprocedural analysis. The P24 property of NPS is much slower than average (around 5 minute time), because the useBuiltin function has complex nested loops and the PHP data-structure is represented using large mutual inductive data types containing collections.

Line 1 in Fig. 9 show the input refinement type FIn for the normalization procedure. The inferred inductive output type FOut (line 3) specifies that the implication is not present in the output (P1), and negation only allows atoms as subformulae (P2). In fact, Rabit inferred a precise formulation of negation normal form as an inductive data type. 2. Memoization statistics for running the abstract interpreter on the properties for the different configurations. Hit (H) specifies when an existing partition key is in the memoization map; miss (M) specifies when a partition key is not found in the memoization map, and then is added to the map returning ⊥; and finally widen (W) is when the partition key is found in the memoization map, but the memoized input was more precise and widening was needed. Configuration: initial letter specifies without (N)/with (T) trace partitioning and second letter specifies simple (S)/type-based (T)/constructor-based (C) widening.

Discussion. In general, it seems that our pragmatic choices of trace partitioning and widening partitioning domain had a considerable influence on whether we were able to verify the properties we had in our evaluation. The configuration that was able to verify most of the stated properties was TC which represents running our analyzer with both trace partitioning on and constructorbased widening. The configuration TT which used type-based widening instead, was able to verify all the same properties as TC except P2, which points out that one could rely on the increased performance gains given by type-based widening while still be able to prove desired properties. The simple widening TS algorithm seemed also to be able to prove a considerable amount of target properties, but we experienced that in practice one also get false positive errors which are due to over-approximation; performance-wise it is definitely the most efficient solution.

There were 8 properties which required trace partitioning (T) to be verified, which could not be verified in the configurations without trace partitioning (N). This is especially true for many properties which have complex pattern matching and traversal require trace partitioning to infer the necessary inductive refinements.

Unlike the conference version of the paper [START_REF] Salim | Verification of high-level transformations with inductive refinement types[END_REF], we are able to verify P3 in this version. This because of two features: first we run the transformation with a nominalized version of the key abstraction to the class map, and then we have refined the preciseness of the map operations for deletion and updating. These refinements have also been useful in proving properties for the ESC transformation. Additionally, ESC required that we performed refinement of the store on simple Boolean conditions when evaluating if-statements, which we have also implemented.

Even the most general configuration TC could not verify properties P7, P19 and P22. The main reason is that our current abstractions were not precise enough to capture these properties. P22 requires widening at a larger depth than we had implemented in our evaluator, and we believe that increasing the widening depth could mitigate the issue (albeit at a huge performance cost). We discuss the extensions based on related work that are required to verify P7 and P19 in Sect. 10.

Table 2 presents statistics regarding about trace memoization, that shows how many hits, misses and widening when accessing the memoization map during execution of each property. In general, there is a correlation on how many misses and hits there were during trace memoization and the runtime of validating a property. Surprisingly. the more rich trace memoization partitioning domains, type-based (T) and constructor-based (C), did not require widening on sub-recursion during trace memoization; this indicates that these partitioning domains are so precise that all subrecursions for our tested properties have been more precise. The simple widening strategy (S) did do widenings during trace memoization, which made the runtime much faster but much less precise. There seems no considerable difference on trace memoization between the configurations that use trace partitioning (T) and those without (N).

RELATED WORK

We start with discussing techniques that could make Rabit verify properties like P7 and P19.

For a concrete input of P7, we know that the number of auxiliary data elements decreases on each iteration, but this information is lost in our abstraction. A possible solution could be to allow abstract attributes that extract additional information about the abstracted structures [START_REF] Bouajjani | Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data[END_REF][START_REF] Pham | An Improved Unrolling-Based Decision Procedure for Algebraic Data Types[END_REF][START_REF] Suter | Decision procedures for algebraic data types with abstractions[END_REF]. A generalization of the multiset abstraction [START_REF] Perrelle | An Analysis of Permutations in Arrays[END_REF], could be useful to track e.g., the auxiliary statement count, and show that they decrease using multiset-ordering [START_REF] Dershowitz | Proving Termination with Multiset Orderings[END_REF]. Other techniques [START_REF] Albarghouthi | Spatial Interpolants[END_REF][START_REF] Bor-Yuh | Relational Inductive Shape Analysis[END_REF][START_REF] Vazou | Abstract Refinement Types[END_REF] support inferring inductive relational properties for general data-types-e.g, binary tree propertybut require a pre-specified structure to indicate where refinement can happen. To verify P19, we need to have a way of knowing that when a superclass has a particular field, then it must necessarily have been removed from both subclasses. Relational abstract interpreteration [START_REF] Mycroft | A relational framework for abstract interpretation[END_REF] allows specifying constraints that relate values across different variables, even inside and across substructures [START_REF] Bor-Yuh | Relational Inductive Shape Analysis[END_REF][START_REF] Halbwachs | Discovering properties about arrays in simple programs[END_REF]37].

Cousot and Cousot [START_REF] Cousot | Modular Static Program Analysis[END_REF] present a general framework for modularly constructing program analyses, but it requires languages with compositional control flow. Toubhans, Rival and Chang [START_REF] Rival | Construction of Abstract Domains for Heterogeneous Properties[END_REF][START_REF] Toubhans | Reduced Product Combination of Abstract Domains for Shapes[END_REF] develop a modular domain design for pointer-manipulating programs, whereas our domain construction focuses on abstracting pure heterogeneous data-structures.

There are similarities between our work and verification techniques based on program transformation [START_REF] De Angelis | Program verification via iterated specialization[END_REF][START_REF] Lisitsa | Finite Countermodel Based Verification for Program Transformation (A Case Study)[END_REF]. Our systematic exploration of execution rules for abstraction is similar to unfolding, and widening is similar to folding. The main difference between the two techniques is that abstract interpretation mainly focuses on capturing rich domains and performing widening at syntactic program points, whereas program transformation based techniques often rely on symbolic inputs and perform folding dynamically on the semantic execution graph during specialization. We believe that there could benefits for the communities, to explore combinations of these two approaches in the future.

Definitional interpreters have been suggested as a technique for building compositional abstract interpreters [START_REF] Darais | Abstracting definitional interpreters (functional pearl)[END_REF]. The idea is to rely on a monad transformer stack to share the implementation of the concrete and abstract interpreters. We believe that our interpreter would benefit by being written in such style footnoteWe only learned about this related work at a late stage, which complements our modular domain construction well. They rely on a caching algorithm to ensure termination, similarly to ordinary finite input trace memoization [START_REF] Rosendahl | Abstract Interpretation as a Programming Language[END_REF]. Similarly, Van Horn and Might [START_REF] Van Horn | Abstracting abstract machines[END_REF] present a systematic framework to abstract higher-order functional languages. They rely on store-allocated continuations to handle recursion, which is kept finite during abstraction to ensure a terminating analysis. We focused on providing a more precise widening based on the abstract input value, which was necessary for verifying the required properties in our evaluation. We believe that it could be useful to look into abstract machine-based abstractions in the future, in the case that higher-order transformation languages need to be handled.

Recently, Keidel and Erdweg [START_REF] Keidel | A Systematic Approach to Abstract Interpretation of Program Transformations[END_REF] have developed a framework, Sturdy, that allows modularly constructing abstract interpreters for program transformations. Sturdy separates the concerns of interpreting a program transformation language from the choice of abstract domains. We believe writing our interpreter in this style could be beneficial for maintainability and trust in its soundness. However, there are some pragmatic challenges that need to be addressed before we could port our interpreter. In particular, trace partitioning seemed to have a big influence in our evaluation yet it is unclear how to apply this technique in their framework. Furthermore, their analyses deal with simpler domains than ours and it is unclear how we would integrate a domain like inductive refinements which require widening in their framework.

Garrigue [START_REF] Garrigue | Programming with polymorphic variants[END_REF][START_REF] Garrigue | Typing deep pattern-matching in presence of polymorphic variants[END_REF] presents algorithms for typing pattern matching on polymorphic variant types in OCaml, where the set of constructors for a data type is not fixed in advance. The theory is useful since it supports inferring simple recursive shapes of programs, but it has its limitations: inference is syntactic and exact, and it is unclear how to generalize it to work with the rich pattern matching constructs and heterogeneous visitors. Haskell supports analysing coverage of its pattern matching language, that includes generalized algebraic data types (GADTs) and Boolean constraints [START_REF] Karachalias | GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and laziness[END_REF]. While general Haskell function calls can occur in the Boolean constraints, the analysis treats them shallowly as function symbols; some covering pattern matches that depend on particular semantics of called functions, will be marked falsely as non-exhaustive. Modern SMT solvers supports reasoning with inductive functions defined over algebraic data-types [START_REF] Reynolds | Induction for SMT Solvers[END_REF]. The properties they can verify are very expressive, but they do not scale to large programs like transformations. Possible constructor analysis [START_REF] Oana Fabiana Andreescu | Dependency Analysis of Functional Specifications with Algebraic Data Structures[END_REF] has been used to calculate the actual dependencies of a predicate and make flow-sensitive analyses more precise. This analysis works with complex data-types and arrays, but only captures the prefix of the target structures.

Techniques for model transformation verification on static analysis [START_REF] Sánchez Cuadrado | Static Analysis of Model Transformations[END_REF] have been suggested, but are on verification of types and undefinedness properties. Symbolic execution has previously been suggested [START_REF] Salim | Symbolic execution of high-level transformations[END_REF] as a way to validate high-level transformation programs, but it targets test generation rather than verification of properties. Semantic typing [START_REF] Véronique Benzaken | Static and dynamic semantics of NoSQL languages[END_REF][START_REF] Castagna | Typed iterators for XML[END_REF] has been used to infer recursive type and shape properties for language with high-level constructs for querying and iteration. However, they only consider small calculi compared to Rascal Light, and our evaluation is more extensive.

CONCLUSION

Our goal was to use abstract interpretation to give a solid semantic foundation for analyzing programs in modern high-level transformation languages. We designed and implemented a Schmidtstyle abstract interpreter, Rabit, including partition-driven trace memoization that supports infinite input domains. This worked well for Rascal, and can be adapted for similar languages with complex control flow. The modular construction of abstract domains was vital for handling a language of this scale and complexity. We evaluated Rabit on classical and open source transformations, by verifying a series of sophisticated shape properties for them.

A OPERATIONAL PATTERN MATCHING

Computing Pattern Matching. For an ordinary pattern 𝑝 (top) the abstraction relation is direct: an abstract store 𝜎 abstracts a concrete store 𝜎 and a value shape vs abstracts a concrete value 𝑣. The notable change is that the abstract semantics uses a set of abstract binding environments 𝜚 ⊆ Store × ValueShape × BindingEnv ⊥ that not only abstracts over the sequence of concrete binding environments 𝜌, but also, for each abstract binding environment stores the corresponding refinement of the input abstract store 𝜎 and the corresponding refinement of the matched value shape vs according to the matched pattern.

For sequences of set sub-patterns ★𝑝, the sequence of concrete values 𝑣 is abstracted by two components: the shape of values vs and an interval approximating the length of the value sequence [𝑙; 𝑢]. Both of these values are refined as a result of the matching, which is captured by the abstract binding environment 𝜚 (of the same type as for the simple patterns), since we treat the value refined as the abstract set containing the values of the given shape and of given cardinality. The concrete semantics of set sub-patterns also contains a backtracking state V which is not used in the abstract semantics, because the abstraction of set elements is coarse and we thus abstractly consider all possible subset assignments at the same time (joining instead of backtracking).

Operational Rules. We will show how refinement is calculated by the abstract operational semantics by presenting some of key rules for abstract pattern matching. Rascal also allows non-linear pattern matching against assigned store variables, and it is possible to use this information for refining the input store and abstract value. In the AP-V-U rule we match the variable to the value shape and restrict the shape abstraction for the variable value to match the pattern. The binding environment does not change as the name is already bound in the store. In the AP-V-F rule, the matching fails (⊥), and then we learn that the value shape in the store should be refined to something that does not match.

𝜚

For example, when it is possible that the abstracted value sequence ( vs, [𝑙; 𝑢]) is empty (𝑙 = 0) and patterned matched against an empty set sub-pattern sequence, we can refine the result to be the empty abstract set {⊥} 0 (rule APL-E-B). ( 𝜎, {⊥ VS } 0 , {[]})

A more complex example is the one where we try to pattern match a potentially non-empty value sequence against a set sub-pattern sequence 𝑝, ★𝑝 ′ starting with an ordinary pattern (APL-M-P).

Here we pattern match against 𝑝 and the rest of the sequence ★𝑝 ′ and combine the refined results of these matches producing a refinement of the containing set value by combining the refined shapes and increasing the refinement of the length by the set sub-pattern sequence by one. shows the formal rules for executing the bottom-up visit-expression; we have omitted the collecting rules and some error handling rules to avoid presenting unnecessary details. We will further discuss the ideas behind the rules in a high-level fashion.

Executing visitors. The evaluation rule for the visit-expression itself is mainly concerned with evaluating the target expression 𝑒 to be traversed to a value, and then using a separate traversal relation to rewrite the value recursively with the sequence of cases cs. The main item to notice is how it uses the value refined by the case patterns in case of failure (AE-Vt-F), turning the result into successful execution (like in our running example in Sect. 2).

Evaluating Cases. During traversal, the target value will be rewritten with a sequence of cases. The evaluation of a case sequence is straight-forward, iterating through the possible cases, pattern matching against each pattern and executing the corresponding expression when applicable. The main idea is that, when the abstract value fails to match a pattern, the refined value is used to match against the rest of the cases (ACS-M-F). This ensures that the order of patterns influences the refinement, leading to a more precise abstract shape that better matches the set of concrete shapes during execution.

1 2 solve(s) { 3 s 5 xsFig. 1 .

 2351 Fig. 1. Transformation in Rascal that flattens all nested blocks in a statement

1 3 |

 3 data Nat = zero() | suc(Nat pred); 2 data Expr = var(str nm) | cst(Nat vl) mult(Expr el, Expr er);

4 5Fig. 2 .

 42 Fig. 2. The running example: eliminating multiplications by zero from expressions

Fig. 3 .

 3 Fig.3. Naively abstractly interpreting the simplification example from Fig.2with initial input mult (cst (Nat) , cst (Nat)). The procedure does not terminate because of infinite recursion on Nat.

Fig. 4 . 6 r

 46 Fig. 4. Three iterations of a fixed point computation for input Nat. Iterations are separated by dotted arrows on top

11 rFig. 5 .

 115 Fig. 5. A prefix of the abstract interpreter run for 𝑒 = mult (cst (Nat) , cst (Nat)). Fragments of two iterations involving node 6 are shown, separated by a dotted arrow.

Fig. 6 .

 6 Fig. 6. Relating concrete semantics (left) to abstract semantics (right).

,

  Vol. 1, No. 1, Article . Publication date: March 2020.

Example 6 . 1 .Fig. 8 .

 618 Fig. 8. Relating abstract operational semantics (left) to the concrete operational semantics (right).

  For data type values the representation of children is a heterogeneous sequence of abstract values vs ′′ , while for set values the representation of children is a pair ( vs ′′ , [𝑙; 𝑢]) with the first component representing the shape of elements and the second representing their count. For example, children(mult (Expr, Expr) ≀ cst (suc (Nat))) = (mult (Expr, Expr) , (Expr, Expr)), (cst (suc (Nat)) , suc (Nat)) and children({Expr} [1;10] ) = {({Expr} [1;10] , (Expr, [1; 10]))}. Note how the children function maintains precision by partitioning the alternatives for data-types, when traversing each corresponding sequence of value shapes for the children.

1 data 3 dataFig. 9 .

 139 Fig. 9. Initial and inferred refinement types for NNF

1 ✓ 1 .

 11 Time Verif. Time Verif. Time Verif. Time Verif. Time Verif. Time Verif. Table Time and success rate for analyzing programs and properties presented earlier this section. The runtime is presented in seconds. Configuration: initial letter specifies without (N)/with (T) trace partitioning and second letter specifies simple (S)/type-based (T)/constructor-based (C) widening.

, Vol. 1 ,

 1 No. 1, Article . Publication date: March 2020.

  AP-C-F1 data at = • • • | 𝑘 (𝑡) | . . . (success 𝑘 ′ ( vs ′ )) ∈ unfold( vs, at) 𝑘 ′ ≠ 𝑘 𝜎 ⊢ 𝑘 (𝑝) ? vs = ========= ⇒ a-match-cons ( 𝜎, exclude( vs, 𝑘), ⊥) AP-C-F2 data at = • • • | 𝑘 (𝑡) | . . . error ∈ unfold( vs, at) 𝜎 ⊢ 𝑘 (𝑝) ? vs = ========= ⇒ a-match-cons ( 𝜎, exclude( vs, 𝑘), ⊥) For set patterns, the refinement happens by pattern matching set sub-patterns. AP-S-S success { vs ′ } [𝑙;𝑢 ] ∈ unfold( vs, set⟨value⟩) 𝜎 ⊢ ★𝑝 ? vs, [𝑙; 𝑢] = ====== ⇒ a-match★ 𝜚 𝜎 ⊢ {★𝑝} ? vs = ======== ⇒ a-match-set

  APL-E-B 𝑙 ≤ 𝑢 𝑙 = 0 𝜎 ⊢ 𝜀 ? vs, [𝑙; 𝑢] = ======== ⇒ a-match★-1

  Figures 12 and 13 shows the formal rules for executing the bottom-up visit-expression; we have omitted the collecting rules and some error handling rules to avoid presenting unnecessary details. We will further discuss the ideas behind the rules in a high-level fashion.

  𝑘 (𝑣) |= 𝜌 𝑘 (𝑝) iff 𝑡 are parameter types of 𝑘 and 𝑣 : 𝑡 ′ and 𝑡 ′ <: 𝑡 and 𝑣 |= ★ ★𝑝 ′ iff 𝑣 |= 𝜌 𝑝 and 𝑣 ′ |= ★ 𝜌 ★𝑝 ′ 𝑣, 𝑣 ′ |= ★ 𝜌 ★𝑥, ★𝑝 ′ iff 𝜌 (𝑥) = {𝑣 } and 𝑣 ′ |= ★ 𝜌 ★𝑝 ′ (a) Concrete (𝑣 |= 𝜌 𝑝 reads: 𝑣 matches 𝑝 with 𝜌) Fig. 7. Satisfiability semantics for pattern matching same binding environment 𝜌. A sequence ★𝑥, ★𝑝 ′ works analogously but it splits the value sequence in two 𝑣 and 𝑣 ′ , such that 𝑥 is assigned to 𝑣 in 𝜌 and 𝑣 ′ matches ★𝑝 ′ consistently in 𝜌.

			𝜌 𝑝
	𝑣 |= 𝜌 𝑥	iff	𝜌 (𝑥) = 𝑣
	{𝑣 } |= 𝜌 {★𝑝}	iff	𝑣 |= ★ 𝜌 ★𝑝
	𝜀 |= ★ 𝜌 𝜀	always
	𝑣, 𝑣 ′ |= ★ 𝜌 𝑝,

, Vol. 1, No. 1, Article . Publication date: March 2020.

𝑘 ( vs) |= 𝜌 𝑘 (𝑝) iff 𝑡 are parameter types of 𝑘 and vs : 𝑡 ′ and 𝑡 ′ <: 𝑡 and vs |= ★ 𝜌 𝑝 vs |= 𝜌 𝑥 iff 𝜌 (𝑥) ⊑ vs { vs} [𝑙;𝑢 ] |= 𝜌 {★𝑝} iff vs, [𝑙; 𝑢] |= ★ 𝜌 ★𝑝 vs, [0; 𝑢] |= ★ 𝜌 𝜀 always vs, [𝑙; 𝑢] |= ★ 𝜌 𝑝, ★𝑝 ′ iff 𝑢 > 0 and vs |= 𝜌 𝑝 and vs, [𝑙 -1; 𝑢 -1] |= ★ 𝜌 𝑝, ★𝑝 ′ vs, [𝑙; 𝑢] |= ★ 𝜌 ★ 𝑥, ★𝑝 ′ iff 𝜌 (𝑥) = { vs ′ } [𝑙 ′ ;𝑢 ′ ] and 𝑙 ′ ≤ 𝑙 and 𝑢 ′ ≤ 𝑢 and vs ′ ⊑ vs and vs, [𝑙 -𝑢 ′ ; 𝑢 -𝑙 ′ ] |= ★ 𝜌 ★𝑝 ′ (b) Abstract ( 𝑣𝑠 |= 𝜌 𝑝 reads: 𝑣𝑠 may match 𝑝 with 𝜌)

  P11 Arithmetic expressions with no variables have type int and no type errors P12 Interpreting expressions with no integer constants and let's gives only Boolean values P13 Compiling expressions with no if's produces no goto's and if instructions P14 Compiling expressions with no if's produces no labels and does not change label counter Mini Configuration Modernization.

, Vol. 1, No. 1, Article . Publication date: March 2020.

Note that it is not a relative complement of the abstract domain lattice. , Vol. 1, No. 1, Article . Publication date: March 2020.

Provided that we bound the depth of type parameters of collections. , Vol. 1, No. 1, Article . Publication date: March 2020.

https://github.com/BulgariaPHP/glagol-dsl , Vol. 1, No. 1, Article . Publication date: March 2020.

http://tutor.rascal-mpl.org/Recipes/Common/Derivative/Derivative.html

https://github.com/cwi-swat/php-analysis. We rely on a simplified and rewritten version of the script for compatability and performance reasons. , Vol. 1, No. 1, Article . Publication date: March 2020.

https://github.com/ahmadsalim/Rascal-Light , Vol. 1, No. 1, Article . Publication date: March 2020.

ACKNOWLEDGMENTS

We thank Paul Klint, Tijs van der Storm, Jurgen Vinju and Davy Landman for discussions on Rascal and its semantics. We thank Rasmus Møgelberg and Jan Midtgaard for discussions on correctness of the recursive shape abstractions. We thank Sebastian Erdweg for discussions on the evaluation, prompting us to investigate the influence of pragmatics. This material is based upon work supported by the Danish Council for Independent Research under Grant No. 0602-02327B and Innovation Fund Denmark under Grant No. 7039-00072B.

We also show the AP-V-B (abstract pattern-variable-bind) rule which simply binds the variable in the binding environment, assuming that it is possibly not assigned in the store (a free name).

AP-V-B 𝜎 (𝑥) = (tt, vs ′ )

( 𝜎 [𝑥 ↦ → (tt, ⊥ VS )], vs, [𝑥 ↦ → vs])

If our matched abstract value possibly contains the pattern constructor 𝑘 (AP-C-S rule: abstract pattern-constructor-success) we produce an abstract value with 𝑘 containing the sub-values refined against constructor sub-patterns:

The total function merge unifies assignments from two binding environments point-wise by names, taking the greatest lower bound of shapes to combine bindings for a name. It yields bottom for the entire result if at least one of the point-wise meets yields bottom (shapes for at least one name are not reconcilable). Otherwise, we try to refine the matched value to exclude the pattern constructor in the AP-C-F rules:

Res

Assignment Expression

Sequencing Expression

Constructor Expression