Require Import Coqlib Maps.
Require Import Classes.Equivalence.
Require Import Registers.
Require Import RTL BTL.
Require Import BTL_SEsimuref BTL_SEtheory OptionMonad.
Require Import BTL_SEimpl_prelude.

Import Notations.
Import HConsing.
Import SvalNotations.

Import ListNotations.
Local Open Scope list_scope.
Local Open Scope lazy_bool_scope.
Local Open Scope option_monad_scope.
Local Open Scope impure.


Section CSASV_apply.

Variable sis0 : sistate.

Program Definition tr_sis_ext (si : fpasv) : sistate := {|
  sis_hyp := sis0.(sis_hyp);
  sis_pre := fun ctx => sis_ok ctx sis0 /\ proj1_sig (si_ok_subst sis0 si) ctx;
  sis_sreg := fun r => match si r with
                       | Some sv => Some (sis_sv_subst sis0 sv)
                       | None => sis0 r
                       end;
  sis_smem := sis0.(sis_smem);
|}.
Solve All Obligations with
  (cbn beta; intros; rewrite sis_ok_preserved, okpred_preserved; reflexivity).

Lemma ok_tr_sis_ext ctx si:
  sis_ok ctx (tr_sis_ext si) <-> sis_ok ctx sis0 /\ proj1_sig (si_ok_subst sis0 si) ctx.

Lemma tr_sis_ext_rel_si si0 si1
  (SI_LE : incl si0.(fpa_ok) si1.(fpa_ok)):
  sis_rel (tr_sis_ext si0) (tr_sis_ext si1).

Lemma exec_seq_strict si l:
  incl (fpa_ok si) (fpa_ok (exec_seq l si)).

Definition tr_sis_ext_empty ctx:
  sistate_eq ctx sis0 (tr_sis_ext si_empty).

Lemma tr_sis_ext_get_reg si r sv:
  tr_sis_ext si r = Some sv ->
  sv = sis_sv_subst sis0 (ext si r).

Lemma tr_sis_ext_get_ireg si ir sv:
  sis_get_ireg sis0 (tr_sis_ext si) ir = Some sv ->
  sv = sis_sv_subst sis0 (ir_subst (ext si) ir).

Lemma tr_sis_ext_get_ival si iv sv:
  sis_get_ival sis0 (tr_sis_ext si) iv = Some sv ->
  sv = sis_sv_subst sis0 (iv_subst (ext si) iv).

Lemma tr_sis_ext_set_ival ctx sis1 si r iv:
  sis_set_ival r iv sis0 (tr_sis_ext si) = Some sis1 ->
  sistate_eq ctx sis1 (tr_sis_ext (si_set r (iv_subst (ext si) iv) si)).

Program Definition sis_restrict_alive (out : reg -> bool) (sis : sistate) : sistate :=
  {|
    sis_hyp := sis.(sis_hyp);
    sis_pre := fun ctx => sis_ok ctx sis;
    sis_sreg := restrict_alive out (ext sis.(sis_sreg));
    sis_smem := sis.(sis_smem);
  |}.

Lemma ok_sis_restrict_alive ctx out sis:
  sis_ok ctx (sis_restrict_alive out sis) <-> sis_ok ctx sis.

Lemma tr_sis_ext_restrict_alive ctx si out:
  sistate_eq ctx (sis_restrict_alive out (tr_sis_ext si))
                 (tr_sis sis0 (si_restrict_alive out si) None).

Definition alive_list (out : list reg) (r : reg) : bool :=
  in_dec Reg.eq r out.

End CSASV_apply.

