Add scheduling oracle to Verilog

1 files changed, 244 insertions, 180 deletions

diff --git a/verilog/SelectLongproof.v b/verilog/SelectLongproof.v
index f008f39e..0fc578bf 100644
--- a/verilog/SelectLongproof.v
+++ b/verilog/SelectLongproof.v
@@ -3,11 +3,16 @@
 (*              The Compcert verified compiler                         *)
 (*                                                                     *)
 (*                 Xavier Leroy, INRIA Paris                           *)
+(*           Prashanth Mundkur, SRI International                      *)
 (*                                                                     *)
 (*  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.     *)
 (*                                                                     *)
+(*  The contributions by Prashanth Mundkur are reused and adapted      *)
+(*  under the terms of a Contributor License Agreement between         *)
+(*  SRI International and INRIA.                                       *)
+(*                                                                     *)
 (* *********************************************************************)
 
 (** Correctness of instruction selection for 64-bit integer operations *)
@@ -104,102 +109,101 @@ Proof.
 - TrivialExists.
 Qed.
 
-Theorem eval_notl: unary_constructor_sound notl Val.notl.
-Proof.
-  unfold notl; destruct Archi.splitlong. apply SplitLongproof.eval_notl.
-  red; intros. destruct (notl_match a).
-- InvEval. econstructor; split. apply eval_longconst. auto.
-- InvEval. subst. exists v1; split; auto. destruct v1; simpl; auto. rewrite Int64.not_involutive; auto.
-- TrivialExists.
-Qed.
-
-Theorem eval_andlimm: forall n, unary_constructor_sound (andlimm n) (fun v => Val.andl v (Vlong n)).
-Proof.
-  unfold andlimm; intros; red; intros.
-  predSpec Int64.eq Int64.eq_spec n Int64.zero.
-  exists (Vlong Int64.zero); split. apply eval_longconst.
-  subst. destruct x; simpl; auto. rewrite Int64.and_zero; auto.
-  predSpec Int64.eq Int64.eq_spec n Int64.mone.
-  exists x; split. assumption.
-  subst. destruct x; simpl; auto. rewrite Int64.and_mone; auto.
-  destruct (andlimm_match a); InvEval; subst.
-- econstructor; split. apply eval_longconst. simpl. rewrite Int64.and_commut; auto.
-- TrivialExists. simpl. rewrite Val.andl_assoc. rewrite Int64.and_commut; auto.
-- TrivialExists.
-Qed.
-
-Theorem eval_andl: binary_constructor_sound andl Val.andl.
+Theorem eval_negl: unary_constructor_sound negl Val.negl.
 Proof.
-  unfold andl; destruct Archi.splitlong. apply SplitLongproof.eval_andl.
-  red; intros. destruct (andl_match a b).
-- InvEval. rewrite Val.andl_commut. apply eval_andlimm; auto.
-- InvEval. apply eval_andlimm; auto.
+  unfold negl. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_negl; auto.
+  red; intros. destruct (is_longconst a) as [n|] eqn:C.
+- exploit is_longconst_sound; eauto. intros EQ; subst x.
+  econstructor; split. apply eval_longconst. auto.
 - TrivialExists.
 Qed.
 
-Theorem eval_orlimm: forall n, unary_constructor_sound (orlimm n) (fun v => Val.orl v (Vlong n)).
+Theorem eval_addlimm: forall n, unary_constructor_sound (addlimm n) (fun v => Val.addl v (Vlong n)).
 Proof.
-  unfold orlimm; intros; red; intros.
+  unfold addlimm; intros; red; intros.
   predSpec Int64.eq Int64.eq_spec n Int64.zero.
