Conversation
…IFIER_nondet_bool
|
|
||
| let instrument_with_gas (ts: TSG.t) gasexpr : TSG.t = | ||
| let modify_pre ts u = | ||
| Printf.printf " --- %d is call edge\n" u; |
There was a problem hiding this comment.
Generally use Log.logf in place of Printf.printf so that debugging info can be turned on / off selectively
| ValueHT.add var_to_sym (VVal v) sym; | ||
| VVal v | ||
|
|
||
| let prophesize var = |
| Printf.printf " --- %d is loop header\n" u; | ||
| let g = ref ts in | ||
| let x = new_vtx () in | ||
| (* step 1: add new out-edge from u -> x *) |
There was a problem hiding this comment.
WG.split_vertex g u (new_vtx ()) (Weight gasexpr) does steps 1 + 2.
| let instrument_main tg entry init_gas_expr = | ||
| let post_entry = new_vtx () in | ||
| (* step 1: add a vertex called post_entry *) | ||
| let tg = WG.add_vertex tg post_entry in |
There was a problem hiding this comment.
If we don't initialize it, it retains its (non-deterministic) initial value.
| (public_name srk) | ||
| (modules (:standard \ bigtop)) | ||
| (modes native) | ||
| (flags (:standard -w -32)) |
| ISet.iter (fun x -> | ||
| greatest := !greatest + 1; | ||
| Hashtbl.add to_map x (!greatest); | ||
| begin match SrkUtil.Int.Map.find_opt x !assertions with (* if x in assertions, new vertex also in assertions *) |
There was a problem hiding this comment.
Ideally we shouldn't duplicate assertions for inlined procedures, and only report safety if the assert is safe in all inlined copies.
| let (src, _) = currproc in | ||
| remove_subgraph tg' src | ||
| in | ||
| displayer tg; |
There was a problem hiding this comment.
Displayer is helpful for debugging the inliner, but I'd remove it from the interface now.
| PHT.add qmap (x, y) (PPS.add (proc, (src, v)) callee_set); | ||
| | _ -> () | ||
| ) (ISet.add x ISet.empty)) procedures; (* populate pmap, qmap *) | ||
| let compute_sinks () = |
There was a problem hiding this comment.
(Reverse) topological traversal of the callgraph? OCamlgraph has a Topological functor that accepts WG.RecGraph.Callgraph as a parameter.
There was a problem hiding this comment.
Or better yet, use the Loop module in srk, which will also identify connected components in the callgraph which you shouldn't inline.
| | Some callees, Some callers -> | ||
| (* a procedure is considered for inlining if it is (1) a sink in the call graph (2) at least one function calls it.*) | ||
| if ((PS.cardinal callees) == 0) && ((PPS.cardinal callers) > 0) then PS.add (x, y) acc else acc | ||
| | (_, _) -> failwith "" |
| PHT.add qmap (src, dst) (PPS.remove ((call_src, call_dst),(call_x, call_y)) callers); | ||
| tg | ||
| in let rec do_inline depth tg = | ||
| if depth == 0 then tg else |
There was a problem hiding this comment.
Depth saves us from non-termination when inlining recursive procedures, but inlining recursive procedures is unsound unless local variables are suitably renamed. I would just abandon trying to inline recursive procedures rather than implement renaming.
2 participants
Fully refactored GPS implementation with each component registered as flags. I just refactored the interpolation procedure into its own separate module today and implemented a routine for doing live-variables analysis from the Dietsch et. al paper (https://dl.acm.org/doi/10.1145/3106237.3106307). I need to write some more tests and do some more editing before working the live-variables analysis into the interpolation code. PR here to show diff, not ready to be merged yet.