Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision | ||
sav08:introduction_to_pointer_analysis [2008/05/21 10:40] vkuncak created |
sav08:introduction_to_pointer_analysis [2008/05/21 10:42] (current) vkuncak |
||
---|---|---|---|
Line 26: | Line 26: | ||
**Examples** | **Examples** | ||
- | <code c> | + | <code> |
#include <stdio.h> | #include <stdio.h> | ||
int main() | int main() | ||
Line 48: | Line 48: | ||
* Can compiler prove one branch is dead? | * Can compiler prove one branch is dead? | ||
* Can it do common subexpression elimination? | * Can it do common subexpression elimination? | ||
- | <code c> | + | <code> |
x = sin(z); | x = sin(z); | ||
*p = 4.0; | *p = 4.0; | ||
Line 58: | Line 58: | ||
Is | Is | ||
- | <code c> | + | <code> |
int* p1, p2; | int* p1, p2; | ||
...S... | ...S... | ||
Line 65: | Line 65: | ||
</code> | </code> | ||
equivalent to | equivalent to | ||
- | <code c> | + | |
+ | <code> | ||
int* p1, p2; | int* p1, p2; | ||
...S... | ...S... | ||
Line 73: | Line 74: | ||
There are also corresponding examples in Java, ocaml. | There are also corresponding examples in Java, ocaml. | ||
- | <code java> | + | |
+ | <code> | ||
x.f = 3; | x.f = 3; | ||
p.f = 4; | p.f = 4; | ||
Line 82: | Line 84: | ||
} | } | ||
</code> | </code> | ||
- | <code ocaml> | + | |
+ | <code> | ||
let x = ref 3 in | let x = ref 3 in | ||
let p = x in | let p = x in | ||
Line 91: | Line 94: | ||
How we can describe this semantically? (Recall verification condition generation in the presence of structures): we can view functions as arrays: | How we can describe this semantically? (Recall verification condition generation in the presence of structures): we can view functions as arrays: | ||
- | <code java> | + | |
+ | <code> | ||
f[x] = 3; | f[x] = 3; | ||
f[p] = 4; | f[p] = 4; | ||
Line 114: | Line 118: | ||
* **pointer analysis:** represent (usually disjoint) sets of locations to which each variable points to. For example, if we can determine that a pointer p points to an abstract location 1, and q points to location 2. If location 1 and location 2 are disjoint, then we can be sure that p and q do not overlap. | * **pointer analysis:** represent (usually disjoint) sets of locations to which each variable points to. For example, if we can determine that a pointer p points to an abstract location 1, and q points to location 2. If location 1 and location 2 are disjoint, then we can be sure that p and q do not overlap. | ||
- | * **alias analysis:** can two symbolic expressions be an 'alias' for the same physical location i.e. can they point to the same location. | + | * **alias analysis:** can two symbolic expressions be an 'alias' for the same physical location i.e. can they point to the same location. |