From be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 18 Feb 2020 16:57:17 +0100 Subject: Refine the type of function results in AST.signature Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions. --- backend/Allocation.v | 10 +++++----- backend/Allocproof.v | 15 ++++++++------- backend/Asmexpandaux.ml | 2 +- backend/Cminor.v | 20 ++++++++++++++++---- backend/Cminortyping.v | 45 ++++++++++++++++++++++++--------------------- backend/PrintAsmaux.ml | 6 +++--- backend/PrintCminor.ml | 4 +--- backend/RTLgen.v | 16 ++++++---------- backend/RTLgenspec.v | 12 ++++++------ backend/RTLtyping.v | 35 +++++++++++++++++++---------------- backend/SplitLong.vp | 14 +++++++------- backend/Tailcall.v | 2 +- backend/Tailcallproof.v | 10 ++++------ 13 files changed, 101 insertions(+), 90 deletions(-) (limited to 'backend') diff --git a/backend/Allocation.v b/backend/Allocation.v index 13e14530..08e0a4f4 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -734,11 +734,11 @@ Function add_equations_args (rl: list reg) (tyl: list typ) (ll: list (rpair loc) (** [add_equations_res] is similar but is specialized to the case where there is only one pseudo-register. *) -Function add_equations_res (r: reg) (oty: option typ) (p: rpair mreg) (e: eqs) : option eqs := - match p, oty with +Function add_equations_res (r: reg) (ty: typ) (p: rpair mreg) (e: eqs) : option eqs := + match p, ty with | One mr, _ => Some (add_equation (Eq Full r (R mr)) e) - | Twolong mr1 mr2, Some Tlong => + | Twolong mr1 mr2, Tlong => if Archi.ptr64 then None else Some (add_equation (Eq Low r (R mr2)) (add_equation (Eq High r (R mr1)) e)) | _, _ => @@ -1084,7 +1084,7 @@ Definition transfer_aux (f: RTL.function) (env: regenv) | BStailcall sg ros args mv1 ros' => let args' := loc_arguments sg in assertion (tailcall_is_possible sg); - assertion (opt_typ_eq sg.(sig_res) f.(RTL.fn_sig).(sig_res)); + assertion (rettype_eq sg.(sig_res) f.(RTL.fn_sig).(sig_res)); assertion (ros_compatible_tailcall ros'); do e1 <- add_equation_ros ros ros' empty_eqs; do e2 <- add_equations_args args (sig_args sg) args' e1; @@ -1114,7 +1114,7 @@ Definition transfer_aux (f: RTL.function) (env: regenv) track_moves env mv empty_eqs | BSreturn (Some arg) mv => let arg' := loc_result (RTL.fn_sig f) in - do e1 <- add_equations_res arg (sig_res (RTL.fn_sig f)) arg' empty_eqs; + do e1 <- add_equations_res arg (proj_sig_res (RTL.fn_sig f)) arg' empty_eqs; track_moves env mv e1 end. diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 1804f46b..51755912 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -1301,10 +1301,10 @@ Proof. Qed. Lemma add_equations_res_lessdef: - forall r oty l e e' rs ls, - add_equations_res r oty l e = Some e' -> + forall r ty l e e' rs ls, + add_equations_res r ty l e = Some e' -> satisf rs ls e' -> - Val.has_type rs#r (match oty with Some ty => ty | None => Tint end) -> + Val.has_type rs#r ty -> Val.lessdef rs#r (Locmap.getpair (map_rpair R l) ls). Proof. intros. functional inversion H; simpl. @@ -1892,7 +1892,7 @@ Qed. Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signature -> Prop := | match_stackframes_nil: forall sg, - sg.(sig_res) = Some Tint -> + sg.(sig_res) = Tint -> match_stackframes nil nil sg | match_stackframes_cons: forall res f sp pc rs s tf bb ls ts sg an e env @@ -2425,13 +2425,13 @@ Proof. (return_regs (parent_locset ts) ls1)) with (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f))) ls1). eapply add_equations_res_lessdef; eauto. - rewrite H13. apply WTRS. + rewrite <- H14. apply WTRS. generalize (loc_result_caller_save (RTL.fn_sig f)). destruct (loc_result (RTL.fn_sig f)); simpl. intros A; rewrite A; auto. intros [A B]; rewrite A, B; auto. apply return_regs_agree_callee_save. - unfold proj_sig_res. rewrite <- H11; rewrite H13. apply WTRS. + rewrite <- H11, <- H14. apply WTRS. (* internal function *) - monadInv FUN. simpl in *. @@ -2463,7 +2463,8 @@ Proof. simpl. destruct (loc_result (ef_sig ef)) eqn:RES; simpl. rewrite Locmap.gss; auto. generalize (loc_result_pair (ef_sig ef)); rewrite RES; intros (A & B & C & D & E). - exploit external_call_well_typed; eauto. unfold proj_sig_res; rewrite B. intros WTRES'. + assert (WTRES': Val.has_type v' Tlong). + { rewrite <- B. eapply external_call_well_typed; eauto. } rewrite Locmap.gss. rewrite Locmap.gso by (red; auto). rewrite Locmap.gss. rewrite val_longofwords_eq_1 by auto. auto. red; intros. rewrite (AG l H0). diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml index f5c76925..0530abe4 100644 --- a/backend/Asmexpandaux.ml +++ b/backend/Asmexpandaux.ml @@ -96,7 +96,7 @@ let translate_annot sp preg_to_dwarf annot = | a::_ -> aux a) let builtin_nop = - let signature ={sig_args = []; sig_res = None; sig_cc = cc_default} in + let signature ={sig_args = []; sig_res = Tvoid; sig_cc = cc_default} in let name = coqstring_of_camlstring "__builtin_nop" in Pbuiltin(EF_builtin(name,signature),[],BR_none) diff --git a/backend/Cminor.v b/backend/Cminor.v index ca01ad50..91a4c104 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -676,12 +676,24 @@ Definition outcome_block (out: outcome) : outcome := | out => out end. +(* Definition outcome_result_value - (out: outcome) (retsig: option typ) (vres: val) : Prop := + (out: outcome) (retsig: rettype) (vres: val) : Prop := match out with | Out_normal => vres = Vundef | Out_return None => vres = Vundef - | Out_return (Some v) => retsig <> None /\ vres = v + | Out_return (Some v) => retsig <> Tvoid /\ vres = v + | Out_tailcall_return v => vres = v + | _ => False + end. +*) + +Definition outcome_result_value + (out: outcome) (vres: val) : Prop := + match out with + | Out_normal => vres = Vundef + | Out_return None => vres = Vundef + | Out_return (Some v) => vres = v | Out_tailcall_return v => vres = v | _ => False end. @@ -711,7 +723,7 @@ Inductive eval_funcall: Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) -> set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e -> exec_stmt f (Vptr sp Ptrofs.zero) e m1 f.(fn_body) t e2 m2 out -> - outcome_result_value out f.(fn_sig).(sig_res) vres -> + outcome_result_value out vres -> outcome_free_mem out m2 sp f.(fn_stackspace) m3 -> eval_funcall m (Internal f) vargs t m3 vres | eval_funcall_external: @@ -995,7 +1007,7 @@ Proof. subst vres. replace k with (call_cont k') by congruence. apply star_one. apply step_return_0; auto. (* Out_return Some *) - destruct H3. subst vres. + subst vres. replace k with (call_cont k') by congruence. apply star_one. eapply step_return_1; eauto. (* Out_tailcall_return *) diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v index fccbda27..92ec45f2 100644 --- a/backend/Cminortyping.v +++ b/backend/Cminortyping.v @@ -130,7 +130,7 @@ Definition opt_set (e: S.typenv) (optid: option ident) (ty: typ) : res S.typenv | Some id => S.set e id ty end. -Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv := +Fixpoint type_stmt (tret: rettype) (e: S.typenv) (s: stmt) : res S.typenv := match s with | Sskip => OK e | Sassign id a => type_assign e id a @@ -141,7 +141,7 @@ Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv := do e2 <- type_exprlist e1 args sg.(sig_args); opt_set e2 optid (proj_sig_res sg) | Stailcall sg fn args => - assertion (opt_typ_eq sg.(sig_res) tret); + assertion (rettype_eq sg.(sig_res) tret); do e1 <- type_expr e fn Tptr; type_exprlist e1 args sg.(sig_args) | Sbuiltin optid ef args => @@ -163,10 +163,14 @@ Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv := | Sswitch sz a tbl dfl => type_expr e a (if sz then Tlong else Tint) | Sreturn opta => - match opta, tret with - | None, _ => OK e - | Some a, Some t => type_expr e a t - | _, _ => Error (msg "inconsistent return") + match opta with + | None => OK e + | Some a => type_expr e a (proj_rettype tret) +(* + if rettype_eq tret Tvoid + then Error (msg "inconsistent return") + else type_expr e a (proj_rettype tret) +*) end | Slabel lbl s1 => type_stmt tret e s1 @@ -186,7 +190,7 @@ Definition type_function (f: function) : res typenv := Section SPEC. Variable env: ident -> typ. -Variable tret: option typ. +Variable tret: rettype. Inductive wt_expr: expr -> typ -> Prop := | wt_Evar: forall id, @@ -205,9 +209,9 @@ Inductive wt_expr: expr -> typ -> Prop := wt_expr a1 Tptr -> wt_expr (Eload chunk a1) (type_of_chunk chunk). -Definition wt_opt_assign (optid: option ident) (optty: option typ) : Prop := +Definition wt_opt_assign (optid: option ident) (ty: rettype) : Prop := match optid with - | Some id => match optty with Some ty => ty | None => Tint end = env id + | Some id => proj_rettype ty = env id | _ => True end. @@ -251,8 +255,8 @@ Inductive wt_stmt: stmt -> Prop := wt_stmt (Sswitch sz a tbl dfl) | wt_Sreturn_none: wt_stmt (Sreturn None) - | wt_Sreturn_some: forall a t, - tret = Some t -> wt_expr a t -> + | wt_Sreturn_some: forall a, + wt_expr a (proj_rettype tret) -> wt_stmt (Sreturn (Some a)) | wt_Slabel: forall lbl s1, wt_stmt s1 -> @@ -393,7 +397,7 @@ Proof. - constructor; eauto. - constructor. - constructor; eauto using type_expr_sound with ty. -- destruct tret, o; try (monadInv T); econstructor; eauto using type_expr_sound with ty. +- destruct o; try (monadInv T); econstructor; eauto using type_expr_sound with ty. - constructor; eauto. - constructor. Qed. @@ -414,9 +418,9 @@ Definition wt_env (env: typenv) (e: Cminor.env) : Prop := Definition def_env (f: function) (e: Cminor.env) : Prop := forall id, In id f.(fn_params) \/ In id f.(fn_vars) -> exists v, e!id = Some v. -Inductive wt_cont_call: cont -> option typ -> Prop := +Inductive wt_cont_call: cont -> rettype -> Prop := | wt_cont_Kstop: - wt_cont_call Kstop (Some Tint) + wt_cont_call Kstop Tint | wt_cont_Kcall: forall optid f sp e k tret env (WT_FN: wt_function env f) (WT_CONT: wt_cont env f.(fn_sig).(sig_res) k) @@ -425,7 +429,7 @@ Inductive wt_cont_call: cont -> option typ -> Prop := (WT_DEST: wt_opt_assign env optid tret), wt_cont_call (Kcall optid f sp e k) tret -with wt_cont: typenv -> option typ -> cont -> Prop := +with wt_cont: typenv -> rettype -> cont -> Prop := | wt_cont_Kseq: forall env tret s k, wt_stmt env tret s -> wt_cont env tret k -> @@ -451,7 +455,7 @@ Inductive wt_state: state -> Prop := (WT_CONT: wt_cont_call k (funsig f).(sig_res)), wt_state (Callstate f args k m) | wt_return_state: forall v k m tret - (WT_RES: Val.has_type v (match tret with None => Tint | Some t => t end)) + (WT_RES: Val.has_type v (proj_rettype tret)) (WT_CONT: wt_cont_call k tret), wt_state (Returnstate v k m). @@ -651,9 +655,8 @@ Proof. rewrite H8; eapply call_cont_wt; eauto. - inv WT_STMT. exploit external_call_well_typed; eauto. intros TRES. econstructor; eauto using wt_Sskip. - unfold proj_sig_res in TRES; red in H5. - destruct optid. rewrite H5 in TRES. apply wt_env_assign; auto. assumption. - destruct optid. apply def_env_assign; auto. assumption. + destruct optid; auto. apply wt_env_assign; auto. rewrite <- H5; auto. + destruct optid; auto. apply def_env_assign; auto. - inv WT_STMT. econstructor; eauto. econstructor; eauto. - inv WT_STMT. destruct b; econstructor; eauto. - inv WT_STMT. econstructor; eauto. econstructor; eauto. constructor; auto. @@ -664,7 +667,7 @@ Proof. - econstructor; eauto using wt_Sexit. - inv WT_STMT. econstructor; eauto using call_cont_wt. exact I. - inv WT_STMT. econstructor; eauto using call_cont_wt. - rewrite H2. eapply wt_eval_expr; eauto. + eapply wt_eval_expr; eauto. - inv WT_STMT. econstructor; eauto. - inversion WT_FN; subst. assert (WT_CK: wt_cont env (sig_res (fn_sig f)) (call_cont k)). @@ -675,7 +678,7 @@ Proof. constructor; auto. apply wt_env_set_locals. apply wt_env_set_params. rewrite H2; auto. red; intros. apply def_set_locals. destruct H4; auto. left; apply def_set_params; auto. -- exploit external_call_well_typed; eauto. unfold proj_sig_res. simpl in *. intros. +- exploit external_call_well_typed; eauto. intros. econstructor; eauto. - inv WT_CONT. econstructor; eauto using wt_Sskip. red in WT_DEST. diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 8652b2c5..d82e6f84 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -99,7 +99,7 @@ let exists_constants () = let current_function_stacksize = ref 0l let current_function_sig = - ref { sig_args = []; sig_res = None; sig_cc = cc_default } + ref { sig_args = []; sig_res = Tvoid; sig_cc = cc_default } (* Functions for printing of symbol names *) let elf_symbol oc symb = @@ -268,8 +268,8 @@ let re_asm_param_2 = Str.regexp "%\\([QR]?\\)\\([0-9]+\\)" let print_inline_asm print_preg oc txt sg args res = let (operands, ty_operands) = match sg.sig_res with - | None -> (args, sg.sig_args) - | Some tres -> (builtin_arg_of_res res :: args, tres :: sg.sig_args) in + | Tvoid -> (args, sg.sig_args) + | tres -> (builtin_arg_of_res res :: args, proj_rettype tres :: sg.sig_args) in let print_fragment = function | Str.Text s -> output_string oc s diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 8c255a65..b77c5645 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -193,9 +193,7 @@ let print_sig p sg = List.iter (fun t -> fprintf p "%s ->@ " (name_of_type t)) sg.sig_args; - match sg.sig_res with - | None -> fprintf p "void" - | Some ty -> fprintf p "%s" (name_of_type ty) + fprintf p "%s" (name_of_rettype sg.sig_res) let rec just_skips s = match s with diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 9d7a8506..f7280c9e 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -410,12 +410,11 @@ Fixpoint convert_builtin_args {A: Type} (al: list (builtin_arg expr)) (rl: list a1' :: convert_builtin_args al rl1 end. -Definition convert_builtin_res (map: mapping) (oty: option typ) (r: builtin_res ident) : mon (builtin_res reg) := - match r, oty with - | BR id, _ => do r <- find_var map id; ret (BR r) - | BR_none, None => ret BR_none - | BR_none, Some _ => do r <- new_reg; ret (BR r) - | _, _ => error (Errors.msg "RTLgen: bad builtin_res") +Definition convert_builtin_res (map: mapping) (ty: rettype) (r: builtin_res ident) : mon (builtin_res reg) := + match r with + | BR id => do r <- find_var map id; ret (BR r) + | BR_none => if rettype_eq ty Tvoid then ret BR_none else (do r <- new_reg; ret (BR r)) + | _ => error (Errors.msg "RTLgen: bad builtin_res") end. (** Translation of an expression. [transl_expr map a rd nd] @@ -667,10 +666,7 @@ Fixpoint reserve_labels (s: stmt) (ms: labelmap * state) (** Translation of a CminorSel function. *) Definition ret_reg (sig: signature) (rd: reg) : option reg := - match sig.(sig_res) with - | None => None - | Some ty => Some rd - end. + if rettype_eq sig.(sig_res) Tvoid then None else Some rd. Definition transl_fun (f: CminorSel.function) (ngoto: labelmap): mon (node * list reg) := do (rparams, map1) <- add_vars init_mapping f.(CminorSel.fn_params); diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 17022a7d..72693f63 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -639,8 +639,8 @@ Lemma new_reg_return_ok: map_valid map s1 -> return_reg_ok s2 map (ret_reg sig r). Proof. - intros. unfold ret_reg. destruct (sig_res sig); constructor. - eauto with rtlg. eauto with rtlg. + intros. unfold ret_reg. + destruct (rettype_eq (sig_res sig) Tvoid); constructor; eauto with rtlg. Qed. (** * Relational specification of the translation *) @@ -1224,9 +1224,9 @@ Lemma convert_builtin_res_charact: Proof. destruct res; simpl; intros. - monadInv TR. constructor. unfold find_var in EQ. destruct (map_vars map)!x; inv EQ; auto. -- destruct oty; monadInv TR. -+ constructor. eauto with rtlg. +- destruct (rettype_eq oty Tvoid); monadInv TR. + constructor. ++ constructor. eauto with rtlg. - monadInv TR. Qed. @@ -1350,7 +1350,7 @@ Proof. intros [C D]. eapply tr_function_intro; eauto with rtlg. eapply transl_stmt_charact; eauto with rtlg. - unfold ret_reg. destruct (sig_res (CminorSel.fn_sig f)). - constructor. eauto with rtlg. eauto with rtlg. + unfold ret_reg. destruct (rettype_eq (sig_res (CminorSel.fn_sig f)) Tvoid). constructor. + constructor; eauto with rtlg. Qed. diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 8336d1bf..5b8646ea 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -151,11 +151,12 @@ Inductive wt_instr : instruction -> Prop := list_length_z tbl * 4 <= Int.max_unsigned -> wt_instr (Ijumptable arg tbl) | wt_Ireturn_none: - funct.(fn_sig).(sig_res) = None -> + funct.(fn_sig).(sig_res) = Tvoid -> wt_instr (Ireturn None) | wt_Ireturn_some: forall arg ty, - funct.(fn_sig).(sig_res) = Some ty -> + funct.(fn_sig).(sig_res) <> Tvoid -> + env arg = proj_sig_res funct.(fn_sig) -> env arg = ty -> wt_instr (Ireturn (Some arg)). @@ -298,7 +299,7 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := | Itailcall sig ros args => do e1 <- type_ros e ros; do e2 <- S.set_list e1 args sig.(sig_args); - if opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res) then + if rettype_eq sig.(sig_res) f.(fn_sig).(sig_res) then if tailcall_is_possible sig then OK e2 else Error(msg "tailcall not possible") @@ -323,9 +324,9 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := then OK e1 else Error(msg "jumptable too big") | Ireturn optres => - match optres, f.(fn_sig).(sig_res) with - | None, None => OK e - | Some r, Some t => S.set e r t + match optres, rettype_eq f.(fn_sig).(sig_res) Tvoid with + | None, left _ => OK e + | Some r, right _ => S.set e r (proj_sig_res f.(fn_sig)) | _, _ => Error(msg "bad return") end end. @@ -468,7 +469,7 @@ Proof. destruct l; try discriminate. destruct l; monadInv EQ0. eauto with ty. destruct (type_of_operation o) as [targs tres] eqn:TYOP. monadInv EQ0. eauto with ty. - (* tailcall *) - destruct (opt_typ_eq (sig_res s) (sig_res (fn_sig f))); try discriminate. + destruct (rettype_eq (sig_res s) (sig_res (fn_sig f))); try discriminate. destruct (tailcall_is_possible s) eqn:TCIP; inv EQ2. eauto with ty. - (* builtin *) @@ -477,7 +478,8 @@ Proof. destruct (zle (list_length_z l * 4) Int.max_unsigned); inv EQ2. eauto with ty. - (* return *) - simpl in H. destruct o as [r|] eqn: RET; destruct (sig_res (fn_sig f)) as [t|] eqn: RES; try discriminate. + simpl in H. + destruct o as [r|] eqn: RET; destruct (rettype_eq (sig_res (fn_sig f)) Tvoid); try discriminate. eauto with ty. inv H; auto with ty. Qed. @@ -519,7 +521,7 @@ Proof. eapply S.set_sound; eauto with ty. eauto with ty. - (* tailcall *) - destruct (opt_typ_eq (sig_res s) (sig_res (fn_sig f))); try discriminate. + destruct (rettype_eq (sig_res s) (sig_res (fn_sig f))); try discriminate. destruct (tailcall_is_possible s) eqn:TCIP; inv EQ2. constructor. eapply type_ros_sound; eauto with ty. @@ -543,8 +545,9 @@ Proof. eapply check_successors_sound; eauto. auto. - (* return *) - simpl in H. destruct o as [r|] eqn: RET; destruct (sig_res (fn_sig f)) as [t|] eqn: RES; try discriminate. - econstructor. eauto. eapply S.set_sound; eauto with ty. + simpl in H. + destruct o as [r|] eqn: RET; destruct (rettype_eq (sig_res (fn_sig f)) Tvoid); try discriminate. + econstructor. auto. eapply S.set_sound; eauto with ty. eauto. inv H. constructor. auto. Qed. @@ -721,9 +724,9 @@ Proof. rewrite check_successor_complete by auto; simpl. apply IHtbl0; intros; auto. - (* return none *) - rewrite H0. exists e; auto. + rewrite H0, dec_eq_true. exists e; auto. - (* return some *) - rewrite H0. apply S.set_complete; auto. + rewrite dec_eq_false by auto. apply S.set_complete; auto. Qed. Lemma type_code_complete: @@ -872,7 +875,7 @@ Qed. Inductive wt_stackframes: list stackframe -> signature -> Prop := | wt_stackframes_nil: forall sg, - sg.(sig_res) = Some Tint -> + sg.(sig_res) = Tint -> wt_stackframes nil sg | wt_stackframes_cons: forall s res f sp pc rs env sg, @@ -964,13 +967,13 @@ Proof. econstructor; eauto. (* Ireturn *) econstructor; eauto. - inv WTI; simpl. auto. unfold proj_sig_res; rewrite H2. auto. + inv WTI; simpl. auto. rewrite <- H3. auto. (* internal function *) simpl in *. inv H5. econstructor; eauto. inv H1. apply wt_init_regs; auto. rewrite wt_params0. auto. (* external function *) - econstructor; eauto. simpl. + econstructor; eauto. eapply external_call_well_typed; eauto. (* return *) inv H1. econstructor; eauto. diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp index de954482..694bb0e2 100644 --- a/backend/SplitLong.vp +++ b/backend/SplitLong.vp @@ -43,13 +43,13 @@ Class helper_functions := mk_helper_functions { i64_smulh: ident; (**r signed multiply high *) }. -Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default. -Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default. -Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle) cc_default. -Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong) cc_default. -Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default. -Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default. -Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default. +Definition sig_l_l := mksignature (Tlong :: nil) Tlong cc_default. +Definition sig_l_f := mksignature (Tlong :: nil) Tfloat cc_default. +Definition sig_l_s := mksignature (Tlong :: nil) Tsingle cc_default. +Definition sig_f_l := mksignature (Tfloat :: nil) Tlong cc_default. +Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) Tlong cc_default. +Definition sig_li_l := mksignature (Tlong :: Tint :: nil) Tlong cc_default. +Definition sig_ii_l := mksignature (Tint :: Tint :: nil) Tlong cc_default. Section SELECT. diff --git a/backend/Tailcall.v b/backend/Tailcall.v index 939abeea..b7a62d74 100644 --- a/backend/Tailcall.v +++ b/backend/Tailcall.v @@ -82,7 +82,7 @@ Definition transf_instr (f: function) (pc: node) (instr: instruction) := | Icall sig ros args res s => if is_return niter f s res && tailcall_is_possible sig - && opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res) + && rettype_eq sig.(sig_res) f.(fn_sig).(sig_res) then Itailcall sig ros args else instr | _ => instr diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 06e314f3..9ec89553 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -157,12 +157,10 @@ Lemma transf_instr_charact: transf_instr_spec f instr (transf_instr f pc instr). Proof. intros. unfold transf_instr. destruct instr; try constructor. - caseEq (is_return niter f n r && tailcall_is_possible s && - opt_typ_eq (sig_res s) (sig_res (fn_sig f))); intros. - destruct (andb_prop _ _ H0). destruct (andb_prop _ _ H1). - eapply transf_instr_tailcall; eauto. - eapply is_return_charact; eauto. - constructor. + destruct (is_return niter f n r && tailcall_is_possible s && + rettype_eq (sig_res s) (sig_res (fn_sig f))) eqn:B. +- InvBooleans. eapply transf_instr_tailcall; eauto. eapply is_return_charact; eauto. +- constructor. Qed. Lemma transf_instr_lookup: -- cgit From 3bffda879e214345635e575a696e8f184bef0e55 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 20 Feb 2020 09:41:16 +0100 Subject: Cosmetic: in OCaml code, write "open! Module" instead of "open !Module" "open!" is the form used in the examples in the OCaml manual. Based on a quick poll it seems to be the preferred form of the OCaml core dev team. --- backend/Inliningaux.ml | 2 +- backend/PrintCminor.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'backend') diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml index 842e0c93..2e83eb0c 100644 --- a/backend/Inliningaux.ml +++ b/backend/Inliningaux.ml @@ -16,7 +16,7 @@ open FSetAVL open Maps open Op open Ordered -open !RTL +open! RTL module PSet = Make(OrderedPositive) diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index b77c5645..c9a6d399 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -16,7 +16,7 @@ (** Pretty-printer for Cminor *) open Format -open !Camlcoq +open! Camlcoq open Integers open AST open PrintAST -- cgit