Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Abstract Interpretation
The formal verification of a program (and more generally a
computer system) consists in proving that its semantics
(describing "what the program executions actually do") satisfies its
specification (describing "what the program executions are
supposed to do").
Abstract interpretation
[22,26] formalizes the idea
that this formal proof can be done at some level of abstraction where
irrelevant details about the semantics and the specification are
ignored. This amounts to proving that an abstract semantics
satisfies an abstract specification. An example of abstract
semantics is Hoare logic while examples of abstract specifications are
invariance, partial, or total correctness. This abstracts away from
concrete properties such as execution times.
Abstractions should preferably be sound (no conclusion derived
from the abstract semantics is wrong relative to the program concrete
semantics and specification). Otherwise stated, a proof that the
abstract semantics satisfies the abstract specification should imply
that the concrete semantics also satisfies the concrete specification.
Hoare logic is a sound verification method, debugging is not (since
some executions are left out), bounded model checking is not either
(since parts of some executions are left out). Unsound abstractions
lead to false negatives (the program may be claimed to be
correct/non erroneous with respect to the specification whereas it is
indeed incorrect).
Abstractions should also preferably be complete (no aspect of
the semantics relevant to the specification is left out). So if the
concrete semantics satisfies the concrete specification this should be
provable in the abstract. However program proofs are undecidable, and
so automatic tools for reasoning about programs are all incomplete
(for non trivial program properties such as safety, liveness, or
security) and must therefore fail on some programs. This can be
achieved by allowing the tool not to terminate, to be unsound (e.g. debugging tools omit possible executions), or to be incomplete (e.g. static analysis tools may produce false alarms). Incomplete
abstractions lead to false positives or false alarms
(the specification is claimed to be potentially violated by some
program executions while it is not).
Potentially non-terminating and unsound program verification tools are
easy to design. Terminating and sound tools are much more difficult
to design. Complete tools are impossible to design, by
undecidability. However static analysis tools producing very few or
no false alarms have been designed and used in industrial contexts for
specific families of properties and programs [42].
In all cases, abstract interpretation provides a systematic
construction method based on the effective approximation of the
concrete semantics, which can be (partly) automated and/or formally
verified.
Abstract interpretation aims at
providing a basic coherent and conceptual theory for
understanding in a unified framework the thousands of ideas, concepts,
reasonings, methods, and tools on formal program analysis and
verification [22,26];
guiding the correct formal design of automatic tools for program
analysis (computing an abstract semantics) and program
verification (proving that an abstract semantics satisfies an
abstract specification) [17].
2 What can be formalized by abstract interpretation?
Abstract interpretation is useful in computer science to formalize
reasonings involving the [sound [and complete]] approximation of the
semantics of formal systems. A non-exhaustive list of typical
examples of application is given below.
The analysis of properties of grammars as well as parsing are abstract
interpretations of the grammar operational semantics and its
abstractions (such as parse trees, protolanguages, or terminal
languages) [39].
The semantics of programs describes their possible runtime executions
in all possible execution environments at some level of abstraction.
The hierarchy of semantics, including trace, small-step, and big-step
operational semantics, relational semantics, denotational semantics,
predicate transformers, and axiomatic semantics in their angelic,
natural, and demoniac versions can be designed by abstract
interpretation [32,19]. An
extension to transfinite behaviors is useful to formalize e.g. semantic slicing [54].
Formal proofs of program correctness involve an abstraction since
specifications always ignore some aspects of program execution which
need not be taken into account in the proof [18].
Static analysis is the automatic determination of abstract program
properties
[22,44,26,15]
including Dataflow Analysis
[67], [26,36],
Set-based Analysis [35], etc. This was
the motivating application behind the introduction of the abstract
interpretation theory.
Static typing and type inference [97] can be
understood as an abstract interpretation of runtime type checking thus
providing a "correct by construction" design method
[16,11].
Model-checking exhaustively verifies temporal properties on a
finite model of hardware or software computer systems
[10]. This abstraction of a system into a
model is often left implicit. Abstract model checking, as
formalized by abstract interpretation, makes this abstraction explicit
[9], [36], .
Model-checking is reputed to be terminating, sound, and complete on the
model. From an abstract interpretation point of view, relating the
system to its model, it may be sound on the model but unsound on the
system (e.g. the model is correct for safety properties but wrong for
liveness properties), it is often incomplete (no finite model can
cover the specified behaviors of the system [100])
and, in practice, may explode combinatorially. In all cases abstract
interpretations of the system into a model have to be considered. All
transition models are abstract semantics but the converse is not true.
Predicate abstraction [61] can be used to reduce any
static analysis on a finite abstract domain to boolean fixpoint
computations as performed by a model-checker using a theorem prover to
automatically derive the abstract transformers involved in the
fixpoint definition. Parametric predicate abstraction is an extension
to infinite abstract domains [20].
Spurious counter-example-based refinement in abstract model-checking
is formalized as an abstract domain completion problem in the abstract
interpretation theory [56,43].
The problem of modifying finite abstract model checking by minimal
refinements in order to get strong preservation for some specification
language, including partition refinement algorithms, is a completion
problem in the abstract interpretation theory
[101].
Program transformations (such as partial evaluation
[72]) often require a static analysis of the
source program, as formalized by abstract interpretation (e.g. [71]). Moreover, the transformation itself, from source
to object programs, involves a loss of information on the original
program or a limitation on the possible program behaviors. This
approximation can be formalized by abstract interpretation. This was
exemplified on dead-code elimination, slicing, partial evaluation, or
program monitoring [38].
In language-based software security, the information to be hidden to an
intruder can be formalized as an abstract interpretation of the
program semantics [55].
The aim of code obfuscation is to prevent malicious users from
discovering properties of the original source program. This goal can
be precisely modeled by abstract interpretation, where the hiding of
properties corresponds to abstracting the semantics
[99].
An obfuscated malware is better detected by the effects of its
execution as recognized by an abstract interpretation rather than by a
syntactic signature [98].
A relational abstract-interpretation-based static analysis on a
well-founded abstract domain can be systematically extended to a
termination analysis [3] (whence liveness analyses).
Termination analysis may require probabilistic hypotheses [87] or fairness hypotheses
on parallel processes [78].
An abstract domain is an abstract algebra, often implemented as a
library module (see Sec. 5), providing a
description of abstract program properties and abstract property
transformers describing the operational effect of program instructions
and commands in the abstract. Abstract domains are often complete
lattices, an abstraction of powersets [26].
The first infinite abstract domain (that of intervals) was introduced
in [21]. This abstract domain was later used
to prove that, thanks to widenings, infinite abstract domains can lead
to effective static analyses for a given programming language that are
strictly more precise and equally efficient than any other one using a
finite abstract domain or an abstract domain satisfying chain
conditions [31].
3.3 Merge over all paths (MOP) in dataflow analysis
The
first dataflow analyses where proved correct by comparing the union of
the abstraction along all execution paths (so-called MOP1 solution) with a fixpoint solution
using transfer functions (i.e. abstract property transformer)
[67]. Instead of comparing one solution of the static
analysis problem to another one, the theory of abstract interpretation
introduced the idea that the correctness/soundness should be expressed
with respect to a formal semantics. A consequence is that static
analysis algorithms can be specified and designed by approximation of
a program semantics. Moreover, the "fixpoint solution" was shown to
be an abstraction of the "MOP solution". These two solutions coincide
for distributive abstract interpretations (for which abstract
transformers preserve union). Otherwise, the abstract domain used for
the fixpoint solution can be minimally enriched into its
disjunctive completion to get exactly the "MOP solution" in
fixpoint form (on the completed abstract domain)
[26].
The collecting semantics or non-standard semantics
(after the static semantics of [22]) is
the semantics of the language formally defining the program execution
properties of interest to be analyzed by abstraction. These program
executions themselves are formalized by the standard semantics.
For example in [22], the standard semantics is
an operational semantics. The concrete properties of interest are invariance
properties so the collecting semantics defines the reachable states
from initial states. This collecting semantics is expressed as the
least fixpoint of equations using strongest postcondition
transformers. Thus the considered abstractions provide abstract
invariance properties (overapproximating the reachable states).
Galois connections can be used when the abstract domain always offers
a most precise approximation of any concrete property
[26]. Indeed the Galois connections
introduced in [21,22] are
the semi-dual of the one introduced by Évariste Galois, and so do
compose (the abstraction of an abstraction is an abstraction).
Equivalent presentations involve closure operators, ideals,
congruences, etc [26].
An interesting consequence of the existence of the best abstraction of
concrete properties is the existence of best/most precise
transformers, which provides guidelines for their [automatic] design
[17]. Moreover by abstracting
fixpoints by fixpoints, static analysis is specified by an abstract
semantics expressed in fixpoint form whereas a static analyzer is an
algorithm for computing or overapproximating this fixpoint.
There are several alternative formalizations in absence of best
approximations [94], [30].
If the correspondance between the concrete and abstract properties is
given by a Galois connection, then the image of the abstract
properties in the concrete is a Moore family, which is the
image of the concrete properties by a closure operator
[26]. The formalization of the abstraction by
closure operators is useful to abstract away from the representation
of the concrete properties. Other equivalent formalizations of the
existence of the best abstraction of concrete properties include
principal ideals, complete join congruences, etc
[26].
If an abstract domains has no best approximations for some concrete
properties its Moore completion is the most abstract abstract
domain more expressive than the original abstract domain which has
this property [26]. This introduces a Galois
connection.
Most program properties can be expressed as fixpoints of monotone or
extensive property transformers, a property preserved by abstraction
[26]. This reduces program analysis to
fixpoint approximation and verification to fixpoint checking
[22].
Most (concrete and abstract) program properties can also be expressed
using inference rules, which indeed is equivalent to definitions
using fixpoints, equations, constraints, etc
[34]. This point of view has the advantage of
separating the design of an (abstract) semantics (or a static
analysis) from its formal presentation.
A standard method for fixpoints construction is iteration. This can
be extended to transfinite iterations to prove Tarski's fixpoint
theorem [25]. In practice one can accelerate the
fixpoint computation using appropriate iteration strategies formalized
as chaotic/asynchronous iterations [14]. This
extends to higher-order
[24], [74].
3.11 Convergence acceleration by widening/narrowing
Convergence acceleration is mandatory in infinite abstract domains in
which the iterative computation of abstract fixpoints may diverge.
Widenings/narrowings and their duals are universal methods to do so
[22,14]. This extends to
higher-order [24,6].
Thanks to Tarski's theorem, fixpoints can be re-expressed as equality
or inequality constraints whence static analysis can be equally viewed
as a fixpoint approximation or as a constraint resolution problem.
Some constraint resolution methods are mere fixpoint iteration (e.g. set-based analysis [35]).
The design of abstractions can be done by parts, by choosing basic
abstractions and then by composing them using abstract domain
combinators [26]. This provides a unifying
view on abstract domain design [52].
There are numerous examples of such abstract domain combinations
including the reduced sum, the reduced product and the
reduced power [26].
The enrichment of an abstract domain so has to express in the refined
domain properties which cannot be expressed in the original domain.
Examples are the Moore completionSec. 3.7, partitioning
[15,5,79], [69],
the disjunctive completion
[26], [53], the Heyting
completion [59],
complementation
[13], etc.
The refinement of an abstract domain into the most abstract abstract
domain which is precise enough to prove a given specification
[26], [93,57,58,104].
A consequence of the formalization of static analyses by Galois
connections is that they can be organized into a complete lattice
according to the partial order of their relative precisions
[26]. All semantics and analyses are
present in this formally defined lattice and so it remains to find the
useful ones, which is the real question!
4 Examples of abstract-interpretation-based static analyses
Contrary to dataflow analyses on lattices satisfying the
ascending/descending chain condition in the seventies, the
generalization to precise static analyses using numerical domains such
as intervals [21], octagons
[83] or polyhedra are
in infinite abstract domains whence required the introduction of new
widening-based iteration convergence acceleration methods to become
effective.
The analysis of the octagon in which the values of pairs of variables
do range (that is the determination of constraints of the form +/-x+/-y ≤ c where x and y are variables and c a rational
constant automatically discovered by the analysis)
[83,84,85].
The analysis of the polyhedron in which the values of tuples of
variables do range. This abstract interpretation can be used for the
automatic discovery of invariant linear inequalities among numerical
variables of a program [44].
Delay analysis in synchronous programs [64], safety
analysis of reactive systems [65], quantitative time
properties of synchronous programs, and linear hybrid systems
[66] are among the many applications.
The analysis of symbolic properties of programs, usually as opposed to
numerical program properties e.g. heap reachability analysis
[23,24]. Also understood as the
symbolic representation of abstract domains, which is almost always
the case, since abstract properties cannot generally be simplistically
represented as the set of concrete values which have this property
(except in enumerative model-checking [10]).
Strictness analysis determines whether a parameter in a lazy language
is always evaluated in a procedure call or this call does not
terminate. This information is useful to replace a call-by-need by a
more efficient call by value [91]. Introduced by Alan Mycroft
[92], this analysis was at the origin of the use of abstract
interpretation in the functional language community
[1,73]. Strictness analysis
[8,95] can be embedded in the lattice of
comportment analyses [33].
The necessity of optimizing Prolog implementations, in particular the
occur checks during unification, is at the origin of the use of
abstract interpretation for the static analysis of Prolog
[80,45,107,75,76,90,7,12,2],
[29].
The static analysis of imperative programs must take accesses and side
effects through aliases and pointers into account
[23]. The profuse literature on pointer analysis
is surveyed in [46,68].
Heap analysis consists in overapproximating the sets of sequences of
graphs representing the memory heap at all time instants during
execution. Applications range from memory leak detection to
shape analysis that is the determination of the shape of data
structures allocated on the heap [103,102].
The static analysis of concurrent programs from shared-memory
[28] to [a]synchronous
communication [27], a vast and difficult
subject, with few analyses that do scale up.
The analysis of dynamically allocated mobile processes (such as the
pi-calculus). This involves the overapproximation of the set of
sequences of graphs representing the process allocations and
communications at all time instants during execution
[109,51].
The notion of abstract domain in abstract interpretation (see
Sec. 3.1) is independent of particular
applications and can be implemented in libraries which can be used as
parts of many different static analyses and even substituted for one
another. Such libraries implement a representation of abstract
properties and algorithms encoding operations on these properties such
as logical operations, property transformers, widenings, etc.
The Parma Polyhedra Library (PPL)
is a user-friendly, fully dynamic, portable, exception-safe, and
efficient C++ library to handle convex polyhedra that can be defined
as the intersection of a finite number of (open or closed)
hyperspaces, each described by an equality or inequality (strict or
non-strict) with rational coefficients.
The Octagon Abstract Domain
Library is a library for manipulating special kinds of polyhedra
called octagons that correspond to sets of constraints of the form
+/-x +/-y ≤ c (where x and y are variables and c a rational
constant and so, in dimension two, these polyhedra have at most eight
faces) [85].
The following list of static analysis and verification automatic tools
provides an idea of the scope of practical applications of abstract
interpretation to software verification (but this list is definitely
not exhaustive). These tools aim at soundness. Since no universal
tool can exist (because of undecidability) such tools are necessarily
incomplete and vary in their capacity to produce very few false alarms and to
scale up to very large programs.
Commercial static analyzers from AbsInt
Angewandte Informatik to statically compute tight bounds for the
worst-case execution time (WCET) of tasks in real-time systems.
A static analyzer from the École normale
supérieure for proving the absence of runtime errors specialized
for synchronous control/command programs written in C.
TVLA is a research tool developed at
Tel Aviv University for experimenting
with abstract interpretation using a logical description of program
semantics with a predefined abstraction of predicates.
7 Conferences with abstract interpretation sessions
J. Berdine, A. Chawdhary, B. Cook, D. Distefano & P. O'Hearn. -
Varianceanalysesfrominvarianceanalyses. In :
34th POPL, edited by M. F. Martin Hofmann, Nice,
FR, 2007. pp. 211-224. -
ACM Press.
F. Bourdoncle. -
EfficientChaoticIterationStrategieswithWidenings.
In : Proc. FMPA, edited by D. Bjørner, M. Broy & I. Pottosin. Akademgorodok, Novosibirsk, RU, LNCS 735, pp.
128-141. -
Springer, 28 June -2 Jul. 1993.
M. Comini, F. Damiani & S. Vrech. -
On polymorphic recursion, type systems, and abstract interrpetation.
In : Proc. 15th Int. Symp.
SAS '08, edited by M. Alpuente & G. Vidal, pp. 144-158.
-
Springer, 2008, Valencia, ES, 16-18 Jul. 2008, LNCS 5079.
P. Cousot. -
Méthodes itératives de construction et
d'approximation de points fixes d'opérateurs
monotones sur un treillis, analyse sémantique de
programmes (in French). -
Grenoble, FR, Thèse d'État ès sciences
mathématiques, Université scientifique et
médicale de Grenoble, 21 Mar. 1978.
P. Cousot. -
VerificationbyAbstractInterpretation,invitedchapter.
In : Proc. Int. Symp. on Verification - Theory &
Practice - Honoring Zohar Manna's 64th Birthday, edited by
N. Dershowitz, pp. 243-268. -
Taormina, IT, LNCS 2772, Springer, 29 June - 4 Jul. 2003.
P. Cousot & R. Cousot. -
ModularStaticProgramAnalysis,invitedpaper.
In : Proc. 11th Int. Conf.
CC '2002, edited by R. Horspool, Grenoble, FR, 6-14 Apr. 2002.
pp. 159-178. -
LNCS 2304, Springer.
P. Cousot & R. Cousot. -
GrammarAnalysisandParsingbyAbstractInterpretation,invitedchapter. In : Program Analysis and Compilation, Theory
and Practice: Essays dedicated to Reinhard Wilhelm, edited by T. Reps,
M. Sagiv & J. Bauer, pp. 178-203. -
Springer, 2006, LNCS 4444.
P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux & X. Rival. -
The ASTRéEanalyser.
In : Proc. 14th ESOP '2005, Edinburg,
UK, edited by M. Sagiv, pp. 21-30. -
Springer, 2-10 Apr. 2005, LNCS, Vol. 3444.
P. Cousot, P. Ganty & J.-F. Raskin. -
Fixpoint-GuidedAbstractionRefinements.
In : Proc. 14th Int. Symp.
SAS '07, edited by G. Filé & H. Riis-Nielson, pp.
333-348. -
Springer, 22-24 Aug. 2007, Kongens Lyngby, DK, LNCS 4634.
S. Debray & D. Warren. -
AutomaticmodeinferencingforPrologprograms. In :
Proc. 1986 Int. Symp. on Logic Programming, pp. 78-88. -
IEEE Comp. Soc. Press, Sep. 1986, Salt Lake City, UT.
A. Di Pierro, C. Hankin & H. Wiklicky. -
Probabilistic lambda calculus and quantitative program analysis.
J. Logic and Comp., Vol. 15, n&86; 2, 2005, pp.
159-179.
C. Ferdinand, R. Heckmann, M. Langenbach, F. Martin, M. Schmidt, H. Theiling,
S. Thesing & R. Wilhelm. -
ReliableandPreciseWCETDeterminationforaReal-LifeProcessor. In : Proc.
1st Int. Work. EMSOFT '2001, edited by
T. Henzinger & C. Kirsch, pp. 469-485. -
Springer, 2001, LNCS, Vol. 2211.
C. Ferdinand, F. Martin, R. Wilhelm & M. Alt. -
Cache behavior prediction by abstract interpretation. Sci.
Comput. Programming, Vol. 35, n&86; 1, 1999, pp.
163-189.
R. Giacobazzi & I. Mastroeni. -
TimedAbstractNon-Interference. In : Proc. 3rd Int. Conf.
FORMATS '05, edited by B. Le Charlier, pp. 289-303. -
Springer, 2005, Uppsala, SE, 26-28 Sep. 2005, LNCS 3829.
É. Goubault, M. Martel & S. Putot. -
Asserting the precision of floating-point computations: a simple
abstract interpreter. In : Proc. 11th
ESOP '2002, edited by D. Le Métayer, pp. 209-212. -
Springer, 8-12 Apr. 2002, Grenoble, FR, LNCS 2305.
S. Graf & H. Saïdi. -
VerifyingInvariantsUsingTheoremProving.
In : Proc. 8th Int. Conf.
CAV '97, edited by R. Alur & T. Henzinger. New
Brunswick, NJ, US, LNCS 1102, pp. 196-207. -
Springer, Jul. 31 - Aug. 3 1996.
N. Halbwachs. -
DelayAnalysisinSynchronousPrograms.
In : Proc. 5th Int. Conf.
CAV '93, edited by C. Courcoubatis. Elounda, GR, LNCS 697,
pp. 333-346. -
Springer, 28 June -1 Jul. 1993.
B. Jeannet, N. Halbwachs & P. Raymond. -
DynamicPartitioninginAnalysesofNumericalProperties.
In : Proc. 6th Int. Symp.
SAS '99, edited by A. Cortesi & G. Filé, pp. 18-38.
-
Springer, 1999, Venice, IT, 22-24 Sep. 1999, LNCS
1694.
N. Jones & F. Nielson. -
Abstractinterpretation:asemantics-basedtoolforprogramanalysis.
In : Semantic Modelling, edited by S. Abramsky,
D. Gabbay & T. Maibaum, Chapter 5, pp. 527-636. -
Clarendon Press, 1995, Handbook of Logic in Computer Science,
Vol. 4.
H. Mannila & E. Ukkonen. -
FlowanalysisofPrologprograms.
In : Proc. 1987 Int. Symp. on Logic Programming.
San Francisco, CA, pp. 205-214. -
IEEE Comp. Soc. Press, 31 Aug. - 4Sep. 1987.
K. Marriott & H. Søndergaard. -
Bottom-UpAbstractInterpretationofLogicPrograms.
In : Proc. 5th Int. Conf. & Symp.
on Logic Programming, Volume 1, edited by R. Kowalski,name
K. Bowen. Seattle, WA, US, pp. 733-748. -
MIT Press, 15-19 Aug. 1988.
L. Mauborgne. -
TreeSchemataandFairTermination.
In : Proc. 7th Int. Symp.
SAS '2000, edited by J. Palsberg, pp. 302-321. -
Springer, 29 June - 1 Jul. 2000, Santa Barbara, CA, US, LNCS
1824.
C. Mellish. -
AbstractInterpretationofPrologPrograms.
In : 3rd ICLP '86, edited by
E. Shapiro, pp. 463-474. -
Springer, 14-18 Jul. 1986, London, GB, LNCS 225.
J. Midtgaard & T. Jensen. -
A calculational approach to control-flow analysis by abstract
interrpetation. In : Proc. 15th Int.
Symp. SAS '08, edited by M. Alpuente & G. Vidal, pp.
347-362. -
Springer, 2008, Valencia, ES, 16-18 Jul. 2008, LNCS 5079.
D. Monniaux. -
Abstractinterpretationofprobabilisticsemantics.
In : Proc. 7th Int. Symp.
SAS '2000, edited by J. Palsberg, pp. 322-339. -
Springer, 29 June - 1 Jul. 2000, Santa Barbara, CA, US, LNCS
1824.
A. Mycroft & N. Jones. -
ARelationalFrameworkforAbstractInterpretation.
In : Programs as Data Objects, Proceedings of a Workshop,
edited by N. Jones & H. Ganzinger, pp. 156-171. -
Springer, 1986, Copenhagen, DK, 17-19 Oct. 1985, LNCS 215.
Y. G. Park & B. Goldberg. -
Escapeanalysisonlists. In :
Proc. ACM SIGPLAN '92 Conf. PLDI. ACM SIGPLAN Not. 31(5),
San Francisco, CA, US, 21-24, May 1992. pp. 116-127. -
ACM Press.
M. D. Preda, M. Christodorescu, S. Jha & S. Debray. -
Semantics-BasedApproachtoMalwareDetection. In : 34th POPL, Nice, France, 17-19
Jan. 2007. pp. 238-252. -
ACM Press.
F. Ranzato. -
OntheCompletenessofModelChecking.
In : Proc. 10th ESOP '2001,
edited by D. Sands. Genova, IT, 2-6 Apr. 2001, LNCS 2028, pp.
137-154. -
Springer, 2001.
M. Sagiv, T. Reps & R. Wilhelm. -
ShapeAnalysis.
In : Proc. Int. Conf. CC '2000, LNCS 1781,
edited by D. A. Watt, Berlin, DE, 25 Mar. - 2 Apr. 2000. pp.
1-17. -
Springer.
PDF version.
This document is hopefully sound, may be too abstract and necessarily
incomplete. Amendments are welcomed at
Patrick.Cousot@ens.fr.
Footnotes:
1MOP
often stands for "Meet Over all Path" where the abstract meet
corresponds to a concrete join, the order in dataflow analysis often
being the inverse of the one used in abstract interpretation, whence
corresponds to a concrete inverse logical implication, which may
sometimes be counter-intuitive.