From 57a630cad254cb8a33663c0d0f64a8cf79e533ea Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Wed, 14 Aug 2024 09:55:47 +0200
Subject: [PATCH 1/2] Value analysis: add IU ("known integer or Vundef") static
 value

This improves analysis precision for comparisons and selections.
---
 backend/ValueDomain.v | 224 ++++++++++++++++++++++++++++++------------
 1 file changed, 160 insertions(+), 64 deletions(-)

diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 764fa2b12..ed7accf1c 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -481,6 +481,7 @@ Qed.
 Inductive aval : Type :=
   | Vbot                     (**r bottom (empty set of values) *)
   | I (n: int)               (**r exactly [Vint n] *)
+  | IU (n: int)              (**r [Vint n] or [Vundef] *)
   | Uns (p: aptr) (n: Z)     (**r a [n]-bit unsigned integer, or [Vundef] *)
   | Sgn (p: aptr) (n: Z)     (**r a [n]-bit signed integer, or [Vundef] *)
   | L (n: int64)             (**r exactly [Vlong n] *)
@@ -512,6 +513,8 @@ Definition is_sgn (n: Z) (i: int) : Prop :=
 
 Inductive vmatch : val -> aval -> Prop :=
   | vmatch_i: forall i, vmatch (Vint i) (I i)
+  | vmatch_iu: forall i, vmatch (Vint i) (IU i)
+  | vmatch_iu_undef: forall i, vmatch Vundef (IU i)
   | vmatch_Uns: forall p i n, 0 <= n -> is_uns n i -> vmatch (Vint i) (Uns p n)
   | vmatch_Uns_undef: forall p n, vmatch Vundef (Uns p n)
   | vmatch_Sgn: forall p i n, 0 < n -> is_sgn n i -> vmatch (Vint i) (Sgn p n)
@@ -882,15 +885,20 @@ Inductive vge: aval -> aval -> Prop :=
   | vge_l: forall i, vge (L i) (L i)
   | vge_f: forall f, vge (F f) (F f)
   | vge_s: forall f, vge (FS f) (FS f)
+  | vge_iu: forall i, vge (IU i) (IU i)
+  | vge_iu_i: forall i, vge (IU i) (I i)
   | vge_uns_i: forall p n i, 0 <= n -> is_uns n i -> vge (Uns p n) (I i)
+  | vge_uns_iu: forall p n i, 0 <= n -> is_uns n i -> vge (Uns p n) (IU i)
   | vge_uns_uns: forall p1 n1 p2 n2, n1 >= n2 -> pge p1 p2 -> vge (Uns p1 n1) (Uns p2 n2)
   | vge_sgn_i: forall p n i, 0 < n -> is_sgn n i -> vge (Sgn p n) (I i)
+  | vge_sgn_iu: forall p n i, 0 < n -> is_sgn n i -> vge (Sgn p n) (IU i)
   | vge_sgn_sgn: forall p1 n1 p2 n2, n1 >= n2 -> pge p1 p2 -> vge (Sgn p1 n1) (Sgn p2 n2)
   | vge_sgn_uns: forall p1 n1 p2 n2, n1 > n2 -> pge p1 p2 -> vge (Sgn p1 n1) (Uns p2 n2)
   | vge_num_i: forall p i, vge (Num p) (I i)
   | vge_num_l: forall p i, vge (Num p) (L i)
   | vge_num_f: forall p f, vge (Num p) (F f)
   | vge_num_s: forall p f, vge (Num p) (FS f)
+  | vge_num_iu: forall p i, vge (Num p) (IU i)
   | vge_num_uns: forall p q n, pge p q -> vge (Num p) (Uns q n)
   | vge_num_sgn: forall p q n, pge p q -> vge (Num p) (Sgn q n)
   | vge_num_num: forall p q, pge p q -> vge (Num p) (Num q)
@@ -901,6 +909,7 @@ Inductive vge: aval -> aval -> Prop :=
   | vge_ip_l: forall p i, vge (Ifptr p) (L i)
   | vge_ip_f: forall p f, vge (Ifptr p) (F f)
   | vge_ip_s: forall p f, vge (Ifptr p) (FS f)
+  | vge_ip_iu: forall  p i, vge (Ifptr p) (IU i)
   | vge_ip_uns: forall p q n, pge p q -> vge (Ifptr p) (Uns q n)
   | vge_ip_sgn: forall p q n, pge p q -> vge (Ifptr p) (Sgn q n)
   | vge_ip_num: forall p q, pge p q -> vge (Ifptr p) (Num q).
@@ -933,24 +942,27 @@ Qed.
 
 (** Least upper bound *)
 
+Definition vlub_int (cstr: int -> aval) (i1 i2: int) : aval :=
+  if Int.eq i1 i2 then cstr i1 else
+  if Int.lt i1 Int.zero || Int.lt i2 Int.zero
+  then sgn Pbot (Z.max (ssize i1) (ssize i2))
+  else uns Pbot (Z.max (usize i1) (usize i2)).
+
 Definition vlub (v w: aval) : aval :=
   match v, w with
   | Vbot, _ => w
   | _, Vbot => v
-  | I i1, I i2 =>
-      if Int.eq i1 i2 then v else
-      if Int.lt i1 Int.zero || Int.lt i2 Int.zero
-      then sgn Pbot (Z.max (ssize i1) (ssize i2))
-      else uns Pbot (Z.max (usize i1) (usize i2))
-  | I i, Uns p n | Uns p n, I i =>
+  | I i1, I i2 => vlub_int I i1 i2
+  | I i1, IU i2 | IU i1, I i2 | IU i1, IU i2 => vlub_int IU i1 i2
+  | (I i | IU i), Uns p n | Uns p n, (I i | IU i) =>
       if Int.lt i Int.zero
       then sgn p (Z.max (ssize i) (n + 1))
       else uns p (Z.max (usize i) n)
