From 20b75c6303e25de30aa9472f87b90dce63d90110 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 22 Aug 2023 18:32:08 +0300 Subject: [PATCH] Use MayPointToA and ReachableFromA in varEq Co-authored-by: Simmo Saan --- src/analyses/libraryFunctions.ml | 1 + src/analyses/varEq.ml | 33 ++++++++++++++------------------ 2 files changed, 15 insertions(+), 19 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 5dc311a587..d9211ce897 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -279,6 +279,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__sigsetjmp", special [__ "env" [w]; drop "savesigs" []] @@ fun env -> Setjmp { env }); (* has two underscores *) ("sigsetjmp", special [__ "env" [w]; drop "savesigs" []] @@ fun env -> Setjmp { env }); ("siglongjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value }); + ("getaddrinfo", unknown [drop "node" [r]; drop "service" [r]; drop "hints" [r_deep]; drop "res" [w_deep]]); ] (** Pthread functions. *) diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index 90ea4e5eae..71ab214481 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -389,17 +389,11 @@ struct (* Give the set of reachables from argument. *) let reachables ~deep (ask: Queries.ask) es = let reachable e st = - match st with - | None -> None - | Some st -> - let q = if deep then Queries.ReachableFrom e else Queries.MayPointTo e in - let vs = ask.f q in - if Queries.LS.is_top vs then - None - else - Some (Queries.LS.join vs st) + let q = if deep then Queries.ReachableFromA e else Queries.MayPointToA e in + let vs = ask.f q in + Queries.AD.join vs st in - List.fold_right reachable es (Some (Queries.LS.empty ())) + List.fold_right reachable es (Queries.AD.empty ()) (* Probably ok as is. *) @@ -460,15 +454,16 @@ struct | None -> ctx.local let remove_reachable ~deep ask es st = - match reachables ~deep ask es with - | None -> D.top () - | Some rs -> - (* Prior to https://github.com/goblint/analyzer/pull/694 checks were done "in the other direction": - each expression in st was checked for reachability from es/rs using very conservative but also unsound reachable_from. - It is unknown, why that was necessary. *) - Queries.LS.fold (fun lval st -> - remove ask (Mval.Exp.to_cil lval) st - ) rs st + let rs = reachables ~deep ask es in + (* Prior to https://github.com/goblint/analyzer/pull/694 checks were done "in the other direction": + each expression in st was checked for reachability from es/rs using very conservative but also unsound reachable_from. + It is unknown, why that was necessary. *) + Queries.AD.fold (fun addr st -> + match addr with + | Queries.AD.Addr.Addr (v,o) -> remove ask (Mval.Exp.to_cil (v,ValueDomain.Offs.to_exp o)) st + | UnknownPtr -> D.top () + | _ -> st + ) rs st let unknown_fn ctx lval f args = let desc = LF.find f in