some more proof for fake hsval checker expansions

2 files changed, 771 insertions, 46 deletions

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index d3805738..11a66322 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -388,7 +388,7 @@ let expanse (sb : superblock) code pm =
           debug "Iop/Ccomp\n";
           exp := cond_int32s false c a1 a2 dest succ [];
           was_exp := true
-      (*| Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) ->
+      | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) ->
           debug "Iop/Ccompu\n";
           exp := cond_int32u false c a1 a2 dest succ [];
           was_exp := true
@@ -432,7 +432,7 @@ let expanse (sb : superblock) code pm =
           debug "Iop/Cnotcompfs\n";
           exp := expanse_cond_fp true cond_single c f1 f2 dest succ [];
           was_exp := true
-      | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) ->
+      (*| Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) ->
           debug "Icond/Ccomp\n";
           exp := cbranch_int32s false c a1 a2 info succ1 succ2 [];
           was_branch := true;
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
index b9fe504e..7b20db6c 100644
--- a/riscV/RTLpathSE_simplify.v
+++ b/riscV/RTLpathSE_simplify.v
@@ -1,7 +1,9 @@
+Require Import Coqlib Floats Values Memory.
 Require Import Integers.
 Require Import Op Registers.
 Require Import RTLpathSE_theory.
 Require Import RTLpathSE_simu_specs.
+Require Import Asmgen Asmgenproof1.
 
 (* Useful functions for conditions/branches expansion *)
 
@@ -26,6 +28,69 @@ Definition make_lhsv_single (hvs: hsval) : list_hsval :=
 
 (* Expansion functions *)
 
+Definition load_hilo32 (hi lo: int) :=
+  if Int.eq lo Int.zero then
+    fSop (OEluiw hi) fSnil
+  else
+    let hvs := fSop (OEluiw hi) fSnil in
+    let hl := make_lhsv_single hvs in
+    fSop (Oaddimm lo) hl.
+
+Definition load_hilo64 (hi lo: int64) :=
+  if Int64.eq lo Int64.zero then
+    fSop (OEluil hi) fSnil
+  else
+    let hvs := fSop (OEluil hi) fSnil in
+    let hl := make_lhsv_single hvs in
+    fSop (Oaddlimm lo) hl.
+
+Definition loadimm32 (n: int) :=
+  match make_immed32 n with
+  | Imm32_single imm =>
+      fSop (OEaddiwr0 imm) fSnil
+  | Imm32_pair hi lo => load_hilo32 hi lo
+  end.
+
+Definition loadimm64 (n: int64) :=
+  match make_immed64 n with
+  | Imm64_single imm =>
+      fSop (OEaddilr0 imm) fSnil
+  | Imm64_pair hi lo => load_hilo64 hi lo
+  | Imm64_large imm => fSop (OEloadli imm) fSnil
+  end.
+
+Definition opimm32 (hv1: hsval) (n: int) (op: operation) (opimm: int -> operation) :=
+  match make_immed32 n with
+  | Imm32_single imm =>
+      let hl := make_lhsv_single hv1 in
+      fSop (opimm imm) hl
+  | Imm32_pair hi lo =>
+      let hvs := load_hilo32 hi lo in
+      let hl := make_lhsv_cmp false hv1 hvs in
+      fSop op hl
+  end.
+
+Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> operation) :=
+  match make_immed64 n with
+  | Imm64_single imm =>
+      let hl := make_lhsv_single hv1 in
+      fSop (opimm imm) hl
+  | Imm64_pair hi lo =>
+      let hvs := load_hilo64 hi lo in
+      let hl := make_lhsv_cmp false hv1 hvs in
+      fSop op hl
+  | Imm64_large imm =>
+      let hvs := fSop (OEloadli imm) fSnil in
+      let hl := make_lhsv_cmp false hv1 hvs in
+      fSop op hl
+  end.
+
+Definition xorimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oxor OExoriw.
+Definition sltimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw.
+Definition sltuimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw.
+Definition xorimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oxorl OExoril.
+Definition sltimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil.
+Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul.
 Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
   match cmp with
   | Ceq => fSop (OEseqw optR0) lhsv
@@ -37,78 +102,706 @@ Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool)
       fSop (OExoriw Int.one) hl
   end.
 
