Module AbMemSignatureCsharpminor

Require Csharpminorannot AlarmMon PExpr.
Import Utf8 Coqlib Util.
Import Maps.
Import AST.
Import Integers.
Import Values.
Import Globalenvs.
Import Csharpminorannot.
Import Annotations.
Import Memory.
Import Events.
Import AdomLib.
Import AlarmMon.

Section GE.

Variable L : Type.
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 L (t+⊥);
  assign_any: ident → PExpr.typ → t → alarm_mon L (t+⊥);
  store: annotation → memory_chunk → expr → expr → t → alarm_mon L (t+⊥);
  assume: expr → t → alarm_mon L (t+⊥ * t+⊥);
  noerror: expr → t → alarm_mon L unit;
  ab_vload: option ident → option (ident * int) → memory_chunk → list expr → t → alarm_mon L (t+⊥);
  ab_vstore: option ident → option (ident * int) → memory_chunk → list expr → t → alarm_mon L (t+⊥);
  deref_fun: expr → t → alarm_mon L (list (ident * fundef));
  push_frame: function →
list expr →
              t → alarm_mon L (t+⊥);
  pop_frame: option (expr) → option(ident) →
             t → alarm_mon L (t+⊥);
  ab_malloc: expr → option ident → t → alarm_mon L (t+⊥);
  ab_free: expr → t → alarm_mon L (t+⊥);
  ab_memcpy: Z → Z → expr → expr → t → alarm_mon L (t+⊥);
  init_mem: list (ident * globdef fundef unit) → alarm_mon L (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 (expr_erase q) v →
         cs = Some ((PTree.set x v t, e) :: s, m)).

Definition AssignAny (x: ident) (ty: PExpr.typ) (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 (expr_erase src) v →
      eval_expr ge e t m (expr_erase 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 (expr_erase 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: concrete_state) (log: list L),
    cs ∈ γ (f b) →
    Some (b, cs) ∈ γ ((f true, f false), (nil, log)).

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 (expr_erase 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 (expr_erase 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 (List.map expr_erase 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 (expr_erase 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 (expr_erase 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 (expr_erase 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 (expr_erase 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 (expr_erase 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 (expr_erase 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 (expr_erase dst_exp) dst →
      eval_expr ge e t m (expr_erase 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.