		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 [C17:6.5.5/2]. The result is the common type according to the usual arithmetic conversions [C17: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 [C17:6.5.5/2]. The result is from the usual arithmetic conversions [C17: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 [C17:6.5.6/2]. In the first case, the result is from the usual arithmetic conversions [C17:6.5.6/4]. In the second case, the result is the pointer type [C17:6.5.6/8]. Because of that second case, which involves pointers, we perform array-to-pointer conversion. We do 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 [C17:6.5.6/3]. In the first case, the result is from the usual arithmetic conversions [C17:6.5.6/4]. In the second case, the result has type ptrdiff_t [C17: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 [C17:6.5.6/8]. Because of the second and third cases, which involve pointers, we perform array-to-pointer conversion. We do 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 [C17:6.5.7/2]. The type of the result is the type of the promoted left operand [C17: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 [C17:6.5.8/2]. The result is always signed int [C17:6.5.8/6]. Since pointers may be involved, we perform array-to-pointer conversion. We do not perform function-to-pointer conversion, because that would result in a pointer to function, while a pointer to object type is required. The standard does not allow a null pointer constants [C17:6.3.2.3/3] without the void * cast to be used as an operand while the other operand has pointer type. But we found it accepted by practical compilers, so it is probably a GCC extensions, and for this reason we accept it for now; we should extend our implementation environments with information about whether GCC extensions are allowed, and condition acceptance under that flag. Since we do not have code yet to recognize null pointer constants, we accept any integer expression; that is, we allow one pointer operand and one integer operand.

The == and != operators require arithmetic types or pointer types [C17:6.5.9/2]; Distinctions betwen qualified and unqualified pointer types, as well as void or non-void pointers types are ignored since we currently approximate all of these as a single pointer type. Since we do not yet implement evaluation of constant expressions, all integer expressions are considered potential null pointer constants: so we allow an operand to be a pointer and the other to be an integer, to accommodate a null pointer constant [C17:6.3.2.3/3] without the void * cast. The result is always signed int [C17: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 [C17:6.5.10/2] [C17:6.5.11/2] [C17:6.5.12/2]. The result has the type from the usual arithmetic conversions [C17:6.5.10/3] [C17:6.5.11/3] [C17:6.5.12/3]. No array-to-pointer or function-to-pointer conversion is needed.

The && and || operators require scalar types [C17:6.5.13/2] [C17:6.5.14/2]. The result has type signed int [C17:6.5.13/3] [C17: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 [C17:6.5.16/2], but currently we do not check that. In our currently approximate type system, the requirements in [C17:6.5.16.1/1] reduce to the following four cases.

Both operands have arithmetic types.
The left operand has a structure or union type, and the two operand types are compatible.
The left operand has the pointer type and the right operand is either a pointer or a null pointer constant (approximated as anything of an integer type).
The left operand has the boolean type and the right operand has the pointer type.

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 [C17:6.5.16/3].

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

The %= operator requires integer operands [C17:6.5.16.2/2], and the result has the type of the first operand [C17: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 [C17:6.5.16.2/1]. The result has the type of the first operand [C17: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 [C17:6.5.13.2/2]. The result has the type of the first operand [C17: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-integerp type2))
                   (retok (type-pointer)))
                  ((and (type-case type1 :pointer)
                        (type-case type2 :pointer))
                   (retok (type-unknown)))
                  (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))
          (if (type-case type1 :pointer)
              (or (type-case type2 :pointer)
                  (expr-null-pointer-constp (expr-binary->arg2 expr)
                                            type2))
            (and (expr-null-pointer-constp (expr-binary->arg1 expr)
                                           type1)
                 (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))
          (if (type-case type1 :pointer)
              (or (type-case type2 :pointer)
                  (expr-null-pointer-constp (expr-binary->arg2 expr)
                                            type2))
            (and (expr-null-pointer-constp (expr-binary->arg1 expr)
                                           type1)
                 (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 (or (type-case type1 :struct)
                   (type-case type1 :union))
               (type-compatiblep type1 type2))
          (and
              (type-case type1 :pointer)
              (or (type-case type2 :pointer)
                  (expr-null-pointer-constp (expr-binary->arg2 expr)
                                            type2)))
          (and (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)