Conversation
JTrenerry
left a comment
JTrenerry
left a comment
There was a problem hiding this comment.
Barely looked, but there is your review :)
| add_edge_e_dir dir g | ||
| ( IntraVertex { proc_id; v = Entry }, | ||
| StubProc { formal_in; globals }, | ||
| IntraVertex { proc_id; v = Return } )) |
There was a problem hiding this comment.
I hope it would be possible to just construct a forward (bidirectional) graph and use Bincaml_util.Reverse_graph to reverse the view of edge direction
There was a problem hiding this comment.
That would be nice but I don't know how to set things up nicely so that the solver works well with a bidirectional graph like that :(
The issue is that (and this answers another point) the solver, or at least as presented in the paper, needs special logic when transferring on the edge to the entry of a procedure, and the meaning of entry needs to change to be the return edge when going backwards since that's just how we traverse the graph (again, following the solver logic). What's worse is that I needed to give call vertices a link to their corresponding return vertex which goes further from any potential bidirectionality... It might be possible but it would need some thinking and I'm not sure how worth it it is.
| IDEGraph.G.succ_e graph l |> Iter.of_list | ||
| |> Iter.iter (fun e -> | ||
| let from, target = match e with from, _, target -> (from, target) in | ||
| match IDEGraph.G.E.label e with |
There was a problem hiding this comment.
Can we factor this match into a function?
| |> Iter.map (fun (d5, e4) -> | ||
| ((d1, d5), D.compose e4 e321)) | ||
| |> propagate worklist summaries priority | ||
| (get_summary aftercall) aftercall)) |
There was a problem hiding this comment.
Lots of places you could probably flatten the indentation by using iter and flat map rather then nesting into the fold/map function argument, eg a |> Option.to_iter |> Iter.flat_map DLMap.to_iter |> ... because I read left to right lol
| edges somehow. I suspect this won't give a huge performance improvement since | ||
| mose of the time in the solver is spent on evaluating transfer functions. *) | ||
| (* TODO write a sample forwards analysis to test forwards correctness *) | ||
|
|
There was a problem hiding this comment.
I hope there would be some way of optimising the transfer; most of the time you're composing id edges so don't rly need to transfer every variable in the state if you know the dependencies of the transfer function : and hopefully the analysis domain could tell you an edge's dependencies? Maybe its possible to push more of the domain composition reasoning into the analysis domain. Anyway I think that can be the next iteration if this is fast enough maybe it doesn't matter.
|
|
||
| val transfer : Program.stmt -> DL.t -> t state_update | ||
| (** update the state for a program statement *) | ||
| end |
There was a problem hiding this comment.
I wonder whether we can do something about the confusing 'return is actually an entry when analysis is backwards' thing; maybe worth even having diff sigs for forwards and backwards. Not a big deal though
There was a problem hiding this comment.
I probably won't be able to do something about this in the solver internally, but maybe the api could be changed instead? Do you think that would work? (So like transfer_return gets run on call edges when running a backwards analysis, where call edges go into return vertices)
3 participants
Rewrites the IDE solver. Interproc livevar analysis has been implemented and tested to some extent.