CS 3220 Processor Design
Fall 2002

Instructor: Pete Manolios

iJVM Specification

The iJVM is a JVM-like machine. A state of the iJVM is a list of length 2. The first component is a call stack and the second is a class table.

• A class table is a list of class declarations.
• A class declaration is a list of length 3 containing a class name, a list of superclasses, and a list of method definitions.
• The class name is a string identifying the class.
• The list of superclasses is a list of names of superclasses, starting with the direct superclass of the class, then its direct superclass, and so on until the class "Object" is reached. Recall that the class "Object" is the superclass of all other classes, as per the JVM specification.
• A method definition is a list whose first element is a string corresponding to the method name, its second argument is a list of formals, and the rest of the list (the cddr) is a method body.
• A call stack is a stack of frames.
• A frame is a list of length 4, containing a program counter, local variables, a local stack, and a method body.
• A program counter is a natural number.
• The local variables are an alist mapping symbols (the variable names) to integers (their values).
• A local stack is a list (whose car is the top of the stack) of integers.
• A method body is a list of instructions.
• The instructions of the iJVM are described here.

What to hand in

1. Define (run s n) so that it returns the state obtained by stepping state s n times. To step a state, we first look at the pc (program counter); say that it has the value i. We then look at the i^th instruction (using 0 indexing) of the method body in the top frame and execute it, obtaining a new state. Note that run is similar to the sm function in the Mechanized Formal Reasoning about Programs and Computing Machines paper by Boyer and Moore. Use the appropriate functions in the ihs book refered to in the bit-vector discussion for the arithmetic and logical operations.
2. Write a pair of functions ijvm-fact-program and ijvm-fact-clock so that for any natural n, something of the form

   	
   (equal (car (stack (run (ijvm-fact-state n)
   			(ijvm-fact-clock n))))
          (fact n))
   	 
   	

   is a theorem, where the function stack above returns the stack of the top frame and fact and ijvm-fact-state are defined as follows.

   	
   (defun fact (n)
     (if (zp n)
         1
       (* n (fact (1- n)))))
   
   (defun ijvm-fact-state (n)
     (make-state
      (push (make-frame 0
                        nil
                        nil
                        `((bipush ,n)
                          (invokestatic "Math" "fact")
                          (halt)))
            nil)
      (list *math-class*)))
   
   (defconst *math-class*
     `("Math"
       ("Object")
       (("fact" (N)
         ,@(ijvm-fact-program)))))