X

Merge branch 'master' into debug_locations

4 files changed, 215 insertions, 77 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index f1c8ec8e..1a6abb6e 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -926,7 +926,7 @@ let add_lineno prev_loc this_loc s =
   if !Clflags.option_g && prev_loc <> this_loc && this_loc <> Cutil.no_loc
   then begin
     let txt = sprintf "#line:%s:%d" (fst this_loc) (snd this_loc) in
-     Ssequence(Sdo(Ebuiltin(EF_annot(intern_string txt, []),
+     Ssequence(Sdo(Ebuiltin(EF_debug(P.one, intern_string txt, []),
                             Tnil, Enil, Tvoid)),
                s)
   end else
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index aba3c094..16d5823b 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -527,6 +527,10 @@ Definition do_ef_annot_val (text: ident) (targ: typ)
   | _ => None
   end.
 
+Definition do_ef_debug (kind: positive) (text: ident) (targs: list typ)
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  Some(w, E0, Vundef, m).
+
 Definition do_external (ef: external_function):
        world -> list val -> mem -> option (world * trace * val * mem) :=
   match ef with
@@ -534,14 +538,13 @@ Definition do_external (ef: external_function):
   | EF_builtin name sg => do_external_function name sg ge
   | EF_vload chunk => do_ef_volatile_load chunk
   | EF_vstore chunk => do_ef_volatile_store chunk
-  | EF_vload_global chunk id ofs => do_ef_volatile_load_global chunk id ofs
-  | EF_vstore_global chunk id ofs => do_ef_volatile_store_global chunk id ofs
   | EF_malloc => do_ef_malloc
   | EF_free => do_ef_free
   | EF_memcpy sz al => do_ef_memcpy sz al
   | EF_annot text targs => do_ef_annot text targs
   | EF_annot_val text targ => do_ef_annot_val text targ
   | EF_inline_asm text sg clob => do_inline_assembly text sg ge
+  | EF_debug kind text targs => do_ef_debug kind text targs
   end.
 
 Lemma do_ef_external_sound:
@@ -550,40 +553,21 @@ Lemma do_ef_external_sound:
   external_call ef ge vargs m t vres m' /\ possible_trace w t w'.
 Proof with try congruence.
   intros until m'.
-
-  assert (VLOAD: forall chunk vargs,
-    do_ef_volatile_load chunk w vargs m = Some (w', t, vres, m') ->
-    volatile_load_sem chunk ge vargs m t vres m' /\ possible_trace w t w').
-  intros chunk vargs'.
-  unfold do_ef_volatile_load. destruct vargs'... destruct v... destruct vargs'... 
-  mydestr. destruct p as [[w'' t''] v]; mydestr.
-  exploit do_volatile_load_sound; eauto. intuition. econstructor; eauto. 
-
-  assert (VSTORE: forall chunk vargs,
-    do_ef_volatile_store chunk w vargs m = Some (w', t, vres, m') ->
-    volatile_store_sem chunk ge vargs m t vres m' /\ possible_trace w t w').
-  intros chunk vargs'.
-  unfold do_ef_volatile_store. destruct vargs'... destruct v... destruct vargs'... destruct vargs'... 
-  mydestr. destruct p as [[w'' t''] m'']. mydestr. 
-  exploit do_volatile_store_sound; eauto. intuition. econstructor; eauto.
-
   destruct ef; simpl.
 (* EF_external *)
   eapply do_external_function_sound; eauto. 
 (* EF_builtin *)
   eapply do_external_function_sound; eauto. 
 (* EF_vload *)
+  unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs... 
+  mydestr. destruct p as [[w'' t''] v]; mydestr.
+  exploit do_volatile_load_sound; eauto. intuition. econstructor; eauto. 
   auto.
 (* EF_vstore *)
+  unfold do_ef_volatile_store. destruct vargs... destruct v... destruct vargs... destruct vargs... 
+  mydestr. destruct p as [[w'' t''] m'']. mydestr. 
+  exploit do_volatile_store_sound; eauto. intuition. econstructor; eauto.
   auto.
-(* EF_vload_global *)
-  rewrite volatile_load_global_charact; simpl.
-  unfold do_ef_volatile_load_global. destruct (Genv.find_symbol ge)...
-  intros. exploit VLOAD; eauto. intros [A B]. split; auto. exists b; auto.
-(* EF_vstore_global *)
-  rewrite volatile_store_global_charact; simpl.
-  unfold do_ef_volatile_store_global. destruct (Genv.find_symbol ge)...
-  intros. exploit VSTORE; eauto. intros [A B]. split; auto. exists b; auto.
 (* EF_malloc *)
   unfold do_ef_malloc. destruct vargs... destruct v... destruct vargs...
   destruct (Mem.alloc m (-4) (Int.unsigned i)) as [m1 b] eqn:?. mydestr.
@@ -606,6 +590,8 @@ Proof with try congruence.
   econstructor. constructor; eauto. constructor.
 (* EF_inline_asm *)
   eapply do_inline_assembly_sound; eauto.
+(* EF_debug *)
+  unfold do_ef_debug. mydestr. split; constructor.
 Qed.
 
 Lemma do_ef_external_complete:
@@ -613,35 +599,17 @@ Lemma do_ef_external_complete:
   external_call ef ge vargs m t vres m' -> possible_trace w t w' ->
   do_external ef w vargs m = Some(w', t, vres, m').
 Proof.
-  intros.
- 
-  assert (VLOAD: forall chunk vargs,
-             volatile_load_sem chunk ge vargs m t vres m' ->
-             do_ef_volatile_load chunk w vargs m = Some (w', t, vres, m')).
-  intros. inv H1; unfold do_ef_volatile_load.
-  exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto.
-
-  assert (VSTORE: forall chunk vargs,
-             volatile_store_sem chunk ge vargs m t vres m' ->
-             do_ef_volatile_store chunk w vargs m = Some (w', t, vres, m')).
-  intros. inv H1; unfold do_ef_volatile_store.
-  exploit do_volatile_store_complete; eauto. intros EQ; rewrite EQ; auto.
-
-  destruct ef; simpl in *.
+  intros. destruct ef; simpl in *.
 (* EF_external *)
   eapply do_external_function_complete; eauto.
 (* EF_builtin *)
   eapply do_external_function_complete; eauto.
 (* EF_vload *)
-  auto.
-(* EF_vstore *)
-  auto.
-(* EF_vload_global *)
-  rewrite volatile_load_global_charact in H; simpl in H. destruct H as [b [P Q]]. 
-  unfold do_ef_volatile_load_global. rewrite P. auto. 
+  inv H; unfold do_ef_volatile_load.
+  exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto.
 (* EF_vstore *)
-  rewrite volatile_store_global_charact in H; simpl in H. destruct H as [b [P Q]]. 
-  unfold do_ef_volatile_store_global. rewrite P. auto. 
+  inv H; unfold do_ef_volatile_store.
+  exploit do_volatile_store_complete; eauto. intros EQ; rewrite EQ; auto.
 (* EF_malloc *)
   inv H; unfold do_ef_malloc. 
   inv H0. rewrite H1. rewrite H2. auto.
@@ -660,6 +628,8 @@ Proof.
   rewrite (eventval_of_val_complete _ _ _ H1). auto.
 (* EF_inline_asm *)
   eapply do_inline_assembly_complete; eauto.
+(* EF_debug *)
+  inv H. inv H0. reflexivity.
 Qed.
 
 (** * Reduction of expressions *)
diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v
index 52ee8377..7fc69324 100644
--- a/cfrontend/SimplLocals.v
+++ b/cfrontend/SimplLocals.v
@@ -22,6 +22,7 @@ Require Import AST.
 Require Import Ctypes.
 Require Import Cop.
 Require Import Clight.
+Require Compopts.
 
 Open Scope error_monad_scope.
 Open Scope string_scope.
@@ -54,6 +55,23 @@ Definition make_cast (a: expr) (tto: type) : expr :=
   | _ => Ecast a tto
   end.
 
+(** Insertion of debug annotations *)
+
+Definition Sdebug_temp (id: ident) (ty: type) :=
+  Sbuiltin None (EF_debug 2%positive id (typ_of_type ty :: nil))
+                (Tcons (typeconv ty) Tnil)
+                (Etempvar id ty :: nil).
+
+Definition Sdebug_var (id: ident) (ty: type) :=
+  Sbuiltin None (EF_debug 5%positive id (AST.Tint :: nil))
+                (Tcons (Tpointer ty noattr) Tnil)
+                (Eaddrof (Evar id ty) (Tpointer ty noattr) :: nil).
+
+Definition Sset_debug (id: ident) (ty: type) (a: expr) :=
+  if Compopts.debug tt
+  then Ssequence (Sset id (make_cast a ty)) (Sdebug_temp id ty)
+  else Sset id (make_cast a ty).
+
 (** Rewriting of expressions and statements. *)
 
 Fixpoint simpl_expr (cenv: compilenv) (a: expr) : expr :=
@@ -94,7 +112,7 @@ Fixpoint simpl_stmt (cenv: compilenv) (s: statement) : res statement :=
   | Sassign a1 a2 =>
       match is_liftable_var cenv a1 with
       | Some id =>
-          OK (Sset id (make_cast (simpl_expr cenv a2) (typeof a1)))
+          OK (Sset_debug id (typeof a1) (simpl_expr cenv a2))
       | None =>
           OK (Sassign (simpl_expr cenv a1) (simpl_expr cenv a2))
       end
@@ -225,6 +243,22 @@ Definition cenv_for (f: function) : compilenv :=
 
 (** Transform a function *)
 
+Definition add_debug_var (id_ty: ident * type) (s: statement) :=
+  let (id, ty) := id_ty in Ssequence (Sdebug_var id ty) s.
+
+Definition add_debug_vars (vars: list (ident * type)) (s: statement) :=
+  if Compopts.debug tt
+  then List.fold_right add_debug_var s vars
+  else s.
+
+Definition add_debug_param (id_ty: ident * type) (s: statement) :=
+  let (id, ty) := id_ty in Ssequence (Sdebug_temp id ty) s.
+
+Definition add_debug_params (params: list (ident * type)) (s: statement) :=
+  if Compopts.debug tt
+  then List.fold_right add_debug_param s params
+  else s.
+
 Definition remove_lifted (cenv: compilenv) (vars: list (ident * type)) :=
   List.filter (fun id_ty => negb (VSet.mem (fst id_ty) cenv)) vars.
 
@@ -235,12 +269,16 @@ Definition transf_function (f: function) : res function :=
   let cenv := cenv_for f in
   assertion (list_disjoint_dec ident_eq (var_names f.(fn_params)) (var_names f.(fn_temps)));
   do body' <- simpl_stmt cenv f.(fn_body);
+  let vars' := remove_lifted cenv (f.(fn_params) ++ f.(fn_vars)) in
+  let temps' := add_lifted cenv f.(fn_vars) f.(fn_temps) in
   OK {| fn_return := f.(fn_return);
         fn_callconv := f.(fn_callconv);
         fn_params := f.(fn_params);
-        fn_vars := remove_lifted cenv (f.(fn_params) ++ f.(fn_vars));
-        fn_temps := add_lifted cenv f.(fn_vars) f.(fn_temps);
-        fn_body := store_params cenv f.(fn_params) body' |}.
+        fn_vars := vars';
+        fn_temps := temps';
+        fn_body := add_debug_params f.(fn_params) 
+                      (store_params cenv f.(fn_params)
+                        (add_debug_vars vars' body')) |}.
 
 (** Whole-program transformation *)
 
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 2a50f985..73092ab9 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -334,6 +334,13 @@ Proof.
   inv H0; constructor.
 Qed.
 
+Lemma forall2_val_casted_inject:
+  forall f vl vl', Val.inject_list f vl vl' ->
+  forall tyl, list_forall2 val_casted vl tyl -> list_forall2 val_casted vl' tyl.
+Proof.
+  induction 1; intros tyl F; inv F; constructor; eauto. eapply val_casted_inject; eauto. 
+Qed.
+
 Inductive val_casted_list: list val -> typelist -> Prop :=
   | vcl_nil:
       val_casted_list nil Tnil
@@ -376,6 +383,116 @@ Proof.
   inv H0; auto.
 Qed.
 
+(** Debug annotations. *)
+
+Lemma cast_typeconv:
+  forall v ty,
+  val_casted v ty ->
+  sem_cast v ty (typeconv ty) = Some v.
+Proof.
+  induction 1; simpl; auto. 
+- destruct sz; auto. 
+- unfold sem_cast. simpl. rewrite dec_eq_true; auto.
+- unfold sem_cast. simpl. rewrite dec_eq_true; auto.
+Qed.
+
+Lemma step_Sdebug_temp:
+  forall f id ty k e le m v,
+  le!id = Some v ->
+  val_casted v ty ->
+  step2 tge (State f (Sdebug_temp id ty) k e le m)
+         E0 (State f Sskip k e le m).
+Proof.
+  intros. unfold Sdebug_temp. eapply step_builtin with (optid := None).
+  econstructor. constructor. eauto. simpl. eapply cast_typeconv; eauto. constructor.
+  simpl. constructor. 
+Qed.
+
+Lemma step_Sdebug_var:
+  forall f id ty k e le m b,
+  e!id = Some(b, ty) ->
+  step2 tge (State f (Sdebug_var id ty) k e le m)
+         E0 (State f Sskip k e le m).
+Proof.
+  intros. unfold Sdebug_var. eapply step_builtin with (optid := None).
+  econstructor. constructor. constructor. eauto. 
+  simpl. reflexivity. constructor. 
+  simpl. constructor. 
+Qed.
+
+Lemma step_Sset_debug:
+  forall f id ty a k e le m v v',
+  eval_expr tge e le m a v ->
+  sem_cast v (typeof a) ty = Some v' ->
+  plus step2 tge (State f (Sset_debug id ty a) k e le m)
+              E0 (State f Sskip k e (PTree.set id v' le) m).
+Proof.
+  intros; unfold Sset_debug. 
+  assert (forall k, step2 tge (State f (Sset id (make_cast a ty)) k e le m)
+                           E0 (State f Sskip k e (PTree.set id v' le) m)).
+  { intros. apply step_set. eapply make_cast_correct; eauto. }
+  destruct (Compopts.debug tt).
+- eapply plus_left. constructor. 
+  eapply star_left. apply H1.
+  eapply star_left. constructor.
+  apply star_one. apply step_Sdebug_temp with (v := v').
+  apply PTree.gss. eapply cast_val_is_casted; eauto. 
+  reflexivity. reflexivity. reflexivity.
+- apply plus_one. apply H1.
+Qed.
+
+Lemma step_add_debug_vars:
+  forall f s e le m vars k,
+  (forall id ty, In (id, ty) vars -> exists b, e!id = Some (b, ty)) ->
+  star step2 tge (State f (add_debug_vars vars s) k e le m)
+              E0 (State f s k e le m).
+Proof.
+  unfold add_debug_vars. destruct (Compopts.debug tt).
+- induction vars; simpl; intros. 
+  + apply star_refl.
+  + destruct a as [id ty].
+    exploit H; eauto. intros (b & TE). 
+    simpl. eapply star_left. constructor. 
+    eapply star_left. eapply step_Sdebug_var; eauto. 
+    eapply star_left. constructor.
+    apply IHvars; eauto.
+    reflexivity. reflexivity. reflexivity.
+- intros. apply star_refl.
+Qed.
+
+Remark bind_parameter_temps_inv:
+  forall id params args le le',
+  bind_parameter_temps params args le = Some le' ->
+  ~In id (var_names params) ->
+  le'!id = le!id.
+Proof.
+  induction params; simpl; intros. 
+  destruct args; inv H. auto.
+  destruct a as [id1 ty1]. destruct args; try discriminate. 
+  transitivity ((PTree.set id1 v le)!id). 
+  eapply IHparams; eauto. apply PTree.gso. intuition. 
+Qed.
+
+Lemma step_add_debug_params:
+  forall f s k e le m params vl le1,
+  list_norepet (var_names params) ->
+  list_forall2 val_casted vl (map snd params) ->
+  bind_parameter_temps params vl le1 = Some le ->
+  star step2 tge (State f (add_debug_params params s) k e le m)
+              E0 (State f s k e le m).
+Proof.
+  unfold add_debug_params. destruct (Compopts.debug tt).
+- induction params as [ | [id ty] params ]; simpl; intros until le1; intros NR CAST BIND; inv CAST; inv NR.
+  + apply star_refl.
+  + assert (le!id = Some a1). { erewrite bind_parameter_temps_inv by eauto. apply PTree.gss. }
+    eapply star_left. constructor. 
+    eapply star_left. eapply step_Sdebug_temp; eauto. 
+    eapply star_left. constructor.
+    eapply IHparams; eauto.
+    reflexivity. reflexivity. reflexivity.
+- intros; apply star_refl.
+Qed.
+
 (** Preservation by assignment to lifted variable. *)
 
 Lemma match_envs_assign_lifted:
@@ -909,7 +1026,8 @@ Theorem match_envs_alloc_variables:
   /\ Mem.inject j' m' tm'
   /\ inject_incr j j'
   /\ (forall b, Mem.valid_block m b -> j' b = j b)
-  /\ (forall b b' delta, j' b = Some(b', delta) -> Mem.valid_block tm b' -> j' b = j b).
+  /\ (forall b b' delta, j' b = Some(b', delta) -> Mem.valid_block tm b' -> j' b = j b)
+  /\ (forall id ty, In (id, ty) vars -> VSet.mem id cenv = false -> exists b, te!id = Some(b, ty)).
 Proof.
   intros. 
   exploit (match_alloc_variables cenv); eauto. instantiate (1 := empty_env). 
@@ -988,6 +1106,10 @@ Proof.
   (* incr *)
   eapply alloc_variables_nextblock; eauto.
   eapply alloc_variables_nextblock; eauto.
+
+  (* other properties *)
+  intuition auto. edestruct F as (b & X & Y); eauto. rewrite H5 in Y.
+  destruct Y as (tb & U & V). exists tb; auto.
 Qed.
 
 Lemma assign_loc_inject:
@@ -1067,19 +1189,6 @@ Proof.
   left. congruence.
 Qed.
 
-Remark bind_parameter_temps_inv:
-  forall id params args le le',
-  bind_parameter_temps params args le = Some le' ->
-  ~In id (var_names params) ->
-  le'!id = le!id.
-Proof.
-  induction params; simpl; intros. 
-  destruct args; inv H. auto.
-  destruct a as [id1 ty1]. destruct args; try discriminate. 
-  transitivity ((PTree.set id1 v le)!id). 
-  eapply IHparams; eauto. apply PTree.gso. intuition. 
-Qed.
-
 Lemma assign_loc_nextblock:
   forall ge ty m b ofs v m',
   assign_loc ge ty m b ofs v m' -> Mem.nextblock m' = Mem.nextblock m.
@@ -1917,6 +2026,7 @@ Proof.
   monadInv TS; auto.
   (* var *)
   destruct (is_liftable_var cenv e); monadInv TS; auto. 
+  unfold Sset_debug. destruct (Compopts.debug tt); auto. 
   (* set *)
   monadInv TS; auto.
   (* call *)
@@ -1975,12 +2085,26 @@ Proof.
 Qed.
 
 Lemma find_label_store_params:
-  forall lbl s k params, find_label lbl (store_params cenv params s) k = find_label lbl s k.
+  forall s k params, find_label lbl (store_params cenv params s) k = find_label lbl s k.
 Proof.
   induction params; simpl. auto. 
   destruct a as [id ty]. destruct (VSet.mem id cenv); auto. 
 Qed.
 
+Lemma find_label_add_debug_vars:
+  forall s k vars, find_label lbl (add_debug_vars vars s) k = find_label lbl s k.
+Proof.
+  unfold add_debug_vars. destruct (Compopts.debug tt); auto. 
+  induction vars; simpl; auto. destruct a as [id ty]; simpl. auto. 
+Qed.
+
+Lemma find_label_add_debug_params:
+  forall s k vars, find_label lbl (add_debug_params vars s) k = find_label lbl s k.
+Proof.
+  unfold add_debug_params. destruct (Compopts.debug tt); auto. 
+  induction vars; simpl; auto. destruct a as [id ty]; simpl. auto. 
+Qed.
+
 End FIND_LABEL.  
 
 
@@ -1999,8 +2123,8 @@ Proof.
   exploit me_vars; eauto. instantiate (1 := id). intros MV. 
   inv H.
   (* local variable *)
-  econstructor; split. 
-  apply plus_one. econstructor. eapply make_cast_correct. eexact A. rewrite typeof_simpl_expr. eexact C.
+  econstructor; split.
+  eapply step_Sset_debug. eauto. rewrite typeof_simpl_expr. eauto.  
   econstructor; eauto with compat. 
   eapply match_envs_assign_lifted; eauto. eapply cast_val_is_casted; eauto.
   eapply match_cont_assign_loc; eauto. exploit me_range; eauto. xomega.
@@ -2154,7 +2278,8 @@ Proof.
     apply compat_cenv_for.
   rewrite H. intros [ts' [tk' [A [B [C D]]]]]. 
   econstructor; split.
-  apply plus_one. econstructor; eauto. simpl. rewrite find_label_store_params. eexact A.
+  apply plus_one. econstructor; eauto. simpl.
+  rewrite find_label_add_debug_params. rewrite find_label_store_params. rewrite find_label_add_debug_vars. eexact A.
   econstructor; eauto.
 
 (* internal function *)
@@ -2166,11 +2291,13 @@ Proof.
     instantiate (1 := cenv_for_gen (addr_taken_stmt f.(fn_body)) (fn_params f ++ fn_vars f)).
     intros. eapply cenv_for_gen_by_value; eauto. rewrite VSF.mem_iff. eexact H4.
     intros. eapply cenv_for_gen_domain. rewrite VSF.mem_iff. eexact H3.
-  intros [j' [te [tm0 [A [B [C [D [E F]]]]]]]].
+  intros [j' [te [tm0 [A [B [C [D [E [F G]]]]]]]]].
+  assert (K: list_forall2 val_casted vargs (map snd (fn_params f))).
+  { apply val_casted_list_params. unfold type_of_function in FUNTY. congruence. }
   exploit store_params_correct.
     eauto. 
     eapply list_norepet_append_left; eauto.
-    apply val_casted_list_params. unfold type_of_function in FUNTY. congruence.
+    eexact K.
     apply val_inject_list_incr with j'; eauto. 
     eexact B. eexact C.
     intros. apply (create_undef_temps_lifted id f). auto.
@@ -2184,8 +2311,11 @@ Proof.
   econstructor; split. 
   eapply plus_left. econstructor. 
   econstructor. exact Y. exact X. exact Z. simpl. eexact A. simpl. eexact Q.
-  simpl. eexact P.
-  traceEq.
+  simpl. eapply star_trans. eapply step_add_debug_params. auto. eapply forall2_val_casted_inject; eauto. eexact Q.
+  eapply star_trans. eexact P. eapply step_add_debug_vars. 
+  unfold remove_lifted; intros. rewrite List.filter_In in H3. destruct H3. 
+  apply negb_true_iff in H4. eauto. 
+  reflexivity. reflexivity. traceEq.
   econstructor; eauto. 
   eapply match_cont_invariant; eauto. 
   intros. transitivity (Mem.load chunk m0 b 0).