From cf4c89727d92afff6432ffd0fd958064550a0c57 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jean-Christophe=20L=C3=A9chenet?=
 <jean-christophe.lechenet@inria.fr>
Date: Mon, 20 Nov 2023 16:18:36 +0100
Subject: [PATCH] Stack zeroization for ARM: add tests

Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>
---
 compiler/Makefile                       |  4 +++-
 compiler/config/tests.config            | 12 ++++++++++++
 compiler/src/pretyping.ml               |  9 ++++-----
 compiler/tests/success/arm-m4/rand.jazz |  6 ++++++
 4 files changed, 25 insertions(+), 6 deletions(-)

diff --git a/compiler/Makefile b/compiler/Makefile
index 7525ebb00..2af0ac0c0 100644
--- a/compiler/Makefile
+++ b/compiler/Makefile
@@ -15,7 +15,9 @@ CHECKCATS ?= \
 	arm-m4 \
 	arm-m4-print \
 	x86-64-stack-zero-loop \
-	x86-64-stack-zero-unrolled
+	x86-64-stack-zero-unrolled \
+	arm-m4-stack-zero-loop \
+	arm-m4-stack-zero-unrolled
 
 # --------------------------------------------------------------------
 DESTDIR  ?=
diff --git a/compiler/config/tests.config b/compiler/config/tests.config
index 9ec800d50..0b3129137 100644
--- a/compiler/config/tests.config
+++ b/compiler/config/tests.config
@@ -67,3 +67,15 @@ args    = -stack-zero=unrolled
 okdirs  = examples/**/x86-64 tests/success/**/x86-64
 kodirs  = tests/fail/**/x86-64
 exclude = !tests/fail/warning
+
+[test-arm-m4-stack-zero-loop]
+bin     = ./scripts/check-arm-m4
+args    = -stack-zero=loop
+okdirs  = examples/**/arm-m4 tests/success/**/arm-m4
+kodirs  = tests/fail/**/arm-m4
+
+[test-arm-m4-stack-zero-unrolled]
+bin     = ./scripts/check-arm-m4
+args    = -stack-zero=unrolled
+okdirs  = examples/**/arm-m4 tests/success/**/arm-m4
+kodirs  = tests/fail/**/arm-m4
diff --git a/compiler/src/pretyping.ml b/compiler/src/pretyping.ml
index 1e36afd30..5d6536881 100644
--- a/compiler/src/pretyping.ml
+++ b/compiler/src/pretyping.ml
@@ -1850,11 +1850,10 @@ let process_f_annot loc funname f_cc annot =
     match strategy, size with
     | None, None -> None
     | None, Some _ ->
-        hierror
-          ~loc:(Lone loc)
-          ~funname
-          ~kind:"unexpected annotation"
-          "\"stackzerosize\" cannot be used alone, you need to specify a strategy with attribute \"stackzero\""
+        warning Always
+          (L.i_loc0 loc)
+          "\"stackzerosize\" is ignored, since you did not specify a strategy with attribute \"stackzero\"";
+        None
     | Some szs, _ -> Some (szs, size)
   in
 
diff --git a/compiler/tests/success/arm-m4/rand.jazz b/compiler/tests/success/arm-m4/rand.jazz
index 02b3c1b18..b2c574478 100644
--- a/compiler/tests/success/arm-m4/rand.jazz
+++ b/compiler/tests/success/arm-m4/rand.jazz
@@ -1,3 +1,9 @@
+/* stack zeroization uses the alignment of the function as the default clear
+   step size. Due to the system call, the function is aligned on u128, but stack
+   zeroization is not implemented for u128 on ARM. Thus we introduce this
+   annotation to use u32 for the clear step size instead.
+*/
+#[stackzerosize=u32]
 export
 fn random32() -> reg u32 {
   stack u8[4] s;