Changes between Version 57 and Version 58 of IR


Ignore:
Timestamp:
11/25/15 16:08:40 (10 years ago)
Author:
siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • IR

    v57 v58  
    1313 * 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
    1414* an array is declared without any length expression.  When it is initialized it can specify length.
     15* curly braces are used only to indicate scopes
    1516
    1617Example:
    1718{{{
    18 f(): Integer {  // something like "f(x:Integer): Integer {" ?
     19f(u:Integer, a:Array[Real]): Integer {
    1920  x: Real;
    2021  y: Real;
    21   z: Float(16,23);
     22  z: Float[16,23];
    2223 
    2324L1 :
    24   {
    2525    when (g1) stmt1; goto L2;
    2626    when (g2) stmt2; goto L3;
    27   }
    2827
    2928  { // begin new scope
    3029    Real x;
    31 
    3230L2 :
    33     {
    3431      when (g3) stmt3; goto L4;
    3532      ...
    36     }
    3733  } // end new scope
    3834...
    … …  
    5248{
    5349  x: Integer;
    54   a_t : Dytype[Array[Integer]]; // I thought Dytype could be a parameterized type, where the parameter is the static type the dytype refines
     50  a_t : Dytype[Array[Integer]];
    5551  a: Array[Integer];
    5652L1:
    … …  
    7268* `Proc` : process type
    7369* `Scope` : scope type
    74 * `Char` : character type.  Alternatively, get rid of this and just use an integer type.
     70* `Char` : character type
    7571* `Bundle` : type representing some un-typed chunk of data
    7672* `Heap` : heap type
    … …  
    9086 * IEEE754 floating point numbers
    9187* `HerbrandReal` : Herbrand real numbers.  Values are unsimplified symbolic expressions.
    92 * `Struct` types **remove struct?**
    93  * `Struct tag { decl1; ...; decln };` or
    94  * `Struct tag;`
    95  * structure type with named fields.  Names may not seem necessary but if you want a subset of CIVL-C...
     88* `Tuple[T0, T1, ...]`: a tuple type, the Cartesian product of T0, T1, ...
    9689 * **What about bit-widths?**
    97 * `Tuple[type0, type1, ...]`: a tuple type which contains a sequence of sub-types
    98 * `Union`: similar to structs
    99 * `Array[T]` : array-of-T
    100 * `Function[S1,...,Sn;T]`
    101  * function consuming `S1,...,Sn` and returning `T`.  `T` can be void.  The actual notation is the horrible C notation.
     90* `Union[T0, T1, ...]`: union type, the disjoint union of T0, T1, ...
     91* `Array[T]` : arrays of any length whose elements belong to T
     92* `Function[(T0,T1,...),T]` : functions consuming T0,T1,... and returning T.  T can be `void` to indicate nothing is returned.
    10293* `Mem` : type representing a memory set.  May be thought of as a set of pointers.
    10394* `Pointer` : all pointers, a subtype of `Mem`
    104  * `Pointer[T]` : pointer-to-T, subtype of `Pointer`
    105 * `Dytype`: dynamic type
     95* `Pointer[T]` : pointer-to-T, subtype of `Pointer`
     96* `Dytype` : the set of all dynamic types
     97* `Dytype[T]`: dynamic types refining T.  Values of this type represent dynamic types that refine T.  For example `\dytype(Array[Integer,24])` has type `Dytype[Array[Integer]]`
    10698
    10799Type facts:
    108100
    109 **Pure types** contain no values anywhere in the type tree.  That is, there is no array length expression in the type.   The pure types are the static types of the CIVL-IR.  Each variable is declared to have some pure type.
    110 
    111 **Augmented types** include all the pure types plus possible length expressions.
    112 
    113 A **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.
    114 
    115 The 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.
    116 
    117 Example:
     101**Static types** are the types assigned to variables in a program statically.   A static type contains no values anywhere in the type tree.  That is, there is no array length expression in the type.  These are the types that are used in declarations.  Each variable is declared to have some static type.
     102
     103**Value types** are the types associated to values.   They include all the static types plus possible length expressions.  A value type refines a static type if when you delete the values from the value type you get the static type.
     104
     105A **type name** is a syntactic element that names a (static or value) type.  Examples of type names include `Array[Integer]` and `Array[Integer,24]`.
     106
     107The expression `\new(t)` takes a Dytype 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 tuple type is the tuple in which each component is assigned the initial value for its type.
     108
     109Example:  the C code
     110{{{
     111int n = 10;
     112struct S { int a[n]; };
     113struct S x1;
     114n=20;
     115struct S x2;
     116}}}
     117
     118may be translated as
     119
    118120{{{
    119121// type definitions
    120 // can we come up with a better way than \type here.  Maybe typedef?  At least you know the original
    121 // program can't use typedef as an identifier...
    122 // also I changed := to = since this is not an assignment.  it is a definition.
    123 \type S=Tuple[Array[Integer]];
     122typedef S=Tuple[Array[Integer]];
    124123
    125124// variable decls
    … …  
    137136}}}
    138137
    139 is semantically equivalent to the C code
    140 
    141 {{{
    142 int n = 10;
    143 struct S { int a[n]; };
    144 struct S x1;
    145 n=20;
    146 struct S x2;
    147 }}}
    148 
    149 
    150 
    151138
    152139== Expressions ==
    … …  
    156143* literals
    157144 * `\true`, `\false` : values of type `Bool`
    158  * 123, -123, 3.1415, etc. : values of type `Integer`, `Int`, `Real`, `Float`
    159   * **what particular notations for floating values?**
    160  * 'a', 'b', ... **UNICODE?**
    161  * `\array(T, (e0, e1, e2, ...))`: values of type `Array[T]`; and `\array(T, n, e)`: an array of type `T` with `n` elements each of which being `e`
    162  * `\tuple(S, (e0, e1, ...))` : values of type `S` (struct literal)
    163  * `e1..e2`, `e1..e2#e3` : values of type `\Range`
    164  * `\domain(r1,...,rn)` : value of type `Domain[n]`
    165  * `"abc"` : string literals: value of type `Array[Char]`
     145 * 123, -123, 3.1415, etc. : values of type `Integer`, `Int`, `Real`, `Float`.   **NEED TO BE MORE SPECIFIC**
     146 * 'a', 'b', ... : Char values.  **UNICODE?**
     147 * `\array(T, (e0, ..., en-1))`: value of type `Array[T, n]`, a literal array
     148 * `\array(T, n, e)`: value of type `Array[T,n]` in which each of the n elements is `e`
     149 * `\tuple(S, (e0, e1, ...))` : value of tuple type `S` (tuple literal)
     150 * `\range(e1,e2,e3)` : value of type `Range` consisting of the integers e1, e1+e3, e1+2*e3, ... that are less than or equal to e2.
     151 * `\domain(r1,...,rn)` : value of type `Domain[n]`, the ordered Cartesian product of the n ranges (dictionary order)
     152 * `"abc"` : string literals: value of type `Array[Char, n+1]`, where n is the length of the string (the last element is the character `\0`)
    166153 * `\root`, `\here` : values of type `Scope`
    167154 * `\self`, `\proc_null` : values of type `Proc`
    … …  
    170157* `\sizeof_type(t)` : the size of the dynamic type t
    171158* `\sizeof_expr(e)` : the size of the value of expression `e`
    172 * `\new(t)` : new (default) value of specified dynamic type
     159* `\new(t)` : new (default) value of dynamic type t
    173160* `\defined(e)` : is `e` defined? Type is `Bool`
    174 * `\has_next(dom, i, j, k, …)`: an expression of boolean type, testing if the domain `dom` contains any element after `(i, j, k, ...)`
     161* `\has_next(dom, (i, j, …))`: an expression of boolean type, testing if the domain `dom` contains any element after `(i, j, ...)`
    175162* `\add(e1, e2)` : numeric addition. 
    176163 * `e1` and `e2` have the same numeric type.  Note that there are no "automatic conversions" as there are in C.  If the original expressions have different types, explicit casts must be inserted. 
    177 * `\padd(e1, e2)`: pointer addition.
    178  * `e1` has pointer type and `e2` has an integer type.
     164* `\padd(e1, e2)`: pointer addition. `e1` has pointer type and `e2` has an integer type.
    179165* `\sub(e1, e2)` : subtraction
    180166* `\mul(e1, e2)` : multiplication
    … …  
    182168 * If both are integer types, the result is integer division.  Otherwise it is real division.  Need to define what happens for negative integers.
    183169* `\mod(e1, e2)` : modulus
    184 * `\array_subscript(e1, e2)` : array subscript expression.  Note that `e1` must have array type, not pointer type. (This is different from C.)   If `e1` has pointer type, use `\deref(\padd(e1, e2))` instead. 
    185  * **maybe shorten to `\sub`? --do you mean `\array_sub` instead?**
     170* `\asub(e1, e2)` : array subscript expression.  Note that `e1` must have array type, not pointer type. (This is different from C.)   If `e1` has pointer type, use `\deref(\padd(e1, e2))` instead. 
    186171* `\deref(e)` : pointer dereference
    187 * `\addressof(e)` : address-of.
     172* `\addressof(e)` : address-of operator
    188173* `\not(e)` : logical not
    189174* `\neg(e)` : negative
    … …  
    196181* `\cond(e1, e2, e3)`: conditional expression, equivalent to `e1?e2:e3` in C.
    197182* `\lt(e1, e2)`, `\lte(e1, e2)`: less than/less than or equal to
    198 * `e0(e1,...,en)` : a function call where `e` must evaluate to an abstract or pure system function
    199 * `\forall`, `\exists` :  `\forall {Integer i | e0} e1`. `\exits` is similar.  ** Is this the best notation? **
     183* `e0(e1,...,en)` : a function invocation where `e` must evaluate to an abstract or pure system function
     184* `\forall`, `\exists` :  `\forall {Integer i | e0} e1`. `\exists` is similar.  ** Is this the best notation? **
    200185* `\tuple_read(e1, i)`, some natural number i (tuple read)
    201186* `\bit_and(e1, e2)`, `\bit_or(e1, e2)`, `\bit_xor(e1, e2)`, `\bit_comp(e1)` : bit-wise operations: arguments are arrays of booleans
    202 * **Memory set expressions**: are these literal values of type `Mem`?
    203  * 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
    204  * `\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`.
    205  * `\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.
    206   * **\mem_reach ?**
    207  * `\mem_union(mem1, mem2)`, where `mem1` and `mem2` are expressions of type `Memory`.  This is the union of the two sets.
     187* 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
     188* `\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`.
     189* `\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.
     190 * **\mem_reach ?**
     191* `\mem_union(mem1, mem2)`, where `mem1` and `mem2` are expressions of type `Memory`.  This is the union of the two sets.
    208192 * **could we use Frama-C notation `p+(e1..e2)` for example?**
    209193