File: jvm-semantic-primitives-2.lisp

package info (click to toggle)
acl2 8.6%2Bdfsg-2
  • links: PTS
  • area: main
  • in suites: trixie
  • size: 1,111,420 kB
  • sloc: lisp: 17,818,294; java: 125,359; python: 28,122; javascript: 23,458; cpp: 18,851; ansic: 11,569; perl: 7,678; xml: 5,591; sh: 3,976; makefile: 3,833; ruby: 2,633; yacc: 1,126; ml: 763; awk: 295; csh: 233; lex: 197; php: 178; tcl: 49; asm: 23; haskell: 17
file content (169 lines) | stat: -rw-r--r-- 5,749 bytes parent folder | download | duplicates (2)
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
(in-package "JVM")
(include-book "../M6-DJVM-shared/jvm-state")
(include-book "../M6-DJVM-shared/jvm-thread")
(include-book "../M6-DJVM-shared/jvm-object-type-hierachy")
(acl2::set-verify-guards-eagerness 0)

(defun set-curframe-sync-obj (obj-ref s)
  (let* ((tid (current-thread s))
         (old-thread-table (thread-table s))
         (old-thread (thread-by-id tid old-thread-table))
         (old-call-stack (thread-call-stack old-thread))
         (old-top-frame (top old-call-stack))
         (new-top-frame (frame-set-sync-obj-ref obj-ref old-top-frame))
         (new-call-stack (push new-top-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 set-top-frame-return-pc (pc s)
  (let* ((old-thread-table (thread-table s))
         (old-thread       (thread-by-id (current-thread s) old-thread-table))
         (old-call-stack   (thread-call-stack old-thread))
         (old-top-frame    (top old-call-stack))
         (new-top-frame    (frame-set-return-pc pc old-top-frame))
         (new-call-stack   (push new-top-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)))



;;;;;;;;; Consider the following as M6/DJVM dependent!! 
;;;;;;;;; moved to m6-semantics-primitives-2.lisp

;;;;;;;;; the pushFrame and popFrame maybe M6/DJVM dependent. (really depend
;;;;;;;;; how much code reuse we expect to have. 

;; ;;
;; ;; set the return pc to KILL_THREAD
;; ;; so when a corresponding return is executed, system know to kill thread. 
;; ;; when there is no active thread, program terminates.
;; ;;

;; ;; for those call back functions, we may not want to use same operation to get
;; ;; access the state. topStack etc. has guards that works only on valid
;; ;; opstacks. 

;; ;;
;; ;; We want to share a major portion of code between Defensive JVM and Regular
;; ;; JVM, we need call back function behave the same. we need Native method
;; ;; behave properly if they manipulate the operand stack.
;; ;;

;; ;; Do I want to get into this?? 
;; ;; (defun topStackAsRef (

;; ;;
;; ;; Mon Dec 29 00:32:23 2003




;; (defun initInitialThreadBehavior (s) 
;;   (let* ((array-ref (topStack s))
;;          (classname (secondStack s))
;;          (main-method-ptr (make-method-ptr classname "main" 
;;                                            '((array "java.lang.String"))
;;                                            'void))
;;          (mainMethod (getSpecialMethod main-method-ptr s)))
;;     (if (equal mainMethod nil)
;;         (stopThread (alertUser "does not have a main function" s))
;;       (if (not (mem '*public* (method-accessflags mainMethod)))
;;           (stopThread (alertUser "main must be public" s))
;;         (let* ((s1 (pushFrame main-method-ptr (list array-ref) s))
;;                (s2 (set-top-frame-return-pc 'KILL_THREAD s1)))
;;           (if (mem '*synchronized* (method-accessflags mainMethod))
;;               ;; why need a synchronize object recorded on the frame??  because
;;               ;; we need to release the monitor when we return from the
;;               ;; methods.
;;               (let* ((class-obj-ref (class-ref-by-name classname s2))
;;                      (s3 (set-curframe-sync-obj class-obj-ref s2)))
;;                 (mv-let (mstatus s4)
;;                     (monitorEnterX class-obj-ref s3)
;;                     (declare (ignore mstatus))
;;                     s4))
;;             (set-curframe-sync-obj -1 s2))))))) ;; use -1 to indicate null pointer.


;; (defun initThreadBehaviorFromThread (s)
;;   (let* ((s1 (popFrame s))
;;          (sync-obj-ref (sync-obj-ref (current-frame s1))))
;;     (if (not (equal sync-obj-ref -1))
;;         (mv-let (mstatus s2)
;;                 (monitorEnterX sync-obj-ref s1)
;;                 (declare (ignore mstatus))
;;                 s2)
;;      s1)))
                


;; (defun interruptedGetOutput1Behavior (s)
;;   (prog2$ (acl2::debug-print "interruptedGetOutput1Behavior called")
;;           (mv-let (os-ref s1)
;;                   (new-instance "java.io.PrintStream" (popFrame s))
;;                   (pushStack os-ref s1))))


;; (defun  newInstanceReturnObject (s) 
;;   (popFrame s))



;; (defun searchForFuncPtr1 (l)
;;   (if (endp l)
;;       nil
;;     (if (callback-func-ptr? (car l))
;;         (car l)
;;       (searchForFuncPtr1 (cdr l)))))


;; (defun searchForFuncPtr (s) 
;;   (let* ((cur-thread (thread-by-id (current-thread s) (thread-table s)))
;;          (operand-stack (operand-stack (top (thread-call-stack cur-thread)))))
;;     (searchForFuncPtr1 operand-stack))) 


;; (defun invoke-CUSTOMCODE (s)
;;   (let* ((call-back-func (searchForFuncPtr s))
;;          (funcname (callback-funcname call-back-func)))
;;     (cond ((equal funcname '*runClinit*) 
;;               (runClinit s))
;;           ((equal funcname '*initInitialThreadBehavior*)
;;            (initInitialThreadBehavior s))
;;           ((equal funcname '*newInstanceReturnObject*)
;;            (newInstanceReturnObject s))
;;           ((equal funcname  '*initThreadBehaviorFromThread*)
;;            (initThreadBehaviorFromThread s))
;;           ((equal funcname  '*interruptedGetOutput1Behavior*)
;;            (interruptedGetOutput1Behavior s))
;;           (t s)))) ;; so far unknown