From 0980bbe2b37adcde04cc93ba73a70e8dc7f7f32a Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 10 Dec 2020 04:45:30 -0800 Subject: [PATCH] [pulse] also visit values involved in array accesses Summary: There was a bug where we forgot to mark these values as reachable. In particular we would forget their arithmetic value as a result. For example, now we remember that the array access is at an index equal to 5 in the summary of this function: ``` foo(int a[]) { a[5] = 42; } ``` Reviewed By: skcho Differential Revision: D25430468 fbshipit-source-id: 4acf09842 --- infer/src/pulse/PulseBaseDomain.ml | 20 ++++++++++++++++---- infer/src/pulse/PulseInterproc.ml | 3 +++ 2 files changed, 19 insertions(+), 4 deletions(-) diff --git a/infer/src/pulse/PulseBaseDomain.ml b/infer/src/pulse/PulseBaseDomain.ml index 1782f1a41..7a128620e 100644 --- a/infer/src/pulse/PulseBaseDomain.ml +++ b/infer/src/pulse/PulseBaseDomain.ml @@ -245,11 +245,23 @@ end = struct let finish visited_accum = Continue visited_accum in Container.fold_until edges ~fold:Memory.Edges.fold ~finish ~init:visited_accum ~f:(fun visited_accum (access, (address, _trace)) -> - match visit_address address ~f (access :: rev_accesses) astate visited_accum with - | Continue _ as cont -> - cont + match visit_access ~f access astate visited_accum with | Stop fin -> - Stop (Stop fin) ) + Stop (Stop fin) + | Continue visited_accum -> ( + match visit_address address ~f (access :: rev_accesses) astate visited_accum with + | Continue _ as cont -> + cont + | Stop fin -> + Stop (Stop fin) ) ) + + + and visit_access ~f (access : Memory.Access.t) astate visited_accum = + match access with + | ArrayAccess (_, addr) -> + visit_address addr ~f [] astate visited_accum + | FieldAccess _ | TakeAddress | Dereference -> + Continue visited_accum let visit_address_from_var (orig_var, (address, _loc)) ~f rev_accesses astate visited_accum = diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 68a489873..c1cbd3248 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -182,6 +182,9 @@ let rec materialize_pre_from_address callee_proc_name call_location ~pre ~addr_p | Some edges_pre -> Container.fold_result ~fold:Memory.Edges.fold ~init:call_state edges_pre ~f:(fun call_state (access_callee, (addr_pre_dest, _)) -> + (* HACK: we should probably visit the value in the (array) access too, but since it's + a value normally it shouldn't appear in the heap anyway so there should be nothing + to visit. *) let subst, access_caller = translate_access_to_caller call_state.subst access_callee in let astate, addr_hist_dest_caller = Memory.eval_edge addr_hist_caller access_caller call_state.astate