CN: move magic-comment mode to a Cerb switch

rems-project · Jul 26, 2023 · be89844 · be89844
1 parent feda0f9
commit be89844
Show file tree

Hide file tree

Showing 4 changed files with 27 additions and 9 deletions.
diff --git a/backend/cn/main.ml b/backend/cn/main.ml
@@ -59,10 +59,8 @@ open Log
 let frontend incl_dirs incl_files astprints filename state_file =
   let open CF in
   Cerb_global.set_cerb_conf "Cn" false Random false Basic false false false false false;
-  (* FIXME: make this a global config thing rather than poking state. *)
-  C_lexer.set_magic_comment_mode (C_lexer.(Magic_At true));
   Ocaml_implementation.set Ocaml_implementation.HafniumImpl.impl;
-  Switches.set ["inner_arg_temps"];
+  Switches.set ["inner_arg_temps"; "at_magic_comments"; "warn_mismatched_magic_comments"];
   let@ stdlib = load_core_stdlib () in
   let@ impl = load_core_impl stdlib impl_name in
   let conf = Setup.conf incl_dirs incl_files astprints in

diff --git a/ocaml_frontend/switches.ml b/ocaml_frontend/switches.ml
@@ -34,6 +34,11 @@ type cerb_switch =
   (* pointer revocation *)
   | SW_revocation of [ `INSTANT | `CORNUCOPIA]
 
+  (* parsing of magic comments (e.g. "/*@ magic() @*/" as statements *)
+  | SW_at_magic_comments
+  | SW_warn_mismatched_magic_comments
+
+
 let internal_ref =
   ref []
 
@@ -83,6 +88,10 @@ let set strs =
         Some (SW_revocation `INSTANT)
     | "cornucopia" ->
         Some (SW_revocation `CORNUCOPIA)
+    | "at_magic_comments" ->
+        Some SW_at_magic_comments
+    | "warn_mismatched_magic_comments" ->
+        Some SW_warn_mismatched_magic_comments
     | _ ->
         None in
   List.iter (fun str ->

diff --git a/ocaml_frontend/switches.mli b/ocaml_frontend/switches.mli
@@ -34,6 +34,10 @@ type cerb_switch =
   (* pointer revocation *)
   | SW_revocation of [ `INSTANT | `CORNUCOPIA]
 
+  (* parsing of magic comments (e.g. "/*@ magic() @*/" as statements *)
+  | SW_at_magic_comments
+  | SW_warn_mismatched_magic_comments
+
 val get_switches: unit -> cerb_switch list
 val has_switch: cerb_switch -> bool
 val has_switch_pred: (cerb_switch -> bool) -> cerb_switch option

diff --git a/parsers/c/c_lexer.mll b/parsers/c/c_lexer.mll
@@ -11,8 +11,7 @@ type magic_comment_mode =
   | Magic_At of bool
 
 type internal_state = {
-  (* maybe make this 'config' rather than 'internal' *)
-  mutable magic_comment_mode: magic_comment_mode;
+  mutable magic_comment_mode: magic_comment_mode option;
 
   mutable inside_cn: bool;
   (* HACK fo fix col positions when seing CN keywords (look at C_parser_driver) *)
@@ -23,7 +22,7 @@ type internal_state = {
   mutable magic_acc: (Cerb_location.t * string) list;
 }
 let internal_state = {
-  magic_comment_mode= Magic_None;
+  magic_comment_mode= None;
   inside_cn= false;
   cnum_hack= 0;
   start_of_comment= Lexing.dummy_pos;
@@ -32,8 +31,16 @@ let internal_state = {
   magic_acc= [];
 }
 
-let set_magic_comment_mode mode =
-  internal_state.magic_comment_mode <- mode
+let get_magic_comment_mode () = match internal_state.magic_comment_mode with
+  | None ->
+    (* fetch the mode from the global switches and cache for faster lookup *)
+    let mode = if Switches.(has_switch SW_at_magic_comments)
+      then Magic_At (Switches.(has_switch SW_warn_mismatched_magic_comments))
+      else Magic_None
+    in
+    internal_state.magic_comment_mode <- Some mode;
+    mode
+  | Some mode -> mode
 
 let new_line lexbuf =
   (* the hacked col offset MUST be reset after every newline *)
@@ -198,7 +205,7 @@ let magic_token start_pos end_pos chars =
   if len < 2 then None
   else
   let first, last = List.hd chars, List.nth chars (len - 1) in
-  match internal_state.magic_comment_mode with
+  match get_magic_comment_mode () with
   | Magic_At _ when first == '@' && last == '@' ->
     let str = String.init (len - 2) (List.nth (List.tl chars)) in
     internal_state.last_magic_comment <- Some (end_pos, loc);