Make sure we don't duplicate function definitions in repeated

specialization rounds

Also print a warning rather than exploding if a plugin can't be loaded
for whatever reason, and remove a rogue prerr_endline

src/bin/sail.ml

@@ -84,8 +84,12 @@ let rec fix_options = function
   | [] -> []
 
 let load_plugin opts plugin =
-  Dynlink.loadfile_private plugin;
-  opts := Arg.align (!opts @ fix_options (Target.extract_options ()))
+  try
+    Dynlink.loadfile_private plugin;
+    opts := Arg.align (!opts @ fix_options (Target.extract_options ()))
+  with
+  | Dynlink.Error _ ->
+     prerr_endline ("Failed to load plugin " ^ plugin)
 
 let version =
   let open Manifest in

src/lib/effects.ml

@@ -193,7 +193,7 @@ let infer_def_direct_effects asserts_termination def =
 
   let scan_pat p_aux annot =
     begin match p_aux with
-    | P_string_append _ -> (prerr_endline "NE"; effects := EffectSet.add NonExec !effects)
+    | P_string_append _ -> effects := EffectSet.add NonExec !effects
     | _ -> ()
     end;
     P_aux (p_aux, annot)

src/lib/jib_compile.ml

@@ -1623,8 +1623,11 @@ let callgraph cdefs =
 
 let mangle_mono_id id ctx ctyps =
   append_id id ("<" ^ Util.string_of_list "," (mangle_string_of_ctyp ctx) ctyps ^ ">")
-
-let rec specialize_functions ctx cdefs =
+
+(* The specialized calls argument keeps track of functions we have
+   already specialized, so we don't accidentally specialize them twice
+   in a future round of specialization *)
+let rec specialize_functions ?(specialized_calls=ref IdSet.empty) ctx cdefs =
   let polymorphic_functions =
     Util.map_filter (function
         | CDEF_spec (id, _, param_ctyps, ret_ctyp) ->
@@ -1659,11 +1662,15 @@ let rec specialize_functions ctx cdefs =
        let tyargs = List.fold_left (fun set ctyp -> KidSet.union (ctyp_vars ctyp) set) KidSet.empty (ret_ctyp :: param_ctyps) in
        spec_tyargs := Bindings.add id tyargs !spec_tyargs;
        let specialized_specs =
-         List.map (fun instantiation ->
-             let substs = List.fold_left2 (fun substs tyarg ty -> KBindings.add tyarg ty substs) KBindings.empty (KidSet.elements tyargs) instantiation in
-             let param_ctyps = List.map (subst_poly substs) param_ctyps in
-             let ret_ctyp = subst_poly substs ret_ctyp in
-             CDEF_spec (mangle_mono_id id ctx instantiation, extern, param_ctyps, ret_ctyp)
+         Util.map_filter (fun instantiation ->
+             let specialized_id = mangle_mono_id id ctx instantiation in
+             if not (IdSet.mem specialized_id !specialized_calls) then (
+               let substs = List.fold_left2 (fun substs tyarg ty -> KBindings.add tyarg ty substs) KBindings.empty (KidSet.elements tyargs) instantiation in
+               let param_ctyps = List.map (subst_poly substs) param_ctyps in
+               let ret_ctyp = subst_poly substs ret_ctyp in
+               Some (CDEF_spec (specialized_id, extern, param_ctyps, ret_ctyp))
+             ) else
+               None
            ) (CTListSet.elements (Bindings.find id !monomorphic_calls))
        in
        let ctx =
@@ -1678,10 +1685,15 @@ let rec specialize_functions ctx cdefs =
     | (CDEF_fundef (id, heap_return, params, body) as orig_cdef) :: cdefs when Bindings.mem id !monomorphic_calls ->
        let tyargs = Bindings.find id !spec_tyargs in
        let specialized_fundefs =
-         List.map (fun instantiation ->
-             let substs = List.fold_left2 (fun substs tyarg ty -> KBindings.add tyarg ty substs) KBindings.empty (KidSet.elements tyargs) instantiation in
-             let body = List.map (map_instr_ctyp (subst_poly substs)) body in
-             CDEF_fundef (mangle_mono_id id ctx instantiation, heap_return, params, body)
+         Util.map_filter (fun instantiation ->
+             let specialized_id = mangle_mono_id id ctx instantiation in
+             if not (IdSet.mem specialized_id !specialized_calls) then (
+               specialized_calls := IdSet.add specialized_id !specialized_calls;
+               let substs = List.fold_left2 (fun substs tyarg ty -> KBindings.add tyarg ty substs) KBindings.empty (KidSet.elements tyargs) instantiation in
+               let body = List.map (map_instr_ctyp (subst_poly substs)) body in
+               Some (CDEF_fundef (specialized_id, heap_return, params, body))
+             ) else
+               None
            ) (CTListSet.elements (Bindings.find id !monomorphic_calls))
        in
        specialize_fundefs ctx (orig_cdef :: specialized_fundefs @ prior) cdefs
@@ -1723,7 +1735,7 @@ let rec specialize_functions ctx cdefs =
   if IdSet.is_empty (IdSet.diff polymorphic_functions unreachable_polymorphic_functions) then
     cdefs, ctx
   else
-    specialize_functions ctx cdefs
+    specialize_functions ~specialized_calls:specialized_calls ctx cdefs
 
 let map_structs_and_variants f = function
   | (CT_lint | CT_fint _ | CT_constant _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit

test/c/fail_issue203.err_expect

@@ -0,0 +1 @@
+Assertion failed: fail_issue203.sail:29: message 1

test/c/fail_issue203.sail

@@ -0,0 +1,31 @@
+default Order dec
+
+$include <prelude.sail>
+
+infixr 5 ^^
+
+overload operator ^^ = {concat_str}
+
+union exception = {
+    Error_internal_error : unit
+}
+
+val internal_error : forall ('a : Type). (string, int, string) -> 'a
+
+function internal_error(file, line, s) = {
+    assert (false, file ^^ ":" ^^ dec_str(line) ^^ ": " ^^ s);
+    throw Error_internal_error()
+}
+
+val internal_error_caller : forall ('a : Type). (string, int, string) -> 'a
+
+function internal_error_caller(f , l, k) -> 'a = {
+    internal_error(f, l, k);
+}
+
+val main : unit -> unit
+
+function main() = {
+    internal_error_caller(__FILE__, __LINE__, "message 1");
+    internal_error(__FILE__, __LINE__, "message 2");
+}