Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Handle pseudo return nodes in Node.of_id and improve their location #1000

Merged
merged 3 commits into from
Feb 28, 2023
Merged

Handle pseudo return nodes in Node.of_id and improve their location #1000

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
29204bf
Fix Node.of_id not handling pseudo returns
sim642 Feb 22, 2023
14c3750
Use function end location for pseudo return node
sim642 Feb 22, 2023
83c40ee
Exclude pseudo returns from dead lines counting
sim642 Feb 28, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions src/framework/cfgTools.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -233,11 +233,13 @@ let createCFG (file: file) =
* lazy, so it's only added when actually needed *)
let pseudo_return = lazy (
if Messages.tracing then Messages.trace "cfg" "adding pseudo-return to the function %s.\n" fd.svar.vname;
let newst = mkStmt (Return (None, fd_loc)) in
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;
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
addEdge newst_node (fd_loc, Ret (None, fd)) (Function fd);
addEdge newst_node (fd_end_loc, Ret (None, fd)) (Function fd);
newst_node
)
in
Expand Down
31 changes: 18 additions & 13 deletions src/framework/control.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,19 +98,24 @@ struct
let live_lines = ref StringMap.empty in
let dead_lines = ref StringMap.empty in
let add_one n v =
(* Not using Node.location here to have updated locations in incremental analysis.
See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *)
let l = UpdateCil.getLoc n in
let f = Node.find_fundec n in
let add_fun = BatISet.add l.line in
let add_file = StringMap.modify_def BatISet.empty f.svar.vname add_fun in
let is_dead = LT.for_all (fun (_,x,f) -> Spec.D.is_bot x) v in
if is_dead then (
dead_lines := StringMap.modify_def StringMap.empty l.file add_file !dead_lines
) else (
live_lines := StringMap.modify_def StringMap.empty l.file add_file !live_lines;
NH.add live_nodes n ()
);
match n with
| Statement s when Cilfacade.(StmtH.mem pseudo_return_to_fun s) ->
(* Exclude pseudo returns from dead lines counting. No user code at "}". *)
()
| _ ->
(* Not using Node.location here to have updated locations in incremental analysis.
See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *)
let l = UpdateCil.getLoc n in
let f = Node.find_fundec n in
let add_fun = BatISet.add l.line in
let add_file = StringMap.modify_def BatISet.empty f.svar.vname add_fun in
let is_dead = LT.for_all (fun (_,x,f) -> Spec.D.is_bot x) v in
if is_dead then (
dead_lines := StringMap.modify_def StringMap.empty l.file add_file !dead_lines
) else (
live_lines := StringMap.modify_def StringMap.empty l.file add_file !live_lines;
NH.add live_nodes n ()
);
in
Result.iter add_one xs;
let live_count = StringMap.fold (fun _ file_lines acc ->
Expand Down
6 changes: 5 additions & 1 deletion src/util/cilfacade.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -513,9 +513,13 @@ let stmt_sids: stmt IntH.t ResettableLazy.t =
h
)

let pseudo_return_stmt_sids: stmt IntH.t = IntH.create 13

(** Find [stmt] by its [sid].
@raise Not_found *)
let find_stmt_sid sid = IntH.find (ResettableLazy.force stmt_sids) sid
let find_stmt_sid sid =
try IntH.find pseudo_return_stmt_sids sid
with Not_found -> IntH.find (ResettableLazy.force stmt_sids) sid


let reset_lazy () =
Expand Down