diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-02-18 16:57:17 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-02-21 13:29:39 +0100 |
| commit | be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b (patch) | |
| tree | 0d54cce547d12567d7e9e9f2c4d650e5a1b94b39 | |
| parent | a9eaf4897c825093aba2137ff76e56bfbf1e72d5 (diff) | |
| download | compcert-kvx-be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b.tar.gz compcert-kvx-be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b.zip | |
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.
43 files changed, 445 insertions, 286 deletions
diff --git a/aarch64/Builtins1.v b/aarch64/Builtins1.v index f6e643d2..53c83d7e 100644 --- a/aarch64/Builtins1.v +++ b/aarch64/Builtins1.v @@ -29,5 +29,5 @@ Definition platform_builtin_table : list (string * platform_builtin) := Definition platform_builtin_sig (b: platform_builtin) : signature := match b with end. -Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := match b with end. diff --git a/aarch64/Conventions1.v b/aarch64/Conventions1.v index 5914e8f2..575d058d 100644 --- a/aarch64/Conventions1.v +++ b/aarch64/Conventions1.v @@ -102,10 +102,9 @@ Definition is_float_reg (r: mreg): bool := with one integer result. *) Definition loc_result (s: signature) : rpair mreg := - match s.(sig_res) with - | None => One R0 - | Some (Tint | Tlong | Tany32 | Tany64) => One R0 - | Some (Tfloat | Tsingle) => One F0 + match proj_sig_res s with + | Tint | Tlong | Tany32 | Tany64 => One R0 + | Tfloat | Tsingle => One F0 end. (** The result registers have types compatible with that given in the signature. *) @@ -114,7 +113,7 @@ Lemma loc_result_type: forall sig, subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. - intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; auto. + intros. unfold loc_result. destruct (proj_sig_res sig); auto. Qed. (** The result locations are caller-save registers *) @@ -124,7 +123,7 @@ Lemma loc_result_caller_save: forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. intros. - unfold loc_result. destruct (sig_res s) as [[]|]; simpl; auto. + unfold loc_result. destruct (proj_sig_res s); simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -134,12 +133,12 @@ Lemma loc_result_pair: match loc_result sg with | One _ => True | Twolong r1 r2 => - r1 <> r2 /\ sg.(sig_res) = Some Tlong + r1 <> r2 /\ proj_sig_res sg = Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.ptr64 = false end. Proof. - intros; unfold loc_result; destruct (sig_res sg) as [[]|]; exact I. + intros; unfold loc_result; destruct (proj_sig_res sg); exact I. Qed. (** The location of the result depends only on the result part of the signature *) @@ -147,7 +146,7 @@ Qed. Lemma loc_result_exten: forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2. Proof. - intros. unfold loc_result. rewrite H; auto. + intros. unfold loc_result, proj_sig_res. rewrite H; auto. Qed. (** ** Location of function arguments *) diff --git a/arm/Builtins1.v b/arm/Builtins1.v index f6e643d2..53c83d7e 100644 --- a/arm/Builtins1.v +++ b/arm/Builtins1.v @@ -29,5 +29,5 @@ Definition platform_builtin_table : list (string * platform_builtin) := Definition platform_builtin_sig (b: platform_builtin) : signature := match b with end. -Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := match b with end. diff --git a/arm/Conventions1.v b/arm/Conventions1.v index c5277e8d..45008bff 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -104,13 +104,12 @@ Definition is_float_reg (r: mreg): bool := representation with a single LDM instruction. *) Definition loc_result (s: signature) : rpair mreg := - match s.(sig_res) with - | None => One R0 - | Some (Tint | Tany32) => One R0 - | Some (Tfloat | Tsingle | Tany64) => One F0 - | Some Tlong => if Archi.big_endian - then Twolong R0 R1 - else Twolong R1 R0 + match proj_sig_res s with + | Tint | Tany32 => One R0 + | Tfloat | Tsingle | Tany64 => One F0 + | Tlong => if Archi.big_endian + then Twolong R0 R1 + else Twolong R1 R0 end. (** The result registers have types compatible with that given in the signature. *) @@ -119,7 +118,7 @@ Lemma loc_result_type: forall sig, subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. - intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; destruct Archi.big_endian; auto. + intros. unfold loc_result. destruct (proj_sig_res sig); destruct Archi.big_endian; auto. Qed. (** The result locations are caller-save registers *) @@ -129,7 +128,7 @@ Lemma loc_result_caller_save: forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. intros. - unfold loc_result. destruct (sig_res s) as [[]|]; destruct Archi.big_endian; simpl; auto. + unfold loc_result. destruct (proj_sig_res s); destruct Archi.big_endian; simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -139,14 +138,13 @@ Lemma loc_result_pair: match loc_result sg with | One _ => True | Twolong r1 r2 => - r1 <> r2 /\ sg.(sig_res) = Some Tlong + r1 <> r2 /\ proj_sig_res sg = Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.ptr64 = false end. Proof. - intros; unfold loc_result; destruct (sig_res sg) as [[]|]; destruct Archi.big_endian; auto. - intuition congruence. - intuition congruence. + intros; unfold loc_result; destruct (proj_sig_res sg); auto. + destruct Archi.big_endian; intuition congruence. Qed. (** The location of the result depends only on the result part of the signature *) @@ -154,7 +152,7 @@ Qed. Lemma loc_result_exten: forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2. Proof. - intros. unfold loc_result. rewrite H; auto. + intros. unfold loc_result, proj_sig_res. rewrite H; auto. Qed. (** ** Location of function arguments *) 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: diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index a76a14ba..6d2b470f 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -444,7 +444,7 @@ Lemma red_selection: Proof. intros. unfold Eselection. set (t := typ_of_type ty). - set (sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default). + set (sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default). assert (LK: lookup_builtin_function "__builtin_sel"%string sg = Some (BI_standard (BI_select t))). { unfold sg, t; destruct ty as [ | ? ? ? | ? | [] ? | ? ? | ? ? ? | ? ? ? | ? ? | ? ? ]; simpl; unfold Tptr; destruct Archi.ptr64; reflexivity. } diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 792a73f9..ee135dcd 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -602,7 +602,7 @@ Fixpoint transl_statement (ce: composite_env) (tyret: type) (nbrk ncnt: nat) do tb <- transl_expr ce b; do tcl <- transl_arglist ce cl args; OK(Scall x {| sig_args := typlist_of_arglist cl args; - sig_res := opttyp_of_type res; + sig_res := rettype_of_type res; sig_cc := cconv |} tb tcl) | _ => Error(msg "Cshmgen.transl_stmt(call)") @@ -667,7 +667,7 @@ Definition transl_var (ce: composite_env) (v: ident * type) := Definition signature_of_function (f: Clight.function) := {| sig_args := map typ_of_type (map snd (Clight.fn_params f)); - sig_res := opttyp_of_type (Clight.fn_return f); + sig_res := rettype_of_type (Clight.fn_return f); sig_cc := Clight.fn_callconv f |}. Definition transl_function (ce: composite_env) (f: Clight.function) : res function := diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index c34a5e13..e3e2c1e9 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -106,7 +106,7 @@ Definition Epreincr (id: incr_or_decr) (l: expr) (ty: type) := Definition Eselection (r1 r2 r3: expr) (ty: type) := let t := typ_of_type ty in - let sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default in + let sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default in Ebuiltin (EF_builtin "__builtin_sel"%string sg) (Tcons type_bool (Tcons ty (Tcons ty Tnil))) (Econs r1 (Econs r2 (Econs r3 Enil))) diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index bfc5daa9..664a60c5 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -732,8 +732,21 @@ Definition typ_of_type (t: type) : AST.typ := | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ | Tstruct _ _ | Tunion _ _ => AST.Tptr end. -Definition opttyp_of_type (t: type) : option AST.typ := - if type_eq t Tvoid then None else Some (typ_of_type t). +Definition rettype_of_type (t: type) : AST.rettype := + match t with + | Tvoid => AST.Tvoid + | Tint I32 _ _ => AST.Tint + | Tint I8 Signed _ => AST.Tint8signed + | Tint I8 Unsigned _ => AST.Tint8unsigned + | Tint I16 Signed _ => AST.Tint16signed + | Tint I16 Unsigned _ => AST.Tint16unsigned + | Tint IBool _ _ => AST.Tint8unsigned + | Tlong _ _ => AST.Tlong + | Tfloat F32 _ => AST.Tsingle + | Tfloat F64 _ => AST.Tfloat + | Tpointer _ _ => AST.Tptr + | Tarray _ _ _ | Tfunction _ _ _ | Tstruct _ _ | Tunion _ _ => AST.Tvoid + end. Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := match tl with @@ -742,7 +755,7 @@ Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := end. Definition signature_of_type (args: typelist) (res: type) (cc: calling_convention): signature := - mksignature (typlist_of_typelist args) (opttyp_of_type res) cc. + mksignature (typlist_of_typelist args) (rettype_of_type res) cc. (** * Construction of the composite environment *) diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 29ea3bf2..00fcf8ab 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -397,10 +397,10 @@ Inductive wt_rvalue : expr -> Prop := wt_arguments rargs tyargs -> (* This typing rule is specialized to the builtin invocations generated by C2C, which are either __builtin_sel or builtins returning void. *) - (ty = Tvoid /\ sig_res (ef_sig ef) = None) + (ty = Tvoid /\ sig_res (ef_sig ef) = AST.Tvoid) \/ (tyargs = Tcons type_bool (Tcons ty (Tcons ty Tnil)) /\ let t := typ_of_type ty in - let sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default in + let sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default in ef = EF_builtin "__builtin_sel"%string sg) -> wt_rvalue (Ebuiltin ef tyargs rargs ty) | wt_Eparen: forall r tycast ty, @@ -521,11 +521,20 @@ Fixpoint bind_globdef (e: typenv) (l: list (ident * globdef fundef type)) : type | (id, Gvar v) :: l => bind_globdef (PTree.set id v.(gvar_info) e) l end. +Inductive wt_fundef (ce: composite_env) (e: typenv) : fundef -> Prop := + | wt_fundef_internal: forall f, + wt_function ce e f -> + wt_fundef ce e (Internal f) + | wt_fundef_external: forall ef targs tres cc, + (ef_sig ef).(sig_res) = rettype_of_type tres -> + wt_fundef ce e (External ef targs tres cc). + Inductive wt_program : program -> Prop := | wt_program_intro: forall p, let e := bind_globdef (PTree.empty _) p.(prog_defs) in - (forall id f, In (id, Gfun (Internal f)) p.(prog_defs) -> - wt_function p.(prog_comp_env) e f) -> + (forall id fd, + In (id, Gfun fd) p.(prog_defs) -> + wt_fundef p.(prog_comp_env) e fd) -> wt_program p. Hint Constructors wt_val wt_rvalue wt_lvalue wt_stmt wt_lblstmts: ty. @@ -745,7 +754,7 @@ Definition ebuiltin (ef: external_function) (tyargs: typelist) (args: exprlist) do x1 <- check_rvals args; do x2 <- check_arguments args tyargs; if type_eq tyres Tvoid - && opt_typ_eq (sig_res (ef_sig ef)) None + && AST.rettype_eq (sig_res (ef_sig ef)) AST.Tvoid then OK (Ebuiltin ef tyargs args tyres) else Error (msg "builtin: wrong type decoration"). @@ -915,7 +924,8 @@ Definition retype_function (ce: composite_env) (e: typenv) (f: function) : res f Definition retype_fundef (ce: composite_env) (e: typenv) (fd: fundef) : res fundef := match fd with | Internal f => do f' <- retype_function ce e f; OK (Internal f') - | External id args res cc => OK fd + | External ef args res cc => + assertion (rettype_eq (ef_sig ef).(sig_res) (rettype_of_type res)); OK fd end. Definition typecheck_program (p: program) : res program := @@ -1241,7 +1251,7 @@ Lemma ebuiltin_sound: Proof. intros. monadInv H. destruct (type_eq tyres Tvoid); simpl in EQ2; try discriminate. - destruct (opt_typ_eq (sig_res (ef_sig ef)) None); inv EQ2. + destruct (rettype_eq (sig_res (ef_sig ef)) AST.Tvoid); inv EQ2. econstructor; eauto. eapply check_arguments_sound; eauto. Qed. @@ -1373,6 +1383,14 @@ Proof. intros. monadInv H. constructor; simpl. eapply retype_stmt_sound; eauto. Qed. +Lemma retype_fundef_sound: + forall ce e fd fd', retype_fundef ce e fd = OK fd' -> wt_fundef ce e fd'. +Proof. + intros. destruct fd; monadInv H. +- constructor; eapply retype_function_sound; eauto. +- constructor; auto. +Qed. + Theorem typecheck_program_sound: forall p p', typecheck_program p = OK p' -> wt_program p'. Proof. @@ -1395,11 +1413,11 @@ Proof. inv H1. simpl. auto. } rewrite ENVS. - intros id f. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp). + intros id fd. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp). induction 1; simpl; intros. contradiction. destruct H0; auto. subst b1; inv H. simpl in H1. inv H1. - destruct f1; monadInv H4. eapply retype_function_sound; eauto. + eapply retype_fundef_sound; eauto. Qed. (** * Subject reduction *) @@ -1711,6 +1729,26 @@ Proof. inv H; auto. Qed. +Lemma has_rettype_wt_val: + forall v ty, + Val.has_rettype v (rettype_of_type ty) -> wt_val v ty. +Proof. + unfold rettype_of_type, Val.has_rettype, Val.has_type; destruct ty; intros. +- destruct v; contradiction || constructor. +- destruct i. + + destruct s; destruct v; try contradiction; constructor; red; auto. + + destruct s; destruct v; try contradiction; constructor; red; auto. + + destruct v; try contradiction; constructor; auto. + + destruct v; try contradiction; constructor; red; auto. +- destruct v; try contradiction; constructor; auto. +- destruct f; destruct v; try contradiction; constructor. +- unfold Tptr in *; destruct v; destruct Archi.ptr64 eqn:P64; try contradiction; constructor; auto. +- destruct v; contradiction || constructor. +- destruct v; contradiction || constructor. +- destruct v; contradiction || constructor. +- destruct v; contradiction || constructor. +Qed. + Lemma wt_rred: forall ge tenv a m t a' m', rred ge a m t a' m' -> wt_rvalue ge tenv a -> wt_rvalue ge tenv a'. @@ -1750,7 +1788,7 @@ Proof. - (* builtin *) subst. destruct H7 as [(A & B) | (A & B)]. + subst ty. auto with ty. + simpl in B. set (T := typ_of_type ty) in *. - set (sg := mksignature (AST.Tint :: T :: T :: nil) (Some T) cc_default) in *. + set (sg := mksignature (AST.Tint :: T :: T :: nil) T cc_default) in *. assert (LK: lookup_builtin_function "__builtin_sel"%string sg = Some (BI_standard (BI_select T))). { unfold sg, T; destruct ty as [ | ? ? ? | ? | [] ? | ? ? | ? ? ? | ? ? ? | ? ? | ? ? ]; simpl; unfold Tptr; destruct Archi.ptr64; reflexivity. } @@ -1896,12 +1934,6 @@ Hypothesis WTPROG: wt_program prog. Let ge := globalenv prog. Let gtenv := bind_globdef (PTree.empty _) prog.(prog_defs). -Hypothesis WT_EXTERNAL: - forall id ef args res cc vargs m t vres m', - In (id, Gfun (External ef args res cc)) prog.(prog_defs) -> - external_call ef ge vargs m t vres m' -> - wt_val vres res. - Inductive wt_expr_cont: typenv -> function -> cont -> Prop := | wt_Kdo: forall te f k, wt_stmt_cont te f k -> @@ -2000,12 +2032,6 @@ Proof. induction 1; simpl; auto; econstructor; eauto. Qed. -Definition wt_fundef (fd: fundef) := - match fd with - | Internal f => wt_function ge gtenv f - | External ef targs tres cc => True - end. - Definition fundef_return (fd: fundef) : type := match fd with | Internal f => f.(fn_return) @@ -2013,10 +2039,10 @@ Definition fundef_return (fd: fundef) : type := end. Lemma wt_find_funct: - forall v fd, Genv.find_funct ge v = Some fd -> wt_fundef fd. + forall v fd, Genv.find_funct ge v = Some fd -> wt_fundef ge gtenv fd. Proof. intros. apply Genv.find_funct_prop with (p := prog) (v := v); auto. - intros. inv WTPROG. destruct f; simpl; auto. apply H1 with id; auto. + intros. inv WTPROG. apply H1 with id; auto. Qed. Inductive wt_state: state -> Prop := @@ -2032,7 +2058,7 @@ Inductive wt_state: state -> Prop := wt_state (ExprState f r k e m) | wt_call_state: forall b fd vargs k m (WTK: wt_call_cont k (fundef_return fd)) - (WTFD: wt_fundef fd) + (WTFD: wt_fundef ge gtenv fd) (FIND: Genv.find_funct ge b = Some fd), wt_state (Callstate fd vargs k m) | wt_return_state: forall v k m ty @@ -2089,7 +2115,6 @@ Qed. End WT_FIND_LABEL. - Lemma preservation_estep: forall S t S', estep ge S t S' -> wt_state S -> wt_state S'. Proof. @@ -2164,9 +2189,10 @@ Proof. - inv WTS; eauto with ty. - exploit wt_find_label. eexact WTB. eauto. eapply call_cont_wt'; eauto. intros [A B]. eauto with ty. -- simpl in WTFD; inv WTFD. econstructor; eauto. apply wt_call_cont_stmt_cont; auto. -- exploit (Genv.find_funct_inversion prog); eauto. intros (id & A). - econstructor; eauto. +- inv WTFD. inv H3. econstructor; eauto. apply wt_call_cont_stmt_cont; auto. +- inv WTFD. econstructor; eauto. + apply has_rettype_wt_val. simpl; rewrite <- H1. + eapply external_call_well_typed_gen; eauto. - inv WTK. eauto with ty. Qed. @@ -2181,7 +2207,7 @@ Theorem wt_initial_state: Proof. intros. inv H. econstructor. constructor. apply Genv.find_funct_ptr_prop with (p := prog) (b := b); auto. - intros. inv WTPROG. destruct f0; simpl; auto. apply H4 with id; auto. + intros. inv WTPROG. apply H4 with id; auto. instantiate (1 := (Vptr b Ptrofs.zero)). rewrite Genv.find_funct_find_funct_ptr. auto. Qed. diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 1c9729c5..03dc5837 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -19,7 +19,7 @@ open Format open Camlcoq open Values open AST -open Ctypes +open! Ctypes open Cop open Csyntax @@ -85,7 +85,7 @@ let name_optid id = let rec name_cdecl id ty = match ty with - | Tvoid -> + | Ctypes.Tvoid -> "void" ^ name_optid id | Ctypes.Tint(sz, sg, a) -> name_inttype sz sg ^ attributes a ^ name_optid id diff --git a/common/AST.v b/common/AST.v index a91138c9..fcbf0b34 100644 --- a/common/AST.v +++ b/common/AST.v @@ -45,9 +45,6 @@ Lemma typ_eq: forall (t1 t2: typ), {t1=t2} + {t1<>t2}. Proof. decide equality. Defined. Global Opaque typ_eq. -Definition opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2} - := option_eq typ_eq. - Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2} := list_eq_dec typ_eq. @@ -91,10 +88,34 @@ Fixpoint subtype_list (tyl1 tyl2: list typ) : bool := | _, _ => false end. +(** To describe the values returned by functions, we use the more precise + types below. *) + +Inductive rettype : Type := + | Tret (t: typ) (**r like type [t] *) + | Tint8signed (**r 8-bit signed integer *) + | Tint8unsigned (**r 8-bit unsigned integer *) + | Tint16signed (**r 16-bit signed integer *) + | Tint16unsigned (**r 16-bit unsigned integer *) + | Tvoid. (**r no value returned *) + +Coercion Tret: typ >-> rettype. + +Lemma rettype_eq: forall (t1 t2: rettype), {t1=t2} + {t1<>t2}. +Proof. generalize typ_eq; decide equality. Defined. +Global Opaque rettype_eq. + +Fixpoint proj_rettype (r: rettype) : typ := + match r with + | Tret t => t + | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => Tint + | Tvoid => Tint + end. + (** Additionally, function definitions and function calls are annotated by function signatures indicating: - the number and types of arguments; -- the type of the returned value, if any; +- the type of the returned value; - additional information on which calling convention to use. These signatures are used in particular to determine appropriate @@ -117,24 +138,20 @@ Global Opaque calling_convention_eq. Record signature : Type := mksignature { sig_args: list typ; - sig_res: option typ; + sig_res: rettype; sig_cc: calling_convention }. -Definition proj_sig_res (s: signature) : typ := - match s.(sig_res) with - | None => Tint - | Some t => t - end. +Definition proj_sig_res (s: signature) : typ := proj_rettype s.(sig_res). Definition signature_eq: forall (s1 s2: signature), {s1=s2} + {s1<>s2}. Proof. - generalize opt_typ_eq, list_typ_eq, calling_convention_eq; decide equality. + generalize rettype_eq, list_typ_eq, calling_convention_eq; decide equality. Defined. Global Opaque signature_eq. Definition signature_main := - {| sig_args := nil; sig_res := Some Tint; sig_cc := cc_default |}. + {| sig_args := nil; sig_res := Tint; sig_cc := cc_default |}. (** Memory accesses (load and store instructions) are annotated by a ``memory chunk'' indicating the type, size and signedness of the @@ -177,6 +194,28 @@ Definition type_of_chunk (c: memory_chunk) : typ := Lemma type_of_Mptr: type_of_chunk Mptr = Tptr. Proof. unfold Mptr, Tptr; destruct Archi.ptr64; auto. Qed. +(** Same, as a return type. *) + +Definition rettype_of_chunk (c: memory_chunk) : rettype := + match c with + | Mint8signed => Tint8signed + | Mint8unsigned => Tint8unsigned + | Mint16signed => Tint16signed + | Mint16unsigned => Tint16unsigned + | Mint32 => Tint + | Mint64 => Tlong + | Mfloat32 => Tsingle + | Mfloat64 => Tfloat + | Many32 => Tany32 + | Many64 => Tany64 + end. + +Lemma proj_rettype_of_chunk: + forall chunk, proj_rettype (rettype_of_chunk chunk) = type_of_chunk chunk. +Proof. + destruct chunk; auto. +Qed. + (** The chunk that is appropriate to store and reload a value of the given type, without losing information. *) @@ -477,15 +516,15 @@ Definition ef_sig (ef: external_function): signature := | EF_external name sg => sg | EF_builtin name sg => sg | EF_runtime name sg => sg - | EF_vload chunk => mksignature (Tptr :: nil) (Some (type_of_chunk chunk)) cc_default - | EF_vstore chunk => mksignature (Tptr :: type_of_chunk chunk :: nil) None cc_default - | EF_malloc => mksignature (Tptr :: nil) (Some Tptr) cc_default - | EF_free => mksignature (Tptr :: nil) None cc_default - | EF_memcpy sz al => mksignature (Tptr :: Tptr :: nil) None cc_default - | EF_annot kind text targs => mksignature targs None cc_default - | EF_annot_val kind text targ => mksignature (targ :: nil) (Some targ) cc_default + | EF_vload chunk => mksignature (Tptr :: nil) (rettype_of_chunk chunk) cc_default + | EF_vstore chunk => mksignature (Tptr :: type_of_chunk chunk :: nil) Tvoid cc_default + | EF_malloc => mksignature (Tptr :: nil) Tptr cc_default + | EF_free => mksignature (Tptr :: nil) Tvoid cc_default + | EF_memcpy sz al => mksignature (Tptr :: Tptr :: nil) Tvoid cc_default + | EF_annot kind text targs => mksignature targs Tvoid cc_default + | EF_annot_val kind text targ => mksignature (targ :: nil) targ cc_default | EF_inline_asm text sg clob => sg - | EF_debug kind text targs => mksignature targs None cc_default + | EF_debug kind text targs => mksignature targs Tvoid cc_default end. (** Whether an external function should be inlined by the compiler. *) diff --git a/common/Builtins.v b/common/Builtins.v index c9097e86..476b541e 100644 --- a/common/Builtins.v +++ b/common/Builtins.v @@ -29,7 +29,7 @@ Definition builtin_function_sig (b: builtin_function) : signature := | BI_platform b => platform_builtin_sig b end. -Definition builtin_function_sem (b: builtin_function) : builtin_sem (proj_sig_res (builtin_function_sig b)) := +Definition builtin_function_sem (b: builtin_function) : builtin_sem (sig_res (builtin_function_sig b)) := match b with | BI_standard b => standard_builtin_sem b | BI_platform b => platform_builtin_sem b diff --git a/common/Builtins0.v b/common/Builtins0.v index b78006dd..8da98314 100644 --- a/common/Builtins0.v +++ b/common/Builtins0.v @@ -26,8 +26,8 @@ Require Import AST Integers Floats Values Memdata. appropriate for the target. *) -Definition val_opt_has_type (ov: option val) (t: typ) : Prop := - match ov with Some v => Val.has_type v t | None => True end. +Definition val_opt_has_rettype (ov: option val) (t: rettype) : Prop := + match ov with Some v => Val.has_rettype v t | None => True end. Definition val_opt_inject (j: meminj) (ov ov': option val) : Prop := match ov, ov' with @@ -42,10 +42,10 @@ Definition val_opt_inject (j: meminj) (ov ov': option val) : Prop := and be compatible with value injections. *) -Record builtin_sem (tret: typ) : Type := mkbuiltin { +Record builtin_sem (tret: rettype) : Type := mkbuiltin { bs_sem :> list val -> option val; bs_well_typed: forall vl, - val_opt_has_type (bs_sem vl) tret; + val_opt_has_rettype (bs_sem vl) tret; bs_inject: forall j vl vl', Val.inject_list j vl vl' -> val_opt_inject j (bs_sem vl) (bs_sem vl') }. @@ -60,8 +60,8 @@ Record builtin_sem (tret: typ) : Type := mkbuiltin { Local Unset Program Cases. Program Definition mkbuiltin_v1t - (tret: typ) (f: val -> val) - (WT: forall v1, Val.has_type (f v1) tret) + (tret: rettype) (f: val -> val) + (WT: forall v1, Val.has_rettype (f v1) tret) (INJ: forall j v1 v1', Val.inject j v1 v1' -> Val.inject j (f v1) (f v1')) := mkbuiltin tret (fun vl => match vl with v1 :: nil => Some (f v1) | _ => None end) _ _. Next Obligation. @@ -72,8 +72,8 @@ Next Obligation. Qed. Program Definition mkbuiltin_v2t - (tret: typ) (f: val -> val -> val) - (WT: forall v1 v2, Val.has_type (f v1 v2) tret) + (tret: rettype) (f: val -> val -> val) + (WT: forall v1 v2, Val.has_rettype (f v1 v2) tret) (INJ: forall j v1 v1' v2 v2', Val.inject j v1 v1' -> Val.inject j v2 v2' -> Val.inject j (f v1 v2) (f v1' v2')) := @@ -86,8 +86,8 @@ Next Obligation. Qed. Program Definition mkbuiltin_v3t - (tret: typ) (f: val -> val -> val -> val) - (WT: forall v1 v2 v3, Val.has_type (f v1 v2 v3) tret) + (tret: rettype) (f: val -> val -> val -> val) + (WT: forall v1 v2 v3, Val.has_rettype (f v1 v2 v3) tret) (INJ: forall j v1 v1' v2 v2' v3 v3', Val.inject j v1 v1' -> Val.inject j v2 v2' -> Val.inject j v3 v3' -> Val.inject j (f v1 v2 v3) (f v1' v2' v3')) := @@ -100,8 +100,8 @@ Next Obligation. Qed. Program Definition mkbuiltin_v1p - (tret: typ) (f: val -> option val) - (WT: forall v1, val_opt_has_type (f v1) tret) + (tret: rettype) (f: val -> option val) + (WT: forall v1, val_opt_has_rettype (f v1) tret) (INJ: forall j v1 v1', Val.inject j v1 v1' -> val_opt_inject j (f v1) (f v1')) := mkbuiltin tret (fun vl => match vl with v1 :: nil => f v1 | _ => None end) _ _. @@ -113,8 +113,8 @@ Next Obligation. Qed. Program Definition mkbuiltin_v2p - (tret: typ) (f: val -> val -> option val) - (WT: forall v1 v2, val_opt_has_type (f v1 v2) tret) + (tret: rettype) (f: val -> val -> option val) + (WT: forall v1 v2, val_opt_has_rettype (f v1 v2) tret) (INJ: forall j v1 v1' v2 v2', Val.inject j v1 v1' -> Val.inject j v2 v2' -> val_opt_inject j (f v1 v2) (f v1' v2')) := @@ -171,7 +171,7 @@ Proof. destruct t; intros; constructor. Qed. -Lemma inj_num_opt_wt: forall t x, val_opt_has_type (option_map (inj_num t) x) t. +Lemma inj_num_opt_wt: forall t x, val_opt_has_rettype (option_map (inj_num t) x) t. Proof. intros. destruct x; simpl. apply inj_num_wt. auto. Qed. @@ -200,13 +200,13 @@ Proof. Qed. Lemma proj_num_opt_wt: - forall tres t k0 k1 v, + forall (tres: typ) t k0 k1 v, k0 = None \/ k0 = Some Vundef -> - (forall x, val_opt_has_type (k1 x) tres) -> - val_opt_has_type (proj_num t k0 v k1) tres. + (forall x, val_opt_has_rettype (k1 x) tres) -> + val_opt_has_rettype (proj_num t k0 v k1) tres. Proof. intros. - assert (val_opt_has_type k0 tres). { destruct H; subst k0; exact I. } + assert (val_opt_has_rettype k0 tres). { destruct H; subst k0; exact I. } destruct t; simpl; destruct v; auto. Qed. @@ -393,33 +393,33 @@ Definition standard_builtin_table : list (string * standard_builtin) := Definition standard_builtin_sig (b: standard_builtin) : signature := match b with | BI_select t => - mksignature (Tint :: t :: t :: nil) (Some t) cc_default + mksignature (Tint :: t :: t :: nil) t cc_default | BI_fabs | BI_fsqrt => - mksignature (Tfloat :: nil) (Some Tfloat) cc_default + mksignature (Tfloat :: nil) Tfloat cc_default | BI_negl => - mksignature (Tlong :: nil) (Some Tlong) cc_default + mksignature (Tlong :: nil) Tlong cc_default | BI_addl | BI_subl | BI_i64_umulh| BI_i64_smulh | BI_i64_sdiv | BI_i64_udiv | BI_i64_smod | BI_i64_umod => - mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default + mksignature (Tlong :: Tlong :: nil) Tlong cc_default | BI_mull => - mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default + mksignature (Tint :: Tint :: nil) Tlong cc_default | BI_i32_bswap => - mksignature (Tint :: nil) (Some Tint) cc_default + mksignature (Tint :: nil) Tint cc_default | BI_i64_bswap => - mksignature (Tlong :: nil) (Some Tlong) cc_default + mksignature (Tlong :: nil) Tlong cc_default | BI_i16_bswap => - mksignature (Tint :: nil) (Some Tint) cc_default + mksignature (Tint :: nil) Tint cc_default | BI_i64_shl | BI_i64_shr | BI_i64_sar => - mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default + mksignature (Tlong :: Tint :: nil) Tlong cc_default | BI_i64_dtos | BI_i64_dtou => - mksignature (Tfloat :: nil) (Some Tlong) cc_default + mksignature (Tfloat :: nil) Tlong cc_default | BI_i64_stod | BI_i64_utod => - mksignature (Tlong :: nil) (Some Tfloat) cc_default + mksignature (Tlong :: nil) Tfloat cc_default | BI_i64_stof | BI_i64_utof => - mksignature (Tlong :: nil) (Some Tsingle) cc_default + mksignature (Tlong :: nil) Tsingle cc_default end. -Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (proj_sig_res (standard_builtin_sig b)) := +Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (sig_res (standard_builtin_sig b)) := match b with | BI_select t => mkbuiltin t diff --git a/common/Events.v b/common/Events.v index 3fb84f49..10e0c232 100644 --- a/common/Events.v +++ b/common/Events.v @@ -623,7 +623,7 @@ Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop := ec_well_typed: forall ge vargs m1 t vres m2, sem ge vargs m1 t vres m2 -> - Val.has_type vres (proj_sig_res sg); + Val.has_rettype vres sg.(sig_res); (** The semantics is invariant under change of global environment that preserves symbols. *) ec_symbols_preserved: @@ -771,12 +771,12 @@ Qed. Lemma volatile_load_ok: forall chunk, extcall_properties (volatile_load_sem chunk) - (mksignature (Tptr :: nil) (Some (type_of_chunk chunk)) cc_default). + (mksignature (Tptr :: nil) (rettype_of_chunk chunk) cc_default). Proof. intros; constructor; intros. (* well typed *) -- unfold proj_sig_res; simpl. inv H. inv H0. apply Val.load_result_type. - eapply Mem.load_type; eauto. +- inv H. inv H0. apply Val.load_result_rettype. + eapply Mem.load_rettype; eauto. (* symbols *) - inv H0. constructor. eapply volatile_load_preserved; eauto. (* valid blocks *) @@ -922,7 +922,7 @@ Qed. Lemma volatile_store_ok: forall chunk, extcall_properties (volatile_store_sem chunk) - (mksignature (Tptr :: type_of_chunk chunk :: nil) None cc_default). + (mksignature (Tptr :: type_of_chunk chunk :: nil) Tvoid cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -967,7 +967,7 @@ Inductive extcall_malloc_sem (ge: Senv.t): Lemma extcall_malloc_ok: extcall_properties extcall_malloc_sem - (mksignature (Tptr :: nil) (Some Tptr) cc_default). + (mksignature (Tptr :: nil) Tptr cc_default). Proof. assert (UNCHANGED: forall (P: block -> Z -> Prop) m lo hi v m' b m'', @@ -984,7 +984,7 @@ Proof. } constructor; intros. (* well typed *) -- inv H. unfold proj_sig_res, Tptr; simpl. destruct Archi.ptr64; auto. +- inv H. simpl. unfold Tptr; destruct Archi.ptr64; auto. (* symbols preserved *) - inv H0; econstructor; eauto. (* valid block *) @@ -1053,11 +1053,11 @@ Inductive extcall_free_sem (ge: Senv.t): Lemma extcall_free_ok: extcall_properties extcall_free_sem - (mksignature (Tptr :: nil) None cc_default). + (mksignature (Tptr :: nil) Tvoid cc_default). Proof. constructor; intros. (* well typed *) -- inv H. unfold proj_sig_res. simpl. auto. +- inv H. simpl. auto. (* symbols preserved *) - inv H0; econstructor; eauto. (* valid block *) @@ -1147,11 +1147,11 @@ Inductive extcall_memcpy_sem (sz al: Z) (ge: Senv.t): Lemma extcall_memcpy_ok: forall sz al, extcall_properties (extcall_memcpy_sem sz al) - (mksignature (Tptr :: Tptr :: nil) None cc_default). + (mksignature (Tptr :: Tptr :: nil) Tvoid cc_default). Proof. intros. constructor. - (* return type *) - intros. inv H. constructor. + intros. inv H. exact I. - (* change of globalenv *) intros. inv H0. econstructor; eauto. - (* valid blocks *) @@ -1258,7 +1258,7 @@ Inductive extcall_annot_sem (text: string) (targs: list typ) (ge: Senv.t): Lemma extcall_annot_ok: forall text targs, extcall_properties (extcall_annot_sem text targs) - (mksignature targs None cc_default). + (mksignature targs Tvoid cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1303,11 +1303,11 @@ Inductive extcall_annot_val_sem (text: string) (targ: typ) (ge: Senv.t): Lemma extcall_annot_val_ok: forall text targ, extcall_properties (extcall_annot_val_sem text targ) - (mksignature (targ :: nil) (Some targ) cc_default). + (mksignature (targ :: nil) targ cc_default). Proof. intros; constructor; intros. (* well typed *) -- inv H. unfold proj_sig_res; simpl. eapply eventval_match_type; eauto. +- inv H. eapply eventval_match_type; eauto. (* symbols *) - destruct H as (A & B & C). inv H0. econstructor; eauto. eapply eventval_match_preserved; eauto. @@ -1347,7 +1347,7 @@ Inductive extcall_debug_sem (ge: Senv.t): Lemma extcall_debug_ok: forall targs, extcall_properties extcall_debug_sem - (mksignature targs None cc_default). + (mksignature targs Tvoid cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1396,7 +1396,8 @@ Proof. intros. set (bsem := builtin_function_sem bf). constructor; intros. (* well typed *) - inv H. - specialize (bs_well_typed _ bsem vargs). unfold val_opt_has_type, bsem; rewrite H0. + specialize (bs_well_typed _ bsem vargs). + unfold val_opt_has_rettype, bsem; rewrite H0. auto. (* symbols *) - inv H0. econstructor; eauto. @@ -1516,7 +1517,7 @@ Proof. apply extcall_debug_ok. Qed. -Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef). +Definition external_call_well_typed_gen ef := ec_well_typed (external_call_spec ef). Definition external_call_symbols_preserved 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). @@ -1527,6 +1528,16 @@ Definition external_call_trace_length ef := ec_trace_length (external_call_spec Definition external_call_receptive ef := ec_receptive (external_call_spec ef). Definition external_call_determ ef := ec_determ (external_call_spec ef). +(** Corollary of [external_call_well_typed_gen]. *) + +Lemma external_call_well_typed: + forall ef ge vargs m1 t vres m2, + external_call ef ge vargs m1 t vres m2 -> + Val.has_type vres (proj_sig_res (ef_sig ef)). +Proof. + intros. apply Val.has_proj_rettype. eapply external_call_well_typed_gen; eauto. +Qed. + (** Corollary of [external_call_valid_block]. *) Lemma external_call_nextblock: diff --git a/common/Memdata.v b/common/Memdata.v index 7144d72c..f3016efe 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -547,18 +547,26 @@ Proof. destruct v1; auto. Qed. -Lemma decode_val_type: +Lemma decode_val_rettype: forall chunk cl, - Val.has_type (decode_val chunk cl) (type_of_chunk chunk). + Val.has_rettype (decode_val chunk cl) (rettype_of_chunk chunk). Proof. intros. unfold decode_val. destruct (proj_bytes cl). - destruct chunk; simpl; auto. -Local Opaque Val.load_result. +- destruct chunk; simpl; rewrite ? Int.sign_ext_idem, ? Int.zero_ext_idem by omega; auto. +- Local Opaque Val.load_result. destruct chunk; simpl; (exact I || apply Val.load_result_type || destruct Archi.ptr64; (exact I || apply Val.load_result_type)). Qed. +Lemma decode_val_type: + forall chunk cl, + Val.has_type (decode_val chunk cl) (type_of_chunk chunk). +Proof. + intros. rewrite <- proj_rettype_of_chunk. + apply Val.has_proj_rettype. apply decode_val_rettype. +Qed. + Lemma encode_val_int8_signed_unsigned: forall v, encode_val Mint8signed v = encode_val Mint8unsigned v. Proof. @@ -607,11 +615,9 @@ Lemma decode_val_cast: | _ => True end. Proof. - unfold decode_val; intros; destruct chunk; auto; destruct (proj_bytes l); auto. - unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. omega. - unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. omega. - unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. omega. - unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. omega. + intros. + assert (A: Val.has_rettype v (rettype_of_chunk chunk)) by apply decode_val_rettype. + destruct chunk; auto; simpl in A; destruct v; try contradiction; simpl; congruence. Qed. (** Pointers cannot be forged. *) diff --git a/common/Memory.v b/common/Memory.v index b68a5049..9f9934c2 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -682,6 +682,15 @@ Proof. apply decode_val_type. Qed. +Theorem load_rettype: + forall m chunk b ofs v, + load chunk m b ofs = Some v -> + Val.has_rettype v (rettype_of_chunk chunk). +Proof. + intros. exploit load_result; eauto; intros. rewrite H0. + apply decode_val_rettype. +Qed. + Theorem load_cast: forall m chunk b ofs v, load chunk m b ofs = Some v -> diff --git a/common/Memtype.v b/common/Memtype.v index 53775d8b..ca9c6f1f 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -300,6 +300,11 @@ Axiom load_type: load chunk m b ofs = Some v -> Val.has_type v (type_of_chunk chunk). +Axiom load_rettype: + forall m chunk b ofs v, + load chunk m b ofs = Some v -> + Val.has_rettype v (rettype_of_chunk chunk). + (** For a small integer or float type, the value returned by [load] is invariant under the corresponding cast. *) Axiom load_cast: diff --git a/common/PrintAST.ml b/common/PrintAST.ml index e477957a..cf3a17d5 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -27,6 +27,14 @@ let name_of_type = function | Tany32 -> "any32" | Tany64 -> "any64" +let name_of_rettype = function + | Tret t -> name_of_type t + | Tvoid -> "void" + | Tint8signed -> "int8s" + | Tint8unsigned -> "int8u" + | Tint16signed -> "int16s" + | Tint16unsigned -> "int16u" + let name_of_chunk = function | Mint8signed -> "int8s" | Mint8unsigned -> "int8u" diff --git a/common/Values.v b/common/Values.v index de317734..68a2054b 100644 --- a/common/Values.v +++ b/common/Values.v @@ -149,6 +149,23 @@ Proof. auto. Defined. +Definition has_rettype (v: val) (r: rettype) : Prop := + match r, v with + | Tret t, _ => has_type v t + | Tint8signed, Vint n => n = Int.sign_ext 8 n + | Tint8unsigned, Vint n => n = Int.zero_ext 8 n + | Tint16signed, Vint n => n = Int.sign_ext 16 n + | Tint16unsigned, Vint n => n = Int.zero_ext 16 n + | _, Vundef => True + | _, _ => False + end. + +Lemma has_proj_rettype: forall v r, + has_rettype v r -> has_type v (proj_rettype r). +Proof. + destruct r; simpl; intros; auto; destruct v; try contradiction; exact I. +Qed. + (** Truth values. Non-zero integers are treated as [True]. The integer 0 (also used to represent the null pointer) is [False]. Other values are neither true nor false. *) @@ -1003,10 +1020,24 @@ Definition load_result (chunk: memory_chunk) (v: val) := | _, _ => Vundef end. +Lemma load_result_rettype: + forall chunk v, has_rettype (load_result chunk v) (rettype_of_chunk chunk). +Proof. + intros. unfold has_rettype; destruct chunk; destruct v; simpl; auto. +- rewrite Int.sign_ext_idem by omega; auto. +- rewrite Int.zero_ext_idem by omega; auto. +- rewrite Int.sign_ext_idem by omega; auto. +- rewrite Int.zero_ext_idem by omega; auto. +- destruct Archi.ptr64 eqn:SF; simpl; auto. +- destruct Archi.ptr64 eqn:SF; simpl; auto. +- destruct Archi.ptr64 eqn:SF; simpl; auto. +Qed. + Lemma load_result_type: forall chunk v, has_type (load_result chunk v) (type_of_chunk chunk). Proof. - intros. unfold has_type; destruct chunk; destruct v; simpl; auto; destruct Archi.ptr64 eqn:SF; simpl; auto. + intros. rewrite <- proj_rettype_of_chunk. apply has_proj_rettype. + apply load_result_rettype. Qed. Lemma load_result_same: @@ -12,4 +12,4 @@ make -q ${1}o || { done) } -"${COQBIN}coqide" $INCLUDES $1 && make ${1}o +"${COQBIN}coqide" -async-proofs off $INCLUDES $1 && make ${1}o diff --git a/driver/Interp.ml b/driver/Interp.ml index a6841460..3fae70e9 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -20,7 +20,7 @@ open Values open Memory open Globalenvs open Events -open Ctypes +open !Ctypes open Csyntax open Csem diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index d86e137a..c9d6fced 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -18,7 +18,7 @@ open Format open Camlcoq open AST -open Ctypes +open! Ctypes open Cop open Clight @@ -221,6 +221,14 @@ let asttype p t = | AST.Tany32 -> "AST.Tany32" | AST.Tany64 -> "AST.Tany64") +let astrettype p = function + | AST.Tret t -> asttype p t + | AST.Tvoid -> fprintf p "AST.Tvoid" + | AST.Tint8signed -> fprintf p "AST.Tint8signed" + | AST.Tint8unsigned -> fprintf p "AST.Tint8unsigned" + | AST.Tint16signed -> fprintf p "AST.Tint16signed" + | AST.Tint16unsigned -> fprintf p "AST.Tint16unsigned" + let name_of_chunk = function | Mint8signed -> "Mint8signed" | Mint8unsigned -> "Mint8unsigned" @@ -236,7 +244,7 @@ let name_of_chunk = function let signatur p sg = fprintf p "@[<hov 2>(mksignature@ %a@ %a@ %a)@]" (print_list asttype) sg.sig_args - (print_option asttype) sg.sig_res + astrettype sg.sig_res callconv sg.sig_cc let assertions = ref ([]: (string * typ list) list) diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 704b0aba..ce88778c 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -852,7 +852,7 @@ let expand_instruction instr = if variadic then begin emit (Pmflr GPR0); emit (Pbl(intern_string "__compcert_va_saveregs", - {sig_args = []; sig_res = None; sig_cc = cc_default})); + {sig_args = []; sig_res = Tvoid; sig_cc = cc_default})); emit (Pmtlr GPR0) end; current_function_stacksize := sz; diff --git a/powerpc/Builtins1.v b/powerpc/Builtins1.v index f6e643d2..53c83d7e 100644 --- a/powerpc/Builtins1.v +++ b/powerpc/Builtins1.v @@ -29,5 +29,5 @@ Definition platform_builtin_table : list (string * platform_builtin) := Definition platform_builtin_sig (b: platform_builtin) : signature := match b with end. -Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := match b with end. diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index 1de55c1a..7c1b2750 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -117,18 +117,16 @@ Definition dummy_float_reg := F0. (**r Used in [Coloring]. *) We treat a function without result as a function with one integer result. *) Definition loc_result_32 (s: signature) : rpair mreg := - match s.(sig_res) with - | None => One R3 - | Some (Tint | Tany32) => One R3 - | Some (Tfloat | Tsingle | Tany64) => One F1 - | Some Tlong => Twolong R3 R4 + match proj_sig_res s with + | Tint | Tany32 => One R3 + | Tfloat | Tsingle | Tany64 => One F1 + | Tlong => Twolong R3 R4 end. Definition loc_result_64 (s: signature) : rpair mreg := - match s.(sig_res) with - | None => One R3 - | Some (Tint | Tlong | Tany32 | Tany64) => One R3 - | Some (Tfloat | Tsingle) => One F1 + match proj_sig_res s with + | Tint | Tlong | Tany32 | Tany64 => One R3 + | Tfloat | Tsingle => One F1 end. Definition loc_result := @@ -140,8 +138,8 @@ Lemma loc_result_type: forall sig, subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. - intros. unfold proj_sig_res, loc_result, loc_result_32, loc_result_64, mreg_type. - destruct Archi.ptr64 eqn:?; destruct (sig_res sig) as [[]|]; destruct Archi.ppc64; simpl; auto. + intros. unfold loc_result, loc_result_32, loc_result_64, mreg_type. + destruct Archi.ptr64 eqn:?; destruct (proj_sig_res sig); destruct Archi.ppc64; simpl; auto. Qed. (** The result locations are caller-save registers *) @@ -151,7 +149,7 @@ Lemma loc_result_caller_save: forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. intros. unfold loc_result, loc_result_32, loc_result_64, is_callee_save; - destruct Archi.ptr64; destruct (sig_res s) as [[]|]; simpl; auto. + destruct Archi.ptr64; destruct (proj_sig_res s); simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -161,13 +159,13 @@ Lemma loc_result_pair: match loc_result sg with | One _ => True | Twolong r1 r2 => - r1 <> r2 /\ sg.(sig_res) = Some Tlong + r1 <> r2 /\ proj_sig_res sg = Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.ptr64 = false end. Proof. intros; unfold loc_result, loc_result_32, loc_result_64, mreg_type; - destruct Archi.ptr64; destruct (sig_res sg) as [[]|]; destruct Archi.ppc64; simpl; auto. + destruct Archi.ptr64; destruct (proj_sig_res sg); destruct Archi.ppc64; simpl; auto. split; auto. congruence. split; auto. congruence. Qed. @@ -177,7 +175,7 @@ Qed. Lemma loc_result_exten: forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2. Proof. - intros. unfold loc_result, loc_result_32, loc_result_64. + intros. unfold loc_result, loc_result_32, loc_result_64, proj_sig_res. destruct Archi.ptr64; rewrite H; auto. Qed. diff --git a/riscV/Builtins1.v b/riscV/Builtins1.v index f6e643d2..53c83d7e 100644 --- a/riscV/Builtins1.v +++ b/riscV/Builtins1.v @@ -29,5 +29,5 @@ Definition platform_builtin_table : list (string * platform_builtin) := Definition platform_builtin_sig (b: platform_builtin) : signature := match b with end. -Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := match b with end. diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v index df7ddfd2..09cbbb44 100644 --- a/riscV/Conventions1.v +++ b/riscV/Conventions1.v @@ -115,11 +115,10 @@ Definition is_float_reg (r: mreg) := with one integer result. *) Definition loc_result (s: signature) : rpair mreg := - match s.(sig_res) with - | None => One R10 - | Some (Tint | Tany32) => One R10 - | Some (Tfloat | Tsingle | Tany64) => One F10 - | Some Tlong => if Archi.ptr64 then One R10 else Twolong R11 R10 + match proj_sig_res s with + | Tint | Tany32 => One R10 + | Tfloat | Tsingle | Tany64 => One F10 + | Tlong => if Archi.ptr64 then One R10 else Twolong R11 R10 end. (** The result registers have types compatible with that given in the signature. *) @@ -128,8 +127,8 @@ Lemma loc_result_type: forall sig, subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. - intros. unfold proj_sig_res, loc_result, mreg_type; - destruct (sig_res sig) as [[]|]; auto; destruct Archi.ptr64; auto. + intros. unfold loc_result, mreg_type; + destruct (proj_sig_res sig); auto; destruct Archi.ptr64; auto. Qed. (** The result locations are caller-save registers *) @@ -139,7 +138,7 @@ Lemma loc_result_caller_save: forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. intros. unfold loc_result, is_callee_save; - destruct (sig_res s) as [[]|]; simpl; auto; destruct Archi.ptr64; simpl; auto. + destruct (proj_sig_res s); simpl; auto; destruct Archi.ptr64; simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -149,13 +148,13 @@ Lemma loc_result_pair: match loc_result sg with | One _ => True | Twolong r1 r2 => - r1 <> r2 /\ sg.(sig_res) = Some Tlong + r1 <> r2 /\ proj_sig_res sg = Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.ptr64 = false end. Proof. intros. - unfold loc_result; destruct (sig_res sg) as [[]|]; auto. + unfold loc_result; destruct (proj_sig_res sg); auto. unfold mreg_type; destruct Archi.ptr64; auto. split; auto. congruence. Qed. @@ -165,7 +164,7 @@ Qed. Lemma loc_result_exten: forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2. Proof. - intros. unfold loc_result. rewrite H; auto. + intros. unfold loc_result, proj_sig_res. rewrite H; auto. Qed. (** ** Location of function arguments *) diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml index 16426ce3..c82d406e 100644 --- a/x86/Asmexpand.ml +++ b/x86/Asmexpand.ml @@ -506,7 +506,7 @@ let expand_instruction instr = (* Save the registers *) emit (Pleaq (R10, linear_addr RSP (Z.of_uint save_regs))); emit (Pcall_s (intern_string "__compcert_va_saveregs", - {sig_args = []; sig_res = None; sig_cc = cc_default})) + {sig_args = []; sig_res = Tvoid; sig_cc = cc_default})) end; (* Stack chaining *) let fullsz = sz + 8 in diff --git a/x86/Builtins1.v b/x86/Builtins1.v index 6103cc4c..f1d60961 100644 --- a/x86/Builtins1.v +++ b/x86/Builtins1.v @@ -33,10 +33,10 @@ Definition platform_builtin_table : list (string * platform_builtin) := Definition platform_builtin_sig (b: platform_builtin) : signature := match b with | BI_fmin | BI_fmax => - mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default + mksignature (Tfloat :: Tfloat :: nil) Tfloat cc_default end. -Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := match b with | BI_fmin => mkbuiltin_n2t Tfloat Tfloat Tfloat diff --git a/x86/Conventions1.v b/x86/Conventions1.v index 646c4afb..595cb721 100644 --- a/x86/Conventions1.v +++ b/x86/Conventions1.v @@ -99,22 +99,20 @@ Definition is_float_reg (r: mreg) := function with one integer result. *) Definition loc_result_32 (s: signature) : rpair mreg := - match s.(sig_res) with - | None => One AX - | Some (Tint | Tany32) => One AX - | Some (Tfloat | Tsingle) => One FP0 - | Some Tany64 => One X0 - | Some Tlong => Twolong DX AX + match proj_sig_res s with + | Tint | Tany32 => One AX + | Tfloat | Tsingle => One FP0 + | Tany64 => One X0 + | Tlong => Twolong DX AX end. (** In 64 bit mode, he result value of a function is passed back to the caller in registers [AX] or [X0]. *) Definition loc_result_64 (s: signature) : rpair mreg := - match s.(sig_res) with - | None => One AX - | Some (Tint | Tlong | Tany32 | Tany64) => One AX - | Some (Tfloat | Tsingle) => One X0 + match proj_sig_res s with + | Tint | Tlong | Tany32 | Tany64 => One AX + | Tfloat | Tsingle => One X0 end. Definition loc_result := @@ -126,8 +124,8 @@ Lemma loc_result_type: forall sig, subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. - intros. unfold proj_sig_res, loc_result, loc_result_32, loc_result_64, mreg_type; - destruct Archi.ptr64; destruct (sig_res sig) as [[]|]; auto. + intros. unfold loc_result, loc_result_32, loc_result_64, mreg_type; + destruct Archi.ptr64; destruct (proj_sig_res sig); auto. Qed. (** The result locations are caller-save registers *) @@ -137,7 +135,7 @@ Lemma loc_result_caller_save: forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. intros. unfold loc_result, loc_result_32, loc_result_64, is_callee_save; - destruct Archi.ptr64; destruct (sig_res s) as [[]|]; simpl; auto. + destruct Archi.ptr64; destruct (proj_sig_res s); simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -147,14 +145,14 @@ Lemma loc_result_pair: match loc_result sg with | One _ => True | Twolong r1 r2 => - r1 <> r2 /\ sg.(sig_res) = Some Tlong + r1 <> r2 /\ proj_sig_res sg = Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.ptr64 = false end. Proof. intros. unfold loc_result, loc_result_32, loc_result_64, mreg_type; - destruct Archi.ptr64; destruct (sig_res sg) as [[]|]; auto. + destruct Archi.ptr64; destruct (proj_sig_res sg); auto. split; auto. congruence. Qed. @@ -163,7 +161,7 @@ Qed. Lemma loc_result_exten: forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2. Proof. - intros. unfold loc_result, loc_result_32, loc_result_64. + intros. unfold loc_result, loc_result_32, loc_result_64, proj_sig_res. destruct Archi.ptr64; rewrite H; auto. Qed. |