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).

Author: xavierleroy

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

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 *)

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)

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 *)

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

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 *)

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

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 *)

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

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 *)