Changes between Version 74 and Version 75 of IR


Ignore:
Timestamp:
11/26/15 15:47:13 (10 years ago)
Author:
siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • IR

    v74 v75  
    11
    22The CIVL-IR language.  A program in this language is also known as a "CIVL model".
    3 
    4 ** CAN WE GET RID OF ALL \S EVERYWHERE???**
    53
    64Properties of the language:
    … …  
    2523Example:
    2624{{{
    27 f(u:Integer, a:Array[Real]): Integer {
     25def f(u:Integer, a:Array[Real]): Integer {
    2826  x: Real;
    2927  y: Real;
    … …  
    3129 
    3230L1 :
    33     when (g1) stmt1; goto L2;
    34     when (g2) stmt2; goto L3;
     31    when g1 do stmt1; goto L2;
     32    when g2 do stmt2; goto L3;
    3533
    3634  { // begin new scope
    3735   x: Real;
    3836L2 :
    39       when (g3) stmt3; goto L4;
     37      when g3 do stmt3; goto L4;
    4038      ...
    4139  } // end new scope
    … …  
    5957  a: Array[Integer];
    6058L1:
    61   when (\true) ASSIGN x, mul(3,y); goto L2;
     59  when true do ASSIGN "x", mul(3,"y"); goto L2;
    6260L2:
    63   when(\true) ASSIGN a_t, dytype(Array[Integer, add(x,1)]); goto L3;
     61  when true do ASSIGN "a_t", dytype(Array[Integer, add("x",1)]); goto L3;
    6462L3:
    65   when (\true) ASSIGN a, new(a_t); goto L4;
     63  when true do ASSIGN "a", new("a_t"); goto L4;
    6664L4:
    6765}
    … …  
    7371The types are:
    7472
    75 * `Bool` : boolean type, values are `\true` and `\false`
     73* `Bool` : boolean type, values are `true` and `false`
    7674* `Proc` : process type
    7775* `Scope` : scope type
    … …  
    8684* `Integer` : the mathematical integers
    8785* `Int[lo,hi,wrap]`
    88  * `lo`, `hi` are integers, `wrap` is boolean
     86 * `lo`, `hi` are concrete (?) integers, `wrap` is boolean
    8987 * 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.
    9088 * **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?**
    9189* `HerbrandInt` : Herbrand integers.  Values are unsimplified symbolic expressions.
    9290* `Real` : the mathematical real numbers
    93 * `Float[e,f]`, e, f are integers, each at least 1.  **Same question for e and f as for lo and hi.**
     91* `Float[e,f]`, `e`, `f` are concrete integers, each at least 1.
    9492 * IEEE754 floating point numbers
    9593* `HerbrandReal` : Herbrand real numbers.  Values are unsimplified symbolic expressions.
    … …  
    135133
    136134L0:
    137   when (\true) ASSIGN n, 10; goto L1;
     135  when true do ASSIGN "n", 10; goto L1;
    138136L1:
    139   when (\true) ASSIGN S_d, dytype(Tuple[<Array[Integer, n]]>); goto L2;
     137  when true do ASSIGN "S_d", dytype(Tuple[<Array[Integer, "n"]]>); goto L2;
    140138L2:
    141   when (\true) ASSIGN x1, new(S_d); goto L3;
     139  when true do ASSIGN "x1", new("S_d"); goto L3;
    142140L3:
    143   when (\true) ASSIGN n, 20; goto L4;
     141  when true do ASSIGN "n", 20; goto L4;
    144142L4:
    145   when (\true) ASSIGN x2, new(S_d); goto L5;
     143  when true do ASSIGN "x2", new("S_d"); goto L5;
    146144L5:
    147145}}}
    … …  
    153151
    154152Logical
    155 * `\true`, `\false` : literal values of type `Bool`
     153* `true`, `false` : literal values of type `Bool`
    156154* `not(e)` : logical not
    157155* `and(e1,e2)`, `or(e1,e2)`: logical and/or operation.  These operators are short-circuiting, which matters because of exception side-effects.
    … …  
    173171Characters and Strings
    174172* 'a', 'b', ... : Char values.  **UNICODE?**
    175 * `"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`)
     173* `string("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`)
    176174Ranges and Domains
    177175* `range(e1,e2,e3)` : value of type `Range`.  If `e3` is positive, the integers e1, e1+e3, e1+2*e3, ... that are less than or equal to `e2`.  If `e3` is negative, the integers e1, e1+e3, e1+2*e3, ... that are greater than or equal to `e2`.  Exception if `e3` is 0.
    … …  
    205203* `mem_slice(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`.
    206204Scopes and Processes
    207 * `\root`, `\here` : values of type `Scope`
    208 * `\self`, `\proc_null` : values of type `Proc`
    209 Other
    210 * variables
     205* `root`, `here` : values of type `Scope`
     206* `self`, `proc_null` : values of type `Proc`
     207Other expressions
     208* `"x"` : x is an identifier, naming either a type, variable, or function
    211209* `sizeof_type(t)` : the size of the dynamic type t; `Integer` type
    212210* `sizeof_expr(e)` : the size of the value of expression `e`; `Integer` type
    … …  
    219217* `ite(e1,e2,e3)`: if-then-else (conditional) expression, like `e1?e2:e3` in C.
    220218* `call(e0,<e1,...,en>)` : a function invocation where `e0` must evaluate to either an abstract or pure system function
     219* `choose_int(e)` : nondeterministic choice of integer
    221220
    222221== The Primitive Statements ==
    … …  
    261260* `abstract`: function is a pure, mathematical function: deterministic function of inputs
    262261* `atomic`: function definition is atomic, and it never blocks **ISN'T THIS TRUE OF EVERY SYSTEM FUNCTION?  IN WHICH CASE, IS THIS ONLY FOR NON-SYSTEM FUNCTIONS?**
    263 * `'lib="..."`: function is a system function defined in specified library
     262* `lib="..."`: function is a system function defined in specified library
     263* `guard="...":` the name of the guard function
    264264
    265265System functions:
    … …  
    272272{{{
    273273g(x:Real):Bool { ... }
    274 def[lib="Blah"] f(x:Real):Integer guard g;
     274def[lib="Blah",guard="g"] f(x:Real):Integer;
    275275}}}
    276276
    … …  
    344344== Program ==
    345345
    346 A program consists of a sequence of global variable declarations, which may include declarations annotated by `$input` and `$output`,
     346A program consists of a sequence of global variable declarations, which may include declarations annotated by `input` and `output`,
    347347followed by a sequence of function declarations and definitions.
    348 * `\input`
    349 * `\output`
     348* `input`
     349* `output`
    350350
    351351== Semantics ==
    … …  
    365365
    366366== Libraries ==
     367
     368Which libraries require system functions?
     369pointer, ...
     370Should these be called part of the language, or not?
     371