Context Navigation

Changes between Version 97 and Version 98 of IR

Timestamp:: 11/30/15 09:31:30 (10 years ago)
Author:: siegel
Comment:: --

Legend:

: Unmodified
: Added
: Removed
: Modified

IR

-              v97
+              v98
 Notes:
 * If goto is missing, default is the next location.
 * If guard missing, deafult is true.
+* If guard missing, default is `true`.
 …
 ...
+}
-// etc.
 }}}
 …
 * `Union[<T0, T1, ...>]`: union type, the disjoint union of `T0`, `T1`, ...
 * `Array[T]` : arrays of any length whose elements belong to T
 * `Function[<T0,T1,...>,T]` : functions consuming T0,T1,... and returning T.  T can be `void` to indicate nothing is returned.
+* `Function[<T0,T1,...>,T]` : functions consuming `T0`,`T1`,... and returning `T`.  `T` can be `void` to indicate nothing is returned.
 * `Mem` : type representing a memory set.  May be thought of as a set of pointers.
 * `Pointer` : all pointers, a subtype of `Mem`
 * `Pointer[T]` : pointer-to-T, subtype of `Pointer`
+* `Pointer[T]` : pointer-to-`T`, subtype of `Pointer`
 * `Dytype` : the set of all dynamic types
+* `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]]`
+* `Dytype[T]`: dynamic types refining `T`, for a static type `T`.
+ * Values of this type represent dynamic types that refine `T`.  For example `dytype(Array[Integer,24])` has static type `Dytype[Array[Integer]]`
 Type facts:
 …
 * `true`, `false` : literal values of type `Bool`
 * `not(e)` : logical not
+* `and(e1,e2)`, `or(e1,e2)`: logical and/or operation.  These operators are short-circuiting, which matters because of exception side-effects.
+* `and(e1,e2)`, `or(e1,e2)`: logical and/or operation.
+ * These operators are short-circuiting, which matters because of exception side-effects.
 * `implies(e1,e2)`: logical implication.  Short-circuiting.
 * `eq(e1,e2)`, `neq(e1,e2)`: equality/inequality test
 …
 * `ceil(e)` : given a real or floating number, returns the least `Integer` greater than or equal to it.
 * `abs(e)`: given any numeric expression e, returns the absolute value; result is same type as `e`.
+* `pow(e,n)`: given any numeric expression e and expression `n` of any integral type, returns e to the n-th power.  `n` must evaluate to a nonnegative integer.
+* `herbrand(e)`: given a numeric value of type `T`, returns the value as type `Herbrand[T]`, a trivial symbolic expression consisting of a single node.
+* `eval(e)` : given a value of type `Herbrand[T]`, returns the value of type `T` obtained by evaluating all the delayed operations
+* `pow(e,n)`: power operator
+ * given any numeric expression e and expression `n` of any integral type, returns e to the n-th power.
+ * `n` must evaluate to a nonnegative integer.
+* `herbrand(e)`: "Herbrandize" a numeric value.
+ * given a numeric value of type `T`, returns the value as type `Herbrand[T]`, a trivial symbolic expression consisting of a single node.
+* `eval(e)` : evaluate a Herbrand expression
+ * given a value of type `Herbrand[T]`, returns the value of type `T` obtained by evaluating all the delayed operations
+ * exceptions may be thrown if evaluating any of the delayed operations results in an exception
 Characters and Strings
 * 'a', 'b', ... : Char values.  **UNICODE?**
+* `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`)
+* `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`)
 Ranges and Domains
+* `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.
+* `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.
 * `domain(<r1,...,rn>)` : value of type `Domain[n]`, the Cartesian product of the n ranges, with dictionary order
 * `hasnext(dom, <i,j,…>)`: an expression of boolean type, testing if the domain `dom` contains any element after `<i,j,...>`
+* `hasnext(dom, <i,j,…>)`: an expression of type `Bool`, testing if the domain `dom` contains any element after `<i,j,...>`
 Arrays (which are also Sequences)
 * `array(T,<e0,...,en-1>)`: value of type `Array[T, n]`, a literal array
 * `array(T,n,e)`: value of type `Array[T,n]` in which each of the n elements is `e`
+* `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.
+* `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.
 * `seq_add(a,e)` : array obtained by adding element e to the end of the array.  Original array a is not modified.
 * `seq_append(a1,a2)` : array obtained by concatenating two arrays.  Original array not modified.
 …
 * `seq_insert(a,i,x)` : array obtained by inserting an element x at position i in a.
 * `seq_length(a)` : returns length of array a (an `Integer`)