+Definition cond_int32u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
+  match cmp with
+  | Ceq => fSop (OEsequw optR0) lhsv
+  | Cne => fSop (OEsneuw optR0) lhsv
+  | Clt | Cgt => fSop (OEsltuw optR0) lhsv
+  | Cle | Cge =>
+      let hvs := (fSop (OEsltuw optR0) lhsv) in
+      let hl := make_lhsv_single hvs in
+      fSop (OExoriw Int.one) hl
+  end.
+
+Definition cond_int64s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
+  match cmp with
+  | Ceq => fSop (OEseql optR0) lhsv
+  | Cne => fSop (OEsnel optR0) lhsv
+  | Clt | Cgt => fSop (OEsltl optR0) lhsv
+  | Cle | Cge =>
+      let hvs := (fSop (OEsltl optR0) lhsv) in
+      let hl := make_lhsv_single hvs in
+      fSop (OExoriw Int.one) hl
+  end.
+
+Definition cond_int64u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
+  match cmp with
+  | Ceq => fSop (OEsequl optR0) lhsv
+  | Cne => fSop (OEsneul optR0) lhsv
+  | Clt | Cgt => fSop (OEsltul optR0) lhsv
+  | Cle | Cge =>
+      let hvs := (fSop (OEsltul optR0) lhsv) in
+      let hl := make_lhsv_single hvs in
+      fSop (OExoriw Int.one) hl
+  end.
+
+Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) :=
+  let is_inv := is_inv_cmp_int cmp in
+  if Int.eq n Int.zero then
+    let optR0 := make_optR0 true is_inv in
+    let hl := make_lhsv_cmp is_inv hv1 hv1 in
+    cond_int32s cmp hl optR0
+  else
+    match cmp with
+    | Ceq | Cne =>
+        let optR0 := make_optR0 true is_inv in
+        let hvs := xorimm32 hv1 n in
+        let hl := make_lhsv_cmp false hvs hvs in
+        cond_int32s cmp hl optR0
+    | Clt => sltimm32 hv1 n
+    | Cle =>
+        if Int.eq n (Int.repr Int.max_signed) then
+          loadimm32 Int.one
+        else sltimm32 hv1 (Int.add n Int.one)
+    | _ =>
+        let optR0 := make_optR0 false is_inv in
+        let hvs := loadimm32 n in
+        let hl := make_lhsv_cmp is_inv hv1 hvs in
+        cond_int32s cmp hl optR0
+    end.
+
+Definition expanse_condimm_int32u (cmp: comparison) (hv1: hsval) (n: int) :=
+  let is_inv := is_inv_cmp_int cmp in
+  if Int.eq n Int.zero then
+    let optR0 := make_optR0 true is_inv in
+    let hl := make_lhsv_cmp is_inv hv1 hv1 in
+    cond_int32u cmp hl optR0
+  else
+    match cmp with
+    | Clt => sltuimm32 hv1 n
+    | _ =>
+        let optR0 := make_optR0 false is_inv in
+        let hvs := loadimm32 n in
+        let hl := make_lhsv_cmp is_inv hv1 hvs in
+        cond_int32u cmp hl optR0
+    end.
+
+Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) :=
+  let is_inv := is_inv_cmp_int cmp in
+  if Int64.eq n Int64.zero then
+    let optR0 := make_optR0 true is_inv in
+    let hl := make_lhsv_cmp is_inv hv1 hv1 in
+    cond_int64s cmp hl optR0
+  else
+    match cmp with
+    | Ceq | Cne =>
+        let optR0 := make_optR0 true is_inv in
+        let hvs := xorimm64 hv1 n in
+        let hl := make_lhsv_cmp false hvs hvs in
+        cond_int64s cmp hl optR0
+    | Clt => sltimm64 hv1 n
+    | Cle =>
+        if Int64.eq n (Int64.repr Int64.max_signed) then
+          loadimm32 Int.one
+        else sltimm64 hv1 (Int64.add n Int64.one)
+    | _ =>
+        let optR0 := make_optR0 false is_inv in
+        let hvs := loadimm64 n in
+        let hl := make_lhsv_cmp is_inv hv1 hvs in
+        cond_int64s cmp hl optR0
+    end.
+
+Definition expanse_condimm_int64u (cmp: comparison) (hv1: hsval) (n: int64) :=
+  let is_inv := is_inv_cmp_int cmp in
+  if Int64.eq n Int64.zero then
+    let optR0 := make_optR0 true is_inv in
+    let hl := make_lhsv_cmp is_inv hv1 hv1 in
+    cond_int64u cmp hl optR0
+  else
+    match cmp with
+    | Clt => sltuimm64 hv1 n
+    | _ =>
+        let optR0 := make_optR0 false is_inv in
+        let hvs := loadimm64 n in
+        let hl := make_lhsv_cmp is_inv hv1 hvs in
+        cond_int64u cmp hl optR0
+    end.
+
+Definition cond_float (cmp: comparison) (lhsv: list_hsval) :=
+  match cmp with
+  | Ceq | Cne => fSop OEfeqd lhsv
+  | Clt | Cgt => fSop OEfltd lhsv
+  | Cle | Cge => fSop OEfled lhsv
+  end.
+
+Definition cond_single (cmp: comparison) (lhsv: list_hsval) :=
+  match cmp with
+  | Ceq | Cne => fSop OEfeqs lhsv
+  | Clt | Cgt => fSop OEflts lhsv
+  | Cle | Cge => fSop OEfles lhsv
+  end.
+
+Definition is_normal_cmp cmp :=
+  match cmp with | Cne => false | _ => true end.
+
+Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) :=
+  let normal := is_normal_cmp cmp in
+  let normal' := if cnot then negb normal else normal in
+  let hvs := fn_cond cmp lhsv in
+  let hl := make_lhsv_single hvs in
+  if normal' then hvs else fSop (OExoriw Int.one) hl.
+
 (* Target op simplifications using "fake" values *)
 
 Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
   match op, lr with
   | Ocmp (Ccomp c), a1 :: a2 :: nil =>
