Skip to content

Commit

Permalink
remove unnecessary orphan side effect handling
Browse files Browse the repository at this point in the history 
it is not needed, as long as narrow-globs does work with incremental solving.
  • Loading branch information
@Red-Panda64
Red-Panda64 committed Dec 3, 2024
1 parent 59f4a2f commit 58c107f
Showing 1 changed file with 80 additions and 101 deletions.
181 changes: 80 additions & 101 deletions src/solver/td3.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ module Base =
sides: VS.t HM.t;
prev_sides: VS.t HM.t;
divided_side_effects: ((S.Dom.t * (int * divided_side_mode) option) HM.t) HM.t;
orphan_side_effects: S.Dom.t HM.t;
narrow_globs_start_values: S.Dom.t HM.t;
rho: S.Dom.t HM.t;
wpoint: unit HM.t;
stable: unit HM.t;
Expand All @@ -80,7 +80,7 @@ module Base =
sides = HM.create 10;
prev_sides = HM.create 10;
divided_side_effects = HM.create (if narrow_globs then 10 else 0);
orphan_side_effects = HM.create (if narrow_globs then 10 else 0);
narrow_globs_start_values = HM.create (if narrow_globs then 10 else 0);
rho = HM.create 10;
wpoint = HM.create 10;
stable = HM.create 10;
Expand Down Expand Up @@ -131,7 +131,7 @@ module Base =
sides = HM.copy data.sides;
prev_sides = HM.copy data.prev_sides;
divided_side_effects = HM.map (fun k v -> HM.copy v) data.divided_side_effects;
orphan_side_effects = HM.copy data.orphan_side_effects;
narrow_globs_start_values = HM.copy data.narrow_globs_start_values;
side_infl = HM.copy data.side_infl;
side_dep = HM.copy data.side_dep;
st = data.st; (* data.st is immutable *)
Expand Down Expand Up @@ -187,10 +187,10 @@ module Base =
HM.iter (fun k (v, gas) -> HM.replace inner_copy (S.Var.relift k) ((S.Dom.relift v), gas)) v;
HM.replace divided_side_effects (S.Var.relift k) inner_copy
) data.divided_side_effects;
let orphan_side_effects = HM.create (HM.length data.orphan_side_effects) in
let narrow_globs_start_values = HM.create (HM.length data.narrow_globs_start_values) in
HM.iter (fun k v ->
HM.replace orphan_side_effects (S.Var.relift k) (S.Dom.relift v)
) data.orphan_side_effects;
HM.replace narrow_globs_start_values (S.Var.relift k) (S.Dom.relift v)
) data.narrow_globs_start_values;
let side_infl = HM.create (HM.length data.side_infl) in
HM.iter (fun k v ->
HM.replace side_infl (S.Var.relift k) (VS.map S.Var.relift v)
Expand All @@ -216,7 +216,7 @@ module Base =
HM.iter (fun k v ->
HM.replace dep (S.Var.relift k) (VS.map S.Var.relift v)
) data.dep;
{st; infl; sides; prev_sides; divided_side_effects; orphan_side_effects; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep}
{st; infl; sides; prev_sides; divided_side_effects; narrow_globs_start_values; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep}

type phase = Widen | Narrow [@@deriving show] (* used in inner solve *)

Expand Down Expand Up @@ -253,7 +253,7 @@ module Base =
let sides = data.sides in
let prev_sides = data.prev_sides in
let divided_side_effects = data.divided_side_effects in
let orphan_side_effects = data.orphan_side_effects in
let narrow_globs_start_values = data.narrow_globs_start_values in
let rho = data.rho in
let wpoint = data.wpoint in
let stable = data.stable in
Expand Down Expand Up @@ -361,7 +361,7 @@ module Base =
begin match prev_sides_x with
| Some prev_sides_x -> VS.iter (fun y ->
if Option.is_none @@ HM.find_option acc y then begin
ignore @@ divided_side D_Narrow ~x y (S.Dom.bot ());
ignore @@ divided_side D_Narrow x y (S.Dom.bot ());
if S.Dom.is_bot @@ HM.find rho y then
let casualties = S.postmortem y in
List.iter (fun x -> solve x Widen) casualties
Expand All @@ -376,9 +376,9 @@ module Base =
HM.replace prev_sides x !new_sides;
end;
if narrow_globs_immediate_growth then
HM.iter (fun y acc -> if not @@ HM.mem changed y then ignore @@ divided_side D_Narrow ~x y acc) acc
HM.iter (fun y acc -> if not @@ HM.mem changed y then ignore @@ divided_side D_Narrow x y acc) acc
else (
HM.iter (fun y acc -> ignore @@ divided_side D_Box ~x y acc) acc
HM.iter (fun y acc -> ignore @@ divided_side D_Box x y acc) acc
)
)) (fun () -> eq x (eval l x) (side_acc acc changed x))
else
Expand Down Expand Up @@ -439,15 +439,15 @@ module Base =
| Some new_acc -> (
HM.replace acc y new_acc;
if narrow_globs_immediate_growth then (
let y_changed = divided_side D_Widen ~x y new_acc in
let y_changed = divided_side D_Widen x y new_acc in
if y_changed then
HM.replace changed y ();
)
)
| _ -> ()
and divided_side (phase:divided_side_mode) ?(do_destabilize=true) ?x y d : bool =
if tracing then trace "side" "divided side to %a from %a ## value: %a" S.Var.pretty_trace y (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty d;
if tracing then trace "sol2" "divided side to %a from %a ## value: %a" S.Var.pretty_trace y (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty d;
and divided_side (phase:divided_side_mode) x y d : bool =
if tracing then trace "side" "divided side to %a from %a ## value: %a" S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty d;
if tracing then trace "sol2" "divided side to %a from %a ## value: %a" S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty d;
if Hooks.system y <> None then (
Logs.warn "side-effect to unknown w/ rhs: %a, contrib: %a" S.Var.pretty_trace y S.Dom.pretty d;
);
Expand All @@ -456,91 +456,72 @@ module Base =
if tracing then trace "sol2" "stable add %a" S.Var.pretty_trace y;
HM.replace stable y ();

match x with
| Some x -> (
let sided = match HM.find_option sides y with
| Some sides -> VS.mem x sides
| None -> false in
if not sided then add_sides y x;
let init_divided_side_effects y = if not (HM.mem divided_side_effects y) then HM.replace divided_side_effects y (HM.create 10) in
init_divided_side_effects y;

let y_sides = HM.find divided_side_effects y in
let (old_side, narrow_gas) = HM.find_default y_sides x (S.Dom.bot (), narrow_globs_gas_default) in
let phase = if phase == D_Box then
if S.Dom.leq d old_side then D_Narrow else D_Widen
else
phase
in
if not (phase = D_Narrow && narrow_gas = Some (0, D_Widen)) then (
let (new_side, narrow_gas) = match phase with
| D_Widen -> (
let tmp = S.Dom.join old_side d in
if not @@ S.Dom.equal tmp old_side then
(if narrow_globs_conservative_widen && (S.Dom.leq tmp (HM.find rho y)) then
tmp
else
S.Dom.widen old_side tmp), Option.map (fun (x, _) -> (x, D_Widen)) narrow_gas
else old_side, narrow_gas)
| D_Narrow ->
let result = S.Dom.narrow old_side d in
let narrow_gas = if not @@ S.Dom.equal result old_side then
Option.map (fun (gas, phase) -> if phase = D_Widen then gas - 1, D_Narrow else (gas, phase)) narrow_gas
else
narrow_gas
in
result, narrow_gas
| _ -> failwith "unreachable"
let sided = match HM.find_option sides y with
| Some sides -> VS.mem x sides
| None -> false in
if not sided then add_sides y x;
let init_divided_side_effects y = if not (HM.mem divided_side_effects y) then HM.replace divided_side_effects y (HM.create 10) in
init_divided_side_effects y;

let y_sides = HM.find divided_side_effects y in
let (old_side, narrow_gas) = HM.find_default y_sides x (S.Dom.bot (), narrow_globs_gas_default) in
let phase = if phase == D_Box then
if S.Dom.leq d old_side then D_Narrow else D_Widen
else
phase
in
if not (phase = D_Narrow && narrow_gas = Some (0, D_Widen)) then (
let (new_side, narrow_gas) = match phase with
| D_Widen -> (
let tmp = S.Dom.join old_side d in
if not @@ S.Dom.equal tmp old_side then
(if narrow_globs_conservative_widen && (S.Dom.leq tmp (HM.find rho y)) then
tmp
else
S.Dom.widen old_side tmp), Option.map (fun (x, _) -> (x, D_Widen)) narrow_gas
else old_side, narrow_gas)
| D_Narrow ->
let result = S.Dom.narrow old_side d in
let narrow_gas = if not @@ S.Dom.equal result old_side then
Option.map (fun (gas, phase) -> if phase = D_Widen then gas - 1, D_Narrow else (gas, phase)) narrow_gas
else
narrow_gas
in
result, narrow_gas
| _ -> failwith "unreachable"
in

if not (S.Dom.equal old_side new_side) then (
if tracing then trace "side" "divided side to %a from %a changed (phase: %s) Old value: %a ## New value: %a" S.Var.pretty_trace y S.Var.pretty_trace x (show_divided_side_mode phase) S.Dom.pretty old_side S.Dom.pretty new_side;
if not (S.Dom.equal old_side new_side) then (
if tracing then trace "side" "divided side to %a from %a changed (phase: %s) Old value: %a ## New value: %a" S.Var.pretty_trace y S.Var.pretty_trace x (show_divided_side_mode phase) S.Dom.pretty old_side S.Dom.pretty new_side;

if S.Dom.is_bot new_side && narrow_gas = None then
HM.remove y_sides x
else
HM.replace y_sides x (new_side, narrow_gas);

let combined_side y =
let combined = match HM.find_option divided_side_effects y with
| Some map -> HM.fold (fun _ (value, _) acc -> S.Dom.join acc value) map (S.Dom.bot ())
| None -> S.Dom.bot () in
let orphaned = HM.find_default orphan_side_effects y (S.Dom.bot()) in
S.Dom.join combined orphaned in
let y_oldval = HM.find rho y in
let y_newval = if S.Dom.leq old_side new_side then
(* If new side is strictly greater than the old one, the value of y can only increase. *)
S.Dom.join y_oldval new_side
else
combined_side y in
if not (S.Dom.equal y_newval y_oldval) then (
if tracing then trace "side" "value of %a changed by side from %a (phase: %s) Old value: %a ## New value: %a"
S.Var.pretty_trace y S.Var.pretty_trace x (show_divided_side_mode phase) S.Dom.pretty y_oldval S.Dom.pretty y_newval;
HM.replace rho y y_newval;
if do_destabilize then
destabilize y;
);
true
) else
false
) else
false
)
| None -> (
let orphaned = HM.find_default orphan_side_effects y (S.Dom.bot ()) in
let wd = S.Dom.widen orphaned (S.Dom.join orphaned d) in
HM.replace orphan_side_effects y wd;
if tracing then trace "side" "orphaned side to %a" S.Var.pretty_trace y;
if S.Dom.is_bot new_side && narrow_gas = None then
HM.remove y_sides x
else
HM.replace y_sides x (new_side, narrow_gas);

let combined_side y =
let combined = match HM.find_option divided_side_effects y with
| Some map -> HM.fold (fun _ (value, _) acc -> S.Dom.join acc value) map (S.Dom.bot ())
| None -> S.Dom.bot () in
let start_value = HM.find_default narrow_globs_start_values y (S.Dom.bot()) in
S.Dom.join combined start_value in
let y_oldval = HM.find rho y in
if not (S.Dom.leq wd y_oldval) then (
if tracing then trace "side" "orphaned side changed %a (phase: %s)" S.Var.pretty_trace y (show_divided_side_mode phase);
HM.replace rho y (S.Dom.join wd y_oldval);
if do_destabilize then
destabilize y;
true
) else
false
)
let y_newval = if S.Dom.leq old_side new_side then
(* If new side is strictly greater than the old one, the value of y can only increase. *)
S.Dom.join y_oldval new_side
else
combined_side y in
if not (S.Dom.equal y_newval y_oldval) then (
if tracing then trace "side" "value of %a changed by side from %a (phase: %s) Old value: %a ## New value: %a"
S.Var.pretty_trace y S.Var.pretty_trace x (show_divided_side_mode phase) S.Dom.pretty y_oldval S.Dom.pretty y_newval;
HM.replace rho y y_newval;
destabilize y;
);
true
) else
false
) else
false
and eq x get set =
if tracing then trace "sol2" "eq %a" S.Var.pretty_trace x;
match Hooks.system x with
Expand Down Expand Up @@ -677,11 +658,9 @@ module Base =
let set_start (x,d) =
if tracing then trace "sol2" "set_start %a ## %a" S.Var.pretty_trace x S.Dom.pretty d;
init x;
(* TODO: SIDE make this change-proof *)
if narrow_globs then
ignore @@ divided_side ~do_destabilize:false D_Widen x d
else
HM.replace rho x d;
HM.replace narrow_globs_start_values x d;
HM.replace rho x d;
HM.replace stable x ();
(* solve x Widen *)
in
Expand Down Expand Up @@ -1233,7 +1212,7 @@ module Base =
print_data_verbose data "Data after postsolve";

verify_data data;
(rho, {st; infl; sides; prev_sides; divided_side_effects; orphan_side_effects; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep})
(rho, {st; infl; sides; prev_sides; divided_side_effects; narrow_globs_start_values; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep})
end

(** TD3 with no hooks. *)
Expand Down

0 comments on commit 58c107f

Please sign in to comment.