• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
        • Syntax-for-tools
        • Atc
        • Transformation-tools
          • Simpadd0
          • Proof-generation
          • Split-gso
          • Wrap-fn
            • Wrap-fn-implementation
              • Initdeclor-list-wrap-fn-add-wrapper-def
              • Declor-wrap-fn-add-wrapper-def
              • Fundef-wrap-fn-add-wrapper-def
              • Extdecl-wrap-fn-add-wrapper-def
              • Decl-wrap-fn-add-wrapper-def
              • Extdecl-list-wrap-fn
              • Wrap-fn-process-param-declon-list-loop
              • Filepath-transunit-map-wrap-fn
              • Wrap-fn-process-param-declon-list
              • Transunit-wrap-fn
              • Transunit-ensemble-wrap-fn
              • Code-ensemble-wrap-fn
              • Code-ensemble-wrap-fn-multiple
              • Declor-wrap-fn-make-wrapper
              • Dirdeclor-wrap-fn-make-wrapper
              • Wrap-fn-input-processing
              • Wrap-fn-event-generation
          • Constant-propagation
          • Specialize
          • Split-fn
          • Split-fn-when
          • Split-all-gso
          • Copy-fn
          • Variables-in-computation-states
          • Rename
          • Utilities
          • Proof-generation-theorems
          • Input-processing
        • Language
        • Representation
        • Insertion-sort
        • Pack
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Wrap-fn-implementation

Extdecl-list-wrap-fn

Transform an external declaration list.

Signature

(extdecl-list-wrap-fn extdecls target-name wrapper-name? blacklist) 
  → 
(mv er? foundp found-satp extdecls$)

Arguments

extdecls — Guard (extdecl-listp extdecls).

target-name — Guard (identp target-name).

wrapper-name? — Guard (ident-optionp wrapper-name?).

blacklist — Guard (ident-setp blacklist).

Returns

er? — Type (maybe-msgp er?).

foundp — Type (booleanp foundp).

found-satp — Type (booleanp found-satp).

extdecls$ — Type (extdecl-listp extdecls$).

This searches for an external declaration matching the target function. When it finds one, it creates the function wrapper. It then substitutes the wrapper function for the original function in direct function calls occurring in the remainder of the translation unit.

Definitions and Theorems

Function: extdecl-list-wrap-fn

(defun extdecl-list-wrap-fn
       (extdecls target-name wrapper-name? blacklist)
 (declare (xargs :guard (and (extdecl-listp extdecls)
                             (identp target-name)
                             (ident-optionp wrapper-name?)
                             (ident-setp blacklist))))
 (declare (xargs :guard (extdecl-list-annop extdecls)))
 (b* (((reterr) nil nil nil)
      ((when (endp extdecls))
       (retok nil nil nil))
      (extdecl (extdecl-fix (first extdecls)))
      ((erp uid? wrapper? wrapper-name?$)
       (extdecl-wrap-fn-add-wrapper-def
            extdecl
            target-name wrapper-name? blacklist))
      ((when (and uid? wrapper?))
       (retok t t
              (list* extdecl (extdecl-fundef wrapper?)
                     (extdecl-list-rename-fn (rest extdecls)
                                             uid? wrapper-name?$))))
      ((erp foundp$ found-satp extdecls$)
       (extdecl-list-wrap-fn (rest extdecls)
                             target-name wrapper-name? blacklist)))
   (retok (if uid? t foundp$)
          found-satp (cons extdecl extdecls$))))

Theorem: maybe-msgp-of-extdecl-list-wrap-fn.er?

(defthm maybe-msgp-of-extdecl-list-wrap-fn.er?
  (b* (((mv ?er? ?foundp ?found-satp ?extdecls$)
        (extdecl-list-wrap-fn extdecls
                              target-name wrapper-name? blacklist)))
    (maybe-msgp er?))
  :rule-classes :rewrite)

Theorem: booleanp-of-extdecl-list-wrap-fn.foundp

(defthm booleanp-of-extdecl-list-wrap-fn.foundp
  (b* (((mv ?er? ?foundp ?found-satp ?extdecls$)
        (extdecl-list-wrap-fn extdecls
                              target-name wrapper-name? blacklist)))
    (booleanp foundp))
  :rule-classes :type-prescription)

Theorem: booleanp-of-extdecl-list-wrap-fn.found-satp

(defthm booleanp-of-extdecl-list-wrap-fn.found-satp
  (b* (((mv ?er? ?foundp ?found-satp ?extdecls$)
        (extdecl-list-wrap-fn extdecls
                              target-name wrapper-name? blacklist)))
    (booleanp found-satp))
  :rule-classes :type-prescription)

