[pulse] rename "PulseArithmetic" to "PulseCItv"

Summary: In preparation for PulseArithmetic to be something else.

Reviewed By: ezgicicek

Differential Revision: D20393928

fbshipit-source-id: d93131e12

infer/src/pulse/PulseAbductiveDomain.ml

@@ -215,9 +215,7 @@ module AddressAttributes = struct
     BaseAddressAttributes.get_closure_proc_name addr (astate.post :> base_domain).attrs
 
 
-  let get_arithmetic addr astate =
-    BaseAddressAttributes.get_arithmetic 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
@@ -451,11 +449,11 @@ module PrePost = struct
             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. *)
-    | Arithmetic of
+    | CItv of
         { addr_caller: AbstractValue.t
         ; addr_callee: AbstractValue.t
-        ; arith_caller: Arithmetic.t option
-        ; arith_callee: Arithmetic.t option
+        ; 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 *)
@@ -475,11 +473,11 @@ module PrePost = struct
           "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
-    | Arithmetic {addr_caller; addr_callee; arith_caller; arith_callee; 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 Arithmetic.pp)
-          arith_caller AbstractValue.pp addr_callee (Pp.option Arithmetic.pp) arith_callee
+           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 pp_call_state call_state AbstractValue.pp addr_callee
     | ArithmeticBo {addr_caller; addr_callee; arith_callee; call_state} ->
         F.fprintf fmt
@@ -633,24 +631,20 @@ module PrePost = struct
 
   let subst_attribute call_state subst_ref astate ~addr_caller attr ~addr_callee =
     match (attr : Attribute.t) with
-    | Arithmetic (arith_callee, hist) -> (
-        let arith_caller_opt =
-          AddressAttributes.get_arithmetic addr_caller astate |> Option.map ~f:fst
-        in
-        match
-          Arithmetic.abduce_binop_is_true ~negated:false Eq arith_caller_opt (Some arith_callee)
-        with
+    | CItv (arith_callee, hist) -> (
+        let arith_caller_opt = AddressAttributes.get_citv addr_caller astate |> Option.map ~f:fst in
+        match CItv.abduce_binop_is_true ~negated:false Eq arith_caller_opt (Some arith_callee) with
         | Unsatisfiable ->
             raise
               (Contradiction
-                 (Arithmetic
+                 (CItv
                     { addr_caller
                     ; addr_callee
                     ; arith_caller= arith_caller_opt
                     ; arith_callee= Some arith_callee
                     ; call_state }))
         | Satisfiable (Some abduce_caller, _abduce_callee) ->
-            Attribute.Arithmetic (abduce_caller, hist)
+            Attribute.CItv (abduce_caller, hist)
         | Satisfiable (None, _) ->
             attr )
     | BoItv itv -> (
@@ -683,9 +677,8 @@ module PrePost = struct
       | Invalid (invalidation, trace) ->
           Attribute.Invalid
             (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)
+      | CItv (arith, trace) ->
+          Attribute.CItv (arith, add_call_to_trace proc_name call_location caller_history trace)
       | Allocated trace ->
           Attribute.Allocated (add_call_to_trace proc_name call_location caller_history trace)
       | AddressOfCppTemporary _

infer/src/pulse/PulseAbductiveDomain.mli

@@ -84,7 +84,7 @@ module AddressAttributes : sig
 
   val std_vector_reserve : AbstractValue.t -> t -> t
 
-  val get_arithmetic : AbstractValue.t -> t -> (Arithmetic.t * Trace.t) option
+  val get_citv : AbstractValue.t -> t -> (CItv.t * Trace.t) option
 
   val get_bo_itv : AbstractValue.t -> t -> Itv.ItvPure.t
 

infer/src/pulse/PulseAttribute.ml

@@ -6,7 +6,7 @@
  *)
 open! IStd
 module F = Format
-module Arithmetic = PulseArithmetic
+module CItv = PulseCItv
 module Invalidation = PulseInvalidation
 module Trace = PulseTrace
 module ValueHistory = PulseValueHistory
@@ -29,7 +29,7 @@ module Attribute = struct
     | AddressOfCppTemporary of Var.t * ValueHistory.t
     | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t
     | Allocated of Trace.t
-    | Arithmetic of Arithmetic.t * Trace.t
+    | CItv of CItv.t * Trace.t
     | BoItv of Itv.ItvPure.t
     | Closure of Procname.t
     | Invalid of Invalidation.t * Trace.t
@@ -63,7 +63,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, dummy_trace))
+  let const_rank = Variants.to_rank (CItv (CItv.equal_to IntLit.zero, dummy_trace))
 
   let bo_itv_rank = Variants.to_rank (BoItv Itv.ItvPure.zero)
 
