From d15e60ffbfe396c53582d142c9ea343684bb0362 Mon Sep 17 00:00:00 2001 From: Dulma Rodriguez Date: Tue, 30 Jun 2015 09:17:55 -0100 Subject: [PATCH] [clang] Translating nonnull attributes as assertions --- infer/src/clang/ast_expressions.ml | 39 +++++++++- infer/src/clang/ast_expressions.mli | 2 + infer/src/clang/cFrontend_config.ml | 2 + infer/src/clang/cFrontend_config.mli | 2 + infer/src/clang/cFrontend_utils.ml | 4 + infer/src/clang/cFrontend_utils.mli | 2 + infer/src/clang/cMethod_decl.ml | 27 +++++-- .../errors/npe/Nonnull_attribute_example.dot | 77 +++++++++++++++++++ .../errors/npe/Nonnull_attribute_example.m | 44 +++++++++++ .../endtoend/objc/NonnullAttributeTest.java | 62 +++++++++++++++ .../frontend/objc/NonnullAttributeTest.java | 44 +++++++++++ 11 files changed, 296 insertions(+), 9 deletions(-) create mode 100644 infer/tests/codetoanalyze/objc/errors/npe/Nonnull_attribute_example.dot create mode 100644 infer/tests/codetoanalyze/objc/errors/npe/Nonnull_attribute_example.m create mode 100644 infer/tests/endtoend/objc/NonnullAttributeTest.java create mode 100644 infer/tests/frontend/objc/NonnullAttributeTest.java diff --git a/infer/src/clang/ast_expressions.ml b/infer/src/clang/ast_expressions.ml index 37371569a..51ea2cd0e 100644 --- a/infer/src/clang/ast_expressions.ml +++ b/infer/src/clang/ast_expressions.ml @@ -128,7 +128,7 @@ let dummy_stmt () = let make_stmt_info di = { Clang_ast_t.si_pointer = di.Clang_ast_t.di_pointer; Clang_ast_t.si_source_range = di.Clang_ast_t.di_source_range } -let make_expr_info qt objc_kind = { +let make_expr_info_with_objc_kind qt objc_kind = { Clang_ast_t.ei_qual_type = qt; Clang_ast_t.ei_value_kind = `LValue; Clang_ast_t.ei_object_kind = objc_kind;} @@ -189,7 +189,7 @@ let make_obj_c_ivar_ref_expr_info k n qt = { (* Build an AST cast expression of a decl_ref_expr *) let make_cast_expr qt di decl_ref_expr_info objc_kind = - let expr_info = make_expr_info qt objc_kind in + let expr_info = make_expr_info_with_objc_kind qt objc_kind in let stmt_info = make_stmt_info di in let decl_ref_exp = make_decl_ref_exp stmt_info expr_info decl_ref_expr_info in let cast_expr = { @@ -202,7 +202,7 @@ let make_cast_expr qt di decl_ref_expr_info objc_kind = (* Build AST expression self.field_name as `LValue *) let make_self_field class_type di qt field_name = let qt_class = create_qual_type class_type in - let expr_info = make_expr_info qt `ObjCProperty in + let expr_info = make_expr_info_with_objc_kind qt `ObjCProperty in let stmt_info = make_stmt_info di in let cast_exp = make_cast_expr qt_class di (make_decl_ref_expr_info (make_decl_ref_self qt_class)) `ObjCProperty in let obj_c_ivar_ref_expr_info = make_obj_c_ivar_ref_expr_info (`ObjCIvar) field_name qt in @@ -213,7 +213,7 @@ let make_self_field class_type di qt field_name = let make_deref_self_field class_decl_opt di qt field_name = let stmt_info = make_stmt_info di in let ivar_ref_exp = make_self_field class_decl_opt di qt field_name in - let expr_info' = make_expr_info qt `ObjCProperty in + let expr_info' = make_expr_info_with_objc_kind qt `ObjCProperty in let cast_exp_info = { Clang_ast_t.cei_cast_kind = `LValueToRValue; @@ -346,3 +346,34 @@ let translate_dispatch_function block_name stmt_info stmt_list ei n = let trans_negation_with_conditional stmt_info expr_info stmt_list = let stmt_list_cond = stmt_list @ [create_integer_literal stmt_info "0"] @ [create_integer_literal stmt_info "1"] in ConditionalOperator(stmt_info, stmt_list_cond, expr_info) + +let create_call stmt_info function_name qt parameters = + let expr_info_call = { + Clang_ast_t.ei_qual_type = qt; + Clang_ast_t.ei_value_kind = `XValue; + Clang_ast_t.ei_object_kind = `Ordinary + } in + let expr_info_dre = make_expr_info_with_objc_kind qt `Ordinary in + let decl_ref = make_general_decl_ref `Function function_name false qt in + let decl_ref_info = make_decl_ref_expr_info decl_ref in + let decl_ref_exp = DeclRefExpr(stmt_info, [], expr_info_dre, decl_ref_info) in + CallExpr(stmt_info, decl_ref_exp:: parameters, expr_info_call) + +let create_assume_not_null_call decl_info var_name var_type = + let stmt_info = stmt_info_with_fresh_pointer (make_stmt_info decl_info) in + let boi = { Clang_ast_t.boi_kind = `NE } in + let decl_ref = make_general_decl_ref `Var var_name false var_type in + let stmt_info_var = dummy_stmt_info () in + let decl_ref_info = make_decl_ref_expr_info decl_ref in + let var_decl_ref = DeclRefExpr(stmt_info_var, [], (make_expr_info var_type), decl_ref_info) in + let expr_info = { + Clang_ast_t.ei_qual_type = var_type; + Clang_ast_t.ei_value_kind = `RValue; + Clang_ast_t.ei_object_kind = `Ordinary + } in + let cast_info_call = { cei_cast_kind = `LValueToRValue; cei_base_path = [] } in + let decl_ref_exp_cast = ImplicitCastExpr(stmt_info, [var_decl_ref], expr_info, cast_info_call) in + let null_expr = create_integer_literal stmt_info "0" in + let bin_op = make_binary_stmt decl_ref_exp_cast null_expr stmt_info (make_expr_info var_type) boi in + let parameters = [bin_op] in + create_call stmt_info (Procname.to_string SymExec.ModelBuiltins.__infer_assume) (create_void_type ()) parameters diff --git a/infer/src/clang/ast_expressions.mli b/infer/src/clang/ast_expressions.mli index 1cc86e530..ed238b1fb 100644 --- a/infer/src/clang/ast_expressions.mli +++ b/infer/src/clang/ast_expressions.mli @@ -62,3 +62,5 @@ val translate_dispatch_function : string -> stmt_info -> stmt list -> expr_info (* We translate the logical negation of an integer with a conditional*) (* !x <=> x?0:1 *) val trans_negation_with_conditional : stmt_info -> expr_info -> stmt list -> stmt + +val create_assume_not_null_call : decl_info -> string -> qual_type -> stmt diff --git a/infer/src/clang/cFrontend_config.ml b/infer/src/clang/cFrontend_config.ml index 7c712b32a..2695c0aef 100644 --- a/infer/src/clang/cFrontend_config.ml +++ b/infer/src/clang/cFrontend_config.ml @@ -121,3 +121,5 @@ let handleFailureInMethod = "handleFailureInMethod:object:file:lineNumber:descri let handleFailureInFunction = "handleFailureInFunction:file:lineNumber:description:" let fbAssertWithSignalAndLogFunctionHelper = "FBAssertWithSignalAndLogFunctionHelper" + +let nonnull_attribute = "__nonnull" diff --git a/infer/src/clang/cFrontend_config.mli b/infer/src/clang/cFrontend_config.mli index b8e524023..25918f50f 100644 --- a/infer/src/clang/cFrontend_config.mli +++ b/infer/src/clang/cFrontend_config.mli @@ -118,3 +118,5 @@ val assert_rtn : string val handleFailureInMethod : string val handleFailureInFunction : string + +val nonnull_attribute : string diff --git a/infer/src/clang/cFrontend_utils.ml b/infer/src/clang/cFrontend_utils.ml index bd7cf6788..1c2a088e1 100644 --- a/infer/src/clang/cFrontend_utils.ml +++ b/infer/src/clang/cFrontend_utils.ml @@ -223,6 +223,10 @@ struct | `Setter setter -> setter.Clang_ast_t.dr_name | _ -> (setter_attribute_opt rest) + (*TODO: take the attributes into account too. To be done after we get the attribute's arguments. *) + let is_type_nonnull qt attributes = + Utils.string_is_prefix CFrontend_config.nonnull_attribute qt.Clang_ast_t.qt_raw + let pointer_counter = ref 0 let get_fresh_pointer () = diff --git a/infer/src/clang/cFrontend_utils.mli b/infer/src/clang/cFrontend_utils.mli index 629910925..b8566884f 100644 --- a/infer/src/clang/cFrontend_utils.mli +++ b/infer/src/clang/cFrontend_utils.mli @@ -57,6 +57,8 @@ sig val is_copy : Clang_ast_t.property_attribute option -> bool + val is_type_nonnull : Clang_ast_t.qual_type -> Clang_ast_t.attribute list -> bool + val get_fresh_pointer : unit -> string val type_from_unary_expr_or_type_trait_expr_info : diff --git a/infer/src/clang/cMethod_decl.ml b/infer/src/clang/cMethod_decl.ml index ffcc1f79c..794f6e50d 100644 --- a/infer/src/clang/cMethod_decl.ml +++ b/infer/src/clang/cMethod_decl.ml @@ -90,9 +90,21 @@ struct let model_exists procname = Specs.summary_exists_in_models procname && not !CFrontend_config.models_mode + let rec add_assume_not_null_calls param_decls attributes = + match param_decls with + | [] -> [] + | decl:: rest -> + let rest_assume_calls = add_assume_not_null_calls rest attributes in + (match decl with + | ParmVarDecl(decl_info, name, qtype, var_decl_info) + when CFrontend_utils.Ast_utils.is_type_nonnull qtype attributes -> + let assume_call = Ast_expressions.create_assume_not_null_call decl_info name qtype in + assume_call:: rest_assume_calls + | _ -> rest_assume_calls) + (* Translates the method/function's body into nodes of the cfg. *) let add_method tenv cg cfg class_decl_opt procname namespace instrs is_objc_method is_instance - captured_vars is_anonym_block = + captured_vars is_anonym_block param_decls attributes = Printing.log_out "\n\n>>---------- ADDING METHOD: '%s' ---------<<\n" (Procname.to_string procname); try @@ -111,7 +123,9 @@ struct Printing.log_out "\n\n>>---------- Start translating the function: '%s' ---------<<" (Procname.to_string procname); - let meth_body_nodes = T.instructions_trans context instrs exit_node in + let nonnull_assume_calls = add_assume_not_null_calls param_decls in + let instrs' = instrs@nonnull_assume_calls attributes in + let meth_body_nodes = T.instructions_trans context instrs' exit_node in if (not is_anonym_block) then CContext.LocalVars.reset_block (); Cfg.Node.set_succs_exn start_node meth_body_nodes []; Cg.add_node (CContext.get_cg context) (Cfg.Procdesc.get_proc_name procdesc)) @@ -139,11 +153,12 @@ struct let is_anonym_block = Option.is_some anonym_block_opt in let is_objc_method = is_anonym_block in let curr_class = if is_anonym_block then curr_class else CContext.ContextNoCls in + let attributes = CMethod_signature.ms_get_attributes ms in add_method tenv cg cfg curr_class procname namespace [body] is_objc_method is_instance - captured_vars is_anonym_block + captured_vars is_anonym_block fdecl_info.Clang_ast_t.fdi_parameters attributes | None, ms -> - CMethod_trans.create_local_procdesc cfg tenv ms [] captured_vars false; - CMethod_signature.add ms + CMethod_trans.create_local_procdesc cfg tenv ms [] captured_vars false; + CMethod_signature.add ms let process_objc_method_decl tenv cg cfg namespace curr_class decl_info method_name method_decl_info = let class_name = CContext.get_curr_class_name curr_class in @@ -154,8 +169,10 @@ struct (match method_body_to_translate decl_info ms method_decl_info.Clang_ast_t.omdi_body with | Some body -> let is_instance = CMethod_signature.ms_is_instance ms in + let attributes = CMethod_signature.ms_get_attributes ms in CMethod_trans.create_local_procdesc cfg tenv ms [body] [] is_instance; add_method tenv cg cfg curr_class procname namespace [body] true is_instance [] false + method_decl_info.Clang_ast_t.omdi_parameters attributes | None -> CMethod_signature.add ms) diff --git a/infer/tests/codetoanalyze/objc/errors/npe/Nonnull_attribute_example.dot b/infer/tests/codetoanalyze/objc/errors/npe/Nonnull_attribute_example.dot new file mode 100644 index 000000000..05f1b8b1a --- /dev/null +++ b/infer/tests/codetoanalyze/objc/errors/npe/Nonnull_attribute_example.dot @@ -0,0 +1,77 @@ +digraph iCFG { +20 [label="20: Call _fun___infer_assume \n n$20=*&callback:_fn_ (*) [line 42]\n n$21=_fun___infer_assume((n$20 != 0):_fn_ (*)) [line 42]\n REMOVE_TEMPS(n$20,n$21); [line 42]\n " shape="box"] + + + 20 -> 19 ; +19 [label="19: Call n$19 \n n$19=*&callback:_fn_ (*) [line 43]\n n$19(0:class NSError *,0:id *) [line 43]\n REMOVE_TEMPS(n$19); [line 43]\n NULLIFY(&callback,false); [line 43]\n APPLY_ABSTRACTION; [line 43]\n " shape="box"] + + + 19 -> 18 ; +18 [label="18: Exit test \n " color=yellow style=filled] + + +17 [label="17: Start test\nFormals: callback:_fn_ (*)\nLocals: \n DECLARE_LOCALS(&return); [line 42]\n " color=yellow style=filled] + + + 17 -> 20 ; +16 [label="16: Call _fun___infer_assume \n n$17=*&name:class NSString * [line -1]\n n$18=_fun___infer_assume((n$17 != 0):class NSString *) [line -1]\n REMOVE_TEMPS(n$17,n$18); [line -1]\n " shape="box"] + + + 16 -> 15 ; +15 [label="15: BinaryOperatorStmt: Assign \n n$14=*&self:class C * [line 27]\n n$16=*&name:class NSString * [line -1]\n n$15=_fun_NSString_copy(n$16:class NSString *) virtual [line -1]\n *n$14._name:class NSString *=n$15 [line -1]\n REMOVE_TEMPS(n$14,n$15,n$16); [line -1]\n NULLIFY(&name,false); [line -1]\n NULLIFY(&self,false); [line -1]\n APPLY_ABSTRACTION; [line -1]\n " shape="box"] + + + 15 -> 14 ; +14 [label="14: Exit C_setName: \n " color=yellow style=filled] + + +13 [label="13: Start C_setName:\nFormals: self:class C * name:class NSString *\nLocals: \n DECLARE_LOCALS(&return); [line -1]\n " color=yellow style=filled] + + + 13 -> 16 ; +12 [label="12: Return Stmt \n n$11=*&self:class C * [line -1]\n n$12=*n$11._name:class NSString * [line -1]\n *&return:class NSString *=n$12 [line -1]\n n$13=_fun___set_autorelease_attribute(n$12:class NSString *) [line -1]\n REMOVE_TEMPS(n$11,n$12,n$13); [line -1]\n NULLIFY(&self,false); [line -1]\n APPLY_ABSTRACTION; [line -1]\n " shape="box"] + + + 12 -> 11 ; +11 [label="11: Exit C_name \n " color=yellow style=filled] + + +10 [label="10: Start C_name\nFormals: self:class C *\nLocals: \n DECLARE_LOCALS(&return); [line -1]\n " color=yellow style=filled] + + + 10 -> 12 ; +9 [label="9: Call _fun___infer_assume \n n$9=*&a:class A * [line -1]\n n$10=_fun___infer_assume((n$9 != 0):class A *) [line -1]\n REMOVE_TEMPS(n$9,n$10); [line -1]\n " shape="box"] + + + 9 -> 8 ; +8 [label="8: DeclStmt \n n$8=*&a:class A * [line 35]\n n$7=_fun_A_getA(n$8:class A *) virtual [line 35]\n _fun___objc_retain(n$7:class A *) [line 35]\n *&a1:class A *=n$7 [line 35]\n REMOVE_TEMPS(n$7,n$8); [line 35]\n NULLIFY(&a,false); [line 35]\n " shape="box"] + + + 8 -> 7 ; +7 [label="7: DeclStmt \n n$5=*&a1:class A * [line 36]\n n$6=*n$5.x:int [line 36]\n *&y:int =n$6 [line 36]\n REMOVE_TEMPS(n$5,n$6); [line 36]\n NULLIFY(&a1,false); [line 36]\n NULLIFY(&y,false); [line 36]\n " shape="box"] + + + 7 -> 6 ; +6 [label="6: Return Stmt \n n$4=*&self:class C * [line 37]\n *&return:struct objc_object *=n$4 [line 37]\n REMOVE_TEMPS(n$4); [line 37]\n NULLIFY(&self,false); [line 37]\n APPLY_ABSTRACTION; [line 37]\n " shape="box"] + + + 6 -> 5 ; +5 [label="5: Exit C_initWithCoder:and: \n " color=yellow style=filled] + + +4 [label="4: Start C_initWithCoder:and:\nFormals: self:class C * aDecoder:class NSString * a:class A *\nLocals: a1:class A * y:int \n DECLARE_LOCALS(&return,&a1,&y); [line 33]\n NULLIFY(&a1,false); [line 33]\n NULLIFY(&aDecoder,false); [line 33]\n NULLIFY(&y,false); [line 33]\n " color=yellow style=filled] + + + 4 -> 9 ; +3 [label="3: Return Stmt \n n$1=_fun___objc_alloc_no_fail(sizeof(class A ):class A *) [line 21]\n n$2=_fun_A_init(n$1:class A *) virtual [line 21]\n *&return:class A *=n$2 [line 21]\n n$3=_fun___set_autorelease_attribute(n$2:class A *) [line 21]\n REMOVE_TEMPS(n$1,n$2,n$3); [line 21]\n APPLY_ABSTRACTION; [line 21]\n " shape="box"] + + + 3 -> 2 ; +2 [label="2: Exit A_getA \n " color=yellow style=filled] + + +1 [label="1: Start A_getA\nFormals: self:class A *\nLocals: \n DECLARE_LOCALS(&return); [line 20]\n NULLIFY(&self,false); [line 20]\n " color=yellow style=filled] + + + 1 -> 3 ; +} diff --git a/infer/tests/codetoanalyze/objc/errors/npe/Nonnull_attribute_example.m b/infer/tests/codetoanalyze/objc/errors/npe/Nonnull_attribute_example.m new file mode 100644 index 000000000..f9781df74 --- /dev/null +++ b/infer/tests/codetoanalyze/objc/errors/npe/Nonnull_attribute_example.m @@ -0,0 +1,44 @@ +/* + * Copyright (c) 2015 - Facebook. + * All rights reserved. + */ + +#import + +void __infer_assume(int cond); + +@interface A : NSObject { + @public int x; +} + +-(A*) getA; + +@end + +@implementation A + +-(A*) getA { + return [A new]; +} + +@end + +@interface C : NSObject +@property (copy, nonnull) NSString *name; + +@end + +@implementation C + +- (instancetype)initWithCoder:(NSString*)aDecoder and:( A* __nonnull)a +{ + A* a1 = [a getA]; + int y = a1->x; + return self; +} + +@end + +void test(void (^ __nonnull callback)(NSError *, id)) { + callback(NULL, NULL); +} diff --git a/infer/tests/endtoend/objc/NonnullAttributeTest.java b/infer/tests/endtoend/objc/NonnullAttributeTest.java new file mode 100644 index 000000000..cbe50967f --- /dev/null +++ b/infer/tests/endtoend/objc/NonnullAttributeTest.java @@ -0,0 +1,62 @@ +/* + * Copyright (c) 2013- Facebook. + * All rights reserved. + */ + +package endtoend.objc; + +import static org.hamcrest.MatcherAssert.assertThat; +import static utils.matchers.ResultContainsExactly.containsExactly; +import static utils.matchers.ResultContainsNoErrorInMethod.doesNotContain; + +import com.google.common.collect.ImmutableList; + +import org.junit.BeforeClass; +import org.junit.ClassRule; +import org.junit.Test; + +import java.io.IOException; + +import utils.DebuggableTemporaryFolder; +import utils.InferException; +import utils.InferResults; +import utils.InferRunner; + +public class NonnullAttributeTest { + + public static final String NONNULL_FILE = + "infer/tests/codetoanalyze/objc/errors/npe/Nonnull_attribute_example.m"; + + private static ImmutableList inferCmdNil; + + public static final String PARAMETER_NOT_NULL_CHECKED = "PARAMETER_NOT_NULL_CHECKED"; + + + @ClassRule + public static DebuggableTemporaryFolder folderNil = new DebuggableTemporaryFolder(); + + @BeforeClass + public static void runInfer() throws InterruptedException, IOException { + inferCmdNil = InferRunner.createiOSInferCommandWithMLBuckets( + folderNil, + NONNULL_FILE, + "cf", + false); + } + + @Test + public void angelismTest() throws InterruptedException, IOException, InferException { + InferResults inferResults = InferRunner.runInferObjC(inferCmdNil); + String[] procedures = {}; + assertThat( + "Results should not contain parameter not null checked", + inferResults, + containsExactly( + PARAMETER_NOT_NULL_CHECKED, + NONNULL_FILE, + procedures + ) + ); + } + +} diff --git a/infer/tests/frontend/objc/NonnullAttributeTest.java b/infer/tests/frontend/objc/NonnullAttributeTest.java new file mode 100644 index 000000000..58b9661ae --- /dev/null +++ b/infer/tests/frontend/objc/NonnullAttributeTest.java @@ -0,0 +1,44 @@ +/* + * Copyright (c) 2014- Facebook. + * All rights reserved. + */ + +package frontend.objc; + +import static org.hamcrest.MatcherAssert.assertThat; +import static utils.matchers.DotFilesEqual.dotFileEqualTo; + +import com.google.common.collect.ImmutableList; + +import org.junit.Rule; +import org.junit.Test; + +import java.io.File; +import java.io.IOException; + +import utils.DebuggableTemporaryFolder; +import utils.InferException; +import utils.InferRunner; + + +public class NonnullAttributeTest { + + @Rule + public DebuggableTemporaryFolder folder = new DebuggableTemporaryFolder(); + + + @Test + public void whenCaptureRunOnNonnullAttributeExampleThenDotFilesAreTheSame() + throws InterruptedException, IOException, InferException { + + String src = "infer/tests/codetoanalyze/objc/errors/npe/Nonnull_attribute_example.m"; + + String dotty = "infer/tests/codetoanalyze/objc/errors/npe/Nonnull_attribute_example.dot"; + + ImmutableList inferCmd = InferRunner.createObjCInferCommandFrontendArc(folder, src); + File newDotFile = InferRunner.runInferFrontend(inferCmd); + assertThat( + "In the capture of " + src + " the dotty files should be the same.", + newDotFile, dotFileEqualTo(dotty)); + } +}