Skip to content

Sanity test all solvers and fix topdown_term & slr3 #1605

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
sim642 merged 7 commits into from
Dec 16, 2024
Merged

Sanity test all solvers and fix topdown_term & slr3 #1605

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
3bb17bc
Add cram tests for some solvers
sim642 Oct 24, 2024
e57072f
Fix option name in topdown_space_cache_term
sim642 Oct 24, 2024
f0a15f6
Fix basic functionality of topdown_term
sim642 Oct 24, 2024
1eb63b9
Fix invalid widen call in topdown_term for side effects
sim642 Oct 24, 2024
c348dd6
Add cram tests for remaining solvers
sim642 Oct 24, 2024
4a9b52f
Fix invalid widen call in slr3 for globals
sim642 Dec 16, 2024
b0243f9
Disable broken two solver
sim642 Dec 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions src/solver/sLR.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ module SLR3 =
if tracing then trace "sol" "Contrib:%a" S.Dom.pretty tmp;
let tmp =
if wpx then
if HM.mem globals x then S.Dom.widen old tmp
if HM.mem globals x then S.Dom.widen old tmp (* TODO: no join in second argument, can call widen incorrectly? *)
else box old tmp
else tmp
in
Expand Down Expand Up @@ -527,7 +527,7 @@ let _ =
Selector.add_solver ("widen2", (module PostSolver.EqIncrSolverFromEqSolver (W2)));
Selector.add_solver ("widen3", (module PostSolver.EqIncrSolverFromEqSolver (W3)));
let module S2 = TwoPhased (struct let ver = 1 end) in
Selector.add_solver ("two", (module PostSolver.EqIncrSolverFromEqSolver (S2)));
Selector.add_solver ("two", (module PostSolver.EqIncrSolverFromEqSolver (S2))); (* TODO: broken even on 00-sanity/01-assert *)
let module S1 = Make (struct let ver = 1 end) in
Selector.add_solver ("new", (module PostSolver.EqIncrSolverFromEqSolver (S1)));
Selector.add_solver ("slr+", (module PostSolver.EqIncrSolverFromEqSolver (S1)))
Expand Down
2 changes: 1 addition & 1 deletion src/solver/topDown_space_cache_term.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,7 @@ module WP =
)
in
(* restore values for non-widening-points *)
if GobConfig.get_bool "solvers.wp.restore" then (
if GobConfig.get_bool "solvers.td3.space_restore" then (
Logs.debug "Restoring missing values.";
let restore () =
let get x =
Expand Down
8 changes: 4 additions & 4 deletions src/solver/topDown_term.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,8 @@ module WP =
let stable = HM.create 10 in
let infl = HM.create 10 in (* y -> xs *)
let called = HM.create 10 in
let rho = HM.create 10 in
let rho' = HM.create 10 in
let rho = HM.create 10 in (* rho for right-hand side values *)
let rho' = HM.create 10 in (* rho for start and side effect values *)
let wpoint = HM.create 10 in

let add_infl y x =
Expand Down Expand Up @@ -85,7 +85,7 @@ module WP =
and side y d =
let old = try HM.find rho' y with Not_found -> S.Dom.bot () in
if not (S.Dom.leq d old) then (
HM.replace rho' y (S.Dom.widen old d);
HM.replace rho' y (S.Dom.widen old (S.Dom.join old d));
HM.remove stable y;
init y;
solve y Widen;
Expand All @@ -101,7 +101,7 @@ module WP =
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;
HM.replace rho x d;
HM.replace rho' x d;
solve x Widen
in

Expand Down
Loading