#|
(DEFPKG "M4"
  (set-difference-equal
   (union-eq '(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 REVERSE STEP ++)))

(certify-book "m4" 1)

|#

; Notes:
; Do JVM objects have an mcount field?  Can the user set them with
; (putfield "Object" "mcount")?  This machine allows that, which
; can screw up monitors.


; ----------------------------------------------------------------------------
; Abstract Machine 4  - by George Porter and J Moore

(in-package "M4")

; -----------------------------------------------------------------------------
; Utilities

(defun push (obj stack) (cons obj stack))
(defun top (stack) (car stack))
(defun pop (stack) (cdr stack))

; Imported from ACL2.

#|
(defun assoc-equal (x alist)
  (cond ((endp alist) nil)
        ((equal x (car (car alist)))
         (car alist))
        (t (assoc-equal x (cdr alist)))))
|#

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

; Imported from ACL2
#|
(defun nth (i lst)
  (if (zp i)
      (car lst)
    (nth (- i 1) (cdr lst))))

(defun zp (i) 
  (if (integerp i) (<= i 0) t))
|#

(defun reverse (x)
  (if (consp x)
      (append (reverse (cdr x)) (list (car x)))
    nil))


; -----------------------------------------------------------------------------
; 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 call-stack (s th)
  (car (binding th (thread-table s))))

(defun call-stack-status (s th)
  (cadr (binding th (thread-table s))))

(defun call-stack-rref (tt th)
  (caddr (binding th tt)))

; -----------------------------------------------------------------------------
; 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 page xxx]

(defun make-class-decl (name superclasses fields methods)
  (list name superclasses fields methods))

(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-methods (dcl)
  (nth 3 dcl))

(defun base-class-def ()
   (list (make-class-decl "Object"
			  nil
			  '("monitor" "mcount" "wait-set")
			  '(("start" () nil ())
			    ("stop" () nil ())))
	 (make-class-decl "Thread"
			  '("Object")
			  nil
			  '(("run" () nil
			     (return))))))

(defun make-class-def (list-of-class-decls)
   (append (base-class-def) list-of-class-decls))

; -----------------------------------------------------------------------------
; Thread Tables
;
; A "thread table" might be used to represent threads in m4.  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 coorespond 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 modify-tt (th call-stack status tt)
  (bind th (list call-stack status (call-stack-rref tt th)) tt))

(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 "Thread" supers)
	   (in-list "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 "Object" instance))
         (new-mcount (+ 1 (binding "mcount" obj-fields)))
	 (new-obj-fields
	    (bind "monitor" th
	       (bind "mcount" new-mcount obj-fields)))
	 (new-object (bind "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 "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 "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 "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 "Object" instance))
         (monitor (binding "monitor" obj-fields)))
      (equal monitor th)))

; -----------------------------------------------------------------------------
; Frames

(defun make-frame (pc locals stack program sync-flg)
  (list pc locals stack program sync-flg))

(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 top-frame (s th) (top (call-stack s th)))


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

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

; -----------------------------------------------------------------------------
; (PUSH const) Instruction

(defun execute-PUSH (inst s th)
  (make-state
   (modify-tt th
              (push (make-frame (+ 1 (pc (top-frame s th)))
                     (locals (top-frame s th))
                     (push (arg1 inst)
                           (stack (top-frame s th)))
                     (program (top-frame s th))
		     (sync-flg (top-frame s th)))
                 (pop (call-stack s th)))
	      'SCHEDULED
	      (thread-table s))
   (heap s)
   (class-table s)))

; -----------------------------------------------------------------------------
; (POP) Instruction

(defun execute-POP (inst s th)
  (declare (ignore inst))
  (make-state
   (modify-tt th
              (push (make-frame (+ 1 (pc (top-frame s th)))
                     (locals (top-frame s th))
                     (pop (stack (top-frame s th)))
                     (program (top-frame s th))
		     (sync-flg (top-frame s th)))
                  (pop (call-stack s th)))
	      'SCHEDULED
	      (thread-table s))
   (heap s)
   (class-table s)))

