; Recursive Static Method for factorial on M5
; 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.
;==============================================================
;; 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
|#
;;- - - - - - - - - - - - - -
;; Note, in Method int fact(int), the ifle instruction 
;; at pc 1 is a branch instruction to pc 13 when the top
;; of the stack is less than or equal to 0. The javap
;; utility displays the jump targets as absolute program
;; counters. But the actual JVM ifle instruction takes
;; an offset from the current pc. Thus this line should
;; read 1 ifle 12 to faithfully display the bytecode.
;; ================================================
(include-book "m5")

(in-package "M5")

;; The constant *Demo-state* given below is an M5 state about
;; to execute the main method of Demo.java.

;; Recall that an M5 state has three parts: a thread-table,
;; a heap, and a class-table.
;;---------------------------
;; Here is the thread table. There is one thread with thread 
;; identifier 0.  The call stack of the thread has one frame,
;; poised to execute the main method of the Demo class. The 
;; thread is SCHEDULED and has nil rref because the main
;; thread is not a heap object.

(defconst *Demo-thread-table*
   (list
    (cons 0                 ; thread identifier
          (make-thread      ; thread
           (push            ;  call stack
            (make-frame     ;   frame
             0              ;    pc
             nil            ;    locals
             nil            ;    operand stack
             '((ICONST_4)   ;    program
               (ISTORE_1)
               (ILOAD_1)
               (ICONST_1)
               (IADD)
               (INVOKESTATIC "Demo" "fact" 1)
               (PUTSTATIC "Demo" "ans" NIL)
               (RETURN))
             'UNLOCKED      ;    sync flg
             "Demo")        ;    current class
            nil)            ;   end of call stack   
           'SCHEDULED       ;  thread status
           nil))))          ;  thread rref
;;- - - - - - - - - - - - - - - - 
;; The program above is that for main:
#|
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
|#
;;---------------------------
;; Here is the heap. Each instance object in this heap 
;; is the object manisfestation of a class. These objects
;; are used by synchronized static methods.

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

;; The instance object with heap address 0 corresponds to the
;; "java.lang.Object" class.  It is an object of class
;; "java.lang.Class" extending "java.lang.Object". It has the
;; field "<name>" from its immediate class and inherits the 
;; fields "monitor", "mcount", and "wait-set" from the Object
;; class.

;; The next entries in the heap are instance objects for the
;; primitive classes ARRAY, java.lang.Thread, java.lang.String,
;; and java.lang.Class.

;; The instance object with heap address 5 corresponds to the
;; "Demo" class. It has the same fields as the other instances
;; shown plus one static field, named "ans".

;;---------------------------
;; Here is the class table for the Demo class. The 
;; "java.lang.Object" class has no superclasses -- it is the only
;; such class. It declares three instance field names, "monitor",
;; "mcount", "wait-set", and no static field names. It has an
;; empty constant pool. It declares only one method, the
;; <init> method.

;; The method declaration lists the name, the formals, the
;; synchronization flag, and then bytecode. In this case,
;; the name is "<init>", the list of formals is empty, the
;; synchronization flag is nil, and the bytecode is just a 
;; list containing the single bytecode instruction (RETURN).

;; The `object in heap' entry is a reference to the instance
;; object representing this class in the heap.

(defconst *Demo-class-table*
  '(("java.lang.Object"              ; Object class
     NIL                             ; superclasses
     ("monitor" "mcount" "wait-set") ; instance fields
     NIL                             ; static fields
     NIL                             ; constant pool
     (("<init>" NIL NIL (RETURN)))   ; methods
     (REF 0))                        ; object in heap

    ("ARRAY"                         ; ARRAY class
     ("java.lang.Object")            ; superclasses
     (("<array>" . *ARRAY*))         ; instance fields
     NIL                             ; static fields
     NIL                             ; constant pool
     NIL                             ; methods
     (REF 1))                        ; object in heap

    ("java.lang.Thread"              ; Thread class
     ("java.lang.Object")            ; superclasses
     NIL                             ; instance fields
     NIL                             ; static fields
     NIL                             ; constant pool
     (("run" NIL NIL (RETURN))       ; methods
      ("start" NIL NIL NIL)
      ("stop" NIL NIL NIL)
      ("<init>" NIL NIL (ALOAD_0)
       (INVOKESPECIAL "java.lang.Object" "<init>" 0)
       (RETURN)))
     (REF 2))                        ; object in heap

    ("java.lang.String"              ; String class
     ("java.lang.Object")            ; superclasses
     ("strcontents")                 ; instance fields
     NIL                             ; static fields
     NIL                             ; constant pool
     (("<init>" NIL NIL              ; methods
       (ALOAD_0)
       (INVOKESPECIAL "java.lang.Object" "<init>" 0)
       (RETURN)))
     (REF 3))                        ; object in heap

    ("java.lang.Class"               ; Class class             
     ("java.lang.Object")            ; superclasses
     NIL                             ; instance fields
     NIL                             ; static fields
     NIL                             ; constant pool
     (("<init>" NIL NIL              ; methods
       (ALOAD_0)
       (INVOKESPECIAL "java.lang.Object" "<init>" 0)
       (RETURN)))
     (REF 4))                        ; object in heap

    ("Demo"                          ; Demo class
     ("java.lang.Object")            ; superclasses
     NIL                             ; instance fields
     ("ans")                         ; static fields
     NIL                             ; constant pool
     (("<init>" NIL NIL              ; methods
       (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))))                      ; object in heap

;; Note the methods declared for the "Demo" class. Three methods are
;; declared, "<init>", "fact", and "main". Each declaration is of the
;; form (name formals sync . program).

;; The <init> method is the initializer for an instance object of the
;; class. It has no formals and is not synchronized. This initializer
;; just invokes the initializer for the superclass.

;; The fact method takes one formal, of type int, and is not 
;; synchronized.

;; The main method takes one formal, of type java.lang.String[], and
;; is not synchronized.

;;---------------------------
;; Here is the M5 state for Demo: 

(defconst *Demo-state*
  (make-state *demo-thread-table*
              *demo-heap*
              *demo-class-table*))

;;---------------------------
;; A Schedule that Runs fact to Completion

(defun repeat (th n)
  (if (zp n)
      nil
    (cons th (repeat th (- n 1)))))

(defun fact-sched (th n)
  (if (zp n)
      (repeat th 5)
    (append (repeat th 7)
            (fact-sched th (- n 1))
            (repeat th 2))))

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

;; After the Run below, we expect to find 120 in the static field ans
;; associated with  the object manisfestation of the class "Demo" in 
;; the heap:

(static-field-value "Demo"
		    "ans"
		    (run (main-sched 0) *Demo-state*))
;; returns 120.

;;- - - - - - - - - - - - - 
(run (main-sched 0) *Demo-state*))

#|
(((0 NIL 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" . 120))
     ("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))))
|#