-      let fv1 := fsi_sreg_get hst a1 in
-      let fv2 := fsi_sreg_get hst a2 in
+      let hv1 := fsi_sreg_get hst a1 in
+      let hv2 := fsi_sreg_get hst a2 in
       let is_inv := is_inv_cmp_int c in
       let optR0 := make_optR0 false is_inv in
-      let lhsv := make_lhsv_cmp is_inv fv1 fv2 in
+      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
       Some (cond_int32s c lhsv optR0)
-
-      (*| Ocmp (Ccompu c), a1 :: a2 :: nil =>
-      DO hv1 <~ hsi_sreg_get hst a1;;
-      DO hv2 <~ hsi_sreg_get hst a2;;
+  | Ocmp (Ccompu c), a1 :: a2 :: nil =>
+      let hv1 := fsi_sreg_get hst a1 in
+      let hv2 := fsi_sreg_get hst a2 in
       let is_inv := is_inv_cmp_int c in
       let optR0 := make_optR0 false is_inv in
-      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
-      cond_int32u c lhsv optR0
+      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
+      Some (cond_int32u c lhsv optR0)
   | Ocmp (Ccompimm c imm), a1 :: nil =>
-      DO hv1 <~ hsi_sreg_get hst a1;;
-      expanse_condimm_int32s c hv1 imm
+      let hv1 := fsi_sreg_get hst a1 in
+      Some (expanse_condimm_int32s c hv1 imm)
   | Ocmp (Ccompuimm c imm), a1 :: nil =>
-      DO hv1 <~ hsi_sreg_get hst a1;;
-      expanse_condimm_int32u c hv1 imm
+      let hv1 := fsi_sreg_get hst a1 in
+      Some (expanse_condimm_int32u c hv1 imm)
   | Ocmp (Ccompl c), a1 :: a2 :: nil =>
-      DO hv1 <~ hsi_sreg_get hst a1;;
-      DO hv2 <~ hsi_sreg_get hst a2;;
+      let hv1 := fsi_sreg_get hst a1 in
+      let hv2 := fsi_sreg_get hst a2 in
       let is_inv := is_inv_cmp_int c in
       let optR0 := make_optR0 false is_inv in
-      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
-      cond_int64s c lhsv optR0
+      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
+      Some (cond_int64s c lhsv optR0)
   | Ocmp (Ccomplu c), a1 :: a2 :: nil =>
-      DO hv1 <~ hsi_sreg_get hst a1;;
-      DO hv2 <~ hsi_sreg_get hst a2;;
+      let hv1 := fsi_sreg_get hst a1 in
+      let hv2 := fsi_sreg_get hst a2 in
       let is_inv := is_inv_cmp_int c in
       let optR0 := make_optR0 false is_inv in
-      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
-      cond_int64u c lhsv optR0
+      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
+      Some (cond_int64u c lhsv optR0)
   | Ocmp (Ccomplimm c imm), a1 :: nil =>
-      DO hv1 <~ hsi_sreg_get hst a1;;
-      expanse_condimm_int64s c hv1 imm
+      let hv1 := fsi_sreg_get hst a1 in
+      Some (expanse_condimm_int64s c hv1 imm)
   | Ocmp (Ccompluimm c imm), a1 :: nil =>
-      DO hv1 <~ hsi_sreg_get hst a1;;
-      expanse_condimm_int64u c hv1 imm
+      let hv1 := fsi_sreg_get hst a1 in
+      Some (expanse_condimm_int64u c hv1 imm)
   | Ocmp (Ccompf c), f1 :: f2 :: nil =>
-      DO hv1 <~ hsi_sreg_get hst f1;;
-      DO hv2 <~ hsi_sreg_get hst f2;;
+      let hv1 := fsi_sreg_get hst f1 in
+      let hv2 := fsi_sreg_get hst f2 in
       let is_inv := is_inv_cmp_float c in
-      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
-      expanse_cond_fp false cond_float c lhsv
+      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
+      Some (expanse_cond_fp false cond_float c lhsv)
   | Ocmp (Cnotcompf c), f1 :: f2 :: nil =>
-      DO hv1 <~ hsi_sreg_get hst f1;;
-      DO hv2 <~ hsi_sreg_get hst f2;;
+      let hv1 := fsi_sreg_get hst f1 in
+      let hv2 := fsi_sreg_get hst f2 in
       let is_inv := is_inv_cmp_float c in
-      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
-      expanse_cond_fp true cond_float c lhsv
+      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
+      Some (expanse_cond_fp true cond_float c lhsv)
   | Ocmp (Ccompfs c), f1 :: f2 :: nil =>
-      DO hv1 <~ hsi_sreg_get hst f1;;
-      DO hv2 <~ hsi_sreg_get hst f2;;
+      let hv1 := fsi_sreg_get hst f1 in
+      let hv2 := fsi_sreg_get hst f2 in
       let is_inv := is_inv_cmp_float c in
-      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
-      expanse_cond_fp false cond_single c lhsv
+      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
+      Some (expanse_cond_fp false cond_single c lhsv)
   | Ocmp (Cnotcompfs c), f1 :: f2 :: nil =>
-      DO hv1 <~ hsi_sreg_get hst f1;;
-      DO hv2 <~ hsi_sreg_get hst f2;;
+      let hv1 := fsi_sreg_get hst f1 in
+      let hv2 := fsi_sreg_get hst f2 in
       let is_inv := is_inv_cmp_float c in
-      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
-         expanse_cond_fp true cond_single c lhsv*)
+      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
+      Some (expanse_cond_fp true cond_single c lhsv)
   | _, _ => None
   end.
 
