[inferbo] Add trace on make_sym

Summary: It adds traces on the make_sym function.

Reviewed By: ezgicicek, mbouaziz

Differential Revision: D9193802

fbshipit-source-id: 13183e6af

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -48,16 +48,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         match typ.Typ.desc with
         | Typ.Tint ikind ->
             let unsigned = Typ.ikind_is_unsigned ikind in
-            let v =
+            let v = Dom.Val.make_sym ~unsigned loc pname symbol_table path new_sym_num location in
-              Dom.Val.make_sym ~unsigned loc pname symbol_table path new_sym_num
-              |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
-            in
             mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
         | Typ.Tfloat _ ->
-            let v =
+            let v = Dom.Val.make_sym loc pname symbol_table path new_sym_num location in
-              Dom.Val.make_sym loc pname symbol_table path new_sym_num
-              |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
-            in
             mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
         | Typ.Tptr (typ, _) when Language.curr_language_is Java && not (Typ.is_array typ) ->
             BoUtils.Exec.decl_sym_java_ptr

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -65,9 +65,7 @@ module Val = struct
 
   let unknown_from : callee_pname:_ -> location:_ -> t =
    fun ~callee_pname ~location ->
-    let traces =
+    let traces = TraceSet.singleton (Trace.UnknownFrom (callee_pname, location)) in
-      Trace.UnknownFrom (callee_pname, location) |> Trace.singleton |> TraceSet.singleton
-    in
     unknown ~traces
 
 
@@ -148,11 +146,12 @@ module Val = struct
 
   let make_sym
       : ?unsigned:bool -> Loc.t -> Typ.Procname.t -> Itv.SymbolTable.t -> Itv.SymbolPath.partial
-        -> Itv.Counter.t -> t =
+        -> Itv.Counter.t -> Location.t -> t =
-   fun ?(unsigned= false) loc pname symbol_table path new_sym_num ->
+   fun ?(unsigned= false) loc pname symbol_table path new_sym_num location ->
     { bot with
       itv= Itv.make_sym ~unsigned pname symbol_table (Itv.SymbolPath.normal path) new_sym_num
-    ; sym= Relation.Sym.of_loc loc }
+    ; sym= Relation.Sym.of_loc loc
+    ; traces= TraceSet.singleton (Trace.SymAssign (loc, location)) }
 
 
   let unknown_bit : t -> t = fun x -> {x with itv= Itv.top; sym= Relation.Sym.top}

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -207,7 +207,7 @@ let set_array_length array length_exp =
 
 module Split = struct
   let std_vector ~adds_at_least_one (vector_exp, vector_typ) location mem =
-    let traces = BufferOverrunTrace.(Call location |> singleton |> Set.singleton) in
+    let traces = BufferOverrunTrace.(Set.singleton (Call location)) in
     let increment_itv = if adds_at_least_one then Itv.pos else Itv.nat in
     let increment = Dom.Val.of_itv ~traces increment_itv in
     let vector_type_name = Option.value_exn (vector_typ |> Typ.strip_ptr |> Typ.name) in

infer/src/bufferoverrun/bufferOverrunTrace.ml

@@ -74,9 +74,9 @@ module Set = struct
 
   let choose_shortest set = min_elt set
 
-  let add_elem elem t =
+  let singleton elem = singleton (BoTrace.singleton elem)
-    if is_empty t then singleton (BoTrace.singleton elem) else map (BoTrace.add_elem elem) t
 
+  let add_elem elem t = if is_empty t then singleton elem else map (BoTrace.add_elem elem) t
 
   let instantiate ~traces_caller ~traces_callee location =
     if is_empty traces_caller then