Implement fixedbv/floatbv conversions in SAT and SMT2 back-ends

regression/cbmc/Double-to-fixedbv1/main.c

@@ -0,0 +1,55 @@
+#include <assert.h>
+#include <math.h>
+
+// Test double to fixedbv conversions
+typedef __CPROVER_fixedbv[32][16] fixedbv_t;
+
+int main(void)
+{
+  // Basic positive conversion
+  double d1 = 10.5;
+  fixedbv_t fixed1 = (fixedbv_t)d1;
+  assert(fixed1 > (fixedbv_t)10.49 && fixed1 < (fixedbv_t)10.51);
+
+  // Basic negative conversion
+  double d2 = -10.5;
+  fixedbv_t fixed2 = (fixedbv_t)d2;
+  assert(fixed2 > (fixedbv_t)(-10.51) && fixed2 < (fixedbv_t)(-10.49));
+
+  // Zero conversion
+  double d3 = 0.0;
+  fixedbv_t fixed3 = (fixedbv_t)d3;
+  assert(fixed3 == (fixedbv_t)0.0);
+
+  // High precision value
+  double d4 = 123.456;
+  fixedbv_t fixed4 = (fixedbv_t)d4;
+  assert(fixed4 > (fixedbv_t)123.455 && fixed4 < (fixedbv_t)123.457);
+
+  // Small fraction
+  double d5 = 0.0625;
+  fixedbv_t fixed5 = (fixedbv_t)d5;
+  assert(fixed5 > (fixedbv_t)0.0624 && fixed5 < (fixedbv_t)0.0626);
+
+  // Large value
+  double d6 = 5000.125;
+  fixedbv_t fixed6 = (fixedbv_t)d6;
+  assert(fixed6 > (fixedbv_t)5000.12 && fixed6 < (fixedbv_t)5000.13);
+
+  // Negative fractional
+  double d7 = -0.75;
+  fixedbv_t fixed7 = (fixedbv_t)d7;
+  assert(fixed7 > (fixedbv_t)(-0.76) && fixed7 < (fixedbv_t)(-0.74));
+
+  // NaN handling
+  double nan_val = NAN;
+  fixedbv_t fixed_nan = (fixedbv_t)nan_val;
+  // NaN conversion is implementation-defined
+
+  // Infinity handling
+  double inf_val = INFINITY;
+  fixedbv_t fixed_inf = (fixedbv_t)inf_val;
+  // Infinity should be clamped to max value
+
+  return 0;
+}

regression/cbmc/Double-to-fixedbv1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/Fixedbv-float-double1/main.c

@@ -0,0 +1,40 @@
+#include <assert.h>
+
+// Test fixedbv conversions with both float and double
+typedef __CPROVER_fixedbv[32][16] fixedbv_t;
+
+int main(void)
+{
+  fixedbv_t fixed_val = (fixedbv_t)123.456;
+
+  // Convert to float
+  float f = (float)fixed_val;
+  assert(f > 123.45f && f < 123.47f);
+
+  // Convert to double
+  double d = (double)fixed_val;
+  assert(d > 123.455 && d < 123.457);
+
+  // Round-trip: fixedbv -> float -> fixedbv
+  float f2 = (float)fixed_val;
+  fixedbv_t fixed_roundtrip1 = (fixedbv_t)f2;
+  assert(
+    fixed_roundtrip1 > (fixedbv_t)123.45 &&
+    fixed_roundtrip1 < (fixedbv_t)123.47);
+
+  // Round-trip: fixedbv -> double -> fixedbv
+  double d2 = (double)fixed_val;
+  fixedbv_t fixed_roundtrip2 = (fixedbv_t)d2;
+  assert(
+    fixed_roundtrip2 > (fixedbv_t)123.45 &&
+    fixed_roundtrip2 < (fixedbv_t)123.47);
+
+  // Test with negative value
+  fixedbv_t fixed_neg = (fixedbv_t)(-50.25);
+  float f_neg = (float)fixed_neg;
+  double d_neg = (double)fixed_neg;
+  assert(f_neg > -50.26f && f_neg < -50.24f);
+  assert(d_neg > -50.26 && d_neg < -50.24);
+
+  return 0;
+}

regression/cbmc/Fixedbv-float-double1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/Fixedbv-float-edge-cases/main.c

