[frontend] Parse binary operator using types of parameters

Summary: It parses "+" (and "-") to PlusA and PlusPI (and MinusA, MinusPI, MinusPP) using types of parameters.

Reviewed By: mbouaziz

Differential Revision: D7443048

fbshipit-source-id: bd560c7

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -385,9 +385,9 @@ module Report = struct
         -> PO.ConditionSet.t -> PO.ConditionSet.t =
    fun pname ~bop ~e1 ~e2 location mem cond_set ->
     match bop with
-    | Binop.PlusA ->
+    | Binop.PlusPI ->
         check_binop_array_access pname ~is_plus:true ~e1 ~e2 location mem cond_set
-    | Binop.MinusA ->
+    | Binop.MinusPI ->
         check_binop_array_access pname ~is_plus:false ~e1 ~e2 location mem cond_set
     | _ ->
         cond_set

infer/src/clang/cArithmetic_trans.ml

@@ -16,16 +16,18 @@ module L = Logging
 (* CompoundAssignment. "binary_expression" is returned when we are calculating an expression*)
 (* "instructions" is not empty when the binary operator is actually a statement like an *)
 (* assignment. *)
-let compound_assignment_binary_operation_instruction boi_kind e1 typ e2 loc =
+let compound_assignment_binary_operation_instruction boi_kind (e1, t1) typ e2 loc =
   let id = Ident.create_fresh Ident.knormal in
   let instr1 = Sil.Load (id, e1, typ, loc) in
   let e_res, instr_op =
     match boi_kind with
     | `AddAssign ->
-        let e1_plus_e2 = Exp.BinOp (Binop.PlusA, Exp.Var id, e2) in
+        let bop = if Typ.is_pointer t1 then Binop.PlusPI else Binop.PlusA in
+        let e1_plus_e2 = Exp.BinOp (bop, Exp.Var id, e2) in
         (e1, [Sil.Store (e1, typ, e1_plus_e2, loc)])
     | `SubAssign ->
-        let e1_sub_e2 = Exp.BinOp (Binop.MinusA, Exp.Var id, e2) in
+        let bop = if Typ.is_pointer t1 then Binop.MinusPI else Binop.MinusA in
+        let e1_sub_e2 = Exp.BinOp (bop, Exp.Var id, e2) in
         (e1, [Sil.Store (e1, typ, e1_sub_e2, loc)])
     | `MulAssign ->
         let e1_mul_e2 = Exp.BinOp (Binop.Mult, Exp.Var id, e2) in
@@ -58,8 +60,10 @@ let compound_assignment_binary_operation_instruction boi_kind e1 typ e2 loc =
 (** Returns a pair ([binary_expression], instructions). "binary_expression" is returned when we are
    calculating an expression "instructions" is not empty when the binary operator is actually a
    statement like an assignment. *)
-let binary_operation_instruction source_range boi e1 typ e2 loc =
+let binary_operation_instruction source_range boi ((e1, t1) as e1_with_typ) typ (e2, t2) loc =
-  let binop_exp op = Exp.BinOp (op, e1, e2) in
+  let binop_exp ?(change_order= false) op =
+    if change_order then Exp.BinOp (op, e2, e1) else Exp.BinOp (op, e1, e2)
+  in
   match boi.Clang_ast_t.boi_kind with
   (* Note: Pointers to members that are not statically known are not
      expressible in Sil. The translation of the PtrMem ops treats the field as
@@ -72,7 +76,9 @@ let binary_operation_instruction source_range boi e1 typ e2 loc =
       let id = Ident.create_fresh Ident.knormal in
       (Exp.BinOp (PlusPI, Exp.Var id, e2), [Sil.Load (id, e1, typ, loc)])
   | `Add ->
