[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

@@ -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

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]

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

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

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})
 

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);
+}