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

I_Heap (HI_Get (Op_getarray AIKRef))

aastore

; I_Heap (HI_Put (Op_putarray AIKRef))

aconst_null

; I_Frame (FI_Stackop (SI_Const KRef (VRef null)))

aload

; I_Frame (FI_Var (VI_Load VIKRef var))

aload_0

; I_Frame (FI_Var (VI_Load VIKRef var0))

aload_1

; I_Frame (FI_Var (VI_Load VIKRef var1))

aload_2

; I_Frame (FI_Var (VI_Load VIKRef var2))

aload_3

; I_Frame (FI_Var (VI_Load VIKRef var3))

anewarray

; I_Heap (HI_New (Op_newarray_ref rt))

areturn

; I_Return (Some KRef)

arraylength

; I_Heap (HI_Get Op_array_length)

astore

; I_Frame (FI_Var (VI_Store VIKRef var))

astore_0

; I_Frame (FI_Var (VI_Store VIKRef var0))

astore_1

; I_Frame (FI_Var (VI_Store VIKRef var1))

astore_2

; I_Frame (FI_Var (VI_Store VIKRef var2))

astore_3

; I_Frame (FI_Var (VI_Store VIKRef var3))

athrow

; I_Throw

baload

; I_Heap (HI_Get (Op_getarray AIKByteBool))

bastore

; I_Heap (HI_Put (Op_putarray AIKByteBool))

bipush

; I_Frame (FI_Stackop (SI_Const KInt (VInt (INum.const 0))))

caload

; I_Heap (HI_Get (Op_getarray AIKChar))

castore

; I_Heap (HI_Put (Op_putarray AIKChar))

checkcast

; I_Heap (HI_Get (Op_checkcast rt))

d2f

; I_Frame (FI_Stackop (SI_Cast KDouble CastOp_f))

d2i

; I_Frame (FI_Stackop (SI_Cast KDouble CastOp_d))

d2l

; I_Frame (FI_Stackop (SI_Cast KDouble CastOp_l))

dadd

; I_Frame (FI_Stackop (SI_Binop KDouble BinOp_add))

daload

; I_Heap (HI_Get (Op_getarray AIKDouble))

dastore

; I_Heap (HI_Put (Op_putarray AIKDouble))

dcmpg

; I_Frame (FI_Stackop (SI_Cmpi KDouble CmpiOp_cmpg))

dcmpl

; I_Frame (FI_Stackop (SI_Cmpi KDouble CmpiOp_cmpl))

dconst_0

; I_Frame (FI_Stackop (SI_Const KDouble (VDouble (DNum.zero))))

dconst_1

; I_Frame (FI_Stackop (SI_Const KDouble (VDouble (DNum.one))))

ddiv

; I_Frame (FI_Stackop (SI_Binop KDouble BinOp_div))

dload

; I_Frame (FI_Var (VI_Load VIKDouble var))

dload_0

; I_Frame (FI_Var (VI_Load VIKDouble var0))

dload_1

; I_Frame (FI_Var (VI_Load VIKDouble var1))

dload_2

; I_Frame (FI_Var (VI_Load VIKDouble var2))

dload_3

; I_Frame (FI_Var (VI_Load VIKDouble var3))

dmul

; I_Frame (FI_Stackop (SI_Binop KDouble BinOp_mul))

dneg

; I_Frame (FI_Stackop (SI_Unop KDouble UnOp_neg))

drem

; I_Frame (FI_Stackop (SI_Binop KDouble BinOp_rem))

dreturn

; I_Return (Some KDouble)

dstore

; I_Frame (FI_Var (VI_Store VIKDouble var))

dstore_0

; I_Frame (FI_Var (VI_Store VIKDouble var0))

dstore_1

; I_Frame (FI_Var (VI_Store VIKDouble var1))

dstore_2

; I_Frame (FI_Var (VI_Store VIKDouble var2))

dstore_3

; I_Frame (FI_Var (VI_Store VIKDouble var3))

dsub

; I_Frame (FI_Stackop (SI_Binop KDouble BinOp_sub))

dup

; I_Frame (FI_Stackop (SI_Generic Op_dup))

dup_x1

; I_Frame (FI_Stackop (SI_Generic Op_dup_x1))

