aboutsummaryrefslogtreecommitdiffstats
path: root/backend/SelectLongproof.v
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2016-10-01 17:25:18 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2016-10-01 17:25:18 +0200
commite637d041c5c2ee3a3ed395a7dab6c9101e8eb16c (patch)
tree518d558674d3e1c6ff41c46d84c784e727ed5d04 /backend/SelectLongproof.v
parentad2a2c862abef3aee701d1bca0524fcbf2d07b30 (diff)
downloadcompcert-e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c.tar.gz
compcert-e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c.zip
Support for 64-bit architectures: generic support
- Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
Diffstat (limited to 'backend/SelectLongproof.v')
-rw-r--r--backend/SelectLongproof.v1174
1 files changed, 0 insertions, 1174 deletions
diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v
deleted file mode 100644
index f15015e8..00000000
--- a/backend/SelectLongproof.v
+++ /dev/null
@@ -1,1174 +0,0 @@
-(* *********************************************************************)
-(* *)
-(* The Compcert verified compiler *)
-(* *)
-(* Xavier Leroy, INRIA Paris-Rocquencourt *)
-(* *)
-(* Copyright Institut National de Recherche en Informatique et en *)
-(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
-(* *)
-(* *********************************************************************)
-
-(** Correctness of instruction selection for integer division *)
-
-Require Import String.
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Errors.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Events.
-Require Import Cminor.
-Require Import Op.
-Require Import CminorSel.
-Require Import SelectOp.
-Require Import SelectOpproof.
-Require Import SelectLong.
-
-Open Local Scope cminorsel_scope.
-Open Local 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 "__i64_dtos" sig_f_l (x::nil) z)
- /\ (forall x z, Val.longuoffloat x = Some z -> external_implements "__i64_dtou" sig_f_l (x::nil) z)
- /\ (forall x z, Val.floatoflong x = Some z -> external_implements "__i64_stod" sig_l_f (x::nil) z)
- /\ (forall x z, Val.floatoflongu x = Some z -> external_implements "__i64_utod" sig_l_f (x::nil) z)
- /\ (forall x z, Val.singleoflong x = Some z -> external_implements "__i64_stof" sig_l_s (x::nil) z)
- /\ (forall x z, Val.singleoflongu x = Some z -> external_implements "__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 "__i64_sdiv" sig_ll_l (x::y::nil) z)
- /\ (forall x y z, Val.divlu x y = Some z -> external_implements "__i64_udiv" sig_ll_l (x::y::nil) z)
- /\ (forall x y z, Val.modls x y = Some z -> external_implements "__i64_smod" sig_ll_l (x::y::nil) z)
- /\ (forall x y z, Val.modlu x y = Some z -> external_implements "__i64_umod" sig_ll_l (x::y::nil) z)
- /\ (forall x y, external_implements "__i64_shl" sig_li_l (x::y::nil) (Val.shll x y))
- /\ (forall x y, external_implements "__i64_shr" sig_li_l (x::y::nil) (Val.shrlu x y))
- /\ (forall x y, external_implements "__i64_sar" sig_li_l (x::y::nil) (Val.shrl 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 hf.(i64_dtos) "__i64_dtos" sig_f_l
- /\ helper_declared p hf.(i64_dtou) "__i64_dtou" sig_f_l
- /\ helper_declared p hf.(i64_stod) "__i64_stod" sig_l_f
- /\ helper_declared p hf.(i64_utod) "__i64_utod" sig_l_f
- /\ helper_declared p hf.(i64_stof) "__i64_stof" sig_l_s
- /\ helper_declared p hf.(i64_utof) "__i64_utof" sig_l_s
- /\ helper_declared p hf.(i64_sdiv) "__i64_sdiv" sig_ll_l
- /\ helper_declared p hf.(i64_udiv) "__i64_udiv" sig_ll_l
- /\ helper_declared p hf.(i64_smod) "__i64_smod" sig_ll_l
- /\ helper_declared p hf.(i64_umod) "__i64_umod" sig_ll_l
- /\ helper_declared p hf.(i64_shl) "__i64_shl" sig_li_l
- /\ helper_declared p hf.(i64_shr) "__i64_shr" sig_li_l
- /\ helper_declared p hf.(i64_sar) "__i64_sar" sig_li_l.
-
-(** * Correctness of the instruction selection functions for 64-bit operators *)
-
-Section CMCONSTR.
-
-Variable prog: program.
-Variable hf: helper_functions.
-Hypothesis HELPERS: helper_functions_declared prog hf.
-Let ge := Genv.globalenv prog.
-Variable sp: val.
-Variable e: env.
-Variable m: mem.
-
-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.
-
-Remark eval_builtin_1:
- forall le id sg arg1 varg1 vres,
- eval_expr ge sp e m le arg1 varg1 ->
- builtin_implements id sg (varg1::nil) vres ->
- eval_expr ge sp e m le (Ebuiltin (EF_builtin id sg) (arg1 ::: Enil)) vres.
-Proof.
- intros. econstructor. econstructor. eauto. constructor. apply H0.
-Qed.
-
-Remark eval_builtin_2:
- forall le id sg arg1 arg2 varg1 varg2 vres,
- eval_expr ge sp e m le arg1 varg1 ->
- eval_expr ge sp e m le arg2 varg2 ->
- builtin_implements id sg (varg1::varg2::nil) vres ->
- eval_expr ge sp e m le (Ebuiltin (EF_builtin id sg) (arg1 ::: arg2 ::: Enil)) vres.
-Proof.
- intros. econstructor. constructor; eauto. constructor; eauto. constructor. apply H1.
-Qed.
-
-Definition unary_constructor_sound (cstr: expr -> expr) (sem: val -> val) : Prop :=
- forall le a x,
- eval_expr ge sp e m le a x ->
- exists v, eval_expr ge sp e m le (cstr a) v /\ Val.lessdef (sem x) v.
-
-Definition binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> val -> val) : Prop :=
- forall le a x b y,
- eval_expr ge sp e m le a x ->
- eval_expr ge sp e m le b y ->
- exists v, eval_expr ge sp e m le (cstr a b) v /\ Val.lessdef (sem x y) v.
-
-Ltac EvalOp :=
- eauto;
- match goal with
- | [ |- eval_exprlist _ _ _ _ _ Enil _ ] => constructor
- | [ |- eval_exprlist _ _ _ _ _ (_:::_) _ ] => econstructor; EvalOp
- | [ |- eval_expr _ _ _ _ _ (Eletvar _) _ ] => constructor; simpl; eauto
- | [ |- eval_expr _ _ _ _ _ (Elet _ _) _ ] => econstructor; EvalOp
- | [ |- eval_expr _ _ _ _ _ (lift _) _ ] => apply eval_lift; EvalOp
- | [ |- eval_expr _ _ _ _ _ _ _ ] => eapply eval_Eop; [EvalOp | simpl; eauto]
- | _ => idtac
- end.
-
-Lemma eval_splitlong:
- forall le a f v sem,
- (forall le a b x y,
- eval_expr ge sp e m le a x ->
- eval_expr ge sp e m le b y ->
- exists v, eval_expr ge sp e m le (f a b) v /\
- (forall p q, x = Vint p -> y = Vint q -> v = sem (Vlong (Int64.ofwords p q)))) ->
- match v with Vlong _ => True | _ => sem v = Vundef end ->
- eval_expr ge sp e m le a v ->
- exists v', eval_expr ge sp e m le (splitlong a f) v' /\ Val.lessdef (sem v) v'.
-Proof.
- intros until sem; intros EXEC UNDEF.
- unfold splitlong. case (splitlong_match a); intros.
-- InvEval. subst v.
- exploit EXEC. eexact H2. eexact H3. intros [v' [A B]].
- exists v'; split. auto.
- destruct v1; simpl in *; try (rewrite UNDEF; auto).
- destruct v0; simpl in *; try (rewrite UNDEF; auto).
- erewrite B; eauto.
-- exploit (EXEC (v :: le) (Eop Ohighlong (Eletvar 0 ::: Enil)) (Eop Olowlong (Eletvar 0 ::: Enil))).
- EvalOp. EvalOp.
- intros [v' [A B]].
- exists v'; split. econstructor; eauto.
- destruct v; try (rewrite UNDEF; auto). erewrite B; simpl; eauto. rewrite Int64.ofwords_recompose. auto.
-Qed.
-
-Lemma eval_splitlong_strict:
- forall le a f va v,
- eval_expr ge sp e m le a (Vlong va) ->
- (forall le a1 a2,
- eval_expr ge sp e m le a1 (Vint (Int64.hiword va)) ->
- eval_expr ge sp e m le a2 (Vint (Int64.loword va)) ->
- eval_expr ge sp e m le (f a1 a2) v) ->
- eval_expr ge sp e m le (splitlong a f) v.
-Proof.
- intros until v.
- unfold splitlong. case (splitlong_match a); intros.
-- InvEval. destruct v1; simpl in H; try discriminate. destruct v0; inv H.
- apply H0. rewrite Int64.hi_ofwords; auto. rewrite Int64.lo_ofwords; auto.
-- EvalOp. apply H0; EvalOp.
-Qed.
-
-Lemma eval_splitlong2:
- forall le a b f va vb sem,
- (forall le a1 a2 b1 b2 x1 x2 y1 y2,
- eval_expr ge sp e m le a1 x1 ->
- eval_expr ge sp e m le a2 x2 ->
- eval_expr ge sp e m le b1 y1 ->
- eval_expr ge sp e m le b2 y2 ->
- exists v,
- eval_expr ge sp e m le (f a1 a2 b1 b2) v /\
- (forall p1 p2 q1 q2,
- x1 = Vint p1 -> x2 = Vint p2 -> y1 = Vint q1 -> y2 = Vint q2 ->
- v = sem (Vlong (Int64.ofwords p1 p2)) (Vlong (Int64.ofwords q1 q2)))) ->
- match va, vb with Vlong _, Vlong _ => True | _, _ => sem va vb = Vundef end ->
- eval_expr ge sp e m le a va ->
- eval_expr ge sp e m le b vb ->
- exists v, eval_expr ge sp e m le (splitlong2 a b f) v /\ Val.lessdef (sem va vb) v.
-Proof.
- intros until sem; intros EXEC UNDEF.
- unfold splitlong2. case (splitlong2_match a b); intros.
-- InvEval. subst va vb.
- exploit (EXEC le h1 l1 h2 l2); eauto. intros [v [A B]].
- exists v; split; auto.
- destruct v1; simpl in *; try (rewrite UNDEF; auto).
- destruct v0; try (rewrite UNDEF; auto).
- destruct v2; simpl in *; try (rewrite UNDEF; auto).
- destruct v3; try (rewrite UNDEF; auto).
- erewrite B; eauto.
-- InvEval. subst va.
- exploit (EXEC (vb :: le) (lift h1) (lift l1)
- (Eop Ohighlong (Eletvar 0 ::: Enil)) (Eop Olowlong (Eletvar 0 ::: Enil))).
- EvalOp. EvalOp. EvalOp. EvalOp.
- intros [v [A B]].
- exists v; split.
- econstructor; eauto.
- destruct v1; simpl in *; try (rewrite UNDEF; auto).
- destruct v0; try (rewrite UNDEF; auto).
- destruct vb; try (rewrite UNDEF; auto).
- erewrite B; simpl; eauto. rewrite Int64.ofwords_recompose. auto.
-- InvEval. subst vb.
- exploit (EXEC (va :: le)
- (Eop Ohighlong (Eletvar 0 ::: Enil)) (Eop Olowlong (Eletvar 0 ::: Enil))
- (lift h2) (lift l2)).
- EvalOp. EvalOp. EvalOp. EvalOp.
- intros [v [A B]].
- exists v; split.
- econstructor; eauto.
- destruct va; try (rewrite UNDEF; auto).
- destruct v1; simpl in *; try (rewrite UNDEF; auto).
- destruct v0; try (rewrite UNDEF; auto).
- erewrite B; simpl; eauto. rewrite Int64.ofwords_recompose. auto.
-- exploit (EXEC (vb :: va :: le)
- (Eop Ohighlong (Eletvar 1 ::: Enil)) (Eop Olowlong (Eletvar 1 ::: Enil))
- (Eop Ohighlong (Eletvar 0 ::: Enil)) (Eop Olowlong (Eletvar 0 ::: Enil))).
- EvalOp. EvalOp. EvalOp. EvalOp.
- intros [v [A B]].
- exists v; split. EvalOp.
- destruct va; try (rewrite UNDEF; auto); destruct vb; try (rewrite UNDEF; auto).
- erewrite B; simpl; eauto. rewrite ! Int64.ofwords_recompose; auto.
-Qed.
-
-Lemma eval_splitlong2_strict:
- forall le a b f va vb v,
- eval_expr ge sp e m le a (Vlong va) ->
- eval_expr ge sp e m le b (Vlong vb) ->
- (forall le a1 a2 b1 b2,
- eval_expr ge sp e m le a1 (Vint (Int64.hiword va)) ->
- eval_expr ge sp e m le a2 (Vint (Int64.loword va)) ->
- eval_expr ge sp e m le b1 (Vint (Int64.hiword vb)) ->
- eval_expr ge sp e m le b2 (Vint (Int64.loword vb)) ->
- eval_expr ge sp e m le (f a1 a2 b1 b2) v) ->
- eval_expr ge sp e m le (splitlong2 a b f) v.
-Proof.
- assert (INV: forall v1 v2 n,
- Val.longofwords v1 v2 = Vlong n -> v1 = Vint(Int64.hiword n) /\ v2 = Vint(Int64.loword n)).
- {
- intros. destruct v1; simpl in H; try discriminate. destruct v2; inv H.
- rewrite Int64.hi_ofwords; rewrite Int64.lo_ofwords; auto.
- }
- intros until v.
- unfold splitlong2. case (splitlong2_match a b); intros.
-- InvEval. exploit INV. eexact H. intros [EQ1 EQ2]. exploit INV. eexact H0. intros [EQ3 EQ4].
- subst. auto.
-- InvEval. exploit INV; eauto. intros [EQ1 EQ2]. subst.
- econstructor. eauto. apply H1; EvalOp.
-- InvEval. exploit INV; eauto. intros [EQ1 EQ2]. subst.
- econstructor. eauto. apply H1; EvalOp.
-- EvalOp. apply H1; EvalOp.
-Qed.
-
-Lemma is_longconst_sound:
- forall le a x n,
- is_longconst a = Some n ->
- eval_expr ge sp e m le a x ->
- x = Vlong n.
-Proof.
- unfold is_longconst; intros until n; intros LC.
- destruct (is_longconst_match a); intros.
- inv LC. InvEval. simpl in H5. inv H5. auto.
- discriminate.
-Qed.
-
-Lemma is_longconst_zero_sound:
- forall le a x,
- is_longconst_zero a = true ->
- eval_expr ge sp e m le a x ->
- x = Vlong Int64.zero.
-Proof.
- unfold is_longconst_zero; intros.
- destruct (is_longconst a) as [n|] eqn:E; try discriminate.
- revert H. predSpec Int64.eq Int64.eq_spec n Int64.zero.
- intros. subst. eapply is_longconst_sound; eauto.
- congruence.
-Qed.
-
-Lemma eval_lowlong: unary_constructor_sound lowlong Val.loword.
-Proof.
- unfold lowlong; red. intros until x. destruct (lowlong_match a); intros.
- InvEval. subst x. exists v0; split; auto.
- destruct v1; simpl; auto. destruct v0; simpl; auto.
- rewrite Int64.lo_ofwords. auto.
- exists (Val.loword x); split; auto. EvalOp.
-Qed.
-
-Lemma eval_highlong: unary_constructor_sound highlong Val.hiword.
-Proof.
- unfold highlong; red. intros until x. destruct (highlong_match a); intros.
- InvEval. subst x. exists v1; split; auto.
- destruct v1; simpl; auto. destruct v0; simpl; auto.
- rewrite Int64.hi_ofwords. auto.
- exists (Val.hiword x); split; auto. EvalOp.
-Qed.
-
-Lemma eval_longconst:
- forall le n, eval_expr ge sp e m le (longconst n) (Vlong n).
-Proof.
- intros. EvalOp. rewrite Int64.ofwords_recompose; auto.
-Qed.
-
-Theorem eval_intoflong: unary_constructor_sound intoflong Val.loword.
-Proof eval_lowlong.
-
-Theorem eval_longofintu: unary_constructor_sound longofintu Val.longofintu.
-Proof.
- red; intros. unfold longofintu. econstructor; split. EvalOp.
- unfold Val.longofintu. destruct x; auto.
- replace (Int64.repr (Int.unsigned i)) with (Int64.ofwords Int.zero i); auto.
- apply Int64.same_bits_eq; intros.
- rewrite Int64.testbit_repr by auto.
- rewrite Int64.bits_ofwords by auto.
- fold (Int.testbit i i0).
- destruct (zlt i0 Int.zwordsize).
- auto.
- rewrite Int.bits_zero. rewrite Int.bits_above by omega. auto.
-Qed.
-
-Theorem eval_longofint: unary_constructor_sound longofint Val.longofint.
-Proof.
- red; intros. unfold longofint.
- exploit (eval_shrimm ge sp e m (Int.repr 31) (x :: le) (Eletvar 0)). EvalOp.
- intros [v1 [A B]].
- econstructor; split. EvalOp.
- destruct x; simpl; auto.
- simpl in B. inv B. simpl.
- replace (Int64.repr (Int.signed i))
- with (Int64.ofwords (Int.shr i (Int.repr 31)) i); auto.
- apply Int64.same_bits_eq; intros.
- rewrite Int64.testbit_repr by auto.
- rewrite Int64.bits_ofwords by auto.
- rewrite Int.bits_signed by omega.
- destruct (zlt i0 Int.zwordsize).
- auto.
- assert (Int64.zwordsize = 2 * Int.zwordsize) by reflexivity.
- rewrite Int.bits_shr by omega.
- change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1).
- f_equal. destruct (zlt (i0 - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); omega.
-Qed.
-
-Theorem eval_negl: unary_constructor_sound negl Val.negl.
-Proof.
- unfold negl; red; intros. destruct (is_longconst a) eqn:E.
- econstructor; split. apply eval_longconst.
- exploit is_longconst_sound; eauto. intros EQ; subst x. simpl. auto.
- econstructor; split. eapply eval_builtin_1; eauto. UseHelper. auto.
-Qed.
-
-Theorem eval_notl: unary_constructor_sound notl Val.notl.
-Proof.
- red; intros. unfold notl. apply eval_splitlong; auto.
- intros.
- exploit eval_notint. eexact H0. intros [va [A B]].
- exploit eval_notint. eexact H1. intros [vb [C D]].
- exists (Val.longofwords va vb); split. EvalOp.
- intros; subst. simpl in *. inv B; inv D.
- simpl. unfold Int.not. rewrite <- Int64.decompose_xor. auto.
- destruct x; auto.
-Qed.
-
-Theorem eval_longoffloat:
- forall le a x y,
- eval_expr ge sp e m le a x ->
- Val.longoffloat x = Some y ->
- exists v, eval_expr ge sp e m le (longoffloat hf a) v /\ Val.lessdef y v.
-Proof.
- intros; unfold longoffloat. econstructor; split.
- eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto.
-Qed.
-
-Theorem eval_longuoffloat:
- forall le a x y,
- eval_expr ge sp e m le a x ->
- Val.longuoffloat x = Some y ->
- exists v, eval_expr ge sp e m le (longuoffloat hf a) v /\ Val.lessdef y v.
-Proof.
- intros; unfold longuoffloat. econstructor; split.
- eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto.
-Qed.
-
-Theorem eval_floatoflong:
- forall le a x y,
- eval_expr ge sp e m le a x ->
- Val.floatoflong x = Some y ->
- exists v, eval_expr ge sp e m le (floatoflong hf a) v /\ Val.lessdef y v.
-Proof.
- intros; unfold floatoflong. econstructor; split.
- eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto.
-Qed.
-
-Theorem eval_floatoflongu:
- forall le a x y,
- eval_expr ge sp e m le a x ->
- Val.floatoflongu x = Some y ->
- exists v, eval_expr ge sp e m le (floatoflongu hf a) v /\ Val.lessdef y v.
-Proof.
- intros; unfold floatoflongu. econstructor; split.
- eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto.
-Qed.
-
-Theorem eval_longofsingle:
- forall le a x y,
- eval_expr ge sp e m le a x ->
- Val.longofsingle x = Some y ->
- exists v, eval_expr ge sp e m le (longofsingle hf a) v /\ Val.lessdef y v.
-Proof.
- intros; unfold longofsingle.
- destruct x; simpl in H0; inv H0. destruct (Float32.to_long f) as [n|] eqn:EQ; simpl in H2; inv H2.
- exploit eval_floatofsingle; eauto. intros (v & A & B). simpl in B. inv B.
- apply Float32.to_long_double in EQ.
- eapply eval_longoffloat; eauto. simpl.
- change (Float.of_single f) with (Float32.to_double f); rewrite EQ; auto.
-Qed.
-
-Theorem eval_longuofsingle:
- forall le a x y,
- eval_expr ge sp e m le a x ->
- Val.longuofsingle x = Some y ->
- exists v, eval_expr ge sp e m le (longuofsingle hf a) v /\ Val.lessdef y v.
-Proof.
- intros; unfold longuofsingle.
- destruct x; simpl in H0; inv H0. destruct (Float32.to_longu f) as [n|] eqn:EQ; simpl in H2; inv H2.
- exploit eval_floatofsingle; eauto. intros (v & A & B). simpl in B. inv B.
- apply Float32.to_longu_double in EQ.
- eapply eval_longuoffloat; eauto. simpl.
- change (Float.of_single f) with (Float32.to_double f); rewrite EQ; auto.
-Qed.
-
-Theorem eval_singleoflong:
- forall le a x y,
- eval_expr ge sp e m le a x ->
- Val.singleoflong x = Some y ->
- exists v, eval_expr ge sp e m le (singleoflong hf a) v /\ Val.lessdef y v.
-Proof.
- intros; unfold singleoflong. econstructor; split.
- eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto.
-Qed.
-
-Theorem eval_singleoflongu:
- forall le a x y,
- eval_expr ge sp e m le a x ->
- Val.singleoflongu x = Some y ->
- exists v, eval_expr ge sp e m le (singleoflongu hf a) v /\ Val.lessdef y v.
-Proof.
- intros; unfold singleoflongu. econstructor; split.
- eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto.
-Qed.
-
-Theorem eval_andl: binary_constructor_sound andl Val.andl.
-Proof.
- red; intros. unfold andl. apply eval_splitlong2; auto.
- intros.
- exploit eval_and. eexact H1. eexact H3. intros [va [A B]].
- exploit eval_and. eexact H2. eexact H4. intros [vb [C D]].
- exists (Val.longofwords va vb); split. EvalOp.
- intros; subst. simpl in B; inv B. simpl in D; inv D.
- simpl. f_equal. rewrite Int64.decompose_and. auto.
- destruct x; auto. destruct y; auto.
-Qed.
-
-Theorem eval_orl: binary_constructor_sound orl Val.orl.
-Proof.
- red; intros. unfold orl. apply eval_splitlong2; auto.
- intros.
- exploit eval_or. eexact H1. eexact H3. intros [va [A B]].
- exploit eval_or. eexact H2. eexact H4. intros [vb [C D]].
- exists (Val.longofwords va vb); split. EvalOp.
- intros; subst. simpl in B; inv B. simpl in D; inv D.
- simpl. f_equal. rewrite Int64.decompose_or. auto.
- destruct x; auto. destruct y; auto.
-Qed.
-
-Theorem eval_xorl: binary_constructor_sound xorl Val.xorl.
-Proof.
- red; intros. unfold xorl. apply eval_splitlong2; auto.
- intros.
- exploit eval_xor. eexact H1. eexact H3. intros [va [A B]].
- exploit eval_xor. eexact H2. eexact H4. intros [vb [C D]].
- exists (Val.longofwords va vb); split. EvalOp.
- intros; subst. simpl in B; inv B. simpl in D; inv D.
- simpl. f_equal. rewrite Int64.decompose_xor. auto.
- destruct x; auto. destruct y; auto.
-Qed.
-
-Lemma is_intconst_sound:
- forall le a x n,
- is_intconst a = Some n ->
- eval_expr ge sp e m le a x ->
- x = Vint n.
-Proof.
- unfold is_intconst; intros until n; intros LC.
- destruct a; try discriminate. destruct o; try discriminate. destruct e0; try discriminate.
- inv LC. intros. InvEval. auto.
-Qed.
-
-Remark eval_shift_imm:
- forall (P: expr -> Prop) n a0 a1 a2 a3,
- (n = Int.zero -> P a0) ->
- (0 <= Int.unsigned n < Int.zwordsize ->
- Int.ltu n Int.iwordsize = true ->
- Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize = true ->
- Int.ltu n Int64.iwordsize' = true ->
- P a1) ->
- (Int.zwordsize <= Int.unsigned n < Int64.zwordsize ->
- Int.ltu (Int.sub n Int.iwordsize) Int.iwordsize = true ->
- P a2) ->
- P a3 ->
- P (if Int.eq n Int.zero then a0
- else if Int.ltu n Int.iwordsize then a1
- else if Int.ltu n Int64.iwordsize' then a2
- else a3).
-Proof.
- intros until a3; intros A0 A1 A2 A3.
- predSpec Int.eq Int.eq_spec n Int.zero.
- apply A0; auto.
- assert (NZ: Int.unsigned n <> 0).
- { red; intros. elim H. rewrite <- (Int.repr_unsigned n). rewrite H0. auto. }
- destruct (Int.ltu n Int.iwordsize) eqn:LT.
- exploit Int.ltu_iwordsize_inv; eauto. intros RANGE.
- assert (0 <= Int.zwordsize - Int.unsigned n < Int.zwordsize) by omega.
- apply A1. auto. auto.
- unfold Int.ltu, Int.sub. rewrite Int.unsigned_repr_wordsize.
- rewrite Int.unsigned_repr. rewrite zlt_true; auto. omega.
- generalize Int.wordsize_max_unsigned; omega.
- unfold Int.ltu. rewrite zlt_true; auto.
- change (Int.unsigned Int64.iwordsize') with 64.
- change Int.zwordsize with 32 in RANGE. omega.
- destruct (Int.ltu n Int64.iwordsize') eqn:LT'.
- exploit Int.ltu_inv; eauto.
- change (Int.unsigned Int64.iwordsize') with (Int.zwordsize * 2).
- intros RANGE.
- assert (Int.zwordsize <= Int.unsigned n).
- unfold Int.ltu in LT. rewrite Int.unsigned_repr_wordsize in LT.
- destruct (zlt (Int.unsigned n) Int.zwordsize). discriminate. omega.
- apply A2. tauto. unfold Int.ltu, Int.sub. rewrite Int.unsigned_repr_wordsize.
- rewrite Int.unsigned_repr. rewrite zlt_true; auto. omega.
- generalize Int.wordsize_max_unsigned; omega.
- auto.
-Qed.
-
-Lemma eval_shllimm:
- forall n,
- unary_constructor_sound (fun e => shllimm hf e n) (fun v => Val.shll v (Vint n)).
-Proof.
- unfold shllimm; red; intros.
- apply eval_shift_imm; intros.
- + (* n = 0 *)
- subst n. exists x; split; auto. destruct x; simpl; auto.
- change (Int64.shl' i Int.zero) with (Int64.shl i Int64.zero).
- rewrite Int64.shl_zero. auto.
- + (* 0 < n < 32 *)
- apply eval_splitlong with (sem := fun x => Val.shll x (Vint n)); auto.
- intros.
- exploit eval_shlimm. eexact H4. instantiate (1 := n). intros [v1 [A1 B1]].
- exploit eval_shlimm. eexact H5. instantiate (1 := n). intros [v2 [A2 B2]].
- exploit eval_shruimm. eexact H5. instantiate (1 := Int.sub Int.iwordsize n). intros [v3 [A3 B3]].
- exploit eval_or. eexact A1. eexact A3. intros [v4 [A4 B4]].
- econstructor; split. EvalOp.
- intros. subst. simpl in *. rewrite H1 in *. rewrite H2 in *. rewrite H3.
- inv B1; inv B2; inv B3. simpl in B4. inv B4.
- simpl. rewrite Int64.decompose_shl_1; auto.
- destruct x; auto.
- + (* 32 <= n < 64 *)
- exploit eval_lowlong. eexact H. intros [v1 [A1 B1]].
- exploit eval_shlimm. eexact A1. instantiate (1 := Int.sub n Int.iwordsize). intros [v2 [A2 B2]].
- econstructor; split. EvalOp.
- destruct x; simpl; auto.
- destruct (Int.ltu n Int64.iwordsize'); auto.
- simpl in B1; inv B1. simpl in B2. rewrite H1 in B2. inv B2.
- simpl. erewrite <- Int64.decompose_shl_2. instantiate (1 := Int64.hiword i).
- rewrite Int64.ofwords_recompose. auto. auto.
- + (* n >= 64 *)
- econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto.
-Qed.
-
-Theorem eval_shll: binary_constructor_sound (shll hf) Val.shll.
-Proof.
- unfold shll; red; intros.
- destruct (is_intconst b) as [n|] eqn:IC.
-- (* Immediate *)
- exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0.
- eapply eval_shllimm; eauto.
-- (* General case *)
- econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
-Qed.
-
-Lemma eval_shrluimm:
- forall n,
- unary_constructor_sound (fun e => shrluimm hf e n) (fun v => Val.shrlu v (Vint n)).
-Proof.
- unfold shrluimm; red; intros. apply eval_shift_imm; intros.
- + (* n = 0 *)
- subst n. exists x; split; auto. destruct x; simpl; auto.
- change (Int64.shru' i Int.zero) with (Int64.shru i Int64.zero).
- rewrite Int64.shru_zero. auto.
- + (* 0 < n < 32 *)
- apply eval_splitlong with (sem := fun x => Val.shrlu x (Vint n)); auto.
- intros.
- exploit eval_shruimm. eexact H5. instantiate (1 := n). intros [v1 [A1 B1]].
- exploit eval_shruimm. eexact H4. instantiate (1 := n). intros [v2 [A2 B2]].
- exploit eval_shlimm. eexact H4. instantiate (1 := Int.sub Int.iwordsize n). intros [v3 [A3 B3]].
- exploit eval_or. eexact A1. eexact A3. intros [v4 [A4 B4]].
- econstructor; split. EvalOp.
- intros. subst. simpl in *. rewrite H1 in *. rewrite H2 in *. rewrite H3.
- inv B1; inv B2; inv B3. simpl in B4. inv B4.
- simpl. rewrite Int64.decompose_shru_1; auto.
- destruct x; auto.
- + (* 32 <= n < 64 *)
- exploit eval_highlong. eexact H. intros [v1 [A1 B1]].
- exploit eval_shruimm. eexact A1. instantiate (1 := Int.sub n Int.iwordsize). intros [v2 [A2 B2]].
- econstructor; split. EvalOp.
- destruct x; simpl; auto.
- destruct (Int.ltu n Int64.iwordsize'); auto.
- simpl in B1; inv B1. simpl in B2. rewrite H1 in B2. inv B2.
- simpl. erewrite <- Int64.decompose_shru_2. instantiate (1 := Int64.loword i).
- rewrite Int64.ofwords_recompose. auto. auto.
- + (* n >= 64 *)
- econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto.
-Qed.
-
-Theorem eval_shrlu: binary_constructor_sound (shrlu hf) Val.shrlu.
-Proof.
- unfold shrlu; red; intros.
- destruct (is_intconst b) as [n|] eqn:IC.
-- (* Immediate *)
- exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0.
- eapply eval_shrluimm; eauto.
-- (* General case *)
- econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
-Qed.
-
-Lemma eval_shrlimm:
- forall n,
- unary_constructor_sound (fun e => shrlimm hf e n) (fun v => Val.shrl v (Vint n)).
-Proof.
- unfold shrlimm; red; intros. apply eval_shift_imm; intros.
- + (* n = 0 *)
- subst n. exists x; split; auto. destruct x; simpl; auto.
- change (Int64.shr' i Int.zero) with (Int64.shr i Int64.zero).
- rewrite Int64.shr_zero. auto.
- + (* 0 < n < 32 *)
- apply eval_splitlong with (sem := fun x => Val.shrl x (Vint n)); auto.
- intros.
- exploit eval_shruimm. eexact H5. instantiate (1 := n). intros [v1 [A1 B1]].
- exploit eval_shrimm. eexact H4. instantiate (1 := n). intros [v2 [A2 B2]].
- exploit eval_shlimm. eexact H4. instantiate (1 := Int.sub Int.iwordsize n). intros [v3 [A3 B3]].
- exploit eval_or. eexact A1. eexact A3. intros [v4 [A4 B4]].
- econstructor; split. EvalOp.
- intros. subst. simpl in *. rewrite H1 in *. rewrite H2 in *. rewrite H3.
- inv B1; inv B2; inv B3. simpl in B4. inv B4.
- simpl. rewrite Int64.decompose_shr_1; auto.
- destruct x; auto.
- + (* 32 <= n < 64 *)
- exploit eval_highlong. eexact H. intros [v1 [A1 B1]].
- assert (eval_expr ge sp e m (v1 :: le) (Eletvar 0) v1) by EvalOp.
- exploit eval_shrimm. eexact H2. instantiate (1 := Int.sub n Int.iwordsize). intros [v2 [A2 B2]].
- exploit eval_shrimm. eexact H2. instantiate (1 := Int.repr 31). intros [v3 [A3 B3]].
- econstructor; split. EvalOp.
- destruct x; simpl; auto.
- destruct (Int.ltu n Int64.iwordsize'); auto.
- simpl in B1; inv B1. simpl in B2. rewrite H1 in B2. inv B2.
- simpl in B3. inv B3.
- change (Int.ltu (Int.repr 31) Int.iwordsize) with true. simpl.
- erewrite <- Int64.decompose_shr_2. instantiate (1 := Int64.loword i).
- rewrite Int64.ofwords_recompose. auto. auto.
- + (* n >= 64 *)
- econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto.
-Qed.
-
-Theorem eval_shrl: binary_constructor_sound (shrl hf) Val.shrl.
-Proof.
- unfold shrl; red; intros.
- destruct (is_intconst b) as [n|] eqn:IC.
-- (* Immediate *)
- exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0.
- eapply eval_shrlimm; eauto.
-- (* General case *)
- econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
-Qed.
-
-Theorem eval_addl: binary_constructor_sound addl Val.addl.
-Proof.
- unfold addl; red; intros.
- set (default := Ebuiltin (EF_builtin "__builtin_addl" sig_ll_l) (a ::: b ::: Enil)).
- assert (DEFAULT:
- exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.addl x y) v).
- {
- econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto.
- }
- destruct (is_longconst a) as [p|] eqn:LC1;
- destruct (is_longconst b) as [q|] eqn:LC2.
-- exploit (is_longconst_sound le a); eauto. intros EQ; subst x.
- exploit (is_longconst_sound le b); eauto. intros EQ; subst y.
- econstructor; split. apply eval_longconst. simpl; auto.
-- predSpec Int64.eq Int64.eq_spec p Int64.zero; auto.
- subst p. exploit (is_longconst_sound le a); eauto. intros EQ; subst x.
- exists y; split; auto. simpl. destruct y; auto. rewrite Int64.add_zero_l; auto.
-- predSpec Int64.eq Int64.eq_spec q Int64.zero; auto.
- subst q. exploit (is_longconst_sound le b); eauto. intros EQ; subst y.
- exists x; split; auto. destruct x; simpl; auto. rewrite Int64.add_zero; auto.
-- auto.
-Qed.
-
-Theorem eval_subl: binary_constructor_sound subl Val.subl.
-Proof.
- unfold subl; red; intros.
- set (default := Ebuiltin (EF_builtin "__builtin_subl" sig_ll_l) (a ::: b ::: Enil)).
- assert (DEFAULT:
- exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.subl x y) v).
- {
- econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto.
- }
- destruct (is_longconst a) as [p|] eqn:LC1;
- destruct (is_longconst b) as [q|] eqn:LC2.
-- exploit (is_longconst_sound le a); eauto. intros EQ; subst x.
- exploit (is_longconst_sound le b); eauto. intros EQ; subst y.
- econstructor; split. apply eval_longconst. simpl; auto.
-- predSpec Int64.eq Int64.eq_spec p Int64.zero; auto.
- replace (Val.subl x y) with (Val.negl y). eapply eval_negl; eauto.
- subst p. exploit (is_longconst_sound le a); eauto. intros EQ; subst x.
- destruct y; simpl; auto.
-- predSpec Int64.eq Int64.eq_spec q Int64.zero; auto.
- subst q. exploit (is_longconst_sound le b); eauto. intros EQ; subst y.
- exists x; split; auto. destruct x; simpl; auto. rewrite Int64.sub_zero_l; auto.
-- auto.
-Qed.
-
-Lemma eval_mull_base: binary_constructor_sound mull_base Val.mull.
-Proof.
- unfold mull_base; red; intros. apply eval_splitlong2; auto.
-- intros.
- set (p := Val.mull' x2 y2). set (le1 := p :: le0).
- assert (E1: eval_expr ge sp e m le1 (Eop Olowlong (Eletvar O ::: Enil)) (Val.loword p)) by EvalOp.
- assert (E2: eval_expr ge sp e m le1 (Eop Ohighlong (Eletvar O ::: Enil)) (Val.hiword p)) by EvalOp.
- exploit eval_mul. apply eval_lift. eexact H2. apply eval_lift. eexact H3.
- instantiate (1 := p). fold le1. intros [v3 [E3 L3]].
- exploit eval_mul. apply eval_lift. eexact H1. apply eval_lift. eexact H4.
- instantiate (1 := p). fold le1. intros [v4 [E4 L4]].
- exploit eval_add. eexact E2. eexact E3. intros [v5 [E5 L5]].
- exploit eval_add. eexact E5. eexact E4. intros [v6 [E6 L6]].
- exists (Val.longofwords v6 (Val.loword p)); split.
- EvalOp. eapply eval_builtin_2; eauto. UseHelper.
- intros. unfold le1, p in *; subst; simpl in *.
- inv L3. inv L4. inv L5. simpl in L6. inv L6.
- simpl. f_equal. symmetry. apply Int64.decompose_mul.
-- destruct x; auto; destruct y; auto.
-Qed.
-
-Lemma eval_mullimm:
- forall n, unary_constructor_sound (fun a => mullimm hf a n) (fun v => Val.mull v (Vlong n)).
-Proof.
- unfold mullimm; red; intros.
- predSpec Int64.eq Int64.eq_spec n Int64.zero.
- subst n. econstructor; split. apply eval_longconst.
- destruct x; simpl; auto. rewrite Int64.mul_zero. auto.
- predSpec Int64.eq Int64.eq_spec n Int64.one.
- subst n. exists x; split; auto.
- destruct x; simpl; auto. rewrite Int64.mul_one. auto.
- destruct (Int64.is_power2 n) as [l|] eqn:P2.
- exploit eval_shllimm. eauto. instantiate (1 := Int.repr (Int64.unsigned l)).
- intros [v [A B]].
- exists v; split; auto.
- destruct x; simpl; auto.
- erewrite Int64.mul_pow2 by eauto.
- assert (EQ: Int.unsigned (Int.repr (Int64.unsigned l)) = Int64.unsigned l).
- { apply Int.unsigned_repr.
- exploit Int64.is_power2_rng; eauto.
- assert (Int64.zwordsize < Int.max_unsigned) by (compute; auto).
- omega.
- }
- simpl in B.
- replace (Int.ltu (Int.repr (Int64.unsigned l)) Int64.iwordsize')
- with (Int64.ltu l Int64.iwordsize) in B.
- erewrite Int64.is_power2_range in B by eauto.
- unfold Int64.shl' in B. rewrite EQ in B. auto.
- unfold Int64.ltu, Int.ltu. rewrite EQ. auto.
- apply eval_mull_base; auto. apply eval_longconst.
-Qed.
-
-Theorem eval_mull: binary_constructor_sound (mull hf) Val.mull.
-Proof.
- unfold mull; red; intros.
- destruct (is_longconst a) as [p|] eqn:LC1;
- destruct (is_longconst b) as [q|] eqn:LC2.
-- exploit (is_longconst_sound le a); eauto. intros EQ; subst x.
- exploit (is_longconst_sound le b); eauto. intros EQ; subst y.
- econstructor; split. apply eval_longconst. simpl; auto.
-- exploit (is_longconst_sound le a); eauto. intros EQ; subst x.
- replace (Val.mull (Vlong p) y) with (Val.mull y (Vlong p)) in *.
- eapply eval_mullimm; eauto.
- destruct y; simpl; auto. rewrite Int64.mul_commut; auto.
-- exploit (is_longconst_sound le b); eauto. intros EQ; subst y.
- eapply eval_mullimm; eauto.
-- apply eval_mull_base; auto.
-Qed.
-
-Lemma eval_binop_long:
- forall id name sem le a b x y z,
- (forall p q, x = Vlong p -> y = Vlong q -> z = Vlong (sem p q)) ->
- helper_declared prog id name sig_ll_l ->
- external_implements name sig_ll_l (x::y::nil) z ->
- eval_expr ge sp e m le a x ->
- eval_expr ge sp e m le b y ->
- exists v, eval_expr ge sp e m le (binop_long id sem a b) v /\ Val.lessdef z v.
-Proof.
- intros. unfold binop_long.
- destruct (is_longconst a) as [p|] eqn:LC1.
- destruct (is_longconst b) as [q|] eqn:LC2.
- exploit is_longconst_sound. eexact LC1. eauto. intros EQ; subst x.
- exploit is_longconst_sound. eexact LC2. eauto. intros EQ; subst y.
- econstructor; split. EvalOp. erewrite H by eauto. rewrite Int64.ofwords_recompose. auto.
- econstructor; split. eapply eval_helper_2; eauto. auto.
- econstructor; split. eapply eval_helper_2; eauto. auto.
-Qed.
-
-Theorem eval_divl:
- forall le a b x y z,
- eval_expr ge sp e m le a x ->
- eval_expr ge sp e m le b y ->
- Val.divls x y = Some z ->
- exists v, eval_expr ge sp e m le (divl hf a b) v /\ Val.lessdef z v.
-Proof.
- intros. eapply eval_binop_long; eauto.
- intros; subst; simpl in H1.
- destruct (Int64.eq q Int64.zero
- || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1.
- auto.
- DeclHelper. UseHelper.
-Qed.
-
-Theorem eval_modl:
- forall le a b x y z,
- eval_expr ge sp e m le a x ->
- eval_expr ge sp e m le b y ->
- Val.modls x y = Some z ->
- exists v, eval_expr ge sp e m le (modl hf a b) v /\ Val.lessdef z v.
-Proof.
- intros. eapply eval_binop_long; eauto.
- intros; subst; simpl in H1.
- destruct (Int64.eq q Int64.zero
- || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1.
- auto.
- DeclHelper. UseHelper.
-Qed.
-
-Theorem eval_divlu:
- forall le a b x y z,
- eval_expr ge sp e m le a x ->
- eval_expr ge sp e m le b y ->
- Val.divlu x y = Some z ->
- exists v, eval_expr ge sp e m le (divlu hf a b) v /\ Val.lessdef z v.
-Proof.
- intros. unfold divlu.
- set (default := Eexternal hf.(i64_udiv) sig_ll_l (a ::: b ::: Enil)).
- assert (DEFAULT:
- exists v, eval_expr ge sp e m le default v /\ Val.lessdef z v).
- {
- econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
- }
- destruct (is_longconst a) as [p|] eqn:LC1;
- destruct (is_longconst b) as [q|] eqn:LC2.
-- exploit (is_longconst_sound le a); eauto. intros EQ; subst x.
- exploit (is_longconst_sound le b); eauto. intros EQ; subst y.
- econstructor; split. apply eval_longconst.
- simpl in H1. destruct (Int64.eq q Int64.zero); inv H1. auto.
-- auto.
-- destruct (Int64.is_power2 q) as [l|] eqn:P2; auto.
- exploit (is_longconst_sound le b); eauto. intros EQ; subst y.
- replace z with (Val.shrlu x (Vint (Int.repr (Int64.unsigned l)))).
- apply eval_shrluimm. auto.
- destruct x; simpl in H1; try discriminate.
- destruct (Int64.eq q Int64.zero); inv H1.
- simpl.
- assert (EQ: Int.unsigned (Int.repr (Int64.unsigned l)) = Int64.unsigned l).
- { apply Int.unsigned_repr.
- exploit Int64.is_power2_rng; eauto.
- assert (Int64.zwordsize < Int.max_unsigned) by (compute; auto).
- omega.
- }
- replace (Int.ltu (Int.repr (Int64.unsigned l)) Int64.iwordsize')
- with (Int64.ltu l Int64.iwordsize).
- erewrite Int64.is_power2_range by eauto.
- erewrite Int64.divu_pow2 by eauto.
- unfold Int64.shru', Int64.shru. rewrite EQ. auto.
- unfold Int64.ltu, Int.ltu. rewrite EQ. auto.
-- auto.
-Qed.
-
-Theorem eval_modlu:
- forall le a b x y z,
- eval_expr ge sp e m le a x ->
- eval_expr ge sp e m le b y ->
- Val.modlu x y = Some z ->
- exists v, eval_expr ge sp e m le (modlu hf a b) v /\ Val.lessdef z v.
-Proof.
- intros. unfold modlu.
- set (default := Eexternal hf.(i64_umod) sig_ll_l (a ::: b ::: Enil)).
- assert (DEFAULT:
- exists v, eval_expr ge sp e m le default v /\ Val.lessdef z v).
- {
- econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
- }
- destruct (is_longconst a) as [p|] eqn:LC1;
- destruct (is_longconst b) as [q|] eqn:LC2.
-- exploit (is_longconst_sound le a); eauto. intros EQ; subst x.
- exploit (is_longconst_sound le b); eauto. intros EQ; subst y.
- econstructor; split. apply eval_longconst.
- simpl in H1. destruct (Int64.eq q Int64.zero); inv H1. auto.
-- auto.
-- destruct (Int64.is_power2 q) as [l|] eqn:P2; auto.
- exploit (is_longconst_sound le b); eauto. intros EQ; subst y.
- replace z with (Val.andl x (Vlong (Int64.sub q Int64.one))).
- apply eval_andl. auto. apply eval_longconst.
- destruct x; simpl in H1; try discriminate.
- destruct (Int64.eq q Int64.zero); inv H1.
- simpl.
- erewrite Int64.modu_and by eauto. auto.
-- auto.
-Qed.
-
-Remark decompose_cmpl_eq_zero:
- forall h l,
- Int64.eq (Int64.ofwords h l) Int64.zero = Int.eq (Int.or h l) Int.zero.
-Proof.
- intros.
- assert (Int64.zwordsize = Int.zwordsize * 2) by reflexivity.
- predSpec Int64.eq Int64.eq_spec (Int64.ofwords h l) Int64.zero.
- replace (Int.or h l) with Int.zero. rewrite Int.eq_true. auto.
- apply Int.same_bits_eq; intros.
- rewrite Int.bits_zero. rewrite Int.bits_or by auto.
- symmetry. apply orb_false_intro.
- transitivity (Int64.testbit (Int64.ofwords h l) (i + Int.zwordsize)).
- rewrite Int64.bits_ofwords by omega. rewrite zlt_false by omega. f_equal; omega.
- rewrite H0. apply Int64.bits_zero.
- transitivity (Int64.testbit (Int64.ofwords h l) i).
- rewrite Int64.bits_ofwords by omega. rewrite zlt_true by omega. auto.
- rewrite H0. apply Int64.bits_zero.
- symmetry. apply Int.eq_false. red; intros; elim H0.
- apply Int64.same_bits_eq; intros.
- rewrite Int64.bits_zero. rewrite Int64.bits_ofwords by auto.
- destruct (zlt i Int.zwordsize).
- assert (Int.testbit (Int.or h l) i = false) by (rewrite H1; apply Int.bits_zero).
- rewrite Int.bits_or in H3 by omega. exploit orb_false_elim; eauto. tauto.
- assert (Int.testbit (Int.or h l) (i - Int.zwordsize) = false) by (rewrite H1; apply Int.bits_zero).
- rewrite Int.bits_or in H3 by omega. exploit orb_false_elim; eauto. tauto.
-Qed.
-
-Lemma eval_cmpl_eq_zero:
- forall le a x,
- eval_expr ge sp e m le a (Vlong x) ->
- eval_expr ge sp e m le (cmpl_eq_zero a) (Val.of_bool (Int64.eq x Int64.zero)).
-Proof.
- intros. unfold cmpl_eq_zero.
- eapply eval_splitlong_strict; eauto. intros.
- exploit eval_or. eexact H0. eexact H1. intros [v1 [A1 B1]]. simpl in B1; inv B1.
- exploit eval_comp. eexact A1. instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp.
- instantiate (1 := Ceq). intros [v2 [A2 B2]].
- unfold Val.cmp in B2; simpl in B2.
- rewrite <- decompose_cmpl_eq_zero in B2.
- rewrite Int64.ofwords_recompose in B2.
- destruct (Int64.eq x Int64.zero); inv B2; auto.
-Qed.
-
-Lemma eval_cmpl_ne_zero:
- forall le a x,
- eval_expr ge sp e m le a (Vlong x) ->
- eval_expr ge sp e m le (cmpl_ne_zero a) (Val.of_bool (negb (Int64.eq x Int64.zero))).
-Proof.
- intros. unfold cmpl_ne_zero.
- eapply eval_splitlong_strict; eauto. intros.
- exploit eval_or. eexact H0. eexact H1. intros [v1 [A1 B1]]. simpl in B1; inv B1.
- exploit eval_comp. eexact A1. instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp.
- instantiate (1 := Cne). intros [v2 [A2 B2]].
- unfold Val.cmp in B2; simpl in B2.
- rewrite <- decompose_cmpl_eq_zero in B2.
- rewrite Int64.ofwords_recompose in B2.
- destruct (negb (Int64.eq x Int64.zero)); inv B2; auto.
-Qed.
-
-Lemma eval_cmplu_gen:
- forall ch cl a b le x y,
- eval_expr ge sp e m le a (Vlong x) ->
- eval_expr ge sp e m le b (Vlong y) ->
- eval_expr ge sp e m le (cmplu_gen ch cl a b)
- (Val.of_bool (if Int.eq (Int64.hiword x) (Int64.hiword y)
- then Int.cmpu cl (Int64.loword x) (Int64.loword y)
- else Int.cmpu ch (Int64.hiword x) (Int64.hiword y))).
-Proof.
- intros. unfold cmplu_gen. eapply eval_splitlong2_strict; eauto. intros.
- econstructor. econstructor. EvalOp. simpl. eauto.
- destruct (Int.eq (Int64.hiword x) (Int64.hiword y)); EvalOp.
-Qed.
-
-Remark int64_eq_xor:
- forall p q, Int64.eq p q = Int64.eq (Int64.xor p q) Int64.zero.
-Proof.
- intros.
- predSpec Int64.eq Int64.eq_spec p q.
- subst q. rewrite Int64.xor_idem. rewrite Int64.eq_true. auto.
- predSpec Int64.eq Int64.eq_spec (Int64.xor p q) Int64.zero.
- elim H. apply Int64.xor_zero_equal; auto.
- auto.
-Qed.
-
-Theorem eval_cmplu:
- forall c le a x b y v,
- eval_expr ge sp e m le a x ->
- eval_expr ge sp e m le b y ->
- Val.cmplu c x y = Some v ->
- eval_expr ge sp e m le (cmplu c a b) v.
-Proof.
- intros. unfold Val.cmplu in H1.
- destruct x; simpl in H1; try discriminate. destruct y; inv H1.
- rename i into x. rename i0 into y.
- destruct c; simpl.
-- (* Ceq *)
- exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B.
- rewrite int64_eq_xor. apply eval_cmpl_eq_zero; auto.
-- (* Cne *)
- exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B.
- rewrite int64_eq_xor. apply eval_cmpl_ne_zero; auto.
-- (* Clt *)
- exploit (eval_cmplu_gen Clt Clt). eexact H. eexact H0. simpl.
- rewrite <- Int64.decompose_ltu. rewrite ! Int64.ofwords_recompose. auto.
-- (* Cle *)
- exploit (eval_cmplu_gen Clt Cle). eexact H. eexact H0. intros.
- rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y).
- rewrite Int64.decompose_leu. auto.
-- (* Cgt *)
- exploit (eval_cmplu_gen Cgt Cgt). eexact H. eexact H0. simpl.
- rewrite Int.eq_sym. rewrite <- Int64.decompose_ltu. rewrite ! Int64.ofwords_recompose. auto.
-- (* Cge *)
- exploit (eval_cmplu_gen Cgt Cge). eexact H. eexact H0. intros.
- rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y).
- rewrite Int64.decompose_leu. rewrite Int.eq_sym. auto.
-Qed.
-
-Lemma eval_cmpl_gen:
- forall ch cl a b le x y,
- eval_expr ge sp e m le a (Vlong x) ->
- eval_expr ge sp e m le b (Vlong y) ->
- eval_expr ge sp e m le (cmpl_gen ch cl a b)
- (Val.of_bool (if Int.eq (Int64.hiword x) (Int64.hiword y)
- then Int.cmpu cl (Int64.loword x) (Int64.loword y)
- else Int.cmp ch (Int64.hiword x) (Int64.hiword y))).
-Proof.
- intros. unfold cmpl_gen. eapply eval_splitlong2_strict; eauto. intros.
- econstructor. econstructor. EvalOp. simpl. eauto.
- destruct (Int.eq (Int64.hiword x) (Int64.hiword y)); EvalOp.
-Qed.
-
-Remark decompose_cmpl_lt_zero:
- forall h l,
- Int64.lt (Int64.ofwords h l) Int64.zero = Int.lt h Int.zero.
-Proof.
- intros.
- generalize (Int64.shru_lt_zero (Int64.ofwords h l)).
- change (Int64.shru (Int64.ofwords h l) (Int64.repr (Int64.zwordsize - 1)))
- with (Int64.shru' (Int64.ofwords h l) (Int.repr 63)).
- rewrite Int64.decompose_shru_2.
- change (Int.sub (Int.repr 63) Int.iwordsize)
- with (Int.repr (Int.zwordsize - 1)).
- rewrite Int.shru_lt_zero.
- destruct (Int64.lt (Int64.ofwords h l) Int64.zero); destruct (Int.lt h Int.zero); auto; intros.
- elim Int64.one_not_zero. auto.
- elim Int64.one_not_zero. auto.
- vm_compute. intuition congruence.
-Qed.
-
-Theorem eval_cmpl:
- forall c le a x b y v,
- eval_expr ge sp e m le a x ->
- eval_expr ge sp e m le b y ->
- Val.cmpl c x y = Some v ->
- eval_expr ge sp e m le (cmpl c a b) v.
-Proof.
- intros. unfold Val.cmpl in H1.
- destruct x; simpl in H1; try discriminate. destruct y; inv H1.
- rename i into x. rename i0 into y.
- destruct c; simpl.
-- (* Ceq *)
- exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B.
- rewrite int64_eq_xor. apply eval_cmpl_eq_zero; auto.
-- (* Cne *)
- exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B.
- rewrite int64_eq_xor. apply eval_cmpl_ne_zero; auto.
-- (* Clt *)
- destruct (is_longconst_zero b) eqn:LC.
-+ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0.
- exploit eval_highlong. eexact H. intros [v1 [A1 B1]]. simpl in B1. inv B1.
- exploit eval_comp. eexact A1.
- instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp.
- instantiate (1 := Clt). intros [v2 [A2 B2]].
- unfold Val.cmp in B2. simpl in B2.
- rewrite <- (Int64.ofwords_recompose x). rewrite decompose_cmpl_lt_zero.
- destruct (Int.lt (Int64.hiword x) Int.zero); inv B2; auto.
-+ exploit (eval_cmpl_gen Clt Clt). eexact H. eexact H0. simpl.
- rewrite <- Int64.decompose_lt. rewrite ! Int64.ofwords_recompose. auto.
-- (* Cle *)
- exploit (eval_cmpl_gen Clt Cle). eexact H. eexact H0. intros.
- rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y).
- rewrite Int64.decompose_le. auto.
-- (* Cgt *)
- exploit (eval_cmpl_gen Cgt Cgt). eexact H. eexact H0. simpl.
- rewrite Int.eq_sym. rewrite <- Int64.decompose_lt. rewrite ! Int64.ofwords_recompose. auto.
-- (* Cge *)
- destruct (is_longconst_zero b) eqn:LC.
-+ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0.
- exploit eval_highlong. eexact H. intros [v1 [A1 B1]]. simpl in B1; inv B1.
- exploit eval_comp. eexact A1.
- instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp.
- instantiate (1 := Cge). intros [v2 [A2 B2]].
- unfold Val.cmp in B2; simpl in B2.
- rewrite <- (Int64.ofwords_recompose x). rewrite decompose_cmpl_lt_zero.
- destruct (negb (Int.lt (Int64.hiword x) Int.zero)); inv B2; auto.
-+ exploit (eval_cmpl_gen Cgt Cge). eexact H. eexact H0. intros.
- rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y).
- rewrite Int64.decompose_le. rewrite Int.eq_sym. auto.
-Qed.
-
-End CMCONSTR.
-