		Search-engine friendly clone of the ACL2 documentation.

Expand-functions

Vl-module-expand-functions

Eliminate functions from a module by inlining functions wherever they are called.

Signature
(vl-module-expand-functions x ss) → new-x
Arguments: x — Guard (vl-module-p x).; ss — Guard (vl-scopestack-p ss).
Returns: new-x — Type (vl-module-p new-x).

This is the top-level routine to eliminates functions from a module. We walk over the expressions in the module. For each function call, we find the called function and process its body into a template consisting of a series of variable declarations and assignments. We then add the contents of that template to the module, with names mangled so as not to conflict with existing names.

We used to preprocess all of the function declarations in the module into templates before walking over the expressions. This could be a performance win because each function is only turned into a template once. However, this couldn't account for functions that were declared in the global scope or imported from packages. For the moment we will just expand each function however many times it is called. If this negatively impacts performance, consider memoizing vl-fnname->template.

Definitions and Theorems

Function: vl-module-expand-functions

(defun vl-module-expand-functions (x ss)
 (declare (xargs :guard (and (vl-module-p x)
                             (vl-scopestack-p ss))))
 (let ((__function__ 'vl-module-expand-functions))
  (declare (ignorable __function__))
  (b*
   ((x (vl-module-fix x))
    ((vl-module x) x)
    ((when (vl-module->hands-offp x)) x)
    (ss (vl-scopestack-push x ss))
    (nf (vl-starting-namefactory x))
    (warnings x.warnings)
    (vacc nil)
    (aacc nil)
    ((mv okp1 warnings nf vacc aacc
         ports portdecls vardecls paramdecls)
     (vl-module-expand-calls-in-decls
          x.ports x.portdecls x.vardecls
          x.paramdecls ss nf vacc aacc warnings))
    ((mv okp2 warnings nf vacc aacc assigns
         modinsts gateinsts alwayses initials)
     (vl-module-expand-calls-in-nondecls
          x.assigns
          x.modinsts x.gateinsts x.alwayses
          x.initials ss nf vacc aacc warnings))
    (- (vl-free-namefactory nf))
    (okp (and okp1 okp2))
    ((unless okp)
     (change-vl-module x :warnings warnings))
    (x-prime (change-vl-module
                  x
                  :ports ports
                  :portdecls portdecls
                  :vardecls (append-without-guard vacc vardecls)
                  :paramdecls paramdecls
                  :fundecls nil
                  :assigns (append-without-guard aacc assigns)
                  :modinsts modinsts
                  :gateinsts gateinsts
                  :alwayses alwayses
                  :initials initials
                  :warnings warnings))
    (allexprs (vl-module-allexprs x-prime))
    ((when (vl-exprlist-has-funcalls allexprs))
     (b*
      ((w
        (make-vl-warning
         :type :vl-programming-error
         :msg
         "In module ~m0, there are still function calls after ~
                       successfully expanding functions?  Found calls to ~&1."
         :args (list x.name
                     (mergesort (vl-exprlist-funnames allexprs)))
         :fn 'vl-module-expand-functions
         :fatalp t)))
      (change-vl-module x-prime
                        :warnings (cons w warnings)))))
   x-prime)))

Theorem: vl-module-p-of-vl-module-expand-functions

(defthm vl-module-p-of-vl-module-expand-functions
  (b* ((new-x (vl-module-expand-functions x ss)))
    (vl-module-p new-x))
  :rule-classes :rewrite)

Subtopics

Vl-module-expand-calls-in-nondecls
Vl-module-expand-calls-in-decls
Vl-plainarglist-expand-function-calls: Expand function calls throughout a vl-plainarglist-p
Vl-plainarg-expand-function-calls: Expand function calls throughout a vl-plainarg-p
Vl-vardecllist-expand-function-calls: Expand function calls throughout a vl-vardecllist-p
Vl-portdecllist-expand-function-calls: Expand function calls throughout a vl-portdecllist-p
Vl-paramdecllist-expand-function-calls: Expand function calls throughout a vl-paramdecllist-p
Vl-modinstlist-expand-function-calls: Expand function calls throughout a vl-modinstlist-p
Vl-initiallist-expand-function-calls: Expand function calls throughout a vl-initiallist-p
Vl-gateinstlist-expand-function-calls: Expand function calls throughout a vl-gateinstlist-p
Vl-arguments-expand-function-calls: Expand function calls throughout a vl-arguments-p
Vl-alwayslist-expand-function-calls: Expand function calls throughout a vl-alwayslist-p
Vl-portlist-expand-function-calls: Expand function calls throughout a vl-portlist-p
Vl-modinst-expand-function-calls: Expand function calls throughout a vl-modinst-p
Vl-gateinst-expand-function-calls: Expand function calls throughout a vl-gateinst-p
Vl-paramdecl-expand-function-calls: Expand function calls throughout a vl-paramdecl-p
Vl-initial-expand-function-calls: Expand function calls throughout a vl-initial-p
Vl-vardecl-expand-function-calls: Expand function calls throughout a vl-vardecl-p
Vl-portdecl-expand-function-calls: Expand function calls throughout a vl-portdecl-p
Vl-always-expand-function-calls: Expand function calls throughout a vl-always-p
Vl-port-expand-function-calls: Expand function calls throughout a vl-port-p