[inferbo] Symbolic value for global variable

Summary:
It assigns symbolic values for global variables in the load commands. However, it does not instantiate the symbols for the global variables yet, which will be addressed in another diff.

Depends on D14208643

Reviewed By: ezgicicek

Differential Revision: D14257619

fbshipit-source-id: f9113c8a3

infer/src/bufferoverrun/absLoc.ml

@@ -218,6 +218,15 @@ module Loc = struct
         None
 
 
+  let rec is_global = function
+    | Var (Var.ProgramVar pvar) ->
+        Pvar.is_global pvar
+    | Var (Var.LogicalVar _) | Allocsite _ ->
+        false
+    | Field (loc, _) ->
+        is_global loc
+
+
   let rec get_path = function
     | Var (LogicalVar _) ->
         None

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -163,8 +163,8 @@ module TransferFunctions = struct
           L.d_printfln_escaped "/!\\ Failed to get initializer name of global constant %a"
             (Pvar.pp Pp.text) pvar ;
           Dom.Mem.add_unknown id ~location mem )
-    | Load (id, exp, _, _) ->
+    | Load (id, exp, typ, _) ->
-        BoUtils.Exec.load_locs id (Sem.eval_locs exp mem) mem
+        BoUtils.Exec.load_locs id typ (Sem.eval_locs exp mem) mem
     | Store (exp1, _, Const (Const.Cstr s), location) ->
         let locs = Sem.eval_locs exp1 mem in
         let model_env =

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -443,6 +443,10 @@ module Val = struct
   let is_mone x = Itv.is_mone (get_itv x)
 
   let of_path tenv ~may_last_field integer_type_widths location typ path =
+    let traces_of_loc l =
+      let trace = if Loc.is_global l then Trace.Global l else Trace.Parameter l in
+      TraceSet.singleton location trace
+    in
     let is_java = Language.curr_language_is Java in
     L.d_printfln_escaped "Val.of_path %a : %a%s%s" SPath.pp_partial path (Typ.pp Pp.text) typ
       (if may_last_field then ", may_last_field" else "")
@@ -450,7 +454,7 @@ module Val = struct
     match typ.Typ.desc with
     | Tint _ | Tfloat _ | Tvoid | Tfun _ | TVar _ ->
         let l = Loc.of_path path in
-        let traces = TraceSet.singleton location (Trace.Parameter l) in
+        let traces = traces_of_loc l in
         let unsigned = Typ.is_unsigned_int typ in
         of_itv ~traces (Itv.of_normal_path ~unsigned path)
     | Tptr (elt, _) ->
@@ -460,13 +464,13 @@ module Val = struct
           in
           let deref_path = SPath.deref ~deref_kind path in
           let l = Loc.of_path deref_path in
-          let traces = TraceSet.singleton location (Trace.Parameter l) in
+          let traces = traces_of_loc l in
           {bot with powloc= PowLoc.singleton l; traces}
         else
           let deref_kind = SPath.Deref_CPointer in
           let deref_path = SPath.deref ~deref_kind path in
           let l = Loc.of_path deref_path in
-          let traces = TraceSet.singleton location (Trace.Parameter l) in
+          let traces = traces_of_loc l in
           let arrayblk =
             let allocsite = Allocsite.make_symbol deref_path in
             let stride =
@@ -486,7 +490,7 @@ module Val = struct
       | Some (CArray {deref_kind; length}) ->
           let deref_path = SPath.deref ~deref_kind path in
           let l = Loc.of_path deref_path in
-          let traces = TraceSet.singleton location (Trace.Parameter l) in
+          let traces = traces_of_loc l in
           let allocsite = Allocsite.make_symbol deref_path in
           let offset = Itv.zero in
           let size = Itv.of_int_lit length in
@@ -494,18 +498,18 @@ module Val = struct
       | Some JavaCollection ->
           let deref_path = SPath.deref ~deref_kind:Deref_ArrayIndex path in
           let l = Loc.of_path deref_path in
-          let traces = TraceSet.singleton location (Trace.Parameter l) in
+          let traces = traces_of_loc l in
           let allocsite = Allocsite.make_symbol deref_path in
           let length = Itv.of_length_path path in
           of_java_array_alloc allocsite ~length ~traces
       | None ->
           let l = Loc.of_path path in
-          let traces = TraceSet.singleton location (Trace.Parameter l) in
+          let traces = traces_of_loc l in
           of_loc ~traces l )
     | Tarray {length; stride} ->
         let deref_path = SPath.deref ~deref_kind:Deref_ArrayIndex path in
         let l = Loc.of_path deref_path in
