• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
        • Syntax-for-tools
        • Atc
        • Language
          • Abstract-syntax
          • Integer-ranges
          • Dynamic-semantics
          • Static-semantics
          • Grammar
          • Integer-formats
          • Types
          • Portable-ascii-identifiers
          • Values
          • Integer-operations
          • Computation-states
            • Write-object
            • Objdesign-of-var
            • Compustate-scopes-numbers
            • Create-var
            • Read-object
            • Compustate
            • Frame
            • Enter-scope
            • Compustate-scopes-numbers-aux
            • Compustate-option
            • Push-frame
            • Exit-scope
            • Compustate-frames-number
            • Compustate-option-result
            • Scope-list-result
            • Pop-frame
            • Compustate-result
            • Scope-result
            • Compustate-top-frame-scopes-number
            • Top-frame
            • Heap
            • Scope
            • Scope-list
            • Frame-list
          • Object-designators
          • Implementation-environments
          • Operations
          • Errors
          • Tag-environments
          • Function-environments
          • Character-sets
          • Flexible-array-member-removal
          • Arithmetic-operations
          • Pointer-operations
          • Bytes
          • Keywords
          • Real-operations
          • Array-operations
          • Scalar-operations
          • Structure-operations
        • Representation
        • Transformation-tools
        • Pack
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Computation-states

Objdesign-of-var

Object designator of a variable.

Signature

(objdesign-of-var var compst) → objdes?

Arguments

var — Guard (identp var).

compst — Guard (compustatep compst).

Returns

objdes? — Type (objdesign-optionp objdes?).

Given the name of a variable in scope, there is an object designator for the variable, which can be found by looking up the variable in the computation states, according to the scoping rules of C.

If there are frames in the computation state, we look in the scopes of the top frame, from innermost (leftmost) scope to outermost (rightmost) scope; note that we pass the index of the top frame to the recursive function, so it can be put into the object designator. We do not look at other frames, because the variables in other frames are not in scope when running in the top frame. If the variable is not found in the top frame, we look for it in static storage.

If there are no frames in the computation state, we look in static storage.

If the variable is not found anywhere, we return nil, which means that the variable is not in scope.

Definitions and Theorems

Function: objdesign-of-var-aux

