Module AllRefinesRulesAux

Require Import
  Utf8 Coqlib Ast Maps Globalenvs
  Utils INJECT RTLinject
  RefinesDefs
.

Fixpoint no_atomic_in_statement (stmt:statement) : bool :=
  match stmt with
    | Sskip
    | Leak _ _ _
    | Sop _ _ _
    | Sfreeperm
    | Sload _ _ _ _
    | Sstore _ _ _ _ _
    | Srequestperm _ _ _
    | Satomicmem _ _ _ _
    | Sfence _
    | Srelease
    | Sreturn _
    | Sabort _ _ _
    | Sassume _ _ => true
    | Sseq stmt1 stmt2
    | Sbranch stmt1 stmt2
    | Sifthenelse _ _ stmt1 stmt2 =>
      no_atomic_in_statement stmt1 && no_atomic_in_statement stmt2
    | Swhile _ _ body
    | Srepeat body _ _
    | Sloop body => no_atomic_in_statement body
    | Satomic _ _ => false
  end.

Fixpoint in_stmt (f:statement->bool) (stmt:statement) : bool :=
  match stmt with
    | Sseq stmt1 stmt2
    | Sbranch stmt1 stmt2
    | Sifthenelse _ _ stmt1 stmt2 => (in_stmt f stmt1) || (in_stmt f stmt2)
    | Swhile _ _ body
    | Srepeat body _ _
    | Sloop body
    | Satomic _ body => in_stmt f body
    | s => f s
  end
.

Definition abrupt_fun (stmt:statement) : bool :=
  match stmt with
    | Sreturn _
    | Sabort _ _ _ => true
    | _ => false
  end.

Definition abrupt (stmt:statement) : bool :=
  in_stmt abrupt_fun stmt.

Fixpoint defs (stmt:statement) : Rset.t :=
  match stmt with
    | Sfence _
    | Sreturn _
    | Sabort _ _ _
    | Sfreeperm
    | Sassume _ _
    | Leak _ _ _
    | Srelease
    | Srequestperm _ _ _
    | Sskip => Rset.empty
    | Sop _ _ dst
    | Sload _ _ _ dst
    | Sstore _ _ _ _ dst
    | Satomicmem _ _ _ dst => Rset.add dst Rset.empty
    | Sseq stmt1 stmt2
    | Sbranch stmt1 stmt2
    | Sifthenelse _ _ stmt1 stmt2 => Rset.union (defs stmt1) (defs stmt2)
    | Swhile _ _ body
    | Srepeat body _ _
    | Satomic _ body
    | Sloop body => defs body
  end
.

Fixpoint store_fun (stmt:statement) : bool :=
  match stmt with
    | Sstore _ _ _ _ _
    | Satomicmem _ _ _ _
    | Srequestperm _ _ _ => true
    | Sabort _ r _
    | Sfence r => r
    | Srelease => true
    | Sseq stmt1 stmt2
    | Sbranch stmt1 stmt2
    | Sifthenelse _ _ stmt1 stmt2 => (store_fun stmt1) || (store_fun stmt2)
    | Swhile _ _ body
    | Srepeat body _ _
    | Sloop body
    | Satomic _ body => store_fun body
    | _ => false
  end.

Definition store (stmt:statement) : bool :=
  store_fun stmt.

Fixpoint dead_in (stmt:statement) (dead_out:Rset.t) : Rset.t :=
  match stmt with
    | Sfence _
    | Sabort _ _ _
    | Sskip
    | Srelease
    | Sfreeperm
    | Leak _ _ _ => dead_out
    | Sreturn arg => Rset.remove_list arg dead_out
    | Srequestperm _ _ args
    | Sassume _ args => Rset.remove_list args dead_out
    | Sload _ _ args dst
    | Satomicmem _ _ args dst
    | Sop _ args dst => Rset.remove_list args (Rset.add dst dead_out)
    | Sstore _ _ _ args dst => Rset.remove_list (dst::args) dead_out
    | Sseq stmt1 stmt2 => dead_in stmt1 (dead_in stmt2 dead_out)
    | Sbranch stmt1 stmt2 => Rset.inter (dead_in stmt1 dead_out) (dead_in stmt2 dead_out)
    | Sifthenelse _ args stmt1 stmt2 =>
      Rset.remove_list args (Rset.inter (dead_in stmt1 dead_out) (dead_in stmt2 dead_out))
    | Swhile _ _ _
    | Srepeat _ _ _
    | Sloop _ => Rset.empty
    | Satomic _ body => dead_in body dead_out
  end
.