+(* Auxiliary lemmas on comparisons *)
+
+Lemma xor_neg_ltle_cmp: forall v1 v2,
+  Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmp_bool Cle v2 v1)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  unfold Val.cmp; simpl;
+  try rewrite Int.eq_sym;
+  try destruct (Int.eq _ _); try destruct (Int.lt _ _) eqn:ELT ; simpl;
+  try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one;
+  auto.
+Qed.
+
+Lemma xor_neg_ltle_cmpu: forall mptr v1 v2,
+  Some (Val.xor (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer mptr) Cle v2 v1)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  unfold Val.cmpu; simpl;
+  try rewrite Int.eq_sym;
+  try destruct (Int.eq _ _); try destruct (Int.ltu _ _) eqn:ELT ; simpl;
+  try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one;
+  auto.
+  1,2:
+    unfold Val.cmpu, Val.cmpu_bool;
+    destruct Archi.ptr64; try destruct (_ && _); try destruct (_ || _);
+    try destruct (eq_block _ _); auto.
+  unfold Val.cmpu, Val.cmpu_bool; simpl;
+  destruct Archi.ptr64; try destruct (_ || _); simpl; auto;
+  destruct (eq_block b b0); destruct (eq_block b0 b);
+  try congruence;
+  try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _);
+  simpl; auto;
+  repeat destruct (_ && _); simpl; auto.
+Qed.
+
+Lemma xor_neg_ltle_cmpl: forall v1 v2,
+  Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmpl_bool Cle v2 v1)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  destruct (Int64.lt _ _); auto.
+Qed.
+
+Lemma xor_neg_ltge_cmpl: forall v1 v2,
+  Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmpl_bool Cge v1 v2)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  destruct (Int64.lt _ _); auto.
+Qed.
+
+Lemma xor_neg_ltle_cmplu: forall mptr v1 v2,
+  Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cle v2 v1)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  destruct (Int64.ltu _ _); auto.
+  1,2: unfold Val.cmplu; simpl; auto;
+  destruct (Archi.ptr64); simpl;
+  try destruct (eq_block _ _); simpl;
+  try destruct (_ && _); simpl;
+  try destruct (Ptrofs.cmpu _ _);
+  try destruct cmp; simpl; auto.
+  unfold Val.cmplu; simpl;
+  destruct Archi.ptr64; try destruct (_ || _); simpl; auto;
+  destruct (eq_block b b0); destruct (eq_block b0 b);
+  try congruence;
+  try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _);
+  simpl; auto;
+  repeat destruct (_ && _); simpl; auto.
+Qed.
+
+Lemma xor_neg_ltge_cmplu: forall mptr v1 v2,
+  Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cge v1 v2)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  destruct (Int64.ltu _ _); auto.
+  1,2: unfold Val.cmplu; simpl; auto;
+  destruct (Archi.ptr64); simpl;
+  try destruct (eq_block _ _); simpl;
+  try destruct (_ && _); simpl;
+  try destruct (Ptrofs.cmpu _ _);
+  try destruct cmp; simpl; auto.
+  unfold Val.cmplu; simpl;
+  destruct Archi.ptr64; try destruct (_ || _); simpl; auto;
+  destruct (eq_block b b0); destruct (eq_block b0 b);
+  try congruence;
+  try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _);
+  simpl; auto;
+  repeat destruct (_ && _); simpl; auto.
+Qed.
+
+Lemma xor_neg_eqne_cmpf: forall v1 v2,
+  Some (Val.xor (Val.cmpf Ceq v1 v2) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmpf_bool Cne v1 v2)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence;
+  unfold Val.cmpf; simpl.
+  rewrite Float.cmp_ne_eq.
+  destruct (Float.cmp _ _ _); simpl; auto.
+Qed.
+
+Lemma xor_neg_eqne_cmpfs: forall v1 v2,
+  Some (Val.xor (Val.cmpfs Ceq v1 v2) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmpfs_bool Cne v1 v2)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence;
+  unfold Val.cmpfs; simpl.
+  rewrite Float32.cmp_ne_eq.
+  destruct (Float32.cmp _ _ _); simpl; auto.
+Qed.
+
+Lemma xor_neg_optb: forall v,
+  Some (Val.xor (Val.of_optbool (option_map negb v))
+    (Vint Int.one)) = Some (Val.of_optbool v).
+Proof.
+  intros.
+  destruct v; simpl; trivial.
+  destruct b; simpl; auto.
+Qed.
+
+Lemma xor_neg_optb': forall v,
+  Some (Val.xor (Val.of_optbool v) (Vint Int.one)) =
+  Some (Val.of_optbool (option_map negb v)).
+Proof.
+  intros.
+  destruct v; simpl; trivial.
+  destruct b; simpl; auto.
+Qed.
+
+Lemma optbool_mktotal: forall v,
+  Val.maketotal (option_map Val.of_bool v) =
+  Val.of_optbool v.
+Proof.
+  intros.
+  destruct v; simpl; auto.
+Qed.
+
+(* TODO gourdinl move to common/Values ? *)
+Theorem swap_cmpf_bool:
+  forall c x y,
+  Val.cmpf_bool (swap_comparison c) x y = Val.cmpf_bool c y x.
+Proof.
+  destruct x; destruct y; simpl; auto. rewrite Float.cmp_swap. auto.
+Qed.
+
+Theorem swap_cmpfs_bool:
+  forall c x y,
+  Val.cmpfs_bool (swap_comparison c) x y = Val.cmpfs_bool c y x.
+Proof.
+  destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto.
+Qed.
+
+(* Intermediates lemmas on each expansed instruction *)
+
+Lemma simplify_ccomp_correct ge sp hst st c r r0 rs0 m0 v v0: forall
+  (SREG: forall r: positive,
+          hsi_sreg_eval ge sp hst r rs0 m0 =
+          seval_sval ge sp (si_sreg st r) rs0 m0)
+  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
+  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0),
+  seval_sval ge sp
+    (hsval_proj
+       (cond_int32s c
+          (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r)
+             (fsi_sreg_get hst r0)) None)) rs0 m0 =
+  Some (Val.of_optbool (Val.cmp_bool c v v0)).
+Proof.
+  intros.
+  unfold cond_int32s in *; destruct c; simpl;
+  erewrite !fsi_sreg_get_correct; eauto;
+  rewrite OKv1, OKv2; trivial;
+  unfold Val.cmp.
+  - apply xor_neg_ltle_cmp.
+  - replace (Clt) with (swap_comparison Cgt) by auto;
+    rewrite Val.swap_cmp_bool; trivial.
+  - replace (Clt) with (negate_comparison Cge) by auto;
+    rewrite Val.negate_cmp_bool.
+    rewrite xor_neg_optb; trivial.
+Qed.
+
+Lemma simplify_ccompu_correct ge sp hst st c r r0 rs0 m m0 v v0: forall
+  (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
+           seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
+           Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
+  (SREG: forall r: positive,
+          hsi_sreg_eval ge sp hst r rs0 m0 =
+          seval_sval ge sp (si_sreg st r) rs0 m0)
+  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
+  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0)
+  (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m),
+  seval_sval ge sp
+    (hsval_proj
+       (cond_int32u c
+          (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r)
+             (fsi_sreg_get hst r0)) None)) rs0 m0 =
+  Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) c v v0)).
+Proof.
+  intros.
+  erewrite (cmpu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)).
+  2: eauto.
+  unfold cond_int32u in *; destruct c; simpl;
+  erewrite !fsi_sreg_get_correct; eauto;
+  rewrite OKv1, OKv2; trivial;
+  unfold Val.cmpu.
+  - apply xor_neg_ltle_cmpu.
+  - replace (Clt) with (swap_comparison Cgt) by auto;
+    rewrite Val.swap_cmpu_bool; trivial.
+  - replace (Clt) with (negate_comparison Cge) by auto;
+    rewrite Val.negate_cmpu_bool.
+    rewrite xor_neg_optb; trivial.
+Qed.
+
+Lemma simplify_ccompuimm_correct ge sp hst st c r n rs0 m m0 v: forall
+  (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
+           seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
+           Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
+  (SREG: forall r: positive,
+          hsi_sreg_eval ge sp hst r rs0 m0 =
+          seval_sval ge sp (si_sreg st r) rs0 m0)
+  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
+  (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m),
+  seval_sval ge sp
+    (hsval_proj (expanse_condimm_int32u c (fsi_sreg_get hst r) n)) rs0 m0 =
+  Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) c v (Vint n))).
+Proof.
+  intros.
+  assert (HMEM: Val.cmpu_bool (Mem.valid_pointer m) c v (Vint n) =
+          Val.cmpu_bool (Mem.valid_pointer m0) c v (Vint n)).
+  erewrite (cmpu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)); eauto.
+  unfold expanse_condimm_int32u, cond_int32u in *; destruct c;
+  intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl;
+  unfold loadimm32, sltuimm32, opimm32, load_hilo32;
+  try erewrite !fsi_sreg_get_correct; eauto;
+  try rewrite OKv1; trivial;
+  unfold Val.cmpu, zero32.
+  (* Simplify make immediate and decompose subcases *)
+  all:
+    try (specialize make_immed32_sound with n;
+    destruct (make_immed32 n) eqn:EQMKI);
+    try destruct (Int.eq lo Int.zero) eqn:EQLO;
+    try erewrite fSop_correct; eauto; simpl;
+    try erewrite !fsi_sreg_get_correct; eauto;
+    try rewrite OKv1;
+    try rewrite OK2;
+    rewrite HMEM.
+  (* Ceq, Cne, Clt = itself *)
+  all: intros; try apply Int.same_if_eq in EQIMM; subst; trivial.
+  (* Cle = xor (Clt) *)
+  all: try apply xor_neg_ltle_cmpu; trivial.
+  (* Others subcases with swap/negation *)
+  all:
+    unfold Val.cmpu;
+    try apply Int.same_if_eq in EQLO; subst;
+    try rewrite Int.add_commut, Int.add_zero_l in *; trivial;
+    try (rewrite <- xor_neg_ltle_cmpu; unfold Val.cmpu;
+    trivial; fail);
+    try (replace (Clt) with (swap_comparison Cgt) by auto;
+    rewrite Val.swap_cmpu_bool; trivial; fail);
+    try (replace (Clt) with (negate_comparison Cge) by auto;
+    rewrite Val.negate_cmpu_bool; rewrite xor_neg_optb; trivial; fail).
+  all: rewrite HMEM; trivial.
+Qed.
+
+Lemma simplify_ccompl_correct ge sp hst st c r r0 rs0 m0 v v0: forall
+  (SREG: forall r: positive,
+          hsi_sreg_eval ge sp hst r rs0 m0 =
+          seval_sval ge sp (si_sreg st r) rs0 m0)
+  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
+  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0),
+  seval_sval ge sp
+    (hsval_proj
+       (cond_int64s c
+          (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r)
+             (fsi_sreg_get hst r0)) None)) rs0 m0 =
+  Some (Val.of_optbool (Val.cmpl_bool c v v0)).
+Proof.
+  intros.
+  unfold cond_int64s in *; destruct c; simpl;
+  erewrite !fsi_sreg_get_correct; eauto;
+  rewrite OKv1, OKv2; trivial;
+  unfold Val.cmpl.
+  1,2,3: rewrite optbool_mktotal; trivial.
+  - apply xor_neg_ltle_cmpl.
+  - replace (Clt) with (swap_comparison Cgt) by auto;
+    rewrite Val.swap_cmpl_bool; trivial.
+    rewrite optbool_mktotal; trivial.
+  - apply xor_neg_ltge_cmpl.
+Qed.
+
+Lemma simplify_ccomplu_correct ge sp hst st c r r0 rs0 m m0 v v0: forall
+  (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
+           seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
+           Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
+  (SREG: forall r: positive,
+          hsi_sreg_eval ge sp hst r rs0 m0 =
+          seval_sval ge sp (si_sreg st r) rs0 m0)
+  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
+  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0)
+  (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m),
+  seval_sval ge sp
+    (hsval_proj
+       (cond_int64u c
+          (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r)
+             (fsi_sreg_get hst r0)) None)) rs0 m0 =
+  Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) c v v0)).
+Proof.
+  intros.
+  erewrite (cmplu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)).
+  2: eauto.
+  unfold cond_int64u in *; destruct c; simpl;
+  erewrite !fsi_sreg_get_correct; eauto;
+  rewrite OKv1, OKv2; trivial;
+  unfold Val.cmplu.
+  1,2,3: rewrite optbool_mktotal; trivial.
+  - apply xor_neg_ltle_cmplu.
+  - replace (Clt) with (swap_comparison Cgt) by auto;
+    rewrite Val.swap_cmplu_bool; trivial.
+    rewrite optbool_mktotal; trivial.
+  - apply xor_neg_ltge_cmplu.
+Qed.
+
+Lemma simplify_ccompluimm_correct ge sp hst st c r n rs0 m m0 v: forall
+  (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
+           seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
+           Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
+  (SREG: forall r: positive,
+          hsi_sreg_eval ge sp hst r rs0 m0 =
+          seval_sval ge sp (si_sreg st r) rs0 m0)
+  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
+  (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m),
+  seval_sval ge sp
+    (hsval_proj (expanse_condimm_int64u c (fsi_sreg_get hst r) n)) rs0 m0 =
+  Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) c v (Vlong n))).
+Proof.
+  intros.
+  assert (HMEM: Val.cmplu_bool (Mem.valid_pointer m) c v (Vlong n) =
+          Val.cmplu_bool (Mem.valid_pointer m0) c v (Vlong n)).
+  erewrite (cmplu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)); eauto.
+  unfold expanse_condimm_int64u, cond_int64u in *; destruct c;
+  intros; destruct (Int64.eq n Int64.zero) eqn:EQIMM; simpl;
+  unfold loadimm64, sltuimm64, opimm64, load_hilo64;
+  try erewrite !fsi_sreg_get_correct; eauto;
+  try rewrite OKv1;
+  unfold Val.cmplu, zero64.
+  (* Simplify make immediate and decompose subcases *)
+  all:
+    try (specialize make_immed64_sound with n;
+    destruct (make_immed64 n) eqn:EQMKI);
+    try destruct (Int64.eq lo Int64.zero) eqn:EQLO;
+    try erewrite fSop_correct; eauto; simpl;
+    try erewrite !fsi_sreg_get_correct; eauto;
+    try rewrite OKv1;
+    try rewrite OK2;
+    rewrite HMEM.
+  (* Ceq, Cne, Clt = itself *)
+  all: intros; try apply Int64.same_if_eq in EQIMM; subst; trivial.
+  (* Cle = xor (Clt) *)
+  all: try apply xor_neg_ltle_cmplu; trivial.
+  (* Others subcases with swap/negation *)
+  all:
+    unfold Val.cmplu;
+    try apply Int64.same_if_eq in EQLO; subst;
+    try rewrite Int64.add_commut, Int64.add_zero_l in *; trivial;
+    try (rewrite <- xor_neg_ltle_cmplu; unfold Val.cmplu;
+    trivial; fail);
+    try (replace (Clt) with (swap_comparison Cgt) by auto;
+    rewrite Val.swap_cmplu_bool; trivial; fail);
+    try (replace (Clt) with (negate_comparison Cge) by auto;
+    rewrite Val.negate_cmplu_bool; rewrite xor_neg_optb; trivial; fail);
+    rewrite optbool_mktotal; trivial.
+  all:
+    try rewrite HMEM; trivial;
+    rewrite <- xor_neg_ltge_cmplu; unfold Val.cmplu; rewrite <- optbool_mktotal; trivial.
+Qed.
+
+Lemma simplify_ccompf_correct ge sp hst st c r r0 rs0 m0 v v0: forall
+  (SREG: forall r: positive,
+          hsi_sreg_eval ge sp hst r rs0 m0 =
+          seval_sval ge sp (si_sreg st r) rs0 m0)
+  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
+  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0),
+  seval_sval ge sp
+    (hsval_proj
+       (expanse_cond_fp false cond_float c
+          (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r)
+             (fsi_sreg_get hst r0)))) rs0 m0 =
+  Some (Val.of_optbool (Val.cmpf_bool c v v0)).
+Proof.
+  intros.
+  unfold expanse_cond_fp in *; destruct c; simpl;
+  erewrite !fsi_sreg_get_correct; eauto;
+  rewrite OKv1, OKv2; trivial;
+  unfold Val.cmpf.
+  - apply xor_neg_eqne_cmpf.
+  - replace (Clt) with (swap_comparison Cgt) by auto;
+    rewrite swap_cmpf_bool; trivial.
+  - replace (Cle) with (swap_comparison Cge) by auto;
+    rewrite swap_cmpf_bool; trivial.
+Qed.
+
+Lemma simplify_cnotcompf_correct ge sp hst st c r r0 rs0 m0 v v0: forall
+  (SREG: forall r: positive,
+          hsi_sreg_eval ge sp hst r rs0 m0 =
+          seval_sval ge sp (si_sreg st r) rs0 m0)
+  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
+  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0),
+  seval_sval ge sp
+    (hsval_proj
+       (expanse_cond_fp true cond_float c
+          (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r)
+             (fsi_sreg_get hst r0)))) rs0 m0 =
+  Some (Val.of_optbool (option_map negb (Val.cmpf_bool c v v0))).
+Proof.
+  intros.
+  unfold expanse_cond_fp in *; destruct c; simpl;
+  erewrite !fsi_sreg_get_correct; eauto;
+  rewrite OKv1, OKv2; trivial;
+  unfold Val.cmpf.
+  1,3,4: apply xor_neg_optb'.
+  all: destruct v, v0; simpl; trivial.
+  rewrite Float.cmp_ne_eq; rewrite negb_involutive; trivial.
+  1: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float.cmp_swap; simpl.
+  2: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float.cmp_swap; simpl.
+  all: destruct (Float.cmp _ _ _); trivial.
+Qed.
+
+Lemma simplify_ccompfs_correct ge sp hst st c r r0 rs0 m0 v v0: forall
+  (SREG: forall r: positive,
+          hsi_sreg_eval ge sp hst r rs0 m0 =
+          seval_sval ge sp (si_sreg st r) rs0 m0)
+  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
+  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0),
+  seval_sval ge sp
+    (hsval_proj
+       (expanse_cond_fp false cond_single c
+          (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r)
+             (fsi_sreg_get hst r0)))) rs0 m0 =
+  Some (Val.of_optbool (Val.cmpfs_bool c v v0)).
+Proof.
+  intros.
+  unfold expanse_cond_fp in *; destruct c; simpl;
+  erewrite !fsi_sreg_get_correct; eauto;
+  rewrite OKv1, OKv2; trivial;
+  unfold Val.cmpfs.
+  - apply xor_neg_eqne_cmpfs.
+  - replace (Clt) with (swap_comparison Cgt) by auto;
+    rewrite swap_cmpfs_bool; trivial.
+  - replace (Cle) with (swap_comparison Cge) by auto;
+    rewrite swap_cmpfs_bool; trivial.
+Qed.
+
+Lemma simplify_cnotcompfs_correct ge sp hst st c r r0 rs0 m0 v v0: forall
+  (SREG: forall r: positive,
+          hsi_sreg_eval ge sp hst r rs0 m0 =
+          seval_sval ge sp (si_sreg st r) rs0 m0)
+  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
+  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0),
+  seval_sval ge sp
+    (hsval_proj
+       (expanse_cond_fp true cond_single c
+          (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r)
+             (fsi_sreg_get hst r0)))) rs0 m0 =
+  Some (Val.of_optbool (option_map negb (Val.cmpfs_bool c v v0))).
+Proof.
+  intros.
+  unfold expanse_cond_fp in *; destruct c; simpl;
+  erewrite !fsi_sreg_get_correct; eauto;
+  rewrite OKv1, OKv2; trivial;
+  unfold Val.cmpfs.
+  1,3,4: apply xor_neg_optb'.
+  all: destruct v, v0; simpl; trivial.
+  rewrite Float32.cmp_ne_eq; rewrite negb_involutive; trivial.
+  1: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float32.cmp_swap; simpl.
+  2: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float32.cmp_swap; simpl.
+  all: destruct (Float32.cmp _ _ _); trivial.
+Qed.
+
+(* Main proof of simplification *)
 
 Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall
    (H: target_op_simplify op lr hst = Some fsv)
