Changes between Version 139 and Version 140 of IR

Timestamp:

01/11/16 17:33:34 (10 years ago)

Author:

zmanchun

Comment:

--

IR

@@ -394 +394 @@
 fun[options] foo(x:Integer, ...) : Real
   // contract clauses (optional):
-  requires expr;
-  ensures expr ;
-  mpi_requires expr ;
-  mpi_ensures expr ;
-  behavior name:
-    assigns expr ;
-    reads expr ;
-    depends actions ;
+  Requires expr;
+  Ensures expr ;
+  MPI_requires expr ;
+  MPI_ensures expr ;
+  Behavior name:
+    Assigns expr ;
+    Reads expr ;
+    Depends actions ;
 {
   // all of the following are missing for a system function...
@@ -451 +451 @@
 
 
-=== Function Contracts ===
-
-[wiki:Function_Contracts]
-
-* action expressions:
- * `read(e)`: `e` has type `Mem`. The function reads the memory units specified by `e`.
- * `write(e)`: `e` has type `Mem`. The function writes the memory units specified by `e`.
- * `call(f, <e1, ...>)`: `f` has type `Function`. The function calls `f` with parameters `e1, ...`.
- * `noaction`: no action
- * `anyaction`: all actions
- * `act_union(ma0, ma1)`: the union of the two memory set actions `ma0` and `ma1`.
- * `act_comp(ma0, ma1)`: action complement (everything not in `ma1`)
- * `act_isect(ma0, ma1)`: action intersection
-
-* depends clause: `depends action0, action1, action2, ... `
- * Example: `depends act_union(act_comp(read(n), call(inc, <x>))), call(dec, <y>))`
- * 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
- * absence of `reads`/`assigns` clause: there is no assumption about the read/assign access of the function, i.e., the function could read/assign 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. **check it**
-
-* For an independent function which has `depends coaction`, 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): Integer
-  depends nothing
-  reads b
-  ;
-}}}
-
-* Example of a function declaration with contracts: 
-{{{
-fun[atomic] sendRecv(Int cmd, Pointer buf): Integer
-  reads deref(buf);
-  behavior send:
-    depends writes(buf);
-    assigns nothing;
-  behavior receive:
-    depends access(deref(buf));
-    assigns deref(buf);
-{
-  begin choose
-  when eq(cmd, 0)
-     do CALL send, <buf, ...>; goto L1;
-  when eq(cmd, 1)
-    do CALL recv, <buf, ...>; goto L1;
-  when and(neq(cmd, 0), neq(cmd, 1))
-    do NOOP; goto L1;
-  end choose
-L1:
-}
-}}}
+Function Contracts: 
+ * [wiki:Function_Contracts] 
 
 == Program ==