simple-instructions-h-i.lisp

Note that when converting an `int` value to a `long`
value, the upper half of the `long` value need not be zero. If
the `int` value is negative, then the upper half will be
non-zero.

(define-djvm-operation (i2l) ---STACK--- (:int x) <rest-of-stack> ==> (:long-top-half (long-top-half x)) (:long-bot-half (long-bot-half x)) <rest-of-stack>)

(define-djvm-operation (i2s) ---STACK--- (:int x) <rest-of-stack> ==> (:int (narrow-to-short x)) <rest-of-stack>)

The JVMS states:

If an

iaddoverflows, then the result is the low-order bits of the true mathematical result in a sufficiently wide two's complement format. If an overflow occurs, then the sign of the result will not be the same as the sign of the mathematical sum of the two values.

[p. 238 in JVMS]

Note that in

This statement is presumably an oversight by Lindholm and Yellin, since they correctly say ``may not'' in similar descriptions elsewhere.

The example (2^{n} - 1) + 1 illustrates a case in which their statement
is true. However, (2^{n} - 1) + (2^{n}-1) = 2^{n+1} - 2, which will
overflow n bits, but for which bits n will be the same as bit
n+1. Here's an example for n=8:

011111111 _{2}+ 011111111 _{2}---------- 111111110 _{2}

Note that the 9^{th} bit (the ``sign bit of the true mathematical
result'') is the same as the 8^{th} bit (the ``sign bit of the
truncated result'').

(define-djvm-operation (iadd) ---STACK--- (:int x) (:int y) <rest-of-stack> ==> (:int (int-add x y)) <rest-of-stack>)(defun

int-add(x y) (declare (xargs :guard (and (int-value-p x) (int-value-p y)))) (narrow-to-int (+ x y)))

(define-djvm-operation (iand) ---STACK--- (:int x) (:int y) <rest-of-stack> ==> (:int (int-logical-and x y)) <rest-of-stack>)

(define-djvm-operation (iconst_0) ---STACK--- <rest-of-stack> ==> (:int 0) <rest-of-stack>---OTHER-PROPERTIES--- :length 1)

(define-djvm-operation (iconst_1) ---STACK--- <rest-of-stack> ==> (:int 1) <rest-of-stack>)

(define-djvm-operation (iconst_2) ---STACK--- <rest-of-stack> ==> (:int 2) <rest-of-stack>)

(define-djvm-operation (iconst_3) ---STACK--- <rest-of-stack> ==> (:int 3) <rest-of-stack>)

(define-djvm-operation (iconst_4) ---STACK--- <rest-of-stack> ==> (:int 4) <rest-of-stack>)

(define-djvm-operation (iconst_5) ---STACK--- <rest-of-stack> ==> (:int 5) <rest-of-stack>)

(define-djvm-operation (iconst_m1) ---STACK--- <rest-of-stack> ==> (:int -1) <rest-of-stack>)

(define-djvm-operation (On the JVM division rounds towards zero. The Common Lisp functionidiv) ---STACK--- (:int denom) (:int num) <rest-of-stack> ==> (:int (narrow-to-int (integer-div num denom))) <rest-of-stack> ---OTHER-PROPERTIES--- :exceptions ((equal denom 0) "ArithmeticException") :length 1)

We define `integer-div` to specify in the guard that the
arguments must be integers. The ACL2 function `truncate`
accepts rational numbers, as well as integers.

(defuninteger-div(x y) (declare (xargs :guard (and (integerp x) (integerp y) (not (= 0 y))))) (truncate x y))

Although the bytecode verifier prohibits such invalid branch
targets, the behavior here is probably wrong. Rather, the invalid
`pc` should only trigger an exception if the branch is taken.

The exception mechanism in `define-djvm-operation`
tests the arguments before the operation, for example to prevent
division by zero in the `idiv` instruction.

So, we could either define invalid branch targets as exceptions using
this mechanism; or ignore the possibility of an invalid branch target
here, let the branch execute, and catch the invalid `pc` in
the general test for invalid `pc` values within the
boiler-plate of the `define-defensive-instruction` definition
form.

(define-djvm-operation (IF_ACMPEQoffset) ---STACK--- (:ref x) (:ref y) <rest-of-stack> ==> <rest-of-stack> ---OTHER-PROPERTIES--- :assert (short-value-p offset) :branch-if (= x y) :branch-target (+ offset Current-Instruction-Address) :instruction-length 3 :exceptions ( (not (djvm-valid-pc? (+ offset Current-Instruction-Address) djvm)) "Invalid branch target"))

