From 7a6bb90048db7a254e959b1e3c308bac5fe6c418 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 11 Oct 2015 17:43:59 +0200 Subject: Use Coq strings instead of idents to name external and builtin functions. The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example: * in $ARCH/Machregs.v to define the register conventions for builtin functions; * in the VST program logic from Princeton to treat thread primitives specially. So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq. This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables. --- backend/Selectionproof.v | 162 ++++++++++++++++++++++++++++++++--------------- 1 file changed, 110 insertions(+), 52 deletions(-) (limited to 'backend/Selectionproof.v') diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 1d2f2b3a..8ea4c56e 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -46,9 +46,9 @@ Variable prog: Cminor.program. Variable tprog: CminorSel.program. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. -Hypothesis HELPERS: - forall name sg, In (name, sg) i64_helpers -> helper_declared ge name sg. -Hypothesis TRANSFPROG: transform_partial_program (sel_fundef ge) prog = OK tprog. +Variable hf: helper_functions. +Hypothesis HELPERS: helper_functions_declared ge hf. +Hypothesis TRANSFPROG: transform_partial_program (sel_fundef hf ge) prog = OK tprog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. @@ -65,7 +65,7 @@ Qed. Lemma function_ptr_translated: forall (b: block) (f: Cminor.fundef), Genv.find_funct_ptr ge b = Some f -> - exists tf, Genv.find_funct_ptr tge b = Some tf /\ sel_fundef ge f = OK tf. + exists tf, Genv.find_funct_ptr tge b = Some tf /\ sel_fundef hf ge f = OK tf. Proof. intros. eapply Genv.find_funct_ptr_transf_partial; eauto. Qed. @@ -74,7 +74,7 @@ Lemma functions_translated: forall (v v': val) (f: Cminor.fundef), Genv.find_funct ge v = Some f -> Val.lessdef v v' -> - exists tf, Genv.find_funct tge v' = Some tf /\ sel_fundef ge f = OK tf. + exists tf, Genv.find_funct tge v' = Some tf /\ sel_fundef hf ge f = OK tf. Proof. intros. inv H0. eapply Genv.find_funct_transf_partial; eauto. @@ -82,13 +82,13 @@ Proof. Qed. Lemma sig_function_translated: - forall f tf, sel_fundef ge f = OK tf -> funsig tf = Cminor.funsig f. + forall f tf, sel_fundef hf ge f = OK tf -> funsig tf = Cminor.funsig f. Proof. intros. destruct f; monadInv H; auto. monadInv EQ. auto. Qed. Lemma stackspace_function_translated: - forall f tf, sel_function ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f. + forall f tf, sel_function hf ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f. Proof. intros. monadInv H. auto. Qed. @@ -100,17 +100,17 @@ Proof. Qed. Lemma helper_declared_preserved: - forall id sg, helper_declared ge id sg -> helper_declared tge id sg. + forall id name sg, helper_declared ge id name sg -> helper_declared tge id name sg. Proof. - intros id sg (b & A & B). + intros id name sg (b & A & B). exploit function_ptr_translated; eauto. simpl. intros (tf & P & Q). inv Q. exists b; split; auto. rewrite symbols_preserved. auto. Qed. -Let HELPERS': - forall name sg, In (name, sg) i64_helpers -> helper_declared tge name sg. +Let HELPERS': helper_functions_declared tge hf. Proof. - intros. apply helper_declared_preserved. auto. + red in HELPERS; decompose [Logic.and] HELPERS. + red. auto 20 using helper_declared_preserved. Qed. Section CMCONSTR. @@ -172,7 +172,7 @@ Lemma eval_sel_unop: forall le op a1 v1 v, eval_expr tge sp e m le a1 v1 -> eval_unop op v1 = Some v -> - exists v', eval_expr tge sp e m le (sel_unop op a1) v' /\ Val.lessdef v v'. + exists v', eval_expr tge sp e m le (sel_unop hf op a1) v' /\ Val.lessdef v v'. Proof. destruct op; simpl; intros; FuncInv; try subst v. apply eval_cast8unsigned; auto. @@ -215,7 +215,7 @@ Lemma eval_sel_binop: eval_expr tge sp e m le a1 v1 -> eval_expr tge sp e m le a2 v2 -> eval_binop op v1 v2 m = Some v -> - exists v', eval_expr tge sp e m le (sel_binop op a1 a2) v' /\ Val.lessdef v v'. + exists v', eval_expr tge sp e m le (sel_binop hf op a1 a2) v' /\ Val.lessdef v v'. Proof. destruct op; simpl; intros; FuncInv; try subst v. apply eval_add; auto. @@ -552,7 +552,7 @@ Lemma sel_expr_correct: Cminor.eval_expr ge sp e m a v -> forall e' le m', env_lessdef e e' -> Mem.extends m m' -> - exists v', eval_expr tge sp e' m' le (sel_expr a) v' /\ Val.lessdef v v'. + exists v', eval_expr tge sp e' m' le (sel_expr hf a) v' /\ Val.lessdef v v'. Proof. induction 1; intros; simpl. (* Evar *) @@ -589,7 +589,7 @@ Lemma sel_exprlist_correct: Cminor.eval_exprlist ge sp e m a v -> forall e' le m', env_lessdef e e' -> Mem.extends m m' -> - exists v', eval_exprlist tge sp e' m' le (sel_exprlist a) v' /\ Val.lessdef_list v v'. + exists v', eval_exprlist tge sp e' m' le (sel_exprlist hf a) v' /\ Val.lessdef_list v v'. Proof. induction 1; intros; simpl. exists (@nil val); split; auto. constructor. @@ -603,13 +603,13 @@ Lemma sel_builtin_arg_correct: env_lessdef e e' -> Mem.extends m m' -> Cminor.eval_expr ge sp e m a v -> exists v', - CminorSel.eval_builtin_arg tge sp e' m' (sel_builtin_arg a c) v' + CminorSel.eval_builtin_arg tge sp e' m' (sel_builtin_arg hf a c) v' /\ Val.lessdef v v'. Proof. intros. unfold sel_builtin_arg. exploit sel_expr_correct; eauto. intros (v1 & A & B). exists v1; split; auto. - destruct (builtin_arg_ok (builtin_arg (sel_expr a)) c). + destruct (builtin_arg_ok (builtin_arg (sel_expr hf a)) c). apply eval_builtin_arg; eauto. constructor; auto. Qed. @@ -622,7 +622,7 @@ Lemma sel_builtin_args_correct: forall cl, exists vl', list_forall2 (CminorSel.eval_builtin_arg tge sp e' m') - (sel_builtin_args al cl) + (sel_builtin_args hf al cl) vl' /\ Val.lessdef_list vl vl'. Proof. @@ -647,21 +647,21 @@ Inductive match_cont: Cminor.cont -> CminorSel.cont -> Prop := | match_cont_stop: match_cont Cminor.Kstop Kstop | match_cont_seq: forall s s' k k', - sel_stmt ge s = OK s' -> + sel_stmt hf ge s = OK s' -> match_cont k k' -> match_cont (Cminor.Kseq s k) (Kseq s' k') | match_cont_block: forall k k', match_cont k k' -> match_cont (Cminor.Kblock k) (Kblock k') | match_cont_call: forall id f sp e k f' e' k', - sel_function ge f = OK f' -> + sel_function hf ge f = OK f' -> match_cont k k' -> env_lessdef e e' -> match_cont (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k'). Inductive match_states: Cminor.state -> CminorSel.state -> Prop := | match_state: forall f f' s k s' k' sp e m e' m' - (TF: sel_function ge f = OK f') - (TS: sel_stmt ge s = OK s') + (TF: sel_function hf ge f = OK f') + (TS: sel_stmt hf ge s = OK s') (MC: match_cont k k') (LD: env_lessdef e e') (ME: Mem.extends m m'), @@ -669,7 +669,7 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (Cminor.State f s k sp e m) (State f' s' k' sp e' m') | match_callstate: forall f f' args args' k k' m m' - (TF: sel_fundef ge f = OK f') + (TF: sel_fundef hf ge f = OK f') (MC: match_cont k k') (LD: Val.lessdef_list args args') (ME: Mem.extends m m'), @@ -684,7 +684,7 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (Cminor.Returnstate v k m) (Returnstate v' k' m') | match_builtin_1: forall ef args args' optid f sp e k m al f' e' k' m' - (TF: sel_function ge f = OK f') + (TF: sel_function hf ge f = OK f') (MC: match_cont k k') (LDA: Val.lessdef_list args args') (LDE: env_lessdef e e') @@ -694,7 +694,7 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m) (State f' (Sbuiltin (sel_builtin_res optid) ef al) k' sp e' m') | match_builtin_2: forall v v' optid f sp e k m f' e' m' k' - (TF: sel_function ge f = OK f') + (TF: sel_function hf ge f = OK f') (MC: match_cont k k') (LDV: Val.lessdef v v') (LDE: env_lessdef e e') @@ -712,16 +712,16 @@ Qed. Remark find_label_commut: forall lbl s k s' k', match_cont k k' -> - sel_stmt ge s = OK s' -> + sel_stmt hf ge s = OK s' -> match Cminor.find_label lbl s k, find_label lbl s' k' with | None, None => True - | Some(s1, k1), Some(s1', k1') => sel_stmt ge s1 = OK s1' /\ match_cont k1 k1' + | Some(s1, k1), Some(s1', k1') => sel_stmt hf ge s1 = OK s1' /\ match_cont k1 k1' | _, _ => False end. Proof. induction s; intros until k'; simpl; intros MC SE; try (monadInv SE); simpl; auto. (* store *) - unfold store. destruct (addressing m (sel_expr e)); simpl; auto. + unfold store. destruct (addressing m (sel_expr hf e)); simpl; auto. (* call *) destruct (classify_call ge e); simpl; auto. (* tailcall *) @@ -886,7 +886,7 @@ Proof. - (* Slabel *) left; econstructor; split. constructor. constructor; auto. - (* Sgoto *) - assert (sel_stmt ge (Cminor.fn_body f) = OK (fn_body f')). + assert (sel_stmt hf ge (Cminor.fn_body f) = OK (fn_body f')). { monadInv TF; simpl; auto. } exploit (find_label_commut lbl (Cminor.fn_body f) (Cminor.call_cont k)). apply call_cont_commut; eauto. eauto. @@ -954,39 +954,97 @@ Qed. End PRESERVATION. -Lemma check_helper_correct: - forall ge name sg res, - check_helper ge (name, sg) = OK res -> helper_declared ge name sg. -Proof with (try discriminate). - unfold check_helper; intros. - destruct (Genv.find_symbol ge name) as [b|] eqn:FS... - destruct (Genv.find_funct_ptr ge b) as [fd|] eqn:FP... - destruct fd... destruct e... destruct (ident_eq name0 name)... - destruct (signature_eq sg0 sg)... - subst. exists b; auto. +(** Processing of helper functions *) + +Lemma record_globdefs_sound: + forall p id fd, + (record_globdefs p)!id = Some (Gfun fd) -> + exists b, Genv.find_symbol (Genv.globalenv p) id = Some b + /\ Genv.find_funct_ptr (Genv.globalenv p) b = Some fd. +Proof. + intros until fd. + set (P := fun (m: PTree.t globdef) (ge: Genv.t Cminor.fundef unit) => + m!id = Some (Gfun fd) -> + exists b, Genv.find_symbol ge id = Some b + /\ Genv.find_funct_ptr ge b = Some fd). + assert (REC: forall gl m ge, + P m ge -> + P (fold_left record_globdef gl m) (Genv.add_globals ge gl)). + { + induction gl; simpl; intros. + - auto. + - apply IHgl. red. destruct a as [id1 gd1]; simpl; intros. + unfold Genv.find_symbol; simpl. rewrite PTree.gsspec. destruct (peq id id1). + + subst id1. exists (Genv.genv_next ge); split; auto. + replace gd1 with (@Gfun Cminor.fundef unit fd). + unfold Genv.find_funct_ptr; simpl. apply PTree.gss. + destruct (globdef_of_interest gd1). + rewrite PTree.gss in H0; congruence. + rewrite PTree.grs in H0; congruence. + + assert (m!id = Some (Gfun fd)). + { destruct (globdef_of_interest gd1). + rewrite PTree.gso in H0; auto. + rewrite PTree.gro in H0; auto. } + exploit H; eauto. intros (b & A & B). + exists b; split; auto. unfold Genv.find_funct_ptr; simpl. + destruct gd1; auto. rewrite PTree.gso; auto. + apply Plt_ne. eapply Genv.genv_symb_range; eauto. + } + eapply REC. red; intros. rewrite PTree.gempty in H; discriminate. +Qed. + +Lemma lookup_helper_correct_1: + forall globs name sg id, + lookup_helper globs name sg = OK id -> + globs!id = Some (Gfun (External (EF_external name sg))). +Proof. + intros. + set (P := fun (m: PTree.t globdef) res => res = Some id -> m!id = Some(Gfun(External (EF_external name sg)))). + assert (P globs (PTree.fold (lookup_helper_aux name sg) globs None)). + { apply PTree_Properties.fold_rec; red; intros. + - rewrite <- H0. apply H1; auto. + - discriminate. + - assert (EITHER: k = id /\ v = Gfun (External (EF_external name sg)) + \/ a = Some id). + { unfold lookup_helper_aux in H3. destruct v; auto. destruct f; auto. destruct e; auto. + destruct (String.string_dec name name0); auto. + destruct (signature_eq sg sg0); auto. + inversion H3. left; split; auto. repeat f_equal; auto. } + destruct EITHER as [[X Y] | X]. + subst k v. apply PTree.gss. + apply H2 in X. rewrite PTree.gso by congruence. auto. + } + red in H0. unfold lookup_helper in H. + destruct (PTree.fold (lookup_helper_aux name sg) globs None); inv H. auto. Qed. -Lemma check_helpers_correct: - forall ge res, check_helpers ge = OK res -> - forall name sg, In (name, sg) i64_helpers -> helper_declared ge name sg. +Lemma lookup_helper_correct: + forall p name sg id, + lookup_helper (record_globdefs p) name sg = OK id -> + helper_declared (Genv.globalenv p) id name sg. Proof. - unfold check_helpers; intros ge res CH name sg. - monadInv CH. generalize (mmap_inversion _ _ EQ). - generalize i64_helpers x. induction 1; simpl; intros. - contradiction. - destruct H1. subst a1. eapply check_helper_correct; eauto. eauto. + intros. apply lookup_helper_correct_1 in H. apply record_globdefs_sound in H. auto. Qed. +Theorem get_helpers_correct: + forall p hf, + get_helpers p = OK hf -> helper_functions_declared (Genv.globalenv p) hf. +Proof. + intros. monadInv H. red; simpl. auto 20 using lookup_helper_correct. +Qed. + +(** All together *) + Theorem transf_program_correct: forall prog tprog, sel_program prog = OK tprog -> forward_simulation (Cminor.semantics prog) (CminorSel.semantics tprog). Proof. - intros. unfold sel_program in H. set (ge := Genv.globalenv prog) in *. - destruct (check_helpers ge) eqn:CH; simpl in H; try discriminate. - apply forward_simulation_opt with (match_states := match_states prog tprog) (measure := measure). + intros. unfold sel_program in H. + destruct (get_helpers prog) as [hf|] eqn:G; simpl in H; try discriminate. + apply forward_simulation_opt with (match_states := match_states prog tprog hf) (measure := measure). eapply public_preserved; eauto. apply sel_initial_states; auto. apply sel_final_states; auto. - apply sel_step_correct; auto. eapply check_helpers_correct; eauto. + apply sel_step_correct; auto. eapply get_helpers_correct; eauto. Qed. -- cgit