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
|
(in-package "M6")
(include-book "../M6/m6-type-value")
(include-book "../M6/m6-thread")
(acl2::set-verify-guards-eagerness 0)
(include-book "../M6-DJVM-shared/jvm-frame-manipulation-primitives")
;; (defun topStack (s)
;; (top (operand-stack (current-frame s))))
;; (defun secondStack (s)
;; (topStack (popStack s)))
(defun thirdStack (s)
(topStack (popStack (popStack s))))
(defun fourthStack (s)
(topStack (popStack (popStack (popStack s)))))
(defun fifthStack (s)
(topStack (popStack (popStack (popStack (popStack s))))))
(defun popStackN (n s)
(if (zp n)
s
(popStackN (- n 1) (popStack s))))
(defun pushLong (v s)
(pushStack v (pushStack 'topx s)))
;; push 'topx then push v. :Thu Jan 15 21:17:00 2004
;; OK.
;;
;; reverse the order of Long representation Thu Jan 15 21:23:47 2004
;;;
;;; does it comply with the current BCV representation?? No. Mon Jan 31
;;; 15:40:14 2005.
;;;
;;; BCV representation is fixed by StackMap generated by static checker.
;;; Mon Jan 31 15:42:27 2005
;; Decision, shall we just fix how the mapping from djvm-state to sig-state?
;; Yes. Let me do that. Mon Jan 31 15:43:05 2005
;;;
;; Fixed already in Dec. 2004. Mon Jan 31 15:44:56 2005
;;
(defun popLong (s)
(popStack (popStack s)))
(defun topLong (s)
(topStack s))
;-- primitives for executing the method.
;; FRAME operation
;; We will rely on guard verification!
;; (defun pushFrame0 (new-frame s)
;; (let* ((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))
;; (new-call-stack (push new-frame old-call-stack))
;; (new-pc 0) ;; set new pc
;; (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-pc new-pc (state-set-thread-table new-thread-table s))))
;; (defun pushFrame (method-ptr initial-locals s)
;; (let* ((new-operand-stack (make-init-operand-stack))
;; (return-pc (pc s))
;; (new-frame (make-frame return-pc new-operand-stack initial-locals
;; method-ptr -1)))
;; (pushFrame0 new-frame s)))
;; (defun popFrame (s)
;; (let* ((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))
;; (new-pc (return-pc (top old-call-stack)))
;; (new-call-stack (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-pc new-pc (state-set-thread-table new-thread-table s))))
;; do nothing if invoked on illegal input. maybe I should add some
;; output to indicate guard violation.
(defun build-initial-local1 (rev-arg-types operand-stack)
(if (endp rev-arg-types)
nil
(if (equal (type-size (car rev-arg-types)) 2)
(cons 'topx (cons (top (pop operand-stack))
;; assuming in locals, a Long value is stored in the first slot.
(build-initial-local1 (cdr rev-arg-types) (pop (pop
operand-stack)))))
(cons (top operand-stack) (build-initial-local1 (cdr rev-arg-types) (pop operand-stack))))))
(defun fill-top (n)
(if (zp n) nil
(cons 'topx (fill-top (- n 1)))))
(defun size-of-param (arg-types)
(if (endp arg-types)
0
(if (equal (type-size (car arg-types)) 2)
(+ 2 (size-of-param (cdr arg-types)))
(+ 1 (size-of-param (cdr arg-types))))))
(defun build-initial-local (arg-types operand-stack length)
(let* ((reversed-params (build-initial-local1 (reverse arg-types)
operand-stack))
(reversed-locals (app (fill-top (- length (len reversed-params)))
reversed-params)))
(reverse reversed-locals)))
; need to fix this!! Mon Oct 25 16:30:21 2004
; We need all slot being preallocated!!
; primitives for how to get a method-ptr to store in the call frame
(defun method-rep-to-method-ptr (method-rep)
(make-method-ptr (method-classname method-rep)
(method-methodname method-rep)
(method-args method-rep)
(method-returntype method-rep)))
(defun pushFrameWithPop (obj-ref method-rep s)
(let* ((args (method-args method-rep))
(method-ptr (method-rep-to-method-ptr method-rep))
(locals (build-initial-local (method-args method-rep)
(operand-stack (current-frame s))
(method-maxlocals method-rep)))
(accessflags (method-accessflags method-rep)))
(if (mem '*static* accessflags) ;; no this pointer
(pushFrame method-ptr locals
(popStackN (size-of-param args) s))
(pushFrame method-ptr (cons obj-ref locals) (popStackN (+ (size-of-param
args) 1) s)))))
;---
|
