• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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
          • Instructions
            • Two-byte-opcodes
            • One-byte-opcodes
              • X86-sal/sar/shl/shr/rcl/rcr/rol/ror
              • X86-add/adc/sub/sbb/or/and/xor/cmp-test-e-i
              • X86-far-jmp-op/en-d
              • X86-add/xadd/adc/sub/sbb/or/and/xor/cmp/test-e-g
              • X86-add/adc/sub/sbb/or/and/xor/cmp-test-rax-i
              • X86-add/adc/sub/sbb/or/and/xor/cmp-g-e
              • X86-push-segment-register
              • X86-pusha
              • X86-shld/shrd
              • X86-mov-op/en-oi
              • X86-inc/dec-4x
                • X86-cmps
                • X86-xchg
                • X86-popa
                • X86-one-byte-jcc
                • X86-movs
                • X86-push-general-register
                • X86-idiv
                • X86-div
                • X86-pop-general-register
                • X86-ret
                • X86-push-i
                • X86-pop-ev
                • X86-imul-op/en-rmi
                • X86-push-ev
                • X86-mul
                • X86-imul-op/en-m
                • X86-stos
                • X86-not/neg-f6-f7
                • X86-call-ff/2-op/en-m
                • X86-iret
                • X86-inc/dec-fe-ff
                • X86-mov-op/en-rm
                • X86-mov-op/en-mr
                • X86-near-jmp-op/en-m
                • X86-mov-op/en-mi
                • X86-loop
                • X86-out
                • X86-call-e8-op/en-m
                • X86-movsxd
                • X86-mov-op/en-fd
                • X86-cmc/clc/stc/cld/std
                • X86-near-jmp-op/en-d
                • X86-mov-op/en-td
                • X86-popf
                • X86-lea
                • X86-jrcxz
                • X86-cbw/cwd/cdqe
                • X86-pushf
                • X86-leave
                • X86-lahf
                • X86-sahf
                • X86-cwd/cdq/cqo
                • X86-rdtsc
                • X86-sti
                • X86-int3
                • X86-hlt
                • X86-cli
              • Fp-opcodes
              • Instruction-semantic-functions
              • X86-illegal-instruction
              • Implemented-opcodes
              • Opcode-maps
              • X86-general-protection
              • X86-device-not-available
              • X86-step-unimplemented
              • Privileged-opcodes
              • Three-byte-opcodes
            • 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
    • One-byte-opcodes

    X86-inc/dec-4x

    Signature
    (x86-inc/dec-4x proc-mode start-rip temp-rip 
                    prefixes rex-byte opcode modr/m sib x86) 
     
      → 
    x86
    Returns
    x86 — Type (x86p x86), given (x86p x86).

    Definitions and Theorems

    Function: x86-inc/dec-4x

    (defun x86-inc/dec-4x
           (proc-mode start-rip temp-rip
                      prefixes rex-byte opcode modr/m sib x86)
     (declare (xargs :stobjs (x86)))
     (declare (type (integer 0 4) proc-mode)
              (type (signed-byte 48) start-rip)
              (type (signed-byte 48) temp-rip)
              (type (unsigned-byte 52) prefixes)
              (type (unsigned-byte 8) rex-byte)
              (type (unsigned-byte 8) opcode)
              (type (unsigned-byte 8) modr/m)
              (type (unsigned-byte 8) sib))
     (declare (ignorable proc-mode start-rip temp-rip
                         prefixes rex-byte opcode modr/m sib))
     (declare (xargs :guard (and (prefixes-p prefixes)
                                 (modr/m-p modr/m)
                                 (sib-p sib)
                                 (rip-guard-okp proc-mode temp-rip))))
     (let ((__function__ 'x86-inc/dec-4x))
      (declare (ignorable __function__))
      (b* ((?ctx 'x86-inc/dec-4x))
       (b*
        (((the (integer 2 4) operand-size)
          (select-operand-size proc-mode
                               nil 0 nil prefixes nil nil nil x86))
         (badlength? (check-instruction-length start-rip temp-rip 0))
         ((when badlength?)
          (!!fault-fresh :gp 0
                         :instruction-length badlength?))
         (reg (the (unsigned-byte 3)
                   (logand 7 opcode)))
         (operand (rgfi-size operand-size reg 0 x86))
         ((the (unsigned-byte 32) input-rflags)
          (rflags x86))
         ((the (unsigned-byte 1) old-cf)
          (rflagsbits->cf input-rflags))
         ((mv result output-rflags undefined-flags)
          (gpr-arith/logic-spec operand-size (if (logbitp 3 opcode) 4 0)
                                operand 1 input-rflags))
         (output-rflags (the (unsigned-byte 32)
                             (!rflagsbits->cf old-cf output-rflags)))
         (x86 (write-user-rflags output-rflags undefined-flags x86))
         (x86 (!rgfi-size operand-size reg result 0 x86))
         (x86 (write-*ip proc-mode temp-rip x86)))
        x86))))

    Theorem: x86p-of-x86-inc/dec-4x

    (defthm x86p-of-x86-inc/dec-4x
     (implies
         (x86p x86)
         (b* ((x86 (x86-inc/dec-4x proc-mode start-rip temp-rip prefixes
                                   rex-byte opcode modr/m sib x86)))
           (x86p x86)))
     :rule-classes :rewrite)