On the Design of Generic Static Analyzers for Imperative Languages

ROBERTO BAGNARA Department of Mathematics, University of Parma, Italy and PATRICIA M. HILL School of Computing, University of Leeds, UK and ANDREA PESCETTI, and ENEA ZAFFANELLA Department of Mathematics, University of Parma, Italy

The design and implementation of precise static analyzers for significant fragments of imperative languages like C, C^{++}, Java and Python is a challenging problem. In this paper, we consider a core imperative language that has several features found in mainstream languages such as those including recursive functions, run-time system and user-defined exceptions, and a realistic data and memory model. For this language we provide a concrete semantics —characterizing both finite and infinite computations— and a generic abstract semantics that we prove sound with respect to the concrete one. We say the abstract semantics is generic since it is designed to be completely parametric on the analysis domains: in particular, it provides support for relational domains (i.e., abstract domains that can capture the relationships between different data objects). We also sketch how the proposed methodology can be extended to accommodate a larger language that includes pointers, compound data objects and non-structured control flow mechanisms. The approach, which is based on structured, big-step G^{∞}SOS operational semantics and on abstract interpretation, is modular in that the overall static analyzer is naturally partitioned into components with clearly identified responsibilities and interfaces, something that greatly simplifies both the proof of correctness and the implementation.

Categories and Subject Descriptors: F3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs.

General Terms: Languages, Verification.

Additional Key Words and Phrases: Abstract interpretation, structured operational semantics.

1. INTRODUCTION

The last few years have witnessed significant progress toward achieving the ideal of the program verification grand challenge [Hoa03]. Still, the distance separating us from that ideal can be measured by the substantial lack of available tools that are able to verify the absence of relevant classes of run-time errors in code written in (reasonably rich fragments of) mainstream imperative languages like C, C^{++}, Java and Python. True: there is a handful of commercial products that target generic applications written in C, but little is known about them. In contrast, several papers explain the essence of the techniques employed by the ASTRÉE analyzer

This work has been partly supported by MIUR project “AIDA — Abstract Interpretation: Design and Applications” and by a Royal Society (UK) International Joint Project (ESEP) award.

2 · R. Bagnara, P.M. Hill, A. Pescetti, and E. Zaffanella

to formally and automatically verify the absence of run-time errors in large safetycritical embedded control/command codes [BCC^{+}02; BCC^{+}03]; however, ASTRÉE is specially targeted at a particular class of programs and program properties, so that widening its scope of application is likely to require significant effort [Cou05]. It is interesting to observe that, among the dozens of software development tools that are freely available, there are hardly any that, by analyzing the program semantics, are able to certify the absence of important classes of run-time hazards such as, say, the widely known buffer overflows in C code.

The reason for the current, extreme scarcity of the resource “precise analyzers for mainstream programming languages” is that the design and implementation of such analyzers is a very challenging problem. The theory of abstract interpretation [CC77a; CC92a] is crucial to the management of the complexity of this problem and, in fact, both ASTRÉE and the existing commercial analyzers are (as far as we know) based on it. Static analysis via abstract interpretation is conducted by mimicking the execution of the analyzed programs on an abstract domain. This is a set of computable representations of program properties equipped with all the operations required to mirror, in an approximate though correct way, the real, concrete executions of the program. Over the last decade, research and development on the abstract domains has led to the availability of several implementations of a wide range of abstract domains: from the most efficient though imprecise, to the most precise though inefficient. Simplification and acceleration techniques have also been developed to mitigate the effects of this complexity/precision trade-off. So the lack of semantics-based static analyzers is not ascribable to a shortage of abstract domains and their implementations. The point is that there is more to a working analyzer than a collection of abstract domains:

(i) A concrete semantics must be selected for the analyzed language that models all the aspects of executions that are relevant to the properties of interest. This semantics must be recognizable as a sound characterization of the language at the intended level of abstraction.

(ii) An abstract semantics must be selected and correlated to the concrete semantics. This requires a proof of correctness that, while greatly simplified by abstract interpretation theory, can be a time-consuming task by highly qualified individuals.

(iii) An algorithm to finitely and efficiently compute (approximations of) the abstract semantics must be selected.

(iv) For good results, the abstract domain needs to be an object that is both complex and easily adaptable. So, instead of designing a new domain from scratch, it is often better if one can be obtained by combining simpler, existing, abstract domains. Even though the theory of abstract interpretation provides important conceptual instruments for the design of such a combination, a significant effort is still needed to achieve, as far as possible, the desired precision and efficiency levels. Note that this point can have an impact on points (ii) and (iii): a generic abstract semantics has the advantage of not requiring an entirely new proof and a new algorithm each time the abstract domain changes.

On the Design of Generic Static Analyzers for Imperative Languages · 3

This paper, which is the first product of a long-term research plan that is meant to deal with all of the points above, specifically addresses points (i) and (ii) and refers to a slight generalization of existing techniques for point (iii).

1.1 Contribution

We build on ideas that have been around for quite some time but, as far as we know, have never been sufficiently elaborated to be applied to the description and analysis of realistic imperative languages. In extreme synthesis, the contribution consists in filling a good portion of the gaps that have impeded the application of these ideas to complex imperative programming languages such as C.^{1}

More precisely, here we define the concrete and generic abstract semantics constructions for a language —called CPM— that incorporates all the features of mainstream, single-threaded imperative programming languages that can be somehow problematic from the point of view of static analysis. Most notably, the CPM language features: a non-toy memory model; exceptions; run-time errors modeled via exceptions (for instance, an exception is raised whenever a division by zero is attempted, when a stack allocation request causes a stack overflow or when other memory errors occur); array types; pointer types to both data objects and functions; short-circuit evaluation of Boolean operators; user-defined (possibly recursive) functions; and non-structured control flow mechanisms.

For the description of the concrete dynamic semantics of the language we have used a structured operational semantics (SOS) approach extended to deal with infinite computations, mainly building on the work of Kahn, Plotkin and Cousot. With respect to what can be found in the literature, we have added the treatment of all non-structured control flow mechanisms of the C language. Of course, as the ultimate goal of this research is to end up with practical analysis tools, the concrete dynamic semantics has been defined in order to facilitate as much as possible the subsequent abstraction phase. Still, our dynamic semantics retains all the traditional good features: in particular, the concrete rule schemata are plainly readable (assuming the reader becomes sufficiently familiar with the unavoidable notational conventions) and fairly concise.

For the abstract semantics, we build on the work of Schmidt by providing the concrete dynamic semantics rules with abstract counterparts. As far as we know, this is the first time that Schmidt’s proposal is applied to the analysis of a realistic programming language [D. Schmidt, personal communication, 2004]. A remarkable feature of our abstract semantics is that it is truly generic in that it fully supports relational abstract domains: the key step in this direction is the identification and specification of a suitable set of operators on (concrete and abstract) memory structures, that allow for domain-independent approximations but without inherent limitations on the obtainable precision.

