Library Instructions


All JVML instructions represented in CoJaq

@author Patryk Czarnik

Require Import Common.
Require Import ValuesNTypes.
Require Import ProgramStructures.
Require Import Heap.
Require Import ZArith.
Require Import Program.
Require Import ArithOps.
Require Import List.
Import List.ListNotations.

Declare Module P : PROGRAM_W_CONSTRUCTORS.
Module PS := P.M_ProgramStructures.
Module VAT := PS.M_ValuesAndTypes.
Module INum := VAT.M_Numeric_Int.
Module FNum := VAT.M_Numeric_Float.
Module LNum := VAT.M_Numeric_Long.
Module DNum := VAT.M_Numeric_Double.
Module PSFacts := ProgramStructuresFacts PS.

Import P PS PSFacts VAT ArithmeticOperators.

Some auxiliary objects used then as example arguments of instructions
Variable rt: TReferenceType.
Variable bt: TBaseType.
Variable cn: TClassName.
Variable fname: TShortName.
Variable msig: TSignature.
Variable var: TVar.
Variable off: TOffset.
Variable k: TKind.
Variable ak: TArrayIKind.
Variable v: TValue.
Variable c: INum.t.
Variable n: nat.

Definition Code_to_test_instructions: P.TCode := P.codeFromList
[
aaload
aastore
aconst_null
aload
aload_0
aload_1
aload_2
aload_3
anewarray
areturn
arraylength
astore
astore_0
astore_1
astore_2
astore_3
athrow
baload
bastore
bipush
caload
castore
checkcast
d2f
d2i
d2l
dadd
daload
dastore
dcmpg
dcmpl
dconst_0
dconst_1
ddiv
dload
dload_0
dload_1
dload_2
dload_3
dmul
dneg
drem
dreturn
dstore
dstore_0
dstore_1
dstore_2
dstore_3
dsub
dup
dup_x1
dup_x2
dup2
dup2_x1
dup2_x2
f2d
f2i
f2l
fadd
faload
fastore
fcmpg
fcmpl
fconst_0
fconst_1
fconst_2
fdiv
fload
fload_0
fload_1
fload_2
fload_3
fmul
fneg
frem
freturn
fstore
fstore_0
fstore_1
fstore_2
fstore_3
fsub
getfield
getstatic
goto goto_w
i2b
i2c
i2d
i2f
i2l
i2s
iadd
iaload
iand
iastore
iconst_0
iconst_1
iconst_2
iconst_3
iconst_4
iconst_5
iconst_m1
idiv
if_acmpeq
if_acmpne
if_icmpeq
if_icmpge
if_icmpgt
if_icmple
if_icmplt
if_icmpne
ifeq
ifge
ifgt
ifle
iflt
ifne
ifnonnull
ifnull
iinc
iload
iload_0
iload_1
iload_2
iload_3
imul
ineg
instanceof
invokeinterface
invokespecial
invokestatic
invokevirtual
ior
irem
ireturn
ishl
ishr
istore
istore_0
istore_1
istore_2
istore_3
isub
iushr
ixor
jsr jsr_w
l2d
l2f
l2i
ladd
laload
land
lastore
lcmp
lconst_0
lconst_1
ldc ldc_w ldc2_w
ldiv
lload
lload_0
lload_1
lload_2
lload_3
lmul
lneg
lookupswitch
lor
lrem
lreturn
lshl
lshr
lstore
lstore_0
lstore_1
lstore_2
lstore_3
lsub
lushr
lxor
monitorenter
monitorexit
multianewarray
new
newarray
nop
pop
pop2
putfield
putstatic
ret
return
saload
sastore
sipush
swap
tableswitch