		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-computation-states

Add-var

Add a variable to a canonical representation of computation states.

Signature
(add-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 create-var, but it only operates on computation states with frames (so that the variable is added to the top scope of the top frame, and not to the static storage), and it never returns an error: it always adds the variable to the current scope. If there are frames, and the variable does not already exist in the current scope, this is equivalent to create-var, as proved later.

The reason for only operating on computation states with frames is that, during symbolic execution, we always have frames, because we are executing code in some function. Thus, during symbolic execution we are only interested in creating variables in the top scope of the top frame, never in static storage. In contrast, create-var is a more general function, that creates variables in both automatic and static storage.

Definitions and Theorems

Function: add-var

(defun add-var (var val compst)
  (declare (xargs :guard (and (identp var)
                              (valuep val)
                              (compustatep compst))))
  (declare (xargs :guard (> (compustate-frames-number compst)
                            0)))
  (let ((__function__ 'add-var))
    (declare (ignorable __function__))
    (b* ((frame (top-frame compst))
         (scopes (frame->scopes frame))
         (scope (car scopes))
         (new-scope (omap::update (ident-fix var)
                                  (remove-flexible-array-member val)
                                  scope))
         (new-scopes (cons new-scope (cdr scopes)))
         (new-frame (change-frame frame :scopes new-scopes))
         (new-compst (push-frame new-frame (pop-frame compst))))
      new-compst)))

Theorem: compustatep-of-add-var

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

Theorem: add-var-of-ident-fix-var

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

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

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

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

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

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

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

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

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

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

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