diff --git a/CONTRIBUTORS b/CONTRIBUTORS new file mode 100644 index 000000000..c7383172e --- /dev/null +++ b/CONTRIBUTORS @@ -0,0 +1,3 @@ +Kihong Heo +Sungkeun Cho +Kwangkeun Yi diff --git a/Makefile b/Makefile index ed72416ac..8a39e654d 100644 --- a/Makefile +++ b/Makefile @@ -38,7 +38,7 @@ endif DIRECT_TESTS= ifeq ($(BUILD_C_ANALYZERS),yes) -DIRECT_TESTS += c_errors c_frontend cpp_checkers cpp_errors cpp_frontend cpp_quandary +DIRECT_TESTS += c_errors c_frontend c_bufferoverrun cpp_checkers cpp_errors cpp_frontend cpp_quandary endif ifeq ($(BUILD_JAVA_ANALYZERS),yes) DIRECT_TESTS += \ diff --git a/infer/src/IR/Localise.ml b/infer/src/IR/Localise.ml index e888d5c9f..acf299734 100644 --- a/infer/src/IR/Localise.ml +++ b/infer/src/IR/Localise.ml @@ -32,6 +32,7 @@ let analysis_stops = "ANALYSIS_STOPS" let array_out_of_bounds_l1 = "ARRAY_OUT_OF_BOUNDS_L1" let array_out_of_bounds_l2 = "ARRAY_OUT_OF_BOUNDS_L2" let array_out_of_bounds_l3 = "ARRAY_OUT_OF_BOUNDS_L3" +let buffer_overrun = "BUFFER_OVERRUN" let class_cast_exception = "CLASS_CAST_EXCEPTION" let comparing_floats_for_equality = "COMPARING_FLOAT_FOR_EQUALITY" let condition_is_assignment = "CONDITION_IS_ASSIGNMENT" @@ -718,6 +719,10 @@ let desc_leak hpred_type_opt value_str_opt resource_opt resource_action_opt loc { no_desc with descriptions = bucket_str :: xxx_allocated_to @ by_call_to @ is_not_rxxx_after; tags = !tags } +let desc_buffer_overrun bucket desc = + let err_desc = { no_desc with descriptions = [desc]; } in + error_desc_set_bucket err_desc bucket Config.show_buckets + (** kind of precondition not met *) type pnm_kind = | Pnm_bounds diff --git a/infer/src/IR/Localise.mli b/infer/src/IR/Localise.mli index 08e721672..627cad693 100644 --- a/infer/src/IR/Localise.mli +++ b/infer/src/IR/Localise.mli @@ -30,6 +30,7 @@ val analysis_stops : t val array_out_of_bounds_l1 : t val array_out_of_bounds_l2 : t val array_out_of_bounds_l3 : t +val buffer_overrun : t val class_cast_exception : t val comparing_floats_for_equality : t val condition_is_assignment : t @@ -214,6 +215,8 @@ val desc_leak : Exp.t option -> string option -> PredSymb.resource option -> PredSymb.res_action option -> Location.t -> string option -> error_desc +val desc_buffer_overrun : string -> string -> error_desc + val desc_null_test_after_dereference : string -> int -> Location.t -> error_desc val java_unchecked_exn_desc : Procname.t -> Typename.t -> string -> error_desc diff --git a/infer/src/IR/Procdesc.re b/infer/src/IR/Procdesc.re index effc716a7..556d93abc 100644 --- a/infer/src/IR/Procdesc.re +++ b/infer/src/IR/Procdesc.re @@ -294,7 +294,8 @@ type t = { mutable nodes: list Node.t, /** list of nodes of this procedure */ mutable nodes_num: int, /** number of nodes */ mutable start_node: Node.t, /** start node of this procedure */ - mutable exit_node: Node.t /** exit node of ths procedure */ + mutable exit_node: Node.t, /** exit node of ths procedure */ + mutable loop_heads: option NodeSet.t /** loop head nodes of this procedure */ } [@@deriving compare]; @@ -307,7 +308,7 @@ let from_proc_attributes called_from_cfg::called_from_cfg attributes => { let pname_opt = Some attributes.ProcAttributes.proc_name; let start_node = Node.dummy pname_opt; let exit_node = Node.dummy pname_opt; - {attributes, nodes: [], nodes_num: 0, start_node, exit_node} + {attributes, nodes: [], nodes_num: 0, start_node, exit_node, loop_heads: None} }; @@ -518,3 +519,41 @@ let node_set_succs_exn pdesc (node: Node.t) succs exn => set_succs_exn_base node' [exit_node] exn | _ => set_succs_exn_base node succs exn }; + + +/** Get loop heads for widening. + It collects all target nodes of back-edges in a depth-first + traversal. + */ +let get_loop_heads pdesc => { + let rec set_loop_head_rec visited heads wl => + switch wl { + | [] => heads + | [(n, ancester), ...wl'] => + if (NodeSet.mem n visited) { + if (NodeSet.mem n ancester) { + set_loop_head_rec visited (NodeSet.add n heads) wl' + } else { + set_loop_head_rec visited heads wl' + } + } else { + let ancester = NodeSet.add n ancester; + let succs = IList.append (Node.get_succs n) (Node.get_exn n); + let works = IList.map (fun m => (m, ancester)) succs; + set_loop_head_rec (NodeSet.add n visited) heads (IList.append works wl') + } + }; + let start_wl = [(get_start_node pdesc, NodeSet.empty)]; + let lh = set_loop_head_rec NodeSet.empty NodeSet.empty start_wl; + pdesc.loop_heads = Some lh; + lh +}; + +let is_loop_head pdesc (node: Node.t) => { + let lh = + switch pdesc.loop_heads { + | Some lh => lh + | None => get_loop_heads pdesc + }; + NodeSet.mem node lh +}; diff --git a/infer/src/IR/Procdesc.rei b/infer/src/IR/Procdesc.rei index 5e7449b7d..8ed820db4 100644 --- a/infer/src/IR/Procdesc.rei +++ b/infer/src/IR/Procdesc.rei @@ -166,6 +166,10 @@ let fold_calls: ('a => (Procname.t, Location.t) => 'a) => 'a => t => 'a; let fold_instrs: ('a => Node.t => Sil.instr => 'a) => 'a => t => 'a; +/** fold over all nodes */ +let fold_nodes: ('a => Node.t => 'a) => 'a => t => 'a; + + /** Only call from Cfg. */ let from_proc_attributes: called_from_cfg::bool => ProcAttributes.t => t; @@ -274,3 +278,5 @@ let set_start_node: t => Node.t => unit; /** indicate that we have performed preanalysis on the CFG assoociated with [t] */ let signal_did_preanalysis: t => unit; + +let is_loop_head: t => Node.t => bool; diff --git a/infer/src/Makefile b/infer/src/Makefile index 43e9667b3..90acc88a1 100644 --- a/infer/src/Makefile +++ b/infer/src/Makefile @@ -121,7 +121,7 @@ else EXTRA_DEPS = opensource endif -DEPENDENCIES = IR backend base checkers eradicate harness integration tp/fts quandary $(EXTRA_DEPS) +DEPENDENCIES = IR backend base checkers eradicate harness integration tp/fts quandary bufferoverrun $(EXTRA_DEPS) # ocamlbuild command with options common to all build targets OCAMLBUILD_BASE = rebuild $(OCAMLBUILD_OPTIONS) -j $(NCPU) $(addprefix -I , $(DEPENDENCIES)) diff --git a/infer/src/backend/InferPrint.re b/infer/src/backend/InferPrint.re index 7ebd5d4e2..1fd26bce6 100644 --- a/infer/src/backend/InferPrint.re +++ b/infer/src/backend/InferPrint.re @@ -316,6 +316,7 @@ let should_report (issue_kind: Exceptions.err_kind) issue_type error_desc eclass | Checkers | Eradicate | Tracing => true + | Bufferoverrun | Capture | Compile | Crashcontext @@ -347,7 +348,8 @@ let should_report (issue_kind: Exceptions.err_kind) issue_type error_desc eclass ]; IList.mem Localise.equal issue_type null_deref_issue_types }; - if issue_type_is_null_deref { + let issue_type_is_buffer_overrun = Localise.equal issue_type Localise.buffer_overrun; + if (issue_type_is_null_deref || issue_type_is_buffer_overrun) { let issue_bucket_is_high = { let issue_bucket = Localise.error_desc_get_bucket error_desc; let high_buckets = Localise.BucketLevel.[b1, b2]; diff --git a/infer/src/backend/infer.ml b/infer/src/backend/infer.ml index a17a4f1f8..e7e51cbf1 100644 --- a/infer/src/backend/infer.ml +++ b/infer/src/backend/infer.ml @@ -319,7 +319,7 @@ let analyze driver_mode = false, false | _, (Capture | Compile) -> false, false - | _, (Infer | Eradicate | Checkers | Tracing | Crashcontext | Quandary | Threadsafety) -> + | _, (Infer | Eradicate | Checkers | Tracing | Crashcontext | Quandary | Threadsafety | Bufferoverrun) -> true, true | _, Linters -> false, true in diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 6360de9ef..cc24616fb 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -327,6 +327,7 @@ type payload = quandary : QuandarySummary.t option; siof : SiofDomain.astate option; threadsafety : ThreadSafetyDomain.summary option; + buffer_overrun : BufferOverrunDomain.Summary.t option; } type summary = @@ -455,17 +456,18 @@ let pp_summary_no_stats_specs fmt summary = F.fprintf fmt "%a@\n" pp_pair (describe_phase summary); F.fprintf fmt "Dependency_map: @[%a@]@\n" pp_dependency_map summary.dependency_map -let pp_payload pe fmt { preposts; typestate; crashcontext_frame; quandary; siof; threadsafety } = +let pp_payload pe fmt { preposts; typestate; crashcontext_frame; quandary; siof; threadsafety; buffer_overrun } = let pp_opt pp fmt = function | Some x -> pp fmt x | None -> () in - F.fprintf fmt "%a%a%a%a%a%a@\n" + F.fprintf fmt "%a%a%a%a%a%a%a@\n" (pp_specs pe) (get_specs_from_preposts preposts) (pp_opt (TypeState.pp TypeState.unit_ext)) typestate (pp_opt Crashcontext.pp_stacktree) crashcontext_frame (pp_opt QuandarySummary.pp) quandary (pp_opt SiofDomain.pp) siof (pp_opt ThreadSafetyDomain.pp_summary) threadsafety + (pp_opt BufferOverrunDomain.Summary.pp) buffer_overrun let pp_summary_text ~whole_seconds fmt summary = @@ -753,6 +755,7 @@ let empty_payload = quandary = None; siof = None; threadsafety = None; + buffer_overrun = None; } (** [init_summary (depend_list, nodes, diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index be5dbb479..3f7d1d3f0 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -136,6 +136,7 @@ type payload = quandary : QuandarySummary.t option; siof : SiofDomain.astate option; threadsafety : ThreadSafetyDomain.summary option; + buffer_overrun : BufferOverrunDomain.Summary.t option; } (** Procedure summary *) diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 382189ef6..c2c13b3c6 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -18,8 +18,9 @@ module CLOpt = CommandLineOption module F = Format -type analyzer = Capture | Compile | Infer | Eradicate | Checkers | Tracing - | Crashcontext | Linters | Quandary | Threadsafety [@@deriving compare] +type analyzer = + Capture | Compile | Infer | Eradicate | Checkers | Tracing | Crashcontext | Linters | Quandary + | Threadsafety | Bufferoverrun [@@deriving compare] let equal_analyzer = [%compare.equal : analyzer] @@ -27,7 +28,8 @@ let string_to_analyzer = [("capture", Capture); ("compile", Compile); ("infer", Infer); ("eradicate", Eradicate); ("checkers", Checkers); ("tracing", Tracing); ("crashcontext", Crashcontext); ("linters", Linters); - ("quandary", Quandary); ("threadsafety", Threadsafety)] + ("quandary", Quandary); ("threadsafety", Threadsafety); + ("bufferoverrun", Bufferoverrun)] let string_of_analyzer a = IList.find (fun (_, a') -> equal_analyzer a a') string_to_analyzer |> fst @@ -449,11 +451,11 @@ and analyzer = (* NOTE: if compilation fails here, it means you have added a new analyzer without updating the documentation of this option *) | Capture | Compile | Infer | Eradicate | Checkers | Tracing | Crashcontext | Linters - | Quandary | Threadsafety -> () in + | Quandary | Threadsafety | Bufferoverrun -> () in CLOpt.mk_symbol_opt ~deprecated:["analyzer"] ~long:"analyzer" ~short:"a" ~exes:CLOpt.[Driver] "Specify which analyzer to run (only one at a time is supported):\n\ - - infer, eradicate, checkers, quandary, threadsafety: run the specified analysis\n\ + - infer, eradicate, checkers, quandary, threadsafety, bufferoverrun: run the specified analysis\n\ - capture: run capture phase only (no analysis)\n\ - compile: run compilation command without interfering (not supported by all frontends)\n\ - crashcontext, tracing: experimental (see --crashcontext and --tracing)\n\ @@ -490,6 +492,10 @@ and bootclasspath = ~exes:CLOpt.[Driver] "Specify the Java bootclasspath" +and bo_debug = + CLOpt.mk_int ~default:0 ~long:"bo-debug" + ~exes:CLOpt.[Driver] "Debug mode for buffer-overrun checker" + (** Automatically set when running from within Buck *) and buck = CLOpt.mk_bool ~long:"buck" @@ -548,7 +554,7 @@ and check_duplicate_symbols = ~exes:CLOpt.[Analyze] "Check if a symbol with the same name is defined in more than one file." -and checkers, crashcontext, eradicate, quandary, threadsafety = +and checkers, crashcontext, eradicate, quandary, threadsafety, bufferoverrun = let checkers = CLOpt.mk_bool ~deprecated:["checkers"] ~long:"checkers" "Activate the checkers instead of the full analysis" @@ -573,7 +579,12 @@ and checkers, crashcontext, eradicate, quandary, threadsafety = "Activate the thread safety analysis" [checkers] [] in - (checkers, crashcontext, eradicate, quandary, threadsafety) + let bufferoverrun = + CLOpt.mk_bool_group ~deprecated:["bufferoverrun"] ~long:"bufferoverrn" + "Activate the buffer overrun analysis" + [checkers] [] + in + (checkers, crashcontext, eradicate, quandary, threadsafety, bufferoverrun) and checkers_repeated_calls = CLOpt.mk_bool ~long:"checkers-repeated-calls" @@ -1352,6 +1363,7 @@ let post_parsing_initialization () = | Some Eradicate -> checkers := true; eradicate := true | Some Quandary -> checkers := true; quandary := true | Some Threadsafety -> checkers := true; threadsafety := true + | Some Bufferoverrun -> checkers := true; bufferoverrun := true | Some Tracing -> tracing := true | Some (Capture | Compile | Infer | Linters) | None -> () @@ -1387,9 +1399,11 @@ and array_level = !array_level and ast_file = !ast_file and blacklist = !blacklist and bootclasspath = !bootclasspath +and bo_debug = !bo_debug and buck = !buck and buck_build_args = !buck_build_args and buck_out = !buck_out +and bufferoverrun = !bufferoverrun and bugs_csv = !bugs_csv and bugs_json = !bugs_json and frontend_tests = !frontend_tests diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index eceb79f59..5d5e3a7c6 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -15,8 +15,9 @@ open! IStd (** Various kind of analyzers *) -type analyzer = Capture | Compile | Infer | Eradicate | Checkers | Tracing - | Crashcontext | Linters | Quandary | Threadsafety [@@deriving compare] +type analyzer = + Capture | Compile | Infer | Eradicate | Checkers | Tracing | Crashcontext | Linters | Quandary + | Threadsafety | Bufferoverrun [@@deriving compare] val equal_analyzer : analyzer -> analyzer -> bool @@ -149,9 +150,11 @@ val array_level : int val ast_file : string option val blacklist : string option val bootclasspath : string option +val bo_debug : int val buck : bool val buck_build_args : string list val buck_out : string option +val bufferoverrun : bool val bugs_csv : string option val bugs_json : string option val bugs_tests : string option diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml new file mode 100644 index 000000000..8b350c858 --- /dev/null +++ b/infer/src/bufferoverrun/absLoc.ml @@ -0,0 +1,76 @@ +(* + * Copyright (c) 2016 - present + * + * Programming Research Laboratory (ROPAS) + * Seoul National University, Korea + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +module F = Format + +module Allocsite = +struct + include String + let pp fmt s = Format.fprintf fmt "%s" s + let make x = x +end + +module Loc = +struct + type t = + | Var of Var.t + | Allocsite of Allocsite.t + | Field of t * Ident.fieldname + [@@deriving compare] + + let rec pp fmt = function + | Var v -> + Var.pp F.str_formatter v; + let s = F.flush_str_formatter () in + if s.[0] = '&' then + F.fprintf fmt "%s" (String.sub s 1 (String.length s - 1)) + else F.fprintf fmt "%s" s + | Allocsite a -> Allocsite.pp fmt a + | Field (l, f) -> F.fprintf fmt "%a.%a" pp l Ident.pp_fieldname f + let is_var = function Var _ -> true | _ -> false + let is_pvar_in_reg v = + Var.pp F.str_formatter v; + let s = F.flush_str_formatter () in + s.[0] = '&' + let is_logical_var = function + | Var (Var.LogicalVar _) -> true + | _ -> false + let of_var v = Var v + let of_allocsite a = Allocsite a + let of_pvar pvar = Var (Var.of_pvar pvar) + let of_id id = Var (Var.of_id id) + let append_field l f = Field (l, f) + + let is_return = function + | Var (Var.ProgramVar x) -> + Mangled.equal (Pvar.get_name x) Ident.name_return + | _ -> false +end + +module PowLoc = +struct + include AbstractDomain.FiniteSet + (struct + include Set.Make (struct type t = Loc.t [@@deriving compare] end) + let pp_element fmt e = Loc.pp fmt e + let pp fmt s = + Format.fprintf fmt "{"; + iter (fun e -> Format.fprintf fmt "%a," pp_element e) s; + Format.fprintf fmt "}" + end) + + let bot = empty + + let of_pvar pvar = singleton (Loc.of_pvar pvar) + let of_id id = singleton (Loc.of_id id) + let append_field ploc fn = fold (fun l -> add (Loc.append_field l fn)) ploc empty +end diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml new file mode 100644 index 000000000..29afdcaa3 --- /dev/null +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -0,0 +1,199 @@ +(* + * Copyright (c) 2016 - present + * + * Programming Research Laboratory (ROPAS) + * Seoul National University, Korea + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +(* Abstract Array Block *) +open! IStd +open AbsLoc + +module ArrInfo = +struct + type t = + { offset : Itv.t; + size : Itv.t; + stride : Itv.t; } + [@@deriving compare] + + type astate = t + + let bot : t + = { offset = Itv.bot; size = Itv.bot; stride = Itv.bot; } + + let initial : t + = bot + + let top : t + = { offset = Itv.top; size = Itv.top; stride = Itv.top; } + + let input : t + = { offset = Itv.zero; size = Itv.pos; stride = Itv.one; } + + let make : Itv.t * Itv.t * Itv.t -> t + = fun (o, s, stride) -> { offset = o; size = s; stride = stride; } + + let join : t -> t -> t + = fun a1 a2 -> + if phys_equal a1 a2 then a2 else + { offset = Itv.join a1.offset a2.offset; + size = Itv.join a1.size a2.size; + stride = Itv.join a1.stride a2.stride; } + + let widen : prev:t -> next:t -> num_iters:int -> t + = fun ~prev ~next ~num_iters -> + if phys_equal prev next then next else + { offset = Itv.widen ~prev:prev.offset ~next:next.offset ~num_iters; + size = Itv.widen ~prev:prev.size ~next:next.size ~num_iters; + stride = Itv.widen ~prev:prev.stride ~next:next.stride ~num_iters; } + + let eq : t -> t -> bool + = fun a1 a2 -> + if phys_equal a1 a2 then true else + Itv.eq a1.offset a2.offset + && Itv.eq a1.size a2.size + && Itv.eq a1.stride a2.stride + + let (<=) : lhs:t -> rhs:t -> bool + = fun ~lhs ~rhs -> + if phys_equal lhs rhs then true else + Itv.le ~lhs:lhs.offset ~rhs:rhs.offset + && Itv.le ~lhs:lhs.size ~rhs:rhs.size + && Itv.le ~lhs:lhs.stride ~rhs:rhs.stride + + let weak_plus_size : t -> Itv.t -> t + = fun arr i -> { arr with size = Itv.join arr.size (Itv.plus i arr.size) } + + let plus_offset : t -> Itv.t -> t + = fun arr i -> { arr with offset = Itv.plus arr.offset i } + + let minus_offset : t -> Itv.astate -> t + = fun arr i -> { arr with offset = Itv.minus arr.offset i } + + let diff : t -> t -> Itv.astate + = fun arr1 arr2 -> + let i1 = Itv.mult arr1.offset arr1.stride in + let i2 = Itv.mult arr2.offset arr2.stride in + Itv.minus i1 i2 + + let subst : t -> Itv.Bound.t Itv.SubstMap.t -> t + = fun arr subst_map -> + { arr with offset = Itv.subst arr.offset subst_map; + size = Itv.subst arr.size subst_map; } + + let pp : Format.formatter -> t -> unit + = fun fmt arr -> + Format.fprintf fmt "offset : %a, size : %a" + Itv.pp arr.offset Itv.pp arr.size + + let get_symbols : t -> Itv.Symbol.t list + = fun arr -> + let s1 = Itv.get_symbols arr.offset in + let s2 = Itv.get_symbols arr.size in + let s3 = Itv.get_symbols arr.stride in + IList.flatten [s1; s2; s3] + + let normalize : t -> t + = fun arr -> + { offset = Itv.normalize arr.offset; + size = Itv.normalize arr.size; + stride = Itv.normalize arr.stride } + + let prune_comp : Binop.t -> t -> t -> t + = fun c arr1 arr2 -> + { arr1 with offset = Itv.prune_comp c arr1.offset arr2.offset } + + let prune_eq : t -> t -> t + = fun arr1 arr2 -> { arr1 with offset = Itv.prune_eq arr1.offset arr2.offset } + + let prune_ne : t -> t -> t + = fun arr1 arr2 -> { arr1 with offset = Itv.prune_ne arr1.offset arr2.offset } +end + +module PPMap = +struct + include PrettyPrintable.MakePPMap (struct + include Allocsite + let pp_key f k = pp f k + end) + + let pp ~pp_value fmt m = + let pp_item fmt (k, v) = F.fprintf fmt "(%a, %a)" pp_key k pp_value v in + PrettyPrintable.pp_collection ~pp_item fmt (bindings m) +end + +include AbstractDomain.Map (PPMap) (ArrInfo) + +let bot : astate + = empty + +let make : Allocsite.t -> Itv.t -> Itv.t -> Itv.t -> astate + = fun a o sz st -> add a (ArrInfo.make (o, sz, st)) bot + +let offsetof : astate -> Itv.t + = fun a -> fold (fun _ arr -> Itv.join arr.ArrInfo.offset) a Itv.bot + +let sizeof : astate -> Itv.t + = fun a -> fold (fun _ arr -> Itv.join arr.ArrInfo.size) a Itv.bot + +let extern : string -> astate + = fun allocsite -> add allocsite ArrInfo.top empty + +let input : string -> astate + = fun allocsite -> add allocsite ArrInfo.input empty + +let weak_plus_size : astate -> Itv.t -> astate + = fun arr i -> map (fun a -> ArrInfo.weak_plus_size a i) arr + +let plus_offset : astate -> Itv.t -> astate + = fun arr i -> map (fun a -> ArrInfo.plus_offset a i) arr + +let minus_offset : astate -> Itv.t -> astate + = fun arr i -> map (fun a -> ArrInfo.minus_offset a i) arr + +let diff : astate -> astate -> Itv.t + = fun arr1 arr2 -> + let diff_join k a2 acc = + match find k arr1 with + | a1 -> Itv.join acc (ArrInfo.diff a1 a2) + | exception Not_found -> acc + in + fold diff_join arr2 Itv.bot + +let get_pow_loc : astate -> PowLoc.t + = fun array -> + let pow_loc_of_allocsite k _ acc = PowLoc.add (Loc.of_allocsite k) acc in + fold pow_loc_of_allocsite array PowLoc.bot + +let subst : astate -> Itv.Bound.t Itv.SubstMap.t -> astate + = fun a subst_map -> map (fun info -> ArrInfo.subst info subst_map) a + +let get_symbols : astate -> Itv.Symbol.t list + = fun a -> + IList.flatten (IList.map (fun (_, ai) -> ArrInfo.get_symbols ai) (bindings a)) + +let normalize : astate -> astate + = fun a -> map ArrInfo.normalize a + +let do_prune + : (ArrInfo.t -> ArrInfo.t -> ArrInfo.t) -> astate -> astate -> astate + = fun arr_info_prune a1 a2 -> + if Int.equal (cardinal a2) 1 then + let (k, v2) = choose a2 in + if mem k a1 then add k (arr_info_prune (find k a1) v2) a1 else a1 + else a1 + +let prune_comp : Binop.t -> astate -> astate -> astate + = fun c a1 a2 -> do_prune (ArrInfo.prune_comp c) a1 a2 + +let prune_eq : astate -> astate -> astate + = fun a1 a2 -> do_prune ArrInfo.prune_eq a1 a2 + +let prune_ne : astate -> astate -> astate + = fun a1 a2 -> do_prune ArrInfo.prune_ne a1 a2 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml new file mode 100644 index 000000000..1fcae5741 --- /dev/null +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -0,0 +1,461 @@ +(* + * Copyright (c) 2016 - present + * + * Programming Research Laboratory (ROPAS) + * Seoul National University, Korea + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +open! IStd +open AbsLoc + +module F = Format +module L = Logging +module Dom = BufferOverrunDomain + +module Summary = Summary.Make (struct + type summary = Dom.Summary.t + + let update_payload astate payload = + { payload with Specs.buffer_overrun = Some astate } + + let read_from_payload payload = + payload.Specs.buffer_overrun + end) + +module TransferFunctions (CFG : ProcCfg.S) = +struct + module CFG = CFG + module Domain = Dom.Mem + module Sem = BufferOverrunSemantics.Make (CFG) + + type extras = Procname.t -> Procdesc.t option + + (* NOTE: heuristic *) + let get_malloc_info : Exp.t -> Typ.t * Exp.t + = function + | Exp.BinOp (Binop.Mult, Exp.Sizeof (typ, _, _), size) + | Exp.BinOp (Binop.Mult, size, Exp.Sizeof (typ, _, _)) -> (typ, size) + | Exp.Sizeof (typ, _, _) -> (typ, Exp.one) + | x -> (Typ.Tint Typ.IChar, x) + + let model_malloc + : Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node + -> Dom.Mem.t -> Dom.Mem.t + = fun pname ret params node mem -> + match ret with + | Some (id, _) -> + let (typ, size) = get_malloc_info (IList.hd params |> fst) in + let size = Sem.eval size mem (CFG.loc node) |> Dom.Val.get_itv in + let v = Sem.eval_array_alloc pname node typ Itv.zero size 0 1 in + Dom.Mem.add_stack (Loc.of_id id) v mem + | _ -> mem + + let model_realloc + : Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node + -> Dom.Mem.t -> Dom.Mem.t + = fun pname ret params node mem -> + model_malloc pname ret (IList.tl params) node mem + + let model_natual_itv : (Ident.t * Typ.t) option -> Dom.Mem.t -> Dom.Mem.t + = fun ret mem -> + match ret with + | Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) Dom.Val.nat_itv mem + | _ -> mem + + let model_unknown_itv : (Ident.t * Typ.t) option -> Dom.Mem.t -> Dom.Mem.t + = fun ret mem -> + match ret with + Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) Dom.Val.top_itv mem + | None -> mem + + let model_infer_print + : (Exp.t * Typ.t) list -> Dom.Mem.t -> Location.t -> Dom.Mem.t + = fun params mem loc -> + match params with + | (e, _) :: _ -> + (* TODO: only print when debug mode? *) + F.fprintf F.err_formatter "@[=== Infer Print === at %a@," + Location.pp loc; + Dom.Val.pp F.err_formatter (Sem.eval e mem loc); + F.fprintf F.err_formatter "@]"; + mem + | _ -> mem + + let handle_unknown_call + : Procname.t -> (Ident.t * Typ.t) option -> Procname.t + -> (Exp.t * Typ.t) list -> CFG.node -> Dom.Mem.t -> Location.t + -> Dom.Mem.t + = fun pname ret callee_pname params node mem loc -> + match Procname.get_method callee_pname with + | "malloc" + | "__new_array" -> model_malloc pname ret params node mem + | "realloc" -> model_realloc pname ret params node mem + | "strlen" + | "fgetc" -> model_natual_itv ret mem + | "infer_print" -> model_infer_print params mem loc + | _ -> model_unknown_itv ret mem + + let rec declare_array + : Procname.t -> CFG.node -> Loc.t -> Typ.t -> IntLit.t -> inst_num:int + -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate + = fun pname node loc typ len ~inst_num ~dimension mem -> + let size = IntLit.to_int len |> Itv.of_int in + let arr = + Sem.eval_array_alloc pname node typ Itv.zero size inst_num dimension + in + let mem = + if Int.equal dimension 1 + then Dom.Mem.add_stack loc arr mem + else Dom.Mem.add_heap loc arr mem + in + let loc = + Loc.of_allocsite (Sem.get_allocsite pname node inst_num dimension) + in + match typ with + | Typ.Tarray (typ, Some len) -> + declare_array pname node loc typ len ~inst_num + ~dimension:(dimension + 1) mem + | _ -> mem + + let declare_symbolic_array + : Procname.t -> Tenv.t -> CFG.node -> Loc.t -> Typ.t -> inst_num:int + -> sym_num:int -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int + = fun pname tenv node loc typ ~inst_num ~sym_num ~dimension mem -> + let offset = Itv.make_sym pname sym_num in + let size = Itv.make_sym pname (sym_num + 2) in + let arr = + Sem.eval_array_alloc pname node typ offset size inst_num dimension + in + let elem_val = Dom.Val.make_sym pname (sym_num + 4) in + let arr_loc = arr |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc in + let mem = + mem + |> Dom.Mem.add_heap loc arr + |> Dom.Mem.strong_update_heap arr_loc elem_val + in + let decl_fld (mem, sym_num) (fn, typ, _) = + let loc = + mem |> Dom.Mem.find_heap loc |> Dom.Val.get_all_locs |> PowLoc.choose + in + let field = Loc.append_field loc fn in + match typ with + | Typ.Tint _ + | Typ.Tfloat _ -> + let v = Dom.Val.make_sym pname sym_num in + (Dom.Mem.add_heap field v mem, sym_num + 2) + | Typ.Tptr (typ, _) -> + let offset = Itv.make_sym pname sym_num in + let size = Itv.make_sym pname (sym_num + 2) in + let v = + Sem.eval_array_alloc pname node typ offset size inst_num dimension + in + (Dom.Mem.add_heap field v mem, sym_num + 4) + | _ -> (mem, sym_num) + in + match typ with + | Typ.Tstruct typename -> + (match Tenv.lookup tenv typename with + | Some str -> + IList.fold_left decl_fld (mem, sym_num + 6) str.StructTyp.fields + | _ -> (mem, sym_num + 6)) + | _ -> (mem, sym_num + 6) + + let declare_symbolic_parameter + : Procdesc.t -> Tenv.t -> CFG.node -> int -> Dom.Mem.t -> Dom.Mem.t + = fun pdesc tenv node inst_num mem -> + let pname = Procdesc.get_proc_name pdesc in + let add_formal (mem, inst_num, sym_num) (pvar, typ) = + match typ with + | Typ.Tint _ -> + let v = Dom.Val.make_sym pname sym_num in + let mem = Dom.Mem.add_heap (Loc.of_pvar pvar) v mem in + (mem, inst_num + 1, sym_num + 2) + | Typ.Tptr (typ, _) -> + let (mem, sym_num) = + declare_symbolic_array pname tenv node (Loc.of_pvar pvar) typ + ~inst_num ~sym_num ~dimension:1 mem + in + (mem, inst_num + 1, sym_num) + | _ -> (mem, inst_num, sym_num) (* TODO: add other cases if necessary *) + in + IList.fold_left add_formal (mem, inst_num, 0) (Sem.get_formals pdesc) + |> fst3 + + let instantiate_ret + : Tenv.t -> Procdesc.t option -> Procname.t -> (Exp.t * Typ.t) list + -> Dom.Mem.t -> Dom.Summary.t -> Location.t -> Dom.Val.astate + = fun tenv callee_pdesc callee_pname params caller_mem summary loc -> + let callee_entry_mem = Dom.Summary.get_input summary in + let callee_exit_mem = Dom.Summary.get_output summary in + match callee_pdesc with + | Some pdesc -> + let subst_map = + Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem loc + in + let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in + let ret_val = Dom.Mem.find_heap ret_loc callee_exit_mem in + Dom.Val.subst ret_val subst_map + |> Dom.Val.normalize (* normalize bottom *) + | _ -> Dom.Val.bot + + let print_debug_info : Sil.instr -> Dom.Mem.t -> Dom.Mem.t -> unit + = fun instr pre post -> + if Config.bo_debug >= 2 then + begin + F.fprintf F.err_formatter "@.@.================================@."; + F.fprintf F.err_formatter "@[Pre-state : @,"; + Dom.Mem.pp F.err_formatter pre; + F.fprintf F.err_formatter "@]@.@."; + Sil.pp_instr Pp.text F.err_formatter instr; + F.fprintf F.err_formatter "@.@."; + F.fprintf F.err_formatter "@[Post-state : @,"; + Dom.Mem.pp F.err_formatter post; + F.fprintf F.err_formatter "@]@."; + F.fprintf F.err_formatter "================================@.@." + end + + let exec_instr + : Dom.Mem.t -> extras ProcData.t -> CFG.node -> Sil.instr -> Dom.Mem.astate + = fun mem { pdesc; tenv; extras } node instr -> + let pname = Procdesc.get_proc_name pdesc in + let try_decl_arr (mem, inst_num) (pvar, typ) = + match typ with + | Typ.Tarray (typ, Some len) -> + let loc = Loc.of_var (Var.of_pvar pvar) in + let mem = + declare_array pname node loc typ len ~inst_num ~dimension:1 mem + in + (mem, inst_num + 1) + | _ -> (mem, inst_num) + in + let output_mem = + match instr with + | Load (id, exp, _, loc) -> + let locs = Sem.eval exp mem loc |> Dom.Val.get_all_locs in + let v = Dom.Mem.find_heap_set locs mem in + Dom.Mem.add_stack (Loc.of_var (Var.of_id id)) v mem + |> Dom.Mem.load_alias id exp + | Store (exp1, _, exp2, loc) -> + let locs = Sem.eval exp1 mem loc |> Dom.Val.get_all_locs in + Dom.Mem.update_mem locs (Sem.eval exp2 mem loc) mem + |> Dom.Mem.store_alias exp1 exp2 + | Prune (exp, loc, _, _) -> Sem.prune exp loc mem + | Call (ret, Const (Cfun callee_pname), params, loc, _) -> + (match Summary.read_summary pdesc callee_pname with + | Some summary -> + let callee = extras callee_pname in + let ret_val = + instantiate_ret tenv callee callee_pname params mem summary loc + in + (match ret with + | Some (id, _) -> + Dom.Mem.add_stack (Loc.of_var (Var.of_id id)) ret_val mem + | _ -> mem) + | None -> + handle_unknown_call pname ret callee_pname params node mem loc) + | Declare_locals (locals, _) -> + (* array allocation in stack e.g., int arr[10] *) + let (mem, inst_num) = IList.fold_left try_decl_arr (mem, 1) locals in + declare_symbolic_parameter pdesc tenv node inst_num mem + | Call _ + | Remove_temps _ + | Abstract _ + | Nullify _ -> mem + in + print_debug_info instr mem output_mem; + output_mem +end + +module Analyzer = + AbstractInterpreter.Make + (ProcCfg.Normal) + (Scheduler.ReversePostorder) + (TransferFunctions) + +module Interprocedural = AbstractInterpreter.Interprocedural (Summary) +module CFG = Analyzer.TransferFunctions.CFG +module Sem = BufferOverrunSemantics.Make (CFG) + +module Report = +struct + type extras = Procname.t -> Procdesc.t option + + let add_condition + : Procname.t -> CFG.node -> Exp.t -> Location.t -> Dom.Mem.astate + -> Dom.ConditionSet.t -> Dom.ConditionSet.t + = fun pname node exp loc mem cond_set -> + let array_access = + match exp with + | Exp.Var _ -> + let arr = Sem.eval exp mem loc |> Dom.Val.get_array_blk in + Some (arr, Itv.zero, true) + | Exp.Lindex (e1, e2) + | Exp.BinOp (Binop.PlusA, e1, e2) -> + let arr = Sem.eval e1 mem loc |> Dom.Val.get_array_blk in + let idx = Sem.eval e2 mem loc |> Dom.Val.get_itv in + Some (arr, idx, true) + | Exp.BinOp (Binop.MinusA, e1, e2) -> + let arr = Sem.eval e1 mem loc |> Dom.Val.get_array_blk in + let idx = Sem.eval e2 mem loc |> Dom.Val.get_itv in + Some (arr, idx, false) + | _ -> None + in + match array_access with + | Some (arr, idx, is_plus) -> + let site = Sem.get_allocsite pname node 0 0 in + let size = ArrayBlk.sizeof arr in + let offset = ArrayBlk.offsetof arr in + let idx = (if is_plus then Itv.plus else Itv.minus) offset idx in + (if Config.bo_debug >= 2 then + (F.fprintf F.err_formatter "@[Add condition :@,"; + F.fprintf F.err_formatter "array: %a@," ArrayBlk.pp arr; + F.fprintf F.err_formatter " idx: %a@," Itv.pp idx; + F.fprintf F.err_formatter "@]@.")); + if size <> Itv.bot && idx <> Itv.bot then + Dom.ConditionSet.add_bo_safety pname loc site ~size ~idx cond_set + else cond_set + | None -> cond_set + + let instantiate_cond + : Tenv.t -> Procname.t -> Procdesc.t option -> (Exp.t * Typ.t) list + -> Dom.Mem.t -> Summary.summary -> Location.t -> Dom.ConditionSet.t + = fun tenv caller_pname callee_pdesc params caller_mem summary loc -> + let callee_entry_mem = Dom.Summary.get_input summary in + let callee_cond = Dom.Summary.get_cond_set summary in + match callee_pdesc with + | Some pdesc -> + let subst_map = + Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem loc + in + let pname = Procdesc.get_proc_name pdesc in + Dom.ConditionSet.subst callee_cond subst_map caller_pname pname loc + | _ -> callee_cond + + let print_debug_info : Sil.instr -> Dom.Mem.t -> Dom.ConditionSet.t -> unit + = fun instr pre cond_set -> + if Config.bo_debug >= 2 then + (F.fprintf F.err_formatter "@.@.================================@."; + F.fprintf F.err_formatter "@[Pre-state : @,"; + Dom.Mem.pp F.err_formatter pre; + F.fprintf F.err_formatter "@]@.@."; + Sil.pp_instr Pp.text F.err_formatter instr; + F.fprintf F.err_formatter "@[@.@."; + Dom.ConditionSet.pp F.err_formatter cond_set; + F.fprintf F.err_formatter "@]@."; + F.fprintf F.err_formatter "================================@.@.") + + let collect_instr + : extras ProcData.t -> CFG.node -> Dom.ConditionSet.t * Dom.Mem.t + -> Sil.instr -> Dom.ConditionSet.t * Dom.Mem.t + = fun ({ pdesc; tenv; extras } as pdata) node (cond_set, mem) instr -> + let pname = Procdesc.get_proc_name pdesc in + let cond_set = + match instr with + | Sil.Load (_, exp, _, loc) + | Sil.Store (exp, _, _, loc) -> + add_condition pname node exp loc mem cond_set + | Sil.Call (_, Const (Cfun callee_pname), params, loc, _) -> + (match Summary.read_summary pdesc callee_pname with + | Some summary -> + let callee = extras callee_pname in + instantiate_cond tenv pname callee params mem summary loc + |> Dom.ConditionSet.rm_invalid + |> Dom.ConditionSet.join cond_set + | _ -> cond_set) + | _ -> cond_set + in + let mem = Analyzer.TransferFunctions.exec_instr mem pdata node instr in + print_debug_info instr mem cond_set; + (cond_set, mem) + + let collect_instrs + : extras ProcData.t -> CFG.node -> Sil.instr list -> Dom.Mem.t + -> Dom.ConditionSet.t -> Dom.ConditionSet.t + = fun pdata node instrs mem cond_set -> + IList.fold_left (collect_instr pdata node) (cond_set, mem) instrs + |> fst + + let collect_node + : extras ProcData.t -> Analyzer.invariant_map -> Dom.ConditionSet.t -> + CFG.node -> Dom.ConditionSet.t + = fun pdata inv_map cond_set node -> + let instrs = CFG.instr_ids node |> IList.map fst in + match Analyzer.extract_pre (CFG.id node) inv_map with + | Some mem -> collect_instrs pdata node instrs mem cond_set + | _ -> cond_set + + let collect : extras ProcData.t -> Analyzer.invariant_map -> Dom.ConditionSet.t + = fun ({ pdesc } as pdata) inv_map -> + let add_node1 acc node = collect_node pdata inv_map acc node in + Procdesc.fold_nodes add_node1 Dom.ConditionSet.empty pdesc + + let report_error : Procdesc.t -> Dom.ConditionSet.t -> unit + = fun pdesc conds -> + let pname = Procdesc.get_proc_name pdesc in + let report1 cond = + let alarm = Dom.Condition.check cond in + let (caller_pname, loc) = + match Dom.Condition.get_trace cond with + | Dom.Condition.Inter (caller_pname, _, loc) -> (caller_pname, loc) + | Dom.Condition.Intra pname -> (pname, Dom.Condition.get_location cond) + in + match alarm with + | None -> () + | Some bucket when Procname.equal pname caller_pname -> + let description = Dom.Condition.to_string cond in + let error_desc = Localise.desc_buffer_overrun bucket description in + let exn = Exceptions.Checkers (Localise.to_string Localise.buffer_overrun, error_desc) in + let trace = [Errlog.make_trace_element 0 loc description []] in + Reporting.log_error pname ~loc ~ltr:trace exn + | _ -> () + in + Dom.ConditionSet.iter report1 conds +end + +let compute_post + : Analyzer.TransferFunctions.extras ProcData.t -> Summary.summary option + = fun { pdesc; tenv; extras = get_pdesc } -> + let cfg = CFG.from_pdesc pdesc in + let pdata = ProcData.make pdesc tenv get_pdesc in + let pname = Procdesc.get_proc_name pdesc in + let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.bot pdata in + let entry_mem = + let entry_id = CFG.id (CFG.start_node cfg) in + Analyzer.extract_post entry_id inv_map + in + let exit_mem = + let exit_id = CFG.id (CFG.exit_node cfg) in + Analyzer.extract_post exit_id inv_map + in + let cond_set = Report.collect pdata inv_map in + Report.report_error pdesc cond_set; + match entry_mem, exit_mem with + | Some entry_mem, Some exit_mem -> + Summary.write_summary pname (entry_mem, exit_mem, cond_set); + Some (entry_mem, exit_mem, cond_set) + | _ -> None + +let print_summary : Procname.t -> Dom.Summary.t -> unit + = fun proc_name s -> + F.fprintf F.err_formatter "@.@[Summary of %a :@," + Procname.pp proc_name; + Dom.Summary.pp_summary F.err_formatter s; + F.fprintf F.err_formatter "@]@." + +let checker : Callbacks.proc_callback_args -> unit + = fun ({ proc_name } as callback) -> + let make_extras _ = callback.get_proc_desc in + let post = + Interprocedural.compute_and_store_post + ~compute_post + ~make_extras + callback + in + match post with + | Some s when Config.bo_debug >= 1 -> print_summary proc_name s + | _ -> () diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml new file mode 100644 index 000000000..78b0cfa1b --- /dev/null +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -0,0 +1,707 @@ +(* + * Copyright (c) 2016 - present + * + * Programming Research Laboratory (ROPAS) + * Seoul National University, Korea + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +open! IStd +open AbsLoc + +module F = Format +module L = Logging + +module Condition = +struct + type t = + { idx : Itv.astate; + size : Itv.astate; + proc_name : Procname.t; + loc : Location.t; + trace : trace; + id : string } + [@@deriving compare] +and trace = Intra of Procname.t + | Inter of Procname.t * Procname.t * Location.t +[@@deriving compare] + +and astate = t + +let set_size_pos : t -> t + = fun c -> + let size = + if Itv.Bound.le (Itv.lb c.size) Itv.Bound.zero + then Itv.make Itv.Bound.zero (Itv.ub c.size) + else c.size + in + { c with size } + +let string_of_location : Location.t -> string + = fun loc -> + let fname = SourceFile.to_string loc.Location.file in + let pos = Location.to_string loc in + F.fprintf F.str_formatter "%s:%s" fname pos; + F.flush_str_formatter () + +let pp_location : F.formatter -> t -> unit + = fun fmt c -> + F.fprintf fmt "%s" (string_of_location c.loc) + +let pp : F.formatter -> t -> unit + = fun fmt c -> + let c = set_size_pos c in + if Config.bo_debug <= 1 then + F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c + else + match c.trace with + Inter (_, pname, loc) -> + let pname = Procname.to_string pname in + F.fprintf fmt "%a < %a at %a by call %s() at %s" + Itv.pp c.idx Itv.pp c.size pp_location c pname (string_of_location loc) + | Intra _ -> F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c + +let pp_element : F.formatter -> t -> unit + = pp + +let get_location : t -> Location.t + = fun c -> c.loc + +let get_trace : t -> trace + = fun c -> c.trace + +let get_proc_name : t -> Procname.t + = fun c -> c.proc_name + +let make : Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t + = fun proc_name loc id ~idx ~size -> + { proc_name; idx; size; loc; id ; trace = Intra proc_name } + +let filter1 : t -> bool + = fun c -> + Itv.eq c.idx Itv.top || Itv.eq c.size Itv.top + || (try Itv.Bound.eq (Itv.lb c.idx) Itv.Bound.MInf with _ -> false) + || (try Itv.Bound.eq (Itv.lb c.size) Itv.Bound.MInf with _ -> false) + || (Itv.eq c.idx Itv.nat && Itv.eq c.size Itv.nat) + +let filter2 : t -> bool + = fun c -> + (not (Itv.is_finite c.idx) || not (Itv.is_finite c.size)) (* basically, alarms involving infinify are filtered *) + && (* except the following cases : *) + not ((Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb < 0 *) + Itv.Bound.lt (Itv.lb c.idx) Itv.Bound.zero) + || + (Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb > size lb *) + (Itv.Bound.gt (Itv.lb c.idx) (Itv.lb c.size))) + || + (Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb > size ub *) + (Itv.Bound.gt (Itv.lb c.idx) (Itv.ub c.size))) + || + (Itv.Bound.is_not_infty (Itv.ub c.idx) && (* idx non-infty ub > size lb *) + (Itv.Bound.gt (Itv.ub c.idx) (Itv.lb c.size))) + || + (Itv.Bound.is_not_infty (Itv.ub c.idx) && (* idx non-infty ub > size ub *) + (Itv.Bound.gt (Itv.ub c.idx) (Itv.ub c.size)))) + +(* check buffer overrun and return its confidence *) +let check : t -> string option + = fun c -> + if Config.bo_debug <= 1 && (Itv.is_symbolic c.idx || Itv.is_symbolic c.size) + then None + else if filter1 c then Some Localise.BucketLevel.b5 + else if filter2 c then Some Localise.BucketLevel.b3 + else + let c = set_size_pos c in + let not_overrun = Itv.lt_sem c.idx c.size in + let not_underrun = Itv.le_sem Itv.zero c.idx in + if (Itv.eq not_overrun Itv.one) && (Itv.eq not_underrun Itv.one) then None + else Some Localise.BucketLevel.b1 + +let invalid : t -> bool + = fun x -> Itv.invalid x.idx || Itv.invalid x.size + +let to_string : t -> string + = fun c -> + let c = set_size_pos c in + "Offset : " ^ Itv.to_string c.idx ^ " Size : " ^ Itv.to_string c.size + ^ " @ " ^ string_of_location c.loc + ^ (match c.trace with + Inter (_, pname, _) -> + " by call " + ^ Procname.to_string pname + ^ "() " + | Intra _ -> "") + +let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Procname.t -> Procname.t -> Location.t -> t + = fun c subst_map caller_pname callee_pname loc -> + if Itv.is_symbolic c.idx || Itv.is_symbolic c.size then + { c with idx = Itv.subst c.idx subst_map; + size = Itv.subst c.size subst_map; + trace = Inter (caller_pname, callee_pname, loc) } + else c +end + +module ConditionSet = +struct + module PPSet = PrettyPrintable.MakePPSet (Condition) + include AbstractDomain.FiniteSet (PPSet) + + module Map = Caml.Map.Make (struct + type t = Location.t [@@deriving compare] + end) + + let add_bo_safety + : Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t -> t + = fun pname loc id ~idx ~size cond -> + add (Condition.make pname loc id ~idx ~size) cond + + let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Procname.t -> Procname.t -> Location.t -> t + = fun x subst_map caller_pname callee_pname loc -> + fold (fun e -> add (Condition.subst e subst_map caller_pname callee_pname loc)) x empty + + let group : t -> t Map.t + = fun x -> + fold (fun cond map -> + let old_set = try Map.find cond.loc map with _ -> empty in + Map.add cond.loc (add cond old_set) map) x Map.empty + + let pp_summary : F.formatter -> t -> unit + = fun fmt x -> + let pp_sep fmt () = F.fprintf fmt ", @," in + let pp_element fmt v = Condition.pp fmt v in + F.fprintf fmt "@[Safety conditions:@,"; + F.fprintf fmt "@[{ "; + F.pp_print_list ~pp_sep pp_element fmt (elements x); + F.fprintf fmt " }@]"; + F.fprintf fmt "@]" + + let pp : Format.formatter -> t -> unit + = fun fmt x -> + let pp_sep fmt () = F.fprintf fmt ", @," in + let pp_element fmt v = Condition.pp fmt v in + F.fprintf fmt "@[Safety conditions :@,"; + F.fprintf fmt "@[{"; + F.pp_print_list ~pp_sep pp_element fmt (elements x); + F.fprintf fmt " }@]"; + F.fprintf fmt "@]" + + let rm_invalid : t -> t + = fun x -> filter (fun c -> not (Condition.invalid c)) x +end + +module Val = +struct + type astate = { + itv : Itv.astate; + powloc : PowLoc.astate; + arrayblk : ArrayBlk.astate; + } + + type t = astate + + let bot : t + = { itv = Itv.bot; powloc = PowLoc.bot; arrayblk = ArrayBlk.bot } + + let (<=) ~lhs ~rhs = + if phys_equal lhs rhs then true + else + Itv.(<=) ~lhs:(lhs.itv) ~rhs:(rhs.itv) + && PowLoc.(<=) ~lhs:(lhs.powloc) ~rhs:(rhs.powloc) + && ArrayBlk.(<=) ~lhs:(lhs.arrayblk) ~rhs:(rhs.arrayblk) + + let widen ~prev ~next ~num_iters = + if phys_equal prev next then prev + else + { itv = Itv.widen ~prev:(prev.itv) ~next:(next.itv) ~num_iters; + powloc = PowLoc.widen ~prev:(prev.powloc) ~next:(next.powloc) ~num_iters; + arrayblk = ArrayBlk.widen ~prev:(prev.arrayblk) ~next:(next.arrayblk) ~num_iters; } + + let pp fmt x = + F.fprintf fmt "(%a, %a, %a)" Itv.pp x.itv PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk + + let join : t -> t -> t + = fun x y -> + if phys_equal x y then x + else + { itv = Itv.join x.itv y.itv; + powloc = PowLoc.join x.powloc y.powloc; + arrayblk = ArrayBlk.join x.arrayblk y.arrayblk } + + let rec joins : t list -> t + = function + | [] -> bot + | [a] -> a + | a :: b -> join a (joins b) + + let get_itv : t -> Itv.t + = fun x -> x.itv + + let get_pow_loc : t -> PowLoc.t + = fun x -> x.powloc + + let get_array_blk : t -> ArrayBlk.astate + = fun x -> x.arrayblk + + let get_all_locs : t -> PowLoc.t + = fun x -> ArrayBlk.get_pow_loc x.arrayblk |> PowLoc.join x.powloc + + let top_itv : t + = { bot with itv = Itv.top } + + let pos_itv : t + = { bot with itv = Itv.pos } + + let nat_itv : t + = { bot with itv = Itv.nat } + + let of_int : int -> t + = fun n -> { bot with itv = Itv.of_int n } + + let of_pow_loc : PowLoc.t -> t + = fun x -> { bot with powloc = x } + + let of_array_blk : ArrayBlk.astate -> t + = fun a -> { bot with arrayblk = a } + + let zero : t + = of_int 0 + + let modify_itv : Itv.t -> t -> t + = fun i x -> { x with itv = i } + + let make_sym : Procname.t -> int -> t + = fun pname i -> { bot with itv = Itv.make_sym pname i } + + let unknown_bit : t -> t + = fun x -> { x with itv = Itv.top } + + let neg : t -> t + = fun x -> { x with itv = Itv.neg x.itv } + + let lnot : t -> t + = fun x -> { x with itv = Itv.lnot x.itv } + + let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> t -> t -> t + = fun f x y -> { bot with itv = f x.itv y.itv } + + let plus : t -> t -> t + = fun x y -> + { x with itv = Itv.plus x.itv y.itv; arrayblk = ArrayBlk.plus_offset x.arrayblk y.itv } + + let minus : t -> t -> t + = fun x y -> + let n = Itv.join (Itv.minus x.itv y.itv) (ArrayBlk.diff x.arrayblk y.arrayblk) in + let a = ArrayBlk.minus_offset x.arrayblk y.itv in + { bot with itv = n; arrayblk = a} + + let mult : t -> t -> t + = lift_itv Itv.mult + + let div : t -> t -> t + = lift_itv Itv.div + + let mod_sem : t -> t -> t + = lift_itv Itv.mod_sem + + let shiftlt : t -> t -> t + = lift_itv Itv.shiftlt + + let shiftrt : t -> t -> t + = lift_itv Itv.shiftrt + + let lt_sem : t -> t -> t + = lift_itv Itv.lt_sem + + let gt_sem : t -> t -> t + = lift_itv Itv.gt_sem + + let le_sem : t -> t -> t + = lift_itv Itv.le_sem + + let ge_sem : t -> t -> t + = lift_itv Itv.ge_sem + + let eq_sem : t -> t -> t + = lift_itv Itv.eq_sem + + let ne_sem : t -> t -> t + = lift_itv Itv.ne_sem + + let land_sem : t -> t -> t + = lift_itv Itv.land_sem + + let lor_sem : t -> t -> t + = lift_itv Itv.lor_sem + + let lift_prune1 : (Itv.t -> Itv.t) -> t -> t + = fun f x -> { x with itv = f x.itv } + + let lift_prune2 + : (Itv.t -> Itv.t -> Itv.t) + -> (ArrayBlk.astate -> ArrayBlk.astate -> ArrayBlk.astate) -> t -> t -> t + = fun f g x y -> + { x with itv = f x.itv y.itv; arrayblk = g x.arrayblk y.arrayblk } + + let prune_zero : t -> t + = lift_prune1 Itv.prune_zero + + let prune_comp : Binop.t -> t -> t -> t + = fun c -> lift_prune2 (Itv.prune_comp c) (ArrayBlk.prune_comp c) + + let prune_eq : t -> t -> t + = lift_prune2 Itv.prune_eq ArrayBlk.prune_eq + + let prune_ne : t -> t -> t + = lift_prune2 Itv.prune_ne ArrayBlk.prune_eq + + let plus_pi : t -> t -> t + = fun x y -> + { bot with arrayblk = ArrayBlk.plus_offset x.arrayblk y.itv } + + let minus_pi : t -> t -> t + = fun x y -> + { bot with arrayblk = ArrayBlk.minus_offset x.arrayblk y.itv } + + let minus_pp : t -> t -> t + = fun x y -> + { bot with itv = ArrayBlk.diff x.arrayblk y.arrayblk } + + let subst : t -> Itv.Bound.t Itv.SubstMap.t -> t + = fun x subst_map -> + { x with itv = Itv.subst x.itv subst_map; + arrayblk = ArrayBlk.subst x.arrayblk subst_map } + + let get_symbols : t -> Itv.Symbol.t list + = fun x -> + IList.append (Itv.get_symbols x.itv) (ArrayBlk.get_symbols x.arrayblk) + + let normalize : t -> t + = fun x -> + { x with itv = Itv.normalize x.itv; arrayblk = ArrayBlk.normalize x.arrayblk } + + let pp_summary : F.formatter -> t -> unit + = fun fmt x -> F.fprintf fmt "(%a, %a)" Itv.pp x.itv ArrayBlk.pp x.arrayblk +end + +module Stack = +struct + module PPMap = + struct + module Ord = struct include Loc let pp_key = pp end + include PrettyPrintable.MakePPMap (Ord) + + let pp_collection + : pp_item:(F.formatter -> 'a -> unit) -> F.formatter -> 'a list -> unit + = fun ~pp_item fmt c -> + let pp_sep fmt () = F.fprintf fmt ",@," in + F.pp_print_list ~pp_sep pp_item fmt c + + let pp + : pp_value:(F.formatter -> 'a -> unit) -> F.formatter -> 'a t -> unit + = fun ~pp_value fmt m -> + let pp_item fmt (k, v) = + F.fprintf fmt "%a -> %a" Ord.pp_key k pp_value v + in + F.fprintf fmt "@[{ "; + pp_collection ~pp_item fmt (bindings m); + F.fprintf fmt " }@]" + end + + include AbstractDomain.Map (PPMap) (Val) + + let bot = empty + + let find : Loc.t -> astate -> Val.t + = fun l m -> + try find l m with + | Not_found -> Val.bot + + let find_set : PowLoc.t -> astate -> Val.t + = fun locs mem -> + let find_join loc acc = Val.join acc (find loc mem) in + PowLoc.fold find_join locs Val.bot + + let strong_update : PowLoc.t -> Val.astate -> astate -> astate + = fun locs v mem -> + PowLoc.fold (fun x -> add x v) locs mem + + let weak_update : PowLoc.t -> Val.astate -> astate -> astate + = fun locs v mem -> + PowLoc.fold (fun x -> add x (Val.join v (find x mem))) locs mem + + let pp_summary : F.formatter -> astate -> unit + = fun fmt mem -> + let pp_not_logical_var k v = + if Loc.is_logical_var k then () else + F.fprintf fmt "%a -> %a@," Loc.pp k Val.pp_summary v + in + iter pp_not_logical_var mem +end + +module Heap = +struct + module PPMap = + struct + module Ord = struct include Loc let pp_key = pp end + include PrettyPrintable.MakePPMap (Ord) + + let pp_collection + : pp_item:(F.formatter -> 'a -> unit) -> F.formatter -> 'a list -> unit + = fun ~pp_item fmt c -> + let pp_sep fmt () = F.fprintf fmt ",@," in + F.pp_print_list ~pp_sep pp_item fmt c + + let pp : pp_value:(F.formatter -> 'a -> unit) -> F.formatter -> 'a t -> unit + = fun ~pp_value fmt m -> + let pp_item fmt (k, v) = + F.fprintf fmt "%a -> %a" Ord.pp_key k pp_value v + in + F.fprintf fmt "@[{ "; + pp_collection ~pp_item fmt (bindings m); + F.fprintf fmt " }@]" + end + + include AbstractDomain.Map (PPMap) (Val) + + let bot = empty + + let find : Loc.t -> astate -> Val.t + = fun l m -> + try find l m with + | Not_found -> Val.bot + + let find_set : PowLoc.t -> astate -> Val.t + = fun locs mem -> + let find_join loc acc = Val.join acc (find loc mem) in + PowLoc.fold find_join locs Val.bot + + let strong_update : PowLoc.t -> Val.t -> astate -> astate + = fun locs v mem -> + PowLoc.fold (fun x -> add x v) locs mem + + let weak_update : PowLoc.t -> Val.t -> astate -> astate + = fun locs v mem -> + PowLoc.fold (fun x -> add x (Val.join v (find x mem))) locs mem + + let pp_summary : F.formatter -> astate -> unit + = fun fmt mem -> + let pp_map fmt (k, v) = F.fprintf fmt "%a -> %a" Loc.pp k Val.pp_summary v in + F.fprintf fmt "@[{ "; + F.pp_print_list pp_map fmt (bindings mem); + F.fprintf fmt " }@]" + + let get_symbols : astate -> Itv.Symbol.t list + = fun mem -> + IList.flatten (IList.map (fun (_, v) -> Val.get_symbols v) (bindings mem)) + + let get_return : astate -> Val.t + = fun mem -> + let mem = filter (fun l _ -> Loc.is_return l) mem in + if is_empty mem then Val.bot else snd (choose mem) +end + +module Alias = +struct + module M = Caml.Map.Make (Ident) + + type t = Pvar.t M.t + + type astate = t + + let bot : t + = M.empty + + let (<=) : lhs:t -> rhs:t -> bool + = fun ~lhs ~rhs -> + let is_in_rhs k v = + match M.find k rhs with + | v' -> Pvar.equal v v' + | exception Not_found -> false + in + M.for_all is_in_rhs lhs + + let join : t -> t -> t + = fun x y -> + let join_v _ v1_opt v2_opt = + match v1_opt, v2_opt with + | None, None -> None + | Some v, None + | None, Some v -> Some v + | Some v1, Some v2 -> if Pvar.equal v1 v2 then Some v1 else assert false + in + M.merge join_v x y + + let widen : prev:t -> next:t -> num_iters:int -> t + = fun ~prev ~next ~num_iters:_ -> join prev next + + let pp : F.formatter -> t -> unit + = fun fmt x -> + let pp_sep fmt () = F.fprintf fmt ", @," in + let pp1 fmt (k, v) = + F.fprintf fmt "%a=%a" (Ident.pp Pp.text) k (Pvar.pp Pp.text) v + in + (* F.fprintf fmt "@[Logical Variables :@,"; *) + F.fprintf fmt "@[{ @,"; + F.pp_print_list ~pp_sep pp1 fmt (M.bindings x); + F.fprintf fmt " }@]"; + F.fprintf fmt "@]" + + let load : Ident.t -> Exp.t -> t -> t + = fun id exp m -> + match exp with + | Exp.Lvar x -> M.add id x m + | _ -> m + + let store : Exp.t -> Exp.t -> t -> t + = fun e _ m -> + match e with + | Exp.Lvar x -> M.filter (fun _ y -> not (Pvar.equal x y)) m + | _ -> m + + let find : Ident.t -> t -> Pvar.t option + = fun k m -> try Some (M.find k m) with Not_found -> None +end + +module Mem = +struct + type astate = { stack : Stack.astate; heap : Heap.astate; alias : Alias.astate } + type t = astate + + let bot : t + = { stack = Stack.bot; heap = Heap.bot; alias = Alias.bot } + + let (<=) ~lhs ~rhs = + if phys_equal lhs rhs then true + else + Stack.(<=) ~lhs:(lhs.stack) ~rhs:(rhs.stack) + && Heap.(<=) ~lhs:(lhs.heap) ~rhs:(rhs.heap) + && Alias.(<=) ~lhs:(lhs.alias) ~rhs:(rhs.alias) + + let widen ~prev ~next ~num_iters = + if phys_equal prev next then prev + else + { stack = Stack.widen ~prev:(prev.stack) ~next:(next.stack) ~num_iters; + heap = Heap.widen ~prev:(prev.heap) ~next:(next.heap) ~num_iters; + alias = Alias.widen ~prev:(prev.alias) ~next:(next.alias) ~num_iters; } + + let join : t -> t -> t + = fun x y -> + { stack = Stack.join x.stack y.stack; + heap = Heap.join x.heap y.heap; + alias = Alias.join x.alias y.alias } + + let pp : F.formatter -> t -> unit + = fun fmt x -> + F.fprintf fmt "Stack :@,"; + F.fprintf fmt "%a@," Stack.pp x.stack; + F.fprintf fmt "Heap :@,"; + F.fprintf fmt "%a" Heap.pp x.heap + + let pp_summary : F.formatter -> t -> unit + = fun fmt x -> + F.fprintf fmt "@[Parameters :@,"; + F.fprintf fmt "%a" Heap.pp_summary x.heap ; + F.fprintf fmt "@]" + + let find_stack : Loc.t -> t -> Val.t + = fun k m -> Stack.find k m.stack + + let find_stack_set : PowLoc.t -> t -> Val.t + = fun k m -> Stack.find_set k m.stack + + let find_heap : Loc.t -> t -> Val.t + = fun k m -> Heap.find k m.heap + + let find_heap_set : PowLoc.t -> t -> Val.t + = fun k m -> Heap.find_set k m.heap + + let find_alias : Ident.t -> t -> Pvar.t option + = fun k m -> Alias.find k m.alias + + let load_alias : Ident.t -> Exp.t -> t -> t + = fun id e m -> { m with alias = Alias.load id e m.alias } + + let store_alias : Exp.t -> Exp.t -> t -> t + = fun e1 e2 m -> { m with alias = Alias.store e1 e2 m.alias } + + let add_stack : Loc.t -> Val.t -> t -> t + = fun k v m -> { m with stack = Stack.add k v m.stack } + + let add_heap : Loc.t -> Val.t -> t -> t + = fun k v m -> { m with heap = Heap.add k v m.heap } + + let strong_update_stack : PowLoc.t -> Val.t -> t -> t + = fun p v m -> { m with stack = Stack.strong_update p v m.stack } + + let strong_update_heap : PowLoc.t -> Val.t -> t -> t + = fun p v m -> { m with heap = Heap.strong_update p v m.heap } + + let weak_update_stack : PowLoc.t -> Val.t -> t -> t + = fun p v m -> { m with stack = Stack.weak_update p v m.stack } + + let weak_update_heap : PowLoc.t -> Val.t -> t -> t + = fun p v m -> { m with heap = Heap.weak_update p v m.heap } + + let get_heap_symbols : t -> Itv.Symbol.t list + = fun m -> Heap.get_symbols m.heap + + let get_return : t -> Val.t + = fun m -> Heap.get_return m.heap + + let can_strong_update : PowLoc.t -> bool + = fun ploc -> + if Int.equal (PowLoc.cardinal ploc) 1 then Loc.is_var (PowLoc.choose ploc) else false + + let update_mem : PowLoc.t -> Val.t -> t -> t + = fun ploc v s -> + if can_strong_update ploc + then strong_update_heap ploc v s + else weak_update_heap ploc v s +end + +module Summary = +struct + type t = Mem.t * Mem.t * ConditionSet.t + + let get_input : t -> Mem.t + = fst3 + + let get_output : t -> Mem.t + = snd3 + + let get_cond_set : t -> ConditionSet.t + = trd3 + + let get_symbols : t -> Itv.Symbol.t list + = fun s -> Mem.get_heap_symbols (get_input s) + + let get_return : t -> Val.t + = fun s -> Mem.get_return (get_output s) + + let pp_symbols : F.formatter -> t -> unit + = fun fmt s -> + let pp_sep fmt () = F.fprintf fmt ", @," in + F.fprintf fmt "@[Symbols: {"; + F.pp_print_list ~pp_sep Itv.Symbol.pp fmt (get_symbols s); + F.fprintf fmt "}@]" + + let pp_symbol_map : F.formatter -> t -> unit + = fun fmt s -> Mem.pp_summary fmt (get_input s) + + let pp_return : F.formatter -> t -> unit + = fun fmt s -> F.fprintf fmt "Return value: %a" Val.pp_summary (get_return s) + + let pp_summary : F.formatter -> t -> unit + = fun fmt s -> + F.fprintf fmt "%a@,%a@,%a" pp_symbol_map s pp_return s + ConditionSet.pp_summary (get_cond_set s) + + let pp : F.formatter -> t -> unit + = fun fmt (entry_mem, exit_mem, condition_set) -> + F.fprintf fmt "%a@,%a@,%a@" + Mem.pp entry_mem Mem.pp exit_mem ConditionSet.pp condition_set +end diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml new file mode 100644 index 000000000..f40d541d1 --- /dev/null +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -0,0 +1,351 @@ +(* + * Copyright (c) 2016 - present + * + * Programming Research Laboratory (ROPAS) + * Seoul National University, Korea + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +open! IStd +open Core_kernel.Fn +open AbsLoc + +module F = Format +module L = Logging +module Domain = BufferOverrunDomain +open Domain + +module Make (CFG : ProcCfg.S) = +struct + exception Not_implemented + + let eval_const : Const.t -> Val.t + = function + | Const.Cint intlit -> Val.of_int (IntLit.to_int intlit) + | Const.Cfloat f -> f |> int_of_float |> Val.of_int + | _ -> Val.bot (* TODO *) + + let sizeof_ikind : Typ.ikind -> int + = function + | Typ.IChar | Typ.ISChar | Typ.IUChar | Typ.IBool -> 1 + | Typ.IInt | Typ.IUInt -> 4 + | Typ.IShort | Typ.IUShort -> 2 + | Typ.ILong | Typ.IULong -> 4 + | Typ.ILongLong | Typ.IULongLong -> 8 + | Typ.I128 | Typ.IU128 -> 16 + + let sizeof_fkind : Typ.fkind -> int + = function + | Typ.FFloat -> 4 + | Typ.FDouble | Typ.FLongDouble -> 8 + + (* NOTE: assume 32bit machine *) + let rec sizeof : Typ.t -> int + = function + | Typ.Tint ikind -> sizeof_ikind ikind + | Typ.Tfloat fkind -> sizeof_fkind fkind + | Typ.Tvoid -> 1 + | Typ.Tptr (_, _) -> 4 + | Typ.Tstruct _ -> 4 (* TODO *) + | Typ.Tarray (typ, Some ilit) -> sizeof typ * IntLit.to_int ilit + | _ -> 4 + + let rec eval : Exp.t -> Mem.astate -> Location.t -> Val.t + = fun exp mem loc -> + match exp with + | Exp.Var id -> Mem.find_stack (Var.of_id id |> Loc.of_var) mem + | Exp.Lvar pvar -> + let ploc = pvar |> Loc.of_pvar |> PowLoc.singleton in + let arr = Mem.find_stack_set ploc mem in + ploc |> Val.of_pow_loc |> Val.join arr + | Exp.UnOp (uop, e, _) -> eval_unop uop e mem loc + | Exp.BinOp (bop, e1, e2) -> eval_binop bop e1 e2 mem loc + | Exp.Const c -> eval_const c + | Exp.Cast (_, e) -> eval e mem loc + | Exp.Lfield (e, fn, _) -> + eval e mem loc + |> Val.get_all_locs + |> flip PowLoc.append_field fn + |> Val.of_pow_loc + | Exp.Lindex (e1, _) -> + let arr = eval e1 mem loc in (* must have array blk *) + (* let idx = eval e2 mem loc in *) + let ploc = arr |> Val.get_array_blk |> ArrayBlk.get_pow_loc in + (* if nested array, add the array blk *) + let arr = Mem.find_heap_set ploc mem in + Val.join (Val.of_pow_loc ploc) arr + | Exp.Sizeof (typ, _, _) -> Val.of_int (sizeof typ) + | Exp.Exn _ + | Exp.Closure _ -> Val.bot + + and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Location.t -> Val.t + = fun unop e mem loc -> + let v = eval e mem loc in + match unop with + | Unop.Neg -> Val.neg v + | Unop.BNot -> Val.unknown_bit v + | Unop.LNot -> Val.lnot v + + and eval_binop + : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Location.t -> Val.t + = fun binop e1 e2 mem loc -> + let v1 = eval e1 mem loc in + let v2 = eval e2 mem loc in + match binop with + | Binop.PlusA -> + Val.join (Val.plus v1 v2) (Val.plus_pi v1 v2) + | Binop.PlusPI -> Val.plus_pi v1 v2 + | Binop.MinusA -> + Val.joins + [ Val.minus v1 v2 + ; Val.minus_pi v1 v2 + ; Val.minus_pp v1 v2 ] + | Binop.MinusPI -> Val.minus_pi v1 v2 + | Binop.MinusPP -> Val.minus_pp v1 v2 + | Binop.Mult -> Val.mult v1 v2 + | Binop.Div -> Val.div v1 v2 + | Binop.Mod -> Val.mod_sem v1 v2 + | Binop.Shiftlt -> Val.shiftlt v1 v2 + | Binop.Shiftrt -> Val.shiftrt v1 v2 + | Binop.Lt -> Val.lt_sem v1 v2 + | Binop.Gt -> Val.gt_sem v1 v2 + | Binop.Le -> Val.le_sem v1 v2 + | Binop.Ge -> Val.ge_sem v1 v2 + | Binop.Eq -> Val.eq_sem v1 v2 + | Binop.Ne -> Val.ne_sem v1 v2 + | Binop.BAnd + | Binop.BXor + | Binop.BOr -> Val.unknown_bit v1 + | Binop.LAnd -> Val.land_sem v1 v2 + | Binop.LOr -> Val.lor_sem v1 v2 + | Binop.PtrFld -> raise Not_implemented + + let get_allocsite : Procname.t -> CFG.node -> int -> int -> string + = fun proc_name node inst_num dimension -> + let proc_name = Procname.to_string proc_name in + let node_num = CFG.hash node |> string_of_int in + let inst_num = string_of_int inst_num in + let dimension = string_of_int dimension in + (proc_name ^ "-" ^ node_num ^ "-" ^ inst_num ^ "-" ^ dimension) + |> Allocsite.make + + let eval_array_alloc + : Procname.t -> CFG.node -> Typ.t -> Itv.t -> Itv.t -> int -> int -> Val.t + = fun pdesc node typ offset size inst_num dimension -> + let allocsite = get_allocsite pdesc node inst_num dimension in + let stride = sizeof typ |> Itv.of_int in + ArrayBlk.make allocsite offset size stride + |> Val.of_array_blk + + let prune_unop : Exp.t -> Mem.astate -> Mem.astate + = fun e mem -> + match e with + | Exp.Var x -> + (match Mem.find_alias x mem with + | Some x' -> + let lv = Loc.of_pvar x' in + let v = Mem.find_heap lv mem in + let v' = Val.prune_zero v in + Mem.update_mem (PowLoc.singleton lv) v' mem + | None -> mem) + | Exp.UnOp (Unop.LNot, Exp.Var x, _) -> + (match Mem.find_alias x mem with + | Some x' -> + let lv = Loc.of_pvar x' in + let v = Mem.find_heap lv mem in + let itv_v = + if Itv.is_bot (Val.get_itv v) then Itv.bot else + Val.get_itv Val.zero + in + let v' = Val.modify_itv itv_v v in + Mem.update_mem (PowLoc.singleton lv) v' mem + | None -> mem) + | _ -> mem + + let prune_binop_left : Exp.t -> Location.t -> Mem.astate -> Mem.astate + = fun e loc mem -> + match e with + | Exp.BinOp (Binop.Lt as comp, Exp.Var x, e') + | Exp.BinOp (Binop.Gt as comp, Exp.Var x, e') + | Exp.BinOp (Binop.Le as comp, Exp.Var x, e') + | Exp.BinOp (Binop.Ge as comp, Exp.Var x, e') -> + (match Mem.find_alias x mem with + | Some x' -> + let lv = Loc.of_pvar x' in + let v = Mem.find_heap lv mem in + let v' = Val.prune_comp comp v (eval e' mem loc) in + Mem.update_mem (PowLoc.singleton lv) v' mem + | None -> mem) + | Exp.BinOp (Binop.Eq, Exp.Var x, e') -> + (match Mem.find_alias x mem with + | Some x' -> + let lv = Loc.of_pvar x' in + let v = Mem.find_heap lv mem in + let v' = Val.prune_eq v (eval e' mem loc) in + Mem.update_mem (PowLoc.singleton lv) v' mem + | None -> mem) + | Exp.BinOp (Binop.Ne, Exp.Var x, e') -> + (match Mem.find_alias x mem with + | Some x' -> + let lv = Loc.of_pvar x' in + let v = Mem.find_heap lv mem in + let v' = Val.prune_ne v (eval e' mem loc) in + Mem.update_mem (PowLoc.singleton lv) v' mem + | None -> mem) + | _ -> mem + + let comp_rev : Binop.t -> Binop.t + = function + | Binop.Lt -> Binop.Gt + | Binop.Gt -> Binop.Lt + | Binop.Le -> Binop.Ge + | Binop.Ge -> Binop.Le + | Binop.Eq -> Binop.Eq + | Binop.Ne -> Binop.Ne + | _ -> assert (false) + + let comp_not : Binop.t -> Binop.t + = function + | Binop.Lt -> Binop.Ge + | Binop.Gt -> Binop.Le + | Binop.Le -> Binop.Gt + | Binop.Ge -> Binop.Lt + | Binop.Eq -> Binop.Ne + | Binop.Ne -> Binop.Eq + | _ -> assert (false) + + let prune_binop_right : Exp.t -> Location.t -> Mem.astate -> Mem.astate + = fun e loc mem -> + match e with + | Exp.BinOp (Binop.Lt as c, e', Exp.Var x) + | Exp.BinOp (Binop.Gt as c, e', Exp.Var x) + | Exp.BinOp (Binop.Le as c, e', Exp.Var x) + | Exp.BinOp (Binop.Ge as c, e', Exp.Var x) + | Exp.BinOp (Binop.Eq as c, e', Exp.Var x) + | Exp.BinOp (Binop.Ne as c, e', Exp.Var x) -> + prune_binop_left (Exp.BinOp (comp_rev c, Exp.Var x, e')) loc mem + | _ -> mem + + let rec prune : Exp.t -> Location.t -> Mem.astate -> Mem.astate + = fun e loc mem -> + let mem = + mem |> prune_unop e |> prune_binop_left e loc |> prune_binop_right e loc + in + match e with + | Exp.BinOp (Binop.Ne, e, Exp.Const (Const.Cint i)) when IntLit.iszero i -> + prune e loc mem + | Exp.BinOp (Binop.Eq, e, Exp.Const (Const.Cint i)) when IntLit.iszero i -> + prune (Exp.UnOp (Unop.LNot, e, None)) loc mem + | Exp.UnOp (Unop.Neg, Exp.Var x, _) -> prune (Exp.Var x) loc mem + | Exp.BinOp (Binop.LAnd, e1, e2) -> + mem |> prune e1 loc |> prune e2 loc + | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) -> + mem + |> prune (Exp.UnOp (Unop.LNot, e1, t)) loc + |> prune (Exp.UnOp (Unop.LNot, e2, t)) loc + | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Lt as c, e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Gt as c, e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Le as c, e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ge as c, e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq as c, e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ne as c, e1, e2), _) -> + prune (Exp.BinOp (comp_not c, e1, e2)) loc mem + | _ -> mem + + let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list + = fun pdesc -> + let proc_name = Procdesc.get_proc_name pdesc in + Procdesc.get_formals pdesc + |> IList.map (fun (name, typ) -> (Pvar.mk name proc_name, typ)) + + let get_matching_pairs + : Tenv.t -> Val.t -> Val.t -> Typ.t -> Mem.astate -> Mem.astate + -> (Itv.Bound.t * Itv.Bound.t) list + = fun tenv formal actual typ caller_mem callee_mem -> + let get_itv v = Val.get_itv v in + let get_offset v = v |> Val.get_array_blk |> ArrayBlk.offsetof in + let get_size v = v |> Val.get_array_blk |> ArrayBlk.sizeof in + let get_field_name (fn, _, _) = fn in + let deref_field v fn mem = + Mem.find_heap_set (PowLoc.append_field (Val.get_all_locs v) fn) mem + in + let deref_ptr v mem = Mem.find_heap_set (Val.get_all_locs v) mem in + let add_pair_itv itv1 itv2 l = + let open Itv in + if itv1 <> bot && itv2 <> bot then + (lb itv1, lb itv2) :: (ub itv1, ub itv2) :: l + else if itv1 <> bot && Itv.eq itv2 bot then + (lb itv1, Bound.Bot) :: (ub itv1, Bound.Bot) :: l + else + l + in + let add_pair_val v1 v2 pairs = + pairs + |> add_pair_itv (get_itv v1) (get_itv v2) + |> add_pair_itv (get_offset v1) (get_offset v2) + |> add_pair_itv (get_size v1) (get_size v2) + in + let add_pair_field v1 v2 pairs fn = + let v1' = deref_field v1 fn callee_mem in + let v2' = deref_field v2 fn caller_mem in + add_pair_val v1' v2' pairs + in + let add_pair_ptr typ v1 v2 pairs = + match typ with + | Typ.Tptr (Typ.Tstruct typename, _) -> + (match Tenv.lookup tenv typename with + | Some str -> + let fns = IList.map get_field_name str.StructTyp.fields in + IList.fold_left (add_pair_field v1 v2) pairs fns + | _ -> pairs) + | Typ.Tptr (_ ,_) -> + let v1' = deref_ptr v1 callee_mem in + let v2' = deref_ptr v2 caller_mem in + add_pair_val v1' v2' pairs + | _ -> pairs + in + [] |> add_pair_val formal actual |> add_pair_ptr typ formal actual + + let subst_map_of_pairs + : (Itv.Bound.t * Itv.Bound.t) list -> Itv.Bound.t Itv.SubstMap.t + = fun pairs -> + let add_pair map (formal, actual) = + match formal with + | Itv.Bound.Linear (0, se1) when Itv.SymLinear.cardinal se1 > 0 -> + let (symbol, coeff) = Itv.SymLinear.choose se1 in + if Int.equal coeff 1 + then Itv.SubstMap.add symbol actual map + else assert false + | _ -> assert false + in + IList.fold_left add_pair Itv.SubstMap.empty pairs + + let rec list_fold2_def + : Val.t -> ('a -> Val.t -> 'b -> 'b) -> 'a list -> Val.t list -> 'b -> 'b + = fun default f xs ys acc -> + match xs, ys with + | [x], _ -> f x (IList.fold_left Val.join Val.bot ys) acc + | [], _ -> acc + | x :: xs', [] -> list_fold2_def default f xs' ys (f x default acc) + | x :: xs', y :: ys' -> list_fold2_def default f xs' ys' (f x y acc) + + let get_subst_map + : Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate + -> Location.t -> Itv.Bound.t Itv.SubstMap.t + = fun tenv callee_pdesc params caller_mem callee_entry_mem loc -> + let add_pair (formal, typ) actual l = + let formal = Mem.find_heap (Loc.of_pvar formal) callee_entry_mem in + let new_matching = + get_matching_pairs tenv formal actual typ caller_mem callee_entry_mem + in + IList.append new_matching l + in + let formals = get_formals callee_pdesc in + let actuals = IList.map (fun (a, _) -> eval a caller_mem loc) params in + list_fold2_def Val.bot add_pair formals actuals [] + |> subst_map_of_pairs +end diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml new file mode 100644 index 000000000..6ebf89849 --- /dev/null +++ b/infer/src/bufferoverrun/itv.ml @@ -0,0 +1,1015 @@ +(* + * Copyright (c) 2016 - present + * + * Programming Research Laboratory (ROPAS) + * Seoul National University, Korea + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +module F = Format +module L = Logging + +let sym_size = ref 0 + +module Symbol = +struct + type t = Procname.t * int [@@deriving compare] + + let eq : t -> t -> bool + = fun x y -> compare x y = 0 + + let get_new : Procname.t -> t + = fun pname -> + let i = !sym_size in + sym_size := !sym_size + 1; + (pname, i) + + let make : Procname.t -> int -> t + = fun pname i -> (pname, i) + + let pp : F.formatter -> t -> unit + = fun fmt x -> + if Config.bo_debug <= 1 then + F.fprintf fmt "s$%d" (snd x) + else + F.fprintf fmt "%s-s$%d" (fst x |> Procname.to_string) (snd x) +end + +module SubstMap = Map.Make (Symbol) + +module SymLinear = +struct + module M = Map.Make (Symbol) + + type t = int M.t [@@deriving compare] + + let empty : t + = M.empty + + let add : Symbol.t -> int -> t -> t + = M.add + + let cardinal : t -> int + = M.cardinal + + let choose : t -> (Symbol.t * int) + = M.choose + + let fold : (Symbol.t -> int -> 'b -> 'b) -> t -> 'b -> 'b + = M.fold + + let mem : Symbol.t -> t -> bool + = M.mem + + let initial : t + = empty + + let find : Symbol.t -> t -> int + = fun s x -> + try M.find s x with + | Not_found -> 0 + + let le : t -> t -> bool + = fun x y -> M.for_all (fun s v -> v <= find s y) x + + let get_new : Procname.t -> t + = fun pname -> M.add (Symbol.get_new pname) 1 empty + + let make : Procname.t -> int -> t + = fun pname i -> M.add (Symbol.make pname i) 1 empty + + let eq : t -> t -> bool + = fun x y -> le x y && le y x + + let pp1 : F.formatter -> (Symbol.t * int) -> unit + = fun fmt (s, c) -> + if c = 0 then () + else if c = 1 then + F.fprintf fmt "%a" Symbol.pp s + else if c < 0 then + F.fprintf fmt "(%d)x%a" c Symbol.pp s + else + F.fprintf fmt "%dx%a" c Symbol.pp s + + let pp : F.formatter -> t -> unit + = fun fmt x -> + if M.cardinal x = 0 then F.fprintf fmt "empty" else + let (s1, c1) = M.min_binding x in + pp1 fmt (s1, c1); + M.iter (fun s c -> F.fprintf fmt " + %a" pp1 (s, c)) (M.remove s1 x) + + let zero : t + = M.empty + + let is_zero : t -> bool + = fun x -> M.for_all (fun _ v -> v = 0) x + + let is_mod_zero : t -> int -> bool + = fun x n -> + assert (n <> 0); + M.for_all (fun _ v -> v mod n = 0) x + + let neg : t -> t + = fun x -> M.map (~-) x + + (* Returns (Some n) only when n is not 0. *) + let is_non_zero : int -> int option + = fun n -> if n = 0 then None else Some n + + let plus : t -> t -> t + = fun x y -> + let plus' _ n_opt m_opt = + match n_opt, m_opt with + | None, None -> None + | Some v, None + | None, Some v -> is_non_zero v + | Some n, Some m -> is_non_zero (n + m) + in + M.merge plus' x y + + let minus : t -> t -> t + = fun x y -> + let minus' _ n_opt m_opt = + match n_opt, m_opt with + | None, None -> None + | Some v, None -> is_non_zero v + | None, Some v -> is_non_zero (-v) + | Some n, Some m -> is_non_zero (n - m) + in + M.merge minus' x y + + let mult_const : t -> int -> t + = fun x n -> M.map (( * ) n) x + + let div_const : t -> int -> t + = fun x n -> M.map ((/) n) x + + (* Returns a symbol when the map contains only one symbol s with the + coefficient 1. *) + let one_symbol : t -> Symbol.t option + = fun x -> + let x = M.filter (fun _ v -> v <> 0) x in + if M.cardinal x = 1 then + let (k, v) = M.choose x in + if v = 1 then Some k else None + else None + + let is_one_symbol : t -> bool + = fun x -> + match one_symbol x with + | Some _ -> true + | None -> false + + let get_symbols : t -> Symbol.t list + = fun x -> IList.map fst (M.bindings x) +end + +module Bound = +struct + type t = + | MInf + | Linear of int * SymLinear.t + | MinMax of min_max_t * int * Symbol.t + | PInf + | Bot + [@@deriving compare] +and min_max_t = Min | Max + +let pp_min_max : F.formatter -> min_max_t -> unit + = fun fmt -> function + | Min -> F.fprintf fmt "min" + | Max -> F.fprintf fmt "max" + + +let pp : F.formatter -> t -> unit + = fun fmt -> function + | MInf -> F.fprintf fmt "-oo" + | PInf -> F.fprintf fmt "+oo" + | Bot -> F.fprintf fmt "_|_" + | Linear (c, x) -> + if SymLinear.le x SymLinear.empty then + F.fprintf fmt "%d" c + else if c = 0 then + F.fprintf fmt "%a" SymLinear.pp x + else + F.fprintf fmt "%a + %d" SymLinear.pp x c + | MinMax (m, c, x) -> F.fprintf fmt "%a(%d, %a)" pp_min_max m c Symbol.pp x + +let of_int : int -> t + = fun n -> Linear (n, SymLinear.empty) + +let of_sym : SymLinear.t -> t + = fun s -> Linear (0, s) + +let is_symbolic : t -> bool + = function + | MInf | PInf | Bot -> false + | Linear (_, se) -> SymLinear.cardinal se > 0 + | MinMax _ -> true + +let opt_lift : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool + = fun f a_opt b_opt -> + match a_opt, b_opt with + | None, _ + | _, None -> false + | Some a, Some b -> f a b + +let eq_symbol : Symbol.t -> t -> bool + = fun s -> function + | Linear (c, se) -> + c = 0 && opt_lift Symbol.eq (SymLinear.one_symbol se) (Some s) + | _ -> false + +let one_symbol : t -> Symbol.t option + = function + | Linear (c, se) when c = 0 -> SymLinear.one_symbol se + | _ -> None + +let is_one_symbol : t -> bool + = fun x -> one_symbol x <> None + +let use_symbol : Symbol.t -> t -> bool + = fun s -> function + | PInf | MInf | Bot -> false + | Linear (_, se) -> SymLinear.find s se <> 0 + | MinMax (_, _, s') -> Symbol.eq s s' + +let subst1 : t -> t -> Symbol.t -> t -> t + = fun default x s y -> + if not (use_symbol s x) then x else + match x, y with + | _, _ when eq_symbol s x -> y + | Linear (c1, se1), Linear (c2, se2) -> + let coeff = SymLinear.find s se1 in + let c' = c1 + coeff * c2 in + let se1 = SymLinear.add s 0 se1 in + let se' = SymLinear.plus se1 (SymLinear.mult_const se2 coeff) in + Linear (c', se') + | MinMax (Min, _, s'), MInf when Symbol.eq s s' -> MInf + | MinMax (Max, c, s'), MInf when Symbol.eq s s' -> + Linear (c, SymLinear.zero) + | MinMax (Max, _, s'), PInf when Symbol.eq s s' -> PInf + | MinMax (Min, c, s'), PInf when Symbol.eq s s' -> + Linear (c, SymLinear.zero) + | MinMax (Min, c1, s'), Linear (c2, se) + when Symbol.eq s s' && SymLinear.is_zero se -> + Linear (min c1 c2, SymLinear.zero) + | MinMax (Max, c1, s'), Linear (c2, se) + when Symbol.eq s s' && SymLinear.is_zero se -> + Linear (max c1 c2, SymLinear.zero) + | MinMax (m, c, s'), _ when Symbol.eq s s' && is_one_symbol y -> + (match one_symbol y with + | Some s'' -> MinMax (m, c, s'') + | _ -> assert false) + | MinMax (Min, c1, s'), MinMax (Min, c2, s'') when Symbol.eq s s' -> + MinMax (Min, min c1 c2, s'') + | MinMax (Max, c1, s'), MinMax (Max, c2, s'') when Symbol.eq s s' -> + MinMax (Max, max c1 c2, s'') + | _ -> default + +(* substitution symbols in ``x'' with respect to ``map'' *) +let subst : t -> t -> t SubstMap.t -> t + = fun default x map -> SubstMap.fold (fun s y x -> subst1 default x s y) map x + +let le : t -> t -> bool + = fun x y -> + assert (x <> Bot && y <> Bot); + match x, y with + | MInf, _ + | _, PInf -> true + | _, MInf + | PInf, _ -> false + | Linear (c0, x0), Linear (c1, x1) -> c0 <= c1 && SymLinear.eq x0 x1 + | MinMax (Min, c0, x0), MinMax (Min, c1, x1) + | MinMax (Max, c0, x0), MinMax (Max, c1, x1) -> c0 <= c1 && Symbol.eq x0 x1 + | MinMax (Min, c0, x0), Linear (c1, x1) -> + (c0 <= c1 && SymLinear.is_zero x1) + || (c1 = 0 && opt_lift Symbol.eq (SymLinear.one_symbol x1) (Some x0)) + | Linear (c1, x1), MinMax (Max, c0, x0) -> + (c1 <= c0 && SymLinear.is_zero x1) + || (c1 = 0 && opt_lift Symbol.eq (SymLinear.one_symbol x1) (Some x0)) + | MinMax (Min, c0, x0), MinMax (Max, c1, x1) -> c0 <= c1 || Symbol.eq x0 x1 + | _, _ -> false + +let lt : t -> t -> bool + = fun x y -> + assert (x <> Bot && y <> Bot); + match x, y with + | MInf, Linear _ + | MInf, MinMax _ + | MInf, PInf + | Linear _, PInf + | MinMax _, PInf -> true + | Linear (c0, x0), Linear (c1, x1) -> c0 < c1 && SymLinear.eq x0 x1 + | MinMax (Min, c0, _), Linear (c1, x1) -> c0 < c1 && SymLinear.is_zero x1 + | Linear (c1, x1), MinMax (Max, c0, _) -> c1 < c0 && SymLinear.is_zero x1 + | MinMax (Min, c0, _), MinMax (Max, c1, _) -> c0 < c1 + | _, _ -> false + +let gt : t -> t -> bool + = fun x y -> lt y x + +let eq : t -> t -> bool + = fun x y -> + if x = Bot && y = Bot then true else + if x = Bot || y = Bot then false else + le x y && le y x + +let min : t -> t -> t + = fun x y -> + assert (x <> Bot && y <> Bot); + if le x y then x else + if le y x then y else + match x, y with + | Linear (c0, x0), Linear (c1, x1) + when SymLinear.is_zero x0 && c1 = 0 && SymLinear.is_one_symbol x1 -> + (match SymLinear.one_symbol x1 with + | Some x' -> MinMax (Min, c0, x') + | None -> assert false) + | Linear (c0, x0), Linear (c1, x1) + when SymLinear.is_zero x1 && c0 = 0 && SymLinear.is_one_symbol x0 -> + (match SymLinear.one_symbol x0 with + | Some x' -> MinMax (Min, c1, x') + | None -> assert false) + | MinMax (Max, c0, _), Linear (c1, x1) + | Linear (c1, x1), MinMax (Max, c0, _) + when SymLinear.is_zero x1 && c0 < c1 -> Linear (c0, x1) + | _, _ -> MInf + +let max : t -> t -> t + = fun x y -> + assert (x <> Bot && y <> Bot); + if le x y then y else + if le y x then x else + match x, y with + | Linear (c0, x0), Linear (c1, x1) + when SymLinear.is_zero x0 && c1 = 0 && SymLinear.is_one_symbol x1 -> + (match SymLinear.one_symbol x1 with + | Some x' -> MinMax (Max, c0, x') + | None -> assert false) + | Linear (c0, x0), Linear (c1, x1) + when SymLinear.is_zero x1 && c0 = 0 && SymLinear.is_one_symbol x0 -> + (match SymLinear.one_symbol x0 with + | Some x' -> MinMax (Max, c1, x') + | None -> assert false) + | MinMax (Min, c0, _), Linear (c1, x1) + | Linear (c1, x1), MinMax (Min, c0, _) + when SymLinear.is_zero x1 && c0 > c1 -> Linear (c0, x1) + | _, _ -> PInf + +let widen_l : t -> t -> t + = fun x y -> + assert (x <> Bot && y <> Bot); + if x = PInf || y = PInf then failwith "Lower bound cannot be +oo." else + if le x y then x else + MInf + +let widen_u : t -> t -> t + = fun x y -> + assert (x <> Bot && y <> Bot); + if x = MInf || y = MInf then failwith "Upper bound cannot be -oo." else + if le y x then x else + PInf + +let initial : t + = of_int 0 + +let zero : t + = Linear (0, SymLinear.zero) + +let one : t + = Linear (1, SymLinear.zero) + +let mone : t + = Linear (-1, SymLinear.zero) + +let is_zero : t -> bool + = fun x -> + assert (x <> Bot); + match x with + | Linear (c, y) -> c = 0 && SymLinear.is_zero y + | _ -> false + +let is_const : t -> int option + = fun x -> + assert (x <> Bot); + match x with + | Linear (c, y) when SymLinear.is_zero y -> Some c + | _ -> None + +let plus_l : t -> t -> t + = fun x y -> + assert (x <> Bot && y <> Bot); + match x, y with + | _, _ when is_zero x -> y + | _, _ when is_zero y -> x + | Linear (c1, x1), Linear (c2, x2) -> Linear (c1 + c2, SymLinear.plus x1 x2) + | MinMax (Max, c1, _), Linear (c2, x2) + | Linear (c2, x2), MinMax (Max, c1, _) -> Linear (c1 + c2, x2) + | _, _ -> MInf + +let plus_u : t -> t -> t + = fun x y -> + assert (x <> Bot && y <> Bot); + match x, y with + | _, _ when is_zero x -> y + | _, _ when is_zero y -> x + | Linear (c1, x1), Linear (c2, x2) -> Linear (c1 + c2, SymLinear.plus x1 x2) + | MinMax (Min, c1, _), Linear (c2, x2) + | Linear (c2, x2), MinMax (Min, c1, _) -> Linear (c1 + c2, x2) + | _, _ -> PInf + +let mult_const : t -> int -> t option + = fun x n -> + assert (x <> Bot); + assert (n <> 0); + match x with + | MInf -> Some (if n > 0 then MInf else PInf) + | PInf -> Some (if n > 0 then PInf else MInf) + | Linear (c, x') -> Some (Linear (c * n, SymLinear.mult_const x' n)) + | _ -> None + +let div_const : t -> int -> t option + = fun x n -> + assert (x <> Bot); + if n = 0 then Some zero else + match x with + | MInf -> Some (if n > 0 then MInf else PInf) + | PInf -> Some (if n > 0 then PInf else MInf) + | Linear (c, x') -> + if c mod n = 0 && SymLinear.is_mod_zero x' n then + Some (Linear (c / n, SymLinear.div_const x' n)) + else None + | _ -> None + +let neg : t -> t option + = function + | MInf -> Some PInf + | PInf -> Some MInf + | Linear (c, x) -> Some (Linear (-c, SymLinear.neg x)) + | MinMax _ -> None + | Bot -> assert false + +let make_min_max : min_max_t -> t -> t -> t option + = fun m x y -> + assert (x <> Bot && y <> Bot); + match x, y with + | Linear (cx, x'), Linear (cy, y') + when cy = 0 && SymLinear.is_zero x' && SymLinear.is_one_symbol y' -> + (match SymLinear.one_symbol y' with + | Some s -> Some (MinMax (m, cx, s)) + | None -> None) + | Linear (cx, x'), Linear (cy, y') + when cx = 0 && SymLinear.is_zero y' && SymLinear.is_one_symbol x' -> + (match SymLinear.one_symbol x' with + | Some s -> Some (MinMax (m, cy, s)) + | None -> None) + | _, _ -> None + +let make_min : t -> t -> t option + = make_min_max Min + +let make_max : t -> t -> t option + = make_min_max Max + +let get_symbols : t -> Symbol.t list + = function + | MInf | PInf -> [] + | Linear (_, se) -> SymLinear.get_symbols se + | MinMax (_, _, s) -> [s] + | Bot -> assert false + +let is_not_infty : t -> bool + = function + | MInf | PInf -> false + | _ -> true +end + +module ItvPure = +struct + type astate = Bound.t * Bound.t + [@@deriving compare] + + type t = astate + + let initial : t + = (Bound.initial, Bound.initial) + + let lb : t -> Bound.t + = fst + + let ub : t -> Bound.t + = snd + + let is_finite : t -> bool + = fun (l, u) -> + match Bound.is_const l, Bound.is_const u with + Some _, Some _ -> true + | _, _ -> false + + let make : Bound.t -> Bound.t -> t + = fun l u -> (l, u) + + let subst : t -> Bound.t SubstMap.t -> t + = fun x map -> + (Bound.subst Bound.MInf (lb x) map, Bound.subst Bound.PInf (ub x) map) + + let (<=) : lhs:t -> rhs:t -> bool + = fun ~lhs:(l1, u1) ~rhs:(l2, u2) -> Bound.le l2 l1 && Bound.le u1 u2 + + let join : t -> t -> t + = fun (l1, u1) (l2, u2) -> (Bound.min l1 l2, Bound.max u1 u2) + + let widen : prev:t -> next:t -> num_iters:int -> t + = fun ~prev:(l1, u1) ~next:(l2, u2) ~num_iters:_ -> + (Bound.widen_l l1 l2, Bound.widen_u u1 u2) + + let pp : F.formatter -> t -> unit + = fun fmt (l, u) -> F.fprintf fmt "[%a, %a]" Bound.pp l Bound.pp u + + let of_int : int -> t + = fun n -> (Bound.of_int n, Bound.of_int n) + + let get_new_sym : Procname.t -> t + = fun pname -> + let lower = Bound.of_sym (SymLinear.get_new pname) in + let upper = Bound.of_sym (SymLinear.get_new pname) in + (lower, upper) + + let make_sym : Procname.t -> int -> t + = fun pname i -> + let lower = Bound.of_sym (SymLinear.make pname i) in + let upper = Bound.of_sym (SymLinear.make pname (i+1)) in + (lower, upper) + + let top : t + = (Bound.MInf, Bound.PInf) + + let pos : t + = (Bound.of_int 1, Bound.PInf) + + let nat : t + = (Bound.of_int 0, Bound.PInf) + + let zero : t + = of_int 0 + + let one : t + = of_int 1 + + let true_sem : t + = one + + let false_sem : t + = zero + + let unknown_bool : t + = (Bound.of_int 0, Bound.of_int 1) + + let is_true : t -> bool + = fun (l, u) -> Bound.le (Bound.of_int 1) l || Bound.le u (Bound.of_int (-1)) + + let is_false : t -> bool + = fun (l, u) -> Bound.is_zero l && Bound.is_zero u + + let is_const : t -> int option + = fun (l, u) -> + match Bound.is_const l, Bound.is_const u with + | Some n, Some m when n = m -> Some n + | _, _ -> None + + let is_symbolic : t -> bool + = fun (lb, ub) -> Bound.is_symbolic lb || Bound.is_symbolic ub + + let neg : t -> t + = fun (l, u) -> + let l' = Option.default Bound.MInf (Bound.neg u) in + let u' = Option.default Bound.PInf (Bound.neg l) in + (l', u') + + let lnot : t -> t + = fun x -> + if is_true x then false_sem else + if is_false x then true_sem else + unknown_bool + + let plus : t -> t -> t + = fun (l1, u1) (l2, u2) -> (Bound.plus_l l1 l2, Bound.plus_u u1 u2) + + let minus : t -> t -> t + = fun i1 i2 -> plus i1 (neg i2) + + let mult_const : t -> int -> t + = fun (l, u) n -> + if n = 0 then zero else + if n > 0 then + let l' = Option.default Bound.MInf (Bound.mult_const l n) in + let u' = Option.default Bound.PInf (Bound.mult_const u n) in + (l', u') + else + let l' = Option.default Bound.MInf (Bound.mult_const u n) in + let u' = Option.default Bound.PInf (Bound.mult_const l n) in + (l', u') + + (* Returns a correct value only when all coefficients are divided by + n without remainder. *) + let div_const : t -> int -> t + = fun (l, u) n -> + assert (n <> 0); + if n > 0 then + let l' = Option.default Bound.MInf (Bound.div_const l n) in + let u' = Option.default Bound.PInf (Bound.div_const u n) in + (l', u') + else + let l' = Option.default Bound.MInf (Bound.div_const u n) in + let u' = Option.default Bound.PInf (Bound.div_const l n) in + (l', u') + + let mult : t -> t -> t + = fun x y -> + match is_const x, is_const y with + | _, Some n -> mult_const x n + | Some n, _ -> mult_const y n + | None, None -> top + + let div : t -> t -> t + = fun x y -> + match is_const y with + | Some n when n <> 0 -> div_const x n + | _ -> top + + (* x % [0,0] does nothing. *) + let mod_sem : t -> t -> t + = fun x y -> + match is_const x, is_const y with + | Some n, Some m -> if m = 0 then x else of_int (n mod m) + | _, Some m -> (Bound.of_int (-m), Bound.of_int m) + | _, None -> top + + (* x << [-1,-1] does nothing. *) + let shiftlt : t -> t -> t + = fun x y -> + match is_const y with + | Some n -> if n >= 0 then mult_const x (1 lsl n) else x + | None -> top + + (* x >> [-1,-1] does nothing. *) + let shiftrt : t -> t -> t + = fun x y -> + match is_const y with + | Some n -> if n >= 0 && n < 63 then div_const x (1 lsl n) else x + | None -> top + + let lt_sem : t -> t -> t + = fun (l1, u1) (l2, u2) -> + if Bound.lt u1 l2 then true_sem else + if Bound.le u2 l1 then false_sem else + unknown_bool + + let gt_sem : t -> t -> t + = fun x y -> lt_sem y x + + let le_sem : t -> t -> t + = fun (l1, u1) (l2, u2) -> + if Bound.le u1 l2 then true_sem else + if Bound.lt u2 l1 then false_sem else + unknown_bool + + let ge_sem : t -> t -> t + = fun x y -> le_sem y x + + let eq_sem : t -> t -> t + = fun (l1, u1) (l2, u2) -> + if Bound.eq l1 u1 && Bound.eq u1 l2 && Bound.eq l2 u2 then true_sem else + if Bound.lt u1 l2 || Bound.lt u2 l1 then false_sem else + unknown_bool + + let ne_sem : t -> t -> t + = fun (l1, u1) (l2, u2) -> + if Bound.eq l1 u1 && Bound.eq u1 l2 && Bound.eq l2 u2 then false_sem else + if Bound.lt u1 l2 || Bound.lt u2 l1 then true_sem else + unknown_bool + + let land_sem : t -> t -> t + = fun x y -> + if is_true x && is_true y then true_sem else + if is_false x || is_false y then false_sem else + unknown_bool + + let lor_sem : t -> t -> t + = fun x y -> + if is_true x || is_true y then true_sem else + if is_false x && is_false y then false_sem else + unknown_bool + + let invalid : t -> bool + = fun (l, u) -> + l = Bound.Bot || u = Bound.Bot + || Bound.eq l Bound.PInf || Bound.eq u Bound.MInf || Bound.lt u l + + let prune_le : t -> t -> t + = fun x y -> + match x, y with + | (l1, u1), (_, u2) when u1 = Bound.PInf -> (l1, u2) + | (l1, Bound.Linear (c1, s1)), (_, Bound.Linear (c2, s2)) + when SymLinear.eq s1 s2 -> + (l1, Bound.Linear (min c1 c2, s1)) + | (l1, Bound.Linear (c, se)), (_, u) + when SymLinear.is_zero se && Bound.is_one_symbol u -> + (match Bound.one_symbol u with + | Some s -> (l1, Bound.MinMax (Bound.Min, c, s)) + | None -> assert false) + | (l1, u), (_, Bound.Linear (c, se)) + when SymLinear.is_zero se && Bound.is_one_symbol u -> + (match Bound.one_symbol u with + | Some s -> (l1, Bound.MinMax (Bound.Min, c, s)) + | None -> assert false) + | (l1, Bound.Linear (c1, se)), (_, Bound.MinMax (Bound.Min, c2, se')) + | (l1, Bound.MinMax (Bound.Min, c1, se')), (_, Bound.Linear (c2, se)) + when SymLinear.is_zero se -> + (l1, Bound.MinMax (Bound.Min, min c1 c2, se')) + | (l1, Bound.MinMax (Bound.Min, c1, se1)), + (_, Bound.MinMax (Bound.Min, c2, se2)) + when Symbol.eq se1 se2 -> + (l1, Bound.MinMax (Bound.Min, min c1 c2, se1)) + | _ -> x + + let prune_ge : t -> t -> t + = fun x y -> + match x, y with + | (l1, u1), (l2, _) when l1 = Bound.MInf -> (l2, u1) + | (Bound.Linear (c1, s1), u1), (Bound.Linear (c2, s2), _) + when SymLinear.eq s1 s2 -> + (Bound.Linear (max c1 c2, s1), u1) + | (Bound.Linear (c, se), u1), (l, _) + when SymLinear.is_zero se && Bound.is_one_symbol l -> + (match Bound.one_symbol l with + | Some s -> (Bound.MinMax (Bound.Max, c, s), u1) + | None -> assert false) + | (l, u1), (Bound.Linear (c, se), _) + when SymLinear.is_zero se && Bound.is_one_symbol l -> + (match Bound.one_symbol l with + | Some s -> (Bound.MinMax (Bound.Max, c, s), u1) + | None -> assert false) + | (Bound.Linear (c1, se), u1), (Bound.MinMax (Bound.Max, c2, se'), _) + | (Bound.MinMax (Bound.Max, c1, se'), u1), (Bound.Linear (c2, se), _) + when SymLinear.is_zero se -> + (Bound.MinMax (Bound.Max, max c1 c2, se'), u1) + | (Bound.MinMax (Bound.Max, c1, se1), u1), + (Bound.MinMax (Bound.Max, c2, se2), _) + when Symbol.eq se1 se2 -> + (Bound.MinMax (Bound.Max, max c1 c2, se1), u1) + | _ -> x + + let prune_lt : t -> t -> t + = fun x y -> prune_le x (minus y one) + + let prune_gt : t -> t -> t + = fun x y -> prune_ge x (plus y one) + + let diff : t -> Bound.t -> t + = fun (l, u) b -> + if Bound.eq l b then (Bound.plus_l l Bound.one, u) else + if Bound.eq u b then (l, Bound.plus_u u Bound.mone) else + (l, u) + + let prune_zero : t -> t + = fun x -> diff x Bound.zero + + let prune_comp : Binop.t -> t -> t -> t option + = fun c x y -> + if invalid y then Some x else + let x = + match c with + | Binop.Le -> prune_le x y + | Binop.Ge -> prune_ge x y + | Binop.Lt -> prune_lt x y + | Binop.Gt -> prune_gt x y + | _ -> assert false + in + if invalid x then None else Some x + + let prune_eq : t -> t -> t option + = fun x y -> + match prune_comp Binop.Le x y with + | None -> None + | Some x' -> prune_comp Binop.Ge x' y + + let prune_ne : t -> t -> t option + = fun x (l, u) -> + if invalid (l, u) then Some x else + let x = if Bound.eq l u then diff x l else x in + if invalid x then None else Some x + + let get_symbols : t -> Symbol.t list + = fun (l, u) -> + IList.append (Bound.get_symbols l) (Bound.get_symbols u) + + let normalize : t -> t option + = fun (l, u) -> + if invalid (l,u) then None + else Some (l, u) + + let has_bnd_bot : t -> bool + = fun (l, u) -> + l = Bound.Bot || u = Bound.Bot +end + +include AbstractDomain.BottomLifted (ItvPure) + +type t = astate + +let compare : t -> t -> int + = fun x y -> + match x, y with + | Bottom, Bottom -> 0 + | Bottom, _ -> -1 + | _, Bottom -> 1 + | NonBottom x, NonBottom y -> ItvPure.compare_astate x y + +let compare_astate = compare + +let bot : t + = Bottom + +let top : t + = NonBottom ItvPure.top + +let lb : t -> Bound.t + = function + | NonBottom x -> ItvPure.lb x + | _ -> raise (Failure "lower bound of bottom") + +let ub : t -> Bound.t + = function + | NonBottom x -> ItvPure.ub x + | _ -> raise (Failure "upper bound of bottom") + +let of_int : int -> astate + = fun n -> NonBottom (ItvPure.of_int n) + +let is_bot : t -> bool + = fun x -> x = Bottom + +let is_finite : t -> bool + = function + | NonBottom x -> ItvPure.is_finite x + | Bottom -> false + +let zero : t + = of_int 0 + +let one : t + = of_int 1 + +let pos : t + = NonBottom ItvPure.pos + +let nat : t + = NonBottom ItvPure.nat + +let make : Bound.t -> Bound.t -> t + = fun l u -> if Bound.lt u l then Bottom else NonBottom (ItvPure.make l u) + +let invalid : t -> bool + = function + | NonBottom x -> ItvPure.invalid x + | Bottom -> false + +let is_symbolic : t -> bool + = function + | NonBottom x -> ItvPure.is_symbolic x + | Bottom -> false + +let le : lhs:t -> rhs:t -> bool + = (<=) + +let eq : t -> t -> bool + = fun x y -> (<=) ~lhs:x ~rhs:y && (<=) ~lhs:y ~rhs:x + +let to_string : t -> string + = fun x -> + pp F.str_formatter x; + F.flush_str_formatter () + +let lift1 : (ItvPure.t -> ItvPure.t) -> t -> t + = fun f -> function + | Bottom -> Bottom + | NonBottom x -> NonBottom (f x) + +let lift1_opt : (ItvPure.t -> ItvPure.t option) -> t -> t + = fun f -> function + | Bottom -> Bottom + | NonBottom x -> + (match f x with + | None -> Bottom + | Some v -> NonBottom v) + +let lift2 : (ItvPure.t -> ItvPure.t -> ItvPure.t) -> t -> t -> t + = fun f x y -> + match x, y with + | Bottom, _ + | _, Bottom -> Bottom + | NonBottom x, NonBottom y -> NonBottom (f x y) + +let lift2_opt : (ItvPure.t -> ItvPure.t -> ItvPure.t option) -> t -> t -> t + = fun f x y -> + match x, y with + | Bottom, _ + | _, Bottom -> Bottom + | NonBottom x, NonBottom y -> + (match f x y with + | Some v -> NonBottom v + | None -> Bottom) + +let plus : t -> t -> t + = lift2 ItvPure.plus + +let minus : t -> t -> t + = lift2 ItvPure.minus + +let get_new_sym : Procname.t -> t + = fun pname -> NonBottom (ItvPure.get_new_sym pname) + +let make_sym : Procname.t -> int -> t + = fun pname i -> NonBottom (ItvPure.make_sym pname i) + +let neg : t -> t + = lift1 ItvPure.neg + +let lnot : t -> t + = lift1 ItvPure.lnot + +let mult : t -> t -> t + = lift2 ItvPure.mult + +let div : t -> t -> t + = lift2 ItvPure.div + +let mod_sem : t -> t -> t + = lift2 ItvPure.mod_sem + +let shiftlt : t -> t -> t + = lift2 ItvPure.shiftlt + +let shiftrt : t -> t -> t + = lift2 ItvPure.shiftrt + +let lt_sem : t -> t -> t + = lift2 ItvPure.lt_sem + +let gt_sem : t -> t -> t + = lift2 ItvPure.gt_sem + +let le_sem : t -> t -> t + = lift2 ItvPure.le_sem + +let ge_sem : t -> t -> t + = lift2 ItvPure.ge_sem + +let eq_sem : t -> t -> t + = lift2 ItvPure.eq_sem + +let ne_sem : t -> t -> t + = lift2 ItvPure.ne_sem + +let land_sem : t -> t -> t + = lift2 ItvPure.land_sem + +let lor_sem : t -> t -> t + = lift2 ItvPure.lor_sem + +let prune_zero : t -> t + = lift1 ItvPure.prune_zero + +let prune_comp : Binop.t -> t -> t -> t + = fun comp -> lift2_opt (ItvPure.prune_comp comp) + +let prune_eq : t -> t -> t + = lift2_opt ItvPure.prune_eq + +let prune_ne : t -> t -> t + = lift2_opt ItvPure.prune_ne + +let subst : t -> Bound.t SubstMap.t -> t + = fun x map -> + match x with + | NonBottom x' -> NonBottom (ItvPure.subst x' map) + | _ -> x + +let get_symbols : t -> Symbol.t list + = function + | Bottom -> [] + | NonBottom x -> ItvPure.get_symbols x + +let normalize : t -> t + = lift1_opt ItvPure.normalize + +let has_bnd_bot : t -> bool + = function + | Bottom -> false + | NonBottom x -> ItvPure.has_bnd_bot x diff --git a/infer/src/checkers/AbstractInterpreter.ml b/infer/src/checkers/AbstractInterpreter.ml index 416aaf557..1aa6994e0 100644 --- a/infer/src/checkers/AbstractInterpreter.ml +++ b/infer/src/checkers/AbstractInterpreter.ml @@ -69,7 +69,7 @@ module MakeNoCFG | Some state -> Some state.pre | None -> None - let exec_node node astate_pre work_queue inv_map proc_data = + let exec_node node astate_pre work_queue inv_map ({ ProcData.pdesc; } as proc_data) = let node_id = CFG.id node in let update_inv_map pre visit_count = let compute_post (pre, inv_map) (instr, id_opt) = @@ -101,7 +101,10 @@ module MakeNoCFG then let old_state = InvariantMap.find node_id inv_map in let widened_pre = - Domain.widen ~prev:old_state.pre ~next:astate_pre ~num_iters:old_state.visit_count in + if CFG.is_loop_head pdesc node + then Domain.widen ~prev:old_state.pre ~next:astate_pre ~num_iters:old_state.visit_count + else astate_pre + in if Domain.(<=) ~lhs:widened_pre ~rhs:old_state.pre then inv_map, work_queue else update_inv_map widened_pre (old_state.visit_count + 1) diff --git a/infer/src/checkers/procCfg.ml b/infer/src/checkers/procCfg.ml index 6ff1ccdb9..0ab158eb2 100644 --- a/infer/src/checkers/procCfg.ml +++ b/infer/src/checkers/procCfg.ml @@ -23,6 +23,7 @@ module type Node = sig val kind : t -> Procdesc.Node.nodekind val id : t -> id + val hash : t -> int val loc : t -> Location.t val underlying_node : t -> Procdesc.Node.t val compare_id : id -> id -> int @@ -35,6 +36,7 @@ module DefaultNode = struct let kind = Procdesc.Node.get_kind let id = Procdesc.Node.get_id + let hash = Procdesc.Node.hash let loc = Procdesc.Node.get_loc let underlying_node t = t let compare_id = Procdesc.Node.compare_id @@ -51,6 +53,8 @@ module InstrNode = struct let id t = Procdesc.Node.get_id (underlying_node t), Node_index + let hash node = Hashtbl.hash (id node) + let loc t = Procdesc.Node.get_loc t let compare_index = compare_index @@ -105,6 +109,8 @@ module type S = sig val nodes : t -> node list val from_pdesc : Procdesc.t -> t + + val is_loop_head : Procdesc.t -> node -> bool end (** Forward CFG with no exceptional control-flow *) @@ -127,6 +133,7 @@ module Normal = struct let proc_desc t = t let nodes = Procdesc.get_nodes let from_pdesc pdesc = pdesc + let is_loop_head = Procdesc.is_loop_head end (** Forward CFG with exceptional control-flow *) @@ -195,6 +202,7 @@ module Exceptional = struct let proc_desc (pdesc, _) = pdesc let start_node (pdesc, _) = Procdesc.get_start_node pdesc let exit_node (pdesc, _) = Procdesc.get_exit_node pdesc + let is_loop_head = Procdesc.is_loop_head end (** Wrapper that reverses the direction of the CFG *) diff --git a/infer/src/checkers/procCfg.mli b/infer/src/checkers/procCfg.mli index 499a7f840..40960bf66 100644 --- a/infer/src/checkers/procCfg.mli +++ b/infer/src/checkers/procCfg.mli @@ -21,6 +21,7 @@ module type Node = sig val kind : t -> Procdesc.Node.nodekind val id : t -> id + val hash : t -> int val loc : t -> Location.t val underlying_node : t -> Procdesc.Node.t val compare_id : id -> id -> int @@ -67,6 +68,8 @@ module type S = sig val nodes : t -> node list val from_pdesc : Procdesc.t -> t + + val is_loop_head : Procdesc.t -> node -> bool end module DefaultNode : Node with type t = Procdesc.Node.t and type id = Procdesc.Node.id diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 91cb88e69..462c2eeeb 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -39,6 +39,7 @@ let active_procedure_checkers () = RepeatedCallsChecker.callback_check_repeated_calls, checkers_enabled; PrintfArgs.callback_printf_args, checkers_enabled; AnnotationReachability.Interprocedural.check_and_report, checkers_enabled; + BufferOverrunChecker.checker, Config.bufferoverrun; ] in (* make sure SimpleChecker.ml is not dead code *) if false then (let module SC = SimpleChecker.Make in ()); @@ -51,6 +52,7 @@ let active_procedure_checkers () = Checkers.callback_print_access_to_globals, false; ClangTaintAnalysis.checker, Config.quandary; Siof.checker, checkers_enabled; + BufferOverrunChecker.checker, Config.bufferoverrun; ] in IList.map (fun (x, y) -> (x, y, Some Config.Clang)) l in diff --git a/infer/src/integration/Buck.ml b/infer/src/integration/Buck.ml index e4b6f5e0f..600554604 100644 --- a/infer/src/integration/Buck.ml +++ b/infer/src/integration/Buck.ml @@ -44,7 +44,7 @@ let add_flavor_to_target target = Some "infer-capture-all" | Checkers | Infer -> Some "infer" - | Eradicate | Tracing | Crashcontext | Quandary | Threadsafety -> + | Eradicate | Tracing | Crashcontext | Quandary | Threadsafety | Bufferoverrun -> failwithf "Unsupported infer analyzer with Buck flavors: %s" (Config.string_of_analyzer Config.analyzer) in if List.exists ~f:(String.is_prefix ~prefix:"infer") target.flavors then diff --git a/infer/src/unit/schedulerTests.ml b/infer/src/unit/schedulerTests.ml index b627b3cda..c5b22e20b 100644 --- a/infer/src/unit/schedulerTests.ml +++ b/infer/src/unit/schedulerTests.ml @@ -20,6 +20,7 @@ module MockNode = struct let instrs _ = [] let instr_ids _ = [] + let hash = Hashtbl.hash let to_instr_nodes _ = assert false let id n = n let loc _ = assert false @@ -68,6 +69,7 @@ module MockProcCfg = struct let exit_node _ = assert false let proc_desc _ = assert false let from_pdesc _ = assert false + let is_loop_head _ = assert false end module S = Scheduler.ReversePostorder (MockProcCfg) diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/Makefile b/infer/tests/codetoanalyze/c/bufferoverrun/Makefile new file mode 100644 index 000000000..5e1e03985 --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/Makefile @@ -0,0 +1,30 @@ +# Copyright (c) 2016 - present +# +# Programming Research Laboratory (ROPAS) +# Seoul National University, Korea +# All rights reserved. +# +# This source code is licensed under the BSD style license found in the +# LICENSE file in the root directory of this source tree. An additional grant +# of patent rights can be found in the PATENTS file in the same directory. + +TESTS_DIR = ../../.. + +ANALYZER = bufferoverrun +CLANG_OPTIONS = -c +INFER_OPTIONS = -nf --project-root $(TESTS_DIR) +INFERPRINT_OPTIONS = --issues-tests + +SOURCES = \ + trivial.c \ + function_call.c \ + for_loop.c \ + while_loop.c \ + do_while.c \ + nested_loop.c \ + nested_loop_with_label.c \ + break_continue_return.c \ + goto_loop.c \ + inf_loop.c + +include $(TESTS_DIR)/clang.make diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/break_continue_return.c b/infer/tests/codetoanalyze/c/bufferoverrun/break_continue_return.c new file mode 100644 index 000000000..f231a50c3 --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/break_continue_return.c @@ -0,0 +1,33 @@ +/* + * Copyright (c) 2016 - present + * + * Programming Research Laboratory (ROPAS) + * Seoul National University, Korea + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +int break_continue_return() { + int i = 0; + char a[10]; + + while (1) { + i++; + if (i >= 10) + break; + if (i < 2) + continue; + a[i] = 'a'; /* SAFE */ + } + i = 0; + while (1) { + if (i > 10) + return 0; + a[i] = 'a'; /* BUG */ + i++; + } + return 0; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/do_while.c b/infer/tests/codetoanalyze/c/bufferoverrun/do_while.c new file mode 100644 index 000000000..df0783dc2 --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/do_while.c @@ -0,0 +1,27 @@ +/* + * Copyright (c) 2016 - present + * + * Programming Research Laboratory (ROPAS) + * Seoul National University, Korea + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +#include + +void do_while_sub(char* a, int len) { + int i = 0; + do { + a[i] = i; + i++; + } while (i < len); +} + +void do_while() { + char* a = malloc(10); + do_while_sub(a, 10); /* SAFE */ + do_while_sub(a, 11); /* BUG */ +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c b/infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c new file mode 100644 index 000000000..1077c9d71 --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c @@ -0,0 +1,40 @@ +/* + * Copyright (c) 2016 - present + * + * Programming Research Laboratory (ROPAS) + * Seoul National University, Korea + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +#include + +char* safealloc(int n) { + char* x; + if (n > 0) + x = malloc(n); + else + x = malloc(10); + + if (!x) + return x; + else + exit(1); +} + +void for_loop() { + char* a; + int i; + + a = safealloc(10); + for (i = 0; i < 10; i++) { + a[i] = 'a'; /* SAFE */ + } + a = safealloc(5); + for (i = 0; i < 10; i++) { + a[i] = 'a'; /* BUG */ + } +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/function_call.c b/infer/tests/codetoanalyze/c/bufferoverrun/function_call.c new file mode 100644 index 000000000..fe4d92d47 --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/function_call.c @@ -0,0 +1,26 @@ +/* + * Copyright (c) 2016 - present + * + * Programming Research Laboratory (ROPAS) + * Seoul National University, Korea + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +#include + +void arr_access(int* arr, char* p, int i) { + int x = arr[0]; + arr[x] = 1; /* BUG */ + *(p + i) = 'a'; /* BUG */ +} + +void function_call() { + int arr[10]; + arr[0] = 100; + char* p = malloc(10); + arr_access(arr, p, 20); +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/goto_loop.c b/infer/tests/codetoanalyze/c/bufferoverrun/goto_loop.c new file mode 100644 index 000000000..136697f39 --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/goto_loop.c @@ -0,0 +1,25 @@ +/* + * Copyright (c) 2016 - present + * + * Programming Research Laboratory (ROPAS) + * Seoul National University, Korea + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +void goto_loop() { + int i = 0; + char a[10]; + +loop_start: + if (i >= 10) + goto loop_end; + a[i] = 'a'; /* SAFE */ + i++; + goto loop_start; +loop_end: + a[i] = 'a'; /* BUG */ +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/inf_loop.c b/infer/tests/codetoanalyze/c/bufferoverrun/inf_loop.c new file mode 100644 index 000000000..b7166523f --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/inf_loop.c @@ -0,0 +1,23 @@ +/* + * Copyright (c) 2016 - present + * + * Programming Research Laboratory (ROPAS) + * Seoul National University, Korea + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +void inf_loop() { + int i = 0; + char a[10]; + + while (1) { + if (i >= 10) + i = 0; + a[i] = 'a'; /* SAFE */ + i++; + } +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp new file mode 100644 index 000000000..a1ff4b301 --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -0,0 +1,11 @@ +codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN, [Offset : [0, 10] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/break_continue_return.c:29:5] +codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call do_while_sub() ] +codetoanalyze/c/bufferoverrun/do_while.c, do_while, 3, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call do_while_sub() ] +codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN, [Offset : [0, 9] Size : [5, 10] @ codetoanalyze/c/bufferoverrun/for_loop.c:38:5] +codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset : [100, 100] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:17:3 by call arr_access() ] +codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset : [20, 20] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:18:3 by call arr_access() ] +codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offset : [10, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/goto_loop.c:24:3] +codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset : [0, 10] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop.c:20:7] +codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c:19:5] +codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [Offset : [10, 10] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/trivial.c:15:3] +codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/while_loop.c:18:10] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/nested_loop.c b/infer/tests/codetoanalyze/c/bufferoverrun/nested_loop.c new file mode 100644 index 000000000..782719f1a --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/nested_loop.c @@ -0,0 +1,23 @@ +/* + * Copyright (c) 2016 - present + * + * Programming Research Laboratory (ROPAS) + * Seoul National University, Korea + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +void nested_loop() { + int i, j; + char a[10]; + + for (i = 0; i < 10; i++) { + a[i] = 'a'; /* SAFE */ + for (j = 0; j <= 10; j++) { + a[j] = 'a'; /* BUG */ + } + } +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/nested_loop_with_label.c b/infer/tests/codetoanalyze/c/bufferoverrun/nested_loop_with_label.c new file mode 100644 index 000000000..a4203f391 --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/nested_loop_with_label.c @@ -0,0 +1,25 @@ +/* + * Copyright (c) 2016 - present + * + * Programming Research Laboratory (ROPAS) + * Seoul National University, Korea + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +void nested_loop_with_label() { + int i, j = 0; + char a[10]; + + for (i = 0; i < 10; i++) { + outer_loop: + a[j] = 'a'; /* BUG */ + for (j = 0; j <= 10; j++) { + if (j >= 10) + goto outer_loop; + } + } +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/trivial.c b/infer/tests/codetoanalyze/c/bufferoverrun/trivial.c new file mode 100644 index 000000000..a97f8c585 --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/trivial.c @@ -0,0 +1,16 @@ +/* + * Copyright (c) 2016 - present + * + * Programming Research Laboratory (ROPAS) + * Seoul National University, Korea + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +void trivial() { + int a[10]; + a[10] = 0; /* BUG */ +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c b/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c new file mode 100644 index 000000000..6d8a9a080 --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c @@ -0,0 +1,20 @@ +/* + * Copyright (c) 2016 - present + * + * Programming Research Laboratory (ROPAS) + * Seoul National University, Korea + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +char* safealloc(int n); + +void while_loop() { + int i = 0; + char* a = safealloc(10); + while (*(a + i) && i < 10) /* BUG */ + a[i++] = 1; /* SAFE */ +}