• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • 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
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
        • Virtualization-for-validation
          • Virtualization-for-validation-debugging
          • Virtualization-for-validation-limitations
          • Dump-virtualizable-state
          • Write-virtualizable-mem
          • Validate-insts
          • Run-until-rip-or-n
          • Validate-inst
          • Write-val1
          • Write-bytes
        • Dynamic-instrumentation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Virtualization-for-validation

Run-until-rip-or-n

Execute the model until we reach the given rip address or have executed n instructions.

Signature

(run-until-rip-or-n rip n x86) → (mv * x86)

Definitions and Theorems

Function: run-until-rip-or-n

(defun run-until-rip-or-n (rip n x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'run-until-rip-or-n))
    (declare (ignorable __function__))
    (if (or (= n 0)
            (ms x86)
            (fault x86)
            (equal (rip x86) (i64 rip)))
        (mv (equal (rip x86) (i64 rip)) x86)
      (b* ((x86 (x86-fetch-decode-execute x86)))
        (run-until-rip-or-n rip (1- n) x86)))))