File: jvm-loader-primitives.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 (132 lines) | stat: -rw-r--r-- 4,843 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
(in-package "JVM")
(include-book "../M6-DJVM-shared/jvm-object-manipulation-primitives")
(include-book "../M6-DJVM-shared/jvm-state")
(include-book "../M6-DJVM-shared/jvm-type-value")


(acl2::set-verify-guards-eagerness 2)

; ---- primitives for converting ACL2 string 
;      to m6 array object, futher to a m6 string.

(defun countdown-measure-guard (bound offset)
  (and (integerp bound)
       (integerp offset)
       (<= offset bound)))

(defun countdown-measure (bound offset)
  (declare (xargs :guard (countdown-measure-guard bound offset)))
  (if (zp (- bound offset))
             0
           (+ 1 (- bound offset))))

(defun str-to-array-char-data (str offset bound) 
  (declare (xargs :measure  (countdown-measure bound offset)
                  :guard (and (countdown-measure-guard bound offset)
                              (<= 0 offset)
                              (stringp str)
                              (<= bound (length str)))))
    (if (zp (- bound offset))
        nil
      (cons (char-code (char str offset))
            (str-to-array-char-data str (+ offset 1) bound))))

(defun str-to-array-obj (str s)
  (declare (xargs :guard (and (stringp str)
                              (build-a-java-visible-instance-guard
                               "java.lang.Object" s))))
  (let* ((array-data (str-to-array-char-data str 0 (length str)))
         (bound (len array-data)))
    (make-array (make-array-type 'char) 
                bound 
                array-data
                S)))


(defun make-immediate-string-part (array offset bound)
  (cons "java.lang.String" 
        (list (cons "value"  array)
              (cons "offset" offset)
              (cons "count"  bound))))


(defun make-java-lang-string-visible-part (str S)
  (declare (xargs :guard (and (stringp str)
                              (wff-state s)
                              (wff-heap (heap s))
                              (build-a-java-visible-instance-guard
                               "java.lang.Object" s))))
  (mv-let (Object-jvp new-s1)
          (build-a-java-visible-instance "java.lang.Object" s)
          ;; build-a-javaString assume the String's superclass is Object.
          (mv-let (array new-s2)
                  (str-to-array-obj str new-s1)
                  (let* ((heap1 (heap new-s2))
                         (new-array-addr (alloc heap1))
                         (heap2 (bind new-array-addr array heap1))
                         (bound (length str))
                         (offset 0)
                         (string-obj  
                          (cons (make-immediate-string-part 
                                 new-array-addr offset bound)
                                Object-jvp)))
                    (mv string-obj
                        (update-trace new-array-addr (state-set-heap heap2 new-s2)))))))

(defthm alistp-bind-alistp
  (implies (alistp l)
           (alistp (bind x any l))))


(defthm make-java-lang-string-visible-part-preserve-wff-state
  (implies (wff-state s)
           (wff-state (mv-nth 1 (make-java-lang-string-visible-part str S)))))

(defthm make-java-lang-string-visible-part-preserve-wff-heap
  (implies (wff-heap (heap s))
           (wff-heap (heap  (mv-nth 1 (make-java-lang-string-visible-part str S))))))

(defthm make-java-lang-string-visible-part-no-change-class-table
  (equal (class-table (mv-nth 1 (make-java-lang-string-visible-part str S)))
         (class-table s)))


;; this functions are used in building the string object when we load constant
;; pool

(defun ACL2-str-to-JavaString (str S)
  (declare (xargs :guard (and (stringp str)
                              (wff-state s)
                              (wff-heap (heap s))
                              (build-a-java-visible-instance-guard
                               "java.lang.Object" s))))
  (let ((common-info     (build-common-info "java.lang.String"))
        (specific-info   (build-STRING-specific-info)))
    (mv-let (java-visible-portion new-state)
            (make-java-lang-string-visible-part str S)
            (mv (make-object common-info specific-info java-visible-portion)
                new-state))))


;; (in-theory (disable ACL2-str-to-JavaString))

(defun create-string-guard (str s)
  (and (stringp str)
       (wff-state s)
       (wff-heap (heap s))
       (build-a-java-visible-instance-guard "java.lang.Object" s)))

(defun ACL2-str-to-JavaString-ref (str S)
  (declare (xargs :guard (create-string-guard str s)))
  (mv-let (the-String-obj new-S)
          (ACL2-str-to-JavaString str S)
          (let* ((heap   (heap new-S))
                 (new-addr (alloc heap))
                 (new-heap (bind new-addr the-String-obj heap)))
            (mv new-addr
                (update-trace new-addr (state-set-heap new-heap new-s))))))

;-----------------