Skip to content

Commit

Permalink
Remove CompareCFG dependency on CfgTools
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Dec 6, 2023
1 parent 036a016 commit dbec9e8
Show file tree
Hide file tree
Showing 4 changed files with 9 additions and 7 deletions.
6 changes: 6 additions & 0 deletions src/common/util/cilfacade.ml
Original file line number Diff line number Diff line change
Expand Up @@ -531,6 +531,12 @@ let stmt_fundecs: fundec StmtH.t ResettableLazy.t =
h
)


let get_pseudo_return_id fd =
let start_id = 10_000_000_000 in (* TODO get max_sid? *)
let sid = Hashtbl.hash fd.svar.vid in (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *)
if sid < start_id then sid + start_id else sid

let pseudo_return_to_fun = StmtH.create 113

(** Find [fundec] which the [stmt] is in. *)
Expand Down
6 changes: 1 addition & 5 deletions src/framework/cfgTools.ml
Original file line number Diff line number Diff line change
Expand Up @@ -122,10 +122,6 @@ let rec pretty_edges () = function
| [_,x] -> Edge.pretty_plain () x
| (_,x)::xs -> Pretty.dprintf "%a; %a" Edge.pretty_plain x pretty_edges xs

let get_pseudo_return_id fd =
let start_id = 10_000_000_000 in (* TODO get max_sid? *)
let sid = Hashtbl.hash fd.svar.vid in (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *)
if sid < start_id then sid + start_id else sid

let node_scc_global = NH.create 113

Expand Down Expand Up @@ -260,7 +256,7 @@ let createCFG (file: file) =
if Messages.tracing then Messages.trace "cfg" "adding pseudo-return to the function %s.\n" fd.svar.vname;
let fd_end_loc = {fd_loc with line = fd_loc.endLine; byte = fd_loc.endByte; column = fd_loc.endColumn} in
let newst = mkStmt (Return (None, fd_end_loc)) in
newst.sid <- get_pseudo_return_id fd;
newst.sid <- Cilfacade.get_pseudo_return_id fd;
Cilfacade.StmtH.add Cilfacade.pseudo_return_to_fun newst fd;
Cilfacade.IntH.replace Cilfacade.pseudo_return_stmt_sids newst.sid newst;
let newst_node = Statement newst in
Expand Down
2 changes: 1 addition & 1 deletion src/framework/constraints.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1004,7 +1004,7 @@ struct

let dummy_pseudo_return_node f =
(* not the same as in CFG, but compares equal because of sid *)
Node.Statement ({Cil.dummyStmt with sid = CfgTools.get_pseudo_return_id f})
Node.Statement ({Cil.dummyStmt with sid = Cilfacade.get_pseudo_return_id f})
in
let add_nodes_of_fun (functions: fundec list) (withEntry: fundec -> bool) =
let add_stmts (f: fundec) =
Expand Down
2 changes: 1 addition & 1 deletion src/incremental/compareCFG.ml
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ let (&&<>) (prev_result: bool * rename_mapping) f : bool * rename_mapping =

let eq_node (x, fun1) (y, fun2) ~rename_mapping =
let isPseudoReturn f sid =
let pid = CfgTools.get_pseudo_return_id f in
let pid = Cilfacade.get_pseudo_return_id f in
sid == pid in
match x,y with
| Statement s1, Statement s2 ->
Expand Down

0 comments on commit dbec9e8

Please sign in to comment.