1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
|
; y86-mem-init.lisp Warren A. Hunt, Jr.
(in-package "ACL2")
(include-book "py86")
(local (include-book "centaur/gl/gl" :dir :system))
; Functions to gather items from the registers and memory.
; Functions to initialize the memory.
(defund rmbytes (n addr x86-32)
(declare (xargs :guard (and (natp n)
(n32p addr)
(x86-32p x86-32))))
(if (mbe :logic (zp n) :exec (= n 0))
nil
(cons (list addr (rm08 addr x86-32))
(rmbytes (1- n) (n32+ addr 1) x86-32))))
(defund+x86-32 m86-clear-mem-dword-addr (x86-32 dword-addr)
;; Clear from dword-addr down to memory address zero
(declare (xargs :guard (and (n30p dword-addr)
(x86-32p x86-32))))
(if (mbe :logic (zp dword-addr) :exec (= dword-addr 0))
x86-32
(let ((x86-32 (!memi dword-addr 0 x86-32)))
(m86-clear-mem-dword-addr x86-32 (1- dword-addr)))))
(encapsulate
()
(local
(def-gl-thm ash-addr--2-is-less-with-exploded-n32p
:hyp (and (integerp addr)
(<= 0 addr)
(< addr 4294967296))
:concl (n30p (ash addr -2))
:g-bindings
`((addr (:g-number ,(gl-int 0 1 33))))))
(defund m86-clear-mem (x86-32 addr)
;; Clear from addr down to memory address zero
(declare (xargs :guard (and (n32p addr)
(x86-32p x86-32))))
(b* ((dword-addr (ash addr -2))
;; Clear "most" of the memory.
(x86-32 (m86-clear-mem-dword-addr x86-32 dword-addr))
((if (zp addr)) x86-32)
(x86-32 (wm08 addr 0 x86-32))
(addr (1- addr))
((if (zp addr)) x86-32)
(x86-32 (wm08 addr 0 x86-32))
(addr (1- addr))
((if (zp addr)) x86-32)
(x86-32 (wm08 addr 0 x86-32)))
x86-32)))
(defun m86-regp (updates)
(declare (xargs :guard t))
(if (atom updates)
t
(b* ((update (car updates))
(rest (cdr updates)))
(and (consp update)
(b* ((field (car update))
(value (cdr update)))
(and (keywordp field)
(assoc field *x86-32-reg-numbers*)
(n32p value)
(m86-regp rest)))))))
(defund+x86-32 m86-reg-updates (x86-32 updates)
(declare (xargs :guard (and (m86-regp updates)
(x86-32p x86-32))))
(if (atom updates)
x86-32
(b* ((update (car updates))
(rest (cdr updates))
(field (car update))
(value (cdr update))
(x86-32 (!rgfi (x86-rton field) value x86-32)))
(m86-reg-updates x86-32 rest))))
(defun m86-memp (updates)
(declare (xargs :guard t))
(if (atom updates)
t
(b* ((update (car updates))
(rest (cdr updates)))
(and (consp update)
(b* ((addr (car update))
(value (cdr update)))
(and (n32p addr)
(n08p value)
(m86-memp rest)))))))
(defund+x86-32 m86-mem-updates (x86-32 updates)
(declare (xargs :guard (and (m86-memp updates)
(x86-32p x86-32))))
(if (atom updates)
x86-32
(b* ((update (car updates))
(rest (cdr updates))
(addr (car update))
(value (cdr update))
(x86-32 (wm08 addr value x86-32)))
(m86-mem-updates x86-32 rest))))
(defund m32-get-regs-and-flags (x86-32)
(declare (xargs :guard (x86-32p x86-32)))
(let ((eflags (flg x86-32)))
(list
(list :eip (eip x86-32))
(list :eax (rgfi *mr-eax* x86-32)
:ebx (rgfi *mr-ebx* x86-32)
:ecx (rgfi *mr-ecx* x86-32)
:edx (rgfi *mr-edx* x86-32))
(list :edi (rgfi *mr-edi* x86-32)
:esi (rgfi *mr-esi* x86-32)
:ebp (rgfi *mr-ebp* x86-32)
:esp (rgfi *mr-esp* x86-32))
(list :eflags eflags
:f-zf (y86-zf eflags)
:f-sf (y86-sf eflags)
:f-of (y86-of eflags))
(list :mr-status (ms x86-32)))))
(defund+x86-32 m86-clear-regs (x86-32)
;; Clear all registers
(declare (xargs :guard (x86-32p x86-32)))
(b* ((x86-32 (!rgfi *mr-eax* 0 x86-32))
(x86-32 (!rgfi *mr-ecx* 0 x86-32))
(x86-32 (!rgfi *mr-edx* 0 x86-32))
(x86-32 (!rgfi *mr-ebx* 0 x86-32))
(x86-32 (!rgfi *mr-esi* 0 x86-32))
(x86-32 (!rgfi *mr-edi* 0 x86-32))
(x86-32 (!rgfi *mr-esp* 0 x86-32))
(x86-32 (!rgfi *mr-ebp* 0 x86-32))
(x86-32 (!eip 0 x86-32))
(x86-32 (y86-ALU-results-store-flgs 0 0 0 x86-32)))
x86-32))
(defund+x86-32 init-y86-state (mr-status pc regs flags mem x86-32)
(declare (xargs :guard (and (n32p pc)
(m86-regp regs)
(m86-memp mem)
(alistp flags)
(x86-32p x86-32)))
(ignorable mr-status pc regs flags mem))
(let* ((x86-32 (m86-mem-updates x86-32 mem))
(x86-32 (m86-reg-updates x86-32 regs))
(x86-32 (!eip pc x86-32))
(x86-32 (!ms mr-status x86-32))
(zf (n01 (nfix (cdr (assoc :zf flags)))))
(sf (n01 (nfix (cdr (assoc :sf flags)))))
(of (n01 (nfix (cdr (assoc :of flags)))))
(x86-32 (y86-ALU-results-store-flgs zf sf of x86-32))
)
x86-32))
|