-  | I i, Sgn p n | Sgn p n, I i =>
+  | (I i | IU i), Sgn p n | Sgn p n, (I i | IU i) =>
       sgn p (Z.max (ssize i) n)
-  | I i, Num p | Num p, I i => Num p
-  | I i, (Ptr p | Ifptr p) | (Ptr p | Ifptr p), I i => Ifptr (plub p (int_provenance i))
-  | I _, (L _ | F _ | FS _) | (L _ | F _ | FS _), I _ => ntop
+  | (I i | IU i), Num p | Num p, (I i | IU i) => Num p
+  | (I i | IU i), (Ptr p | Ifptr p) | (Ptr p | Ifptr p), (I i | IU i) => Ifptr (plub p (int_provenance i))
+  | (I _ | IU _), (L _ | F _ | FS _) | (L _ | F _ | FS _), (I _ | IU _) => ntop
   | Uns p1 n1, Uns p2 n2 => Uns (plub p1 p2) (Z.max n1 n2)
   | Uns p1 n1, Sgn p2 n2 => sgn (plub p1 p2) (Z.max (n1 + 1) n2)
   | Sgn p1 n1, Uns p2 n2 => sgn (plub p1 p2) (Z.max n1 (n2 + 1))
@@ -978,9 +990,11 @@ Definition vlub (v w: aval) : aval :=
 Lemma vlub_comm:
   forall v w, vlub v w = vlub w v.
 Proof.
+  assert (INT: forall cstr i j, vlub_int cstr i j = vlub_int cstr j i).
+  { intros. unfold vlub_int. rewrite Int.eq_sym, orb_comm.
+    predSpec Int.eq Int.eq_spec j i. congruence.
+    destruct orb; f_equal; apply Z.max_comm. }
   intros. unfold vlub; destruct v; destruct w; auto; f_equal; auto using Z.max_comm, plub_comm.
-- rewrite Int.eq_sym. predSpec Int.eq Int.eq_spec n0 n. congruence.
-  rewrite orb_comm. destruct orb; f_equal; apply Z.max_comm.
 - rewrite Int64.eq_sym. predSpec Int64.eq Int64.eq_spec n0 n; congruence.
 - rewrite dec_eq_sym. destruct (Float.eq_dec f0 f); congruence.
 - rewrite dec_eq_sym. destruct (Float32.eq_dec f0 f); congruence.
@@ -996,6 +1010,11 @@ Proof.
   intros. apply vge_trans with (Uns p n). apply vge_uns_uns'. auto with va.
 Qed.
 
+Lemma vge_uns_iu': forall p n i, 0 <= n -> is_uns n i -> vge (uns p n) (IU i).
+Proof.
+  intros. apply vge_trans with (Uns p n). apply vge_uns_uns'. auto with va.
+Qed.
+
 Lemma vge_sgn_sgn': forall p n, vge (sgn p n) (Sgn p n).
 Proof.
   unfold sgn; intros. repeat (destruct zle); eauto with va.
@@ -1006,19 +1025,39 @@ Proof.
   intros. apply vge_trans with (Sgn p n). apply vge_sgn_sgn'. auto with va.
 Qed.
 
-Hint Resolve vge_uns_uns' vge_uns_i' vge_sgn_sgn' vge_sgn_i' : va.
+Lemma vge_sgn_iu': forall p n i, 0 < n -> is_sgn n i -> vge (sgn p n) (IU i).
+Proof.
+  intros. apply vge_trans with (Sgn p n). apply vge_sgn_sgn'. auto with va.
+Qed.
+
+Hint Resolve vge_uns_uns' vge_uns_i' vge_uns_iu' vge_sgn_sgn' vge_sgn_i' vge_sgn_iu': va.
 
 Lemma vge_lub_l:
   forall x y, vge (vlub x y) x.
 Proof.