; -----------------------------------------------------------------------------
; (LOAD var) Instruction

(defun execute-LOAD (inst s th)
  (make-state
   (modify-tt th
              (push (make-frame (+ 1 (pc (top-frame s th)))
                     (locals (top-frame s th))
                     (push (binding (arg1 inst)
                                    (locals (top-frame s th)))
                           (stack (top-frame s th)))
                     (program (top-frame s th))
		     (sync-flg (top-frame s th)))
                  (pop (call-stack s th)))
	      'SCHEDULED
	      (thread-table s))
   (heap s)
   (class-table s)))

; -----------------------------------------------------------------------------
; (STORE var) Instruction

(defun execute-STORE (inst s th)
  (make-state
   (modify-tt th
              (push (make-frame (+ 1 (pc (top-frame s th)))
                     (bind (arg1 inst)
                           (top (stack (top-frame s th)))
                           (locals (top-frame s th)))
                     (pop (stack (top-frame s th)))
                     (program (top-frame s th))
		     (sync-flg (top-frame s th)))
                  (pop (call-stack s th)))
	      'SCHEDULED
	      (thread-table s))
   (heap s)
   (class-table s)))

; -----------------------------------------------------------------------------
; (ADD) Instruction

(defun execute-ADD (inst s th)
  (declare (ignore inst))
  (make-state
   (modify-tt th
              (push (make-frame (+ 1 (pc (top-frame s th)))
                     (locals (top-frame s th))
                     (push (+ (top (pop (stack (top-frame s th))))
                              (top (stack (top-frame s th))))
                           (pop (pop (stack (top-frame s th)))))
                     (program (top-frame s th))
		     (sync-flg (top-frame s th)))
                  (pop (call-stack s th)))
	      'SCHEDULED
	      (thread-table s))
   (heap s)
   (class-table s)))

; -----------------------------------------------------------------------------
; (SUB) Instruction

(defun execute-SUB (inst s th)
  (declare (ignore inst))
  (make-state
   (modify-tt th
              (push (make-frame (+ 1 (pc (top-frame s th)))
                     (locals (top-frame s th))
                     (push (- (top (pop (stack (top-frame s th))))
                              (top (stack (top-frame s th))))
                           (pop (pop (stack (top-frame s th)))))
                     (program (top-frame s th))
		     (sync-flg (top-frame s th)))
                  (pop (call-stack s th)))
	      'SCHEDULED
	      (thread-table s))
   (heap s)
   (class-table s)))

; -----------------------------------------------------------------------------
; (MUL) Instruction

(defun execute-MUL (inst s th)
  (declare (ignore inst))
  (make-state
   (modify-tt th
              (push (make-frame (+ 1 (pc (top-frame s th)))
                     (locals (top-frame s th))
                     (push (* (top (pop (stack (top-frame s th))))
                              (top (stack (top-frame s th))))
                           (pop (pop (stack (top-frame s th)))))
                     (program (top-frame s th))
		     (sync-flg (top-frame s th)))
                  (pop (call-stack s th)))
	      'SCHEDULED
	      (thread-table s))
   (heap s)
   (class-table s)))

; -----------------------------------------------------------------------------
; (GOTO pc) Instruction

(defun execute-GOTO (inst s th)
  (make-state
   (modify-tt th
              (push (make-frame (+ (arg1 inst) (pc (top-frame s th)))
                     (locals (top-frame s th))
                     (stack (top-frame s th))
                     (program (top-frame s th))
		     (sync-flg (top-frame s th)))
                  (pop (call-stack s th)))
              'SCHEDULED
	      (thread-table s))
   (heap s)
   (class-table s)))

; -----------------------------------------------------------------------------
; (IFEQ pc) Instruction

