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: identexprtalarm_mon L (t+⊥);
  assign_any: identPExpr.typtalarm_mon L (t+⊥);
  store: annotationmemory_chunkexprexprtalarm_mon L (t+⊥);
  assume: exprtalarm_mon L (t+⊥ * t+⊥);
  noerror: exprtalarm_mon L unit;
  ab_vload: option identoption (ident * int) → memory_chunklist exprtalarm_mon L (t+⊥);
  ab_vstore: option identoption (ident * int) → memory_chunklist exprtalarm_mon L (t+⊥);
  deref_fun: exprtalarm_mon L (list (ident * fundef));
  push_frame: function
list expr
              talarm_mon L (t+⊥);
  pop_frame: option (expr) → option(ident) →
             talarm_mon L (t+⊥);
  ab_malloc: exproption identtalarm_mon L (t+⊥);
  ab_free: exprtalarm_mon L (t+⊥);
  ab_memcpy: ZZexprexprtalarm_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 csExistsCState 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: boolt) :
  ∀ b (cs: concrete_state) (log: list L),
    cs ∈ γ (f b) →
    Some (b, cs) ∈ γ ((f true, f false), (nil, log)).
Proof.
intros () cs log H; exact H. Qed.

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 rcs = 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) vvVundefu = Some tt).

Definition VLoad (rettemp: option ident) (g_ofs: option (ident * int)) (κ: memory_chunk) (args: list expr) (E: ℘ concrete_state) : ℘ (option concrete_state) :=
  ExistsCState Et 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 ofseval_expr ge e t m (expr_erase arg)
    | Some (g', ofs'), nil => g' = gofs' = 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
     thenv, vVundefVal.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 Et e s m cs,
    ∀ tr g b ofs arg v,
    match g_ofs, args with
    | None, addr :: arg' :: nil => arg' = argVptr b ofseval_expr ge e t m (expr_erase addr)
    | Some (g', ofs'), arg' :: nil => g' = gofs' = ofsarg' = arg
    | _, _ => False
    end
   Genv.find_symbol ge g = Some b
   veval_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)
   elsem', 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 eab) ⊆ γ (assign x e ab);
  assign_any_sound: ∀ x ty ab, AssignAny x tyab) ⊆ γ (assign_any x ty ab);
  store_sound: ∀ α κ dst src ab, Store κ dst srcab) ⊆ γ (store α κ dst src ab);
  assume_sound: ∀ e ab, Assume eab) ⊆ γ(assume e ab);
  noerror_sound: ∀ e ab, Noerror eab) ⊆ γ (noerror e ab);
  ab_vload_sound: ∀ rettemp gofs κ args ab, VLoad rettemp gofs κ argsab) ⊆ γ (ab_vload rettemp gofs κ args ab);
  ab_vstore_sound: ∀ rettemp gofs κ args ab, VStore rettemp gofs κ argsab) ⊆ γ (ab_vstore rettemp gofs κ args ab);
  deref_fun_sound: ∀ e ab, DerefFun eab) ⊆ γ (deref_fun e ab);
  pop_frame_sound: ∀ ret rettemp ab, PopFrame ret rettempab) ⊆ γ (pop_frame ret rettemp ab);
  push_frame_sound: ∀ f args ab, PushFrame f argsab) ⊆ γ (push_frame f args ab);
  malloc_sound: ∀ sz rettemp ab, Malloc sz rettempab) ⊆ γ (ab_malloc sz rettemp ab);
  free_sound: ∀ ptr ab, Free ptrab) ⊆ γ (ab_free ptr ab);
  memcpy_sound: ∀ sz al dst src ab, Memcpy sz al dst srcab) ⊆ γ (ab_memcpy sz al dst src ab);
  init_mem_sound: ∀ defs, Init_Mem defs ⊆ γ (init_mem defs)
}.

End GE.