(define-djvm-operation (IF_ACMPNEoffset) ---STACK--- (:ref x) (:ref y) <rest-of-stack> ==> <rest-of-stack> ---OTHER-PROPERTIES--- :assert (short-value-p offset) :branch-if (not (= x y)) :branch-target (+ offset Current-Instruction-Address) :instruction-length 3 :exceptions ( (not (djvm-valid-pc? (+ offset Current-Instruction-Address) djvm)) "Invalid branch target"))

(define-djvm-operation (IF_ICMPEQoffset) ---STACK--- (:int x) (:int y) <rest-of-stack> ==> <rest-of-stack> ---OTHER-PROPERTIES--- :assert (short-value-p offset) :branch-if (= x y) :branch-target (+ offset Current-Instruction-Address) :instruction-length 3 :exceptions ( (not (djvm-valid-pc? (+ offset Current-Instruction-Address) djvm)) "Invalid branch target"))

(define-djvm-operation (IF_ICMPNEoffset) ---STACK--- (:int x) (:int y) <rest-of-stack> ==> <rest-of-stack> ---OTHER-PROPERTIES--- :assert (short-value-p offset) :branch-if (not (= x y)) :branch-target (+ offset Current-Instruction-Address) :instruction-length 3 :exceptions ( (not (djvm-valid-pc? (+ offset Current-Instruction-Address) djvm)) "Invalid branch target"))

(define-djvm-operation (IF_ICMPLToffset) ---STACK--- (:int x) (:int y) <rest-of-stack> ==> <rest-of-stack> ---OTHER-PROPERTIES--- :assert (short-value-p offset) :branch-if (< y x) :branch-target (+ offset Current-Instruction-Address) :instruction-length 3 :exceptions ( (not (djvm-valid-pc? (+ offset Current-Instruction-Address) djvm)) "Invalid branch target"))

(define-djvm-operation (IF_ICMPGEoffset) ---STACK--- (:int x) (:int y) <rest-of-stack> ==> <rest-of-stack> ---OTHER-PROPERTIES--- :assert (short-value-p offset) :branch-if (>= y x) :branch-target (+ offset Current-Instruction-Address) :instruction-length 3 :exceptions ( (not (djvm-valid-pc? (+ offset Current-Instruction-Address) djvm)) "Invalid branch target"))

(define-djvm-operation (IF_ICMPGToffset) ---STACK--- (:int x) (:int y) <rest-of-stack> ==> <rest-of-stack> ---OTHER-PROPERTIES--- :assert (short-value-p offset) :branch-if (> y x) :branch-target (+ offset Current-Instruction-Address) :instruction-length 3 :exceptions ( (not (djvm-valid-pc? (+ offset Current-Instruction-Address) djvm)) "Invalid branch target"))

(define-djvm-operation (IF_ICMPLEoffset) ---STACK--- (:int x) (:int y) <rest-of-stack> ==> <rest-of-stack> ---OTHER-PROPERTIES--- :assert (short-value-p offset) :branch-if (<= y x) :branch-target (+ offset Current-Instruction-Address) :instruction-length 3 :exceptions ( (not (djvm-valid-pc? (+ offset Current-Instruction-Address) djvm)) "Invalid branch target"))

(define-djvm-operation (IFEQoffset) ---STACK--- (:int x) <rest-of-stack> ==> <rest-of-stack> ---OTHER-PROPERTIES--- :assert (short-value-p offset) :branch-if (= x 0) :branch-target (+ offset Current-Instruction-Address) :instruction-length 3 :exceptions ( (not (djvm-valid-pc? (+ offset Current-Instruction-Address) djvm)) "Invalid branch target"))

(define-djvm-operation (IFNEoffset) ---STACK--- (:int x) <rest-of-stack> ==> <rest-of-stack> ---OTHER-PROPERTIES--- :assert (short-value-p offset) :branch-if (not (= x 0)) :branch-target (+ offset Current-Instruction-Address) :instruction-length 3 :exceptions ( (not (djvm-valid-pc? (+ offset Current-Instruction-Address) djvm)) "Invalid branch target"))

(define-djvm-operation (IFLToffset) ---STACK--- (:int x) <rest-of-stack> ==> <rest-of-stack> ---OTHER-PROPERTIES--- :assert (short-value-p offset) :branch-if (< x 0) :branch-target (+ offset Current-Instruction-Address) :instruction-length 3 :exceptions ( (not (djvm-valid-pc? (+ offset Current-Instruction-Address) djvm)) "Invalid branch target"))

