path: root/aarch64/SelectLongproof.v

(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*         Xavier Leroy, Collège de France and INRIA Paris             *)
(*                                                                     *)
(*  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 64-bit integer operators *)

Require Import Coqlib Zbits.
Require Import AST Integers Floats Values Memory Globalenvs.
Require Import Cminor Op CminorSel.
Require Import SelectOp SelectLong SelectOpproof.
Require Import OpHelpers OpHelpersproof.

Local Open Scope cminorsel_scope.
Local Transparent Archi.ptr64.

(** * Correctness of the smart constructors *)

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.

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.

Definition partial_unary_constructor_sound (cstr: expr -> expr) (sem: val -> option val) : Prop :=
  forall le a x y,
  eval_expr ge sp e m le a x ->
  sem x = Some y ->
  exists v, eval_expr ge sp e m le (cstr a) v /\ Val.lessdef y v.

Definition partial_binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> val -> option val) : Prop :=
  forall le a x b y z,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  sem x y = Some z ->
  exists v, eval_expr ge sp e m le (cstr a b) v /\ Val.lessdef z v.

(** ** Constants *)

Theorem eval_longconst:
  forall le n, eval_expr ge sp e m le (longconst n) (Vlong n).
Proof.
  intros; EvalOp.
Qed.

(** ** Conversions *)

Theorem eval_intoflong: unary_constructor_sound intoflong Val.loword.
Proof.
  unfold intoflong; red; intros until x; destruct (intoflong_match a); intros; InvEval; subst.
- TrivialExists.
- TrivialExists.
Qed.

Theorem eval_longofintu: unary_constructor_sound longofintu Val.longofintu.
Proof.
  unfold longofintu; red; intros until x; destruct (longofintu_match a); intros; InvEval; subst.
- TrivialExists.
- TrivialExists. simpl. unfold eval_extend. rewrite mk_amount64_eq by reflexivity.
  destruct x; simpl; auto. rewrite Int64.shl'_zero. auto.
Qed.

Theorem eval_longofint: unary_constructor_sound longofint Val.longofint.
Proof.
  unfold longofint; red; intros until x; destruct (longofint_match a); intros; InvEval; subst.
- TrivialExists.
- TrivialExists. simpl. unfold eval_extend. rewrite mk_amount64_eq by reflexivity.
  destruct x; simpl; auto. rewrite Int64.shl'_zero. auto.
Qed.

(** ** Addition, opposite, subtraction *)

Theorem eval_addlimm:
  forall n, unary_constructor_sound (addlimm n) (fun x => Val.addl x (Vlong n)).
Proof.
  red; unfold addlimm; intros until x.
  predSpec Int64.eq Int64.eq_spec n Int64.zero.
- subst n. intros. exists x; split; auto.
  destruct x; simpl; auto.
  rewrite Int64.add_zero; auto.
  rewrite Ptrofs.add_zero; auto.
- case (addlimm_match a); intros; InvEval; subst.
+ rewrite Int64.add_commut; TrivialExists.
+ TrivialExists. simpl. rewrite Ptrofs.add_commut, Genv.shift_symbol_address_64; auto.
+ econstructor; split. EvalOp. destruct sp; simpl; auto. 
  rewrite Ptrofs.add_assoc, (Ptrofs.add_commut m0); auto.
+ rewrite Val.addl_assoc, Int64.add_commut; TrivialExists.  
+ TrivialExists.
Qed.

Theorem eval_addl: binary_constructor_sound addl Val.addl.
Proof.
  red; intros until y.
  unfold addl; case (addl_match a b); intros; InvEval; subst.
- rewrite Val.addl_commut. apply eval_addlimm; auto.
- apply eval_addlimm; auto.
- 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.
- TrivialExists. simpl. 
  rewrite Val.addl_commut, Val.addl_assoc. f_equal; f_equal. 
  destruct sp; simpl; auto. rewrite Ptrofs.add_assoc, (Ptrofs.add_commut n2). auto.
- TrivialExists. simpl.
  rewrite <- (Val.addl_commut v1), <- (Val.addl_commut (Val.addl v1 (Vlong n2))).
  rewrite Val.addl_assoc. f_equal; f_equal.
  destruct sp; simpl; auto. rewrite Ptrofs.add_assoc. auto.
- 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.
- rewrite <- Val.addl_assoc. apply eval_addlimm. EvalOp.
- rewrite Val.addl_commut. TrivialExists.
- TrivialExists.
- rewrite Val.addl_commut. TrivialExists.
- TrivialExists.
- rewrite Val.addl_commut. TrivialExists.
- TrivialExists.
- TrivialExists.
Qed.

