• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
          • Syntax-for-tools
          • Atc
          • Language
          • Representation
            • Representation-of-integer-operations
            • Atc-arrays
              • Atc-def-integer-arrays
              • Ushort-array-write
              • Ushort-array-integer-write
              • Ulong-array-integer-write
              • Ullong-array-write
              • Ullong-array-integer-write
              • Uchar-array-integer-write
              • Sshort-array-write
              • Sshort-array-integer-write
              • Slong-array-integer-write
              • Sllong-array-write
              • Sllong-array-integer-write
              • Schar-array-integer-write
              • Ulong-array-write
              • Uchar-array-write
              • Slong-array-write
              • Schar-array-write
              • Uint-array-write
              • Uint-array-integer-write
              • Sint-array-write
              • Sint-array-integer-write
              • Ushort-array
              • Ullong-array
              • Sshort-array
              • Sllong-array
              • Ulong-array
              • Uint-array
              • Uchar-array
              • Slong-array
              • Sint-array
              • Schar-array
              • Ushort-array-integer-read
              • Ushort-array-integer-index-okp
              • Ullong-array-integer-read
              • Ullong-array-integer-index-okp
              • Sshort-array-integer-read
              • Sshort-array-integer-index-okp
              • Sllong-array-integer-read
              • Sllong-array-integer-index-okp
              • Ulong-array-integer-read
              • Ulong-array-integer-index-okp
              • Ullong-array-read
              • Uint-array-integer-read
              • Uint-array-integer-index-okp
              • Uchar-array-integer-read
              • Uchar-array-integer-index-okp
              • Slong-array-integer-read
              • Slong-array-integer-index-okp
              • Sllong-array-read
              • Sint-array-integer-read
              • Sint-array-integer-index-okp
              • Schar-array-integer-read
              • Schar-array-integer-index-okp
              • Ushort-array-read
              • Ushort-array-index-okp
              • Ulong-array-read
              • Ulong-array-index-okp
              • Ullong-array-index-okp
              • Uint-array-read
              • Uchar-array-read
              • Uchar-array-index-okp
              • Sshort-array-read
              • Sshort-array-index-okp
              • Slong-array-read
              • Slong-array-index-okp
              • Sllong-array-index-okp
              • Sint-array-read
              • Schar-array-read
              • Schar-array-index-okp
              • Uint-array-index-okp
              • Sint-array-index-okp
              • Ushort-array-of
              • Ullong-array-of
              • Uchar-array-length
              • Sshort-array-of
              • Sllong-array-of
              • Ulong-array-of
              • Uint-array-of
              • Uchar-array-of
              • Slong-array-of
              • Sint-array-of
              • Schar-array-of
              • Ushort-array-length
              • Ulong-array-length
              • Ullong-array-length
              • Sshort-array-length
              • Sllong-array-length
              • Uint-array-length
              • Slong-array-length
              • Sint-array-length
              • Schar-array-length
              • Atc-def-integer-arrays-loop
            • Representation-of-integers
            • Representation-of-integer-conversions
            • Pointed-integers
            • Shallow-deep-embedding-relation
          • Transformation-tools
          • Insertion-sort
          • Pack
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Representation

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. [C17:6.5.2.1/2] explains that array indexing a[i] boils down to addition between the pointer a and the integer i, and [C17: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.

[C17: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. [C17] 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.