Changes between Version 16 and Version 17 of IR


Ignore:
Timestamp:
11/22/15 08:58:41 (10 years ago)
Author:
siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • IR

    v16 v17  
    22The CIVL-IR.  Also known as "CIVL model".
    33
    4 Grammar:
     4Properties of language:
    55
    6 * a subset of CIVL-C, explicit guarded-transition systems
    7 * functions, scopes, functions defined in any scope
    8 * all blocks start with variable declarations; no initializers
     6* the language (and grammar) are subsets of CIVL-C
     7* a CIVL-IR programs represents a guarded-transition system explicitly
     8* as in CIVL-C, there are functions, scopes, and functions can be defined in any scope
     9* all blocks (including a function body) consist of the following elements, in order:
     10 * a sequence of variable declarations with no initializers
     11 * a sequence of function definitions
     12 * 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
    913* an array is declared without any length expression.  When it is initialized it can specify length.
    1014
    … …  
    4044
    4145* `$bool` : boolean type, values are `$true` and `$false`
    42 * `$proc`
    43 * `$scope`
    44 * `$char`
    45 * `$mem`
    46 * `$bundle`
    47 * `$heap`
    48 * `$range`
    49 * `$domain`
    50  * `$domain(n)`, n is an integer at least 1; subtype of above
     46* `$proc` : process type
     47* `$scope` : scope type
     48* `$char` : character type.  Alternatively, get rid of this and just use an integer type.
     49* `$mem` : type representing set of memory units
     50* `$bundle` : type representing some un-typed chunk of data
     51* `$heap` : heap type
     52* `$range` : ordered set of integers
     53* `$domain` : ordered set of tuples of integers
     54 * `$domain(n)`, n is an integer at least 1; subtype of above in which all tuples have arity n.
    5155* `enum` types.
    52  * different from integers or like C?
     56 * **different from integers or like C?**
    5357* `$integer` : the mathematical integers
    5458* `$int(lo,hi,wrap)`
    5559 * lo, hi are integers, wrap is boolean
    5660 * 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.
     61* `$hint` : Herbrand integers.  Values are unsimplified symbolic expressions.
    5762* `$real` : the mathematical real numbers
    5863* `$float(e,f)`, e, f are integers, each at least 1
    5964 * IEEE754 floating point numbers
     65* `$hreal` : Herbrand real numbers.  Values are unsimplified symbolic expressions.
    6066* `struct(T1,...,Tn)`
    61  * Why do we need the field names?
     67 * structure type with named fields.  Names may not seem necessary but if you want a subset of CIVL-C...
    6268 * What about bit-widths?
    6369* `union(T1,...,Tn)` : similar to struct
    6470* `T[]` : array-of-T
    65 * `Function<S1,...,Sn;T>`
     71* Function<S1,...,Sn;T>
     72 * function consuming S1,...,Sn and returning T.  T can be void.  The actual notation is the horrible C notation.
    6673* `void*` : all pointers
    6774 * `T*` : pointer-to-T, subtype of above
    … …  
    162169== Libraries ==
    163170
    164