From d58e9c73731b969ebfb8e098dc5ea60d61747d79 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 21 May 2019 15:08:46 +0100 Subject: SMT: Add control flow node numbers to memory events to track program order Add path conditions to memory events Allow simplication of generated SMT based on constructor kinds --- src/jib/jib_smt.ml | 97 +++++++++++++++++++++++++++++++---------------------- src/jib/jib_smt.mli | 6 ++-- src/jib/jib_ssa.mli | 2 +- src/smtlib.ml | 86 +++++++++++++++++++++++++++++------------------ 4 files changed, 116 insertions(+), 75 deletions(-) (limited to 'src') diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 897c685a..7420707c 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -88,6 +88,7 @@ type ctx = { arg_stack : (int * string) Stack.t; ast : Type_check.tannot defs; events : smt_exp Stack.t EventMap.t ref; + node : int; pathcond : smt_exp Lazy.t; use_string : bool ref; use_real : bool ref @@ -112,6 +113,7 @@ let initial_ctx () = { arg_stack = Stack.create (); ast = Defs []; events = ref EventMap.empty; + node = -1; pathcond = lazy (Bool_lit true); use_string = ref false; use_real = ref false; @@ -1022,7 +1024,8 @@ 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_ctyp ctx (cval_ctyp addr), smt_cval ctx data, smt_ctyp ctx (cval_ctyp data))], + [Write_mem (name, ctx.node, Lazy.force ctx.pathcond, 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 ea_writes = ref (-1) @@ -1030,7 +1033,8 @@ let ea_writes = ref (-1) let builtin_write_mem_ea ctx wk addr_size addr data_size = incr ea_writes; let name = "A" ^ string_of_int !ea_writes in - [Write_mem_ea (name, smt_cval ctx wk, smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr), smt_cval ctx data_size, smt_ctyp ctx (cval_ctyp data_size))], + [Write_mem_ea (name, ctx.node, Lazy.force ctx.pathcond, smt_cval ctx wk, + smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr), smt_cval ctx data_size, smt_ctyp ctx (cval_ctyp data_size))], Enum "unit" let reads = ref (-1) @@ -1038,7 +1042,8 @@ 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, smt_ctyp ctx (cval_ctyp addr))], + [Read_mem (name, ctx.node, Lazy.force ctx.pathcond, smt_ctyp ctx ret_ctyp, smt_cval ctx rk, + smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr))], Var (name ^ "_ret") let excl_results = ref (-1) @@ -1046,7 +1051,7 @@ let excl_results = ref (-1) let builtin_excl_res ctx = incr excl_results; let name = "E" ^ string_of_int !excl_results in - [Excl_res name], + [Excl_res (name, ctx.node, Lazy.force ctx.pathcond)], Var (name ^ "_ret") let barriers = ref (-1) @@ -1054,7 +1059,7 @@ let barriers = ref (-1) let builtin_barrier ctx bk = incr barriers; let name = "B" ^ string_of_int !barriers in - [Barrier (name, smt_cval ctx bk)], + [Barrier (name, ctx.node, Lazy.force ctx.pathcond, smt_cval ctx bk)], Enum "unit" let rec smt_conversion ctx from_ctyp to_ctyp x = @@ -1297,8 +1302,8 @@ let smt_ssanode ctx cfg preds = | Phi (id, ctyp, ids) -> let get_pi n = match get_vertex cfg n with - | Some ((ssanodes, _), _, _) -> - List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes) + | Some ((ssa_elems, _), _, _) -> + List.concat (List.map (function Pi guards -> guards | _ -> []) ssa_elems) | None -> failwith "Predecessor node does not exist" in let pis = List.map get_pi (IntSet.elements preds) in @@ -1362,8 +1367,8 @@ let rec get_pathcond n cfg ctx = let open Jib_ssa in let get_pi m = match get_vertex cfg m with - | Some ((ssanodes, _), _, _) -> - V_call (Band, List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes)) + | Some ((ssa_elems, _), _, _) -> + V_call (Band, List.concat (List.map (function Pi guards -> guards | _ -> []) ssa_elems)) | None -> failwith "Node does not exist" in match get_vertex cfg n with @@ -1535,7 +1540,7 @@ let smt_instr ctx = end else if not extern then let smt_args = List.map (smt_cval ctx) args in - [define_const ctx id ret_ctyp (Fn (zencode_id function_id, smt_args))] + [define_const ctx id ret_ctyp (Ctor (zencode_id function_id, smt_args))] else failwith ("Unrecognised function " ^ string_of_id function_id) @@ -1571,7 +1576,7 @@ let smt_instr ctx = | instr -> failwith ("Cannot translate: " ^ Pretty_print_sail.to_string (pp_instr instr)) -let smt_cfnode all_cdefs ctx ssanodes = +let smt_cfnode all_cdefs ctx ssa_elems = let open Jib_ssa in function | CF_start inits -> @@ -1622,7 +1627,7 @@ module Make_optimizer(S : Sequence) = struct | None -> Hashtbl.add uses var 1 end | Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> () - | Fn (f, exps) -> + | Fn (_, exps) | Ctor (_, exps) -> List.iter uses_in_exp exps | Ite (cond, t, e) -> uses_in_exp cond; uses_in_exp t; uses_in_exp e @@ -1646,19 +1651,20 @@ module Make_optimizer(S : Sequence) = struct end | (Declare_datatypes _ | Declare_tuple _) as def -> Stack.push def stack' - | Write_mem (_, wk, addr, _, data, _) as def -> - uses_in_exp wk; uses_in_exp addr; uses_in_exp data; + | Write_mem (_, _, active, wk, addr, _, data, _) as def -> + uses_in_exp active; uses_in_exp wk; uses_in_exp addr; uses_in_exp data; Stack.push def stack' - | Write_mem_ea (_, wk, addr, _, data_size, _) as def -> - uses_in_exp wk; uses_in_exp addr; uses_in_exp data_size; + | Write_mem_ea (_, _, active, wk, addr, _, data_size, _) as def -> + uses_in_exp active; uses_in_exp wk; uses_in_exp addr; uses_in_exp data_size; Stack.push def stack' - | Read_mem (_, _, rk, addr, _) as def -> - uses_in_exp rk; uses_in_exp addr; + | Read_mem (_, _, active, _, rk, addr, _) as def -> + uses_in_exp active; uses_in_exp rk; uses_in_exp addr; Stack.push def stack' - | Barrier (_, bk) as def -> - uses_in_exp bk; + | Barrier (_, _, active, bk) as def -> + uses_in_exp active; uses_in_exp bk; Stack.push def stack' - | Excl_res _ as def -> + | Excl_res (_, _, active) as def -> + uses_in_exp active; Stack.push def stack' | Assert exp as def -> uses_in_exp exp; @@ -1668,35 +1674,46 @@ module Make_optimizer(S : Sequence) = struct Stack.fold remove_unused () stack; let vars = Hashtbl.create (Stack.length stack') in + let kinds = Hashtbl.create (Stack.length stack') in let seq = S.create () in let constant_propagate = function | Declare_const _ as def -> S.add def seq | Define_const (var, typ, exp) -> - begin match Hashtbl.find_opt uses var, simp_smt_exp vars exp with + let exp = simp_smt_exp vars kinds exp in + begin match Hashtbl.find_opt uses var, simp_smt_exp vars kinds exp with | _, (Bin _ | Bool_lit _) -> Hashtbl.add vars var exp | _, Var _ when !opt_propagate_vars -> Hashtbl.add vars var exp + | _, (Ctor (str, _)) -> + Hashtbl.add kinds var str; + S.add (Define_const (var, typ, exp)) seq | Some 1, _ -> Hashtbl.add vars var exp | Some _, exp -> S.add (Define_const (var, typ, exp)) seq | None, _ -> assert false end - | Write_mem (name, wk, addr, addr_ty, data, data_ty) -> - S.add (Write_mem (name, simp_smt_exp vars wk, simp_smt_exp vars addr, addr_ty, simp_smt_exp vars data, data_ty)) seq - | Write_mem_ea (name, wk, addr, addr_ty, data_size, data_size_ty) -> - S.add (Write_mem_ea (name, simp_smt_exp vars wk, simp_smt_exp vars addr, addr_ty, simp_smt_exp vars data_size, data_size_ty)) seq - | Read_mem (name, typ, rk, addr, addr_typ) -> - S.add (Read_mem (name, typ, simp_smt_exp vars rk, simp_smt_exp vars addr, addr_typ)) seq - | Barrier (name, bk) -> - S.add (Barrier (name, simp_smt_exp vars bk)) seq - | Excl_res name -> - S.add (Excl_res name) seq + | Write_mem (name, node, active, wk, addr, addr_ty, data, data_ty) -> + S.add (Write_mem (name, node, simp_smt_exp vars kinds active, simp_smt_exp vars kinds wk, + simp_smt_exp vars kinds addr, addr_ty, simp_smt_exp vars kinds data, data_ty)) + seq + | Write_mem_ea (name, node, active, wk, addr, addr_ty, data_size, data_size_ty) -> + S.add (Write_mem_ea (name, node, simp_smt_exp vars kinds active, simp_smt_exp vars kinds wk, + simp_smt_exp vars kinds addr, addr_ty, simp_smt_exp vars kinds data_size, data_size_ty)) + seq + | Read_mem (name, node, active, typ, rk, addr, addr_typ) -> + S.add (Read_mem (name, node, simp_smt_exp vars kinds active, typ, simp_smt_exp vars kinds rk, + simp_smt_exp vars kinds addr, addr_typ)) + seq + | Barrier (name, node, active, bk) -> + S.add (Barrier (name, node, simp_smt_exp vars kinds active, simp_smt_exp vars kinds bk)) seq + | Excl_res (name, node, active) -> + S.add (Excl_res (name, node, simp_smt_exp vars kinds active)) seq | Assert exp -> - S.add (Assert (simp_smt_exp vars exp)) seq + S.add (Assert (simp_smt_exp vars kinds exp)) seq | (Declare_datatypes _ | Declare_tuple _) as def -> S.add def seq | Define_fun _ -> assert false @@ -1817,18 +1834,18 @@ let smt_instr_list name ctx all_cdefs instrs = List.iter (fun n -> begin match get_vertex cfg n with | None -> () - | Some ((ssanodes, cfnode), preds, succs) -> + | Some ((ssa_elems, cfnode), preds, succs) -> let muxers = - ssanodes |> List.map (smt_ssanode ctx cfg preds) |> List.concat + ssa_elems |> 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 + let ctx = { ctx with node = n; pathcond = lazy (get_pathcond n cfg ctx) } in + let basic_block = smt_cfnode all_cdefs ctx ssa_elems cfnode in push_smt_defs stack muxers; - push_smt_defs stack basic_block; + push_smt_defs stack basic_block end ) visit_order; - stack + stack, cfg 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 -> @@ -1855,7 +1872,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function |> remove_pointless_goto in - let stack = smt_instr_list (string_of_id function_id) ctx all_cdefs instrs in + 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]))]; diff --git a/src/jib/jib_smt.mli b/src/jib/jib_smt.mli index f6198a37..910388b6 100644 --- a/src/jib/jib_smt.mli +++ b/src/jib/jib_smt.mli @@ -52,6 +52,7 @@ open Ast open Ast_util open Jib open Jib_util +open Jib_ssa open Smtlib val opt_ignore_overflow : bool ref @@ -95,8 +96,9 @@ type ctx = { 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 + the global path conditional of the containing block/node in the control flow graph *) + node : int; 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 @@ -116,7 +118,7 @@ val compile : Type_check.Env.t -> Type_check.tannot defs -> cdef list * ctx val smt_header : ctx -> cdef list -> smt_def list -val smt_instr_list : string -> ctx -> cdef list -> instr list -> smt_def Stack.t +val smt_instr_list : string -> ctx -> cdef list -> instr list -> smt_def Stack.t * (ssa_elem list * cf_node) Jib_ssa.array_graph module type Sequence = sig type 'a t diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli index dadb20fd..3357bc11 100644 --- a/src/jib/jib_ssa.mli +++ b/src/jib/jib_ssa.mli @@ -61,7 +61,7 @@ val make : initial_size:int -> unit -> 'a array_graph module IntSet : Set.S with type elt = int val get_cond : 'a array_graph -> int -> Jib.cval - + val get_vertex : 'a array_graph -> int -> ('a * IntSet.t * IntSet.t) option val iter_graph : ('a -> IntSet.t -> IntSet.t -> unit) -> 'a array_graph -> unit diff --git a/src/smtlib.ml b/src/smtlib.ml index 5a2fcd44..5de13bdb 100644 --- a/src/smtlib.ml +++ b/src/smtlib.ml @@ -96,6 +96,7 @@ type smt_exp = | Var of string | Enum of string | Fn of string * smt_exp list + | Ctor of string * smt_exp list | Ite of smt_exp * smt_exp * smt_exp | SignExtend of int * smt_exp | Extract of int * int * smt_exp @@ -103,6 +104,7 @@ type smt_exp = let rec fold_smt_exp f = function | Fn (name, args) -> f (Fn (name, List.map (fold_smt_exp f) args)) + | Ctor (name, args) -> f (Ctor (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)) @@ -196,44 +198,55 @@ let simp_ite = function | Ite (Bool_lit false, _, else_exp) -> else_exp | exp -> exp -let rec simp_smt_exp vars = function +let rec simp_smt_exp vars kinds = function | Var v -> begin match Hashtbl.find_opt vars v with - | Some exp -> simp_smt_exp vars exp + | Some exp -> simp_smt_exp vars kinds exp | None -> Var v end | (Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ as exp) -> exp | Fn (f, exps) -> - let exps = List.map (simp_smt_exp vars) exps in + let exps = List.map (simp_smt_exp vars kinds) exps in simp_fn (Fn (f, exps)) + | Ctor (f, exps) -> + let exps = List.map (simp_smt_exp vars kinds) exps in + simp_fn (Ctor (f, exps)) | Ite (cond, t, e) -> - let cond = simp_smt_exp vars cond in - let t = simp_smt_exp vars t in - let e = simp_smt_exp vars e in + let cond = simp_smt_exp vars kinds cond in + let t = simp_smt_exp vars kinds t in + let e = simp_smt_exp vars kinds e in simp_ite (Ite (cond, t, e)) | Extract (i, j, exp) -> - let exp = simp_smt_exp vars exp in + let exp = simp_smt_exp vars kinds exp in 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) + let exp = simp_smt_exp vars kinds exp in + begin match exp with + | Var v -> + begin match Hashtbl.find_opt kinds v with + | Some str' when str = str' -> Bool_lit true + | Some str' -> Bool_lit false + | None -> Tester (str, exp) + end + | _ -> Tester (str, exp) + end | SignExtend (i, exp) -> - let exp = simp_smt_exp vars exp in + let exp = simp_smt_exp vars kinds exp in SignExtend (i, exp) 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_typ * smt_exp * smt_typ - | Write_mem_ea of string * smt_exp * smt_exp * smt_typ * smt_exp * smt_typ - | Read_mem of string * smt_typ * smt_exp * smt_exp * smt_typ - | Barrier of string * smt_exp - | Excl_res of string + | Write_mem of string * int * smt_exp * smt_exp * smt_exp * smt_typ * smt_exp * smt_typ + | Write_mem_ea of string * int * smt_exp * smt_exp * smt_exp * smt_typ * smt_exp * smt_typ + | Read_mem of string * int * smt_exp * smt_typ * smt_exp * smt_exp * smt_typ + | Barrier of string * int * smt_exp * smt_exp + | Excl_res of string * int * smt_exp | Declare_datatypes of string * (string * (string * smt_typ) list) list | Declare_tuple of int | Assert of smt_exp @@ -252,16 +265,19 @@ let suffix_variables_def sfx = function 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) - | Write_mem_ea (name, wk, addr, addr_ty, data_size, data_size_ty) -> - Write_mem (name ^ sfx, suffix_variables_exp sfx wk, suffix_variables_exp sfx addr, addr_ty, suffix_variables_exp sfx data_size, data_size_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) - | Barrier (name, bk) -> - Barrier (name ^ sfx, bk) - | Excl_res name -> - Excl_res (name ^ sfx) + | Write_mem (name, node, active, wk, addr, addr_ty, data, data_ty) -> + Write_mem (name ^ sfx, node, suffix_variables_exp sfx active, suffix_variables_exp sfx wk, + suffix_variables_exp sfx addr, addr_ty, suffix_variables_exp sfx data, data_ty) + | Write_mem_ea (name, node, active , wk, addr, addr_ty, data_size, data_size_ty) -> + Write_mem (name ^ sfx, node, suffix_variables_exp sfx active, suffix_variables_exp sfx wk, + suffix_variables_exp sfx addr, addr_ty, suffix_variables_exp sfx data_size, data_size_ty) + | Read_mem (name, node, active, ty, rk, addr, addr_ty) -> + Read_mem (name ^ sfx, node, suffix_variables_exp sfx active, ty, suffix_variables_exp sfx rk, + suffix_variables_exp sfx addr, addr_ty) + | Barrier (name, node, active, bk) -> + Barrier (name ^ sfx, node, suffix_variables_exp sfx active, suffix_variables_exp sfx bk) + | Excl_res (name, node, active) -> + Excl_res (name ^ sfx, node, suffix_variables_exp sfx active) | Declare_datatypes (name, ctors) -> Declare_datatypes (name, ctors) | Declare_tuple n -> @@ -316,6 +332,7 @@ let rec pp_smt_exp = | Var str -> string str | Enum str -> string str | Fn (str, exps) -> parens (string str ^^ space ^^ separate_map space pp_smt_exp exps) + | Ctor (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 cond; pp_smt_exp then_exp; pp_smt_exp else_exp]) | Extract (i, j, exp) -> @@ -354,27 +371,32 @@ let pp_smt_def = | Define_const (name, ty, exp) -> pp_sfun "define-const" [string name; pp_smt_typ ty; pp_smt_exp exp] - | Write_mem (name, wk, addr, addr_ty, data, data_ty) -> + | Write_mem (name, _, active, 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 ^ "_active"); pp_smt_typ Bool; pp_smt_exp active] ^^ 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] - | Write_mem_ea (name, wk, addr, addr_ty, data_size, data_size_ty) -> + | Write_mem_ea (name, _, active, wk, addr, addr_ty, data_size, data_size_ty) -> pp_sfun "define-const" [string (name ^ "_kind"); string "Zwrite_kind"; pp_smt_exp wk] ^^ hardline + ^^ pp_sfun "define-const" [string (name ^ "_active"); pp_smt_typ Bool; pp_smt_exp active] ^^ hardline ^^ pp_sfun "define-const" [string (name ^ "_size"); pp_smt_typ data_size_ty; pp_smt_exp data_size] ^^ hardline ^^ pp_sfun "define-const" [string (name ^ "_addr"); pp_smt_typ addr_ty; pp_smt_exp addr] - | Read_mem (name, ty, rk, addr, addr_ty) -> + | Read_mem (name, _, active, 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 ^ "_active"); pp_smt_typ Bool; pp_smt_exp active] ^^ 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] - | Barrier (name, bk) -> - pp_sfun "define-const" [string (name ^ "_kind"); string "Zbarrier_kind"; pp_smt_exp bk] + | Barrier (name, _, active, bk) -> + pp_sfun "define-const" [string (name ^ "_kind"); string "Zbarrier_kind"; pp_smt_exp bk] ^^ hardline + ^^ pp_sfun "define-const" [string (name ^ "_active"); pp_smt_typ Bool; pp_smt_exp active] - | Excl_res name -> - pp_sfun "declare-const" [string (name ^ "_res"); pp_smt_typ Bool] + | Excl_res (name, _, active) -> + pp_sfun "declare-const" [string (name ^ "_res"); pp_smt_typ Bool] ^^ hardline + ^^ pp_sfun "define-const" [string (name ^ "_active"); pp_smt_typ Bool; pp_smt_exp active] | Declare_datatypes (name, ctors) -> let pp_ctor (ctor_name, fields) = -- cgit v1.2.3