From d8242083a81fb099983e78273a1d0625aa198826 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 6 Nov 2023 05:37:03 -0800 Subject: [PATCH] [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 | 6 +++++ infer/src/pulse/PulseArithmetic.mli | 2 ++ infer/src/pulse/PulseFormula.ml | 31 +++++++++---------------- infer/src/pulse/PulseFormula.mli | 2 +- infer/src/pulse/PulseLoadInstrModels.ml | 10 ++++---- infer/src/pulse/PulseModelsImport.ml | 4 ++-- infer/src/pulse/PulseOperations.ml | 13 +++++------ 7 files changed, 32 insertions(+), 36 deletions(-) diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml index 66a65d7dd94..315aef3d09a 100644 --- a/infer/src/pulse/PulseArithmetic.ml +++ b/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) diff --git a/infer/src/pulse/PulseArithmetic.mli b/infer/src/pulse/PulseArithmetic.mli index b3b83f70286..59c00f25d99 100644 --- a/infer/src/pulse/PulseArithmetic.mli +++ b/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 diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index b34d44e26fd..992cb82bb72 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/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) diff --git a/infer/src/pulse/PulseFormula.mli b/infer/src/pulse/PulseFormula.mli index 7a3608da360..4b76de8e096 100644 --- a/infer/src/pulse/PulseFormula.mli +++ b/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 diff --git a/infer/src/pulse/PulseLoadInstrModels.ml b/infer/src/pulse/PulseLoadInstrModels.ml index 964798f09de..a51f075727e 100644 --- a/infer/src/pulse/PulseLoadInstrModels.ml +++ b/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 = diff --git a/infer/src/pulse/PulseModelsImport.ml b/infer/src/pulse/PulseModelsImport.ml index 0b3c4b786e6..486d06ea040 100644 --- a/infer/src/pulse/PulseModelsImport.ml +++ b/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 = diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index f309cd6e42f..2726474ea83 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/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 *)