		Search-engine friendly clone of the ACL2 documentation.

Vl-fun-assignorder-okp

Vl-fun-assignorder-okp-aux

Main checking for vl-fun-assignorder-okp.

Signature
(vl-fun-assignorder-okp-aux x innames varnames written-vars read-vars read-inputs warnings function) → (mv okp warnings written-vars read-vars read-inputs)
Arguments: x — Assignments derived from a function's body.
Guard (vl-assignlist-p x).; innames — Names of all inputs to the functions.
Guard (string-listp innames).; varnames — Names of all variables declared in the function.
Guard (string-listp varnames).; written-vars — Accumulator. Names of all variables written to so far. This lets us check that all variables are written before they are read, and that no variable is written to more than once.
Guard (string-listp written-vars).; read-vars — Accumulator. Names of all variables we've read from so far. This is useful for reporting unused variables.
Guard (string-listp read-vars).; read-inputs — Accumulator. Names all the inputs we've read from so far. This is useful for reporting unused inputs.
Guard (string-listp read-inputs).; warnings — Ordinary warnings accumulator.
Guard (vl-warninglist-p warnings).; function — The function itself, mostly useful as a context for error messages, but also gives us the function's name so we can check that the function's name is the last thing written to and isn't written to until the end.
Guard (vl-fundecl-p function).
Returns: okp — Type (booleanp okp).; warnings — Type (vl-warninglist-p warnings).; written-vars — Type (string-listp written-vars), given the guard.; read-vars — Type (string-listp read-vars), given the guard.; read-inputs — Type (string-listp read-inputs), given the guard.

Definitions and Theorems

Function: vl-fun-assignorder-okp-aux

