summaryrefslogtreecommitdiff
path: root/books/workshops/2003/moore_vcg/support
diff options
context:
space:
mode:
Diffstat (limited to 'books/workshops/2003/moore_vcg/support')
-rw-r--r--books/workshops/2003/moore_vcg/support/README11
-rw-r--r--books/workshops/2003/moore_vcg/support/certify.lsp172
-rw-r--r--books/workshops/2003/moore_vcg/support/demo.acl27
-rw-r--r--books/workshops/2003/moore_vcg/support/demo.lisp714
-rw-r--r--books/workshops/2003/moore_vcg/support/m5.acl2160
-rw-r--r--books/workshops/2003/moore_vcg/support/m5.lisp3032
-rw-r--r--books/workshops/2003/moore_vcg/support/utilities.acl27
-rw-r--r--books/workshops/2003/moore_vcg/support/utilities.lisp209
-rw-r--r--books/workshops/2003/moore_vcg/support/vcg-examples.acl26
-rw-r--r--books/workshops/2003/moore_vcg/support/vcg-examples.lisp904
10 files changed, 5222 insertions, 0 deletions
diff --git a/books/workshops/2003/moore_vcg/support/README b/books/workshops/2003/moore_vcg/support/README
new file mode 100644
index 0000000..ba50c33
--- /dev/null
+++ b/books/workshops/2003/moore_vcg/support/README
@@ -0,0 +1,11 @@
+; Tail-Recursive Completion of Inductive Assertions
+; in an Operational Semantics Setting
+
+; J Strother Moore
+
+; This directory contains supporting material for the paper above.
+; To recertify the books here, type make to the linux prompt or
+; get into ACL2 while standing on this directory and type
+
+; (ld "certify.lsp" :ld-pre-eval-print t)
+
diff --git a/books/workshops/2003/moore_vcg/support/certify.lsp b/books/workshops/2003/moore_vcg/support/certify.lsp
new file mode 100644
index 0000000..93d7d98
--- /dev/null
+++ b/books/workshops/2003/moore_vcg/support/certify.lsp
@@ -0,0 +1,172 @@
+
+;(certify-book "defpun")
+;(u)
+
+(defpkg "LABEL" '(nil t))
+(defpkg "JVM" '(nil t))
+(defpkg "M5"
+ (set-difference-equal
+ (union-eq
+ '(JVM::SCHEDULED
+ JVM::UNSCHEDULED
+ JVM::REF
+ JVM::LOCKED
+ JVM::S_LOCKED
+ JVM::UNLOCKED
+ JVM::AALOAD
+ JVM::AASTORE
+ JVM::ACONST_NULL
+ JVM::ALOAD
+ JVM::ALOAD_0
+ JVM::ALOAD_1
+ JVM::ALOAD_2
+ JVM::ALOAD_3
+ JVM::ANEWARRAY
+ JVM::ARETURN
+ JVM::ARRAYLENGTH
+ JVM::ASTORE
+ JVM::ASTORE_0
+ JVM::ASTORE_1
+ JVM::ASTORE_2
+ JVM::ASTORE_3
+ JVM::BALOAD
+ JVM::BASTORE
+ JVM::BIPUSH
+ JVM::CALOAD
+ JVM::CASTORE
+ JVM::DUP
+ JVM::DUP_X1
+ JVM::DUP_X2
+ JVM::DUP2
+ JVM::DUP2_X1
+ JVM::DUP2_X2
+ JVM::GETFIELD
+ JVM::GETSTATIC
+ JVM::GOTO
+ JVM::GOTO_W
+ JVM::I2B
+ JVM::I2C
+ JVM::I2L
+ JVM::I2S
+ JVM::IADD
+ JVM::IALOAD
+ JVM::IAND
+ JVM::IASTORE
+ JVM::ICONST_M1
+ JVM::ICONST_0
+ JVM::ICONST_1
+ JVM::ICONST_2
+ JVM::ICONST_3
+ JVM::ICONST_4
+ JVM::ICONST_5
+ JVM::IDIV
+ JVM::IF_ACMPEQ
+ JVM::IF_ACMPNE
+ JVM::IF_ICMPEQ
+ JVM::IF_ICMPGE
+ JVM::IF_ICMPGT
+ JVM::IF_ICMPLE
+ JVM::IF_ICMPLT
+ JVM::IF_ICMPNE
+ JVM::IFEQ
+ JVM::IFGE
+ JVM::IFGT
+ JVM::IFLE
+ JVM::IFLT
+ JVM::IFNE
+ JVM::IFNONNULL
+ JVM::IFNULL
+ JVM::IINC
+ JVM::ILOAD
+ JVM::ILOAD_0
+ JVM::ILOAD_1
+ JVM::ILOAD_2
+ JVM::ILOAD_3
+ JVM::IMUL
+ JVM::INEG
+ JVM::INSTANCEOF
+ JVM::INVOKESPECIAL
+ JVM::INVOKESTATIC
+ JVM::INVOKEVIRTUAL
+ JVM::IOR
+ JVM::IREM
+ JVM::IRETURN
+ JVM::ISHL
+ JVM::ISHR
+ JVM::ISTORE
+ JVM::ISTORE_0
+ JVM::ISTORE_1
+ JVM::ISTORE_2
+ JVM::ISTORE_3
+ JVM::ISUB
+ JVM::IUSHR
+ JVM::IXOR
+ JVM::JSR
+ JVM::JSR_W
+ JVM::L2I
+ JVM::LADD
+ JVM::LALOAD
+ JVM::LAND
+ JVM::LASTORE
+ JVM::LCMP
+ JVM::LCONST_0
+ JVM::LCONST_1
+ JVM::LDC
+ JVM::LDC_W
+ JVM::LDC2_W
+ JVM::LDIV
+ JVM::LLOAD
+ JVM::LLOAD_0
+ JVM::LLOAD_1
+ JVM::LLOAD_2
+ JVM::LLOAD_3
+ JVM::LMUL
+ JVM::LNEG
+ JVM::LOR
+ JVM::LREM
+ JVM::LRETURN
+ JVM::LSHL
+ JVM::LSHR
+ JVM::LSTORE
+ JVM::LSTORE_0
+ JVM::LSTORE_1
+ JVM::LSTORE_2
+ JVM::LSTORE_3
+ JVM::LSUB
+ JVM::LUSHR
+ JVM::LXOR
+ JVM::MONITORENTER
+ JVM::MONITOREXIT
+ JVM::MULTIANEWARRAY
+ JVM::NEW
+ JVM::NEWARRAY
+ JVM::NOP
+ JVM::POP
+ JVM::POP2
+ JVM::PUTFIELD
+ JVM::PUTSTATIC
+ JVM::RET
+ JVM::RETURN
+ JVM::SALOAD
+ JVM::SASTORE
+ JVM::SIPUSH
+ JVM::SWAP
+ ASSOC-EQUAL LEN NTH ZP SYNTAXP
+ QUOTEP FIX NFIX E0-ORDINALP E0-ORD-<)
+ (union-eq *acl2-exports*
+ *common-lisp-symbols-from-main-lisp-package*))
+ '(PC PROGRAM PUSH POP RETURN REVERSE STEP ++)))
+(certify-book "m5" 3)
+(u) (u) (u) (u)
+
+(include-book "m5")
+(certify-book "utilities" 1)
+(u) (u)
+
+(include-book "utilities")
+(certify-book "demo" 1)
+(u) (u)
+
+(include-book "utilities")
+(certify-book "vcg-examples" 1)
+(u) (u)
diff --git a/books/workshops/2003/moore_vcg/support/demo.acl2 b/books/workshops/2003/moore_vcg/support/demo.acl2
new file mode 100644
index 0000000..4b92f00
--- /dev/null
+++ b/books/workshops/2003/moore_vcg/support/demo.acl2
@@ -0,0 +1,7 @@
+(value :q)
+
+(lp)
+
+(include-book "utilities")
+
+(certify-book "demo" ? t)
diff --git a/books/workshops/2003/moore_vcg/support/demo.lisp b/books/workshops/2003/moore_vcg/support/demo.lisp
new file mode 100644
index 0000000..8d07589
--- /dev/null
+++ b/books/workshops/2003/moore_vcg/support/demo.lisp
@@ -0,0 +1,714 @@
+; Copyright (C) 2001, Regents of the University of Texas
+; Written by J Strother Moore
+; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
+
+; This book proves the correctness of a recursive static method
+; for factorial on M5.
+
+#|
+; Certification Instructions.
+
+(include-book
+ "utilities")
+
+(certify-book "demo" 1)
+
+J Moore
+
+Here is the Java for a factorial method.
+
+class Demo {
+
+ static int ans;
+
+ public static int fact(int n){
+ if (n>0)
+ {return n*fact(n-1);}
+ else return 1;
+ }
+
+ public static void main(String[] args){
+ int k = 4;
+ ans = fact(k+1);
+ return;
+ }
+ }
+
+If you put this into Demo.java and run
+
+% javac Demo.java
+% javap -o Demo
+
+you get the following:
+
+Compiled from Demo.java
+synchronized class Demo extends java.lang.Object
+ /* ACC_SUPER bit set */
+{
+ static int ans;
+ public static int fact(int);
+ public static void main(java.lang.String[]);
+ Demo();
+}
+
+Method int fact(int)
+ 0 iload_0
+ 1 ifle 13
+ 4 iload_0
+ 5 iload_0
+ 6 iconst_1
+ 7 isub
+ 8 invokestatic #5 <Method int fact(int)>
+ 11 imul
+ 12 ireturn
+ 13 iconst_1
+ 14 ireturn
+
+Method void main(java.lang.String[])
+ 0 iconst_4
+ 1 istore_1
+ 2 iload_1
+ 3 iconst_1
+ 4 iadd
+ 5 invokestatic #5 <Method int fact(int)>
+ 8 putstatic #4 <Field int ans>
+ 11 return
+
+Method Demo()
+ 0 aload_0
+ 1 invokespecial #3 <Method java.lang.Object()>
+ 4 return
+
+Below is the output of jvm2acl2 for M5.
+
+|#
+
+(in-package "M5")
+
+(defconst *Demo-class-table-in-tagged-form*
+ (make-class-def
+ (list
+ (make-class-decl
+ "Demo"
+ '("java.lang.Object")
+ '()
+ '("ans")
+ '()
+ (list
+ '("<init>" () nil
+ (aload_0)
+ (invokespecial "java.lang.Object" "<init>" 0)
+ (return))
+ '("fact" (int) nil
+ (iload_0)
+ (ifle LABEL::TAG_0)
+ (iload_0)
+ (iload_0)
+ (iconst_1)
+ (isub)
+ (invokestatic "Demo" "fact" 1)
+ (imul)
+ (ireturn)
+ (LABEL::TAG_0 iconst_1)
+ (ireturn))
+ '("main" (java.lang.String[]) nil
+ (iconst_4)
+ (istore_1)
+ (iload_1)
+ (iconst_1)
+ (iadd)
+ (invokestatic "Demo" "fact" 1)
+ (putstatic "Demo" "ans" nil)
+ (return)))
+ '(REF -1)))))
+
+(defconst *Demo-main*
+ '((iconst_4)
+ (istore_1)
+ (iload_1)
+ (iconst_1)
+ (iadd)
+ (invokestatic "Demo" "fact" 1)
+ (putstatic "Demo" "ans" nil)
+ (return)))
+
+(defun Demo-ms ()
+ (make-state
+ (make-tt (push (make-frame 0
+ nil
+ nil
+ *Demo-main*
+ 'UNLOCKED
+ "Demo")
+ nil))
+ nil
+ *Demo-class-table-in-tagged-form*))
+
+(defun Demo ()
+ (m5_load (Demo-ms)))
+
+; Here is the state created by (Demo):
+#|
+(((0 ((0 NIL NIL
+ ((ICONST_4)
+ (ISTORE_1)
+ (ILOAD_1)
+ (ICONST_1)
+ (IADD)
+ (INVOKESTATIC "Demo" "fact" 1)
+ (PUTSTATIC "Demo" "ans" NIL)
+ (RETURN))
+ UNLOCKED "Demo"))
+ SCHEDULED NIL))
+ ((0 ("java.lang.Class" ("<name>" . "java.lang.Object"))
+ ("java.lang.Object" ("monitor" . 0)
+ ("mcount" . 0)
+ ("wait-set" . 0)))
+ (1 ("java.lang.Class" ("<name>" . "ARRAY"))
+ ("java.lang.Object" ("monitor" . 0)
+ ("mcount" . 0)
+ ("wait-set" . 0)))
+ (2 ("java.lang.Class" ("<name>" . "java.lang.Thread"))
+ ("java.lang.Object" ("monitor" . 0)
+ ("mcount" . 0)
+ ("wait-set" . 0)))
+ (3 ("java.lang.Class" ("<name>" . "java.lang.String"))
+ ("java.lang.Object" ("monitor" . 0)
+ ("mcount" . 0)
+ ("wait-set" . 0)))
+ (4 ("java.lang.Class" ("<name>" . "java.lang.Class"))
+ ("java.lang.Object" ("monitor" . 0)
+ ("mcount" . 0)
+ ("wait-set" . 0)))
+ (5 ("java.lang.Class" ("<name>" . "Demo")
+ ("ans" . 0))
+ ("java.lang.Object" ("monitor" . 0)
+ ("mcount" . 0)
+ ("wait-set" . 0))))
+ (("java.lang.Object" NIL ("monitor" "mcount" "wait-set")
+ NIL NIL (("<init>" NIL NIL (RETURN)))
+ (REF 0))
+ ("ARRAY" ("java.lang.Object")
+ (("<array>" . *ARRAY*))
+ NIL NIL NIL (REF 1))
+ ("java.lang.Thread"
+ ("java.lang.Object")
+ NIL NIL NIL
+ (("run" NIL NIL (RETURN))
+ ("start" NIL NIL NIL)
+ ("stop" NIL NIL NIL)
+ ("<init>" NIL NIL (ALOAD_0)
+ (INVOKESPECIAL "java.lang.Object" "<init>" 0)
+ (RETURN)))
+ (REF 2))
+ ("java.lang.String"
+ ("java.lang.Object")
+ ("strcontents")
+ NIL NIL
+ (("<init>" NIL NIL (ALOAD_0)
+ (INVOKESPECIAL "java.lang.Object" "<init>" 0)
+ (RETURN)))
+ (REF 3))
+ ("java.lang.Class" ("java.lang.Object")
+ NIL NIL NIL
+ (("<init>" NIL NIL (ALOAD_0)
+ (INVOKESPECIAL "java.lang.Object" "<init>" 0)
+ (RETURN)))
+ (REF 4))
+ ("Demo" ("java.lang.Object")
+ NIL ("ans")
+ NIL
+ (("<init>" NIL NIL (ALOAD_0)
+ (INVOKESPECIAL "java.lang.Object" "<init>" 0)
+ (RETURN))
+ ("fact" (INT)
+ NIL (ILOAD_0)
+ (IFLE 12)
+ (ILOAD_0)
+ (ILOAD_0)
+ (ICONST_1)
+ (ISUB)
+ (INVOKESTATIC "Demo" "fact" 1)
+ (IMUL)
+ (IRETURN)
+ (ICONST_1)
+ (IRETURN))
+ ("main" (|JAVA.LANG.STRING[]|)
+ NIL (ICONST_4)
+ (ISTORE_1)
+ (ILOAD_1)
+ (ICONST_1)
+ (IADD)
+ (INVOKESTATIC "Demo" "fact" 1)
+ (PUTSTATIC "Demo" "ans" NIL)
+ (RETURN)))
+ (REF 5))))
+|#
+
+; But in the paper we discuss it component by component and
+; define constants for each. Note that we can write ICONST_4 or
+; ICONST\_4 in Common Lisp. We use the latter so that we can
+; pick these forms up and dump them into LaTeX.
+
+(defconst *Demo-thread-table*
+ (list
+ (cons 0
+ (make-thread
+ (push
+ (make-frame
+ 0
+ nil
+ nil
+ '((ICONST\_4)
+ (ISTORE\_1)
+ (ILOAD\_1)
+ (ICONST\_1)
+ (IADD)
+ (INVOKESTATIC "Demo" "fact" 1)
+ (PUTSTATIC "Demo" "ans" NIL)
+ (RETURN))
+ 'UNLOCKED
+ "Demo")
+ nil)
+ 'SCHEDULED
+ nil))))
+
+(defconst *Demo-heap*
+ '((0 . (("java.lang.Class"
+ ("<name>" . "java.lang.Object"))
+ ("java.lang.Object"
+ ("monitor" . 0)
+ ("mcount" . 0)
+ ("wait-set" . 0))))
+ (1 . (("java.lang.Class"
+ ("<name>" . "ARRAY"))
+ ("java.lang.Object"
+ ("monitor" . 0)
+ ("mcount" . 0)
+ ("wait-set" . 0))))
+ (2 . (("java.lang.Class"
+ ("<name>" . "java.lang.Thread"))
+ ("java.lang.Object"
+ ("monitor" . 0)
+ ("mcount" . 0)
+ ("wait-set" . 0))))
+ (3 . (("java.lang.Class"
+ ("<name>" . "java.lang.String"))
+ ("java.lang.Object"
+ ("monitor" . 0)
+ ("mcount" . 0)
+ ("wait-set" . 0))))
+ (4 . (("java.lang.Class"
+ ("<name>" . "java.lang.Class"))
+ ("java.lang.Object"
+ ("monitor" . 0)
+ ("mcount" . 0)
+ ("wait-set" . 0))))
+ (5 . (("java.lang.Class"
+ ("<name>" . "Demo")
+ ("ans" . 0))
+ ("java.lang.Object"
+ ("monitor" . 0)
+ ("mcount" . 0)
+ ("wait-set" . 0))))))
+
+(defconst *Demo-class-table*
+ '(("java.lang.Object"
+ NIL
+ ("monitor" "mcount" "wait-set")
+ NIL
+ NIL
+ (("<init>" NIL NIL (RETURN)))
+ (REF 0))
+ ("ARRAY"
+ ("java.lang.Object")
+ (("<array>" . *ARRAY*))
+ NIL
+ NIL
+ NIL
+ (REF 1))
+ ("java.lang.Thread"
+ ("java.lang.Object")
+ NIL
+ NIL
+ NIL
+ (("run" NIL NIL (RETURN))
+ ("start" NIL NIL NIL)
+ ("stop" NIL NIL NIL)
+ ("<init>" NIL NIL (ALOAD\_0)
+ (INVOKESPECIAL "java.lang.Object" "<init>" 0)
+ (RETURN)))
+ (REF 2))
+ ("java.lang.String"
+ ("java.lang.Object")
+ ("strcontents")
+ NIL
+ NIL
+ (("<init>" NIL NIL
+ (ALOAD\_0)
+ (INVOKESPECIAL "java.lang.Object" "<init>" 0)
+ (RETURN)))
+ (REF 3))
+ ("java.lang.Class"
+ ("java.lang.Object")
+ NIL
+ NIL
+ NIL
+ (("<init>" NIL NIL
+ (ALOAD\_0)
+ (INVOKESPECIAL "java.lang.Object" "<init>" 0)
+ (RETURN)))
+ (REF 4))
+ ("Demo"
+ ("java.lang.Object")
+ NIL
+ ("ans")
+ NIL
+ (("<init>" NIL NIL
+ (ALOAD\_0)
+ (INVOKESPECIAL "java.lang.Object" "<init>" 0)
+ (RETURN))
+ ("fact" (INT) NIL
+ (ILOAD\_0)
+ (IFLE 12)
+ (ILOAD\_0)
+ (ILOAD\_0)
+ (ICONST\_1)
+ (ISUB)
+ (INVOKESTATIC "Demo" "fact" 1)
+ (IMUL)
+ (IRETURN)
+ (ICONST\_1)
+ (IRETURN))
+ ("main" (|JAVA.LANG.STRING[]|) NIL
+ (ICONST\_4)
+ (ISTORE\_1)
+ (ILOAD\_1)
+ (ICONST\_1)
+ (IADD)
+ (INVOKESTATIC "Demo" "fact" 1)
+ (PUTSTATIC "Demo" "ans" NIL)
+ (RETURN)))
+ (REF 5))))
+
+(defconst *Demo-state*
+ (make-state *demo-thread-table*
+ *demo-heap*
+ *demo-class-table*))
+
+(defthm demo-state-is-demo
+ (equal (Demo)
+ *Demo-state*)
+ :rule-classes nil)
+
+; The Mathematical Function
+
+(defun factorial (n)
+ (if (zp n)
+ 1
+ (* n (factorial (- n 1)))))
+
+(defthm integerp-factorial
+ (integerp (factorial n))
+ :rule-classes :type-prescription)
+
+; A Schedule that Runs fact to Completion
+
+(defun fact-sched (th n)
+ (if (zp n)
+ (repeat th 5)
+ (append (repeat th 7)
+ (fact-sched th (- n 1))
+ (repeat th 2))))
+
+(defthm len-repeat
+ (equal (len (repeat th n)) (nfix n)))
+
+(defthm len-append
+ (equal (len (append a b))
+ (+ (len a) (len b))))
+
+(defthm len-fact-sched
+ (equal (len (fact-sched th n))
+ (+ 5 (* 9 (nfix n)))))
+
+; Playing Around with Main
+
+; This schedule executes main to termination.
+
+(defun main-sched (th)
+ (append (repeat th 5)
+ (fact-sched th 5)
+ (repeat th 2)))
+
+(defthm sample-execution
+ (equal (static-field-value "Demo" "ans"
+ (run (main-sched 0) *Demo-state*))
+ 120)
+ :rule-classes nil)
+
+#|
+
+; Below is a fact-test function. I define it in raw Lisp rather
+; than ACL2 so that I can time the execution of the JVM model
+; without timing the construction of the schedule. To define
+; this function, exit the loop with :q and do these two forms.
+
+(in-package "M5")
+(compile
+ (defun fact-test (n)
+ (format t "Computing schedule for ~a.~%" n)
+ (let ((sched (append (repeat 0 1)
+ (fact-sched 0 n)
+ (repeat 0 2))))
+ (format t "Schedule length: ~a.~%" (len sched))
+ (time
+ (static-field-value
+ "Demo" "ans"
+ (run sched
+ (make-state
+ (list
+ (cons 0
+ (make-thread
+ (push
+ (make-frame
+ 0
+ (list n)
+ nil
+ '((ILOAD\_0)
+ (INVOKESTATIC "Demo" "fact" 1)
+ (PUTSTATIC "Demo" "ans" NIL)
+ (RETURN))
+ 'UNLOCKED
+ "Demo")
+ nil)
+ 'SCHEDULED
+ nil)))
+ *demo-heap*
+ *demo-class-table*)))))))
+; Allocate additional bignum space
+(si::allocate 'lisp::bignum 400 t)
+T
+
+; Then do things like (fact-test 17) or (fact-test 1000). On a 797
+; MHz Pentium III, the latter requires a schedule of length 9008 and
+; takes 0.100 seconds to execute, provided no (BIGNUM) gcs occur.
+; This gives a simulation speed of 90K JVM bytecodes per second.
+
+|#
+
+; Proving Fact Correct
+
+(defconst *fact-def*
+ '("fact" (INT) NIL
+ (ILOAD_0) ;;; 0
+ (IFLE 12) ;;; 1
+ (ILOAD_0) ;;; 4
+ (ILOAD_0) ;;; 5
+ (ICONST_1) ;;; 6
+ (ISUB) ;;; 7
+ (INVOKESTATIC "Demo" "fact" 1) ;;; 8
+ (IMUL) ;;; 11
+ (IRETURN) ;;; 12
+ (ICONST_1) ;;; 13
+ (IRETURN))) ;;; 14
+
+(defun poised-to-invoke-fact (th s n)
+ (and (equal (status th s) 'SCHEDULED)
+ (equal (next-inst th s) '(invokestatic "Demo" "fact" 1))
+ (equal n (top (stack (top-frame th s))))
+ (intp n)
+ (equal (lookup-method "fact" "Demo" (class-table s))
+ *fact-def*)))
+
+(defun induction-hint (th s n)
+ (if (zp n)
+ s
+ (induction-hint
+ th
+ (make-state ;;; (run (repeat th 7) s)
+ (bind
+ th
+ (make-thread
+ (push
+ (make-frame
+ 8
+ (list (top (stack (top-frame th s))))
+ (push (- (top (stack (top-frame th s))) 1)
+ (push (top (stack (top-frame th s)))
+ nil))
+ (method-program *fact-def*)
+ 'UNLOCKED
+ "Demo")
+ (push (make-frame (+ 3 (pc (top (call-stack th s))))
+ (locals (top (call-stack th s)))
+ (pop (stack (top (call-stack th s))))
+ (program (top (call-stack th s)))
+ (sync-flg (top (call-stack th s)))
+ (cur-class (top (call-stack th s))))
+ (pop (call-stack th s))))
+ 'scheduled
+ (rref th s))
+ (thread-table s))
+ (heap s)
+ (class-table s))
+ (- n 1))))
+
+; The make-state in the induction-hint above is equivalent to
+; (run (repeat th 7) s), under the hypotheses that s is poised to
+; invoke fact and that n is non-0. We prove that below, just to
+; demonstrate this claim. The import of this claim is that we
+; could use this to help generate the induction hint, i.e., the
+; make-state is not "magic."
+
+(defthm induction-hint-explanation
+ (implies (and (poised-to-invoke-fact th s n)
+ (not (zp n)))
+ (equal (run (repeat th 7) s)
+ (make-state ;;; (run (repeat th 7) s)
+ (bind
+ th
+ (make-thread
+ (push
+ (make-frame
+ 8
+ (list (top (stack (top-frame th s))))
+ (push (- (top (stack (top-frame th s))) 1)
+ (push (top (stack (top-frame th s)))
+ nil))
+ (method-program *fact-def*)
+ 'UNLOCKED
+ "Demo")
+ (push (make-frame (+ 3 (pc (top (call-stack th s))))
+ (locals (top (call-stack th s)))
+ (pop (stack (top (call-stack th s))))
+ (program (top (call-stack th s)))
+ (sync-flg (top (call-stack th s)))
+ (cur-class (top (call-stack th s))))
+ (pop (call-stack th s))))
+ 'scheduled
+ (rref th s))
+ (thread-table s))
+ (heap s)
+ (class-table s))))
+ :rule-classes nil)
+
+(defthm fact-is-correct
+ (implies (poised-to-invoke-fact th s n)
+ (equal
+ (run (fact-sched th n) s)
+ (modify th s
+ :pc (+ 3 (pc (top-frame th s)))
+ :stack (push (int-fix (factorial n))
+ (pop (stack (top-frame th s)))))))
+ :hints (("Goal"
+ :induct (induction-hint th s n))))
+
+(in-theory (disable fact-sched))
+
+(defthm weak-version-of-fact-is-correct
+ (implies (poised-to-invoke-fact th s n)
+ (equal (top
+ (stack
+ (top-frame
+ th
+ (run (fact-sched th n) s))))
+ (int-fix (factorial n)))))
+
+; Symbolic Computation and Use of fact as a Subroutine
+
+(defthm symbolic-computation
+ (implies
+ (intp (+ 1 k))
+ (equal
+ (nth 3
+ (locals
+ (top-frame 0
+ (run (append (repeat 0 4)
+ (fact-sched 0 (+ 1 k))
+ (repeat 0 2))
+ (make-state
+ (make-tt
+ (push
+ (make-frame 0
+ (list v0 v1 v2 k)
+ stk
+ '((iconst_2)
+ (iload_3)
+ (iconst_1)
+ (iadd)
+ (invokestatic "Demo" "fact" 1)
+ (imul)
+ (istore_3))
+ 'UNLOCKED
+ "Test")
+ nil))
+ *demo-heap*
+ *demo-class-table*)))))
+
+ (int-fix (* 2 (factorial (+ 1 k)))))))
+
+; In the steps below we demonstrate the key steps in the
+; simplification above, to check the claims made in the paper.
+
+(defun alpha (pc locals stk)
+ (make-state
+ (make-tt
+ (push (make-frame pc
+ locals
+ stk
+ '((iconst_2)
+ (iload_3)
+ (iconst_1)
+ (iadd)
+ (invokestatic "Demo" "fact" 1)
+ (imul)
+ (istore_3))
+ 'UNLOCKED
+ "Test")
+ nil))
+ *demo-heap*
+ *demo-class-table*))
+
+(defthm symbolic-computation-step1
+ (implies
+ (intp (+ 1 k))
+ (equal (run (append (repeat 0 4)
+ (fact-sched 0 (+ 1 k))
+ (repeat 0 2))
+ (alpha 0 (list v0 v1 v2 k) stk))
+ (run (repeat 0 2)
+ (run (fact-sched 0 (+ 1 k))
+ (run (repeat 0 4)
+ (alpha 0 (list v0 v1 v2 k) stk)))))))
+
+(defthm symbolic-computation-step2
+ (implies
+ (intp (+ 1 k))
+ (equal (run (repeat 0 4)
+ (alpha 0 (list v0 v1 v2 k) stk))
+ (alpha 4 (list v0 v1 v2 k)
+ (push (+ 1 k) (push 2 stk))))))
+
+(defthm symbolic-computation-step3
+ (implies
+ (intp (+ 1 k))
+ (equal (run (fact-sched 0 (+ 1 k))
+ (alpha 4 (list v0 v1 v2 k)
+ (push (+ 1 k) (push 2 stk))))
+ (alpha 7 (list v0 v1 v2 k)
+ (push (int-fix (factorial (+ 1 k)))
+ (push 2 stk))))))
+
+
+(defthm symbolic-computation-step4
+ (implies
+ (intp (+ 1 k))
+ (equal (run (repeat 0 2)
+ (alpha 7 (list v0 v1 v2 k)
+ (push (int-fix (factorial (+ 1 k)))
+ (push 2 stk))))
+ (alpha 9 (list v0 v1 v2
+ (int-fix
+ (* 2 (factorial (+ 1 k))))) stk))))
+
diff --git a/books/workshops/2003/moore_vcg/support/m5.acl2 b/books/workshops/2003/moore_vcg/support/m5.acl2
new file mode 100644
index 0000000..3113f2e
--- /dev/null
+++ b/books/workshops/2003/moore_vcg/support/m5.acl2
@@ -0,0 +1,160 @@
+(value :q)
+
+(lp)
+
+(defpkg "LABEL" '(nil t))
+(defpkg "JVM" '(nil t))
+
+(DEFPKG "M5"
+ (set-difference-equal
+ (union-eq '(JVM::SCHEDULED
+ JVM::UNSCHEDULED
+ JVM::REF
+ JVM::LOCKED
+ JVM::S_LOCKED
+ JVM::UNLOCKED
+ JVM::AALOAD
+ JVM::AASTORE
+ JVM::ACONST_NULL
+ JVM::ALOAD
+ JVM::ALOAD_0
+ JVM::ALOAD_1
+ JVM::ALOAD_2
+ JVM::ALOAD_3
+ JVM::ANEWARRAY
+ JVM::ARETURN
+ JVM::ARRAYLENGTH
+ JVM::ASTORE
+ JVM::ASTORE_0
+ JVM::ASTORE_1
+ JVM::ASTORE_2
+ JVM::ASTORE_3
+ JVM::BALOAD
+ JVM::BASTORE
+ JVM::BIPUSH
+ JVM::CALOAD
+ JVM::CASTORE
+ JVM::DUP
+ JVM::DUP_X1
+ JVM::DUP_X2
+ JVM::DUP2
+ JVM::DUP2_X1
+ JVM::DUP2_X2
+ JVM::GETFIELD
+ JVM::GETSTATIC
+ JVM::GOTO
+ JVM::GOTO_W
+ JVM::I2B
+ JVM::I2C
+ JVM::I2L
+ JVM::I2S
+ JVM::IADD
+ JVM::IALOAD
+ JVM::IAND
+ JVM::IASTORE
+ JVM::ICONST_M1
+ JVM::ICONST_0
+ JVM::ICONST_1
+ JVM::ICONST_2
+ JVM::ICONST_3
+ JVM::ICONST_4
+ JVM::ICONST_5
+ JVM::IDIV
+ JVM::IF_ACMPEQ
+ JVM::IF_ACMPNE
+ JVM::IF_ICMPEQ
+ JVM::IF_ICMPGE
+ JVM::IF_ICMPGT
+ JVM::IF_ICMPLE
+ JVM::IF_ICMPLT
+ JVM::IF_ICMPNE
+ JVM::IFEQ
+ JVM::IFGE
+ JVM::IFGT
+ JVM::IFLE
+ JVM::IFLT
+ JVM::IFNE
+ JVM::IFNONNULL
+ JVM::IFNULL
+ JVM::IINC
+ JVM::ILOAD
+ JVM::ILOAD_0
+ JVM::ILOAD_1
+ JVM::ILOAD_2
+ JVM::ILOAD_3
+ JVM::IMUL
+ JVM::INEG
+ JVM::INSTANCEOF
+ JVM::INVOKESPECIAL
+ JVM::INVOKESTATIC
+ JVM::INVOKEVIRTUAL
+ JVM::IOR
+ JVM::IREM
+ JVM::IRETURN
+ JVM::ISHL
+ JVM::ISHR
+ JVM::ISTORE
+ JVM::ISTORE_0
+ JVM::ISTORE_1
+ JVM::ISTORE_2
+ JVM::ISTORE_3
+ JVM::ISUB
+ JVM::IUSHR
+ JVM::IXOR
+ JVM::JSR
+ JVM::JSR_W
+ JVM::L2I
+ JVM::LADD
+ JVM::LALOAD
+ JVM::LAND
+ JVM::LASTORE
+ JVM::LCMP
+ JVM::LCONST_0
+ JVM::LCONST_1
+ JVM::LDC
+ JVM::LDC_W
+ JVM::LDC2_W
+ JVM::LDIV
+ JVM::LLOAD
+ JVM::LLOAD_0
+ JVM::LLOAD_1
+ JVM::LLOAD_2
+ JVM::LLOAD_3
+ JVM::LMUL
+ JVM::LNEG
+ JVM::LOR
+ JVM::LREM
+ JVM::LRETURN
+ JVM::LSHL
+ JVM::LSHR
+ JVM::LSTORE
+ JVM::LSTORE_0
+ JVM::LSTORE_1
+ JVM::LSTORE_2
+ JVM::LSTORE_3
+ JVM::LSUB
+ JVM::LUSHR
+ JVM::LXOR
+ JVM::MONITORENTER
+ JVM::MONITOREXIT
+ JVM::MULTIANEWARRAY
+ JVM::NEW
+ JVM::NEWARRAY
+ JVM::NOP
+ JVM::POP
+ JVM::POP2
+ JVM::PUTFIELD
+ JVM::PUTSTATIC
+ JVM::RET
+ JVM::RETURN
+ JVM::SALOAD
+ JVM::SASTORE
+ JVM::SIPUSH
+ JVM::SWAP
+ ASSOC-EQUAL LEN NTH ZP SYNTAXP
+ QUOTEP FIX NFIX E0-ORDINALP E0-ORD-<)
+ (union-eq *acl2-exports*
+ *common-lisp-symbols-from-main-lisp-package*))
+ '(PC PROGRAM PUSH POP RETURN REVERSE STEP ++)))
+
+(certify-book "m5" ? t)
diff --git a/books/workshops/2003/moore_vcg/support/m5.lisp b/books/workshops/2003/moore_vcg/support/m5.lisp
new file mode 100644
index 0000000..80a75ec
--- /dev/null
+++ b/books/workshops/2003/moore_vcg/support/m5.lisp
@@ -0,0 +1,3032 @@
+; Copyright (C) 2001, Regents of the University of Texas
+; Written by J Strother Moore and George Porter
+; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
+
+; M5.lisp
+; J Strother Moore <moore@cs.utexas.edu>
+; George Porter <george@cs.utexas.edu>
+;
+; Fixed arithmetic work by Robert Krug <rkrug@cs.utexas.edu>
+; Support for Arrays by Hanbing Liu <hbl@cs.utexas.edu>
+;
+; $Id: m5.lisp,v 1.1 2001/07/10 17:37:06 george Exp $
+
+#|
+
+(defpkg "LABEL" '(nil t))
+(defpkg "JVM" '(nil t))
+
+(DEFPKG "M5"
+ (set-difference-equal
+ (union-eq '(JVM::SCHEDULED
+ JVM::UNSCHEDULED
+ JVM::REF
+ JVM::LOCKED
+ JVM::S_LOCKED
+ JVM::UNLOCKED
+ JVM::AALOAD
+ JVM::AASTORE
+ JVM::ACONST_NULL
+ JVM::ALOAD
+ JVM::ALOAD_0
+ JVM::ALOAD_1
+ JVM::ALOAD_2
+ JVM::ALOAD_3
+ JVM::ANEWARRAY
+ JVM::ARETURN
+ JVM::ARRAYLENGTH
+ JVM::ASTORE
+ JVM::ASTORE_0
+ JVM::ASTORE_1
+ JVM::ASTORE_2
+ JVM::ASTORE_3
+ JVM::BALOAD
+ JVM::BASTORE
+ JVM::BIPUSH
+ JVM::CALOAD
+ JVM::CASTORE
+ JVM::DUP
+ JVM::DUP_X1
+ JVM::DUP_X2
+ JVM::DUP2
+ JVM::DUP2_X1
+ JVM::DUP2_X2
+ JVM::GETFIELD
+ JVM::GETSTATIC
+ JVM::GOTO
+ JVM::GOTO_W
+ JVM::I2B
+ JVM::I2C
+ JVM::I2L
+ JVM::I2S
+ JVM::IADD
+ JVM::IALOAD
+ JVM::IAND
+ JVM::IASTORE
+ JVM::ICONST_M1
+ JVM::ICONST_0
+ JVM::ICONST_1
+ JVM::ICONST_2
+ JVM::ICONST_3
+ JVM::ICONST_4
+ JVM::ICONST_5
+ JVM::IDIV
+ JVM::IF_ACMPEQ
+ JVM::IF_ACMPNE
+ JVM::IF_ICMPEQ
+ JVM::IF_ICMPGE
+ JVM::IF_ICMPGT
+ JVM::IF_ICMPLE
+ JVM::IF_ICMPLT
+ JVM::IF_ICMPNE
+ JVM::IFEQ
+ JVM::IFGE
+ JVM::IFGT
+ JVM::IFLE
+ JVM::IFLT
+ JVM::IFNE
+ JVM::IFNONNULL
+ JVM::IFNULL
+ JVM::IINC
+ JVM::ILOAD
+ JVM::ILOAD_0
+ JVM::ILOAD_1
+ JVM::ILOAD_2
+ JVM::ILOAD_3
+ JVM::IMUL
+ JVM::INEG
+ JVM::INSTANCEOF
+ JVM::INVOKESPECIAL
+ JVM::INVOKESTATIC
+ JVM::INVOKEVIRTUAL
+ JVM::IOR
+ JVM::IREM
+ JVM::IRETURN
+ JVM::ISHL
+ JVM::ISHR
+ JVM::ISTORE
+ JVM::ISTORE_0
+ JVM::ISTORE_1
+ JVM::ISTORE_2
+ JVM::ISTORE_3
+ JVM::ISUB
+ JVM::IUSHR
+ JVM::IXOR
+ JVM::JSR
+ JVM::JSR_W
+ JVM::L2I
+ JVM::LADD
+ JVM::LALOAD
+ JVM::LAND
+ JVM::LASTORE
+ JVM::LCMP
+ JVM::LCONST_0
+ JVM::LCONST_1
+ JVM::LDC
+ JVM::LDC_W
+ JVM::LDC2_W
+ JVM::LDIV
+ JVM::LLOAD
+ JVM::LLOAD_0
+ JVM::LLOAD_1
+ JVM::LLOAD_2
+ JVM::LLOAD_3
+ JVM::LMUL
+ JVM::LNEG
+ JVM::LOR
+ JVM::LREM
+ JVM::LRETURN
+ JVM::LSHL
+ JVM::LSHR
+ JVM::LSTORE
+ JVM::LSTORE_0
+ JVM::LSTORE_1
+ JVM::LSTORE_2
+ JVM::LSTORE_3
+ JVM::LSUB
+ JVM::LUSHR
+ JVM::LXOR
+ JVM::MONITORENTER
+ JVM::MONITOREXIT
+ JVM::MULTIANEWARRAY
+ JVM::NEW
+ JVM::NEWARRAY
+ JVM::NOP
+ JVM::POP
+ JVM::POP2
+ JVM::PUTFIELD
+ JVM::PUTSTATIC
+ JVM::RET
+ JVM::RETURN
+ JVM::SALOAD
+ JVM::SASTORE
+ JVM::SIPUSH
+ JVM::SWAP
+ ASSOC-EQUAL LEN NTH ZP SYNTAXP
+ QUOTEP FIX NFIX E0-ORDINALP E0-ORD-<)
+ (union-eq *acl2-exports*
+ *common-lisp-symbols-from-main-lisp-package*))
+ '(PC PROGRAM PUSH POP RETURN REVERSE STEP ++)))
+
+(certify-book "m5" 3)
+
+J & George
+|#
+
+(in-package "M5")
+
+(include-book "../../../../ordinals/e0-ordinal")
+(set-well-founded-relation e0-ord-<)
+
+; -----------------------------------------------------------------------------
+; Utilities
+
+(defun push (obj stack) (cons obj stack))
+(defun top (stack) (car stack))
+(defun pop (stack) (cdr stack))
+
+(defun popn (n stack)
+ (if (zp n)
+ stack
+ (popn (- n 1) (pop stack))))
+
+(defun bound? (x alist) (assoc-equal x alist))
+
+(defun bind (x y alist)
+ (cond ((endp alist) (list (cons x y)))
+ ((equal x (car (car alist)))
+ (cons (cons x y) (cdr alist)))
+ (t (cons (car alist) (bind x y (cdr alist))))))
+
+(defun binding (x alist) (cdr (assoc-equal x alist)))
+
+(defun op-code (inst) (car inst))
+(defun arg1 (inst) (car (cdr inst)))
+(defun arg2 (inst) (car (cdr (cdr inst))))
+(defun arg3 (inst) (car (cdr (cdr (cdr inst)))))
+
+(defun nullrefp (ref)
+ (equal ref '(ref -1)))
+
+; Imported from ACL2
+
+(defun reverse (x)
+ (if (consp x)
+ (append (reverse (cdr x)) (list (car x)))
+ nil))
+
+; The following are constants and functions related to fixed integer sizes
+
+(defconst *largest-integer-value* (- (expt 2 31) 1))
+(defconst *largest-long-value* (- (expt 2 63) 1))
+(defconst *most-negative-integer* (- (expt 2 31)))
+(defconst *most-negative-long* (- (expt 2 63)))
+
+; Coerce x to an unsigned integer which will fit in n bits.
+(defun u-fix (x n)
+ (mod (ifix x) (expt 2 n)))
+
+; Coerce x to a signed integer which will fit in n bits.
+(defun s-fix (x n)
+ (let ((temp (mod (ifix x) (expt 2 n))))
+ (if (< temp (expt 2 (1- n)))
+ temp
+ (- temp (expt 2 n)))))
+
+(defun byte-fix (x)
+ (s-fix x 8))
+
+(defun ubyte-fix (x)
+ (u-fix x 8))
+
+(defun short-fix (x)
+ (s-fix x 16))
+
+(defun int-fix (x)
+ (s-fix x 32))
+
+(defun uint-fix (x)
+ (u-fix x 32))
+
+(defun long-fix (x)
+ (s-fix x 64))
+
+(defun ulong-fix (x)
+ (u-fix x 64))
+
+(defun char-fix (x)
+ (u-fix x 16))
+
+(defun 6-bit-fix (x)
+ (u-fix x 6))
+
+(defun 5-bit-fix (x)
+ (u-fix x 5))
+
+(defun expt2 (n)
+ (expt 2 n))
+
+(defun shl (x n)
+ (* x (expt2 n)))
+
+(defun shr (x n)
+ (floor (* x (expt2 (- n))) 1))
+
+; -----------------------------------------------------------------------------
+; States
+
+(defun make-state (thread-table heap class-table)
+ (list thread-table heap class-table))
+(defun thread-table (s) (nth 0 s))
+(defun heap (s) (nth 1 s))
+(defun class-table (s) (nth 2 s))
+
+(defun make-thread (call-stack status rref)
+ (list call-stack status rref))
+
+(defun call-stack (th s)
+ (nth 0 (binding th (thread-table s))))
+
+(defun status (th s)
+ (nth 1 (binding th (thread-table s))))
+
+(defun rref (th s)
+ (nth 2 (binding th (thread-table s))))
+
+; -----------------------------------------------------------------------------
+; Class Declarations and the Class Table
+
+; The class table of a state is an alist. Each entry in a class table is
+; a "class declaration" and is of the form
+
+; (class-name super-class-names fields defs)
+
+; Note that the definition below of the Thread class includes a 'run' method,
+; which most applications will override. The definition is consistent
+; with the default run method provided by the Thread class [O'Reily]
+
+(defun make-class-decl (name superclasses fields sfields cp methods href)
+ (list name superclasses fields sfields cp methods href))
+
+(defun class-decl-name (dcl)
+ (nth 0 dcl))
+(defun class-decl-superclasses (dcl)
+ (nth 1 dcl))
+(defun class-decl-fields (dcl)
+ (nth 2 dcl))
+(defun class-decl-sfields (dcl)
+ (nth 3 dcl))
+(defun class-decl-cp (dcl)
+ (nth 4 dcl))
+(defun class-decl-methods (dcl)
+ (nth 5 dcl))
+(defun class-decl-heapref (dcl)
+ (nth 6 dcl))
+
+(defun base-class-def ()
+ (list (make-class-decl "java.lang.Object"
+ nil
+ '("monitor" "mcount" "wait-set")
+ '()
+ '()
+ '(("<init>" () nil (RETURN)))
+ '(REF -1))
+ (make-class-decl "ARRAY"
+ '("java.lang.Object")
+ '(("<array>" . *ARRAY*))
+ '()
+ '()
+ '()
+ '(REF -1))
+ (make-class-decl "java.lang.Thread"
+ '("java.lang.Object")
+ '()
+ '()
+ '()
+ '(("run" () nil
+ (RETURN))
+ ("start" () nil ())
+ ("stop" () nil ())
+ ("<init>" ()
+ nil
+ (aload_0)
+ (invokespecial "java.lang.Object" "<init>" 0)
+ (return)))
+ '(REF -1))
+ (make-class-decl "java.lang.String"
+ '("java.lang.Object")
+ '("strcontents")
+ '()
+ '()
+ '(("<init>" ()
+ nil
+ (aload_0)
+ (invokespecial "java.lang.Object" "<init>" 0)
+ (return)))
+ '(REF -1))
+ (make-class-decl "java.lang.Class"
+ '("java.lang.Object")
+ '()
+ '()
+ '()
+ '(("<init>" ()
+ nil
+ (aload_0)
+ (invokespecial "java.lang.Object" "<init>" 0)
+ (return)))
+ '(REF -1))))
+
+(defun make-class-def (list-of-class-decls)
+ (append (base-class-def) list-of-class-decls))
+
+; -----------------------------------------------------------------------------
+; A Constant Pool
+;
+; There is one constant pool per class
+
+; A constant pool is a list of entries. Each entry is either:
+;
+; '(INT n)
+; Where n is a 32-bit number, in the range specified by the JVM spec
+;
+; '(STRING (REF -1) "Hello, World!")
+; The 3rd element (a string) is resolved to a heap reference the
+; first time it is used. Once it is resolved, its reference is placed
+; as the second element (displacing the null ref currently there).
+
+(defun cp-make-int-entry (n)
+ (list 'INT n))
+
+(defun cp-make-string-entry (str)
+ (list 'STRING '(REF -1) str))
+
+(defun cp-string-resolved? (entry)
+ (not (equal (cadr (caddr entry)) -1)))
+
+(defun retrieve-cp (class-name class-table)
+ (class-decl-cp (bound? class-name class-table)))
+
+(defun update-ct-string-ref (class idx newval ct)
+ (let* ((class-entry (bound? class ct))
+ (oldstrval (caddr (nth idx (retrieve-cp class ct))))
+ (newstrentry (list 'STRING newval oldstrval))
+ (new-cp (update-nth idx
+ newstrentry
+ (class-decl-cp class-entry)))
+ (new-class-entry
+ (make-class-decl (class-decl-name class-entry)
+ (class-decl-superclasses class-entry)
+ (class-decl-fields class-entry)
+ (class-decl-sfields class-entry)
+ new-cp
+ (class-decl-methods class-entry)
+ (class-decl-heapref class-entry))))
+ (bind class (cdr new-class-entry) ct)))
+
+; -----------------------------------------------------------------------------
+; Thread Tables
+;
+; A "thread table" might be used to represent threads in m5. It consists of
+; a reference, a call stack, a flag to indicate whether its call-stack
+; should be stepped by the scheduler, and a ref to the original object
+; in the heap.
+;
+; Thread table:
+; ((n . (call-stack flag reverse-ref))
+; (n+1 . (call-stack flag reverse-ref)))
+;
+; The flags 'SCHEDULED and 'UNSCHEDULED correspond to two of the
+; four states threads can be in (according to [O'Reily]). For our
+; model, this will suffice.
+
+(defun make-tt (call-stack)
+ (bind 0 (list call-stack 'SCHEDULED nil) nil))
+
+(defun addto-tt (call-stack status heapRef tt)
+ (bind (len tt) (list call-stack status heapRef) tt))
+
+(defun mod-thread-scheduling (th sched tt)
+ (let* ((thrd (binding th tt))
+ (oldcs (car thrd))
+ (oldhr (caddr thrd))
+ (newTH (list oldcs sched oldhr)))
+ (bind th newTH tt)))
+
+(defun schedule-thread (th tt)
+ (mod-thread-scheduling th 'SCHEDULED tt))
+
+(defun unschedule-thread (th tt)
+ (mod-thread-scheduling th 'UNSCHEDULED tt))
+
+(defun rrefToThread (ref tt)
+ (cond ((endp tt) nil)
+ ((equal ref (cadddr (car tt))) (caar tt))
+ (t (rrefToThread ref (cdr tt)))))
+
+; ----------------------------------------------------------------------------
+; Helper function for determining if an object is a 'Thread' object
+
+(defun in-list (item list)
+ (cond ((endp list) nil)
+ ((equal item (car list)) t)
+ (t (in-list item (cdr list)))))
+
+(defun isThreadObject? (class-name class-table)
+ (let* ((class (bound? class-name class-table))
+ (psupers (class-decl-superclasses class))
+ (supers (cons class-name psupers)))
+ (or (in-list "java.lang.Thread" supers)
+ (in-list "java.lang.ThreadGroup" supers))))
+
+; ----------------------------------------------------------------------------
+; Helper functions for locking and unlocking objects
+
+; lock-object and unlock-object will obtain a lock on an instance
+; of an object, using th as the locking id (a thread owns a lock). If th
+; already has a lock on an object, then the mcount of the object is
+; incremented. Likewise if you unlock an object with mcount > 0, then
+; the lock will be decremented. Note: you must make sure that th can
+; and should get the lock, since this function will blindly go ahead and
+; get the lock
+
+(defun lock-object (th obj-ref heap)
+ (let* ((obj-ref-num (cadr obj-ref))
+ (instance (binding (cadr obj-ref) heap))
+ (obj-fields (binding "java.lang.Object" instance))
+ (new-mcount (+ 1 (binding "mcount" obj-fields)))
+ (new-obj-fields
+ (bind "monitor" th
+ (bind "mcount" new-mcount obj-fields)))
+ (new-object (bind "java.lang.Object" new-obj-fields instance)))
+ (bind obj-ref-num new-object heap)))
+
+(defun unlock-object (th obj-ref heap)
+ (let* ((obj-ref-num (cadr obj-ref))
+ (instance (binding (cadr obj-ref) heap))
+ (obj-fields (binding "java.lang.Object" instance))
+ (old-mcount (binding "mcount" obj-fields))
+ (new-mcount (ACL2::max 0 (- old-mcount 1)))
+ (new-monitor (if (zp new-mcount)
+ 0
+ th))
+ (new-obj-fields
+ (bind "monitor" new-monitor
+ (bind "mcount" new-mcount obj-fields)))
+ (new-object (bind "java.lang.Object" new-obj-fields instance)))
+ (bind obj-ref-num new-object heap)))
+
+; objectLockable? is used to determine if th can unlock instance. This
+; occurs when either mcount is zero (nobody has a lock), or mcount is
+; greater than zero, but monitor is equal to th. This means that th
+; already has a lock on the object, and when the object is locked yet again,
+; monitor will remain the same, but mcount will be incremented.
+;
+; objectUnLockable? determins if a thread can unlock an object (ie if it
+; has a lock on that object)
+(defun objectLockable? (instance th)
+ (let* ((obj-fields (binding "java.lang.Object" instance))
+ (monitor (binding "monitor" obj-fields))
+ (mcount (binding "mcount" obj-fields)))
+ (or (zp mcount)
+ (equal monitor th))))
+
+(defun objectUnLockable? (instance th)
+ (let* ((obj-fields (binding "java.lang.Object" instance))
+ (monitor (binding "monitor" obj-fields)))
+ (equal monitor th)))
+
+; -----------------------------------------------------------------------------
+; Frames
+
+(defun make-frame (pc locals stack program sync-flg cur-class)
+ (list pc locals stack program sync-flg cur-class))
+
+(defun top-frame (th s) (top (call-stack th s)))
+
+(defun pc (frame) (nth 0 frame))
+(defun locals (frame) (nth 1 frame))
+(defun stack (frame) (nth 2 frame))
+(defun program (frame) (nth 3 frame))
+(defun sync-flg (frame) (nth 4 frame))
+(defun cur-class (frame) (nth 5 frame))
+
+; -----------------------------------------------------------------------------
+; Method Declarations
+
+; The methods component of a class declaration is a list of method definitions.
+; A method definition is a list of the form
+
+; (name formals sync-status . program)
+
+; We never build these declarations but just enter list constants for them,
+
+; Note the similarity to our old notion of a program definition. We
+; will use strings to name methods now.
+
+; sync-status is 't' if the method is synchronized, 'nil' if not
+
+; Method definitions will be constructed by expressions such as:
+; (Note: all of the symbols below are understood to be in the pkg "JVM".)
+
+; ("move" (dx dy) nil
+; (load this)
+; (load this)
+; (getfield "Point" "x")
+; (load dx)
+; (add)
+; (putfield "Point" "x") ; this.x = this.x + dx;
+; (load :this)
+; (load :this)
+; (getfield "Point" "y")
+; (load dy)
+; (add)
+; (putfield "Point" "y") ; this.y = this.y + dy;
+; (push 1)
+; (xreturn))) ; return 1;
+
+; Provided this method is defined in the class "Point" it can be invoked by
+
+; (invokevirtual "Point" "move" 2)
+
+; This assumes that the stack, at the time of invocation, contains an
+; reference to an object of type "Point" and two numbers, dx and dy.
+
+; If a method declaration has an empty list for the program (ie- there are
+; no bytecodes associated with the method), then the method is considered
+; native. Native methods are normally written in something like C or
+; assembly language. The JVM would normally ensure that the correct number
+; and type of arguments are passed to the native method, and would then hand
+; over control to C. In our model, we simply "hardwire" invokevirtual to
+; to handle these methods.
+; * Note that a method in Java will never have 0 bytecodes, since even if
+; it has no body, it will consist of at least the (xreturn) bytecode.
+
+; The accessors for methods are:
+
+(defun method-name (m)
+ (nth 0 m))
+(defun method-formals (m)
+ (nth 1 m))
+(defun method-sync (m)
+ (nth 2 m))
+(defun method-program (m)
+ (cdddr m))
+(defun method-isNative? (m)
+ (equal '(NIL)
+ (method-program m)))
+
+; The Standard Modify
+
+(defun suppliedp (key args)
+ (cond ((endp args) nil)
+ ((equal key (car args)) t)
+ (t (suppliedp key (cdr args)))))
+
+(defun actual (key args)
+ (cond ((endp args) nil)
+ ((equal key (car args)) (cadr args))
+ (t (actual key (cdr args)))))
+
+(defmacro modify (th s &rest args)
+ (list 'make-state
+ (cond
+ ((or (suppliedp :call-stack args)
+ (suppliedp :pc args)
+ (suppliedp :locals args)
+ (suppliedp :stack args)
+ (suppliedp :program args)
+ (suppliedp :sync-flg args)
+ (suppliedp :cur-class args)
+ (suppliedp :status args))
+ (list 'bind
+ th
+ (list 'make-thread
+ (cond
+ ((suppliedp :call-stack args)
+ (actual :call-stack args))
+ ((and (suppliedp :status args)
+ (null (cddr args)))
+ (list 'call-stack th s))
+ (t
+ (list 'push
+ (list 'make-frame
+ (if (suppliedp :pc args)
+ (actual :pc args)
+ (list 'pc (list 'top-frame th s)))
+ (if (suppliedp :locals args)
+ (actual :locals args)
+ (list 'locals (list 'top-frame th s)))
+ (if (suppliedp :stack args)
+ (actual :stack args)
+ (list 'stack (list 'top-frame th s)))
+ (if (suppliedp :program args)
+ (actual :program args)
+ (list 'program (list 'top-frame th s)))
+ (if (suppliedp :sync-flg args)
+ (actual :sync-flg args)
+ (list 'sync-flg (list 'top-frame th s)))
+ (if (suppliedp :cur-class args)
+ (actual :cur-class args)
+ (list 'cur-class
+ (list 'top-frame th s))))
+ (list 'pop (list 'call-stack th s)))))
+ (if (suppliedp :status args)
+ (actual :status args)
+ (list 'status th s))
+ (list 'rref th s))
+ (list 'thread-table s)))
+ ((suppliedp :thread-table args)
+ (actual :thread-table args))
+ (t (list 'thread-table s)))
+ (if (suppliedp :heap args)
+ (actual :heap args)
+ (list 'heap s))
+ (if (suppliedp :class-table args)
+ (actual :class-table args)
+ (list 'class-table s))))
+
+; -----------------------------------------------------------------------------
+; Helper functions related to building instances of objects
+
+(defun deref (ref heap)
+ (binding (cadr ref) heap))
+
+(defun field-value (class-name field-name instance)
+ (binding field-name
+ (binding class-name instance)))
+
+(defun build-class-field-bindings (field-names)
+ (if (endp field-names)
+ nil
+ (cons (cons (car field-names) 0)
+ (build-class-field-bindings (cdr field-names)))))
+
+(defun build-class-object-field-bindings ()
+ '(("monitor" . 0) ("monitor-count" . 0) ("wait-set" . nil)))
+
+(defun build-immediate-instance-data (class-name class-table)
+ (cons class-name
+ (build-class-field-bindings
+ (class-decl-fields
+ (bound? class-name class-table)))))
+
+(defun build-an-instance (class-names class-table)
+ (if (endp class-names)
+ nil
+ (cons (build-immediate-instance-data (car class-names) class-table)
+ (build-an-instance (cdr class-names) class-table))))
+
+(defun build-class-data (sfields)
+ (cons "java.lang.Class"
+ (build-class-field-bindings
+ (cons "<name>" sfields))))
+
+(defun build-a-class-instance (sfields class-table)
+ (list (build-class-data sfields)
+ (build-immediate-instance-data "java.lang.Object" class-table)))
+
+
+; -----------------------------------------------------------------------------
+; Arrays
+
+(defun value-of (obj)
+ (cdr obj))
+
+(defun superclasses-of (class ct)
+ (class-decl-superclasses (bound? class ct)))
+
+(defun array-content (array)
+ (value-of (field-value "ARRAY" "<array>" array)))
+
+(defun array-type (array)
+ (nth 0 (array-content array)))
+
+(defun array-bound (array)
+ (nth 1 (array-content array)))
+
+(defun array-data (array)
+ (nth 2 (array-content array)))
+
+(defun element-at (index array)
+ (nth index (array-data array)))
+
+(defun makearray (type bound data class-table)
+ (cons (list "ARRAY"
+ (cons "<array>" (cons '*array* (list type bound data))))
+ (build-an-instance
+ (superclasses-of "ARRAY" class-table)
+ class-table)))
+
+(defun set-element-at (value index array class-table)
+ (makearray (array-type array)
+ (array-bound array)
+ (update-nth index value (array-data array))
+ class-table))
+
+(defun primitive-type (type)
+ (cond ((equal type 'T_BYTE) t)
+ ((equal type 'T_SHORT) t)
+ ((equal type 'T_INT) t)
+ ((equal type 'T_LONG) t)
+ ((equal type 'T_FLOAT) t)
+ ((equal type 'T_DOUBLE) t)
+ ((equal type 'T_CHAR) t)
+ ((equal type 'T_BOOLEAN) t)
+ (t nil)))
+
+(defun atype-to-identifier (atype-num)
+ (cond ((equal atype-num 4) 'T_BOOLEAN)
+ ((equal atype-num 5) 'T_CHAR)
+ ((equal atype-num 6) 'T_FLOAT)
+ ((equal atype-num 7) 'T_DOUBLE)
+ ((equal atype-num 8) 'T_BYTE)
+ ((equal atype-num 9) 'T_SHORT)
+ ((equal atype-num 10) 'T_INT)
+ ((equal atype-num 11) 'T_LONG)
+ (t nil)))
+
+(defun identifier-to-atype (ident)
+ (cond ((equal ident 'T_BOOLEAN) 4)
+ ((equal ident 'T_CHAR) 5)
+ ((equal ident 'T_FLOAT) 6)
+ ((equal ident 'T_DOUBLE) 7)
+ ((equal ident 'T_BYTE) 8)
+ ((equal ident 'T_SHORT) 9)
+ ((equal ident 'T_INT) 10)
+ ((equal ident 'T_LONG) 11)
+ (t nil)))
+
+(defun default-value1 (type)
+ (if (primitive-type type)
+ 0
+ nil))
+
+(defun init-array (type count)
+ (if (zp count)
+ nil
+ (cons (default-value1 type) (init-array type (- count 1)))))
+
+; The following measure is due to J
+(defun natural-sum (lst)
+ (cond ((endp lst) 0)
+ (t (+ (nfix (car lst)) (natural-sum (cdr lst))))))
+
+(mutual-recursion
+
+ ; makemultiarray2 :: num, counts, s, ac --> [refs]
+ (defun makemultiarray2 (car-counts cdr-counts s ac)
+ (declare (xargs :measure (cons (len (cons car-counts cdr-counts))
+ (natural-sum (cons car-counts cdr-counts)))))
+ (if (zp car-counts)
+ (mv (heap s) ac)
+ (mv-let (new-addr new-heap)
+ (makemultiarray cdr-counts s)
+ (makemultiarray2 (- car-counts 1)
+ cdr-counts
+ (make-state (thread-table s)
+ new-heap
+ (class-table s))
+ (cons (list 'REF new-addr) ac)))))
+
+ ; makemultiarray :: [counts], s --> addr, new-heap
+ (defun makemultiarray (counts s)
+ (declare (xargs :measure (cons (+ 1 (len counts))
+ (natural-sum counts))))
+ (if (<= (len counts) 1)
+
+ ; "Base case" Handles initializing the final dimension
+ (mv (len (heap s))
+ (bind (len (heap s))
+ (makearray 'T_REF
+ (car counts)
+ (init-array 'T_REF (car counts))
+ (class-table s))
+ (heap s)))
+
+ ; "Recursive Case"
+ (mv-let (heap-prime lst-of-refs)
+ (makemultiarray2 (car counts)
+ (cdr counts)
+ s
+ nil)
+ (let* ((obj (makearray 'T_REF
+ (car counts)
+ lst-of-refs
+ (class-table s)))
+ (new-addr (len heap-prime))
+ (new-heap (bind new-addr obj heap-prime)))
+ (mv new-addr new-heap)))))
+)
+
+; -----------------------------------------------------------------------------
+; Instruction length table -- PCs are now in bytes, not # of instructions
+
+(defun inst-length (inst)
+ (case (op-code inst)
+ (AALOAD 1)
+ (AASTORE 1)
+ (ACONST_NULL 1)
+ (ALOAD 2)
+ (ALOAD_0 1)
+ (ALOAD_1 1)
+ (ALOAD_2 1)
+ (ALOAD_3 1)
+ (ANEWARRAY 3)
+ (ARETURN 1)
+ (ARRAYLENGTH 1)
+ (ASTORE 2)
+ (ASTORE_0 1)
+ (ASTORE_1 1)
+ (ASTORE_2 1)
+ (ASTORE_3 1)
+ (BALOAD 1)
+ (BASTORE 1)
+ (BIPUSH 2)
+ (CALOAD 1)
+ (CASTORE 1)
+ (DUP 1)
+ (DUP_X1 1)
+ (DUP_X2 1)
+ (DUP2 1)
+ (DUP2_X1 1)
+ (DUP2_X2 1)
+ (GETFIELD 3)
+ (GETSTATIC 3)
+ (GOTO 3)
+ (GOTO_W 5)
+ (I2B 1)
+ (I2C 1)
+ (I2L 1)
+ (I2S 1)
+ (IADD 1)
+ (IALOAD 1)
+ (IAND 1)
+ (IASTORE 1)
+ (ICONST_M1 1)
+ (ICONST_0 1)
+ (ICONST_1 1)
+ (ICONST_2 1)
+ (ICONST_3 1)
+ (ICONST_4 1)
+ (ICONST_5 1)
+ (IDIV 1)
+ (IF_ACMPEQ 3)
+ (IF_ACMPNE 3)
+ (IF_ICMPEQ 3)
+ (IF_ICMPGE 3)
+ (IF_ICMPGT 3)
+ (IF_ICMPLE 3)
+ (IF_ICMPLT 3)
+ (IF_ICMPNE 3)
+ (IFEQ 3)
+ (IFGE 3)
+ (IFGT 3)
+ (IFLE 3)
+ (IFLT 3)
+ (IFNE 3)
+ (IFNONNULL 3)
+ (IFNULL 3)
+ (IINC 3)
+ (ILOAD 2)
+ (ILOAD_0 1)
+ (ILOAD_1 1)
+ (ILOAD_2 1)
+ (ILOAD_3 1)
+ (IMUL 1)
+ (INEG 1)
+ (INSTANCEOF 3)
+ (INVOKESPECIAL 3)
+ (INVOKESTATIC 3)
+ (INVOKEVIRTUAL 3)
+ (IOR 1)
+ (IREM 1)
+ (IRETURN 1)
+ (ISHL 1)
+ (ISHR 1)
+ (ISTORE 2)
+ (ISTORE_0 1)
+ (ISTORE_1 1)
+ (ISTORE_2 1)
+ (ISTORE_3 1)
+ (ISUB 1)
+ (IUSHR 1)
+ (IXOR 1)
+ (JSR 3)
+ (JSR_W 5)
+ (L2I 1)
+ (LADD 1)
+ (LALOAD 1)
+ (LAND 1)
+ (LASTORE 1)
+ (LCMP 1)
+ (LCONST_0 1)
+ (LCONST_1 1)
+ (LDC 2)
+ (LDC_W 3)
+ (LDC2_W 3)
+ (LDIV 1)
+ (LLOAD 2)
+ (LLOAD_0 1)
+ (LLOAD_1 1)
+ (LLOAD_2 1)
+ (LLOAD_3 1)
+ (LMUL 1)
+ (LNEG 1)
+ (LOR 1)
+ (LREM 1)
+ (LRETURN 1)
+ (LSHL 1)
+ (LSHR 1)
+ (LSTORE 2)
+ (LSTORE_0 1)
+ (LSTORE_1 1)
+ (LSTORE_2 1)
+ (LSTORE_3 1)
+ (LSUB 1)
+ (LUSHR 1)
+ (LXOR 1)
+ (MONITORENTER 1)
+ (MONITOREXIT 1)
+ (MULTIANEWARRAY 4)
+ (NEW 3)
+ (NEWARRAY 2)
+ (NOP 1)
+ (POP 1)
+ (POP2 1)
+ (PUTFIELD 3)
+ (PUTSTATIC 3)
+ (RET 2)
+ (RETURN 1)
+ (SALOAD 1)
+ (SASTORE 1)
+ (SIPUSH 3)
+ (SWAP 1)
+ (t 1)))
+
+
+; =============================================================================
+; JVM INSTRUCTIONS BEGIN HERE
+; =============================================================================
+
+; -----------------------------------------------------------------------------
+; (AALOAD) Instruction
+
+(defun execute-AALOAD (inst th s)
+ (let* ((index (top (stack (top-frame th s))))
+ (arrayref (top (pop (stack (top-frame th s)))))
+ (array (deref arrayref (heap s))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (element-at index array)
+ (pop (pop (stack (top-frame th s))))))))
+
+; -----------------------------------------------------------------------------
+; (AASTORE) Instruction
+
+(defun execute-AASTORE (inst th s)
+ (let* ((value (top (stack (top-frame th s))))
+ (index (top (pop (stack (top-frame th s)))))
+ (arrayref (top (pop (pop (stack (top-frame th s)))))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (pop (pop (pop (stack (top-frame th s)))))
+ :heap (bind (cadr arrayref)
+ (set-element-at value
+ index
+ (deref arrayref (heap s))
+ (class-table s))
+ (heap s)))))
+
+; -----------------------------------------------------------------------------
+; (ACONST_NULL) Instruction
+
+(defun execute-ACONST_NULL (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push '(REF -1)
+ (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (ALOAD idx) Instruction - load a reference from the locals
+
+(defun execute-ALOAD (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (nth (arg1 inst)
+ (locals (top-frame th s)))
+ (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (ALOAD_X) Instruction - load a reference from the locals
+; covers ALOAD_{0, 1, 2, 3}
+
+(defun execute-ALOAD_X (inst th s n)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (nth n (locals (top-frame th s)))
+ (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (ANEWARRAY) Instruction
+
+(defun execute-ANEWARRAY (inst th s)
+ (let* ((type 'T_REF)
+ (count (top (stack (top-frame th s))))
+ (addr (len (heap s)))
+ (obj (makearray type
+ count
+ (init-array type count)
+ (class-table s))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (list 'REF addr)
+ (pop (stack (top-frame th s))))
+ :heap (bind addr
+ obj
+ (heap s)))))
+
+; -----------------------------------------------------------------------------
+; (ARETURN) Instruction - return a reference to the preceeding frame
+
+(defun execute-ARETURN (inst th s)
+ (declare (ignore inst))
+ (let* ((val (top (stack (top-frame th s))))
+ (obj-ref (nth 0 (locals (top-frame th s))))
+ (sync-status (sync-flg (top-frame th s)))
+ (class (cur-class (top-frame th s)))
+ (ret-ref (class-decl-heapref (bound? class (class-table s))))
+ (new-heap (cond ((equal sync-status 'LOCKED)
+ (unlock-object th obj-ref (heap s)))
+ ((equal sync-status 'S_LOCKED)
+ (unlock-object th ret-ref (heap s)))
+ (t (heap s))))
+ (s1 (modify th s
+ :call-stack (pop (call-stack th s))
+ :heap new-heap)))
+ (modify th s1
+ :stack (push val (stack (top-frame th s1))))))
+
+; -----------------------------------------------------------------------------
+; (ARRAYLENGTH) Instruction
+
+(defun execute-ARRAYLENGTH (inst th s)
+ (let* ((arrayref (top (stack (top-frame th s))))
+ (array (deref arrayref (heap s))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (array-bound array)
+ (pop (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (ASTORE idx) Instruction - store a reference into the locals
+
+(defun execute-ASTORE (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :locals (update-nth (arg1 inst)
+ (top (stack (top-frame th s)))
+ (locals (top-frame th s)))
+ :stack (pop (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (ASTORE_X) Instruction - store a reference into the locals
+; covers ASTORE_{0, 1, 2, 3}
+
+(defun execute-ASTORE_X (inst th s n)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :locals (update-nth n
+ (top (stack (top-frame th s)))
+ (locals (top-frame th s)))
+ :stack (pop (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (BALOAD) Instruction
+
+(defun execute-BALOAD (inst th s)
+ (let* ((index (top (stack (top-frame th s))))
+ (arrayref (top (pop (stack (top-frame th s)))))
+ (array (deref arrayref (heap s)))
+ (element (if (equal (array-type array)
+ 'T_BOOLEAN)
+ (ubyte-fix (element-at index array))
+ (byte-fix (element-at index array)))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push element
+ (pop (pop (stack (top-frame th s))))))))
+
+; -----------------------------------------------------------------------------
+; (BASTORE) Instruction
+
+(defun execute-BASTORE (inst th s)
+ (let* ((value (top (stack (top-frame th s))))
+ (index (top (pop (stack (top-frame th s)))))
+ (arrayref (top (pop (pop (stack (top-frame th s))))))
+ (element (if (equal (array-type (deref arrayref (heap s)))
+ 'T_BYTE)
+ (byte-fix value)
+ (u-fix value 1))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (pop (pop (pop (stack (top-frame th s)))))
+ :heap (bind (cadr arrayref)
+ (set-element-at element
+ index
+ (deref arrayref (heap s))
+ (class-table s))
+ (heap s)))))
+
+; -----------------------------------------------------------------------------
+; (BIPUSH const) Instruction
+
+(defun execute-BIPUSH (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (byte-fix (arg1 inst))
+ (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (CALOAD) Instruction
+
+(defun execute-CALOAD (inst th s)
+ (let* ((index (top (stack (top-frame th s))))
+ (arrayref (top (pop (stack (top-frame th s)))))
+ (array (deref arrayref (heap s))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (char-fix (element-at index array))
+ (pop (pop (stack (top-frame th s))))))))
+
+; -----------------------------------------------------------------------------
+; (CASTORE) Instruction
+
+(defun execute-CASTORE (inst th s)
+ (let* ((value (top (stack (top-frame th s))))
+ (index (top (pop (stack (top-frame th s)))))
+ (arrayref (top (pop (pop (stack (top-frame th s)))))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (pop (pop (pop (stack (top-frame th s)))))
+ :heap (bind (cadr arrayref)
+ (set-element-at (char-fix value)
+ index
+ (deref arrayref (heap s))
+ (class-table s))
+ (heap s)))))
+
+; -----------------------------------------------------------------------------
+; (DUP) Instruction
+
+(defun execute-DUP (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (top (stack (top-frame th s)))
+ (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (DUP_X1) Instruction
+
+(defun execute-DUP_X1 (inst th s)
+ (let* ((val1 (top (stack (top-frame th s))))
+ (val2 (top (pop (stack (top-frame th s)))))
+ (stack_prime (pop (pop (stack (top-frame th s))))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push val1 (push val2 (push val1 stack_prime))))))
+
+; -----------------------------------------------------------------------------
+; (DUP_X2) Instruction
+
+(defun execute-DUP_X2 (inst th s)
+ (let* ((val1 (top (stack (top-frame th s))))
+ (val2 (top (pop (stack (top-frame th s)))))
+ (val3 (top (popn 2 (stack (top-frame th s)))))
+ (stack_prime (popn 3 (stack (top-frame th s)))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push val1
+ (push val2
+ (push val3
+ (push val1 stack_prime)))))))
+
+; -----------------------------------------------------------------------------
+; (DUP2) Instruction
+
+(defun execute-DUP2 (inst th s)
+ (let* ((val1 (top (stack (top-frame th s))))
+ (val2 (top (pop (stack (top-frame th s)))))
+ (stack_prime (pop (pop (stack (top-frame th s))))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push val1
+ (push val2
+ (push val1
+ (push val2 stack_prime)))))))
+
+; -----------------------------------------------------------------------------
+; (DUP2_X1) Instruction
+
+(defun execute-DUP2_X1 (inst th s)
+ (let* ((val1 (top (stack (top-frame th s))))
+ (val2 (top (pop (stack (top-frame th s)))))
+ (val3 (top (popn 2 (stack (top-frame th s)))))
+ (stack_prime (popn 3 (stack (top-frame th s)))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push val1
+ (push val2
+ (push val3
+ (push val1
+ (push val2 stack_prime))))))))
+
+; -----------------------------------------------------------------------------
+; (DUP2_X2) Instruction
+
+(defun execute-DUP2_X2 (inst th s)
+ (let* ((val1 (top (stack (top-frame th s))))
+ (val2 (top (pop (stack (top-frame th s)))))
+ (val3 (top (popn 2 (stack (top-frame th s)))))
+ (val4 (top (popn 3 (stack (top-frame th s)))))
+ (stack_prime (popn 4 (stack (top-frame th s)))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push val1
+ (push val2
+ (push val3
+ (push val4
+ (push val1
+ (push val2 stack_prime)))))))))
+
+; -----------------------------------------------------------------------------
+; (GETFIELD "class" "field" ?long-flag?) Instruction
+
+(defun execute-GETFIELD (inst th s)
+ (let* ((class-name (arg1 inst))
+ (field-name (arg2 inst))
+ (long-flag (arg3 inst))
+ (instance (deref (top (stack (top-frame th s))) (heap s)))
+ (field-value (field-value class-name field-name instance)))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (if long-flag
+ (push 0 (push field-value
+ (pop (stack (top-frame th s)))))
+ (push field-value
+ (pop (stack (top-frame th s))))))))
+
+; -----------------------------------------------------------------------------
+; (GETSTATIC "class" "field" ?long-flag?) Instruction
+
+(defun static-field-value (class-name field-name s)
+ (let* ((class-ref (class-decl-heapref
+ (bound? class-name (class-table s))))
+ (instance (deref class-ref (heap s))))
+ (field-value "java.lang.Class" field-name instance)))
+
+(defun execute-GETSTATIC (inst th s)
+ (let* ((class-name (arg1 inst))
+ (field-name (arg2 inst))
+ (long-flag (arg3 inst))
+ (class-ref (class-decl-heapref
+ (bound? class-name (class-table s))))
+ (instance (deref class-ref (heap s)))
+ (field-value (field-value "java.lang.Class" field-name instance)))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (if long-flag
+ (push 0 (push field-value (stack (top-frame th s))))
+ (push field-value (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (GOTO pc) Instruction
+
+(defun execute-GOTO (inst th s)
+ (modify th s
+ :pc (+ (arg1 inst) (pc (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (GOTO_W pc) Instruction
+
+(defun execute-GOTO_W (inst th s)
+ (modify th s
+ :pc (+ (arg1 inst) (pc (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (I2B) Instruction - int to byte narrowing conversion
+
+(defun execute-I2B (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (byte-fix (top (stack (top-frame th s))))
+ (pop (stack (top-frame th s))))))
+
+; -----------------------------------------------------------------------------
+; (I2C) Instruction - int to char narrowing conversion
+
+(defun execute-I2C (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (char-fix (top (stack (top-frame th s))))
+ (pop (stack (top-frame th s))))))
+
+; -----------------------------------------------------------------------------
+; (I2L) Instruction - int to long conversion
+
+(defun execute-I2L (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push 0
+ (push (long-fix (top (stack (top-frame th s))))
+ (pop (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (I2S) Instruction - int to short narrowing conversion
+
+(defun execute-I2S (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (short-fix (top (stack (top-frame th s))))
+ (pop (stack (top-frame th s))))))
+
+; -----------------------------------------------------------------------------
+; (IADD) Instruction
+
+(defun execute-IADD (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (int-fix
+ (+ (top (pop (stack (top-frame th s))))
+ (top (stack (top-frame th s)))))
+ (pop (pop (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (IALOAD) Instruction
+
+(defun execute-IALOAD (inst th s)
+ (let* ((index (top (stack (top-frame th s))))
+ (arrayref (top (pop (stack (top-frame th s)))))
+ (array (deref arrayref (heap s))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (element-at index array)
+ (pop (pop (stack (top-frame th s))))))))
+
+; -----------------------------------------------------------------------------
+; (IAND) Instruction
+
+(defun execute-IAND (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (logand (top (pop (stack (top-frame th s))))
+ (top (stack (top-frame th s))))
+ (pop (pop (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (IASTORE) Instruction
+
+(defun execute-IASTORE (inst th s)
+ (let* ((value (top (stack (top-frame th s))))
+ (index (top (pop (stack (top-frame th s)))))
+ (arrayref (top (pop (pop (stack (top-frame th s)))))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (pop (pop (pop (stack (top-frame th s)))))
+ :heap (bind (cadr arrayref)
+ (set-element-at value
+ index
+ (deref arrayref (heap s))
+ (class-table s))
+ (heap s)))))
+
+; -----------------------------------------------------------------------------
+; (ICONST_X) Instruction - push a certain constant onto the stack
+; covers ICONST_{M1, 0, 1, 2, 3, 4, 5}
+
+(defun execute-ICONST_X (inst th s n)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push n (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (IDIV) Instruction
+
+(defun execute-IDIV (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (int-fix
+ (truncate (top (pop (stack (top-frame th s))))
+ (top (stack (top-frame th s)))))
+ (pop (pop (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (IF_ACMPEQ pc) Instruction
+
+(defun execute-IF_ACMPEQ (inst th s)
+ (modify th s
+ :pc (if (equal (top (pop (stack (top-frame th s))))
+ (top (stack (top-frame th s))))
+ (+ (arg1 inst) (pc (top-frame th s)))
+ (+ (inst-length inst) (pc (top-frame th s))))
+ :stack (pop (pop (stack (top-frame th s))))))
+
+; -----------------------------------------------------------------------------
+; (IF_ACMPNE pc) Instruction
+
+(defun execute-IF_ACMPNE (inst th s)
+ (modify th s
+ :pc (if (equal (top (pop (stack (top-frame th s))))
+ (top (stack (top-frame th s))))
+ (+ (inst-length inst) (pc (top-frame th s)))
+ (+ (arg1 inst) (pc (top-frame th s))))
+ :stack (pop (pop (stack (top-frame th s))))))
+
+; -----------------------------------------------------------------------------
+; (IF_ICMPEQ pc) Instruction
+
+(defun execute-IF_ICMPEQ (inst th s)
+ (modify th s
+ :pc (if (equal (top (pop (stack (top-frame th s))))
+ (top (stack (top-frame th s))))
+ (+ (arg1 inst) (pc (top-frame th s)))
+ (+ (inst-length inst) (pc (top-frame th s))))
+ :stack (pop (pop (stack (top-frame th s))))))
+
+; -----------------------------------------------------------------------------
+; (IF_ICMPGE pc) Instruction
+
+(defun execute-IF_ICMPGE (inst th s)
+ (modify th s
+ :pc (if (>= (top (pop (stack (top-frame th s))))
+ (top (stack (top-frame th s))))
+ (+ (arg1 inst) (pc (top-frame th s)))
+ (+ (inst-length inst) (pc (top-frame th s))))
+ :stack (pop (pop (stack (top-frame th s))))))
+
+; -----------------------------------------------------------------------------
+; (IF_ICMPGT pc) Instruction
+
+(defun execute-IF_ICMPGT (inst th s)
+ (modify th s
+ :pc (if (> (top (pop (stack (top-frame th s))))
+ (top (stack (top-frame th s))))
+ (+ (arg1 inst) (pc (top-frame th s)))
+ (+ (inst-length inst) (pc (top-frame th s))))
+ :stack (pop (pop (stack (top-frame th s))))))
+
+; -----------------------------------------------------------------------------
+; (IF_ICMPLT pc) Instruction
+
+(defun execute-IF_ICMPLT (inst th s)
+ (modify th s
+ :pc (if (< (top (pop (stack (top-frame th s))))
+ (top (stack (top-frame th s))))
+ (+ (arg1 inst) (pc (top-frame th s)))
+ (+ (inst-length inst) (pc (top-frame th s))))
+ :stack (pop (pop (stack (top-frame th s))))))
+
+; -----------------------------------------------------------------------------
+; (IF_ICMPLE pc) Instruction
+
+(defun execute-IF_ICMPLE (inst th s)
+ (modify th s
+ :pc (if (<= (top (pop (stack (top-frame th s))))
+ (top (stack (top-frame th s))))
+ (+ (arg1 inst) (pc (top-frame th s)))
+ (+ (inst-length inst) (pc (top-frame th s))))
+ :stack (pop (pop (stack (top-frame th s))))))
+
+; -----------------------------------------------------------------------------
+; (IF_ICMPNE pc) Instruction
+
+(defun execute-IF_ICMPNE (inst th s)
+ (modify th s
+ :pc (if (equal (top (pop (stack (top-frame th s))))
+ (top (stack (top-frame th s))))
+ (+ (inst-length inst) (pc (top-frame th s)))
+ (+ (arg1 inst) (pc (top-frame th s))))
+ :stack (pop (pop (stack (top-frame th s))))))
+
+; -----------------------------------------------------------------------------
+; (IFEQ pc) Instruction
+
+(defun execute-IFEQ (inst th s)
+ (modify th s
+ :pc (if (equal (top (stack (top-frame th s))) 0)
+ (+ (arg1 inst) (pc (top-frame th s)))
+ (+ (inst-length inst) (pc (top-frame th s))))
+ :stack (pop (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (IFGE pc) Instruction
+
+(defun execute-IFGE (inst th s)
+ (modify th s
+ :pc (if (>= (top (stack (top-frame th s))) 0)
+ (+ (arg1 inst) (pc (top-frame th s)))
+ (+ (inst-length inst) (pc (top-frame th s))))
+ :stack (pop (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (IFGT pc) Instruction
+
+(defun execute-IFGT (inst th s)
+ (modify th s
+ :pc (if (> (top (stack (top-frame th s))) 0)
+ (+ (arg1 inst) (pc (top-frame th s)))
+ (+ (inst-length inst) (pc (top-frame th s))))
+ :stack (pop (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (IFLE pc) Instruction
+
+(defun execute-IFLE (inst th s)
+ (modify th s
+ :pc (if (<= (top (stack (top-frame th s))) 0)
+ (+ (arg1 inst) (pc (top-frame th s)))
+ (+ (inst-length inst) (pc (top-frame th s))))
+ :stack (pop (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (IFLT pc) Instruction
+
+(defun execute-IFLT (inst th s)
+ (modify th s
+ :pc (if (< (top (stack (top-frame th s))) 0)
+ (+ (arg1 inst) (pc (top-frame th s)))
+ (+ (inst-length inst) (pc (top-frame th s))))
+ :stack (pop (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (IFNE pc) Instruction
+
+(defun execute-IFNE (inst th s)
+ (modify th s
+ :pc (if (equal (top (stack (top-frame th s))) 0)
+ (+ (inst-length inst) (pc (top-frame th s)))
+ (+ (arg1 inst) (pc (top-frame th s))))
+ :stack (pop (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (IFNONNULL pc) Instruction
+
+(defun execute-IFNONNULL (inst th s)
+ (modify th s
+ :pc (if (equal (top (stack (top-frame th s))) '(REF -1))
+ (+ (inst-length inst) (pc (top-frame th s)))
+ (+ (arg1 inst) (pc (top-frame th s))))
+ :stack (pop (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (IFNULL pc) Instruction
+
+(defun execute-IFNULL (inst th s)
+ (modify th s
+ :pc (if (equal (top (stack (top-frame th s))) '(REF -1))
+ (+ (arg1 inst) (pc (top-frame th s)))
+ (+ (inst-length inst) (pc (top-frame th s))))
+ :stack (pop (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (IINC idx const) Instruction - Increment local variable by a constant
+
+(defun execute-IINC (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :locals (update-nth (arg1 inst)
+ (int-fix
+ (+ (arg2 inst)
+ (nth (arg1 inst)
+ (locals (top-frame th s)))))
+ (locals (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (ILOAD idx) Instruction - Push a local onto the stack
+
+(defun execute-ILOAD (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (nth (arg1 inst)
+ (locals (top-frame th s)))
+ (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (ILOAD_X) Instruction - Push a local onto the stack
+; covers ILOAD_{0, 1, 2, 3}
+
+(defun execute-ILOAD_X (inst th s n)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (nth n (locals (top-frame th s)))
+ (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (IMUL) Instruction
+
+(defun execute-IMUL (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (int-fix
+ (* (top (pop (stack (top-frame th s))))
+ (top (stack (top-frame th s)))))
+ (pop (pop (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (INEG) Instruction
+; Because of the way the JVM represents 2's complement ints,
+; the negation of the most negative int is itself
+
+(defun execute-INEG (inst th s)
+ (let* ((result (if (equal (top (stack (top-frame th s)))
+ *most-negative-integer*)
+ *most-negative-integer*
+ (- (top (stack (top-frame th s)))))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push result (pop (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (INSTANCEOF) Instruction
+
+(defun execute-INSTANCEOF (inst th s)
+ (let* ((ref (top (stack (top-frame th s))))
+ (obj (deref ref (heap s)))
+ (obj-class (caar obj))
+ (obj-supers (cons obj-class (class-decl-superclasses
+ (bound? obj-class (class-table s)))))
+ (value (if (nullrefp ref)
+ 0
+ (if (member-equal (arg1 inst) obj-supers)
+ 1
+ 0))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push value (pop (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (IOR) Instruction
+
+(defun execute-IOR (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (logior (top (pop (stack (top-frame th s))))
+ (top (stack (top-frame th s))))
+ (pop (pop (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (IREM) Instruction
+
+(defun execute-IREM (inst th s)
+ (let* ((val1 (top (pop (stack (top-frame th s)))))
+ (val2 (top (stack (top-frame th s))))
+ (result (- val1 (* (truncate val1 val2) val2))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push result
+ (pop (pop (stack (top-frame th s))))))))
+
+; -----------------------------------------------------------------------------
+; (IRETURN) Instruction - return an int
+
+(defun execute-IRETURN (inst th s)
+ (declare (ignore inst))
+ (let* ((val (top (stack (top-frame th s))))
+ (obj-ref (nth 0 (locals (top-frame th s))))
+ (sync-status (sync-flg (top-frame th s)))
+ (class (cur-class (top-frame th s)))
+ (ret-ref (class-decl-heapref (bound? class (class-table s))))
+ (new-heap (cond ((equal sync-status 'LOCKED)
+ (unlock-object th obj-ref (heap s)))
+ ((equal sync-status 'S_LOCKED)
+ (unlock-object th ret-ref (heap s)))
+ (t (heap s))))
+ (s1 (modify th s
+ :call-stack (pop (call-stack th s))
+ :heap new-heap)))
+ (modify th s1
+ :stack (push val (stack (top-frame th s1))))))
+
+; -----------------------------------------------------------------------------
+; (ISHL) Instruction
+
+(defun execute-ISHL (inst th s)
+ (let* ((val1 (top (pop (stack (top-frame th s)))))
+ (val2 (top (stack (top-frame th s))))
+ (shiftval (5-bit-fix val2))
+ (result (shl val1 shiftval)))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (int-fix result)
+ (pop (pop (stack (top-frame th s))))))))
+
+; -----------------------------------------------------------------------------
+; (ISHR) Instruction
+
+(defun execute-ISHR (inst th s)
+ (let* ((val1 (top (pop (stack (top-frame th s)))))
+ (val2 (top (stack (top-frame th s))))
+ (shiftval (5-bit-fix val2))
+ (result (shr val1 shiftval)))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (int-fix result)
+ (pop (pop (stack (top-frame th s))))))))
+
+; -----------------------------------------------------------------------------
+; (ISTORE idx) Instruction - store an int into the locals
+
+(defun execute-ISTORE (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :locals (update-nth (arg1 inst)
+ (top (stack (top-frame th s)))
+ (locals (top-frame th s)))
+ :stack (pop (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (ISTORE_X) Instruction - store an int into the locals
+; covers ISTORE_{0, 1, 2, 3}
+
+(defun execute-ISTORE_X (inst th s n)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :locals (update-nth n
+ (top (stack (top-frame th s)))
+ (locals (top-frame th s)))
+ :stack (pop (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (ISUB) Instruction
+
+(defun execute-ISUB (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (int-fix (- (top (pop (stack (top-frame th s))))
+ (top (stack (top-frame th s)))))
+ (pop (pop (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (IUSHR) Instruction
+
+(defun execute-IUSHR (inst th s)
+ (let* ((val1 (top (pop (stack (top-frame th s)))))
+ (val2 (top (stack (top-frame th s))))
+ (shiftval (5-bit-fix val2))
+ (result (shr val1 shiftval)))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (int-fix result)
+ (pop (pop (stack (top-frame th s))))))))
+
+; -----------------------------------------------------------------------------
+; (IXOR) Instruction
+
+(defun execute-IXOR (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (logxor (top (pop (stack (top-frame th s))))
+ (top (stack (top-frame th s))))
+ (pop (pop (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (JSR) Instruction
+
+(defun execute-JSR (inst th s)
+ (modify th s
+ :pc (+ (arg1 inst) (pc (top-frame th s)))
+ :stack (push (list 'RETURNADDRESS
+ (+ (inst-length inst)
+ (pc (top-frame th s))))
+ (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (JSR_W) Instruction
+
+(defun execute-JSR_W (inst th s)
+ (modify th s
+ :pc (+ (arg1 inst) (pc (top-frame th s)))
+ :stack (push (list 'RETURNADDRESS
+ (+ (inst-length inst)
+ (pc (top-frame th s))))
+ (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (INVOKESPECIAL "class" "name" n) Instruction
+
+(defun class-name-of-ref (ref heap)
+ (car (car (deref ref heap))))
+
+(defun bind-formals (n stack)
+ (if (zp n)
+ nil
+ (cons (top stack)
+ (bind-formals (- n 1) (pop stack)))))
+
+(defun lookup-method-in-superclasses (name classes class-table)
+ (cond ((endp classes) nil)
+ (t (let* ((class-name (car classes))
+ (class-decl (bound? class-name class-table))
+ (method (bound? name (class-decl-methods class-decl))))
+ (if method
+ method
+ (lookup-method-in-superclasses name (cdr classes)
+ class-table))))))
+
+(defun lookup-method (name class-name class-table)
+ (lookup-method-in-superclasses name
+ (cons class-name
+ (class-decl-superclasses
+ (bound? class-name class-table)))
+ class-table))
+
+(defun execute-INVOKESPECIAL (inst th s)
+ (let* ((method-name (arg2 inst))
+ (nformals (arg3 inst))
+ (obj-ref (top (popn nformals (stack (top-frame th s)))))
+ (instance (deref obj-ref (heap s)))
+ (obj-class-name (arg1 inst))
+ (closest-method
+ (lookup-method method-name
+ obj-class-name
+ (class-table s)))
+ (prog (method-program closest-method))
+ (s1 (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (popn (+ nformals 1)
+ (stack (top-frame th s)))))
+ (tThread (rrefToThread obj-ref (thread-table s))))
+ (cond
+ ((method-isNative? closest-method)
+ (cond ((equal method-name "start")
+ (modify tThread s1 :status 'SCHEDULED))
+ ((equal method-name "stop")
+ (modify tThread s1
+ :status 'UNSCHEDULED))
+ (t s)))
+ ((and (method-sync closest-method)
+ (objectLockable? instance th))
+ (modify th s1
+ :call-stack
+ (push (make-frame 0
+ (reverse
+ (bind-formals (+ nformals 1)
+ (stack (top-frame th s))))
+ nil
+ prog
+ 'LOCKED
+ (arg1 inst))
+ (call-stack th s1))
+ :heap (lock-object th obj-ref (heap s))))
+ ((method-sync closest-method)
+ s)
+ (t
+ (modify th s1
+ :call-stack
+ (push (make-frame 0
+ (reverse
+ (bind-formals (+ nformals 1)
+ (stack (top-frame th s))))
+ nil
+ prog
+ 'UNLOCKED
+ (arg1 inst))
+ (call-stack th s1)))))))
+
+; -----------------------------------------------------------------------------
+; (INVOKESTATIC "class" "name" n) Instruction
+
+(defun execute-INVOKESTATIC (inst th s)
+ (let* ((class (arg1 inst))
+ (method-name (arg2 inst))
+ (nformals (arg3 inst))
+ (obj-ref (class-decl-heapref (bound? class (class-table s))))
+ (instance (deref obj-ref (heap s)))
+ (closest-method
+ (lookup-method method-name
+ (arg1 inst)
+ (class-table s)))
+ (prog (method-program closest-method))
+ (s1 (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (popn nformals (stack (top-frame th s))))))
+ (cond
+ ((and (method-sync closest-method)
+ (objectLockable? instance th))
+ (modify th s1
+ :call-stack
+ (push (make-frame 0
+ (reverse
+ (bind-formals nformals
+ (stack (top-frame th s))))
+ nil
+ prog
+ 'S_LOCKED
+ (arg1 inst))
+ (call-stack th s1))
+ :heap (lock-object th obj-ref (heap s))))
+ ((method-sync closest-method)
+ s)
+ (t
+ (modify th s1
+ :call-stack
+ (push (make-frame 0
+ (reverse
+ (bind-formals nformals
+ (stack (top-frame th s))))
+ nil
+ prog
+ 'UNLOCKED
+ (arg1 inst))
+ (call-stack th s1)))))))
+
+; -----------------------------------------------------------------------------
+; (INVOKEVIRTUAL "class" "name" n) Instruction
+
+(defun execute-INVOKEVIRTUAL (inst th s)
+ (let* ((method-name (arg2 inst))
+ (nformals (arg3 inst))
+ (obj-ref (top (popn nformals (stack (top-frame th s)))))
+ (instance (deref obj-ref (heap s)))
+ (obj-class-name (class-name-of-ref obj-ref (heap s)))
+ (closest-method
+ (lookup-method method-name
+ obj-class-name
+ (class-table s)))
+ (prog (method-program closest-method))
+ (s1 (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (popn (+ nformals 1)
+ (stack (top-frame th s)))))
+ (tThread (rrefToThread obj-ref (thread-table s))))
+ (cond
+ ((method-isNative? closest-method)
+ (cond ((equal method-name "start")
+ (modify tThread s1 :status 'SCHEDULED))
+ ((equal method-name "stop")
+ (modify tThread s1
+ :status 'UNSCHEDULED))
+ (t s)))
+ ((and (method-sync closest-method)
+ (objectLockable? instance th))
+ (modify th s1
+ :call-stack
+ (push (make-frame 0
+ (reverse
+ (bind-formals (+ nformals 1)
+ (stack (top-frame th s))))
+ nil
+ prog
+ 'LOCKED
+ (arg1 inst))
+ (call-stack th s1))
+ :heap (lock-object th obj-ref (heap s))))
+ ((method-sync closest-method)
+ s)
+ (t
+ (modify th s1
+ :call-stack
+ (push (make-frame 0
+ (reverse
+ (bind-formals (+ nformals 1)
+ (stack (top-frame th s))))
+ nil
+ prog
+ 'UNLOCKED
+ (arg1 inst))
+ (call-stack th s1)))))))
+
+; -----------------------------------------------------------------------------
+; (L2I) Instruction - long to int narrowing conversion
+
+(defun execute-L2I (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (int-fix (top (pop (stack (top-frame th s)))))
+ (pop (pop (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (LADD) Instruction - Add to longs from the top of the stack
+
+(defun execute-LADD (inst th s)
+ (let* ((val1 (top (pop (stack (top-frame th s)))))
+ (val2 (top (popn 3 (stack (top-frame th s))))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push 0
+ (push (long-fix (+ val1 val2))
+ (popn 4 (stack (top-frame th s))))))))
+
+; -----------------------------------------------------------------------------
+; (LALOAD) Instruction
+
+(defun execute-LALOAD (inst th s)
+ (let* ((index (top (stack (top-frame th s))))
+ (arrayref (top (pop (stack (top-frame th s)))))
+ (array (deref arrayref (heap s))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push 0
+ (push (element-at index array)
+ (pop (pop (stack (top-frame th s)))))))))
+
+; -----------------------------------------------------------------------------
+; (LAND) Instruction
+
+(defun execute-LAND (inst th s)
+ (let* ((val1 (top (pop (stack (top-frame th s)))))
+ (val2 (top (popn 3 (stack (top-frame th s))))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push 0
+ (push (logand val1 val2)
+ (popn 4 (stack (top-frame th s))))))))
+
+; -----------------------------------------------------------------------------
+; (LASTORE) Instruction
+
+(defun execute-LASTORE (inst th s)
+ (let* ((value (top (pop (stack (top-frame th s)))))
+ (index (top (pop (pop (stack (top-frame th s))))))
+ (arrayref (top (popn 3 (stack (top-frame th s))))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (popn 4 (stack (top-frame th s)))
+ :heap (bind (cadr arrayref)
+ (set-element-at value
+ index
+ (deref arrayref (heap s))
+ (class-table s))
+ (heap s)))))
+
+; -----------------------------------------------------------------------------
+; (LCMP) Instruction - compare two longs
+; val1 > val2 --> 1
+; val1 = val2 --> 0
+; val1 < val2 --> -1
+
+(defun execute-LCMP (inst th s)
+ (let* ((val2 (top (pop (stack (top-frame th s)))))
+ (val1 (top (popn 3 (stack (top-frame th s)))))
+ (result (cond ((> val1 val2) 1)
+ ((< val1 val2) -1)
+ (t 0))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push result
+ (popn 4 (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (LCONST_X) Instruction - push a certain long constant onto the stack
+; covers LCONST_{0, 1}
+
+(defun execute-LCONST_X (inst th s n)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push 0
+ (push n (stack (top-frame th s))))))
+
+; -----------------------------------------------------------------------------
+; (LDC) Instruction
+
+(defun set-instance-field (class-name field-name value instance)
+ (bind class-name
+ (bind field-name value
+ (binding class-name instance))
+ instance))
+
+(defun execute-LDC (inst th s)
+ (let* ((class (cur-class (top-frame th s)))
+ (cp (retrieve-cp class (class-table s)))
+ (entry (nth (arg1 inst) cp))
+ (value (cadr entry)))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push value (stack (top-frame th s))))))
+
+; -----------------------------------------------------------------------------
+; (LDC2_W) Instruction
+
+(defun execute-LDC2_W (inst th s)
+ (let* ((class (cur-class (top-frame th s)))
+ (cp (retrieve-cp class (class-table s)))
+ (entry (nth (arg1 inst) cp))
+ (value (cadr entry)))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push value (stack (top-frame th s))))))
+
+; -----------------------------------------------------------------------------
+; (LDIV) Instruction
+
+(defun execute-LDIV (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push 0
+ (push
+ (long-fix
+ (truncate (top (popn 3 (stack (top-frame th s))))
+ (top (pop (stack (top-frame th s))))))
+ (popn 4 (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (LLOAD idx) Instruction - Push a long local onto the stack
+
+(defun execute-LLOAD (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push 0
+ (push (nth (arg1 inst)
+ (locals (top-frame th s)))
+ (stack (top-frame th s))))))
+
+; -----------------------------------------------------------------------------
+; (LLOAD_X) Instruction - Push a long local onto the stack
+; covers LLOAD_{0, 1, 2, 3}
+
+(defun execute-LLOAD_X (inst th s n)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push 0
+ (push (nth n (locals (top-frame th s)))
+ (stack (top-frame th s))))))
+
+; -----------------------------------------------------------------------------
+; (LMUL) Instruction
+
+(defun execute-LMUL (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push 0
+ (push (ulong-fix
+ (* (top (pop (stack (top-frame th s))))
+ (top (popn 3 (stack (top-frame th s))))))
+ (popn 4 (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (LNEG) Instruction
+; Because of the way the JVM represents 2's complement ints,
+; the negation of the most negative int is itself
+
+(defun execute-LNEG (inst th s)
+ (let* ((result (if (equal (top (pop (stack (top-frame th s))))
+ *most-negative-long*)
+ *most-negative-long*
+ (- (top (pop (stack (top-frame th s))))))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push 0
+ (push result (popn 2 (stack (top-frame th s))))))))
+
+; -----------------------------------------------------------------------------
+; (LOR) Instruction
+
+(defun execute-LOR (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push 0
+ (push (logior (top (pop (stack (top-frame th s))))
+ (top (popn 3 (stack (top-frame th s)))))
+ (popn 4 (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (LREM) Instruction
+
+(defun execute-LREM (inst th s)
+ (let* ((val1 (top (pop (stack (top-frame th s)))))
+ (val2 (top (popn 3 (stack (top-frame th s)))))
+ (result (- val1 (* (truncate val1 val2) val2))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push 0
+ (push result
+ (popn 4 (stack (top-frame th s))))))))
+
+; -----------------------------------------------------------------------------
+; (LRETURN) Instruction - return a long
+
+(defun execute-LRETURN (inst th s)
+ (declare (ignore inst))
+ (let* ((val (top (pop (stack (top-frame th s)))))
+ (obj-ref (nth 0 (locals (top-frame th s))))
+ (sync-status (sync-flg (top-frame th s)))
+ (class (cur-class (top-frame th s)))
+ (ret-ref (class-decl-heapref (bound? class (class-table s))))
+ (new-heap (cond ((equal sync-status 'LOCKED)
+ (unlock-object th obj-ref (heap s)))
+ ((equal sync-status 'S_LOCKED)
+ (unlock-object th ret-ref (heap s)))
+ (t (heap s))))
+ (s1 (modify th s
+ :call-stack (pop (call-stack th s))
+ :heap new-heap)))
+ (modify th s1
+ :stack (push 0 (push val (stack (top-frame th s1)))))))
+
+; -----------------------------------------------------------------------------
+; (LSHL) Instruction
+
+(defun execute-LSHL (inst th s)
+ (let* ((val1 (top (popn 2 (stack (top-frame th s)))))
+ (val2 (top (stack (top-frame th s))))
+ (shiftval (6-bit-fix val2))
+ (result (shl val1 shiftval)))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push 0
+ (push (long-fix result)
+ (popn 3 (stack (top-frame th s))))))))
+
+; -----------------------------------------------------------------------------
+; (LSHR) Instruction
+
+(defun execute-LSHR (inst th s)
+ (let* ((val1 (top (popn 2 (stack (top-frame th s)))))
+ (val2 (top (stack (top-frame th s))))
+ (shiftval (6-bit-fix val2))
+ (result (shr val1 shiftval)))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push 0
+ (push (long-fix result)
+ (popn 3 (pop (stack (top-frame th s)))))))))
+
+; -----------------------------------------------------------------------------
+; (LSTORE idx) Instruction - store a long into the locals
+
+(defun execute-LSTORE (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :locals (update-nth (arg1 inst)
+ (top (pop (stack (top-frame th s))))
+ (locals (top-frame th s)))
+ :stack (popn 2 (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (LSTORE_X) Instruction - store a long into the locals
+; covers LSTORE_{0, 1, 2, 3}
+
+(defun execute-LSTORE_X (inst th s n)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :locals (update-nth n
+ (top (pop (stack (top-frame th s))))
+ (locals (top-frame th s)))
+ :stack (popn 2 (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (LSUB) Instruction
+
+(defun execute-LSUB (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push 0
+ (push
+ (ulong-fix (- (top (popn 3 (stack (top-frame th s))))
+ (top (pop (stack (top-frame th s))))))
+ (popn 4 (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (LUSHR) Instruction
+
+(defun execute-LUSHR (inst th s)
+ (let* ((val1 (top (popn 2 (stack (top-frame th s)))))
+ (val2 (top (stack (top-frame th s))))
+ (shiftval (6-bit-fix val2))
+ (result (shr val1 shiftval)))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push 0
+ (push (long-fix result)
+ (popn 3 (stack (top-frame th s))))))))
+
+; -----------------------------------------------------------------------------
+; (LXOR) Instruction
+
+(defun execute-LXOR (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push 0
+ (push (logxor (top (pop (stack (top-frame th s))))
+ (top (popn 3 (stack (top-frame th s)))))
+ (popn 4 (stack (top-frame th s)))))))
+
+; -----------------------------------------------------------------------------
+; (MONITORENTER) Instruction
+
+(defun execute-MONITORENTER (inst th s)
+ (let* ((obj-ref (top (stack (top-frame th s))))
+ (instance (deref obj-ref (heap s))))
+ (cond
+ ((objectLockable? instance th)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (pop (stack (top-frame th s)))
+ :heap (lock-object th obj-ref (heap s))))
+ (t s))))
+
+; -----------------------------------------------------------------------------
+; (MONITOREXIT) Instruction
+
+(defun execute-MONITOREXIT (inst th s)
+ (let* ((obj-ref (top (stack (top-frame th s))))
+ (instance (deref obj-ref (heap s))))
+ (cond
+ ((objectUnLockable? instance th)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (pop (stack (top-frame th s)))
+ :heap (unlock-object th obj-ref (heap s))))
+ (t s))))
+
+; -----------------------------------------------------------------------------
+; (MULTIANEWARRAY) Instruction
+
+(defun execute-MULTIANEWARRAY (inst th s)
+ (let* ((dimentions (arg1 inst))
+ (counts (reverse (take dimentions (stack (top-frame th s))))))
+ (mv-let (addr new-heap)
+ (makemultiarray counts s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (list 'REF addr)
+ (nthcdr dimentions (stack (top-frame th s))))
+ :heap new-heap))))
+
+; -----------------------------------------------------------------------------
+; (NEW "class") Instruction
+
+(defun execute-NEW (inst th s)
+ (let* ((class-name (arg1 inst))
+ (class-table (class-table s))
+ (closest-method (lookup-method "run" class-name class-table))
+ (prog (method-program closest-method))
+ (new-object (build-an-instance
+ (cons class-name
+ (class-decl-superclasses
+ (bound? class-name class-table)))
+ class-table))
+ (new-address (len (heap s)))
+ (s1 (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (list 'REF new-address)
+ (stack (top-frame th s)))
+ :heap (bind new-address new-object (heap s)))))
+ (if (isThreadObject? class-name class-table)
+ (modify nil s1
+ :thread-table
+ (addto-tt
+ (push
+ (make-frame 0
+ (list (list 'REF new-address))
+ nil
+ prog
+ 'UNLOCKED
+ class-name)
+ nil)
+ 'UNSCHEDULED
+ (list 'REF new-address)
+ (thread-table s1)))
+ s1)))
+
+; -----------------------------------------------------------------------------
+; (NEWARRAY) Instruction
+
+(defun execute-NEWARRAY (inst th s)
+ (let* ((type (arg1 inst))
+ (count (top (stack (top-frame th s))))
+ (addr (len (heap s)))
+ (obj (makearray type
+ count
+ (init-array type count)
+ (class-table s))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (list 'REF addr)
+ (pop (stack (top-frame th s))))
+ :heap (bind addr
+ obj
+ (heap s)))))
+
+; -----------------------------------------------------------------------------
+; (NOP) Instruction
+
+(defun execute-NOP (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (POP) Instruction
+
+(defun execute-POP (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (pop (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (POP2) Instruction
+
+(defun execute-POP2 (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (popn 2 (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (PUTFIELD "class" "field" ?long-flag?) Instruction
+
+(defun execute-PUTFIELD (inst th s)
+ (let* ((class-name (arg1 inst))
+ (field-name (arg2 inst))
+ (long-flag (arg3 inst))
+ (value (if long-flag
+ (top (pop (stack (top-frame th s))))
+ (top (stack (top-frame th s)))))
+ (instance (if long-flag
+ (deref (top (popn 2 (stack (top-frame th s)))) (heap s))
+ (deref (top (pop (stack (top-frame th s)))) (heap s))))
+ (address (cadr (if long-flag
+ (top (popn 2 (stack (top-frame th s))))
+ (top (pop (stack (top-frame th s))))))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (if long-flag
+ (popn 3 (stack (top-frame th s)))
+ (pop (pop (stack (top-frame th s)))))
+ :heap (bind address
+ (set-instance-field class-name
+ field-name
+ value
+ instance)
+ (heap s)))))
+
+; -----------------------------------------------------------------------------
+; (PUTSTATIC "class" "field" ?long-flag?) Instruction
+
+(defun execute-PUTSTATIC (inst th s)
+ (let* ((class-name (arg1 inst))
+ (field-name (arg2 inst))
+ (long-flag (arg3 inst))
+ (class-ref (class-decl-heapref
+ (bound? class-name (class-table s))))
+ (value (if long-flag
+ (top (pop (stack (top-frame th s))))
+ (top (stack (top-frame th s)))))
+ (instance (deref class-ref (heap s))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (if long-flag
+ (popn 2 (stack (top-frame th s)))
+ (pop (stack (top-frame th s))))
+ :heap (bind (cadr class-ref)
+ (set-instance-field "java.lang.Class"
+ field-name
+ value
+ instance)
+ (heap s)))))
+
+; -----------------------------------------------------------------------------
+; (RET) Instruction
+
+(defun execute-RET (inst th s)
+ (let* ((ret-addr (nth (arg1 inst) (locals (top-frame th s))))
+ (addr (cadr ret-addr)))
+ (modify th s :pc addr)))
+
+; -----------------------------------------------------------------------------
+; (RETURN) Instruction - Void Return
+
+(defun execute-RETURN (inst th s)
+ (declare (ignore inst))
+ (let* ((obj-ref (nth 0 (locals (top-frame th s))))
+ (sync-status (sync-flg (top-frame th s)))
+ (class (cur-class (top-frame th s)))
+ (ret-ref (class-decl-heapref (bound? class (class-table s))))
+ (new-heap (cond ((equal sync-status 'LOCKED)
+ (unlock-object th obj-ref (heap s)))
+ ((equal sync-status 'S_LOCKED)
+ (unlock-object th ret-ref (heap s)))
+ (t (heap s)))))
+ (modify th s
+ :call-stack (pop (call-stack th s))
+ :heap new-heap)))
+
+; -----------------------------------------------------------------------------
+; (SALOAD) Instruction
+
+(defun execute-SALOAD (inst th s)
+ (let* ((index (top (stack (top-frame th s))))
+ (arrayref (top (pop (stack (top-frame th s)))))
+ (array (deref arrayref (heap s))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (element-at index array)
+ (pop (pop (stack (top-frame th s))))))))
+
+; -----------------------------------------------------------------------------
+; (SASTORE) Instruction
+
+(defun execute-SASTORE (inst th s)
+ (let* ((value (top (stack (top-frame th s))))
+ (index (top (pop (stack (top-frame th s)))))
+ (arrayref (top (pop (pop (stack (top-frame th s)))))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (pop (pop (pop (stack (top-frame th s)))))
+ :heap (bind (cadr arrayref)
+ (set-element-at (short-fix value)
+ index
+ (deref arrayref (heap s))
+ (class-table s))
+ (heap s)))))
+
+; -----------------------------------------------------------------------------
+; (SIPUSH const) Instruction
+
+(defun execute-SIPUSH (inst th s)
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push (short-fix (arg1 inst))
+ (stack (top-frame th s)))))
+
+; -----------------------------------------------------------------------------
+; (SWAP) Instruction
+
+(defun execute-SWAP (inst th s)
+ (let* ((val1 (top (stack (top-frame th s))))
+ (val2 (top (pop (stack (top-frame th s))))))
+ (modify th s
+ :pc (+ (inst-length inst) (pc (top-frame th s)))
+ :stack (push val2
+ (push val1
+ (pop (pop (stack (top-frame th s)))))))))
+
+; -----------------------------------------------------------------------------
+; Putting it all together
+
+(defun index-into-program (byte-offset program)
+ (declare (xargs :measure (len program)))
+ (if (endp program)
+ nil
+ (if (zp byte-offset)
+ (car program)
+ (index-into-program (- byte-offset
+ (inst-length (car program)))
+ (cdr program)))))
+
+(defun next-inst (th s)
+ (index-into-program (pc (top-frame th s))
+ (program (top-frame th s))))
+
+(defun do-inst (inst th s)
+ (case (op-code inst)
+ (AALOAD (execute-AALOAD inst th s))
+ (AASTORE (execute-AASTORE inst th s))
+ (ACONST_NULL (execute-ACONST_NULL inst th s))
+ (ALOAD (execute-ALOAD inst th s))
+ (ALOAD_0 (execute-ALOAD_X inst th s 0))
+ (ALOAD_1 (execute-ALOAD_X inst th s 1))
+ (ALOAD_2 (execute-ALOAD_X inst th s 2))
+ (ALOAD_3 (execute-ALOAD_X inst th s 3))
+ (ANEWARRAY (execute-ANEWARRAY inst th s))
+ (ARETURN (execute-ARETURN inst th s))
+ (ARRAYLENGTH (execute-ARRAYLENGTH inst th s))
+ (ASTORE (execute-ASTORE inst th s))
+ (ASTORE_0 (execute-ASTORE_X inst th s 0))
+ (ASTORE_1 (execute-ASTORE_X inst th s 1))
+ (ASTORE_2 (execute-ASTORE_X inst th s 2))
+ (ASTORE_3 (execute-ASTORE_X inst th s 3))
+ (BALOAD (execute-BALOAD inst th s))
+ (BASTORE (execute-BASTORE inst th s))
+ (BIPUSH (execute-BIPUSH inst th s))
+ (CALOAD (execute-CALOAD inst th s))
+ (CASTORE (execute-CASTORE inst th s))
+ (DUP (execute-DUP inst th s))
+ (DUP_X1 (execute-DUP_X1 inst th s))
+ (DUP_X2 (execute-DUP_X2 inst th s))
+ (DUP2 (execute-DUP2 inst th s))
+ (DUP2_X1 (execute-DUP2_X1 inst th s))
+ (DUP2_X2 (execute-DUP2_X2 inst th s))
+ (GETFIELD (execute-GETFIELD inst th s))
+ (GETSTATIC (execute-GETSTATIC inst th s))
+ (GOTO (execute-GOTO inst th s))
+ (GOTO_W (execute-GOTO_W inst th s))
+ (I2B (execute-I2B inst th s))
+ (I2C (execute-I2C inst th s))
+ (I2L (execute-I2L inst th s))
+ (I2S (execute-I2S inst th s))
+ (IADD (execute-IADD inst th s))
+ (IALOAD (execute-IALOAD inst th s))
+ (IAND (execute-IAND inst th s))
+ (IASTORE (execute-IASTORE inst th s))
+ (ICONST_M1 (execute-ICONST_X inst th s -1))
+ (ICONST_0 (execute-ICONST_X inst th s 0))
+ (ICONST_1 (execute-ICONST_X inst th s 1))
+ (ICONST_2 (execute-ICONST_X inst th s 2))
+ (ICONST_3 (execute-ICONST_X inst th s 3))
+ (ICONST_4 (execute-ICONST_X inst th s 4))
+ (ICONST_5 (execute-ICONST_X inst th s 5))
+ (IDIV (execute-IDIV inst th s))
+ (IF_ACMPEQ (execute-IF_ACMPEQ inst th s))
+ (IF_ACMPNE (execute-IF_ACMPNE inst th s))
+ (IF_ICMPEQ (execute-IF_ICMPEQ inst th s))
+ (IF_ICMPGE (execute-IF_ICMPGE inst th s))
+ (IF_ICMPGT (execute-IF_ICMPGT inst th s))
+ (IF_ICMPLE (execute-IF_ICMPLE inst th s))
+ (IF_ICMPLT (execute-IF_ICMPLT inst th s))
+ (IF_ICMPNE (execute-IF_ICMPNE inst th s))
+ (IFEQ (execute-IFEQ inst th s))
+ (IFGE (execute-IFGE inst th s))
+ (IFGT (execute-IFGT inst th s))
+ (IFLE (execute-IFLE inst th s))
+ (IFLT (execute-IFLT inst th s))
+ (IFNE (execute-IFNE inst th s))
+ (IFNONNULL (execute-IFNONNULL inst th s))
+ (IFNULL (execute-IFNULL inst th s))
+ (IINC (execute-IINC inst th s))
+ (ILOAD (execute-ILOAD inst th s))
+ (ILOAD_0 (execute-ILOAD_X inst th s 0))
+ (ILOAD_1 (execute-ILOAD_X inst th s 1))
+ (ILOAD_2 (execute-ILOAD_X inst th s 2))
+ (ILOAD_3 (execute-ILOAD_X inst th s 3))
+ (IMUL (execute-IMUL inst th s))
+ (INEG (execute-INEG inst th s))
+ (INSTANCEOF (execute-INSTANCEOF inst th s))
+ (INVOKESPECIAL (execute-INVOKESPECIAL inst th s))
+ (INVOKESTATIC (execute-INVOKESTATIC inst th s))
+ (INVOKEVIRTUAL (execute-INVOKEVIRTUAL inst th s))
+ (IOR (execute-IOR inst th s))
+ (IREM (execute-IREM inst th s))
+ (IRETURN (execute-IRETURN inst th s))
+ (ISHL (execute-ISHL inst th s))
+ (ISHR (execute-ISHR inst th s))
+ (ISTORE (execute-ISTORE inst th s))
+ (ISTORE_0 (execute-ISTORE_X inst th s 0))
+ (ISTORE_1 (execute-ISTORE_X inst th s 1))
+ (ISTORE_2 (execute-ISTORE_X inst th s 2))
+ (ISTORE_3 (execute-ISTORE_X inst th s 3))
+ (ISUB (execute-ISUB inst th s))
+ (IUSHR (execute-IUSHR inst th s))
+ (IXOR (execute-IXOR inst th s))
+ (JSR (execute-JSR inst th s))
+ (JSR_W (execute-JSR_W inst th s))
+ (L2I (execute-L2I inst th s))
+ (LADD (execute-LADD inst th s))
+ (LALOAD (execute-LALOAD inst th s))
+ (LAND (execute-LAND inst th s))
+ (LASTORE (execute-LASTORE inst th s))
+ (LCMP (execute-LCMP inst th s))
+ (LCONST_0 (execute-LCONST_X inst th s 0))
+ (LCONST_1 (execute-LCONST_X inst th s 1))
+ (LDC (execute-LDC inst th s))
+ (LDC_W (execute-LDC inst th s))
+ (LDC2_W (execute-LDC2_W inst th s))
+ (LDIV (execute-LDIV inst th s))
+ (LLOAD (execute-LLOAD inst th s))
+ (LLOAD_0 (execute-LLOAD_X inst th s 0))
+ (LLOAD_1 (execute-LLOAD_X inst th s 1))
+ (LLOAD_2 (execute-LLOAD_X inst th s 2))
+ (LLOAD_3 (execute-LLOAD_X inst th s 3))
+ (LMUL (execute-LMUL inst th s))
+ (LNEG (execute-LNEG inst th s))
+ (LOR (execute-LOR inst th s))
+ (LREM (execute-LREM inst th s))
+ (LRETURN (execute-LRETURN inst th s))
+ (LSHL (execute-LSHL inst th s))
+ (LSHR (execute-LSHR inst th s))
+ (LSTORE (execute-LSTORE inst th s))
+ (LSTORE_0 (execute-LSTORE_X inst th s 0))
+ (LSTORE_1 (execute-LSTORE_X inst th s 1))
+ (LSTORE_2 (execute-LSTORE_X inst th s 2))
+ (LSTORE_3 (execute-LSTORE_X inst th s 3))
+ (LSUB (execute-LSUB inst th s))
+ (LUSHR (execute-LUSHR inst th s))
+ (LXOR (execute-LXOR inst th s))
+ (MONITORENTER (execute-MONITORENTER inst th s))
+ (MONITOREXIT (execute-MONITOREXIT inst th s))
+ (MULTIANEWARRAY (execute-MULTIANEWARRAY inst th s))
+ (NEW (execute-NEW inst th s))
+ (NEWARRAY (execute-NEWARRAY inst th s))
+ (NOP (execute-NOP inst th s))
+ (POP (execute-POP inst th s))
+ (POP2 (execute-POP2 inst th s))
+ (PUTFIELD (execute-PUTFIELD inst th s))
+ (PUTSTATIC (execute-PUTSTATIC inst th s))
+ (RET (execute-RET inst th s))
+ (RETURN (execute-RETURN inst th s))
+ (SALOAD (execute-SALOAD inst th s))
+ (SASTORE (execute-SASTORE inst th s))
+ (SIPUSH (execute-SIPUSH inst th s))
+ (SWAP (execute-SWAP inst th s))
+ (HALT s)
+ (otherwise s)))
+
+(defun step (th s)
+ (if (equal (status th s) 'SCHEDULED)
+ (do-inst (next-inst th s) th s)
+ s))
+
+(defun run (sched s)
+ (if (endp sched)
+ s
+ (run (cdr sched) (step (car sched) s))))
+
+; Begin the simulator
+;
+
+(defun ack2 (num n lst)
+ (if (zp n)
+ lst
+ (ack2 num (- n 1) (cons num lst))))
+
+(defun ack0 (n)
+ (ack2 0 n nil))
+
+(acl2::set-state-ok t)
+
+(defun sim-loop (s acl2::state)
+ (declare (acl2::xargs :mode :program))
+ (prog2$
+ (acl2::cw "~%>>") ;;; Print prompt
+ (acl2::mv-let
+ (flg cmd acl2::state)
+ (acl2::read-object acl2::*standard-oi* acl2::state) ;;; read next command
+ (declare (ignore flg))
+ (cond
+ ((equal cmd :q) (acl2::value t)) ;;; quit on :q
+ ((and (consp cmd) ;;; recognize (step i) and (step i j)
+ (acl2::eq (car cmd) 'step) ;;; where i and j are integers
+ (true-listp cmd)
+ (consp (cdr cmd))
+ (integerp (cadr cmd))
+ (or (acl2::null (cddr cmd))
+ (and (integerp (caddr cmd))
+ (acl2::null (cdddr cmd)))))
+ (let ((thread (cadr cmd))
+ (n (if (cddr cmd) (caddr cmd) 1)))
+ (sim-loop (run (ack2 thread n nil) s) acl2::state)))
+ (t (acl2::mv-let (flg val acl2::state)
+ (acl2::simple-translate-and-eval cmd
+ (list (cons 's s))
+ nil
+ "Your command" 'sim
+ (acl2::w acl2::state)
+ acl2::state
+ nil)
+ (prog2$
+ (cond (flg nil)
+ (t (acl2::cw "~x0~%" (cdr val))))
+ (sim-loop s acl2::state))))))))
+
+(defun sim (s acl2::state)
+ (declare (acl2::xargs :mode :program))
+ (prog2$
+ (acl2::cw "~%M5 Simulator.~%~%")
+ (sim-loop s acl2::state)))
+
+; A small assembler to resolve labels into relative byte addresses
+;
+; Labels are symbols in the "LABEL" package. Examples include:
+; LABEL::JUMP LABEL::FOR LABEL::START1
+;
+; To denote the jump-to point, insert a label before the opcode
+;
+; '((aconst_null) '((aconst_null)
+; (goto LABEL::TARGET) (goto 5)
+; (iconst_0) =====> (iconst_0)
+; (iconst_2) (iconst_2)
+; (LABEL::TARGET ADD) (add)
+; (ireturn)) (ireturn))
+
+(defun isLabel? (sym)
+ (and (symbolp sym)
+ (equal (symbol-package-name sym) "LABEL")))
+
+(defun isLabeledInst? (inst)
+ (isLabel? (car inst)))
+
+(defun gen_label_alist (bytecodes cur_pc label_alist)
+ (if (endp bytecodes)
+ label_alist
+ (let* ((bare_inst (if (isLabeledInst? (car bytecodes))
+ (cdr (car bytecodes))
+ (car bytecodes))))
+ (gen_label_alist (cdr bytecodes)
+ (+ cur_pc
+ (inst-length bare_inst))
+ (if (isLabeledInst? (car bytecodes))
+ (bind (car (car bytecodes))
+ cur_pc
+ label_alist)
+ label_alist)))))
+
+(defun resolve_labels (bytecodes cur_pc label_alist)
+ (if (endp bytecodes)
+ nil
+ (let* ((inst (car bytecodes))
+ (bare-inst (if (isLabeledInst? inst)
+ (cdr inst)
+ inst))
+ (resolved-inst (if (isLabel? (arg1 bare-inst))
+ (list (op-code bare-inst)
+ (- (binding (arg1 bare-inst)
+ label_alist)
+ cur_pc))
+ bare-inst)))
+ (append (list resolved-inst)
+ (resolve_labels (cdr bytecodes)
+ (+ cur_pc
+ (inst-length bare-inst))
+ label_alist)))))
+
+; resolve_basic_block takes a method and resolves all of the labels
+;
+; note that the JVM restricts jumps to within the method
+
+(defun resolve_basic_block (bytecodes)
+ (resolve_labels bytecodes
+ 0
+ (gen_label_alist bytecodes 0 nil)))
+
+; The following functions are used to strip a state down to resolve
+; all of the basic blocks and build up the newly resolved state
+
+; resolving thread tables
+;
+(defun assemble_frame (frame)
+ (make-frame (pc frame)
+ (locals frame)
+ (stack frame)
+ (resolve_basic_block (program frame))
+ (sync-flg frame)
+ (cur-class frame)))
+
+(defun assemble_call_stack (cs)
+ (if (endp cs)
+ nil
+ (cons (assemble_frame (car cs))
+ (assemble_call_stack (cdr cs)))))
+
+(defun assemble_thread (thread)
+ (list (assemble_call_stack (car thread))
+ (cadr thread)
+ (caddr thread)))
+
+(defun assemble_thread_table (tt)
+ (if (endp tt)
+ nil
+ (cons (cons (caar tt)
+ (assemble_thread (cdar tt)))
+ (assemble_thread_table (cdr tt)))))
+
+; resolving class tables
+;
+(defun assemble_method (method)
+ (append (list (method-name method)
+ (method-formals method)
+ (method-sync method))
+ (resolve_basic_block (method-program method))))
+
+(defun assemble_methods (methods)
+ (if (endp methods)
+ nil
+ (cons (assemble_method (car methods))
+ (assemble_methods (cdr methods)))))
+
+(defun assemble_class (class)
+ (make-class-decl (class-decl-name class)
+ (class-decl-superclasses class)
+ (class-decl-fields class)
+ (class-decl-sfields class)
+ (class-decl-cp class)
+ (assemble_methods (class-decl-methods class))
+ (class-decl-heapref class)))
+
+(defun assemble_class_table (ct)
+ (if (endp ct)
+ nil
+ (cons (assemble_class (car ct))
+ (assemble_class_table (cdr ct)))))
+
+(defun assemble_state (s)
+ (make-state (assemble_thread_table (thread-table s))
+ (heap s)
+ (assemble_class_table (class-table s))))
+
+; -----------------------------------------------------------------------------
+; load_class_library: a utility for populating the heap with Class and
+; String objects
+
+(defun make-string-obj (class cpentry s idx)
+ (let* ((new-object (build-an-instance
+ (cons "java.lang.String"
+ (class-decl-superclasses
+ (bound? "java.lang.String" (class-table s))))
+ (class-table s)))
+ (stuffed-obj (set-instance-field "java.lang.String"
+ "strcontents"
+ (caddr cpentry)
+ new-object))
+ (new-address (len (heap s))))
+ (modify th s
+ :heap (bind new-address stuffed-obj (heap s))
+ :class-table (update-ct-string-ref
+ class
+ idx
+ (list 'REF new-address)
+ (class-table s)))))
+
+
+(defun resolve-string-constants (class cp s idx)
+ (cond ((endp cp) s)
+ ((equal (caar cp) 'STRING)
+ (resolve-string-constants class
+ (cdr cp)
+ (make-string-obj class (car cp) s idx)
+ (+ idx 1)))
+ (t (resolve-string-constants class (cdr cp) s (+ idx 1)))))
+
+
+(defun gen_class_obj (class s)
+ (let* ((new-state (resolve-string-constants class
+ (retrieve-cp class (class-table s))
+ s
+ 0))
+ (new-heap (heap new-state))
+ (new-ct (class-table new-state))
+ (new-object (build-a-class-instance
+ (class-decl-sfields (bound? class new-ct))
+ new-ct))
+ (stuffed-obj (set-instance-field "java.lang.Class"
+ "<name>"
+ class
+ new-object))
+ (new-address (len new-heap))
+ (old-class-ent (bound? class new-ct))
+ (new-class-ent
+ (make-class-decl (class-decl-name old-class-ent)
+ (class-decl-superclasses old-class-ent)
+ (class-decl-fields old-class-ent)
+ (class-decl-sfields old-class-ent)
+ (class-decl-cp old-class-ent)
+ (class-decl-methods old-class-ent)
+ (list 'REF new-address)))
+ (new-class-table (bind class
+ (cdr new-class-ent)
+ new-ct)))
+ (make-state (thread-table s)
+ (bind new-address stuffed-obj new-heap)
+ new-class-table)))
+
+(defun ld_class_lib (classes s)
+ (if (endp classes)
+ s
+ (ld_class_lib (cdr classes) (gen_class_obj (car classes) s))))
+
+(defun load_class_library (s)
+ (ld_class_lib (strip-cars (class-table s)) s))
+
+; -----------------------------------------------------------------------------
+; m5_load: both load and resolve a given state
+
+(defun m5_load (s)
+ (load_class_library (assemble_state s)))
+
diff --git a/books/workshops/2003/moore_vcg/support/utilities.acl2 b/books/workshops/2003/moore_vcg/support/utilities.acl2
new file mode 100644
index 0000000..af0e795
--- /dev/null
+++ b/books/workshops/2003/moore_vcg/support/utilities.acl2
@@ -0,0 +1,7 @@
+(value :q)
+
+(lp)
+
+(include-book "m5")
+
+(certify-book "utilities" ? t)
diff --git a/books/workshops/2003/moore_vcg/support/utilities.lisp b/books/workshops/2003/moore_vcg/support/utilities.lisp
new file mode 100644
index 0000000..ea8c44b
--- /dev/null
+++ b/books/workshops/2003/moore_vcg/support/utilities.lisp
@@ -0,0 +1,209 @@
+; Copyright (C) 2001, Regents of the University of Texas
+; Written by J Strother Moore
+; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
+
+#|
+; Certification Instructions.
+
+(include-book
+ "m5")
+
+(certify-book "utilities" 1)
+
+J Moore
+|#
+
+(in-package "M5")
+
+; Here we develop the general theory for proving things about the
+; M5 bytecode.
+
+; Arithmetic
+
+(include-book "../../../../arithmetic/top-with-meta")
+
+; We prove a few things about int arithmetic. We ought to prove
+; many more, but I just put enough here to get the factorial
+; proof to go through.
+
+(include-book "../../../../ihs/quotient-remainder-lemmas")
+
+(defun intp (x)
+ (and (integerp x)
+ (<= (- (expt 2 31)) x)
+ (< x (expt 2 31))))
+
+(defthm int-lemma0
+ (implies (intp x)
+ (integerp x))
+ :rule-classes (:rewrite :forward-chaining))
+
+(defthm int-lemma1
+ (intp (int-fix x)))
+
+(local (in-theory (cons 'zp (disable mod))))
+
+(defthm int-lemma2
+ (implies (and (intp x)
+ (not (zp x)))
+ (equal (int-fix (+ -1 x))
+ (+ -1 x))))
+
+(defthm int-lemma3
+ (implies (and (intp x)
+ (not (zp x)))
+ (intp (+ -1 x))))
+
+(defthm int-lemma4a
+ (implies (and (integerp x)
+ (integerp y))
+ (equal (int-fix (* x (int-fix y)))
+ (int-fix (* x y)))))
+
+(defthm int-lemma5a
+ (implies (and (integerp x)
+ (integerp y))
+ (equal (int-fix (+ x (int-fix y)))
+ (int-fix (+ x y)))))
+
+; This is a special case of the above. I need a more general
+; handling of this, but this will do for the moment.
+
+(defthm int-lemma5a1
+ (implies (and (integerp x1)
+ (integerp x2)
+ (integerp y))
+ (equal (int-fix (+ x1 x2 (int-fix y)))
+ (int-fix (+ x1 x2 y))))
+ :hints (("Goal" :use (:instance int-lemma5a (x (+ x1 x2))))))
+
+(defthm int-lemma6
+ (implies (intp x)
+ (equal (int-fix x) x)))
+
+(in-theory (disable intp int-fix))
+
+(defthm int-lemma4b
+ (implies (and (integerp x)
+ (integerp y))
+ (equal (int-fix (* (int-fix y) x))
+ (int-fix (* y x)))))
+
+(defthm int-lemma5b
+ (implies (and (integerp x)
+ (integerp y))
+ (equal (int-fix (+ (int-fix y) x))
+ (int-fix (+ y x)))))
+
+; Structures
+
+(defthm states
+ (and (equal (thread-table (make-state tt h c)) tt)
+ (equal (heap (make-state tt h c)) h)
+ (equal (class-table (make-state tt h c)) c)))
+
+(in-theory (disable make-state thread-table heap class-table))
+
+(defthm frames
+ (and
+ (equal (pc (make-frame pc l s prog sync-flg cur-class))
+ pc)
+ (equal (locals (make-frame pc l s prog sync-flg cur-class))
+ l)
+ (equal (stack (make-frame pc l s prog sync-flg cur-class))
+ s)
+ (equal (program (make-frame pc l s prog sync-flg cur-class))
+ prog)
+ (equal (sync-flg (make-frame pc l s prog sync-flg cur-class))
+ sync-flg)
+ (equal (cur-class (make-frame pc l s prog sync-flg cur-class))
+ cur-class)))
+
+(in-theory
+ (disable make-frame pc locals stack program sync-flg cur-class))
+
+(defthm stacks
+ (and (equal (top (push x s)) x)
+ (equal (pop (push x s)) s)))
+
+(in-theory (disable push top pop))
+
+; Mappings
+
+(defthm assoc-equal-bind
+ (equal (assoc-equal key1 (bind key2 val alist))
+ (if (equal key1 key2)
+ (cons key1 val)
+ (assoc-equal key1 alist))))
+
+(defthm bind-bind
+ (equal (bind x v (bind x w a))
+ (bind x v a)))
+
+; Semi-Ground Terms
+
+(defthm bind-formals-opener
+ (implies (and (integerp n)
+ (<= 0 n))
+ (equal (bind-formals (+ 1 n) stack)
+ (cons (top stack)
+ (bind-formals n (pop stack))))))
+
+(defthm nth-opener
+ (and (equal (nth 0 lst) (car lst))
+ (implies (and (integerp n)
+ (<= 0 n))
+ (equal (nth (+ 1 n) lst)
+ (nth n (cdr lst))))))
+
+(in-theory (disable nth))
+
+(defthm popn-opener
+ (implies (and (integerp n)
+ (<= 0 n))
+ (equal (popn (+ 1 n) stack)
+ (popn n (pop stack)))))
+
+(defun repeat (th n)
+ (if (zp n)
+ nil
+ (cons th (repeat th (- n 1)))))
+
+(defthm repeat-opener
+ (implies (and (integerp n)
+ (<= 0 n))
+ (equal (repeat th (+ 1 n))
+ (cons th (repeat th n)))))
+
+; The nil conjunct below is needed because we will disable run.
+
+(defthm run-opener
+ (and (equal (run nil s) s)
+ (equal (run (cons th sched) s)
+ (run sched (step th s))))
+ :hints (("Goal" :in-theory (disable step))))
+
+;(in-theory (enable top pop push lookup-method))
+
+; Step Stuff
+
+(defthm step-opener
+ (implies (consp (next-inst th s))
+ (equal (step th s)
+ (if (equal (status th s) 'SCHEDULED)
+ (do-inst (next-inst th s) th s)
+ s)))
+ :hints (("Goal" :in-theory (disable do-inst))))
+
+(in-theory (disable step))
+
+; Clocks
+
+
+
+(defthm run-append
+ (equal (run (append sched1 sched2) s)
+ (run sched2 (run sched1 s))))
+
+(in-theory (disable run))
+
diff --git a/books/workshops/2003/moore_vcg/support/vcg-examples.acl2 b/books/workshops/2003/moore_vcg/support/vcg-examples.acl2
new file mode 100644
index 0000000..ce63104
--- /dev/null
+++ b/books/workshops/2003/moore_vcg/support/vcg-examples.acl2
@@ -0,0 +1,6 @@
+(value :q)
+
+(lp)
+
+(include-book "utilities")
+(certify-book "vcg-examples" ? t)
diff --git a/books/workshops/2003/moore_vcg/support/vcg-examples.lisp b/books/workshops/2003/moore_vcg/support/vcg-examples.lisp
new file mode 100644
index 0000000..d3e17a4
--- /dev/null
+++ b/books/workshops/2003/moore_vcg/support/vcg-examples.lisp
@@ -0,0 +1,904 @@
+; Copyright (C) 2003, Regents of the University of Texas
+; Written by J Strother Moore
+; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
+
+; Use of Tail-Recursion to Propagate Inductive Assertions
+; J Strother Moore
+; February 26, 2003
+
+; cd /u/moore/m5/tolquhon
+; (include-book "utilities")
+; (ld "vcg-examples.lisp" :ld-pre-eval-print t)
+
+; Certification:
+; (include-book "utilities")
+; (certify-book "vcg-examples" 1)
+
+; ---------------------------------------------------------------------------
+; Preliminaries
+
+; This first part is just ``prelude''. It has nothing to do with the
+; specific programs we will verify.
+
+(in-package "M5")
+
+(include-book "../../../../misc/defpun")
+
+(defmacro defpun (g args &rest tail)
+ `(acl2::defpun ,g ,args ,@tail))
+
+;(ACL2::SET-MATCH-FREE-ERROR NIL)
+
+(defthm update-nth-opener
+ (and (equal (update-nth 0 x a) (cons x (cdr a)))
+ (implies (not (zp n))
+ (equal (update-nth n x a)
+ (cons (car a) (update-nth (- n 1) x (cdr a)))))))
+
+; ---------------------------------------------------------------------------
+; Some Preliminaries for Our First Program
+
+(defthm int-evenp-inv-a
+ (implies (intp i)
+ (iff (evenp (int-fix (- i 2)))
+ (evenp i)))
+ :hints
+ (("Goal" :in-theory (e/d (intp int-fix)
+ (floor)))))
+
+(defthm int-evenp-inv-b
+ (implies (intp i)
+ (iff (evenp (- i 2))
+ (evenp i)))
+ :hints
+ (("Goal" :in-theory (e/d (intp int-fix)
+ (floor)))))
+
+(in-theory (disable evenp))
+
+(defthm int-lemma2a
+ (implies (and (intp x)
+ (<= 0 x))
+ (equal (int-fix (+ -2 x))
+ (+ -2 x)))
+ :hints (("Goal" :in-theory (e/d (intp) nil))))
+
+(defthm int-lemma2b
+ (implies (and (intp x)
+ (<= 0 x))
+ (intp (+ -2 x)))
+ :hints (("Goal" :in-theory (e/d (intp) nil))))
+
+; ---------------------------------------------------------------------------
+; Our First Program
+
+; Below is an m5 program that decrements its first local, n, by 2 and
+; iterates until the result is 0. On each iteration it adds 1 to a
+; local variable, a, which is initialized to 0. The program ends with
+; a HALT instruction, which puts the machine in an infinite loop, i.e.,
+; executing HALT doesn't change the pc and the machine "stops." Later
+; we deal with the more realistic situation of a RETURN to some caller.
+; We will prove that if the program below reaches the HALT instruction,
+; the initial value, n0, of n was even and the result on the stack is
+; n0/2. This program does not terminate when n0 is odd.
+
+; To make the program slightly simpler to deal with, I only consider
+; the case where n0 is a non-negative int. (Java programmers will note
+; that the program actually halts for even negative ints, because of
+; wrap-around.)
+
+(defconst *flat-prog*
+ '((iconst_0) ; 0
+ (istore_1) ; 1 a := 0;
+ (iload_0) ; 2 top of loop:
+ (ifeq 14) ; 3 if n=0, goto 17;
+ (iload_1) ; 6
+ (iconst_1) ; 7
+ (iadd) ; 8
+ (istore_1) ; 9 a := a+1;
+ (iload_0) ;10
+ (iconst_2) ;11
+ (isub) ;12
+ (istore_0) ;13 n := n-2;
+ (goto -12) ;14 goto top of loop
+ (iload_1) ;17
+ (halt))) ;18
+
+; Here is the ``semantics'' of the loop, in the case in interest.
+
+(defun halfa (n a)
+ (declare (xargs :measure (nfix n)))
+ (if (zp n)
+ a
+ (halfa (- n 2) (int-fix (+ a 1)))))
+
+; ---------------------------------------------------------------------------
+; The Assertions at the Three Cut Points
+
+; We will use a classic ``inductive assertion'' method. The following
+; function takes a state, s, and the ``initial'' value of n, n0, and
+; states the assertions we wish to attach to pcs 0, 2, and 18. These
+; are the so-called ``cut points'' of my choice: the entry to the
+; program, the top of the loop, and exit from the program.
+
+; The particular assertions are not my main interest in this paper.
+; You can read them if you want. The real nugget in this paper is not
+; the assertions but the fact that I use tail recursion by step to
+; propagate assertions from the cut points to all the pcs.
+
+; That said, let me note that the assertions are complicated because
+; they have to handle the fact that halfa tracks the program only as
+; long as n stays non-negative. Things would be simpler if I assumed
+; that n0 was even. But I like illustrating the capability of
+; establishing conditions that hold for n0 in the event of
+; termination.
+
+(defun flat-pre-condition (n0 n)
+ (and (equal n n0)
+ (intp n0)
+ (<= 0 n0)))
+
+(defun flat-loop-invariant (n0 n a)
+ (and (intp n0)
+ (<= 0 n0)
+ (intp n)
+ (if (and (<= 0 n)
+ (evenp n))
+ (equal (halfa n a)
+ (halfa n0 0))
+ (not (evenp n)))
+ (iff (evenp n0) (evenp n))))
+
+(defun flat-post-condition (n0 value)
+ (and (evenp n0)
+ (equal value (halfa n0 0))))
+
+(defun flat-assertion (n0 th s)
+ (let ((n (nth 0 (locals (top-frame th s))))
+ (a (nth 1 (locals (top-frame th s)))))
+ (and (equal (program (top-frame th s)) *flat-prog*)
+ (case (pc (top-frame th s))
+ (0 (flat-pre-condition n0 n))
+ (2 (flat-loop-invariant n0 n a))
+ (18 (let ((value (top (stack (top-frame th s)))))
+ (flat-post-condition n0 value)))
+ (otherwise nil)))))
+
+; Observe that the output condition is that n0 is even and that the
+; top of the stack contains the semantic expression (halfa n0 0).
+; We will later convert this to n0/2.
+
+; ---------------------------------------------------------------------------
+; The Invariant -- The Only New Idea in this Note
+
+; Here is the new idea. I define the invariant for the program by
+; using defpun. The assertions are attached at the three cut points
+; and all other statements inherit the invariant of the next
+; statement.
+
+(defpun flat-inv (n0 th s)
+ (if (or (equal (pc (top-frame th s)) 0)
+ (equal (pc (top-frame th s)) 2)
+ (equal (pc (top-frame th s)) 18))
+ (flat-assertion n0 th s)
+ (flat-inv n0 th (step th s))))
+
+; In one sense, the next lemma is just a technical lemma to force
+; flat-inv to keep opening if it hasn't reached a cut point yet. But
+; in another sense, this lemma highlights the nice feature of this
+; approach. Suppose that in our function flat-assertion we had failed
+; to supply a cut point for some loop. Then we'll get a stack
+; overflow from the repeated indefinite application of this rewrite
+; rule. But we do not have to prove we've cut every loop, because the
+; flat-inv function is tail recursive and so was admitted by defpun.
+
+; In the past when I've used the classic inductive invariant approach
+; and used recursion in flat-inv to avoid an assertion at every pc, I
+; had to invent some kind of measure (``distance to the next cut
+; point'') to prove that I had cut every loop. That annoyed me
+; because in the classic inductive invariant approach that burden is
+; merely pragmatic -- you had to cut every loop or you couldn't
+; generate verification conditions. But you didn't have to prove you
+; had cut every loop. In my past attempts to mimic this, I had to
+; prove more stuff!
+
+(defthm flat-inv-opener
+ (implies (and (equal pc (pc (top-frame th s)))
+ (syntaxp (quotep pc))
+ (not (equal pc 0))
+ (not (equal pc 2))
+ (not (equal pc 18)))
+ (equal (flat-inv n0 th s)
+ (flat-inv n0 th (step th s)))))
+
+; ---------------------------------------------------------------------------
+; The Verification Conditions
+
+(defthm VC1
+ (implies (flat-pre-condition n0 n) (flat-loop-invariant n0 n 0)))
+
+
+(defthm VC2
+ (implies (and (flat-loop-invariant n0 n a)
+ (not (equal n 0)))
+ (flat-loop-invariant n0 (int-fix (- n 2)) (int-fix (+ 1 a)))))
+
+(defthm VC3
+ (implies (and (flat-loop-invariant N0 n a)
+ (EQUAL n 0))
+ (flat-post-condition N0 a)))
+
+(in-theory (disable flat-pre-condition
+ flat-loop-invariant
+ flat-post-condition))
+
+; ---------------------------------------------------------------------------
+; Using the VCs in the Operational Semantics
+
+; So here is the key theorem of the inductive invariant approach, showing
+; that inv is an invariant.
+
+(defthm flat-inv-step
+ (implies (flat-inv n0 th s)
+ (flat-inv n0 th (step th s))))
+
+; We can immediately conclude that flat-inv is an invariant under run,
+; as long as the only thread we step is th.
+
+(defun mono-threadedp (th sched)
+ (if (endp sched)
+ t
+ (and (equal th (car sched))
+ (mono-threadedp th (cdr sched)))))
+
+(defthm flat-inv-run
+ (implies (and (mono-threadedp th sched)
+ (flat-inv n0 th s))
+ (flat-inv n0 th (run sched s)))
+ :rule-classes nil
+ :hints (("Goal" :in-theory (e/d (run)(flat-inv-def)))))
+
+; And so we're done. If we plug in an initial state satisfying the
+; invariant we get a final state satisfying it. If the final state is
+; supposed to have pc 18, then we can read out what the invariant
+; tells us about that cut point.
+
+(defthm flat-main
+ (let ((s1 (run sched s0)))
+ (implies (and (intp n0)
+ (<= 0 n0)
+ (equal (pc (top-frame th s0)) 0)
+ (equal (locals (top-frame th s0)) (list n0 any))
+ (equal (program (top-frame th s0)) *flat-prog*)
+ (mono-threadedp th sched)
+ (equal (pc (top-frame th s1)) 18))
+ (and (evenp n0)
+ (equal (top (stack (top-frame th s1)))
+ (halfa n0 0)))))
+
+ :hints (("Goal" :use
+ (:instance flat-inv-run
+ (n0 n0)
+ (s s0)
+ (th th)
+ (sched sched))
+ :in-theory (enable flat-pre-condition flat-post-condition)))
+ :rule-classes nil)
+
+; ---------------------------------------------------------------------------
+; Getting Rid of the Semantic Function
+
+; Now, following our standard paradigm, we get rid of halfa and
+; introduce n/2 instead. There is nothing new here, but I have to
+; fight intp and int-fix.
+
+(defthm int-back
+ (implies (and (intp (+ a x))
+ (integerp a)
+ (<= 0 a)
+ (integerp x)
+ (<= 0 x)
+ (integerp y)
+ (<= 0 y)
+ (<= y x))
+ (intp (+ y a)))
+ :hints (("Goal" :in-theory (enable intp))))
+
+(defthm halfa-is-half
+ (implies (and (intp n)
+ (<= 0 n)
+ (evenp n)
+ (integerp a)
+ (<= 0 a)
+ (intp (+ (/ n 2) a)))
+ (equal (halfa n a)
+ (+ (/ n 2) a)))
+ :hints (("Goal" :in-theory (enable evenp))))
+
+(defthm intp-half-n
+ (implies (and (intp n)
+ (<= 0 n)
+ (evenp n))
+ (intp (* 1/2 n)))
+ :hints (("Goal" :in-theory (enable evenp intp))))
+
+; ---------------------------------------------------------------------------
+; The (Partial) Correctness Theorem for Half
+
+; The following theorem summarizes what we now know. Start with a a
+; state running *flat-prog* from pc 0 with initial n=n0 and run it
+; under an arbitrary mono-threaded schedule to get to s1. Suppose n0
+; is a non-negative int and the pc of s1 is 18.
+
+; Then we conclude that n0 is even and that the top of the stack is
+; n0/2.
+
+(defthm flat-is-partially-correct
+ (let ((s1 (run sched s0)))
+ (implies (and (intp n0)
+ (<= 0 n0)
+ (equal (pc (top-frame th s0)) 0)
+ (equal (locals (top-frame th s0)) (list n0 any))
+ (equal (program (top-frame th s0)) *flat-prog*)
+ (mono-threadedp th sched)
+ (equal (pc (top-frame th s1)) 18))
+ (and (evenp n0)
+ (equal (top (stack (top-frame th s1)))
+ (/ n0 2)))))
+ :rule-classes nil
+ :hints (("Goal"
+ :use ((:instance flat-main)))))
+
+; Note that at no point in this exercise have we counted instructions
+; or defined a clock or schedule generator.
+
+; ---------------------------------------------------------------------------
+; Dealing with Return
+
+(defconst *half-prog*
+ '((iconst_0) ; 0
+ (istore_1) ; 1 a := 0;
+ (iload_0) ; 2 top of loop:
+ (ifeq 14) ; 3 if n=0, goto 17;
+ (iload_1) ; 6
+ (iconst_1) ; 7
+ (iadd) ; 8
+ (istore_1) ; 9 a := a+1;
+ (iload_0) ;10
+ (iconst_2) ;11
+ (isub) ;12
+ (istore_0) ;13 n := n-2;
+ (goto -12) ;14 goto top of loop
+ (iload_1) ;17
+ (ireturn))) ;18 return a;
+
+(defun sdepth (stk)
+ (declare (xargs :hints (("Goal" :in-theory (enable pop)))))
+ (if (endp stk)
+ 0
+ (+ 1 (sdepth (pop stk)))))
+
+(defun half-assertion (n0 d0 th s)
+ (cond
+ ((< (sdepth (call-stack th s)) d0)
+ (let ((value (top (stack (top-frame th s)))))
+ (flat-post-condition n0 value)))
+ (t
+ (let ((n (nth 0 (locals (top-frame th s))))
+ (a (nth 1 (locals (top-frame th s)))))
+ (and (equal (sdepth (call-stack th s)) d0)
+ (equal (program (top-frame th s)) *half-prog*)
+ (equal (sync-flg (top-frame th s)) 'UNLOCKED)
+ (case (pc (top-frame th s))
+ (0 (flat-pre-condition n0 n))
+ (2 (flat-loop-invariant n0 n a))
+ (18 (let ((value (top (stack (top-frame th s)))))
+ (flat-post-condition n0 value)))
+ (otherwise nil)))))))
+
+(defpun half-inv (n0 d0 th s)
+ (if (or (< (sdepth (call-stack th s)) d0)
+ (equal (pc (top-frame th s)) 0)
+ (equal (pc (top-frame th s)) 2)
+ (equal (pc (top-frame th s)) 18))
+ (half-assertion n0 d0 th s)
+ (half-inv n0 d0 th (step th s))))
+
+(defthm half-inv-opener
+ (implies (and (equal pc (pc (top-frame th s)))
+ (syntaxp (quotep pc))
+ (not (equal pc 0))
+ (not (equal pc 2))
+ (not (equal pc 18)))
+ (equal (half-inv n0 d0 th s)
+ (if (< (sdepth (call-stack th s)) d0)
+ (half-assertion n0 d0 th s)
+ (half-inv n0 d0 th (step th s))))))
+
+(defthm half-inv-step
+ (implies (and (integerp d0)
+ (< 1 d0)
+ (<= d0 (sdepth (call-stack th s)))
+ (half-inv n0 d0 th s))
+ (half-inv n0 d0 th (step th s)))
+ :hints (("Goal" :in-theory (disable halfa-is-half))))
+
+(defun run-to-return (sched th d0 s)
+ (cond ((endp sched) s)
+ ((<= d0 (sdepth (call-stack th s)))
+ (run-to-return (cdr sched) th d0 (step (car sched) s)))
+ (t s)))
+
+(defthm half-inv-run-to-return
+ (implies (and (mono-threadedp th sched)
+ (integerp d0)
+ (< 1 d0)
+ (half-inv n0 d0 th s))
+ (half-inv n0 d0 th (run-to-return sched th d0 s)))
+ :rule-classes nil
+ :hints (("Goal" :in-theory (disable half-inv-def))))
+
+; And so we're done. If we plug in an initial state satisfying the
+; invariant we get a final state satisfying it. If the final state is
+; supposed to have pc 18, then we can read out what the invariant
+; tells us about that cut point.
+
+(defthm half-main
+ (let ((s1 (run-to-return sched th (sdepth (call-stack th s0)) s0)))
+ (implies (and (intp n0)
+ (<= 0 n0)
+ (equal (pc (top-frame th s0)) 0)
+ (equal (locals (top-frame th s0)) (list n0 any))
+ (equal (program (top-frame th s0)) *half-prog*)
+ (equal (sync-flg (top-frame th s0)) 'unlocked)
+ (< 1 (sdepth (call-stack th s0)))
+ (mono-threadedp th sched)
+ (< (sdepth (call-stack th s1))
+ (sdepth (call-stack th s0))))
+ (and (evenp n0)
+ (equal (top (stack (top-frame th s1)))
+ (halfa n0 0)))))
+ :hints (("Goal" :use
+ (:instance half-inv-run-to-return
+ (n0 n0)
+ (d0 (sdepth (call-stack th s0)))
+ (s s0)
+ (th th)
+ (sched sched))
+ :in-theory (enable flat-pre-condition
+ flat-post-condition)))
+ :rule-classes nil)
+
+(defthm half-partially-correct
+ (let ((s1 (run-to-return sched th (sdepth (call-stack th s0)) s0)))
+ (implies (and (intp n0)
+ (<= 0 n0)
+ (equal (pc (top-frame th s0)) 0)
+ (equal (locals (top-frame th s0)) (list n0 any))
+ (equal (program (top-frame th s0)) *half-prog*)
+ (equal (sync-flg (top-frame th s0)) 'unlocked)
+ (< 1 (sdepth (call-stack th s0)))
+ (mono-threadedp th sched)
+ (< (sdepth (call-stack th s1))
+ (sdepth (call-stack th s0))))
+ (and (evenp n0)
+ (equal (top (stack (top-frame th s1)))
+ (/ n0 2)))))
+ :hints (("Goal" :use half-main))
+ :rule-classes nil)
+
+; ---------------------------------------------------------------------------
+; Doing a Sum Program
+
+; To re-illustrate the same methodology, without worrying about
+; demonstrating that we can conclude things about the input if we're
+; told we terminate, here is a program that sums the ints from n0 down
+; to 0.
+
+(defconst *sum-prog*
+ ; We name local[0] n and local[1] a.
+ '((iconst_0) ; 0
+ (istore_1) ; 1 a := 0;
+ (iload_0) ; 2 top of loop:
+ (ifeq 14) ; 3 if n=0, goto 17;
+ (iload_0) ; 6
+ (iload_1) ; 7
+ (iadd) ; 8
+ (istore_1) ; 9 a := n+a;
+ (iload_0) ;10
+ (iconst_m1) ;11
+ (iadd) ;12
+ (istore_0) ;13 n := n-1;
+ (goto -12) ;14 goto top of loop
+ (iload_1) ;17
+ (ireturn))) ;18 return a;
+
+(defun suma (n a)
+ (if (zp n)
+ a
+ (suma (- n 1) (int-fix (+ n a)))))
+
+(defun sum-pre-condition (n0 n)
+ (and (equal n n0)
+ (intp n0)
+ (<= 0 n0)))
+
+(defun sum-loop-invariant (n0 n a)
+ (and (intp n0)
+ (intp n)
+ (<= 0 n)
+ (<= n n0)
+ (equal (suma n a)
+ (suma n0 0))))
+
+(defun sum-post-condition (n0 value)
+ (equal value (suma n0 0)))
+
+(defun sum-assertion (n0 d0 th s)
+ (cond ((< (sdepth (call-stack th s)) d0)
+ (let ((value (top (stack (top-frame th s)))))
+ (sum-post-condition n0 value)))
+ (t
+ (let ((n (nth 0 (locals (top-frame th s))))
+ (a (nth 1 (locals (top-frame th s)))))
+ (and (equal (sdepth (call-stack th s)) d0)
+ (equal (program (top-frame th s)) *sum-prog*)
+ (equal (sync-flg (top-frame th s)) 'UNLOCKED)
+ (case (pc (top-frame th s))
+ (0 (sum-pre-condition n0 n))
+ (2 (sum-loop-invariant n0 n a))
+ (18 (let ((value (top (stack (top-frame th s)))))
+ (sum-post-condition n0 value)))
+ (otherwise nil)))))))
+
+(defpun sum-inv (n0 d0 th s)
+ (if (or (< (sdepth (call-stack th s)) d0)
+ (equal (pc (top-frame th s)) 0)
+ (equal (pc (top-frame th s)) 2)
+ (equal (pc (top-frame th s)) 18))
+ (sum-assertion n0 d0 th s)
+ (sum-inv n0 d0 th (step th s))))
+
+(defthm sum-inv-opener
+ (implies (and (equal pc (pc (top-frame th s)))
+ (syntaxp (quotep pc))
+ (not (equal pc 0))
+ (not (equal pc 2))
+ (not (equal pc 18)))
+ (equal (sum-inv n0 d0 th s)
+ (if (< (sdepth (call-stack th s)) d0)
+ (sum-assertion n0 d0 th s)
+ (sum-inv n0 d0 th (step th s))))))
+
+(defthm sum-VC1
+ (implies (sum-pre-condition n0 n) (sum-loop-invariant n0 n 0)))
+
+(defthm sum-VC2
+ (implies (and (sum-loop-invariant n0 n a)
+ (not (equal n 0)))
+ (sum-loop-invariant n0 (int-fix (- n 1)) (int-fix (+ n a)))))
+
+(defthm sum-VC3
+ (implies (and (sum-loop-invariant N0 n a)
+ (EQUAL n 0))
+ (sum-post-condition N0 a)))
+
+(in-theory (disable sum-pre-condition
+ sum-loop-invariant
+ sum-post-condition))
+
+(defthm sum-inv-step
+ (implies (and (integerp d0)
+ (< 1 d0)
+ (<= d0 (sdepth (call-stack th s)))
+ (sum-inv n0 d0 th s))
+ (sum-inv n0 d0 th (step th s))))
+
+(defthm sum-inv-run-to-return
+ (implies (and (mono-threadedp th sched)
+ (integerp d0)
+ (< 1 d0)
+ (sum-inv n0 d0 th s))
+ (sum-inv n0 d0 th (run-to-return sched th d0 s)))
+ :rule-classes nil
+ :hints (("Goal" :in-theory (disable sum-inv-def))))
+
+(defthm sum-main
+ (let ((s1 (run-to-return sched th (sdepth (call-stack th s0)) s0)))
+ (implies (and (intp n0)
+ (<= 0 n0)
+ (equal (pc (top-frame th s0)) 0)
+ (equal (locals (top-frame th s0)) (list n0 any))
+ (equal (program (top-frame th s0)) *sum-prog*)
+ (equal (sync-flg (top-frame th s0)) 'unlocked)
+ (< 1 (sdepth (call-stack th s0)))
+ (mono-threadedp th sched)
+ (< (sdepth (call-stack th s1))
+ (sdepth (call-stack th s0))))
+ (equal (top (stack (top-frame th s1)))
+ (suma n0 0))))
+ :hints (("Goal" :use
+ (:instance sum-inv-run-to-return
+ (n0 n0)
+ (d0 (sdepth (call-stack th s0)))
+ (s s0)
+ (th th)
+ (sched sched))
+ :in-theory (enable sum-pre-condition
+ sum-post-condition)))
+ :rule-classes nil)
+
+; We don't bother to eliminate suma, though we could if we hacked around
+; with intp long enough!
+
+; ---------------------------------------------------------------------------
+; A Recursive Method
+
+; Now let's do recursive factorial. We'll bring in the clocked work
+; we have already done, just to have the *demo-state* etc.
+
+(include-book "demo")
+
+(defun ! (n)
+ (if (zp n)
+ 1
+ (* n (! (- n 1)))))
+
+; Here is the (redundant) definition of the program.
+
+(defconst *fact-def*
+ '("fact" (INT) NIL
+ (ILOAD_0) ;;; 0
+ (IFLE 12) ;;; 1
+ (ILOAD_0) ;;; 4
+ (ILOAD_0) ;;; 5
+ (ICONST_1) ;;; 6
+ (ISUB) ;;; 7
+ (INVOKESTATIC "Demo" "fact" 1) ;;; 8
+ (IMUL) ;;; 11
+ (IRETURN) ;;; 12
+ (ICONST_1) ;;; 13
+ (IRETURN))) ;;; 14
+
+; The following function recognizes the call stack (cs) of a call of
+; the "fact" method on n0. The function is not applied to the
+; top-most frame, because the constraints on the frame are so
+; pc-sensitive and the top-most frame may have "any" pc. So the
+; function actually recognizes the rest of the "fact" call stack.
+; Here is a picture of the entire call stack.
+
+; ------------------- top-most frame
+; pc: any
+; locals: (n) 5 <- suppose n=5
+; stack: any
+; program: fact prog
+; ------------------- caller-frame
+; pc: 11
+; locals: (n+1) 6 this is caller-frame 3
+; stack: (n+1)
+; program: fact prog
+; ------------------- caller-frame
+; pc: 11
+; locals: (n+2) 7 this is caller-frame 2
+; stack: (n+2)
+; program: fact prog
+; ------------------- caller-frame
+; ...
+; ------------------- caller-frame
+; pc: 11
+; locals: (n0) 8 <- suppose n0 = 8 ; this is caller frame 1
+; stack: (n0)
+; program: fact prog
+; ------------------- the frame below called fact on n0
+; ... this is caller frame 0
+
+; Note that there are n0-n fact caller frames. We number them from
+; n0-n down to 1. Caller frame 0 is actually the ``external'' entry
+; into fact on n0. We don't know (or care) whether fact or some other
+; program is running there. Let k be the number of the caller frame.
+; Then note that the value of n in that frame is n0-k+1.
+
+(defun fact-caller-framesp (cs n0 k)
+ (declare (xargs :measure (acl2-count k)))
+ (cond ((zp k) t)
+ ((and (equal (pc (top cs)) 11)
+ (equal (program (top cs)) (cdddr *fact-def*))
+ (equal (sync-flg (top cs)) 'UNLOCKED)
+ (intp (nth 0 (locals (top cs))))
+ (equal (+ n0 (- k)) (- (nth 0 (locals (top cs))) 1))
+ (equal (nth 0 (locals (top cs)))
+ (top (stack (top cs)))))
+ (fact-caller-framesp (pop cs) n0 (- k 1)))
+ (t nil)))
+
+(defun fact-assertion (n0 d0 th s)
+ (cond
+ ((< (sdepth (call-stack th s)) d0)
+ (equal (top (stack (top-frame th s)))
+ (int-fix (! n0))))
+ (t
+ (let ((n (nth 0 (locals (top-frame th s)))))
+ (and (equal (program (top-frame th s)) (cdddr *fact-def*))
+ (equal (lookup-method "fact" "Demo" (class-table s))
+ *fact-def*)
+ (equal (sync-flg (top-frame th s)) 'UNLOCKED)
+ (intp n0)
+ (intp n)
+ (<= 0 n)
+ (<= n n0)
+ (equal (sdepth (call-stack th s)) (+ d0 (- n0 n)))
+ (fact-caller-framesp (pop (call-stack th s)) n0 (- n0 n))
+ (case (pc (top-frame th s))
+ (0 t)
+ ((12 14) (equal (top (stack (top-frame th s)))
+ (int-fix (! n))))
+ (otherwise nil)))))))
+
+(defpun fact-inv (n0 d0 th s)
+ (if (or (< (sdepth (call-stack th s)) d0)
+ (equal (pc (top-frame th s)) 0)
+ (equal (pc (top-frame th s)) 12)
+ (equal (pc (top-frame th s)) 14))
+ (fact-assertion n0 d0 th s)
+ (fact-inv n0 d0 th (step th s))))
+
+(defthm fact-inv-opener
+ (implies (and (equal pc (pc (top-frame th s)))
+ (syntaxp (quotep pc))
+ (not (equal pc 0))
+ (not (equal pc 12))
+ (not (equal pc 14)))
+ (equal (fact-inv n0 d0 th s)
+ (if (< (sdepth (call-stack th s)) d0)
+ (fact-assertion n0 d0 th s)
+ (fact-inv n0 d0 th (step th s))))))
+
+; These next three lemmas are technical. The first two force
+; substitutions. The last opens the stack predicate when we're
+; returning and need to know what we're being told about the caller.
+
+(DEFTHM KB-HACK1
+ (IMPLIES
+ (AND
+ (FACT-CALLER-FRAMESP
+ (POP (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))
+ N0
+ (+ -1 N0 (- NNN)))
+ (EQUAL
+ NNN
+ (+ -1
+ (CAR (LOCALS (TOP (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))))))
+ (FACT-CALLER-FRAMESP
+ (POP (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))
+ N0
+ (+
+ N0
+ (-
+ (CAR (LOCALS (TOP (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))))))))
+
+(defthm kb-hack2
+ (implies
+ (and (integerp n)
+ (EQUAL
+ tos
+ (INT-FIX
+ (! (CAR (LOCALS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))))))
+
+ (EQUAL
+ (INT-FIX (* tos n))
+ (INT-FIX
+ (* (! (CAR (LOCALS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))))
+ n)))))
+
+(defthm fact-caller-framesp-opener-1
+ (implies (and (syntaxp
+ (equal cs
+ '(POP (CAR (CDR (ASSOC-EQUAL TH (THREAD-TABLE S)))))))
+ (EQUAL (PC (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) pc0)
+ (syntaxp (or (equal pc0 ''12) (equal pc0 ''14))))
+ (equal (fact-caller-framesp cs n0 k)
+ (COND ((ZP K) T)
+ ((AND (EQUAL (PC (TOP CS)) 11)
+ (EQUAL (PROGRAM (TOP CS))
+ (CDDDR *FACT-DEF*))
+ (EQUAL (SYNC-FLG (TOP CS)) 'UNLOCKED)
+ (INTP (NTH 0 (LOCALS (TOP CS))))
+ (EQUAL (+ N0 (- K))
+ (- (NTH 0 (LOCALS (TOP CS))) 1))
+ (EQUAL (NTH 0 (LOCALS (TOP CS)))
+ (TOP (STACK (TOP CS)))))
+ (FACT-CALLER-FRAMESP (POP CS)
+ N0 (- K 1)))
+ (T NIL)))))
+
+(defthm fact-inv-step
+ (implies (and (integerp d0)
+ (< 1 d0)
+ (<= d0 (sdepth (call-stack th s)))
+ (fact-inv n0 d0 th s))
+ (fact-inv n0 d0 th (step th s))))
+
+(defthm fact-inv-run-to-return
+ (implies (and (mono-threadedp th sched)
+ (integerp d0)
+ (< 1 d0)
+ (fact-inv n0 d0 th s))
+ (fact-inv n0 d0 th (run-to-return sched th d0 s)))
+ :rule-classes nil
+ :hints (("Goal" :in-theory (disable fact-inv-def))))
+
+; Here is the main theorem. It opens by letting s1 be a run-to-return
+; of s0. That particular call runs s0 with an abitrarily long
+; schedule, sched. Note that run-to-return does not always return a
+; state that has returned to a shorter call-stack depth -- if the
+; schedule is exhausted before that happens, the final state may still
+; be as deep or deeper than the initial state. In any case, s0 is the
+; initial state and s1 is the final state.
+
+; Now let's read the hypotheses of the implication. There are five
+; blocks of hypotheses. The first says that n0 is a positive intp.
+; The second says that the top-frame of thread th of s0 is a call of
+; our "fact" method on n0. The third says that the depth of the
+; call-stack of thread th is greater than 1. That means there is a
+; frame under the call of "fact". We will call that frame the
+; ``caller's frame.'' Of course, if s1 has a shorter call-stack than
+; s0, then the caller's frame will be its top-frame, since
+; run-to-return stops as soon as we've returned to that depth. The
+; fourth says the schedule consists of nothing but th steps. Note
+; that otherwise we say nothing about the schedule -- it may be
+; arbitrarily long. The fifth block says that the depth of the call
+; stack of s1 is less than that of s0, so we know the initial state
+; did run long enough to return and hence, the caller's frame is the
+; top-frame of s1.
+
+; Then the conclusion is that (int-fix (! n0)) is on top of
+; the stack of the caller's frame.
+
+(defthm fact-main
+ (let ((s1 (run-to-return sched th (sdepth (call-stack th s0)) s0)))
+ (implies (and (intp n0)
+ (<= 0 n0)
+
+ (equal (pc (top-frame th s0)) 0)
+ (equal (locals (top-frame th s0)) (list n0))
+ (equal (program (top-frame th s0))
+ (cdddr *fact-def*))
+ (equal (sync-flg (top-frame th s0)) 'unlocked)
+ (equal (lookup-method "fact" "Demo" (class-table s0))
+ *fact-def*)
+
+ (< 1 (sdepth (call-stack th s0)))
+
+ (mono-threadedp th sched)
+
+ (< (sdepth (call-stack th s1))
+ (sdepth (call-stack th s0))))
+ (equal (top (stack (top-frame th s1)))
+ (int-fix (! n0)))))
+
+ :hints (("Goal"
+ :use
+ (:instance fact-inv-run-to-return
+ (n0 n0)
+ (d0 (sdepth (call-stack th s0)))
+ (s s0)
+ (th th)
+ (sched sched))))
+ :rule-classes nil)
+
+; ---------------------------------------------------------------------------
+; The Basic Relation Between Run-to-Return and Run
+
+(defun sched-to-return (sched th d0 s)
+ (cond ((endp sched) sched)
+ ((<= d0 (sdepth (call-stack th s)))
+ (sched-to-return (cdr sched) th d0 (step (car sched) s)))
+ (t sched)))
+
+(defthm run-to-return-v-run
+ (equal (run sched s)
+ (run (sched-to-return sched th d0 s)
+ (run-to-return sched th d0 s)))
+ :rule-classes nil)
+
+; I need to develop the compositional rules.
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-29 22:06:38 +0000