|
|
|---|
|
|
|
|---|
Calculate the integer value result of an operation.
(result-integer-value mathint type) → val
This applies to most (but not all) integer operations, and thus it is factored in this ACL2 function.
Operations on unsigned integers are always well-defined, because if the exact mathematical result does not fit in the type, it is reduced modulo one plus the maximum integer of the type [C:6.2.5/9]. In contrast, operations on signed integers are not necessarily well-defined when the exact mathematical result does not fit in the type [C:6.5/5]. [C] could be clearer on this point, but it seems that it allows implementations that silently wrap around as well as implementations that trap on overflow, as suggested by the example in [C:5.1.2.3//15], as well as by the wording in [C:H.2.2/1]. Note also that [C:3.4.3] says that integer overflow is an example of undefined behavior, but this should be taken to mean signed integer overflow, given that [C:6.2.5/9] says that unsigned operations do not overflow (due to the modular reduction mentioned above). So for now we regard as an error the situation of a signed result that does not fit in the type, given that [C] does not prescribe what should happen in this case; in the future, we may extend our model with a parameterization over the specifics of how this situation is handled.
We define most of the integer operations to obtain the mathematical integers from the operands, combine them according to the specifics of the operation, and then turning the resulting mathematical integer into an integer value. This ACL2 function serves to accomplish the last step. The type of the result, which is also the type of the operand(s) (after the usual arithmetic conversions [C:6.3.1.8] for binary operations), is passed as argument to this ACL2 function, along with the mathematical integer of the result. We return a value or an error, according to the criteria explained above.
Note that this is the same calculation done in convert-integer-value after obtaining the mathematical integer from the starting value. So we could use this function in the definition of convert-integer-value, but we prefer to keep them separate because in the future we may parameterize our C dynamic semantics on the choice of whether overflowing signed arithmetic should be an error (as it is now) or silently wrap around, or cause a trap (traps may have to be modeled explicitly). Since integer conversions are described separately from other integer operations in [C], the behavior of integer conversions and other integer operations could be parameterized differently.
Function:
(defun result-integer-value (mathint type) (declare (xargs :guard (and (integerp mathint) (typep type)))) (declare (xargs :guard (type-nonchar-integerp type))) (let ((__function__ 'result-integer-value)) (declare (ignorable __function__)) (b* ((mathint (ifix mathint))) (cond ((type-unsigned-integerp type) (value-integer (mod mathint (1+ (integer-type-max type))) type)) ((integer-type-rangep mathint type) (value-integer mathint type)) (t (error (list :out-of-range mathint (type-fix type))))))))
Theorem:
(defthm value-resultp-of-result-integer-value (b* ((val (result-integer-value mathint type))) (value-resultp val)) :rule-classes :rewrite)
Theorem:
(defthm result-integer-value-of-ifix-mathint (equal (result-integer-value (ifix mathint) type) (result-integer-value mathint type)))
Theorem:
(defthm result-integer-value-int-equiv-congruence-on-mathint (implies (acl2::int-equiv mathint mathint-equiv) (equal (result-integer-value mathint type) (result-integer-value mathint-equiv type))) :rule-classes :congruence)
Theorem:
(defthm result-integer-value-of-type-fix-type (equal (result-integer-value mathint (type-fix type)) (result-integer-value mathint type)))
Theorem:
(defthm result-integer-value-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (result-integer-value mathint type) (result-integer-value mathint type-equiv))) :rule-classes :congruence)