Note-2-7-bug-fixes
ACL2 Version 2.7 Notes on Bug Fixes
Francisco J. Martin-Mateos emailed us a soundness bug (!) in our
handling of functional instantiation (for example see functional-instantiation-example). We are grateful for that email, which
clearly illustrated the problem. It is included just below the definition of
push-clause in ACL2 source file prove.lisp, where we have fixed the
bug. This bug was fixed in a re-release of Version 2.6 in February, 2002.
Rob Sumners emailed us a soundness bug (!) in function commutative-p1,
which is used by the ACL2 bdd package. We are grateful for his help;
his email gave a proof of nil and also pointed to the problem function. This
bug was fixed in a re-release of Version 2.6 in February, 2002.
We discovered and fixed a soundness bug illustrated by the book below,
which was certifiable in Version 2.6 and ends in a proof of nil. The
event (verify-guards foo) should have been rejected, because foo
calls a function whose guards have not been verified, namely, bar.
However, ACL2 did not notice the call of function bar in the body of
foo because it was looking in the simplified (normalized) body of
foo rather than in the original body of foo. During processing of
the book below, the logical definition of zp is used before
(verify-guards foo), and (zp -3) reduces to t in the logic.
After (verify-guards foo), ACL2 simplifies (foo -3) by going into
raw Lisp, where (zp -3) is evaluated and reduces to nil.
(in-package "ACL2")
(defun bar (x)
(zp x))
(defthm zp-false-on-negatives
(implies (< x 0)
(bar x))
:rule-classes :type-prescription)
(defun foo (x)
(declare (xargs :guard (rationalp x)
:verify-guards nil))
(if (< x 0)
(if (bar x) 0 1) ; simplified body reduces this line to 0
17))
(defthm foo-of-minus-3-is-0
(equal (foo -3) 0)
:rule-classes nil)
(verify-guards foo)
(defthm foo-of-minus-3-is-1
(equal (foo -3) 1)
:rule-classes nil)
(defthm bug
nil
:rule-classes nil
:hints (("Goal" :use (foo-of-minus-3-is-0 foo-of-minus-3-is-1))))
The above bug exploited the fact that zp has a different definition
in raw Lisp than in the logic for arguments that violate its guard). The
following example caused a hard error in raw Lisp, though not a soundness
error.
(in-package "ACL2")
(defun bar (x)
(cons (car x) (car x)))
(defun foo (x)
(declare (xargs :guard t
:verify-guards nil))
(if (bar x) x nil))
(verify-guards foo)
(defthm bug
(equal (foo 3) t)
:rule-classes nil)
We have made a minor change to the notion of the formula of a
function symbol, related to the change above, which however is unlikely to be
noticeable.
In order to make it harder to hit problems like the guard problem above, we
have slightly modified the raw Lisp definition of zp.
A break-rewrite command, :ancestors, was broken, but has been
fixed. Thanks to Eric Smith for bringing the problem to our attention, and to
Robert Krug for supplying the final part of the fix.
Some proof-builder commands caused errors when all goals have
already been proved. This has been fixed. Thanks to Matt Wilding for
reporting this bug.
Fixed a bug in :comp. When compiling uncompiled functions
with very large definitions, ACL2 was inserted a backslash (\) character
into generated files.
Fixed the :type-alist :brr command (see brr-commands), whose output was difficult to read when typed after an
:eval..
Fixed some clumsy handling of errors when including an uncertified book,
for example, with the error message when including an uncertified book with a
bad deftheory event. Thanks to Eric Smith for pointing out this
problem.
Two modifications to certify-book now cause it to reflect natural
expectations with respect to soundness. First, it now has default values of
nil instead of t for keyword arguments :skip-proofs-okp and
:defaxioms-okp. Thanks to Robert Krug for suggesting this change and the
ACL2 seminar at the University of Texas for discussing it. Second, when
:skip-proofs-okp (respectively, :defaxioms-okp) is nil, either
explicitly or by default, then skip-proofs commands (respectively,
defaxiom events) are disallowed inside any included books, regardless
of the keyword parameters passed to include-book. This had not been
the case for previous versions of ACL2, regardless of the values of
:skip-proofs-okp or :defaxioms-okp passed to include-book.
Improved warnings and errors for certify-book and include-book to mention the portcullis as a possible source of skip-proofs and defaxioms.
ACL2 formerly caused an error when hints in a :corollary were not well-formed. This situation could arise as follows when
certifying a book. A lemma FOO is proved locally to the book (or, is
present in a sub-book that is included locally). The :corollary of a
subsequent theorem, BAR, disables that rule in a hint. When BAR is proved,
this is not a problem. But certify-book makes a second pass after
processing the events in a book: it essentially does an include-book.
During the include-book pass, FOO is not known (because it was local), and therefore ACL2 fails to process the disable of FOO in an
in-theory hint. The fix is that during include-book, hints are ignored in corollaries just as they have been for the main theorem
(or definition).
It was possible for guard verification to succeed where it should have
failed. We have fixed the bug (which was in source function (ironically
named!) fcons-term-smart). Thanks to Robert Krug for sending us an
example of bungled guard verification. It turns out that this bug was also
present in Version_2.6.
The proof-builder command = has been improved. Formerly, it
could fail to apply when certain implies terms were in the context.
Thanks to Pete Manolios for bringing this problem to our attention.
The command add-binop failed to work. This has been fixed. Thanks
to Rob Sumners for pointing out this problem. Also see note-2-7-other
for a discussion of how this and another table are no longer part of
the ACL2-defaults-table.
Book certification could cause a segmentation fault in cases where the
certification world (see certify-book) has a very large number of
events. This has been fixed.
We now allow empty :use hints and empty hints, as requested by
Eric Smith. Examples:
("Goal" :use ())
("Goal")
A large mutual-recursion nest could cause a stack overflow when
executing either :pr FN, :pr! FN, or :monitor (:definition FN)
t, where FN is in that large mutual recursion nest. This has been
fixed (implementation detail: function actual-props has been made
tail-recursive). NOTE: If you just want the definition of FN,
:pf FN can be much faster than :pr FN if
FN is in a large mutual-recursion.
Hard Lisp errors could occur when including uncertified books. This has
been fixed; ACL2 now does syntax-checking formerly omitted when including
uncertified books.
Previously, the evaluation of defstobj and mutual-recursion
forms could cause ``undefined'' warnings when the form was compiled. This has
been fixed. Thanks to Eric Smith for bringing a mutual-recursion example
to our attention.
A bug has been fixed in the syntactic check for valid :loop-stopper values. Formerly, valid :loop-stopper values were
erroneously restricted to lists of length at most 2 (a minor problem, since
these lists typically have length 1), and the function symbol(s) need not have
been defined in the current ACL2 world. Thanks to Eric Smith for
sending an example to demonstrate the latter problem.
Functions definitions that are :non-executable (see xargs) had
never been recognized as redundant, but this has been fixed. Thanks to Vernon
Austel for pointing out this problem.
Compilation using :comp now compiles user-defined :program mode functions. Formerly only :logic mode functions
could be compiled using :comp.
Handling of :by hints has been improved in essentially three ways.
The primary change is that now, when the current goal exactly matches the
supplied lemma instance, the subsumption test will always succeeds (see hints, in particular the discussion of :by). Second, certain proof
failures involving :by hints were failing silently, with duplicate
messages ``As indicated by the hint, this goal is subsumed by....'' This
could happen when the original goal was among the goals generated by applying
the hint. This problem has been fixed by no longer considering this proof
step to be specious (see specious-simplification). Third and finally,
when the lemma-instance refers to a definition, the original body of
that definition is used rather than the simplified (``normalized'') body.
In addition to the above, we now recognize more cases of specious
simplification (see specious-simplification). Thanks to Eric Smith for
bringing this issue to our attention.
Fixed building of ACL2 under CLISP so that (1) the appropriate ACL2 startup
message is printed out when ACL2 starts up, and (2) the lisp process supplied
to make, e.g., LISP=/usr/bin/clisp, is the one written out to the saved ACL2
file. Thanks to Dave Greve and Noah Friedman for suggesting (2). Also, ACL2
now works with CLISP 2.30. We have accommodated a change in CLISP's handling
of streams and its package-locking mechanism, as well as certain non-standard
characters that formerly could cause CLISP 2.30 to break, even when those
characters are in comments.
Eliminated compiler warnings for CMU Lisp.
Fixed an incorrect error supplied when book certification proceeded so
quickly that the file write dates of the book (.lisp file) and the
corresponding compiled file are equal. Now that error only occurs if the
compiled file has a strictly earlier write date, which probably should never
happen.
Fixed an infinite loop when executing make clean-books (and hence
`make' with targets that call clean-books, namely,
certify-books-fresh, regression-fresh, and
regression-nonstd-fresh), which could occur when any subdirectories of
books/ are missing — even workshops/, which is intended to be
optional. Thanks to Pete Manolios for pointing out this bug.
The include-book command now works properly even when filenames, or
their directories or parent directories (etc.) are links. Thanks to Matt
Wilding for pointing out this problem.
The commands :puff :puff* have been fixed.
Formerly, there was a bug when :puff or :puff* caused the execution
of an include-book for an absolute pathname, P, that was
other than the current connected book directory (see cbd). When
including P, any subsidiary include-book with a relative pathname
would be erroneously considered relative to the current cbd rather
than relative to the directory of P. Thanks to Pete Manolios and Matt
Wilding for pointing out this problem.
It had been possible in a ``large'' ACL2 image to call verify-termination successfully on built-in function sys-call, with
undesirable results. This hole has been plugged. Thanks to Rob Sumners for
pointing out this problem. The new function gc$ must also stay in
:program mode.
ACL2 no longer warns when certifying a book based on local
functions whose guards have not yet been verified. Thanks to Pete
Manolios for pointing out this issue.
An occasional ``slow array warning'' had been possible during proofs. The
following sequence shows how to evoke that warning in previous versions.
(in-theory (disable binary-append))
(in-theory (enable binary-append))
(in-theory (disable binary-append))
(ubt 2)
(thm (equal (car (cons x y)) x))
(See note-2-7-other for a discussion of a change to compress1 in support of this fix; however, users should not need to read that
discussion.)
The raw Lisp code for defchoose had a small bug, which was only
evidenced in CLISP implementations as far as we know. It has been fixed.
When ld is applied to a stringp file name, it now temporarily sets
the connected book directory (see cbd) to the directory of that file
while evaluating forms in that file. To see the effect of this change,
imagine a subdirectory "sub" of the current directory, and imagine
executing (ld "sub/foo.lisp"), where file foo.lisp contains the
form (include-book "bar"). Presumably the intention was to consider
the file bar.lisp in the same directory, sub/, as foo.lisp.
Ld now honors that intention, but in previous versions "bar.lisp"
would have been a reference to a file in the current directory, not in
sub/.
For users of run-acl2 [perhaps there are none!]: A fix has been
provided by a Debian user via Camm Maguire so that acl2-mode will work in
Xemacs, which apparently uses variable lisp-mode-shared-map rather than
shared-lisp-mode-map.
ACL2 has, for a long time (always?), had a mechanism for avoiding
re-proving constraints generated by :functional-instance lemma-instances in :use and :by hints. But this mechanism had not
applied to defined (as opposed to constrained) functions. This has been
fixed. Thanks to Francisco J. Martin-Mateos (ChesKo) for pointing out this
problem by sending a clear example.