1It is worth noticing that we improperly refer to the C language to actually mean some more constrained language —like CIL, the C Intermediate Language described in [NMRW02]— where all ambiguities have been removed, in addition to an ABI (Application Binary Interface) that further defines its semantics. Similarly, by ‘Python’ we mean a tractable subset of the language, such as the RPython subset being developed by the PyPy project (http://pypy.org/).

Schmidt’s proposal about the abstract interpretation of natural semantics has, in our opinion, two important advantages: concrete and abstract rules can be made executable and are easily correlated. We review these two aspects in turn.

Even though here we do not provide details in this respect, a prototype system —called ECLAIR^{2}— has been developed in parallel with the writing of the present paper. The Prolog implementation exploits nice features of a semantics construction based on SOS approach: the concrete semantics rule schemata can be directly translated into Prolog clauses; and the resulting interpreter, with the help of a C^{++} implementation of memory structures, is efficient enough to run non-trivial programs. Similar considerations apply to the modules implementing the abstract semantics: the abstract semantics rules are almost directly translated to generic Prolog code that is interfaced with specialized libraries implementing several abstract domains, including accurate ones such as the ones provided by the Parma Polyhedra Library [BHRZ05; BHZ05; BHZ06]. So, following this approach, the distance between the expression of the concrete semantics and its executable realization is, as is well known, very little; but the same can be said about the distance between the specification of the abstract semantics and the static analyzer that results from its implementation. This prototype system therefore gives us confidence that both the concrete and abstract semantics are correctly modeled and that, in this paper, no real difficulties have been overlooked.

For space reasons, only a subset of CPM is treated in full depth in the main body of the paper (the extension of the design to the full language is only briefly described even though all the important points are covered). For this subset, we give a complete proof of correctness that relates the abstract semantics to the concrete semantics. The proofs are not complicated and suggest (also because of the way we present them) the possibility of their automatization. To summarize, at this stage of the research work it does not seem unreasonable that we may end up with: readable and executable representations of the concrete semantics of mainstream programming languages; readable and executable representations of program analyzers; correctness of the analyzers established by automatic specialized theorem provers; and, at last, availability of sophisticated program analyzers for such languages.

A final word is due to address the following concern: if the target languages are “real” imperative programming languages, why choose CPM, an unreal one? The reason is indeed quite simple: Java and Python miss some of the “hard” features of C; C misses exceptions; C^{++} is too hard, for the time being. So, choosing any one of these real languages would have been unlikely to provide us with the answer we were looking for, which was about the adequacy of Schmidt’s approach with respect to the above goals. Moreover, in its ECLAIR realization, the CPM language is being extended so as to become a superset of C (i.e., with all the floating-point and integer types, cast and bitwise operators and so forth). Once that code has stabilized, a C and a Java subsystem will be forked.

2The ‘Extended CLAIR’ system targets the analysis of mainstream programming languages by building upon CLAIR, the ‘Combined Language and Abstract Interpretation Resource’, which was initially developed and used in a teaching context (see http://www.cs.unipr.it/clair/).

1.2 Related Work

The literature on abstract interpretation proposes several frameworks for static analysis, where the more general approaches put forward in foundational papers are partially specialized according to a given criterion. For a few examples of specializations based on the programming paradigm, one can mention the frameworks in [Bru91] and [GDL92] for the analysis of (constraint) logic programs; the approach in [CC94] for the analysis of functional programs; and the so called “Marktoberdorf’98 generic static analyzer” specified in [Cou99] for the analysis of imperative programs.

All of these frameworks are “generic” in that, while fixing some of the parameters of the considered problem, they are still characterized by several degrees of freedom. It is therefore natural to reason on the similarities and differences between these approaches. However, independently from the programming paradigm under analysis, direct comparisons between frameworks are extremely difficult in that each proposal typically focuses on the solution of a subset of the relevant issues, while partially disregarding other important problems. For instance, both [Bru91] and [GDL92] study the generic algebraic properties that allow for a clean and safe separation between the abstract domains and the abstract interpreter; in contrast, [Cou99] provides full details for a specific instance of the proposed framework, ranging from the parsing of literal constants to the explicit implementation of the abstract operators for the abstract domain of intervals. On the other hand, the frameworks mentioned above differ from the one presented in this paper in that they allow for significant simplifications of the language analyzed. Here we briefly discuss the main differences between the language considered in our proposal and the one in [Cou99].

At the syntactic level, as already mentioned, the language CPM is much richer than the simple imperative language adopted in [Cou99], which has no support for functions, nesting of block statements, exceptions, non-structured control flows and it allows for a single data type (in particular, no pointers and arrays). These syntactic differences are clearly mirrored at the semantics level. In particular, even though the detection of initialization and arithmetic errors is considered by the semantics in [Cou99], the actual process of error propagation is not modeled. In contrast, the semantics construction we propose can easily accommodate the sophisticated exception propagation and handling mechanisms that can be found in languages such as C^{++}, Java and Python. Note that this choice has a non-trivial impact on the specification of the other components of the semantic construction. For example, the short-circuit evaluation of Boolean expressions cannot be normalized as proposed in [Cou99], because such a normalization process, by influencing the order of evaluation of subexpressions, is unable to preserve the concrete semantics as far as exceptional computation paths are concerned. A minor difference is in the modeling of integer variables and values: while [Cou99] considers the case of possibly uninitialized variables taking values in a finite set of machine-representable integers, for ease of presentation we have opted for definitely initialized variables storing arbitrary (i.e., unbounded) integer values. Since the CPM language supports an extensible set of RTS exceptions, the specification of a semantics modeling (the generation, propagation and handling of) uninitialization errors is rather straightforward. An extension of the semantics to the case of several sets of bounded and unbounded numerical types, with suitable type conversion functions, is under development. Another difference is in the generality of the abstract semantics construction: following the approach described here, an analyzer can take full advantage of the more accurate information provided by a relational domain such as that of polyhedra. In contrast, the work in [Cou99] only considers the simpler case of non-relational abstract domains. As mentioned above, the semantics we propose also models the case of possibly recursive functions (with a call-by-value parameter passing mechanism), which are not supported by the language syntax considered in [Cou99]. While both this paper and [Cou99] consider the specification of a forward static analysis framework, [Cou99] also provides a backward analysis for arithmetic expressions, to be used in reductive iterations so as to improve precision losses that are usually incurred by non-relational approximations.

1.3 Plan of the Paper

The paper is organized as follows. Section 2 introduces the notation and terminology used throughout the paper; Section 3 defines the syntax of a subset of the imperative language CPM, whereas Section 4 defines its static semantics; the concrete dynamic semantics of this fragment is presented in Section 5, whereas its abstract counterpart is defined in Section 6. The proof of correctness of the abstract semantics is the subject of Section 7, while the computation of further approximations is treated in Section 8. The integration of the full CPM language in the analysis framework presented in this paper is discussed in Section 9. Section 10 concludes.

2. PRELIMINARIES

Let S and T be sets. The notation S ⊆_{f} T means that S is a finite subset of T. We write S ⊎ T to denote the union S ∪ T, yet emphasizing the fact that S ∩ T = ∅. The set of total (resp., partial) functions from S to T is denoted by S → T (resp., S ↣ T). We denote by dom(f) the domain of a function f: S → T (resp., f: S ↣ T), where dom(f) = S (resp., dom(f) ⊆ S). Let (S, ⪯) be a partial order and f: S → S be a function. An element x ∈ S such that x = f(x) (resp., x ⪯ f(x)) is called a fixpoint (resp., post-fixpoint) of f. The notation lfp_{⪯}(f) (resp., gfp_{⪯}(f)) stands, if it exists, for the least (resp., greatest) fixpoint of f. A complete lattice is a partial order (S, ⪯) such that lub T exists for each T ⊆ S. If f: S → S is monotonic over the complete lattice S, the Knaster-Tarski theorem ensures that the set of post-fixpoints of f is itself a complete lattice. The fixpoint coinduction proof principle follows: if f is monotonic over the complete lattice S then, in order to prove that x ⪯ gfp_{⪯}(f), it is sufficient to prove that x ⪯ f(x).

Let S = {s_{1}, …, s_{n}} be a finite set of cardinality n ≥ 0. Then, the notation {s_{1} ↦ t_{1}, …, s_{n} ↦ t_{n}}, where {t_{1}, …, t_{n}} ⊆ T, stands for the function f: S → T such that f(s_{i}) = t_{i}, for each i = 1, …, n. Note that, assuming that the codomain T is clear from context, the empty set ∅ denotes the (nowhere defined) function f: ∅ → T.

When denoting the application of a function f: (S_{1} × ⋯ × S_{n}) → T we omit, as customary, the outer parentheses and write f(s_{1}, …, s_{n}) to mean f((s_{1}, …, s_{n})).

Let f_{0} : S_{0} ↣ T_{0} and f_{1} : S_{1} ↣ T_{1} be partial functions. Then the function f_{0}[f_{1}]: (S_{0} ∪ S_{1}) ↣ (T_{0} ∪ T_{1}) is defined, for each x ∈ dom(f_{0}) ∪ dom(f_{1}), by

(f_{0}[f_{1}])(x) =^{def} \begin{cases}f_{1}(x), & if x ∈ dom(f_{1}); \\ f_{0}(x), & if x ∈ dom(f_{0}) \ dom(f_{1}). \end{cases}

(Note that, if f_{0} and f_{1} are total functions, then f_{0}[f_{1}] is total too.)

For a partial function f: S ↣ T and a set S′ ⊆ S, f |_{S′} denotes the restriction of f to S′, i.e., the function f |_{S′}: S′ ↣ T defined, for each x ∈ S′ ∩ dom(f), by f |_{S′}(x) = f(x). (Note that, if f is a total function, then f |_{S′} is total too.) With a minor abuse of notation, we will sometimes write f \ S′′ to denote f |_{S\S′′}.

S^{⋆} denotes the set of all finite, possibly empty strings of symbols taken from S. The empty string is denoted by ϵ. If w, z ∈ S ∪ S^{⋆}, the concatenation of w and z is an element of S^{⋆} denoted by wz or, to avoid ambiguities, by w · z. The length of a string z is denoted by |z|.

The integer part function int: ℝ → ℤ is given, for each x ∈ ℝ, by int(x) =^{def} ⌊x⌋, if x ≥ 0, and int(x) =^{def} ⌈x⌉, if x < 0. The integer division and the modulo operations ÷, mod : (ℤ × ℤ \ {0}) → ℤ are defined, for each x, y ∈ ℤ with y ≠ 0, respectively

by x ÷ y =^{def} int(x/y) and x mod y =^{def} x − (x ÷ y) · y.

We assume familiarity with the field of program analysis and verification via abstract interpretation. The reader is referred to the literature for the theory (e.g., [Cou81; CC76; CC77a; CC79; CC92a; CC92c]) and examples of applications [DRS01; Hal93; SKS00].

3. THE LANGUAGE SYNTAX

The run-time support of CPM uses exceptions to communicate run-time errors. The set of RTS exceptions is left open so that it can be extended if and when needed. That said, the basic syntactic sets of the CPM language are:

Identifiers. id ∈ Id = \{main, x, x_{0}, x_{1}, …\} ⊎ rId, where rId =^{def} \{\underline{x}, \underline{x}_{0}, \underline{x}_{1}, …\};

Basic types. T ∈ Type =^{def} {integer, boolean};

Integers. m ∈ Integer =^{def} ℤ;

Booleans. t ∈ Bool =^{def} {tt, ff};

RTS exceptions. χ ∈ RTSExcept =^{def} {divbyzero, stkovflw, memerror, …}.

The identifiers in rId are “reserved” for the specification of the concrete semantics.

From the basic sets, a number of syntactic categories are defined, along with their syntactic meta-variables, by means of the BNF rules:

Expressions.

Exp ∋ e ::= m | −e | e_{0} + e_{1} | e_{0} − e_{1} | e_{0} ∗ e_{1} | e_{0} / e_{1} | e_{0} % e_{1}
| t | e_{0} = e_{1} | e_{0} ≠ e_{1} | e_{0} < e_{1} | e_{0} ≤ e_{1} | e_{0} ≥ e_{1} | e_{0} > e_{1}
| not e | e_{0} and e_{1} | e_{0} or e_{1} | id

Sequences of expressions.

Exps ∋ es ::= □ | e, es

8 · R. Bagnara, P.M. Hill, A. Pescetti, and E. Zaffanella

Storable types. sType ∋ sT ::= T Formal parameters. formParams ∋ fps ::= □ | id : sT, fps Function bodies. Body ∋ body ::= let d in s result e | extern Global declarations. Glob ∋ g ::= gvar id : sT = e | function id(fps) : sT = body | rec g | g_{0}; g_{1} Local declarations. Decl ∋ d ::= nil | lvar id : sT = e | d_{0}; d_{1} Catchable types. cType ∋ cT ::= rts exception | sT Exception declarations. exceptDecl ∋ p ::= χ | cT | id : sT | any Catch clauses. Catch ∋ k ::= (p) s | k_{0}; k_{1} Statements.

Stmt ∋ s ::= nop | id := e | id_{0} := id(es) | s_{0}; s_{1} | d; s
| if e then s_{0} else s_{1} | while e do s
| throw χ | throw e | try s catch k | try s_{0} finally s_{1}

Observe that there is no need of a separate syntactic category for programs: as we will see, a CPM program is just a global declaration defining the special function ‘main’, like in C and C^{++}.

It should be noted that some apparent limitations of the abstract syntax of CPM are not real limitations. For instance: the use of function calls as expressions can be avoided by introducing temporary variables; procedures can be rendered by functions that return a dummy value; and so forth. More generally, a slight elaboration of the abstract syntax presented here and extended in Section 9 is used in the ECLAIR prototype to encode the C language almost in its entirety, plus the basic exception handling mechanisms of C^{++} and Java.

For notational convenience, we also define the syntactic categories of constants, storable values^{3} and exceptions:

Constants. Con ∋ con ::= m | t

3The reason for a distinction between the roles of constants and storable values (as well as basic types and storable types) will become clear when discussing language extensions in Section 9.

Storable values.

sVal ∋ sval ::= con

Exceptions.

Except ∋ ξ ::= χ | sval

The function type: sVal ↣ sType, mapping a storable value to its type name ‘integer’ or ‘boolean’, is defined by:

type(sval) =^{def} \begin{cases}integer, & if sval = m ∈ Integer; \\ boolean, & if sval = t ∈ Bool. \end{cases}

For ease of notation, we also define the overloadings type: Except ↣ cType and type: exceptDecl ↣ cType defined by

type(ξ) =^{def} \begin{cases}rts exception, & if ξ = χ ∈ RTSExcept; \\ type(sval), & if ξ = sval ∈ sVal; \end{cases}

type(p) =^{def} \begin{cases}rts exception, & if p = χ ∈ RTSExcept; \\ cT, & if p = cT ∈ cType; \\ sT, & if p = id : sT and sT ∈ sType. \end{cases}

Note that such an overloading is consistent and the resulting function is not defined on value any ∈ exceptDecl.

The helper function dom: cType → {Integer, Bool, RTSExcept}, which associates a catchable type name to the corresponding domain, is defined by

dom(cT) =^{def} \begin{cases}Integer, & if cT = integer; \\ Bool, & if cT = boolean; \\ RTSExcept, & if cT = rts exception. \end{cases}

4. STATIC SEMANTICS

The static semantics of the CPM language establishes the conditions under which a program is well typed. Only well-typed programs are given a dynamic semantics.

4.1 Defined and Free Identifiers

The set of identifiers defined by sequences of formal parameters, (global or local) declarations or exception declarations is defined as follows:

DI(□) =^{def} DI(nil) =^{def} DI(body) =^{def} DI(χ) =^{def} DI(cT) =^{def} DI(any) =^{def} ∅;

DI(id : sT) =^{def} DI(gvar id : sT = e) =^{def} DI(lvar id : sT = e)

=^{def} DI(function id(fps) : sT = body) =^{def} {id};

DI(id : sT, fps) =^{def} DI(id : sT) ∪ DI(fps);

DI(rec g) =^{def} DI(g);

DI(g_{0}; g_{1}) =^{def} DI(g_{0}) ∪ DI(g_{1});

10 · R. Bagnara, P.M. Hill, A. Pescetti, and E. Zaffanella

DI(d_{0}; d_{1}) =^{def} DI(d_{0}) ∪ DI(d_{1}). The set of identifiers that occur freely in (sequences of) expressions, (exception) declarations, statements and catch clauses is defined by:

FI(m) =^{def} FI(t) =^{def} FI(nop) =^{def} FI(□) =^{def} FI(id : sT) =^{def} FI(nil)

=^{def} FI(χ) =^{def} FI(cT) =^{def} FI(any) =^{def} FI(throw χ) =^{def} FI(extern) =^{def} ∅; FI(−e) =^{def} FI(not e) =^{def} FI(lvar id : sT = e)

=^{def} FI(gvar id : sT = e) =^{def} FI(throw e) =^{def} FI(e); FI(e_{0} op e_{1}) =^{def} FI(e_{0}) ∪ FI(e_{1}), for op ∈ {+, …, %, =, …, >, and, or}; FI(id) =^{def} {id}; FI(let d in s result e) =^{def} FI(d) ∪ (FI(s) \ DI(d)) ∪ (FI(e) \ DI(d)); FI(function id(fps) : sT = body) =^{def} FI(body) \ DI(fps); FI(rec g) =^{def} FI(g) \ DI(g); FI(g_{0}; g_{1}) =^{def} FI(g_{0}) ∪ (FI(g_{1}) \ DI(g_{0})); FI(d_{0}; d_{1}) =^{def} FI(d_{0}) ∪ (FI(d_{1}) \ DI(d_{0})); FI(id := e) =^{def} {id} ∪ FI(e); FI(e, es) =^{def} FI(e) ∪ FI(es); FI(id_{0} := id(es)) =^{def} {id, id_{0}} ∪ FI(es); FI(d; s) =^{def} FI(d) ∪ (FI(s) \ DI(d)); FI((p) s) =^{def} FI(s) \ DI(p); FI(k_{0}; k_{1}) =^{def} FI(k_{0}) ∪ FI(k_{1}); FI(s_{0}; s_{1}) =^{def} FI(try s_{0} finally s_{1}) =^{def} FI(s_{0}) ∪ FI(s_{1}); FI(if e then s_{0} else s_{1}) =^{def} FI(e) ∪ FI(s_{0}) ∪ FI(s_{1}); FI(while e do s) =^{def} FI(e) ∪ FI(s); FI(try s catch k) =^{def} FI(s) ∪ FI(k).

4.2 Type Environments We start by defining the convenience syntactic category of

Denotable types. dType ∋ dT ::= sT loc | fps → sT

A type environment associates a denotable type to each identifier of a given, finite set of identifiers.

Definition 4.1. (TEnv_{I}, TEnv.) For each I ⊆_{f} Id, the set of type environments over I is TEnv_{I} =^{def} I → dType; the set of all type environments is given by TEnv =^{def} ⨄_{I⊆_{f} Id} TEnv_{I}. Type environments are denoted by β, β_{0}, β_{1} and so forth. The notation β : I is a shorthand for β ∈ TEnv_{I}.

4.3 Static Semantics Predicates

Let I ⊆_{f} Id and β ∈ TEnv_{I}. The well-typedness of program constructs whose free identifiers are contained in I is encoded by the following predicates, here listed along with their informal meaning:

β ⊢_{I} e : sT,  e is well-formed and has type sT in β;
β ⊢_{I} body : sT,  body is well-formed and has type sT in β;
β, fps ⊢_{I} es,  es is compatible with fps and well formed in β;
fps : δ,  fps is well formed and yields the type environment δ;
β ⊢_{I} g : δ,  g is well formed and yields the type environment δ in β;
β ⊢_{I} d : δ,  d is well-formed and yields the type environment δ in β;
p : δ,  p is well-formed and yields the type environment δ;
β ⊢_{I} k,  k is well-formed in β;
β ⊢_{I} s,  s is well-formed in β.

These predicates are defined inductively on the abstract syntax by means of the following rules.

Expressions.

β ⊢_{I} m : integer  β ⊢_{I} t : boolean

β ⊢_{I} e : integer

β ⊢_{I} −e : integer

β ⊢_{I} e : boolean
β ⊢_{I} not e : boolean

β ⊢_{I} e_{0} : integer β ⊢_{I} e_{1} : integer

\overline{if ⧇ ∈ \{+, −, ∗, /, %\}}
β ⊢_{I} e_{0} ⧇ e_{1} : integer

β ⊢_{I} e_{0} : integer β ⊢_{I} e_{1} : integer

\overline{if ⧆ ∈ \{=, ≠, <, ≤, ≥, >\}}
β ⊢_{I} e_{0} ⧆ e_{1} : boolean

β ⊢_{I} e_{0} : boolean β ⊢_{I} e_{1} : boolean

\overline{if ⋄ ∈ \{and, or\}}
β ⊢_{I} e_{0} ⋄ e_{1} : boolean

if β(id) = sT loc

β ⊢_{I} id : sT

Sequences of expressions.

β, □ ⊢_{I} □

β ⊢_{I} e : sT β, fps ⊢_{I} es
β, (id : sT, fps) ⊢_{I} (e, es)

Sequences of formal parameters.

□ : ∅

fps : δ

if id ∉ DI(fps)

(id : sT, fps) : {id ↦ sT loc} ∪ δ

Function bodies.

β ⊢_{I} d : β_{0}  β[β_{0}] ⊢_{I∪DI(d)} s  β[β_{0}] ⊢_{I∪DI(d)} e : sT
β ⊢_{I} (let d in s result e) : sT

Declarations.

β ⊢_{I} nil : ∅

β ⊢_{I} e : sT
β ⊢_{I} gvar id : sT = e : {id ↦ sT loc}
β ⊢_{I} e : sT
β ⊢_{I} lvar id : sT = e : {id ↦ sT loc}
fps : δ β[δ] ⊢_{I∪DI(fps)} body : sT

if body ≠ extern

β ⊢_{I} (function id(fps) : sT = body) : {id ↦ (fps → sT)}

fps : δ

β ⊢_{I} (function id(fps) : sT = extern) : {id ↦ (fps → sT)}

β[δ |_{J}] ⊢_{I∪J} g : δ

if J = FI(g) ∩ DI(g) and ∀id, sT : (id ↦ sT loc) ∉ δ

β ⊢_{I} (rec g) : δ

(1)

{β ⊢_{I} g_{0} : β_{0} β[β_{0}] ⊢_{I∪DI(g_{0})} g_{1} : β_{1} \atop β ⊢_{I} g_{0}; g_{1} : β_{0}[β_{1}]}  {β ⊢_{I} d_{0} : β_{0} β[β_{0}] ⊢_{I∪DI(d_{0})} d_{1} : β_{1} \atop β ⊢_{I} d_{0}; d_{1} : β_{0}[β_{1}]}

Note that rule (1) seems to suggest that δ must be guessed. Indeed, this is not the case, as it can be proved that the environment generated by a declaration g only depends on g and not on the environment used to establish whether g is well formed. While the right thing to do is to define two static semantics predicates for declarations —one for the generated environments and the other for well-formedness [Plo04]— we opted for a more concise presentation. Also notice that the side condition in rule (1) explicitly forbids recursive declarations of variables.^{4}

Exception declarations.

⊢_{I} χ : ∅  ⊢_{I} cT : ∅

⊢_{I} id : sT : {id ↦ sT loc}  ⊢_{I} any : ∅

Catch clauses.

{p : δ β[δ] ⊢_{I∪DI(p)} s \atop β ⊢_{I} (p) s}  {β ⊢_{I} k_{0} β ⊢_{I} k_{1} \atop β ⊢_{I} k_{0}; k_{1}}

4Namely, a recursive declaration such as rec gvar id : sT = e is not well-typed.

Statements.

β ⊢_{I} nop

β ⊢_{I} e : sT

if β(id) = sT loc

β ⊢_{I} id := e

β, fps ⊢_{I} es

if β(id_{0}) = sT loc and β(id) = fps → sT

β ⊢_{I} id_{0} := id(es)

{β ⊢_{I} s_{0} β ⊢_{I} s_{1} \atop β ⊢_{I} s_{0}; s_{1}}  {β ⊢_{I} d : β_{0} β[β_{0}] ⊢_{I∪DI(d)} s \atop β ⊢_{I} d; s}

β ⊢_{I} e : boolean β ⊢_{I} s_{0} β ⊢_{I} s_{1}

β ⊢_{I} if e then s_{0} else s_{1}

β ⊢_{I} e : boolean β ⊢_{I} s
β ⊢_{I} while e do s
β ⊢_{I} throw χ  {β ⊢_{I} e : sT \atop β ⊢_{I} throw e}
β ⊢_{I} s β ⊢_{I} k

β ⊢_{I} try s catch k

β ⊢_{I} s_{0} β ⊢_{I} s_{1}
β ⊢_{I} try s_{0} finally s_{1}

A program g is said to be valid if and only if it does not contain any occurrence of a reserved identifier id ∈ rId, ∅ ⊢_{∅} g : β and β(main) = □ → integer.

5. CONCRETE DYNAMIC SEMANTICS

For the specification of the concrete dynamic semantics for CPM, we adopt the G^{∞}SOS approach of Cousot and Cousot [CC92c]. This generalizes with infinite computations the natural semantics approach by Kahn [Kah87], which, in turn, is a “big-step” operational semantics defined by structural induction on program structures in the style of Plotkin [Plo04].

5.1 Absolute Locations and Indirect Locators

An absolute location (or, simply, location) is a unique identifier for a memory area of unspecified size. The (possibly infinite) set of all locations is denoted by Loc, while individual locations are denoted by l, l_{0}, l_{1} and so forth. We also postulate the existence of a set Ind =^{def} ℕ of indirect (stack) locators such that Loc ∩ Ind = ∅. Indirect locators are denoted by i, i_{0}, i_{1} and so forth. For notational convenience, we define the set of addresses as Addr =^{def} Loc ⊎ Ind. Addresses are denoted by a, a_{0}, a_{1} and so forth.

5.2 Concrete Execution Environments

The concrete dynamic aspect of declarations is captured by concrete execution environments. These map a finite set of identifiers to concrete denotable values. In the sequel we will simply write ‘environment’ to refer to execution environments.

Definition 5.1. (Abstract, dVal, Env_{I}.) We define

Abstract =^{def} { (λ fps . body, sT) | fps ∈ formParams, body ∈ Body, sT ∈ sType }.

The set of concrete denotable values is

dVal =^{def} (Addr × sType) ⊎ Abstract.

For I ⊆_{f} Id, Env_{I} =^{def} I → dVal is the set of concrete environments over I. The set of all environments is given by Env =^{def} ⨄_{I⊆_{f} Id} Env_{I}. Environments in Env_{I} are denoted by ρ, ρ_{0}, ρ_{1} and so forth. We write ρ : I as a shorthand for ρ ∈ Env_{I}. For ρ : I and β : I, we write ρ : β to signify that

∀id ∈ I : (∃(a, sT) ∈ Addr × sType . β(id) = sT loc ∧ ρ(id) = (a, sT))

∨(∃(λ fps . body, sT) ∈ Abstract . β(id) = fps → sT∧ρ(id) = (λ fps . body, sT)).

5.3 Memory Structures, Value States and Exception States

A memory structure uses a stack and suitable operators to allocate/deallocate, organize, read and update the locations of an absolute memory map, which is a partial function mapping a location and a storable type to a storable value. Memory structures model all the memory areas that are used in the most common implementations of imperative programming languages: the data segment (for global variables) and the stack segment (for local variables) are of interest for the language fragment we are considering; the text segment (where pointers to function point to) and the heap segment (for dynamically allocated memory) are required to deal with the extensions of Section 9. As it will be clear from the following definition, our notion of memory structure is underspecified: while we define it and its operations so that the semantics of programs is the expected one, we allow for many possible implementations by leaving out many details that are inessential to the achievement of that objective. It is for this same reason that we treat locations as unique identifiers neglecting the mathematical structure they may or may not have. More generally, what we call “concrete semantics” is indeed an abstraction of an infinite number of machines and compilation schemes that could be used to execute our programs. Furthermore, since the considered fragment of CPM does not support pointers, arrays, type casts and unions, we can here make the simplifying assumption that there is no overlap between the storage cells associated to different locations. In Section 9 we will hint at how these assumptions must be modified in order to accommodate the full language.

Memory structures will be used to describe the outcome of computations whose only observable behavior is given by their side effects. Computations yielding a proper value will be described by a value state, which pairs the value computed with a memory structure recording the side effects of the execution. Exceptional behavior must, of course, be taken into proper account: thus, the result of an exceptional computation path will be described by pairing the memory structure with an exception, yielding what we call an exception state.

Definition 5.2. (Map, Stack, Mem, ValState, ExceptState.) The set of all absolute maps is the set of partial functions

Map =^{def} (Loc × sType) ↣ sVal.

Absolute maps are denoted by μ, μ_{0}, μ_{1} and so forth. The absolute map update partial function

·[· := ·]: (Map × (Loc × sType) × sVal) ↣ Map

is defined, for each μ ∈ Map, (l, sT) ∈ Loc × sType such that (l, sT) ∈ dom(μ) and sval ∈ sVal such that sT = type(sval), by

μ[(l, sT) := sval] =^{def} μ′,

where μ′ ∈ Map is any absolute map satisfying the following conditions:

(i) dom(μ′) = dom(μ); (ii) μ′(l, sT) = sval; (iii) μ′(l′, sT′) = μ(l′, sT′), for each (l′, sT′) ∈ dom(μ) such that l′ ≠ l.

Let W =^{def} (Loc∪{†, ‡})^{⋆}. An element w ∈ W is a stack if and only if no location occurs more than once in it. The set of all stacks is denoted by Stack. ‘ †’ is called stack marker and ‘ ‡’ is called frame marker. The top-most frame of w ∈ Stack, denoted by tf(w), is the longest suffix of w containing no frame marker; formally, tf(w) ∈ (Loc ∪ {†})^{⋆} satisfies either w = tf(w) or w = w′‡ tf(w). The partial infix operator @: Stack × Ind ↣ Loc maps, when defined, a stack w and an indirect locator i into an absolute location to be found in the top-most frame; formally, if tf(w) = z_{0} ⋯ z_{n−1} where, for all i < n, z_{i} = †^{⋆} · l_{i} · †^{⋆} and l_{i} ∈ Loc, then, for each

i < n, w @ i =^{def} l_{i}.

A memory structure is an element of Mem =^{def} Map × Stack. Memory structures are denoted by σ, σ_{0}, σ_{1} and so forth.

A value state is an element of ValState =^{def} sVal × Mem. Value states are denoted by υ, υ_{0}, υ_{1} and so forth.

An exception state is an element of ExceptState =^{def} Mem × Except. Exception states are denoted by ε, ε_{0}, ε_{1} and so forth.

The overloading @: Mem×Addr ↣ Loc of the partial infix operator @ is defined, for each σ = (μ, w) and a ∈ Addr, as follows and under the following conditions:

σ @ a =^{def} \begin{cases}a, & if a ∈ Loc; \\ l, & if a ∈ Ind and l = w @ a is defined. \end{cases}

The memory structure read and update operators

·[·, ·]: (Mem × Addr × sType) → (ValState ⊎ ExceptState),
·[· := ·]: (Mem × (Addr × sType) × sVal) → (Mem ⊎ ExceptState)

are respectively defined, for each σ = (μ, w) ∈ Mem, a ∈ Addr, sT ∈ sType and sval ∈ sVal, as follows: let d = (σ @ a, sT); then

σ[a, sT] =^{def} \begin{cases}(μ(d), σ), & if d ∈ dom(μ); \\ (σ, memerror), & otherwise; \end{cases}

σ[(a, sT) := sval] =^{def} \begin{cases}(μ[d := sval], w), & if d ∈ dom(μ) and sT = type(sval); \\ (σ, memerror), & otherwise. \end{cases}

The data and stack memory allocation functions

new_{d} : ValState → ((Mem × Loc) ⊎ ExceptState),
new_{s} : ValState → ((Mem × Ind) ⊎ ExceptState)

are defined, for each υ = (sval, σ) ∈ ValState, where σ = (μ, w), by

new_{d}(υ) =^{def} \begin{cases}((μ′, w), l), & if the data segment of σ can be extended; \\ (σ, datovflw), & otherwise; \end{cases}
new_{s}(υ) =^{def} \begin{cases}((μ′, w′), i), & if the stack segment of σ can be extended; \\ (σ, stkovflw), & otherwise; \end{cases}

where, in the case of new_{s}, w′ ∈ Stack and i ∈ Ind are such that:

(i) w′ = w · l; (ii) i = | tf(w)|; and, for both new_{d} and new_{s}, μ′ ∈ Map and l ∈ Loc are such that: (iii) for each sT ∈ sType, (l, sT) ∉ dom(μ); (iv) for each (l′, sT′) ∈ dom(μ), μ′(l′, sT′) = μ(l′, sT′);

(v) μ′(l, type(sval)) = sval. The memory structure data cleanup function cleanup_{d} : ExceptState → ExceptState is given, for each ε = (σ, ξ) ∈ ExceptState, by

cleanup_{d}(ε) =^{def} ((∅, ϵ), ξ).

The stack mark function mark_{s} : Mem → Mem is given, for each σ ∈ Mem, by

mark_{s}(σ) =^{def} (μ, w†), where σ = (μ, w).

The stack unmark partial function unmark_{s} : Mem ↣ Mem is given, for each σ ∈ Mem such that σ = (μ, w′†w′′) and w′′ ∈ Loc^{⋆}, by

unmark_{s}(μ, w′†w′′) =^{def} (μ′, w′),

where the absolute map μ′ ∈ Map satisfies:

(i) dom(μ′) = { (l, sT) ∈ dom(μ) | l does not occur in w′′ }; (ii) μ′ = μ |_{dom(μ′)}. The frame link partial function link_{s} : Mem ↣ Mem is given, for each σ ∈ Mem such that σ = (μ, w′†w′′) and w′′ ∈ Loc^{⋆}, by

link_{s}(μ, w′†w′′) =^{def} (μ, w′‡w′′).

The frame unlink partial function unlink_{s} : Mem ↣ Mem is given, for each σ ∈ Mem such that σ = (μ, w′‡w′′) and w′′ ∈ Loc^{⋆}, by

unlink_{s}(μ, w′‡w′′) =^{def} (μ, w′†w′′).

For ease of notation, the stack unmark and the frame unlink partial functions are lifted to also work on exception states. Namely, for each ε = (σ, ξ) ∈ ExceptState,

unmark_{s}(σ, ξ) =^{def} (unmark_{s}(σ), ξ);
unlink_{s}(σ, ξ) =^{def} (unlink_{s}(σ), ξ).

Intuitively, global variables are allocated in the data segment using new_{d} and are accessed through absolute locations; function cleanup_{d} models their deallocation due to an RTS exception thrown during the program start-up phase. The functions mark_{s} and unmark_{s} use the stack marker ‘†’ to implement the automatic allocation (through new_{s}) and deallocation of stack slots for storing local variables, return values and actual arguments of function calls. The functions link_{s} and unlink_{s} use the frame marker ‘‡’ to partition the stack into activation frames, each frame corresponding to a function call. All accesses to the top-most frame can be expressed in terms of indirect locators (i.e., offsets from the top-most frame marker), because at each program point the layout of the current top-most frame is statically known. As it will be clearer when considering the concrete rules for function calls, the frame marker is used to move the return value and the actual arguments, which are allocated by the caller, from the activation frame of the caller to the activation frame of the callee, and vice versa.

The memory structures and operations satisfy the following property: for each pair of memory structures σ_{0} and σ_{1} such that σ_{1} has been obtained from σ_{0} by any sequence of operations where each link_{s} is matched by a corresponding unlink_{s}, for each indirect locator i ∈ Ind, if σ_{0}@i and σ_{1}@i are both defined, then σ_{0}@i = σ_{1}@i.

As anticipated, we profit from the lack of aliasing in the fragment of CPM considered here, i.e., we assume there is no overlap between the storage cells associated to (l_{0}, sT_{0}) and the ones associated to (l_{1}, sT_{1}), unless l_{0} = l_{1}. Moreover, we need not specify the relationship between μ(l, sT_{0}) and μ(l, sT_{1}) for the case where sT_{0} ≠ sT_{1}. This also implies that the absolute map update operator is underspecified, resulting in a nondeterministic operator. Of course, any real implementation will be characterized by a complete specification: for instance, a precise definition of the memory overflow conditions will take the place of the informal conditions “if the data (resp., stack) segment of σ can be extended” in the definitions of new_{d} and new_{s}. As is clear from the definition above, where memory is writable if and only if it is readable, we do not attempt to model read-only memory. It is also worth observing that, in the sequel, the “meaning” of variable identifiers will depend on unrestricted elements of Env × Mem. As a consequence we can have dangling references, that is, a pair (ρ, σ) ∈ Env × Mem with ρ : I can be such that there exists an identifier id ∈ I for which ρ(id) = (a, sT) and σ[a, sT] = memerror.

5.4 Configurations

The dynamic semantics of CPM is expressed by means of an evaluation (or reduction) relation, which specifies how a non-terminal configuration is reduced to a terminal configuration. The sets of non-terminal configurations are parametric with respect to a type environment associating every identifier to its type.

Definition 5.3. (Non-terminal configurations.) The sets of non-terminal configurations for expressions, local and global declarations, statements, function bodies and catch clauses are given, respectively and for each β ∈ TEnv_{I}, by

Γ_{e}^{β} =^{def} { ⟨e, σ⟩ ∈ Exp × Mem | ∃sT ∈ sType . β ⊢_{I} e : sT },
Γ_{d}^{β} =^{def} { ⟨d, σ⟩ ∈ Decl × Mem | ∃δ ∈ TEnv . β ⊢_{I} d : δ },
Γ_{g}^{β} =^{def} { ⟨g, σ⟩ ∈ Glob × Mem | ∃δ ∈ TEnv . β ⊢_{I} g : δ },
Γ_{s}^{β} =^{def} { ⟨s, σ⟩ ∈ Stmt × Mem | β ⊢_{I} s },
Γ_{b}^{β} =^{def} { ⟨body, σ⟩ ∈ Body × Mem | ∃sT ∈ sType . β ⊢_{I} body : sT },
Γ_{k}^{β} =^{def} { ⟨k, ε⟩ ∈ Catch × ExceptState | β ⊢_{I} k }.

Each kind of terminal configuration has to allow for the possibility of both a non-exceptional and an exceptional computation path.

Definition 5.4. (Terminal configurations.) The sets of terminal configurations for expressions, local and global declarations, statements, function bodies and catch clauses are given, respectively, by

T_{e} =^{def} ValState ⊎ ExceptState,
T_{d} =^{def} T_{g} =^{def} (Env × Mem) ⊎ ExceptState,
T_{s} =^{def} T_{b} =^{def} Mem ⊎ ExceptState,
T_{k} =^{def} ({caught} × T_{s}) ⊎ ({uncaught} × ExceptState).

Note that T_{e} is defined as ValState ⊎ ExceptState; as it will be apparent from the concrete semantics, expressions never modify the memory structure, so T_{e} could have been defined as sVal ⊎ Except; but defining it as ValState ⊎ ExceptState simplifies the approximation relations in Section 6.

In the following, we write N and η to denote a non-terminal and a terminal concrete configuration, respectively. For clarity of notation, we often use angle brackets to highlight that a tuple is indeed representing a configuration. Angle brackets are not normally used for configurations made of a single element. Therefore, when ε = (σ, ξ) ∈ ExceptState, we indifferently write ε ∈ T_{s} or ⟨σ, ξ⟩ ∈ T_{s}, as well as ⟨caught, ε⟩ ∈ T_{k} or ⟨caught, (σ, ξ)⟩ ∈ T_{k}.

A few explanatory words are needed for T_{k}. When the evaluation of a nonterminal configuration for catch clauses ⟨k, ε⟩ ∈ Γ_{k}^{β} yields the terminal configuration ⟨caught, η⟩ ∈ T_{k}, then the exception ξ in ε = (σ, ξ) was caught inside k and η ∈ T_{s} is the result of evaluating the corresponding exception handler statement; note that η ∈ T_{s} may itself be another exception state, meaning that another exception was thrown during the evaluation of the exception handler statement. In contrast, when the resulting terminal configuration is ⟨uncaught, ε⟩ ∈ T_{k}, then the exception in ε was not caught inside k and will be propagated to the outer context.^{5}

5Note that the names of the labels caught and uncaught have been chosen as such for clarity, but provide no special meaning: they are only needed for a correct application of the disjoint union construction, since we have T_{s} ∩ ExceptState ≠ ∅.

5.5 Concrete Evaluation Relations

For convenience, in order to represent function closures, we extend the syntactic category of local declarations with (recursive) execution environments. These syntactic constructs are meant to be only available in the dynamic semantics (in non-terminal configurations): they cannot occur in the program text. Thus we have

Decl ∋ d ::= … | ρ | rec ρ

Consequently, if ρ : I we define DI(ρ) =^{def} DI(rec ρ) =^{def} I, FI(ρ) =^{def} ⋃_{id∈I} FI(ρ(id))

and FI(rec ρ) =^{def} FI(ρ) \ I, where the function FI is defined on elements of dVal by FI(l, sT) =^{def} FI(i, sT) =^{def} ∅ and FI(λ fps . body) =^{def} FI(body) \ DI(fps). The static semantics is extended by adding the rules

{ρ : δ \atop β ⊢_{I} ρ : δ} β[δ |_{J}] ⊢_{I∪J} ρ : δ

if J = FI(ρ) ∩ DI(ρ) and ∀id : (id ↦ sT loc) ∉ δ.

β ⊢_{I} rec ρ : δ

The concrete evaluation relations that complete the definition of the concrete semantics for CPM are defined, as usual, by structural induction from a set of rule schemata. The evaluation relations are of the form ρ ⊢_{β} N → η, where β ∈ TEnv_{I}, ρ ∈ Env_{J}, ρ : β |_{J} and, for some q ∈ {e, d, g, s, b, k}, N ∈ Γ_{q}^{β} and η ∈ T_{q}.

5.5.1 Expressions

Constant.

ρ ⊢_{β} ⟨con, σ⟩ → ⟨con, σ⟩  (2)

Identifier.

ρ ⊢_{β} ⟨id, σ⟩ → σ[ρ(id)]  (3)

Unary minus.

{ρ ⊢_{β} ⟨e, σ⟩ → ε \atop ρ ⊢_{β} ⟨−e, σ⟩ → ε}  (4)

{ρ ⊢_{β} ⟨e, σ⟩ → ⟨m, σ_{0}⟩ \atop ρ ⊢_{β} ⟨−e, σ⟩ → ⟨−m, σ_{0}⟩}  (5)

Binary arithmetic operations. Letting ⧇ denote any abstract syntax operator in {+, −, ∗, /, %} and ∘ ∈ {+, −, ·, ÷, mod} the corresponding arithmetic operation. Then the rules for addition, subtraction, multiplication, division and remainder are given by the following schemata:

{ρ ⊢_{β} ⟨e_{0}, σ⟩ → ε \atop ρ ⊢_{β} ⟨e_{0} ⧇ e_{1}, σ⟩ → ε}  (6)

{ρ ⊢_{β} ⟨e_{0}, σ⟩ → ⟨m_{0}, σ_{0}⟩ ρ ⊢_{β} ⟨e_{1}, σ_{0}⟩ → ε \atop ρ ⊢_{β} ⟨e_{0} ⧇ e_{1}, σ⟩ → ε}  (7)

ρ ⊢_{β} ⟨e_{0}, σ⟩ → ⟨m_{0}, σ_{0}⟩ ρ ⊢_{β} ⟨e_{1}, σ_{0}⟩ → ⟨m_{1}, σ_{1}⟩ ; \overline{if ⧇ ∉ \{/, %\} or m_{1} ≠ 0} ; ρ ⊢_{β} ⟨e_{0} ⧇ e_{1}, σ⟩ → ⟨m_{0} ∘ m_{1}, σ_{1}⟩(8)

ρ ⊢_{β} ⟨e_{0}, σ⟩ → ⟨m_{0}, σ_{0}⟩ ρ ⊢_{β} ⟨e_{1}, σ_{0}⟩ → ⟨0, σ_{1}⟩

\overline{if ⧇ ∈ \{/, %\}}

ρ ⊢_{β} ⟨e_{0} ⧇ e_{1}, σ⟩ → ⟨σ_{1}, divbyzero⟩ (9)

Arithmetic tests. Let ⧆ ∈ {=, ≠, <, ≤, ≥, >} be an abstract syntax operator and denote with ‘≶’ the corresponding test operation in ℤ × ℤ → Bool. The rules for the arithmetic tests are then given by the following schemata:

{ρ ⊢_{β} ⟨e_{0}, σ⟩ → ε \atop ρ ⊢_{β} ⟨e_{0} ⧆ e_{1}, σ⟩ → ε}  (10)

{ρ ⊢_{β} ⟨e_{0}, σ⟩ → ⟨m_{0}, σ_{0}⟩ ρ ⊢_{β} ⟨e_{1}, σ_{0}⟩ → ε \atop ρ ⊢_{β} ⟨e_{0} ⧆ e_{1}, σ⟩ → ε}  (11)

{ρ ⊢_{β} ⟨e_{0}, σ⟩ → ⟨m_{0}, σ_{0}⟩ ρ ⊢_{β} ⟨e_{1}, σ_{0}⟩ → ⟨m_{1}, σ_{1}⟩ \atop ρ ⊢_{β} ⟨e_{0} ⧆ e_{1}, σ⟩ → ⟨m_{0} ≶ m_{1}, σ_{1}⟩}  (12)

Negation.

{ρ ⊢_{β} ⟨b, σ⟩ → ε \atop ρ ⊢_{β} ⟨not b, σ⟩ → ε}  (13)

{ρ ⊢_{β} ⟨b, σ⟩ → ⟨t, σ_{0}⟩ \atop ρ ⊢_{β} ⟨not b, σ⟩ → ⟨¬ t, σ_{0}⟩}  (14)

Conjunction.

{ρ ⊢_{β} ⟨b_{0}, σ⟩ → ε \atop ρ ⊢_{β} ⟨b_{0} and b_{1}, σ⟩ → ε}  (15)

{ρ ⊢_{β} ⟨b_{0}, σ⟩ → ⟨ff, σ_{0}⟩ \atop ρ ⊢_{β} ⟨b_{0} and b_{1}, σ⟩ → ⟨ff, σ_{0}⟩}  (16)

{ρ ⊢_{β} ⟨b_{0}, σ⟩ → ⟨tt, σ_{0}⟩ ρ ⊢_{β} ⟨b_{1}, σ_{0}⟩ → η \atop ρ ⊢_{β} ⟨b_{0} and b_{1}, σ⟩ → η}  (17)

Disjunction.

{ρ ⊢_{β} ⟨b_{0}, σ⟩ → ε \atop ρ ⊢_{β} ⟨b_{0} or b_{1}, σ⟩ → ε}  (18)

{ρ ⊢_{β} ⟨b_{0}, σ⟩ → ⟨tt, σ_{0}⟩ \atop ρ ⊢_{β} ⟨b_{0} or b_{1}, σ⟩ → ⟨tt, σ_{0}⟩}  (19)

{ρ ⊢_{β} ⟨b_{0}, σ⟩ → ⟨ff, σ_{0}⟩ ρ ⊢_{β} ⟨b_{1}, σ_{0}⟩ → η \atop ρ ⊢_{β} ⟨b_{0} or b_{1}, σ⟩ → η}  (20)

On the Design of Generic Static Analyzers for Imperative Languages · 21

5.5.2 Declarations Nil.

ρ ⊢_{β} ⟨nil, σ⟩ → ⟨∅, σ⟩  (21)

Environment.

ρ ⊢_{β} ⟨ρ_{0}, σ⟩ → ⟨ρ_{0}, σ⟩  (22)

Recursive environment.

ρ ⊢_{β} ⟨rec ρ_{0}, σ⟩ → ⟨ρ_{1}, σ⟩  (23)

if ρ_{1} = { id ↦ ρ_{0}(id) | ρ_{0}(id) = (λ fps . extern, sT) }

∪ \{ id ↦ abs_{1} | \begin{matrix}∀i ∈ \{0, 1\} : abs_{i} = (λ fps . let d_{i} in s result e, sT), \\ ρ_{0}(id) = abs_{0}, d_{1} = rec(ρ_{0} \ DI(fps)); d_{0} \end{matrix} \}.

Global variable declaration.

ρ ⊢_{β} ⟨e, σ⟩ → ε

ρ ⊢_{β} ⟨gvar id : sT = e, σ⟩ → cleanup_{d}(ε)

(24)

ρ ⊢_{β} ⟨e, σ⟩ → υ

\overline{if new_{d}(υ) = ε}

ρ ⊢_{β} ⟨gvar id : sT = e, σ⟩ → cleanup_{d}(ε)

(25)

ρ ⊢_{β} ⟨e, σ⟩ → υ

ρ ⊢_{β} ⟨gvar id : sT = e, σ⟩ → ⟨ρ_{1}, σ_{1}⟩ (26)

if new_{d}(υ) = (σ_{1}, l) and ρ_{1} = {id ↦ (l, sT)}.

Local variable declaration.

ρ ⊢_{β} ⟨e, σ⟩ → ε

ρ ⊢_{β} ⟨lvar id : sT = e, σ⟩ → unmark_{s}(ε)

(27)

ρ ⊢_{β} ⟨e, σ⟩ → υ

\overline{if new_{s}(υ) = ε}

ρ ⊢_{β} ⟨lvar id : sT = e, σ⟩ → unmark_{s}(ε)

(28)

ρ ⊢_{β} ⟨e, σ⟩ → υ

ρ ⊢_{β} ⟨lvar id : sT = e, σ⟩ → ⟨ρ_{1}, σ_{1}⟩ (29)

if new_{s}(υ) = (σ_{1}, i) and ρ_{1} = {id ↦ (i, sT)}.

Function declaration.

ρ ⊢_{β} ⟨function id(fps) : sT = body_{0}, σ⟩ → ⟨ρ_{0}, σ⟩  (30)

if ρ_{0} = {id ↦ (λ fps . body_{1}, sT)} and either body_{0} = body_{1} = extern or, for each i ∈ {0, 1}, body_{i} = let d_{i} in s result e, I = FI(body_{0}) \ DI(fps) and d_{1} = ρ |_{I}; d_{0}.

22 · R. Bagnara, P.M. Hill, A. Pescetti, and E. Zaffanella

Recursive declaration.

{(ρ \ J) ⊢_{β[β_{1}]} ⟨g, σ⟩ → ⟨ρ_{0}, σ_{0}⟩ ρ ⊢_{β} ⟨rec ρ_{0}, σ_{0}⟩ → η \atop ρ ⊢_{β} ⟨rec g, σ⟩ → η}  (31)

if J = FI(g) ∩ DI(g), β ⊢_{FI(g)} g : β_{0} and β_{1} = β_{0} |_{J}. Global sequential composition.

{ρ ⊢_{β} ⟨g_{0}, σ⟩ → ε \atop ρ ⊢_{β} ⟨g_{0}; g_{1}, σ⟩ → ε}  (32)
ρ ⊢_{β} ⟨g_{0}, σ⟩ → ⟨ρ_{0}, σ_{0}⟩ ρ[ρ_{0}] ⊢_{β[β_{0}]} ⟨g_{1}, σ_{0}⟩ → ε ; \overline{if β ⊢_{FI(g_{0})} g_{0} : β_{0}} ; ρ ⊢_{β} ⟨g_{0}; g_{1}, σ⟩ → ε  (33)

ρ ⊢_{β} ⟨g_{0}, σ⟩ → ⟨ρ_{0}, σ_{0}⟩ ρ[ρ_{0}] ⊢_{β[β_{0}]} ⟨g_{1}, σ_{0}⟩ → ⟨ρ_{1}, σ_{1}⟩ ; \overline{if β ⊢_{FI(g_{0})} g_{0} : β_{0}} ; ρ ⊢_{β} ⟨g_{0}; g_{1}, σ⟩ → ⟨ρ_{0}[ρ_{1}], σ_{1}⟩(34)

Local sequential composition.

{ρ ⊢_{β} ⟨d_{0}, σ⟩ → ε \atop ρ ⊢_{β} ⟨d_{0}; d_{1}, σ⟩ → ε}  (35)
ρ ⊢_{β} ⟨d_{0}, σ⟩ → ⟨ρ_{0}, σ_{0}⟩ ρ[ρ_{0}] ⊢_{β[β_{0}]} ⟨d_{1}, σ_{0}⟩ → ε ; \overline{if β ⊢_{FI(d_{0})} d_{0} : β_{0}} ; ρ ⊢_{β} ⟨d_{0}; d_{1}, σ⟩ → ε  (36)

ρ ⊢_{β} ⟨d_{0}, σ⟩ → ⟨ρ_{0}, σ_{0}⟩ ρ[ρ_{0}] ⊢_{β[β_{0}]} ⟨d_{1}, σ_{0}⟩ → ⟨ρ_{1}, σ_{1}⟩ ; \overline{if β ⊢_{FI(d_{0})} d_{0} : β_{0}} ; ρ ⊢_{β} ⟨d_{0}; d_{1}, σ⟩ → ⟨ρ_{0}[ρ_{1}], σ_{1}⟩(37)

5.5.3 Statements Nop.

ρ ⊢_{β} ⟨nop, σ⟩ → σ  (38)

Assignment.

{ρ ⊢_{β} ⟨e, σ⟩ → ε \atop ρ ⊢_{β} ⟨id := e, σ⟩ → ε}  (39)
ρ ⊢_{β} ⟨e, σ⟩ → ⟨sval, σ_{0}⟩

ρ ⊢_{β} ⟨id := e, σ⟩ → σ_{0}[ρ(id) := sval]

(40)

Statement sequence.

{ρ ⊢_{β} ⟨s_{0}, σ⟩ → ε \atop ρ ⊢_{β} ⟨s_{0}; s_{1}, σ⟩ → ε}  (41)
{ρ ⊢_{β} ⟨s_{0}, σ⟩ → σ_{0} ρ ⊢_{β} ⟨s_{1}, σ_{0}⟩ → η \atop ρ ⊢_{β} ⟨s_{0}; s_{1}, σ⟩ → η}  (42)

On the Design of Generic Static Analyzers for Imperative Languages · 23

Block.

ρ ⊢_{β} ⟨d, mark_{s}(σ)⟩ → ε ; ρ ⊢_{β} ⟨d; s, σ⟩ → ε  (43)

ρ ⊢_{β} ⟨d, mark_{s}(σ)⟩ → ⟨ρ_{0}, σ_{0}⟩ ρ[ρ_{0}] ⊢_{β[β_{0}]} ⟨s, σ_{0}⟩ → η

\overline{if β ⊢_{FI(d)} d : β_{0}}
ρ ⊢_{β} ⟨d; s, σ⟩ → unmark_{s}(η)

(44)

Conditional.

ρ ⊢_{β} ⟨e, σ⟩ → ε

ρ ⊢_{β} ⟨if e then s_{0} else s_{1}, σ⟩ → ε (45)

ρ ⊢_{β} ⟨e, σ⟩ → ⟨tt, σ_{0}⟩ ρ ⊢_{β} ⟨s_{0}, σ_{0}⟩ → η

ρ ⊢_{β} ⟨if e then s_{0} else s_{1}, σ⟩ → η (46)

ρ ⊢_{β} ⟨e, σ⟩ → ⟨ff, σ_{0}⟩ ρ ⊢_{β} ⟨s_{1}, σ_{0}⟩ → η

ρ ⊢_{β} ⟨if e then s_{0} else s_{1}, σ⟩ → η (47)

While.

{ρ ⊢_{β} ⟨e, σ⟩ → ε \atop ρ ⊢_{β} ⟨while e do s, σ⟩ → ε}  (48)

ρ ⊢_{β} ⟨e, σ⟩ → ⟨ff, σ_{0}⟩

ρ ⊢_{β} ⟨while e do s, σ⟩ → σ_{0} (49)

ρ ⊢_{β} ⟨e, σ⟩ → ⟨tt, σ_{0}⟩ ρ ⊢_{β} ⟨s, σ_{0}⟩ → ε

ρ ⊢_{β} ⟨while e do s, σ⟩ → ε (50)

ρ ⊢_{β} ⟨e, σ⟩ → ⟨tt, σ_{0}⟩ ρ ⊢_{β} ⟨s, σ_{0}⟩ → σ_{1} ρ ⊢_{β} ⟨while e do s, σ_{1}⟩ → η

ρ ⊢_{β} ⟨while e do s, σ⟩ → η (51)

Throw.

ρ ⊢_{β} ⟨throw χ, σ⟩ → ⟨σ, χ⟩  (52)
{ρ ⊢_{β} ⟨e, σ⟩ → ε \atop ρ ⊢_{β} ⟨throw e, σ⟩ → ε}  (53)

ρ ⊢_{β} ⟨e, σ⟩ → ⟨sval, σ_{0}⟩

ρ ⊢_{β} ⟨throw e, σ⟩ → ⟨σ_{0}, sval⟩ (54)

Try blocks.

ρ ⊢_{β} ⟨s, σ⟩ → σ_{0}

ρ ⊢_{β} ⟨try s catch k, σ⟩ → σ_{0} (55)

ρ ⊢_{β} ⟨s, σ⟩ → ε_{0} ρ ⊢_{β} ⟨k, ε_{0}⟩ → ⟨u, η⟩

                                  if u ∈ {caught, uncaught}

ρ ⊢_{β} ⟨try s catch k, σ⟩ → η (56) ρ ⊢_{β} ⟨s_{0}, σ⟩ → σ_{0} ρ ⊢_{β} ⟨s_{1}, σ_{0}⟩ → η

ρ ⊢_{β} ⟨try s_{0} finally s_{1}, σ⟩ → η (57)

ρ ⊢_{β} ⟨s_{0}, σ⟩ → ⟨σ_{0}, ξ_{0}⟩ ρ ⊢_{β} ⟨s_{1}, σ_{0}⟩ → σ_{1}

ρ ⊢_{β} ⟨try s_{0} finally s_{1}, σ⟩ → ⟨σ_{1}, ξ_{0}⟩ (58)

ρ ⊢_{β} ⟨s_{0}, σ⟩ → ⟨σ_{0}, ξ_{0}⟩ ρ ⊢_{β} ⟨s_{1}, σ_{0}⟩ → ε

ρ ⊢_{β} ⟨try s_{0} finally s_{1}, σ⟩ → ε (59)

Function call. Consider the following conditions:

\begin{matrix}β(id) & = (fps → sT_{0}) \\ ρ(id) & = λ id_{1} : sT_{1}, …, id_{n} : sT_{n} . body \\ d & = (lvar \underline{x}_{0} : sT_{0} = id_{0}; lvar \underline{x}_{1} : sT_{1} = e_{1}; …; lvar \underline{x}_{n} : sT_{n} = e_{n}) \end{matrix}\} (60)

ρ_{1} = \{\underline{x}_{0} ↦ (0, sT_{0})\} ∪ \{ id_{j} ↦ (j, sT_{j}) | j = 1, …, n \}, ρ_{0} : β_{0}, ρ_{1} : β_{1}. (61)

Then the rule schemata for function calls are the following:

ρ ⊢_{β} ⟨d, mark_{s}(σ)⟩ → ε
\overline{if (60) holds}

ρ ⊢_{β} ⟨id_{0} := id(e_{1}, …, e_{n}), σ⟩ → ε

(62)

ρ ⊢_{β} ⟨d, mark_{s}(σ)⟩ → ⟨ρ_{0}, σ_{0}⟩
ρ[ρ_{1}] ⊢_{β[β_{1}]} ⟨body, link_{s}(σ_{0})⟩ → ε

if (60) and (61) hold

ρ ⊢_{β} ⟨id_{0} := id(e_{1}, …, e_{n}), σ⟩ → unmark_{s}(unlink_{s}(ε))

(63)

ρ ⊢_{β} ⟨d, mark_{s}(σ)⟩ → ⟨ρ_{0}, σ_{0}⟩

ρ[ρ_{1}] ⊢_{β[β_{1}]} ⟨body, link_{s}(σ_{0})⟩ → σ_{1}

ρ[ρ_{0}] ⊢_{β[β_{0}]} ⟨id_{0} := \underline{x}_{0}, unlink_{s}(σ_{1})⟩ → η_{2}

if (60) and (61) hold

ρ ⊢_{β} ⟨id_{0} := id(e_{1}, …, e_{n}), σ⟩ → unmark_{s}(η_{2})

(64)

Note that parameter passing is implemented by using reserved identifiers that reference the return value (\underline{x}_{0}) and the actual arguments (\underline{x}_{1}, …, \underline{x}_{n}). When evaluating the function body (i.e., after linking a new activation frame), the callee can get access to the return value and the arguments’ values by using the indirect locators 0 and 1, …, n, respectively; to this end, the callee uses the environment ρ_{1}, where the reserved identifier \underline{x}_{0} is still mapped to the return value, whereas the arguments are accessible using the formal parameters’ names id_{1}, …, id_{n}.

5.5.4 Function Bodies.

ρ ⊢_{β} ⟨d, mark_{s}(σ)⟩ → ε

ρ ⊢_{β} ⟨let d in s result e, σ⟩ → ε

(65)

ρ ⊢_{β} ⟨d, mark_{s}(σ)⟩ → ⟨ρ_{0}, σ_{0}⟩ ρ[ρ_{0}] ⊢_{β[β_{0}]} ⟨s, σ_{0}⟩ → ε

\overline{if β ⊢_{FI(d)} d : β_{0}}
ρ ⊢_{β} ⟨let d in s result e, σ⟩ → unmark_{s}(ε)

(66) ρ ⊢_{β} ⟨d, mark_{s}(σ)⟩ → ⟨ρ_{0}, σ_{0}⟩ ρ[ρ_{0}] ⊢_{β[β_{0}]} ⟨s, σ_{0}⟩ → σ_{1}

ρ[ρ_{0}] ⊢_{β[β_{0}]} ⟨\underline{x}_{0} := e, σ_{1}⟩ → η_{0} \overline{if β ⊢_{FI(d)} d : β_{0}}

ρ ⊢_{β} ⟨let d in s result e, σ⟩ → unmark_{s}(η_{0})

(67)

ρ ⊢_{β} ⟨extern, (μ, w)⟩ → η  (68)

if ∃σ_{0} = (μ_{0}, w) ∈ Mem, ξ ∈ Except . η = σ_{0} ∨ η = ⟨σ_{0}, ξ⟩.

5.5.5 Catch Clauses

Catch.

ρ ⊢_{β} ⟨s, σ⟩ → η_{0} ; ρ ⊢_{β} ⟨(p) s, (σ, ξ)⟩ → ⟨caught, η_{0}⟩  (69)

if p = ξ ∈ RTSExcept, or p = type(ξ), or p = any.

ρ ⊢_{β} ⟨(id : sT) s, (σ, sval)⟩ → ⟨caught, unmark_{s}(ε_{0})⟩  (70)

if sT = type(sval) and ε_{0} = new_{s}(sval, mark_{s}(σ)).

ρ[{id ↦ (i, sT)}] ⊢_{β[{id↦sT loc}]} ⟨s, σ_{0}⟩ → η_{0}
ρ ⊢_{β} ⟨(id : sT) s, (σ, sval)⟩ → ⟨caught, unmark_{s}(η_{0})⟩

(71)

if sT = type(sval) and (σ_{0}, i) = new_{s}(sval, mark_{s}(σ)).

ρ ⊢_{β} ⟨(p) s, (σ, ξ)⟩ → ⟨uncaught, (σ, ξ)⟩  (72)

if, letting cT = type(ξ), we have p ∉ {ξ, cT, any} and ∀id ∈ Id : p ≠ id : cT. Catch sequence.

ρ ⊢_{β} ⟨k_{0}, ε⟩ → ⟨caught, η_{0}⟩

ρ ⊢_{β} ⟨k_{0}; k_{1}, ε⟩ → ⟨caught, η_{0}⟩ (73)

ρ ⊢_{β} ⟨k_{0}, ε⟩ → ⟨uncaught, ε_{0}⟩ ρ ⊢_{β} ⟨k_{1}, ε_{0}⟩ → η

ρ ⊢_{β} ⟨k_{0}; k_{1}, ε⟩ → η (74)

5.6 Concrete Divergence Relation

In order to capture divergent computations, we follow the approach of Cousot and Cousot [CC92c], also advocated by Schmidt [Sch98] and Leroy [Ler06]. This consists in introducing a divergence relation by means of sequents of the form ρ ⊢_{β} N ⟶^{∞}, where N ∈ Γ_{q} and q ∈ {s, b, k}. Intuitively, a divergence sequent of the form, say, ρ ⊢_{β} ⟨s, σ⟩ ⟶^{∞} means that, in the context given by ρ and σ, the execution of statement s diverges. We now give a set of rules that (interpreted coinductively, as we will see later) allow to characterize the behavior of divergent computations. For instance, the following rule schemata characterize the divergence behavior of statement sequences:

ρ ⊢_{β} ⟨s_{0}, σ⟩ ⟶^{∞} ; = ; ρ ⊢_{β} ⟨s_{0}; s_{1}, σ⟩ ⟶^{∞}  ρ ⊢_{β} ⟨s_{0}, σ⟩ → σ_{0} ρ ⊢_{β} ⟨s_{1}, σ_{0}⟩ ⟶^{∞} ; = ; ρ ⊢_{β} ⟨s_{0}; s_{1}, σ⟩ ⟶^{∞}

Notice that, once the set of concrete rules characterizing finite computations is known, the concrete rules modeling divergences can be specified systematically (and thus implicitly). Namely, for each concrete rule

P_{0} ⋯ P_{i−1} ρ_{i} ⊢_{β_{i}} N_{i} → η_{i} P_{i+1} ⋯ P_{h−1}

(side condition)

ρ ⊢_{β} N → η (75)

such that 0 ≤ i < h and, for q ∈ {s, b, k}, N_{i} ∈ ⨄ Γ_{q}^{β_{i}} and N ∈ ⨄ Γ_{q}^{β}, there is the corresponding divergence rule where the i-th premise is diverging, i.e.,

P_{0} ⋯ P_{i−1} ρ_{i} ⊢_{β_{i}} N_{i} ⟶^{∞}

= (side condition)

ρ ⊢_{β} N ⟶^{∞}

Therefore, there are two rules above modeling the divergence of statement sequences, which can be obtained from rule (42). It is worth noting that a single divergence rule schema can be obtained from more than one of the concrete rules in Section 5.5.

We will use the terms negative and positive to distinguish the different kinds of rules constructed in this and the previous section, respectively.

Definition 5.5. (Concrete semantics rules.) The set R_{+} (resp., R_{−}) of positive (resp., negative) concrete semantics rules is the infinite set obtained by instantiating the rule schemata of Section 5.5 (resp., Section 5.6) in all possible ways (respecting, of course, the side conditions). Moreover, R =^{def} R_{+} ⊎ R_{−}.

5.7 Concrete Semantics Trees

The concrete semantics of a program is a (possibly infinite) set of finite or infinite trees. Such trees are defined in terms of the (infinite) set of instances of the rules defined in the previous two sections.

Let S be the (infinite) set of sequents occurring in the premises and conclusions of the rules in R. The concrete semantics universe, denoted by U, is the set of finitely branching trees of at most ω-depth with labels in S.

Definition 5.6. (Concrete semantics universe.) A set P ⊆ ℕ^{⋆} is prefixclosed if, for each z ∈ ℕ^{⋆} and each n ∈ ℕ, zn ∈ P implies z ∈ P. A set P ⊆ ℕ^{⋆} is canonical if, for each z ∈ ℕ^{⋆} there exists h ∈ ℕ such that

{ n ∈ ℕ | zn ∈ P } = {0, …, h − 1}.

An S-tree is a partial function θ: ℕ^{⋆} ↣ S such that dom(θ) is prefix-closed and canonical. The concrete semantics universe U is the set of all S-trees.

For each p ∈ dom(θ), the tree θ_{[p]} defined, for each z ∈ ℕ^{⋆}, by θ_{[p]}(z) =^{def} θ(pz), is called a subtree of θ; it is called a proper subtree if p ≠ ϵ. If dom(θ) = ∅, then θ is the empty tree. If θ is not empty, then θ(ϵ) is the root of θ and, if {0, …, h − 1} ⊆ dom(θ) and h ∉ dom(θ), then θ_{[0]}, …, θ_{[h−1]} are its immediate subtrees (note that h ∈ ℕ may be zero); in this case θ can be denoted by \frac{θ_{[0]} ··· θ_{[h−1]}}{θ(ϵ)} .

Definition 5.7. (Concrete semantics trees.) Let F_{+} : ℘(U) → ℘(U) be the continuous function over the complete lattice (℘(U), ⊆) given, for all U ∈ ℘(U), by

F_{+}(U) =^{def} \{ {θ_{0} ⋯ θ_{h−1} \atop s} | \begin{matrix}θ_{0}, …, θ_{h−1} ∈ U, \\ {θ_{0}(ϵ) ⋯ θ_{h−1}(ϵ) \atop s} ∈ R_{+} \end{matrix} \}.

The set of positive concrete semantics trees is Θ_{+} =^{def} lfp_{⊆}(F_{+}). Consider now the co-continuous function F_{−}: ℘(U) → ℘(U) given, for each U ∈ ℘(U), by

F_{−}(U) =^{def} \{ {θ_{0} ⋯ θ_{h−1} \atop s} | \begin{matrix}θ_{0}, …, θ_{h−2} ∈ Θ_{+}, θ_{h−1} ∈ U, \\ {θ_{0}(ϵ) ⋯ θ_{h−1}(ϵ) \atop s} ∈ R_{−} \end{matrix} \}.

The set of negative concrete semantics trees is Θ_{−} =^{def} gfp_{⊆}(F_{−}). The set of all

concrete semantics trees is Θ =^{def} Θ_{+} ⊎ Θ_{−}.

We now show that, for every concrete non-terminal configuration, there exists a concrete semantics tree with that in the root.

Proposition 5.8. For each β ∈ TEnv, ρ ∈ Env such that ρ : β and N ∈ Γ_{q}^{β}, where q ∈ {e, d, g, s, b, k}, there exists θ ∈ Θ such that

θ(ϵ) ∈ { (ρ ⊢_{β} N → η) | η ∈ T_{q} } ⊎ { (ρ ⊢_{β} N ⟶^{∞}) }.

Proof. If q = e and η ∈ T_{e}, we say that the sequent (ρ ⊢_{β} N → η) is well-typed if N = ⟨e, σ_{0}⟩ and η = ⟨sval, σ_{1}⟩ imply β ⊢ e : type(sval). For the proof, let

S_{+}(ρ, β, N) =^{def} { s | s = (ρ ⊢_{β} N → η), η ∈ T_{q}, (q = e ⟹ s is well-typed) }.

We now assume that N ∈ Γ_{q}^{β} is a fixed but arbitrary non-terminal configuration. It suffices to show there exists θ ∈ Θ such that θ(ϵ) ∈ S_{+}(ρ, β, N)⊎{ (ρ ⊢_{β} N ⟶^{∞}) }. Let R_{0} be the set of all rules in R_{+} whose conclusions are in S_{+}(ρ, β, N). By inspecting the concrete evaluation rule schemata in Section 5.5, R_{0} ≠ ∅. Let j ≥ 0 be the maximal value for which there exist finite trees θ_{0}, …, θ_{j−1} ∈ Θ_{+} where P_{0} = θ_{0}(ϵ), …, P_{j−1} = θ_{j−1}(ϵ) are the first j premises of a rule in R_{0}. Let R_{j} ⊆ R_{0} be the set of all rules in R_{0} with P_{0}, …, P_{j−1} as their first j premises; then R_{j} ≠ ∅. By inspecting the rule schemata in Section 5.5, it can be seen that, if there exists \frac{P_{0} ··· P_{j−1} P′_{j} ···}{s′} ∈ R_{j} for some P′_{j} ∈ S_{+}(ρ_{j}, β_{j}, N_{j}) and s′ ∈ S_{+}(ρ, β, N), then^{6}

∀P_{j} ∈ S_{+}(ρ_{j}, β_{j}, N_{j}) : ∃s ∈ S_{+}(ρ, β, N) . \frac{P_{0} ⋯ P_{j−1} P_{j} ⋯}{s} ∈ R_{j}. (76)

Suppose that q ∈ {e, d, g} so that we can also assume N = ⟨u, σ⟩. We show by structural induction on u that there exists θ ∈ Θ_{+} such that θ(ϵ) ∈ S_{+}(ρ, β, N). By inspecting the rule schemata in Section 5.5, it can be seen that, if u is atomic, the rules in R_{0} have no premises (so that j = 0) and hence, letting θ ∈ Θ_{+} be the singleton tree consisting of the conclusion of a rule in R_{0}, we obtain that θ(ϵ) ∈ S_{+}(ρ, β, N). Otherwise, u is not atomic, we show that each of the rules in R_{j} has exactly j premises; to do this, we assume there exists a rule in R_{j} with a (j + 1)-th premise P_{j} and derive a contradiction. Let N_{j} ∈ Γ_{q_{j}}^{β_{j}} be the non-terminal configuration in P_{j}. By inspecting the rule schemata in Section 5.5 in the case that q ∈ {e, d, g}, it can be seen that:

(i) q_{j} ∈ {e, d, g} so that N_{j} has the form ⟨u_{j}, σ_{j}⟩; (ii) u_{j} is a substructure of u unless R_{j} consists of instances of the schematic

rule (31) and j = 1.

If u_{j} is a substructure of u, by property (i), we can apply structural induction to obtain that there exists a finite tree θ_{j} ∈ Θ_{+} such that P_{j} = θ_{j}(ϵ) ∈ S_{+}(ρ_{j}, β_{j}, N_{j}); hence, by property (76), there exists a rule in R_{j} having P_{j} as its (j +1)-th premise; contradicting the assumption that j was maximal. Otherwise, by property (ii), if u_{j} is not a substructure of u, the rules in R_{0} must be instances of rule schema (31) and j = 1; in this case, rule schema (23), which has no premises, can be instantiated with the second premise of a rule in R_{j} as its conclusion; and again we have a contradiction. Thus, for any u_{j}, all rules in R_{j} have exactly j premises. By Definition 5.7, θ = \frac{θ_{0} ··· θ_{j−1}}{s} ∈ Θ_{+} for some s ∈ S_{+}(ρ, β, N). Therefore, since Θ_{+} ⊆ Θ, the thesis holds when q ∈ {e, d, g}.

Suppose now that q ∈ {s, b, k}. We prove that, if there does not exist a tree θ ∈ Θ_{+} such that θ(ϵ) ∈ S_{+}(ρ, β, N), then, for all n ≥ 0, there exists a tree θ such that θ(ϵ) = s_{∞} =^{def} (ρ ⊢_{β} N ⟶^{∞}) and θ ∈ F_{−}^{n}(U). To this end, we reason by induction on n ≥ 0. By our assumption that there is no tree θ ∈ Θ_{+} such that θ(ϵ) ∈ S_{+}(ρ, β, N), there must exist a rule

\frac{P_{0} ⋯ P_{j−1} P_{j} ⋯}{s} ∈ R_{j}

for some P_{j} ∈ S_{+}(ρ_{j}, β_{j}, N_{j}); let q_{j} be such that N_{j} ∈ Γ_{q_{j}}^{β_{j}}. By the maximality of j, there is no tree in Θ_{+} whose root is P_{j}. We have already shown that, if

6To help understand this property, we illustrate it in the case that q = e and the non-terminal configuration is N = ⟨b_{0} and b_{1}, σ⟩; hence the concrete rule schemata (15)–(17) will apply. In all the rule instances, the first premise is of the form P_{0} = (ρ ⊢_{β} N_{0} → η_{0}), where N_{0} = ⟨b_{0}, σ⟩; as a consequence, we have S_{+}(ρ, β, N_{0}) = { (ρ ⊢_{β} N_{0} → η_{0}) | η_{0} ∈ B }, where B =^{def} ExceptState ⊎ { ⟨t, σ_{0}⟩ ∈ T_{e} | t ∈ Bool, σ_{0} ∈ Mem }. Thus, for each terminal configuration η_{0} ∈ B, there is a rule instance having η_{0} in its first premise — that is we instantiate rule (15) when η_{0} = ε, rule (16) when η_{0} = ⟨ff, σ_{0}⟩ and rule (17) when η_{0} = ⟨tt, σ_{0}⟩. Thus property (76) holds for j = 0. Moreover, although only rule (17) applies when j = 1, the terminal configuration for the second premise (P_{1}) is just any terminal configuration in T_{e}. Thus property (76) also holds for j = 1.

q_{j} ∈ {e, d, g}, then there exists a tree θ_{j} ∈ Θ_{+} such that θ_{j}(ϵ) ∈ S_{+}(ρ_{j}, β_{j}, N_{j}); thus, by property (76), there must be a rule in R_{j} whose (j + 1)-th premise is θ_{j}(ϵ); contradicting the assumption that j ≥ 0 is maximal. Hence q_{j} ∈ {s, b, k}. By the definition of the negative concrete semantics rules in Section 5.6, there exists a corresponding negative rule

\frac{P_{0} ⋯ P_{j−1} P_{∞}}{s_{∞}} ∈ R_{−}

such that P_{∞} = (ρ_{j} ⊢_{β_{j}} N_{j} ⟶^{∞}). Hence, by Definition 5.6, there exists a tree in U = F_{−}^{0}(U) with root s_{∞}, so that the inductive hypothesis holds for n = 0. Suppose now that n > 0. By the inductive hypothesis, there exists a tree θ_{∞} ∈ F_{−}^{n−1}(U) such that θ_{∞}(ϵ) = P_{∞}. Hence, by Definition 5.7, \frac{θ_{0} ··· θ_{j−1} θ_{∞}}{s_{∞}} ∈ F_{−}^{n}(U). Thus, for all n ≥ 0, there exists a tree in F_{−}^{n}(U) with root s_{∞} and hence, by Definition 5.7, there exists a tree in Θ_{−} with root s_{∞}. Since Θ = Θ_{+} ⊎ Θ_{−}, the thesis holds when q ∈ {s, b, k}.

The concrete semantics of a valid program g with respect to the initial memory structure σ_{i} =^{def} (∅, ϵ) ∈ Mem is a set of concrete semantics trees. This set will always include a tree θ_{0} ∈ Θ (which, by Proposition 5.8, must exist) such that

θ_{0}(ϵ) = (∅ ⊢_{∅} ⟨(g; gvar \underline{x} : integer = 0), σ_{i}⟩ → η_{0}).

If η_{0} = ε_{0}, i.e., an RTS exception is thrown during the evaluation of g, then the concrete semantics is {θ_{0}}. If, instead, η_{0} = ⟨ρ_{0}, σ_{0}⟩, then the concrete semantics is

{θ_{0}} ∪ { θ ∈ Θ | θ(ϵ) = (ρ_{0} ⊢_{β} N → η) or θ(ϵ) = (ρ_{0} ⊢_{β} N ⟶^{∞}) },

where N = ⟨(\underline{x} := main(□)), σ_{0}⟩ ∈ Γ_{s}^{β} and ∅ ⊢_{∅} (g; gvar \underline{x} : integer = 0) : β.

The concrete semantics for CPM we have just presented, extended as indicated in Section 9, allows us to reason on a number of interesting program safety properties (such as the absence of division-by-zero and other run-time errors) as well as termination and computational complexity. In the next section, we will see how the usually non-computable concrete semantics can be given an abstract counterpart that is amenable to effective computation.

6. ABSTRACT DYNAMIC SEMANTICS

For the specification of the abstract semantics, we mainly follow the approach outlined in the works by Schmidt [Sch95; Sch97; Sch98]. The specification of the abstract semantics requires that appropriate abstract domains are chosen to provide correct approximations for the values that are involved in the concrete computation [CC77a; CC79; CC92a; CC92c]. For the sake of generality and extensibility, we will not target any specific abstraction, but rather consider arbitrary abstract domains that satisfy a limited set of properties that are sufficient to provide the correctness of the overall analysis without compromising its potential precision.

6.1 Abstract Semantic Domains

We adopt the framework proposed in [CC92a, Section 7], where the correspondence between the concrete and the abstract domains is induced from a concrete approximation relation and a concretization function. For the sole purpose of simplifying the presentation, we will consider a particular instance of the framework by assuming a few additional but non-essential domain properties. The resulting construction is adequate for our purposes and still allows for algebraically weak abstract domains, such as the domain of convex polyhedra [CH78].

A concrete domain is modeled as a complete lattice (C, ⊑, ⊥, ⊤, ⊓, ⊔) of semantic properties; as usual, the concrete approximation relation c_{1} ⊑ c_{2} holds if c_{1} is a stronger property than c_{2} (i.e., c_{2} approximates c_{1}). An abstract domain is modeled as a bounded join-semilattice (D^{♯}, ⊑^{♯}, ⊥^{♯}, ⊔^{♯}), so that it has a bottom element ⊥^{♯} and the least upper bound d_{1}^{♯} ⊔^{♯} d_{2}^{♯} exists for all d_{1}^{♯}, d_{2}^{♯} ∈ D^{♯}. When the abstract domain is also provided with a top element ⊤^{♯} ∈ D^{♯}, we will write (D^{♯}, ⊑^{♯}, ⊥^{♯}, ⊤^{♯}, ⊔^{♯}). The abstract domain D^{♯} is related to C by a monotonic concretization function γ: D^{♯} → C: in words, C is approximated by D^{♯} through γ; this approximation is said to be strict if γ is a strict function.^{7}

In order to compute approximations for specific concrete objects, we assume the existence of a partial abstraction function α: C ↣ D^{♯} such that, for each c ∈ C, if α(c) is defined then c ⊑ γ(α(c)). In particular, we assume that α(⊥) = ⊥^{♯} is always defined; if an abstract top element exists, then α(⊤) = ⊤^{♯} is also defined. When needed or useful, we will require a few additional properties.

Most of the concrete domains used in the concrete semantics construction are obtained as the powerset lattice (℘(D), ⊆, ∅, D, ∩, ∪) of some set of concrete objects D. In such a situation, for each concrete object d ∈ D and abstract element d^{♯} ∈ D^{♯} such that the corresponding domains are related by the concretization function γ: D^{♯} → ℘(D), we write d ∝ d^{♯} and d ∝̸ d^{♯} to denote the assertions d ∈ γ(d^{♯}) and d ∉ γ(d^{♯}), respectively. For a lighter notation, we denote ⊑^{♯}, ⊥^{♯}, ⊤^{♯} and ⊔^{♯} by ⊑, ⊥, ⊤ and ⊔, respectively. We also overload the symbols ⊑, ⊥, ⊤, ⊔, γ and α: the context will always make clear which incarnation has to be considered.

The approximations of composite concrete domains are typically obtained by suitably combining the approximations already available for their basic components. For i = 1, 2, let D_{i} be a set of concrete objects and consider the corresponding powerset lattice (℘(D_{i}), ⊆, ∅, D_{i}, ∩, ∪); let also D_{i}^{♯} be an abstract domain related to ℘(D_{i}) by the concretization function γ_{i}: D_{i}^{♯} → ℘(D_{i}).

6.1.1 Approximation of Cartesian Products. Values of the Cartesian product D_{1} × D_{2} can be approximated by elements of the Cartesian product D_{1}^{♯} × D_{2}^{♯}. Namely, the component-wise ordered abstract domain (D_{1}^{♯} × D_{2}^{♯}, ⊑, ⊥, ⊔) is related to the concrete powerset lattice (℘(D_{1}×D_{2}), ⊆, ∅, D_{1}×D_{2}, ∩, ∪) by the concretization function γ: (D_{1}^{♯} × D_{2}^{♯}) → ℘(D_{1} × D_{2}) defined, for each (d_{1}^{♯}, d_{2}^{♯}) ∈ D_{1}^{♯} × D_{2}^{♯}, by

γ(d_{1}^{♯}, d_{2}^{♯}) =^{def} { (d_{1}, d_{2}) ∈ D_{1} × D_{2} | d_{1} ∈ γ_{1}(d_{1}^{♯}), d_{2} ∈ γ_{2}(d_{2}^{♯}) }. (77)

Hence, (d_{1}, d_{2}) ∝ (d_{1}^{♯}, d_{2}^{♯}) holds if and only if d_{1} ∝ d_{1}^{♯} and d_{2} ∝ d_{2}^{♯}.

If the underlying approximations D_{1}^{♯} and D_{2}^{♯} are both strict, then a better approximation scheme can be obtained by adopting the strict product (also called

7Let f: D_{1} × ⋯ × D_{n} → D_{0}, where (D_{i}, ⊑_{i}, ⊥_{i}, ⊔_{i}) is a bounded join-semilattice, for each i = 0, …, n. Then, function f is strict on the i-th argument if d_{i} = ⊥_{i} implies f(d_{1}, …, d_{n}) = ⊥_{0}.

smash product) construction, which performs a simple form of reduction by collapsing (d_{1}^{♯}, d_{2}^{♯}) to the bottom element whenever d_{1}^{♯} = ⊥ or d_{2}^{♯} = ⊥. Namely,

D_{1}^{♯} ⊗ D_{2}^{♯} =^{def} { (d_{1}^{♯}, d_{2}^{♯}) ∈ D_{1}^{♯} × D_{2}^{♯} | d_{1}^{♯} = ⊥ if and only if d_{2}^{♯} = ⊥ }.

The concretization function is defined exactly as in (77). The constructor function · ⊗ ·: (D_{1}^{♯} × D_{2}^{♯}) → (D_{1}^{♯} ⊗ D_{2}^{♯}) is defined by

d_{1}^{♯} ⊗ d_{2}^{♯} =^{def} \begin{cases}(d_{1}^{♯}, d_{2}^{♯}), & if d_{1}^{♯} ≠ ⊥ and d_{2}^{♯} ≠ ⊥; \\ ⊥, & otherwise. \end{cases}

6.1.2 Approximation of Disjoint Unions. In order to provide an abstract domain approximating sets of concrete objects drawn from a disjoint union, we use the following well-known construction several times.

Suppose that D_{1}∩D_{2} = ∅. Then, values of the disjoint union D = D_{1}⊎D_{2} can be approximated by elements of the Cartesian product D^{♯} = D_{1}^{♯} ×D_{2}^{♯}. In this case, the abstract domain D^{♯} is related to the concrete powerset lattice (℘(D), ⊆, ∅, D, ∩, ∪) by means of the concretization function γ: (D_{1}^{♯} × D_{2}^{♯}) → ℘(D_{1} ⊎ D_{2}) defined, for each (d_{1}^{♯}, d_{2}^{♯}) ∈ D_{1}^{♯} × D_{2}^{♯}, by

γ(d_{1}^{♯}, d_{2}^{♯}) =^{def} γ_{1}(d_{1}^{♯}) ⊎ γ_{2}(d_{2}^{♯}).

Therefore, the approximation provided by D^{♯} is strict if both D_{1}^{♯} and D_{2}^{♯} are so. In order to simplify notation, if d_{1}^{♯} ∈ D_{1}^{♯} then we will sometimes write d_{1}^{♯} to also denote the abstract element (d_{1}^{♯}, ⊥) ∈ D^{♯}; similarly, d_{2}^{♯} ∈ D_{2}^{♯} also denotes the abstract element (⊥, d_{2}^{♯}) ∈ D^{♯}. As usual, for each i = 1, 2 and d_{i} ∈ D_{i}, the notation d_{i} ∝ (d_{1}^{♯}, d_{2}^{♯}) stands for the assertion d_{i} ∈ γ(d_{1}^{♯}, d_{2}^{♯}), which is equivalent to d_{i} ∈ γ_{i}(d_{i}^{♯}). For the sake of clarity, the abstract domain D^{♯} as specified above will be denoted by D_{1}^{♯} ⊎^{♯} D_{2}^{♯}. It is worth stressing that D_{1}^{♯} ⊎^{♯} D_{2}^{♯} ≠ D_{1}^{♯} ⊎ D_{2}^{♯}.

6.2 Approximation of Integers

The concrete domain of integers (℘(Integer), ⊆, ∅, Integer, ∩, ∪) is correctly approximated by an abstract domain (Integer^{♯}, ⊑, ⊥, ⊤, ⊔), where we assume that γ is strict. Elements of Integer^{♯} are denoted by m^{♯}, m_{0}^{♯}, m_{1}^{♯} and so forth. We assume that the partial abstraction function α: ℘(Integer) ↣ Integer^{♯} is defined on all singletons {m} ∈ ℘(Integer). We also assume that there are abstract binary operations ‘⊕’, ‘⊖’, ‘⊙’, ‘⊘’ and ‘⌽’ on Integer^{♯} that are strict on each argument and sound with respect to the corresponding operations on ℘(Integer) which, in turn, are the obvious pointwise extensions of addition, subtraction, multiplication, division and remainder over the integers. More formally, we require γ(m_{0}^{♯} ⊕ m_{1}^{♯}) ⊇ { m_{0} + m_{1} | m_{0} ∈ γ(m_{0}^{♯}), m_{1} ∈ γ(m_{1}^{♯}) } for each m_{0}^{♯}, m_{1}^{♯} ∈ Integer^{♯}, to ensure that ‘⊕’ is sound with respect to addition. Likewise for ‘⊖’ and ‘⊙’ with respect to subtraction and multiplication, respectively. For the ‘⊘’ operation we require soundness with respect to integer division i.e., that, for each m_{0}^{♯}, m_{1}^{♯} ∈ Integer^{♯}, γ(m_{0}^{♯} ⊘ m_{1}^{♯}) ⊇ { m_{0} ÷ m_{1} | m_{0} ∈ γ(m_{0}^{♯}), m_{1} ∈ γ(m_{1}^{♯}), m_{1} ≠ 0 }. Likewise for ‘⌽’ with respect to the ‘mod’ operation. We also assume there is a unary abstract operation, denoted by ‘⊖’, which is strict and sound with respect to the unary minus concrete operation, that is, γ(⊖m^{♯}) ⊇ { −m | m ∈ γ(m^{♯}) }.

6.3 Approximation of Booleans

We assume a complete lattice (Bool^{♯}, ⊑, ⊥, ⊤, ⊓, ⊔) is given that is related to the concrete domain of Booleans (℘(Bool), ⊆, ∅, Bool, ∩, ∪) by means of a Galois connection where γ is strict. Elements of Bool^{♯} are denoted by t^{♯}, t_{0}^{♯}, t_{1}^{♯} and so forth. We assume that there are abstract operations ‘⊝’, ‘ ’ and ‘ ’ on Bool^{♯} that are strict on each argument and sound with respect to the pointwise extensions of Boolean negation, disjunction and conjunction over ℘(Bool). For instance, for the operation ‘ ’ to be sound with respect to disjunction on ℘(Bool), it is required that, γ(t_{0}^{♯} t_{1}^{♯}) ⊇ { t_{0} ∨ t_{1} | t_{0} ∈ γ(t_{0}^{♯}), t_{1} ∈ γ(t_{1}^{♯}) } for each t_{0}^{♯} and t_{1}^{♯} in Bool^{♯}. Likewise for ‘ ’. For operation ‘⊝’ to be sound with respect to negation on ℘(Bool), we require that, for each t^{♯} in Bool^{♯}, γ(⊝ t^{♯}) ⊇ { ¬ t | t ∈ γ(t^{♯}) }.

Furthermore, we assume that there are abstract operations ‘≜’, ‘≜̸’, ‘◁’, ‘⊴’, ‘⊵’ and ‘▷’ on Integer^{♯} that are strict on each argument and sound with respect to the pointwise extensions over ℘(Integer) of the corresponding relational operators ‘=’, ‘≠’, ‘<’, ‘≤’, ‘≥’ and ‘>’ over the integers, considered as functions taking values in Bool. For instance, for the operation ‘≜’ to be sound with respect to equality on ℘(Integer), we require that γ(m_{0}^{♯} ≜ m_{1}^{♯}) ⊇ { m_{0} = m_{1} | m_{0} ∈ γ(m_{0}^{♯}), m_{1} ∈ γ(m_{1}^{♯}) } for each m_{0}^{♯}, m_{1}^{♯} ∈ Integer^{♯}. Likewise for ‘≜̸’, ‘◁’, ‘⊴’, ‘⊵’ and ‘▷’.

6.4 Approximation of Storable Values

The concrete domain of storable values (℘(sVal), ⊆, ∅, sVal, ∩, ∪), including both

integers and Booleans, is abstracted by the domain sVal^{♯} =^{def} Integer^{♯} ⊎^{♯} Bool^{♯}. The hypotheses on Integer^{♯} and Bool^{♯} imply that the approximation is strict.

6.5 Approximation of Exceptions

For the approximation of RTS exceptions, we assume that there is an abstract domain (RTSExcept^{♯}, ⊑, ⊥, ⊤, ⊔), which is related to the concrete powerset domain (℘(RTSExcept), ⊆, ∅, RTSExcept, ∩, ∪) by a strict concretization function. The partial abstraction function α: ℘(RTSExcept) ↣ RTSExcept^{♯} is assumed to be defined on all singletons. Elements of RTSExcept^{♯} are denoted by χ^{♯}, χ_{0}^{♯}, χ_{1}^{♯} and so forth.

Generic exceptions, including both RTS exceptions and user-defined exceptions, are approximated by elements of the domain Except^{♯} =^{def} RTSExcept^{♯} ⊎^{♯} sVal^{♯}. The hypotheses on its components imply that the approximation is strict. Elements of Except^{♯} are denoted by ξ^{♯}, ξ_{0}^{♯}, ξ_{1}^{♯} and so forth.

6.6 Approximation of Memory Structures, Value States and Exception States

Here we differ from other published abstract semantics in that we explicitly cater for relational abstract domains as well as for attribute-independent ones [CC79]. While this complicates the presentation, it results in a truly generic abstract semantics. Moreover, the approach presented here is —all things considered— quite simple and reflects into a modular, clean design of the analyzer.

Definition 6.1. (Mem^{♯}, ValState^{♯}, ExceptState^{♯}.) We assume there exists an abstract domain (Mem^{♯}, ⊑, ⊥, ⊔) that is related, by means of a strict concretization function, to the concrete powerset domain (℘(Mem), ⊆, ∅, Mem, ∩, ∪). Elements of Mem^{♯} are denoted by σ^{♯}, σ_{0}^{♯}, σ_{1}^{♯} and so forth. We assume that, for each σ ∈ Mem, there exists σ^{♯} ∈ Mem^{♯} such that σ ∝ σ^{♯}.

The abstract domain of value states is ValState^{♯} =^{def} sVal^{♯} ⊗ Mem^{♯}. Elements of ValState^{♯} will be denoted by υ^{♯}, υ_{0}^{♯}, υ_{1}^{♯} and so forth.

The abstract domain of exception states is ExceptState^{♯} =^{def} Mem^{♯} ⊗ Except^{♯}. Elements of ExceptState^{♯} will be denoted by ε^{♯}, ε_{0}^{♯}, ε_{1}^{♯} and so forth. To improve readability, none^{♯} will denote the bottom element ⊥ ∈ ExceptState^{♯}, indicating that no exception is possible.

The abstract memory structure read and update operators

·[·, ·]: (Mem^{♯} × Addr × sType) → (ValState^{♯} ⊎^{♯} ExceptState^{♯}),

·[· :=^{♯} ·]: (Mem^{♯} × (Addr × sType) × sVal^{♯}) → (Mem^{♯} ⊎^{♯} ExceptState^{♯})

are assumed to be such that, for each σ^{♯} ∈ Mem^{♯}, a ∈ Addr, sT ∈ sType and sval^{♯} ∈ sVal^{♯}:

γ(σ^{♯}[a, sT]) ⊇ { σ[a, sT] | σ ∈ γ(σ^{♯}) },
γ(σ^{♯}[(a, sT) :=^{♯} sval^{♯}]) ⊇ { σ[(a, sT) := sval] | σ ∈ γ(σ^{♯}), sval ∈ γ(sval^{♯}) }.

The abstract data and stack memory allocation functions

new_{d}^{♯}: ValState^{♯} → ((Mem^{♯} × Loc) ⊎^{♯} ExceptState^{♯}),
new_{s}^{♯}: ValState^{♯} → ((Mem^{♯} × Ind) ⊎^{♯} ExceptState^{♯})

are assumed to be such that, for each υ ∈ ValState and υ^{♯} ∈ ValState^{♯} such that υ ∈ γ(υ^{♯}), and each h ∈ {d, s}: if new_{h}(υ) = (σ, a) (resp., new_{h}(υ) = ε) and new_{h}^{♯}(υ^{♯}) = ((σ^{♯}, a′), ε^{♯}), then σ ∈ γ(σ^{♯}) and a = a′ (resp., ε ∈ γ(ε^{♯})).

The abstract memory structure data cleanup function

cleanup_{d}^{♯}: ExceptState^{♯} → ExceptState^{♯}

is such that, for each ε^{♯} ∈ ExceptState^{♯}, we have

γ(cleanup_{d}^{♯}(ε^{♯})) ⊇ { cleanup_{d}(ε) | ε ∈ γ(ε^{♯}) }.

The abstract functions

{mark_{s}^{♯}, unmark_{s}^{♯}, link_{s}^{♯}, unlink_{s}^{♯}} ⊆ Mem^{♯} → Mem^{♯}

are defined to be such that, for each σ^{♯} ∈ Mem^{♯}:

γ(mark_{s}^{♯}(σ^{♯})) ⊇ { mark_{s}(σ) | σ ∈ γ(σ^{♯}) },
γ(unmark_{s}^{♯}(σ^{♯})) ⊇ { unmark_{s}(σ) | σ ∈ γ(σ^{♯}) and unmark_{s}(σ) is defined },
γ(link_{s}^{♯}(σ^{♯})) ⊇ { link_{s}(σ) | σ ∈ γ(σ^{♯}) and link_{s}(σ) is defined },
γ(unlink_{s}^{♯}(σ^{♯})) ⊇ { unlink_{s}(σ) | σ ∈ γ(σ^{♯}) and unlink_{s}(σ) is defined }.

It is assumed that all the abstract operators mentioned above are strict on each of their arguments taken from an abstract domain.

As done in the concrete, the abstract stack unmark and the abstract frame unlink functions are lifted to also work on abstract exception states. Namely, for each ε^{♯} = (σ^{♯}, ξ^{♯}) ∈ ExceptState^{♯},

unmark_{s}^{♯}(σ^{♯}, ξ^{♯}) =^{def} (unmark_{s}^{♯}(σ^{♯}), ξ^{♯}),
unlink_{s}^{♯}(σ^{♯}, ξ^{♯}) =^{def} (unlink_{s}^{♯}(σ^{♯}), ξ^{♯}).

Besides the abstract operators specified above, which closely mimic the concrete operators related to concrete memory structures and exception states, other abstract operators will be used in the abstract semantics construction so as to enhance its precision.

When dealing with Boolean guards during the abstract evaluation of conditional and iteration statements, it might be the case that no definite information is available. In such a situation, the abstract execution can be made more precise if the abstract memory structure is filtered according to the condition holding in the considered computation branch.

Definition 6.2. (Memory structure filter.) An abstract memory structure filter is any computable function ϕ: (Env × Mem^{♯} × Exp) → Mem^{♯} such that, for each e ∈ Exp, each β : I with FI(e) ⊆ I and β ⊢_{I} e : boolean, for each ρ ∈ Env with ρ : β and each σ^{♯} ∈ Mem^{♯}, if ϕ(ρ, σ^{♯}, e) = σ_{tt}^{♯}, then

γ(σ_{tt}^{♯}) ⊇ { σ_{tt} ∈ Mem | σ ∈ γ(σ^{♯}), ρ ⊢_{β} ⟨e, σ⟩ → ⟨tt, σ_{tt}⟩ }.

Similarly, abstract exception states can be filtered according to whether or not they can be caught by the guard of a catch clause.

Definition 6.3. (Exception state filters and selectors.) The abstract exception state filters are computable functions

ϕ^{+}, ϕ^{−}: (exceptDecl × ExceptState^{♯}) → ExceptState^{♯}

such that, for each p ∈ exceptDecl and each ε^{♯} ∈ ExceptState^{♯},

γ(ϕ^{+}(p, ε^{♯})) ⊇ \begin{cases}γ(ε^{♯}), & if p = any; \\ \{ (σ, ξ) ∈ γ(ε^{♯}) | ξ = p \}, & if p ∈ RTSExcept; \\ \{ (σ, ξ) ∈ γ(ε^{♯}) | ξ ∈ dom(type(p)) \}, & otherwise; \end{cases}

γ(ϕ^{−}(p, ε^{♯})) ⊇ \begin{cases}∅, & if p = any; \\ \{ (σ, ξ) ∈ γ(ε^{♯}) | ξ ≠ p \}, & if p ∈ RTSExcept; \\ \{ (σ, ξ) ∈ γ(ε^{♯}) | ξ ∉ dom(type(p)) \}, & otherwise. \end{cases}

The abstract memory structure and abstract exception selectors

mem: ExceptState^{♯} → Mem^{♯},
sel: (cType × ExceptState^{♯}) → (RTSExcept^{♯} ⊎ Integer^{♯} ⊎ Bool^{♯})

are defined, for each ε^{♯} = (σ^{♯}, (χ^{♯}, (m^{♯}, t^{♯}))) ∈ ExceptState^{♯} and cT ∈ cType, by

mem(ε^{♯}) =^{def} σ^{♯};

sel(cT, ε^{♯}) =^{def} \begin{cases}χ^{♯}, & if cT = rts exception; \\ m^{♯}, & if cT = integer; \\ t^{♯}, & if cT = boolean. \end{cases}

To simplify notation, we will write cT(ε^{♯}) to denote sel(cT, ε^{♯}).

The generic specification provided above for abstract memory structures and the corresponding abstract operators plays a central role for the modularity of the overall construction. By exploiting this “black box” approach, we achieve orthogonality not only from the specific abstract domains used to approximate (sets of tuples of) storable values, but also from the critical design decisions that have to be taken when approximating the concrete stack, which may be unbounded in size due to recursive functions. Hence, while still staying in the boundaries of the current framework, we can flexibly explore, combine, and finely tune the sophisticated proposals that have been put forward in the literature, such as the work in [JS03; JS04], which encompasses both the functional and the call string approaches to interprocedural analysis [CC77b; SP81].

6.7 Abstract Configurations

Terminal and non-terminal configurations of the abstract transition system are now defined.

Definition 6.4. (Non-terminal abstract configurations.) The sets of nonterminal abstract configurations for expressions, local and global declarations, statements, function bodies and catch clauses are given, for each β ∈ TEnv_{I} and respectively, by

Γ_{e}^{β♯} =^{def} { ⟨e, σ^{♯}⟩ ∈ Exp × Mem^{♯} | ∃sT ∈ sType . β ⊢_{I} e : sT },
Γ_{d}^{β♯} =^{def} { ⟨d, σ^{♯}⟩ ∈ Decl × Mem^{♯} | ∃δ ∈ TEnv . β ⊢_{I} d : δ },
Γ_{g}^{β♯} =^{def} { ⟨g, σ^{♯}⟩ ∈ Glob × Mem^{♯} | ∃δ ∈ TEnv . β ⊢_{I} g : δ },
Γ_{s}^{β♯} =^{def} { ⟨s, σ^{♯}⟩ ∈ Stmt × Mem^{♯} | β ⊢_{I} s },
Γ_{b}^{β♯} =^{def} { ⟨body, σ^{♯}⟩ ∈ Body × Mem^{♯} | ∃sT ∈ sType . β ⊢_{I} body : sT },
Γ_{k}^{β♯} =^{def} { ⟨k, ε^{♯}⟩ ∈ Catch × ExceptState^{♯} | β ⊢_{I} k }.

We write N^{♯} to denote a non-terminal abstract configuration.

The approximation relation between concrete and abstract non-terminal configurations is defined as follows. For each q ∈ {e, d, g, s, b}, N = ⟨q_{1}, σ⟩ ∈ Γ_{q}^{β} and N^{♯} = ⟨q_{2}, σ^{♯}⟩ ∈ Γ_{q}^{β♯},

N ∝ N^{♯} ⟺ (q_{1} = q_{2} ∧ σ ∝ σ^{♯}).  (78)

For each N = ⟨k_{1}, ε⟩ ∈ Γ_{k}^{β} and N^{♯} = ⟨k_{2}, ε^{♯}⟩ ∈ Γ_{k}^{β♯},

N ∝ N^{♯} ⟺ (k_{1} = k_{2} ∧ ε ∝ ε^{♯}).  (79)

Definition 6.5. (Terminal abstract configurations.) The sets of terminal abstract configurations for expressions, local and global declarations, statements, function bodies and catch clauses are given, respectively, by

T_{e}^{♯} =^{def} ValState^{♯} ⊎^{♯} ExceptState^{♯},
T_{d}^{♯} =^{def} T_{g}^{♯} =^{def} (Env × Mem^{♯}) ⊎^{♯} ExceptState^{♯},

T_{s}^{♯} =^{def} T_{b}^{♯} =^{def} Mem^{♯} ⊎^{♯} ExceptState^{♯},
T_{k}^{♯} =^{def} T_{s}^{♯} ⊎^{♯} ExceptState^{♯}.

We write η^{♯} to denote a terminal abstract configuration.

The approximation relation η ∝ η^{♯} between concrete and abstract terminal configurations is defined as follows. For expressions,

η ∝ ⟨υ^{♯}, ε^{♯}⟩ ⟺ \begin{cases}υ ∝ υ^{♯}, & if η = υ; \\ ε ∝ ε^{♯}, & if η = ε. \end{cases}  (80)

For local and global declarations,

η ∝ ⟨(ρ_{2}, σ^{♯}), ε^{♯}⟩ ⟺ \begin{cases}(ρ_{1} = ρ_{2} ∧ σ ∝ σ^{♯}), & if η = ⟨ρ_{1}, σ⟩; \\ ε ∝ ε^{♯}, & if η = ε. \end{cases}  (81)

For statements and function bodies,

η ∝ ⟨σ^{♯}, ε^{♯}⟩ ⟺ \begin{cases}σ ∝ σ^{♯}, & if η = σ; \\ ε ∝ ε^{♯}, & if η = ε. \end{cases}  (82)

For catch sequences,

η ∝ ⟨η_{s}^{♯}, ε^{♯}⟩ ⟺ \begin{cases}η_{s} ∝ η_{s}^{♯}, & if η = ⟨caught, η_{s}⟩; \\ ε ∝ ε^{♯}, & if η = ⟨uncaught, ε⟩. \end{cases}  (83)

The approximation relation for sequents is trivially obtained from the approximation relations defined above for configurations.

Definition 6.6. (‘∝’ on sequents.) The approximation relation between concrete (positive and negative) sequents and abstract sequents is defined, for each β ∈ TEnv_{I}, for each ρ_{0}, ρ_{1} ∈ Env_{J} such that ρ_{0} : β |_{J} and ρ_{1} : β |_{J}, for each q ∈ {e, d, g, s, b, k}, N ∈ Γ_{q}^{β}, η ∈ T_{q}, N^{♯} ∈ Γ_{q}^{β♯} and η^{♯} ∈ T_{q}^{♯}, by

(ρ_{0} ⊢_{β} N → η) ∝ (ρ_{1} ⊢_{β} N^{♯} → η^{♯}) ⟺ (ρ_{0} = ρ_{1} ∧ N ∝ N^{♯} ∧ η ∝ η^{♯}); (84)
(ρ_{0} ⊢_{β} N ⟶^{∞}) ∝ (ρ_{1} ⊢_{β} N^{♯} → η^{♯}) ⟺ (ρ_{0} = ρ_{1} ∧ N ∝ N^{♯}).  (85)

6.8 Supported Expressions, Declarations and Statements

Each abstract domain has to provide a relation saying which (abstract configuration for) expressions, declarations and statements it directly supports, as well as an abstract evaluation function providing safe approximations of any supported expressions, declarations and statements.

Definition 6.7. (supported^{♯}, eval^{♯}.) For each q ∈ {e, d, g, s}, we assume there exists a computable relation and a partial and computable operation,

supported^{♯} ⊆ Env × Γ_{q}^{β♯}  and  eval^{♯}: (Env × Γ_{q}^{β♯}) ↣ T_{q}^{♯},

such that whenever ρ : β and supported^{♯}(ρ, N^{♯}) holds, eval^{♯}(ρ, N^{♯}) is defined and has value η^{♯} ∈ T_{q}^{♯} and, for each N ∈ Γ_{q}^{β} and each η ∈ T_{q} such that N ∝ N^{♯} and ρ ⊢_{β} N → η, we have η ∝ η^{♯}.

An appropriate use of ‘supported^{♯}’ and ‘eval^{♯}’ allows the design of the domain of abstract memory structures to be decoupled from the design of the analyzer. In particular, it enables the use of relational as well as non-relational domains. For example, using the domain of convex polyhedra the proper way, one can easily implement a safe evaluation function for (the non-terminal abstract configuration of) any affine expression e. As a consequence, one can specify the support relation so that supported^{♯}(ρ, ⟨e, σ^{♯}⟩) holds. Similarly, one can specify supported^{♯}(ρ, ⟨id := e, σ^{♯}⟩) holds for any affine assignment, i.e., an assignment where e is an affine expression. Other implementation choices are possible. For instance, besides supporting affine expressions, the implementer could specify that supported^{♯}(ρ, ⟨id_{1} ∗ id_{2}, σ^{♯}⟩) holds provided ρ : I, id_{1}, id_{2} ∈ I and, for at least one i ∈ {1, 2}, γ(σ^{♯}[ρ(id_{i})]) = {m}, for some integer value m. Similarly, the design can impose that supported^{♯}(ρ, ⟨id ∗ id, σ^{♯}⟩) always holds.

6.9 Abstract Evaluation Relations

The abstract evaluation relations that provide the first part of the specification of the abstract interpreter for CPM are now defined. These relations are of the form

ρ ⊢_{β} N^{♯} → η^{♯},

where β ∈ TEnv, ρ : β and, for some q ∈ {e, d, g, s, b, k}, N^{♯} ∈ Γ_{q}^{β♯} and η^{♯} ∈ T_{q}^{♯}. The definition is again by structural induction from a set of rule schemata. In order to allow for the arbitrary weakening of the abstract descriptions in the conclusion, without having to introduce precondition strengthening and postcondition weakening rules, and to save typing at the same time, we will use the notation

P_{0} ⋯ P_{ℓ−1}

(side condition)

ρ ⊢_{β} N^{♯} ⇝ η_{0}^{♯}

to denote

P_{0} ⋯ P_{ℓ−1}
(side condition) and η_{0}^{♯} ⊑ η^{♯}
ρ ⊢_{β} N^{♯} → η^{♯}

where ‘⊑’ is the natural ordering relation on the appropriate abstract lattice (i.e., one of the T_{q}^{♯}, for q ∈ {e, d, g, s, b, k}.

Recalling the shorthand notation introduced in Section 6.1.2, when an abstract storable value sval^{♯} is expected and we write an abstract integer m^{♯} or an abstract Boolean t^{♯}, then we are actually meaning the abstract storable value (m^{♯}, ⊥) or (⊥, t^{♯}), respectively; similarly, when an abstract exception ξ^{♯} is expected and we write an abstract RTS exception χ^{♯} or an abstract storable value sval^{♯}, then we are actually meaning the abstract exceptions (χ^{♯}, ⊥) or (⊥, sval^{♯}), respectively.

6.9.1 Unsupported Expressions. The following rules for the abstract evaluation of expressions apply only if supported^{♯}(ρ, ⟨e, σ^{♯}⟩) does not hold, where e is the expression being evaluated. This side condition will be left implicit in order not to clutter the presentation.

Constant.

ρ ⊢_{β} ⟨con, σ^{♯}⟩ ⇝ ⟨α({con}) ⊗ σ^{♯}, none^{♯}⟩  (86)

Identifier.

ρ ⊢_{β} ⟨id, σ^{♯}⟩ ⇝ σ^{♯}[ρ(id)]  (87)

Unary minus.

ρ ⊢_{β} ⟨e, σ^{♯}⟩ → ⟨(m^{♯}, σ_{0}^{♯}), ε^{♯}⟩ ; ρ ⊢_{β} ⟨−e, σ^{♯}⟩ ⇝ ⟨(⊖ m^{♯}, σ_{0}^{♯}), ε^{♯}⟩  (88)

Binary arithmetic operations. Let ⧇ ∈ {+, −, ∗, /, %} be a syntactic operator and ⊚ ∈ {⊕, ⊖, ⊙, ⊘, ⌽} denote the corresponding abstract operation. Then the abstract rules for addition, subtraction, multiplication, division and remainder are given by the following schemata:

ρ ⊢_{β} ⟨e_{0}, σ^{♯}⟩ → ⟨(m_{0}^{♯}, σ_{0}^{♯}), ε_{0}^{♯}⟩ ρ ⊢_{β} ⟨e_{1}, σ_{0}^{♯}⟩ → ⟨(m_{1}^{♯}, σ_{1}^{♯}), ε_{1}^{♯}⟩ ; ρ ⊢_{β} ⟨e_{0} ⧇ e_{1}, σ^{♯}⟩ ⇝ ⟨(m_{0}^{♯} ⊚ m_{1}^{♯}, σ_{1}^{♯}), ε_{0}^{♯} ⊔ ε_{1}^{♯}⟩  (89)

if ⧇ ∉ {/, %} or 0 ∝̸ m_{1}^{♯}.

ρ ⊢_{β} ⟨e_{0}, σ^{♯}⟩ → ⟨(m_{0}^{♯}, σ_{0}^{♯}), ε_{0}^{♯}⟩ ρ ⊢_{β} ⟨e_{1}, σ_{0}^{♯}⟩ → ⟨(m_{1}^{♯}, σ_{1}^{♯}), ε_{1}^{♯}⟩ ; ρ ⊢_{β} ⟨e_{0} ⧇ e_{1}, σ^{♯}⟩ ⇝ ⟨(m_{0}^{♯} ⊚ m_{1}^{♯}, σ_{1}^{♯}), ε_{0}^{♯} ⊔ ε_{1}^{♯} ⊔ ε_{2}^{♯}⟩  (90)

if ⧇ ∈ {/, %}, 0 ∝ m_{1}^{♯} and ε_{2}^{♯} = σ_{1}^{♯} ⊗ α({divbyzero}).

Arithmetic tests. Let ⧆ ∈ {=, ≠, <, ≤, ≥, >} be an abstract syntax operator and let ▷◁: (Integer^{♯} × Integer^{♯}) → Bool^{♯} denote the corresponding abstract test operation in {≜, ≜̸, ◁, ⊴, ⊵, ▷}. Then the rules for the abstract arithmetic tests are given by

ρ ⊢_{β} ⟨e_{0}, σ^{♯}⟩ → ⟨(m_{0}^{♯}, σ_{0}^{♯}), ε_{0}^{♯}⟩ ρ ⊢_{β} ⟨e_{1}, σ_{0}^{♯}⟩ → ⟨(m_{1}^{♯}, σ_{1}^{♯}), ε_{1}^{♯}⟩ ; ρ ⊢_{β} ⟨e_{0} ⧆ e_{1}, σ^{♯}⟩ ⇝ ⟨(m_{0}^{♯} ▷◁ m_{1}^{♯}, σ_{1}^{♯}), ε_{0}^{♯} ⊔ ε_{1}^{♯}⟩  (91)

Negation.

ρ ⊢_{β} ⟨b, σ^{♯}⟩ → ⟨(t^{♯}, σ_{0}^{♯}), ε^{♯}⟩ ; ρ ⊢_{β} ⟨not b, σ^{♯}⟩ ⇝ ⟨(⊝ t^{♯}, σ_{0}^{♯}), ε^{♯}⟩  (92)

Conjunction.

ρ ⊢_{β} ⟨b_{0}, σ^{♯}⟩ → ⟨υ_{0}^{♯}, ε_{0}^{♯}⟩ ρ ⊢_{β} ⟨b_{1}, σ_{tt}^{♯}⟩ → ⟨υ_{1}^{♯}, ε_{1}^{♯}⟩ ; ρ ⊢_{β} ⟨b_{0} and b_{1}, σ^{♯}⟩ ⇝ ⟨υ_{ff}^{♯} ⊔ υ_{1}^{♯}, ε_{0}^{♯} ⊔ ε_{1}^{♯}⟩,  (93)

if σ_{tt}^{♯} = ϕ(ρ, σ^{♯}, b_{0}), σ_{ff}^{♯} = ϕ(ρ, σ^{♯}, not b_{0}) and υ_{ff}^{♯} = α({ff}) ⊗ σ_{ff}^{♯}.

Disjunction.

{ρ ⊢_{β} ⟨b_{0}, σ^{♯}⟩ → ⟨υ_{0}^{♯}, ε_{0}^{♯}⟩ ρ ⊢_{β} ⟨b_{1}, σ_{ff}^{♯}⟩ → ⟨υ_{1}^{♯}, ε_{1}^{♯}⟩ \atop ρ ⊢_{β} ⟨b_{0} or b_{1}, σ^{♯}⟩ ⇝ ⟨υ_{tt}^{♯} ⊔ υ_{1}^{♯}, ε_{0}^{♯} ⊔ ε_{1}^{♯}⟩}  (94)

if σ_{tt}^{♯} = ϕ(ρ, σ^{♯}, b_{0}), σ_{ff}^{♯} = ϕ(ρ, σ^{♯}, not b_{0}) and υ_{tt}^{♯} = α({tt}) ⊗ σ_{tt}^{♯}.

6.9.2 Unsupported Declarations. The following rules only apply if the condition supported^{♯}(ρ, ⟨q, σ^{♯}⟩) does not hold, where q ∈ Decl ⊎ Glob is the declaration being evaluated. Again, this side condition is left implicit.

Nil.

ρ ⊢_{β} ⟨nil, σ^{♯}⟩ ⇝ ⟨(∅, σ^{♯}), none^{♯}⟩  (95)

Environment.

ρ ⊢_{β} ⟨ρ_{0}, σ^{♯}⟩ ⇝ ⟨(ρ_{0}, σ^{♯}), none^{♯}⟩  (96)

Recursive environment.

ρ ⊢_{β} ⟨rec ρ_{0}, σ^{♯}⟩ ⇝ ⟨(ρ_{1}, σ^{♯}), none^{♯}⟩  (97)

if ρ_{1} = { id ↦ ρ_{0}(id) | ρ_{0}(id) = (λ fps . extern, sT) }

∪ \{ id ↦ abs_{1} | \begin{matrix}∀i ∈ \{0, 1\} : abs_{i} = (λ fps . let d_{i} in s result e, sT), \\ ρ_{0}(id) = abs_{0}, d_{1} = rec(ρ_{0} \ DI(fps)); d_{0} \end{matrix} \}.

Global variable declaration.

ρ ⊢_{β} ⟨e, σ^{♯}⟩ → ⟨υ^{♯}, ε_{0}^{♯}⟩

ρ ⊢_{β} ⟨gvar id : sT = e, σ^{♯}⟩ ⇝ ⟨(ρ_{1}, σ_{1}^{♯}), cleanup_{d}^{♯}(ε_{0}^{♯} ⊔ ε_{1}^{♯})⟩

(98)

if new_{d}^{♯}(υ^{♯}) = ((σ_{1}^{♯}, l), ε_{1}^{♯}) and ρ_{1} = {id ↦ (l, sT)}.

Local variable declaration.

ρ ⊢_{β} ⟨e, σ^{♯}⟩ → ⟨υ^{♯}, ε_{0}^{♯}⟩

ρ ⊢_{β} ⟨lvar id : sT = e, σ^{♯}⟩ ⇝ ⟨(ρ_{1}, σ_{1}^{♯}), unmark_{s}^{♯}(ε_{0}^{♯} ⊔ ε_{1}^{♯})⟩

(99)

if new_{s}^{♯}(υ^{♯}) = ((σ_{1}^{♯}, i), ε_{1}^{♯}) and ρ_{1} = {id ↦ (i, sT)}.

Function declaration.

ρ ⊢_{β} ⟨function id(fps) : sT = body_{0}, σ^{♯}⟩ ⇝ ⟨(ρ_{0}, σ^{♯}), none^{♯}⟩  (100)

if ρ_{0} = {id ↦ (λ fps . body_{1}, sT)} and either body_{0} = body_{1} = extern or, for each i ∈ {0, 1}, body_{i} = let d_{i} in s result e, I = FI(body_{0}) \ DI(fps) and d_{1} = ρ |_{I}; d_{0}.

Recursive declaration.

(ρ \ J) ⊢_{β[β_{1}]} ⟨g, σ^{♯}⟩ → ⟨(ρ_{0}, σ_{0}^{♯}), none^{♯}⟩ ρ ⊢_{β} ⟨rec ρ_{0}, σ_{0}^{♯}⟩ → η^{♯}

ρ ⊢_{β} ⟨rec g, σ^{♯}⟩ ⇝ η^{♯}

(101)

if J = FI(g) ∩ DI(g), β ⊢_{FI(g)} g : β_{0} and β_{1} = β_{0} |_{J}.

Global sequential composition.

ρ ⊢_{β} ⟨g_{0}, σ^{♯}⟩ → ⟨(ρ_{0}, σ_{0}^{♯}), ε_{0}^{♯}⟩ ρ[ρ_{0}] ⊢_{β[β_{0}]} ⟨g_{1}, σ_{0}^{♯}⟩ → ⟨(ρ_{1}, σ_{1}^{♯}), ε_{1}^{♯}⟩ ; ρ ⊢_{β} ⟨g_{0}; g_{1}, σ^{♯}⟩ ⇝ ⟨(ρ_{0}[ρ_{1}], σ_{1}^{♯}), ε_{0}^{♯} ⊔ ε_{1}^{♯}⟩  (102)

if β ⊢_{I} g_{0} : β_{0} and FI(g_{0}) ⊆ I.

Local sequential composition.

ρ ⊢_{β} ⟨d_{0}, σ^{♯}⟩ → ⟨(ρ_{0}, σ_{0}^{♯}), ε_{0}^{♯}⟩ ρ[ρ_{0}] ⊢_{β[β_{0}]} ⟨d_{1}, σ_{0}^{♯}⟩ → ⟨(ρ_{1}, σ_{1}^{♯}), ε_{1}^{♯}⟩ ; ρ ⊢_{β} ⟨d_{0}; d_{1}, σ^{♯}⟩ ⇝ ⟨(ρ_{0}[ρ_{1}], σ_{1}^{♯}), ε_{0}^{♯} ⊔ ε_{1}^{♯}⟩  (103)

if β ⊢_{I} d_{0} : β_{0} and FI(d_{0}) ⊆ I.

6.9.3 Unsupported Statements. The following rules only apply if the implicit side condition supported^{♯}(ρ, ⟨s, σ^{♯}⟩) does not hold, where s is the statement being evaluated.

Nop.

ρ ⊢_{β} ⟨nop, σ^{♯}⟩ ⇝ σ^{♯}  (104)

Assignment.

ρ ⊢_{β} ⟨e, σ^{♯}⟩ → ⟨(sval^{♯}, σ_{0}^{♯}), ε_{0}^{♯}⟩

if σ_{0}^{♯}[ρ(id) :=^{♯} sval^{♯}] = (σ_{1}^{♯}, ε_{1}^{♯})

ρ ⊢_{β} ⟨id := e, σ^{♯}⟩ ⇝ ⟨σ_{1}^{♯}, ε_{0}^{♯} ⊔ ε_{1}^{♯}⟩

(105)

Statement sequence.

ρ ⊢_{β} ⟨s_{0}, σ^{♯}⟩ → ⟨σ_{0}^{♯}, ε_{0}^{♯}⟩ ρ ⊢_{β} ⟨s_{1}, σ_{0}^{♯}⟩ → ⟨σ_{1}^{♯}, ε_{1}^{♯}⟩ ; ρ ⊢_{β} ⟨s_{0}; s_{1}, σ^{♯}⟩ ⇝ ⟨σ_{1}^{♯}, ε_{0}^{♯} ⊔ ε_{1}^{♯}⟩  (106)

Block. ρ ⊢_{β} ⟨d, mark_{s}^{♯}(σ^{♯})⟩ → ⟨(ρ_{0}, σ_{0}^{♯}), ε_{0}^{♯}⟩ ρ[ρ_{0}] ⊢_{β[β_{0}]} ⟨s, σ_{0}^{♯}⟩ → ⟨σ_{1}^{♯}, ε_{1}^{♯}⟩

ρ ⊢_{β} ⟨d; s, σ^{♯}⟩ ⇝ ⟨unmark_{s}^{♯}(σ_{1}^{♯}), ε_{0}^{♯} ⊔ unmark_{s}^{♯}(ε_{1}^{♯})⟩

(107)

if β ⊢_{FI(d)} d : β_{0}.

Conditional.

\begin{aligned}ρ ⊢_{β} ⟨e, σ^{♯}⟩ → ⟨υ_{0}^{♯}, ε_{0}^{♯}⟩ & ρ ⊢_{β} ⟨s_{0}, σ_{tt}^{♯}⟩ → ⟨σ_{1}^{♯}, ε_{1}^{♯}⟩ \\ & ρ ⊢_{β} ⟨s_{1}, σ_{ff}^{♯}⟩ → ⟨σ_{2}^{♯}, ε_{2}^{♯}⟩ \end{aligned}

ρ ⊢_{β} ⟨if e then s_{0} else s_{1}, σ^{♯}⟩ ⇝ ⟨σ_{1}^{♯} ⊔ σ_{2}^{♯}, ε_{0}^{♯} ⊔ ε_{1}^{♯} ⊔ ε_{2}^{♯}⟩

(108)

if σ_{tt}^{♯} = ϕ(ρ, σ^{♯}, e) and σ_{ff}^{♯} = ϕ(ρ, σ^{♯}, not e).

While.

ρ ⊢_{β} ⟨e, σ^{♯}⟩ → ⟨υ_{0}^{♯}, ε_{0}^{♯}⟩ ρ ⊢_{β} ⟨s, σ_{tt}^{♯}⟩ → ⟨σ_{1}^{♯}, ε_{1}^{♯}⟩
ρ ⊢_{β} ⟨while e do s, σ_{1}^{♯}⟩ → ⟨σ_{2}^{♯}, ε_{2}^{♯}⟩
ρ ⊢_{β} ⟨while e do s, σ^{♯}⟩ ⇝ ⟨σ_{ff}^{♯} ⊔ σ_{2}^{♯}, ε_{0}^{♯} ⊔ ε_{1}^{♯} ⊔ ε_{2}^{♯}⟩

(109)

if σ_{tt}^{♯} = ϕ(ρ, σ^{♯}, e) and σ_{ff}^{♯} = ϕ(ρ, σ^{♯}, not e).

On the Design of Generic Static Analyzers for Imperative Languages · 41

Throw.

\overline{if ε^{♯} = σ^{♯} ⊗ α(\{χ\})} ; ρ ⊢_{β} ⟨throw χ, σ^{♯}⟩ ⇝ ⟨⊥, ε^{♯}⟩  (110)

ρ ⊢_{β} ⟨e, σ^{♯}⟩ → ⟨(sval^{♯}, σ_{0}^{♯}), ε_{0}^{♯}⟩

\overline{if ε_{1}^{♯} = σ_{0}^{♯} ⊗ sval^{♯}}

ρ ⊢_{β} ⟨throw e, σ^{♯}⟩ ⇝ ⟨⊥, ε_{0}^{♯} ⊔ ε_{1}^{♯}⟩

(111)

Try blocks. ρ ⊢_{β} ⟨s, σ^{♯}⟩ → ⟨σ_{0}^{♯}, ε_{0}^{♯}⟩ ρ ⊢_{β} ⟨k, ε_{0}^{♯}⟩ → ⟨(σ_{1}^{♯}, ε_{1}^{♯}), ε_{2}^{♯}⟩

ρ ⊢_{β} ⟨try s catch k, σ^{♯}⟩ ⇝ ⟨σ_{0}^{♯} ⊔ σ_{1}^{♯}, ε_{1}^{♯} ⊔ ε_{2}^{♯}⟩

(112)

\begin{aligned}ρ ⊢_{β} ⟨s_{0}, σ^{♯}⟩ → ⟨σ_{0}^{♯}, (σ_{1}^{♯}, ξ_{1}^{♯})⟩ & ρ ⊢_{β} ⟨s_{1}, σ_{0}^{♯}⟩ → ⟨σ_{2}^{♯}, ε_{2}^{♯}⟩ \\ & ρ ⊢_{β} ⟨s_{1}, σ_{1}^{♯}⟩ → ⟨σ_{3}^{♯}, ε_{3}^{♯}⟩ \end{aligned}

ρ ⊢_{β} ⟨try s_{0} finally s_{1}, σ^{♯}⟩ ⇝ ⟨σ_{2}^{♯}, ε_{2}^{♯} ⊔ ε_{3}^{♯} ⊔ (σ_{3}^{♯} ⊗ ξ_{1}^{♯})⟩

(113)

Function call. With reference to conditions (60) and (61) of the concrete rules for function calls, the corresponding abstract rule schema is

ρ ⊢_{β} ⟨d, mark_{s}^{♯}(σ^{♯})⟩ → ⟨(ρ_{0}, σ_{0}^{♯}), ε_{0}^{♯}⟩ ρ[ρ_{1}] ⊢_{β[β_{1}]} ⟨body, link_{s}^{♯}(σ_{0}^{♯})⟩ → ⟨σ_{1}^{♯}, ε_{1}^{♯}⟩ ρ[ρ_{0}] ⊢_{β[β_{0}]} ⟨id_{0} := \underline{x}_{0}, unlink_{s}^{♯}(σ_{1}^{♯})⟩ → ⟨σ_{2}^{♯}, ε_{2}^{♯}⟩

ρ ⊢_{β} ⟨id_{0} := id(e_{1}, …, e_{n}), σ^{♯}⟩ ⇝ ⟨unmark_{s}^{♯}(σ_{2}^{♯}), ε^{♯}⟩

(114)

if (60) and (61) hold and ε^{♯} = ε_{0}^{♯} ⊔ unmark_{s}^{♯}(unlink_{s}^{♯}(ε_{1}^{♯})) ⊔ unmark_{s}^{♯}(ε_{2}^{♯}).

6.9.4 Function Bodies.

ρ ⊢_{β} ⟨d, mark_{s}^{♯}(σ^{♯})⟩ → ⟨(ρ_{0}, σ_{0}^{♯}), ε_{0}^{♯}⟩

ρ[ρ_{0}] ⊢_{β[β_{0}]} ⟨s, σ_{0}^{♯}⟩ → ⟨σ_{1}^{♯}, ε_{1}^{♯}⟩
ρ[ρ_{0}] ⊢_{β[β_{0}]} ⟨\underline{x}_{0} := e, σ_{1}^{♯}⟩ → ⟨σ_{2}^{♯}, ε_{2}^{♯}⟩

ρ ⊢_{β} ⟨let d in s result e, σ^{♯}⟩ ⇝ ⟨unmark_{s}^{♯}(σ_{2}^{♯}), ε_{3}^{♯}⟩

(115)

if β ⊢_{FI(d)} d : β_{0}, ε_{3}^{♯} = ε_{0}^{♯} ⊔ unmark_{s}^{♯}(ε_{1}^{♯} ⊔ ε_{2}^{♯}).

ρ ⊢_{β} ⟨extern, σ^{♯}⟩ ⇝ ⟨σ_{0}^{♯}, (σ_{0}^{♯}, ⊤)⟩  (116)

if ∀σ, σ_{0} ∈ Mem : (σ = (μ, w) ∧ σ ∝ σ^{♯} ∧ σ_{0} = (μ_{0}, w)) ⟹ σ_{0} ∝ σ_{0}^{♯}. 6.9.5 Catch Clauses Catch.

ρ ⊢_{β} ⟨s, mem(ε_{0}^{♯})⟩ → η_{1}^{♯} ; ρ ⊢_{β} ⟨(p) s, ε^{♯}⟩ ⇝ ⟨η_{1}^{♯}, ε_{1}^{♯}⟩  (117)

if p = any or p = χ or p = cT, ε_{0}^{♯} = ϕ^{+}(p, ε^{♯}) and ε_{1}^{♯} = ϕ^{−}(p, ε^{♯}).

ρ[{id ↦ (i, sT)}] ⊢_{β[{id↦sT loc}]} ⟨s, σ_{2}^{♯}⟩ → ⟨σ_{3}^{♯}, ε_{3}^{♯}⟩
ρ ⊢_{β} ⟨(id : sT) s, ε^{♯}⟩ ⇝ ⟨(σ_{4}^{♯}, ε_{4}^{♯}), ε_{1}^{♯}⟩

(118)

if ε_{0}^{♯} = ϕ^{+}(sT, ε^{♯}), ε_{1}^{♯} = ϕ^{−}(sT, ε^{♯}), new_{s}^{♯}(sT(ε_{0}^{♯}), mark_{s}^{♯}(mem(ε_{0}^{♯}))) = ((σ_{2}^{♯}, i), ε_{2}^{♯}),

σ_{4}^{♯} = unmark_{s}^{♯}(σ_{3}^{♯}) and ε_{4}^{♯} = unmark_{s}^{♯}(ε_{2}^{♯}) ⊔ unmark_{s}^{♯}(ε_{3}^{♯}).

Catch sequence.

ρ ⊢_{β} ⟨k_{0}, ε^{♯}⟩ → ⟨(σ_{0}^{♯}, ε_{0}^{♯}), ε_{1}^{♯}⟩ ρ ⊢_{β} ⟨k_{1}, ε_{1}^{♯}⟩ → ⟨(σ_{1}^{♯}, ε_{2}^{♯}), ε_{3}^{♯}⟩ ; ρ ⊢_{β} ⟨k_{0}; k_{1}, ε^{♯}⟩ ⇝⟨(σ_{0}^{♯} ⊔ σ_{1}^{♯}, ε_{0}^{♯} ⊔ ε_{2}^{♯}), ε_{3}^{♯}⟩  (119)

6.9.6 Supported Expressions, Declarations and Statements. Let q ∈ {e, d, g, s} and N^{♯} ∈ Γ_{q}^{β♯}. Then, whenever supported^{♯}(ρ, N^{♯}) holds, alternate versions of the rules above apply. For each of the rules above,

P_{0} ⋯ P_{ℓ−1}

if (side condition) and not supported^{♯}(ρ, N^{♯})

ρ ⊢_{β} N^{♯} ⇝ η^{♯}

we also have the rule

P_{0} ⋯ P_{ℓ−1}

if (side condition) and supported^{♯}(ρ, N^{♯})

ρ ⊢_{β} N^{♯} ⇝ eval^{♯}(ρ, N^{♯})

Notice that even if eval^{♯}(ρ, N^{♯}) does not depend on the rule antecedents P_{0}, …, P_{ℓ−1}, these cannot be omitted, as this would neglect the sub-computations spawned by the unsupported evaluation of N^{♯}.

6.10 Abstract Semantics Trees

We now define possibly infinite abstract semantics trees along the lines of what we did in Section 5.7. Notice that the need to consider infinite abstract trees goes beyond the need to observe infinite concrete computations. For instance, there is no finite abstract tree corresponding to a program containing a while command, because (109) is the only abstract rule for while and it recursively introduces a new while node into the tree.

Definition 6.8. (Abstract semantics rules.) The set R^{♯} of abstract semantics rules is the infinite set obtained by instantiating the rule schemata of Section 6.9 in all possible ways (respecting the side conditions).

Let S^{♯} be the (infinite) set of sequents occurring in the premises and conclusions of the rules in R^{♯}. Matching Definition 5.6, the abstract semantics universe, denoted by U^{♯}, is the set of finitely branching trees of at most ω-depth with labels in S^{♯}.

Definition 6.9. (Abstract semantics trees.) Let F^{♯}: ℘(U^{♯}) → ℘(U^{♯}) be given, for each U^{♯} ∈ ℘(U^{♯}), by

F^{♯}(U^{♯}) =^{def} \{ {θ_{0}^{♯} ⋯ θ_{ℓ−1}^{♯} \atop s} | \{θ_{0}^{♯}, …, θ_{ℓ−1}^{♯}\} ⊆ U^{♯}, {θ_{0}^{♯}(ϵ) ⋯ θ_{ℓ−1}^{♯}(ϵ) \atop s} ∈ R^{♯} \}.

The set of abstract semantics trees is Θ^{♯} =^{def} gfp_{⊆}(F^{♯}).

We now show that, for every non-terminal abstract configuration, there exists an abstract tree with that in the root.

Proposition 6.10. For each β ∈ TEnv, ρ ∈ Env such that ρ : β and N^{♯} ∈ Γ_{q}^{β♯}, where q ∈ {e, d, g, s, b, k}, there exists θ^{♯} ∈ Θ^{♯} such that,

θ^{♯}(ϵ) ∈ { (ρ ⊢_{β} N^{♯} → η^{♯}) | η^{♯} ∈ T_{q}^{♯} }.

Proof. For the proof, let^{8}

S_{+}^{♯}(ρ, β, N^{♯}) =^{def} { s^{♯} | s^{♯} = (ρ ⊢_{β} N^{♯} → η^{♯}), (s ∝ s^{♯} ⟹ s is well-typed) }.

We now assume that N^{♯} ∈ Γ_{q}^{β♯} is a fixed but arbitrary non-terminal abstract configuration. Suppose that supported^{♯}(ρ, N^{♯}) does not hold. By inspecting the abstract evaluation rules given in Section 6.9, it can be seen that there exists ℓ ≥ 0 and a nonempty set of rules R_{0} ∈ R^{♯} with ℓ premises and a conclusion in S_{+}^{♯}(ρ, β, N^{♯}). If, on the other hand, supported^{♯}(ρ, N^{♯}) does hold, then it follows from Section 6.9.6 that, by Definition 6.7, eval^{♯}(ρ, N^{♯}) is defined and, for each rule in R_{0}, there is a rule with the same set of premises but where the conclusion (ρ ⊢_{β} N^{♯} → eval^{♯}(ρ, N^{♯})) is also in S_{+}^{♯}(ρ, β, N^{♯}). Thus, in both cases, by definition of U^{♯}, there exists a tree in U^{♯} with root in S_{+}^{♯}(ρ, β, N^{♯}).

We prove that, for any n ∈ ℕ, there exists a tree θ^{♯} ∈ F^{♯n}(U^{♯}) such that θ^{♯}(ϵ) ∈ S_{+}^{♯}(ρ, β, N^{♯}). To this end, we reason by induction on n ≥ 0. In the case n = 0, U = F^{♯n}(U^{♯}) so that the hypothesis holds.

We now suppose that n > 0. Let j ∈ {0, …, ℓ} be the maximal value for which there exist trees θ_{0}^{♯}, …, θ_{j−1}^{♯} ∈ F^{♯(n−1)}(U^{♯}) where P_{0} = θ_{0}^{♯}(ϵ), …, P_{j−1} = θ_{j−1}^{♯}(ϵ) are the first j premises of a rule in R_{0}; let R_{j} ⊆ R_{0} be the set of all rules in R_{0} with P_{0}, …, P_{j−1} as their first j premises; then R_{j} ≠ ∅. We assume that j < ℓ and derive a contradiction. By inspecting the rule schemata in Section 6.9, it can be seen that, if there exists \frac{P_{0} ··· P_{j−1} P′_{j} ···}{ś^{♯}} ∈ R_{j} for some P′_{j} ∈ S_{+}^{♯}(ρ_{j}, β_{j}, N_{j}^{♯}) and ś^{♯} ∈ S_{+}^{♯}(ρ, β, N^{♯}), then

∀P_{j} ∈ S_{+}^{♯}(ρ_{j}, β_{j}, N_{j}^{♯}) : ∃s^{♯} ∈ S_{+}^{♯}(ρ, β, N^{♯}) . \frac{P_{0} ⋯ P_{j−1} P_{j} ⋯}{s^{♯}} ∈ R_{j}. (120)

By the inductive hypothesis, there exists θ_{j}^{♯} ∈ F^{♯(n−1)}(U^{♯}) such that P_{j} = θ_{j}^{♯}(ϵ) ∈ S_{+}^{♯}(ρ_{j}, β_{j}, N_{j}^{♯}); hence, by (120), there must be a rule in R_{j} whose (j +1)-th premise is P_{j}; contradicting the assumption that j < ℓ is maximal. Hence j = ℓ. Thus there exists a rule \frac{P_{0} ··· P_{ℓ−1}}{s^{♯}} ∈ R_{0} for some s^{♯} ∈ S_{+}^{♯}(ρ, β, N^{♯}); hence, by Definition 6.9,

the tree \frac{θ_{0}^{♯} ··· θ_{ℓ−1}^{♯}}{s^{♯}} ∈ F^{♯n}(U^{♯}). Therefore since, by Definition 6.9, Θ^{♯} = gfp_{⊆}(F^{♯}), there exists a tree θ^{♯} in Θ^{♯} such that θ^{♯}(ϵ) ∈ S_{+}^{♯}(ρ, β, N^{♯}).

7. CORRECTNESS OF THE ABSTRACT SEMANTICS

In Section 6, we introduced the notion of sound approximation for configurations and sequents in terms of the concretization function γ defined for each abstract domain. We now proceed to define the notion of sound approximation for trees.

8For the definition of a well-typed sequent, see the proof of Proposition 5.8.

Definition 7.1. (‘∝’ for trees.) Let \overline{∝}: ℘(Θ × Θ^{♯}) → ℘(Θ × Θ^{♯}) be given, for each U ∈ ℘(Θ × Θ^{♯}), by

\overline{∝}(U) =^{def} \{ (θ, θ^{♯}) ∈ Θ × Θ^{♯} | \begin{matrix}θ(ϵ) ∝ θ^{♯}(ϵ), \\ ∀i ∈ dom(θ) ∩ ℕ : \\ ∃j ∈ dom(θ^{♯}) ∩ ℕ . (θ_{[i]}, θ_{[j]}^{♯}) ∈ U \end{matrix} \}.

Then θ ∝ θ^{♯} if and only if (θ, θ^{♯}) ∈ gfp_{⊆}(\overline{∝}).

In words, θ ∝ θ^{♯} means that the root of θ is approximated by the root of θ^{♯} and every immediate subtree of θ is approximated by some immediate subtrees of θ^{♯}. Notice that one immediate subtree in θ^{♯} may be related by ‘∝’ to none, one or more than one immediate subtree of θ.

The following result states that, for each concrete tree, there is always an abstract tree that is generated from a corresponding non-terminal abstract configuration.

Theorem 7.2. Let θ ∈ Θ be a concrete tree such that θ(ϵ) = (ρ ⊢_{β} N → η) or θ(ϵ) = (ρ ⊢_{β} N ⟶^{∞}). Then there exists θ^{♯} ∈ Θ^{♯} such that, θ^{♯}(ϵ) = (ρ ⊢_{β} N^{♯} → η^{♯}) and N ∝ N^{♯}.

Proof. Suppose first that N = ⟨q, σ⟩ where q ∈ {e, d, g, s, b}. By Definition 6.1, we can always find σ^{♯} ∈ Mem^{♯} such that σ ∝ σ^{♯}. Hence, letting N^{♯} = ⟨q, σ^{♯}⟩, by (78) in Definition 6.4, we obtain N ∝ N^{♯}. Next suppose N = ⟨k, ε⟩, where ε = (σ, ξ). As before, by Definition 6.1, we can always find σ^{♯} ∈ Mem^{♯} such that σ ∝ σ^{♯}. Moreover, by the definition of the approximation for exceptions, we can always find ξ^{♯} ∈ Except^{♯} such that ξ ∝ ξ^{♯}. Hence, letting N^{♯} = ⟨k, σ^{♯} ⊗ ξ^{♯}⟩, by (79) in Definition 6.4, we again obtain N ∝ N^{♯}. In both cases, by Proposition 6.10, there exists an abstract tree θ^{♯} such that θ^{♯}(ϵ) = (ρ ⊢_{β} N^{♯} → η^{♯}) and N ∝ N^{♯}.

The next result states that our abstract rules only generate abstract trees that are correct approximations of their concrete counterparts (i.e., concrete trees rooted with the same statement, the same environment and initial memory structure).

Theorem 7.3. Let θ ∈ Θ and θ^{♯} ∈ Θ^{♯} be such that θ(ϵ) = (ρ ⊢_{β} N → η) or

θ(ϵ) = (ρ ⊢_{β} N ⟶^{∞}) and θ^{♯}(ϵ) = (ρ ⊢_{β} N^{♯} → η^{♯}), where N ∝ N^{♯}. Then θ ∝ θ^{♯}.

Theorem 7.3 is a trivial corollary of the following

Proposition 7.4. Let

S =^{def} \{ (θ, θ^{♯}) ∈ Θ × Θ^{♯} | \begin{matrix}θ(ϵ) ∈ \{ρ ⊢_{β} N → η, ρ ⊢_{β} N ⟶^{∞}\}, \\ θ^{♯}(ϵ) = ρ ⊢_{β} N^{♯} → η^{♯}, \\ N ∝ N^{♯} \end{matrix} \}.  (121)

Then, for all (θ, θ^{♯}) ∈ S, θ ∝ θ^{♯}.

Proof. Let θ ∈ Θ and θ^{♯} ∈ Θ^{♯}. We define:

r =^{def} {θ_{[0]}(ϵ) ⋯ θ_{[h−1]}(ϵ) \atop θ(ϵ)}  r^{♯} =^{def} {θ_{[0]}^{♯}(ϵ) ⋯ θ_{[ℓ−1]}^{♯}(ϵ) \atop θ^{♯}(ϵ)}

where, for some h, ℓ ≥ 0, {0, …, h − 1} ⊆ dom(θ), {0, …, ℓ − 1} ⊆ dom(θ^{♯}), h ∉ dom(θ) and ℓ ∉ dom(θ^{♯}). By Definitions 5.7 and 6.9, r ∈ R and r^{♯} ∈ R^{♯}. Note that, to simplify the proof, we will use the schematic concrete and abstract rules given in Sections 5.5 and 6.9 to denote the actual rule instances r and r^{♯}.

Letting (θ, θ^{♯}) ∈ S, we need to show that θ ∝ θ^{♯}; by Definition 7.1, this is equivalent to showing that (θ, θ^{♯}) ∈ gfp_{⊆}(\overline{∝}). To this end, by the principle of fixpoint coinduction, we will show that (θ, θ^{♯}) ∈ \overline{∝}(S).

By Definition 7.1, we need to show that the following properties hold:

(i) θ(ϵ) ∝ θ^{♯}(ϵ); (ii) for each i = 0, …, h−1 there exists j ∈ {0, …, ℓ−1} such that (θ_{[i]}, θ_{[j]}^{♯}) ∈ S.

The proof that properties (i) and (ii) hold is by (well-founded) induction on the structure of the concrete tree θ. Observe that the “immediate subtree” relation between trees in Θ_{+} is a well-founded partial ordering because, if θ ∈ Θ_{+} then, by Definition 5.7, there are no infinite descending chains. We extend this ordering relation to the immediate positive subtree relation between trees in Θ: θ′ is said to be an immediate positive subtree of θ if and only if θ′ ∈ Θ_{+} and is an immediate subtree of θ. Clearly, by Definition 5.7, the immediate positive subtree ordering on trees in Θ is also well-founded.

We first note that it is not restrictive to only consider unsupported expressions, declarations or statements: as noted in Section 6.9, the tree for any supported expression (resp., declaration or statement) has the same structure as the tree for the same expression (resp., declaration or statement) as if it were unsupported. Hence, once correctness of the approximation for unsupported expressions, declarations or statements is proved, the correctness for their supported counterparts will immediately follow from Definition 6.7.

Let

θ(ϵ) = (ρ ⊢_{β} N → η) or θ(ϵ) = (ρ ⊢_{β} N ⟶^{∞}),

θ^{♯}(ϵ) = (ρ ⊢_{β} N^{♯} ⇝ η^{♯}).

By (121), N ∝ N^{♯}. Therefore, by condition (85) of Definition 6.6, property (i) holds trivially whenever θ ∈ Θ_{−} (i.e., when r is a negative concrete rule). In addition, to prove that property (i) holds for each θ ∈ Θ_{+} (i.e., when r is a positive concrete rule), by condition (84) of Definition 6.6, we just need to show η ∝ η^{♯}.

Consider next property (ii). The base cases are when the concrete rule r has no premises (i.e., h = 0); and this property holds trivially in these cases. For the inductive steps (i.e., h > 0) suppose i ∈ {0, …, h−1} and j ∈ {0, …, ℓ−1} are such that (θ_{[i]}, θ_{[j]}^{♯}) ∈ S. If θ ∈ Θ_{+} then, by the inductive hypothesis, we can assume that

(θ_{[i]}, θ_{[j]}^{♯}) ∈ \overline{∝}(S); similarly, if θ ∈ Θ_{−} and i ≠ h − 1, by the inductive hypothesis,

we can assume that, (θ_{[i]}, θ_{[j]}^{♯}) ∈ \overline{∝}(S). Hence, in both cases, by Definition 7.1,

θ_{[i]}(ϵ) ∝ θ_{[j]}^{♯}(ϵ). Also, if θ ∈ Θ_{−}, by Definition 5.7, θ_{[h−1]}(ϵ) is a divergent sequent

so that, by Definitions 6.6 and 7.1, θ_{[h−1]}(ϵ) ∝ θ_{[j]}^{♯}(ϵ). Thus, for all concrete trees θ ∈ Θ, we can safely assume the following:

∀i ∈ {0, …, h − 1}, j ∈ {0, …, ℓ − 1} : (θ_{[i]}, θ_{[j]}^{♯}) ∈ S ⟹ θ_{[i]}(ϵ) ∝ θ_{[j]}^{♯}(ϵ). (122)

Moreover, we need only explicitly prove property (ii) for each of the positive rules since, by the definition of the concrete divergence (negative) rules, (122) and Defini-

Table I. Corresponding concrete and abstract rules and terminals for expressions

E r r^{♯} η_{e} η_{e}^{♯} = ⟨(sval_{a}^{♯}, σ_{a}^{♯}), ε_{a}^{♯}⟩
(sval_{a}^{♯}, σ_{a}^{♯})  ε_{a}^{♯}
con  2  86 ⟨con, σ⟩  α({con}) ⊗ σ^{♯} none^{♯}
id  3  87 σ[ρ(id)]  σ^{♯}[ρ(id)]
−e  4  88 ε  (⊖ m^{♯}, σ_{0}^{♯})  ε^{♯}
5  ⟨−m, σ_{0}⟩
e_{0} ⧇ e_{1} 6/7 89 ε (m_{0}^{♯} ⊚ m_{1}^{♯}, σ_{1}^{♯}) ε_{0}^{♯} ⊔ ε_{1}^{♯}
90  (m_{0}^{♯} ⊚ m_{1}^{♯}, σ_{1}^{♯}) ε_{0}^{♯} ⊔ ε_{1}^{♯} ⊔ ε_{2}^{♯}
8 89 ⟨m_{0} ∘ m_{1}, σ_{1}⟩ (m_{0}^{♯} ⊚ m_{1}^{♯}, σ_{1}^{♯}) ε_{0}^{♯} ⊔ ε_{1}^{♯}
90  (m_{0}^{♯} ⊚ m_{1}^{♯}, σ_{1}^{♯}) ε_{0}^{♯} ⊔ ε_{1}^{♯} ⊔ ε_{2}^{♯}
9  90 ⟨σ_{1}, divbyzero⟩ (m_{0}^{♯} ⊚ m_{1}^{♯}, σ_{1}^{♯}) ε_{0}^{♯} ⊔ ε_{1}^{♯} ⊔ ε_{2}^{♯}
m_{0} ⧆ m_{1} 10/11 91 ε  (m_{0}^{♯} ▷◁ m_{1}^{♯}, σ_{1}^{♯}) ε_{0}^{♯} ⊔ ε_{1}^{♯}
12  ⟨m_{0} ≶ m_{1}, σ_{1}⟩
not b 13 92 ε (⊝ t^{♯}, σ_{0}^{♯}) ε^{♯}
14  ⟨¬ t, σ_{0}⟩
b_{0} and b_{1} 15 93 ε υ_{ff}^{♯} ⊔ υ_{1}^{♯} ε_{0}^{♯} ⊔ ε_{1}^{♯}
16  ⟨ff, σ_{0}⟩
17  η
b_{0} or b_{1} 18–20 94  Similar to the rows for ‘b_{0} and b_{1}’

tion 6.4, if property (ii) holds for any positive rule it also holds for the corresponding negative rules. Thus in the detailed proofs of properties (i) and (ii) for the inductive steps, we only consider the positive rules.

To help the reader, Tables I, II, III, IV and V, contain a summary of the conclusions of rules r and r^{♯}. The first column Q ∈ {E, D, G, S, B, K}, gives the syntactic forms in the first component of the non-terminal configurations N and N^{♯} (which, by Definition 6.4, must be the same); the second and third columns give a concrete rule r and abstract rule r^{♯}, respectively, that apply to Q. Note that we do not pair concrete rules with abstract rules that have mutually inconsistent side conditions. Justification for the omission of any abstract rules for a particular concrete rule r is given in the detailed proof for that case. The column headed η_{q}, where q ∈ {e, d, g, s, b, k} gives the concrete terminal configuration for r, while the columns headed by η_{q}^{♯} give the components of the abstract terminal configuration for r^{♯}. A blank entry in any table cell means that the value is exactly the same as the value found in the same column of the previous row. To save space in Tables II, III, IV and V, we have denoted the operations ‘cleanup_{d}’, ‘unmark_{s}’, ‘unlink_{s}’, ‘unmark_{s}^{♯}’ and ‘unlink_{s}^{♯}’ by ‘cu_{d}’, ‘um_{s}’, ‘ul_{s}’, ‘um_{s}^{♯}’ and ‘ul_{s}^{♯}’, respectively. Note that the premises and the side conditions for the rules are not provided in any of the tables; reference must be made to the actual rules for this information.

7.1 Expressions

For this part of the proof, we use Table I. By (121), N ∝ N^{♯}. Thus letting N = ⟨E, σ⟩ and N^{♯} = ⟨E, σ^{♯}⟩, by Definition 6.4, we have the implicit hypothesis σ ∝ σ^{♯}. We show using (80) in Definition 6.5, that η_{e} ∝ η_{e}^{♯}.

Constant. Suppose r is an instance of (2). By definition of α: ℘(Integer) ↣ Integer^{♯} and α: ℘(Bool) ↣ Bool^{♯}, we have con ∝ α({con}); by hypothesis, σ ∝ σ^{♯} so that ⟨con, σ⟩ ∝ α({con}) ⊗ σ^{♯}. Hence η_{e} ∝ η_{e}^{♯}.

Identifier. Suppose r is an instance of (3). Since, by hypothesis, σ ∝ σ^{♯}, by Definition 6.1 we obtain σ[ρ(id)] ∝ σ^{♯}[ρ(id)]. Hence, η_{e} ∝ η_{e}^{♯}.

Unary Minus. Suppose r is an instance of (4) or (5). Then, by hypothesis, (θ_{[0]}, θ_{[0]}^{♯}) ∈ S and, hence, as h = 1, property (ii) holds. By (122), θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ). Thus, if r is an instance of (4), then ε ∝ ε^{♯}; if r is an instance of (5), then m ∝ m^{♯} and σ_{0} ∝ σ_{0}^{♯}. In the latter case, by the soundness of ‘⊖’, −m ∝ ⊖ m^{♯}. Hence, in both cases, η_{e} ∝ η_{e}^{♯}.

Binary Arithmetic Operations. Suppose that r is an instance of one of the rules (6)–(9). Then, by hypothesis, (θ_{[0]}, θ_{[0]}^{♯}) ∈ S. By (122), θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ). Note that, in the condition for abstract rule (90), ε_{2}^{♯} = σ_{1}^{♯} ⊗ α({divbyzero}).