+  assert (INT: forall i j, vge (vlub_int I i j) (I i)).
+  { unfold vlub_int; intros. predSpec Int.eq Int.eq_spec i j. auto with va.
+    destruct orb. eauto with va.
+    apply vge_sgn_i'. generalize (ssize_pos i); lia. eauto with va.
+    apply vge_uns_i'. generalize (usize_pos i); lia. eauto with va. }
+  assert (INTU: forall i j, vge (vlub_int IU i j) (IU i)).
+  { unfold vlub_int; intros. predSpec Int.eq Int.eq_spec i j. auto with va.
+    destruct orb.
+    apply vge_sgn_iu'. generalize (ssize_pos i); lia. eauto with va.
+    apply vge_uns_iu'. generalize (usize_pos i); lia. eauto with va. }
   unfold vlub, ntop; destruct x, y; eauto using vge_trans, pge_lub_l with va.
-- predSpec Int.eq Int.eq_spec n n0. auto with va. destruct orb.
-  apply vge_sgn_i'. generalize (ssize_pos n); lia. eauto with va.
-  apply vge_uns_i'. generalize (usize_pos n); lia. eauto with va.
 - destruct (Int.lt n Int.zero).
   apply vge_sgn_i'. generalize (ssize_pos n); lia. eauto with va.
   apply vge_uns_i'. generalize (usize_pos n); lia. eauto with va.
 - apply vge_sgn_i'. generalize (ssize_pos n); lia. eauto with va.
+- destruct (Int.lt n Int.zero).
+  apply vge_sgn_iu'. generalize (ssize_pos n); lia. eauto with va.
+  apply vge_uns_iu'. generalize (usize_pos n); lia. eauto with va.
+- apply vge_sgn_iu'. generalize (ssize_pos n); lia. eauto with va.
+- destruct (Int.lt n0 Int.zero).
+  eapply vge_trans. apply vge_sgn_sgn'.
+  apply vge_trans with (Sgn p (n + 1)); eauto with va.
+  eapply vge_trans. apply vge_uns_uns'. eauto with va.
 - destruct (Int.lt n0 Int.zero).
   eapply vge_trans. apply vge_sgn_sgn'.
   apply vge_trans with (Sgn p (n + 1)); eauto with va.
@@ -1124,15 +1163,17 @@ Definition vincl (v w: aval) : bool :=
   match v, w with
   | Vbot, _ => true
   | I i, I j => Int.eq_dec i j
-  | I i, Uns p n => Int.eq_dec (Int.zero_ext n i) i && zle 0 n
-  | I i, Sgn p n => Int.eq_dec (Int.sign_ext n i) i && zlt 0 n
+  | I i, IU j => Int.eq_dec i j
+  | IU i, IU j => Int.eq_dec i j
+  | (I i | IU i), Uns p n => Int.eq_dec (Int.zero_ext n i) i && zle 0 n
+  | (I i | IU i), Sgn p n => Int.eq_dec (Int.sign_ext n i) i && zlt 0 n
   | Uns p n, Uns q m => zle n m && pincl p q
   | Uns p n, Sgn q m => zlt n m && pincl p q
   | Sgn p n, Sgn q m => zle n m && pincl p q
   | L i, L j => Int64.eq_dec i j
   | F i, F j => Float.eq_dec i j
   | FS i, FS j => Float32.eq_dec i j
-  | (I _ | L _ | F _ | FS _), (Num _ | Ifptr _) => true
+  | (I _ | IU _ | L _ | F _ | FS _), (Num _ | Ifptr _) => true
   | (Uns p _ | Sgn p _ | Num p), Num q => pincl p q
   | Ptr p, Ptr q => pincl p q
   | (Ptr p | Ifptr p | Num p | Uns p _ | Sgn p _), Ifptr q => pincl p q
@@ -1145,6 +1186,8 @@ Proof.
   intros; try discriminate; try InvBooleans; try subst; eauto using pincl_ge with va.
 - constructor; auto. rewrite is_uns_zero_ext; auto.
 - constructor; auto. rewrite is_sgn_sign_ext; auto.
+- constructor; auto. rewrite is_uns_zero_ext; auto.
+- constructor; auto. rewrite is_sgn_sign_ext; auto.
 Qed.
 
 Lemma ge_vincl: forall v w, vge v w -> vincl w v = true.
@@ -1152,8 +1195,8 @@ Proof.
   induction 1; simpl; try (apply andb_true_intro; split); auto using ge_pincl, proj_sumbool_is_true.
   all: try (unfold proj_sumbool; rewrite zle_true by lia; auto).
   all: try (unfold proj_sumbool; rewrite zlt_true by lia; auto).
-- apply is_uns_zero_ext in H0; rewrite H0. auto using proj_sumbool_is_true.
-- apply is_sgn_sign_ext in H0; auto. rewrite H0. auto using proj_sumbool_is_true.
+  1,2: apply is_uns_zero_ext in H0; rewrite H0; auto using proj_sumbool_is_true.
+  1,2: apply is_sgn_sign_ext in H0; auto; rewrite H0; auto using proj_sumbool_is_true.
 Qed.
 
 (** Loading constants *)
@@ -1198,7 +1241,7 @@ Qed.
 (** Generic operations that just do constant propagation. *)
 
 Definition unop_int (sem: int -> int) (x: aval) :=
-  match x with I n => I (sem n) | _ => ntop1 x end.
+  match x with I n => I (sem n) | IU n => IU (sem n) | _ => ntop1 x end.
 
 Lemma unop_int_sound:
   forall sem v x,
@@ -1209,7 +1252,10 @@ Proof.
 Qed.
 
 Definition binop_int (sem: int -> int -> int) (x y: aval) :=
-  match x, y with I n, I m => I (sem n m) | _, _ => ntop2 x y end.
+  match x, y with
+  | I n, I m => I (sem n m)
+  | I n, IU m | IU n, I m | IU n, IU m => IU (sem n m)
+  | _, _ => ntop2 x y end.
 
 Lemma binop_int_sound:
   forall sem v x w y,
@@ -1293,6 +1339,7 @@ Definition shl (v w: aval) :=
       if Int.ltu amount Int.iwordsize then
         match v with
         | I i => I (Int.shl i amount)
+        | IU i => IU (Int.shl i amount)
         | Uns p n => uns p (n + Int.unsigned amount)
         | Sgn p n => sgn p (n + Int.unsigned amount)
         | _ => ntop1 v
@@ -1329,6 +1376,7 @@ Definition shru (v w: aval) :=
       if Int.ltu amount Int.iwordsize then
         match v with
         | I i => I (Int.shru i amount)
+        | IU i => IU (Int.shru i amount)
         | Uns p n => uns p (n - Int.unsigned amount)
         | _ => uns (provenance v) (Int.zwordsize - Int.unsigned amount)
         end
@@ -1367,6 +1415,7 @@ Definition shr (v w: aval) :=
       if Int.ltu amount Int.iwordsize then
         match v with
         | I i => I (Int.shr i amount)
+        | IU i => IU (Int.shr i amount)
         | Uns p n => sgn p (n + 1 - Int.unsigned amount)
         | Sgn p n => sgn p (n - Int.unsigned amount)
         | _ => sgn (provenance v) (Int.zwordsize - Int.unsigned amount)
@@ -1415,8 +1464,9 @@ Qed.
 Definition and (v w: aval) :=
   match v, w with
   | I i1, I i2 => I (Int.and i1 i2)
-  | I i, Uns p n | Uns p n, I i => uns p (Z.min n (usize i))
-  | I i, x | x, I i => uns (provenance x) (usize i)
+  | I i1, IU i2 | IU i1, I i2 | IU i1, IU i2 => IU (Int.and i1 i2)
+  | (I i | IU i), Uns p n | Uns p n, (I i | IU i) => uns p (Z.min n (usize i))
+  | (I i | IU i), x | x, (I i | IU i) => uns (provenance x) (usize i)
   | Uns p1 n1, Uns p2 n2 => uns (plub p1 p2) (Z.min n1 n2)
   | Uns p n, _ => uns (plub p (provenance w)) n
   | _, Uns p n => uns (plub (provenance v) p) n
@@ -1451,7 +1501,8 @@ Qed.
 Definition or (v w: aval) :=
   match v, w with
   | I i1, I i2 => I (Int.or i1 i2)
-  | I i, Uns p n | Uns p n, I i => uns p (Z.max n (usize i))
+  | I i1, IU i2 | IU i1, I i2 | IU i1, IU i2 => IU (Int.or i1 i2)
+  | (I i | IU i), Uns p n | Uns p n, (I i | IU i) => uns p (Z.max n (usize i))
   | Uns p1 n1, Uns p2 n2 => uns (plub p1 p2) (Z.max n1 n2)
   | Sgn p1 n1, Sgn p2 n2 => sgn (plub p1 p2) (Z.max n1 n2)
   | _, _ => ntop2 v w
@@ -1476,7 +1527,8 @@ Qed.
 Definition xor (v w: aval) :=
   match v, w with
   | I i1, I i2 => I (Int.xor i1 i2)
-  | I i, Uns p n | Uns p n, I i => uns p (Z.max n (usize i))
+  | I i1, IU i2 | IU i1, I i2 | IU i1, IU i2 => IU (Int.xor i1 i2)
+  | (I i | IU i), Uns p n | Uns p n, (I i | IU i) => uns p (Z.max n (usize i))
   | Uns p1 n1, Uns p2 n2 => uns (plub p1 p2) (Z.max n1 n2)
   | Sgn p1 n1, Sgn p2 n2 => sgn (plub p1 p2) (Z.max n1 n2)
   | _, _ => ntop2 v w
@@ -1501,6 +1553,7 @@ Qed.
 Definition notint (v: aval) :=
   match v with
   | I i => I (Int.not i)
+  | IU i => IU (Int.not i)
   | Uns p n => sgn p (n + 1)
   | Sgn p n => Sgn p n
   | _ => ntop1 v
@@ -1520,6 +1573,7 @@ Qed.
 Definition rol (x y: aval) :=
   match y, x with
   | I j, I i => I(Int.rol i j)
+  | I j, IU i => IU(Int.rol i j)
   | I j, Uns p n => uns p (n + Int.unsigned j)
   | I j, Sgn p n => if zlt n Int.zwordsize then sgn p (n + Int.unsigned j) else ntop1 x
   | _, _ => ntop1 x
@@ -1550,6 +1604,7 @@ Qed.
 Definition ror (x y: aval) :=
   match y, x with
   | I j, I i => I(Int.ror i j)
+  | I j, IU i => IU(Int.ror i j)
   | _, _ => ntop1 x
   end.
 
@@ -1583,6 +1638,7 @@ Qed.
 Definition neg (x: aval) :=
   match x with
   | I i => I (Int.neg i)
+  | IU i => IU (Int.neg i)
   | Sgn p n => sgn p (n + 1)
   | _ => ntop1 x
   end.
@@ -1604,14 +1660,15 @@ Qed.
 Definition add (x y: aval) :=
   match x, y with
   | I i, I j => I (Int.add i j)
-  | I i, Uns p n | Uns p n, I i => uns p (Z.max n (usize i) + 1)
-  | I i, Sgn p n | Sgn p n, I i => sgn p (Z.max n (ssize i) + 1)
+  | I i, IU j | IU i, I j | IU i, IU j => IU (Int.add i j)
+  | (I i | IU i), Uns p n | Uns p n, (I i | IU i) => uns p (Z.max n (usize i) + 1)
+  | (I i | IU i), Sgn p n | Sgn p n, (I i | IU i) => sgn p (Z.max n (ssize i) + 1)
   | Uns p1 n1, Uns p2 n2 => uns (plub p1 p2) (Z.max n1 n2 + 1)
   | Sgn p1 n1, Sgn p2 n2 => sgn (plub p1 p2) (Z.max n1 n2 + 1)
   | Uns p1 n1, Sgn p2 n2 | Sgn p2 n2, Uns p1 n1 => sgn (plub p1 p2) (Z.max (n1 + 1) n2 + 1)
-  | Ptr p, I i | I i, Ptr p => Ptr (if Archi.ptr64 then poffset p else padd p (Ptrofs.of_int i))
+  | Ptr p, (I i | IU i) | (I i | IU i), Ptr p => Ptr (if Archi.ptr64 then poffset p else padd p (Ptrofs.of_int i))
   | Ptr p, _   | _, Ptr p   => Ptr (poffset p)
-  | Ifptr p, I i | I i, Ifptr p => Ifptr (if Archi.ptr64 then poffset p else padd p (Ptrofs.of_int i))
+  | Ifptr p, (I i | IU i) | (I i | IU i), Ifptr p => Ifptr (if Archi.ptr64 then poffset p else padd p (Ptrofs.of_int i))
   | Ifptr p, Ifptr q => Ifptr (plub (poffset p) (poffset q))
   | Ifptr p, _ | _, Ifptr p => Ifptr (poffset p)
   | _, _ => ntop2 x y
@@ -1655,14 +1712,15 @@ Qed.
 Definition sub (v w: aval) :=
   match v, w with
   | I i1, I i2 => I (Int.sub i1 i2)
-  | I i, Uns p n | Uns p n, I i => sgn p (Z.max (n + 1) (ssize i) + 1)
-  | I i, Sgn p n | Sgn p n, I i => sgn p (Z.max n (ssize i) + 1)
+  | I i1, IU i2 | IU i1, I i2 | IU i1, IU i2 => IU (Int.sub i1 i2)
+  | (I i | IU i), Uns p n | Uns p n, (I i | IU i) => sgn p (Z.max (n + 1) (ssize i) + 1)
+  | (I i | IU i), Sgn p n | Sgn p n, (I i | IU i) => sgn p (Z.max n (ssize i) + 1)
   | Uns p1 n1, Uns p2 n2 => sgn (plub p1 p2) (Z.max n1 n2 + 1)
   | Sgn p1 n1, Sgn p2 n2 => sgn (plub p1 p2) (Z.max n1 n2 + 1)
   | Uns p1 n1, Sgn p2 n2 | Sgn p2 n2, Uns p1 n1 => sgn (plub p1 p2) (Z.max (n1 + 1) n2 + 1)
-  | Ptr p, I i => if Archi.ptr64 then Ifptr (poffset p) else Ptr (psub p (Ptrofs.of_int i))
+  | Ptr p, (I i | IU i) => if Archi.ptr64 then Ifptr (poffset p) else Ptr (psub p (Ptrofs.of_int i))
   | Ptr p, _   => Ifptr (poffset p)
-  | Ifptr p, I i => if Archi.ptr64 then Ifptr (plub (poffset p) (provenance w)) else Ifptr (psub p (Ptrofs.of_int i))
+  | Ifptr p, (I i | IU i) => if Archi.ptr64 then Ifptr (plub (poffset p) (provenance w)) else Ifptr (psub p (Ptrofs.of_int i))
   | Ifptr p, _ => Ifptr (plub (poffset p) (provenance w))
   | _, _ => ntop2 v w
   end.
@@ -2193,6 +2251,7 @@ Proof (binop_single_sound Float32.div).
 Definition zero_ext (nbits: Z) (v: aval) :=
   match v with
   | I i => I (Int.zero_ext nbits i)
+  | IU i => IU (Int.zero_ext nbits i)
   | Uns p n => uns p (Z.min n nbits)
   | _ => uns (provenance v) nbits
   end.
@@ -2214,6 +2273,7 @@ Definition sign_ext (nbits: Z) (v: aval) :=
   if zle nbits 0 then Uns (provenance v) 0 else
   match v with
   | I i => I (Int.sign_ext nbits i)
+  | IU i => IU (Int.sign_ext nbits i)
   | Uns p n => if zlt n nbits then Uns p n else sgn p nbits
   | Sgn p n => sgn p (Z.min n nbits)
   | _ => sgn (provenance v) nbits
@@ -2772,11 +2832,12 @@ Qed.
 Definition cmpu_bool (c: comparison) (v w: aval) : abool :=
   match v, w with
   | I i1, I i2 => Just (Int.cmpu c i1 i2)
+  | I i1, IU i2 | IU i1, I i2 | IU i1, IU i2 => Maybe (Int.cmpu c i1 i2)
   | Ptr _, I i => if Int.eq i Int.zero then cmp_different_blocks c else Btop
   | I i, Ptr _ => if Int.eq i Int.zero then cmp_different_blocks c else Btop
   | Ptr p1, Ptr p2 => pcmp c p1 p2
-  | _, I i => club (cmp_intv c (uintv v) (Int.unsigned i)) (cmp_different_blocks c)
-  | I i, _ => club (cmp_intv (swap_comparison c) (uintv w) (Int.unsigned i)) (cmp_different_blocks c)
+  | _, (I i | IU i) => club (cmp_intv c (uintv v) (Int.unsigned i)) (cmp_different_blocks c)
+  | (I i | IU i), _ => club (cmp_intv (swap_comparison c) (uintv w) (Int.unsigned i)) (cmp_different_blocks c)
   | _, _ => Btop
   end.
 
@@ -2805,8 +2866,16 @@ Proof.
              cmatch_lub_l, cmatch_lub_r, pcmp_sound,
              cmpu_intv_sound, cmpu_intv_sound_2, cmp_intv_None.
 - constructor.
+- constructor.
+- constructor.
 - destruct (Int.eq i Int.zero); auto using cmatch_top.
 - simpl; destruct (Int.eq i Int.zero); auto using cmatch_top, cmp_different_blocks_none.
+- constructor.
+- constructor.
+- constructor.
+- constructor.
+- constructor.
+- constructor.
 - destruct (Int.eq i Int.zero); auto using cmatch_top.
 - simpl; destruct (Int.eq i Int.zero); auto using cmatch_top, cmp_different_blocks_none.
 Qed.
@@ -2814,8 +2883,9 @@ Qed.
 Definition cmp_bool (c: comparison) (v w: aval) : abool :=
   match v, w with
   | I i1, I i2 => Just (Int.cmp c i1 i2)
-  | _, I i => cmp_intv c (sintv v) (Int.signed i)
-  | I i, _ => cmp_intv (swap_comparison c) (sintv w) (Int.signed i)
+  | I i1, IU i2 | IU i1, I i2 | IU i1, IU i2 => Maybe (Int.cmp c i1 i2)
+  | _, (I i | IU i) => cmp_intv c (sintv v) (Int.signed i)
+  | (I i | IU i), _ => cmp_intv (swap_comparison c) (sintv w) (Int.signed i)
   | _, _ => Btop
   end.
 
@@ -2824,8 +2894,8 @@ Lemma cmp_bool_sound:
 Proof.
   intros.
   unfold cmp_bool; inversion H; subst; inversion H0; subst;
-  auto using cmatch_top, cmp_intv_sound, cmp_intv_sound_2, cmp_intv_None.
-- constructor.
+  auto using cmatch_top, cmp_intv_sound, cmp_intv_sound_2, cmp_intv_None;
+  constructor.
 Qed.
 
 Definition cmplu_bool (c: comparison) (v w: aval) : abool :=
@@ -2909,6 +2979,7 @@ Qed.
 Definition maskzero (x: aval) (mask: int) : abool :=
   match x with
   | I i => Just (Int.eq (Int.and i mask) Int.zero)
+  | IU i => Maybe (Int.eq (Int.and i mask) Int.zero)
   | Uns p n => if Int.eq (Int.zero_ext n mask) Int.zero then Maybe true else Btop
   | _ => Btop
   end.
@@ -2931,21 +3002,20 @@ Qed.
 Definition of_optbool (ab: abool) : aval :=
   match ab with
   | Just b => I (if b then Int.one else Int.zero)
+  | Maybe b => IU (if b then Int.one else Int.zero)
   | _ => Uns Pbot 1
   end.
 
 Lemma of_optbool_sound:
   forall ob ab, cmatch ob ab -> vmatch (Val.of_optbool ob) (of_optbool ab).
 Proof.
-  intros.
-  assert (DEFAULT: vmatch (Val.of_optbool ob) (Uns Pbot 1)).
-  {
-    destruct ob; simpl; auto with va.
-    destruct b; constructor; try lia.
-    change 1 with (usize Int.one). apply is_uns_usize.
-    red; intros. apply Int.bits_zero.
-  }
-  inv H; auto. simpl. destruct b; constructor.
+  intros. inv H; simpl; auto with va.
+- destruct b; constructor.
+- destruct b; constructor.
+- destruct ob; simpl; auto with va.
+  destruct b; constructor; try lia.
+  change 1 with (usize Int.one). apply is_uns_usize.
+  red; intros. apply Int.bits_zero.
 Qed.
 
 Definition resolve_branch (ab: abool) : option bool :=
@@ -2968,10 +3038,7 @@ Qed.
 Definition add_undef (x: aval) :=
   match x with
   | Vbot => ntop
-  | I i =>
-      if Int.lt i Int.zero
-      then sgn Pbot (ssize i)
-      else uns Pbot (usize i)
+  | I i => IU i
   | L _ | F _ | FS _ => ntop
   | _ => x
   end.
@@ -2980,16 +3047,12 @@ Lemma add_undef_sound:
   forall v x, vmatch v x -> vmatch v (add_undef x).
 Proof.
   destruct 1; simpl; auto with va.
-  destruct (Int.lt i Int.zero).
-  apply vmatch_sgn; apply is_sgn_ssize.
-  apply vmatch_uns; apply is_uns_usize.
 Qed.
 
 Lemma add_undef_undef:
   forall x, vmatch Vundef (add_undef x).
 Proof.
   destruct x; simpl; auto with va.
-  destruct (Int.lt n Int.zero); auto with va.
 Qed.
 
 (** Normalization by the select operation. *)
@@ -3053,22 +3116,29 @@ Definition vnormalize (chunk: memory_chunk) (v: aval) :=
   | Mbool, I i =>
       let j := Int.zero_ext 8 i in
       if Int.eq j Int.zero || Int.eq j Int.one then I j else Uns Pbot 1
+  | Mbool, IU i =>
+      let j := Int.zero_ext 8 i in
+      if Int.eq j Int.zero || Int.eq j Int.one then IU j else Uns Pbot 1
   | Mbool, _ => Uns (provenance v) 1
   | Mint8signed, I i => I (Int.sign_ext 8 i)
+  | Mint8signed, IU i => IU (Int.sign_ext 8 i)
   | Mint8signed, Uns p n => if zlt n 8 then Uns (provenance v) n else Sgn (provenance v) 8
   | Mint8signed, Sgn p n => Sgn (provenance v) (Z.min n 8)
   | Mint8signed, _ => Sgn (provenance v) 8
   | Mint8unsigned, I i => I (Int.zero_ext 8 i)
+  | Mint8unsigned, IU i => IU (Int.zero_ext 8 i)
   | Mint8unsigned, Uns p n => Uns (provenance v) (Z.min n 8)
   | Mint8unsigned, _ => Uns (provenance v) 8
   | Mint16signed, I i => I (Int.sign_ext 16 i)
+  | Mint16signed, IU i => IU (Int.sign_ext 16 i)
   | Mint16signed, Uns p n => if zlt n 16 then Uns (provenance v) n else Sgn (provenance v) 16
   | Mint16signed, Sgn p n => Sgn (provenance v) (Z.min n 16)
   | Mint16signed, _ => Sgn (provenance v) 16
   | Mint16unsigned, I i => I (Int.zero_ext 16 i)
+  | Mint16unsigned, IU i => IU (Int.zero_ext 16 i)
   | Mint16unsigned, Uns p n => Uns (provenance v) (Z.min n 16)
   | Mint16unsigned, _ => Uns (provenance v) 16
-  | Mint32, (I _ | Uns _ _ | Sgn _ _ | Num _) => v
+  | Mint32, (I _ | IU _ | Uns _ _ | Sgn _ _ | Num _) => v
   | Mint32, (Ptr p | Ifptr p) => if Archi.ptr64 then Num (provenance v) else v
   | Mint32, _ => Num (provenance v)
   | Mint64, L _ => v
@@ -3078,7 +3148,7 @@ Definition vnormalize (chunk: memory_chunk) (v: aval) :=
   | Mfloat32, _ => Num (provenance v)
   | Mfloat64, F f => v
   | Mfloat64, _ => Num (provenance v)
-  | Many32, (I _ | Uns _ _ | Sgn _ _ | FS _) => v
+  | Many32, (I _ | IU _ | Uns _ _ | Sgn _ _ | FS _) => v
   | Many32, (Ptr p | Ifptr p) => if Archi.ptr64 then Num (provenance v) else v
   | Many32, _ => Num (provenance v)
   | Many64, _ => v
@@ -3094,6 +3164,11 @@ Proof.
   predSpec Int.eq Int.eq_spec j Int.zero. rewrite H. apply vmatch_i.
   predSpec Int.eq Int.eq_spec j Int.one. rewrite H0. apply vmatch_i.
   simpl. unfold proj_sumbool, Vtrue, Vfalse. rewrite ! dec_eq_false by congruence. apply vmatch_Uns_undef.
+- set (j := Int.zero_ext 8 i). unfold Val.norm_bool, Val.is_bool.
+  predSpec Int.eq Int.eq_spec j Int.zero. rewrite H. apply vmatch_iu.
+  predSpec Int.eq Int.eq_spec j Int.one. rewrite H0. apply vmatch_iu.
+  simpl. unfold proj_sumbool, Vtrue, Vfalse. rewrite ! dec_eq_false by congruence. apply vmatch_Uns_undef.
+- destruct orb; auto with va.
 - destruct (zlt n 8); constructor; auto with va.
   apply is_sign_ext_uns; auto.
   apply is_sign_ext_sgn; auto with va.
@@ -3168,15 +3243,18 @@ Lemma vnormalize_monotone:
   vge x y -> vge (vnormalize chunk x) (vnormalize chunk y).
 Proof with (auto using provenance_monotone, provenance_ifptr_ge with va).
 Local Opaque provenance.
-  assert (BOOL: forall p i,
-          vge (Uns p 1) (if Int.eq i Int.zero || Int.eq i Int.one then I i else Uns Pbot 1)).
+  assert (BOOL1: forall p i,
+          vge (Uns p 1) (if Int.eq i Int.zero || Int.eq i Int.one then IU i else Uns Pbot 1)).
   {
     intros. predSpec Int.eq Int.eq_spec i Int.zero; subst.
-    apply vge_uns_i. lia. red; intros. apply Int.bits_zero.
+    apply vge_uns_iu. lia. red; intros. apply Int.bits_zero.
     predSpec Int.eq Int.eq_spec i Int.one; subst.
-    apply vge_uns_i. lia. apply (is_uns_usize Int.one).
+    apply vge_uns_iu. lia. apply (is_uns_usize Int.one).
     apply vge_uns_uns. lia. auto with va.
   }
+  assert (BOOL2: forall p i,
+          vge (Uns p 1) (if Int.eq i Int.zero || Int.eq i Int.one then I i else Uns Pbot 1)).
+  { intros. eapply vge_trans. apply (BOOL1 p i). destruct orb; auto with va. } 
   induction 1;
   unfold vnormalize; generalize Archi.ptr64; intro ptr64; subst; 
   destruct chunk eqn:C; simpl;
@@ -3187,6 +3265,12 @@ Local Opaque provenance.
 - constructor... apply is_sign_ext_uns...
 - constructor... apply is_sign_ext_sgn...
 - constructor... apply is_zero_ext_uns... apply Z.min_case...
+- constructor... apply is_sign_ext_uns...
+- constructor... apply is_sign_ext_sgn...
+- constructor... apply is_zero_ext_uns... apply Z.min_case...
+- constructor... apply is_sign_ext_uns...
+- constructor... apply is_sign_ext_sgn...
+- constructor... apply is_zero_ext_uns... apply Z.min_case...
 - rewrite zlt_true by lia...
 - destruct (zlt n2 8)...
 - rewrite zlt_true by lia...
@@ -3195,18 +3279,30 @@ Local Opaque provenance.
 - constructor... apply is_zero_ext_uns...
 - constructor... apply is_sign_ext_sgn... apply Z.min_case...
 - constructor... apply is_zero_ext_uns...
+- constructor... apply is_sign_ext_sgn... apply Z.min_case...
+- constructor... apply is_zero_ext_uns...
+- constructor... apply is_sign_ext_sgn... apply Z.min_case...
+- constructor... apply is_zero_ext_uns...
 - destruct (zlt n2 8); constructor...
 - destruct (zlt n2 16); constructor...
 - constructor... apply is_sign_ext_sgn...
 - constructor... apply is_zero_ext_uns...
 - constructor... apply is_sign_ext_sgn...
 - constructor... apply is_zero_ext_uns...
+- constructor... apply is_sign_ext_sgn...
+- constructor... apply is_zero_ext_uns...
+- constructor... apply is_sign_ext_sgn...
+- constructor... apply is_zero_ext_uns...
 - destruct (zlt n 8); constructor...
 - destruct (zlt n 16); constructor...
 - constructor... apply is_sign_ext_sgn...
 - constructor... apply is_zero_ext_uns...
 - constructor... apply is_sign_ext_sgn...
 - constructor... apply is_zero_ext_uns...
+- constructor... apply is_sign_ext_sgn...
+- constructor... apply is_zero_ext_uns...
+- constructor... apply is_sign_ext_sgn...
+- constructor... apply is_zero_ext_uns...
 - destruct (zlt n 8); constructor...
 - destruct (zlt n 16); constructor...
 Qed.

From f3f1dc29e9f527acebf0f71afca1a964bba1f5cb Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Wed, 21 Aug 2024 09:14:30 +0200
Subject: [PATCH 2/2] Constant propagation: optimize "known integer or Vundef"
 results

Results that analyze to `IU n` are turned into
`load-integer-immediate(n)` operations.

This is semantically safe, and enables compile-time evaluation of some
pointer comparisons (e.g. `&x == &x` where `x` is a global variable or
a stack-allocated variable).
---
 aarch64/ConstpropOp.vp     | 2 +-
 aarch64/ConstpropOpproof.v | 2 ++
 arm/ConstpropOp.vp         | 2 +-
 arm/ConstpropOpproof.v     | 2 ++
 powerpc/ConstpropOp.vp     | 2 +-
 powerpc/ConstpropOpproof.v | 2 ++
 riscV/ConstpropOp.vp       | 2 +-
 riscV/ConstpropOpproof.v   | 2 ++
 x86/ConstpropOp.vp         | 2 +-
 x86/ConstpropOpproof.v     | 2 ++
 10 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/aarch64/ConstpropOp.vp b/aarch64/ConstpropOp.vp
index f2d17a519..5ab21b60d 100644
--- a/aarch64/ConstpropOp.vp
+++ b/aarch64/ConstpropOp.vp
@@ -23,7 +23,7 @@ Require SelectOp.
 
 Definition const_for_result (a: aval) : option operation :=
   match a with
-  | I n => Some(Ointconst n)
+  | I n | IU n => Some(Ointconst n)
   | L n => Some(Olongconst n)
   | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None
   | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None
diff --git a/aarch64/ConstpropOpproof.v b/aarch64/ConstpropOpproof.v
index 7f5f1e06f..7f60ef9a4 100644
--- a/aarch64/ConstpropOpproof.v
+++ b/aarch64/ConstpropOpproof.v
@@ -92,6 +92,8 @@ Proof.
   unfold const_for_result; intros; destruct a; inv H; SimplVM.
 - (* integer *)
   exists (Vint n); auto.
+- (* integer or undef *)
+  exists (Vint n); split; auto. inv H0; auto.
 - (* long *)
   exists (Vlong n); auto.
 - (* float *)
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index 8555d3aab..986be7148 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -26,7 +26,7 @@ Require Import ValueDomain ValueAOp.
 
 Definition const_for_result (a: aval) : option operation :=
   match a with
-  | I n => Some(Ointconst n)
+  | I n | IU n => Some(Ointconst n)
   | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None
   | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None
   | Ptr(Gl id ofs) => Some (Oaddrsymbol id ofs)
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index cd0afb7ae..a203145a9 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -107,6 +107,8 @@ Proof.
   destruct a; inv H; SimplVM.
 - (* integer *)
   exists (Vint n); auto.
+- (* integer or undef *)
+  exists (Vint n); split; auto. inv H0; auto.
 - (* float *)
   destruct (generate_float_constants tt); inv H2. exists (Vfloat f); auto.
 - (* single *)
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index 8e90a8496..2e10ec938 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -22,7 +22,7 @@ Require Import ValueDomain ValueAOp.
 
 Definition const_for_result (a: aval) : option operation :=
   match a with
-  | I n => Some(Ointconst n)
+  | I n | IU n => Some(Ointconst n)
   | L n => if Archi.ppc64 then Some (Olongconst n) else None
   | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None
   | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 1dd2e0e42..d6e62fb15 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -101,6 +101,8 @@ Proof.
   destruct a; inv H; SimplVM.
 - (* integer *)
   exists (Vint n); auto.
+- (* integer or undef *)
+  exists (Vint n); split; auto. inv H0; auto.
 - (* long *)
   destruct (Archi.ppc64); inv H2. exists (Vlong n); auto.
 - (* float *)
diff --git a/riscV/ConstpropOp.vp b/riscV/ConstpropOp.vp
index aab2424d6..75f8a2bb8 100644
--- a/riscV/ConstpropOp.vp
+++ b/riscV/ConstpropOp.vp
@@ -23,7 +23,7 @@ Require Import ValueDomain.
 
 Definition const_for_result (a: aval) : option operation :=
   match a with
-  | I n => Some(Ointconst n)
+  | I n | IU n => Some(Ointconst n)
   | L n => if Archi.ptr64 then Some(Olongconst n) else None
   | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None
   | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None
diff --git a/riscV/ConstpropOpproof.v b/riscV/ConstpropOpproof.v
index 8445e55f3..85a19a0a7 100644
--- a/riscV/ConstpropOpproof.v
+++ b/riscV/ConstpropOpproof.v
@@ -91,6 +91,8 @@ Proof.
   destruct a; inv H; SimplVM.
 - (* integer *)
   exists (Vint n); auto.
+- (* integer or undef *)
+  exists (Vint n); split; auto. inv H0; auto.
 - (* long *)
   destruct ptr64; inv H2. exists (Vlong n); auto.
 - (* float *)
diff --git a/x86/ConstpropOp.vp b/x86/ConstpropOp.vp
index dd4b839aa..ada7ca6be 100644
--- a/x86/ConstpropOp.vp
+++ b/x86/ConstpropOp.vp
@@ -25,7 +25,7 @@ Definition Olea_ptr (a: addressing) := if Archi.ptr64 then Oleal a else Olea a.
 
 Definition const_for_result (a: aval) : option operation :=
   match a with
-  | I n => Some(Ointconst n)
+  | I n | IU n => Some(Ointconst n)
   | L n => if Archi.ptr64 then Some(Olongconst n) else None
   | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None
   | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None
diff --git a/x86/ConstpropOpproof.v b/x86/ConstpropOpproof.v
index 09c6e91b8..562495364 100644
--- a/x86/ConstpropOpproof.v
+++ b/x86/ConstpropOpproof.v
@@ -98,6 +98,8 @@ Proof.
   destruct a; inv H; SimplVM.
 - (* integer *)
   exists (Vint n); auto.
+- (* integer or undef *)
+  exists (Vint n); split; auto. inv H0; auto.
 - (* long *)
   destruct ptr64; inv H2. exists (Vlong n); auto.
 - (* float *)