Add support for including extra SMT files

Add --smt-include which inserts additional smtlib2 files into the output. This is can be used to define external functions for the SMT backend.

src/lib/util.ml

@@ -364,6 +364,13 @@ let same_content_files file1 file2 : bool =
        result
      end
 
+let read_whole_file filename =
+  (* open_in_bin works correctly on Unix and Windows *)
+  let ch = open_in_bin filename in
+  let s = really_input_string ch (in_channel_length ch) in
+  close_in ch;
+  s
+
 (*String formatting *)
 let rec string_of_list sep string_of = function
   | [] -> ""

src/lib/util.mli

@@ -178,7 +178,7 @@ val map_if : ('a -> bool) -> ('a -> 'a) -> 'a list -> 'a list
 val map_exists : ('b -> bool) -> ('a -> 'b) -> 'a list -> bool
 
 (** [list_to_front i l] resorts the list [l] by bringing the element at index [i]
-    to the front. 
+    to the front.
     @throws Failure if [i] is not smaller than the length of [l]*)
 val list_to_front : int -> 'a list -> 'a list
 
@@ -246,6 +246,9 @@ If at least one of the files does not exist, [false] is returned. [same_content_
 if one of the files exists, but cannot be read. *)
 val same_content_files : string -> string -> bool
 
+(** [read_whole_file filename] reads the contents of the file and returns it as a string. *)
+val read_whole_file : string -> string
+
 (** {2 Strings} *)
 
 (** [string_to_list l] translates the string [l] to the list of its characters. *)

src/sail_smt_backend/jib_smt.ml

@@ -2218,7 +2218,7 @@ let smt_instr_list name ctx all_cdefs instrs =
 
   (stack, start, cfg)
 
-let smt_cdef props lets name_file ctx all_cdefs = function
+let smt_cdef props lets name_file ctx all_cdefs smt_includes = function
   | CDEF_val (function_id, _, arg_ctyps, ret_ctyp) when Bindings.mem function_id props -> begin
       match find_function [] function_id all_cdefs with
       | intervening_lets, Some (None, args, instrs) ->
@@ -2267,6 +2267,9 @@ let smt_cdef props lets name_file ctx all_cdefs = function
             )
             header;
 
+          (* Include custom SMT definitions. *)
+          List.iter (fun include_file -> output_string out_chan (Util.read_whole_file include_file)) smt_includes;
+
           let queue = Queue_optimizer.optimize stack in
           Queue.iter
             (fun def ->
@@ -2295,13 +2298,13 @@ let smt_cdef props lets name_file ctx all_cdefs = function
     end
   | _ -> ()
 
-let rec smt_cdefs props lets name_file ctx ast = function
+let rec smt_cdefs props lets name_file ctx ast smt_includes = function
   | CDEF_let (_, vars, setup) :: cdefs ->
       let vars = List.map (fun (id, ctyp) -> idecl (id_loc id) ctyp (name id)) vars in
-      smt_cdefs props (lets @ vars @ setup) name_file ctx ast cdefs
+      smt_cdefs props (lets @ vars @ setup) name_file ctx ast smt_includes cdefs
   | cdef :: cdefs ->
-      smt_cdef props lets name_file ctx ast cdef;
-      smt_cdefs props lets name_file ctx ast cdefs
+      smt_cdef props lets name_file ctx ast smt_includes cdef;
+      smt_cdefs props lets name_file ctx ast smt_includes cdefs
   | [] -> ()
 
 (* In order to support register references, we need to build a map
@@ -2352,8 +2355,8 @@ let deserialize_smt_model file =
   close_in in_chan;
   (cdefs, { (initial_ctx ()) with tc_env = env; register_map = rmap })
 
-let generate_smt props name_file env effect_info ast =
+let generate_smt props name_file env effect_info smt_includes ast =
   try
     let cdefs, _, ctx = compile env effect_info ast in
-    smt_cdefs props [] name_file ctx cdefs cdefs
+    smt_cdefs props [] name_file ctx cdefs smt_includes cdefs
   with Type_error.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))

src/sail_smt_backend/jib_smt.mli

@@ -179,5 +179,6 @@ val generate_smt :
   (* Applied to each function name to generate the file name for the smtlib file *)
   Type_check.Env.t ->
   Effects.side_effect_info ->
+  string list ->
   Type_check.tannot ast ->
   unit

src/sail_smt_backend/sail_plugin_smt.ml

@@ -67,9 +67,11 @@
 
 open Libsail
 
+let opt_includes_smt : string list ref = ref []
+
 let smt_options =
   [
-    ("-smt_auto", Arg.Tuple [Arg.Set Jib_smt.opt_auto], " generate SMT and automatically call the CVC4 solver");
+    ("-smt_auto", Arg.Tuple [Arg.Set Jib_smt.opt_auto], " generate SMT and automatically call the CVC5 solver");
     ("-smt_ignore_overflow", Arg.Set Jib_smt.opt_ignore_overflow, " ignore integer overflow in generated SMT");
     ("-smt_propagate_vars", Arg.Set Jib_smt.opt_propagate_vars, " propgate variables through generated SMT");
     ( "-smt_int_size",
@@ -84,6 +86,10 @@ let smt_options =
       Arg.String (fun n -> Jib_smt.opt_default_vector_index := int_of_string n),
       "<n> set a bound of 2 ^ n for generic vectors in generated SMT (default 5)"
     );
+    ( "-smt_include",
+      Arg.String (fun i -> opt_includes_smt := i :: !opt_includes_smt),
+      "<filename> insert additional file in SMT output"
+    );
   ]
 
 let smt_rewrites =
@@ -132,6 +138,6 @@ let smt_target _ _ out_file ast effect_info env =
     match out_file with Some f -> fun str -> f ^ "_" ^ str ^ ".smt2" | None -> fun str -> str ^ ".smt2"
   in
   Reporting.opt_warnings := true;
-  Jib_smt.generate_smt props name_file env effect_info ast_smt
+  Jib_smt.generate_smt props name_file env effect_info !opt_includes_smt ast_smt
 
 let _ = Target.register ~name:"smt" ~options:smt_options ~rewrites:smt_rewrites smt_target