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
|
(in-package "JVM")
(acl2::set-verify-guards-eagerness 2)
;----------------------------------------------------------------------
;; internal primitive stack operation
(defun push (item stack)
(cons item stack))
(defun top (stack)
(declare (xargs :guard (consp stack)))
(car stack))
(defun pop (stack)
(declare (xargs :guard (consp stack)))
(cdr stack))
(defun deref (ref heap)
(declare (xargs :guard (and (alistp heap)
(bound? ref heap))))
(binding ref heap))
(defun alloc (heap)
(len heap)) ;; simple implementation of memory allocation heap
;-- primitives for dealing with array internal reprsentation ---
;; (acl2::set-verify-guards-eagerness 0)
;; Tue Jan 13 14:57:51 2004. This is part of class loader!! We need to deal
;; with class loading sometime.
;;
;; Currently I am working on defining a consistent-state. No hurry on this.
;;; This is also used in raise-exception. Need to Assert it!! Thu Apr 8 20:48:21 2004
;; purely for M6's implementation. forget about guard verificaiton for now.
;; not really these following are for the implementation of loader... which
;; we haven't touched. ... Wed Dec 24 23:19:13 2003
(defun sub-list (l1 s1 len)
(declare (xargs :guard (and (integerp len)
(true-listp l1)
(integerp len)
(integerp s1)
(<= 0 len)
(<= 0 s1))))
(if (endp l1)
nil
(if (zp s1)
(if (zp len)
nil
(cons (car l1) (sub-list (cdr l1) 0 (- len 1))))
(sub-list (cdr l1) (- s1 1) len))))
(defun setChars (l1 s1 l2 s2 len)
(declare (xargs :guard (and (integerp len)
(true-listp l1)
(true-listp l2)
(integerp s1)
(integerp s2)
(equal (len l1) len)
(<= 0 s1)
(<= (+ s2 len) (len l2))
(<= s1 s2)
(<= 0 len)
(<= 0 s2))))
(app (sub-list l2 0 s2)
(app (sub-list l1 s1 len)
(sub-list l2 (+ s2 len) (- (len l2) (+ s2 len))))))
(defun charsp (chars)
(if (not (consp chars)) t
(and (characterp (car chars))
(charsp (cdr chars)))))
(defun make-acl2-string (chars)
(declare (xargs :guard (and (true-listp chars)
(charsp chars))))
(coerce chars 'string))
(defun chars-numsp (nums)
(if (not (consp nums)) t
(and (and (integerp (car nums))
(>= (car nums) 0)
(< (car nums) 256))
(chars-numsp (cdr nums)))))
(defun code-to-chars (nums)
(declare (xargs :guard (and (true-listp nums)
(chars-numsp nums))))
(if (endp nums)
nil
(cons (code-char (car nums))
(code-to-chars (cdr nums)))))
;----- add primitives for recording the Heap Object creation order in the AUX
; component of the State.
;(acl2::set-verify-guards-eagerness 2)
(defun make-trace (th-obj-counters rtrace)
(list (cons 'th-obj-counters th-obj-counters)
(cons 'rtrace rtrace)))
(defun th-counters (trace)
(declare (xargs :guard t))
(if (not (true-listp trace)) nil
(if (not (consp (nth 0 trace))) nil
(cdr (nth 0 trace)))))
(defun rtrace (trace)
(declare (xargs :guard t))
(if (not (true-listp trace)) nil
(if (not (consp (nth 1 trace))) nil
(cdr (nth 1 trace)))))
(defun init-trace ()
(make-trace nil nil))
(defun add-obj-th-count (obj-ref th trace)
(declare (xargs :guard t))
(if (not (alistp trace)) trace
(let ((counters (th-counters trace))
(rtrace (rtrace trace)))
(if (not (alistp counters)) trace
(if (bound? th counters)
(if (not (integerp (binding th counters))) trace
(let* ((new-count (+ 1 (binding th counters)))
(new-counters (bind th new-count counters))
(new-trace (cons (cons obj-ref (cons th new-count)) rtrace)))
(make-trace new-counters new-trace)))
(let* ((new-count 0)
(new-counters (bind th new-count counters))
(new-trace (cons (cons obj-ref (cons th new-count)) rtrace)))
(make-trace new-counters new-trace)))))))
;; (defconst *jvm-internal-primitives*
;; '(push
;; pop
;; pop
;; deref
;; alloc
;; sub-list
;; setChars
;; make-acl2-string
;; code-to-chars
;; make-trace
;; th-counters
;; rtrace
;; init-trace
;; add-obj-th-count))
|
