diff options
Diffstat (limited to 'backend/SplitLongproof.v')
| -rw-r--r-- | backend/SplitLongproof.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index 18c1f18d..df77b322 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -16,11 +16,15 @@ Require Import String. Require Import Coqlib Maps. Require Import AST Errors Integers Floats. Require Import Values Memory Globalenvs Builtins Events Cminor Op CminorSel. +Require Import OpHelpers OpHelpersproof. +Require Import Values Memory Globalenvs Builtins Events Cminor Op CminorSel. Require Import SelectOp SelectOpproof SplitLong. Local Open Scope cminorsel_scope. Local Open Scope string_scope. +<<<<<<< HEAD +======= (** * Properties of the helper functions *) Definition helper_declared {F V: Type} (p: AST.program (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop := @@ -43,6 +47,7 @@ Definition helper_functions_declared {F V: Type} (p: AST.program (AST.fundef F) /\ helper_declared p i64_umulh "__compcert_i64_umulh" sig_ll_l /\ helper_declared p i64_smulh "__compcert_i64_smulh" sig_ll_l. +>>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf (** * Correctness of the instruction selection functions for 64-bit operators *) Section CMCONSTR. @@ -55,6 +60,10 @@ Variable sp: val. Variable e: env. Variable m: mem. +<<<<<<< HEAD +Ltac UseHelper := decompose [Logic.and] arith_helpers_correct; eauto. +======= +>>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto. Lemma eval_helper: @@ -342,7 +351,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. |