		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-binary

Validate a binary expression, given the type of the sub-expression.

Signature
(valid-binary expr op type-arg1 type-arg2 ienv) → (mv erp type)
Arguments: expr — Guard (exprp expr).; op — Guard (binopp op).; type-arg1 — Guard (typep type-arg1).; type-arg2 — Guard (typep type-arg2).; ienv — Guard (ienvp ienv).
Returns: type — Type (typep type).

The * binary and / operators require arithmetic operands [C:6.5.5/2]. The result is the common type according to the usual arithmetic conversions [C:6.5.5/3]. There is no need for array-to-pointer or function-to-pointer conversions because those never produce arithmetic types.

The % operator requires integer operands [C:6.5.5/2]. The result is from the usual arithmetic conversions [C:6.5.5/3]. No array-to-pointer or function-to-pointer conversions are needed.

The + binary operator requires either two arithmetic operands or an integer and a pointer operand [C:6.5.6/2]. In the first case, the result is from the usual arithmetic conversions [C:6.5.6/4]. In the second case, the result is the pointer type [C:6.5.6/8]. Because of that second case, which involves pointers, we perform array-to-pointer conversion. We not perform function-to-pointer conversion, because that would result in a pointer to function, while a pointer to complete object type is required.

The - binary operator requires either two arithmetic operands, or two pointer operands, or a pointer first operand and an integer second operand [C:6.5.6/3]. In the first case, the result is from the usual arithmetic conversions [C:6.5.6/4]. In the second case, the result has type ptrdiff_t [C:6.5.6/9], which has an implementation-specific definition, and so we return the unknown type in this case. In the third case, the result has the pointer type [C:6.5.6/8]. Because of the second and third cases, which involve pointers, we perform array-to-pointer conversion. We not perform function-to-pointer conversion, because that would result in a pointer to function, while a pointer to complete object type is required.

The << and >> operators require integer operands [C:6.5.7/2]. The type of the result is the type of the promoted left operand [C:6.5.7/3]. There is no need for array-to-pointer or function-to-pointer conversions.

The <, >, <=, and >= operators require real types or pointer types [C:6.5.8/2]. The result is always signed int [C:6.5.8/6]. Since pointers may be involved, we perform array-to-pointer conversion. We not perform function-to-pointer conversion, because that would result in a pointer to function, while a pointer to object type is required.

The == and != operators require arithmetic types or pointer types [C:6.5.9/2]; since we currently have just one type for pointers, the distinctions between the three cases involving pointers reduce to just the simple case of two pointers for us for now. The result is always signed int [C:6.5.9/3]. Since pointers may be involved, we perform array-to-pointer and function-to-pointer conversions.

The &, ^, and | operators require integer operands [C:6.5.10/2] [C:6.5.11/2] [C:6.5.12/2]. The result has the type from the usual arithmetic conversions [C:6.5.10/3] [C:6.5.11/3] [C:6.5.12/3]. No array-to-pointer or function-to-pointer conversion is needed.

The && and || operators require scalar types [C:6.5.13/2] [C:6.5.14/2]. The result has type signed int [C:6.5.13/3] [C:6.5.14/3]. Since pointers may be involved, we need to perform array-to-pointer and function-to-pointer conversions.

The = simple assignment operator requires an lvalue as left operand [C:6.5.16/2], but currently we do not check that. In our currently approximate type system, the requirements in [C:6.5.16.1/1] reduce to the two operands having both arithmetic types, or both the structure type, or both the union type, or both pointer types. We do not perform array-to-pointer or function-to-pointer conversion on the left operand, because the result would not be an lvalue. The type of the result is the type of the left operand [C:6.5.16/3].

The *= and /= operators require arithmetic operands [C:6.5.16.2/2], and the result has the type of the first operand [C:6.5.16/3]. No array-to-pointer or function-to-pointer conversions are needed.

The %= operator requires integer operands [C:6.5.16.2/2], and the result has the type of the first operand [C:6.5.16/3]. No array-to-pointer or function-to-pointer conversions are needed.

The += and -= operands require either arithmetic operands or a first pointer operand and a second integer operand [C:6.5.16.2/1]. The result has the type of the first operand [C:6.5.16/3]. Since pointers may be involved, we perform array-to-pointer and function-to-pointer conversions.

The <<=, >>=, &=, ^=, and |= operators require integer operands [C:6.5.13.2/2]. The result has the type of the first operand [C:6.5.13/3]. No array-to-pointer or function-to-pointer conversions are needed.