dup_x2

; I_Frame (FI_Stackop (SI_Generic Op_dup_x2))

dup2

; I_Frame (FI_Stackop (SI_Generic Op_dup2))

dup2_x1

; I_Frame (FI_Stackop (SI_Generic Op_dup2_x1))

dup2_x2

; I_Frame (FI_Stackop (SI_Generic Op_dup2_x2))

f2d

; I_Frame (FI_Stackop (SI_Cast KFloat CastOp_d))

f2i

; I_Frame (FI_Stackop (SI_Cast KFloat CastOp_i))

f2l

; I_Frame (FI_Stackop (SI_Cast KFloat CastOp_l))

fadd

; I_Frame (FI_Stackop (SI_Binop KFloat BinOp_add))

faload

; I_Heap (HI_Get (Op_getarray AIKFloat))

fastore

; I_Heap (HI_Put (Op_putarray AIKFloat))

fcmpg

; I_Frame (FI_Stackop (SI_Cmpi KFloat CmpiOp_cmpg))

fcmpl

; I_Frame (FI_Stackop (SI_Cmpi KFloat CmpiOp_cmpl))

fconst_0

; I_Frame (FI_Stackop (SI_Const KFloat (VFloat (FNum.zero))))

fconst_1

; I_Frame (FI_Stackop (SI_Const KFloat (VFloat (FNum.one))))

fconst_2

; I_Frame (FI_Stackop (SI_Const KFloat (VFloat (FNum.two))))

fdiv

; I_Frame (FI_Stackop (SI_Binop KFloat BinOp_div))

fload

; I_Frame (FI_Var (VI_Load VIKFloat var))

fload_0

; I_Frame (FI_Var (VI_Load VIKFloat var0))

fload_1

; I_Frame (FI_Var (VI_Load VIKFloat var1))

fload_2

; I_Frame (FI_Var (VI_Load VIKFloat var2))

fload_3

; I_Frame (FI_Var (VI_Load VIKFloat var3))

fmul

; I_Frame (FI_Stackop (SI_Binop KFloat BinOp_mul))

fneg

; I_Frame (FI_Stackop (SI_Unop KFloat UnOp_neg))

frem

; I_Frame (FI_Stackop (SI_Binop KFloat BinOp_rem))

freturn

; I_Return (Some KFloat)

fstore

; I_Frame (FI_Var (VI_Store VIKFloat var))

fstore_0

; I_Frame (FI_Var (VI_Store VIKFloat var0))

fstore_1

; I_Frame (FI_Var (VI_Store VIKFloat var1))

fstore_2

; I_Frame (FI_Var (VI_Store VIKFloat var2))

fstore_3

; I_Frame (FI_Var (VI_Store VIKFloat var3))

fsub

; I_Frame (FI_Stackop (SI_Binop KFloat BinOp_sub))

getfield

; I_Heap (HI_Get (Op_getfield cn fname))

getstatic

; I_Heap (HI_Get (Op_getstatic cn fname))

goto goto_w

; I_Frame (FI_Cond (CI_Goto off))

i2b

; I_Frame (FI_Stackop (SI_Cast KInt CastOp_b))

i2c

; I_Frame (FI_Stackop (SI_Cast KInt CastOp_c))

i2d

; I_Frame (FI_Stackop (SI_Cast KInt CastOp_d))

i2f

; I_Frame (FI_Stackop (SI_Cast KInt CastOp_f))

i2l

; I_Frame (FI_Stackop (SI_Cast KInt CastOp_l))

i2s

; I_Frame (FI_Stackop (SI_Cast KInt CastOp_s))

iadd

; I_Frame (FI_Stackop (SI_Binop KInt BinOp_add))

iaload

; I_Heap (HI_Get (Op_getarray AIKInt))

iand

; I_Frame (FI_Stackop (SI_Binop KInt BinOp_and))

iastore

; I_Heap (HI_Put (Op_putarray AIKInt))

iconst_0

; I_Frame (FI_Stackop (SI_Const KInt (VInt (INum.zero))))

iconst_1

; I_Frame (FI_Stackop (SI_Const KInt (VInt (INum.one))))

iconst_2

; I_Frame (FI_Stackop (SI_Const KInt (VInt (INum.const 2))))

