diff options
| -rw-r--r-- | backend/SelectLong.vp | 152 | ||||
| -rw-r--r-- | backend/SelectLongproof.v | 177 | ||||
| -rw-r--r-- | backend/Selection.v | 53 | ||||
| -rw-r--r-- | backend/Selectionproof.v | 114 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 55 | ||||
| -rw-r--r-- | extraction/extraction.v | 6 |
6 files changed, 306 insertions, 251 deletions
diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp index ab4ab8c4..970386a9 100644 --- a/backend/SelectLong.vp +++ b/backend/SelectLong.vp @@ -20,31 +20,30 @@ Require Import Op. Require Import CminorSel. Require Import SelectOp. -Open Local Scope cminorsel_scope. +Local Open Scope cminorsel_scope. +Local Open Scope string_scope. (** Some operations on 64-bit integers are transformed into calls to - runtime library functions. The following record type collects - the names of these functions. *) - -Record helper_functions : Type := mk_helper_functions { - i64_dtos: ident; (**r float64 -> signed long *) - i64_dtou: ident; (**r float64 -> unsigned long *) - i64_stod: ident; (**r signed long -> float64 *) - i64_utod: ident; (**r unsigned long -> float64 *) - i64_stof: ident; (**r signed long -> float32 *) - i64_utof: ident; (**r unsigned long -> float32 *) - i64_neg: ident; (**r opposite *) - i64_add: ident; (**r addition *) - i64_sub: ident; (**r subtraction *) - i64_mul: ident; (**r multiplication 32x32->64 *) - i64_sdiv: ident; (**r signed division *) - i64_udiv: ident; (**r unsigned division *) - i64_smod: ident; (**r signed remainder *) - i64_umod: ident; (**r unsigned remainder *) - i64_shl: ident; (**r shift left *) - i64_shr: ident; (**r shift right unsigned *) - i64_sar: ident (**r shift right signed *) -}. + runtime library functions or built-in functions. + Here are the names and signatures of these functions. *) + +Definition i64_dtos := ident_of_string "__i64_dtos". +Definition i64_dtou := ident_of_string "__i64_dtou". +Definition i64_stod := ident_of_string "__i64_stod". +Definition i64_utod := ident_of_string "__i64_utod". +Definition i64_stof := ident_of_string "__i64_stof". +Definition i64_utof := ident_of_string "__i64_utof". +Definition i64_neg := ident_of_string "__builtin_negl". +Definition i64_add := ident_of_string "__builtin_addl". +Definition i64_sub := ident_of_string "__builtin_subl". +Definition i64_mul := ident_of_string "__builtin_mull". +Definition i64_sdiv := ident_of_string "__i64_sdiv". +Definition i64_udiv := ident_of_string "__i64_udiv". +Definition i64_smod := ident_of_string "__i64_smod". +Definition i64_umod := ident_of_string "__i64_umod". +Definition i64_shl := ident_of_string "__i64_shl". +Definition i64_shr := ident_of_string "__i64_shr". +Definition i64_sar := ident_of_string "__i64_sar". Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default. Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default. @@ -56,8 +55,6 @@ Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default Section SELECT. -Variable hf: helper_functions. - Definition makelong (h l: expr): expr := Eop Omakelong (h ::: l ::: Enil). @@ -124,28 +121,28 @@ Definition longofintu (e: expr) := Definition negl (e: expr) := match is_longconst e with | Some n => longconst (Int64.neg n) - | None => Ebuiltin (EF_builtin hf.(i64_neg) sig_l_l) (e ::: Enil) + | None => Ebuiltin (EF_builtin i64_neg sig_l_l) (e ::: Enil) end. Definition notl (e: expr) := splitlong e (fun h l => makelong (notint h) (notint l)). Definition longoffloat (arg: expr) := - Eexternal hf.(i64_dtos) sig_f_l (arg ::: Enil). + Eexternal i64_dtos sig_f_l (arg ::: Enil). Definition longuoffloat (arg: expr) := - Eexternal hf.(i64_dtou) sig_f_l (arg ::: Enil). + Eexternal i64_dtou sig_f_l (arg ::: Enil). Definition floatoflong (arg: expr) := - Eexternal hf.(i64_stod) sig_l_f (arg ::: Enil). + Eexternal i64_stod sig_l_f (arg ::: Enil). Definition floatoflongu (arg: expr) := - Eexternal hf.(i64_utod) sig_l_f (arg ::: Enil). + Eexternal i64_utod sig_l_f (arg ::: Enil). Definition longofsingle (arg: expr) := longoffloat (floatofsingle arg). Definition longuofsingle (arg: expr) := longuoffloat (floatofsingle arg). Definition singleoflong (arg: expr) := - Eexternal hf.(i64_stof) sig_l_s (arg ::: Enil). + Eexternal i64_stof sig_l_s (arg ::: Enil). Definition singleoflongu (arg: expr) := - Eexternal hf.(i64_utof) sig_l_s (arg ::: Enil). + Eexternal i64_utof sig_l_s (arg ::: Enil). Definition andl (e1 e2: expr) := splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (and h1 h2) (and l1 l2)). @@ -166,7 +163,7 @@ Definition shllimm (e1: expr) (n: int) := makelong (shlimm (lowlong e1) (Int.sub n Int.iwordsize)) (Eop (Ointconst Int.zero) Enil) else - Eexternal hf.(i64_shl) sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). + Eexternal i64_shl sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). Definition shrluimm (e1: expr) (n: int) := if Int.eq n Int.zero then e1 else @@ -178,7 +175,7 @@ Definition shrluimm (e1: expr) (n: int) := makelong (Eop (Ointconst Int.zero) Enil) (shruimm (highlong e1) (Int.sub n Int.iwordsize)) else - Eexternal hf.(i64_shr) sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). + Eexternal i64_shr sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). Definition shrlimm (e1: expr) (n: int) := if Int.eq n Int.zero then e1 else @@ -191,7 +188,7 @@ Definition shrlimm (e1: expr) (n: int) := (makelong (shrimm (Eletvar 0) (Int.repr 31)) (shrimm (Eletvar 0) (Int.sub n Int.iwordsize))) else - Eexternal hf.(i64_sar) sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). + Eexternal i64_sar sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). Definition is_intconst (e: expr) := match e with @@ -202,23 +199,23 @@ Definition is_intconst (e: expr) := Definition shll (e1 e2: expr) := match is_intconst e2 with | Some n => shllimm e1 n - | None => Eexternal hf.(i64_shl) sig_li_l (e1 ::: e2 ::: Enil) + | None => Eexternal i64_shl sig_li_l (e1 ::: e2 ::: Enil) end. Definition shrlu (e1 e2: expr) := match is_intconst e2 with | Some n => shrluimm e1 n - | None => Eexternal hf.(i64_shr) sig_li_l (e1 ::: e2 ::: Enil) + | None => Eexternal i64_shr sig_li_l (e1 ::: e2 ::: Enil) end. Definition shrl (e1 e2: expr) := match is_intconst e2 with | Some n => shrlimm e1 n - | None => Eexternal hf.(i64_sar) sig_li_l (e1 ::: e2 ::: Enil) + | None => Eexternal i64_sar sig_li_l (e1 ::: e2 ::: Enil) end. Definition addl (e1 e2: expr) := - let default := Ebuiltin (EF_builtin hf.(i64_add) sig_ll_l) (e1 ::: e2 ::: Enil) in + let default := Ebuiltin (EF_builtin i64_add sig_ll_l) (e1 ::: e2 ::: Enil) in match is_longconst e1, is_longconst e2 with | Some n1, Some n2 => longconst (Int64.add n1 n2) | Some n1, _ => if Int64.eq n1 Int64.zero then e2 else default @@ -227,7 +224,7 @@ Definition addl (e1 e2: expr) := end. Definition subl (e1 e2: expr) := - let default := Ebuiltin (EF_builtin hf.(i64_sub) sig_ll_l) (e1 ::: e2 ::: Enil) in + let default := Ebuiltin (EF_builtin i64_sub sig_ll_l) (e1 ::: e2 ::: Enil) in match is_longconst e1, is_longconst e2 with | Some n1, Some n2 => longconst (Int64.sub n1 n2) | Some n1, _ => if Int64.eq n1 Int64.zero then negl e2 else default @@ -237,7 +234,7 @@ Definition subl (e1 e2: expr) := Definition mull_base (e1 e2: expr) := splitlong2 e1 e2 (fun h1 l1 h2 l2 => - Elet (Ebuiltin (EF_builtin hf.(i64_mul) sig_ii_l) (l1 ::: l2 ::: Enil)) + Elet (Ebuiltin (EF_builtin i64_mul sig_ii_l) (l1 ::: l2 ::: Enil)) (makelong (add (add (Eop Ohighlong (Eletvar O ::: Enil)) (mul (lift l1) (lift h2))) @@ -266,11 +263,11 @@ Definition binop_long (id: ident) (sem: int64 -> int64 -> int64) (e1 e2: expr) : | _, _ => Eexternal id sig_ll_l (e1 ::: e2 ::: Enil) end. -Definition divl := binop_long hf.(i64_sdiv) Int64.divs. -Definition modl := binop_long hf.(i64_smod) Int64.mods. +Definition divl := binop_long i64_sdiv Int64.divs. +Definition modl := binop_long i64_smod Int64.mods. Definition divlu (e1 e2: expr) := - let default := Eexternal hf.(i64_udiv) sig_ll_l (e1 ::: e2 ::: Enil) in + let default := Eexternal i64_udiv sig_ll_l (e1 ::: e2 ::: Enil) in match is_longconst e1, is_longconst e2 with | Some n1, Some n2 => longconst (Int64.divu n1 n2) | _, Some n2 => @@ -282,7 +279,7 @@ Definition divlu (e1 e2: expr) := end. Definition modlu (e1 e2: expr) := - let default := Eexternal hf.(i64_umod) sig_ll_l (e1 ::: e2 ::: Enil) in + let default := Eexternal i64_umod sig_ll_l (e1 ::: e2 ::: Enil) in match is_longconst e1, is_longconst e2 with | Some n1, Some n2 => longconst (Int64.modu n1 n2) | _, Some n2 => @@ -363,35 +360,44 @@ Definition cmpl (c: comparison) (e1 e2: expr) := End SELECT. -(** Setting up the helper functions *) +(** Checking that the helper functions are available. *) Require Import Errors. - -Local Open Scope string_scope. +Require Import Globalenvs. Local Open Scope error_monad_scope. -Parameter get_helper: Cminor.genv -> String.string -> signature -> res ident. -Parameter get_builtin: String.string -> signature -> res ident. - -Definition get_helpers (ge: Cminor.genv): res helper_functions := - do i64_dtos <- get_helper ge "__i64_dtos" sig_f_l ; - do i64_dtou <- get_helper ge "__i64_dtou" sig_f_l ; - do i64_stod <- get_helper ge "__i64_stod" sig_l_f ; - do i64_utod <- get_helper ge "__i64_utod" sig_l_f ; - do i64_stof <- get_helper ge "__i64_stof" sig_l_s ; - do i64_utof <- get_helper ge "__i64_utof" sig_l_s ; - do i64_neg <- get_builtin "__builtin_negl" sig_l_l ; - do i64_add <- get_builtin "__builtin_addl" sig_ll_l ; - do i64_sub <- get_builtin "__builtin_subl" sig_ll_l ; - do i64_mul <- get_builtin "__builtin_mull" sig_ll_l ; - do i64_sdiv <- get_helper ge "__i64_sdiv" sig_ll_l ; - do i64_udiv <- get_helper ge "__i64_udiv" sig_ll_l ; - do i64_smod <- get_helper ge "__i64_smod" sig_ll_l ; - do i64_umod <- get_helper ge "__i64_umod" sig_ll_l ; - do i64_shl <- get_helper ge "__i64_shl" sig_li_l ; - do i64_shr <- get_helper ge "__i64_shr" sig_li_l ; - do i64_sar <- get_helper ge "__i64_sar" sig_li_l ; - OK (mk_helper_functions - i64_dtos i64_dtou i64_stod i64_utod i64_stof i64_utof - i64_neg i64_add i64_sub i64_mul i64_sdiv i64_udiv i64_smod i64_umod - i64_shl i64_shr i64_sar). +Definition check_helper (ge: Cminor.genv) (name_sg: ident * signature) : res unit := + let (name, sg) := name_sg in + match Genv.find_symbol ge name with + | None => + Error (CTX name :: MSG ": not declared" :: nil) + | Some b => + match Genv.find_funct_ptr ge b with + | Some (External (EF_external name' sg')) => + if ident_eq name' name && signature_eq sg' sg + then OK tt + else Error (CTX name :: MSG ": wrong declaration" :: nil) + | _ => + Error (CTX name :: MSG ": wrong declaration" :: nil) + end + end. + +Definition i64_helpers := + (i64_dtos, sig_f_l) :: + (i64_dtou, sig_f_l) :: + (i64_stod, sig_l_f) :: + (i64_utod, sig_l_f) :: + (i64_stof, sig_l_s) :: + (i64_utof, sig_l_s) :: + (i64_sdiv, sig_ll_l) :: + (i64_udiv, sig_ll_l) :: + (i64_smod, sig_ll_l) :: + (i64_umod, sig_ll_l) :: + (i64_shl, sig_li_l) :: + (i64_shr, sig_li_l) :: + (i64_sar, sig_li_l) :: + nil. + +Definition check_helpers (ge: Cminor.genv): res unit := + do x <- mmap (check_helper ge) i64_helpers; + OK tt. diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v index c7c7ab2d..40c11dd8 100644 --- a/backend/SelectLongproof.v +++ b/backend/SelectLongproof.v @@ -32,69 +32,67 @@ Open Local Scope cminorsel_scope. (** * Axiomatization of the helper functions *) -Section HELPERS. - -Context {F V: Type} (ge: Genv.t (AST.fundef F) V). - -Definition helper_implements (id: ident) (sg: signature) (vargs: list val) (vres: val) : Prop := - exists b, exists ef, - Genv.find_symbol ge id = Some b - /\ Genv.find_funct_ptr ge b = Some (External ef) - /\ ef_sig ef = sg - /\ forall m, external_call ef ge vargs m E0 vres m. +Definition external_implements (id: ident) (sg: signature) (vargs: list val) (vres: val) : Prop := + forall F V (ge: Genv.t F V) m, + external_call (EF_external id sg) ge vargs m E0 vres m. Definition builtin_implements (id: ident) (sg: signature) (vargs: list val) (vres: val) : Prop := - forall m, external_call (EF_builtin id sg) ge vargs m E0 vres m. - -Definition i64_helpers_correct (hf: helper_functions) : Prop := - (forall x z, Val.longoffloat x = Some z -> helper_implements hf.(i64_dtos) sig_f_l (x::nil) z) - /\(forall x z, Val.longuoffloat x = Some z -> helper_implements hf.(i64_dtou) sig_f_l (x::nil) z) - /\(forall x z, Val.floatoflong x = Some z -> helper_implements hf.(i64_stod) sig_l_f (x::nil) z) - /\(forall x z, Val.floatoflongu x = Some z -> helper_implements hf.(i64_utod) sig_l_f (x::nil) z) - /\(forall x z, Val.singleoflong x = Some z -> helper_implements hf.(i64_stof) sig_l_s (x::nil) z) - /\(forall x z, Val.singleoflongu x = Some z -> helper_implements hf.(i64_utof) sig_l_s (x::nil) z) - /\(forall x, builtin_implements hf.(i64_neg) sig_l_l (x::nil) (Val.negl x)) - /\(forall x y, builtin_implements hf.(i64_add) sig_ll_l (x::y::nil) (Val.addl x y)) - /\(forall x y, builtin_implements hf.(i64_sub) sig_ll_l (x::y::nil) (Val.subl x y)) - /\(forall x y, builtin_implements hf.(i64_mul) sig_ii_l (x::y::nil) (Val.mull' x y)) - /\(forall x y z, Val.divls x y = Some z -> helper_implements hf.(i64_sdiv) sig_ll_l (x::y::nil) z) - /\(forall x y z, Val.divlu x y = Some z -> helper_implements hf.(i64_udiv) sig_ll_l (x::y::nil) z) - /\(forall x y z, Val.modls x y = Some z -> helper_implements hf.(i64_smod) sig_ll_l (x::y::nil) z) - /\(forall x y z, Val.modlu x y = Some z -> helper_implements hf.(i64_umod) sig_ll_l (x::y::nil) z) - /\(forall x y, helper_implements hf.(i64_shl) sig_li_l (x::y::nil) (Val.shll x y)) - /\(forall x y, helper_implements hf.(i64_shr) sig_li_l (x::y::nil) (Val.shrlu x y)) - /\(forall x y, helper_implements hf.(i64_sar) sig_li_l (x::y::nil) (Val.shrl x y)). - -End HELPERS. + forall F V (ge: Genv.t F V) m, + external_call (EF_builtin id sg) ge vargs m E0 vres m. + +Axiom i64_helpers_correct : + (forall x z, Val.longoffloat x = Some z -> external_implements i64_dtos sig_f_l (x::nil) z) + /\ (forall x z, Val.longuoffloat x = Some z -> external_implements i64_dtou sig_f_l (x::nil) z) + /\ (forall x z, Val.floatoflong x = Some z -> external_implements i64_stod sig_l_f (x::nil) z) + /\ (forall x z, Val.floatoflongu x = Some z -> external_implements i64_utod sig_l_f (x::nil) z) + /\ (forall x z, Val.singleoflong x = Some z -> external_implements i64_stof sig_l_s (x::nil) z) + /\ (forall x z, Val.singleoflongu x = Some z -> external_implements i64_utof sig_l_s (x::nil) z) + /\ (forall x, builtin_implements i64_neg sig_l_l (x::nil) (Val.negl x)) + /\ (forall x y, builtin_implements i64_add sig_ll_l (x::y::nil) (Val.addl x y)) + /\ (forall x y, builtin_implements i64_sub sig_ll_l (x::y::nil) (Val.subl x y)) + /\ (forall x y, builtin_implements i64_mul sig_ii_l (x::y::nil) (Val.mull' x y)) + /\ (forall x y z, Val.divls x y = Some z -> external_implements i64_sdiv sig_ll_l (x::y::nil) z) + /\ (forall x y z, Val.divlu x y = Some z -> external_implements i64_udiv sig_ll_l (x::y::nil) z) + /\ (forall x y z, Val.modls x y = Some z -> external_implements i64_smod sig_ll_l (x::y::nil) z) + /\ (forall x y z, Val.modlu x y = Some z -> external_implements i64_umod sig_ll_l (x::y::nil) z) + /\ (forall x y, external_implements i64_shl sig_li_l (x::y::nil) (Val.shll x y)) + /\ (forall x y, external_implements i64_shr sig_li_l (x::y::nil) (Val.shrlu x y)) + /\ (forall x y, external_implements i64_sar sig_li_l (x::y::nil) (Val.shrl x y)). + +Definition helper_declared {F V: Type} (ge: Genv.t (AST.fundef F) V) (name: ident) (sg: signature) : Prop := + exists b, Genv.find_symbol ge name = Some b + /\ Genv.find_funct_ptr ge b = Some (External (EF_external name sg)). (** * Correctness of the instruction selection functions for 64-bit operators *) Section CMCONSTR. -Variable hf: helper_functions. Variable ge: genv. -Hypothesis HELPERS: i64_helpers_correct ge hf. +Hypothesis HELPERS: + forall name sg, In (name, sg) i64_helpers -> helper_declared ge name sg. Variable sp: val. Variable e: env. Variable m: mem. Ltac UseHelper := - red in HELPERS; + generalize i64_helpers_correct; intros; repeat (eauto; match goal with | [ H: _ /\ _ |- _ ] => destruct H end). Lemma eval_helper: forall le id sg args vargs vres, eval_exprlist ge sp e m le args vargs -> - helper_implements ge id sg vargs vres -> + In (id, sg) i64_helpers -> + external_implements id sg vargs vres -> eval_expr ge sp e m le (Eexternal id sg args) vres. Proof. - intros. destruct H0 as (b & ef & A & B & C & D). econstructor; eauto. + intros. exploit HELPERS; eauto. intros (b & A & B). econstructor; eauto. Qed. Corollary eval_helper_1: forall le id sg arg1 varg1 vres, eval_expr ge sp e m le arg1 varg1 -> - helper_implements ge id sg (varg1::nil) vres -> + In (id, sg) i64_helpers -> + external_implements id sg (varg1::nil) vres -> eval_expr ge sp e m le (Eexternal id sg (arg1 ::: Enil)) vres. Proof. intros. eapply eval_helper; eauto. constructor; auto. constructor. @@ -104,7 +102,8 @@ Corollary eval_helper_2: forall le id sg arg1 arg2 varg1 varg2 vres, eval_expr ge sp e m le arg1 varg1 -> eval_expr ge sp e m le arg2 varg2 -> - helper_implements ge id sg (varg1::varg2::nil) vres -> + In (id, sg) i64_helpers -> + external_implements id sg (varg1::varg2::nil) vres -> eval_expr ge sp e m le (Eexternal id sg (arg1 ::: arg2 ::: Enil)) vres. Proof. intros. eapply eval_helper; eauto. constructor; auto. constructor; auto. constructor. @@ -113,7 +112,7 @@ Qed. Remark eval_builtin_1: forall le id sg arg1 varg1 vres, eval_expr ge sp e m le arg1 varg1 -> - builtin_implements ge id sg (varg1::nil) vres -> + builtin_implements id sg (varg1::nil) vres -> eval_expr ge sp e m le (Ebuiltin (EF_builtin id sg) (arg1 ::: Enil)) vres. Proof. intros. econstructor. econstructor. eauto. constructor. apply H0. @@ -123,7 +122,7 @@ Remark eval_builtin_2: forall le id sg arg1 arg2 varg1 varg2 vres, eval_expr ge sp e m le arg1 varg1 -> eval_expr ge sp e m le arg2 varg2 -> - builtin_implements ge id sg (varg1::varg2::nil) vres -> + builtin_implements id sg (varg1::varg2::nil) vres -> eval_expr ge sp e m le (Ebuiltin (EF_builtin id sg) (arg1 ::: arg2 ::: Enil)) vres. Proof. intros. econstructor. constructor; eauto. constructor; eauto. constructor. apply H1. @@ -371,7 +370,7 @@ Proof. f_equal. destruct (zlt (i0 - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); omega. Qed. -Theorem eval_negl: unary_constructor_sound (negl hf) Val.negl. +Theorem eval_negl: unary_constructor_sound negl Val.negl. Proof. unfold negl; red; intros. destruct (is_longconst a) eqn:E. econstructor; split. apply eval_longconst. @@ -395,10 +394,10 @@ Theorem eval_longoffloat: forall le a x y, eval_expr ge sp e m le a x -> Val.longoffloat x = Some y -> - exists v, eval_expr ge sp e m le (longoffloat hf a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longoffloat a) v /\ Val.lessdef y v. Proof. intros; unfold longoffloat. econstructor; split. - eapply eval_helper_1; eauto. UseHelper. + eapply eval_helper_1; eauto. simpl; auto. UseHelper. auto. Qed. @@ -406,10 +405,10 @@ Theorem eval_longuoffloat: forall le a x y, eval_expr ge sp e m le a x -> Val.longuoffloat x = Some y -> - exists v, eval_expr ge sp e m le (longuoffloat hf a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longuoffloat a) v /\ Val.lessdef y v. Proof. intros; unfold longuoffloat. econstructor; split. - eapply eval_helper_1; eauto. UseHelper. + eapply eval_helper_1; eauto. simpl; auto. UseHelper. auto. Qed. @@ -417,10 +416,10 @@ Theorem eval_floatoflong: forall le a x y, eval_expr ge sp e m le a x -> Val.floatoflong x = Some y -> - exists v, eval_expr ge sp e m le (floatoflong hf a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (floatoflong a) v /\ Val.lessdef y v. Proof. intros; unfold floatoflong. econstructor; split. - eapply eval_helper_1; eauto. UseHelper. + eapply eval_helper_1; eauto. simpl; auto. UseHelper. auto. Qed. @@ -428,10 +427,10 @@ Theorem eval_floatoflongu: forall le a x y, eval_expr ge sp e m le a x -> Val.floatoflongu x = Some y -> - exists v, eval_expr ge sp e m le (floatoflongu hf a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (floatoflongu a) v /\ Val.lessdef y v. Proof. intros; unfold floatoflongu. econstructor; split. - eapply eval_helper_1; eauto. UseHelper. + eapply eval_helper_1; eauto. simpl; auto. UseHelper. auto. Qed. @@ -439,7 +438,7 @@ Theorem eval_longofsingle: forall le a x y, eval_expr ge sp e m le a x -> Val.longofsingle x = Some y -> - exists v, eval_expr ge sp e m le (longofsingle hf a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longofsingle a) v /\ Val.lessdef y v. Proof. intros; unfold longofsingle. destruct x; simpl in H0; inv H0. destruct (Float32.to_long f) as [n|] eqn:EQ; simpl in H2; inv H2. @@ -453,7 +452,7 @@ Theorem eval_longuofsingle: forall le a x y, eval_expr ge sp e m le a x -> Val.longuofsingle x = Some y -> - exists v, eval_expr ge sp e m le (longuofsingle hf a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longuofsingle a) v /\ Val.lessdef y v. Proof. intros; unfold longuofsingle. destruct x; simpl in H0; inv H0. destruct (Float32.to_longu f) as [n|] eqn:EQ; simpl in H2; inv H2. @@ -467,10 +466,10 @@ Theorem eval_singleoflong: forall le a x y, eval_expr ge sp e m le a x -> Val.singleoflong x = Some y -> - exists v, eval_expr ge sp e m le (singleoflong hf a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (singleoflong a) v /\ Val.lessdef y v. Proof. intros; unfold singleoflong. econstructor; split. - eapply eval_helper_1; eauto. UseHelper. + eapply eval_helper_1; eauto. simpl; auto 20. UseHelper. auto. Qed. @@ -478,10 +477,10 @@ Theorem eval_singleoflongu: forall le a x y, eval_expr ge sp e m le a x -> Val.singleoflongu x = Some y -> - exists v, eval_expr ge sp e m le (singleoflongu hf a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (singleoflongu a) v /\ Val.lessdef y v. Proof. intros; unfold singleoflongu. econstructor; split. - eapply eval_helper_1; eauto. UseHelper. + eapply eval_helper_1; eauto. simpl; auto 20. UseHelper. auto. Qed. @@ -579,7 +578,7 @@ Qed. Lemma eval_shllimm: forall n, - unary_constructor_sound (fun e => shllimm hf e n) (fun v => Val.shll v (Vint n)). + unary_constructor_sound (fun e => shllimm e n) (fun v => Val.shll v (Vint n)). Proof. unfold shllimm; red; intros. apply eval_shift_imm; intros. @@ -609,10 +608,11 @@ Proof. simpl. erewrite <- Int64.decompose_shl_2. instantiate (1 := Int64.hiword i). rewrite Int64.ofwords_recompose. auto. auto. + (* n >= 64 *) - econstructor; split. eapply eval_helper_2; eauto. EvalOp. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. EvalOp. + simpl; auto 20. UseHelper. auto. Qed. -Theorem eval_shll: binary_constructor_sound (shll hf) Val.shll. +Theorem eval_shll: binary_constructor_sound shll Val.shll. Proof. unfold shll; red; intros. destruct (is_intconst b) as [n|] eqn:IC. @@ -620,12 +620,12 @@ Proof. exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0. eapply eval_shllimm; eauto. - (* General case *) - econstructor; split. eapply eval_helper_2; eauto. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto. Qed. Lemma eval_shrluimm: forall n, - unary_constructor_sound (fun e => shrluimm hf e n) (fun v => Val.shrlu v (Vint n)). + unary_constructor_sound (fun e => shrluimm e n) (fun v => Val.shrlu v (Vint n)). Proof. unfold shrluimm; red; intros. apply eval_shift_imm; intros. + (* n = 0 *) @@ -654,10 +654,10 @@ Proof. simpl. erewrite <- Int64.decompose_shru_2. instantiate (1 := Int64.loword i). rewrite Int64.ofwords_recompose. auto. auto. + (* n >= 64 *) - econstructor; split. eapply eval_helper_2; eauto. EvalOp. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. EvalOp. simpl; auto 20. UseHelper. auto. Qed. -Theorem eval_shrlu: binary_constructor_sound (shrlu hf) Val.shrlu. +Theorem eval_shrlu: binary_constructor_sound shrlu Val.shrlu. Proof. unfold shrlu; red; intros. destruct (is_intconst b) as [n|] eqn:IC. @@ -665,12 +665,12 @@ Proof. exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0. eapply eval_shrluimm; eauto. - (* General case *) - econstructor; split. eapply eval_helper_2; eauto. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto. Qed. Lemma eval_shrlimm: forall n, - unary_constructor_sound (fun e => shrlimm hf e n) (fun v => Val.shrl v (Vint n)). + unary_constructor_sound (fun e => shrlimm e n) (fun v => Val.shrl v (Vint n)). Proof. unfold shrlimm; red; intros. apply eval_shift_imm; intros. + (* n = 0 *) @@ -703,10 +703,10 @@ Proof. erewrite <- Int64.decompose_shr_2. instantiate (1 := Int64.loword i). rewrite Int64.ofwords_recompose. auto. auto. + (* n >= 64 *) - econstructor; split. eapply eval_helper_2; eauto. EvalOp. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. EvalOp. simpl; auto 20. UseHelper. auto. Qed. -Theorem eval_shrl: binary_constructor_sound (shrl hf) Val.shrl. +Theorem eval_shrl: binary_constructor_sound shrl Val.shrl. Proof. unfold shrl; red; intros. destruct (is_intconst b) as [n|] eqn:IC. @@ -714,17 +714,17 @@ Proof. exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0. eapply eval_shrlimm; eauto. - (* General case *) - econstructor; split. eapply eval_helper_2; eauto. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto. Qed. -Theorem eval_addl: binary_constructor_sound (addl hf) Val.addl. +Theorem eval_addl: binary_constructor_sound addl Val.addl. Proof. unfold addl; red; intros. - set (default := Ebuiltin (EF_builtin (i64_add hf) sig_ll_l) (a ::: b ::: Enil)). + set (default := Ebuiltin (EF_builtin i64_add sig_ll_l) (a ::: b ::: Enil)). assert (DEFAULT: exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.addl x y) v). { - econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto. + econstructor; split. eapply eval_builtin_2; eauto. simpl; auto 20. UseHelper. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. @@ -740,14 +740,14 @@ Proof. - auto. Qed. -Theorem eval_subl: binary_constructor_sound (subl hf) Val.subl. +Theorem eval_subl: binary_constructor_sound subl Val.subl. Proof. unfold subl; red; intros. - set (default := Ebuiltin (EF_builtin (i64_sub hf) sig_ll_l) (a ::: b ::: Enil)). + set (default := Ebuiltin (EF_builtin i64_sub sig_ll_l) (a ::: b ::: Enil)). assert (DEFAULT: exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.subl x y) v). { - econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto. + econstructor; split. eapply eval_builtin_2; eauto. simpl; auto 20. UseHelper. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. @@ -764,7 +764,7 @@ Proof. - auto. Qed. -Lemma eval_mull_base: binary_constructor_sound (mull_base hf) Val.mull. +Lemma eval_mull_base: binary_constructor_sound mull_base Val.mull. Proof. unfold mull_base; red; intros. apply eval_splitlong2; auto. - intros. @@ -778,7 +778,7 @@ Proof. exploit eval_add. eexact E2. eexact E3. intros [v5 [E5 L5]]. exploit eval_add. eexact E5. eexact E4. intros [v6 [E6 L6]]. exists (Val.longofwords v6 (Val.loword p)); split. - EvalOp. eapply eval_builtin_2; eauto. UseHelper. + EvalOp. eapply eval_builtin_2; eauto. simpl; auto 20. UseHelper. intros. unfold le1, p in *; subst; simpl in *. inv L3. inv L4. inv L5. simpl in L6. inv L6. simpl. f_equal. symmetry. apply Int64.decompose_mul. @@ -786,7 +786,7 @@ Proof. Qed. Lemma eval_mullimm: - forall n, unary_constructor_sound (fun a => mullimm hf a n) (fun v => Val.mull v (Vlong n)). + forall n, unary_constructor_sound (fun a => mullimm a n) (fun v => Val.mull v (Vlong n)). Proof. unfold mullimm; red; intros. predSpec Int64.eq Int64.eq_spec n Int64.zero. @@ -816,7 +816,7 @@ Proof. apply eval_mull_base; auto. apply eval_longconst. Qed. -Theorem eval_mull: binary_constructor_sound (mull hf) Val.mull. +Theorem eval_mull: binary_constructor_sound mull Val.mull. Proof. unfold mull; red; intros. destruct (is_longconst a) as [p|] eqn:LC1; @@ -836,7 +836,8 @@ Qed. Lemma eval_binop_long: forall id sem le a b x y z, (forall p q, x = Vlong p -> y = Vlong q -> z = Vlong (sem p q)) -> - helper_implements ge id sig_ll_l (x::y::nil) z -> + external_implements id sig_ll_l (x::y::nil) z -> + In (id, sig_ll_l) i64_helpers -> eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> exists v, eval_expr ge sp e m le (binop_long id sem a b) v /\ Val.lessdef z v. @@ -856,7 +857,7 @@ Theorem eval_divl: eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.divls x y = Some z -> - exists v, eval_expr ge sp e m le (divl hf a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (divl a b) v /\ Val.lessdef z v. Proof. intros. eapply eval_binop_long; eauto. intros; subst; simpl in H1. @@ -864,6 +865,7 @@ Proof. || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1. auto. UseHelper. + simpl; auto 20. Qed. Theorem eval_modl: @@ -871,7 +873,7 @@ Theorem eval_modl: eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.modls x y = Some z -> - exists v, eval_expr ge sp e m le (modl hf a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (modl a b) v /\ Val.lessdef z v. Proof. intros. eapply eval_binop_long; eauto. intros; subst; simpl in H1. @@ -879,6 +881,7 @@ Proof. || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1. auto. UseHelper. + simpl; auto 20. Qed. Theorem eval_divlu: @@ -886,14 +889,14 @@ Theorem eval_divlu: eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.divlu x y = Some z -> - exists v, eval_expr ge sp e m le (divlu hf a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (divlu a b) v /\ Val.lessdef z v. Proof. intros. unfold divlu. - set (default := Eexternal (i64_udiv hf) sig_ll_l (a ::: b ::: Enil)). + set (default := Eexternal i64_udiv sig_ll_l (a ::: b ::: Enil)). assert (DEFAULT: exists v, eval_expr ge sp e m le default v /\ Val.lessdef z v). { - econstructor; split. eapply eval_helper_2; eauto. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. @@ -929,14 +932,14 @@ Theorem eval_modlu: eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.modlu x y = Some z -> - exists v, eval_expr ge sp e m le (modlu hf a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (modlu a b) v /\ Val.lessdef z v. Proof. intros. unfold modlu. - set (default := Eexternal (i64_umod hf) sig_ll_l (a ::: b ::: Enil)). + set (default := Eexternal i64_umod sig_ll_l (a ::: b ::: Enil)). assert (DEFAULT: exists v, eval_expr ge sp e m le default v /\ Val.lessdef z v). { - econstructor; split. eapply eval_helper_2; eauto. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. diff --git a/backend/Selection.v b/backend/Selection.v index cd17b9fd..11125856 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -66,8 +66,6 @@ Definition store (chunk: memory_chunk) (e1 e2: expr) := Section SELECTION. -Variable hf: helper_functions. - Definition sel_constant (cst: Cminor.constant) : expr := match cst with | Cminor.Ointconst n => Eop (Ointconst n) Enil @@ -100,19 +98,19 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr := | Cminor.Ointuofsingle => intuofsingle arg | Cminor.Osingleofint => singleofint arg | Cminor.Osingleofintu => singleofintu arg - | Cminor.Onegl => negl hf arg + | Cminor.Onegl => negl arg | Cminor.Onotl => notl arg | Cminor.Ointoflong => intoflong arg | Cminor.Olongofint => longofint arg | Cminor.Olongofintu => longofintu arg - | Cminor.Olongoffloat => longoffloat hf arg - | Cminor.Olonguoffloat => longuoffloat hf arg - | Cminor.Ofloatoflong => floatoflong hf arg - | Cminor.Ofloatoflongu => floatoflongu hf arg - | Cminor.Olongofsingle => longofsingle hf arg - | Cminor.Olonguofsingle => longuofsingle hf arg - | Cminor.Osingleoflong => singleoflong hf arg - | Cminor.Osingleoflongu => singleoflongu hf arg + | Cminor.Olongoffloat => longoffloat arg + | Cminor.Olonguoffloat => longuoffloat arg + | Cminor.Ofloatoflong => floatoflong arg + | Cminor.Ofloatoflongu => floatoflongu arg + | Cminor.Olongofsingle => longofsingle arg + | Cminor.Olonguofsingle => longuofsingle arg + | Cminor.Osingleoflong => singleoflong arg + | Cminor.Osingleoflongu => singleoflongu arg end. Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := @@ -138,19 +136,19 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := | Cminor.Osubfs => subfs arg1 arg2 | Cminor.Omulfs => mulfs arg1 arg2 | Cminor.Odivfs => divfs arg1 arg2 - | Cminor.Oaddl => addl hf arg1 arg2 - | Cminor.Osubl => subl hf arg1 arg2 - | Cminor.Omull => mull hf arg1 arg2 - | Cminor.Odivl => divl hf arg1 arg2 - | Cminor.Odivlu => divlu hf arg1 arg2 - | Cminor.Omodl => modl hf arg1 arg2 - | Cminor.Omodlu => modlu hf arg1 arg2 + | Cminor.Oaddl => addl arg1 arg2 + | Cminor.Osubl => subl arg1 arg2 + | Cminor.Omull => mull arg1 arg2 + | Cminor.Odivl => divl arg1 arg2 + | Cminor.Odivlu => divlu arg1 arg2 + | Cminor.Omodl => modl arg1 arg2 + | Cminor.Omodlu => modlu arg1 arg2 | Cminor.Oandl => andl arg1 arg2 | Cminor.Oorl => orl arg1 arg2 | Cminor.Oxorl => xorl arg1 arg2 - | Cminor.Oshll => shll hf arg1 arg2 - | Cminor.Oshrl => shrl hf arg1 arg2 - | Cminor.Oshrlu => shrlu hf arg1 arg2 + | Cminor.Oshll => shll arg1 arg2 + | Cminor.Oshrl => shrl arg1 arg2 + | Cminor.Oshrlu => shrlu arg1 arg2 | Cminor.Ocmp c => comp c arg1 arg2 | Cminor.Ocmpu c => compu c arg1 arg2 | Cminor.Ocmpf c => compf c arg1 arg2 @@ -248,7 +246,7 @@ Definition sel_switch_long := sel_switch (fun arg n => cmpl Ceq arg (longconst (Int64.repr n))) (fun arg n => cmplu Clt arg (longconst (Int64.repr n))) - (fun arg ofs => subl hf arg (longconst (Int64.repr ofs))) + (fun arg ofs => subl arg (longconst (Int64.repr ofs))) lowlong. (** Conversion from Cminor statements to Cminorsel statements. *) @@ -303,8 +301,8 @@ End SELECTION. (** Conversion of functions. *) -Definition sel_function (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.function) : res function := - do body' <- sel_stmt hf ge f.(Cminor.fn_body); +Definition sel_function (ge: Cminor.genv) (f: Cminor.function) : res function := + do body' <- sel_stmt ge f.(Cminor.fn_body); OK (mkfunction f.(Cminor.fn_sig) f.(Cminor.fn_params) @@ -312,12 +310,13 @@ Definition sel_function (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.func f.(Cminor.fn_stackspace) body'). -Definition sel_fundef (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.fundef) : res fundef := - transf_partial_fundef (sel_function hf ge) f. +Definition sel_fundef (ge: Cminor.genv) (f: Cminor.fundef) : res fundef := + transf_partial_fundef (sel_function ge) f. (** Conversion of programs. *) Definition sel_program (p: Cminor.program) : res program := let ge := Genv.globalenv p in - do hf <- get_helpers ge; transform_partial_program (sel_fundef hf ge) p. + do x <- check_helpers ge; + transform_partial_program (sel_fundef ge) p. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 672853e3..bb9bd592 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -46,9 +46,9 @@ Variable prog: Cminor.program. Variable tprog: CminorSel.program. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. -Variable hf: helper_functions. -Hypothesis HELPERS: i64_helpers_correct tge hf. -Hypothesis TRANSFPROG: transform_partial_program (sel_fundef hf ge) prog = OK tprog. +Hypothesis HELPERS: + forall name sg, In (name, sg) i64_helpers -> helper_declared ge name sg. +Hypothesis TRANSFPROG: transform_partial_program (sel_fundef ge) prog = OK tprog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. @@ -65,7 +65,7 @@ Qed. Lemma function_ptr_translated: forall (b: block) (f: Cminor.fundef), Genv.find_funct_ptr ge b = Some f -> - exists tf, Genv.find_funct_ptr tge b = Some tf /\ sel_fundef hf ge f = OK tf. + exists tf, Genv.find_funct_ptr tge b = Some tf /\ sel_fundef ge f = OK tf. Proof. intros. eapply Genv.find_funct_ptr_transf_partial; eauto. Qed. @@ -74,7 +74,7 @@ Lemma functions_translated: forall (v v': val) (f: Cminor.fundef), Genv.find_funct ge v = Some f -> Val.lessdef v v' -> - exists tf, Genv.find_funct tge v' = Some tf /\ sel_fundef hf ge f = OK tf. + exists tf, Genv.find_funct tge v' = Some tf /\ sel_fundef ge f = OK tf. Proof. intros. inv H0. eapply Genv.find_funct_transf_partial; eauto. @@ -82,13 +82,13 @@ Proof. Qed. Lemma sig_function_translated: - forall f tf, sel_fundef hf ge f = OK tf -> funsig tf = Cminor.funsig f. + forall f tf, sel_fundef ge f = OK tf -> funsig tf = Cminor.funsig f. Proof. intros. destruct f; monadInv H; auto. monadInv EQ. auto. Qed. Lemma stackspace_function_translated: - forall f tf, sel_function hf ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f. + forall f tf, sel_function ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f. Proof. intros. monadInv H. auto. Qed. @@ -99,38 +99,18 @@ Proof. intros; eapply Genv.find_var_info_transf_partial; eauto. Qed. -Lemma helper_implements_preserved: - forall id sg vargs vres, - helper_implements ge id sg vargs vres -> - helper_implements tge id sg vargs vres. +Lemma helper_declared_preserved: + forall id sg, helper_declared ge id sg -> helper_declared tge id sg. Proof. - intros. destruct H as (b & ef & A & B & C & D). + intros id sg (b & A & B). exploit function_ptr_translated; eauto. simpl. intros (tf & P & Q). inv Q. - exists b; exists ef. - split. rewrite symbols_preserved. auto. - split. auto. - split. auto. - intros. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. -Qed. - -Lemma builtin_implements_preserved: - forall id sg vargs vres, - builtin_implements ge id sg vargs vres -> - builtin_implements tge id sg vargs vres. -Proof. - unfold builtin_implements; intros. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + exists b; split; auto. rewrite symbols_preserved. auto. Qed. -Lemma helpers_correct_preserved: - forall h, i64_helpers_correct ge h -> i64_helpers_correct tge h. +Let HELPERS': + forall name sg, In (name, sg) i64_helpers -> helper_declared tge name sg. Proof. - unfold i64_helpers_correct; intros. - repeat (match goal with [ H: _ /\ _ |- _ /\ _ ] => destruct H; split end); - intros; try (eapply helper_implements_preserved; eauto); - try (eapply builtin_implements_preserved; eauto). + intros. apply helper_declared_preserved. auto. Qed. Section CMCONSTR. @@ -192,7 +172,7 @@ Lemma eval_sel_unop: forall le op a1 v1 v, eval_expr tge sp e m le a1 v1 -> eval_unop op v1 = Some v -> - exists v', eval_expr tge sp e m le (sel_unop hf op a1) v' /\ Val.lessdef v v'. + exists v', eval_expr tge sp e m le (sel_unop op a1) v' /\ Val.lessdef v v'. Proof. destruct op; simpl; intros; FuncInv; try subst v. apply eval_cast8unsigned; auto. @@ -235,7 +215,7 @@ Lemma eval_sel_binop: eval_expr tge sp e m le a1 v1 -> eval_expr tge sp e m le a2 v2 -> eval_binop op v1 v2 m = Some v -> - exists v', eval_expr tge sp e m le (sel_binop hf op a1 a2) v' /\ Val.lessdef v v'. + exists v', eval_expr tge sp e m le (sel_binop op a1 a2) v' /\ Val.lessdef v v'. Proof. destruct op; simpl; intros; FuncInv; try subst v. apply eval_add; auto. @@ -456,7 +436,7 @@ Lemma sel_switch_long_correct: forall dfl cases arg sp e m i t le, validate_switch Int64.modulus dfl cases t = true -> eval_expr tge sp e m le arg (Vlong i) -> - eval_exitexpr tge sp e m le (XElet arg (sel_switch_long hf O t)) (switch_target (Int64.unsigned i) dfl cases). + eval_exitexpr tge sp e m le (XElet arg (sel_switch_long O t)) (switch_target (Int64.unsigned i) dfl cases). Proof. intros. eapply sel_switch_correct with (R := Rlong); eauto. - intros until n; intros EVAL R RANGE. @@ -470,7 +450,7 @@ Proof. rewrite Int64.unsigned_repr. destruct (zlt (Int64.unsigned n0) n); auto. unfold Int64.max_unsigned; omega. - intros until n; intros EVAL R RANGE. - exploit eval_subl. eexact HELPERS. eexact EVAL. apply eval_longconst with (n := Int64.repr n). + exploit eval_subl. eexact EVAL. apply eval_longconst with (n := Int64.repr n). intros (vb & A & B). inv R. simpl in B. inv B. econstructor; split; eauto. replace ((Int64.unsigned n0 - n) mod Int64.modulus) @@ -564,7 +544,7 @@ Lemma sel_expr_correct: Cminor.eval_expr ge sp e m a v -> forall e' le m', env_lessdef e e' -> Mem.extends m m' -> - exists v', eval_expr tge sp e' m' le (sel_expr hf a) v' /\ Val.lessdef v v'. + exists v', eval_expr tge sp e' m' le (sel_expr a) v' /\ Val.lessdef v v'. Proof. induction 1; intros; simpl. (* Evar *) @@ -601,7 +581,7 @@ Lemma sel_exprlist_correct: Cminor.eval_exprlist ge sp e m a v -> forall e' le m', env_lessdef e e' -> Mem.extends m m' -> - exists v', eval_exprlist tge sp e' m' le (sel_exprlist hf a) v' /\ Val.lessdef_list v v'. + exists v', eval_exprlist tge sp e' m' le (sel_exprlist a) v' /\ Val.lessdef_list v v'. Proof. induction 1; intros; simpl. exists (@nil val); split; auto. constructor. @@ -616,21 +596,21 @@ Inductive match_cont: Cminor.cont -> CminorSel.cont -> Prop := | match_cont_stop: match_cont Cminor.Kstop Kstop | match_cont_seq: forall s s' k k', - sel_stmt hf ge s = OK s' -> + sel_stmt ge s = OK s' -> match_cont k k' -> match_cont (Cminor.Kseq s k) (Kseq s' k') | match_cont_block: forall k k', match_cont k k' -> match_cont (Cminor.Kblock k) (Kblock k') | match_cont_call: forall id f sp e k f' e' k', - sel_function hf ge f = OK f' -> + sel_function ge f = OK f' -> match_cont k k' -> env_lessdef e e' -> match_cont (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k'). Inductive match_states: Cminor.state -> CminorSel.state -> Prop := | match_state: forall f f' s k s' k' sp e m e' m' - (TF: sel_function hf ge f = OK f') - (TS: sel_stmt hf ge s = OK s') + (TF: sel_function ge f = OK f') + (TS: sel_stmt ge s = OK s') (MC: match_cont k k') (LD: env_lessdef e e') (ME: Mem.extends m m'), @@ -638,7 +618,7 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (Cminor.State f s k sp e m) (State f' s' k' sp e' m') | match_callstate: forall f f' args args' k k' m m' - (TF: sel_fundef hf ge f = OK f') + (TF: sel_fundef ge f = OK f') (MC: match_cont k k') (LD: Val.lessdef_list args args') (ME: Mem.extends m m'), @@ -653,7 +633,7 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (Cminor.Returnstate v k m) (Returnstate v' k' m') | match_builtin_1: forall ef args args' optid f sp e k m al f' e' k' m' - (TF: sel_function hf ge f = OK f') + (TF: sel_function ge f = OK f') (MC: match_cont k k') (LDA: Val.lessdef_list args args') (LDE: env_lessdef e e') @@ -663,7 +643,7 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m) (State f' (Sbuiltin optid ef al) k' sp e' m') | match_builtin_2: forall v v' optid f sp e k m f' e' m' k' - (TF: sel_function hf ge f = OK f') + (TF: sel_function ge f = OK f') (MC: match_cont k k') (LDV: Val.lessdef v v') (LDE: env_lessdef e e') @@ -681,16 +661,16 @@ Qed. Remark find_label_commut: forall lbl s k s' k', match_cont k k' -> - sel_stmt hf ge s = OK s' -> + sel_stmt ge s = OK s' -> match Cminor.find_label lbl s k, find_label lbl s' k' with | None, None => True - | Some(s1, k1), Some(s1', k1') => sel_stmt hf ge s1 = OK s1' /\ match_cont k1 k1' + | Some(s1, k1), Some(s1', k1') => sel_stmt ge s1 = OK s1' /\ match_cont k1 k1' | _, _ => False end. Proof. induction s; intros until k'; simpl; intros MC SE; try (monadInv SE); simpl; auto. (* store *) - unfold store. destruct (addressing m (sel_expr hf e)); simpl; auto. + unfold store. destruct (addressing m (sel_expr e)); simpl; auto. (* call *) destruct (classify_call ge e); simpl; auto. (* tailcall *) @@ -854,7 +834,7 @@ Proof. - (* Slabel *) left; econstructor; split. constructor. constructor; auto. - (* Sgoto *) - assert (sel_stmt hf ge (Cminor.fn_body f) = OK (fn_body f')). + assert (sel_stmt ge (Cminor.fn_body f) = OK (fn_body f')). { monadInv TF; simpl; auto. } exploit (find_label_commut lbl (Cminor.fn_body f) (Cminor.call_cont k)). apply call_cont_commut; eauto. eauto. @@ -922,19 +902,39 @@ Qed. End PRESERVATION. -Axiom get_helpers_correct: - forall ge hf, get_helpers ge = OK hf -> i64_helpers_correct ge hf. +Lemma check_helper_correct: + forall ge name sg res, + check_helper ge (name, sg) = OK res -> helper_declared ge name sg. +Proof with (try discriminate). + unfold check_helper; intros. + destruct (Genv.find_symbol ge name) as [b|] eqn:FS... + destruct (Genv.find_funct_ptr ge b) as [fd|] eqn:FP... + destruct fd... destruct e... destruct (ident_eq name0 name)... + destruct (signature_eq sg0 sg)... + subst. exists b; auto. +Qed. + +Lemma check_helpers_correct: + forall ge res, check_helpers ge = OK res -> + forall name sg, In (name, sg) i64_helpers -> helper_declared ge name sg. +Proof. + unfold check_helpers; intros ge res CH name sg. + monadInv CH. generalize (mmap_inversion _ _ EQ). + generalize i64_helpers x. induction 1; simpl; intros. + contradiction. + destruct H1. subst a1. eapply check_helper_correct; eauto. eauto. +Qed. Theorem transf_program_correct: forall prog tprog, sel_program prog = OK tprog -> forward_simulation (Cminor.semantics prog) (CminorSel.semantics tprog). Proof. - intros. unfold sel_program in H. - destruct (get_helpers (Genv.globalenv prog)) as [hf|] eqn:E; simpl in H; try discriminate. - apply forward_simulation_opt with (match_states := match_states prog tprog hf) (measure := measure). + intros. unfold sel_program in H. set (ge := Genv.globalenv prog) in *. + destruct (check_helpers ge) eqn:CH; simpl in H; try discriminate. + apply forward_simulation_opt with (match_states := match_states prog tprog) (measure := measure). eapply public_preserved; eauto. apply sel_initial_states; auto. apply sel_final_states; auto. - apply sel_step_correct; auto. eapply helpers_correct_preserved; eauto. apply get_helpers_correct. auto. + apply sel_step_correct; auto. eapply check_helpers_correct; eauto. Qed. diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 118b6d2d..584c265a 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -188,7 +188,60 @@ let builtins_generic = { "__compcert_va_float64", (TFloat(FDouble, []), [TPtr(TVoid [], [])], - false) + false); + (* Helper functions for int64 arithmetic *) + "__i64_dtos", + (TInt(ILongLong, []), + [TFloat(FDouble, [])], + false); + "__i64_dtou", + (TInt(IULongLong, []), + [TFloat(FDouble, [])], + false); + "__i64_stod", + (TFloat(FDouble, []), + [TInt(ILongLong, [])], + false); + "__i64_utod", + (TFloat(FDouble, []), + [TInt(IULongLong, [])], + false); + "__i64_stof", + (TFloat(FFloat, []), + [TInt(ILongLong, [])], + false); + "__i64_utof", + (TFloat(FFloat, []), + [TInt(IULongLong, [])], + false); + "__i64_sdiv", + (TInt(ILongLong, []), + [TInt(ILongLong, []); TInt(ILongLong, [])], + false); + "__i64_udiv", + (TInt(IULongLong, []), + [TInt(IULongLong, []); TInt(IULongLong, [])], + false); + "__i64_smod", + (TInt(ILongLong, []), + [TInt(ILongLong, []); TInt(ILongLong, [])], + false); + "__i64_umod", + (TInt(IULongLong, []), + [TInt(IULongLong, []); TInt(IULongLong, [])], + false); + "__i64_shl", + (TInt(ILongLong, []), + [TInt(ILongLong, []); TInt(IInt, [])], + false); + "__i64_shr", + (TInt(IULongLong, []), + [TInt(IULongLong, []); TInt(IInt, [])], + false); + "__i64_sar", + (TInt(ILongLong, []), + [TInt(ILongLong, []); TInt(IInt, [])], + false) ] } diff --git a/extraction/extraction.v b/extraction/extraction.v index ee496ffa..94ac6f52 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -57,12 +57,6 @@ Extract Constant Iteration.GenIter.iterate => (* Selection *) -Extract Constant SelectLong.get_helper => - "fun ge s sg -> - Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))". -Extract Constant SelectLong.get_builtin => - "fun s sg -> - Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))". Extract Constant Selection.compile_switch => "Switchaux.compile_switch". (* RTLgen *) |