@@ -82,8 +82,8 @@ module Attribute = struct
         F.fprintf f "BoItv (%a)" Itv.ItvPure.pp bo_itv
     | Closure pname ->
         Procname.pp f pname
-    | Arithmetic (phi, trace) ->
-        F.fprintf f "Arith %a" (Trace.pp ~pp_immediate:(fun fmt -> Arithmetic.pp fmt phi)) trace
+    | CItv (phi, trace) ->
+        F.fprintf f "Arith %a" (Trace.pp ~pp_immediate:(fun fmt -> CItv.pp fmt phi)) trace
     | Invalid (invalidation, trace) ->
         F.fprintf f "Invalid %a"
           (Trace.pp ~pp_immediate:(fun fmt -> Invalidation.pp fmt invalidation))
@@ -143,10 +143,10 @@ module Attributes = struct
     || Option.is_some (Set.find_rank attrs Attribute.invalid_rank)
 
 
-  let get_arithmetic attrs =
+  let get_citv attrs =
     Set.find_rank attrs Attribute.const_rank
     |> Option.map ~f:(fun attr ->
-           let[@warning "-8"] (Attribute.Arithmetic (a, trace)) = attr in
+           let[@warning "-8"] (Attribute.CItv (a, trace)) = attr in
            (a, trace) )
 
 
@@ -163,7 +163,7 @@ end
 include Attribute
 
 let is_suitable_for_pre = function
-  | Arithmetic _ | BoItv _ | MustBeValid _ ->
+  | CItv _ | BoItv _ | MustBeValid _ ->
       true
   | AddressOfCppTemporary _
   | AddressOfStackVariable _

infer/src/pulse/PulseAttribute.mli

@@ -6,7 +6,7 @@
  *)
 open! IStd
 module F = Format
-module Arithmetic = PulseArithmetic
+module CItv = PulseCItv
 module Invalidation = PulseInvalidation
 module Trace = PulseTrace
 module ValueHistory = PulseValueHistory
@@ -15,7 +15,7 @@ type t =
   | AddressOfCppTemporary of Var.t * ValueHistory.t
   | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t
   | Allocated of Trace.t
-  | Arithmetic of Arithmetic.t * Trace.t
+  | CItv of CItv.t * Trace.t
   | BoItv of Itv.ItvPure.t
   | Closure of Procname.t
   | Invalid of Invalidation.t * Trace.t
@@ -35,7 +35,7 @@ module Attributes : sig
 
   val get_closure_proc_name : t -> Procname.t option
 
-  val get_arithmetic : t -> (Arithmetic.t * Trace.t) option
+  val get_citv : t -> (CItv.t * Trace.t) option
 
   val get_bo_itv : t -> Itv.ItvPure.t option
 

infer/src/pulse/PulseBaseAddressAttributes.ml

@@ -71,7 +71,7 @@ let get_attribute getter address attrs =
 
 let get_closure_proc_name = get_attribute Attributes.get_closure_proc_name
 
-let get_arithmetic = get_attribute Attributes.get_arithmetic
+let get_citv = get_attribute Attributes.get_citv
 
 let get_bo_itv v memory =
   match get_attribute Attributes.get_bo_itv v memory with

infer/src/pulse/PulseBaseAddressAttributes.mli

@@ -30,7 +30,7 @@ val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.
 
 val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option
 
-val get_arithmetic : AbstractValue.t -> t -> (Arithmetic.t * Trace.t) option
+val get_citv : AbstractValue.t -> t -> (CItv.t * Trace.t) option
 
 val get_bo_itv : AbstractValue.t -> t -> Itv.ItvPure.t
 

infer/src/pulse/PulseBasicInterface.ml

@@ -9,10 +9,10 @@ open! IStd
 (** Basic Pulse modules that are safe to use in any module *)
 
 module AbstractValue = PulseAbstractValue
-module Arithmetic = PulseArithmetic
 module Attribute = PulseAttribute
 module Attributes = PulseAttribute.Attributes
 module CallEvent = PulseCallEvent
+module CItv = PulseCItv
 module Diagnostic = PulseDiagnostic
 module Invalidation = PulseInvalidation
 module Trace = PulseTrace

infer/src/pulse/PulseCItv.ml

@@ -5,8 +5,6 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-[@@@ocamlformat "parse-docstrings = false"]
-
 open! IStd
 module F = Format
 module L = Logging
@@ -112,8 +110,8 @@ end
 
 module Unsafe : sig
   type t = private
-    | Between of Bound.t * Bound.t  (** we write [b1,b2] for these *)
-    | Outside of IntLit.t * IntLit.t  (** we write i1][i2 for these *)
+    | Between of Bound.t * Bound.t  (** we write \[b1,b2\] for these *)
+    | Outside of IntLit.t * IntLit.t  (** we write i1\]\[i2 for these *)
   [@@deriving compare]
 
   val between : Bound.t -> Bound.t -> t
