Affect certain program-mode updates to stobjs or arrays

See invariant-risk for an introduction to the notion of invariant-risk. Also see set-register-invariant-risk for a way to avoid marking a specific set of functions as having invariant-risk, which can be much safer than avoiding invariant-risk checking for all functions at runtime as described below.

Briefly put, if a syntactic analysis suggests that the call of a
`program`-mode function can lead to an ill-guarded call of a stobj updater or of `aset1` or `aset2`, then ACL2 considers such
a call to be an ``invariant-risk call''. There are four different ways that
ACL2 can handle such a call, corresponding to four different values of the
``invariant-risk mode'', which is the value obtained by evaluating

The utility,

(set-check-invariant-risk :ERROR) ; new mode is :ERROR (set-check-invariant-risk :WARNING) ; new mode is :WARNING (the default) (set-check-invariant-risk T) ; new mode is T (set-check-invariant-risk NIL) ; new mode is NIL

The argument is evaluated (to itself when given one of the four constants
shown above). There must be an active trust tag in order to set the
invariant-risk mode to

An environment variable, `string-upcase`, and then corresponding call is make
automatically (after loading the ACL2-customization file, if any).

"error", ":error" ==> (set-check-invariant-risk :ERROR) "warning", ":warning" ==> (set-check-invariant-risk :WARNING) "t" ==> (set-check-invariant-risk T) "nil" ==> (set-check-invariant-risk NIL)

Whether by direct user evaluation or environment variable, these calls
simply set a certain global parameter, `encapsulate` events, or `progn` events. A
non-nil second (optional) argument causes an `ACL2-defaults-table` entry
to be made, associating the key `ACL2-defaults-table`.

(set-check-invariant-risk :ERROR t) (set-check-invariant-risk :WARNING t) (set-check-invariant-risk t t) (set-check-invariant-risk NIL t) (set-check-invariant-risk :CLEAR t) ; avoid using table to determine mode

As before, the value `encapsulate` event in which they occur; `ACL2-defaults-table`.
Therefore, do not surround the forms just above with `local`.

When the `ACL2-defaults-table` associates the key

; current invariant-risk mode (:WARNING by default): (get-check-invariant-risk state) ; invariant-risk mode stored in global parameter 'check-invariant-risk: (@ check-invariant-risk) ; invariant-risk mode stored in the acl2-defaults-table: (table acl2-defaults-table :check-invariant-risk)

The following log illustrates the interaction of the two ways of setting the invariant-risk mode (state global and table).

ACL2 !>(set-check-invariant-risk :error t) ACL2 Observation in SET-CHECK-INVARIANT-RISK: No change is being made in the value computed by (GET-CHECK-INVARIANT-RISK STATE). This happens when the value of state global 'check-invariant-risk is less than the new table value; see :DOC set-check-invariant-risk. :ERROR ACL2 !>(get-check-invariant-risk state) :WARNING ACL2 !>(@ check-invariant-risk) :WARNING ACL2 !>(set-check-invariant-risk :error) :ERROR ACL2 !>(@ check-invariant-risk) :ERROR ACL2 !>(get-check-invariant-risk state) :ERROR ACL2 !>(set-check-invariant-risk t t) T ACL2 !>(get-check-invariant-risk state) T ACL2 !>(set-check-invariant-risk :warning) ACL2 Observation in SET-CHECK-INVARIANT-RISK: No change is being made in the value computed by (GET-CHECK-INVARIANT-RISK STATE), because the new value of state global 'check-invariant-risk is greater than the table value; see :DOC set-check-invariant-risk. :WARNING ACL2 !>(get-check-invariant-risk state) T ACL2 !>(set-check-invariant-risk :clear t) :CLEAR ACL2 !>(get-check-invariant-risk state) :WARNING ACL2 !>

Note that the handling of an invariant-risk call of a function,

It might not be obvious how a given function call could lead to an ill-guarded call of a stobj updater or of a primitive with invariant-risk such as aref1. It should be reasonably straightforward to write a utility that provides this information; contact the ACL2 implementors if you want assistance in writing such a utility.