CS378 A Formal Model of the JVM                 Spring, 2012 / March 7, 2012
J Strother Moore                                Midterm Exam

This exam is 3 pages long, plus three attachments: copies of m1.lisp,
m1-support.lisp, and template.lisp for reference only.  There are six 
problems, each worth a specified number of points.  100 points are available
in all.  Partial credit will be given.  Write clearly.  You are free to 
define auxiliary functions in answering any of the questions.  Make sure you
write your name on each page turned in.  You have until 5:00 pm.

----------------------------------------------------------------------------

Problem 1 (30 points -- 5 points for each item below) : Express these ideas
about an M1 state s.

(a) ``the instruction that will be executed when s is stepped''

(b) ``the value of local variable 2 in s''

(c) ``the item just below the topmost item on the stack of s''

(d) ``the state obtained from s by incrementing the pc and setting local
      variable 2 to 0''

(e) ``the number of HALT instructions in the program of s''

(f) ``the highest numbered local variable used in the program of s.''  Return
    -1 if the program uses no local variables.  By the way, (max i j) is an
    ACL2 expression that returns the maximum of the numbers i and j.

----------------------------------------------------------------------------

Problem 2 (10 points): Suppose we decided to change M1 so that the machine
halts if an ISTORE is executed when there is nothing on the stack.  How would
you redefine execute-ISTORE, which I've shown below for your reference?

(defun execute-ISTORE (inst s)
  (make-state (+ 1 (pc s))
              (update-nth (arg1 inst) (top (stack s)) (locals s))
              (pop (stack s))
              (program s)))

----------------------------------------------------------------------------



[page 1 of 3]

----------------------------------------------------------------------------

Problem 3 (15 points): Extend M1 to include the following instruction.  It
suffices merely to define the semantic function, execute-IFEQDEC.

Instruction: (IFEQDEC index delta)

Stack:  ... ==> ...

Description: Decrement the local variable at index and if the new value is
equal to 0, increment the pc by delta.  (Otherwise, go to the next
instruction.)

----------------------------------------------------------------------------

Problem 4 (15 points): Extend M1 to include the following instruction.  It
suffices merely to define the semantic function, execute-POPN:

Instruction: (POPN)

Stack: ... v1,---, vn, n ==> ...

Description: Pop n values off the stack, where n is the topmost item on the
stack.  You may assume that n is a natural number and that there are at least
n+1 items on the stack.

----------------------------------------------------------------------------


















[page 2 of 3]

----------------------------------------------------------------------------

Problem 5 (15 points): Write the schedule function for the following code.
Name the local variables x, y, and a (locals 0, 1, and 2) respectively.  You
may assume x, y, and a are natural numbers.

(ILOAD 0)   ;  0
(ILOAD 1)   ;  1
(IADD)      ;  2
(ISTORE 2)  ;  3
(ILOAD 0)   ;  4
(IFEQ 14)   ;  5 
(ILOAD 0)   ;  6
(ICONST 1)  ;  7
(ISUB)      ;  8
(ISTORE 0)  ;  9
(ILOAD 2)   ; 10
(ILOAD 1)   ; 11
(IFEQ 3)    ; 12
(ICONST 1)  ; 13
(IADD)      ; 14
(ICONST 1)  ; 15
(IADD)      ; 16
(ISTORE 2)  ; 17
(GOTO -14)  ; 18
(ILOAD 2)   ; 19
(HALT)      ; 20

----------------------------------------------------------------------------

Problem 6 (15 points): To compute 2^n (two raised to the nth power) for a
natural number n, we could use the following algorithm:

(defun helper (n a)
  (if (zp n)
      a
      (helper (- n 1) (+ a a))))

(defun fn (n) (helper n 1))

Write down the two theorems needed to prove the algorithm correct, i.e., the
theorems called helper-is-theta and fn-is-theta in the template.

----------------------------------------------------------------------------

[page 3 of 3]                                             The End