diff --git a/src/causality.ml b/src/causality.ml
index a94519cc4c9189e19b73f6f2a613caba34488fe2..a579e096c3973b389bd223d8078c6093925deb1d 100644
--- a/src/causality.ml
+++ b/src/causality.ml
@@ -48,7 +48,8 @@ exception Error of error
to break cycle, then start afresh - insert g' into g - return g *)
(* Tests whether [v] is a root of graph [g], i.e. a source *)
-let is_graph_root v g = IdentDepGraph.in_degree g v = 0
+let is_graph_root v g =
+ IdentDepGraph.in_degree g v = 0
(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *)
let graph_roots g =
diff --git a/src/checks/liveness.ml b/src/checks/liveness.ml
index 03a91558e00851001febae31afd4b2349a454e0d..99ea71ae18638a9aa75f9684ad17263755225486 100644
--- a/src/checks/liveness.ml
+++ b/src/checks/liveness.ml
@@ -183,7 +183,7 @@ let pp_context fmt ctx =
quasi-reusable variables - [reusable] is the set of dead/reusable
dependencies of [var] in graph [g] - [policy] is the reuse map (which domain
is [evaluated]) *)
-let compute_dependencies heads ctx =
+let update_dependencies heads ctx =
(*Log.report ~level:6 (fun fmt -> Format.fprintf fmt
"compute_reusable_dependencies %a %a %a@." Disjunction.pp_ciset locals
Printers.pp_var_name var pp_context ctx);*)
@@ -201,32 +201,47 @@ let compute_dependencies heads ctx =
[v] is not an aliasable input of the equation defining [var] - [v] is not one
of the current heads (which contain [var]) - [v] is not currently in use *)
let eligible node ctx heads var v =
+ let is_another_head head v =
+ head.var_id = v.var_id || try Hashtbl.find ctx.policy head.var_id = v with Not_found -> false
+ in
Hashtbl.find ctx.policy v.var_id == v
&& Typing.eq_ground
(Types.unclock_type var.var_type)
(Types.unclock_type v.var_type)
&& (not (is_aliasable_input node var.var_id v))
- && (not (List.exists (fun h -> h.var_id = v.var_id) heads))
+ && List.for_all (fun h -> not (is_another_head h v)) heads
&& (*let repr_v = Hashtbl.find ctx.policy v.var_id*)
not
(Disjunction.CISet.exists
(fun p -> IdentDepGraph.mem_edge ctx.dep_graph p.var_id v.var_id)
ctx.evaluated)
-let compute_reuse node ctx heads var =
+let compute_reuse node inputs ctx heads var =
+ (*Format.eprintf "compute_reuse %s@ %a@." var.var_id pp_context ctx;*)
let disjoint = Hashtbl.find ctx.disjoint var.var_id in
let locally_reusable v =
+ let v_id =
+ if Disjunction.CISet.mem v inputs
+ then ExprDep.mk_read_var v.var_id
+ else v.var_id in
IdentDepGraph.fold_pred
(fun p r ->
r && Disjunction.CISet.exists (fun d -> p = d.var_id) disjoint)
ctx.dep_graph
- v.var_id
+ v_id
true
in
let eligibles =
- if ISet.mem var.var_id (ExprDep.node_memory_variables node) then
+ if ISet.mem var.var_id (ExprDep.node_memory_variables node)
+ then
Disjunction.CISet.empty
- else Disjunction.CISet.filter (eligible node ctx heads var) ctx.evaluated
+ else
+ if ISet.mem var.var_id (ExprDep.node_output_variables node)
+ then
+ Disjunction.CISet.filter (fun v -> (not (Disjunction.CISet.mem v inputs))
+ && eligible node ctx heads var v) ctx.evaluated
+ else
+ Disjunction.CISet.filter (eligible node ctx heads var) ctx.evaluated
in
let quasi_dead, live =
Disjunction.CISet.partition locally_reusable eligibles
@@ -234,7 +249,7 @@ let compute_reuse node ctx heads var =
let disjoint_live = Disjunction.CISet.inter disjoint live in
let dead =
Disjunction.CISet.filter
- (fun v -> is_graph_root v.var_id ctx.dep_graph)
+ (fun v -> is_graph_root (if Disjunction.CISet.mem v inputs then ExprDep.mk_read_var v.var_id else v.var_id) ctx.dep_graph)
quasi_dead
in
Log.report ~level:7 (fun fmt ->
@@ -273,14 +288,27 @@ let remove_call_return_dependency g =
IdentDepGraph.(iter_succ (remove_edge g v) g v))
g
+let add_input_dependency inputs g =
+ Disjunction.CISet.iter (fun v -> IdentDepGraph.add_vertex g ExprDep.(mk_read_var v.var_id)) inputs
+
let compute_reuse_policy node schedule disjoint g =
+ let inputs =
+ List.fold_left
+ (fun inputs v -> Disjunction.CISet.add v inputs)
+ Disjunction.CISet.empty
+ (if node.node_iscontract then node.node_inputs @ node.node_outputs
+ else node.node_inputs) in
+ (*let inputs = Disjunction.CISet.empty in*)
+ let policy = Hashtbl.create 23 in
+ Disjunction.CISet.iter (fun v -> Hashtbl.add policy v.var_id v) inputs;
remove_call_return_dependency g;
+ add_input_dependency inputs g;
let ctx =
{
- evaluated = Disjunction.CISet.empty;
+ evaluated = inputs;
dep_graph = g;
disjoint;
- policy = Hashtbl.create 23;
+ policy = policy;
}
in
List.iter
@@ -308,18 +336,14 @@ let compute_reuse_policy node schedule disjoint g =
Printers.pp_node_eq
(get_node_eq head.var_id node)))
heads));
- compute_dependencies heads ctx;
+ update_dependencies heads ctx;
Log.report ~level:6 (fun fmt ->
Format.fprintf
fmt
"@[<v>@[<v 2>new context:@,%a@]@,COMPUTE_REUSE@,@]"
pp_context
ctx);
- List.iter
- (fun head ->
- compute_dependencies [ head ] ctx;
- compute_reuse node ctx heads head)
- heads;
+ List.iter (fun head -> update_dependencies [head] ctx; compute_reuse node inputs ctx heads head) heads;
(*compute_evaluated heads ctx;*)
Log.report ~level:6 (fun fmt ->
Format.(
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index cb8833d20b0917989dc02a8683af1a382c2ba46d..766352c1257b15434e40658362cff80b24d4554f 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -1044,9 +1044,12 @@ let step_replace_var m reuse step =
List.fold_left
(fun res l ->
let l' = fvar l in
- if List.exists (fun o -> o.var_id = l'.var_id) step.step_outputs then
+ if List.exists (fun o -> o.var_id = l'.var_id) step.step_outputs
+ || List.exists (fun i -> i.var_id = l'.var_id) step.step_inputs
+ then
res
- else Utils.add_cons l' res)
+ else
+ Utils.add_cons l' res)
[]
step.step_locals
in