[clang] Translating nonnull attributes as assertions

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

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

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"

infer/src/clang/cFrontend_config.mli

@@ -118,3 +118,5 @@ val assert_rtn : string
 val handleFailureInMethod : string
 
 val handleFailureInFunction : string
+
+val nonnull_attribute : string

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 () =

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 :

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,8 +153,9 @@ 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
@@ -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)
 

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 ;
+}

infer/tests/codetoanalyze/objc/errors/npe/Nonnull_attribute_example.m

@@ -0,0 +1,44 @@
+/*
+ * Copyright (c) 2015 - Facebook.
+ * All rights reserved.
+ */
+
+#import <Foundation/NSString.h>
+
+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);
+}

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<String> 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
+        )
+    );
+  }
+
+}

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<String> 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));
+  }
+}