Require Import Coqlib Utf8.
Require Import Maps.
Require Import Ast.
Require Import Integers.
Require Import Pointers.
Require Import Values.
Require Import Mem.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import Libtactics.
Require RTL.
Require Import Events.
Require Import Classical Relations.
Require Import INJECT.
Require Import Utils.
Require Import Permissions Emem TSOMemoryMachine MemoryMachine.

Definition node := RTL.node.

RTL-inject.

Inductive instruction: Type :=
| Inop (succ: node)
| Icond (cond:condition) (args:list reg) (if_so:node) (if_not:node)
| Iop (op:operation) (args:list reg) (dst:reg) (succ:node)
| Ithreadcreate (fp: reg) (arg: reg) (succ: node)
| Icall (sig:signature) (f:reg + ident) (args:list reg) (dst:reg) (succ:node)
| Ireturn (res:reg)
| Iinject (inj: injected_body) (args dst: list reg) (succ: node)
.

Definition code: Type := PTree.t instruction.

Record function: Type := mkfunction
{ fn_sig: signature
; fn_params: list reg
; fn_stacksize: int
; fn_code: code
; fn_entrypoint: node
}.

Definition fundef := Ast.fundef function.

Definition program := Ast.program fundef unit.

Definition funsig (fd: fundef) :=
  match fd with
  | Internal f => f.(fn_sig)
  | External ef => ef.(ef_sig)
  end.

Definition genv := Genv.t fundef.

Record stack_frame : Type := mksf
{ sf_res: reg (* return register *)
; sf_code: code (* function code *)
; sf_sp: option pointer (* poiter to local variables *)
; sf_pc: node (* destination program counter *)
; sf_reg: regset (* saved register file *)
}.

Definition stack : Type := list stack_frame.

Inductive intra_state : Type :=
| RIState (stk: stack) (c: code) (sp: option pointer) (pc: node) (rs: regset)
| RIInjectState (stk: stack) (c: code) (sp: option pointer)
                (next: node) (rs: regset) (dst: list reg) (is: INJECT.state)
| RICallState (stk: stack) (f: fundef) (args: list val)
| RIRetState (stk: stack) (res: val)
| RIBlockedState (stk: stack) (efsig: signature)
.

Section intra_step.

Variable ge: genv.

Definition find_function (ros: reg + ident) (rs: regset) : option fundef :=
  match ros with
    | inl r => Genv.find_funct ge (rs r)
    | inr symb => do b <- Genv.find_symbol ge symb;
                  Genv.find_funct_ptr ge b
  end.

Definition reg_upd : regset → list reg → list val → regset := fold_right2 upd.

