From 06a04ca9f58b2847a9aa9441563fe33728d32aa5 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 12 Jul 2018 09:42:38 -0700 Subject: [PATCH] Revert "[Inferbo] Add relational domain" Summary: This reverts commit "[Inferbo] Add relational domain" due to linking issues. Reviewed By: mbouaziz Differential Revision: D8821355 fbshipit-source-id: b39bfa6 --- Makefile.autoconf.in | 4 - configure.ac | 2 - infer/src/absint/AbstractInterpreter.ml | 2 +- infer/src/base/Config.ml | 9 - infer/src/base/Config.mli | 2 - infer/src/bufferoverrun/absLoc.ml | 11 - .../src/bufferoverrun/bufferOverrunChecker.ml | 76 +- .../src/bufferoverrun/bufferOverrunDomain.ml | 207 +-- .../bufferOverrunDomainRelation.ml | 1623 ----------------- .../src/bufferoverrun/bufferOverrunModels.ml | 18 +- .../bufferOverrunProofObligations.ml | 95 +- .../bufferoverrun/bufferOverrunSemantics.ml | 115 +- infer/src/bufferoverrun/bufferOverrunUtils.ml | 44 +- .../src/bufferoverrun/bufferOverrunUtils.mli | 4 +- infer/src/bufferoverrun/itv.ml | 2 - infer/src/bufferoverrun/itv.mli | 2 - infer/src/checkers/cost.ml | 2 +- infer/src/deadcode/jbuild.in | 4 +- infer/src/jbuild.common.in | 3 - infer/src/jbuild.in | 3 +- .../codetoanalyze/c/bufferoverrun/issues.exp | 4 - .../codetoanalyze/c/bufferoverrun/relation.c | 43 - opam | 4 - opam.lock | 7 - 24 files changed, 132 insertions(+), 2154 deletions(-) delete mode 100644 infer/src/bufferoverrun/bufferOverrunDomainRelation.ml delete mode 100644 infer/tests/codetoanalyze/c/bufferoverrun/relation.c diff --git a/Makefile.autoconf.in b/Makefile.autoconf.in index 061a908ee..4faf1d9dd 100644 --- a/Makefile.autoconf.in +++ b/Makefile.autoconf.in @@ -18,7 +18,6 @@ CFLAGS = @CFLAGS@ CLANG_INCLUDES = @CLANG_INCLUDES@ CLANG_PREFIX = @CLANG_PREFIX@ CMAKE = @CMAKE@ -CPATH = @CPATH@ CPP = @CPP@ CXX = @CXX@ CXXFLAGS = @CXXFLAGS@ @@ -43,7 +42,6 @@ LDFLAGS = @LDFLAGS@ libdir = @libdir@ # override in your `make` command to make the install relocatable libdir_relative_to_bindir = $(libdir) -LIBRARY_PATH = @LIBRARY_PATH@ LIBS = @LIBS@ mandir = @mandir@ MENHIR = @MENHIR@ @@ -81,7 +79,5 @@ endif # Export parts of the config relevant to running other programs export PATH := $(PATH) -export CPATH := $(CPATH) -export LIBRARY_PATH := $(LIBRARY_PATH) export CAML_LD_LIBRARY_PATH := $(CAML_LD_LIBRARY_PATH) export OPAMROOT := $(OPAMROOT) diff --git a/configure.ac b/configure.ac index 8a5aa0410..2b1b8cd2b 100644 --- a/configure.ac +++ b/configure.ac @@ -192,8 +192,6 @@ AC_ASSERT_OCAML_PKG([oUnit], [], [2.0.0]) AC_CHECK_TOOL([UTOP], [utop], [no]) AC_ASSERT_OCAML_PKG([yojson]) -AC_ARG_VAR([CPATH], [Additional directories to search for C headers.]) -AC_ARG_VAR([LIBRARY_PATH], [Additional directories to search for C shared objects.]) AC_ARG_VAR([CAML_LD_LIBRARY_PATH], [Additional directories to search for dynamically-loaded libraries.]) AC_ARG_VAR([OPAMROOT], [Root of the local opam installation.]) diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 7a0ff2acf..bfc9a27e5 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -93,7 +93,7 @@ struct in if debug then ( L.d_strln - (Format.asprintf "@[PRE: %a@]@\n@[INSTRS: %a@]@[POST: %a@]@." Domain.pp pre + (Format.asprintf "PRE: %a@.INSTRS: %aPOST: %a@." Domain.pp pre (Instrs.pp Pp.(html Green)) instrs Domain.pp astate_post) ; NodePrinter.finish_session (Node.underlying_node node) ) ; diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index f8b118e5b..03af48298 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -823,13 +823,6 @@ and blacklist = ~meta:"regex" "Skip analysis of files matched by the specified regular expression" -and bo_relational_domain = - CLOpt.mk_symbol_opt ~long:"bo-relational-domain" - ~in_help:InferCommand.[(Analyze, manual_buffer_overrun)] - ~symbols:[("oct", `Bo_relational_domain_oct); ("poly", `Bo_relational_domain_poly)] - "Select a relational domain being used in the bufferoverrun checker (experimental)" - - and bootclasspath = CLOpt.mk_string_opt ~long:"bootclasspath" ~in_help:InferCommand.[(Capture, manual_java)] @@ -2452,8 +2445,6 @@ and bootclasspath = !bootclasspath and bo_debug = !bo_debug -and bo_relational_domain = !bo_relational_domain - and buck = !buck and buck_build_args = !buck_build_args diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index af5f9ae38..4c4b38ee7 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -242,8 +242,6 @@ val bootclasspath : string option val bo_debug : int -val bo_relational_domain : [`Bo_relational_domain_oct | `Bo_relational_domain_poly] option - val buck : bool val buck_build_args : string list diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 1b6f2023e..5940c7e49 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -42,8 +42,6 @@ module Loc = struct F.fprintf fmt "%a.%a" pp l Typ.Fieldname.pp f - let to_string x = F.asprintf "%a" pp x - let is_var = function Var _ -> true | _ -> false let rec contains_allocsite = function @@ -91,12 +89,3 @@ module PowLoc = struct let is_singleton x = Int.equal (cardinal x) 1 end - -(** unsound but ok for bug catching *) -let always_strong_update = true - -let can_strong_update : PowLoc.t -> bool = - fun ploc -> - if always_strong_update then true - else if Int.equal (PowLoc.cardinal ploc) 1 then Loc.is_var (PowLoc.choose ploc) - else false diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index a96bd3177..b58716146 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -13,7 +13,6 @@ open AbsLoc open! AbstractDomain.Types module BoUtils = BufferOverrunUtils module Dom = BufferOverrunDomain -module Relation = BufferOverrunDomainRelation module L = Logging module Models = BufferOverrunModels module Sem = BufferOverrunSemantics @@ -48,16 +47,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Typ.Tint ikind -> let unsigned = Typ.ikind_is_unsigned ikind in let v = - Dom.Val.make_sym ~unsigned loc pname path new_sym_num + Dom.Val.make_sym ~unsigned pname path new_sym_num |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location)) in - mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc + Dom.Mem.add_heap loc v mem | Typ.Tfloat _ -> let v = - Dom.Val.make_sym loc pname path new_sym_num + Dom.Val.make_sym pname path new_sym_num |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location)) in - mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc + Dom.Mem.add_heap loc v mem | Typ.Tptr (typ, _) -> BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname path tenv ~node_hash location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem @@ -183,12 +182,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct try List.fold2_exn formals actuals ~init:mem ~f with Invalid_argument _ -> mem - let forget_ret_relation ret callee_pname mem = - let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in - let ret_var = Loc.of_var (Var.of_id (fst ret)) in - Dom.Mem.forget_locs (PowLoc.add ret_loc (PowLoc.singleton ret_var)) mem - - let instantiate_mem : Tenv.t -> Ident.t * Typ.t -> Procdesc.t option -> Typ.Procname.t -> (Exp.t * Typ.t) list -> Dom.Mem.astate -> Dom.Summary.t -> Location.t -> Dom.Mem.astate = @@ -198,17 +191,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let callee_ret_alias = Dom.Mem.find_ret_alias callee_exit_mem in match callee_pdesc with | Some pdesc -> - let bound_subst_map, ret_alias, rel_subst_map = + let subst_map, ret_alias = Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias in - let caller_mem = - instantiate_ret ret callee_pname ~callee_entry_mem ~callee_exit_mem bound_subst_map - caller_mem ret_alias location - |> instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem bound_subst_map - location - |> forget_ret_relation ret callee_pname - in - Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem + instantiate_ret ret callee_pname ~callee_entry_mem ~callee_exit_mem subst_map caller_mem + ret_alias location + |> instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map location | None -> caller_mem @@ -236,14 +224,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Store (exp1, _, exp2, location) -> let locs = Sem.eval exp1 mem |> Dom.Val.get_all_locs in let v = Sem.eval exp2 mem |> Dom.Val.add_trace_elem (Trace.Assign location) in - let mem = - let sym_exps = - Dom.Relation.SymExp.of_exps ~get_int_sym_f:(Sem.get_sym_f mem) - ~get_offset_sym_f:(Sem.get_offset_sym_f mem) - ~get_size_sym_f:(Sem.get_size_sym_f mem) exp2 - in - Dom.Mem.store_relation locs sym_exps mem - in let mem = Dom.Mem.update_mem locs v mem in let mem = if PowLoc.is_singleton locs then @@ -384,9 +364,7 @@ module Report = struct fun pname ~is_plus ~e1 ~e2 location mem cond_set -> let arr = Sem.eval e1 mem in let idx = Sem.eval e2 mem in - let idx_sym_exp = Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f mem) e2 in - let relation = Dom.Mem.get_relation mem in - BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus pname location cond_set + BoUtils.Check.array_access ~arr ~idx ~is_plus pname location cond_set let check_binop @@ -425,10 +403,7 @@ module Report = struct match exp with | Exp.Var _ -> let arr = Sem.eval exp mem in - let idx, idx_sym_exp = (Dom.Val.Itv.zero, Some Relation.SymExp.zero) in - let relation = Dom.Mem.get_relation mem in - BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true pname location - cond_set + BoUtils.Check.array_access ~arr ~idx:Dom.Val.Itv.zero ~is_plus:true pname location cond_set | Exp.BinOp (bop, e1, e2) -> check_binop pname ~bop ~e1 ~e2 location mem cond_set | _ -> @@ -443,13 +418,11 @@ module Report = struct let callee_cond = Dom.Summary.get_cond_set summary in match callee_pdesc with | Some pdesc -> - let bound_subst_map, _, rel_subst_map = + let subst_map, _ = Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias:None in let pname = Procdesc.get_proc_name pdesc in - let caller_rel = Dom.Mem.get_relation caller_mem in - PO.ConditionSet.subst callee_cond bound_subst_map rel_subst_map caller_rel caller_pname - pname location + PO.ConditionSet.subst callee_cond subst_map caller_pname pname location | _ -> callee_cond @@ -585,9 +558,6 @@ module Report = struct Reporting.log_error summary ~loc:location ~ltr:trace exn in PO.ConditionSet.check_all ~report cond_set - - - let forget_locs = PO.ConditionSet.forget_locs end let extract_pre = Analyzer.extract_pre @@ -600,34 +570,16 @@ let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit = "@\n@[Summary of %a:@,%a@]@." Typ.Procname.pp proc_name Dom.Summary.pp_summary s -let get_local_decls cfg = - let accum_pvar_list acc pvars = - List.fold pvars ~init:acc ~f:(fun acc (pvar, _) -> PowLoc.add (Loc.of_pvar pvar) acc) - in - let accum_decls_of_instr acc instr = - match instr with Sil.Declare_locals (vars, _) -> accum_pvar_list acc vars | _ -> acc - in - let accum_decls_of_node acc node = - Instrs.fold (CFG.instrs node) ~init:acc ~f:accum_decls_of_instr - in - let decls = CFG.fold_nodes cfg ~init:PowLoc.empty ~f:accum_decls_of_node in - let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar (Procdesc.get_proc_name cfg)) in - PowLoc.remove ret_loc decls - - let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t = fun {proc_desc; tenv; summary} -> Preanal.do_preanalysis proc_desc tenv ; let pdata = ProcData.make_default proc_desc tenv in let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata in let cfg = CFG.from_pdesc proc_desc in - let locals = get_local_decls cfg in - let forget_locals mem = Option.map ~f:(Dom.Mem.forget_locs locals) mem in - let entry_mem = extract_post (CFG.start_node cfg |> CFG.Node.id) inv_map |> forget_locals in - let exit_mem = extract_post (CFG.exit_node cfg |> CFG.Node.id) inv_map |> forget_locals in + let entry_mem = extract_post (CFG.start_node cfg |> CFG.Node.id) inv_map in + let exit_mem = extract_post (CFG.exit_node cfg |> CFG.Node.id) inv_map in let cond_set = Report.check_proc summary proc_desc tenv cfg inv_map |> Report.report_errors summary proc_desc - |> Report.forget_locs locals in let summary = match (entry_mem, exit_mem) with diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 45fe13a93..defcf6ab0 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -13,54 +13,31 @@ open AbsLoc open! AbstractDomain.Types module F = Format module L = Logging -module Relation = BufferOverrunDomainRelation module PO = BufferOverrunProofObligations module Trace = BufferOverrunTrace module TraceSet = Trace.Set +(** unsound but ok for bug catching *) +let always_strong_update = true + module Val = struct type astate = - { itv: Itv.astate - ; sym: Relation.Sym.astate - ; powloc: PowLoc.astate - ; arrayblk: ArrayBlk.astate - ; offset_sym: Relation.Sym.astate - ; size_sym: Relation.Sym.astate - ; traces: TraceSet.t } + {itv: Itv.astate; powloc: PowLoc.astate; arrayblk: ArrayBlk.astate; traces: TraceSet.t} type t = astate - let bot : t = - { itv= Itv.bot - ; sym= Relation.Sym.bot - ; powloc= PowLoc.bot - ; arrayblk= ArrayBlk.bot - ; offset_sym= Relation.Sym.bot - ; size_sym= Relation.Sym.bot - ; traces= TraceSet.empty } - + let bot : t = {itv= Itv.bot; powloc= PowLoc.bot; arrayblk= ArrayBlk.bot; traces= TraceSet.empty} let pp fmt x = - let relation_sym_pp fmt sym = - if Option.is_some Config.bo_relational_domain then F.fprintf fmt ", %a" Relation.Sym.pp sym - in - let trace_pp fmt traces = - if Config.bo_debug <= 1 then F.fprintf fmt ", %a" TraceSet.pp traces - in - F.fprintf fmt "(%a%a, %a, %a%a%a%a)" Itv.pp x.itv relation_sym_pp x.sym PowLoc.pp x.powloc - ArrayBlk.pp x.arrayblk relation_sym_pp x.offset_sym relation_sym_pp x.size_sym trace_pp - x.traces + if Config.bo_debug <= 1 then + F.fprintf fmt "(%a, %a, %a)" Itv.pp x.itv PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk + else + F.fprintf fmt "(%a, %a, %a, %a)" Itv.pp x.itv PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk + TraceSet.pp x.traces let unknown : traces:TraceSet.t -> t = - fun ~traces -> - { itv= Itv.top - ; sym= Relation.Sym.top - ; powloc= PowLoc.unknown - ; arrayblk= ArrayBlk.unknown - ; offset_sym= Relation.Sym.top - ; size_sym= Relation.Sym.top - ; traces } + fun ~traces -> {itv= Itv.top; powloc= PowLoc.unknown; arrayblk= ArrayBlk.unknown; traces} let unknown_from : callee_pname:_ -> location:_ -> t = @@ -74,11 +51,8 @@ module Val = struct let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true else - Itv.( <= ) ~lhs:lhs.itv ~rhs:rhs.itv && Relation.Sym.( <= ) ~lhs:lhs.sym ~rhs:rhs.sym - && PowLoc.( <= ) ~lhs:lhs.powloc ~rhs:rhs.powloc + Itv.( <= ) ~lhs:lhs.itv ~rhs:rhs.itv && PowLoc.( <= ) ~lhs:lhs.powloc ~rhs:rhs.powloc && ArrayBlk.( <= ) ~lhs:lhs.arrayblk ~rhs:rhs.arrayblk - && Relation.Sym.( <= ) ~lhs:lhs.offset_sym ~rhs:rhs.offset_sym - && Relation.Sym.( <= ) ~lhs:lhs.size_sym ~rhs:rhs.size_sym let equal x y = phys_equal x y || (( <= ) ~lhs:x ~rhs:y && ( <= ) ~lhs:y ~rhs:x) @@ -87,11 +61,8 @@ module Val = struct if phys_equal prev next then prev else { itv= Itv.widen ~prev:prev.itv ~next:next.itv ~num_iters - ; sym= Relation.Sym.widen ~prev:prev.sym ~next:next.sym ~num_iters ; powloc= PowLoc.widen ~prev:prev.powloc ~next:next.powloc ~num_iters ; arrayblk= ArrayBlk.widen ~prev:prev.arrayblk ~next:next.arrayblk ~num_iters - ; offset_sym= Relation.Sym.widen ~prev:prev.offset_sym ~next:next.offset_sym ~num_iters - ; size_sym= Relation.Sym.widen ~prev:prev.size_sym ~next:next.size_sym ~num_iters ; traces= TraceSet.join prev.traces next.traces } @@ -100,20 +71,13 @@ module Val = struct if phys_equal x y then x else { itv= Itv.join x.itv y.itv - ; sym= Relation.Sym.join x.sym y.sym ; powloc= PowLoc.join x.powloc y.powloc ; arrayblk= ArrayBlk.join x.arrayblk y.arrayblk - ; offset_sym= Relation.Sym.join x.offset_sym y.offset_sym - ; size_sym= Relation.Sym.join x.size_sym y.size_sym ; traces= TraceSet.join x.traces y.traces } let get_itv : t -> Itv.t = fun x -> x.itv - let get_sym : t -> Relation.Sym.astate = fun x -> x.sym - - let get_sym_var : t -> Relation.Var.t option = fun x -> Relation.Sym.get_var x.sym - let get_pow_loc : t -> PowLoc.t = fun x -> x.powloc let get_array_blk : t -> ArrayBlk.astate = fun x -> x.arrayblk @@ -122,10 +86,6 @@ module Val = struct let get_all_locs : t -> PowLoc.t = fun x -> PowLoc.join x.powloc (get_array_locs x) - let get_offset_sym : t -> Relation.Sym.astate = fun x -> x.offset_sym - - let get_size_sym : t -> Relation.Sym.astate = fun x -> x.size_sym - let get_traces : t -> TraceSet.t = fun x -> x.traces let set_traces : TraceSet.t -> t -> t = fun traces x -> {x with traces} @@ -136,29 +96,20 @@ module Val = struct let of_pow_loc : PowLoc.t -> t = fun x -> {bot with powloc= x} - let of_array_blk : allocsite:Allocsite.t -> ArrayBlk.astate -> t = - fun ~allocsite a -> - { bot with - arrayblk= a - ; offset_sym= Relation.Sym.of_allocsite_offset allocsite - ; size_sym= Relation.Sym.of_allocsite_size allocsite } - + let of_array_blk : ArrayBlk.astate -> t = fun a -> {bot with arrayblk= a} let modify_itv : Itv.t -> t -> t = fun i x -> {x with itv= i} - let make_sym - : ?unsigned:bool -> Loc.t -> Typ.Procname.t -> Itv.SymbolPath.partial -> Itv.Counter.t -> t = - fun ?(unsigned= false) loc pname path new_sym_num -> - { bot with - itv= Itv.make_sym ~unsigned pname (Itv.SymbolPath.normal path) new_sym_num - ; sym= Relation.Sym.of_loc loc } + let make_sym : ?unsigned:bool -> Typ.Procname.t -> Itv.SymbolPath.partial -> Itv.Counter.t -> t = + fun ?(unsigned= false) pname path new_sym_num -> + {bot with itv= Itv.make_sym ~unsigned pname (Itv.SymbolPath.normal path) new_sym_num} - let unknown_bit : t -> t = fun x -> {x with itv= Itv.top; sym= Relation.Sym.top} + 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; sym= Relation.Sym.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 |> Itv.of_bool; sym= Relation.Sym.top} + let lnot : t -> t = fun x -> {x with itv= Itv.lnot x.itv |> Itv.of_bool} let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> t -> t -> t = fun f x y -> {bot with itv= f x.itv y.itv; traces= TraceSet.join x.traces y.traces} @@ -344,15 +295,6 @@ module Heap = struct fun ~f locs mem -> PowLoc.fold (fun loc -> find loc mem |> f |> add loc) locs mem - let add x v = - let sym = if Itv.is_empty (Val.get_itv v) then Relation.Sym.bot else Relation.Sym.of_loc x in - let offset_sym, size_sym = - if ArrayBlk.is_bot (Val.get_array_blk v) then (Relation.Sym.bot, Relation.Sym.bot) - else (Relation.Sym.of_loc_offset x, Relation.Sym.of_loc_size x) - in - add x {v with Val.sym; Val.offset_sym; Val.size_sym} - - let strong_update : PowLoc.t -> Val.t -> astate -> astate = fun locs v mem -> PowLoc.fold (fun x -> add x v) locs mem @@ -454,9 +396,10 @@ module AliasMap = struct let pp_sep fmt () = F.fprintf fmt ", @," in let pp1 fmt (k, v) = F.fprintf fmt "%a=%a" Ident.pp k AliasTarget.pp v in (* F.fprintf fmt "@[Logical Variables :@,"; *) - F.fprintf fmt "@[{ " ; + F.fprintf fmt "@[{ @," ; F.pp_print_list ~pp_sep pp1 fmt (M.bindings x) ; - F.fprintf fmt " }@]" + F.fprintf fmt " }@]" ; + F.fprintf fmt "@]" let load : Ident.t -> AliasTarget.t -> t -> t = fun id loc m -> M.add id loc m @@ -563,7 +506,7 @@ module Alias = struct let pp : F.formatter -> astate -> unit = fun fmt (aliasmap, aliasret) -> - F.fprintf fmt "AliasMap:@;%a@;AliasRet:@;%a" AliasMap.pp aliasmap AliasRet.pp aliasret + F.fprintf fmt "AliasMap:@;%a@;AliasRet:@;%a@;" AliasMap.pp aliasmap AliasRet.pp aliasret end module PrunePairs = struct @@ -650,21 +593,11 @@ end module MemReach = struct type astate = - { stack: Stack.astate - ; heap: Heap.astate - ; alias: Alias.astate - ; latest_prune: LatestPrune.astate - ; relation: Relation.astate } + {stack: Stack.astate; heap: Heap.astate; alias: Alias.astate; latest_prune: LatestPrune.astate} type t = astate - let init : t = - { stack= Stack.bot - ; heap= Heap.bot - ; alias= Alias.bot - ; latest_prune= LatestPrune.top - ; relation= Relation.empty } - + let init : t = {stack= Stack.bot; heap= Heap.bot; alias= Alias.bot; latest_prune= LatestPrune.top} let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true @@ -672,7 +605,6 @@ module MemReach = struct Stack.( <= ) ~lhs:lhs.stack ~rhs:rhs.stack && Heap.( <= ) ~lhs:lhs.heap ~rhs:rhs.heap && Alias.( <= ) ~lhs:lhs.alias ~rhs:rhs.alias && LatestPrune.( <= ) ~lhs:lhs.latest_prune ~rhs:rhs.latest_prune - && Relation.( <= ) ~lhs:lhs.relation ~rhs:rhs.relation let widen ~prev ~next ~num_iters = @@ -682,7 +614,7 @@ module MemReach = struct ; heap= Heap.widen ~prev:prev.heap ~next:next.heap ~num_iters ; alias= Alias.widen ~prev:prev.alias ~next:next.alias ~num_iters ; latest_prune= LatestPrune.widen ~prev:prev.latest_prune ~next:next.latest_prune ~num_iters - ; relation= Relation.widen ~prev:prev.relation ~next:next.relation ~num_iters } + } let join : t -> t -> t = @@ -690,15 +622,12 @@ module MemReach = struct { stack= Stack.join x.stack y.stack ; heap= Heap.join x.heap y.heap ; alias= Alias.join x.alias y.alias - ; latest_prune= LatestPrune.join x.latest_prune y.latest_prune - ; relation= Relation.join x.relation y.relation } + ; latest_prune= LatestPrune.join x.latest_prune y.latest_prune } let pp : F.formatter -> t -> unit = fun fmt x -> - F.fprintf fmt "Stack:@;%a@;Heap:@;%a@;%a" Stack.pp x.stack Heap.pp x.heap Alias.pp x.alias ; - if Option.is_some Config.bo_relational_domain then - F.fprintf fmt "@;Relation:@;%a" Relation.pp x.relation + F.fprintf fmt "Stack:@;%a@;Heap:@;%a@;%a" Stack.pp x.stack Heap.pp x.heap Alias.pp x.alias let pp_summary : F.formatter -> t -> unit = @@ -760,6 +689,13 @@ module MemReach = struct let get_return : t -> Val.t = fun m -> Heap.get_return m.heap + let can_strong_update : PowLoc.t -> bool = + fun ploc -> + if always_strong_update then true + else 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 @@ -832,41 +768,6 @@ module MemReach = struct let heap_range : filter_loc:(Loc.t -> bool) -> t -> Itv.NonNegativePolynomial.astate = fun ~filter_loc {heap} -> Heap.range ~filter_loc heap - - - let get_relation : t -> Relation.astate = fun m -> m.relation - - let is_relation_unsat : t -> bool = fun m -> Relation.is_unsat m.relation - - let lift_relation : (Relation.astate -> Relation.astate) -> t -> t = - fun f m -> {m with relation= f m.relation} - - - let meet_constraints : Relation.Constraints.t -> t -> t = - fun constrs -> lift_relation (Relation.meet_constraints constrs) - - - let store_relation - : PowLoc.t -> Relation.SymExp.t option * Relation.SymExp.t option * Relation.SymExp.t option - -> t -> t = - fun locs symexp_opts -> lift_relation (Relation.store_relation locs symexp_opts) - - - let forget_locs : PowLoc.t -> t -> t = fun locs -> lift_relation (Relation.forget_locs locs) - - let init_param_relation : Loc.t -> t -> t = fun loc -> lift_relation (Relation.init_param loc) - - let init_array_relation - : Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:Relation.SymExp.t option -> t - -> t = - fun allocsite ~offset ~size ~size_exp_opt -> - lift_relation (Relation.init_array allocsite ~offset ~size ~size_exp_opt) - - - let instantiate_relation : Relation.SubstMap.t -> caller:t -> callee:t -> t = - fun subst_map ~caller ~callee -> - { caller with - relation= Relation.instantiate subst_map ~caller:caller.relation ~callee:callee.relation } end module Mem = struct @@ -993,42 +894,6 @@ module Mem = struct let update_latest_prune : Exp.t -> Exp.t -> t -> t = fun e1 e2 -> f_lift (MemReach.update_latest_prune e1 e2) - - - let get_relation : t -> Relation.astate = - fun m -> f_lift_default ~default:Relation.bot MemReach.get_relation m - - - let meet_constraints : Relation.Constraints.t -> t -> t = - fun constrs -> f_lift (MemReach.meet_constraints constrs) - - - let is_relation_unsat m = f_lift_default ~default:true MemReach.is_relation_unsat m - - let store_relation - : PowLoc.t -> Relation.SymExp.t option * Relation.SymExp.t option * Relation.SymExp.t option - -> t -> t = - fun locs symexp_opts -> f_lift (MemReach.store_relation locs symexp_opts) - - - let forget_locs : PowLoc.t -> t -> t = fun locs -> f_lift (MemReach.forget_locs locs) - - let init_param_relation : Loc.t -> t -> t = fun loc -> f_lift (MemReach.init_param_relation loc) - - let init_array_relation - : Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:Relation.SymExp.t option -> t - -> t = - fun allocsite ~offset ~size ~size_exp_opt -> - f_lift (MemReach.init_array_relation allocsite ~offset ~size ~size_exp_opt) - - - let instantiate_relation : Relation.SubstMap.t -> caller:t -> callee:t -> t = - fun subst_map ~caller ~callee -> - match callee with - | Bottom -> - caller - | NonBottom callee -> - f_lift (fun caller -> MemReach.instantiate_relation subst_map ~caller ~callee) caller end module Summary = struct @@ -1056,5 +921,5 @@ module Summary = struct 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 PO.ConditionSet.pp condition_set + F.fprintf fmt "%a@,%a@,%a@," Mem.pp entry_mem Mem.pp exit_mem PO.ConditionSet.pp condition_set end diff --git a/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml b/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml deleted file mode 100644 index fd7cdf0dd..000000000 --- a/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml +++ /dev/null @@ -1,1623 +0,0 @@ -(* - * Copyright (c) 2018-present, Facebook, Inc. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd -open Core -open AbsLoc -open! AbstractDomain.Types -module F = Format -open Apron - -module type S = sig - module Var : sig - type t - end - - module Sym : sig - include AbstractDomain.S - - val bot : astate - - val top : astate - - val of_loc : Loc.t -> astate - - val of_loc_offset : Loc.t -> astate - - val of_loc_size : Loc.t -> astate - - val of_allocsite_offset : Allocsite.t -> astate - - val of_allocsite_size : Allocsite.t -> astate - - val get_var : astate -> Var.t option - end - - module SymExp : sig - type t [@@deriving compare] - - val pp_opt : F.formatter -> t option -> unit - - val zero : t - - val of_sym : Sym.astate -> t option - - val of_exp : get_sym_f:(Exp.t -> Sym.astate) -> Exp.t -> t option - - val of_exps : - get_int_sym_f:(Exp.t -> Sym.astate) -> get_offset_sym_f:(Exp.t -> Sym.astate) - -> get_size_sym_f:(Exp.t -> Sym.astate) -> Exp.t -> t option * t option * t option - - val of_exp_opt : get_sym_f:(Exp.t -> Sym.astate) -> Exp.t option -> t option - - val plus : t -> t -> t - - val minus : t -> t -> t - end - - module Constraints : sig - type t - - val of_exp : get_sym_f:(Exp.t -> Sym.astate) -> Exp.t -> t - end - - module SubstMap : sig - type t - - val empty : t - - val add : Var.t -> SymExp.t option -> t -> t - - val symexp_subst_opt : t -> SymExp.t option -> SymExp.t option - end - - include AbstractDomain.S - - val set_deserialize : unit -> unit - - val compare_astate : astate -> astate -> int - - val empty : astate - - val bot : astate - - val is_unsat : astate -> bool - - val lt_sat_opt : SymExp.t option -> SymExp.t option -> astate -> bool - - val le_sat_opt : SymExp.t option -> SymExp.t option -> astate -> bool - - val meet_constraints : Constraints.t -> astate -> astate - - val store_relation : - PowLoc.t -> SymExp.t option * SymExp.t option * SymExp.t option -> astate -> astate - - val init_param : Loc.t -> astate -> astate - - val init_array : - Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:SymExp.t option -> astate -> astate - - val forget_locs : PowLoc.t -> astate -> astate - - val instantiate : caller:astate -> callee:astate -> SubstMap.t -> astate -end - -module NoRelation = struct - module UnitDom = struct - type astate = unit [@@deriving compare] - - type t = astate [@@deriving compare] - - let compare_astate _ _ = 0 - - let f1 _ = () - - let f2 _ _ = () - - let f3 _ _ _ = () - - let f1_none _ = None - - let f2_none _ _ = None - - let f1_false _ = false - - let f3_false _ _ _ = false - - let ( <= ) ~lhs:() ~rhs:() = true - - let join = f2 - - let widen ~prev:() ~next:() ~num_iters:_ = () - - let pp = f2 - - let bot = () - - let top = () - end - - module Var = UnitDom - - module Sym = struct - include UnitDom - - let of_loc = f1 - - let of_loc_offset = f1 - - let of_loc_size = f1 - - let of_allocsite_offset = f1 - - let of_allocsite_size = f1 - - let get_var = f1_none - end - - module SymExp = struct - include UnitDom - - let pp_opt = f2 - - let zero = () - - let of_exp ~get_sym_f:_ = f1_none - - let of_exps ~get_int_sym_f:_ ~get_offset_sym_f:_ ~get_size_sym_f:_ _x = (None, None, None) - - let of_exp_opt ~get_sym_f:_ = f1_none - - let of_sym = f1_none - - let plus = f2 - - let minus = f2 - end - - module Constraints = struct - include UnitDom - - let of_exp ~get_sym_f:_ = f1 - end - - module SubstMap = struct - include UnitDom - - let empty = () - - let add = f3 - - let symexp_subst_opt = f2_none - end - - include UnitDom - - let set_deserialize = f1 - - let empty = () - - let is_unsat = f1_false - - let lt_sat_opt = f3_false - - let le_sat_opt = f3_false - - let meet_constraints = f2 - - let store_relation = f3 - - let init_param = f2 - - let init_array _allocsite ~offset:_ ~size:_ ~size_exp_opt:_ = f1 - - let forget_locs = f2 - - let instantiate ~caller:_ ~callee:_ = f1 -end - -module type Manager_S = sig - type domain_t - - val alloc_man : unit -> domain_t Manager.t -end - -module Make (Manager : Manager_S) = struct - let man = Manager.alloc_man () - - let set_deserialize () = Apron.Manager.set_deserialize man - - module Compares = struct - let lift int_of x y = int_of x - int_of y - - let int_of_unop = function Texpr0.Neg -> 0 | Texpr0.Cast -> 1 | Texpr0.Sqrt -> 2 - - let int_of_binop = function - | Texpr0.Add -> - 0 - | Texpr0.Sub -> - 1 - | Texpr0.Mul -> - 2 - | Texpr0.Div -> - 3 - | Texpr0.Mod -> - 4 - | Texpr0.Pow -> - 5 - - - let int_of_typ = function - | Texpr0.Real -> - 0 - | Texpr0.Int -> - 1 - | Texpr0.Single -> - 2 - | Texpr0.Double -> - 3 - | Texpr0.Extended -> - 4 - | Texpr0.Quad -> - 5 - - - let int_of_round = function - | Texpr0.Near -> - 0 - | Texpr0.Zero -> - 1 - | Texpr0.Up -> - 2 - | Texpr0.Down -> - 3 - | Texpr0.Rnd -> - 4 - - - let compare_unop = lift int_of_unop - - let compare_binop = lift int_of_binop - - let compare_typ = lift int_of_typ - - let compare_round = lift int_of_round - - let ( ) n (cmp, x, y) = if n <> 0 then n else cmp x y - - let rec compare_texpr0_expr x y = - let int_of_texpr0_expr = function - | Texpr0.Cst _ -> - 0 - | Texpr0.Dim _ -> - 1 - | Texpr0.Unop _ -> - 2 - | Texpr0.Binop _ -> - 3 - in - match (x, y) with - | Texpr0.Cst c1, Texpr0.Cst c2 -> - Coeff.cmp c1 c2 - | Texpr0.Dim i1, Texpr0.Dim i2 -> - i1 - i2 - | Texpr0.Unop (uop1, e1, t1, r1), Texpr0.Unop (uop2, e2, t2, r2) -> - compare_unop uop1 uop2 (compare_texpr0_expr, e1, e2) (compare_typ, t1, t2) - (compare_round, r1, r2) - | Texpr0.Binop (bop1, le1, re1, t1, r1), Texpr0.Binop (bop2, le2, re2, t2, r2) -> - compare_binop bop1 bop2 (compare_texpr0_expr, le1, le2) - (compare_texpr0_expr, re1, re2) (compare_typ, t1, t2) (compare_round, r1, r2) - | _, _ -> - int_of_texpr0_expr x - int_of_texpr0_expr y - - - let compare_texpr0 x y = compare_texpr0_expr (Texpr0.to_expr x) (Texpr0.to_expr y) - - let compare_texpr1 x y = - compare_texpr0 (Texpr1.get_texpr0 x) (Texpr1.get_texpr0 y) - (Environment.compare, Texpr1.get_env x, Texpr1.get_env y) - - - let compare_abstract1 x y = Abstract1.hash man x - Abstract1.hash man y - end - - module TexprToLinexpr = struct - let scalar_op (float_op, mpqf_op, mpfrf_op) s1 s2 = - match (s1, s2) with - | Scalar.Float f1, Scalar.Float f2 -> - Scalar.Float (float_op f1 f2) - | Scalar.Float f1, Scalar.Mpqf m2 | Scalar.Mpqf m2, Scalar.Float f1 -> - Scalar.Mpqf (mpqf_op (Mpqf.of_float f1) m2) - | Scalar.Float f1, Scalar.Mpfrf m2 | Scalar.Mpfrf m2, Scalar.Float f1 -> - Scalar.Mpfrf (mpfrf_op (Mpfrf.of_float f1 Mpfr.Near) m2 Mpfr.Near) - | Scalar.Mpqf m1, Scalar.Mpqf m2 -> - Scalar.Mpqf (mpqf_op m1 m2) - | Scalar.Mpqf m1, Scalar.Mpfrf m2 | Scalar.Mpfrf m2, Scalar.Mpqf m1 -> - Scalar.Mpfrf (mpfrf_op (Mpfrf.of_mpq m1 Mpfr.Near) m2 Mpfr.Near) - | Scalar.Mpfrf m1, Scalar.Mpfrf m2 -> - Scalar.Mpfrf (mpfrf_op m1 m2 Mpfr.Near) - - - let scalar_add = scalar_op (( +. ), Mpqf.add, Mpfrf.add) - - let scalar_mult = scalar_op (( *. ), Mpqf.mul, Mpfrf.mul) - - let coeff_plus c1 c2 = - match (c1, c2) with - | Coeff.Scalar s1, Coeff.Scalar s2 -> - Coeff.Scalar (scalar_add s1 s2) - | _, _ -> - assert false - - - let coeff_minus c1 c2 = coeff_plus c1 (Coeff.neg c2) - - let coeff_mult c1 c2 = - match (c1, c2) with - | Coeff.Scalar s1, Coeff.Scalar s2 -> - Coeff.Scalar (scalar_mult s1 s2) - | _, _ -> - assert false - - - let rec is_constant = function - | Texpr1.Cst c -> - Some c - | Texpr1.Unop (Texpr1.Neg, re1, _, _) -> - Option.map (is_constant re1) ~f:Coeff.neg - | Texpr1.Binop (Texpr1.Add, re1, re2, _, _) -> - Option.map2 (is_constant re1) (is_constant re2) ~f:coeff_plus - | Texpr1.Binop (Texpr1.Sub, re1, re2, _, _) -> - Option.map2 (is_constant re1) (is_constant re2) ~f:coeff_minus - | Texpr1.Binop (Texpr1.Mul, re1, re2, _, _) -> - Option.map2 (is_constant re1) (is_constant re2) ~f:coeff_mult - | _ -> - None - - - let rec add_coeffs ~coeff re x = - match re with - | Texpr1.Cst c -> - let c' = Linexpr1.get_cst x in - Linexpr1.set_cst x (coeff_plus c' (coeff_mult c coeff)) ; - Some x - | Texpr1.Var var -> - let c' = Linexpr1.get_coeff x var in - Linexpr1.set_coeff x var (coeff_plus c' coeff) ; - Some x - | Texpr1.Unop (Texpr1.Neg, re1, _, _) -> - add_coeffs ~coeff:(Coeff.neg coeff) re1 x - | Texpr1.Binop (Texpr1.Add, re1, re2, _, _) -> - Option.bind (add_coeffs ~coeff re1 x) ~f:(add_coeffs ~coeff re2) - | Texpr1.Binop (Texpr1.Sub, re1, re2, _, _) -> - Option.bind (add_coeffs ~coeff re1 x) ~f:(add_coeffs ~coeff:(Coeff.neg coeff) re2) - | Texpr1.Binop (Texpr1.Mul, re1, re2, _, _) -> ( - match is_constant re1 with - | None -> - Option.value_map (is_constant re2) ~default:None ~f:(fun c -> - add_coeffs ~coeff:(coeff_mult coeff c) re1 x ) - | Some c -> - add_coeffs ~coeff:(coeff_mult coeff c) re2 x ) - | _ -> - assert false - - - let trans x = - let lin = Linexpr1.make (Texpr1.get_env x) in - add_coeffs ~coeff:(Coeff.s_of_int 1) (Texpr1.to_expr x) lin - end - - module Var = struct - include Apron.Var - - let pp = print - - let dummy = of_string "dummy" - - let return = of_string "return" - - let param_prefix = "__inferbo_param_" - - let temp_param_prefix = "__inferbo_temp_param_" - - let loc_offset_prefix = "__inferbo_loc_offset_" - - let loc_size_prefix = "__inferbo_loc_size_" - - let allocsite_offset_prefix = "__inferbo_allocsite_offset_" - - let allocsite_size_prefix = "__inferbo_allocsite_size_" - - let of_loc loc = of_string (Loc.to_string loc) - - let of_loc_offset loc = of_string (loc_offset_prefix ^ Loc.to_string loc) - - let of_loc_size loc = of_string (loc_size_prefix ^ Loc.to_string loc) - - let of_allocsite_offset allocsite = - of_string (allocsite_offset_prefix ^ Allocsite.to_string allocsite) - - - let of_allocsite_size allocsite = - of_string (allocsite_size_prefix ^ Allocsite.to_string allocsite) - - - let param_of var = of_string (param_prefix ^ to_string var) - - let temp_param_of var = of_string (temp_param_prefix ^ to_string var) - - let param_of_loc loc = of_string (param_prefix ^ Loc.to_string loc) - - let array_of_var var = Array.create ~len:1 var - - let array_of_powloc of_loc locs = - let len = PowLoc.cardinal locs in - let a = Array.create ~len dummy in - let i = ref 0 in - PowLoc.iter - (fun loc -> - a.(!i) <- of_loc loc ; - i := !i + 1 ) - locs ; - a - - - let int_array_of_powloc locs = array_of_powloc of_loc locs - - let offset_array_of_powloc locs = array_of_powloc of_loc_offset locs - - let size_array_of_powloc locs = array_of_powloc of_loc_size locs - end - - module VarSet = struct - include PrettyPrintable.MakePPSet (Var) - - let of_array var_array = Array.fold var_array ~init:empty ~f:(fun acc var -> add var acc) - - let to_array x = - let a = Array.create ~len:(cardinal x) Var.dummy in - let n = ref 0 in - iter - (fun var -> - a.(!n) <- var ; - n := !n + 1 ) - x ; - a - - - let of_powloc var_of_loc locs = - PowLoc.fold (fun loc acc -> add (var_of_loc loc) acc) locs empty - - - let int_of_powloc locs = of_powloc Var.of_loc locs - - let offset_of_powloc locs = of_powloc Var.of_loc_offset locs - - let size_of_powloc locs = of_powloc Var.of_loc_size locs - end - - module VarMap = struct - include PrettyPrintable.MakePPMap (Var) - - let iter x ~f = iter f x - - let fold x ~init ~f = fold f x init - - let fold2 x y ~init ~f = - let m = merge (fun _ v1 v2 -> Some (v1, v2)) x y in - fold m ~init ~f:(fun k (v1, v2) acc -> f k v1 v2 acc) - end - - module Sym = struct - type astate = Bot | V of Var.t | Top [@@deriving compare] - - let ( <= ) ~lhs ~rhs = - match (lhs, rhs) with - | Bot, _ -> - true - | _, Bot -> - false - | _, Top -> - true - | Top, _ -> - false - | V x, V y -> - Int.equal (Var.compare x y) 0 - - - let join x y = - match (x, y) with - | Bot, a | a, Bot -> - a - | _, Top | Top, _ -> - Top - | V x', V y' -> - if Int.equal (Var.compare x' y') 0 then x else Top - - - let widen ~prev ~next ~num_iters:_ = join prev next - - let pp fmt = function - | Bot -> - F.fprintf fmt "_|_" - | Top -> - F.fprintf fmt "T" - | V x -> - Var.pp fmt x - - - let bot = Bot - - let top = Top - - let lift f x = V (f x) - - let of_loc = lift Var.of_loc - - let of_loc_offset = lift Var.of_loc_offset - - let of_loc_size = lift Var.of_loc_size - - let of_allocsite_offset = lift Var.of_allocsite_offset - - let of_allocsite_size = lift Var.of_allocsite_size - - let get_var = function V x -> Some x | Bot | Top -> None - end - - module Env = struct - type t = Environment.t - - let empty : t = Environment.make [||] [||] - - let join env1 env2 = - let vars, _ = Environment.vars env2 in - let vars = Array.filter vars ~f:(fun var -> not (Environment.mem_var env1 var)) in - Environment.add env1 vars [||] - - - let of_vars_array vars = Environment.make vars [||] - - let of_vars_set vars = of_vars_array (VarSet.to_array vars) - - let to_vars_set x = - let vars, _ = Environment.vars x in - VarSet.of_array vars - end - - module SymExp = struct - (* raw tree expression without environments *) - type raw = Texpr1.expr - - (* efficient tree expression with environments *) - type t = Texpr1.t - - let string_of_binop = function - | Texpr1.Add -> - "+" - | Texpr1.Sub -> - "-" - | Texpr1.Mul -> - "*" - | Texpr1.Div -> - "/" - | Texpr1.Mod -> - "%" - | Texpr1.Pow -> - "^" - - - let rec pp_raw ~need_paren fmt = function - | Texpr1.Cst coeff -> - Coeff.print fmt coeff - | Texpr1.Var x -> - Var.print fmt x - | Texpr1.Unop (Texpr1.Neg, e, _, _) -> - F.fprintf fmt "-%a" (pp_raw ~need_paren:true) e - | Texpr1.Unop (Texpr1.Cast, e, typ, _) -> - F.fprintf fmt "(%a)%a" Texpr1.print_typ typ (pp_raw ~need_paren:true) e - | Texpr1.Unop (Texpr1.Sqrt, e, _, _) -> - F.fprintf fmt "sqrt(%a)" (pp_raw ~need_paren:false) e - | Texpr1.Binop (bop, e1, e2, _, _) -> - (if need_paren then F.fprintf fmt "(%a%s%a)" else F.fprintf fmt "%a%s%a") - (pp_raw ~need_paren:true) e1 (string_of_binop bop) (pp_raw ~need_paren:true) e2 - - - let pp fmt x = pp_raw ~need_paren:false fmt (Texpr1.to_expr x) - - let pp_opt fmt = function None -> F.fprintf fmt "None" | Some x -> pp fmt x - - let compare = Compares.compare_texpr1 - - (* NOTE: We consider only integer values as of now. *) - let default_round = Texpr1.Near - - let raw_uop_make typ re = Texpr1.Unop (typ, re, Texpr1.Int, default_round) - - let raw_bop_make typ re1 re2 = Texpr1.Binop (typ, re1, re2, Texpr1.Int, default_round) - - let vars_array_of_raw re = - let rec vars_set_of = function - | Texpr1.Cst _ -> - VarSet.empty - | Texpr1.Var x -> - VarSet.singleton x - | Texpr1.Unop (_, re, _, _) -> - vars_set_of re - | Texpr1.Binop (_, re1, re2, _, _) -> - VarSet.union (vars_set_of re1) (vars_set_of re2) - in - VarSet.to_array (vars_set_of re) - - - let vars_set_of x = Env.to_vars_set (Texpr1.get_env x) - - let vars_set_of_opt x_opt = Option.value_map x_opt ~default:VarSet.empty ~f:vars_set_of - - let env_of_raw re = Env.of_vars_array (vars_array_of_raw re) - - let raw_of_exp ~get_sym_f e : raw option = - let try_get_sym_f e = match get_sym_f e with Sym.V x -> Some (Texpr1.Var x) | _ -> None in - let rec raw_of_exp' e = - match e with - | Exp.UnOp (Unop.Neg, e', _) -> ( - match raw_of_exp' e' with - | Some re -> - Some (raw_uop_make Texpr1.Neg re) - | None -> - try_get_sym_f e ) - | Exp.BinOp (bop, e1, e2) -> ( - match (raw_of_exp' e1, raw_of_exp' e2) with - | Some re1, Some re2 -> ( - match bop with - | Binop.PlusA -> - Some (raw_bop_make Texpr1.Add re1 re2) - | Binop.MinusA -> - Some (raw_bop_make Texpr1.Sub re1 re2) - | Binop.Mult -> - Some (raw_bop_make Texpr1.Mul re1 re2) - | _ -> - try_get_sym_f e ) - | _, _ -> - try_get_sym_f e ) - | Exp.Const (Const.Cint i) -> ( - try Some (Texpr1.Cst (Coeff.s_of_int (IntLit.to_int i))) with _ -> None ) - | _ -> - try_get_sym_f e - in - raw_of_exp' e - - - let raw_offset_of_exp ~get_int_sym_f ~get_offset_sym_f e = - let try_get_offset_sym_f e = - match get_offset_sym_f e with Sym.V x -> Some (Texpr1.Var x) | _ -> None - in - let rec raw_offset_of_exp' e = - match e with - | Exp.BinOp (bop, e1, e2) -> ( - match (raw_offset_of_exp' e1, raw_of_exp ~get_sym_f:get_int_sym_f e2) with - | Some re1, Some re2 -> ( - match bop with - | Binop.PlusPI -> - Some (raw_bop_make Texpr1.Add re1 re2) - | Binop.MinusPI -> - Some (raw_bop_make Texpr1.Sub re1 re2) - | _ -> - try_get_offset_sym_f e ) - | _, _ -> - try_get_offset_sym_f e ) - | _ -> - try_get_offset_sym_f e - in - raw_offset_of_exp' e - - - let raw_size_of_exp ~get_size_sym_f e = - let try_get_size_sym_f e = - match get_size_sym_f e with Sym.V x -> Some (Texpr1.Var x) | _ -> None - in - let rec raw_size_of_exp' e = - match e with - | Exp.BinOp (bop, e1, _e2) -> ( - match raw_size_of_exp' e1 with - | Some re1 -> ( - match bop with Binop.PlusPI | Binop.MinusPI -> Some re1 | _ -> try_get_size_sym_f e ) - | _ -> - try_get_size_sym_f e ) - | _ -> - try_get_size_sym_f e - in - raw_size_of_exp' e - - - let of_raw re = Texpr1.of_expr (env_of_raw re) re - - let of_exp ~get_sym_f e = Option.map (raw_of_exp ~get_sym_f e) ~f:of_raw - - let offset_of_exp ~get_int_sym_f ~get_offset_sym_f e : t option = - Option.map (raw_offset_of_exp ~get_int_sym_f ~get_offset_sym_f e) ~f:of_raw - - - let size_of_exp ~get_size_sym_f e : t option = - Option.map (raw_size_of_exp ~get_size_sym_f e) ~f:of_raw - - - let of_exps ~get_int_sym_f ~get_offset_sym_f ~get_size_sym_f e : t option * t option * t option = - let int_sym = of_exp ~get_sym_f:get_int_sym_f e in - let offset_sym = offset_of_exp ~get_int_sym_f ~get_offset_sym_f e in - let size_sym = size_of_exp ~get_size_sym_f e in - (int_sym, offset_sym, size_sym) - - - let of_exp_opt ~get_sym_f opt_e : t option = Option.find_map opt_e ~f:(of_exp ~get_sym_f) - - let of_int i = Texpr1.cst Env.empty (Coeff.s_of_int i) - - let zero = of_int 0 - - let one = of_int 1 - - let of_sym s = match s with Sym.V x -> Some (of_raw (Texpr1.Var x)) | _ -> None - - let of_var var = of_raw (Texpr1.Var var) - - let dummy = of_var Var.dummy - - let linexpr_dummy = Linexpr1.make Env.empty - - let to_var x = match Texpr1.to_expr x with Texpr1.Var x' -> Some x' | _ -> None - - let is_var x = match to_var x with Some _ -> true | None -> false - - let bop_make typ x y = - let env = Env.join (Texpr1.get_env x) (Texpr1.get_env y) in - let re = raw_bop_make typ (Texpr1.to_expr x) (Texpr1.to_expr y) in - Texpr1.of_expr env re - - - let plus = bop_make Texpr1.Add - - let minus = bop_make Texpr1.Sub - - let to_linexpr = TexprToLinexpr.trans - end - - module SubstMap = struct - type t = SymExp.t option VarMap.t - - let add = VarMap.add - - let empty = VarMap.empty - - let fold = VarMap.fold - - let mem = VarMap.mem - - let singleton = VarMap.singleton - - let map_opt ~f x = VarMap.map (Option.value_map ~default:None ~f) x - - let to_arrays dummy x = - let x = - VarMap.fold x ~init:VarMap.empty ~f:(fun k v_opt acc -> - Option.value_map v_opt ~default:acc ~f:(fun v -> VarMap.add k v acc) ) - in - let keys = Array.create ~len:(VarMap.cardinal x) Var.dummy in - let values = Array.create ~len:(VarMap.cardinal x) dummy in - let n = ref 0 in - VarMap.iter x ~f:(fun key value -> - keys.(!n) <- key ; - values.(!n) <- value ; - n := !n + 1 ) ; - (keys, values) - - - let to_arrays_symexp = to_arrays SymExp.dummy - - let to_arrays_linexpr = to_arrays SymExp.linexpr_dummy - - let rec symexp_raw_subst subst_map x = - match x with - | Texpr1.Cst _ -> - Some x - | Texpr1.Var var -> - if mem var subst_map then Option.map (VarMap.find var subst_map) ~f:Texpr1.to_expr - else None - | Texpr1.Unop (uop, re, typ, round) -> - Option.map (symexp_raw_subst subst_map re) ~f:(fun re' -> - Texpr1.Unop (uop, re', typ, round) ) - | Texpr1.Binop (bop, re1, re2, typ, round) -> - Option.map2 (symexp_raw_subst subst_map re1) (symexp_raw_subst subst_map re2) ~f: - (fun re1' re2' -> Texpr1.Binop (bop, re1', re2', typ, round) ) - - - let symexp_subst subst_map x = - let re_opt = symexp_raw_subst subst_map (Texpr1.to_expr x) in - Option.map re_opt ~f:SymExp.of_raw - - - let symexp_subst_opt subst_map x_opt = - Option.value_map x_opt ~default:None ~f:(symexp_subst subst_map) - end - - module Constraints = struct - type t = Tcons1.earray - - let empty = Tcons1.array_make Env.empty 0 - - let singleton e = - let tcons_array = Tcons1.array_make (Tcons1.get_env e) 1 in - Tcons1.array_set tcons_array 0 e ; tcons_array - - - let doubleton e1 e2 = - let env = Env.join (Tcons1.get_env e1) (Tcons1.get_env e2) in - let tcons_array = Tcons1.array_make env 2 in - Tcons1.array_set tcons_array 0 e1 ; Tcons1.array_set tcons_array 1 e2 ; tcons_array - - - let and_ x y = - let env = Env.join (Tcons1.array_get_env x) (Tcons1.array_get_env y) in - let x, y = (Tcons1.array_extend_environment x env, Tcons1.array_extend_environment y env) in - let len1, len2 = (Tcons1.array_length x, Tcons1.array_length y) in - let tcons_array = Tcons1.array_make env (len1 + len2) in - for i = 0 to len1 - 1 do Tcons1.array_set tcons_array i (Tcons1.array_get x i) done ; - for i = 0 to len2 - 1 do Tcons1.array_set tcons_array (len1 + i) (Tcons1.array_get y i) done ; - tcons_array - - - let eq_of var1 var2 = - let sym_exp1, sym_exp2 = (SymExp.of_var var1, SymExp.of_var var2) in - let sym_exp = SymExp.minus sym_exp1 sym_exp2 in - singleton (Tcons1.make sym_exp Tcons1.EQ) - - - let eq_of_sym sym1 sym_exp2 = - Option.map (SymExp.of_sym sym1) ~f:(fun sym_exp1 -> - let sym_exp = SymExp.minus sym_exp1 sym_exp2 in - singleton (Tcons1.make sym_exp Tcons1.EQ) ) - - - let itv_of sym itv = - if Itv.is_empty itv then empty - else - let lb, ub = (Itv.lb itv, Itv.ub itv) in - Option.value_map (SymExp.of_sym sym) ~default:empty ~f:(fun sym_exp -> - let tcons_lb = - Option.map (Itv.Bound.is_const lb) ~f:(fun lb -> - let sym_minus_lb = SymExp.minus sym_exp (SymExp.of_int lb) in - Tcons1.make sym_minus_lb Tcons1.SUPEQ ) - in - let tcons_ub = - Option.map (Itv.Bound.is_const ub) ~f:(fun ub -> - let ub_minus_sym = SymExp.minus (SymExp.of_int ub) sym_exp in - Tcons1.make ub_minus_sym Tcons1.SUPEQ ) - in - match (tcons_lb, tcons_ub) with - | Some tcons_lb, Some tcons_ub -> - doubleton tcons_lb tcons_ub - | Some tcons, None | None, Some tcons -> - singleton tcons - | None, None -> - empty ) - - - let of_raw_symexp re typ = singleton (Tcons1.make (SymExp.of_raw re) typ) - - let of_exp ~get_sym_f e : t = - let of_bin_compare bop e1 e2 = - match (SymExp.raw_of_exp ~get_sym_f e1, SymExp.raw_of_exp ~get_sym_f e2) with - | Some re1, Some re2 -> - of_raw_symexp (SymExp.raw_bop_make Texpr1.Sub re1 re2) bop - | _, _ -> - empty - in - match e with - | Exp.Var _ | Exp.Lvar _ | Exp.Cast _ | Exp.Lfield _ | Exp.Lindex _ -> ( - match get_sym_f e with Sym.V x -> of_raw_symexp (Texpr1.Var x) Tcons1.DISEQ | _ -> empty ) - | Exp.BinOp (Binop.Eq, e1, e2) | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ne, e1, e2), _) -> - of_bin_compare Tcons1.EQ e1 e2 - | Exp.BinOp (Binop.Ne, e1, e2) | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq, e1, e2), _) -> - of_bin_compare Tcons1.DISEQ e1 e2 - | Exp.BinOp (Binop.Gt, e1, e2) - | Exp.BinOp (Binop.Lt, e2, e1) - | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Le, e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ge, e2, e1), _) -> - of_bin_compare Tcons1.SUP e1 e2 - | Exp.BinOp (Binop.Ge, e1, e2) - | Exp.BinOp (Binop.Le, e2, e1) - | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Lt, e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Gt, e2, e1), _) -> - of_bin_compare Tcons1.SUPEQ e1 e2 - | _ -> - empty - - - let vars_set_of x = - let vars = ref VarSet.empty in - for i = 0 to Tcons1.array_length x - 1 do - vars := VarSet.union !vars (SymExp.vars_set_of (Tcons1.get_texpr1 (Tcons1.array_get x i))) - done ; - !vars - - - let remove_strict_ineq_tcons1 x = - match Tcons1.get_typ x with - | Tcons1.SUP -> - let e_minus_one = SymExp.minus (Tcons1.get_texpr1 x) SymExp.one in - Tcons1.make e_minus_one Tcons1.SUPEQ - | _ -> - x - - - let remove_strict_ineq x = - let length = Tcons1.array_length x in - let x' = Tcons1.array_make (Tcons1.array_get_env x) length in - for i = 0 to length - 1 do - let tcons1 = Tcons1.array_get x i in - Tcons1.array_set x' i (remove_strict_ineq_tcons1 tcons1) - done ; - x' - end - - module Val = struct - type astate = Manager.domain_t Abstract1.t - - let compare_astate = Compares.compare_abstract1 - - let bot = Abstract1.bottom man Env.empty - - let top = Abstract1.top man Env.empty - - let is_bot x = Abstract1.is_bottom man x - - let is_top x = Abstract1.is_top man x - - let sync_env x y = - let x, y = (Abstract1.minimize_environment man x, Abstract1.minimize_environment man y) in - let env = Env.join (Abstract1.env x) (Abstract1.env y) in - let x = Abstract1.change_environment man x env false in - let y = Abstract1.change_environment man y env false in - (x, y) - - - let extend_env env x = - let x = Abstract1.minimize_environment man x in - let new_env = Env.join (Abstract1.env x) env in - Abstract1.change_environment man x new_env false - - - let sync_env_lift f x y = - let x, y = sync_env x y in - f x y - - - let join = sync_env_lift (Abstract1.join man) - - let meet = sync_env_lift (Abstract1.meet man) - - let widen ~prev ~next ~num_iters:_ = sync_env_lift (Abstract1.widening man) prev next - - let pp fmt x = Abstract1.print fmt x - - let ( <= ) ~lhs ~rhs = sync_env_lift (Abstract1.is_leq man) lhs rhs - - let sat_tcons tcons x = - let tcons = Constraints.remove_strict_ineq_tcons1 tcons in - let x = extend_env (Tcons1.get_env tcons) x in - Abstract1.sat_tcons man x tcons - - - let is_unsat_constraint constr x = - let symexp = Tcons1.get_texpr1 constr in - let typ = Tcons1.get_typ constr in - let neg_constr_opt = - match typ with - | Tcons1.EQ -> - Some (Tcons1.make symexp Tcons1.DISEQ) - | Tcons1.DISEQ -> - Some (Tcons1.make symexp Tcons1.EQ) - | Tcons1.SUPEQ | Tcons1.SUP - -> ( - let env = Tcons1.get_env constr in - let neg_symexp = - Texpr1.of_expr env (SymExp.raw_uop_make Texpr1.Neg (Texpr1.to_expr symexp)) - in - match typ with - | Tcons1.SUPEQ -> - Some (Tcons1.make neg_symexp Tcons1.SUP) - | Tcons1.SUP -> - Some (Tcons1.make neg_symexp Tcons1.SUPEQ) - | _ -> - assert false ) - | _ -> - None - in - Option.value_map neg_constr_opt ~default:false ~f:(fun neg_constr -> sat_tcons neg_constr x) - - - let is_unsat_constraints constrs x = - let sat = ref true in - for i = 0 to Tcons1.array_length constrs - 1 do - let constr = Tcons1.array_get constrs i in - if is_unsat_constraint constr x then sat := false - done ; - not !sat - - - let meet_constraints constrs x = - let constrs = Constraints.remove_strict_ineq constrs in - let x = extend_env (Tcons1.array_get_env constrs) x in - if is_unsat_constraints constrs x then bot else Abstract1.meet_tcons_array man x constrs - - - let forget_vars_array vars x = - let x = extend_env (Env.of_vars_array vars) x in - Abstract1.forget_array man x vars false - - - let forget_vars_set vars x = forget_vars_array (VarSet.to_array vars) x - - let assign_vars vars texpr x = - let x = extend_env (Env.join (Texpr1.get_env texpr) (Env.of_vars_array vars)) x in - let texprs = Array.create ~len:(Array.length vars) texpr in - Abstract1.assign_texpr_array man x vars texprs None - - - let store_relation var_array_of_powloc locs texpr_opt x = - let vars = var_array_of_powloc locs in - if can_strong_update locs then - match texpr_opt with - | Some texpr -> - assign_vars vars texpr x - | None -> - forget_vars_array vars x - else forget_vars_array vars x - - - let store_relation_int locs texpr_opt x = - store_relation Var.int_array_of_powloc locs texpr_opt x - - - let store_relation_offset locs texpr_opt x = - store_relation Var.offset_array_of_powloc locs texpr_opt x - - - let store_relation_size locs texpr_opt x = - store_relation Var.size_array_of_powloc locs texpr_opt x - - - let forget_var var x = forget_vars_array (Var.array_of_var var) x - - let lt_sat e1 e2 x = sat_tcons (Tcons1.make (SymExp.minus e2 e1) Tcons1.SUP) x - - let le_sat e1 e2 x = sat_tcons (Tcons1.make (SymExp.minus e2 e1) Tcons1.SUPEQ) x - - let subst : forget_free:bool -> SubstMap.t -> astate -> astate = - let forget_free_vars vars_in_subst_map x = - let free_vars = VarSet.diff (Env.to_vars_set (Abstract1.env x)) vars_in_subst_map in - let free_vars = VarSet.remove Var.return free_vars in - forget_vars_set free_vars x - in - let filter_vars_to_none subst_map x = - let vars_to_none = - SubstMap.fold subst_map ~init:VarSet.empty ~f:(fun k v acc -> - match v with None -> VarSet.add k acc | Some _ -> acc ) - in - forget_vars_set vars_to_none x - in - let extend_and_substitute subst_map to_arrays new_env substitute x = - let x = filter_vars_to_none subst_map x in - let vars, exps = to_arrays subst_map in - let x = extend_env new_env x in - substitute man x vars exps None - in - fun ~forget_free subst_map x -> - let vars_in_subst_map = - SubstMap.fold subst_map ~init:VarSet.empty ~f:(fun var sym_exp_opt acc -> - acc |> VarSet.add var |> VarSet.add (Var.param_of var) - |> VarSet.union (SymExp.vars_set_of_opt sym_exp_opt) ) - in - let new_env = Env.of_vars_set vars_in_subst_map in - let x = if forget_free then forget_free_vars vars_in_subst_map x else x in - match Config.bo_relational_domain with - | None -> - assert false - | Some `Bo_relational_domain_oct -> - extend_and_substitute subst_map SubstMap.to_arrays_symexp new_env - Abstract1.substitute_texpr_array x - | Some `Bo_relational_domain_poly -> - let subst_map = SubstMap.map_opt ~f:SymExp.to_linexpr subst_map in - extend_and_substitute subst_map SubstMap.to_arrays_linexpr new_env - Abstract1.substitute_linexpr_array x - end - - module Pack = struct - type t = int [@@deriving compare] - - let equal = Int.equal - - let pp fmt x = F.fprintf fmt "%d" x - - let subst ~from ~to_ x = if equal x from then to_ else x - end - - module PackSet = struct - include PrettyPrintable.MakePPSet (Pack) - - let subst ~from ~to_ x = if mem x from then to_ else x - end - - module PackMap = struct - include PrettyPrintable.MakePPMap (Pack) - - let remove_packs pack_ids x = PackSet.fold remove pack_ids x - end - - module PackedVal = struct - type astate = {pack_ids: Pack.t VarMap.t; packs: Val.astate PackMap.t} [@@deriving compare] - - let empty = {pack_ids= VarMap.empty; packs= PackMap.empty} - - let pp_packs = PackMap.pp ~pp_value:Val.pp - - let pp fmt x = pp_packs fmt x.packs - - let sync_pack x y = - let id_ref = ref 0 in - let get_new_id () : Pack.t = - id_ref := !id_ref + 1 ; - !id_ref - in - let add_subst_partial var id (pack_ids, subst) = - match PackMap.find id subst with - | id' -> - (VarMap.add var id' pack_ids, subst) - | exception Caml.Not_found -> - let id' = get_new_id () in - (VarMap.add var id' pack_ids, PackMap.add id id' subst) - in - let add_subst var id1_opt id2_opt ((pack_ids, subst1, subst2) as subst_res) = - match (id1_opt, id2_opt) with - | Some id1, Some id2 -> ( - match (PackMap.find_opt id1 subst1, PackMap.find_opt id2 subst2) with - | Some id1', Some id2' -> - if Pack.equal id1' id2' then (VarMap.add var id1' pack_ids, subst1, subst2) - else - let pack_ids = - pack_ids |> VarMap.add var id1' |> VarMap.map (Pack.subst ~from:id2' ~to_:id1') - in - let subst1 = PackMap.map (Pack.subst ~from:id2' ~to_:id1') subst1 in - let subst2 = PackMap.map (Pack.subst ~from:id2' ~to_:id1') subst2 in - (pack_ids, subst1, subst2) - | Some id1', None -> - (VarMap.add var id1' pack_ids, subst1, PackMap.add id2 id1' subst2) - | None, Some id2' -> - (VarMap.add var id2' pack_ids, PackMap.add id1 id2' subst1, subst2) - | None, None -> - let id' = get_new_id () in - (VarMap.add var id' pack_ids, PackMap.add id1 id' subst1, PackMap.add id2 id' subst2) - ) - | Some id1, None -> - let pack_ids, subst1 = add_subst_partial var id1 (pack_ids, subst1) in - (pack_ids, subst1, subst2) - | None, Some id2 -> - let pack_ids, subst2 = add_subst_partial var id2 (pack_ids, subst2) in - (pack_ids, subst1, subst2) - | None, None -> - subst_res - in - let get_subst_map pack_ids1 pack_ids2 = - VarMap.fold2 pack_ids1 pack_ids2 ~f:add_subst - ~init:(VarMap.empty, PackMap.empty, PackMap.empty) - in - let subst subst_map packs = - let subst_helper pack_id v acc = - match PackMap.find pack_id subst_map with - | pack_id' -> - let v = - Option.value_map (PackMap.find_opt pack_id' acc) ~default:v ~f:(fun v' -> - Val.meet v' v ) - in - PackMap.add pack_id' v acc - | exception Caml.Not_found -> - acc - in - PackMap.fold subst_helper packs PackMap.empty - in - let pack_ids, subst_map_x, subst_map_y = get_subst_map x.pack_ids y.pack_ids in - (pack_ids, subst subst_map_x x.packs, subst subst_map_y y.packs) - - - let le_synced_packs ~lhs ~rhs = - let ge_than_lhs pack_id rhs = - match PackMap.find pack_id lhs with - | lhs -> - Val.( <= ) ~lhs ~rhs - | exception Caml.Not_found -> - Val.is_top rhs - in - PackMap.for_all ge_than_lhs rhs - - - let join_synced_packs x y = - let join_opt _ v1_opt v2_opt = Option.map2 v1_opt v2_opt ~f:Val.join in - PackMap.merge join_opt x y - - - let meet_synced_packs x y = - let exception BottomByMeet in - let meet_opt _ v1_opt v2_opt = - match (v1_opt, v2_opt) with - | Some v1, Some v2 -> - let v = Val.meet v1 v2 in - if Val.is_bot v then raise BottomByMeet else Some v - | Some v, None | None, Some v -> - Some v - | None, None -> - None - in - match PackMap.merge meet_opt x y with packs -> Some packs | exception BottomByMeet -> None - - - let widen_synced_packs ~prev ~next ~num_iters = - let widen_opt _ prev_opt next_opt = - Option.map2 prev_opt next_opt ~f:(fun prev next -> Val.widen ~prev ~next ~num_iters) - in - PackMap.merge widen_opt prev next - - - let ( <= ) ~lhs ~rhs = - let _, packs_lhs, packs_rhs = sync_pack lhs rhs in - le_synced_packs ~lhs:packs_lhs ~rhs:packs_rhs - - - let join x y = - let pack_ids, packs_x, packs_y = sync_pack x y in - if le_synced_packs ~lhs:packs_x ~rhs:packs_y then y - else if le_synced_packs ~lhs:packs_y ~rhs:packs_x then x - else {pack_ids; packs= join_synced_packs packs_x packs_y} - - - let meet x y = - let pack_ids, packs_x, packs_y = sync_pack x y in - if le_synced_packs ~lhs:packs_x ~rhs:packs_y then NonBottom x - else if le_synced_packs ~lhs:packs_y ~rhs:packs_x then NonBottom y - else - Option.value_map (meet_synced_packs packs_x packs_y) ~default:Bottom ~f:(fun packs -> - NonBottom {pack_ids; packs} ) - - - let widen ~prev ~next ~num_iters = - let pack_ids, packs_prev, packs_next = sync_pack prev next in - {pack_ids; packs= widen_synced_packs ~prev:packs_prev ~next:packs_next ~num_iters} - - - let pack_id_of_var var x = VarMap.find var x.pack_ids - - let pack_id_of_var_opt var x = VarMap.find_opt var x.pack_ids - - let pack_ids_of_vars vars x = - let add_id var acc = - Option.value_map (pack_id_of_var_opt var x) ~default:acc ~f:(fun id -> PackSet.add id acc) - in - VarSet.fold add_id vars PackSet.empty - - - let val_of_pack_id_opt pack_id x = PackMap.find_opt pack_id x.packs - - let val_of_pack_id pack_id x = Option.value (val_of_pack_id_opt pack_id x) ~default:Val.top - - let val_of_pack_ids ids x = - let meet_val id acc = - Option.value_map (val_of_pack_id_opt id x) ~default:acc ~f:(fun v -> Val.meet acc v) - in - PackSet.fold meet_val ids Val.top - - - let val_of_vars vars x = val_of_pack_ids (pack_ids_of_vars vars x) x - - let lt_sat e1 e2 x = - let vars = VarSet.union (SymExp.vars_set_of e1) (SymExp.vars_set_of e2) in - Val.lt_sat e1 e2 (val_of_vars vars x) - - - let le_sat e1 e2 x = - let vars = VarSet.union (SymExp.vars_set_of e1) (SymExp.vars_set_of e2) in - Val.le_sat e1 e2 (val_of_vars vars x) - - - let lift_sat_opt f e1_opt e2_opt x = - match (e1_opt, e2_opt) with Some e1, Some e2 -> f e1 e2 x | _, _ -> false - - - let lt_sat_opt = lift_sat_opt lt_sat - - let le_sat_opt = lift_sat_opt le_sat - - let repack_with_vars vars x = - let id_ref = - let max_pack_id = - VarMap.fold x.pack_ids ~init:0 ~f:(fun _ pack_id acc -> max acc pack_id) - in - ref max_pack_id - in - let get_new_id () : Pack.t = - id_ref := !id_ref + 1 ; - !id_ref - in - let set_pack_id_of_vars vars id pack_ids = - VarSet.fold (fun var acc -> VarMap.add var id acc) vars pack_ids - in - let vars_ids = pack_ids_of_vars vars x in - let num_vars_ids = PackSet.cardinal vars_ids in - if Int.equal num_vars_ids 0 then - let id = get_new_id () in - {x with pack_ids= set_pack_id_of_vars vars id x.pack_ids} - else if Int.equal num_vars_ids 1 then - let id = PackSet.choose vars_ids in - {x with pack_ids= set_pack_id_of_vars vars id x.pack_ids} - else - let id = PackSet.min_elt vars_ids in - let other_ids = PackSet.remove id vars_ids in - let pack_ids = - x.pack_ids |> set_pack_id_of_vars vars id - |> VarMap.map (PackSet.subst ~from:other_ids ~to_:id) - in - let packs = - let v = val_of_pack_ids vars_ids x in - x.packs |> PackMap.remove_packs other_ids |> PackMap.add id v - in - {pack_ids; packs} - - - let subst ~forget_free subst_map x = - let exception BottomBySubst in - let repack_for_subst subst_map x = - SubstMap.fold subst_map ~init:x ~f:(fun var sym_exp_opt acc -> - let vars = VarSet.add var (SymExp.vars_set_of_opt sym_exp_opt) in - repack_with_vars vars acc ) - in - let pack_subst_map x subst_map = - let add_subst var exp acc = - let pack_id = pack_id_of_var var x in - match PackMap.find pack_id acc with - | subst_map -> - PackMap.add pack_id (SubstMap.add var exp subst_map) acc - | exception Caml.Not_found -> - PackMap.add pack_id (SubstMap.singleton var exp) acc - in - SubstMap.fold subst_map ~init:PackMap.empty ~f:add_subst - in - let do_subst packed_subst_map pack_id v acc = - let subst_map = - Option.value (PackMap.find_opt pack_id packed_subst_map) ~default:SubstMap.empty - in - let v = Val.subst ~forget_free subst_map v in - if Val.is_bot v then raise BottomBySubst else PackMap.add pack_id v acc - in - let x = repack_for_subst subst_map x in - let packed_subst_map = pack_subst_map x subst_map in - match PackMap.fold (do_subst packed_subst_map) x.packs PackMap.empty with - | packs -> - NonBottom {x with packs} - | exception BottomBySubst -> - Bottom - - - let meet_constraints constrs x = - let vars = Constraints.vars_set_of constrs in - if VarSet.is_empty vars then - if Val.is_unsat_constraints constrs Val.top then Bottom else NonBottom x - else - let x = repack_with_vars vars x in - let pack_id = pack_id_of_var (VarSet.choose vars) x in - let v = Val.meet_constraints constrs (val_of_pack_id pack_id x) in - if Val.is_bot v then Bottom else NonBottom {x with packs= PackMap.add pack_id v x.packs} - - - let store_relation locs (int_exp, offset_exp, size_exp) x = - let store_relation' varset_of_locs exp_opt val_store_relation x = - let vars_of_exp = VarSet.union (varset_of_locs locs) (SymExp.vars_set_of_opt exp_opt) in - let x = repack_with_vars vars_of_exp x in - let pack_id = pack_id_of_var (VarSet.choose vars_of_exp) x in - let v = val_store_relation locs exp_opt (val_of_pack_id pack_id x) in - if Val.is_bot v then Bottom else NonBottom {x with packs= PackMap.add pack_id v x.packs} - in - let ( ||> ) x f = match x with Bottom -> Bottom | NonBottom x -> f x in - if PowLoc.is_empty locs then NonBottom x - else - store_relation' VarSet.int_of_powloc int_exp Val.store_relation_int x - ||> store_relation' VarSet.offset_of_powloc offset_exp Val.store_relation_offset - ||> store_relation' VarSet.size_of_powloc size_exp Val.store_relation_size - - - let forget_var var x = - let forget_var_in pack_id = - let pack_ids = VarMap.remove var x.pack_ids in - let packs = - Option.value_map (val_of_pack_id_opt pack_id x) ~default:x.packs ~f:(fun v -> - PackMap.add pack_id (Val.forget_var var v) x.packs ) - in - {pack_ids; packs} - in - Option.value_map (pack_id_of_var_opt var x) ~default:x ~f:forget_var_in - - - let forget_loc loc x = forget_var (Var.of_loc loc) x - - let forget_locs locs x = PowLoc.fold forget_loc locs x - - let forget_vars vars x = VarSet.fold forget_var vars x - - let init_param loc x = - let param_var = Var.param_of_loc loc in - let var = Var.of_loc loc in - meet_constraints (Constraints.eq_of param_var var) x - - - let init_array allocsite ~offset ~size ~size_exp_opt x = - let offset_sym = Sym.of_allocsite_offset allocsite in - let size_sym = Sym.of_allocsite_size allocsite in - let offset_constrs = Constraints.itv_of offset_sym offset in - let size_constrs = - match size_exp_opt with - | None -> - Constraints.itv_of size_sym size - | Some size_exp -> - match Constraints.eq_of_sym size_sym size_exp with - | None -> - Constraints.itv_of size_sym size - | Some constr -> - constr - in - meet_constraints (Constraints.and_ offset_constrs size_constrs) x - - - let subst_param_caller subst_map caller = - let accum_rev_if_var k v acc = - Option.value_map (SymExp.to_var v) ~default:acc ~f:(fun k' -> - SubstMap.add k' (Some (SymExp.of_var (Var.temp_param_of k))) acc ) - in - let accum_rev k v_opt acc = - Option.value_map v_opt ~default:acc ~f:(fun v -> accum_rev_if_var k v acc) - in - let rev_subst_map = SubstMap.fold subst_map ~init:SubstMap.empty ~f:accum_rev in - subst ~forget_free:false rev_subst_map caller - - - let subst_callee subst_map callee = - let accum_param_subst k v acc = - let v = - match v with - | Some v' when SymExp.is_var v' -> - Some (SymExp.of_var (Var.temp_param_of k)) - | _ -> - v - in - SubstMap.add (Var.param_of k) v acc - in - let param_subst_map = SubstMap.fold subst_map ~init:SubstMap.empty ~f:accum_param_subst in - subst ~forget_free:true param_subst_map callee - - - let forget_temp_param subst_map x = - let temps = - SubstMap.fold subst_map ~init:VarSet.empty ~f:(fun k _ acc -> - VarSet.add (Var.temp_param_of k) acc ) - in - forget_vars temps x - - - let instantiate ~caller ~callee subst_map = - match subst_param_caller subst_map caller with - | Bottom -> - Bottom - | NonBottom caller -> - match subst_callee subst_map callee with - | Bottom -> - Bottom - | NonBottom callee -> - match meet caller callee with - | Bottom -> - Bottom - | NonBottom relation -> - NonBottom (forget_temp_param subst_map relation) - end - - include AbstractDomain.BottomLifted (PackedVal) - - let compare_astate x y = - match (x, y) with - | Bottom, Bottom -> - 0 - | Bottom, _ -> - -1 - | _, Bottom -> - 1 - | NonBottom x', NonBottom y' -> - PackedVal.compare_astate x' y' - - - let empty : astate = NonBottom PackedVal.empty - - let bot : astate = Bottom - - let is_unsat : astate -> bool = function Bottom -> true | NonBottom _ -> false - - let lift_default : default:'a -> (PackedVal.astate -> 'a) -> astate -> 'a = - fun ~default f -> function Bottom -> default | NonBottom x -> f x - - - let lift : (PackedVal.astate -> PackedVal.astate) -> astate -> astate = - fun f -> function Bottom -> Bottom | NonBottom x -> NonBottom (f x) - - - let lift2 : (PackedVal.astate -> PackedVal.astate -> astate) -> astate -> astate -> astate = - fun f x y -> - match (x, y) with Bottom, _ | _, Bottom -> Bottom | NonBottom x', NonBottom y' -> f x' y' - - - let lt_sat_opt : SymExp.t option -> SymExp.t option -> astate -> bool = - fun e1_opt e2_opt -> lift_default ~default:true (PackedVal.lt_sat_opt e1_opt e2_opt) - - - let le_sat_opt : SymExp.t option -> SymExp.t option -> astate -> bool = - fun e1_opt e2_opt -> lift_default ~default:true (PackedVal.le_sat_opt e1_opt e2_opt) - - - let meet_constraints : Constraints.t -> astate -> astate = - fun constrs -> lift_default ~default:Bottom (PackedVal.meet_constraints constrs) - - - let store_relation - : PowLoc.t -> SymExp.t option * SymExp.t option * SymExp.t option -> astate -> astate = - fun locs texpr_opts -> lift_default ~default:Bottom (PackedVal.store_relation locs texpr_opts) - - - let init_param : Loc.t -> astate -> astate = - fun loc -> lift_default ~default:Bottom (PackedVal.init_param loc) - - - let init_array - : Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:SymExp.t option -> astate - -> astate = - fun allocsite ~offset ~size ~size_exp_opt -> - lift_default ~default:Bottom (PackedVal.init_array allocsite ~offset ~size ~size_exp_opt) - - - let forget_locs : PowLoc.t -> astate -> astate = fun locs -> lift (PackedVal.forget_locs locs) - - let instantiate : caller:astate -> callee:astate -> SubstMap.t -> astate = - fun ~caller ~callee subst_map -> - lift2 (fun caller callee -> PackedVal.instantiate ~caller ~callee subst_map) caller callee -end - -module ApronOctagonManager = struct - type domain_t = Oct.t - - let alloc_man : unit -> domain_t Manager.t = Oct.manager_alloc -end - -module ElinaPolyManager = struct - type domain_t = Elina_poly.loose Elina_poly.t - - let alloc_man : unit -> domain_t Manager.t = Elina_poly.manager_alloc_loose -end - -include ( val match Config.bo_relational_domain with - | None -> - (module NoRelation : S) - | Some `Bo_relational_domain_oct -> - (module Make (ApronOctagonManager) : S) - | Some `Bo_relational_domain_poly -> - (module Make (ElinaPolyManager) : S) -) - -(* NOTE: Globally only one manager (of a relational domain depends on - Apron) can set deserialization functions. *) -let () = set_deserialize () diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 58f1273f4..1c82979e9 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -13,7 +13,6 @@ module BoUtils = BufferOverrunUtils module Dom = BufferOverrunDomain module PO = BufferOverrunProofObligations module Sem = BufferOverrunSemantics -module Relation = BufferOverrunDomainRelation module Trace = BufferOverrunTrace module TraceSet = Trace.Set @@ -83,17 +82,12 @@ let malloc size_exp = let typ, stride, length0, dyn_length = get_malloc_info size_exp in let length = Sem.eval length0 mem in let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in - let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num:0 ~dimension:1 in - let offset, size = (Itv.zero, Dom.Val.get_itv length) in - let size_exp_opt = - let size_exp = Option.value dyn_length ~default:length0 in - Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f mem) size_exp - in let v = - Sem.eval_array_alloc allocsite typ ~stride ~offset ~size |> Dom.Val.set_traces traces + Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero + ~size:(Dom.Val.get_itv length) ~inst_num:0 ~dimension:1 + |> Dom.Val.set_traces traces in mem |> Dom.Mem.add_stack (Loc.of_id id) v - |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt |> set_uninitialized location typ (Dom.Val.get_array_locs v) |> BoUtils.Exec.init_array_fields tenv pname ~node_hash typ (Dom.Val.get_array_locs v) ?dyn_length @@ -184,8 +178,10 @@ let set_array_length array length_exp = | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} -> let length = Sem.eval length_exp mem |> Dom.Val.get_itv in let stride = Option.map ~f:IntLit.to_int stride in - let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num:0 ~dimension:1 in - let v = Sem.eval_array_alloc allocsite elt ~stride ~offset:Itv.zero ~size:length in + let v = + Sem.eval_array_alloc pname ~node_hash elt ~stride ~offset:Itv.zero ~size:length + ~inst_num:0 ~dimension:1 + in mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v |> set_uninitialized location elt (Dom.Val.get_array_locs v) | _ -> diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 27a523dd1..e0c0f1726 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -10,7 +10,6 @@ open! AbstractDomain.Types module F = Format module L = Logging module ItvPure = Itv.ItvPure -module Relation = BufferOverrunDomainRelation module MF = MarkupFormatter module ValTraceSet = BufferOverrunTrace.Set @@ -94,13 +93,7 @@ module AllocSizeCondition = struct end module ArrayAccessCondition = struct - type t = - { idx: ItvPure.astate - ; size: ItvPure.astate - ; idx_sym_exp: Relation.SymExp.t option - ; size_sym_exp: Relation.SymExp.t option - ; relation: Relation.astate } - [@@deriving compare] + type t = {idx: ItvPure.astate; size: ItvPure.astate} [@@deriving compare] let get_symbols c = ItvPure.get_symbols c.idx @ ItvPure.get_symbols c.size @@ -113,10 +106,7 @@ module ArrayAccessCondition = struct let pp : F.formatter -> t -> unit = fun fmt c -> let c = set_size_pos c in - F.fprintf fmt "%a < %a" ItvPure.pp c.idx ItvPure.pp c.size ; - if Option.is_some Config.bo_relational_domain then - F.fprintf fmt "@,%a < %a when %a" Relation.SymExp.pp_opt c.idx_sym_exp Relation.SymExp.pp_opt - c.size_sym_exp Relation.pp c.relation + F.fprintf fmt "%a < %a" ItvPure.pp c.idx ItvPure.pp c.size let pp_description : F.formatter -> t -> unit = @@ -125,12 +115,9 @@ module ArrayAccessCondition = struct F.fprintf fmt "Offset: %a Size: %a" ItvPure.pp c.idx ItvPure.pp c.size - let make - : idx:ItvPure.t -> size:ItvPure.t -> idx_sym_exp:Relation.SymExp.t option - -> size_sym_exp:Relation.SymExp.t option -> relation:Relation.astate -> t option = - fun ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation -> - if ItvPure.is_invalid idx || ItvPure.is_invalid size then None - else Some {idx; size; idx_sym_exp; size_sym_exp; relation} + let make : idx:ItvPure.t -> size:ItvPure.t -> t option = + fun ~idx ~size -> + if ItvPure.is_invalid idx || ItvPure.is_invalid size then None else Some {idx; size} let have_similar_bounds {idx= lidx; size= lsiz} {idx= ridx; size= rsiz} = @@ -219,15 +206,8 @@ module ArrayAccessCondition = struct (* idx = [il, iu], size = [sl, su], we want to check that 0 <= idx < size *) let c' = set_size_pos c in (* if sl < 0, use sl' = 0 *) - let not_overrun = - if Relation.lt_sat_opt c'.idx_sym_exp c'.size_sym_exp c'.relation then Itv.Boolean.true_ - else ItvPure.lt_sem c'.idx c'.size - in - let not_underrun = - if Relation.le_sat_opt (Some Relation.SymExp.zero) c'.idx_sym_exp c'.relation then - Itv.Boolean.true_ - else ItvPure.le_sem ItvPure.zero c'.idx - in + let not_overrun = ItvPure.lt_sem c'.idx c'.size in + let not_underrun = ItvPure.le_sem ItvPure.zero c'.idx in (* il >= 0 and iu < sl, definitely not an error *) if Itv.Boolean.is_true not_overrun && Itv.Boolean.is_true not_underrun then {report_issue_type= None; propagate= false} (* iu < 0 or il >= su, definitely an error *) @@ -255,22 +235,13 @@ module ArrayAccessCondition = struct {report_issue_type; propagate= is_symbolic} - let subst - : Itv.Bound.t bottom_lifted Itv.SymbolMap.t -> Relation.SubstMap.t -> Relation.astate -> t - -> t option = - fun bound_map rel_map caller_relation c -> + let subst : Itv.Bound.t bottom_lifted Itv.SymbolMap.t -> t -> t option = + fun bound_map c -> match (ItvPure.subst c.idx bound_map, ItvPure.subst c.size bound_map) with | NonBottom idx, NonBottom size -> - let idx_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.idx_sym_exp in - let size_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.size_sym_exp in - let relation = Relation.instantiate rel_map ~caller:caller_relation ~callee:c.relation in - Some {idx; size; idx_sym_exp; size_sym_exp; relation} + Some {idx; size} | _ -> None - - - let forget_locs : AbsLoc.PowLoc.t -> t -> t = - fun locs c -> {c with relation= Relation.forget_locs locs c.relation} end module Condition = struct @@ -287,11 +258,11 @@ module Condition = struct ArrayAccessCondition.get_symbols c - let subst bound_map rel_map caller_relation = function + let subst bound_map = function | AllocSize c -> AllocSizeCondition.subst bound_map c |> make_alloc_size | ArrayAccess c -> - ArrayAccessCondition.subst bound_map rel_map caller_relation c |> make_array_access + ArrayAccessCondition.subst bound_map c |> make_array_access let have_similar_bounds c1 c2 = @@ -335,14 +306,6 @@ module Condition = struct AllocSizeCondition.check c | ArrayAccess c -> ArrayAccessCondition.check c - - - let forget_locs locs x = - match x with - | ArrayAccess c -> - ArrayAccess (ArrayAccessCondition.forget_locs locs c) - | AllocSize _ -> - x end module ConditionTrace = struct @@ -423,12 +386,12 @@ module ConditionWithTrace = struct cmp - let subst (bound_map, trace_map) rel_map caller_relation caller_pname callee_pname location cwt = + let subst (bound_map, trace_map) caller_pname callee_pname location cwt = match Condition.get_symbols cwt.cond with | [] -> Some cwt | symbols -> - match Condition.subst bound_map rel_map caller_relation cwt.cond with + match Condition.subst bound_map cwt.cond with | None -> None | Some cond -> @@ -462,9 +425,6 @@ module ConditionWithTrace = struct report_issue_type |> Option.map ~f:(set_buffer_overrun_u5 cwt) |> Option.iter ~f:(report cwt.cond cwt.trace) ; propagate - - - let forget_locs locs cwt = {cwt with cond= Condition.forget_locs locs cwt.cond} end module ConditionSet = struct @@ -526,10 +486,9 @@ module ConditionSet = struct join [cwt] condset - let add_array_access pname location ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation val_traces - condset = - ArrayAccessCondition.make ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation - |> Condition.make_array_access |> add_opt pname location val_traces condset + let add_array_access pname location ~idx ~size val_traces condset = + ArrayAccessCondition.make ~idx ~size |> Condition.make_array_access + |> add_opt pname location val_traces condset let add_alloc_size pname location ~length val_traces condset = @@ -537,12 +496,10 @@ module ConditionSet = struct |> add_opt pname location val_traces condset - let subst condset bound_map_trace_map rel_subst_map caller_relation caller_pname callee_pname - location = + let subst condset bound_map_trace_map caller_pname callee_pname location = let subst_add_cwt condset cwt = match - ConditionWithTrace.subst bound_map_trace_map rel_subst_map caller_relation caller_pname - callee_pname location cwt + ConditionWithTrace.subst bound_map_trace_map caller_pname callee_pname location cwt with | None -> condset @@ -566,14 +523,12 @@ module ConditionSet = struct let pp : Format.formatter -> t -> unit = fun fmt condset -> - let pp_sep fmt () = F.fprintf fmt ",@," in - F.fprintf fmt "Safety conditions:@;@[{ %a }@]" - (F.pp_print_list ~pp_sep ConditionWithTrace.pp) - condset - - - let forget_locs : AbsLoc.PowLoc.t -> t -> t = - fun locs x -> List.map x ~f:(ConditionWithTrace.forget_locs locs) + let pp_sep fmt () = F.fprintf fmt ", @," in + F.fprintf fmt "@[Safety conditions :@," ; + F.fprintf fmt "@[{" ; + F.pp_print_list ~pp_sep ConditionWithTrace.pp fmt condset ; + F.fprintf fmt " }@]" ; + F.fprintf fmt "@]" end let description cond trace = diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index e76be7dbe..5f4d47bb2 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -314,7 +314,7 @@ let rec eval_arr : Exp.t -> Mem.astate -> Val.t = Val.bot -let get_allocsite : Typ.Procname.t -> node_hash:int -> inst_num:int -> dimension:int -> Allocsite.t = +let get_allocsite : Typ.Procname.t -> node_hash:int -> inst_num:int -> dimension:int -> string = fun proc_name ~node_hash ~inst_num ~dimension -> let proc_name = Typ.Procname.to_string proc_name in let node_num = string_of_int node_hash in @@ -324,19 +324,15 @@ let get_allocsite : Typ.Procname.t -> node_hash:int -> inst_num:int -> dimension let eval_array_alloc - : Allocsite.t -> Typ.t -> stride:int option -> offset:Itv.t -> size:Itv.t -> Val.t = - fun allocsite typ ~stride ~offset ~size -> + : Typ.Procname.t -> node_hash:int -> Typ.t -> stride:int option -> offset:Itv.t -> size:Itv.t + -> inst_num:int -> dimension:int -> Val.t = + fun pdesc ~node_hash typ ~stride ~offset ~size ~inst_num ~dimension -> + let allocsite = get_allocsite pdesc ~node_hash ~inst_num ~dimension in let int_stride = match stride with None -> sizeof typ | Some stride -> stride in let stride = Itv.of_int int_stride in - ArrayBlk.make allocsite ~offset ~size ~stride |> Val.of_array_blk ~allocsite + ArrayBlk.make allocsite ~offset ~size ~stride |> Val.of_array_blk -let get_sym_f mem e = Val.get_sym (eval e mem) - -let get_offset_sym_f mem e = Val.get_offset_sym (eval e mem) - -let get_size_sym_f mem e = Val.get_size_sym (eval e mem) - module Prune = struct type astate = {prune_pairs: PrunePairs.t; mem: Mem.astate} @@ -427,16 +423,12 @@ module Prune = struct let is_unreachable_constant : Exp.t -> Mem.astate -> bool = - fun e m -> - let v = eval e m in - Itv.( <= ) ~lhs:(Val.get_itv v) ~rhs:(Itv.of_int 0) && PowLoc.is_bot (Val.get_pow_loc v) - && ArrayBlk.is_bot (Val.get_array_blk v) + fun e m -> Val.( <= ) ~lhs:(eval e m) ~rhs:(Val.of_int 0) let prune_unreachable : Exp.t -> astate -> astate = fun e ({mem} as astate) -> - if is_unreachable_constant e mem || Mem.is_relation_unsat mem then {astate with mem= Mem.bot} - else astate + if is_unreachable_constant e mem then {astate with mem= Mem.bot} else astate let rec prune_helper e astate = @@ -469,10 +461,6 @@ module Prune = struct let prune : Exp.t -> Mem.astate -> Mem.astate = fun e mem -> let mem = Mem.apply_latest_prune e mem in - let mem = - let constrs = Relation.Constraints.of_exp e ~get_sym_f:(get_sym_f mem) in - Mem.meet_constraints constrs mem - in let {mem; prune_pairs} = prune_helper e {mem; prune_pairs= PrunePairs.empty} in Mem.set_prune_pairs prune_pairs mem end @@ -484,17 +472,13 @@ let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list = let get_matching_pairs - : Tenv.t -> Val.t -> Val.t -> Exp.t option -> Typ.t -> Mem.astate -> Mem.astate + : Tenv.t -> Val.t -> Val.t -> Typ.t -> Mem.astate -> Mem.astate -> callee_ret_alias:AliasTarget.t option - -> (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list - * AliasTarget.t option - * (Relation.Var.t * Relation.SymExp.t option) list = - fun tenv formal actual actual_exp_opt typ caller_mem callee_mem ~callee_ret_alias -> + -> (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list * AliasTarget.t option = + fun tenv formal actual typ caller_mem callee_mem ~callee_ret_alias -> 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_offset_sym v = Val.get_offset_sym v in - let get_size_sym v = Val.get_size_sym v in let get_field_name (fn, _, _) = fn in let append_field v fn = PowLoc.append_field (Val.get_all_locs v) ~fn in let deref_field v fn mem = Mem.find_heap_set (append_field v fn) mem in @@ -522,38 +506,17 @@ let get_matching_pairs else (lb itv1, NonBottom (lb itv2), traces) :: (ub itv1, NonBottom (ub itv2), traces) :: l else l in - let add_pair_sym_main_value v1 v2 ~e2_opt l = - Option.value_map (Val.get_sym_var v1) ~default:l ~f:(fun var -> - let sym_exp_opt = - Option.first_some - (Relation.SymExp.of_exp_opt ~get_sym_f:(get_sym_f caller_mem) e2_opt) - (Relation.SymExp.of_sym (Val.get_sym v2)) - in - (var, sym_exp_opt) :: l ) - in - let add_pair_sym s1 s2 l = - Option.value_map (Relation.Sym.get_var s1) ~default:l ~f:(fun var -> - (var, Relation.SymExp.of_sym s2) :: l ) - in - let add_pair_val v1 v2 ~e2_opt (bound_pairs, rel_pairs) = + let add_pair_val v1 v2 pairs = add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ; - let bound_pairs = - bound_pairs |> add_pair_itv (get_itv v1) (get_itv v2) (Val.get_traces v2) - |> add_pair_itv (get_offset v1) (get_offset v2) (Val.get_traces v2) - |> add_pair_itv (get_size v1) (get_size v2) (Val.get_traces v2) - in - let rel_pairs = - rel_pairs |> add_pair_sym_main_value v1 v2 ~e2_opt - |> add_pair_sym (get_offset_sym v1) (get_offset_sym v2) - |> add_pair_sym (get_size_sym v1) (get_size_sym v2) - in - (bound_pairs, rel_pairs) + pairs |> add_pair_itv (get_itv v1) (get_itv v2) (Val.get_traces v2) + |> add_pair_itv (get_offset v1) (get_offset v2) (Val.get_traces v2) + |> add_pair_itv (get_size v1) (get_size v2) (Val.get_traces v2) in let add_pair_field v1 v2 pairs fn = add_ret_alias (append_field v1 fn) (append_field v2 fn) ; let v1' = deref_field v1 fn callee_mem in let v2' = deref_field v2 fn caller_mem in - add_pair_val v1' v2' ~e2_opt:None pairs + add_pair_val v1' v2' pairs in let add_pair_ptr typ v1 v2 pairs = add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ; @@ -568,17 +531,15 @@ let get_matching_pairs | Typ.Tptr (_, _) -> let v1' = deref_ptr v1 callee_mem in let v2' = deref_ptr v2 caller_mem in - add_pair_val v1' v2' ~e2_opt:None pairs + add_pair_val v1' v2' pairs | _ -> pairs in - let bound_pairs, rel_pairs = - ([], []) |> add_pair_val formal actual ~e2_opt:actual_exp_opt |> add_pair_ptr typ formal actual - in - (bound_pairs, !ret_alias, rel_pairs) + let pairs = [] |> add_pair_val formal actual |> add_pair_ptr typ formal actual in + (pairs, !ret_alias) -let subst_map_of_bound_pairs +let subst_map_of_pairs : (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list -> Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t = fun pairs -> @@ -591,16 +552,8 @@ let subst_map_of_bound_pairs List.fold ~f:add_pair ~init:(Itv.SymbolMap.empty, Itv.SymbolMap.empty) pairs -let subst_map_of_rel_pairs - : (Relation.Var.t * Relation.SymExp.t option) list -> Relation.SubstMap.t = - fun pairs -> - let add_pair rel_map (x, e) = Relation.SubstMap.add x e rel_map in - List.fold pairs ~init:Relation.SubstMap.empty ~f:add_pair - - let rec list_fold2_def - : default:Val.t * Exp.t option -> f:('a -> Val.t * Exp.t option -> 'b -> 'b) -> 'a list - -> (Val.t * Exp.t option) list -> init:'b -> 'b = + : default:Val.t -> f:('a -> Val.t -> 'b -> 'b) -> 'a list -> Val.t list -> init:'b -> 'b = fun ~default ~f xs ys ~init:acc -> match (xs, ys) with | [], _ -> @@ -608,9 +561,7 @@ let rec list_fold2_def | x :: xs', [] -> list_fold2_def ~default ~f xs' ys ~init:(f x default acc) | [x], _ :: _ -> - let v = List.fold ys ~init:Val.bot ~f:(fun acc (y, _) -> Val.join y acc) in - let exp_opt = match ys with [(_, exp_opt)] -> exp_opt | _ -> None in - f x (v, exp_opt) acc + f x (List.fold ~f:Val.join ~init:Val.bot ys) acc | x :: xs', y :: ys' -> list_fold2_def ~default ~f xs' ys' ~init:(f x y acc) @@ -619,22 +570,18 @@ let get_subst_map : Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate -> callee_ret_alias:AliasTarget.t option -> (Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t) - * AliasTarget.t option - * Relation.SubstMap.t = + * AliasTarget.t option = fun tenv callee_pdesc params caller_mem callee_entry_mem ~callee_ret_alias -> - let add_pair (formal, typ) (actual, actual_exp) (bound_l, ret_alias, rel_l) = + let add_pair (formal, typ) actual (l, ret_alias) = let formal = Mem.find_heap (Loc.of_pvar formal) callee_entry_mem in - let new_bound_matching, ret_alias', new_rel_matching = - get_matching_pairs tenv formal actual actual_exp typ caller_mem callee_entry_mem - ~callee_ret_alias + let new_matching, ret_alias' = + get_matching_pairs tenv formal actual typ caller_mem callee_entry_mem ~callee_ret_alias in - ( List.rev_append new_bound_matching bound_l - , Option.first_some ret_alias ret_alias' - , List.rev_append new_rel_matching rel_l ) + (List.rev_append new_matching l, Option.first_some ret_alias ret_alias') in let formals = get_formals callee_pdesc in - let actuals = List.map ~f:(fun (a, _) -> (eval a caller_mem, Some a)) params in - let bound_pairs, ret_alias, rel_pairs = - list_fold2_def ~default:(Val.Itv.top, None) ~f:add_pair formals actuals ~init:([], None, []) + let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem) params in + let pairs, ret_alias = + list_fold2_def ~default:Val.Itv.top ~f:add_pair formals actuals ~init:([], None) in - (subst_map_of_bound_pairs bound_pairs, ret_alias, subst_map_of_rel_pairs rel_pairs) + (subst_map_of_pairs pairs, ret_alias) diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 1aa48a176..79e259958 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -10,7 +10,6 @@ open AbsLoc open! AbstractDomain.Types module L = Logging module Dom = BufferOverrunDomain -module Relation = BufferOverrunDomainRelation module PO = BufferOverrunProofObligations module Sem = BufferOverrunSemantics module Trace = BufferOverrunTrace @@ -34,18 +33,15 @@ module Exec = struct -> length:IntLit.t option -> ?stride:int -> inst_num:int -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int = fun ~decl_local pname ~node_hash location loc typ ~length ?stride ~inst_num ~dimension mem -> - let offset = Itv.zero in let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in - let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension in let arr = - Sem.eval_array_alloc allocsite typ ~stride ~offset ~size + Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero ~size ~inst_num ~dimension |> Dom.Val.add_trace_elem (Trace.ArrDecl location) 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 mem = Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None mem in - let loc = Loc.of_allocsite allocsite in + let loc = Loc.of_allocsite (Sem.get_allocsite pname ~node_hash ~inst_num ~dimension) in let mem, _ = decl_local pname ~node_hash location loc typ ~inst_num ~dimension:(dimension + 1) mem in @@ -73,14 +69,12 @@ module Exec = struct in let alloc_num = Itv.Counter.next new_alloc_num in let elem = Trace.SymAssign (loc, location) in - let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension:alloc_num in let arr = - Sem.eval_array_alloc allocsite typ ~stride:None ~offset ~size |> Dom.Val.add_trace_elem elem - in - let mem = - mem |> Dom.Mem.add_heap loc arr |> Dom.Mem.init_param_relation loc - |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None + Sem.eval_array_alloc pname ~node_hash typ ~stride:None ~offset ~size ~inst_num + ~dimension:alloc_num + |> Dom.Val.add_trace_elem elem in + let mem = Dom.Mem.add_heap loc arr mem in let deref_loc = Loc.of_allocsite (Sem.get_allocsite pname ~node_hash ~inst_num ~dimension:alloc_num) in @@ -101,11 +95,11 @@ module Exec = struct Itv.plus i length ) in let stride = Option.map stride ~f:IntLit.to_int in - let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension in - let offset, size = (Itv.zero, length) in - let v = Sem.eval_array_alloc allocsite typ ~stride ~offset ~size in - mem |> Dom.Mem.strong_update_heap field_loc v - |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None + let v = + Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero ~size:length + ~inst_num ~dimension + in + Dom.Mem.strong_update_heap field_loc v mem | _ -> init_fields field_typ field_loc dimension ?dyn_length mem in @@ -147,21 +141,14 @@ module Exec = struct end module Check = struct - let array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus pname location cond_set = + let array_access ~arr ~idx ~is_plus pname location cond_set = let arr_blk = Dom.Val.get_array_blk arr in let arr_traces = Dom.Val.get_traces arr in let size = ArrayBlk.sizeof arr_blk in - let size_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_size_sym arr) in let offset = ArrayBlk.offsetof arr_blk in - let offset_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_offset_sym arr) in let idx_itv = Dom.Val.get_itv idx in let idx_traces = Dom.Val.get_traces idx in let idx_in_blk = (if is_plus then Itv.plus else Itv.minus) offset idx_itv in - let idx_sym_exp = - Option.map2 offset_sym_exp idx_sym_exp ~f:(fun offset_sym_exp idx_sym_exp -> - let op = if is_plus then Relation.SymExp.plus else Relation.SymExp.minus in - op idx_sym_exp offset_sym_exp ) - in L.(debug BufferOverrun Verbose) "@[Add condition :@," ; L.(debug BufferOverrun Verbose) "array: %a@," ArrayBlk.pp arr_blk ; L.(debug BufferOverrun Verbose) " idx: %a@," Itv.pp idx_in_blk ; @@ -169,8 +156,7 @@ module Check = struct match (size, idx_in_blk) with | NonBottom size, NonBottom idx -> let traces = TraceSet.merge ~arr_traces ~idx_traces location in - PO.ConditionSet.add_array_access pname location ~size ~idx ~size_sym_exp ~idx_sym_exp - ~relation traces cond_set + PO.ConditionSet.add_array_access pname location ~size ~idx traces cond_set | _ -> cond_set @@ -178,7 +164,5 @@ module Check = struct let lindex ~array_exp ~index_exp mem pname location cond_set = let arr = Sem.eval_arr array_exp mem in let idx = Sem.eval index_exp mem in - let idx_sym_exp = Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f mem) index_exp in - let relation = Dom.Mem.get_relation mem in - array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true pname location cond_set + array_access ~arr ~idx ~is_plus:true pname location cond_set end diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index d674290c1..0f04fb0bd 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -8,7 +8,6 @@ open! IStd open AbsLoc module Dom = BufferOverrunDomain -module Relation = BufferOverrunDomainRelation module PO = BufferOverrunProofObligations module Exec : sig @@ -42,8 +41,7 @@ end module Check : sig val array_access : - arr:Dom.Val.t -> idx:Dom.Val.t -> idx_sym_exp:Relation.SymExp.t option - -> relation:Relation.astate -> is_plus:bool -> Typ.Procname.t -> Location.t + arr:Dom.Val.t -> idx:Dom.Val.t -> is_plus:bool -> Typ.Procname.t -> Location.t -> PO.ConditionSet.t -> PO.ConditionSet.t val lindex : diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index ba43d4b2a..f587d5733 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -35,8 +35,6 @@ module Boolean = struct let top = Top - let true_ = True - let equal = [%compare.equal : t] let is_false = function False -> true | _ -> false diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index d72e418e0..50437ad04 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -22,8 +22,6 @@ module Boolean : sig val top : t - val true_ : t - val equal : t -> t -> bool val is_false : t -> bool diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 572514fd7..242687f9c 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -61,7 +61,7 @@ module TransferFunctionsNodesBasicCost = struct let callee_entry_mem = BufferOverrunDomain.Summary.get_input inferbo_summary in let callee_exit_mem = BufferOverrunDomain.Summary.get_output inferbo_summary in let callee_ret_alias = BufferOverrunDomain.Mem.find_ret_alias callee_exit_mem in - let (subst_map, _), _, _ = + let (subst_map, _), _ = BufferOverrunSemantics.get_subst_map tenv callee_pdesc params inferbo_caller_mem callee_entry_mem ~callee_ret_alias in diff --git a/infer/src/deadcode/jbuild.in b/infer/src/deadcode/jbuild.in index f289f0cbb..e4be88c2c 100644 --- a/infer/src/deadcode/jbuild.in +++ b/infer/src/deadcode/jbuild.in @@ -1,8 +1,6 @@ (* -*- tuareg -*- *) (* NOTE: prepend jbuild.common to this file! *) -let deadcode_cflags = common_cflags @ ["-cclib -lparmap_stubs"] - ;; Format.sprintf {| (executable @@ -14,7 +12,7 @@ let deadcode_cflags = common_cflags @ ["-cclib -lparmap_stubs"] (preprocess (pps (ppx_compare ppx_sexp_conv -no-check))) )) |} - (String.concat " " deadcode_cflags) + (String.concat " " common_cflags) (String.concat " " common_optflags) (String.concat " " common_libraries) |> Jbuild_plugin.V1.send diff --git a/infer/src/jbuild.common.in b/infer/src/jbuild.common.in index d325430db..f1579a19d 100644 --- a/infer/src/jbuild.common.in +++ b/infer/src/jbuild.common.in @@ -55,9 +55,6 @@ let common_optflags = match build_mode with Opt -> ["-O3"] | Default | Test -> [ let common_libraries = (if java then ["javalib"; "ptrees"; "sawja"] else []) @ [ "ANSITerminal" - ; "apron" - ; "apron.octMPQ" - ; "elina" ; "atdgen" ; "base" ; "base64" diff --git a/infer/src/jbuild.in b/infer/src/jbuild.in index b0adab22b..834a14050 100644 --- a/infer/src/jbuild.in +++ b/infer/src/jbuild.in @@ -38,8 +38,7 @@ let infer_cflags = ; "-open" ; "InferIR" ; "-open" - ; "InferBase" - ; "-cclib -lparmap_stubs" ] + ; "InferBase" ] (** The build stanzas to be passed to jbuilder *) diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index b1ae71592..89bc25e22 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -86,10 +86,6 @@ codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 3, CONDI codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [1, 1]] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_true_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_value_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] -codetoanalyze/c/bufferoverrun/relation.c, FP_array_access2_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [3, 3] Size: [1, 1]] -codetoanalyze/c/bufferoverrun/relation.c, FP_array_access3_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [3, 3] Size: [1, 1]] -codetoanalyze/c/bufferoverrun/relation.c, FP_array_access4_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [3, 3] Size: [1, 1]] -codetoanalyze/c/bufferoverrun/relation.c, FP_call_array_access_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: [-1, -1] Size: [1, 1] by call to `array_access_Ok()` ] codetoanalyze/c/bufferoverrun/sizeof.c, FN_static_stride_bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [0, 0]] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/relation.c b/infer/tests/codetoanalyze/c/bufferoverrun/relation.c deleted file mode 100644 index 0b3d5af36..000000000 --- a/infer/tests/codetoanalyze/c/bufferoverrun/relation.c +++ /dev/null @@ -1,43 +0,0 @@ -/* - * Copyright (c) 2018-present, Facebook, Inc. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - */ -void array_access_Ok(int x, int y) { - int a[1]; - if (x + y == 1) { - a[x + y - 1] = 0; - } -} - -void FP_call_array_access_Ok() { array_access_Ok(0, 0); } - -void FP_array_access2_Ok(int x, int y) { - int a[1]; - if (x + y == 1) { - if (x + y != 1) { - a[3] = 0; - } - } -} - -void FP_array_access3_Ok(int x, int* y) { - int a[1]; - *y = x + 1; - if (x + 1 == 1) { - if (*y != 1) { - a[3] = 0; - } - } -} - -void FP_array_access4_Ok(int x, int* y) { - int a[1]; - *y = x * 3 + 1; - if (x * 3 + 1 == 1) { - if (*y != 1) { - a[3] = 0; - } - } -} diff --git a/opam b/opam index d5819d6d8..355910ea2 100644 --- a/opam +++ b/opam @@ -27,18 +27,14 @@ remove: [ ocaml-version: [ >= "4.04.2" ] depends: [ "ANSITerminal" {>="0.7"} - "apron" "atdgen" {>="1.6.0"} "base64" "cmdliner" {>="1.0.0"} "core" "conf-autoconf" {build} - "conf-gmp" {build} - "conf-mpfr" {build} "conf-sqlite3" {build} "conf-zlib" {build} "ctypes" {>="0.9.2"} - "elina" "extlib-compat" "javalib" {>="2.3.4"} "jbuilder" {build & >="1.0+beta14"} diff --git a/opam.lock b/opam.lock index 7b538c00d..f60868baf 100644 --- a/opam.lock +++ b/opam.lock @@ -1,21 +1,16 @@ ANSITerminal = 0.8 -apron = 20160125 atd = 1.12.0 atdgen = 1.12.0 base = v0.11.0 base64 = 2.2.0 bin_prot = v0.11.0 biniou = 1.2.0 -camlidl = 1.05 camlp4 = 4.06+1 camlzip = 1.07 cmdliner = 1.0.2 conf-aclocal = 1.0.0 conf-autoconf = 0.1 -conf-gmp = 1 conf-m4 = 1 -conf-mpfr = 1 -conf-perl = 1 conf-pkg-config = 1.0 conf-sqlite3 = 1 conf-which = 1 @@ -27,7 +22,6 @@ cppo = 1.6.4 cppo_ocamlbuild = 1.6.0 ctypes = 0.14.0 easy-format = 1.3.1 -elina = 1.0 extlib-compat = 1.7.2 fieldslib = v0.11.0 integers = 0.2.2 @@ -35,7 +29,6 @@ jane-street-headers = v0.11.0 javalib = 2.3.4 jbuilder = 1.0+beta20 menhir = 20171222 -mlgmpidl = 1.2.6-1 mtime = 1.1.0 num = 1.1 ocaml-compiler-libs = v0.11.0