• 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
        • Representation
        • Transformation-tools
          • Deftrans
          • Simpadd0
          • Split-fn
          • Copy-fn
          • Specialize
            • Paramdecl-list-remove-param-by-ident
            • Specialize-fundef
            • Specialize-extdecl
            • Specialize-filepath-transunit-map
            • Specialize-transunit-ensemble
            • Specialize-extdecl-list
            • Paramdecl-to-decl
            • Specialize-transunit
            • Ident-from-paramdecl
          • Rename
          • Splitgso
          • Utilities
        • 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

• Specialize

Specialize-fundef

Transform a function definition.

Signature

(specialize-fundef fundef target-fn target-param const) 
  → 
(mv found new-fundef)

Arguments

fundef — Guard (fundefp fundef).

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

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

const — Guard (exprp const).

Returns

found — Type (booleanp found).

new-fundef — Type (fundefp new-fundef).

Definitions and Theorems

Function: specialize-fundef

(defun specialize-fundef (fundef target-fn target-param const)
 (declare (xargs :guard (and (fundefp fundef)
                             (identp target-fn)
                             (identp target-param)
                             (exprp const))))
 (let ((__function__ 'specialize-fundef))
  (declare (ignorable __function__))
  (b* (((fundef fundef) fundef)
       ((declor fundef.declor) fundef.declor))
   (stmt-case
    fundef.body
    :compound
    (dirdeclor-case
     fundef.declor.direct :function-params
     (b*
      (((unless
            (equal target-fn
                   (dirdeclor-get-ident fundef.declor.direct.decl)))
        (mv nil (fundef-fix fundef)))
       ((mv success new-params removed-param)
        (paramdecl-list-remove-param-by-ident
             fundef.declor.direct.params
             target-param))
       ((unless success)
        (prog2$ (raise "Function ~x0 did not have a parameter ~x1"
                       target-fn target-param)
                (mv nil (fundef-fix fundef))))
       (dirdeclor-params
            (make-dirdeclor-function-params
                 :decl fundef.declor.direct.decl
                 :params new-params
                 :ellipsis fundef.declor.direct.ellipsis))
       ((mv - decl)
        (paramdecl-to-decl removed-param (initer-single const))))
      (mv t
          (make-fundef
               :extension fundef.extension
               :spec fundef.spec
               :declor (make-declor :pointers fundef.declor.pointers
                                    :direct dirdeclor-params)
               :decls fundef.decls
               :body (stmt-compound (cons (block-item-decl decl)
                                          fundef.body.items)))))
     :otherwise (mv nil (fundef-fix fundef)))
    :otherwise
    (prog2$
     (raise "Function definition body is not a compound statement.")
     (mv nil (fundef-fix fundef)))))))

Theorem: booleanp-of-specialize-fundef.found

(defthm booleanp-of-specialize-fundef.found
  (b* (((mv ?found ?new-fundef)
        (specialize-fundef fundef target-fn target-param const)))
    (booleanp found))
  :rule-classes :rewrite)

Theorem: fundefp-of-specialize-fundef.new-fundef

(defthm fundefp-of-specialize-fundef.new-fundef
  (b* (((mv ?found ?new-fundef)
        (specialize-fundef fundef target-fn target-param const)))
    (fundefp new-fundef))
  :rule-classes :rewrite)