@@ -177,7 +175,7 @@ let has_empty_intersection a1 a2 =
   | Between (lower1, upper1), Between (lower2, upper2) ->
       Bound.lt upper1 lower2 || Bound.lt upper2 lower1
   | Between (lower1, upper1), Outside (l2, u2) | Outside (l2, u2), Between (lower1, upper1) ->
-      (* is [l1, u1] inside [l2, u2]? *)
+      (* is \[l1, u1\] inside \[l2, u2\]? *)
       Bound.le (Int l2) lower1 && Bound.ge (Int u2) upper1
 
 
@@ -235,22 +233,22 @@ let rec abduce_eq (a1 : t) (a2 : t) =
   | Outside (l1, u1), Outside (l2, u2) ->
       (* ∃x. (x<l1 ∨ x>u1) ∧ (x<l2 ∨ x>u2) ∧ li<=ui*)
       (* all the possible cases:
-         x: --------[   ]---------
-         y: -----[       ]--------
+         x: --------\[   \]---------
+         y: -----\[       \]--------
 
-         x: ---[           ]------
-         y: -----[       ]--------
+         x: ---\[           \]------
+         y: -----\[       \]--------
 
-         x: ---[       ]----------
-         y: -----[       ]--------
+         x: ---\[       \]----------
+         y: -----\[       \]--------
 
-         x: ---------[       ]----
-         y: -----[       ]--------
+         x: ---------\[       \]----
+         y: -----\[       \]--------
 
-         -> SAT, can tighten both to min(l1,l2)][max(u1,u2)
+         -> SAT, can tighten both to min(l1,l2)\]\[max(u1,u2)
 
-         x: ---------------[   ]--
-         y: -----[       ]--------
+         x: ---------------\[   \]--
+         y: -----\[       \]--------
          or symmetrically x<->y => cannot express the 3 intervals that would be needed so return SAT
          (TODO: we might want to keep only one of these, which would be a kind of recency model of
          disequalities: remember the last known disequality)
@@ -267,24 +265,24 @@ let rec abduce_eq (a1 : t) (a2 : t) =
       (* ∃x. l1≤x≤u1 ∧ (x<l2 ∨ x>u2) *)
       (* all the possible cases:
 
-         x:  [-------]
-         y: --[   ]---
+         x:  \[-------\]
+         y: --\[   \]---
 
-         case 1 above: SAT, cannot say more unless a1 is [-∞,+∞] (then we can abduce that a1 is
+         case 1 above: SAT, cannot say more unless a1 is \[-∞,+∞\] (then we can abduce that a1 is
          the same as a2)
 
-         x:        [--]
-         y: ------[   ]--
+         x:        \[--\]
+         y: ------\[   \]--
 
          case 2 above: UNSAT
 
-         x:   [---]
-         y: ------[   ]--
+         x:   \[---\]
+         y: ------\[   \]--
 
          case 3 above: SAT: x = x\cap y for both
 
-         x:      [----]
-         y: ------[   ]--
+         x:      \[----\]
+         y: ------\[   \]--
 
          case 4 above: SAT: x\cap y for both
       *)
@@ -360,11 +358,11 @@ let abduce_le (a1 : t) (a2 : t) =
       (* two cases:
          1. l1<l2: we don't know if x≤y for sure and cannot express a good fact to abduce to make
          it true
-         x:   [----doesn't matter where u1 is
-         y: -----[       ]---------------------
+         x:   \[----doesn't matter where u1 is
+         y: -----\[       \]---------------------
          2. l1≥l2: we can abduce that y≥max(u2+1, l1) and that makes it SAT
-         x:      [----doesn't matter either
-         y: -----[       ]---------------------
+         x:      \[----doesn't matter either
+         y: -----\[       \]---------------------
       *)
       if Bound.lt lower1 (Int l2) then (* case 1: l1<l2 *) Satisfiable (None, None)
       else
@@ -374,12 +372,12 @@ let abduce_le (a1 : t) (a2 : t) =
   | Outside (l1, u1), Between (_lower2, upper2) ->
       (* similarly, two cases:
          1. u1≥u2: can refine to x≤min(l1+1, u2)
-         x: -----[       ]---------------------
-         y: ..-]
-         or y:      ...-----]
+         x: -----\[       \]---------------------
+         y: ..-\]
+         or y:      ...-----\]
          2. u1<u2: cannot deduce anything
-         x: -----[       ]---------------------
-         y:          ...---]
+         x: -----\[       \]---------------------
+         y:          ...---\]
       *)
       if Bound.ge (Int u1) upper2 then
         (* case 1: l1>l2 *)