If r is an instance of (6), then h = 1 so that property (ii) holds. The property θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ) implies ε ∝ ε_{0}^{♯}. Therefore,^{9} η_{e} ∝ η_{e}^{♯}.

If r is an instance of (7), (8) or (9), then h = 2. Property θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ) implies σ_{0} ∝ σ_{0}^{♯} and m_{0} ∝ m_{0}^{♯}; hence (θ_{[1]}, θ_{[1]}^{♯}) ∈ S and property (ii) holds. By (122), θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ).

If r is an instance of (7), then property θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ) implies ε ∝ ε_{1}^{♯}; thus η_{e} ∝ η_{e}^{♯}. If r is an instance of (8), then property θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ) implies σ_{1} ∝ σ_{1}^{♯} and m_{1} ∝ m_{1}^{♯} so that, by the soundness of ‘⊚’, (m_{0} ⧇ m_{1}) ∝ (m_{0}^{♯} ⊚ m_{1}^{♯}); and hence η_{e} ∝ η_{e}^{♯}. If r is an instance of (9), then the condition θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ) implies σ_{1} ∝ σ_{1}^{♯} and 0 ∝ m_{1}^{♯}. Hence, by the side conditions, r^{♯} must be an instance of (90); so that, as ⟨σ_{1}, divbyzero⟩ ∝ σ_{1}^{♯} ⊗ α({divbyzero}), we have η_{e} ∝ η_{e}^{♯}.

