diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-20 11:30:49 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-20 11:30:49 +0100 |
commit | c10a470bf10e0f1caf0df9d8491ae01464146b55 (patch) | |
tree | fee0729c08881b3997e558345e05e0c17aa66362 | |
parent | 37e78559ccf9b1db585442ff0b8ca4cf2d613386 (diff) | |
parent | 7bd5d66520bfae2bdef6573a40798a5d6375be79 (diff) | |
download | compcert-kvx-c10a470bf10e0f1caf0df9d8491ae01464146b55.tar.gz compcert-kvx-c10a470bf10e0f1caf0df9d8491ae01464146b55.zip |
Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-mul
-rw-r--r-- | backend/SelectDivproof.v | 2 | ||||
-rw-r--r-- | backend/SplitLongproof.v | 2 | ||||
-rw-r--r-- | mppa_k1c/SelectOpproof.v | 53 |
3 files changed, 49 insertions, 8 deletions
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index 3fd50b76..9b99fcbf 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -702,7 +702,7 @@ Proof. || Int.eq i (Int.repr Int.min_signed) && Int.eq n2 Int.mone) eqn:Z2; inv DIV. destruct (Int.is_power2 n2) as [l | ] eqn:P2. - destruct (Int.ltu l (Int.repr 31)) eqn:LT31. - + exploit (eval_shrximm ge sp e m (Vint i :: le) (Eletvar O)). + + exploit (eval_shrximm prog sp e m (Vint i :: le) (Eletvar O)). constructor. simpl; eauto. eapply Val.divs_pow2; eauto. intros [v1 [X LD]]. inv LD. econstructor; split. econstructor. eauto. diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index 3b74b216..a74276c7 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -313,7 +313,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. diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index c6fbef6b..5a3f4521 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -65,10 +65,10 @@ Axiom i64_helpers_correct : /\ (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)) - /\ (forall x y z, Val.divls x y = Some z -> external_implements "__compcert_i32_sdiv" sig_ii_i (x::y::nil) z) - /\ (forall x y z, Val.divlu x y = Some z -> external_implements "__compcert_i32_udiv" sig_ii_i (x::y::nil) z) - /\ (forall x y z, Val.modls x y = Some z -> external_implements "__compcert_i32_smod" sig_ii_i (x::y::nil) z) - /\ (forall x y z, Val.modlu x y = Some z -> external_implements "__compcert_i32_umod" sig_ii_i (x::y::nil) z) + /\ (forall x y z, Val.divs x y = Some z -> external_implements "__compcert_i32_sdiv" sig_ii_i (x::y::nil) z) + /\ (forall x y z, Val.divu x y = Some z -> external_implements "__compcert_i32_udiv" sig_ii_i (x::y::nil) z) + /\ (forall x y z, Val.mods x y = Some z -> external_implements "__compcert_i32_smod" sig_ii_i (x::y::nil) z) + /\ (forall x y z, Val.modu x y = Some z -> external_implements "__compcert_i32_umod" sig_ii_i (x::y::nil) z) . Definition helper_declared {F V: Type} (p: AST.program (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop := @@ -146,11 +146,50 @@ Section CMCONSTR. Variable prog: program. Variable hf: helper_functions. Hypothesis HELPERS: helper_functions_declared prog hf. -Variable ge: genv. +Let ge := Genv.globalenv prog. Variable sp: val. Variable e: env. Variable m: mem. +(* Helper lemmas - from SplitLongproof.v *) + +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 name sg args vargs vres, + eval_exprlist ge sp e m le args vargs -> + 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. + 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 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. + intros. eapply eval_helper; eauto. constructor; auto. constructor. +Qed. + +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 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. + intros. eapply eval_helper; eauto. constructor; auto. constructor; auto. constructor. +Qed. + (** We now show that the code generated by "smart constructor" functions such as [Selection.notint] behaves as expected. Continuing the [notint] example, we show that if the expression [e] @@ -622,7 +661,9 @@ Theorem eval_divs_base: Val.divs x y = Some z -> exists v, eval_expr ge sp e m le (divs_base a b) v /\ Val.lessdef z v. Proof. -Admitted. + intros; unfold divs_base. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. +Qed. Theorem eval_mods_base: forall le a b x y z, |