From 2d4cfd1d6b0e0dd81431a00b8d183b44a520c697 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Mon, 10 May 2021 18:20:21 +0200 Subject: [PATCH] [Eva] Fixes dynamic split when the first split fails. --- src/plugins/value/partitioning/partition.ml | 24 ++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml index 47019da338d..84848f17b4a 100644 --- a/src/plugins/value/partitioning/partition.ml +++ b/src/plugins/value/partitioning/partition.ml @@ -104,7 +104,7 @@ type key = { branches : branch list; loops : (int * int) list; (* current iteration / max unrolling *) static_split : (Integer.t*split_monitor) SplitMap.t; (* exp->value*monitor *) - dynamic_split : (Integer.t*split_monitor) SplitMap.t; (* exp->value*monitor *) + dynamic_split : (Integer.t option * split_monitor) SplitMap.t; (* exp->value*monitor *) } module Key = @@ -127,10 +127,13 @@ struct let compare_split (i1,_m1) (i2,_m2) = Integer.compare i1 i2 in + let compare_optsplit (i1,_m1) (i2,_m2) = + Option.compare Integer.compare i1 i2 + in Option.compare IntPair.compare k1.ration_stamp k2.ration_stamp <?> (LoopList.compare, k1.loops, k2.loops) <?> (SplitMap.compare compare_split, k1.static_split, k2.static_split) - <?> (SplitMap.compare compare_split, k1.dynamic_split, k2.dynamic_split) + <?> (SplitMap.compare compare_optsplit, k1.dynamic_split, k2.dynamic_split) <?> (BranchList.compare, k1.branches, k2.branches) let pretty fmt key = @@ -151,7 +154,13 @@ struct SplitTerm.pretty t (Integer.pretty ~hexa:false) i) fmt - (SplitMap.bindings key.static_split @ SplitMap.bindings key.dynamic_split) + (SplitMap.bindings key.static_split); + Pretty_utils.pp_list ~pre:"{@[" ~sep:" ;@ " ~suf:"@]}" + (fun fmt (t,(i,_m)) -> Format.fprintf fmt "%a:%a" + SplitTerm.pretty t + (Pretty_utils.pp_opt (Integer.pretty ~hexa:false)) i) + fmt + (SplitMap.bindings key.dynamic_split) let exceed_rationing key = key.ration_stamp = None end @@ -392,13 +401,13 @@ struct let split_state ~monitor (kind : split_kind) (term : split_term) (key : key) (state : state) : (key * state) list = + let add value map = SplitMap.add term (value, monitor) map in try - let add value map = SplitMap.add term (value, monitor) map in let update_key (v,x) = let k = match kind with | Static -> { key with static_split = add v key.static_split } - | Dynamic -> { key with dynamic_split = add v key.dynamic_split } + | Dynamic -> { key with dynamic_split = add (Some v) key.dynamic_split } in (k,x) in @@ -409,6 +418,11 @@ struct in List.map update_key states with Operation_failed -> + let key = + match kind with + | Static -> key + | Dynamic -> { key with dynamic_split = add None key.dynamic_split } + in [(key,state)] let split ~monitor (kind : split_kind) (term : split_term) (p : t) = -- GitLab