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
|
[See README for an explanation of this file.]
DOWNLOAD
--------
http://www.cs.utexas.edu/~hbl/dissertation/dist.tgz
DIRECTORY STRUCTURE
-------------------
top-level-directory
|
|--- README -- this file
|
|--- src/ -- ACL2 inputs
| |
| |--- common/ -- supporting JVM related materials
| |
| |--- M6-DJVM-shared/ -- data structures/operations (Chapter 4 & 6)
| |
| |--- M6/ -- JVM model in ACL2. (Chapter 4)
| |
| |--- DJVM/ -- Defensive JVM in ACL2. (Chapter 6)
| | |
| | |--- INST/ -- Leaf-level lemmas and libraries (Section 7.4)
| |
| |--- BCV/ -- CLDC bytecode verifier (JSR139)
| |
| | (Chapter 5 and Section 7.3)
| |
| |--- main/ -- Top level proof decomposition (Section 7.2)
| |
| |--- hanoi/ -- Tower hanoi example (Chapter 3)
| |
| |--- small/ -- Small machine example (Section 7.1)
|
|
|--- data/ -- Java libraries to run M6 with
|
|--- bin/ -- misc. scripts
|
|--- lib/ -- jvm2acl2 tool (in Java)
|
|--- papers/
| |
|--- dissertation/ -- the dissertation
UNPACK AND REBUILD ALL ACL2 PROOFS
----------------------------------
cd src/
make ACL2=<your-acl2> BASE=.. all
USING ACL2: HANOI TOWER EXAMPLE (Chapter 3)
-------------------------------
ACL2 as a programming language for modeling (Section 3.1)
Primitives/data structures:
src/hanoi/stack.lisp
src/hanoi/state.lisp
src/hanoi/move.lisp
Interpreter model:
src/hanoi/hanoi-model.lisp
The move planner:
src/hanoi/hanoi-solution.lisp
ACL2 as a mathematical logic for specification (Section 3.2)
Operational specifiation:
src/hanoi/hanoi-model.lisp
Functional specification:
src/hanoi/hanoi-solution.lisp
Safety specification:
src/hanoi/hanoi-safety.lisp
ACL2 as a theorem prover for computer-aided verification (Section 3.3)
meet the functional specification:
src/hanoi/hanoi-solution.lisp
Meet the safety specification:
src/hanoi/hanoi-safety.lisp
JVM MODEL: M6 (Chapter 4)
-------------
See src/M6/m6-*.lisp
A good starting point is:
src/M6/m6-interpreter.lisp
State representation: (Section 4.2.1)
src/M6/m6-state.lisp
src/M6/m6-thread.lisp
src/M6/m6-class-table.lisp
...
State manipulation primitives: (Section 4.2.2)
src/M6/m6-frame-manipulation-primitives.lisp
...
State transition functions: (Section 4.2.3)
src/M6/m6-bytecode.lisp
...
Top level interpreter loop: (Section 4.3.1)
src/M6/m6-interpreter.lisp
Class initialization: (Section 4.3.2)
src/M6/m6-static-initializer.lisp
Dynamic class loading: (Section 4.3.3)
src/M6/m6-loader.lisp
src/M6-DJVM-shared/jvm-loader.lisp
RUNNING M6 AS A JVM SIMULATOR
-----------------------------
Assuming "acl2" is in your executable search path.
1. See the rough example program:
src/M6/example-*.lisp
including src/M6/example-parallel-factorial.lisp
4. To run a new Java program:
a) compile your Java program
b) convert the .class file into format M6 can use.
i) at the top level directory execute "source set-env"
ii) java jvm2acl2 output <yourclassfiles.class>
iii) edit src/M6-DJVM-shared/cldc-classtable.lisp and merge
forms from output-classtable.lisp
c) edit src/M6/example-template.lisp to set up an initial state
for executing the program
d) start ACL2 and load the edited src/M6/example-template.lisp
JVM PROPERTY VERIFICATION EXAMPLE USING M6 (Section 4.4.1)
------------------------------------------
Dynamic class loading preserves invariant on JVM state.
See src/M6-DJVM-shared/jvm-loader-property.lisp
Replay the proof:
cd src
make M6-DJVM-shared/jvm-loader-property.cert
JAVA PROGRAM VERIFICATION EXAMPLE USING M6 (Section 4.4.2)
------------------------------------------
Replay the proof:
1) ADD1 program adds one:
cd src
make M6/ADD1-program-correct.improved.cert
2) Factorial program computes factorial:
cd src
make M6/factorial-program-correct.improved.cert
CLDC BYTECODE VERIFER (Chapter 5)
---------------------
See src/BCV/typechecker.lisp (Section 5.3)
Compare with Prolog-rules
src/BCV/typechecker.pl (Section 5.2)
Our alternative type checker definition
src/BCV/typechecker-simple.lisp (Section 7.3.2)
RUNNING CLDC BYTECODE VERIFER
-----------------------------
See src/BCV/typechecker-test-*.lisp
CLDC BYTECODE VERIFIER SIMPLE PROPERTY VERIFIED (Section 5.4)
-----------------------------------------------
See src/BCV/typechecker-property.lisp
JVM SAFETY SPECIFICATION (Chapter 6)
------------------------
The defensive JVM (DJVM) (Section 6.2)
src/DJVM/djvm-*.lisp
src/DJVM/INST/<INST>.lisp
src/M6-DJVM-shared/jvm-*.lisp
Global Inductive Invariant (Section 6.4)
src/DJVM/consistent-state.lisp
src/DJVM/consistent-state-strong.lisp
src/DJVM/consistent-state-bcv-on-track.lisp
Guards for DJVM operations (Section 6.5)
src/DJVM/djvm-*.lisp
src/DJVM/INST/<INST>.lisp
src/M6-DJVM-shared/jvm-*.lisp
FRAMEWORK AND PROOFS (Chapter 7)
--------------------
[
NOTE to replay a proof:
cd src/
make INHIBIT="" ACL2=<youracl2> BASE=.. path/to/book.cert
ACL2 output is saved in path/to/book.out
]
Complete proof that Small machine is safe (Section 7.1)
src/small/*.lisp
Models:
M6-like interpreter: src/small/jvm-model.lisp (Section 7.1.1)
CLDC bytecode verifier: src/small/bcv-model.lisp
DJVM-like interpreter: src/small/djvm-model.lisp (Section 7.1.2)
src/small/djvm-<INST>.lisp
Intermediate bytecode verifier:
src/small/bcv-simple-model.lisp
Approach: (Section 7.1.3)
Alternative bytecode verifier is effective
Leaf level lemma:
src/small/<INST>.lisp
Supporting library for proving leaf level lemma:
src/small/djvm-<INST>.lisp
Overall proof:
src/small/djvm-is-safe.lisp
src/small/bcv-is-effective.lisp
"Reduction theorem":
original CLDC bytecode verifier is no-less effective
bcv-succeed-implies-bcv-simple-succeed.lisp
Bootstrap class loader Verified (Section 7.2)
See
src/DJVM/INST/base-consistent-state-load-class.lisp
src/DJVM/INST/base-load-class-normalize.lisp
src/M6-DJVM-shared/jvm-loader-guard-verification.lisp
Reduction theorem for CLDC bytecode verifier (Section 7.3)
See
src/BCV/bcv-succeed-implies-bcv-simple-succeed.lisp
Leaf-level lemma and supporting libraries (Section 7.4)
Leaf-level lemma: src/DJVM/INST/<INST>.lisp
Supporting libraries: src/DJVM/INST/base-*.lisp
Using leaf-level lemma for constructing top level proof:
src/main/djvm-is-safe.lisp
src/main/bcv-is-effective.lisp
|
