Skip to content

GitLab

why3
why3
Commit 44f44412 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files
Options

Add a debug flag to get profiling data on the interpreter

parent 00755d2d
Hide whitespace changes
Inline Side-by-side
Showing with 132 additions and 56 deletions
examples/in_progress/multiprecision/lineardecision.mlw
View file @ 44f44412
......@@ -920,7 +920,7 @@ let rmul (a b:t)
= (from_int n1 *. from_int n2) /. (from_int d1 *. from_int d2)
= (from_int n1 /. from_int d1) *. (from_int n2 /. from_int d2)
= rinterp a y *. rinterp b y };
simp r
r
end
end
......@@ -945,6 +945,12 @@ let rinv (a:t)
| (n,d) -> if n = 0 || d = 0 then raise QError else (d,n)
end
let is_zero (a:t)
ensures { result <-> req a rzero }
= match a with
| (n,d) -> n = 0 && d <> 0
end
end
module LinearDecisionRational
......@@ -1251,8 +1257,8 @@ let madd (a b:t)
raises { Q.QError -> true }
= match a, b with
| (q1, e1), (q2, e2) ->
if Q.req q1 Q.rzero then b
else if Q.req q2 Q.rzero then a
if Q.is_zero q1 then b
else if Q.is_zero q2 then a
else if same_exp e1 e2
then begin
let q = Q.radd q1 q2 in
......@@ -1273,7 +1279,7 @@ let mmul (a b:t)
= match a, b with
| (q1,e1), (q2,e2) ->
let q = Q.rmul q1 q2 in
if Q.req q Q.rzero then mzero
if Q.is_zero q then mzero
else begin
let e = add_exp e1 e2 in
assert { forall y. minterp (q,e) y = minterp a y *. minterp b y
......@@ -1310,7 +1316,7 @@ let rec predicate pure_same_exp (e1 e2: exp)
let predicate meq (a b:t)
ensures { result -> forall y. minterp a y = minterp b y }
= match (a,b) with
| (q1,e1), (q2,e2) -> (Q.req q1 q2 && pure_same_exp e1 e2) || (Q.req q1 Q.rzero && Q.req q2 Q.rzero)
| (q1,e1), (q2,e2) -> (Q.req q1 q2 && pure_same_exp e1 e2) || (Q.is_zero q1 && Q.is_zero q2)
end
let minv (a:t)
......
examples/in_progress/multiprecision/lineardecision/why3session.xml
View file @ 44f44412
......@@ -150,10 +150,10 @@
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC sprod.2" expl="exceptional postcondition" proved="true">
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sprod.3" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
</transf>
</goal>
......@@ -1131,7 +1131,7 @@
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC linear_decision.10" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="21"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC linear_decision.11" expl="precondition" proved="true">
......@@ -1141,24 +1141,24 @@
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC linear_decision.13" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="21"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC linear_decision.14" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="39"/></proof>
</goal>
<goal name="VC linear_decision.15" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.16" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.17" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.18" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.19" expl="assertion" proved="true">
......@@ -1180,10 +1180,10 @@
<proof prover="0"><result status="valid" time="0.02" steps="26"/></proof>
</goal>
<goal name="VC linear_decision.25" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="49"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="49"/></proof>
</goal>
<goal name="VC linear_decision.26" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="31"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="31"/></proof>
</goal>
<goal name="VC linear_decision.27" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="28"/></proof>
......@@ -1195,10 +1195,10 @@
<proof prover="0"><result status="valid" time="0.02" steps="26"/></proof>
</goal>
<goal name="VC linear_decision.30" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="49"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="49"/></proof>
</goal>
<goal name="VC linear_decision.31" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="31"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="31"/></proof>
</goal>
<goal name="VC linear_decision.32" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="28"/></proof>
......@@ -1232,34 +1232,34 @@
<proof prover="0"><result status="valid" time="0.02" steps="44"/></proof>
</goal>
<goal name="VC linear_decision.42" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="23"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
<goal name="VC linear_decision.43" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="VC linear_decision.44" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="28"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="28"/></proof>
</goal>
<goal name="VC linear_decision.45" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="VC linear_decision.46" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.47" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
<goal name="VC linear_decision.48" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="VC linear_decision.49" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="28"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
<goal name="VC linear_decision.50" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="VC linear_decision.51" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.52" expl="exceptional postcondition" proved="true">
......@@ -1305,17 +1305,17 @@
<proof prover="0"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="VC linear_decision.66" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.67" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC linear_decision.68" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.68" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC linear_decision.69" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.70" expl="precondition" proved="true">
......@@ -1359,16 +1359,16 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.82" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.83" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.84" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.85" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
......@@ -1787,6 +1787,31 @@
</goal>
</transf>
</goal>
<goal name="VC is_zero" expl="VC for is_zero" proved="true">
<transf name="split_intros_goal_wp" proved="true" >
<goal name="VC is_zero.0" expl="postcondition" proved="true">
<transf name="split_intros_goal_wp" proved="true" >
<goal name="VC is_zero.0.0" expl="VC for is_zero" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC is_zero.0.0.0" expl="VC for is_zero" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="VC is_zero.0.0.0.0" expl="VC for is_zero" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC is_zero.0.1" expl="VC for is_zero" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="VC is_zero.1" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="LinearDecisionRational" proved="true">
<goal name="C.A.Assoc" proved="true">
......@@ -2508,43 +2533,43 @@
</goal>
<goal name="VC mmul" expl="VC for mmul" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC mmul.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC mmul.1" expl="assertion" proved="true">
<goal name="VC mmul.0" expl="assertion" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC mmul.1.0" expl="assertion" proved="true">
<goal name="VC mmul.0.0" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mmul.1.1" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="13"/></proof>
<goal name="VC mmul.0.1" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="10"/></proof>
</goal>
<goal name="VC mmul.1.2" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="12"/></proof>
<goal name="VC mmul.0.2" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="9"/></proof>
</goal>
<goal name="VC mmul.1.3" expl="VC for mmul" proved="true">
<goal name="VC mmul.0.3" expl="VC for mmul" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mmul.1.4" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="9"/></proof>
<goal name="VC mmul.0.4" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="8"/></proof>
</goal>
<goal name="VC mmul.1.5" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="12"/></proof>
<goal name="VC mmul.0.5" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="9"/></proof>
</goal>
<goal name="VC mmul.1.6" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="13"/></proof>
<goal name="VC mmul.0.6" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
</transf>
</goal>
<goal name="VC mmul.2" expl="postcondition" proved="true">
<goal name="VC mmul.1" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mmul.3" expl="exceptional postcondition" proved="true">
<goal name="VC mmul.2" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mmul.4" expl="exceptional postcondition" proved="true">
<goal name="VC mmul.3" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mmul.0">
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
</goal>
<goal name="VC mopp" expl="VC for mopp" proved="true">
......@@ -2563,7 +2588,15 @@
<proof prover="0"><result status="valid" time="0.67" steps="227"/></proof>
</goal>
<goal name="VC meq.1" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="1.19" steps="660"/></proof>
<transf name="introduce_premises" proved="true" >
<goal name="VC meq.1.0" expl="postcondition" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="VC meq.1.0.0" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.14"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
......
src/transform/reification.ml
View file @ 44f44412
......@@ -18,6 +18,9 @@ let debug_interp = Debug.register_info_flag
let debug_refl = Debug.register_info_flag
~desc:"Reflection transformations"
"reflection"
let debug_flamegraph = Debug.register_info_flag
~desc:"Print callstacks from the interpreter in Flamegraph input format."
"interp_flamegraph"
let print_id fmt id = Format.fprintf fmt "%s" id.id_string
......@@ -601,8 +604,6 @@ open Ity
exception CannotReduce
let append l = List.fold_left (fun acc s -> acc^":"^s) "" l
type value =
| Vconstr of rsymbol * field list
| Vtuple of value list
......@@ -615,7 +616,7 @@ type value =
and field = Fimmutable of value | Fmutable of value ref
exception Raised of xsymbol * value option * string
exception Raised of xsymbol * value option * rsymbol list
open Format
......@@ -931,9 +932,36 @@ type info = {
recs: rsymbol Mrs.t;
funs: decl Mrs.t;
get_decl: rsymbol -> Mltree.decl;
cs: string list; (* callstack for debugging *)
cur_rs: rsymbol; (* current function *)
cs: rsymbol list; (* callstack for debugging/profiling *)
}
let ts = ref 0. (* timestamp for current callstack *)
let print_callstack cs time =
Format.eprintf "%a %d@."
(Pp.print_list (fun fmt () -> Format.fprintf fmt ";") Expr.print_rs)
(List.rev cs)
(int_of_float (time *. 100000000.))
let cs_push info rs =
let new_cs = rs :: info.cs in
if Debug.test_flag debug_flamegraph
then begin
let ts_end = Unix.gettimeofday () in
print_callstack info.cs (ts_end -. !ts);
ts := Unix.gettimeofday ();
{ info with cur_rs = rs; cs = new_cs }
end
else { info with cur_rs = rs; cs = new_cs }
let cs_pop info =
if Debug.test_flag debug_flamegraph
then begin
let ts_end = Unix.gettimeofday () in
print_callstack info.cs (ts_end -. !ts);
ts := Unix.gettimeofday () end
let get pv info : value = Mid.find pv.pv_vs.vs_name info.vars
let add_id id v info = {info with vars = Mid.add id v info.vars}
......@@ -992,7 +1020,13 @@ let rec interp_expr info (e:Mltree.expr) : value =
print_id id print_value v;
add_id id v info)
info le vl in
interp_expr { info' with cs = rs.rs_name.id_string::(info'.cs) } e in
if rs_equal rs info.cur_rs
then interp_expr info' e
else begin
let info' = cs_push info' rs in
let v = interp_expr info' e in
cs_pop info';
v end in
Debug.dprintf debug_interp "eval call@.";
let res = try begin
let rs = if Mrs.mem rs info.recs then Mrs.find rs info.recs else rs in
......@@ -1125,7 +1159,7 @@ let rec interp_expr info (e:Mltree.expr) : value =
let ov = match oe with
| None -> None
| Some e -> Some (interp_expr info e) in
raise (Raised (xs, ov, append info.cs))
raise (Raised (xs, ov, info.cs))
| Eexn _ -> Debug.dprintf debug_interp "Eexn@.";
raise CannotReduce
| Eabsurd -> Debug.dprintf debug_interp "Eabsurd@.";
......@@ -1295,13 +1329,16 @@ let reflection_by_function do_trans s env = Trans.store (fun task ->
recs = Mrs.empty;
vars = vars;
get_decl = get_decl;
cur_rs = rs;
cs = [];
} in
Debug.dprintf debug_refl "eval_fun@.";
ts := Unix.gettimeofday ();
let res =
try term_of_value (eval_fun decl info)
with Raised (xs,_,s) ->
Format.eprintf "Raised %s %s@." (xs.xs_name.id_string) s;
with Raised (xs,_,cs) ->
Format.eprintf "Raised %s %a@." (xs.xs_name.id_string)
(Pp.print_list Pp.semi Expr.print_rs) cs;
raise (ReductionFail renv) (*(try eval_fun decl info with Raised _ -> Vbool false)*) in
Debug.dprintf debug_refl "res %a@." Pretty.print_term res;
let rinfo = {renv with subst = Mvs.add vres res renv.subst} in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment