From 16be51f61801c021d75679720e950dd5498652ac Mon Sep 17 00:00:00 2001 From: Keshav Kini Date: Tue, 10 Oct 2017 16:31:13 -0700 Subject: [PATCH 01/10] Link :doc xdoc::syntax to :doc xdoc::markup I always search for `xdoc::syntax` in the manual before remembering the correct doc topic name is `xdoc::markup`, so I figure this alias might help someone else in the future. Also corrected an example in :doc defpointer while I was at it. --- books/xdoc/topics.lisp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/books/xdoc/topics.lisp b/books/xdoc/topics.lisp index 72b7b9eeb83..07c178f4619 100644 --- a/books/xdoc/topics.lisp +++ b/books/xdoc/topics.lisp @@ -406,6 +406,8 @@ an example table:

images and icons, but this is currently awkward. In the future, we may add other tags that users request.

") +(defpointer syntax markup) + (defxdoc preprocessor :short "In addition to its @(see markup) language, XDOC includes a @@ -1746,7 +1748,7 @@ terminal with @(':doc') or in the ACL2-Doc Emacs viewer.

") :long "

Examples:

@({ - (defpointer acl2 acl2-sedan) + (defpointer acl2s acl2-sedan) (defpointer guard-hints xargs t) }) From 5988770b6dafb56fc0163788bd3a0a20c355d6f9 Mon Sep 17 00:00:00 2001 From: "David L. Rager" Date: Tue, 10 Oct 2017 22:55:38 -0500 Subject: [PATCH 02/10] Adding alias for cgen --- books/acl2s/cgen/top.lisp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/books/acl2s/cgen/top.lisp b/books/acl2s/cgen/top.lisp index 3aa1074b876..1a96399c17a 100644 --- a/books/acl2s/cgen/top.lisp +++ b/books/acl2s/cgen/top.lisp @@ -239,6 +239,8 @@ package.

" ) +(acl2::defpointer acl2::counter-example-generation acl2::cgen) + (defxdoc cgen::flush :parents (acl2::cgen) :short "Flush/Reset the Cgen state globals to sane values." From 12abca18084cbafdafa03a7d70bf03bf39964691 Mon Sep 17 00:00:00 2001 From: "David L. Rager" Date: Tue, 10 Oct 2017 23:01:03 -0500 Subject: [PATCH 03/10] Adding note about AVR-ISA to book relnotes --- books/doc/relnotes.lisp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/books/doc/relnotes.lisp b/books/doc/relnotes.lisp index dd152540834..23a3be7ae74 100644 --- a/books/doc/relnotes.lisp +++ b/books/doc/relnotes.lisp @@ -347,6 +347,10 @@ model-specific field. A more complete model of segment address translation has been added.

+

AVR ISA

+ Julien Schmaltz and Peter Schwabes' AVR ISA model has been contributed in book + \"projects/avr-isa\". +

Miscellaneous Books

The book \"clause-processors/use-by-hint\" now contains an additional From 958989fbf6e898ca61b178b1579502b7e36f4ce5 Mon Sep 17 00:00:00 2001 From: "David L. Rager" Date: Wed, 11 Oct 2017 07:51:09 -0500 Subject: [PATCH 04/10] Unbreaking the build --- books/acl2s/cgen/top.lisp | 2 -- 1 file changed, 2 deletions(-) diff --git a/books/acl2s/cgen/top.lisp b/books/acl2s/cgen/top.lisp index 1a96399c17a..3aa1074b876 100644 --- a/books/acl2s/cgen/top.lisp +++ b/books/acl2s/cgen/top.lisp @@ -239,8 +239,6 @@ package.

" ) -(acl2::defpointer acl2::counter-example-generation acl2::cgen) - (defxdoc cgen::flush :parents (acl2::cgen) :short "Flush/Reset the Cgen state globals to sane values." From af8a09bac287a14b2da182e66e5159f7160c42ad Mon Sep 17 00:00:00 2001 From: Matt Kaufmann Date: Wed, 11 Oct 2017 07:54:36 -0500 Subject: [PATCH 05/10] Modified handling of warnings on guard-checking being inhibited on recursive calls. Quoting a comment in (deflabel note-7-5 ...): ; Cleaned up handling of raw-guard-warningp, including: now a state global ; instead of a Lisp special, modified warning message, added :doc ; guard-checking-inhibited, and cleared raw-guard-warningp in a simple way for ; each top level form (in ld-read-eval-print). --- axioms.lisp | 1 + books/system/doc/acl2-doc.lisp | 41 +++++++++++++++++++++ doc.lisp | 42 +++++++++++++++++++++- futures-raw.lisp | 2 +- interface-raw.lisp | 24 ++++++------- ld.lisp | 1 + translate.lisp | 65 ++++------------------------------ 7 files changed, 102 insertions(+), 74 deletions(-) diff --git a/axioms.lisp b/axioms.lisp index ea8825f8e1e..79e4a4c684f 100644 --- a/axioms.lisp +++ b/axioms.lisp @@ -13347,6 +13347,7 @@ evaluated. See :DOC certify-book, in particular, the discussion about ``Step (proofs-co . acl2-output-channel::standard-character-output-0) (protect-memoize-statistics . nil) (raw-arity-alist . nil) + (raw-guard-warningp . nil) (raw-include-book-dir!-alist . :ignore) (raw-include-book-dir-alist . :ignore) (raw-proof-format . nil) diff --git a/books/system/doc/acl2-doc.lisp b/books/system/doc/acl2-doc.lisp index 9f2179632be..eea0369e107 100644 --- a/books/system/doc/acl2-doc.lisp +++ b/books/system/doc/acl2-doc.lisp @@ -33686,6 +33686,42 @@ current fast alists." guard-quick-reference). For a discussion of the use of proof to verify the absence of guard violations, see @(see verify-guards).

