From 7bd5d66520bfae2bdef6573a40798a5d6375be79 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Wed, 20 Mar 2019 11:30:21 +0100
Subject: Proving eval_divs_base

---
 mppa_k1c/SelectOpproof.v | 53 ++++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 47 insertions(+), 6 deletions(-)

(limited to 'mppa_k1c')

diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 88eeada8..1626e3fe 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]
@@ -614,7 +653,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,
-- 
cgit