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
|
#|
(include-book "m5")
(certify-book "apprentice-state" 1)
JSM
|#
(in-package "M5")
; The material below is the output of jvm2acl2 on Apprentice.java.
(defconst *Apprentice-class-table*
(make-class-def
(list
(make-class-decl "Apprentice"
'("java.lang.Object")
'()
'()
'()
(list
'("<init>" () nil
(aload_0)
(invokespecial "java.lang.Object" "<init>" 0)
(return))
'("main" (java.lang.String[]) nil
(new "Container")
(dup)
(invokespecial "Container" "<init>" 0)
(astore_1)
(goto LABEL::TAG_0)
(LABEL::TAG_0 new "Job")
(dup)
(invokespecial "Job" "<init>" 0)
(astore_2)
(aload_2)
(aload_1)
(invokevirtual "Job" "setref" 1)
(aload_2)
(invokevirtual "java.lang.Thread" "start" 0)
(goto LABEL::TAG_0)))
'(REF -1))
(make-class-decl "Container"
'("java.lang.Object")
'("counter")
'()
'()
(list
'("<init>" () nil
(aload_0)
(invokespecial "java.lang.Object" "<init>" 0)
(return)))
'(REF -1))
(make-class-decl "Job"
'("java.lang.Thread" "java.lang.Object")
'("objref")
'()
'()
(list
'("<init>" () nil
(aload_0)
(invokespecial "java.lang.Thread" "<init>" 0)
(return))
'("incr" () nil
(aload_0)
(getfield "Job" "objref")
(astore_1)
(aload_1)
(monitorenter)
(LABEL::TAG_1 aload_0)
(getfield "Job" "objref")
(aload_0)
(getfield "Job" "objref")
(getfield "Container" "counter")
(iconst_1)
(iadd)
(putfield "Container" "counter")
(aload_1)
(monitorexit)
(goto LABEL::TAG_0)
(LABEL::TAG_2 astore_2)
(aload_1)
(monitorexit)
(aload_2)
(athrow)
(LABEL::TAG_0 aload_0)
(areturn))
'("setref" (Container) nil
(aload_0)
(aload_1)
(putfield "Job" "objref")
(return))
'("run" () nil
(goto LABEL::TAG_0)
(LABEL::TAG_0 aload_0)
(invokevirtual "Job" "incr" 0)
(pop)
(goto LABEL::TAG_0)))
'(REF -1)))))
(defconst *Apprentice-main*
'((new "Container")
(dup)
(invokespecial "Container" "<init>" 0)
(astore_1)
(goto LABEL::TAG_0)
(LABEL::TAG_0 new "Job")
(dup)
(invokespecial "Job" "<init>" 0)
(astore_2)
(aload_2)
(aload_1)
(invokevirtual "Job" "setref" 1)
(aload_2)
(invokevirtual "java.lang.Thread" "start" 0)
(goto LABEL::TAG_0)))
(defun Apprentice-ms ()
(make-state
(make-tt (push (make-frame 0
nil
nil
*Apprentice-main*
'UNLOCKED
nil)
nil))
nil
*Apprentice-class-table*))
(defun Apprentice ()
(m5_load (Apprentice-ms)))
|
