Skip to content

Bugfix/overflow test #771

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Apr 13, 2017
Merged

Bugfix/overflow test #771

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
219b8bd
Make it clear test isn't really working
Apr 6, 2017
8dcd386
Make test work again and turn it on
Apr 6, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 14 additions & 7 deletions regression/cbmc/unsigned___int128/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,30 +1,37 @@
# include <stdint.h>

typedef unsigned __int128 uint128_t;
typedef unsigned __int128 uint128_t;

typedef uint64_t limb;
typedef uint128_t widelimb;

typedef limb felem[4];
typedef widelimb widefelem[7];

felem p = {0x1FFFFFFFFFFFFFF,
0xFFFFFFFFFFFFFF,
0xFFFFE000000000,
felem p = {0x1FFFFFFFFFFFFFF,
0xFFFFFFFFFFFFFF,
0xFFFFE000000000,
0x00000000000002};


/*-
* 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));
__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);
Expand Down Expand Up @@ -75,9 +82,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 */
Expand Down