Definitions and Theorems

Function: valid-binary

(defun valid-binary (expr op type-arg1 type-arg2 ienv)
 (declare (xargs :guard (and (exprp expr)
                             (binopp op)
                             (typep type-arg1)
                             (typep type-arg2)
                             (ienvp ienv))))
 (declare (xargs :guard (expr-case expr :binary)))
 (let ((__function__ 'valid-binary))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-type))
    ((when (or (type-case type-arg1 :unknown)
               (type-case type-arg2 :unknown)))
     (retok (type-unknown)))
    (msg
     (msg
      "In the binary expression ~x0, ~
                  the sub-expressiona have types ~x1 and ~x2."
      (expr-fix expr)
      (type-fix type-arg1)
      (type-fix type-arg2))))
   (case (binop-kind op)
     ((:mul :div)
      (b* (((unless (and (type-arithmeticp type-arg1)
                         (type-arithmeticp type-arg2)))
            (reterr msg)))
        (retok (type-uaconvert type-arg1 type-arg2 ienv))))
     (:rem (b* (((unless (and (type-arithmeticp type-arg1)
                              (type-arithmeticp type-arg2)))
                 (reterr msg)))
             (retok (type-uaconvert type-arg1 type-arg2 ienv))))
     (:add (b* ((type1 (type-apconvert type-arg1))
                (type2 (type-apconvert type-arg2)))
             (cond ((and (type-arithmeticp type1)
                         (type-arithmeticp type2))
                    (retok (type-uaconvert type1 type2 ienv)))
                   ((or (and (type-integerp type1)
                             (type-case type2 :pointer))
                        (and (type-case type1 :pointer)
                             (type-integerp type2)))
                    (retok (type-pointer)))
                   (t (reterr msg)))))
     (:sub (b* ((type1 (type-apconvert type-arg1))
                (type2 (type-apconvert type-arg2)))
             (cond ((and (type-arithmeticp type1)
                         (type-arithmeticp type2))
                    (retok (type-uaconvert type1 type2 ienv)))
                   ((and (type-case type1 :pointer)
                         (type-case type2 :pointer))
                    (retok (type-unknown)))
                   ((and (type-case type1 :pointer)
                         (type-integerp type2))
                    (retok (type-pointer)))
                   (t (reterr msg)))))
     ((:shl :shr)
      (b* (((unless (and (type-integerp type-arg1)
                         (type-integerp type-arg2)))
            (reterr msg)))
        (retok (type-promote type-arg1 ienv))))
     ((:lt :gt :le :ge)
      (b* ((type1 (type-apconvert type-arg1))
           (type2 (type-apconvert type-arg2))
           ((unless (or (and (type-realp type1)
                             (type-realp type2))
                        (and (type-case type1 :pointer)
                             (type-case type2 :pointer))))
            (reterr msg)))
        (retok (type-sint))))
     ((:eq :ne)
      (b* ((type1 (type-fpconvert (type-apconvert type-arg1)))
           (type2 (type-fpconvert (type-apconvert type-arg2)))
           ((unless (or (and (type-arithmeticp type1)
                             (type-arithmeticp type2))
                        (and (type-case type1 :pointer)
                             (type-case type2 :pointer))))
            (reterr msg)))
        (retok (type-sint))))
     ((:bitand :bitxor :bitior)
      (b* (((unless (and (type-integerp type-arg1)
                         (type-integerp type-arg2)))
            (reterr msg)))
        (retok (type-uaconvert type-arg1 type-arg2 ienv))))
     ((:logand :logor)
      (b* ((type1 (type-fpconvert (type-apconvert type-arg1)))
           (type2 (type-fpconvert (type-apconvert type-arg2)))
           ((unless (and (type-scalarp type1)
                         (type-scalarp type2)))
            (reterr msg)))
        (retok (type-sint))))
     (:asg (b* ((type1 type-arg1)
                (type2 (type-fpconvert (type-apconvert type-arg2)))
                ((unless (or (and (type-arithmeticp type1)
                                  (type-arithmeticp type2))
                             (and (type-case type1 :struct)
                                  (type-case type2 :struct))
                             (and (type-case type1 :union)
                                  (type-case type2 :union))
                             (and (or (type-case type1 :pointer)
                                      (type-case type1 :bool))
                                  (type-case type2 :pointer))))
                 (reterr msg)))
             (retok (type-fix type-arg1))))
     ((:asg-mul :asg-div)
      (b* (((unless (and (type-arithmeticp type-arg1)
                         (type-arithmeticp type-arg2)))
            (reterr msg)))
        (retok (type-fix type-arg1))))
     (:asg-rem (b* (((unless (and (type-integerp type-arg1)
                                  (type-integerp type-arg2)))
                     (reterr msg)))
                 (retok (type-fix type-arg1))))
     ((:asg-add :asg-sub)
      (b* ((type1 (type-fpconvert (type-apconvert type-arg1)))
           (type2 (type-fpconvert (type-apconvert type-arg2)))
           ((unless (or (and (type-arithmeticp type1)
                             (type-arithmeticp type2))
                        (and (type-case type1 :pointer)
                             (type-integerp type2))))
            (reterr msg)))
        (retok (type-fix type-arg1))))
     ((:asg-shl :asg-shr :asg-and
                :asg-xor :asg-ior)
      (b* (((unless (and (type-integerp type-arg1)
                         (type-integerp type-arg2)))
            (reterr msg)))
        (retok (type-fix type-arg1))))
     (t (prog2$ (impossible) (reterr t)))))))

