@@ -230,7 +230,7 @@ digraph ast {
230
230
}
231
231
\enddot
232
232
233
- In the end, we produce a sequence of graphs modeling each declaration
233
+ In the end, we produce a sequence of trees modeling each declaration
234
234
in the translation unit (i.e., the file `factorial.c`).
235
235
236
236
This data structure is already useful: At this level, we can easily
@@ -371,9 +371,7 @@ here is the code:
371
371
}
372
372
return fac;
373
373
```
374
-
375
- This function
376
- consists of four basic blocks:
374
+ This function consists of four basic blocks:
377
375
1 . ` Declaration: unsigned long fac.1, value 1 ` <br />
378
376
` Declaration: unsigned i.1, value 1 `
379
377
2 . ` i.1 <= n.1 `
@@ -708,7 +706,18 @@ An abstract interpretation is made up from four ingredients:
708
706
in the previous step that describes the behavior of the program.
709
707
710
708
The first ingredient we need for abstract interpretation is the
711
- ** abstract domain** . An abstract domain is a set $D$ (or, if you
709
+ ** abstract domain** .
710
+ The domain allows us to express what we know about a given variable or
711
+ value at a given program location; in our example, whether it is zero or not.
712
+ The way we use the abstract domain is for each program point, we have a
713
+ map from visible variables to elements of the abstract domain,
714
+ describing what we know about the values of the variables at this point.
715
+
716
+ For instance, consider the ` factorial ` example again. After running the
717
+ first basic block, we know that ` fac ` and ` i ` both contain 1, so we have
718
+ a map that associates both ` fac ` and ` i ` to "not 0".
719
+
720
+ An abstract domain is a set $D$ (or, if you
712
721
prefer, a data type) with the following properties:
713
722
- There is a function merge that takes two elements of $D$ and returns
714
723
an element of $D$. This function is associative (merge(x, merge(y,z))
@@ -717,9 +726,11 @@ prefer, a data type) with the following properties:
717
726
- There is an element bottom of $D$ such that merge(x, bottom) = x.
718
727
719
728
Algebraically speaking, $D$ needs to be a semi-lattice.
729
+
720
730
For our example, we use the following domain:
721
731
- D contains the elements "bottom" (nothing is known),
722
732
"equals 0", "not 0" and "could be 0".
733
+
723
734
- merge is defined as follows:
724
735
merge(bottom, x) = x
725
736
merge("could be 0", x) = "could be 0"
@@ -728,16 +739,6 @@ For our example, we use the following domain:
728
739
- bottom is bottom, obviously.
729
740
It is easy but tedious to check that all conditions hold.
730
741
731
- The domain allows us to express what we know about a given variable or
732
- value at a given program location; in our example, whether it is zero or not.
733
- The way we use the abstract domain is for each program point, we have a
734
- map from visible variables to elements of the abstract domain,
735
- describing what we know about the values of the variables at this point.
736
-
737
- For instance, consider the ` factorial ` example again. After running the
738
- first basic block, we know that ` fac ` and ` i ` both contain 1, so we have
739
- a map that associates both ` fac ` and ` i ` to "not 0".
740
-
741
742
The second ingredient we need are the ** abstract state transformers** .
742
743
An abstract state transformer describes how a specific expression or
743
744
statement processes abstract values. For the example, we need to define
0 commit comments