Equivalence extensions

smackers · Sep 12, 2024 · 8c77e35 · 8c77e35
1 parent 0a86b67
commit 8c77e35
Show file tree

Hide file tree

Showing 2 changed files with 78 additions and 14 deletions.
diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c
@@ -2087,36 +2087,41 @@ void __VERIFIER_equiv_assume_signed_long(signed long x, int id) {
   __SMACK_code("assume @ == equiv_store_signed_long(@);", x, id);
 }
 
-void __VERIFIER_equiv_store_float(float x, int id) {
   #ifdef BIT_PRECISE
-	  __SMACK_top_decl("function equiv_store_float(x: bv32) returns (bvfloat);");
+    #define INTT "bv32"
+  #else
+    #define INTT "int"
+  #endif
+  #ifdef FLOAT_ENABLED
+    #define FLOATT "bvfloat"
+    #define DOUBLET "bvdouble"
   #else
-    __SMACK_top_decl("function equiv_store_float(x: int) returns (bvfloat);");
+    #define FLOATT "float"
+    #define DOUBLET "double"
   #endif
-	__SMACK_code("assume equiv_store_float(@) == @;", id, x);
+
+void __VERIFIER_equiv_store_float(float x, int id) {
+  __SMACK_top_decl("function equiv_store_float(x: "INTT") returns ("FLOATT");");
+  __SMACK_code("assume $foeq."FLOATT".bool(equiv_store_float(@),  @f);", id, x);
 }
 
 void __VERIFIER_equiv_check_float(float x, int id) {
-	__SMACK_code("assert @ == equiv_store_float(@);", x, id);
+	__SMACK_code("assert $foeq."FLOATT".bool(@f, equiv_store_float(@));", x, id);
 }
 
 void __VERIFIER_equiv_assume_float(float x, int id) {
-	__SMACK_code("assume @ == equiv_store_float(@);", x, id);
+	__SMACK_code("assume $foeq."FLOATT".bool(@f, equiv_store_float(@));", x, id);
 }
 
 void __VERIFIER_equiv_store_double(double x, int id) {
-  #ifdef BIT_PRECISE
-	  __SMACK_top_decl("function equiv_store_double(x: bv32) returns (bvdouble);");
-  #else
-    __SMACK_top_decl("function equiv_store_double(x: int) returns (bvdouble);");
-  #endif
-	__SMACK_code("assume equiv_store_double(@) == @;", id, x);
+  __SMACK_top_decl("function equiv_store_double(x: "INTT") returns ("DOUBLET");");
+	__SMACK_code("assume $foeq."DOUBLET".bool(equiv_store_double(@), @);", id, x);
 }
 
 void __VERIFIER_equiv_check_double(double x, int id) {
-	__SMACK_code("assert @ == equiv_store_double(@);", x, id);
+	__SMACK_code("assert $foeq."DOUBLET".bool(@, equiv_store_double(@));", x, id);
 }
 
 void __VERIFIER_equiv_assume_double(double x, int id) {
-	__SMACK_code("assume @ == equiv_store_double(@);", x, id);
+	__SMACK_code("assume $foeq."DOUBLET".bool(@, equiv_store_double(@));", x, id);
 }
diff --git a/share/smack/lib/smack.rs b/share/smack/lib/smack.rs
@@ -763,3 +763,62 @@ impl<T: Sized> Deref for Box<T> {
         unsafe { mem::transmute::<*mut T, &T>(self.ptr.as_ptr()) }
     }
 }
+
+// Put config here
+pub trait VerifierFloat {
+    fn verifier_is_nan(self) -> bool;
+    fn verifier_is_infinite(self) -> bool;
+    fn verifier_is_finite(self) -> bool;
+    fn verifier_is_subnormal(self) -> bool;
+    fn verifier_is_normal(self) -> bool;
+}
+
+extern "C" {
+    pub fn __isnanf(x: f32) -> i32;
+    pub fn __isinff(x: f32) -> i32;
+    pub fn __issubnormalf(x: f32) -> i32;
+    pub fn __isnormalf(x: f32) -> i32;
+}
+
+impl VerifierFloat for f32 {
+    fn verifier_is_nan(self) -> bool {
+        unsafe { __isnanf(self) != 0 }
+    }
+    fn verifier_is_infinite(self) -> bool {
+        unsafe { __isinff(self) != 0 }
+    }
+    fn verifier_is_finite(self) -> bool {
+        !self.verifier_is_infinite() && !self.is_nan()
+    }
+    fn verifier_is_subnormal(self) -> bool {
+        unsafe { __issubnormalf(self) != 0 }
+    }
+    fn verifier_is_normal(self) -> bool {
+        unsafe { __isnormalf(self) != 0 }
+    }
+}
+
+extern "C" {
+    pub fn __isnan(x: f64) -> i32;
+    pub fn __isinf(x: f64) -> i32;
+    pub fn __issubnormal(x: f64) -> i32;
+    pub fn __isnormal(x: f64) -> i32;
+}
+
+impl VerifierFloat for f64 {
+    fn verifier_is_nan(self) -> bool {
+        unsafe { __isnan(self) != 0 }
+    }
+    fn verifier_is_infinite(self) -> bool {
+        unsafe { __isinf(self) != 0 }
+    }
+    fn verifier_is_finite(self) -> bool {
+        !self.verifier_is_infinite() && !self.is_nan()
+    }
+    fn verifier_is_subnormal(self) -> bool {
+        unsafe { __issubnormal(self) != 0 }
+    }
+    fn verifier_is_normal(self) -> bool {
+        unsafe { __isnormal(self) != 0 }
+    }
+}