		Search-engine friendly clone of the ACL2 documentation.

Invariant-risk

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 g produces an "Invariant-risk" warning, and indeed guards are checked for the ensuing calls of f, causing a guard violation for the second call of g.

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 books/std/system/invariant-risk.lisp.

Controlling runtime checking for invariant-risk

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 (get-check-invariant-risk state) to see the current setting for invariant-risk checking. For details, including a dangerous way to remove invariant-risk checking completely at runtime, see set-check-invariant-risk.

Eliminating invariant-risk checking done by specific functions

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.

Subtopics

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