File: jvm-verifier.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 (44 lines) | stat: -rw-r--r-- 1,655 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
(in-package "JVM")
(include-book "../M6-DJVM-shared/jvm-class-table")
(include-book "../M6-DJVM-shared/jvm-state")

(defun class-rep-verified? (class-rep)
  (< (class-status class-rep) *CLASS_VERIFIED*))

;; temp implementation, which every class is verified.

(defun verify-class1 (class-rep s)
  (let* ((new-class-rep 
          (class-rep-set-class-status *CLASS_VERIFIED* class-rep))
         (old-instance-class-table (instance-class-table s))
         (new-instance-class-table 
          (replace-class-table-entry class-rep new-class-rep
                                     old-instance-class-table)))
    (state-set-instance-class-table 
     new-instance-class-table s)))
         

;; we can proof, if it reach the stage of verifying class,
;; loading must succeeded, (super must exists? except for java.lang.Object)

(defun check-super-class-isnt-final (class-rep s)
  (let* ((supername (super class-rep))
         (super-rep   (class-by-name supername (instance-class-table s)))
         (accessflags (class-accessflags super-rep)))
    (mem '*final* accessflags)))

(defun check-interface-super-class-is-JavaLangObject (class-rep s)
  (declare (ignore s))
  (let* ((supername (super class-rep)))
    (equal supername "java.lang.Object")))


(defun verify-class (class-rep s) 
  (if (not (check-super-class-isnt-final class-rep s))
      (fatalError "class-extends-final-class" s)
    (if (isInterface class-rep) 
        (if (not (check-interface-super-class-is-JavaLangObject class-rep s))
            (fatalError "interfaces-does-not-extends-JavaLangObject" s)
          (verify-class1 class-rep s))
      (verify-class1 class-rep s))))