Test Operators. Suppose r is an instance of one of rules (10)–(12). Then, by hypothesis, (θ_{[0]}, θ_{[0]}^{♯}) ∈ S. By (122), θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ).

If r is an instance of (10), then h = 1 and property (ii) holds. θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ) implies ε ∝ ε_{0}^{♯}. Hence η_{e} ∝ η_{e}^{♯}.

If r is an instance of (11) or (12), then h = 2. θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ) implies σ_{0} ∝ σ_{0}^{♯} and m_{0} ∝ m_{0}^{♯}. Thus (θ_{[1]}, θ_{[1]}^{♯}) ∈ S and property (ii) holds. By (122), θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ). If r is an instance of (11), then ε ∝ ε_{1}^{♯}; and if r is an instance of (12), σ_{1} ∝ σ_{1}^{♯} and m_{1} ∝ m_{1}^{♯} so that, by soundness of ‘▷◁’, (m_{0} ≶ m_{1}) ∝ (m_{0}^{♯} ▷◁ m_{1}^{♯}). Hence, for both concrete rules, η_{e} ∝ η_{e}^{♯}.

Negation. The proof when r is an instance of (13) or (14) has the same structure of the proof for the unary minus case shown before.

Conjunction. Suppose r is an instance of one of rules (15)–(17). By hypothesis, (θ_{[0]}, θ_{[0]}^{♯}) ∈ S.

