pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[sledge] Remove dead code in Exp and Term

Browse Source 
Reviewed By: bennostein

Differential Revision: D17665249

fbshipit-source-id: c242634f1
master
Josh Berdine 6 years ago committed by Facebook Github Bot
parent 442c8e92f4
commit 310d00f380
5 changed files with 2 additions and 355 deletions
Show Stats Download Patch File Download Diff File

230
sledge/src/llair/exp.ml
Unescape View File

@ -102,9 +102,8 @@ module rec T : sig
| Float of {data: string}
[@@deriving compare, equal, hash, sexp]
(* Note: solve (and invariant) requires Qset.min_elt to return a
non-coefficient, so Integer exps must compare higher than any valid
monomial *)
(* Note: invariant requires Qset.min_elt to return a non-coefficient, so
Integer exps must compare higher than any valid monomial *)
type comparator_witness
@ -209,7 +208,6 @@ type _t = T0.t
include T
let empty_map = Map.empty (module T)
let empty_qset = Qset.empty (module T)
let fix (f : (t -> 'a as 'f) -> 'f) (bot : 'f) (e : t) : 'a =
@ -376,8 +374,6 @@ let rec typ_of = function
match typ_of thn with Some _ as t -> t | None -> typ_of els )
| _ -> None
let typ = typ_of
let type_check e typ =
assert (
Option.for_all ~f:(Typ.castable typ) (typ_of e)
@ -518,7 +514,6 @@ module Reg = struct
let pp_full ?is_x vs = Set.pp (pp_full ?is_x) vs
let pp = pp_full ?is_x:None
let empty = Set.empty (module T)
let of_option = Option.fold ~f:Set.add ~init:empty
let of_list = Set.of_list (module T)
let union_list = Set.union_list (module T)
let of_vector = Set.of_vector (module T)
@ -564,7 +559,6 @@ module Reg = struct
Invariant.invariant [%here] x [%sexp_of: t]
@@ fun () -> match x with Reg _ -> invariant x | _ -> assert false
let id = function Reg {id} -> id | x -> violates invariant x
let name = function Reg {name} -> name | x -> violates invariant x
let global = function Reg {global} -> global | x -> violates invariant x
@ -574,85 +568,6 @@ module Reg = struct
let program ?global name =
Reg {id= 0; name; global= Option.is_some global} |> check invariant
let fresh name ~(wrt : Set.t) =
let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in
let x' = Reg {name; id= max + 1; global= false} in
(x', Set.add wrt x')
(** Register renaming substitutions *)
module Subst = struct
type t = T.t Map.M(T).t [@@deriving compare, equal, sexp]
let invariant s =
Invariant.invariant [%here] s [%sexp_of: t]
@@ fun () ->
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 fs s =
Format.fprintf fs "@[<1>[%a]@]"
(List.pp ",@ " (fun fs (k, v) ->
Format.fprintf fs "@[[%a ↦ %a]@]" pp_t k pp_t v ))
(Map.to_alist s)
let empty = empty_map
let is_empty = Map.is_empty
let freshen vs ~wrt =
let xs = Set.inter wrt vs in
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 extend sub ~replace ~with_ =
( match Map.add sub ~key:replace ~data:with_ with
| `Duplicate -> sub
| `Ok sub ->
Map.map_preserving_phys_equal sub ~f:(fun v ->
if T.equal v replace then with_ else v ) )
|> check invariant
let invert sub =
Map.fold sub ~init:empty ~f:(fun ~key ~data sub' ->
Map.add_exn sub' ~key:data ~data:key )
|> check invariant
let exclude sub vs =
Set.fold vs ~init:sub ~f:Map.remove |> 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 = try Map.find_exn sub v with Caml.Not_found -> v
let apply_set sub vs =
Map.fold sub ~init:vs ~f:(fun ~key ~data vs ->
let vs' = Set.remove vs key in
if Set.to_tree vs' == Set.to_tree vs then vs
else (
assert (not (Set.equal vs' vs)) ;
Set.add vs' data ) )
let close_set sub vs =
Map.fold sub ~init:vs ~f:(fun ~key:_ ~data vs -> Set.add vs data)
end
end
let fold_exps e ~init ~f =
@ -679,8 +594,6 @@ let fold_regs e ~init ~f =
fold_exps e ~init ~f:(fun z -> function
| Reg _ as x -> f z (x :> Reg.t) | _ -> z )
let fv e = fold_regs e ~f:Set.add ~init:Reg.Set.empty
(** Construct *)
let reg x = x
@ -694,9 +607,6 @@ let float data = Float {data} |> check invariant
let zero (typ : Typ.t) =
match typ with Float _ -> float "0" | _ -> integer Z.zero typ
let one (typ : Typ.t) =
match typ with Float _ -> float "1" | _ -> integer Z.one typ
let minus_one (typ : Typ.t) =
match typ with Float _ -> float "-1" | _ -> integer Z.minus_one typ
@ -917,17 +827,6 @@ let rec simp_mul2 typ e f =
(* x₁ × x₂ ==> ∏ᵢ₌₁² xᵢ *)
| _ -> Mul {args= Prod.add e (Prod.singleton f); typ}
let simp_mul typ es =
(* (bas ^ pwr) × exp *)
let rec mul_pwr bas pwr exp =
if Q.equal Q.zero pwr then exp
else mul_pwr bas Q.(pwr - one) (simp_mul2 typ bas exp)
in
let one = one typ in
Qset.fold es ~init:one ~f:(fun bas pwr exp ->
if Q.sign pwr >= 0 then mul_pwr bas pwr exp
else simp_div exp (mul_pwr bas (Q.neg pwr) one) )
let simp_negate typ x = simp_mul2 typ (minus_one typ) x
let simp_sub typ x y =
@ -1126,17 +1025,6 @@ let iter e ~f =
| Concat {args} | Struct_rec {elts= args} -> Vector.iter ~f args
| _ -> ()
let fold e ~init:s ~f =
match e with
| App {op= x; arg= y} | Splat {byt= x; siz= y} | Memory {siz= x; arr= y}
->
f y (f x s)
| Add {args} | Mul {args} ->
Qset.fold ~f:(fun e _ s -> f e s) args ~init:s
| Concat {args} | Struct_rec {elts= args} ->
Vector.fold ~f:(fun s e -> f e s) args ~init:s
| _ -> s
let is_subexp ~sub ~sup =
With_return.with_return
@@ fun {return} ->
@ -1192,8 +1080,6 @@ let app1 ?(partial = false) op arg =
let app2 op x y = app1 (app1 ~partial:true op x) y
let app3 op x y z = app1 (app1 ~partial:true (app1 ~partial:true op x) y) z
let addN typ args = simp_add typ args |> check invariant
let mulN typ args = simp_mul typ args |> check invariant
let check1 op typ x =
type_check x typ ;
@ -1293,49 +1179,6 @@ let struct_rec key =
let convert ?(signed = false) ~dst ~src exp =
app1 (Convert {signed; dst; src}) exp
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)) Typ.siz) else None
)
(** Transform *)
let map e ~f =
let map_ : (t -> t) -> t -> t =
fun map_ e ->
let map_bin mk ~f x y =
let x' = f x in
let y' = f y in
if x' == x && y' == y then e else mk x' y'
in
let map_vector mk ~f args =
let args' = Vector.map_preserving_phys_equal ~f args in
if args' == args then e else mk args'
in
let map_qset mk typ ~f args =
let args' = Qset.map ~f:(fun arg q -> (f arg, q)) args in
if args' == args then e else mk typ args'
in
match e with
| App {op; arg} -> map_bin (app1 ~partial:true) ~f op arg
| Add {args; typ} -> map_qset addN typ ~f args
| Mul {args; typ} -> map_qset mulN typ ~f args
| Splat {byt; siz} -> map_bin simp_splat ~f byt siz
| Memory {siz; arr} -> map_bin simp_memory ~f siz arr
| Concat {args} -> map_vector simp_concat ~f args
| Struct_rec {elts= args} -> Struct_rec {elts= Vector.map args ~f:map_}
| _ -> e
in
fix map_ (fun e -> e) e
let rename sub e =
let rec rename_ sub e =
match e with
| Reg _ -> Reg.Subst.apply sub e
| _ -> map ~f:(rename_ sub) e
in
rename_ sub e |> check (invariant ~partial:true)
(** Query *)
let is_true = function
@ -1345,72 +1188,3 @@ let is_true = function
let is_false = function
| Integer {data; typ= Integer {bits= 1}} -> Z.is_false data
| _ -> false
let rec is_constant e =
let is_constant_bin x y = is_constant x && is_constant y in
match e with
| Reg _ | Nondet _ -> false
| App {op= x; arg= y} | Splat {byt= x; siz= y} | Memory {siz= x; arr= y}
->
is_constant_bin x y
| Add {args} | Mul {args} ->
Qset.for_all ~f:(fun arg _ -> is_constant arg) args
| Concat {args} | Struct_rec {elts= args} ->
Vector.for_all ~f:is_constant args
| _ -> true
let classify = function
| Add _ | Mul _ -> `Interpreted
| App {op= Eq | Dq | App {op= Eq | Dq}} -> `Simplified
| App _ -> `Uninterpreted
| _ -> `Atomic
let solve e f =
[%Trace.call fun {pf} -> pf "%a@ %a" pp e pp f]
;
let rec solve_ e f s =
let solve_uninterp e f =
let ord = compare e f in
match (is_constant e, is_constant f) with
| true, true when ord <> 0 -> None
(* orient equation to discretionarily prefer exp that is constant or
compares smaller as class representative *)
| true, false -> Some (Map.add_exn s ~key:f ~data:e)
| false, true -> Some (Map.add_exn s ~key:e ~data:f)
| _ ->
let key, data = if ord > 0 then (e, f) else (f, e) in
Some (Map.add_exn s ~key ~data)
in
let concat_size args =
Vector.fold_until args ~init:(integer Z.zero Typ.siz)
~f:(fun sum -> function
| Memory {siz} -> Continue (add Typ.siz siz sum) | _ -> Stop None
)
~finish:(fun _ -> None)
in
match (e, f) with
| (Add {typ} | Mul {typ} | Integer {typ}), _
|_, (Add {typ} | Mul {typ} | Integer {typ}) -> (
match sub typ e f with
| Add {args} ->
let c, q = Qset.min_elt_exn args in
let n = Sum.to_exp typ (Qset.remove args c) in
let d = rational (Q.neg q) typ in
let r = div n d in
Some (Map.add_exn s ~key:c ~data:r)
| e_f -> solve_uninterp e_f (zero typ) )
| Concat {args= ms}, Concat {args= ns} -> (
match (concat_size ms, concat_size ns) with
| Some p, Some q -> solve_uninterp e f >>= solve_ p q
| _ -> solve_uninterp e f )
| Memory {siz= m}, Concat {args= ns} | Concat {args= ns}, Memory {siz= m}
-> (
match concat_size ns with
| Some p -> solve_uninterp e f >>= solve_ p m
| _ -> solve_uninterp e f )
| _ -> solve_uninterp e f
in
solve_ e f empty_map
|>
[%Trace.retn fun {pf} ->
function Some s -> pf "%a" Reg.Subst.pp s | None -> pf "false"]

41
sledge/src/llair/exp.mli
Unescape View File

@ -77,9 +77,7 @@ val comparator : (t, comparator_witness) Comparator.t
type exp = t
val pp_full : ?is_x:(exp -> bool) -> t pp
val pp : t pp
val invariant : ?partial:bool -> t -> unit
(** Exp.Reg is re-exported as Reg *)
module Reg : sig
@ -92,10 +90,8 @@ module Reg : sig
type t = (reg, comparator_witness) Set.t
[@@deriving compare, equal, sexp]
val pp_full : ?is_x:(exp -> bool) -> t pp
val pp : t pp
val empty : t
val of_option : reg option -> t
val of_list : reg list -> t
val of_vector : reg vector -> t
val union_list : t list -> t
@ -115,27 +111,8 @@ module Reg : sig
val of_exp : exp -> t option
val program : ?global:unit -> string -> t
val fresh : string -> wrt:Set.t -> t * Set.t
val id : t -> int
val name : t -> string
val global : t -> bool
module Subst : sig
type t [@@deriving compare, equal, sexp]
val pp : t pp
val empty : t
val freshen : Set.t -> wrt:Set.t -> t
val extend : t -> replace:reg -> with_:reg -> t
val invert : t -> t
val exclude : t -> Set.t -> t
val restrict : t -> Set.t -> t
val is_empty : t -> bool
val domain : t -> Set.t
val range : t -> Set.t
val apply_set : t -> Set.t -> Set.t
val close_set : t -> Set.t -> Set.t
end
end
(** Construct *)
@ -146,10 +123,8 @@ val label : parent:string -> name:string -> t
val null : t
val splat : byt:t -> siz:t -> t
val memory : siz:t -> arr:t -> t
val concat : t array -> t
val bool : bool -> t
val integer : Z.t -> Typ.t -> t
val rational : Q.t -> Typ.t -> t
val float : string -> t
val eq : t -> t -> t
val dq : t -> t -> t
@ -195,25 +170,9 @@ val struct_rec :
stack overflow. *)
val convert : ?signed:bool -> dst:Typ.t -> src:Typ.t -> t -> t
val size_of : Typ.t -> t option
(** Access *)
val iter : t -> f:(t -> unit) -> unit
val fold_regs : t -> init:'a -> f:('a -> Reg.t -> 'a) -> 'a
val fold_exps : t -> init:'a -> f:('a -> t -> 'a) -> 'a
val fold : t -> init:'a -> f:(t -> 'a -> 'a) -> 'a
(** Transform *)
val map : t -> f:(t -> t) -> t
val rename : Reg.Subst.t -> t -> t
(** Query *)
val fv : t -> Reg.Set.t
val is_true : t -> bool
val is_false : t -> bool
val typ : t -> Typ.t option
val classify : t -> [> `Atomic | `Interpreted | `Simplified | `Uninterpreted]
val solve : t -> t -> (t, t, comparator_witness) Map.t option

18
sledge/src/symbheap/equality_test.ml
Unescape View File

@ -112,24 +112,6 @@ let%test_module _ =
let%test _ = entails_eq r2 (f y) y
let%test _ = entails_eq r2 (f x) (f z)
let%test _ = entails_eq r2 (g x y) (g z y)
let%test _ =
entails_eq
(rename r2 Var.Subst.(extend empty ~replace:x_ ~with_:w_))
w z
let%test _ =
r2 == rename r2 Var.Subst.(extend empty ~replace:w_ ~with_:x_)
let%test _ =
entails_eq
(rename r2
Var.Subst.(
empty
|> extend ~replace:x_ ~with_:v_
|> extend ~replace:y_ ~with_:w_))
v w
let%test _ = difference (or_ r1 r2) x z |> Poly.equal None
let r3 = of_eqs [(g y z, w); (v, w); (g y w, t); (x, v); (x, u); (u, z)]

43
sledge/src/symbheap/term.ml
Unescape View File

@ -531,35 +531,8 @@ module Var = struct
with type ('key, 'value, 'cmp) t := ('key, 'value, 'cmp) Map.t )
type 'v t = 'v Map.M(T).t [@@deriving compare, equal, sexp]
let empty = Map.empty (module T)
end
let demangle =
let open Ctypes in
let cxa_demangle =
(* char *__cxa_demangle(const char *, char *, size_t *, int * ) *)
Foreign.foreign "__cxa_demangle"
( string @-> ptr char @-> ptr size_t @-> ptr int
@-> returning string_opt )
in
let null_ptr_char = from_voidp char null in
let null_ptr_size_t = from_voidp size_t null in
let status = allocate int 0 in
fun mangled ->
let demangled =
cxa_demangle mangled null_ptr_char null_ptr_size_t status
in
if !@status = 0 then demangled else None
let pp_demangled fs = function
| Var {name} -> (
match demangle name with
| Some demangled when not (String.equal name demangled) ->
Format.fprintf fs "“%s”" demangled
| _ -> () )
| _ -> ()
let invariant x =
Invariant.invariant [%here] x [%sexp_of: t]
@@ fun () -> match x with Var _ -> invariant x | _ -> assert false
@ -571,8 +544,6 @@ module Var = struct
| Var _ as v -> Some (v |> check invariant)
| _ -> None
let program name = Var {id= 0; name} |> check invariant
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
@ -611,22 +582,11 @@ module Var = struct
(sub, wrt) )
|> fst |> check invariant
let extend sub ~replace ~with_ =
( match Map.add sub ~key:replace ~data:with_ with
| `Duplicate -> sub
| `Ok sub ->
Map.map_preserving_phys_equal sub ~f:(fun v ->
if T.equal v replace then with_ else v ) )
|> check invariant
let invert sub =
Map.fold sub ~init:empty ~f:(fun ~key ~data sub' ->
Map.add_exn sub' ~key:data ~data:key )
|> check invariant
let exclude sub vs =
Set.fold vs ~init:sub ~f:Map.remove |> check invariant
let restrict sub vs =
Map.filter_keys ~f:(Set.mem vs) sub |> check invariant
@ -647,9 +607,6 @@ module Var = struct
else (
assert (not (Set.equal vs' vs)) ;
Set.add vs' data ) )
let close_set sub vs =
Map.fold sub ~init:vs ~f:(fun ~key:_ ~data vs -> Set.add vs data)
end
end

25
sledge/src/symbheap/term.mli
Unescape View File

@ -100,23 +100,13 @@ module Var : sig
val of_regs : Reg.Set.t -> t
end
module Map : sig
type 'a t = (var, 'a, comparator_witness) Map.t
[@@deriving compare, equal, sexp]
val empty : 'a t
end
val pp : t pp
val pp_demangled : 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 id : t -> int
val name : t -> string
module Subst : sig
@ -125,15 +115,12 @@ module Var : sig
val pp : t pp
val empty : t
val freshen : Set.t -> wrt:Set.t -> t
val extend : t -> replace:var -> with_:var -> t
val invert : t -> t
val exclude : t -> Set.t -> t
val restrict : t -> Set.t -> t
val is_empty : t -> bool
val domain : t -> Set.t
val range : t -> Set.t
val apply_set : t -> Set.t -> Set.t
val close_set : t -> Set.t -> Set.t
end
end
@ -182,18 +169,6 @@ val conditional : cnd:t -> thn:t -> els:t -> t
val record : t list -> t
val select : rcd:t -> idx:t -> t
val update : rcd:t -> elt:t -> idx:t -> t
val struct_rec :
(module Hashtbl.Key with type t = 'id)
-> (id:'id -> t lazy_t vector -> t) Staged.t
(** [struct_rec Id id element_thunks] constructs a possibly-cyclic [Struct]
value. Cycles are detected using [Id]. The caller of [struct_rec Id]
must ensure that a single unstaging of [struct_rec Id] is used for each
complete cyclic value. Also, the caller must ensure that recursive calls
to [struct_rec Id] provide [id] values that uniquely identify at least
one point on each cycle. Failure to obey these requirements will lead to
stack overflow. *)
val convert : ?signed:bool -> dst:Typ.t -> src:Typ.t -> t -> t
val size_of : Typ.t -> t option

Write Preview
Loading…
Cancel
Save