From 38979db0bbd3ea53bfbc67f4981c0777713d649d Mon Sep 17 00:00:00 2001
From: Alexandre BOURBEILLON <alexandrebourbeillon@gmail.com>
Date: Fri, 24 Jan 2025 14:07:58 +0100
Subject: [PATCH] Changing some prettyping errors to be able to ignore them
 (with a global boolean, it is useful for experimentation purposes)

---
 CHANGELOG.md              |  3 +++
 compiler/src/pretyping.ml | 14 +++++---------
 compiler/src/utils.ml     | 28 ++++++++++++++++++++--------
 compiler/src/utils.mli    |  2 ++
 4 files changed, 30 insertions(+), 17 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7315e3f90..1d01dc65a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -35,6 +35,9 @@
   therefore old intrinsic `#VPBLENDVB` is deprecated
   ([PR #1010](https://github.com/jasmin-lang/jasmin/pull/1010)).
 
+- Add an option to treat some pre-typing error as warning instead. 
+  ([PR #1023](https://github.com/jasmin-lang/jasmin/pull/1023))
+
 ## Bug fixes
 
 - Fix EasyCrypt semantics of shift operators
diff --git a/compiler/src/pretyping.ml b/compiler/src/pretyping.ml
index b987f0722..ac2405afe 100644
--- a/compiler/src/pretyping.ml
+++ b/compiler/src/pretyping.ml
@@ -46,7 +46,6 @@ type tyerror =
   | UnknownPrim of A.symbol * string
   | PrimWrongSuffix of A.symbol * Sopn.prim_x86_suffix list
   | PtrOnlyForArray
-  | WriteToConstantPointer of A.symbol
   | PackSigned
   | PackWrongWS of int
   | PackWrongPE of int
@@ -207,9 +206,6 @@ let pp_tyerror fmt (code : tyerror) =
   | PtrOnlyForArray -> 
     F.fprintf fmt "Pointer allowed only on array"
 
-  | WriteToConstantPointer v ->
-    F.fprintf fmt "Cannot write to the constant pointer %s" v
-
   | PackSigned ->
     F.fprintf fmt "packs should be unsigned"
 
@@ -1279,7 +1275,7 @@ let tt_lvalue pd (env : 'asm Env.env) { L.pl_desc = pl; L.pl_loc = loc; } =
   let reject_constant_pointers loc x =
     match x.P.v_kind with
     | Stack (Pointer Constant) | Reg (_, Pointer Constant) ->
-       rs_tyerror ~loc (WriteToConstantPointer x.P.v_name)
+       warning PedanticPretyping (L.i_loc0 loc) "Cannot write to the constant pointer %s" x.P.v_name
     | _ -> ()
   in
 
@@ -1729,7 +1725,7 @@ let mk_call loc inline lvs f es =
     let rec check_e = function
       | Pvar _ | Psub _ -> ()
       | Pif (_, _, e1, e2) -> check_e e1; check_e e2
-      | _ -> rs_tyerror ~loc (string_error "only variables and subarray are allowed in arguments of non-inlined function") in
+      | _ -> warning PedanticPretyping (L.i_loc0 loc)  "only variables and subarray are allowed in arguments of non-inlined function" in
     List.iter check_lval lvs;
     List.iter check_e es
   | Subroutine _ -> ()
@@ -1993,10 +1989,10 @@ let tt_call_conv _loc params returns cc =
   | Some `Export | None ->
     let check s x =
       if not (P.is_reg_kind (L.unloc x).P.v_kind) then 
-        rs_tyerror ~loc:(L.loc x) 
-          (string_error "%a has kind %a, only reg or reg ptr are allowed in %s of non inlined function"
+        warning PedanticPretyping (L.i_loc0 (L.loc x))
+          "%a has kind %a, only reg or reg ptr are allowed in %s of non inlined function"
             Printer.pp_pvar (L.unloc x)
-            PrintCommon.pp_kind (L.unloc x).P.v_kind s) in
+            PrintCommon.pp_kind (L.unloc x).P.v_kind s in
     List.iter (check "parameter") params;
     List.iter (check "result") returns;
     let returned_params =
diff --git a/compiler/src/utils.ml b/compiler/src/utils.ml
index 5cb7f806c..cfb82c14f 100644
--- a/compiler/src/utils.ml
+++ b/compiler/src/utils.ml
@@ -426,8 +426,12 @@ type warning =
   | Deprecated
   | Experimental
   | Always
+  | PedanticPretyping
 
 let warns = ref None
+let warn_recoverable = ref false
+
+let set_warn_recoverable b = warn_recoverable := b
 
 let add_warning (w:warning) () = 
   match !warns with
@@ -438,6 +442,7 @@ let add_warning (w:warning) () =
 
 let nowarning () = warns := Some []
 
+
 let to_warn w = 
   match !warns with
   | None -> true
@@ -445,11 +450,18 @@ let to_warn w =
 
 let warning (w:warning) loc =
   Format.kdprintf (fun pp ->
-    if to_warn w then
-      let pp_warning fmt = pp_print_bold_magenta pp_string fmt "warning" in
-      let pp_iloc fmt d =
-        if not (Location.isdummy d.Location.base_loc) then
-          Format.fprintf fmt "%a@ " (pp_print_bold Location.pp_iloc) d in
-      Format.eprintf "@[<v>%a%t: %t@]@."
-        pp_iloc loc
-        pp_warning pp)
+    match w with 
+    | PedanticPretyping when not !warn_recoverable -> 
+      hierror ~loc:(Lmore loc) ~kind:"typing error"
+        "%t" pp
+    | _ ->
+      if to_warn w then
+        let pp_warning fmt = pp_print_bold_magenta pp_string fmt "warning" in
+        let pp_iloc fmt d =
+          if not (Location.isdummy d.Location.base_loc) then
+            Format.fprintf fmt "%a@ " (pp_print_bold Location.pp_iloc) d in
+        Format.eprintf "@[<v>%a%t: %t@]@."
+          pp_iloc loc
+          pp_warning pp
+    )
+        
diff --git a/compiler/src/utils.mli b/compiler/src/utils.mli
index 251991941..b2cc8ffdd 100644
--- a/compiler/src/utils.mli
+++ b/compiler/src/utils.mli
@@ -186,7 +186,9 @@ type warning =
   | Deprecated
   | Experimental
   | Always
+  | PedanticPretyping
 
+val set_warn_recoverable : bool -> unit
 val nowarning : unit -> unit
 val add_warning : warning -> unit -> unit 
 val warning :