From a34e1a87597261ff540e575bd248d64241294df0 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 6 May 2020 11:23:23 -0700 Subject: [PATCH] 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 | 2 +- infer/src/bufferoverrun/bounds.mli | 2 +- .../src/bufferoverrun/bufferOverrunChecker.ml | 4 +- infer/src/bufferoverrun/dune | 14 ++++++ infer/src/bufferoverrun/itv.ml | 2 +- infer/src/bufferoverrun/itv.mli | 2 +- infer/src/bufferoverrun/symb.ml | 46 +++++++++++-------- infer/src/bufferoverrun/symb.mli | 9 ++-- infer/src/deadcode/Makefile | 4 +- infer/src/dune.in | 5 +- infer/src/pulse/PulsePathCondition.ml | 12 +++-- 11 files changed, 65 insertions(+), 37 deletions(-) create mode 100644 infer/src/bufferoverrun/dune diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 0abd97801..fe1d92cd8 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index 8b165998e..88021ca07 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 345ee42c8..eba30cafe 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 diff --git a/infer/src/bufferoverrun/dune b/infer/src/bufferoverrun/dune new file mode 100644 index 000000000..c383edbb7 --- /dev/null +++ b/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)) +) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index a09aa9e5e..455e86d1b 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/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 diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index ba298251f..213aac9ae 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/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 diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index 12a0c386b..69d0ed019 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/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 -> - PulseAbstractValue.pp fmt v + | ForeignVariable {id} -> + 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 -> - PulseAbstractValue.compare x y + | ForeignVariable {id= x}, ForeignVariable {id= 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 - | PulseValue v -> - v + let of_foreign_id id = ForeignVariable {id} + + 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 diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index 26f0a3575..c24c4150c 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/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 diff --git a/infer/src/deadcode/Makefile b/infer/src/deadcode/Makefile index 0f23644bf..44bf8f114 100644 --- a/infer/src/deadcode/Makefile +++ b/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 -INCLUDE_FOLDERS = -I absint -I IR -I atd -I base -I biabduction -I c_stubs -I istd -I nullsafe -I 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 bufferoverrun -I c_stubs -I istd -I nullsafe -I scripts ml_src_files:=$(shell \ cd $(INFER_BUILD_DIR); \ diff --git a/infer/src/dune.in b/infer/src/dune.in index 32af18cef..dab9a0bab 100644 --- a/infer/src/dune.in +++ b/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) diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml index d6f1e0e2d..59b681c3b 100644 --- a/infer/src/pulse/PulsePathCondition.ml +++ b/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 = - match find_opt v bo_itvs with Some bo_itv -> bo_itv | None -> Itv.ItvPure.of_pulse_value v + 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_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