Require Import Coqlib.
Require Intv.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import NormaliseSpec.
Require Import Memory.
Require Import Globalenvs.
Require Import Values_symbolic.
Require Import Values_symbolictype.
Require Import IntFacts.
Require Import Equivalences.

Events and traces

Inductive eventval: Type :=
  | EVint: int -> eventval
  | EVlong: int64 -> eventval
  | EVfloat: float -> eventval
  | EVsingle: float32 -> eventval
  | EVptr_global: ident -> int -> eventval.

Inductive event: Type :=
  | Event_syscall: ident -> list eventval -> eventval -> event
  | Event_vload: memory_chunk -> ident -> int -> eventval -> event
  | Event_vstore: memory_chunk -> ident -> int -> eventval -> event
.
 

Definition trace := list event.

Definition E0 : trace := nil.

Definition Eapp (t1 t2: trace) : trace := t1 ++ t2.

CoInductive traceinf : Type :=
  | Econsinf: event -> traceinf -> traceinf.

Fixpoint Eappinf (t: trace) (T: traceinf) {struct t} : traceinf :=
  match t with
  | nil => T
  | ev :: t' => Econsinf ev (Eappinf t' T)
  end.


Infix "**" := Eapp (at level 60, right associativity).
Infix "***" := Eappinf (at level 60, right associativity).

Lemma E0_left: forall t, E0 ** t = t.

Lemma E0_right: forall t, t ** E0 = t.

Lemma Eapp_assoc: forall t1 t2 t3, (t1 ** t2) ** t3 = t1 ** (t2 ** t3).

Lemma Eapp_E0_inv: forall t1 t2, t1 ** t2 = E0 -> t1 = E0 /\ t2 = E0.
Proof (@app_eq_nil event).
  
Lemma E0_left_inf: forall T, E0 *** T = T.

Lemma Eappinf_assoc: forall t1 t2 T, (t1 ** t2) *** T = t1 *** (t2 *** T).

Hint Rewrite E0_left E0_right Eapp_assoc
             E0_left_inf Eappinf_assoc: trace_rewrite.

Opaque trace E0 Eapp Eappinf.


Ltac substTraceHyp :=
  match goal with
  | [ H: (@eq trace ?x ?y) |- _ ] =>
       subst x || clear H
  end.

Ltac decomposeTraceEq :=
  match goal with
  | [ |- (_ ** _) = (_ ** _) ] =>
      apply (f_equal2 Eapp); auto; decomposeTraceEq
  | _ =>
      auto
  end.

Ltac traceEq :=
  repeat substTraceHyp; autorewrite with trace_rewrite; decomposeTraceEq.


CoInductive traceinf_sim: traceinf -> traceinf -> Prop :=
  | traceinf_sim_cons: forall e T1 T2,
      traceinf_sim T1 T2 ->
      traceinf_sim (Econsinf e T1) (Econsinf e T2).

Lemma traceinf_sim_refl:
  forall T, traceinf_sim T T.
 
Lemma traceinf_sim_sym:
  forall T1 T2, traceinf_sim T1 T2 -> traceinf_sim T2 T1.

Lemma traceinf_sim_trans:
  forall T1 T2 T3,
  traceinf_sim T1 T2 -> traceinf_sim T2 T3 -> traceinf_sim T1 T3.

CoInductive traceinf_sim': traceinf -> traceinf -> Prop :=
  | traceinf_sim'_cons: forall t T1 T2,
      t <> E0 -> traceinf_sim' T1 T2 -> traceinf_sim' (t *** T1) (t *** T2).

Lemma traceinf_sim'_sim:
  forall T1 T2, traceinf_sim' T1 T2 -> traceinf_sim T1 T2.


CoInductive traceinf': Type :=
  | Econsinf': forall (t: trace) (T: traceinf'), t <> E0 -> traceinf'.

Program Definition split_traceinf' (t: trace) (T: traceinf') (NE: t <> E0): event * traceinf' :=
  match t with
  | nil => _
  | e :: nil => (e, T)
  | e :: t' => (e, Econsinf' t' T _)
  end.

CoFixpoint traceinf_of_traceinf' (T': traceinf') : traceinf :=
  match T' with
  | Econsinf' t T'' NOTEMPTY =>
      let (e, tl) := split_traceinf' t T'' NOTEMPTY in
      Econsinf e (traceinf_of_traceinf' tl)
  end.

Remark unroll_traceinf':
  forall T, T = match T with Econsinf' t T' NE => Econsinf' t T' NE end.

Remark unroll_traceinf:
  forall T, T = match T with Econsinf t T' => Econsinf t T' end.

Lemma traceinf_traceinf'_app:
  forall t T NE,
  traceinf_of_traceinf' (Econsinf' t T NE) = t *** traceinf_of_traceinf' T.


