[pulse] unified API for arithmetic

Summary:
Instead of having to remember to update both the inferbo and the concrete
intervals domains of pulse, hide these details under a unified API. This
should help the transition to adding a third(!) numerical domain later
on (pudge!).

Reviewed By: ezgicicek

Differential Revision: D21022920

fbshipit-source-id: 783157464

infer/src/pulse/PulseArithmetic.ml

@@ -0,0 +1,193 @@
+(*
+ * 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
+open PulseBasicInterface
+open PulseDomainInterface
+
+(** {2 Building arithmetic constraints} *)
+
+let and_nonnegative trace v astate =
+  AddressAttributes.add_one v (BoItv Itv.ItvPure.nat) astate
+  |> AddressAttributes.add_one v (CItv (CItv.zero_inf, trace))
+
+
+let and_positive trace v astate =
+  AddressAttributes.add_one v (BoItv Itv.ItvPure.pos) astate
+  |> AddressAttributes.add_one v (CItv (CItv.ge_to IntLit.one, trace))
+
+
+let and_eq_int trace v i astate =
+  AddressAttributes.add_one v (BoItv (Itv.ItvPure.of_int_lit i)) astate
+  |> AddressAttributes.add_one v (CItv (CItv.equal_to i, trace))
+
+
+(** {2 Operations} *)
+
+type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t
+
+let eval_arith_operand location binop_addr binop_hist bop op_lhs op_rhs astate =
+  let arith_of_op op astate =
+    match op with
+    | LiteralOperand i ->
+        Some (CItv.equal_to i)
+    | AbstractValueOperand v ->
+        AddressAttributes.get_citv v astate |> Option.map ~f:fst
+  in
+  match
+    Option.both (arith_of_op op_lhs astate) (arith_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 binop_trace = Trace.Immediate {location; history= binop_hist} in
+      let astate = AddressAttributes.add_one binop_addr (CItv (binop_a, binop_trace)) 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_binop location binop op_lhs op_rhs binop_hist astate =
+  let binop_addr = AbstractValue.mk_fresh () in
+  let astate =
+    eval_arith_operand location binop_addr binop_hist binop op_lhs op_rhs astate
+    |> eval_bo_itv_binop binop_addr binop op_lhs op_rhs
+  in
+  (astate, (binop_addr, binop_hist))
+
+
+let eval_unop_arith location unop_addr unop operand_addr unop_hist astate =
+  match
+    AddressAttributes.get_citv operand_addr astate
+    |> Option.bind ~f:(function a, _ -> CItv.unop unop a)
+  with
+  | None ->
+      astate
+  | Some unop_a ->
+      let unop_trace = Trace.Immediate {location; history= unop_hist} in
+      AddressAttributes.add_one unop_addr (CItv (unop_a, unop_trace)) 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_unop location unop addr unop_hist astate =
+  let unop_addr = AbstractValue.mk_fresh () in
+  let astate =
+    eval_unop_arith location unop_addr unop addr unop_hist astate
+    |> eval_unop_bo_itv unop_addr unop addr
+  in
+  (astate, (unop_addr, unop_hist))
+
+
+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 location astate = function
+  | LiteralOperand i ->
+      ( None
+      , Some
+          (CItv.equal_to i, Trace.Immediate {location; history= [ValueHistory.Assignment location]})
+      , Itv.ItvPure.of_int_lit i )
+  | AbstractValueOperand v ->
+      (Some v, AddressAttributes.get_citv v astate, AddressAttributes.get_bo_itv v astate)
+
+
+let record_abduced event location addr_opt orig_arith_hist_opt arith_opt astate =
+  match Option.both addr_opt arith_opt with
+  | None ->
+      astate
+  | Some (addr, arith) ->
+      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.CItv (arith, trace) 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 ~is_then_branch if_kind location ~negated bop lhs_op rhs_op astate =
+  let value_lhs_opt, arith_lhs_opt, bo_itv_lhs = eval_operand location astate lhs_op in
+  let value_rhs_opt, arith_rhs_opt, bo_itv_rhs = eval_operand location astate rhs_op in
+  match
+    CItv.abduce_binop_is_true ~negated bop (Option.map ~f:fst arith_lhs_opt)
+      (Option.map ~f:fst arith_rhs_opt)
+  with
+  | Unsatisfiable ->
+      (astate, false)
+  | Satisfiable (abduced_lhs, abduced_rhs) ->
+      let event = ValueHistory.Conditional {is_then_branch; if_kind; location} in
+      let astate =
+        record_abduced event location value_lhs_opt arith_lhs_opt abduced_lhs astate
+        |> record_abduced event location value_rhs_opt arith_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
+  |> function Some (arith, _) -> CItv.is_equal_to_zero arith | None -> false )
+  || Itv.ItvPure.is_zero (AddressAttributes.get_bo_itv v astate)

infer/src/pulse/PulseArithmetic.mli

@@ -0,0 +1,58 @@
+(*
+ * 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
+open PulseBasicInterface
+open PulseDomainInterface
+
+(** {2 Building arithmetic constraints} *)
+
+val and_nonnegative : Trace.t -> AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t
+(** [and_nonnegative trace v astate] is [astate ∧ v≥0] *)
+
+val and_positive : Trace.t -> AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t
+(** [and_positive v astate] is [astate ∧ v>0] *)
+
+val and_eq_int : Trace.t -> 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
+
+val eval_binop :
+     Location.t
+  -> Binop.t
+  -> operand
+  -> operand
+  -> ValueHistory.t
+  -> AbductiveDomain.t
+  -> AbductiveDomain.t * (AbstractValue.t * ValueHistory.t)
+
+val eval_unop :
+     Location.t
+  -> Unop.t
+  -> AbstractValue.t
+  -> ValueHistory.t
+  -> AbductiveDomain.t
+  -> AbductiveDomain.t * (AbstractValue.t * ValueHistory.t)
+
+val prune_binop :
+     is_then_branch:bool
+  -> Sil.if_kind
+  -> Location.t
+  -> negated:bool
+  -> Binop.t
+  -> operand
+  -> operand
+  -> AbductiveDomain.t
+  -> AbductiveDomain.t * bool
+
+(** {2 Queries} *)
+
+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 *)

infer/src/pulse/PulseModels.ml

@@ -44,9 +44,7 @@ module Misc = struct
     let ret_addr = AbstractValue.mk_fresh () in
     let astate =
       let i = IntLit.of_int64 i64 in
-      AddressAttributes.add_one ret_addr (BoItv (Itv.ItvPure.of_int_lit i)) astate
+      PulseArithmetic.and_eq_int (Immediate {location; history= []}) ret_addr i astate
-      |> AddressAttributes.add_one ret_addr
-           (CItv (CItv.equal_to i, Immediate {location; history= []}))
     in
     PulseOperations.write_id ret_id (ret_addr, []) astate |> PulseOperations.ok_continue
 
@@ -55,9 +53,7 @@ module Misc = struct
    fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let ret_addr = AbstractValue.mk_fresh () in
     let astate =
-      AddressAttributes.add_one ret_addr (BoItv Itv.ItvPure.nat) astate
+      PulseArithmetic.and_nonnegative (Immediate {location; history= []}) ret_addr astate
-      |> AddressAttributes.add_one ret_addr
-           (CItv (CItv.zero_inf, Immediate {location; history= []}))
     in
     PulseOperations.write_id ret_id (ret_addr, []) astate |> PulseOperations.ok_continue
 
@@ -82,12 +78,8 @@ module C = struct
    fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate ->
     (* NOTE: we could introduce a case-split explicitly on =0 vs ≠0 but instead only act on what we
        currently know about the value. This is purely to avoid contributing to path explosion. *)
-    let is_known_zero =
+    (* freeing 0 is a no-op *)
-      ( AddressAttributes.get_citv (fst deleted_access) astate
+    if PulseArithmetic.is_known_zero astate (fst deleted_access) then
-      |> function Some (arith, _) -> CItv.is_equal_to_zero arith | None -> false )
-      || Itv.ItvPure.is_zero (AddressAttributes.get_bo_itv (fst deleted_access) astate)
-    in
-    if is_known_zero then (* freeing 0 is a no-op *)
       PulseOperations.ok_continue astate
     else
       let+ astate = PulseOperations.invalidate location Invalidation.CFree deleted_access astate in
@@ -105,13 +97,11 @@ module C = struct
     let immediate_hist = Trace.Immediate {location; history= hist} in
     let astate_alloc =
       PulseOperations.allocate callee_procname location ret_value astate
-      |> AddressAttributes.add_one ret_addr (BoItv Itv.ItvPure.pos)
+      |> PulseArithmetic.and_positive immediate_hist ret_addr
-      |> AddressAttributes.add_one ret_addr (CItv (CItv.ge_to IntLit.one, immediate_hist))
       |> ExecutionDomain.continue
     in
     let+ astate_null =
-      AddressAttributes.add_one ret_addr (BoItv (Itv.ItvPure.of_int_lit IntLit.zero)) astate
+      PulseArithmetic.and_eq_int immediate_hist ret_addr IntLit.zero astate
-      |> AddressAttributes.add_one ret_addr (CItv (CItv.equal_to IntLit.zero, immediate_hist))
       |> PulseOperations.invalidate location (Invalidation.ConstantDereference IntLit.zero)
            ret_value
     in
@@ -169,7 +159,7 @@ module StdAtomicInteger = struct
   let arith_bop prepost location event ret_id bop this operand astate =
     let* astate, int_addr, (old_int, old_int_hist) = load_backing_int location this astate in
     let astate, (new_int, hist) =
-      PulseOperations.eval_binop location bop (AbstractValueOperand old_int) operand old_int_hist
+      PulseArithmetic.eval_binop location bop (AbstractValueOperand old_int) operand old_int_hist
         astate
     in
     let+ astate =

infer/src/pulse/PulseOperations.ml

@@ -102,80 +102,6 @@ let eval_access location addr_hist access astate =
   Memory.eval_edge addr_hist access astate
 
 
-type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t
-
-let eval_arith_operand location binop_addr binop_hist bop op_lhs op_rhs astate =
-  let arith_of_op op astate =
-    match op with
-    | LiteralOperand i ->
-        Some (CItv.equal_to i)
-    | AbstractValueOperand v ->
-        AddressAttributes.get_citv v astate |> Option.map ~f:fst
-  in
-  match
-    Option.both (arith_of_op op_lhs astate) (arith_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 binop_trace = Trace.Immediate {location; history= binop_hist} in
-      let astate = AddressAttributes.add_one binop_addr (CItv (binop_a, binop_trace)) 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_binop location binop op_lhs op_rhs binop_hist astate =
-  let binop_addr = AbstractValue.mk_fresh () in
-  let astate =
-    eval_arith_operand location binop_addr binop_hist binop op_lhs op_rhs astate
-    |> eval_bo_itv_binop binop_addr binop op_lhs op_rhs
-  in
-  (astate, (binop_addr, binop_hist))
-
-
-let eval_unop_arith location unop_addr unop operand_addr unop_hist astate =
-  match
-    AddressAttributes.get_citv operand_addr astate
-    |> Option.bind ~f:(function a, _ -> CItv.unop unop a)
-  with
-  | None ->
-      astate
-  | Some unop_a ->
-      let unop_trace = Trace.Immediate {location; history= unop_hist} in
-      AddressAttributes.add_one unop_addr (CItv (unop_a, unop_trace)) 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_unop location unop addr unop_hist astate =
-  let unop_addr = AbstractValue.mk_fresh () in
-  let astate =
-    eval_unop_arith location unop_addr unop addr unop_hist astate
-    |> eval_unop_bo_itv unop_addr unop addr
-  in
-  (astate, (unop_addr, unop_hist))
-
-
 let eval location exp0 astate =
   let rec eval exp astate =
     match (exp : Exp.t) with
@@ -210,10 +136,7 @@ let eval location exp0 astate =
         (* TODO: make identical const the same address *)
         let addr = AbstractValue.mk_fresh () in
         let astate =
-          AddressAttributes.add_one addr
+          PulseArithmetic.and_eq_int (Immediate {location; history= []}) addr i astate
-            (CItv (CItv.equal_to i, Immediate {location; history= []}))
-            astate
-          |> AddressAttributes.add_one addr (BoItv (Itv.ItvPure.of_int_lit i))
           |> AddressAttributes.invalidate
                (addr, [ValueHistory.Assignment location])
                (ConstantDereference i) location
@@ -221,7 +144,7 @@ let eval location exp0 astate =
         Ok (astate, (addr, []))
     | UnOp (unop, exp, _typ) ->
         let+ astate, (addr, hist) = eval exp astate in
-        eval_unop location unop addr hist astate
+        PulseArithmetic.eval_unop location unop addr hist astate
     | BinOp (bop, e_lhs, e_rhs) ->
         let* astate, (addr_lhs, hist_lhs) = eval e_lhs astate in
         let+ ( astate
@@ -230,108 +153,31 @@ let eval location exp0 astate =
                _ ) ) =
           eval e_rhs astate
         in
-        eval_binop location bop (AbstractValueOperand addr_lhs) (AbstractValueOperand addr_rhs)
+        PulseArithmetic.eval_binop location bop (AbstractValueOperand addr_lhs)
-          hist_lhs astate
+          (AbstractValueOperand addr_rhs) hist_lhs astate
     | Const _ | Sizeof _ | Exn _ ->
         Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) []))
   in
   eval exp0 astate
 
 