@@ -117,8 +810,40 @@ Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall
    (OK1: seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args)
    (OK2: seval_smem ge sp (si_smem st) rs0 m0 = Some m),
    seval_sval ge sp (hsval_proj fsv) rs0 m0 = eval_operation ge sp op args m.
-Proof. Admitted. (*
-  unfold target_op_simplify; simpl. congruence.
-                    Qed.*)
+Proof.
+  unfold target_op_simplify; simpl.
+  intros H (LREF & SREF & SREG & SMEM) ? ? ?.
+  destruct op; try congruence.
+  destruct cond; repeat (destruct lr; simpl; try congruence);
+  simpl in OK1;
+  try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence);
+  try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence);
+  inv H; inv OK1.
+  (* Ccomp *)
+  - eapply simplify_ccomp_correct; eauto.
+  (* Ccompu *)
+  - eapply simplify_ccompu_correct; eauto.
+  (* Ccompimm *)
+  - (* TODO gourdinl *) admit.
+  (* Ccompuimm *)
+  - eapply simplify_ccompuimm_correct; eauto.
+  (* Ccompl *)
+  - eapply simplify_ccompl_correct; eauto.
+  (* Ccomplu *)
+  - eapply simplify_ccomplu_correct; eauto.
+  (* Ccomplimm *)
+  - admit.
+  (* Ccompluimm *)
+  - eapply simplify_ccompluimm_correct; eauto.
+  (* Ccompf *)
+  - eapply simplify_ccompf_correct; eauto.
+  (* Cnotcompf *)
+  - eapply simplify_cnotcompf_correct; eauto.
+  (* Ccompfs *)
+  - eapply simplify_ccompfs_correct; eauto.
+  (* Cnotcompfs *)
+  - eapply simplify_cnotcompfs_correct; eauto.
+      Admitted.
+(*Qed.*)
 Global Opaque target_op_simplify.