• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Booting-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • To-do
      • Proof-utilities
        • System-level-marking-view-proof-utilities
        • Non-marking-view-proof-utilities
        • App-view-proof-utilities
        • Subset-p
        • Disjoint-p
        • Pos
        • Member-p
        • No-duplicates-p
        • Common-system-level-utils
        • Debugging-code-proofs
        • General-memory-utils
          • Separate
          • Disjoint-p$
        • X86-row-wow-thms
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• General-memory-utils

Separate

Signature

(separate r-w-x-1 n-1 addr-1 r-w-x-2 n-2 addr-2) → *

Arguments

n-1 — Guard (posp n-1).

addr-1 — Guard (integerp addr-1).

n-2 — Guard (posp n-2).

addr-2 — Guard (integerp addr-2).

Definitions and Theorems

Function: separate

(defun separate (r-w-x-1 n-1 addr-1 r-w-x-2 n-2 addr-2)
  (declare (type (member :r :w :x) r-w-x-1)
           (type (member :r :w :x) r-w-x-2))
  (declare (xargs :guard (and (posp n-1)
                              (integerp addr-1)
                              (posp n-2)
                              (integerp addr-2))))
  (declare (xargs :non-executable t))
  (prog2$ (acl2::throw-nonexec-error
               'separate
               (list r-w-x-1 n-1 addr-1 r-w-x-2 n-2 addr-2))
          (let ((__function__ 'separate))
            (declare (ignorable __function__))
            (or (<= (+ n-2 addr-2) addr-1)
                (<= (+ n-1 addr-1) addr-2)))))

Theorem: separate-is-commutative

(defthm separate-is-commutative
  (implies (separate r-w-x-1 n-1 a-1 r-w-x-2 n-2 a-2)
           (separate r-w-x-2 n-2 a-2 r-w-x-1 n-1 a-1)))

Function: separate-free-var-candidates

(defun separate-free-var-candidates (calls)
  (if (endp calls)
      nil
    (cons (list (cons 'n-1 (nth 2 (car calls)))
                (cons 'a-1 (nth 3 (car calls)))
                (cons 'n-2 (nth 5 (car calls)))
                (cons 'a-2 (nth 6 (car calls))))
          (separate-free-var-candidates (cdr calls)))))

Function: separate-bindings

(defun separate-bindings (name r-w-x-1 r-w-x-2 mfc state)
  (declare (xargs :stobjs (state))
           (ignorable name state))
  (b*
   ((calls (acl2::find-matches-list
                (cons 'separate
                      (cons r-w-x-1
                            (cons 'a
                                  (cons 'b (cons r-w-x-2 '(c d))))))
                (mfc-clause mfc)
                nil))
    ((when (not calls)) nil))
   (separate-free-var-candidates calls)))

Theorem: separate-smaller-regions

(defthm separate-smaller-regions
  (implies
       (and (bind-free (separate-bindings 'separate-smaller-regions
                                          r-w-x-1 r-w-x-2 mfc state)
                       (n-1 a-1 n-2 a-2))
            (<= a-2 a-2-bigger)
            (<= (+ n-2-smaller a-2-bigger)
                (+ n-2 a-2))
            (<= a-1 a-1-bigger)
            (<= (+ n-1-smaller a-1-bigger)
                (+ n-1 a-1))
            (separate r-w-x-1 n-1 a-1 r-w-x-2 n-2 a-2))
       (separate r-w-x-1 n-1-smaller a-1-bigger
                 r-w-x-2 n-2-smaller a-2-bigger))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: separate-contiguous-regions

(defthm separate-contiguous-regions
  (and (separate r-w-x-1 i (+ (- i) x)
                 r-w-x-2 j x)
       (implies (<= j i)
                (separate r-w-x-1 i x r-w-x-2 j (+ (- i) x)))
       (separate r-w-x-1 i x r-w-x-2 j (+ i x))
       (implies (or (<= (+ j k2) k1) (<= (+ i k1) k2))
                (separate r-w-x-1 i (+ k1 x)
                          r-w-x-2 j (+ k2 x)))))