bufferoverrun/dune

Summary:
Main change: needed to cut the dependency of inferbo on pulse, since
pulse will need to depend on inferbo. Achieved by changing the ad-hoc
"PulseValue" into a little less ad-hoc "ForeignVariable" variant.

Reviewed By: skcho

Differential Revision: D21401816

fbshipit-source-id: bb341b9ff

infer/src/bufferoverrun/bounds.ml

@@ -317,7 +317,7 @@ module Bound = struct
 
   let of_sym : SymLinear.t -> t = fun s -> Linear (Z.zero, s)
 
-  let of_pulse_value v = of_sym (SymLinear.singleton_one (Symb.Symbol.of_pulse_value v))
+  let of_foreign_id id = of_sym (SymLinear.singleton_one (Symb.Symbol.of_foreign_id id))
 
   let of_path path_of_partial make_symbol ~unsigned ?non_int partial =
     let s = make_symbol ~unsigned ?non_int (path_of_partial partial) in

infer/src/bufferoverrun/bounds.mli

@@ -27,7 +27,7 @@ module Bound : sig
 
   val of_big_int : Z.t -> t
 
-  val of_pulse_value : PulseAbstractValue.t -> t
+  val of_foreign_id : int -> t
 
   val minf : t
 

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -432,7 +432,7 @@ let checker ({InterproceduralAnalysis.proc_desc; tenv; exe_env; analyze_dependen
   in
   let underlying_exit_node = Procdesc.get_exit_node proc_desc in
   let pp_name f = F.pp_print_string f "bufferoverrun check" in
-  NodePrinter.with_session ~pp_name underlying_exit_node ~f:(fun () ->
+  AnalysisCallbacks.html_debug_new_node_session ~pp_name underlying_exit_node ~f:(fun () ->
       let cfg = CFG.from_pdesc proc_desc in
       let checks =
         let get_checks_summary callee_pname =
@@ -440,7 +440,7 @@ let checker ({InterproceduralAnalysis.proc_desc; tenv; exe_env; analyze_dependen
           |> Option.bind ~f:(fun (_, (checker_summary, _analysis_summary)) -> checker_summary)
         in
         let get_formals callee_pname =
-          Ondemand.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals
+          AnalysisCallbacks.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals
         in
         compute_checks get_checks_summary get_formals proc_name tenv integer_type_widths cfg inv_map
       in

infer/src/bufferoverrun/dune

@@ -0,0 +1,14 @@
+; Copyright (c) Facebook, Inc. and its affiliates.
+;
+; This source code is licensed under the MIT license found in the
+; LICENSE file in the root directory of this source tree.
+
+(library
+ (name bo)
+ (public_name infer.bo)
+ (flags
+  (:standard -open Core -open OpenSource -open InferIR -open InferStdlib -open IStd -open InferGenerated
+    -open InferBase -open Absint -open Biabduction))
+ (libraries base64 core InferStdlib InferGenerated InferBase InferIR absint biabduction)
+ (preprocess (pps ppx_compare))
+)

infer/src/bufferoverrun/itv.ml

@@ -125,7 +125,7 @@ module ItvPure = struct
 
   let of_int_lit n = of_big_int (IntLit.to_big_int n)
 
-  let of_pulse_value v = of_bound (Bound.of_pulse_value v)
+  let of_foreign_id id = of_bound (Bound.of_foreign_id id)
 
   let mone = of_bound Bound.mone
 

infer/src/bufferoverrun/itv.mli

@@ -108,7 +108,7 @@ module ItvPure : sig
 
   val of_int_lit : IntLit.t -> t
 
-  val of_pulse_value : PulseAbstractValue.t -> t
+  val of_foreign_id : int -> t
 
   val get_bound : t -> Symb.BoundEnd.t -> Bound.t
 

infer/src/bufferoverrun/symb.ml

@@ -287,7 +287,7 @@ module Symbol = struct
   (* NOTE: non_int represents the symbols that are not integer type,
      so that their ranges are not used in the cost checker. *)
   type t =
-    | PulseValue of PulseAbstractValue.t
+    | ForeignVariable of {id: int}
     | OneValue of {unsigned: extra_bool; non_int: extra_bool; path: SymbolPath.t}
     | BoundEnd of
         {unsigned: extra_bool; non_int: extra_bool; path: SymbolPath.t; bound_end: BoundEnd.t}
@@ -296,15 +296,15 @@ module Symbol = struct
   let pp : F.formatter -> t -> unit =
    fun fmt s ->
     match s with
-    | PulseValue v ->
+    | ForeignVariable {id} ->
-        PulseAbstractValue.pp fmt v
+        F.fprintf fmt "v%d" id
     | OneValue {unsigned; non_int; path} | BoundEnd {unsigned; non_int; path} ->
         SymbolPath.pp fmt path ;
         ( if Config.developer_mode then
           match s with
           | BoundEnd {bound_end} ->
               Format.fprintf fmt ".%s" (BoundEnd.to_string bound_end)
-          | PulseValue _ | OneValue _ ->
+          | ForeignVariable _ | OneValue _ ->
               () ) ;
         if Config.bo_debug > 1 then
           F.fprintf fmt "(%c%s)" (if unsigned then 'u' else 's') (if non_int then "n" else "")
@@ -312,12 +312,12 @@ module Symbol = struct
 
   let compare s1 s2 =
     match (s1, s2) with
-    | PulseValue _, (OneValue _ | BoundEnd _) ->
+    | ForeignVariable _, (OneValue _ | BoundEnd _) ->
         -1
-    | (OneValue _ | BoundEnd _), PulseValue _ ->
+    | (OneValue _ | BoundEnd _), ForeignVariable _ ->
         1
-    | PulseValue x, PulseValue y ->
+    | ForeignVariable {id= x}, ForeignVariable {id= y} ->
-        PulseAbstractValue.compare x y
+        compare_int x y
     | OneValue _, BoundEnd _ ->
         -1
     | BoundEnd _, OneValue _ ->
@@ -337,7 +337,8 @@ module Symbol = struct
 
   let paths_equal s1 s2 =
     match (s1, s2) with
-    | PulseValue _, _ | _, PulseValue _ | OneValue _, BoundEnd _ | BoundEnd _, OneValue _ ->
+    | ForeignVariable _, _ | _, ForeignVariable _ | OneValue _, BoundEnd _ | BoundEnd _, OneValue _
+      ->
         false
     | OneValue {path= path1}, OneValue {path= path2} | BoundEnd {path= path1}, BoundEnd {path= path2}
       ->
@@ -354,46 +355,51 @@ module Symbol = struct
    fun bound_end ~unsigned ?(non_int = false) path -> BoundEnd {unsigned; non_int; path; bound_end}
 
 
-  let of_pulse_value v = PulseValue v
-
   let pp_mark ~markup = if markup then MarkupFormatter.wrap_monospaced pp else pp
 
   let is_unsigned : t -> bool = function
-    | PulseValue _ ->
+    | ForeignVariable _ ->
         false
     | OneValue {unsigned} | BoundEnd {unsigned} ->
         unsigned
 
 
   let is_non_int : t -> bool = function
-    | PulseValue _ ->
+    | ForeignVariable _ ->
         false
     | OneValue {non_int} | BoundEnd {non_int} ->
         non_int
 
 
   let is_global : t -> bool = function
-    | PulseValue _ ->
+    | ForeignVariable _ ->
         false
     | OneValue {path} | BoundEnd {path} ->
         SymbolPath.is_global path
 
 
-  let get_pulse_value_exn : t -> PulseAbstractValue.t = function
+  let of_foreign_id id = ForeignVariable {id}
-    | PulseValue v ->
+
-        v
+  let get_foreign_id_exn : t -> int = function
+    | ForeignVariable {id} ->
+        id
     | OneValue _ | BoundEnd _ ->
         assert false
 
 
   (* This should be called on non-pulse bound as of now. *)
-  let path = function PulseValue _ -> assert false | OneValue {path} | BoundEnd {path} -> path
+  let path = function
+    | ForeignVariable _ ->
+        assert false
+    | OneValue {path} | BoundEnd {path} ->
+        path
+
 
   (* NOTE: This may not be satisfied in the cost checker for simplifying its results. *)
   let check_bound_end s be =
     if Config.bo_debug >= 3 then
       match s with
-      | PulseValue _ | OneValue _ ->
+      | ForeignVariable _ | OneValue _ ->
           ()
       | BoundEnd {bound_end} ->
           if not (BoundEnd.equal be bound_end) then
@@ -403,7 +409,7 @@ module Symbol = struct
 
 
   let exists_str ~f = function
-    | PulseValue _ ->
+    | ForeignVariable _ ->
         false
     | OneValue {path} | BoundEnd {path} ->
         SymbolPath.exists_str ~f path

infer/src/bufferoverrun/symb.mli

@@ -121,11 +121,14 @@ module Symbol : sig
 
   val make_boundend : BoundEnd.t -> make_t
 
-  val of_pulse_value : PulseAbstractValue.t -> t
-
   val exists_str : f:(string -> bool) -> t -> bool
 
-  val get_pulse_value_exn : t -> PulseAbstractValue.t
+  val of_foreign_id : int -> t
+  (** make a symbol out of any type of variables that can be represented by their [int] id *)
+
+  val get_foreign_id_exn : t -> int
+  (** Return the [int] id of the foreign variable represented by the symbol. Will fail if called on
+      a symbol not created with [of_foreign_id]. *)
 end
 
 module SymbolSet : sig

infer/src/deadcode/Makefile

@@ -50,8 +50,8 @@ endif
 # Note that we run find under _build directory. Since we copy some
 # sources from subfolders to src/ folder to avoid duplicates we use
 # $(DEPTH_ONE) and iteration over main and library folders.
-LIBRARY_FOLDERS = . ./IR ./absint ./atd ./base ./biabduction ./c_stubs ./istd ./nullsafe ./scripts
+LIBRARY_FOLDERS = . ./IR ./absint ./atd ./base ./biabduction ./bufferoverrun ./c_stubs ./istd ./nullsafe ./scripts
-INCLUDE_FOLDERS = -I absint -I IR -I atd -I base -I biabduction -I c_stubs -I istd -I nullsafe -I scripts
+INCLUDE_FOLDERS = -I absint -I IR -I atd -I base -I biabduction -I bufferoverrun -I c_stubs -I istd -I nullsafe -I scripts
 
 ml_src_files:=$(shell \
 	cd $(INFER_BUILD_DIR); \

infer/src/dune.in

@@ -13,7 +13,6 @@ let source_dirs =
   (if clang then ["al"; "clang"; "unit" ^/ "clang"] else ["clang_stubs"; "unit" ^/ "clang_stubs"])
   @ [ (if java then "java" else "java_stubs")
     ; "backend"
-    ; "bufferoverrun"
     ; "checkers"
     ; "concurrency"
     ; "cost"
@@ -56,6 +55,8 @@ let infer_cflags =
   ; "-open"
   ; "Biabduction"
   ; "-open"
+  ; "Bo"
+  ; "-open"
   ; "Nullsafe"
   ; "-open"
   ; "Absint"
@@ -90,7 +91,7 @@ let main_lib_stanza =
 |}
     infer_cflags
     (String.concat " "
-       ("biabduction" :: "nullsafe" :: "absint" :: "InferCStubs" :: "InferIR" :: common_libraries))
+       (common_libraries @ ["InferIR"; "InferCStubs"; "absint"; "biabduction"; "nullsafe"; "bo"]))
     (String.concat " " infer_binaries)
 
 

infer/src/pulse/PulsePathCondition.ml

@@ -15,8 +15,12 @@ module ValueHistory = PulseValueHistory
 module BoItvs = struct
   include PrettyPrintable.MakePPMonoMap (AbstractValue) (Itv.ItvPure)
 
-  let find_or_default v bo_itvs =
+  let find_or_default (v : AbstractValue.t) bo_itvs =
-    match find_opt v bo_itvs with Some bo_itv -> bo_itv | None -> Itv.ItvPure.of_pulse_value v
+    match find_opt v bo_itvs with
+    | Some bo_itv ->
+        bo_itv
+    | None ->
+        Itv.ItvPure.of_foreign_id (v :> int)
 end
 
 module CItvs = PrettyPrintable.MakePPMonoMap (AbstractValue) (CItv)
@@ -88,14 +92,14 @@ let subst_find_or_new subst addr_callee =
 
 
 let eval_sym_of_subst bo_itvs subst s bound_end =
-  let v = Symb.Symbol.get_pulse_value_exn s in
+  let v = Symb.Symbol.get_foreign_id_exn s |> AbstractValue.of_id in
   match AbstractValue.Map.find_opt v !subst with
   | Some (v', _) ->
       Itv.ItvPure.get_bound (BoItvs.find_or_default v' bo_itvs) bound_end
   | None ->
       let v' = AbstractValue.mk_fresh () in
       subst := AbstractValue.Map.add v (v', []) !subst ;
-      Bounds.Bound.of_pulse_value v'
+      Bounds.Bound.of_foreign_id (v' :> int)
 
 
 exception Contradiction