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
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
|
(in-package "DJVM")
(include-book "../M6-DJVM-shared/jvm-frame-manipulation-primitives")
(acl2::set-verify-guards-eagerness 2)
;;; Define stronger guard for pushStack, popStack that are used in defining
;;; bytecode semantics.
(include-book "../DJVM/consistent-state")
;; DJVM specific. In fact is about the same as current-thread
(defthm wff-call-frame-implies-wff-method-ptr-method-ptr
(implies (wff-call-frame frame)
(wff-method-ptr (method-ptr frame)))
:hints (("Goal" :in-theory (enable method-ptr wff-call-frame))))
(local (in-theory (disable wff-method-ptr method-ptr)))
(defun op-stack-primitive-shared-guard (s)
(mylet* ((cid (current-thread s))
(tt (thread-table s))
(thread (thread-by-id cid tt))
(callstack (thread-call-stack thread))
(topframe (top callstack))
(method-ptr (method-ptr (current-frame s)))
(cl (instance-class-table s))
(method (deref-method method-ptr cl)))
(and (wff-state s)
(wff-thread-table tt)
(thread-exists? cid tt)
(wff-thread thread)
;;
;; we don't need wff-call-stack we do need a wff-top-frame, we don't
;; care whether return pc are right or not. Just the syntax is right
;; to allow us to access certain fields and assert properties on certain
;; pieces that are concerned with validity of the operation.
;;
(wff-call-stack callstack)
(wff-call-frame topframe)
(wff-class-table (class-table s))
(wff-instance-class-table (instance-class-table s))
(wff-method-decl method)
(not (mem '*native*
(method-accessflags method))))))
;; Lets consider jvm-frame-manipulation-primitives.lisp's topStack being
;; INTERNAL operations of JVM, which does not check whether topStack is called
;; on a category1 top.
(defun topStack-guard-strong (s)
(mylet*
((opstack
(operand-stack
(top (thread-call-stack (thread-by-id (current-thread s)
(thread-table s)))))))
(and (op-stack-primitive-shared-guard s)
(canPopCategory1 opstack))))
;;; This is a different popStack. We want stronger check!!
;;;
;;; Previously we use internal popStack
;;;;
;;;; Defensive machine could check stronger guard than non defensive machine
;;;; could!!
;;;;
;;; should I change the definition. some proof might fail. but they should be
;;; easy to fix.
;;; let keep the current definition...
;;;
;;; safe-popStack is used in defining djvm bytecode semantics.
;;;
;;; We have the folllowing property, if consistent-state, if guard does not
;;; fail, executing instruction perserves the consistent-state.
;;;
(defthm wff-thread-table-thread-by-id-thread-id
(implies (and (wff-thread-table ths)
(thread-by-id x ths))
(equal (thread-id (thread-by-id x ths))
x)))
(defthm wff-thread-table-thread-by-id-thread-id-2
(implies (and (wff-thread-table ths)
(thread-by-id x ths))
(equal (nth 1 (thread-by-id x ths))
x))
:hints (("Goal" :in-theory (enable wff-thread thread-id wff-thread-table))))
(in-theory (enable wff-thread thread-id))
(defun safe-popStack (s)
(declare (xargs :guard (topStack-guard-strong s)))
(mylet* ((curthread-id (current-thread s))
(old-thread-table (thread-table s))
(old-thread (thread-by-id curthread-id old-thread-table))
(old-call-stack (thread-call-stack old-thread))
(old-frame (top old-call-stack))
(old-op-stack (operand-stack old-frame))
(new-op-stack (pop old-op-stack))
(new-frame (frame-set-operand-stack new-op-stack old-frame))
(new-call-stack (push new-frame (pop old-call-stack)))
(new-thread (thread-set-call-stack new-call-stack old-thread))
(new-thread-table (replace-thread-table-entry old-thread
new-thread
old-thread-table)))
(state-set-thread-table new-thread-table s)))
;;; enable many things. guard verification should be easy.
;; Fri Jan 16 00:16:44 2004
(defun secondStack-guard-strong (s)
(and (topStack-guard-strong s)
(topStack-guard-strong (safe-popStack s))))
(defun thirdStack-guard-strong (s)
(and (secondStack-guard-strong s)
(topStack-guard-strong (safe-popStack (safe-popStack s)))))
;;
;; could disable more functions and prove more accessors
;;
(defun safe-topStack (s)
(declare (xargs :guard (topStack-guard-strong s)))
;; we could not be able to guard verify that topStack's guard can be verified
;; unless we have a extensive ... check-inst
(top (operand-stack
(top (thread-call-stack (thread-by-id (current-thread s)
(thread-table s)))))))
(defun safe-secondStack (s)
(declare (xargs :guard (secondStack-guard-strong s)
:guard-hints (("Goal" :in-theory (disable topStack-guard)))))
(safe-topStack (safe-popStack s)))
(defun safe-thirdStack (s)
(declare (xargs :guard (thirdStack-guard-strong s)
:guard-hints (("Goal" :in-theory (disable topStack-guard)))))
(safe-topStack (safe-popStack (safe-popStack s))))
;----------------------------------------------------------------------
;; push is always allowed.
;; pushStack now has a stronger guard!!
;; Maybe we do not need that.
;; Any operations now needs such a stronge guard.
;;
;; have to think again about whether we need to just use pushStack as ...
;;
;; notice this is a very strong guard, if a state is not consistent,
;; safe-pushStack will signal a guard violation.
(defthm consistent-state-implies-wff-thread-table
(implies (consistent-state s)
(wff-thread-table (thread-table s)))
:rule-classes :forward-chaining)
;; do I want to disable consistent-state
(defthm consistent-state-implies-wff-thread-table-b
(implies (consistent-state s)
(wff-thread-table (thread-table s))))
;; do I want to disable thread-table, here?
(defthm consistent-state-implies-wff-thread-exists
(implies (consistent-state s)
(thread-exists? (current-thread s)
(thread-table s)))
:rule-classes :forward-chaining)
(defthm consistent-state-implies-wff-thread-exists-b
(implies (consistent-state s)
(thread-exists? (current-thread s)
(thread-table s))))
(defthm thread-exists-wff-thread-table-wff-thread
(implies (and (thread-exists? id ths)
(wff-thread-table ths))
(wff-thread (thread-by-id id ths)))
:rule-classes :forward-chaining)
(defthm thread-exists-wff-thread-table-wff-thread-b
(implies (and (thread-exists? id ths)
(wff-thread-table ths))
(wff-thread (thread-by-id id ths))))
(defthm thread-exists-consistent-thread-table-consistent-thread
(implies (and (thread-exists? id ths)
(consistent-thread-entries ths cl hp))
(consistent-thread-entry (thread-by-id id ths) cl hp))
:rule-classes :forward-chaining)
(defthm thread-exists-consistent-thread-table-consistent-thread-b
(implies (and (thread-exists? id ths)
(consistent-thread-entries ths cl hp))
(consistent-thread-entry (thread-by-id id ths) cl hp)))
(defthm consistent-thread-entry-implies-consistent-call-stack
(implies (consistent-thread-entry th cl hp)
(consistent-call-stack (thread-call-stack th) cl hp))
:rule-classes :forward-chaining)
(defthm consistent-thread-entry-implies-consistent-call-stack-b
(implies (consistent-thread-entry th cl hp)
(consistent-call-stack (thread-call-stack th) cl hp)))
(defthm consistent-call-stack-implies-wff-call-frame-top-frame
(implies (and (consistent-call-stack cstack cl hp)
(consp cstack))
(wff-call-frame (car cstack)))
:rule-classes :forward-chaining)
;; (acl2::set-match-free-error nil)
(defthm consistent-call-stack-implies-wff-call-frame-top-frame-b
(implies (and (consistent-call-stack cstack cl hp)
(consp cstack))
(wff-call-frame (car cstack))))
;; this is not a good backchain rule, although it is quite general
;; strong for people to use.
(defthm consistent-thread-entry-implies-wff-call-frame
(implies (consistent-thread-entry th cl hp)
(wff-call-frame (top (thread-call-stack th))))
:rule-classes :forward-chaining)
(defthm consistent-thread-entry-implies-wff-call-frame-b
(implies (consistent-thread-entry th cl hp)
(wff-call-frame (top (thread-call-stack th)))))
;;
;; this it could get from
;; consistent-call-stack-implies-wff-call-frame-top-frame-b
;; consistent-thread-entry-implies-consistent-call-stack-b
;; and definition of consistent-thread-entry
;;
;; Not it could not. Because of the free variable. 10/06/03
;;
(defthm consistent-state-implies-consistent-thread-entry
(implies (consistent-state s)
(consistent-thread-entry (thread-by-id (current-thread s)
(thread-table s))
(instance-class-table s)
(heap s)))
:rule-classes :forward-chaining)
(defthm consistent-thread-entry-consp-call-stack
(implies (consistent-thread-entry th cl hp)
(consp (thread-call-stack th)))
:rule-classes :forward-chaining)
;; need to prove some theorems about updating subcomponent in a disiplined way
;; will preserve the consistent-state or well-formed ness
(defthm wff-thread-set-wff-call-stack-remains-wff
(implies (and (wff-thread tt)
(consp cs))
(wff-thread (thread-set-call-stack cs tt)))
:hints (("Goal" :in-theory (enable wff-thread))))
(defthm thread-set-call-stack-not-change-thread-id
(equal (thread-id (thread-set-call-stack cs th))
(thread-id th))
:hints (("Goal" :in-theory (enable thread-set-call-stack))))
;; (include-book "../DJVM/consistent-state-properties")
(acl2::set-verify-guards-eagerness 0)
(defun safe-pushStack (value s)
(declare (xargs :guard (and (consistent-state s)
(not (mem '*native*
(method-accessflags
(deref-method (method-ptr
(current-frame s))
(instance-class-table s)))))
(<= (+ 1 (len (operand-stack (current-frame s))))
(max-stack s)))))
(mylet* ((curthread-id (current-thread s))
(old-thread-table (thread-table s))
(old-thread (thread-by-id curthread-id old-thread-table))
(old-call-stack (thread-call-stack old-thread))
(old-frame (top old-call-stack))
(old-op-stack (operand-stack old-frame))
(new-op-stack (push value old-op-stack))
(new-frame (frame-set-operand-stack new-op-stack old-frame))
(new-call-stack (push new-frame (pop old-call-stack)))
(new-thread (thread-set-call-stack new-call-stack old-thread))
(new-thread-table (replace-thread-table-entry old-thread
new-thread
old-thread-table)))
(state-set-thread-table new-thread-table s)))
(defun safe-pushCategory2 (value s)
(declare (xargs :guard (and (consistent-state s)
(not (mem '*native* (method-accessflags
(deref-method (method-ptr
(current-frame s))
(instance-class-table s)))))
(<= (+ 2 (len (operand-stack (current-frame s))))
(max-stack s)))))
(pushStack value (pushStack '(topx . topx) s)))
;;
;; Tue Jul 26 12:06:21 2005
;; fixed to make the life of base-untag-state.lisp easier!!
;;
|
