diff options
Diffstat (limited to 'backend/SelectLongproof.v')
| -rw-r--r-- | backend/SelectLongproof.v | 56 |
1 files changed, 30 insertions, 26 deletions
diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v index 35d53215..f15015e8 100644 --- a/backend/SelectLongproof.v +++ b/backend/SelectLongproof.v @@ -14,6 +14,7 @@ Require Import String. Require Import Coqlib. +Require Import Maps. Require Import AST. Require Import Errors. Require Import Integers. @@ -36,7 +37,7 @@ Open Local Scope string_scope. 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 name sg) ge vargs m E0 vres m. + external_call (EF_runtime name sg) ge vargs m E0 vres m. Definition builtin_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop := forall F V (ge: Genv.t F V) m, @@ -61,32 +62,32 @@ Axiom i64_helpers_correct : /\ (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. +Definition helper_declared {F V: Type} (p: AST.program (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop := + (prog_defmap p)!id = Some (Gfun (External (EF_runtime name sg))). + +Definition helper_functions_declared {F V: Type} (p: AST.program (AST.fundef F) V) (hf: helper_functions) : Prop := + helper_declared p hf.(i64_dtos) "__i64_dtos" sig_f_l + /\ helper_declared p hf.(i64_dtou) "__i64_dtou" sig_f_l + /\ helper_declared p hf.(i64_stod) "__i64_stod" sig_l_f + /\ helper_declared p hf.(i64_utod) "__i64_utod" sig_l_f + /\ helper_declared p hf.(i64_stof) "__i64_stof" sig_l_s + /\ helper_declared p hf.(i64_utof) "__i64_utof" sig_l_s + /\ helper_declared p hf.(i64_sdiv) "__i64_sdiv" sig_ll_l + /\ helper_declared p hf.(i64_udiv) "__i64_udiv" sig_ll_l + /\ helper_declared p hf.(i64_smod) "__i64_smod" sig_ll_l + /\ helper_declared p hf.(i64_umod) "__i64_umod" sig_ll_l + /\ helper_declared p hf.(i64_shl) "__i64_shl" sig_li_l + /\ helper_declared p hf.(i64_shr) "__i64_shr" sig_li_l + /\ helper_declared p hf.(i64_sar) "__i64_sar" sig_li_l. (** * Correctness of the instruction selection functions for 64-bit operators *) Section CMCONSTR. -Variable ge: genv. +Variable prog: program. Variable hf: helper_functions. -Hypothesis HELPERS: helper_functions_declared ge hf. +Hypothesis HELPERS: helper_functions_declared prog hf. +Let ge := Genv.globalenv prog. Variable sp: val. Variable e: env. Variable m: mem. @@ -97,17 +98,20 @@ Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto. Lemma eval_helper: forall le id name sg args vargs vres, eval_exprlist ge sp e m le args vargs -> - helper_declared ge id name sg -> + helper_declared prog id name sg -> external_implements name sg vargs vres -> eval_expr ge sp e m le (Eexternal id sg args) vres. Proof. - intros. destruct H0 as (b & P & Q). econstructor; eauto. + intros. + red in H0. apply Genv.find_def_symbol in H0. destruct H0 as (b & P & Q). + rewrite <- Genv.find_funct_ptr_iff in Q. + econstructor; eauto. Qed. Corollary eval_helper_1: forall le id name sg arg1 varg1 vres, eval_expr ge sp e m le arg1 varg1 -> - helper_declared ge id name sg -> + helper_declared prog id name sg -> external_implements name sg (varg1::nil) vres -> eval_expr ge sp e m le (Eexternal id sg (arg1 ::: Enil)) vres. Proof. @@ -118,7 +122,7 @@ Corollary eval_helper_2: 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 -> - helper_declared ge id name sg -> + helper_declared prog 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. @@ -845,7 +849,7 @@ Qed. Lemma eval_binop_long: forall id name sem le a b x y z, (forall p q, x = Vlong p -> y = Vlong q -> z = Vlong (sem p q)) -> - helper_declared ge id name sig_ll_l -> + helper_declared prog 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 -> |