		Search-engine friendly clone of the ACL2 documentation.

Vl-funbody-to-assignments

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.

Signature
(vl-fun-assignorder-okp x warnings function) → (mv okp warnings)
Arguments: x — Assignments derived from a function's body.
Guard (vl-assignlist-p x).; warnings — Ordinary warnings accumulator.
Guard (vl-warninglist-p warnings).; function — The function itself: used as a context for error messages, and also to determine the function's name to check the final assignment.
Guard (vl-fundecl-p function).
Returns: okp — Type (booleanp okp).; warnings — Type (vl-warninglist-p warnings).

The checks we perform are intended to ensure that it is legitimate to convert this series of blocking assignments into wiring:

Write-before-read ensures that there is no possible interaction with previous function calls, or other "simultaneous" function calls.
No multiple writes ensures that we won't be putting multiple drivers on some wire when we convert the assignments into continuous assignments; we could probably drop this restriction easily by doing some kind of renaming.
Writing to the function at the end seems like a basic reasonableness criteria.

We also take this opportunity to issue non-fatal warnings about unused variables and inputs.

Definitions and Theorems

Function: vl-fun-assignorder-okp

(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: booleanp-of-vl-fun-assignorder-okp.okp

(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: vl-warninglist-p-of-vl-fun-assignorder-okp.warnings

(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)

Subtopics

Vl-fun-assignorder-okp-aux: Main checking for vl-fun-assignorder-okp.