From e01b960c38f5e146140487916de3172f495108a6 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Mon, 19 Feb 2024 10:53:39 +0000 Subject: [PATCH] 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 | 7 +++++++ src/lib/util.mli | 5 ++++- src/sail_smt_backend/jib_smt.ml | 17 ++++++++++------- src/sail_smt_backend/jib_smt.mli | 1 + src/sail_smt_backend/sail_plugin_smt.ml | 10 ++++++++-- 5 files changed, 30 insertions(+), 10 deletions(-) diff --git a/src/lib/util.ml b/src/lib/util.ml index 18d1aa707..f7005bdf6 100644 --- a/src/lib/util.ml +++ b/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 | [] -> "" diff --git a/src/lib/util.mli b/src/lib/util.mli index 4e3df46a7..da7cffea2 100644 --- a/src/lib/util.mli +++ b/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. *) diff --git a/src/sail_smt_backend/jib_smt.ml b/src/sail_smt_backend/jib_smt.ml index d49af4972..7a9929c8b 100644 --- a/src/sail_smt_backend/jib_smt.ml +++ b/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)) diff --git a/src/sail_smt_backend/jib_smt.mli b/src/sail_smt_backend/jib_smt.mli index 35b5c4351..2f3f509da 100644 --- a/src/sail_smt_backend/jib_smt.mli +++ b/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 diff --git a/src/sail_smt_backend/sail_plugin_smt.ml b/src/sail_smt_backend/sail_plugin_smt.ml index bda7ecb76..079de23b1 100644 --- a/src/sail_smt_backend/sail_plugin_smt.ml +++ b/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), " 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), + " 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