Require Import Logic.
Require Import Relations.
Require Import List.
Require Import Common.
Require Import ValuesNTypes.
Require Import ProgramStructures.
Require Import Heap.
Require Import ZArith.
Require Import Program.
Require Import RuntimeStructures.
Require Import AllStructures.
Require Import Sem_Monitor.

Module Type SEM_HEAP.
  Declare Module M_AllStructures : ALL_STRUCTURES.

  Declare Module M_Sem_Monitor : SEM_MONITOR
    with Module M_AllStructures := M_AllStructures.

  Import M_AllStructures.
  Import M_Program.M_ProgramStructures.M_ValuesAndTypes.
  Import M_Program.M_ProgramStructures.
  Import M_ProgramStructuresFacts.
  Import M_Program.
  Import M_RuntimeStructures.M_Heap.
  Import M_RuntimeStructures.

  Open Local Scope Z_scope.
  Import List.ListNotations.

  Inductive semGet: TGetOp → TProgram → TThreadId → THeap → (list TValue) → TResultOrException (list TValue) → Prop :=
  | SemGet_getstatic: ∀ cn field p thid h v,

    getStaticField h thid cn field = Some v →
    semGet (Op_getstatic cn field) p thid h [] (Result [v])

  | SemGet_getfield: ∀ cn field p thid h loc obj v,
    
    
    loc ≠ null →
    get h thid loc = HV_Object obj →
    getObjectField obj field = Some v →
    semGet (Op_getfield cn field) p thid h [VRef loc] (Result [v])

  | SemGet_getfield_null: ∀ cn fn p thid h,
    semGet (Op_getfield cn fn) p thid h [VRef null] (Exception StandardNames.NullPointerException)

  | SemGet_array: ∀ aik t p thid h loc size arr idx v av,
    loc ≠ null →
    get h thid loc = HV_Array arr →
    getArrayComponentType arr = t →
    arrayKindOfType t = aik →
    kindOfValue v = kindOfArrayKind aik →
    getArraySize arr = size →
    validIndex size idx →
    getArrayCell arr idx = Some av →
    transformAToValue av = v →
    semGet (Op_getarray aik) p thid h [VInt idx; VRef loc] (Result [v])

  | SemGet_array_null: ∀ aik p thid h idx,
    semGet (Op_getarray aik) p thid h [VInt idx; VRef null] (Exception StandardNames.NullPointerException)

  | SemGet_array_out: ∀ aik t p thid h loc size arr idx,
    loc ≠ null →
    get h thid loc = HV_Array arr →
    getArrayComponentType arr = t →
    arrayKindOfType t = aik →
    getArraySize arr = size →
    ¬ validIndex size idx →
    semGet (Op_getarray aik) p thid h [VInt idx; VRef loc] (Exception StandardNames.ArrayIndexOutOfBoundsException)

  | SemGet_arrayLength: ∀ p thid h loc arr size,
    loc ≠ null →
    get h thid loc = HV_Array arr →
    getArraySize arr = size →
    semGet Op_array_length p thid h [VRef loc] (Result [VInt size])

  | SemGet_arrayLength_null: ∀ p thid h,
    semGet Op_array_length p thid h [VRef null] (Exception StandardNames.NullPointerException)

  | SemGet_instanceOf_true: ∀ required_rt p thid h loc actual_rt,
    loc ≠ null →
    getReferenceType h thid loc = Some actual_rt →
    subtypeRef p actual_rt required_rt →
    semGet (Op_instanceof required_rt) p thid h [VRef loc] (Result [VInt M_Numeric_Int.one])

  | SemGet_instanceOf_false: ∀ required_rt p thid h loc actual_rt,
    loc ≠ null →
    getReferenceType h thid loc = Some actual_rt →
    ¬ subtypeRef p actual_rt required_rt →
    semGet (Op_instanceof required_rt) p thid h [VRef loc] (Result [VInt M_Numeric_Int.zero])
  
  | SemGet_instanceOf_null: ∀ required_rt p thid h,
    semGet (Op_instanceof required_rt) p thid h [VRef null] (Result [VInt M_Numeric_Int.zero])
  
  | SemGet_checkCast_true: ∀ required_rt p thid h loc actual_rt,
    loc ≠ null →
    getReferenceType h thid loc = Some actual_rt →
    subtypeRef p actual_rt required_rt →
    semGet (Op_checkcast required_rt) p thid h [VRef loc] (Result [VRef loc])

  | SemGet_checkCast_false: ∀ required_rt p thid h loc actual_rt,
    loc ≠ null →
    getReferenceType h thid loc = Some actual_rt →
    ¬ subtypeRef p actual_rt required_rt →
    semGet (Op_checkcast required_rt) p thid h [VRef loc] (Exception StandardNames.ClassCastException)
  
  | SemGet_checkCast_null: ∀ required_rt p thid h,
    semGet (Op_checkcast required_rt) p thid h [VRef null] (Result [VRef null])
  .

  Inductive semPut: TPutOp → TProgram → TThreadId → (list TValue × THeap) → TResultOrException (list TValue × THeap) → Prop :=
  | SemPut_putstatic: ∀ cn field p thid h h' v,
    setStaticField h thid cn field v = Some h' →
    semPut (Op_putstatic cn field) p thid ([v], h) (Result ([], h'))

  | SemPut_putfield: ∀ cn fn p thid h h' loc obj obj' v,
    
    loc ≠ null →
    get h thid loc = HV_Object obj →
    setObjectField obj fn v = obj' →
    set h thid loc (HV_Object obj') = h' →
    semPut (Op_putfield cn fn) p thid ([v; VRef loc], h) (Result ([], h'))

  | SemPut_putfield_null: ∀ cn fn p thid h v,
    semPut (Op_putfield cn fn) p thid ([VRef null; v], h) (Exception StandardNames.NullPointerException)

  | SemPut_array: ∀ aik p t thid h h' loc size arr arr' idx v av,
    get h thid loc = HV_Array arr →
    getArrayComponentType arr = t →
    arrayKindOfType t = aik →
    kindOfValue v = kindOfArrayKind aik →
    getArraySize arr = size →
    validIndex size idx →
    transformAFromValue t v = Some av →
    arr' = setArrayCell arr idx av →
    h' = set h thid loc (HV_Array arr') →
    semPut (Op_putarray aik) p thid ([v; VInt idx; VRef loc], h) (Result ([], h'))
  

  | SemPut_array_null: ∀ aik p thid h idx v,
    kindOfValue v = kindOfArrayKind aik →
    semPut (Op_putarray aik) p thid ([v; VInt idx; VRef null], h) (Exception StandardNames.NullPointerException)

  | SemPut_array_indexOutOfBounds: ∀ aik p t thid h loc size arr idx v,
    get h thid loc = HV_Array arr →
    getArrayComponentType arr = t →
    arrayKindOfType t = aik →
    kindOfValue v = kindOfArrayKind aik →
    getArraySize arr = size →
    ¬ validIndex size idx →
    semPut (Op_putarray aik) p thid ([v; VInt idx; VRef loc], h) (Exception StandardNames.ArrayIndexOutOfBoundsException)
  .

  Parameter makeMultiArray: TReferenceType → list TValue → TThreadId → THeap → (THeap × TLoc).

  Inductive madeMultiArrayInd: TType → list TValue → TThreadId → THeap → THeap → TAValue → Prop :=
  | MadeMultiArray_step:
    ∀ t size sizes thid h h' loc arr,
    get h' thid loc = HV_Array arr →
    getArrayComponentType arr = t →
    getArraySize arr = size →
    (∀ i inner_val, validIndex (getArraySize arr) i →
       getArrayCell arr i = Some inner_val →
       madeMultiArrayInd t sizes thid h h' inner_val) →
    madeMultiArrayInd (ReferenceType (RTArray t)) (cons (VInt size) sizes) thid h h' (VARef loc)

  | MadeMultiArray_end:
    ∀ t thid h h',
    madeMultiArrayInd t nil thid h h' (defaultArrayValueForType t)
  .

  Axiom PmakeMultiArray: ∀ rt sizes thid h h' loc,
    makeMultiArray rt sizes thid h = (h', loc) ↔ madeMultiArrayInd (ReferenceType rt) sizes thid h h' (VARef loc).

  Inductive semNew: TNewOp → TProgram → TThreadId → (list TValue × THeap) → TResultOrException (list TValue × THeap) → Prop :=
  | SemNew_object: ∀ p cn class thid loc obj h h',
    getClass p cn = Some class →
    initObject (getEmptyObject class) = obj →
    loc = freshLocation h →
    h' = set h thid loc (HV_Object obj) →
    semNew (Op_newobject cn) p thid ([], h) (Result ([VRef loc], h'))

  | SemNew_array: ∀ p bt thid loc arr size h h',
    initArray (BaseType bt) size = arr →
    freshLocation h = loc →
    set h thid loc (HV_Array arr) = h' →
    semNew (Op_newarray bt) p thid ([VInt size], h) (Result ([VRef loc], h'))

  | SemNew_array_neg: ∀ p bt thid size h,
    M_Numeric_Int.toZ size < 0 →
    semNew (Op_newarray bt) p thid ([VInt size], h) (Exception StandardNames.NegativeArraySizeException)

  | SemNew_refarray: ∀ p rt thid loc arr size h h',
    M_Numeric_Int.toZ size ≥ 0 →
    initArray (ReferenceType rt) size = arr →
    freshLocation h = loc →
    set h thid loc (HV_Array arr) = h' →
    semNew (Op_newarray_ref rt) p thid ([VInt size], h) (Result ([VRef loc], h'))

  | SemNew_refarray_neg: ∀ p rt thid size h,
    M_Numeric_Int.toZ size < 0 →
    semNew (Op_newarray_ref rt) p thid ([VInt size], h) (Exception StandardNames.NegativeArraySizeException)

  | SemNew_multiarray: ∀ p rt dimensions thid loc sizes h h',
    (dimensions > 0)%nat →
    dimensions = length sizes →
    (∀ size, In (VInt size) sizes → M_Numeric_Int.toZ size ≥ 0) →
    makeMultiArray rt sizes thid h = (h', loc) →
    semNew (Op_newmultiarray rt dimensions) p thid (sizes, h) (Result ([VRef loc], h'))

  | SemNew_multiarray_negativeSize: ∀ p rt dimensions thid sizes h,
    (dimensions > 0)%nat →
    dimensions = length sizes →
    (∃ size, In (VInt size) sizes ∧ M_Numeric_Int.toZ size < 0) →
    semNew (Op_newmultiarray rt dimensions) p thid (sizes, h) (Exception StandardNames.NegativeArraySizeException)
  .

  Inductive semHeap (p: TProgram) (code: TCode): THeapInstr → TThreadId → ((list TValue) × THeap) → TResultOrException ((list TValue) × THeap) → Prop:=
  | SemHeap_get: ∀ get_op thid vs vs' h,
    semGet get_op p thid h vs (Result vs') →
    semHeap p code (HI_Get get_op) thid (vs, h) (Result (vs', h))

  | SemHeap_put: ∀ put_op thid vs h vs' h',
    semPut put_op p thid (vs, h) (Result (vs', h')) →
    semHeap p code (HI_Put put_op) thid (vs, h) (Result (vs', h'))

  | SemHeap_new: ∀ new_op thid vs h vs' h',
    semNew new_op p thid (vs, h) (Result (vs', h')) →
    semHeap p code (HI_New new_op) thid (vs, h) (Result (vs', h'))

  | SemHeap_monitor: ∀ mon_op thid h h' loc,
    M_Sem_Monitor.semMonitor mon_op thid loc h (Result h') →
    semHeap p code (HI_Monitor mon_op) thid ([VRef loc], h) (Result ([], h'))
  .
End SEM_HEAP.