Implement AtomicExpr translation (#1434)

Summary:
Implements the translation of most clang atomic builtins to SIL, including those used in `stdatomic.h`. It does not attempt to model the atomicity of the operations, since I don't know of any way Infer can represent that. I didn't bother implementing the rarely used min/max builtins, so they're left as `BuiltinDecl` calls.

This is my first major OCaml project, so any feedback is appreciated!

Also, CONTRIBUTING.md says to update the [facebook-clang-plugins](https://github.com/facebook/facebook-clang-plugins) submodule, but it doesn't seem to be a submodule anymore, and the code has diverged from that repo. Should I still make a PR over there?

Pull Request resolved: https://github.com/facebook/infer/pull/1434

Reviewed By: skcho

Differential Revision: D28118300

Pulled By: jvillard

fbshipit-source-id: 121c4ad25

facebook-clang-plugins/libtooling/ASTExporter.h

@@ -404,6 +404,7 @@ class ASTExporter : public ConstDeclVisitor<ASTExporter<ATDWriter>>,
   DECLARE_VISITOR(ExtVectorElementExpr)
   DECLARE_VISITOR(BinaryOperator)
   DECLARE_VISITOR(CompoundAssignOperator)
+  DECLARE_VISITOR(AtomicExpr)
   DECLARE_VISITOR(AddrLabelExpr)
   DECLARE_VISITOR(BlockExpr)
   DECLARE_VISITOR(OpaqueValueExpr)
@@ -3878,6 +3879,34 @@ void ASTExporter<ATDWriter>::VisitCompoundAssignOperator(
   dumpQualType(Node->getComputationResultType());
 }
 
+template <class ATDWriter>
+int ASTExporter<ATDWriter>::AtomicExprTupleSize() {
+  return ExprTupleSize() + 1;
+}
+#define BUILTIN(ID, TYPE, ATTRS)
+//@atd #define atomic_expr_tuple expr_tuple * atomic_expr_info
+//@atd type atomic_expr_info = {
+//@atd   kind : atomic_expr_kind
+//@atd } <ocaml field_prefix="aei_">
+//@atd type atomic_expr_kind = [
+#define ATOMIC_BUILTIN(ID, TYPE, ATTRS) //@atd | AO@@ID
+#include <clang/Basic/Builtins.def>
+//@atd ]
+template <class ATDWriter>
+void ASTExporter<ATDWriter>::VisitAtomicExpr(const AtomicExpr *Node) {
+  VisitExpr(Node);
+  ObjectScope Scope(OF, 1);
+  OF.emitTag("kind");
+  switch (Node->getOp()) {
+#define BUILTIN(ID, TYPE, ATTRS)
+#define ATOMIC_BUILTIN(ID, TYPE, ATTRS) \
+  case AtomicExpr::AO##ID:              \
+    OF.emitSimpleVariant("AO" #ID);     \
+    break;
+#include <clang/Basic/Builtins.def>
+  }
+}
+
 template <class ATDWriter>
 int ASTExporter<ATDWriter>::BlockExprTupleSize() {
   return ExprTupleSize() + DeclTupleSize();

infer/src/IR/BuiltinDecl.ml

@@ -36,6 +36,26 @@ let __array_access = create_procname "__array_access"
 
 let __assert_fail = create_procname "__assert_fail"
 
+let __atomic_fetch_max = create_procname "__atomic_fetch_max"
+
+let __atomic_fetch_min = create_procname "__atomic_fetch_min"
+
+let __atomic_fetch_nand = create_procname "__atomic_fetch_nand"
+
+let __atomic_max_fetch = create_procname "__atomic_max_fetch"
+
+let __atomic_min_fetch = create_procname "__atomic_min_fetch"
+
+let __atomic_nand_fetch = create_procname "__atomic_nand_fetch"
+
+let __c11_atomic_fetch_max = create_procname "__c11_atomic_fetch_max"
+
+let __c11_atomic_fetch_min = create_procname "__c11_atomic_fetch_min"
+
+let __opencl_atomic_fetch_max = create_procname "__opencl_atomic_fetch_max"
+
+let __opencl_atomic_fetch_min = create_procname "__opencl_atomic_fetch_min"
+
 let __builtin_va_arg = create_procname "__builtin_va_arg"
 
 let __builtin_va_copy = create_procname "__builtin_va_copy"

infer/src/IR/BuiltinDecl.mli

@@ -21,4 +21,24 @@ val __infer_skip_gcc_asm_stmt : Procname.t
 
 val __infer_generic_selection_expr : Procname.t
 
+val __atomic_fetch_max : Procname.t
+
+val __atomic_fetch_min : Procname.t
+
+val __atomic_fetch_nand : Procname.t
+
+val __atomic_max_fetch : Procname.t
+
+val __atomic_min_fetch : Procname.t
+
+val __atomic_nand_fetch : Procname.t
+
+val __c11_atomic_fetch_max : Procname.t
+
+val __c11_atomic_fetch_min : Procname.t
+
+val __opencl_atomic_fetch_max : Procname.t
+
+val __opencl_atomic_fetch_min : Procname.t
+
 val match_builtin : t -> 'a -> string -> bool

infer/src/IR/Procdesc.ml

@@ -57,6 +57,8 @@ module Node = struct
 
   type stmt_nodekind =
     | AssertionFailure
+    | AtomicCompareExchangeBranch
+    | AtomicExpr
     | BetweenJoinAndExit
     | BinaryConditionalStmtInit
     | BinaryOperatorStmt of string
@@ -284,6 +286,10 @@ module Node = struct
   let pp_stmt fmt = function
     | AssertionFailure ->
         F.pp_print_string fmt "Assertion failure"
+    | AtomicCompareExchangeBranch ->
+        F.pp_print_string fmt "Atomic compare exchange branch"
+    | AtomicExpr ->
+        F.pp_print_string fmt "AtomicExpr"
     | BetweenJoinAndExit ->
         F.pp_print_string fmt "between_join_and_exit"
     | BinaryConditionalStmtInit ->

infer/src/IR/Procdesc.mli

@@ -38,6 +38,8 @@ module Node : sig
   (** kind of statement node *)
   type stmt_nodekind =
     | AssertionFailure
+    | AtomicCompareExchangeBranch
+    | AtomicExpr
     | BetweenJoinAndExit
     | BinaryConditionalStmtInit
     | BinaryOperatorStmt of string

infer/src/IR/Sil.ml

@@ -17,6 +17,7 @@ module L = Logging
 (** Kind of prune instruction *)
 type if_kind =
   | Ik_bexp  (** boolean expressions, and exp ? exp : exp *)
+  | Ik_compexch  (** used in atomic compare exchange expressions *)
   | Ik_dowhile
   | Ik_for
   | Ik_if
@@ -146,6 +147,8 @@ let exps_of_instr = function
 let if_kind_to_string = function
   | Ik_bexp ->
       "boolean exp"
+  | Ik_compexch ->
+      "atomic compare exchange"
   | Ik_dowhile ->
       "do while"
   | Ik_for ->

infer/src/IR/Sil.mli

@@ -16,6 +16,7 @@ module F = Format
 (** Kind of prune instruction *)
 type if_kind =
   | Ik_bexp  (** boolean expressions, and exp ? exp : exp *)
+  | Ik_compexch  (** used in atomic compare exchange expressions *)
   | Ik_dowhile
   | Ik_for
   | Ik_if

infer/src/biabduction/Paths.ml

@@ -503,6 +503,10 @@ end = struct
                     "Switch condition is true. Entering switch case"
                 | false, Sil.Ik_switch ->
                     "Switch condition is false. Skipping switch case"
+                | true, Sil.Ik_compexch ->
+                    "Pointer contains expected value. Writing desired to pointer"
+                | false, Sil.Ik_compexch ->
+                    "Pointer does not contain expected value. Writing to expected"
                 | true, (Sil.Ik_bexp | Sil.Ik_land_lor) ->
                     "Condition is true"
                 | false, (Sil.Ik_bexp | Sil.Ik_land_lor) ->

infer/src/clang/cArithmetic_trans.ml

@@ -183,6 +183,53 @@ let unary_operation_instruction translation_unit_context uoi e typ loc =
       (e, [])
 
 
+let atomic_operation_instruction aei e1 e2 typ loc =
+  let atomic_binop bop ~fetch_first =
+    let id = Ident.create_fresh Ident.knormal in
+    let instr1 = Sil.Load {id; e= e1; root_typ= typ; typ; loc} in
+    let e1_op_e2 = Exp.BinOp (bop, Exp.Var id, e2) in
+    if fetch_first then (Exp.Var id, [instr1; Sil.Store {e1; root_typ= typ; typ; e2= e1_op_e2; loc}])
+    else
+      let fetch_id = Ident.create_fresh Ident.knormal in
+      let fetch_instr = Sil.Load {id= fetch_id; e= e1; root_typ= typ; typ; loc} in
+      ( Exp.Var fetch_id
+      , [instr1; Sil.Store {e1; root_typ= typ; typ; e2= e1_op_e2; loc}; fetch_instr] )
+  in
+  match aei.Clang_ast_t.aei_kind with
+  (* GNU builtins do arithmetic operations even with pointers *)
+  | `AO__atomic_fetch_add ->
+      atomic_binop (Binop.PlusA (Typ.get_ikind_opt typ)) ~fetch_first:true
+  | `AO__c11_atomic_fetch_add | `AO__opencl_atomic_fetch_add ->
+      atomic_binop
+        (if Typ.is_pointer typ then Binop.PlusPI else Binop.PlusA (Typ.get_ikind_opt typ))
+        ~fetch_first:true
+  | `AO__atomic_add_fetch ->
+      atomic_binop (Binop.PlusA (Typ.get_ikind_opt typ)) ~fetch_first:false
+  | `AO__atomic_fetch_sub ->
+      atomic_binop (Binop.MinusA (Typ.get_ikind_opt typ)) ~fetch_first:true
+  | `AO__c11_atomic_fetch_sub | `AO__opencl_atomic_fetch_sub ->
+      atomic_binop
+        (if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA (Typ.get_ikind_opt typ))
+        ~fetch_first:true
+  | `AO__atomic_sub_fetch ->
+      atomic_binop (Binop.MinusA (Typ.get_ikind_opt typ)) ~fetch_first:false
+  | `AO__atomic_fetch_or | `AO__c11_atomic_fetch_or | `AO__opencl_atomic_fetch_or ->
+      atomic_binop Binop.BOr ~fetch_first:true
+  | `AO__atomic_or_fetch ->
+      atomic_binop Binop.BOr ~fetch_first:false
+  | `AO__atomic_fetch_xor | `AO__c11_atomic_fetch_xor | `AO__opencl_atomic_fetch_xor ->
+      atomic_binop Binop.BXor ~fetch_first:true
+  | `AO__atomic_xor_fetch ->
+      atomic_binop Binop.BXor ~fetch_first:false
+  | `AO__atomic_fetch_and | `AO__c11_atomic_fetch_and | `AO__opencl_atomic_fetch_and ->
+      atomic_binop Binop.BAnd ~fetch_first:true
+  | `AO__atomic_and_fetch ->
+      atomic_binop Binop.BAnd ~fetch_first:false
+  | _ ->
+      (* We only call this function if it's been implemented. *)
+      assert false
+
+
 let bin_op_to_string boi =
   match boi.Clang_ast_t.boi_kind with
   | `PtrMemD ->

infer/src/clang/cArithmetic_trans.mli

@@ -7,7 +7,7 @@
 
 open! IStd
 
-(** Utility module for translating unary and binary operations and compound assignments *)
+(** Utility module for translating unary, binary, and atomic operations and compound assignments *)
 
 val bin_op_to_string : Clang_ast_t.binary_operator_info -> string
 
@@ -31,4 +31,7 @@ val unary_operation_instruction :
   -> Location.t
   -> Exp.t * Sil.instr list
 
+val atomic_operation_instruction :
+  Clang_ast_t.atomic_expr_info -> Exp.t -> Exp.t -> Typ.t -> Location.t -> Exp.t * Sil.instr list
+
 val sil_const_plus_one : Exp.t -> Exp.t

infer/src/clang/cTrans.ml

@@ -1105,6 +1105,417 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
         assert false
 
 
+  and atomicExpr_trans trans_state atomic_expr_info stmt_info expr_info stmt_list =
+    let context = trans_state.context in
+    let sil_loc =
+      CLocation.location_of_stmt_info context.translation_unit_context.source_file stmt_info
+    in
+    let ret_typ =
+      CType_decl.qual_type_to_sil_type context.CContext.tenv expr_info.Clang_ast_t.ei_qual_type
+    in
+    let node_name = Procdesc.Node.AtomicExpr in
+    let handle_unimplemented builtin =
+      call_function_with_args node_name builtin trans_state stmt_info ret_typ stmt_list
+    in
+    match atomic_expr_info.Clang_ast_t.aei_kind with
+    | `AO__atomic_add_fetch
+    | `AO__atomic_sub_fetch
+    | `AO__atomic_or_fetch
+    | `AO__atomic_xor_fetch
+    | `AO__atomic_and_fetch
+    | `AO__atomic_fetch_add
+    | `AO__atomic_fetch_sub
+    | `AO__atomic_fetch_or
+    | `AO__atomic_fetch_xor
+    | `AO__atomic_fetch_and
+    | `AO__c11_atomic_fetch_add
+    | `AO__c11_atomic_fetch_sub
+    | `AO__c11_atomic_fetch_or
+    | `AO__c11_atomic_fetch_xor
+    | `AO__c11_atomic_fetch_and
+    | `AO__opencl_atomic_fetch_add
+    | `AO__opencl_atomic_fetch_sub
+    | `AO__opencl_atomic_fetch_or
+    | `AO__opencl_atomic_fetch_xor
+    | `AO__opencl_atomic_fetch_and ->
+        let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in
+        let trans_state' = {trans_state_pri with succ_nodes= []; var_exp_typ= None} in
+        let s1, s2, mem_controls =
+          match stmt_list with
+          | [s1; memorder; s2] ->
+              let res_trans_memorder = instruction trans_state' memorder in
+              (s1, s2, [res_trans_memorder.control])
+          | [s1; memorder; s2; memscope] ->
+              let res_trans_memorder = instruction trans_state' memorder in
+              let res_trans_memscope = instruction trans_state' memscope in
+              (s1, s2, [res_trans_memorder.control; res_trans_memscope.control])
+          | _ ->
+              assert false
+        in
+        let res_trans_s1 = instruction trans_state' s1 in
+        let sil_e1, _ = res_trans_s1.return in
+        let res_trans_s2 = instruction trans_state' s2 in
+        let sil_e2, _ = res_trans_s2.return in
+        let exp_op, instr_op =
+          CArithmetic_trans.atomic_operation_instruction atomic_expr_info sil_e1 sil_e2 ret_typ
+            sil_loc
+        in
+        let atomic_op_control = {empty_control with instrs= instr_op} in
+        let all_control =
+          mem_controls @ [res_trans_s1.control; res_trans_s2.control; atomic_op_control]
+        in
+        PriorityNode.compute_controls_to_parent trans_state_pri sil_loc node_name stmt_info
+          all_control
+        |> mk_trans_result (exp_op, ret_typ)
+    | `AO__atomic_load_n | `AO__c11_atomic_load | `AO__opencl_atomic_load ->
+        let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in
+        let trans_state' = {trans_state_pri with succ_nodes= []; var_exp_typ= None} in
+        let ptr, mem_controls =
+          match stmt_list with
+          | [ptr; memorder] ->
+              let res_trans_memorder = instruction trans_state' memorder in
+              (ptr, [res_trans_memorder.control])
+          | [ptr; memorder; memscope] ->
+              let res_trans_memorder = instruction trans_state' memorder in
+              let res_trans_memscope = instruction trans_state' memscope in
+              (ptr, [res_trans_memorder.control; res_trans_memscope.control])
+          | _ ->
+              assert false
+        in
+        let res_trans_ptr = instruction trans_state' ptr in
+        let e, _ = res_trans_ptr.return in
+        let id = Ident.create_fresh Ident.knormal in
+        let instrs = [Sil.Load {id; e; root_typ= ret_typ; typ= ret_typ; loc= sil_loc}] in
+        let load_control = {empty_control with instrs} in
+        let all_control = mem_controls @ [res_trans_ptr.control; load_control] in
+        PriorityNode.compute_controls_to_parent trans_state_pri sil_loc node_name stmt_info
+          all_control
+        |> mk_trans_result (Exp.Var id, ret_typ)
+    | `AO__atomic_load ->
+        let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in
+        let trans_state' = {trans_state_pri with succ_nodes= []; var_exp_typ= None} in
+        let ptr, ret, mem_controls =
+          match stmt_list with
+          | [ptr; memorder; ret] ->
+              let res_trans_memorder = instruction trans_state' memorder in
+              (ptr, ret, [res_trans_memorder.control])
+          | _ ->
+              assert false
+        in
+        let res_trans_ret = instruction trans_state' ret in
+        let ret_exp, ret_typ = res_trans_ret.return in
+        let res_trans_ptr = instruction trans_state' ptr in
+        let ptr_exp, ptr_typ = res_trans_ptr.return in
+        let ptr_id = Ident.create_fresh Ident.knormal in
+        let instrs =
+          [ Sil.Load
+              { id= ptr_id
+              ; e= ptr_exp
+              ; root_typ= Typ.strip_ptr ptr_typ
+              ; typ= Typ.strip_ptr ptr_typ
+              ; loc= sil_loc }
+          ; Sil.Store
+              { e1= ret_exp
+              ; e2= Exp.Var ptr_id
+              ; root_typ= Typ.strip_ptr ret_typ
+              ; typ= Typ.strip_ptr ret_typ
+              ; loc= sil_loc } ]
+        in
+        let load_control = {empty_control with instrs} in
+        let all_control =
+          mem_controls @ [res_trans_ret.control; res_trans_ptr.control; load_control]
+        in
+        PriorityNode.compute_controls_to_parent trans_state_pri sil_loc node_name stmt_info
+          all_control
+        |> mk_trans_result (mk_fresh_void_exp_typ ())
+    | `AO__atomic_store_n
+    | `AO__c11_atomic_store
+    | `AO__opencl_atomic_store
+    | `AO__c11_atomic_init
+    | `AO__opencl_atomic_init ->
+        let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in
+        let trans_state' = {trans_state_pri with succ_nodes= []; var_exp_typ= None} in
+        let ptr, value, mem_controls =
+          match stmt_list with
+          | [ptr; value] ->
+              (ptr, value, [])
+          | [ptr; memorder; value] ->
+              let res_trans_memorder = instruction trans_state' memorder in
+              (ptr, value, [res_trans_memorder.control])
+          | [ptr; memorder; value; memscope] ->
+              let res_trans_memorder = instruction trans_state' memorder in
+              let res_trans_memscope = instruction trans_state' memscope in
+              (ptr, value, [res_trans_memorder.control; res_trans_memscope.control])
+          | _ ->
+              assert false
+        in
+        let res_trans_ptr = instruction trans_state' ptr in
+        let ptr_exp, _ = res_trans_ptr.return in
+        let res_trans_value = instruction trans_state' value in
+        let value_exp, value_typ = res_trans_value.return in
+        let instrs =
+          [Sil.Store {e1= ptr_exp; e2= value_exp; root_typ= value_typ; typ= value_typ; loc= sil_loc}]
+        in
+        let load_control = {empty_control with instrs} in
+        let all_control =
+          mem_controls @ [res_trans_ptr.control; res_trans_value.control; load_control]
+        in
+        PriorityNode.compute_controls_to_parent trans_state_pri sil_loc node_name stmt_info
+          all_control
+        |> mk_trans_result (mk_fresh_void_exp_typ ())
+    | `AO__atomic_store ->
+        let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in
+        let trans_state' = {trans_state_pri with succ_nodes= []; var_exp_typ= None} in
+        let ptr, value, mem_controls =
+          match stmt_list with
+          | [ptr; memorder; value] ->
+              let res_trans_memorder = instruction trans_state' memorder in
+              (ptr, value, [res_trans_memorder.control])
+          | _ ->
+              assert false
+        in
+        let res_trans_ptr = instruction trans_state' ptr in
+        let ptr_exp, _ = res_trans_ptr.return in
+        let res_trans_value = instruction trans_state' value in
+        let value_exp, value_typ = res_trans_value.return in
+        let typ = Typ.strip_ptr value_typ in
+        let id = Ident.create_fresh Ident.knormal in
+        let instrs =
+          [ Sil.Load {id; e= value_exp; root_typ= typ; typ; loc= sil_loc}
+          ; Sil.Store {e1= ptr_exp; e2= Exp.Var id; root_typ= typ; typ; loc= sil_loc} ]
+        in
+        let load_control = {empty_control with instrs} in
+        let all_control =
+          mem_controls @ [res_trans_ptr.control; res_trans_value.control; load_control]
+        in
+        PriorityNode.compute_controls_to_parent trans_state_pri sil_loc node_name stmt_info
+          all_control
+        |> mk_trans_result (mk_fresh_void_exp_typ ())
+    | `AO__atomic_exchange_n | `AO__c11_atomic_exchange | `AO__opencl_atomic_exchange ->
+        let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in
+        let trans_state' = {trans_state_pri with succ_nodes= []; var_exp_typ= None} in
+        let ptr, value, mem_controls =
+          match stmt_list with
+          | [ptr; memorder; value] ->
+              let res_trans_memorder = instruction trans_state' memorder in
+              (ptr, value, [res_trans_memorder.control])
+          | [ptr; memorder; value; memscope] ->
+              let res_trans_memorder = instruction trans_state' memorder in
+              let res_trans_memscope = instruction trans_state' memscope in
+              (ptr, value, [res_trans_memorder.control; res_trans_memscope.control])
+          | _ ->
+              assert false
+        in
+        let res_trans_ptr = instruction trans_state' ptr in
+        let ptr_exp, _ = res_trans_ptr.return in
+        let res_trans_value = instruction trans_state' value in
+        let value_exp, value_typ = res_trans_value.return in
+        let id = Ident.create_fresh Ident.knormal in
+        let instrs =
+          [ Sil.Load {id; e= ptr_exp; root_typ= ret_typ; typ= ret_typ; loc= sil_loc}
+          ; Sil.Store {e1= ptr_exp; e2= value_exp; root_typ= value_typ; typ= value_typ; loc= sil_loc}
+          ]
+        in
+        let load_control = {empty_control with instrs} in
+        let all_control =
+          mem_controls @ [res_trans_ptr.control; res_trans_value.control; load_control]
+        in
+        PriorityNode.compute_controls_to_parent trans_state_pri sil_loc node_name stmt_info
+          all_control
+        |> mk_trans_result (Exp.Var id, ret_typ)
+    | `AO__atomic_exchange ->
+        let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in
+        let trans_state' = {trans_state_pri with succ_nodes= []; var_exp_typ= None} in
+        let ptr, value, ret, mem_controls =
+          match stmt_list with
+          | [ptr; memorder; value; ret] ->
+              let res_trans_memorder = instruction trans_state' memorder in
+              (ptr, value, ret, [res_trans_memorder.control])
+          | _ ->
+              assert false
+        in
+        let res_trans_ptr = instruction trans_state' ptr in
+        let ptr_exp, _ = res_trans_ptr.return in
+        let res_trans_value = instruction trans_state' value in
+        let value_exp, value_typ = res_trans_value.return in
+        let res_trans_ret = instruction trans_state' ret in
+        let ret_exp, _ = res_trans_ret.return in
+        let ptr_id = Ident.create_fresh Ident.knormal in
+        let value_id = Ident.create_fresh Ident.knormal in
+        let typ = Typ.strip_ptr value_typ in
+        let instrs =
+          [ Sil.Load {id= ptr_id; e= ptr_exp; root_typ= typ; typ; loc= sil_loc}
+          ; Sil.Load {id= value_id; e= value_exp; root_typ= typ; typ; loc= sil_loc}
+          ; Sil.Store {e1= ptr_exp; e2= Exp.Var value_id; root_typ= typ; typ; loc= sil_loc}
+          ; Sil.Store {e1= ret_exp; e2= Exp.Var ptr_id; root_typ= typ; typ; loc= sil_loc} ]
+        in
+        let load_control = {empty_control with instrs} in
+        let all_control =
+          mem_controls
+          @ [res_trans_ptr.control; res_trans_value.control; res_trans_ret.control; load_control]
+        in
+        PriorityNode.compute_controls_to_parent trans_state_pri sil_loc node_name stmt_info
+          all_control
+        |> mk_trans_result (mk_fresh_void_exp_typ ())
+    | `AO__atomic_compare_exchange
+    | `AO__atomic_compare_exchange_n
+    | `AO__c11_atomic_compare_exchange_strong
+    | `AO__c11_atomic_compare_exchange_weak
+    | `AO__opencl_atomic_compare_exchange_strong
+    | `AO__opencl_atomic_compare_exchange_weak ->
+        let trans_state = PriorityNode.try_claim_priority_node trans_state stmt_info in
+        let trans_state' = {trans_state with succ_nodes= []; var_exp_typ= None} in
+        let ptr, expected, desired, mem_controls =
+          match stmt_list with
+          | [ptr; success_memorder; expected; failure_memorder; desired; weak_or_memscope] ->
+              let res_trans_success_memorder = instruction trans_state' success_memorder in
+              let res_trans_failure_memorder = instruction trans_state' failure_memorder in
+              let res_trans_weak_or_memscope = instruction trans_state' weak_or_memscope in
+              ( ptr
+              , expected
+              , desired
+              , [ res_trans_success_memorder.control
+                ; res_trans_failure_memorder.control
+                ; res_trans_weak_or_memscope.control ] )
+          | [ptr; success_memorder; expected; failure_memorder; desired] ->
+              let res_trans_success_memorder = instruction trans_state' success_memorder in
+              let res_trans_failure_memorder = instruction trans_state' failure_memorder in
+              ( ptr
+              , expected
+              , desired
+              , [res_trans_success_memorder.control; res_trans_failure_memorder.control] )
+          | _ ->
+              assert false
+        in
+        let res_trans_ptr = instruction trans_state' ptr in
+        let ptr_exp, _ = res_trans_ptr.return in
+        let ptr_id = Ident.create_fresh Ident.knormal in
+        let res_trans_expected = instruction trans_state' expected in
+        let expected_exp, _ = res_trans_expected.return in
+        let expected_id = Ident.create_fresh Ident.knormal in
+        let res_trans_desired = instruction trans_state' desired in
+        let (desired_exp, typ), desired_instrs =
+          match atomic_expr_info.Clang_ast_t.aei_kind with
+          | `AO__atomic_compare_exchange -> (
+            match res_trans_desired.return with
+            | exp, typ ->
+                let desired_id = Ident.create_fresh Ident.knormal in
+                let typ = Typ.strip_ptr typ in
+                ( (Exp.Var desired_id, typ)
+                , [Sil.Load {id= desired_id; e= exp; root_typ= typ; typ; loc= sil_loc}] ) )
+          | _ ->
+              (res_trans_desired.return, [])
+        in
+        let is_expected_cond = Exp.BinOp (Binop.Eq, Exp.Var ptr_id, Exp.Var expected_id) in
+        let load_instrs =
+          [ Sil.Load {id= ptr_id; e= ptr_exp; root_typ= typ; typ; loc= sil_loc}
+          ; Sil.Load {id= expected_id; e= expected_exp; root_typ= typ; typ; loc= sil_loc} ]
+          @ desired_instrs
+        in
+        let join_node = Procdesc.create_node context.procdesc sil_loc Join_node [] in
+        Procdesc.node_set_succs context.procdesc join_node ~normal:trans_state.succ_nodes ~exn:[] ;
+        let var_exp_typ =
+          match trans_state.var_exp_typ with
+          | Some var_exp_typ ->
+              `ParentExp var_exp_typ
+          | None ->
+              let pvar =
+                CVar_decl.mk_temp_sil_var context.procdesc ~name:"SIL_temp_compare_exchange___"
+              in
+              let var_data =
+                ProcAttributes.
+                  { name= Pvar.get_name pvar
+                  ; typ= ret_typ
+                  ; modify_in_block= false
+                  ; is_constexpr= false
+                  ; is_declared_unused= false }
+              in
+              Procdesc.append_locals context.procdesc [var_data] ;
+              `Temp pvar
+        in
+        let do_branch trans_state branch exp_to_init =
+          let trans_state_pri = PriorityNode.force_claim_priority_node trans_state stmt_info in
+          let prune_node =
+            create_prune_node context.procdesc ~branch ~negate_cond:(not branch) is_expected_cond []
+              sil_loc Sil.Ik_compexch
+          in
+          let instrs =
+            if branch then
+              [ Sil.Store {e1= ptr_exp; e2= desired_exp; root_typ= typ; typ; loc= sil_loc}
+              ; Sil.Store
+                  {e1= exp_to_init; e2= Exp.one; root_typ= ret_typ; typ= ret_typ; loc= sil_loc} ]
+            else
+              [ Sil.Store {e1= expected_exp; e2= Exp.Var ptr_id; root_typ= typ; typ; loc= sil_loc}
+              ; Sil.Store
+                  {e1= exp_to_init; e2= Exp.zero; root_typ= ret_typ; typ= ret_typ; loc= sil_loc} ]
+          in
+          let return = (exp_to_init, ret_typ) in
+          let res_trans =
+            PriorityNode.compute_results_to_parent trans_state_pri sil_loc
+              AtomicCompareExchangeBranch stmt_info ~return
+              [mk_trans_result return {empty_control with instrs; initd_exps= [exp_to_init]}]
+          in
+          Procdesc.node_set_succs context.procdesc prune_node ~normal:res_trans.control.root_nodes
+            ~exn:[] ;
+          prune_node
+        in
+        let exp_to_init =
+          match var_exp_typ with `ParentExp (exp, _) -> exp | `Temp pvar -> Exp.Lvar pvar
+        in
+        let prune_success = do_branch {trans_state with succ_nodes= [join_node]} true exp_to_init in
+        let prune_failure =
+          do_branch {trans_state with succ_nodes= [join_node]} false exp_to_init
+        in
+        let instrs, return =
+          match var_exp_typ with
+          | `ParentExp var_exp_typ ->
+              ([], var_exp_typ)
+          | `Temp pvar ->
+              let id = Ident.create_fresh Ident.knormal in
+              ( [Sil.Load {id; e= Lvar pvar; root_typ= ret_typ; typ= ret_typ; loc= sil_loc}]
+              , (Exp.Var id, ret_typ) )
+        in
+        let load_controls =
+          mem_controls
+          @ [ res_trans_ptr.control
+            ; res_trans_expected.control
+            ; res_trans_desired.control
+            ; {empty_control with instrs= load_instrs} ]
+        in
+        let trans_state_pri = PriorityNode.force_claim_priority_node trans_state stmt_info in
+        let control =
+          PriorityNode.compute_controls_to_parent trans_state_pri sil_loc node_name stmt_info
+            load_controls
+        in
+        List.iter
+          ~f:(fun n ->
+            Procdesc.node_set_succs context.procdesc n ~normal:[prune_success; prune_failure]
+              ~exn:[] )
+          control.leaf_nodes ;
+        mk_trans_result return
+          {control with instrs; initd_exps= [exp_to_init]; leaf_nodes= [join_node]}
+    | `AO__atomic_fetch_max ->
+        handle_unimplemented BuiltinDecl.__atomic_fetch_max
+    | `AO__atomic_fetch_min ->
+        handle_unimplemented BuiltinDecl.__atomic_fetch_min
+    | `AO__atomic_fetch_nand ->
+        handle_unimplemented BuiltinDecl.__atomic_fetch_nand
+    | `AO__atomic_max_fetch ->
+        handle_unimplemented BuiltinDecl.__atomic_max_fetch
+    | `AO__atomic_min_fetch ->
+        handle_unimplemented BuiltinDecl.__atomic_min_fetch
+    | `AO__atomic_nand_fetch ->
+        handle_unimplemented BuiltinDecl.__atomic_nand_fetch
+    | `AO__c11_atomic_fetch_max ->
+        handle_unimplemented BuiltinDecl.__c11_atomic_fetch_max
+    | `AO__c11_atomic_fetch_min ->
+        handle_unimplemented BuiltinDecl.__c11_atomic_fetch_min
+    | `AO__opencl_atomic_fetch_max ->
+        handle_unimplemented BuiltinDecl.__opencl_atomic_fetch_max
+    | `AO__opencl_atomic_fetch_min ->
+        handle_unimplemented BuiltinDecl.__opencl_atomic_fetch_min
+
+
   and callExpr_trans trans_state si stmt_list expr_info =
     let context = trans_state.context in
     let fn_type_no_ref = CType_decl.get_type_from_expr_info expr_info context.CContext.tenv in
@@ -4295,6 +4706,8 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
         arraySubscriptExpr_trans trans_state expr_info stmt_list
     | BinaryOperator (stmt_info, stmt_list, expr_info, binop_info) ->
         binaryOperator_trans_with_cond trans_state stmt_info stmt_list expr_info binop_info
+    | AtomicExpr (stmt_info, stmt_list, expr_info, atomic_info) ->
+        atomicExpr_trans trans_state atomic_info stmt_info expr_info stmt_list
     | CallExpr (stmt_info, stmt_list, ei) | UserDefinedLiteral (stmt_info, stmt_list, ei) ->
         callExpr_trans trans_state stmt_info stmt_list ei
     | ConstantExpr (_, stmt_list, _) -> (
@@ -4544,7 +4957,6 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
     | AddrLabelExpr _
     | ArrayTypeTraitExpr _
     | AsTypeExpr _
-    | AtomicExpr _
     | CapturedStmt _
     | ChooseExpr _
     | CoawaitExpr _

infer/tests/codetoanalyze/c/frontend/atomic_expr/arithmetic.c

@@ -0,0 +1,67 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+#include <stdatomic.h>
+
+void c11_builtins() {
+  int _a;
+  atomic_int a;
+  atomic_init(&a, 0);
+  _a = atomic_fetch_add(&a, 1);
+  _a = atomic_fetch_sub(&a, 1);
+  _a = atomic_fetch_and(&a, 1);
+  _a = atomic_fetch_or(&a, 1);
+  _a = atomic_fetch_xor(&a, 1);
+}
+
+void opencl_builtins() {
+  int _o;
+  atomic_int o;
+  __opencl_atomic_init(&o, 0);
+  _o = __opencl_atomic_fetch_add(
+      &o, 1, __ATOMIC_SEQ_CST, __OPENCL_MEMORY_SCOPE_WORK_GROUP);
+  _o = __opencl_atomic_fetch_sub(
+      &o, 1, __ATOMIC_SEQ_CST, __OPENCL_MEMORY_SCOPE_WORK_GROUP);
+  _o = __opencl_atomic_fetch_and(
+      &o, 1, __ATOMIC_SEQ_CST, __OPENCL_MEMORY_SCOPE_WORK_GROUP);
+  _o = __opencl_atomic_fetch_or(
+      &o, 1, __ATOMIC_SEQ_CST, __OPENCL_MEMORY_SCOPE_WORK_GROUP);
+  _o = __opencl_atomic_fetch_xor(
+      &o, 1, __ATOMIC_SEQ_CST, __OPENCL_MEMORY_SCOPE_WORK_GROUP);
+}
+
+void gnu_builtins() {
+  int _i;
+  int i = 0;
+  _i = __atomic_fetch_add(&i, 1, __ATOMIC_SEQ_CST);
+  _i = __atomic_fetch_sub(&i, 1, __ATOMIC_SEQ_CST);
+  _i = __atomic_fetch_and(&i, 1, __ATOMIC_SEQ_CST);
+  _i = __atomic_fetch_or(&i, 1, __ATOMIC_SEQ_CST);
+  _i = __atomic_fetch_xor(&i, 1, __ATOMIC_SEQ_CST);
+  _i = __atomic_add_fetch(&i, 1, __ATOMIC_SEQ_CST);
+  _i = __atomic_sub_fetch(&i, 1, __ATOMIC_SEQ_CST);
+  _i = __atomic_and_fetch(&i, 1, __ATOMIC_SEQ_CST);
+  _i = __atomic_or_fetch(&i, 1, __ATOMIC_SEQ_CST);
+  _i = __atomic_xor_fetch(&i, 1, __ATOMIC_SEQ_CST);
+}
+
+void unimplemented() {
+  int i;
+  atomic_int a;
+  __atomic_fetch_max(&i, 0, __ATOMIC_SEQ_CST);
+  __atomic_fetch_min(&i, 0, __ATOMIC_SEQ_CST);
+  __atomic_fetch_nand(&i, 0, __ATOMIC_SEQ_CST);
+  __atomic_max_fetch(&i, 0, __ATOMIC_SEQ_CST);
+  __atomic_min_fetch(&i, 0, __ATOMIC_SEQ_CST);
+  __atomic_nand_fetch(&i, 0, __ATOMIC_SEQ_CST);
+  __c11_atomic_fetch_max(&a, 0, __ATOMIC_SEQ_CST);
+  __c11_atomic_fetch_min(&a, 0, __ATOMIC_SEQ_CST);
+  __opencl_atomic_fetch_max(
+      &a, 0, __ATOMIC_SEQ_CST, __OPENCL_MEMORY_SCOPE_WORK_GROUP);
+  __opencl_atomic_fetch_min(
+      &a, 0, __ATOMIC_SEQ_CST, __OPENCL_MEMORY_SCOPE_WORK_GROUP);
+}

infer/tests/codetoanalyze/c/frontend/atomic_expr/arithmetic.c.dot

@@ -0,0 +1,163 @@
+/* @generated */
+digraph cfg {
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_1" [label="1: Start c11_builtins\nFormals: \nLocals:  a:void _a:int \n  " color=yellow style=filled]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_1" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_8" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_2" [label="2: Exit c11_builtins \n  " color=yellow style=filled]
+	
+
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_3" [label="3:  BinaryOperatorStmt: Assign \n   n$0=*&a:int [line 18, column 8]\n  *&a:int=(n$0 ^ 1) [line 18, column 8]\n  *&_a:int=n$0 [line 18, column 3]\n " shape="box"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_3" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_2" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_4" [label="4:  BinaryOperatorStmt: Assign \n   n$1=*&a:int [line 17, column 8]\n  *&a:int=(n$1 | 1) [line 17, column 8]\n  *&_a:int=n$1 [line 17, column 3]\n " shape="box"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_4" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_3" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_5" [label="5:  BinaryOperatorStmt: Assign \n   n$2=*&a:int [line 16, column 8]\n  *&a:int=(n$2 & 1) [line 16, column 8]\n  *&_a:int=n$2 [line 16, column 3]\n " shape="box"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_5" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_4" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_6" [label="6:  BinaryOperatorStmt: Assign \n   n$3=*&a:int [line 15, column 8]\n  *&a:int=(n$3 - 1) [line 15, column 8]\n  *&_a:int=n$3 [line 15, column 3]\n " shape="box"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_6" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_5" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_7" [label="7:  BinaryOperatorStmt: Assign \n   n$4=*&a:int [line 14, column 8]\n  *&a:int=(n$4 + 1) [line 14, column 8]\n  *&_a:int=n$4 [line 14, column 3]\n " shape="box"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_7" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_6" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_8" [label="8:  AtomicExpr \n   *&a:int=0 [line 13, column 3]\n " shape="box"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_8" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_7" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_1" [label="1: Start gnu_builtins\nFormals: \nLocals:  i:int _i:int \n  " color=yellow style=filled]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_1" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_13" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_2" [label="2: Exit gnu_builtins \n  " color=yellow style=filled]
+	
+
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_3" [label="3:  BinaryOperatorStmt: Assign \n   n$0=*&i:int [line 49, column 8]\n  *&i:int=(n$0 ^ 1) [line 49, column 8]\n  n$1=*&i:int [line 49, column 8]\n  *&_i:int=n$1 [line 49, column 3]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_3" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_2" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_4" [label="4:  BinaryOperatorStmt: Assign \n   n$2=*&i:int [line 48, column 8]\n  *&i:int=(n$2 | 1) [line 48, column 8]\n  n$3=*&i:int [line 48, column 8]\n  *&_i:int=n$3 [line 48, column 3]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_4" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_3" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_5" [label="5:  BinaryOperatorStmt: Assign \n   n$4=*&i:int [line 47, column 8]\n  *&i:int=(n$4 & 1) [line 47, column 8]\n  n$5=*&i:int [line 47, column 8]\n  *&_i:int=n$5 [line 47, column 3]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_5" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_4" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_6" [label="6:  BinaryOperatorStmt: Assign \n   n$6=*&i:int [line 46, column 8]\n  *&i:int=(n$6 - 1) [line 46, column 8]\n  n$7=*&i:int [line 46, column 8]\n  *&_i:int=n$7 [line 46, column 3]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_6" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_5" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_7" [label="7:  BinaryOperatorStmt: Assign \n   n$8=*&i:int [line 45, column 8]\n  *&i:int=(n$8 + 1) [line 45, column 8]\n  n$9=*&i:int [line 45, column 8]\n  *&_i:int=n$9 [line 45, column 3]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_7" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_6" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_8" [label="8:  BinaryOperatorStmt: Assign \n   n$10=*&i:int [line 44, column 8]\n  *&i:int=(n$10 ^ 1) [line 44, column 8]\n  *&_i:int=n$10 [line 44, column 3]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_8" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_7" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_9" [label="9:  BinaryOperatorStmt: Assign \n   n$11=*&i:int [line 43, column 8]\n  *&i:int=(n$11 | 1) [line 43, column 8]\n  *&_i:int=n$11 [line 43, column 3]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_9" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_8" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_10" [label="10:  BinaryOperatorStmt: Assign \n   n$12=*&i:int [line 42, column 8]\n  *&i:int=(n$12 & 1) [line 42, column 8]\n  *&_i:int=n$12 [line 42, column 3]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_10" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_9" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_11" [label="11:  BinaryOperatorStmt: Assign \n   n$13=*&i:int [line 41, column 8]\n  *&i:int=(n$13 - 1) [line 41, column 8]\n  *&_i:int=n$13 [line 41, column 3]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_11" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_10" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_12" [label="12:  BinaryOperatorStmt: Assign \n   n$14=*&i:int [line 40, column 8]\n  *&i:int=(n$14 + 1) [line 40, column 8]\n  *&_i:int=n$14 [line 40, column 3]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_12" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_11" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_13" [label="13:  DeclStmt \n   VARIABLE_DECLARED(i:int); [line 39, column 3]\n  *&i:int=0 [line 39, column 3]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_13" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_12" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_1" [label="1: Start opencl_builtins\nFormals: \nLocals:  o:void _o:int \n  " color=yellow style=filled]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_1" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_8" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_2" [label="2: Exit opencl_builtins \n  " color=yellow style=filled]
+	
+
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_3" [label="3:  BinaryOperatorStmt: Assign \n   n$0=*&o:int [line 33, column 8]\n  *&o:int=(n$0 ^ 1) [line 33, column 8]\n  *&_o:int=n$0 [line 33, column 3]\n " shape="box"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_3" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_2" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_4" [label="4:  BinaryOperatorStmt: Assign \n   n$1=*&o:int [line 31, column 8]\n  *&o:int=(n$1 | 1) [line 31, column 8]\n  *&_o:int=n$1 [line 31, column 3]\n " shape="box"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_4" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_3" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_5" [label="5:  BinaryOperatorStmt: Assign \n   n$2=*&o:int [line 29, column 8]\n  *&o:int=(n$2 & 1) [line 29, column 8]\n  *&_o:int=n$2 [line 29, column 3]\n " shape="box"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_5" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_4" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_6" [label="6:  BinaryOperatorStmt: Assign \n   n$3=*&o:int [line 27, column 8]\n  *&o:int=(n$3 - 1) [line 27, column 8]\n  *&_o:int=n$3 [line 27, column 3]\n " shape="box"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_6" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_5" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_7" [label="7:  BinaryOperatorStmt: Assign \n   n$4=*&o:int [line 25, column 8]\n  *&o:int=(n$4 + 1) [line 25, column 8]\n  *&_o:int=n$4 [line 25, column 3]\n " shape="box"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_7" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_6" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_8" [label="8:  AtomicExpr \n   *&o:int=0 [line 24, column 3]\n " shape="box"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_8" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_7" ;
+"unimplemented.4316423dfe3ade85c292aa38185f9817_1" [label="1: Start unimplemented\nFormals: \nLocals:  a:void i:int \n  " color=yellow style=filled]
+	
+
+	 "unimplemented.4316423dfe3ade85c292aa38185f9817_1" -> "unimplemented.4316423dfe3ade85c292aa38185f9817_12" ;
+"unimplemented.4316423dfe3ade85c292aa38185f9817_2" [label="2: Exit unimplemented \n  " color=yellow style=filled]
+	
+
+"unimplemented.4316423dfe3ade85c292aa38185f9817_3" [label="3:  AtomicExpr \n   n$0=_fun___opencl_atomic_fetch_min(&a:void*,5:int,0:int,1:int) [line 65, column 3]\n " shape="box"]
+	
+
+	 "unimplemented.4316423dfe3ade85c292aa38185f9817_3" -> "unimplemented.4316423dfe3ade85c292aa38185f9817_2" ;
+"unimplemented.4316423dfe3ade85c292aa38185f9817_4" [label="4:  AtomicExpr \n   n$1=_fun___opencl_atomic_fetch_max(&a:void*,5:int,0:int,1:int) [line 63, column 3]\n " shape="box"]
+	
+
+	 "unimplemented.4316423dfe3ade85c292aa38185f9817_4" -> "unimplemented.4316423dfe3ade85c292aa38185f9817_3" ;
+"unimplemented.4316423dfe3ade85c292aa38185f9817_5" [label="5:  AtomicExpr \n   n$2=_fun___c11_atomic_fetch_min(&a:void*,5:int,0:int) [line 62, column 3]\n " shape="box"]
+	
+
+	 "unimplemented.4316423dfe3ade85c292aa38185f9817_5" -> "unimplemented.4316423dfe3ade85c292aa38185f9817_4" ;
+"unimplemented.4316423dfe3ade85c292aa38185f9817_6" [label="6:  AtomicExpr \n   n$3=_fun___c11_atomic_fetch_max(&a:void*,5:int,0:int) [line 61, column 3]\n " shape="box"]
+	
+
+	 "unimplemented.4316423dfe3ade85c292aa38185f9817_6" -> "unimplemented.4316423dfe3ade85c292aa38185f9817_5" ;
+"unimplemented.4316423dfe3ade85c292aa38185f9817_7" [label="7:  AtomicExpr \n   n$4=_fun___atomic_nand_fetch(&i:int*,5:int,0:int) [line 60, column 3]\n " shape="box"]
+	
+
+	 "unimplemented.4316423dfe3ade85c292aa38185f9817_7" -> "unimplemented.4316423dfe3ade85c292aa38185f9817_6" ;
+"unimplemented.4316423dfe3ade85c292aa38185f9817_8" [label="8:  AtomicExpr \n   n$5=_fun___atomic_min_fetch(&i:int*,5:int,0:int) [line 59, column 3]\n " shape="box"]
+	
+
+	 "unimplemented.4316423dfe3ade85c292aa38185f9817_8" -> "unimplemented.4316423dfe3ade85c292aa38185f9817_7" ;
+"unimplemented.4316423dfe3ade85c292aa38185f9817_9" [label="9:  AtomicExpr \n   n$6=_fun___atomic_max_fetch(&i:int*,5:int,0:int) [line 58, column 3]\n " shape="box"]
+	
+
+	 "unimplemented.4316423dfe3ade85c292aa38185f9817_9" -> "unimplemented.4316423dfe3ade85c292aa38185f9817_8" ;
+"unimplemented.4316423dfe3ade85c292aa38185f9817_10" [label="10:  AtomicExpr \n   n$7=_fun___atomic_fetch_nand(&i:int*,5:int,0:int) [line 57, column 3]\n " shape="box"]
+	
+
+	 "unimplemented.4316423dfe3ade85c292aa38185f9817_10" -> "unimplemented.4316423dfe3ade85c292aa38185f9817_9" ;
+"unimplemented.4316423dfe3ade85c292aa38185f9817_11" [label="11:  AtomicExpr \n   n$8=_fun___atomic_fetch_min(&i:int*,5:int,0:int) [line 56, column 3]\n " shape="box"]
+	
+
+	 "unimplemented.4316423dfe3ade85c292aa38185f9817_11" -> "unimplemented.4316423dfe3ade85c292aa38185f9817_10" ;
+"unimplemented.4316423dfe3ade85c292aa38185f9817_12" [label="12:  AtomicExpr \n   n$9=_fun___atomic_fetch_max(&i:int*,5:int,0:int) [line 55, column 3]\n " shape="box"]
+	
+
+	 "unimplemented.4316423dfe3ade85c292aa38185f9817_12" -> "unimplemented.4316423dfe3ade85c292aa38185f9817_11" ;
+}

infer/tests/codetoanalyze/c/frontend/atomic_expr/atomic_with_others.c

@@ -0,0 +1,56 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+#include <stdatomic.h>
+#include <stdbool.h>
+
+int other_func(int a, int* b);
+
+void arithmetic() {
+  int _a;
+  int* p = &_a;
+  atomic_int a;
+  atomic_int a2;
+  atomic_init(&a, 0);
+  _a = atomic_fetch_add(&a, _a << 2);
+  _a = atomic_fetch_sub(&a, atomic_fetch_add(&a2, a ? 5 : _a));
+  _a = __opencl_atomic_fetch_add(&a,
+                                 1,
+                                 a ? __atomic_sub_fetch(p, 5, 0) : 10,
+                                 __OPENCL_MEMORY_SCOPE_WORK_GROUP);
+  _a = *__atomic_fetch_add(
+      &p, __atomic_or_fetch(&_a, _a = 0, __ATOMIC_SEQ_CST), 1);
+  _a = __opencl_atomic_fetch_or(&a,
+                                other_func(0, NULL),
+                                __ATOMIC_SEQ_CST,
+                                __OPENCL_MEMORY_SCOPE_WORK_GROUP);
+  _a = other_func(atomic_fetch_xor(&a, 1) + 5, 0);
+}
+
+void load_store_exchange() {
+  bool b;
+  int** p;
+  int _a;
+  atomic_int a;
+  atomic_int a2;
+  atomic_init(&a, 1 + _a);
+  _a = (atomic_load(&a) ? 5 : 2);
+  _a = atomic_load(b ? &a : &a2);
+  __opencl_atomic_store(
+      b ? &a : &a2, 1, _a++ - 20, __OPENCL_MEMORY_SCOPE_WORK_GROUP);
+  _a = atomic_exchange(&a, 2);
+  other_func(atomic_exchange(&a2, 2), 0);
+  other_func(__atomic_compare_exchange_n(
+                 *p, &_a, **p, true, _a + **p, other_func(0, NULL)),
+             0);
+  __atomic_compare_exchange_n(&_a,
+                              *p,
+                              other_func(0, NULL),
+                              ++_a | 8,
+                              other_func(0, NULL),
+                              other_func(atomic_load(&a), NULL));
+}

infer/tests/codetoanalyze/c/frontend/atomic_expr/atomic_with_others.c.dot

@@ -0,0 +1,240 @@
+/* @generated */
+digraph cfg {
+"arithmetic.26e816805c2eb54063da29d3d21a3641_1" [label="1: Start arithmetic\nFormals: \nLocals:  0$?%__sil_tmpSIL_temp_conditional___n$9:int 0$?%__sil_tmpSIL_temp_conditional___n$16:int a2:void a:void p:int* _a:int \n  " color=yellow style=filled]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_1" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_20" ;
+"arithmetic.26e816805c2eb54063da29d3d21a3641_2" [label="2: Exit arithmetic \n  " color=yellow style=filled]
+	
+
+"arithmetic.26e816805c2eb54063da29d3d21a3641_3" [label="3:  BinaryOperatorStmt: Assign \n   n$0=*&a:int [line 31, column 19]\n  *&a:int=(n$0 ^ 1) [line 31, column 19]\n  n$1=_fun_other_func((n$0 + 5):int,null:int*) [line 31, column 8]\n  *&_a:int=n$1 [line 31, column 3]\n " shape="box"]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_3" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_2" ;
+"arithmetic.26e816805c2eb54063da29d3d21a3641_4" [label="4:  BinaryOperatorStmt: Assign \n   n$2=_fun_other_func(0:int,null:int*) [line 28, column 33]\n  n$3=*&a:int [line 27, column 8]\n  *&a:int=(n$3 | n$2) [line 27, column 8]\n  *&_a:int=n$3 [line 27, column 3]\n " shape="box"]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_4" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_3" ;
+"arithmetic.26e816805c2eb54063da29d3d21a3641_5" [label="5:  BinaryOperatorStmt: Assign \n   *&_a:int=0 [line 26, column 34]\n  n$4=*&_a:int [line 26, column 34]\n  n$5=*&_a:int [line 26, column 11]\n  *&_a:int=(n$5 | n$4) [line 26, column 11]\n  n$6=*&_a:int [line 26, column 11]\n  n$7=*&p:int* [line 25, column 9]\n  *&p:int*=(n$7 + n$6) [line 25, column 9]\n  n$8=*n$7:int [line 25, column 8]\n  *&_a:int=n$8 [line 25, column 3]\n " shape="box"]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_5" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_4" ;
+"arithmetic.26e816805c2eb54063da29d3d21a3641_6" [label="6: + \n  " ]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_6" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_11" ;
+"arithmetic.26e816805c2eb54063da29d3d21a3641_7" [label="7: Prune (true branch, boolean exp) \n   n$10=*&a:void [line 23, column 34]\n  PRUNE(n$10, true); [line 23, column 34]\n " shape="invhouse"]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_7" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_9" ;
+"arithmetic.26e816805c2eb54063da29d3d21a3641_8" [label="8: Prune (false branch, boolean exp) \n   n$10=*&a:void [line 23, column 34]\n  PRUNE(!n$10, false); [line 23, column 34]\n " shape="invhouse"]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_8" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_10" ;
+"arithmetic.26e816805c2eb54063da29d3d21a3641_9" [label="9:  ConditionalStmt Branch \n   n$11=*&p:int* [line 23, column 57]\n  n$12=*n$11:int [line 23, column 38]\n  *n$11:int=(n$12 - 5) [line 23, column 38]\n  n$13=*n$11:int [line 23, column 38]\n  *&0$?%__sil_tmpSIL_temp_conditional___n$9:int=n$13 [line 23, column 34]\n " shape="box"]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_9" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_6" ;
+"arithmetic.26e816805c2eb54063da29d3d21a3641_10" [label="10:  ConditionalStmt Branch \n   *&0$?%__sil_tmpSIL_temp_conditional___n$9:int=10 [line 23, column 34]\n " shape="box"]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_10" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_6" ;
+"arithmetic.26e816805c2eb54063da29d3d21a3641_11" [label="11:  BinaryOperatorStmt: Assign \n   n$14=*&0$?%__sil_tmpSIL_temp_conditional___n$9:int [line 23, column 34]\n  n$15=*&a:int [line 21, column 8]\n  *&a:int=(n$15 + 1) [line 21, column 8]\n  *&_a:int=n$15 [line 21, column 3]\n " shape="box"]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_11" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_5" ;
+"arithmetic.26e816805c2eb54063da29d3d21a3641_12" [label="12: + \n  " ]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_12" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_17" ;
+"arithmetic.26e816805c2eb54063da29d3d21a3641_13" [label="13: Prune (true branch, boolean exp) \n   n$17=*&a:void [line 20, column 8]\n  PRUNE(n$17, true); [line 20, column 8]\n " shape="invhouse"]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_13" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_15" ;
+"arithmetic.26e816805c2eb54063da29d3d21a3641_14" [label="14: Prune (false branch, boolean exp) \n   n$17=*&a:void [line 20, column 8]\n  PRUNE(!n$17, false); [line 20, column 8]\n " shape="invhouse"]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_14" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_16" ;
+"arithmetic.26e816805c2eb54063da29d3d21a3641_15" [label="15:  ConditionalStmt Branch \n   *&0$?%__sil_tmpSIL_temp_conditional___n$16:int=5 [line 20, column 8]\n " shape="box"]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_15" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_12" ;
+"arithmetic.26e816805c2eb54063da29d3d21a3641_16" [label="16:  ConditionalStmt Branch \n   n$18=*&_a:int [line 20, column 8]\n  *&0$?%__sil_tmpSIL_temp_conditional___n$16:int=n$18 [line 20, column 8]\n " shape="box"]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_16" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_12" ;
+"arithmetic.26e816805c2eb54063da29d3d21a3641_17" [label="17:  BinaryOperatorStmt: Assign \n   n$19=*&0$?%__sil_tmpSIL_temp_conditional___n$16:int [line 20, column 8]\n  n$20=*&a2:int [line 20, column 8]\n  *&a2:int=(n$20 + n$19) [line 20, column 8]\n  n$21=*&a:int [line 20, column 8]\n  *&a:int=(n$21 - n$20) [line 20, column 8]\n  *&_a:int=n$21 [line 20, column 3]\n " shape="box"]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_17" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_7" ;
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_17" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_8" ;
+"arithmetic.26e816805c2eb54063da29d3d21a3641_18" [label="18:  BinaryOperatorStmt: Assign \n   n$22=*&_a:int [line 19, column 8]\n  n$23=*&a:int [line 19, column 8]\n  *&a:int=(n$23 + (n$22 << 2)) [line 19, column 8]\n  *&_a:int=n$23 [line 19, column 3]\n " shape="box"]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_18" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_13" ;
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_18" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_14" ;
+"arithmetic.26e816805c2eb54063da29d3d21a3641_19" [label="19:  AtomicExpr \n   *&a:int=0 [line 18, column 3]\n " shape="box"]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_19" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_18" ;
+"arithmetic.26e816805c2eb54063da29d3d21a3641_20" [label="20:  DeclStmt \n   VARIABLE_DECLARED(p:int*); [line 15, column 3]\n  *&p:int*=&_a [line 15, column 3]\n " shape="box"]
+	
+
+	 "arithmetic.26e816805c2eb54063da29d3d21a3641_20" -> "arithmetic.26e816805c2eb54063da29d3d21a3641_19" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_1" [label="1: Start load_store_exchange\nFormals: \nLocals:  0$?%__sil_tmpSIL_temp_compare_exchange___n$9:_Bool 0$?%__sil_tmpSIL_temp_compare_exchange___n$23:_Bool 0$?%__sil_tmpSIL_temp_conditional___n$30:void* 0$?%__sil_tmpSIL_temp_conditional___n$34:void* a2:void a:void _a:int p:int** b:_Bool \n  " color=yellow style=filled]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_1" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_38" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_2" [label="2: Exit load_store_exchange \n  " color=yellow style=filled]
+	
+
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_3" [label="3: + \n  " ]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_3" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_10" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_4" [label="4:  between_join_and_exit \n  " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_4" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_2" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_5" [label="5: Prune (true branch, atomic compare exchange) \n   PRUNE((n$4 == n$7), true); [line 50, column 3]\n " shape="invhouse"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_5" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_6" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_6" [label="6:  Atomic compare exchange branch \n   *&_a:int=n$8 [line 50, column 3]\n  *&0$?%__sil_tmpSIL_temp_compare_exchange___n$9:_Bool=1 [line 50, column 3]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_6" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_3" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_7" [label="7: Prune (false branch, atomic compare exchange) \n   PRUNE(!(n$4 == n$7), false); [line 50, column 3]\n " shape="invhouse"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_7" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_8" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_8" [label="8:  Atomic compare exchange branch \n   *n$6:int=n$4 [line 50, column 3]\n  *&0$?%__sil_tmpSIL_temp_compare_exchange___n$9:_Bool=0 [line 50, column 3]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_8" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_3" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_9" [label="9:  AtomicExpr \n   n$0=_fun_other_func(0:int,null:int*) [line 54, column 31]\n  n$1=*&a:int [line 55, column 42]\n  n$2=_fun_other_func(n$1:int,null:int*) [line 55, column 31]\n  n$3=*&_a:int [line 53, column 31]\n  *&_a:int=(n$3 + 1) [line 53, column 31]\n  n$5=*&p:int** [line 51, column 32]\n  n$6=*n$5:int* [line 51, column 31]\n  n$8=_fun_other_func(0:int,null:int*) [line 52, column 31]\n  n$4=*&_a:int [line 50, column 3]\n  n$7=*n$6:int [line 50, column 3]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_9" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_5" ;
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_9" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_7" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_10" [label="10:  Compound statement \n   n$10=*&0$?%__sil_tmpSIL_temp_compare_exchange___n$9:_Bool [line 50, column 3]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_10" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_2" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_11" [label="11: + \n  " ]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_11" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_17" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_12" [label="12: Prune (true branch, atomic compare exchange) \n   PRUNE((n$18 == n$19), true); [line 47, column 14]\n " shape="invhouse"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_12" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_13" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_13" [label="13:  Atomic compare exchange branch \n   *n$17:int=n$22 [line 47, column 14]\n  *&0$?%__sil_tmpSIL_temp_compare_exchange___n$23:_Bool=1 [line 47, column 14]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_13" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_11" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_14" [label="14: Prune (false branch, atomic compare exchange) \n   PRUNE(!(n$18 == n$19), false); [line 47, column 14]\n " shape="invhouse"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_14" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_15" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_15" [label="15:  Atomic compare exchange branch \n   *&_a:int=n$18 [line 47, column 14]\n  *&0$?%__sil_tmpSIL_temp_compare_exchange___n$23:_Bool=0 [line 47, column 14]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_15" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_11" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_16" [label="16:  AtomicExpr \n   n$11=*&_a:int [line 48, column 38]\n  n$12=*&p:int** [line 48, column 45]\n  n$13=*n$12:int* [line 48, column 44]\n  n$14=*n$13:int [line 48, column 43]\n  n$15=_fun_other_func(0:int,null:int*) [line 48, column 48]\n  n$16=*&p:int** [line 48, column 19]\n  n$17=*n$16:int* [line 48, column 18]\n  n$20=*&p:int** [line 48, column 29]\n  n$21=*n$20:int* [line 48, column 28]\n  n$22=*n$21:int [line 48, column 27]\n  n$18=*n$17:int [line 47, column 14]\n  n$19=*&_a:int [line 47, column 14]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_16" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_12" ;
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_16" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_14" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_17" [label="17:  Call _fun_other_func \n   n$24=*&0$?%__sil_tmpSIL_temp_compare_exchange___n$23:_Bool [line 47, column 14]\n  n$25=_fun_other_func(n$24:int,null:int*) [line 47, column 3]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_17" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_9" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_18" [label="18:  Call _fun_other_func \n   n$26=*&a2:int [line 46, column 14]\n  *&a2:int=2 [line 46, column 14]\n  n$27=_fun_other_func(n$26:int,null:int*) [line 46, column 3]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_18" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_16" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_19" [label="19:  BinaryOperatorStmt: Assign \n   n$28=*&a:int [line 45, column 8]\n  *&a:int=2 [line 45, column 8]\n  *&_a:int=n$28 [line 45, column 3]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_19" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_18" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_20" [label="20: + \n  " ]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_20" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_25" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_21" [label="21: Prune (true branch, boolean exp) \n   n$31=*&b:_Bool [line 44, column 7]\n  PRUNE(n$31, true); [line 44, column 7]\n " shape="invhouse"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_21" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_23" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_22" [label="22: Prune (false branch, boolean exp) \n   n$31=*&b:_Bool [line 44, column 7]\n  PRUNE(!n$31, false); [line 44, column 7]\n " shape="invhouse"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_22" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_24" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_23" [label="23:  ConditionalStmt Branch \n   *&0$?%__sil_tmpSIL_temp_conditional___n$30:void*=&a [line 44, column 7]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_23" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_20" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_24" [label="24:  ConditionalStmt Branch \n   *&0$?%__sil_tmpSIL_temp_conditional___n$30:void*=&a2 [line 44, column 7]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_24" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_20" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_25" [label="25:  AtomicExpr \n   n$29=*&_a:int [line 44, column 24]\n  *&_a:int=(n$29 + 1) [line 44, column 24]\n  n$32=*&0$?%__sil_tmpSIL_temp_conditional___n$30:void* [line 44, column 7]\n  *n$32:int=1 [line 43, column 3]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_25" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_19" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_26" [label="26: + \n  " ]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_26" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_31" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_27" [label="27: Prune (true branch, boolean exp) \n   n$35=*&b:_Bool [line 42, column 8]\n  PRUNE(n$35, true); [line 42, column 8]\n " shape="invhouse"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_27" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_29" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_28" [label="28: Prune (false branch, boolean exp) \n   n$35=*&b:_Bool [line 42, column 8]\n  PRUNE(!n$35, false); [line 42, column 8]\n " shape="invhouse"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_28" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_30" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_29" [label="29:  ConditionalStmt Branch \n   *&0$?%__sil_tmpSIL_temp_conditional___n$34:void*=&a [line 42, column 8]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_29" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_26" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_30" [label="30:  ConditionalStmt Branch \n   *&0$?%__sil_tmpSIL_temp_conditional___n$34:void*=&a2 [line 42, column 8]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_30" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_26" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_31" [label="31:  BinaryOperatorStmt: Assign \n   n$36=*&0$?%__sil_tmpSIL_temp_conditional___n$34:void* [line 42, column 8]\n  n$37=*n$36:int [line 42, column 8]\n  *&_a:int=n$37 [line 42, column 3]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_31" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_21" ;
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_31" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_22" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_32" [label="32: + \n  " ]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_32" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_27" ;
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_32" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_28" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_33" [label="33:  AtomicExpr \n   n$38=*&a:int [line 41, column 9]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_33" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_34" ;
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_33" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_35" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_34" [label="34: Prune (true branch, boolean exp) \n   PRUNE(n$38, true); [line 41, column 9]\n " shape="invhouse"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_34" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_36" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_35" [label="35: Prune (false branch, boolean exp) \n   PRUNE(!n$38, false); [line 41, column 9]\n " shape="invhouse"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_35" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_37" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_36" [label="36:  ConditionalStmt Branch \n   *&_a:int=5 [line 41, column 9]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_36" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_32" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_37" [label="37:  ConditionalStmt Branch \n   *&_a:int=2 [line 41, column 9]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_37" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_32" ;
+"load_store_exchange.3da178fb2a20c1b276e1502becee6b78_38" [label="38:  AtomicExpr \n   n$39=*&_a:int [line 40, column 23]\n  *&a:int=(1 + n$39) [line 40, column 3]\n " shape="box"]
+	
+
+	 "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_38" -> "load_store_exchange.3da178fb2a20c1b276e1502becee6b78_33" ;
+}

infer/tests/codetoanalyze/c/frontend/atomic_expr/load_store_exchange.c

@@ -0,0 +1,63 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+#include <stdatomic.h>
+#include <stdbool.h>
+
+void c11_builtins() {
+  bool b;
+  int _a;
+  atomic_int a;
+  atomic_init(&a, 0);
+  _a = atomic_load(&a);
+  atomic_store(&a, 1);
+  _a = atomic_exchange(&a, 2);
+  b = atomic_compare_exchange_strong(&a, &_a, 0);
+  b = atomic_compare_exchange_weak(&a, &_a, 0);
+}
+
+void opencl_builtins() {
+  bool b;
+  int _o;
+  atomic_int o;
+  __opencl_atomic_init(&o, 0);
+  _o = __opencl_atomic_load(
+      &o, __ATOMIC_SEQ_CST, __OPENCL_MEMORY_SCOPE_WORK_GROUP);
+  __opencl_atomic_store(
+      &o, 1, __ATOMIC_SEQ_CST, __OPENCL_MEMORY_SCOPE_WORK_GROUP);
+  _o = __opencl_atomic_exchange(
+      &o, 2, __ATOMIC_SEQ_CST, __OPENCL_MEMORY_SCOPE_WORK_GROUP);
+  b = __opencl_atomic_compare_exchange_strong(&o,
+                                              &_o,
+                                              0,
+                                              __ATOMIC_SEQ_CST,
+                                              __ATOMIC_SEQ_CST,
+                                              __OPENCL_MEMORY_SCOPE_WORK_GROUP);
+  b = __opencl_atomic_compare_exchange_weak(&o,
+                                            &_o,
+                                            0,
+                                            __ATOMIC_SEQ_CST,
+                                            __ATOMIC_SEQ_CST,
+                                            __OPENCL_MEMORY_SCOPE_WORK_GROUP);
+}
+
+void gnu_builtins() {
+  bool b;
+  int _i;
+  int _a;
+  int i = 0;
+  _i = __atomic_load_n(&i, __ATOMIC_SEQ_CST);
+  __atomic_load(&i, &_i, __ATOMIC_SEQ_CST);
+  __atomic_store_n(&i, 1, __ATOMIC_SEQ_CST);
+  __atomic_store(&i, &_i, __ATOMIC_SEQ_CST);
+  _i = __atomic_exchange_n(&i, 1, __ATOMIC_SEQ_CST);
+  __atomic_exchange(&i, &_i, &_a, __ATOMIC_SEQ_CST);
+  b = __atomic_compare_exchange_n(
+      &i, &_i, 0, false, __ATOMIC_SEQ_CST, __ATOMIC_SEQ_CST);
+  b = __atomic_compare_exchange(
+      &i, &_i, &_a, false, __ATOMIC_SEQ_CST, __ATOMIC_SEQ_CST);
+}

infer/tests/codetoanalyze/c/frontend/atomic_expr/load_store_exchange.c.dot

@@ -0,0 +1,246 @@
+/* @generated */
+digraph cfg {
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_1" [label="1: Start c11_builtins\nFormals: \nLocals:  a:void _a:int b:_Bool \n  " color=yellow style=filled]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_1" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_19" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_2" [label="2: Exit c11_builtins \n  " color=yellow style=filled]
+	
+
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_3" [label="3: + \n  " ]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_3" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_4" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_4" [label="4:  between_join_and_exit \n  " shape="box"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_4" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_2" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_5" [label="5: Prune (true branch, atomic compare exchange) \n   PRUNE((n$0 == n$1), true); [line 20, column 7]\n " shape="invhouse"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_5" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_6" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_6" [label="6:  Atomic compare exchange branch \n   *&a:int=0 [line 20, column 7]\n  *&b:_Bool=1 [line 20, column 7]\n " shape="box"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_6" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_3" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_7" [label="7: Prune (false branch, atomic compare exchange) \n   PRUNE(!(n$0 == n$1), false); [line 20, column 7]\n " shape="invhouse"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_7" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_8" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_8" [label="8:  Atomic compare exchange branch \n   *&_a:int=n$0 [line 20, column 7]\n  *&b:_Bool=0 [line 20, column 7]\n " shape="box"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_8" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_3" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_9" [label="9:  AtomicExpr \n   n$0=*&a:int [line 20, column 7]\n  n$1=*&_a:int [line 20, column 7]\n " shape="box"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_9" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_5" ;
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_9" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_7" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_10" [label="10: + \n  " ]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_10" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_9" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_11" [label="11: Prune (true branch, atomic compare exchange) \n   PRUNE((n$2 == n$3), true); [line 19, column 7]\n " shape="invhouse"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_11" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_12" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_12" [label="12:  Atomic compare exchange branch \n   *&a:int=0 [line 19, column 7]\n  *&b:_Bool=1 [line 19, column 7]\n " shape="box"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_12" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_10" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_13" [label="13: Prune (false branch, atomic compare exchange) \n   PRUNE(!(n$2 == n$3), false); [line 19, column 7]\n " shape="invhouse"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_13" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_14" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_14" [label="14:  Atomic compare exchange branch \n   *&_a:int=n$2 [line 19, column 7]\n  *&b:_Bool=0 [line 19, column 7]\n " shape="box"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_14" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_10" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_15" [label="15:  AtomicExpr \n   n$2=*&a:int [line 19, column 7]\n  n$3=*&_a:int [line 19, column 7]\n " shape="box"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_15" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_11" ;
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_15" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_13" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_16" [label="16:  BinaryOperatorStmt: Assign \n   n$4=*&a:int [line 18, column 8]\n  *&a:int=2 [line 18, column 8]\n  *&_a:int=n$4 [line 18, column 3]\n " shape="box"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_16" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_15" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_17" [label="17:  AtomicExpr \n   *&a:int=1 [line 17, column 3]\n " shape="box"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_17" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_16" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_18" [label="18:  BinaryOperatorStmt: Assign \n   n$6=*&a:int [line 16, column 8]\n  *&_a:int=n$6 [line 16, column 3]\n " shape="box"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_18" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_17" ;
+"c11_builtins.cde4bc28f3f67eacb05e50ced6138039_19" [label="19:  AtomicExpr \n   *&a:int=0 [line 15, column 3]\n " shape="box"]
+	
+
+	 "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_19" -> "c11_builtins.cde4bc28f3f67eacb05e50ced6138039_18" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_1" [label="1: Start gnu_builtins\nFormals: \nLocals:  i:int _a:int _i:int b:_Bool \n  " color=yellow style=filled]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_1" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_22" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_2" [label="2: Exit gnu_builtins \n  " color=yellow style=filled]
+	
+
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_3" [label="3: + \n  " ]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_3" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_4" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_4" [label="4:  between_join_and_exit \n  " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_4" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_2" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_5" [label="5: Prune (true branch, atomic compare exchange) \n   PRUNE((n$0 == n$1), true); [line 61, column 7]\n " shape="invhouse"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_5" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_6" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_6" [label="6:  Atomic compare exchange branch \n   *&i:int=n$2 [line 61, column 7]\n  *&b:_Bool=1 [line 61, column 7]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_6" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_3" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_7" [label="7: Prune (false branch, atomic compare exchange) \n   PRUNE(!(n$0 == n$1), false); [line 61, column 7]\n " shape="invhouse"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_7" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_8" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_8" [label="8:  Atomic compare exchange branch \n   *&_i:int=n$0 [line 61, column 7]\n  *&b:_Bool=0 [line 61, column 7]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_8" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_3" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_9" [label="9:  AtomicExpr \n   n$0=*&i:int [line 61, column 7]\n  n$1=*&_i:int [line 61, column 7]\n  n$2=*&_a:int [line 61, column 7]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_9" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_5" ;
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_9" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_7" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_10" [label="10: + \n  " ]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_10" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_9" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_11" [label="11: Prune (true branch, atomic compare exchange) \n   PRUNE((n$3 == n$4), true); [line 59, column 7]\n " shape="invhouse"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_11" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_12" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_12" [label="12:  Atomic compare exchange branch \n   *&i:int=0 [line 59, column 7]\n  *&b:_Bool=1 [line 59, column 7]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_12" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_10" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_13" [label="13: Prune (false branch, atomic compare exchange) \n   PRUNE(!(n$3 == n$4), false); [line 59, column 7]\n " shape="invhouse"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_13" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_14" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_14" [label="14:  Atomic compare exchange branch \n   *&_i:int=n$3 [line 59, column 7]\n  *&b:_Bool=0 [line 59, column 7]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_14" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_10" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_15" [label="15:  AtomicExpr \n   n$3=*&i:int [line 59, column 7]\n  n$4=*&_i:int [line 59, column 7]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_15" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_11" ;
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_15" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_13" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_16" [label="16:  AtomicExpr \n   n$5=*&i:int [line 58, column 3]\n  n$6=*&_i:int [line 58, column 3]\n  *&i:int=n$6 [line 58, column 3]\n  *&_a:int=n$5 [line 58, column 3]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_16" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_15" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_17" [label="17:  BinaryOperatorStmt: Assign \n   n$8=*&i:int [line 57, column 8]\n  *&i:int=1 [line 57, column 8]\n  *&_i:int=n$8 [line 57, column 3]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_17" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_16" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_18" [label="18:  AtomicExpr \n   n$9=*&_i:int [line 56, column 3]\n  *&i:int=n$9 [line 56, column 3]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_18" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_17" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_19" [label="19:  AtomicExpr \n   *&i:int=1 [line 55, column 3]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_19" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_18" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_20" [label="20:  AtomicExpr \n   n$12=*&i:int [line 54, column 3]\n  *&_i:int=n$12 [line 54, column 3]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_20" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_19" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_21" [label="21:  BinaryOperatorStmt: Assign \n   n$14=*&i:int [line 53, column 8]\n  *&_i:int=n$14 [line 53, column 3]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_21" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_20" ;
+"gnu_builtins.c169a1fafd45300f7ea517157b55c968_22" [label="22:  DeclStmt \n   VARIABLE_DECLARED(i:int); [line 52, column 3]\n  *&i:int=0 [line 52, column 3]\n " shape="box"]
+	
+
+	 "gnu_builtins.c169a1fafd45300f7ea517157b55c968_22" -> "gnu_builtins.c169a1fafd45300f7ea517157b55c968_21" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_1" [label="1: Start opencl_builtins\nFormals: \nLocals:  o:void _o:int b:_Bool \n  " color=yellow style=filled]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_1" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_19" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_2" [label="2: Exit opencl_builtins \n  " color=yellow style=filled]
+	
+
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_3" [label="3: + \n  " ]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_3" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_4" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_4" [label="4:  between_join_and_exit \n  " shape="box"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_4" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_2" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_5" [label="5: Prune (true branch, atomic compare exchange) \n   PRUNE((n$0 == n$1), true); [line 40, column 7]\n " shape="invhouse"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_5" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_6" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_6" [label="6:  Atomic compare exchange branch \n   *&o:int=0 [line 40, column 7]\n  *&b:_Bool=1 [line 40, column 7]\n " shape="box"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_6" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_3" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_7" [label="7: Prune (false branch, atomic compare exchange) \n   PRUNE(!(n$0 == n$1), false); [line 40, column 7]\n " shape="invhouse"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_7" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_8" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_8" [label="8:  Atomic compare exchange branch \n   *&_o:int=n$0 [line 40, column 7]\n  *&b:_Bool=0 [line 40, column 7]\n " shape="box"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_8" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_3" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_9" [label="9:  AtomicExpr \n   n$0=*&o:int [line 40, column 7]\n  n$1=*&_o:int [line 40, column 7]\n " shape="box"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_9" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_5" ;
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_9" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_7" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_10" [label="10: + \n  " ]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_10" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_9" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_11" [label="11: Prune (true branch, atomic compare exchange) \n   PRUNE((n$2 == n$3), true); [line 34, column 7]\n " shape="invhouse"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_11" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_12" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_12" [label="12:  Atomic compare exchange branch \n   *&o:int=0 [line 34, column 7]\n  *&b:_Bool=1 [line 34, column 7]\n " shape="box"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_12" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_10" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_13" [label="13: Prune (false branch, atomic compare exchange) \n   PRUNE(!(n$2 == n$3), false); [line 34, column 7]\n " shape="invhouse"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_13" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_14" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_14" [label="14:  Atomic compare exchange branch \n   *&_o:int=n$2 [line 34, column 7]\n  *&b:_Bool=0 [line 34, column 7]\n " shape="box"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_14" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_10" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_15" [label="15:  AtomicExpr \n   n$2=*&o:int [line 34, column 7]\n  n$3=*&_o:int [line 34, column 7]\n " shape="box"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_15" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_11" ;
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_15" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_13" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_16" [label="16:  BinaryOperatorStmt: Assign \n   n$4=*&o:int [line 32, column 8]\n  *&o:int=2 [line 32, column 8]\n  *&_o:int=n$4 [line 32, column 3]\n " shape="box"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_16" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_15" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_17" [label="17:  AtomicExpr \n   *&o:int=1 [line 30, column 3]\n " shape="box"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_17" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_16" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_18" [label="18:  BinaryOperatorStmt: Assign \n   n$6=*&o:int [line 28, column 8]\n  *&_o:int=n$6 [line 28, column 3]\n " shape="box"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_18" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_17" ;
+"opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_19" [label="19:  AtomicExpr \n   *&o:int=0 [line 27, column 3]\n " shape="box"]
+	
+
+	 "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_19" -> "opencl_builtins.9b1efc71247f6a0d7d54fa1b2b0da1ed_18" ;
+}