Theorem: typep-of-valid-binary.type

(defthm typep-of-valid-binary.type
  (b* (((mv acl2::?erp ?type)
        (valid-binary expr op type-arg1 type-arg2 ienv)))
    (typep type))
  :rule-classes :rewrite)

Theorem: valid-binary-of-expr-fix-expr

(defthm valid-binary-of-expr-fix-expr
  (equal (valid-binary (expr-fix expr)
                       op type-arg1 type-arg2 ienv)
         (valid-binary expr op type-arg1 type-arg2 ienv)))

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

(defthm valid-binary-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (valid-binary expr op type-arg1 type-arg2 ienv)
                  (valid-binary expr-equiv
                                op type-arg1 type-arg2 ienv)))
  :rule-classes :congruence)

Theorem: valid-binary-of-binop-fix-op

(defthm valid-binary-of-binop-fix-op
  (equal (valid-binary expr (binop-fix op)
                       type-arg1 type-arg2 ienv)
         (valid-binary expr op type-arg1 type-arg2 ienv)))

Theorem: valid-binary-binop-equiv-congruence-on-op

(defthm valid-binary-binop-equiv-congruence-on-op
  (implies (binop-equiv op op-equiv)
           (equal (valid-binary expr op type-arg1 type-arg2 ienv)
                  (valid-binary expr
                                op-equiv type-arg1 type-arg2 ienv)))
  :rule-classes :congruence)

Theorem: valid-binary-of-type-fix-type-arg1

(defthm valid-binary-of-type-fix-type-arg1
  (equal (valid-binary expr op (type-fix type-arg1)
                       type-arg2 ienv)
         (valid-binary expr op type-arg1 type-arg2 ienv)))

Theorem: valid-binary-type-equiv-congruence-on-type-arg1

(defthm valid-binary-type-equiv-congruence-on-type-arg1
  (implies (type-equiv type-arg1 type-arg1-equiv)
           (equal (valid-binary expr op type-arg1 type-arg2 ienv)
                  (valid-binary expr
                                op type-arg1-equiv type-arg2 ienv)))
  :rule-classes :congruence)

Theorem: valid-binary-of-type-fix-type-arg2

(defthm valid-binary-of-type-fix-type-arg2
  (equal (valid-binary expr op type-arg1 (type-fix type-arg2)
                       ienv)
         (valid-binary expr op type-arg1 type-arg2 ienv)))

Theorem: valid-binary-type-equiv-congruence-on-type-arg2

(defthm valid-binary-type-equiv-congruence-on-type-arg2
  (implies (type-equiv type-arg2 type-arg2-equiv)
           (equal (valid-binary expr op type-arg1 type-arg2 ienv)
                  (valid-binary expr
                                op type-arg1 type-arg2-equiv ienv)))
  :rule-classes :congruence)

Theorem: valid-binary-of-ienv-fix-ienv

(defthm valid-binary-of-ienv-fix-ienv
  (equal (valid-binary expr
                       op type-arg1 type-arg2 (ienv-fix ienv))
         (valid-binary expr op type-arg1 type-arg2 ienv)))

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

(defthm valid-binary-ienv-equiv-congruence-on-ienv
  (implies (ienv-equiv ienv ienv-equiv)
           (equal (valid-binary expr op type-arg1 type-arg2 ienv)
                  (valid-binary expr
                                op type-arg1 type-arg2 ienv-equiv)))
  :rule-classes :congruence)