-  exists x; split; auto. subst. destruct x; simpl; auto. rewrite Int64.or_zero; auto.
-  predSpec Int64.eq Int64.eq_spec n Int64.mone.
-  econstructor; split. apply eval_longconst. subst. destruct x; simpl; auto. rewrite Int64.or_mone; auto.
-  destruct (orlimm_match a); InvEval; subst.
-- econstructor; split. apply eval_longconst. simpl. rewrite Int64.or_commut; auto.
-- TrivialExists. simpl. rewrite Val.orl_assoc. rewrite Int64.or_commut; auto.
+  subst. exists x; split; auto.
+  destruct x; simpl; rewrite ?Int64.add_zero, ?Ptrofs.add_zero; auto.
+  destruct Archi.ptr64; auto.
+  destruct (addlimm_match a); InvEval.
+- econstructor; split. apply eval_longconst. rewrite Int64.add_commut; auto.
+- econstructor; split. EvalOp. simpl; eauto. 
+  unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. 
+  destruct Archi.ptr64; auto. rewrite Ptrofs.add_commut; auto. 
+- econstructor; split. EvalOp. simpl; eauto. 
+  destruct sp; simpl; auto. destruct Archi.ptr64; auto. 
+  rewrite Ptrofs.add_assoc, (Ptrofs.add_commut m0). auto. 
+- subst x. rewrite Val.addl_assoc. rewrite Int64.add_commut. TrivialExists.
 - TrivialExists.
 Qed.
 
-Theorem eval_orl: binary_constructor_sound orl Val.orl.
+Theorem eval_addl: binary_constructor_sound addl Val.addl.
 Proof.
