		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-computation-states

Update-var

Update a variable in a canonical representation of computation states.

Signature
(update-var var val compst) → new-compst
Arguments: var — Guard (identp var).; val — Guard (valuep val).; compst — Guard (compustatep compst).
Returns: new-compst — Type (compustatep new-compst).

This is like write-var, but it does not return an error. First, if we do not find the variable in automatic storage, we add it to static storage unconditionally: this ensures that the variable is always there, which simplifies other rules; we check that the variable is actually there when we turn write-var into update-var, in another rule. Second, we do not check the type of the new value against the type of the old value if the variable is found, and instead we unconditionally overwrite the old value with the new value: this ensures that the new value is always there, which simplified other rules; we check that the types match when we turn write-var into update-var, in another rule.

The guard requires at least one frame. This is adequate, since we only use this function during symbolic execution, when we are executing some function's code, and so there must be always some frame. (Actually, given that this function is only used for symbolic execution, it does not need to be guard-verified; the same applies to add-frame and add-var, but for now we keep them guard-verified.)

Definitions and Theorems

Function: update-var-aux

(defun update-var-aux (var val scopes)
  (declare (xargs :guard (and (identp var)
                              (valuep val)
                              (scope-listp scopes))))
  (let ((__function__ 'update-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))
          (cons (omap::update (ident-fix var)
                              (remove-flexible-array-member val)
                              scope)
                (scope-list-fix (cdr scopes)))))
      (cons scope
            (update-var-aux var val (cdr scopes))))))

Theorem: scope-listp-of-update-var-aux

(defthm scope-listp-of-update-var-aux
  (b* ((new-scopes (update-var-aux var val scopes)))
    (scope-listp new-scopes))
  :rule-classes :rewrite)

Theorem: consp-of-update-var-aux

(defthm consp-of-update-var-aux
  (b* ((?new-scopes (update-var-aux var val scopes)))
    (equal (consp new-scopes)
           (consp scopes))))

Theorem: var-in-scopes-p-of-update-var-aux

(defthm var-in-scopes-p-of-update-var-aux
  (iff (var-in-scopes-p var (update-var-aux var2 val scopes))
       (var-in-scopes-p var scopes)))

Theorem: update-var-aux-of-ident-fix-var

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

Theorem: update-var-aux-ident-equiv-congruence-on-var

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

Theorem: update-var-aux-of-value-fix-val

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

Theorem: update-var-aux-value-equiv-congruence-on-val

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

Theorem: update-var-aux-of-scope-list-fix-scopes

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

Theorem: update-var-aux-scope-list-equiv-congruence-on-scopes

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

Function: update-var

(defun update-var (var val compst)
 (declare (xargs :guard (and (identp var)
                             (valuep val)
                             (compustatep compst))))
 (declare (xargs :guard (> (compustate-frames-number compst)
                           0)))
 (let ((__function__ 'update-var))
   (declare (ignorable __function__))
   (b* ((frame (top-frame compst))
        (scopes (frame->scopes frame))
        (autop (var-in-scopes-p var scopes))
        ((when autop)
         (b* ((new-scopes (update-var-aux var val scopes))
              (new-frame (change-frame frame
                                       :scopes new-scopes)))
           (push-frame new-frame (pop-frame compst))))
        (static (compustate->static compst))
        (new-static (omap::update (ident-fix var)
                                  (remove-flexible-array-member val)
                                  static)))
     (change-compustate compst
                        :static new-static))))

Theorem: compustatep-of-update-var

(defthm compustatep-of-update-var
  (b* ((new-compst (update-var var val compst)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: update-var-of-ident-fix-var

(defthm update-var-of-ident-fix-var
  (equal (update-var (ident-fix var) val compst)
         (update-var var val compst)))

Theorem: update-var-ident-equiv-congruence-on-var

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

Theorem: update-var-of-value-fix-val

(defthm update-var-of-value-fix-val
  (equal (update-var var (value-fix val) compst)
         (update-var var val compst)))

Theorem: update-var-value-equiv-congruence-on-val

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

Theorem: update-var-of-compustate-fix-compst

(defthm update-var-of-compustate-fix-compst
  (equal (update-var var val (compustate-fix compst))
         (update-var var val compst)))

Theorem: update-var-compustate-equiv-congruence-on-compst

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