|
|
|---|
|
|
|
|---|
ATC tutorial: ACL2 representation of C conditional expressions.
C has both conditional statements and conditional expressions.
Conditional expressions are ternary expressions of the form
C conditional expressions are represented by ACL2 ifs wrapped with condexpr. This is the identity function, and should be normally enabled in proofs. Its purpose is to indicate to ATC that the wrapped if represents a conditional expressions instead of a conditional statements. Given that conditional statements are more frequent than conditional expressions in C, using the wrapper for conditional expressions, and no wrapper for conditional statements, reduces verbosity while still supporting the explicit distinction.
For example, the ACL2 function
(defun |h| (|x| |y|) (declare (xargs :guard (and (c::sintp |x|) (c::sintp |y|) ;; x > 0: (> (c::integer-from-sint |x|) 0)) :guard-hints (("Goal" :in-theory (enable c::sub-sint-sint-okp c::sint-integerp-alt-def c::sint-integer-fix c::integer-from-sint))))) (c::sub-sint-sint |x| (c::condexpr (if (c::boolean-from-sint (c::ge-sint-sint |y| (c::sint-dec-const 18))) (c::sint 0) (c::sint 1)))))
represents the C function
int h(int x, int y) {
return x - (y >= 18 ? 0 : 1);
}As another example, the ACL2 function
(defun |i| (|a| |b|) (declare (xargs :guard (and (c::sintp |a|) (c::sintp |b|)) :guard-hints (("Goal" :in-theory (enable c::boolean-from-sint c::sint-integerp-alt-def c::sint-integer-fix c::gt-sint-sint c::sub-sint-sint-okp c::integer-from-sint))))) (if (c::boolean-from-sint (c::gt-sint-sint |a| |b|)) (c::sub-sint-sint |a| (c::condexpr (if (c::boolean-from-sint (c::eq-sint-sint |b| (c::sint-dec-const 3))) (c::sint-dec-const 0) (c::sint-dec-const 1)))) |b|))
represents the C function
int i(int a, int b) {
if (a > b) {
return a - (b == 3 ? 0 : 1);
} else {
return b;
}
}Note that the two ACL2 ifs are treated differently because of the absence or presence of the condexpr wrapper: the outer one represents a conditional statement, the inner one represents a conditional expression.
The tests of the ACL2 ifs that represent conditional expressions
must return ACL2 booleans,
in the same way as the ifs that represent conditional statements.
As explained in atc-tutorial-conditional-statements,
the function boolean-from-sint is used
to convert C
It is important to note that representing C conditional expressions with a ternary function defined to be equal to if does not work. Such a function would have to be strict, like all ACL2 functions except if. But in general conditional expressions must be non-strict.