Theorem: extdecl-listp-of-extdecl-list-wrap-fn.extdecls$

(defthm extdecl-listp-of-extdecl-list-wrap-fn.extdecls$
  (b* (((mv ?er? ?foundp ?found-satp ?extdecls$)
        (extdecl-list-wrap-fn extdecls
                              target-name wrapper-name? blacklist)))
    (extdecl-listp extdecls$))
  :rule-classes :rewrite)

Theorem: true-listp-of-extdecl-list-wrap-fn.extdecls$

(defthm true-listp-of-extdecl-list-wrap-fn.extdecls$
  (b* (((mv ?er? ?foundp ?found-satp ?extdecls$)
        (extdecl-list-wrap-fn extdecls
                              target-name wrapper-name? blacklist)))
    (true-listp extdecls$))
  :rule-classes :type-prescription)

Theorem: extdecl-list-wrap-fn-of-extdecl-list-fix-extdecls

(defthm extdecl-list-wrap-fn-of-extdecl-list-fix-extdecls
 (equal (extdecl-list-wrap-fn (extdecl-list-fix extdecls)
                              target-name wrapper-name? blacklist)
        (extdecl-list-wrap-fn extdecls
                              target-name wrapper-name? blacklist)))

Theorem: extdecl-list-wrap-fn-extdecl-list-equiv-congruence-on-extdecls

(defthm
     extdecl-list-wrap-fn-extdecl-list-equiv-congruence-on-extdecls
 (implies
   (c$::extdecl-list-equiv extdecls extdecls-equiv)
   (equal
        (extdecl-list-wrap-fn extdecls
                              target-name wrapper-name? blacklist)
        (extdecl-list-wrap-fn extdecls-equiv
                              target-name wrapper-name? blacklist)))
 :rule-classes :congruence)

Theorem: extdecl-list-wrap-fn-of-ident-fix-target-name

(defthm extdecl-list-wrap-fn-of-ident-fix-target-name
 (equal (extdecl-list-wrap-fn extdecls (ident-fix target-name)
                              wrapper-name? blacklist)
        (extdecl-list-wrap-fn extdecls
                              target-name wrapper-name? blacklist)))

Theorem: extdecl-list-wrap-fn-ident-equiv-congruence-on-target-name

(defthm extdecl-list-wrap-fn-ident-equiv-congruence-on-target-name
 (implies
   (c$::ident-equiv target-name target-name-equiv)
   (equal (extdecl-list-wrap-fn extdecls
                                target-name wrapper-name? blacklist)
          (extdecl-list-wrap-fn extdecls target-name-equiv
                                wrapper-name? blacklist)))
 :rule-classes :congruence)

Theorem: extdecl-list-wrap-fn-of-ident-option-fix-wrapper-name?

(defthm extdecl-list-wrap-fn-of-ident-option-fix-wrapper-name?
 (equal (extdecl-list-wrap-fn extdecls target-name
                              (ident-option-fix wrapper-name?)
                              blacklist)
        (extdecl-list-wrap-fn extdecls
                              target-name wrapper-name? blacklist)))

Theorem: extdecl-list-wrap-fn-ident-option-equiv-congruence-on-wrapper-name?

(defthm
 extdecl-list-wrap-fn-ident-option-equiv-congruence-on-wrapper-name?
 (implies
   (c$::ident-option-equiv wrapper-name? wrapper-name?-equiv)
   (equal (extdecl-list-wrap-fn extdecls
                                target-name wrapper-name? blacklist)
          (extdecl-list-wrap-fn extdecls target-name
                                wrapper-name?-equiv blacklist)))
 :rule-classes :congruence)

Theorem: extdecl-list-wrap-fn-of-ident-set-fix-blacklist

(defthm extdecl-list-wrap-fn-of-ident-set-fix-blacklist
 (equal
      (extdecl-list-wrap-fn extdecls target-name
                            wrapper-name? (ident-set-fix blacklist))
      (extdecl-list-wrap-fn extdecls
                            target-name wrapper-name? blacklist)))

Theorem: extdecl-list-wrap-fn-ident-set-equiv-congruence-on-blacklist

(defthm extdecl-list-wrap-fn-ident-set-equiv-congruence-on-blacklist
 (implies
   (c$::ident-set-equiv blacklist blacklist-equiv)
   (equal (extdecl-list-wrap-fn extdecls
                                target-name wrapper-name? blacklist)
          (extdecl-list-wrap-fn extdecls target-name
                                wrapper-name? blacklist-equiv)))
 :rule-classes :congruence)