`modify-raw-defun` breaks when loaded from a certified book

[mister-walter]

When modify-raw-defun from the hacker books is used inside of a book that is certified and loaded via include-book, the modified defun does not use the correct "old definition" for the original version of the function. This only appears to be an issue when loading a certified book - if the book is left uncertified or the events in the book are evaluated in the REPL, everything works as expected.

I'm using SBCL 2.1.11 and the latest ACL2 (commit 5223521d995b21b25ba828fcd9ba0e1bfa5920b2) on a Linux machine.

Take the following file, foo-test.lisp:

(in-package "ACL2")

(include-book "hacking/hacker" :dir :system)
(include-book "hacking/defcode" :dir :system :ttags ((defcode)))
(include-book "hacking/redefun" :dir :system)
(include-book "hacking/rewrite-code" :dir :system)
(include-book "hacking/raw" :dir :system)

(program)
(set-state-ok t)

(defun foo (x)
  (let ((y (cw "hi")))
    (declare (ignore y))
    x))

(defun foo-safe-mode-begin (state)
  (if (boundp-global 'foo-safe-mode state)
    (er soft 'foo-safe-mode-begin "Already in safe mode")
    (er-progn
     (assign foo-safe-mode t)
     (value :invisible))))

(push-untouchable foo-safe-mode nil)

(defun foo-safe-modep (state)
  (boundp-global 'foo-safe-mode state))

;; Danger ahead!
(defttag :modify-foo)

(make-event
 (let ((formals (getprop 'foo 'formals nil 'current-acl2-world (w state))))
   `(modify-raw-defun foo original-foo ,formals
                      (progn
                       (when (foo-safe-modep acl2::*the-live-state*)
                             (hard-error
                              'foo
                              "Cannot call foo in foo safe mode."
                              ()))
                       (original-foo . ,formals)))))

;; If the above commands are run in an ACL2 instance before the
;; following, everything works as expected. The first foo prints
;; "hi3", and the second foo prints an error saying that you can't
;; call foo in foo safe mode.

;; However, if this file is certified and loaded, then a call to foo
;; will result in an infinite loop.

;; My guess is that the old definition is not being saved correctly.
#|
(foo 3)
(foo-safe-mode-begin state)
(foo 3)
|#

My theory that the old definition is not being saved correctly is supported by the output of disassemble on foo and original-foo after loading the certified book: foo-disassembly.txt. Compare this to the output when the book is loaded without first certifying: foo-without-cert-disassembly.txt.

I'm not sure if modify-raw-defun was intended to work with certification and include-book, but I didn't find any documentation suggesting this is the case.

[MattKaufmann]

I haven't drilled down into this, but my strong guess is that the old defun is being saved in the .cert file, and that ACL2 was rebuilt on top of source files that were modified after the book was certified. A solution would then be to recertify the book any time the definition changes in the ACL2 sources. Perhaps there's a way to automate that with the build system; actually I think there is, by emulating the use of write-defrec-certdeps in books/build/cert_features.lsp using the get-event utility (which has :doc). I realize that I haven't worked this all out, but I hope it helps.

[mister-walter]

This occurs without having a rebuild of ACL2 in between when the certification was performed and when the book is included. I think that rules out your guess above, but I may be misinterpreting your comment?

[MattKaufmann]

Sorry, I probably shouldn't have said anything; I was just making a quick guess. But I haven't learned my lesson, so here's a wild guess: you could try using :check-expansion t with the make-event and see if that helps.

[mister-walter]

:check-expansion t did not fix the issue, but I was able to minimize the example to the following by looking at what modify-raw-defun expands into:

(in-package "ACL2")

(include-book "hacking/hacker" :dir :system)
(include-book "hacking/raw" :dir :system)

(program)
(set-state-ok t)

(defun foo (x)
  (+ x 1))

(defttag :modify-foo)
(in-raw-mode (setf (symbol-function 'original-foo)
                   (symbol-function 'foo)))
(in-raw-mode (defun foo (x)
               (+ 3 (original-foo x))))

Thanks for your follow-ups! Hopefully the minimization is helpful!

[MattKaufmann]

That's helpful, but I don't have an answer. I tried to make the problem simpler still by creating a book that doesn't use the hacking/ books, but then the infinite loop disappeared. Here's my attempt, in case that's helpful to you or anyone in solving this.

(in-package "ACL2")
(defun foo (x)
  (+ x 1))
(defttag t)
(progn!
 (set-raw-mode t)
 (setf (symbol-function 'original-foo)
       (symbol-function 'foo))
 (defun foo (x)
   (+ 3 (original-foo x)))
 (set-raw-mode nil))

[mister-walter]

Note that if you put ACL2 into program mode (e.g insert (program) right before the first defun foo), your attempt also results in an infinite loop. Similarly, if I remove the (program) from my minimized example, I do not get an infinite loop.

[MattKaufmann]

That's a big clue -- thanks! I'm reasonably confident that this behavior is a consequence of the way ACL2 handles early loading of compiled files. It's a complex mechanism that normally can accommodate hacks using trust tags, but apparently not this time. (If you want to know about it, you can read "Essay on Hash Table Support for Compilation" in ACL2 source file interface-raw.lisp.) Anyhow, the problem goes away if you set the symbol-function only once, as in the following book (using defvar so that the form is only evaluated once).

(in-package "ACL2")
(program)
(defun foo (x)
  (+ x 1))
(defttag t)
(progn!
 (set-raw-mode t)
 (defvar *fn* (symbol-function 'foo))
 (setf (symbol-function 'original-foo)
       *fn*)
 (defun foo (x)
   (+ 3 (original-foo x)))
 (set-raw-mode nil))

When I certified with (certify-book "foo-test2" 0 t :ttags :all) -- I called the above book foo-test2.lisp -- and then included that book in a fresh session, (foo 3) evaluated to 7 without a stack overflow.

I think that the use of program-mode made a difference because evaluation of foo used the raw-Lisp foo, not merely the 1 function (see :DOC evaluation if you want details). Adding, say, (declare (xargs :guard (natp x))) without program mode also creates the problem with symbol-function and that's also solved by use of defvar, above.

By the way, I don't consider this to be an ACL2 bug -- you get what you get when you do fancy raw-Lisp stuff with trust tags. (But such problems are rare as far as I know.)

[acoglio]

@mister-walter Do you think that this issue is resolved and could be closed?

[mister-walter]

Apologies for the extreme delay here. As Matt says, we're doing a bunch of hacky raw-Lisp stuff here so it's totally fair to consider this not to be an ACL2 bug. I'll close this now and post additional comments if I end up diving deeper into this issue.