Skip to content

Commit 85d35d1

Browse files
hanno-beckerhanno-becker
committed
Debug: Reduce number of macros, assimilate to CBMC assertions
Previously, debug.h provided a host of bounds checking assertions, such as POLY_BOUND, POLY_UBOUND, POLY_BOUND_MSG, POLYVEC_BOUND, ... This commit simplifies debug.h by reducing to three assertions - debug_assert: For any boolean valued assertion - debug_assert_bound: For a lower+upper bounds assertion on an array, akin to the CBMC assertion array_bound - debug_assert_abs_bound: For an absolute bounds assertion on an array, akin to the CBMC assertion array_abs_bound. Moreover, assertion strings are removed: The filename and linenumber already provide enough information to locate the issue when an assertion fails -- the additional test clutters the code and doesn't add much. While adjusting the code, two smaller issues were noted and fixed: - The debug assertions had gone out of sync with the CBMC specs for the basemul functions: The CBMC spec would assert that the a-input is coefficient-wise in [0..4095], while the debug assertions would assert an absolute bound. This is unified by using bound by [0..4095] as proved correct by CBMC. - In `poly_basemul_montgomery_cached`, a debug assertion was placed on the mulcache what should have been placed on the a-input. This is fixed. - The documentation of `poly_basemul_montgomery_cached` had gone out of sync with the CBMC assertions: The documentation still stated the older output bound by 3/2q, while the CBMC assertions showed only 2q. This change stemmed from the recent relaxation of input bounds from MLKEM_Q -> 4096. Also, there was no debug-assertion for the post-condition, which is added. Signed-off-by: Hanno Becker <[email protected]>
1 parent 32f9876 commit 85d35d1

File tree

12 files changed

+111
-294
lines changed

12 files changed

+111
-294
lines changed

‎examples/monolithic_build/mlkem_native_monobuild.c

+12-87
Original file line numberDiff line numberDiff line change
@@ -358,114 +358,39 @@
358358
#undef empty_cu_debug
359359
#endif
360360

361-
/* mlkem/debug/debug.h */
362-
#if defined(BOUND)
363-
#undef BOUND
364-
#endif
365-
366-
/* mlkem/debug/debug.h */
367-
#if defined(BOUND)
368-
#undef BOUND
369-
#endif
370-
371-
/* mlkem/debug/debug.h */
372-
#if defined(CASSERT)
373-
#undef CASSERT
374-
#endif
375-
376-
/* mlkem/debug/debug.h */
377-
#if defined(CASSERT)
378-
#undef CASSERT
379-
#endif
380-
381361
/* mlkem/debug/debug.h */
382362
#if defined(MLKEM_DEBUG_H)
383363
#undef MLKEM_DEBUG_H
384364
#endif
385365

386366
/* mlkem/debug/debug.h */
387-
#if defined(POLYVEC_BOUND)
388-
#undef POLYVEC_BOUND
389-
#endif
390-
391-
/* mlkem/debug/debug.h */
392-
#if defined(POLYVEC_BOUND)
393-
#undef POLYVEC_BOUND
394-
#endif
395-
396-
/* mlkem/debug/debug.h */
397-
#if defined(POLYVEC_UBOUND)
398-
#undef POLYVEC_UBOUND
399-
#endif
400-
401-
/* mlkem/debug/debug.h */
402-
#if defined(POLYVEC_UBOUND)
403-
#undef POLYVEC_UBOUND
404-
#endif
405-
406-
/* mlkem/debug/debug.h */
407-
#if defined(POLY_BOUND)
408-
#undef POLY_BOUND
409-
#endif
410-
411-
/* mlkem/debug/debug.h */
412-
#if defined(POLY_BOUND)
413-
#undef POLY_BOUND
414-
#endif
415-
416-
/* mlkem/debug/debug.h */
417-
#if defined(POLY_BOUND_MSG)
418-
#undef POLY_BOUND_MSG
419-
#endif
420-
421-
/* mlkem/debug/debug.h */
422-
#if defined(POLY_BOUND_MSG)
423-
#undef POLY_BOUND_MSG
424-
#endif
425-
426-
/* mlkem/debug/debug.h */
427-
#if defined(POLY_UBOUND)
428-
#undef POLY_UBOUND
429-
#endif
430-
431-
/* mlkem/debug/debug.h */
432-
#if defined(POLY_UBOUND)
433-
#undef POLY_UBOUND
434-
#endif
435-
436-
/* mlkem/debug/debug.h */
437-
#if defined(POLY_UBOUND_MSG)
438-
#undef POLY_UBOUND_MSG
439-
#endif
440-
441-
/* mlkem/debug/debug.h */
442-
#if defined(POLY_UBOUND_MSG)
443-
#undef POLY_UBOUND_MSG
367+
#if defined(debug_assert)
368+
#undef debug_assert
444369
#endif
445370

