		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-unary

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

Signature
(valid-unary expr op type-arg ienv) → (mv erp type)
Arguments: expr — Guard (exprp expr).; op — Guard (unopp op).; type-arg — Guard (typep type-arg).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; type — Type (typep type).

The & operator requires an lvalue of any type as operand [C17:6.5.3.2/1] [C17:6.5.3.2/3], but we are not yet distinguishing lvalues from non-lvalues, so we allow any type of operand, and we return the pointer type derived from the operand type.

The * unary operator requires an operand of a pointer type [C17:6.5.3.2/2], after array-to-pointer and function-to-pointer conversions; as always, we also need to allow the unknown type. The result is the referenced type.

The + and - unary operators require an operand of an arithmetic type [C17:6.5.3.3/1], and the result has the promoted type [C17:6.5.3.3/2]. There is no need for array-to-pointer and function-to-pointer conversions, because they never result in arithmetic types.

The ~ operator requires an operand of an integer type [C17:6.5.3.3/1], and the result has the promoted type [C17:.6.5.3.3/4]. There is no need for array-to-pointer and function-to-pointer conversions, because they never result in arithmetic types.

The ! operator requires an operand of a scalar type [C17:6.5.3.3/1], and result is always signed int [C17:6.5.3.3/5]. Since pointers may be involved, we perform array-to-pointer and function-to-pointer conversions.

The sizeof operator applied to an expression requires a non-function complete type [C17:6.5.3.4/1]. In our current approximate type system, we just exclude function types, but we do not have a notion of complete types yet. The result has type size_t [C17:6.5.3.4/5], whose definition is implementation-defined, so for now we just return the unknown type; we will need to extend implementation environments with information about the definition of size_t.

The ++ pre-increment and -- pre-decrement operators require a real or pointer operand [C17:6.5.3.1/1]. Since these expressions are equivalent to assignments [C17:6.5.3.1/2] [C17:6.5.3.1/3], the type of the result must be the type of the operand. We do not perform array-to-pointer or function-to-pointer conversions, because those result in pointers, not lvalues as required [C17:6.5.3.1/1].

The ++ post-increment and -- post-decrement operators require a real or pointer operand [C17:6.5.2.4/1]. The type of the result is the same as the operand [C17:6.5.2.4/2] [C17:6.5.2.4/3]. We do not perform array-to-pointer or function-to-pointer conversions, because those result in pointers, not lvalues as required [C17:6.5.2.4/1].

The __real__ and __imag__ operators (GCC extensions) require a complex operand and return a corresponding real operand. This is what the GCC documentation seems to suggest, although the description is not as precise as in [C17].

Definitions and Theorems

Function: valid-unary

(defun valid-unary (expr op type-arg ienv)
 (declare (xargs :guard (and (exprp expr)
                             (unopp op)
                             (typep type-arg)
                             (ienvp ienv))))
 (declare (xargs :guard (expr-case expr :unary)))
 (b*
  (((reterr) (irr-type))
   (msg
    (msg$
     "In the unary expression ~x0, ~
                   the sub-expression has type ~x1."
     (expr-fix expr)
     (type-fix type-arg))))
  (case (unop-kind op)
    (:address (retok (make-type-pointer :to type-arg)))
    (:indir (b* (((when (type-case type-arg :unknown))
                  (retok (type-unknown)))
                 (type (type-fpconvert (type-apconvert type-arg))))
              (type-case type
                         :pointer (retok type.to)
                         :otherwise (reterr msg))))
    ((:plus :minus)
     (b* (((when (type-case type-arg :unknown))
           (retok (type-unknown)))
          ((unless (type-arithmeticp type-arg))
           (reterr msg)))
       (retok (type-integer-promote type-arg ienv))))
    (:bitnot (b* (((when (type-case type-arg :unknown))
                   (retok (type-unknown)))
                  ((unless (type-integerp type-arg))
                   (reterr msg)))
               (retok (type-integer-promote type-arg ienv))))
    (:lognot (b* (((when (type-case type-arg :unknown))
                   (retok (type-unknown)))
                  (type (type-fpconvert (type-apconvert type-arg)))
                  ((unless (type-scalarp type))
                   (reterr msg)))
               (retok (type-sint))))
    ((:preinc :predec :postinc :postdec)
     (b* (((when (type-case type-arg :unknown))
           (retok (type-unknown)))
          ((unless (or (type-realp type-arg)
                       (type-case type-arg :pointer)))
           (reterr msg)))
       (retok (type-fix type-arg))))
    (:sizeof (b* (((when (type-case type-arg :function))
                   (reterr msg)))
               (retok (type-unknown))))
    (:alignof (b* (((when (type-case type-arg :function))
                    (reterr msg)))
                (retok (type-unknown))))
    (:real (type-case type-arg
                      :floatc (retok (type-float))
                      :doublec (retok (type-double))
                      :ldoublec (retok (type-ldouble))
                      :unknown (retok (type-unknown))
                      :otherwise (reterr msg)))
    (:imag (type-case type-arg
                      :floatc (retok (type-float))
                      :doublec (retok (type-double))
                      :ldoublec (retok (type-ldouble))
                      :unknown (retok (type-unknown))
                      :otherwise (reterr msg)))
    (t (prog2$ (impossible) (retmsg$ ""))))))

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

(defthm maybe-msgp-of-valid-unary.erp
  (b* (((mv acl2::?erp ?type)
        (valid-unary expr op type-arg ienv)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: typep-of-valid-unary.type

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

Theorem: valid-unary-of-expr-fix-expr

(defthm valid-unary-of-expr-fix-expr
  (equal (valid-unary (expr-fix expr)
                      op type-arg ienv)
         (valid-unary expr op type-arg ienv)))

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

(defthm valid-unary-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (valid-unary expr op type-arg ienv)
                  (valid-unary expr-equiv op type-arg ienv)))
  :rule-classes :congruence)

Theorem: valid-unary-of-unop-fix-op

(defthm valid-unary-of-unop-fix-op
  (equal (valid-unary expr (unop-fix op)
                      type-arg ienv)
         (valid-unary expr op type-arg ienv)))

Theorem: valid-unary-unop-equiv-congruence-on-op

(defthm valid-unary-unop-equiv-congruence-on-op
  (implies (unop-equiv op op-equiv)
           (equal (valid-unary expr op type-arg ienv)
                  (valid-unary expr op-equiv type-arg ienv)))
  :rule-classes :congruence)

Theorem: valid-unary-of-type-fix-type-arg

(defthm valid-unary-of-type-fix-type-arg
  (equal (valid-unary expr op (type-fix type-arg)
                      ienv)
         (valid-unary expr op type-arg ienv)))

Theorem: valid-unary-type-equiv-congruence-on-type-arg

(defthm valid-unary-type-equiv-congruence-on-type-arg
  (implies (type-equiv type-arg type-arg-equiv)
           (equal (valid-unary expr op type-arg ienv)
                  (valid-unary expr op type-arg-equiv ienv)))
  :rule-classes :congruence)

Theorem: valid-unary-of-ienv-fix-ienv

(defthm valid-unary-of-ienv-fix-ienv
  (equal (valid-unary expr op type-arg (ienv-fix ienv))
         (valid-unary expr op type-arg ienv)))

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

(defthm valid-unary-ienv-equiv-congruence-on-ienv
  (implies (ienv-equiv ienv ienv-equiv)
           (equal (valid-unary expr op type-arg ienv)
                  (valid-unary expr op type-arg ienv-equiv)))
  :rule-classes :congruence)