Atc-arrays
A model of shallowly embedded C arrays for ATC.
We represent arrays as
sequences of values that can be read and written.
These array representations can be passed around, and manipulated by,
ACL2 functions that represent C functions,
and ATC translates those to corresponding array manipulations.
We represent arrays as values of fixtypes that wrap lists of C values.
We provide operations to read and write elements,
essentially wrappers of nth and update-nth.
Besides the list of C values,
each array fixtype includes the type of the element.
This is redundant information,
but it is needed so that arrays thus modeled
are a subset of the values in the C deep embedding.
This fairly simple model should suffice to generate C code
that manipulates arrays in some interesting ways.
The model should suffice to represent C functions
that receive arrays from external callers,
and possibly update them.
However, we may need to extend the model in the future;
in particular, we may provide operations to create arrays.
This array model is similar to ATJ's model of Java primitive arrays. But C arrays differ from Java arrays:
in particular, Java arrays are self-contained objects,
whose length and other attributes can be programmatically queried;
in contrast, C arrays are a ``view'' of certain memory regions.
Nonetheless, at the level of ACL2 manipulations,
the two kinds of arrays differ less (at least for certain mundane uses),
because, even though C does not provide ``direct access'' to
an array's length and other attributes,
there is nonetheless an implicit notion of array,
with its length and other attributes,
that is conceptually created and passed around and manipulated.
Similarly to the use of the Java array model in ATJ,
the C arrays modeled here have to be treated in a stobj-like manner
by the ACL2 functions to be translated to C by ATC.
In general, each of these ACL2 functions
takes zero or more arrays as inputs (possibly among other inputs),
and must return, in an mv,
all the arrays that it possibly modifies,
along with the regular return result of the function (if any);
the arrays that are only read by the function do not have to be returned.
Inside the function, the arrays must be updated (if at all)
in a single-threaded way, analogously to stobjs.
ATC ensures that this discipline is followed, analogously to ATJ.
Our model of arrays assumes that different arrays do not overlap.
That is,
either two arrays are the same array (when they have the same pointer),
or they are completely disjoint.
The model does not capture
the situation of an array being a subarray of another one.
We may extend the model in the future.
We provide a model of arrays of all the integer types
supported in ATC's model of C,
i.e. arrays of unsigned charss, arrays of ints, etc.
[C:6.5.2.1/2] explains that array indexing a[i] boils down to
addition between the pointer a and the integer i,
and [C:6.5.6/2] allows the integer to have any integer type.
This means that, for each possible array type,
any integer type is allowed as index.
We define operations that take indices of type cinteger,
one operation per element array type;
note that the type of the index does not affect the result,
so having operations that take indices of all C integer types
does not require a weakening or complication of the return types.
We also have operations that take specific integer types as indices;
these will be removed, using instead the aforementioned ones
that take indices of any C integer types.
We also have operations that take ACL2 integers as indices,
in terms of which the ones that take specific integer types are defined;
the ones that take ACL2 integers will be also removed.
Since all these functions follow a common pattern,
we generate array types and functions programmatically,
as done for the integers.
[C:6.2.5/20] requires arrays to be non-empty,
i.e. to contain at least one element,
i.e. to have positive length.
As noted above, arrays are indexed via integers.
[C] only provides minimum requirements for the sizes of integer types,
not maximum requirements:
other than practical considerations,
nothing, mathematically, prevents some integer types
to consists of thousands or millions of bits.
So our model of arrays requires them to be non-empty
but puts no maximum limits on their length.
For each integer type <type>,
besides the fixtype of arrays of that type,
we generate functions
<type>-array-read and <type>-array-write
that take C integers as indices.
We also generate convenience functions
to test whether indices are in range
and to return the length of the arrays:
these do not represent C constructs,
but are useful in guards for example.
Subtopics
- Atc-def-integer-arrays
- Event to generate the model of arrays of an integer type.
- Ushort-array-write
- Write an element to an array of type unsigned short, using a c integer index.
- Ushort-array-integer-write
- Write an element to an array of type unsigned short, using an ACL2 integer index.
- Ulong-array-integer-write
- Write an element to an array of type unsigned long, using an ACL2 integer index.
- Ullong-array-write
- Write an element to an array of type unsigned long long, using a c integer index.
- Ullong-array-integer-write
- Write an element to an array of type unsigned long long, using an ACL2 integer index.
- Uchar-array-integer-write
- Write an element to an array of type unsigned char, using an ACL2 integer index.
- Sshort-array-write
- Write an element to an array of type signed short, using a c integer index.
- Sshort-array-integer-write
- Write an element to an array of type signed short, using an ACL2 integer index.
- Slong-array-integer-write
- Write an element to an array of type signed long, using an ACL2 integer index.
- Sllong-array-write
- Write an element to an array of type signed long long, using a c integer index.
- Sllong-array-integer-write
- Write an element to an array of type signed long long, using an ACL2 integer index.
- Schar-array-integer-write
- Write an element to an array of type signed char, using an ACL2 integer index.
- Ulong-array-write
- Write an element to an array of type unsigned long, using a c integer index.
- Uchar-array-write
- Write an element to an array of type unsigned char, using a c integer index.
- Slong-array-write
- Write an element to an array of type signed long, using a c integer index.
- Schar-array-write
- Write an element to an array of type signed char, using a c integer index.
- Uint-array-write
- Write an element to an array of type unsigned int, using a c integer index.
- Uint-array-integer-write
- Write an element to an array of type unsigned int, using an ACL2 integer index.
- Sint-array-write
- Write an element to an array of type signed int, using a c integer index.
- Sint-array-integer-write
- Write an element to an array of type signed int, using an ACL2 integer index.
- Ushort-array
- Fixtype of (ATC's model of) arrays of type unsigned short.
- Ullong-array
- Fixtype of (ATC's model of) arrays of type unsigned long long.
- Sshort-array
- Fixtype of (ATC's model of) arrays of type signed short.
- Sllong-array
- Fixtype of (ATC's model of) arrays of type signed long long.
- Ulong-array
- Fixtype of (ATC's model of) arrays of type unsigned long.
- Uint-array
- Fixtype of (ATC's model of) arrays of type unsigned int.
- Uchar-array
- Fixtype of (ATC's model of) arrays of type unsigned char.
- Slong-array
- Fixtype of (ATC's model of) arrays of type signed long.
- Sint-array
- Fixtype of (ATC's model of) arrays of type signed int.
- Schar-array
- Fixtype of (ATC's model of) arrays of type signed char.
- Ushort-array-integer-read
- Read an element from an array of type unsigned short, using an ACL2 integer index.
- Ushort-array-integer-index-okp
- Check if an ACL2 integer is
a valid index (i.e. in range)
for an array of type unsigned short.
- Ullong-array-integer-read
- Read an element from an array of type unsigned long long, using an ACL2 integer index.
- Ullong-array-integer-index-okp
- Check if an ACL2 integer is
a valid index (i.e. in range)
for an array of type unsigned long long.
- Sshort-array-integer-read
- Read an element from an array of type signed short, using an ACL2 integer index.
- Sshort-array-integer-index-okp
- Check if an ACL2 integer is
a valid index (i.e. in range)
for an array of type signed short.
- Sllong-array-integer-read
- Read an element from an array of type signed long long, using an ACL2 integer index.
- Sllong-array-integer-index-okp
- Check if an ACL2 integer is
a valid index (i.e. in range)
for an array of type signed long long.
- Ulong-array-integer-read
- Read an element from an array of type unsigned long, using an ACL2 integer index.
- Ulong-array-integer-index-okp
- Check if an ACL2 integer is
a valid index (i.e. in range)
for an array of type unsigned long.
- Ullong-array-read
- Read an element from an array of type unsigned long long, using a C integer index.
- Uint-array-integer-read
- Read an element from an array of type unsigned int, using an ACL2 integer index.
- Uint-array-integer-index-okp
- Check if an ACL2 integer is
a valid index (i.e. in range)
for an array of type unsigned int.
- Uchar-array-integer-read
- Read an element from an array of type unsigned char, using an ACL2 integer index.
- Uchar-array-integer-index-okp
- Check if an ACL2 integer is
a valid index (i.e. in range)
for an array of type unsigned char.
- Slong-array-integer-read
- Read an element from an array of type signed long, using an ACL2 integer index.
- Slong-array-integer-index-okp
- Check if an ACL2 integer is
a valid index (i.e. in range)
for an array of type signed long.
- Sllong-array-read
- Read an element from an array of type signed long long, using a C integer index.
- Sint-array-integer-read
- Read an element from an array of type signed int, using an ACL2 integer index.
- Sint-array-integer-index-okp
- Check if an ACL2 integer is
a valid index (i.e. in range)
for an array of type signed int.
- Schar-array-integer-read
- Read an element from an array of type signed char, using an ACL2 integer index.
- Schar-array-integer-index-okp
- Check if an ACL2 integer is
a valid index (i.e. in range)
for an array of type signed char.
- Ushort-array-read
- Read an element from an array of type unsigned short, using a C integer index.
- Ushort-array-index-okp
- Check if a C integer is
a valid index (i.e. in range)
for an array of type unsigned short.
- Ulong-array-read
- Read an element from an array of type unsigned long, using a C integer index.
- Ulong-array-index-okp
- Check if a C integer is
a valid index (i.e. in range)
for an array of type unsigned long.
- Ullong-array-index-okp
- Check if a C integer is
a valid index (i.e. in range)
for an array of type unsigned long long.
- Uint-array-read
- Read an element from an array of type unsigned int, using a C integer index.
- Uchar-array-read
- Read an element from an array of type unsigned char, using a C integer index.
- Uchar-array-index-okp
- Check if a C integer is
a valid index (i.e. in range)
for an array of type unsigned char.
- Sshort-array-read
- Read an element from an array of type signed short, using a C integer index.
- Sshort-array-index-okp
- Check if a C integer is
a valid index (i.e. in range)
for an array of type signed short.
- Slong-array-read
- Read an element from an array of type signed long, using a C integer index.
- Slong-array-index-okp
- Check if a C integer is
a valid index (i.e. in range)
for an array of type signed long.
- Sllong-array-index-okp
- Check if a C integer is
a valid index (i.e. in range)
for an array of type signed long long.
- Sint-array-read
- Read an element from an array of type signed int, using a C integer index.
- Schar-array-read
- Read an element from an array of type signed char, using a C integer index.
- Schar-array-index-okp
- Check if a C integer is
a valid index (i.e. in range)
for an array of type signed char.
- Uint-array-index-okp
- Check if a C integer is
a valid index (i.e. in range)
for an array of type unsigned int.
- Sint-array-index-okp
- Check if a C integer is
a valid index (i.e. in range)
for an array of type signed int.
- Ushort-array-of
- Build an array of type unsigned shortfrom a list of its elements.
- Ullong-array-of
- Build an array of type unsigned long longfrom a list of its elements.
- Uchar-array-length
- Length of an array of type unsigned char.
- Sshort-array-of
- Build an array of type signed shortfrom a list of its elements.
- Sllong-array-of
- Build an array of type signed long longfrom a list of its elements.
- Ulong-array-of
- Build an array of type unsigned longfrom a list of its elements.
- Uint-array-of
- Build an array of type unsigned intfrom a list of its elements.
- Uchar-array-of
- Build an array of type unsigned charfrom a list of its elements.
- Slong-array-of
- Build an array of type signed longfrom a list of its elements.
- Sint-array-of
- Build an array of type signed intfrom a list of its elements.
- Schar-array-of
- Build an array of type signed charfrom a list of its elements.
- Ushort-array-length
- Length of an array of type unsigned short.
- Ulong-array-length
- Length of an array of type unsigned long.
- Ullong-array-length
- Length of an array of type unsigned long long.
- Sshort-array-length
- Length of an array of type signed short.
- Sllong-array-length
- Length of an array of type signed long long.
- Uint-array-length
- Length of an array of type unsigned int.
- Slong-array-length
- Length of an array of type signed long.
- Sint-array-length
- Length of an array of type signed int.
- Schar-array-length
- Length of an array of type signed char.
- Atc-def-integer-arrays-loop
- Events to generate the model of arrays
for the given array element types.
