User-stobjs-modified-warnings
Interactions of trans-eval with stobjs that violate
applicative semantics
The utility, trans-eval, may be called to evaluate
arbitrary ACL2 forms. It can thus be useful for writers of tools. This topic
discusses certain warnings that may be issued by trans-eval for
stobj updates that may violate applicative semantics. Also see trans-eval-and-locally-bound-stobjs for how trans-eval relates to
updates of locally bound stobjs.
Please see trans-eval and trans-eval-and-stobjs for relevant
background.
Consider the following log.
ACL2 !>(foo st state)
ACL2 Warning [User-stobjs-modified] in FOO: A call of the ACL2 evaluator
on the term (UPDATE-FLD '4 ST) may have modified the user stobj ST. See
:DOC user-stobjs-modified-warnings.
(4 <state> <st>)
ACL2 !>
The warning is intended to indicate that a stobj may have been
modified even though that stobj was accessed indirectly, through the ACL2
state. If you see such a warning, it is probably caused by a utility
that you are invoking. At this time there are no special tools for
identifying which tool is issuing those warnings, but the ``context'' on the
first line of the warning — FOO, above — may give a clue.
Below we discuss the following events, which were evaluated before
producing the log above.
(defstobj st fld)
(defun foo (st state)
(declare (xargs :stobjs (st state)
:mode :program))
(let ((st (update-fld 3 st)))
(mv-let (erp val state)
(trans-eval '(update-fld 4 st) 'foo state nil)
(declare (ignore erp val))
(mv (fld st) state st))))
After submitting these two forms, we can submit to ACL2 the form (foo st
state) to produce the log displayed near the top of this topic. That log is
actually very surprising if you think about it, since the trans-eval call
in the definition of foo modifies only the state parameter, not the
st parameter, and yet the value st has changed: (fld st) has
changed from 3 to 4, while evaluating code in which st does not occur
free! Let us discuss this point further.
First consider the definition of foo. Now trans-eval returns an
error-triple, say (mv erp val state), where erp and val
are ordinary (non-stobj) values. In particular, trans-eval does
not return the user-defined stobj, st. It ``should'' follow, then, that
the only modification to st before returning is by the form
(update-fld 3 st). So the final value of (fld st) ``should'' be 3;
yet, it is 4, not 3! So the first return value of 4, above, can very
reasonably be considered to violate applicative semantics. ACL2 acknowledges
this concern — that is, the concern that an operation (i.e., fld)
now gives a different result on an object (i.e., st) that ``should'' not
have changed, thus violating normal applicative semantics — by printing
the warning displayed above.
To see how this can happen, consider that in raw Lisp the stobj, st,
is actually a one-element array whose unique value is (fld st). The
trans-eval call in foo replaces that element, in this case 3, with a
new value, in this case 4. It does this destructively: the memory
location of st is not changed. Thus, evaluation of (fld st) after
the trans-eval call now returns the new array element, which is 4.
Worse yet, there are similar cases where there is no such violation
of applicative semantics! We return to this point later below. First we
provide some additional discussion of such warnings, as well as observations
for tool writers who want to eliminate the warnings.
In general, such a warning is printed whenever the stobjs-out returned
in the car of the value, as discussed above, contains a user-defined
stobj name, that is, a non-nil value other than state.
Fortunately, this behavior can only happen with :program-mode
functions; trans-eval will never be in :logic mode, and
therefore, neither will its callers. Nevertheless, even without proving
nil one might reasonably be frustrated by this sort of violation of
applicative semantics. The warning is, at least, an acknowledgment of this
situation.
We next discuss how to write tools that avoid producing such warnings, and
the advisability (or not) of doing so.
There may be cases in which you want to write a tool that calls
trans-eval and modifies user-defined stobjs, but you don't want the users
of your tool to see the warning, perhaps because you are convinced that no
stobj parameter is modified indirectly using trans-eval. Think carefully
about whether you really don't want them to see the warning! After all, they
may be relying on normal applicative semantics, even with :program-mode
functions.
If indeed you want to avoid warnings, you can call the function
trans-eval-no-warning exactly as you call trans-eval. For example,
if you replace trans-eval by trans-eval-no-warning in the definition
above, and then you evaluate (foo st state), you will not see the warning
printed above. Again, consider whether you really want to suppress that
warning.
Remark pertaining to (ld ...). There is another alternative to
trans-eval, trans-eval-default-warning. This alternative behaves
like trans-eval when the ld special,
ld-user-stobjs-modified-warning, is t; otherwise it behaves like
trans-eval-no-warning. See ld. There are several calls of
trans-eval-default-warning in the ACL2 source code: in function
ld-read-eval-print, which evaluates on behalf of the top-level loop, and
in some functions that support events, such as those supporting the
proof-builder. But for user-level code it may be more appropriate to call
trans-eval so that violations of applicative semantics are reported.
These warnings are unimportant for the top-level calls of trans-eval that
implement the ACL2 read-eval-print loop, because one expects stobjs to be
updated by evaluation. End of Remark.
For trans-eval and trans-eval-default-warning, the normal way
of inhibiting warnings is supported: (set-inhibit-warnings
"User-stobjs-modified").
We now elaborate on a point made briefly above, that there are cases where
the usual violation of applicative semantics does not take place. This
happens when the underlying raw Lisp stobj is actually replaced, which happens
when there is a single stobj field that is either an array being resized or a
hash table being initialized (with the ``clear'' or ``init'' function); see
defstobj. Consider the following example.
(defstobj st2 (ar :type (array t (10)) :resizable t))
(defun foo2 (st2 state)
(declare (xargs :stobjs (st2 state)
:mode :program))
(let ((st2 (update-ari 3 'old st2)))
(mv-let (erp val state)
(trans-eval '(let ((st2 (resize-ar 20 st2)))
(update-ari 3 'new st2))
'foo state nil)
(declare (ignore erp val))
(mv (ari 3 st2) state st2))))
After submitting these forms, evaluation of the form (foo2 st2 state)
produces (OLD <state> <st2>). But based on the first example, foo,
we might expect that destructive modification of st2 would result instead
in (NEW <state> <st2>). Indeed, if the first argument of trans-eval
in the definition of foo2 is instead (update-ari 3 'new st2)), then
the result is (NEW <state> <st2>). So why do we get the OLD result using
the definition of foo2 displayed above?
The reason is that when a stobj has a single field, and that field is an
array or hash table, then in raw Lisp the stobj is exactly that field.
When we call resize-ar, the entire array is rebuilt, and thus the stobj
is at a new memory location. To be precise: After the resizing, then the
value of st2 in the user-stobj-alist of the ACL2 state is a new
stobj: the actual parameter st2 of foo2 is not destructively
modified. Thus, normal applicative semantics apply: the final value of
(fld st2) is independent of the replacement of st2 in the
user-stobj-alist hence is still 3 (from the first update).
We close with a more realistic example.
(It is based on our experience modifying the definition of the macro,
local-test, in community-book
books/system/tests/nested-stobj-tests.lisp, when we changed ACL2 so that
the stobj is the entire array field when there is only that one field.) The
make-event call below fails, because the resizing operation replaces
the stobj in the global user-stobj-alist of the ACL2 state, but
the call of EQUAL still references the original stobj. This failure is
thus exactly as expected for an applicative semantics. However, it fails only
because the resize operation is not destructive: it replaces the entire
stobj.
(defstobj st3 (ar3 :type (array t (10)) :resizable t))
; Fails (see discussion above):
(make-event
(er-progn (trans-eval '(let ((st3 (resize-ar3 30 st3)))
(update-ar3i 24 'done st3))
'top
state t)
(value (equal (ar3i 24 st3) 'done))
(value '(value-triple :success))))
; Passes because by now, the user-stobj-alist has been updated by
; the top-level call of trans-eval to implement the ACL2
; read-eval-print loop:
(assert-event (equal (ar3i 24 st3) 'done))
; The following version passes because the second trans-eval call
; below references the value of st3 in the user-stobj-alist that was
; produced by the first trans-eval call below.
(make-event
(er-progn (trans-eval '(let ((st3 (resize-ar3 40 st3)))
(update-ar3i 34 'new st3))
'top state t)
(trans-eval '(if (equal (ar3i 34 st3) 'new)
(value nil)
(er soft 'top "Failed!"))
'top state t)
(value '(value-triple :success))))