9Here and in the following, whenever we need to prove ι ∝ ι_{0}^{♯} ⊔ ι_{1}^{♯}, we just prove either ι ∝ ι_{0}^{♯} or ι ∝ ι_{1}^{♯} and implicitly use the monotonicity of γ.

Table II. Corresponding concrete and abstract rules and terminals for declarations

Q r r^{♯} η_{q} η_{q}^{♯} = ⟨(ρ_{a}^{♯}, σ_{a}^{♯}), ε_{a}^{♯}⟩
(ρ_{a}^{♯}, σ_{a}^{♯})  ε_{a}^{♯}
nil  21  95  ⟨∅, σ⟩  (∅, σ^{♯})  none^{♯}
ρ_{0}  22  96  ⟨ρ_{0}, σ⟩  (ρ_{0}, σ^{♯})  none^{♯}
rec ρ_{0}  23  97  ⟨ρ_{1}, σ⟩  (ρ_{1}, σ^{♯})  none^{♯}
gvar id : sT = e  24/25 98  cu_{d}(ε)  (ρ_{1}, σ_{1}^{♯})  cu_{d}^{♯}(ε_{0}^{♯} ⊔ ε_{1}^{♯})
26  ⟨ρ_{1}, σ_{1}⟩
lvar id : sT = e 27/28 99 um_{s}(ε) (ρ_{1}, σ_{1}^{♯}) um_{s}^{♯}(ε_{0}^{♯} ⊔ ε_{1}^{♯})
29  ⟨ρ_{1}, σ_{1}⟩
function id(fps) : sT = e 30  100 ⟨ρ_{0}, σ⟩  (ρ_{0}, σ^{♯})  none^{♯}
rec g  31  101 η  η^{♯}
g_{0}; g_{1}  32/33 102 ε  (ρ_{0}[ρ_{1}], σ_{1}^{♯}) ε_{0}^{♯} ⊔ ε_{1}^{♯}
34  ⟨ρ_{0}[ρ_{1}], σ_{1}⟩
d_{0}; d_{1}  35–37 103  Similar to the rows for ‘g_{0}; g_{1}’

