Skip to content
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

Final tweak to the work on unused variables #385

Merged
merged 10 commits into from
Oct 18, 2023
Merged

Final tweak to the work on unused variables #385

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
53bfdfc
hints & dist
msprotz Oct 9, 2023
c4c71d5
More idiomatic treatment of ignored return values and possibly unused…
msprotz Oct 9, 2023
a5c5633
Fix corner case
msprotz Oct 9, 2023
44856e8
Merge branch 'master' into protz_ignore_ifdef
msprotz Oct 9, 2023
e2fee13
Merge branch 'master' into protz_ignore_ifdef
msprotz Oct 11, 2023
d10aebf
Merge remote-tracking branch 'origin/master' into protz_ignore_ifdef
msprotz Oct 13, 2023
a77fb02
Refine criterion for sequencing without using the return value
msprotz Oct 13, 2023
abf1a3b
dist
msprotz Oct 16, 2023
a76ef19
Enable more value eliminations
msprotz Oct 16, 2023
1b9dcc4
Fix pointer dereference which masquerades as a function call but actu…
msprotz Oct 17, 2023
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
4 changes: 4 additions & 0 deletions include/krml/internal/target.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,10 @@
# define KRML_HOST_IGNORE(x) (void)(x)
#endif

#ifndef KRML_MAYBE_UNUSED_VAR
# define KRML_MAYBE_UNUSED_VAR(x) KRML_HOST_IGNORE(x)
#endif

#ifndef KRML_MAYBE_UNUSED
# if defined(__GNUC__)
# define KRML_MAYBE_UNUSED __attribute__((unused))
Expand Down
6 changes: 3 additions & 3 deletions krmllib/dist/generic/FStar_BV.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ Prims_list__bool *FStar_Seq_Base_create__bool(krml_checked_int_t len, bool v)
Prims_list__bool
*FStar_BV_bv_uext(krml_checked_int_t n, krml_checked_int_t i, Prims_list__bool *a)
{
KRML_HOST_IGNORE(n);
KRML_MAYBE_UNUSED_VAR(n);
return FStar_Seq_Base_append__bool(FStar_Seq_Base_create__bool(i, false), a);
}

Expand Down Expand Up @@ -117,7 +117,7 @@ Prims_list__bool *FStar_Seq_Properties_seq_of_list__bool(Prims_list__bool *l)

Prims_list__bool *FStar_BV_list2bv(krml_checked_int_t n, Prims_list__bool *l)
{
KRML_HOST_IGNORE(n);
KRML_MAYBE_UNUSED_VAR(n);
return FStar_Seq_Properties_seq_of_list__bool(l);
}

Expand Down Expand Up @@ -270,7 +270,7 @@ Prims_list__bool *FStar_Seq_Properties_seq_to_list__bool(Prims_list__bool *s)

Prims_list__bool *FStar_BV_bv2list(krml_checked_int_t n, Prims_list__bool *s)
{
KRML_HOST_IGNORE(n);
KRML_MAYBE_UNUSED_VAR(n);
return FStar_Seq_Properties_seq_to_list__bool(s);
}

Expand Down
18 changes: 9 additions & 9 deletions krmllib/dist/generic/FStar_UInt128_Verified.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@

static inline uint64_t FStar_UInt128_constant_time_carry(uint64_t a, uint64_t b)
{
return (a ^ ((a ^ b) | ((a - b) ^ b))) >> (uint32_t)63U;
return (a ^ ((a ^ b) | ((a - b) ^ b))) >> 63U;
}

static inline uint64_t FStar_UInt128_carry(uint64_t a, uint64_t b)
Expand Down Expand Up @@ -118,7 +118,7 @@ static inline FStar_UInt128_uint128 FStar_UInt128_lognot(FStar_UInt128_uint128 a
return lit;
}

static uint32_t FStar_UInt128_u32_64 = (uint32_t)64U;
static uint32_t FStar_UInt128_u32_64 = 64U;

