From d1f8714b56e1def25cbd5f833eb85bba001f0537 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 10 Jun 2020 07:04:48 -0700 Subject: [PATCH] [sledge] Refactor: Move Exp.term to Term.of_exp Summary: and Reg.var to Var.of_reg Reviewed By: jvillard Differential Revision: D21720988 fbshipit-source-id: 8f1ddb1a2 --- sledge/bin/domain_itv.ml | 4 +- sledge/src/domain_sh.ml | 77 +++++---- sledge/src/domain_used_globals.ml | 4 +- sledge/src/exp.ml | 69 +------- sledge/src/exp.mli | 4 +- sledge/src/exp_test.ml | 2 +- sledge/src/global.ml | 2 +- sledge/src/term.ml | 273 ++++++++++++++++++------------ sledge/src/term.mli | 7 +- sledge/src/term_test.ml | 2 +- 10 files changed, 223 insertions(+), 221 deletions(-) diff --git a/sledge/bin/domain_itv.ml b/sledge/bin/domain_itv.ml index 9372fc2ce..153f4b2a4 100644 --- a/sledge/bin/domain_itv.ml +++ b/sledge/bin/domain_itv.ml @@ -173,7 +173,7 @@ let assign reg exp q = let lval = apron_var_of_reg reg in ( match Option.bind - ~f:(apron_texpr_of_llair_term (Exp.term exp) q) + ~f:(apron_texpr_of_llair_term (Term.of_exp exp) q) (apron_typ_of_llair_typ (Reg.typ reg)) with | Some e -> @@ -196,7 +196,7 @@ let assign reg exp q = (** block if [e] is known to be false; skip otherwise *) let exec_assume q e = - match apron_texpr_of_llair_term (Exp.term e) q Texpr1.Int with + match apron_texpr_of_llair_term (Term.of_exp e) q Texpr1.Int with | Some e -> let cond = Abstract1.bound_texpr (Lazy.force man) q (Texpr1.of_expr q.env e) diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index 7b8df0c9a..f7fcfdd6e 100644 --- a/sledge/src/domain_sh.ml +++ b/sledge/src/domain_sh.ml @@ -19,9 +19,9 @@ let simplify q = if !simplify_states then Sh.simplify q else q let init globals = IArray.fold globals ~init:Sh.emp ~f:(fun q -> function | {Global.reg; init= Some (arr, siz)} -> - let loc = Term.var (Reg.var reg) in + let loc = Term.var (Var.of_reg reg) in let len = Term.integer (Z.of_int siz) in - let arr = Exp.term arr in + let arr = Term.of_exp arr in Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr}) | _ -> q ) @@ -34,11 +34,15 @@ let join p q = let is_false = Sh.is_false let dnf = Sh.dnf -let exec_assume q b = Exec.assume q (Exp.term b) |> Option.map ~f:simplify -let exec_kill q r = Exec.kill q (Reg.var r) |> simplify + +let exec_assume q b = + Exec.assume q (Term.of_exp b) |> Option.map ~f:simplify + +let exec_kill q r = Exec.kill q (Var.of_reg r) |> simplify let exec_move q res = - Exec.move q (IArray.map res ~f:(fun (r, e) -> (Reg.var r, Exp.term e))) + Exec.move q + (IArray.map res ~f:(fun (r, e) -> (Var.of_reg r, Term.of_exp e))) |> simplify let exec_inst pre inst = @@ -46,33 +50,36 @@ let exec_inst pre inst = | Move {reg_exps; _} -> Some (Exec.move pre - (IArray.map reg_exps ~f:(fun (r, e) -> (Reg.var r, Exp.term e)))) + (IArray.map reg_exps ~f:(fun (r, e) -> + (Var.of_reg r, Term.of_exp e) ))) | Load {reg; ptr; len; _} -> - Exec.load pre ~reg:(Reg.var reg) ~ptr:(Exp.term ptr) - ~len:(Exp.term len) + Exec.load pre ~reg:(Var.of_reg reg) ~ptr:(Term.of_exp ptr) + ~len:(Term.of_exp len) | Store {ptr; exp; len; _} -> - Exec.store pre ~ptr:(Exp.term ptr) ~exp:(Exp.term exp) - ~len:(Exp.term len) + Exec.store pre ~ptr:(Term.of_exp ptr) ~exp:(Term.of_exp exp) + ~len:(Term.of_exp len) | Memset {dst; byt; len; _} -> - Exec.memset pre ~dst:(Exp.term dst) ~byt:(Exp.term byt) - ~len:(Exp.term len) + Exec.memset pre ~dst:(Term.of_exp dst) ~byt:(Term.of_exp byt) + ~len:(Term.of_exp len) | Memcpy {dst; src; len; _} -> - Exec.memcpy pre ~dst:(Exp.term dst) ~src:(Exp.term src) - ~len:(Exp.term len) + Exec.memcpy pre ~dst:(Term.of_exp dst) ~src:(Term.of_exp src) + ~len:(Term.of_exp len) | Memmov {dst; src; len; _} -> - Exec.memmov pre ~dst:(Exp.term dst) ~src:(Exp.term src) - ~len:(Exp.term len) + Exec.memmov pre ~dst:(Term.of_exp dst) ~src:(Term.of_exp src) + ~len:(Term.of_exp len) | Alloc {reg; num; len; _} -> - Exec.alloc pre ~reg:(Reg.var reg) ~num:(Exp.term num) - ~len:(Exp.term len) - | Free {ptr; _} -> Exec.free pre ~ptr:(Exp.term ptr) - | Nondet {reg; _} -> Some (Exec.nondet pre (Option.map ~f:Reg.var reg)) + Exec.alloc pre ~reg:(Var.of_reg reg) ~num:(Term.of_exp num) + ~len:(Term.of_exp len) + | Free {ptr; _} -> Exec.free pre ~ptr:(Term.of_exp ptr) + | Nondet {reg; _} -> Some (Exec.nondet pre (Option.map ~f:Var.of_reg reg)) | Abort _ -> Exec.abort pre ) |> Option.map ~f:simplify let exec_intrinsic ~skip_throw q r i es = - Exec.intrinsic ~skip_throw q (Option.map ~f:Reg.var r) (Reg.var i) - (List.map ~f:Exp.term es) + Exec.intrinsic ~skip_throw q + (Option.map ~f:Var.of_reg r) + (Var.of_reg i) + (List.map ~f:Term.of_exp es) |> Option.map ~f:(Option.map ~f:simplify) let term_eq_class_has_only_vars_in fvs cong term = @@ -121,10 +128,12 @@ let and_eqs sub formals actuals q = let localize_entry globals actuals formals freturn locals subst pre entry = (* Add the formals here to do garbage collection and then get rid of them *) let formals_set = Var.Set.of_list formals in - let freturn_locals = Reg.Set.vars (Reg.Set.add_option freturn locals) in + let freturn_locals = + Var.Set.of_regs (Reg.Set.add_option freturn locals) + in let function_summary_pre = garbage_collect entry - ~wrt:(Var.Set.union formals_set (Reg.Set.vars globals)) + ~wrt:(Var.Set.union formals_set (Var.Set.of_regs globals)) in [%Trace.info "function summary pre %a" pp function_summary_pre] ; let foot = Sh.exists formals_set function_summary_pre in @@ -153,10 +162,12 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q = (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Reg.pp) (List.rev formals) Reg.Set.pp locals Reg.Set.pp globals pp q] ; - let actuals = List.map ~f:Exp.term actuals in - let areturn = Option.map ~f:Reg.var areturn in - let formals = List.map ~f:Reg.var formals in - let freturn_locals = Reg.Set.vars (Reg.Set.add_option freturn locals) in + let actuals = List.map ~f:Term.of_exp actuals in + let areturn = Option.map ~f:Var.of_reg areturn in + let formals = List.map ~f:Var.of_reg formals in + let freturn_locals = + Var.Set.of_regs (Reg.Set.add_option freturn locals) + in let modifs = Var.Set.of_option areturn in (* quantify modifs, their current value will be overwritten and so does not need to be saved in the freshening renaming *) @@ -191,7 +202,7 @@ let post locals _ q = [%Trace.call fun {pf} -> pf "@[locals: {@[%a@]}@ q: %a@]" Reg.Set.pp locals Sh.pp q] ; - Sh.exists (Reg.Set.vars locals) q |> simplify + Sh.exists (Var.Set.of_regs locals) q |> simplify |> [%Trace.retn fun {pf} -> pf "%a" Sh.pp] @@ -207,8 +218,8 @@ let retn formals freturn {areturn; subst; frame} q = (Option.pp "@ areturn: %a" Var.pp) areturn Var.Subst.pp (Var.Subst.invert subst) pp q pp frame] ; - let formals = List.map ~f:Reg.var formals in - let freturn = Option.map ~f:Reg.var freturn in + let formals = List.map ~f:Var.of_reg formals in + let freturn = Option.map ~f:Var.of_reg freturn in let inv_subst = Var.Subst.invert subst in let q, inv_subst = match areturn with @@ -253,8 +264,8 @@ let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) = pf "formals %a@ entry: %a@ current: %a" Reg.Set.pp formals pp entry pp post] ; - let locals = Reg.Set.vars locals in - let formals = Reg.Set.vars formals in + let locals = Var.Set.of_regs locals in + let formals = Var.Set.of_regs formals in let foot = Sh.exists locals entry in let foot, subst = Sh.freshen ~wrt:(Var.Set.union foot.us post.us) foot in let restore_formals q = diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml index 085e3b5d8..1f1653f74 100644 --- a/sledge/src/domain_used_globals.ml +++ b/sledge/src/domain_used_globals.ml @@ -23,9 +23,7 @@ let is_false _ = false let post _ _ state = state let retn _ _ from_call post = Reg.Set.union from_call post let dnf t = [t] - -let add_if_global gs v = - if Var.is_global (Reg.var v) then Reg.Set.add gs v else gs +let add_if_global gs v = if Reg.is_global v then Reg.Set.add gs v else gs let used_globals ?(init = empty) exp = Exp.fold_regs exp ~init ~f:add_if_global diff --git a/sledge/src/exp.ml b/sledge/src/exp.ml index 4e1f23ab5..a52525623 100644 --- a/sledge/src/exp.ml +++ b/sledge/src/exp.ml @@ -79,58 +79,6 @@ include T module Set = struct include Set.Make (T) include Provide_of_sexp (T) end module Map = Map.Make (T) -let unsigned typ = Term.unsigned (Typ.bit_size_of typ) - -let rec term = function - | Reg {name; global; typ= _} -> - Term.var (Var.program ?global:(Option.some_if global ()) name) - | Nondet {msg; typ= _} -> Term.nondet msg - | Label {parent; name} -> Term.label ~parent ~name - | Integer {data; typ= _} -> Term.integer data - | Float {data; typ= _} -> Term.float data - | Ap1 (Signed {bits}, _, x) -> Term.signed bits (term x) - | Ap1 (Unsigned {bits}, _, x) -> Term.unsigned bits (term x) - | Ap1 (Convert {src}, dst, exp) -> Term.convert src ~to_:dst (term exp) - | Ap2 (Eq, _, x, y) -> Term.eq (term x) (term y) - | Ap2 (Dq, _, x, y) -> Term.dq (term x) (term y) - | Ap2 (Gt, _, x, y) -> Term.lt (term y) (term x) - | Ap2 (Ge, _, x, y) -> Term.le (term y) (term x) - | Ap2 (Lt, _, x, y) -> Term.lt (term x) (term y) - | Ap2 (Le, _, x, y) -> Term.le (term x) (term y) - | Ap2 (Ugt, typ, x, y) -> - Term.lt (unsigned typ (term y)) (unsigned typ (term x)) - | Ap2 (Uge, typ, x, y) -> - Term.le (unsigned typ (term y)) (unsigned typ (term x)) - | Ap2 (Ult, typ, x, y) -> - Term.lt (unsigned typ (term x)) (unsigned typ (term y)) - | Ap2 (Ule, typ, x, y) -> - Term.le (unsigned typ (term x)) (unsigned typ (term y)) - | Ap2 (Ord, _, x, y) -> Term.ord (term x) (term y) - | Ap2 (Uno, _, x, y) -> Term.uno (term x) (term y) - | Ap2 (Add, _, x, y) -> Term.add (term x) (term y) - | Ap2 (Sub, _, x, y) -> Term.sub (term x) (term y) - | Ap2 (Mul, _, x, y) -> Term.mul (term x) (term y) - | Ap2 (Div, _, x, y) -> Term.div (term x) (term y) - | Ap2 (Rem, _, x, y) -> Term.rem (term x) (term y) - | Ap2 (Udiv, typ, x, y) -> - Term.div (unsigned typ (term x)) (unsigned typ (term y)) - | Ap2 (Urem, typ, x, y) -> - Term.rem (unsigned typ (term x)) (unsigned typ (term y)) - | Ap2 (And, _, x, y) -> Term.and_ (term x) (term y) - | Ap2 (Or, _, x, y) -> Term.or_ (term x) (term y) - | Ap2 (Xor, _, x, y) -> Term.xor (term x) (term y) - | Ap2 (Shl, _, x, y) -> Term.shl (term x) (term y) - | Ap2 (Lshr, _, x, y) -> Term.lshr (term x) (term y) - | Ap2 (Ashr, _, x, y) -> Term.ashr (term x) (term y) - | Ap3 (Conditional, _, cnd, thn, els) -> - Term.conditional ~cnd:(term cnd) ~thn:(term thn) ~els:(term els) - | Ap1 (Splat, _, byt) -> Term.splat (term byt) - | ApN (Record, _, elts) -> Term.record (IArray.map ~f:term elts) - | Ap1 (Select idx, _, rcd) -> Term.select ~rcd:(term rcd) ~idx - | Ap2 (Update idx, _, rcd, elt) -> - Term.update ~rcd:(term rcd) ~idx ~elt:(term elt) - | RecRecord (i, _) -> Term.rec_record i - let pp_op2 fs op = let pf fmt = Format.fprintf fs fmt in match op with @@ -167,10 +115,8 @@ let rec pp fs exp = Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt in match exp with - | Reg {name} -> ( - match Var.of_term (term exp) with - | Some v when Var.is_global v -> pf "%@%s" name - | _ -> pf "%%%s" name ) + | Reg {name; global= true} -> pf "%@%s" name + | Reg {name; global= false} -> pf "%%%s" name | Nondet {msg} -> pf "nondet \"%s\"" msg | Label {name} -> pf "%s" name | Integer {data; typ= Pointer _} when Z.equal Z.zero data -> pf "null" @@ -332,18 +278,10 @@ module Reg = struct let pp = pp - let var r = - match Var.of_term (term r) with - | Some v -> v - | _ -> violates invariant r - module Set = struct include Set let pp = Set.pp pp_exp - - let vars = - Set.fold ~init:Var.Set.empty ~f:(fun s r -> Var.Set.add s (var r)) end module Map = Map @@ -364,7 +302,8 @@ module Reg = struct match x with Reg _ -> invariant x | _ -> assert false let name = function Reg x -> x.name | r -> violates invariant r - let typ r = match r with Reg x -> x.typ | _ -> violates invariant r + let typ = function Reg x -> x.typ | r -> violates invariant r + let is_global = function Reg x -> x.global | r -> violates invariant r let of_exp = function | Reg _ as e -> Some (e |> check invariant) diff --git a/sledge/src/exp.mli b/sledge/src/exp.mli index f867f503a..9ea6771b4 100644 --- a/sledge/src/exp.mli +++ b/sledge/src/exp.mli @@ -102,7 +102,6 @@ module Reg : sig val sexp_of_t : t -> Sexp.t val t_of_sexp : Sexp.t -> t val pp : t pp - val vars : t -> Var.Set.t end module Map : Map.S with type key := t @@ -115,9 +114,9 @@ module Reg : sig val of_exp : exp -> t option val program : ?global:unit -> Typ.t -> string -> t - val var : t -> Var.t val name : t -> string val typ : t -> Typ.t + val is_global : t -> bool end (** Construct *) @@ -191,6 +190,5 @@ val fold_regs : t -> init:'a -> f:('a -> Reg.t -> 'a) -> 'a (** Query *) -val term : t -> Term.t val is_true : t -> bool val is_false : t -> bool diff --git a/sledge/src/exp_test.ml b/sledge/src/exp_test.ml index afef8e38a..7a4958e0c 100644 --- a/sledge/src/exp_test.ml +++ b/sledge/src/exp_test.ml @@ -14,7 +14,7 @@ let%test_module _ = open Exp let pp e = - Format.printf "@\n{desc= %a; term= %a}@." pp e Term.pp (Exp.term e) + Format.printf "@\n{desc= %a; term= %a}@." pp e Term.pp (Term.of_exp e) let ( ! ) i = integer Typ.siz (Z.of_int i) diff --git a/sledge/src/global.ml b/sledge/src/global.ml index dce9085e5..c80f6625b 100644 --- a/sledge/src/global.ml +++ b/sledge/src/global.ml @@ -28,6 +28,6 @@ let invariant g = let@ () = Invariant.invariant [%here] g [%sexp_of: t] in let {reg} = g in assert (Typ.is_sized (Reg.typ reg)) ; - assert (Var.is_global (Reg.var reg)) + assert (Reg.is_global reg) let mk ?init reg loc = {reg; init; loc} |> check invariant diff --git a/sledge/src/term.ml b/sledge/src/term.ml index 0599636cf..cd6adce02 100644 --- a/sledge/src/term.ml +++ b/sledge/src/term.ml @@ -320,116 +320,6 @@ let invariant e = | _ -> () [@@warning "-9"] -(** Variables are the terms constructed by [Var] *) -module Var = struct - include T - - let pp = pp - - type strength = t -> [`Universal | `Existential | `Anonymous] option - - module Map = Map - - module Set = struct - include Set - - let pp vs = Set.pp pp_t vs - let ppx strength vs = Set.pp (ppx strength) vs - - let pp_xs fs xs = - if not (is_empty xs) then - Format.fprintf fs "@<2>∃ @[%a@] .@;<1 2>" pp xs - end - - let invariant x = - let@ () = Invariant.invariant [%here] x [%sexp_of: t] in - match x with Var _ -> invariant x | _ -> assert false - - let id = function Var v -> v.id | x -> violates invariant x - let name = function Var v -> v.name | x -> violates invariant x - let is_global = function Var v -> v.id = -1 | x -> violates invariant x - let of_ = function Var _ as v -> v | _ -> invalid_arg "Var.of_" - - let of_term = function - | Var _ as v -> Some (v |> check invariant) - | _ -> None - - let program ?global name = - Var {name; id= (if Option.is_some global then -1 else 0)} - - let fresh name ~wrt = - let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in - let x' = Var {name; id= max + 1} in - (x', Set.add wrt x') - - let identified ~name ~id = Var {name; id} - - (** Variable renaming substitutions *) - module Subst = struct - type t = T.t Map.t [@@deriving compare, equal, sexp_of] - - let t_of_sexp = Map.t_of_sexp T.t_of_sexp - - let invariant s = - let@ () = Invariant.invariant [%here] s [%sexp_of: t] in - let domain, range = - Map.fold s ~init:(Set.empty, Set.empty) - ~f:(fun ~key ~data (domain, range) -> - assert (not (Set.mem range data)) ; - (Set.add domain key, Set.add range data) ) - in - assert (Set.disjoint domain range) - - let pp = Map.pp pp_t pp_t - let empty = Map.empty - let is_empty = Map.is_empty - - let freshen vs ~wrt = - let xs = Set.inter wrt vs in - ( if Set.is_empty xs then empty - else - let wrt = Set.union wrt vs in - Set.fold xs ~init:(empty, wrt) ~f:(fun (sub, wrt) x -> - let x', wrt = fresh (name x) ~wrt in - let sub = Map.add_exn sub ~key:x ~data:x' in - (sub, wrt) ) - |> fst ) - |> check invariant - - let fold sub ~init ~f = - Map.fold sub ~init ~f:(fun ~key ~data s -> f key data s) - - let invert sub = - Map.fold sub ~init:empty ~f:(fun ~key ~data sub' -> - Map.add_exn sub' ~key:data ~data:key ) - |> check invariant - - let restrict sub vs = - Map.filter_keys ~f:(Set.mem vs) sub |> check invariant - - let domain sub = - Map.fold sub ~init:Set.empty ~f:(fun ~key ~data:_ domain -> - Set.add domain key ) - - let range sub = - Map.fold sub ~init:Set.empty ~f:(fun ~key:_ ~data range -> - Set.add range data ) - - let apply sub v = Map.find sub v |> Option.value ~default:v - - let apply_set sub vs = - Map.fold sub ~init:vs ~f:(fun ~key ~data vs -> - let vs' = Set.remove vs key in - if vs' == vs then vs - else ( - assert (not (Set.equal vs' vs)) ; - Set.add vs' data ) ) - |> check (fun vs' -> - assert (Set.disjoint (domain sub) vs') ; - assert (Set.is_subset (range sub) ~of_:vs') ) - end -end - (** Construct *) (* variables *) @@ -1089,6 +979,169 @@ let eq_concat (siz, arr) ms = eq (memory ~siz ~arr) (concat (Array.map ~f:(fun (siz, arr) -> memory ~siz ~arr) ms)) +let rec binary mk x y = mk (of_exp x) (of_exp y) + +and ubinary mk typ x y = + let unsigned typ = unsigned (Typ.bit_size_of typ) in + mk (unsigned typ (of_exp x)) (unsigned typ (of_exp y)) + +and of_exp e = + match (e : Exp.t) with + | Reg {name; global; typ= _} -> Var {name; id= (if global then -1 else 0)} + | Nondet {msg; typ= _} -> nondet msg + | Label {parent; name} -> label ~parent ~name + | Integer {data; typ= _} -> integer data + | Float {data; typ= _} -> float data + | Ap1 (Signed {bits}, _, x) -> signed bits (of_exp x) + | Ap1 (Unsigned {bits}, _, x) -> unsigned bits (of_exp x) + | Ap1 (Convert {src}, dst, exp) -> convert src ~to_:dst (of_exp exp) + | Ap2 (Eq, _, x, y) -> binary eq x y + | Ap2 (Dq, _, x, y) -> binary dq x y + | Ap2 (Gt, _, x, y) -> binary lt y x + | Ap2 (Ge, _, x, y) -> binary le y x + | Ap2 (Lt, _, x, y) -> binary lt x y + | Ap2 (Le, _, x, y) -> binary le x y + | Ap2 (Ugt, typ, x, y) -> ubinary lt typ y x + | Ap2 (Uge, typ, x, y) -> ubinary le typ y x + | Ap2 (Ult, typ, x, y) -> ubinary lt typ x y + | Ap2 (Ule, typ, x, y) -> ubinary le typ x y + | Ap2 (Ord, _, x, y) -> binary ord x y + | Ap2 (Uno, _, x, y) -> binary uno x y + | Ap2 (Add, _, x, y) -> binary add x y + | Ap2 (Sub, _, x, y) -> binary sub x y + | Ap2 (Mul, _, x, y) -> binary mul x y + | Ap2 (Div, _, x, y) -> binary div x y + | Ap2 (Rem, _, x, y) -> binary rem x y + | Ap2 (Udiv, typ, x, y) -> ubinary div typ x y + | Ap2 (Urem, typ, x, y) -> ubinary rem typ x y + | Ap2 (And, _, x, y) -> binary and_ x y + | Ap2 (Or, _, x, y) -> binary or_ x y + | Ap2 (Xor, _, x, y) -> binary xor x y + | Ap2 (Shl, _, x, y) -> binary shl x y + | Ap2 (Lshr, _, x, y) -> binary lshr x y + | Ap2 (Ashr, _, x, y) -> binary ashr x y + | Ap3 (Conditional, _, cnd, thn, els) -> + conditional ~cnd:(of_exp cnd) ~thn:(of_exp thn) ~els:(of_exp els) + | Ap1 (Splat, _, byt) -> splat (of_exp byt) + | ApN (Record, _, elts) -> record (IArray.map ~f:of_exp elts) + | Ap1 (Select idx, _, rcd) -> select ~rcd:(of_exp rcd) ~idx + | Ap2 (Update idx, _, rcd, elt) -> + update ~rcd:(of_exp rcd) ~idx ~elt:(of_exp elt) + | RecRecord (i, _) -> rec_record i + +(** Variables are the terms constructed by [Var] *) +module Var = struct + include T + + let pp = pp + + type strength = t -> [`Universal | `Existential | `Anonymous] option + + let invariant x = + let@ () = Invariant.invariant [%here] x [%sexp_of: t] in + match x with Var _ -> invariant x | _ -> assert false + + let id = function Var v -> v.id | x -> violates invariant x + let name = function Var v -> v.name | x -> violates invariant x + let of_ = function Var _ as v -> v | _ -> invalid_arg "Var.of_" + + let of_term = function + | Var _ as v -> Some (v |> check invariant) + | _ -> None + + let of_reg r = + match of_term (of_exp (r : Reg.t :> Exp.t)) with + | Some v -> v + | _ -> violates Reg.invariant r + + let fresh name ~wrt = + let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in + let x' = Var {name; id= max + 1} in + (x', Set.add wrt x') + + let identified ~name ~id = Var {name; id} + + module Map = Map + + module Set = struct + include Set + + let pp vs = Set.pp pp_t vs + let ppx strength vs = Set.pp (ppx strength) vs + + let pp_xs fs xs = + if not (is_empty xs) then + Format.fprintf fs "@<2>∃ @[%a@] .@;<1 2>" pp xs + + let of_regs = Reg.Set.fold ~init:empty ~f:(fun s r -> add s (of_reg r)) + end + + (** Variable renaming substitutions *) + module Subst = struct + type t = T.t Map.t [@@deriving compare, equal, sexp_of] + + let t_of_sexp = Map.t_of_sexp T.t_of_sexp + + let invariant s = + let@ () = Invariant.invariant [%here] s [%sexp_of: t] in + let domain, range = + Map.fold s ~init:(Set.empty, Set.empty) + ~f:(fun ~key ~data (domain, range) -> + assert (not (Set.mem range data)) ; + (Set.add domain key, Set.add range data) ) + in + assert (Set.disjoint domain range) + + let pp = Map.pp pp_t pp_t + let empty = Map.empty + let is_empty = Map.is_empty + + let freshen vs ~wrt = + let xs = Set.inter wrt vs in + ( if Set.is_empty xs then empty + else + let wrt = Set.union wrt vs in + Set.fold xs ~init:(empty, wrt) ~f:(fun (sub, wrt) x -> + let x', wrt = fresh (name x) ~wrt in + let sub = Map.add_exn sub ~key:x ~data:x' in + (sub, wrt) ) + |> fst ) + |> check invariant + + let fold sub ~init ~f = + Map.fold sub ~init ~f:(fun ~key ~data s -> f key data s) + + let invert sub = + Map.fold sub ~init:empty ~f:(fun ~key ~data sub' -> + Map.add_exn sub' ~key:data ~data:key ) + |> check invariant + + let restrict sub vs = + Map.filter_keys ~f:(Set.mem vs) sub |> check invariant + + let domain sub = + Map.fold sub ~init:Set.empty ~f:(fun ~key ~data:_ domain -> + Set.add domain key ) + + let range sub = + Map.fold sub ~init:Set.empty ~f:(fun ~key:_ ~data range -> + Set.add range data ) + + let apply sub v = Map.find sub v |> Option.value ~default:v + + let apply_set sub vs = + Map.fold sub ~init:vs ~f:(fun ~key ~data vs -> + let vs' = Set.remove vs key in + if vs' == vs then vs + else ( + assert (not (Set.equal vs' vs)) ; + Set.add vs' data ) ) + |> check (fun vs' -> + assert (Set.disjoint (domain sub) vs') ; + assert (Set.is_subset (range sub) ~of_:vs') ) + end +end + (** Transform *) let map e ~f = diff --git a/sledge/src/term.mli b/sledge/src/term.mli index 026e6fcd7..39fe77097 100644 --- a/sledge/src/term.mli +++ b/sledge/src/term.mli @@ -118,6 +118,7 @@ module Var : sig val ppx : strength -> t pp val pp : t pp val pp_xs : t pp + val of_regs : Reg.Set.t -> t end val pp : t pp @@ -126,10 +127,9 @@ module Var : sig val name : t -> string val id : t -> int - val is_global : t -> bool val of_ : term -> t val of_term : term -> t option - val program : ?global:unit -> string -> t + val of_reg : Reg.t -> t val fresh : string -> wrt:Set.t -> t * Set.t val identified : name:string -> id:int -> t @@ -238,6 +238,9 @@ val select : rcd:t -> idx:int -> t val update : rcd:t -> idx:int -> elt:t -> t val rec_record : int -> t +(* convert *) +val of_exp : Exp.t -> t + (** Transform *) val map : t -> f:(t -> t) -> t diff --git a/sledge/src/term_test.ml b/sledge/src/term_test.ml index 14505d375..e7fb5ebcc 100644 --- a/sledge/src/term_test.ml +++ b/sledge/src/term_test.ml @@ -40,7 +40,7 @@ let%test_module _ = let%test "unsigned boolean overflow" = is_true - (Exp.term + (Term.of_exp (Exp.uge (Exp.integer Typ.bool Z.minus_one) (Exp.signed 1 (Exp.integer Typ.siz Z.one) ~to_:Typ.bool)))