From 385b6fa914550e2494a43269e7493d7b4cac5fd6 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 1 May 2020 03:57:54 -0700 Subject: [PATCH] [pulse] revamp arithmetic, put everything in the path condition Summary: List of things happening in this unreviewable diff: - moved PulsePathCondition to PulseSledge - renamed --pulse-path-conditions to --pudge - PulsePathCondition now contains all the arithmetic of pulse (inferbo+concrete intervals+pudge). In particular, moved arithmetic attributes into PulsePathCondition.t. PulsePathCondition plays the role of PulseArithmetic (combining all domains). - added tests for a false positive involving free() - PulseArithmetic is now just a thin wrapper around PulsePathCondition to operate on states directly (instead of on path conditions). - The rest is mostly moving code into PulsePathCondition (eg, from PulseInterproc) and adjusting it. Reviewed By: jberdine Differential Revision: D21332073 fbshipit-source-id: 184c8e0a9 --- infer/man/man1/infer-full.txt | 5 + infer/src/base/Config.ml | 17 +- infer/src/base/Config.mli | 4 +- infer/src/pulse/Pudge.ml | 13 + ...{PulseDummyPathCondition.mli => Pudge.mli} | 2 +- ...thConditionModuleType.ml => Pudge_intf.ml} | 0 infer/src/pulse/Pulse.ml | 13 +- infer/src/pulse/PulseAbductiveDomain.ml | 6 - infer/src/pulse/PulseAbductiveDomain.mli | 7 - infer/src/pulse/PulseArithmetic.ml | 210 +------ infer/src/pulse/PulseArithmetic.mli | 21 +- infer/src/pulse/PulseAttribute.ml | 34 +- infer/src/pulse/PulseAttribute.mli | 7 - infer/src/pulse/PulseBaseAddressAttributes.ml | 10 - .../src/pulse/PulseBaseAddressAttributes.mli | 4 - infer/src/pulse/PulseBasicInterface.ml | 11 +- ...myPathCondition.ml => PulseDummySledge.ml} | 6 +- infer/src/pulse/PulseDummySledge.mli | 10 + infer/src/pulse/PulseExecutionDomain.ml | 2 +- infer/src/pulse/PulseInterproc.ml | 147 +---- infer/src/pulse/PulseOperations.mli | 2 +- infer/src/pulse/PulsePathCondition.ml | 514 ++++++++++++------ infer/src/pulse/PulsePathCondition.mli | 51 +- infer/src/pulse/PulseSledge.ml | 174 ++++++ infer/src/pulse/PulseSledge.mli | 10 + infer/tests/codetoanalyze/c/pulse/issues.exp | 1 + infer/tests/codetoanalyze/c/pulse/nullptr.c | 12 + .../tests/codetoanalyze/cpp/pulse/issues.exp | 2 +- 28 files changed, 723 insertions(+), 572 deletions(-) create mode 100644 infer/src/pulse/Pudge.ml rename infer/src/pulse/{PulseDummyPathCondition.mli => Pudge.mli} (83%) rename infer/src/pulse/{PulsePathConditionModuleType.ml => Pudge_intf.ml} (100%) rename infer/src/pulse/{PulseDummyPathCondition.ml => PulseDummySledge.ml} (82%) create mode 100644 infer/src/pulse/PulseDummySledge.mli create mode 100644 infer/src/pulse/PulseSledge.ml create mode 100644 infer/src/pulse/PulseSledge.mli diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index c0d7a6f3b..4358c1aa2 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1594,6 +1594,11 @@ INTERNAL OPTIONS --profiler-samples-reset Cancel the effect of --profiler-samples. + --pudge + Activates: Experimental flag to enable sledge arithmetic on path + conditions. This is intended for Pulse development only and will + be removed once the feature is stable. (Conversely: --no-pudge) + --pulse-intraprocedural-only Activates: Disable inter-procedural analysis in Pulse. Used for experimentations only. (Conversely: diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 30f9d7acb..ab0b64284 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1754,6 +1754,12 @@ and project_root = ~meta:"dir" "Specify the root directory of the project" +and pudge = + CLOpt.mk_bool ~long:"pudge" ~default:false + "Experimental flag to enable sledge arithmetic on path conditions. This is intended for Pulse \ + development only and will be removed once the feature is stable." + + and pulse_recency_limit = CLOpt.mk_int ~long:"pulse-recency-limit" ~default:32 "Maximum number of array elements and structure fields to keep track of for a given array \ @@ -1782,13 +1788,6 @@ and pulse_model_free_pattern = "Regex of methods that should be modelled as free in Pulse" -and pulse_path_conditions = - CLOpt.mk_bool ~long:"" ~deprecated:["-pulse-path-conditions"] - ~deprecated_no:["-no-pulse-path-conditions"] ~default:false - "Experimental flag to enable arithmetic on path conditions. This is intended for Pulse \ - development only and will be removed once the feature is stable." - - and pulse_widen_threshold = CLOpt.mk_int ~long:"pulse-widen-threshold" ~default:3 "Under-approximate after $(i,int) loop iterations" @@ -2855,6 +2854,8 @@ and progress_bar = and project_root = !project_root +and pudge = !pudge + and pulse_recency_limit = !pulse_recency_limit and pulse_intraprocedural_only = !pulse_intraprocedural_only @@ -2865,8 +2866,6 @@ and pulse_model_alloc_pattern = Option.map ~f:Str.regexp !pulse_model_alloc_patt and pulse_model_free_pattern = Option.map ~f:Str.regexp !pulse_model_free_pattern -and pulse_path_conditions = !pulse_path_conditions - and pulse_widen_threshold = !pulse_widen_threshold and pure_by_default = !pure_by_default diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 9a22e4d02..dbeacb476 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -443,6 +443,8 @@ val progress_bar : [`MultiLine | `Plain | `Quiet] val project_root : string +val pudge : bool + val pulse_recency_limit : int val pulse_intraprocedural_only : bool @@ -453,8 +455,6 @@ val pulse_model_alloc_pattern : Str.regexp option val pulse_model_free_pattern : Str.regexp option -val pulse_path_conditions : bool - val pulse_widen_threshold : int val pure_by_default : bool diff --git a/infer/src/pulse/Pudge.ml b/infer/src/pulse/Pudge.ml new file mode 100644 index 000000000..5e77c3f5d --- /dev/null +++ b/infer/src/pulse/Pudge.ml @@ -0,0 +1,13 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +module Pudge = ( val if Config.pudge then (module PulseSledge) else (module PulseDummySledge) + : Pudge_intf.S ) + +include Pudge diff --git a/infer/src/pulse/PulseDummyPathCondition.mli b/infer/src/pulse/Pudge.mli similarity index 83% rename from infer/src/pulse/PulseDummyPathCondition.mli rename to infer/src/pulse/Pudge.mli index 8e460e1ac..d61ffc8d3 100644 --- a/infer/src/pulse/PulseDummyPathCondition.mli +++ b/infer/src/pulse/Pudge.mli @@ -7,4 +7,4 @@ open! IStd -include PulsePathConditionModuleType.S +include Pudge_intf.S diff --git a/infer/src/pulse/PulsePathConditionModuleType.ml b/infer/src/pulse/Pudge_intf.ml similarity index 100% rename from infer/src/pulse/PulsePathConditionModuleType.ml rename to infer/src/pulse/Pudge_intf.ml diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 9e75138b4..160384011 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -22,7 +22,7 @@ let check_error_transform summary ~f = function | Ok astate -> f astate | Error (diagnostic, astate) -> - if PulseArithmetic.is_unsat astate then [] + if PulseArithmetic.is_unsat_expensive astate then [] else ( report summary diagnostic ; [ExecutionDomain.AbortProgram astate] ) @@ -179,12 +179,13 @@ module PulseTransferFunctions = struct check_error_continue summary result | Prune (condition, loc, _is_then_branch, _if_kind) -> PulseOperations.prune loc ~condition astate - |> check_error_transform summary ~f:(fun (exec_state, cond_satisfiable) -> - if cond_satisfiable then + |> check_error_transform summary ~f:(fun astate -> + if PulseArithmetic.is_unsat_cheap astate then + (* [condition] is known to be unsatisfiable: prune path *) + [] + else (* [condition] is true or unknown value: go into the branch *) - [Domain.ContinueProgram exec_state] - else (* [condition] is known to be unsatisfiable: prune path *) - [] ) + [Domain.ContinueProgram astate] ) | Call (ret, call_exp, actuals, loc, call_flags) -> dispatch_call tenv summary ret call_exp actuals loc call_flags get_formals astate |> check_error_transform summary ~f:(fun id -> id) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 667c84c3b..19747b751 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -217,12 +217,6 @@ module AddressAttributes = struct BaseAddressAttributes.get_closure_proc_name addr (astate.post :> base_domain).attrs - let get_citv addr astate = BaseAddressAttributes.get_citv addr (astate.post :> base_domain).attrs - - let get_bo_itv addr astate = - BaseAddressAttributes.get_bo_itv addr (astate.post :> base_domain).attrs - - let std_vector_reserve addr astate = map_post_attrs astate ~f:(BaseAddressAttributes.std_vector_reserve addr) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index f76ff7927..7030bd7c6 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -114,9 +114,6 @@ end (** attribute operations like {!BaseAddressAttributes} but that also take care of propagating facts to the precondition *) module AddressAttributes : sig - val abduce_attribute : AbstractValue.t -> Attribute.t -> t -> t - (** add the attribute to the pre, if meaningful (does not modify the post) *) - val abduce_and_add : AbstractValue.t -> Attributes.t -> t -> t (** add the attributes to both the current state and, if meaningful, the pre *) @@ -137,10 +134,6 @@ module AddressAttributes : sig val std_vector_reserve : AbstractValue.t -> t -> t - val get_citv : AbstractValue.t -> t -> CItv.t option - - val get_bo_itv : AbstractValue.t -> t -> Itv.ItvPure.t - val find_opt : AbstractValue.t -> t -> Attributes.t option end diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml index 91eb16fc8..136611d2d 100644 --- a/infer/src/pulse/PulseArithmetic.ml +++ b/infer/src/pulse/PulseArithmetic.ml @@ -8,214 +8,46 @@ open! IStd open PulseBasicInterface module AbductiveDomain = PulseAbductiveDomain -module AddressAttributes = AbductiveDomain.AddressAttributes -(** {2 Building arithmetic constraints} *) - -let and_eq_terms t1 t2 astate = - let phi = PathCondition.and_eq t1 t2 astate.AbductiveDomain.path_condition in - AbductiveDomain.set_path_condition phi astate - - -let and_term t astate = - let phi = PathCondition.and_term t astate.AbductiveDomain.path_condition in - AbductiveDomain.set_path_condition phi astate +let map_path_condition ~f astate = + AbductiveDomain.set_path_condition (f astate.AbductiveDomain.path_condition) astate let and_nonnegative v astate = - AddressAttributes.add_one v (BoItv Itv.ItvPure.nat) astate - |> AddressAttributes.add_one v (CItv CItv.zero_inf) - |> and_term PathCondition.Term.(le zero (of_absval v)) + map_path_condition astate ~f:(fun phi -> PathCondition.and_nonnegative v phi) let and_positive v astate = - AddressAttributes.add_one v (BoItv Itv.ItvPure.pos) astate - |> AddressAttributes.add_one v (CItv (CItv.ge_to IntLit.one)) - |> and_term PathCondition.Term.(lt zero (of_absval v)) + map_path_condition astate ~f:(fun phi -> PathCondition.and_positive v phi) let and_eq_int v i astate = - AddressAttributes.add_one v (BoItv (Itv.ItvPure.of_int_lit i)) astate - |> AddressAttributes.add_one v (CItv (CItv.equal_to i)) - |> and_eq_terms (PathCondition.Term.of_absval v) (PathCondition.Term.of_intlit i) - - -(** {2 Operations} *) + map_path_condition astate ~f:(fun phi -> PathCondition.and_eq_int v i phi) -type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t - -let eval_citv_operand binop_addr bop op_lhs op_rhs astate = - let citv_of_op op astate = - match op with - | LiteralOperand i -> - Some (CItv.equal_to i) - | AbstractValueOperand v -> - AddressAttributes.get_citv v astate - in - match - Option.both (citv_of_op op_lhs astate) (citv_of_op op_rhs astate) - |> Option.bind ~f:(fun (addr_lhs, addr_rhs) -> CItv.binop bop addr_lhs addr_rhs) - with - | None -> - astate - | Some binop_a -> - let astate = AddressAttributes.add_one binop_addr (CItv binop_a) astate in - astate - - -let eval_bo_itv_binop binop_addr bop op_lhs op_rhs astate = - let bo_itv_of_op op astate = - match op with - | LiteralOperand i -> - Itv.ItvPure.of_int_lit i - | AbstractValueOperand v -> - AddressAttributes.get_bo_itv v astate - in - let bo_itv = - Itv.ItvPure.arith_binop bop (bo_itv_of_op op_lhs astate) (bo_itv_of_op op_rhs astate) - in - AddressAttributes.add_one binop_addr (BoItv bo_itv) astate - - -let eval_path_condition_binop binop_addr binop op_lhs op_rhs astate = - let term_of_op = function - | LiteralOperand i -> - PathCondition.Term.of_intlit i - | AbstractValueOperand v -> - PathCondition.Term.of_absval v - in - and_eq_terms - (PathCondition.Term.of_absval binop_addr) - (PathCondition.Term.of_binop binop (term_of_op op_lhs) (term_of_op op_rhs)) - astate +type operand = PathCondition.operand = + | LiteralOperand of IntLit.t + | AbstractValueOperand of AbstractValue.t let eval_binop binop_addr binop op_lhs op_rhs astate = - eval_path_condition_binop binop_addr binop op_lhs op_rhs astate - |> eval_citv_operand binop_addr binop op_lhs op_rhs - |> eval_bo_itv_binop binop_addr binop op_lhs op_rhs - + map_path_condition astate ~f:(fun phi -> + PathCondition.eval_binop binop_addr binop op_lhs op_rhs phi ) -let eval_unop_citv unop_addr unop operand_addr astate = - match - AddressAttributes.get_citv operand_addr astate |> Option.bind ~f:(fun a -> CItv.unop unop a) - with - | None -> - astate - | Some unop_a -> - AddressAttributes.add_one unop_addr (CItv unop_a) astate +let eval_unop unop_addr unop addr astate = + map_path_condition astate ~f:(fun phi -> PathCondition.eval_unop unop_addr unop addr phi) -let eval_unop_bo_itv unop_addr unop operand_addr astate = - match Itv.ItvPure.arith_unop unop (AddressAttributes.get_bo_itv operand_addr astate) with - | None -> - astate - | Some itv -> - AddressAttributes.add_one unop_addr (BoItv itv) astate +let prune_binop ~negated bop lhs_op rhs_op astate = + let phi' = + PathCondition.prune_binop ~negated bop lhs_op rhs_op astate.AbductiveDomain.path_condition + in + AbductiveDomain.set_path_condition phi' astate -let eval_path_condition_unop unop_addr unop addr astate = - and_eq_terms - (PathCondition.Term.of_absval unop_addr) - PathCondition.Term.(of_unop unop (of_absval addr)) - astate +let is_known_zero astate v = PathCondition.is_known_zero astate.AbductiveDomain.path_condition v -let eval_unop unop_addr unop addr astate = - eval_path_condition_unop unop_addr unop addr astate - |> eval_unop_citv unop_addr unop addr - |> eval_unop_bo_itv unop_addr unop addr - - -let prune_with_bop ~negated v_opt arith bop arith' astate = - match - Option.both v_opt (if negated then Binop.negate bop else Some bop) - |> Option.map ~f:(fun (v, positive_bop) -> (v, Itv.ItvPure.prune_binop positive_bop arith arith') - ) - with - | None -> - (astate, true) - | Some (_, Bottom) -> - (astate, false) - | Some (v, NonBottom arith_pruned) -> - let attr_arith = Attribute.BoItv arith_pruned in - let astate = - AddressAttributes.abduce_attribute v attr_arith astate - |> AddressAttributes.add_one v attr_arith - in - (astate, true) - - -let eval_operand astate = function - | LiteralOperand i -> - (None, Some (CItv.equal_to i), Itv.ItvPure.of_int_lit i, PathCondition.Term.of_intlit i) - | AbstractValueOperand v -> - ( Some v - , AddressAttributes.get_citv v astate - , AddressAttributes.get_bo_itv v astate - , PathCondition.Term.of_absval v ) - - -let record_abduced addr_opt arith_opt astate = - match Option.both addr_opt arith_opt with - | None -> - astate - | Some (addr, arith) -> - let attribute = Attribute.CItv arith in - AddressAttributes.abduce_attribute addr attribute astate - |> AddressAttributes.add_one addr attribute - - -let bind_satisfiable ~satisfiable astate ~f = if satisfiable then f astate else (astate, false) +let is_unsat_cheap astate = PathCondition.is_unsat_cheap astate.AbductiveDomain.path_condition -let prune_binop ~negated bop lhs_op rhs_op astate = - let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, path_cond_lhs = eval_operand astate lhs_op in - let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, path_cond_rhs = eval_operand astate rhs_op in - let astate = - let path_condition = - let t_positive = PathCondition.Term.of_binop bop path_cond_lhs path_cond_rhs in - let t = if negated then PathCondition.Term.not_ t_positive else t_positive in - PathCondition.and_term t astate.AbductiveDomain.path_condition - in - AbductiveDomain.set_path_condition path_condition astate - in - match CItv.abduce_binop_is_true ~negated bop arith_lhs_opt arith_rhs_opt with - | Unsatisfiable -> - (astate, false) - | Satisfiable (abduced_lhs, abduced_rhs) -> - let astate = - record_abduced value_lhs_opt abduced_lhs astate |> record_abduced value_rhs_opt abduced_rhs - in - let satisfiable = - match Itv.ItvPure.arith_binop bop bo_itv_lhs bo_itv_rhs |> Itv.ItvPure.to_boolean with - | False -> - negated - | True -> - not negated - | Top -> - true - | Bottom -> - false - in - let astate, satisfiable = - bind_satisfiable ~satisfiable astate ~f:(fun astate -> - prune_with_bop ~negated value_lhs_opt bo_itv_lhs bop bo_itv_rhs astate ) - in - Option.value_map (Binop.symmetric bop) ~default:(astate, satisfiable) ~f:(fun bop' -> - bind_satisfiable ~satisfiable astate ~f:(fun astate -> - prune_with_bop ~negated value_rhs_opt bo_itv_rhs bop' bo_itv_lhs astate ) ) - - -(** {2 Queries} *) - -let is_known_zero astate v = - AddressAttributes.get_citv v astate |> Option.value_map ~default:false ~f:CItv.is_equal_to_zero - || (let phi = astate.AbductiveDomain.path_condition in - PathCondition.is_known_zero (PathCondition.Term.of_absval v) phi ) - || Itv.ItvPure.is_zero (AddressAttributes.get_bo_itv v astate) - - -let is_unsat astate = - (* note: contradictions are detected eagerly for all domains except path conditions, so just - evaluate that one *) - PathCondition.is_unsat astate.AbductiveDomain.path_condition +let is_unsat_expensive astate = + PathCondition.is_unsat_expensive astate.AbductiveDomain.path_condition diff --git a/infer/src/pulse/PulseArithmetic.mli b/infer/src/pulse/PulseArithmetic.mli index d2c05158a..138822587 100644 --- a/infer/src/pulse/PulseArithmetic.mli +++ b/infer/src/pulse/PulseArithmetic.mli @@ -9,20 +9,17 @@ open! IStd open PulseBasicInterface module AbductiveDomain = PulseAbductiveDomain -(** {2 Building arithmetic constraints} *) +(** Wrapper around {!PathCondition} that operates on {!AbductiveDomain.t}. *) val and_nonnegative : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t -(** [and_nonnegative v astate] is [astate ∧ v≥0] *) val and_positive : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t -(** [and_positive v astate] is [astate ∧ v>0] *) val and_eq_int : AbstractValue.t -> IntLit.t -> AbductiveDomain.t -> AbductiveDomain.t -(** [and_eq_int v i astate] is [astate ∧ v=i] *) -(** {2 Operations} *) - -type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t +type operand = PathCondition.operand = + | LiteralOperand of IntLit.t + | AbstractValueOperand of AbstractValue.t val eval_binop : AbstractValue.t -> Binop.t -> operand -> operand -> AbductiveDomain.t -> AbductiveDomain.t @@ -31,12 +28,10 @@ val eval_unop : AbstractValue.t -> Unop.t -> AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t val prune_binop : - negated:bool -> Binop.t -> operand -> operand -> AbductiveDomain.t -> AbductiveDomain.t * bool - -(** {2 Queries} *) + negated:bool -> Binop.t -> operand -> operand -> AbductiveDomain.t -> AbductiveDomain.t val is_known_zero : AbductiveDomain.t -> AbstractValue.t -> bool -(** [is_known_zero astate t] returns [true] if [astate |- t = 0], [false] if we don't know for sure *) -val is_unsat : AbductiveDomain.t -> bool -(** returns whether the state contains a contradiction *) +val is_unsat_cheap : AbductiveDomain.t -> bool + +val is_unsat_expensive : AbductiveDomain.t -> bool diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 54fa8c03d..4057573ea 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -6,7 +6,6 @@ *) open! IStd module F = Format -module CItv = PulseCItv module Invalidation = PulseInvalidation module Trace = PulseTrace module ValueHistory = PulseValueHistory @@ -29,8 +28,6 @@ module Attribute = struct | AddressOfCppTemporary of Var.t * ValueHistory.t | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t | Allocated of Procname.t * Trace.t - | CItv of CItv.t - | BoItv of Itv.ItvPure.t | Closure of Procname.t | Invalid of Invalidation.t * Trace.t | MustBeValid of Trace.t @@ -63,10 +60,6 @@ module Attribute = struct let std_vector_reserve_rank = Variants.to_rank StdVectorReserve - let citv_rank = Variants.to_rank (CItv (CItv.equal_to IntLit.zero)) - - let bo_itv_rank = Variants.to_rank (BoItv Itv.ItvPure.zero) - let allocated_rank = Variants.to_rank (Allocated (Procname.Linters_dummy_method, dummy_trace)) let pp f attribute = @@ -83,12 +76,8 @@ module Attribute = struct (Trace.pp ~pp_immediate:(pp_string_if_debug ("allocation with " ^ Procname.to_string procname))) trace - | BoItv bo_itv -> - F.fprintf f "BoItv (%a)" Itv.ItvPure.pp bo_itv | Closure pname -> Procname.pp f pname - | CItv phi -> - F.fprintf f "Arith %a" CItv.pp phi | Invalid (invalidation, trace) -> F.fprintf f "Invalid %a" (Trace.pp ~pp_immediate:(fun fmt -> Invalidation.pp fmt invalidation)) @@ -155,27 +144,13 @@ module Attributes = struct (procname, trace) ) - let get_citv attrs = - Set.find_rank attrs Attribute.citv_rank - |> Option.map ~f:(fun attr -> - let[@warning "-8"] (Attribute.CItv a) = attr in - a ) - - - let get_bo_itv attrs = - Set.find_rank attrs Attribute.bo_itv_rank - |> Option.map ~f:(fun attr -> - let[@warning "-8"] (Attribute.BoItv itv) = attr in - itv ) - - include Set end include Attribute let is_suitable_for_pre = function - | CItv _ | BoItv _ | MustBeValid _ -> + | MustBeValid _ -> true | AddressOfCppTemporary _ | AddressOfStackVariable _ @@ -196,10 +171,5 @@ let map_trace ~f = function MustBeValid (f trace) | WrittenTo trace -> WrittenTo (f trace) - | ( AddressOfCppTemporary _ - | AddressOfStackVariable _ - | BoItv _ - | CItv _ - | Closure _ - | StdVectorReserve ) as attr -> + | (AddressOfCppTemporary _ | AddressOfStackVariable _ | Closure _ | StdVectorReserve) as attr -> attr diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index 5daa502fb..319763dd8 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/infer/src/pulse/PulseAttribute.mli @@ -6,7 +6,6 @@ *) open! IStd module F = Format -module CItv = PulseCItv module Invalidation = PulseInvalidation module Trace = PulseTrace module ValueHistory = PulseValueHistory @@ -16,8 +15,6 @@ type t = | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t | Allocated of Procname.t * Trace.t (** the {!Procname.t} is the function causing the allocation, eg [malloc] *) - | CItv of CItv.t - | BoItv of Itv.ItvPure.t | Closure of Procname.t | Invalid of Invalidation.t * Trace.t | MustBeValid of Trace.t @@ -41,10 +38,6 @@ module Attributes : sig val get_allocation : t -> (Procname.t * Trace.t) option - val get_citv : t -> CItv.t option - - val get_bo_itv : t -> Itv.ItvPure.t option - val get_invalid : t -> (Invalidation.t * Trace.t) option val get_must_be_valid : t -> Trace.t option diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml index b5fc4e0cf..480c15dc1 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.ml +++ b/infer/src/pulse/PulseBaseAddressAttributes.ml @@ -90,16 +90,6 @@ let remove_allocation_attr address memory = let get_closure_proc_name = get_attribute Attributes.get_closure_proc_name -let get_citv = get_attribute Attributes.get_citv - -let get_bo_itv v memory = - match get_attribute Attributes.get_bo_itv v memory with - | None -> - Itv.ItvPure.of_pulse_value v - | Some itv -> - itv - - let get_must_be_valid = get_attribute Attributes.get_must_be_valid let std_vector_reserve address memory = add_one address Attribute.StdVectorReserve memory diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index 90fed44c6..f395b1d73 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/infer/src/pulse/PulseBaseAddressAttributes.mli @@ -32,10 +32,6 @@ val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location. val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option -val get_citv : AbstractValue.t -> t -> CItv.t option - -val get_bo_itv : AbstractValue.t -> t -> Itv.ItvPure.t - val get_must_be_valid : AbstractValue.t -> t -> Trace.t option val std_vector_reserve : AbstractValue.t -> t -> t diff --git a/infer/src/pulse/PulseBasicInterface.ml b/infer/src/pulse/PulseBasicInterface.ml index c93291a26..ea025227e 100644 --- a/infer/src/pulse/PulseBasicInterface.ml +++ b/infer/src/pulse/PulseBasicInterface.ml @@ -4,6 +4,7 @@ * This source code is licensed under the MIT license found in the * LICENSE file in the root directory of this source tree. *) + open! IStd (** Basic Pulse modules that are safe to use in any module *) @@ -12,14 +13,9 @@ module AbstractValue = PulseAbstractValue module Attribute = PulseAttribute module Attributes = PulseAttribute.Attributes module CallEvent = PulseCallEvent -module CItv = PulseCItv module Diagnostic = PulseDiagnostic module Invalidation = PulseInvalidation - -module PathCondition = ( val if Config.pulse_path_conditions then (module PulsePathCondition) - else (module PulseDummyPathCondition) : PulsePathConditionModuleType.S - ) - +module PathCondition = PulsePathCondition module SkippedCalls = PulseSkippedCalls module Trace = PulseTrace module ValueHistory = PulseValueHistory @@ -33,7 +29,6 @@ include struct [@@deprecated "use the short form AbstractValue instead"] module PulseAttribute = PulseAttribute [@@deprecated "use the short form Attribute instead"] module PulseCallEvent = PulseCallEvent [@@deprecated "use the short form CallEvent instead"] - module PulseCItv = PulseCItv [@@deprecated "use the short form CItv instead"] module PulseDiagnostic = PulseDiagnostic [@@deprecated "use the short form Diagnostic instead"] module PulseInvalidation = PulseInvalidation [@@deprecated "use the short form Invalidation instead"] @@ -41,6 +36,8 @@ include struct [@@deprecated "use the short form PathCondition instead"] module PulseSkippedCalls = PulseSkippedCalls [@@deprecated "use the short form SkippedCalls instead"] + module PulseSledge = PulseSledge [@@deprecated "use Pudge instead"] + module PulseDummySledge = PulseDummySledge [@@deprecated "use Pudge instead"] module PulseTrace = PulseTrace [@@deprecated "use the short form Trace instead"] module PulseValueHistory = PulseValueHistory [@@deprecated "use the short form ValueHistory instead"] diff --git a/infer/src/pulse/PulseDummyPathCondition.ml b/infer/src/pulse/PulseDummySledge.ml similarity index 82% rename from infer/src/pulse/PulseDummyPathCondition.ml rename to infer/src/pulse/PulseDummySledge.ml index ddd6b5f7c..170924242 100644 --- a/infer/src/pulse/PulseDummyPathCondition.ml +++ b/infer/src/pulse/PulseDummySledge.ml @@ -6,6 +6,7 @@ *) open! IStd +module F = Format module Var = struct type t = unit @@ -38,7 +39,10 @@ end (* same type as {!PulsePathCondition.t} to be nice to summary serialization *) type t = {eqs: Sledge.Equality.t lazy_t; non_eqs: Sledge.Term.t lazy_t} -let pp _ _ = () +(* still print to make sure the formula never changes in debug *) +let pp fmt {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} = + F.fprintf fmt "%a∧%a" Sledge.Equality.pp eqs Sledge.Term.pp non_eqs + let true_ = {eqs= Lazy.from_val Sledge.Equality.true_; non_eqs= Lazy.from_val Sledge.Term.true_} diff --git a/infer/src/pulse/PulseDummySledge.mli b/infer/src/pulse/PulseDummySledge.mli new file mode 100644 index 000000000..d61ffc8d3 --- /dev/null +++ b/infer/src/pulse/PulseDummySledge.mli @@ -0,0 +1,10 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +include Pudge_intf.S diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index 68ecbc44c..0ab123aa8 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -50,5 +50,5 @@ let map ~f exec_state = let of_posts pdesc posts = List.filter_map posts ~f:(fun exec_state -> let (AbortProgram astate | ContinueProgram astate | ExitProgram astate) = exec_state in - if PulseArithmetic.is_unsat astate then None + if PulseArithmetic.is_unsat_expensive astate then None else Some (map exec_state ~f:(AbductiveDomain.of_post pdesc)) ) diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 64f4118f0..61177401c 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -56,23 +56,9 @@ type contradiction = addresses [callee_addr] and [callee_addr'] that are distinct in the pre are aliased to a single address [caller_addr] in the caller's current state. Typically raised when calling [foo(z,z)] where the spec for [foo(x,y)] says that [x] and [y] are disjoint. *) - | CItv of - { addr_caller: AbstractValue.t - ; addr_callee: AbstractValue.t - ; arith_caller: CItv.t option - ; arith_callee: CItv.t option - ; call_state: call_state } - (** raised when the pre asserts arithmetic facts that are demonstrably false in the caller - state *) - | ArithmeticBo of - { addr_caller: AbstractValue.t - ; addr_callee: AbstractValue.t - ; arith_callee: Itv.ItvPure.t - ; call_state: call_state } - (** raised when the pre asserts arithmetic facts that are demonstrably false in the caller - state *) | FormalActualLength of {formals: Var.t list; actuals: ((AbstractValue.t * ValueHistory.t) * Typ.t) list} + | PathCondition let pp_contradiction fmt = function | Aliasing {addr_caller; addr_callee; addr_callee'; call_state} -> @@ -80,20 +66,11 @@ let pp_contradiction fmt = function "address %a in caller already bound to %a, not %a@\nnote: current call state was %a" AbstractValue.pp addr_caller AbstractValue.pp addr_callee' AbstractValue.pp addr_callee pp_call_state call_state - | CItv {addr_caller; addr_callee; arith_caller; arith_callee; call_state} -> - F.fprintf fmt - "caller addr %a%a but callee addr %a%a; %a=%a is unsatisfiable@\n\ - note: current call state was %a" AbstractValue.pp addr_caller (Pp.option CItv.pp) - arith_caller AbstractValue.pp addr_callee (Pp.option CItv.pp) arith_callee AbstractValue.pp - addr_caller AbstractValue.pp addr_callee pp_call_state call_state - | ArithmeticBo {addr_caller; addr_callee; arith_callee; call_state} -> - F.fprintf fmt - "callee addr %a%a is incompatible with caller addr %a's arithmetic constraints@\n\ - note: current call state was %a" AbstractValue.pp addr_callee Itv.ItvPure.pp arith_callee - AbstractValue.pp addr_caller pp_call_state call_state | FormalActualLength {formals; actuals} -> F.fprintf fmt "formals have length %d but actuals have length %d" (List.length formals) (List.length actuals) + | PathCondition -> + F.pp_print_string fmt "path condition evaluates to false" exception Contradiction of contradiction @@ -225,67 +202,10 @@ let materialize_pre_for_globals callee_proc_name call_location pre_post call_sta ~addr_pre ~addr_hist_caller call_state ) -let eval_sym_of_subst astate subst s bound_end = - let v = Symb.Symbol.get_pulse_value_exn s in - match AbstractValue.Map.find_opt v !subst with - | Some (v', _) -> - Itv.ItvPure.get_bound (AddressAttributes.get_bo_itv v' astate) bound_end - | None -> - let v' = AbstractValue.mk_fresh () in - subst := AbstractValue.Map.add v (v', []) !subst ; - Bounds.Bound.of_pulse_value v' - - -let subst_attribute call_state subst_ref astate ~addr_caller attr ~addr_callee = - match (attr : Attribute.t) with - | CItv arith_callee -> ( - let arith_caller_opt = AddressAttributes.get_citv addr_caller astate in - match CItv.abduce_binop_is_true ~negated:false Eq arith_caller_opt (Some arith_callee) with - | Unsatisfiable -> - raise - (Contradiction - (CItv - { addr_caller - ; addr_callee - ; arith_caller= arith_caller_opt - ; arith_callee= Some arith_callee - ; call_state })) - | Satisfiable (Some abduce_caller, _abduce_callee) -> - Attribute.CItv abduce_caller - | Satisfiable (None, _) -> - attr ) - | BoItv itv -> ( - match - Itv.ItvPure.subst itv (fun symb bound -> - AbstractDomain.Types.NonBottom (eval_sym_of_subst astate subst_ref symb bound) ) - with - | NonBottom itv' -> - Attribute.BoItv itv' - | Bottom -> - raise - (Contradiction (ArithmeticBo {addr_callee; addr_caller; arith_callee= itv; call_state})) ) - | AddressOfCppTemporary _ - | AddressOfStackVariable _ - | Allocated _ - | Closure _ - | Invalid _ - | MustBeValid _ - | StdVectorReserve - | WrittenTo _ -> - (* non-relational attributes *) - attr - - -let add_call_to_attributes proc_name call_location ~addr_callee ~addr_caller caller_history attrs - call_state = - let subst_ref = ref call_state.subst in - let attrs = - Attributes.map attrs ~f:(fun attr -> - subst_attribute call_state subst_ref call_state.astate ~addr_callee ~addr_caller attr - |> Attribute.map_trace ~f:(fun trace -> - add_call_to_trace proc_name call_location caller_history trace ) ) - in - (!subst_ref, attrs) +let add_call_to_attributes proc_name call_location caller_history attrs = + Attributes.map attrs ~f:(fun attr -> + Attribute.map_trace attr ~f:(fun trace -> + add_call_to_trace proc_name call_location caller_history trace ) ) let subst_find_or_new subst addr_callee ~default_hist_caller = @@ -298,40 +218,27 @@ let subst_find_or_new subst addr_callee ~default_hist_caller = let conjoin_callee_arith pre_post call_state = - L.d_printfln "applying callee path condition: %a[%a]" PathCondition.pp + L.d_printfln "applying callee path condition: (%a)[%a]" PathCondition.pp pre_post.AbductiveDomain.path_condition (AddressMap.pp ~pp_value:(fun fmt (addr, _) -> AbstractValue.pp fmt addr)) call_state.subst ; - let subst, callee_path_cond = - (* need to translate callee variables to make sense for the caller, thereby possibly extending - the current substitution *) - PathCondition.fold_map_variables pre_post.AbductiveDomain.path_condition ~init:call_state.subst - ~f:(fun subst v_callee_arith -> - let v_callee = PathCondition.Var.to_absval v_callee_arith in - let subst', (v_caller, _) = subst_find_or_new subst v_callee ~default_hist_caller:[] in - (subst', PathCondition.Var.of_absval v_caller) ) + let subst, path_condition = + PathCondition.and_callee call_state.subst call_state.astate.path_condition + ~callee:pre_post.AbductiveDomain.path_condition in - let path_condition = PathCondition.and_ call_state.astate.path_condition callee_path_cond in - let astate = AbductiveDomain.set_path_condition path_condition call_state.astate in - (* Don't trigger the computation of [path_condition] by asking for satisfiability here. Instead, - (un-)satisfiability is computed lazily when we discover issues. *) - {call_state with astate; subst} - - -(* shadowed to take config into account *) -let conjoin_callee_arith pre_post call_state = - if Config.pulse_path_conditions then conjoin_callee_arith pre_post call_state else call_state + if PathCondition.is_unsat_cheap path_condition then raise (Contradiction PathCondition) + else + let astate = AbductiveDomain.set_path_condition path_condition call_state.astate in + {call_state with astate; subst} let apply_arithmetic_constraints callee_proc_name call_location pre_post call_state = - let one_address_sat addr_callee callee_attrs (addr_caller, caller_history) call_state = - let subst, attrs_caller = - add_call_to_attributes callee_proc_name call_location ~addr_callee ~addr_caller caller_history - callee_attrs call_state + let one_address_sat callee_attrs (addr_caller, caller_history) call_state = + let attrs_caller = + add_call_to_attributes callee_proc_name call_location caller_history callee_attrs in let astate = AddressAttributes.abduce_and_add addr_caller attrs_caller call_state.astate in - if phys_equal subst call_state.subst && phys_equal astate call_state.astate then call_state - else {call_state with subst; astate} + if phys_equal astate call_state.astate then call_state else {call_state with astate} in let call_state = conjoin_callee_arith pre_post call_state in (* check all callee addresses that make sense for the caller, i.e. the domain of [call_state.subst] *) @@ -344,7 +251,7 @@ let apply_arithmetic_constraints callee_proc_name call_location pre_post call_st | None -> call_state | Some callee_attrs -> - one_address_sat addr_callee callee_attrs addr_hist_caller call_state ) + one_address_sat callee_attrs addr_hist_caller call_state ) call_state.subst call_state @@ -398,12 +305,11 @@ let record_post_cell callee_proc_name call_loc ~addr_callee ~edges_pre_opt ~cell_callee_post:(edges_callee_post, attrs_callee_post) ~addr_hist_caller:(addr_caller, hist_caller) call_state = let call_state = - let subst, attrs_post_caller = - add_call_to_attributes ~addr_callee ~addr_caller callee_proc_name call_loc hist_caller - attrs_callee_post call_state + let attrs_post_caller = + add_call_to_attributes callee_proc_name call_loc hist_caller attrs_callee_post in let astate = AddressAttributes.abduce_and_add addr_caller attrs_post_caller call_state.astate in - {call_state with subst; astate} + {call_state with astate} in let subst, translated_post_edges = BaseMemory.Edges.fold_map ~init:call_state.subst edges_callee_post @@ -549,12 +455,9 @@ let record_post_remaining_attributes callee_proc_name call_loc pre_post call_sta | None -> (* callee address has no meaning for the caller *) call_state | Some (addr_caller, history) -> - let subst, attrs' = - add_call_to_attributes callee_proc_name call_loc ~addr_callee ~addr_caller history - attrs call_state - in + let attrs' = add_call_to_attributes callee_proc_name call_loc history attrs in let astate = AddressAttributes.abduce_and_add addr_caller attrs' call_state.astate in - {call_state with subst; astate} ) + {call_state with astate} ) (pre_post.AbductiveDomain.post :> BaseDomain.t).attrs call_state diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 26a98f5fb..0b5754075 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -27,7 +27,7 @@ val eval : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) Return an error state if it traverses some known invalid address or if the end destination is known to be invalid. *) -val prune : Location.t -> condition:Exp.t -> t -> (t * bool) access_result +val prune : Location.t -> condition:Exp.t -> t -> t access_result val eval_deref : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) access_result (** Like [eval] but evaluates [*exp]. *) diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml index cce4fc5d2..d6f1e0e2d 100644 --- a/infer/src/pulse/PulsePathCondition.ml +++ b/infer/src/pulse/PulsePathCondition.ml @@ -9,166 +9,376 @@ open! IStd module F = Format module L = Logging module AbstractValue = PulseAbstractValue +module CItv = PulseCItv +module ValueHistory = PulseValueHistory -[@@@warning "+9"] +module BoItvs = struct + include PrettyPrintable.MakePPMonoMap (AbstractValue) (Itv.ItvPure) -module Var = struct - module Var = Sledge.Var - - let of_absval (v : AbstractValue.t) = Var.identified ~name:"v" ~id:(v :> int) - - let to_absval v = - assert (String.equal (Var.name v) "v") ; - Var.id v |> AbstractValue.of_id - - - include Var -end - -module Term = struct - module Term = Sledge.Term - - let of_intlit i = Term.integer (IntLit.to_big_int i) - - let of_absval v = Term.var (Var.of_absval v) - - let of_unop (unop : Unop.t) t = match unop with Neg -> Term.neg t | BNot | LNot -> Term.not_ t - - let of_binop (binop : Binop.t) t1 t2 = - let open Term in - match binop with - | PlusA _ | PlusPI -> - add t1 t2 - | MinusA _ | MinusPI | MinusPP -> - sub t1 t2 - | Mult _ -> - mul t1 t2 - | Div -> - div t1 t2 - | Mod -> - rem t1 t2 - | Shiftlt -> - shl t1 t2 - | Shiftrt -> - lshr t1 t2 - | Lt -> - lt t1 t2 - | Gt -> - lt t2 t1 - | Le -> - le t1 t2 - | Ge -> - le t2 t1 - | Eq -> - eq t1 t2 - | Ne -> - dq t1 t2 - | BAnd | LAnd -> - and_ t1 t2 - | BOr | LOr -> - or_ t1 t2 - | BXor -> - xor t1 t2 - - - include Term -end - -module Equality = struct - include Sledge.Equality - - let assert_no_new_vars api new_vars = - if not (Var.Set.is_empty new_vars) then - L.die InternalError "Huho, %s generated fresh new variables %a" api Var.Set.pp new_vars - - - let and_eq t1 t2 r = - let new_vars, r' = Sledge.Equality.and_eq Var.Set.empty t1 t2 r in - assert_no_new_vars "Equality.and_eq" new_vars ; - r' - - - let and_term t r = - let new_vars, r' = Sledge.Equality.and_term Var.Set.empty t r in - assert_no_new_vars "Equality.and_term" new_vars ; - r' - - - let and_ r1 r2 = - let new_vars, r' = Sledge.Equality.and_ Var.Set.empty r1 r2 in - assert_no_new_vars "Equality.and_" new_vars ; - r' - - - let apply_subst subst r = - let new_vars, r' = Sledge.Equality.apply_subst Var.Set.empty subst r in - assert_no_new_vars "Equality.apply_subst" new_vars ; - r' + let find_or_default v bo_itvs = + match find_opt v bo_itvs with Some bo_itv -> bo_itv | None -> Itv.ItvPure.of_pulse_value v end -(** We distinguish between what the equality relation of sledge can express and the "non-equalities" - terms that this relation ignores. We keep the latter around for completeness: we can still - substitute known equalities into these and sometimes get contradictions back. *) -type t = {eqs: Equality.t lazy_t; non_eqs: Term.t lazy_t} - -let pp fmt {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} = - F.fprintf fmt "%a∧%a" Equality.pp eqs Term.pp non_eqs - - -let true_ = {eqs= Lazy.from_val Equality.true_; non_eqs= Lazy.from_val Term.true_} - -let and_eq t1 t2 phi = {phi with eqs= lazy (Equality.and_eq t1 t2 (Lazy.force phi.eqs))} - -let and_term (t : Term.t) phi = - (* add the term to the relation *) - let eqs = lazy (Equality.and_term t (Lazy.force phi.eqs)) in - (* [t] normalizes to [true_] so [non_eqs] never changes, do this regardless for now *) - let non_eqs = lazy (Term.and_ (Lazy.force phi.non_eqs) (Equality.normalize (Lazy.force eqs) t)) in - {eqs; non_eqs} - - -let and_ phi1 phi2 = - { eqs= lazy (Equality.and_ (Lazy.force phi1.eqs) (Lazy.force phi2.eqs)) - ; non_eqs= lazy (Term.and_ (Lazy.force phi1.non_eqs) (Lazy.force phi2.non_eqs)) } - - -let is_known_zero t phi = Equality.entails_eq (Lazy.force phi.eqs) t Term.zero - -(* NOTE: not normalizing non_eqs here gives imprecise results but is cheaper *) -let is_unsat {eqs; non_eqs} = - Equality.is_false (Lazy.force eqs) || Term.is_false (Lazy.force non_eqs) - - -let fv {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} = - Term.Var.Set.union (Equality.fv eqs) (Term.fv non_eqs) +module CItvs = PrettyPrintable.MakePPMonoMap (AbstractValue) (CItv) + +(** A mash-up of several arithmetic domains. At the moment they are independent, i.e. we don't use + facts deduced by one domain to inform another. *) +type t = + { satisfiable: bool + (** If [true] then [pudge] could still be unsatisfiable (asking that question is expensive). + + If [false] then the other components of the record can be arbitrary. *) + ; bo_itvs: BoItvs.t + ; citvs: CItvs.t + ; pudge: Pudge.t } + +let pp fmt {satisfiable; bo_itvs; citvs; pudge} = + F.fprintf fmt "@[sat:%b,@;bo: @[%a@],@;citv: @[%a@],@;pudge: @[%a@]@]" satisfiable BoItvs.pp + bo_itvs CItvs.pp citvs Pudge.pp pudge + + +let true_ = {satisfiable= true; bo_itvs= BoItvs.empty; citvs= CItvs.empty; pudge= Pudge.true_} + +let false_ = {satisfiable= false; bo_itvs= BoItvs.empty; citvs= CItvs.empty; pudge= Pudge.true_} + +let and_nonnegative v ({satisfiable; bo_itvs; citvs; pudge} as phi) = + if not satisfiable then phi + else + { satisfiable + ; bo_itvs= BoItvs.add v Itv.ItvPure.nat bo_itvs + ; citvs= CItvs.add v CItv.zero_inf citvs + ; pudge= Pudge.and_term Pudge.Term.(le zero (of_absval v)) pudge } + + +let and_positive v ({satisfiable; bo_itvs; citvs; pudge} as phi) = + if not satisfiable then phi + else + { satisfiable + ; bo_itvs= BoItvs.add v Itv.ItvPure.pos bo_itvs + ; citvs= CItvs.add v (CItv.ge_to IntLit.one) citvs + ; pudge= Pudge.and_term Pudge.Term.(lt zero (of_absval v)) pudge } + + +let and_eq_int v i ({satisfiable; bo_itvs; citvs; pudge} as phi) = + if not satisfiable then phi + else + { satisfiable + ; bo_itvs= BoItvs.add v (Itv.ItvPure.of_int_lit i) bo_itvs + ; citvs= CItvs.add v (CItv.equal_to i) citvs + ; pudge= Pudge.and_eq (Pudge.Term.of_absval v) (Pudge.Term.of_intlit i) pudge } + + +let simplify ~keep {satisfiable; bo_itvs; citvs; pudge} = + if not satisfiable then false_ + else + let is_in_keep v _ = AbstractValue.Set.mem v keep in + { satisfiable + ; bo_itvs= BoItvs.filter is_in_keep bo_itvs + ; citvs= CItvs.filter is_in_keep citvs + ; pudge= Pudge.simplify ~keep pudge } + + +let subst_find_or_new subst addr_callee = + match AbstractValue.Map.find_opt addr_callee subst with + | None -> + let addr_hist_fresh = (AbstractValue.mk_fresh (), []) in + (AbstractValue.Map.add addr_callee addr_hist_fresh subst, fst addr_hist_fresh) + | Some addr_hist_caller -> + (subst, fst addr_hist_caller) + + +let eval_sym_of_subst bo_itvs subst s bound_end = + let v = Symb.Symbol.get_pulse_value_exn s in + match AbstractValue.Map.find_opt v !subst with + | Some (v', _) -> + Itv.ItvPure.get_bound (BoItvs.find_or_default v' bo_itvs) bound_end + | None -> + let v' = AbstractValue.mk_fresh () in + subst := AbstractValue.Map.add v (v', []) !subst ; + Bounds.Bound.of_pulse_value v' + + +exception Contradiction + +(* TODO: this doesn't actually do "and" (it doesn't even take the caller interval into account) *) +let and_bo_itv_callee bo_itvs subst_ref itv_callee = + match + Itv.ItvPure.subst itv_callee (fun symb bound -> + AbstractDomain.Types.NonBottom (eval_sym_of_subst bo_itvs subst_ref symb bound) ) + with + | NonBottom itv' -> + itv' + | Bottom -> + raise Contradiction + + +let and_bo_itvs_callee subst bo_itvs_caller bo_itvs_callee = + (* first translate callee keys into caller values *) + let subst, bo_itvs_callee_renamed = + BoItvs.fold + (fun v_callee bo_itv (subst, bo_itvs) -> + let subst, v_caller = subst_find_or_new subst v_callee in + (* TODO: it could be that the same value already had a binding; in that case we want to + "and" the intervals *) + let bo_itvs = BoItvs.add v_caller bo_itv bo_itvs in + (subst, bo_itvs) ) + bo_itvs_callee (subst, BoItvs.empty) + in + let subst_ref = ref subst in + let bo_itvs' = + BoItvs.merge + (fun _v_caller bo_itv bo_itv_callee -> + match (bo_itv, bo_itv_callee) with + | None, None -> + None + | Some _, None -> + bo_itv + | _, Some bo_itv_callee -> + Some (and_bo_itv_callee bo_itvs_caller subst_ref bo_itv_callee) ) + bo_itvs_caller bo_itvs_callee_renamed + in + (!subst_ref, bo_itvs') + + +let and_citv_callee citv_caller citv_callee = + match CItv.abduce_binop_is_true ~negated:false Eq (Some citv_caller) (Some citv_callee) with + | Unsatisfiable -> + raise Contradiction + | Satisfiable (Some abduce_caller, _abduce_callee) -> + abduce_caller + | Satisfiable (None, _) -> + citv_caller + + +let and_citvs_callee subst citvs_caller citvs_callee = + let subst, citvs_callee_renamed = + CItvs.fold + (fun v_callee citv (subst, citvs) -> + let subst, v_caller = subst_find_or_new subst v_callee in + (* TODO: it could be that the same value already had a binding if several variables from the + callee map to the same caller variable; in that case we want to "and" the intervals *) + let citvs = CItvs.add v_caller citv citvs in + (subst, citvs) ) + citvs_callee (subst, CItvs.empty) + in + let citvs' = + CItvs.union + (fun _v citv citv_callee -> Some (and_citv_callee citv citv_callee)) + citvs_caller citvs_callee_renamed + in + (subst, citvs') -let fold_map_variables phi ~init ~f = - let term_fold_map t ~init ~f = - Term.fold_map_rec_pre t ~init ~f:(fun acc t -> - Var.of_term t - |> Option.map ~f:(fun v -> - let acc', v' = f acc v in - (acc', Term.var v') ) ) +let and_pudge_callee subst pudge_caller pudge_callee = + (* need to translate callee variables to make sense for the caller, thereby possibly extending + the current substitution *) + let subst, pudge_callee_translated = + Pudge.fold_map_variables pudge_callee ~init:subst ~f:(fun subst v_callee_arith -> + let v_callee = Pudge.Var.to_absval v_callee_arith in + let subst', v_caller = subst_find_or_new subst v_callee in + (subst', Pudge.Var.of_absval v_caller) ) + in + (* Don't trigger the computation of [path_condition] by asking for satisfiability here. Instead, + pudge (un-)satisfiability is computed lazily when we discover issues. *) + (subst, Pudge.and_ pudge_caller pudge_callee_translated) + + +let and_callee subst phi ~callee:phi_callee = + if (not phi.satisfiable) || not phi_callee.satisfiable then (subst, false_) + else + match and_bo_itvs_callee subst phi.bo_itvs phi_callee.bo_itvs with + | exception Contradiction -> + L.d_printfln "contradiction found by inferbo intervals" ; + (subst, false_) + | subst, bo_itvs' -> ( + match and_citvs_callee subst phi.citvs phi_callee.citvs with + | exception Contradiction -> + L.d_printfln "contradiction found by concrete intervals" ; + (subst, false_) + | subst, citvs' -> + let subst, pudge' = and_pudge_callee subst phi.pudge phi_callee.pudge in + (subst, {satisfiable= true; bo_itvs= bo_itvs'; citvs= citvs'; pudge= pudge'}) ) + + +(** {2 Operations} *) + +type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t + +let eval_citv_binop binop_addr bop op_lhs op_rhs citvs = + let citv_of_op op citvs = + match op with + | LiteralOperand i -> + Some (CItv.equal_to i) + | AbstractValueOperand v -> + CItvs.find_opt v citvs + in + match + Option.both (citv_of_op op_lhs citvs) (citv_of_op op_rhs citvs) + |> Option.bind ~f:(fun (addr_lhs, addr_rhs) -> CItv.binop bop addr_lhs addr_rhs) + with + | None -> + citvs + | Some binop_a -> + CItvs.add binop_addr binop_a citvs + + +let eval_bo_itv_binop binop_addr bop op_lhs op_rhs bo_itvs = + let bo_itv_of_op op bo_itvs = + match op with + | LiteralOperand i -> + Itv.ItvPure.of_int_lit i + | AbstractValueOperand v -> + BoItvs.find_or_default v bo_itvs in - let acc, eqs' = - Equality.classes (Lazy.force phi.eqs) - |> Term.Map.fold ~init:(init, Equality.true_) ~f:(fun ~key:t ~data:equal_ts (acc, eqs') -> - let acc, t' = term_fold_map ~init:acc ~f t in - List.fold equal_ts ~init:(acc, eqs') ~f:(fun (acc, eqs') equal_t -> - let acc, t_mapped = term_fold_map ~init:acc ~f equal_t in - (acc, Equality.and_eq t' t_mapped eqs') ) ) + let bo_itv = + Itv.ItvPure.arith_binop bop (bo_itv_of_op op_lhs bo_itvs) (bo_itv_of_op op_rhs bo_itvs) in - let acc, non_eqs' = term_fold_map ~init:acc ~f (Lazy.force phi.non_eqs) in - (acc, {eqs= Lazy.from_val eqs'; non_eqs= Lazy.from_val non_eqs'}) + BoItvs.add binop_addr bo_itv bo_itvs -let simplify ~keep phi = - let all_vs = fv phi in - let keep_vs = - AbstractValue.Set.fold - (fun v keep_vs -> Term.Var.Set.add keep_vs (Var.of_absval v)) - keep Term.Var.Set.empty +let eval_path_condition_binop binop_addr binop op_lhs op_rhs pudge = + let term_of_op = function + | LiteralOperand i -> + Pudge.Term.of_intlit i + | AbstractValueOperand v -> + Pudge.Term.of_absval v in - let simpl_subst = Equality.solve_for_vars [keep_vs; all_vs] (Lazy.force phi.eqs) in - {phi with eqs= Lazy.from_val (Equality.apply_subst simpl_subst (Lazy.force phi.eqs))} + Pudge.and_eq (Pudge.Term.of_absval binop_addr) + (Pudge.Term.of_binop binop (term_of_op op_lhs) (term_of_op op_rhs)) + pudge + + +let eval_binop binop_addr binop op_lhs op_rhs ({satisfiable; bo_itvs; citvs; pudge} as phi) = + if not phi.satisfiable then phi + else + { satisfiable + ; bo_itvs= eval_bo_itv_binop binop_addr binop op_lhs op_rhs bo_itvs + ; citvs= eval_citv_binop binop_addr binop op_lhs op_rhs citvs + ; pudge= eval_path_condition_binop binop_addr binop op_lhs op_rhs pudge } + + +let eval_citv_unop unop_addr unop operand_addr citvs = + match CItvs.find_opt operand_addr citvs |> Option.bind ~f:(fun a -> CItv.unop unop a) with + | None -> + citvs + | Some unop_a -> + CItvs.add unop_addr unop_a citvs + + +let eval_bo_itv_unop unop_addr unop operand_addr bo_itvs = + let op_itv = BoItvs.find_or_default operand_addr bo_itvs in + match Itv.ItvPure.arith_unop unop op_itv with + | None -> + bo_itvs + | Some itv -> + BoItvs.add unop_addr itv bo_itvs + + +let eval_path_condition_unop unop_addr unop addr pudge = + Pudge.and_eq (Pudge.Term.of_absval unop_addr) Pudge.Term.(of_unop unop (of_absval addr)) pudge + + +let eval_unop unop_addr unop addr ({satisfiable; bo_itvs; citvs; pudge} as phi) = + if not phi.satisfiable then phi + else + { satisfiable + ; bo_itvs= eval_bo_itv_unop unop_addr unop addr bo_itvs + ; citvs= eval_citv_unop unop_addr unop addr citvs + ; pudge= eval_path_condition_unop unop_addr unop addr pudge } + + +let prune_bo_with_bop ~negated v_opt arith bop arith' phi = + match + Option.both v_opt (if negated then Binop.negate bop else Some bop) + |> Option.map ~f:(fun (v, positive_bop) -> (v, Itv.ItvPure.prune_binop positive_bop arith arith') + ) + with + | None -> + phi + | Some (_, Bottom) -> + {phi with satisfiable= false} + | Some (v, NonBottom arith_pruned) -> + {phi with bo_itvs= BoItvs.add v arith_pruned phi.bo_itvs} + + +let eval_operand phi = function + | LiteralOperand i -> + (None, Some (CItv.equal_to i), Itv.ItvPure.of_int_lit i, Pudge.Term.of_intlit i) + | AbstractValueOperand v -> + ( Some v + , CItvs.find_opt v phi.citvs + , BoItvs.find_or_default v phi.bo_itvs + , Pudge.Term.of_absval v ) + + +let record_citv_abduced addr_opt arith_opt citvs = + match Option.both addr_opt arith_opt with + | None -> + citvs + | Some (addr, arith) -> + CItvs.add addr arith citvs + + +let bind_satisfiable phi ~f = if phi.satisfiable then f phi else phi + +let prune_binop ~negated bop lhs_op rhs_op ({satisfiable; bo_itvs= _; citvs; pudge} as phi) = + if not satisfiable then phi + else + let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, path_cond_lhs = eval_operand phi lhs_op in + let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, path_cond_rhs = eval_operand phi rhs_op in + let phi = + let pudge = + let t_positive = Pudge.Term.of_binop bop path_cond_lhs path_cond_rhs in + let t = if negated then Pudge.Term.not_ t_positive else t_positive in + Pudge.and_term t pudge + in + {phi with pudge} + in + match CItv.abduce_binop_is_true ~negated bop arith_lhs_opt arith_rhs_opt with + | Unsatisfiable -> + L.d_printfln "contradiction detected by concrete intervals" ; + false_ + | Satisfiable (abduced_lhs, abduced_rhs) -> + let phi = + let citvs = + record_citv_abduced value_lhs_opt abduced_lhs citvs + |> record_citv_abduced value_rhs_opt abduced_rhs + in + {phi with citvs} + in + let satisfiable = + match Itv.ItvPure.arith_binop bop bo_itv_lhs bo_itv_rhs |> Itv.ItvPure.to_boolean with + | False -> + negated + | True -> + not negated + | Top -> + true + | Bottom -> + false + in + if not satisfiable then L.d_printfln "contradiction detected by inferbo intervals" ; + let phi = {phi with satisfiable} in + let phi = + bind_satisfiable phi ~f:(fun phi -> + prune_bo_with_bop ~negated value_lhs_opt bo_itv_lhs bop bo_itv_rhs phi ) + in + Option.value_map (Binop.symmetric bop) ~default:phi ~f:(fun bop' -> + bind_satisfiable phi ~f:(fun phi -> + prune_bo_with_bop ~negated value_rhs_opt bo_itv_rhs bop' bo_itv_lhs phi ) ) + + +(** {2 Queries} *) + +let is_known_zero phi v = + (* don't ask sledge because it might be too expensive *) + CItvs.find_opt v phi.citvs |> Option.value_map ~default:false ~f:CItv.is_equal_to_zero + || BoItvs.find_opt v phi.bo_itvs |> Option.value_map ~default:false ~f:Itv.ItvPure.is_zero + + +let is_unsat_cheap phi = not phi.satisfiable + +let is_unsat_expensive phi = + (* note: contradictions are detected eagerly for all sub-domains except pudge, so just + evaluate that one *) + is_unsat_cheap phi || Pudge.is_unsat phi.pudge diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli index 8e460e1ac..55556e818 100644 --- a/infer/src/pulse/PulsePathCondition.mli +++ b/infer/src/pulse/PulsePathCondition.mli @@ -6,5 +6,54 @@ *) open! IStd +module F = Format +module AbstractValue = PulseAbstractValue +module ValueHistory = PulseValueHistory -include PulsePathConditionModuleType.S +type t + +val true_ : t + +val pp : F.formatter -> t -> unit + +(** {2 Building arithmetic constraints} *) + +val and_nonnegative : AbstractValue.t -> t -> t +(** [and_nonnegative v phi] is [phi ∧ v≥0] *) + +val and_positive : AbstractValue.t -> t -> t +(** [and_positive v phi] is [phi ∧ v>0] *) + +val and_eq_int : AbstractValue.t -> IntLit.t -> t -> t +(** [and_eq_int v i phi] is [phi ∧ v=i] *) + +val simplify : keep:AbstractValue.Set.t -> t -> t +(** [simplify ~keep phi] attempts to get rid of as many variables in [fv phi] but not in [keep] as + possible *) + +val and_callee : + (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t + -> t + -> callee:t + -> (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t * t + +(** {2 Operations} *) + +type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t + +val eval_binop : AbstractValue.t -> Binop.t -> operand -> operand -> t -> t + +val eval_unop : AbstractValue.t -> Unop.t -> AbstractValue.t -> t -> t + +val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> t + +(** {2 Queries} *) + +val is_known_zero : t -> AbstractValue.t -> bool +(** [is_known_zero phi t] returns [true] if [phi |- t = 0], [false] if we don't know for sure *) + +val is_unsat_cheap : t -> bool +(** whether the state contains a contradiction, call this as often as you want *) + +val is_unsat_expensive : t -> bool +(** whether the state contains a contradiction, only call this when you absolutely have to *) diff --git a/infer/src/pulse/PulseSledge.ml b/infer/src/pulse/PulseSledge.ml new file mode 100644 index 000000000..cce4fc5d2 --- /dev/null +++ b/infer/src/pulse/PulseSledge.ml @@ -0,0 +1,174 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +module F = Format +module L = Logging +module AbstractValue = PulseAbstractValue + +[@@@warning "+9"] + +module Var = struct + module Var = Sledge.Var + + let of_absval (v : AbstractValue.t) = Var.identified ~name:"v" ~id:(v :> int) + + let to_absval v = + assert (String.equal (Var.name v) "v") ; + Var.id v |> AbstractValue.of_id + + + include Var +end + +module Term = struct + module Term = Sledge.Term + + let of_intlit i = Term.integer (IntLit.to_big_int i) + + let of_absval v = Term.var (Var.of_absval v) + + let of_unop (unop : Unop.t) t = match unop with Neg -> Term.neg t | BNot | LNot -> Term.not_ t + + let of_binop (binop : Binop.t) t1 t2 = + let open Term in + match binop with + | PlusA _ | PlusPI -> + add t1 t2 + | MinusA _ | MinusPI | MinusPP -> + sub t1 t2 + | Mult _ -> + mul t1 t2 + | Div -> + div t1 t2 + | Mod -> + rem t1 t2 + | Shiftlt -> + shl t1 t2 + | Shiftrt -> + lshr t1 t2 + | Lt -> + lt t1 t2 + | Gt -> + lt t2 t1 + | Le -> + le t1 t2 + | Ge -> + le t2 t1 + | Eq -> + eq t1 t2 + | Ne -> + dq t1 t2 + | BAnd | LAnd -> + and_ t1 t2 + | BOr | LOr -> + or_ t1 t2 + | BXor -> + xor t1 t2 + + + include Term +end + +module Equality = struct + include Sledge.Equality + + let assert_no_new_vars api new_vars = + if not (Var.Set.is_empty new_vars) then + L.die InternalError "Huho, %s generated fresh new variables %a" api Var.Set.pp new_vars + + + let and_eq t1 t2 r = + let new_vars, r' = Sledge.Equality.and_eq Var.Set.empty t1 t2 r in + assert_no_new_vars "Equality.and_eq" new_vars ; + r' + + + let and_term t r = + let new_vars, r' = Sledge.Equality.and_term Var.Set.empty t r in + assert_no_new_vars "Equality.and_term" new_vars ; + r' + + + let and_ r1 r2 = + let new_vars, r' = Sledge.Equality.and_ Var.Set.empty r1 r2 in + assert_no_new_vars "Equality.and_" new_vars ; + r' + + + let apply_subst subst r = + let new_vars, r' = Sledge.Equality.apply_subst Var.Set.empty subst r in + assert_no_new_vars "Equality.apply_subst" new_vars ; + r' +end + +(** We distinguish between what the equality relation of sledge can express and the "non-equalities" + terms that this relation ignores. We keep the latter around for completeness: we can still + substitute known equalities into these and sometimes get contradictions back. *) +type t = {eqs: Equality.t lazy_t; non_eqs: Term.t lazy_t} + +let pp fmt {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} = + F.fprintf fmt "%a∧%a" Equality.pp eqs Term.pp non_eqs + + +let true_ = {eqs= Lazy.from_val Equality.true_; non_eqs= Lazy.from_val Term.true_} + +let and_eq t1 t2 phi = {phi with eqs= lazy (Equality.and_eq t1 t2 (Lazy.force phi.eqs))} + +let and_term (t : Term.t) phi = + (* add the term to the relation *) + let eqs = lazy (Equality.and_term t (Lazy.force phi.eqs)) in + (* [t] normalizes to [true_] so [non_eqs] never changes, do this regardless for now *) + let non_eqs = lazy (Term.and_ (Lazy.force phi.non_eqs) (Equality.normalize (Lazy.force eqs) t)) in + {eqs; non_eqs} + + +let and_ phi1 phi2 = + { eqs= lazy (Equality.and_ (Lazy.force phi1.eqs) (Lazy.force phi2.eqs)) + ; non_eqs= lazy (Term.and_ (Lazy.force phi1.non_eqs) (Lazy.force phi2.non_eqs)) } + + +let is_known_zero t phi = Equality.entails_eq (Lazy.force phi.eqs) t Term.zero + +(* NOTE: not normalizing non_eqs here gives imprecise results but is cheaper *) +let is_unsat {eqs; non_eqs} = + Equality.is_false (Lazy.force eqs) || Term.is_false (Lazy.force non_eqs) + + +let fv {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} = + Term.Var.Set.union (Equality.fv eqs) (Term.fv non_eqs) + + +let fold_map_variables phi ~init ~f = + let term_fold_map t ~init ~f = + Term.fold_map_rec_pre t ~init ~f:(fun acc t -> + Var.of_term t + |> Option.map ~f:(fun v -> + let acc', v' = f acc v in + (acc', Term.var v') ) ) + in + let acc, eqs' = + Equality.classes (Lazy.force phi.eqs) + |> Term.Map.fold ~init:(init, Equality.true_) ~f:(fun ~key:t ~data:equal_ts (acc, eqs') -> + let acc, t' = term_fold_map ~init:acc ~f t in + List.fold equal_ts ~init:(acc, eqs') ~f:(fun (acc, eqs') equal_t -> + let acc, t_mapped = term_fold_map ~init:acc ~f equal_t in + (acc, Equality.and_eq t' t_mapped eqs') ) ) + in + let acc, non_eqs' = term_fold_map ~init:acc ~f (Lazy.force phi.non_eqs) in + (acc, {eqs= Lazy.from_val eqs'; non_eqs= Lazy.from_val non_eqs'}) + + +let simplify ~keep phi = + let all_vs = fv phi in + let keep_vs = + AbstractValue.Set.fold + (fun v keep_vs -> Term.Var.Set.add keep_vs (Var.of_absval v)) + keep Term.Var.Set.empty + in + let simpl_subst = Equality.solve_for_vars [keep_vs; all_vs] (Lazy.force phi.eqs) in + {phi with eqs= Lazy.from_val (Equality.apply_subst simpl_subst (Lazy.force phi.eqs))} diff --git a/infer/src/pulse/PulseSledge.mli b/infer/src/pulse/PulseSledge.mli new file mode 100644 index 000000000..d61ffc8d3 --- /dev/null +++ b/infer/src/pulse/PulseSledge.mli @@ -0,0 +1,10 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +include Pudge_intf.S diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index 50b6c54ac..5eef917a5 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -1,5 +1,6 @@ codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad, 0, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `create_p` here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] +codetoanalyze/c/pulse/nullptr.c, FP_interproc_free_ok, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,use-after-lifetime part of the trace starts here,allocated by call to `malloc` (modelled),assigned,when calling `wrap_free` here,parameter `p` of wrap_free,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, malloc_no_check_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,use-after-lifetime part of the trace starts here,allocated by call to `malloc` (modelled),assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/c/pulse/nullptr.c b/infer/tests/codetoanalyze/c/pulse/nullptr.c index 8276b8813..5ec9011f9 100644 --- a/infer/tests/codetoanalyze/c/pulse/nullptr.c +++ b/infer/tests/codetoanalyze/c/pulse/nullptr.c @@ -65,3 +65,15 @@ void nullptr_deref_old_bad_FP(int* x) { x, x, x, x, x, x, x, x, x, x, x, x, x, x}; int p = *vec[0]; } + +void malloc_free_ok() { + int* p = (int*)malloc(sizeof(int)); + free(p); +} + +void wrap_free(void* p) { free(p); } + +void FP_interproc_free_ok() { + int* p = (int*)malloc(sizeof(int)); + wrap_free(p); +} diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index b98cfa6dd..fa7783888 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,4 +1,4 @@ -codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,when calling `setLanguage` here,variable `C++ temporary` declared here,passed as argument to `Range::Range`,parameter `str` of Range::Range,return from call to `Range::Range`,passed as argument to `std::basic_string::~basic_string()` (modelled),return from call to `std::basic_string::~basic_string()` (modelled),was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `s` declared here,passed as argument to `setLanguage`,variable `C++ temporary` declared here,passed as argument to `Range::Range`,parameter `str` of Range::Range,passed as argument to `std::basic_string::data()` (modelled),return from call to `std::basic_string::data()` (modelled),assigned,return from call to `Range::Range`,return from call to `setLanguage`,when calling `Range::operator[]` here,parameter `this` of Range::operator[],invalid access occurs here] +codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `setLanguage` here,variable `C++ temporary` declared here,passed as argument to `Range::Range`,parameter `str` of Range::Range,return from call to `Range::Range`,passed as argument to `std::basic_string::~basic_string()` (modelled),return from call to `std::basic_string::~basic_string()` (modelled),was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `setLanguage`,variable `C++ temporary` declared here,passed as argument to `Range::Range`,parameter `str` of Range::Range,passed as argument to `std::basic_string::data()` (modelled),return from call to `std::basic_string::data()` (modelled),assigned,return from call to `Range::Range`,return from call to `setLanguage`,when calling `Range::operator[]` here,parameter `this` of Range::operator[],invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,invalid access occurs here]