		Search-engine friendly clone of the ACL2 documentation.

Read-write-variables

Write-auto-var

Write a variable in automatic storage.

Signature
(write-auto-var var val compst) → new-compst
Arguments: var — Guard (identp var).; val — Guard (valuep val).; compst — Guard (compustatep compst).
Returns: new-compst — Type (compustate-option-resultp new-compst).

That is, write the variable in the scopes of the top frame. The scopes are searched in the same way as read-auto-var. The variable must exist in order to write to it, i.e. it is not created; variables are created only via create-var. The new value must have the same type as the old value; note that, in our restricted dynamic semantics of C, variables always have values, they are never uninitialized.

If the variable is not found, we return nil, not an error. The reason is that this ACL2 function is used as a subroutine of write-var, where if a variable is not found in automatic storage, it is looked up in static storage. Thus, not finding a variable in automatic storage, in this ACL2 function, is not necessarily an error. If the auxiliary recursive function returns nil, it means that the variable was not found: since a frame always has at least one scope (see frame), this cannot be confused with a result where the variable was just not found in the scopes.

We do not look at other frames, because the variables in other frames are not in scope when running in the top frame.

Prior to storing the value, we remove its flexible array member, if any. See remove-flexible-array-member.

Definitions and Theorems

Function: write-auto-var-aux

(defun write-auto-var-aux (var val scopes)
  (declare (xargs :guard (and (identp var)
                              (valuep val)
                              (scope-listp scopes))))
  (let ((__function__ 'write-auto-var-aux))
    (declare (ignorable __function__))
    (b* (((when (endp scopes)) nil)
         (scope (scope-fix (car scopes)))
         (pair (omap::assoc (ident-fix var) scope))
         ((when (consp pair))
          (if (equal (type-of-value (cdr pair))
                     (type-of-value val))
              (cons (omap::update (ident-fix var)
                                  (remove-flexible-array-member val)
                                  scope)
                    (scope-list-fix (cdr scopes)))
            (error (list :write-auto-object-mistype (ident-fix var)
                         :old (type-of-value (cdr pair))
                         :new (type-of-value val)))))
         (new-cdr-scopes (write-auto-var-aux var val (cdr scopes)))
         ((when (errorp new-cdr-scopes))
          new-cdr-scopes)
         ((when (endp new-cdr-scopes)) nil))
      (cons scope new-cdr-scopes))))

Theorem: scope-list-resultp-of-write-auto-var-aux

(defthm scope-list-resultp-of-write-auto-var-aux
  (b* ((new-scopes (write-auto-var-aux var val scopes)))
    (scope-list-resultp new-scopes))
  :rule-classes :rewrite)

Theorem: consp-of-write-auto-var-aux

(defthm consp-of-write-auto-var-aux
  (b* ((?new-scopes (write-auto-var-aux var val scopes)))
    (implies (and (scope-listp new-scopes)
                  (consp new-scopes))
             (equal (consp new-scopes)
                    (consp scopes)))))

Theorem: len-of-write-auto-var-aux

(defthm len-of-write-auto-var-aux
  (b* ((?new-scopes (write-auto-var-aux var val scopes)))
    (implies (and (scope-listp new-scopes)
                  (consp new-scopes))
             (equal (len new-scopes) (len scopes)))))

Theorem: write-auto-var-aux-of-ident-fix-var

(defthm write-auto-var-aux-of-ident-fix-var
  (equal (write-auto-var-aux (ident-fix var)
                             val scopes)
         (write-auto-var-aux var val scopes)))

Theorem: write-auto-var-aux-ident-equiv-congruence-on-var

(defthm write-auto-var-aux-ident-equiv-congruence-on-var
  (implies (ident-equiv var var-equiv)
           (equal (write-auto-var-aux var val scopes)
                  (write-auto-var-aux var-equiv val scopes)))
  :rule-classes :congruence)

Theorem: write-auto-var-aux-of-value-fix-val

(defthm write-auto-var-aux-of-value-fix-val
  (equal (write-auto-var-aux var (value-fix val)
                             scopes)
         (write-auto-var-aux var val scopes)))

Theorem: write-auto-var-aux-value-equiv-congruence-on-val

(defthm write-auto-var-aux-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (write-auto-var-aux var val scopes)
                  (write-auto-var-aux var val-equiv scopes)))
  :rule-classes :congruence)

