Changes between Version 33 and Version 34 of IR

Timestamp:

11/23/15 14:40:30 (10 years ago)

Author:

zmanchun

Comment:

--

IR

@@ -257 +257 @@
  | EventSetExpression & EventSetExpression
 }}}
-
-* depends clause:
-`dependsClause: $depends [condition] { EventSetExpression}`
-
-Example:
+* depends clause: `$depends [condition] { event1, event2, ...}`
+ * Example:
 {{{
 $depends {
-  $access(n) - ($calls(inc(MemorySetExpression)) + $calls(dec(MemorySetExpression)))}
-}}}
-
-
+  $access(n) - ($calls(inc(MemorySetExpression)) + $calls(dec(MemorySetExpression)))
+}
+}}}
+ * **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:
+  * 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.
+e.g., 
+{{{
+/* Returns the size of the given bundle b. */
+int $bundle_size($bundle b)
+  $depends {$nothing}
+  $reads {$nothing}
+  ;
+}}}
+
+* Example of a function declaration with contracts: 
+{{{
+$atomic_f void sendRecv(int cmd, void*buf)
+  $depends [cmd==SEND] {$write(buf)}
+  $depends [cmd==RECV] {$access(*buf)}
+  $assigns [cmd==SEND] {$nothing}
+  $assigns [cmd==RECV] {*buf}
+  $reads {*buf}
+{
+  if(cmd == SEND){
+     send(*buf, ...);
+  }else if(cmd==RECV){
+    *buf=recv(...);
+  }
+}
+}}}
 
 == Program Graph ==