		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-cond

Check a ternary conditional expression [C:6.5.15].

Signature
(check-cond test-expr test-etype then-expr then-etype else-expr else-etype) → etype
Arguments: test-expr — Guard (exprp test-expr).; test-etype — Guard (expr-typep test-etype).; then-expr — Guard (exprp then-expr).; then-etype — Guard (expr-typep then-etype).; else-expr — Guard (exprp else-expr).; else-etype — Guard (expr-typep else-etype).
Returns: etype — Type (expr-type-resultp etype).

The test of a conditional expression must be scalar. For now we require the two branches to have arithmetic types. According to [C:6.5.15/3], in this case the type of the conditional expression is the one resulting from the usual arithmetic conversions [C:6.5.15/5]. This means that, at run time, in our dynamic semantics of C, we need to convert the branch that is executed to that type; but at run time we do not have information about the type of the other branch (the one that is not executed). Thus, in order to handle the execution properly, the static semantics should add information to the abstract syntax about the resulting type of the conditional expression, so that the dynamic semantics can perform the conversion while evaluating just one branch. (Presumably, C compilers would generate code that performs the conversion, if needed, for both branches of the conditional expression.) To avoid this complication, for now we make our static semantics more restrictive: we require the two branches to have the same promoted type. This means that that promoted type is also the type resulting from the usual arithmetic conversions, as can be easily seen in uaconvert-types. We may relax the treatment eventually, but note that we would have to restructure the static semantics to return possibly modified abstract syntax. This is not surprising, as it is a used approach for compiler-like tools, namely annotating abstract syntax trees with additional information. We apply both lvalue conversion and array-to-pointer conversion. A conditional expression is never an lvalue.

We perform lvalue conversion and array-to-pointer conversion on all three operands. A conditional expression is never an lvalue.

Definitions and Theorems

Function: check-cond