infer/src/pulse/PulseCItv.mli

@@ -7,6 +7,8 @@
 open! IStd
 module F = Format
 
+(** Concrete interval domain (CItv) *)
+
 type t [@@deriving compare]
 
 val equal_to : IntLit.t -> t

infer/src/pulse/PulseModels.ml

@@ -43,7 +43,7 @@ module Misc = struct
       let i = IntLit.of_int64 i64 in
       AddressAttributes.add_one ret_addr (BoItv (Itv.ItvPure.of_int_lit i)) astate
       |> AddressAttributes.add_one ret_addr
-           (Arithmetic (Arithmetic.equal_to i, Immediate {location; history= []}))
+           (CItv (CItv.equal_to i, Immediate {location; history= []}))
     in
     Ok [PulseOperations.write_id ret_id (ret_addr, []) astate]
 
@@ -54,7 +54,7 @@ module Misc = struct
     let astate =
       AddressAttributes.add_one ret_addr (BoItv Itv.ItvPure.nat) astate
       |> AddressAttributes.add_one ret_addr
-           (Arithmetic (Arithmetic.zero_inf, Immediate {location; history= []}))
+           (CItv (CItv.zero_inf, Immediate {location; history= []}))
     in
     Ok [PulseOperations.write_id ret_id (ret_addr, []) astate]
 
@@ -78,8 +78,8 @@ module C = struct
     (* 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 =
-      ( AddressAttributes.get_arithmetic (fst deleted_access) astate
-      |> function Some (arith, _) -> Arithmetic.is_equal_to_zero arith | None -> false )
+      ( AddressAttributes.get_citv (fst deleted_access) astate
+      |> 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 *)

infer/src/pulse/PulseOperations.ml

@@ -105,21 +105,19 @@ 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 (Arithmetic.equal_to i)
+        Some (CItv.equal_to i)
     | AbstractValueOperand v ->
-        AddressAttributes.get_arithmetic v astate |> Option.map ~f:fst
+        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) -> Arithmetic.binop bop addr_lhs addr_rhs)
+    |> 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 (Arithmetic (binop_a, binop_trace)) astate
-      in
+      let astate = AddressAttributes.add_one binop_addr (CItv (binop_a, binop_trace)) astate in
       astate
 
 
@@ -148,14 +146,14 @@ let eval_binop location binop op_lhs op_rhs binop_hist astate =
 
 let eval_unop_arith location unop_addr unop operand_addr unop_hist astate =
   match
-    AddressAttributes.get_arithmetic operand_addr astate
-    |> Option.bind ~f:(function a, _ -> Arithmetic.unop unop a)
+    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 (Arithmetic (unop_a, unop_trace)) astate
+      AddressAttributes.add_one unop_addr (CItv (unop_a, unop_trace)) astate
 
 
 let eval_unop_bo_itv unop_addr unop operand_addr astate =
@@ -210,7 +208,7 @@ let eval location exp0 astate =
         let addr = AbstractValue.mk_fresh () in
         let astate =
           AddressAttributes.add_one addr
-            (Arithmetic (Arithmetic.equal_to i, Immediate {location; history= []}))
+            (CItv (CItv.equal_to i, Immediate {location; history= []}))
             astate
           |> AddressAttributes.add_one addr (BoItv (Itv.ItvPure.of_int_lit i))
           |> AddressAttributes.invalidate
@@ -244,14 +242,14 @@ let eval_arith location exp astate =
         ( astate
         , None
         , Some
-            ( Arithmetic.equal_to i
+            ( 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
       , Some value
-      , AddressAttributes.get_arithmetic value astate
+      , AddressAttributes.get_citv value astate
       , AddressAttributes.get_bo_itv value astate )
 
 
@@ -267,7 +265,7 @@ let record_abduced event location addr_opt orig_arith_hist_opt arith_opt astate
         | Some (_, trace) ->
             Trace.add_event event trace
       in
-      let attribute = Attribute.Arithmetic (arith, trace) in
+      let attribute = Attribute.CItv (arith, trace) in
       AddressAttributes.abduce_attribute addr attribute astate
       |> AddressAttributes.add_one addr attribute
 
@@ -302,7 +300,7 @@ let prune ~is_then_branch if_kind location ~condition astate =
           eval_arith location exp_rhs astate
         in
         match
-          Arithmetic.abduce_binop_is_true ~negated bop (Option.map ~f:fst arith_lhs_opt)
+          CItv.abduce_binop_is_true ~negated bop (Option.map ~f:fst arith_lhs_opt)
             (Option.map ~f:fst arith_rhs_opt)
         with
         | Unsatisfiable ->