		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-expr-asg

Check an expression that must be an assignment expression.

Signature
(check-expr-asg e funtab vartab tagenv) → wf?
Arguments: e — Guard (exprp e).; funtab — Guard (fun-tablep funtab).; vartab — Guard (var-tablep vartab).; tagenv — Guard (tag-envp tagenv).
Returns: wf? — Type (wellformed-resultp wf?).

For now, we only allow simple assignment expressions. The left-hand side expression must be a pure lvalue. Before checking that, we perform an array-to-pointer conversion [C17:6.3.2.1/3]: in doing so, we also turn off the lvalue flag of the expression type, as specified in [C17:6.3.2.1/3]; this means that using something of an array type as the left-hand side of assignment fails. The right-hand side must be a function call or a pure expression; we implicitly apply lvalue conversion to it (because check-expr-call-or-pure returns a plain type; we apply array-to-pointer conversion to it as well.

The two sides must have the same type, which is more restrictive than [C17:6.5.16.1]. Since it is an invariant (currently not formally proved) that variables never have void type, the equality of types implies that, if the right-hand side is a function call, the function must not return void. We require the left type (and thus the right type) to be arithmetic or structure or pointer [C17:6.5.16.1]. We do not return any type information from the assignment because an expression statement throws away the expression's value; indeed, we are only interested in the side effects of assignment here.

Definitions and Theorems

Function: check-expr-asg

(defun check-expr-asg (e funtab vartab tagenv)
 (declare (xargs :guard (and (exprp e)
                             (fun-tablep funtab)
                             (var-tablep vartab)
                             (tag-envp tagenv))))
 (let ((__function__ 'check-expr-asg))
  (declare (ignorable __function__))
  (b*
   (((unless (expr-case e :binary))
     (reserrf (list :expr-asg-not-binary (expr-fix e))))
    (op (expr-binary->op e))
    (left (expr-binary->arg1 e))
    (right (expr-binary->arg2 e))
    ((unless (binop-case op :asg))
     (reserrf (list :expr-asg-not-asg op)))
    ((okf left-etype)
     (check-expr-pure left vartab tagenv))
    (left-type (expr-type->type left-etype))
    (left-etype (if (type-case left-type :array)
                    (make-expr-type :type (apconvert-type left-type)
                                    :lvalue nil)
                  left-etype))
    ((unless (expr-type->lvalue left-etype))
     (reserrf (list :asg-left-not-lvalue (expr-fix e))))
    (left-type (expr-type->type left-etype))
    ((okf right-type)
     (check-expr-call-or-pure right funtab vartab tagenv))
    (right-type (apconvert-type right-type))
    ((unless (equal left-type right-type))
     (reserrf (list :asg-mistype left right
                    :required left-type
                    :supplied right-type)))
    ((unless (or (type-arithmeticp left-type)
                 (type-case left-type :struct)
                 (type-case left-type :pointer)))
     (reserrf (list :expr-asg-disallowed-type left-type))))
   :wellformed)))

Theorem: wellformed-resultp-of-check-expr-asg

(defthm wellformed-resultp-of-check-expr-asg
  (b* ((wf? (check-expr-asg e funtab vartab tagenv)))
    (wellformed-resultp wf?))
  :rule-classes :rewrite)

Theorem: check-expr-asg-of-expr-fix-e

(defthm check-expr-asg-of-expr-fix-e
  (equal (check-expr-asg (expr-fix e)
                         funtab vartab tagenv)
         (check-expr-asg e funtab vartab tagenv)))

Theorem: check-expr-asg-expr-equiv-congruence-on-e

(defthm check-expr-asg-expr-equiv-congruence-on-e
  (implies (expr-equiv e e-equiv)
           (equal (check-expr-asg e funtab vartab tagenv)
                  (check-expr-asg e-equiv funtab vartab tagenv)))
  :rule-classes :congruence)

Theorem: check-expr-asg-of-fun-table-fix-funtab

(defthm check-expr-asg-of-fun-table-fix-funtab
  (equal (check-expr-asg e (fun-table-fix funtab)
                         vartab tagenv)
         (check-expr-asg e funtab vartab tagenv)))

Theorem: check-expr-asg-fun-table-equiv-congruence-on-funtab

(defthm check-expr-asg-fun-table-equiv-congruence-on-funtab
  (implies (fun-table-equiv funtab funtab-equiv)
           (equal (check-expr-asg e funtab vartab tagenv)
                  (check-expr-asg e funtab-equiv vartab tagenv)))
  :rule-classes :congruence)

Theorem: check-expr-asg-of-var-table-fix-vartab

(defthm check-expr-asg-of-var-table-fix-vartab
  (equal (check-expr-asg e funtab (var-table-fix vartab)
                         tagenv)
         (check-expr-asg e funtab vartab tagenv)))

Theorem: check-expr-asg-var-table-equiv-congruence-on-vartab

(defthm check-expr-asg-var-table-equiv-congruence-on-vartab
  (implies (var-table-equiv vartab vartab-equiv)
           (equal (check-expr-asg e funtab vartab tagenv)
                  (check-expr-asg e funtab vartab-equiv tagenv)))
  :rule-classes :congruence)

Theorem: check-expr-asg-of-tag-env-fix-tagenv

(defthm check-expr-asg-of-tag-env-fix-tagenv
  (equal (check-expr-asg e funtab vartab (tag-env-fix tagenv))
         (check-expr-asg e funtab vartab tagenv)))

Theorem: check-expr-asg-tag-env-equiv-congruence-on-tagenv

(defthm check-expr-asg-tag-env-equiv-congruence-on-tagenv
  (implies (tag-env-equiv tagenv tagenv-equiv)
           (equal (check-expr-asg e funtab vartab tagenv)
                  (check-expr-asg e funtab vartab tagenv-equiv)))
  :rule-classes :congruence)