Module INJECT

Require Import Coqlib.
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 Import TSOmachine.
Require RTL MIR.

Require Import Utils Emem.

Inductive leak : Set :=
| LFree
| LAlloc
| LGrey
| LSave
| LHS
| LShadowPush | LShadowPop
| LSpawn
| LMark
.

Definition regset := reg -> val.
Definition upd_regset (rs:regset) r0 v0 :=
  fun r => if peq r r0 then v0 else rs r.
Notation "a ## b <- c" := (upd_regset a b c) (at level 1, b at next level).

Inductive request_perm := RPread | RPwrite.
Inductive annot_perm := Local | Global.
Inductive atomic_flag := Atomic | Interleaved.

Inductive statement : Type :=
  | Sskip
  | Leak (l: leak) (arg: reg) (out: reg)
  | Sop (op:operation) (args:list reg) (dst:reg)
  | Sload (ap:annot_perm) (addr:addressing) (args:list reg) (dst:reg)
  | Sstore (release:bool) (ap:annot_perm) (addr:addressing) (args:list reg) (dst:reg)
  | Satomicmem (release:bool) (op:atomic_statement) (args:list reg) (dst:reg)
  | Sfence (release:bool)
  | Sifthenelse (cond:condition) (args:list reg) (ifso:statement) (ifnot:statement)
  | Swhile (cond:condition) (args:list reg) (body:statement)
  | Srepeat (body:statement) (cond:condition) (args:list reg)
  | Sseq (stmt1:statement) (stmt2:statement)
  | Sreturn (args: list reg)
  | Sabort (af:atomic_flag) (release:bool) (msg:MIR.abort_msg)
  | Satomic (with_fence:bool) (body:statement)
  | Sassume (cond:condition) (args:list reg)
  | Sloop (body:statement)
  | Sbranch (body1 body2:statement)
  | Srelease
  | Srequestperm (rp:request_perm) (addr:addressing) (args:list reg)
  | Sfreeperm
.

Definition ok_op (op: operation) : bool :=
  match op with
    | Ointconst _
    | Omove
    | Olea _
    | Oneg
    | Oshrimm _
    | Oorimm _
    | Oxorimm _
    | Ocmp _
      => true
    | _ => false
  end.

Record injected_body : Type := Make_IC {
  ic_stmt_low : statement; (* the low level statement that will be compiled to RTL *)
  ic_stmt_high : statement; (* the high level statement that should refine the low level statement and exibit less interleaving with the other threads *)
  ic_params : list reg
}.

Inductive continuation : Type :=
  | Kstmt (s:statement) (k:continuation)
  | Kendatomic (fence: bool) (k:continuation)
  | Kend.

Fixpoint in_atomic (k: continuation) {struct k} : option (bool*continuation) :=
  match k with
    | Kstmt _ k' => in_atomic k'
    | Kendatomic fence k => Some (fence,k)
    | Kend => None
  end.

Inductive state : Type :=
  | NormalState:
      forall (rs: regset) (* external register state *)
             (stmt: statement) (* current statement *)
             (cont: continuation) (* continuation *)
      ,state
  | ReturnState: state
.

Definition release_flag := bool.
Definition read_in_buf_flag := bool.

Inductive perm_event : Type :=
  | PEcheck_store : annot_perm -> pointer -> perm_event
  | PEcheck_load : annot_perm -> pointer -> perm_event
  | PErequest : request_perm -> pointer -> perm_event
  | PErelease : perm_event
  | PEfreeperm : perm_event.

Inductive mem_event : Type :=
  | MEwrite : release_flag -> annot_perm -> pointer -> val -> mem_event
  | MEread : annot_perm -> read_in_buf_flag -> pointer -> val -> mem_event
  | MErmw : release_flag -> pointer -> val -> Events.rmw_instr -> mem_event
  | MEalloc : pointer -> int -> mobject_kind -> mem_event
  | MEfree : pointer -> mobject_kind -> mem_event
  | MEperm : perm_event -> mem_event.

Inductive atomic_statement_mem_event (r: release_flag) :
  atomic_statement -> list val -> val -> mem_event -> Prop:=
  | atomic_statement_mem_event_cas: forall p v o n
    (NUo : o <> Vundef)
    (NUn : n <> Vundef)
    (HTo : Val.has_type o Tint)
    (HTn : wf_val n),
    atomic_statement_mem_event r AScas (Vptr p :: n :: o :: nil) v
                               (MErmw r p v (Events.rmw_CAS o n))
