• 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
          • X86isa-state
          • Syscalls
          • Cpuid
          • Linear-memory
          • Rflag-specifications
          • Characterizing-undefined-behavior
          • App-view
          • Top-level-memory
          • X86-decoder
          • Physical-memory
          • Decoding-and-spec-utils
          • Instructions
            • Two-byte-opcodes
            • One-byte-opcodes
            • Fp-opcodes
            • Instruction-semantic-functions
              • Sar-spec
              • Shr-spec
              • Sal/shl-spec
              • Rol-spec
              • Ror-spec
              • Rcl-spec
              • Rcr-spec
              • Simd-sub-spec
              • Simd-add-spec
              • Imul-spec
              • Mul-spec
              • Idiv-spec
              • Div-spec
              • Shrd-spec
              • Shld-spec
              • Gpr-arith/logic-spec
                • Gpr-arith/logic-spec-8
                • Gpr-arith/logic-spec-4
                • Gpr-arith/logic-spec-2
                  • Gpr-xadd-spec-2
                  • Gpr-adc-spec-2
                  • Gpr-sbb-spec-2
                  • Gpr-add-spec-2
                  • Gpr-sub-spec-2
                  • Gpr-xor-spec-2
                  • Gpr-and-spec-2
                  • Gpr-or-spec-2
                • Gpr-arith/logic-spec-1
              • Shrx-spec
              • Shlx-spec
              • Sarx-spec
              • Floating-point-specifications
            • 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
  • Gpr-arith/logic-spec

Gpr-arith/logic-spec-2

Signature
(gpr-arith/logic-spec-2 operation dst src input-rflags) 
  → 
(mv * * *)

Definitions and Theorems

Function: gpr-arith/logic-spec-2

(defun gpr-arith/logic-spec-2 (operation dst src input-rflags)
  (declare (type (member 0 38 2 4 6 8 1 3 5 7)
                 operation)
           (type (unsigned-byte 16) dst)
           (type (unsigned-byte 16) src)
           (type (unsigned-byte 32) input-rflags))
  (let ((__function__ 'gpr-arith/logic-spec-2))
    (declare (ignorable __function__))
    (case operation
      (0 (gpr-add-spec-2 dst src input-rflags))
      (1 (gpr-or-spec-2 dst src input-rflags))
      (2 (gpr-adc-spec-2 dst src input-rflags))
      (3 (gpr-and-spec-2 dst src input-rflags))
      (4 (gpr-sub-spec-2 dst src input-rflags))
      (5 (gpr-xor-spec-2 dst src input-rflags))
      (6 (gpr-sbb-spec-2 dst src input-rflags))
      (7 (gpr-and-spec-2 dst src input-rflags))
      (8 (gpr-sub-spec-2 dst src input-rflags))
      (38 (gpr-xadd-spec-2 dst src input-rflags))
      (otherwise (mv 0 0 0)))))

Subtopics

Gpr-xadd-spec-2
Gpr-adc-spec-2
Gpr-sbb-spec-2
Gpr-add-spec-2
Gpr-sub-spec-2
Gpr-xor-spec-2
Gpr-and-spec-2
Gpr-or-spec-2