From 3e5b4c81830309054bda7590b56afc1f4b13799b Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 31 Mar 2021 12:54:16 -0700 Subject: [PATCH] [sledge] Make tracing more explicit by including module names Summary: There are not too many cases where the function name is not enough to disambiguate a trace message, but it is still perhaps more approachable to include the module names as well. Reviewed By: jvillard Differential Revision: D27396914 fbshipit-source-id: ea4c8b44f --- sledge/cli/frontend.ml | 2 +- sledge/ppx_trace/trace/trace.ml | 26 ++++++--- sledge/src/control.ml | 73 +++++++++++++------------ sledge/src/domain_used_globals.ml | 2 +- sledge/src/fol/context.ml | 5 +- sledge/src/llair/llair.ml | 2 +- sledge/src/sh.ml | 2 +- sledge/src/solver.ml | 91 ++++++++++++++++--------------- sledge/src/test/solver_test.ml | 63 +++++++++++---------- 9 files changed, 142 insertions(+), 124 deletions(-) diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml index 3f4d27f5f..0acddc50d 100644 --- a/sledge/cli/frontend.ml +++ b/sledge/cli/frontend.ml @@ -1501,7 +1501,7 @@ let xlate_block : pop_thunk -> x -> Llvm.llbasicblock -> Llair.block list = let report_undefined func name = if Option.is_some (Llvm.use_begin func) then - [%Trace.info "undefined function: %a" Function.pp name] + [%Trace.printf "@\n@[undefined function: %a@]" Function.pp name] let xlate_function_decl x llfunc typ k = let loc = find_loc llfunc in diff --git a/sledge/ppx_trace/trace/trace.ml b/sledge/ppx_trace/trace/trace.ml index ea87f598e..586d5b11b 100644 --- a/sledge/ppx_trace/trace/trace.ml +++ b/sledge/ppx_trace/trace/trace.ml @@ -191,25 +191,33 @@ let fprintf mod_fun_name fs fmt = let printf mod_fun_name fmt = fprintf mod_fun_name fs fmt let info mod_fun_name fmt = - if enabled mod_fun_name then ( - Format.fprintf fs "@\n@[<2>| " ; - Format.kfprintf (fun fs -> Format.fprintf fs "@]") fs fmt ) - else Format.ifprintf fs fmt + if not (enabled mod_fun_name) then Format.ifprintf fs fmt + else + let mod_name, fun_name = split_mod_fun_name mod_fun_name in + Format.fprintf fs "@\n@[<4>| %s.%s:" mod_name fun_name ; + Format.kfprintf (fun fs -> Format.fprintf fs "@]") fs fmt + +let infok_ mod_fun_name fmt = + if not (enabled mod_fun_name) then Format.ifprintf fs fmt + else + let mod_name, _ = split_mod_fun_name mod_fun_name in + Format.fprintf fs "@\n@[<4>| %s." mod_name ; + Format.kfprintf (fun fs -> Format.fprintf fs "@]") fs fmt -let infok mod_fun_name k = k {pf= (fun fmt -> info mod_fun_name fmt)} +let infok mod_fun_name k = k {pf= (fun fmt -> infok_ mod_fun_name fmt)} let incf mod_fun_name fmt = if not (enabled mod_fun_name) then Format.ifprintf fs fmt else - let _, fun_name = split_mod_fun_name mod_fun_name in - Format.fprintf fs "@\n@[<2>@[( %s:" fun_name ; + let mod_name, fun_name = split_mod_fun_name mod_fun_name in + Format.fprintf fs "@\n@[<2>@[( %s.%s:" mod_name fun_name ; Format.kfprintf (fun fs -> Format.fprintf fs "@]") fs fmt let decf mod_fun_name fmt = if not (enabled mod_fun_name) then Format.ifprintf fs fmt else - let _, fun_name = split_mod_fun_name mod_fun_name in - Format.fprintf fs "@]@\n@[<2>) %s:@ " fun_name ; + let mod_name, fun_name = split_mod_fun_name mod_fun_name in + Format.fprintf fs "@]@\n@[<2>) %s.%s:@ " mod_name fun_name ; Format.kfprintf (fun fs -> Format.fprintf fs "@]") fs fmt let call mod_fun_name k = k {pf= (fun fmt -> incf mod_fun_name fmt)} diff --git a/sledge/src/control.ml b/sledge/src/control.ml index aa7e16b50..f02c48e9f 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -259,6 +259,37 @@ module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct Some (top, elts, {queue; removed}) end + let enqueue depth edge state depths queue = + [%Trace.info + " %i: %a [%a]@ | %a" depth Edge.pp edge Stack.pp edge.stk + PrioQueue.pp queue] ; + let depths = Depths.add ~key:edge ~data:depth depths in + PrioQueue.add {depth; edge; state; depths} queue + + let prune depth edge queue = + [%Trace.info " %i: %a" depth Edge.pp edge] ; + Report.hit_bound Opts.bound ; + queue + + let dequeue queue = + let+ {depth; edge; state; depths}, elts, queue = + PrioQueue.pop queue + in + [%Trace.info + " %i: %a [%a]@ | %a" depth Edge.pp edge Stack.pp edge.stk + PrioQueue.pp queue] ; + let state, depths, queue = + List.fold elts (state, depths, queue) + ~f:(fun elt (state, depths, queue) -> + match Dom.join elt.state state with + | Some state -> + let depths = Depths.join elt.depths depths in + let queue = PrioQueue.remove elt queue in + (state, depths, queue) + | None -> (state, depths, queue) ) + in + (edge, state, depths, queue) + type t = PrioQueue.t type x = Depths.t -> t -> t @@ -269,41 +300,18 @@ module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct let edge = {Edge.dst= curr; src= prev; stk} in let depth = Option.value (Depths.find edge depths) ~default:0 in let depth = if retreating then depth + 1 else depth in - if depth <= Opts.bound then ( - [%Trace.info - "@[<6>enqueue %i: %a [%a]@ | %a@]" depth Edge.pp edge Stack.pp - edge.stk PrioQueue.pp queue] ; - let depths = Depths.add ~key:edge ~data:depth depths in - PrioQueue.add {depth; edge; state; depths} queue ) - else ( - [%Trace.info "prune: %i: %a" depth Edge.pp edge] ; - Report.hit_bound Opts.bound ; - queue ) + if depth <= Opts.bound then enqueue depth edge state depths queue + else prune depth edge queue let init state curr = add ~retreating:false Stack.empty state curr Depths.empty (PrioQueue.create ()) let rec run ~f queue = - match PrioQueue.pop queue with - | Some ({depth; edge; state; depths}, elts, queue) -> - [%Trace.info - "@[<6>dequeue %i: %a [%a]@ | %a@]" depth Edge.pp edge Stack.pp - edge.stk PrioQueue.pp queue] ; - let state, depths, queue = - List.fold elts (state, depths, queue) - ~f:(fun elt (state, depths, queue) -> - match Dom.join elt.state state with - | Some state -> - let depths = Depths.join elt.depths depths in - let queue = PrioQueue.remove elt queue in - (state, depths, queue) - | None -> (state, depths, queue) ) - in + match dequeue queue with + | Some (edge, state, depths, queue) -> run ~f (f edge.stk state edge.dst depths queue) - | None -> - [%Trace.info "queue empty"] ; - () + | None -> () end let exec_jump stk state block Llair.{dst; retreating} = @@ -447,15 +455,13 @@ module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct | Some state -> exec_jump stk state block jump | None -> [%Trace.info - "@[<2>infeasible assume %a@\n@[%a@]@]" Llair.Exp.pp cond Dom.pp - state] ; + " infeasible %a@\n@[%a@]" Llair.Exp.pp cond Dom.pp state] ; Work.skip let exec_term : Llair.program -> Stack.t -> Dom.t -> Llair.block -> Work.x = fun pgm stk state block -> - [%Trace.info - "@[<2>exec term@\n@[%a@]@\n%a@]" Dom.pp state Llair.Term.pp block.term] ; + [%Trace.info "@\n@[%a@]@\n%a" Dom.pp state Llair.Term.pp block.term] ; Report.step_term block ; match block.term with | Switch {key; tbl; els} -> @@ -499,8 +505,7 @@ module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct -> Dom.t -> (Dom.t, Dom.t * Llair.inst) result = fun block inst state -> - [%Trace.info - "@[<2>exec inst@\n@[%a@]@\n%a@]" Dom.pp state Llair.Inst.pp inst] ; + [%Trace.info "@\n@[%a@]@\n%a" Dom.pp state Llair.Inst.pp inst] ; Report.step_inst block inst ; Dom.exec_inst inst state |> function diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml index 39a0747d8..e50c63fce 100644 --- a/sledge/src/domain_used_globals.ml +++ b/sledge/src/domain_used_globals.ml @@ -15,7 +15,7 @@ let empty = Llair.Global.Set.empty let init globals = [%Trace.info - "pgm globals: {%a}" (IArray.pp ", " Llair.GlobalDefn.pp) globals] ; + " globals: {%a}" (IArray.pp ", " Llair.GlobalDefn.pp) globals] ; empty let join l r = Some (Llair.Global.Set.union l r) diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index f68b4197a..187dbc475 100644 --- a/sledge/src/fol/context.ml +++ b/sledge/src/fol/context.ml @@ -132,8 +132,7 @@ end = struct ( noninterp_with_solvable_var_in xs e || noninterp_with_solvable_var_in xs f ) $> fun b -> - [%Trace.info - "is_valid_eq %a%a=%a = %b" Var.Set.pp_xs xs Trm.pp e Trm.pp f b] + [%Trace.info " %a%a=%a = %b" Var.Set.pp_xs xs Trm.pp e Trm.pp f b] (** Partition ∃xs. σ into equivalent ∃xs. τ ∧ ∃ks. ν where ks and ν are maximal where ∃ks. ν is universally valid, xs ⊇ ks and @@ -423,7 +422,7 @@ let pre_invariant x = ) ) ) with exc -> let bt = Printexc.get_raw_backtrace () in - [%Trace.info "%a" pp_raw x] ; + [%Trace.info " %a" pp_raw x] ; Printexc.raise_with_backtrace exc bt let invariant x = diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index ade2b032e..b36a5c926 100644 --- a/sledge/src/llair/llair.ml +++ b/sledge/src/llair/llair.ml @@ -654,7 +654,7 @@ module Func = struct | _ -> assert false with exc -> let bt = Printexc.get_raw_backtrace () in - [%Trace.info "%a" pp func] ; + [%Trace.info " %a" pp func] ; Printexc.raise_with_backtrace exc bt let find name functions = diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index 2ea1386db..4d367df3f 100644 --- a/sledge/src/sh.ml +++ b/sledge/src/sh.ml @@ -296,7 +296,7 @@ let rec invariant q = invariant sjn ) ) with exc -> let bt = Printexc.get_raw_backtrace () in - [%Trace.info "%a" pp_raw q] ; + [%Trace.info " %a" pp_raw q] ; Printexc.raise_with_backtrace exc bt (** Query *) diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml index 86f27c545..ad24b0d67 100644 --- a/sledge/src/solver.ml +++ b/sledge/src/solver.ml @@ -83,7 +83,7 @@ end = struct assert (Var.Set.disjoint us xs) ; assert (Var.Set.subset zs ~of_:(Var.Set.union us xs)) with exc -> - [%Trace.info "%a" pp g] ; + [%Trace.info " %a" pp g] ; raise exc let with_ ?us ?com ?min ?xs ?sub ?zs ?pgs g = @@ -147,7 +147,7 @@ let excise (k : Trace.pf -> _) = [%Trace.infok k] let trace (k : Trace.pf -> _) = [%Trace.infok k] let excise_exists goal = - trace (fun {pf} -> pf "@[<2>excise_exists@ %a@]" pp goal) ; + trace (fun {pf} -> pf "excise_exists:@ %a" pp goal) ; if Var.Set.is_empty goal.xs then goal else let solutions_for_xs = @@ -170,7 +170,7 @@ let excise_exists goal = if Context.Subst.is_empty witnesses then goal else ( excise (fun {pf} -> - pf "@[<2>excise_exists @[%a%a@]@]" Var.Set.pp_xs removed + pf "excise_exists: @[%a%a@]" Var.Set.pp_xs removed Context.Subst.pp witnesses ) ; let us = Var.Set.union goal.us removed in let xs = Var.Set.diff goal.xs removed in @@ -192,8 +192,8 @@ let excise_exists goal = *) let excise_seg_same ({com; min; sub} as goal) msg ssg = excise (fun {pf} -> - pf "@[excise_seg_same@ %a@ \\- %a@]" (Sh.pp_seg_norm sub.ctx) - msg (Sh.pp_seg_norm sub.ctx) ssg ) ; + pf "excise_seg_same:@ %a@ \\- %a" (Sh.pp_seg_norm sub.ctx) msg + (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.bas= b; len= m; cnt= a} = msg in let {Sh.bas= b'; len= m'; cnt= a'} = ssg in let com = Sh.star (Sh.seg msg) com in @@ -221,8 +221,8 @@ let excise_seg_same ({com; min; sub} as goal) msg ssg = let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n = excise (fun {pf} -> - pf "@[excise_seg_sub_prefix@ %a@ \\- %a@]" - (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; + pf "excise_seg_sub_prefix:@ %a@ \\- %a" (Sh.pp_seg_norm sub.ctx) msg + (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in let {Sh.bas= b'; len= m'; siz= n; cnt= a'} = ssg in let o_n = Term.integer o_n in @@ -261,8 +261,8 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o = excise (fun {pf} -> - pf "@[excise_seg_min_prefix@ %a@ \\- %a@]" - (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; + pf "excise_seg_min_prefix:@ %a@ \\- %a" (Sh.pp_seg_norm sub.ctx) msg + (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.bas= b; len= m; siz= o; cnt= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in let n_o = Term.integer n_o in @@ -297,8 +297,8 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k = excise (fun {pf} -> - pf "@[excise_seg_sub_suffix@ %a@ \\- %a@]" - (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; + pf "excise_seg_sub_suffix:@ %a@ \\- %a" (Sh.pp_seg_norm sub.ctx) msg + (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in let l_k = Term.integer l_k in @@ -339,8 +339,8 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k ko_ln = excise (fun {pf} -> - pf "@[excise_seg_sub_infix@ %a@ \\- %a@]" - (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; + pf "excise_seg_sub_infix:@ %a@ \\- %a" (Sh.pp_seg_norm sub.ctx) msg + (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in let l_k = Term.integer l_k in @@ -386,8 +386,8 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k ko_l ln_ko = excise (fun {pf} -> - pf "@[excise_seg_min_skew@ %a@ \\- %a@]" - (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; + pf "excise_seg_min_skew:@ %a@ \\- %a" (Sh.pp_seg_norm sub.ctx) msg + (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in let l_k = Term.integer l_k in @@ -436,8 +436,8 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l = excise (fun {pf} -> - pf "@[excise_seg_min_suffix@ %a@ \\- %a@]" - (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; + pf "excise_seg_min_suffix:@ %a@ \\- %a" (Sh.pp_seg_norm sub.ctx) msg + (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.bas= b; len= m; siz= o; cnt= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in let k_l = Term.integer k_l in @@ -473,8 +473,8 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l ln_ko = excise (fun {pf} -> - pf "@[excise_seg_min_infix@ %a@ \\- %a@]" - (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; + pf "excise_seg_min_infix:@ %a@ \\- %a" (Sh.pp_seg_norm sub.ctx) msg + (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in let k_l = Term.integer k_l in @@ -514,8 +514,8 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l ln_k ko_ln = excise (fun {pf} -> - pf "@[excise_seg_sub_skew@ %a@ \\- %a@]" - (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; + pf "excise_seg_sub_skew:@ %a@ \\- %a" (Sh.pp_seg_norm sub.ctx) msg + (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in let k_l = Term.integer k_l in @@ -549,7 +549,7 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l (* C ❮ k-[b;m)->⟨o,α⟩ * M ⊢ ∃xs. l-[b';m')->⟨n,α'⟩ * S ❯ R *) let excise_seg ({sub} as goal) msg ssg = trace (fun {pf} -> - pf "@[<2>excise_seg@ %a@ |- %a@]" (Sh.pp_seg_norm sub.ctx) msg + pf "excise_seg:@ %a@ |- %a" (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.loc= k; bas= b; len= m; siz= o} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n} = ssg in @@ -627,7 +627,7 @@ let excise_seg ({sub} as goal) msg ssg = | Zero | Pos -> None ) ) let excise_heap ({min; sub} as goal) = - trace (fun {pf} -> pf "@[<2>excise_heap@ %a@]" pp goal) ; + trace (fun {pf} -> pf "excise_heap:@ %a" pp goal) ; match List.find_map sub.heap ~f:(fun ssg -> List.find_map min.heap ~f:(fun msg -> excise_seg goal msg ssg) ) @@ -638,7 +638,7 @@ let excise_heap ({min; sub} as goal) = let pure_entails x q = Sh.is_empty q && Context.implies x (Sh.pure_approx q) let rec excise ({min; xs; sub; zs; pgs} as goal) = - [%Trace.info "@[<2>excise@ %a@]" pp goal] ; + [%Trace.info "@ %a" pp goal] ; Report.step_solver () ; if Sh.is_unsat min then Some (Sh.false_ (Var.Set.diff sub.us zs)) else if pure_entails min.ctx sub then @@ -646,33 +646,36 @@ let rec excise ({min; xs; sub; zs; pgs} as goal) = else if Sh.is_unsat sub then None else if pgs then goal |> with_ ~pgs:false |> excise_exists |> excise_heap >>= excise - else None $> fun _ -> [%Trace.info "@[<2>excise fail@ %a@]" pp goal] + else None $> fun _ -> [%Trace.info " fail@ %a" pp goal] let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option = fun minuend xs subtrahend -> let dnf_minuend = Sh.dnf minuend in let dnf_subtrahend = Sh.dnf subtrahend in - Iter.fold_opt + let excise_subtrahend us min zs sub = + [%trace] + ~call:(fun {pf} -> pf "@ %a" Sh.pp sub) + ~retn:(fun {pf} -> pf "%a" (Option.pp "%a" Sh.pp)) + @@ fun () -> + let com = Sh.emp in + let sub = Sh.and_ctx min.Sh.ctx (Sh.extend_us us sub) in + excise (goal ~us ~com ~min ~xs ~sub ~zs ~pgs:true) + in + let from_minuend minuend remainders = + [%trace] + ~call:(fun {pf} -> pf "@ %a" Sh.pp minuend) + ~retn:(fun {pf} -> pf "%a" (Option.pp "%a" Sh.pp)) + @@ fun () -> + let zs, min = Sh.bind_exists minuend ~wrt:xs in + let us = min.us in + let+ remainder = + List.find_map ~f:(excise_subtrahend us min zs) dnf_subtrahend + in + Sh.or_ remainders remainder + in + Iter.fold_opt ~f:from_minuend (Iter.of_list dnf_minuend) (Sh.false_ (Var.Set.union minuend.us xs)) - ~f:(fun minuend remainders -> - [%trace] - ~call:(fun {pf} -> pf "@ @[<2>minuend@ %a@]" Sh.pp minuend) - ~retn:(fun {pf} -> pf "%a" (Option.pp "%a" Sh.pp)) - @@ fun () -> - let zs, min = Sh.bind_exists minuend ~wrt:xs in - let us = min.us in - let com = Sh.emp in - let+ remainder = - List.find_map dnf_subtrahend ~f:(fun sub -> - [%trace] - ~call:(fun {pf} -> pf "@ @[<2>subtrahend@ %a@]" Sh.pp sub) - ~retn:(fun {pf} -> pf "%a" (Option.pp "%a" Sh.pp)) - @@ fun () -> - let sub = Sh.and_ctx min.ctx (Sh.extend_us us sub) in - excise (goal ~us ~com ~min ~xs ~sub ~zs ~pgs:true) ) - in - Sh.or_ remainders remainder ) let query_count = ref (-1) diff --git a/sledge/src/test/solver_test.ml b/sledge/src/test/solver_test.ml index 1ee764944..1d6998769 100644 --- a/sledge/src/test/solver_test.ml +++ b/sledge/src/test/solver_test.ml @@ -59,22 +59,22 @@ let%test_module _ = check_frame Sh.emp [] Sh.emp ; [%expect {| - ( infer_frame: 0 emp \- emp - ) infer_frame: emp |}] + ( Solver.infer_frame: 0 emp \- emp + ) Solver.infer_frame: emp |}] let%expect_test _ = check_frame (Sh.false_ Var.Set.empty) [] Sh.emp ; [%expect {| - ( infer_frame: 1 false \- emp - ) infer_frame: false |}] + ( Solver.infer_frame: 1 false \- emp + ) Solver.infer_frame: false |}] let%expect_test _ = check_frame Sh.emp [n_; m_] (Sh.and_ (Formula.eq m n) Sh.emp) ; [%expect {| - ( infer_frame: 2 emp \- ∃ %m_8, %n_9 . %m_8 = %n_9 ∧ emp - ) infer_frame: %m_8 = %n_9 ∧ emp |}] + ( Solver.infer_frame: 2 emp \- ∃ %m_8, %n_9 . %m_8 = %n_9 ∧ emp + ) Solver.infer_frame: %m_8 = %n_9 ∧ emp |}] let%expect_test _ = check_frame @@ -82,8 +82,9 @@ let%test_module _ = [] Sh.emp ; [%expect {| - ( infer_frame: 3 %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ \- emp - ) infer_frame: %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ |}] + ( Solver.infer_frame: 3 + %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ \- emp + ) Solver.infer_frame: %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ |}] let%expect_test _ = check_frame @@ -92,10 +93,10 @@ let%test_module _ = (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a}) ; [%expect {| - ( infer_frame: 4 + ( Solver.infer_frame: 4 %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ \- %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ - ) infer_frame: emp |}] + ) Solver.infer_frame: emp |}] let%expect_test _ = let common = Sh.seg {loc= l2; bas= b; len= !10; siz= !10; cnt= a2} in @@ -110,11 +111,11 @@ let%test_module _ = infer_frame minued [n_; m_] subtrahend ; [%expect {| - ( infer_frame: 5 + ( Solver.infer_frame: 5 %l_6 -[ %b_4, 10 )-> ⟨10,%a_1⟩ * %l_7 -[ %b_4, 10 )-> ⟨10,%a_2⟩ \- ∃ %m_8, %n_9 . ∃ %m_10 . %m_8 = %n_9 ∧ %l_7 -[ %b_4, 10 )-> ⟨10,%a_2⟩ - ) infer_frame: + ) Solver.infer_frame: ∃ %m_10 . %m_8 = %n_9 ∧ %l_6 -[ %b_4, 10 )-> ⟨10,%a_1⟩ |}] let%expect_test _ = @@ -126,11 +127,11 @@ let%test_module _ = (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a}) ; [%expect {| - ( infer_frame: 6 + ( Solver.infer_frame: 6 %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ * %l_7 -[ %b_4, %m_8 )-> ⟨%n_9,%a_2⟩ \- %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ - ) infer_frame: %l_7 -[ %b_4, %m_8 )-> ⟨%n_9,%a_2⟩ |}] + ) Solver.infer_frame: %l_7 -[ %b_4, %m_8 )-> ⟨%n_9,%a_2⟩ |}] let%expect_test _ = check_frame @@ -141,9 +142,9 @@ let%test_module _ = (Sh.seg {loc= l; bas= l; len= !16; siz= !16; cnt= a3}) ; [%expect {| - ( infer_frame: 7 + ( Solver.infer_frame: 7 %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩ \- ∃ %a_3 . %l_6 -[)-> ⟨16,%a_3⟩ - ) infer_frame: (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}] + ) Solver.infer_frame: (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}] let%expect_test _ = check_frame @@ -154,11 +155,12 @@ let%test_module _ = (Sh.seg {loc= l; bas= l; len= m; siz= !16; cnt= a3}) ; [%expect {| - ( infer_frame: 8 + ( Solver.infer_frame: 8 %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩ \- ∃ %a_3, %m_8 . %l_6 -[ %l_6, %m_8 )-> ⟨16,%a_3⟩ - ) infer_frame: 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}] + ) Solver.infer_frame: + 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}] let%expect_test _ = check_frame @@ -169,11 +171,12 @@ let%test_module _ = (Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a3}) ; [%expect {| - ( infer_frame: 9 + ( Solver.infer_frame: 9 %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩ \- ∃ %a_3, %m_8 . %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_3⟩ - ) infer_frame: 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}] + ) Solver.infer_frame: + 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}] let%expect_test _ = check_frame @@ -186,11 +189,11 @@ let%test_module _ = (Sh.seg {loc= k; bas= k; len= m; siz= n; cnt= a2})) ; [%expect {| - ( infer_frame: 10 + ( Solver.infer_frame: 10 %k_5 -[ %k_5, 16 )-> ⟨32,%a_1⟩ * %l_6 -[)-> ⟨8,16⟩ \- ∃ %a_2, %m_8, %n_9 . %k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨8,%n_9⟩ - ) infer_frame: + ) Solver.infer_frame: ∃ %a0_10, %a1_11 . %a_2 = %a0_10 ∧ 16 = %m_8 = %n_9 @@ -208,11 +211,11 @@ let%test_module _ = (Sh.seg {loc= l; bas= l; len= !8; siz= !8; cnt= n})) ; [%expect {| - ( infer_frame: 11 + ( Solver.infer_frame: 11 %k_5 -[ %k_5, 16 )-> ⟨32,%a_1⟩ * %l_6 -[)-> ⟨8,16⟩ \- ∃ %a_2, %m_8, %n_9 . %k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨8,%n_9⟩ - ) infer_frame: + ) Solver.infer_frame: ∃ %a0_10, %a1_11 . %a_2 = %a0_10 ∧ 16 = %m_8 = %n_9 @@ -234,7 +237,7 @@ let%test_module _ = (Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a}) ; [%expect {| - ( infer_frame: 12 + ( Solver.infer_frame: 12 %l_6 -[ %l_6, 16 )-> ⟨8×%n_9,%a_2⟩^⟨(16 + -8×%n_9),%a_3⟩ * ( ( 1 = %n_9 ∧ emp) ∨ ( 0 = %n_9 ∧ emp) @@ -242,7 +245,7 @@ let%test_module _ = ) \- ∃ %a_1, %m_8 . %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩ - ) infer_frame: + ) Solver.infer_frame: ( ( 1 = %n_9 ∧ 16 = %m_8 ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1 ∧ emp) ∨ ( %a_1 = %a_2 ∧ 2 = %n_9 @@ -259,12 +262,12 @@ let%test_module _ = (Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a}) ; [%expect {| - ( infer_frame: 13 + ( Solver.infer_frame: 13 (2 ≥ %n_9) ∧ %l_6 -[ %l_6, 16 )-> ⟨8×%n_9,%a_2⟩^⟨(16 + -8×%n_9),%a_3⟩ \- ∃ %a_1, %m_8 . %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩ - ) infer_frame: |}] + ) Solver.infer_frame: |}] (* Incompleteness: cannot witness existentials to satisfy non-equality pure constraints *) @@ -276,7 +279,7 @@ let%test_module _ = infer_frame minuend [m_] subtrahend ; [%expect {| - ( infer_frame: 14 + ( Solver.infer_frame: 14 emp \- ∃ %m_8 . %a_1 = %m_8 ∧ (0 ≠ %a_1) ∧ emp - ) infer_frame: |}] + ) Solver.infer_frame: |}] end )