; The M2 Virtual Machine
; Copyright (C) 2004  J Strother Moore,
;               University of Texas at Austin

; This program is free software; you can redistribute it and/or 
; modify it under the terms of the GNU General Public License as
; published by the Free Software Foundation; either version 2 of
; the License, or (at your option) any later version.

; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
; GNU General Public License for more details.

; You should have received a copy of the GNU General Public
; License along with this program; if not, write to the Free 
; Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139,
; USA.

; Written by: J Strother Moore
; email:      Moore@cs.utexas.edu
; Department of Computer Sciences
; University of Texas at Austin
; Austin, TX 78712-1188 U.S.A.

; Modified by: John Cowles
; email:       cowles@uwyo.edu
; Department of Computer Science
; University of Wyoming
; Laramie, WY 82071 U.S.A.
;==============================================================
; This file is a certified book that contains the definition of 
; m2.

; M2 is similar to M1 except that we now have the heap, classes
; and invokevirtual.

; Instructions

; To certify this book, make sure it is on a directory on which 
; you have write permission, fire up ACL2 while connected to that
; directory, and then execute the following two events.

#|
(defpkg "M2"
  (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 "m2" 1)
|#

(in-package "M2")

; Utilities

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

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

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

; M2 States
(defun make-state (call-stack heap class-table)
  (list call-stack heap class-table))

(defun call-stack (s) (nth 0 s))
(defun heap (s) (nth 1 s))
(defun class-table (s) (nth 2 s))

; Frames
(defun top-frame (s) (top (call-stack 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 make-frame (pc locals stack program sync-flg)
  (list pc locals stack program sync-flg))

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

; Class Declarations
(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))

; This is a base set of classes that are 'built in' to M2 states
(defun base-class-def ()
   (list (make-class-decl "Object"
                          nil
                          '("monitor" "mcount" "wait-set")
                          nil)
         (make-class-decl "Thread"
                          '("Object")
                          nil
                          '(("run" () nil
                             (return))
			    ("start" () nil ())
			    ("stop" () nil ())))))

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

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

