diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 3dad80fe5..e3472d78d 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -232,9 +232,15 @@ module Make (Dom : Domain_sig.Dom) = struct match Fheap.pop pq0 with | Some ((_, ({Edge.dst; stk} as edge)), pq) -> ( match Map.find_and_remove ws dst with - | Some (state :: states, ws) -> + | Some (q :: qs, ws) -> let join (qa, da) (q, d) = (Dom.join q qa, Depths.join d da) in - let qs, depths = List.fold ~f:join ~init:state states in + let skipped, (qs, depths) = + List.fold qs ~init:([], q) ~f:(fun (skipped, joined) curr -> + match join curr joined with + | Some joined, depths -> (skipped, (joined, depths)) + | None, _ -> (curr :: skipped, joined) ) + in + let ws = Map.add_exn ws ~key:dst ~data:skipped in run ~f (f stk qs dst depths (pq, ws, bnd)) | _ -> [%Trace.info "done: %a" Edge.pp edge] ; diff --git a/sledge/src/domain/domain_sig.ml b/sledge/src/domain/domain_sig.ml index a38400c25..70b95e4e0 100644 --- a/sledge/src/domain/domain_sig.ml +++ b/sledge/src/domain/domain_sig.ml @@ -12,7 +12,7 @@ module type Dom = sig val pp : t pp val report_fmt_thunk : t -> Formatter.t -> unit val init : Global.t vector -> t - val join : t -> t -> t + val join : t -> t -> t option val is_false : t -> bool val exec_assume : t -> Exp.t -> t option val exec_kill : t -> Var.t -> t diff --git a/sledge/src/domain/relation.ml b/sledge/src/domain/relation.ml index bb644f667..a1fb3f4cc 100644 --- a/sledge/src/domain/relation.ml +++ b/sledge/src/domain/relation.ml @@ -32,8 +32,10 @@ module Make (State_domain : State_domain_sig) = struct let init globals = embed (State_domain.init globals) let join (entry_a, current_a) (entry_b, current_b) = - assert (State_domain.equal entry_b entry_a) ; - (entry_a, State_domain.join current_a current_b) + if State_domain.equal entry_b entry_a then + State_domain.join current_a current_b + >>= fun curr -> Some (entry_a, curr) + else None let is_false (_, curr) = State_domain.is_false curr diff --git a/sledge/src/domain/unit.ml b/sledge/src/domain/unit.ml index eaf392374..ce7e375f4 100644 --- a/sledge/src/domain/unit.ml +++ b/sledge/src/domain/unit.ml @@ -12,7 +12,7 @@ type t = unit [@@deriving equal, sexp_of] let pp fs () = Format.pp_print_string fs "()" let report_fmt_thunk () fs = pp fs () let init _ = () -let join () () = () +let join () () = Some () let is_false _ = false let exec_assume () _ = Some () let exec_kill () _ = () diff --git a/sledge/src/domain/used_globals.ml b/sledge/src/domain/used_globals.ml index a6f78f34e..d6ec071d4 100644 --- a/sledge/src/domain/used_globals.ml +++ b/sledge/src/domain/used_globals.ml @@ -18,7 +18,7 @@ let init globals = "pgm globals: {%a}" (Vector.pp ", " Llair_.Global.pp) globals] ; empty -let join = Set.union +let join l r = Some (Set.union l r) let recursion_beyond_bound = `skip let is_false _ = false let post _ _ state = state diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml index 783fbede5..bc3d14967 100644 --- a/sledge/src/symbheap/state_domain.ml +++ b/sledge/src/symbheap/state_domain.ml @@ -25,7 +25,7 @@ let init globals = Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr}) | _ -> q ) -let join = Sh.or_ +let join l r = Some (Sh.or_ l r) let is_false = Sh.is_false let exec_assume = Exec.assume let exec_kill = Exec.kill