Potential slowdown for program-mode updates to stobjs or arrays

You may see a warning like this:

ACL2 Warning [Invariant-risk] in MY-FUNCTION: Invariant-risk has been detected for a call of function MY-FUNCTION (as possibly leading to an ill-guarded call of UPDATE-FLD); see :DOC invariant-risk.

Such warnings indicate potential slowdown due to aggressive protection by ACL2 against either:

- writing a value of the wrong type to a stobj field; or
- performing an out-of-bounds write to an ACL2 array.

Whenever a `program`-mode function call can perhaps lead to
such a write, guard-checking is performed by ACL2, even though the
normal expectation is to execute without such checks in Common Lisp; see evaluation. Consider the following example.

(defstobj st (fld :type integer :initially 0)) (defun f (n st) (declare (xargs :stobjs st :guard (integerp n))) (update-fld n st)) ; This :program-mode wrapper for f fails to require (integerp n): (defun g (n st) (declare (xargs :stobjs st :mode :program)) (f n st)) ; Produces an invariant-risk warning: (g 3 st) ; Produces an invariant-risk warning and a guard violation: (g 'a st)

Each of the two calls of

We may say that such `program`-mode functions have
invariant-risk. Because of how the ``aggressive protection'' discussed above
is implemented, recursive calls of invariant-risk functions are not traced;
see trace$.

There are two general methods for avoiding such warnings: at runtime with
`set-check-invariant-risk`, and at definition time with `set-register-invariant-risk`. We describe each briefly below. For more
information follow the links just above to their respective documentation
topics. For yet more detail about invariant-risk see invariant-risk-details. For tools that may help find sources of
invariant-risk, see community-book

You can avoid seeing warnings like the one displayed above (without affecting the check that is actually performed) by evaluating either one of the following forms.

(set-check-invariant-risk t) (set-inhibit-warnings "invariant-risk")

You can also replace such warnings by errors:

(set-check-invariant-risk :error)

Evaluate

On occasion you may define functions that you know avoid invariant-risk
danger, even though ACL2 designates those functions as having invariant-risk.
Rather than removing invariant-risk checking for *all* functions at
runtime with `set-check-invariant-risk`, it is probably much safer to
remove it only for the functions in a given book or `encapsulate` event.
See set-register-invariant-risk for how to do that.

- Set-check-invariant-risk
- Affect certain program-mode updates to stobjs or arrays
- Invariant-risk-details
- More details about invariant-risk
- Set-register-invariant-risk
- Avoid invariant-risk checking for specified functions