(defun objdesign-of-var-aux (var frame scopes)
  (declare (xargs :guard (and (identp var)
                              (natp frame)
                              (scope-listp scopes))))
  (let ((__function__ 'objdesign-of-var-aux))
    (declare (ignorable __function__))
    (b* (((when (endp scopes)) nil)
         (scope (car scopes))
         (var+val? (omap::assoc (ident-fix var)
                                (scope-fix scope)))
         ((when (consp var+val?))
          (make-objdesign-auto :name var
                               :frame frame
                               :scope (1- (len scopes)))))
      (objdesign-of-var-aux var frame (cdr scopes)))))

Theorem: objdesign-optionp-of-objdesign-of-var-aux

(defthm objdesign-optionp-of-objdesign-of-var-aux
  (b* ((objdes? (objdesign-of-var-aux var frame scopes)))
    (objdesign-optionp objdes?))
  :rule-classes :rewrite)

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

(defthm objdesign-of-var-aux-of-ident-fix-var
  (equal (objdesign-of-var-aux (ident-fix var)
                               frame scopes)
         (objdesign-of-var-aux var frame scopes)))

Theorem: objdesign-of-var-aux-ident-equiv-congruence-on-var

(defthm objdesign-of-var-aux-ident-equiv-congruence-on-var
  (implies (ident-equiv var var-equiv)
           (equal (objdesign-of-var-aux var frame scopes)
                  (objdesign-of-var-aux var-equiv frame scopes)))
  :rule-classes :congruence)

Theorem: objdesign-of-var-aux-of-nfix-frame

(defthm objdesign-of-var-aux-of-nfix-frame
  (equal (objdesign-of-var-aux var (nfix frame)
                               scopes)
         (objdesign-of-var-aux var frame scopes)))

Theorem: objdesign-of-var-aux-nat-equiv-congruence-on-frame

(defthm objdesign-of-var-aux-nat-equiv-congruence-on-frame
  (implies (acl2::nat-equiv frame frame-equiv)
           (equal (objdesign-of-var-aux var frame scopes)
                  (objdesign-of-var-aux var frame-equiv scopes)))
  :rule-classes :congruence)

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

(defthm objdesign-of-var-aux-of-scope-list-fix-scopes
  (equal (objdesign-of-var-aux var frame (scope-list-fix scopes))
         (objdesign-of-var-aux var frame scopes)))

Theorem: objdesign-of-var-aux-scope-list-equiv-congruence-on-scopes

(defthm objdesign-of-var-aux-scope-list-equiv-congruence-on-scopes
  (implies (scope-list-equiv scopes scopes-equiv)
           (equal (objdesign-of-var-aux var frame scopes)
                  (objdesign-of-var-aux var frame scopes-equiv)))
  :rule-classes :congruence)

Theorem: objdesign-kind-of-objdesign-of-var-aux

(defthm objdesign-kind-of-objdesign-of-var-aux
  (b* ((objdes (objdesign-of-var-aux var frame scopes)))
    (implies objdes
             (equal (objdesign-kind objdes) :auto))))

Theorem: objdesign-auto->scope-of-objdesign-of-var-aux-upper-bound

(defthm objdesign-auto->scope-of-objdesign-of-var-aux-upper-bound
  (b* ((objdes (objdesign-of-var-aux var frame scopes)))
    (implies objdes
             (< (objdesign-auto->scope objdes)
                (len scopes))))
  :rule-classes :linear)

Theorem: objdesign-of-var-aux-lemma

(defthm objdesign-of-var-aux-lemma
 (b*
  ((objdes (objdesign-of-var-aux var frame scopes))
   (pair
     (omap::assoc (objdesign-auto->name objdes)
                  (scope-fix (nth (- (1- (len scopes))
                                     (objdesign-auto->scope objdes))
                                  scopes)))))
  (implies objdes
           (and (objdesign-case objdes :auto)
                (equal (objdesign-auto->name objdes)
                       (ident-fix var))
                (equal (objdesign-auto->frame objdes)
                       (nfix frame))
                (< (objdesign-auto->scope objdes)
                   (len scopes))
                (< (- (1- (len scopes))
                      (objdesign-auto->scope objdes))
                   (len scopes))
                (consp pair)
                (valuep (cdr pair))))))

Function: objdesign-of-var

(defun objdesign-of-var (var compst)
 (declare (xargs :guard (and (identp var)
                             (compustatep compst))))
 (let ((__function__ 'objdesign-of-var))
  (declare (ignorable __function__))
  (b*
   ((objdes?
     (and
        (> (compustate-frames-number compst) 0)
        (objdesign-of-var-aux var
                              (1- (compustate-frames-number compst))
                              (frame->scopes (top-frame compst)))))
    ((when objdes?) objdes?)
    (var+val? (omap::assoc (ident-fix var)
                           (compustate->static compst))))
   (and (consp var+val?)
        (objdesign-static var)))))

Theorem: objdesign-optionp-of-objdesign-of-var

(defthm objdesign-optionp-of-objdesign-of-var
  (b* ((objdes? (objdesign-of-var var compst)))
    (objdesign-optionp objdes?))
  :rule-classes :rewrite)

Theorem: objdesign-kind-of-objdesign-of-var

(defthm objdesign-kind-of-objdesign-of-var
  (b* ((objdes (objdesign-of-var var compst)))
    (implies (and objdes
                  (> (compustate-frames-number compst) 0))
             (member-equal (objdesign-kind objdes)
                           '(:auto :static)))))

Theorem: objdesign-of-var-of-ident-fix-var

(defthm objdesign-of-var-of-ident-fix-var
  (equal (objdesign-of-var (ident-fix var)
                           compst)
         (objdesign-of-var var compst)))

Theorem: objdesign-of-var-ident-equiv-congruence-on-var

(defthm objdesign-of-var-ident-equiv-congruence-on-var
  (implies (ident-equiv var var-equiv)
           (equal (objdesign-of-var var compst)
                  (objdesign-of-var var-equiv compst)))
  :rule-classes :congruence)

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

(defthm objdesign-of-var-of-compustate-fix-compst
  (equal (objdesign-of-var var (compustate-fix compst))
         (objdesign-of-var var compst)))

Theorem: objdesign-of-var-compustate-equiv-congruence-on-compst

(defthm objdesign-of-var-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (objdesign-of-var var compst)
                  (objdesign-of-var var compst-equiv)))
  :rule-classes :congruence)