diff options
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/C2C.ml | 2 | ||||
-rw-r--r-- | cfrontend/Cexec.v | 70 | ||||
-rw-r--r-- | cfrontend/SimplLocals.v | 46 | ||||
-rw-r--r-- | cfrontend/SimplLocalsproof.v | 174 |
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). |