Theorem eval_negl: unary_constructor_sound negl (fun v => Val.subl (Vlong Int64.zero) v).
Proof.
  red; intros until x; unfold negl. case (negl_match a); intros; InvEval; subst.
- TrivialExists.
- TrivialExists.
- TrivialExists.
Qed.

Theorem eval_subl: binary_constructor_sound subl Val.subl.
Proof.
  red; intros until y; unfold subl; case (subl_match a b); intros; InvEval; subst.
- rewrite Val.subl_addl_opp. apply eval_addlimm; auto.
- 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.
- rewrite Val.subl_addl_l. apply eval_addlimm; EvalOp.
- rewrite Val.subl_addl_r. apply eval_addlimm; EvalOp.
- TrivialExists.
- TrivialExists.
- TrivialExists.
- TrivialExists.
Qed.

(** ** Immediate shifts *)

Remark eval_shllimm_base: forall le a n x,
  eval_expr ge sp e m le a x ->
  Int.ltu n Int64.iwordsize' = true ->
  eval_expr ge sp e m le (shllimm_base a n) (Val.shll x (Vint n)).
Proof.
Local Opaque mk_amount64.
  unfold shlimm_base; intros; EvalOp. simpl. rewrite mk_amount64_eq by auto. auto.
Qed.

Theorem eval_shllimm:
  forall n, unary_constructor_sound (fun a => shllimm a n)
                                    (fun x => Val.shll x (Vint n)).
