Commit 3cdc073f authored by Andrei Paskevich's avatar Andrei Paskevich

Trans: do not memoize transformations of goals

the goal declarations are not shared and thus memoizing transformations
on them is only interesting if we apply the same transformation on the
same goal (which may happen when we launch several provers of the same
family on the same goal). On the other hand, goal declarations are big
(think WP) and numerous (think goal_split), and keeping them in memory
is a bad idea.

The same example from BWare can now be treated with 1/4 of memory:

why3-replayer : full memoization
106.81user 7.86system 1:59.32elapsed 96%CPU (0avgtext+0avgdata 1656908maxresident)k

why3-replayer : no memoization on goals (this commit)
74.14user 4.24system 1:24.93elapsed 92%CPU (0avgtext+0avgdata 429376maxresident)k

why3-replayer : no memoization at all
217.78user 6.25system 3:43.56elapsed 100%CPU (0avgtext+0avgdata 615204maxresident)k

One side effect of this commit is that polymorphism encoding
transformations are likely to be memoized only for a short time.
The transformations that select the type instances to discriminate
and the types to preserve in encoding are full-task-dependent and
therefore are not memoized anymore. Thus, as soon the the task that
contains all the selection metas is GCed, the rest of the chain
will go, too, and Why3 will have to re-monomorphize the same decls.
We'll see if this is a problem in practice.
parent caf8cdf2
......@@ -47,7 +47,9 @@ module Wtask = Weakhtbl.Make (struct
let tag t = t.task_tag
end)
let store fn = Wtask.memoize_option 63 fn
let store fn = let tr = Wtask.memoize_option 63 fn in fun t -> match t with
| Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,_,_)}}} -> fn t
| _ -> tr t
let bind f g = store (fun task -> g (f task) task)
......@@ -60,8 +62,9 @@ let fold fn v =
| Use _ -> 'U' | Meta _ -> 'M') (task.task_decl.td_tag);
*)
let acc = fn task acc in
Wtask.set h task acc;
acc
match task.task_decl.td_node with
| Decl {d_node = Dprop (Pgoal,_,_)} -> acc
| _ -> Wtask.set h task acc; acc
in
let current task =
try Some (Wtask.find h task)
......@@ -82,8 +85,12 @@ let fold_map fn v t = conv_res snd (fold fn (v, t))
let fold_map_l fn v t = conv_res (List.map snd) (fold_l fn (v, t))
(* we use List.map instead of List.map_rev to preserve the order *)
let store_decl fn = let tr = Wdecl.memoize 63 fn in function
| {d_node = Dprop (Pgoal,_,_)} as d -> fn d
| d -> tr d
let gen_decl add fn =
let fn = Wdecl.memoize 63 fn in
let fn = store_decl fn in
let fn task acc = match task.task_decl.td_node with
| Decl d -> List.fold_left add acc (fn d)
| _ -> add_tdecl acc task.task_decl
......@@ -91,7 +98,7 @@ let gen_decl add fn =
fold fn
let gen_decl_l add fn =
let fn = Wdecl.memoize 63 fn in
let fn = store_decl fn in
let fn task acc = match task.task_decl.td_node with
| Decl d -> List.map (List.fold_left add acc) (fn d)
| _ -> [add_tdecl acc task.task_decl]
......@@ -107,17 +114,15 @@ let apply_to_goal fn d = match d.d_node with
| Dprop (Pgoal,pr,f) -> fn pr f
| _ -> assert false
let gen_goal add fn =
let fn = Wdecl.memoize 5 (apply_to_goal fn) in store (function
| Some { task_decl = { td_node = Decl d }; task_prev = prev } ->
List.fold_left add prev (fn d)
| _ -> assert false)
let gen_goal_l add fn =
let fn = Wdecl.memoize 5 (apply_to_goal fn) in store (function
| Some { task_decl = { td_node = Decl d }; task_prev = prev } ->
List.map (List.fold_left add prev) (fn d)
| _ -> assert false)
let gen_goal add fn = function
| Some { task_decl = { td_node = Decl d }; task_prev = prev } ->
List.fold_left add prev (apply_to_goal fn d)
| _ -> assert false
let gen_goal_l add fn = function
| Some { task_decl = { td_node = Decl d }; task_prev = prev } ->
List.map (List.fold_left add prev) (apply_to_goal fn d)
| _ -> assert false
let goal = gen_goal add_decl
let goal_l = gen_goal_l add_decl
......
......@@ -248,36 +248,26 @@ let call_on_buffer ~command ?timelimit ?memlimit ?inplace ~filename drv buffer =
exception NoPrinter
let update_task drv task_orig =
(** task_orig is the task for looking for theories
task is the task for adding new metas
goal is the last decl that we want to keep at the end (goal or clone)
*)
let task, goal = match task_orig with
| Some { task_decl = g ; task_prev = t } -> t,g
| None -> raise Task.GoalNotFound
in
let task =
let update_task = let ht = Hint.create 5 in fun drv ->
let update task0 =
Mid.fold (fun _ (th,s) task ->
Task.on_theory th (fun task sm ->
Stdecl.fold (fun tdm task ->
add_tdecl task (clone_meta tdm sm)
) s task
) task task_orig
) drv.drv_meta task
) task task0
) drv.drv_meta task0
in
add_tdecl task goal
let update_task =
let h = Hint.create 5 in
fun drv ->
let update = try Hint.find h drv.drv_tag with
| Not_found ->
let upd = Trans.store (update_task drv) in
Hint.add h drv.drv_tag upd;
upd
in
Trans.apply update
function
| Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,_,_)}} as goal;
task_prev = task} ->
(* we cannot add metas nor memoize after goal *)
let update = try Hint.find ht drv.drv_tag with Not_found ->
let upd = Trans.store update in
Hint.add ht drv.drv_tag upd; upd in
let task = Trans.apply update task in
add_tdecl task goal
| task -> update task
let prepare_task drv task =
let lookup_transform t = lookup_transform t drv.drv_env 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