[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
master
Jules Villard 5 years ago committed by Facebook GitHub Bot
parent ffde64c0c9
commit 385b6fa914

@ -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:

@ -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

@ -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

@ -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

@ -7,4 +7,4 @@
open! IStd
include PulsePathConditionModuleType.S
include Pudge_intf.S

@ -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)

@ -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)

@ -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

@ -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)
map_path_condition astate ~f:(fun phi -> PathCondition.and_eq_int v i phi)
(** {2 Operations} *)
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
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_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 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
map_path_condition astate ~f:(fun phi ->
PathCondition.eval_binop binop_addr binop op_lhs op_rhs phi )
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 )
map_path_condition astate ~f:(fun phi -> PathCondition.eval_unop unop_addr unop addr phi)
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 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
let phi' =
PathCondition.prune_binop ~negated bop lhs_op rhs_op astate.AbductiveDomain.path_condition
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 ) )
AbductiveDomain.set_path_condition phi' 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_known_zero astate v = PathCondition.is_known_zero astate.AbductiveDomain.path_condition v
let is_unsat_cheap astate = PathCondition.is_unsat_cheap astate.AbductiveDomain.path_condition
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

@ -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

@ -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

@ -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

@ -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

@ -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

@ -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"]

@ -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_}

@ -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

@ -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)) )

@ -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 =
let add_call_to_attributes proc_name call_location caller_history 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 ->
Attribute.map_trace attr ~f:(fun trace ->
add_call_to_trace proc_name call_location caller_history trace ) )
in
(!subst_ref, attrs)
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
if PathCondition.is_unsat_cheap path_condition then raise (Contradiction PathCondition)
else
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
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

@ -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]. *)

@ -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
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
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}
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 "@[<hv>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 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 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 bo_itv =
Itv.ItvPure.arith_binop bop (bo_itv_of_op op_lhs bo_itvs) (bo_itv_of_op op_rhs bo_itvs)
in
BoItvs.add binop_addr bo_itv bo_itvs
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 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
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 ) )
let fv {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} =
Term.Var.Set.union (Equality.fv eqs) (Term.fv non_eqs)
(** {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 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 is_unsat_cheap phi = not phi.satisfiable
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))}
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

@ -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 *)

@ -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))}

@ -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

@ -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]

@ -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);
}

@ -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]

Loading…
Cancel
Save