Use warnings for duplicate and missing extensions

Author: bclement-ocp

doc/extensions.md

@@ -14,10 +14,10 @@ The `dolmen` command-line tool looks up user-defined extensions using the Dune
 plugin mechanism. A plugin named `plugin.typing` will be picked up when
 `--ext plugin` or `--ext plugin.typing` is provided on the command-line, and
 the plugin must register a typing extension named `"plugin"` using
-`Dolmen_loop.Typer.Ext.create`. A plugin named `plugin.model` will be picked up
+`Dolmen_loop.Typer.Ext.register`. A plugin named `plugin.model` will be picked up
 when `--ext plugin` or `--ext plugin.model` is provided on the command-line and
 the plugin must register a model extension named `"plugin"` using
-`Dolmen_model.Env.Ext.create`. A plugin named `plugin` (without dots) will be
+`Dolmen_model.Ext.register`. A plugin named `plugin` (without dots) will be
 picked up when either of the above command line flags is provided, and must
 provide both a typing and model extension.
 

examples/extensions/abs_real/abs_real.ml

@@ -46,4 +46,4 @@ let builtins ~eval:_ _ (cst : Dolmen.Std.Expr.Term.Const.t) =
   | _ -> None
 
 let model_ext =
-  Dolmen_model.Ext.create ~name:"abs_real" ~builtins
+  Dolmen_model.Ext.create ~name:"abs_real" ~builtins

examples/extensions/abs_real_split/abs_real_model.ml

@@ -13,4 +13,4 @@ let builtins ~eval:_ _ (cst : Dolmen.Std.Expr.Term.Const.t) =
   | _ -> None
 
 let model_ext =
-  Dolmen_model.Ext.create ~name:"abs_real_split" ~builtins
+  Dolmen_model.Ext.create ~name:"abs_real_split" ~builtins

examples/extensions/abs_real_split/abs_real_typing.ml