(defun execute-IFEQ (inst s th)
  (make-state
   (modify-tt th
              (push (make-frame (if (equal (top (stack (top-frame s th))) 0)
                         (+ (arg1 inst) (pc (top-frame s th)))
                       (+ 1 (pc (top-frame s th))))
                     (locals (top-frame s th)) (pop (stack (top-frame s th)))
                     (program (top-frame s th))
		     (sync-flg (top-frame s th)))
                  (pop (call-stack s th)))
	      'SCHEDULED
	      (thread-table s))
   (heap s)
   (class-table s)))

; -----------------------------------------------------------------------------
; (IFGT pc) Instruction

(defun execute-IFGT (inst s th)
  (make-state
   (modify-tt th
              (push (make-frame (if (> (top (stack (top-frame s th))) 0)
                         (+ (arg1 inst) (pc (top-frame s th)))
                       (+ 1 (pc (top-frame s th))))
                     (locals (top-frame s th))
                     (pop (stack (top-frame s th)))
                     (program (top-frame s th))
		     (sync-flg (top-frame s th)))
                  (pop (call-stack s th)))
	      'SCHEDULED
	      (thread-table s))
   (heap s)
   (class-table s)))

; -----------------------------------------------------------------------------
; (IFLT pc) Instruction

(defun execute-IFLT (inst s th)
  (make-state
   (modify-tt th
              (push (make-frame (if (< (top (stack (top-frame s th))) 0)
                         (+ (arg1 inst) (pc (top-frame s th)))
                       (+ 1 (pc (top-frame s th))))
                     (locals (top-frame s th))
                     (pop (stack (top-frame s th)))
                     (program (top-frame s th))
		     (sync-flg (top-frame s th)))
                  (pop (call-stack s th)))
	      'SCHEDULED
	      (thread-table s))
   (heap s)
   (class-table s)))

; -----------------------------------------------------------------------------
; (GETFIELD "class" "field") Instruction

(defun deref (ref heap)
  (binding (cadr ref) heap))

(defun field-value (class-name field-name instance)
  (binding field-name
           (binding class-name instance)))

(defun execute-GETFIELD (inst s th)
  (let* ((class-name (arg1 inst))
         (field-name (arg2 inst))
         (instance (deref (top (stack (top-frame s th))) (heap s)))
         (field-value (field-value class-name field-name instance)))
    (make-state
     (modify-tt th
                (push (make-frame (+ 1 (pc (top-frame s th)))
		       (locals (top-frame s th))
		       (push field-value
			     (pop (stack (top-frame s th))))
		       (program (top-frame s th))
		       (sync-flg (top-frame s th)))
	            (pop (call-stack s th)))
		'SCHEDULED
		(thread-table s))
     (heap s)
     (class-table s))))

; -----------------------------------------------------------------------------
; (PUTFIELD "class" "field") 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-PUTFIELD (inst s th)
  (let* ((class-name (arg1 inst))
         (field-name (arg2 inst))
         (value (top (stack (top-frame s th))))
         (instance (deref (top (pop (stack (top-frame s th)))) (heap s)))
         (address (cadr (top (pop (stack (top-frame s th)))))))
        (make-state
         (modify-tt th
	            (push (make-frame (+ 1 (pc (top-frame s th)))
                           (locals (top-frame s th))
                           (pop (pop (stack (top-frame s th))))
                           (program (top-frame s th))
		           (sync-flg (top-frame s th)))
                        (pop (call-stack s th)))
	            'SCHEDULED
		    (thread-table s))
         (bind address
               (set-instance-field class-name field-name value instance)
               (heap s))
         (class-table s))))

; -----------------------------------------------------------------------------
; (INVOKEVIRTUAL "class" "name" n) Instruction

(defun bind-formals (rformals stack)
  (if (endp rformals)
      nil
    (cons (cons (car rformals) (top stack))
          (bind-formals (cdr rformals) (pop stack)))))

(defun popn (n stack)
  (if (zp n)
      stack
    (popn (- n 1) (pop stack))))

(defun class-name-of-ref (ref heap)
  (car (car (deref ref heap))))

