[pulse] Adding IsInstanceOf predicate

Summary:
As a first step to support the Java `instanceof`
operator, this change allows the path condition to be appended with
`IsInstanceOf(var, typ)`.

Reviewed By: jvillard

Differential Revision: D26664009

fbshipit-source-id: cd19dce83

infer/src/pulse/PulseArithmetic.ml

@@ -58,3 +58,7 @@ let is_unsat_cheap astate = PathCondition.is_unsat_cheap astate.AbductiveDomain.
 
 let has_no_assumptions astate =
   PathCondition.has_no_assumptions astate.AbductiveDomain.path_condition
+
+
+let and_equal_instanceof v1 v2 t astate =
+  map_path_condition astate ~f:(fun phi -> PathCondition.and_eq_instanceof v1 v2 t phi)

infer/src/pulse/PulseArithmetic.mli

@@ -41,3 +41,6 @@ val is_known_zero : AbductiveDomain.t -> AbstractValue.t -> bool
 val is_unsat_cheap : AbductiveDomain.t -> bool
 
 val has_no_assumptions : AbductiveDomain.t -> bool
+
+val and_equal_instanceof :
+  AbstractValue.t -> AbstractValue.t -> Typ.t -> AbductiveDomain.t -> AbductiveDomain.t

infer/src/pulse/PulseFormula.ml

@@ -239,6 +239,7 @@ module Term = struct
     | BitShiftLeft of t * t
     | BitShiftRight of t * t
     | BitXor of t * t
+    | IsInstanceOf of Var.t * Typ.t
   [@@deriving compare, equal, yojson_of]
 
   let equal_syntax = [%compare.equal: t]
@@ -270,7 +271,8 @@ module Term = struct
     | LessThan _
     | LessEqual _
     | Equal _
-    | NotEqual _ ->
+    | NotEqual _
+    | IsInstanceOf _ ->
         true
 
 
@@ -325,6 +327,8 @@ module Term = struct
         F.fprintf fmt "%a=%a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) t2
     | NotEqual (t1, t2) ->
         F.fprintf fmt "%a≠%a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) t2
+    | IsInstanceOf (v, t) ->
+        F.fprintf fmt "%a instanceof %a" pp_var v (Typ.pp Pp.text) t
 
 
   let of_q q = Const q
@@ -395,7 +399,7 @@ module Term = struct
   (** Fold [f] on the strict sub-terms of [t], if any. Preserve physical equality if [f] does. *)
   let fold_map_direct_subterms t ~init ~f =
     match t with
-    | Var _ | Const _ | Linear _ ->
+    | Var _ | Const _ | Linear _ | IsInstanceOf _ ->
         (init, t)
     | Minus t_not | BitNot t_not | Not t_not ->
         let acc, t_not' = f init t_not in
