CS 3220 Processor Design
Fall 2002

Instructor: Pete Manolios

iJVM2 Specification

The iJVM2 is a JVM-like machine. A state of the iJVM2 is a list of length 6. The first four components: pc (progam counter), sp (stack pointer), fp (frame pointer), and ap (argument pointer) are addresses. The last two, stack and code, are memories. Code is a read-only memory.  There is no way for an iJVM2 program to modify code.  Pc is a pointer into code. Stack is where frames, local variables, local stacks, etc. reside.  It is the memory that programs modify as they run.  Even though each address has a byte associated with it,  we usually are manipulating 32-bit words, e.g., the stack consists of signed 32-bit  words, each of which requires four consecutive bytes of storage.  These four bytes are in "big endian" order (the most significant byte is at the lowest address).  For example, the word 878082202 stored at address 0 is really stored as four bytes: 0: 52, 1: 86, 2: 120, 3: 154.  To see this, note that #x3456789a is 878082202 (recall that ACL2 allows one to specify numbers in hexadecimal) and that  #x34 is 52, #x56 is 86,  #x78 is 120, and #x9a is 154.

iJVM2 programs execute as follows.  The next instruction to execute is determined by the value of the pc.  The value of the pc is a byte in code.  That byte is an opcode which corresponds to one of the iJVM2 instructions.  (The instructions are given below.)   Depending on the instruction there can by 0, 1, or 2 bytes in arguments.  The local stack, local variables, frames, etc. are all on stack. This is why we need sp, fp, and apSp points to the top of  stack, by which we mean that it points to the first unused address in stack.  Since there is no call stack in the iJVM2 (as oppossed to the iJVM), we have to explicitely save frames on stack and this is what the other addresses are used for. Fp points to the location on stack that records the values of pc, fp, and ap of the calling frame.  Ap points to the location on stack that contains the arguments passed on the method call that created the frame, which are followed by the local variables used by the method.

The instructions of the iJVM2 explain in detail how to step a state and 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; say that it has the value i. We then find the opcode stored at location i in alist code and execute the instruction, 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 ijvm2-fact-program and ijvm2-fact-clock so that for any natural n that does not lead to overflow, something of the form
    (equal (get-word 0 (stack (run (ijvm2-fact-state n)
    			       (ijvm2-fact-clock n))))
           (fact n))
    is a theorem, where (get-word n) returns the 32-bit word at address n and fact, ijvm2-fact-state are defined as follows.
    (defun fact (n)
      (if (zp n)
        (* n (fact (1- n)))))
    (defun ijvm2-fact-state (n)
      (modify nil
    	  :pc 0
    	  :sp 0
    	  :ap 0
    	  :fp 0
    	  :code (ijvm2-fact-program n)
    	  :stack nil))
    Modify is analogous to the st macro of the small machine. Your program should start by pushing a number onto stack and then it should call the "fact method" with an invokestatic instruction.