From 00e113907159a0889dd06ec45ba4319ce1461e3e Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 3 Apr 2018 21:40:20 -0700 Subject: [PATCH] [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 --- .../src/bufferoverrun/bufferOverrunChecker.ml | 4 +-- infer/src/clang/cArithmetic_trans.ml | 36 ++++++++++++------- infer/src/clang/cArithmetic_trans.mli | 4 +-- infer/src/clang/cTrans.ml | 8 ++--- .../codetoanalyze/c/bufferoverrun/issues.exp | 5 +-- .../c/bufferoverrun/pointer_arith.c | 2 +- .../codetoanalyze/c/bufferoverrun/sizeof.c | 2 +- 7 files changed, 37 insertions(+), 24 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 879e2352f..e73076798 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 diff --git a/infer/src/clang/cArithmetic_trans.ml b/infer/src/clang/cArithmetic_trans.ml index 43c47b0d9..e8ace7764 100644 --- a/infer/src/clang/cArithmetic_trans.ml +++ b/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 binop_exp op = Exp.BinOp (op, e1, e2) in +let binary_operation_instruction source_range boi ((e1, t1) as e1_with_typ) typ (e2, t2) loc = + 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 diff --git a/infer/src/clang/cArithmetic_trans.mli b/infer/src/clang/cArithmetic_trans.mli index 9710ecc30..efc0ee2a4 100644 --- a/infer/src/clang/cArithmetic_trans.mli +++ b/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 - -> Location.t -> Exp.t * Sil.instr list + Clang_ast_t.source_range -> Clang_ast_t.binary_operator_info -> Exp.t * Typ.t -> Typ.t + -> 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. *) diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 24d638405..5eec67d3a 100644 --- a/infer/src/clang/cTrans.ml +++ b/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 = diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index d32f3ee05..52fc8a686 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/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, [] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c index ca192f8a3..efeb835fc 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c +++ b/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) diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c b/infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c index 5617ae29a..e6ffbc65b 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c +++ b/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]);