If r is an instance of (15) or (16), then h = 1 and property (ii) holds. If r is an instance of (15), by (122), we have θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ), which implies ε ∝ ε_{0}^{♯}. If r

is an instance of (16), by Definition 6.2, σ_{0} ∝ σ_{ff}^{♯} = ϕ(ρ, σ^{♯}, not b_{0}). Thus, since ff ∝ α({ff}) holds by definition, we have ⟨ff, σ_{0}⟩ ∝ υ_{ff}^{♯}. Hence, for both concrete rules, η_{e} ∝ η_{e}^{♯}.

If r is an instance of (17), then h = 2. By Definition 6.2, σ_{0} ∝ σ_{tt}^{♯}, so that (θ_{[1]}, θ_{[1]}^{♯}) ∈ S and property (ii) holds. By (122), θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ) so that η ∝ ⟨υ_{1}^{♯}, ε_{1}^{♯}⟩. Hence, η_{e} ∝ η_{e}^{♯}.

Disjunction. The proof when r is an instance of one of rules (18)–(20) is similar to that for conjunction.

7.2 Declarations

In Table II, Q denotes a local declaration D or a global declaration G. Moreover, η_{q} ∈ {T_{d}, T_{g}} and η_{q}^{♯} ∈ {T_{d}^{♯}, T_{g}^{♯}}, the actual domains for η_{q} and η_{q}^{♯} will depend on context.

By (121) we have N ∝ N^{♯}. Thus letting N = ⟨Q, σ⟩ and N^{♯} = ⟨Q, σ^{♯}⟩ for any Q ∈ {D, G}, by Definition 6.4, we have the implicit hypothesis σ ∝ σ^{♯}. We show using (81) in Definition 6.5, that η_{q} ∝ η_{q}^{♯}.

Nil. If r is an instance of (21) then, by the hypothesis, η_{q} ∝ η_{q}^{♯}.

(Recursive) Environment. If r is an instance of (22) or (23) then, by the hypothesis, η_{q} ∝ η_{q}^{♯}.

Global Variable Declaration. If r is an instance of one of rules (24)–(26) then, by the hypothesis (θ_{[0]}, θ_{[0]}^{♯}) ∈ S so that, as h = 1, property (ii) holds. By (122),

θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ). If r is an instance of (24), then θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ) implies ε ∝ ε_{0}^{♯};

by Definition 6.1 and monotonicity of γ, we have cleanup_{d}(ε) ∝ cleanup_{d}^{♯}(ε_{0}^{♯} ⊔ ε_{1}^{♯}), i.e., η_{q} ∝ η_{q}^{♯}. If r is an instance of (25) or (26), then θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ) implies υ ∝ υ^{♯}. By Definition 6.1, new_{d}(υ) ∝ new_{d}^{♯}(υ^{♯}). By the side condition for abstract rule (98), new_{d}^{♯}(υ) = ((σ_{1}^{♯}, l), ε_{1}^{♯}). By the side conditions for (25) and (26), either new_{d}(υ) = ε ∝ ε_{1}^{♯} —and hence cleanup_{d}(ε) ∝ cleanup_{d}^{♯}(ε_{0}^{♯} ⊔ε_{1}^{♯}) by Definition 6.1— or new_{d}(υ) = (σ_{1}, l) ∝ (σ_{1}^{♯}, l). Thus, in both cases, η_{q} ∝ η_{q}^{♯}.

Local Variable Declaration. The proof for local variable declaration, when r is an instance of one of rules (27)–(29), is the same as that for global variable declaration, with the few necessary adjustments (i.e., using unmark_{s}, unmark_{s}^{♯}, new_{s}, new_{s}^{♯} and i in place of cleanup_{d}, cleanup_{d}^{♯}, new_{d}, new_{d}^{♯} and l).

Function Declaration. If r is an instance of (30) then, by the hypothesis, η_{q} ∝ η_{q}^{♯}.

Recursive Declaration. If r is an instance of (31), then h = 2 and, by the hypothesis, (θ_{[0]}, θ_{[0]}^{♯}) ∈ S. By (122), θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ), which implies that ρ_{0} denotes the same environment in both r and r^{♯} and σ_{0} ∝ σ_{0}^{♯}. Hence, (θ_{[1]}, θ_{[1]}^{♯}) ∈ S and property (ii) holds. By (122), θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ) which implies η ∝ η^{♯}. Hence, η_{q} ∝ η_{q}^{♯}.

Global Sequential Composition. If r is an instance of one of rules (32)–(34), then 1 ≤ h ≤ 2 and (θ_{[0]}, θ_{[0]}^{♯}) ∈ S. By (122), θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ).

If r is an instance of (32), then h = 1 and property (ii) holds. Also, θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ) implies ε ∝ ε_{0}^{♯} and hence η_{q} ∝ η_{q}^{♯}.

If r is an instance of (33) or (34), then h = 2 and, since σ_{0} ∝ σ_{0}^{♯}, (θ_{[1]} ∝ θ_{[1]}^{♯}) ∈ S, so that property (ii) holds. By (122), we have θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ). If r is an instance of (33), then θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ) implies ε ∝ ε_{1}^{♯}, so that η_{q} ∝ η_{q}^{♯}. If r is an instance of (34), then θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ) and θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ) imply that σ_{1} ∝ σ_{1}^{♯} and that the two environments ρ_{0} and ρ_{1} are the same in both r and r^{♯}. Hence, their composition ρ_{0}[ρ_{1}] is the same in both rules r and r^{♯}, so that η_{q} ∝ η_{q}^{♯}.

Local Sequential Composition. The proof when r is an instance of one of rules (35)–(37) is similar to that for global sequential composition.

7.3 Statements For this part of the proof, we use Table III. By (121), N ∝ N^{♯}. Thus letting N = ⟨s, σ⟩ and N^{♯} = ⟨s, σ^{♯}⟩, by Definition 6.4, we have the implicit hypothesis σ ∝ σ^{♯}. We show using (82) in Definition 6.5, that η_{s} ∝ η_{s}^{♯}.

Nop. If r is an instance of (38) then, by the hypothesis, η_{e} ∝ η_{e}^{♯}.

Assignment. Suppose r is an instance of (39) or (40). Then h = 1 and, by the hypothesis, (θ_{[0]}, θ_{[0]}^{♯}) ∈ S and hence property (ii) holds. By (122) we have θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ). If r is an instance of (39), ε ∝ ε_{0}^{♯}. Moreover, if r is an instance of (40), ⟨sval, σ_{0}⟩ ∝ ⟨sval_{0}^{♯}, σ_{0}^{♯}⟩ so that, by Definition 6.1, σ_{0}[ρ(id) := sval] ∝ σ_{0}^{♯}[ρ(id) := sval^{♯}]; letting σ_{0}^{♯}[ρ(id) := sval^{♯}] = (σ_{1}^{♯}, ε_{1}^{♯}), this means that either we have σ_{0}[ρ(id) := sval] ∈ ExceptState, so that σ_{0}[ρ(id) := sval] ∝ ε_{1}^{♯}, or we have σ_{0}[ρ(id) := sval] ∈ Mem, so that σ_{0}[ρ(id) := sval] ∝ σ_{1}^{♯}. In all cases, η_{s} ∝ η_{s}^{♯}.

Table III. Corresponding concrete and abstract rules and terminals for statements

S r r^{♯} η_{s} η_{s}^{♯} = ⟨σ_{a}^{♯}, ε_{a}^{♯}⟩
σ_{a}^{♯}  ε_{a}^{♯}
nop  38  104 σ  σ^{♯}  none^{♯}
id := e  39  105 ε  σ_{1}^{♯}  ε_{0}^{♯} ⊔ ε_{1}^{♯}
40  σ_{0}[ρ(id) := sval]
s_{0}; s_{1} 41 106 ε σ_{1}^{♯} ε_{0}^{♯} ⊔ ε_{1}^{♯}
42  η
d; s 43 107 ε um_{s}^{♯}(σ_{1}^{♯}) ε_{0}^{♯} ⊔ um_{s}^{♯}(ε_{1}^{♯})
44  um_{s}(η)
if e then s_{0} else s_{1} 45 108 ε σ_{1}^{♯} ⊔ σ_{2}^{♯} ε_{0}^{♯} ⊔ ε_{1}^{♯} ⊔ ε_{2}^{♯}
46/47  η
while e do s_{0} 48/50 109 ε σ_{ff}^{♯} ⊔ σ_{2}^{♯} ε_{0}^{♯} ⊔ ε_{1}^{♯} ⊔ ε_{2}^{♯}
49  σ_{0}
51  η
throw s  52  110 ⟨σ, χ⟩  ⊥  ε^{♯}
53  111 ε  ε_{0}^{♯} ⊔ ε_{1}^{♯}
54  ⟨σ_{0}, sval⟩
try s catch k 55 112 σ_{0} σ_{0}^{♯} ⊔ σ_{1}^{♯} ε_{1}^{♯} ⊔ ε_{2}^{♯}
56  η
try s_{0} finally s_{1} 57 113 η σ_{2}^{♯} ε_{2}^{♯} ⊔ ε_{3}^{♯} ⊔ (σ_{3}^{♯} ⊗ ξ_{1}^{♯})
58  ⟨σ_{1}, ξ_{0}⟩
59  ε
id := id_{0}(e_{1}, …, e_{n}) 62  114 ε  um_{s}^{♯}(σ_{2}^{♯}) ε^{♯} = ε_{0}^{♯}
63  um_{s}(ul_{s}(ε))  ⊔ um_{s}^{♯}(ul_{s}^{♯}(ε_{1}^{♯}))
64  um_{s}(η_{2})  ⊔ um_{s}(ε_{2}^{♯})

Statement Sequence. Suppose r is an instance of (41) or (42). Then 1 ≤ h ≤ 2 and, by the hypothesis, (θ_{[0]}, θ_{[0]}^{♯}) ∈ S. By (122), θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ). If r is an instance of rule (41), as h = 1, property (ii) holds and also ε ∝ ε_{0}^{♯}. If r is an instance of (42), then σ_{0} ∝ σ_{0}^{♯} so that (θ_{[1]}, θ_{[1]}^{♯}) ∈ S; also, as h = 2, property (ii) holds; by (122), θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ) so that η ∝ ⟨σ_{1}^{♯}, ε_{1}^{♯}⟩. Hence, in both cases, η_{s} ∝ η_{s}^{♯}.

Block. Suppose r is an instance of (43) or (44). Then 1 ≤ h ≤ 2 and, by the hypothesis and Definition 6.1, (θ_{[0]}, θ_{[0]}^{♯}) ∈ S. By (122), θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ). If r is an instance of (43), as h = 1, property (ii) holds and also ε ∝ ε_{0}^{♯}. If r is an instance of (44), then σ_{0} ∝ σ_{0}^{♯} so that (θ_{[1]}, θ_{[1]}^{♯}) ∈ S; also, as h = 2, property (ii) holds; by (122), θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ); so that η ∝ ⟨σ_{1}^{♯}, ε_{1}^{♯}⟩ and therefore, by Definition 6.1, unmark_{s}(η) ∝ ⟨unmark_{s}^{♯}(σ_{1}^{♯}), unmark_{s}^{♯}(ε_{1}^{♯})⟩. Hence, in both cases η_{s} ∝ η_{s}^{♯}.

Conditional. Suppose r is an instance of one of rules (45)–(47). Then 1 ≤ h ≤ 2 and, by the hypothesis, (θ_{[0]}, θ_{[0]}^{♯}) ∈ S. By (122), θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ).

If r is an instance of (45), h = 1, property (ii) holds and, as ε ∝ ε_{0}^{♯}, η_{s} ∝ η_{s}^{♯}. If r is an instance of (46) or (47), then h = 2 and σ_{0} ∝ σ_{0}^{♯}. By the side

conditions and Definition 6.2, if tt ∝ t^{♯}, then ⟨tt, σ_{0}⟩ ∝ ⟨t^{♯}, σ_{tt}⟩ and, if ff ∝ t^{♯}, then ⟨ff, σ_{0}⟩ ∝ ⟨t^{♯}, σ_{ff}⟩. Hence, if (46) applies, θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ) so that η ∝ ⟨σ_{1}^{♯}, ε_{1}^{♯}⟩; and, if (47) applies, θ_{[1]}(ϵ) ∝ θ_{[2]}^{♯}(ϵ) so that η ∝ ⟨σ_{2}^{♯}, ε_{2}^{♯}⟩. Hence, in both cases, η_{s} ∝ η_{s}^{♯}.

While. Suppose r is an instance of one of rules (48)–(51). Then 1 ≤ h ≤ 3 and, by hypothesis, (θ_{[0]}, θ_{[0]}^{♯}) ∈ S. By (122), θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ).

If r is an instance of (48), h = 1, property (ii) holds and, as ε ∝ ε_{0}^{♯}, η_{s} ∝ η_{s}^{♯}. Suppose r is an instance of (49), (50) or (51). By the side conditions and Defi-

nition 6.2, if tt ∝ t^{♯}, then ⟨tt, σ_{0}⟩ ∝ ⟨t^{♯}, σ_{tt}⟩ and, if ff ∝ t^{♯}, then ⟨ff, σ_{0}⟩ ∝ ⟨t^{♯}, σ_{ff}⟩. If r is an instance of (49), then, as h = 1, property (ii) holds and hence η_{s} ∝ η_{s}^{♯}. If r is an instance of (50), then h = 2. Thus (θ_{[1]}, θ_{[1]}^{♯}) ∈ S and property (ii)

holds. By (122), θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ) so that ε ∝ ε_{1}^{♯}. Hence η_{s} ∝ η_{s}^{♯}.

If r is an instance of (51), then h = 3. Thus (θ_{[1]}, θ_{[1]}^{♯}) ∈ S. By (122), θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ) so that σ_{1} ∝ σ_{1}^{♯}. Thus (θ_{[2]}, θ_{[2]}^{♯}) ∈ S and property (ii) holds. By (122), θ_{[2]}(ϵ) ∝ θ_{[2]}^{♯}(ϵ) so that η ∝ ⟨σ_{2}^{♯}, ε_{2}^{♯}⟩. Hence η_{s} ∝ η_{s}^{♯}.

Throw. Suppose r is an instance of (52). Then s = χ ∈ RTSExcept (so that rule (111) is not applicable). By definition of α: ℘(RTSExcept) ↣ RTSExcept^{♯}, χ ∝ α({χ}). Since, by hypothesis, σ ∝ σ^{♯}, σ^{♯} ⊗ α({χ}) = ⟨σ^{♯}, α({χ})⟩ so that, by the side condition for (110), (σ, χ) ∝ ε^{♯}. Hence η_{s} ∝ η_{s}^{♯}.

Suppose r is an instance of (53) or (54). Then s = e ∈ Exp (so that rule (110) is not applicable). By hypothesis, (θ_{[0]}, θ_{[0]}^{♯}) ∈ S and, as h = 1, property (ii) holds. By (122), θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ). If r is an instance of (53), then ε ∝ ε_{0}^{♯}, while, if r is an instance of (54), sval ∝ sval^{♯} and σ_{0} ∝ σ_{0}^{♯}. Hence, in both cases, η_{s} ∝ η_{s}^{♯}.

Try Blocks. Suppose r is an instance of (55)–(59). By hypothesis, (θ_{[0]}, θ_{[0]}^{♯}) ∈ S. By (122), θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ). Note that if r is an instance of (55) or (56), only abstract rule (112) will be applicable while if r is an instance of (57)–(59), only abstract rule (113) will be applicable.

If r is an instance of (55), h = 1, property (ii) holds and, as σ_{0} ∝ σ_{0}^{♯}, η_{s} ∝ η_{s}^{♯}. If r is an instance of (56), then ε_{0} ∝ ε_{0}^{♯} so that (θ_{[1]}, θ_{[1]}^{♯}) ∈ S. Thus, as h = 2,

property (ii) holds. By (122), θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ) so that ⟨u, η⟩ ∝ ⟨(σ_{1}^{♯}, ε_{1}^{♯}), ε_{2}^{♯}⟩ where u ∈ {caught, uncaught}. By Definition 6.5, if u = caught, then η ∝ ⟨σ_{1}^{♯}, ε_{1}^{♯}⟩ and, if u = uncaught, then η ∝ ε_{2}^{♯}. Hence, in both cases, η_{s} ∝ η_{s}^{♯}.

If r is an instance of rule (57), σ_{0} ∝ σ_{0}^{♯}; hence (θ_{[1]}, θ_{[1]}^{♯}) ∈ S and property (ii) holds. By (122), θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ) so that η ∝ ⟨σ_{2}^{♯}, ε_{2}^{♯}⟩. Hence η_{s} ∝ η_{s}^{♯}.

If r is an instance of (58) or (59), ⟨σ_{0}, ξ_{0}⟩ ∝ ⟨σ_{1}^{♯}, ξ_{1}^{♯}⟩; hence σ_{0} ∝ σ_{1}^{♯} and ξ_{0} ∝ ξ_{1}^{♯} so that (θ_{[1]}, θ_{[2]}^{♯}) ∈ S and property (ii) holds. By (122), θ_{[1]}(ϵ) ∝ θ_{[2]}^{♯}(ϵ). Thus, if (58) applies, σ_{1} ∝ ⟨σ_{3}^{♯}, ε_{3}^{♯}⟩ so that ⟨σ_{1}, ξ_{0}⟩ ∝ (σ_{3}^{♯} ⊗ ξ_{1}^{♯}); and, if (59) applies, ε ∝ ⟨σ_{3}^{♯}, ε_{3}^{♯}⟩ so that ε ∝ ε_{3}^{♯}. Hence, in both cases, η_{s} ∝ η_{s}^{♯}.

Function call. If r is an instance of one of rules (62)–(64), then 1 ≤ h ≤ 3 and ℓ = 3. Then the conditions (60) and (61) are also conditions for abstract rule (114). By hypothesis and Definition 6.1, (θ_{[0]}, θ_{[0]}^{♯}) ∈ S; by (122), θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ).

Table IV. Corresponding concrete and abstract rules and terminals for function bodies

B r r^{♯} η_{b} η_{b}^{♯} = ⟨(sval_{a}^{♯}, σ_{a}^{♯}), ε_{a}^{♯}⟩
(sval_{a}^{♯}, σ_{a}^{♯})  ε_{a}^{♯}
let d in s result e 65 115 ε  um_{s}^{♯}(σ_{2}^{♯}) ε_{3}^{♯} = ε_{0}^{♯}
66 um_{s}(ε) ⊔ um_{s}^{♯}(ε_{1}^{♯} ⊔ ε_{2}^{♯})
67  um_{s}(η_{0})
extern  68 116 σ_{0} | ⟨σ_{0}, ξ⟩ σ_{0}^{♯}  (σ_{0}^{♯}, ⊤)

If r is an instance of (62), then ε ∝ ε_{0}^{♯}, h = 1 and property (ii) holds. Hence η_{s} ∝ η_{s}^{♯}.

If r is an instance of (63), then σ_{0} ∝ σ_{0}^{♯} so that, by Definition 6.1, (θ_{[1]}, θ_{[1]}^{♯}) ∈ S; also, as h = 2, property (ii) holds. By (122), θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ) and ε ∝ ε_{1}^{♯}; by Definition 6.1, unmark_{s}(unlink_{s}(ε)) ∝ unmark_{s}^{♯}(unlink_{s}^{♯}(ε_{1}^{♯})). Hence η_{s} ∝ η_{s}^{♯}.

If r is an instance of (64), then σ_{1} ∝ σ_{1}^{♯} so that, by Definition 6.1, (θ_{[2]}, θ_{[2]}^{♯}) ∈ S; also, as h = 3, property (ii) holds. By (122), θ_{[2]}(ϵ) ∝ θ_{[2]}^{♯}(ϵ) and η_{2} ∝ ⟨σ_{2}^{♯}, ε_{2}^{♯}⟩; by Definition 6.1, unmark_{s}(η_{2}) ∝ ⟨unmark_{s}^{♯}(σ_{2}^{♯}), unmark_{s}^{♯}(ε_{2}^{♯})⟩. Hence η_{s} ∝ η_{s}^{♯}. 7.4 Function Bodies For this part of the proof, we use Table IV. By (121), N ∝ N^{♯}. Thus letting N = ⟨B, σ⟩ and N^{♯} = ⟨B, σ^{♯}⟩, by Definition 6.4, we have the implicit hypothesis σ ∝ σ^{♯}. We show using (82) in Definition 6.5, that η_{b} ∝ η_{b}^{♯}.

Suppose r is an instance of one of rules (65)–(67). By hypothesis and Definition 6.1, mark_{s}(σ) ∝ mark_{s}^{♯}(σ^{♯}), so that (θ_{[0]}, θ_{[0]}^{♯}) ∈ S. By (122), θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ).

If r is an instance of (65), ε ∝ ε_{0}^{♯}, h = 1 and property (ii) holds. Hence η_{b} ∝ η_{b}^{♯}. If r is an instance of (66), σ_{0} ∝ σ_{0}^{♯}; hence (θ_{[1]}, θ_{[1]}^{♯}) ∈ S and, as h = 2, prop-

erty (ii) holds. By (122), θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ) so that ε ∝ ε_{1}^{♯}. By Definition 6.1, unmark_{s}(ε) ∝ unmark_{s}^{♯}(ε_{1}^{♯}); hence η_{b} ∝ η_{b}^{♯}.

If r is an instance of (67), σ_{0} ∝ σ_{0}^{♯}; hence (θ_{[1]}, θ_{[1]}^{♯}) ∈ S. By (122) we have θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ), so that σ_{1} ∝ σ_{1}^{♯}; hence (θ_{[2]}, θ_{[2]}^{♯}) ∈ S; as h = 3, property (ii) holds. Again, by (122), θ_{[2]}(ϵ) ∝ θ_{[2]}^{♯}(ϵ); hence, η_{0} ∝ ⟨σ_{2}^{♯}, ε_{2}^{♯}⟩. By Definition 6.1, unmark_{s}(η_{0}) ∝ ⟨unmark_{s}^{♯}(σ_{2}^{♯}), unmark_{s}^{♯}(ε_{2}^{♯})⟩; hence η_{b} ∝ η_{b}^{♯}.

Suppose r is an instance of (68). Then σ = (μ, w) and σ_{0} = (μ_{0}, w). By the hypothesis, σ ∝ σ^{♯}; hence, by the side conditions, σ_{0} ∝ σ_{0}^{♯}; also, ξ ∝ ⊤, so that η_{b} ∝ η_{b}^{♯}. 7.5 Catch Clauses For this part of the proof, we use Table V. By (121), N ∝ N^{♯}. Thus, letting N = ⟨K, ε⟩ and N^{♯} = ⟨K, ε^{♯}⟩, by Definition 6.4, we have the implicit hypothesis ε ∝ ε^{♯}. We show using (83) in Definition 6.5, that η_{k} ∝ η_{k}^{♯}.

Catch. Let K have the form (p) s for some exception declaration p.

Suppose r is an instance of one of rules (69)–(71). Then, by the hypothesis and Definition 6.3, ε ∝ ϕ^{+}(p, ε^{♯}); by the side conditions for the abstract rules, ε ∝ ε_{0}^{♯}.

Table V. Corresponding concrete and abstract rules and terminals for catch clauses