(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-INVOKEVIRTUAL (inst s th)
  (let* ((method-name (arg2 inst))
         (nformals (arg3 inst))
         (obj-ref (nth nformals (stack (top-frame s th))))
	 (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)))
         (vars (cons 'this (method-formals closest-method)))
         (prog (method-program closest-method))
	 (stepped-cs (push (make-frame (+ 1 (pc (top-frame s th)))
	                           (locals (top-frame s th))
				   (popn (len vars)
				         (stack (top-frame s th)))
			           (program (top-frame s th))
		                   (sync-flg (top-frame s th)))
                       (pop (call-stack s th))))
	 (tThread (rrefToThread obj-ref (thread-table s))))
      (if (method-isNative? closest-method)
	  (cond ((equal method-name "start")
		  (make-state
		    (modify-tt
		      th
		      stepped-cs
		      'SCHEDULED
		      (schedule-thread tThread (thread-table s)))
		    (heap s)
		    (class-table s)))

		((equal method-name "stop")
		  (make-state
		    (modify-tt
		      th
		      stepped-cs 'SCHEDULED
		      (unschedule-thread tThread (thread-table s)))
		    (heap s)
		    (class-table s)))
                (t s))

	  (cond ((and (method-sync closest-method)
		      (objectLockable? instance th))
		  (make-state
		    (modify-tt
		      th
		      (push 
		         (make-frame 0
				     (reverse
				      (bind-formals (reverse vars)
						    (stack (top-frame s th))))
				     nil
				     prog
				     'LOCKED)
			 stepped-cs)
		      'SCHEDULED
		      (thread-table s))
		    (lock-object th obj-ref (heap s))
		    (class-table s)))

		((method-sync closest-method)
		  s)

		(t
		  (make-state
		    (modify-tt
		      th
		      (push 
			 (make-frame 0
				     (reverse
				      (bind-formals (reverse vars)
						    (stack (top-frame s th))))
				     nil
				     prog
				     'UNLOCKED)
			 stepped-cs)
		      'SCHEDULED
		      (thread-table s))
		    (heap s)
		    (class-table s)))))))

; -----------------------------------------------------------------------------
; (NEW "class") Instruction

(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 execute-NEW (inst s th)
  (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)))
	 (modified-thread-table
		 (modify-tt th
			    (push (make-frame (+ 1 (pc (top-frame s th)))
					      (locals (top-frame s th))
					      (push (list 'REF new-address)
						  (stack (top-frame s th)))
					      (program (top-frame s th))
		                              (sync-flg (top-frame s th)))
				  (pop (call-stack s th)))
			    'SCHEDULED
			    (thread-table s))))
    (if (isThreadObject? class-name class-table)
      ; We need to create a new thread here
      (make-state
       (addto-tt
	 (push
	   (make-frame 0
		       (list (cons 'this (list 'REF new-address)))
		       nil
		       prog
		       'UNLOCKED)
	   nil)
	 'UNSCHEDULED
	 (list 'REF new-address)
	 modified-thread-table)
       (bind new-address new-object (heap s))
       (class-table s))

      ; We create an object in the heap the old way
      (make-state
       modified-thread-table
       (bind new-address new-object (heap s))
       (class-table s))
       )))


; -----------------------------------------------------------------------------
; (RETURN) Instruction - Void Return

