summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/jib/jib_smt.ml97
-rw-r--r--src/jib/jib_smt.mli6
-rw-r--r--src/jib/jib_ssa.mli2
-rw-r--r--src/smtlib.ml86
4 files changed, 116 insertions, 75 deletions
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) =
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-15 15:02:13 +0000