Representation-of-integers
A representation of C integers in ACL2.
This is part of the shallow embedding.
We define a representation of
the C standard signed and unsigned integer values,
except _Bool for now,
based on their format definitions and range definitions. As mentioned in the documentation of the integer formats,
the definitions of values we give here
should still work if the format definitions are changed.
For each C integer type covered by our representation,
we define the C values as wrappers of ACL2 integers in appropriate ranges.
We also define lists of these C values,
and some operations between these lists
and lists of ACL2 integers in the corresponding ranges.
For the unsigned types,
we also introduce ACL2 functions
to turn ACL2 integers into values of those types
by reducing them modulo one plus the maximum value of the type.
These functions are used
to define certain C integer conversions and operations,
which are modular for unsigned integer types.
This representation of C integers in ACL2 should be treated like
abstract data types whose definition is opaque.
Consider the representation of unsigned char, for instance.
The exact definition of ucharp does not matter.
What matters is that the set of ACL2 values that satisfy that predicate
is isomorphic to the set of ACL2 integers
that satisfy uchar-integerp;
the isomorphisms between the two sets are
integer-from-uchar and uchar-from-integer.
The fixer uchar-fix should be treated opaquely too.
There should be sufficient theorems
that capture the isomorphism property
and that support reasoning about these C integers in ACL2
independently from their representation.
On the other hand, uchar-integerp is not opaque:
it is a known set of ACL2 integers, and that matters for reasoning.
As a practical issue, uchar-integerp-alt-def,
which as the name suggests is like an alternative definition,
is generally more convenient than the actual definition,
because the latter involves powers of two and bit sizes,
while the alternate definition involves minima and maxima.
As another practical issue, it is generally unnecessary
to enable the fixer uchar-integer-fix,
which exposes uchar-integerp,
which therefore needs to be enabled anyways;
there is a theorem that simplifies away uchar-integer-fix
when uchar-integerp holds,
so enabling uchar-integerp-alt-def should normally suffice.
Even with the aforementioned isomorphisms disabled,
their executable counterparts are enabled (per ACL2's defaults),
exposing the internal representation in some constant cases;
we may consider keeping those executable counterparts disabled too.
Subtopics
- Def-integer-values
- Event to generate the model of the values of a C integer type.
- Ushort-list-from-integer-list
- Lift ushort to lists.
- Ullong-list-from-integer-list
- Lift ullong to lists.
- Sshort-list-from-integer-list
- Lift sshort to lists.
- Sllong-list-from-integer-list
- Lift sllong to lists.
- Integer-list-from-ushort-list
- Lift integer-from-ushort to lists.
- Integer-list-from-ullong-list
- Lift integer-from-ullong to lists.
- Integer-list-from-sshort-list
- Lift integer-from-sshort to lists.
- Integer-list-from-sllong-list
- Lift integer-from-sllong to lists.
- Ulong-list-from-integer-list
- Lift ulong to lists.
- Uchar-list-from-integer-list
- Lift uchar to lists.
- Slong-list-from-integer-list
- Lift slong to lists.
- Schar-list-from-integer-list
- Lift schar to lists.
- Integer-list-from-ulong-list
- Lift integer-from-ulong to lists.
- Integer-list-from-uchar-list
- Lift integer-from-uchar to lists.
- Integer-list-from-slong-list
- Lift integer-from-slong to lists.
- Integer-list-from-schar-list
- Lift integer-from-schar to lists.
- Uint-list-from-integer-list
- Lift uint to lists.
- Sint-list-from-integer-list
- Lift sint to lists.
- Integer-list-from-uint-list
- Lift integer-from-uint to lists.
- Integer-list-from-sint-list
- Lift integer-from-sint to lists.
- Cinteger
- Fixtype of all the supported C integer types.
- Ullongp
- Recognizer of values of type unsigned long long.
- Ucharp
- Recognizer of values of type unsigned char.
- Sintp
- Recognizer of values of type signed int.
- Ushortp
- Recognizer of values of type unsigned short.
- Ulongp
- Recognizer of values of type unsigned long.
- Uintp
- Recognizer of values of type unsigned int.
- Sllongp
- Recognizer of values of type signed long long.
- Slongp
- Recognizer of values of type signed long.
- Sshortp
- Recognizer of values of type signed short.
- Scharp
- Recognizer of values of type signed char.
- Integer-from-sshort
- Accessor for values of type signed short.
- Integer-from-sllong
- Accessor for values of type signed long long.
- Integer-from-sint
- Accessor for values of type signed int.
- Integer-from-slong
- Accessor for values of type signed long.
- Integer-from-schar
- Accessor for values of type signed char.
- Integer-type-to-fixtype
- Name of the fixtype of the values of a C integer type.
- Integer-from-ushort
- Accessor for values of type unsigned short.
- Integer-from-ullong
- Accessor for values of type unsigned long long.
- Integer-from-uchar
- Accessor for values of type unsigned char.
- Integer-from-cinteger
- ACL2 integer corresponding to the C integer.
- Integer-from-ulong
- Accessor for values of type unsigned long.
- Integer-from-uint
- Accessor for values of type unsigned int.
- Def-integer-values-loop
- Events to generate the models of the values of some C integer types.
- Sint-from-integer
- Constructor for values of type signed int.
- Sint
- Fixtype of values of type signed int.
- Fixtype-to-integer-type
- Integer type corresponding to a fixtype name, if any.
- Uchar-from-integer
- Constructor for values of type unsigned char.
- Ushort-from-integer-mod
- Reduce modularly ACL2 integers to values of type unsigned short.
- Ushort-from-integer
- Constructor for values of type unsigned short.
- Ulong-from-integer-mod
- Reduce modularly ACL2 integers to values of type unsigned long.
- Ulong-from-integer
- Constructor for values of type unsigned long.
- Ullong-from-integer-mod
- Reduce modularly ACL2 integers to values of type unsigned long long.
- Ullong-from-integer
- Constructor for values of type unsigned long long.
- Uchar-from-integer-mod
- Reduce modularly ACL2 integers to values of type unsigned char.
- Sshort-from-integer
- Constructor for values of type signed short.
- Slong-from-integer
- Constructor for values of type signed long.
- Sllong-from-integer
- Constructor for values of type signed long long.
- Schar-from-integer
- Constructor for values of type signed char.
- Uint-from-integer-mod
- Reduce modularly ACL2 integers to values of type unsigned int.
- Uint-from-integer
- Constructor for values of type unsigned int.
- Uchar
- Fixtype of values of type unsigned char.
- Schar
- Fixtype of values of type signed char.
- Ushort
- Fixtype of values of type unsigned short.
- Ulong
- Fixtype of values of type unsigned long.
- Ullong
- Fixtype of values of type unsigned long long.
- Sshort
- Fixtype of values of type signed short.
- Slong
- Fixtype of values of type signed long.
- Sllong
- Fixtype of values of type signed long long.
- Ullong-fix
- Fixer for values of type unsigned long long.
- Uint
- Fixtype of values of type unsigned int.
- Uchar-fix
- Fixer for values of type unsigned char.
- Sint-fix
- Fixer for values of type signed int.
- Ushort-fix
- Fixer for values of type unsigned short.
- Ulong-fix
- Fixer for values of type unsigned long.
- Uint-fix
- Fixer for values of type unsigned int.
- Sshort-fix
- Fixer for values of type signed short.
- Slong-fix
- Fixer for values of type signed long.
- Sllong-fix
- Fixer for values of type signed long long.
- Schar-fix
- Fixer for values of type signed char.
- Ushort-list
- Fixtype of lists of values of type unsigned short.
- Ulong-list
- Fixtype of lists of values of type unsigned long.
- Ullong-list
- Fixtype of lists of values of type unsigned long long.
- Uint-list
- Fixtype of lists of values of type unsigned int.
- Uchar-list
- Fixtype of lists of values of type unsigned char.
- Sshort-list
- Fixtype of lists of values of type signed short.
- Slong-list
- Fixtype of lists of values of type signed long.
- Sllong-list
- Fixtype of lists of values of type signed long long.
- Sint-list
- Fixtype of lists of values of type signed int.
- Schar-list
- Fixtype of lists of values of type signed char.
- Integer-type-to/from-fixtype-theorems
- Inversion theorems about the mappings between
integer types and fixtype symbols.
- *nonchar-integer-fixtypes*
- List of the fixtype names of
the (supported) C integer types except plain char.
