Module AbMemSignatureCsharpminor

Require Import Utf8 Coqlib Util.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Globalenvs.
Require Import Csharpminor.
Require Import Memory.
Require Import Events.
Require Import AdomLib.
Require Import TypesDomain.
Require Import AlarmMon.

Section GE.

Variable ge : genv.

Unset Elimination Schemes.
Class mem_dom (t iter_t:Type) := {
  leb_mem :> leb_op t;
  join_mem :> join_op t (t+⊥);
  widen_mem :> widen_op iter_t (t+⊥);
  assign: ident → expr → t → alarm_mon (t+⊥);
  assign_any: ident → AbTy.t → t → alarm_mon (t+⊥);
  store: memory_chunk → expr → expr → t → alarm_mon (t+⊥);
  assume: expr → t → alarm_mon (t+⊥ * t+⊥);
  noerror: expr → t → alarm_mon unit;
  ab_vload: option ident → option (ident * int) → memory_chunk → list expr → t → alarm_mon (t+⊥);
  ab_vstore: option ident → option (ident * int) → memory_chunk → list expr → t → alarm_mon (t+⊥);
  deref_fun: expr → t → alarm_mon (list (ident * fundef));
  push_frame: function →
list expr →
              t → alarm_mon (t+⊥);
  pop_frame: option (expr) → option(ident) →
             t → alarm_mon (t+⊥);
  ab_malloc: expr → option ident → t → alarm_mon (t+⊥);
  ab_free: expr → t → alarm_mon (t+⊥);
  ab_memcpy: Z → Z → expr → expr → t → alarm_mon (t+⊥);
  init_mem: list (ident * globdef fundef unit) → alarm_mon (t+⊥)
}.

Definition concrete_state := (list (temp_env * env) * mem)%type.

Inductive ExistsCState {T:Type} (E : ℘ concrete_state) Trans (cs:option T) : Prop :=
  ExistsCStateC :
    ∀ t e s m, E ((t, e) :: s, m) → Trans t e s m cs → ExistsCState E Trans cs.

Definition Assign (x: ident) (q: expr) (E: ℘ concrete_state) : ℘ (option concrete_state) :=
  ExistsCState E (fun t e s m cs =>
    ∀ v, eval_expr ge e t m q v →
         cs = Some ((PTree.set x v t, e) :: s, m)).

Definition AssignAny (x: ident) (ty: AbTy.t) (E: ℘ concrete_state) : ℘ (option concrete_state) :=
  ExistsCState E (fun t e s m cs =>
    ∃ v, v ∈ γ(ty) ∧ cs = Some ((PTree.set x v t, e) :: s, m)).