-let eval_arith location exp astate =
+let eval_to_operand location exp astate =
   match (exp : Exp.t) with
   | Const (Cint i) ->
-      Ok
+      Ok (astate, PulseArithmetic.LiteralOperand i)
-        ( astate
-        , None
-        , Some
-            ( CItv.equal_to i
-            , Trace.Immediate {location; history= [ValueHistory.Assignment location]} )
-        , Itv.ItvPure.of_int_lit i )
   | exp ->
       let+ astate, (value, _) = eval location exp astate in
-      ( astate
+      (astate, PulseArithmetic.AbstractValueOperand value)
-      , Some value
-      , AddressAttributes.get_citv value astate
-      , AddressAttributes.get_bo_itv value astate )
-
-
-let record_abduced event location addr_opt orig_arith_hist_opt arith_opt astate =
-  match Option.both addr_opt arith_opt with
-  | None ->
-      astate
-  | Some (addr, arith) ->
-      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.CItv (arith, trace) in
-      AddressAttributes.abduce_attribute addr attribute astate
-      |> AddressAttributes.add_one addr attribute
 
 
 let prune ~is_then_branch if_kind location ~condition astate =
-  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)
-  in
-  let bind_satisfiable ~satisfiable astate ~f = if satisfiable then f astate else (astate, false) in
   let rec prune_aux ~negated exp astate =
     match (exp : Exp.t) with
