[pulse] detect contradictions on non-integer integer values

Summary:
A known weakness of the arithmetic engine in Pulse is that it treats
values as rationals instead of integers. This mitigates this weakness by
introducing an `is_int()` predicate that gets added on each load and
store of/to a known-integer value. The only rule currently implemented
for it is that `is_int(e)` is `true` if `e` is a known integer literal,
and `false` (contradiction) if `e` is a known non-integer literal.

Reviewed By: da319

Differential Revision: D31932970

fbshipit-source-id: c92cae436

Author: jvillard

infer/src/pulse/Pulse.ml

@@ -290,6 +290,10 @@ module PulseTransferFunctions = struct
     (astates, ret_vars)
 
 
+  let and_is_int_if_integer_type typ v astate =
+    if Typ.is_int typ then PulseArithmetic.and_is_int v astate else Ok astate
+
+
   let exec_instr_aux ({PathContext.timestamp} as path) (astate : ExecutionDomain.t)
       (astate_n : NonDisjDomain.t)
       ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) _cfg_node
@@ -302,18 +306,20 @@ module PulseTransferFunctions = struct
         ([astate], path, astate_n)
     | ContinueProgram astate -> (
       match instr with
-      | Load {id= lhs_id; e= rhs_exp; loc} ->
+      | Load {id= lhs_id; e= rhs_exp; loc; typ} ->
           (* [lhs_id := *rhs_exp] *)
           let deref_rhs astate =
             let results =
               if Config.pulse_isl then
                 PulseOperations.eval_deref_isl path loc rhs_exp astate
                 |> List.map ~f:(fun result ->
-                       let+ astate, rhs_addr_hist = result in
-                       PulseOperations.write_id lhs_id rhs_addr_hist astate )
+                       let* astate, rhs_addr_hist = result in
+                       and_is_int_if_integer_type typ (fst rhs_addr_hist) astate
+                       >>| PulseOperations.write_id lhs_id rhs_addr_hist )
               else
-                [ (let+ astate, rhs_addr_hist = PulseOperations.eval_deref path loc rhs_exp astate in
-                   PulseOperations.write_id lhs_id rhs_addr_hist astate ) ]
+                [ (let* astate, rhs_addr_hist = PulseOperations.eval_deref path loc rhs_exp astate in
+                   and_is_int_if_integer_type typ (fst rhs_addr_hist) astate
+                   >>| PulseOperations.write_id lhs_id rhs_addr_hist ) ]
             in
             PulseReport.report_results tenv proc_desc err_log loc results
           in
@@ -347,7 +353,7 @@ module PulseTransferFunctions = struct
                 [astate]
           in
           (List.concat_map set_global_astates ~f:deref_rhs, path, astate_n)
-      | Store {e1= lhs_exp; e2= rhs_exp; loc} ->
+      | Store {e1= lhs_exp; e2= rhs_exp; loc; typ} ->
           (* [*lhs_exp := rhs_exp] *)
           let event =
             match lhs_exp with
@@ -379,6 +385,7 @@ module PulseTransferFunctions = struct
             let astates =
               List.concat_map ls_astate_lhs_addr_hist ~f:(fun result ->
                   let<*> astate, lhs_addr_hist = result in
+                  let<*> astate = and_is_int_if_integer_type typ rhs_addr astate in
                   write_function lhs_addr_hist astate )
             in
             let astates =

infer/src/pulse/PulseArithmetic.ml

@@ -78,5 +78,7 @@ let has_no_assumptions astate =
   PathCondition.has_no_assumptions astate.AbductiveDomain.path_condition
 
 
+let and_is_int v astate = map_path_condition astate ~f:(fun phi -> PathCondition.and_is_int v phi)
+
 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

@@ -61,6 +61,8 @@ val is_unsat_cheap : AbductiveDomain.t -> bool
 
 val has_no_assumptions : AbductiveDomain.t -> bool
 
+val and_is_int : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t AccessResult.t
+
 val and_equal_instanceof :
      AbstractValue.t
   -> AbstractValue.t

infer/src/pulse/PulseFormula.ml

