(*
 * Copyright (c) 2017-present,
 * Programming Research Laboratory (ROPAS), Seoul National University, Korea
 * This software is distributed under the term of the BSD-3 clause license.
 *)
(** * Abstract Array Block.  *)

Set Implicit Arguments.

Require Import ZArith Morphisms.
Require Import hpattern vgtac DLat DItv DProd DMap DPow DomBasic.
Require Import VocabA.

Module ArrInfo <: LAT.

(** Abstract type of array information is [offset * size * stride]. *)

Include Prod3 Itv Itv Itv.

Definition top : t := (Itv.top, Itv.top, Itv.top).

Definition make (o sz st : Itv.t) : t := (o, sz, st).

Definition plus_offset (x : t) (i : Itv.t) : t :=
  let '(o, s, st) := x in
  if Itv.eq_dec Itv.bot o then x else
  (Itv.plus o i, s, st).

Lemma plus_offset_mor : Proper (eq ==> Itv.eq ==> eq) plus_offset.
Proof.
unfold plus_offset; intros [[o1 s1] st1] [[o2 s2] st2] Hx i1 i2 Hi.
destruct (Itv.eq_dec Itv.bot o1), (Itv.eq_dec Itv.bot o2)
; [ by auto
  | elim f; apply Itv.eq_trans with o1; [by apply e|by apply Hx]
  | elim f; apply Itv.eq_trans with o2
    ; [by apply e|apply Itv.eq_sym; by apply Hx] |].
split; [split|]; [|by apply Hx|by apply Hx].
apply Itv.plus_mor; [by apply Hx|by apply Hi].
Qed.

Lemma plus_offset_non_bot :
  forall (x : t) (i : Itv.t) (Hx : ~ eq x bot) (Hi : ~ Itv.eq i Itv.bot),
    ~ eq (plus_offset x i) bot.
Proof.
i; destruct x as [[o sz] st]; ss.
destruct (Itv.eq_dec Itv.bot o); [by elim Hx|].
inversion FH as [[Ho Hsz] Hst]; ss.
eapply Itv.plus_non_bot; [|apply Hi|apply FH].
i; apply Hx; repeat econs; by done.
Qed.

Definition minus_offset (x : t) (i : Itv.t) : t :=
  let '(o, s, st) := x in
  if Itv.eq_dec Itv.bot o then x else
  (Itv.minus o i, s, st).

Lemma minus_offset_mor : Proper (eq ==> Itv.eq ==> eq) minus_offset.
Proof.
unfold minus_offset; intros [[o1 s1] st1] [[o2 s2] st2] Hx i1 i2 Hi.
destruct (Itv.eq_dec Itv.bot o1), (Itv.eq_dec Itv.bot o2)
; [ by auto
  | elim f; apply Itv.eq_trans with o1; [by apply e|by apply Hx]
  | elim f; apply Itv.eq_trans with o2
    ; [by apply e|apply Itv.eq_sym; by apply Hx] |].
split; [split|]; [|by apply Hx|by apply Hx].
apply Itv.minus_mor; [by apply Hx|by apply Hi].
Qed.

Lemma minus_offset_non_bot :
  forall (x : t) (i : Itv.t) (Hx : ~ eq x bot) (Hi : ~ Itv.eq i Itv.bot),
    ~ eq (minus_offset x i) bot.
Proof.
i; destruct x as [[o sz] st]; ss.
destruct (Itv.eq_dec Itv.bot o); [by elim Hx|].
inversion FH as [[Ho Hsz] Hst]; ss.
eapply Itv.minus_non_bot; [|apply Hi|apply FH].
i; apply Hx; repeat econs; by done.
Qed.

End ArrInfo.

Module ArrayBlk <: LAT.

(** ArrayBlock is a map from allocsites to array informations. *)

Include Map Allocsite ArrInfo.

Definition make (a : Allocsite.t) (o sz st : Itv.t) : t :=
  add a (ArrInfo.make o sz st) bot.

Definition extern (a : Allocsite.t) : t := add a ArrInfo.top empty.

Definition plus_offset (ab : t) (i : Itv.t) : t :=
  if Itv.eq_dec i Itv.bot then bot else
    map (fun a => ArrInfo.plus_offset a i) ab.

