Changes between Version 53 and Version 54 of IR
- Timestamp:
- 11/25/15 09:48:10 (10 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
IR
v53 v54 5 5 6 6 * 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 7 * the language (and grammar) are subsets of CIVL-C. **MAYBE, MAYBE NOT**8 7 * a CIVL-IR program represents a guarded-transition system explicitly 9 8 * as in CIVL-C, there are functions, scopes, and functions can be defined in any scope … … 17 16 Example: 18 17 {{{ 19 f(;Integer) { 18 f(;Integer) { // now sure what this signature means. maybe something like "f(x:Integer): Integer {" ? 20 19 x: Real; 21 20 y: Real; … … 53 52 { 54 53 x: Integer; 55 a_t : Dytype[Array[Integer]]; 54 a_t : Dytype[Array[Integer]]; // I thought Dytype could be a parameterized type, where the parameter is the static type the dytype refines 56 55 a: Array[Integer]; 57 56 L1: … … 119 118 {{{ 120 119 // type definitions 120 // can we come up with a better way than \type here. Maybe typedef? At least you know the original 121 // program can't use typedef as an identifier... 122 // also I changed := to = since this is not an assignment. it is a definition. 121 123 \type S=Tuple[Array[Integer]]; 122 124 … … 155 157 * `\true`, `\false` : values of type `Bool` 156 158 * 123, -123, 3.1415, etc. : values of type `Integer`, `Int`, `Real`, `Float` 157 * what particular notations for floating values?158 * 'a', 'b', ... UNICODE?159 * `\cast(Array[T], {e0, e1, ...})` : values of type `Array[T]` 160 * `\cast(S, {e0, ...})` : values of type `S` (struct literal) 159 * **what particular notations for floating values?** 160 * 'a', 'b', ... **UNICODE?** 161 * `\cast(Array[T], {e0, e1, ...})` : values of type `Array[T]` **THIS IS NOT A CAST. Need better notation ** 162 * `\cast(S, {e0, ...})` : values of type `S` (struct literal) **THIS IS NOT A CAST. Need better notation ** 161 163 * `e1..e2`, `e1..e2#e3` : values of type `\Range` 162 * `\cast(Domain, {r1,...,rn})` : value of type `Domain[n]` 164 * `\cast(Domain, {r1,...,rn})` : value of type `Domain[n]` **NOT A CAST** 163 165 * `"abc"` : string literals: value of type `Array[Char]` 164 166 * `\root`, `\here` : values of type `Scope` … … 167 169 * variables 168 170 * `\sizeof_type(t)` : the size of the dynamic type t 169 * `\sizeof(e)` : the size of the value of expression `e` 171 * `\sizeof(e)` : the size of the value of expression `e` **Should this be \sizeof_expr since the other one is \sizeof_type ?** 170 172 * `\new(t)` : new (default) value of specified dynamic type 171 173 * `\defined(e)` : is `e` defined? Type is `Bool` … … 181 183 * `\mod(e1, e2)` : modulus 182 184 * `\array_subscript(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. 185 * **maybe shorten to `\sub`?** 183 186 * `\deref(e)` : pointer dereference 184 * `\address_of(e)` : address-of 187 * `\address_of(e)` : address-of. **Or: \addressof ? After all, we have \sizeof.** 185 188 * `\not(e)` : logical not 186 189 * `\neg(e)` : negative … … 188 191 * need to list all of the legal casts and what they mean exactly 189 192 * cast of integer to array-of-boolean, and vice-versa? 193 * **Instead of casts would it be better to have explicit functions for each legal kind of cast?** 190 194 * `\eq(e1, e2)`, `\neq(e1, e2)`: equality/inequality test 191 195 * `\and(e1, e2)`, `\or(e1, e2)`: logical and/or operation … … 193 197 * `\lt(e1, e2)`, `\lte(e1, e2)`: less than/less than or equal to 194 198 * `e0(e1,...,en)` : a function call where `e` must evaluate to an abstract or pure system function 195 * `\forall`, `\exists` : `\forall {Integer i | e0} e1`. `\exits` is similar. 199 * `\forall`, `\exists` : `\forall {Integer i | e0} e1`. `\exits` is similar. ** Is this the best notation? ** 196 200 * `\tuple_read(e1, i)`, some natural number i (tuple read) 197 201 * `\bit_and(e1, e2)`, `\bit_or(e1, e2)`, `\bit_xor(e1, e2)`, `\bit_comp(e1)` : bit-wise operations: arguments are arrays of booleans … … 200 204 * `\array_chunk(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`. 201 205 * `\region(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. 206 * **\mem_reach ?** 202 207 * `\mem_union(mem1, mem2)`, where `mem1` and `mem2` are expressions of type `Memory`. This is the union of the two sets. 203 208 * **could we use Frama-C notation `p+(e1..e2)` for example?** … … 210 215 * Call: `e0(e1,...,en);` and `e:=e0(e1,...,en);` 211 216 * regular function (one with flow graph) 212 * function can be system, pure, abstract?217 * ** distinguish this kind of call from an expression involving a pure system or abstract call???** 213 218 * Spawn: `\spawn e0(e1,...,en);` and `e:=\spawn e0(e1,...,en);` 214 219 * Wait: `\wait(e);` … … 228 233 * Atomic_enter: `\atomic_enter;` 229 234 * Atomic_exit: `\atomic_exit;` 230 * Parfor_spawn: `\parfor_spawn(int i,j,..: dom) f(i,j,...);` 231 * Domain iterator: `\next(dom, i, j,k, …)` updates `i`, `j`, `k`, ... to be the value of the inter tuple in `dom` after `(i, j, k, ...)`235 * Parfor_spawn: `\parfor_spawn(int i,j,..: dom) f(i,j,...);` ** Maybe `\parspawn` ? ** 236 * Domain iterator: `\next(dom,i,j,…)` updates `i`, `j`, ... to be the value of the inter tuple in `dom` after `(i, j, ...)` 232 237 * For_dom_enter (for domains): `\for_enter(i,j,k..: dom);` 233 238
