$ make
-
-
Save samoht/7c27b6418148ee04590e571f390f1997 to your computer and use it in GitHub Desktop.
mirage-crypto-ec repro
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#define LIMBS 4 | |
#define WORD uint64_t | |
#define WORDSIZE 64 | |
#define LEN_PRIME 256 | |
#define CURVE_DESCRIPTION fiat_p256 | |
#include "p256_64.h" | |
int printf(const char *, ...); | |
static __inline__ void _fiat_p256_addcarryx_u64(uint64_t* out1, fiat_p256_uint1* out2, fiat_p256_uint1 arg1, uint64_t arg2, uint64_t arg3) { | |
fiat_p256_uint128 x1; | |
uint64_t x2; | |
fiat_p256_uint1 x3; | |
x1 = ((arg1 + (fiat_p256_uint128)arg2) + arg3); | |
x2 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff)); | |
x3 = (fiat_p256_uint1)(x1 >> 64); | |
*out1 = x2; | |
*out2 = x3; | |
} | |
static __inline__ void _fiat_p256_divstep(uint64_t* out1, uint64_t out2[5], uint64_t out3[5], uint64_t out4[4], uint64_t out5[4], uint64_t arg1, const uint64_t arg2[5], const uint64_t arg3[5], const uint64_t arg4[4], const uint64_t arg5[4]) { | |
printf ("---\n"); | |
} | |
int main (void) { | |
uint64_t g[5]; | |
WORD d, out1; | |
WORD f[5]; | |
WORD v[4]; | |
WORD r[4]; | |
WORD out2[5], out3[5], out4[4], out5[4]; | |
d=UINT64_C(1); | |
f[0]=UINT64_C(18446744073709551615); | |
f[1]=UINT64_C(4294967295); | |
f[2]=UINT64_C(0); | |
f[3]=UINT64_C(18446744069414584321); | |
f[4]=UINT64_C(0); | |
g[0]=UINT64_C(3164219169453123020); | |
g[1]=UINT64_C(5610335456920920796); | |
g[2]=UINT64_C(4531946527682827593); | |
g[3]=UINT64_C(17678136164097313971); | |
g[4]=UINT64_C(0); | |
v[0]=UINT64_C(0); | |
v[1]=UINT64_C(0); | |
v[2]=UINT64_C(0); | |
v[3]=UINT64_C(0); | |
r[0]=UINT64_C(1); | |
r[1]=UINT64_C(18446744069414584320); | |
r[2]=UINT64_C(18446744073709551615); | |
r[3]=UINT64_C(4294967294); | |
out1=0; | |
out2[0]=0; | |
out2[1]=0; | |
out2[2]=0; | |
out2[3]=0; | |
out2[4]=0; | |
out3[0]=0; | |
out3[1]=0; | |
out3[2]=0; | |
out3[3]=0; | |
out3[4]=0; | |
out4[0]=0; | |
out4[1]=0; | |
out4[2]=0; | |
out4[3]=0; | |
out5[0]=0; | |
out5[1]=0; | |
out5[2]=0; | |
out5[3]=0; | |
fiat_p256_divstep(&out1,out2,out3,out4,out5,d,f,g,v,r); | |
fiat_p256_divstep(&d,f,g,v,r,out1,out2,out3,out4,out5); | |
// f[2] = UINT64_C(0); // CHANGE FAIL TO PASS | |
// fiat_p256_divstep(&out1,out2,out3,out4,out5,d,f,g,v,r); | |
uint64_t x12; | |
fiat_p256_uint1 x13; | |
uint64_t x14; | |
fiat_p256_uint1 x15; | |
uint64_t x16; | |
fiat_p256_uint1 x17; | |
uint64_t x18; | |
fiat_p256_uint1 x19; | |
fiat_p256_uint128 _x1; | |
uint64_t _x2; | |
fiat_p256_uint1 _x3; | |
fiat_p256_addcarryx_u64(&x12, &x13, 0x0, 0x1, (~(f[0]))); | |
fiat_p256_addcarryx_u64(&x14, &x15, x13, 0x0, (~(f[1]))); | |
fiat_p256_addcarryx_u64(&x16, &x17, x15, 0x0, (~(f[2]))); | |
fiat_p256_addcarryx_u64(&x18, &x19, x17, 0x0, (~(f[3]))); | |
// fiat_p256_addcarryx_u64(&x20, &x21, x19, 0x0, (~(f[4]))); | |
_x1 = ((x19 + (fiat_p256_uint128)0x0) + (~(f[4]))); | |
_x2 = (uint64_t)(_x1 & UINT64_C(0xffffffffffffffff)); | |
if (_x2 != UINT64_C(18446744073709551615)) { | |
printf("FAIL\n"); | |
return 1; | |
} | |
printf("PASS\n"); | |
return 0; | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
CLANG_OK=/opt/homebrew/Cellar/llvm/16.0.4/bin/clang | |
CLANG=/usr/bin/clang | |
all: repro-ok.exe repro-ko.exe repro-ok.s repro-ko.s | |
./repro-ok.exe | |
./repro-ko.exe | |
repro-ok.exe: *.c *.h | |
# clang -fsanitize=undefined,address main.c -o repro-ok.exe -O1 | |
# clang main.c -o repro-ok.exe -O0 | |
# $(CLANG) main.c -O1 -o repro-ok.exe -mllvm --instcombine-max-iterations=0 | |
$(CLANG_OK) main.c -O1 -o repro-ok.exe \ | |
-mllvm --instcombine-max-iterations=1 \ | |
-mllvm --instcombine-max-num-phis=0 \ | |
-mllvm --instcombine-max-sink-users=0 \ | |
-mllvm --instcombine-maxarray-size=0 \ | |
-mllvm --instcombine-negator-max-depth=0 | |
repro-ko.exe: *.c *.h | |
$(CLANG) main.c -O1 -o repro-ko.exe \ | |
-mllvm --instcombine-max-iterations=1 \ | |
-mllvm --instcombine-max-num-phis=0 \ | |
-mllvm --instcombine-max-sink-users=0 \ | |
-mllvm --instcombine-maxarray-size=0 \ | |
-mllvm --instcombine-negator-max-depth=0 | |
bissect: | |
$(CLANG) main.c -O1 -o repro.exe -mllvm -opt-bisect-limit=180 && ./repro.exe | |
repro-ok.s: repro-ok.exe | |
objdump -M intel -d repro-ok.exe > repro-ok.s | |
repro-ko.s: repro-ko.exe | |
objdump -M intel -d repro-ko.exe > repro-ko.s |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include <stdint.h> | |
typedef unsigned char fiat_p256_uint1; | |
typedef signed char fiat_p256_int1; | |
#if defined(__GNUC__) || defined(__clang__) | |
# define FIAT_P256_FIAT_EXTENSION __extension__ | |
# define FIAT_P256_FIAT_INLINE __inline__ | |
#else | |
# define FIAT_P256_FIAT_EXTENSION | |
# define FIAT_P256_FIAT_INLINE | |
#endif | |
FIAT_P256_FIAT_EXTENSION typedef signed __int128 fiat_p256_int128; | |
FIAT_P256_FIAT_EXTENSION typedef unsigned __int128 fiat_p256_uint128; | |
typedef uint64_t fiat_p256_montgomery_domain_field_element[4]; | |
typedef uint64_t fiat_p256_non_montgomery_domain_field_element[4]; | |
#if (-1 & 3) != 3 | |
#error "This code only works on a two's complement system" | |
#endif | |
#if !defined(FIAT_P256_NO_ASM) && (defined(__GNUC__) || defined(__clang__)) | |
static __inline__ uint64_t fiat_p256_value_barrier_u64(uint64_t a) { | |
__asm__("" : "+r"(a) : /* no inputs */); | |
return a; | |
} | |
#else | |
# define fiat_p256_value_barrier_u64(x) (x) | |
#endif | |
static FIAT_P256_FIAT_INLINE void fiat_p256_addcarryx_u64(uint64_t* out1, fiat_p256_uint1* out2, fiat_p256_uint1 arg1, uint64_t arg2, uint64_t arg3) { | |
fiat_p256_uint128 x1; | |
uint64_t x2; | |
fiat_p256_uint1 x3; | |
x1 = ((arg1 + (fiat_p256_uint128)arg2) + arg3); | |
x2 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff)); | |
x3 = (fiat_p256_uint1)(x1 >> 64); | |
*out1 = x2; | |
*out2 = x3; | |
} | |
static FIAT_P256_FIAT_INLINE void fiat_p256_subborrowx_u64(uint64_t* out1, fiat_p256_uint1* out2, fiat_p256_uint1 arg1, uint64_t arg2, uint64_t arg3) { | |
fiat_p256_int128 x1; | |
fiat_p256_int1 x2; | |
uint64_t x3; | |
x1 = ((arg2 - (fiat_p256_int128)arg1) - arg3); | |
x2 = (fiat_p256_int1)(x1 >> 64); | |
x3 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff)); | |
*out1 = x3; | |
*out2 = (fiat_p256_uint1)(0x0 - x2); | |
} | |
static FIAT_P256_FIAT_INLINE void fiat_p256_cmovznz_u64(uint64_t* out1, fiat_p256_uint1 arg1, uint64_t arg2, uint64_t arg3) { | |
fiat_p256_uint1 x1; | |
uint64_t x2; | |
uint64_t x3; | |
x1 = (!(!arg1)); | |
x2 = ((fiat_p256_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff)); | |
x3 = ((fiat_p256_value_barrier_u64(x2) & arg3) | (fiat_p256_value_barrier_u64((~x2)) & arg2)); | |
*out1 = x3; | |
} | |
static FIAT_P256_FIAT_INLINE void fiat_p256_divstep(uint64_t* out1, uint64_t out2[5], uint64_t out3[5], uint64_t out4[4], uint64_t out5[4], uint64_t arg1, const uint64_t arg2[5], const uint64_t arg3[5], const uint64_t arg4[4], const uint64_t arg5[4]) { | |
uint64_t x1; | |
fiat_p256_uint1 x2; | |
fiat_p256_uint1 x3; | |
uint64_t x4; | |
fiat_p256_uint1 x5; | |
uint64_t x6; | |
uint64_t x7; | |
uint64_t x8; | |
uint64_t x9; | |
uint64_t x10; | |
uint64_t x11; | |
uint64_t x12; | |
fiat_p256_uint1 x13; | |
uint64_t x14; | |
fiat_p256_uint1 x15; | |
uint64_t x16; | |
fiat_p256_uint1 x17; | |
uint64_t x18; | |
fiat_p256_uint1 x19; | |
uint64_t x20; | |
fiat_p256_uint1 x21; | |
uint64_t x22; | |
uint64_t x23; | |
uint64_t x24; | |
uint64_t x25; | |
uint64_t x26; | |
uint64_t x27; | |
uint64_t x28; | |
uint64_t x29; | |
uint64_t x30; | |
uint64_t x31; | |
fiat_p256_uint1 x32; | |
uint64_t x33; | |
fiat_p256_uint1 x34; | |
uint64_t x35; | |
fiat_p256_uint1 x36; | |
uint64_t x37; | |
fiat_p256_uint1 x38; | |
uint64_t x39; | |
fiat_p256_uint1 x40; | |
uint64_t x41; | |
fiat_p256_uint1 x42; | |
uint64_t x43; | |
fiat_p256_uint1 x44; | |
uint64_t x45; | |
fiat_p256_uint1 x46; | |
uint64_t x47; | |
fiat_p256_uint1 x48; | |
uint64_t x49; | |
uint64_t x50; | |
uint64_t x51; | |
uint64_t x52; | |
uint64_t x53; | |
fiat_p256_uint1 x54; | |
uint64_t x55; | |
fiat_p256_uint1 x56; | |
uint64_t x57; | |
fiat_p256_uint1 x58; | |
uint64_t x59; | |
fiat_p256_uint1 x60; | |
uint64_t x61; | |
uint64_t x62; | |
fiat_p256_uint1 x63; | |
uint64_t x64; | |
fiat_p256_uint1 x65; | |
uint64_t x66; | |
fiat_p256_uint1 x67; | |
uint64_t x68; | |
fiat_p256_uint1 x69; | |
uint64_t x70; | |
uint64_t x71; | |
uint64_t x72; | |
uint64_t x73; | |
fiat_p256_uint1 x74; | |
uint64_t x75; | |
uint64_t x76; | |
uint64_t x77; | |
uint64_t x78; | |
uint64_t x79; | |
uint64_t x80; | |
fiat_p256_uint1 x81; | |
uint64_t x82; | |
fiat_p256_uint1 x83; | |
uint64_t x84; | |
fiat_p256_uint1 x85; | |
uint64_t x86; | |
fiat_p256_uint1 x87; | |
uint64_t x88; | |
fiat_p256_uint1 x89; | |
uint64_t x90; | |
uint64_t x91; | |
uint64_t x92; | |
uint64_t x93; | |
uint64_t x94; | |
fiat_p256_uint1 x95; | |
uint64_t x96; | |
fiat_p256_uint1 x97; | |
uint64_t x98; | |
fiat_p256_uint1 x99; | |
uint64_t x100; | |
fiat_p256_uint1 x101; | |
uint64_t x102; | |
fiat_p256_uint1 x103; | |
uint64_t x104; | |
fiat_p256_uint1 x105; | |
uint64_t x106; | |
fiat_p256_uint1 x107; | |
uint64_t x108; | |
fiat_p256_uint1 x109; | |
uint64_t x110; | |
fiat_p256_uint1 x111; | |
uint64_t x112; | |
fiat_p256_uint1 x113; | |
uint64_t x114; | |
uint64_t x115; | |
uint64_t x116; | |
uint64_t x117; | |
uint64_t x118; | |
uint64_t x119; | |
uint64_t x120; | |
uint64_t x121; | |
uint64_t x122; | |
uint64_t x123; | |
uint64_t x124; | |
uint64_t x125; | |
uint64_t x126; | |
fiat_p256_addcarryx_u64(&x1, &x2, 0x0, (~arg1), 0x1); | |
x3 = (fiat_p256_uint1)((fiat_p256_uint1)(x1 >> 63) & (fiat_p256_uint1)((arg3[0]) & 0x1)); | |
fiat_p256_addcarryx_u64(&x4, &x5, 0x0, (~arg1), 0x1); | |
fiat_p256_cmovznz_u64(&x6, x3, arg1, x4); | |
fiat_p256_cmovznz_u64(&x7, x3, (arg2[0]), (arg3[0])); | |
fiat_p256_cmovznz_u64(&x8, x3, (arg2[1]), (arg3[1])); | |
fiat_p256_cmovznz_u64(&x9, x3, (arg2[2]), (arg3[2])); | |
fiat_p256_cmovznz_u64(&x10, x3, (arg2[3]), (arg3[3])); | |
fiat_p256_cmovznz_u64(&x11, x3, (arg2[4]), (arg3[4])); | |
fiat_p256_addcarryx_u64(&x12, &x13, 0x0, 0x1, (~(arg2[0]))); | |
fiat_p256_addcarryx_u64(&x14, &x15, x13, 0x0, (~(arg2[1]))); | |
fiat_p256_addcarryx_u64(&x16, &x17, x15, 0x0, (~(arg2[2]))); | |
fiat_p256_addcarryx_u64(&x18, &x19, x17, 0x0, (~(arg2[3]))); | |
fiat_p256_addcarryx_u64(&x20, &x21, x19, 0x0, (~(arg2[4]))); | |
fiat_p256_cmovznz_u64(&x22, x3, (arg3[0]), x12); | |
fiat_p256_cmovznz_u64(&x23, x3, (arg3[1]), x14); | |
fiat_p256_cmovznz_u64(&x24, x3, (arg3[2]), x16); | |
fiat_p256_cmovznz_u64(&x25, x3, (arg3[3]), x18); | |
fiat_p256_cmovznz_u64(&x26, x3, (arg3[4]), x20); | |
fiat_p256_cmovznz_u64(&x27, x3, (arg4[0]), (arg5[0])); | |
fiat_p256_cmovznz_u64(&x28, x3, (arg4[1]), (arg5[1])); | |
fiat_p256_cmovznz_u64(&x29, x3, (arg4[2]), (arg5[2])); | |
fiat_p256_cmovznz_u64(&x30, x3, (arg4[3]), (arg5[3])); | |
fiat_p256_addcarryx_u64(&x31, &x32, 0x0, x27, x27); | |
fiat_p256_addcarryx_u64(&x33, &x34, x32, x28, x28); | |
fiat_p256_addcarryx_u64(&x35, &x36, x34, x29, x29); | |
fiat_p256_addcarryx_u64(&x37, &x38, x36, x30, x30); | |
fiat_p256_subborrowx_u64(&x39, &x40, 0x0, x31, UINT64_C(0xffffffffffffffff)); | |
fiat_p256_subborrowx_u64(&x41, &x42, x40, x33, UINT32_C(0xffffffff)); | |
fiat_p256_subborrowx_u64(&x43, &x44, x42, x35, 0x0); | |
fiat_p256_subborrowx_u64(&x45, &x46, x44, x37, UINT64_C(0xffffffff00000001)); | |
fiat_p256_subborrowx_u64(&x47, &x48, x46, x38, 0x0); | |
x49 = (arg4[3]); | |
x50 = (arg4[2]); | |
x51 = (arg4[1]); | |
x52 = (arg4[0]); | |
fiat_p256_subborrowx_u64(&x53, &x54, 0x0, 0x0, x52); | |
fiat_p256_subborrowx_u64(&x55, &x56, x54, 0x0, x51); | |
fiat_p256_subborrowx_u64(&x57, &x58, x56, 0x0, x50); | |
fiat_p256_subborrowx_u64(&x59, &x60, x58, 0x0, x49); | |
fiat_p256_cmovznz_u64(&x61, x60, 0x0, UINT64_C(0xffffffffffffffff)); | |
fiat_p256_addcarryx_u64(&x62, &x63, 0x0, x53, x61); | |
fiat_p256_addcarryx_u64(&x64, &x65, x63, x55, (x61 & UINT32_C(0xffffffff))); | |
fiat_p256_addcarryx_u64(&x66, &x67, x65, x57, 0x0); | |
fiat_p256_addcarryx_u64(&x68, &x69, x67, x59, (x61 & UINT64_C(0xffffffff00000001))); | |
fiat_p256_cmovznz_u64(&x70, x3, (arg5[0]), x62); | |
fiat_p256_cmovznz_u64(&x71, x3, (arg5[1]), x64); | |
fiat_p256_cmovznz_u64(&x72, x3, (arg5[2]), x66); | |
fiat_p256_cmovznz_u64(&x73, x3, (arg5[3]), x68); | |
x74 = (fiat_p256_uint1)(x22 & 0x1); | |
fiat_p256_cmovznz_u64(&x75, x74, 0x0, x7); | |
fiat_p256_cmovznz_u64(&x76, x74, 0x0, x8); | |
fiat_p256_cmovznz_u64(&x77, x74, 0x0, x9); | |
fiat_p256_cmovznz_u64(&x78, x74, 0x0, x10); | |
fiat_p256_cmovznz_u64(&x79, x74, 0x0, x11); | |
fiat_p256_addcarryx_u64(&x80, &x81, 0x0, x22, x75); | |
fiat_p256_addcarryx_u64(&x82, &x83, x81, x23, x76); | |
fiat_p256_addcarryx_u64(&x84, &x85, x83, x24, x77); | |
fiat_p256_addcarryx_u64(&x86, &x87, x85, x25, x78); | |
fiat_p256_addcarryx_u64(&x88, &x89, x87, x26, x79); | |
fiat_p256_cmovznz_u64(&x90, x74, 0x0, x27); | |
fiat_p256_cmovznz_u64(&x91, x74, 0x0, x28); | |
fiat_p256_cmovznz_u64(&x92, x74, 0x0, x29); | |
fiat_p256_cmovznz_u64(&x93, x74, 0x0, x30); | |
fiat_p256_addcarryx_u64(&x94, &x95, 0x0, x70, x90); | |
fiat_p256_addcarryx_u64(&x96, &x97, x95, x71, x91); | |
fiat_p256_addcarryx_u64(&x98, &x99, x97, x72, x92); | |
fiat_p256_addcarryx_u64(&x100, &x101, x99, x73, x93); | |
fiat_p256_subborrowx_u64(&x102, &x103, 0x0, x94, UINT64_C(0xffffffffffffffff)); | |
fiat_p256_subborrowx_u64(&x104, &x105, x103, x96, UINT32_C(0xffffffff)); | |
fiat_p256_subborrowx_u64(&x106, &x107, x105, x98, 0x0); | |
fiat_p256_subborrowx_u64(&x108, &x109, x107, x100, UINT64_C(0xffffffff00000001)); | |
fiat_p256_subborrowx_u64(&x110, &x111, x109, x101, 0x0); | |
fiat_p256_addcarryx_u64(&x112, &x113, 0x0, x6, 0x1); | |
x114 = ((x80 >> 1) | ((x82 << 63) & UINT64_C(0xffffffffffffffff))); | |
x115 = ((x82 >> 1) | ((x84 << 63) & UINT64_C(0xffffffffffffffff))); | |
x116 = ((x84 >> 1) | ((x86 << 63) & UINT64_C(0xffffffffffffffff))); | |
x117 = ((x86 >> 1) | ((x88 << 63) & UINT64_C(0xffffffffffffffff))); | |
x118 = ((x88 & UINT64_C(0x8000000000000000)) | (x88 >> 1)); | |
fiat_p256_cmovznz_u64(&x119, x48, x39, x31); | |
fiat_p256_cmovznz_u64(&x120, x48, x41, x33); | |
fiat_p256_cmovznz_u64(&x121, x48, x43, x35); | |
fiat_p256_cmovznz_u64(&x122, x48, x45, x37); | |
fiat_p256_cmovznz_u64(&x123, x111, x102, x94); | |
fiat_p256_cmovznz_u64(&x124, x111, x104, x96); | |
fiat_p256_cmovznz_u64(&x125, x111, x106, x98); | |
fiat_p256_cmovznz_u64(&x126, x111, x108, x100); | |
*out1 = x112; | |
out2[0] = x7; | |
out2[1] = x8; | |
out2[2] = x9; | |
out2[3] = x10; | |
out2[4] = x11; | |
out3[0] = x114; | |
out3[1] = x115; | |
out3[2] = x116; | |
out3[3] = x117; | |
out3[4] = x118; | |
out4[0] = x119; | |
out4[1] = x120; | |
out4[2] = x121; | |
out4[3] = x122; | |
out5[0] = x123; | |
out5[1] = x124; | |
out5[2] = x125; | |
out5[3] = x126; | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment