CBMC: Use instrumented malloc/free for MLD_ALLOC/MLD_FREE

proofs/cbmc/H/H_harness.c

@@ -9,6 +9,11 @@ void mld_H(uint8_t *out, size_t outlen, const uint8_t *in1, size_t in1len,
 
 void harness(void)
 {
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
   uint8_t *out;
   size_t outlen;
   const uint8_t *in1;

proofs/cbmc/Makefile.common

@@ -247,7 +247,7 @@ endif
 #   * an entire project when added to Makefile-project-defines
 #   * a specific proof when added to the harness Makefile
 
-CBMC_FLAG_MALLOC_MAY_FAIL ?= --malloc-fail-assert
+CBMC_FLAG_MALLOC_MAY_FAIL ?= --malloc-may-fail --malloc-fail-null # alloc may fail with returning NULL
 CBMC_FLAG_BOUNDS_CHECK ?= # set to --no-bounds-check to disable
 CBMC_FLAG_CONVERSION_CHECK ?= --conversion-check
 CBMC_FLAG_DIV_BY_ZERO_CHECK ?= # set to --no-div-by-zero-check to disable

proofs/cbmc/check_pct/Makefile

@@ -10,7 +10,7 @@ HARNESS_FILE = check_pct_harness
 # Litani dashboard. It can be human-readable and contain spaces if you wish.
 PROOF_UID = mld_check_pct
 
-DEFINES += -DMLD_CONFIG_KEYGEN_PCT
+DEFINES +=
 INCLUDES +=
 
 REMOVE_FUNCTION_BODY +=

proofs/cbmc/mldsa_native_config_cbmc.h

@@ -25,11 +25,14 @@
  */
 
 /*
- * Test configuration: mldsa-native configuration used for CBMC proofs
+ * Test configuration: mldsa-native configuration used for CBMC proofs, using
+ * instrumented alloc/free
  *
  * This configuration differs from the default mldsa/mldsa_native_config.h in
  * the following places:
  *   - MLD_CONFIG_NAMESPACE_PREFIX
+ *   - MLD_CONFIG_KEYGEN_PCT
+ *   - MLD_CONFIG_CUSTOM_ALLOC_FREE
  */
 
 
@@ -541,15 +544,13 @@
  *              code will handle this case and invoke MLD_CUSTOM_FREE.
  *
  *****************************************************************************/
-/* #define MLD_CONFIG_CUSTOM_ALLOC_FREE
-   #if !defined(__ASSEMBLER__)
-   #include <stdlib.h>
-   #define MLD_CUSTOM_ALLOC(v, T, N)                              \
-     T* (v) = (T *)aligned_alloc(MLD_DEFAULT_ALIGN,               \
-                                 MLD_ALIGN_UP(sizeof(T) * (N)))
-   #define MLD_CUSTOM_FREE(v, T, N) free(v)
-   #endif
-*/
+#define MLD_CONFIG_CUSTOM_ALLOC_FREE
+#if !defined(__ASSEMBLER__)
+#include <stdlib.h>
+#define MLD_CUSTOM_ALLOC(v, T, N) T *v = (T *)malloc(sizeof(T) * (N))
+#define MLD_CUSTOM_FREE(v, T, N) free(v)
+#endif
+
 
 /******************************************************************************
  * Name:        MLD_CONFIG_CUSTOM_MEMCPY
@@ -678,7 +679,7 @@
  *              requires crypto_sign_signature() and crypto_sign_verify().
  *
  *****************************************************************************/
-/* #define MLD_CONFIG_KEYGEN_PCT */
+#define MLD_CONFIG_KEYGEN_PCT
 
 /******************************************************************************
  * Name:        MLD_CONFIG_KEYGEN_PCT_BREAKAGE_TEST

proofs/cbmc/prepare_domain_separation_prefix/prepare_domain_separation_prefix_harness.c

@@ -5,6 +5,11 @@
 
 void harness(void)
 {
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
   uint8_t *prefix;
   const uint8_t *ph;
   size_t phlen;

proofs/cbmc/sample_s1_s2/sample_s1_s2_harness.c

@@ -8,6 +8,11 @@ static void mld_sample_s1_s2(mld_polyvecl *s1, mld_polyveck *s2,
 
 void harness(void)
 {
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
   mld_polyvecl *s1;
   mld_polyveck *s2;
   uint8_t *seed;

proofs/cbmc/sample_s1_s2_serial/sample_s1_s2_harness.c

@@ -8,6 +8,11 @@ static void mld_sample_s1_s2(mld_polyvecl *s1, mld_polyveck *s2,
 
 void harness(void)
 {
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
   mld_polyvecl *s1;
   mld_polyveck *s2;
   uint8_t *seed;

proofs/cbmc/sign_signature_internal/Makefile

@@ -43,7 +43,7 @@ FUNCTION_NAME = sign_signature_internal
 # EXPENSIVE = true
 
 # This function is large enough to need...
-CBMC_OBJECT_BITS = 8
+CBMC_OBJECT_BITS = 9
 
 # If you require access to a file-local ("static") function or object to conduct
 # your proof, set the following (and do not include the original source file

test/configs/configs.yml

@@ -472,8 +472,17 @@ configs:
         comment: "/* No need to set this -- we _are_ already in a custom config */"
 
   - path: proofs/cbmc/mldsa_native_config_cbmc.h
-    description: "mldsa-native configuration used for CBMC proofs"
+    description: "mldsa-native configuration used for CBMC proofs, using instrumented alloc/free"
     defines:
       MLD_CONFIG_NAMESPACE_PREFIX: mld
+      MLD_CONFIG_KEYGEN_PCT: true
+      MLD_CONFIG_CUSTOM_ALLOC_FREE:
+        content: |
+          #define MLD_CONFIG_CUSTOM_ALLOC_FREE
+          #if !defined(__ASSEMBLER__)
+          #include <stdlib.h>
+          #define MLD_CUSTOM_ALLOC(v, T, N) T* v = (T *)malloc(sizeof(T) * (N))
+          #define MLD_CUSTOM_FREE(v, T, N) free(v)
+          #endif /* !__ASSEMBLER__ */
       MLD_CONFIG_FILE:
         comment: "/* No need to set this -- we _are_ already in a custom config */"