Fix translation of BinaryConditionalOperator

Summary:BinaryConditionalOperator should evaluate condition expression once, but we used to evaluate it twice.
Fix translation to account for it.

Reviewed By: dulmarod

Differential Revision: D3179803

fb-gh-sync-id: a801a7e
fbshipit-source-id: a801a7e
master
Andrzej Kotulski 9 years ago committed by Facebook Github Bot 1
parent 8a1288860b
commit 66d3d492f8

@ -1175,6 +1175,32 @@ struct
} }
| _ -> assert false) | _ -> assert false)
and binaryConditionalOperator_trans trans_state stmt_info stmt_list expr_info =
match stmt_list with
| [stmt1; ostmt1; ostmt2; stmt2]
when contains_opaque_value_expr ostmt1 && contains_opaque_value_expr ostmt2 ->
let sil_loc = CLocation.get_sil_location stmt_info trans_state.context in
let trans_state_pri = PriorityNode.force_claim_priority_node trans_state stmt_info in
let trans_state_cond = { trans_state_pri with
continuation = mk_cond_continuation trans_state_pri.continuation
} in
(* evaluate stmt1 once. Then, use it as replacement for OpaqueValueExpr*)
(* when translating ostmt1 and ostmt2 *)
let init_res_trans = instruction trans_state_cond stmt1 in
let opaque_exp = extract_exp_from_list init_res_trans.exps "" in
let trans_state' = { trans_state_pri with opaque_exp = Some opaque_exp } in
let op_res_trans = conditionalOperator_trans trans_state' stmt_info
[ostmt1; ostmt2; stmt2] expr_info in
let trans_state'' = { trans_state_cond with succ_nodes = op_res_trans.root_nodes } in
let init_res_trans' = PriorityNode.compute_results_to_parent trans_state'' sil_loc
"BinaryConditinalStmt Init" stmt_info [init_res_trans] in
let root_nodes = init_res_trans'.root_nodes in
let root_nodes' = if root_nodes <> [] then root_nodes else op_res_trans.root_nodes in
let ids = op_res_trans.ids @ init_res_trans'.ids in
{ op_res_trans with root_nodes = root_nodes'; ids = ids }
| _ -> Printing.log_stats "BinaryConditionalOperator not translated@.";
assert false
(* Translate a condition for if/loops statement. It shorts-circuit and/or. *) (* Translate a condition for if/loops statement. It shorts-circuit and/or. *)
(* The invariant is that the translation of a condition always contains (at least) *) (* The invariant is that the translation of a condition always contains (at least) *)
(* the prune nodes. Moreover these are always the leaf nodes of the translation. *) (* the prune nodes. Moreover these are always the leaf nodes of the translation. *)
@ -1772,9 +1798,12 @@ struct
and opaqueValueExpr_trans trans_state opaque_value_expr_info = and opaqueValueExpr_trans trans_state opaque_value_expr_info =
Printing.log_out " priority node free = '%s'\n@." Printing.log_out " priority node free = '%s'\n@."
(string_of_bool (PriorityNode.is_priority_free trans_state)); (string_of_bool (PriorityNode.is_priority_free trans_state));
match opaque_value_expr_info.Clang_ast_t.ovei_source_expr with match trans_state.opaque_exp with
| Some exp -> { empty_res_trans with exps = [exp] }
| _ ->
(match opaque_value_expr_info.Clang_ast_t.ovei_source_expr with
| Some stmt -> instruction trans_state stmt | Some stmt -> instruction trans_state stmt
| _ -> assert false | _ -> assert false)
(* NOTE: This translation has several hypothesis. Need to be verified when we have more*) (* NOTE: This translation has several hypothesis. Need to be verified when we have more*)
(* experience with this construct. Assert false will help to see if we encounter programs*) (* experience with this construct. Assert false will help to see if we encounter programs*)
@ -2531,14 +2560,7 @@ struct
stringLiteral_trans trans_state expr_info "" stringLiteral_trans trans_state expr_info ""
| BinaryConditionalOperator (stmt_info, stmts, expr_info) -> | BinaryConditionalOperator (stmt_info, stmts, expr_info) ->
(match stmts with binaryConditionalOperator_trans trans_state stmt_info stmts expr_info
| [stmt1; ostmt1; ostmt2; stmt2]
when contains_opaque_value_expr ostmt1 && contains_opaque_value_expr ostmt2 ->
conditionalOperator_trans trans_state stmt_info [stmt1; stmt1; stmt2] expr_info
| _ -> Printing.log_stats
"BinaryConditionalOperator not translated %s @."
(Ast_utils.string_of_stmt instr);
assert false)
| CXXNewExpr (stmt_info, _, expr_info, cxx_new_expr_info) -> | CXXNewExpr (stmt_info, _, expr_info, cxx_new_expr_info) ->
cxxNewExpr_trans trans_state stmt_info expr_info cxx_new_expr_info cxxNewExpr_trans trans_state stmt_info expr_info cxx_new_expr_info
| CXXDeleteExpr (stmt_info, stmt_list, _, delete_expr_info) -> | CXXDeleteExpr (stmt_info, stmt_list, _, delete_expr_info) ->
@ -2663,6 +2685,7 @@ struct
continuation = None; continuation = None;
priority = Free; priority = Free;
var_exp_typ = None; var_exp_typ = None;
opaque_exp = None;
} in } in
let res_trans_stmt = instruction trans_state stmt in let res_trans_stmt = instruction trans_state stmt in
fst (CTrans_utils.extract_exp_from_list res_trans_stmt.exps warning) fst (CTrans_utils.extract_exp_from_list res_trans_stmt.exps warning)
@ -2674,6 +2697,7 @@ struct
continuation = None; continuation = None;
priority = Free; priority = Free;
var_exp_typ = None; var_exp_typ = None;
opaque_exp = None;
} in } in
let instrs = extra_instrs @ [`ClangStmt body] in let instrs = extra_instrs @ [`ClangStmt body] in
let instrs_trans = IList.map get_custom_stmt_trans instrs in let instrs_trans = IList.map get_custom_stmt_trans instrs in

