Changes between Version 115 and Version 116 of IR

Timestamp:

12/02/15 14:06:09 (10 years ago)

Author:

zmanchun

Comment:

--

IR

@@ -454 +454 @@
 * depends clause: `depends [condition] action0, action1, action2, ... `
  * Example: `depends ma_union(ma_comp(reads n, calls inc, <x>)), calls(dec, y))`
-
- * **absence of depends clause**:
-* assigns-or-reads clause
- * assigns clause: `assigns [condition] {memory-list}`
- * reads clause: `reads [condition] {memory-list}`
- * `reads {nothing}` implies `assigns {nothing}`
- * `reads {\nothing}` is equivalent to: `reads {\nothing} assigns {\nothing}`
- * `assigns {X}` where `X != \nothing`, implies `reads {X}`
- * `assigns {X}` is equivalent to:` assigns{X} reads{X}`
+ * absence of depends clause: there is no information about the dependency of the function, which means that the analysis needs to figure it out by itself.
+* some facts about assigns-or-reads clause
+ * `reads nothing` implies `assigns nothing`
+ * `reads nothing` is equivalent to: `ma_union(reads nothing, assigns nothing)`
+ * `assigns X` where `X != nothing`, implies `reads X`
+ * `assigns X` is equivalent to: `ma_union(assigns X, reads X)`
  * absence:
   * absence of `reads` clause: there is no assumption about the read access of the function, i.e., the function could read anything
   * absence of `assigns` clause: similar to the absence of `reads` clause
- * `reads/assigns {\nothing}` doesn’t necessarily means that the function never reads or assigns any variable. The function could still reads/assigns its “local” variables, including function parameters and any variable declared inside the function body.
-
-* For an independent function which has `depends {\nothing}`, usually we also need to specify `reads{nothing}`, for the purpose of reachability analysis.
+ * `reads/assigns nothing` doesn’t necessarily means that the function never reads or assigns any variable. The function could still reads/assigns its “local” variables, including function parameters and any variable declared inside the function body.
+
+* For an independent function which has `depends nothing`, usually we also need to specify `reads nothing`, for the purpose of reachability analysis.
 e.g., 
 {{{
 /* Returns the size of the given bundle b. */
-bundle_size(Bundle b; Int)
-  depends {\nothing}
-  reads {\nothing}
+bundle_size(Bundle b): Integer
+  depends nothing
+  reads b
   ;
 }}}
@@ -480 +477 @@
 * Example of a function declaration with contracts: 
 {{{
-atomic_f sendRecv(Int cmd, Pointer buf; Int)
-  depends [eq(cmd, SEND)] {write(buf)}
-  depends [eq(cmd, RECV)] {access(deref(buf))}
-  assigns [eq(cmd, SEND)] {\nothing}
-  assigns [eq(cmd, RECV)] {deref(buf)}
-  reads {deref(buf)}
+atomic_f sendRecv(Int cmd, Pointer buf): Integer
+  depends [eq(cmd, SEND)] writes(buf)
+  depends [eq(cmd, RECV)] access(deref(buf))
+  assigns [eq(cmd, SEND)] nothing
+  assigns [eq(cmd, RECV)] deref(buf)
+  reads deref(buf)
 {
-L0:
+  begin choose
   when (eq(cmd, SEND))
-     send(deref(buf), ...); goto L1;
+     do CALL send, <buf, ...>; goto L1;
   when (eq(cmd, RECV))
-    deref(buf):=recv(...); goto L1;
+    do CALL recv, <buf, ...>; goto L1;
   when (and(neq(cmd, SEND), neq(cmd, RECV)))
-    ; goto L1;
+    do NOOP; goto L1;
+  end choose
 L1:
 }