Definition trace_prefix (t1 t2: trace) :=
  exists t3, t2 = t1 ** t3.

Definition traceinf_prefix (t1: trace) (T2: traceinf) :=
  exists T3, T2 = t1 *** T3.

Lemma trace_prefix_app:
  forall t1 t2 t,
  trace_prefix t1 t2 ->
  trace_prefix (t ** t1) (t ** t2).

Lemma traceinf_prefix_app:
  forall t1 T2 t,
  traceinf_prefix t1 T2 ->
  traceinf_prefix (t ** t1) (t *** T2).

Relating values and event values

Set Implicit Arguments.

Section EVENTVAL.

Variables F V: Type.
Variable ge: Genv.t F V.


Inductive eventval_match: eventval -> typ -> expr_sym -> Prop :=
| ev_match_int: forall i,
                  eventval_match (EVint i) AST.Tint (Eval (Eint i))
| ev_match_long: forall i,
                   eventval_match (EVlong i) AST.Tlong (Eval (Elong i))
| ev_match_float: forall f,
                    eventval_match (EVfloat f) AST.Tfloat (Eval (Efloat f))
| ev_match_single: forall f,
                     eventval_match (EVsingle f) AST.Tsingle (Eval (Esingle f))
| ev_match_ptr: forall id b ofs,
                  Genv.find_symbol ge id = Some b ->
                  eventval_match (EVptr_global id ofs) AST.Tint (Eval (Eptr b ofs)).

Inductive eventval_list_match: list eventval -> list typ -> list expr_sym -> Prop :=
  | evl_match_nil:
      eventval_list_match nil nil nil
  | evl_match_cons:
      forall ev1 evl ty1 tyl v1 vl,
      eventval_match ev1 ty1 v1 ->
      eventval_list_match evl tyl vl ->
      eventval_list_match (ev1::evl) (ty1::tyl) (v1::vl).


Lemma eventval_match_type:
  forall ev ty v,
  eventval_match ev ty v -> Val.has_type v (Normalise.styp_of_typ ty).

Lemma eventval_list_match_length:
  forall evl tyl vl, eventval_list_match evl tyl vl -> List.length vl = List.length tyl.

Lemma eventval_match_lessdef:
  forall ev ty v1 v2 p,
  eventval_match ev ty v1 -> Val.lessdef p v1 v2 -> eventval_match ev ty v2.

Lemma eventval_list_match_lessdef:
  forall p evl tyl vl1, eventval_list_match evl tyl vl1 ->
  forall vl2, Val.lessdef_list p vl1 vl2 -> eventval_list_match evl tyl vl2.


Variable f: block -> option (block * Z).
Variable p: Val.partial_undef_allocation.

Definition meminj_preserves_globals : Prop :=
     (forall id b, Genv.find_symbol ge id = Some b -> f b = Some(b, 0))
  /\ (forall b gv, Genv.find_var_info ge b = Some gv -> f b = Some(b, 0))
  /\ (forall b1 b2 delta gv, Genv.find_var_info ge b2 = Some gv -> f b1 = Some(b2, delta) -> b2 = b1).

Hypothesis glob_pres: meminj_preserves_globals.

Lemma eventval_match_inject:
  forall ev ty v1 v2,
  eventval_match ev ty v1 -> Val.expr_inject p f v1 v2 -> eventval_match ev ty v2.

Lemma eventval_match_inject_2:
  forall ev ty v,
  eventval_match ev ty v -> Val.expr_inject p f v v.

Lemma eventval_list_match_inject:
  forall evl tyl vl1, eventval_list_match evl tyl vl1 ->
  forall vl2, Val.expr_list_inject p f vl1 vl2 -> eventval_list_match evl tyl vl2.


Lemma eventval_match_determ_1:
  forall ev ty v1 v2, eventval_match ev ty v1 -> eventval_match ev ty v2 -> v1 = v2.

Lemma eventval_match_determ_2:
  forall ev1 ev2 ty v, eventval_match ev1 ty v -> eventval_match ev2 ty v -> ev1 = ev2.

Lemma eventval_list_match_determ_2:
  forall evl1 tyl vl, eventval_list_match evl1 tyl vl ->
  forall evl2, eventval_list_match evl2 tyl vl -> evl1 = evl2.


Definition eventval_valid (ev: eventval) : Prop :=
  match ev with
  | EVint _ => True
  | EVlong _ => True
  | EVfloat _ => True
  | EVsingle _ => True
  | EVptr_global id ofs => exists b, Genv.find_symbol ge id = Some b
  end.

Definition eventval_type (ev: eventval) : typ :=
  match ev with
  | EVint _ => AST.Tint
  | EVlong _ => AST.Tlong
  | EVfloat _ => AST.Tfloat
  | EVsingle _ => AST.Tsingle
  | EVptr_global id ofs => AST.Tint
  end.

