Changes between Version 46 and Version 47 of IR


Ignore:
Timestamp:
11/24/15 16:00:10 (10 years ago)
Author:
zmanchun
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • IR

    v46 v47  
    1212 * a sequence of variable declarations with no initializers
    1313 * a sequence of function definitions
    14  * a sequence of labeled `$choose` statements.   Each clause in the choose statement is a `$when` statement with some guard and a primitive statement, followed by a `goto` statement
     14 * a sequence of labeled statements.   Each clause in the labeled statement is a `\when` statement with some guard and a primitive statement, followed by a `\goto` statement
    1515* an array is declared without any length expression.  When it is initialized it can specify length.
    1616
    1717Example:
    1818{{{
    19 \Integer f() {
    20   \Real x;
    21   \Rreal y;
    22   \Float(16,23) z;
     19f(;Integer) {
     20  x: Real;
     21  y: Real;
     22  z: Float(16,23);
    2323 
    2424L1 :
    2525  {
    26     $when (g1) stmt1; goto L2;
    27     $when (g2) stmt2; goto L3;
     26    \when (g1) stmt1; \goto L2;
     27    \when (g2) stmt2; \goto L3;
    2828  }
    2929
    3030  { // begin new scope
    31     \Real x;
     31    Real x;
    3232
    3333L2 :
    3434    {
    35       $when (g3) stmt3; goto L4;
     35      \when (g3) stmt3; \goto L4;
    3636      ...
    3737    }
    … …  
    4545{{{
    4646{
    47   \Integer x=3*y;
    48   \Array(\Integer, x+1) a;
     47  int x=3*y;
     48  int a[x+1];
    4949}
    5050}}}
    … …  
    5252{{{
    5353{
    54   \Integer x;
    55   \Array(\Integer) a;
     54  x: Integer;
     55  a: Array[Integer];
    5656L1:
    57   { $when ($true) x=3*y; goto L2; }
     57  { \when (\true) x:=3*y; \goto L2; }
    5858L2:
    59   { $when ($true) a=\initval(\Array(\Integer, x+1)); goto L3; }
     59  { \when (\true) a:=\new(Array[Integer, x+1]); \goto L3; }
    6060L3:
    6161}
    … …  
    6767The types are:
    6868
    69 * `\Bool` : boolean type, values are `$true` and `$false`
    70 * `\Proc` : process type
    71 * `\Scope` : scope type
    72 * `\Char` : character type.  Alternatively, get rid of this and just use an integer type.
    73 * `\Bundle` : type representing some un-typed chunk of data
    74 * `\Heap` : heap type
    75 * `\Range` : ordered set of integers
    76 * `\Domain` : ordered set of tuples of integers
    77 * `\Domain(n)`, n is an integer at least 1; subtype of `$domain` in which all tuples have arity n.
    78 * `\Enum` types.
     69* `Bool` : boolean type, values are `\true` and `\false`
     70* `Proc` : process type
     71* `Scope` : scope type
     72* `Char` : character type.  Alternatively, get rid of this and just use an integer type.
     73* `Bundle` : type representing some un-typed chunk of data
     74* `Heap` : heap type
     75* `Range` : ordered set of integers
     76* `Domain` : ordered set of tuples of integers
     77* `Domain[n]`, n is an integer at least 1; subtype of `Domain` in which all tuples have arity n.
     78* `Enum` types.
    7979 * **different from integers or like C?**
    80 * `\Integer` : the mathematical integers
    81 * `\Int(lo,hi,wrap)`
     80* `Integer` : the mathematical integers
     81* `Int[lo,hi,wrap]`
    8282 * `lo`, `hi` are integers, `wrap` is boolean
    8383 * finite interval of integers `[lo,hi]`.  If `wrap` is true then all operations "wrap", otherwise, any operation resulting in a value outside of the interval results in an exception being thrown.
    84  * **Do we want to allow `lo` and `hi` to be any values of type `$integer`, which means they are dynamic types, like complete array types?**
    85 * `\Hint` : Herbrand integers.  Values are unsimplified symbolic expressions.
    86 * `\Real` : the mathematical real numbers
    87 * `\Float(e,f)`, e, f are integers, each at least 1.  **Same question for e and f as for lo and hi.**
     84 * **Do we want to allow `lo` and `hi` to be any values of type `Integer`, which means they are dynamic types, like complete array types?**
     85* `HerbrandInt` : Herbrand integers.  Values are unsimplified symbolic expressions.
     86* `Real` : the mathematical real numbers
     87* `Float[e,f]`, e, f are integers, each at least 1.  **Same question for e and f as for lo and hi.**
    8888 * IEEE754 floating point numbers
    89 * `\Hreal` : Herbrand real numbers.  Values are unsimplified symbolic expressions.
    90 * `\Struct` types
    91  * `\Struct tag { decl1; ...; decln };` or
    92  * `\Struct tag;`
     89* `HerbrandReal` : Herbrand real numbers.  Values are unsimplified symbolic expressions.
     90* `Struct` types **remove struct?**
     91 * `Struct tag { decl1; ...; decln };` or
     92 * `Struct tag;`
    9393 * structure type with named fields.  Names may not seem necessary but if you want a subset of CIVL-C...
    9494 * **What about bit-widths?**
    95 * `\Union`: similar to structs
    96 * `\Array(T)` : array-of-T
    97 * `\Function(S1,...,Sn;T)`
     95* `Tuple[type0, type1, ...]`: a tuple type which contains a sequence of sub-types
     96* `Union`: similar to structs
     97* `Array[T]` : array-of-T
     98* `Function[S1,...,Sn;T]`
    9899 * function consuming `S1,...,Sn` and returning `T`.  `T` can be void.  The actual notation is the horrible C notation.
    99 * `\Mem` : type representing a memory set.  May be thought of as a set of pointers.
    100 * `\Pointer(\Void)` : all pointers, a subtype of `\Mem`
    101  * `\Pointer(T)` : pointer-to-T, subtype of `\Pointer(\Void)`
     100* `Mem` : type representing a memory set.  May be thought of as a set of pointers.
     101* `Pointer` : all pointers, a subtype of `Mem`
     102 * `Pointer[T]` : pointer-to-T, subtype of `Pointer`
    102103
    103104Type facts:
    … …  
    109110A **type name** is a syntactic element that names a (pure or augmented) type  Examples include `int[]` and `int[n*m]`.  This is the same as in C.
    110111
    111 The expression `\initval(T)` takes a type name and returns the initial value for an object of that type.   The initial value of `\Integer` and other primitive (non-compound) types is "undefined".   The initial value of `\Array(\Integer)` is an array of length 0 of `\Integer`.  The initial value of `\Pointer(\Real)` is the undefined pointer to `\Real`.    The initial value of `\Array(\Real, 10)` is the array of length 10 in which each element is undefined.  In general, the initial value of an array of length n is the sequence of length n in which every element is the initial value of the element type of the array.   The initial value of a structure is the tuple in which each component is assigned the initial value for its type.
     112The expression `\new(T)` takes a type name and returns the initial value for an object of that type.   The initial value of `Integer` and other primitive (non-compound) types is "undefined".   The initial value of `Array[Integer]` is an array of length 0 of `Integer`.  The initial value of `Pointer[Real]` is the undefined pointer to `Real`.    The initial value of `Array[Real, 10]` is the array of length 10 in which each element is undefined.  In general, the initial value of an array of length n is the sequence of length n in which every element is the initial value of the element type of the array.   The initial value of a structure is the tuple in which each component is assigned the initial value for its type.
    112113
    113114Example:
    114115{{{
    115116// type definitions
    116 \Struct S { \Array(\Integer) a;}
     117Type S:=Tuple[Array[Integer]];
    117118
    118119// variable decls
    119 \Integer n;
    120 \Struct S _S_init;
    121 \Struct S x1;
    122 \Struct S x2;
     120n: Integer;
     121_S_init: S;
     122x1: S;
     123x2: S;
    123124
    124125// statements (leaving out the chooses and whens for brevity)
    125 n=10;
    126 _S_init=\initval(\Struct S { \Array(\Integer, n) a; };
    127 x1=_S_init;
    128 n=20;
    129 x2=_S_init;
     126n:=10;
     127_S_init:=\new(Tuple[Array[Integer, n]]);
     128x1:=_S_init;
     129n:=20;
     130x2:=_S_init;
    130131}}}
    131132
    … …  
    145146== Expressions ==
    146147
    147 In the following list of expressions, `e`, `e0`, `e1`, etc., are expressions.  `T` is a type name. `t` is an expression of type `$type`.
     148In the following list of expressions, `e`, `e0`, `e1`, etc., are expressions.  `T` is a type name. `t` is an expression of type `Type`.
    148149
    149150* literals
    150  * `$true`, `$false` : values of type `\Bool`
    151  * 123, -123, 3.1415, etc. : values of type `\Integer`, `\Int`, `\Real`, `\Float`
     151 * `\true`, `\false` : values of type `Bool`
     152 * 123, -123, 3.1415, etc. : values of type `Integer`, `Int`, `Real`, `Float`
    152153  * what particular notations for floating values?
    153154 * 'a', 'b', ... UNICODE?
    154  * `\cast(\Array(T), {e0, e1, ...})` : values of type `\Array(T)`
     155 * `\cast(Array[T], {e0, e1, ...})` : values of type `Array[T]`
    155156 * `\cast(S, {e0, ...})` : values of type `S` (struct literal)
    156157 * `e1..e2`, `e1..e2#e3` : values of type `\Range`
    157  * `($domain){r1,...,rn}` : value of type `$domain(n)`
    158  * `"abc"` : string literals: value of type `$char[]`
    159  * `$root`, `$here` : values of type `$scope`
    160  * `$self`, `$proc_null` : values of type `$proc`
     158 * `\cast(Domain, {r1,...,rn})` : value of type `Domain[n]`
     159 * `"abc"` : string literals: value of type `Array[Char]`
     160 * `\root`, `\here` : values of type `Scope`
     161 * `\self`, `\proc_null` : values of type `Proc`
    161162 * `NULL` : value of type `void*`
    162163* variables
    163 * `\sizeof(T)` : the size of the named type
     164* `\sizeof_type(T)` : the size of the named type
    164165* `\sizeof(e)` : the size of the value of expression `e`
    165 * `\initval(T)` : initial value of the named type
    166 * `\defined(e)` : is `e` defined? Type is `$bool`
     166* `\new(T)` : initial value of the named type
     167* `\defined(e)` : is `e` defined? Type is `Bool`
    167168* `\has_next(dom, i, j, k, …)`: an expression of boolean type, testing if the domain `dom` contains any element after `(i, j, k, ...)`
    168169* `\add(e1, e2)` : numeric addition. 
    … …  
    170171* `\padd(e1, e2)`: pointer addition.
    171172 * `e1` has pointer type and `e2` has an integer type.
    172 * `\subtract(e1, e2)` : subtraction
    173 * `\multiply(e1, e2)` : multiplication
    174 * `\divide(e1, e2)` : division
     173* `\sub(e1, e2)` : subtraction
     174* `\mul(e1, e2)` : multiplication
     175* `\div(e1, e2)` : division
    175176 * If both are integer types, the result is integer division.  Otherwise it is real division.  Need to define what happens for negative integers.
    176177* `\mod(e1, e2)` : modulus
    … …  
    188189* `\lt(e1, e2)`, `\lte(e1, e2)`: less than/less than or equal to
    189190* `e0(e1,...,en)` : a function call where `e` must evaluate to an abstract or pure system function
    190 * `\forall`, `\exists` :  `\forall {\Integer i | e0} e1` or `\forall {\Integer i| e0}`
    191 * `e1.i`, some natural number i (tuple read)
    192 * `e1&e2`, `e1|e2`, `e1^e2`, `~e1` : bit-wise operations: arguments are arrays of booleans
    193 * **Memory set expressions**: are these literal values of type `$mem`?
    194  * a left-hand-side expression, when used in certain contexts, is automatically converted to `$mem`.  The contexts are: arguments to the built-in functions `$access`, `$read`, and `$write` described below, or occurrence in the list of an `$assigns` clause
    195  * `a[dom]`, where `a` is an expression of array type and `dom` is an expression of `$domain` type.   The dimension of the array must match the dimension of the domain.   This represents all memory units which are the cells in the array indexed by a tuple in `dom`.
    196  * `$region(ptr)`, where `ptr` is an expression with a pointer type.  This represents the set of all memory units reachable from `ptr`, including the memory unit pointed to by `ptr` itself.
    197  * `mem1+mem2`, where `mem1` and `mem2` are expressions of type `$memory`.  This is the union of the two sets.  **Problem this is ambiguous with numeric +, as in x+y.**
     191* `\forall`, `\exists` :  `\forall {Integer i | e0} e1`. `\exits` is similar.
     192* `\tuple_read(e1, i)`, some natural number i (tuple read)
     193* `\bit_and(e1, e2)`, `\bit_or(e1, e2)`, `\bit_xor(e1, e2)`, `\bit_comp(e1)` : bit-wise operations: arguments are arrays of booleans
     194* **Memory set expressions**: are these literal values of type `Mem`?
     195 * a left-hand-side expression, when used in certain contexts, is automatically converted to `Mem`.  The contexts are: arguments to the built-in functions `\access`, `\read`, and `\write` described below, or occurrence in the list of an `\assigns` clause
     196 * `\array_chunk(a, dom)`, where `a` is an expression of array type and `dom` is an expression of `Domain` type.   The dimension of the array must match the dimension of the domain.   This represents all memory units which are the cells in the array indexed by a tuple in `dom`.
     197 * `\region(ptr)`, where `ptr` is an expression with a pointer type.  This represents the set of all memory units reachable from `ptr`, including the memory unit pointed to by `ptr` itself.
     198 * `\mem_union(mem1, mem2)`, where `mem1` and `mem2` are expressions of type `Memory`.  This is the union of the two sets.
    198199 * **could we use Frama-C notation `p+(e1..e2)` for example?**
    199200 * **are there conversions between pointers and mems?**
    200201
    201 Pointers: unlike C, there is no "array-pointer pun".   If an array `a` needs to be converted to a pointer, you must use `&a[0]`.
     202Pointers: unlike C, there is no "array-pointer pun".   If an array `a` needs to be converted to a pointer, you must use `\address_of(\address_of(\array_subscript(a, 0)))`.
    202203
    203204== The Primitive Statements ==
    204205
    205 * Assign:  `e1=e2;`
    206 * Call: `e0(e1,...,en);` and `e=e0(e1,...,en);`
     206* Assign:  `e1:=e2;`
     207* Call: `e0(e1,...,en);` and `e:=e0(e1,...,en);`
    207208 * regular function (one with flow graph)
    208209 * function can be system, pure, abstract?
    209 * Spawn: `$spawn e0(e1,...,en);` and `e=$spawn e0(e1,...,en);`
    210 * Wait: `$wait(e);`
    211 * Wailtall: `$waitall(e, n)` where `e` is the pointer to an array element and `n` is the number of processes to be waited for;
     210* Spawn: `\spawn e0(e1,...,en);` and `e:=\spawn e0(e1,...,en);`
     211* Wait: `\wait(e);`
     212* Wailtall: `\waitall(e)` where `e` is an array of process references (`Proc`) to be waited for;
    212213* Allocation
    213  * `e=$allocate(h,t,e);`, where
    214   * `h` as type `$heap`
    215   * `t` has type `$type`
     214 * `e:=\allocate(h,t,e);`, where
     215  * `h` as type `Heap`
     216  * `t` has type `Type`
    216217  * `e` has integer type.
    217218 * Allocates `e` objects of type `t` on heap `h`
    218  * To translate the C `malloc` you first need to figure out the type of the elements being malloced.  If the argument to malloc is `n`, then you first need to insert an assertion `n%$sizeof(t)==0`, and then `$allocate(h,t,n/$sizeof(t))`.
    219 * Free: `free(p);`
     219 * To translate the C `malloc` you first need to figure out the type of the elements being malloced.  If the argument to malloc is `n`, then you first need to insert an assertion `\eq(\mod(n, \sizeof_type(t)), 0)`, and then `\allocate(h,t,\div(n, \sizeof_t(t)))`.
     220* Free: `\free(p);`
    220221* Expression statement: `e;`, where `e` is side effect free except that it might contain error/exception (e.g., array index out of bound, division by zero);
    221222* Noop: `;`
    222223 * **Is there a need to add annotations for "true" or "false" branch, etc.?**  If so, we can just make these parameters to the Noop.
    223 * Return: `return;` and `return e;`
    224 * Atomic_enter: `$atomic_enter;`
    225 * Atomic_exit: `$atomic_exit;`
    226 * Parfor_spawn: `$parfor_spawn(int i,j,..: dom) f(i,j,...);`
    227 * Domain iterator: `$next(dom, i, j,k,  …)` updates `i`, `j`, `k`, ... to be the value of the inter tuple in `dom` after `(i, j, k, ...)`
    228 * For_dom_enter (for domains): `$for_enter(i,j,k..: dom);`
     224* Return: `\return;` and `\return e;`
     225* Atomic_enter: `\atomic_enter;`
     226* Atomic_exit: `\atomic_exit;`
     227* Parfor_spawn: `\parfor_spawn(int i,j,..: dom) f(i,j,...);`
     228* Domain iterator: `\next(dom, i, j,k,  …)` updates `i`, `j`, `k`, ... to be the value of the inter tuple in `dom` after `(i, j, k, ...)`
     229* For_dom_enter (for domains): `\for_enter(i,j,k..: dom);`
    229230
    230231== Declarations and Function Definitions ==