|
|
|---|
|
|
|
|---|
Function:
(defun gen-read-function-fn (size signed? check-alignment?-var mem-ptr?-var) (declare (xargs :guard (and (natp size) (booleanp signed?) (booleanp check-alignment?-var) (booleanp mem-ptr?-var)))) (let ((__function__ 'gen-read-function)) (declare (ignorable __function__)) (b* ((size-str (symbol-name (if (< size 10) (acl2::packn (list 0 size)) (acl2::packn (list size))))) (fn (str::cat (if signed? "RIME" "RME") size-str)) (fn-name (intern$ fn "X86ISA")) (fn-call (cons fn-name (cons 'proc-mode (cons 'eff-addr (cons 'seg-reg (cons 'r-x (append (and check-alignment?-var '(check-alignment?)) (cons 'x86 (and mem-ptr?-var '(:mem-ptr? mem-ptr?)))))))))) (lin-mem-fn (str::cat (if signed? "RIML" "RML") size-str)) (lin-mem-fn-name (intern$ lin-mem-fn "X86ISA")) (short-doc-string (str::cat "Read " (if signed? "a signed " "an unsigned ") (str::nat-to-dec-string size) "-bit value from memory via an effective address.")) (long-doc-string (str::cat "<p>The effective address @('eff-addr') is translated to a canonical linear address using @(see ea-to-la). If this translation is successful and no other errors (like alignment errors) occur, then @(see " lin-mem-fn ") is called.</p> <p>Prior to the effective address translation, we check whether read access is allowed. The only case in which it is not allowed is when a read access is attempted on an execute-only code segment, in 32-bit mode. In 64-bit mode, the R bit of the code segment descriptor is ignored (see Atmel manual, Dec'17, Volume 2, Section 4.8.1).</p>"))) (cons 'define (cons fn-name (cons (cons '(proc-mode :type (integer 0 4)) (cons '(eff-addr :type (signed-byte 64)) (cons '(seg-reg :type (integer 0 5)) (cons '(r-x :type (member :r :x)) (append (and check-alignment?-var '((check-alignment? booleanp))) (cons 'x86 (and mem-ptr?-var '(&key ((mem-ptr? booleanp) 'nil))))))))) (cons ':inline (cons 't (cons ':no-function (cons 't (cons ':returns (cons (cons 'mv (cons 'flg (cons (cons 'value (cons (cons (if signed? 'signed-byte-p 'unsigned-byte-p) (cons size '(value))) '(:hyp (x86p x86)))) '((x86-new x86p :hyp (x86p x86)))))) (cons ':parents (cons '(top-level-memory) (cons ':short (cons short-doc-string (cons ':long (cons long-doc-string (cons (cons 'b* (cons (cons '((when (and (/= proc-mode 0) (= seg-reg 1) (eq r-x :r) (b* ((attr (loghead 16 (seg-hidden-attri seg-reg x86))) (r (code-segment-descriptor-attributesbits->r attr))) (= r 0)))) (mv (list :execute-only-code-segment eff-addr) 0 x86)) (cons (cons '(mv flg lin-addr) (cons (cons 'ea-to-la (cons 'proc-mode (cons 'eff-addr (cons 'seg-reg (cons (/ size 8) '(x86)))))) 'nil)) (cons '((when flg) (mv flg 0 x86)) (and check-alignment?-var (cons (cons (cons 'unless (cons (cons 'or (cons '(not check-alignment?) (cons (cons 'address-aligned-p (cons 'lin-addr (cons (/ size 8) (cons (if mem-ptr?-var 'mem-ptr? 'nil) 'nil)))) 'nil))) 'nil)) '((mv (list :unaligned-linear-address lin-addr) 0 x86))) 'nil))))) (cons (cons lin-mem-fn-name '(lin-addr r-x x86)) 'nil))) (cons '/// (cons (cons (if signed? 'defthm-signed-byte-p 'defthm-unsigned-byte-p) (cons (mk-name (if signed? "I" "N") size-str "P-OF-MV-NTH-1-" fn) (cons ':hyp (cons 't (cons ':bound (cons size (cons ':concl (cons (cons 'mv-nth (cons '1 (cons fn-call 'nil))) '(:gen-linear t :gen-type t))))))))) (cons (cons 'defrule (cons (mk-name fn "-VALUE-WHEN-ERROR") (cons (cons 'implies (cons (cons 'mv-nth (cons '0 (cons fn-call 'nil))) (cons (cons 'equal (cons (cons 'mv-nth (cons '1 (cons fn-call 'nil))) '(0))) 'nil))) (cons ':enable (cons (and signed? (cons lin-mem-fn-name 'nil)) 'nil))))) (cons (cons 'defrule (cons (mk-name fn "-DOES-NOT-AFFECT-STATE-IN-APP-VIEW") (cons (cons 'implies (cons '(app-view x86) (cons (cons 'equal (cons (cons 'mv-nth (cons '2 (cons fn-call 'nil))) '(x86))) 'nil))) (cons ':enable (cons (and signed? (cons lin-mem-fn-name 'nil)) 'nil))))) (cons (cons 'defrule (cons (mk-name "XR-" fn "-STATE-APP-VIEW") (cons (cons 'implies (cons '(app-view x86) (cons (cons 'equal (cons (cons 'xr (cons 'fld (cons 'index (cons (cons 'mv-nth (cons '2 (cons fn-call 'nil))) 'nil)))) '((xr fld index x86)))) 'nil))) (cons ':enable (cons (and signed? (cons lin-mem-fn-name 'nil)) 'nil))))) (cons (cons 'defrule (cons (mk-name "XR-" fn "-STATE-SYS-VIEW") (cons (cons 'implies (cons (cons 'and (cons '(not (app-view x86)) (cons '(not (equal fld :mem)) (cons '(not (equal fld :fault)) (cons '(not (equal fld :tlb)) (if (< size 10) nil '((member-equal fld *x86-field-names-as-keywords*)))))))) (cons (cons 'equal (cons (cons 'xr (cons 'fld (cons 'index (cons (cons 'mv-nth (cons '2 (cons fn-call 'nil))) 'nil)))) '((xr fld index x86)))) 'nil))) (cons ':enable (cons (and signed? (cons lin-mem-fn-name 'nil)) (if (< size 10) nil '(:disable (rb unsigned-byte-p signed-byte-p member-equal)))))))) (cons (cons 'defrule (cons (mk-name fn "-XW-APP-VIEW") (cons (cons 'implies (cons '(and (app-view x86) (not (equal fld :mem)) (not (equal fld :app-view)) (not (equal fld :seg-hidden-base)) (not (equal fld :seg-hidden-limit)) (not (equal fld :seg-hidden-attr)) (not (equal fld :seg-visible)) (not (equal fld :msr))) (cons (cons 'and (cons (cons 'equal (cons (cons 'mv-nth (cons '0 (cons (search-and-replace-once 'x86 '(xw fld index value x86) fn-call) 'nil))) (cons (cons 'mv-nth (cons '0 (cons fn-call 'nil))) 'nil))) (cons (cons 'equal (cons (cons 'mv-nth (cons '1 (cons (search-and-replace-once 'x86 '(xw fld index value x86) fn-call) 'nil))) (cons (cons 'mv-nth (cons '1 (cons fn-call 'nil))) 'nil))) 'nil))) 'nil))) (cons ':enable (cons (and signed? (cons lin-mem-fn-name 'nil)) '(:disable (rb))))))) (cons (cons 'defrule (cons (mk-name fn "-XW-SYS-VIEW") (cons (cons 'implies (cons (cons 'and (cons '(not (app-view x86)) (cons '(not (equal fld :fault)) (cons '(not (equal fld :seg-visible)) (cons '(not (equal fld :seg-hidden-base)) (cons '(not (equal fld :seg-hidden-limit)) (cons '(not (equal fld :seg-hidden-attr)) (cons '(not (equal fld :mem)) (cons '(not (equal fld :ctr)) (cons '(not (equal fld :msr)) (cons '(not (equal fld :rflags)) (cons '(not (equal fld :app-view)) (cons '(not (equal fld :tlb)) (cons '(not (equal fld :marking-view)) (cons '(not (equal fld :implicit-supervisor-access)) (if (< size 10) nil '((member-equal fld *x86-field-names-as-keywords*)))))))))))))))))) (cons (cons 'and (cons (cons 'equal (cons (cons 'mv-nth (cons '0 (cons (search-and-replace-once 'x86 '(xw fld index value x86) fn-call) 'nil))) (cons (cons 'mv-nth (cons '0 (cons fn-call 'nil))) 'nil))) (cons (cons 'equal (cons (cons 'mv-nth (cons '1 (cons (search-and-replace-once 'x86 '(xw fld index value x86) fn-call) 'nil))) (cons (cons 'mv-nth (cons '1 (cons fn-call 'nil))) 'nil))) (cons (cons 'equal (cons (cons 'mv-nth (cons '2 (cons (search-and-replace-once 'x86 '(xw fld index value x86) fn-call) 'nil))) (cons (cons 'xw (cons 'fld (cons 'index (cons 'value (cons (cons 'mv-nth (cons '2 (cons fn-call 'nil))) 'nil))))) 'nil))) 'nil)))) 'nil))) (cons ':enable (cons (and signed? (cons lin-mem-fn-name 'nil)) (if (< size 10) nil '(:disable (rb unsigned-byte-p signed-byte-p member-equal)))))))) (cons (cons 'defrule (cons (mk-name fn "-XW-SYS-VIEW-RFLAGS-NOT-AC") (cons (cons 'implies (cons '(and (not (app-view x86)) (equal (rflagsbits->ac value) (rflagsbits->ac (rflags x86)))) (cons (cons 'and (cons (cons 'equal (cons (cons 'mv-nth (cons '0 (cons (search-and-replace-once 'x86 '(xw :rflags nil value x86) fn-call) 'nil))) (cons (cons 'mv-nth (cons '0 (cons fn-call 'nil))) 'nil))) (cons (cons 'equal (cons (cons 'mv-nth (cons '1 (cons (search-and-replace-once 'x86 '(xw :rflags nil value x86) fn-call) 'nil))) (cons (cons 'mv-nth (cons '1 (cons fn-call 'nil))) 'nil))) (cons (cons 'equal (cons (cons 'mv-nth (cons '2 (cons (search-and-replace-once 'x86 '(xw :rflags nil value x86) fn-call) 'nil))) (cons (cons 'xw (cons ':rflags (cons 'nil (cons 'value (cons (cons 'mv-nth (cons '2 (cons fn-call 'nil))) 'nil))))) 'nil))) 'nil)))) 'nil))) (cons ':enable (cons (and signed? (cons lin-mem-fn-name 'nil)) '(:disable (rb unsigned-byte-p signed-byte-p))))))) (cons (cons 'defrule (cons (mk-name fn "-WHEN-64-BIT-MODEP-AND-NOT-FS/GS") (cons (cons 'implies (cons (cons 'and (cons '(not (equal seg-reg 4)) (cons '(not (equal seg-reg 5)) (cons '(canonical-address-p eff-addr) (and check-alignment?-var (cons (cons 'or (cons '(not check-alignment?) (cons (cons 'address-aligned-p (cons 'eff-addr (cons (/ size 8) (cons (if mem-ptr?-var 'mem-ptr? 'nil) 'nil)))) 'nil))) 'nil)))))) (cons (cons 'equal (cons (search-and-replace-once 'proc-mode '0 fn-call) (cons (cons lin-mem-fn-name '(eff-addr r-x x86)) 'nil))) 'nil))) 'nil))) (append (and check-alignment?-var (cons (cons 'defrule (cons (mk-name fn "-UNALIGNED-WHEN-64-BIT-MODEP-AND-NOT-FS/GS") (cons (cons 'implies (cons (cons 'and (cons '(not (equal seg-reg 4)) (cons '(not (equal seg-reg 5)) (cons (cons 'not (cons (cons 'or (cons '(not check-alignment?) (cons (cons 'address-aligned-p (cons 'eff-addr (cons (/ size 8) (cons (if mem-ptr?-var 'mem-ptr? 'nil) 'nil)))) 'nil))) 'nil)) '((canonical-address-p eff-addr)))))) (cons (cons 'equal (cons (search-and-replace-once 'proc-mode '0 fn-call) '((list (list :unaligned-linear-address eff-addr) 0 x86)))) 'nil))) 'nil))) 'nil)) (cons (cons 'defrule (cons (mk-name fn "-WHEN-64-BIT-MODEP-AND-FS/GS") (cons (cons 'implies (cons '(or (equal seg-reg 4) (equal seg-reg 5)) (cons (cons 'equal (cons (search-and-replace-once 'proc-mode '0 fn-call) (cons (cons 'b* (cons (cons '((mv flg lin-addr) (b* (((mv base & &) (segment-base-and-bounds 0 seg-reg x86)) (lin-addr (i64 (+ base (n64 eff-addr))))) (if (canonical-address-p lin-addr) (mv nil lin-addr) (mv (list :non-canonical-address lin-addr) 0)))) (cons '((when flg) (mv flg 0 x86)) (and check-alignment?-var (cons (cons (cons 'unless (cons (cons 'or (cons '(not check-alignment?) (cons (cons 'address-aligned-p (cons 'lin-addr (cons (/ size 8) (cons (if mem-ptr?-var 'mem-ptr? 'nil) 'nil)))) 'nil))) 'nil)) '((mv (list :unaligned-linear-address lin-addr) 0 x86))) 'nil)))) (cons (cons lin-mem-fn-name '(lin-addr r-x x86)) 'nil))) 'nil))) 'nil))) '(:hints (("Goal" :in-theory (e/d (ea-to-la) nil))))))) 'nil)))))))))))))))))))))))))))))))