.

Definition init_low (ic:injected_body) (vl:list val) : state :=
  NormalState (fold_left2 upd (fun _ => Vundef) ic.(ic_params) vl) ic.(ic_stmt_low) Kend.

Definition init_high (ic:injected_body) (vl:list val) : state :=
  NormalState (fold_left2 upd (fun _ => Vundef) ic.(ic_params) vl) ic.(ic_stmt_high) Kend.


Inductive begin_event : Type := BeginLow | BeginHigh.

Inductive end_event : Type :=
  | ReturnVoid
  | ReturnEvent (vres: list val) (* returned values *)
  | FailEvent (* when then the injected code aborts *).

Inductive buf_item : Type :=
  | WBufItem : pointer -> val -> buf_item
  | ABufItem : pointer -> int -> mobject_kind -> buf_item
  | FBufItem : pointer -> mobject_kind -> buf_item
.

Inductive tso_event : Type :=
| TSOmem (ev:mem_event)
| TSOunbuf (e:mem_event)
| TSOfence
| TSObeginatomic
| TSOendatomic (fence: bool)
| TSOstart (newtid: positive)
.

Inductive thread_event : Type :=
| TEext (ev:Events.event)
| TEtso (ev:tso_event)
| TEato (ev:mem_event)
| TEtau
| TEstart (fp:pointer) (v:val)
| TEexit
| TEbegin (be:begin_event) | TEend (e:end_event)
.

Fixpoint no_atomic_in_statement (stmt:statement) : Prop :=
  match stmt with
    | Sskip
    | Leak _ _ _
    | Sop _ _ _
    | Sload _ _ _ _
    | Sstore _ _ _ _ _
    | Satomicmem _ _ _ _
    | Sfence _
    | Sreturn _
    | Sabort _ _ _
    | Srequestperm _ _ _
    | Sfreeperm
    | Srelease
    | 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.

Section step.

Context {fundef: Type}.
Variable ge: Genv.t fundef.
Variable sp: option pointer.