Proof.
  red; intros until x; unfold shllimm.
  predSpec Int.eq Int.eq_spec n Int.zero; [| destruct (Int.ltu n Int64.iwordsize') eqn:L]; simpl.
- intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int64.shl'_zero; auto.
- destruct (shllimm_match a); intros; InvEval; subst.
+ TrivialExists. simpl; rewrite L; auto.
+ destruct (Int.ltu (Int.add a n) Int64.iwordsize') eqn:L2.
* econstructor; split. eapply eval_shllimm_base; eauto.
  destruct v1; simpl; auto. rewrite a64_range; simpl. rewrite L, L2. 
  rewrite Int64.shl'_shl'; auto using a64_range.
* econstructor; split; [|eauto]. apply eval_shllimm_base; auto. EvalOp.
+ TrivialExists. simpl. rewrite mk_amount64_eq; auto.
+ TrivialExists. simpl. rewrite mk_amount64_eq; auto.
+ destruct (Int.ltu (Int.add a n) Int64.iwordsize') eqn:L2.
* TrivialExists. simpl. rewrite mk_amount64_eq by auto. 
  destruct (Val.zero_ext_l s v1); simpl; auto.
  rewrite a64_range; simpl; rewrite L, L2.
  rewrite Int64.shl'_shl'; auto using a64_range.
* econstructor; split. eapply eval_shllimm_base; eauto. EvalOp; simpl; eauto. auto.
+ destruct (Int.ltu (Int.add a n) Int64.iwordsize') eqn:L2.
* TrivialExists. simpl. rewrite mk_amount64_eq by auto. 
  destruct (Val.sign_ext_l s v1); simpl; auto.
  rewrite a64_range; simpl; rewrite L, L2.
  rewrite Int64.shl'_shl'; auto using a64_range.
* econstructor; split. eapply eval_shllimm_base; eauto. EvalOp; simpl; eauto. auto.
+ destruct (Int.ltu (Int.add a n) Int64.iwordsize') eqn:L2.
* TrivialExists. simpl. unfold eval_extend. rewrite mk_amount64_eq by auto. 
  destruct (match x0 with Xsgn32 => Val.longofint v1 | Xuns32 => Val.longofintu v1 end); simpl; auto.
  rewrite a64_range; simpl; rewrite L, L2.
  rewrite Int64.shl'_shl'; auto using a64_range.
* econstructor; split. eapply eval_shllimm_base; eauto. EvalOp; simpl; eauto. auto.
+ econstructor; eauto using eval_shllimm_base.
- intros; TrivialExists.
Qed.

Remark eval_shrluimm_base: forall le a n x,
  eval_expr ge sp e m le a x ->
  Int.ltu n Int64.iwordsize' = true ->
  eval_expr ge sp e m le (shrluimm_base a n) (Val.shrlu x (Vint n)).
Proof.
  unfold shrluimm_base; intros; EvalOp. simpl. rewrite mk_amount64_eq by auto. auto.
Qed.

Remark sub_shift_amount:
  forall y z,
  Int.ltu y Int64.iwordsize' = true -> Int.ltu z Int64.iwordsize' = true -> Int.unsigned y <= Int.unsigned z ->
  Int.ltu (Int.sub z y) Int64.iwordsize' = true.
Proof.
  intros. unfold Int.ltu; apply zlt_true.
  apply Int.ltu_inv in H. apply Int.ltu_inv in H0.
  change (Int.unsigned Int64.iwordsize') with Int64.zwordsize in *.
  unfold Int.sub; rewrite Int.unsigned_repr. lia.
  assert (Int64.zwordsize < Int.max_unsigned) by reflexivity. lia.
Qed.

Theorem eval_shrluimm:
  forall n, unary_constructor_sound (fun a => shrluimm a n)
                                    (fun x => Val.shrlu x (Vint n)).
Proof.
Local Opaque Int64.zwordsize.
  red; intros until x; unfold shrluimm.
  predSpec Int.eq Int.eq_spec n Int.zero; [| destruct (Int.ltu n Int64.iwordsize') eqn:L]; simpl.
- intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int64.shru'_zero; auto.
- destruct (shrluimm_match a); intros; InvEval; subst.
+ TrivialExists. simpl; rewrite L; auto.
+ destruct (Int.ltu n a) eqn:L2.
* assert (L3: Int.ltu (Int.sub a n) Int64.iwordsize' = true).
  { apply sub_shift_amount; auto using a64_range.
    apply Int.ltu_inv in L2. lia. }
  econstructor; split. EvalOp.
  destruct v1; simpl; auto. rewrite mk_amount64_eq, L3, a64_range by auto.
  simpl. rewrite L. rewrite Int64.shru'_shl', L2 by auto using a64_range. auto.
* assert (L3: Int.ltu (Int.sub n a) Int64.iwordsize' = true).
  { apply sub_shift_amount; auto using a64_range.
    unfold Int.ltu in L2. destruct zlt in L2; discriminate || lia. }
  econstructor; split. EvalOp.
  destruct v1; simpl; auto. rewrite mk_amount64_eq, L3, a64_range by auto.
  simpl. rewrite L. rewrite Int64.shru'_shl', L2 by auto using a64_range. auto.
+ destruct (Int.ltu (Int.add a n) Int64.iwordsize') eqn:L2.
* econstructor; split. eapply eval_shrluimm_base; eauto.
  destruct v1; simpl; auto. rewrite a64_range; simpl. rewrite L, L2. 
  rewrite Int64.shru'_shru'; auto using a64_range.
* econstructor; split; [|eauto]. apply eval_shrluimm_base; auto. EvalOp.
+ destruct (zlt (Int.unsigned n) s).
* econstructor; split. EvalOp. rewrite mk_amount64_eq by auto.
  destruct v1; simpl; auto. rewrite ! L; simpl.
  set (s' := s - Int.unsigned n).
  replace s with (s' + Int.unsigned n) by (unfold s'; lia).
  rewrite Int64.shru'_zero_ext. auto. unfold s'; lia.
* econstructor; split. EvalOp.
  destruct v1; simpl; auto. rewrite ! L; simpl.
  rewrite Int64.shru'_zero_ext_0 by lia. auto. 
+ econstructor; eauto using eval_shrluimm_base.
- intros; TrivialExists.
Qed.

Remark eval_shrlimm_base: forall le a n x,
  eval_expr ge sp e m le a x ->
  Int.ltu n Int64.iwordsize' = true ->
  eval_expr ge sp e m le (shrlimm_base a n) (Val.shrl x (Vint n)).
Proof.
  unfold shrlimm_base; intros; EvalOp. simpl. rewrite mk_amount64_eq by auto. auto.
Qed.

Theorem eval_shrlimm:
  forall n, unary_constructor_sound (fun a => shrlimm a n)
                                    (fun x => Val.shrl x (Vint n)).
Proof.
  red; intros until x; unfold shrlimm.
  predSpec Int.eq Int.eq_spec n Int.zero; [| destruct (Int.ltu n Int64.iwordsize') eqn:L]; simpl.
- intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int64.shr'_zero; auto.
- destruct (shrlimm_match a); intros; InvEval; subst.
+ TrivialExists. simpl; rewrite L; auto.
+ destruct (Int.ltu n a) eqn:L2.
* assert (L3: Int.ltu (Int.sub a n) Int64.iwordsize' = true).
  { apply sub_shift_amount; auto using a64_range.
    apply Int.ltu_inv in L2. lia. }
  econstructor; split. EvalOp.
  destruct v1; simpl; auto. rewrite mk_amount64_eq, L3, a64_range by auto.
  simpl. rewrite L. rewrite Int64.shr'_shl', L2 by auto using a64_range. auto.
* assert (L3: Int.ltu (Int.sub n a) Int64.iwordsize' = true).
  { apply sub_shift_amount; auto using a64_range.
    unfold Int.ltu in L2. destruct zlt in L2; discriminate || lia. }
  econstructor; split. EvalOp.
  destruct v1; simpl; auto. rewrite mk_amount64_eq, L3, a64_range by auto.
  simpl. rewrite L. rewrite Int64.shr'_shl', L2 by auto using a64_range. auto.
+ destruct (Int.ltu (Int.add a n) Int64.iwordsize') eqn:L2.
* econstructor; split. eapply eval_shrlimm_base; eauto.
  destruct v1; simpl; auto. rewrite a64_range; simpl. rewrite L, L2. 
  rewrite Int64.shr'_shr'; auto using a64_range.
* econstructor; split; [|eauto]. apply eval_shrlimm_base; auto. EvalOp.
+ destruct (zlt (Int.unsigned n) s && zlt s Int64.zwordsize) eqn:E.
* InvBooleans. econstructor; split. EvalOp. rewrite mk_amount64_eq by auto.
  destruct v1; simpl; auto. rewrite ! L; simpl.
  set (s' := s - Int.unsigned n).
  replace s with (s' + Int.unsigned n) by (unfold s'; lia).
  rewrite Int64.shr'_sign_ext. auto. unfold s'; lia. unfold s'; lia.
* econstructor; split; [|eauto]. apply eval_shrlimm_base; auto. EvalOp.
+ econstructor; eauto using eval_shrlimm_base.
- intros; TrivialExists.
Qed.

(** ** Multiplication *)

Lemma eval_mullimm_base:
  forall n, unary_constructor_sound (mullimm_base n) (fun x => Val.mull x (Vlong n)).
Proof.
  intros; red; intros; unfold mullimm_base.
  assert (DFL: exists v, eval_expr ge sp e m le (Eop Omull (Eop (Olongconst n) Enil ::: a ::: Enil)) v /\ Val.lessdef (Val.mull x (Vlong n)) v).
  { rewrite Val.mull_commut; TrivialExists. } 
  generalize (Int64.one_bits'_decomp n); generalize (Int64.one_bits'_range n);
  destruct (Int64.one_bits' n) as [ | i [ | j []]]; intros P Q.
- apply DFL.
- replace (Val.mull x (Vlong n)) with (Val.shll x (Vint i)).
  apply eval_shllimm; auto.
  simpl in Q. destruct x; auto; simpl. rewrite P by auto with coqlib.
  rewrite Q, Int64.add_zero, Int64.shl'_mul. auto.
- exploit (eval_shllimm i (x :: le) (Eletvar 0) x). constructor; auto. intros [v1 [A1 B1]].
  exploit (eval_shllimm j (x :: le) (Eletvar 0) x). constructor; auto. intros [v2 [A2 B2]].
  exploit (eval_addl (x :: le)). eexact A1. eexact A2. intros [v [A B]].
  exists v; split. econstructor; eauto.
  simpl in Q. rewrite Q, Int64.add_zero. eapply Val.lessdef_trans; [|eexact B].
  eapply Val.lessdef_trans; [|eapply Val.addl_lessdef; eauto].
  destruct x; simpl; auto; rewrite ! P by auto with coqlib.
  rewrite Int64.mul_add_distr_r, <- ! Int64.shl'_mul. auto.
- apply DFL.
Qed.

Theorem eval_mullimm:
  forall n, unary_constructor_sound (mullimm n) (fun x => Val.mull x (Vlong n)).
Proof.
  intros; red; intros until x; unfold mullimm.
  predSpec Int64.eq Int64.eq_spec n Int64.zero.
  intros. exists (Vlong Int64.zero); split. EvalOp.
  destruct x; simpl; auto. subst n. rewrite Int64.mul_zero. auto.
  predSpec Int64.eq Int64.eq_spec n Int64.one.
  intros. exists x; split; auto.
  destruct x; simpl; auto. subst n. rewrite Int64.mul_one. auto.
  case (mullimm_match a); intros; InvEval; subst.
- TrivialExists. simpl. rewrite Int64.mul_commut; auto.
- rewrite Val.mull_addl_distr_l.
  exploit eval_mullimm_base; eauto. instantiate (1 := n). intros [v' [A1 B1]].
  exploit (eval_addlimm (Int64.mul n n2) le (mullimm_base n t2) v'). auto. intros [v'' [A2 B2]].
  exists v''; split; auto. eapply Val.lessdef_trans. eapply Val.addl_lessdef; eauto.
  rewrite Val.mull_commut; auto.
- apply eval_mullimm_base; auto.
Qed.

Theorem eval_mull: binary_constructor_sound mull Val.mull.
Proof.
  red; intros until y; unfold mull; case (mull_match a b); intros; InvEval; subst.
- rewrite Val.mull_commut. apply eval_mullimm; auto.
- apply eval_mullimm; auto.
- TrivialExists.
Qed.

Theorem eval_mullhu: 
  forall n, unary_constructor_sound (fun a => mullhu a n) (fun v => Val.mullhu v (Vlong n)).
Proof.
  unfold mullhu; red; intros; TrivialExists.
Qed.

Theorem eval_mullhs: 
  forall n, unary_constructor_sound (fun a => mullhs a n) (fun v => Val.mullhs v (Vlong n)).
Proof.
  unfold mullhs; red; intros; TrivialExists.
Qed.

(** Integer conversions *)

Theorem eval_zero_ext_l:
  forall sz, 0 <= sz -> unary_constructor_sound (zero_ext_l sz) (Val.zero_ext_l sz).
Proof.
  intros; red; intros until x; unfold zero_ext_l; case (zero_ext_l_match a); intros; InvEval; subst.
- TrivialExists.
- TrivialExists.
- destruct (zlt (Int.unsigned a0) sz).
+ econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite a64_range; simpl.
  apply Val.lessdef_same. f_equal. rewrite Int64.shl'_zero_ext by lia. f_equal. lia.
+ TrivialExists.
- TrivialExists.
Qed.

(** Bitwise not, and, or, xor *)

Theorem eval_notl: unary_constructor_sound notl Val.notl.
Proof.
  assert (INV: forall v, Val.lessdef (Val.notl (Val.notl v)) v).
  { destruct v; auto. simpl; rewrite Int64.not_involutive; auto. } 
  unfold notl; red; intros until x; case (notl_match a); intros; InvEval; subst.
- TrivialExists.
- TrivialExists.
- exists v1; auto.
- exists (eval_shiftl s v1 a0); split; auto. EvalOp.
- econstructor; split. EvalOp. 
  destruct v1; simpl; auto; destruct v0; simpl; auto.
  rewrite Int64.not_and_or_not, Int64.not_involutive, Int64.or_commut. auto.
- econstructor; split. EvalOp. 
  destruct v1; simpl; auto; destruct v0; simpl; auto.
  rewrite Int64.not_or_and_not, Int64.not_involutive, Int64.and_commut. auto.
- econstructor; split. EvalOp.
  destruct v1; simpl; auto; destruct v0; simpl; auto.
  unfold Int64.not; rewrite ! Int64.xor_assoc. auto.
- econstructor; split. EvalOp.
  destruct v1; simpl; auto; destruct v0; simpl; auto.
  unfold Int64.not; rewrite ! Int64.xor_assoc, Int64.xor_idem, Int64.xor_zero. auto.
- TrivialExists.
Qed.

Lemma eval_andlimm_base:
  forall n, unary_constructor_sound (andlimm_base n) (fun x => Val.andl x (Vlong n)).
Proof.
  intros; red; intros. unfold andlimm_base.
  predSpec Int64.eq Int64.eq_spec n Int64.zero.
  exists (Vlong Int64.zero); split. EvalOp.
  destruct x; simpl; auto. subst n. rewrite Int64.and_zero. auto.
  predSpec Int64.eq Int64.eq_spec n Int64.mone.
  exists x; split; auto.
  subst. destruct x; simpl; auto. rewrite Int64.and_mone; auto.
  destruct (Z_is_power2m1 (Int64.unsigned n)) as [s|] eqn:P.
  assert (0 <= s) by (eapply Z_is_power2m1_nonneg; eauto).
  rewrite <- (Int64.repr_unsigned n), (Z_is_power2m1_sound _ _ P), <- Val.zero_ext_andl by auto.
  apply eval_zero_ext_l; auto.
  TrivialExists.
Qed.

Theorem eval_andlimm:
  forall n, unary_constructor_sound (andlimm n) (fun x => Val.andl x (Vlong n)).
Proof.
  intros; red; intros until x. unfold andlimm.
  case (andlimm_match a); intros; InvEval; subst.
- rewrite Int64.and_commut; TrivialExists.
- rewrite Val.andl_assoc, Int64.and_commut. apply eval_andlimm_base; auto.
- destruct (zle 0 s).
+ replace (Val.zero_ext_l s v1) with (Val.andl v1 (Vlong (Int64.repr (two_p s - 1)))).
  rewrite Val.andl_assoc, Int64.and_commut.
  apply eval_andlimm_base; auto.
  destruct v1; simpl; auto. rewrite Int64.zero_ext_and by auto. auto. 
+ apply eval_andlimm_base. EvalOp.
- apply eval_andlimm_base; auto.
Qed.

Theorem eval_andl: binary_constructor_sound andl Val.andl.
Proof.
  red; intros until y; unfold andl; case (andl_match a b); intros; InvEval; subst.
- rewrite Val.andl_commut; apply eval_andlimm; auto.
- apply eval_andlimm; auto.
- rewrite Val.andl_commut; TrivialExists.
- TrivialExists.
- rewrite Val.andl_commut; TrivialExists.
- TrivialExists.
- rewrite Val.andl_commut; TrivialExists.
- TrivialExists.
- TrivialExists.
Qed.

Theorem eval_orlimm:
  forall n, unary_constructor_sound (orlimm n) (fun x => Val.orl x (Vlong n)).
Proof.
  intros; red; intros until x. unfold orlimm.
  predSpec Int64.eq Int64.eq_spec n Int64.zero.
  intros. subst. exists x; split; auto.
  destruct x; simpl; auto. rewrite Int64.or_zero; auto.
  predSpec Int64.eq Int64.eq_spec n Int64.mone.
  intros. exists (Vlong Int64.mone); split. EvalOp.
  destruct x; simpl; auto. subst n. rewrite Int64.or_mone. auto.
  destruct (orlimm_match a); intros; InvEval; subst.
- rewrite Int64.or_commut; TrivialExists.
- rewrite Val.orl_assoc, Int64.or_commut; TrivialExists.
- TrivialExists.
Qed.

Theorem eval_orl: binary_constructor_sound orl Val.orl.
Proof.
  red; intros until y; unfold orl; case (orl_match a b); intros; InvEval; subst.
- rewrite Val.orl_commut. apply eval_orlimm; auto.
- apply eval_orlimm; auto.
- rewrite Val.orl_commut; TrivialExists.
- TrivialExists.
- rewrite Val.orl_commut; TrivialExists.
- TrivialExists.
- (* shl - shru *)
  destruct (Int.eq (Int.add a1 a2) Int64.iwordsize' && same_expr_pure t1 t2) eqn:?.
+ InvBooleans. apply Int.same_if_eq in H.
  exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst.
  econstructor; split. EvalOp.
  destruct v0; simpl; auto. rewrite ! a64_range. simpl. rewrite <- Int64.or_ror'; auto using a64_range.
+ TrivialExists.
- (* shru - shl *)
  destruct (Int.eq (Int.add a2 a1) Int64.iwordsize' && same_expr_pure t1 t2) eqn:?.
+ InvBooleans. apply Int.same_if_eq in H.
  exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst.
  econstructor; split. EvalOp.
  destruct v0; simpl; auto. rewrite ! a64_range. simpl.
  rewrite Int64.or_commut, <- Int64.or_ror'; auto using a64_range.
+ TrivialExists.
- rewrite Val.orl_commut; TrivialExists.
- TrivialExists.
- TrivialExists.
Qed.

Lemma eval_xorlimm_base:
  forall n, unary_constructor_sound (xorlimm_base n) (fun x => Val.xorl x (Vlong n)).
Proof.
  intros; red; intros. unfold xorlimm_base.
  predSpec Int64.eq Int64.eq_spec n Int64.zero.
  intros. exists x; split. auto.
  destruct x; simpl; auto. subst n. rewrite Int64.xor_zero. auto.
  predSpec Int64.eq Int64.eq_spec n Int64.mone.
  subst n. change (Val.xorl x (Vlong Int64.mone)) with (Val.notl x). apply eval_notl; auto.
  TrivialExists.
Qed.

Theorem eval_xorlimm:
  forall n, unary_constructor_sound (xorlimm n) (fun x => Val.xorl x (Vlong n)).
Proof.
  intros; red; intros until x. unfold xorlimm.
  destruct (xorlimm_match a); intros; InvEval; subst.
- rewrite Int64.xor_commut; TrivialExists.
- rewrite Val.xorl_assoc; simpl. rewrite (Int64.xor_commut n2). apply eval_xorlimm_base; auto.
- apply eval_xorlimm_base; auto.
Qed.

Theorem eval_xorl: binary_constructor_sound xorl Val.xorl.
Proof.
  red; intros until y; unfold xorl; case (xorl_match a b); intros; InvEval; subst.
- rewrite Val.xorl_commut; apply eval_xorlimm; auto.
- apply eval_xorlimm; auto.
- rewrite Val.xorl_commut; TrivialExists.
- TrivialExists.
- rewrite Val.xorl_commut; TrivialExists.
- TrivialExists.
- rewrite Val.xorl_commut; TrivialExists.
- TrivialExists.
- TrivialExists.
Qed.

(** ** Integer division and modulus *)

Theorem eval_divls_base: partial_binary_constructor_sound divls_base Val.divls.
Proof.
  red; intros; unfold divls_base; TrivialExists.
  cbn. rewrite H1. reflexivity.
Qed.

Theorem eval_modls_base: partial_binary_constructor_sound modls_base Val.modls.
Proof.
  red; intros; unfold modls_base, modl_aux.
  exploit Val.modls_divls; eauto. intros (q & A & B). subst z.
  TrivialExists. repeat (econstructor; eauto with evalexpr).
  rewrite A. reflexivity.
Qed.

Theorem eval_divlu_base: partial_binary_constructor_sound divlu_base Val.divlu.
Proof.
  red; intros; unfold divlu_base; TrivialExists.
  cbn. rewrite H1. reflexivity.
Qed.

Theorem eval_modlu_base: partial_binary_constructor_sound modlu_base Val.modlu.
Proof.
  red; intros; unfold modlu_base, modl_aux.
  exploit Val.modlu_divlu; eauto. intros (q & A & B). subst z.
  TrivialExists. repeat (econstructor; eauto with evalexpr).
  rewrite A. reflexivity.
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.
  intros; unfold shrxlimm. 
  predSpec Int.eq Int.eq_spec n Int.zero.
- subst n. exists x; split; auto.
  destruct x; simpl in H0; try discriminate.
  change (Int.ltu Int.zero (Int.repr 63)) with true in H0; inv H0.
  rewrite Int64.shrx'_zero. auto.
- TrivialExists. cbn. rewrite H0. reflexivity.
Qed.

(** General shifts *)

Theorem eval_shll: binary_constructor_sound shll Val.shll.
Proof.
  red; intros until y; unfold shll; case (shll_match b); intros.
  InvEval. apply eval_shllimm; auto.
  TrivialExists.
Qed.

Theorem eval_shrl: binary_constructor_sound shrl Val.shrl.
Proof.
  red; intros until y; unfold shrl; case (shrl_match b); intros.
  InvEval. apply eval_shrlimm; auto.
  TrivialExists.
Qed.

Theorem eval_shrlu: binary_constructor_sound shrlu Val.shrlu.
Proof.
  red; intros until y; unfold shrlu; case (shrlu_match b); intros.
  InvEval. apply eval_shrluimm; auto.
  TrivialExists.
Qed.

(** Comparisons *)

Remark option_map_of_bool_inv: forall ov w,
  option_map Val.of_bool ov = Some w -> Val.of_optbool ov = w.
Proof.
  intros. destruct ov; inv H; auto.
Qed.

Section COMP_IMM.

Variable default: comparison -> int64 -> condition.
Variable intsem: comparison -> int64 -> int64 -> bool.
Variable sem: comparison -> val -> val -> option val.

Hypothesis sem_int: forall c x y, 
  sem c (Vlong x) (Vlong y) = Some (Val.of_bool (intsem c x y)).
Hypothesis sem_undef: forall c v,
  sem c Vundef v = None.
Hypothesis sem_eq: forall x y,
  sem Ceq (Vlong x) (Vlong y) = Some (Val.of_bool (Int64.eq x y)).
Hypothesis sem_ne: forall x y,
  sem Cne (Vlong x) (Vlong y) = Some (Val.of_bool (negb (Int64.eq x y))).
Hypothesis sem_default: forall c v n,
  sem c v (Vlong n) = option_map Val.of_bool (eval_condition (default c n) (v :: nil) m).

Lemma eval_complimm_default: forall le a x c n2 v,
  sem c x (Vlong n2) = Some v ->
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le (Eop (Ocmp (default c n2)) (a:::Enil)) v.
Proof.
  intros. EvalOp. simpl. rewrite sem_default in H. apply option_map_of_bool_inv in H.
  congruence.
Qed.

Lemma eval_complimm:
  forall le c a n2 x v,
  eval_expr ge sp e m le a x ->
  sem c x (Vlong n2) = Some v ->
  eval_expr ge sp e m le (complimm default intsem c a n2) v.
Proof.
  intros until x; unfold complimm; case (complimm_match c a); intros; InvEval; subst.
- (* constant *)
  rewrite sem_int in H0; inv H0. EvalOp. destruct (intsem c0 n1 n2); auto.
- (* mask zero *)
  predSpec Int64.eq Int64.eq_spec n2 Int64.zero.
+ subst n2. destruct v1; simpl in H0; rewrite ? sem_undef, ? sem_eq in H0; inv H0.
  EvalOp.
+ eapply eval_complimm_default; eauto. EvalOp. 
- (* mask not zero *)
  predSpec Int64.eq Int64.eq_spec n2 Int64.zero.
+ subst n2. destruct v1; simpl in H0; rewrite ? sem_undef, ? sem_ne in H0; inv H0.
  EvalOp.
+ eapply eval_complimm_default; eauto. EvalOp.
- (* default *)
  eapply eval_complimm_default; eauto.
Qed.

Hypothesis sem_swap:
  forall c x y, sem (swap_comparison c) x y = sem c y x.

Lemma eval_complimm_swap:
  forall le c a n2 x v,
  eval_expr ge sp e m le a x ->
  sem c (Vlong n2) x = Some v ->
  eval_expr ge sp e m le (complimm default intsem (swap_comparison c) a n2) v.
Proof.
  intros. eapply eval_complimm; eauto. rewrite sem_swap; auto.
Qed.

End COMP_IMM.

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 until y; unfold cmpl; case (cmpl_match a b); intros; InvEval; subst.
- apply eval_complimm_swap with (sem := Val.cmpl) (x := y); auto.
  intros; unfold Val.cmpl; rewrite Val.swap_cmpl_bool; auto. 
- apply eval_complimm with (sem := Val.cmpl) (x := x); auto.
- EvalOp. simpl. rewrite Val.swap_cmpl_bool. apply option_map_of_bool_inv in H1. congruence.
- EvalOp. simpl. apply option_map_of_bool_inv in H1. congruence.
- EvalOp. simpl. apply option_map_of_bool_inv in H1. congruence.
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 (Mem.valid_pointer m) c x y = Some v ->
  eval_expr ge sp e m le (cmplu c a b) v.
Proof.
  intros until y; unfold cmplu; case (cmplu_match a b); intros; InvEval; subst.
- apply eval_complimm_swap with (sem := Val.cmplu (Mem.valid_pointer m)) (x := y); auto.
  intros; unfold Val.cmplu; rewrite Val.swap_cmplu_bool; auto. 
- apply eval_complimm with (sem := Val.cmplu (Mem.valid_pointer m)) (x := x); auto.
- EvalOp. simpl. rewrite Val.swap_cmplu_bool. apply option_map_of_bool_inv in H1. congruence.
- EvalOp. simpl. apply option_map_of_bool_inv in H1. congruence.
- EvalOp. simpl. apply option_map_of_bool_inv in H1. congruence.
Qed.


(** Floating-point conversions *)

Theorem eval_longoffloat: partial_unary_constructor_sound longoffloat Val.longoffloat.
Proof.
  red; intros; TrivialExists. cbn. rewrite H0. reflexivity.
Qed.

Theorem eval_longuoffloat: partial_unary_constructor_sound longuoffloat Val.longuoffloat.
Proof.
  red; intros; TrivialExists. cbn. rewrite H0. reflexivity.
Qed.

Theorem eval_floatoflong: partial_unary_constructor_sound floatoflong Val.floatoflong.
Proof.
  red; intros; TrivialExists.  cbn. rewrite H0. reflexivity.
Qed.

Theorem eval_floatoflongu: partial_unary_constructor_sound floatoflongu Val.floatoflongu.
Proof.
  red; intros; TrivialExists. cbn. rewrite H0. reflexivity.
Qed.

Theorem eval_longofsingle: partial_unary_constructor_sound longofsingle Val.longofsingle.
Proof.
  red; intros; TrivialExists. cbn. rewrite H0. reflexivity.
Qed.

Theorem eval_longuofsingle: partial_unary_constructor_sound longuofsingle Val.longuofsingle.
Proof.
  red; intros; TrivialExists. cbn. rewrite H0. reflexivity.
Qed.

Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong.
Proof.
  red; intros; TrivialExists. cbn. rewrite H0. reflexivity.
Qed.

Theorem eval_singleoflongu: partial_unary_constructor_sound singleoflongu Val.singleoflongu.
Proof.
  red; intros; TrivialExists. cbn. rewrite H0. reflexivity.
Qed.

End CMCONSTR.