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.
-
An address is an unsigned 32-bit number.
-
A memory is an alist. The car of an element in the alist is an address
and the cdr is a byte. We also
require that memories are sorted by the addresses of their elements.
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 ap. Sp
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
-
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.
-
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)
1
(* 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.