Memory Analysis

Definitions

1. memory unit: mu = (dyscopeID, variableID, reference, access) A memory unit mu is referring to a certain region of a variable, which is defined by a dyscopeID and a variable ID. A mu has an access attribute which denotes whether the it is writable by a given process.

2. impact memory unit: a memory unit being accessed at the current location by a given process.

3. reachable impact memory unit: a memory unit being accessed at the current location or any reachable future location of a given process.

4. variable addressed-of: a variable that's used as the operand of the address-of operator &.

Impact memory unit analysis

The analysis below is an over approximation.

Given a location L, which has outgoing statements s1, s2, ... sn, the impact memory units of L is:
impact(L) = impact(s1) U impact(s2) U ... U impact(sn).

Reachable memory units analysis:

reach(L) = U L --> L' reach(L') U impact(L).

Expressions

let e be an expression, let le be an left-hand-side expression, let impact(e) be the set of impact memory units of e. letmu(e) be a function to convert an expression, of pointer type or being a left-hand-side expression, to a memory unit.

1. abstract function call: f(e0,e1, ...)

impact(f(e0,e1, ...)) = impact(e0) U impact(e1) ...

2. address-of: &le

impact($le)=impact(sub(le))

3. array literal: {e0, e1, ...}

impact({e0, e1, ...}) = impact(e0) U impact(e1) ...

4. binary expression: e0 op e1

impact(e0 op e1) = impact(e0) U impact(e1)

5. bound variable expression: eb

impact(eb)=\empty

6. cast expression: (T)e

impact((T)e)=impact(e)

7. char literal: {e0, e1, ...}

similar to array literal

8. conditional expression: e0 ? e1 : e2

impact(e0 ? e1 : e2) = impact(e0) U impact(e1) U impact(e2)

9. dereference expression: *e

impact(*e) = mu(e) U impact(sub(e)) the impact memory units of *e include the memory unit refers to by e, and the impact memory units of the sub-expressions of e. e.g., the impact memory units of *(p+i) is {mu(p+5), impact(i)}, because p is of pointer type and sub(p+i) is {i}.

10. derivative call expression: de

impact(de) = \empty

11. domain guard expression: (int i0, i1, ... : e)

impact((int i0, i1, ... : e)) = impact(e)

12. dot expression: e.k

impact(e.k) = mu(e.k) U impact(sub(e))

the impact memory units of e.k include the memory unit refers to by e, and the impact memory units of the sub-expressions of e. e.g., the impact memory units of points[k].x is {mu(points[k]+x), impact(k)}, because sub(points[k]) is {k}.

13. quantified expression: quantifier er: e where er is the restriction expression

impact(quantifier er: e) = impact(er) U impact(e)

14. rectangular domain expression: {e0, e1, ...}

similar to array literal

15. regular range expression: {el, eh#es}

impact({el, eh#es}) = impact(el) U impact(eh) U impact(es)

16. scope-of expression: scopeof(e)

impact(scopeof(e))=\empty

17. sizeof expression: sizeof(e)

impact(sizeof(e))=\empty

18. struct or union literal: {e0, e1, ...}

similar to array literal

19. subscript expression: ea[ei]

impact(ea[ei])=mu(ea[ei]) U impact(sub(ea)) U impact(ei)

for example, the impact units of (a[i])[j] is mu(a[i][j]) U impact(i) U impact(j) because sub(a[i]) is {i}.

Sub-expressions

let e be an expression, let sub(e) be the set of sub-expressions of e.

1. abstract function call: f(e0,e1, ...)

sub(f(e0,e1, ...)) = {e0, e1, ...}

2. address-of: &le

sub(&le)={le} U sub(le)

3. array literal: {e0, e1, ...}

sub({e0, e1, ...}) = {e0, e1, ...}`

4. binary expression: e0 op e1 sub(e0 op e1) = e0.type== pointer ? {e1} : {e0, e1}

5. bound variable expression: eb

sub(eb)=\empty

6. cast expression: (T)e

sub((T)e)={e}

statements

1. assignment: l := e impact(l := e) = impact(l) U impact(e);

2. call: l := f(e0, e1, e2, ...)
   • f is atomic specified ($atomic_f) and f has contracts:
     TBC
   • otherwise:
     impact(l := f(e0, e1, e2, ...)) = impact(l) U impact(e0) U impact(e1) ... U impact(f), where impact(f) is the impact memory unit set of the function f.

3. guarded statement: [e]s

impact([e]s) = impact(e) U impact(s)