+* `bit_and(e1, e2)`, `bit_or(e1, e2)`, `bit_xor(e1, e2)`, `bit_comp(e1)` : bit-wise operations: arguments are arrays of booleans of equal length.
+* `bit_and(e1, e2)`, `bit_or(e1, e2)`, `bit_xor(e1, e2)`, `bit_comp(e1)` : bit-wise operations
+ * arguments are arrays of booleans of the same length
 Tuples
 …
 * `union_inj(U,i,x)` : `x` is in `Ti`, result is in the union type `U`
 * `union_sel(U,i,y)` : `y` is in `U`, result is in `Ti` (or exception if `y` is not in image of injection from `Ti`)
 * `union_test(U,i,y)` : `y` is in `U`; determines if `y` is in the image under injection of `Ti`.  Returns a Boolean.
+* `union_test(U,i,y)` : `y` is in `U`; determines if `y` is in the image under injection of `Ti`.  Returns a `Bool`.
 Pointers and Memory
 …
 * `deref(e)` : pointer dereference
 * `addr(e)` : address-of operator
+* `padd(e1,e2)`: pointer addition. `e1` has pointer type and `e2` has an integer type or range type.  If `e2` has integer type the result has pointer type.   Otherwise, the result has `Mem` type.
+* `padd(e1,e2)`: pointer addition.
+ * `e1` has pointer type and `e2` has an integer type or range type.
+ * If `e2` has integer type the result has pointer type.   Otherwise, the result has `Mem` type. (**BETTER TO USE A DIFFERENT FUNCTION?**)
 * `psub(e1,e2)`: pointer subtraction
+* `mem_reach(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.
+* `mem_union(mem1,mem2)`, where `mem1` and `mem2` are expressions of type `Memory`.  This is the union of the two memory sets.
+ * Both args must have same type `Pointer[T]` for some `T`.
+ * Result has type `Integer`
+* `mem_reach(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.
+* `mem_union(mem1,mem2)`, where `mem1` and `mem2` are expressions of type `Memory`.
+ * This is the union of the two memory sets.
 * `mem_isect(mem1,mem1)` : set intersection
 * `mem_comp(mem1)` : set complement (everything not in `mem1`)
+* `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`.
+* `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`.
 Scopes and Processes
 …
 Types
 * `new(t)` : new (default) value of `Dytype` t.  If `t` has type `Dytype[T]`, then this expression has static type `T`.
+* `typeof(e)` : returns the value of type `Dytype` representing the value type of `e`.  If `e` has static type `T` then this expression has static type `Dytype[T]`.
+* `typeof(e)` : returns the value of type `Dytype` representing the value type of `e`.
+ * If `e` has static type `T` then this expression has static type `Dytype[T]`.
 * `subtype(t1,t2)`: is `t1` a subtype of `t2`?  Both args have type `Dytype`.  Returns a `Bool`
 * `sizeof_type(t)` : the size of the dynamic type `t`; return an `Integer`
+* `cast(e,t)` : casts `e` to a value of dytype `t`.  If `t` has type `Dytype[T]`, this expression has static type `T` and the value will have dynamic type `t`.
+* `cast(e,t)` : casts `e` to a value of dytype `t`.
+ * If `t` has type `Dytype[T]`, this expression has static type `T` and the value will have dynamic type `t`.
  * A cast can only take place when there is no change to the underlying value in the concrete semantics.  It is only for changing the type.
  * One can cast from any integral type to another (as the values in all cases are integers), but there might be an exception if the value is not in the range of the targeted type.
 …
 * `sizeof_expr(e)` : the size of the value of expression `e`; return an `Integer`
 * `defined(e)` : is `e` defined? `Bool` type
+* `ite(e1,e2,e3)`: if-then-else (conditional) expression, like `e1?e2:e3` in C.   `e1` must have `Bool` type.  `e2` and `e3` must have the same static types, which is the static type of the result.
+* `ite(e1,e2,e3)`: if-then-else (conditional) expression, like `e1?e2:e3` in C.
+ * `e1` must have `Bool` type.  `e2` and `e3` must have the same static types, which is the static type of the result.
 * `call(e0,<e1,...,en>)` : a function invocation where `e0` must evaluate to either an abstract or pure system function
 * `choose_int(e)` : nondeterministic choice of integer
 …
 * `pure` : the function has no side effects, but may be nondeterministic
 * `abstract`: function is a pure, mathematical function: deterministic function of inputs
+* `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?**
+* `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?**
 * `lib="..."`: function is a system function defined in specified library
 * `guard="...":` the name of the guard function