Inductive rtli_step: intra_state -> thread_event -> intra_state -> Prop :=
| RTLI_nop stk c sp pc rs pc'
    (PC: c ! pc = Some (Inop pc'))
  : rtli_step (RIState stk c sp pc rs)
              TEtau
              (RIState stk c sp pc' rs)

| RTLI_cond_true stk c sp pc rs cond args if_so if_not
    (PC: c ! pc = Some (Icond cond args if_so if_not))
    (COND: eval_condition cond (map rs args) = Some true)
  : rtli_step (RIState stk c sp pc rs)
              TEtau
              (RIState stk c sp if_so rs)
| RTLI_cond_false stk c sp pc rs cond args if_so if_not
    (PC: c ! pc = Some (Icond cond args if_so if_not))
    (COND: eval_condition cond (map rs args) = Some false)
  : rtli_step (RIState stk c sp pc rs)
              TEtau
              (RIState stk c sp if_not rs)

| RTLI_op stk c sp pc rs op args res succ v
    (PC: c ! pc = Some (Iop op args res succ))
    (OP: eval_operation ge sp op (map rs args) = Some v)
  : rtli_step (RIState stk c sp pc rs)
              TEtau
              (RIState stk c sp succ (upd rs res v))

| RTLI_threadcreate stk c sp pc rs fp arg pc' pfp
    (PC: c ! pc = Some (Ithreadcreate fp arg pc'))
    (FP: rs fp = Vptr pfp)
  : rtli_step (RIState stk c sp pc rs)
              (TEstart pfp (rs arg))
              (RIState stk c sp pc' rs)

| RTLI_call stk c sp pc rs sig dst ros args pc' fd
    (PC: c ! pc = Some (Icall sig ros args dst pc'))
    (FUNC: find_function ros rs = Some fd)
    (SG: funsig fd = sig)
  : rtli_step (RIState stk c sp pc rs)
              TEtau
              (RICallState (mksf dst c sp pc' rs :: stk) fd (map rs args))

| RTLI_fun_internal_alloc stk f args sp
    (SP: f.(fn_stacksize) ≠ Int.zero)
  : rtli_step (RICallState stk (Ast.Internal f) args)
              (TEtso (TSOmem (MEalloc sp f.(fn_stacksize) MObjStack)))
              (RIState stk f.(fn_code) (Some sp) f.(fn_entrypoint) (reg_upd (fun _ => Vundef) f.(fn_params) args))
| RTLI_fun_internal_none stk f args
    (SP: f.(fn_stacksize) = Int.zero)
  : rtli_step (RICallState stk (Ast.Internal f) args)
              TEtau
              (RIState stk f.(fn_code) None f.(fn_entrypoint) (reg_upd (fun _ => Vundef) f.(fn_params) args))
| RTLI_fun_external stk f eargs
  : rtli_step (RICallState stk (Ast.External f) (List.map Vint eargs))
              (TEext (Ecall f.(Ast.ef_id) (map EVint eargs)))
              (RIBlockedState stk f.(Ast.ef_sig))

| RTLI_return_external stk sg res
    (SG: match sg.(sig_res) with Some t => t = Ast.Tint | None => True end)
  : rtli_step (RIBlockedState stk sg)
              (TEext (Ereturn Ast.Tint (EVint res)))
              (RIRetState stk (Vint res))

| RTLI_return_cont sf stk res
  : rtli_step (RIRetState (sf::stk) res)
              TEtau
              (RIState stk sf.(sf_code) sf.(sf_sp) sf.(sf_pc) (upd sf.(sf_reg) sf.(sf_res) res))
| RTLI_return_end res
  : rtli_step (RIRetState nil res)
              TEexit
              (RIRetState nil res)

| RTLI_ret_free stk c sp pc rs res vres
    (PC: c ! pc = Some (Ireturn res))
    (RES: rs res = vres)
  : rtli_step (RIState stk c (Some sp) pc rs)
              (TEtso (TSOmem (MEfree sp MObjStack)))
              (RIRetState stk vres)
| RTLI_ret_none stk c pc rs res vres
    (PC: c ! pc = Some (Ireturn res))
    (RES: rs res = vres)
  : rtli_step (RIState stk c None pc rs)
              TEtau
              (RIRetState stk vres)

| RTLI_inject_start_high stk c sp pc rs ij args dst pc'
    (PC: c ! pc = Some (Iinject ij args dst pc'))
  : rtli_step (RIState stk c sp pc rs)
              (TEbegin BeginHigh)
              (RIInjectState stk c sp pc' rs dst (init_high ij (map rs args)))
| RTLI_inject_start_low stk c sp pc rs ij args dst pc'
    (PC: c ! pc = Some (Iinject ij args dst pc'))
  : rtli_step (RIState stk c sp pc rs)
              (TEbegin BeginLow)
              (RIInjectState stk c sp pc' rs dst (init_low ij (map rs args)))
| RTLI_inject_step stk c sp pc rs dst is is' ev
    (INJECT: INJECT.step ge sp is ev is')
    (EV: ∀eev, ev ≠ TEend eev)
  : rtli_step (RIInjectState stk c sp pc rs dst is)
              ev
              (RIInjectState stk c sp pc rs dst is')
| RTLI_inject_end_return stk c sp pc rs dst is res
    (INJECT: INJECT.step ge sp is (TEend (ReturnEvent res)) ReturnState)
  : rtli_step (RIInjectState stk c sp pc rs dst is)
              (TEend (ReturnEvent res))
              (RIState stk c sp pc (reg_upd rs dst res))
| RTLI_inject_end_return_void stk c sp pc rs dst is
    (INJECT: INJECT.step ge sp is (TEend ReturnVoid) ReturnState)
  : rtli_step (RIInjectState stk c sp pc rs dst is)
              (TEend ReturnVoid)
              (RIState stk c sp pc rs)
| RTLI_inject_end_fail stk c sp pc rs dst is
    (INJECT: INJECT.step ge sp is (TEend FailEvent) ReturnState)
  : rtli_step (RIInjectState stk c sp pc rs dst is)
              (TEend FailEvent)
              (RIState stk c sp pc rs)
.

Definition rtl_inject_init (p : pointer) (vs : list val) : option intra_state :=
  match Genv.find_funct_ptr ge p with
   | Some (Internal f) =>
       if beq_nat (length vs) (length f.(fn_sig).(sig_args))
         then Some (RICallState nil (Internal f) (Val.conv_list vs f.(fn_sig).(sig_args)))
         else None
   | _ => None
  end.

Inductive intra_step t : (tsomem * intra_state)%type -> thread_event -> (tsomem * intra_state)%type -> Prop :=
| intra_step_not_mem: forall st st' m e
  (ST:rtli_step st e st')
  (IS_not_mem:forall e', e <> TEtso e'),
  intra_step t (m, st) e (m, st')
| intra_step_mem: forall m st st' m' e'
  (ST:rtli_step st (TEtso e') st')
  (ES:tso_step t m e' m'),
  intra_step t (m, st) (TEtso e') (m', st')
.

Inductive atomic_intra_step t : (mem * intra_state)%type -> thread_event -> (mem * intra_state)%type -> Prop :=
| atomic_intra_step_not_mem: forall st st' m e
  (ST:rtli_step st e st')
  (IS_not_mem:forall e', e <> TEtso e'),
  atomic_intra_step t (m, st) e (m, st')
| atomic_intra_step_mem: forall m st st' m' e'
  (ST:rtli_step st (TEtso (TSOmem e')) st')
  (AIS1:forall ap ib a v, e' = MEread ap ib a v -> ib = false)
  (AIS2:forall r p v a, e' = MErmw r p v a -> False)
  (ES:mem_step t m e' m'),
  atomic_intra_step t (m, st) (TEato e') (m', st').


Inductive atrace t : (mem * intra_state)%type -> list thread_event -> (mem * intra_state)%type -> Prop :=
| atrace_nil : forall s, atrace t s nil s
| atrace_cons : forall s0 m st e m' st' l
   (AT1:atomic_intra_step t (m, st) e (m', st'))
   (AT2:atrace t s0 l (m,st))
   (AT5:forall ev, e<>TEend ev),
   atrace t s0 (e::l) (m',st').

End intra_step.

Definition state : Type := (tsomem * PTree.t intra_state)%type.

Inductive astep ge : state -> thread_id * list thread_event -> state -> Prop :=
| astep_free: forall m st tid e m' st' s s'
   (AS3: st ! tid = Some s)
   (AS4: st' = st ! tid <- s')
   (AS1: intra_step ge tid (m, s) e (m', s'))
   (AS2: e<>TEtso TSObeginatomic)
   (AS5: ∀ fp v, e ≠ TEstart fp v)
   (AS6: e ≠ TEexit),
   astep ge (m, st) (tid,e::nil) (m', st')
| astep_unbuf tid m bi m' st
   (AS: tso_step tid m (TSOunbuf bi) m')
  : astep ge (m, st) (tid, TEtso (TSOunbuf bi)::nil) (m', st)
| astep_spawn: forall m st tid fp v m' st' s s' tid' init m''
   (AS3: st ! tid = Some s)
   (AS4: st' = st ! tid <- s')
   (AS1: intra_step ge tid (m, s) (TEstart fp v) (m', s'))
   (AS2: st ! tid' = None)
   (AS5: rtl_inject_init ge fp (v::nil) = Some init)
   (AS6: tso_step tid m' (TSOstart tid') m''),
   astep ge (m, st) (tid, TEstart fp v ::nil) (m'', st' ! tid' <- init)
| astep_spawn_fail: forall m st tid fp v m' st' s s'
   (AS3: st ! tid = Some s)
   (AS4: st' = st ! tid <- s')
   (AS1: intra_step ge tid (m, s) (TEstart fp v) (m', s'))
   (AS5: rtl_inject_init ge fp (v::nil) = None),
   astep ge (m, st) (tid, TEext Efail ::nil) (m', st')
| astep_exit: forall m st tid m' s s'
   (AS3: st ! tid = Some s)
   (AS1: intra_step ge tid (m, s) TEexit (m', s')),
   astep ge (m, st) (tid, TEexit ::nil) (m', PTree.remove tid st)
| astep_locked: forall m b st tid m' fence l st' s s' s'' s'''
   (AS3: st ! tid = Some s)
   (AS4: st' = st ! tid <- s''')
   (AS1: rtli_step ge s (TEtso TSObeginatomic) s')
   (AS6: b tid = nil)
   (AS2: atrace ge tid (m, s') l (m', s''))
   (AS5: rtli_step ge s'' (TEtso (TSOendatomic fence)) s'''),
   astep ge (TSOMEM m b, st) (tid,l) (TSOMEM m' b, st').

Inductive trace ge (s0:state) : list (thread_id * list thread_event) -> state -> Prop :=
| trace_nil : trace ge s0 nil s0
| trace_cons : forall tr s1 e s2
  (HT1: trace ge s0 tr s1)
  (HT2: astep ge s1 e s2),
  trace ge s0 (e::tr) s2.

Definition low_trace ge (s1: state) (tr: list (thread_id * list thread_event)) (s2:state) : Prop :=
  trace ge s1 tr s2 /\ forall tid, ~ (In (tid,TEbegin BeginHigh::nil) tr).

Definition high_trace ge (s1: state) (tr: list (thread_id * list thread_event)) (s2:state) : Prop :=
  trace ge s1 tr s2 /\ forall tid, ~ (In (tid,TEbegin BeginLow::nil) tr).

Fixpoint filter_fullevent_list (l:list thread_event) : list Events.event :=
  match l with
    | nil => nil
    | (TEext e)::q => e::(filter_fullevent_list q)
    | _::q => filter_fullevent_list q
  end.

Fixpoint filter_fullevent (l:list (thread_id * list thread_event)) : list Events.event :=
  match l with
    | nil => nil
    | (id,l)::q => (filter_fullevent_list l)++(filter_fullevent q)
  end.

Lemma filter_fullevent_app : forall l1 l2,
  filter_fullevent (l1++l2) = (filter_fullevent l1)++(filter_fullevent l2).

Definition inject_state (s:intra_state) : bool :=
  match s with
    | RIInjectState _ _ _ _ _ _ _ => true
    | _ => false
  end.

Definition backwardsim ge := forall st1 tr st2,
  low_trace ge st1 tr st2 ->
  (forall tid s, (snd st2)!tid = Some s -> inject_state s = false) ->
  exists tr',
    high_trace ge st1 tr' st2 /\ filter_fullevent tr' = filter_fullevent tr.

Lemma trace_app ge : forall tr' {x y z tr},
  trace ge x tr y →
  trace ge y tr' z →
  trace ge x (tr' ++ tr) z.