diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 9387a843f..6d6b87a3b 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -168,9 +168,10 @@ module PulseTransferFunctions = struct Ok astate in [check_error summary result] - | Prune (condition, loc, _is_then_branch, _if_kind) -> + | Prune (condition, loc, is_then_branch, if_kind) -> let post, cond_satisfiable = - PulseOperations.assert_is_true loc ~condition astate |> check_error summary + PulseOperations.prune ~is_then_branch if_kind loc ~condition astate + |> check_error summary in if cond_satisfiable then (* [condition] is true or unknown value: go into the branch *) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index bfb9f21af..bd11de4e6 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -440,25 +440,41 @@ module PrePost = struct (* {3 reading the pre from the current state} *) - let solve_arithmetic_constraints ~addr_pre ~attrs_pre ~addr_hist_caller call_state = + let add_call_to_trace proc_name call_location caller_history in_call = + Trace.ViaCall {f= Call proc_name; location= call_location; history= caller_history; in_call} + + + let solve_arithmetic_constraints callee_proc_name call_location ~addr_pre ~attrs_pre + ~addr_hist_caller call_state = match Attributes.get_arithmetic attrs_pre with | None -> call_state - | Some _ as arith_callee -> ( - let addr_caller = fst addr_hist_caller in + | Some (arith_callee, arith_callee_hist) -> ( + let addr_caller, hist_caller = addr_hist_caller in let astate = call_state.astate in - let arith_caller = Memory.get_arithmetic addr_caller astate in + let arith_caller_opt = Memory.get_arithmetic addr_caller astate |> Option.map ~f:fst in (* TODO: we don't use [abduced_callee] but we could probably use it to refine the attributes for that address in the post since abstract values are immutable *) - match Arithmetic.abduce_binop_is_true ~negated:false Eq arith_caller arith_callee with + match + Arithmetic.abduce_binop_is_true ~negated:false Eq arith_caller_opt (Some arith_callee) + with | Unsatisfiable -> raise (CannotApplyPre - (Arithmetic {addr_caller; addr_callee= addr_pre; arith_caller; arith_callee})) + (Arithmetic + { addr_caller + ; addr_callee= addr_pre + ; arith_caller= arith_caller_opt + ; arith_callee= Some arith_callee })) | Satisfiable (abduce_caller, _abduce_callee) -> let new_astate = Option.fold abduce_caller ~init:astate ~f:(fun astate abduce_caller -> - let attribute = Attribute.Arithmetic abduce_caller in + let attribute = + Attribute.Arithmetic + ( abduce_caller + , add_call_to_trace callee_proc_name call_location hist_caller + arith_callee_hist ) + in Memory.abduce_attribute addr_caller attribute astate |> Memory.add_attribute addr_caller attribute ) in @@ -479,7 +495,8 @@ module PrePost = struct Ok call_state | Some (edges_pre, attrs_pre) -> let call_state = - solve_arithmetic_constraints ~addr_pre ~attrs_pre ~addr_hist_caller call_state + solve_arithmetic_constraints callee_proc_name call_location ~addr_pre ~attrs_pre + ~addr_hist_caller call_state in Container.fold_result ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) @@ -610,14 +627,13 @@ module PrePost = struct let add_call_to_attr proc_name call_location caller_history attr = match (attr : Attribute.t) with - | Invalid (invalidation, in_call) -> + | Invalid (invalidation, trace) -> Attribute.Invalid - ( invalidation - , ViaCall {f= Call proc_name; location= call_location; history= caller_history; in_call} - ) + (invalidation, add_call_to_trace proc_name call_location caller_history trace) + | Arithmetic (arith, trace) -> + Attribute.Arithmetic (arith, add_call_to_trace proc_name call_location caller_history trace) | AddressOfCppTemporary (_, _) | AddressOfStackVariable (_, _, _) - | Arithmetic _ | Closure _ | MustBeValid _ | StdVectorReserve diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index b6087437d..36a576646 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -80,7 +80,7 @@ module Memory : sig (** [eval_edge (addr,hist) access astate] follows the edge [addr --access--> .] in memory and returns what it points to or creates a fresh value if that edge didn't exist. *) - val get_arithmetic : AbstractValue.t -> t -> Arithmetic.t option + val get_arithmetic : AbstractValue.t -> t -> (Arithmetic.t * Trace.t) option end val is_local : Var.t -> t -> bool diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 81daeba2f..c26594b9c 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -29,7 +29,7 @@ module Attribute = struct type t = | AddressOfCppTemporary of Var.t * ValueHistory.t | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t - | Arithmetic of Arithmetic.t + | Arithmetic of Arithmetic.t * Trace.t | Closure of Typ.Procname.t | Invalid of Invalidation.t * Trace.t | MustBeValid of Trace.t @@ -60,7 +60,7 @@ module Attribute = struct let std_vector_reserve_rank = Variants.to_rank StdVectorReserve - let const_rank = Variants.to_rank (Arithmetic (Arithmetic.equal_to IntLit.zero)) + let const_rank = Variants.to_rank (Arithmetic (Arithmetic.equal_to IntLit.zero, dummy_trace)) let pp f attribute = let pp_string_if_debug string fmt = @@ -73,8 +73,8 @@ module Attribute = struct F.fprintf f "s&%a (%a) at %a" Var.pp var ValueHistory.pp history Location.pp location | Closure pname -> Typ.Procname.pp f pname - | Arithmetic phi -> - Arithmetic.pp f phi + | Arithmetic (phi, trace) -> + F.fprintf f "Arith %a" (Trace.pp ~pp_immediate:(fun fmt -> Arithmetic.pp fmt phi)) trace | Invalid (invalidation, trace) -> F.fprintf f "Invalid %a" (Trace.pp ~pp_immediate:(fun fmt -> Invalidation.pp fmt invalidation)) @@ -137,8 +137,8 @@ module Attributes = struct let get_arithmetic attrs = Set.find_rank attrs Attribute.const_rank |> Option.map ~f:(fun attr -> - let[@warning "-8"] (Attribute.Arithmetic a) = attr in - a ) + let[@warning "-8"] (Attribute.Arithmetic (a, trace)) = attr in + (a, trace) ) include Set diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index bd395f0fd..5a41a9d9f 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/infer/src/pulse/PulseAttribute.mli @@ -14,7 +14,7 @@ module ValueHistory = PulseValueHistory type t = | AddressOfCppTemporary of Var.t * ValueHistory.t | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t - | Arithmetic of Arithmetic.t + | Arithmetic of Arithmetic.t * Trace.t | Closure of Typ.Procname.t | Invalid of Invalidation.t * Trace.t | MustBeValid of Trace.t @@ -31,7 +31,7 @@ module Attributes : sig val get_closure_proc_name : t -> Typ.Procname.t option - val get_arithmetic : t -> Arithmetic.t option + val get_arithmetic : t -> (Arithmetic.t * Trace.t) option val get_invalid : t -> (Invalidation.t * Trace.t) option diff --git a/infer/src/pulse/PulseBaseMemory.mli b/infer/src/pulse/PulseBaseMemory.mli index 03a7e3c21..902b8bfdb 100644 --- a/infer/src/pulse/PulseBaseMemory.mli +++ b/infer/src/pulse/PulseBaseMemory.mli @@ -60,7 +60,7 @@ val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t * Trace.t) resul val get_closure_proc_name : AbstractValue.t -> t -> Typ.Procname.t option -val get_arithmetic : AbstractValue.t -> t -> Arithmetic.t option +val get_arithmetic : AbstractValue.t -> t -> (Arithmetic.t * Trace.t) option val get_must_be_valid : AbstractValue.t -> t -> Trace.t option diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index c711b02be..f2c9da9ef 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -134,7 +134,11 @@ let eval location exp0 astate = | Const (Cint i) -> (* TODO: make identical const the same address *) let addr = AbstractValue.mk_fresh () in - let astate = Memory.add_attribute addr (Arithmetic (Arithmetic.equal_to i)) astate in + let astate = + Memory.add_attribute addr + (Arithmetic (Arithmetic.equal_to i, Immediate {location; history= []})) + astate + in Ok (astate, (addr, [])) | Const _ | Sizeof _ | UnOp _ | BinOp _ | Exn _ -> Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) [])) @@ -145,7 +149,12 @@ let eval location exp0 astate = let eval_arith location exp astate = match (exp : Exp.t) with | Const (Cint i) -> - Ok (astate, None, Some (Arithmetic.equal_to i)) + Ok + ( astate + , None + , Some + ( Arithmetic.equal_to i + , Trace.Immediate {location; history= [ValueHistory.Assignment location]} ) ) | exp -> ( eval location exp astate >>| fun (astate, (addr, _)) -> @@ -156,36 +165,51 @@ let eval_arith location exp astate = (astate, Some addr, None) ) -let record_abduced addr_opt arith_opt astate = +let record_abduced ~is_then_branch if_kind location addr_opt orig_arith_hist_opt arith_opt astate = match Option.both addr_opt arith_opt with | None -> astate | Some (addr, arith) -> - let attribute = Attribute.Arithmetic arith in + let event = ValueHistory.Conditional {is_then_branch; if_kind; location} in + let trace = + match orig_arith_hist_opt with + | None -> + Trace.Immediate {location; history= [event]} + | Some (_, trace) -> + Trace.add_event event trace + in + let attribute = Attribute.Arithmetic (arith, trace) in Memory.abduce_attribute addr attribute astate |> Memory.add_attribute addr attribute -let rec eval_cond ~negated location exp astate = - match (exp : Exp.t) with - | BinOp (bop, e1, e2) -> ( - eval_arith location e1 astate - >>= fun (astate, addr1, eval1) -> - eval_arith location e2 astate - >>| fun (astate, addr2, eval2) -> - match Arithmetic.abduce_binop_is_true ~negated bop eval1 eval2 with - | Unsatisfiable -> - (astate, false) - | Satisfiable (abduced1, abduced2) -> - let astate = record_abduced addr1 abduced1 astate |> record_abduced addr2 abduced2 in - (astate, true) ) - | UnOp (LNot, exp', _) -> - eval_cond ~negated:(not negated) location exp' astate - | exp -> - let zero = Exp.Const (Cint IntLit.zero) in - eval_cond ~negated location (Exp.BinOp (Ne, exp, zero)) astate - - -let assert_is_true location ~condition astate = eval_cond ~negated:false location condition astate +let prune ~is_then_branch if_kind location ~condition astate = + let rec prune_aux ~negated exp astate = + match (exp : Exp.t) with + | BinOp (bop, e1, e2) -> ( + eval_arith location e1 astate + >>= fun (astate, addr1, eval1) -> + eval_arith location e2 astate + >>| fun (astate, addr2, eval2) -> + match + Arithmetic.abduce_binop_is_true ~negated bop (Option.map ~f:fst eval1) + (Option.map ~f:fst eval2) + with + | Unsatisfiable -> + (astate, false) + | Satisfiable (abduced1, abduced2) -> + let astate = + record_abduced ~is_then_branch if_kind location addr1 eval1 abduced1 astate + |> record_abduced ~is_then_branch if_kind location addr2 eval2 abduced2 + in + (astate, true) ) + | UnOp (LNot, exp', _) -> + prune_aux ~negated:(not negated) exp' astate + | exp -> + let zero = Exp.Const (Cint IntLit.zero) in + prune_aux ~negated (Exp.BinOp (Ne, exp, zero)) astate + in + prune_aux ~negated:false condition astate + let eval_deref location exp astate = eval location exp astate diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 223e0a5df..7d6c1afe1 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -25,7 +25,13 @@ 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 assert_is_true : Location.t -> condition:Exp.t -> t -> (t * bool) access_result +val prune : + is_then_branch:bool + -> Sil.if_kind + -> Location.t + -> condition:Exp.t + -> t + -> (t * bool) 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/PulseTrace.ml b/infer/src/pulse/PulseTrace.ml index c603cca57..d82af5f3c 100644 --- a/infer/src/pulse/PulseTrace.ml +++ b/infer/src/pulse/PulseTrace.ml @@ -37,6 +37,13 @@ let rec pp ~pp_immediate fmt trace = in_call +let add_event event = function + | Immediate {location; history} -> + Immediate {location; history= event :: history} + | ViaCall {f; in_call; location; history} -> + ViaCall {f; in_call; location; history= event :: history} + + let rec add_to_errlog ~nesting ~pp_immediate trace errlog = match trace with | Immediate {location; history} -> diff --git a/infer/src/pulse/PulseTrace.mli b/infer/src/pulse/PulseTrace.mli index 414fff4d0..e12bd0d80 100644 --- a/infer/src/pulse/PulseTrace.mli +++ b/infer/src/pulse/PulseTrace.mli @@ -27,6 +27,8 @@ val get_outer_location : t -> Location.t val get_start_location : t -> Location.t (** initial step in the history if not empty, or else same as {!get_outer_location} *) +val add_event : ValueHistory.event -> t -> t + val add_to_errlog : nesting:int -> pp_immediate:(F.formatter -> unit) diff --git a/infer/src/pulse/PulseValueHistory.ml b/infer/src/pulse/PulseValueHistory.ml index 9af63bdb2..5af5e223e 100644 --- a/infer/src/pulse/PulseValueHistory.ml +++ b/infer/src/pulse/PulseValueHistory.ml @@ -12,6 +12,7 @@ type event = | Assignment of Location.t | Call of {f: CallEvent.t; location: Location.t; in_call: t} | Capture of {captured_as: Pvar.t; location: Location.t} + | Conditional of {is_then_branch: bool; if_kind: Sil.if_kind; location: Location.t} | CppTemporaryCreated of Location.t | FormalDeclared of Pvar.t * Location.t | VariableAccessed of Pvar.t * Location.t @@ -31,6 +32,9 @@ let pp_event_no_location fmt event = F.fprintf fmt "passed as argument to %a" CallEvent.pp f | Capture {captured_as; location= _} -> F.fprintf fmt "value captured as `%a`" Pvar.pp_value_non_verbose captured_as + | Conditional {is_then_branch; if_kind; location= _} -> + F.fprintf fmt "expression in %s condition is %b" (Sil.if_kind_to_string if_kind) + is_then_branch | CppTemporaryCreated _ -> F.pp_print_string fmt "C++ temporary created" | FormalDeclared (pvar, _) -> @@ -49,6 +53,7 @@ let location_of_event = function | Assignment location | Call {location} | Capture {location} + | Conditional {location} | CppTemporaryCreated location | FormalDeclared (_, location) | VariableAccessed (_, location) diff --git a/infer/src/pulse/PulseValueHistory.mli b/infer/src/pulse/PulseValueHistory.mli index 1c02962a2..07c937156 100644 --- a/infer/src/pulse/PulseValueHistory.mli +++ b/infer/src/pulse/PulseValueHistory.mli @@ -12,6 +12,7 @@ type event = | Assignment of Location.t | Call of {f: CallEvent.t; location: Location.t; in_call: t} | Capture of {captured_as: Pvar.t; location: Location.t} + | Conditional of {is_then_branch: bool; if_kind: Sil.if_kind; location: Location.t} | CppTemporaryCreated of Location.t | FormalDeclared of Pvar.t * Location.t | VariableAccessed of Pvar.t * Location.t