Cause fatal warnings if function calls are in unacceptable places.
(vl-check-bad-funcalls ctx exprs description warnings) → (mv okp warnings)
If these expressions contain any function calls, we add a fatal
warning and set
Which expressions should we allow to involve function calls? Well, clearly we want to allow function calls on the right-hand sides of assignments, and in the inputs to module and gate instances. But there are many other places where we clearly don't want to allow function calls, for instance what would it mean to assign to a function call, or to connect a function call to the output port of a module? We think these things are crazy and should not be allowed.
In other contexts the right thing to do is less clear. Should we expand function calls in a delay statement? In an parameter-argument? In a wire's range declaration?
These things probably make some sense, especially if the function is being applied to constant arguments and can be completely resolved at "elaboration time." But it does not seem like it makes any sense for functions that are dealing with wires. At any rate, for now I am not going to try to support this sort of thing, because (1) handling all of this properly raises so many questions regarding widths, etc., and (2) it seems more elaborate than we really need to support.
The moral of the story is:
Some day, we might add better support for constant functions, and some of this could be changed, but there'd better be a really good reason to do so since it will be so tricky to get right.
Function:
(defun vl-check-bad-funcalls (ctx exprs description warnings) (declare (xargs :guard (and (vl-context-p ctx) (vl-exprlist-p exprs) (stringp description) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-check-bad-funcalls)) (declare (ignorable __function__)) (b* (((unless (vl-exprlist-has-funcalls exprs)) (mv t (ok))) (fns-called (vl-exprlist-funnames exprs))) (mv nil (fatal :type :vl-bad-funcall :msg "In ~a0, function calls in ~s1 are not supported, but ~ we found ~s2 of ~&3." :args (list ctx description (if (vl-plural-p fns-called) "calls" "a call") (mergesort fns-called)))))))
Theorem:
(defthm booleanp-of-vl-check-bad-funcalls.okp (b* (((mv ?okp ?warnings) (vl-check-bad-funcalls ctx exprs description warnings))) (booleanp okp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-check-bad-funcalls.warnings (b* (((mv ?okp ?warnings) (vl-check-bad-funcalls ctx exprs description warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)