Set-check-invariant-risk
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
(get-check-invariant-risk state). The default invariant-risk mode is
:WARNING: in that mode, ACL2 prints a warning when encountering a topmost
invariant-risk call and uses a slower mode of execution in order to avoid
ill-guarded calls as discussed above. Mode T has the same behavior, but
without the warning. Mode :ERROR causes a break when encountering a
topmost invariant-risk call; the Lisp should give you the option of
continuing (as though the mode were T) or aborting, as you choose.
Finally, mode NIL — which is unsafe and hence involves a trust
tag (see defttag), as discussed below — avoids any special
treatment for invariant-risk calls.
The utility, set-check-invariant-risk, is provided for changing
invariant-risk mode. The simplest case is when that utility is only called
with one argument, in which case, that argument becomes the new invariant-risk
mode, as follows.
(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 NIL. However, ACL2 arranges automatically to
create a temporary trust tag when invoking set-check-invariant-risk on an
expression that is other than one of the symbols :ERROR, :WARNING,
or T.
An environment variable, ACL2_CHECK_INVARIANT_RISK, provides a
convenient way to evaluate one of these forms automatically when ACL2 is
invoked. When that environment variable has a value other than the empty
string, the value is converted to a symbol after converting to upper-case with
the function 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, 'check-invariant-risk
(technically, a state global variable). However, they are not embedded
event forms (see embedded-event-form: they cannot appear at the top
level of books, encapsulate events, or progn events. A
non-nil second (optional) argument causes an ACL2-defaults-table entry
to be made, associating the key :check-invariant-risk with the
invariant-risk mode. Thus, the following forms are embedded event forms.
Notice the new ``mode'', :CLEAR, which behaves as though removing the key
:check-invariant-risk from the 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 NIL requires an active trust tag; but unlike
before, ACL2 does not create a temporary trust tag, but instead expect the
user to have created one already. Note also that changes to the
acl2-defaults-table are automatically local to a book or 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
:check-invariant-risk with any value (as in the calls above) other than
:CLEAR, then the invariant-risk mode is actually the ``minimum'' of that
value and the value of the global parameter, 'check-invariant-risk, where
the modes are ordered from greatest to least as shown in the displays above.
An observation is printed when the new mode does not change: for
example, if you start your ACL2 session by evaluating
(set-check-invariant-risk :ERROR t), then the invariant-risk mode will be
the minimum of the existing (default) value of :WARNING and the proposed
value (newly stored in the acl2-defaults-table of :ERROR; that
minimum is :WARNING, so the mode will remain :WARNING and an observation will be printed to that effect. You can see all the relevant
mode values as follows.
; 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, f,
depends on the current invariant-risk mode, not on the mode in place when
f was defined.
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.