(define-djvm-operation (IFLEoffset) ---STACK--- (:int x) <rest-of-stack> ==> <rest-of-stack> ---OTHER-PROPERTIES--- :assert (short-value-p offset) :branch-if (<= x 0) :branch-target (+ offset Current-Instruction-Address) :instruction-length 3 :exceptions ( (not (djvm-valid-pc? (+ offset Current-Instruction-Address) djvm)) "Invalid branch target"))

(define-djvm-operation (IFGToffset) ---STACK--- (:int x) <rest-of-stack> ==> <rest-of-stack> ---OTHER-PROPERTIES--- :assert (short-value-p offset) :branch-if (> x 0) :branch-target (+ offset Current-Instruction-Address) :instruction-length 3 :exceptions ( (not (djvm-valid-pc? (+ offset Current-Instruction-Address) djvm)) "Invalid branch target"))

(define-djvm-operation (IFGEoffset) ---STACK--- (:int x) <rest-of-stack> ==> <rest-of-stack> ---OTHER-PROPERTIES--- :assert (short-value-p offset) :branch-if (>= x 0) :branch-target (+ offset Current-Instruction-Address) :instruction-length 3 :exceptions ( (not (djvm-valid-pc? (+ offset Current-Instruction-Address) djvm)) "Invalid branch target"))

(define-djvm-operation (IFNONNULLoffset) ---STACK--- (:ref x) <rest-of-stack> ==> <rest-of-stack> ---OTHER-PROPERTIES--- :assert (short-value-p offset) :branch-if (not (ref-to-null-p x)) :branch-target (+ offset Current-Instruction-Address) :instruction-length 3 :exceptions ( (not (djvm-valid-pc? (+ offset Current-Instruction-Address) djvm)) "Invalid branch target"))

(define-djvm-operation (IFNULLoffset) ---STACK--- (:ref x) <rest-of-stack> ==> <rest-of-stack> ---OTHER-PROPERTIES--- :assert (short-value-p offset) :branch-if (ref-to-null-p x) :branch-target (+ offset Current-Instruction-Address) :instruction-length 3 :exceptions ( (not (djvm-valid-pc? (+ offset Current-Instruction-Address) djvm)) "Invalid branch target"))

(define-dJVM-Operation (IINCindex const) ---LOCALS--- (:local-var index (:int x)) ==> (:local-var index (:int (int-add x const))) ---OTHER-PROPERTIES--- :assert (and (unsigned-byte-value-p index) (byte-value-p const)) :instruction-length 3)

The `wide` form of the `iinc` instruction permits the
*index* and `constant` instruction arguments to be
16-bit values, rather than being restricted to the 8-bit values
permitted by the unmodified form of the instruction. The 16-bit value
for the local-variable index value is interpreted as an ``unsigned
short'' value, and the constant is interpreted as a `short`
integer value.

(define-dJVM-Operation (IINC_WIDEindex const) ---LOCALS--- (:local-var index (:int x)) ==> (:local-var index (:int (int-add x const))) ---OTHER-PROPERTIES--- :assert (and (unsigned-short-value-p index) (short-value-p const)) :instruction-length 3)

(define-dJVM-Operation (ILOADindex) ---STACK--- <rest-of-stack> ==> (:int x) <rest-of-stack> ---LOCALS--- (:local-var index (:int x)) ==> <unchanged> ---OTHER-PROPERTIES--- :assert (unsigned-byte-value-p index) :instruction-length 2)

(define-dJVM-Operation (The abbreviated instructionsILOAD_wideindex) ---STACK--- <rest-of-stack> ==> (:int x) <rest-of-stack>---LOCALS--- (:local-var index (:int x)) ==> <unchanged> ---OTHER-PROPERTIES--- :assert (unsigned-short-value-p index) :instruction-length 4)

(define-dJVM-Operation (ILOAD_0) ---STACK--- <rest-of-stack> ==> (:int x) <rest-of-stack> ---LOCALS--- (:local-var 0 (:int x)) ==> <unchanged> ---OTHER-PROPERTIES--- :instruction-length 1)

(define-dJVM-Operation (ILOAD_1) ---STACK--- <rest-of-stack> ==> (:int x) <rest-of-stack> ---LOCALS--- (:local-var 1 (:int x)) ==> <unchanged> ---OTHER-PROPERTIES--- :instruction-length 1)

(define-dJVM-Operation (ILOAD_2) ---STACK--- <rest-of-stack> ==> (:int x) <rest-of-stack> ---LOCALS--- (:local-var 2 (:int x)) ==> <unchanged> ---OTHER-PROPERTIES--- :instruction-length 1)