@@ -249,6 +249,7 @@ module Term = struct
     | BitShiftRight of t * t
     | BitXor of t * t
     | IsInstanceOf of Var.t * Typ.t
+    | IsInt of t
   [@@deriving compare, equal, yojson_of]
 
   let equal_syntax = [%compare.equal: t]
@@ -285,7 +286,8 @@ module Term = struct
     | LessEqual _
     | Equal _
     | NotEqual _
-    | IsInstanceOf _ ->
+    | IsInstanceOf _
+    | IsInt _ ->
         true
 
 
@@ -348,6 +350,8 @@ module Term = struct
         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
+    | IsInt t ->
+        F.fprintf fmt "is_int(%a)" (pp_no_paren pp_var) t
 
 
   let of_q q = Const q
@@ -437,18 +441,20 @@ module Term = struct
         let t' = if !changed then FunctionApplication {f= t_f'; actuals= actuals'} else t in
         (acc, t')
     (* one sub-term *)
-    | Minus t_not | BitNot t_not | Not t_not ->
-        let acc, t_not' = f init t_not in
+    | Minus sub_t | BitNot sub_t | Not sub_t | IsInt sub_t ->
+        let acc, sub_t' = f init sub_t in
         let t' =
-          if phys_equal t_not t_not' then t
+          if phys_equal sub_t sub_t' then t
           else
             match[@warning "-8"] t with
             | Minus _ ->
-                Minus t_not'
+                Minus sub_t'
             | BitNot _ ->
-                BitNot t_not'
+                BitNot sub_t'
             | Not _ ->
-                Not t_not'
+                Not sub_t'
+            | IsInt _ ->
+                IsInt sub_t'
         in
         (acc, t')
     (* two sub-terms *)
@@ -564,7 +570,8 @@ module Term = struct
     | BitNot _
     | BitShiftLeft _
     | BitShiftRight _
-    | BitXor _ ->
+    | BitXor _
+    | IsInt _ ->
         fold_map_direct_subterms t ~init ~f:(fun acc t' -> fold_subst_variables t' ~init:acc ~f)
 
 
@@ -605,6 +612,13 @@ module Term = struct
         t0
     | Linear l ->
         LinArith.get_as_const l |> Option.value_map ~default:t0 ~f:(fun c -> Const c)
+    | IsInt t' ->
+        q_map t' (fun q ->
+            if Z.(equal one) (Q.den q) then (* an integer *) Q.one
+            else (
+              (* a non-integer rational *)
+              L.d_printfln ~color:Orange "CONTRADICTION: is_int(%a)" Q.pp_print q ;
+              Q.zero ) )
     | Minus t' ->
         q_map t' Q.(mul minus_one)
     | Add (t1, t2) ->
@@ -812,7 +826,8 @@ module Term = struct
       | LessEqual _
       | Equal _
       | NotEqual _
-      | IsInstanceOf _ ->
+      | IsInstanceOf _
+      | IsInt _ ->
           None
     in
     match aux_linearize t with
@@ -1636,6 +1651,11 @@ let and_equal_instanceof v1 v2 t phi =
   and_known_atom atom phi
 
 
+let and_is_int v phi =
+  let atom = Atom.equal (IsInt (Var v)) Term.one 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

@@ -56,6 +56,8 @@ val and_equal_unop : Var.t -> Unop.t -> operand -> t -> (t * new_eqs) SatUnsat.t
 
 val and_equal_binop : Var.t -> Binop.t -> operand -> operand -> t -> (t * new_eqs) SatUnsat.t
 
+val and_is_int : Var.t -> t -> (t * new_eqs) SatUnsat.t
+
 val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> (t * new_eqs) SatUnsat.t
 
 (** {3 Operations} *)

infer/src/pulse/PulseOperations.ml

@@ -272,7 +272,7 @@ let eval path mode location exp0 astate =
             (AbstractValueOperand addr_rhs) astate
         in
         (astate, (binop_addr, ValueHistory.Branching [hist_lhs; hist_rhs]))
-    | Const _ | Sizeof _ | Exn _ ->
+    | Const (Cfloat _ | Cclass _) | Sizeof _ | Exn _ ->
         Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) ValueHistory.Epoch))
   in
   eval path mode exp0 astate