446371
/* mlkem/debug/debug.h */
447-
#if defined(SCALAR_BOUND)
448-
#undef SCALAR_BOUND
372+
#if defined(debug_assert)
373+
#undef debug_assert
449374
#endif
450375

451376
/* mlkem/debug/debug.h */
452-
#if defined(SCALAR_BOUND)
453-
#undef SCALAR_BOUND
377+
#if defined(debug_assert_abs_bound)
378+
#undef debug_assert_abs_bound
454379
#endif
455380

456381
/* mlkem/debug/debug.h */
457-
#if defined(STATIC_ASSERT)
458-
#undef STATIC_ASSERT
382+
#if defined(debug_assert_abs_bound)
383+
#undef debug_assert_abs_bound
459384
#endif
460385

461386
/* mlkem/debug/debug.h */
462-
#if defined(UBOUND)
463-
#undef UBOUND
387+
#if defined(debug_assert_bound)
388+
#undef debug_assert_bound
464389
#endif
465390

466391
/* mlkem/debug/debug.h */
467-
#if defined(UBOUND)
468-
#undef UBOUND
392+
#if defined(debug_assert_bound)
393+
#undef debug_assert_bound
469394
#endif
470395

471396
/* mlkem/debug/debug.h */

‎mlkem/cbmc.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@
1313

1414
#define __contract__(x)
1515
#define __loop__(x)
16-
#define cassert(x, y)
16+
#define cassert(x)
1717

1818
#else /* CBMC _is_ defined, therefore we're doing proof */
1919

@@ -30,7 +30,7 @@
3030
#define invariant(...) __CPROVER_loop_invariant(__VA_ARGS__)
3131
#define decreases(...) __CPROVER_decreases(__VA_ARGS__)
3232
/* cassert to avoid confusion with in-built assert */
33-
#define cassert(...) __CPROVER_assert(__VA_ARGS__)
33+
#define cassert(x) __CPROVER_assert(x, "cbmc assertion failed")
3434
#define assume(...) __CPROVER_assume(__VA_ARGS__)
3535

3636
/***************************************************

‎mlkem/debug/debug.c

+11-11
Original file line numberDiff line numberDiff line change
@@ -7,24 +7,23 @@
77
#if defined(MLKEM_DEBUG)
88

99
#include <stdio.h>
10+
#include <stdlib.h>
1011
#include "debug.h"
1112

1213
#define MLKEM_NATIVE_DEBUG_ERROR_HEADER "[ERROR:%s:%04d] "
1314

14-
void mlkem_debug_assert(const char *file, int line, const char *description,
15-
const int val)
15+
void mlkem_debug_assert(const char *file, int line, const int val)
1616
{
1717
if (val == 0)
1818
{
1919
fprintf(stderr,
20-
MLKEM_NATIVE_DEBUG_ERROR_HEADER "Assertion failed: %s (value %d)\n",
21-
file, line, description, val);
20+
MLKEM_NATIVE_DEBUG_ERROR_HEADER "Assertion failed (value %d)\n",
21+
file, line, val);
2222
exit(1);
2323
}
2424
}
2525

26-
void mlkem_debug_check_bounds(const char *file, int line,
27-
const char *description, const int16_t *ptr,
26+
void mlkem_debug_check_bounds(const char *file, int line, const int16_t *ptr,
2827
unsigned len, int lower_bound_exclusive,
2928
int upper_bound_exclusive)
3029
{
@@ -35,11 +34,12 @@ void mlkem_debug_check_bounds(const char *file, int line,
3534
int16_t val = ptr[i];
3635
if (!(val > lower_bound_exclusive && val < upper_bound_exclusive))
3736
{
38-
fprintf(stderr,
39-
MLKEM_NATIVE_DEBUG_ERROR_HEADER
40-
"%s, index %u, value %d out of bounds (%d,%d)\n",
41-
file, line, description, i, (int)val, lower_bound_exclusive,
42-
upper_bound_exclusive);
37+
fprintf(
38+
stderr,
39+
MLKEM_NATIVE_DEBUG_ERROR_HEADER
40+
"Bounds assertion failed: Index %u, value %d out of bounds (%d,%d)\n",
41+
file, line, i, (int)val, lower_bound_exclusive,
42+
upper_bound_exclusive);
4343
err = 1;
4444
}
4545
}

0 commit comments

Comments
 (0)