(defun check-cond (test-expr test-etype then-expr
                             then-etype else-expr else-etype)
  (declare (xargs :guard (and (exprp test-expr)
                              (expr-typep test-etype)
                              (exprp then-expr)
                              (expr-typep then-etype)
                              (exprp else-expr)
                              (expr-typep else-etype))))
  (let ((__function__ 'check-cond))
    (declare (ignorable __function__))
    (b* ((test-expr (expr-fix test-expr))
         (then-expr (expr-fix then-expr))
         (else-expr (expr-fix else-expr))
         (test-type (expr-type->type test-etype))
         (then-type (expr-type->type then-etype))
         (else-type (expr-type->type else-etype))
         (test-type (apconvert-type test-type))
         (then-type (apconvert-type then-type))
         (else-type (apconvert-type else-type))
         ((unless (type-scalarp test-type))
          (reserrf (list :cond-mistype-test
                         test-expr then-expr else-expr
                         :required :scalar
                         :supplied test-type)))
         ((unless (type-arithmeticp then-type))
          (reserrf (list :cond-mistype-then
                         test-expr then-expr else-expr
                         :required :arithmetic
                         :supplied then-type)))
         ((unless (type-arithmeticp else-type))
          (reserrf (list :cond-mistype-else
                         test-expr then-expr else-expr
                         :required :arithmetic
                         :supplied else-type)))
         (then-type (promote-type then-type))
         (else-type (promote-type else-type))
         ((unless (equal then-type else-type))
          (reserrf (list :diff-promoted-types
                         then-type else-type)))
         (type then-type))
      (make-expr-type :type type
                      :lvalue nil))))

Theorem: expr-type-resultp-of-check-cond

(defthm expr-type-resultp-of-check-cond
  (b* ((etype (check-cond test-expr test-etype then-expr
                          then-etype else-expr else-etype)))
    (expr-type-resultp etype))
  :rule-classes :rewrite)

Theorem: check-cond-of-expr-fix-test-expr

(defthm check-cond-of-expr-fix-test-expr
  (equal (check-cond (expr-fix test-expr)
                     test-etype then-expr
                     then-etype else-expr else-etype)
         (check-cond test-expr test-etype then-expr
                     then-etype else-expr else-etype)))

Theorem: check-cond-expr-equiv-congruence-on-test-expr

(defthm check-cond-expr-equiv-congruence-on-test-expr
  (implies (expr-equiv test-expr test-expr-equiv)
           (equal (check-cond test-expr test-etype then-expr
                              then-etype else-expr else-etype)
                  (check-cond test-expr-equiv test-etype then-expr
                              then-etype else-expr else-etype)))
  :rule-classes :congruence)

Theorem: check-cond-of-expr-type-fix-test-etype

(defthm check-cond-of-expr-type-fix-test-etype
  (equal (check-cond test-expr (expr-type-fix test-etype)
                     then-expr
                     then-etype else-expr else-etype)
         (check-cond test-expr test-etype then-expr
                     then-etype else-expr else-etype)))

Theorem: check-cond-expr-type-equiv-congruence-on-test-etype

(defthm check-cond-expr-type-equiv-congruence-on-test-etype
  (implies (expr-type-equiv test-etype test-etype-equiv)
           (equal (check-cond test-expr test-etype then-expr
                              then-etype else-expr else-etype)
                  (check-cond test-expr test-etype-equiv then-expr
                              then-etype else-expr else-etype)))
  :rule-classes :congruence)

Theorem: check-cond-of-expr-fix-then-expr

(defthm check-cond-of-expr-fix-then-expr
  (equal (check-cond test-expr
                     test-etype (expr-fix then-expr)
                     then-etype else-expr else-etype)
         (check-cond test-expr test-etype then-expr
                     then-etype else-expr else-etype)))

Theorem: check-cond-expr-equiv-congruence-on-then-expr

(defthm check-cond-expr-equiv-congruence-on-then-expr
  (implies (expr-equiv then-expr then-expr-equiv)
           (equal (check-cond test-expr test-etype then-expr
                              then-etype else-expr else-etype)
                  (check-cond test-expr test-etype then-expr-equiv
                              then-etype else-expr else-etype)))
  :rule-classes :congruence)

Theorem: check-cond-of-expr-type-fix-then-etype

(defthm check-cond-of-expr-type-fix-then-etype
  (equal (check-cond test-expr test-etype
                     then-expr (expr-type-fix then-etype)
                     else-expr else-etype)
         (check-cond test-expr test-etype then-expr
                     then-etype else-expr else-etype)))

Theorem: check-cond-expr-type-equiv-congruence-on-then-etype

(defthm check-cond-expr-type-equiv-congruence-on-then-etype
  (implies
       (expr-type-equiv then-etype then-etype-equiv)
       (equal (check-cond test-expr test-etype then-expr
                          then-etype else-expr else-etype)
              (check-cond test-expr test-etype then-expr
                          then-etype-equiv else-expr else-etype)))
  :rule-classes :congruence)

Theorem: check-cond-of-expr-fix-else-expr

(defthm check-cond-of-expr-fix-else-expr
  (equal (check-cond test-expr test-etype then-expr
                     then-etype (expr-fix else-expr)
                     else-etype)
         (check-cond test-expr test-etype then-expr
                     then-etype else-expr else-etype)))

Theorem: check-cond-expr-equiv-congruence-on-else-expr

(defthm check-cond-expr-equiv-congruence-on-else-expr
  (implies
       (expr-equiv else-expr else-expr-equiv)
       (equal (check-cond test-expr test-etype then-expr
                          then-etype else-expr else-etype)
              (check-cond test-expr test-etype then-expr
                          then-etype else-expr-equiv else-etype)))
  :rule-classes :congruence)

Theorem: check-cond-of-expr-type-fix-else-etype

(defthm check-cond-of-expr-type-fix-else-etype
  (equal (check-cond test-expr
                     test-etype then-expr then-etype
                     else-expr (expr-type-fix else-etype))
         (check-cond test-expr test-etype then-expr
                     then-etype else-expr else-etype)))

Theorem: check-cond-expr-type-equiv-congruence-on-else-etype

(defthm check-cond-expr-type-equiv-congruence-on-else-etype
  (implies
       (expr-type-equiv else-etype else-etype-equiv)
       (equal (check-cond test-expr test-etype then-expr
                          then-etype else-expr else-etype)
              (check-cond test-expr test-etype then-expr
                          then-etype else-expr else-etype-equiv)))
  :rule-classes :congruence)