infer/src/pulse/PulsePathCondition.ml

@@ -417,6 +417,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_is_int v phi =
+  let+ {is_unsat; bo_itvs; citvs; formula} = phi in
+  let+| formula, new_eqs = Formula.and_is_int v formula in
+  ({is_unsat; bo_itvs; citvs; 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

infer/src/pulse/PulsePathCondition.mli

@@ -67,6 +67,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_is_int : AbstractValue.t -> t -> t * new_eqs
+
 val and_eq_instanceof : AbstractValue.t -> AbstractValue.t -> Typ.t -> t -> t * new_eqs
 
 (** {2 Queries} *)

infer/src/pulse/unit/PulseFormulaTest.ml

@@ -49,6 +49,11 @@ let instanceof typ x_var y_var phi =
   phi
 
 
+let is_int x phi =
+  let+ phi, _new_eqs = and_is_int x phi in
+  phi
+
+
 let ( + ) f1 f2 phi = of_binop (PlusA None) f1 f2 phi
 
 let ( - ) f1 f2 phi = of_binop (MinusA None) f1 f2 phi
@@ -272,6 +277,32 @@ let%test_module "normalization" =
              -1=v7∧0=v8∧1=w∧3=v∧12=z∧[-v6 -1]=x∧[1/3·v6]=y
              &&
              true (no atoms)|}]
+
+    (* expected: [is_int(x)] and [is_int(y)] get simplified away, [is_int(z)] is kept around *)
+    let%expect_test _ =
+      normalize
+        (is_int x_var && x + x = i 4 && is_int y_var && y = i (-42) && is_int z_var && z = x + w) ;
+      [%expect
+        {|
+        known=z=v7
+              &&
+              x = 2 ∧ y = -42 ∧ z = w +2 ∧ v6 = 4
+              &&
+              -42=y∧2=x∧4=v6∧[w +2]=z
+              &&
+              {is_int([z]) = 1},
+        pruned=true (no atoms),
+        both=z=v7
+             &&
+             x = 2 ∧ y = -42 ∧ z = w +2 ∧ v6 = 4
+             &&
+             -42=y∧2=x∧4=v6∧[w +2]=z
+             &&
+             {is_int([z]) = 1}|}]
+
+    let%expect_test _ =
+      normalize (is_int x_var && x + x = i 5) ;
+      [%expect {|unsat|}]
   end )
 
 let%test_module "variable elimination" =

infer/tests/codetoanalyze/c/pulse/integers.c

@@ -0,0 +1,58 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+#include <stdlib.h>
+
+void even_cannot_be_odd_local_ok(int y) {
+  int x = y;
+  if (x + x == 5) {
+    int* p = NULL;
+    *p = 42;
+  }
+}
+
+void even_cannot_be_odd_parameter_ok(int x) {
+  if (x + x == 5) {
+    int* p = NULL;
+    *p = 42;
+  }
+}
+
+void even_cannot_be_odd_float_conv_FP() {
+  int x = random();
+  // two causes here: 1) Pulse represents floats as arbitrary values
+  // and 2) the int conversion is omitted by the frontend
+  if (x + x == (int)5.5) {
+    int* p = NULL;
+    *p = 42;
+  }
+}
+
+void int_conversions_feasible_bad() {
+  int x = random();
+  int y = 3 / 2;
+  int z = (int)1.234;
+  int w = x / 2;
+  if (w == 5 && x == 10 && y == 1 && z == 1) {
+    int* p = NULL;
+    *p = 42;
+  }
+}
+
+struct s {
+  int i;
+  int j;
+};
+
+void FPlatent_even_cannot_be_odd_fields_ok(struct s* x) {
+  if (x->i + x->i == 5 || x->i + x->i + x->j + x->j == 5) {
+    // latent issue is FP: arithmetic does not know 2x + 2y == 5 is impossible
+    // when x and y are ints
+    int* p = NULL;
+    *p = 42;
+  }
+}