(defun execute-RETURN (inst s th)
  (declare (ignore inst))
  (let* ((caller-frame (top (pop (call-stack s th))))
         (obj-ref (binding 'THIS (locals (top-frame s th))))
         (new-cs (modify-tt th
                            (push (make-frame (pc caller-frame)
                                              (locals caller-frame)
                                              (stack caller-frame)
                                              (program caller-frame)
                                              (sync-flg caller-frame))
                                  (pop (pop (call-stack s th))))
                            'SCHEDULED
                            (thread-table s))))
    (if (equal (sync-flg (top-frame s th))
               'LOCKED)
	(make-state
         new-cs
         (unlock-object th obj-ref (heap s))
         (class-table s))
      (make-state
       new-cs
       (heap s)
       (class-table s)))))

; -----------------------------------------------------------------------------
; (XRETURN) Instruction - return 1 thing of arbitrary type

(defun execute-XRETURN (inst s th)
  (declare (ignore inst))
  (let* ((val (top (stack (top-frame s th))))
         (caller-frame (top (pop (call-stack s th))))
         (obj-ref (binding 'THIS (locals (top-frame s th))))
         (new-cs (modify-tt th
                            (push (make-frame (pc caller-frame)
                                              (locals caller-frame)
                                              (push val (stack caller-frame))
                                              (program caller-frame)
                                              (sync-flg caller-frame))
                                  (pop (pop (call-stack s th))))
                            'SCHEDULED
                            (thread-table s))))
    (if (equal (sync-flg (top-frame s th))
               'LOCKED)
	(make-state
         new-cs
         (unlock-object th obj-ref (heap s))
         (class-table s))
      (make-state
       new-cs
       (heap s)
       (class-table s)))))


; -----------------------------------------------------------------------------
; (MONITORENTER) Instruction

(defun execute-MONITORENTER (inst s th)
; George:  I added this declare.
  (declare (ignore inst))
  (let* ((obj-ref (top (stack (top-frame s th))))
         (instance (deref obj-ref (heap s)))
	 (stepped-cs (push (make-frame (+ 1 (pc (top-frame s th)))
			 (locals (top-frame s th))
			 (pop (stack (top-frame s th)))
			 (program (top-frame s th))
		         (sync-flg (top-frame s th)))
		      (pop (call-stack s th)))))
    (if (objectLockable? instance th)
	(make-state
	 (modify-tt th
		    stepped-cs
		    'SCHEDULED
		    (thread-table s))
	 (lock-object th obj-ref (heap s))
	 (class-table s))

	s)))

; -----------------------------------------------------------------------------
; (MONITOREXIT) Instruction

(defun execute-MONITOREXIT (inst s th)
; George:  I added this declare.
  (declare (ignore inst))
  (let* ((obj-ref (top (stack (top-frame s th))))
         (instance (deref obj-ref (heap s)))
	 (stepped-cs (push (make-frame (+ 1 (pc (top-frame s th)))
			 (locals (top-frame s th))
			 (pop (stack (top-frame s th)))
			 (program (top-frame s th))
		         (sync-flg (top-frame s th)))
		      (pop (call-stack s th)))))
    (if (objectUnLockable? instance th)
	(make-state
	 (modify-tt th
		    stepped-cs
		    'SCHEDULED
		    (thread-table s))
	 (unlock-object th obj-ref (heap s))
	 (class-table s))

	s)))

; -----------------------------------------------------------------------------
; Putting it all together

(defun next-inst (s th)
  (nth (pc (top-frame s th))
       (program (top-frame s th)))) 

(defun do-inst (inst s th)
  (case (op-code inst)
    (PUSH           (execute-PUSH inst s th))
    (POP            (execute-POP  inst s th))
    (LOAD           (execute-LOAD inst s th))
    (STORE          (execute-STORE inst s th))
    (ADD            (execute-ADD inst s th))
    (SUB            (execute-SUB inst s th))    
    (MUL            (execute-MUL inst s th))
    (GOTO           (execute-GOTO inst s th))
    (IFEQ           (execute-IFEQ inst s th))
    (IFLT           (execute-IFLT inst s th))
    (IFGT           (execute-IFGT inst s th))
    (INVOKEVIRTUAL  (execute-INVOKEVIRTUAL inst s th))
    (RETURN         (execute-RETURN inst s th))
    (XRETURN        (execute-XRETURN inst s th))
    (NEW            (execute-NEW inst s th))
    (GETFIELD       (execute-GETFIELD inst s th))
    (PUTFIELD       (execute-PUTFIELD inst s th))
    (MONITORENTER   (execute-MONITORENTER inst s th))
    (MONITOREXIT    (execute-MONITOREXIT inst s th))
    (HALT           s)
    (otherwise s)))

(defun step (s th)
  (if (equal (call-stack-status s th) 'SCHEDULED)
    (do-inst (next-inst s th) s th)
    s))

(defun run (sched s)
  (if (endp sched)
      s
    (run (cdr sched) (step s (car sched)))))

; -----------------------------------------------------------------------------
; An Example of M4

(defun the-class-table ()
  (list (make-class-decl "Object" nil nil nil)
        (make-class-decl "Alpha"
                         '("Object")
                         '("x" "y")
                         '(("chgx" (dx) t
                            (load this)
                            (load this)
                            (getfield "Alpha" "x")  
                            (load dx)
                            (add)
                            (putfield "Alpha" "x")  ; this.x = this.x + dx;
                            (push 1)
                            (xreturn))                  ; return 1;
                           ("chgy" (dy) nil 
                            (load this)
                            (load this)
                            (getfield "Alpha" "y")
                            (load dy)
                            (add)
                            (putfield "Alpha" "y")  ; this.y = this.y + dy;
                            (push 1)
                            (xreturn))))                ; return 1;
        (make-class-decl "Beta"
                         '("Alpha" "Object")
                         '("x")
                         '(("chgx" (xx) t
                            (load this)
                            (load this)
                            (getfield "Beta" "x")
                            (load xx)
                            (mul)
                            (putfield "Beta" "x")  ; this.x = this.x * xx
                            (push 1)
                            (xreturn))))))             ; return 1;


(defun main-program ()
  '((new "Alpha")
    (store a)                                ; Alpha a = new Alpha();
    (new "Beta")
    (store b)                                ; Alpha b = new Beta();
    (load a)
    (push 1)
    (putfield "Alpha" "x")                   ; a.x = 1;
    (load a)
    (push 2)
    (putfield "Alpha" "y")                   ; a.y = 2;
    (load b)
    (push 3)
    (putfield "Beta" "x")                    ; b.x = 3;
    (load b)
    (push 4)
    (putfield "Alpha" "x")                   ; ((Alpha)b).x = 4;
    (load b)
    (push 5)
    (putfield "Alpha" "y")                   ; b.y = 5;
    (load a)
    (push 6)
    (invokevirtual "Alpha" "chgx" 1)         ; a.chgx(6);
    (pop)
    (load b)
    (push 7)
    (invokevirtual "Alpha" "chgx" 1)         ; b.chgx(7);
    (pop)
    (load b)
    (push 8)
    (invokevirtual "Alpha" "chgy" 1)         ; b.chgy(8);
    (pop)))

(defun s0 ()
  (make-state
   (push (make-frame 0
                     '((a . nil) (b . nil))
                     nil
                     (main-program)
		     'UNLOCKED)
         nil)
   nil
   (the-class-table)))


; Here, is the factorial program written as a recursive instance method.

; Here is the Alpha class in Java
; class Alpha {
; public int fact(int n){
;  if (n<=0) return 1;
;    else return n*fact(n-1);}
; 
;  public static void main(String[] args){
;  Alpha obj = new Alpha();
;  int n = Integer.parseInt(args[0],10);
;  System.out.println(obj.fact(n));}
;  }

; Here is the our fact byte code, as presented in M4.lisp and the javap -c
; output for the class above.

(defconst *fact-def*
 '("fact" (n) nil               ; Method int fact(int)
   (load n)                     ;    0 iload_1
   (ifgt 3)                     ;    1 ifgt 6
   (push 1)                     ;    4 iconst_1
   (xreturn)                    ;    5 ireturn
   (load n)                     ;    6 iload_1
   (load this)                  ;    7 aload_0
   (load n)                     ;    8 iload_1
   (push 1)                     ;    9 iconst_1
   (sub)                        ;   10 isub
   (invokevirtual "Alpha" "fact" 1)
                                ;   11 invokevirtual #8 <Method int fact(int)>
   (mul)                        ;   14 imul
   (xreturn)))                  ;   15 ireturn

(defconst *Alpha-class-table*
  (make-class-def 
   (list (make-class-decl "Alpha"
                          '("Object")
                          '()
                          (list *fact-def*)))))
  

(defun sfact ()
  (make-state
   (make-tt (push (make-frame 0
                              nil
                              nil
                              '((new "Alpha")
                                (push 3)
                                (invokevirtual "Alpha" "fact" 1))
                              'UNLOCKED)
                  nil))
   nil
   *Alpha-class-table*))

(defun fact (n)
  (if (zp n) 1 (* n (fact (- n 1)))))


; Here is an example that illustrates method resolution.
(defun yet-another-class-table ()
  (make-class-def 
     (list 
	(make-class-decl "Alpha"
                         '("Object")
                         '("x")
                         '(("hitx" () t
                            (load this)
                            (push 1)
                            (putfield "Alpha" "x")
                            (load this)
                            (xreturn))))
        (make-class-decl "Delta"
                         '("Thread" "Object")
                         '("x" "objref")
                         '(("hitx-sync" () t
                            (load this)
                            (push 1)
                            (putfield "Delta" "x")
                            (load this)
                            (xreturn))
			   ("hitx" () nil
                            (load this)
                            (push 1)
                            (putfield "Delta" "x")
                            (load this)
                            (xreturn))
                         ("run" (n) nil
			    (load this)
			    (getfield "Delta" "objref")
			    (invokevirtual "Delta" "hitx" 0)
			    (load this)
			    (getfield "Delta" "objref")
			    (invokevirtual "Delta" "hitx-sync" 0)
			    (load this)
			    (getfield "Delta" "objref")
			    (monitorenter)
			    (load this)
			    (getfield "Delta" "objref")
			    (monitorexit)
			    (halt))
                         ("setref" (r) nil
			    (load this)
			    (load r)
			    (putfield "Delta" "objref")
                            (xreturn))
			   ))
        (make-class-decl "Beta"
                         '("Alpha" "Object")
                         '("x")
                         '(("hitx" () t
                            (load this)
                            (push 2) (putfield "Beta" "x")
                            (load this)
                            (xreturn))
                           ("start" (n) nil
			    (load this)
			    (getfield "Delta" "objref")
			    (halt))
                           ("meth" (b) nil
                            (load b)
                            (invokevirtual "Beta" "hitx" 0)
                            (xreturn)))))))

