• 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
            • Rflags-reads-and-writes
              • Write-user-rflags
                • Undef-flg-logic
                • Undef-flg
              • General-sf-spec-fn
              • General-cf-spec-fn
              • General-pf-spec-fn
              • General-of-spec-fn
              • Zf-spec
              • Sbb-af-spec8
              • Sbb-af-spec64
              • Sbb-af-spec32
              • Sbb-af-spec16
              • Adc-af-spec8
              • Adc-af-spec64
              • Adc-af-spec32
              • Adc-af-spec16
              • Sub-af-spec8
              • Sub-af-spec64
              • Sub-af-spec32
              • Sub-af-spec16
              • Add-af-spec8
              • Add-af-spec64
              • Add-af-spec32
              • Add-af-spec16
              • Pf-spec64
              • Pf-spec32
              • Pf-spec16
              • Of-spec64
              • Sf-spec64
              • Sf-spec32
              • Sf-spec16
              • Pf-spec8
              • Of-spec8
              • Of-spec32
              • Of-spec16
              • Cf-spec8
              • Cf-spec64
              • Cf-spec32
              • Cf-spec16
              • Sf-spec8
            • Characterizing-undefined-behavior
            • Top-level-memory
            • App-view
            • X86-decoder
            • Physical-memory
            • Decoding-and-spec-utils
            • 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
    • Rflags-reads-and-writes

    Write-user-rflags

    Writing user rflags (CF, PF, AF, ZF, SF, and OF), including undefined ones, to the x86 state

    Signature
    (write-user-rflags user-flags-vector undefined-mask x86) → x86
    Returns
    x86 — Type (x86p x86), given (x86p x86).

    We set the undefined flags, which are indicated by mask, to the value returned by undef-read.

    Definitions and Theorems

    Function: write-user-rflags$inline

    (defun write-user-rflags$inline
           (user-flags-vector undefined-mask x86)
      (declare (xargs :stobjs (x86)))
      (declare (type (unsigned-byte 32)
                     user-flags-vector)
               (type (unsigned-byte 32)
                     undefined-mask))
      (b* ((user-flags-vector (mbe :logic (n32 user-flags-vector)
                                   :exec user-flags-vector))
           (undefined-mask (mbe :logic (n32 undefined-mask)
                                :exec undefined-mask))
           ((the (unsigned-byte 32) input-rflags)
            (mbe :logic (n32 (rflags x86))
                 :exec (rflags x86))))
        (mbe :logic
             (b* ((x86 (if (equal (rflagsbits->cf undefined-mask)
                                  1)
                           (!flgi-undefined :cf x86)
                         (!flgi :cf (rflagsbits->cf user-flags-vector)
                                x86)))
                  (x86 (if (equal (rflagsbits->pf undefined-mask)
                                  1)
                           (!flgi-undefined :pf x86)
                         (!flgi :pf (rflagsbits->pf user-flags-vector)
                                x86)))
                  (x86 (if (equal (rflagsbits->af undefined-mask)
                                  1)
                           (!flgi-undefined :af x86)
                         (!flgi :af (rflagsbits->af user-flags-vector)
                                x86)))
                  (x86 (if (equal (rflagsbits->zf undefined-mask)
                                  1)
                           (!flgi-undefined :zf x86)
                         (!flgi :zf (rflagsbits->zf user-flags-vector)
                                x86)))
                  (x86 (if (equal (rflagsbits->sf undefined-mask)
                                  1)
                           (!flgi-undefined :sf x86)
                         (!flgi :sf (rflagsbits->sf user-flags-vector)
                                x86)))
                  (x86 (if (equal (rflagsbits->of undefined-mask)
                                  1)
                           (!flgi-undefined :of x86)
                         (!flgi :of (rflagsbits->of user-flags-vector)
                                x86))))
               x86)
             :exec
             (if (eql undefined-mask 0)
                 (b* ((x86 (!flgi :cf (rflagsbits->cf user-flags-vector)
                                  x86))
                      (x86 (!flgi :pf (rflagsbits->pf user-flags-vector)
                                  x86))
                      (x86 (!flgi :af (rflagsbits->af user-flags-vector)
                                  x86))
                      (x86 (!flgi :zf (rflagsbits->zf user-flags-vector)
                                  x86))
                      (x86 (!flgi :sf (rflagsbits->sf user-flags-vector)
                                  x86))
                      (x86 (!flgi :of (rflagsbits->of user-flags-vector)
                                  x86)))
                   x86)
               (b* ((x86 (if (equal (rflagsbits->cf undefined-mask)
                                    1)
                             (!flgi-undefined :cf x86)
                           (!flgi :cf (rflagsbits->cf user-flags-vector)
                                  x86)))
                    (x86 (if (equal (rflagsbits->pf undefined-mask)
                                    1)
                             (!flgi-undefined :pf x86)
                           (!flgi :pf (rflagsbits->pf user-flags-vector)
                                  x86)))
                    (x86 (if (equal (rflagsbits->af undefined-mask)
                                    1)
                             (!flgi-undefined :af x86)
                           (!flgi :af (rflagsbits->af user-flags-vector)
                                  x86)))
                    (x86 (if (equal (rflagsbits->zf undefined-mask)
                                    1)
                             (!flgi-undefined :zf x86)
                           (!flgi :zf (rflagsbits->zf user-flags-vector)
                                  x86)))
                    (x86 (if (equal (rflagsbits->sf undefined-mask)
                                    1)
                             (!flgi-undefined :sf x86)
                           (!flgi :sf (rflagsbits->sf user-flags-vector)
                                  x86)))
                    (x86 (if (equal (rflagsbits->of undefined-mask)
                                    1)
                             (!flgi-undefined :of x86)
                           (!flgi :of (rflagsbits->of user-flags-vector)
                                  x86))))
                 x86)))))

    Theorem: x86p-of-write-user-rflags

    (defthm x86p-of-write-user-rflags
      (implies (x86p x86)
               (b* ((x86 (write-user-rflags$inline
                              user-flags-vector undefined-mask x86)))
                 (x86p x86)))
      :rule-classes :rewrite)

    Theorem: xr-write-user-rflags

    (defthm xr-write-user-rflags
      (implies (and (not (equal fld :rflags))
                    (not (equal fld :undef)))
               (equal (xr fld index
                          (write-user-rflags flags mask x86))
                      (xr fld index x86))))

    Theorem: xr-write-user-rflags-no-mask

    (defthm xr-write-user-rflags-no-mask
      (implies (not (equal fld :rflags))
               (equal (xr fld
                          index (write-user-rflags flags 0 x86))
                      (xr fld index x86))))

    Theorem: rflags-and-write-user-rflags-no-mask

    (defthm rflags-and-write-user-rflags-no-mask
      (equal (write-user-rflags user-flags-vector 0 x86)
             (b* ((x86 (!flgi :cf (rflagsbits->cf user-flags-vector)
                              x86))
                  (x86 (!flgi :pf (rflagsbits->pf user-flags-vector)
                              x86))
                  (x86 (!flgi :af (rflagsbits->af user-flags-vector)
                              x86))
                  (x86 (!flgi :zf (rflagsbits->zf user-flags-vector)
                              x86))
                  (x86 (!flgi :sf (rflagsbits->sf user-flags-vector)
                              x86))
                  (x86 (!flgi :of (rflagsbits->of user-flags-vector)
                              x86)))
               x86)))