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

[sledge] Do not use Base.Map to implement Qset

Browse Source 
Reviewed By: ngorogiannis

Differential Revision: D20482766

fbshipit-source-id: 9884fc6cf
master
Josh Berdine 5 years ago committed by Facebook GitHub Bot
parent 152cc38e9b
commit 434c40e646
9 changed files with 224 additions and 270 deletions
Show Stats Download Patch File Download Diff File

4
sledge/bin/domain_itv.ml
Unescape View File

@ -74,7 +74,7 @@ let rec pow base typ = function
* (See sledge/src/llair/term.ml functions assert_(mono|poly)mial for details)
*)
let rec texpr_of_nary_term subtms typ q op =
assert (Qset.length subtms >= 2) ;
assert (Term.Qset.length subtms >= 2) ;
let term_to_texpr (tm, coeff) =
let* base = apron_texpr_of_llair_term tm q typ in
match op with
@ -87,7 +87,7 @@ let rec texpr_of_nary_term subtms typ q op =
Some (pow base typ (Q.to_int coeff))
| _ -> None
in
match Qset.to_list subtms with
match Term.Qset.to_list subtms with
| hd :: tl ->
List.fold tl ~init:(term_to_texpr hd) ~f:(fun acc curr ->
let* c = term_to_texpr curr in

7
sledge/lib/import/import.ml
Unescape View File

@ -121,12 +121,7 @@ module Vector = Vector
include Vector.Infix
module Set = Set
module Map = Map
module Qset = struct
include Qset
let pp sep pp_elt fs s = List.pp sep pp_elt fs (to_list s)
end
module Qset = Qset
module Array = struct
include Base.Array

7
sledge/lib/import/import.mli
Unescape View File

@ -114,12 +114,7 @@ module Vector = Vector
include module type of Vector.Infix
module Set = Set
module Map = Map
module Qset : sig
include module type of Qset
val pp : (unit, unit) fmt -> ('a * Q.t) pp -> ('a, _) t pp
end
module Qset = Qset
module Array : sig
include module type of Base.Array

1
sledge/lib/import/import0.ml
Unescape View File

@ -11,6 +11,7 @@ type 'a pp = Format.formatter -> 'a -> unit
(** Format strings. *)
type ('a, 'b) fmt = ('a, 'b) Trace.fmt
module Hash = Ppx_hash_lib.Std.Hash
module Sexp = Sexplib.Sexp
module type Applicative_syntax = sig

226
sledge/lib/import/qset.ml
Unescape View File

@ -7,112 +7,134 @@
(** Qset - Set with (signed) rational multiplicity for each element *)
open Base
open Import0
type ('elt, 'cmp) t = ('elt, Q.t, 'cmp) Map.t
module M (Elt : sig
module type S = sig
type elt
type t
type comparator_witness
end) =
struct
type nonrec t = (Elt.t, Elt.comparator_witness) t
end
module type Sexp_of_m = sig
type t [@@deriving sexp_of]
end
val compare : t -> t -> int
val equal : t -> t -> bool
val hash_fold_t : elt Hash.folder -> t Hash.folder
val sexp_of_t : t -> Sexp.t
val t_of_sexp : (Sexp.t -> elt) -> Sexp.t -> t
val pp : (unit, unit) fmt -> (elt * Q.t) pp -> t pp
val empty : t
(** The empty multiset over the provided order. *)
val add : t -> elt -> Q.t -> t
(** Add to multiplicity of single element. [O(log n)] *)
val remove : t -> elt -> t
(** Set the multiplicity of an element to zero. [O(log n)] *)
val union : t -> t -> t
(** Sum multiplicities pointwise. [O(n + m)] *)
val length : t -> int
(** Number of elements with non-zero multiplicity. [O(1)]. *)
module type M_of_sexp = sig
type t [@@deriving of_sexp]
val count : t -> elt -> Q.t
(** Multiplicity of an element. [O(log n)]. *)
include Comparator.S with type t := t
val map : t -> f:(elt -> Q.t -> elt * Q.t) -> t
(** Map over the elements in ascending order. Preserves physical equality
if [f] does. *)
val map_counts : t -> f:(elt -> Q.t -> Q.t) -> t
(** Map over the multiplicities of the elements in ascending order. *)
val fold : t -> f:(elt -> Q.t -> 's -> 's) -> init:'s -> 's
(** Fold over the elements in ascending order. *)
val iter : t -> f:(elt -> Q.t -> unit) -> unit
(** Iterate over the elements in ascending order. *)
val exists : t -> f:(elt -> Q.t -> bool) -> bool
(** Search for an element satisfying a predicate. *)
val min_elt : t -> (elt * Q.t) option
(** Minimum element. *)
val min_elt_exn : t -> elt * Q.t
(** Minimum element. *)
val to_list : t -> (elt * Q.t) list
(** Convert to a list of elements in ascending order. *)
end
module type Compare_m = sig end
module type Hash_fold_m = Hasher.S
let sexp_of_q q = Sexp.Atom (Q.to_string q)
let q_of_sexp = function Sexp.Atom s -> Q.of_string s | _ -> assert false
let hash_fold_q state q = Hash.fold_int state (Hashtbl.hash q)
let sexp_of_m__t (type elt) (module Elt : Sexp_of_m with type t = elt) t =
Map.sexp_of_m__t (module Elt) sexp_of_q t
let m__t_of_sexp (type elt cmp)
(module Elt : M_of_sexp
with type t = elt
and type comparator_witness = cmp) sexp =
Map.m__t_of_sexp (module Elt) q_of_sexp sexp
let compare_m__t (module Elt : Compare_m) = Map.compare_direct Q.compare
let equal_m__t (module Elt : Compare_m) = Map.equal Q.equal
let hash_fold_m__t (type elt) (module Elt : Hash_fold_m with type t = elt)
state =
Map.hash_fold_m__t (module Elt) hash_fold_q state
let hash_m__t (type elt) (module Elt : Hash_fold_m with type t = elt) =
Hash.of_fold (hash_fold_m__t (module Elt))
type ('elt, 'cmp) comparator =
(module Comparator.S with type t = 'elt and type comparator_witness = 'cmp)
let empty cmp = Map.empty cmp
let if_nz q = if Q.equal Q.zero q then None else Some q
let add m x i =
Map.change m x ~f:(function Some j -> if_nz Q.(i + j) | None -> if_nz i)
let remove m x = Map.remove m x
let union m n =
Map.merge m n ~f:(fun ~key:_ -> function
| `Both (i, j) -> if_nz Q.(i + j) | `Left i | `Right i -> Some i )
let length m = Map.length m
let count m x = match Map.find m x with Some q -> q | None -> Q.zero
let count_and_remove m x =
let found = ref Q.zero in
let m =
Map.change m x ~f:(function
| None -> None
| Some i ->
found := i ;
None )
in
if Q.equal !found Q.zero then None else Some (!found, m)
let min_elt = Map.min_elt
let min_elt_exn = Map.min_elt_exn
let fold m ~f ~init = Map.fold m ~f:(fun ~key ~data s -> f key data s) ~init
let map m ~f =
let m' = Map.empty (Map.comparator_s m) in
let m, m' =
fold m ~init:(m, m') ~f:(fun x i (m, m') ->
let x', i' = f x i in
if phys_equal x' x then
if Q.equal i' i then (m, m') else (Map.set m ~key:x ~data:i', m')
else (Map.remove m x, add m' x' i') )
in
fold m' ~init:m ~f:(fun x i m -> add m x i)
let fold_map m ~f ~init:s =
let m' = Map.empty (Map.comparator_s m) in
let m, m', s =
fold m ~init:(m, m', s) ~f:(fun x i (m, m', s) ->
let x', i', s = f x i s in
if phys_equal x' x then
if Q.equal i' i then (m, m', s)
else (Map.set m ~key:x ~data:i', m', s)
else (Map.remove m x, add m' x' i', s) )
in
(fold m' ~init:m ~f:(fun x i m -> add m x i), s)
let for_all m ~f = Map.for_alli m ~f:(fun ~key ~data -> f key data)
let map_counts m ~f = Map.mapi m ~f:(fun ~key ~data -> f key data)
let iter m ~f = Map.iteri m ~f:(fun ~key ~data -> f key data)
let exists m ~f = Map.existsi m ~f:(fun ~key ~data -> f key data)
let to_list m = Map.to_alist m
module Make (Elt : OrderedType) = struct
module M = Stdlib.Map.Make (Elt)
type elt = Elt.t
type t = Q.t M.t
let compare = M.compare Q.compare
let equal = M.equal Q.equal
let hash_fold_t hash_fold_elt s m =
let hash_fold_q s q = Hash.fold_int s (Hashtbl.hash q) in
M.fold
(fun key data state -> hash_fold_q (hash_fold_elt state key) data)
m
(Hash.fold_int s (M.cardinal m))
let sexp_of_t s =
let sexp_of_q q = Sexp.Atom (Q.to_string q) in
List.sexp_of_t
(Sexplib.Conv.sexp_of_pair Elt.sexp_of_t sexp_of_q)
(M.bindings s)
let t_of_sexp elt_of_sexp sexp =
let q_of_sexp = function
| Sexp.Atom s -> Q.of_string s
| _ -> assert false
in
List.fold_left
~f:(fun m (k, v) -> M.add k v m)
~init:M.empty
(List.t_of_sexp
(Sexplib.Conv.pair_of_sexp elt_of_sexp q_of_sexp)
sexp)
let pp sep pp_elt fs s = List.pp sep pp_elt fs (M.bindings s)
let empty = M.empty
let if_nz q = if Q.equal Q.zero q then None else Some q
let add m x i =
M.update x (function Some j -> if_nz Q.(i + j) | None -> if_nz i) m
let remove m x = M.remove x m
let union m n =
M.merge
(fun _ m_q n_q ->
match (m_q, n_q) with
| Some i, Some j -> if_nz Q.(i + j)
| Some i, None | None, Some i -> Some i
| None, None -> None )
m n
let length m = M.cardinal m
let count m x = try M.find x m with Not_found -> Q.zero
let fold m ~f ~init = M.fold (fun key data s -> f key data s) m init
let map m ~f =
let m' = M.empty in
let m, m' =
fold m ~init:(m, m') ~f:(fun x i (m, m') ->
let x', i' = f x i in
if x' == x then
if Q.equal i' i then (m, m') else (M.add x i' m, m')
else (M.remove x m, add m' x' i') )
in
fold m' ~init:m ~f:(fun x i m -> add m x i)
let map_counts m ~f = M.mapi (fun key data -> f key data) m
let iter m ~f = M.iter (fun key data -> f key data) m
let exists m ~f = M.exists (fun key data -> f key data) m
let min_elt = M.min_binding_opt
let min_elt_exn = M.min_binding
let to_list m = M.bindings m
end

129
sledge/lib/import/qset.mli
Unescape View File

@ -7,110 +7,61 @@
(** Qset - Set with (signed) rational multiplicity for each element *)
open Base
open Import0
type ('elt, 'cmp) t
type ('elt, 'cmp) comparator =
(module Comparator.S with type t = 'elt and type comparator_witness = 'cmp)
module M (Elt : sig
module type S = sig
type elt
type t
type comparator_witness
end) : sig
type nonrec t = (Elt.t, Elt.comparator_witness) t
end
module type Sexp_of_m = sig
type t [@@deriving sexp_of]
end
module type M_of_sexp = sig
type t [@@deriving of_sexp]
include Comparator.S with type t := t
end
module type Compare_m = sig end
module type Hash_fold_m = Hasher.S
val sexp_of_m__t :
(module Sexp_of_m with type t = 'elt) -> ('elt, 'cmp) t -> Sexp.t
val compare : t -> t -> int
val equal : t -> t -> bool
val hash_fold_t : elt Hash.folder -> t Hash.folder
val sexp_of_t : t -> Sexp.t
val t_of_sexp : (Sexp.t -> elt) -> Sexp.t -> t
val pp : (unit, unit) fmt -> (elt * Q.t) pp -> t pp
val m__t_of_sexp :
(module M_of_sexp with type t = 'elt and type comparator_witness = 'cmp)
-> Sexp.t
-> ('elt, 'cmp) t
val empty : t
(** The empty multiset over the provided order. *)
val compare_m__t :
(module Compare_m) -> ('elt, 'cmp) t -> ('elt, 'cmp) t -> int
val add : t -> elt -> Q.t -> t
(** Add to multiplicity of single element. [O(log n)] *)
val equal_m__t :
(module Compare_m) -> ('elt, 'cmp) t -> ('elt, 'cmp) t -> bool
val remove : t -> elt -> t
(** Set the multiplicity of an element to zero. [O(log n)] *)
val hash_fold_m__t :
(module Hash_fold_m with type t = 'elt)
-> Hash.state
-> ('elt, _) t
-> Hash.state
val union : t -> t -> t
(** Sum multiplicities pointwise. [O(n + m)] *)
val hash_m__t :
(module Hash_fold_m with type t = 'elt) -> ('elt, _) t -> Hash.hash_value
val length : t -> int
(** Number of elements with non-zero multiplicity. [O(1)]. *)
val empty : ('elt, 'cmp) comparator -> ('elt, 'cmp) t
(** The empty multiset over the provided order. *)
val count : t -> elt -> Q.t
(** Multiplicity of an element. [O(log n)]. *)
val add : ('a, 'c) t -> 'a -> Q.t -> ('a, 'c) t
(** Add to multiplicity of single element. [O(log n)] *)
val map : t -> f:(elt -> Q.t -> elt * Q.t) -> t
(** Map over the elements in ascending order. Preserves physical equality
if [f] does. *)
val remove : ('a, 'c) t -> 'a -> ('a, 'c) t
(** Set the multiplicity of an element to zero. [O(log n)] *)
val map_counts : t -> f:(elt -> Q.t -> Q.t) -> t
(** Map over the multiplicities of the elements in ascending order. *)
val union : ('a, 'c) t -> ('a, 'c) t -> ('a, 'c) t
(** Sum multiplicities pointwise. [O(n + m)] *)
val fold : t -> f:(elt -> Q.t -> 's -> 's) -> init:'s -> 's
(** Fold over the elements in ascending order. *)
val length : _ t -> int
(** Number of elements with non-zero multiplicity. [O(1)]. *)
val iter : t -> f:(elt -> Q.t -> unit) -> unit
(** Iterate over the elements in ascending order. *)
val count : ('a, _) t -> 'a -> Q.t
(** Multiplicity of an element. [O(log n)]. *)
val exists : t -> f:(elt -> Q.t -> bool) -> bool
(** Search for an element satisfying a predicate. *)
val count_and_remove : ('a, 'c) t -> 'a -> (Q.t * ('a, 'c) t) option
(** Multiplicity of an element, and remove it. [O(log n)]. *)
val min_elt : t -> (elt * Q.t) option
(** Minimum element. *)
val map : ('a, 'c) t -> f:('a -> Q.t -> 'a * Q.t) -> ('a, 'c) t
(** Map over the elements in ascending order. Preserves physical equality if
[f] does. *)
val min_elt_exn : t -> elt * Q.t
(** Minimum element. *)
val map_counts : ('a, 'c) t -> f:('a -> Q.t -> Q.t) -> ('a, 'c) t
(** Map over the multiplicities of the elements in ascending order. *)
val fold : ('a, _) t -> f:('a -> Q.t -> 's -> 's) -> init:'s -> 's
(** Fold over the elements in ascending order. *)
val fold_map :
('a, 'c) t
-> f:('a -> Q.t -> 's -> 'a * Q.t * 's)
-> init:'s
-> ('a, 'c) t * 's
(** Folding map over the elements in ascending order. Preserves physical
equality if [f] does. *)
val for_all : ('a, _) t -> f:('a -> Q.t -> bool) -> bool
(** Universal property test. [O(n)] but returns as soon as a violation is
found, in ascending order. *)
val iter : ('a, _) t -> f:('a -> Q.t -> unit) -> unit
(** Iterate over the elements in ascending order. *)
val exists : ('a, _) t -> f:('a -> Q.t -> bool) -> bool
(** Search for an element satisfying a predicate. *)
val min_elt : ('a, _) t -> ('a * Q.t) option
(** Minimum element. *)
val min_elt_exn : ('a, _) t -> 'a * Q.t
(** Minimum element. *)
val to_list : t -> (elt * Q.t) list
(** Convert to a list of elements in ascending order. *)
end
val to_list : ('a, _) t -> ('a * Q.t) list
(** Convert to a list of elements in ascending order. *)
module Make (Elt : OrderedType) : S with type elt = Elt.t

2
sledge/lib/sh.ml
Unescape View File

@ -180,7 +180,7 @@ let pp_block x fs segs =
let pp_heap x ?pre cong fs heap =
let bas_off = function
| Term.Add poly as sum ->
let const = Qset.count poly Term.one in
let const = Term.Qset.count poly Term.one in
(Term.sub sum (Term.rational const), const)
| e -> (e, Q.zero)
in

58
sledge/lib/term.ml
Unescape View File

@ -40,38 +40,22 @@ type op3 = Conditional | Extract [@@deriving compare, equal, hash, sexp]
type opN = Concat | Record [@@deriving compare, equal, hash, sexp]
type recN = Record [@@deriving compare, equal, hash, sexp]
module rec T : sig
type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
module rec Qset : sig
include Import.Qset.S with type elt := T.t
type t =
| Add of qset
| Mul of qset
| Var of {id: int; name: string}
| Ap1 of op1 * t
| Ap2 of op2 * t * t
| Ap3 of op3 * t * t * t
| ApN of opN * t vector
| RecN of recN * t vector (** NOTE: cyclic *)
| Label of {parent: string; name: string}
| Nondet of {msg: string}
| Float of {data: string}
| Integer of {data: Z.t}
[@@deriving compare, equal, hash, sexp]
(* Note: solve (and invariant) requires Qset.min_elt to return a
non-coefficient, so Integer terms must compare higher than any valid
monomial *)
type comparator_witness
val comparator : (t, comparator_witness) Comparator.t
val hash : t -> int
val hash_fold_t : t Hash.folder
val t_of_sexp : Sexp.t -> t
end = struct
include T0 include Comparator.Make (T0)
include Import.Qset.Make (T)
let hash_fold_t = hash_fold_t T.hash_fold_t
let hash = Hash.of_fold hash_fold_t
let t_of_sexp = t_of_sexp T.t_of_sexp
end
(* auxiliary definition for safe recursive module initialization *)
and T0 : sig
type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
and T : sig
type qset = Qset.t [@@deriving compare, equal, hash, sexp]
type t =
| Add of qset
@ -81,14 +65,14 @@ and T0 : sig
| Ap2 of op2 * t * t
| Ap3 of op3 * t * t * t
| ApN of opN * t vector
| RecN of recN * t vector
| RecN of recN * t vector (** NOTE: cyclic *)
| Label of {parent: string; name: string}
| Nondet of {msg: string}
| Float of {data: string}
| Integer of {data: Z.t}
[@@deriving compare, equal, hash, sexp]
end = struct
type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
type qset = Qset.t [@@deriving compare, equal, hash, sexp]
type t =
| Add of qset
@ -98,13 +82,16 @@ end = struct
| Ap2 of op2 * t * t
| Ap3 of op3 * t * t * t
| ApN of opN * t vector
| RecN of recN * t vector
| RecN of recN * t vector (** NOTE: cyclic *)
| Label of {parent: string; name: string}
| Nondet of {msg: string}
| Float of {data: string}
| Integer of {data: Z.t}
[@@deriving compare, equal, hash, sexp]
(* Note: solve (and invariant) requires Qset.min_elt to return a
non-coefficient, so Integer terms must compare higher than any valid
monomial *)
let compare x y =
match (x, y) with
| Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
@ -112,9 +99,6 @@ end = struct
| _ -> compare x y
end
(* suppress spurious "Warning 60: unused module T0." *)
type _t = T0.t
include T
module Map = Map.Make (T)
@ -124,8 +108,6 @@ module Set = struct
let t_of_sexp = t_of_sexp T.t_of_sexp
end
let empty_qset = Qset.empty (module T)
let fix (f : (t -> 'a as 'f) -> 'f) (bot : 'f) (e : t) : 'a =
let rec fix_f seen e =
match e with
@ -462,7 +444,7 @@ let simp_convert src dst arg =
elements are Xᵢ with multiplicities cᵢ. A constant is treated as the
coefficient of the empty monomial, which is the unit of multiplication 1. *)
module Sum = struct
let empty = empty_qset
let empty = Qset.empty
let add coeff term sum =
assert (not (Q.equal Q.zero coeff)) ;
@ -486,7 +468,7 @@ end
of indeterminates xᵢ is represented by a multiset where the elements are
xᵢ and the multiplicities are the exponents nᵢ. *)
module Prod = struct
let empty = empty_qset
let empty = Qset.empty
let add term prod =
assert (match term with Integer _ -> false | _ -> true) ;

60
sledge/lib/term.mli
Unescape View File

@ -60,37 +60,45 @@ type opN =
type recN = Record (** Recursive record (array / struct) constant *)
[@@deriving compare, equal, hash, sexp]
type comparator_witness
type qset = (t, comparator_witness) Qset.t
and t = private
| Add of qset (** Sum of terms with rational coefficients *)
| Mul of qset (** Product of terms with rational exponents *)
| Var of {id: int; name: string} (** Local variable / virtual register *)
| Ap1 of op1 * t (** Unary application *)
| Ap2 of op2 * t * t (** Binary application *)
| Ap3 of op3 * t * t * t (** Ternary application *)
| ApN of opN * t vector (** N-ary application *)
| RecN of recN * t vector
(** Recursive n-ary application, may recursively refer to itself
(transitively) from its args. NOTE: represented by cyclic values. *)
| Label of {parent: string; name: string}
(** Address of named code block within parent function *)
| Nondet of {msg: string}
(** Anonymous local variable with arbitrary value, representing
non-deterministic approximation of value described by [msg] *)
| Float of {data: string} (** Floating-point constant *)
| Integer of {data: Z.t} (** Integer constant *)
[@@deriving compare, equal, hash, sexp]
module rec Qset : sig
include Import.Qset.S with type elt := T.t
val hash_fold_t : t Hash.folder
val t_of_sexp : Sexp.t -> t
end
and T : sig
type qset = Qset.t [@@deriving compare, equal, hash, sexp]
and t = private
| Add of qset (** Sum of terms with rational coefficients *)
| Mul of qset (** Product of terms with rational exponents *)
| Var of {id: int; name: string}
(** Local variable / virtual register *)
| Ap1 of op1 * t (** Unary application *)
| Ap2 of op2 * t * t (** Binary application *)
| Ap3 of op3 * t * t * t (** Ternary application *)
| ApN of opN * t vector (** N-ary application *)
| RecN of recN * t vector
(** Recursive n-ary application, may recursively refer to itself
(transitively) from its args. NOTE: represented by cyclic
values. *)
| Label of {parent: string; name: string}
(** Address of named code block within parent function *)
| Nondet of {msg: string}
(** Anonymous local variable with arbitrary value, representing
non-deterministic approximation of value described by [msg] *)
| Float of {data: string} (** Floating-point constant *)
| Integer of {data: Z.t} (** Integer constant *)
[@@deriving compare, equal, hash, sexp]
end
include module type of T with type t = T.t
(** Term.Var is re-exported as Var *)
module Var : sig
type term := t
type t = private term [@@deriving compare, equal, hash, sexp]
include Comparator.S with type t := t
type strength = t -> [`Universal | `Existential | `Anonymous] option
module Map : Map.S with type key := t

Write Preview
Loading…
Cancel
Save