(defun vl-fun-assignorder-okp-aux
       (x innames varnames written-vars
          read-vars read-inputs warnings function)
 (declare (xargs :guard (and (vl-assignlist-p x)
                             (string-listp innames)
                             (string-listp varnames)
                             (string-listp written-vars)
                             (string-listp read-vars)
                             (string-listp read-inputs)
                             (vl-warninglist-p warnings)
                             (vl-fundecl-p function))))
 (let ((__function__ 'vl-fun-assignorder-okp-aux))
  (declare (ignorable __function__))
  (b*
   ((funname (vl-fundecl->name function))
    ((when (atom x))
     (mv
      nil
      (fatal
       :type :vl-bad-function-stmt
       :msg
       "In ~a0, there are no assignments.  There needs to at ~
                         least be an assignment to ~s1 to give it a return ~
                         value."
       :args (list function funname))
      written-vars read-vars read-inputs))
    ((vl-assign x1) (car x))
    ((unless (vl-idexpr-p x1.lvalue))
     (mv
      nil
      (fatal
       :type :vl-bad-function-stmt
       :msg
       "In ~a0, the assignment to ~a1 is too complex; we ~
                         only support assigning to a function's variables and ~
                         to its name directly; e.g., you cannot even write ~
                         things like foo[3:0] = 1.  This is overly ~
                         restrictive, and we can work on improving it if ~
                         necessary."
       :args (list function x1.lvalue))
      written-vars read-vars read-inputs))
    (lhs-name (vl-idexpr->name x1.lvalue))
    (rhs-names (vl-expr-names x1.expr))
    (rhs-var-names (intersection-equal rhs-names varnames))
    (rhs-unwritten-vars
         (set-difference-equal rhs-var-names written-vars))
    ((when rhs-unwritten-vars)
     (mv
      nil
      (fatal
       :type :vl-bad-function-stmt
       :msg
       "In ~a0, assignment to ~a1 involves the variable~s2 ~
                         ~&3, which ~s4 not yet been assigned at this point ~
                         in the function.  We do not allow this because it ~
                         can lead to very odd behavior when there are ~
                         multiple calls of the function."
       :args (list function x1.lvalue
                   (if (vl-plural-p rhs-unwritten-vars)
                       "s"
                     "")
                   rhs-unwritten-vars
                   (if (vl-plural-p rhs-unwritten-vars)
                       "have"
                     "has")))
      written-vars read-vars read-inputs))
    (read-vars (append rhs-var-names read-vars))
    (read-inputs (append (intersection-equal innames rhs-names)
                         read-inputs))
    ((when (atom (cdr x)))
     (if (equal lhs-name funname)
         (mv t (ok)
             written-vars read-vars read-inputs)
      (mv
       nil
       (fatal
        :type :vl-bad-function-stmt
        :msg
        "In ~a0, the final assignment in ~s1 must be to ~
                           ~s1, but instead it is to ~a2."
        :args (list function funname x1.lvalue))
       written-vars read-vars read-inputs)))
    ((when (equal lhs-name funname))
     (mv
      nil
      (fatal
       :type :vl-bad-function-stmt
       :msg
       "In ~a0, assigning to ~a1 is not permitted except as ~
                         the very last statement in the function."
       :args (list function x1.lvalue))
      written-vars read-vars read-inputs))
    ((unless (member-equal lhs-name varnames))
     (mv
      nil
      (fatal
       :type :vl-bad-function-stmt
       :msg
       "In ~a0, the assignment to ~a1 is not permitted; we ~
                         only allow assignments to the function's variables ~
                         and its name."
       :args (list function x1.lvalue))
      written-vars read-vars read-inputs))
    ((when (member-equal lhs-name written-vars))
     (mv
      nil
      (fatal
       :type :vl-bad-function-stmt
       :msg
       "In ~a0, we only allow a single assignment to each of ~
                         the function's variables, but ~a1 is written to more ~
                         than once."
       :args (list function x1.lvalue))
      written-vars read-vars read-inputs))
    (written-vars (cons lhs-name written-vars)))
   (vl-fun-assignorder-okp-aux
        (cdr x)
        innames varnames written-vars read-vars
        read-inputs warnings function))))

Theorem: booleanp-of-vl-fun-assignorder-okp-aux.okp

(defthm booleanp-of-vl-fun-assignorder-okp-aux.okp
  (b* (((mv ?okp ?warnings
            ?written-vars ?read-vars ?read-inputs)
        (vl-fun-assignorder-okp-aux
             x
             innames varnames written-vars read-vars
             read-inputs warnings function)))
    (booleanp okp))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-fun-assignorder-okp-aux.warnings

(defthm vl-warninglist-p-of-vl-fun-assignorder-okp-aux.warnings
  (b* (((mv ?okp ?warnings
            ?written-vars ?read-vars ?read-inputs)
        (vl-fun-assignorder-okp-aux
             x
             innames varnames written-vars read-vars
             read-inputs warnings function)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: string-listp-of-vl-fun-assignorder-okp-aux.written-vars

(defthm string-listp-of-vl-fun-assignorder-okp-aux.written-vars
  (implies (and (force (vl-assignlist-p x))
                (force (string-listp innames))
                (force (string-listp varnames))
                (force (string-listp written-vars))
                (force (string-listp read-vars))
                (force (string-listp read-inputs))
                (force (vl-warninglist-p warnings))
                (force (vl-fundecl-p function)))
           (b* (((mv ?okp ?warnings
                     ?written-vars ?read-vars ?read-inputs)
                 (vl-fun-assignorder-okp-aux
                      x
                      innames varnames written-vars read-vars
                      read-inputs warnings function)))
             (string-listp written-vars)))
  :rule-classes :rewrite)

Theorem: string-listp-of-vl-fun-assignorder-okp-aux.read-vars

(defthm string-listp-of-vl-fun-assignorder-okp-aux.read-vars
  (implies (and (force (vl-assignlist-p x))
                (force (string-listp innames))
                (force (string-listp varnames))
                (force (string-listp written-vars))
                (force (string-listp read-vars))
                (force (string-listp read-inputs))
                (force (vl-warninglist-p warnings))
                (force (vl-fundecl-p function)))
           (b* (((mv ?okp ?warnings
                     ?written-vars ?read-vars ?read-inputs)
                 (vl-fun-assignorder-okp-aux
                      x
                      innames varnames written-vars read-vars
                      read-inputs warnings function)))
             (string-listp read-vars)))
  :rule-classes :rewrite)

Theorem: string-listp-of-vl-fun-assignorder-okp-aux.read-inputs

(defthm string-listp-of-vl-fun-assignorder-okp-aux.read-inputs
  (implies (and (force (vl-assignlist-p x))
                (force (string-listp innames))
                (force (string-listp varnames))
                (force (string-listp written-vars))
                (force (string-listp read-vars))
                (force (string-listp read-inputs))
                (force (vl-warninglist-p warnings))
                (force (vl-fundecl-p function)))
           (b* (((mv ?okp ?warnings
                     ?written-vars ?read-vars ?read-inputs)
                 (vl-fun-assignorder-okp-aux
                      x
                      innames varnames written-vars read-vars
                      read-inputs warnings function)))
             (string-listp read-inputs)))
  :rule-classes :rewrite)