Store all incremental data into single file #748
Conversation
Incremental data is kept in-memory, maintained by Serialize.Cache. Retrieving the data from there can be done using a GADT.
src/incremental/serialize.ml
Outdated
| solver_data: Obj.t option ref; | ||
| analysis_data: Obj.t option ref; | ||
| version_data: MaxIdUtil.max_ids option ref; | ||
| cil_file: Cil.file option ref; |
There was a problem hiding this comment.
Instead of refs, the fields could simply be mutable.
Also, why are they all options? When would we ever have incremental data that doesn't have all four components present? I think we always need all of them (or have none of them), so the whole record could be optional.
There was a problem hiding this comment.
Instead of refs, the fields could simply be mutable.
Done.
Also, why are they all options? When would we ever have incremental data that doesn't have all four components present? I think we always need all of them (or have none of them), so the whole record could be optional.
The issue is that during the initial analysis, these fields would not all become available at the same time. Namely, the Cil file and the max ids would become available after parsing (in Maingoblint), while the solver and analysis data only becomes availabe after solving the constraint system.
If one were to make the fields in the record non-optional, one would have to drag the cil file and max ids around until all of the data is available, so that one can set them in the record here.
There was a problem hiding this comment.
One could potentially have two different records for the data that was read from the previous run and for the data that one produces in the current run. Then in first record the fields would be non-optional and in the other they would be optional.
There was a problem hiding this comment.
these fields would not all become available at the same time
Right. At some point this bothered me before, but I think we can keep them optional for now.
At some point it might be useful to have them all in an immutable record that's read and created as a whole, because storing them at different times maybe can cause some inconsistencies during server mode or such. For example, if the new file is parsed and stored, the solving starts but is aborted, then the cache possibly has inconsistent state.
in some intermediate version of the code refs were used, as they make it possbile to extract the code that obtains the reference to a field into a separate method. This is no longer needed.
Remove "Request" suffix for variants of the data_query constructor.
… incremental data
…ype. This way, it can be avoided to do an explicit cast via Obj.obj when querying the AnalysisData.
sim642
left a comment
sim642
left a comment
There was a problem hiding this comment.
I didn't test this, but the code looks like it should.
2 participants
With this PR, the incremental data is stored to a single file.
Now, incremental data is kept in-memory, maintained by
Serialize.Cache. Data stored on disc can be loaded into memory withload_data, and stored from the cache to disk withstore_data.Retrieving the data from there can be done using a GADT, giving some type safety for the stored data with static type. As the the types for solver and analysis data are determined at run time, they are still kept as
Obj.tin the cache.Closes #357.