		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-unary

Check the application of a unary operator to an expression.

Signature
(check-unary op arg-expr arg-etype) → etype
Arguments: op — Guard (unopp op).; arg-expr — Guard (exprp arg-expr).; arg-etype — Guard (expr-typep arg-etype).
Returns: etype — Type (expr-type-resultp etype).

We check arg-etype against op; arg-expr is used just for errors. We return the type of the unary expression.

The operand of the address operator must be an lvalue [C17:6.5.3.2/1]. The text in [C17:6.5.3.2/1] talks about lvalues but singles out postfix [] expressions and unary * expressions, even though those are just special cases of lvalues; perhaps this has to do with the restriction about the bit-field and the register modifier, but since none of these are covered in our current C model, we can just say that, for us, the argument of & must be an lvalue. This is why this ACL2 function takes an expression type, not just a type, for the argument: it is so that we can check the & operator; checking the other operators only involves the type. If the type of the argument is T, the type of the result is pointer to T [C17:6.5.3.2/3]; the expression is not an lvalue.

The operand of the indirection operator must be a pointer [C17:6.5.3.2/2]. The result has the referenced type, and the expression is an lvalue [C17:6.5.3.2/4]. We return an expression type, not a type, so that we can represent the fact that an indirection expression is an lvalue. All the other unary expressions are not lvalues.

For unary plus and minus, the operand must be arithmetic, and the result has the promoted type.

For bitwise negation, the operand must be integer, and the result has the promoted type.

For logical negation, the operand must be scalar and the result is int -- 0 or 1.

For all operators except &, the argument is subjected to lvalue conversion [C17:6.3.2.1/2] and array-to-pointer conversion [C17:6.3.2.1/3]. In our static semantics, lvalue conversion just amounts to ignoring the lvalue flag of the expression type.

Definitions and Theorems

Function: check-unary

(defun check-unary (op arg-expr arg-etype)
 (declare (xargs :guard (and (unopp op)
                             (exprp arg-expr)
                             (expr-typep arg-etype))))
 (let ((__function__ 'check-unary))
   (declare (ignorable __function__))
   (case (unop-kind op)
     (:address
          (if (expr-type->lvalue arg-etype)
              (make-expr-type
                   :type (type-pointer (expr-type->type arg-etype))
                   :lvalue nil)
            (reserrf (list :unary-mistype (unop-fix op)
                           (expr-fix arg-expr)
                           :required :lvalue
                           :supplied (expr-type-fix arg-etype)))))
     (:indir (b* ((arg-type (expr-type->type arg-etype))
                  (arg-type (apconvert-type arg-type)))
               (if (type-case arg-type :pointer)
                   (make-expr-type :type (type-pointer->to arg-type)
                                   :lvalue t)
                 (reserrf (list :unary-mistype (unop-fix op)
                                (expr-fix arg-expr)
                                :required :pointer
                                :supplied arg-type)))))
     ((:plus :minus)
      (b* ((arg-type (expr-type->type arg-etype))
           (arg-type (apconvert-type arg-type)))
        (if (type-arithmeticp arg-type)
            (make-expr-type :type (promote-type arg-type)
                            :lvalue nil)
          (reserrf (list :unary-mistype (unop-fix op)
                         (expr-fix arg-expr)
                         :required :arithmetic
                         :supplied (type-fix arg-type))))))
     (:bitnot (b* ((arg-type (expr-type->type arg-etype))
                   (arg-type (apconvert-type arg-type)))
                (if (type-integerp arg-type)
                    (make-expr-type :type (promote-type arg-type)
                                    :lvalue nil)
                  (reserrf (list :unary-mistype (unop-fix op)
                                 (expr-fix arg-expr)
                                 :required :integer
                                 :supplied (type-fix arg-type))))))
     (:lognot (b* ((arg-type (expr-type->type arg-etype))
                   (arg-type (apconvert-type arg-type)))
                (if (type-scalarp arg-type)
                    (make-expr-type :type (type-sint)
                                    :lvalue nil)
                  (reserrf (list :unary-mistype (unop-fix op)
                                 (expr-fix arg-expr)
                                 :required :scalar
                                 :supplied (type-fix arg-type))))))
     (t (reserrf (impossible))))))

Theorem: expr-type-resultp-of-check-unary

(defthm expr-type-resultp-of-check-unary
  (b* ((etype (check-unary op arg-expr arg-etype)))
    (expr-type-resultp etype))
  :rule-classes :rewrite)

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

(defthm check-unary-of-unop-fix-op
  (equal (check-unary (unop-fix op)
                      arg-expr arg-etype)
         (check-unary op arg-expr arg-etype)))

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

(defthm check-unary-unop-equiv-congruence-on-op
  (implies (unop-equiv op op-equiv)
           (equal (check-unary op arg-expr arg-etype)
                  (check-unary op-equiv arg-expr arg-etype)))
  :rule-classes :congruence)

Theorem: check-unary-of-expr-fix-arg-expr

(defthm check-unary-of-expr-fix-arg-expr
  (equal (check-unary op (expr-fix arg-expr)
                      arg-etype)
         (check-unary op arg-expr arg-etype)))

Theorem: check-unary-expr-equiv-congruence-on-arg-expr

(defthm check-unary-expr-equiv-congruence-on-arg-expr
  (implies (expr-equiv arg-expr arg-expr-equiv)
           (equal (check-unary op arg-expr arg-etype)
                  (check-unary op arg-expr-equiv arg-etype)))
  :rule-classes :congruence)

Theorem: check-unary-of-expr-type-fix-arg-etype

(defthm check-unary-of-expr-type-fix-arg-etype
  (equal (check-unary op arg-expr (expr-type-fix arg-etype))
         (check-unary op arg-expr arg-etype)))

Theorem: check-unary-expr-type-equiv-congruence-on-arg-etype

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