@ -131,6 +131,7 @@ type trans_state = {
continuation: continuation option; (* current continuation *) continuation: continuation option; (* current continuation *)
priority: priority_node; priority: priority_node;
var_exp_typ: (Sil.exp * Sil.typ) option; var_exp_typ: (Sil.exp * Sil.typ) option;
opaque_exp: (Sil.exp * Sil.typ) option;
} }
(* A translation result. It is returned by the translation function. *) (* A translation result. It is returned by the translation function. *)

@ -27,6 +27,7 @@ type trans_state = {
continuation: continuation option; continuation: continuation option;
priority: priority_node; priority: priority_node;
var_exp_typ: (Sil.exp * Sil.typ) option; var_exp_typ: (Sil.exp * Sil.typ) option;
opaque_exp: (Sil.exp * Sil.typ) option;
} }
type trans_result = { type trans_result = {

@ -31,3 +31,5 @@ int test6(int* p) {
int z = 1 ? *p : 0; int z = 1 ? *p : 0;
return z; return z;
} }
int test7(int b) { return test2(2 + test2(2)) ?: 2; }

@ -1,128 +1,177 @@
digraph iCFG { digraph iCFG {
54 [label="54: DeclStmt \n n$3=*&SIL_temp_conditional___49:int [line 31]\n NULLIFY(&SIL_temp_conditional___49,true); [line 31]\n *&z:int =n$3 [line 31]\n REMOVE_TEMPS(n$3); [line 31]\n " shape="box"] 66 [label="66: Return Stmt \n n$2=*&SIL_temp_conditional___60:int [line 35]\n NULLIFY(&SIL_temp_conditional___60,true); [line 35]\n *&return:int =n$2 [line 35]\n REMOVE_TEMPS(n$2,n$0,n$1); [line 35]\n APPLY_ABSTRACTION; [line 35]\n " shape="box"]
54 -> 48 ; 66 -> 59 ;
53 [label="53: ConditinalStmt Branch \n NULLIFY(&p,false); [line 31]\n DECLARE_LOCALS(&SIL_temp_conditional___49); [line 31]\n *&SIL_temp_conditional___49:int =0 [line 31]\n APPLY_ABSTRACTION; [line 31]\n " shape="box"] 65 [label="65: BinaryConditinalStmt Init \n n$0=_fun_test2(2:int ) [line 35]\n n$1=_fun_test2((2 + n$0):int ) [line 35]\n " shape="box"]
53 -> 49 ; 65 -> 61 ;
52 [label="52: ConditinalStmt Branch \n n$1=*&p:int * [line 31]\n n$2=*n$1:int [line 31]\n DECLARE_LOCALS(&SIL_temp_conditional___49); [line 31]\n *&SIL_temp_conditional___49:int =n$2 [line 31]\n REMOVE_TEMPS(n$1,n$2); [line 31]\n NULLIFY(&p,false); [line 31]\n APPLY_ABSTRACTION; [line 31]\n " shape="box"] 65 -> 62 ;
64 [label="64: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___60); [line 35]\n *&SIL_temp_conditional___60:int =2 [line 35]\n APPLY_ABSTRACTION; [line 35]\n " shape="box"]
52 -> 49 ; 64 -> 60 ;
51 [label="51: Prune (false branch) \n PRUNE((1 == 0), false); [line 31]\n " shape="invhouse"] 63 [label="63: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___60); [line 35]\n *&SIL_temp_conditional___60:int =n$1 [line 35]\n APPLY_ABSTRACTION; [line 35]\n " shape="box"]
51 -> 53 ; 63 -> 60 ;
50 [label="50: Prune (true branch) \n PRUNE((1 != 0), true); [line 31]\n " shape="invhouse"] 62 [label="62: Prune (false branch) \n PRUNE((n$1 == 0), false); [line 35]\n " shape="invhouse"]
50 -> 52 ; 62 -> 64 ;
49 [label="49: + \n " ] 61 [label="61: Prune (true branch) \n PRUNE((n$1 != 0), true); [line 35]\n " shape="invhouse"]
61 -> 63 ;
60 [label="60: + \n " ]
60 -> 66 ;
59 [label="59: Exit test7 \n " color=yellow style=filled]
58 [label="58: Start test7\nFormals: b:int \nLocals: \n DECLARE_LOCALS(&return); [line 35]\n NULLIFY(&b,false); [line 35]\n " color=yellow style=filled]
58 -> 65 ;
57 [label="57: DeclStmt \n n$3=*&SIL_temp_conditional___52:int [line 31]\n NULLIFY(&SIL_temp_conditional___52,true); [line 31]\n *&z:int =n$3 [line 31]\n REMOVE_TEMPS(n$3); [line 31]\n " shape="box"]
57 -> 51 ;
56 [label="56: ConditinalStmt Branch \n NULLIFY(&p,false); [line 31]\n DECLARE_LOCALS(&SIL_temp_conditional___52); [line 31]\n *&SIL_temp_conditional___52:int =0 [line 31]\n APPLY_ABSTRACTION; [line 31]\n " shape="box"]
56 -> 52 ;
55 [label="55: ConditinalStmt Branch \n n$1=*&p:int * [line 31]\n n$2=*n$1:int [line 31]\n DECLARE_LOCALS(&SIL_temp_conditional___52); [line 31]\n *&SIL_temp_conditional___52:int =n$2 [line 31]\n REMOVE_TEMPS(n$1,n$2); [line 31]\n NULLIFY(&p,false); [line 31]\n APPLY_ABSTRACTION; [line 31]\n " shape="box"]
55 -> 52 ;
54 [label="54: Prune (false branch) \n PRUNE((1 == 0), false); [line 31]\n " shape="invhouse"]
54 -> 56 ;
53 [label="53: Prune (true branch) \n PRUNE((1 != 0), true); [line 31]\n " shape="invhouse"]
53 -> 55 ;
52 [label="52: + \n " ]
52 -> 57 ;
51 [label="51: Return Stmt \n n$0=*&z:int [line 32]\n *&return:int =n$0 [line 32]\n REMOVE_TEMPS(n$0); [line 32]\n NULLIFY(&z,false); [line 32]\n APPLY_ABSTRACTION; [line 32]\n " shape="box"]
51 -> 50 ;
50 [label="50: Exit test6 \n " color=yellow style=filled]
49 [label="49: Start test6\nFormals: p:int *\nLocals: z:int \n DECLARE_LOCALS(&return,&z); [line 30]\n NULLIFY(&z,false); [line 30]\n " color=yellow style=filled]
49 -> 53 ;
49 -> 54 ; 49 -> 54 ;
48 [label="48: Return Stmt \n n$0=*&z:int [line 32]\n *&return:int =n$0 [line 32]\n REMOVE_TEMPS(n$0); [line 32]\n NULLIFY(&z,false); [line 32]\n APPLY_ABSTRACTION; [line 32]\n " shape="box"] 48 [label="48: Return Stmt \n n$1=*&SIL_temp_conditional___42:int [line 28]\n NULLIFY(&SIL_temp_conditional___42,true); [line 28]\n *&return:int =n$1 [line 28]\n REMOVE_TEMPS(n$1,n$0); [line 28]\n APPLY_ABSTRACTION; [line 28]\n " shape="box"]
48 -> 47 ; 48 -> 41 ;
47 [label="47: Exit test6 \n " color=yellow style=filled] 47 [label="47: BinaryConditinalStmt Init \n n$0=*&b:int [line 28]\n NULLIFY(&b,false); [line 28]\n " shape="box"]
46 [label="46: Start test6\nFormals: p:int *\nLocals: z:int \n DECLARE_LOCALS(&return,&z); [line 30]\n NULLIFY(&z,false); [line 30]\n " color=yellow style=filled] 47 -> 43 ;
47 -> 44 ;
46 [label="46: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___42); [line 28]\n *&SIL_temp_conditional___42:int =1 [line 28]\n APPLY_ABSTRACTION; [line 28]\n " shape="box"]
46 -> 50 ; 46 -> 42 ;
46 -> 51 ; 45 [label="45: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___42); [line 28]\n *&SIL_temp_conditional___42:int =n$0 [line 28]\n APPLY_ABSTRACTION; [line 28]\n " shape="box"]
45 [label="45: Return Stmt \n n$2=*&SIL_temp_conditional___40:int [line 28]\n NULLIFY(&SIL_temp_conditional___40,true); [line 28]\n *&return:int =n$2 [line 28]\n REMOVE_TEMPS(n$2); [line 28]\n APPLY_ABSTRACTION; [line 28]\n " shape="box"]
45 -> 39 ; 45 -> 42 ;
44 [label="44: ConditinalStmt Branch \n NULLIFY(&b,false); [line 28]\n DECLARE_LOCALS(&SIL_temp_conditional___40); [line 28]\n *&SIL_temp_conditional___40:int =1 [line 28]\n APPLY_ABSTRACTION; [line 28]\n " shape="box"] 44 [label="44: Prune (false branch) \n PRUNE((n$0 == 0), false); [line 28]\n " shape="invhouse"]
44 -> 40 ; 44 -> 46 ;
43 [label="43: ConditinalStmt Branch \n n$1=*&b:int [line 28]\n DECLARE_LOCALS(&SIL_temp_conditional___40); [line 28]\n *&SIL_temp_conditional___40:int =n$1 [line 28]\n REMOVE_TEMPS(n$1); [line 28]\n NULLIFY(&b,false); [line 28]\n APPLY_ABSTRACTION; [line 28]\n " shape="box"] 43 [label="43: Prune (true branch) \n PRUNE((n$0 != 0), true); [line 28]\n " shape="invhouse"]
43 -> 40 ; 43 -> 45 ;
42 [label="42: Prune (false branch) \n n$0=*&b:int [line 28]\n PRUNE((n$0 == 0), false); [line 28]\n REMOVE_TEMPS(n$0); [line 28]\n " shape="invhouse"] 42 [label="42: + \n " ]
42 -> 44 ; 42 -> 48 ;
41 [label="41: Prune (true branch) \n n$0=*&b:int [line 28]\n PRUNE((n$0 != 0), true); [line 28]\n REMOVE_TEMPS(n$0); [line 28]\n " shape="invhouse"] 41 [label="41: Exit test5 \n " color=yellow style=filled]
41 -> 43 ; 40 [label="40: Start test5\nFormals: b:int \nLocals: \n DECLARE_LOCALS(&return); [line 28]\n " color=yellow style=filled]
40 [label="40: + \n " ]
40 -> 45 ; 40 -> 47 ;
39 [label="39: Exit test5 \n " color=yellow style=filled] 39 [label="39: Return Stmt \n n$1=*&SIL_temp_conditional___33:int [line 26]\n NULLIFY(&SIL_temp_conditional___33,true); [line 26]\n n$2=_fun_test2(n$1:int ) [line 26]\n *&return:int =n$2 [line 26]\n REMOVE_TEMPS(n$1,n$0,n$2); [line 26]\n APPLY_ABSTRACTION; [line 26]\n " shape="box"]
38 [label="38: Start test5\nFormals: b:int \nLocals: \n DECLARE_LOCALS(&return); [line 28]\n " color=yellow style=filled] 39 -> 32 ;
38 [label="38: BinaryConditinalStmt Init \n n$0=*&b:int [line 26]\n NULLIFY(&b,false); [line 26]\n " shape="box"]
38 -> 41 ; 38 -> 34 ;
38 -> 42 ; 38 -> 35 ;
37 [label="37: Return Stmt \n n$2=*&SIL_temp_conditional___32:int [line 26]\n NULLIFY(&SIL_temp_conditional___32,true); [line 26]\n n$3=_fun_test2(n$2:int ) [line 26]\n *&return:int =n$3 [line 26]\n REMOVE_TEMPS(n$2,n$3); [line 26]\n APPLY_ABSTRACTION; [line 26]\n " shape="box"] 37 [label="37: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___33); [line 26]\n *&SIL_temp_conditional___33:int =1 [line 26]\n APPLY_ABSTRACTION; [line 26]\n " shape="box"]
37 -> 31 ; 37 -> 33 ;
36 [label="36: ConditinalStmt Branch \n NULLIFY(&b,false); [line 26]\n DECLARE_LOCALS(&SIL_temp_conditional___32); [line 26]\n *&SIL_temp_conditional___32:int =1 [line 26]\n APPLY_ABSTRACTION; [line 26]\n " shape="box"] 36 [label="36: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___33); [line 26]\n *&SIL_temp_conditional___33:int =n$0 [line 26]\n APPLY_ABSTRACTION; [line 26]\n " shape="box"]
36 -> 32 ; 36 -> 33 ;
35 [label="35: ConditinalStmt Branch \n n$1=*&b:int [line 26]\n DECLARE_LOCALS(&SIL_temp_conditional___32); [line 26]\n *&SIL_temp_conditional___32:int =n$1 [line 26]\n REMOVE_TEMPS(n$1); [line 26]\n NULLIFY(&b,false); [line 26]\n APPLY_ABSTRACTION; [line 26]\n " shape="box"] 35 [label="35: Prune (false branch) \n PRUNE((n$0 == 0), false); [line 26]\n " shape="invhouse"]
35 -> 32 ; 35 -> 37 ;
34 [label="34: Prune (false branch) \n n$0=*&b:int [line 26]\n PRUNE((n$0 == 0), false); [line 26]\n REMOVE_TEMPS(n$0); [line 26]\n " shape="invhouse"] 34 [label="34: Prune (true branch) \n PRUNE((n$0 != 0), true); [line 26]\n " shape="invhouse"]
34 -> 36 ; 34 -> 36 ;
33 [label="33: Prune (true branch) \n n$0=*&b:int [line 26]\n PRUNE((n$0 != 0), true); [line 26]\n REMOVE_TEMPS(n$0); [line 26]\n " shape="invhouse"] 33 [label="33: + \n " ]
33 -> 35 ; 33 -> 39 ;
32 [label="32: + \n " ] 32 [label="32: Exit test4 \n " color=yellow style=filled]
32 -> 37 ; 31 [label="31: Start test4\nFormals: b:int \nLocals: \n DECLARE_LOCALS(&return); [line 26]\n " color=yellow style=filled]
31 [label="31: Exit test4 \n " color=yellow style=filled]
30 [label="30: Start test4\nFormals: b:int \nLocals: \n DECLARE_LOCALS(&return); [line 26]\n " color=yellow style=filled] 31 -> 38 ;
30 [label="30: DeclStmt \n n$2=*&SIL_temp_conditional___24:int [line 22]\n NULLIFY(&SIL_temp_conditional___24,true); [line 22]\n *&x:int =n$2 [line 22]\n REMOVE_TEMPS(n$2,n$1); [line 22]\n " shape="box"]
30 -> 33 ; 30 -> 23 ;
30 -> 34 ; 29 [label="29: BinaryConditinalStmt Init \n n$1=*&b:int [line 22]\n NULLIFY(&b,false); [line 22]\n " shape="box"]
29 [label="29: DeclStmt \n n$3=*&SIL_temp_conditional___24:int [line 22]\n NULLIFY(&SIL_temp_conditional___24,true); [line 22]\n *&x:int =n$3 [line 22]\n REMOVE_TEMPS(n$3); [line 22]\n " shape="box"]
29 -> 23 ; 29 -> 25 ;
28 [label="28: ConditinalStmt Branch \n NULLIFY(&b,false); [line 22]\n DECLARE_LOCALS(&SIL_temp_conditional___24); [line 22]\n *&SIL_temp_conditional___24:int =1 [line 22]\n APPLY_ABSTRACTION; [line 22]\n " shape="box"] 29 -> 26 ;
28 [label="28: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___24); [line 22]\n *&SIL_temp_conditional___24:int =1 [line 22]\n APPLY_ABSTRACTION; [line 22]\n " shape="box"]
28 -> 24 ; 28 -> 24 ;
27 [label="27: ConditinalStmt Branch \n n$2=*&b:int [line 22]\n DECLARE_LOCALS(&SIL_temp_conditional___24); [line 22]\n *&SIL_temp_conditional___24:int =n$2 [line 22]\n REMOVE_TEMPS(n$2); [line 22]\n NULLIFY(&b,false); [line 22]\n APPLY_ABSTRACTION; [line 22]\n " shape="box"] 27 [label="27: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___24); [line 22]\n *&SIL_temp_conditional___24:int =n$1 [line 22]\n APPLY_ABSTRACTION; [line 22]\n " shape="box"]
27 -> 24 ; 27 -> 24 ;
26 [label="26: Prune (false branch) \n n$1=*&b:int [line 22]\n PRUNE((n$1 == 0), false); [line 22]\n REMOVE_TEMPS(n$1); [line 22]\n " shape="invhouse"] 26 [label="26: Prune (false branch) \n PRUNE((n$1 == 0), false); [line 22]\n " shape="invhouse"]
26 -> 28 ; 26 -> 28 ;
25 [label="25: Prune (true branch) \n n$1=*&b:int [line 22]\n PRUNE((n$1 != 0), true); [line 22]\n REMOVE_TEMPS(n$1); [line 22]\n " shape="invhouse"] 25 [label="25: Prune (true branch) \n PRUNE((n$1 != 0), true); [line 22]\n " shape="invhouse"]
25 -> 27 ; 25 -> 27 ;
24 [label="24: + \n " ] 24 [label="24: + \n " ]
24 -> 29 ; 24 -> 30 ;
23 [label="23: Return Stmt \n n$0=*&x:int [line 23]\n *&return:int =n$0 [line 23]\n REMOVE_TEMPS(n$0); [line 23]\n NULLIFY(&x,false); [line 23]\n APPLY_ABSTRACTION; [line 23]\n " shape="box"] 23 [label="23: Return Stmt \n n$0=*&x:int [line 23]\n *&return:int =n$0 [line 23]\n REMOVE_TEMPS(n$0); [line 23]\n NULLIFY(&x,false); [line 23]\n APPLY_ABSTRACTION; [line 23]\n " shape="box"]
@ -133,8 +182,7 @@ digraph iCFG {
21 [label="21: Start test3\nFormals: b:int \nLocals: x:int \n DECLARE_LOCALS(&return,&x); [line 21]\n NULLIFY(&x,false); [line 21]\n " color=yellow style=filled] 21 [label="21: Start test3\nFormals: b:int \nLocals: x:int \n DECLARE_LOCALS(&return,&x); [line 21]\n NULLIFY(&x,false); [line 21]\n " color=yellow style=filled]
21 -> 25 ; 21 -> 29 ;
21 -> 26 ;
20 [label="20: DeclStmt \n n$3=*&SIL_temp_conditional___15:int [line 17]\n NULLIFY(&SIL_temp_conditional___15,true); [line 17]\n *&x:int =n$3 [line 17]\n REMOVE_TEMPS(n$3); [line 17]\n " shape="box"] 20 [label="20: DeclStmt \n n$3=*&SIL_temp_conditional___15:int [line 17]\n NULLIFY(&SIL_temp_conditional___15,true); [line 17]\n *&x:int =n$3 [line 17]\n REMOVE_TEMPS(n$3); [line 17]\n " shape="box"]

@ -0,0 +1,28 @@
/*
* Copyright (c) 2016 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
struct X {
operator bool() { return true; }
};
X getX() {
X x;
return x;
}
// more conditional operator tests in C tests
void binaryConditional() {
X a;
X x = getX() ?: a;
}
void conditional() {
X a;
X x = getX() ? getX() : a;
}

@ -0,0 +1,133 @@
digraph iCFG {
34 [label="34: DeclStmt \n _fun_X_X(&a:class X *) [line 26]\n " shape="box"]
34 -> 28 ;
33 [label="33: DeclStmt \n n$6=*&SIL_temp_conditional___27:class X [line 27]\n NULLIFY(&SIL_temp_conditional___27,true); [line 27]\n *&SIL_materialize_temp__n$0:class X =n$6 [line 27]\n _fun_X_X(&x:class X *,&SIL_materialize_temp__n$0:class X &) [line 27]\n REMOVE_TEMPS(n$6); [line 27]\n NULLIFY(&SIL_materialize_temp__n$0,false); [line 27]\n NULLIFY(&SIL_materialize_temp__n$4,false); [line 27]\n NULLIFY(&__temp_return_n$2,false); [line 27]\n NULLIFY(&a,false); [line 27]\n NULLIFY(&x,false); [line 27]\n APPLY_ABSTRACTION; [line 27]\n " shape="box"]
33 -> 26 ;
32 [label="32: ConditinalStmt Branch \n _fun_X_X(&SIL_materialize_temp__n$0:class X *,&a:class X &) [line 27]\n DECLARE_LOCALS(&SIL_temp_conditional___27); [line 27]\n *&SIL_temp_conditional___27:class X =&SIL_materialize_temp__n$0 [line 27]\n APPLY_ABSTRACTION; [line 27]\n " shape="box"]
32 -> 27 ;
31 [label="31: ConditinalStmt Branch \n _fun_getX(&SIL_materialize_temp__n$4:class X *) [line 27]\n _fun_X_X(&SIL_materialize_temp__n$0:class X *,&SIL_materialize_temp__n$4:class X &) [line 27]\n DECLARE_LOCALS(&SIL_temp_conditional___27); [line 27]\n *&SIL_temp_conditional___27:class X =&SIL_materialize_temp__n$0 [line 27]\n APPLY_ABSTRACTION; [line 27]\n " shape="box"]
31 -> 27 ;
30 [label="30: Prune (false branch) \n PRUNE((n$3 == 0), false); [line 27]\n REMOVE_TEMPS(n$3); [line 27]\n " shape="invhouse"]
30 -> 32 ;
29 [label="29: Prune (true branch) \n PRUNE((n$3 != 0), true); [line 27]\n REMOVE_TEMPS(n$3); [line 27]\n " shape="invhouse"]
29 -> 31 ;
28 [label="28: Call _fun_X_operator bool \n _fun_getX(&__temp_return_n$2:class X *) [line 27]\n n$3=_fun_X_operator bool(&__temp_return_n$2:class X &) [line 27]\n " shape="box"]
28 -> 29 ;
28 -> 30 ;
27 [label="27: + \n " ]
27 -> 33 ;
26 [label="26: Exit conditional \n " color=yellow style=filled]
25 [label="25: Start conditional\nFormals: \nLocals: x:class X SIL_materialize_temp__n$0:class X __temp_return_n$2:class X SIL_materialize_temp__n$4:class X a:class X \n DECLARE_LOCALS(&return,&x,&SIL_materialize_temp__n$0,&__temp_return_n$2,&SIL_materialize_temp__n$4,&a); [line 25]\n " color=yellow style=filled]
25 -> 34 ;
24 [label="24: DeclStmt \n _fun_X_X(&a:class X *) [line 21]\n " shape="box"]
24 -> 22 ;
23 [label="23: DeclStmt \n n$4=*&SIL_temp_conditional___16:class X [line 22]\n NULLIFY(&SIL_temp_conditional___16,true); [line 22]\n *&SIL_materialize_temp__n$0:class X =n$4 [line 22]\n _fun_X_X(&x:class X *,&SIL_materialize_temp__n$0:class X &) [line 22]\n REMOVE_TEMPS(n$4); [line 22]\n NULLIFY(&SIL_materialize_temp__n$0,false); [line 22]\n NULLIFY(&SIL_materialize_temp__n$3,false); [line 22]\n NULLIFY(&a,false); [line 22]\n NULLIFY(&x,false); [line 22]\n APPLY_ABSTRACTION; [line 22]\n " shape="box"]
23 -> 15 ;
22 [label="22: BinaryConditinalStmt Init \n _fun_getX(&SIL_materialize_temp__n$0:class X *) [line 22]\n " shape="box"]
22 -> 17 ;
21 [label="21: ConditinalStmt Branch \n _fun_X_X(&SIL_materialize_temp__n$0:class X *,&a:class X &) [line 22]\n DECLARE_LOCALS(&SIL_temp_conditional___16); [line 22]\n *&SIL_temp_conditional___16:class X =&SIL_materialize_temp__n$0 [line 22]\n APPLY_ABSTRACTION; [line 22]\n " shape="box"]
21 -> 16 ;
20 [label="20: ConditinalStmt Branch \n *&SIL_materialize_temp__n$3:class X =&SIL_materialize_temp__n$0 [line 22]\n _fun_X_X(&SIL_materialize_temp__n$0:class X *,&SIL_materialize_temp__n$3:class X &) [line 22]\n DECLARE_LOCALS(&SIL_temp_conditional___16); [line 22]\n *&SIL_temp_conditional___16:class X =&SIL_materialize_temp__n$0 [line 22]\n APPLY_ABSTRACTION; [line 22]\n " shape="box"]
20 -> 16 ;
19 [label="19: Prune (false branch) \n PRUNE((n$2 == 0), false); [line 22]\n REMOVE_TEMPS(n$2); [line 22]\n " shape="invhouse"]
19 -> 21 ;
18 [label="18: Prune (true branch) \n PRUNE((n$2 != 0), true); [line 22]\n REMOVE_TEMPS(n$2); [line 22]\n " shape="invhouse"]
18 -> 20 ;
17 [label="17: Call _fun_X_operator bool \n n$2=_fun_X_operator bool(&SIL_materialize_temp__n$0:class X &) [line 22]\n " shape="box"]
17 -> 18 ;
17 -> 19 ;
16 [label="16: + \n " ]
16 -> 23 ;
15 [label="15: Exit binaryConditional \n " color=yellow style=filled]
14 [label="14: Start binaryConditional\nFormals: \nLocals: x:class X SIL_materialize_temp__n$0:class X SIL_materialize_temp__n$3:class X a:class X \n DECLARE_LOCALS(&return,&x,&SIL_materialize_temp__n$0,&SIL_materialize_temp__n$3,&a); [line 20]\n " color=yellow style=filled]
14 -> 24 ;
13 [label="13: DeclStmt \n _fun_X_X(&x:class X *) [line 15]\n " shape="box"]
13 -> 12 ;
12 [label="12: Return Stmt \n n$0=*&__return_param:class X * [line 16]\n _fun_X_X(n$0:class X *,&x:class X &) [line 16]\n REMOVE_TEMPS(n$0); [line 16]\n NULLIFY(&__return_param,false); [line 16]\n NULLIFY(&x,false); [line 16]\n APPLY_ABSTRACTION; [line 16]\n " shape="box"]
12 -> 11 ;
11 [label="11: Exit getX \n " color=yellow style=filled]
10 [label="10: Start getX\nFormals: __return_param:class X *\nLocals: x:class X \n DECLARE_LOCALS(&return,&x); [line 14]\n " color=yellow style=filled]
10 -> 13 ;
9 [label="9: Exit X_X \n " color=yellow style=filled]
8 [label="8: Start X_X\nFormals: this:class X * __param_0:class X &\nLocals: \n DECLARE_LOCALS(&return); [line 10]\n NULLIFY(&__param_0,false); [line 10]\n NULLIFY(&this,false); [line 10]\n " color=yellow style=filled]
8 -> 9 ;
7 [label="7: Exit X_X \n " color=yellow style=filled]
6 [label="6: Start X_X\nFormals: this:class X * __param_0:class X &\nLocals: \n DECLARE_LOCALS(&return); [line 10]\n NULLIFY(&__param_0,false); [line 10]\n NULLIFY(&this,false); [line 10]\n " color=yellow style=filled]
6 -> 7 ;
5 [label="5: Exit X_X \n " color=yellow style=filled]
4 [label="4: Start X_X\nFormals: this:class X *\nLocals: \n DECLARE_LOCALS(&return); [line 10]\n NULLIFY(&this,false); [line 10]\n " color=yellow style=filled]
4 -> 5 ;
3 [label="3: Return Stmt \n *&return:_Bool =1 [line 11]\n APPLY_ABSTRACTION; [line 11]\n " shape="box"]
3 -> 2 ;
2 [label="2: Exit X_operator bool \n " color=yellow style=filled]
1 [label="1: Start X_operator bool\nFormals: this:class X *\nLocals: \n DECLARE_LOCALS(&return); [line 11]\n NULLIFY(&this,false); [line 11]\n " color=yellow style=filled]
1 -> 3 ;
}

@ -0,0 +1,42 @@
/*
* Copyright (c) 2016 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
#import <Foundation/Foundation.h>
@interface A : NSObject {
int x;
}
- (NSString*)name;
@end
@implementation A
- (NSString*)name {
return @"1";
}
void binaryConditionalNoNPE(A* transfer) {
NSString* val = transfer.name ?: @"0";
NSMutableDictionary* extraBlock =
[[NSMutableDictionary alloc] initWithDictionary:@{
@"key" : val
}];
}
void conditionalNPE(A* transfer) {
NSString* val = transfer.name ? transfer.name : @"0";
NSMutableDictionary* extraBlock =
[[NSMutableDictionary alloc] initWithDictionary:@{
@"key" : val
}];
}
@end

@ -0,0 +1,64 @@
/*
* Copyright (c) 2016 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
package endtoend.objc;
import static org.hamcrest.MatcherAssert.assertThat;
import static utils.matchers.ResultContainsExactly.containsExactly;
import com.google.common.collect.ImmutableList;
import org.junit.BeforeClass;
import org.junit.ClassRule;
import org.junit.Test;
import java.io.IOException;
import utils.DebuggableTemporaryFolder;
import utils.InferException;
import utils.InferResults;
import utils.InferRunner;
public class NPEConditionalTest {
public static final String NPE_CONDITIONAL =
"infer/tests/codetoanalyze/objc/errors/npe/npe_conditional.m";
private static ImmutableList<String> inferCmd;
public static final String NULL_DEREFERENCE = "NULL_DEREFERENCE";
@ClassRule
public static DebuggableTemporaryFolder folderNPD = new DebuggableTemporaryFolder();
@BeforeClass
public static void runInfer() throws InterruptedException, IOException {
inferCmd = InferRunner.createObjCInferCommandWithMLBuckets(
folderNPD,
NPE_CONDITIONAL,
"cf",
true);
}
@Test
public void whenInferRunsOnTestThenNoNPENotFound()
throws InterruptedException, IOException, InferException {
InferResults inferResults = InferRunner.runInferObjC(inferCmd);
String[] expectedNPEProcedures = {
"conditionalNPE"
};
assertThat(
"Only NPE should be found", inferResults,
containsExactly(
NULL_DEREFERENCE,
NPE_CONDITIONAL,
expectedNPEProcedures));
}
}

@ -34,4 +34,10 @@ public class ConditionalTest {
throws InterruptedException, IOException, InferException { throws InterruptedException, IOException, InferException {
frontendTest("lvalue_conditional.cpp"); frontendTest("lvalue_conditional.cpp");
} }
@Test
public void testBinaryConditionalDotFilesMatch()
throws InterruptedException, IOException, InferException {
frontendTest("binary_conditional.cpp");
}
} }

Loading…
Cancel
Save