static inline uint64_t FStar_UInt128_add_u64_shift_left(uint64_t hi, uint64_t lo, uint32_t s)
{
Expand All @@ -134,7 +134,7 @@ FStar_UInt128_add_u64_shift_left_respec(uint64_t hi, uint64_t lo, uint32_t s)
static inline FStar_UInt128_uint128
FStar_UInt128_shift_left_small(FStar_UInt128_uint128 a, uint32_t s)
{
if (s == (uint32_t)0U)
if (s == 0U)
{
return a;
}
Expand All @@ -151,7 +151,7 @@ static inline FStar_UInt128_uint128
FStar_UInt128_shift_left_large(FStar_UInt128_uint128 a, uint32_t s)
{
FStar_UInt128_uint128 lit;
lit.low = (uint64_t)0U;
lit.low = 0ULL;
lit.high = a.low << (s - FStar_UInt128_u32_64);
return lit;
}
Expand Down Expand Up @@ -183,7 +183,7 @@ FStar_UInt128_add_u64_shift_right_respec(uint64_t hi, uint64_t lo, uint32_t s)
static inline FStar_UInt128_uint128
FStar_UInt128_shift_right_small(FStar_UInt128_uint128 a, uint32_t s)
{
if (s == (uint32_t)0U)
if (s == 0U)
{
return a;
}
Expand All @@ -201,7 +201,7 @@ FStar_UInt128_shift_right_large(FStar_UInt128_uint128 a, uint32_t s)
{
FStar_UInt128_uint128 lit;
lit.low = a.high >> (s - FStar_UInt128_u32_64);
lit.high = (uint64_t)0U;
lit.high = 0ULL;
return lit;
}

Expand Down Expand Up @@ -269,7 +269,7 @@ static inline FStar_UInt128_uint128 FStar_UInt128_uint64_to_uint128(uint64_t a)
{
FStar_UInt128_uint128 lit;
lit.low = a;
lit.high = (uint64_t)0U;
lit.high = 0ULL;
return lit;
}

Expand All @@ -280,10 +280,10 @@ static inline uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 a)

static inline uint64_t FStar_UInt128_u64_mod_32(uint64_t a)
{
return a & (uint64_t)0xffffffffU;
return a & 0xffffffffULL;
}

static uint32_t FStar_UInt128_u32_32 = (uint32_t)32U;
static uint32_t FStar_UInt128_u32_32 = 32U;

static inline uint64_t FStar_UInt128_u32_combine(uint64_t hi, uint64_t lo)
{
Expand Down
68 changes: 34 additions & 34 deletions krmllib/dist/generic/FStar_UInt_8_16_32_64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,10 +33,10 @@ extern uint32_t FStar_UInt64_n_minus_one;
static KRML_NOINLINE uint64_t FStar_UInt64_eq_mask(uint64_t a, uint64_t b)
{
uint64_t x = a ^ b;
uint64_t minus_x = ~x + (uint64_t)1U;
uint64_t minus_x = ~x + 1ULL;
uint64_t x_or_minus_x = x | minus_x;
uint64_t xnx = x_or_minus_x >> (uint32_t)63U;
return xnx - (uint64_t)1U;
uint64_t xnx = x_or_minus_x >> 63U;
return xnx - 1ULL;
}

static KRML_NOINLINE uint64_t FStar_UInt64_gte_mask(uint64_t a, uint64_t b)
Expand All @@ -48,8 +48,8 @@ static KRML_NOINLINE uint64_t FStar_UInt64_gte_mask(uint64_t a, uint64_t b)
uint64_t x_sub_y_xor_y = x_sub_y ^ y;
uint64_t q = x_xor_y | x_sub_y_xor_y;
uint64_t x_xor_q = x ^ q;
uint64_t x_xor_q_ = x_xor_q >> (uint32_t)63U;
return x_xor_q_ - (uint64_t)1U;
uint64_t x_xor_q_ = x_xor_q >> 63U;
return x_xor_q_ - 1ULL;
}

extern Prims_string FStar_UInt64_to_string(uint64_t uu___);
Expand Down Expand Up @@ -81,10 +81,10 @@ extern uint32_t FStar_UInt32_n_minus_one;
static KRML_NOINLINE uint32_t FStar_UInt32_eq_mask(uint32_t a, uint32_t b)
{
uint32_t x = a ^ b;
uint32_t minus_x = ~x + (uint32_t)1U;
uint32_t minus_x = ~x + 1U;
uint32_t x_or_minus_x = x | minus_x;
uint32_t xnx = x_or_minus_x >> (uint32_t)31U;
return xnx - (uint32_t)1U;
uint32_t xnx = x_or_minus_x >> 31U;
return xnx - 1U;
}

static KRML_NOINLINE uint32_t FStar_UInt32_gte_mask(uint32_t a, uint32_t b)
Expand All @@ -96,8 +96,8 @@ static KRML_NOINLINE uint32_t FStar_UInt32_gte_mask(uint32_t a, uint32_t b)
uint32_t x_sub_y_xor_y = x_sub_y ^ y;
uint32_t q = x_xor_y | x_sub_y_xor_y;
uint32_t x_xor_q = x ^ q;
uint32_t x_xor_q_ = x_xor_q >> (uint32_t)31U;
return x_xor_q_ - (uint32_t)1U;
uint32_t x_xor_q_ = x_xor_q >> 31U;
return x_xor_q_ - 1U;
}

extern Prims_string FStar_UInt32_to_string(uint32_t uu___);
Expand Down Expand Up @@ -128,24 +128,24 @@ extern uint32_t FStar_UInt16_n_minus_one;

static KRML_NOINLINE uint16_t FStar_UInt16_eq_mask(uint16_t a, uint16_t b)
{
uint16_t x = a ^ b;
uint16_t minus_x = ~x + (uint16_t)1U;
uint16_t x_or_minus_x = x | minus_x;
uint16_t xnx = x_or_minus_x >> (uint32_t)15U;
return xnx - (uint16_t)1U;
uint16_t x = (uint32_t)a ^ (uint32_t)b;
uint16_t minus_x = (uint32_t)~x + 1U;
uint16_t x_or_minus_x = (uint32_t)x | (uint32_t)minus_x;
uint16_t xnx = (uint32_t)x_or_minus_x >> 15U;
return (uint32_t)xnx - 1U;
}

static KRML_NOINLINE uint16_t FStar_UInt16_gte_mask(uint16_t a, uint16_t b)
{
uint16_t x = a;
uint16_t y = b;
uint16_t x_xor_y = x ^ y;
uint16_t x_sub_y = x - y;
uint16_t x_sub_y_xor_y = x_sub_y ^ y;
uint16_t q = x_xor_y | x_sub_y_xor_y;
uint16_t x_xor_q = x ^ q;
uint16_t x_xor_q_ = x_xor_q >> (uint32_t)15U;
return x_xor_q_ - (uint16_t)1U;
uint16_t x_xor_y = (uint32_t)x ^ (uint32_t)y;
uint16_t x_sub_y = (uint32_t)x - (uint32_t)y;
uint16_t x_sub_y_xor_y = (uint32_t)x_sub_y ^ (uint32_t)y;
uint16_t q = (uint32_t)x_xor_y | (uint32_t)x_sub_y_xor_y;
uint16_t x_xor_q = (uint32_t)x ^ (uint32_t)q;
uint16_t x_xor_q_ = (uint32_t)x_xor_q >> 15U;
return (uint32_t)x_xor_q_ - 1U;
}

extern Prims_string FStar_UInt16_to_string(uint16_t uu___);
Expand Down Expand Up @@ -176,24 +176,24 @@ extern uint32_t FStar_UInt8_n_minus_one;

static KRML_NOINLINE uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b)
{
uint8_t x = a ^ b;
uint8_t minus_x = ~x + (uint8_t)1U;
uint8_t x_or_minus_x = x | minus_x;
uint8_t xnx = x_or_minus_x >> (uint32_t)7U;
return xnx - (uint8_t)1U;
uint8_t x = (uint32_t)a ^ (uint32_t)b;
uint8_t minus_x = (uint32_t)~x + 1U;
uint8_t x_or_minus_x = (uint32_t)x | (uint32_t)minus_x;
uint8_t xnx = (uint32_t)x_or_minus_x >> 7U;
return (uint32_t)xnx - 1U;
}