Lemma eventval_match_receptive:
  forall ev1 ty v1 ev2,
  eventval_match ev1 ty v1 ->
  eventval_valid ev1 -> eventval_valid ev2 -> eventval_type ev1 = eventval_type ev2 ->
  exists v2, eventval_match ev2 ty v2.

Lemma eventval_match_valid:
  forall ev ty v, eventval_match ev ty v -> eventval_valid ev.

Lemma eventval_match_same_type:
  forall ev1 ty v1 ev2 v2,
  eventval_match ev1 ty v1 -> eventval_match ev2 ty v2 -> eventval_type ev1 = eventval_type ev2.

End EVENTVAL.


Section EVENTVAL_INV.

Variables F1 V1 F2 V2: Type.
Variable ge1: Genv.t F1 V1.
Variable ge2: Genv.t F2 V2.

Hypothesis symbols_preserved:
  forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id.

Lemma eventval_match_preserved:
  forall ev ty v,
  eventval_match ge1 ev ty v -> eventval_match ge2 ev ty v.

Lemma eventval_list_match_preserved:
  forall evl tyl vl,
  eventval_list_match ge1 evl tyl vl -> eventval_list_match ge2 evl tyl vl.

Lemma eventval_valid_preserved:
  forall ev, eventval_valid ge1 ev -> eventval_valid ge2 ev.

End EVENTVAL_INV.

Matching traces.

Section MATCH_TRACES.

Variables F V: Type.
Variable ge: Genv.t F V.


Inductive match_traces: trace -> trace -> Prop :=
  | match_traces_E0:
      match_traces nil nil
  | match_traces_syscall: forall id args res1 res2,
      eventval_valid ge res1 -> eventval_valid ge res2 -> eventval_type res1 = eventval_type res2 ->
      match_traces (Event_syscall id args res1 :: nil) (Event_syscall id args res2 :: nil)
  | match_traces_vload: forall chunk id ofs res1 res2,
      eventval_valid ge res1 -> eventval_valid ge res2 -> eventval_type res1 = eventval_type res2 ->
      match_traces (Event_vload chunk id ofs res1 :: nil) (Event_vload chunk id ofs res2 :: nil)
  | match_traces_vstore: forall chunk id ofs arg,
      match_traces (Event_vstore chunk id ofs arg :: nil) (Event_vstore chunk id ofs arg :: nil)
.

End MATCH_TRACES.


Section MATCH_TRACES_INV.

Variables F1 V1 F2 V2: Type.
Variable ge1: Genv.t F1 V1.
Variable ge2: Genv.t F2 V2.

Hypothesis symbols_preserved:
  forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id.

Lemma match_traces_preserved:
  forall t1 t2, match_traces ge1 t1 t2 -> match_traces ge2 t1 t2.

End MATCH_TRACES_INV.


Definition output_event (ev: event) : Prop :=
  match ev with
  | Event_syscall _ _ _ => False
  | Event_vload _ _ _ _ => False
  | Event_vstore _ _ _ _ => True
  end.
  
Fixpoint output_trace (t: trace) : Prop :=
  match t with
  | nil => True
  | ev :: t' => output_event ev /\ output_trace t'
  end.

Semantics of volatile memory accesses

Definition block_is_volatile (F V: Type) (ge: Genv.t F V) (b: block) : bool :=
  match Genv.find_var_info ge b with
  | None => false
  | Some gv => gv.(gvar_volatile)
  end.

Inductive volatile_load (F V: Type) (ge: Genv.t F V):
                   memory_chunk -> mem -> expr_sym -> trace -> expr_sym -> Prop :=
| volatile_load_vol: forall addr chunk m b ofs id ev v,
                       Mem.mem_norm m addr Ptr = Vptr b ofs ->
                       block_is_volatile ge b = true ->
                       Genv.find_symbol ge id = Some b ->
                       eventval_match ge ev (AST.type_of_chunk chunk) v ->
                       volatile_load ge chunk m addr
                                     (Event_vload chunk id ofs ev :: nil)
                                     (Val.load_result chunk v)
| volatile_load_nonvol: forall addr chunk m b ofs v,
                          Mem.mem_norm m addr Ptr = Vptr b ofs ->
                          block_is_volatile ge b = false ->
                          Mem.load chunk m b (Int.unsigned ofs) = Some v ->
                          volatile_load ge chunk m addr E0 v.


Definition result_of_styp (s: styp) : result :=
  match s with
      Tint => Int
    | Tlong => Long
    | Tfloat => Float
    | Tsingle => Single
  end.


Inductive volatile_store (F V: Type) (ge: Genv.t F V):
                  memory_chunk -> mem -> expr_sym -> expr_sym -> trace -> mem -> Prop :=
| volatile_store_vol: forall addr chunk m b ofs id ev v nv,
                        Mem.mem_norm m addr Ptr = Vptr b ofs ->
                        block_is_volatile ge b = true ->
                        Genv.find_symbol ge id = Some b ->
                        Mem.mem_norm m (Val.load_result chunk v) (result_of_styp (type_of_chunk chunk)) = nv ->
                        eventval_match ge ev (AST.type_of_chunk chunk)
                                       (Eval (NormaliseSpec.sval_of_val nv)) ->
                        volatile_store ge chunk m addr v
                                       (Event_vstore chunk id ofs ev :: nil)
                                       m
| volatile_store_nonvol: forall addr chunk m b ofs v m',
                           Mem.mem_norm m addr Ptr = Vptr b ofs ->
                           block_is_volatile ge b = false ->
                           Mem.store chunk m b (Int.unsigned ofs) v = Some m' ->
                           volatile_store ge chunk m addr v E0 m'.

Semantics of external functions

Definition extcall_sem : Type :=
  forall (F V: Type), Genv.t F V -> list expr_sym -> mem -> trace -> expr_sym -> mem -> Prop.


Definition loc_out_of_bounds (m: mem) (b: block) (ofs: Z) : Prop :=
  ~Mem.perm m b ofs Max Nonempty.

Definition loc_not_writable (m: mem) (b: block) (ofs: Z) : Prop :=
  ~Mem.perm m b ofs Max Writable.

Definition loc_unmapped (f: meminj) (b: block) (ofs: Z): Prop :=
  f b = None.

Definition loc_out_of_reach (f: meminj) (m: mem) (b: block) (ofs: Z): Prop :=
  forall b0 delta,
  f b0 = Some(b, delta) -> ~Mem.perm m b0 (ofs - delta) Max Nonempty.

Definition inject_separated (f f': meminj) (m1 m2: mem): Prop :=
  forall b1 b2 delta,
  f b1 = None -> f' b1 = Some(b2, delta) ->
  ~Mem.valid_block m1 b1 /\ ~Mem.valid_block m2 b2.

Record extcall_properties (sem: extcall_sem)
                          (sg: signature) : Prop := mk_extcall_properties {

  ec_well_typed:
    forall F V (ge: Genv.t F V) vargs m1 t vres m2,
    sem F V ge vargs m1 t vres m2 ->
    Val.has_type vres (Normalise.styp_of_typ (proj_sig_res sg));

  ec_symbols_preserved:
    forall F1 V1 (ge1: Genv.t F1 V1) F2 V2 (ge2: Genv.t F2 V2) vargs m1 t vres m2,
    (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) ->
    (forall b, block_is_volatile ge2 b = block_is_volatile ge1 b) ->
    sem F1 V1 ge1 vargs m1 t vres m2 ->
    sem F2 V2 ge2 vargs m1 t vres m2;

  ec_valid_block:
     forall F V (ge: Genv.t F V) vargs m1 t vres m2 b,
    sem F V ge vargs m1 t vres m2 ->
    Mem.valid_block m1 b -> Mem.valid_block m2 b;

  ec_max_perm:
    forall F V (ge: Genv.t F V) vargs m1 t vres m2 b ofs p,
    sem F V ge vargs m1 t vres m2 ->
    Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p;

  ec_readonly:
    forall F V (ge: Genv.t F V) vargs m1 t vres m2,
    sem F V ge vargs m1 t vres m2 ->
    Mem.unchanged_on (loc_not_writable m1) m1 m2;


  ec_mem_inject:
    forall p F V (ge: Genv.t F V) vargs m1 t vres m2 f m1' vargs'
           (ABI: Mem.all_blocks_injected f m1),
    meminj_preserves_globals ge f ->
    sem F V ge vargs m1 t vres m2 ->
    Mem.inject p f m1 m1' ->
    Val.expr_list_inject p f vargs vargs' ->
exists vres', exists m2',
       sem F V ge vargs' m1' t vres' m2'
       /\ Mem.all_blocks_injected f m2
    /\ Val.expr_inject p f vres vres'
    /\ Mem.inject p f m2 m2'
    /\ Mem.unchanged_on (loc_unmapped f) m1 m2
    /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'
;

  ec_trace_length:
    forall F V ge vargs m t vres m',
    sem F V ge vargs m t vres m' -> (length t <= 1)%nat;

  ec_receptive:
    forall F V ge vargs m t1 vres1 m1 t2,
    sem F V ge vargs m t1 vres1 m1 -> match_traces ge t1 t2 ->
    exists vres2, exists m2, sem F V ge vargs m t2 vres2 m2;

  ec_determ:
    forall F V ge vargs m t1 vres1 m1 t2 vres2 m2,
    sem F V ge vargs m t1 vres1 m1 -> sem F V ge vargs m t2 vres2 m2 ->
    match_traces ge t1 t2 /\ (t1 = t2 -> vres1 = vres2 /\ m1 = m2)
}.

Semantics of volatile loads

Inductive volatile_load_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V):
              list expr_sym -> mem -> trace -> expr_sym -> mem -> Prop :=
  | volatile_load_sem_intro: forall addr m t v ,
      volatile_load ge chunk m addr t v ->
      volatile_load_sem chunk ge (addr :: nil) m t v m.


