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.

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.

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

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

2. address-of: e=&le

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

Sub-expressions

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

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

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

2. address-of: e=&le

sub(&le)=sub(le)