Merge pull request #520 from AbsInt/value-analysis-IU

More precise value analysis for "known integer or Vundef" results
AbsInt · Aug 22, 2024 · d351f4b · d351f4b
2 parents af83e9a + f3f1dc2
commit d351f4b
Show file tree

Hide file tree

Showing 11 changed files with 175 additions and 69 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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/backend/ValueDomain.v b/backend/ValueDomain.v
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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 *)