@@ -0,0 +1,52 @@
+#include <assert.h>
+#include <math.h>
+
+// Test edge cases for fixedbv/float conversions
+typedef __CPROVER_fixedbv[16][8] fixedbv_small_t;
+typedef __CPROVER_fixedbv[32][16] fixedbv_t;
+
+int main(void)
+{
+  // Test with very small positive value
+  fixedbv_t fixed_tiny = (fixedbv_t)0.001;
+  float f_tiny = (float)fixed_tiny;
+  assert(f_tiny > 0.0f && f_tiny < 0.01f);
+
+  // Test with very small negative value
+  fixedbv_t fixed_tiny_neg = (fixedbv_t)(-0.001);
+  float f_tiny_neg = (float)fixed_tiny_neg;
+  assert(f_tiny_neg < 0.0f && f_tiny_neg > -0.01f);
+
+  // Test conversion of positive zero
+  fixedbv_t fixed_pos_zero = (fixedbv_t)0.0;
+  float f_pos_zero = (float)fixed_pos_zero;
+  assert(f_pos_zero == 0.0f);
+
+  // Test round-trip with precision loss
+  float original = 1.234567f;
+  fixedbv_t fixed = (fixedbv_t)original;
+  float roundtrip = (float)fixed;
+  // Should be approximately equal (within fixedbv precision)
+  assert(roundtrip > 1.23f && roundtrip < 1.25f);
+
+  // Test boundary values for smaller fixedbv type
+  fixedbv_small_t small_pos = (fixedbv_small_t)127.0;
+  float f_small_pos = (float)small_pos;
+  assert(f_small_pos > 126.9f && f_small_pos < 127.1f);
+
+  fixedbv_small_t small_neg = (fixedbv_small_t)(-128.0);
+  float f_small_neg = (float)small_neg;
+  assert(f_small_neg > -128.1f && f_small_neg < -127.9f);
+
+  // Test float to fixedbv with values that should fit
+  float f_in_range = 50.5f;
+  fixedbv_t fixed_in_range = (fixedbv_t)f_in_range;
+  assert(fixed_in_range > (fixedbv_t)50.4 && fixed_in_range < (fixedbv_t)50.6);
+
+  // Test float to fixedbv with truncation
+  float f_trunc = 3.9999f;
+  fixedbv_t fixed_trunc = (fixedbv_t)f_trunc;
+  assert(fixed_trunc > (fixedbv_t)3.99 && fixed_trunc < (fixedbv_t)4.01);
+
+  return 0;
+}

regression/cbmc/Fixedbv-float-edge-cases/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/Fixedbv-float-precisions/main.c

@@ -0,0 +1,68 @@
+#include <assert.h>
+
+// Test fixedbv/float conversions with different precisions
+typedef __CPROVER_fixedbv[16]
+                         [8] fixedbv_16_8_t; // 16 bits total, 8 fraction bits
+typedef __CPROVER_fixedbv
+  [32][16] fixedbv_32_16_t; // 32 bits total, 16 fraction bits
+typedef __CPROVER_fixedbv
+  [24][12] fixedbv_24_12_t; // 24 bits total, 12 fraction bits
+
+int main(void)
+{
+  // Test with 16-bit fixedbv (8 fraction bits)
+  fixedbv_16_8_t fixed_16 = (fixedbv_16_8_t)10.25;
+  float f_16 = (float)fixed_16;
+  assert(f_16 > 10.24f && f_16 < 10.26f);
+
+  fixedbv_16_8_t roundtrip_16 = (fixedbv_16_8_t)f_16;
+  assert(
+    roundtrip_16 > (fixedbv_16_8_t)10.24 &&
+    roundtrip_16 < (fixedbv_16_8_t)10.26);
+
+  // Test with 32-bit fixedbv (16 fraction bits)
+  fixedbv_32_16_t fixed_32 = (fixedbv_32_16_t)10.25;
+  float f_32 = (float)fixed_32;
+  assert(f_32 > 10.24f && f_32 < 10.26f);
+
+  fixedbv_32_16_t roundtrip_32 = (fixedbv_32_16_t)f_32;
+  assert(
+    roundtrip_32 > (fixedbv_32_16_t)10.24 &&
+    roundtrip_32 < (fixedbv_32_16_t)10.26);
+
+  // Test with 24-bit fixedbv (12 fraction bits)
+  fixedbv_24_12_t fixed_24 = (fixedbv_24_12_t)10.25;
+  float f_24 = (float)fixed_24;
+  assert(f_24 > 10.24f && f_24 < 10.26f);
+
+  fixedbv_24_12_t roundtrip_24 = (fixedbv_24_12_t)f_24;
+  assert(
+    roundtrip_24 > (fixedbv_24_12_t)10.24 &&
+    roundtrip_24 < (fixedbv_24_12_t)10.26);
+
+  // Test negative values with different precisions
+  fixedbv_16_8_t fixed_16_neg = (fixedbv_16_8_t)(-5.5);
+  float f_16_neg = (float)fixed_16_neg;
+  assert(f_16_neg > -5.51f && f_16_neg < -5.49f);
+
+  fixedbv_32_16_t fixed_32_neg = (fixedbv_32_16_t)(-5.5);
+  float f_32_neg = (float)fixed_32_neg;
+  assert(f_32_neg > -5.51f && f_32_neg < -5.49f);
+
+  fixedbv_24_12_t fixed_24_neg = (fixedbv_24_12_t)(-5.5);
+  float f_24_neg = (float)fixed_24_neg;
+  assert(f_24_neg > -5.51f && f_24_neg < -5.49f);
+
+  // Test fractional precision differences
+  float precise_val = 1.234567f;
+
+  fixedbv_16_8_t fixed_16_prec = (fixedbv_16_8_t)precise_val;
+  float f_16_prec = (float)fixed_16_prec;
+  assert(f_16_prec > 1.23f && f_16_prec < 1.25f);
+
+  fixedbv_32_16_t fixed_32_prec = (fixedbv_32_16_t)precise_val;
+  float f_32_prec = (float)fixed_32_prec;
+  assert(f_32_prec > 1.23f && f_32_prec < 1.25f);
+
+  return 0;
+}