; A very basic state used for testing, mostly

(defun simple-main-program ()
  '((push 1)
    (push 2)
    (add)
    (new "Alpha")
    (invokevirtual "Alpha" "hitx" 0) (halt)
   ))

(defun ss ()
  (make-state
   (make-tt (push 
   	       (make-frame 0
		           '((a . nil) (b . nil))
			   nil
			   (simple-main-program)
			   'UNLOCKED)
	     nil))
   nil
   (yet-another-class-table)))

; Another simple state, demonstrating threads

(defun simple-main-thread-program ()
  '((new "Delta")
    (store a)
    (load a)
    (load a)
    (invokevirtual "Delta" "setref" 1)
    (load a)
    (invokevirtual "Delta" "start" 0)
    (load a)
    (monitorenter)
    (load a)
    (monitorexit)
    (load a)
    (invokevirtual "Delta" "hitx-sync" 0)
    (load a)
    (invokevirtual "Delta" "hitx" 0)
    (halt)
   ))

(defun ssth ()
  (make-state
   (make-tt (push 
   	       (make-frame 0
		           '((a . nil) (b . nil))
			   nil
			   (simple-main-thread-program)
			   'UNLOCKED)
	     nil))
   nil
   (yet-another-class-table)))

(defun ack2 (num n lst)
  (if (zp n)
      lst
      (cons num (ack2 num (- n 1) lst))))

(defun ack0 (n)
  (ack2 0 n nil))
(defun ack1 (n)
  (ack2 1 n nil))

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

; George:  That's the end of your m4.lisp.

(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)
                      (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 "~%M4 Simulator.~%~%")
   (sim-loop s acl2::state)))