Lemma volatile_load_preserved:
  forall F1 V1 (ge1: Genv.t F1 V1) F2 V2 (ge2: Genv.t F2 V2) chunk m addr b ofs t v
         (MN: Mem.mem_norm m addr Ptr = Vptr b ofs)
         (GFS: forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id)
         (IV: forall b, block_is_volatile ge2 b = block_is_volatile ge1 b),
    volatile_load ge1 chunk m addr t v ->
    volatile_load ge2 chunk m addr t v.


Remark meminj_preserves_block_is_volatile:
  forall F V (ge: Genv.t F V) f b1 b2 delta,
  meminj_preserves_globals ge f ->
  f b1 = Some (b2, delta) ->
  block_is_volatile ge b2 = block_is_volatile ge b1.

Lemma volatile_load_inject:
  forall p F V (ge: Genv.t F V) f chunk m addr addr' t v m'
         (ABI: Mem.all_blocks_injected f m),
    meminj_preserves_globals ge f ->
    volatile_load ge chunk m addr t v ->
    Val.expr_inject p f addr addr' ->
    Mem.inject p f m m' ->
    exists v', volatile_load ge chunk m' addr' t v' /\ Val.expr_inject p f v v'.

Lemma volatile_load_receptive:
  forall F V (ge: Genv.t F V) chunk m addr t1 t2 v1,
  volatile_load ge chunk m addr t1 v1 -> match_traces ge t1 t2 ->
  exists v2, volatile_load ge chunk m addr t2 v2.

Lemma volatile_load_ok:
  forall chunk,
  extcall_properties (volatile_load_sem chunk)
                     (mksignature (AST.Tint :: nil) (Some (AST.type_of_chunk chunk)) cc_default).

Inductive volatile_load_global_sem (chunk: memory_chunk) (id: ident) (ofs: int)
                                   (F V: Type) (ge: Genv.t F V):
              list expr_sym -> mem -> trace -> expr_sym -> mem -> Prop :=
  | volatile_load_global_sem_intro: forall b t v m,
      Genv.find_symbol ge id = Some b ->
      volatile_load ge chunk m (Eval (Eptr b ofs)) t v ->
      volatile_load_global_sem chunk id ofs ge nil m t v m.

Remark volatile_load_global_charact:
  forall chunk id ofs (F V: Type) (ge: Genv.t F V) vargs m t vres m',
  volatile_load_global_sem chunk id ofs ge vargs m t vres m' <->
  exists b,
    Genv.find_symbol ge id = Some b /\ volatile_load_sem chunk ge (Eval (Eptr b ofs) :: vargs) m t vres m'.

Lemma volatile_load_global_ok:
  forall chunk id ofs,
  extcall_properties (volatile_load_global_sem chunk id ofs)
                     (mksignature nil (Some (AST.type_of_chunk chunk)) cc_default).

Semantics of volatile stores

Inductive volatile_store_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V):
              list expr_sym -> mem -> trace -> expr_sym -> mem -> Prop :=
  | volatile_store_sem_intro: forall addr m1 v t m2 ,
      volatile_store ge chunk m1 addr v t m2 ->
      volatile_store_sem chunk ge (addr :: v :: nil) m1 t (Eval (Eint Int.zero)) m2.

Lemma volatile_store_preserved:
  forall F1 V1 (ge1: Genv.t F1 V1) F2 V2 (ge2: Genv.t F2 V2) chunk m1 addr b ofs v t m2
         (MN: Mem.mem_norm m1 addr Ptr = Vptr b ofs)
         (GFS: forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id)
         (IV: forall b, block_is_volatile ge2 b = block_is_volatile ge1 b)
         (VS: volatile_store ge1 chunk m1 addr v t m2),
    volatile_store ge2 chunk m1 addr v t m2.

Lemma volatile_store_readonly:
  forall F V (ge: Genv.t F V) chunk1 m1 addr v t m2,
  volatile_store ge chunk1 m1 addr v t m2 ->
  Mem.unchanged_on (loc_not_writable m1) m1 m2.