-      (binop_exp Binop.PlusA, [])
+      if Typ.is_pointer t1 then (binop_exp Binop.PlusPI, [])
+      else if Typ.is_pointer t2 then (binop_exp ~change_order:true Binop.PlusPI, [])
+      else (binop_exp Binop.PlusA, [])
   | `Mul ->
       (binop_exp Binop.Mult, [])
   | `Div ->
@@ -80,7 +86,9 @@ let binary_operation_instruction source_range boi e1 typ e2 loc =
   | `Rem ->
       (binop_exp Binop.Mod, [])
   | `Sub ->
-      (binop_exp Binop.MinusA, [])
+      if Typ.is_pointer t1 then
+        if Typ.is_pointer t2 then (binop_exp Binop.MinusPP, []) else (binop_exp Binop.MinusPI, [])
+      else (binop_exp Binop.MinusA, [])
   | `Shl ->
       (binop_exp Binop.Shiftlt, [])
   | `Shr ->
@@ -124,7 +132,7 @@ let binary_operation_instruction source_range boi e1 typ e2 loc =
     | `AndAssign
     | `XorAssign
     | `OrAssign ) as boi_kind ->
-      compound_assignment_binary_operation_instruction boi_kind e1 typ e2 loc
+      compound_assignment_binary_operation_instruction boi_kind e1_with_typ typ e2 loc
 
 
 let unary_operation_instruction translation_unit_context uoi e typ loc =
@@ -133,12 +141,14 @@ let unary_operation_instruction translation_unit_context uoi e typ loc =
   | `PostInc ->
       let id = Ident.create_fresh Ident.knormal in
       let instr1 = Sil.Load (id, e, typ, loc) in