-    | BinOp (bop, exp_lhs, exp_rhs) -> (
+    | BinOp (bop, exp_lhs, exp_rhs) ->
-        let* astate, value_lhs_opt, arith_lhs_opt, bo_itv_lhs =
+        let* astate, lhs_op = eval_to_operand location exp_lhs astate in
-          eval_arith location exp_lhs astate
+        let+ astate, rhs_op = eval_to_operand location exp_rhs astate in
-        in
+        PulseArithmetic.prune_binop ~is_then_branch if_kind location ~negated bop lhs_op rhs_op
-        let+ astate, value_rhs_opt, arith_rhs_opt, bo_itv_rhs =
+          astate
-          eval_arith location exp_rhs astate
-        in
-        match
-          CItv.abduce_binop_is_true ~negated bop (Option.map ~f:fst arith_lhs_opt)
-            (Option.map ~f:fst arith_rhs_opt)
-        with
-        | Unsatisfiable ->
-            (astate, false)
-        | Satisfiable (abduced_lhs, abduced_rhs) ->
-            let event = ValueHistory.Conditional {is_then_branch; if_kind; location} in
-            let astate =
-              record_abduced event location value_lhs_opt arith_lhs_opt abduced_lhs astate
-              |> record_abduced event location value_rhs_opt arith_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 ) ) )
     | UnOp (LNot, exp', _) ->
         prune_aux ~negated:(not negated) exp' astate
     | exp ->

infer/src/pulse/PulseOperations.mli

@@ -47,17 +47,6 @@ val eval_access :
 (** Like [eval] but starts from an address instead of an expression, checks that it is valid, and if
     so dereferences it according to the access. *)
 
-type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t
-
-val eval_binop :
-     Location.t
-  -> Binop.t
-  -> operand
-  -> operand
-  -> ValueHistory.t
-  -> t
-  -> t * (AbstractValue.t * ValueHistory.t)
-
 val havoc_id : Ident.t -> ValueHistory.t -> t -> t
 
 val havoc_field :