		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-cond

Validate a conditional expression, given types for its operands.

Signature
(valid-cond expr type-test type-then type-else ienv) → (mv erp type)
Arguments: expr — Guard (exprp expr).; type-test — Guard (typep type-test).; type-then — Guard (typep type-then).; type-else — Guard (typep type-else).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; type — Type (typep type).

The first operand must have scalar type [C17:6.5.15/2]. In our currently approximate type system, the other two operands must have both arithmetic type, or both the same structure type, or both the union type, or both the void type, or compatible pointer types, or one pointer type and the other operand a null pointer constant, or one pointer to an object type and one pointer to void [C17:6.5.15/3]. Currently, null pointer constants [C17:6.3.2.3/3] are approximated as any expression with an integer type. The type of the result is the one from the usual arithmetic converions in the first case, and the common type in the other cases [C17:6.5.15/5]. Since pointers may be involved, we need to perform array-to-pointer and function-to-pointer conversions.

Definitions and Theorems

Function: valid-cond

(defun valid-cond (expr type-test type-then type-else ienv)
 (declare (xargs :guard (and (exprp expr)
                             (typep type-test)
                             (typep type-then)
                             (typep type-else)
                             (ienvp ienv))))
 (declare (xargs :guard (expr-case expr :cond)))
 (b*
  (((reterr) (irr-type))
   ((when (or (type-case type-test :unknown)
              (type-case type-then :unknown)
              (type-case type-else :unknown)))
    (retok (type-unknown)))
   (type1 (type-fpconvert (type-apconvert type-test)))
   (type2 (type-fpconvert (type-apconvert type-then)))
   (type3 (type-fpconvert (type-apconvert type-else)))
   ((unless (type-scalarp type1))
    (retmsg$
     "In the conditional expression ~x0, ~
                  the first operand has type ~x1."
     (expr-fix expr)
     (type-fix type-test)))
   ((when (and (type-arithmeticp type2)
               (type-arithmeticp type3)))
    (retok (type-uaconvert type2 type3 ienv)))
   ((when (and (type-case type2 :struct)
               (type-case type3 :struct)))
    (if (type-equiv type2 type3)
        (retok type2)
      (retmsg$ "Struct types ~x0 and ~x1 are incompatible."
               type2 type3)))
   ((when (and (type-case type2 :union)
               (type-case type3 :union)))
    (retok (type-union)))
   ((when (and (type-case type2 :pointer)
               (type-compatiblep type2 type3 ienv)))
    (retok (type-composite type2 type3 ienv)))
   ((when (and (type-case type2 :pointer)
               (expr-null-pointer-constp (expr-cond->else expr)
                                         type3)))
    (retok (type-fix type2)))
   ((when (and (type-case type3 :pointer)
               (expr-cond->then expr)
               (expr-null-pointer-constp (expr-cond->then expr)
                                         type2)))
    (retok (type-fix type3)))
   ((when (and (type-case type2 :pointer)
               (type-case type3 :pointer)
               (let ((type-to2 (type-pointer->to type2))
                     (type-to3 (type-pointer->to type3)))
                 (or (and (type-case type-to2 :void)
                          (not (type-case type-to3 :function)))
                     (and (type-case type-to3 :void)
                          (not (type-case type-to2 :function)))))))
    (retok (make-type-pointer :to (type-void)))))
  (retmsg$
   "In the conditional expression ~x0, ~
              the second operand has type ~x1 ~
              and the third operand has type ~x2."
   (expr-fix expr)
   (type-fix type-then)
   (type-fix type-else))))

Theorem: maybe-msgp-of-valid-cond.erp

(defthm maybe-msgp-of-valid-cond.erp
  (b* (((mv acl2::?erp ?type)
        (valid-cond expr
                    type-test type-then type-else ienv)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: typep-of-valid-cond.type

(defthm typep-of-valid-cond.type
  (b* (((mv acl2::?erp ?type)
        (valid-cond expr
                    type-test type-then type-else ienv)))
    (typep type))
  :rule-classes :rewrite)

Theorem: valid-cond-of-expr-fix-expr

(defthm valid-cond-of-expr-fix-expr
  (equal (valid-cond (expr-fix expr)
                     type-test type-then type-else ienv)
         (valid-cond expr
                     type-test type-then type-else ienv)))

Theorem: valid-cond-expr-equiv-congruence-on-expr

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

Theorem: valid-cond-of-type-fix-type-test

(defthm valid-cond-of-type-fix-type-test
  (equal (valid-cond expr (type-fix type-test)
                     type-then type-else ienv)
         (valid-cond expr
                     type-test type-then type-else ienv)))

Theorem: valid-cond-type-equiv-congruence-on-type-test

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

Theorem: valid-cond-of-type-fix-type-then

(defthm valid-cond-of-type-fix-type-then
  (equal (valid-cond expr type-test (type-fix type-then)
                     type-else ienv)
         (valid-cond expr
                     type-test type-then type-else ienv)))

Theorem: valid-cond-type-equiv-congruence-on-type-then

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

Theorem: valid-cond-of-type-fix-type-else

(defthm valid-cond-of-type-fix-type-else
  (equal (valid-cond expr
                     type-test type-then (type-fix type-else)
                     ienv)
         (valid-cond expr
                     type-test type-then type-else ienv)))

Theorem: valid-cond-type-equiv-congruence-on-type-else

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

Theorem: valid-cond-of-ienv-fix-ienv

(defthm valid-cond-of-ienv-fix-ienv
  (equal (valid-cond expr type-test
                     type-then type-else (ienv-fix ienv))
         (valid-cond expr
                     type-test type-then type-else ienv)))

Theorem: valid-cond-ienv-equiv-congruence-on-ienv

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