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

[sledge] Make tracing more explicit by including module names

Browse Source 
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
master
Josh Berdine 4 years ago committed by Facebook GitHub Bot
parent 5408be4a3a
commit 3e5b4c8183
9 changed files with 142 additions and 124 deletions
Show Stats Download Patch File Download Diff File

2
sledge/cli/frontend.ml
Unescape View File

@ -1501,7 +1501,7 @@ let xlate_block : pop_thunk -> x -> Llvm.llbasicblock -> Llair.block list =
let report_undefined func name = let report_undefined func name =
if Option.is_some (Llvm.use_begin func) then 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 xlate_function_decl x llfunc typ k =
let loc = find_loc llfunc in let loc = find_loc llfunc in

26
sledge/ppx_trace/trace/trace.ml
Unescape View File

@ -191,25 +191,33 @@ let fprintf mod_fun_name fs fmt =
let printf mod_fun_name fmt = fprintf mod_fun_name fs fmt let printf mod_fun_name fmt = fprintf mod_fun_name fs fmt
let info mod_fun_name fmt = let info mod_fun_name fmt =
if enabled mod_fun_name then ( if not (enabled mod_fun_name) then Format.ifprintf fs fmt
Format.fprintf fs "@\n@[<2>| " ; else
Format.kfprintf (fun fs -> Format.fprintf fs "@]") fs fmt ) let mod_name, fun_name = split_mod_fun_name mod_fun_name in
else Format.ifprintf fs fmt 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 = let incf mod_fun_name fmt =
if not (enabled mod_fun_name) then Format.ifprintf fs fmt if not (enabled mod_fun_name) then Format.ifprintf fs fmt
else else
let _, fun_name = split_mod_fun_name mod_fun_name in let mod_name, fun_name = split_mod_fun_name mod_fun_name in
Format.fprintf fs "@\n@[<2>@[<hv 2>( %s:" fun_name ; Format.fprintf fs "@\n@[<2>@[<hv 2>( %s.%s:" mod_name fun_name ;
Format.kfprintf (fun fs -> Format.fprintf fs "@]") fs fmt Format.kfprintf (fun fs -> Format.fprintf fs "@]") fs fmt
let decf mod_fun_name fmt = let decf mod_fun_name fmt =
if not (enabled mod_fun_name) then Format.ifprintf fs fmt if not (enabled mod_fun_name) then Format.ifprintf fs fmt
else else
let _, fun_name = split_mod_fun_name mod_fun_name in let mod_name, fun_name = split_mod_fun_name mod_fun_name in
Format.fprintf fs "@]@\n@[<2>) %s:@ " fun_name ; Format.fprintf fs "@]@\n@[<2>) %s.%s:@ " mod_name fun_name ;
Format.kfprintf (fun fs -> Format.fprintf fs "@]") fs fmt Format.kfprintf (fun fs -> Format.fprintf fs "@]") fs fmt
let call mod_fun_name k = k {pf= (fun fmt -> incf mod_fun_name fmt)} let call mod_fun_name k = k {pf= (fun fmt -> incf mod_fun_name fmt)}

73
sledge/src/control.ml
Unescape View File