regression/cbmc/Fixedbv-float-precisions/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/Fixedbv-float-roundtrip/main.c

@@ -0,0 +1,55 @@
+#include <assert.h>
+
+// Test round-trip conversions between fixedbv and float
+typedef __CPROVER_fixedbv[32][16] fixedbv_t;
+
+int main(void)
+{
+  // Test 1: fixedbv -> float -> fixedbv
+  fixedbv_t original1 = (fixedbv_t)25.5;
+  float f1 = (float)original1;
+  fixedbv_t result1 = (fixedbv_t)f1;
+  // Should be approximately equal (within precision)
+  assert(result1 > (fixedbv_t)25.49 && result1 < (fixedbv_t)25.51);
+
+  // Test 2: float -> fixedbv -> float
+  float original2 = 37.25f;
+  fixedbv_t fixed2 = (fixedbv_t)original2;
+  float result2 = (float)fixed2;
+  // Should be approximately equal
+  assert(result2 > 37.24f && result2 < 37.26f);
+
+  // Test 3: Negative round-trip
+  fixedbv_t original3 = (fixedbv_t)(-18.75);
+  float f3 = (float)original3;
+  fixedbv_t result3 = (fixedbv_t)f3;
+  assert(result3 > (fixedbv_t)(-18.76) && result3 < (fixedbv_t)(-18.74));
+
+  // Test 4: Zero round-trip
+  fixedbv_t original4 = (fixedbv_t)0.0;
+  float f4 = (float)original4;
+  fixedbv_t result4 = (fixedbv_t)f4;
+  assert(result4 == (fixedbv_t)0.0);
+
+  // Test 5: Small fractional value
+  fixedbv_t original5 = (fixedbv_t)0.0625;
+  float f5 = (float)original5;
+  fixedbv_t result5 = (fixedbv_t)f5;
+  assert(result5 > (fixedbv_t)0.0624 && result5 < (fixedbv_t)0.0626);
+
+  // Test 6: Integer value
+  fixedbv_t original6 = (fixedbv_t)1000.0;
+  float f6 = (float)original6;
+  fixedbv_t result6 = (fixedbv_t)f6;
+  assert(result6 > (fixedbv_t)999.9 && result6 < (fixedbv_t)1000.1);
+
+  // Test 7: Multiple conversions
+  fixedbv_t start = (fixedbv_t)15.5;
+  float temp1 = (float)start;
+  fixedbv_t temp2 = (fixedbv_t)temp1;
+  float temp3 = (float)temp2;
+  fixedbv_t end = (fixedbv_t)temp3;
+  assert(end > (fixedbv_t)15.49 && end < (fixedbv_t)15.51);
+
+  return 0;
+}

regression/cbmc/Fixedbv-float-roundtrip/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/Fixedbv-to-double1/main.c

@@ -0,0 +1,44 @@
+#include <assert.h>
+
+// Test fixedbv to double conversions
+typedef __CPROVER_fixedbv[32][16] fixedbv_t;
+
+int main(void)
+{
+  // Basic positive conversion
+  fixedbv_t fixed_pos = (fixedbv_t)10.5;
+  double d1 = (double)fixed_pos;
+  assert(d1 > 10.49 && d1 < 10.51);
+
+  // Basic negative conversion
+  fixedbv_t fixed_neg = (fixedbv_t)(-10.5);
+  double d2 = (double)fixed_neg;
+  assert(d2 > -10.51 && d2 < -10.49);
+
+  // Zero conversion
+  fixedbv_t fixed_zero = (fixedbv_t)0.0;
+  double d3 = (double)fixed_zero;
+  assert(d3 == 0.0);
+
+  // High precision value
+  fixedbv_t fixed_prec = (fixedbv_t)123.456;
+  double d4 = (double)fixed_prec;
+  assert(d4 > 123.455 && d4 < 123.457);
+
+  // Small fraction
+  fixedbv_t fixed_small = (fixedbv_t)0.0625;
+  double d5 = (double)fixed_small;
+  assert(d5 > 0.0624 && d5 < 0.0626);
+
+  // Large value
+  fixedbv_t fixed_large = (fixedbv_t)5000.125;
+  double d6 = (double)fixed_large;
+  assert(d6 > 5000.12 && d6 < 5000.13);
+
+  // Negative fractional
+  fixedbv_t fixed_neg_frac = (fixedbv_t)(-0.75);
+  double d7 = (double)fixed_neg_frac;
+  assert(d7 > -0.76 && d7 < -0.74);
+
+  return 0;
+}

regression/cbmc/Fixedbv-to-double1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring