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

[sledge] Do not use Base.Set

Browse Source 
Summary:
The base containers have inconvenient interfaces due to lacking
support for functors, which also leads to the representation of values
of containers including closures for the comparison functions. This
causes problems when `Marshal`ing these values.

This diff is one step toward not using the base containers.

Reviewed By: ngorogiannis

Differential Revision: D20482756

fbshipit-source-id: 0312c422d
master
Josh Berdine 5 years ago committed by Facebook GitHub Bot
parent 57a8748e9f
commit 124a1fed20
17 changed files with 497 additions and 406 deletions
Show Stats Download Patch File Download Diff File

6
sledge/bin/domain_itv.ml
Unescape View File

@ -219,9 +219,9 @@ let exec_move q move_vec =
let defs, uses = let defs, uses =
Vector.fold move_vec ~init:(Reg.Set.empty, Reg.Set.empty) Vector.fold move_vec ~init:(Reg.Set.empty, Reg.Set.empty)
~f:(fun (defs, uses) (r, e) -> ~f:(fun (defs, uses) (r, e) ->
(Set.add defs r, Exp.fold_regs e ~init:uses ~f:Set.add) ) (Reg.Set.add defs r, Exp.fold_regs e ~init:uses ~f:Reg.Set.add) )
in in
assert (Set.disjoint defs uses) ; assert (Reg.Set.disjoint defs uses) ;
Vector.fold move_vec ~init:q ~f:(fun a (r, e) -> assign r e a) Vector.fold move_vec ~init:q ~f:(fun a (r, e) -> assign r e a)
let exec_inst q i = let exec_inst q i =
@ -259,7 +259,7 @@ let recursion_beyond_bound = `prune
(** existentially quantify locals *) (** existentially quantify locals *)
let post locals _ (q : t) = let post locals _ (q : t) =
let locals = let locals =
Set.fold locals ~init:[] ~f:(fun a r -> Reg.Set.fold locals ~init:[] ~f:(fun a r ->
let v = apron_var_of_reg r in let v = apron_var_of_reg r in
if Environment.mem_var q.env v then v :: a else a ) if Environment.mem_var q.env v then v :: a else a )
|> Array.of_list |> Array.of_list

2
sledge/bin/sledge.ml
Unescape View File

@ -85,7 +85,7 @@ let used_globals pgm preanalyze : Domain_used_globals.r =
else else
Declared Declared
(Vector.fold pgm.globals ~init:Reg.Set.empty ~f:(fun acc g -> (Vector.fold pgm.globals ~init:Reg.Set.empty ~f:(fun acc g ->
Set.add acc g.reg )) Reg.Set.add acc g.reg ))
let analyze = let analyze =
let%map_open bound = let%map_open bound =

2
sledge/lib/control.ml
Unescape View File

@ -319,7 +319,7 @@ module Make (Dom : Domain_intf.Dom) = struct
in in
let function_summary, post_state = let function_summary, post_state =
Dom.create_summary ~locals post_state Dom.create_summary ~locals post_state
~formals:(Set.union (Reg.Set.of_list formals) globals) ~formals:(Reg.Set.union (Reg.Set.of_list formals) globals)
in in
Hashtbl.add_multi summary_table ~key:name.reg ~data:function_summary ; Hashtbl.add_multi summary_table ~key:name.reg ~data:function_summary ;
pp_st () ; pp_st () ;

48
sledge/lib/domain_sh.ml
Unescape View File

@ -81,7 +81,7 @@ let term_eq_class_has_only_vars_in fvs cong term =
Equality.pp cong Term.pp term] Equality.pp cong Term.pp term]
; ;
let term_has_only_vars_in fvs term = let term_has_only_vars_in fvs term =
Set.is_subset (Term.fv term) ~of_:fvs Var.Set.is_subset (Term.fv term) ~of_:fvs
in in
let term_eq_class = Equality.class_of cong term in let term_eq_class = Equality.class_of cong term in
List.exists ~f:(term_has_only_vars_in fvs) term_eq_class List.exists ~f:(term_has_only_vars_in fvs) term_eq_class
@ -100,7 +100,7 @@ let garbage_collect (q : t) ~wrt =
List.fold ~init:current q.heap ~f:(fun current seg -> List.fold ~init:current q.heap ~f:(fun current seg ->
if term_eq_class_has_only_vars_in current q.cong seg.loc then if term_eq_class_has_only_vars_in current q.cong seg.loc then
List.fold (Equality.class_of q.cong seg.arr) ~init:current List.fold (Equality.class_of q.cong seg.arr) ~init:current
~f:(fun c e -> Set.union c (Term.fv e)) ~f:(fun c e -> Var.Set.union c (Term.fv e))
else current ) else current )
in in
all_reachable_vars current new_set q all_reachable_vars current new_set q
@ -121,10 +121,10 @@ let and_eqs sub formals actuals q =
let localize_entry globals actuals formals freturn locals subst pre entry = 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 *) (* Add the formals here to do garbage collection and then get rid of them *)
let formals_set = Var.Set.of_list formals in let formals_set = Var.Set.of_list formals in
let freturn_locals = Reg.Set.vars (Set.add_option freturn locals) in let freturn_locals = Reg.Set.vars (Reg.Set.add_option freturn locals) in
let function_summary_pre = let function_summary_pre =
garbage_collect entry garbage_collect entry
~wrt:(Set.union formals_set (Reg.Set.vars globals)) ~wrt:(Var.Set.union formals_set (Reg.Set.vars globals))
in in
[%Trace.info "function summary pre %a" pp function_summary_pre] ; [%Trace.info "function summary pre %a" pp function_summary_pre] ;
let foot = Sh.exists formals_set function_summary_pre in let foot = Sh.exists formals_set function_summary_pre in
@ -156,18 +156,23 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q =
let actuals = List.map ~f:Exp.term actuals in let actuals = List.map ~f:Exp.term actuals in
let areturn = Option.map ~f:Reg.var areturn in let areturn = Option.map ~f:Reg.var areturn in
let formals = List.map ~f:Reg.var formals in let formals = List.map ~f:Reg.var formals in
let freturn_locals = Reg.Set.vars (Set.add_option freturn locals) in let freturn_locals = Reg.Set.vars (Reg.Set.add_option freturn locals) in
let modifs = Var.Set.of_option areturn in let modifs = Var.Set.of_option areturn in
(* quantify modifs, their current value will be overwritten and so does (* quantify modifs, their current value will be overwritten and so does
not need to be saved in the freshening renaming *) not need to be saved in the freshening renaming *)
let q = Sh.exists modifs q in let q = Sh.exists modifs q in
(* save current values of shadowed formals and locals with a renaming *) (* save current values of shadowed formals and locals with a renaming *)
let q', subst = Sh.freshen q ~wrt:(Set.add_list formals freturn_locals) in let q', subst =
assert (Set.disjoint modifs (Var.Subst.domain subst)) ; Sh.freshen q ~wrt:(Var.Set.add_list formals freturn_locals)
in
assert (Var.Set.disjoint modifs (Var.Subst.domain subst)) ;
(* pass arguments by conjoining equations between formals and actuals *) (* pass arguments by conjoining equations between formals and actuals *)
let entry = and_eqs subst formals actuals q' in let entry = and_eqs subst formals actuals q' in
(* note: locals and formals are in scope *) (* note: locals and formals are in scope *)
assert (Set.is_subset (Set.add_list formals freturn_locals) ~of_:entry.us) ; assert (
Var.Set.is_subset
(Var.Set.add_list formals freturn_locals)
~of_:entry.us ) ;
(* simplify *) (* simplify *)
let entry = simplify entry in let entry = simplify entry in
( if not summaries then (entry, {areturn; subst; frame= Sh.emp}) ( if not summaries then (entry, {areturn; subst; frame= Sh.emp})
@ -218,7 +223,9 @@ let retn formals freturn {areturn; subst; frame} q =
| None -> (q, inv_subst) | None -> (q, inv_subst)
in in
(* exit scope of formals *) (* exit scope of formals *)
let q = Sh.exists (Set.add_list formals (Var.Set.of_option freturn)) q in let q =
Sh.exists (Var.Set.add_list formals (Var.Set.of_option freturn)) q
in
(* reinstate shadowed values of locals *) (* reinstate shadowed values of locals *)
let q = Sh.rename inv_subst q in let q = Sh.rename inv_subst q in
(* reconjoin frame *) (* reconjoin frame *)
@ -249,9 +256,9 @@ let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
let locals = Reg.Set.vars locals in let locals = Reg.Set.vars locals in
let formals = Reg.Set.vars formals in let formals = Reg.Set.vars formals in
let foot = Sh.exists locals entry in let foot = Sh.exists locals entry in
let foot, subst = Sh.freshen ~wrt:(Set.union foot.us post.us) foot in let foot, subst = Sh.freshen ~wrt:(Var.Set.union foot.us post.us) foot in
let restore_formals q = let restore_formals q =
Set.fold formals ~init:q ~f:(fun q var -> Var.Set.fold formals ~init:q ~f:(fun q var ->
let var = Term.var var in let var = Term.var var in
let renamed_var = Term.rename subst var in let renamed_var = Term.rename subst var in
Sh.and_ (Term.eq renamed_var var) q ) Sh.and_ (Term.eq renamed_var var) q )
@ -261,11 +268,11 @@ let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
let foot = restore_formals foot in let foot = restore_formals foot in
let post = restore_formals post in let post = restore_formals post in
[%Trace.info "subst: %a" Var.Subst.pp subst] ; [%Trace.info "subst: %a" Var.Subst.pp subst] ;
let xs = Set.inter (Sh.fv foot) (Sh.fv post) in let xs = Var.Set.inter (Sh.fv foot) (Sh.fv post) in
let xs = Set.diff xs formals in let xs = Var.Set.diff xs formals in
let xs_and_formals = Set.union xs formals in let xs_and_formals = Var.Set.union xs formals in
let foot = Sh.exists (Set.diff foot.us xs_and_formals) foot in let foot = Sh.exists (Var.Set.diff foot.us xs_and_formals) foot in
let post = Sh.exists (Set.diff post.us xs_and_formals) post in let post = Sh.exists (Var.Set.diff post.us xs_and_formals) post in
let current = Sh.extend_us xs post in let current = Sh.extend_us xs post in
({xs; foot; post}, current) ({xs; foot; post}, current)
|> |>
@ -274,8 +281,8 @@ let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
let apply_summary q ({xs; foot; post} as fs) = let apply_summary q ({xs; foot; post} as fs) =
[%Trace.call fun {pf} -> pf "fs: %a@ q: %a" pp_summary fs pp q] [%Trace.call fun {pf} -> pf "fs: %a@ q: %a" pp_summary fs pp q]
; ;
let xs_in_q = Set.inter xs q.Sh.us in let xs_in_q = Var.Set.inter xs q.Sh.us in
let xs_in_fv_q = Set.inter xs (Sh.fv q) in let xs_in_fv_q = Var.Set.inter xs (Sh.fv q) in
(* Between creation of a summary and its use, the vocabulary of q (q.us) (* Between creation of a summary and its use, the vocabulary of q (q.us)
might have been extended. That means infer_frame would fail, because q might have been extended. That means infer_frame would fail, because q
and foot have different vocabulary. This might indicate that the and foot have different vocabulary. This might indicate that the
@ -286,11 +293,12 @@ let apply_summary q ({xs; foot; post} as fs) =
[%Trace.info "xs inter q.us: %a" Var.Set.pp xs_in_q] ; [%Trace.info "xs inter q.us: %a" Var.Set.pp xs_in_q] ;
[%Trace.info "xs inter fv.q %a" Var.Set.pp xs_in_fv_q] ; [%Trace.info "xs inter fv.q %a" Var.Set.pp xs_in_fv_q] ;
let q, add_back = let q, add_back =
if Set.is_empty xs_in_fv_q then (Sh.exists xs_in_q q, xs_in_q) if Var.Set.is_empty xs_in_fv_q then (Sh.exists xs_in_q q, xs_in_q)
else (q, Var.Set.empty) else (q, Var.Set.empty)
in in
let frame = let frame =
if Set.is_empty xs_in_fv_q then Solver.infer_frame q xs foot else None if Var.Set.is_empty xs_in_fv_q then Solver.infer_frame q xs foot
else None
in in
[%Trace.info "frame %a" (Option.pp "%a" pp) frame] ; [%Trace.info "frame %a" (Option.pp "%a" pp) frame] ;
Option.map ~f:(Sh.extend_us add_back) (Option.map ~f:(Sh.star post) frame) Option.map ~f:(Sh.extend_us add_back) (Option.map ~f:(Sh.star post) frame)

12
sledge/lib/domain_used_globals.ml
Unescape View File

@ -9,7 +9,7 @@
type t = Reg.Set.t [@@deriving equal, sexp] type t = Reg.Set.t [@@deriving equal, sexp]
let pp = Set.pp Reg.pp let pp = Reg.Set.pp
let report_fmt_thunk = Fn.flip pp let report_fmt_thunk = Fn.flip pp
let empty = Reg.Set.empty let empty = Reg.Set.empty
@ -17,13 +17,15 @@ let init globals =
[%Trace.info "pgm globals: {%a}" (Vector.pp ", " Global.pp) globals] ; [%Trace.info "pgm globals: {%a}" (Vector.pp ", " Global.pp) globals] ;
empty empty
let join l r = Some (Set.union l r) let join l r = Some (Reg.Set.union l r)
let recursion_beyond_bound = `skip let recursion_beyond_bound = `skip
let is_false _ = false let is_false _ = false
let post _ _ state = state let post _ _ state = state
let retn _ _ from_call post = Set.union from_call post let retn _ _ from_call post = Reg.Set.union from_call post
let dnf t = [t] let dnf t = [t]
let add_if_global gs v = if Var.global (Reg.var v) then Set.add gs v else gs
let add_if_global gs v =
if Var.global (Reg.var v) then Reg.Set.add gs v else gs
let used_globals ?(init = empty) exp = let used_globals ?(init = empty) exp =
Exp.fold_regs exp ~init ~f:add_if_global Exp.fold_regs exp ~init ~f:add_if_global
@ -79,7 +81,7 @@ type summary = t
let pp_summary = pp let pp_summary = pp
let create_summary ~locals:_ ~formals:_ state = (state, state) let create_summary ~locals:_ ~formals:_ state = (state, state)
let apply_summary st summ = Some (Set.union st summ) let apply_summary st summ = Some (Reg.Set.union st summ)
(** Query *) (** Query *)

52
sledge/lib/equality.ml
Unescape View File

@ -126,7 +126,9 @@ end = struct
[not (is_valid_eq xs e f)] implies [not (is_valid_eq ys e f)] for [not (is_valid_eq xs e f)] implies [not (is_valid_eq ys e f)] for
[ys ⊆ xs]. *) [ys ⊆ xs]. *)
let is_valid_eq xs e f = let is_valid_eq xs e f =
let is_var_in xs e = Option.exists ~f:(Set.mem xs) (Var.of_term e) in let is_var_in xs e =
Option.exists ~f:(Var.Set.mem xs) (Var.of_term e)
in
( is_var_in xs e || is_var_in xs f ( is_var_in xs e || is_var_in xs f
|| (uninterpreted e && Term.exists ~f:(is_var_in xs) e) || (uninterpreted e && Term.exists ~f:(is_var_in xs) e)
|| (uninterpreted f && Term.exists ~f:(is_var_in xs) f) ) || (uninterpreted f && Term.exists ~f:(is_var_in xs) f) )
@ -148,7 +150,8 @@ end = struct
if is_valid_eq ks key data then (t, ks, s) if is_valid_eq ks key data then (t, ks, s)
else else
let t = Term.Map.set ~key ~data t let t = Term.Map.set ~key ~data t
and ks = Set.diff ks (Set.union (Term.fv key) (Term.fv data)) and ks =
Var.Set.diff ks (Var.Set.union (Term.fv key) (Term.fv data))
and s = Term.Map.remove s key in and s = Term.Map.remove s key in
(t, ks, s) ) (t, ks, s) )
in in
@ -202,7 +205,7 @@ let extend ?f ~var ~rep (us, xs, s) =
let fresh name (us, xs, s) = let fresh name (us, xs, s) =
let x, us = Var.fresh name ~wrt:us in let x, us = Var.fresh name ~wrt:us in
let xs = Set.add xs x in let xs = Var.Set.add xs x in
(Term.var x, (us, xs, s)) (Term.var x, (us, xs, s))
let solve_poly ?f p q s = let solve_poly ?f p q s =
@ -270,14 +273,14 @@ and solve_ ?f d e s =
| Some m -> solve_ ?f n m s ) | Some m -> solve_ ?f n m s )
>>= solve_ ?f a b >>= solve_ ?f a b
| Some ((Var _ as v), (Ap3 (Extract, _, _, l) as e)) -> | Some ((Var _ as v), (Ap3 (Extract, _, _, l) as e)) ->
if not (Set.mem (Term.fv e) (Var.of_ v)) then if not (Var.Set.mem (Term.fv e) (Var.of_ v)) then
(* v = α[o,l) ==> v ↦ α[o,l) when v ∉ fv(α[o,l)) *) (* v = α[o,l) ==> v ↦ α[o,l) when v ∉ fv(α[o,l)) *)
extend ?f ~var:v ~rep:e s extend ?f ~var:v ~rep:e s
else else
(* v = α[o,l) ==> α[o,l) ↦ ⟨l,v⟩ when v ∈ fv(α[o,l)) *) (* v = α[o,l) ==> α[o,l) ↦ ⟨l,v⟩ when v ∈ fv(α[o,l)) *)
extend ?f ~var:e ~rep:(Term.memory ~siz:l ~arr:v) s extend ?f ~var:e ~rep:(Term.memory ~siz:l ~arr:v) s
| Some ((Var _ as v), (ApN (Concat, a0V) as c)) -> | Some ((Var _ as v), (ApN (Concat, a0V) as c)) ->
if not (Set.mem (Term.fv c) (Var.of_ v)) then if not (Var.Set.mem (Term.fv c) (Var.of_ v)) then
(* v = α₀^…^αᵥ ==> v ↦ α₀^…^αᵥ when v ∉ fv(α₀^…^αᵥ) *) (* v = α₀^…^αᵥ ==> v ↦ α₀^…^αᵥ when v ∉ fv(α₀^…^αᵥ) *)
extend ?f ~var:v ~rep:c s extend ?f ~var:v ~rep:c s
else else
@ -467,7 +470,7 @@ let merge us a b r =
; ;
( match solve ~us ~xs:r.xs a b with ( match solve ~us ~xs:r.xs a b with
| Some (xs, s) -> | Some (xs, s) ->
{r with xs= Set.union r.xs xs; rep= Subst.compose r.rep s} {r with xs= Var.Set.union r.xs xs; rep= Subst.compose r.rep s}
| None -> {r with sat= false} ) | None -> {r with sat= false} )
|> |>
[%Trace.retn fun {pf} r' -> [%Trace.retn fun {pf} r' ->
@ -648,7 +651,7 @@ let fold_terms r ~init ~f =
let fold_vars r ~init ~f = let fold_vars r ~init ~f =
fold_terms r ~init ~f:(fun init -> Term.fold_vars ~f ~init) fold_terms r ~init ~f:(fun init -> Term.fold_vars ~f ~init)
let fv e = fold_vars e ~f:Set.add ~init:Var.Set.empty let fv e = fold_vars e ~f:Var.Set.add ~init:Var.Set.empty
let pp_classes fs r = pp_clss fs (classes r) let pp_classes fs r = pp_clss fs (classes r)
let ppx_classes x fs r = ppx_clss x fs (classes r) let ppx_classes x fs r = ppx_clss x fs (classes r)
@ -678,11 +681,11 @@ let subst_invariant us s0 s =
(* dom of new entries not ito us *) (* dom of new entries not ito us *)
assert ( assert (
Option.for_all ~f:(Term.equal data) (Subst.find s0 key) Option.for_all ~f:(Term.equal data) (Subst.find s0 key)
|| not (Set.is_subset (Term.fv key) ~of_:us) ) ; || not (Var.Set.is_subset (Term.fv key) ~of_:us) ) ;
(* rep not ito us implies trm not ito us *) (* rep not ito us implies trm not ito us *)
assert ( assert (
Set.is_subset (Term.fv data) ~of_:us Var.Set.is_subset (Term.fv data) ~of_:us
|| not (Set.is_subset (Term.fv key) ~of_:us) ) ) ; || not (Var.Set.is_subset (Term.fv key) ~of_:us) ) ) ;
true ) true )
type 'a zom = Zero | One of 'a | Many type 'a zom = Zero | One of 'a | Many
@ -696,7 +699,7 @@ let solve_poly_eq us p' q' subst =
let max_solvables_not_ito_us = let max_solvables_not_ito_us =
fold_max_solvables diff ~init:Zero ~f:(fun solvable_subterm -> function fold_max_solvables diff ~init:Zero ~f:(fun solvable_subterm -> function
| Many -> Many | Many -> Many
| zom when Set.is_subset (Term.fv solvable_subterm) ~of_:us -> zom | zom when Var.Set.is_subset (Term.fv solvable_subterm) ~of_:us -> zom
| One _ -> Many | One _ -> Many
| Zero -> One solvable_subterm ) | Zero -> One solvable_subterm )
in in
@ -710,8 +713,8 @@ let solve_memory_eq us e' f' subst =
[%Trace.call fun {pf} -> pf "%a = %a" Term.pp e' Term.pp f'] [%Trace.call fun {pf} -> pf "%a = %a" Term.pp e' Term.pp f']
; ;
let f x u = let f x u =
(not (Set.is_subset (Term.fv x) ~of_:us)) (not (Var.Set.is_subset (Term.fv x) ~of_:us))
&& Set.is_subset (Term.fv u) ~of_:us && Var.Set.is_subset (Term.fv u) ~of_:us
in in
let solve_concat ms n a = let solve_concat ms n a =
let a, n = let a, n =
@ -720,7 +723,7 @@ let solve_memory_eq us e' f' subst =
| None -> (Term.memory ~siz:n ~arr:a, n) | None -> (Term.memory ~siz:n ~arr:a, n)
in in
let+ _, xs, s = solve_concat ~f ms a n (us, Var.Set.empty, subst) in let+ _, xs, s = solve_concat ~f ms a n (us, Var.Set.empty, subst) in
assert (Set.is_empty xs) ; assert (Var.Set.is_empty xs) ;
s s
in in
( match ((e' : Term.t), (f' : Term.t)) with ( match ((e' : Term.t), (f' : Term.t)) with
@ -805,7 +808,7 @@ let solve_uninterp_eqs us (cls, subst) =
let {rep_us; cls_us; rep_xs; cls_xs} = let {rep_us; cls_us; rep_xs; cls_xs} =
List.fold cls ~init:{rep_us= None; cls_us= []; rep_xs= None; cls_xs= []} List.fold cls ~init:{rep_us= None; cls_us= []; rep_xs= None; cls_xs= []}
~f:(fun ({rep_us; cls_us; rep_xs; cls_xs} as s) trm -> ~f:(fun ({rep_us; cls_us; rep_xs; cls_xs} as s) trm ->
if Set.is_subset (Term.fv trm) ~of_:us then if Var.Set.is_subset (Term.fv trm) ~of_:us then
match rep_us with match rep_us with
| Some rep when compare rep trm <= 0 -> | Some rep when compare rep trm <= 0 ->
{s with cls_us= trm :: cls_us} {s with cls_us= trm :: cls_us}
@ -869,7 +872,7 @@ let solve_class us us_xs ~key:rep ~data:cls (classes, subst) =
; ;
let cls, cls_not_ito_us_xs = let cls, cls_not_ito_us_xs =
List.partition_tf List.partition_tf
~f:(fun e -> Set.is_subset (Term.fv e) ~of_:us_xs) ~f:(fun e -> Var.Set.is_subset (Term.fv e) ~of_:us_xs)
(rep :: cls) (rep :: cls)
in in
let cls, subst = solve_interp_eqs us (cls, subst) in let cls, subst = solve_interp_eqs us (cls, subst) in
@ -929,7 +932,8 @@ let solve_concat_extracts r us x (classes, subst, us_xs) =
List.fold (cls_of r e) ~init:None ~f:(fun rep_ito_us trm -> List.fold (cls_of r e) ~init:None ~f:(fun rep_ito_us trm ->
match rep_ito_us with match rep_ito_us with
| Some rep when Term.compare rep trm <= 0 -> rep_ito_us | Some rep when Term.compare rep trm <= 0 -> rep_ito_us
| _ when Set.is_subset (Term.fv trm) ~of_:us -> Some trm | _ when Var.Set.is_subset (Term.fv trm) ~of_:us ->
Some trm
| _ -> rep_ito_us ) | _ -> rep_ito_us )
in in
Term.memory ~siz:(Term.agg_size_exn e) ~arr:rep_ito_us :: suffix Term.memory ~siz:(Term.agg_size_exn e) ~arr:rep_ito_us :: suffix
@ -943,7 +947,7 @@ let solve_concat_extracts r us x (classes, subst, us_xs) =
| None -> (classes, subst, us_xs) | None -> (classes, subst, us_xs)
let solve_for_xs r us xs (classes, subst, us_xs) = let solve_for_xs r us xs (classes, subst, us_xs) =
Set.fold xs ~init:(classes, subst, us_xs) Var.Set.fold xs ~init:(classes, subst, us_xs)
~f:(fun (classes, subst, us_xs) x -> ~f:(fun (classes, subst, us_xs) x ->
let x = Term.var x in let x = Term.var x in
if Subst.mem subst x then (classes, subst, us_xs) if Subst.mem subst x then (classes, subst, us_xs)
@ -964,7 +968,7 @@ let solve_classes r (classes, subst, us) xs =
if subst != subst0 then solve_classes_ (classes, subst, us_xs) if subst != subst0 then solve_classes_ (classes, subst, us_xs)
else (classes, subst, us_xs) else (classes, subst, us_xs)
in in
(classes, subst, Set.union us xs) (classes, subst, Var.Set.union us xs)
|> solve_classes_ |> solve_for_xs r us xs |> solve_classes_ |> solve_for_xs r us xs
|> |>
[%Trace.retn fun {pf} (classes', subst', _) -> [%Trace.retn fun {pf} (classes', subst', _) ->
@ -1000,14 +1004,14 @@ let solve_for_vars vss r =
assert ( assert (
List.fold_until vss ~init:us List.fold_until vss ~init:us
~f:(fun us xs -> ~f:(fun us xs ->
let us_xs = Set.union us xs in let us_xs = Var.Set.union us xs in
let ks = Term.fv key in let ks = Term.fv key in
let ds = Term.fv data in let ds = Term.fv data in
if if
Set.is_subset ks ~of_:us_xs Var.Set.is_subset ks ~of_:us_xs
&& Set.is_subset ds ~of_:us_xs && Var.Set.is_subset ds ~of_:us_xs
&& ( Set.is_subset ds ~of_:us && ( Var.Set.is_subset ds ~of_:us
|| not (Set.is_subset ks ~of_:us) ) || not (Var.Set.is_subset ks ~of_:us) )
then Stop true then Stop true
else Continue us_xs ) else Continue us_xs )
~finish:(fun _ -> false) ) )] ~finish:(fun _ -> false) ) )]

3
sledge/lib/equality_test.ml
Unescape View File

@ -188,8 +188,7 @@ let%test_module _ =
let r5 = of_eqs [(x, y); (g w x, y); (g w y, f z)] let r5 = of_eqs [(x, y); (g w x, y); (g w y, f z)]
let%test _ = let%test _ = Var.Set.equal (fv r5) (Var.Set.of_list [w_; x_; y_; z_])
Set.equal (fv r5) (Set.of_list (module Var) [w_; x_; y_; z_])
let r6 = of_eqs [(x, !1); (!1, y)] let r6 = of_eqs [(x, !1); (!1, y)]

40
sledge/lib/exec.ml
Unescape View File

@ -17,7 +17,7 @@ type xseg = {us: Var.Set.t; xs: Var.Set.t; seg: Sh.seg}
let fresh_var nam us xs = let fresh_var nam us xs =
let var, us = Var.fresh nam ~wrt:us in let var, us = Var.fresh nam ~wrt:us in
(Term.var var, us, Set.add xs var) (Term.var var, us, Var.Set.add xs var)
let fresh_seg ~loc ?bas ?len ?siz ?arr ?(xs = Var.Set.empty) us = let fresh_seg ~loc ?bas ?len ?siz ?arr ?(xs = Var.Set.empty) us =
let freshen term nam us xs = let freshen term nam us xs =
@ -38,10 +38,10 @@ let null_eq ptr = Sh.pure (Term.eq Term.null ptr)
precondition; [us] are the variables to which ghosts must be chosen precondition; [us] are the variables to which ghosts must be chosen
fresh. *) fresh. *)
let assign ~ws ~rs ~us = let assign ~ws ~rs ~us =
let ovs = Set.inter ws rs in let ovs = Var.Set.inter ws rs in
let sub = Var.Subst.freshen ovs ~wrt:us in let sub = Var.Subst.freshen ovs ~wrt:us in
let us = Set.union us (Var.Subst.range sub) in let us = Var.Set.union us (Var.Subst.range sub) in
let ms = Set.diff ws (Var.Subst.domain sub) in let ms = Var.Set.diff ws (Var.Subst.domain sub) in
(sub, ms, us) (sub, ms, us)
(* (*
@ -58,7 +58,7 @@ let move_spec us reg_exps =
let ws, rs = let ws, rs =
Vector.fold reg_exps ~init:(Var.Set.empty, Var.Set.empty) Vector.fold reg_exps ~init:(Var.Set.empty, Var.Set.empty)
~f:(fun (ws, rs) (reg, exp) -> ~f:(fun (ws, rs) (reg, exp) ->
(Set.add ws reg, Set.union rs (Term.fv exp)) ) (Var.Set.add ws reg, Var.Set.union rs (Term.fv exp)) )
in in
let sub, ms, _ = assign ~ws ~rs ~us in let sub, ms, _ = assign ~ws ~rs ~us in
let post = let post =
@ -327,7 +327,9 @@ let posix_memalign_spec us reg ptr siz =
let {us; xs; seg= pseg} = fresh_seg ~loc:ptr ~siz:size_of_ptr us in let {us; xs; seg= pseg} = fresh_seg ~loc:ptr ~siz:size_of_ptr us in
let foot = Sh.seg pseg in let foot = Sh.seg pseg in
let sub, ms, us = let sub, ms, us =
assign ~ws:(Var.Set.of_ reg) ~rs:(Set.union foot.us (Term.fv siz)) ~us assign ~ws:(Var.Set.of_ reg)
~rs:(Var.Set.union foot.us (Term.fv siz))
~us
in in
let q, us, xs = fresh_var "q" us xs in let q, us, xs = fresh_var "q" us xs in
let pseg' = {pseg with arr= q} in let pseg' = {pseg with arr= q} in
@ -358,7 +360,9 @@ let realloc_spec us reg ptr siz =
in in
let foot = Sh.or_ (null_eq ptr) (Sh.seg pseg) in let foot = Sh.or_ (null_eq ptr) (Sh.seg pseg) in
let sub, ms, us = let sub, ms, us =
assign ~ws:(Var.Set.of_ reg) ~rs:(Set.union foot.us (Term.fv siz)) ~us assign ~ws:(Var.Set.of_ reg)
~rs:(Var.Set.union foot.us (Term.fv siz))
~us
in in
let loc = Term.var reg in let loc = Term.var reg in
let siz = Term.rename sub siz in let siz = Term.rename sub siz in
@ -421,7 +425,7 @@ let xallocx_spec us reg ptr siz ext =
let foot = Sh.and_ Term.(dq siz zero) (Sh.seg seg) in let foot = Sh.and_ Term.(dq siz zero) (Sh.seg seg) in
let sub, ms, us = let sub, ms, us =
assign ~ws:(Var.Set.of_ reg) assign ~ws:(Var.Set.of_ reg)
~rs:Set.(union foot.us (union (Term.fv siz) (Term.fv ext))) ~rs:Var.Set.(union foot.us (union (Term.fv siz) (Term.fv ext)))
~us ~us
in in
let reg = Term.var reg in let reg = Term.var reg in
@ -601,10 +605,10 @@ let strlen_spec us reg ptr =
*) *)
let check_preserve_us (q0 : Sh.t) (q1 : Sh.t) = let check_preserve_us (q0 : Sh.t) (q1 : Sh.t) =
let gain_us = Set.diff q1.us q0.us in let gain_us = Var.Set.diff q1.us q0.us in
let lose_us = Set.diff q0.us q1.us in let lose_us = Var.Set.diff q0.us q1.us in
(Set.is_empty gain_us || fail "gain us: %a" Var.Set.pp gain_us ()) (Var.Set.is_empty gain_us || fail "gain us: %a" Var.Set.pp gain_us ())
&& (Set.is_empty lose_us || fail "lose us: %a" Var.Set.pp lose_us ()) && (Var.Set.is_empty lose_us || fail "lose us: %a" Var.Set.pp lose_us ())
(* execute a command with given spec from pre *) (* execute a command with given spec from pre *)
let exec_spec pre0 {xs; foot; sub; ms; post} = let exec_spec pre0 {xs; foot; sub; ms; post} =
@ -617,20 +621,20 @@ let exec_spec pre0 {xs; foot; sub; ms; post} =
Format.fprintf fs "∧ %a" Var.Subst.pp sub ) Format.fprintf fs "∧ %a" Var.Subst.pp sub )
sub sub
(fun fs ms -> (fun fs ms ->
if not (Set.is_empty ms) then if not (Var.Set.is_empty ms) then
Format.fprintf fs "%a := " Var.Set.pp ms ) Format.fprintf fs "%a := " Var.Set.pp ms )
ms Sh.pp post ; ms Sh.pp post ;
assert ( assert (
let vs = Set.diff (Set.diff foot.us xs) pre0.us in let vs = Var.Set.diff (Var.Set.diff foot.us xs) pre0.us in
Set.is_empty vs || fail "unbound foot: {%a}" Var.Set.pp vs () ) ; Var.Set.is_empty vs || fail "unbound foot: {%a}" Var.Set.pp vs () ) ;
assert ( assert (
let vs = Set.diff (Set.diff post.us xs) pre0.us in let vs = Var.Set.diff (Var.Set.diff post.us xs) pre0.us in
Set.is_empty vs || fail "unbound post: {%a}" Var.Set.pp vs () )] Var.Set.is_empty vs || fail "unbound post: {%a}" Var.Set.pp vs () )]
; ;
let foot = Sh.extend_us xs foot in let foot = Sh.extend_us xs foot in
let zs, pre = Sh.bind_exists pre0 ~wrt:xs in let zs, pre = Sh.bind_exists pre0 ~wrt:xs in
let+ frame = Solver.infer_frame pre xs foot in let+ frame = Solver.infer_frame pre xs foot in
Sh.exists (Set.union zs xs) Sh.exists (Var.Set.union zs xs)
(Sh.star post (Sh.exists ms (Sh.rename sub frame)))) (Sh.star post (Sh.exists ms (Sh.rename sub frame))))
|> |>
[%Trace.retn fun {pf} r -> [%Trace.retn fun {pf} r ->

157
sledge/lib/exp.ml
Unescape View File

@ -10,80 +10,82 @@
[@@@warning "+9"] [@@@warning "+9"]
module T = struct module T = struct
module T0 = struct type op1 =
type op1 = (* conversion *)
(* conversion *) | Signed of {bits: int}
| Signed of {bits: int} | Unsigned of {bits: int}
| Unsigned of {bits: int} | Convert of {src: Typ.t}
| Convert of {src: Typ.t} (* array/struct operations *)
(* array/struct operations *) | Splat
| Splat | Select of int
| Select of int [@@deriving compare, equal, hash, sexp]
[@@deriving compare, equal, hash, sexp]
type op2 =
type op2 = (* comparison *)
(* comparison *) | Eq
| Eq | Dq
| Dq | Gt
| Gt | Ge
| Ge | Lt
| Lt | Le
| Le | Ugt
| Ugt | Uge
| Uge | Ult
| Ult | Ule
| Ule | Ord
| Ord | Uno
| Uno (* arithmetic, numeric and pointer *)
(* arithmetic, numeric and pointer *) | Add
| Add | Sub
| Sub | Mul
| Mul | Div
| Div | Rem
| Rem | Udiv
| Udiv | Urem
| Urem (* boolean / bitwise *)
(* boolean / bitwise *) | And
| And | Or
| Or | Xor
| Xor | Shl
| Shl | Lshr
| Lshr | Ashr
| Ashr (* array/struct operations *)
(* array/struct operations *) | Update of int
| Update of int [@@deriving compare, equal, hash, sexp]
[@@deriving compare, equal, hash, sexp]
type op3 = (* if-then-else *)
type op3 = (* if-then-else *) | Conditional
| Conditional [@@deriving compare, equal, hash, sexp]
[@@deriving compare, equal, hash, sexp]
type opN =
type opN = (* array/struct constants *)
(* array/struct constants *) | Record
| Record | Struct_rec (** NOTE: may be cyclic *)
| Struct_rec (** NOTE: may be cyclic *) [@@deriving compare, equal, hash, sexp]
[@@deriving compare, equal, hash, sexp]
type t = {desc: desc; term: Term.t}
type t = {desc: desc; term: Term.t}
and desc =
and desc = | Reg of {name: string; typ: Typ.t}
| Reg of {name: string; typ: Typ.t} | Nondet of {msg: string; typ: Typ.t}
| Nondet of {msg: string; typ: Typ.t} | Label of {parent: string; name: string}
| Label of {parent: string; name: string} | Integer of {data: Z.t; typ: Typ.t}
| Integer of {data: Z.t; typ: Typ.t} | Float of {data: string; typ: Typ.t}
| Float of {data: string; typ: Typ.t} | Ap1 of op1 * Typ.t * t
| Ap1 of op1 * Typ.t * t | Ap2 of op2 * Typ.t * t * t
| Ap2 of op2 * Typ.t * t * t | Ap3 of op3 * Typ.t * t * t * t
| Ap3 of op3 * Typ.t * t * t * t | ApN of opN * Typ.t * t vector
| ApN of opN * Typ.t * t vector [@@deriving compare, equal, hash, sexp]
[@@deriving compare, equal, hash, sexp]
end
include T0
include Comparator.Make (T0)
end end
include T include T
module Set = struct
include Set.Make (T)
let t_of_sexp = t_of_sexp T.t_of_sexp
end
module Map = Map.Make (T) module Map = Map.Make (T)
let term e = e.term let term e = e.term
@ -316,17 +318,12 @@ module Reg = struct
match Var.of_term r.term with Some v -> v | _ -> violates invariant r match Var.of_term r.term with Some v -> v | _ -> violates invariant r
module Set = struct module Set = struct
include ( include Set
Set :
module type of Set with type ('elt, 'cmp) t := ('elt, 'cmp) Set.t )
type t = Set.M(T).t [@@deriving compare, equal, sexp]
let pp = Set.pp pp_exp let pp = Set.pp pp_exp
let empty = Set.empty (module T)
let of_list = Set.of_list (module T) let vars =
let union_list = Set.union_list (module T) Set.fold ~init:Var.Set.empty ~f:(fun s r -> Var.Set.add s (var r))
let vars = Set.fold ~init:Var.Set.empty ~f:(fun s r -> add s (var r))
end end
module Map = Map module Map = Map

14
sledge/lib/exp.mli
Unescape View File

@ -90,8 +90,6 @@ and desc = private
| ApN of opN * Typ.t * t vector | ApN of opN * Typ.t * t vector
[@@deriving compare, equal, hash, sexp] [@@deriving compare, equal, hash, sexp]
include Comparator.S with type t := t
val pp : t pp val pp : t pp
include Invariant.S with type t := t include Invariant.S with type t := t
@ -101,18 +99,12 @@ module Reg : sig
type exp := t type exp := t
type t = private exp [@@deriving compare, equal, hash, sexp] type t = private exp [@@deriving compare, equal, hash, sexp]
include Comparator.S with type t := t
module Set : sig module Set : sig
type reg := t include Set.S with type elt := t
type t = (reg, comparator_witness) Set.t
[@@deriving compare, equal, sexp]
val sexp_of_t : t -> Sexp.t
val t_of_sexp : Sexp.t -> t
val pp : t pp val pp : t pp
val empty : t
val of_list : reg list -> t
val union_list : t list -> t
val vars : t -> Var.Set.t val vars : t -> Var.Set.t
end end

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

@ -171,6 +171,14 @@ end
include Option.Monad_infix include Option.Monad_infix
include Option.Monad_syntax include Option.Monad_syntax
module Result = struct
include Base.Result
let pp fmt pp_elt fs = function
| Ok x -> Format.fprintf fs fmt pp_elt x
| Error _ -> ()
end
module List = struct module List = struct
include Base.List include Base.List
@ -253,6 +261,14 @@ module List = struct
pp sep pp_diff_elt fs (symmetric_diff ~compare xs ys) pp sep pp_diff_elt fs (symmetric_diff ~compare xs ys)
end end
module Vector = struct
include Vector
let pp sep pp_elt fs v = List.pp sep pp_elt fs (to_list v)
end
include Vector.Infix
module type OrderedType = sig module type OrderedType = sig
type t type t
@ -262,6 +278,94 @@ end
exception Duplicate exception Duplicate
module Set = struct
module type S = sig
type elt
type t
val compare : t -> t -> int
val equal : t -> t -> bool
val sexp_of_t : t -> Sexp.t
val t_of_sexp : (Sexp.t -> elt) -> Sexp.t -> t
val pp : elt pp -> t pp
val pp_diff : elt pp -> (t * t) pp
(* initial constructors *)
val empty : t
val of_ : elt -> t
val of_option : elt option -> t
val of_list : elt list -> t
val of_vector : elt vector -> t
(* constructors *)
val add : t -> elt -> t
val add_option : elt option -> t -> t
val add_list : elt list -> t -> t
val remove : t -> elt -> t
val filter : t -> f:(elt -> bool) -> t
val union : t -> t -> t
val union_list : t list -> t
val diff : t -> t -> t
val inter : t -> t -> t
val diff_inter : t -> t -> t * t
(* queries *)
val is_empty : t -> bool
val mem : t -> elt -> bool
val is_subset : t -> of_:t -> bool
val disjoint : t -> t -> bool
val max_elt : t -> elt option
(* traversals *)
val fold : t -> init:'s -> f:('s -> elt -> 's) -> 's
end
module Make (Elt : OrderedType) : S with type elt = Elt.t = struct
module S = Caml.Set.Make (Elt)
type elt = Elt.t
type t = S.t
let compare = S.compare
let equal = S.equal
let sexp_of_t s = List.sexp_of_t Elt.sexp_of_t (S.elements s)
let t_of_sexp elt_of_sexp sexp =
S.of_list (List.t_of_sexp elt_of_sexp sexp)
let pp pp_elt fs x = List.pp ",@ " pp_elt fs (S.elements x)
let pp_diff pp_elt fs (xs, ys) =
let lose = S.diff xs ys and gain = S.diff ys xs in
if not (S.is_empty lose) then
Format.fprintf fs "-- %a" (pp pp_elt) lose ;
if not (S.is_empty gain) then
Format.fprintf fs "++ %a" (pp pp_elt) gain
let empty = S.empty
let of_ x = S.add x empty
let of_option = Option.fold ~f:(fun x y -> S.add y x) ~init:empty
let of_list = S.of_list
let of_vector x = S.of_list (Vector.to_list x)
let add s e = S.add e s
let add_option yo x = Option.fold ~f:(fun x y -> S.add y x) ~init:x yo
let add_list ys x = List.fold ~f:(fun x y -> S.add y x) ~init:x ys
let remove s e = S.remove e s
let filter s ~f = S.filter f s
let union = S.union
let union_list ss = List.fold ss ~init:empty ~f:union
let diff = S.diff
let inter = S.inter
let diff_inter x y = (S.diff x y, S.inter x y)
let is_empty = S.is_empty
let mem s e = S.mem e s
let is_subset x ~of_ = S.subset x of_
let disjoint = S.disjoint
let max_elt = S.max_elt_opt
let fold s ~init:z ~f = S.fold (fun z x -> f x z) s z
end
end
module Map = struct module Map = struct
module type S = sig module type S = sig
type key type key
@ -450,51 +554,6 @@ module Map = struct
end end
end end
module Result = struct
include Base.Result
let pp fmt pp_elt fs = function
| Ok x -> Format.fprintf fs fmt pp_elt x
| Error _ -> ()
end
module Vector = struct
include Vector
let pp sep pp_elt fs v = List.pp sep pp_elt fs (to_list v)
end
include Vector.Infix
module Set = struct
include Base.Set
type ('elt, 'cmp) tree = ('elt, 'cmp) Using_comparator.Tree.t
let equal_m__t (module Elt : Compare_m) = equal
let pp pp_elt fs x = List.pp ",@ " pp_elt fs (to_list x)
let pp_diff pp_elt fs (xs, ys) =
let lose = diff xs ys and gain = diff ys xs in
if not (is_empty lose) then Format.fprintf fs "-- %a" (pp pp_elt) lose ;
if not (is_empty gain) then Format.fprintf fs "++ %a" (pp pp_elt) gain
let disjoint x y = is_empty (inter x y)
let add_option yo x = Option.fold ~f:add ~init:x yo
let add_list ys x = List.fold ~f:add ~init:x ys
let diff_inter x y = (diff x y, inter x y)
let diff_inter_diff x y = (diff x y, inter x y, diff y x)
let of_vector cmp x = of_array cmp (Vector.to_array x)
let to_tree = Using_comparator.to_tree
let union x y =
let xy = union x y in
let xy_tree = to_tree xy in
if xy_tree == to_tree x then x
else if xy_tree == to_tree y then y
else xy
end
module Qset = struct module Qset = struct
include Qset include Qset

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

@ -138,6 +138,13 @@ end
include module type of Option.Monad_infix include module type of Option.Monad_infix
include module type of Option.Monad_syntax with type 'a t = 'a option include module type of Option.Monad_syntax with type 'a t = 'a option
module Result : sig
include module type of Base.Result
val pp : ('a_pp -> 'a -> unit, unit) fmt -> 'a_pp -> ('a, _) t pp
(** Pretty-print a result. *)
end
module List : sig module List : sig
include module type of Base.List include module type of Base.List
@ -192,6 +199,15 @@ module List : sig
compare:('a -> 'a -> int) -> 'a t -> 'a t -> ('a, 'a) Either.t t compare:('a -> 'a -> int) -> 'a t -> 'a t -> ('a, 'a) Either.t t
end end
module Vector : sig
include module type of Vector
val pp : (unit, unit) fmt -> 'a pp -> 'a t pp
(** Pretty-print a vector. *)
end
include module type of Vector.Infix
module type OrderedType = sig module type OrderedType = sig
type t type t
@ -201,6 +217,51 @@ end
exception Duplicate exception Duplicate
module Set : sig
module type S = sig
type elt
type t
val compare : t -> t -> int
val equal : t -> t -> bool
val sexp_of_t : t -> Sexp.t
val t_of_sexp : (Sexp.t -> elt) -> Sexp.t -> t
val pp : elt pp -> t pp
val pp_diff : elt pp -> (t * t) pp
(* initial constructors *)
val empty : t
val of_ : elt -> t
val of_option : elt option -> t
val of_list : elt list -> t
val of_vector : elt vector -> t
(* constructors *)
val add : t -> elt -> t
val add_option : elt option -> t -> t
val add_list : elt list -> t -> t
val remove : t -> elt -> t
val filter : t -> f:(elt -> bool) -> t
val union : t -> t -> t
val union_list : t list -> t
val diff : t -> t -> t
val inter : t -> t -> t
val diff_inter : t -> t -> t * t
(* queries *)
val is_empty : t -> bool
val mem : t -> elt -> bool
val is_subset : t -> of_:t -> bool
val disjoint : t -> t -> bool
val max_elt : t -> elt option
(* traversals *)
val fold : t -> init:'s -> f:('s -> elt -> 's) -> 's
end
module Make (Elt : OrderedType) : S with type elt = Elt.t
end
module Map : sig module Map : sig
module type S = sig module type S = sig
type key type key
@ -265,44 +326,6 @@ module Map : sig
module Make (Key : OrderedType) : S with type key = Key.t module Make (Key : OrderedType) : S with type key = Key.t
end end
module Result : sig
include module type of Base.Result
val pp : ('a_pp -> 'a -> unit, unit) fmt -> 'a_pp -> ('a, _) t pp
(** Pretty-print a result. *)
end
module Vector : sig
include module type of Vector
val pp : (unit, unit) fmt -> 'a pp -> 'a t pp
(** Pretty-print a vector. *)
end
include module type of Vector.Infix
module Set : sig
include module type of Base.Set
type ('e, 'c) tree
val equal_m__t :
(module Compare_m) -> ('elt, 'cmp) t -> ('elt, 'cmp) t -> bool
val pp : 'e pp -> ('e, 'c) t pp
val pp_diff : 'e pp -> (('e, 'c) t * ('e, 'c) t) pp
val disjoint : ('e, 'c) t -> ('e, 'c) t -> bool
val add_option : 'e option -> ('e, 'c) t -> ('e, 'c) t
val add_list : 'e list -> ('e, 'c) t -> ('e, 'c) t
val diff_inter : ('e, 'c) t -> ('e, 'c) t -> ('e, 'c) t * ('e, 'c) t
val diff_inter_diff :
('e, 'c) t -> ('e, 'c) t -> ('e, 'c) t * ('e, 'c) t * ('e, 'c) t
val of_vector : ('e, 'c) comparator -> 'e vector -> ('e, 'c) t
val to_tree : ('e, 'c) t -> ('e, 'c) tree
end
module Qset : sig module Qset : sig
include module type of Qset include module type of Qset

21
sledge/lib/llair.ml
Unescape View File

@ -254,9 +254,11 @@ module Inst = struct
let union_locals inst vs = let union_locals inst vs =
match inst with match inst with
| Move {reg_exps; _} -> | Move {reg_exps; _} ->
Vector.fold ~f:(fun vs (reg, _) -> Set.add vs reg) ~init:vs reg_exps Vector.fold
~f:(fun vs (reg, _) -> Reg.Set.add vs reg)
~init:vs reg_exps
| Load {reg; _} | Alloc {reg; _} | Nondet {reg= Some reg; _} -> | Load {reg; _} | Alloc {reg; _} | Nondet {reg= Some reg; _} ->
Set.add vs reg Reg.Set.add vs reg
| Store _ | Memcpy _ | Memmov _ | Memset _ | Free _ | Store _ | Memcpy _ | Memmov _ | Memset _ | Free _
|Nondet {reg= None; _} |Nondet {reg= None; _}
|Abort _ -> |Abort _ ->
@ -349,7 +351,7 @@ module Term = struct
let union_locals term vs = let union_locals term vs =
match term with match term with
| Call {areturn; _} -> Set.add_option areturn vs | Call {areturn; _} -> Reg.Set.add_option areturn vs
| _ -> vs | _ -> vs
end end
@ -389,8 +391,7 @@ module Block_label = struct
end end
include T include T
module Set = Set.Make (T)
let empty_set = Set.empty (module T)
end end
module BlockQ = Hash_queue.Make (Block_label) module BlockQ = Hash_queue.Make (Block_label)
@ -535,9 +536,10 @@ let set_derived_metadata functions =
let rec visit ancestors func src = let rec visit ancestors func src =
if BlockQ.mem tips_to_roots src then () if BlockQ.mem tips_to_roots src then ()
else else
let ancestors = Set.add ancestors src in let ancestors = Block_label.Set.add ancestors src in
let jump jmp = let jump jmp =
if Set.mem ancestors jmp.dst then jmp.retreating <- true if Block_label.Set.mem ancestors jmp.dst then
jmp.retreating <- true
else visit ancestors func jmp.dst else visit ancestors func jmp.dst
in in
( match src.term with ( match src.term with
@ -551,7 +553,8 @@ let set_derived_metadata functions =
(Option.map ~f:Reg.name (Reg.of_exp callee)) (Option.map ~f:Reg.name (Reg.of_exp callee))
with with
| Some func -> | Some func ->
if Set.mem ancestors func.entry then call.recursive <- true if Block_label.Set.mem ancestors func.entry then
call.recursive <- true
else visit ancestors func func.entry else visit ancestors func func.entry
| None -> | None ->
(* conservatively assume all virtual calls are recursive *) (* conservatively assume all virtual calls are recursive *)
@ -561,7 +564,7 @@ let set_derived_metadata functions =
BlockQ.enqueue_back_exn tips_to_roots src () BlockQ.enqueue_back_exn tips_to_roots src ()
in in
FuncQ.iter roots ~f:(fun root -> FuncQ.iter roots ~f:(fun root ->
visit Block_label.empty_set root root.entry ) ; visit Block_label.Set.empty root root.entry ) ;
tips_to_roots tips_to_roots
in in
let set_sort_indices tips_to_roots = let set_sort_indices tips_to_roots =

175
sledge/lib/sh.ml
Unescape View File

@ -103,10 +103,11 @@ let rec var_strength_ xs m q =
| Some `Anonymous -> Var.Map.set m ~key:v ~data:`Existential | Some `Anonymous -> Var.Map.set m ~key:v ~data:`Existential
| Some _ -> m | Some _ -> m
in in
let xs = Set.union xs q.xs in let xs = Var.Set.union xs q.xs in
let m_stem = let m_stem =
fold_vars_stem ~ignore_cong:() q ~init:m ~f:(fun m var -> fold_vars_stem ~ignore_cong:() q ~init:m ~f:(fun m var ->
if not (Set.mem xs var) then Var.Map.set m ~key:var ~data:`Universal if not (Var.Set.mem xs var) then
Var.Map.set m ~key:var ~data:`Universal
else add m var ) else add m var )
in in
let m = let m =
@ -124,7 +125,7 @@ let rec var_strength_ xs m q =
let var_strength_full ?(xs = Var.Set.empty) q = let var_strength_full ?(xs = Var.Set.empty) q =
let m = let m =
Set.fold xs ~init:Var.Map.empty ~f:(fun m x -> Var.Set.fold xs ~init:Var.Map.empty ~f:(fun m x ->
Var.Map.set m ~key:x ~data:`Existential ) Var.Map.set m ~key:x ~data:`Existential )
in in
var_strength_ xs m q var_strength_ xs m q
@ -202,12 +203,12 @@ let pp_heap x ?pre cong fs heap =
let pp_us ?(pre = ("" : _ fmt)) ?vs () fs us = let pp_us ?(pre = ("" : _ fmt)) ?vs () fs us =
match vs with match vs with
| None -> | None ->
if not (Set.is_empty us) then if not (Var.Set.is_empty us) then
[%Trace.fprintf fs "%( %)@[%a@] .@ " pre Var.Set.pp us] [%Trace.fprintf fs "%( %)@[%a@] .@ " pre Var.Set.pp us]
| Some vs -> | Some vs ->
if not (Set.equal vs us) then if not (Var.Set.equal vs us) then
[%Trace.fprintf [%Trace.fprintf
fs "%( %)@[%a@] .@ " pre (Set.pp_diff Var.pp) (vs, us)] fs "%( %)@[%a@] .@ " pre (Var.Set.pp_diff Var.pp) (vs, us)]
let rec pp_ ?var_strength vs parent_xs parent_cong fs let rec pp_ ?var_strength vs parent_xs parent_cong fs
{us; xs; cong; pure; heap; djns} = {us; xs; cong; pure; heap; djns} =
@ -215,14 +216,14 @@ let rec pp_ ?var_strength vs parent_xs parent_cong fs
let x v = Option.bind ~f:(fun (_, m) -> Var.Map.find m v) var_strength in let x v = Option.bind ~f:(fun (_, m) -> Var.Map.find m v) var_strength in
pp_us ~vs () fs us ; pp_us ~vs () fs us ;
let xs_d_vs, xs_i_vs = let xs_d_vs, xs_i_vs =
Set.diff_inter Var.Set.diff_inter
(Set.filter xs ~f:(fun v -> Poly.(x v <> Some `Anonymous))) (Var.Set.filter xs ~f:(fun v -> Poly.(x v <> Some `Anonymous)))
vs vs
in in
if not (Set.is_empty xs_i_vs) then ( if not (Var.Set.is_empty xs_i_vs) then (
Format.fprintf fs "@<2>∃ @[%a@] ." (Var.Set.ppx x) xs_i_vs ; Format.fprintf fs "@<2>∃ @[%a@] ." (Var.Set.ppx x) xs_i_vs ;
if not (Set.is_empty xs_d_vs) then Format.fprintf fs "@ " ) ; if not (Var.Set.is_empty xs_d_vs) then Format.fprintf fs "@ " ) ;
if not (Set.is_empty xs_d_vs) then if not (Var.Set.is_empty xs_d_vs) then
Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.ppx x) xs_d_vs ; Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.ppx x) xs_d_vs ;
let first = Equality.entails parent_cong cong in let first = Equality.entails parent_cong cong in
if not first then Format.fprintf fs " " ; if not first then Format.fprintf fs " " ;
@ -250,8 +251,9 @@ let rec pp_ ?var_strength vs parent_xs parent_cong fs
~pre:(if first then " " else "@ * ") ~pre:(if first then " " else "@ * ")
"@ * " "@ * "
(pp_djn ?var_strength (pp_djn ?var_strength
(Set.union vs (Set.union us xs)) (Var.Set.union vs (Var.Set.union us xs))
(Set.union parent_xs xs) cong) (Var.Set.union parent_xs xs)
cong)
fs djns ; fs djns ;
Format.pp_close_box fs () Format.pp_close_box fs ()
@ -265,7 +267,7 @@ and pp_djn ?var_strength vs xs cong fs = function
var_strength_ xs var_strength_stem sjn var_strength_ xs var_strength_stem sjn
in in
Format.fprintf fs "@[<hv 1>(%a)@]" Format.fprintf fs "@[<hv 1>(%a)@]"
(pp_ ?var_strength vs (Set.union xs sjn.xs) cong) (pp_ ?var_strength vs (Var.Set.union xs sjn.xs) cong)
sjn )) sjn ))
djn djn
@ -275,11 +277,13 @@ let pp_diff_eq ?(us = Var.Set.empty) ?(xs = Var.Set.empty) cong fs q =
let pp fs q = pp_diff_eq Equality.true_ fs q let pp fs q = pp_diff_eq Equality.true_ fs q
let pp_djn fs d = pp_djn Var.Set.empty Var.Set.empty Equality.true_ fs d let pp_djn fs d = pp_djn Var.Set.empty Var.Set.empty Equality.true_ fs d
let pp_raw fs q = pp_ Var.Set.empty Var.Set.empty Equality.true_ fs q let pp_raw fs q = pp_ Var.Set.empty Var.Set.empty Equality.true_ fs q
let fv_seg seg = fold_vars_seg seg ~f:Set.add ~init:Var.Set.empty let fv_seg seg = fold_vars_seg seg ~f:Var.Set.add ~init:Var.Set.empty
let fv ?ignore_cong q = let fv ?ignore_cong q =
let rec fv_union init q = let rec fv_union init q =
Set.diff (fold_vars ?ignore_cong fv_union q ~init ~f:Set.add) q.xs Var.Set.diff
(fold_vars ?ignore_cong fv_union q ~init ~f:Var.Set.add)
q.xs
in in
fv_union Var.Set.empty q fv_union Var.Set.empty q
@ -295,12 +299,13 @@ let rec invariant q =
let {us; xs; cong; pure; heap; djns} = q in let {us; xs; cong; pure; heap; djns} = q in
try try
assert ( assert (
Set.disjoint us xs Var.Set.disjoint us xs
|| fail "inter: @[%a@]@\nq: @[%a@]" Var.Set.pp (Set.inter us xs) pp q || fail "inter: @[%a@]@\nq: @[%a@]" Var.Set.pp (Var.Set.inter us xs)
() ) ; pp q () ) ;
assert ( assert (
Set.is_subset (fv q) ~of_:us Var.Set.is_subset (fv q) ~of_:us
|| fail "unbound but free: %a" Var.Set.pp (Set.diff (fv q) us) () ) ; || fail "unbound but free: %a" Var.Set.pp (Var.Set.diff (fv q) us) ()
) ;
Equality.invariant cong ; Equality.invariant cong ;
( match djns with ( match djns with
| [[]] -> | [[]] ->
@ -312,7 +317,7 @@ let rec invariant q =
List.iter heap ~f:invariant_seg ; List.iter heap ~f:invariant_seg ;
List.iter djns ~f:(fun djn -> List.iter djns ~f:(fun djn ->
List.iter djn ~f:(fun sjn -> List.iter djn ~f:(fun sjn ->
assert (Set.is_subset sjn.us ~of_:(Set.union us xs)) ; assert (Var.Set.is_subset sjn.us ~of_:(Var.Set.union us xs)) ;
invariant sjn ) ) invariant sjn ) )
with exc -> [%Trace.info "%a" pp q] ; raise exc with exc -> [%Trace.info "%a" pp q] ; raise exc
@ -324,7 +329,8 @@ let rec apply_subst sub q =
map q ~f_sjn:(rename sub) map q ~f_sjn:(rename sub)
~f_cong:(fun r -> Equality.rename r sub) ~f_cong:(fun r -> Equality.rename r sub)
~f_trm:(Term.rename sub) ~f_trm:(Term.rename sub)
|> check (fun q' -> assert (Set.disjoint (fv q') (Var.Subst.domain sub))) |> check (fun q' ->
assert (Var.Set.disjoint (fv q') (Var.Subst.domain sub)) )
and rename sub q = and rename sub q =
[%Trace.call fun {pf} -> pf "@[%a@]@ %a" Var.Subst.pp sub pp q] [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Var.Subst.pp sub pp q]
@ -333,20 +339,20 @@ and rename sub q =
( if Var.Subst.is_empty sub then q ( if Var.Subst.is_empty sub then q
else else
let us = Var.Subst.apply_set sub q.us in let us = Var.Subst.apply_set sub q.us in
assert (not (Set.equal us q.us)) ; assert (not (Var.Set.equal us q.us)) ;
let q' = apply_subst sub (freshen_xs q ~wrt:(Set.union q.us us)) in let q' = apply_subst sub (freshen_xs q ~wrt:(Var.Set.union q.us us)) in
{q' with us} ) {q' with us} )
|> |>
[%Trace.retn fun {pf} q' -> [%Trace.retn fun {pf} q' ->
pf "%a" pp q' ; pf "%a" pp q' ;
invariant q' ; invariant q' ;
assert (Set.disjoint q'.us (Var.Subst.domain sub))] assert (Var.Set.disjoint q'.us (Var.Subst.domain sub))]
(** freshen existentials, preserving vocabulary *) (** freshen existentials, preserving vocabulary *)
and freshen_xs q ~wrt = and freshen_xs q ~wrt =
[%Trace.call fun {pf} -> [%Trace.call fun {pf} ->
pf "{@[%a@]}@ %a" Var.Set.pp wrt pp q ; pf "{@[%a@]}@ %a" Var.Set.pp wrt pp q ;
assert (Set.is_subset q.us ~of_:wrt)] assert (Var.Set.is_subset q.us ~of_:wrt)]
; ;
let sub = Var.Subst.freshen q.xs ~wrt in let sub = Var.Subst.freshen q.xs ~wrt in
( if Var.Subst.is_empty sub then q ( if Var.Subst.is_empty sub then q
@ -357,32 +363,33 @@ and freshen_xs q ~wrt =
|> |>
[%Trace.retn fun {pf} q' -> [%Trace.retn fun {pf} q' ->
pf "%a@ %a" Var.Subst.pp sub pp q' ; pf "%a@ %a" Var.Subst.pp sub pp q' ;
assert (Set.equal q'.us q.us) ; assert (Var.Set.equal q'.us q.us) ;
assert (Set.disjoint q'.xs (Var.Subst.domain sub)) ; assert (Var.Set.disjoint q'.xs (Var.Subst.domain sub)) ;
assert (Set.disjoint q'.xs (Set.inter q.xs wrt)) ; assert (Var.Set.disjoint q'.xs (Var.Set.inter q.xs wrt)) ;
invariant q'] invariant q']
let extend_us us q = let extend_us us q =
let us = Set.union us q.us in let us = Var.Set.union us q.us in
let q' = freshen_xs q ~wrt:us in let q' = freshen_xs q ~wrt:us in
(if us == q.us && q' == q then q else {q' with us}) |> check invariant (if us == q.us && q' == q then q else {q' with us}) |> check invariant
let freshen ~wrt q = let freshen ~wrt q =
let sub = Var.Subst.freshen q.us ~wrt:(Set.union wrt q.xs) in let sub = Var.Subst.freshen q.us ~wrt:(Var.Set.union wrt q.xs) in
let q' = extend_us wrt (rename sub q) in let q' = extend_us wrt (rename sub q) in
(if q' == q then (q, sub) else (q', sub)) (if q' == q then (q, sub) else (q', sub))
|> check (fun (q', _) -> |> check (fun (q', _) ->
invariant q' ; invariant q' ;
assert (Set.is_subset wrt ~of_:q'.us) ; assert (Var.Set.is_subset wrt ~of_:q'.us) ;
assert (Set.disjoint wrt (fv q')) ) assert (Var.Set.disjoint wrt (fv q')) )
let bind_exists q ~wrt = let bind_exists q ~wrt =
[%Trace.call fun {pf} -> pf "{@[%a@]}@ %a" Var.Set.pp wrt pp q] [%Trace.call fun {pf} -> pf "{@[%a@]}@ %a" Var.Set.pp wrt pp q]
; ;
let q' = let q' =
if Set.is_empty wrt then q else freshen_xs q ~wrt:(Set.union q.us wrt) if Var.Set.is_empty wrt then q
else freshen_xs q ~wrt:(Var.Set.union q.us wrt)
in in
(q'.xs, {q' with us= Set.union q'.us q'.xs; xs= Var.Set.empty}) (q'.xs, {q' with us= Var.Set.union q'.us q'.xs; xs= Var.Set.empty})
|> |>
[%Trace.retn fun {pf} (_, q') -> pf "%a" pp q'] [%Trace.retn fun {pf} (_, q') -> pf "%a" pp q']
@ -390,12 +397,12 @@ let exists_fresh xs q =
[%Trace.call fun {pf} -> [%Trace.call fun {pf} ->
pf "{@[%a@]}@ %a" Var.Set.pp xs pp q ; pf "{@[%a@]}@ %a" Var.Set.pp xs pp q ;
assert ( assert (
Set.disjoint xs q.us Var.Set.disjoint xs q.us
|| fail "Sh.exists_fresh xs ∩ q.us: %a" Var.Set.pp || fail "Sh.exists_fresh xs ∩ q.us: %a" Var.Set.pp
(Set.inter xs q.us) () )] (Var.Set.inter xs q.us) () )]
; ;
( if Set.is_empty xs then q ( if Var.Set.is_empty xs then q
else {q with xs= Set.union q.xs xs} |> check invariant ) else {q with xs= Var.Set.union q.xs xs} |> check invariant )
|> |>
[%Trace.retn fun {pf} -> pf "%a" pp] [%Trace.retn fun {pf} -> pf "%a" pp]
@ -403,26 +410,27 @@ let exists xs q =
[%Trace.call fun {pf} -> pf "{@[%a@]}@ %a" Var.Set.pp xs pp q] [%Trace.call fun {pf} -> pf "{@[%a@]}@ %a" Var.Set.pp xs pp q]
; ;
assert ( assert (
Set.is_subset xs ~of_:q.us Var.Set.is_subset xs ~of_:q.us
|| fail "Sh.exists xs - q.us: %a" Var.Set.pp (Set.diff xs q.us) () ) ; || fail "Sh.exists xs - q.us: %a" Var.Set.pp (Var.Set.diff xs q.us) ()
( if Set.is_empty xs then q ) ;
( if Var.Set.is_empty xs then q
else else
{q with us= Set.diff q.us xs; xs= Set.union q.xs xs} |> check invariant {q with us= Var.Set.diff q.us xs; xs= Var.Set.union q.xs xs}
) |> check invariant )
|> |>
[%Trace.retn fun {pf} -> pf "%a" pp] [%Trace.retn fun {pf} -> pf "%a" pp]
(** remove quantification on variables disjoint from vocabulary *) (** remove quantification on variables disjoint from vocabulary *)
let elim_exists xs q = let elim_exists xs q =
assert (Set.disjoint xs q.us) ; assert (Var.Set.disjoint xs q.us) ;
{q with us= Set.union q.us xs; xs= Set.diff q.xs xs} {q with us= Var.Set.union q.us xs; xs= Var.Set.diff q.xs xs}
(** Construct *) (** Construct *)
(** conjoin an equality relation assuming vocabulary is compatible *) (** conjoin an equality relation assuming vocabulary is compatible *)
let and_cong_ cong q = let and_cong_ cong q =
assert (Set.is_subset (Equality.fv cong) ~of_:q.us) ; assert (Var.Set.is_subset (Equality.fv cong) ~of_:q.us) ;
let xs, cong = Equality.and_ (Set.union q.us q.xs) q.cong cong in let xs, cong = Equality.and_ (Var.Set.union q.us q.xs) q.cong cong in
if Equality.is_false cong then false_ q.us if Equality.is_false cong then false_ q.us
else exists_fresh xs {q with cong} else exists_fresh xs {q with cong}
@ -440,30 +448,30 @@ let star q1 q2 =
; ;
( match (q1, q2) with ( match (q1, q2) with
| {djns= [[]]; _}, _ | _, {djns= [[]]; _} -> | {djns= [[]]; _}, _ | _, {djns= [[]]; _} ->
false_ (Set.union q1.us q2.us) false_ (Var.Set.union q1.us q2.us)
| {us= _; xs= _; cong; pure= []; heap= []; djns= []}, _ | {us= _; xs= _; cong; pure= []; heap= []; djns= []}, _
when Equality.is_true cong -> when Equality.is_true cong ->
let us = Set.union q1.us q2.us in let us = Var.Set.union q1.us q2.us in
if us == q2.us then q2 else {q2 with us} if us == q2.us then q2 else {q2 with us}
| _, {us= _; xs= _; cong; pure= []; heap= []; djns= []} | _, {us= _; xs= _; cong; pure= []; heap= []; djns= []}
when Equality.is_true cong -> when Equality.is_true cong ->
let us = Set.union q1.us q2.us in let us = Var.Set.union q1.us q2.us in
if us == q1.us then q1 else {q1 with us} if us == q1.us then q1 else {q1 with us}
| _ -> | _ ->
let us = Set.union q1.us q2.us in let us = Var.Set.union q1.us q2.us in
let q1 = freshen_xs q1 ~wrt:(Set.union us q2.xs) in let q1 = freshen_xs q1 ~wrt:(Var.Set.union us q2.xs) in
let q2 = freshen_xs q2 ~wrt:(Set.union us q1.xs) in let q2 = freshen_xs q2 ~wrt:(Var.Set.union us q1.xs) in
let {us= us1; xs= xs1; cong= c1; pure= p1; heap= h1; djns= d1} = q1 in let {us= us1; xs= xs1; cong= c1; pure= p1; heap= h1; djns= d1} = q1 in
let {us= us2; xs= xs2; cong= c2; pure= p2; heap= h2; djns= d2} = q2 in let {us= us2; xs= xs2; cong= c2; pure= p2; heap= h2; djns= d2} = q2 in
assert (Set.equal us (Set.union us1 us2)) ; assert (Var.Set.equal us (Var.Set.union us1 us2)) ;
let xs, cong = let xs, cong =
Equality.and_ (Set.union us (Set.union xs1 xs2)) c1 c2 Equality.and_ (Var.Set.union us (Var.Set.union xs1 xs2)) c1 c2
in in
if Equality.is_false cong then false_ us if Equality.is_false cong then false_ us
else else
exists_fresh xs exists_fresh xs
{ us { us
; xs= Set.union xs1 xs2 ; xs= Var.Set.union xs1 xs2
; cong ; cong
; pure= List.append p1 p2 ; pure= List.append p1 p2
; heap= List.append h1 h2 ; heap= List.append h1 h2
@ -472,7 +480,7 @@ let star q1 q2 =
[%Trace.retn fun {pf} q -> [%Trace.retn fun {pf} q ->
pf "%a" pp q ; pf "%a" pp q ;
invariant q ; invariant q ;
assert (Set.equal q.us (Set.union q1.us q2.us))] assert (Var.Set.equal q.us (Var.Set.union q1.us q2.us))]
let starN = function let starN = function
| [] -> emp | [] -> emp
@ -487,14 +495,14 @@ let or_ q1 q2 =
| _, {djns= [[]]; _} -> extend_us q2.us q1 | _, {djns= [[]]; _} -> extend_us q2.us q1
| ( ({djns= []; _} as q) | ( ({djns= []; _} as q)
, ({us= _; xs; cong= _; pure= []; heap= []; djns= [djn]} as d) ) , ({us= _; xs; cong= _; pure= []; heap= []; djns= [djn]} as d) )
when Set.is_empty xs -> when Var.Set.is_empty xs ->
{d with us= Set.union q.us d.us; djns= [q :: djn]} {d with us= Var.Set.union q.us d.us; djns= [q :: djn]}
| ( ({us= _; xs; cong= _; pure= []; heap= []; djns= [djn]} as d) | ( ({us= _; xs; cong= _; pure= []; heap= []; djns= [djn]} as d)
, ({djns= []; _} as q) ) , ({djns= []; _} as q) )
when Set.is_empty xs -> when Var.Set.is_empty xs ->
{d with us= Set.union q.us d.us; djns= [q :: djn]} {d with us= Var.Set.union q.us d.us; djns= [q :: djn]}
| _ -> | _ ->
{ us= Set.union q1.us q2.us { us= Var.Set.union q1.us q2.us
; xs= Var.Set.empty ; xs= Var.Set.empty
; cong= Equality.true_ ; cong= Equality.true_
; pure= [] ; pure= []
@ -504,7 +512,7 @@ let or_ q1 q2 =
[%Trace.retn fun {pf} q -> [%Trace.retn fun {pf} q ->
pf "%a" pp_raw q ; pf "%a" pp_raw q ;
invariant q ; invariant q ;
assert (Set.equal q.us (Set.union q1.us q2.us))] assert (Var.Set.equal q.us (Var.Set.union q1.us q2.us))]
let orN = function let orN = function
| [] -> false_ Var.Set.empty | [] -> false_ Var.Set.empty
@ -545,7 +553,7 @@ let subst sub q =
let dom, eqs = let dom, eqs =
Var.Subst.fold sub ~init:(Var.Set.empty, Term.true_) Var.Subst.fold sub ~init:(Var.Set.empty, Term.true_)
~f:(fun var trm (dom, eqs) -> ~f:(fun var trm (dom, eqs) ->
( Set.add dom var ( Var.Set.add dom var
, Term.and_ (Term.eq (Term.var var) (Term.var trm)) eqs ) ) , Term.and_ (Term.eq (Term.var var) (Term.var trm)) eqs ) )
in in
exists dom (and_ eqs q) exists dom (and_ eqs q)
@ -553,7 +561,7 @@ let subst sub q =
[%Trace.retn fun {pf} q' -> [%Trace.retn fun {pf} q' ->
pf "%a" pp q' ; pf "%a" pp q' ;
invariant q' ; invariant q' ;
assert (Set.disjoint q'.us (Var.Subst.domain sub))] assert (Var.Set.disjoint q'.us (Var.Subst.domain sub))]
let seg pt = let seg pt =
let us = fv_seg pt in let us = fv_seg pt in
@ -603,7 +611,7 @@ let pure_approx q =
let fold_dnf ~conj ~disj sjn (xs, conjuncts) disjuncts = let fold_dnf ~conj ~disj sjn (xs, conjuncts) disjuncts =
let rec add_disjunct pending_splits sjn (xs, conjuncts) disjuncts = let rec add_disjunct pending_splits sjn (xs, conjuncts) disjuncts =
let ys, sjn = bind_exists sjn ~wrt:xs in let ys, sjn = bind_exists sjn ~wrt:xs in
let xs = Set.union ys xs in let xs = Var.Set.union ys xs in
let djns = sjn.djns in let djns = sjn.djns in
let sjn = {sjn with djns= []} in let sjn = {sjn with djns= []} in
split_case split_case
@ -638,7 +646,7 @@ let rec norm_ s q =
let q = let q =
map q ~f_sjn:(norm_ s) ~f_cong:Fn.id ~f_trm:(Equality.Subst.subst s) map q ~f_sjn:(norm_ s) ~f_cong:Fn.id ~f_trm:(Equality.Subst.subst s)
in in
let xs, cong = Equality.apply_subst (Set.union q.us q.xs) s q.cong in let xs, cong = Equality.apply_subst (Var.Set.union q.us q.xs) s q.cong in
exists_fresh xs {q with cong} exists_fresh xs {q with cong}
|> |>
[%Trace.retn fun {pf} q' -> pf "%a" pp_raw q' ; invariant q'] [%Trace.retn fun {pf} q' -> pf "%a" pp_raw q' ; invariant q']
@ -657,19 +665,19 @@ let rec freshen_nested_xs q =
; ;
(* trim xs to those that appear in the stem and sink the rest *) (* trim xs to those that appear in the stem and sink the rest *)
let fv_stem = fv {q with xs= Var.Set.empty; djns= []} in let fv_stem = fv {q with xs= Var.Set.empty; djns= []} in
let xs_sink, xs = Set.diff_inter q.xs fv_stem in let xs_sink, xs = Var.Set.diff_inter q.xs fv_stem in
let xs_below, djns = let xs_below, djns =
List.fold_map ~init:Var.Set.empty q.djns ~f:(fun xs_below djn -> List.fold_map ~init:Var.Set.empty q.djns ~f:(fun xs_below djn ->
List.fold_map ~init:xs_below djn ~f:(fun xs_below dj -> List.fold_map ~init:xs_below djn ~f:(fun xs_below dj ->
(* quantify xs not in stem and freshen disjunct *) (* quantify xs not in stem and freshen disjunct *)
let dj' = let dj' =
freshen_nested_xs (exists (Set.inter xs_sink dj.us) dj) freshen_nested_xs (exists (Var.Set.inter xs_sink dj.us) dj)
in in
let xs_below' = Set.union xs_below dj'.xs in let xs_below' = Var.Set.union xs_below dj'.xs in
(xs_below', dj') ) ) (xs_below', dj') ) )
in in
(* rename xs to miss all xs in subformulas *) (* rename xs to miss all xs in subformulas *)
freshen_xs {q with xs; djns} ~wrt:(Set.union q.us xs_below) freshen_xs {q with xs; djns} ~wrt:(Var.Set.union q.us xs_below)
|> |>
[%Trace.retn fun {pf} q' -> pf "%a" pp q' ; invariant q'] [%Trace.retn fun {pf} q' -> pf "%a" pp q' ; invariant q']
@ -678,7 +686,7 @@ let rec propagate_equality_ ancestor_vs ancestor_cong q =
pf "(%a)@ %a" Equality.pp_classes ancestor_cong pp q] pf "(%a)@ %a" Equality.pp_classes ancestor_cong pp q]
; ;
(* extend vocabulary with variables in scope above *) (* extend vocabulary with variables in scope above *)
let ancestor_vs = Set.union ancestor_vs (Set.union q.us q.xs) in let ancestor_vs = Var.Set.union ancestor_vs (Var.Set.union q.us q.xs) in
(* decompose formula *) (* decompose formula *)
let xs, stem, djns = let xs, stem, djns =
(q.xs, {q with us= ancestor_vs; xs= emp.xs; djns= emp.djns}, q.djns) (q.xs, {q with us= ancestor_vs; xs= emp.xs; djns= emp.djns}, q.djns)
@ -695,10 +703,10 @@ let rec propagate_equality_ ancestor_vs ancestor_cong q =
in in
let new_xs, djn_cong = Equality.orN ancestor_vs dj_congs in let new_xs, djn_cong = Equality.orN ancestor_vs dj_congs in
(* hoist xs appearing in disjunction's equality relation *) (* hoist xs appearing in disjunction's equality relation *)
let djn_xs = Set.diff (Equality.fv djn_cong) q'.us in let djn_xs = Var.Set.diff (Equality.fv djn_cong) q'.us in
let djn = List.map ~f:(elim_exists djn_xs) djn in let djn = List.map ~f:(elim_exists djn_xs) djn in
let cong_djn = and_cong_ djn_cong (orN djn) in let cong_djn = and_cong_ djn_cong (orN djn) in
assert (is_false cong_djn || Set.is_subset new_xs ~of_:djn_xs) ; assert (is_false cong_djn || Var.Set.is_subset new_xs ~of_:djn_xs) ;
star (exists djn_xs cong_djn) q' )) star (exists djn_xs cong_djn) q' ))
|> |>
[%Trace.retn fun {pf} q' -> pf "%a" pp q' ; invariant q'] [%Trace.retn fun {pf} q' -> pf "%a" pp q' ; invariant q']
@ -717,16 +725,17 @@ let pp_vss fs vss =
vss vss
let remove_absent_xs ks q = let remove_absent_xs ks q =
let ks = Set.inter ks q.xs in let ks = Var.Set.inter ks q.xs in
if Set.is_empty ks then q if Var.Set.is_empty ks then q
else else
let xs = Set.diff q.xs ks in let xs = Var.Set.diff q.xs ks in
let djns = let djns =
let rec trim_ks ks djns = let rec trim_ks ks djns =
List.map djns ~f:(fun djn -> List.map djns ~f:(fun djn ->
List.map djn ~f:(fun sjn -> List.map djn ~f:(fun sjn ->
{sjn with us= Set.diff sjn.us ks; djns= trim_ks ks sjn.djns} { sjn with
) ) us= Var.Set.diff sjn.us ks
; djns= trim_ks ks sjn.djns } ) )
in in
trim_ks ks q.djns trim_ks ks q.djns
in in
@ -740,7 +749,7 @@ let rec simplify_ us rev_xss q =
let q = let q =
exists q.xs exists q.xs
(starN (starN
( {q with us= Set.union q.us q.xs; xs= emp.xs; djns= []} ( {q with us= Var.Set.union q.us q.xs; xs= emp.xs; djns= []}
:: List.map q.djns ~f:(fun djn -> :: List.map q.djns ~f:(fun djn ->
orN (List.map djn ~f:(fun sjn -> simplify_ us rev_xss sjn)) orN (List.map djn ~f:(fun sjn -> simplify_ us rev_xss sjn))
) )) ) ))
@ -755,7 +764,7 @@ let rec simplify_ us rev_xss q =
let q = norm subst q in let q = norm subst q in
(* reconjoin only non-redundant equations *) (* reconjoin only non-redundant equations *)
let removed = let removed =
Set.diff Var.Set.diff
(Var.Set.union_list rev_xss) (Var.Set.union_list rev_xss)
(fv ~ignore_cong:() (elim_exists q.xs q)) (fv ~ignore_cong:() (elim_exists q.xs q))
in in

85
sledge/lib/solver.ml
Unescape View File

@ -69,7 +69,7 @@ end = struct
Format.fprintf fs "@[<hv>%s %a@ | %a@ @[\\- %a%a@]@]" Format.fprintf fs "@[<hv>%s %a@ | %a@ @[\\- %a%a@]@]"
(if pgs then "t" else "f") (if pgs then "t" else "f")
Sh.pp com Sh.pp min Var.Set.pp_xs xs Sh.pp com Sh.pp min Var.Set.pp_xs xs
(Sh.pp_diff_eq ~us:(Set.union min.us sub.us) ~xs min.cong) (Sh.pp_diff_eq ~us:(Var.Set.union min.us sub.us) ~xs min.cong)
sub sub
let invariant g = let invariant g =
@ -77,11 +77,11 @@ end = struct
@@ fun () -> @@ fun () ->
try try
let {us; com; min; xs; sub; zs; pgs= _} = g in let {us; com; min; xs; sub; zs; pgs= _} = g in
assert (Set.equal us com.us) ; assert (Var.Set.equal us com.us) ;
assert (Set.equal us min.us) ; assert (Var.Set.equal us min.us) ;
assert (Set.equal (Set.union us xs) sub.us) ; assert (Var.Set.equal (Var.Set.union us xs) sub.us) ;
assert (Set.disjoint us xs) ; assert (Var.Set.disjoint us xs) ;
assert (Set.is_subset zs ~of_:(Set.union us xs)) assert (Var.Set.is_subset zs ~of_:(Var.Set.union us xs))
with exc -> [%Trace.info "%a" pp g] ; raise exc with exc -> [%Trace.info "%a" pp g] ; raise exc
let with_ ?us ?com ?min ?xs ?sub ?zs ?pgs g = let with_ ?us ?com ?min ?xs ?sub ?zs ?pgs g =
@ -91,11 +91,13 @@ end = struct
let us = Option.value us ~default:Var.Set.empty in let us = Option.value us ~default:Var.Set.empty in
let us = let us =
Option.fold Option.fold
~f:(fun us sub -> Set.union (Set.diff sub.Sh.us xs) us) ~f:(fun us sub -> Var.Set.union (Var.Set.diff sub.Sh.us xs) us)
sub ~init:us sub ~init:us
in in
let union_us q_opt us' = let union_us q_opt us' =
Option.fold ~f:(fun us' q -> Set.union q.Sh.us us') q_opt ~init:us' Option.fold
~f:(fun us' q -> Var.Set.union q.Sh.us us')
q_opt ~init:us'
in in
union_us com (union_us min us) union_us com (union_us min us)
in in
@ -104,10 +106,10 @@ end = struct
let xs, sub, zs = let xs, sub, zs =
match sub with match sub with
| Some sub -> | Some sub ->
let sub = Sh.extend_us (Set.union new_us xs) sub in let sub = Sh.extend_us (Var.Set.union new_us xs) sub in
let ys, sub = Sh.bind_exists sub ~wrt:xs in let ys, sub = Sh.bind_exists sub ~wrt:xs in
let xs = Set.union xs ys in let xs = Var.Set.union xs ys in
let zs = Set.union zs ys in let zs = Var.Set.union zs ys in
(xs, sub, zs) (xs, sub, zs)
| None -> | None ->
let sub = Sh.extend_us new_us (Option.value sub ~default:g.sub) in let sub = Sh.extend_us new_us (Option.value sub ~default:g.sub) in
@ -131,8 +133,8 @@ open Goal
let fresh_var name vs zs ~wrt = let fresh_var name vs zs ~wrt =
let v, wrt = Var.fresh name ~wrt in let v, wrt = Var.fresh name ~wrt in
let vs = Set.add vs v in let vs = Var.Set.add vs v in
let zs = Set.add zs v in let zs = Var.Set.add zs v in
let v = Term.var v in let v = Term.var v in
(v, vs, zs, wrt) (v, vs, zs, wrt)
@ -141,21 +143,22 @@ let trace (k : Trace.pf -> _) = [%Trace.infok k]
let excise_exists goal = let excise_exists goal =
trace (fun {pf} -> pf "@[<2>excise_exists@ %a@]" pp goal) ; trace (fun {pf} -> pf "@[<2>excise_exists@ %a@]" pp goal) ;
if Set.is_empty goal.xs then goal if Var.Set.is_empty goal.xs then goal
else else
let solutions_for_xs = let solutions_for_xs =
let xs = let xs =
Set.diff goal.xs (Sh.fv ~ignore_cong:() (Sh.with_pure [] goal.sub)) Var.Set.diff goal.xs
(Sh.fv ~ignore_cong:() (Sh.with_pure [] goal.sub))
in in
Equality.solve_for_vars [Var.Set.empty; goal.us; xs] goal.sub.cong Equality.solve_for_vars [Var.Set.empty; goal.us; xs] goal.sub.cong
in in
if Equality.Subst.is_empty solutions_for_xs then goal if Equality.Subst.is_empty solutions_for_xs then goal
else else
let removed = let removed =
Set.diff goal.xs Var.Set.diff goal.xs
(Sh.fv ~ignore_cong:() (Sh.norm solutions_for_xs goal.sub)) (Sh.fv ~ignore_cong:() (Sh.norm solutions_for_xs goal.sub))
in in
if Set.is_empty removed then goal if Var.Set.is_empty removed then goal
else else
let _, removed, witnesses = let _, removed, witnesses =
Equality.Subst.partition_valid removed solutions_for_xs Equality.Subst.partition_valid removed solutions_for_xs
@ -165,8 +168,8 @@ let excise_exists goal =
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<2>excise_exists @[%a%a@]@]" Var.Set.pp_xs removed pf "@[<2>excise_exists @[%a%a@]@]" Var.Set.pp_xs removed
Equality.Subst.pp witnesses ) ; Equality.Subst.pp witnesses ) ;
let us = Set.union goal.us removed in let us = Var.Set.union goal.us removed in
let xs = Set.diff goal.xs removed in let xs = Var.Set.diff goal.xs removed in
let min = Sh.and_subst witnesses goal.min in let min = Sh.and_subst witnesses goal.min in
goal |> with_ ~us ~min ~xs ~pgs:true ) goal |> with_ ~us ~min ~xs ~pgs:true )
@ -234,9 +237,9 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
let {Sh.bas= b'; len= m'; siz= n; arr= a'} = ssg in let {Sh.bas= b'; len= m'; siz= n; arr= a'} = ssg in
let o_n = Term.integer o_n in let o_n = Term.integer o_n in
let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Var.Set.union us xs) in
let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in
let xs = Set.diff xs (Term.fv n) in let xs = Var.Set.diff xs (Term.fv n) in
let com = Sh.star (Sh.seg {msg with siz= n; arr= a0}) com in let com = Sh.star (Sh.seg {msg with siz= n; arr= a0}) com in
let min = let min =
Sh.and_ Sh.and_
@ -276,7 +279,7 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
let n_o = Term.integer n_o in let n_o = Term.integer n_o in
let com = Sh.star (Sh.seg msg) com in let com = Sh.star (Sh.seg msg) com in
let min = Sh.rem_seg msg min in let min = Sh.rem_seg msg min in
let a1', xs, zs, _ = fresh_var "a1" xs zs ~wrt:(Set.union us xs) in let a1', xs, zs, _ = fresh_var "a1" xs zs ~wrt:(Var.Set.union us xs) in
let sub = let sub =
Sh.and_ (Term.eq b b') Sh.and_ (Term.eq b b')
(Sh.and_ (Term.eq m m') (Sh.and_ (Term.eq m m')
@ -310,9 +313,9 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
let l_k = Term.integer l_k in let l_k = Term.integer l_k in
let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Var.Set.union us xs) in
let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in
let xs = Set.diff xs (Term.fv n) in let xs = Var.Set.diff xs (Term.fv n) in
let com = let com =
Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a1}) com Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a1}) com
in in
@ -354,10 +357,10 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
let l_k = Term.integer l_k in let l_k = Term.integer l_k in
let ko_ln = Term.integer ko_ln in let ko_ln = Term.integer ko_ln in
let ln = Term.add l n in let ln = Term.add l n in
let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Var.Set.union us xs) in
let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in
let xs = Set.diff xs (Set.union (Term.fv l) (Term.fv n)) in let xs = Var.Set.diff xs (Var.Set.union (Term.fv l) (Term.fv n)) in
let com = let com =
Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a1}) com Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a1}) com
in in
@ -402,10 +405,10 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
let ko_l = Term.integer ko_l in let ko_l = Term.integer ko_l in
let ln_ko = Term.integer ln_ko in let ln_ko = Term.integer ln_ko in
let ko = Term.add k o in let ko = Term.add k o in
let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Var.Set.union us xs) in
let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in
let xs = Set.diff xs (Term.fv l) in let xs = Var.Set.diff xs (Term.fv l) in
let com = let com =
Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= ko_l; arr= a1}) com Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= ko_l; arr= a1}) com
in in
@ -449,7 +452,7 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
let {Sh.bas= b; len= m; siz= o; arr= a} = msg in let {Sh.bas= b; len= m; siz= o; arr= a} = msg in
let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
let k_l = Term.integer k_l in let k_l = Term.integer k_l in
let a0', xs, zs, _ = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in let a0', xs, zs, _ = fresh_var "a0" xs zs ~wrt:(Var.Set.union us xs) in
let com = Sh.star (Sh.seg msg) com in let com = Sh.star (Sh.seg msg) com in
let min = Sh.rem_seg msg min in let min = Sh.rem_seg msg min in
let sub = let sub =
@ -488,7 +491,7 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
let k_l = Term.integer k_l in let k_l = Term.integer k_l in
let ln_ko = Term.integer ln_ko in let ln_ko = Term.integer ln_ko in
let ko = Term.add k o in let ko = Term.add k o in
let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Var.Set.union us xs) in
let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in
let com = Sh.star (Sh.seg msg) com in let com = Sh.star (Sh.seg msg) com in
let min = Sh.rem_seg msg min in let min = Sh.rem_seg msg min in
@ -530,7 +533,7 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
let ln_k = Term.integer ln_k in let ln_k = Term.integer ln_k in
let ko_ln = Term.integer ko_ln in let ko_ln = Term.integer ko_ln in
let ln = Term.add l n in let ln = Term.add l n in
let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Var.Set.union us xs) in
let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in
let com = let com =
@ -644,7 +647,7 @@ let excise_heap ({min; sub} as goal) =
let rec excise ({min; xs; sub; zs; pgs} as goal) = let rec excise ({min; xs; sub; zs; pgs} as goal) =
[%Trace.info "@[<2>excise@ %a@]" pp goal] ; [%Trace.info "@[<2>excise@ %a@]" pp goal] ;
if Sh.is_false min then Some (Sh.false_ (Set.diff sub.us zs)) if Sh.is_false min then Some (Sh.false_ (Var.Set.diff sub.us zs))
else if Sh.is_emp sub then Some (Sh.exists zs (Sh.extend_us xs min)) else if Sh.is_emp sub then Some (Sh.exists zs (Sh.extend_us xs min))
else if Sh.is_false sub then None else if Sh.is_false sub then None
else if pgs then else if pgs then
@ -657,7 +660,7 @@ let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
let dnf_minuend = Sh.dnf minuend in let dnf_minuend = Sh.dnf minuend in
let dnf_subtrahend = Sh.dnf subtrahend in let dnf_subtrahend = Sh.dnf subtrahend in
List.fold_option dnf_minuend List.fold_option dnf_minuend
~init:(Sh.false_ (Set.union minuend.us xs)) ~init:(Sh.false_ (Var.Set.union minuend.us xs))
~f:(fun remainders minuend -> ~f:(fun remainders minuend ->
([%Trace.call fun {pf} -> pf "@[<2>minuend@ %a@]" Sh.pp minuend] ([%Trace.call fun {pf} -> pf "@[<2>minuend@ %a@]" Sh.pp minuend]
; ;
@ -683,16 +686,16 @@ let infer_frame : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
pf "@[<hv>%a@ \\- %a%a@]" Sh.pp minuend Var.Set.pp_xs xs Sh.pp pf "@[<hv>%a@ \\- %a%a@]" Sh.pp minuend Var.Set.pp_xs xs Sh.pp
subtrahend] subtrahend]
; ;
assert (Set.disjoint minuend.us xs) ; assert (Var.Set.disjoint minuend.us xs) ;
assert (Set.is_subset xs ~of_:subtrahend.us) ; assert (Var.Set.is_subset xs ~of_:subtrahend.us) ;
assert (Set.is_subset (Set.diff subtrahend.us xs) ~of_:minuend.us) ; assert (Var.Set.is_subset (Var.Set.diff subtrahend.us xs) ~of_:minuend.us) ;
excise_dnf minuend xs subtrahend excise_dnf minuend xs subtrahend
|> |>
[%Trace.retn fun {pf} r -> [%Trace.retn fun {pf} r ->
pf "%a" (Option.pp "%a" Sh.pp) r ; pf "%a" (Option.pp "%a" Sh.pp) r ;
Option.iter r ~f:(fun frame -> Option.iter r ~f:(fun frame ->
let lost = Set.diff (Set.union minuend.us xs) frame.us in let lost = Var.Set.diff (Var.Set.union minuend.us xs) frame.us in
let gain = Set.diff frame.us (Set.union minuend.us xs) in let gain = Var.Set.diff frame.us (Var.Set.union minuend.us xs) in
assert (Set.is_empty lost || fail "lost: %a" Var.Set.pp lost ()) ; assert (Var.Set.is_empty lost || fail "lost: %a" Var.Set.pp lost ()) ;
assert (Set.is_empty gain || fail "gained: %a" Var.Set.pp gain ()) assert (
)] Var.Set.is_empty gain || fail "gained: %a" Var.Set.pp gain () ) )]

21
sledge/lib/term.ml
Unescape View File

@ -118,6 +118,12 @@ type _t = T0.t
include T include T
module Map = Map.Make (T) module Map = Map.Make (T)
module Set = struct
include Set.Make (T)
let t_of_sexp = t_of_sexp T.t_of_sexp
end
let empty_qset = Qset.empty (module T) let empty_qset = Qset.empty (module T)
let fix (f : (t -> 'a as 'f) -> 'f) (bot : 'f) (e : t) : 'a = let fix (f : (t -> 'a as 'f) -> 'f) (bot : 'f) (e : t) : 'a =
@ -316,11 +322,7 @@ module Var = struct
module Map = Map module Map = Map
module Set = struct module Set = struct
include ( include Set
Set :
module type of Set with type ('elt, 'cmp) t := ('elt, 'cmp) Set.t )
type t = Set.M(T).t [@@deriving compare, equal, sexp]
let pp vs = Set.pp pp_t vs let pp vs = Set.pp pp_t vs
let ppx strength vs = Set.pp (ppx strength) vs let ppx strength vs = Set.pp (ppx strength) vs
@ -328,13 +330,6 @@ module Var = struct
let pp_xs fs xs = let pp_xs fs xs =
if not (is_empty xs) then if not (is_empty xs) then
Format.fprintf fs "@<2>∃ @[%a@] .@;<1 2>" pp xs Format.fprintf fs "@<2>∃ @[%a@] .@;<1 2>" pp xs
let empty = Set.empty (module T)
let of_ = Set.add empty
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 union_list = Set.union_list (module T)
end end
let invariant x = let invariant x =
@ -415,7 +410,7 @@ module Var = struct
let apply_set sub vs = let apply_set sub vs =
Map.fold sub ~init:vs ~f:(fun ~key ~data vs -> Map.fold sub ~init:vs ~f:(fun ~key ~data vs ->
let vs' = Set.remove vs key in let vs' = Set.remove vs key in
if Set.to_tree vs' == Set.to_tree vs then vs if vs' == vs then vs
else ( else (
assert (not (Set.equal vs' vs)) ; assert (not (Set.equal vs' vs)) ;
Set.add vs' data ) ) Set.add vs' data ) )

17
sledge/lib/term.mli
Unescape View File

@ -93,25 +93,18 @@ module Var : sig
type strength = t -> [`Universal | `Existential | `Anonymous] option type strength = t -> [`Universal | `Existential | `Anonymous] option
module Set : sig module Map : Map.S with type key := t
type var := t
type t = (var, comparator_witness) Set.t module Set : sig
[@@deriving compare, equal, sexp] include Set.S with type elt := t
val sexp_of_t : t -> Sexp.t
val t_of_sexp : Sexp.t -> t
val ppx : strength -> t pp val ppx : strength -> t pp
val pp : t pp val pp : t pp
val pp_xs : t pp val pp_xs : t pp
val empty : t
val of_ : var -> t
val of_option : var option -> t
val of_list : var list -> t
val of_vector : var vector -> t
val union_list : t list -> t
end end
module Map : Map.S with type key := t
val pp : t pp val pp : t pp
include Invariant.S with type t := t include Invariant.S with type t := t

Write Preview
Loading…
Cancel
Save