From 8ee0c67d1fcc1d4ecb117975797b7621183ab360 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 9 Oct 2019 08:36:45 -0700 Subject: [PATCH] [sledge] Precompute the Term form of each Exp, and add it to Exp.t Reviewed By: bennostein Differential Revision: D17665261 fbshipit-source-id: 25f2e656f --- sledge/src/llair/exp.ml | 251 ++++++++++++++----- sledge/src/llair/exp.mli | 8 +- sledge/src/{symbheap => llair}/term.ml | 59 +---- sledge/src/{symbheap => llair}/term.mli | 8 +- sledge/src/{symbheap => llair}/term_test.ml | 20 +- sledge/src/{symbheap => llair}/term_test.mli | 0 sledge/src/{symbheap => llair}/var.ml | 0 sledge/src/{symbheap => llair}/var.mli | 0 sledge/src/symbheap/exec.ml | 25 +- sledge/src/symbheap/sh_domain.ml | 36 ++- 10 files changed, 240 insertions(+), 167 deletions(-) rename sledge/src/{symbheap => llair}/term.ml (93%) rename sledge/src/{symbheap => llair}/term.mli (97%) rename sledge/src/{symbheap => llair}/term_test.ml (94%) rename sledge/src/{symbheap => llair}/term_test.mli (100%) rename sledge/src/{symbheap => llair}/var.ml (100%) rename sledge/src/{symbheap => llair}/var.mli (100%) diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index 68ddd9eed..2666af1f7 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -7,6 +7,8 @@ (** Expressions *) +[@@@warning "+9"] + module T = struct module T0 = struct type op1 = @@ -59,7 +61,9 @@ module T = struct | Struct_rec (** NOTE: may be cyclic *) [@@deriving compare, equal, hash, sexp] - type t = + type t = {desc: desc; term: Term.t} + + and desc = | Reg of {name: string; typ: Typ.t; global: bool} | Nondet of {msg: string; typ: Typ.t} | Label of {parent: string; name: string} @@ -78,16 +82,18 @@ end include T +let term e = e.term + let fix (f : (t -> 'a as 'f) -> 'f) (bot : 'f) (e : t) : 'a = let rec fix_f seen e = - match e with + match e.desc with | ApN (Struct_rec, _, _) -> if List.mem ~equal:( == ) seen e then f bot e else f (fix_f (e :: seen)) e | _ -> f (fix_f seen) e in let rec fix_f_seen_nil e = - match e with + match e.desc with | ApN (Struct_rec, _, _) -> f (fix_f [e]) e | _ -> f fix_f_seen_nil e in @@ -132,7 +138,7 @@ let rec pp fs exp = Format.pp_open_box fs 2 ; Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt in - match exp with + match exp.desc with | Reg {name; global= true} -> pf "%@%s" name | Reg {name; global= false} -> pf "%%%s" name | Nondet {msg} -> pf "nondet \"%s\"" msg @@ -149,9 +155,11 @@ let rec pp fs exp = | Ap1 (Select idx, _, rcd) -> pf "%a[%i]" pp rcd idx | Ap2 (Update idx, _, rcd, elt) -> pf "[%a@ @[| %i → %a@]]" pp rcd idx pp elt - | Ap2 (Xor, Integer {bits= 1}, Integer {data}, x) when Z.is_true data -> + | Ap2 (Xor, Integer {bits= 1}, {desc= Integer {data}}, x) + when Z.is_true data -> pf "¬%a" pp x - | Ap2 (Xor, Integer {bits= 1}, x, Integer {data}) when Z.is_true data -> + | Ap2 (Xor, Integer {bits= 1}, x, {desc= Integer {data}}) + when Z.is_true data -> pf "¬%a" pp x | Ap2 (op, _, x, y) -> pf "(%a@ %a %a)" pp x pp_op2 op pp y | Ap3 (Conditional, _, cnd, thn, els) -> @@ -160,6 +168,7 @@ let rec pp fs exp = | ApN (Struct_rec, _, elts) -> pf "{|%a|}" (Vector.pp ",@ " pp) elts in fix_flip pp_ (fun _ _ -> ()) fs exp + [@@warning "-9"] and pp_record fs elts = [%Trace.fprintf @@ -167,7 +176,7 @@ and pp_record fs elts = (fun fs elts -> match String.init (Vector.length elts) ~f:(fun i -> - match Vector.get elts i with + match (Vector.get elts i).desc with | Integer {data} -> Char.of_int_exn (Z.to_int data) | _ -> raise (Invalid_argument "not a string") ) with @@ -175,6 +184,7 @@ and pp_record fs elts = | exception _ -> Format.fprintf fs "@[%a@]" (Vector.pp ",@ " pp) elts ) elts] + [@@warning "-9"] type exp = t @@ -187,7 +197,7 @@ let valid_idx idx elts = 0 <= idx && idx < Vector.length elts let rec invariant exp = Invariant.invariant [%here] exp [%sexp_of: t] @@ fun () -> - match exp with + match exp.desc with | Reg {typ} | Nondet {typ} -> assert (Typ.is_sized typ) | Integer {data; typ} -> ( match typ with @@ -245,11 +255,12 @@ let rec invariant exp = Vector.for_all2_exn elts args ~f:(fun typ arg -> Typ.equal typ (typ_of arg) ) ) | _ -> assert false ) + [@@warning "-9"] (** Type query *) and typ_of exp = - match exp with + match exp.desc with | Reg {typ} | Nondet {typ} | Integer {typ} | Float {typ} -> typ | Label _ -> Typ.ptr | Ap1 (Convert {dst}, _, _) -> dst @@ -273,6 +284,7 @@ and typ_of exp = |Ap3 (Conditional, typ, _, _, _) |ApN ((Record | Struct_rec), typ, _) -> typ + [@@warning "-9"] let typ = typ_of @@ -284,6 +296,9 @@ module Reg = struct type reg = t + let var r = + match Var.of_term r.term with Some v -> v | _ -> violates invariant r + module Set = struct include ( Set : @@ -295,7 +310,7 @@ module Reg = struct let empty = Set.empty (module T) let of_list = Set.of_list (module T) let union_list = Set.union_list (module T) - let of_vector = Set.of_vector (module T) + let vars = Set.fold ~init:Var.Set.empty ~f:(fun s r -> add s (var r)) end module Map = struct @@ -326,27 +341,34 @@ module Reg = struct in if !@status = 0 then demangled else None - let pp_demangled fs = function + let pp_demangled fs e = + match e.desc with | Reg {name} -> ( match demangle name with | Some demangled when not (String.equal name demangled) -> Format.fprintf fs "“%s”" demangled | _ -> () ) | _ -> () + [@@warning "-9"] let invariant x = Invariant.invariant [%here] x [%sexp_of: t] - @@ fun () -> match x with Reg _ -> invariant x | _ -> assert false + @@ fun () -> + match x.desc with Reg _ -> invariant x | _ -> assert false + + let name r = + match r.desc with Reg x -> x.name | _ -> violates invariant r - let name = function Reg {name} -> name | x -> violates invariant x - let global = function Reg {global} -> global | x -> violates invariant x + let global r = + match r.desc with Reg x -> x.global | _ -> violates invariant r - let of_exp = function - | Reg _ as x -> Some (x |> check invariant) - | _ -> None + let of_exp e = + match e.desc with Reg _ -> Some (e |> check invariant) | _ -> None let program ?global typ name = - Reg {name; typ; global= Option.is_some global} |> check invariant + { desc= Reg {name; typ; global= Option.is_some global} + ; term= Term.var (Var.program name) } + |> check invariant end (** Access *) @@ -354,7 +376,7 @@ end let fold_exps e ~init ~f = let fold_exps_ fold_exps_ e z = let z = - match e with + match e.desc with | Ap1 (_, _, x) -> fold_exps_ x z | Ap2 (_, _, x, y) -> fold_exps_ y (fold_exps_ x z) | Ap3 (_, _, w, x, y) -> fold_exps_ w (fold_exps_ y (fold_exps_ x z)) @@ -367,87 +389,194 @@ let fold_exps e ~init ~f = fix fold_exps_ (fun _ z -> z) e init let fold_regs e ~init ~f = - fold_exps e ~init ~f:(fun z -> function - | Reg _ as x -> f z (x :> Reg.t) | _ -> z ) + fold_exps e ~init ~f:(fun z x -> + match x.desc with Reg _ -> f z (x :> Reg.t) | _ -> z ) (** Construct *) let reg x = x -let nondet typ msg = Nondet {msg; typ} |> check invariant -let label ~parent ~name = Label {parent; name} |> check invariant -let integer typ data = Integer {data; typ} |> check invariant + +let nondet typ msg = + {desc= Nondet {msg; typ}; term= Term.nondet msg} |> check invariant + +let label ~parent ~name = + {desc= Label {parent; name}; term= Term.label ~parent ~name} + |> check invariant + +let integer typ data = + {desc= Integer {data; typ}; term= Term.integer data} |> check invariant + let null = integer Typ.ptr Z.zero let bool b = integer Typ.bool (Z.of_bool b) -let float typ data = Float {data; typ} |> check invariant + +let float typ data = + {desc= Float {data; typ}; term= Term.float data} |> check invariant let convert ?(unsigned = false) ~dst ~src exp = ( if (not unsigned) && Typ.equal dst src then exp - else Ap1 (Convert {unsigned; dst}, src, exp) ) + else + { desc= Ap1 (Convert {unsigned; dst}, src, exp) + ; term= Term.convert ~unsigned ~dst ~src exp.term } ) + |> check invariant + +let select typ rcd idx = + {desc= Ap1 (Select idx, typ, rcd); term= Term.select ~rcd:rcd.term ~idx} + |> check invariant + +let unsigned typ op x y = + let bits = Option.value_exn (Typ.prim_bit_size_of typ) in + op + (Term.extract ~unsigned:true ~bits x) + (Term.extract ~unsigned:true ~bits y) + +let eq typ x y = + {desc= Ap2 (Eq, typ, x, y); term= Term.eq x.term y.term} + |> check invariant + +let dq typ x y = + {desc= Ap2 (Dq, typ, x, y); term= Term.dq x.term y.term} |> check invariant -let select typ rcd idx = Ap1 (Select idx, typ, rcd) |> check invariant -let eq typ x y = Ap2 (Eq, typ, x, y) |> check invariant -let dq typ x y = Ap2 (Dq, typ, x, y) |> check invariant -let gt typ x y = Ap2 (Gt, typ, x, y) |> check invariant -let ge typ x y = Ap2 (Ge, typ, x, y) |> check invariant -let lt typ x y = Ap2 (Lt, typ, x, y) |> check invariant -let le typ x y = Ap2 (Le, typ, x, y) |> check invariant -let ugt typ x y = Ap2 (Ugt, typ, x, y) |> check invariant -let uge typ x y = Ap2 (Uge, typ, x, y) |> check invariant -let ult typ x y = Ap2 (Ult, typ, x, y) |> check invariant -let ule typ x y = Ap2 (Ule, typ, x, y) |> check invariant -let ord typ x y = Ap2 (Ord, typ, x, y) |> check invariant -let uno typ x y = Ap2 (Uno, typ, x, y) |> check invariant -let add typ x y = Ap2 (Add, typ, x, y) |> check invariant -let sub typ x y = Ap2 (Sub, typ, x, y) |> check invariant -let mul typ x y = Ap2 (Mul, typ, x, y) |> check invariant -let div typ x y = Ap2 (Div, typ, x, y) |> check invariant -let rem typ x y = Ap2 (Rem, typ, x, y) |> check invariant -let udiv typ x y = Ap2 (Udiv, typ, x, y) |> check invariant -let urem typ x y = Ap2 (Urem, typ, x, y) |> check invariant -let and_ typ x y = Ap2 (And, typ, x, y) |> check invariant -let or_ typ x y = Ap2 (Or, typ, x, y) |> check invariant -let xor typ x y = Ap2 (Xor, typ, x, y) |> check invariant -let shl typ x y = Ap2 (Shl, typ, x, y) |> check invariant -let lshr typ x y = Ap2 (Lshr, typ, x, y) |> check invariant -let ashr typ x y = Ap2 (Ashr, typ, x, y) |> check invariant +let gt typ x y = + {desc= Ap2 (Gt, typ, x, y); term= Term.lt y.term x.term} + |> check invariant + +let ge typ x y = + {desc= Ap2 (Ge, typ, x, y); term= Term.le y.term x.term} + |> check invariant + +let lt typ x y = + {desc= Ap2 (Lt, typ, x, y); term= Term.lt x.term y.term} + |> check invariant + +let le typ x y = + {desc= Ap2 (Le, typ, x, y); term= Term.le x.term y.term} + |> check invariant + +let ugt typ x y = + {desc= Ap2 (Ugt, typ, x, y); term= unsigned typ Term.lt y.term x.term} + |> check invariant + +let uge typ x y = + {desc= Ap2 (Uge, typ, x, y); term= unsigned typ Term.le y.term x.term} + |> check invariant + +let ult typ x y = + {desc= Ap2 (Ult, typ, x, y); term= unsigned typ Term.lt x.term y.term} + |> check invariant + +let ule typ x y = + {desc= Ap2 (Ule, typ, x, y); term= unsigned typ Term.le x.term y.term} + |> check invariant + +let ord typ x y = + {desc= Ap2 (Ord, typ, x, y); term= Term.ord x.term y.term} + |> check invariant + +let uno typ x y = + {desc= Ap2 (Uno, typ, x, y); term= Term.uno x.term y.term} + |> check invariant + +let add typ x y = + {desc= Ap2 (Add, typ, x, y); term= Term.add x.term y.term} + |> check invariant + +let sub typ x y = + {desc= Ap2 (Sub, typ, x, y); term= Term.sub x.term y.term} + |> check invariant + +let mul typ x y = + {desc= Ap2 (Mul, typ, x, y); term= Term.mul x.term y.term} + |> check invariant + +let div typ x y = + {desc= Ap2 (Div, typ, x, y); term= Term.div x.term y.term} + |> check invariant + +let rem typ x y = + {desc= Ap2 (Rem, typ, x, y); term= Term.rem x.term y.term} + |> check invariant + +let udiv typ x y = + {desc= Ap2 (Udiv, typ, x, y); term= unsigned typ Term.div x.term y.term} + |> check invariant + +let urem typ x y = + {desc= Ap2 (Urem, typ, x, y); term= unsigned typ Term.rem x.term y.term} + |> check invariant + +let and_ typ x y = + {desc= Ap2 (And, typ, x, y); term= Term.and_ x.term y.term} + |> check invariant + +let or_ typ x y = + {desc= Ap2 (Or, typ, x, y); term= Term.or_ x.term y.term} + |> check invariant + +let xor typ x y = + {desc= Ap2 (Xor, typ, x, y); term= Term.xor x.term y.term} + |> check invariant + +let shl typ x y = + {desc= Ap2 (Shl, typ, x, y); term= Term.shl x.term y.term} + |> check invariant + +let lshr typ x y = + {desc= Ap2 (Lshr, typ, x, y); term= Term.lshr x.term y.term} + |> check invariant + +let ashr typ x y = + {desc= Ap2 (Ashr, typ, x, y); term= Term.ashr x.term y.term} + |> check invariant let update typ ~rcd idx ~elt = - Ap2 (Update idx, typ, rcd, elt) |> check invariant + { desc= Ap2 (Update idx, typ, rcd, elt) + ; term= Term.update ~rcd:rcd.term ~idx ~elt:elt.term } + |> check invariant let conditional typ ~cnd ~thn ~els = - Ap3 (Conditional, typ, cnd, thn, els) |> check invariant + { desc= Ap3 (Conditional, typ, cnd, thn, els) + ; term= Term.conditional ~cnd:cnd.term ~thn:thn.term ~els:els.term } + |> check invariant -let record typ elts = ApN (Record, typ, elts) |> check invariant +let record typ elts = + { desc= ApN (Record, typ, elts) + ; term= Term.record (Vector.map ~f:(fun elt -> elt.term) elts) } + |> check invariant let struct_rec key = let memo_id = Hashtbl.create key in - let dummy = null in + let rec_app = (Staged.unstage (Term.rec_app key)) Term.Record in Staged.stage @@ fun ~id typ elt_thks -> match Hashtbl.find memo_id id with | None -> (* Add placeholder to prevent computing [elts] in calls to [struct_rec] from [elt_thks] for recursive occurrences of [id]. *) - let elta = Array.create ~len:(Vector.length elt_thks) dummy in + let elta = Array.create ~len:(Vector.length elt_thks) null in let elts = Vector.of_array elta in Hashtbl.set memo_id ~key:id ~data:elts ; + let term = + rec_app ~id (Vector.map ~f:(fun elt -> lazy elt.term) elts) + in Vector.iteri elt_thks ~f:(fun i (lazy elt) -> elta.(i) <- elt) ; - ApN (Struct_rec, typ, elts) |> check invariant + {desc= ApN (Struct_rec, typ, elts); term} |> check invariant | Some elts -> (* Do not check invariant as invariant will be checked above after the thunks are forced, before which invariant-checking may spuriously fail. Note that it is important that the value constructed here shares the array in the memo table, so that the update after forcing the recursive thunks also updates this value. *) - ApN (Struct_rec, typ, elts) + {desc= ApN (Struct_rec, typ, elts); term= rec_app ~id Vector.empty} (** Query *) -let is_true = function +let is_true e = + match e.desc with | Integer {data; typ= Integer {bits= 1}} -> Z.is_true data | _ -> false -let is_false = function +let is_false e = + match e.desc with | Integer {data; typ= Integer {bits= 1}} -> Z.is_false data | _ -> false diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli index aef04fb92..c2a760a74 100644 --- a/sledge/src/llair/exp.mli +++ b/sledge/src/llair/exp.mli @@ -61,7 +61,9 @@ type opN = (transitively) from [elts]. NOTE: represented by cyclic values. *) [@@deriving compare, equal, hash, sexp] -type t = +type t = private {desc: desc; term: Term.t} + +and desc = private | Reg of {name: string; typ: Typ.t; global: bool} (** Virtual register *) | Nondet of {msg: string; typ: Typ.t} (** Anonymous register with arbitrary value, representing @@ -98,8 +100,8 @@ module Reg : sig val pp : t pp val empty : t val of_list : reg list -> t - val of_vector : reg vector -> t val union_list : t list -> t + val vars : t -> Var.Set.t end module Map : sig @@ -116,6 +118,7 @@ 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 global : t -> bool end @@ -178,6 +181,7 @@ 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 val typ : t -> Typ.t diff --git a/sledge/src/symbheap/term.ml b/sledge/src/llair/term.ml similarity index 93% rename from sledge/src/symbheap/term.ml rename to sledge/src/llair/term.ml index cde3aff17..109f6544c 100644 --- a/sledge/src/symbheap/term.ml +++ b/sledge/src/llair/term.ml @@ -387,11 +387,6 @@ module Var = struct type var = t - let of_reg (r : Reg.t) = - match (r :> Exp.t) with - | Reg {name} -> Var {id= 0; name} - | _ -> violates Reg.invariant r - module Set = struct include ( Set : @@ -405,7 +400,6 @@ module Var = struct let of_option = Option.fold ~f:Set.add ~init:empty let of_list = Set.of_list (module T) let of_vector = Set.of_vector (module T) - let of_regs = Set.fold ~init:empty ~f:(fun s r -> add s (of_reg r)) end module Map = struct @@ -428,6 +422,8 @@ module Var = struct | Var _ as v -> Some (v |> check invariant) | _ -> None + let program name = Var {name; id= 0} + let fresh name ~(wrt : Set.t) = let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in let x' = Var {name; id= max + 1} in @@ -992,57 +988,6 @@ let size_of t = Option.bind (Typ.prim_bit_size_of t) ~f:(fun n -> if n % 8 = 0 then Some (integer (Z.of_int (n / 8))) else None ) -let of_exp e = - let rec_app = Staged.unstage (rec_app (module Exp)) in - let rec of_exp e = - let unsigned op typ x y = - match Typ.prim_bit_size_of typ with - | Some bits -> - op - (extract ~unsigned:true ~bits (of_exp x)) - (extract ~unsigned:true ~bits (of_exp y)) - | None -> violates Exp.invariant e - in - match e with - | Reg {name} -> var (Var {id= 0; name}) - | Nondet {msg} -> nondet msg - | Label {parent; name} -> label ~parent ~name - | Integer {data} -> integer data - | Float {data} -> float data - | Ap1 (Convert {unsigned; dst}, src, arg) -> - convert ~unsigned ~dst ~src (of_exp arg) - | Ap1 (Select idx, _, arg) -> select ~rcd:(of_exp arg) ~idx - | Ap2 (Eq, _, x, y) -> eq (of_exp x) (of_exp y) - | Ap2 (Dq, _, x, y) -> dq (of_exp x) (of_exp y) - | Ap2 (Lt, _, x, y) | Ap2 (Gt, _, y, x) -> lt (of_exp x) (of_exp y) - | Ap2 (Le, _, x, y) | Ap2 (Ge, _, y, x) -> le (of_exp x) (of_exp y) - | Ap2 (Ult, typ, x, y) | Ap2 (Ugt, typ, y, x) -> unsigned lt typ x y - | Ap2 (Ule, typ, x, y) | Ap2 (Uge, typ, y, x) -> unsigned le typ x y - | Ap2 (Ord, _, x, y) -> ord (of_exp x) (of_exp y) - | Ap2 (Uno, _, x, y) -> uno (of_exp x) (of_exp y) - | Ap2 (Add, _, x, y) -> add (of_exp x) (of_exp y) - | Ap2 (Sub, _, x, y) -> sub (of_exp x) (of_exp y) - | Ap2 (Mul, _, x, y) -> mul (of_exp x) (of_exp y) - | Ap2 (Div, _, x, y) -> div (of_exp x) (of_exp y) - | Ap2 (Rem, _, x, y) -> rem (of_exp x) (of_exp y) - | Ap2 (Udiv, typ, x, y) -> unsigned div typ x y - | Ap2 (Urem, typ, x, y) -> unsigned rem typ x y - | Ap2 (And, _, x, y) -> and_ (of_exp x) (of_exp y) - | Ap2 (Or, _, x, y) -> or_ (of_exp x) (of_exp y) - | Ap2 (Xor, _, x, y) -> xor (of_exp x) (of_exp y) - | Ap2 (Shl, _, x, y) -> shl (of_exp x) (of_exp y) - | Ap2 (Lshr, _, x, y) -> lshr (of_exp x) (of_exp y) - | Ap2 (Ashr, _, x, y) -> ashr (of_exp x) (of_exp y) - | Ap2 (Update idx, _, rcd, elt) -> - update ~rcd:(of_exp rcd) ~idx ~elt:(of_exp elt) - | Ap3 (Conditional, _, cnd, thn, els) -> - conditional ~cnd:(of_exp cnd) ~thn:(of_exp thn) ~els:(of_exp els) - | ApN (Record, _, elts) -> record (Vector.map ~f:of_exp elts) - | ApN (Struct_rec, _, elts) -> - rec_app ~id:e Record (Vector.map ~f:(fun e -> lazy (of_exp e)) elts) - in - of_exp e - (** Transform *) let map e ~f = diff --git a/sledge/src/symbheap/term.mli b/sledge/src/llair/term.mli similarity index 97% rename from sledge/src/symbheap/term.mli rename to sledge/src/llair/term.mli index 73787a11f..ec37fcf74 100644 --- a/sledge/src/symbheap/term.mli +++ b/sledge/src/llair/term.mli @@ -112,15 +112,14 @@ module Var : sig val of_option : var option -> t val of_list : var list -> t val of_vector : var vector -> t - val of_regs : Reg.Set.t -> t end val pp : t pp include Invariant.S with type t := t - val of_reg : Reg.t -> t val of_term : term -> t option + val program : string -> t val fresh : string -> wrt:Set.t -> t * Set.t val name : t -> string @@ -183,7 +182,10 @@ val update : rcd:t -> idx:int -> elt:t -> t val extract : ?unsigned:bool -> bits:int -> t -> t val convert : ?unsigned:bool -> dst:Typ.t -> src:Typ.t -> t -> t val size_of : Typ.t -> t option -val of_exp : Exp.t -> t + +val rec_app : + (module Hashtbl.Key with type t = 'id) + -> (id:'id -> recN -> t lazy_t vector -> t) Staged.t (** Access *) diff --git a/sledge/src/symbheap/term_test.ml b/sledge/src/llair/term_test.ml similarity index 94% rename from sledge/src/symbheap/term_test.ml rename to sledge/src/llair/term_test.ml index 7ad091165..3413657b0 100644 --- a/sledge/src/symbheap/term_test.ml +++ b/sledge/src/llair/term_test.ml @@ -35,19 +35,19 @@ let%test_module _ = let%test "boolean overflow" = Term.is_true - (Term.of_exp - (Exp.eq Typ.bool - (Exp.integer Typ.bool Z.minus_one) - (Exp.convert ~dst:Typ.bool ~src:Typ.siz - (Exp.integer Typ.siz Z.one)))) + (Exp.eq Typ.bool + (Exp.integer Typ.bool Z.minus_one) + (Exp.convert ~dst:Typ.bool ~src:Typ.siz + (Exp.integer Typ.siz Z.one))) + .term let%test "unsigned boolean overflow" = Term.is_true - (Term.of_exp - (Exp.uge Typ.bool - (Exp.integer Typ.bool Z.minus_one) - (Exp.convert ~dst:Typ.bool ~src:Typ.siz - (Exp.integer Typ.siz Z.one)))) + (Exp.uge Typ.bool + (Exp.integer Typ.bool Z.minus_one) + (Exp.convert ~dst:Typ.bool ~src:Typ.siz + (Exp.integer Typ.siz Z.one))) + .term let%expect_test _ = pp (!42 + !13) ; diff --git a/sledge/src/symbheap/term_test.mli b/sledge/src/llair/term_test.mli similarity index 100% rename from sledge/src/symbheap/term_test.mli rename to sledge/src/llair/term_test.mli diff --git a/sledge/src/symbheap/var.ml b/sledge/src/llair/var.ml similarity index 100% rename from sledge/src/symbheap/var.ml rename to sledge/src/llair/var.ml diff --git a/sledge/src/symbheap/var.mli b/sledge/src/llair/var.mli similarity index 100% rename from sledge/src/symbheap/var.mli rename to sledge/src/llair/var.mli diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml index 08c1ca793..656844ee3 100644 --- a/sledge/src/symbheap/exec.ml +++ b/sledge/src/symbheap/exec.ml @@ -703,38 +703,33 @@ let inst : Sh.t -> Llair.inst -> (Sh.t, unit) result = fun pre inst -> [%Trace.info "@[<2>exec inst %a from@ @[{ %a@ }@]@]" Llair.Inst.pp inst Sh.pp pre] ; - assert ( - Set.disjoint (Sh.fv pre) (Var.Set.of_regs (Llair.Inst.locals inst)) ) ; + assert (Set.disjoint (Sh.fv pre) (Reg.Set.vars (Llair.Inst.locals inst))) ; let us = pre.us in match inst with | Move {reg_exps; _} -> exec_spec pre (move_spec us - (Vector.map reg_exps ~f:(fun (r, e) -> - (Var.of_reg r, Term.of_exp e) ))) + (Vector.map reg_exps ~f:(fun (r, e) -> (Reg.var r, Exp.term e)))) | Load {reg; ptr; len; _} -> exec_spec pre - (load_spec us (Var.of_reg reg) (Term.of_exp ptr) (Term.of_exp len)) + (load_spec us (Reg.var reg) (Exp.term ptr) (Exp.term len)) | Store {ptr; exp; len; _} -> exec_spec pre - (store_spec us (Term.of_exp ptr) (Term.of_exp exp) (Term.of_exp len)) + (store_spec us (Exp.term ptr) (Exp.term exp) (Exp.term len)) | Memset {dst; byt; len; _} -> exec_spec pre - (memset_spec us (Term.of_exp dst) (Term.of_exp byt) - (Term.of_exp len)) + (memset_spec us (Exp.term dst) (Exp.term byt) (Exp.term len)) | Memcpy {dst; src; len; _} -> exec_specs pre - (memcpy_specs us (Term.of_exp dst) (Term.of_exp src) - (Term.of_exp len)) + (memcpy_specs us (Exp.term dst) (Exp.term src) (Exp.term len)) | Memmov {dst; src; len; _} -> exec_specs pre - (memmov_specs us (Term.of_exp dst) (Term.of_exp src) - (Term.of_exp len)) + (memmov_specs us (Exp.term dst) (Exp.term src) (Exp.term len)) | Alloc {reg; num; len; _} -> exec_spec pre - (alloc_spec us (Var.of_reg reg) (Term.of_exp num) (Term.of_exp len)) - | Free {ptr; _} -> exec_spec pre (free_spec us (Term.of_exp ptr)) - | Nondet {reg= Some reg; _} -> Ok (kill pre (Var.of_reg reg)) + (alloc_spec us (Reg.var reg) (Exp.term num) (Exp.term len)) + | Free {ptr; _} -> exec_spec pre (free_spec us (Exp.term ptr)) + | Nondet {reg= Some reg; _} -> Ok (kill pre (Reg.var reg)) | Nondet {reg= None; _} -> Ok pre | Abort _ -> Error () diff --git a/sledge/src/symbheap/sh_domain.ml b/sledge/src/symbheap/sh_domain.ml index d4f4bcb5a..a0025f924 100644 --- a/sledge/src/symbheap/sh_domain.ml +++ b/sledge/src/symbheap/sh_domain.ml @@ -20,24 +20,22 @@ let report_fmt_thunk = Fn.flip pp let init globals = Vector.fold globals ~init:Sh.emp ~f:(fun q -> function | {Global.reg; init= Some (arr, siz)} -> - let loc = Term.var (Var.of_reg reg) in + let loc = Term.var (Reg.var reg) in let len = Term.integer (Z.of_int siz) in - let arr = Term.of_exp arr in + let arr = arr.term in Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr}) | _ -> q ) let join l r = Some (Sh.or_ l r) let is_false = Sh.is_false -let exec_assume q b = Exec.assume q (Term.of_exp b) -let exec_kill q r = Exec.kill q (Var.of_reg r) -let exec_move q r e = Exec.move q (Var.of_reg r) (Term.of_exp e) +let exec_assume q b = Exec.assume q (Exp.term b) +let exec_kill q r = Exec.kill q (Reg.var r) +let exec_move q r e = Exec.move q (Reg.var r) (Exp.term e) let exec_inst = Exec.inst let exec_intrinsic ~skip_throw q r i es = - Exec.intrinsic ~skip_throw q - (Option.map ~f:Var.of_reg r) - (Var.of_reg i) - (List.map ~f:Term.of_exp es) + Exec.intrinsic ~skip_throw q (Option.map ~f:Reg.var r) (Reg.var i) + (List.map ~f:Exp.term es) let dnf = Sh.dnf @@ -91,10 +89,10 @@ let call ~summaries ~globals actuals areturn formals ~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: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 locals = Var.Set.of_regs locals in + 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 locals = Reg.Set.vars locals in let q', freshen_locals = Sh.freshen q ~wrt:(Set.add_list formals locals) in @@ -115,7 +113,7 @@ let call ~summaries ~globals actuals areturn formals ~locals q = let formals_set = Var.Set.of_list formals in let function_summary_pre = garbage_collect q'' - ~wrt:(Set.union formals_set (Var.Set.of_regs globals)) + ~wrt:(Set.union formals_set (Reg.Set.vars globals)) in [%Trace.info "function summary pre %a" pp function_summary_pre] ; let foot = Sh.exists formals_set function_summary_pre in @@ -140,7 +138,7 @@ let post locals _ q = [%Trace.call fun {pf} -> pf "@[locals: {@[%a@]}@ q: %a@]" Reg.Set.pp locals Sh.pp q] ; - let locals = Var.Set.of_regs locals in + let locals = Reg.Set.vars locals in Sh.exists locals q |> [%Trace.retn fun {pf} -> pf "%a" Sh.pp] @@ -154,8 +152,8 @@ let retn formals freturn {areturn; subst; frame} q = (List.pp ", " Reg.pp) formals Var.Subst.pp (Var.Subst.invert subst) pp q pp frame] ; - let formals = List.map ~f:Var.of_reg formals in - let freturn = Option.map ~f:Var.of_reg freturn in + let formals = List.map ~f:Reg.var formals in + let freturn = Option.map ~f:Reg.var freturn in let q = match (areturn, freturn) with | Some areturn, Some freturn -> Exec.move q areturn (Term.var freturn) @@ -184,8 +182,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 = Var.Set.of_regs locals in - let formals = Var.Set.of_regs formals in + let locals = Reg.Set.vars locals in + let formals = Reg.Set.vars formals in let foot = Sh.exists locals entry in let foot, subst = Sh.freshen ~wrt:(Set.union foot.us post.us) foot in let restore_formals q =