[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

@@ -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
 

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

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

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

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