Implementation-environments
Implementation environments for C.
Some aspects of the syntax and semantics of C are implementation-dependent.
[C17:5] introduces the notion of translation and execution environments,
which specify those aspects.
In our formalization, we introduce a notion of implementation environment,
which puts together the translation and execution environments in [C17].
That is, an implementation environment
specifies the implementation-dependent aspects of C.
We prefer to formalize one (implementation) environment,
instead of two (translation and execution) environments,
because the latter two share several aspects (e.g. integer sizes),
and therefore it seems simpler to have one notion.
We start by capturing some aspects of the C implementation environment.
More will be added in the future.
Initially, our formalization of implementation environments
is not used in other parts of the C formalization;
furthermore, it captures notions already captured elsewhere,
such as the integer formats. But we plan to update the rest of the formalization to use this,
also removing those then-redundant parts.
Subtopics
- Uinteger-bit-roles-for-sinteger-bit-roles
- Create the simplest list of unsigned bit roles
consistent with a given list of signed bit roles.
- Sinteger-bit-roles-for-uinteger-bit-roles
- Create the simplest list of signed bit roles
consistent with a given list of unsigned bit roles.
- Integer-format
- Fixtype of formats of (signed and unsigned) integer objects.
- Schar-format
- Fixtype of formats of signed char objects.
- Uinteger-sinteger-bit-roles-wfp
- Check if a list of roles of unsigned integer bits
and a list of roles of signed integer bits
are mutually consistent.
- Sinteger-format
- Fixtype of formats of signed integer objects.
- Integer-format-llong-wfp
- Check if an integer format is well-formed
when used for (signed and unsigned) long long.
- Integer-format-short-wfp
- Check if an integer format is well-formed
when used for (signed and unsigned) short.
- Integer-format-long-wfp
- Check if an integer format is well-formed
when used for (signed and unsigned) long.
- Integer-format-int-wfp
- Check if an integer format is well-formed
when used for (signed and unsigned) int.
- Uinteger-format
- Fixtype of formats of unsigned integer objects.
- Schar-format->min
- The ACL2 integer value of SCHAR_MIN [C17:5.2.4.2.1/1].
- Char+short+int+long+llong-format
- Fixtype of formats of
(unsigned, signed, and plain) char objects,
(unsigned and signed) short objects,
(unsigned and signed) int objects,
(unsigned and signed) long objects, and
(unsigned and signed) long long objects.
- Uchar-format
- Fixtype of formats of unsigned char objects.
- Char-format->min
- The ACL2 integer value of CHAR_MIN [C17:5.2.4.2.1/1].
- Integer-format-inc-sign-tcnpnt
- The unsigned and signed integer format defined by
a size greater than 1,
increasing value bits,
a sign bit at the end (for the signed format),
two's complement signed format,
no padding bits,
and no trap representations.
- Char-format->max
- The ACL2 integer value of CHAR_MAX [C17:5.2.4.2.1/1].
- Sinteger-format->min
- The ACL2 integer value of
the minimum value representable in a signed integer format.
- Sinteger-bit-role
- Fixtype of roles of integer bits in signed integers.
- Sinteger-bit-roles-wfp
- Check if a list of roles of signed integer bits is well-formed.
- Schar-format->max
- The ACL2 integer value of SCHAR_MAX [C17:5.2.4.2.1/1].
- Signed-format
- Fixtype of signed formats.
- Short-format-16tcnt
- The (unsigned and signed) short format defined by
16 bits with increasing values,
two's complement,
and no trap representations.
- Llong-format-64tcnt
- The (unsigned and signed) long long format defined by
64 bits with increasing values,
two's complement,
and no trap representations.
- Ienv
- Fixtype of implementation environments.
- Uinteger-bit-roles-wfp
- Check if a list of roles of unsigned integer bits is well-formed.
- Uinteger-bit-role
- Fixtype of roles of integer bits in unsigned integers.
- Long-format-32tcnt
- The (unsigned and signed) long format defined by
32 bits with increasing values,
two's complement,
and no trap representations.
- Int-format-16tcnt
- The (unsigned and signed) int format defined by
16 bits with increasing values,
two's complement,
and no trap representations.
- Uinteger+sinteger-format
- Fixtype of pairs consisting of
a format of unsigned integer objects
and a format of signed integer objects.
- Uinteger-bit-roles-value-count
- Number of value bit roles in
a list of roles of unsigned integer bits.
- Sinteger-bit-roles-value-count
- Number of value bit roles in
a list of roles of signed integer bits.
- Sinteger-bit-roles-inc-n-and-sign
- List of n signed integer value bit roles,
starting with exponent 0, in increasing exponent order,
and with a sign bit added at the end.
- Uinteger-bit-roles-inc-n
- List of n unsigned integer value bit roles,
starting with exponent 0, in increasing exponent order.
- Sinteger-format-inc-sign-tcnpnt
- The signed integer format defined by
n increasing value bits,
a sign bit at the end,
two's complement signed format,
no padding bits,
and no trap representations.
- Sinteger-bit-roles-inc-n
- List of n signed integer value bit roles,
starting with exponent 0, in increasing exponent order.
- Uchar-format->max
- The ACL2 integer value of UCHAR_MAX [C17:5.2.4.2.1/1].
- Char+short+int+long+llong-format-wfp
- Check if the formats of
char, short, int, long, and long long objects
are well-formed.
- Uinteger-bit-roles-exponents
- Exponents of a list of roles of unsigned integer bits.
- Sinteger-bit-roles-exponents
- Exponents of a list of roles of signed integer bits.
- Integer-format->bit-size
- Number of bits of an integer format.
- Char-format
- Fixtype of formats of char objects.
- Sinteger-bit-roles-sign-count
- Number of sign bit roles in a list of roles of signed integer bits.
- Ienv->char-min
- The ACL2 integer value of CHAR_MIN [C17:5.2.4.2.1/1].
- Uinteger-format-inc-npnt
- The unsigned integer format defined by
n increasing value bits,
no padding bits,
and no trap representations.
- Ienv->schar-min
- The ACL2 integer value of SCHAR_MIN [C17:5.2.4.2.1/1].
- Ienv->char-size
- The ACL2 integer value of CHAR_BIT [C17:5.2.4.2.1/1].
- Ienv->char-max
- The ACL2 integer value of CHAR_MAX [C17:5.2.4.2.1/1].
- Uinteger-format->max
- The ACL2 integer value of
the maximum value representable in an unsigned integer format.
- Sinteger-format->max
- The ACL2 integer value of
the maximum value representable in a signed integer format.
- Ienv->schar-max
- The ACL2 integer value of SCHAR_MAX [C17:5.2.4.2.1/1].
- Ienv->uchar-max
- The ACL2 integer value of UCHAR_MAX [C17:5.2.4.2.1/1].
- Ienv->short-bit-size
- Number of bits of unsigned and signed short objects.
- Ienv->long-bit-size
- Number of bits of unsigned and signed long objects.
- Ienv->llong-bit-size
- Number of bits of unsigned and signed long long objects.
- Schar-format-8tcnt
- The signed char format defined by
8 bits, two's complement, and no trap representations.
- Ienv->int-bit-size
- Number of bits of unsigned and signed int objects.
- Char-format-8u
- The char format defined by 8 bits and unsignedness.
- Char8+short16+int16+long32+llong64-tcnt
- The char, short, int, long, and long long
integer formats defined by
the minimal number of bits with increasing values,
two's complement,
no trap representations, and
unsigned plain chars.
- Uchar-format-8
- The unsigned char format defined by 8 bits.
- Uinteger-bit-role-list
- Fixtype of lists of roles of integer bits in unsigned integers.
- Sinteger-bit-role-list
- Fixtype of lists of roles of integer bits in signed integers.
- Uinteger-sinteger-bit-roles-wfp-of-inc-n-and-sign
- Mutual well-formedness of the lists of bit roles
from uinteger-bit-roles-inc-n
and sinteger-bit-roles-inc-n-and-sign.