-  unfold orl; destruct Archi.splitlong. apply SplitLongproof.eval_orl.
-  red; intros.
-  assert (DEFAULT: exists v, eval_expr ge sp e m le (Eop Oorl (a:::b:::Enil)) v /\ Val.lessdef (Val.orl x y) v) by TrivialExists.
-  assert (ROR: forall v n1 n2,
-    Int.add n1 n2 = Int64.iwordsize' ->
-    Val.lessdef (Val.orl (Val.shll v (Vint n1)) (Val.shrlu v (Vint n2)))
-                (Val.rorl v (Vint n2))).
-  { intros. destruct v; simpl; auto.
-    destruct (Int.ltu n1 Int64.iwordsize') eqn:N1; auto.
-    destruct (Int.ltu n2 Int64.iwordsize') eqn:N2; auto.
-    simpl. rewrite <- Int64.or_ror'; auto. }
-  destruct (orl_match a b).
-- InvEval. rewrite Val.orl_commut. apply eval_orlimm; auto.
-- InvEval. apply eval_orlimm; auto.
-- predSpec Int.eq Int.eq_spec (Int.add n1 n2) Int64.iwordsize'; auto.
-  destruct (same_expr_pure t1 t2) eqn:?; auto.
-  InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst.
-  exists (Val.rorl v0 (Vint n2)); split. EvalOp. apply ROR; auto.
-- predSpec Int.eq Int.eq_spec (Int.add n1 n2) Int64.iwordsize'; auto.
-  destruct (same_expr_pure t1 t2) eqn:?; auto.
-  InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst.
-  exists (Val.rorl v1 (Vint n2)); split. EvalOp. rewrite Val.orl_commut. apply ROR; auto.
-- apply DEFAULT.
-Qed.
+  unfold addl. destruct Archi.splitlong eqn:SL. 
+  apply SplitLongproof.eval_addl. apply Archi.splitlong_ptr32; auto.
+(*
+  assert (SF: Archi.ptr64 = true).
+  { Local Transparent Archi.splitlong. unfold Archi.splitlong in SL. 
+    destruct Archi.ptr64; simpl in *; congruence. }  
+*)
+(*
+  assert (B: forall id ofs n,
+             Genv.symbol_address ge id (Ptrofs.add ofs (Ptrofs.repr n)) =
+             Val.addl (Genv.symbol_address ge id ofs) (Vlong (Int64.repr n))).
+  { intros. replace (Ptrofs.repr n) with (Ptrofs.of_int64 (Int64.repr n)) by auto with ptrofs.
+    apply Genv.shift_symbol_address_64; auto. }
 
-Theorem eval_xorlimm: forall n, unary_constructor_sound (xorlimm n) (fun v => Val.xorl v (Vlong n)).
-Proof.
-  unfold xorlimm; intros; red; intros.
-  predSpec Int64.eq Int64.eq_spec n Int64.zero.
-  exists x; split; auto. subst. destruct x; simpl; auto. rewrite Int64.xor_zero; auto.
-  predSpec Int64.eq Int64.eq_spec n Int64.mone.
-  replace (Val.xorl x (Vlong n)) with (Val.notl x). apply eval_notl; auto.
-  subst n. destruct x; simpl; auto.
-  destruct (xorlimm_match a); InvEval; subst.
-- econstructor; split. apply eval_longconst. simpl. rewrite Int64.xor_commut; auto.
-- TrivialExists. simpl. rewrite Val.xorl_assoc. rewrite Int64.xor_commut; auto.
-- TrivialExists. simpl. destruct v1; simpl; auto. unfold Int64.not.
-  rewrite Int64.xor_assoc. apply f_equal. apply f_equal. apply f_equal.
-  apply Int64.xor_commut.
-- TrivialExists.
+*)
+  red; intros until y.
+  case (addl_match a b); intros; InvEval.
+  - rewrite Val.addl_commut. apply eval_addlimm; auto.
+  - apply eval_addlimm; auto.
+  - subst.
+    replace (Val.addl (Val.addl v1 (Vlong n1)) (Val.addl v0 (Vlong n2)))
+       with (Val.addl (Val.addl v1 v0) (Val.addl (Vlong n1) (Vlong n2))).
+    apply eval_addlimm. EvalOp.
+    repeat rewrite Val.addl_assoc. decEq. apply Val.addl_permut.
+  - subst. econstructor; split.
+    EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. simpl; eauto.
+    rewrite Val.addl_commut. destruct sp; simpl; auto.
+    destruct v1; simpl; auto.
+    destruct Archi.ptr64 eqn:SF; auto. 
+    apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. 
+    rewrite (Ptrofs.add_commut (Ptrofs.of_int64 n1)), Ptrofs.add_assoc. f_equal. auto with ptrofs.
+    destruct Archi.ptr64 eqn:SF; auto.
+  - subst. econstructor; split.
+    EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. simpl; eauto.
+    destruct sp; simpl; auto.
+    destruct v1; simpl; auto.
+    destruct Archi.ptr64 eqn:SF; auto. 
+    apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. f_equal.
+    rewrite Ptrofs.add_commut. auto with ptrofs.
+    destruct Archi.ptr64 eqn:SF; auto.
+  - subst.
+    replace (Val.addl (Val.addl v1 (Vlong n1)) y)
+       with (Val.addl (Val.addl v1 y) (Vlong n1)).
+    apply eval_addlimm. EvalOp.
+    repeat rewrite Val.addl_assoc. decEq. apply Val.addl_commut.
+  - subst.
+    replace (Val.addl x (Val.addl v1 (Vlong n2)))
+       with (Val.addl (Val.addl x v1) (Vlong n2)).
+    apply eval_addlimm. EvalOp.
+    repeat rewrite Val.addl_assoc. reflexivity.
+  - TrivialExists.
 Qed.
 
-Theorem eval_xorl: binary_constructor_sound xorl Val.xorl.
+Theorem eval_subl: binary_constructor_sound subl Val.subl.
 Proof.
-  unfold xorl; destruct Archi.splitlong. apply SplitLongproof.eval_xorl.
-  red; intros. destruct (xorl_match a b).
-- InvEval. rewrite Val.xorl_commut. apply eval_xorlimm; auto.
-- InvEval. apply eval_xorlimm; auto.
+  unfold subl. destruct Archi.splitlong eqn:SL.
+  apply SplitLongproof.eval_subl. apply Archi.splitlong_ptr32; auto.
+  red; intros; destruct (subl_match a b); InvEval.
+- rewrite Val.subl_addl_opp. apply eval_addlimm; auto.
+- subst. rewrite Val.subl_addl_l. rewrite Val.subl_addl_r.
+  rewrite Val.addl_assoc. simpl. rewrite Int64.add_commut. rewrite <- Int64.sub_add_opp.
+  apply eval_addlimm; EvalOp.
+- subst. rewrite Val.subl_addl_l. apply eval_addlimm; EvalOp.
+- subst. rewrite Val.subl_addl_r.
+  apply eval_addlimm; EvalOp.
 - TrivialExists.
 Qed.
 
@@ -215,20 +219,13 @@ Proof.
   assert (DEFAULT: exists v, eval_expr ge sp e m le (Eop (Oshllimm n) (a:::Enil)) v
                          /\  Val.lessdef (Val.shll x (Vint n)) v) by TrivialExists.
   destruct (shllimm_match a); InvEval.
-- TrivialExists. simpl; rewrite LT; auto.
+- econstructor; split. apply eval_longconst. simpl; rewrite LT; auto.
 - destruct (Int.ltu (Int.add n n1) Int64.iwordsize') eqn:LT'; auto.
   subst. econstructor; split. EvalOp. simpl; eauto.
   destruct v1; simpl; auto. rewrite LT'.
   destruct (Int.ltu n1 Int64.iwordsize') eqn:LT1; auto.
   simpl; rewrite LT. rewrite Int.add_commut, Int64.shl'_shl'; auto. rewrite Int.add_commut; auto.
-- destruct (shift_is_scale n); auto.
-  TrivialExists. simpl. destruct v1; simpl; auto.
-  rewrite LT. rewrite ! Int64.repr_unsigned. rewrite Int64.shl'_one_two_p.
-  rewrite ! Int64.shl'_mul_two_p.  rewrite Int64.mul_add_distr_l. auto.
-- destruct (shift_is_scale n); auto.
-  TrivialExists. simpl. destruct x; simpl; auto.
-  rewrite LT. rewrite ! Int64.repr_unsigned. rewrite Int64.shl'_one_two_p.
-  rewrite ! Int64.shl'_mul_two_p. rewrite Int64.add_zero. auto.
+- apply DEFAULT.  
 - TrivialExists. constructor; eauto. constructor. EvalOp. simpl; eauto. constructor. auto.
 Qed.
 
@@ -244,7 +241,7 @@ Proof.
   assert (DEFAULT: exists v, eval_expr ge sp e m le (Eop (Oshrluimm n) (a:::Enil)) v
                          /\  Val.lessdef (Val.shrlu x (Vint n)) v) by TrivialExists.
   destruct (shrluimm_match a); InvEval.
-- TrivialExists. simpl; rewrite LT; auto.
+- econstructor; split. apply eval_longconst. simpl; rewrite LT; auto.
 - destruct (Int.ltu (Int.add n n1) Int64.iwordsize') eqn:LT'; auto.
   subst. econstructor; split. EvalOp. simpl; eauto.
   destruct v1; simpl; auto. rewrite LT'.
@@ -266,7 +263,7 @@ Proof.
   assert (DEFAULT: exists v, eval_expr ge sp e m le (Eop (Oshrlimm n) (a:::Enil)) v
                          /\  Val.lessdef (Val.shrl x (Vint n)) v) by TrivialExists.
   destruct (shrlimm_match a); InvEval.
-- TrivialExists. simpl; rewrite LT; auto.
+- econstructor; split. apply eval_longconst. simpl; rewrite LT; auto.
 - destruct (Int.ltu (Int.add n n1) Int64.iwordsize') eqn:LT'; auto.
   subst. econstructor; split. EvalOp. simpl; eauto.
   destruct v1; simpl; auto. rewrite LT'.
@@ -300,82 +297,17 @@ Proof.
 - TrivialExists.
 Qed.
 
-Theorem eval_negl: unary_constructor_sound negl Val.negl.
-Proof.
-  unfold negl. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_negl; auto.
-  red; intros. destruct (is_longconst a) as [n|] eqn:C.
-- exploit is_longconst_sound; eauto. intros EQ; subst x.
-  econstructor; split. apply eval_longconst. auto.
-- TrivialExists.
-Qed.
-
-Theorem eval_addlimm: forall n, unary_constructor_sound (addlimm n) (fun v => Val.addl v (Vlong n)).
-Proof.
-  unfold addlimm; intros; red; intros.
-  predSpec Int64.eq Int64.eq_spec n Int64.zero.
-  subst. exists x; split; auto.
-  destruct x; simpl; rewrite ?Int64.add_zero, ?Ptrofs.add_zero; auto.
-  destruct (addlimm_match a); InvEval.
-- econstructor; split. apply eval_longconst. rewrite Int64.add_commut; auto.
-- inv H. simpl in H6. TrivialExists. simpl.
-  erewrite eval_offset_addressing_total_64 by eauto. rewrite Int64.repr_signed; auto.
-- TrivialExists. simpl. rewrite Int64.repr_signed; auto.
-Qed.
-
-Theorem eval_addl: binary_constructor_sound addl Val.addl.
-Proof.
-  assert (A: forall x y, Int64.repr (x + y) = Int64.add (Int64.repr x) (Int64.repr y)).
-  { intros; apply Int64.eqm_samerepr; auto with ints. }
-  assert (B: forall id ofs n, Archi.ptr64 = true ->
-             Genv.symbol_address ge id (Ptrofs.add ofs (Ptrofs.repr n)) =
-             Val.addl (Genv.symbol_address ge id ofs) (Vlong (Int64.repr n))).
-  { intros. replace (Ptrofs.repr n) with (Ptrofs.of_int64 (Int64.repr n)) by auto with ptrofs.
-    apply Genv.shift_symbol_address_64; auto. }
-  unfold addl. destruct Archi.splitlong eqn:SL.
-  apply SplitLongproof.eval_addl. apply Archi.splitlong_ptr32; auto.
-  red; intros; destruct (addl_match a b); InvEval.
-- rewrite Val.addl_commut. apply eval_addlimm; auto.
-- apply eval_addlimm; auto.
-- subst. TrivialExists. simpl. rewrite A, Val.addl_permut_4. auto.
-- subst. TrivialExists. simpl. rewrite A, Val.addl_assoc. decEq; decEq. rewrite Val.addl_permut. auto.
-- subst. TrivialExists. simpl. rewrite A, Val.addl_permut_4. rewrite <- Val.addl_permut. rewrite <- Val.addl_assoc. auto.
-- subst. TrivialExists. simpl. rewrite Val.addl_commut; auto.
-- subst. TrivialExists.
-- subst. TrivialExists. simpl. rewrite ! Val.addl_assoc. rewrite (Val.addl_commut y). auto.
-- subst. TrivialExists. simpl. rewrite ! Val.addl_assoc. auto.
-- TrivialExists. simpl.
-  unfold Val.addl. destruct Archi.ptr64, x, y; auto.
-  + rewrite Int64.add_zero; auto.
-  + rewrite Ptrofs.add_assoc, Ptrofs.add_zero. auto.
-  + rewrite Ptrofs.add_assoc, Ptrofs.add_zero. auto.
-  + rewrite Int64.add_zero; auto.
-Qed.
-
-Theorem eval_subl: binary_constructor_sound subl Val.subl.
-Proof.
-  unfold subl. destruct Archi.splitlong eqn:SL.
-  apply SplitLongproof.eval_subl. apply Archi.splitlong_ptr32; auto.
-  red; intros; destruct (subl_match a b); InvEval.
-- rewrite Val.subl_addl_opp. apply eval_addlimm; auto.
-- subst. rewrite Val.subl_addl_l. rewrite Val.subl_addl_r.
-  rewrite Val.addl_assoc. simpl. rewrite Int64.add_commut. rewrite <- Int64.sub_add_opp.
-  replace (Int64.repr (n1 - n2)) with (Int64.sub (Int64.repr n1) (Int64.repr n2)).
-  apply eval_addlimm; EvalOp.
-  apply Int64.eqm_samerepr; auto with ints.
-- subst. rewrite Val.subl_addl_l. apply eval_addlimm; EvalOp.
-- subst. rewrite Val.subl_addl_r.
-  replace (Int64.repr (-n2)) with (Int64.neg (Int64.repr n2)).
-  apply eval_addlimm; EvalOp.
-  apply Int64.eqm_samerepr; auto with ints.
-- TrivialExists.
-Qed.
-
 Theorem eval_mullimm_base: forall n, unary_constructor_sound (mullimm_base n) (fun v => Val.mull v (Vlong n)).
 Proof.
   intros; unfold mullimm_base. red; intros.
+  assert (DEFAULT: exists v,
+                eval_expr ge sp e m le (Eop Omull (a ::: longconst n ::: Enil)) v
+             /\ Val.lessdef (Val.mull x (Vlong n)) v).
+  { econstructor; split. EvalOp. constructor. eauto. constructor. apply eval_longconst. constructor. simpl; eauto.
+    auto. }
   generalize (Int64.one_bits'_decomp n); intros D.
   destruct (Int64.one_bits' n) as [ | i [ | j [ | ? ? ]]] eqn:B.
-- TrivialExists.
+- apply DEFAULT.
 - replace (Val.mull x (Vlong n)) with (Val.shll x (Vint i)).
   apply eval_shllimm; auto.
   simpl in D. rewrite D, Int64.add_zero. destruct x; simpl; auto.
@@ -393,14 +325,14 @@ Proof.
   rewrite (Int64.one_bits'_range n) in B2 by (rewrite B; auto with coqlib).
   inv B1; inv B2. simpl in B3; inv B3.
   rewrite Int64.mul_add_distr_r. rewrite <- ! Int64.shl'_mul. auto.
-- TrivialExists.
+- apply DEFAULT.
 Qed.
 
 Theorem eval_mullimm: forall n, unary_constructor_sound (mullimm n) (fun v => Val.mull v (Vlong n)).
 Proof.
   unfold mullimm. intros; red; intros.
   destruct Archi.splitlong eqn:SL.
-  eapply SplitLongproof.eval_mullimm; eauto.
+  eapply SplitLongproof.eval_mullimm; eauto.  
   predSpec Int64.eq Int64.eq_spec n Int64.zero.
   exists (Vlong Int64.zero); split. apply eval_longconst.
   destruct x; simpl; auto. subst n; rewrite Int64.mul_zero; auto.
@@ -410,11 +342,12 @@ Proof.
   destruct (mullimm_match a); InvEval.
 - econstructor; split. apply eval_longconst. rewrite Int64.mul_commut; auto.
 - exploit (eval_mullimm_base n); eauto. intros (v2 & A2 & B2).
-  exploit (eval_addlimm (Int64.mul n (Int64.repr n2))). eexact A2. intros (v3 & A3 & B3).
+  exploit (eval_addlimm (Int64.mul n n2)). eexact A2. intros (v3 & A3 & B3).
   exists v3; split; auto.
-  destruct v1; simpl; auto.
+  subst x. destruct v1; simpl; auto.
   simpl in B2; inv B2. simpl in B3; inv B3. rewrite Int64.mul_add_distr_l.
   rewrite (Int64.mul_commut n). auto.
+  destruct Archi.ptr64; simpl; auto.
 - apply eval_mullimm_base; auto.
 Qed.
 
@@ -427,39 +360,105 @@ Proof.
 - TrivialExists.
 Qed.
 
-Theorem eval_mullhu:
+Theorem eval_mullhu: 
   forall n, unary_constructor_sound (fun a => mullhu a n) (fun v => Val.mullhu v (Vlong n)).
 Proof.
   unfold mullhu; intros. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_mullhu; auto.
   red; intros. TrivialExists. constructor. eauto. constructor. apply eval_longconst. constructor. auto.
 Qed.
 
-Theorem eval_mullhs:
+Theorem eval_mullhs: 
   forall n, unary_constructor_sound (fun a => mullhs a n) (fun v => Val.mullhs v (Vlong n)).
 Proof.
   unfold mullhs; intros. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_mullhs; auto.
   red; intros. TrivialExists. constructor. eauto. constructor. apply eval_longconst. constructor. auto.
 Qed.
 
-Theorem eval_shrxlimm:
-  forall le a n x z,
-  eval_expr ge sp e m le a x ->
-  Val.shrxl x (Vint n) = Some z ->
-  exists v, eval_expr ge sp e m le (shrxlimm a n) v /\ Val.lessdef z v.
+Theorem eval_andlimm: forall n, unary_constructor_sound (andlimm n) (fun v => Val.andl v (Vlong n)).
 Proof.
-  unfold shrxlimm; intros. destruct Archi.splitlong eqn:SL.
-+ eapply SplitLongproof.eval_shrxlimm; eauto using Archi.splitlong_ptr32.
-+ predSpec Int.eq Int.eq_spec n Int.zero.
-- subst n. destruct x; simpl in H0; inv H0. econstructor; split; eauto.
-  change (Int.ltu Int.zero (Int.repr 63)) with true. simpl. rewrite Int64.shrx'_zero; auto.
+  unfold andlimm; intros; red; intros.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero.
+  exists (Vlong Int64.zero); split. apply eval_longconst.
+  subst. destruct x; simpl; auto. rewrite Int64.and_zero; auto.
+  predSpec Int64.eq Int64.eq_spec n Int64.mone.
+  exists x; split. assumption.
+  subst. destruct x; simpl; auto. rewrite Int64.and_mone; auto.
+  destruct (andlimm_match a); InvEval; subst.
+- econstructor; split. apply eval_longconst. simpl. rewrite Int64.and_commut; auto.
+- TrivialExists. simpl. rewrite Val.andl_assoc. rewrite Int64.and_commut; auto.
+- TrivialExists.
+Qed.
+
+Theorem eval_andl: binary_constructor_sound andl Val.andl.
+Proof.
+  unfold andl; destruct Archi.splitlong. apply SplitLongproof.eval_andl.
+  red; intros. destruct (andl_match a b).
+- InvEval. rewrite Val.andl_commut. apply eval_andlimm; auto.
+- InvEval. apply eval_andlimm; auto.
+- TrivialExists.
+Qed.
+
+Theorem eval_orlimm: forall n, unary_constructor_sound (orlimm n) (fun v => Val.orl v (Vlong n)).
+Proof.
+  unfold orlimm; intros; red; intros.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero.
+  exists x; split; auto. subst. destruct x; simpl; auto. rewrite Int64.or_zero; auto.
+  predSpec Int64.eq Int64.eq_spec n Int64.mone.
+  econstructor; split. apply eval_longconst. subst. destruct x; simpl; auto. rewrite Int64.or_mone; auto.
+  destruct (orlimm_match a); InvEval; subst.
+- econstructor; split. apply eval_longconst. simpl. rewrite Int64.or_commut; auto.
+- TrivialExists. simpl. rewrite Val.orl_assoc. rewrite Int64.or_commut; auto.
 - TrivialExists.
 Qed.
 
+Theorem eval_orl: binary_constructor_sound orl Val.orl.
+Proof.
+  unfold orl; destruct Archi.splitlong. apply SplitLongproof.eval_orl.
+  red; intros.
+  destruct (orl_match a b).
+- InvEval. rewrite Val.orl_commut. apply eval_orlimm; auto.
+- InvEval. apply eval_orlimm; auto.
+- TrivialExists.
+Qed.
+
+Theorem eval_xorlimm: forall n, unary_constructor_sound (xorlimm n) (fun v => Val.xorl v (Vlong n)).
+Proof.
+  unfold xorlimm; intros; red; intros.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero.
+  exists x; split; auto. subst. destruct x; simpl; auto. rewrite Int64.xor_zero; auto.
+  destruct (xorlimm_match a); InvEval; subst.
+- econstructor; split. apply eval_longconst. simpl. rewrite Int64.xor_commut; auto.
+- rewrite Val.xorl_assoc. simpl. rewrite (Int64.xor_commut n2).
+  predSpec Int64.eq Int64.eq_spec (Int64.xor n n2) Int64.zero.
++ rewrite H. exists v1; split; auto. destruct v1; simpl; auto. rewrite Int64.xor_zero; auto. 
++ TrivialExists.
+- TrivialExists.
+Qed.
+
+Theorem eval_xorl: binary_constructor_sound xorl Val.xorl.
+Proof.
+  unfold xorl; destruct Archi.splitlong. apply SplitLongproof.eval_xorl.
+  red; intros. destruct (xorl_match a b).
+- InvEval. rewrite Val.xorl_commut. apply eval_xorlimm; auto.
+- InvEval. apply eval_xorlimm; auto.
+- TrivialExists.
+Qed.
+
+Theorem eval_notl: unary_constructor_sound notl Val.notl.
+Proof.
+  unfold notl; destruct Archi.splitlong. apply SplitLongproof.eval_notl.
+  red; intros. rewrite Val.notl_xorl. apply eval_xorlimm; auto.
+Qed.
+
 Theorem eval_divls_base: partial_binary_constructor_sound divls_base Val.divls.
 Proof.
   unfold divls_base; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_divls_base; eauto.
   TrivialExists.
+  cbn.
+  rewrite H1.
+  cbn.
+  trivial.
 Qed.
 
 Theorem eval_modls_base: partial_binary_constructor_sound modls_base Val.modls.
@@ -467,6 +466,10 @@ Proof.
   unfold modls_base; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_modls_base; eauto.
   TrivialExists.
+  cbn.
+  rewrite H1.
+  cbn.
+  trivial.
 Qed.
 
 Theorem eval_divlu_base: partial_binary_constructor_sound divlu_base Val.divlu.
@@ -474,6 +477,10 @@ Proof.
   unfold divlu_base; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_divlu_base; eauto.
   TrivialExists.
+  cbn.
+  rewrite H1.
+  cbn.
+  trivial.
 Qed.
 
 Theorem eval_modlu_base: partial_binary_constructor_sound modlu_base Val.modlu.
@@ -481,6 +488,27 @@ Proof.
   unfold modlu_base; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_modlu_base; eauto.
   TrivialExists.
+  cbn.
+  rewrite H1.
+  cbn.
+  trivial.
+Qed.
+
+Theorem eval_shrxlimm:
+  forall le a n x z,
+  eval_expr ge sp e m le a x ->
+  Val.shrxl x (Vint n) = Some z ->
+  exists v, eval_expr ge sp e m le (shrxlimm a n) v /\ Val.lessdef z v.
+Proof.
+  unfold shrxlimm; intros. destruct Archi.splitlong eqn:SL.
++ eapply SplitLongproof.eval_shrxlimm; eauto using Archi.splitlong_ptr32.
++ predSpec Int.eq Int.eq_spec n Int.zero.
+- subst n. destruct x; simpl in H0; inv H0. econstructor; split; eauto.
+  change (Int.ltu Int.zero (Int.repr 63)) with true. simpl. rewrite Int64.shrx'_zero; auto.
+- TrivialExists.
+  cbn.
+  rewrite H0.
+  reflexivity.
 Qed.
 
 Theorem eval_cmplu:
@@ -530,6 +558,15 @@ Proof.
   unfold longoffloat; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_longoffloat; eauto.
   TrivialExists.
+  cbn; rewrite H0; reflexivity.
+Qed.
+
+Theorem eval_longuoffloat: partial_unary_constructor_sound longuoffloat Val.longuoffloat.
+Proof.
+  unfold longuoffloat; red; intros. destruct Archi.splitlong eqn:SL.
+  eapply SplitLongproof.eval_longuoffloat; eauto.
+  TrivialExists.
+  cbn; rewrite H0; reflexivity.
 Qed.
 
 Theorem eval_floatoflong: partial_unary_constructor_sound floatoflong Val.floatoflong.
@@ -537,6 +574,15 @@ Proof.
   unfold floatoflong; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_floatoflong; eauto.
   TrivialExists.
+  cbn; rewrite H0; reflexivity.
+Qed.
+
+Theorem eval_floatoflongu: partial_unary_constructor_sound floatoflongu Val.floatoflongu.
+Proof.
+  unfold floatoflongu; red; intros. destruct Archi.splitlong eqn:SL.
+  eapply SplitLongproof.eval_floatoflongu; eauto.
+  TrivialExists.
+  cbn; rewrite H0; reflexivity.
 Qed.
 
 Theorem eval_longofsingle: partial_unary_constructor_sound longofsingle Val.longofsingle.
@@ -544,6 +590,15 @@ Proof.
   unfold longofsingle; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_longofsingle; eauto.
   TrivialExists.
+  cbn; rewrite H0; reflexivity.
+Qed.
+
+Theorem eval_longuofsingle: partial_unary_constructor_sound longuofsingle Val.longuofsingle.
+Proof.
+  unfold longuofsingle; red; intros. destruct Archi.splitlong eqn:SL.
+  eapply SplitLongproof.eval_longuofsingle; eauto.
+  TrivialExists.
+  cbn; rewrite H0; reflexivity.
 Qed.
 
 Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong.
@@ -551,6 +606,15 @@ Proof.
   unfold singleoflong; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_singleoflong; eauto.
   TrivialExists.
+  cbn; rewrite H0; reflexivity.
+Qed.
+
+Theorem eval_singleoflongu: partial_unary_constructor_sound singleoflongu Val.singleoflongu.
+Proof.
+  unfold singleoflongu; red; intros. destruct Archi.splitlong eqn:SL.
+  eapply SplitLongproof.eval_singleoflongu; eauto.
+  TrivialExists.
+  cbn; rewrite H0; reflexivity.
 Qed.
 
 End CMCONSTR.