Cleanup some option related code
#1689
Conversation
There was a problem hiding this comment.
This simplifies some uses but I'm unsure about others.
In particular, replacing some matches with large bodies with Option.map_default (or similar) sometimes moves what's being matched much further down (after the lambda). This might hurt readability because the code doesn't read top-down as it executes.
I think it would be good for someone else to also have a look with this in mind to see if they also get this impression.
| match ID.to_bool i with | ||
| | Some b -> b | ||
| | None -> Bool.top () | ||
| BatOption.default (Bool.top ()) (ID.to_bool i) |
There was a problem hiding this comment.
This might make no difference here, but previously Bool.top was only called when actually needed, now it's always called but possibly ignored.
There is BatOption.default_delayed for that purpose. Maybe there are other instances where that would be more needed.
| f' | ||
| ) (S.system x) |
There was a problem hiding this comment.
I think usually we have the lambda body indented by one more level in calls like this.
| (* there should be smarter ways to do this, e.g. by keeping track of which values are written etc. ... *) | ||
| (* See, e.g, Beckschulze E, Kowalewski S, Brauer J (2012) Access-based localization for octagons. Electron Notes Theor Comput Sci 287:29–40 *) | ||
| (* Also, a local *) | ||
| let vname = GobApron.Var.show var in | ||
| let locals = fundec.sformals @ fundec.slocals in | ||
| match List.find_opt (fun v -> VM.var_name (Local v) = vname) locals with (* TODO: optimize *) |
There was a problem hiding this comment.
I suspect the TODO: optimize should be preserved. I guess it's about using repeated string conversions to find some variable.
| let st' = set_savetop ~man st address lval_type new_val in | ||
| match Dep.find_opt v fun_st.deps with | ||
| | None -> st' | ||
| (* if a var partitions an array, all cpa-info for arrays it may partition are added from callee to caller *) |
Co-authored-by: Simmo Saan <[email protected]>
Co-authored-by: Simmo Saan <[email protected]>
Using
map_default,map_defualt_delayed, and friends makes the code much more concise.