diff --git a/facebook-clang-plugins/libtooling/ASTExporter.h b/facebook-clang-plugins/libtooling/ASTExporter.h index 40a423bbb..715b4aad6 100644 --- a/facebook-clang-plugins/libtooling/ASTExporter.h +++ b/facebook-clang-plugins/libtooling/ASTExporter.h @@ -404,6 +404,7 @@ class ASTExporter : public ConstDeclVisitor>, 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::VisitCompoundAssignOperator( dumpQualType(Node->getComputationResultType()); } +template +int ASTExporter::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 } +//@atd type atomic_expr_kind = [ +#define ATOMIC_BUILTIN(ID, TYPE, ATTRS) //@atd | AO@@ID +#include +//@atd ] +template +void ASTExporter::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 + } +} + template int ASTExporter::BlockExprTupleSize() { return ExprTupleSize() + DeclTupleSize(); diff --git a/infer/src/IR/BuiltinDecl.ml b/infer/src/IR/BuiltinDecl.ml index ee860f355..a1ca5fbea 100644 --- a/infer/src/IR/BuiltinDecl.ml +++ b/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" diff --git a/infer/src/IR/BuiltinDecl.mli b/infer/src/IR/BuiltinDecl.mli index 3b902e868..2511da9c2 100644 --- a/infer/src/IR/BuiltinDecl.mli +++ b/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 diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index 34983457c..e2d67482b 100644 --- a/infer/src/IR/Procdesc.ml +++ b/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 -> diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index 50c25555a..79c225dd0 100644 --- a/infer/src/IR/Procdesc.mli +++ b/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 diff --git a/infer/src/IR/Sil.ml b/infer/src/IR/Sil.ml index c8a51846c..4a3f556f5 100644 --- a/infer/src/IR/Sil.ml +++ b/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 -> diff --git a/infer/src/IR/Sil.mli b/infer/src/IR/Sil.mli index fffc18d64..7c06e33ec 100644 --- a/infer/src/IR/Sil.mli +++ b/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 diff --git a/infer/src/biabduction/Paths.ml b/infer/src/biabduction/Paths.ml index 7a86a2160..19f08bd4e 100644 --- a/infer/src/biabduction/Paths.ml +++ b/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) -> diff --git a/infer/src/clang/cArithmetic_trans.ml b/infer/src/clang/cArithmetic_trans.ml index 4a98df832..5c103e6ad 100644 --- a/infer/src/clang/cArithmetic_trans.ml +++ b/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 -> diff --git a/infer/src/clang/cArithmetic_trans.mli b/infer/src/clang/cArithmetic_trans.mli index 68784487c..2019c8343 100644 --- a/infer/src/clang/cArithmetic_trans.mli +++ b/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 diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index f25700379..a990d34dc 100644 --- a/infer/src/clang/cTrans.ml +++ b/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 _ diff --git a/infer/tests/codetoanalyze/c/frontend/atomic_expr/arithmetic.c b/infer/tests/codetoanalyze/c/frontend/atomic_expr/arithmetic.c new file mode 100644 index 000000000..fd1c42e6b --- /dev/null +++ b/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 + +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); +} diff --git a/infer/tests/codetoanalyze/c/frontend/atomic_expr/arithmetic.c.dot b/infer/tests/codetoanalyze/c/frontend/atomic_expr/arithmetic.c.dot new file mode 100644 index 000000000..fd5e520a1 --- /dev/null +++ b/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" ; +} diff --git a/infer/tests/codetoanalyze/c/frontend/atomic_expr/atomic_with_others.c b/infer/tests/codetoanalyze/c/frontend/atomic_expr/atomic_with_others.c new file mode 100644 index 000000000..eef6b9285 --- /dev/null +++ b/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 +#include + +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)); +} diff --git a/infer/tests/codetoanalyze/c/frontend/atomic_expr/atomic_with_others.c.dot b/infer/tests/codetoanalyze/c/frontend/atomic_expr/atomic_with_others.c.dot new file mode 100644 index 000000000..5e462e268 --- /dev/null +++ b/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" ; +} diff --git a/infer/tests/codetoanalyze/c/frontend/atomic_expr/load_store_exchange.c b/infer/tests/codetoanalyze/c/frontend/atomic_expr/load_store_exchange.c new file mode 100644 index 000000000..05ec9bab7 --- /dev/null +++ b/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 +#include + +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); +} diff --git a/infer/tests/codetoanalyze/c/frontend/atomic_expr/load_store_exchange.c.dot b/infer/tests/codetoanalyze/c/frontend/atomic_expr/load_store_exchange.c.dot new file mode 100644 index 000000000..4b48e72e8 --- /dev/null +++ b/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" ; +}