Editing Abstract interpretation

{{Short description|Approach to static program analysis}}
In [[computer science]], '''abstract interpretation''' is a theory of [[soundness|sound approximation]] of the [[semantics of programming languages|semantics of computer programs]], based on [[Monotonic function#Monotonicity in order theory|monotonic function]]s over [[ordered set]]s, especially [[lattice (order)|lattice]]s. It can be viewed as a partial [[Execution (computers)|execution]] of a [[computer program]] which gains information about its semantics (e.g., [[control-flow analysis|control-flow]], [[data-flow analysis|data-flow]]) without performing all the [[calculation]]s.

Its main concrete application is formal [[static code analysis|static analysis]], the automatic [[information extraction|extraction of information]] about the possible executions of computer programs; such analyses have two main usages:
* inside [[compiler]]s, to analyse programs to decide whether certain [[Optimization (computer science)|optimization]]s or [[Program transformation|transformation]]s are applicable;
* for [[debugging]] or even the certification of programs against classes of bugs.

Abstract interpretation was formalized by the French computer scientist working couple [[Patrick Cousot]] and [[Radhia Cousot]] in the late 1970s.<ref>{{cite book |first1=Patrick |last1=Cousot |first2=Radhia |last2=Cousot |chapter-url=https://www.di.ens.fr/~cousot/publications.www/CousotCousot-POPL-77-ACM-p238--252-1977.pdf |chapter=Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints |title=Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977 |publisher=ACM Press |year=1977 |pages=238–252 |doi=10.1145/512950.512973 |s2cid=207614632 }}</ref><ref name="CCPOPL79">{{cite book |first1=Patrick |last1=Cousot |first2=Radhia |last2=Cousot |chapter-url=https://www.di.ens.fr/~cousot/publications.www/CousotCousot-POPL-79-ACM-p269--282-1979.pdf |chapter=Systematic Design of Program Analysis Frameworks  |title=Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, January 1979 |publisher=ACM Press |year=1979 |pages=269–282 |doi=10.1145/567752.567778|s2cid=1547466 }}</ref>

==Intuition==
This section illustrates abstract interpretation by means of real-world, non-computing examples.

Consider the people in a conference room.  Assume a unique identifier for each person in the room, like a [[social security number]] in the United States.  To prove that someone is not present, all one needs to do is see if their social security number is not on the list. Since two different people cannot have the same number, it is possible to prove or disprove the presence of a participant simply by looking up their number.

However it is possible that only the names of attendees were registered. If the name of a person is not found in the list, we may safely conclude that that person was not present; but if it is, we cannot conclude definitely without further inquiries, due to the possibility of [[homonym]]s (for example, two people named John Smith).  Note that this imprecise information will still be adequate for most purposes, because homonyms are rare in practice. However, in all rigor, we cannot say for sure that somebody was present in the room; all we can say is that they were ''possibly'' here. If the person we are looking up is a criminal, we will issue an ''alarm''; but there is of course the possibility of issuing a ''false alarm''. Similar phenomena will occur in the analysis of programs.

If we are only interested in some specific information, say, "was there a person of age <math>n</math> in the room?", keeping a list of all names and dates of births is unnecessary. We may safely and without loss of precision restrict ourselves to keeping a list of the participants' ages. If this is already too much to handle, we might keep only the age of the youngest, <math>m</math> and oldest person, <math>M</math>. If the question is about an age strictly lower than <math>m</math> or strictly higher than <math>M</math>, then we may safely respond that no such participant was present. Otherwise, we may only be able to say that we do not know.

In the case of computing, concrete, precise information is in general not computable within finite time and memory (see [[Rice's theorem]] and the [[halting problem]]). [[Abstraction]] is used to allow for generalized answers to questions (for example, answering "maybe" to a yes/no question, meaning "yes or no", when we (an algorithm of abstract interpretation) cannot compute the precise answer with certainty); this simplifies the problems, making them amenable to automatic solutions. One crucial requirement is to add enough vagueness so as to make problems manageable while still retaining enough precision for answering the important questions (such as "might the program crash?").

== Abstract interpretation of computer programs ==

Given a programming or specification language, abstract interpretation consists of giving several semantics linked by relations of abstraction. A semantics is a mathematical characterization of a possible behavior of the program. The most precise semantics, describing very closely the actual execution of the program, are called the ''concrete semantics''. For instance, the concrete semantics of an [[imperative programming]] language may associate to each program the set of execution traces it may produce &ndash; an execution trace being a sequence of possible consecutive states of the execution of the program; a state typically consists of the value of the program counter and the memory locations (globals, stack and heap). More abstract semantics are then derived; for instance, one may consider only the set of reachable states in the executions (which amounts to considering the last states in finite traces).

The goal of static analysis is to derive a computable semantic interpretation  at some point. For instance, one may choose to represent the state of a program manipulating integer variables by forgetting the actual values of the variables and only keeping their signs (+, − or 0). For some elementary operations, such as [[multiplication]], such an abstraction does not lose any precision: to get the sign of a product, it is sufficient to know the sign of the operands. For some other operations, the abstraction may lose precision: for instance, it is impossible to know the sign of a sum whose operands are respectively positive and negative.

Sometimes a loss of precision is necessary to make the semantics decidable (see [[Rice's theorem]] and the [[halting problem]]). In general, there is a compromise to be made between the precision of the analysis and its decidability ([[computability theory (computation)|computability]]), or tractability ([[computational complexity|computational cost]]).

In practice the abstractions that are defined are tailored to both the program properties one desires to analyze, and to the set of target programs. The first large scale automated analysis of computer programs with abstract interpretation was motivated by the accident that resulted in the destruction of the [[Ariane 5 Flight 501|first flight of the Ariane 5]] rocket in 1996.<ref>{{cite web|title=PolySpace Technologies History | last=Faure | first=Christèle | url=http://christele.faure.pagesperso-orange.fr/polyspace.html | access-date=3 October 2010}}</ref>

== Formalization ==

[[File:Abstract interpretation of integers by signs svg.svg|thumb|Example: abstraction of integer sets (red) to sign sets (green)]]
Let <math>L</math> be an [[ordered set]], called ''concrete set'', and let <math>L'</math> be another ordered set, called ''abstract set''. These two sets are related to each other by defining [[total function]]s that map elements from one to the other.

A  function <math>\alpha</math> is called an ''abstraction function'' if it maps an element <math>x</math> in the concrete set <math>L</math> to an element <math>\alpha(x)</math> in the abstract set <math>L'</math>. That is, element  <math>\alpha(x)</math> in <math>L'</math> is the ''abstraction'' of <math>x</math> in <math>L</math>.

A function <math>\gamma</math> is called a ''concretization function'' if it maps an element <math>x'</math> in the abstract set <math>L'</math> to an element <math>\gamma(x')</math> in the concrete set <math>L</math>. That is, element <math>\gamma(x')</math> in <math>L</math> is a ''concretization'' of <math>x'</math> in <math>L'</math>.

Let <math>L_1</math>, <math>L_2</math>, <math>L'_{1}</math>, and <math>L'_2</math> be ordered sets. The concrete semantics <math>f</math> is a monotonic function from <math>L_1</math> to <math>L_2</math>. A function <math>f'</math> from <math>L'_{1}</math> to <math>L'_2</math> is said to be a ''valid abstraction'' of <math>f</math> if, for all <math>x'</math> in <math>L'_{1}</math>, we have <math>(f \circ \gamma)(x') \leq (\gamma \circ f')(x')</math>.

Program semantics are generally described using [[fixed point (mathematics)|fixed point]]s in the presence of loops or recursive procedures. Suppose that <math>L</math> is a [[complete lattice]] and let <math>f</math> be a [[monotonic function]] from <math>L</math> into <math>L</math>. Then, any <math>x'</math> such that <math>f(x') \leq x'</math> is an abstraction of the least fixed-point of <math>f</math>, which exists, according to the [[Knaster&ndash;Tarski theorem]].

The difficulty is now to obtain such an <math>x'</math>. If <math>L'</math> is of finite height, or at least verifies the [[ascending chain condition]] (all ascending sequences are ultimately stationary), then such an <math>x'</math> may be obtained as the stationary limit of the [[monotonic sequence|ascending sequence]] <math>x'_{n}</math> defined by induction as follows: <math>x'_{0} = \bot</math> (the least element of <math>L'</math>) and <math>x'_{n+1} = f'(x'_{n})</math>.

In other cases, it is still possible to obtain such an <math>x'</math> through a (pair-)[[Widening (computer science)|widening operator]],<ref>{{cite book |first1=P. |last1=Cousot |first2=R. |last2=Cousot| chapter=Comparing the Galois Connection and Widening / Narrowing Approaches to Abstract Interpretation |chapter-url=http://www.dsi.unive.it/%7Ecortesi/paperi/sefm08.pdf |editor-first=Maurice |editor-last=Bruynooghe |editor-first2=Martin |editor-last2=Wirsing |title=Proc. 4th Int. Symp. on Programming Language Implementation and Logic Programming (PLILP)|date=August 1992 |pages=269–296| publisher=Springer |isbn=978-0-387-55844-8 |volume=631 |series=Lecture Notes in Computer Science}}</ref> defined as a binary operator <math>\nabla\colon L\times L\to L</math> which satisfies the following conditions:

# For all <math>x</math> and <math>y</math>, we have <math>x \leq x \mathbin{\nabla} y</math> and <math>y \leq x \mathbin{\nabla} y</math>, and
# For any ascending sequence <math>(y'_{n})_{n\geq 0}</math>, the sequence defined by <math>x'_{0} := \bot</math> and <math>x'_{n+1} := x'_{n} \mathbin{\nabla} y'_{n}</math> is ultimately stationary. We can then take <math>y'_{n}=f'(x'_{n})</math>.

In some cases, it is possible to define abstractions using [[Galois connection]]s <math>(\alpha, \gamma)</math> where <math>\alpha</math> is from <math>L</math> to <math>L'</math> and <math>\gamma</math> is from <math>L'</math> to <math>L</math>. This supposes the existence of best abstractions, which is not necessarily the case. For instance, if we abstract sets of couples <math>(x, y)</math> of [[real number]]s by enclosing convex [[polyhedron|polyhedra]], there is no optimal abstraction to the disc defined by <math>x^2 + y^2 \leq 1</math>.

==Examples of abstract domains==

===Numerical abstract domains===

One can assign to each variable <math>x</math> available at a given program point an interval <math>[L_{x}, H_{x}]</math>. A state assigning the value <math>v(x)</math> to variable <math>x</math> will be a concretization of these intervals if, for all <math>x</math>, we have <math>v(x) \in [L_{x}, H_{x}]</math>. From the intervals <math>[L_{x}, H_{x}]</math> and <math>[L_{y}, H_{y}]</math> for variables <math>x</math> and <math>y</math>, respectively, one can easily obtain intervals for <math>x + y</math> (namely, <math>[L_{x}+L_{y}, H_{x}+H_{y}]</math>) and for <math>x - y</math> (namely, <math>[L_{x} - H_{y}, H_{x} - L_{y}]</math>); note that these are ''exact'' abstractions, since the set of possible outcomes for, say, <math>x+y</math>, is precisely the interval <math>[L_{x}+L_{y}, H_{x}+H_{y}]</math>. More complex formulas can be derived for multiplication, division, etc., yielding so-called [[interval arithmetic]]s.<ref>{{cite book |first1=Patrick |last1=Cousot  |first2=Radhia |last2=Cousot | contribution=Static determination of dynamic properties of programs | title=Proceedings of the Second International Symposium on Programming | publisher=Dunod, Paris, France | pages=106–130 | year=1976 |contribution-url=https://www.di.ens.fr/~cousot/COUSOTpapers/publications.www/CousotCousot-ISOP-76-Dunod-p106--130-1976.pdf}}</ref>

Let us now consider the following very simple program:
<pre>
y = x;
z = x - y;
</pre>
{| style="float:right"
| [[File:Combination of abstract domains.svg|thumb|Combination of [[interval arithmetic]] ({{color|#00ff00|green}}) and congruence mod 2 on integers ({{color|#00ffff|cyan}}) as abstract domains to analyze a simple piece of [[C (programming language)|C]] code ({{color|#ff8080|red}}: concrete sets of possible values at runtime). Using the congruence information ({{color|#00ffff|0}}=even, {{color|#00ffff|1}}=odd), a [[Zero division#In computer arithmetic|zero division]] can be excluded. (Since only one variable is involved, relational vs. non-relational domains is not an issue here.)]]
|}
{| style="float:right"
| [[File:3dpoly.svg|thumb|A 3-dimensional convex example polyhedron describing the possible values of 3 variables at some program point. Each of the variables may be zero, but all three can't be zero simultaneously. The latter property cannot be described in the interval arithmetics domain.]]
|}
With reasonable arithmetic types, the result for {{samp|z}} should be zero. But if we do interval arithmetic starting from {{samp|x}} in [0, 1], one gets {{samp|z}} in [−1, +1]. While each of the operations taken individually was exactly abstracted, their composition isn't.

The problem is evident: we did not keep track of the equality relationship between {{samp|x}} and {{samp|y}}; actually, this domain of intervals does not take into account any relationships between variables, and is thus a ''non-relational domain''. Non-relational domains tend to be fast and simple to implement, but imprecise.

Some examples of ''relational'' numerical abstract domains are:
* [[congruence relation#Basic example|congruence relations]] on integers<ref>{{cite journal |first=Philippe |last=Granger | title=Static Analysis of Arithmetical Congruences | journal=International Journal of Computer Mathematics | volume=30 |issue=3–4 | pages=165–190 | year=1989 | doi=10.1080/00207168908803778}}</ref><ref>{{cite book | author=Philippe Granger | contribution=Static Analysis of Linear Congruence Equalities Among Variables of a Program |editor-first=S. |editor-last=Abramsky |editor2-first=T.S.E. |editor2-last=Maibaum | title=Proc. Int. J. Conf. on Theory and Practice of Software Development (TAPSOFT) | publisher=Springer | series=Lecture Notes in Computer Science | volume=493 | pages=169–192 | year=1991 }}</ref>
* convex [[polyhedra]]<ref>{{cite book |first1=Patrick |last1=Cousot |first2=Nicolas |last2=Halbwachs | contribution=Automatic Discovery of Linear Restraints Among Variables of a Program | title=Conf. Rec. 5th ACM Symp. on Principles of Programming Languages (POPL) | pages=84–97 | contribution-url=https://www.di.ens.fr/~cousot/publications.www/CousotHalbwachs-POPL-78-ACM-p84--97-1978.pdf | date=January 1978 }}</ref> (cf. left picture) – with some high computational costs
* difference-bound matrices<ref>{{cite book |first=Antoine |last=Miné | chapter=A New Numerical Abstract Domain Based on Difference-Bound Matrices
| title=Programs as Data Objects, Second Symposium, (PADO)|date=2001 | volume=2053| pages=155–172| publisher=Springer |editor-first=Olivier |editor-last=Danvy |editor2-first=Andrzej |editor2-last=Filinski |series=Lecture Notes in Computer Science | arxiv=cs/0703073}}</ref>
* "octagons"<ref>{{cite thesis | type=Ph.D. thesis |first=Antoine |last=Miné | title=Weakly Relational Numerical Abstract Domains | institution=Laboratoire d'Informatique de l'École Normale Supérieure | url=https://www.di.ens.fr/~mine/these/these-color.pdf | date=Dec 2004 }}</ref><ref>{{cite journal | author=Antoine Miné | title=The Octagon Abstract Domain | journal=Higher Order Symbol. Comput. | volume=19 | number=1 | pages=31–100 | year=2006 | doi=10.1007/s10990-006-8609-1| arxiv=cs/0703084 }}</ref><ref>{{cite journal |first1=Robert |last1=Clarisó |first2=Jordi |last2=Cortadella |author2-link=Jordi Cortadella| title=The Octahedron Abstract Domain | journal=Science of Computer Programming | volume=64 | pages=115–139 | year=2007 | doi=10.1016/j.scico.2006.03.009| hdl=10609/109823 | hdl-access=free }}</ref>
* linear equalities<ref>{{cite journal | author=Michael Karr | title=Affine Relationships Among Variables of a Program | journal=Acta Informatica | volume=6 | issue=2 | pages=133–151 | year=1976 | doi=10.1007/BF00268497| s2cid=376574 }}</ref>
and combinations thereof (such as the reduced product,<ref name="CCPOPL79"/> cf. right picture).

When one chooses an abstract domain, one typically has to strike a balance between keeping fine-grained relationships, and high computational costs.

===Machine word abstract domains===

While high-level languages such as [[Python (programming language)|Python]] or [[Haskell (programming language)|Haskell]] use unbounded integers by default, lower-level programming languages such as [[C (programming language)|C]] or [[assembly language]] typically operate on finitely-sized [[Word (computer architecture)|machine words]], which are more suitably modeled using the [[Integers modulo n|integers modulo <math display=inline>2^n</math>]] (where ''n'' is the bit width of a machine word). There are several abstract domains suitable for various analyses of such variables.

The ''bitfield domain'' treats each bit in a machine word separately, i.e., a word of width ''n'' is treated as an array of ''n'' abstract values. The abstract values are taken from the set <math display=inline>\{0,1,\bot\}</math>, and the abstraction and concretization functions are given by:<ref>{{Cite journal |last=Miné |first=Antoine |date=Jun 2012 |title=Abstract domains for bit-level machine integer and floating-point operations |url=https://hal.archives-ouvertes.fr/hal-00748094 |journal=WING'12 - 4th International Workshop on Invariant Generation |location=Manchester, United Kingdom |pages=16}}</ref><ref>{{Cite book |last1=Regehr |first1=John |last2=Duongsaa |first2=Usit |title=Proceedings of the 2006 ACM SIGPLAN/SIGBED conference on Language, compilers, and tool support for embedded systems |chapter=Deriving abstract transfer functions for analyzing embedded software |date=Jun 2006 |chapter-url=https://doi.org/10.1145/1134650.1134657 |series=LCTES '06 |location=New York, NY, USA |publisher=Association for Computing Machinery |pages=34–43 |doi=10.1145/1134650.1134657 |isbn=978-1-59593-362-1|s2cid=13221224 }}</ref> <math>\gamma(0) = \{0\}</math>, <math>\gamma(1) = \{1\}</math>, <math>\gamma(\bot) = \{0,1\}</math>, <math>\alpha(\{0\}) = 0</math>, <math>\alpha(\{1\}) = 1</math>, <math>\alpha(\{0, 1\}) = \bot</math>, <math>\alpha(\{\}) = \bot</math>. Bitwise operations on these abstract values are identical with the corresponding logical operations in some [[Three-valued logic|three-valued logics]]:<ref>{{Cite book |last1=Reps |first1=T. |last2=Loginov |first2=A. |last3=Sagiv |first3=M. |title=Proceedings 17th Annual IEEE Symposium on Logic in Computer Science |chapter=Semantic minimization of 3-valued propositional formulae |date=Jul 2002 |chapter-url=https://ieeexplore.ieee.org/document/1029816 |pages=40–51 |doi=10.1109/LICS.2002.1029816|isbn=0-7695-1483-9 |s2cid=8451238 }}</ref>

{| style="border-spacing: 10px 0;" align="center"
| colspan="3" style="text-align:center;" |
|- valign="bottom"
|
{| class="wikitable" style="text-align:center;"
|+ NOT(A)
! width="25" | A
! width="25" | ¬A
|-
! scope="row" {{no|0}}
| {{yes|1}}
|-
! scope="row" | ⊥
| ⊥
|-
! scope="row" {{yes|1}}
| {{no|0}}
|}
|
{| class="wikitable" style="text-align:center;"
|+ AND(A, B)
! rowspan="2" colspan="2" | A ∧ B
! colspan="3" | B
|-
! width="25" {{no|0}}
! width="25" | ⊥
! width="25" {{yes|1}}
|-
! scope="row" rowspan="3" width="25" | A
! scope="row" width="25" {{no|0}}
| {{no|0}}
| {{no|0}}
| {{no|0}}
|-
! scope="row" | ⊥
| {{no|0}}
| ⊥
| ⊥
|-
! scope="row" {{yes|1}}
| {{no|0}}
| ⊥
| {{yes|1}}
|}
|
{| class="wikitable" style="text-align:center;"
|+ OR(A, B)
! rowspan="2" colspan="2" | A ∨ B
! colspan="3" | B
|-
! width="25" {{no|0}}
! width="25" | ⊥
! width="25" {{yes|1}}
|-
! scope="row" rowspan="3" width="25" | A
! scope="row" width="25" {{no|0}}
| {{no|0}}
| ⊥
| {{yes|1}}
|-
! scope="row" | ⊥
| ⊥
| ⊥
| {{yes|1}}
|-
! scope="row" {{yes|1}}
| {{yes|1}}
| {{yes|1}}
| {{yes|1}}
|}
|}

Further domains include the ''signed interval domain'' and the ''unsigned interval domain''. All three of these domains support forwards and backwards abstract operators for common operations such as addition, [[Bitwise operation#Bit shifts|shifts]], xor, and multiplication. These domains can be combined using the reduced product.<ref>{{Cite journal |last1=Yoon |first1=Yongho |last2=Lee |first2=Woosuk |last3=Yi |first3=Kwangkeun |date=2023-06-06 |title=Inductive Program Synthesis via Iterative Forward-Backward Abstract Interpretation |journal=Proceedings of the ACM on Programming Languages |volume=7 |issue=PLDI |pages=174:1657–174:1681 |doi=10.1145/3591288|doi-access=free |arxiv=2304.10768 }}</ref>

==See also==
* [[Model checking]]
* [[Symbolic simulation]]
* [[Symbolic execution]]
* [[List of tools for static code analysis]] &mdash; contains both abstract-interpretation based (sound) and ad hoc (unsound) tools
* [[Static program analysis]] &mdash; overview of analysis methods, including, but not restricted to, abstract interpretation
* [[Interpreter (computing)]]

==References==
{{Reflist|40em}}

==External links==
* [https://www.di.ens.fr/~cousot/AI/ A web-page on Abstract Interpretation maintained by Patrick Cousot]
* [http://www.cs.unipr.it/~bagnara/Papers/PDF/Q485.pdf Roberto Bagnara's paper showing how it is possible to implement an abstract-interpretation based static analyzer for a C-like programming language]
* [http://staticanalysis.org The Static Analysis Symposia], [https://dblp1.uni-trier.de/db/conf/sas/ proceedings] appearing in the Springer [[LNCS]] series
* Conference on Verification, Model-Checking, and Abstract Interpretation (VMCAI), affiliated at the [[Symposium on Principles of Programming Languages#Affiliated events|POPL conference]], [https://dblp.uni-trier.de/db/conf/vmcai/ proceedings] appearing in the Springer [[LNCS]] series
; Lecture notes
* [http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www/ Abstract Interpretation]. Patrick Cousot. MIT.
* [https://web.archive.org/web/20221123194810/https://people.cs.ksu.edu/~schmidt/papers/schmidt/Escuela03/home.html David Schmidt's lecture notes on abstract interpretation]
* [http://cs.au.dk/~amoeller/spa/ Møller and Schwarzbach's lecture notes on Static Program Analysis]
* [http://www.dsi.unive.it/~avp/ Agostino Cortesi's lecture notes on Program Analysis and Verification]
* [http://www.mpi-inf.mpg.de/vtsa08/slides/sutre2.pdf Slides by Grégoire Sutre going through every step of Abstract Interpretation with many examples - also introducing Galois connections]

{{Program analysis}}
[[Category:Abstract interpretation| ]]
[[Category:Program analysis|Abstract interpretation]]