Section SymbolicInvariants.

  Context `{HCF : HashConsingFcts}.
  Context `{HC : HashConsingHyps HCF}.
  Context `{RRULES: rrules_set}.


Section IMemSubst.
  Variable (se_mode : se_mode) (hrs0 : ristate).

Definition meminv_annot_get (an : meminv_annot_t) : ?? option store_num_t * meminv_annot_t :=
  match an with
  | Some (an0 :: an) => RET (Some an0, Some an)
  | None => RET (None, None)
  | Some nil => FAILWITH "meminv_annot_get"
  end.
Global Opaque meminv_annot_get.

Definition apply_meminv_annot (an : option store_num_t) (si : store_info) : store_info :=
  match an with
  | None => si
  | Some num => set_store_num num si
  end.

Fixpoint hrs_imem_subst_aux (an : meminv_annot_t) (im : imem) (hrs : ristate) {struct im} : ?? ristate :=
  match im with
  | nil =>
      RET hrs
  | mk_istore chk addr iargs sinfo isrc :: im =>
      DO an <~ @meminv_annot_get an;;
      let (an0, an) := an in
      DO args <~ @hrs_lr_get HCF hrs0 iargs;;
      DO src <~ @hrs_sreg_get HCF hrs0 isrc;;
      DO hrs1 <~ @hrs_set_store HCF HC RRULES se_mode (ris_smem hrs) chk addr args src
                      (apply_meminv_annot an0 sinfo) hrs;;
      hrs_imem_subst_aux an im hrs1
  end.

Lemma hrs_imem_subst_aux_rel an im hrs:
  WHEN hrs_imem_subst_aux an im hrs ~> hrs' THEN
  ris_rel se_mode hrs hrs'.

Lemma hrs_imem_subst_aux_spec ctx an im sis0 hrs sis m0
  (RR0 : ris_refines_ok ctx hrs0 sis0)
  (RR : ris_refines se_mode ctx hrs (set_smem (sis_sm_subst_trg sis0 m0) sis)):
  WHEN hrs_imem_subst_aux an im hrs ~> hrs1 THEN
  let m1 := sis_sm_subst_trg sis0 (fold_left istore_subst im m0) in
  ris_refines se_mode ctx hrs1 (set_smem m1 sis).
Global Opaque hrs_imem_subst_aux.

Definition hrs_imem_subst (an : meminv_annot_t) (im : imem) : ?? (smem * OKset.t) :=
  DO hrs <~ hrs_imem_subst_aux an im hrs0;;
  RET (ris_smem hrs, ris_pre hrs).

Lemma hrs_imem_subst_strict ctx an im:
  WHEN hrs_imem_subst an im ~> res THEN
  let (_, ok) := res in
  OKset.eval ctx ok -> ris_ok ctx hrs0.

Lemma hrs_imem_subst_spec ctx sis0 an im
  (RR : ris_refines se_mode ctx hrs0 sis0):
  let sm := sis_sm_subst_trg sis0 (imem_subst im) in
  WHEN hrs_imem_subst an im ~> res THEN
  let (m, ok) := res in
  ok_equivp True (sis_ok ctx sis0 /\ alive (eval_smem ctx sm)) (OKset.eval ctx ok) (se_ok_equiv se_mode) /\
  (OKset.eval ctx ok -> smem_equiv ctx m sm).
Global Opaque hrs_imem_subst.

Definition hrs_imem_subst_isol an (im : imem) : ?? (smem * OKset.t) :=
  let hrs_mem := {|
    ris_smem := ris_smem hrs0;
    ris_input_init := Some false; ris_sreg := PTree.empty _;
    ris_pre := OKset.empty;
  |} in
  DO hrs <~ hrs_imem_subst_aux an im hrs_mem;;
  RET (ris_smem hrs, ris_pre hrs).

Lemma hrs_imem_subst_isol_spec ctx sis0 an im
  (RR : ris_refines_ok ctx hrs0 sis0):
  let sm := sis_sm_subst_trg sis0 (imem_subst im) in
  WHEN hrs_imem_subst_isol an im ~> res THEN
  let (m, ok) := res in
  OKset.eval ctx ok ->
  alive (eval_smem ctx sm) /\ smem_equiv ctx m sm.
Global Opaque hrs_imem_subst_isol.

End IMemSubst.


Section TrSingle.
  Variable (m : se_mode).

Definition hrs_sv_set r sv (hrs: ristate): ?? ristate :=
  RET (ris_sreg_set hrs (red_PTree_set r sv hrs)).

Definition hrs_ival_set (hrs hrs_old: ristate) (r: reg) (iv: ival): ?? ristate :=
  match iv with
  | Ireg ir =>
      DO sv <~ @hrs_ir_get HCF hrs hrs_old ir;;
      hrs_sv_set r sv hrs
  | Iop rop args =>
      DO lsv <~ @hrs_lir_get HCF hrs hrs_old args;;
      @hrs_rsv_set HCF HC RRULES m r rop lsv None hrs_old.(ris_smem) hrs
  end.

Lemma hrs_ival_set_spec ctx sis0 sis1 hrs hrs_old r iv
  (RR0: ris_refines_ok ctx hrs_old sis0)
  (RR1: ris_refines_ok ctx hrs sis1):
  WHEN hrs_ival_set hrs hrs_old r iv ~> hrs' THEN
  exists sis2,
    sis_set_ival r iv sis0 sis1 = Some sis2 /\
    ris_refines m ctx hrs' sis2.

Lemma hrs_ival_set_rel hrs hrs_old r iv:
  WHEN hrs_ival_set hrs hrs_old r iv ~> hrs' THEN
  ris_rel m hrs hrs'.

Global Opaque hrs_ival_set hrs_sv_set.

Applying a sequence of invariant operations

Fixpoint exec_seq_imp (hrs hrs_old: ristate) (l: list (reg*ival)): ?? ristate :=
  match l with
  | nil => RET hrs
  | (r,iv)::l =>
      DO hrs' <~ hrs_ival_set hrs hrs_old r iv;;
      exec_seq_imp hrs' hrs_old l
  end.

Lemma exec_seq_imp_rel hrs hrs_old l:
  WHEN exec_seq_imp hrs hrs_old l ~> hrs' THEN
  ris_rel m hrs hrs'.

Lemma exec_seq_imp_spec ctx sis0 si hrs hrs_old l
  (RR0: ris_refines_ok ctx hrs_old sis0)
  (RR1: ris_refines_ok ctx hrs (tr_sis_ext sis0 si)):
  WHEN exec_seq_imp hrs hrs_old l ~> hrs' THEN
  ris_refines m ctx hrs' (tr_sis_ext sis0 (exec_seq l si)).
Global Opaque exec_seq_imp.

Building a PTree from the compact invariants representation, only on live variables

Fixpoint build_alive_imp (loutputs: list reg) (hrs: ristate): ?? (PTree.t sval) :=
  match loutputs with
  | nil => RET (PTree.empty sval)
  | r :: tl =>
      DO sreg <~ build_alive_imp tl hrs;;
      DO hsv <~ @hrs_sreg_get HCF hrs r;;
      RET (PTree.set r hsv sreg)
  end.

Lemma build_alive_imp_spec ctx loutputs hrs sis r
  (RR: ris_refines_ok ctx hrs sis):
  WHEN build_alive_imp loutputs hrs ~> sreg THEN
  optsv_simu ctx (sreg ! r) (restrict_alive (alive_list loutputs) (ext sis) r).

Global Opaque build_alive_imp.

Applying a csasv

Definition tr_hrs_single (hrs: ristate) (csi: csasv): ?? ristate :=
  DO hrs' <~ exec_seq_imp hrs hrs csi.(aseq);;
  DO sreg <~ build_alive_imp (Regset.elements csi.(outputs)) hrs';;
  RET (ris_sreg_set hrs' sreg).

Lemma tr_hrs_single_rel hrs csi:
  WHEN tr_hrs_single hrs csi ~> hrs' THEN
  ris_rel m hrs hrs'.

Section TrSingleSpec.
  Variable (ctx : iblock_common_context).

Theorem tr_hrs_single_spec hrs sis csi
  (RR: ris_refines_ok ctx hrs sis):
  WHEN tr_hrs_single hrs csi ~> hrs' THEN
  ris_refines m ctx (ris_input_init_set hrs' None) (tr_sis sis (siof csi) None).

Global Opaque tr_hrs_single.

Corollary tr_hrs_single_spec_input_init hrs sis csi ini
  (RR: ris_refines_ok ctx hrs sis):
  WHEN tr_hrs_single hrs csi ~> hrs' THEN
  ris_refines m ctx (ris_input_init_set hrs' (Some ini)) (tr_sis sis (siof csi) (Some ini)).

Corollary tr_hrs_single_correct hrs sis csi
  (SIM: se_ok_check m = true)
  (RR: ris_refines_ok ctx hrs sis):
  WHEN tr_hrs_single hrs csi ~> hrs' THEN
  ris_refines_ok ctx (ris_input_init_set hrs' None) (tr_sis sis (siof csi) None).



Definition hrs_ini_states (csix : invariants) : ?? ristate * ristate :=
  DO hrsH <~ tr_hrs_single ris_empty (history csix);;
  DO hrsHG <~ tr_hrs_single hrsH (glue csix);;
  let hrsT := ris_input_init_set hrsHG (Some true) in
  DO memS <~ hrs_imem_subst m hrsT None (meminv csix);;
  let (memS, okS) := memS in
  let hrsS := {|
    ris_smem := memS;
    ris_input_init := Some false;
    ris_sreg := ris_sreg hrsH;
    ris_pre := okS;
  |} in
  RET (hrsS, hrsT).

Lemma hrs_ini_states_spec csix:
  WHEN hrs_ini_states csix ~> r THEN
  let (hrsS, hrsT) := r in
  ris_refines m ctx hrsS (sis_source csix) /\
  ris_refines m ctx hrsT (sis_target csix).

End TrSingleSpec.
End TrSingle.

Memory invariant meminv_sfv_set

Definition meminv_rfv (im : node -> imem) (rfv : rfval) : ?? list imem :=
  match rfv with
  | Sgoto pc => RET [im pc]
  | Scall _ _ _ _ pc | Sbuiltin _ _ _ pc =>
      if is_nil (im pc)
      then RET [nil]
      else FAILWITH "meminv_rfv: memory invariant at Call / Builtin"
  | Stailcall _ _ _ | Sreturn _ => RET [nil]
  | Sjumptable _ lpc => RET (map im lpc)
  end.

Lemma meminv_rfv_spec im rfv:
  WHEN meminv_rfv im rfv ~> res THEN
  let (imP, imS) := meminv_sfv_set im (sfval_of_rsval rfv) in
  imP /\ forall m : imem, imS m <-> In m res.
Global Opaque meminv_rfv.

Register invariants si_sfv_set

Definition si_rfv (gm : node -> csasv) rfv: ?? list csasv :=
  match rfv with
  | Sgoto pc => RET [gm pc]
  | Scall sig svid args res pc =>
      if test_clobberable (gm pc) res
      then RET [csi_remove res (gm pc)]
      else FAILWITH "ri_sfv: Scall res not clobberable"
  | Sbuiltin ef args bres pc =>
      match reg_builtin_res bres with
      | Some r =>
          if test_clobberable (gm pc) r
          then RET [csi_remove r (gm pc)]
          else FAILWITH "ri_sfv: Sbuiltin res not clobberable"
      | None =>
          if test_csifreem (gm pc)
          then RET [gm pc]
          else FAILWITH "ri_sfv: Sbuiltin memory dependent"
      end
  | Stailcall _ _ _ | Sreturn _ => RET []
  | Sjumptable sv lpc => RET (map gm lpc)
  end.

Lemma si_rfv_spec gm rfv:
  WHEN si_rfv gm rfv ~> res THEN
  let (siP, siS) := si_sfv_set gm (sfval_of_rsval rfv) in
  siP /\ forall si : csasv, siS si <-> In si res.
Global Opaque si_rfv.
End SymbolicInvariants.