K r r^{♯} η_{k} η_{k}^{♯} = ⟨η_{a}^{♯}, ε_{a}^{♯}⟩
η_{a}^{♯}  ε_{a}^{♯}
(any) s | (χ) s | (sT) s 69 117 ⟨caught, η_{0}⟩  η_{1}^{♯}  ε_{1}^{♯}
(id : sT) s  70 118 ⟨caught, um_{s}(ε_{0})⟩ (σ_{4}, ε_{4}) = (um_{s}^{♯}(σ_{3}^{♯}),  ε_{1}^{♯}
71  ⟨caught, η_{0}⟩  um_{s}^{♯}(ε_{2}^{♯}) ⊔ um_{s}^{♯}(ε_{3}^{♯}))
(χ) s | (sT) s  72 117 ⟨uncaught, (σ, ξ)⟩ η_{1}^{♯}  ε_{1}^{♯}
(id : sT) s  72 118 ⟨uncaught, (σ, ξ)⟩ (σ_{3}^{♯}, ε_{2}^{♯} ⊔ ε_{3}^{♯})  ε_{1}^{♯}
k_{0}; k_{1}  73 119 ⟨caught, η_{0}⟩  (σ_{0}^{♯} ⊔ σ_{1}^{♯}, ε_{0}^{♯} ⊔ ε_{2}^{♯})  ε_{3}^{♯}
74  η

If r is an instance of (69) then ε = (σ, ξ); by Definition 6.1, σ ∝ mem(ε_{0}^{♯}); Hence (θ_{[0]}, θ_{[0]}^{♯}) ∈ S and, as h = 1, property (ii) holds. By (122), θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ), which

implies η_{0} ∝ η_{1}^{♯} so that η_{k} ∝ η_{k}^{♯}.

If r is an instance of (70) or (71), then ε = (σ, sval) and type(sval) = sT; by Definition 6.1, σ ∝ mem(ε_{0}^{♯}) and sval ∝ sT(ε_{0}^{♯}). Hence, by Definition 6.1,

new_{s}(sval, mark_{s}(σ)) ∝ new_{s}^{♯}(sT(ε_{0}^{♯}), mark_{s}^{♯}(mem(ε_{0}^{♯}))) = ((σ_{2}^{♯}, i), ε_{2}^{♯}). (123)

If (70) applies, then h = 0, so that property (ii) holds trivially, and, by the side condition, ε_{0} = new_{s}(sval, mark_{s}(σ)) so that by (123), ε_{0} ∝ ε_{2}^{♯}; by Definition 6.1, unmark_{s}(ε_{0}) ∝ unmark_{s}^{♯}(ε_{2}^{♯}). If (71) applies, then, by the side condition, (σ_{0}, i) = new_{s}(sval, mark_{s}(σ)) so that by (123), σ_{0} ∝ σ_{2}^{♯}. Hence, (θ_{[0]}, θ_{[0]}^{♯}) ∈ S and, as h = 1,

property (ii) holds. By (122), θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ), which implies η_{0} ∝ ⟨σ_{3}^{♯}, ε_{3}^{♯}⟩. Thus, by

Definition 6.1, unmark_{s}(η_{0}) ∝ (unmark_{s}^{♯}(σ_{3}^{♯}), unmark_{s}^{♯}(ε_{2}^{♯})). Hence, in both cases, η_{k} ∝ η_{k}^{♯}.

If r is an instance of (72), then h = 0, so that property (ii) holds trivially. We have ε = (σ, ξ) and, by the side condition, p ∉ {ξ, cT, any}, where cT = type(ξ). If p ∈ {χ, sT} then abstract rule (117) applies so that, by the hypothesis, the side conditions and Definition 6.3, (σ, ξ) ∝ ϕ^{−}(p, ε^{♯}) = ε_{1}^{♯}. Similarly, if p = id : sT and abstract rule (118) applies, (σ, ξ) ∝ ϕ^{−}(sT, ε^{♯}) = ε_{1}^{♯}. Hence, in both cases, η_{k} ∝ η_{k}^{♯}.

Catch Sequence. If r is an instance of (73), then as h = 1 and (θ_{[0]}, θ_{[0]}^{♯}) ∈ S,

property (ii) holds. By (122), θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ), so that ⟨caught, η_{0}⟩ ∝ ⟨(σ_{0}^{♯}, ε_{0}^{♯}), ε_{1}^{♯}⟩.

By (83) in Definition 6.5, η_{0} ∝ (σ_{0}^{♯}, ε_{0}^{♯}), which implies η_{k} ∝ η_{k}^{♯}.

If r is an instance of (74), then (θ_{[0]}, θ_{[0]}^{♯}) ∈ S and, by (122), θ_{[0]}(ϵ) ∝ θ_{[0]}^{♯}(ϵ).

Thus, ⟨uncaught, ε_{0}⟩ ∝ ⟨(σ_{0}^{♯}, ε_{0}^{♯}), ε_{1}^{♯}⟩, so that, by (83) in Definition 6.5, ε_{0} ∝ ε_{1}^{♯}. Hence (θ_{[1]}, θ_{[1]}^{♯}) ∈ S and, as h = 2, property (ii) holds. By (122), θ_{[1]}(ϵ) ∝ θ_{[1]}^{♯}(ϵ),

so that η ∝ ⟨(σ_{1}^{♯}, ε_{2}^{♯}), ε_{3}^{♯}⟩, which implies η_{k} ∝ η_{k}^{♯}.

A few observations regarding the precision of the proposed approximations are in order. Consider an abstract tree θ^{♯} ∈ Θ^{♯} such that θ^{♯}(ϵ) = (ρ ⊢_{β} N^{♯} → η^{♯}), where N^{♯} ∈ Γ_{s}^{β♯} and η^{♯} ∈ T_{s}^{♯}. If the concretization functions relating the concrete and abstract domains are strict, then the abstract tree above will encode the following definite information:

—non-terminating computations (i.e., unreachable code), if η^{♯} = ⊥;

—non-exceptional computations, if η^{♯} = ⟨σ^{♯}, none^{♯}⟩ and σ^{♯} ≠ ⊥;

—exceptional computations, if η^{♯} = ⟨⊥, ε^{♯}⟩ and ε^{♯} ≠ none^{♯}.

Obviously, a precise propagation of this definite information requires that all of the abstract domain operators are strict too. Hence, if θ^{♯}(ϵ) = (ρ ⊢_{β} ⟨s, ⊥⟩ → η^{♯}), we will also have η^{♯} = ⊥. Similar properties hold when considering expressions, declarations and catch clauses.

8. COMPUTING ABSTRACT TREES

The results of the previous section (Theorems 7.2 and 7.3) guarantee that each concrete tree can be safely approximated by an abstract tree, provided the nonterminal configurations in the roots satisfy the approximation relation.

For expository purposes, suppose we are interested in a whole-program analysis. For each (concrete and abstract) pair of initial memories satisfying σ_{i} ∝ σ_{i}^{♯} and each g_{0} = (g; gvar \underline{x} : integer = 0), where g is a valid program, we obtain that any abstract tree θ_{0}^{♯} ∈ Θ^{♯} such that θ_{0}^{♯}(ϵ) = (∅ ⊢_{∅} ⟨g_{0}, σ_{i}^{♯}⟩ → η_{0}^{♯}) correctly approximates each concrete tree θ_{0} ∈ Θ such that θ_{0}(ϵ) = (∅ ⊢_{∅} ⟨g_{0}, σ_{i}⟩ → η_{0}). Notice that θ_{0}^{♯} is a finite tree. Letting η_{0}^{♯} = ⟨(ρ_{0}, σ_{0}^{♯}), ε_{0}^{♯}⟩ and assuming η_{0} ∉ ExceptState, we obtain η_{0} = ⟨ρ_{0}, σ_{0}⟩, where σ_{0} ∝ σ_{0}^{♯}. Hence, letting s_{0} = (\underline{x} := main(□)) and ρ_{0} : β, any abstract tree θ_{1}^{♯} ∈ Θ^{♯} such that θ_{1}^{♯}(ϵ) = (ρ_{0} ⊢_{β} ⟨s_{0}, σ_{0}^{♯}⟩ → η_{1}^{♯}) correctly approximates each concrete tree θ_{1} ∈ Θ such that either θ_{1}(ϵ) = (ρ_{0} ⊢_{β} ⟨s_{0}, σ_{0}⟩ → η_{1}) or θ_{1}(ϵ) = (ρ_{0} ⊢_{β} ⟨s_{0}, σ_{0}⟩ ⟶^{∞}). We are thus left with the problem of computing (any) one of these abstract trees, which are usually infinite. In particular, we are interested in choosing θ_{1}^{♯} in a subclass of trees admitting finite representations and, within this class, in maintaining a level of accuracy that is compatible with the complexity/precision trade-off dictated by the application.

A classical choice is to restrict attention to rational trees, that is, trees with only finitely many subtrees: the algorithm sketched in [Sch95; Sch97; Sch98], which assumes that the abstract domain is Noetherian (i.e., all of its ascending chains are finite), guides the analysis toward the computation of a rational tree by forcing each infinite path to contain a repetition node. Here below we describe a variation, also working for abstract domains that admit infinite ascending chains, that exploits widening operators [CC76; CC77a; CC92b].

Definition 8.1. (Widening operators.) Let (D^{♯}, ⊑, ⊥, ⊔) be an abstract domain. The partial operator ∇: D^{♯} × D^{♯} ↣ D^{♯} is a widening if:

—for all x^{♯}, y^{♯} ∈ D^{♯}, y^{♯} ⊑ x^{♯} implies that y^{♯} ∇ x^{♯} is defined and x^{♯} ⊑ y^{♯} ∇ x^{♯};

—for all increasing chains x_{0}^{♯} ⊑ x_{1}^{♯} ⊑ ⋯, the increasing chain defined by y_{0}^{♯} =^{def} x_{0}^{♯} and y_{i+1}^{♯} =^{def} y_{i}^{♯} ∇ (y_{i}^{♯} ⊔ x_{i+1}^{♯}), for i ∈ ℕ, is not strictly increasing.

The algorithm works by recursively constructing a finite approximation for the abstract subtree rooted in the current node (initially, the root of the whole tree). Let n = (ρ ⊢_{β} ⟨q, y_{n}^{♯}⟩ → r_{n}) be the current node, where q is a uniquely labeled program phrase,^{10} y^{♯} ∈ D^{♯} is either an abstract memory σ^{♯} ∈ Mem^{♯} or an abstract exception state ε^{♯} ∈ ExceptState^{♯}, and r_{n} is a placeholder for the “yet to be computed” conclusion. The node n is processed according to the following alternatives.

(i) If no ancestor of n is labeled by the program phrase q, the node has to be expanded using an applicable abstract rule instance. Namely, descendants of the premises of the rule are (recursively) processed, one at a time and from left to right. When the expansion of all the premises has been completed, including the case when the rule has no premise at all, the marker r_{n} is replaced by an abstract value computed according to the conclusion of the rule.

(ii) If there exists an ancestor node m = (ρ ⊢_{β} ⟨q, y_{m}^{♯}⟩ → r_{m}) of n labeled by the same program phrase q and such that y_{n}^{♯} ⊑ y_{m}^{♯}, i.e., if node n is subsumed by node m, then the node is not expanded further and the placeholder r_{n} is replaced by the least fixpoint of the equation r_{n} = f_{m}(r_{n}), where f_{m} is the expression corresponding to the conclusion of the abstract rule that was used for the expansion of node m.^{11} Intuitively, an infinite subtree rooted in node m has been identified and the “repetition node” n is transformed to a back edge to the root m of this subtree.

(iii) Otherwise, there must be an ancestor node m = (ρ ⊢_{β} ⟨q, y_{m}^{♯}⟩ → r_{m}) of n labeled by the same program phrase q, but the subsumption condition y_{n}^{♯} ⊑ y_{m}^{♯} does not hold. Then, to ensure convergence, the abstract element y_{n}^{♯} in node n is further approximated by y_{m}^{♯} ∇ (y_{m}^{♯} ⊔ y_{n}^{♯}) and we proceed as in case (i).

Termination of the algorithm can be proved thanks to the following observations: an infinite abstract tree necessarily has infinite paths (since the tree is finitely branching); each infinite path necessarily has an infinite number of nodes labeled by the same program phrase (since the set of program phrases is finite); the application of case (iii) leads to the computation, along each infinite path, of increasing chains of abstract elements and, by Definition 8.1, these chains are necessarily finite; hence, case (ii) is eventually applied to all infinite paths, leading to a finite representation of the rational tree where all the infinite paths are expressed by using back edges.

It should be stressed that, as far as efficiency is concerned, the algorithm outlined above can be improved by the adoption of well studied memoization techniques; as noted in [Sch97], by clearly separating design concerns from implementation concerns, the adopted methodology produces simpler proofs of correctness. Also note that the choice of the widening operator has a deep impact on the precision of the results obtained and, moreover, even a precise widening can lead to inaccurate results if applied too eagerly. However, precision problems can be mitigated by the application of suitable “widening delay” techniques [CC92b; HPR97; BHRZ05].

10Unique labels (e.g., given by the address of the root node for q in the program parse tree) ensure that different occurrences of the same syntax are not confused [Sch95]; this also means that, in each node n, the type and execution environments ρ and β are uniquely determined by q. 11As explained in [Sch95; Sch97; Sch98], the computation of such a least fixpoint (in the context of a coinductive interpretation of the abstract rules) is justified by the fact that here we only need to approximate the conclusions produced by the terminating concrete computations, i.e., by the concrete rules that are interpreted inductively. Also note that the divergence rules have no conclusion at all.

9. EXTENSIONS

In this section we outline how the techniques presented in the first part of the paper can be extended so as to encompass the C language and all the imperative aspects of C^{++} (including, of course, exceptions): Section 9.1 shows how the set of primitive types can be extended by discussing the introduction of bounded integer and floating-point types; Section 9.2 provides a sketch of how C-like pointers, arrays and records can be dealt with; dynamic memory allocation and deallocation is treated in Section 9.3; and Section 9.4 illustrates how all the non-structured control flow mechanisms of C and C^{++} can be accounted for.

Once an ABI (Application Binary Interface) has been fixed and its characteristics have been reflected into concrete and abstract memory structures, C struct and union compound types can be accommodated, even in presence of pointer casts and unrestricted pointer arithmetics, by compiling down all their uses to memory reads and writes performed through pointer dereferencing [Min06].

While we have not yet tried to incorporate object-oriented features (like classes, inheritance, method calls with dynamic binding and so forth) we do not see what, in the current design, would prevent such an extension.

9.1 Additional Arithmetic Types

The addition of more arithmetic types such as (signed and unsigned) finite integer and floating-point types is fairly straightforward. It is assumed that a preprocessor will add, as needed, a value cast operator that, for a given numeric type and constant expression, ensures that either the returned value is in the domain of that type or an appropriate exception is thrown. With this assumption, all the operations need only to be specified for operands of the very same type.

9.1.1 Syntax. For floating-point numbers, we add a new basic type float that represents a fixed and finite subset of the reals together with a set of special values denoting infinities, NaN (Not a Number) value and so forth. The exact format and range of a floating-point literal is unspecified. The addition of other floating-point types to represent double and extended precision numbers can be done the same way. To exemplify the inclusion of signed and unsigned bounded integer types, we also add the signed char and unsigned char basic types.

Integer types. iT ∈ iType =^{def} {integer, signed char, unsigned char, …};

Numeric types. nT ∈ nType =^{def} iType ∪ {float, …};

Basic types. T ∈ Type =^{def} nType ∪ {boolean};

Floating-point literals. fl ∈ Float;

Signed char literals. sc ∈ sChar;

Unsigned char literals. uc ∈ uChar.

Expressions and constants. Expressions are extended with floating-point constants, bounded integer constants, and vcast, a value cast operator for converting values from one basic type to another, when possible, or yielding an appropriate exception:

Exp ∋ e ::= … | fl | sc | uc | vcast(nT, e)
Con ∋ con ::= … | fl | sc | uc.

The functions dom: cType → {Integer, Bool, RTSExcept, Float, sChar, uChar} and type: sVal ↣ sType are easily extended:

dom(float) =^{def} Float,  type(fl) =^{def} float,
dom(signed char) =^{def} sChar,  type(sc) =^{def} signed char,
dom(unsigned char) =^{def} uChar,  type(uc) =^{def} unsigned char.

9.1.2 Static Semantics. The required adjustments to functions FI and DI are straightforward and thus omitted. Then, we add the following static semantic rules, where ⧇ ∈ {+, −, ∗, /, %} and ⧆ ∈ {=, ≠, <, ≤, ≥, >}:

Expressions.

β ⊢_{I} fl : float  β ⊢_{I} sc : signed char

{β ⊢_{I} e : nT \atop β ⊢_{I} −e : nT}  β ⊢_{I} uc : unsigned char

{β ⊢_{I} e_{0} : nT β ⊢_{I} e_{1} : nT \atop β ⊢_{I} e_{0} ⧇ e_{1} : nT} β ⊢_{I} e_{0} : nT β ⊢_{I} e_{1} : nT

β ⊢_{I} e_{0} ⧆ e_{1} : boolean
β ⊢_{I} e : T_{0}
if casting T_{0} to T_{1} is legal.

β ⊢_{I} vcast(T_{1}, e) : T_{1}

9.1.3 Concrete Dynamic Semantics. The added numeric types and the operations upon them bring in a considerable degree of complexity. Consider the C language, for example: unsigned bounded integers employ modular arithmetic; for signed bounded integers, overflow yields undefined behavior; the results of floatingpoint operations depend on the rounding mode in effect and on the settings that cause floating-point exceptions to be trapped or ignored; relational operators may or may not raise a floating-point exception when one or both arguments are NaN. In order to factor out these details and delegate them to the memory structure, we resort to a device like the one used to model supported and unsupported language elements in the abstract semantics. We thus postulate the existence of the partial functions

eval_{vc} : (nType × Con × Mem) ↣ ValState ⊎ ExceptState,
eval_{−_{1}} : (Con × Mem) ↣ ValState ⊎ ExceptState,
eval_{⧇}: (Con × Con × Mem) ↣ ValState ⊎ ExceptState,
eval_{⧆}: (Con × Con × Mem) ↣ ValState ⊎ ExceptState,

that model the cast operator, unary minus, binary operators ⧇ ∈ {+, −, ∗, /, %} and relational operators ⧆ ∈ {=, ≠, <, ≤, ≥, >}, respectively. Such functions need not be always defined: for example, there is no need to define eval_{+}(con_{0}, con_{1}, σ) for the case type(con_{0}) ≠ type(con_{1}).

Value casts. The following concrete rule schemata use the corresponding evaluation function to specify the execution of the vcast operator.

{ρ ⊢_{β} ⟨e, σ⟩ → ε \atop ρ ⊢_{β} ⟨vcast(nT, e), σ⟩ → ε} ρ ⊢_{β} ⟨e, σ⟩ → ⟨con, σ_{0}⟩

ρ ⊢_{β} ⟨vcast(nT, e), σ⟩ → eval_{vc}(nT, con, σ_{0})

Arithmetic evaluation. By using the evaluation functions, we can substitute rules (5), (8) and (9) with the following (note that they also capture the case when a divide-by-zero exception is thrown):

ρ ⊢_{β} ⟨e, σ⟩ → ⟨con, σ_{0}⟩

ρ ⊢_{β} ⟨−e, σ⟩ → eval_{−_{1}}(nT, con, σ_{0})

ρ ⊢_{β} ⟨e_{0}, σ⟩ → ⟨con_{0}, σ_{0}⟩ ρ ⊢_{β} ⟨e_{1}, σ_{0}⟩ → ⟨con_{1}, σ_{1}⟩

ρ ⊢_{β} ⟨e_{0} ⧇ e_{1}, σ⟩ → eval_{⧇}(con_{0}, con_{1}, σ_{1})

Arithmetic tests. Similarly, rule (12) is replaced by the more general rule

ρ ⊢_{β} ⟨e_{0}, σ⟩ → ⟨con_{0}, σ_{0}⟩ ρ ⊢_{β} ⟨e_{1}, σ_{0}⟩ → ⟨con_{1}, σ_{1}⟩

ρ ⊢_{β} ⟨e_{0} ⧆ e_{1}, σ⟩ → eval_{⧆}(con_{0}, con_{1}, σ_{1})

9.2 C-like Pointers, Arrays and Records

9.2.1 Syntax. Recall that in Sections 3 and 4 we defined the set of storable types, whose values can be read from and written to memory, and the set of denotable types, that can occur in declarations. The introduction of pointer, array and record types requires the adoption of a finer classification. The set of all memory types is partitioned into object types and function types: the latter differ in that we cannot read or update the “value” of a function; rather, we execute it. Object types are further partitioned into elementary types (also called scalar types, including basic types and pointer types) and aggregate types (arrays and records). All the elementary types are storable, meaning that their values can be read directly from or written directly to memory, as well as passed to and returned from functions. Regarding aggregate types, the C language prescribes that record types are storable, whereas array types are not. Pointer, array and record type derivations can be applied repeatedly to obtain, e.g., multi-dimensional arrays.

Types.

eType ∋ eT ::= T | pT  oType ∋ oT ::= sT | aT
pType ∋ pT ::= mT∗  fType ∋ fT ::= fps → sT
sType ∋ sT ::= eT | rT  mType ∋ mT ::= oT | fT
aType ∋ aT ::= array m of oT  dType ∋ dT ::= mT loc
rType ∋ rT ::= record id of id_{1} : oT_{1}, …, id_{j} : oT_{j}

We assume, without loss of generality, that the field names of record types are unique across the entire program (for example, id_{1}, …, id_{j} could contain id as some kind of special prefix).

Identifiers are no longer the only way to denote a memory structure location. This can also be referred to by combining a pointer with the indirection operator ‘∗’, an array with the indexing operator, or a record with the field selection operator. Hence, we introduce the concept of lvalue, which can be read as “location-valued expression.”

Offsets and lvalues.

Offset ∋ o ::= □ | [e] · o | . id · o LValue ∋ lval ::= id · o | (∗ e) · o

Consequently, the syntactic production for expressions generating identifiers, as well as the productions for statements generating assignments and function calls, are replaced by more general versions using lvalues; expressions and declarations are also extended with the address-of operator, null pointers and array variables.

Expressions, declarations and statements.

Exp ∋ e ::= … | val lval | & lval | (pT) 0  Glob ∋ g ::= … | gvar id : aT = e
Stmt ∋ s ::= … | lval := e | lval := e(es)  Decl ∋ d ::= … | lvar id : aT = e

9.2.2 Static Semantics. The required adjustments to functions FI and DI are straightforward and thus omitted. The well-typedness of offsets and lvalues is encoded by the following predicates:

β, dT_{0} ⊢_{I} o : dT_{1},  o is compatible with dT_{0} and has type dT_{1} in β;
β ⊢_{I} lval : dT,  lval is well-formed and has type dT in β.

The static semantics is thus extended by the following rules.^{12} Note that the evaluation of an lvalue as an expression —val lval— causes a suitable type conversion, sometimes referred to as “type decay.” Pointer arithmetics can only be applied to object types. In function calls, the callee is specified via an expression having function pointer type (typically resulting from a type decay).

Offset.

β, dT ⊢_{I} □ : dT

β ⊢_{I} e : integer β, oT loc ⊢_{I} o : dT
β, (array m of oT) loc ⊢_{I} [e] · o : dT
β, oT_{i} loc ⊢_{I} o : dT
\overline{if i ∈ \{1, …, j\}}

β, (record id of id_{1} : oT_{1}; …; id_{j} : oT_{j}) loc ⊢_{I} . id_{i} · o : dT

Lvalue.

β, dT_{0} ⊢_{I} o : dT_{1}

\overline{if β(id) = dT_{0}}

β ⊢_{I} id · o : dT_{1}

β ⊢_{I} e : mT ∗ β, mT loc ⊢_{I} o : dT
β ⊢_{I} (∗ e) · o : dT

Null pointer and address-of operator.

β ⊢_{I} (pT) 0 : pT

β ⊢_{I} lval : mT loc
β ⊢_{I} & lval : mT∗

12The previous rules for identifier, assignment and function call are no longer used.

Type decay.

β ⊢_{I} lval : sT loc

β ⊢_{I} val lval : sT β ⊢_{I} lval : (array m of oT) loc

β ⊢_{I} val lval : oT∗

β ⊢_{I} lval : fT loc
β ⊢_{I} val lval : fT∗

Pointer arithmetics.

β ⊢_{I} e_{0} : oT ∗ β ⊢_{I} e_{1} : integer

β ⊢_{I} e_{0} + e_{1} : oT∗

β ⊢_{I} e_{0} : integer β ⊢_{I} e_{1} : oT∗
β ⊢_{I} e_{0} + e_{1} : oT∗

β ⊢_{I} e_{0} : oT ∗ β ⊢_{I} e_{1} : integer

β ⊢_{I} e_{0} − e_{1} : oT∗

β ⊢_{I} e_{0} : oT ∗ β ⊢_{I} e_{1} : oT∗
β ⊢_{I} e_{0} − e_{1} : integer

Pointer comparison.

β ⊢_{I} e_{0} : pT β ⊢_{I} e_{1} : pT

\overline{where ⧆ ∈ \{=, ≠, <, ≤, ≥, >\}.}
β ⊢_{I} e_{0} ⧆ e_{1} : boolean

Assignment and function call.

β ⊢_{I} lval : sT loc β ⊢_{I} e : sT

β ⊢_{I} lval := e

β ⊢_{I} lval : sT loc β ⊢_{I} e : (fps → sT) ∗ β, fps ⊢_{I} es

β ⊢_{I} lval := e(es)

(Multi-dimensional) Global array declaration.

β ⊢_{I} gvar id : oT = e : {id ↦ oT loc}
\overline{if m > 0}

β ⊢_{I} gvar id : array m of oT = e : {id ↦ (array m of oT) loc}

The static semantics rule for a local array declaration is similar.

9.2.3 Concrete Dynamic Semantics. Concrete execution environments now map function identifiers to (properly typed) locations, rather than function abstracts: hence, we redefine dVal =^{def} Addr × mType.

A proper handling of aggregate and function types in memory structures requires a few semantic adjustments and extensions. New memory functions allow the allocation of function abstracts in the text segment, as well as the contiguous allocation of a number of memory cells, so as to model (multi-dimensional) arrays:

new_{t} : (Abstract × Mem) → ((Mem × Loc) ⊎ ExceptState),
newarray_{d} : (Integer × ValState) → ((Mem × Loc) ⊎ ExceptState),
newarray_{s} : (Integer × ValState) → ((Mem × Ind) ⊎ ExceptState).

It can be observed that the properties stated in Definition 5.2 still hold as long as we consider locations having non-aggregate type and properly extend the domain and codomain of the absolute memory map:

Map =^{def} (Loc × (eType ⊎ fType)) ↣ (Con ⊎ Loc ⊎ Abstract).

These “elementary” memory maps need to be extended to read or update record values. To this end, we assume the existence of a couple of helper functions working on locations having aggregate type:

locfield: (Id × Loc × rType) ↣ (Loc × oType),
locindex: (Integer × Loc × aType) ↣ (Loc × oType).

Intuitively, when defined, these functions map a record (resp., array) typed location to the typed location of one of its record fields (resp., array elements). Hence, for each μ ∈ Map, the extension μ: (Loc × sType) ↣ sVal can be recursively obtained, for each l ∈ Loc and rT = record id of id_{1} : oT_{1}; …; id_{j} : oT_{j}, as follows and under the following conditions:

μ(l, rT) =^{def} ⟨μ(locfield(id_{1}, l, rT)), …, μ(locfield(id_{j}, l, rT))⟩,

where, for each l ∈ Loc and aT = array m of oT ∈ aType,

μ(l, aT) =^{def} [μ(locindex(0, l, aT)), …, μ(locindex(m − 1, l, aT))].

A similar extension is required for the memory update operator. Note that we will still use υ as a syntactic meta-variable for ValState = sVal × Mem, but now its first component can be either a constant, or an absolute location, or a record value.

Pointer and array indexing errors are modeled via RTS exceptions. It is assumed there exists a special location l_{null} ∈ Loc (the null pointer value) such that (l_{null}, mT) ∉ dom(σ) for all σ ∈ Mem and mT ∈ mType; this also implies that l_{null} cannot be returned by the memory allocation operators. Hence, any attempt to read from or write to memory through this location will result in an exception state. Suitable operators on memory structures are required to check the constraints regarding pointer arithmetics (e.g., out-of-bounds array accesses), pointer comparisons (where ⧆ ranges over {=, ≠, <, ≤, ≥, >}) and to perform “array-to-pointer decay” conversions or record field selections:

ptrmove: (Integer × Loc × Mem) → ValState ⊎ ExceptState,
ptrdiff : (Loc × Loc × Mem) → ValState ⊎ ExceptState,
ptrcmp_{⧆}: (Loc × Loc × Mem) → ValState ⊎ ExceptState,
firstof : (Loc × Mem) → ValState ⊎ ExceptState,
field: (Id × Loc × Mem) → ValState ⊎ ExceptState.

Note that array indexing is semantically equivalent to a suitable combination of type decay, pointer arithmetics and pointer indirection. Nonetheless, for the sake of clarity and also to simplify the application of pointer and array dependence analyses [EGH94], we keep the distinction of the two constructs and, to simplify notation, we define^{13}

index: (Loc × ValState) ↣ ValState ⊎ ExceptState

as follows:

index(l, (m, σ)) =^{def} \begin{cases}ε, & if firstof(l, σ) = ε; \\ ptrmove(m, l_{0}, σ_{0}), & if firstof(l, σ) = (l_{0}, σ_{0}). \end{cases}

13Functions ‘field’ and ‘index’ are similar to ‘locfield’ and ‘locindex’, but they are also meant to check their arguments against the memory structure, possibly returning an RTS exception.

Non-terminal and terminal configurations are extended so as to allow for the syntactic categories of offsets and lvalues, whose non-exceptional evaluation leads to a location:

Γ_{o}^{β} =^{def} \{ ⟨o, l, σ⟩ ∈ Offset × Loc × Mem | \begin{matrix}∃dT_{0}, dT_{1} ∈ dType . \\ β, dT_{0} ⊢_{I} o : dT_{1} \end{matrix} \},
Γ_{l}^{β} =^{def} { ⟨lval, σ⟩ ∈ LValue × Mem | ∃dT ∈ dType . β ⊢_{I} lval : dT },
T_{o} =^{def} T_{l} =^{def} (Loc × Mem) ⊎ ExceptState,

The dynamic concrete semantics is extended with the following rule schemata.

Offset.

ρ ⊢_{β} ⟨□, l, σ⟩ → ⟨l, σ⟩

ρ ⊢_{β} ⟨e, σ⟩ → ε ; ρ ⊢_{β} ⟨[e] · o, l, σ⟩ → ε  ρ ⊢_{β} ⟨e, σ⟩ → υ ; \overline{if index(l, υ) = ε} ; ρ ⊢_{β} ⟨[e] · o, l, σ⟩ → ε

ρ ⊢_{β} ⟨e, σ⟩ → υ ρ ⊢_{β} ⟨o, l_{0}, σ_{0}⟩ → η

\overline{if index(l, υ) = (l_{0}, σ_{0})}
ρ ⊢_{β} ⟨[e] · o, l, σ⟩ → η
if field(id_{i}, l, σ) = ε

ρ ⊢_{β} ⟨. id_{i} · o, l, σ⟩ → ε

ρ ⊢_{β} ⟨o, l_{0}, σ_{0}⟩ → η

if field(id_{i}, l, σ) = (l_{0}, σ_{0})

ρ ⊢_{β} ⟨. id_{i} · o, l, σ⟩ → η

Lvalue. ρ ⊢_{β} ⟨o, σ @ a, σ⟩ → η

\overline{if ρ(id) = (a, mT)}

ρ ⊢_{β} ⟨id · o, σ⟩ → η

ρ ⊢_{β} ⟨e, σ⟩ → ε ; ρ ⊢_{β} ⟨(∗ e) · o, σ⟩ → ε  ρ ⊢_{β} ⟨e, σ⟩ → ⟨l_{0}, σ_{0}⟩ ρ ⊢_{β} ⟨o, l_{0}, σ_{0}⟩ → η ; ρ ⊢_{β} ⟨(∗ e) · o, σ⟩ → η