@@ -476,11 +480,39 @@ module Term = struct
         let acc, op = f init v in
         let t' = match op with VarSubst v' when Var.equal v v' -> t | _ -> of_subst_target op in
         (acc, t')
+    | IsInstanceOf (v, typ) ->
+        let acc, op = f init v in
+        let t' =
+          match op with
+          | VarSubst v' when not (Var.equal v v') ->
+              IsInstanceOf (v', typ)
+          | QSubst _ | VarSubst _ | LinSubst _ ->
+              t
+        in
+        (acc, t')
     | Linear l ->
         let acc, l' = LinArith.fold_subst_variables l ~init ~f in
         let t' = if phys_equal l l' then t else Linear l' in
         (acc, t')
-    | _ ->
+    | Const _
+    | Add _
+    | Minus _
+    | LessThan _
+    | LessEqual _
+    | Equal _
+    | NotEqual _
+    | Mult _
+    | Div _
+    | And _
+    | Or _
+    | Not _
+    | Mod _
+    | BitAnd _
+    | BitOr _
+    | BitNot _
+    | BitShiftLeft _
+    | BitShiftRight _
+    | BitXor _ ->
         fold_map_direct_subterms t ~init ~f:(fun acc t' -> fold_subst_variables t' ~init:acc ~f)
 
 
@@ -515,7 +547,7 @@ module Term = struct
     let map_z_z = conv2 Q.to_bigint Q.to_bigint Q.of_bigint in
     let or_undef q_opt = Option.value ~default:Q.undef q_opt in
     match t0 with
-    | Const _ | Var _ ->
+    | Const _ | Var _ | IsInstanceOf _ ->
         t0
     | Linear l ->
         LinArith.get_as_const l |> Option.value_map ~default:t0 ~f:(fun c -> Const c)
@@ -682,7 +714,8 @@ module Term = struct
       | LessThan _
       | LessEqual _
       | Equal _
-      | NotEqual _ ->
+      | NotEqual _
+      | IsInstanceOf _ ->
           None
     in
     match aux_linearize t with None -> t | Some l -> Linear l
@@ -1305,6 +1338,11 @@ let and_mk_atom mk_atom op1 op2 phi =
 
 let and_equal = and_mk_atom Atom.equal
 
+let and_equal_instanceof v1 v2 t phi =
+  let atom = Atom.equal (Var v1) (IsInstanceOf (v2, t)) in
+  and_known_atom atom phi
+
+
 let and_less_equal = and_mk_atom Atom.less_equal
 
 let and_less_than = and_mk_atom Atom.less_than

infer/src/pulse/PulseFormula.mli

@@ -39,6 +39,8 @@ val ttrue : t
 
 val and_equal : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
 
+val and_equal_instanceof : Var.t -> Var.t -> Typ.t -> t -> (t * new_eqs) SatUnsat.t
+
 val and_less_equal : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
 
 val and_less_than : operand -> operand -> t -> (t * new_eqs) SatUnsat.t

infer/src/pulse/PulseModels.ml

@@ -911,14 +911,21 @@ module StdVector = struct
 end
 
 module Java = struct
-  let instance_of (argv, hist) _ : model =
+  let instance_of (argv, hist) typeexpr : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model "Java.instanceof"; location; in_call= []} in
     let res_addr = AbstractValue.mk_fresh () in
-    PulseArithmetic.prune_positive argv astate
-    |> PulseArithmetic.and_eq_int res_addr IntLit.one
-    |> PulseOperations.write_id ret_id (res_addr, event :: hist)
-    |> ok_continue
+    match typeexpr with
+    | Exp.Sizeof {typ} ->
+        PulseArithmetic.and_equal_instanceof res_addr argv typ astate
+        |> PulseArithmetic.prune_positive argv
+        |> PulseArithmetic.and_eq_int res_addr IntLit.one
+        |> PulseOperations.write_id ret_id (res_addr, event :: hist)
+        |> ok_continue
+    (* The type expr is sometimes a Var expr but this is not expected.
+       This seems to be introduced by inline mechanism of Java synthetic methods during preanalysis *)
+    | _ ->
+        astate |> ok_continue
 end
 
 module JavaCollection = struct

infer/src/pulse/PulsePathCondition.ml

@@ -400,6 +400,12 @@ let prune_binop ~negated bop lhs_op rhs_op ({is_unsat; bo_itvs= _; citvs; formul
             ({phi with is_unsat; formula}, new_eqs) )
 
 
+let and_eq_instanceof v1 v2 t phi =
+  let+ {is_unsat; bo_itvs; citvs; formula} = phi in
+  let+| formula, new_eqs = Formula.and_equal_instanceof v1 v2 t formula in
+  ({is_unsat; bo_itvs; citvs; formula}, new_eqs)
+
+
 (** {2 Queries} *)
 
 let is_known_zero phi v =

infer/src/pulse/PulsePathCondition.mli

@@ -57,6 +57,8 @@ val eval_unop : AbstractValue.t -> Unop.t -> AbstractValue.t -> t -> t * new_eqs
 
 val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> t * new_eqs
 
+val and_eq_instanceof : AbstractValue.t -> AbstractValue.t -> Typ.t -> t -> t * new_eqs
+
 (** {2 Queries} *)
 
 val is_known_zero : t -> AbstractValue.t -> bool