Merge pull request hacl-star#828 from hacl-star/afromher_824

Inline double_row definition in Blake to avoid VLA
mtzguido · Jun 9, 2023 · c7bf4f4 · c7bf4f4
2 parents 3663d03 + 6230d2e
commit c7bf4f4
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 20 deletions.
diff --git a/code/blake2/Hacl.Impl.Blake2.Generic.fst b/code/blake2/Hacl.Impl.Blake2.Generic.fst
@@ -675,6 +675,7 @@ val blake2_finish:#al:Spec.alg -> #ms:m_spec -> blake2_finish_st al ms
 
 let blake2_finish #al #ms nn output hash =
   let h0 = ST.get () in
+  [@inline_let]
   let double_row = 2ul *. size_row al in
   [@inline_let]
   let spec _ h1 = h1.[|output|] == Spec.blake2_finish al (state_v h0 hash) (v nn) in

diff --git a/dist/gcc-compatible/Hacl_Hash_Blake2.c b/dist/gcc-compatible/Hacl_Hash_Blake2.c
@@ -625,10 +625,7 @@ blake2b_update(uint64_t *wv, uint64_t *hash, uint32_t kk, uint8_t *k, uint32_t l
 
 void Hacl_Blake2b_32_blake2b_finish(uint32_t nn, uint8_t *output, uint64_t *hash)
 {
-  uint32_t double_row = (uint32_t)64U;
-  KRML_CHECK_SIZE(sizeof (uint8_t), double_row);
-  uint8_t b[double_row];
-  memset(b, 0U, double_row * sizeof (uint8_t));
+  uint8_t b[64U] = { 0U };
   uint8_t *first = b;
   uint8_t *second = b + (uint32_t)32U;
   uint64_t *row0 = hash;
@@ -645,7 +642,7 @@ void Hacl_Blake2b_32_blake2b_finish(uint32_t nn, uint8_t *output, uint64_t *hash
     store64_le(second + i * (uint32_t)8U, row1[i]););
   uint8_t *final = b;
   memcpy(output, final, nn * sizeof (uint8_t));
-  Lib_Memzero0_memzero(b, double_row * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b, (uint32_t)64U * sizeof (b[0U]));
 }
 
 /**
@@ -1267,10 +1264,7 @@ blake2s_update(uint32_t *wv, uint32_t *hash, uint32_t kk, uint8_t *k, uint32_t l
 
 void Hacl_Blake2s_32_blake2s_finish(uint32_t nn, uint8_t *output, uint32_t *hash)
 {
-  uint32_t double_row = (uint32_t)32U;
-  KRML_CHECK_SIZE(sizeof (uint8_t), double_row);
-  uint8_t b[double_row];
-  memset(b, 0U, double_row * sizeof (uint8_t));
+  uint8_t b[32U] = { 0U };
   uint8_t *first = b;
   uint8_t *second = b + (uint32_t)16U;
   uint32_t *row0 = hash;
@@ -1287,7 +1281,7 @@ void Hacl_Blake2s_32_blake2s_finish(uint32_t nn, uint8_t *output, uint32_t *hash
     store32_le(second + i * (uint32_t)4U, row1[i]););
   uint8_t *final = b;
   memcpy(output, final, nn * sizeof (uint8_t));
-  Lib_Memzero0_memzero(b, double_row * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b, (uint32_t)32U * sizeof (b[0U]));
 }
 
 /**

diff --git a/dist/gcc-compatible/Hacl_Hash_Blake2b_256.c b/dist/gcc-compatible/Hacl_Hash_Blake2b_256.c
@@ -360,10 +360,7 @@ Hacl_Blake2b_256_blake2b_finish(
   Lib_IntVector_Intrinsics_vec256 *hash
 )
 {
-  uint32_t double_row = (uint32_t)64U;
-  KRML_CHECK_SIZE(sizeof (uint8_t), double_row);
-  uint8_t b[double_row];
-  memset(b, 0U, double_row * sizeof (uint8_t));
+  uint8_t b[64U] = { 0U };
   uint8_t *first = b;
   uint8_t *second = b + (uint32_t)32U;
   Lib_IntVector_Intrinsics_vec256 *row0 = hash;
@@ -372,7 +369,7 @@ Hacl_Blake2b_256_blake2b_finish(
   Lib_IntVector_Intrinsics_vec256_store64_le(second, row1[0U]);
   uint8_t *final = b;
   memcpy(output, final, nn * sizeof (uint8_t));
-  Lib_Memzero0_memzero(b, double_row * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b, (uint32_t)64U * sizeof (b[0U]));
 }
 
 /**

diff --git a/dist/gcc-compatible/Hacl_Hash_Blake2s_128.c b/dist/gcc-compatible/Hacl_Hash_Blake2s_128.c
@@ -352,10 +352,7 @@ Hacl_Blake2s_128_blake2s_finish(
   Lib_IntVector_Intrinsics_vec128 *hash
 )
 {
-  uint32_t double_row = (uint32_t)32U;
-  KRML_CHECK_SIZE(sizeof (uint8_t), double_row);
-  uint8_t b[double_row];
-  memset(b, 0U, double_row * sizeof (uint8_t));
+  uint8_t b[32U] = { 0U };
   uint8_t *first = b;
   uint8_t *second = b + (uint32_t)16U;
   Lib_IntVector_Intrinsics_vec128 *row0 = hash;
@@ -364,7 +361,7 @@ Hacl_Blake2s_128_blake2s_finish(
   Lib_IntVector_Intrinsics_vec128_store32_le(second, row1[0U]);
   uint8_t *final = b;
   memcpy(output, final, nn * sizeof (uint8_t));
-  Lib_Memzero0_memzero(b, double_row * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b, (uint32_t)32U * sizeof (b[0U]));
 }
 
 /**