| 1 | # CIVL Libraries
|
|---|
| 2 |
|
|---|
| 3 | In progress.
|
|---|
| 4 |
|
|---|
| 5 | ## bundle
|
|---|
| 6 |
|
|---|
| 7 | Header: [bundle.cvh](https://github.com/verified-software-lab/civl/blob/main/mods/dev.civl.abc/src/dev/civl/abc/include/bundle.cvh).
|
|---|
| 8 | Uses: [op](#op).
|
|---|
| 9 |
|
|---|
| 10 | A bundle is a sequence of objects of the same type, wrapped into an atomic package.
|
|---|
| 11 | A bundle is created using a function that specifies a region of memory.
|
|---|
| 12 | One can create a bundle from an array of integers, and another bundle from an array of reals.
|
|---|
| 13 | Both bundles have the same type, `$bundle`.
|
|---|
| 14 | They can therefore be entered into an array of `$bundle`, for example.
|
|---|
| 15 | Hence bundles are useful for mixing objects of different (even statically unknown) types into a single data structure.
|
|---|
| 16 | Later, the contents of a bundle can be extracted with another function that specifies a region of memory into which to unpack the bundle;
|
|---|
| 17 | if that memory does not have the right type to receive the contents of the bundle, a runtime error occurs.
|
|---|
| 18 |
|
|---|
| 19 | ### Types
|
|---|
| 20 | * `$bundle`: the bundle type
|
|---|
| 21 |
|
|---|
| 22 | ### Functions
|
|---|
| 23 | * `$system int $bundle_size($bundle b)`
|
|---|
| 24 | * Returns the size of the given bundle, i.e., the number of bytes consumed by all elements of the bundle. This is the product of the number of elements and the size of one element.
|
|---|
| 25 | * `$system $bundle $bundle_pack(void *ptr, int size)`
|
|---|
| 26 | * This function creates a bundle from the memory region specified by `ptr` and `size` (the total number of bytes to copy), copying the data into the new bundle. It returns the new bundle.
|
|---|
| 27 | * `$system void $bundle_unpack($bundle b, void *ptr)`
|
|---|
| 28 | * This function copies the data from the given bundle into the memory region starting at `ptr`. The memory region extends for `$bundle_size(b)` bytes.
|
|---|
| 29 | * `$atomic_f void $bundle_unpack_apply($bundle data, void *buf, $operation op, int count, void *result)`
|
|---|
| 30 | * This function unpacks the bundle while applying the specified numeric operation. Parameter `op` specifies a binary operation. For each *i* in 0..*count*-1, the operation is applied to the *i*-th element of `buf` and the *i*-th element of the bundle, and the result is stored in the *i*-th position of `result`. Parameter `count` is the number of elements in the bundle; `buf` and `result` should each point to a region of memory capable of holding at least `count` elements.
|
|---|
| 31 |
|
|---|
| 32 | ### Example
|
|---|
| 33 | ```civl
|
|---|
| 34 | #include <bundle.cvh>
|
|---|
| 35 | int main() {
|
|---|
| 36 | int n = 10;
|
|---|
| 37 | int a[n], b[n], c[n];
|
|---|
| 38 | for (int i=0; i<n; i++) a[i] = i;
|
|---|
| 39 | $bundle bun = $bundle_pack(a, n*sizeof(int));
|
|---|
| 40 | $assert($bundle_size(bun) == n*sizeof(int));
|
|---|
| 41 | $bundle_unpack(bun, b);
|
|---|
| 42 | $assert($forall (int i: 0..n-1) b[i]==a[i]);
|
|---|
| 43 | $bundle_unpack_apply(bun, b, _SUM, n, c);
|
|---|
| 44 | $assert($forall (int i: 0..n-1) c[i]==2*a[i]);
|
|---|
| 45 | }
|
|---|
| 46 | ```
|
|---|
| 47 |
|
|---|
| 48 | ## comm {#comm}
|
|---|
| 49 |
|
|---|
| 50 | Header: [comm.cvh](https://github.com/verified-software-lab/civl/blob/main/mods/dev.civl.abc/src/dev/civl/abc/include/comm.cvh).
|
|---|
| 51 | Uses: [bundle](#bundle).
|
|---|
| 52 |
|
|---|
| 53 | The comm library supports message-passing-style communication.
|
|---|
| 54 | It provides a number of basic data structures which can be used to implement specific message-passing interfaces, such as MPI.
|
|---|
| 55 |
|
|---|
| 56 | ### Types
|
|---|
| 57 | * `$message`: A message consists of data and meta-data. The data is a finite sequence of objects, all of the same type. The meta-data consists of 3 integers: the source, destination, and tag. The source identifies the process that sent the message. The destination identifies the process to which the message is sent. Both `source` and `destination` are "places", which are nonnegative integer IDs that abstract places from which messages are sent or received. Typically, a single place is associated to each process in a message-passing system, but this is not required. The tag is an additional nonnegative integer that can be used to represent anything the user wants; the receiving process may select a message based on the tag.
|
|---|
| 58 | * `$gcomm`: This is an opaque handle to an object that stores the state of the message-passing system. In particular, the buffered messages (those that have been sent, but not yet received) are stored in the gcomm.
|
|---|
| 59 | * `$comm`: Each place has its own comm, an opaque handle local to that place that is used to access all message-passing functions (e.g., sends and receives) at that place. It contains a reference to the gcomm.
|
|---|
| 60 |
|
|---|
| 61 | ### Constants
|
|---|
| 62 | * `$COMM_ANY_SOURCE`: a constant that can be used as the source argument in a dequeue operation to indicate that a message may be taken from any source
|
|---|
| 63 | * `$COMM_ANY_TAG`: a constant that can be used as the tag argument in a dequeue operation to indicate that a message with any tag may be selected
|
|---|
| 64 | * `$comm_null`: a constant representing the absence of `$comm`
|
|---|
| 65 |
|
|---|
| 66 | ### Functions
|
|---|
| 67 | * `$atomic_f $message $message_pack(int source, int dest, int tag, const void *data, int size)`
|
|---|
| 68 | * Creates a new message with the given meta-data, and the data taken from the memory region that begins at `data` and extends for `size` bytes. The data is copied into the new message object. The source, destination, and tag must be nonnegative. The size may be 0.
|
|---|
| 69 | * `$atomic_f int $message_source($message message)`
|
|---|
| 70 | * Gets the source of the message.
|
|---|
| 71 | * `$atomic_f int $message_tag($message message)`
|
|---|
| 72 | * Gets the tag of the message.
|
|---|
| 73 | * `$atomic_f int $message_dest($message message)`
|
|---|
| 74 | * Gets the destination of the message.
|
|---|
| 75 | * `$atomic_f int $message_size($message message)`
|
|---|
| 76 | * Gets the size of the message data (in bytes).
|
|---|
| 77 | * `$atomic_f void $message_unpack($message message, void *buf, int size)`
|
|---|
| 78 | * Extracts the data from a message, storing it in the buffer that starts at `buf`. The argument `size` must be greater than or equal to the size of message, else an error occurs.
|
|---|
| 79 | * `$atomic_f $gcomm $gcomm_create($scope scope, int size)`
|
|---|
| 80 | * Allocates a new gcomm object that will be stored in the heap of the specified scope. The `size` is the number of "places" that will be associated to this gcomm. The place IDs range from 0 to `size`-1 (inclusive).
|
|---|
| 81 | * `$atomic_f int $gcomm_destroy($gcomm gcomm, void * junkMsgs)`
|
|---|
| 82 | * Destroys the gcomm, deallocating memory that was allocated for it. If `junkMsgs` is not NULL it shall be a pointer to an array of indeterminate length of `$message`. This function will populate that array with all messages remaining the gcomm's buffers and return the number of such messages.
|
|---|
| 83 | * `$atomic_f void $gcomm_dup($comm comm, $comm newcomm)`
|
|---|
| 84 | * Duplicates the communicator `comm`. The `newcomm` is initialized to have the same gcomm and place as the original `comm`.
|
|---|
| 85 | * `$atomic_f $comm $comm_create($scope scope, $gcomm gcomm, int place)`
|
|---|
| 86 | * Creates a new `comm` associated with the specified `place` in `gcomm`. If `place` is less than 0, or greater than the size of `gcomm`, or another process has already occupied `place` in `gcomm`, an error occurs. The new comm object is allocated in the heap of the given scope.
|
|---|
| 87 | * `$atomic_f void $comm_destroy($comm comm)`
|
|---|
| 88 | * Deallocates the comm.
|
|---|
| 89 | * `$atomic_f int $comm_size($comm comm)`
|
|---|
| 90 | * Gets the size of the gcomm that owns `comm`.
|
|---|
| 91 | * `$atomic_f int $comm_place($comm comm)`
|
|---|
| 92 | * Gets the place of the given `comm` in its gcomm object.
|
|---|
| 93 | * `$system void $comm_enqueue($comm comm, $message message)`
|
|---|
| 94 | * Enqueues a message in a FIFO channel in the gcomm. The message should have its source be the place of `comm`. The message will enqueued on channel *(i,j)* in the gcomm, where *i* is the place of the source, and *j* is the place of the destination of the message.
|
|---|
| 95 | * `$system $state_f _Bool $comm_probe($comm comm, int source, int tag)`
|
|---|
| 96 | * Determines whether there exists a message with the given source and tag, and with destination the place of `comm`, in the gcomm associated to `comm`. `source` may be `$COMM_ANY_SOURCE` and `tag` may be `$COMM_ANY_TAG`.
|
|---|
| 97 | * `$system $message $comm_seek($comm comm, int source, int tag)`
|
|---|
| 98 | * Returns the oldest message in the gcomm associated to `comm` that matches `source` and `tag` without modifying gcomm. `source` may be `$COMM_ANY_SOURCE` and `tag` may be `$COMM_ANY_TAG`. If no such message found, returns a message with empty data and all meta-data being `-1`.
|
|---|
| 99 | * `$system $message $comm_dequeue($comm comm, int source, int tag)`
|
|---|
| 100 | * Dequeues a message in a FIFO channel in the gcomm. The message should have its destination be the place of `comm`. The message will be dequeued from channel *(i,j)* in the gcomm, where *i* is the place of the source, and *j* is the place of the destination of the message. A call to this function will not return until a matching message can be dequeued.
|
|---|
| 101 | * `$system $state_f _Bool $comm_empty_in($comm )`
|
|---|
| 102 | * deprecated
|
|---|
| 103 | * `$system $state_f _Bool $comm_empty_out($comm )`
|
|---|
| 104 | * deprecated
|
|---|
| 105 |
|
|---|
| 106 |
|
|---|
| 107 |
|
|---|
| 108 | ## concurrency {#concurrency}
|
|---|
| 109 |
|
|---|
| 110 | Header: [concurrency.cvh](https://github.com/verified-software-lab/civl/blob/main/mods/dev.civl.abc/src/dev/civl/abc/include/concurrency.cvh).
|
|---|
| 111 | Uses: [bundle](#bundle).
|
|---|
| 112 |
|
|---|
| 113 | ### Types
|
|---|
| 114 | * `$gbarrier`
|
|---|
| 115 | * A data type representing a handle to a global barrier object.
|
|---|
| 116 | * `$barrier`
|
|---|
| 117 | * A data type representing a process-local handle used to operate a global barrier
|
|---|
| 118 |
|
|---|
| 119 | ### Functions
|
|---|
| 120 | * `$atomic_f $gbarrier $gbarrier_create($scope scope, int size)`
|
|---|
| 121 | * Creates a new global barrier object and returns a handle to it. The barrier has the specified `size`. The new object will be allocated in the given `scope`.
|
|---|
| 122 | * `$atomic_f void $gbarrier_destroy($gbarrier gbarrier)`
|
|---|
| 123 | * Destroys the global barrier object referred by the handle `gbarrier`
|
|---|
| 124 | * `int $get_nprocs($gbarrier gbarrier)`
|
|---|
| 125 | * Returns the size of the global barrier object
|
|---|
| 126 | * `$atomic_f $barrier $barrier_create($scope scope, $gbarrier gbarrier, int place)`
|
|---|
| 127 | * Creates a process-local handle for operating the global barrier referred by `gbarrier`. The `place` must be in [0,`get_nprocs(gbarrier)`-1]. It specifies the place in the global barrier that will be occupied by the local handle.
|
|---|
| 128 | * `$atomic_f void $barrier_destroy($barrier barrier)`
|
|---|
| 129 | * Destroys the local handle to a global barrier
|
|---|
| 130 | * `void $barrier_call($barrier barrier)`
|
|---|
| 131 | * Calls the barrier referred by `barrier`
|
|---|
| 132 | * `void $barrier_call_yield($barrier barrier)`
|
|---|
| 133 | * Calls the barrier from within an atomic section: this will yield at the point where process is waiting to exit barrier.
|
|---|
| 134 | * `void $barrier_call_subset($barrier barrier, int nprocs)`
|
|---|
| 135 | * under construction
|
|---|
| 136 | * `void $barrier_call_execute($barrier barrier, void foo(void))`
|
|---|
| 137 | * under construction
|
|---|
| 138 |
|
|---|
| 139 | ## domain {#domain}
|
|---|
| 140 |
|
|---|
| 141 | Header: [domain.cvh](https://github.com/verified-software-lab/civl/blob/main/mods/dev.civl.abc/src/dev/civl/abc/include/domain.cvh).
|
|---|
| 142 | Uses: (nothing).
|
|---|
| 143 |
|
|---|
| 144 | ### Types
|
|---|
| 145 | * `$domain_strategy`
|
|---|
| 146 | * An enumeration type used to specify how domains are decomposed. There are three options: `ALL`, `RANDOM`, and `ROUND_ROBIN`.
|
|---|
| 147 | * `$domain_decomposition`
|
|---|
| 148 | * A data structure representing the decomposition result of a domain.
|
|---|
| 149 |
|
|---|
| 150 | ### Functions
|
|---|
| 151 | * `$system $domain_decomposition $domain_partition($domain domain, $domain_strategy strategy, int n)`
|
|---|
| 152 | * Takes a domain and some n>0 and returns some partition of the domain into n sub-domains, according to the decomposition strategy specified.
|
|---|
| 153 | * `$system $range $range_of_rectangular_domain($domain dom, int index)`
|
|---|
| 154 | * Returns the `index`-th range of the given domain `dom`. Requires `index` to be between 1 and the dimension of `dom` minus 1.
|
|---|
| 155 | * `$system int $high_of_regular_range($range range)`
|
|---|
| 156 | * Returns the upper bound of a regular range.
|
|---|
| 157 | * `$system int $low_of_regular_range($range range)`
|
|---|
| 158 | * Returns the lower bound of a regular range.
|
|---|
| 159 | * `$system int $step_of_regular_range($range range)`
|
|---|
| 160 | * Returns the step of a regular range
|
|---|
| 161 | * `$system _Bool $is_rectangular_domain($domain domain)`
|
|---|
| 162 | * Returns true if this `domain` is a rectangular domain.
|
|---|
| 163 | * `$system _Bool $is_regular_range($range range)`
|
|---|
| 164 | * Returns true if this `range` is a regular range, i.e., it is composed of a lower bound, a higher bound and a step.
|
|---|
| 165 | * `$system int $dimension_of($domain domain)`
|
|---|
| 166 | * Returns the dimension of the given domain.
|
|---|
| 167 |
|
|---|
| 168 | ## mem {#mem}
|
|---|
| 169 |
|
|---|
| 170 | Header: [mem.cvh](https://github.com/verified-software-lab/civl/blob/main/mods/dev.civl.abc/src/dev/civl/abc/include/mem.cvh).
|
|---|
| 171 | Uses: (nothing).
|
|---|
| 172 |
|
|---|
| 173 | The `mem` library provides functions to manipulate objects of the CIVL-C built-in type---`$mem`. A `$mem` object represents a set of memory locations.
|
|---|
| 174 |
|
|---|
| 175 | ### Functions
|
|---|
| 176 |
|
|---|
| 177 | * `$system void $write_set_push()`
|
|---|
| 178 | * Pushes a new entry (i.e. an empty `$mem`) onto the write stack of the calling process. Each process maintains a write stack. A stack entry is a `$mem` object. A write to a memory location will cause the memory location being added to the top entry of the write stack, if the stack is non-empty.
|
|---|
| 179 | * `$system $mem $write_set_pop()`
|
|---|
| 180 | * Pops and returns the top entry of the write stack of the calling process.
|
|---|
| 181 | * `$state_f $system $mem $write_set_peek()`
|
|---|
| 182 | * Returns the top entry of the write stack of the calling process.
|
|---|
| 183 | * `$system void $read_set_push()`
|
|---|
| 184 | * Pushes a new entry (i.e. an empty `$mem`) onto the read stack of the calling process. Each process maintains a read stack. A stack entry is a `$mem` object. Reading a memory location will cause the memory location being added to the top entry of the read stack, if the stack is non-empty.
|
|---|
| 185 | * `$system $mem $read_set_pop()`
|
|---|
| 186 | * Pops and returns the top entry of the read stack of the calling process.
|
|---|
| 187 | * `$state_f $system $mem $read_set_peek()`
|
|---|
| 188 | * Returns the top entry of the read stack of the calling process.
|
|---|
| 189 | * `$atomic_f $system $mem $mem_empty()`
|
|---|
| 190 | * Creates a new empty `$mem` object.
|
|---|
| 191 | * `$atomic_f $system _Bool $mem_equals($mem m0, $mem m1)`
|
|---|
| 192 | * Returns true iff `m0` and `m1` are the identical set of memory locations.
|
|---|
| 193 | * `$atomic_f $system _Bool $mem_contains($mem super, $mem sub)`
|
|---|
| 194 | * Returns true iff `super` is a super-set of `sub`.
|
|---|
| 195 | * `$atomic_f $system _Bool $mem_no_intersect($mem m0, $mem m1, $mem *out0, $mem *out1)`
|
|---|
| 196 | * Returns true iff `m0` and `m1` are two disjoint sets. If `m0` and `m1` overlap, `out0` and `out1` will be assigned two overlapping memory location sets, which are as small as the function can figure out from `m0` and `m1`, respectively.
|
|---|
| 197 | * `$atomic_f $system $mem $mem_union($mem mem0, $mem mem1)`
|
|---|
| 198 | * Returns the union of the two sets of memory locations `mem0` and `mem1`.
|
|---|
| 199 | * `$atomic_f $system $mem $mem_union_widening($mem, $mem)`
|
|---|
| 200 | * Similar to the `$mem_union` function but may return an over-approximated super-set of the union set. The over-approximation is done by the model checker in order to make state space finite.
|
|---|
| 201 | * `$atomic_f $system void $mem_havoc($mem m)`
|
|---|
| 202 | * Assigns arbitrary values to memory locations in `m`
|
|---|
| 203 | * `$atomic_f $system $mem $mem_unary_widening($mem m)`
|
|---|
| 204 | * Returns an over-approximated super-set of `m`. The over-approximation is done by the model checker in order to make state space finite.
|
|---|
| 205 | * `$atomic_f $system void $mem_assign_from($state s, $mem m)`
|
|---|
| 206 | * deprecated
|
|---|
| 207 |
|
|---|
| 208 | ## op {#op}
|
|---|
| 209 |
|
|---|
| 210 | Header: [op.h](https://github.com/verified-software-lab/civl/blob/main/mods/dev.civl.abc/src/dev/civl/abc/include/op.h).
|
|---|
| 211 | Uses: (nothing).
|
|---|
| 212 |
|
|---|
| 213 | Defines an enumerated type `$operation` with the following values:
|
|---|
| 214 |
|
|---|
| 215 | | Constant | Description |
|
|---|
| 216 | |-----------|------------------------|
|
|---|
| 217 | | `_NO_OP` | no operation |
|
|---|
| 218 | | `_MAX` | maximum |
|
|---|
| 219 | | `_MIN` | minimum |
|
|---|
| 220 | | `_SUM` | sum |
|
|---|
| 221 | | `_PROD` | product |
|
|---|
| 222 | | `_LAND` | logical and |
|
|---|
| 223 | | `_BAND` | bit-wise and |
|
|---|
| 224 | | `_LOR` | logical or |
|
|---|
| 225 | | `_BOR` | bit-wise or |
|
|---|
| 226 | | `_LXOR` | logical exclusive or |
|
|---|
| 227 | | `_BXOR` | bit-wise exclusive or |
|
|---|
| 228 | | `_MINLOC` | min value and location |
|
|---|
| 229 | | `_MAXLOC` | max value and location |
|
|---|
| 230 | | `_EQ` | equal to |
|
|---|
| 231 | | `_NEQ` | not Equal to |
|
|---|
| 232 |
|
|---|
| 233 | ## pointer {#pointer}
|
|---|
| 234 |
|
|---|
| 235 | Header: [pointer.cvh](https://github.com/verified-software-lab/civl/blob/main/mods/dev.civl.abc/src/dev/civl/abc/include/pointer.cvh).
|
|---|
| 236 | Uses: [op](#op).
|
|---|
| 237 |
|
|---|
| 238 | * `$system void $set_default(void *obj);`
|
|---|
| 239 | * Updates the leaf nodes of a status variable to the default value 0
|
|---|
| 240 | * `$system void $apply(void *obj1, $operation op, void *obj2, void *result);`
|
|---|
| 241 | * Applies the operation op on `obj1` and `obj2` and stores the result
|
|---|
| 242 | * `$system _Bool $equals(void *x, void *y);`
|
|---|
| 243 | * Are the object pointed to equal?
|
|---|
| 244 | * `$system void $assert_equals(void *x, void *y, ...);`
|
|---|
| 245 | * Assert that the two objects pointed are equal
|
|---|
| 246 | * `$system _Bool $contains(void *obj1, void *obj2);`
|
|---|
| 247 | * Semantics: Does the object pointed to by `obj1` contain that pointed to by `obj1`?
|
|---|
| 248 | * `$system void * $translate_ptr(void *ptr, void *obj);`
|
|---|
| 249 | * Translates a pointer into one object to a pointer into a different object with similar structure.
|
|---|
| 250 | * `$system void $copy(void *ptr, void *value);`
|
|---|
| 251 | * Copies the value pointed to by the right operand to the memory location specified by the left operand
|
|---|
| 252 | * `$system void $leaf_node_ptrs(void *array, void *obj);`
|
|---|
| 253 | * copy the references to the leaf nodes of obj to the given array obj: pointer to type T' whose leaf node types are all type T array: pointer to array of pointer to type T
|
|---|
| 254 | * `$system _Bool $is_identity_ref(void *obj);`
|
|---|
| 255 | * returns true if the given pointer is referencing to an object by identity reference
|
|---|
| 256 | * `$system void $set_leaf_nodes(void *obj, int value);`
|
|---|
| 257 | * updates the leaf nodes of the given objects to with the given integer value
|
|---|
| 258 | * `$system _Bool $leaf_nodes_equal_to(void *obj, int value);`
|
|---|
| 259 | * returns true iff all leaf nodes of the given object equal to the given value
|
|---|
| 260 | * `$system _Bool $has_leaf_node_equal_to(void *obj, int value);`
|
|---|
| 261 | * returns true iff at least one leaf nodes of the given object equal to the given value
|
|---|
| 262 | * `$system _Bool $is_derefable_pointer(void *ptr);`
|
|---|
| 263 | * can the given pointer be safely referenced? A derefable pointer is not NULL and is referring to a memory location of some dyscope.
|
|---|
| 264 | * `$system void * $pointer_add(const void *ptr, int offset, int type_size);`
|
|---|
| 265 | * Gives a pointer addition operation. Note that the input pointer will always be casted to the form of a pointer to a primitive data type.
|
|---|
| 266 |
|
|---|
| 267 | ## scope {#scope}
|
|---|
| 268 |
|
|---|
| 269 | Header: [scope.cvh](https://github.com/verified-software-lab/civl/blob/main/mods/dev.civl.abc/src/dev/civl/abc/include/scope.cvh).
|
|---|
| 270 | Uses: (nothing).
|
|---|
| 271 |
|
|---|
| 272 |
|
|---|
| 273 |
|
|---|
| 274 | ## seq {#seq}
|
|---|
| 275 |
|
|---|
| 276 | Header: [seq.cvh](https://github.com/verified-software-lab/civl/blob/main/mods/dev.civl.abc/src/dev/civl/abc/include/seq.cvh).
|
|---|
| 277 | Uses: (nothing).
|
|---|
| 278 |
|
|---|
| 279 |
|
|---|
| 280 |
|
|---|
| 281 | ## C Standard library
|
|---|
| 282 |
|
|---|
| 283 | ### stdlib
|
|---|
| 284 |
|
|---|
| 285 | ### stdio
|
|---|
| 286 |
|
|---|
| 287 | ### string
|
|---|
| 288 |
|
|---|
