Skip to content

Commit

Permalink
Add debug assertion for checking scalar bounds
Browse files Browse the repository at this point in the history
We already have `mlkem_debug_check_bounds()` to check
bounds on all elements of an array.

In preparation for use in `fqmul()`, this commit adds
generic `mlkem_debug_assert()` and `ASSERT()` to checking
assertions, and a wrapper assertion `SCALAR_BOUND` to assert
absolute bounds on scalars.

Signed-off-by: Hanno Becker <[email protected]>
  • Loading branch information
hanno-becker committed Oct 31, 2024
1 parent 24d93b3 commit 20dbffb
Show file tree
Hide file tree
Showing 2 changed files with 51 additions and 0 deletions.
10 changes: 10 additions & 0 deletions mlkem/debug/debug.c
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,16 @@

static char debug_buf[256];

void mlkem_debug_assert(const char *file, int line,
const char *description, const int val) {
if (val == 0)
{
snprintf(debug_buf, sizeof(debug_buf),
"Assertion failed: %s (value %d)", description, val);
mlkem_debug_print_error(file, line, debug_buf);
exit(1);
}
}
void mlkem_debug_check_bounds(const char *file, int line,
const char *description, const int16_t *ptr,
unsigned len, int lower_bound_exclusive,
Expand Down
41 changes: 41 additions & 0 deletions mlkem/debug/debug.h
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,22 @@
#include <stdio.h>
#include <stdlib.h>

/*************************************************
* Name: mlkem_debug_assert
*
* Description: Check debug assertion
*
* Prints an error message to stderr and calls
* exit(1) if not.
*
* Arguments: - file: filename
* - line: line number
* - description: Textual description of assertion
* - val: Value asserted to be non-zero
**************************************************/
void mlkem_debug_assert(const char *file, int line,
const char *description, const int val);

/*************************************************
* Name: mlkem_debug_check_bounds
*
Expand All @@ -32,6 +48,25 @@ void mlkem_debug_check_bounds(const char *file, int line,
/* Print error message to stderr alongside file and line information */
void mlkem_debug_print_error(const char *file, int line, const char *msg);

/* Check assertion, calling exit() upon failure
*
* val: Value that's asserted to be non-zero
* msg: Message to print on failure
*
* Currently called CASSERT to avoid clash with CBMC assert.
*/
#define CASSERT(val, msg) \
do { \
mlkem_debug_assert(__FILE__, __LINE__, (msg), (val)); \
} while (0)

/* Check absolute bounds of scalar
* val: Scalar to be checked
* abs_bound: Exclusive upper bound on absolute value to check
* msg: Message to print on failure */
#define SCALAR_BOUND(val, abs_bound, msg) \
CASSERT((val) > -(abs_bound) && (val) < (abs_bound), msg)

/* Check that all coefficients in array of int16_t's are non-negative
* and below an exclusive upper bound.
*
Expand Down Expand Up @@ -127,6 +162,12 @@ void mlkem_debug_print_error(const char *file, int line, const char *msg);

#else /* MLKEM_DEBUG */

#define CASSERT(...) \
do { \
} while (0)
#define SCALAR_BOUND(...) \
do { \
} while (0)
#define BOUND(...) \
do { \
} while (0)
Expand Down

0 comments on commit 20dbffb

Please sign in to comment.