@ -259,6 +259,37 @@ module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct
Some (top, elts, {queue; removed}) Some (top, elts, {queue; removed})
end 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 t = PrioQueue.t
type x = Depths.t -> t -> 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 edge = {Edge.dst= curr; src= prev; stk} in
let depth = Option.value (Depths.find edge depths) ~default:0 in let depth = Option.value (Depths.find edge depths) ~default:0 in
let depth = if retreating then depth + 1 else depth in let depth = if retreating then depth + 1 else depth in
if depth <= Opts.bound then ( if depth <= Opts.bound then enqueue depth edge state depths queue
[%Trace.info else prune depth edge queue
"@[<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 )
let init state curr = let init state curr =
add ~retreating:false Stack.empty state curr Depths.empty add ~retreating:false Stack.empty state curr Depths.empty
(PrioQueue.create ()) (PrioQueue.create ())
let rec run ~f queue = let rec run ~f queue =
match PrioQueue.pop queue with match dequeue queue with
| Some ({depth; edge; state; depths}, elts, queue) -> | Some (edge, state, depths, 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
run ~f (f edge.stk state edge.dst depths queue) run ~f (f edge.stk state edge.dst depths queue)
| None -> | None -> ()
[%Trace.info "queue empty"] ;
()
end end
let exec_jump stk state block Llair.{dst; retreating} = 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 | Some state -> exec_jump stk state block jump
| None -> | None ->
[%Trace.info [%Trace.info
"@[<2>infeasible assume %a@\n@[%a@]@]" Llair.Exp.pp cond Dom.pp " infeasible %a@\n@[%a@]" Llair.Exp.pp cond Dom.pp state] ;
state] ;
Work.skip Work.skip
let exec_term : Llair.program -> Stack.t -> Dom.t -> Llair.block -> Work.x let exec_term : Llair.program -> Stack.t -> Dom.t -> Llair.block -> Work.x
= =
fun pgm stk state block -> fun pgm stk state block ->
[%Trace.info [%Trace.info "@\n@[%a@]@\n%a" Dom.pp state Llair.Term.pp block.term] ;
"@[<2>exec term@\n@[%a@]@\n%a@]" Dom.pp state Llair.Term.pp block.term] ;
Report.step_term block ; Report.step_term block ;
match block.term with match block.term with
| Switch {key; tbl; els} -> | 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, Dom.t * Llair.inst) result = -> (Dom.t, Dom.t * Llair.inst) result =
fun block inst state -> fun block inst state ->
[%Trace.info [%Trace.info "@\n@[%a@]@\n%a" Dom.pp state Llair.Inst.pp inst] ;
"@[<2>exec inst@\n@[%a@]@\n%a@]" Dom.pp state Llair.Inst.pp inst] ;
Report.step_inst block inst ; Report.step_inst block inst ;
Dom.exec_inst inst state Dom.exec_inst inst state
|> function |> function

2
sledge/src/domain_used_globals.ml
Unescape View File

@ -15,7 +15,7 @@ let empty = Llair.Global.Set.empty
let init globals = let init globals =
[%Trace.info [%Trace.info
"pgm globals: {%a}" (IArray.pp ", " Llair.GlobalDefn.pp) globals] ; " globals: {%a}" (IArray.pp ", " Llair.GlobalDefn.pp) globals] ;
empty empty
let join l r = Some (Llair.Global.Set.union l r) let join l r = Some (Llair.Global.Set.union l r)

5
sledge/src/fol/context.ml
Unescape View File

@ -132,8 +132,7 @@ end = struct
( noninterp_with_solvable_var_in xs e ( noninterp_with_solvable_var_in xs e
|| noninterp_with_solvable_var_in xs f ) || noninterp_with_solvable_var_in xs f )
$> fun b -> $> fun b ->
[%Trace.info [%Trace.info " %a%a=%a = %b" Var.Set.pp_xs xs Trm.pp e Trm.pp f b]
"is_valid_eq %a%a=%a = %b" Var.Set.pp_xs xs Trm.pp e Trm.pp f b]
(** Partition ∃xs. σ into equivalent ∃xs. τ ∧ ∃ks. ν where ks (** Partition ∃xs. σ into equivalent ∃xs. τ ∧ ∃ks. ν where ks
and ν are maximal where ∃ks. ν is universally valid, xs ⊇ ks and and ν are maximal where ∃ks. ν is universally valid, xs ⊇ ks and
@ -423,7 +422,7 @@ let pre_invariant x =
) ) ) ) ) )
with exc -> with exc ->
let bt = Printexc.get_raw_backtrace () in 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 Printexc.raise_with_backtrace exc bt
let invariant x = let invariant x =

2
sledge/src/llair/llair.ml
Unescape View File

