• 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
        • Running-linux
        • Introduction
        • Asmtest
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
          • X86isa-state
          • Syscalls
          • Cpuid
          • Linear-memory
          • Rflag-specifications
          • Characterizing-undefined-behavior
          • Top-level-memory
          • App-view
          • X86-decoder
          • Physical-memory
          • Decoding-and-spec-utils
            • Read-operands-and-write-results
            • Effective-address-computations
            • Select-operand-size
            • Instruction-pointer-operations
            • Stack-pointer-operations
            • Select-segment-register
            • Prefix-modrm-sib-decoding
            • Select-address-size
            • Rex-byte-from-vex-prefixes
            • Check-instruction-length
            • Error-objects
              • Rip-guard-okp
              • Sib-decoding
            • Instructions
            • Register-readers-and-writers
            • X86-modes
            • Segmentation
            • Other-non-deterministic-computations
            • Environment
            • Paging
          • Implemented-opcodes
          • To-do
          • Proof-utilities
          • Peripherals
          • Model-validation
          • Modelcalls
          • Concrete-simulation-examples
          • Utils
          • Debugging-code-proofs
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Decoding-and-spec-utils

    Error-objects

    Utilities trafficking in erp objects

    We introduce several utilities trafficking in erp objects, each of which is a stack of individual error objects typically of the form (ctx . kwd-alist), where ctx is typically a function name. We do not enforce the shape of an individual error object, however.

    • !ms-erp: This macro assumes that erp is already bound to an error stack, and ctx is bound to the current context, which is typically the function name (a symbol).
    • !ms-erp-fresh: This is same as !ms-erp, but where erp is not bound and we bind it to nil.
    • !!ms: erp, ctx, and also x86 must already be bound. We return an updated x86 that has a non-nil ms field conveying useful information.
    • !!ms-fresh: ctx and x86 must already be bound.
    • !!fault-fresh: like !!ms-fresh but it updates the fault field instead.

    Macro: !ms-erp

    (defmacro !ms-erp (&rest args)
      (cons 'cons
            (cons (cons 'list (cons 'ctx args))
                  '(erp))))

    Macro: !ms-erp-fresh

    (defmacro !ms-erp-fresh (&rest args)
      (cons 'let
            (cons '((erp nil))
                  (cons (cons '!ms-erp args) 'nil))))

    Macro: !!ms

    (defmacro !!ms (&rest args)
      (cons '!ms
            (cons (cons '!ms-erp
                        (cons ':rip (cons '(rip x86) args)))
                  '(x86))))

    Macro: !!ms-fresh

    (defmacro !!ms-fresh (&rest args)
      (cons '!ms
            (cons (cons '!ms-erp-fresh
                        (cons ':rip (cons '(rip x86) args)))
                  '(x86))))

    Macro: !!fault-fresh

    (defmacro !!fault-fresh (&rest args)
      (cons '!fault
            (cons (cons '!ms-erp-fresh
                        (cons ':rip (cons '(rip x86) args)))
                  '(x86))))