-        let traces = TraceSet.singleton location (Trace.Parameter l) in
+        let traces = traces_of_loc l in
         let allocsite = Allocsite.make_symbol deref_path in
         let size =
           match length with
@@ -525,8 +529,14 @@ module Val = struct
           of_c_array_alloc allocsite ~stride ~offset ~size ~traces
 
 
-  let on_demand : default:t -> OndemandEnv.t -> Loc.t -> t =
+  let on_demand : default:t -> ?typ:Typ.t -> OndemandEnv.t -> Loc.t -> t =
-   fun ~default {tenv; typ_of_param_path; may_last_field; entry_location; integer_type_widths} l ->
+   fun ~default ?typ {tenv; typ_of_param_path; may_last_field; entry_location; integer_type_widths}
+       l ->
+    let do_on_demand path typ =
+      let may_last_field = may_last_field path in
+      let path = OndemandEnv.canonical_path typ_of_param_path path in
+      of_path tenv ~may_last_field integer_type_widths entry_location typ path
+    in
     match Loc.is_literal_string l with
     | Some s ->
         deref_of_literal_string s
@@ -541,14 +551,17 @@ module Val = struct
             default
         | Some path -> (
           match typ_of_param_path path with
-          | None ->
+          | None -> (
-              L.d_printfln_escaped "Val.on_demand for %a -> no type" Loc.pp l ;
+            match typ with
-              default
+            | Some typ when Loc.is_global l ->
+                L.d_printfln_escaped "Val.on_demand for %a -> global" Loc.pp l ;
+                do_on_demand path typ
+            | _ ->
+                L.d_printfln_escaped "Val.on_demand for %a -> no type" Loc.pp l ;
+                default )
           | Some typ ->
               L.d_printfln_escaped "Val.on_demand for %a" Loc.pp l ;
-              let may_last_field = may_last_field path in
+              do_on_demand path typ ) ) )
-              let path = OndemandEnv.canonical_path typ_of_param_path path in
-              of_path tenv ~may_last_field integer_type_widths entry_location typ path ) ) )
 
 
   module Itv = struct
@@ -1174,21 +1187,23 @@ module MemReach = struct
 
   let find_stack : Loc.t -> _ t0 -> Val.t = fun l m -> Option.value (find_opt l m) ~default:Val.bot
 
-  let find_heap_default : default:Val.t -> Loc.t -> _ t0 -> Val.t =
+  let find_heap_default : default:Val.t -> ?typ:Typ.t -> Loc.t -> _ t0 -> Val.t =
-   fun ~default l m ->
+   fun ~default ?typ l m ->
     IOption.value_default_f (find_opt l m) ~f:(fun () ->
-        GOption.value_map m.oenv ~default ~f:(fun oenv -> Val.on_demand ~default oenv l) )
+        GOption.value_map m.oenv ~default ~f:(fun oenv -> Val.on_demand ~default ?typ oenv l) )
+
 
+  let find_heap : ?typ:Typ.t -> Loc.t -> _ t0 -> Val.t =
+   fun ?typ l m -> find_heap_default ~default:Val.Itv.top ?typ l m
 
-  let find_heap : Loc.t -> _ t0 -> Val.t = fun l m -> find_heap_default ~default:Val.Itv.top l m
 
-  let find : Loc.t -> _ t0 -> Val.t =
+  let find : ?typ:Typ.t -> Loc.t -> _ t0 -> Val.t =
-   fun l m -> if is_stack_loc l m then find_stack l m else find_heap l m
+   fun ?typ l m -> if is_stack_loc l m then find_stack l m else find_heap ?typ l m
 
 
-  let find_set : PowLoc.t -> _ t0 -> Val.t =
+  let find_set : ?typ:Typ.t -> PowLoc.t -> _ t0 -> Val.t =
-   fun locs m ->
+   fun ?typ locs m ->
-    let find_join loc acc = Val.join acc (find loc m) in
+    let find_join loc acc = Val.join acc (find ?typ loc m) in
     PowLoc.fold find_join locs Val.bot
 
 
@@ -1267,7 +1282,7 @@ module MemReach = struct
     let transform_mem1 l m =
       let add, find =
         if is_stack_loc l m then (replace_stack, find_stack)
-        else (add_heap, find_heap_default ~default:Val.bot)
+        else (add_heap, find_heap_default ~default:Val.bot ?typ:None)
       in
       add l (f l (find l m)) m
     in
