| 21 | | * unlike C, there is no "array-pointer pun". If an array `a` needs to be converted to a pointer, you must use \addr(\asub(a, 0))`. |
| 22 | | * there are no automatic conversions. All conversions must be by explicit casts or other functions. Operations such as numeric addition (`\add`) require that both operands have the exact same type. |
| | 21 | * unlike C, there is no "array-pointer pun". If an array `a` needs to be converted to a pointer, you must use addr(asub(a, 0))`. |
| | 22 | * there are no automatic conversions. All conversions must be by explicit casts or other functions. Operations such as numeric addition (`add`) require that both operands have the exact same type. |
| 156 | | * `\not(e)` : logical not |
| 157 | | * `\and(e1,e2)`, `\or(e1,e2)`: logical and/or operation. These operators are short-circuiting, which matters because of exception side-effects. |
| 158 | | * `\implies(e1,e2)`: logical implication. Short-circuiting. |
| 159 | | * `\eq(e1,e2)`, `\neq(e1,e2)`: equality/inequality test |
| 160 | | * `\forall(<i1:T1,i2:T2,...>,e)` : universal quantification. For all i1 in type T1, i2 in type T2, ..., e2 holds. |
| 161 | | * `\exists(<i1:T1,i2:T2,...>,e)`: existential quantification. There is some i1 in type T1, i2 in type T2, ..., such that e holds. |
| | 156 | * `not(e)` : logical not |
| | 157 | * `and(e1,e2)`, `or(e1,e2)`: logical and/or operation. These operators are short-circuiting, which matters because of exception side-effects. |
| | 158 | * `implies(e1,e2)`: logical implication. Short-circuiting. |
| | 159 | * `eq(e1,e2)`, `neq(e1,e2)`: equality/inequality test |
| | 160 | * `forall(<i1:T1,i2:T2,...>,e)` : universal quantification. For all i1 in type T1, i2 in type T2, ..., e2 holds. |
| | 161 | * `exists(<i1:T1,i2:T2,...>,e)`: existential quantification. There is some i1 in type T1, i2 in type T2, ..., such that e holds. |
| 177 | | * `\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. |
| 178 | | * `\domain(<r1,...,rn>)` : value of type `Domain[n]`, the Cartesian product of the n ranges, with dictionary order |
| 179 | | * `\hasnext(dom, <i,j,…>)`: an expression of boolean type, testing if the domain `dom` contains any element after `<i,j,...>` |
| | 177 | * `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. |
| | 178 | * `domain(<r1,...,rn>)` : value of type `Domain[n]`, the Cartesian product of the n ranges, with dictionary order |
| | 179 | * `hasnext(dom, <i,j,…>)`: an expression of boolean type, testing if the domain `dom` contains any element after `<i,j,...>` |
| 181 | | * `\array(T,<e0,...,en-1>)`: value of type `Array[T, n]`, a literal array |
| 182 | | * `\array(T,n,e)`: value of type `Array[T,n]` in which each of the n elements is `e` |
| 183 | | * `\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. |
| 184 | | * `\seq_add(a,e)` : array obtained by adding element e to the end of the array. Original array a is not modified. |
| 185 | | * `\seq_append(a1,a2)` : array obtained by concatenating two arrays. Original array not modified. |
| 186 | | * `\seq_remove(a,i)` : array obtained by removing element at position i from a. Original array a not modified. |
| 187 | | * `\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. |
| | 181 | * `array(T,<e0,...,en-1>)`: value of type `Array[T, n]`, a literal array |
| | 182 | * `array(T,n,e)`: value of type `Array[T,n]` in which each of the n elements is `e` |
| | 183 | * `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. |
| | 184 | * `seq_add(a,e)` : array obtained by adding element e to the end of the array. Original array a is not modified. |
| | 185 | * `seq_append(a1,a2)` : array obtained by concatenating two arrays. Original array not modified. |
| | 186 | * `seq_remove(a,i)` : array obtained by removing element at position i from a. Original array a not modified. |
| | 187 | * `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. |
| 192 | | * `\union_inj(U,i,x)` : `x` is in `Ti`, result is in the union type `U` |
| 193 | | * `\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`) |
| 194 | | * `\union_test(U,i,y)` : `y` is in `U`; determines if `y` is in the image under injection of `Ti`. Returns a Boolean. |
| | 192 | * `union_inj(U,i,x)` : `x` is in `Ti`, result is in the union type `U` |
| | 193 | * `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`) |
| | 194 | * `union_test(U,i,y)` : `y` is in `U`; determines if `y` is in the image under injection of `Ti`. Returns a Boolean. |
| 197 | | * `\deref(e)` : pointer dereference |
| 198 | | * `\addr(e)` : address-of operator |
| 199 | | * `\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. |
| 200 | | * `\psub(e1,e2)`: pointer subtraction |
| 201 | | * `\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. |
| 202 | | * `\mem_union(mem1,mem2)`, where `mem1` and `mem2` are expressions of type `Memory`. This is the union of the two memory sets. |
| 203 | | * `\mem_isect(mem1,mem1)` : set intersection |
| 204 | | * `\mem_comp(mem1)` : set complement (everything not in `mem1`) |
| 205 | | * `\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`. |
| | 197 | * `deref(e)` : pointer dereference |
| | 198 | * `addr(e)` : address-of operator |
| | 199 | * `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. |
| | 200 | * `psub(e1,e2)`: pointer subtraction |
| | 201 | * `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. |
| | 202 | * `mem_union(mem1,mem2)`, where `mem1` and `mem2` are expressions of type `Memory`. This is the union of the two memory sets. |
| | 203 | * `mem_isect(mem1,mem1)` : set intersection |
| | 204 | * `mem_comp(mem1)` : set complement (everything not in `mem1`) |
| | 205 | * `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`. |
| 211 | | * `\sizeof_type(t)` : the size of the dynamic type t; `Integer` type |
| 212 | | * `\sizeof_expr(e)` : the size of the value of expression `e`; `Integer` type |
| 213 | | * `\new(t)` : new (default) value of `Dytype` t |
| 214 | | * `\defined(e)` : is `e` defined? `Bool` type |
| 215 | | * `\cast(e,T)` : casts `e` to a value of the named type |
| | 211 | * `sizeof_type(t)` : the size of the dynamic type t; `Integer` type |
| | 212 | * `sizeof_expr(e)` : the size of the value of expression `e`; `Integer` type |
| | 213 | * `new(t)` : new (default) value of `Dytype` t |
| | 214 | * `defined(e)` : is `e` defined? `Bool` type |
| | 215 | * `cast(e,T)` : casts `e` to a value of the named type |
| 238 | | * To translate the C `malloc` you first need to figure out the type of the elements being malloced. If the argument to malloc is `n`, then you first need to insert an assertion `\eq(\mod(n, \sizeof_type(t)), 0)`, and then `ALLOCATE e, h, t, \div(n, \sizeof_type(t))`. |
| | 238 | * To translate the C `malloc` you first need to figure out the type of the elements being malloced. If the argument to malloc is `n`, then you first need to insert an assertion `eq(mod(n, sizeof_type(t)), 0)`, and then `ALLOCATE e, h, t, div(n, sizeof_type(t))`. |
| 260 | | * `\pure` : the function has no side effects, but may be nondeterministic |
| 261 | | * `\abstract`: function is a pure, mathematical function: deterministic function of inputs |
| 262 | | * `\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?** |
| | 260 | * `pure` : the function has no side effects, but may be nondeterministic |
| | 261 | * `abstract`: function is a pure, mathematical function: deterministic function of inputs |
| | 262 | * `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?** |
| 302 | | * assigns clause: `\assigns [condition] {memory-list}` |
| 303 | | * reads clause: `\reads [condition] {memory-list}` |
| 304 | | * `\reads {\nothing}` implies `\assigns {\nothing}` |
| 305 | | * `\reads {\nothing}` is equivalent to: `\reads {\nothing} \assigns {\nothing}` |
| 306 | | * `\assigns {X}` where `X != \nothing`, implies `\reads {X}` |
| 307 | | * `\assigns {X}` is equivalent to:` \assigns{X} \reads{X}` |
| | 302 | * assigns clause: `assigns [condition] {memory-list}` |
| | 303 | * reads clause: `reads [condition] {memory-list}` |
| | 304 | * `reads {nothing}` implies `assigns {nothing}` |
| | 305 | * `reads {\nothing}` is equivalent to: `reads {\nothing} assigns {\nothing}` |
| | 306 | * `assigns {X}` where `X != \nothing`, implies `reads {X}` |
| | 307 | * `assigns {X}` is equivalent to:` assigns{X} reads{X}` |
| 309 | | * absence of `\reads` clause: there is no assumption about the read access of the function, i.e., the function could read anything |
| 310 | | * absence of `\assigns` clause: similar to the absence of `\reads` clause |
| 311 | | * `\reads/\assigns {\nothing}` doesn’t necessarily means that the function never reads or assigns any variable. The function could still reads/assigns its “local” variables, including function parameters and any variable declared inside the function body. |
| 312 | | |
| 313 | | * For an independent function which has `\depends {\nothing}`, usually we also need to specify `\reads{nothing}`, for the purpose of reachability analysis. |
| | 309 | * absence of `reads` clause: there is no assumption about the read access of the function, i.e., the function could read anything |
| | 310 | * absence of `assigns` clause: similar to the absence of `reads` clause |
| | 311 | * `reads/assigns {\nothing}` doesn’t necessarily means that the function never reads or assigns any variable. The function could still reads/assigns its “local” variables, including function parameters and any variable declared inside the function body. |
| | 312 | |
| | 313 | * For an independent function which has `depends {\nothing}`, usually we also need to specify `reads{nothing}`, for the purpose of reachability analysis. |
| 325 | | \atomic_f sendRecv(Int cmd, Pointer buf; Int) |
| 326 | | \depends [\eq(cmd, SEND)] {\write(buf)} |
| 327 | | \depends [\eq(cmd, RECV)] {\access(\deref(buf))} |
| 328 | | \assigns [\eq(cmd, SEND)] {\nothing} |
| 329 | | \assigns [\eq(cmd, RECV)] {\deref(buf)} |
| 330 | | \reads {\deref(buf)} |
| | 325 | atomic_f sendRecv(Int cmd, Pointer buf; Int) |
| | 326 | depends [eq(cmd, SEND)] {write(buf)} |
| | 327 | depends [eq(cmd, RECV)] {access(deref(buf))} |
| | 328 | assigns [eq(cmd, SEND)] {\nothing} |
| | 329 | assigns [eq(cmd, RECV)] {deref(buf)} |
| | 330 | reads {deref(buf)} |
| 333 | | when (\eq(cmd, SEND)) |
| 334 | | send(\deref(buf), ...); goto L1; |
| 335 | | when (\eq(cmd, RECV)) |
| 336 | | \deref(buf):=recv(...); goto L1; |
| 337 | | when (\and(\neq(cmd, SEND), \neq(cmd, RECV))) |
| | 333 | when (eq(cmd, SEND)) |
| | 334 | send(deref(buf), ...); goto L1; |
| | 335 | when (eq(cmd, RECV)) |
| | 336 | deref(buf):=recv(...); goto L1; |
| | 337 | when (and(neq(cmd, SEND), neq(cmd, RECV))) |
