Merge branch 'testing' of github.com:acl2/acl2

axioms.lisp

@@ -12727,6 +12727,7 @@ evaluated.  See :DOC certify-book, in particular, the discussion about ``Step
     sys-call-status ; *last-sys-call-status*
     sys-call ; system-call
     sys-call+ ; system-call+
+    sys-call* ; system-call+
 
     canonical-pathname ; under dependent clause-processor
 
@@ -15627,6 +15628,16 @@ evaluated.  See :DOC certify-book, in particular, the discussion about ``Step
                        (alistp (table-alist 'acl2-defaults-table wrld)))))
   (cdr (assoc-eq :ttag (table-alist 'acl2-defaults-table wrld))))
 
+(defun get-register-invariant-risk-world (wrld)
+  (declare (xargs :guard
+                  (and (plist-worldp wrld)
+                       (alistp (table-alist 'acl2-defaults-table wrld)))))
+  (let ((pair (assoc-eq :register-invariant-risk
+                        (table-alist 'acl2-defaults-table wrld))))
+    (cond (pair (cdr pair))
+          (t ; default
+           t))))
+
 (table acl2-defaults-table nil nil
 
 ; Warning: If you add or delete a new key, there will probably be a change you
@@ -15760,6 +15771,16 @@ evaluated.  See :DOC certify-book, in particular, the discussion about ``Step
                                 the :check-invariant-risk key to nil in the ~
                                 acl2-defaults-table."
                                nil)))))
+        ((eq key :register-invariant-risk)
+         (or (eq val t)
+             (and (eq val nil)
+                  (or (null (get-register-invariant-risk-world world))
+                      (ttag world)
+                      (illegal 'acl2-defaults-table
+                               "An active trust tag is required for setting ~
+                                the :register-invariant-risk key to nil in ~
+                                the acl2-defaults-table."
+                               nil)))))
         ((eq key :user)
 
 ; The :user key is reserved for users; the ACL2 system will not consult or
@@ -19051,16 +19072,41 @@ evaluated.  See :DOC certify-book, in particular, the discussion about ``Step
 (defvar *last-sys-call-status* 0)
 
 (defun sys-call (command-string args)
-  (declare (xargs :guard t))
+  (declare (xargs :guard (and (stringp command-string)
+                              (string-listp args))))
   #+acl2-loop-only
   (declare (ignore command-string args))
   #-acl2-loop-only
-  (let ((rslt (system-call command-string args)))
-    (progn (setq *last-sys-call-status* rslt)
-           nil))
+  (cond
+   ((or (f-get-global 'in-prove-flg *the-live-state*)
+        (f-get-global 'in-verify-flg *the-live-state*))
+
+; We use (er hard ...) rather than (er hard! ...) to avoid a distracting error
+; when reasoning about calls of sys-call on concrete data during a proof.  We
+; really only want to see this error message when sys-call is invoked by a
+; metafunction or a clause-processor.
+
+    (er hard 'sys-call
+        "It is illegal to call ~x0 inside the ~s1.  Consider using ~x2 ~
+         or ~x3 instead."
+        'sys-call
+        (if (f-get-global 'in-prove-flg *the-live-state*)
+            "prover"
+          "proof-builder")
+        'sys-call+
+        'sys-call*))
+   (t
+    (let ((rslt (system-call command-string args)))
+      (progn (setq *last-sys-call-status* rslt)
+             nil))))
   #+acl2-loop-only
   nil)
 
+; Avoid running sys-call on terms.  We already prevent this under prover and
+; proof-builder calls, but not for example under the expander from community
+; book books/misc/expander.lisp.
+(in-theory (disable (:executable-counterpart sys-call)))
+
 (defun sys-call-status (state)
   (declare (xargs :stobjs state))
   #-acl2-loop-only
@@ -19099,29 +19145,56 @@ evaluated.  See :DOC certify-book, in particular, the discussion about ``Step
 (in-theory (disable update-acl2-oracle))
 
 (defun sys-call+ (command-string args state)
-  (declare (xargs :stobjs state))
+  (declare (xargs :stobjs state
+                  :guard (and (stringp command-string)
+                              (string-listp args))))
   #+acl2-loop-only
   (declare (ignore command-string args))
-  #+acl2-loop-only
+  #-acl2-loop-only
+  (when (live-state-p state)
+    (return-from sys-call+
+      (multiple-value-bind
+          (status rslt)
+          (system-call+ command-string args)
+        (mv (if (eql status 0)
+                nil
+              status)
+            rslt
+            state))))
   (mv-let (erp1 erp state)
-          (read-acl2-oracle state)
-          (declare (ignore erp1))
-          (mv-let (erp2 val state)
-                  (read-acl2-oracle state)
-                  (declare (ignore erp2))
-                  (mv (and (integerp erp)
-                           (not (eql 0 erp))
-                           erp)
-                      (if (stringp val) val "")
-                      state)))
+    (read-acl2-oracle state)
+    (declare (ignore erp1))
+    (mv-let (erp2 val state)
+      (read-acl2-oracle state)
+      (declare (ignore erp2))
+      (mv (and (integerp erp)
+               (not (eql 0 erp))
+               erp)
+          (if (stringp val) val "")
+          state))))
+
+(defun sys-call* (command-string args state)
+  (declare (xargs :stobjs state
+                  :guard (and (stringp command-string)
+                              (string-listp args))))
+  #+acl2-loop-only
+  (declare (ignore command-string args))
   #-acl2-loop-only
-  (multiple-value-bind
-      (status rslt)
-      (system-call+ command-string args)
-    (mv (if (eql status 0)
+  (when (live-state-p state)
+    (return-from sys-call*
+      (let ((status (system-call command-string args)))
+        (mv (if (eql status 0)
+                nil
+              status)
             nil
-          status)
-        rslt
+            state))))
+  (mv-let (erp1 erp state)
+    (read-acl2-oracle state)
+    (declare (ignore erp1))
+    (mv (and (integerp erp)
+             (not (eql 0 erp))
+             erp)
+        nil
         state)))
 
 ; End of system calls
@@ -26404,6 +26477,7 @@ Lisp definition."
     (set-temp-touchable-fns)
     (set-temp-touchable-vars)
     (sys-call)
+    (sys-call*)
     (sys-call+)
     ))
 

basis-a.lisp

@@ -6080,20 +6080,11 @@
 ; stobj (introduced after x).  We return nil if x is not either sort of valid
 ; type spec.
 
-; Our intended use of this function is in generation of guards for field
-; accessors and updaters, in the case of fields that are themselves stobjs.
-; When the defstobj is introduced, there are no stobj declarations, so the
-; subfield's recognizer (stobj-recog, below) is called on an ordinary object.
-; We started allowing such calls when translating for execution after
-; Version_6.1; see translate11-call.
-
-; Presumably the two arguments of OR below -- the guard corresponding to the
-; type x, and the stobj recognizer term -- cannot both be non-nil, since types
-; are in the main Lisp package and hence cannot be stobj names.  Nevertheless,
-; in case we're wrong about that, we translate the type first, in order to
-; avoid ambiguity in case there is a stobj previously defined locally in a book
-; or encapsulate, for example (which would cause x to translate as a type in
-; the first pass but to a type in the second pass).
+; Our intended use of this function is in generation of guards for recognizers
+; of stobj fields that may themselves be stobjs.  We do not use this however in
+; accessors or updators, where translate-declaration-to-guard suffices: we do
+; not want to generate a stobj recognizer since the child stobj is supplied
+; explicitly using :stobjs.
 
   (or (translate-declaration-to-guard x var wrld)
       (let ((stobj-recog (and (not (eq x 'state))
@@ -6515,7 +6506,8 @@
    ((symbolp pat)
     (cond
      ((or (eq pat t)
-          (eq pat nil))
+          (eq pat nil)
+          (keywordp pat))
       (mv (cons (list 'eq x pat) tests) bindings))
      ((and (> (length (symbol-name pat)) 0)
            (eql #\* (char (symbol-name pat) 0)))

books/add-ons/hash-stobjs.lisp

@@ -703,20 +703,31 @@
              (hashp (and (consp type) (eq (car type) 'hash-table)))
              (hash-test (and hashp (cadr type)))
 ;   >---
+             (array-etype (and arrayp (cadr type)))
+             (stobj-formal
+              (cond (arrayp (and (not (eq array-etype 'state))
+                                 (stobjp array-etype t wrld)
+                                 array-etype))
+                    (t (and (not (eq type 'state))
+                            (stobjp type t wrld)
+                            type))))
+             (v-formal (or stobj-formal 'v))
+             (stobj-xargs (and stobj-formal
+                               `(:stobjs ,stobj-formal)))
              (type-term            ; used in guard
               (and (not arrayp)    ; else type-term is not used
 ;---<
                    (not hashp)
 ;   >---
                    (if (null wrld) ; called from raw Lisp, so guard is ignored
                        t
-                     (translate-stobj-type-to-guard type 'v wrld))))
-             (array-etype (and arrayp (cadr type)))
+                     (translate-declaration-to-guard type v-formal wrld))))
              (array-etype-term     ; used in guard
               (and arrayp          ; else array-etype-term is not used
                    (if (null wrld) ; called from raw Lisp, so guard is ignored
                        t
-                     (translate-stobj-type-to-guard array-etype 'v wrld))))
+                     (translate-declaration-to-guard array-etype v-formal
+                                                     wrld))))
              (array-length (and arrayp (car (caddr type))))
              (accessor-name (access defstobj-field-template
                                     field-template
@@ -774,26 +785,38 @@
                            (list (cons #\0 ',accessor-name)
                                  (cons #\1 ',var)))
                           ,var)))
-              (,accessor-name (i ,var)
-                              (declare (xargs :guard
-                                              (and (,top-recog ,var)
-                                                   (integerp i)
-                                                   (<= 0 i)
-                                                   (< i (,length-name ,var)))
-                                              :verify-guards t))
-                              (nth i (nth ,n ,var)))
-              (,updater-name (i v ,var)
+             (,accessor-name (i ,var)
                              (declare (xargs :guard
                                              (and (,top-recog ,var)
                                                   (integerp i)
                                                   (<= 0 i)
-                                                  (< i (,length-name ,var))
-                                                  ,@(if (eq array-etype-term
-                                                            t)
-                                                        nil
-                                                      (list array-etype-term)))
+                                                  (< i (,length-name ,var)))
                                              :verify-guards t))
-                             (update-nth-array ,n i v ,var)))
+                             (nth i (nth ,n ,var)))
+             (,updater-name (i ,v-formal ,var)
+                            (declare
+                             (xargs :guard
+                                    (and (,top-recog ,var)
+                                         (integerp i)
+                                         (<= 0 i)
+                                         (< i (,length-name ,var))
+
+; We avoid laying down the stobj recognizer twice for a child stobj (although
+; that would nevertheless be removed by the use of stobj-optp).
+
+                                         ,@(and (not stobj-xargs)
+                                                (assert$
+                                                 array-etype-term
+                                                 (if (eq array-etype-term
+                                                         t)
+                                                     nil
+                                                   (list array-etype-term)))))
+                                    :verify-guards t
+                                    ,@stobj-xargs))
+                            ,(if stobj-formal
+                                 `(non-exec
+                                   (update-nth-array ,n i ,v-formal ,var))
+                               `(update-nth-array ,n i ,v-formal ,var))))
            (defstobj-field-fns-axiomatic-defs
              top-recog var (+ n 1) (cdr field-templates) wrld)))
 ;---<
@@ -872,14 +895,25 @@
                              (declare (xargs :guard (,top-recog ,var)
                                              :verify-guards t))
                              (nth ,n ,var))
-             (,updater-name (v ,var)
+             (,updater-name (,v-formal ,var)
                             (declare (xargs :guard
-                                            ,(if (eq type-term t)
+                                            ,(if (or (eq type-term t)
+
+; We avoid laying down the stobj recognizer twice for a child stobj (although
+; that would nevertheless be removed by the use of stobj-optp).
+
+                                                     stobj-xargs)
                                                  `(,top-recog ,var)
-                                               `(and ,type-term
-                                                     (,top-recog ,var)))
-                                            :verify-guards t))
-                            (update-nth ,n v ,var)))
+                                               (assert$
+                                                type-term
+                                                `(and ,type-term
+                                                      (,top-recog ,var))))
+                                            :verify-guards t
+                                            ,@stobj-xargs))
+                            ,(if stobj-formal
+                                 `(non-exec
+                                   (update-nth ,n ,v-formal ,var))
+                               `(update-nth ,n ,v-formal ,var))))
            (defstobj-field-fns-axiomatic-defs
              top-recog var (+ n 1) (cdr field-templates) wrld))))))))