Fixpoint local_before_abort (s:statement) : bool :=
  match s with
    | Sop _ _ _
    | Sskip
    | Leak _ _ _
    | Sassume _ _ => true
    | Sload _ _ _ _ => true
    | Sifthenelse _ _ s1 s2
    | Sbranch s1 s2
    | Sseq s1 s2 => local_before_abort s1 && local_before_abort s2
    | Sfence r => negb r
    | Swhile _ _ s
    | Srepeat s _ _
    | Sloop s => local_before_abort s
    | Satomic _ s => local_before_abort s
    | _ => false
  end.

Fixpoint left_mover (s:statement) : bool :=
  match s with
    | Sop _ _ _
    | Sskip
    | Leak _ _ _
    | Sassume _ _ => true
    | Sseq stmt1 stmt2
    | Sifthenelse _ _ stmt1 stmt2 => left_mover stmt1 && left_mover stmt2
    | Sbranch stmt1 stmt2 => left_mover stmt1 && left_mover stmt2
    | Sloop stmt
    | Swhile _ _ stmt
    | Srepeat stmt _ _ => left_mover stmt
    | _ => false
  end.

Fixpoint left_mover_strong (s:statement) : bool :=
  match s with
    | Sop _ _ _
    | Sseq (Sfence _) (Sabort Interleaved _ _)
    | Sskip
    | Leak _ _ _
    | Sassume _ _
    | Sload Local _ _ _
    | Sstore false Local _ _ _ => true
    | Sseq stmt1 stmt2
    | Sifthenelse _ _ stmt1 stmt2 => left_mover_strong stmt1 && left_mover_strong stmt2
    | Srepeat stmt _ _
    | Swhile _ _ stmt => left_mover_strong stmt
    | _ => false
  end.

Fixpoint left_move_conv (s:statement) : statement :=
  match s with
    | Sabort _ r msg => Sabort Atomic r msg
    | Sseq (Sfence r1) (Sabort Interleaved r2 msg) =>
      if r1 then Sseq Srelease (Sabort Atomic r2 msg) else Sabort Atomic r2 msg
    | Sfence _
    | Sskip
    | Sfreeperm
    | Leak _ _ _
    | Sreturn _
    | Sop _ _ _
    | Sassume _ _
    | Sload _ _ _ _
    | Sstore _ _ _ _ _
    | Srequestperm _ _ _
    | Srelease
    | Satomicmem _ _ _ _ => s
    | Sbranch stmt1 stmt2 =>
      Sbranch (left_move_conv stmt1) (left_move_conv stmt2)
    | Sifthenelse c a stmt1 stmt2 =>
      Sifthenelse c a (left_move_conv stmt1) (left_move_conv stmt2)
    | Sseq stmt1 stmt2 => Sseq (left_move_conv stmt1) (left_move_conv stmt2)
    | Swhile c a body => Swhile c a (left_move_conv body)
    | Sloop body => Sloop (left_move_conv body)
    | Srepeat body c a => Srepeat (left_move_conv body) c a
    | Satomic f body => Satomic f (left_move_conv body)
  end
.

Fixpoint right_mover (s:statement) : bool :=
  match s with
    | Sop _ _ _
    | Sskip
    | Leak _ _ _
    | Sreturn _
    | Sassume _ _ => true
    | Sbranch stmt1 stmt2
    | Sseq stmt1 stmt2
    | Sifthenelse _ _ stmt1 stmt2 => right_mover stmt1 && right_mover stmt2
    | Sloop stmt
    | Swhile _ _ stmt
    | Srepeat stmt _ _ => right_mover stmt
    | _ => false
  end.

Fixpoint no_perm_update (stmt:statement) : bool :=
  match stmt with
    | Sfence r => negb r
    | Sskip
    | Sfreeperm
    | Leak _ _ _
    | Sreturn _
    | Sop _ _ _
    | Sload _ _ _ _
    | Sassume _ _ => true
    | Srelease => false
    | Sabort _ b _
    | Sstore b _ _ _ _
    | Satomicmem b _ _ _ => negb b
    | Srequestperm _ _ _ => false
    | Sbranch stmt1 stmt2
    | Sifthenelse _ _ stmt1 stmt2
    | Sseq stmt1 stmt2 => no_perm_update stmt1 && no_perm_update stmt2
    | Swhile _ _ body
    | Srepeat body _ _
    | Satomic _ body
    | Sloop body => no_perm_update body
  end
.