Lemma volatile_store_inject:
  forall p F V (ge: Genv.t F V) f chunk m1 bofs v t m2 m1' bofs' v'
    (ABI:Mem.all_blocks_injected f m1),
  meminj_preserves_globals ge f ->
  volatile_store ge chunk m1 bofs v t m2 ->
  Val.expr_inject p f bofs bofs' ->
  Val.expr_inject p f v v' ->
  Mem.inject p f m1 m1' ->
  exists m2',
       volatile_store ge chunk m1' bofs' v' t m2'
    /\ Mem.inject p f m2 m2'
    /\ Mem.unchanged_on (loc_unmapped f) m1 m2
    /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'.


Lemma volatile_store_receptive:
  forall F V (ge: Genv.t F V) chunk m addr v t1 m1 t2,
  volatile_store ge chunk m addr v t1 m1 -> match_traces ge t1 t2 -> t1 = t2.

Lemma sval_of_val_inj:
  forall v v0, sval_of_val v = sval_of_val v0 -> v = v0.

Lemma volatile_store_ok:
  forall chunk,
  extcall_properties (volatile_store_sem chunk)
                     (mksignature (AST.Tint :: AST.type_of_chunk chunk :: nil) None cc_default).

Inductive volatile_store_global_sem (chunk: memory_chunk) (id: ident) (ofs: int)
                                   (F V: Type) (ge: Genv.t F V):
              list expr_sym -> mem -> trace -> expr_sym -> mem -> Prop :=
  | volatile_store_global_sem_intro: forall b m1 v t m2,
      Genv.find_symbol ge id = Some b ->
      volatile_store ge chunk m1 (Eval (Eptr b ofs)) v t m2 ->
      volatile_store_global_sem chunk id ofs ge (v :: nil) m1 t (Eval (Eint Int.zero)) m2.

Remark volatile_store_global_charact:
  forall chunk id ofs (F V: Type) (ge: Genv.t F V) vargs m t vres m',
  volatile_store_global_sem chunk id ofs ge vargs m t vres m' <->
  exists b, Genv.find_symbol ge id = Some b /\ volatile_store_sem chunk ge (Eval (Eptr b ofs) :: vargs) m t vres m'.

Lemma volatile_store_global_ok:
  forall chunk id ofs,
  extcall_properties (volatile_store_global_sem chunk id ofs)
                     (mksignature (AST.type_of_chunk chunk :: nil) None cc_default).

Semantics of dynamic memory allocation (malloc)

Semantics of memcpy operations.

Inductive extcall_memcpy_sem (sz al: Z) (F V: Type) (ge: Genv.t F V): list expr_sym -> mem -> trace -> expr_sym -> mem -> Prop :=
  | extcall_memcpy_sem_intro: forall bdst odst bsrc osrc m bytes m',
      al = 1 \/ al = 2 \/ al = 4 \/ al = 8 -> sz >= 0 -> (al | sz) ->
      (sz > 0 -> (al | Int.unsigned osrc)) ->
      (sz > 0 -> (al | Int.unsigned odst)) ->
      bsrc <> bdst \/ Int.unsigned osrc = Int.unsigned odst
                   \/ Int.unsigned osrc + sz <= Int.unsigned odst
                   \/ Int.unsigned odst + sz <= Int.unsigned osrc ->
      Mem.loadbytes m bsrc (Int.unsigned osrc) sz = Some bytes ->
      Mem.storebytes m bdst (Int.unsigned odst) bytes = Some m' ->
      forall v' v,
        Mem.mem_norm m v' Ptr = Vptr bdst odst ->
        Mem.mem_norm m v Ptr = Vptr bsrc osrc ->
        extcall_memcpy_sem sz al ge (v' :: v :: nil)
                           m E0 (Eval (Eint Int.zero)) m'.



Lemma extcall_memcpy_ok:
  forall sz al,
  extcall_properties (extcall_memcpy_sem sz al) (mksignature (AST.Tint :: AST.Tint :: nil) None cc_default).

Semantics of annotations.

Lemma map_inj:
  forall {A B: Type} (f: A -> B)
         (f_inj: forall a0 a1, f a0 = f a1 -> a0 = a1) l0 l1,
    map f l0 = map f l1 ->
    l0 = l1.

Semantics of external functions.

Parameter external_functions_sem: ident -> signature -> extcall_sem.

Axiom external_functions_properties:
  forall id sg, extcall_properties (external_functions_sem id sg) sg.


Parameter inline_assembly_sem: ident -> extcall_sem.

Axiom inline_assembly_properties:
  forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None cc_default).


Axiom external_call_not_taken_into_account:
  forall name sg (F V: Type) (ge: Genv.t F V) args m t vres m2,
    external_functions_sem name sg ge args m t vres m2 ->
    forall P : Prop, P.

