From 219b8bd2cbc51e050616d3a6dc4f550539225497 Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Thu, 6 Apr 2017 15:12:56 +0100 Subject: [PATCH 1/2] Make it clear test isn't really working CBMC can't cope with arrays as parameters to C functions yet. It assumes they are null pointers. I'm not sure why this test was passing, but refactoring it to not use arrays makes it clear it shouldn't be. (Also remove some unneeded whitespace.) --- regression/cbmc/unsigned___int128/main.c | 18 +++++++++++------- regression/cbmc/unsigned___int128/test.desc | 2 +- 2 files changed, 12 insertions(+), 8 deletions(-) diff --git a/regression/cbmc/unsigned___int128/main.c b/regression/cbmc/unsigned___int128/main.c index b695484a332..21cfcf4a0df 100644 --- a/regression/cbmc/unsigned___int128/main.c +++ b/regression/cbmc/unsigned___int128/main.c @@ -1,6 +1,6 @@ # include -typedef unsigned __int128 uint128_t; +typedef unsigned __int128 uint128_t; typedef uint64_t limb; typedef uint128_t widelimb; @@ -8,9 +8,9 @@ typedef uint128_t widelimb; typedef limb felem[4]; typedef widelimb widefelem[7]; -felem p = {0x1FFFFFFFFFFFFFF, - 0xFFFFFFFFFFFFFF, - 0xFFFFE000000000, +felem p = {0x1FFFFFFFFFFFFFF, + 0xFFFFFFFFFFFFFF, + 0xFFFFE000000000, 0x00000000000002}; @@ -18,8 +18,12 @@ felem p = {0x1FFFFFFFFFFFFFF, * Reduce seven 128-bit coefficients to four 64-bit coefficients. * Requires in[i] < 2^126, * ensures out[0] < 2^56, out[1] < 2^56, out[2] < 2^56, out[3] <= 2^56 + 2^16 */ -void reduce(felem out, const widefelem in) +void reduce( + limb out0, limb out1, limb out2, limb out3, widelimb in0, widelimb in1, + widelimb in2, widelimb in3, widelimb in4, widelimb in5, widelimb in6) { + felem out = {out0, out1, out2, out3}; + const widefelem in = {in0, in1, in2, in3, in4, in5, in6}; __CPROVER_assume(in[0]<(widelimb)((widelimb)1<<126)); __CPROVER_assume(in[1]<((widelimb)1<<126)); @@ -75,9 +79,9 @@ void reduce(felem out, const widefelem in) output[2] += output[1] >> 56; /* output[2] < 2^57 + 2^72 */ - + assert(output[2] < (((widelimb)1)<<57)+(((widelimb)1)<<72)); - + out[1] = output[1] & 0x00ffffffffffffff; output[3] += output[2] >> 56; /* output[3] <= 2^56 + 2^16 */ diff --git a/regression/cbmc/unsigned___int128/test.desc b/regression/cbmc/unsigned___int128/test.desc index 67b0294bc90..aaeabeba360 100644 --- a/regression/cbmc/unsigned___int128/test.desc +++ b/regression/cbmc/unsigned___int128/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --unsigned-overflow-check --signed-overflow-check --function reduce ^EXIT=0$ From 8dcd386add4214eb95012a3816ae817fac5a658d Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Thu, 6 Apr 2017 15:44:59 +0100 Subject: [PATCH 2/2] Make test work again and turn it on Three assumptions were missing. Now the test works and we can turn it back on. --- regression/cbmc/unsigned___int128/main.c | 3 +++ regression/cbmc/unsigned___int128/test.desc | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/regression/cbmc/unsigned___int128/main.c b/regression/cbmc/unsigned___int128/main.c index 21cfcf4a0df..b3bfbd5ea28 100644 --- a/regression/cbmc/unsigned___int128/main.c +++ b/regression/cbmc/unsigned___int128/main.c @@ -29,6 +29,9 @@ void reduce( __CPROVER_assume(in[1]<((widelimb)1<<126)); __CPROVER_assume(in[2]<((widelimb)1<<126)); __CPROVER_assume(in[3]<((widelimb)1<<126)); + __CPROVER_assume(in[4]<((widelimb)1<<126)); + __CPROVER_assume(in[5]<((widelimb)1<<126)); + __CPROVER_assume(in[6]<((widelimb)1<<126)); static const widelimb two127p15 = (((widelimb) 1) << 127) + (((widelimb) 1) << 15); diff --git a/regression/cbmc/unsigned___int128/test.desc b/regression/cbmc/unsigned___int128/test.desc index aaeabeba360..67b0294bc90 100644 --- a/regression/cbmc/unsigned___int128/test.desc +++ b/regression/cbmc/unsigned___int128/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --unsigned-overflow-check --signed-overflow-check --function reduce ^EXIT=0$