iconst_3

; I_Frame (FI_Stackop (SI_Const KInt (VInt (INum.const 3))))

iconst_4

; I_Frame (FI_Stackop (SI_Const KInt (VInt (INum.const 4))))

iconst_5

; I_Frame (FI_Stackop (SI_Const KInt (VInt (INum.const 5))))

iconst_m1

; I_Frame (FI_Stackop (SI_Const KInt (VInt (INum.minus_one))))

idiv

; I_Frame (FI_Stackop (SI_Binop KInt BinOp_div))

if_acmpeq

; I_Frame (FI_Cond (CI_Cmp KRef CmpOp_eq off))

if_acmpne

; I_Frame (FI_Cond (CI_Cmp KRef CmpOp_ne off))

if_icmpeq

; I_Frame (FI_Cond (CI_Cmp KInt CmpOp_eq off))

if_icmpge

; I_Frame (FI_Cond (CI_Cmp KInt CmpOp_ge off))

if_icmpgt

; I_Frame (FI_Cond (CI_Cmp KInt CmpOp_gt off))

if_icmple

; I_Frame (FI_Cond (CI_Cmp KInt CmpOp_le off))

if_icmplt

; I_Frame (FI_Cond (CI_Cmp KInt CmpOp_lt off))

if_icmpne

; I_Frame (FI_Cond (CI_Cmp KInt CmpOp_ne off))

ifeq

; I_Frame (FI_Cond (CI_If KInt CmpOp_eq off))

ifge

; I_Frame (FI_Cond (CI_If KInt CmpOp_ge off))

ifgt

; I_Frame (FI_Cond (CI_If KInt CmpOp_gt off))

ifle

; I_Frame (FI_Cond (CI_If KInt CmpOp_le off))

iflt

; I_Frame (FI_Cond (CI_If KInt CmpOp_lt off))

ifne

; I_Frame (FI_Cond (CI_If KInt CmpOp_ne off))

ifnonnull

; I_Frame (FI_Cond (CI_If KRef CmpOp_ne off))

ifnull

; I_Frame (FI_Cond (CI_If KRef CmpOp_eq off))

iinc

; I_Frame (FI_Var (VI_Inc var c))

iload

; I_Frame (FI_Var (VI_Load VIKInt var))

iload_0

; I_Frame (FI_Var (VI_Load VIKInt var0))

iload_1

; I_Frame (FI_Var (VI_Load VIKInt var1))

iload_2

; I_Frame (FI_Var (VI_Load VIKInt var2))

iload_3

; I_Frame (FI_Var (VI_Load VIKInt var3))

imul

; I_Frame (FI_Stackop (SI_Binop KInt BinOp_mul))

ineg

; I_Frame (FI_Stackop (SI_Unop KInt UnOp_neg))

instanceof

; I_Heap (HI_Get (Op_instanceof rt))

invokeinterface

; I_Invoke InvokeInterface cn msig

invokespecial

; I_Invoke InvokeSpecial cn msig

invokestatic

; I_Invoke InvokeStatic cn msig

invokevirtual

; I_Invoke InvokeVirtual cn msig

ior

; I_Frame (FI_Stackop (SI_Binop KInt BinOp_or))

irem

; I_Frame (FI_Stackop (SI_Binop KInt BinOp_rem))

ireturn

; I_Return (Some KInt)

ishl

; I_Frame (FI_Stackop (SI_Binop KInt BinOp_shl))

ishr

; I_Frame (FI_Stackop (SI_Binop KInt BinOp_shr))

istore

; I_Frame (FI_Var (VI_Store VIKInt var))

istore_0

; I_Frame (FI_Var (VI_Store VIKInt var0))

istore_1

; I_Frame (FI_Var (VI_Store VIKInt var1))

istore_2

; I_Frame (FI_Var (VI_Store VIKInt var2))

istore_3

; I_Frame (FI_Var (VI_Store VIKInt var3))

isub

; I_Frame (FI_Stackop (SI_Binop KInt BinOp_sub))

iushr

; I_Frame (FI_Stackop (SI_Binop KInt BinOp_ushr))

ixor

; I_Frame (FI_Stackop (SI_Binop KInt BinOp_xor))

