• 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
            • 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-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
  • Instruction-semantic-functions

Gpr-arith/logic-spec

Semantics of general-purpose arithmetic and logical instructions

These instructions are:

  • ADD
  • ADC
  • SUB
  • SBB
  • CMP
  • OR
  • AND
  • XOR
  • TEST
  • XADD

Macro: gpr-arith/logic-spec

(defmacro gpr-arith/logic-spec
          (operand-size operation dst src input-rflags)
 (cons
  'case
  (cons
   operand-size
   (cons
    (cons
      '1
      (cons (cons 'gpr-arith/logic-spec-1
                  (cons operation
                        (cons dst
                              (cons src (cons input-rflags 'nil)))))
            'nil))
    (cons
     (cons
      '2
      (cons (cons 'gpr-arith/logic-spec-2
                  (cons operation
                        (cons dst
                              (cons src (cons input-rflags 'nil)))))
            'nil))
     (cons
      (cons
       '4
       (cons
            (cons 'gpr-arith/logic-spec-4
                  (cons operation
                        (cons dst
                              (cons src (cons input-rflags 'nil)))))
            'nil))
      (cons
       (cons
        'otherwise
        (cons
            (cons 'gpr-arith/logic-spec-8
                  (cons operation
                        (cons dst
                              (cons src (cons input-rflags 'nil)))))
            'nil))
       'nil)))))))

Subtopics

Gpr-arith/logic-spec-8
Gpr-arith/logic-spec-4
Gpr-arith/logic-spec-2
Gpr-arith/logic-spec-1