Fixpoint if_abrupt_release (stmt:statement) : bool :=
  match stmt with
    | Sreturn _ => false
    | Sfence _
    | Sskip
    | Sfreeperm
    | Leak _ _ _
    | Sop _ _ _
    | Sassume _ _
    | Sload _ _ _ _
    | Sstore _ _ _ _ _
    | Satomicmem _ _ _ _
    | Srelease
    | Srequestperm _ _ _ => true
    | Sseq Srelease (Sabort _ _ _) => true
    | Sseq (Sfence true) (Sabort _ _ _) => true
    | Sseq Srelease (Sreturn _) => true
    | Sbranch stmt1 stmt2
    | Sseq stmt1 stmt2
    | Sifthenelse _ _ stmt1 stmt2 => if_abrupt_release stmt1 && if_abrupt_release stmt2
    | Swhile _ _ body
    | Sloop body
    | Srepeat body _ _
    | Satomic _ body => if_abrupt_release body
    | Sabort _ _ _ => false
  end
.

Fixpoint release_point (stmt:statement) : bool :=
  match stmt with
    | Sfence b => b
    | Sskip
    | Sfreeperm
    | Leak _ _ _
    | Sreturn _
    | Sop _ _ _
    | Sload _ _ _ _
    | Sabort _ _ _
    | Sassume _ _ => false
    | Srelease => true
    | Sstore b _ _ _ _
    | Satomicmem b _ _ _ => b
    | Srequestperm _ _ _ => false
    | Sbranch stmt1 stmt2
    | Sifthenelse _ _ stmt1 stmt2 => release_point stmt1 && release_point stmt2
    | Sseq stmt1 stmt2 =>
       (if_abrupt_release stmt1 && release_point stmt2) || (release_point stmt1 && no_perm_update stmt2)
    | Swhile _ _ _
    | Sloop _
    | Srepeat _ _ _ => false
    | Satomic _ body => release_point body
  end
.

Fixpoint remove_perm (stmt:statement) : statement :=
  match stmt with
    | Sfence _ => Sfence false
    | Sskip
    | Sfreeperm
    | Leak _ _ _
    | Sreturn _
    | Sop _ _ _
    | Sassume _ _ => stmt
    | Srelease => Sskip
    | Sabort af _ msg => Sabort af false msg
    | Sload _ addr args res => Sload Global addr args res
    | Sstore released _ addr args res => Sstore false Global addr args res
    | Satomicmem released op args res => Satomicmem false op args res
    | Srequestperm _ _ _ => Sskip
    | Sbranch stmt1 stmt2 => Sbranch (remove_perm stmt1) (remove_perm stmt2)
    | Sifthenelse c a stmt1 stmt2 => Sifthenelse c a (remove_perm stmt1) (remove_perm stmt2)
    | Sseq stmt1 stmt2 => Sseq (remove_perm stmt1) (remove_perm stmt2)
    | Swhile c a body => Swhile c a (remove_perm body)
    | Sloop body => Sloop (remove_perm body)
    | Srepeat body c a => Srepeat (remove_perm body) c a
    | Satomic f body => Satomic f (remove_perm body)
  end
.

Definition refines_in_atomic (stmt1 stmt2:statement) : Prop :=
  forall ge sp tid st st',
    Bigstep.bigstep ge sp st tid stmt1 Atomic nil st' ->
    Bigstep.bigstep ge sp st tid stmt2 Atomic nil st'.

Section S.
  Variable refines : statement → statement → Prop.

  Definition wf_c (c: code) : Prop :=
    forall pc body args dst succ,
      c!pc = Some (Iinject body args dst succ) ->
      refines body.(ic_stmt_low) body.(ic_stmt_high).

  Definition wf_stack stack :=
    forall sf, In sf stack -> wf_c sf.(sf_code).

  Inductive wf_intra_state : intra_state → Prop :=
  | WF_state stk c sp pc rs
             (WFSTK: wf_stack stk)
             (WFC: wf_c c)
    : wf_intra_state (RIState stk c sp pc rs)
  | WF_injectstate stk c sp next rs dst is
             (WFSTK: wf_stack stk)
             (WFC: wf_c c)
    : wf_intra_state (RIInjectState stk c sp next rs dst is)
  | WF_callstate stk f args
             (WFSTK: wf_stack stk)
             (WFC: ∀ f', f = Internal f' → wf_c f'.(fn_code))
    : wf_intra_state (RICallState stk f args)
  | WF_returnstate stk res (WFSTK: wf_stack stk)
    : wf_intra_state (RIRetState stk res)
  | WF_blockedstate stk efsig (WFSTK: wf_stack stk)
    : wf_intra_state (RIBlockedState stk efsig)
  .

  Definition wf_istate : RTLinject.state → Prop :=
    fun s => let (m,st) := s in
    ∀ tid si,
      st!tid = Some si → wf_intra_state si.

  Definition ge_correct_wrt_refines (ge:genv) : Prop :=
  forall b f,
    Genv.find_funct_ptr ge b = Some (Internal f) ->
    forall pc inj args dst s,
      (fn_code f)!pc = Some (Iinject inj args dst s) ->
      refines inj.(ic_stmt_low) inj.(ic_stmt_high).

End S.