arXiv:cs/0703116v2 [] 28 Jun 2007

On the Design of Generic Static Analyzers
for Modern 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 modern
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 ASTRÉ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, ASTRÉ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 ASTRÉ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 Modern 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.

1 It

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/).

4

·

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

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 ECLAIR2 — 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.

2 The

‘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/).

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

5

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
modern 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) uninitial-

6

·

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

ization 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 = {s1 , . . . , sn } be a finite set of cardinality n ≥ 0. Then, the notation
{s1 7→ t1 , . . . , sn 7→ tn }, where {t1 , . . . , tn } ⊆ T , stands for the function f : S → T
such that f (si ) = ti , 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 : (S1 × · · · × Sn ) → T we omit, as
customary, the outer parentheses and write f (s1 , . . . , sn ) to mean f (s1 , . . . , sn ) .

·

On the Design of Generic Static Analyzers for Modern Imperative Languages

7

Let f0 : S0 ֌ T0 and f1 : S1 ֌ T1 be partial functions. Then the function
f0 [f1 ] : (S0 ∪ S1 ) ֌ (T0 ∪ T1 ) is defined, for each x ∈ dom(f0 ) ∪ dom(f1 ), by
(

f1 (x), if x ∈ dom(f1 );
def
f0 [f1 ] (x) =
f0 (x), if x ∈ dom(f0 ) \ dom(f1 ).

(Note that, if f0 and f1 are total functions, then f0 [f1 ] 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|.
def

The integer part function int : R → Z is given, for each x ∈ R, by int(x) = ⌊x⌋, if
def

x ≥ 0, and int(x) = ⌈x⌉,
 if x < 0. The integer division and the modulo operations
÷, mod : Z × Z \ {0} → Z are defined, for each x, y ∈ Z with y 6= 0, respectively
def

def

by x ÷ y = int(x/y) and x mod y = 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:
def

Identifiers. id ∈ Id = {main, x, x0 , x1 , . . .} ⊎ rId, where rId = {x, x0 , x1 , . . .};
def

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

Integers. m ∈ Integer = Z;
def

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

RTS exceptions. χ ∈ RTSExcept = {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 | e0 + e1 | e0 − e1 | e0 ∗ e1 | e0 / e1 | e0 % e1
| t | e0 = e1 | e0 6= e1 | e0 < e1 | e0 ≤ e1 | e0 ≥ e1 | e0 > e1
| not e | e0 and e1 | e0 or e1 | 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 : sT
Global declarations.
Glob ∋ g ::= gvar id : sT = e | function id(fps) = body | rec g | g0 ; g1
Local declarations.
Decl ∋ d ::= nil | lvar id : sT = e | d0 ; d1
Catchable types.
cType ∋ cT ::= rts exception | sT
Exception declarations.
exceptDecl ∋ p ::= χ | cT | id : sT | any
Catch clauses.
Catch ∋ k ::= (p) s | k0 ; k1
Statements.
Stmt ∋ s ::= nop | id := e | id0 := id(es) | s0 ; s1 | d; s
| if e then s0 else s1 | while e do s
| throw χ | throw e | try s catch k | try s0 finally s1
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 values3 and exceptions:
Constants.
Con ∋ con ::= m | t
3 The

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.

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

9

Storable values.
sVal ∋ sval ::= con
Exceptions.
Except ∋ ξ ::= χ | sval
The (partial) function type : sVal ֌ sType, mapping a storable value to its type
name ‘integer’ or ‘boolean’, is defined by:
(
integer, if sval = m ∈ Integer;
def
type(sval) =
boolean, if sval = t ∈ Bool.
For ease of notation, we also define the overloadings type : Except ֌ cType and
type : exceptDecl ֌ cType defined by
(
rts exception, if ξ = χ ∈ RTSExcept;
def
type(ξ) =
type(sval),
if ξ = sval ∈ sVal;


rts exception, if p = χ ∈ RTSExcept;
def
type(p) = cT,
if p = cT ∈ cType;


sT,
if p = id : sT and sT ∈ sType.

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


if cT = integer;
Integer,
def
dom(cT) = Bool,
if cT = boolean;


RTSExcept, if cT = rts exception.

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:
def

def

def

def

def

def

DI() = DI(nil) = DI(body) = DI(χ) = DI(cT) = DI(any) = ∅;
def

def

DI(id : sT) = DI(gvar id : sT = e) = DI(lvar id : sT = e)
def

def

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

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

DI(rec g) = DI(g);
def

DI(g0 ; g1 ) = DI(g0 ) ∪ DI(g1 );

10

·

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

DI(d0 ; d1 ) = DI(d0 ) ∪ DI(d1 ).
The set of identifiers that occur freely in (sequences of) expressions, (exception)
declarations, statements and catch clauses is defined by:
def

def

def

def

def

FI(m) = FI(t) = FI(nop) = FI() = FI(id : sT) = FI(nil)
def

def

def

def

def

def

= FI(χ) = FI(cT) = FI(any) = FI(throw χ) = FI(extern : sT) = ∅;
def

def

FI(−e) = FI(not e) = FI(lvar id : sT = e)
def

def

def

= FI(gvar id : sT = e) = FI(throw e) = FI(e);
def

FI(e0 op e1 ) = FI(e0 ) ∪ FI(e1 ), for op ∈ {+, . . . , %, =, . . . , >, and, or};
def

FI(id) = {id};


def
FI(let d in s result e) = FI(d) ∪ FI(s) \ DI(d) ∪ FI(e) \ DI(d) ;
def

FI(function id(fps) = body) = FI(body) \ DI(fps);
def

FI(rec g) = FI(g) \ DI(g);

def
FI(g0 ; g1 ) = FI(g0 ) ∪ FI(g1 ) \ DI(g0 ) ;

def
FI(d0 ; d1 ) = FI(d0 ) ∪ FI(d1 ) \ DI(d0 ) ;
def

FI(id := e) = {id} ∪ FI(e);
def

FI(e, es) = FI(e) ∪ FI(es);
 def
FI id0 := id(es) = {id, id0 } ∪ FI(es);

def
FI(d; s) = FI(d) ∪ FI(s) \ DI(d) ;
 def
FI (p) s = FI(s) \ DI(p);
def

FI(k0 ; k1 ) = FI(k0 ) ∪ FI(k1 );
def

def

FI(s0 ; s1 ) = FI(try s0 finally s1 ) = FI(s0 ) ∪ FI(s1 );
def

FI(if e then s0 else s1 ) = FI(e) ∪ FI(s0 ) ∪ FI(s1 );
def

FI(while e do s) = FI(e) ∪ FI(s);
def

FI(try s catch k) = 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.

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

11

Definition 4.1. (TEnvI , TEnv.) For each I ⊆f Id, the set of type environdef

ments over I is TEnvI = I → dType; the set of all type environments is given by
def U
TEnv = I⊆f Id TEnvI . Type environments are denoted by β, β0 , β1 and so forth.
The notation β : I is a shorthand for β ∈ TEnvI .
4.3 Static Semantics Predicates
Let I ⊆f Id and β ∈ TEnvI . 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,
β ⊢I body : sT,

e is well-formed and has type sT in β;
body is well-formed and has type sT in β;

β, fps ⊢I es,
fps : δ,

es is compatible with fps and well formed in β;
fps is well formed and yields the type environment δ;

β ⊢I g : δ,
β ⊢I d : δ,

g is well formed and yields the type environment δ in β;
d is well-formed and yields the type environment δ in β;

⊢I p : δ,

p is well-formed and yields the type environment δ;

β ⊢I k,
β ⊢I s,

k is well-formed in β;
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 : boolean

β ⊢I −e : integer

β ⊢I not e : boolean

β ⊢I e0 : integer β ⊢I e1 : integer
β ⊢I e0  e1 : integer
β ⊢I e0 : integer β ⊢I e1 : integer
β ⊢I e0  e1 : boolean
β ⊢I e0 : boolean β ⊢I e1 : boolean
β ⊢I e0 ⋄ e1 : boolean
β ⊢I id : sT

if  ∈ {+, −, ∗, /, %}
if  ∈ {=, 6=, <, ≤, ≥, >}
if ⋄ ∈ {and, or}

if β(id) = sT loc

Sequences of expressions.
β ⊢I e : sT β, fps ⊢I es
β,  ⊢I 

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

12

·

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

Sequences of formal parameters.
fps : δ
:∅

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

if id ∈
/ DI(fps)

Function bodies.
β ⊢ I d : β0

β[β0 ] ⊢I∪DI(d) s

β[β0 ] ⊢I∪DI(d) e : sT

β ⊢I (let d in s result e) : sT

β ⊢I (extern : sT) : sT
Declarations.
β ⊢I e : sT
β ⊢I nil : ∅

β ⊢I gvar id : sT = e : {id 7→ sT loc}
β ⊢I e : sT
β ⊢I lvar id : sT = e : {id 7→ sT loc}

fps : δ

β ⊢I

β[δ] ⊢I∪DI(fps) body : sT
 
function id(fps) = body : id 7→ (fps → sT)

β[δ |J ] ⊢I∪J g : δ
β ⊢I (rec g) : δ
β ⊢ I g 0 : β0

if J = FI(g) ∩ DI(g) and ∀id, sT : (id 7→ sT loc) ∈
/δ

β[β0 ] ⊢I∪DI(g0 ) g1 : β1

β ⊢I g0 ; g1 : β0 [β1 ]

β ⊢I d0 : β0

(1)

β[β0 ] ⊢I∪DI(d0 ) d1 : β1

β ⊢I d0 ; d1 : β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 7→ sT loc}

⊢I any : ∅

Catch clauses.
⊢I p : δ

β[δ] ⊢I∪DI(p) s

β ⊢I (p) s
4 Namely,

β ⊢I k0

β ⊢I k1

β ⊢I k0 ; k1

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

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

13

Statements.
β ⊢I e : sT
β ⊢I nop

β ⊢I id := e

β, fps ⊢I es
β ⊢I id0 := id(es)
β ⊢ I s0

if β(id) = sT loc

if β(id0 ) = sT loc and β(id) = fps → sT

β ⊢ I s1

β ⊢ I d : β0

β ⊢ I s0 ; s1
β ⊢I e : boolean β ⊢I s0

β[β0 ] ⊢I∪DI(d) s

β ⊢I d; s
β ⊢ I s1

β ⊢I e : boolean β ⊢I s

β ⊢I if e then s0 else s1

β ⊢I while e do s
β ⊢I e : sT

β ⊢I throw χ
β ⊢I s

β ⊢I throw e

β ⊢I k

β ⊢I try s catch k

β ⊢ I s0

β ⊢ I s1

β ⊢I try s0 finally s1

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, l0 , l1 and so forth. We also postulate
def
the existence of a set Ind = N of indirect (stack) locators such that Loc ∩ Ind = ∅.
Indirect locators are denoted by i, i0 , i1 and so forth. For notational convenience,
def
we define the set of addresses as Addr = Loc ⊎ Ind. Addresses are denoted by a,
a0 , a1 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, EnvI .) We define
def

Abstract = { λ fps . body | fps ∈ formParams, body ∈ Body }.

14

·

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

The set of concrete denotable values is
def

dVal = (Addr × sType) ⊎ Abstract.
def

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

∀id ∈ I : ∃(a, sT) ∈ Addr × sType . β(id) = sT loc ∧ ρ(id) = (a, sT)
∨ ∃abs = (λ fps . body) ∈ Abstract . β(id) = fps → sT ∧ β ⊢I body : sT

5.3 Memory Structures, Value States and Exception States


∧ ρ(id) = abs .

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
def

Map = (Loc × sType) ֌ sVal.

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

15

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

 def
µ (l, sT) := sval = µ′ ,

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′ 6= l.
⋆
def
Let W = 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
def
i < n = | tf(w)|, tf(w) = z0 · · · zn−1 and zi = l, then w @ i = l.
def

A memory structure is an element of Mem = Map × Stack. Memory structures
are denoted by σ, σ0 , σ1 and so forth.
def
A value state is an element of ValState = sVal × Mem. Value states are denoted
by υ, υ0 , υ1 and so forth.
def
An exception state is an element of ExceptState = 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, if a ∈ Loc;
def
σ@a =
l, if a ∈ Ind and l = w @ a is defined.
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
(

µ(d), σ ,
if d ∈ dom(µ);
def
σ[a, sT] =
(σ, memerror), otherwise;
(


 def
µ[d := sval], w , if d ∈ dom(µ) and sT = type(sval);
σ (a, sT) := sval =
(σ, memerror),
otherwise.

16

·

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

The data and stack memory allocation functions

newd : ValState → (Mem × Loc) ⊎ ExceptState ,

news : ValState → (Mem × Ind) ⊎ ExceptState

are defined, for each υ = (sval, σ) ∈ ValState, where σ = (µ, w), by
(
((µ′ , w), l),
if the data segment of σ can be extended;
def
newd (υ) =
(σ, datovflw), otherwise;
(
((µ′ , w′ ), i),
if the stack segment of σ can be extended;
def
news (υ) =
(σ, stkovflw), otherwise;
where, in the case of news , w′ ∈ Stack and i ∈ Ind are such that:
(i) w′ = w · l;
(ii) i = | tf(w)|;
and, for both newd and news , µ′ ∈ 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 cleanupd : ExceptState → ExceptState
is given, for each ε = (σ, ξ) ∈ ExceptState, by

def
cleanupd (ε) = (∅, ǫ), ξ .
The stack mark function marks : Mem → Mem is given, for each σ ∈ Mem, by
def

marks (σ) = (µ, w†),

where σ = (µ, w).

The stack unmark partial function unmarks : Mem ֌ Mem is given, for each σ ∈
Mem such that σ = (µ, w′ †w′′ ) and w′′ ∈ Loc⋆ , by
def

unmarks (µ, w′ †w′′ ) = (µ′ , 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 links : Mem ֌ Mem is given, for each σ ∈ Mem
such that σ = (µ, w′ †w′′ ) and w′′ ∈ Loc⋆ , by
def

links (µ, w′ †w′′ ) = (µ, w′ ‡w′′ ).
The frame unlink partial function unlinks : Mem ֌ Mem is given, for each σ ∈
Mem such that σ = (µ, w′ ‡w′′ ) and w′′ ∈ Loc⋆ , by
def

unlinks (µ, w′ ‡w′′ ) = (µ, w′ †w′′ ).

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

17

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,

def
unmarks (σ, ξ) = unmarks (σ), ξ ;

def
unlinks (σ, ξ) = unlinks (σ), ξ .

Intuitively, global variables are allocated in the data segment using newd and are
accessed through absolute locations; function cleanupd models their deallocation
due to an RTS exception thrown during the program start-up phase. The functions
marks and unmarks use the stack marker ‘†’ to implement the automatic allocation
(through news ) and deallocation of stack slots for storing local variables, return
values and actual arguments of function calls. The functions links and unlinks 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 links is matched by a corresponding unlinks , 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 (l0 , sT0 ) and the ones associated to (l1 , sT1 ), unless l0 = l1 . Moreover, we
need not specify the relationship between µ(l, sT0 ) and µ(l, sT1 ) for the case where
sT0 6= sT1 . 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 newd and
news . 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.

·

18

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

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 β ∈ TEnvI , by
def 
Γβe = he, σi ∈ Exp × Mem ∃sT ∈ sType . β ⊢I e : sT ,
def 
Γβd = hd, σi ∈ Decl × Mem ∃δ ∈ TEnv . β ⊢I d : δ ,
def 
Γβg = hg, σi ∈ Glob × Mem ∃δ ∈ TEnv . β ⊢I g : δ ,
def 
Γβs = hs, σi ∈ Stmt × Mem β ⊢I s ,
def 
Γβb = hbody, σi ∈ Body × Mem ∃sT ∈ sType . β ⊢I body : sT ,
def 
Γβk = hk, εi ∈ 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
def

Te = ValState ⊎ ExceptState,
def

def

def

def

Td = Tg = (Env × Mem) ⊎ ExceptState,
Ts = Tb = Mem ⊎ ExceptState,


def
Tk = {caught} × Ts ⊎ {uncaught} × ExceptState .

Note that Te is defined as ValState ⊎ ExceptState; as it will be apparent from the
concrete semantics, expressions never modify the memory structure, so Te 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 ε ∈ Ts or hσ, ξi ∈ Ts , as well as
hcaught, εi ∈ Tk or caught, (σ, ξ) ∈ Tk .
A few explanatory words are needed for Tk . When the evaluation of a nonterminal configuration for catch clauses hk, εi ∈ Γβk yields the terminal configuration
hcaught, ηi ∈ Tk , then the exception ξ in ε = (σ, ξ) was caught inside k and η ∈ Ts
is the result of evaluating the corresponding exception handler statement; note that
η ∈ Ts 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 huncaught, εi ∈ Tk , then the exception in ε
was not caught inside k and will be propagated to the outer context.5
5 Note

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 Ts ∩ ExceptState 6= ∅.

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

19

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 ρ
def

def

def

Consequently, if ρ : I we define DI(ρ) = DI(rec ρ) = I, FI(ρ) =
def

S

id∈I


FI ρ(id)

and FI(rec ρ) = FI(ρ) \ I, where the function FI is defined on elements of dVal by
def

def

def

FI(l, sT) = FI(i, sT) = ∅ and FI(λ fps . body) = FI(body) \ DI(fps). The static
semantics is extended by adding the rules
ρ:δ

β[δ |J ] ⊢I∪J ρ : δ

β ⊢I ρ : δ

β ⊢I rec ρ : δ

if J = FI(ρ) ∩ DI(ρ) and ∀id : (id 7→ sT loc) ∈
/ δ.

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 β ∈ TEnvI ,
ρ ∈ EnvJ , ρ : β |J and, for some q ∈ {e, d, g, s, b, k}, N ∈ Γβq and η ∈ Tq .
5.5.1

Expressions

Constant.
ρ ⊢β hcon, σi → hcon, σi

(2)

Identifier.


ρ ⊢β hid, σi → σ ρ(id)

(3)

Unary minus.

ρ ⊢β he, σi → ε
ρ ⊢β h−e, σi → ε
ρ ⊢β he, σi → hm, σ0 i
ρ ⊢β h−e, σi → h−m, σ0 i

(4)

(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:
ρ ⊢β he0 , σi → ε
ρ ⊢β he0  e1 , σi → ε
ρ ⊢β he0 , σi → hm0 , σ0 i ρ ⊢β he1 , σ0 i → ε
ρ ⊢β he0  e1 , σi → ε

(6)

(7)

20

·

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

ρ ⊢β he0 , σi → hm0 , σ0 i ρ ⊢β he1 , σ0 i → hm1 , σ1 i
ρ ⊢β he0  e1 , σi → hm0 ◦ m1 , σ1 i

if  ∈
/ {/, %} or m1 6= 0
(8)

ρ ⊢β he0 , σi → hm0 , σ0 i ρ ⊢β he1 , σ0 i → h0, σ1 i
ρ ⊢β he0  e1 , σi → hσ1 , divbyzeroi

if  ∈ {/, %}

(9)

Arithmetic tests. Let  ∈ {=, 6=, <, ≤, ≥, >} be an abstract syntax operator and
denote with ‘≶’ the corresponding test operation in Z × Z → Bool. The rules for
the arithmetic tests are then given by the following schemata:
ρ ⊢β he0 , σi → ε
ρ ⊢β he0  e1 , σi → ε
ρ ⊢β he0 , σi → hm0 , σ0 i ρ ⊢β he1 , σ0 i → ε
ρ ⊢β he0  e1 , σi → ε
ρ ⊢β he0 , σi → hm0 , σ0 i ρ ⊢β he1 , σ0 i → hm1 , σ1 i
ρ ⊢β he0  e1 , σi → hm0 ≶ m1 , σ1 i

(10)

(11)

(12)

Negation.
ρ ⊢β hb, σi → ε
ρ ⊢β hnot b, σi → ε
ρ ⊢β hb, σi → ht, σ0 i
ρ ⊢β hnot b, σi → h¬ t, σ0 i

(13)

(14)

Conjunction.
ρ ⊢β hb0 , σi → ε
ρ ⊢β hb0 and b1 , σi → ε
ρ ⊢β hb0 , σi → hff, σ0 i
ρ ⊢β hb0 and b1 , σi → hff, σ0 i
ρ ⊢β hb0 , σi → htt, σ0 i ρ ⊢β hb1 , σ0 i → η
ρ ⊢β hb0 and b1 , σi → η

(15)

(16)

(17)

Disjunction.
ρ ⊢β hb0 , σi → ε
ρ ⊢β hb0 or b1 , σi → ε
ρ ⊢β hb0 , σi → htt, σ0 i
ρ ⊢β hb0 or b1 , σi → htt, σ0 i
ρ ⊢β hb0 , σi → hff, σ0 i ρ ⊢β hb1 , σ0 i → η
ρ ⊢β hb0 or b1 , σi → η

(18)

(19)

(20)

·

On the Design of Generic Static Analyzers for Modern Imperative Languages

5.5.2

21

Declarations

Nil.
(21)

ρ ⊢β hnil, σi → h∅, σi
Environment.

(22)

ρ ⊢β hρ0 , σi → hρ0 , σi
Recursive environment.

(23)

ρ ⊢β hrec ρ0 , σi → hρ1 , σi
if ρ1 =
∪



(

id 7→ ρ0 (id) ρ0 (id) = λfps . extern : sT
id 7→ abs1

∀i ∈ {0, 1} : absi = λfps . let di in s result e,

ρ0 (id) = abs0 , d1 = rec ρ0 \ DI(fps) ; d0

)

.

Global variable declaration.

ρ ⊢β he, σi → ε

(24)

ρ ⊢β hgvar id : sT = e, σi → cleanupd (ε)
ρ ⊢β he, σi → υ
ρ ⊢β hgvar id : sT = e, σi → cleanupd (ε)

if newd (υ) = ε

ρ ⊢β he, σi → υ

(26)

ρ ⊢β hgvar id : sT = e, σi → hρ1 , σ1 i

if newd (υ) = (σ1 , l) and ρ1 = id 7→ (l, sT) .
Local variable declaration.
ρ ⊢β he, σi → ε

(27)

ρ ⊢β hlvar id : sT = e, σi → unmarks (ε)
ρ ⊢β he, σi → υ
ρ ⊢β hlvar id : sT = e, σi → unmarks (ε)

(25)

if news (υ) = ε

ρ ⊢β he, σi → υ
ρ ⊢β hlvar id : sT = e, σi → hρ1 , σ1 i

if news (υ) = (σ1 , i) and ρ1 = id 7→ (i, sT) .
Function declaration.
ρ ⊢β function id(fps) = body0 , σ → hρ0 , σi

(28)

(29)

(30)

if ρ0 = {id 7→ λ fps . body1 } and either body0 = body1 = extern : sT or, for each
i ∈ {0, 1}, bodyi = let di in s result e, I = FI(body0 ) \ DI(fps) and d1 = ρ |I ; d0 .

22

·

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

Recursive declaration.
(ρ \ J) ⊢β[β1 ] hg, σi → hρ0 , σ0 i

ρ ⊢β hrec ρ0 , σ0 i → η

(31)

ρ ⊢β hrec g, σi → η
if J = FI(g) ∩ DI(g), β ⊢FI(g) g : β0 and β1 = β0 |J .
Global sequential composition.
ρ ⊢β hg0 , σi → ε

(32)

ρ ⊢β hg0 ; g1 , σi → ε
ρ ⊢β hg0 , σi → hρ0 , σ0 i ρ[ρ0 ] ⊢β[β0 ] hg1 , σ0 i → ε
ρ ⊢β hg0 ; g1 , σi → ε

if β ⊢FI(g0 ) g0 : β0

ρ ⊢β hg0 , σi → hρ0 , σ0 i ρ[ρ0 ] ⊢β[β0 ] hg1 , σ0 i → hρ1 , σ1 i
ρ ⊢β hg0 ; g1 , σi → ρ0 [ρ1 ], σ1

(33)

if β ⊢FI(g0 ) g0 : β0
(34)

Local sequential composition.
ρ ⊢β hd0 , σi → ε

(35)

ρ ⊢β hd0 ; d1 , σi → ε
ρ ⊢β hd0 , σi → hρ0 , σ0 i ρ[ρ0 ] ⊢β[β0 ] hd1 , σ0 i → ε
ρ ⊢β hd0 ; d1 , σi → ε

if β ⊢FI(d0 ) d0 : β0

ρ ⊢β hd0 , σi → hρ0 , σ0 i ρ[ρ0 ] ⊢β[β0 ] hd1 , σ0 i → hρ1 , σ1 i
ρ ⊢β hd0 ; d1 , σi → ρ0 [ρ1 ], σ1

(36)

if β ⊢FI(d0 ) d0 : β0
(37)

5.5.3

Statements

Nop.
(38)

ρ ⊢β hnop, σi → σ
Assignment.
ρ ⊢β he, σi → ε
ρ ⊢β hid := e, σi → ε
ρ ⊢β he, σi → hsval, σ0 i


ρ ⊢β hid := e, σi → σ0 ρ(id) := sval

(39)

(40)

Statement sequence.
ρ ⊢β hs0 , σi → ε

(41)

ρ ⊢β hs0 ; s1 , σi → ε
ρ ⊢β hs0 , σi → σ0

ρ ⊢β hs1 , σ0 i → η

ρ ⊢β hs0 ; s1 , σi → η

(42)

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

Block.
ρ ⊢β d, marks (σ) → ε

(43)

ρ ⊢β hd; s, σi → ε
ρ ⊢β d, marks (σ) → hρ0 , σ0 i

23

ρ[ρ0 ] ⊢β[β0 ] hs, σ0 i → η

ρ ⊢β hd; s, σi → unmarks (η)

if β ⊢FI(d) d : β0
(44)

Conditional.
ρ ⊢β he, σi → ε

(45)

ρ ⊢β hif e then s0 else s1 , σi → ε
ρ ⊢β he, σi → htt, σ0 i

ρ ⊢β hs0 , σ0 i → η

(46)

ρ ⊢β hif e then s0 else s1 , σi → η
ρ ⊢β he, σi → hff, σ0 i ρ ⊢β hs1 , σ0 i → η

(47)

ρ ⊢β hif e then s0 else s1 , σi → η
While.
ρ ⊢β he, σi → ε

(48)

ρ ⊢β hwhile e do s, σi → ε
ρ ⊢β he, σi → hff, σ0 i

(49)

ρ ⊢β hwhile e do s, σi → σ0
ρ ⊢β he, σi → htt, σ0 i

ρ ⊢β hs, σ0 i → ε

(50)

ρ ⊢β hwhile e do s, σi → ε
ρ ⊢β he, σi → htt, σ0 i

ρ ⊢β hs, σ0 i → σ1

ρ ⊢β hwhile e do s, σ1 i → η

ρ ⊢β hwhile e do s, σi → η

(51)

Throw.
(52)

ρ ⊢β hthrow χ, σi → hσ, χi
ρ ⊢β he, σi → ε

(53)

ρ ⊢β hthrow e, σi → ε
ρ ⊢β he, σi → hsval, σ0 i

(54)

ρ ⊢β hthrow e, σi → hσ0 , svali
Try blocks.
ρ ⊢β hs, σi → σ0

(55)

ρ ⊢β htry s catch k, σi → σ0
ρ ⊢β hs, σi → ε0

ρ ⊢β hk, ε0 i → hu, ηi

ρ ⊢β htry s catch k, σi → η

if u ∈ {caught, uncaught}

(56)

24

·

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

ρ ⊢β hs0 , σi → σ0

ρ ⊢β hs1 , σ0 i → η

(57)

ρ ⊢β htry s0 finally s1 , σi → η
ρ ⊢β hs0 , σi → hσ0 , ξ0 i ρ ⊢β hs1 , σ0 i → σ1

(58)

ρ ⊢β htry s0 finally s1 , σi → hσ1 , ξ0 i
ρ ⊢β hs0 , σi → hσ0 , ξ0 i ρ ⊢β hs1 , σ0 i → ε

(59)

ρ ⊢β htry s0 finally s1 , σi → ε
Function call. Consider the following conditions:




β(id) = (fps → sT0 )
ρ(id) = λ id1 : sT1 , . . . , idn : sTn . body

(60)


d = (lvar x0 : sT0 = id0 ; lvar x1 : sT1 = e1 ; . . . ; lvar xn : sTn = en )


ρ1 = x0 7→ (0, sT0 ) ∪ idj 7→ (j, sTj ) j = 1, . . . , n , ρ0 : β0 , ρ1 : β1 . (61)

Then the rule schemata for function calls are the following:
ρ ⊢β d, marks (σ) → ε
ρ ⊢β id0 := id(e1 , . . . , en ), σ → ε

if (60) holds

(62)

ρ ⊢β d, marks (σ) → hρ0 , σ0 i
ρ[ρ1 ] ⊢β[β1 ] body, links (σ0 ) → ε

ρ ⊢β id0 := id(e1 , . . . , en ), σ → unmarks unlinks (ε)

if (60) and (61) hold
(63)

ρ ⊢β d, marks (σ) → hρ0 , σ0 i
ρ[ρ1 ] ⊢β[β1 ] body, links (σ0 ) → σ1
ρ[ρ0 ] ⊢β[β0 ] id0 := x0 , unlinks (σ1 ) → η2
ρ ⊢β id0 := id(e1 , . . . , en ), σ → unmarks (η2 )

(64)
if (60) and (61) hold

Note that parameter passing is implemented by using reserved identifiers that reference the return value (x0 ) and the actual arguments (x1 , . . . , xn ). 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 x0 is still mapped to the return value, whereas the arguments
are accessible using the formal parameters’ names id1 , . . . , idn .
5.5.4

Function Bodies.
ρ ⊢β d, marks (σ) → ε

(65)

ρ ⊢β hlet d in s result e, σi → ε
ρ ⊢β d, marks (σ) → hρ0 , σ0 i

ρ[ρ0 ] ⊢β[β0 ] hs, σ0 i → ε

ρ ⊢β hlet d in s result e, σi → unmarks (ε)

if β ⊢FI(d) d : β0 (66)

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

25

ρ ⊢β d, marks (σ) → hρ0 , σ0 i
ρ[ρ0 ] ⊢β[β0 ] hs, σ0 i → σ1
ρ[ρ0 ] ⊢β[β0 ] hx0 := e, σ1 i → η0
ρ ⊢β hlet d in s result e, σi → unmarks (η0 )

(67)
if β ⊢FI(d) d : β0

ρ ⊢β extern : sT, (µ, w) → η

(68)

if ∃σ0 = (µ0 , w) ∈ Mem, ξ ∈ Except . η = σ0 ∨ η = hσ0 , ξi.
5.5.5

Catch Clauses

Catch.
ρ ⊢β hs, σi → η0
ρ ⊢β (p) s, (σ, ξ) → hcaught, η0 i

(69)

if p = ξ ∈ RTSExcept, or p = type(ξ), or p = any.
ρ ⊢β (id : sT) s, (σ, sval) → caught, unmarks (ε0 )

if sT = type(sval) and ε0 = news sval, marks (σ) .


ρ {id 7→ (i, sT)} ⊢β[{id7→sT loc}] hs, σ0 i → η0

ρ ⊢β (id : sT) s, (σ, sval) → caught, unmarks (η0 )


if sT = type(sval) and (σ0 , i) = news sval, marks (σ) .
ρ ⊢β (p) s, (σ, ξ) → uncaught, (σ, ξ)

if, letting cT = type(ξ), we have p ∈
/ ξ, cT, any and ∀id ∈ Id : p 6= id : cT.
Catch sequence.
ρ ⊢β hk0 , εi → hcaught, η0 i
ρ ⊢β hk0 ; k1 , εi → hcaught, η0 i
ρ ⊢β hk0 , εi → huncaught, ε0 i ρ ⊢β hk1 , ε0 i → η
ρ ⊢β hk0 ; k1 , εi → η

(70)

(71)

(72)

(73)

(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, ρ ⊢β hs, σi −→ means that, in the context given by ρ and σ, the execution of
statement s diverges. We now give a set of rules that (interpreted coinductively,

26

·

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

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:
∞

∞

ρ ⊢β hs0 , σi → σ0 ρ ⊢β hs1 , σ0 i −→
====================
========
∞
ρ ⊢β hs0 ; s1 , σi −→

ρ ⊢β hs0 , σi −→
==============
∞
ρ ⊢β hs0 ; s1 , σi −→

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
P0

···

Pi−1

ρi ⊢βi Ni → ηi

Pi+1

···

Ph−1

ρ ⊢β N → η

(side condition)

(75)

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

P0 · · · Pi−1 ρi ⊢βi Ni −→
===============
=========
∞
ρ ⊢β N −→

(side condition)

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
def

ways (respecting, of course, the side conditions). Moreover, R = 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 ⊆ N⋆ is prefixclosed if, for each z ∈ N⋆ and each n ∈ N, zn ∈ P implies z ∈ P . A set P ⊆ N⋆ is
canonical if, for each z ∈ N⋆ there exists h ∈ N such that
{ n ∈ N | zn ∈ P } = {0, . . . , h − 1}.
An S-tree is a partial function θ : N⋆ ֌ S such that dom(θ) is prefix-closed and
canonical. The concrete semantics universe U is the set of all S-trees.
def

For each p ∈ dom(θ), the tree θ[p] defined, for each z ∈ N⋆ , by θ[p] (z) = θ(pz),
is called a subtree of θ; it is called a proper subtree if p 6= ǫ. If dom(θ) = ∅,

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

27

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 ∈ N may be zero); in this case θ can be denoted by

θ[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


θ0 , . . . , θh−1 ∈ U,
θ ··· θ
0
h−1
def
F+ (U ) =
θ0 (ǫ) · · · θh−1 (ǫ)

∈ R+

s
s

def





.




The set of positive concrete semantics trees is Θ+ = lfp⊆ (F+ ). Consider now the
co-continuous function F− : ℘(U) → ℘(U) given, for each U ∈ ℘(U), by



θ0 , . . . , θh−2 ∈ Θ+ , θh−1 ∈ U, 

θ ··· θ
0
h−1
def
.
F− (U ) =
θ
(ǫ)
·
·
·
θ
(ǫ)
0
h−1


∈ R−


s
s
def

The set of negative concrete semantics trees is Θ− = gfp⊆ (F− ). The set of all
def

concrete semantics trees is Θ = Θ+ ⊎ Θ− .
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 → η) η ∈ Tq


∞
⊎ (ρ ⊢β N −→) .

Proof. If q = e and η ∈ Te , we say that the sequent (ρ ⊢β N → η) is well-typed
if N = he, σ0 i and η = hsval, σ1 i imply β ⊢ e : type(sval). For the proof, let
def

S+ (ρ, β, N ) =



s s = (ρ ⊢β N → η), η ∈ Tq , (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 R0 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, R0 6= ∅. Let j ≥ 0
be the maximal value for which there exist finite trees θ0 , . . . , θj−1 ∈ Θ+ where
P0 = θ0 (ǫ), . . . , Pj−1 = θj−1 (ǫ) are the first j premises of a rule in R0 . Let Rj ⊆ R0
be the set of all rules in R0 with P0 , . . . , Pj−1 as their first j premises; then Rj 6= ∅.
By inspecting the rule schemata in Section 5.5, it can be seen that, if there exists

28

·

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

P0 ··· Pj−1 Pj′ ···
s′

∈ Rj for some Pj′ ∈ S+ (ρj , βj , Nj ) and s′ ∈ S+ (ρ, β, N ), then6

P0 · · · Pj−1 Pj · · ·
∈ Rj .
(76)
s
Suppose that q ∈ {e, d, g} so that we can also assume N = hu, σi. 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 R0 have no premises (so that j = 0) and hence, letting θ ∈ Θ+
be the singleton tree consisting of the conclusion of a rule in R0 , we obtain that
θ(ǫ) ∈ S+ (ρ, β, N ). Otherwise, u is not atomic, we show that each of the rules in
Rj has exactly j premises; to do this, we assume there exists a rule in Rj with a
β
(j + 1)-th premise Pj and derive a contradiction. Let Nj ∈ Γqjj be the non-terminal
configuration in Pj . By inspecting the rule schemata in Section 5.5 in the case that
q ∈ {e, d, g}, it can be seen that:
∀Pj ∈ S+ (ρj , βj , Nj ) : ∃s ∈ S+ (ρ, β, N ) .

(i) qj ∈ {e, d, g} so that Nj has the form huj , σj i;
(ii) uj is a substructure of u unless Rj consists of instances of the schematic
rule (31) and j = 1.
If uj is a substructure of u, by property (i), we can apply structural induction to
obtain that there exists a finite tree θj ∈ Θ+ such that Pj = θj (ǫ) ∈ S+ (ρj , βj , Nj );
hence, by property (76), there exists a rule in Rj having Pj as its (j + 1)-th premise;
contradicting the assumption that j was maximal. Otherwise, by property (ii), if
uj is not a substructure of u, the rules in R0 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 Rj as its conclusion; and again we have
a contradiction. Thus, for any uj , all rules in Rj have exactly j premises. By Defiθ ··· θ
nition 5.7, θ = 0 s j−1 ∈ Θ+ 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 θ
def

∞

n
(U). To this end, we reason by
such that θ(ǫ) = s∞ = (ρ ⊢β N −→) and θ ∈ F−
induction on n ≥ 0. By our assumption that there is no tree θ ∈ Θ+ such that
θ(ǫ) ∈ S+ (ρ, β, N ), there must exist a rule

P0 · · · Pj−1 Pj · · ·
∈ Rj
s
β

for some Pj ∈ S+ (ρj , βj , Nj ); let qj be such that Nj ∈ Γqjj . By the maximality
of j, there is no tree in Θ+ whose root is Pj . We have already shown that, if
6 To

help understand this property, we illustrate it in the case that q = e and the non-terminal
configuration is N = hb0 and b1 , σi; hence the concrete rule schemata (15)–(17) will apply. In all
the rule instances, the first premise is of the form P0 = (ρ ⊢β N0 → η0 ), where N0 = hb0 , σi; as
˛
˘
¯
def
a consequence, we have S+ (ρ, β, N0 ) = (ρ ⊢β N0 → η0 ) ˛ η0 ∈ B , where B = ExceptState ⊎
{ ht, σ0 i ∈ Te | 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 = hff, σ0 i and rule (17) when η0 = htt, σ0 i. Thus property (76) holds for j = 0.
Moreover, although only rule (17) applies when j = 1, the terminal configuration for the second
premise (P1 ) is just any terminal configuration in Te . Thus property (76) also holds for j = 1.

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

29

qj ∈ {e, d, g}, then there exists a tree θj ∈ Θ+ such that θj (ǫ) ∈ S+ (ρj , βj , Nj );
thus, by property (76), there must be a rule in Rj whose (j + 1)-th premise is θj (ǫ);
contradicting the assumption that j ≥ 0 is maximal. Hence qj ∈ {s, b, k}. By
the definition of the negative concrete semantics rules in Section 5.6, there exists a
corresponding negative rule
P0 · · · Pj−1 P∞
∈ R−
s∞
∞

such that P∞ = (ρj ⊢βj Nj −→). Hence, by Definition 5.6, there exists a tree in
0
U = F−
(U) with root s∞ , so that the inductive hypothesis holds for n = 0. Suppose
n−1
now that n > 0. By the inductive hypothesis, there exists a tree θ∞ ∈ F−
(U)
θ0 ··· θj−1 θ∞
n
such that θ∞ (ǫ) = P∞ . Hence, by Definition 5.7,
∈ F− (U). Thus, for
s∞
n
all n ≥ 0, there exists a tree in F−
(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
def
structure σi = (∅, ǫ) ∈ 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 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 = hρ0 , σ0 i, then the concrete semantics
is

∞
{θ0 } ∪ θ ∈ Θ θ(ǫ) = (ρ0 ⊢β N → η) or θ(ǫ) = (ρ0 ⊢β N −→) ,

where N = x := main() , σ0 ∈ Γβs and ∅ ⊢∅ (g; gvar 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

30

·

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

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 c1 ⊑ c2 holds if c1
is a stronger property than c2 (i.e., c2 approximates c1 ). 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 6∝ 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 Di be a set of concrete
objects and consider the corresponding

powerset lattice ℘(Di ), ⊆, ∅, Di , ∩, ∪ ; let also Di♯ be an abstract domain related
to ℘(Di ) by the concretization function γi : Di♯ → ℘(Di ).
6.1.1 Approximation of Cartesian Products. Values of the Cartesian product
D1 × D2 can be approximated by elements of the Cartesian product D1♯ × D2♯ .

Namely, the component-wise ordered abstract domain D1♯ × D2♯, ⊑, ⊥, ⊔ is related
to the concrete powerset lattice ℘(D1 ×D2 ), ⊆, ∅, D1 ×D2 , ∩, ∪ by the concretization function γ : (D1♯ × D2♯ ) → ℘(D1 × D2 ) defined, for each (d♯1 , d♯2 ) ∈ D1♯ × D2♯ ,
by
def 
γ(d♯1 , d♯2 ) = (d1 , d2 ) ∈ D1 × D2 d1 ∈ γ1 (d♯1 ), d2 ∈ γ2 (d♯2 ) .
(77)

Hence, (d1 , d2 ) ∝ (d♯1 , d♯2 ) holds if and only if d1 ∝ d♯1 and d2 ∝ d♯2 .
If the underlying approximations D1♯ and D2♯ are both strict, then a better approximation scheme can be obtained by adopting the strict product (also called
7 Let f : D × · · · × D → D , where (D , ⊑ , ⊥ , ⊔ ) is a bounded join-semilattice, for each i = 0,
n
1
0
i
i
i
i
. . . , n. Then, function f is strict on the i-th argument if di = ⊥i implies f (d1 , . . . , dn ) = ⊥0 .

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

31

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,
def 
D1♯ ⊗ D2♯ = (d♯1 , d♯2 ) ∈ D1♯ × D2♯ d♯1 = ⊥ if and only if d♯2 = ⊥ .
The concretization function is defined exactly as in (77). The constructor function
· ⊗ · : (D1♯ × D2♯ ) → (D1♯ ⊗ D2♯ ) is defined by
(
(d♯1 , d♯2 ), if d♯1 6= ⊥ and d♯2 6= ⊥;
♯ def
♯
d1 ⊗ d2 =
⊥,
otherwise.

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 D1 ∩D2 = ∅. Then, values of the disjoint union D = D1 ⊎D2 can be
approximated by elements of the Cartesian product D♯ = D1♯ ×D2♯ . In this case, the
abstract domain D♯ is related to the concrete powerset lattice ℘(D), ⊆, ∅, D, ∩, ∪
by means of the concretization function γ : (D1♯ × D2♯ ) → ℘(D1 ⊎ D2 ) defined, for
each (d♯1 , d♯2 ) ∈ D1♯ × D2♯ , by
def

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

The concrete domain of integers ℘(Integer), ⊆, ∅, Integer, ∩, ∪ is correctly ap
proximated 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 ) ⊇ m0 + m1 m0 ∈ γ(m♯0 ), m1 ∈ γ(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 ) ⊇ m0 ÷ m1 m0 ∈ γ(m♯0 ), m1 ∈ γ(m♯1 ), m1 6= 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♯ ) .

32

·

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

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 ) ⊇ t0 ∨ t1 t0 ∈ γ(t♯0 ), t1 ∈ γ(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 ‘,’, ‘6,’, ‘⊳’, ‘E’, ‘D’
and ‘⊲’ on Integer♯ that are strict on each argument and sound with respect to the
pointwise extensions over ℘(Integer) of the corresponding relational operators ‘=’,
‘6=’, ‘<’, ‘≤’, ‘≥’ 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 ) ⊇ m0 = m1 m0 ∈ γ(m♯0 ), m1 ∈ γ(m♯1 )
for each m♯0 , m♯1 ∈ Integer♯ . Likewise for ‘6,’, ‘⊳’, ‘E’, ‘D’ and ‘⊲’.
6.4 Approximation of Storable Values

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

integers and Booleans, is abstracted by the domain sVal♯ = 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,
def
are approximated by elements of the domain Except♯ = 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

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

33

Mem♯ are denoted by σ ♯ , σ0♯ , σ1♯ and so forth. We assume that, for each σ ∈ Mem,
there exists σ ♯ ∈ Mem♯ such that σ ∝ σ ♯ .
def
The abstract domain of value states is ValState♯ = sVal♯ ⊗ Mem♯ . Elements of
♯
♯
♯
ValState will be denoted by υ ♯ , υ0 , υ1 and so forth.
def

The abstract domain of exception states is ExceptState♯ = 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

newd ♯ : ValState♯ → (Mem♯ × Loc) ⊎♯ ExceptState♯ ,

news ♯ : ValState♯ → (Mem♯ × Ind) ⊎♯ ExceptState♯

are assumed to be such that, for each υ ∈ ValState and υ ♯ ∈ ValState♯ such that
υ ∈ γ(υ ♯ ), and each h ∈ {d, s}: if newh (υ) = (σ, a) (resp., newh (υ) = ε) and
newh ♯ (υ ♯ ) = (σ ♯ , a′ ), ε♯ , then σ ∈ γ(σ ♯ ) and a = a′ (resp., ε ∈ γ(ε♯ )).
The abstract memory structure data cleanup function
cleanupd ♯ : ExceptState♯ → ExceptState♯

is such that, for each ε♯ ∈ ExceptState♯ , we have
 
γ cleanupd ♯ (ε♯ ) ⊇ cleanupd (ε) ε ∈ γ(ε♯ ) .
The abstract functions

{mark♯s , unmark♯s , link♯s , unlink♯s } ⊆ Mem♯ → Mem♯
are defined to be such that, for each σ ♯ ∈ Mem♯ :
 
γ mark♯s (σ ♯ ) ⊇ marks (σ) σ ∈ γ(σ ♯ ) ,
 
γ unmark♯s (σ ♯ ) ⊇ unmarks (σ) σ ∈ γ(σ ♯ ) and unmarks (σ) is defined ,
 
γ link♯s (σ ♯ ) ⊇ links (σ) σ ∈ γ(σ ♯ ) and links (σ) is defined ,
 
γ unlink♯s (σ ♯ ) ⊇ unlinks (σ) σ ∈ γ(σ ♯ ) and unlinks (σ) 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

34

·

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

ε♯ = (σ ♯ , ξ ♯ ) ∈ ExceptState♯ ,

def
unmark♯s (σ ♯ , ξ ♯ ) = unmark♯s (σ ♯ ), ξ ♯ ,

def
unlink♯s (σ ♯ , ξ ♯ ) = 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 ∈ Mem σ ∈ γ(σ ♯ ), ρ ⊢β he, σi → htt, σtt i .
γ(σ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♯ ,

γ(ε♯ ),
if p = any;
 
+
♯
γ φ (p, ε ) ⊇
(σ, ξ) ∈ γ(ε♯ ) ξ = p ,
if p ∈ RTSExcept;



(σ, ξ) ∈ γ(ε♯ ) ξ ∈ dom type(p) , otherwise;

∅,
if p = any;
 
−
♯
♯
γ φ (p, ε ) ⊇
(σ, ξ) ∈ γ(ε ) ξ 6= p ,
if p ∈ RTSExcept;



♯
(σ, ξ) ∈ γ(ε ) ξ ∈
/ dom type(p) , otherwise.
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
def

mem(ε♯ ) = σ ♯ ;

♯

χ ,
def
sel(cT, ε♯ ) = m♯ ,

♯
t,

if cT = rts exception;
if cT = integer;
if cT = boolean.

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

35

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 β ∈ TEnvI and respectively, by
def 
he, σ ♯ i ∈ Exp × Mem♯ ∃sT ∈ sType . β ⊢I e : sT ,
Γβ♯
e =

def
Γβ♯
hd, σ ♯ i ∈ Decl × Mem♯ ∃δ ∈ TEnv . β ⊢I d : δ ,
d =
def 
hg, σ ♯ i ∈ Glob × Mem♯ ∃δ ∈ TEnv . β ⊢I g : δ ,
Γβ♯
g =
def 
Γβ♯
hs, σ ♯ i ∈ Stmt × Mem♯ β ⊢I s ,
s =
def 
hbody, σ ♯ i ∈ Body × Mem♯ ∃sT ∈ sType . β ⊢I body : sT ,
Γβ♯
b =
def 
Γβ♯
hk, ε♯ i ∈ Catch × ExceptState♯ β ⊢I k .
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 = hq1 , σi ∈ Γβq and
N ♯ = hq2 , σ ♯ i ∈ Γβ♯
q ,
N ∝ N ♯ ⇐⇒ (q1 = q2 ∧ σ ∝ σ ♯ ).

(78)

For each N = hk1 , εi ∈ Γβk and N ♯ = hk2 , ε♯ i ∈ Γβ♯
k ,
N ∝ N ♯ ⇐⇒ (k1 = k2 ∧ ε ∝ ε♯ ).

(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
def

Te♯ = ValState♯ ⊎♯ ExceptState♯ ,
def

def

Td♯ = Tg♯ = (Env × Mem♯ ) ⊎♯ ExceptState♯ ,

36

·

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

def

Ts♯ = Tb♯ = Mem♯ ⊎♯ ExceptState♯ ,
def

Tk♯ = Ts♯ ⊎♯ ExceptState♯ .
We write η ♯ to denote a terminal abstract configuration.
The approximation relation η ∝ η ♯ between concrete and abstract terminal configurations is defined as follows. For expressions,
(
υ ∝ υ ♯ , if η = υ;
η ∝ hυ ♯ , ε♯ i ⇐⇒
(80)
ε ∝ ε♯ , if η = ε.
For local and global declarations,
(
(ρ1 = ρ2 ∧ σ ∝ σ ♯ ),
♯
♯
η ∝ (ρ2 , σ ), ε ⇐⇒
ε ∝ ε♯ ,
For statements and function bodies,
(
σ ∝ σ♯ ,
η ∝ hσ ♯ , ε♯ i ⇐⇒
ε ∝ ε♯ ,

if η = hρ1 , σi;
if η = ε.

(81)

if η = σ;
if η = ε.

(82)

if η = hcaught, ηs i;
if η = huncaught, εi.

(83)

For catch sequences,
η∝

hηs♯ , ε♯ i

⇐⇒

(

ηs ∝ ηs♯ ,
ε ∝ ε♯ ,

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
β ∈ TEnvI , for each ρ0 , ρ1 ∈ EnvJ such that ρ0 : β |J and ρ1 : β |J , for each
♯
♯
q ∈ {e, d, g, s, b, k}, N ∈ Γβq , η ∈ Tq , N ♯ ∈ Γβ♯
q and η ∈ Tq , by
(ρ0 ⊢β N → η) ∝ (ρ1 ⊢β N ♯ → η ♯ ) ⇐⇒ (ρ0 = ρ1 ∧ N ∝ N ♯ ∧ η ∝ η ♯ );
∞

♯

♯

♯

(ρ0 ⊢β N −→) ∝ (ρ1 ⊢β N → η ) ⇐⇒ (ρ0 = ρ1 ∧ N ∝ N ).

(84)
(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 ) ֌ Tq ,

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

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

37

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♯ ρ, he, σ ♯ i holds. Similarly, one can specify

supported♯ ρ, hid := e, σ ♯ i 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♯ ρ, hid1 ∗ id2
, σ ♯ i holds provided ρ : I, id1 , id2 ∈ I and, for at least one
♯
i ∈ {1, 2}, γ σ ρ(idi ) = {m}, for some integer value m. Similarly, the design

can impose that supported♯ ρ, hid ∗ id, σ ♯ i 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 η ∈ Tq .
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

P0 · · · Pℓ−1
ρ ⊢β N ♯

η0♯

(side condition)

to denote
P0 · · · Pℓ−1
ρ ⊢β N ♯ → η ♯

(side condition) and η0♯ ⊑ η ♯

where ‘⊑’ is the natural ordering relation on the appropriate abstract lattice (i.e.,
one of the Tq♯ , 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 followingrules for the abstract evaluation
of expressions apply only if supported♯ ρ, he, σ ♯ i does not hold, where e is the
expression being evaluated. This side condition will be left implicit in order not to
clutter the presentation.

38

·

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

Constant.
ρ ⊢β hcon, σ ♯ i

(86)

α({con}) ⊗ σ ♯ , none♯

Identifier.
ρ ⊢β hid, σ ♯ i
Unary minus.

(87)



σ ♯ ρ(id)

ρ ⊢β he, σ ♯ i → (m♯ , σ0♯ ), ε♯
ρ ⊢β h−e, σ ♯ i

(88)

(⊖ m♯ , σ0♯ ), ε♯

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:
ρ ⊢β he0 , σ ♯ i → (m♯0 , σ0♯ ), ε♯0

ρ ⊢β he1 , σ0♯ i → (m♯1 , σ1♯ ), ε♯1
(m♯0 ⊚ m♯1 , σ1♯ ), ε♯0 ⊔ ε♯1

ρ ⊢β he0  e1 , σ ♯ i

(89)

if  ∈
/ {/, %} or 0 6∝ m♯1 .
ρ ⊢β he1 , σ0♯ i → (m♯1 , σ1♯ ), ε♯1

ρ ⊢β he0 , σ ♯ i → (m♯0 , σ0♯ ), ε♯0
ρ ⊢β he0  e1 , σ ♯ i

(m♯0 ⊚ m♯1 , σ1♯ ), ε♯0 ⊔ ε♯1 ⊔ ε♯2

(90)

if  ∈ {/, %}, 0 ∝ m♯1 and ε♯2 = σ1♯ ⊗ α({divbyzero}).
Arithmetic tests. Let  ∈ {=, 6=, <, ≤, ≥, >} be an abstract syntax operator and
let ⊲⊳ : (Integer♯ × Integer♯ ) → Bool♯ denote the corresponding abstract test operation in {,, 6,, ⊳, E, D, ⊲}. Then the rules for the abstract arithmetic tests are
given by
ρ ⊢β he1 , σ0♯ i → (m♯1 , σ1♯ ), ε♯1

ρ ⊢β he0 , σ ♯ i → (m♯0 , σ0♯ ), ε♯0

(m♯0 ⊲⊳ m♯1 , σ1♯ ), ε♯0 ⊔ ε♯1

ρ ⊢β he0  e1 , σ ♯ i

(91)

Negation.
ρ ⊢β hb, σ ♯ i → (t♯ , σ0♯ ), ε♯
ρ ⊢β hnot b, σ ♯ i

(92)

(⊖ t♯ , σ0♯ ), ε♯

Conjunction.
ρ ⊢β hb0 , σ ♯ i → hυ0♯ , ε♯0 i
ρ ⊢β hb0 and b1 , σ ♯ i

♯
ρ ⊢β hb1 , σtt
i → hυ1♯ , ε♯1 i

υff♯ ⊔ υ1♯ , ε♯0 ⊔ ε♯1

,

(93)

♯
if σtt
= φ(ρ, σ ♯ , b0 ), σff♯ = φ(ρ, σ ♯ , not b0 ) and υff♯ = α({ff}) ⊗ σff♯ .
Disjunction.

ρ ⊢β hb0 , σ ♯ i → hυ0♯ , ε♯0 i
ρ ⊢β hb0 or b1 , σ ♯ i

ρ ⊢β hb1 , σff♯ i → hυ1♯ , ε♯1 i
♯
hυtt
⊔ υ1♯ , ε♯0 ⊔ ε♯1 i

(94)

·

On the Design of Generic Static Analyzers for Modern Imperative Languages

39

♯
♯
♯
if σtt
= φ(ρ, σ ♯ , b0 ), σff♯ = φ(ρ, σ ♯ , not b0 ) and υtt
= α({tt}) ⊗ σtt
.

6.9.2 Unsupported
 Declarations. The following rules only apply if the condition
supported♯ ρ, hq, σ ♯ i does not hold, where q ∈ Decl ⊎ Glob is the declaration being
evaluated. Again, this side condition is left implicit.
Nil.
ρ ⊢β hnil, σ ♯ i

(∅, σ ♯ ), none♯

(95)

(ρ0 , σ ♯ ), none♯

(96)

Environment.
ρ ⊢β hρ0 , σ ♯ i

Recursive environment.
ρ ⊢β hrec ρ0 , σ ♯ i
if ρ1 =
∪



(

(97)

(ρ1 , σ ♯ ), none♯

id 7→ ρ0 (id) ρ0 (id) = λfps . extern : sT
id 7→ abs1

∀i ∈ {0, 1} : absi = λfps . let di in s result e,

ρ0 (id) = abs0 , d1 = rec ρ0 \ DI(fps) ; d0

)

.

Global variable declaration.

ρ ⊢β he, σ ♯ i → hυ ♯ , ε♯0 i
ρ ⊢β hgvar id : sT = e, σ ♯ i
(ρ1 , σ1♯ ), cleanupd ♯ (ε♯0 ⊔ ε♯1 )


if newd ♯ (υ ♯ ) = (σ1♯ , l), ε♯1 and ρ1 = id 7→ (l, sT) .

(98)

Local variable declaration.

ρ ⊢β he, σ ♯ i → hυ ♯ , ε♯0 i
ρ ⊢β hlvar id : sT = e, σ ♯ i
(ρ1 , σ1♯ ), unmark♯s (ε♯0 ⊔ ε♯1 )


if news ♯ (υ ♯ ) = (σ1♯ , i), ε♯1 and ρ1 = id 7→ (i, sT) .

(99)

Function declaration.

ρ ⊢β function id(fps) = body0 , σ ♯

(ρ0 , σ ♯ ), none♯

(100)

if ρ0 = {id 7→ λ fps . body1 } and either body0 = body1 = extern : sT or, for each
i ∈ {0, 1}, bodyi = let di in s result e, I = FI(body0 ) \ DI(fps) and d1 = ρ |I ; d0 .
Recursive declaration.
(ρ \ J) ⊢β[β1 ] hg, σ ♯ i → (ρ0 , σ0♯ ), none♯
ρ ⊢β hrec g, σ ♯ i

ρ ⊢β hrec ρ0 , σ0♯ i → η ♯
η♯

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

(101)

·

40

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

Global sequential composition.
ρ[ρ0 ] ⊢β[β0 ] hg1 , σ0♯ i → (ρ1 , σ1♯ ), ε♯1

ρ ⊢β hg0 , σ ♯ i → (ρ0 , σ0♯ ), ε♯0

(ρ0 [ρ1 ], σ1♯ ), ε♯0 ⊔ ε♯1

ρ ⊢β hg0 ; g1 , σ ♯ i

(102)

if β ⊢I g0 : β0 and FI(g0 ) ⊆ I.
Local sequential composition.
ρ[ρ0 ] ⊢β[β0 ] hd1 , σ0♯ i → (ρ1 , σ1♯ ), ε♯1

ρ ⊢β hd0 , σ ♯ i → (ρ0 , σ0♯ ), ε♯0

(ρ0 [ρ1 ], σ1♯ ), ε♯0 ⊔ ε♯1

ρ ⊢β hd0 ; d1 , σ ♯ i

(103)

if β ⊢I d0 : β0 and FI(d0 ) ⊆ I.
6.9.3 Unsupported Statements. The following rules only apply if the implicit
side condition supported♯ ρ, hs, σ ♯ i does not hold, where s is the statement being
evaluated.
Nop.
ρ ⊢β hnop, σ ♯ i

(104)

σ♯

Assignment.
ρ ⊢β he, σ ♯ i → (sval♯ , σ0♯ ), ε♯0
ρ ⊢β hid := e, σ ♯ i

hσ1♯ , ε♯0

⊔

ε♯1 i

Statement sequence.
ρ ⊢β hs0 , σ ♯ i → hσ0♯ , ε♯0 i



if σ0♯ ρ(id) :=♯ sval♯ = (σ1♯ , ε♯1 )

ρ ⊢β hs1 , σ0♯ i → hσ1♯ , ε♯1 i

(106)

σ1♯ , ε♯0 ⊔ ε♯1

ρ ⊢β hs0 ; s1 , σ ♯ i

(105)

Block.
ρ ⊢β d, mark♯s (σ ♯ ) → (ρ0 , σ0♯ ), ε♯0

ρ[ρ0 ] ⊢β[β0 ] hs, σ0♯ i → hσ1♯ , ε♯1 i

unmark♯s (σ1♯ ), ε♯0 ⊔ unmark♯s (ε♯1 )

ρ ⊢β hd; s, σ ♯ i

(107)

if β ⊢FI(d) d : β0 .
Conditional.
ρ ⊢β he, σ ♯ i → hυ0♯ , ε♯0 i

♯
ρ ⊢β hs0 , σtt
i → hσ1♯ , ε♯1 i

ρ ⊢β hs1 , σff♯ i → hσ2♯ , ε♯2 i
ρ ⊢β hif e then s0 else s1 , σ ♯ i

(108)

hσ1♯ ⊔ σ2♯ , ε♯0 ⊔ ε♯1 ⊔ ε♯2 i

♯
if σtt
= φ(ρ, σ ♯ , e) and σff♯ = φ(ρ, σ ♯ , not e).
While.
♯
ρ ⊢β he, σ ♯ i → hυ0♯ , ε♯0 i ρ ⊢β hs, σtt
i → hσ1♯ , ε♯1 i

ρ ⊢β hwhile e do s, σ1♯ i → hσ2♯ , ε♯2 i
ρ ⊢β hwhile e do s, σ ♯ i
if

♯
σtt

= φ(ρ, σ ♯ , e) and

σff♯

hσff♯

⊔

σ2♯ , ε♯0

= φ(ρ, σ ♯ , not e).

⊔

ε♯1

⊔

ε♯2 i

(109)

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

41

Throw.
ρ ⊢β hthrow χ, σ ♯ i

h⊥, ε♯ i

if ε♯ = σ ♯ ⊗ α({χ})

ρ ⊢β he, σ ♯ i → (sval♯ , σ0♯ ), ε♯0
ρ ⊢β hthrow e, σ ♯ i

if ε♯1 = σ0♯ ⊗ sval♯

h⊥, ε♯0 ⊔ ε♯1 i

(110)

(111)

Try blocks.
ρ ⊢β hs, σ ♯ i → hσ0♯ , ε♯0 i ρ ⊢β hk, ε♯0 i → (σ1♯ , ε♯1 ), ε♯2
ρ ⊢β htry s catch k, σ ♯ i
ρ ⊢β hs0 , σ ♯ i → σ0♯ , (σ1♯ , ξ1♯ )

hσ0♯ ⊔ σ1♯ , ε♯1 ⊔ ε♯2 i
ρ ⊢β hs1 , σ0♯ i → hσ2♯ , ε♯2 i
ρ ⊢β hs1 , σ1♯ i → hσ3♯ , ε♯3 i
σ2♯ , ε♯2

♯

ρ ⊢β htry s0 finally s1 , σ i

(112)

⊔

ε♯3

⊔

(σ3♯

⊗

(113)

ξ1♯ )

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♯ ) → hσ1♯ , ε♯1 i
ρ[ρ0 ] ⊢β[β0 ] id0 := x0 , unlink♯s (σ1♯ ) → hσ2♯ , ε♯2 i
ρ ⊢β id0 := id(e1 , . . . , en ), σ ♯

(114)

unmark♯s (σ2♯ ), ε♯


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 ] hs, σ0♯ i → hσ1♯ , ε♯1 i
ρ[ρ0 ] ⊢β[β0 ] hx0 := e, σ1♯ i → hσ2♯ , ε♯2 i
ρ ⊢β hlet d in s result e, σ ♯ i

(115)

unmark♯s (σ2♯ ), ε♯3

if β ⊢FI(d) d : β0 , ε♯3 = ε♯0 ⊔ unmark♯s (ε♯1 ⊔ ε♯2 ).

ρ ⊢β hextern : sT, σ ♯ i

σ0♯ , (σ0♯ , ⊤)

(116)


if ∀σ, σ0 ∈ Mem : σ = (µ, w) ∧ σ ∝ σ ♯ ∧ σ0 = (µ0 , w) =⇒ σ0 ∝ σ0♯ .
6.9.5

Catch Clauses

Catch.
ρ ⊢β s, mem(ε♯0 ) → η1♯
ρ ⊢β (p) s, ε♯

hη1♯ , ε♯1 i

(117)

42

·

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

if p = any or p = χ or p = cT, ε♯0 = φ+ (p, ε♯ ) and ε♯1 = φ− (p, ε♯ ).


ρ {id 7→ (i, sT)} ⊢β[{id7→sT loc}] hs, σ2♯ i → hσ3♯ , ε♯3 i

(118)
(σ4♯ , ε♯4 ), ε♯1



if ε♯0 = φ+ (sT, ε♯ ), ε♯1 = φ− (sT, ε♯ ), news ♯ sT(ε♯0 ), mark♯s mem(ε♯0 ) = (σ2♯ , i), ε♯2 ,
ρ ⊢β (id : sT) s, ε♯

σ4♯ = unmark♯s (σ3♯ ) and ε♯4 = unmark♯s (ε♯2 ) ⊔ unmark♯s (ε♯3 ).
Catch sequence.
ρ ⊢β hk0 , ε♯ i → (σ0♯ , ε♯0 ), ε♯1

ρ ⊢β hk1 , ε♯1 i → (σ1♯ , ε♯2 ), ε♯3
(σ0♯ ⊔ σ1♯ , ε♯0 ⊔ ε♯2 ), ε♯3

ρ ⊢β hk0 ; k1 , ε♯ i

(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,
P0

···

ρ ⊢β N

Pℓ−1
♯

η♯

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

we also have the rule
P0
ρ ⊢β N

···
♯

Pℓ−1

eval♯ (ρ, N ♯ )

if (side condition) and supported♯ (ρ, N ♯ )

Notice that even if eval♯ (ρ, N ♯ ) does not depend on the rule antecedents P0 , . . . , 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

 ♯
♯
♯
θ♯ (ǫ) · · · θℓ−1
(ǫ)
θ0 · · · θℓ−1
def
♯
∈ R♯ .
{θ0♯ , . . . , θℓ−1
} ⊆ U ♯, 0
F ♯ (U ♯ ) =
s
s
def

The set of abstract semantics trees is Θ♯ = gfp⊆ (F ♯ ).

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

43

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 ♯ → η ♯ ) η ♯ ∈ Tq♯ .
Proof. For the proof, let8
def 
♯
S+
(ρ, β, N ♯ ) = 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 R0 ∈ R♯ with ℓ premises and a conclusion
♯
(ρ, β, N ♯ ). If, on the other hand, supported♯ (ρ, N ♯ ) does hold, then it follows
in S+
from Section 6.9.6 that, by Definition 6.7, eval♯ (ρ, N ♯ ) is defined and, for each
rule in R0 , there is a rule
set of premises but where the conclusion
 with the same
♯
ρ ⊢β N ♯ → eval♯ (ρ, N ♯ ) is also in S+
(ρ, β, N ♯ ). Thus, in both cases, by definition
♯
(ρ, β, N ♯ ).
of U ♯ , there exists a tree in U ♯ with root in S+
We prove that, for any n ∈ 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 P0 = θ0♯ (ǫ), . . . , Pj−1 = θj−1
(ǫ)
are the first j premises of a rule in R0 ; let Rj ⊆ R0 be the set of all rules in R0
with P0 , . . . , Pj−1 as their first j premises; then Rj 6= ∅. We assume that j < ℓ
and derive a contradiction. By inspecting the rule schemata in Section 6.9, it can
P0 ··· Pj−1 Pj′ ···
♯
∈ Rj for some Pj′ ∈ S+
(ρj , βj , Nj♯ ) and
be seen that, if there exists
ś♯
♯
ś♯ ∈ S+
(ρ, β, N ♯ ), then
♯
♯
∀Pj ∈ S+
(ρj , βj , Nj♯ ) : ∃s♯ ∈ S+
(ρ, β, N ♯ ) .

P0 · · · Pj−1 Pj · · ·
∈ Rj .
s♯

(120)

By the inductive hypothesis, there exists θj♯ ∈ F ♯(n−1) (U ♯ ) such that Pj = θj♯ (ǫ) ∈
♯
S+
(ρj , βj , Nj♯ ); hence, by (120), there must be a rule in Rj whose (j + 1)-th premise
is Pj ; contradicting the assumption that j < ℓ is maximal. Hence j = ℓ. Thus there
P ··· P
♯
(ρ, β, N ♯ ); hence, by Definition 6.9,
exists a rule 0 s♯ ℓ−1 ∈ R0 for some s♯ ∈ S+
θ ♯ ··· θ ♯

the tree 0 s♯ ℓ−1 ∈ 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.
8 For

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

44

·

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

Definition 7.1. (‘∝’ for trees.) Let ∝ : ℘(Θ × Θ♯ ) → ℘(Θ × Θ♯ ) be given, for
each U ∈ ℘(Θ × Θ♯ ), by




θ(ǫ) ∝ θ♯ (ǫ),


def
♯
♯
.
∝(U ) = (θ, θ ) ∈ Θ × Θ ∀i ∈ dom(θ) ∩ N :




∃j ∈ dom(θ♯ ) ∩ N . θ , θ♯ ∈ U 
[i]

[j]

Then θ ∝ θ♯ if and only if (θ, θ♯ ) ∈ gfp⊆ (∝).

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 = hq, σi where q ∈ {e, d, g, s, b}. By Definition 6.1,
we can always find σ ♯ ∈ Mem♯ such that σ ∝ σ ♯ . Hence, letting N ♯ = hq, σ ♯ i,
by (78) in Definition 6.4, we obtain N ∝ N ♯ . Next suppose N = hk, εi, 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 ♯ = hk, σ ♯ ⊗ ξ ♯ i, 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



∞

θ(ǫ) ∈ ρ ⊢β N → η, ρ ⊢β N −→ , 


def
S = (θ, θ♯ ) ∈ Θ × Θ♯ θ♯ (ǫ) = ρ ⊢β N ♯ → η ♯ ,
.




♯
N ∝N

(121)

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

Proof. Let θ ∈ Θ and θ♯ ∈ Θ♯ . We define:
def

r =

θ[0] (ǫ) · · · θ[h−1] (ǫ)
θ(ǫ)

def

r♯ =

♯
♯
θ[0]
(ǫ) · · · θ[ℓ−1]
(ǫ)

θ♯ (ǫ)

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

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

45

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⊆ (∝). To this end, by the principle of
fixpoint coinduction, we will show that (θ, θ♯ ) ∈ ∝(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]
) ∈ ∝(S); similarly, if θ ∈ Θ− and i 6= h − 1, by the inductive hypothesis,

♯
we can assume that, (θ[i] , θ[j]
) ∈ ∝(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-

46

·

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

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
id
−e
e0  e1

2
3
4
5
6/7
8

m0  m1
not b
b0 and b1

b0 or b1

9
10/11
12
13
14
15
16
17
18–20

86
87
88
89
90
89
90
90
91
92
93

94

hcon, σi
σ[ρ(id)]
ε
h−m, σ0 i
ε
hm0 ◦ m1 , σ1 i

α({con}) ⊗ σ♯
none♯
♯
σ [ρ(id)]
(⊖ m♯ , σ0♯ )
ε♯
(m♯0
(m♯0
(m♯0
(m♯0
(m♯0
(m♯0

⊚ m♯1 , σ1♯ )
⊚ m♯1 , σ1♯ )
⊚ m♯1 , σ1♯ )
⊚ m♯1 , σ1♯ )
⊚ m♯1 , σ1♯ )
⊲⊳ m♯1 , σ1♯ )

ε♯0 ⊔ ε♯1
ε♯0 ⊔ ε♯1 ⊔ ε♯2
ε♯0 ⊔ ε♯1
ε♯0 ⊔ ε♯1 ⊔ ε♯2
ε♯0 ⊔ ε♯1 ⊔ ε♯2
ε♯0 ⊔ ε♯1

hσ1 , divbyzeroi
ε
hm0 ≶ m1 , σ1 i
ε
(⊖ t♯ , σ0♯ )
ε♯
h¬ t, σ0 i
♯
ε
υff
⊔ υ1♯
ε♯0 ⊔ ε♯1
hff, σ0 i
η
Similar to the rows for ‘b0 and b1 ’

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 ‘cleanupd ’, ‘unmarks ’, ‘unlinks ’,
‘unmark♯s ’ and ‘unlink♯s ’ by ‘cud ’, ‘ums ’, ‘uls ’, ‘ums ♯ ’ and ‘uls ♯ ’, 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 = hE, σi and N ♯ = hE, σ ♯ i, 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, σ ∝ σ ♯

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

47

so that hcon, σi ∝ α({con}) ⊗ σ ♯ . Hence ηe ∝ ηe♯ .
Identifier. Suppose r isan instance
σ ∝ σ ♯ , by

 of (3).
 Since, by hypothesis,
♯
♯
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 m0 ∝ 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
♯
(ǫ) implies σ1 ∝ σ1♯
ηe ∝ ηe♯ . If r is an instance of (8), then property θ[1] (ǫ) ∝ θ[1]

and m1 ∝ m♯1 so that, by the soundness of ‘⊚’, (m0  m1 ) ∝ (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 hσ1 , divbyzeroi ∝ σ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
♯
♯
) ∈ S and property (ii) holds. By (122), θ[1] (ǫ) ∝ θ[1]
(ǫ).
m0 ∝ m♯0 . Thus (θ[1] , θ[1]

If r is an instance of (11), then ε ∝ ε♯1 ; and if r is an instance of (12), σ1 ∝ σ1♯ and
m1 ∝ m♯1 so that, by soundness of ‘⊲⊳’, (m0 ≶ m1 ) ∝ (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.
and in the following, whenever we need to prove ι ∝ ι♯0 ⊔ ι♯1 , we just prove either ι ∝ ι♯0 or
ι ∝ ι♯1 and implicitly use the monotonicity of γ.

9 Here

48

·

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

Table II.

Corresponding concrete and abstract rules and terminals for declarations
˙
¸
Q
r
r♯
ηq
ηq♯ = (ρ♯a , σa♯ ), ε♯a
(ρ♯a , σa♯ )
ε♯a

nil
ρ0
rec ρ0
gvar id : sT = e
lvar id : sT = e
function id(fps) : sT = e
rec g
g0 ; g1
d0 ; d1

21
22
23
24/25
26
27/28
29
30
31
32/33
34
35–37

95
96
97
98
99
100
101
102
103

h∅, σi
hρ0 , σi
hρ1 , σi
cud (ε)
hρ1 , σ1 i
ums (ε)
hρ1 , σ1 i
hρ0 , σi
η
ε˙
¸
ρ0 [ρ1 ], σ1
Similar

(∅, σ♯ )
(ρ0 , σ♯ )
(ρ1 , σ♯ )
(ρ1 , σ1♯ )

none♯
none♯
none♯
cud ♯ (ε♯0 ⊔ ε♯1 )

(ρ1 , σ1♯ )

ums ♯ (ε♯0 ⊔ ε♯1 )

(ρ0 , σ♯ )

none♯
η♯
(ρ0 [ρ1 ], σ1♯ )
ε♯0 ⊔ ε♯1
to the rows for ‘g0 ; g1 ’

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 b0 ). Thus, since
ff ∝ α({ff}) holds by definition, we have hff, σ0 i ∝ υ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 η ∝ hυ1♯ , ε♯1 i.
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 ∈ {Td , Tg } and ηq♯ ∈ {Td♯ , Tg♯ }, the actual domains for ηq and ηq♯ will depend on
context.
By (121) we have N ∝ N ♯ . Thus letting N = hQ, σi and N ♯ = hQ, σ ♯ i 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,
♯
) ∈ S so that, as h = 1, property (ii) holds. By (122),
by the hypothesis (θ[0] , θ[0]
♯
♯
θ[0] (ǫ) ∝ θ[0]
(ǫ). If r is an instance of (24), then θ[0] (ǫ) ∝ θ[0]
(ǫ) implies ε ∝ ε♯0 ;

by Definition 6.1 and monotonicity of γ, we have cleanupd (ε) ∝ cleanupd ♯ (ε♯0 ⊔ ε♯1 ),
♯
i.e., ηq ∝ ηq♯ . If r is an instance of (25) or (26), then θ[0] (ǫ) ∝ θ[0]
(ǫ) implies
υ ∝ υ ♯ . By Definition 6.1, newd (υ) ∝ newd ♯ (υ ♯ ). By the side condition for abstract

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

49


rule (98), newd ♯ (υ) = (σ1♯ , l), ε♯1 . By the side conditions for (25) and (26), either
newd (υ) = ε ∝ ε♯1 —and hence cleanupd (ε) ∝ cleanupd ♯ (ε♯0 ⊔ε♯1 ) by Definition 6.1—
or newd (υ) = (σ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 unmarks , unmark♯s , news , news ♯ and
i in place of cleanupd , cleanupd ♯ , newd , newd ♯ 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 hy♯
♯
pothesis, (θ[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
♯
♯
(ǫ).
) ∈ S. By (122), θ[0] (ǫ) ∝ θ[0]
1 ≤ h ≤ 2 and (θ[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 = hs, σi and N ♯ = hs, σ ♯ i, 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), hsval, σ0 i ∝ hsval♯0 , σ0♯ i 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♯ .

50

·

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

Table III.
S

Corresponding concrete and abstract rules and terminals for statements
r
r♯
ηs
ηs♯ = hσa♯ , ε♯a i
♯
σa
ε♯a

nop
id := e
s0 ; s1
d; s
if e then s0 else s1
while e do s0

throw s

try s catch k
try s0 finally s1

id := id0 (e1 , . . . , en )

38
39
40
41
42
43
44
45
46/47
48/50
49
51
52
53
54
55
56
57
58
59
62
63
64

104
105
106
107
108
109

110
111
112
113

114

σ
ε ˆ
˜
σ0 ρ(id) := sval
ε
η
ε
ums (η)
ε
η
ε
σ0
η
hσ, χi
ε
hσ0 , svali
σ0
η
η
hσ1 , ξ0 i
ε
ε
`
´
ums uls (ε)
ums (η2 )

σ♯
σ1♯

none♯
ε♯0 ⊔ ε♯1

σ1♯

ε♯0 ⊔ ε♯1

ums ♯ (σ1♯ )

ε♯0 ⊔ ums ♯ (ε♯1 )

σ1♯ ⊔ σ2♯

ε♯0 ⊔ ε♯1 ⊔ ε♯2

♯
⊔ σ2♯
σff

ε♯0 ⊔ ε♯1 ⊔ ε♯2

⊥

ε♯
ε♯0 ⊔ ε♯1

σ0♯ ⊔ σ1♯

ε♯1 ⊔ ε♯2

σ2♯

ε♯2 ⊔ ε♯3 ⊔ (σ3♯ ⊗ ξ1♯ )

ums ♯ (σ2♯ )

ε♯ = ε♯0
´
`
⊔ ums ♯ uls ♯ (ε♯1 )
⊔ ums (ε♯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 η ∝ hσ1♯ , ε♯1 i. 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 η ∝ hσ1♯ , ε♯1 i and therefore, by Definition 6.1,

unmarks (η) ∝ 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 htt, σ0 i ∝ ht♯ , σtt i and, if ff ∝ t♯ , then
♯
hff, σ0 i ∝ ht♯ , σff i. Hence, if (46) applies, θ[1] (ǫ) ∝ θ[1]
(ǫ) so that η ∝ hσ1♯ , ε♯1 i; and,

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

51

♯
if (47) applies, θ[1] (ǫ) ∝ θ[2]
(ǫ) so that η ∝ hσ2♯ , ε♯2 i. 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 Definition 6.2, if tt ∝ t♯ , then htt, σ0 i ∝ ht♯ , σtt i and, if ff ∝ t♯ , then hff, σ0 i ∝ ht♯ , σff i.
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)
♯
(ǫ) so that ε ∝ ε♯1 . Hence ηs ∝ ηs♯ .
holds. By (122), θ[1] (ǫ) ∝ θ[1]
♯
If r is an instance of (51), then h = 3. Thus (θ[1] , θ[1]
) ∈ S. By (122), θ[1] (ǫ) ∝
♯
♯
(ǫ) so that σ1 ∝ σ1♯ . Thus (θ[2] , θ[2]
) ∈ S and property (ii) holds. By (122),
θ[1]
♯
(ǫ) so that η ∝ hσ2♯ , ε♯2 i. Hence ηs ∝ ηs♯ .
θ[2] (ǫ) ∝ θ[2]

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 hu, ηi ∝ (σ1♯ , ε♯1 ), ε♯2 where

u ∈ {caught, uncaught}. By Definition 6.5, if u = caught, then η ∝ hσ1♯ , ε♯1 i 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 η ∝ hσ2♯ , ε♯2 i. Hence ηs ∝ ηs♯ .

If r is an instance of (58) or (59), hσ0 , ξ0 i ∝ hσ1♯ , ξ1♯ i; hence σ0 ∝ σ1♯ and ξ0 ∝ ξ1♯ so
♯
♯
that (θ[1] , θ[2]
) ∈ S and property (ii) holds. By (122), θ[1] (ǫ) ∝ θ[2]
(ǫ). Thus, if (58)
applies, σ1 ∝ hσ3♯ , ε♯3 i so that hσ1 , ξ0 i ∝ (σ3♯ ⊗ ξ1♯ ); and, if (59) applies, ε ∝ hσ3♯ , ε♯3 i
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]
(ǫ).

52

·

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

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

extern : sT

65
66
67
68

115

116

ε
ums (ε)
ums (η0 )
σ0 | hσ0 , ξi

ums ♯ (σ2♯ )

ε♯3 = ε♯0
⊔ ums ♯ (ε♯1 ⊔ ε♯2 )

σ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, unmarks unlinks (ε) ∝ 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 ∝ hσ2♯ , ε♯2 i; by

Definition 6.1, unmarks (η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 = hB, σi and N ♯ = hB, σ ♯ i, 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 Defini♯
♯
tion 6.1, marks (σ) ∝ 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♯ .
♯
) ∈ S and, as h = 2, propIf r is an instance of (66), σ0 ∝ σ0♯ ; hence (θ[1] , θ[1]
♯
erty (ii) holds. By (122), θ[1] (ǫ) ∝ θ[1]
(ǫ) so that ε ∝ ε♯1 . By Definition 6.1,

unmarks (ε) ∝ unmark♯s (ε♯1 ); hence ηb ∝ ηb♯ .
♯
If r is an instance of (67), σ0 ∝ σ0♯ ; hence (θ[1] , θ[1]
) ∈ S. By (122) we have
♯
♯
) ∈ S; as h = 3, property (ii)
(ǫ), so that σ1 ∝ σ1♯ ; hence (θ[2] , θ[2]
θ[1] (ǫ) ∝ θ[1]
♯
holds. Again, by (122), θ[2] (ǫ) ∝ θ[2]
(ǫ); hence, η0 ∝ hσ2♯ , ε♯2 i. By Definition 6.1,

unmarks (η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 = hK, εi and N ♯ = hK, ε♯ i, 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 .

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

53

Table V. Corresponding concrete and abstract rules and terminals for catch clauses
K
r
r♯
ηk
ηk♯ = hηa♯ , ε♯a i
ηa♯
ε♯a
(any) s | (χ) s | (sT) s
(id : sT) s
(χ) s | (sT) s
(id : sT) s
k0 ; k1

69
70
71
72
72
73
74

117
118
117
118
119

hcaught, η0 i
˙
¸
caught, ums (ε0 )
hcaught, η0 i
˙
¸
uncaught, (σ, ξ)
˙
¸
uncaught, (σ, ξ)
hcaught, η0 i
η

η1♯
`
(σ4 , ε4 ) = ums ♯ (σ3♯ ),
´
ums ♯ (ε♯2 ) ⊔ ums ♯ (ε♯3 )
η1♯
(σ3♯ , ε♯2 ⊔ ε♯3 )
(σ0♯ ⊔ σ1♯ , ε♯0 ⊔ ε♯2 )

ε♯1
ε♯1
ε♯1
ε♯1
ε♯3

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,




news sval, marks (σ) ∝ news ♯ 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 = news sval, marks (σ) so that by (123), ε0 ∝ ε♯2 ; by Definition 6.1,
unmarks (ε0 ) ∝ unmark♯s (ε♯2 ). If (71) applies, then, by the side condition, (σ0 , i) =

♯
) ∈ S and, as h = 1,
news sval, marks (σ) so that by (123), σ0 ∝ σ2♯ . Hence, (θ[0] , θ[0]

♯
(ǫ), which implies η0 ∝ hσ3♯ , ε♯3 i. Thus, by
property (ii) holds. By (122), θ[0] (ǫ) ∝ θ[0]

Definition 6.1, unmarks (η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 hcaught, η0 i ∝ (σ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, huncaught, ε0 i ∝ (σ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 η ∈ Ts . If the concretization functions relating the concrete and
abstract domains are strict, then the abstract tree above will encode the following
definite information:

54

·

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

—non-terminating computations (i.e., unreachable code), if η ♯ = ⊥;
—non-exceptional computations, if η ♯ = hσ ♯ , none♯ i and σ ♯ 6= ⊥;
—exceptional computations, if η ♯ = h⊥, ε♯ i and ε♯ 6= none♯ .
Obviously, a precise propagation of this definite information requires that all of the

abstract domain operators are strict too. Hence, if θ♯ (ǫ) = ρ ⊢β hs, ⊥i → η ♯ ,
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
g0 = (g; gvar x : integer = 0), where g is a valid program, we obtain that any ab
stract tree θ0♯ ∈ Θ♯ such that θ0♯ (ǫ) = ∅ ⊢∅ hg0 , σi♯ i → η0♯ correctly approximates

each concrete tree θ0 ∈ Θ such that θ0 (ǫ) = ∅ ⊢∅ hg0 , σi i → η0 . Notice that θ0♯ is
a finite tree. Letting η0♯ = (ρ0 , σ0♯ ), ε♯0 and assuming η0 ∈
/ ExceptState, we obtain

η0 = hρ0 , σ0 i, where σ0 ∝ σ0♯ . Hence, letting s0 = x := main() and ρ0 : β, any

abstract tree θ1♯ ∈ Θ♯ such that θ1♯ (ǫ) = ρ0 ⊢β hs0 , σ0♯ → η1♯ correctly approx-
imates each concrete tree θ1 ∈ Θ such that either θ1 (ǫ) = ρ0 ⊢β hs0 , σ0 → η1
∞ 
or θ1 (ǫ) = ρ0 ⊢β hs0 , σ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♯ ;
def

—for all increasing chains x♯0 ⊑ x♯1 ⊑ · · · , the increasing chain defined by y0♯ = x♯0
def

♯
and yi+1
= yi♯ ∇ (yi♯ ⊔ x♯i+1 ), for i ∈ N, is not strictly increasing.

The algorithm works by recursively constructing a finite approximation for the
abstract subtree rootedin the current node (initially, the root of the whole tree). Let
n = ρ ⊢β hq, yn♯ i → rn be the current node, where q is a uniquely labeled program

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

55

phrase,10 y ♯ ∈ D♯ is either an abstract memory σ ♯ ∈ Mem♯ or an abstract exception
state ε♯ ∈ ExceptState♯ , and rn 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 rn is
replaced by an abstract value computed according to the conclusion of the
rule.

♯
(ii) If there exists an ancestor node m = ρ ⊢β hq, ym
i → rm of n labeled by the
♯
same program phrase q and such that yn♯ ⊑ ym
, i.e., if node n is subsumed
by node m, then the node is not expanded further and the placeholder rn is
replaced by the least fixpoint of the equation rn = fm (rn ), where fm 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 = ρ ⊢β hq, ym
i → rm of n
♯
labeled by the same program phrase q, but the subsumption condition yn♯ ⊑ ym
♯
does not hold. Then, to ensure convergence, the abstract element yn in node
♯
♯
n is further approximated by ym
∇ (ym
⊔ yn♯ ) 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].
10 Unique

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.
11 As 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.

56

·

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

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.
def

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

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

Basic types. T ∈ Type = 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.

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

57

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

dom(float) = Float,

def

type(fl) = float,

def

type(sc) = signed char,

def

type(uc) = unsigned char.

dom(signed char) = sChar,
dom(unsigned char) = uChar,

def
def

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  ∈ {=, 6=, <, ≤, ≥, >}:
Expressions.
β ⊢I fl : float

β ⊢I sc : signed char

β ⊢I e : nT
β ⊢I uc : unsigned char

β ⊢I −e : nT
β ⊢I e0 : nT

β ⊢I e1 : nT

β ⊢I e0  e1 : nT
β ⊢I e : T 0
β ⊢I vcast(T1 , e) : T1

β ⊢I e0 : nT

β ⊢I e1 : nT

β ⊢I e0  e1 : boolean
if casting T0 to T1 is legal.

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
evalvc : (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  ∈ {=, 6=, <, ≤, ≥, >}, respectively. Such functions need
not be always defined: for example, there is no need to define eval+ (con0 , con1 , σ)
for the case type(con0 ) 6= type(con1 ).

58

·

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

Value casts. The following concrete rule schemata use the corresponding evaluation function to specify the execution of the vcast operator.
ρ ⊢β he, σi → ε

ρ ⊢β he, σi → hcon, σ0 i

ρ ⊢β hvcast(nT, e), σi → ε

ρ ⊢β hvcast(nT, e), σi → evalvc (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):
ρ ⊢β he, σi → hcon, σ0 i
ρ ⊢β h−e, σi → eval−1 (nT, con, σ0 )
ρ ⊢β he0 , σi → hcon0 , σ0 i ρ ⊢β he1 , σ0 i → hcon1 , σ1 i
ρ ⊢β he0  e1 , σi → eval (con0 , con1 , σ1 )
Arithmetic tests. Similarly, rule (12) is replaced by the more general rule
ρ ⊢β he0 , σi → hcon0 , σ0 i ρ ⊢β he1 , σ0 i → hcon1 , σ1 i
ρ ⊢β he0  e1 , σi → eval (con0 , con1 , σ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∗
sType ∋ sT ::= eT | rT

fType ∋ fT ::= fps → sT
mType ∋ mT ::= oT | fT

aType ∋ aT ::= array m of oT
dType ∋ dT ::= mT loc
rType ∋ rT ::= record id of id1 : oT1 , . . . , idj : oTj
We assume, without loss of generality, that the field names of record types are
unique across the entire program (for example, id1 , . . . , idj 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

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

59

‘∗’, 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
Stmt ∋ s ::= . . . | lval := e | lval := e(es)

Glob ∋ g ::= . . . | gvar id : aT = e
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:
β, dT0 ⊢I o : dT1 ,
β ⊢I lval : dT,

o is compatible with dT0 and has type dT1 in β;
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.
β ⊢I e : integer β, oT loc ⊢I o : dT
β, dT ⊢I  : dT

β, (array m of oT) loc ⊢I [e] · o : dT
β, oTi loc ⊢I o : dT

β, (record id of id1 : oT1 ; . . . ; idj : oTj ) loc ⊢I . idi · o : dT

if i ∈ {1, . . . , j}

Lvalue.
β, dT0 ⊢I o : dT1
β ⊢I id · o : dT1

if β(id) = dT0

β ⊢I e : mT ∗

β, mT loc ⊢I o : dT

β ⊢I (∗ e) · o : dT

Null pointer and address-of operator.
β ⊢I lval : mT loc
β ⊢I (pT) 0 : pT
12 The

β ⊢I & lval : mT∗

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

60

·

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

Type decay.
β ⊢I lval : sT loc

β ⊢I lval : (array m of oT) loc

β ⊢I lval : fT loc

β ⊢I val lval : sT

β ⊢I val lval : oT∗

β ⊢I val lval : fT∗

Pointer arithmetics.
β ⊢I e0 : oT ∗ β ⊢I e1 : integer

β ⊢I e0 : integer β ⊢I e1 : oT∗

β ⊢I e0 + e1 : oT∗
β ⊢I e0 : oT ∗

β ⊢I e0 + e1 : oT∗

β ⊢I e1 : integer

β ⊢I e0 : oT ∗

β ⊢I e0 − e1 : oT∗

β ⊢I e1 : oT∗

β ⊢I e0 − e1 : integer

Pointer comparison.
β ⊢I e0 : pT

β ⊢I e1 : pT

β ⊢I e0  e1 : boolean

where  ∈ {=, 6=, <, ≤, ≥, >}.

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 7→ oT loc}

β ⊢I gvar id : array m of oT = e : id 7→ (array m of oT) loc

if m > 0

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:
def

hence, we redefine dVal = 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:

newt : (Abstract × Mem) → (Mem × Loc) ⊎ ExceptState ,

newarrayd : (Integer × ValState) → (Mem × Loc) ⊎ ExceptState ,

newarrays : (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:
def

Map = (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 the Design of Generic Static Analyzers for Modern Imperative Languages

·

61

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 id1 : oT1 ; . . . ; idj : oTj , as follows and under
the following conditions:
D

E
def
µ(l, rT) = µ locfield(id1 , l, rT) , . . . , µ locfield(idj , l, rT) ,
where, for each l ∈ Loc and aT = array m of oT ∈ aType,
h

i
def
µ(l, aT) = µ 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 lnull ∈ Loc (the null pointer value) such that
(lnull , mT) ∈
/ dom(σ) for all σ ∈ Mem and mT ∈ mType; this also implies that
lnull 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 {=, 6=, <, ≤, ≥, >}) 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 define13
index : (Loc × ValState) ֌ ValState ⊎ ExceptState
as follows:
 def
index l, (m, σ) =
13 Functions

(

ε,
if firstof(l, σ) = ε;
ptrmove(m, l0 , σ0 ), if firstof(l, σ) = (l0 , σ0 ).

‘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.

62

·

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

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:
(
)
∃dT0 , dT1 ∈ dType .
β def
Γo = ho, l, σi ∈ Offset × Loc × Mem
,
β, dT0 ⊢I o : dT1
def 
Γβl = hlval, σi ∈ LValue × Mem ∃dT ∈ dType . β ⊢I lval : dT ,
def

def

To = Tl = (Loc × Mem) ⊎ ExceptState,

The dynamic concrete semantics is extended with the following rule schemata.
Offset.
ρ ⊢β h, l, σi → hl, σi
ρ ⊢β he, σi → ε

ρ ⊢β he, σi → υ

ρ ⊢β [e] · o, l, σ → ε

ρ ⊢β [e] · o, l, σ → ε

ρ ⊢β he, σi → υ

ρ ⊢β ho, l0 , σ0 i → η

ρ ⊢β [e] · o, l, σ → η

ρ ⊢β ho, l0 , σ0 i → η

if field(idi , l, σ) = (l0 , σ0 )

ρ ⊢β h. idi · o, l, σi → η

ρ ⊢β hid · o, σi → η

if index(l, υ) = (l0 , σ0 )

if field(idi , l, σ) = ε

ρ ⊢β h. idi · o, l, σi → ε

Lvalue.
ρ ⊢β ho, σ @ a, σi → η

if index(l, υ) = ε

if ρ(id) = (a, mT)

ρ ⊢β he, σi → ε

ρ ⊢β he, σi → hl0 , σ0 i ρ ⊢β ho, l0 , σ0 i → η

ρ ⊢β (∗ e) · o, σ → ε

ρ ⊢β (∗ e) · o, σ → η

Null pointer and address-of operator.
ρ ⊢β hlval, σi → η
ρ ⊢β (pT) 0, σ → hlnull , σi

ρ ⊢β h& lval, σi → η

Type decay.
ρ ⊢β hlval, σi → ε
ρ ⊢β hval lval, σi → ε
ρ ⊢β hlval, σi → hl, σ0 i
ρ ⊢β hval lval, σi → σ0 [l, sT]
ρ ⊢β hlval, σi → υ
ρ ⊢β hval lval, σi → firstof(υ)

if β ⊢FI(lval) lval : sT loc
if β ⊢FI(lval) lval : aT loc

On the Design of Generic Static Analyzers for Modern Imperative Languages

ρ ⊢β hlval, σi → υ
ρ ⊢β hval lval, σi → υ

·

63

if β ⊢FI(lval) lval : fT loc

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).
ρ ⊢β he0 , σi → hl, σ0 i

ρ ⊢β he1 , σ0 i → ε

ρ ⊢β he0  e1 , σi → ε
ρ ⊢β he0 , σi → hl, σ0 i

ρ ⊢β he1 , σ0 i → hm, σ1 i

ρ ⊢β he0  e1 , σi → ptrmove(m0 , l, σ1 )

if m0 =  m

ρ ⊢β he0 , σi → hm, σ0 i ρ ⊢β he1 , σ0 i → hl, σ1 i
ρ ⊢β he0 + e1 , σi → ptrmove(m, l, σ1 )
ρ ⊢β he0 , σi → hl0 , σ0 i ρ ⊢β he1 , σ0 i → hl1 , σ1 i
ρ ⊢β he0 − e1 , σi → ptrdiff(l0 , l1 , σ1 )
Pointer comparison. Let  denote a binary abstract syntax operator in the set
{=, 6=, <, ≤, ≥, >}. Then, the following are added to rule schemata (10)–(12).
ρ ⊢β he0 , σi → hl, σ0 i

ρ ⊢β he1 , σ0 i → ε

ρ ⊢β he0  e1 , σi → ε
ρ ⊢β he0 , σi → hl0 , σ0 i ρ ⊢β he1 , σ0 i → hl1 , σ1 i
ρ ⊢β he0  e1 , σi → ptrcmp (l0 , l1 , σ1 )
Assignment.
ρ ⊢β hlval, σi → ε

ρ ⊢β hlval, σi → (l, σ0 ) ρ ⊢β he, σ0 i → ε

ρ ⊢β hlval := e, σi → ε

ρ ⊢β hlval := e, σi → ε

ρ ⊢β hlval, σi → (l, σ0 )

ρ ⊢β he, σ0 i → hsval, σ1 i


ρ ⊢β hlval := e, σi → σ1 (l, sT) := sval

if β ⊢FI(e) e : sT

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.

64

·

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

(Multi-dimensional) Global array declaration. In the following rule schemata, let
n > 0, aT = array m1 of (. . . (array mn of sT) . . . ) and m = m1 × . . . × mn .
ρ ⊢β he, σi → η
ρ ⊢β hgvar id : aT = e, σi → cleanupd (ε)
if either η = ε, or η = υ and newarrayd (m, υ) = ε;
ρ ⊢β he, σi → υ
ρ ⊢β hgvar id : aT = e, σi → hρ0 , σ0 i

if newarrayd (m, υ) = (σ0 , l) and ρ0 = id 7→ (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 newt ) 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
(newh , deleteh 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∗
9.3.3

β ⊢I e : sT∗
β ⊢I delete e

Concrete Dynamic Semantics. This is extended with the schemata:

New expression.
ρ ⊢β he, σi → ε

ρ ⊢β he, σi → υ

ρ ⊢β hnew sT = e, σi → ε

ρ ⊢β hnew sT = e, σi → ε

ρ ⊢β he, σi → υ
ρ ⊢β hnew sT = e, σi → hl, σ0 i

if newh (υ) = ε

if newh (υ) = (σ0 , l)

Delete operator.
ρ ⊢β he, σi → ε

ρ ⊢β he, σi → υ

ρ ⊢β hdelete e, σi → ε

ρ ⊢β hdelete e, σi → deleteh (υ)

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

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

65

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
def 
GotoMode = goto(id) id ∈ Id ,
def 
SwitchMode = switch(sval) sval ∈ sVal ,
def 
ValMode = value(sval) sval ∈ sVal ,
def 
EnvMode = env(ρ) ρ ∈ Env ,
def 
ExceptMode = except(ξ) ξ ∈ Except ,
def

CtrlMode = GotoMode ⊎ SwitchMode ⊎ ValMode ⊎ EnvMode

66

·

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

⊎ 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, cm0 , cm1 and so forth.
def
A control state is an element of CtrlState = CtrlMode × Mem. Control states
are denoted by cs, cs0 , cs1 and so forth.
The concrete semantics of the goto statement can now be expressed by
ρ ⊢β goto id, (cm, σ) → hcm0 , σi
if cm = exec and cm0 = goto(id) or cm 6= exec and cm0 = cm.
The semantics of labeled statements is given by
ρ ⊢β s, (cm0 , σ) → η
ρ ⊢β l : s, (cm, σ)i → η
where cm0 = exec if cm = exec, or cm = goto(id) and l = id, or cm = switch(sval)
and l ∈ {default, sval}; otherwise cm0 = 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 by14
ρ ⊢β e, (exec, σ) → hcm0 , σ0 i
ρ ⊢β if e then s0 else s1 , (exec, σ) → hcm0 , σ0 i
ρ ⊢β e, (exec, σ) → value(tt), σ0

if cm0 ∈ ExceptMode

ρ ⊢β s0 , (exec, σ0 ) → hcm1 , σ1 i
ρ ⊢β s1 , (cm1 , σ1 ) → η

(124)

ρ ⊢β if e then s0 else s1 , (exec, σ) → η
if cm1 ∈ GotoMode;
ρ ⊢β e, (exec, σ) → value(tt), σ0

ρ ⊢β s0 , (exec, σ0 ) → hcm1 , σ1 i

ρ ⊢β if e then s0 else s1 , (exec, σ) → hcm1 , σ1 i
if cm1 ∈
/ GotoMode;
ρ ⊢β e, (exec, σ) → value(ff), σ0

ρ ⊢β s1 , (exec, σ0 ) → η

ρ ⊢β if e then s0 else s1 , (exec, σ) → η
ρ ⊢β s0 , (cm, σ) → hcm0 , σ0 i
ρ ⊢β if e then s0 else s1 , (cm, σ) → hcm0 , σ0 i
if cm ∈ GotoMode ⊎ SwitchMode and cm0 ∈
/ GotoMode ⊎ SwitchMode;
ρ ⊢β s0 , (cm, σ) → hcm0 , σ0 i ρ ⊢β s1 , (cm0 , σ0 ) → η
ρ ⊢β if e then s0 else s1 , (cm, σ) → η
14 Recall

that, in C, it is perfectly legal to jump into the “else branch” from the “then branch.”

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

67

if cm ∈ GotoMode ⊎ SwitchMode and cm0 ∈ GotoMode ⊎ SwitchMode;
ρ ⊢β if e then s0 else s1 , (cm, σ) → hcm, σi
if cm ∈
/ GotoMode ⊎ SwitchMode ⊎ {exec}.
Likewise, the semantics of the switch statement can be captured by:
ρ ⊢β e, (exec, σ) → hcm0 , σ0 i
ρ ⊢β switch e in s, (exec, σ) → hcm0 , σ0 i

if cm0 ∈ ExceptMode

ρ ⊢β e, (exec, σ) → value(sval0 ), σ0
ρ ⊢β s, (switch(sval0 ), σ0 ) → hcm1 , σ1 i
ρ ⊢β switch e in s, (exec, σ) → hcm2 , σ1 i
(
exec, if cm1 ∈ SwitchMode ⊎ {break},
if cm2 =
cm1 , otherwise;
ρ ⊢β s, (goto(id), σ) → hcm0 , σ0 i
ρ ⊢β switch e in s, (goto(id), σ) → hcm1 , σ0 i
(
exec, if cm0 = break,
if cm1 =
cm0 , otherwise;
ρ ⊢β switch e in s, (cm, σ) → hcm, σi

if cm ∈
/ GotoMode ⊎ {exec}.

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
ρ ⊢β hs, csi → hcm, σi
ρ ⊢β hloop s, csi → hcm, σi
ρ ⊢β hs, csi → goto(id), σ

if cm 6= goto(id) for each id ∈ SL(s)
ρ ⊢β loop s, goto(id), σ

ρ ⊢β hloop s, csi → η



→η

if id ∈ SL(s)

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

·

68

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

are straightforward; return e can be modeled as the assignment to the reserved
identifier x0 (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:
ρ ⊢β he, cs♯cond i → cs♯0

ρ ⊢β hs0 , cs♯then i → cs♯1

ρ ⊢β hif e then s0 else s1 , cs♯ i

ρ ⊢β hs1 , cs♯else i → cs♯2
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 ,
(
⊥,
if Φm (cs♯ , GotoMode ⊎ SwitchMode) = ⊥,
♯
csjump =
♯
Φm (cs1 , Cjump ), otherwise,

Cjump = 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:




∃σ ∈ Mem . cs = (exec, σ),



♯
♯
′
γ Φe (ρ, cs , e) ⊇ cs ∈ γ(cs ) ∃σ ∈ Mem
,




′
. ρ ⊢β he, csi → value(tt), σ
 
♯
♯
γ Φ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 im-

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

69

perative 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.

70

·

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

REFERENCES
B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, 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, SpringerVerlag, 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 polyhedra, 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, Università 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. Steinbrüggen, eds.), NATO ASI Series F. IOS Press, Amsterdam, NL, 1999.

On the Design of Generic Static Analyzers for Modern Imperative Languages

·

71

, The verification grand challenge and abstract interpretation, Verified Software: Theories,
Tools, Experiments (VSTTE) (ETH Zü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. 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 relation 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. Miné, 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.

72

·

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

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 MultipleAgent 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.

