From 02d6b99a2d3f8f009e3197f517cf3879f17a1471 Mon Sep 17 00:00:00 2001 From: David Pichardie Date: Fri, 29 Sep 2023 02:32:00 -0700 Subject: [PATCH] [pulse][java] rewriting Java Integer models using the new DSL Summary: this is a good exercice for this young DSL. I may have changed the behavior of the old model because I use less indirections, but I don't see regressions. Reviewed By: skcho Differential Revision: D49732629 Privacy Context Container: L1208441 fbshipit-source-id: 989ff51168c42518bc78de5d323b26fb36d98a5d --- infer/src/pulse/PulseModelsDSL.ml | 12 ++++++ infer/src/pulse/PulseModelsDSL.mli | 2 + infer/src/pulse/PulseModelsImport.ml | 3 -- infer/src/pulse/PulseModelsImport.mli | 2 - infer/src/pulse/PulseModelsJava.ml | 55 +++++++++------------------ 5 files changed, 33 insertions(+), 41 deletions(-) diff --git a/infer/src/pulse/PulseModelsDSL.ml b/infer/src/pulse/PulseModelsDSL.ml index bc2e62554d7..dfa282cdc05 100644 --- a/infer/src/pulse/PulseModelsDSL.ml +++ b/infer/src/pulse/PulseModelsDSL.ml @@ -233,6 +233,18 @@ module Syntax = struct let aval_operand (addr, _) = PulseArithmetic.AbstractValueOperand addr + let eval_binop binop (addr1, hist1) (addr2, hist2) : aval model_monad = + let* {path} = get_data in + let addr_res = AbstractValue.mk_fresh () in + let hist_res = Hist.binop path binop hist1 hist2 in + let* addr_res = + PulseArithmetic.eval_binop addr_res binop (AbstractValueOperand addr1) + (AbstractValueOperand addr2) + |> exec_partial_operation + in + ret (addr_res, hist_res) + + let prune_binop ~negated binop operand1 operand2 = PulseArithmetic.prune_binop ~negated binop operand1 operand2 |> exec_partial_command diff --git a/infer/src/pulse/PulseModelsDSL.mli b/infer/src/pulse/PulseModelsDSL.mli index 5cfd75e99f1..0484c7a29a6 100644 --- a/infer/src/pulse/PulseModelsDSL.mli +++ b/infer/src/pulse/PulseModelsDSL.mli @@ -66,6 +66,8 @@ module Syntax : sig val deep_copy : ?depth_max:int -> aval -> aval model_monad + val eval_binop : Binop.t -> aval -> aval -> aval model_monad + val eval_read : Exp.t -> aval model_monad val eval_deref_access : access_mode -> aval -> Access.t -> aval model_monad diff --git a/infer/src/pulse/PulseModelsImport.ml b/infer/src/pulse/PulseModelsImport.ml index b7dc4657a3a..09e94648bfe 100644 --- a/infer/src/pulse/PulseModelsImport.ml +++ b/infer/src/pulse/PulseModelsImport.ml @@ -73,9 +73,6 @@ module Hist = struct let binop path bop hist1 hist2 = ValueHistory.in_context path.PathContext.conditions (ValueHistory.binary_op bop hist1 hist2) - - - let hist path hist = ValueHistory.in_context path.PathContext.conditions hist end module Basic = struct diff --git a/infer/src/pulse/PulseModelsImport.mli b/infer/src/pulse/PulseModelsImport.mli index 1a9c7ffbdc8..daffb5c60b4 100644 --- a/infer/src/pulse/PulseModelsImport.mli +++ b/infer/src/pulse/PulseModelsImport.mli @@ -70,8 +70,6 @@ module Hist : sig val single_alloc : PathContext.t -> Location.t -> ?more:string -> string -> ValueHistory.t val binop : PathContext.t -> Binop.t -> ValueHistory.t -> ValueHistory.t -> ValueHistory.t - - val hist : PathContext.t -> ValueHistory.t -> ValueHistory.t end module Basic : sig diff --git a/infer/src/pulse/PulseModelsJava.ml b/infer/src/pulse/PulseModelsJava.ml index c7b30511dc1..48f9a9a7707 100644 --- a/infer/src/pulse/PulseModelsJava.ml +++ b/infer/src/pulse/PulseModelsJava.ml @@ -10,6 +10,7 @@ open PulseBasicInterface open PulseDomainInterface open PulseOperationResult.Import open PulseModelsImport +module DSL = PulseModelsDSL module Cplusplus = PulseModelsCpp module GenericArrayBackedCollection = PulseModelsGenericArrayBackedCollection module StringSet = Caml.Set.Make (String) @@ -529,51 +530,33 @@ end module Integer = struct let internal_int = mk_java_field "java.lang" "Integer" "__infer_model_backing_int" - let load_backing_int path location this astate = - let* astate, obj = PulseOperations.eval_access path Read location this Dereference astate in - load_field path internal_int location obj astate - - - let construct path this_address init_value event location astate = - let this = (AbstractValue.mk_fresh (), Hist.single_event path event) in - let* astate, int_field = - PulseOperations.eval_access path Write location this (FieldAccess internal_int) astate - in - let* astate = PulseOperations.write_deref path location ~ref:int_field ~obj:init_value astate in - PulseOperations.write_deref path location ~ref:this_address ~obj:this astate - - - let init this_address init_value : model = - fun {path; location} astate -> - let event = Hist.call_event path location "Integer.init" in - let<+> astate = construct path this_address init_value event location astate in - astate + let init this init_value : model = + let open DSL.Syntax in + start_model @@ write_deref_field ~ref:this internal_int ~obj:init_value let equals this arg : model = - fun {path; location; ret= ret_id, _} astate -> - let<*> astate, _int_addr1, (int1, hist1) = load_backing_int path location this astate in - let<*> astate, _int_addr2, (int2, hist2) = load_backing_int path location arg astate in - let binop_addr = AbstractValue.mk_fresh () in - let<++> astate, binop_addr = - PulseArithmetic.eval_binop binop_addr Eq (AbstractValueOperand int1) - (AbstractValueOperand int2) astate - in - PulseOperations.write_id ret_id (binop_addr, Hist.binop path Eq hist1 hist2) astate + let open DSL.Syntax in + start_model + @@ let* this_int = eval_deref_access Read this (FieldAccess internal_int) in + let* arg_int = eval_deref_access Read arg (FieldAccess internal_int) in + let* res = eval_binop Eq this_int arg_int in + assign_ret res let int_val this : model = - fun {path; location; ret= ret_id, _} astate -> - let<*> astate, _int_addr1, (int_value, hist) = load_backing_int path location this astate in - PulseOperations.write_id ret_id (int_value, Hist.hist path hist) astate |> Basic.ok_continue + let open DSL.Syntax in + start_model + @@ let* this_int = eval_deref_access Read this (FieldAccess internal_int) in + assign_ret this_int let value_of init_value : model = - fun {path; location; ret= ret_id, _} astate -> - let event = Hist.call_event path location "Integer.valueOf" in - let new_alloc = (AbstractValue.mk_fresh (), Hist.single_event path event) in - let<+> astate = construct path new_alloc init_value event location astate in - PulseOperations.write_id ret_id new_alloc astate + let open DSL.Syntax in + start_model + @@ let* res = mk_fresh ~model_desc:"Integer.valueOf" in + let* () = lift_to_monad (init res init_value) in + assign_ret res end module Preconditions = struct