Idea

New data structures are needed in CIVL-C in order to model what happens in OpenMP and other complex APIs. Sequences, sets, and maps, specifically. The purpose of this page is to propose the new interface for these structures.

Typeof

First we need a new expression $typeof. This expression has the syntax $typeof(typename). It is just like sizeof syntactically. It represents any type as a value. The type of the $typeof expression is the type $type. This is also represented in the CIVL model layer as "dynamic type".

Immutable Version

Sequences

This is an abstract datatype for an immutable (functional) sequence of elements of the same type.

New type: $seq. Functions:

/* Returns the empty seq whose elements (if it had any)
 * would have the given type.  The type becomes associated
 * with the seq.  */
$seq $seq_empty($type type);

/* Returns the sequence formed by reading n consecutive elements
 * from memory.  The parameter ptr points to the first such element,
 * and type is the type of each element.
 */
$seq $seq_from_array($type type, void * ptr, int n);

/* Returns the type of an element that goes in this seq */
$type $seq_get_element_type($seq seq);

/* Returns the seq that is like the given one but with one more
 * element added.  A runtime exception is generated if the thing pointed
 * to by eltptr doesn't have the right type for the seq. */
$seq $seq_add($seq seq, void * eltptr);

/* Returns the seq that is like the given one but with the element
 * at position index removed and the subsequent elements shifted down */
$seq $seq_remove($seq seq, int index);

/* Returns the seq that is like the given one but with the element
 * at position index replaced with whatever object is pointed to by
 * ptr. */
$seq $seq_set($seq seq, int index, void * ptr);

/* Returns the length of the seq (i.e., the number of elements) */
int $seq_get_length($seq seq);

/* Returns the seq that is like the given one but with an element
 * inserted at position i (and the subsequent elements shifted up).
 * The parameter eltptr is a pointer to the element to insert. */
$seq $seq_insert($seq seq, int index, void * eltptr);

/* Gets the element at position index and stores it in wherever
 * ptr points to. */
void $seq_get($seq seq, int index, void * ptr);

/* Returns the subsequence consisting of elements at index i, for
 * start<=i<stop. */
$seq $seq_subseq($seq seq, int start, int stop);

/* Returns the concatenation of the two sequences */
$seq $seq_concat($seq s1, $seq s2);

Sets

Should we make it an ordered set, $oset?

New type: $set. Functions:

/* Returns the empty set whose elements (if it had any)
 * would have the given type.  The type becomes associated
 * with the set.  */
$set $set_empty($type type);

/* Returns the cardinality of the set */
int $set_get_size($set set);

/* Returns the type of an element that goes in this set */
$type $set_get_element_type($set set);

/* Returns the set that is like the given one but with one more
 * element added.  A runtime exception is generated if the thing pointed
 * to by eltptr doesn't have the right type for s. */
$set $set_add($set set, void * eltptr);

/* Returns the set that is like the given one but with the specified element
 * removed.  If the set does not contain the element the set returned
 * will equal the given one. */
$set $set_remove($set set, void * eltptr);

/* Does the set contain the specified element? */
_Bool $set_contains($set set, void * eltptr);

$set $set_union($set s1, $set s2);

$set $set_intersection($set s1, $set s2);

$set $set_difference($set s1, $set s2);

/* Returns the singleton set consisting of the single element
 * specified by the pointer and the type */
$set $set_single($type type, void * eltptr);

/* Returns a sequence consisting of the elements of the set */
$seq $set_to_seq($set set);

Maps

$map

/* Returns the empty map with the given key type and
 * value type.
 */
$map $map_empty($type keyType, $type valType);

/* Returns the map obtained by starting with the given
 * map, removing the entry with the specified key (if
 * one exists) and then adding the specified key-value
 * pair.  If that key-value pair already exists in the given map,
 * the map returned is identical to the given on.
 */
$map $map_put($map map, void * keyPtr, void * valPtr);

/* If an entry with the specified key exists in the map, it
 * the corresponding value is copied into the region specified
 * by the resultPtr.  Otherwise, a no-op.
 */
void $map_get($map map, void * keyPtr, void * resultPtr);

/* Returns the map obtained by removing an entry
 * with the specified key, if one exists.
 */
$map $map_removeKey($map map, void * keyPtr);

/* Returns the set of keys in the given map. */
$set $map_get_keySet($map map);

/* Returns the set of ordered pairs of the form (key,val).
 * Each ordered pair has a struct type consisting of two fields
 * named key and val.  The type of the key field is the keyType;
 * the type of the val field is the valType.
 */
$set $map_get_entrySet($map map);

Mutable Version

Sequences

This is an abstract datatype for a mutable sequence of elements of the same type.

New type: $mseq. Functions:

/* Creates a new mutable sequence allocated in the given
 * scope's heap.  The type of the elements that this sequence
 * can hold is specified.  The sequence is initially empty.
 * A handle to the new sequence is returned.
 */
