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))))))
;-----------------
|