") +(defxdoc guard-checking-inhibited + :parents (evaluation guard) + :short "Evaluating ACL2 expressions" + :long "

ACL2 sometimes omits the checking of @(see guard)s on recursive + calls of functions. This omission is signaled by a message like the one shown + below.

+ + @({ + ACL2 !>(factorial 3) + + ACL2 Warning [Guards] in TOP-LEVEL: Guard-checking will be inhibited + for some recursive calls for FACTORIAL and perhaps other functions; + see :DOC guard-checking-inhibited. + + 6 + ACL2 !> + }) + +

More precisely, the warning is printed only when guard-checking is the + default, @('t') (see @(see set-guard-checking)) and guards are not verified + for the indicated function. No further such message is printed (for any + function) before the next top-level form is submitted.

+ +

To check guards on all recursive calls:

+ + @({ + (set-guard-checking :all) + }) + +

To leave the current behavior unchanged except for inhibiting such + messages:

+ + @({ + (set-guard-checking :nowarn) + })") + (defxdoc guard-debug :parents (guard debugging) :short "Generate markers to indicate sources of @(see guard) proof obligations" @@ -76488,6 +76524,11 @@ it." ; some error messages related to :do-not-induct. Thanks to a query from Eric ; Smith that led to these changes. +; Cleaned up handling of raw-guard-warningp, including: now a state global +; instead of a Lisp special, modified warning message, added :doc +; guard-checking-inhibited, and cleared raw-guard-warningp in a simple way for +; each top level form (in ld-read-eval-print). + :parents (release-notes) :short "ACL2 Version 7.5 (xxx, 20xx) Notes" :long "