-      let e_plus_1 = Exp.BinOp (Binop.PlusA, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in
+      let bop = if Typ.is_pointer typ then Binop.PlusPI else Binop.PlusA in
+      let e_plus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in
       (Exp.Var id, [instr1; Sil.Store (e, typ, e_plus_1, loc)])
   | `PreInc ->
       let id = Ident.create_fresh Ident.knormal in
       let instr1 = Sil.Load (id, e, typ, loc) in
-      let e_plus_1 = Exp.BinOp (Binop.PlusA, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in
+      let bop = if Typ.is_pointer typ then Binop.PlusPI else Binop.PlusA in
+      let e_plus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in
       let exp =
         if CGeneral_utils.is_cpp_translation translation_unit_context then e else e_plus_1
       in
@@ -146,12 +156,14 @@ let unary_operation_instruction translation_unit_context uoi e typ loc =
   | `PostDec ->
       let id = Ident.create_fresh Ident.knormal in
       let instr1 = Sil.Load (id, e, typ, loc) in
-      let e_minus_1 = Exp.BinOp (Binop.MinusA, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in
+      let bop = if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA in
+      let e_minus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in
       (Exp.Var id, [instr1; Sil.Store (e, typ, e_minus_1, loc)])
   | `PreDec ->
       let id = Ident.create_fresh Ident.knormal in
       let instr1 = Sil.Load (id, e, typ, loc) in
-      let e_minus_1 = Exp.BinOp (Binop.MinusA, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in
+      let bop = if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA in
+      let e_minus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in
       let exp =
         if CGeneral_utils.is_cpp_translation translation_unit_context then e else e_minus_1
       in

infer/src/clang/cArithmetic_trans.mli

@@ -14,8 +14,8 @@ open! IStd
 val bin_op_to_string : Clang_ast_t.binary_operator_info -> string
 
 val binary_operation_instruction :
-  Clang_ast_t.source_range -> Clang_ast_t.binary_operator_info -> Exp.t -> Typ.t -> Exp.t
+  Clang_ast_t.source_range -> Clang_ast_t.binary_operator_info -> Exp.t * Typ.t -> Typ.t
-  -> Location.t -> Exp.t * Sil.instr list
+  -> Exp.t * Typ.t -> Location.t -> Exp.t * Sil.instr list
 (** Returns a pair ([binary_expression], instructions). "binary_expression" is returned when we are
    calculating an expression "instructions" is not empty when the binary operator is actually a
    statement like an assignment. *)

infer/src/clang/cTrans.ml

@@ -930,18 +930,18 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
         (* becomes the successor of the nodes that may be created when     *)
         (* translating the operands.                                       *)
         let res_trans_e1 = exec_with_self_exception instruction trans_state' s1 in
-        let var_exp, var_exp_typ =
+        let (var_exp, var_exp_typ) as e1_with_typ =
           extract_exp_from_list res_trans_e1.exps
             "@\nWARNING: Missing LHS operand in BinOp. Returning -1. Fix needed...@\n"
         in
-        let trans_state'' = {trans_state' with var_exp_typ= Some (var_exp, var_exp_typ)} in
+        let trans_state'' = {trans_state' with var_exp_typ= Some e1_with_typ} in
         let res_trans_e2 =
           (* translation of s2 is done taking care of block special case *)
           exec_with_block_priority_exception
             (exec_with_self_exception instruction)
             trans_state'' s2 stmt_info
         in
-        let sil_e2, _ =
+        let e2_with_typ =
           extract_exp_from_list res_trans_e2.exps
             "@\nWARNING: Missing RHS operand in BinOp. Returning -1. Fix needed...@\n"
         in
@@ -950,7 +950,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
           else
             let exp_op, instr_bin =
               CArithmetic_trans.binary_operation_instruction stmt_info.Clang_ast_t.si_source_range
-                binary_operator_info var_exp typ sil_e2 sil_loc
+                binary_operator_info e1_with_typ typ e2_with_typ sil_loc
             in
             (* Create a node if the priority if free and there are instructions *)
             let creating_node =

infer/tests/codetoanalyze/c/bufferoverrun/issues.exp

@@ -59,8 +59,9 @@ codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, ERR
 codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN_L3, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1, 255] Size: [10000, 10000]]
 codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L4, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/pointer_arith.c, FN_pointer_arith_bad, 3, CONDITION_ALWAYS_FALSE, WARNING, []
+codetoanalyze/c/bufferoverrun/pointer_arith.c, FN_pointer_arith_bad, 3, CONDITION_ALWAYS_TRUE, WARNING, []
 codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
-codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_arrblk_eq_Ok, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: [15, 5] Size: [5, 5] @ codetoanalyze/c/bufferoverrun/prune_alias.c:135:5 by call to `prune_arrblk_eq()` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [1, 1]]
 codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: [5, 5] Size: [5, 5] @ codetoanalyze/c/bufferoverrun/prune_alias.c:117:5 by call to `prune_arrblk_ne()` ]
@@ -83,9 +84,9 @@ codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 3, CONDI
 codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [1, 1]]
 codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_true_Ok, 3, CONDITION_ALWAYS_TRUE, WARNING, []
 codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_value_Ok, 3, CONDITION_ALWAYS_FALSE, WARNING, []
+codetoanalyze/c/bufferoverrun/sizeof.c, FN_static_stride_bad, 5, CONDITION_ALWAYS_FALSE, WARNING, []
 codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRUE, WARNING, []
 codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [0, 0]]
-codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 7, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [0, 0]]
 codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_once_intentional_good, 3, CONDITION_ALWAYS_FALSE, WARNING, []
 codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_break_good, 1, CONDITION_ALWAYS_TRUE, WARNING, []

infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c

@@ -7,7 +7,7 @@
  * of patent rights can be found in the PATENTS file in the same directory.
  */
 
-void pointer_arith_bad() {
+void FN_pointer_arith_bad() {
   char arr[10];
   int x = 0;
   if (&x - 1 == 0)

infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c

@@ -22,7 +22,7 @@ struct some_struct {
   int x1;
 };
 
-void static_stride_bad() {
+void FN_static_stride_bad() {
   struct some_struct a[10];
   struct some_struct *x, *y;
   x = &(a[5]);