Select condition x < 0 with x unsigned leads to falsev3.9_kvx_fix1

Squashed commit of the following:

commit 808e72db2022d05a4e34818b33cc9af17aaa4df0
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date:   Fri Sep 17 14:53:39 2021 +0200

    selectOp for comp0

commit f38e1f15359cceb3c0764635336125a1ceae78ff
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date:   Fri Sep 17 14:49:45 2021 +0200

    SelectOp for ccomp0 ok

commit ca969280380a593aef590a1fe2ec6f0fc112c2f5
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date:   Fri Sep 17 14:46:01 2021 +0200

    progress

commit e60a970f541ae6be30ec51cf95d60eb672ade829
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date:   Fri Sep 17 14:40:49 2021 +0200

    progres sur ltu etc.

commit 6f7d51e59a61d43fca06b1b4bad6dedada6e031e
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date:   Fri Sep 17 14:13:07 2021 +0200

    change selection

commit c2af349c6dd3e09fec25f3a96e1272377b6450ef
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date:   Fri Sep 17 14:03:31 2021 +0200

    begin rewrite selector

3 files changed, 141 insertions, 14 deletions

diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp
index aa241c1e..16607cf5 100644
--- a/kvx/SelectOp.vp
+++ b/kvx/SelectOp.vp
@@ -64,29 +64,49 @@ Section SELECT.
 
 Context {hf: helper_functions}.
 
+Inductive to_cond0 :=
+| Cond0_some : condition0 -> expr -> to_cond0
+| Cond0_none : to_cond0
+| Cond0_true : to_cond0
+| Cond0_false : to_cond0.
+
+Definition compu0 c e1 :=
+  match c with
+  | Clt => Cond0_false
+  | Cge => Cond0_true
+  | _ => Cond0_some (Ccompu0 c) e1
+  end.
+
+Definition complu0 c e1 :=
+  match c with
+  | Clt => Cond0_false
+  | Cge => Cond0_true
+  | _ => Cond0_some (Ccomplu0 c) e1
+  end.
+
 Nondetfunction cond_to_condition0 (cond : condition) (args : exprlist) :=
   match cond, args with
   | (Ccompimm c x), (e1 ::: Enil) =>
     if Int.eq_dec x Int.zero
-    then Some ((Ccomp0 c), e1)
-    else None
+    then Cond0_some (Ccomp0 c) e1
+    else Cond0_none
            
   | (Ccompuimm c x), (e1 ::: Enil) =>
     if Int.eq_dec x Int.zero
-    then Some ((Ccompu0 c), e1)
-    else None
+    then compu0 c e1
+    else Cond0_none
 
   | (Ccomplimm c x), (e1 ::: Enil) =>
     if Int64.eq_dec x Int64.zero
-    then Some ((Ccompl0 c), e1)
-    else None
+    then Cond0_some (Ccompl0 c) e1
+    else Cond0_none
            
   | (Ccompluimm c x), (e1 ::: Enil) =>
     if Int64.eq_dec x Int64.zero
-    then Some ((Ccomplu0 c), e1)
-    else None
+    then complu0 c e1
+    else Cond0_none
            
-  | _, _ => None
+  | _, _ => Cond0_none
   end.
   
 (** Ternary operator *)
@@ -112,8 +132,10 @@ Definition same_expr_pure (e1 e2: expr) :=
 Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr)  : option expr :=
   Some (if same_expr_pure e1 e2 then e1 else
   match cond_to_condition0 cond args with
-  | None => select0 ty (Ccomp0 Cne) e1 e2 (Eop (Ocmp cond) args)
-  | Some(cond0, ec) => select0 ty cond0 e1 e2 ec
+  | Cond0_none => select0 ty (Ccomp0 Cne) e1 e2 (Eop (Ocmp cond) args)
+  | Cond0_some cond0 ec => select0 ty cond0 e1 e2 ec
+  | Cond0_true => e1
+  | Cond0_false => e2
   end).
 
 				      
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
index a7169881..45aa3343 100644
--- a/kvx/SelectOpproof.v
+++ b/kvx/SelectOpproof.v
@@ -1533,6 +1533,70 @@ Proof.
   apply Val.swap_cmplu_bool.
 Qed.
 
