Editing Abstract interpretation (section)

===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 |last=Yoon |first=Yongho |last2=Lee |first2=Woosuk |last3=Yi |first3=Kwangkeun |date=2023-06-06 |title=Inductive Program Synthesis via Iterative Forward-Backward Abstract Interpretation |url=https://dl.acm.org/doi/10.1145/3591288 |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>