Proving eval_divs_base

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 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,