• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Booting-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
        • Structures
        • Utilities
          • Constants-conversions-and-bounds
          • Globally-disabled-events
          • Mk-name
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Utilities

Globally-disabled-events

A ruleset containing all the events supposed to be mostly globally disabled in our books

The macro globally-disable adds its argument --- either a ruleset or an event --- to the ruleset called globally-disabled-events, and then disables globally-disabled-events.

Use the following form to see the events in this ruleset:

(show-globally-disabled-events-ruleset) 

The idea behind having a globally-disabled-events ruleset is to provide some indication to the user of these books which events are supposed to be mostly disabled throughout the books. This ruleset does NOT reflect the enabled status of these events at any point, i.e., we do not guarantee that an event FOO in this ruleset will be disabled everywhere in these books.

If you need to enable some events in globally-disabled-events during book/proof development, it is recommended to do so locally.

Use the following form to see the current status (enabled or disabled) of the events in the globally-disabled-events ruleset:

(show-globally-disabled-events-status) 

show-globally-disabled-events-status simply calls disabledp recursively on the events in globally-disabled-events.

Definitions and Theorems

Function: globally-disable-fn

(defun globally-disable-fn (events)
 (declare (xargs :guard t))
 (let ((__function__ 'globally-disable-fn))
  (declare (ignorable __function__))
  (b* ((events (if (true-listp events)
                   (cons 'quote (cons events 'nil))
                 events)))
   (cons
       'progn
       (cons (cons 'add-to-ruleset
                   (cons 'globally-disabled-events
                         (cons events 'nil)))
             '((in-theory (disable* globally-disabled-events))))))))

Function: show-globally-disabled-events-fn

(defun show-globally-disabled-events-fn (state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((__function__ 'show-globally-disabled-events-fn))
    (declare (ignorable __function__))
    (let ((world (w state)))
      (ruleset-theory 'globally-disabled-events))))

Function: disabledp-lst

(defun disabledp-lst (lst count state)
 (declare (xargs :stobjs (state)))
 (if
  (endp lst)
  (mv
     (cw "~%~%Number of events in GLOBALLY-DISABLED-EVENTS: ~x0~%~%"
         count)
     :invisible state)
  (b* ((- (cw "~%-- ~x0 ~%~t1 ~x2~%" (car lst)
              1 (or (disabledp (car lst)) :enabled))))
    (disabledp-lst (cdr lst)
                   (1+ count)
                   state))))