		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: type — Type (typep type).

The & operator requires an lvalue of any type as operand [C:6.5.3.2/1] [C: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 (one) pointer type.

The * unary operator requires an operand of a pointer type [C:6.5.3.2/2], after array-to-pointer and function-to-pointer conversions; as always, we also need to allow the unknown type. Since we only have one type for pointers for now, the resulting type is unknown.

The + and - unary operators require an operand of an arithmetic type [C:6.5.3.3/1], and the result has the promoted type [C: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 [C:6.5.3.3/1], and the result has the promoted type [C:.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 [C:6.5.3.3/1], and result is always signed int [C: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 [C: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 [C: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 [C:6.5.3.1/1]. Since these expressions are equivalent to assignments [C:6.5.3.1/2] [C: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 [C:6.5.3.1/1].

The ++ post-increment and -- post-decrement operators require a real or pointer operand [C:6.5.2.4/1]. The type of the result is the same as the operand [C:6.5.2.4/2] [C: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 [C:6.5.2.4/1].

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)))
 (let ((__function__ 'valid-unary))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-type))
    ((when (type-case type-arg :unknown))
     (retok (type-unknown)))
    (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 (type-pointer)))
     (:indir (b* ((type (type-fpconvert (type-apconvert type-arg)))
                  ((unless (type-case type :pointer))
                   (reterr msg)))
               (retok (type-unknown))))
     ((:plus :minus)
      (b* (((unless (type-arithmeticp type-arg))
            (reterr msg)))
        (retok (type-promote type-arg ienv))))
     (:bitnot (b* (((unless (type-integerp type-arg))
                    (reterr msg)))
                (retok (type-promote type-arg ienv))))
     (:lognot (b* ((type (type-fpconvert (type-apconvert type-arg)))
                   ((unless (type-scalarp type))
                    (reterr msg)))
                (retok (type-sint))))
     ((:preinc :predec :postinc :postdec)
      (b* (((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))))
     (t (prog2$ (impossible) (reterr t)))))))

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)