Null pointer and address-of operator.

ρ ⊢_{β} ⟨(pT) 0, σ⟩ → ⟨l_{null}, σ⟩

ρ ⊢_{β} ⟨lval, σ⟩ → η
ρ ⊢_{β} ⟨& lval, σ⟩ → η

Type decay.

ρ ⊢_{β} ⟨lval, σ⟩ → ε

ρ ⊢_{β} ⟨val lval, σ⟩ → ε

ρ ⊢_{β} ⟨lval, σ⟩ → ⟨l, σ_{0}⟩

if β ⊢_{FI(lval)} lval : sT loc

ρ ⊢_{β} ⟨val lval, σ⟩ → σ_{0}[l, sT]

ρ ⊢_{β} ⟨lval, σ⟩ → υ
if β ⊢_{FI(lval)} lval : aT loc

ρ ⊢_{β} ⟨val lval, σ⟩ → firstof(υ) ρ ⊢_{β} ⟨lval, σ⟩ → υ

if β ⊢_{FI(lval)} lval : fT loc

ρ ⊢_{β} ⟨val lval, σ⟩ → υ

Pointer arithmetics. Let ⧇ denote a binary abstract syntax operator in {+, −}, as well as the corresponding unary operation on integers. Then, the following are added to rule schemata (6)–(9).

{ρ ⊢_{β} ⟨e_{0}, σ⟩ → ⟨l, σ_{0}⟩ ρ ⊢_{β} ⟨e_{1}, σ_{0}⟩ → ε \atop ρ ⊢_{β} ⟨e_{0} ⧇ e_{1}, σ⟩ → ε}

ρ ⊢_{β} ⟨e_{0}, σ⟩ → ⟨l, σ_{0}⟩ ρ ⊢_{β} ⟨e_{1}, σ_{0}⟩ → ⟨m, σ_{1}⟩

\overline{if m_{0} = ⧇ m}
ρ ⊢_{β} ⟨e_{0} ⧇ e_{1}, σ⟩ → ptrmove(m_{0}, l, σ_{1})

{ρ ⊢_{β} ⟨e_{0}, σ⟩ → ⟨m, σ_{0}⟩ ρ ⊢_{β} ⟨e_{1}, σ_{0}⟩ → ⟨l, σ_{1}⟩ \atop ρ ⊢_{β} ⟨e_{0} + e_{1}, σ⟩ → ptrmove(m, l, σ_{1})}

{ρ ⊢_{β} ⟨e_{0}, σ⟩ → ⟨l_{0}, σ_{0}⟩ ρ ⊢_{β} ⟨e_{1}, σ_{0}⟩ → ⟨l_{1}, σ_{1}⟩ \atop ρ ⊢_{β} ⟨e_{0} − e_{1}, σ⟩ → ptrdiff(l_{0}, l_{1}, σ_{1})}

Pointer comparison. Let ⧆ denote a binary abstract syntax operator in the set {=, ≠, <, ≤, ≥, >}. Then, the following are added to rule schemata (10)–(12).

{ρ ⊢_{β} ⟨e_{0}, σ⟩ → ⟨l, σ_{0}⟩ ρ ⊢_{β} ⟨e_{1}, σ_{0}⟩ → ε \atop ρ ⊢_{β} ⟨e_{0} ⧆ e_{1}, σ⟩ → ε}

{ρ ⊢_{β} ⟨e_{0}, σ⟩ → ⟨l_{0}, σ_{0}⟩ ρ ⊢_{β} ⟨e_{1}, σ_{0}⟩ → ⟨l_{1}, σ_{1}⟩ \atop ρ ⊢_{β} ⟨e_{0} ⧆ e_{1}, σ⟩ → ptrcmp_{⧆}(l_{0}, l_{1}, σ_{1})}

Assignment.

ρ ⊢_{β} ⟨lval, σ⟩ → ε

ρ ⊢_{β} ⟨lval := e, σ⟩ → ε

ρ ⊢_{β} ⟨lval, σ⟩ → (l, σ_{0}) ρ ⊢_{β} ⟨e, σ_{0}⟩ → ε
ρ ⊢_{β} ⟨lval := e, σ⟩ → ε

ρ ⊢_{β} ⟨lval, σ⟩ → (l, σ_{0}) ρ ⊢_{β} ⟨e, σ_{0}⟩ → ⟨sval, σ_{1}⟩

\overline{if β ⊢_{FI(e)} e : sT}
ρ ⊢_{β} ⟨lval := e, σ⟩ → σ_{1}[(l, sT) := sval]

Similar changes are required for the case of a function call. First, the lvalue is evaluated so as to obtain the target location where the result of the function call will be stored; then, the function designator (an expression) is evaluated to obtain a location having function type; this location is fed to the memory structure so as to obtain the function abstract. All the other computation steps, including parameter passing, are performed as before. On exit from the function call, the return value is stored at the location computed in the first step. Exceptions are eventually detected and propagated as usual. Also note that, thanks to the rules for type decay, arrays and functions can be passed to and returned from function calls.

(Multi-dimensional) Global array declaration. In the following rule schemata, let n > 0, aT = array m_{1} of (… (array m_{n} of sT) …) and m = m_{1} × … × m_{n}.

ρ ⊢_{β} ⟨e, σ⟩ → η
ρ ⊢_{β} ⟨gvar id : aT = e, σ⟩ → cleanup_{d}(ε)

if either η = ε, or η = υ and newarray_{d}(m, υ) = ε;

ρ ⊢_{β} ⟨e, σ⟩ → υ
ρ ⊢_{β} ⟨gvar id : aT = e, σ⟩ → ⟨ρ_{0}, σ_{0}⟩

if newarray_{d}(m, υ) = (σ_{0}, l) and ρ_{0} = {id ↦ (l, aT)}.

The rules for local array declaration are similar. Since function abstracts are now stored in memory structures, a few minor adaptations, omitted for space reasons, are also required for the rule of function declarations (which uses new_{t}) and the rules for recursive environments and declarations.

9.3 Heap Memory Management

By adding a heap segment to memory structures, as well as suitable helper functions (new_{h}, delete_{h} and the corresponding array versions), it is possible to further extend the language to embrace dynamic memory allocation and deallocation.

9.3.1 Syntax. We add an allocation expression and a deallocation statement:

Exp ∋ e ::= … | new sT = e
Stmt ∋ s ::= … | delete e

9.3.2 Static Semantics.

β ⊢_{I} e : sT

β ⊢_{I} new sT = e : sT∗

β ⊢_{I} e : sT∗ ; β ⊢_{I} delete e

9.3.3 Concrete Dynamic Semantics. This is extended with the schemata:

New expression.

{ρ ⊢_{β} ⟨e, σ⟩ → ε \atop ρ ⊢_{β} ⟨new sT = e, σ⟩ → ε} ρ ⊢_{β} ⟨e, σ⟩ → υ

\overline{if new_{h}(υ) = ε}
ρ ⊢_{β} ⟨new sT = e, σ⟩ → ε
ρ ⊢_{β} ⟨e, σ⟩ → υ
\overline{if new_{h}(υ) = (σ_{0}, l)}

ρ ⊢_{β} ⟨new sT = e, σ⟩ → ⟨l, σ_{0}⟩

Delete operator.

{ρ ⊢_{β} ⟨e, σ⟩ → ε \atop ρ ⊢_{β} ⟨delete e, σ⟩ → ε} ρ ⊢_{β} ⟨e, σ⟩ → υ

ρ ⊢_{β} ⟨delete e, σ⟩ → delete_{h}(υ)

Similar rules allow for allocation and deallocation of an array on the heap: note that, contrary to the previous cases, the dimensions of the array can be specified as expressions that will be evaluated dynamically.

Regarding the abstract semantics, the extensions concerning C-like pointers and arrays as well as heap memory management can be obtained along the lines followed in Section 6. In particular, the new memory structure operators described above are provided with safe approximations and a new abstract domain Loc^{♯} for locationvalued expressions has to be defined. By generalizing the abstract memory read and update operators so as to take as input an abstract location, we realize the so-called weak read and weak update operators, so as to correctly deal with, e.g., assignments or function calls whose target is not statically known. In practice, no fundamentally new issue has to be solved as far as the specification of the abstract interpreter is concerned. This is not to say that these extensions are trivial; rather, the real issues (e.g., the efficient and accurate tracking of aliasing information for pointers [Ema93; EGH94] or the appropriate summarization techniques for large arrays [GRS05] and heap-allocated data [GDD^{+}04; SRW02]) are orthogonal to the current approach and should be addressed elsewhere.

9.4 Non-Structured Control Flow Mechanisms

It turns out that the approach we have chosen to model exceptional behavior of programs can be easily generalized so as to capture all the non-structured control flow mechanisms of languages such as C and C^{++}. To exemplify such a generalization, the abstract syntax of commands is extended with branching and labeled statements:

Label ∋ l ::= id | m | default
Stmt ∋ s ::= … | goto id | switch e in s | break | continue | return e | l : s

We assume that the static semantics ensures the labels used in a function body are all distinct (if the language supports local labels, then a trivial renaming will be required) and that every goto has access to a corresponding labeled statement, respecting the constraints imposed by the language (concerning, for instance, jumping into and outside blocks).

The state of a computation is captured, besides the current program point, by a control mode and a memory structure, which together constitute what we call a control state. A control state is classified by the corresponding control mode in either a plain execution state or an exception state; a plain execution state can be further distinguished in either a normal execution state, or a branching state, or a value state (for computations yielding a proper value), or an environment state (for computations yielding an execution environment).

Definition 9.1. (GotoMode, SwitchMode, ValMode, EnvMode, ExceptMode, CtrlMode, CtrlState.) The sets of goto, switch, value, environment, exception and all control modes are given, respectively, by

GotoMode =^{def} { goto(id) | id ∈ Id },
SwitchMode =^{def} { switch(sval) | sval ∈ sVal },
ValMode =^{def} { value(sval) | sval ∈ sVal },
EnvMode =^{def} { env(ρ) | ρ ∈ Env },
ExceptMode =^{def} { except(ξ) | ξ ∈ Except },
CtrlMode =^{def} GotoMode ⊎ SwitchMode ⊎ ValMode ⊎ EnvMode

⊎ ExceptMode ⊎ {continue, break, return, exec},

where continue, break and return are the exit modes and exec is the plain execution mode. Control modes are denoted by cm, cm_{0}, cm_{1} and so forth.

A control state is an element of CtrlState =^{def} CtrlMode × Mem. Control states are denoted by cs, cs_{0}, cs_{1} and so forth.

The concrete semantics of the goto statement can now be expressed by

ρ ⊢_{β} ⟨goto id, (cm, σ)⟩ → ⟨cm_{0}, σ⟩

if cm = exec and cm_{0} = goto(id) or cm ≠ exec and cm_{0} = cm.

The semantics of labeled statements is given by

ρ ⊢_{β} ⟨s, (cm_{0}, σ)⟩ → η ; ρ ⊢_{β} ⟨l : s, (cm, σ)⟩ → η

where cm_{0} = exec if cm = exec, or cm = goto(id) and l = id, or cm = switch(sval) and l ∈ {default, sval}; otherwise cm_{0} = cm.

Of course, the semantics of all statements must be suitably modified. For instance, the assignment should behave like a nop unless the control mode is the normal execution one. Statements with non trivial control flow need more work. For example, the semantics of the conditional statement can be captured by^{14}

ρ ⊢_{β} ⟨e, (exec, σ)⟩ → ⟨cm_{0}, σ_{0}⟩

if cm_{0} ∈ ExceptMode

ρ ⊢_{β} ⟨if e then s_{0} else s_{1}, (exec, σ)⟩ → ⟨cm_{0}, σ_{0}⟩

ρ ⊢_{β} ⟨e, (exec, σ)⟩ → ⟨value(tt), σ_{0}⟩ ρ ⊢_{β} ⟨s_{0}, (exec, σ_{0})⟩ → ⟨cm_{1}, σ_{1}⟩
ρ ⊢_{β} ⟨s_{1}, (cm_{1}, σ_{1})⟩ → η
ρ ⊢_{β} ⟨if e then s_{0} else s_{1}, (exec, σ)⟩ → η

(124)

if cm_{1} ∈ GotoMode;

ρ ⊢_{β} ⟨e, (exec, σ)⟩ → ⟨value(tt), σ_{0}⟩ ρ ⊢_{β} ⟨s_{0}, (exec, σ_{0})⟩ → ⟨cm_{1}, σ_{1}⟩
ρ ⊢_{β} ⟨if e then s_{0} else s_{1}, (exec, σ)⟩ → ⟨cm_{1}, σ_{1}⟩

if cm_{1} ∉ GotoMode;

ρ ⊢_{β} ⟨e, (exec, σ)⟩ → ⟨value(ff), σ_{0}⟩ ρ ⊢_{β} ⟨s_{1}, (exec, σ_{0})⟩ → η
ρ ⊢_{β} ⟨if e then s_{0} else s_{1}, (exec, σ)⟩ → η
ρ ⊢_{β} ⟨s_{0}, (cm, σ)⟩ → ⟨cm_{0}, σ_{0}⟩
ρ ⊢_{β} ⟨if e then s_{0} else s_{1}, (cm, σ)⟩ → ⟨cm_{0}, σ_{0}⟩

if cm ∈ GotoMode ⊎ SwitchMode and cm_{0} ∉ GotoMode ⊎ SwitchMode;

ρ ⊢_{β} ⟨s_{0}, (cm, σ)⟩ → ⟨cm_{0}, σ_{0}⟩ ρ ⊢_{β} ⟨s_{1}, (cm_{0}, σ_{0})⟩ → η
ρ ⊢_{β} ⟨if e then s_{0} else s_{1}, (cm, σ)⟩ → η

14Recall that, in C, it is perfectly legal to jump into the “else branch” from the “then branch.”

if cm ∈ GotoMode ⊎ SwitchMode and cm_{0} ∈ GotoMode ⊎ SwitchMode;

ρ ⊢_{β} ⟨if e then s_{0} else s_{1}, (cm, σ)⟩ → ⟨cm, σ⟩

if cm ∉ GotoMode ⊎ SwitchMode ⊎ {exec}.

Likewise, the semantics of the switch statement can be captured by:

ρ ⊢_{β} ⟨e, (exec, σ)⟩ → ⟨cm_{0}, σ_{0}⟩

if cm_{0} ∈ ExceptMode

ρ ⊢_{β} ⟨switch e in s, (exec, σ)⟩ → ⟨cm_{0}, σ_{0}⟩

ρ ⊢_{β} ⟨e, (exec, σ)⟩ → ⟨value(sval_{0}), σ_{0}⟩
ρ ⊢_{β} ⟨s, (switch(sval_{0}), σ_{0})⟩ → ⟨cm_{1}, σ_{1}⟩
ρ ⊢_{β} ⟨switch e in s, (exec, σ)⟩ → ⟨cm_{2}, σ_{1}⟩

if cm_{2} = \begin{cases}exec, & if cm_{1} ∈ SwitchMode ⊎ \{break\}, \\ cm_{1}, & otherwise; \end{cases}

ρ ⊢_{β} ⟨s, (goto(id), σ)⟩ → ⟨cm_{0}, σ_{0}⟩
ρ ⊢_{β} ⟨switch e in s, (goto(id), σ)⟩ → ⟨cm_{1}, σ_{0}⟩

if cm_{1} = \begin{cases}exec, & if cm_{0} = break, \\ cm_{0}, & otherwise; \end{cases}

if cm ∉ GotoMode ⊎ {exec}.

ρ ⊢_{β} ⟨switch e in s, (cm, σ)⟩ → ⟨cm, σ⟩

While such a semantic treatment captures all forward jumps, for backward jumps something more is required. One simple possibility (which is not the only one) is to explicitly introduce a looping construct that is (only) available in the abstract syntax. That is, we extend Stmt once again as

Stmt ∋ s ::= … | loop s

and assume that a set of such loops has been inserted so that all backward jumps are enclosed in at least one loop (notice that at most one such loop per function body suffices, but more can be used as a matter of optimization). For s ∈ Stmt, let SL(s) denote the set of statement labels in s. The concrete semantics of this looping construct is now given by

ρ ⊢_{β} ⟨s, cs⟩ → ⟨cm, σ⟩

if cm ≠ goto(id) for each id ∈ SL(s)

ρ ⊢_{β} ⟨loop s, cs⟩ → ⟨cm, σ⟩

ρ ⊢_{β} ⟨s, cs⟩ → ⟨goto(id), σ⟩ ρ ⊢_{β} ⟨loop s, (goto(id), σ)⟩ → η

\overline{if id ∈ SL(s)}

ρ ⊢_{β} ⟨loop s, cs⟩ → η

Observe that the systematic use of the looping construct can make rule schema (124) redundant.

Other rules are omitted for space reasons. However, there are no additional difficulties besides the ones just addressed: the rules for break and continue are straightforward; return e can be modeled as the assignment to the reserved identifier \underline{x}_{0} (see concrete rule (67)), followed by the setting of the control mode; the rules for the while loop are a bit involved as they must support the ‘break’ and ‘continue’ control modes in addition to ‘goto’ and ‘switch’.

The proposed approach handles non-structured control flow mechanisms essentially by adding a sort of control register to the rule-based interpreter of the language. As far as the abstract semantics is concerned, a first choice to be made concerns the approximation of the values that the control register can take. As usual, there is a complexity/precision trade-off to be faced: the simple solution is to approximate ℘(CtrlMode) by some (simple) abstract domain CtrlMode^{♯} and then approximate CtrlState = CtrlMode × Mem by CtrlMode^{♯} ⊗ Mem^{♯}; a more precise solution is to approximate ℘(CtrlState) by an abstract domain CtrlState^{♯} that captures relational information connecting the control modes to the memory structures they can be coupled with. The abstract rules schemata must of course be modified to match the concrete world. For instance, the abstract rule for the conditional statement becomes:

ρ ⊢_{β} ⟨e, cs_{cond}^{♯}⟩ → cs_{0}^{♯} ρ ⊢_{β} ⟨s_{0}, cs_{then}^{♯}⟩ → cs_{1}^{♯} ρ ⊢_{β} ⟨s_{1}, cs_{else}^{♯}⟩ → cs_{2}^{♯}
ρ ⊢_{β} ⟨if e then s_{0} else s_{1}, cs^{♯}⟩ ⇝ cs_{3}^{♯}

where

cs_{cond}^{♯} = Φ_{e}(ρ, cs^{♯}, tt),
cs_{then}^{♯} = Φ_{e}(ρ, cs^{♯}, e) ⊔ Φ_{m}(cs^{♯}, GotoMode ⊎ SwitchMode),
cs_{else}^{♯} = Φ_{e}(ρ, cs^{♯}, not e) ⊔ Φ_{m}(cs_{1}^{♯}, GotoMode) ⊔ cs_{jump}^{♯},
cs_{jump}^{♯} = \begin{cases}⊥, & if Φ_{m}(cs^{♯}, GotoMode ⊎ SwitchMode) = ⊥, \\ Φ_{m}(cs_{1}^{♯}, C_{jump}), & otherwise, \end{cases}
C_{jump} = GotoMode ∪ { cm ∈ CtrlMode | ∃σ ∈ Mem . γ(cs^{♯}) = (cm, σ) },
cs_{3}^{♯} = Φ_{m}(cs^{♯}, CtrlMode \ ({exec} ⊎ GotoMode ⊎ SwitchMode))
⊔ Φ_{m}(cs_{0}^{♯}, CtrlMode \ ValMode) ⊔ cs_{1}^{♯} ⊔ cs_{2}^{♯},

and the two computable filter functions Φ_{e} : (Env ×CtrlState^{♯} ×Exp) → CtrlState^{♯} and Φ_{m} : (CtrlState^{♯} × ℘(CtrlMode)) → CtrlState^{♯} are defined as follows, for each ρ ∈ Env, cs^{♯} ∈ CtrlState^{♯}, e ∈ Exp and C ⊆ CtrlMode such that, for some β ∈ TEnv, β : I with FI(e) ⊆ I and β ⊢_{I} e : boolean:

γ(Φ_{e}(ρ, cs^{♯}, e)) ⊇ \{ cs ∈ γ(cs^{♯}) | \begin{matrix}∃σ ∈ Mem . cs = (exec, σ), \\ ∃σ′ ∈ Mem \\ . (ρ ⊢_{β} ⟨e, cs⟩ → ⟨value(tt), σ′⟩) \end{matrix} \},

γ(Φ_{m}(cs^{♯}, C)) ⊇ { cs ∈ γ(cs^{♯}) | ∃σ ∈ Mem . cs = (cm, σ), cm ∈ C }.

10. CONCLUSION

In this paper, we have confronted the problem of defining an analysis framework for the specification and realization of precise static analyzers for mainstream imperative programming languages, tools in very short supply that, however, ought to become part of the current programming practice. A proposal put forward by Schmidt twelve years ago [Sch95] held, in our eyes, considerable promise, despite the fact it had not been fully developed and applied in realistic contexts. It was therefore natural to question whether the promise could be fulfilled. To investigate Schmidt’s approach, which is based on structured operational semantics and abstract interpretation, we have defined an imperative language, CPM, that embodies all the “problematic features” of single-threaded imperative languages now in widespread use. We have presented a concrete semantics of CPM that is suitable for abstraction while retaining all the nice features of SOS descriptions. For a subset of the language we have formally defined an abstract semantics that can fully exploit the precision offered by relational abstract domains, and proved its soundness with respect to the concrete one. We have also shown how approximations of the abstract semantics can be effectively computed. In order to provide an experimental evaluation of the ideas presented in this paper, both the concrete and the abstract semantics —instantiated over sophisticated numeric domains and together with a suitable fixpoint computation engine— have been incorporated into the ECLAIR system. This work allows us to conclude that the proposal of Schmidt can play a crucial role in the development of reliable and precise analyzers. The key features of this approach are:

—a fairly concise concrete semantics that experts can easily read (and modify as needed) and that everyone can execute on non-trivial examples in order to check its agreement with the applicable language standards;

—a fairly concise abstract semantics that is fully parametric with respect to the abstract domain, that is not difficult to prove correct with respect to the concrete one (to the point that automatizing the proof seems to be a reasonable goal), and that directly leads to the implementation of static analyzers.

Of course, the story does not end here. For instance, our analysis framework is parametric on abstract memory structures. While the literature seems to provide all that is necessary to realize very sophisticated ones, it is not difficult to predict that, among all the code out there waiting to be analyzed, some will greatly exacerbate the complexity/precision trade-off. However, these are research problems for the future — now that we have, as given here, a formal design on which analyzers can be built, our next goal is to complete the build and make the technology described here truly available and deployable.

ACKNOWLEDGMENTS

Anna Dolma Alonso, Irene Bacchi, Danilo Bonardi, Andrea Cimino, Enrico Franchi, Davide Masi and Alessandro Vincenzi (all students of the course on “Analysis and Verification of Software” taught by Roberto Bagnara at the University of Parma) and Vajirapan Panumong (University of Leeds) collaborated on previous, much more restricted versions of this work. We are also grateful to David Merchat (formerly at the University of Parma) and Katy Dobson (University of Leeds) for the discussions we have had on the subject of this paper.

REFERENCES

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival, Design and implementation of a special-purpose static program analyzer for safety-critical realtime embedded software, The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones [on occasion of his 60th birthday] (T. Æ. Mogensen, D. A. Schmidt, and I. Hal Sudborough, eds.), Lecture Notes in Computer Science, vol. 2566, Springer-Verlag, Berlin, 2002, pp. 85–108.

, A static analyzer for large safety-critical software, Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI’03) (San Diego, California, USA), ACM Press, 2003, pp. 196–207.

R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella, Precise widening operators for convex poly-

hedra, Science of Computer Programming 58 (2005), no. 1–2, 28–56. R. Bagnara, P. M. Hill, and E. Zaffanella, Not necessarily closed convex polyhedra and the double

description method, Formal Aspects of Computing 17 (2005), no. 2, 222–257.

, The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems, Quaderno 457, Dipartimento di Matematica, Università di Parma, Italy, 2006, Available at http://www.cs.unipr.it/

Publications/. Also published as arXiv:cs.MS/0612085, available from http://arxiv.org/.

M. Bruynooghe, A practical framework for the abstract interpretations of logic programs, Journal

of Logic Programming 10 (1991), 91–124. P. Cousot and R. Cousot, Static determination of dynamic properties of programs, Proceedings

of the Second International Symposium on Programming (Paris, France) (B. Robinet, ed.), Dunod, Paris, France, 1976, pp. 106–130.

, Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages (New York), ACM Press, 1977, pp. 238–252.

, Static determination of dynamic properties of recursive procedures, IFIP Conference on Formal Description of Programming Concepts (E. J. Neuhold, ed.), North-Holland, 1977, pp. 237–277.

, Systematic design of program analysis frameworks, Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages (New York), ACM Press, 1979, pp. 269–282.

, Abstract interpretation frameworks, Journal of Logic and Computation 2 (1992), no. 4, 511–547.

, Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming (Leuven, Belgium) (M. Bruynooghe and M. Wirsing, eds.), Lecture Notes in Computer Science, vol. 631, Springer-Verlag, Berlin, 1992, pp. 269–295.

, Inductive definitions, semantics and abstract interpretation, Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages (Albuquerque, New Mexico, USA), ACM Press, 1992, pp. 83–94.

, Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages), Proceedings of the IEEE Computer Society 1994 International Conference on Computer Languages (Toulouse, France) (H. E. Bal, ed.), IEEE Computer Society Press, 1994, Invited paper, pp. 95– 112.

P. Cousot and N. Halbwachs, Automatic discovery of linear restraints among variables of a program, Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages (Tucson, Arizona), ACM Press, 1978, pp. 84–96.

P. Cousot, Semantic foundations of program analysis, Program Flow Analysis: Theory and Applications (S. S. Muchnick and N. D. Jones, eds.), Prentice Hall, Englewood Cliffs, NJ, USA, 1981, pp. 303–342.

, The calculational design of a generic abstract interpreter, Calculational System Design (M. Broy and R. Steinbrüggen, eds.), NATO ASI Series F. IOS Press, Amsterdam, NL, 1999.

, The verification grand challenge and abstract interpretation, Verified Software: Theories, Tools, Experiments (VSTTE) (ETH Zürich, Switzerland), 2005, Position paper.

N. Dor, M. Rodeh, and S. Sagiv, Cleanness checking of string manipulations in C programs via integer analysis, Static Analysis: 8th International Symposium, SAS 2001 (Paris, France) (P. Cousot, ed.), Lecture Notes in Computer Science, vol. 2126, Springer-Verlag, Berlin, 2001, pp. 194–212.

M. Emami, R. Ghiya, and L. J. Hendren, Context-sensitive interprocedural points-to analysis in the presence of function pointers, Proceedings of the ACM SIGPLAN’94 Conference on Programming Language Design and Implementation (Orlando, Florida), vol. 29, ACM SIGPLAN Notices, no. 6, Association for Computing Machinery, 1994, pp. 242–256.

M. Emami, A practical inter-procedural alias analysis for an optimizing/paralleling C compiler, Master’s thesis, School of Computer Science, McGill University, Montreal, Canada, August 1993.

D. Gopan, F. DiMaio, N. Dor, T. W. Reps, and M. Sagiv, Numeric domains with summarized dimensions, Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004 (Barcelona, Spain) (K. Jensen and A. Podelski, eds.), Lecture Notes in Computer Science, vol. 2988, Springer-Verlag, Berlin, 2004, pp. 512–529.

R. Giacobazzi, S. K. Debray, and G. Levi, A generalized semantics for constraint logic programs, Proceedings of the International Conference on Fifth Generation Computer Systems (FGCS’92) (Tokyo, Japan), ICOT, 1992, pp. 581–591.

D. Gopan, T. W. Reps, and M. Sagiv, A framework for numeric analysis of array operations, Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Long Beach, California, USA), 2005, pp. 338–350.

N. Halbwachs, Delay analysis in synchronous programs, Computer Aided Verification: Proceedings of the 5th International Conference (Elounda, Greece) (C. Courcoubetis, ed.), Lecture Notes in Computer Science, vol. 697, Springer-Verlag, Berlin, 1993, pp. 333–346.

C. A. R. Hoare, The verifying compiler: A grand challenge for computing research, Journal of the

ACM 50 (2003), no. 1, 63–69. N. Halbwachs, Y.-E. Proy, and P. Roumanoff, Verification of real-time systems using linear rela-

tion analysis, Formal Methods in System Design 11 (1997), no. 2, 157–185. B. Jeannet and W. Serwe, Abstracting call-stacks for interprocedural verification of imperative

programs, Publication interne 1543, IRISA, Campus de Beaulieu, Rennes, France, 2003.

, Abstracting call-stacks for interprocedural verification of imperative programs, Proceedings of the 10th International Conference on Algebraic Methodology and Software Technology (Stirling, Scotland, UK) (C. Rattray, S. Maharaj, and C. Shankland, eds.), Lecture Notes in Computer Science, vol. 3116, Springer-Verlag, Berlin, 2004, pp. 258–273.

G. Kahn, Natural semantics, Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science (Passau, Germany) (F.-J. Brandenburg, G. Vidal-Naquet, and M. Wirsing, eds.), Lecture Notes in Computer Science, vol. 247, Springer-Verlag, Berlin, 1987, pp. 22–39.

X. Leroy, Coinductive big-step operational semantics, Programming Languages and Systems, Proceedings of the 14th European Symposium on Programming (Vienna, Austria) (P. Sestoft, ed.), Lecture Notes in Computer Science, vol. 3924, Springer-Verlag, Berlin, 2006, pp. 54–68.

A. Miné, Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics, Proceedings of the 2006 ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (Ottawa, Ontario, Canada) (M. J. Irwin and K. De Bosschere, eds.), ACM Press, 2006, pp. 54–63.

G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer, CIL: Intermediate language and tools for analysis and transformation of C programs, Compiler Construction: Proceedings of the 11th International Conference (CC 2002) (Grenoble, France) (R. N. Horspool, ed.), Lecture Notes in Computer Science, vol. 2304, Springer-Verlag, Berlin, 2002, pp. 213–228.

G. D. Plotkin, A structural approach to operational semantics, Journal of Logic and Algebraic Programming 60–61 (2004), 17–139.

D. A. Schmidt, Natural-semantics-based abstract interpretation (preliminary version), Static Analysis: Proceedings of the 2nd International Symposium (Glasgow, UK) (A. Mycroft, ed.), Lecture Notes in Computer Science, vol. 983, Springer-Verlag, Berlin, 1995, pp. 1–18.

, Abstract interpretation of small-step semantics, Analysis and Verification of Multiple-Agent Languages (M. Dam, ed.), Lecture Notes in Computer Science, vol. 1192, Springer-Verlag, Berlin, 1997, 5th LOMAPS Workshop Stockholm, Sweden, June 24–26, 1996, Selected Papers, pp. 76–99.

, Trace-based abstract interpretation of operational semantics, LISP and Symbolic Computation 10 (1998), no. 3, 237–271.

R. Shaham, E. K. Kolodner, and S. Sagiv, Automatic removal of array memory leaks in Java, Proceedings of the 9th International Conference on Compiler Construction (CC 2000) (Berlin, Germany) (D. A. Watt, ed.), Lecture Notes in Computer Science, vol. 1781, Springer-Verlag, Berlin, 2000, pp. 50–66.

M. Sharir and A. Pnueli, Two approaches to interprocedural data flow analysis, Program Flow Analysis: Theory and Applications (S. S. Muchnick and N. D. Jones, eds.), Prentice Hall, Englewood Cliffs, NJ, USA, 1981, pp. 189–233.

S. Sagiv, T. W. Reps, and R. Wilhelm, Parametric shape analysis via 3-valued logic, ACM Transactions on Programming Languages and Systems 24 (2002), no. 3, 217–298.