static KRML_NOINLINE uint8_t FStar_UInt8_gte_mask(uint8_t a, uint8_t b)
{
uint8_t x = a;
uint8_t y = b;
uint8_t x_xor_y = x ^ y;
uint8_t x_sub_y = x - y;
uint8_t x_sub_y_xor_y = x_sub_y ^ y;
uint8_t q = x_xor_y | x_sub_y_xor_y;
uint8_t x_xor_q = x ^ q;
uint8_t x_xor_q_ = x_xor_q >> (uint32_t)7U;
return x_xor_q_ - (uint8_t)1U;
uint8_t x_xor_y = (uint32_t)x ^ (uint32_t)y;
uint8_t x_sub_y = (uint32_t)x - (uint32_t)y;
uint8_t x_sub_y_xor_y = (uint32_t)x_sub_y ^ (uint32_t)y;
uint8_t q = (uint32_t)x_xor_y | (uint32_t)x_sub_y_xor_y;
uint8_t x_xor_q = (uint32_t)x ^ (uint32_t)q;
uint8_t x_xor_q_ = (uint32_t)x_xor_q >> 7U;
return (uint32_t)x_xor_q_ - 1U;
}

extern Prims_string FStar_UInt8_to_string(uint8_t uu___);
Expand Down
23 changes: 11 additions & 12 deletions krmllib/dist/generic/WasmSupport.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,9 @@