Lemma plus_offset_mor : Proper (eq ==> Itv.eq ==> eq) plus_offset.
Proof.
unfold eq, plus_offset; intros ab1 ab2 Hab i1 i2 Hi.
destruct (Itv.eq_dec i1 Itv.bot), (Itv.eq_dec i2 Itv.bot)
; [ by apply eq_refl
  | elim f; by eauto using Itv.eq_trans, Itv.eq_sym
  | elim f; by eauto using Itv.eq_trans, Itv.eq_sym |].
intro a. specialize Hab with a.
unfold find, map in *.
do 2 rewrite M.P.F.map_o.
remember (M.find a ab1) as opt_v1; destruct opt_v1 as [v1|]
; remember (M.find a ab2) as opt_v2; destruct opt_v2 as [v2|]; s.
- by apply ArrInfo.plus_offset_mor.
- destruct v1 as [[o1 s1] st1].
  destruct Hab as [[Ho Hs] Hst]; simpl in *.
  destruct (Itv.eq_dec Itv.bot o1).
  + split; [split|]; s; by auto.
  + elim f1; apply Itv.eq_sym; by auto.
- destruct v2 as [[o2 s2] st2].
  destruct Hab as [[Ho Hs] Hst]; simpl in *.
  destruct (Itv.eq_dec Itv.bot o2).
  + split; [split|]; s; by auto.
  + elim f1; by auto.
- by apply ArrInfo.eq_refl.
Qed.

Definition minus_offset (ab : t) (i : Itv.t) : t :=
  if Itv.eq_dec i Itv.bot then bot else
    map (fun a => ArrInfo.minus_offset a i) ab.

Lemma minus_offset_mor : Proper (eq ==> Itv.eq ==> eq) minus_offset.
Proof.
unfold eq, minus_offset; intros ab1 ab2 Hab i1 i2 Hi.
destruct (Itv.eq_dec i1 Itv.bot), (Itv.eq_dec i2 Itv.bot)
; [ by apply eq_refl
  | elim f; by eauto using Itv.eq_trans, Itv.eq_sym
  | elim f; by eauto using Itv.eq_trans, Itv.eq_sym |].
intro a. specialize Hab with a.
unfold find, map in *.
do 2 rewrite M.P.F.map_o.
remember (M.find a ab1) as opt_v1; destruct opt_v1 as [v1|]
; remember (M.find a ab2) as opt_v2; destruct opt_v2 as [v2|]; s.
- by apply ArrInfo.minus_offset_mor.
- destruct v1 as [[o1 s1] st1].
  destruct Hab as [[Ho Hs] Hst]; simpl in *.
  destruct (Itv.eq_dec Itv.bot o1).
  + split; [split|]; s; by auto.
  + elim f1; apply Itv.eq_sym; by auto.
- destruct v2 as [[o2 s2] st2].
  destruct Hab as [[Ho Hs] Hst]; simpl in *.
  destruct (Itv.eq_dec Itv.bot o2).
  + split; [split|]; s; by auto.
  + elim f1; by auto.
- by apply ArrInfo.eq_refl.
Qed.

Definition cast_array (new_st : Itv.t) (ab : t) : t :=
  let resize orig_st x := Itv.divide (Itv.times x orig_st) new_st in
  let cast_offset x :=
      let '((o, s), orig_st) := x in
      let new_o := resize orig_st o in
      let new_s := resize orig_st s in
      if Itv.eq_dec Itv.bot orig_st then x else
        (new_o, new_s, new_st) in
  map cast_offset ab.

Lemma cast_array_mor : Proper (Itv.eq ==> eq ==> eq) cast_array.
Proof.
unfold cast_array, eq; intros i1 i2 Hi ab1 ab2 Hab.
intro a. specialize Hab with a.
unfold find, map in *.
do 2 rewrite M.P.F.map_o.
remember (M.find a ab1) as opt_v1; destruct opt_v1 as [v1|]
; remember (M.find a ab2) as opt_v2; destruct opt_v2 as [v2|]; s.
- destruct v1 as [[o1 s1] st1].
  destruct v2 as [[o2 s2] st2].
  destruct Hab as [[Ho Hs] Hst]; simpl in *.
  destruct (Itv.eq_dec Itv.bot st1); destruct (Itv.eq_dec Itv.bot st2).
  + split; [split|]; s; by auto.
  + elim f; apply Itv.eq_trans with st1; by auto.
  + elim f; apply Itv.eq_trans with st2; [|apply Itv.eq_sym]; by auto.
  + split; [split|]; s.
    * apply Itv.divide_mor; [|by auto].
      apply Itv.times_mor; by auto.
    * apply Itv.divide_mor; [|by auto].
      apply Itv.times_mor; by auto.
    * assumption.
- destruct v1 as [[o1 s1] st1].
  destruct Hab as [[Ho Hs] Hst]; simpl in *.
  destruct (Itv.eq_dec Itv.bot st1).
  + split; [split|]; s; by auto.
  + elim f; apply Itv.eq_sym; by auto.
- destruct v2 as [[o2 s2] st2].
  destruct Hab as [[Ho Hs] Hst]; simpl in *.
  destruct (Itv.eq_dec Itv.bot st2).
  + split; [split|]; s; by auto.
  + elim f; by auto.
- by apply ArrInfo.eq_refl.
Qed.

Definition cast_array_int (z : Z) (ab : t) : t := cast_array (Itv.of_int z) ab.

Lemma cast_array_int_mor (z : Z) : Proper (eq ==> eq) (cast_array_int z).
Proof.
unfold cast_array_int; intros ab1 ab2 Hab.
apply cast_array_mor; [by apply Itv.eq_refl|by auto].
Qed.

Definition pow_loc_of_array (ab : t) : PowLoc.t :=
  let add_array_to_pow_loc k v acc :=
      if ArrInfo.eq_dec ArrInfo.bot v then acc else
        PowLoc.add (loc_of_allocsite k) acc in
  foldi add_array_to_pow_loc ab PowLoc.empty.

Lemma pow_loc_of_array_mor : Proper (eq ==> PowLoc.eq) pow_loc_of_array.
Proof.
unfold pow_loc_of_array; intros ab1 ab2 Hab.
apply foldi_mor; [| | |by auto|by apply PowLoc.eq_refl].
- constructor.
  + intros x; by apply PowLoc.eq_refl.
  + intros x y z; by apply PowLoc.eq_trans.
  + intros x y; by apply PowLoc.eq_sym.
- intros k1 k2 Hk v1 v2 Hv acc1 acc2 Hacc.
  destruct (ArrInfo.eq_dec ArrInfo.bot v1), (ArrInfo.eq_dec ArrInfo.bot v2)
  ; [ by auto
    | elim f; apply ArrInfo.eq_trans with v1; by auto
    | elim f; apply ArrInfo.eq_trans with v2; by auto using ArrInfo.eq_sym |].
  apply PowLoc.add_mor; [|by auto].
  by apply loc_of_allocsite_mor.
- i. destruct (ArrInfo.eq_dec ArrInfo.bot v); [by apply PowLoc.eq_refl|tauto].
Qed.

Definition pow_loc_of_struct_w_field (ab : t) (f : Field.t) : PowLoc.t :=
  let add_to_pow_loc a v acc :=
    if ArrInfo.eq_dec v ArrInfo.bot then acc else
      PowLoc.add (append_field (loc_of_allocsite a) f) acc in
  foldi add_to_pow_loc ab PowLoc.bot.

Lemma pow_loc_of_struct_w_field_mor :
  Proper (eq ==> Field.eq ==> PowLoc.eq) pow_loc_of_struct_w_field.
Proof.
intros s1 s2 Hs f1 f2 Hf. unfold pow_loc_of_struct_w_field. apply foldi2_1.
- i; dest_if_dec. elim f; by apply ArrInfo.eq_sym.
- i; dest_if_dec. elim f; by apply ArrInfo.eq_sym.
- i; dest_if_dec.
  + dest_if_dec.
    elim f; apply ArrInfo.eq_trans with v1; [by apply ArrInfo.eq_sym|by auto].
  + dest_if_dec.
    * elim f; apply ArrInfo.eq_trans with v2; by auto.
    * apply PowLoc.add_mor; [|by auto].
      apply append_field_mor; [by apply loc_of_allocsite_mor|by auto].
- by apply PowLoc.eq_refl.
- by auto.
Qed.

End ArrayBlk.