Changes between Version 3 and Version 4 of MemoryAnalysis

Timestamp:

07/29/15 11:26:33 (11 years ago)

Author:

zmanchun

Comment:

--

MemoryAnalysis

@@ -15 +15 @@
 ==== 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`.
+let`mu(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: `e = f(e0,e1, ...)`
+1. abstract function call: `f(e0,e1, ...)`
     `impact(f(e0,e1, ...)) = impact(e0) U impact(e1) ...`
-2. address-of: `e=&le`
+2. address-of: `&le`
     `impact($le)=impact(sub(le))`
-3. 
+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: `e = f(e0,e1, ...)`
+1. abstract function call: `f(e0,e1, ...)`
     `sub(f(e0,e1, ...)) = {e0, e1, ...}`
-2. address-of: `e=&le`
-    `sub(&le)=sub(le)`
-3. 
-   
+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}`
+
+
+
+
+
+
+