(define-dJVM-Operation (ILOAD_3) ---STACK--- <rest-of-stack> ==> (:int x) <rest-of-stack> ---LOCALS--- (:local-var 3 (:int x)) ==> <unchanged> ---OTHER-PROPERTIES--- :instruction-length 1)

The `imul` instruction multiplies two `int` values, and
pushes an `int`result onto the stack. If the product is
outside the range of `int` values, it is ``truncated'' via
`narrow-to-int`. No arithmetic exception are ever thrown by
this instruction.

If an

intmultiplication overflows, then the result is the low-order bits of the mathematical product as anint. If overflow occurs, then the sign of the result may not be the same as the sign of the mathematical produce of the two values.

[p. 254 in JVMS]

(define-djvm-operation (IMUL) ---STACK--- (:int x) (:int y) <rest-of-stack> ==> (:int (int-mul x y)) <rest-of-stack>)(defun

int-mul(x y) (declare (xargs :guard (and (int-value-p x) (int-value-p y)))) (narrow-to-int (* x y)))

For

intvalues, negation is the same as subtraction from zero. Because the Java Virtual Machine uses two's-complement representation for integer and the range of two's-complement values is not symmetric, the negation of the maximum negative valueintresults in that same maximum negative number. Despite the fact that overflow has occurred, no exception is thrown.

[p. 255 in JVMS]

(define-djvm-operation (JVM arithmetic is defined in terms of two's-complement representation. Negation is defined in two's complement arithmetic as ``complement and increment'' --- ( x) + 1. For the most negative value in a two's-complement representation, this operation yields its input. The functionINEG) ---STACK--- (:int x) <rest-of-stack> ==> (:int (int-neg x)) <rest-of-stack>)

(defunint-neg(x) (declare (xargs :guard (int-value-p x))) (narrow-to-int (- x)))

(define-djvm-operation (ior) ---STACK--- (:int x) (:int y) <rest-of-stack> ==> (:int (int-logical-ior x y)) <rest-of-stack>)

The use of `(:local-var index tagged-value)`
implicitly requires that

(define-dJVM-Operation (ISTOREindex) ---STACK--- (:int x) <rest-of-stack> ==> <rest-of-stack> ---LOCALS--- <no-constraints> ==> (:local-var index (:int x)) ---OTHER-PROPERTIES--- :assert (unsigned-byte-value-p index) :instruction-length 2)

(define-dJVM-Operation (ISTORE_wideindex) ---STACK--- (:int x) <rest-of-stack> ==> <rest-of-stack>---LOCALS--- <no-constraints> ==> (:local-var index (:int x)) ---OTHER-PROPERTIES--- :assert (unsigned-short-value-p index) :instruction-length 4)

(define-dJVM-Operation (ISTORE_0) ---STACK--- (:int x) <rest-of-stack> ==> <rest-of-stack> ---LOCALS--- <no-constraints> ==> (:local-var 0 (:int x)) ---OTHER-PROPERTIES--- :instruction-length 1)

(define-dJVM-Operation (ISTORE_1) ---STACK--- (:int x) <rest-of-stack> ==> <rest-of-stack> ---LOCALS--- <no-constraints> ==> (:local-var 1 (:int x)) ---OTHER-PROPERTIES--- :instruction-length 1)

(define-dJVM-Operation (ISTORE_2) ---STACK--- (:int x) <rest-of-stack> ==> <rest-of-stack> ---LOCALS--- <no-constraints> ==> (:local-var 2 (:int x)) ---OTHER-PROPERTIES--- :instruction-length 1)

(define-dJVM-Operation (ISTORE_3) ---STACK--- (:int x) <rest-of-stack> ==> <rest-of-stack> ---LOCALS--- <no-constraints> ==> (:local-var 3 (:int x)) ---OTHER-PROPERTIES--- :instruction-length 1)

(define-djvm-operation (ISUB) ---STACK--- (:int x) (:int y) <rest-of-stack> ==> (:int (int-sub y x)) <rest-of-stack>)(defun

int-sub(x y) (declare (xargs :guard (and (int-value-p x) (int-value-p y)))) (narrow-to-int (- x y)))

(define-djvm-operation (IXOR) ---STACK--- (:int x) (:int y) <rest-of-stack> ==> (:int (int-logical-xor x y)) <rest-of-stack>)(defun

int-logical-xor(x y) (declare (xargs :guard (and (int-value-p x) (int-value-p y)) :guard-hints (("Goal" :in-theory (enable int-value-p))))) (narrow-to-int (logxor x y)))