Skip to content
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

Fix load_run pruning entire solution in Gobview #651

Closed
wants to merge 1 commit into from
Closed

Fix load_run pruning entire solution in Gobview #651

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
8 changes: 7 additions & 1 deletion src/framework/control.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -422,7 +422,13 @@ struct
let save_run = let o = get_string "save_run" in if o = "" then (if gobview then "run" else "") else o in

let lh, gh = if load_run <> "" then (
let module S2' = (GlobSolverFromEqSolver (Generic.LoadRunIncrSolver (PostSolverArg))) (EQSys) (LHT) (GHT) in
let module PostSolverArg2 =
struct
include PostSolverArg
let should_prune = false (* the run should have been already pruned *)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should have indeed, but pruning a pruned solution shouldn't delete everything either, so this might be indicative of a deeper issue. If a solution is loaded, then the postsolver should be doing complete reverification anyway to check its validity and emit the warnings (by corresponding postsolvers), so it should still be reaching all the nodes and not pruning them.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just a thought, maybe the postsolver runs correctly on the loaded solution to check it and prints its warnings. While doing that it also collects a reachable set, which should prevent everything from being pruned. But maybe due to some hashconsing relifting problem, the reachable set lookups all fail, despite the values being in there or something.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The issue is caused by the fact that in that reachable set, the node's id are not the same as in the one that are unmarshalled, which cause the pruning to remove everything.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's unusual because the postsolver should add to the reachable set the same nodes that it handles when iterating the loaded solution.
Maybe something related to this Gobview change? goblint/gobview@f8c509d

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Okay so commenting out the code of goblint/gobview@f8c509d does indeed restore the correct node id, but it does not solve the problem that the pruning remove everything.
So the way gobview load a solution must differ from the way of goblint

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh damn! I automatically thought you were already testing with that change.
Turns out that commit was on the master branch in Gobview's repository, but the gobview submodule in this Goblint's repository hadn't yet been updated to include that commenting out. I now did that though.

I suppose one thing to try would be disabling ana.opt.hashcons to see if it might have anything to do with hashconsing and relifting.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Disabling ana.opt.hashcons does indeed solve the issue, but I don't think the issue comes directly from it, as one can execute a query with ana.opt.hashcons enabled and the load_run option set to some directory containing the results from goblint, and it works as expected.

My best guess is that there is something different between goblint's initialization and gobview's one, which I cannot find.

Copy link
Member

@jerhard jerhard Mar 29, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does GobView already perform relift on the loaded data, so that the hashcons tables are populated again?
Similar to what Goblint already does for the compare_runs option:

analyzer/src/framework/control.ml

Lines 440 to 442 in fe5c98d

VH.iter (fun k v ->
VH.replace vh' (S2.Var.relift k) (S2.Dom.relift v)
) vh;

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The code you linked is for the case the compare_runs option is set. For the load_run option in both Goblint and Gobview the relifting is done with the same code :

analyzer/src/solvers/generic.ml

Lines 20 to 26 in fe5c98d

let vh' = VH.create (VH.length vh) in
VH.iter (fun x d ->
let x' = S.Var.relift x in
let d' = S.Dom.relift d in
VH.replace vh' x' d'
) vh;
vh'

end
in
let module S2' = (GlobSolverFromEqSolver (Generic.LoadRunIncrSolver (PostSolverArg2))) (EQSys) (LHT) (GHT) in
let (r2, _) = S2'.solve entrystates entrystates_global startvars' in
r2
) else if compare_runs <> [] then (
Expand Down