@@ -29,4 +29,4 @@ let builtins _lang env s =
   | _ -> `Not_found
 
 let typing_ext =
-  Dolmen_loop.Typer.Ext.create ~name:"abs_real_split" ~builtins
+  Dolmen_loop.Typer.Ext.create ~name:"abs_real_split" ~builtins

src/bin/extensions.ml

@@ -15,8 +15,8 @@ let is_available = function
   | Unavailable -> false
   | Builtin _ | Dune_plugin _ -> true
 
-(* Merge two possible locations for the same plugin. Prefer external plugins
-   over built-in plugins to allow overrides. *)
+(* Merge two possible locations for the same plugin. Prefer builtin plugins over
+   external plugins. *)
 let merge_location p1 p2 =
   match p1, p2 with
   | Dune_plugin _ as p, _ | _, (Dune_plugin _ as p) -> p
@@ -82,15 +82,15 @@ let infos =
         { extension_name = Dolmen_loop.Typer.Ext.name ext
         ; typing_plugin = Builtin ext
         ; model_plugin = Unavailable }
-    ) (Dolmen_loop.Typer.Ext.list ());
+    ) [ Dolmen_loop.Typer.Ext.bvconv ];
 
     (* Add builtin model extensions. *)
     List.iter (fun ext ->
       add_ext extensions
         { extension_name = Dolmen_model.Ext.name ext
         ; typing_plugin = Unavailable
         ; model_plugin = Builtin ext }
-    ) (Dolmen_model.Ext.list ());
+    ) [ Dolmen_model.Ext.bvconv ];
 
     (* Add extensions from plugins. *)
     let add_plugin invalid plugin = function
@@ -134,33 +134,127 @@ let find_ext name =
       name
       Fmt.(list (box pp)) (list ())
 
-let load_typing_extension ext =
+let load_plugin_or_fail plugin =
+  try Ok (Dolmen.Sites.Plugins.Plugins.load plugin)
+  with Dynlink.Error err ->
+    Fmt.error_msg "while loading plugin %s: %s"
+      plugin (Dynlink.error_message err)
+
+let missing_extension =
+  Dolmen_loop.Report.Warning.mk ~mnemonic:"missing-extension"
+    ~message:(fun ppf (kind, ext, _) ->
+      Format.fprintf ppf "There is no %s extension named '%s'." kind ext)
+    ~hints:[fun (kind, _, plugin) ->
+      Some (Format.dprintf
+        "Expected plugin '%s' to register this %s extension." plugin kind)]
+    ~name:"Missing extension" ()
+
+let duplicate_extension =
+  Dolmen_loop.Report.Warning.mk ~mnemonic:"duplicate-extension"
+    ~message:(fun ppf (kind, name, _) ->
+      Format.fprintf ppf
+        "%s extension '%s' was registered multiple times."
+          (String.capitalize_ascii kind)
+          name)
+    ~hints:[
+      (fun (kind, name, _) ->
+        Some (
+          Format.dprintf "%a@ %s@ extension@ '%s'."
+            Fmt.words
+            "This is likely caused by multiple plugins trying to register the"
+            kind name));
+      (fun (kind, _, plugin) ->
+        Some (
+          Format.dprintf "Expected plugin '%s' to register this %s extension."
+            plugin kind))]
+    ~name:"Duplicate extension" ()
+
+let cannot_override_builtin_extension =
+  Dolmen_loop.Report.Warning.mk ~mnemonic:"cannot-override-builtin-extension"
+    ~message:(fun ppf (kind, name) ->
+      Format.fprintf ppf "Cannot override builtin %s extension '%s'."
+        kind name)
+    ~name:"Cannot override builtin extension" ()
+
+let add_typing_extension ext st =
+  Loop.State.update Loop.Typer.extension_builtins (List.cons ext) st
+
+let load_typing_extension ext st =
     match ext.typing_plugin with
     | Unavailable ->
-      Fmt.error_msg "No typing extension '%s'" ext.extension_name
-    | Builtin e ->  Ok e
+      Fmt.error_msg
+        "No plugin provides the typing extension '%s'" ext.extension_name
+    | Builtin e -> (
+      match Dolmen_loop.Typer.Ext.find_all (Dolmen_loop.Typer.Ext.name e) with
+      | [] ->
+        Ok (add_typing_extension e st)
+      | _ ->
+        let st =
+          Loop.State.warn st
+            cannot_override_builtin_extension
+            ("typing", Dolmen_loop.Typer.Ext.name e)
+        in
+        Ok (add_typing_extension e st)
+    )
     | Dune_plugin plugin ->
-      Dolmen.Sites.Plugins.Plugins.load plugin;
-      try
-        Ok (Dolmen_loop.Typer.Ext.find_exn ext.extension_name)
-      with Not_found ->
-        Fmt.error_msg
-          "Plugin '%s' did not register a typing extension for '%s'"
-          plugin ext.extension_name
-
-let load_model_extension ext =
+      Result.bind (load_plugin_or_fail plugin) @@ fun () ->
+      match Dolmen_loop.Typer.Ext.find_all ext.extension_name with
+      | [] ->
+        Ok (
+          Loop.State.warn st
+            missing_extension
+            ("typing", ext.extension_name, plugin)
+        )
+      | [ e ] ->
+        Ok (add_typing_extension e st)
+      | e :: _ ->
+        let st =
+          Loop.State.warn st
+            duplicate_extension
+            ("typing", ext.extension_name, plugin)
+        in
+        Ok (add_typing_extension e st)
+
+let add_model_extension b st =
+  Loop.State.update Loop.Check.builtins
+   (fun bs -> Dolmen_model.Eval.builtins [ Dolmen_model.Ext.builtins b ; bs ])
+   st
+
+let load_model_extension ext st =
     match ext.model_plugin with
     | Unavailable ->
-      Fmt.error_msg "No model extension '%s'" ext.extension_name
-    | Builtin e ->  Ok e
+      Fmt.error_msg
+        "No plugin provides the model extension '%s'" ext.extension_name
+    | Builtin e -> (
+      match Dolmen_model.Ext.find_all (Dolmen_model.Ext.name e) with
+      | [] ->
+        Ok (add_model_extension e st)
+      | _ ->
+        let st =
+          Loop.State.warn st
+            cannot_override_builtin_extension
+            ("model", Dolmen_model.Ext.name e)
+        in
+        Ok (add_model_extension e st)
+    )
     | Dune_plugin plugin ->
-      Dolmen.Sites.Plugins.Plugins.load plugin;
-      try
-        Ok (Dolmen_model.Ext.find_exn ext.extension_name)
-      with Not_found ->
-        Fmt.error_msg
-          "Plugin '%s' did not register a model extension for '%s'"
-          plugin ext.extension_name
+      Result.bind (load_plugin_or_fail plugin) @@ fun () ->
+      match Dolmen_model.Ext.find_all ext.extension_name with
+      | [] ->
+        Ok (
+          Loop.State.warn st
+            missing_extension
+            ("model", ext.extension_name, plugin)
+        )
+      | [ e ] ->
+        Ok (add_model_extension e st)
+      | e :: _ ->
+        let st =
+          Loop.State.warn st
+            duplicate_extension
+            ("model", ext.extension_name, plugin)
+        in
+        Ok (add_model_extension e st)
 
 let parse s =
   match parse_ext_opt s with

src/bin/extensions.mli

@@ -6,15 +6,15 @@ val name : t -> string
 (** Returns the name of the extension. *)
 
 val load_typing_extension :
-  t -> (Dolmen_loop.Typer.Ext.t, [> `Msg of string]) result
+  t -> Loop.State.t -> (Loop.State.t, [> `Msg of string]) result
 (** [load_typing_extension e] loads and returns the typing extension associated
     with [e].
 
-    Fails if [e] has no typing extension, or an error occurs during loading of
+    Fails if an error occurs during loading of
     an external typing extension. *)
 
 val load_model_extension :
-  t -> (Dolmen_model.Ext.t, [> `Msg of string]) result
+  t -> Loop.State.t -> (Loop.State.t, [> `Msg of string]) result
 (** [load_model_extension e] loads and returns the model extension associated
     with [e].
 

src/bin/options.ml

@@ -378,36 +378,8 @@ let mk_run_state
   let () = if gc then at_exit (fun () -> Gc.print_stat stdout;) in
   let () = if abort_on_bug then Dolmen_loop.Code.abort Dolmen_loop.Code.bug in
   let () = Hints.model ~check_model (* ~check_model_mode *) in
-  (* Extensions *)
-  let typing_exts =
-    List.fold_left (fun typing_exts (ext, kind) ->
-      Result.bind typing_exts @@ fun typing_exts ->
-      match kind with
-      | None | Some Extensions.Typing ->
-        Result.map
-          (fun e -> e :: typing_exts)
-          (Extensions.load_typing_extension ext)
-      | Some _ -> Ok typing_exts
-    ) (Ok []) extensions
-  in
-  Result.bind typing_exts @@ fun typing_extension_builtins ->
-  let model_exts =
-    if check_model then
-      List.fold_left (fun model_exts (ext, kind) ->
-        Result.bind model_exts @@ fun model_exts ->
-        match kind with
-        | None | Some Extensions.Model ->
-          Result.map
-            (fun e -> e :: model_exts)
-            (Extensions.load_model_extension ext)
-        | Some _ -> Ok model_exts
-      ) (Ok []) extensions
-    else
-      Ok []
-  in
-  Result.bind model_exts @@ fun model_extension_builtins ->
   (* State creation *)
-  Ok (
+  let st =
     Loop.State.empty
     |> Loop.State.init
       ~bt ~debug ~report_style ~reports
@@ -418,17 +390,34 @@ let mk_run_state
       ~interactive_prompt:Loop.Parser.interactive_prompt_lang
     |> Loop.Typer.init
       ~smtlib2_forced_logic
-      ~extension_builtins:typing_extension_builtins
     |> Loop.Typer_Pipe.init ~type_check
     |> Loop.Check.init
-      ~check_model ~extension_builtins:model_extension_builtins
+      ~check_model
       (* ~check_model_mode *)
     |> Loop.Flow.init ~flow_check
     |> Loop.Header.init
       ~header_check
       ~header_licenses
       ~header_lang_version
-  )
+  in
+  (* Extensions *)
+  let st =
+    List.fold_left (fun st (ext, kind) ->
+      match kind with
+      | None | Some Extensions.Typing ->
+        Result.bind st (Extensions.load_typing_extension ext)
+      | Some _ -> st
+    ) (Ok st) extensions
+  in
+  if check_model then
+    List.fold_left (fun st (ext, kind) ->
+      match kind with
+      | None | Some Extensions.Model ->
+        Result.bind st (Extensions.load_model_extension ext)
+      | Some _ -> st
+    ) st extensions
+  else
+    st
 
 (* Profiling *)
 (* ************************************************************************* *)

src/loop/report.mli

@@ -43,7 +43,6 @@ module T : sig
 
   val doc : [< t ] -> (Format.formatter -> unit)
   (** documentation for a report. *)
-
 end
 
 

src/loop/typer.ml

@@ -83,17 +83,22 @@ module Ext = struct
     builtins : Typer_intf.lang -> T.builtin_symbols;
   }
 
-  let all = Hashtbl.create 17
-  let list () =
-    List.fast_sort (fun e e' -> String.compare e.name e'.name) @@
-    Hashtbl.fold (fun _ e acc -> e :: acc) all []
-  let find_exn = Hashtbl.find all
   let name { name; _ } = name
   let builtins { builtins; _ } = builtins
 
+  let registry = Hashtbl.create 17
+
+  let register ({ name; _ } as ext)  =
+    match Hashtbl.find registry name with
+    | exception Not_found -> Hashtbl.replace registry name [ ext ]
+    | exts -> Hashtbl.replace registry name (ext :: exts)
+
+  let find_all name =
+    try Hashtbl.find registry name with Not_found -> []
+
   let create ~name ~builtins =
-    let t = { name; builtins; } in
-    Hashtbl.replace all name t;
+    let t = { name ; builtins } in
+    register t;
     t
 
   let bvconv =

src/loop/typer.mli

@@ -64,14 +64,10 @@ module Ext : sig
   val bvconv : t
   (** Typing extension to add `bv2nat` and `int2bv`. *)
 
-  val list : unit -> t list
-  (** The list of all extensions. *)
+  val find_all : string -> t list
+  (** Returns the extensions that have been registered with the given name.
 
-  val find_exn : string -> t
-  (** Returns the typing extension with the given name.
-
-     @raise Not_found if no such extension exists.
-     @since 0.11 *)
+      @since 0.11 *)
 end
 
 (** {2 Typechecker Functor} *)

src/model/ext.ml

@@ -8,17 +8,22 @@ type t = {
   builtins : Env.builtins;
 }
 
-let all = Hashtbl.create 17
-let list () =
-  List.fast_sort (fun e e' -> String.compare e.name e'.name) @@
-  Hashtbl.fold (fun _ e acc -> e :: acc) all []
-let find_exn = Hashtbl.find all
 let name { name; _ } = name
 let builtins { builtins; _ } = builtins
 
+let registry = Hashtbl.create 17
+
+let register ({ name; _ } as ext)  =
+  match Hashtbl.find registry name with
+  | exception Not_found -> Hashtbl.replace registry name [ ext ]
+  | exts -> Hashtbl.replace registry name (ext :: exts)
+
+let find_all name =
+  try Hashtbl.find registry name with Not_found -> []
+
 let create ~name ~builtins =
-  let t = { name; builtins; } in
-  Hashtbl.replace all name t;
+  let t = { name ; builtins } in
+  register t;
   t
 
 let bvconv =