[pulse] get rid of constants cache

Summary:
Now that the formula is incrementally normalising we can get rid of the
"constant cache" which mapped integer constants to their corresponding abstract
values. The formula already has this information in `term_eqs`.

Reviewed By: dulmarod

Differential Revision: D50972775

fbshipit-source-id: 13215272b45eedf88e87dfc0c106549cf8b62f61

infer/src/pulse/PulseArithmetic.ml

@@ -123,3 +123,9 @@ let and_is_int v astate = map_path_condition astate ~f:(fun phi -> Formula.and_i
 
 let and_equal_instanceof v1 v2 t astate =
   map_path_condition astate ~f:(fun phi -> Formula.and_equal_instanceof v1 v2 t phi)
+
+
+let absval_of_int astate i =
+  let phi, v = Formula.absval_of_int astate.AbductiveDomain.path_condition i in
+  let astate = AbductiveDomain.set_path_condition phi astate in
+  (astate, v)

infer/src/pulse/PulseArithmetic.mli

@@ -111,3 +111,5 @@ val and_equal_instanceof :
   -> Typ.t
   -> AbductiveDomain.t
   -> AbductiveDomain.t AccessResult.t SatUnsat.t
+
+val absval_of_int : AbductiveDomain.t -> IntLit.t -> AbductiveDomain.t * AbstractValue.t

infer/src/pulse/PulseFormula.ml

@@ -3982,23 +3982,14 @@ let fold_variables {conditions; phi} ~init ~f =
   Formula.fold_variables phi ~init ~f
 
 
-module Constants = struct
-  module M = Caml.Map.Make (IntLit)
-
-  let initial_cache = M.empty
-
-  let cache = ref initial_cache
-
-  let get_int formula i =
-    match M.find_opt i !cache with
-    | Some v ->
-        get_var_repr formula v
-    | None ->
-        let v = Var.mk_fresh () in
-        cache := M.add i v !cache ;
-        v
-end
-
-let () = AnalysisGlobalState.register_ref Constants.cache ~init:(fun () -> Constants.initial_cache)
-
-let absval_of_int formula i = Constants.get_int formula i
+let absval_of_int formula i =
+  match Formula.get_term_eq formula.phi (Term.of_intlit i) with
+  | Some v ->
+      (formula, v)
+  | None ->
+      let assert_sat = function Sat x -> x | Unsat -> assert false in
+      let v = Var.mk_fresh () in
+      let formula =
+        and_equal (AbstractValueOperand v) (ConstOperand (Cint i)) formula |> assert_sat |> fst
+      in
+      (formula, v)

infer/src/pulse/PulseFormula.mli

@@ -126,7 +126,7 @@ val and_callee_formula :
 val fold_variables : (t, Var.t, 'acc) Container.fold
 (** note: each variable mentioned in the formula is visited at least once, possibly more *)
 
-val absval_of_int : t -> IntLit.t -> Var.t
+val absval_of_int : t -> IntLit.t -> t * Var.t
 (** Get or create an abstract value ([Var.t] is [AbstractValue.t]) associated with a constant
     {!IR.IntLit.t}. The idea is that clients will record in the abstract state that the returned [t]
     is equal to the given integer. If the same integer is queried later on then this module will

infer/src/pulse/PulseLoadInstrModels.ml

@@ -22,13 +22,11 @@ type model =
 let std_is_same_v t1 t2 : model =
  fun {path; location} astate ->
   if Typ.equal_template_arg t1 t2 then
-    let one = Formula.absval_of_int astate.AbductiveDomain.path_condition IntLit.one in
-    let++ astate = PulseArithmetic.and_eq_int one IntLit.one astate in
-    (astate, (one, Hist.single_call path location "std_is_same_v is true"))
+    let astate, one = PulseArithmetic.absval_of_int astate IntLit.one in
+    Sat (Ok (astate, (one, Hist.single_call path location "std_is_same_v is true")))
   else
-    let zero = Formula.absval_of_int astate.AbductiveDomain.path_condition IntLit.zero in
-    let++ astate = PulseArithmetic.and_eq_int zero IntLit.zero astate in
-    (astate, (zero, Hist.single_call path location "std_is_same_v is false"))
+    let astate, zero = PulseArithmetic.absval_of_int astate IntLit.zero in
+    Sat (Ok (astate, (zero, Hist.single_call path location "std_is_same_v is false")))
 
 
 let dispatch ~load:load_exp =

infer/src/pulse/PulseModelsImport.ml

@@ -159,9 +159,9 @@ module Basic = struct
   let return_int ~desc : Int64.t -> model =
    fun i64 {path; location; ret= ret_id, _} astate ->
     let i = IntLit.of_int64 i64 in
-    let ret_addr = Formula.absval_of_int astate.AbductiveDomain.path_condition i in
-    let<++> astate = PulseArithmetic.and_eq_int ret_addr i astate in
+    let astate, ret_addr = PulseArithmetic.absval_of_int astate i in
     PulseOperations.write_id ret_id (ret_addr, Hist.single_call path location desc) astate
+    |> ok_continue
 
 
   let return_positive ~desc : model =

infer/src/pulse/PulseOperations.ml

@@ -246,18 +246,17 @@ and eval_to_value_origin (path : PathContext.t) mode location exp astate :
   | Cast (_, exp') ->
       eval_to_value_origin path mode location exp' astate
   | Const (Cint i) ->
-      let v = Formula.absval_of_int astate.AbductiveDomain.path_condition i in
+      let astate, v = PulseArithmetic.absval_of_int astate i in
       let invalidation = Invalidation.ConstantDereference i in
-      let++ astate =
-        PulseArithmetic.and_eq_int v i astate
-        >>|| AddressAttributes.invalidate
-               (v, ValueHistory.singleton (Assignment (location, path.timestamp)))
-               invalidation location
+      let astate =
+        AddressAttributes.invalidate
+          (v, ValueHistory.singleton (Assignment (location, path.timestamp)))
+          invalidation location astate
       in
       let addr_hist =
         (v, ValueHistory.singleton (Invalidated (invalidation, location, path.timestamp)))
       in
-      (astate, ValueOrigin.Unknown addr_hist)
+      Sat (Ok (astate, ValueOrigin.Unknown addr_hist))
   | Const (Cstr s) ->
       (* TODO: record actual string value; since we are making strings be a record in memory
          instead of pure values some care has to be added to access string values once written *)