Module RefinesInjectedCodes

Require Import Coqlib.
Require Import Maps.
Require Import Ast.
Require Import Integers.
Require Import Pointers.
Require Import Values.
Require Import Mem.
Require Import Events.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import Libtactics.
Require Import INJECT.
Require Import Classical.
Require Import Utils.
Require Import Permissions Emem MemoryMachine RTLinject RefinesDefs RefinesUtils.
Require Import RefinesRules.
Require Import RefinesRules2.
Require Import RefinesRules3.
Require Import DataStructures Common InjectedCode GCthread.
Require Import Utf8.
Require Import AllRefinesRulesAux.

Require MIRexample.


Ltac build_refines_fold f trm :=
  match trm with
    | ?x => f x
    | Sseq ?s1 ?s2 =>
      let h := build_refines_fold f s1 in
        constr:(refines_seq_left _ s2 _ h)
    | Sseq ?s1 ?s2 =>
      let h := build_refines_fold f s2 in
        constr:(refines_seq_right s1 _ _ h)
    | Sbranch ?s1 ?s2 =>
      let h := build_refines_fold f s1 in
        constr:(refines_branch_left _ s2 _ h)
    | Sbranch ?s1 ?s2 =>
      let h := build_refines_fold f s2 in
        constr:(refines_branch_right s1 _ _ h)
    | Sifthenelse ?c ?a ?s1 ?s2 =>
      let h := build_refines_fold f s1 in
        constr:(refines_if1 c a s1 _ s2 h)
    | Sifthenelse ?c ?a ?s1 ?s2 =>
      let h := build_refines_fold f s2 in
        constr:(refines_if2 c a s1 s2 _ h)
    | Srepeat ?b ?c ?a =>
      let h := build_refines_fold f b in
        constr:(refines_repeat_congruence b _ c a h)
    | Swhile ?c ?a ?b =>
      let h := build_refines_fold f b in
        constr:(while_repeat_congruence b _ c a h)
    | Sloop ?s =>
      let h := build_refines_fold f s in
        constr:(refines_loop _ _ h)
    | Satomic ?b ?s =>
      let h := build_refines_fold f s in
        constr:(refines_atomic b _ _ h (refl_equal _))
  end.

Ltac refines_fold f :=
  match goal with
    | |- refines ?stmt _ =>
      let h := build_refines_fold f stmt in
        apply refines_trans with (1:=h)
  end.

Ltac build_refines_fold_not_conservative f trm :=
  match trm with
    | ?x => f x
    | Sseq ?s1 ?s2 =>
      let h := build_refines_fold_not_conservative f s1 in
        constr:(refines_seq_left _ s2 _ h)
    | Sseq ?s1 ?s2 =>
      let h := build_refines_fold_not_conservative f s2 in
        constr:(refines_seq_right s1 _ _ h)
    | Sloop ?s =>
      let h := build_refines_fold_not_conservative f s in
        constr:(refines_loop _ _ h)
    | Sbranch ?s1 ?s2 =>
      let h := build_refines_fold_not_conservative f s1 in
        constr:(refines_branch_left _ s2 _ h)
    | Sbranch ?s1 ?s2 =>
      let h := build_refines_fold_not_conservative f s2 in
        constr:(refines_branch_right s1 _ _ h)

  end.

Ltac refines_fold_not_conservative f :=
  match goal with
    | |- refines ?stmt _ =>
      let h := build_refines_fold_not_conservative f stmt in
        apply refines_trans with (1:=h)
  end.


Ltac build_refines_branch trm :=
  match trm with
    | Sseq ?s3 (Sbranch ?s1 ?s2) =>
      constr:(refines_seq_branch s3 s1 s2)
    | Sseq (Sbranch ?s1 ?s2) ?s3 =>
      constr:(refines_branch_seq s1 s2 s3)
    | Sbranch (Sbranch ?s1 ?s2) ?s3 =>
      constr:(refines_branch_assoc s1 s2 s3)
    | Sbranch ?s1 (Sbranch ?s1 ?s2) =>
      constr:(refines_branch_dup s1 s2)
  end.

Ltac refines_branch := refines_fold build_refines_branch.


Ltac build_refines_remove_freeperm trm :=
  match trm with
    | Sseq ?s Sfreeperm =>
      constr:(refines_remove_freeperm_right s)
  end.

Ltac refines_remove_freeperm := refines_fold build_refines_remove_freeperm.