Axiom inline_assembly_not_taken_into_account:
  forall name (F V: Type) (ge: Genv.t F V) args m t vres m2,
    inline_assembly_sem name ge args m t vres m2 ->
    forall P : Prop, P.

Combined semantics of external calls

Definition external_call (ef: external_function): extcall_sem :=
  match ef with
  | EF_external name sg => external_functions_sem name sg
  | EF_builtin name sg => external_functions_sem name sg
  | EF_vload chunk => volatile_load_sem chunk
  | EF_vstore chunk => volatile_store_sem chunk
  | EF_vload_global chunk id ofs => volatile_load_global_sem chunk id ofs
  | EF_vstore_global chunk id ofs => volatile_store_global_sem chunk id ofs
  | EF_memcpy sz al => extcall_memcpy_sem sz al
  | EF_inline_asm txt => inline_assembly_sem txt
  end.

Theorem external_call_spec:
  forall ef,
  extcall_properties (external_call ef) (ef_sig ef).

Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef).
Definition external_call_symbols_preserved_gen ef := ec_symbols_preserved (external_call_spec ef).
Definition external_call_valid_block ef := ec_valid_block (external_call_spec ef).
Definition external_call_max_perm ef := ec_max_perm (external_call_spec ef).
Definition external_call_readonly ef := ec_readonly (external_call_spec ef).
Definition external_call_mem_inject ef := ec_mem_inject (external_call_spec ef).
Definition external_call_trace_length ef := ec_trace_length (external_call_spec ef).
Definition external_call_receptive ef := ec_receptive (external_call_spec ef).
Definition external_call_determ ef := ec_determ (external_call_spec ef).


Lemma external_call_symbols_preserved:
  forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2,
  external_call ef ge1 vargs m1 t vres m2 ->
  (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) ->
  (forall b, Genv.find_var_info ge2 b = Genv.find_var_info ge1 b) ->
  external_call ef ge2 vargs m1 t vres m2.

Require Import Errors.

Lemma external_call_symbols_preserved_2:
  forall ef F1 V1 F2 V2 (tvar: V1 -> res V2)
         (ge1: Genv.t F1 V1) (ge2: Genv.t F2 V2) vargs m1 t vres m2,
  external_call ef ge1 vargs m1 t vres m2 ->
  (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) ->
  (forall b gv1, Genv.find_var_info ge1 b = Some gv1 ->
     exists gv2, Genv.find_var_info ge2 b = Some gv2 /\ transf_globvar tvar gv1 = OK gv2) ->
  (forall b gv2, Genv.find_var_info ge2 b = Some gv2 ->
     exists gv1, Genv.find_var_info ge1 b = Some gv1 /\ transf_globvar tvar gv1 = OK gv2) ->
  external_call ef ge2 vargs m1 t vres m2.


Lemma external_call_nextblock:
  forall ef (F V : Type) (ge : Genv.t F V) vargs m1 t vres m2,
  external_call ef ge vargs m1 t vres m2 ->
  Ple (Mem.nextblock m1) (Mem.nextblock m2).


Lemma external_call_match_traces:
  forall ef (F V : Type) (ge : Genv.t F V) vargs m t1 vres1 m1 t2 vres2 m2,
  external_call ef ge vargs m t1 vres1 m1 ->
  external_call ef ge vargs m t2 vres2 m2 ->
  match_traces ge t1 t2.

Lemma external_call_deterministic:
  forall ef (F V : Type) (ge : Genv.t F V) vargs m t vres1 m1 vres2 m2,
  external_call ef ge vargs m t vres1 m1 ->
  external_call ef ge vargs m t vres2 m2 ->
  vres1 = vres2 /\ m1 = m2.


Fixpoint decode_longs (tyl: list typ) (vl: list expr_sym) : list expr_sym :=
  match tyl with
  | nil => nil
  | AST.Tlong :: tys =>
      match vl with
      | v1 :: v2 :: vs => Val.longofwords v1 v2 :: decode_longs tys vs
      | _ => nil
      end
  | ty :: tys =>
      match vl with
      | v1 :: vs => v1 :: decode_longs tys vs
      | _ => nil
      end
  end.

Definition encode_long (oty: option typ) (v: expr_sym) : list expr_sym :=
  match oty with
  | Some AST.Tlong => Val.hiword v :: Val.loword v :: nil
  | _ => v :: nil
  end.

Definition proj_sig_res' (s: signature) : list typ :=
  match s.(sig_res) with
  | Some AST.Tlong => AST.Tint :: AST.Tint :: nil
  | Some ty => ty :: nil
  | None => AST.Tint :: nil
  end.