jsr jsr_w

; I_Frame (FI_Jsr off)

l2d

; I_Frame (FI_Stackop (SI_Cast KLong CastOp_d))

l2f

; I_Frame (FI_Stackop (SI_Cast KLong CastOp_f))

l2i

; I_Frame (FI_Stackop (SI_Cast KLong CastOp_i))

ladd

; I_Frame (FI_Stackop (SI_Binop KLong BinOp_add))

laload

; I_Heap (HI_Get (Op_getarray AIKLong))

land

; I_Frame (FI_Stackop (SI_Binop KLong BinOp_and))

lastore

; I_Heap (HI_Put (Op_putarray AIKLong))

lcmp

; I_Frame (FI_Stackop (SI_Cmpi KLong CmpiOp_cmpl))

lconst_0

; I_Frame (FI_Stackop (SI_Const KLong (VLong (LNum.zero))))

lconst_1

; I_Frame (FI_Stackop (SI_Const KLong (VLong (LNum.one))))

ldc ldc_w ldc2_w

; I_Frame (FI_Stackop (SI_Const k v))

ldiv

; I_Frame (FI_Stackop (SI_Binop KLong BinOp_div))

lload

; I_Frame (FI_Var (VI_Load VIKLong var))

lload_0

; I_Frame (FI_Var (VI_Load VIKLong var0))

lload_1

; I_Frame (FI_Var (VI_Load VIKLong var1))

lload_2

; I_Frame (FI_Var (VI_Load VIKLong var2))

lload_3

; I_Frame (FI_Var (VI_Load VIKLong var3))

lmul

; I_Frame (FI_Stackop (SI_Binop KLong BinOp_mul))

lneg

; I_Frame (FI_Stackop (SI_Unop KLong UnOp_neg))

lookupswitch

; I_Frame (FI_Cond (CI_Lookupswitch off [(INum.one , off )]))

lor

; I_Frame (FI_Stackop (SI_Binop KLong BinOp_or))

lrem

; I_Frame (FI_Stackop (SI_Binop KLong BinOp_rem))

lreturn

; I_Return (Some KLong)

lshl

; I_Frame (FI_Stackop (SI_Binop KLong BinOp_shl))

lshr

; I_Frame (FI_Stackop (SI_Binop KLong BinOp_shr))

lstore

; I_Frame (FI_Var (VI_Store VIKLong var))

lstore_0

; I_Frame (FI_Var (VI_Store VIKLong var0))

lstore_1

; I_Frame (FI_Var (VI_Store VIKLong var1))

lstore_2

; I_Frame (FI_Var (VI_Store VIKLong var2))

lstore_3

; I_Frame (FI_Var (VI_Store VIKLong var3))

lsub

; I_Frame (FI_Stackop (SI_Binop KLong BinOp_sub))

lushr

; I_Frame (FI_Stackop (SI_Binop KLong BinOp_ushr))

lxor

; I_Frame (FI_Stackop (SI_Binop KLong BinOp_xor))

monitorenter

; I_Heap (HI_Monitor Op_Lock)

monitorexit

; I_Heap (HI_Monitor Op_Unlock)

multianewarray

; I_Heap (HI_New (Op_newmultiarray rt n))

new

; I_Heap (HI_New (Op_newobject cn))

newarray

; I_Heap (HI_New (Op_newarray bt))

nop

; I_Frame (FI_Stackop (SI_Generic Op_nop))

pop

; I_Frame (FI_Stackop (SI_Generic Op_pop))

pop2

; I_Frame (FI_Stackop (SI_Generic Op_pop2))

putfield

; I_Heap (HI_Put (Op_putfield cn fname))

putstatic

; I_Heap (HI_Put (Op_putstatic cn fname))

ret

; I_Frame (FI_Ret var)

return

; I_Return None

saload

; I_Heap (HI_Get (Op_getarray AIKShort))

sastore

; I_Heap (HI_Put (Op_putarray AIKShort))

sipush

; I_Frame (FI_Stackop (SI_Const KInt (VInt (INum.const 0))))

swap

; I_Frame (FI_Stackop (SI_Generic Op_swap))

tableswitch

; I_Frame (FI_Cond (CI_Tableswitch INum.one off [off ]))
].