DSL iterators

Reviewed By: davidpichardie

Differential Revision: D47673643

fbshipit-source-id: 962d023e1aec29d5142519eeb36c46ae20913d6b

infer/lib/hack/models.sil

@@ -54,18 +54,6 @@ define $builtins.hack_make_random_bool(): *HackBool {
     ret $builtins.hack_bool($builtins.nondet())
 }
 
-define $builtins.hack_is_true(b: *HackMixed) : int {
-  #entry:
-    n0: *HackMixed = load &b
-    if __sil_eq(n0, 0) then ret 0
-      // this is not a boxed boolean (always non null) so the test is b!=null
-    else if __sil_instanceof(n0, <HackBool>) then jmp is_bool
-    else ret 1
-  #is_bool:
-    n1: int = load n0.HackBool.val
-    ret n1
-}
-
 define $builtins.hhbc_cmp_eq(x: *HackMixed, y: *HackMixed) : *HackBool {
   // TODO: we need a better model for polymorphic equality. The current one is null-safe and works
   // for ints but otherwise is questionable when applied to some random types

infer/src/pulse/PulseModelsDSL.ml

@@ -188,6 +188,21 @@ module Syntax = struct
     ret res data astate
 
 
+  let and_eq_int (size_addr, _) i : unit model_monad =
+    PulseArithmetic.and_eq_int size_addr i |> exec_partial_command
+
+
+  (* and_eq v and_equal inconsistent naming *)
+  let and_eq (x, _) (y, _) : unit model_monad =
+    PulseArithmetic.and_equal (PulseArithmetic.AbstractValueOperand x)
+      (PulseArithmetic.AbstractValueOperand y)
+    |> exec_partial_command
+
+
+  let and_positive (addr, _) : unit model_monad =
+    PulseArithmetic.and_positive addr |> exec_partial_command
+
+
   let add_static_type typ_name (addr, _) : unit model_monad =
    fun ({analysis_data= {tenv}} as data) astate ->
     let astate = AbductiveDomain.AddressAttributes.add_static_type tenv typ_name addr astate in
@@ -231,6 +246,11 @@ module Syntax = struct
     PulseOperations.write_deref_field path location ~ref ~obj field >> sat |> exec_partial_command
 
 
+  let write_deref ~ref ~obj : unit model_monad =
+    let* {path; location} = get_data in
+    PulseOperations.write_deref path location ~ref ~obj >> sat |> exec_partial_command
+
+
   let deep_copy ?depth_max source : aval model_monad =
     let* {path; location} = get_data in
     PulseOperations.deep_copy ?depth_max path location source >> sat |> exec_partial_operation
@@ -250,6 +270,16 @@ module Syntax = struct
     ret (addr_res, hist_res)
 
 
+  let eval_binop_int binop (arg, hist) i : aval model_monad =
+    let addr_res = AbstractValue.mk_fresh () in
+    let* addr_res =
+      PulseArithmetic.eval_binop addr_res binop (AbstractValueOperand arg)
+        (PulseArithmetic.ConstOperand (Cint i))
+      |> exec_partial_operation
+    in
+    ret (addr_res, hist)
+
+
   let prune_binop ~negated binop operand1 operand2 =
     PulseArithmetic.prune_binop ~negated binop operand1 operand2 |> exec_partial_command
 
@@ -274,6 +304,22 @@ module Syntax = struct
     prune_binop ~negated:false Binop.Lt (aval_operand arg1) (aval_operand arg2)
 
 
+  let prune_lt_int arg1 i : unit model_monad =
+    prune_binop ~negated:false Binop.Lt (aval_operand arg1) (PulseArithmetic.ConstOperand (Cint i))
+
+
+  let prune_ge arg1 arg2 : unit model_monad =
+    prune_binop ~negated:true Binop.Lt (aval_operand arg1) (aval_operand arg2)
+
+
+  let prune_ge_int arg1 i : unit model_monad =
+    prune_binop ~negated:true Binop.Lt (aval_operand arg1) (PulseArithmetic.ConstOperand (Cint i))
+
+
+  let prune_gt arg1 arg2 = prune_lt arg2 arg1
+
+  let prune_le arg1 arg2 = prune_ge arg2 arg1
+
   let prune_eq arg1 arg2 : unit model_monad =
     prune_binop ~negated:false Binop.Eq (aval_operand arg1) (aval_operand arg2)
 

infer/src/pulse/PulseModelsDSL.mli

@@ -75,6 +75,8 @@ module Syntax : sig
 
   val eval_binop : Binop.t -> aval -> aval -> aval model_monad
 
+  val eval_binop_int : Binop.t -> aval -> IntLit.t -> aval model_monad
+
   val eval_read : Exp.t -> aval model_monad
 
   val eval_to_value_origin : Exp.t -> ValueOrigin.t model_monad
@@ -98,15 +100,33 @@ module Syntax : sig
 
   val prune_lt : aval -> aval -> unit model_monad
 
+  val prune_lt_int : aval -> IntLit.t -> unit model_monad
+
+  val prune_le : aval -> aval -> unit model_monad
+
+  val prune_gt : aval -> aval -> unit model_monad
+
+  val prune_ge : aval -> aval -> unit model_monad
+
+  val prune_ge_int : aval -> IntLit.t -> unit model_monad
+
   val prune_ne : aval -> aval -> unit model_monad
 
   val prune_ne_int : aval -> IntLit.t -> unit model_monad
 
   val prune_ne_zero : aval -> unit model_monad
 
+  val and_eq_int : aval -> IntLit.t -> unit model_monad
+
+  val and_eq : aval -> aval -> unit model_monad
+
+  val and_positive : aval -> unit model_monad
+
   (* Tenv operations *)
   val tenv_resolve_fieldname : Typ.name -> Fieldname.t -> Struct.field_info option model_monad
 
+  val write_deref : ref:aval -> obj:aval -> unit model_monad
+
   (* if necessary you can convert an operation outside of this module with the following operators *)
   val exec_command : (astate -> astate) -> unit model_monad