Changes between Version 49 and Version 50 of IR


Ignore:
Timestamp:
11/24/15 17:17:18 (10 years ago)
Author:
zmanchun
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • IR

    v49 v50  
    101101* `Pointer` : all pointers, a subtype of `Mem`
    102102 * `Pointer[T]` : pointer-to-T, subtype of `Pointer`
    103 * `DType`: dynamic type
     103* `Dytype`: dynamic type
    104104
    105105Type facts:
    … …  
    117117// type definitions
    118118Type S:=Tuple[Array[Integer]];
    119 _dynamic_S: DType;
     119_dynamic_S: Dytype;
    120120
    121121// variable decls
    … …  
    237237Example of declaration of a function:
    238238{{{
    239 f($real x, $bool y):integer;
     239f(Real x, Bool y; Integer);
    240240}}}
    241241
    242242Additional modifiers that may be placed on any of above:
    243 * `$pure` : the function has no side effects, but may be nondeterministic
    244 * `$abstract`: function is a pure, mathematical function: deterministic function of inputs
    245 * `$atomic_f`: function definition is atomic, and it never blocks
     243* `\pure` : the function has no side effects, but may be nondeterministic
     244* `\abstract`: function is a pure, mathematical function: deterministic function of inputs
     245* `\atomic_f`: function definition is atomic, and it never blocks
    246246
    247247System functions:
    … …  
    253253Example of a declaration of a system function with guard.
    254254{{{
    255 $bool g($real x, $bool y) { ... }
    256 $integer f($real x, $bool y) $guard {g};
     255g(Real x, Bool y; Bool) { ... }
     256f(Real x, Bool y; Integer) \guard {g};
    257257}}}
    258258
    … …  
    263263{{{
    264264EventSetExpression
    265  : $read(MemorySetExpression)
    266  | $write(MemorySetExpression)
    267  | $access(MemorySetExpression)
    268  | $calls(FunctionCallExpression)
    269  | $nothing
    270  | $everything
     265 : \read(MemorySetExpression)
     266 | \write(MemorySetExpression)
     267 | \access(MemorySetExpression)
     268 | \calls(FunctionCallExpression)
     269 | \nothing
     270 | \everything
    271271 | ‘(’ EventSetExpression ‘)’
    272272 | EventSetExpression + EventSetExpression
    … …  
    274274 | EventSetExpression & EventSetExpression
    275275}}}
    276 * depends clause: `$depends [condition] { event1, event2, ...}`
     276* depends clause: `\depends [condition] { event1, event2, ...}`
    277277 * Example:
    278278{{{
    279 $depends {
    280   $access(n) - ($calls(inc(MemorySetExpression)) + $calls(dec(MemorySetExpression)))
    281 }
    282 }}}
    283  * **absence of $depends clause**:
     279\depends {
     280  \access(n) - (\calls(inc(MemorySetExpression)) + \calls(dec(MemorySetExpression)))
     281}
     282}}}
     283 * **absence of \depends clause**:
    284284* assigns-or-reads clause
    285  * assigns clause: `$assigns [condition] {memory-list}`
    286  * reads clause: `$reads [condition] {memory-list}`
    287  * `$reads {$nothing}` implies `$assigns {$nothing}`
    288  * `$reads {$nothing}` is equivalent to: `$reads {$nothing} $assigns {$nothing}`
    289  * `$assigns {X}` where `X != $nothing`, implies `$reads {X}`
    290  * `$assigns {X}` is equivalent to:` $assigns{X} $reads{X}`
     285 * assigns clause: `\assigns [condition] {memory-list}`
     286 * reads clause: `\reads [condition] {memory-list}`
     287 * `\reads {\nothing}` implies `\assigns {\nothing}`
     288 * `\reads {\nothing}` is equivalent to: `\reads {\nothing} \assigns {\nothing}`
     289 * `\assigns {X}` where `X != \nothing`, implies `\reads {X}`
     290 * `\assigns {X}` is equivalent to:` \assigns{X} \reads{X}`
    291291 * absence:
    292   * absence of `$reads` clause: there is no assumption about the read access of the function, i.e., the function could read anything
    293   * absence of `$assigns` clause: similar to the absence of `$reads` clause
    294  * `$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.
    295 
    296 * For an independent function which has `$depends {$nothing}`, usually we also need to specify `$reads{nothing}`, for the purpose of reachability analysis.
     292  * absence of `\reads` clause: there is no assumption about the read access of the function, i.e., the function could read anything
     293  * absence of `\assigns` clause: similar to the absence of `\reads` clause
     294 * `\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.
     295
     296* For an independent function which has `\depends {\nothing}`, usually we also need to specify `\reads{nothing}`, for the purpose of reachability analysis.
    297297e.g.,
    298298{{{
    299299/* Returns the size of the given bundle b. */
    300 int $bundle_size($bundle b)
    301   $depends {$nothing}
    302   $reads {$nothing}
     300\bundle_size(Bundle b; Int)
     301  \depends {\nothing}
     302  \reads {\nothing}
    303303  ;
    304304}}}
    … …  
    306306* Example of a function declaration with contracts:
    307307{{{
    308 $atomic_f void sendRecv(int cmd, void*buf)
    309   $depends [cmd==SEND] {$write(buf)}
    310   $depends [cmd==RECV] {$access(*buf)}
    311   $assigns [cmd==SEND] {$nothing}
    312   $assigns [cmd==RECV] {*buf}
    313   $reads {*buf}
     308\atomic_f sendRecv(Int cmd, Pointer buf; Int)
     309  \depends [cmd==SEND] {$write(buf)}
     310  \depends [cmd==RECV] {$access(*buf)}
     311  \assigns [cmd==SEND] {$nothing}
     312  \assigns [cmd==RECV] {*buf}
     313  \reads {*buf}
    314314{
    315315  if(cmd == SEND){