summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/jib/jib_smt.ml127
-rw-r--r--src/jib/jib_smt.mli113
-rw-r--r--src/property.ml11
-rw-r--r--src/property.mli4
-rw-r--r--src/sail.ml3
-rw-r--r--src/smtlib.ml158
6 files changed, 319 insertions, 97 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 4fbfa589..0f78f5bf 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -69,32 +69,26 @@ let opt_auto = ref false
let opt_debug_graphs = ref false
+let opt_propagate_vars = ref false
+
module EventMap = Map.Make(Event)
(* Note that we have to use x : ty ref rather than mutable x : ty, to
make sure { ctx with x = ... } doesn't break the mutable state. *)
+(* See mli file for a description of each field *)
type ctx = {
- (* Arbitrary-precision bitvectors are represented as a (BitVec lbits_index, BitVec (2 ^ lbits_index)) pair. *)
lbits_index : int;
- (* The size we use for integers where we don't know how large they are statically. *)
lint_size : int;
- (* A generic vector, vector('a) becomes Array (BitVec vector_index) 'a.
- We need to take care that vector_index is large enough for all generic vectors. *)
vector_index : int;
register_map : id list CTMap.t;
- (* Keep track of all the tuple sizes we need to genenerate types for *)
tuple_sizes : IntSet.t ref;
tc_env : Type_check.Env.t;
pragma_l : Ast.l;
arg_stack : (int * string) Stack.t;
ast : Type_check.tannot defs;
events : smt_exp Stack.t EventMap.t ref;
- (* When generating SMT for an instruction pathcond will contain
- the global path conditional of the containing block in the
- control flow graph *)
pathcond : smt_exp Lazy.t;
- (* Set if we need to use strings *)
use_string : bool ref;
use_real : bool ref
}
@@ -1028,16 +1022,16 @@ let writes = ref (-1)
let builtin_write_mem ctx wk addr_size addr data_size data =
incr writes;
let name = "W" ^ string_of_int !writes in
- [Write_mem (name, smt_cval ctx wk, smt_cval ctx addr, smt_cval ctx data)],
- Var name
+ [Write_mem (name, smt_cval ctx wk, smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr), smt_cval ctx data, smt_ctyp ctx (cval_ctyp data))],
+ Var (name ^ "_ret")
let reads = ref (-1)
let builtin_read_mem ctx rk addr_size addr data_size ret_ctyp =
incr reads;
let name = "R" ^ string_of_int !reads in
- [Read_mem (name, smt_ctyp ctx ret_ctyp, smt_cval ctx rk, smt_cval ctx addr)],
- Var name
+ [Read_mem (name, smt_ctyp ctx ret_ctyp, smt_cval ctx rk, smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr))],
+ Var (name ^ "_ret")
let rec smt_conversion ctx from_ctyp to_ctyp x =
match from_ctyp, to_ctyp with
@@ -1596,10 +1590,10 @@ let optimize_smt stack =
end
| (Declare_datatypes _ | Declare_tuple _) as def ->
Stack.push def stack'
- | Write_mem (_, wk, addr, data) as def ->
+ | Write_mem (_, wk, addr, _, data, _) as def ->
uses_in_exp wk; uses_in_exp addr; uses_in_exp data;
Stack.push def stack'
- | Read_mem (_, _, rk, addr) as def ->
+ | Read_mem (_, _, rk, addr, _) as def ->
uses_in_exp rk; uses_in_exp addr;
Stack.push def stack'
| Assert exp as def ->
@@ -1616,17 +1610,21 @@ let optimize_smt stack =
| Declare_const _ as def ->
Queue.add def queue
| Define_const (var, typ, exp) ->
- begin match Hashtbl.find_opt uses var with
- | Some 1 ->
+ begin match Hashtbl.find_opt uses var, simp_smt_exp vars exp with
+ | _, (Bin _ | Bool_lit _) ->
Hashtbl.add vars var exp
- | Some _ ->
- Queue.add (Define_const (var, typ, simp_smt_exp vars exp)) queue
- | None -> assert false
+ | _, Var _ when !opt_propagate_vars ->
+ Hashtbl.add vars var exp
+ | Some 1, _ ->
+ Hashtbl.add vars var exp
+ | Some _, exp ->
+ Queue.add (Define_const (var, typ, exp)) queue
+ | None, _ -> assert false
end
- | Write_mem (name, wk, addr, data) ->
- Queue.add (Write_mem (name, simp_smt_exp vars wk, simp_smt_exp vars addr, simp_smt_exp vars data)) queue
- | Read_mem (name, typ, rk, addr) ->
- Queue.add (Read_mem (name, typ, simp_smt_exp vars rk, simp_smt_exp vars addr)) queue
+ | Write_mem (name, wk, addr, addr_ty, data, data_ty) ->
+ Queue.add (Write_mem (name, simp_smt_exp vars wk, simp_smt_exp vars addr, addr_ty, simp_smt_exp vars data, data_ty)) queue
+ | Read_mem (name, typ, rk, addr, addr_typ) ->
+ Queue.add (Read_mem (name, typ, simp_smt_exp vars rk, simp_smt_exp vars addr, addr_typ)) queue
| Assert exp ->
Queue.add (Assert (simp_smt_exp vars exp)) queue
| (Declare_datatypes _ | Declare_tuple _) as def ->
@@ -1653,15 +1651,15 @@ let smt_header ctx cdefs =
checks if r is any one of the registers with type t, and reads that
register if it is. We also do a similar thing for *r = x
*)
-let expand_reg_deref ctx = function
+let expand_reg_deref env register_map = function
| I_aux (I_funcall (clexp, false, function_id, [reg_ref]), (_, l)) as instr ->
let open Type_check in
- begin match (if Env.is_extern function_id ctx.tc_env "smt" then Some (Env.get_extern function_id ctx.tc_env "smt") else None) with
+ begin match (if Env.is_extern function_id env "smt" then Some (Env.get_extern function_id env "smt") else None) with
| Some "reg_deref" ->
begin match cval_ctyp reg_ref with
| CT_ref reg_ctyp ->
(* Not find all the registers with this ctyp *)
- begin match CTMap.find_opt reg_ctyp ctx.register_map with
+ begin match CTMap.find_opt reg_ctyp register_map with
| Some regs ->
let end_label = label "end_reg_deref_" in
let try_reg r =
@@ -1683,7 +1681,7 @@ let expand_reg_deref ctx = function
| I_aux (I_copy (CL_addr (CL_id (id, ctyp)), cval), (_, l)) ->
begin match ctyp with
| CT_ref reg_ctyp ->
- begin match CTMap.find_opt reg_ctyp ctx.register_map with
+ begin match CTMap.find_opt reg_ctyp register_map with
| Some regs ->
let end_label = label "end_reg_write_" in
let try_reg r =
@@ -1716,12 +1714,43 @@ let rec smt_query ctx = function
| Q_or qs ->
Fn ("or", List.map (smt_query ctx) qs)
-let dump_graph function_id cfg =
- let gv_file = string_of_id function_id ^ ".gv" in
+let dump_graph name cfg =
+ let gv_file = name ^ ".gv" in
let out_chan = open_out gv_file in
Jib_ssa.make_dot out_chan cfg;
close_out out_chan
+let smt_instr_list name ctx all_cdefs instrs =
+ let stack = Stack.create () in
+
+ let open Jib_ssa in
+ let start, cfg = ssa instrs in
+ let visit_order =
+ try topsort cfg with
+ | Not_a_DAG n ->
+ dump_graph name cfg;
+ raise (Reporting.err_general ctx.pragma_l
+ (Printf.sprintf "%s: control flow graph is not acyclic (node %d is in cycle)\nWrote graph to %s.gv" name n name))
+ in
+ if !opt_debug_graphs then
+ dump_graph name cfg;
+
+ List.iter (fun n ->
+ begin match get_vertex cfg n with
+ | None -> ()
+ | Some ((ssanodes, cfnode), preds, succs) ->
+ let muxers =
+ ssanodes |> List.map (smt_ssanode ctx cfg preds) |> List.concat
+ in
+ let ctx = { ctx with pathcond = lazy (get_pathcond n cfg ctx) } in
+ let basic_block = smt_cfnode all_cdefs ctx ssanodes cfnode in
+ push_smt_defs stack muxers;
+ push_smt_defs stack basic_block;
+ end
+ ) visit_order;
+
+ stack
+
let smt_cdef props lets name_file ctx all_cdefs = function
| CDEF_spec (function_id, arg_ctyps, ret_ctyp) when Bindings.mem function_id props ->
begin match find_function [] function_id all_cdefs with
@@ -1730,8 +1759,6 @@ let smt_cdef props lets name_file ctx all_cdefs = function
let pragma = parse_pragma pragma_l prop_args in
- let stack = Stack.create () in
-
let ctx = { ctx with events = ref EventMap.empty; pragma_l = pragma_l; arg_stack = Stack.create () } in
(* When we create each argument declaration, give it a unique
@@ -1743,41 +1770,13 @@ let smt_cdef props lets name_file ctx all_cdefs = function
let open Jib_optimize in
(lets @ intervening_lets @ arg_decls @ instrs)
|> inline all_cdefs (fun _ -> true)
- |> List.map (map_instr (expand_reg_deref ctx))
+ |> List.map (map_instr (expand_reg_deref ctx.tc_env ctx.register_map))
|> flatten_instrs
|> remove_unused_labels
|> remove_pointless_goto
in
- (* let str = Pretty_print_sail.to_string PPrint.(separate_map hardline Jib_util.pp_instr instrs) in
- prerr_endline str; *)
-
- let open Jib_ssa in
- let start, cfg = ssa instrs in
- let visit_order =
- try topsort cfg with
- | Not_a_DAG n ->
- dump_graph function_id cfg;
- raise (Reporting.err_general pragma_l
- (Printf.sprintf "$%s %s: control flow graph is not acyclic (node %d is in cycle)\nWrote graph to %s.gv"
- prop_type (string_of_id function_id) n (string_of_id function_id)))
- in
- if !opt_debug_graphs then
- dump_graph function_id cfg;
-
- List.iter (fun n ->
- begin match get_vertex cfg n with
- | None -> ()
- | Some ((ssanodes, cfnode), preds, succs) ->
- let muxers =
- ssanodes |> List.map (smt_ssanode ctx cfg preds) |> List.concat
- in
- let ctx = { ctx with pathcond = lazy (get_pathcond n cfg ctx) } in
- let basic_block = smt_cfnode all_cdefs ctx ssanodes cfnode in
- push_smt_defs stack muxers;
- push_smt_defs stack basic_block;
- end
- ) visit_order;
+ let stack = smt_instr_list (string_of_id function_id) ctx all_cdefs instrs in
let query = smt_query ctx pragma.query in
push_smt_defs stack [Assert (Fn ("not", [query]))];
@@ -1794,10 +1793,10 @@ let smt_cdef props lets name_file ctx all_cdefs = function
else
output_string out_chan "(set-logic QF_AUFBVDT)\n";
- List.iter (fun def -> output_string out_chan (string_of_smt_def "" def); output_string out_chan "\n") header;
+ List.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") header;
let queue = optimize_smt stack in
- Queue.iter (fun def -> output_string out_chan (string_of_smt_def "" def); output_string out_chan "\n") queue;
+ Queue.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") queue;
output_string out_chan "(check-sat)\n";
if prop_type = "counterexample" then
diff --git a/src/jib/jib_smt.mli b/src/jib/jib_smt.mli
new file mode 100644
index 00000000..f9f42ff5
--- /dev/null
+++ b/src/jib/jib_smt.mli
@@ -0,0 +1,113 @@
+(**************************************************************************)
+(* Sail *)
+(* *)
+(* Copyright (c) 2013-2017 *)
+(* Kathyrn Gray *)
+(* Shaked Flur *)
+(* Stephen Kell *)
+(* Gabriel Kerneis *)
+(* Robert Norton-Wright *)
+(* Christopher Pulte *)
+(* Peter Sewell *)
+(* Alasdair Armstrong *)
+(* Brian Campbell *)
+(* Thomas Bauereiss *)
+(* Anthony Fox *)
+(* Jon French *)
+(* Dominic Mulligan *)
+(* Stephen Kell *)
+(* Mark Wassell *)
+(* *)
+(* All rights reserved. *)
+(* *)
+(* This software was developed by the University of Cambridge Computer *)
+(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
+(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
+(* *)
+(* Redistribution and use in source and binary forms, with or without *)
+(* modification, are permitted provided that the following conditions *)
+(* are met: *)
+(* 1. Redistributions of source code must retain the above copyright *)
+(* notice, this list of conditions and the following disclaimer. *)
+(* 2. Redistributions in binary form must reproduce the above copyright *)
+(* notice, this list of conditions and the following disclaimer in *)
+(* the documentation and/or other materials provided with the *)
+(* distribution. *)
+(* *)
+(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
+(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
+(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
+(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
+(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
+(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
+(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
+(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
+(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
+(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
+(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
+(* SUCH DAMAGE. *)
+(**************************************************************************)
+
+open Ast
+open Ast_util
+open Jib
+open Jib_util
+open Smtlib
+
+val opt_ignore_overflow : bool ref
+val opt_auto : bool ref
+val opt_debug_graphs : bool ref
+val opt_propagate_vars : bool ref
+
+module IntSet : Set.S with type elt = int
+module EventMap : Map.S with type key = Property.event
+
+val opt_default_lint_size : int ref
+val opt_default_lbits_index : int ref
+val opt_default_vector_index : int ref
+
+type ctx = {
+ (** Arbitrary-precision bitvectors are represented as a (BitVec lbits_index, BitVec (2 ^ lbits_index)) pair. *)
+ lbits_index : int;
+ (** The size we use for integers where we don't know how large they are statically. *)
+ lint_size : int;
+ (** A generic vector, vector('a) becomes Array (BitVec vector_index) 'a.
+ We need to take care that vector_index is large enough for all generic vectors. *)
+ vector_index : int;
+ (** A map from each ctyp to a list of registers of that ctyp *)
+ register_map : id list CTMap.t;
+ (** A set to keep track of all the tuple sizes we need to generate types for *)
+ tuple_sizes : IntSet.t ref;
+ (** tc_env is the global type-checking environment *)
+ tc_env : Type_check.Env.t;
+ (** A location, usually the $counterexample or $property we are
+ generating the SMT for. Used for error messages. *)
+ pragma_l : Ast.l;
+ (** Used internally to keep track of function argument names *)
+ arg_stack : (int * string) Stack.t;
+ (** The fully type-checked ast *)
+ ast : Type_check.tannot defs;
+ (** For every event type we have a stack of boolean SMT
+ expressions for each occurance of that event. See
+ src/property.ml for the event types *)
+ events : smt_exp Stack.t EventMap.t ref;
+ (** When generating SMT for an instruction pathcond will contain
+ the global path conditional of the containing block in the
+ control flow graph *)
+ pathcond : smt_exp Lazy.t;
+ (** Set if we need to use strings or real numbers in the generated
+ SMT, which then requires set-logic ALL or similar depending on
+ the solver *)
+ use_string : bool ref;
+ use_real : bool ref
+ }
+
+val smt_instr_list : string -> ctx -> cdef list -> instr list -> smt_def Stack.t
+
+(** Generate SMT for all the $property and $counterexample pragmas in an AST *)
+val generate_smt :
+ (string * string * l * 'a val_spec) Bindings.t
+ -> (string -> string)
+ -> Type_check.Env.t
+ -> Type_check.tannot defs
+ -> unit
diff --git a/src/property.ml b/src/property.ml
index 8dbc31fe..955e755d 100644
--- a/src/property.ml
+++ b/src/property.ml
@@ -199,11 +199,13 @@ let parse_query =
parse (exp0 ()) "[ \n\t]+\\|(\\|)\\|&\\||\\|~"
type pragma = {
- query : query
+ query : query;
+ litmus : string list;
}
let default_pragma = {
- query = default_query
+ query = default_query;
+ litmus = [];
}
let parse_pragma l input =
@@ -212,10 +214,13 @@ let parse_pragma l input =
let rec process_toks pragma = function
| Str.Delim ":query" :: Str.Text query :: rest ->
begin match parse_query query with
- | Some q -> process_toks { query = q } rest
+ | Some q -> process_toks { pragma with query = q } rest
| None ->
raise (Reporting.err_general l ("Could not parse query " ^ String.trim query))
end
+ | Str.Delim ":litmus" :: rest ->
+ let args, rest = Util.take_drop (function Str.Text _ -> true | _ -> false) rest in
+ process_toks { pragma with litmus = List.map (function Str.Text t -> t | _ -> assert false) args } rest
| [] -> pragma
| _ ->
raise (Reporting.err_general l "Could not parse pragma")
diff --git a/src/property.mli b/src/property.mli
index f84a85e3..8005f91a 100644
--- a/src/property.mli
+++ b/src/property.mli
@@ -105,8 +105,8 @@ type query =
| Q_or of query list
type pragma = {
- query : query
+ query : query;
+ litmus : string list;
}
val parse_pragma : Parse_ast.l -> string -> pragma
-
diff --git a/src/sail.ml b/src/sail.ml
index 65be5474..c4991fe5 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -149,6 +149,9 @@ let options = Arg.align ([
( "-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",
Arg.String (fun n -> Jib_smt.opt_default_lint_size := int_of_string n),
"<n> set a bound of n on the maximum integer bitwidth for generated SMT (default 128)");
diff --git a/src/smtlib.ml b/src/smtlib.ml
index ac8370e0..c6b86fcb 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -101,6 +101,14 @@ type smt_exp =
| Extract of int * int * smt_exp
| Tester of string * smt_exp
+let rec fold_smt_exp f = function
+ | Fn (name, args) -> f (Fn (name, List.map (fold_smt_exp f) args))
+ | Ite (cond, t, e) -> f (Ite (fold_smt_exp f cond, fold_smt_exp f t, fold_smt_exp f e))
+ | SignExtend (n, exp) -> f (SignExtend (n, fold_smt_exp f exp))
+ | Extract (n, m, exp) -> f (Extract (n, m, fold_smt_exp f exp))
+ | Tester (ctor, exp) -> f (Tester (ctor, fold_smt_exp f exp))
+ | (Bool_lit _ | Hex _ | Bin _ | Real_lit _ | String_lit _ | Var _ | Enum _ as exp) -> f exp
+
let smt_conj = function
| [] -> Bool_lit true
| [x] -> x
@@ -137,13 +145,47 @@ let bvones n =
else
Bin (String.concat "" (Util.list_init n (fun _ -> "1")))
+let simp_equal x y =
+ match x, y with
+ | Bin str1, Bin str2 -> Some (str1 = str2)
+ | _, _ -> None
+
+let simp_and xs =
+ let xs = List.filter (function Bool_lit true -> false | _ -> true) xs in
+ match xs with
+ | [] -> Bool_lit true
+ | [x] -> x
+ | _ ->
+ if List.exists (function Bool_lit false -> true | _ -> false) xs then
+ Bool_lit false
+ else
+ Fn ("and", xs)
+
+let simp_or xs =
+ let xs = List.filter (function Bool_lit false -> false | _ -> true) xs in
+ match xs with
+ | [] -> Bool_lit false
+ | [x] -> x
+ | _ ->
+ if List.exists (function Bool_lit true -> true | _ -> false) xs then
+ Bool_lit true
+ else
+ Fn ("or", xs)
+
let simp_fn = function
| Fn ("not", [Fn ("not", [exp])]) -> exp
| Fn ("not", [Bool_lit b]) -> Bool_lit (not b)
| Fn ("contents", [Fn ("Bits", [_; contents])]) -> contents
| Fn ("len", [Fn ("Bits", [len; _])]) -> len
- | Fn ("or", [x]) -> x
- | Fn ("and", [x]) -> x
+ | Fn ("or", xs) -> simp_or xs
+ | Fn ("and", xs) -> simp_and xs
+ | Fn ("=>", [Bool_lit true; y]) -> y
+ | Fn ("=>", [Bool_lit false; y]) -> Bool_lit true
+ | Fn ("=", [x; y]) as exp ->
+ begin match simp_equal x y with
+ | Some b -> Bool_lit b
+ | None -> exp
+ end
| exp -> exp
let simp_ite = function
@@ -171,7 +213,11 @@ let rec simp_smt_exp vars = function
simp_ite (Ite (cond, t, e))
| Extract (i, j, exp) ->
let exp = simp_smt_exp vars exp in
- Extract (i, j, exp)
+ begin match exp with
+ | Bin str ->
+ Bin (String.sub str ((String.length str - 1) - i) ((i + 1) - j))
+ | _ -> Extract (i, j, exp)
+ end
| Tester (str, exp) ->
let exp = simp_smt_exp vars exp in
Tester (str, exp)
@@ -183,8 +229,8 @@ type smt_def =
| Define_fun of string * (string * smt_typ) list * smt_typ * smt_exp
| Declare_const of string * smt_typ
| Define_const of string * smt_typ * smt_exp
- | Write_mem of string * smt_exp * smt_exp * smt_exp
- | Read_mem of string * smt_typ * smt_exp * smt_exp
+ | Write_mem of string * smt_exp * smt_exp * smt_typ * smt_exp * smt_typ
+ | Read_mem of string * smt_typ * smt_exp * smt_exp * smt_typ
| Declare_datatypes of string * (string * (string * smt_typ) list) list
| Declare_tuple of int
| Assert of smt_exp
@@ -193,13 +239,64 @@ let declare_datatypes = function
| Datatype (name, ctors) -> Declare_datatypes (name, ctors)
| _ -> assert false
+let suffix_variables_exp sfx =
+ fold_smt_exp (function Var v -> Var (v ^ sfx) | exp -> exp)
+
+let suffix_variables_def sfx = function
+ | Define_fun (name, args, ty, exp) ->
+ Define_fun (name ^ sfx, List.map (fun (arg, ty) -> sfx ^ arg, ty) args, ty, suffix_variables_exp sfx exp)
+ | Declare_const (name, ty) ->
+ Declare_const (name ^ sfx, ty)
+ | Define_const (name, ty, exp) ->
+ Define_const (name ^ sfx, ty, suffix_variables_exp sfx exp)
+ | Write_mem (name, wk, addr, addr_ty, data, data_ty) ->
+ Write_mem (name ^ sfx, suffix_variables_exp sfx wk, suffix_variables_exp sfx addr, addr_ty, suffix_variables_exp sfx data, data_ty)
+ | Read_mem (name, ty, rk, addr, addr_ty) ->
+ Read_mem (name ^ sfx, ty, suffix_variables_exp sfx rk, suffix_variables_exp sfx addr, addr_ty)
+ | Declare_datatypes (name, ctors) ->
+ Declare_datatypes (name, ctors)
+ | Declare_tuple n ->
+ Declare_tuple n
+ | Assert exp ->
+ Assert (suffix_variables_exp sfx exp)
+
+let merge_datatypes defs1 defs2 =
+ let module StringSet = Set.Make(String) in
+ let datatype_name = function
+ | Declare_datatypes (name, _) -> name
+ | _ -> assert false
+ in
+ let names = List.fold_left (fun set def -> StringSet.add (datatype_name def) set) StringSet.empty defs1 in
+ defs1 @ List.filter (fun def -> not (StringSet.mem (datatype_name def) names)) defs2
+
+let merge_tuples defs1 defs2 =
+ let tuple_size = function
+ | Declare_tuple size -> size
+ | _ -> assert false
+ in
+ let names = List.fold_left (fun set def -> Util.IntSet.add (tuple_size def) set) Util.IntSet.empty defs1 in
+ defs1 @ List.filter (fun def -> not (Util.IntSet.mem (tuple_size def) names)) defs2
+
+let merge_smt_defs defs1 defs2 =
+ let is_tuple = function
+ | Declare_datatypes _ | Declare_tuple _ -> true
+ | _ -> false
+ in
+ let is_datatype = function
+ | Declare_datatypes _ | Declare_tuple _ -> true
+ | _ -> false
+ in
+ let datatypes1, body1 = List.partition is_datatype defs1 in
+ let datatypes2, body2 = List.partition is_datatype defs2 in
+ let tuples1, datatypes1 = List.partition is_tuple datatypes1 in
+ let tuples2, datatypes2 = List.partition is_tuple datatypes2 in
+ merge_tuples tuples1 tuples2 @ merge_datatypes datatypes1 datatypes2 @ body1 @ body2
+
let pp_sfun str docs =
let open PPrint in
parens (separate space (string str :: docs))
-let prefix_string pre str = PPrint.string (pre ^ str)
-
-let rec pp_smt_exp pre =
+let rec pp_smt_exp =
let open PPrint in
function
| Bool_lit b -> string (string_of_bool b)
@@ -207,17 +304,17 @@ let rec pp_smt_exp pre =
| String_lit str -> string ("\"" ^ str ^ "\"")
| Hex str -> string ("#x" ^ str)
| Bin str -> string ("#b" ^ str)
- | Var str -> prefix_string pre str
+ | Var str -> string str
| Enum str -> string str
- | Fn (str, exps) -> parens (string str ^^ space ^^ separate_map space (pp_smt_exp pre) exps)
+ | Fn (str, exps) -> parens (string str ^^ space ^^ separate_map space pp_smt_exp exps)
| Ite (cond, then_exp, else_exp) ->
- parens (separate space [string "ite"; pp_smt_exp pre cond; pp_smt_exp pre then_exp; pp_smt_exp pre else_exp])
+ parens (separate space [string "ite"; pp_smt_exp cond; pp_smt_exp then_exp; pp_smt_exp else_exp])
| Extract (i, j, exp) ->
- parens (string (Printf.sprintf "(_ extract %d %d)" i j) ^^ space ^^ pp_smt_exp pre exp)
+ parens (string (Printf.sprintf "(_ extract %d %d)" i j) ^^ space ^^ pp_smt_exp exp)
| Tester (kind, exp) ->
- parens (string (Printf.sprintf "(_ is %s)" kind) ^^ space ^^ pp_smt_exp pre exp)
+ parens (string (Printf.sprintf "(_ is %s)" kind) ^^ space ^^ pp_smt_exp exp)
| SignExtend (i, exp) ->
- parens (string (Printf.sprintf "(_ sign_extend %d)" i) ^^ space ^^ pp_smt_exp pre exp)
+ parens (string (Printf.sprintf "(_ sign_extend %d)" i) ^^ space ^^ pp_smt_exp exp)
let rec pp_smt_typ =
let open PPrint in
@@ -232,27 +329,32 @@ let rec pp_smt_typ =
let pp_str_smt_typ (str, ty) = let open PPrint in string str ^^ space ^^ pp_smt_typ ty
-let pp_smt_def pre =
+let pp_smt_def =
let open PPrint in
let open Printf in
function
- | Define_fun (str, args, ty, exp) ->
- parens (string "define-fun"
+ | Define_fun (name, args, ty, exp) ->
+ parens (string "define-fun" ^^ space ^^ string name
^^ space ^^ parens (separate_map space pp_str_smt_typ args)
^^ space ^^ pp_smt_typ ty
- ^//^ pp_smt_exp pre exp)
+ ^//^ pp_smt_exp exp)
| Declare_const (name, ty) ->
- pp_sfun "declare-const" [prefix_string pre name; pp_smt_typ ty]
+ pp_sfun "declare-const" [string name; pp_smt_typ ty]
| Define_const (name, ty, exp) ->
- pp_sfun "define-const" [prefix_string pre name; pp_smt_typ ty; pp_smt_exp pre exp]
+ pp_sfun "define-const" [string name; pp_smt_typ ty; pp_smt_exp exp]
- | Write_mem (name, wk, addr, data) ->
- pp_sfun "declare-const" [prefix_string pre name; pp_smt_typ Bool]
+ | Write_mem (name, wk, addr, addr_ty, data, data_ty) ->
+ pp_sfun "define-const" [string (name ^ "_kind"); string "Zwrite_kind"; pp_smt_exp wk] ^^ hardline
+ ^^ pp_sfun "define-const" [string (name ^ "_data"); pp_smt_typ data_ty; pp_smt_exp data] ^^ hardline
+ ^^ pp_sfun "define-const" [string (name ^ "_addr"); pp_smt_typ addr_ty; pp_smt_exp addr] ^^ hardline
+ ^^ pp_sfun "declare-const" [string (name ^ "_ret"); pp_smt_typ Bool]
- | Read_mem (name, ty, rk, addr) ->
- pp_sfun "declare-const" [prefix_string pre name; pp_smt_typ ty]
+ | Read_mem (name, ty, rk, addr, addr_ty) ->
+ pp_sfun "define-const" [string (name ^ "_kind"); string "Zread_kind"; pp_smt_exp rk] ^^ hardline
+ ^^ pp_sfun "define-const" [string (name ^ "_addr"); pp_smt_typ addr_ty; pp_smt_exp addr] ^^ hardline
+ ^^ pp_sfun "declare-const" [string (name ^ "_ret"); pp_smt_typ ty]
| Declare_datatypes (name, ctors) ->
let pp_ctor (ctor_name, fields) =
@@ -275,12 +377,12 @@ let pp_smt_def pre =
parens (parens (ksprintf string "tup%d" n ^^ space ^^ fields))]))]
| Assert exp ->
- pp_sfun "assert" [pp_smt_exp pre exp]
+ pp_sfun "assert" [pp_smt_exp exp]
-let string_of_smt_def pre def = Pretty_print_sail.to_string (pp_smt_def pre def)
+let string_of_smt_def def = Pretty_print_sail.to_string (pp_smt_def def)
-let output_smt_defs out_chan pre smt =
- List.iter (fun def -> output_string out_chan (string_of_smt_def pre def ^ "\n")) smt
+let output_smt_defs out_chan smt =
+ List.iter (fun def -> output_string out_chan (string_of_smt_def def ^ "\n")) smt
(**************************************************************************)
(* 2. Parser for SMT solver output *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 09:01:48 +0000