From afc0f30cbdd1eb805a9073c771648d249b5d8163 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 28 Mar 2024 10:38:01 -0700 Subject: [PATCH] [uninit] Degrade eval mode when unknown effect is found Summary: When a variable is given to an unknown function, all reachable addresses from the variable are havoc'ed with being set as having the "unknown effect" attribute. The problem is that when the variable had not enough fields in the abstract memory, e.g. given as a parameter, it missed the attribue setting. ``` foo (arg) { unknown(arg); _ = arg.f; } ``` Although `arg.f` may be initialized by `unknown`, the summary of foo included "`arg.f` must be initialized" before calling `foo`, because it did not havoc `arg.f` when `unknown` was called. To avoid the problem, when evaluating `arg.f`, this diff checks whether `arg` has "unknown effect" or not, and if so, assumes `arg.f` has been initialized. Reviewed By: jvillard Differential Revision: D55380943 fbshipit-source-id: 4fcf07434db75297acbd110df9c0972f857e35c6 --- infer/src/pulse/PulseAbductiveDomain.ml | 8 ++++ infer/src/pulse/PulseAbductiveDomain.mli | 2 + infer/src/pulse/PulseBaseAddressAttributes.ml | 7 ++++ .../src/pulse/PulseBaseAddressAttributes.mli | 2 + infer/src/pulse/PulseOperations.ml | 38 +++++++++++++++++-- .../tests/codetoanalyze/cpp/pulse/uninit.cpp | 19 ++++++++++ 6 files changed, 72 insertions(+), 4 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index f626f49c1ea..cede28c670a 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -629,6 +629,10 @@ module Internal = struct abduce_one addr (MustBeValid (path.PathContext.timestamp, access_trace, must_be_valid_reason)) astate + + + let has_unknown_effect addr astate = + BaseAddressAttributes.has_unknown_effect addr (astate.post :> base_domain).attrs end module SafeMemory = struct @@ -2375,6 +2379,10 @@ module AddressAttributes = struct let get_address_of_stack_variable v astate = SafeAttributes.get_address_of_stack_variable (CanonValue.canon' astate v) astate + + + let has_unknown_effect v astate = + SafeAttributes.has_unknown_effect (CanonValue.canon' astate v) astate end module CanonValue = struct diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 7d3144da7ff..53529baeee8 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -256,6 +256,8 @@ module AddressAttributes : sig val get_address_of_stack_variable : AbstractValue.t -> t -> (Var.t * Location.t * ValueHistory.t) option + + val has_unknown_effect : AbstractValue.t -> t -> bool end val should_havoc_if_unknown : unit -> [> `ShouldHavoc | `ShouldOnlyHavocResources] diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml index c39063fa299..2a2a83b2bbd 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.ml +++ b/infer/src/pulse/PulseBaseAddressAttributes.ml @@ -325,6 +325,11 @@ let get_address_of_stack_variable address attrs = get_attribute Attributes.get_address_of_stack_variable address attrs +let has_unknown_effect address attrs = + Graph.find_opt address attrs + |> Option.exists ~f:(fun attribute -> Option.is_some (Attributes.get_unknown_effect attribute)) + + let merge attrs attrs' = (* "merge" attributes if two different values ([addr] and [addr']) are found to be equal after attributes of the same kind were recorded for them. This arbitrarily @@ -477,4 +482,6 @@ module type S = sig val initialize : key -> t -> t val get_address_of_stack_variable : key -> t -> (Var.t * Location.t * ValueHistory.t) option + + val has_unknown_effect : key -> t -> bool end diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index 11bac6a8626..d74fb652582 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/infer/src/pulse/PulseBaseAddressAttributes.mli @@ -129,6 +129,8 @@ module type S = sig val initialize : key -> t -> t val get_address_of_stack_variable : key -> t -> (Var.t * Location.t * ValueHistory.t) option + + val has_unknown_effect : key -> t -> bool end include S with type key := AbstractValue.t diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 0280c689b08..587d1b9e6f3 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -165,6 +165,14 @@ let write_deref path location ~ref:addr_trace_ref ~obj:addr_trace_obj astate = write_access path location addr_trace_ref Dereference addr_trace_obj astate +let degrade_mode addr astate mode = + match mode with + | Read when AbductiveDomain.AddressAttributes.has_unknown_effect addr astate -> + NoAccess + | _ -> + mode + + let rec eval (path : PathContext.t) mode location exp astate : (t * (AbstractValue.t * ValueHistory.t)) PulseOperationResult.t = let++ astate, value_origin = eval_to_value_origin path mode location exp astate in @@ -232,11 +240,13 @@ and eval_to_value_origin (path : PathContext.t) mode location exp astate : | Lvar pvar -> Sat (Ok (eval_var_to_value_origin path location pvar astate)) | Lfield (exp', field, _) -> - let+* astate, addr_hist = eval path Read location exp' astate in + let+* astate, ((addr, _) as addr_hist) = eval path Read location exp' astate in + let mode = degrade_mode addr astate mode in eval_access_to_value_origin path mode location addr_hist (FieldAccess field) astate | Lindex (exp', exp_index) -> let** astate, addr_hist_index = eval path Read location exp_index astate in - let+* astate, addr_hist = eval path Read location exp' astate in + let+* astate, ((addr, _) as addr_hist) = eval path Read location exp' astate in + let mode = degrade_mode addr astate mode in eval_access_to_value_origin path mode location addr_hist (ArrayAccess (StdTyp.void, fst addr_hist_index)) astate @@ -345,9 +355,29 @@ let prune path location ~condition astate = prune_aux ~negated:false condition astate +let degrade_mode_exp path location exp astate mode = + let rec has_unknown_effect exp = + match (exp : Exp.t) with + | Lfield (exp, _, _) | Lindex (exp, _) -> + let** astate, (addr, _) = eval path NoAccess location exp astate in + if AddressAttributes.has_unknown_effect addr astate then Sat (Ok true) + else has_unknown_effect exp + | _ -> + let** astate, (addr, _) = eval path NoAccess location exp astate in + Sat (Ok (AddressAttributes.has_unknown_effect addr astate)) + in + match mode with + | Read -> + let++ has_unknown_effect = has_unknown_effect exp in + if has_unknown_effect then NoAccess else Read + | _ -> + Sat (Ok mode) + + let eval_deref_to_value_origin path ?must_be_valid_reason location exp astate = - let+* astate, addr_hist = eval path Read location exp astate in - let+ astate = check_addr_access path ?must_be_valid_reason Read location addr_hist astate in + let** astate, addr_hist = eval path Read location exp astate in + let+* mode = degrade_mode_exp path location exp astate Read in + let+ astate = check_addr_access path ?must_be_valid_reason mode location addr_hist astate in let astate, dest_addr_hist = Memory.eval_edge addr_hist Dereference astate in (astate, ValueOrigin.InMemory {src= addr_hist; access= Dereference; dest= dest_addr_hist}) diff --git a/infer/tests/codetoanalyze/cpp/pulse/uninit.cpp b/infer/tests/codetoanalyze/cpp/pulse/uninit.cpp index ac4f1fe0c8a..1aa9a26a3da 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/uninit.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/uninit.cpp @@ -117,6 +117,7 @@ class Uninit { }; class Uninit2 { + public: int f1; int f2; @@ -168,3 +169,21 @@ int init_in_callee_ok() { init_param(&x); return x; } + +class Nested { + public: + int i; + Uninit2 mc; +}; + +void unknown_init_nested(Nested& x); + +int read_nested(Nested& x) { + unknown_init_nested(x); + return x.mc.f1; +} + +int call_read_nested_ok() { + Nested x; + return read_nested(x); +}