+Lemma int_ltu_zero : forall i, Int.ltu i Int.zero = false.
+Proof.
+  intro.
+  unfold Int.ltu.
+  apply zlt_false.
+  rewrite Int.unsigned_zero.
+  pose proof (Int.unsigned_range i).
+  lia.
+Qed.
+
+Lemma cmpu_bool_Clt : forall pred v0 b,
+    Val.cmpu_bool pred Clt v0 (Vint Int.zero) = Some b -> b = false.
+Proof.
+  intros until b. intro CMP.
+  destruct v0; cbn in CMP; try discriminate.
+  inv CMP.
+  apply int_ltu_zero.
+Qed.
+
+Lemma cmpu_bool_Cge : forall pred v0 b,
+    Val.cmpu_bool pred Cge v0 (Vint Int.zero) = Some b -> b = true.
+Proof.
+  intros until b. intro CMP.
+  destruct v0; cbn in CMP; try discriminate.
+  inv CMP.
+  rewrite int_ltu_zero.
+  reflexivity.
+Qed.
+  
+Lemma int64_ltu_zero : forall i, Int64.ltu i Int64.zero = false.
+Proof.
+  intro.
+  unfold Int64.ltu.
+  apply zlt_false.
+  rewrite Int64.unsigned_zero.
+  pose proof (Int64.unsigned_range i).
+  lia.
+Qed.
+
+Lemma cmplu_bool_Clt : forall pred v0 b,
+    Val.cmplu_bool pred Clt v0 (Vlong Int64.zero) = Some b -> b = false.
+Proof.
+  intros until b. intro CMP.
+  destruct v0; cbn in CMP; try discriminate.
+  { inv CMP.
+    apply int64_ltu_zero.
+  }
+  repeat rewrite if_same in CMP.
+  discriminate.
+Qed.
+
+Lemma cmplu_bool_Cge : forall pred v0 b,
+    Val.cmplu_bool pred Cge v0 (Vlong Int64.zero) = Some b -> b = true.
+Proof.
+  intros until b. intro CMP.
+  destruct v0; cbn in CMP; try discriminate.
+  { inv CMP.
+    rewrite int64_ltu_zero.
+    reflexivity.
+  }
+  repeat rewrite if_same in CMP.
+  discriminate.
+Qed.
+
 Theorem eval_select: 
   forall le ty cond al vl a1 v1 a2 v2 a b,
   select ty cond al a1 a2 = Some a ->
@@ -1581,8 +1645,27 @@ Proof.
       simpl.
       change (Val.cmpu_bool (Mem.valid_pointer m) c v0 (Vint Int.zero))
         with (eval_condition0 (Ccompu0 c) v0 m).
-      eapply eval_select0; eassumption.
-    }
+      destruct c.
+      all: try (eapply eval_select0; eassumption).
+      all: cbn.
+      all: cbn in HeC.
+      {
+      destruct (Val.cmpu_bool (Mem.valid_pointer m) Clt v0 (Vint Int.zero)) eqn:CMP; try discriminate.
+      inv HeC.
+      rewrite (cmpu_bool_Clt (Mem.valid_pointer m) v0 b CMP).
+      cbn.
+      exists v2.
+      split; auto using Val.lessdef_normalize.
+      }
+      {
+      destruct (Val.cmpu_bool (Mem.valid_pointer m) Cge v0 (Vint Int.zero)) eqn:CMP; try discriminate.
+      inv HeC.
+      rewrite (cmpu_bool_Cge (Mem.valid_pointer m) v0 b CMP).
+      cbn.
+      exists v1.
+      split; auto using Val.lessdef_normalize.
+      }
+     }
     simpl.
     erewrite <- (bool_cond0_ne (Val.cmpu_bool (Mem.valid_pointer m) c v0 (Vint x))).
     eapply eval_select0; repeat (try econstructor; try eassumption).
@@ -1609,7 +1692,26 @@ Proof.
       simpl.
       change (Val.cmplu_bool  (Mem.valid_pointer m) c v0 (Vlong Int64.zero))
       with (eval_condition0 (Ccomplu0 c) v0 m).
-      eapply eval_select0; eassumption.
+      destruct c.
+      all: try (eapply eval_select0; eassumption).
+      all: cbn.
+      all: cbn in HeC.
+      {
+      destruct (Val.cmplu_bool (Mem.valid_pointer m) Clt v0 (Vlong Int64.zero)) eqn:CMP; try discriminate.
+      inv HeC.
+      rewrite (cmplu_bool_Clt (Mem.valid_pointer m) v0 b CMP).
+      cbn.
+      exists v2.
+      split; auto using Val.lessdef_normalize.
+      }
+      {
+      destruct (Val.cmplu_bool (Mem.valid_pointer m) Cge v0 (Vlong Int64.zero)) eqn:CMP; try discriminate.
+      inv HeC.
+      rewrite (cmplu_bool_Cge (Mem.valid_pointer m) v0 b CMP).
+      cbn.
+      exists v1.
+      split; auto using Val.lessdef_normalize.
+      }
     }
     simpl.
     erewrite <- (bool_cond0_ne (Val.cmplu_bool (Mem.valid_pointer m) c v0 (Vlong x))).
diff --git a/test/monniaux/codegen/comp0.c b/test/monniaux/codegen/comp0.c
new file mode 100644
index 00000000..60f8ba77
--- /dev/null
+++ b/test/monniaux/codegen/comp0.c
@@ -0,0 +1,3 @@
+int toto(unsigned x) {
+  return (x < 0) ? 1 : 2;
+}