Definition Store (κ: memory_chunk) (dst src: expr) (E: ℘ concrete_state) : ℘ (option concrete_state) :=
  ExistsCState E (fun t e s m cs =>
    ∀ v a m',
      eval_expr ge e t m src v →
      eval_expr ge e t m dst a →
      Mem.storev κ m a v = Some m' →
      cs = Some ((t, e) :: s, m')).

Definition Assume (q: expr) (E: ℘ concrete_state) : ℘ (option (bool * concrete_state)) :=
  ExistsCState E (fun t e s m cs =>
    ∀ v b,
      Val.bool_of_val v b →
      eval_expr ge e t m q v →
      cs = Some (b, ((t, e) :: s, m))).

Local Instance boolean_partitionning t (_: gamma_op t concrete_state) :
  gamma_op (t * t) (bool * concrete_state) :=
  fun x y =>
  if fst y
  then γ (fst x) (snd y)
  else γ (snd x) (snd y).

Lemma boolean_partition t (_: gamma_op t concrete_state) (f: bool → t) :
  ∀ b cs,
    cs ∈ γ (f b) →
    Some (b, cs) ∈ γ ((f true, f false), nil).

Definition DerefFun (q: expr) (E: ℘ concrete_state) : ℘ (option (ident * fundef)) :=
  ExistsCState E (fun t e s m fid =>
    ∀ b fi fd, eval_expr ge e t m q (Vptr b Int.zero) →
               Genv.find_funct_ptr ge b = Some fd →
               Genv.find_symbol ge fi = Some b →
               fid = Some (fi, fd)).

Definition PopFrame (ret: option expr) (rettemp: option (ident)) (E: ℘ concrete_state) : ℘ (option concrete_state) :=
  ExistsCState E (fun t e s m cs =>
    ∀ m', Mem.free_list m (blocks_of_env e) = Some m' ->
    ∀ v, match ret with None => v = Vundef | Some q => eval_expr ge e t m q v end ->
         match s with
         | nil =>
           ∀ r, v = Vint r → cs = Some (s, m')
         | (t', e') :: s' =>
           cs = Some ((Cminor.set_optvar rettemp v t', e') :: s', m')
         end).

Definition PushFrame (f:function) (args:list expr)
           (E: ℘ concrete_state) : ℘ (option concrete_state) :=
  fun cs =>
    ∃ s m, E (s, m) ∧
     list_norepet (List.map fst f.(fn_vars)) ∧
     (∀ vargs,
        match s with
          | nil => vargs = nil
          | (t, e) :: _ => eval_exprlist ge e t m args vargs
        end →
      ∀ m1 e1, alloc_variables empty_env m (f.(fn_vars)) e1 m1 →
      ∀ t1, bind_parameters f.(fn_params) vargs (create_undef_temps f.(fn_temps)) = Some t1 →
      cs = Some ((t1, e1)::s, m1)).

Definition Noerror (q:expr) (E: ℘ concrete_state) : ℘ (option unit) :=
  ExistsCState E (fun t e s m u => ∀ v, eval_expr ge e t m q v → v <> Vundef → u = Some tt).

Definition VLoad (rettemp: option ident) (g_ofs: option (ident * int)) (κ: memory_chunk) (args: list expr) (E: ℘ concrete_state) : ℘ (option concrete_state) :=
  ExistsCState E (λ t e s m cs,
    match κ with Mint64 | Mfloat32 | Mfloat64 | Mint32 => True | _ => False end →
    ∀ tr vres g b ofs,
    match g_ofs, args with
    | None, arg :: nil => Vptr b ofs ∈ eval_expr ge e t m arg
    | Some (g', ofs'), nil => g' = g ∧ ofs' = ofs
    | _, _ => False
    end →
   Genv.find_symbol ge g = Some b →
   volatile_load ge κ m b ofs tr vres →
   if Senv.block_is_volatile ge b
     then ∃ v, v ≠ Vundef ∧ Val.has_type v (type_of_chunk κ) ∧ cs = Some ((Cminor.set_optvar rettemp v t, e) :: s, m)
     else cs = Some ((Cminor.set_optvar rettemp vres t, e) :: s, m)
  ).

Definition VStore (rettemp: option ident) (g_ofs: option (ident * int)) (κ: memory_chunk) (args: list expr) (E: ℘ concrete_state) : ℘ (option concrete_state) :=
  ExistsCState E (λ t e s m cs,
    ∀ tr g b ofs arg v,
    match g_ofs, args with
    | None, addr :: arg' :: nil => arg' = arg ∧ Vptr b ofs ∈ eval_expr ge e t m addr
    | Some (g', ofs'), arg' :: nil => g' = g ∧ ofs' = ofs ∧ arg' = arg
    | _, _ => False
    end →
   Genv.find_symbol ge g = Some b →
   v ∈ eval_expr ge e t m arg →
   volatile_store ge κ m b ofs v tr m ->
   if Senv.block_is_volatile ge b
   then cs = Some ((Cminor.set_optvar rettemp Vundef t, e) :: s, m)
   else ∀ m', Mem.store κ m b (Int.unsigned ofs) v = Some m' →
              cs = Some ((Cminor.set_optvar rettemp Vundef t, e) :: s, m')
  ).

Definition Malloc (sz_exp:expr) (rettemp:option ident) (E: ℘ concrete_state) : ℘ (option concrete_state) :=
  ExistsCState E (fun t e s m cs =>
    ∀ sz m' vres, eval_expr ge e t m sz_exp sz →
                   extcall_malloc_sem ge (sz::nil) m E0 vres m' →
                   cs = Some ((Cminor.set_optvar rettemp vres t, e) :: s, m')).

Definition Free (ptr_exp:expr) (E: ℘ concrete_state) : ℘ (option concrete_state) :=
  ExistsCState E (fun t e s m cs =>
    ∀ ptr m', eval_expr ge e t m ptr_exp ptr →
              extcall_free_sem ge (ptr::nil) m E0 Vundef m' →
              cs = Some ((t, e) :: s, m')).

Definition Memcpy (sz al:Z) (dst_exp src_exp:expr) (E: ℘ concrete_state) : ℘ (option concrete_state) :=
  ExistsCState E (fun t e s m cs =>
    ∀ dst src m',
      eval_expr ge e t m dst_exp dst →
      eval_expr ge e t m src_exp src →
      extcall_memcpy_sem sz al ge (dst::src::nil) m E0 Vundef m' →
      cs = Some ((t, e) :: s, m')).

Definition Init_Mem (defs:list (ident * globdef fundef unit)) : ℘ (option concrete_state) :=
  fun cs =>
    ∃ prog : program,
      ge = Genv.globalenv prog
    ∧ defs = prog.(prog_defs)
    ∧ ∀ m, Genv.alloc_globals ge Mem.empty defs = Some m →
           cs = Some (nil, m).

Local Instance ListIncl : gamma_op (list (ident * fundef)) (ident * fundef) :=
  λ l x, In x l.

Local Instance UnitGamma : gamma_op unit unit := eq.

Class mem_dom_spec {t iter_t: Type}
       (DOM: mem_dom t iter_t)
       (mem_gamma: gamma_op t concrete_state)
       (mem_gamma_iter: gamma_op iter_t concrete_state)
  : Prop := {
  leb_mem_correct:> leb_op_correct t concrete_state;
  join_mem_correct:> join_op_correct t (t+⊥) concrete_state;
  widen_mem_correct:> widen_op_correct iter_t (t+⊥) concrete_state;
  assign_sound: ∀ x e ab, Assign x e (γ ab) ⊆ γ (assign x e ab);
  assign_any_sound: ∀ x ty ab, AssignAny x ty (γ ab) ⊆ γ (assign_any x ty ab);
  store_sound: ∀ κ dst src ab, Store κ dst src (γ ab) ⊆ γ (store κ dst src ab);
  assume_sound: ∀ e ab, Assume e (γ ab) ⊆ γ(assume e ab);
  noerror_sound: ∀ e ab, Noerror e (γ ab) ⊆ γ (noerror e ab);
  ab_vload_sound: ∀ rettemp gofs κ args ab, VLoad rettemp gofs κ args (γ ab) ⊆ γ (ab_vload rettemp gofs κ args ab);
  ab_vstore_sound: ∀ rettemp gofs κ args ab, VStore rettemp gofs κ args (γ ab) ⊆ γ (ab_vstore rettemp gofs κ args ab);
  deref_fun_sound: ∀ e ab, DerefFun e (γ ab) ⊆ γ (deref_fun e ab);
  pop_frame_sound: ∀ ret rettemp ab, PopFrame ret rettemp (γ ab) ⊆ γ (pop_frame ret rettemp ab);
  push_frame_sound: ∀ f args ab, PushFrame f args (γ ab) ⊆ γ (push_frame f args ab);
  malloc_sound: ∀ sz rettemp ab, Malloc sz rettemp (γ ab) ⊆ γ (ab_malloc sz rettemp ab);
  free_sound: ∀ ptr ab, Free ptr (γ ab) ⊆ γ (ab_free ptr ab);
  memcpy_sound: ∀ sz al dst src ab, Memcpy sz al dst src (γ ab) ⊆ γ (ab_memcpy sz al dst src ab);
  init_mem_sound: ∀ defs, Init_Mem defs ⊆ γ (init_mem defs)
}.

End GE.