Changes between Version 43 and Version 44 of IR

Timestamp:

11/24/15 08:54:38 (10 years ago)

Author:

siegel

Comment:

--

IR

@@ -5 +5 @@
 
 * the language is not intended to be written by humans; it is an intermediate form constructed by CIVL.  However it should be readable to help debug things
-* the language (and grammar) are subsets of CIVL-C
+* the language (and grammar) are subsets of CIVL-C. **MAYBE, MAYBE NOT**
 * a CIVL-IR program represents a guarded-transition system explicitly
 * as in CIVL-C, there are functions, scopes, and functions can be defined in any scope
-* all blocks (including a function body) consist of the following elements:
+* all blocks (including a function body) consist of the following elements, in this order:
  * a sequence of type definitions
  * a sequence of variable declarations with no initializers
@@ -15 +15 @@
 * an array is declared without any length expression.  When it is initialized it can specify length.
 
-**Can we specify that elements must appear in the order above?**  Or would that create a problem in something like
-{{{
-{
-  $integer x=3*y;
-  $integer a[x+1];
-}
-}}}
-
-
 Example:
-
 {{{
 $integer f() {
@@ -52 +42 @@
 }}}
 
+Example:
+{{{
+{
+  $integer x=3*y;
+  $integer a[x+1];
+}
+}}}
+translates to:
+{{{
+{
+  $integer x;
+  $integer a[];
+L1:
+  $choose { $when ($true) x=3*y; goto L2; }
+L2:
+  $choose { $when ($true) a=$initval($integer[x+1]); goto L3; }
+L3:
+}
+
+
 ==  Types ==
 
@@ -60 +70 @@
 * `$scope` : scope type
 * `$char` : character type.  Alternatively, get rid of this and just use an integer type.
-* `$mem` : type representing set of memory units
 * `$bundle` : type representing some un-typed chunk of data
 * `$heap` : heap type
 * `$range` : ordered set of integers
 * `$domain` : ordered set of tuples of integers
- * `$domain(n)`, n is an integer at least 1; subtype of above in which all tuples have arity n.
+* `$domain(n)`, n is an integer at least 1; subtype of `$domain` in which all tuples have arity n.
 * `enum` types.
  * **different from integers or like C?**
@@ -78 +87 @@
  * IEEE754 floating point numbers
 * `$hreal` : Herbrand real numbers.  Values are unsimplified symbolic expressions.
-* `struct(T1,...,Tn)`
+* `struct` types
+ * `struct tag { decl1; ...; decln };` or
+ * `struct tag;`
  * structure type with named fields.  Names may not seem necessary but if you want a subset of CIVL-C...
  * **What about bit-widths?**
-* `union(T1,...,Tn)` : similar to struct
+* `union`: similar to structs
 * `T[]` : array-of-T
 * Function<S1,...,Sn;T>
  * function consuming S1,...,Sn and returning T.  T can be void.  The actual notation is the horrible C notation.
-* `void*` : all pointers
- * `T*` : pointer-to-T, subtype of above
+* `$mem` : type representing a memory set.  May be thought of as a set of pointers.
+* `void*` : all pointers, a subtype of `$mem`
+ * `T*` : pointer-to-T, subtype of `void*`
 
 Type facts:
@@ -128 +140 @@
 
 
-== Declarations ==
-
-Declarations follow the C notation.   Function prototypes are considered to be declarations similar to variable declarations.
-
-Example of declaration of a function:
-{{{
-$integer f($real x, $bool y);
-}}}
-
-Additional modifiers that may be placed on any of above: 
-* `$pure` : the function has no side effects, but may be nondeterministic
-* `$abstract`: function is a pure, mathematical function: deterministic function of inputs
-* `$atomic_f`: function definition is atomic, and it never blocks
-
-System functions:
-* A function declaration which is not abstract and for which no definition is provided is a system function.
-* If the system function is called anywhere in the program, it must be defined by providing Java code in an Enabler and Executor.  Failure to do so will result in an exception.
-* A system function may modify any memory it can reach.  This includes allocating new data on heaps it can reach.
-* A system function may have a guard.
-
-Example of a declaration of a system function with guard.
-{{{
-$bool g($real x, $bool y) { ... }
-$integer f($real x, $bool y) $guard {g};
-}}}
 
 
@@ -239 +226 @@
 * For_dom_enter (for domains): `$for_enter(i,j,k..: dom);`
 
-
-== Contracts of Functions ==
+== Declarations and Function Definitions ==
+
+Declarations follow the C notation.   Function prototypes are considered to be declarations similar to variable declarations.
+
+Example of declaration of a function:
+{{{
+$integer f($real x, $bool y);
+}}}
+
+Additional modifiers that may be placed on any of above: 
+* `$pure` : the function has no side effects, but may be nondeterministic
+* `$abstract`: function is a pure, mathematical function: deterministic function of inputs
+* `$atomic_f`: function definition is atomic, and it never blocks
+
+System functions:
+* A function declaration which is not abstract and for which no definition is provided is a system function.
+* If the system function is called anywhere in the program, it must be defined by providing Java code in an Enabler and Executor.  Failure to do so will result in an exception.
+* A system function may modify any memory it can reach.  This includes allocating new data on heaps it can reach.
+* A system function may have a guard.
+
+Example of a declaration of a system function with guard.
+{{{
+$bool g($real x, $bool y) { ... }
+$integer f($real x, $bool y) $guard {g};
+}}}
+
+
+== Function Contracts ==
+
 * event set expressions:
 {{{
@@ -302 +316 @@
 }}}
 
-== Function definition ==
-
 == Program ==
 
@@ -321 +333 @@
 
 
-
 === Transitions ===
 
 
-
 == Libraries ==