1. Quoting :doc note-4-4:

| Improvements have been made related to the reading of characters.  In
| particular, checks are now done for ASCII encoding and for the expected
| char-code values for Space,Tab,Newline,Page, and
| Rubout.  Also, an error no longer occurs with certain uses of
| non-standard characters.  For example, it had caused an error to certify a
| book after a single portcullis command of
| (make-event `(defconst *my-null* ,(code-char 0))); but this is no longer
| an issue.  Thanks to Jared Davis for helpful correspondence that led us to
| make these improvements.

2. Do not read .port file when include-book is done under certification.

Author: MattKaufmann

acl2-characters

@@ -159,28 +159,125 @@ most-negative-fixnum = ~s."
 ;                           ACL2 CHARACTERS
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-; At one time we read the legal ACL2 characters from a string in a file, so
-; that we could be confident that we know exactly what they are.  But if
-; code-char is not a function, then we lose anyhow, because we have defined it
-; in ACL2.  And if code-char is a function, then we can do our checking without
-; having to get the characters from a file, the idea being that the range of
-; code-char on {0,1,...,255} is exactly the set of legal ACL2 characters.
-
-; Note that this issue is orthogonal to the problem of ensuring that #\c is
-; read in as the same character in different ACL2 sessions, for any ACL2
-; character c.  (Even #\Newline is potentially problematic, as its char-code is
-; 10 in most Common Lisps but is 13 in MCL!)  Because of the latter issue, our
-; story about ACL2 could include a caveat that certified books may only be
-; soundly loaded into the same Lisp image in which they were certified.  When
-; we say ``same lisp image'' we don't mean the same exact process necessarily,
-; but rather simply an invocation of the same saved image.  Another reason for
-; such a caveat, independent of the character-reading issue, is that different
-; saved images may be tied into different compilers, thus making the object
-; files of the books incompatible.
-
-; However, we believe that we can prevent the most serious assaults on
-; soundness due to implementation dependencies, simply by making notes in the
-; version string, state global 'acl2-version; see :DOC version.
+; It is difficult or impossible to ensure that #\c is read in as the same
+; character in different ACL2 sessions, for any ACL2 character c.  (Even
+; #\Newline is potentially problematic, as its char-code is 10 in most Common
+; Lisps but is 13 in [now-obsolete] MCL!)  Thus, the soundness of ACL2 rests on
+; a caveat that all books are certified using the same Lisp image.  When we say
+; ``same lisp image'' we don't mean the same exact process necessarily, but
+; rather, an invocation of the same saved image.  Another reason for such a
+; caveat, independent of the character-reading issue, is that different saved
+; images may be tied into different compilers, thus making the object files of
+; the books incompatible.
+
+; Nevertheless, it would of course be nice if all host Lisp implementations of
+; ACL2 actually do agree on character and string constants provided by the Lisp
+; reader (based on *acl2-readtable*).  Our first check is intended to address
+; this point, by providing some confidence that the host Lisp has an ASCII
+; character set.  As explained above, we only intend soundness in the case that
+; all books are certified from scratch using the same host Lisp, and we do not
+; actually assume ASCII characters -- more precisely, we do not assume any
+; particular values for code-char and code-char -- so this check is not really
+; necessary, except for a claim about ASCII characters in "Precise Description
+; of the ACL2 Logic", which should perhaps be removed.  However, as of January
+; 2012 we seem to be able to make the following check in all supported Lisps,
+; at least on our Linux and Mac OS platforms.  It should be sound for users to
+; comment out this check, but with the understanding that ACL2 is taking
+; whatever the Lisp reader (using *acl2-readtable*) gives it.
+
+(let ((filename "acl2-characters"))
+
+; Why do we read from a separate file, rather than just saving the relevant
+; characters in the present file?  For example, it may seem reasonable to use a
+; trusted host Lisp to obtain an alist by evaluating the following expression.
+
+; (loop for i from 0 to 255 do (princ (cons i (code-char i))))
+
+; Could the resulting the alist be placed into this file and used for the check
+; below?
+
+; We run into a problem right away with that approach because of Control-D.
+; For example, try this
+
+; (princ (cons 4 (code-char 4)))
+
+; and then try quoting the output and reading it back in.  Or,
+; try evaluating the following.
+
+; (read-from-string (format nil "~a" (code-char 4)))
+
+; We have seen an error in both cases.
+
+; So instead, we originally generated the file acl2-characters as follows,
+; using an ACL2 image based on CCL.
+
+; (with-open-file (str "acl2-characters" :direction :output)
+;                 (loop for i from 0 to 255
+;                       do (write-char (code-char i) str)))
+
+  (with-open-file
+   (str filename :direction :input
+
+; In SBCL and CLISP we have found the need to specify :external-format in order
+; to avoid errors.  Note that (for example) in our SBCL,
+; (stream-external-format *terminal-io*) evaluates to (:UTF-8 :REPLACEMENT
+; #\REPLACEMENT_CHARACTER).
+
+        #+(or clisp sbcl) :external-format
+        #+sbcl :iso-8859-1
+        #+clisp
+; The following came from
+; http://en.wikibooks.org/wiki/Common_Lisp/Advanced_topics/Files_and_Directories
+; in January 2012.
+        (ext:make-encoding :charset 'charset:iso-8859-1
+                           :line-terminator :unix))
+   (loop for i from 0 to 255
+
+; The function legal-acl2-character-p, called in bad-lisp-objectp for
+; characters and strings, checks that the char-code of any character that is
+; read must be between 0 and 255.
+
+         do (let ((temp (read-char str)))
+              (when #-clisp (not (eql (char-code temp) i))
+
+; In CLISP we find character 10 (Newline) at position 13 (expected Return).
+; Perhaps this has something to do CLISP's attempt to comply with the CL
+; HyperSpec Section 13.1.8, "Treatment of Newline during Input and Output".
+; But something is amiss.  Consider for example the following log (with some
+; output edited in the case of the first two forms, but no editing of output
+; for the third form).
+
+; ACL2 [RAW LISP]> (with-open-file (str "tmp" :direction :output)
+;                                  (write-char (code-char 13) str))
+; #\Return
+; ACL2 [RAW LISP]> (with-open-file (str "tmp" :direction :input)
+;                                  (equal (read-char str) (code-char 10)))
+; T
+; ACL2 [RAW LISP]> (format nil "~a" (code-char 13))
+; "
+; ACL2 [RAW LISP]> 
+
+; So our check for CLISP is incomplete, but as explained in the comment just
+; above this check, we can live with that.
+
+                    #+clisp
+                    (and (not (eql (char-code temp) i))
+                         (not (eql i 13)))
+                (error "Bad character in file ~s: character ~s at position ~s."
+                       filename (char-code temp) i))))))
+
+; The check just above does not say anything about the five character names
+; that we support (see acl2-read-character-string), as described in :doc
+; characters; so we add suitable checks on these here.
+
+(loop for pair in (pairlis '(#\Space #\Tab #\Newline #\Page #\Rubout)
+                           '(32 9 10 12 127))
+      do (let* ((ch (car pair))
+                (code (cdr pair))
+                (val (char-code ch)))
+           (or (eql val code)
+               (error "(char-code ~s) evaluated to ~s (expected ~s)."
+                      ch val code))))
 
 ; Test that all purportedly standard characters are standard, and vice versa.
 

acl2-check.lisp

@@ -1,3 +1,3 @@
 "$Revision$"
-Mon Jan  2 18:01:03 CST 2012
+Mon Jan  9 09:51:15 CST 2012
 Books Revision: 934

acl2-startup-info.txt

@@ -1306,6 +1306,9 @@ which is saved just in case it's needed later.")
    #\u
    #'sharp-u-read))
 
+(defvar *old-character-reader*
+  (get-dispatch-macro-character #\# #\\))
+
 (defun modify-acl2-readtable (do-all-changes)
   (let ((*readtable* *acl2-readtable*))
 
@@ -1405,6 +1408,10 @@ which is saved just in case it's needed later.")
     (set-dispatch-macro-character #\#
                                   #\=
                                   #'reckless-sharp-equal-read)
+    (set-dispatch-macro-character
+     #\#
+     #\\
+     *old-character-reader*)
 
 ; Thanks to Jared Davis for contributing the code for #\Z and #\z (see
 ; serialize-raw.lisp).  But is this readtable even necessary now that

acl2.lisp

@@ -5,6 +5,7 @@ Makefile
 # README-images.html -- developer file
 # The following is distributed but is not in the svn repository:
 TAGS
+acl2-characters
 acl2-check.lisp
 acl2-fns.lisp
 acl2-init.lisp

all-files.txt

@@ -26066,6 +26066,7 @@
     with-parallelism-hazard-warnings ; for #+acl2-par
     warn-about-parallelism-hazard ; for #+acl2-par
     state-global-let* ; raw Lisp version for efficiency
+    with-reckless-readtable
     ))
 
 (defmacro with-live-state (form)
@@ -44951,6 +44952,24 @@ Lisp definition."
                   '(:bt :break-bt :bt-break))
        (print-call-history)))
 
+(defmacro with-reckless-readtable (form)
+
+; This macro creates a context in which reading takes place without usual
+; checks that #n# is only used after #n= and without the usual restrictions on
+; characters (specifically, *old-character-reader* is used rather than the ACL2
+; character reader, #'acl2-character-reader).  See *reckless-acl2-readtable*.
+
+  #+acl2-loop-only
+  form
+  #-acl2-loop-only
+  `(let ((*readtable* *reckless-acl2-readtable*)
+
+; Since print-object$ binds *readtable* to *acl2-readtable*, we bind the latter
+; here:
+
+         (*acl2-readtable* *reckless-acl2-readtable*))
+     ,form))
+
 (defmacro set-debugger-enable (val)
 
 ; WARNING: Keep this documentation in sync with the initial setting of

axioms.lisp

@@ -18352,6 +18352,16 @@
   called without a ~c[:ttagsx] argument supplied, then the value of ~c[:ttagsx]
   defaults to the (explicit or default) value of the ~c[:ttags] argument.
 
+  Improvements have been made related to the reading of characters.  In
+  particular, checks are now done for ASCII encoding and for the expected
+  ~ilc[char-code] values for ~c[Space],~c[Tab],~c[Newline],~c[Page], and
+  ~c[Rubout].  Also, an error no longer occurs with certain uses of
+  non-standard characters.  For example, it had caused an error to certify a
+  book after a single ~il[portcullis] ~il[command] of
+  ~c[(make-event `(defconst *my-null* ,(code-char 0)))]; but this is no longer
+  an issue.  Thanks to Jared Davis for helpful correspondence that led us to
+  make these improvements.
+
   ~st[NEW FEATURES]
 
   A new ``tau system'' provides a kind of ``type checker.''  ~l[tau-system].