@@ -1446,8 +1461,8 @@ module Mem = struct
    fun k -> f_lift_default ~default:Val.bot (MemReach.find_stack k)
 
 
-  let find_set : PowLoc.t -> _ t0 -> Val.t =
+  let find_set : ?typ:Typ.t -> PowLoc.t -> _ t0 -> Val.t =
-   fun k -> f_lift_default ~default:Val.bot (MemReach.find_set k)
+   fun ?typ k -> f_lift_default ~default:Val.bot (MemReach.find_set ?typ k)
 
 
   let find_opt : Loc.t -> _ t0 -> Val.t option =

infer/src/bufferoverrun/bufferOverrunTrace.ml

@@ -17,6 +17,7 @@ module BoTrace = struct
   type elem =
     | ArrayDeclaration
     | Assign of PowLoc.t
+    | Global of Loc.t
     | Parameter of Loc.t
     | Through of {risky_fun: lib_fun option}
   [@@deriving compare]
@@ -78,6 +79,8 @@ module BoTrace = struct
         F.pp_print_string f "ArrayDeclaration"
     | Assign locs ->
         F.fprintf f "Assign `%a`" PowLoc.pp locs
+    | Global loc ->
+        F.fprintf f "Global `%a`" Loc.pp loc
     | Parameter loc ->
         F.fprintf f "Parameter `%a`" Loc.pp loc
     | Through {risky_fun} ->
@@ -112,7 +115,7 @@ module BoTrace = struct
   let has_unknown = final_exists ~f:(function UnknownFrom _ -> true)
 
   let elem_has_risky = function
-    | ArrayDeclaration | Assign _ | Parameter _ ->
+    | ArrayDeclaration | Assign _ | Global _ | Parameter _ ->
         false
     | Through {risky_fun} ->
         Option.is_some risky_fun
@@ -156,6 +159,8 @@ module BoTrace = struct
         "Array declaration"
     | Assign _ ->
         "Assignment"
+    | Global loc ->
+        if Loc.is_pretty loc then F.asprintf "Global `%a`" Loc.pp loc else ""
     | Parameter loc ->
         if Loc.is_pretty loc then F.asprintf "Parameter `%a`" Loc.pp loc else ""
     | Through {risky_fun} -> (

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -32,8 +32,8 @@ end
 module Exec = struct
   open ModelEnv
 
-  let load_locs id locs mem =
+  let load_locs id typ locs mem =
-    let v = Dom.Mem.find_set locs mem in
+    let v = Dom.Mem.find_set ~typ locs mem in
     let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in
     if not v.represents_multiple_values then
       match PowLoc.is_singleton_or_more locs with

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -24,7 +24,7 @@ module ModelEnv : sig
 end
 
 module Exec : sig
-  val load_locs : Ident.t -> PowLoc.t -> Dom.Mem.t -> Dom.Mem.t
+  val load_locs : Ident.t -> Typ.t -> PowLoc.t -> Dom.Mem.t -> Dom.Mem.t
 
   val decl_local : ModelEnv.model_env -> Dom.Mem.t * int -> Loc.t * Typ.t -> Dom.Mem.t * int
 

infer/tests/codetoanalyze/java/purity/GlobalTest.java

@@ -35,7 +35,7 @@ class GlobalTest {
   }
 
   // aliased_foo is aliasing a global and then is modified by incr.
-  void global_mod_via_argument_passing_bad_FP(int size, Foo f) {
+  void global_mod_via_argument_passing_bad_aliased(int size, Foo f) {
     Foo aliased_foo = foo; // Inferbo can't recognize aliasing here
     // and assumes aliased_foo is in [-oo,+oo] not in foo
     for (int i = 0; i < size; i++) {

infer/tests/codetoanalyze/java/purity/issues.exp

@@ -1,4 +1,3 @@
-codetoanalyze/java/purity/GlobalTest.java, GlobalTest.global_mod_via_argument_passing_bad_FP(int,GlobalTest$Foo):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void GlobalTest.global_mod_via_argument_passing_bad_FP(int,GlobalTest$Foo)]
 codetoanalyze/java/purity/Test.java, Test.call_pure_ok(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Test.call_pure_ok(int)]
 codetoanalyze/java/purity/Test.java, Test.emptyList_bad_FP():java.util.ArrayList, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function ArrayList Test.emptyList_bad_FP()]
 codetoanalyze/java/purity/Test.java, Test.local_alloc_ok(int,int):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int Test.local_alloc_ok(int,int)]