Main checking for vl-fun-assignorder-okp.
(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)
Function:
(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:
(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:
(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:
(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:
(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:
(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)