Skip to content

Commit

Permalink
Add a rewrite rule to collapse constant casts
Browse files Browse the repository at this point in the history 
If, e.g., we know from bounds analysis that the result of an operation
fits in the range r[0~>0], we now just replace it with the literal
constant.

Fixes #493
  • Loading branch information
@JasonGross
JasonGross committed Jan 15, 2019
1 parent 538e541 commit efb70cc
Show file tree
Hide file tree
Showing 16 changed files with 6,006 additions and 6,429 deletions.
148 changes: 73 additions & 75 deletions curve25519_32.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -748,43 +748,42 @@ static void fiat_25519_to_bytes(uint8_t out1[32], const uint32_t arg1[10]) {
uint8_t x81 = (uint8_t)(x78 & UINT8_C(0xff));
uint8_t x82 = (uint8_t)(x80 >> 8);
uint8_t x83 = (uint8_t)(x80 & UINT8_C(0xff));
fiat_25519_uint1 x84 = (fiat_25519_uint1)(x82 >> 8);
uint8_t x85 = (uint8_t)(x82 & UINT8_C(0xff));
uint32_t x86 = (x84 + x32);
uint32_t x87 = (x86 >> 8);
uint8_t x88 = (uint8_t)(x86 & UINT8_C(0xff));
uint32_t x89 = (x87 >> 8);
uint8_t x90 = (uint8_t)(x87 & UINT8_C(0xff));
fiat_25519_uint1 x91 = (fiat_25519_uint1)(x89 >> 8);
uint8_t x92 = (uint8_t)(x89 & UINT8_C(0xff));
uint32_t x93 = (x91 + x45);
uint32_t x94 = (x93 >> 8);
uint8_t x95 = (uint8_t)(x93 & UINT8_C(0xff));
uint32_t x96 = (x94 >> 8);
uint8_t x97 = (uint8_t)(x94 & UINT8_C(0xff));
uint8_t x98 = (uint8_t)(x96 >> 8);
uint8_t x99 = (uint8_t)(x96 & UINT8_C(0xff));
uint32_t x100 = (x98 + x44);
uint32_t x101 = (x100 >> 8);
uint8_t x102 = (uint8_t)(x100 & UINT8_C(0xff));
uint32_t x103 = (x101 >> 8);
uint8_t x104 = (uint8_t)(x101 & UINT8_C(0xff));
uint8_t x105 = (uint8_t)(x103 >> 8);
uint8_t x106 = (uint8_t)(x103 & UINT8_C(0xff));
uint32_t x107 = (x105 + x43);
uint32_t x108 = (x107 >> 8);
uint8_t x109 = (uint8_t)(x107 & UINT8_C(0xff));
uint32_t x110 = (x108 >> 8);
uint8_t x111 = (uint8_t)(x108 & UINT8_C(0xff));
uint8_t x112 = (uint8_t)(x110 >> 8);
uint8_t x113 = (uint8_t)(x110 & UINT8_C(0xff));
uint32_t x114 = (x112 + x42);
uint32_t x115 = (x114 >> 8);
uint8_t x116 = (uint8_t)(x114 & UINT8_C(0xff));
uint32_t x117 = (x115 >> 8);
uint8_t x118 = (uint8_t)(x115 & UINT8_C(0xff));
uint8_t x119 = (uint8_t)(x117 >> 8);
uint8_t x120 = (uint8_t)(x117 & UINT8_C(0xff));
uint8_t x84 = (uint8_t)(x82 & UINT8_C(0xff));
uint32_t x85 = (0x0 + x32);
uint32_t x86 = (x85 >> 8);
uint8_t x87 = (uint8_t)(x85 & UINT8_C(0xff));
uint32_t x88 = (x86 >> 8);
uint8_t x89 = (uint8_t)(x86 & UINT8_C(0xff));
fiat_25519_uint1 x90 = (fiat_25519_uint1)(x88 >> 8);
uint8_t x91 = (uint8_t)(x88 & UINT8_C(0xff));
uint32_t x92 = (x90 + x45);
uint32_t x93 = (x92 >> 8);
uint8_t x94 = (uint8_t)(x92 & UINT8_C(0xff));
uint32_t x95 = (x93 >> 8);
uint8_t x96 = (uint8_t)(x93 & UINT8_C(0xff));
uint8_t x97 = (uint8_t)(x95 >> 8);
uint8_t x98 = (uint8_t)(x95 & UINT8_C(0xff));
uint32_t x99 = (x97 + x44);
uint32_t x100 = (x99 >> 8);
uint8_t x101 = (uint8_t)(x99 & UINT8_C(0xff));
uint32_t x102 = (x100 >> 8);
uint8_t x103 = (uint8_t)(x100 & UINT8_C(0xff));
uint8_t x104 = (uint8_t)(x102 >> 8);
uint8_t x105 = (uint8_t)(x102 & UINT8_C(0xff));
uint32_t x106 = (x104 + x43);
uint32_t x107 = (x106 >> 8);
uint8_t x108 = (uint8_t)(x106 & UINT8_C(0xff));
uint32_t x109 = (x107 >> 8);
uint8_t x110 = (uint8_t)(x107 & UINT8_C(0xff));
uint8_t x111 = (uint8_t)(x109 >> 8);
uint8_t x112 = (uint8_t)(x109 & UINT8_C(0xff));
uint32_t x113 = (x111 + x42);
uint32_t x114 = (x113 >> 8);
uint8_t x115 = (uint8_t)(x113 & UINT8_C(0xff));
uint32_t x116 = (x114 >> 8);
uint8_t x117 = (uint8_t)(x114 & UINT8_C(0xff));
uint8_t x118 = (uint8_t)(x116 >> 8);
uint8_t x119 = (uint8_t)(x116 & UINT8_C(0xff));
out1[0] = x51;
out1[1] = x53;
out1[2] = x55;
Expand All @@ -800,23 +799,23 @@ static void fiat_25519_to_bytes(uint8_t out1[32], const uint32_t arg1[10]) {
out1[12] = x79;
out1[13] = x81;
out1[14] = x83;
out1[15] = x85;
out1[16] = x88;
out1[17] = x90;
out1[18] = x92;
out1[19] = x95;
out1[20] = x97;
out1[21] = x99;
out1[22] = x102;
out1[23] = x104;
out1[24] = x106;
out1[25] = x109;
out1[26] = x111;
out1[27] = x113;
out1[28] = x116;
out1[29] = x118;
out1[30] = x120;
out1[31] = x119;
out1[15] = x84;
out1[16] = x87;
out1[17] = x89;
out1[18] = x91;
out1[19] = x94;
out1[20] = x96;
out1[21] = x98;
out1[22] = x101;
out1[23] = x103;
out1[24] = x105;
out1[25] = x108;
out1[26] = x110;
out1[27] = x112;
out1[28] = x115;
out1[29] = x117;
out1[30] = x119;
out1[31] = x118;
}

/*
Expand Down Expand Up @@ -880,30 +879,29 @@ static void fiat_25519_from_bytes(uint32_t out1[10], const uint8_t arg1[32]) {
uint8_t x52 = (uint8_t)(x51 >> 25);
uint32_t x53 = (x51 & UINT32_C(0x1ffffff));
uint32_t x54 = (x52 + x41);
fiat_25519_uint1 x55 = (fiat_25519_uint1)(x54 >> 26);
uint32_t x56 = (x54 & UINT32_C(0x3ffffff));
uint32_t x57 = (x55 + x40);
uint8_t x58 = (uint8_t)(x57 >> 25);
uint32_t x59 = (x57 & UINT32_C(0x1ffffff));
uint32_t x60 = (x58 + x39);
uint8_t x61 = (uint8_t)(x60 >> 26);
uint32_t x62 = (x60 & UINT32_C(0x3ffffff));
uint32_t x63 = (x61 + x38);
uint8_t x64 = (uint8_t)(x63 >> 25);
uint32_t x65 = (x63 & UINT32_C(0x1ffffff));
uint32_t x66 = (x64 + x37);
uint8_t x67 = (uint8_t)(x66 >> 26);
uint32_t x68 = (x66 & UINT32_C(0x3ffffff));
uint32_t x69 = (x67 + x36);
uint32_t x55 = (x54 & UINT32_C(0x3ffffff));
uint32_t x56 = (0x0 + x40);
uint8_t x57 = (uint8_t)(x56 >> 25);
uint32_t x58 = (x56 & UINT32_C(0x1ffffff));
uint32_t x59 = (x57 + x39);
uint8_t x60 = (uint8_t)(x59 >> 26);
uint32_t x61 = (x59 & UINT32_C(0x3ffffff));
uint32_t x62 = (x60 + x38);
uint8_t x63 = (uint8_t)(x62 >> 25);
uint32_t x64 = (x62 & UINT32_C(0x1ffffff));
uint32_t x65 = (x63 + x37);
uint8_t x66 = (uint8_t)(x65 >> 26);
uint32_t x67 = (x65 & UINT32_C(0x3ffffff));
uint32_t x68 = (x66 + x36);
out1[0] = x35;
out1[1] = x47;
out1[2] = x50;
out1[3] = x53;
out1[4] = x56;
out1[5] = x59;
out1[6] = x62;
out1[7] = x65;
out1[8] = x68;
out1[9] = x69;
out1[4] = x55;
out1[5] = x58;
out1[6] = x61;
out1[7] = x64;
out1[8] = x67;
out1[9] = x68;
}

Loading

0 comments on commit efb70cc

Please sign in to comment.