$mseq $mseq_create($scope scope, $type type);

/* Forms a new mutable sequence by copying the data from an 
 * existing sequence of values.  The parameter ptr points to the
 * element in the existing sequence of adjacent values in memory.
 * The number of elements is n, and the type of each element is type.
 * The new sequence is allocated in the heap of the specified scope.
 * A handle to the new sequence is returned.
 */
$mseq $mseq_create_from_array($scope scope, $type type, void * ptr, int n);

/* Creates a new mutable sequence by copying a subsequence
 * of data from an existing mutable sequence.  The elements
 * at indexes start, state+1, ..., stop-1 are copied from the original
 * to create the new sequence, where they will have indexes 0, 1, ...,
 * stop-start-1.  The length of the new sequence will be stop-start,
 * unless stop-start is negative, in which case the length will be 0.
 */
$mseq $mseq_create_subseq($scope scope, $mseq original, int start int stop);

/* Destroys the mseq specified by the given handle.
 * All memory associated with the mseq is deallocated.
 * The handle then becomes an undefined value.
 * The sequence does not have to be empty when this is called.
 */
void $mseq_destroy($mseq mseq);

/* Returns the type of an element that goes in this seq */
$type $mseq_get_element_type($mseq mseq);

/* Adds the specified element to the mseq.
 * A runtime exception is generated if the thing pointed
 * to by eltptr doesn't have the right type for the mseq.
 */
void $mseq_add($mseq mseq, void * eltptr);

/* Removes the element at position index from the mseq
 * and shifts the subsequence elements down.
 * If result is not NULL, the value removed is written to the memory
 * pointed to by result.  If the result is NULL, this is not done.
 */
void $mseq_remove($mseq mseq, int index, void * result);

/* Replaces the element at position index with whatever
 * object is pointed to by ptr. 
 * If old is not NULL, the old entry at index is copied to the
 * memory specified by old.  If old is NULL, this is not done.
 */
void $mseq_set($mseq mseq, int index, void * ptr, void * old);

/* Returns the length of the mseq (i.e., the number of elements) */
int $mseq_get_length($mseq mseq);

/* Inserts the specified element at the given index.
 * Subsequent elements are shifted up.n
 * The parameter eltptr is a pointer to the element to insert. */
void $mseq_insert($mseq mseq, int index, void * eltptr);

/* Gets the element at position index and stores it in wherever
 * ptr points to. */
void $mseq_get($mseq mseq, int index, void * ptr);

/* Adds all the elements of s2 to s1.  The
 * elements from s2 are copied and appended to the
 * end of s1.  The sequence s2 itself is not modified.
 */
$mseq $mseq_append($mseq s1, $mseq s2);

Sets

New type: $set. Functions:

/* Returns the empty set whose elements (if it had any)
 * would have the given type.  The type becomes associated
 * with the set.  */
$set $set_empty($type type);

/* Returns the cardinality of the set */
int $set_get_size($set set);

/* Returns the type of an element that goes in this set */
$type $set_get_element_type($set set);

/* Returns the set that is like the given one but with one more
 * element added.  A runtime exception is generated if the thing pointed
 * to by eltptr doesn't have the right type for s. */
$set $set_add($set set, void * eltptr);

/* Returns the set that is like the given one but with the specified element
 * removed.  If the set does not contain the element the set returned
 * will equal the given one. */
$set $set_remove($set set, void * eltptr);

/* Does the set contain the specified element? */
_Bool $set_contains($set set, void * eltptr);

$set $set_union($set s1, $set s2);

$set $set_intersection($set s1, $set s2);

$set $set_difference($set s1, $set s2);

/* Returns the singleton set consisting of the single element
 * specified by the pointer and the type */
$set $set_single($type type, void * eltptr);

/* Returns a sequence consisting of the elements of the set */
$seq $set_to_seq($set set);

Maps

$map

/* Returns the empty map with the given key type and
 * value type.
 */
$map $map_empty($type keyType, $type valType);

/* Returns the map obtained by starting with the given
 * map, removing the entry with the specified key (if
 * one exists) and then adding the specified key-value
 * pair.  If that key-value pair already exists in the given map,
 * the map returned is identical to the given on.
 */
$map $map_put($map map, void * keyPtr, void * valPtr);

/* If an entry with the specified key exists in the map, it
 * the corresponding value is copied into the region specified
 * by the resultPtr.  Otherwise, a no-op.
 */
void $map_get($map map, void * keyPtr, void * resultPtr);

/* Returns the map obtained by removing an entry
 * with the specified key, if one exists.
 */
$map $map_removeKey($map map, void * keyPtr);

/* Returns the set of keys in the given map. */
$set $map_get_keySet($map map);

/* Returns the set of ordered pairs of the form (key,val).
 * Each ordered pair has a struct type consisting of two fields
 * named key and val.  The type of the key field is the keyType;
 * the type of the val field is the valType.
 */
$set $map_get_entrySet($map map);