diff options
Diffstat (limited to 'backend/SplitLongproof.v')
| -rw-r--r-- | backend/SplitLongproof.v | 56 |
1 files changed, 3 insertions, 53 deletions
diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index f1e8b590..6718ba5b 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -16,62 +16,12 @@ Require Import String. Require Import Coqlib Maps. Require Import AST Errors Integers Floats. Require Import Values Memory Globalenvs Events Cminor Op CminorSel. +Require Import OpHelpers OpHelpersproof. Require Import SelectOp SelectOpproof SplitLong. Local Open Scope cminorsel_scope. Local Open Scope string_scope. -(** * Axiomatization of the helper functions *) - -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_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, - 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 "__compcert_i64_dtos" sig_f_l (x::nil) z) - /\ (forall x z, Val.longuoffloat x = Some z -> external_implements "__compcert_i64_dtou" sig_f_l (x::nil) z) - /\ (forall x z, Val.floatoflong x = Some z -> external_implements "__compcert_i64_stod" sig_l_f (x::nil) z) - /\ (forall x z, Val.floatoflongu x = Some z -> external_implements "__compcert_i64_utod" sig_l_f (x::nil) z) - /\ (forall x z, Val.singleoflong x = Some z -> external_implements "__compcert_i64_stof" sig_l_s (x::nil) z) - /\ (forall x z, Val.singleoflongu x = Some z -> external_implements "__compcert_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 "__compcert_i64_sdiv" sig_ll_l (x::y::nil) z) - /\ (forall x y z, Val.divlu x y = Some z -> external_implements "__compcert_i64_udiv" sig_ll_l (x::y::nil) z) - /\ (forall x y z, Val.modls x y = Some z -> external_implements "__compcert_i64_smod" sig_ll_l (x::y::nil) z) - /\ (forall x y z, Val.modlu x y = Some z -> external_implements "__compcert_i64_umod" sig_ll_l (x::y::nil) z) - /\ (forall x y, external_implements "__compcert_i64_shl" sig_li_l (x::y::nil) (Val.shll x y)) - /\ (forall x y, external_implements "__compcert_i64_shr" sig_li_l (x::y::nil) (Val.shrlu x y)) - /\ (forall x y, external_implements "__compcert_i64_sar" sig_li_l (x::y::nil) (Val.shrl x y)) - /\ (forall x y, external_implements "__compcert_i64_umulh" sig_ll_l (x::y::nil) (Val.mullhu x y)) - /\ (forall x y, external_implements "__compcert_i64_smulh" sig_ll_l (x::y::nil) (Val.mullhs x y)). - -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 i64_dtos "__compcert_i64_dtos" sig_f_l - /\ helper_declared p i64_dtou "__compcert_i64_dtou" sig_f_l - /\ helper_declared p i64_stod "__compcert_i64_stod" sig_l_f - /\ helper_declared p i64_utod "__compcert_i64_utod" sig_l_f - /\ helper_declared p i64_stof "__compcert_i64_stof" sig_l_s - /\ helper_declared p i64_utof "__compcert_i64_utof" sig_l_s - /\ helper_declared p i64_sdiv "__compcert_i64_sdiv" sig_ll_l - /\ helper_declared p i64_udiv "__compcert_i64_udiv" sig_ll_l - /\ helper_declared p i64_smod "__compcert_i64_smod" sig_ll_l - /\ helper_declared p i64_umod "__compcert_i64_umod" sig_ll_l - /\ helper_declared p i64_shl "__compcert_i64_shl" sig_li_l - /\ helper_declared p i64_shr "__compcert_i64_shr" sig_li_l - /\ helper_declared p i64_sar "__compcert_i64_sar" sig_li_l - /\ helper_declared p i64_umulh "__compcert_i64_umulh" sig_ll_l - /\ helper_declared p i64_smulh "__compcert_i64_smulh" sig_ll_l. - (** * Correctness of the instruction selection functions for 64-bit operators *) Section CMCONSTR. @@ -84,7 +34,7 @@ Variable sp: val. Variable e: env. Variable m: mem. -Ltac UseHelper := decompose [Logic.and] i64_helpers_correct; eauto. +Ltac UseHelper := decompose [Logic.and] arith_helpers_correct; eauto. Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto. Lemma eval_helper: @@ -364,7 +314,7 @@ Theorem eval_longofint: unary_constructor_sound longofint Val.longofint. Proof. red; intros. unfold longofint. destruct (longofint_match a). - InvEval. econstructor; split. apply eval_longconst. auto. -- exploit (eval_shrimm ge sp e m (Int.repr 31) (x :: le) (Eletvar 0)). EvalOp. +- exploit (eval_shrimm prog sp e m (Int.repr 31) (x :: le) (Eletvar 0)). EvalOp. intros [v1 [A B]]. econstructor; split. EvalOp. destruct x; simpl; auto. |