Theorem: write-auto-var-aux-of-scope-list-fix-scopes

(defthm write-auto-var-aux-of-scope-list-fix-scopes
  (equal (write-auto-var-aux var val (scope-list-fix scopes))
         (write-auto-var-aux var val scopes)))

Theorem: write-auto-var-aux-scope-list-equiv-congruence-on-scopes

(defthm write-auto-var-aux-scope-list-equiv-congruence-on-scopes
  (implies (scope-list-equiv scopes scopes-equiv)
           (equal (write-auto-var-aux var val scopes)
                  (write-auto-var-aux var val scopes-equiv)))
  :rule-classes :congruence)

Function: write-auto-var

(defun write-auto-var (var val compst)
 (declare (xargs :guard (and (identp var)
                             (valuep val)
                             (compustatep compst))))
 (declare (xargs :guard (> (compustate-frames-number compst)
                           0)))
 (let ((__function__ 'write-auto-var))
   (declare (ignorable __function__))
   (b*
    ((frame (top-frame compst))
     (new-scopes (write-auto-var-aux var val (frame->scopes frame)))
     ((when (errorp new-scopes)) new-scopes)
     ((when (endp new-scopes)) nil)
     (new-frame (change-frame frame
                              :scopes new-scopes)))
    (push-frame new-frame (pop-frame compst)))))

Theorem: compustate-option-resultp-of-write-auto-var

(defthm compustate-option-resultp-of-write-auto-var
  (b* ((new-compst (write-auto-var var val compst)))
    (compustate-option-resultp new-compst))
  :rule-classes :rewrite)

Theorem: compustate-frames-number-of-write-auto-var

(defthm compustate-frames-number-of-write-auto-var
  (b* ((?new-compst (write-auto-var var val compst)))
    (implies (and (> (compustate-frames-number compst) 0)
                  (compustatep new-compst))
             (equal (compustate-frames-number new-compst)
                    (compustate-frames-number compst)))))

Theorem: compustate-scopes-numbers-of-write-auto-var

(defthm compustate-scopes-numbers-of-write-auto-var
  (b* ((?new-compst (write-auto-var var val compst)))
    (implies (and (> (compustate-frames-number compst) 0)
                  (compustatep new-compst))
             (equal (compustate-scopes-numbers new-compst)
                    (compustate-scopes-numbers compst)))))

Theorem: write-auto-var-of-ident-fix-var

(defthm write-auto-var-of-ident-fix-var
  (equal (write-auto-var (ident-fix var)
                         val compst)
         (write-auto-var var val compst)))

Theorem: write-auto-var-ident-equiv-congruence-on-var

(defthm write-auto-var-ident-equiv-congruence-on-var
  (implies (ident-equiv var var-equiv)
           (equal (write-auto-var var val compst)
                  (write-auto-var var-equiv val compst)))
  :rule-classes :congruence)

Theorem: write-auto-var-of-value-fix-val

(defthm write-auto-var-of-value-fix-val
  (equal (write-auto-var var (value-fix val)
                         compst)
         (write-auto-var var val compst)))

Theorem: write-auto-var-value-equiv-congruence-on-val

(defthm write-auto-var-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (write-auto-var var val compst)
                  (write-auto-var var val-equiv compst)))
  :rule-classes :congruence)

Theorem: write-auto-var-of-compustate-fix-compst

(defthm write-auto-var-of-compustate-fix-compst
  (equal (write-auto-var var val (compustate-fix compst))
         (write-auto-var var val compst)))

Theorem: write-auto-var-compustate-equiv-congruence-on-compst

(defthm write-auto-var-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (write-auto-var var val compst)
                  (write-auto-var var val compst-equiv)))
  :rule-classes :congruence)