diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/CMparser.mly | 12 | ||||
-rw-r--r-- | backend/SelectLong.vp | 123 | ||||
-rw-r--r-- | backend/SelectLongproof.v | 195 | ||||
-rw-r--r-- | backend/Selection.v | 110 | ||||
-rw-r--r-- | backend/Selectionproof.v | 162 |
5 files changed, 347 insertions, 255 deletions
diff --git a/backend/CMparser.mly b/backend/CMparser.mly index b48a486e..41bd35a1 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -35,9 +35,9 @@ type ef_token = let mkef sg toks = match toks with | [EFT_tok "extern"; EFT_string s] -> - EF_external(intern_string s, sg) + EF_external(coqstring_of_camlstring s, sg) | [EFT_tok "builtin"; EFT_string s] -> - EF_builtin(intern_string s, sg) + EF_builtin(coqstring_of_camlstring s, sg) | [EFT_tok "volatile"; EFT_tok "load"; EFT_chunk c] -> EF_vload c | [EFT_tok "volatile"; EFT_tok "store"; EFT_chunk c] -> @@ -49,12 +49,12 @@ let mkef sg toks = | [EFT_tok "memcpy"; EFT_tok "size"; EFT_int sz; EFT_tok "align"; EFT_int al] -> EF_memcpy(Z.of_sint32 sz, Z.of_sint32 al) | [EFT_tok "annot"; EFT_string txt] -> - EF_annot(intern_string txt, sg.sig_args) + EF_annot(coqstring_of_camlstring txt, sg.sig_args) | [EFT_tok "annot_val"; EFT_string txt] -> if sg.sig_args = [] then raise Parsing.Parse_error; - EF_annot_val(intern_string txt, List.hd sg.sig_args) + EF_annot_val(coqstring_of_camlstring txt, List.hd sg.sig_args) | [EFT_tok "inline_asm"; EFT_string txt] -> - EF_inline_asm(intern_string txt, sg, []) + EF_inline_asm(coqstring_of_camlstring txt, sg, []) | _ -> raise Parsing.Parse_error @@ -473,7 +473,7 @@ proc: fn_stackspace = $8; fn_body = $10 })) } | EXTERN STRINGLIT COLON signature - { (intern_string $2, Gfun(External(EF_external(intern_string $2,$4)))) } + { (intern_string $2, Gfun(External(EF_external(coqstring_of_camlstring $2,$4)))) } | EXTERN STRINGLIT EQUAL eftoks COLON signature { (intern_string $2, Gfun(External(mkef $6 $4))) } ; diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp index 970386a9..105b284c 100644 --- a/backend/SelectLong.vp +++ b/backend/SelectLong.vp @@ -12,6 +12,7 @@ (** Instruction selection for 64-bit integer operations *) +Require String. Require Import Coqlib. Require Import AST. Require Import Integers. @@ -24,26 +25,24 @@ Local Open Scope cminorsel_scope. Local Open Scope string_scope. (** Some operations on 64-bit integers are transformed into calls to - 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". + 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_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 *) +}. Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default. Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default. @@ -55,6 +54,8 @@ 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). @@ -121,28 +122,28 @@ Definition longofintu (e: expr) := Definition negl (e: expr) := match is_longconst e with | Some n => longconst (Int64.neg n) - | None => Ebuiltin (EF_builtin i64_neg sig_l_l) (e ::: Enil) + | None => Ebuiltin (EF_builtin "__builtin_negl" 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 i64_dtos sig_f_l (arg ::: Enil). + Eexternal hf.(i64_dtos) sig_f_l (arg ::: Enil). Definition longuoffloat (arg: expr) := - Eexternal i64_dtou sig_f_l (arg ::: Enil). + Eexternal hf.(i64_dtou) sig_f_l (arg ::: Enil). Definition floatoflong (arg: expr) := - Eexternal i64_stod sig_l_f (arg ::: Enil). + Eexternal hf.(i64_stod) sig_l_f (arg ::: Enil). Definition floatoflongu (arg: expr) := - Eexternal i64_utod sig_l_f (arg ::: Enil). + Eexternal hf.(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 i64_stof sig_l_s (arg ::: Enil). + Eexternal hf.(i64_stof) sig_l_s (arg ::: Enil). Definition singleoflongu (arg: expr) := - Eexternal i64_utof sig_l_s (arg ::: Enil). + Eexternal hf.(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)). @@ -163,7 +164,7 @@ Definition shllimm (e1: expr) (n: int) := makelong (shlimm (lowlong e1) (Int.sub n Int.iwordsize)) (Eop (Ointconst Int.zero) Enil) else - Eexternal i64_shl sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). + Eexternal hf.(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 @@ -175,7 +176,7 @@ Definition shrluimm (e1: expr) (n: int) := makelong (Eop (Ointconst Int.zero) Enil) (shruimm (highlong e1) (Int.sub n Int.iwordsize)) else - Eexternal i64_shr sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). + Eexternal hf.(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 @@ -188,7 +189,7 @@ Definition shrlimm (e1: expr) (n: int) := (makelong (shrimm (Eletvar 0) (Int.repr 31)) (shrimm (Eletvar 0) (Int.sub n Int.iwordsize))) else - Eexternal i64_sar sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). + Eexternal hf.(i64_sar) sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). Definition is_intconst (e: expr) := match e with @@ -199,23 +200,23 @@ Definition is_intconst (e: expr) := Definition shll (e1 e2: expr) := match is_intconst e2 with | Some n => shllimm e1 n - | None => Eexternal i64_shl sig_li_l (e1 ::: e2 ::: Enil) + | None => Eexternal hf.(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 i64_shr sig_li_l (e1 ::: e2 ::: Enil) + | None => Eexternal hf.(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 i64_sar sig_li_l (e1 ::: e2 ::: Enil) + | None => Eexternal hf.(i64_sar) sig_li_l (e1 ::: e2 ::: Enil) end. Definition addl (e1 e2: expr) := - let default := Ebuiltin (EF_builtin i64_add sig_ll_l) (e1 ::: e2 ::: Enil) in + let default := Ebuiltin (EF_builtin "__builtin_addl" 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 @@ -224,7 +225,7 @@ Definition addl (e1 e2: expr) := end. Definition subl (e1 e2: expr) := - let default := Ebuiltin (EF_builtin i64_sub sig_ll_l) (e1 ::: e2 ::: Enil) in + let default := Ebuiltin (EF_builtin "__builtin_subl" 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 @@ -234,7 +235,7 @@ Definition subl (e1 e2: expr) := Definition mull_base (e1 e2: expr) := splitlong2 e1 e2 (fun h1 l1 h2 l2 => - Elet (Ebuiltin (EF_builtin i64_mul sig_ii_l) (l1 ::: l2 ::: Enil)) + Elet (Ebuiltin (EF_builtin "__builtin_mull" sig_ii_l) (l1 ::: l2 ::: Enil)) (makelong (add (add (Eop Ohighlong (Eletvar O ::: Enil)) (mul (lift l1) (lift h2))) @@ -263,11 +264,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 i64_sdiv Int64.divs. -Definition modl := binop_long i64_smod Int64.mods. +Definition divl e1 e2 := binop_long hf.(i64_sdiv) Int64.divs e1 e2. +Definition modl e1 e2 := binop_long hf.(i64_smod) Int64.mods e1 e2. Definition divlu (e1 e2: expr) := - let default := Eexternal i64_udiv sig_ll_l (e1 ::: e2 ::: Enil) in + let default := Eexternal hf.(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 => @@ -279,7 +280,7 @@ Definition divlu (e1 e2: expr) := end. Definition modlu (e1 e2: expr) := - let default := Eexternal i64_umod sig_ll_l (e1 ::: e2 ::: Enil) in + let default := Eexternal hf.(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 => @@ -359,45 +360,3 @@ Definition cmpl (c: comparison) (e1 e2: expr) := end. End SELECT. - -(** Checking that the helper functions are available. *) - -Require Import Errors. -Require Import Globalenvs. -Local Open Scope error_monad_scope. - -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 40c11dd8..cdfb1107 100644 --- a/backend/SelectLongproof.v +++ b/backend/SelectLongproof.v @@ -12,6 +12,7 @@ (** Correctness of instruction selection for integer division *) +Require Import String. Require Import Coqlib. Require Import AST. Require Import Errors. @@ -29,81 +30,96 @@ Require Import SelectOpproof. Require Import SelectLong. Open Local Scope cminorsel_scope. +Open Local Scope string_scope. (** * Axiomatization of the helper functions *) -Definition external_implements (id: ident) (sg: signature) (vargs: list val) (vres: val) : Prop := +Definition external_implements (name: string) (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. + external_call (EF_external name sg) ge vargs m E0 vres m. -Definition builtin_implements (id: ident) (sg: signature) (vargs: list val) (vres: val) : Prop := +Definition builtin_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop := forall F V (ge: Genv.t F V) m, - external_call (EF_builtin id sg) ge vargs m E0 vres m. + external_call (EF_builtin name 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 + (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 "__builtin_negl" sig_l_l (x::nil) (Val.negl x)) + /\ (forall x y, builtin_implements "__builtin_addl" sig_ll_l (x::y::nil) (Val.addl x y)) + /\ (forall x y, builtin_implements "__builtin_subl" sig_ll_l (x::y::nil) (Val.subl x y)) + /\ (forall x y, builtin_implements "__builtin_mull" 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) (id: ident) (name: string) (sg: signature) : Prop := + exists b, Genv.find_symbol ge id = Some b /\ Genv.find_funct_ptr ge b = Some (External (EF_external name sg)). +Definition helper_functions_declared {F V: Type} (ge: Genv.t (AST.fundef F) V) (hf: helper_functions) : Prop := + helper_declared ge hf.(i64_dtos) "__i64_dtos" sig_f_l + /\ helper_declared ge hf.(i64_dtou) "__i64_dtou" sig_f_l + /\ helper_declared ge hf.(i64_stod) "__i64_stod" sig_l_f + /\ helper_declared ge hf.(i64_utod) "__i64_utod" sig_l_f + /\ helper_declared ge hf.(i64_stof) "__i64_stof" sig_l_s + /\ helper_declared ge hf.(i64_utof) "__i64_utof" sig_l_s + /\ helper_declared ge hf.(i64_sdiv) "__i64_sdiv" sig_ll_l + /\ helper_declared ge hf.(i64_udiv) "__i64_udiv" sig_ll_l + /\ helper_declared ge hf.(i64_smod) "__i64_smod" sig_ll_l + /\ helper_declared ge hf.(i64_umod) "__i64_umod" sig_ll_l + /\ helper_declared ge hf.(i64_shl) "__i64_shl" sig_li_l + /\ helper_declared ge hf.(i64_shr) "__i64_shr" sig_li_l + /\ helper_declared ge hf.(i64_sar) "__i64_sar" sig_li_l. + (** * Correctness of the instruction selection functions for 64-bit operators *) Section CMCONSTR. Variable ge: genv. -Hypothesis HELPERS: - forall name sg, In (name, sg) i64_helpers -> helper_declared ge name sg. +Variable hf: helper_functions. +Hypothesis HELPERS: helper_functions_declared ge hf. Variable sp: val. Variable e: env. Variable m: mem. -Ltac UseHelper := - generalize i64_helpers_correct; intros; - repeat (eauto; match goal with | [ H: _ /\ _ |- _ ] => destruct H end). +Ltac UseHelper := decompose [Logic.and] i64_helpers_correct; eauto. +Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto. Lemma eval_helper: - forall le id sg args vargs vres, + forall le id name sg args vargs vres, eval_exprlist ge sp e m le args vargs -> - In (id, sg) i64_helpers -> - external_implements id sg vargs vres -> + helper_declared ge id name sg -> + external_implements name sg vargs vres -> eval_expr ge sp e m le (Eexternal id sg args) vres. Proof. - intros. exploit HELPERS; eauto. intros (b & A & B). econstructor; eauto. + intros. destruct H0 as (b & P & Q). econstructor; eauto. Qed. Corollary eval_helper_1: - forall le id sg arg1 varg1 vres, + forall le id name sg arg1 varg1 vres, eval_expr ge sp e m le arg1 varg1 -> - In (id, sg) i64_helpers -> - external_implements id sg (varg1::nil) vres -> + helper_declared ge id name sg -> + external_implements name 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. Qed. Corollary eval_helper_2: - forall le id sg arg1 arg2 varg1 varg2 vres, + forall le id name sg arg1 arg2 varg1 varg2 vres, eval_expr ge sp e m le arg1 varg1 -> eval_expr ge sp e m le arg2 varg2 -> - In (id, sg) i64_helpers -> - external_implements id sg (varg1::varg2::nil) vres -> + helper_declared ge id name sg -> + external_implements name 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. @@ -394,51 +410,47 @@ 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 a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longoffloat hf a) v /\ Val.lessdef y v. Proof. intros; unfold longoffloat. econstructor; split. - eapply eval_helper_1; eauto. simpl; auto. UseHelper. - auto. + eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. Qed. 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 a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longuoffloat hf a) v /\ Val.lessdef y v. Proof. intros; unfold longuoffloat. econstructor; split. - eapply eval_helper_1; eauto. simpl; auto. UseHelper. - auto. + eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. Qed. 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 a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (floatoflong hf a) v /\ Val.lessdef y v. Proof. intros; unfold floatoflong. econstructor; split. - eapply eval_helper_1; eauto. simpl; auto. UseHelper. - auto. + eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. Qed. 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 a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (floatoflongu hf a) v /\ Val.lessdef y v. Proof. intros; unfold floatoflongu. econstructor; split. - eapply eval_helper_1; eauto. simpl; auto. UseHelper. - auto. + eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. Qed. 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 a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longofsingle hf 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. @@ -452,7 +464,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 a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longuofsingle hf 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. @@ -466,22 +478,20 @@ 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 a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (singleoflong hf a) v /\ Val.lessdef y v. Proof. intros; unfold singleoflong. econstructor; split. - eapply eval_helper_1; eauto. simpl; auto 20. UseHelper. - auto. + eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. Qed. 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 a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (singleoflongu hf a) v /\ Val.lessdef y v. Proof. intros; unfold singleoflongu. econstructor; split. - eapply eval_helper_1; eauto. simpl; auto 20. UseHelper. - auto. + eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. Qed. Theorem eval_andl: binary_constructor_sound andl Val.andl. @@ -578,7 +588,7 @@ Qed. Lemma eval_shllimm: forall n, - unary_constructor_sound (fun e => shllimm e n) (fun v => Val.shll v (Vint n)). + unary_constructor_sound (fun e => shllimm hf e n) (fun v => Val.shll v (Vint n)). Proof. unfold shllimm; red; intros. apply eval_shift_imm; intros. @@ -608,11 +618,10 @@ 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. - simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto. Qed. -Theorem eval_shll: binary_constructor_sound shll Val.shll. +Theorem eval_shll: binary_constructor_sound (shll hf) Val.shll. Proof. unfold shll; red; intros. destruct (is_intconst b) as [n|] eqn:IC. @@ -620,12 +629,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. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. Lemma eval_shrluimm: forall n, - unary_constructor_sound (fun e => shrluimm e n) (fun v => Val.shrlu v (Vint n)). + unary_constructor_sound (fun e => shrluimm hf e n) (fun v => Val.shrlu v (Vint n)). Proof. unfold shrluimm; red; intros. apply eval_shift_imm; intros. + (* n = 0 *) @@ -654,10 +663,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. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto. Qed. -Theorem eval_shrlu: binary_constructor_sound shrlu Val.shrlu. +Theorem eval_shrlu: binary_constructor_sound (shrlu hf) Val.shrlu. Proof. unfold shrlu; red; intros. destruct (is_intconst b) as [n|] eqn:IC. @@ -665,12 +674,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. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. Lemma eval_shrlimm: forall n, - unary_constructor_sound (fun e => shrlimm e n) (fun v => Val.shrl v (Vint n)). + unary_constructor_sound (fun e => shrlimm hf e n) (fun v => Val.shrl v (Vint n)). Proof. unfold shrlimm; red; intros. apply eval_shift_imm; intros. + (* n = 0 *) @@ -703,10 +712,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. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto. Qed. -Theorem eval_shrl: binary_constructor_sound shrl Val.shrl. +Theorem eval_shrl: binary_constructor_sound (shrl hf) Val.shrl. Proof. unfold shrl; red; intros. destruct (is_intconst b) as [n|] eqn:IC. @@ -714,17 +723,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. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. Theorem eval_addl: binary_constructor_sound addl Val.addl. Proof. unfold addl; red; intros. - set (default := Ebuiltin (EF_builtin i64_add sig_ll_l) (a ::: b ::: Enil)). + set (default := Ebuiltin (EF_builtin "__builtin_addl" 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. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. @@ -743,11 +752,11 @@ Qed. Theorem eval_subl: binary_constructor_sound subl Val.subl. Proof. unfold subl; red; intros. - set (default := Ebuiltin (EF_builtin i64_sub sig_ll_l) (a ::: b ::: Enil)). + set (default := Ebuiltin (EF_builtin "__builtin_subl" 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. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. @@ -778,7 +787,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. simpl; auto 20. UseHelper. + EvalOp. eapply eval_builtin_2; eauto. 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 +795,7 @@ Proof. Qed. Lemma eval_mullimm: - forall n, unary_constructor_sound (fun a => mullimm a n) (fun v => Val.mull v (Vlong n)). + forall n, unary_constructor_sound (fun a => mullimm hf 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 +825,7 @@ Proof. apply eval_mull_base; auto. apply eval_longconst. Qed. -Theorem eval_mull: binary_constructor_sound mull Val.mull. +Theorem eval_mull: binary_constructor_sound (mull hf) Val.mull. Proof. unfold mull; red; intros. destruct (is_longconst a) as [p|] eqn:LC1; @@ -834,10 +843,10 @@ Proof. Qed. Lemma eval_binop_long: - forall id sem le a b x y z, + forall id name sem le a b x y z, (forall p q, x = Vlong p -> y = Vlong q -> z = Vlong (sem p q)) -> - external_implements id sig_ll_l (x::y::nil) z -> - In (id, sig_ll_l) i64_helpers -> + helper_declared ge id name sig_ll_l -> + external_implements name sig_ll_l (x::y::nil) z -> 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. @@ -857,15 +866,14 @@ 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 a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (divl hf a b) v /\ Val.lessdef z v. Proof. intros. eapply eval_binop_long; eauto. intros; subst; simpl in H1. destruct (Int64.eq q Int64.zero || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1. auto. - UseHelper. - simpl; auto 20. + DeclHelper. UseHelper. Qed. Theorem eval_modl: @@ -873,15 +881,14 @@ 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 a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (modl hf a b) v /\ Val.lessdef z v. Proof. intros. eapply eval_binop_long; eauto. intros; subst; simpl in H1. destruct (Int64.eq q Int64.zero || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1. auto. - UseHelper. - simpl; auto 20. + DeclHelper. UseHelper. Qed. Theorem eval_divlu: @@ -889,14 +896,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 a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (divlu hf a b) v /\ Val.lessdef z v. Proof. intros. unfold divlu. - set (default := Eexternal i64_udiv sig_ll_l (a ::: b ::: Enil)). + set (default := Eexternal hf.(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. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. @@ -932,14 +939,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 a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (modlu hf a b) v /\ Val.lessdef z v. Proof. intros. unfold modlu. - set (default := Eexternal i64_umod sig_ll_l (a ::: b ::: Enil)). + set (default := Eexternal hf.(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. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. 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 2e631ad2..dea8a008 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -22,7 +22,9 @@ Instruction selection proceeds by bottom-up rewriting over expressions. The source language is Cminor and the target language is CminorSel. *) +Require String. Require Import Coqlib. +Require Import Maps. Require Import AST. Require Import Errors. Require Import Integers. @@ -67,6 +69,8 @@ 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 @@ -104,14 +108,14 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr := | Cminor.Ointoflong => intoflong arg | Cminor.Olongofint => longofint arg | Cminor.Olongofintu => longofintu 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 + | 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 end. Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := @@ -139,17 +143,17 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := | Cminor.Odivfs => divfs 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.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.Oandl => andl arg1 arg2 | Cminor.Oorl => orl arg1 arg2 | Cminor.Oxorl => xorl arg1 arg2 - | Cminor.Oshll => shll arg1 arg2 - | Cminor.Oshrl => shrl arg1 arg2 - | Cminor.Oshrlu => shrlu arg1 arg2 + | Cminor.Oshll => shll hf arg1 arg2 + | Cminor.Oshrl => shrl hf arg1 arg2 + | Cminor.Oshrlu => shrlu hf arg1 arg2 | Cminor.Ocmp c => comp c arg1 arg2 | Cminor.Ocmpu c => compu c arg1 arg2 | Cminor.Ocmpf c => compf c arg1 arg2 @@ -324,8 +328,6 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt := | Cminor.Sgoto lbl => OK (Sgoto lbl) end. -End SELECTION. - (** Conversion of functions. *) Definition sel_function (ge: Cminor.genv) (f: Cminor.function) : res function := @@ -340,10 +342,76 @@ Definition sel_function (ge: Cminor.genv) (f: Cminor.function) : res function := Definition sel_fundef (ge: Cminor.genv) (f: Cminor.fundef) : res fundef := transf_partial_fundef (sel_function ge) f. +End SELECTION. + +(** Setting up the helper functions. *) + +Definition globdef := AST.globdef Cminor.fundef unit. + +(** We build a partial mapping from global identifiers to their definitions, + restricting ourselves to the globals we are interested in, namely + the external function declarations whose name starts with "__i64_". + This ensures that the mapping remains small and that [lookup_helper] + below is efficient. *) + +Definition globdef_of_interest (gd: globdef) : bool := + match gd with + | Gfun (External (EF_external name sg)) => String.prefix "__i64_" name + | _ => false + end. + +Definition record_globdef (globs: PTree.t globdef) (id_gd: ident * globdef) := + let (id, gd) := id_gd in + if globdef_of_interest gd + then PTree.set id gd globs + else PTree.remove id globs. + +Definition record_globdefs (p: Cminor.program) : PTree.t globdef := + List.fold_left record_globdef p.(prog_defs) (PTree.empty _). + +Definition lookup_helper_aux + (name: String.string) (sg: signature) (res: option ident) + (id: ident) (gd: globdef) := + match gd with + | Gfun (External (EF_external name' sg')) => + if String.string_dec name name' && signature_eq sg sg' + then Some id + else res + | _ => res + end. + +Definition lookup_helper (globs: PTree.t globdef) + (name: String.string) (sg: signature) : res ident := + match PTree.fold (lookup_helper_aux name sg) globs None with + | Some id => OK id + | None => Error (MSG name :: MSG ": missing or incorrect declaration" :: nil) + end. + +Local Open Scope string_scope. + +Definition get_helpers (p: Cminor.program) : res helper_functions := + let globs := record_globdefs p in + do i64_dtos <- lookup_helper globs "__i64_dtos" sig_f_l ; + do i64_dtou <- lookup_helper globs "__i64_dtou" sig_f_l ; + do i64_stod <- lookup_helper globs "__i64_stod" sig_l_f ; + do i64_utod <- lookup_helper globs "__i64_utod" sig_l_f ; + do i64_stof <- lookup_helper globs "__i64_stof" sig_l_s ; + do i64_utof <- lookup_helper globs "__i64_utof" sig_l_s ; + do i64_sdiv <- lookup_helper globs "__i64_sdiv" sig_ll_l ; + do i64_udiv <- lookup_helper globs "__i64_udiv" sig_ll_l ; + do i64_smod <- lookup_helper globs "__i64_smod" sig_ll_l ; + do i64_umod <- lookup_helper globs "__i64_umod" sig_ll_l ; + do i64_shl <- lookup_helper globs "__i64_shl" sig_li_l ; + do i64_shr <- lookup_helper globs "__i64_shr" sig_li_l ; + do i64_sar <- lookup_helper globs "__i64_sar" sig_li_l ; + OK (mk_helper_functions + i64_dtos i64_dtou i64_stod i64_utod i64_stof i64_utof + i64_sdiv i64_udiv i64_smod i64_umod + i64_shl i64_shr i64_sar). + (** Conversion of programs. *) Definition sel_program (p: Cminor.program) : res program := - let ge := Genv.globalenv p in - do x <- check_helpers ge; - transform_partial_program (sel_fundef ge) p. + do hf <- get_helpers p; + transform_partial_program (sel_fundef hf (Genv.globalenv p)) p. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 1d2f2b3a..8ea4c56e 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -46,9 +46,9 @@ Variable prog: Cminor.program. Variable tprog: CminorSel.program. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. -Hypothesis HELPERS: - forall name sg, In (name, sg) i64_helpers -> helper_declared ge name sg. -Hypothesis TRANSFPROG: transform_partial_program (sel_fundef ge) prog = OK tprog. +Variable hf: helper_functions. +Hypothesis HELPERS: helper_functions_declared ge hf. +Hypothesis TRANSFPROG: transform_partial_program (sel_fundef hf ge) prog = OK tprog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. @@ -65,7 +65,7 @@ Qed. Lemma function_ptr_translated: forall (b: block) (f: Cminor.fundef), Genv.find_funct_ptr ge b = Some f -> - exists tf, Genv.find_funct_ptr tge b = Some tf /\ sel_fundef ge f = OK tf. + exists tf, Genv.find_funct_ptr tge b = Some tf /\ sel_fundef hf ge f = OK tf. Proof. intros. eapply Genv.find_funct_ptr_transf_partial; eauto. Qed. @@ -74,7 +74,7 @@ Lemma functions_translated: forall (v v': val) (f: Cminor.fundef), Genv.find_funct ge v = Some f -> Val.lessdef v v' -> - exists tf, Genv.find_funct tge v' = Some tf /\ sel_fundef ge f = OK tf. + exists tf, Genv.find_funct tge v' = Some tf /\ sel_fundef hf ge f = OK tf. Proof. intros. inv H0. eapply Genv.find_funct_transf_partial; eauto. @@ -82,13 +82,13 @@ Proof. Qed. Lemma sig_function_translated: - forall f tf, sel_fundef ge f = OK tf -> funsig tf = Cminor.funsig f. + forall f tf, sel_fundef hf ge f = OK tf -> funsig tf = Cminor.funsig f. Proof. intros. destruct f; monadInv H; auto. monadInv EQ. auto. Qed. Lemma stackspace_function_translated: - forall f tf, sel_function ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f. + forall f tf, sel_function hf ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f. Proof. intros. monadInv H. auto. Qed. @@ -100,17 +100,17 @@ Proof. Qed. Lemma helper_declared_preserved: - forall id sg, helper_declared ge id sg -> helper_declared tge id sg. + forall id name sg, helper_declared ge id name sg -> helper_declared tge id name sg. Proof. - intros id sg (b & A & B). + intros id name sg (b & A & B). exploit function_ptr_translated; eauto. simpl. intros (tf & P & Q). inv Q. exists b; split; auto. rewrite symbols_preserved. auto. Qed. -Let HELPERS': - forall name sg, In (name, sg) i64_helpers -> helper_declared tge name sg. +Let HELPERS': helper_functions_declared tge hf. Proof. - intros. apply helper_declared_preserved. auto. + red in HELPERS; decompose [Logic.and] HELPERS. + red. auto 20 using helper_declared_preserved. Qed. Section CMCONSTR. @@ -172,7 +172,7 @@ Lemma eval_sel_unop: forall le op a1 v1 v, eval_expr tge sp e m le a1 v1 -> eval_unop op v1 = Some v -> - exists v', eval_expr tge sp e m le (sel_unop op a1) v' /\ Val.lessdef v v'. + exists v', eval_expr tge sp e m le (sel_unop hf op a1) v' /\ Val.lessdef v v'. Proof. destruct op; simpl; intros; FuncInv; try subst v. apply eval_cast8unsigned; auto. @@ -215,7 +215,7 @@ Lemma eval_sel_binop: eval_expr tge sp e m le a1 v1 -> eval_expr tge sp e m le a2 v2 -> eval_binop op v1 v2 m = Some v -> - exists v', eval_expr tge sp e m le (sel_binop op a1 a2) v' /\ Val.lessdef v v'. + exists v', eval_expr tge sp e m le (sel_binop hf op a1 a2) v' /\ Val.lessdef v v'. Proof. destruct op; simpl; intros; FuncInv; try subst v. apply eval_add; auto. @@ -552,7 +552,7 @@ Lemma sel_expr_correct: Cminor.eval_expr ge sp e m a v -> forall e' le m', env_lessdef e e' -> Mem.extends m m' -> - exists v', eval_expr tge sp e' m' le (sel_expr a) v' /\ Val.lessdef v v'. + exists v', eval_expr tge sp e' m' le (sel_expr hf a) v' /\ Val.lessdef v v'. Proof. induction 1; intros; simpl. (* Evar *) @@ -589,7 +589,7 @@ Lemma sel_exprlist_correct: Cminor.eval_exprlist ge sp e m a v -> forall e' le m', env_lessdef e e' -> Mem.extends m m' -> - exists v', eval_exprlist tge sp e' m' le (sel_exprlist a) v' /\ Val.lessdef_list v v'. + exists v', eval_exprlist tge sp e' m' le (sel_exprlist hf a) v' /\ Val.lessdef_list v v'. Proof. induction 1; intros; simpl. exists (@nil val); split; auto. constructor. @@ -603,13 +603,13 @@ Lemma sel_builtin_arg_correct: env_lessdef e e' -> Mem.extends m m' -> Cminor.eval_expr ge sp e m a v -> exists v', - CminorSel.eval_builtin_arg tge sp e' m' (sel_builtin_arg a c) v' + CminorSel.eval_builtin_arg tge sp e' m' (sel_builtin_arg hf a c) v' /\ Val.lessdef v v'. Proof. intros. unfold sel_builtin_arg. exploit sel_expr_correct; eauto. intros (v1 & A & B). exists v1; split; auto. - destruct (builtin_arg_ok (builtin_arg (sel_expr a)) c). + destruct (builtin_arg_ok (builtin_arg (sel_expr hf a)) c). apply eval_builtin_arg; eauto. constructor; auto. Qed. @@ -622,7 +622,7 @@ Lemma sel_builtin_args_correct: forall cl, exists vl', list_forall2 (CminorSel.eval_builtin_arg tge sp e' m') - (sel_builtin_args al cl) + (sel_builtin_args hf al cl) vl' /\ Val.lessdef_list vl vl'. Proof. @@ -647,21 +647,21 @@ Inductive match_cont: Cminor.cont -> CminorSel.cont -> Prop := | match_cont_stop: match_cont Cminor.Kstop Kstop | match_cont_seq: forall s s' k k', - sel_stmt ge s = OK s' -> + sel_stmt hf ge s = OK s' -> match_cont k k' -> match_cont (Cminor.Kseq s k) (Kseq s' k') | match_cont_block: forall k k', match_cont k k' -> match_cont (Cminor.Kblock k) (Kblock k') | match_cont_call: forall id f sp e k f' e' k', - sel_function ge f = OK f' -> + sel_function hf ge f = OK f' -> match_cont k k' -> env_lessdef e e' -> match_cont (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k'). Inductive match_states: Cminor.state -> CminorSel.state -> Prop := | match_state: forall f f' s k s' k' sp e m e' m' - (TF: sel_function ge f = OK f') - (TS: sel_stmt ge s = OK s') + (TF: sel_function hf ge f = OK f') + (TS: sel_stmt hf ge s = OK s') (MC: match_cont k k') (LD: env_lessdef e e') (ME: Mem.extends m m'), @@ -669,7 +669,7 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (Cminor.State f s k sp e m) (State f' s' k' sp e' m') | match_callstate: forall f f' args args' k k' m m' - (TF: sel_fundef ge f = OK f') + (TF: sel_fundef hf ge f = OK f') (MC: match_cont k k') (LD: Val.lessdef_list args args') (ME: Mem.extends m m'), @@ -684,7 +684,7 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (Cminor.Returnstate v k m) (Returnstate v' k' m') | match_builtin_1: forall ef args args' optid f sp e k m al f' e' k' m' - (TF: sel_function ge f = OK f') + (TF: sel_function hf ge f = OK f') (MC: match_cont k k') (LDA: Val.lessdef_list args args') (LDE: env_lessdef e e') @@ -694,7 +694,7 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m) (State f' (Sbuiltin (sel_builtin_res optid) ef al) k' sp e' m') | match_builtin_2: forall v v' optid f sp e k m f' e' m' k' - (TF: sel_function ge f = OK f') + (TF: sel_function hf ge f = OK f') (MC: match_cont k k') (LDV: Val.lessdef v v') (LDE: env_lessdef e e') @@ -712,16 +712,16 @@ Qed. Remark find_label_commut: forall lbl s k s' k', match_cont k k' -> - sel_stmt ge s = OK s' -> + sel_stmt hf ge s = OK s' -> match Cminor.find_label lbl s k, find_label lbl s' k' with | None, None => True - | Some(s1, k1), Some(s1', k1') => sel_stmt ge s1 = OK s1' /\ match_cont k1 k1' + | Some(s1, k1), Some(s1', k1') => sel_stmt hf ge s1 = OK s1' /\ match_cont k1 k1' | _, _ => False end. Proof. induction s; intros until k'; simpl; intros MC SE; try (monadInv SE); simpl; auto. (* store *) - unfold store. destruct (addressing m (sel_expr e)); simpl; auto. + unfold store. destruct (addressing m (sel_expr hf e)); simpl; auto. (* call *) destruct (classify_call ge e); simpl; auto. (* tailcall *) @@ -886,7 +886,7 @@ Proof. - (* Slabel *) left; econstructor; split. constructor. constructor; auto. - (* Sgoto *) - assert (sel_stmt ge (Cminor.fn_body f) = OK (fn_body f')). + assert (sel_stmt hf ge (Cminor.fn_body f) = OK (fn_body f')). { monadInv TF; simpl; auto. } exploit (find_label_commut lbl (Cminor.fn_body f) (Cminor.call_cont k)). apply call_cont_commut; eauto. eauto. @@ -954,39 +954,97 @@ Qed. End PRESERVATION. -Lemma check_helper_correct: - forall ge name sg res, - check_helper ge (name, sg) = OK res -> helper_declared ge name sg. -Proof with (try discriminate). - unfold check_helper; intros. - destruct (Genv.find_symbol ge name) as [b|] eqn:FS... - destruct (Genv.find_funct_ptr ge b) as [fd|] eqn:FP... - destruct fd... destruct e... destruct (ident_eq name0 name)... - destruct (signature_eq sg0 sg)... - subst. exists b; auto. +(** Processing of helper functions *) + +Lemma record_globdefs_sound: + forall p id fd, + (record_globdefs p)!id = Some (Gfun fd) -> + exists b, Genv.find_symbol (Genv.globalenv p) id = Some b + /\ Genv.find_funct_ptr (Genv.globalenv p) b = Some fd. +Proof. + intros until fd. + set (P := fun (m: PTree.t globdef) (ge: Genv.t Cminor.fundef unit) => + m!id = Some (Gfun fd) -> + exists b, Genv.find_symbol ge id = Some b + /\ Genv.find_funct_ptr ge b = Some fd). + assert (REC: forall gl m ge, + P m ge -> + P (fold_left record_globdef gl m) (Genv.add_globals ge gl)). + { + induction gl; simpl; intros. + - auto. + - apply IHgl. red. destruct a as [id1 gd1]; simpl; intros. + unfold Genv.find_symbol; simpl. rewrite PTree.gsspec. destruct (peq id id1). + + subst id1. exists (Genv.genv_next ge); split; auto. + replace gd1 with (@Gfun Cminor.fundef unit fd). + unfold Genv.find_funct_ptr; simpl. apply PTree.gss. + destruct (globdef_of_interest gd1). + rewrite PTree.gss in H0; congruence. + rewrite PTree.grs in H0; congruence. + + assert (m!id = Some (Gfun fd)). + { destruct (globdef_of_interest gd1). + rewrite PTree.gso in H0; auto. + rewrite PTree.gro in H0; auto. } + exploit H; eauto. intros (b & A & B). + exists b; split; auto. unfold Genv.find_funct_ptr; simpl. + destruct gd1; auto. rewrite PTree.gso; auto. + apply Plt_ne. eapply Genv.genv_symb_range; eauto. + } + eapply REC. red; intros. rewrite PTree.gempty in H; discriminate. +Qed. + +Lemma lookup_helper_correct_1: + forall globs name sg id, + lookup_helper globs name sg = OK id -> + globs!id = Some (Gfun (External (EF_external name sg))). +Proof. + intros. + set (P := fun (m: PTree.t globdef) res => res = Some id -> m!id = Some(Gfun(External (EF_external name sg)))). + assert (P globs (PTree.fold (lookup_helper_aux name sg) globs None)). + { apply PTree_Properties.fold_rec; red; intros. + - rewrite <- H0. apply H1; auto. + - discriminate. + - assert (EITHER: k = id /\ v = Gfun (External (EF_external name sg)) + \/ a = Some id). + { unfold lookup_helper_aux in H3. destruct v; auto. destruct f; auto. destruct e; auto. + destruct (String.string_dec name name0); auto. + destruct (signature_eq sg sg0); auto. + inversion H3. left; split; auto. repeat f_equal; auto. } + destruct EITHER as [[X Y] | X]. + subst k v. apply PTree.gss. + apply H2 in X. rewrite PTree.gso by congruence. auto. + } + red in H0. unfold lookup_helper in H. + destruct (PTree.fold (lookup_helper_aux name sg) globs None); inv H. auto. Qed. -Lemma check_helpers_correct: - forall ge res, check_helpers ge = OK res -> - forall name sg, In (name, sg) i64_helpers -> helper_declared ge name sg. +Lemma lookup_helper_correct: + forall p name sg id, + lookup_helper (record_globdefs p) name sg = OK id -> + helper_declared (Genv.globalenv p) id name sg. Proof. - unfold check_helpers; intros ge res CH name sg. - monadInv CH. generalize (mmap_inversion _ _ EQ). - generalize i64_helpers x. induction 1; simpl; intros. - contradiction. - destruct H1. subst a1. eapply check_helper_correct; eauto. eauto. + intros. apply lookup_helper_correct_1 in H. apply record_globdefs_sound in H. auto. Qed. +Theorem get_helpers_correct: + forall p hf, + get_helpers p = OK hf -> helper_functions_declared (Genv.globalenv p) hf. +Proof. + intros. monadInv H. red; simpl. auto 20 using lookup_helper_correct. +Qed. + +(** All together *) + Theorem transf_program_correct: forall prog tprog, sel_program prog = OK tprog -> forward_simulation (Cminor.semantics prog) (CminorSel.semantics tprog). Proof. - intros. unfold sel_program in H. set (ge := Genv.globalenv prog) in *. - destruct (check_helpers ge) eqn:CH; simpl in H; try discriminate. - apply forward_simulation_opt with (match_states := match_states prog tprog) (measure := measure). + intros. unfold sel_program in H. + destruct (get_helpers prog) as [hf|] eqn:G; simpl in H; try discriminate. + apply forward_simulation_opt with (match_states := match_states prog tprog hf) (measure := measure). eapply public_preserved; eauto. apply sel_initial_states; auto. apply sel_final_states; auto. - apply sel_step_correct; auto. eapply check_helpers_correct; eauto. + apply sel_step_correct; auto. eapply get_helpers_correct; eauto. Qed. |