uint32_t WasmSupport_align_64(uint32_t x)
{
if (!((x & (uint32_t)0x07U) == (uint32_t)0U))
if (!((x & 0x07U) == 0U))
{
return (x & (uint32_t)4294967288U) + (uint32_t)0x08U;
return (x & 4294967288U) + 0x08U;
}
else
{
Expand All @@ -20,42 +20,41 @@ uint32_t WasmSupport_align_64(uint32_t x)

void WasmSupport_check_buffer_size(uint32_t s)
{
if (s == (uint32_t)0U)
if (s == 0U)
{
WasmSupport_trap("Zero-sized arrays are not supported in C and in WASM either. See WasmSupport.fst");
}
}

uint16_t WasmSupport_betole16(uint16_t x)
{
return (x >> (uint32_t)8U & (uint16_t)0x00FFU) | (x << (uint32_t)8U & (uint16_t)0xFF00U);
return ((uint32_t)x >> 8U & 0x00FFU) | ((uint32_t)x << 8U & 0xFF00U);
}

uint32_t WasmSupport_betole32(uint32_t x)
{
return
(((x >> (uint32_t)24U & (uint32_t)0x000000FFU) | (x >> (uint32_t)8U & (uint32_t)0x0000FF00U))
| (x << (uint32_t)8U & (uint32_t)0x00FF0000U))
| (x << (uint32_t)24U & (uint32_t)0xFF000000U);
(((x >> 24U & 0x000000FFU) | (x >> 8U & 0x0000FF00U)) | (x << 8U & 0x00FF0000U))
| (x << 24U & 0xFF000000U);
}

uint64_t WasmSupport_betole64(uint64_t x)
{
uint64_t low = (uint64_t)WasmSupport_betole32((uint32_t)x);
uint64_t high = (uint64_t)WasmSupport_betole32((uint32_t)(x >> (uint32_t)32U));
return low << (uint32_t)32U | high;
uint64_t high = (uint64_t)WasmSupport_betole32((uint32_t)(x >> 32U));
return low << 32U | high;
}

void WasmSupport_memzero(uint8_t *x, uint32_t len, uint32_t sz)
{
if (len >= (uint32_t)0xffffffffU / sz)
if (len >= 0xffffffffU / sz)
{
WasmSupport_trap("Overflow in memzero; see WasmSupport.fst");
}
uint32_t n_bytes = len * sz;
for (uint32_t i = (uint32_t)0U; i < n_bytes; i++)
for (uint32_t i = 0U; i < n_bytes; i++)
{
x[i] = (uint8_t)0U;
x[i] = 0U;
}
}

18 changes: 9 additions & 9 deletions krmllib/dist/minimal/FStar_UInt128_Verified.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@

static inline uint64_t FStar_UInt128_constant_time_carry(uint64_t a, uint64_t b)
{
return (a ^ ((a ^ b) | ((a - b) ^ b))) >> (uint32_t)63U;
return (a ^ ((a ^ b) | ((a - b) ^ b))) >> 63U;
}

static inline uint64_t FStar_UInt128_carry(uint64_t a, uint64_t b)
Expand Down Expand Up @@ -118,7 +118,7 @@ static inline FStar_UInt128_uint128 FStar_UInt128_lognot(FStar_UInt128_uint128 a
return lit;
}

static uint32_t FStar_UInt128_u32_64 = (uint32_t)64U;
static uint32_t FStar_UInt128_u32_64 = 64U;

static inline uint64_t FStar_UInt128_add_u64_shift_left(uint64_t hi, uint64_t lo, uint32_t s)
{
Expand All @@ -134,7 +134,7 @@ FStar_UInt128_add_u64_shift_left_respec(uint64_t hi, uint64_t lo, uint32_t s)
static inline FStar_UInt128_uint128
FStar_UInt128_shift_left_small(FStar_UInt128_uint128 a, uint32_t s)
{
if (s == (uint32_t)0U)
if (s == 0U)
{
return a;
}
Expand All @@ -151,7 +151,7 @@ static inline FStar_UInt128_uint128
FStar_UInt128_shift_left_large(FStar_UInt128_uint128 a, uint32_t s)
{
FStar_UInt128_uint128 lit;
lit.low = (uint64_t)0U;
lit.low = 0ULL;
lit.high = a.low << (s - FStar_UInt128_u32_64);
return lit;
}
Expand Down Expand Up @@ -183,7 +183,7 @@ FStar_UInt128_add_u64_shift_right_respec(uint64_t hi, uint64_t lo, uint32_t s)
static inline FStar_UInt128_uint128
FStar_UInt128_shift_right_small(FStar_UInt128_uint128 a, uint32_t s)
{
if (s == (uint32_t)0U)
if (s == 0U)
{
return a;
}
Expand All @@ -201,7 +201,7 @@ FStar_UInt128_shift_right_large(FStar_UInt128_uint128 a, uint32_t s)
{
FStar_UInt128_uint128 lit;
lit.low = a.high >> (s - FStar_UInt128_u32_64);
lit.high = (uint64_t)0U;
lit.high = 0ULL;
return lit;
}

Expand Down Expand Up @@ -269,7 +269,7 @@ static inline FStar_UInt128_uint128 FStar_UInt128_uint64_to_uint128(uint64_t a)
{
FStar_UInt128_uint128 lit;
lit.low = a;
lit.high = (uint64_t)0U;
lit.high = 0ULL;
return lit;
}

Expand All @@ -280,10 +280,10 @@ static inline uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 a)

static inline uint64_t FStar_UInt128_u64_mod_32(uint64_t a)
{
return a & (uint64_t)0xffffffffU;
return a & 0xffffffffULL;
}

static uint32_t FStar_UInt128_u32_32 = (uint32_t)32U;
static uint32_t FStar_UInt128_u32_32 = 32U;

static inline uint64_t FStar_UInt128_u32_combine(uint64_t hi, uint64_t lo)
{
Expand Down
Loading