From 94930e3b11676a04b3694f5d610bcfd1ad74f88c Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 18 Feb 2021 07:48:53 -0800 Subject: [PATCH] [pulse] refactor incorporate_new_eqs Summary: Pretty minor, it's more convenient to make it return the state and will be used in a later diff when that function will actually sometimes modify the state. Reviewed By: skcho Differential Revision: D26488376 fbshipit-source-id: a21eaf008 --- infer/src/pulse/PulseAbductiveDomain.ml | 37 ++++++++++++++---------- infer/src/pulse/PulseAbductiveDomain.mli | 2 +- infer/src/pulse/PulseArithmetic.ml | 12 +++----- infer/src/pulse/PulseInterproc.ml | 11 +++---- 4 files changed, 31 insertions(+), 31 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 9659b863a..cd7d18ee5 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -687,21 +687,23 @@ let is_allocated {post; pre} v = let incorporate_new_eqs astate new_eqs = - List.fold_until new_eqs ~init:() - ~finish:(fun () -> Sat ()) - ~f:(fun () (new_eq : PulseFormula.new_eq) -> + List.fold_until new_eqs ~init:astate + ~finish:(fun astate -> Sat astate) + ~f:(fun astate (new_eq : PulseFormula.new_eq) -> match new_eq with | EqZero v when is_allocated astate v -> L.d_printfln "CONTRADICTION: %a = 0 but is allocated" AbstractValue.pp v ; Stop Unsat - | Equal (v1, v2) - when (not (AbstractValue.equal v1 v2)) && is_allocated astate v1 && is_allocated astate v2 - -> - L.d_printfln "CONTRADICTION: %a = %a but both are separately allocated" AbstractValue.pp - v1 AbstractValue.pp v2 ; - Stop Unsat + | Equal (v1, v2) when AbstractValue.equal v1 v2 -> + Continue astate + | Equal (v1, v2) -> + if is_allocated astate v1 && is_allocated astate v2 then ( + L.d_printfln "CONTRADICTION: %a = %a but both are separately allocated" AbstractValue.pp + v1 AbstractValue.pp v2 ; + Stop Unsat ) + else Continue astate | _ -> - Continue () ) + Continue astate ) (** it's a good idea to normalize the path condition before calling this function *) @@ -744,7 +746,7 @@ let summary_of_post pdesc astate = if is_unsat then Unsat else let astate = {astate with path_condition} in - let* () = incorporate_new_eqs astate new_eqs in + let* astate = incorporate_new_eqs astate new_eqs in L.d_printfln "Canonicalizing...@\n" ; let* astate = canonicalize astate in L.d_printfln "Canonicalized state: %a@\n" pp astate ; @@ -756,7 +758,7 @@ let summary_of_post pdesc astate = let* path_condition, new_eqs = PathCondition.simplify ~keep:live_addresses astate.path_condition in - let+ () = incorporate_new_eqs astate new_eqs in + let+ astate = incorporate_new_eqs astate new_eqs in let astate = {astate with path_condition; topl= PulseTopl.simplify ~keep:live_addresses astate.topl} in @@ -768,9 +770,14 @@ let get_pre {pre} = (pre :> BaseDomain.t) let get_post {post} = (post :> BaseDomain.t) (* re-exported for mli *) -let incorporate_new_eqs astate (phi, new_eqs) = - if PathCondition.is_unsat_cheap phi then phi - else match incorporate_new_eqs astate new_eqs with Unsat -> PathCondition.false_ | Sat () -> phi +let incorporate_new_eqs new_eqs astate = + if PathCondition.is_unsat_cheap astate.path_condition then astate + else + match incorporate_new_eqs astate new_eqs with + | Unsat -> + {astate with path_condition= PathCondition.false_} + | Sat astate -> + astate module Topl = struct diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index a861d82cc..4c370487f 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -202,7 +202,7 @@ val set_post_edges : AbstractValue.t -> BaseMemory.Edges.t -> t -> t val set_post_cell : AbstractValue.t * ValueHistory.t -> BaseDomain.cell -> Location.t -> t -> t (** directly set the edges and attributes for the given address, bypassing abduction altogether *) -val incorporate_new_eqs : t -> PathCondition.t * PathCondition.new_eqs -> PathCondition.t +val incorporate_new_eqs : PathCondition.new_eqs -> t -> t (** Check that the new equalities discovered are compatible with the current pre and post heaps, e.g. [x = 0] is not compatible with [x] being allocated, and [x = y] is not compatible with [x] and [y] being allocated separately. In those cases, the resulting path condition is diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml index 3b7b20a4b..1be0f79d2 100644 --- a/infer/src/pulse/PulseArithmetic.ml +++ b/infer/src/pulse/PulseArithmetic.ml @@ -10,9 +10,8 @@ open PulseBasicInterface module AbductiveDomain = PulseAbductiveDomain let map_path_condition ~f astate = - AbductiveDomain.set_path_condition - (f astate.AbductiveDomain.path_condition |> AbductiveDomain.incorporate_new_eqs astate) - astate + let phi, new_eqs = f astate.AbductiveDomain.path_condition in + AbductiveDomain.set_path_condition phi astate |> AbductiveDomain.incorporate_new_eqs new_eqs let and_nonnegative v astate = @@ -41,11 +40,8 @@ let eval_unop unop_addr unop addr 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 - |> AbductiveDomain.incorporate_new_eqs astate - in - AbductiveDomain.set_path_condition phi' astate + map_path_condition astate ~f:(fun phi -> + PathCondition.prune_binop ~negated bop lhs_op rhs_op phi ) let prune_eq_zero v astate = diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 08f655626..5fd8fcf86 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -270,13 +270,10 @@ let conjoin_callee_arith pre_post call_state = PathCondition.and_callee call_state.subst call_state.astate.path_condition ~callee:pre_post.AbductiveDomain.path_condition in - let path_condition = - AbductiveDomain.incorporate_new_eqs call_state.astate (path_condition, new_eqs) - 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 - {call_state with astate; subst} + let astate = AbductiveDomain.set_path_condition path_condition call_state.astate in + let astate = AbductiveDomain.incorporate_new_eqs new_eqs astate in + if PathCondition.is_unsat_cheap astate.path_condition then raise (Contradiction PathCondition) + else {call_state with astate; subst} let apply_arithmetic_constraints callee_proc_name call_location pre_post call_state =