mldsa-native/mldsa/src/debug.h at v1.0.0-beta · pq-code-package/mldsa-native · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
/*
 * Copyright (c) The mlkem-native project authors
 * Copyright (c) The mldsa-native project authors
 * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 */
#ifndef MLD_DEBUG_H
#define MLD_DEBUG_H
#include "common.h"

#if defined(MLDSA_DEBUG)

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

/*************************************************
 * Name:        mld_debug_check_bounds
 *
 * Description: Check whether values in an array of int32_t
 *              are within specified bounds.
 *
 *              Prints an error message to stderr and calls
 *              exit(1) if not.
 *
 * Arguments:   - file: filename
 *              - line: line number
 *              - ptr: Base of array to be checked
 *              - len: Number of int32_t in ptr
 *              - lower_bound_exclusive: Exclusive lower bound
 *              - upper_bound_exclusive: Exclusive upper bound
 **************************************************/
#define mld_debug_check_bounds MLD_NAMESPACE(mldsa_debug_check_bounds)
void mld_debug_check_bounds(const char *file, int line, const int32_t *ptr,
                            unsigned len, int64_t lower_bound_exclusive,
                            int64_t upper_bound_exclusive);

/* Check assertion, calling exit() upon failure
 *
 * val: Value that's asserted to be non-zero
 */
#define mld_assert(val) mld_debug_check_assert(__FILE__, __LINE__, (val))

/* Check bounds in array of int32_t's
 * ptr: Base of int32_t array; will be explicitly cast to int32_t*,
 *      so you may pass a byte-compatible type such as mld_poly or mld_polyvec.
 * len: Number of int32_t in array
 * value_lb: Inclusive lower value bound
 * value_ub: Exclusive upper value bound */
#define mld_assert_bound(ptr, len, value_lb, value_ub)                      \
  mld_debug_check_bounds(__FILE__, __LINE__, (const int32_t *)(ptr), (len), \
                         ((int64_t)(value_lb)) - 1, (value_ub))

/* Check absolute bounds in array of int32_t's
 * ptr: Base of array, expression of type int32_t*
 * len: Number of int32_t in array
 * value_abs_bd: Exclusive absolute upper bound */
#define mld_assert_abs_bound(ptr, len, value_abs_bd)               \
  mld_assert_bound((ptr), (len), (-((int64_t)(value_abs_bd)) + 1), \
                   (value_abs_bd))

/* Version of bounds assertions for 2-dimensional arrays */
#define mld_assert_bound_2d(ptr, len0, len1, value_lb, value_ub) \
  mld_assert_bound((ptr), ((len0) * (len1)), (value_lb), (value_ub))

#define mld_assert_abs_bound_2d(ptr, len0, len1, value_abs_bd) \
  mld_assert_abs_bound((ptr), ((len0) * (len1)), (value_abs_bd))

/* When running CBMC, convert debug assertions into proof obligations */
#elif defined(CBMC)
#include "cbmc.h"

#define mld_assert(val) cassert(val)

#define mld_assert_bound(ptr, len, value_lb, value_ub) \
  cassert(array_bound(((int32_t *)(ptr)), 0, (len), (value_lb), (value_ub)))

#define mld_assert_abs_bound(ptr, len, value_abs_bd) \
  cassert(array_abs_bound(((int32_t *)(ptr)), 0, (len), (value_abs_bd)))

/* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
 * just use a single flattened array_bound(...) here. */
#define mld_assert_bound_2d(ptr, M, N, value_lb, value_ub)              \
  cassert(forall(kN, 0, (M),                                            \
                 array_bound(&((int32_t (*)[(N)])(ptr))[kN][0], 0, (N), \
                             (value_lb), (value_ub))))

#define mld_assert_abs_bound_2d(ptr, M, N, value_abs_bd)                    \
  cassert(forall(kN, 0, (M),                                                \
                 array_abs_bound(&((int32_t (*)[(N)])(ptr))[kN][0], 0, (N), \
                                 (value_abs_bd))))

#else /* !MLDSA_DEBUG && CBMC */

#define mld_assert(val) \
  do                    \
  {                     \
  } while (0)
#define mld_assert_bound(ptr, len, value_lb, value_ub) \
  do                                                   \
  {                                                    \
  } while (0)
#define mld_assert_abs_bound(ptr, len, value_abs_bd) \
  do                                                 \
  {                                                  \
  } while (0)

#define mld_assert_bound_2d(ptr, len0, len1, value_lb, value_ub) \
  do                                                             \
  {                                                              \
  } while (0)

#define mld_assert_abs_bound_2d(ptr, len0, len1, value_abs_bd) \
  do                                                           \
  {                                                            \
  } while (0)


#endif /* !MLDSA_DEBUG && !CBMC */
#endif /* !MLD_DEBUG_H */