• 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
        • 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

Check-instruction-length

Check if the length of an instruction exceeds 15 bytes.

Signature

(check-instruction-length start-rip temp-rip delta-rip) 
  → 
badlength?

Returns

badlength? — Type (acl2::maybe-natp badlength?).

The maximum length of an instruction is 15 bytes; a longer instruction causes a #GP(0) exception. See AMD manual, Dec'17, Volume 2, Table 8-6. This function is used to check this condition.

The start-rip argument is the instruction pointer at the beginning of the instruction. The temp-rip argument is generally the instruction pointer just past the end of the instruction, in which case the delta-rip argument is 0. In the other cases, delta-rip is a small non-zero number, and temp-rip + delta-rip is the instruction pointer just past the end of the instruction.

This function returns nil if the length does not exceed 15 bytes. Otherwise, this function returns the offending length (a number above 15), which is useful for error reporting in the model.

Definitions and Theorems

Function: check-instruction-length$inline

(defun check-instruction-length$inline
       (start-rip temp-rip delta-rip)
  (declare (type (signed-byte 48) start-rip)
           (type (signed-byte 48) temp-rip)
           (type (unsigned-byte 3) delta-rip))
  (b* ((start-rip (mbe :logic (ifix start-rip)
                       :exec start-rip))
       (temp-rip (mbe :logic (ifix temp-rip)
                      :exec temp-rip))
       (delta-rip (mbe :logic (nfix delta-rip)
                       :exec delta-rip))
       ((the (signed-byte 49) end-rip)
        (+ (the (signed-byte 48) temp-rip)
           (the (unsigned-byte 3) delta-rip)))
       ((the (signed-byte 50) length)
        (- (the (signed-byte 49) end-rip)
           (the (signed-byte 48) start-rip))))
    (and (> length 15) length)))

Theorem: maybe-natp-of-check-instruction-length

(defthm maybe-natp-of-check-instruction-length
 (b*
  ((badlength?
    (check-instruction-length$inline start-rip temp-rip delta-rip)))
  (acl2::maybe-natp badlength?))
 :rule-classes :rewrite)