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-fun-assignorder-okp x warnings function) → (mv okp warnings)
The checks we perform are intended to ensure that it is legitimate to convert this series of blocking assignments into wiring:
We also take this opportunity to issue non-fatal warnings about unused variables and inputs.
Function:
(defun vl-fun-assignorder-okp (x warnings function) (declare (xargs :guard (and (vl-assignlist-p x) (vl-warninglist-p warnings) (vl-fundecl-p function)))) (let ((__function__ 'vl-fun-assignorder-okp)) (declare (ignorable __function__)) (b* ((vardecls (vl-remove-fake-function-vardecls (vl-fundecl->vardecls function))) (varnames (vl-vardecllist->names vardecls)) (innames (vl-portdecllist->names (vl-fundecl->portdecls function))) ((mv okp warnings written-vars read-vars read-inputs) (vl-fun-assignorder-okp-aux x innames varnames nil nil nil warnings function)) ((unless okp) (mv nil warnings)) (innames (mergesort innames)) (varnames (mergesort varnames)) (read-inputs (mergesort read-inputs)) (read-vars (mergesort read-vars)) (written-vars (mergesort written-vars)) (unread-inputs (difference innames read-inputs)) (unread-vars (difference varnames read-vars)) (unwritten-vars (difference varnames written-vars)) (spurious-vars (intersect unread-vars unwritten-vars)) (unread-vars (difference unread-vars spurious-vars)) (unwritten-vars (difference unwritten-vars spurious-vars)) (unread-all (union unread-vars unread-inputs)) (spurious-sep (if (or unread-all unwritten-vars) "; " "")) (spurious-msg (cond ((not spurious-vars) "") ((vl-plural-p spurious-vars) (cat "~&1 are never mentioned" spurious-sep)) (t (cat "~&1 is never mentioned" spurious-sep)))) (unread-sep (if unwritten-vars "; " "")) (unread-msg (cond ((not unread-all) "") ((vl-plural-p unread-all) (cat "~&2 are never read" unread-sep)) (t (cat "~&2 is never read" unread-sep)))) (unwritten-msg (cond ((not unwritten-vars) "") ((vl-plural-p unwritten-vars) "~&3 are never written") (t "~&3 is never written"))) (warnings (if (or spurious-vars unread-all unwritten-vars) (warn :type :vl-warn-function-vars :msg (cat "In ~a0, " spurious-msg unread-msg unwritten-msg ".") :args (list function spurious-vars unread-all unwritten-vars)) (ok)))) (mv t warnings))))
Theorem:
(defthm booleanp-of-vl-fun-assignorder-okp.okp (b* (((mv ?okp ?warnings) (vl-fun-assignorder-okp x warnings function))) (booleanp okp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-fun-assignorder-okp.warnings (b* (((mv ?okp ?warnings) (vl-fun-assignorder-okp x warnings function))) (vl-warninglist-p warnings)) :rule-classes :rewrite)