Ltac build_refines_remove_leak trm :=
  match trm with
    | Sseq (Leak ?l ?r1 ?r2) ?s =>
      constr:(refines_remove_leak_left l r1 r2 s)
    | Sseq ?s (Leak ?l ?r1 ?r2) =>
      constr:(refines_remove_leak_right l r1 r2 s)
  end.

Ltac refines_remove_leak := refines_fold build_refines_remove_leak.

Ltac build_freeperm_next trm :=
  match trm with
    | Sseq Sfreeperm (Sseq ?s1 ?s2) =>
      constr:(refines_seq_assoc1 Sfreeperm s1 s2)
  end.

Ltac refines_freeperm_next := refines_fold build_freeperm_next.

Ltac build_refines_swap_freeperm trm :=
  match trm with
    | Sseq Sfreeperm ?s =>
      constr:(refines_remove_perm s (refl_equal _))
  end.

Ltac refines_swap_freeperm := refines_fold build_refines_swap_freeperm.

Ltac build_refines_fold_atomic stmt1 stmt2 hr trm :=
  match trm with
    | Satomic ?b stmt1 => constr:(refines_atomic' b stmt1 stmt2 hr (refl_equal _))
    | Sseq ?s1 ?s2 =>
      let h := build_refines_fold_atomic stmt1 stmt2 hr s1 in
        constr:(refines_seq_left _ s2 _ h)
    | Sseq ?s1 ?s2 =>
      let h := build_refines_fold_atomic stmt1 stmt2 hr s2 in
        constr:(refines_seq_right s1 _ _ h)
    | Sbranch ?s1 ?s2 =>
      let h := build_refines_fold_atomic stmt1 stmt2 hr s1 in
        constr:(refines_branch_left _ s2 _ h)
    | Sbranch ?s1 ?s2 =>
      let h := build_refines_fold_atomic stmt1 stmt2 hr s2 in
        constr:(refines_branch_right s1 _ _ h)
    | Sloop ?s =>
      let h := build_refines_fold_atomic stmt1 stmt2 hr s in
        constr:(refines_loop _ _ h)
    | Satomic ?b ?s =>
      let h := build_refines_fold_atomic stmt1 stmt2 hr s in
        constr:(refines_atomic b _ _ h (refl_equal _))
  end.

Ltac refines_replace_in_atomic stmt1 stmt2 :=
  unfold reg;
  let h:= fresh in
  (assert (h:refines_in_atomic stmt1 stmt2);
  [ idtac|
    match goal with
    | |- refines ?stmt _ =>
      let h2 := build_refines_fold_atomic stmt1 stmt2 h stmt in
        apply refines_trans with (1:=h2)
  end]).

Ltac refines_replace_in_atomic_with_lemma h :=
  unfold reg;
  match type of h with
    | refines_in_atomic ?stmt1 ?stmt2 =>
    match goal with
    | |- refines ?stmt _ =>
      let h2 := build_refines_fold_atomic stmt1 stmt2 h stmt in
        apply refines_trans with (1:=h2)
   end
  end.


Ltac build_refines_fold_replace stmt1 stmt2 hr trm :=
  match trm with
    | stmt1 => constr:(hr)
    | Sseq ?s1 ?s2 =>
      let h := build_refines_fold_replace stmt1 stmt2 hr s1 in
        constr:(refines_seq_left _ s2 _ h)
    | Sseq ?s1 ?s2 =>
      let h := build_refines_fold_replace stmt1 stmt2 hr s2 in
        constr:(refines_seq_right s1 _ _ h)
    | Sbranch ?s1 ?s2 =>
      let h := build_refines_fold_replace stmt1 stmt2 hr s1 in
        constr:(refines_branch_left _ s2 _ h)
    | Sbranch ?s1 ?s2 =>
      let h := build_refines_fold_replace stmt1 stmt2 hr s2 in
        constr:(refines_branch_right s1 _ _ h)
    | Sloop ?s =>
      let h := build_refines_fold_replace stmt1 stmt2 hr s in
        constr:(refines_loop _ _ h)
    | Satomic ?b ?s =>
      let h := build_refines_fold_replace stmt1 stmt2 hr s in
        constr:(refines_atomic b _ _ h (refl_equal _))
  end.

Ltac refines_replace stmt1 stmt2 :=
  unfold reg;
  let h:= fresh in
  (assert (h:refines stmt1 stmt2);
  [ idtac|
    match goal with
    | |- refines ?stmt _ =>
      let h2 := build_refines_fold_replace stmt1 stmt2 h stmt in
        apply refines_trans with (1:=h2)
  end]).

Ltac build_refines_remove stmt trm :=
  match trm with
    | Sseq stmt ?s2 =>
        constr:(refines_dead_code stmt s2 (refl_equal _) (refl_equal _) (refl_equal _))
    | Sseq ?s1 ?s2 =>
      let h := build_refines_remove stmt s2 in
        constr:(refines_seq_right s1 _ _ h)
  end.

Ltac refines_remove_dead stmt1 :=
  match goal with
    | |- refines ?stmt _ =>
      let h2 := build_refines_remove stmt1 stmt in
        apply refines_trans with (1:=h2)
  end.



Ltac build_refines_abort trm :=
  match trm with
    | Sseq ?s (Sabort ?af ?r ?e) =>
      constr:(refines_stmt_abort s af e r (refl_equal _))
    | Sseq (Sabort ?af ?r ?e) ?s =>
      constr:(refines_abort_stmt s af r e)
    | Sloop (Sbranch (Sabort ?af ?r ?e) ?stmt) =>
      constr:(refines_loop_branch_abort af r e stmt)
    | Satomic true (Sabort Atomic ?r ?msg) =>
      constr:(refines_depromotes_abort r msg)
  end.

Ltac refines_abort := refines_fold build_refines_abort.


Ltac build_refines_seq_assoc trm :=
  match trm with
    | Sseq (Sseq ?s1 ?s2) ?s3 =>
      constr:(refines_seq_assoc2 s1 s2 s3)
    | Sseq ?s Sskip =>
      constr:(refines_stmt_skip s)
    | Sseq Sskip ?s =>
      constr:(refines_skip_stmt s)
  end.

Ltac build_refines_seq_assoc_right trm :=
  match trm with
    | Sseq ?s3 (Sseq ?s1 ?s2) =>
      constr:(refines_seq_assoc1 s3 s1 s2)
  end.

Ltac refines_seq_assoc := refines_fold build_refines_seq_assoc.
Ltac refines_seq_assoc_inv := refines_fold build_refines_seq_assoc_right.

Ltac refines_fold2 f :=
  match goal with
    | |- refines _ ?stmt =>
      let h := build_refines_fold f stmt in
        apply refines_trans with (2:=h)
  end.

Ltac refines_seq_assoc_right := refines_fold2 build_refines_seq_assoc_right.

Ltac build_refines_if trm :=
  match trm with
    | Sifthenelse ?cond ?args ?ifso ?ifnot =>
        constr:(refines_if_with_branch cond args ifso ifnot)
  end.

Ltac refines_if :=
  refines_fold build_refines_if;
  repeat refines_seq_assoc;
  simpl negate_condition.

Ltac build_refines_repeat trm :=
  match trm with
    | Srepeat ?b ?c ?a => constr:(refines_repeat b c a)
  end.

Ltac refines_repeat :=
  refines_fold build_refines_repeat;
  repeat refines_seq_assoc;
  simpl negate_condition.

Ltac build_refines_while trm :=
  match trm with
    | Swhile ?b ?c ?a => constr:(refines_while a b c)
  end.

Ltac refines_while :=
  refines_fold build_refines_while;
  repeat refines_seq_assoc;
  simpl negate_condition.

Ltac build_refines_swap_assert trm :=
  match trm with
    | Sseq ?s1 (Sseq (Sassume ?c ?a) ?s2) =>
      let h1 := constr:(refines_seq_assoc1 s1 (Sassume c a) s2) in
      let h2 := build_refines_swap_assert (Sseq s1 (Sassume c a)) in
      let h3 := constr:(refines_seq_left _ s2 _ h2) in
        constr:(refines_trans _ _ _ h1 h3)
    | Sseq ?s (Sassume ?c ?a) =>
      constr:(refines_swap_assert s c a (refl_equal _) (refl_equal _))
  end.

Ltac refines_swap_assert :=
  refines_fold build_refines_swap_assert;
  repeat refines_seq_assoc.

Ltac build_refines_cas trm :=
  match trm with
    | (Sseq
      (Satomicmem ?r Op.AScas (?ptr::?new::?old::nil) ?dst)
      (Sseq (Sassume (Op.Ccomp Cne) (?dst::?old::nil)) ?stmt)) =>
    let h1 := constr:(refines_cas_fail_stronger r ptr new old dst) in
      constr:(refines_trans _ _ _ (refines_seq_assoc1 _ _ _)
               (refines_seq_left _ stmt _ h1))
    | (Sseq
      (Satomicmem ?r Op.AScas (?ptr::?new::?old::nil) ?dst)
      (Sseq (Sassume (Op.Ccomp Ceq) (?dst::?old::nil)) ?stmt)) =>
    let h1 := constr:(refines_cas_success r ptr new old dst
      (eq_refl _) (eq_refl _) (eq_refl _)) in
      constr:(refines_trans _ _ _ (refines_seq_assoc1 _ _ _)
               (refines_seq_left _ stmt _ h1))
    | (Sseq
       (Satomicmem ?r Op.AScas (?ptr::?new::?old::nil) ?dst)
       (Sassume (Op.Ccomp Cne) (?dst::?old::nil))) =>
         constr:(refines_cas_fail_stronger r ptr new old dst)
    | (Sseq
        (Satomicmem ?r Op.AScas (?ptr::?new::?old::nil) ?dst)
        (Sassume (Op.Ccomp Ceq) (?dst::?old::nil))) =>
    constr:(refines_cas_success r ptr new old dst
      (eq_refl _) (eq_refl _) (eq_refl _))
  end.

Ltac refines_cas:=
  refines_fold build_refines_cas;
  repeat refines_seq_assoc.


Ltac build_refines_dead_code trm :=
  match trm with
    | Sseq ?s1 (Sreturn ?a) =>
        constr:(refines_dead_code_return s1 a (refl_equal _) (refl_equal _) (refl_equal _))
    | Sseq ?s1 ?s2 =>
        constr:(refines_dead_code s1 s2 (refl_equal _) (refl_equal _) (refl_equal _))
    | Sseq ?s1 (Sseq ?s2 ?s3) =>
      let h1 := constr:(refines_seq_assoc1 s1 s2 s3) in
      let h2 := build_refines_dead_code (Sseq s1 s2) in
      let h3 := constr:(refines_seq_left _ s3 _ h2) in
        constr:(refines_trans _ _ _ h1 h3)
  end.

Ltac refines_dead_code :=
  refines_fold_not_conservative build_refines_dead_code.


Ltac build_refines_promotes_fence trm :=
  match trm with
    | Sfence ?r => constr:(refines_promotes_fence true r)
  end.

Ltac refines_promotes_fence :=
  refines_fold build_refines_promotes_fence;
  repeat refines_seq_assoc.


Ltac build_refines_promotes_abort trm :=
  match trm with
    | (Sseq (Sfence true) (Sabort Interleaved ?r ?msg)) =>
      constr:(refines_atomic_abort r msg)
  end.

Ltac refines_promotes_abort :=
  refines_fold build_refines_promotes_abort;
  repeat refines_seq_assoc.

Ltac build_refines_store_fence trm :=
  match trm with
    | (Sseq (Sstore false ?af ?addr ?args ?dst) (Sfence ?r)) =>
      constr:(refines_store_fence true r af addr args dst)
    | (Sseq (Sstore false ?af ?addr ?args ?dst)
       (Sseq (Sfence ?r) ?stmt)) =>
    let h1 := constr:(refines_store_fence true r af addr args dst) in
      constr:(refines_trans _ _ _ (refines_seq_assoc1 _ _ _)
               (refines_seq_left _ stmt _ h1))
  end.

Ltac refines_store_fence:=
  refines_fold build_refines_store_fence;
  repeat refines_seq_assoc.


Ltac build_refines_fence_load trm :=
  match trm with
    | (Sseq (Sfence false) (Sload ?af ?addr ?args ?dst)) =>
      constr:(refines_fence_load true af addr args dst)
    | (Sseq (Sfence false)
       (Sseq (Sload ?af ?addr ?args ?dst) ?stmt)) =>
    let h1 := constr:(refines_fence_load true af addr args dst) in
      constr:(refines_trans _ _ _ (refines_seq_assoc1 _ _ _)
               (refines_seq_left _ stmt _ h1))
  end.

Ltac refines_fence_load:=
  refines_fold build_refines_fence_load;
  repeat refines_seq_assoc.


Lemma refines_atomic_if_skip_right: forall f cond args stmt,
  no_atomic_in_statement stmt ->
  refines (Sifthenelse cond args (Satomic f stmt) (Sfence false))
      (Satomic f (Sifthenelse cond args stmt Sskip)).

Ltac refines_dead_code_strong :=
  refines_fold build_refines_dead_code.

Ltac build_refines_local trm :=
  match trm with
    | (Sseq (Satomic ?b ?s1) ?s2) =>
      constr:(refines_right_mover s1 b s2 (refl_equal _) (refl_equal _) (refl_equal _))
    | (Sseq ?s1 (Satomic ?b ?s2)) =>
      constr:(refines_left_mover_strong s1 b s2 (refl_equal _) (refl_equal _) (refl_equal _))
    | (Sifthenelse ?cond ?args (Satomic ?f ?stmt1) (Sfence false)) =>
      constr:(refines_atomic_if_skip_right f cond args stmt1 (refl_equal _))
    | (Sseq (Sstore Local ?addr ?args ?dst) (Satomic ?b ?s2)) =>
      constr:(refines_localstore addr args dst b s2)
    | (Sseq (Sload Local ?addr ?args ?dst) (Satomic ?b ?s2)) =>
      constr:(refines_localload addr args dst b s2)
    | Sseq ?s1 (Sseq (Satomic ?b ?s2) ?s3) =>
      let h1 := constr:(refines_seq_assoc1 s1 (Satomic b s2) s3) in
      let h2 := build_refines_local (Sseq s1 (Satomic b s2)) in
      let h3 := constr:(refines_seq_left _ s3 _ h2) in
        constr:(refines_trans _ _ _ h1 h3)
    | Sseq (Satomic ?b ?s1) (Sseq ?s2 ?s3) =>
      let h1 := constr:(refines_seq_assoc1 (Satomic b s2) s2 s3) in
      let h2 := build_refines_local (Sseq (Satomic b s1) s2) in
      let h3 := constr:(refines_seq_left _ s3 _ h2) in
        constr:(refines_trans _ _ _ h1 h3)
  end.


Ltac refines_local :=
  refines_fold build_refines_local;
  repeat refines_seq_assoc.

Ltac build_refines_branch_same_begin trm :=
  match trm with
    | Sbranch (Sseq ?s1 ?s2) (Sseq ?s1 ?s3) =>
      constr:(refines_branch_same_begin s1 s2 s3)
  end.

Ltac refines_branch_same_begin := refines_fold build_refines_branch_same_begin.

Ltac start_build_atomics :=
  eapply refines_trans; [eapply refines_seq;[eapply refines_refl|idtac]|idtac].

Ltac end_build_atomics :=
  apply refines_refl.

Ltac sweep_permissions :=
  refines_swap_freeperm; simpl; refines_remove_freeperm.

Open Scope positive_scope.



Lemma lock_refines: refines (lock_statement) (lock_high).

Lemma unlock_refines: refines (unlock_statement) (unlock_high).

Ltac simpl_regmap H :=
  unfold upd_regset in H;
  repeat (rewrite peq_false in H; [idtac|congruence]); try rewrite peq_true in H.
Ltac simpl_regmap_goal :=
  unfold upd_regset;
  repeat (rewrite peq_false; [idtac|congruence]); try rewrite peq_true.

Remark treiber_stack_equiv :
   refines_in_atomic
     (Move 5 := 4;;
      Assume 5 <> Int.zero;;
      Load 6 := 5 [blk_next];;
      Load 4 := 3 [Int.zero];;
      Assume 4 = 5;;
      Store 3 [Int.zero]:=6)%I
     (Load 5 := 3 [Int.zero];;
      Move 4 := 5;;
      Assume 5 <> Int.zero;;
      Load 6 := 5 [blk_next];;
      Store 3 [Int.zero]:=6)%I.

Lemma allocator_refines: forall bi slot header,
  refines (new_statement bi slot header) (new_statement_high bi slot header).

Lemma write_barrier_refines: forall bi fld, refines (update_stmt bi fld) (update_stmt_high bi fld).

Lemma refines_cooperate bi : refines (cooperate bi) (cooperate_high bi).

Lemma refines_spawn bi func : refines (spawn_statement bi func) (spawn_statement_high bi func).

Lemma refines_start : refines start_statement start_statement_high.

Lemma refines_end_thread : forall bi, refines (end_statement bi) (end_statement_high bi).

Lemma refines_prologue N : refines (prologue N) (prologue_high N).

Lemma refines_epilogue : refines epilogue epilogue_high.

Lemma refines_gc_startup: forall bi om p, refines (gc_startup bi om p) (gc_startup_high bi om p).

Lemma refines_wait_hs: forall bi fld val,
  refines (wait_hs bi fld val) (wait_hs_high bi fld val) .

Lemma refines_trace: forall bi, refines (trace bi MIRexample.om) (trace_high bi MIRexample.om).

Lemma refines_sweep: forall bi, refines (sweep bi MIRexample.om) (sweep_high bi MIRexample.om).

Ltac debug :=
  repeat
    (apply refines_repeat_congruence)
    || (apply while_repeat_congruence)
    || (apply refines_atomic)
    || (apply refines_if)
    || (apply refines_seq)
    || (apply refines_refl)
    || (apply refines_branch)
    || (apply refines_loop)
    || reflexivity.