NOTE! New users can ignore these release notes, because the @(see diff --git a/doc.lisp b/doc.lisp index e790a27b511..a998fdc7388 100644 --- a/doc.lisp +++ b/doc.lisp @@ -28429,7 +28429,13 @@ Subtopics [guards-and-evaluation], for a discussion of guards and their connection to evaluation. Advanced system hackers who want to see the executable-counterpart definition for f may invoke (trace! - (oneify-cltl-code :native t)) before defining f in ACL2.") + (oneify-cltl-code :native t)) before defining f in ACL2. + + +Subtopics + + [Guard-checking-inhibited] + Evaluating ACL2 expressions") (EVALUATOR-RESTRICTIONS (META) "Some restrictions on the use of evaluators in meta-level rules @@ -36705,6 +36711,9 @@ Subtopics [Extra-info] Sources of measure or guard proof obligations + [Guard-checking-inhibited] + Evaluating ACL2 expressions + [Guard-debug] Generate markers to indicate sources of [guard] proof obligations @@ -36796,6 +36805,37 @@ Subtopics [With-guard-checking-event] Suppress or enable guard-checking for an event form") + (GUARD-CHECKING-INHIBITED + (EVALUATION GUARD) + "Evaluating ACL2 expressions + + ACL2 sometimes omits the checking of [guard]s on recursive calls of + functions. This omission is signaled by a message like the one + shown below. + + ACL2 !>(factorial 3) + + ACL2 Warning [Guards] in TOP-LEVEL: Guard-checking will be inhibited + for some recursive calls for FACTORIAL and perhaps other functions; + see :DOC guard-checking-inhibited. + + 6 + ACL2 !> + + More precisely, the warning is printed only when guard-checking is + the default, t (see [set-guard-checking]) and guards are not + verified for the indicated function. No further such message is + printed (for any function) before the next top-level form is + submitted. + + To check guards on all recursive calls: + + (set-guard-checking :all) + + To leave the current behavior unchanged except for inhibiting such + messages: + + (set-guard-checking :nowarn)") (GUARD-DEBUG (GUARD DEBUGGING) "Generate markers to indicate sources of [guard] proof obligations diff --git a/futures-raw.lisp b/futures-raw.lisp index 50daf02e495..87e76c54436 100644 --- a/futures-raw.lisp +++ b/futures-raw.lisp @@ -1208,7 +1208,7 @@ ; Parallelism no-fix: we have considered causing child threads to inherit ; ld-specials from their parents, or even other state globals such as -; *ev-shortcut-okp* and *raw-guard-warningp*, as the following comment from +; *ev-shortcut-okp* and raw-guard-warningp, as the following comment from ; David Rager suggests. But this now seems too difficult to justify that ; effort, and we do not feel obligated to do so; see the "IMPORTANT NOTE" in ; :doc parallelism. diff --git a/interface-raw.lisp b/interface-raw.lisp index ca6d20f2732..7ec121d70c2 100644 --- a/interface-raw.lisp +++ b/interface-raw.lisp @@ -1616,17 +1616,14 @@ (t nil)))) (get-declared-stobjs (cdr edcls))))) -(defun-one-output warn-for-guard-body (fn) - (assert$ (boundp '*raw-guard-warningp*) - (setq *raw-guard-warningp* nil)) - (let ((state *the-live-state*)) - (warning$ 'top-level "Guards" - "Guard-checking will be inhibited on recursive calls of the ~ - executable-counterpart (i.e., in the ACL2 logic) of ~x0. To ~ - check guards on all recursive calls:~% (set-guard-checking ~ - :all)~%To leave behavior unchanged except for inhibiting this ~ - message:~% (set-guard-checking :nowarn)" - fn))) +(defun maybe-warn-for-guard-body (fn state) + (assert$ (f-get-global 'raw-guard-warningp state) + (pprogn (f-put-global 'raw-guard-warningp nil state) + (warning$ 'top-level "Guards" + "Guard-checking will be inhibited for some ~ + recursive calls, including ~x0; see :DOC ~ + guard-checking-inhibited." + fn)))) (defun-one-output create-live-user-stobjp-test (stobjs) (if (endp stobjs) @@ -2358,9 +2355,10 @@ (return-from ,*1*fn ,*1*body))))) (and (and labels-can-miss-guard (not trace-rec-for-none)) ; else skip labels form - `((when (and *raw-guard-warningp* + `((when (and (f-get-global 'raw-guard-warningp + *the-live-state*) (eq ,guard-checking-on-form t)) - (warn-for-guard-body ',fn)))))) + (maybe-warn-for-guard-body ',fn *the-live-state*)))))) (*1*-body-forms (cond ((eq defun-mode :program) (append diff --git a/ld.lisp b/ld.lisp index dab47ba20b5..970309e6906 100644 --- a/ld.lisp +++ b/ld.lisp @@ -1058,6 +1058,7 @@ (pprogn (f-put-global 'trace-level 0 state) (print-deferred-ttag-notes-summary state))) (t state)) + (f-put-global 'raw-guard-warningp t state) (mv-let (col state) (if (and (eql (f-get-global 'in-verify-flg state) 1) diff --git a/translate.lisp b/translate.lisp index b91072c6aa4..4429e118c92 100644 --- a/translate.lisp +++ b/translate.lisp @@ -271,14 +271,6 @@ (t latches))) (t (latch-stobjs1 stobjs-out vals latches)))) -#-acl2-loop-only -; We deliberately do not assign a value for the following. It is let-bound in -; ev and friends and assigned during the evaluation of *1* functions. If we -; call *1* functions directly in raw Lisp, we will presumably get an -; unbound-variable error, but at least that will call our attention to the fact -; that it should be bound before calling *1* functions. -(defvar *raw-guard-warningp*) - (defun actual-stobjs-out1 (stobjs-in args user-stobj-alist) (cond ((endp stobjs-in) (assert$ (null args) nil)) @@ -1069,35 +1061,6 @@ (untranslate-preprocess-fn ,wrld) ,wrld)) -#-acl2-loop-only -(defmacro raw-guard-warningp-binding () - -; We bind *raw-guard-warningp* in calls of ev-fncall, ev, ev-lst, ev-w, -; ev-w-lst, and ev-fncall-w. The initial binding is t if guard-checking is on, -; else nil. When a *1* function is poised to call warn-for-guard-body to print -; a warning related to guard violations, it first checks that -; *raw-guard-warningp*. Hence, we do not want to re-assign this variable once -; it is bound to nil by warn-for-guard-body, because we only want to see the -; corresponding guard warning once per top-level evaluation. We do however -; want to re-assign this variable from t to nil once the warning has been -; printed and also if guard-checking has been turned off, in particular for the -; situation involving the prover that is described in the next paragraph. (But -; if guard-checking were, surprisingly, to transition instead from nil to t, -; and we failed to re-assign this variable from nil to t, we could live with -; that.) - -; Note that *raw-guard-warningp* will be bound to t just under the trans-eval -; at the top level. If we then enter the prover we will bind guard-checking-on -; to nil, and we then want to re-bind *raw-guard-warningp* to nil if we enter -; ev-fncall during the proof, so that the proof output will not contain guard -; warning messages. (This was handled incorrectly in Version_2.9.1.) - - '(if (and (boundp '*raw-guard-warningp*) - (null *raw-guard-warningp*)) - nil - (eq (f-get-global 'guard-checking-on *the-live-state*) - t))) - (defun save-ev-fncall-guard-er (fn guard stobjs-in args) (wormhole-eval 'ev-fncall-guard-er-wormhole '(lambda (whs) @@ -2460,9 +2423,6 @@ (defun ev-fncall-rec (fn args w user-stobj-alist big-n safe-mode gc-off latches hard-error-returns-nilp aok) - -; WARNING: This function should only be called with *raw-guard-warningp* bound. - (declare (xargs :guard (plist-worldp w))) #-acl2-loop-only (cond (*ev-shortcut-okp* @@ -2606,8 +2566,6 @@ (defun ev-rec (form alist w user-stobj-alist big-n safe-mode gc-off latches hard-error-returns-nilp aok) -; WARNING: This function should only be called with *raw-guard-warningp* bound. - ; See also ev-respecting-ens. ; Note: Latches includes a binding of 'state. See the Essay on EV. @@ -2791,9 +2749,6 @@ (defun ev-rec-lst (lst alist w user-stobj-alist big-n safe-mode gc-off latches hard-error-returns-nilp aok) - -; WARNING: This function should only be called with *raw-guard-warningp* bound. - (declare (xargs :guard (and (plist-worldp w) (term-listp lst w) (symbol-alistp alist)))) @@ -2826,8 +2781,6 @@ safe-mode gc-off latches hard-error-returns-nilp aok) -; WARNING: This function should only be called with *raw-guard-warningp* bound. - ; Sketch: We know that form is a termp wrt w and that it is recognized by ; translated-acl2-unwind-protectp. We therefore unpack it into its body and ; two cleanup forms and give it special attention. If the body evaluates @@ -3064,8 +3017,7 @@ ; Keep the two ev-fncall-rec calls below in sync. #-acl2-loop-only - (let ((*ev-shortcut-okp* t) - (*raw-guard-warningp* (raw-guard-warningp-binding))) + (let ((*ev-shortcut-okp* t)) (state-free-global-let* ((safe-mode safe-mode) (guard-checking-on @@ -3128,8 +3080,7 @@ ; See the comment in ev for why we don't check the time limit here. #-acl2-loop-only - (let ((*ev-shortcut-okp* t) - (*raw-guard-warningp* (raw-guard-warningp-binding))) + (let ((*ev-shortcut-okp* t)) (state-free-global-let* ((safe-mode safe-mode) (guard-checking-on @@ -3648,8 +3599,7 @@ (defun ev-fncall (fn args state latches hard-error-returns-nilp aok) (declare (xargs :guard (state-p state))) - (let #-acl2-loop-only ((*ev-shortcut-okp* (live-state-p state)) - (*raw-guard-warningp* (raw-guard-warningp-binding))) + (let #-acl2-loop-only ((*ev-shortcut-okp* (live-state-p state))) #+acl2-loop-only () ; See the comment in ev for why we don't check the time limit here. @@ -3669,8 +3619,7 @@ (declare (xargs :guard (and (state-p state) (termp form (w state)) (symbol-alistp alist)))) - (let #-acl2-loop-only ((*ev-shortcut-okp* (live-state-p state)) - (*raw-guard-warningp* (raw-guard-warningp-binding))) + (let #-acl2-loop-only ((*ev-shortcut-okp* (live-state-p state))) #+acl2-loop-only () ; At one time we called time-limit5-reached-p here so that we can quit if we @@ -3703,8 +3652,7 @@ (declare (xargs :guard (and (state-p state) (term-listp lst (w state)) (symbol-alistp alist)))) - (let #-acl2-loop-only ((*ev-shortcut-okp* (live-state-p state)) - (*raw-guard-warningp* (raw-guard-warningp-binding))) + (let #-acl2-loop-only ((*ev-shortcut-okp* (live-state-p state))) #+acl2-loop-only () ; See the comment in ev for why we don't check the time limit here. @@ -3801,8 +3749,7 @@ ; See the comment in ev for why we don't check the time limit here. #-acl2-loop-only - (let ((*ev-shortcut-okp* t) - (*raw-guard-warningp* (raw-guard-warningp-binding))) + (let ((*ev-shortcut-okp* t)) (state-free-global-let* ((safe-mode safe-mode) (guard-checking-on From 85cadb39a816d2a523912c0e8b385ddaf45364ac Mon Sep 17 00:00:00 2001 From: Keshav Kini Date: Wed, 11 Oct 2017 14:15:04 -0700 Subject: [PATCH 06/10] Make defpointer support package-external symbols Previously, defpointer took its arguments and ignored what package they were in, incorrectly using the symbols with the same names in the current package instead. Now it respects the package in which its arguments lie. In making this change, I also had to decide what the link text of the pointer should look like, depending on what package the linked doc topic's symbol was in. I decided that if the `from` and `to` symbols were both in the same package, we should leave off the package qualification in the text, and otherwise we should include it. I also added a guard to the macro to ensure that only symbols are accepted. --- books/xdoc/top.lisp | 36 +++++++++++++++++++++++------------- 1 file changed, 23 insertions(+), 13 deletions(-) diff --git a/books/xdoc/top.lisp b/books/xdoc/top.lisp index 315cc129e25..7746ec3d817 100644 --- a/books/xdoc/top.lisp +++ b/books/xdoc/top.lisp @@ -470,20 +470,30 @@ (concatenate-symbol-names (list ,@args)) mksym-package-symbol))) -; Moved from acl2-doc.lisp to make it more widely available (defmacro defpointer (from to &optional keyword-p) - `(defxdoc ,from - :parents (pointers) - :short ,(concatenate 'string - "See @(see " - (acl2::string-downcase (symbol-name to)) - ")" - (if keyword-p - (concatenate 'string - " for keyword @(':" - (acl2::string-downcase (symbol-name from)) - "').") - ".")))) + (declare (xargs :guard (and (symbolp from) (symbolp to)))) + (let ((from-pkg (acl2::string-downcase (symbol-package-name from))) + (from-name (acl2::string-downcase (symbol-name from))) + (to-pkg (acl2::string-downcase (symbol-package-name to))) + (to-name (acl2::string-downcase (symbol-name to)))) + `(defxdoc ,from + :parents (pointers) + :short ,(concatenate + 'string + "See " + (if (equal to-pkg from-pkg) + to-name + (concatenate 'string to-pkg "::" to-name)) + "" + (if keyword-p + (concatenate + 'string + " for information about the keyword @(':" + from-name + "').") + "."))))) (defun add-resource-directory-fn (dirname fullpath world) From ae4db760c97389d2bca237a9d0f2c5f3a986bacf Mon Sep 17 00:00:00 2001 From: Keshav Kini Date: Wed, 11 Oct 2017 14:18:11 -0700 Subject: [PATCH 07/10] Document keyword-p argument of defpointer --- books/xdoc/topics.lisp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/books/xdoc/topics.lisp b/books/xdoc/topics.lisp index 07c178f4619..0a42ae22323 100644 --- a/books/xdoc/topics.lisp +++ b/books/xdoc/topics.lisp @@ -1761,7 +1761,15 @@ terminal with @(':doc') or in the ACL2-Doc Emacs viewer.

")

This is a simple macro that expands to a @(see defxdoc) form. It introduces a new @(see xdoc) topic, @('new-topic'), that merely links to @('target-topic'). The new topic will only be listed under @(see -pointers).

") +pointers).

+ +

A common practice when documenting keyword symbols is to create a +doc topic in in the \"ACL2\" package or some other relevant package, +rather than the \"KEYWORD\" package to which the keyword symbol +rightfully belongs. In keeping with this practice, the @('keywordp') +argument to @('defpointer'), if non-nil, adds a clarification that the +doc topic is really about the keyword symbol with the same name as +@('new-topic'), rather than @('new-topic') itself.

") (defxdoc add-resource-directory From 25deb4f55c4831d5f23c6e250da25c548d40de3d Mon Sep 17 00:00:00 2001 From: Keshav Kini Date: Wed, 11 Oct 2017 14:18:29 -0700 Subject: [PATCH 08/10] Reinstate David's defpointer in acl2s/cgen/top book --- books/acl2s/cgen/top.lisp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/books/acl2s/cgen/top.lisp b/books/acl2s/cgen/top.lisp index 3aa1074b876..d3fefce9071 100644 --- a/books/acl2s/cgen/top.lisp +++ b/books/acl2s/cgen/top.lisp @@ -239,6 +239,9 @@ package.

" ) +#!ACL2 +(defpointer counter-example-generation cgen) + (defxdoc cgen::flush :parents (acl2::cgen) :short "Flush/Reset the Cgen state globals to sane values." From bbf835a2df29a6ad75bac952c3ec4a4852915406 Mon Sep 17 00:00:00 2001 From: Matt Kaufmann Date: Wed, 11 Oct 2017 17:57:33 -0500 Subject: [PATCH 09/10] Fixed a problem with system function ev-fncall-w (really, raw-ev-fncall). Quoting :doc note-7-5: The built-in evaluator functions for ACL2 relied on a system function, ev-fncall-w, that was not a function! We do not see how to exploit this oddity to prove nil, since ev-fncall-w is guaranteed never to be in [logic] mode. However, it is clearly undesirable. In the following example, the two ev-fncall-w calls gave different answers on the same inputs --- (mv nil 7) and (mv nil 12) --- but now the second call results in an error. (defun foo (x y) (+ x y)) (assign old-w (w state)) (ev-fncall-w 'foo '(3 4) (@ old-w) nil nil nil t nil) (u) (defun foo (x y) (* x y)) (ev-fncall-w 'foo '(3 4) (@ old-w) nil nil nil t nil) The following comment in (deflabel note-7-5 ...) explains further: ; The problem with ev-fncall-w (not a function) was really a problem with ; raw-ev-fncall, which has been fixed. I'm seeing a bit less than a 1% slowdown, which I think is tolerable and actually pretty good, given that the solution requires (as far as I know) some sort of check that the world is "close to" the world of the live state. See chk-raw-ev-fncall and its subfunction, raw-ev-fncall-okp, if interested. --- books/system/doc/acl2-doc.lisp | 20 ++ defuns.lisp | 4 +- doc.lisp | 15 ++ history-management.lisp | 1 + translate.lisp | 324 +++++++++++++++++++++------------ 5 files changed, 245 insertions(+), 119 deletions(-) diff --git a/books/system/doc/acl2-doc.lisp b/books/system/doc/acl2-doc.lisp index eea0369e107..ea9ccabc294 100644 --- a/books/system/doc/acl2-doc.lisp +++ b/books/system/doc/acl2-doc.lisp @@ -76529,6 +76529,9 @@ it." ; guard-checking-inhibited, and cleared raw-guard-warningp in a simple way for ; each top level form (in ld-read-eval-print). +; The problem with ev-fncall-w (not a function) was really a problem with +; raw-ev-fncall, which has been fixed. + :parents (release-notes) :short "ACL2 Version 7.5 (xxx, 20xx) Notes" :long "

NOTE! New users can ignore these release notes, because the @(see @@ -76792,6 +76795,23 @@ it." especially for his contributions to a fix through helpful conversations and by providing code and examples.

+

The built-in evaluator functions for ACL2 relied on a system function, + @('ev-fncall-w'), that was not a function! We do not see how to exploit this + oddity to prove @('nil'), since @('ev-fncall-w') is guaranteed never to be in + @(see logic) mode. However, it is clearly undesirable. In the following + example, the two @('ev-fncall-w') calls gave different answers on the same + inputs — @('(mv nil 7)') and @('(mv nil 12)') — but now the second + call results in an error.

+ + @({ + (defun foo (x y) (+ x y)) + (assign old-w (w state)) + (ev-fncall-w 'foo '(3 4) (@ old-w) nil nil nil t nil) + (u) + (defun foo (x y) (* x y)) + (ev-fncall-w 'foo '(3 4) (@ old-w) nil nil nil t nil) + }) +

The check for the requisite theorems supporting a @(tsee defabsstobj) event included a case where the check was too weak, and it also could cause an unexpected assertion. The first of these could probably cause unsoundness. diff --git a/defuns.lisp b/defuns.lisp index 62d73f8be4e..469c753ec7d 100644 --- a/defuns.lisp +++ b/defuns.lisp @@ -1825,7 +1825,9 @@ ; Sol Swords sent an example in which a clause-processor failed during a ; termination proof. That problem goes away if we install the world, which we -; do by making the following binding. +; do by making the following binding. This seems particularly important now +; that raw-ev-fncall calls chk-raw-ev-fncall to ensure that the world is +; (essentially) installed. t ; formerly big-mutrec wrld1)) diff --git a/doc.lisp b/doc.lisp index a998fdc7388..e4608bff3ca 100644 --- a/doc.lisp +++ b/doc.lisp @@ -75492,6 +75492,21 @@ Bug Fixes especially for his contributions to a fix through helpful conversations and by providing code and examples. + The built-in evaluator functions for ACL2 relied on a system + function, ev-fncall-w, that was not a function! We do not see how + to exploit this oddity to prove nil, since ev-fncall-w is + guaranteed never to be in [logic] mode. However, it is clearly + undesirable. In the following example, the two ev-fncall-w calls + gave different answers on the same inputs --- (mv nil 7) and (mv + nil 12) --- but now the second call results in an error. + + (defun foo (x y) (+ x y)) + (assign old-w (w state)) + (ev-fncall-w 'foo '(3 4) (@ old-w) nil nil nil t nil) + (u) + (defun foo (x y) (* x y)) + (ev-fncall-w 'foo '(3 4) (@ old-w) nil nil nil t nil) + The check for the requisite theorems supporting a [defabsstobj] event included a case where the check was too weak, and it also could cause an unexpected assertion. The first of these could probably diff --git a/history-management.lisp b/history-management.lisp index 7857a0ba9de..02944b41c60 100644 --- a/history-management.lisp +++ b/history-management.lisp @@ -3547,6 +3547,7 @@ (t (f-put-global 'current-package "ACL2" state)))) #-acl2-loop-only (cond ((live-state-p state) + (setf (car *fncall-cache*) nil) (cond ((and *wormholep* (not (eq wrld (w *the-live-state*)))) (push-wormhole-undo-formi 'cloaked-set-w! (w *the-live-state*) diff --git a/translate.lisp b/translate.lisp index 4429e118c92..cb5f5f98ea4 100644 --- a/translate.lisp +++ b/translate.lisp @@ -405,124 +405,6 @@ nil) -#-acl2-loop-only -(defun raw-ev-fncall (fn args latches w user-stobj-alist - hard-error-returns-nilp aok) - (the #+acl2-mv-as-values (values t t t) - #-acl2-mv-as-values t - (let* ((*aokp* - -; We expect the parameter aok, here and in all functions in the "ev family" -; that take aok as an argument, to be Boolean. If it's not, then there is no -; real harm done: *aokp* would be bound here to a non-Boolean value, suggesting -; that an attachment has been used when that isn't necessarily the case; see -; *aokp*. - - aok) - (pair (assoc-eq 'state latches)) - (w (if pair (w (cdr pair)) w)) ; (cdr pair) = *the-live-state* - (throw-raw-ev-fncall-flg t) - (**1*-as-raw* - -; We defeat the **1*-as-raw* optimization so that when we use raw-ev-fncall to -; evaluate a call of a :logic mode term, all of the evaluation will take place -; in the logic. Note that we don't restrict this special treatment to -; :common-lisp-compliant functions, because such a function might call an -; :ideal mode function wrapped in ec-call. But we do restrict to :logic mode -; functions, since they cannot call :program mode functions and hence there -; cannot be a subsidiary rebinding of **1*-as-raw* to t. - - (if (logicp fn w) - nil - **1*-as-raw*)) - (*1*fn (*1*-symbol fn)) - (applied-fn (cond - ((fboundp *1*fn) *1*fn) - ((and (global-val 'boot-strap-flg w) - (not (global-val 'boot-strap-pass-2 w))) - fn) - (t - (er hard 'raw-ev-fncall - "We had thought that *1* functions were ~ - always defined outside the first pass of ~ - initialization, but the *1* function for ~ - ~x0, which should be ~x1, is not." - fn *1*fn)))) - (stobjs-out - (cond ((eq fn 'return-last) - -; Things can work out fine if we imagine that return-last returns a single -; value: in the case of (return-last ... (mv ...)), the mv returns a list and -; we just pass that along. - - '(nil)) -; The next form was originally conditionalized with #+acl2-extra-checks, but we -; want to do this unconditionally. - (latches ; optimization - (actual-stobjs-out fn args w user-stobj-alist)) - (t (stobjs-out fn w)))) - (val (catch 'raw-ev-fncall - (cond ((not (fboundp fn)) - (er hard 'raw-ev-fncall - "A function, ~x0, that was supposed to be ~ - defined is not. Supposedly, this can only ~ - arise because of aborts during undoing. ~ - There is no recovery from this erroneous ~ - state." - fn))) - (prog1 - (let ((*hard-error-returns-nilp* - hard-error-returns-nilp)) - #-acl2-mv-as-values - (apply applied-fn args) - #+acl2-mv-as-values - (cond ((null (cdr stobjs-out)) - (apply applied-fn args)) - (t (multiple-value-list - (apply applied-fn args))))) - (setq throw-raw-ev-fncall-flg nil)))) - -; It is important to rebind w here, since we may have updated state since the -; last binding of w. - - (w (if pair - -; We use the live state now if and only if we used it above, in which case (cdr -; pair) = *the-live-state*. - - (w (cdr pair)) - w))) - -; Observe that if a throw to 'raw-ev-fncall occurred during the -; (apply fn args) then the local variable throw-raw-ev-fncall-flg -; is t and otherwise it is nil. If a throw did occur, val is the -; value thrown. - - (cond - (throw-raw-ev-fncall-flg - (mv t (ev-fncall-msg val w user-stobj-alist) latches)) - (t #-acl2-mv-as-values ; adjust val for the multiple value case - (let ((val - (cond - ((null (cdr stobjs-out)) val) - (t (cons val - (mv-refs (1- (length stobjs-out)))))))) - (mv nil - val -; The next form was originally conditionalized with #+acl2-extra-checks, with -; value latches when #-acl2-extra-checks; but we want this unconditionally. - (latch-stobjs stobjs-out ; adjusted to actual-stobjs-out - val - latches))) - #+acl2-mv-as-values ; val already adjusted for multiple value case - (mv nil - val -; The next form was originally conditionalized with #+acl2-extra-checks, with -; value latches when #-acl2-extra-checks; but we want this unconditionally. - (latch-stobjs stobjs-out ; adjusted to actual-stobjs-out - val - latches))))))) - (defun translated-acl2-unwind-protectp4 (term) ; This hideous looking function recognizes those terms that are the @@ -2033,8 +1915,214 @@ (cadr x))) (t (list 'not x)))) +(defun event-tuple-fn-names (ev-tuple) + (case (access-event-tuple-type ev-tuple) + ((defun) + (list (access-event-tuple-namex ev-tuple))) + ((defuns defstobj) + (access-event-tuple-namex ev-tuple)) + (otherwise nil))) + +#-acl2-loop-only +(progn + +(defvar *fncall-cache* + '(nil)) + +(defun raw-ev-fncall-okp (wrld aokp &aux (w-state (w *the-live-state*))) + (when (eq wrld w-state) + (return-from raw-ev-fncall-okp :live)) + (let* ((fncall-cache *fncall-cache*) + (cached-w (car *fncall-cache*))) + (cond ((and wrld + (eq wrld cached-w)) + t) + (t + (let ((fns nil)) + (loop for tail on wrld + until (eq tail w-state) + do (let ((trip (car tail))) + (cond + ((member-eq (cadr trip) + '(unnormalized-body + stobjs-out + +; 'Symbol-class supports the programp call in ev-fncall-guard-er-msg. + + symbol-class + table-alist)) + (setq fns (add-to-set-eq (car trip) fns))) + ((and (eq (car trip) 'guard-msg-table) + (eq (cadr trip) 'table-alist)) + +; The table, guard-msg-table, is consulted in ev-fncall-guard-er-msg. + + (return-from raw-ev-fncall-okp nil)) + ((and (eq (car trip) 'event-landmark) + (eq (cadr trip) 'global-value)) + +; This case is due to the get-event call in guard-raw. + + (setq fns + (union-eq (event-tuple-fn-names (cddr trip)) + fns))) + ((and aokp + (eq (car trip) 'attachment-records) + (eq (cadr trip) 'global-value)) + (return-from raw-ev-fncall-okp nil)))) + finally + (cond (tail (setf (car fncall-cache) nil + (cdr fncall-cache) fns + (car fncall-cache) wrld)) + (t (return-from raw-ev-fncall-okp nil))))) + t) + (t nil)))) + +(defun chk-raw-ev-fncall (fn wrld aokp) + (let ((ctx 'raw-ev-fncall) + (okp (raw-ev-fncall-okp wrld aokp))) + (cond ((eq okp :live) nil) + (okp + (when (member-eq fn (cdr *fncall-cache*)) + (er hard ctx + "Implementation error: Unexpected call of raw-ev-fncall for ~ + function ~x0 (the world is sufficiently close to (w state) ~ + in general, but not for that function symbol)." + fn))) + (t + (er hard ctx + "Implementation error: Unexpected call of raw-ev-fncall (the ~ + world is not sufficiently close to (w state))."))))) + +(defun raw-ev-fncall (fn args latches w user-stobj-alist + hard-error-returns-nilp aok) + +; Here we assume that w is "close to" (w state), as implemented by +; chk-raw-ev-fncall. + + (the #+acl2-mv-as-values (values t t t) + #-acl2-mv-as-values t + (let* ((*aokp* + +; We expect the parameter aok, here and in all functions in the "ev family" +; that take aok as an argument, to be Boolean. If it's not, then there is no +; real harm done: *aokp* would be bound here to a non-Boolean value, suggesting +; that an attachment has been used when that isn't necessarily the case; see +; *aokp*. + + aok) + (pair (assoc-eq 'state latches)) + (w (if pair (w (cdr pair)) w)) ; (cdr pair) = *the-live-state* + (throw-raw-ev-fncall-flg t) + (**1*-as-raw* + +; We defeat the **1*-as-raw* optimization so that when we use raw-ev-fncall to +; evaluate a call of a :logic mode term, all of the evaluation will take place +; in the logic. Note that we don't restrict this special treatment to +; :common-lisp-compliant functions, because such a function might call an +; :ideal mode function wrapped in ec-call. But we do restrict to :logic mode +; functions, since they cannot call :program mode functions and hence there +; cannot be a subsidiary rebinding of **1*-as-raw* to t. + + (if (logicp fn w) + nil + **1*-as-raw*)) + (*1*fn (*1*-symbol fn)) + (applied-fn (cond + ((fboundp *1*fn) *1*fn) + ((and (global-val 'boot-strap-flg w) + (not (global-val 'boot-strap-pass-2 w))) + fn) + (t + (er hard 'raw-ev-fncall + "We had thought that *1* functions were ~ + always defined outside the first pass of ~ + initialization, but the *1* function for ~ + ~x0, which should be ~x1, is not." + fn *1*fn)))) + (stobjs-out + (cond ((eq fn 'return-last) + +; Things can work out fine if we imagine that return-last returns a single +; value: in the case of (return-last ... (mv ...)), the mv returns a list and +; we just pass that along. + + '(nil)) +; The next form was originally conditionalized with #+acl2-extra-checks, but we +; want to do this unconditionally. + (latches ; optimization + (actual-stobjs-out fn args w user-stobj-alist)) + (t (stobjs-out fn w)))) + (val (catch 'raw-ev-fncall + (chk-raw-ev-fncall fn w aok) + (cond ((not (fboundp fn)) + (er hard 'raw-ev-fncall + "A function, ~x0, that was supposed to be ~ + defined is not. Supposedly, this can only ~ + arise because of aborts during undoing. ~ + There is no recovery from this erroneous ~ + state." + fn))) + (prog1 + (let ((*hard-error-returns-nilp* + hard-error-returns-nilp)) + #-acl2-mv-as-values + (apply applied-fn args) + #+acl2-mv-as-values + (cond ((null (cdr stobjs-out)) + (apply applied-fn args)) + (t (multiple-value-list + (apply applied-fn args))))) + (setq throw-raw-ev-fncall-flg nil)))) + +; It is important to rebind w here, since we may have updated state since the +; last binding of w. + + (w (if pair + +; We use the live state now if and only if we used it above, in which case (cdr +; pair) = *the-live-state*. + + (w (cdr pair)) + w))) + +; Observe that if a throw to 'raw-ev-fncall occurred during the +; (apply fn args) then the local variable throw-raw-ev-fncall-flg +; is t and otherwise it is nil. If a throw did occur, val is the +; value thrown. + + (cond + (throw-raw-ev-fncall-flg + (mv t (ev-fncall-msg val w user-stobj-alist) latches)) + (t #-acl2-mv-as-values ; adjust val for the multiple value case + (let ((val + (cond + ((null (cdr stobjs-out)) val) + (t (cons val + (mv-refs (1- (length stobjs-out)))))))) + (mv nil + val +; The next form was originally conditionalized with #+acl2-extra-checks, with +; value latches when #-acl2-extra-checks; but we want this unconditionally. + (latch-stobjs stobjs-out ; adjusted to actual-stobjs-out + val + latches))) + #+acl2-mv-as-values ; val already adjusted for multiple value case + (mv nil + val +; The next form was originally conditionalized with #+acl2-extra-checks, with +; value latches when #-acl2-extra-checks; but we want this unconditionally. + (latch-stobjs stobjs-out ; adjusted to actual-stobjs-out + val + latches))))))) +) + (mutual-recursion +; These functions assume that the input world is "close to" the installed +; world, (w *the-live-state*), since ultimately they typically lead to calls of +; the check chk-raw-ev-fncall within raw-ev-fncall. + ; Here we combine what may naturally be thought of as two separate ; mutual-recursion nests: One for evaluation and one for untranslate. However, ; functions in the ev nest call untranslate1 for error messages, and From 622a9f9bd0ee216a937f9204a8033be44024c45f Mon Sep 17 00:00:00 2001 From: Matt Kaufmann Date: Thu, 12 Oct 2017 12:45:40 -0500 Subject: [PATCH 10/10] Fixed an ACL2(p) error that I apparently introduced in commit a680a466da987be381b0c93895f5cd336d5bcb2c. In my editing of translate-in-theory-hint@par, I accidentally changed eval-theory-expr@par to eval-theory-expr. I've changed it back. Note: since this is definitely an improvement, I did only the equivalent of a "basic" regression before doing this commit/push. Thanks to David Rager for pointing out an ACL2(p) build failure on leeroy. --- history-management.lisp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/history-management.lisp b/history-management.lisp index 02944b41c60..f3a662a21eb 100644 --- a/history-management.lisp +++ b/history-management.lisp @@ -13214,7 +13214,7 @@ (declare (ignorable chk-boot-strap-fns-flg)) ; suppress irrelevance warning (er-let*@par - ((runic-value (eval-theory-expr expr ctx wrld state))) + ((runic-value (eval-theory-expr@par expr ctx wrld state))) (let* ((warning-disabled-p (warning-disabled-p "Theory")) (ens (ens state))) (prog2$