Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Changing some prettyping errors to be able to ignore them (preparation to fix bug #727) #1023

Merged
merged 1 commit into from
Jan 27, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
14 changes: 5 additions & 9 deletions compiler/src/pretyping.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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"

Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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 _ -> ()
Expand Down Expand Up @@ -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 =
Expand Down
28 changes: 20 additions & 8 deletions compiler/src/utils.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -438,18 +442,26 @@ let add_warning (w:warning) () =

let nowarning () = warns := Some []


let to_warn w =
match !warns with
| None -> true
| Some ws -> w = Always || List.mem w ws

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
)

2 changes: 2 additions & 0 deletions compiler/src/utils.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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 :
Expand Down