diff --git a/regression/cbmc/Double-to-fixedbv1/main.c b/regression/cbmc/Double-to-fixedbv1/main.c new file mode 100644 index 00000000000..9f331d76894 --- /dev/null +++ b/regression/cbmc/Double-to-fixedbv1/main.c @@ -0,0 +1,55 @@ +#include +#include + +// 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; +} diff --git a/regression/cbmc/Double-to-fixedbv1/test.desc b/regression/cbmc/Double-to-fixedbv1/test.desc new file mode 100644 index 00000000000..b7d95a28215 --- /dev/null +++ b/regression/cbmc/Double-to-fixedbv1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--floatbv +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Fixedbv-float-double1/main.c b/regression/cbmc/Fixedbv-float-double1/main.c new file mode 100644 index 00000000000..174a3235140 --- /dev/null +++ b/regression/cbmc/Fixedbv-float-double1/main.c @@ -0,0 +1,40 @@ +#include + +// 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; +} diff --git a/regression/cbmc/Fixedbv-float-double1/test.desc b/regression/cbmc/Fixedbv-float-double1/test.desc new file mode 100644 index 00000000000..b7d95a28215 --- /dev/null +++ b/regression/cbmc/Fixedbv-float-double1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--floatbv +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Fixedbv-float-edge-cases/main.c b/regression/cbmc/Fixedbv-float-edge-cases/main.c new file mode 100644 index 00000000000..e8f7cb2d48e --- /dev/null +++ b/regression/cbmc/Fixedbv-float-edge-cases/main.c @@ -0,0 +1,52 @@ +#include +#include + +// 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; +} diff --git a/regression/cbmc/Fixedbv-float-edge-cases/test.desc b/regression/cbmc/Fixedbv-float-edge-cases/test.desc new file mode 100644 index 00000000000..b7d95a28215 --- /dev/null +++ b/regression/cbmc/Fixedbv-float-edge-cases/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--floatbv +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Fixedbv-float-precisions/main.c b/regression/cbmc/Fixedbv-float-precisions/main.c new file mode 100644 index 00000000000..6c52255fc75 --- /dev/null +++ b/regression/cbmc/Fixedbv-float-precisions/main.c @@ -0,0 +1,68 @@ +#include + +// 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; +} diff --git a/regression/cbmc/Fixedbv-float-precisions/test.desc b/regression/cbmc/Fixedbv-float-precisions/test.desc new file mode 100644 index 00000000000..b7d95a28215 --- /dev/null +++ b/regression/cbmc/Fixedbv-float-precisions/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--floatbv +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Fixedbv-float-roundtrip/main.c b/regression/cbmc/Fixedbv-float-roundtrip/main.c new file mode 100644 index 00000000000..c1ec07dd61e --- /dev/null +++ b/regression/cbmc/Fixedbv-float-roundtrip/main.c @@ -0,0 +1,55 @@ +#include + +// 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; +} diff --git a/regression/cbmc/Fixedbv-float-roundtrip/test.desc b/regression/cbmc/Fixedbv-float-roundtrip/test.desc new file mode 100644 index 00000000000..b7d95a28215 --- /dev/null +++ b/regression/cbmc/Fixedbv-float-roundtrip/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--floatbv +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Fixedbv-to-double1/main.c b/regression/cbmc/Fixedbv-to-double1/main.c new file mode 100644 index 00000000000..6aa24c73883 --- /dev/null +++ b/regression/cbmc/Fixedbv-to-double1/main.c @@ -0,0 +1,44 @@ +#include + +// 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; +} diff --git a/regression/cbmc/Fixedbv-to-double1/test.desc b/regression/cbmc/Fixedbv-to-double1/test.desc new file mode 100644 index 00000000000..b7d95a28215 --- /dev/null +++ b/regression/cbmc/Fixedbv-to-double1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--floatbv +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Fixedbv-to-float-smt2/main.c b/regression/cbmc/Fixedbv-to-float-smt2/main.c new file mode 100644 index 00000000000..41e5d00a1fe --- /dev/null +++ b/regression/cbmc/Fixedbv-to-float-smt2/main.c @@ -0,0 +1,34 @@ +#include + +// Test fixedbv to float conversions with SMT2 backend +typedef __CPROVER_fixedbv[32][16] fixedbv_t; + +int main(void) +{ + // Test basic conversion + fixedbv_t fixed1 = (fixedbv_t)5.5; + float f1 = (float)fixed1; + assert(f1 > 5.49f && f1 < 5.51f); + + // Test negative conversion + fixedbv_t fixed2 = (fixedbv_t)(-7.25); + float f2 = (float)fixed2; + assert(f2 > -7.26f && f2 < -7.24f); + + // Test zero + fixedbv_t fixed3 = (fixedbv_t)0.0; + float f3 = (float)fixed3; + assert(f3 == 0.0f); + + // Test fractional value + fixedbv_t fixed4 = (fixedbv_t)0.125; + float f4 = (float)fixed4; + assert(f4 > 0.124f && f4 < 0.126f); + + // Test integer value + fixedbv_t fixed5 = (fixedbv_t)100.0; + float f5 = (float)fixed5; + assert(f5 > 99.9f && f5 < 100.1f); + + return 0; +} diff --git a/regression/cbmc/Fixedbv-to-float-smt2/test.desc b/regression/cbmc/Fixedbv-to-float-smt2/test.desc new file mode 100644 index 00000000000..459f231be5c --- /dev/null +++ b/regression/cbmc/Fixedbv-to-float-smt2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--floatbv --smt2 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Fixedbv-to-float1/main.c b/regression/cbmc/Fixedbv-to-float1/main.c new file mode 100644 index 00000000000..e725da6aa18 --- /dev/null +++ b/regression/cbmc/Fixedbv-to-float1/main.c @@ -0,0 +1,44 @@ +#include + +// Test fixedbv to float conversions +typedef __CPROVER_fixedbv[32][16] fixedbv_t; + +int main(void) +{ + // Basic positive conversion + fixedbv_t fixed_pos = (fixedbv_t)10.5; + float f1 = (float)fixed_pos; + assert(f1 > 10.49f && f1 < 10.51f); + + // Basic negative conversion + fixedbv_t fixed_neg = (fixedbv_t)(-10.5); + float f2 = (float)fixed_neg; + assert(f2 > -10.51f && f2 < -10.49f); + + // Zero conversion + fixedbv_t fixed_zero = (fixedbv_t)0.0; + float f3 = (float)fixed_zero; + assert(f3 == 0.0f); + + // Integer value (no fraction) + fixedbv_t fixed_int = (fixedbv_t)42.0; + float f4 = (float)fixed_int; + assert(f4 > 41.99f && f4 < 42.01f); + + // Small fraction + fixedbv_t fixed_small = (fixedbv_t)0.25; + float f5 = (float)fixed_small; + assert(f5 > 0.24f && f5 < 0.26f); + + // Large value + fixedbv_t fixed_large = (fixedbv_t)1000.75; + float f6 = (float)fixed_large; + assert(f6 > 1000.7f && f6 < 1000.8f); + + // Negative small fraction + fixedbv_t fixed_neg_small = (fixedbv_t)(-0.25); + float f7 = (float)fixed_neg_small; + assert(f7 > -0.26f && f7 < -0.24f); + + return 0; +} diff --git a/regression/cbmc/Fixedbv-to-float1/test.desc b/regression/cbmc/Fixedbv-to-float1/test.desc new file mode 100644 index 00000000000..b7d95a28215 --- /dev/null +++ b/regression/cbmc/Fixedbv-to-float1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--floatbv +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Float-to-fixedbv-overflow/main.c b/regression/cbmc/Float-to-fixedbv-overflow/main.c new file mode 100644 index 00000000000..88467d5d1b2 --- /dev/null +++ b/regression/cbmc/Float-to-fixedbv-overflow/main.c @@ -0,0 +1,54 @@ +#include +#include + +// Test float to fixedbv overflow and clamping behavior +typedef __CPROVER_fixedbv + [16][8] fixedbv_small_t; // Small type for easier overflow testing + +int main(void) +{ + // Test value that fits within range + float f1 = 50.5f; + fixedbv_small_t fixed1 = (fixedbv_small_t)f1; + assert(fixed1 > (fixedbv_small_t)50.4 && fixed1 < (fixedbv_small_t)50.6); + + // Test large positive value (potential overflow) + // For 16-bit fixedbv with 8 fraction bits: max ~= 127.99 + float f2 = 127.0f; + fixedbv_small_t fixed2 = (fixedbv_small_t)f2; + assert(fixed2 > (fixedbv_small_t)126.9 && fixed2 < (fixedbv_small_t)127.1); + + // Test large negative value (potential underflow) + // Min ~= -128.0 + float f3 = -128.0f; + fixedbv_small_t fixed3 = (fixedbv_small_t)f3; + assert( + fixed3 > (fixedbv_small_t)(-128.1) && fixed3 < (fixedbv_small_t)(-127.9)); + + // Test value very close to zero + float f4 = 0.01f; + fixedbv_small_t fixed4 = (fixedbv_small_t)f4; + assert(fixed4 > (fixedbv_small_t)0.0 && fixed4 < (fixedbv_small_t)0.02); + + // Test negative value close to zero + float f5 = -0.01f; + fixedbv_small_t fixed5 = (fixedbv_small_t)f5; + assert(fixed5 > (fixedbv_small_t)(-0.02) && fixed5 < (fixedbv_small_t)0.0); + + // Test positive infinity (should be clamped) + float inf_pos = INFINITY; + fixedbv_small_t fixed_inf_pos = (fixedbv_small_t)inf_pos; + // Should be clamped to max value (implementation-defined behavior) + + // Test negative infinity (should be clamped) + float inf_neg = -INFINITY; + fixedbv_small_t fixed_inf_neg = (fixedbv_small_t)inf_neg; + // Should be clamped to min value (implementation-defined behavior) + + // Test NaN (should result in zero or implementation-defined value) + float nan_val = NAN; + fixedbv_small_t fixed_nan = (fixedbv_small_t)nan_val; + // NaN handling is implementation-defined + + return 0; +} diff --git a/regression/cbmc/Float-to-fixedbv-overflow/test.desc b/regression/cbmc/Float-to-fixedbv-overflow/test.desc new file mode 100644 index 00000000000..b7d95a28215 --- /dev/null +++ b/regression/cbmc/Float-to-fixedbv-overflow/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--floatbv +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Float-to-fixedbv-smt2/main.c b/regression/cbmc/Float-to-fixedbv-smt2/main.c new file mode 100644 index 00000000000..5df9e1258da --- /dev/null +++ b/regression/cbmc/Float-to-fixedbv-smt2/main.c @@ -0,0 +1,34 @@ +#include + +// Test float to fixedbv conversions with SMT2 backend +typedef __CPROVER_fixedbv[32][16] fixedbv_t; + +int main(void) +{ + // Test basic conversion + float f1 = 5.5f; + fixedbv_t fixed1 = (fixedbv_t)f1; + assert(fixed1 > (fixedbv_t)5.49 && fixed1 < (fixedbv_t)5.51); + + // Test negative conversion + float f2 = -7.25f; + fixedbv_t fixed2 = (fixedbv_t)f2; + assert(fixed2 > (fixedbv_t)(-7.26) && fixed2 < (fixedbv_t)(-7.24)); + + // Test zero + float f3 = 0.0f; + fixedbv_t fixed3 = (fixedbv_t)f3; + assert(fixed3 == (fixedbv_t)0.0); + + // Test fractional value + float f4 = 0.125f; + fixedbv_t fixed4 = (fixedbv_t)f4; + assert(fixed4 > (fixedbv_t)0.124 && fixed4 < (fixedbv_t)0.126); + + // Test integer value + float f5 = 100.0f; + fixedbv_t fixed5 = (fixedbv_t)f5; + assert(fixed5 > (fixedbv_t)99.9 && fixed5 < (fixedbv_t)100.1); + + return 0; +} diff --git a/regression/cbmc/Float-to-fixedbv-smt2/test.desc b/regression/cbmc/Float-to-fixedbv-smt2/test.desc new file mode 100644 index 00000000000..459f231be5c --- /dev/null +++ b/regression/cbmc/Float-to-fixedbv-smt2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--floatbv --smt2 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Float-to-fixedbv1/main.c b/regression/cbmc/Float-to-fixedbv1/main.c new file mode 100644 index 00000000000..977d2c8b713 --- /dev/null +++ b/regression/cbmc/Float-to-fixedbv1/main.c @@ -0,0 +1,55 @@ +#include +#include + +// Test float to fixedbv conversions +typedef __CPROVER_fixedbv[32][16] fixedbv_t; + +int main(void) +{ + // Basic positive conversion + float f1 = 10.5f; + fixedbv_t fixed1 = (fixedbv_t)f1; + assert(fixed1 > (fixedbv_t)10.49 && fixed1 < (fixedbv_t)10.51); + + // Basic negative conversion + float f2 = -10.5f; + fixedbv_t fixed2 = (fixedbv_t)f2; + assert(fixed2 > (fixedbv_t)(-10.51) && fixed2 < (fixedbv_t)(-10.49)); + + // Zero conversion + float f3 = 0.0f; + fixedbv_t fixed3 = (fixedbv_t)f3; + assert(fixed3 == (fixedbv_t)0.0); + + // Integer value (no fraction) + float f4 = 42.0f; + fixedbv_t fixed4 = (fixedbv_t)f4; + assert(fixed4 > (fixedbv_t)41.99 && fixed4 < (fixedbv_t)42.01); + + // Small fraction + float f5 = 0.25f; + fixedbv_t fixed5 = (fixedbv_t)f5; + assert(fixed5 > (fixedbv_t)0.24 && fixed5 < (fixedbv_t)0.26); + + // Large value + float f6 = 1000.75f; + fixedbv_t fixed6 = (fixedbv_t)f6; + assert(fixed6 > (fixedbv_t)1000.7 && fixed6 < (fixedbv_t)1000.8); + + // Negative small fraction + float f7 = -0.25f; + fixedbv_t fixed7 = (fixedbv_t)f7; + assert(fixed7 > (fixedbv_t)(-0.26) && fixed7 < (fixedbv_t)(-0.24)); + + // NaN handling - result should be zero or clamped + float nan_val = NAN; + fixedbv_t fixed_nan = (fixedbv_t)nan_val; + // NaN conversion is implementation-defined, just check it doesn't crash + + // Infinity handling - result should be clamped to max + float inf_val = INFINITY; + fixedbv_t fixed_inf = (fixedbv_t)inf_val; + // Infinity conversion should be clamped to max value + + return 0; +} diff --git a/regression/cbmc/Float-to-fixedbv1/test.desc b/regression/cbmc/Float-to-fixedbv1/test.desc new file mode 100644 index 00000000000..b7d95a28215 --- /dev/null +++ b/regression/cbmc/Float-to-fixedbv1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--floatbv +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp index 84d25cc8883..9d680d6ffd6 100644 --- a/src/solvers/flattening/boolbv_typecast.cpp +++ b/src/solvers/flattening/boolbv_typecast.cpp @@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include #include #include #include @@ -193,12 +194,70 @@ bool boolbvt::type_conversion( dest.resize(dest_width); return false; + case bvtypet::IS_FIXED: // fixed to float + { + // Convert fixedbv to floatbv + // fixedbv format: [sign bit][integer bits][fraction bits] + const fixedbv_typet &fixedbv_type = to_fixedbv_type(src_type); + std::size_t fraction_bits = fixedbv_type.get_fraction_bits(); + std::size_t integer_bits = fixedbv_type.get_integer_bits(); + + float_utils.spec = ieee_float_spect(to_floatbv_type(dest_type)); + + // Convert fixed-point to integer by treating it as a scaled integer + // The value is: bits / (2^fraction_bits) + // We can use from_signed_integer and then divide by 2^fraction_bits + // But since float_utils doesn't have direct division by power of 2, + // we'll construct the float manually from the components + + // Extract sign bit + literalt sign_bit = src[src_width - 1]; + + // Take absolute value of the fixed-point number + bvt abs_src = bv_utils.absolute_value(src); + + // Extract integer part (upper bits after fraction) + bvt integer_part; + for(std::size_t i = 0; i < integer_bits; i++) + integer_part.push_back(abs_src[fraction_bits + i]); + + // Extract fraction part (lower bits) + bvt fraction_part; + for(std::size_t i = 0; i < fraction_bits; i++) + fraction_part.push_back(abs_src[i]); + + // Convert integer part to float + bvt integer_as_float = float_utils.from_unsigned_integer(integer_part); + + // Convert fraction part to float: fraction / (2^fraction_bits) + // Build 2^fraction_bits as a float + mp_integer divisor = power(mp_integer(2), mp_integer(fraction_bits)); + ieee_float_spect dest_spec(to_floatbv_type(dest_type)); + ieee_floatt divisor_float(dest_spec, ieee_floatt::ROUND_TO_EVEN); + divisor_float.from_integer(divisor); + bvt divisor_bv = convert_bv(divisor_float.to_expr()); + + // Convert fraction part to unsigned integer then to float + bvt fraction_as_float = float_utils.from_unsigned_integer(fraction_part); + + // Divide fraction by 2^fraction_bits + bvt scaled_fraction = float_utils.div(fraction_as_float, divisor_bv); + + // Add integer and scaled fraction parts + bvt result = float_utils.add(integer_as_float, scaled_fraction); + + // Apply sign + dest = result; + dest[dest.size() - 1] = sign_bit; + + return false; + } + case bvtypet::IS_C_BIT_FIELD: case bvtypet::IS_UNKNOWN: case bvtypet::IS_RANGE: case bvtypet::IS_VERILOG_UNSIGNED: case bvtypet::IS_VERILOG_SIGNED: - case bvtypet::IS_FIXED: if(src_type.id() == ID_bool) { // bool to float @@ -302,6 +361,86 @@ bool boolbvt::type_conversion( return false; } + else if(src_bvtype == bvtypet::IS_FLOAT) + { + // float to fixed + float_utilst float_utils(prop, to_floatbv_type(src_type)); + + const fixedbv_typet &dest_fixedbv_type = to_fixedbv_type(dest_type); + std::size_t dest_fraction_bits = dest_fixedbv_type.get_fraction_bits(); + std::size_t dest_integer_bits = dest_fixedbv_type.get_integer_bits(); + + // Handle special cases first + literalt is_nan = float_utils.is_NaN(src); + literalt is_inf = float_utils.is_infinity(src); + literalt is_zero_val = float_utils.is_zero(src); + + // For NaN and infinity, we'll set result to zero (could be implementation-defined) + bvt zero_result; + zero_result.resize(dest_width, const_literal(false)); + + // Extract sign of the float + literalt sign_bit = float_utils.sign_bit(src); + + // Convert float to signed integer (this handles the scaling) + // We need to scale by 2^fraction_bits to get the fixed-point representation + + // Create scaling factor: 2^fraction_bits as a float + mp_integer scale_factor = + power(mp_integer(2), mp_integer(dest_fraction_bits)); + ieee_float_spect src_spec(to_floatbv_type(src_type)); + ieee_floatt scale_float(src_spec, ieee_floatt::ROUND_TO_EVEN); + scale_float.from_integer(scale_factor); + bvt scale_bv = convert_bv(scale_float.to_expr()); + + // Multiply float by scaling factor + bvt scaled_float = float_utils.mul(src, scale_bv); + + // Convert to signed integer with appropriate width + bvt integer_result = + float_utils.to_signed_integer(scaled_float, dest_width); + + // Handle overflow/underflow by clamping + // Maximum positive value for signed fixed-point + mp_integer max_val = power(mp_integer(2), mp_integer(dest_width - 1)) - 1; + bvt max_bv = bv_utils.build_constant(max_val, dest_width); + + // Minimum negative value for signed fixed-point + mp_integer min_val = -power(mp_integer(2), mp_integer(dest_width - 1)); + bvt min_bv = bv_utils.build_constant(min_val, dest_width); + + // Check for overflow (result > max_val) + literalt overflow_pos = bv_utils.signed_less_than(max_bv, integer_result); + + // Check for underflow (result < min_val) + literalt overflow_neg = bv_utils.signed_less_than(integer_result, min_bv); + + // Select result based on conditions + // If NaN or infinity, use zero + // If overflow positive, use max_val + // If overflow negative, use min_val + // Otherwise use integer_result + literalt use_zero = prop.lor(is_nan, is_inf); + literalt use_max = prop.land(!use_zero, overflow_pos); + literalt use_min = + prop.land(!use_zero, prop.land(!overflow_pos, overflow_neg)); + + dest.resize(dest_width); + for(std::size_t i = 0; i < dest_width; i++) + { + literalt normal_bit = integer_result[i]; + literalt max_bit = max_bv[i]; + literalt min_bit = min_bv[i]; + literalt zero_bit = const_literal(false); + + // Mux between the different cases + literalt tmp1 = prop.lselect(use_max, max_bit, normal_bit); + literalt tmp2 = prop.lselect(use_min, min_bit, tmp1); + dest[i] = prop.lselect(use_zero, zero_bit, tmp2); + } + + return false; + } else if(src_type.id() == ID_bool) { // bool to fixed diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 50a59a6f9dd..8cf55882979 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -3107,6 +3107,59 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) out << "))"; // concat, let } + else if(src_type.id() == ID_floatbv) // floatbv to fixedbv + { + // Convert float to fixed-point + // Strategy: multiply float by 2^fraction_bits, then convert to signed integer + const fixedbv_typet &dest_fixedbv_type = to_fixedbv_type(dest_type); + std::size_t dest_fraction_bits = dest_fixedbv_type.get_fraction_bits(); + std::size_t dest_width = dest_fixedbv_type.get_width(); + + if(use_FPA_theory) + { + const floatbv_typet &src_floatbv_type = to_floatbv_type(src_type); + + // Create scaling factor 2^fraction_bits as a float + mp_integer scale_factor = + power(mp_integer(2), mp_integer(dest_fraction_bits)); + ieee_floatt scale_float(src_floatbv_type, ieee_floatt::ROUND_TO_EVEN); + scale_float.from_integer(scale_factor); + + // Multiply by scaling factor + out << "(let ((scaled_val (fp.mul RNE "; + convert_expr(src); + out << " "; + convert_constant(scale_float.to_expr()); + out << "))) "; + + // Convert to signed bitvector + out << "(fp.to_sbv " << dest_width << " RNE scaled_val))"; + } + else + { + // Without FPA theory, we work with the bit-level representation + // This is more complex and requires manual handling + // For now, we'll use a simplified approach treating it as bit manipulation + + // Get the float as bitvector + out << "(let ((float_bv "; + convert_expr(src); + out << ")) "; + + // Create scale factor as bitvector representation of float + mp_integer scale_factor = + power(mp_integer(2), mp_integer(dest_fraction_bits)); + ieee_floatt scale_float( + to_floatbv_type(src_type), ieee_floatt::ROUND_TO_EVEN); + scale_float.from_integer(scale_factor); + + // This is a placeholder - proper implementation would need float arithmetic + // For bit-level representation without FPA, we'd need to implement + // float multiplication and conversion manually + SMT2_TODO("floatbv to fixedbv conversion without FPA theory"); + out << "(_ bv0 " << dest_width << "))"; // Close let + } + } else UNEXPECTEDCASE("unexpected typecast to fixedbv"); } @@ -3221,6 +3274,50 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) else convert_expr(src); } + else if(src_type.id() == ID_fixedbv) // fixedbv to floatbv + { + // Convert fixed-point to floating-point + // Strategy: treat fixedbv as signed integer, convert to float, then + // divide by 2^fraction_bits + const fixedbv_typet &src_fixedbv_type = to_fixedbv_type(src_type); + std::size_t src_fraction_bits = src_fixedbv_type.get_fraction_bits(); + std::size_t src_width = src_fixedbv_type.get_width(); + + if(use_FPA_theory) + { + // Convert the fixedbv (as signed integer) to float + out << "(let ((fixed_as_int "; + convert_expr(src); + out << ")) "; + + // Convert signed integer to float + out << "(fp.div RNE "; + out << "((_ to_fp " << dest_floatbv_type.get_e() << " " + << dest_floatbv_type.get_f() + 1 << ") "; + out << "fixed_as_int)"; + + // Create divisor: 2^fraction_bits as a float + mp_integer divisor = + power(mp_integer(2), mp_integer(src_fraction_bits)); + ieee_floatt divisor_float( + dest_floatbv_type, ieee_floatt::ROUND_TO_EVEN); + divisor_float.from_integer(divisor); + + out << " "; + convert_constant(divisor_float.to_expr()); + out << "))"; // Close fp.div and let + } + else + { + // Without FPA theory, use bit-level representation + // This is complex - would need manual float construction + // For now, provide a placeholder + SMT2_TODO("fixedbv to floatbv conversion without FPA theory"); + + // At minimum, output something valid + out << "(_ bv0 " << dest_floatbv_type.get_width() << ")"; + } + } else UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> float"); }