Vl-funbody-to-assignments
Transform a function's body into a list of assignment statements if
it is safe to do so.
- Signature
(vl-funbody-to-assignments x warnings)
→
(mv successp warnings assigns)
- Arguments
- x — Function to convert.
Guard (vl-fundecl-p x).
- warnings — Ordinary warnings accumulator.
Guard (vl-warninglist-p warnings).
- Returns
- successp — Type (booleanp successp).
- warnings — Type (vl-warninglist-p warnings).
- assigns — Type (vl-assignlist-p assigns).
This is the top-level function for converting function bodies into
assignments.
If x is a function that we think we can safely support, we convert its
body into a list of assignments which capture its effect. This is a fairly
elaborate process with a lot of checking to make sure things are reasonable.
At a high level:
- We start by checking that the function's body isn't prohibited because of
one of the Function Rules in 10.4.4 (see vl-fun-stmt-okp). This is
important in order to justify our use of rewriting in the next step.
- We then rewrite the function's body using our ordinary stmtrewrite
functions. This may help to flatten out nested sub-blocks and generally just
helps to expand the class of functions we can support.
- We then try to convert the body into a simple vl-assignlist-p using
a helper routine, vl-funbody-to-assignments-aux. This only works if the
rewritten function is nothing more than a list of blocking assignments.
- If that was successful, we check this sequence of assignments to make sure
that it follows several rules (write-before-read, don't write twice, etc.) to
ensure that it is safe to convert the function into a series of continuous
assignments; see vl-fun-assignorder-okp for details.
If all of this works and everything looks okay, we successfully return the
generated list of assignments. Otherwise we fail with fatal warnings.
Definitions and Theorems
Function: vl-funbody-to-assignments
(defun vl-funbody-to-assignments (x warnings)
(declare (xargs :guard (and (vl-fundecl-p x)
(vl-warninglist-p warnings))))
(let ((__function__ 'vl-funbody-to-assignments))
(declare (ignorable __function__))
(b*
((body (vl-fundecl->body x))
((mv successp warnings)
(vl-fun-stmt-okp body warnings x))
((unless successp)
(mv nil warnings nil))
((mv warnings body)
(vl-stmt-rewrite body 1000 warnings))
(body-as-stmt-list
(if (and (not (vl-atomicstmt-p body))
(vl-blockstmt-p body)
(vl-blockstmt->sequentialp body)
(not (vl-blockstmt->name body))
(not (vl-blockstmt->vardecls body))
(not (vl-blockstmt->paramdecls body))
(not (vl-blockstmt->imports body)))
(vl-blockstmt->stmts body)
(list body)))
((mv okp warnings assigns)
(vl-funbody-to-assignments-aux body-as-stmt-list warnings x))
((unless okp) (mv nil warnings nil))
((mv okp warnings)
(vl-fun-assignorder-okp assigns warnings x))
((unless okp) (mv nil warnings nil)))
(mv t warnings assigns))))
Theorem: booleanp-of-vl-funbody-to-assignments.successp
(defthm booleanp-of-vl-funbody-to-assignments.successp
(b* (((mv ?successp ?warnings ?assigns)
(vl-funbody-to-assignments x warnings)))
(booleanp successp))
:rule-classes :type-prescription)
Theorem: vl-warninglist-p-of-vl-funbody-to-assignments.warnings
(defthm vl-warninglist-p-of-vl-funbody-to-assignments.warnings
(b* (((mv ?successp ?warnings ?assigns)
(vl-funbody-to-assignments x warnings)))
(vl-warninglist-p warnings))
:rule-classes :rewrite)
Theorem: vl-assignlist-p-of-vl-funbody-to-assignments.assigns
(defthm vl-assignlist-p-of-vl-funbody-to-assignments.assigns
(b* (((mv ?successp ?warnings ?assigns)
(vl-funbody-to-assignments x warnings)))
(vl-assignlist-p assigns))
:rule-classes :rewrite)
Subtopics
- Vl-fun-assignorder-okp
- Ensure that the assignments from a function's body always write to
variables before they read from them, never write to a variable twice, and end
with a write to the function's name.
- Vl-funbody-to-assignments-aux
- Try to convert a list of statements that make up a function's body
into a vl-assignlist-p.