Inductive external_call'
      (ef: external_function) (F V: Type) (ge: Genv.t F V)
      (vargs: list expr_sym) (m1: mem) (t: trace) (vres: list expr_sym) (m2: mem) : Prop :=
  external_call'_intro: forall v,
    external_call ef ge (decode_longs (sig_args (ef_sig ef)) vargs) m1 t v m2 ->
    vres = encode_long (sig_res (ef_sig ef)) v ->
    external_call' ef ge vargs m1 t vres m2.

Lemma decode_longs_lessdef:
  forall p tyl vl1 vl2, Val.lessdef_list p vl1 vl2 -> Val.lessdef_list p (decode_longs tyl vl1) (decode_longs tyl vl2).

Lemma decode_longs_inject:
  forall p f tyl vl1 vl2, Val.expr_list_inject p f vl1 vl2 -> Val.expr_list_inject p f (decode_longs tyl vl1) (decode_longs tyl vl2).

Lemma encode_long_lessdef:
  forall p oty v1 v2, Val.lessdef p v1 v2 -> Val.lessdef_list p (encode_long oty v1) (encode_long oty v2).

Lemma encode_long_inject:
  forall p f oty v1 v2, Val.expr_inject p f v1 v2 -> Val.expr_list_inject p f (encode_long oty v1) (encode_long oty v2).

Lemma encode_long_has_type:
  forall v sg,
  Val.has_type v (styp_of_ast (proj_sig_res sg)) ->
  Val.has_type_list (encode_long (sig_res sg) v) (map styp_of_ast (proj_sig_res' sg)).

Lemma external_call_well_typed':
  forall ef (F V : Type) (ge : Genv.t F V) vargs m1 t vres m2,
  external_call' ef ge vargs m1 t vres m2 ->
  Val.has_type_list vres (map styp_of_ast (proj_sig_res' (ef_sig ef))).

Lemma external_call_symbols_preserved':
  forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2,
  external_call' ef ge1 vargs m1 t vres m2 ->
  (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) ->
  (forall b, Genv.find_var_info ge2 b = Genv.find_var_info ge1 b) ->
  external_call' ef ge2 vargs m1 t vres m2.

Lemma external_call_valid_block':
  forall ef (F V : Type) (ge : Genv.t F V) vargs m1 t vres m2 b,
  external_call' ef ge vargs m1 t vres m2 ->
  Mem.valid_block m1 b -> Mem.valid_block m2 b.

Lemma external_call_nextblock':
  forall ef (F V : Type) (ge : Genv.t F V) vargs m1 t vres m2,
  external_call' ef ge vargs m1 t vres m2 ->
  Ple (Mem.nextblock m1) (Mem.nextblock m2).


Lemma same_eval_load_result:
  forall chunk v v',
    same_eval v v' ->
    same_eval (Val.load_result chunk v) (Val.load_result chunk v').

Lemma external_call_se:
  forall (F V: Type) m m' args args' ef (ge: Genv.t F V) t vres m2,
    mem_equiv m m' ->
    list_forall2 same_eval args args' ->
    external_call ef ge args m t vres m2 ->
    exists vres' m2',
      external_call ef ge args' m' t vres' m2' /\
      same_eval vres vres' /\
      mem_equiv m2 m2'.



Lemma external_call_mem_inject':
  forall ef p F V (ge: Genv.t F V) vargs m1 t vres m2 f m1' vargs'
  (ABI: Mem.all_blocks_injected f m1),
  meminj_preserves_globals ge f ->
  external_call' ef ge vargs m1 t vres m2 ->
  Mem.inject p f m1 m1' ->
  Val.expr_list_inject p f vargs vargs' ->
  exists vres' m2',
     external_call' ef ge vargs' m1' t vres' m2'
  /\ Val.expr_list_inject p f vres vres'
  /\ Mem.inject p f m2 m2'
  /\ Mem.unchanged_on (loc_unmapped f) m1 m2
  /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'
.


Lemma external_call_determ':
  forall ef (F V : Type) (ge : Genv.t F V) vargs m t1 vres1 m1 t2 vres2 m2,
  external_call' ef ge vargs m t1 vres1 m1 ->
  external_call' ef ge vargs m t2 vres2 m2 ->
  match_traces ge t1 t2 /\ (t1 = t2 -> vres1 = vres2 /\ m1 = m2).

Lemma external_call_match_traces':
  forall ef (F V : Type) (ge : Genv.t F V) vargs m t1 vres1 m1 t2 vres2 m2,
  external_call' ef ge vargs m t1 vres1 m1 ->
  external_call' ef ge vargs m t2 vres2 m2 ->
  match_traces ge t1 t2.

Lemma external_call_deterministic':
  forall ef (F V : Type) (ge : Genv.t F V) vargs m t vres1 m1 vres2 m2,
  external_call' ef ge vargs m t vres1 m1 ->
  external_call' ef ge vargs m t vres2 m2 ->
  vres1 = vres2 /\ m1 = m2.