Translate SynchronizedStmt

Reviewed By: ngorogiannis

Differential Revision: D14744924

fbshipit-source-id: 84e708701

infer/src/clang/ast_expressions.ml

@@ -184,6 +184,23 @@ let make_next_object_exp stmt_info item items =
   (assignment, loop_cond)
 
 
+let make_function_call stmt_info fname params =
+  let expr_info = make_expr_info (builtin_to_qual_type `Void) `XValue `Ordinary in
+  let name_decl_info = {Clang_ast_t.ni_name= fname; ni_qual_name= [fname]} in
+  let decl_ref =
+    make_decl_ref `Function 0 name_decl_info false (Some (builtin_to_qual_type `Void))
+  in
+  let decl_ref_expr_info = make_decl_ref_expr_info decl_ref in
+  let decl_ref_expr = Clang_ast_t.DeclRefExpr (stmt_info, [], expr_info, decl_ref_expr_info) in
+  let implicit_cast_expr =
+    create_implicit_cast_expr stmt_info [decl_ref_expr]
+      (builtin_to_qual_type `Void)
+      `FunctionToPointerDecay
+  in
+  let stmts = implicit_cast_expr :: params in
+  Clang_ast_t.CallExpr (stmt_info, stmts, expr_info)
+
+
 (* We translate an expression with a conditional*)
 (* x <=> x?1:0 *)
 let trans_with_conditional stmt_info expr_info stmt_list =

infer/src/clang/ast_expressions.mli

@@ -26,6 +26,8 @@ val create_implicit_cast_expr : stmt_info -> stmt list -> qual_type -> cast_kind
 val make_obj_c_message_expr_info_class :
   string -> Typ.Name.t -> pointer option -> obj_c_message_expr_info
 
+val make_function_call : stmt_info -> string -> stmt list -> stmt
+
 val trans_with_conditional : stmt_info -> expr_info -> stmt list -> stmt
 (** We translate an expression with a conditional
     x <=> x?1:0 *)

infer/src/clang/cTrans.ml

@@ -2691,15 +2691,25 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
     instruction trans_state message_stmt
 
 
-  (* Assumption: stmt_list contains 2 items, the first can be ObjCMessageExpr or ParenExpr *)
-  (* We ignore this item since we don't deal with the concurrency problem yet *)
-  (* For the same reason we also ignore the stmt_info that
-     is related with the ObjCAtSynchronizedStmt construct *)
-  (* Finally we recursively work on the CompoundStmt, the second item of stmt_list *)
-  and objCAtSynchronizedStmt_trans trans_state stmt_list =
+  (* @synchronized(anObj) {body} is translated as 
+      
+     __set_locked_attribue(anObj);
+     body;
+     __delete_locked_attribute(anObj);    
+   *)
+  and objCAtSynchronizedStmt_trans trans_state stmt_list stmt_info =
     match stmt_list with
-    | [_; compound_stmt] ->
-        instruction trans_state compound_stmt
+    | [lockExpr; compound_stmt] ->
+        let set_lock_stmt =
+          Ast_expressions.make_function_call stmt_info "__set_locked_attribute" [lockExpr]
+        in
+        let set_delete_stmt =
+          Ast_expressions.make_function_call stmt_info "__delete_locked_attribute" [lockExpr]
+        in
+        let sync_compound_stmt =
+          Clang_ast_t.CompoundStmt (stmt_info, [set_lock_stmt; compound_stmt; set_delete_stmt])
+        in
+        instruction trans_state sync_compound_stmt
     | _ ->
         assert false
 
@@ -3411,8 +3421,8 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
         breakStmt_trans trans_state stmt_info
     | ContinueStmt (stmt_info, _) ->
         continueStmt_trans trans_state stmt_info
-    | ObjCAtSynchronizedStmt (_, stmt_list) ->
-        objCAtSynchronizedStmt_trans trans_state stmt_list
+    | ObjCAtSynchronizedStmt (stmt_info, stmt_list) ->
+        objCAtSynchronizedStmt_trans trans_state stmt_list stmt_info
     | ObjCIndirectCopyRestoreExpr (_, stmt_list, _) ->
         let control, returns = instructions trans_state stmt_list in
         mk_trans_result (last_or_mk_fresh_void_exp_typ returns) control

infer/tests/codetoanalyze/objc/frontend/arc/Makefile

@@ -12,6 +12,7 @@ SOURCES = \
   ../types/attributes.m \
   ../types/void_call.m \
   ../vardecl/initlist.m \
+  ../synchronizedStmt/sync.m \
   ../shared/block/BlockVar.m \
 	../shared/block/Blocks_as_parameters.m \
   ../shared/memory_leaks_benchmark/ArcExample.m \

infer/tests/codetoanalyze/objc/frontend/noarc/Makefile

@@ -53,6 +53,7 @@ SOURCES = \
   ../subclass/MyClass.m \
   ../subclass/MySubClass.m \
   ../subclass/main.c \
+  ../synchronizedStmt/sync.m \
   ../types/testloop.m \
   ../vardecl/aclass.m \
   ../vardecl/aclass_2.m \

infer/tests/codetoanalyze/objc/frontend/synchronizedStmt/sync.m

@@ -0,0 +1,30 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#import <Foundation/NSObject.h>
+
+void foo(int);
+
+@interface A : NSObject
+@end
+
+@implementation A
+
+- (void)myMethod:(id)anObj
+
+{
+  @synchronized(anObj)
+
+  {
+    // Everything between the braces is protected by the @synchronized
+    // directive.
+    int x = 0;
+    x++;
+    foo(x);
+  }
+}
+
+@end

infer/tests/codetoanalyze/objc/frontend/synchronizedStmt/sync.m.dot

@@ -0,0 +1,30 @@
+/* @generated */
+digraph cfg {
+"myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_1" [label="1: Start A_myMethod:\nFormals:  self:A* anObj:objc_object*\nLocals:  x:int \n  " color=yellow style=filled]
+	
+
+	 "myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_1" -> "myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_7" ;
+"myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_2" [label="2: Exit A_myMethod: \n  " color=yellow style=filled]
+	
+
+"myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_3" [label="3:  Call _fun___delete_locked_attribute \n   n$0=*&anObj:objc_object* [line 19, column 17]\n  n$1=_fun___delete_locked_attribute(n$0:objc_object*) [line 19, column 3]\n  NULLIFY(&anObj); [line 19, column 3]\n  EXIT_SCOPE(n$0,n$1,anObj); [line 19, column 3]\n  APPLY_ABSTRACTION; [line 19, column 3]\n " shape="box"]
+	
+
+	 "myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_3" -> "myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_2" ;
+"myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_4" [label="4:  Call _fun_foo \n   n$2=*&x:int [line 26, column 9]\n  n$3=_fun_foo(n$2:int) [line 26, column 5]\n  NULLIFY(&x); [line 26, column 5]\n  EXIT_SCOPE(n$2,n$3,x); [line 26, column 5]\n " shape="box"]
+	
+
+	 "myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_4" -> "myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_3" ;
+"myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_5" [label="5:  UnaryOperator \n   n$4=*&x:int [line 25, column 5]\n  *&x:int=(n$4 + 1) [line 25, column 5]\n  EXIT_SCOPE(n$4); [line 25, column 5]\n " shape="box"]
+	
+
+	 "myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_5" -> "myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_4" ;
+"myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_6" [label="6:  DeclStmt \n   n$5=_fun___variable_initialization(&x:int) assign_last [line 24, column 5]\n  *&x:int=0 [line 24, column 5]\n  EXIT_SCOPE(n$5); [line 24, column 5]\n " shape="box"]
+	
+
+	 "myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_6" -> "myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_5" ;
+"myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_7" [label="7:  Call _fun___set_locked_attribute \n   n$6=*&anObj:objc_object* [line 19, column 17]\n  n$7=_fun___set_locked_attribute(n$6:objc_object*) [line 19, column 3]\n  EXIT_SCOPE(n$6,n$7); [line 19, column 3]\n " shape="box"]
+	
+
+	 "myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_7" -> "myMethod:#A(struct objc_object)#instance.6280971b05d6b617955d8216a04fe405_6" ;
+}