; 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 (s &rest args)
  (list 'make-state
        (cond ((suppliedp :call-stack args)
               (actual :call-stack args))
              ((or (suppliedp :pc args)
                   (suppliedp :locals args)
                   (suppliedp :stack args)
                   (suppliedp :program args)
		   (suppliedp :sync-flg args))
               (list 'push
                     (list 'make-frame
                           (if (suppliedp :pc args)
                               (actual :pc args)
                             (list 'pc (list 'top-frame s)))
                           (if (suppliedp :locals args)
                               (actual :locals args)
                             (list 'locals (list 'top-frame s)))
                           (if (suppliedp :stack args)
                               (actual :stack args)
                             (list 'stack (list 'top-frame s)))
                           (if (suppliedp :program args)
                               (actual :program args)
                             (list 'program (list 'top-frame s)))
			   (if (suppliedp :sync-flg args)
			       (actual :sync-flg args)
			     (list 'sync-flg (list 'top-frame s))))
                     (list 'pop (list 'call-stack s))))
              (t (list 'call-stack s)))
        (if (suppliedp :heap args)
            (actual :heap args)
          (list 'heap s))
        (if (suppliedp :class-table args)
            (actual :class-table args)
          (list 'class-table s))))

; (PUSH const)
(defun execute-PUSH (inst s)
  (modify s
          :pc (+ 1 (pc (top-frame s)))
          :stack (push (arg1 inst) (stack (top-frame s)))))

; (POP)
(defun execute-POP (inst s)
  (declare (ignore inst))
  (modify s
          :pc (+ 1 (pc (top-frame s)))
          :stack (pop (stack (top-frame s)))))

; (LOAD var)
(defun execute-LOAD (inst s)
  (modify s
          :pc (+ 1 (pc (top-frame s)))
          :stack (push (binding (arg1 inst)
                                (locals (top-frame s)))
                       (stack (top-frame s)))))

; (STORE var)
(defun execute-STORE (inst s)
  (modify s
          :pc (+ 1 (pc (top-frame s)))
          :locals (bind (arg1 inst)
                        (top (stack (top-frame s)))
                        (locals (top-frame s)))
          :stack (pop (stack (top-frame s)))))

; (DUP)
(defun execute-DUP (inst s)
  (declare (ignore inst))
  (modify s
          :pc (+ 1 (pc (top-frame s)))
          :stack (push (top (stack (top-frame s))) (stack (top-frame s)))))

; (ADD)
(defun execute-ADD (inst s)
  (declare (ignore inst))
  (modify s
          :pc (+ 1 (pc (top-frame s)))
          :stack (push (+ (top (pop (stack (top-frame s))))
                          (top (stack (top-frame s))))
                       (pop (pop (stack (top-frame s)))))))

; (SUB)
(defun execute-SUB (inst s)
  (declare (ignore inst))
  (modify s
          :pc (+ 1 (pc (top-frame s)))
          :stack (push (- (top (pop (stack (top-frame s))))
                          (top (stack (top-frame s))))
                       (pop (pop (stack (top-frame s)))))))

; (MUL)
(defun execute-MUL (inst s)
  (declare (ignore inst))
  (modify s
          :pc (+ 1 (pc (top-frame s)))
          :stack (push (* (top (pop (stack (top-frame s))))
                          (top (stack (top-frame s))))
                       (pop (pop (stack (top-frame s)))))))

; (GOTO n)
(defun execute-GOTO (inst s)
  (modify s
          :pc (+ (arg1 inst) (pc (top-frame s)))))

; (IFEQ n)
(defun execute-IFEQ (inst s)
  (modify s
          :pc (if (equal (top (stack (top-frame s))) 0)
                  (+ (arg1 inst) (pc (top-frame s)))
                (+ 1 (pc (top-frame s))))
          :stack (pop (stack (top-frame s)))))

; (IFNE n)
(defun execute-IFNE (inst s)
  (modify s
          :pc (if (equal (top (stack (top-frame s))) 0)
                  (+ 1 (pc (top-frame s)))
                (+ (arg1 inst) (pc (top-frame s))))
          :stack (pop (stack (top-frame s)))))

; (IFGT n)
(defun execute-IFGT (inst s)
  (modify s
          :pc (if (> (top (stack (top-frame s))) 0)
                  (+ (arg1 inst) (pc (top-frame s)))
                (+ 1 (pc (top-frame s))))
          :stack (pop (stack (top-frame s)))))

; (IFLE n)
(defun execute-IFLE (inst s)
  (modify s
          :pc (if (> (top (stack (top-frame s))) 0)
		  (+ 1 (pc (top-frame s)))
		(+ (arg1 inst) (pc (top-frame s))))
          :stack (pop (stack (top-frame s)))))

; (NEW class)
(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-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)
  (let* ((class-name (arg1 inst))
         (class-table (class-table s))
         (new-object (build-an-instance
                      (cons class-name
                            (class-decl-superclasses
                             (bound? class-name class-table)))
                      class-table))
         (new-address (len (heap s))))
    (modify s
            :pc (+ 1 (pc (top-frame s)))
            :stack (push (list 'REF new-address)
                         (stack (top-frame s)))
            :heap (bind new-address new-object (heap s)))))

; (GETFIELD class field)
(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)
  (let* ((class-name (arg1 inst))
         (field-name (arg2 inst))
         (instance (deref (top (stack (top-frame s))) (heap s)))
         (field-value (field-value class-name field-name instance)))
    (modify s
            :pc (+ 1 (pc (top-frame s)))
            :stack (push field-value
                         (pop (stack (top-frame s)))))))

; (PUTFIELD class field)
(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)
  (let* ((class-name (arg1 inst))
         (field-name (arg2 inst))
         (value (top (stack (top-frame s))))
         (instance (deref (top (pop (stack (top-frame s)))) (heap s)))
         (address (cadr (top (pop (stack (top-frame s)))))))
    (modify s
            :pc (+ 1 (pc (top-frame s)))
            :stack (pop (pop (stack (top-frame s))))
            :heap (bind address
                        (set-instance-field class-name
                                            field-name
                                            value
                                            instance)
                        (heap s)))))

; (INVOKEVIRTUAL class method n)
(defun reverse (lst)
  (if (consp lst)
      (append (reverse (cdr lst)) (list (car lst)))
    nil))

(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)
  (let* ((method-name (arg2 inst))
         (nformals (arg3 inst))
         (obj-ref (top (popn nformals (stack (top-frame 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))
         (s1 (modify s
                     :pc (+ 1 (pc (top-frame s)))
                     :stack (popn (len vars) (stack (top-frame s))))))
    (modify s1
            :call-stack
            (push (make-frame 0
                              (reverse
                               (bind-formals (reverse vars)
                                             (stack (top-frame s))))
                              nil
                              prog
			      'UNLOCKED)
                  (call-stack s1)))))

; (XRETURN)
(defun execute-XRETURN (inst s)
  (declare (ignore inst))
  (let ((val (top (stack (top-frame s))))
        (s1 (modify s
                    :call-stack (pop (call-stack s)))))
    (modify s1
            :stack (push val (stack (top-frame s1))))))

; (RETURN)
(defun execute-RETURN (inst s)
  (declare (ignore inst))
  (modify s
          :call-stack (pop (call-stack s))))

; The M2 Run Level
(defun do-inst (inst s)
  (case (op-code inst)
    (PUSH            (execute-PUSH          inst s))
    (POP             (execute-POP           inst s))
    (LOAD            (execute-LOAD          inst s))
    (STORE           (execute-STORE         inst s))
    (DUP             (execute-DUP           inst s))
    (ADD             (execute-ADD           inst s))
    (SUB             (execute-SUB           inst s))
    (MUL             (execute-MUL           inst s))
    (GOTO            (execute-GOTO          inst s))
    (IFEQ            (execute-IFEQ          inst s))
    (IFNE            (execute-IFNE          inst s))
    (IFGT            (execute-IFGT          inst s))
    (IFLE            (execute-IFLE          inst s))
    (NEW             (execute-NEW           inst s))
    (GETFIELD        (execute-GETFIELD      inst s))
    (PUTFIELD        (execute-PUTFIELD      inst s))
    (INVOKEVIRTUAL   (execute-INVOKEVIRTUAL inst s))
    (XRETURN         (execute-XRETURN       inst s))
    (RETURN          (execute-RETURN        inst s))
    (otherwise       s)))

(defun step (s)
  (do-inst (next-inst s) s))

(defun run (s n)
  (if (zp n)
      s
    (run (step s) (- n 1))))