now also fwdSolver with widening per node

Author: hseidl

src/framework/fwdSolver.ml

@@ -9,11 +9,13 @@ module FwdSolver (System: FwdGlobConstrSys) = struct
 
   module GM = Hashtbl.Make(System.GVar)
   module LM = Hashtbl.Make(System.LVar)
+  module OM = Hashtbl.Make(Node)
+
+  let source = System.LVar.node
 
   let gwarrow a b = if G.leq b a then G.narrow a b else G.widen a (G.join a b)
   let lwarrow a b = if D.leq b a then D.narrow a b else D.widen a (D.join a b)
 
-
   let work = ref (([] : System.LVar.t list), LS.empty)
 
   let add_work x = let (l,s) = !work in
@@ -30,7 +32,7 @@ module FwdSolver (System: FwdGlobConstrSys) = struct
 
   let gas = ref (10,3)
 
-  type glob = {value : G.t; init : G.t;  infl : System.LVar.t list; from : (G.t * int * int) LM.t}
+  type glob = {value : G.t; init : G.t;  infl : System.LVar.t list; from : (G.t * int * int) OM.t}
        (*
           now table from with widening delay and narrowing gas to ensure termination
        *)
@@ -42,7 +44,7 @@ module FwdSolver (System: FwdGlobConstrSys) = struct
   let get_global_ref g =
     try GM.find glob g
     with _ ->
-      (let rglob = {value = G.bot (); init = G.bot (); infl = []; from = LM.create 10} in
+      (let rglob = {value = G.bot (); init = G.bot (); infl = []; from = OM.create 10} in
        GM.add glob g rglob;
        rglob
       )
@@ -52,16 +54,17 @@ module FwdSolver (System: FwdGlobConstrSys) = struct
       value = d;
       init = d;
       infl = [];
-      from = LM.create 10
+      from = OM.create 10
     }
 
-  let get_global_value init from = LM.fold (fun _ (b,_,_) a -> G.join a b) from init
+  let get_global_value init from = OM.fold (fun _ (b,_,_) a -> G.join a b) from init
 
   let get_old_global_value x from =
-    try LM.find from x
+    let sx = source x in
+    try OM.find from sx
     with _ ->
       let (delay,gas) = !gas in
-      LM.add from x (G.bot (),delay,gas);
+      OM.add from sx (G.bot (),delay,gas);
       (G. bot (),delay,gas)
 
   (* now the getters and setters for globals, setters with warrowing per origin *)
@@ -72,6 +75,7 @@ module FwdSolver (System: FwdGlobConstrSys) = struct
     rglob.value
 
   let set_global x g d =
+    let sx = source x in
     (*
       replaces old contribution with the new one;
       reconstructs value of g from contributions;
@@ -81,24 +85,27 @@ module FwdSolver (System: FwdGlobConstrSys) = struct
     let (old_value,delay,gas) = get_old_global_value x from in
     if G.equal d old_value then () 
     else let (new_value,delay,gas) = if G.leq d old_value then
-        if gas > 0 then (G.narrow old_value d,delay,gas-1)
-        else (old_value,delay,0)
-      else if delay > 0 then (G.join old_value d,delay-1,gas)
-      else (G.widen old_value (G.join old_value d), 0, gas) in
-    let _ = LM.replace from x (new_value,delay,gas) in
-    let new_g = get_global_value init from in
-    if G.equal value new_g then
-      ()
-    else
-      let _ = List.iter add_work infl in
-      GM.replace glob g {value = new_g; init = init; infl = []; from}
+             if gas > 0 then (G.narrow old_value d,delay,gas-1)
+             else (old_value,delay,0)
+           else if delay > 0 then (G.join old_value d,delay-1,gas)
+           else (G.widen old_value (G.join old_value d), 0, gas) in
+      let _ = OM.replace from sx (new_value,delay,gas) in
+      let new_g = get_global_value init from in
+      if G.equal value new_g then
+        ()
+      else
+        let _ = List.iter add_work infl in
+        GM.replace glob g {value = new_g; init = init; infl = []; from}
 
   type loc = {loc_value : D.t; loc_init : D.t; loc_infl: System.LVar.t list; loc_from : (D.t * int * int) LM.t}
   (*
     init may contain some initial value not provided by separate origin;
     perhaps, dynamic tracking of dependencies required for certain locals?
 
-    One might additionally maintain in table loc_from some widening delay?
+    One might additionally maintain in table loc the set of previous contribs 
+    for rewoking vacuous previous contributions - important if large values 
+    are prematurely propagated which later become obsolete (no contrib from that
+    origin anymore ...
   *)
 
   let loc: loc LM.t = LM.create 100
@@ -146,17 +153,17 @@ module FwdSolver (System: FwdGlobConstrSys) = struct
     let (old_value,delay,gas) = get_old_local_value x loc_from in
     if D.equal d old_value then ()
     else let (new_value,delay,gas) = if D.leq d old_value then
-        if gas > 0 then (D.narrow old_value d,delay,gas-1)
-        else (old_value,delay,0)
-      else if delay > 0 then (D.join old_value d,delay-1,gas)
-      else (D.widen old_value (D.join old_value d), 0, gas) in
-    let _ = LM.replace loc_from x (new_value,delay,gas) in
-    let new_y = get_local_value loc_init loc_from in
-    if D.equal loc_value new_y then
-      ()
-    else let _ = add_work y in
-      let _ = List.iter add_work loc_infl in
-      LM.replace loc y {loc_value = new_y; loc_init; loc_infl = []; loc_from}
+             if gas > 0 then (D.narrow old_value d,delay,gas-1)
+             else (old_value,delay,0)
+           else if delay > 0 then (D.join old_value d,delay-1,gas)
+           else (D.widen old_value (D.join old_value d), 0, gas) in
+      let _ = LM.replace loc_from x (new_value,delay,gas) in
+      let new_y = get_local_value loc_init loc_from in
+      if D.equal loc_value new_y then
+        ()
+      else let _ = add_work y in
+        let _ = List.iter add_work loc_infl in
+        LM.replace loc y {loc_value = new_y; loc_init; loc_infl = []; loc_from}
 
 (*
         wrapper around propagation function to collect multiple contributions to same unknowns;