@ -654,7 +654,7 @@ module Func = struct
| _ -> assert false | _ -> assert false
with exc -> with exc ->
let bt = Printexc.get_raw_backtrace () in let bt = Printexc.get_raw_backtrace () in
[%Trace.info "%a" pp func] ; [%Trace.info " %a" pp func] ;
Printexc.raise_with_backtrace exc bt Printexc.raise_with_backtrace exc bt
let find name functions = let find name functions =

2
sledge/src/sh.ml
Unescape View File

@ -296,7 +296,7 @@ let rec invariant q =
invariant sjn ) ) invariant sjn ) )
with exc -> with exc ->
let bt = Printexc.get_raw_backtrace () in 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 Printexc.raise_with_backtrace exc bt
(** Query *) (** Query *)

91
sledge/src/solver.ml
Unescape View File

@ -83,7 +83,7 @@ end = struct
assert (Var.Set.disjoint us xs) ; assert (Var.Set.disjoint us xs) ;
assert (Var.Set.subset zs ~of_:(Var.Set.union us xs)) assert (Var.Set.subset zs ~of_:(Var.Set.union us xs))
with exc -> with exc ->
[%Trace.info "%a" pp g] ; [%Trace.info " %a" pp g] ;
raise exc raise exc
let with_ ?us ?com ?min ?xs ?sub ?zs ?pgs g = 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 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 "excise_exists:@ %a" pp goal) ;
if Var.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 =
@ -170,7 +170,7 @@ let excise_exists goal =
if Context.Subst.is_empty witnesses then goal if Context.Subst.is_empty witnesses then goal
else ( else (
excise (fun {pf} -> 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 ) ; Context.Subst.pp witnesses ) ;
let us = Var.Set.union goal.us removed in let us = Var.Set.union goal.us removed in
let xs = Var.Set.diff goal.xs 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 = let excise_seg_same ({com; min; sub} as goal) msg ssg =
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_same@ %a@ \\- %a@]" (Sh.pp_seg_norm sub.ctx) pf "excise_seg_same:@ %a@ \\- %a" (Sh.pp_seg_norm sub.ctx) msg
msg (Sh.pp_seg_norm sub.ctx) ssg ) ; (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} = msg in
let {Sh.bas= b'; len= m'; cnt= a'} = ssg in let {Sh.bas= b'; len= m'; cnt= a'} = ssg in
let com = Sh.star (Sh.seg msg) com 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 let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
= =
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_sub_prefix@ %a@ \\- %a@]" pf "excise_seg_sub_prefix:@ %a@ \\- %a" (Sh.pp_seg_norm sub.ctx) msg
(Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in 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 {Sh.bas= b'; len= m'; siz= n; cnt= a'} = ssg in
let o_n = Term.integer o_n 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 let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
= =
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_min_prefix@ %a@ \\- %a@]" pf "excise_seg_min_prefix:@ %a@ \\- %a" (Sh.pp_seg_norm sub.ctx) msg
(Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.bas= b; len= m; siz= o; cnt= a} = msg in 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 {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in
let n_o = Term.integer n_o 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 let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
= =
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_sub_suffix@ %a@ \\- %a@]" pf "excise_seg_sub_suffix:@ %a@ \\- %a" (Sh.pp_seg_norm sub.ctx) msg
(Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in 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 {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in
let l_k = Term.integer l_k 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 let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
ko_ln = ko_ln =
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_sub_infix@ %a@ \\- %a@]" pf "excise_seg_sub_infix:@ %a@ \\- %a" (Sh.pp_seg_norm sub.ctx) msg
(Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in 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 {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in
let l_k = Term.integer l_k 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 let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
ko_l ln_ko = ko_l ln_ko =
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_min_skew@ %a@ \\- %a@]" pf "excise_seg_min_skew:@ %a@ \\- %a" (Sh.pp_seg_norm sub.ctx) msg
(Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in 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 {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in
let l_k = Term.integer l_k 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 let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
= =
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_min_suffix@ %a@ \\- %a@]" pf "excise_seg_min_suffix:@ %a@ \\- %a" (Sh.pp_seg_norm sub.ctx) msg
(Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.bas= b; len= m; siz= o; cnt= a} = msg in 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 {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in
let k_l = Term.integer k_l 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 let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
ln_ko = ln_ko =
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_min_infix@ %a@ \\- %a@]" pf "excise_seg_min_infix:@ %a@ \\- %a" (Sh.pp_seg_norm sub.ctx) msg
(Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in 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 {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in
let k_l = Term.integer k_l 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 let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
ln_k ko_ln = ln_k ko_ln =
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_sub_skew@ %a@ \\- %a@]" pf "excise_seg_sub_skew:@ %a@ \\- %a" (Sh.pp_seg_norm sub.ctx) msg
(Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o; cnt= a} = msg in 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 {Sh.loc= l; bas= b'; len= m'; siz= n; cnt= a'} = ssg in
let k_l = Term.integer k_l 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 *) (* C ❮ k-[b;m)->⟨o,α⟩ * M ⊢ ∃xs. l-[b';m')->⟨n,α'⟩ * S ❯ R *)
let excise_seg ({sub} as goal) msg ssg = let excise_seg ({sub} as goal) msg ssg =
trace (fun {pf} -> 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 ) ; (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o} = msg in let {Sh.loc= k; bas= b; len= m; siz= o} = msg in
let {Sh.loc= l; bas= b'; len= m'; siz= n} = ssg 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 ) ) | Zero | Pos -> None ) )
let excise_heap ({min; sub} as goal) = 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 match
List.find_map sub.heap ~f:(fun ssg -> List.find_map sub.heap ~f:(fun ssg ->
List.find_map min.heap ~f:(fun msg -> excise_seg goal msg 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 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) = 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 () ; Report.step_solver () ;
if Sh.is_unsat min then Some (Sh.false_ (Var.Set.diff sub.us zs)) if Sh.is_unsat min then Some (Sh.false_ (Var.Set.diff sub.us zs))
else if pure_entails min.ctx sub then 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 Sh.is_unsat sub then None
else if pgs then else if pgs then
goal |> with_ ~pgs:false |> excise_exists |> excise_heap >>= excise 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 = let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
fun minuend xs subtrahend -> fun minuend xs subtrahend ->
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
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) (Iter.of_list dnf_minuend)
(Sh.false_ (Var.Set.union minuend.us xs)) (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) let query_count = ref (-1)

63
sledge/src/test/solver_test.ml
Unescape View File

@ -59,22 +59,22 @@ let%test_module _ =
check_frame Sh.emp [] Sh.emp ; check_frame Sh.emp [] Sh.emp ;
[%expect [%expect
{| {|
( infer_frame: 0 emp \- emp ( Solver.infer_frame: 0 emp \- emp
) infer_frame: emp |}] ) Solver.infer_frame: emp |}]
let%expect_test _ = let%expect_test _ =
check_frame (Sh.false_ Var.Set.empty) [] Sh.emp ; check_frame (Sh.false_ Var.Set.empty) [] Sh.emp ;
[%expect [%expect
{| {|
( infer_frame: 1 false \- emp ( Solver.infer_frame: 1 false \- emp
) infer_frame: false |}] ) Solver.infer_frame: false |}]
let%expect_test _ = let%expect_test _ =
check_frame Sh.emp [n_; m_] (Sh.and_ (Formula.eq m n) Sh.emp) ; check_frame Sh.emp [n_; m_] (Sh.and_ (Formula.eq m n) Sh.emp) ;
[%expect [%expect
{| {|
( infer_frame: 2 emp \- ∃ %m_8, %n_9 . %m_8 = %n_9 ∧ emp ( Solver.infer_frame: 2 emp \- ∃ %m_8, %n_9 . %m_8 = %n_9 ∧ emp
) infer_frame: %m_8 = %n_9 ∧ emp |}] ) Solver.infer_frame: %m_8 = %n_9 ∧ emp |}]
let%expect_test _ = let%expect_test _ =
check_frame check_frame
@ -82,8 +82,9 @@ let%test_module _ =
[] Sh.emp ; [] Sh.emp ;
[%expect [%expect
{| {|
( infer_frame: 3 %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ \- emp ( Solver.infer_frame: 3
) infer_frame: %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ |}] %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 _ = let%expect_test _ =
check_frame check_frame
@ -92,10 +93,10 @@ let%test_module _ =
(Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a}) ; (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a}) ;
[%expect [%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⟩
\- %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%expect_test _ =
let common = Sh.seg {loc= l2; bas= b; len= !10; siz= !10; cnt= a2} in 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 ; infer_frame minued [n_; m_] subtrahend ;
[%expect [%expect
{| {|
( infer_frame: 5 ( Solver.infer_frame: 5
%l_6 -[ %b_4, 10 )-> ⟨10,%a_1⟩ * %l_7 -[ %b_4, 10 )-> ⟨10,%a_2⟩ %l_6 -[ %b_4, 10 )-> ⟨10,%a_1⟩ * %l_7 -[ %b_4, 10 )-> ⟨10,%a_2⟩
\- ∃ %m_8, %n_9 . \- ∃ %m_8, %n_9 .
∃ %m_10 . %m_8 = %n_9 ∧ %l_7 -[ %b_4, 10 )-> ⟨10,%a_2⟩ ∃ %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⟩ |}] ∃ %m_10 . %m_8 = %n_9 ∧ %l_6 -[ %b_4, 10 )-> ⟨10,%a_1⟩ |}]
let%expect_test _ = let%expect_test _ =
@ -126,11 +127,11 @@ let%test_module _ =
(Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a}) ; (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a}) ;
[%expect [%expect
{| {|
( infer_frame: 6 ( Solver.infer_frame: 6
%l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩
* %l_7 -[ %b_4, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_7 -[ %b_4, %m_8 )-> ⟨%n_9,%a_2⟩
\- %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ \- %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 _ = let%expect_test _ =
check_frame check_frame
@ -141,9 +142,9 @@ let%test_module _ =
(Sh.seg {loc= l; bas= l; len= !16; siz= !16; cnt= a3}) ; (Sh.seg {loc= l; bas= l; len= !16; siz= !16; cnt= a3}) ;
[%expect [%expect
{| {|
( infer_frame: 7 ( Solver.infer_frame: 7
%l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩ \- ∃ %a_3 . %l_6 -[)-> ⟨16,%a_3⟩ %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 _ = let%expect_test _ =
check_frame check_frame
@ -154,11 +155,12 @@ let%test_module _ =
(Sh.seg {loc= l; bas= l; len= m; siz= !16; cnt= a3}) ; (Sh.seg {loc= l; bas= l; len= m; siz= !16; cnt= a3}) ;
[%expect [%expect
{| {|
( infer_frame: 8 ( Solver.infer_frame: 8
%l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩ %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩
\- ∃ %a_3, %m_8 . \- ∃ %a_3, %m_8 .
%l_6 -[ %l_6, %m_8 )-> ⟨16,%a_3⟩ %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 _ = let%expect_test _ =
check_frame check_frame
@ -169,11 +171,12 @@ let%test_module _ =
(Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a3}) ; (Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a3}) ;
[%expect [%expect
{| {|
( infer_frame: 9 ( Solver.infer_frame: 9
%l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩ %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩
\- ∃ %a_3, %m_8 . \- ∃ %a_3, %m_8 .
%l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_3⟩ %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 _ = let%expect_test _ =
check_frame check_frame
@ -186,11 +189,11 @@ let%test_module _ =
(Sh.seg {loc= k; bas= k; len= m; siz= n; cnt= a2})) ; (Sh.seg {loc= k; bas= k; len= m; siz= n; cnt= a2})) ;
[%expect [%expect
{| {|
( infer_frame: 10 ( Solver.infer_frame: 10
%k_5 -[ %k_5, 16 )-> ⟨32,%a_1⟩ * %l_6 -[)-> ⟨8,16⟩ %k_5 -[ %k_5, 16 )-> ⟨32,%a_1⟩ * %l_6 -[)-> ⟨8,16⟩
\- ∃ %a_2, %m_8, %n_9 . \- ∃ %a_2, %m_8, %n_9 .
%k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨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 . ∃ %a0_10, %a1_11 .
%a_2 = %a0_10 %a_2 = %a0_10
∧ 16 = %m_8 = %n_9 ∧ 16 = %m_8 = %n_9
@ -208,11 +211,11 @@ let%test_module _ =
(Sh.seg {loc= l; bas= l; len= !8; siz= !8; cnt= n})) ; (Sh.seg {loc= l; bas= l; len= !8; siz= !8; cnt= n})) ;
[%expect [%expect
{| {|
( infer_frame: 11 ( Solver.infer_frame: 11
%k_5 -[ %k_5, 16 )-> ⟨32,%a_1⟩ * %l_6 -[)-> ⟨8,16⟩ %k_5 -[ %k_5, 16 )-> ⟨32,%a_1⟩ * %l_6 -[)-> ⟨8,16⟩
\- ∃ %a_2, %m_8, %n_9 . \- ∃ %a_2, %m_8, %n_9 .
%k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨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 . ∃ %a0_10, %a1_11 .
%a_2 = %a0_10 %a_2 = %a0_10
∧ 16 = %m_8 = %n_9 ∧ 16 = %m_8 = %n_9
@ -234,7 +237,7 @@ let%test_module _ =
(Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a}) ; (Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a}) ;
[%expect [%expect
{| {|
( infer_frame: 12 ( Solver.infer_frame: 12
%l_6 -[ %l_6, 16 )-> ⟨8×%n_9,%a_2⟩^⟨(16 + -8×%n_9),%a_3⟩ %l_6 -[ %l_6, 16 )-> ⟨8×%n_9,%a_2⟩^⟨(16 + -8×%n_9),%a_3⟩
* ( ( 1 = %n_9 ∧ emp) * ( ( 1 = %n_9 ∧ emp)
∨ ( 0 = %n_9 ∧ emp) ∨ ( 0 = %n_9 ∧ emp)
@ -242,7 +245,7 @@ let%test_module _ =
) )
\- ∃ %a_1, %m_8 . \- ∃ %a_1, %m_8 .
%l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩ %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) ( ( 1 = %n_9 ∧ 16 = %m_8 ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1 ∧ emp)
∨ ( %a_1 = %a_2 ∨ ( %a_1 = %a_2
∧ 2 = %n_9 ∧ 2 = %n_9
@ -259,12 +262,12 @@ let%test_module _ =
(Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a}) ; (Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a}) ;
[%expect [%expect
{| {|
( infer_frame: 13 ( Solver.infer_frame: 13
(2 ≥ %n_9) (2 ≥ %n_9)
∧ %l_6 -[ %l_6, 16 )-> ⟨8×%n_9,%a_2⟩^⟨(16 + -8×%n_9),%a_3⟩ ∧ %l_6 -[ %l_6, 16 )-> ⟨8×%n_9,%a_2⟩^⟨(16 + -8×%n_9),%a_3⟩
\- ∃ %a_1, %m_8 . \- ∃ %a_1, %m_8 .
%l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩ %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
) infer_frame: |}] ) Solver.infer_frame: |}]
(* Incompleteness: cannot witness existentials to satisfy non-equality (* Incompleteness: cannot witness existentials to satisfy non-equality
pure constraints *) pure constraints *)
@ -276,7 +279,7 @@ let%test_module _ =
infer_frame minuend [m_] subtrahend ; infer_frame minuend [m_] subtrahend ;
[%expect [%expect
{| {|
( infer_frame: 14 ( Solver.infer_frame: 14
emp \- ∃ %m_8 . %a_1 = %m_8 ∧ (0 ≠ %a_1) ∧ emp emp \- ∃ %m_8 . %a_1 = %m_8 ∧ (0 ≠ %a_1) ∧ emp
) infer_frame: |}] ) Solver.infer_frame: |}]
end ) end )

Write Preview
Loading…
Cancel
Save