Inductive step: state -> thread_event -> state -> Prop :=
  | exec_skip: forall rs stmt k,
      step (NormalState rs Sskip (Kstmt stmt k))
        TEtau (NormalState rs stmt k)

  | exec_skip_seq: forall rs fence k,
      step (NormalState rs Sskip (Kendatomic fence k))
        (TEtso (TSOendatomic fence))
        (NormalState rs Sskip k)

  | exec_op: forall rs k v op args res rs',
      eval_operation ge sp op (map rs args) = Some v ->
      rs' = (rs##res <- v) ->
      step (NormalState rs (Sop op args res) k)
        TEtau (NormalState rs' Sskip k)

  | exec_load:
      forall rs k a v addr args res rs' ap inbuf
      (HTv: Val.has_type v Tint),
      rs' = (rs##res <- v) ->
      eval_addressing ge sp addr (map rs args) = Some (Vptr a) ->
      step (NormalState rs (Sload ap addr args res) k)
        (TEtso (TSOmem (MEread ap inbuf a v)))
        (NormalState rs' Sskip k)

  | exec_store:
      forall rs k a addr args src ap released
      (HTv: wf_val (rs src)),
      eval_addressing ge sp addr (map rs args) = Some (Vptr a) ->
      step (NormalState rs (Sstore released ap addr args src) k)
        (TEtso (TSOmem (MEwrite released ap a (rs src))))
        (NormalState rs Sskip k)

  | exec_request:
      forall rs k a addr args rp,
      eval_addressing ge sp addr (map rs args) = Some (Vptr a) ->
      step (NormalState rs (Srequestperm rp addr args) k)
        (TEtso (TSOmem (MEperm (PErequest rp a))))
        (NormalState rs Sskip k)

  | exec_atomic:
      forall op args res v rs rs' lab k released
      (ASME : atomic_statement_mem_event released op (map rs args) v lab)
      (Ers' : rs' = (rs##res <- v))
      (HTv : Val.has_type v Tint),
      step
        (NormalState rs (Satomicmem released op args res) k)
        (TEtso (TSOmem lab))
        (NormalState rs' Sskip k)

  | exec_fence rs k
      : step
      (NormalState rs (Sfence false) k)
      (TEtso TSOfence)
      (NormalState rs Sskip k)

  | exec_fence_release rs k
      : step
      (NormalState rs (Sfence true) k)
      (TEtso TSOfence)
      (NormalState rs Srelease k)

  | exec_leak: forall rs l arg out k,
      step (NormalState rs (Leak l arg out) k)
        TEtau (NormalState rs Sskip k)

  | exec_if_true rs cond args ifso ifnot k
      : eval_condition cond (map rs args) = Some true ->
      step
      (NormalState rs (Sifthenelse cond args ifso ifnot) k)
      TEtau
      (NormalState rs ifso k)

  | exec_if_false rs cond args ifso ifnot k
      : eval_condition cond (map rs args) = Some false ->
      step
      (NormalState rs (Sifthenelse cond args ifso ifnot) k)
      TEtau
      (NormalState rs ifnot k)

  | exec_while_true rs cond args body k
      : eval_condition cond (map rs args) = Some true ->
      step
      (NormalState rs (Swhile cond args body) k)
      TEtau
      (NormalState rs body (Kstmt (Swhile cond args body) k))

  | exec_while_false rs cond args body k
      : eval_condition cond (map rs args) = Some false ->
      step
      (NormalState rs (Swhile cond args body) k)
      TEtau
      (NormalState rs Sskip k)

  | exec_repeat rs cond args body k
      : step
      (NormalState rs (Srepeat body cond args) k)
      TEtau
      (NormalState rs (Sseq body (Swhile (Op.negate_condition cond) args body)) k)

  | exec_seq rs s1 s2 k
      : step
      (NormalState rs (Sseq s1 s2) k)
      TEtau
      (NormalState rs s1 (Kstmt s2 k))

  | exec_return rs res k
      :
      in_atomic k = None ->
      step
      (NormalState rs (Sreturn res) k)
      (TEend (ReturnEvent (map rs res)))
      ReturnState

  | exec_return_endatomic rs fence res k k'
      :
      in_atomic k = Some (fence,k') ->
      step
      (NormalState rs (Sreturn res) k)
      (TEtso (TSOendatomic fence))
      (NormalState rs (Sreturn res) k')

  | exec_abort rs k e r
      (ATM: in_atomic k = None)
      : step
      (NormalState rs (Sabort Interleaved r e) k)
      (TEend FailEvent)
      ReturnState

  | exec_end rs
      : step
      (NormalState rs Sskip Kend)
      (TEend ReturnVoid)
      ReturnState

  | exec_abort_endatomic rs k r e fence k'
      :
      in_atomic k = Some (fence,k') ->
      step
      (NormalState rs (Sabort Atomic r e) k)
      (TEtso (TSOendatomic fence))
      (NormalState rs (Sabort Interleaved r e) k')

  | exec_Satomic rs s k with_fence
      :
      no_atomic_in_statement s ->
      step
      (NormalState rs (Satomic with_fence s) k)
      (TEtso TSObeginatomic)
      (NormalState rs s (Kendatomic with_fence k))

  | exec_assert_true rs cond args k
      : eval_condition cond (map rs args) = Some true ->
      step
      (NormalState rs (Sassume cond args) k)
      TEtau
      (NormalState rs Sskip k)

  | exec_branch_left rs s1 s2 k
      : step
      (NormalState rs (Sbranch s1 s2) k)
      TEtau
      (NormalState rs s1 k)

  | exec_branch_right rs s1 s2 k
      : step
      (NormalState rs (Sbranch s1 s2) k)
      TEtau
      (NormalState rs s2 k)

  | exec_loop_end rs s k
      : step
      (NormalState rs (Sloop s) k)
      TEtau
      (NormalState rs Sskip k)

  | exec_loop_again rs s k
      : step
      (NormalState rs (Sloop s) k)
      TEtau
      (NormalState rs s (Kstmt (Sloop s) k))

  | exec_release rs k
      : step
      (NormalState rs Srelease k)
      (TEtso (TSOmem (MEperm PErelease)))
      (NormalState rs Sskip k)
  | exec_freeperm rs k
      : step
      (NormalState rs Sfreeperm k)
      (TEtso (TSOmem (MEperm PEfreeperm)))
      (NormalState rs Sskip k)
.

End step.