Handle lvalues inside conditional operator right + fix init_expr_trans to fix materializeTempExpr not connecting nodes

Summary:
public
Conditional operator in C++ allows to return lvalues as a result of the operator.
Make infer frontend smart enough to detect when that happens and treat this
case correctly

Reviewed By: ddino

Differential Revision: D2729468

fb-gh-sync-id: f4a110d
master
Andrzej Kotulski 9 years ago committed by facebook-github-bot-7
parent 9c9504ba51
commit 92690551a6

@ -201,16 +201,22 @@ struct
{ empty_res_trans with
exps = [(Sil.Sizeof(expanded_type, Sil.Subtype.exact), Sil.Tint Sil.IULong)] }
let add_reference_if_lvalue typ expr_info =
if expr_info.Clang_ast_t.ei_value_kind = `LValue then
Sil.Tptr (typ, Sil.Pk_reference)
else typ
(** Execute translation and then possibly adjust the type of the result of translation:
In C++, when expression returns reference to type T, it will be lvalue to T, not T&, but
infer needs it to be T& *)
let exec_with_lvalue_as_reference f trans_state stmt =
let expr_info = match Clang_ast_proj.get_expr_tuple stmt with
| Some (_, _, ei) -> ei
| None -> assert false in
let res_trans = f trans_state stmt in
if expr_info.Clang_ast_t.ei_value_kind = `LValue then
let (exp, typ) = extract_exp_from_list res_trans.exps
"[Warning] Need exactly one expression to add reference type\n" in
{ res_trans with exps = [(exp, Sil.Tptr (typ, Sil.Pk_reference))] }
else res_trans
let (exp, typ) = extract_exp_from_list res_trans.exps
"[Warning] Need exactly one expression to add reference type\n" in
{ res_trans with exps = [(exp, add_reference_if_lvalue typ expr_info)] }
(* Execute translation of e forcing to release priority (if it's not free) and then setting it back.*)
(* This is used in conditional operators where we need to force the priority to be free for the *)
@ -928,7 +934,7 @@ struct
Sil.mk_pvar (Mangled.from_string ("SIL_temp_conditional___"^(string_of_int id))) procname in
let sil_loc = CLocation.get_sil_location stmt_info parent_line_number context in
let line_number = CLocation.get_line stmt_info parent_line_number in
let do_branch branch stmt typ prune_nodes join_node pvar =
let do_branch branch stmt var_typ prune_nodes join_node pvar =
let trans_state_pri = PriorityNode.force_claim_priority_node trans_state stmt_info in
let trans_state' = { trans_state_pri with
succ_nodes = [];
@ -937,8 +943,8 @@ struct
let (e', e'_typ) = extract_exp_from_list res_trans_b.exps
"\nWARNING: Missing branch expression for Conditional operator. Need to be fixed\n" in
let set_temp_var = [
Sil.Declare_locals([(pvar, typ)], sil_loc);
Sil.Set (Sil.Lvar pvar, typ, e', sil_loc)
Sil.Declare_locals([(pvar, var_typ)], sil_loc);
Sil.Set (Sil.Lvar pvar, var_typ, e', sil_loc)
] in
let tmp_var_res_trans = { empty_res_trans with instrs = set_temp_var } in
let trans_state'' = { trans_state' with succ_nodes = [join_node] } in
@ -952,6 +958,7 @@ struct
| [cond; exp1; exp2] ->
let typ =
CTypes_decl.type_ptr_to_sil_type context.CContext.tenv expr_info.Clang_ast_t.ei_type_ptr in
let var_typ = add_reference_if_lvalue typ expr_info in
let join_node = create_node (Cfg.Node.Join_node) [] [] sil_loc context in
Cfg.Node.set_succs_exn join_node succ_nodes [];
let pvar = mk_temp_var (Cfg.Node.get_id join_node) in
@ -959,10 +966,13 @@ struct
let trans_state' = { trans_state with continuation = continuation'; parent_line_number = line_number; succ_nodes =[]} in
let res_trans_cond = exec_with_priority_exception trans_state' cond cond_trans in
(* Note: by contruction prune nodes are leafs_nodes_cond *)
do_branch true exp1 typ res_trans_cond.leaf_nodes join_node pvar;
do_branch false exp2 typ res_trans_cond.leaf_nodes join_node pvar;
do_branch true exp1 var_typ res_trans_cond.leaf_nodes join_node pvar;
do_branch false exp2 var_typ res_trans_cond.leaf_nodes join_node pvar;
let id = Ident.create_fresh Ident.knormal in
let instrs =[Sil.Letderef (id, Sil.Lvar pvar, typ, sil_loc); Sil.Nullify (pvar, sil_loc, true)] in
let instrs = [
Sil.Letderef (id, Sil.Lvar pvar, var_typ, sil_loc);
Sil.Nullify (pvar, sil_loc, true)
] in
{ root_nodes = res_trans_cond.root_nodes;
leaf_nodes = [join_node];
ids = [id];
@ -1497,14 +1507,14 @@ struct
let root_nodes = if (IList.length root_nodes) = 0 then [node] else root_nodes in
{
root_nodes = root_nodes;
leaf_nodes = [];
leaf_nodes = [node];
ids = ids;
instrs = instrs;
exps = [(var_exp, ie_typ)];
}
) else {
root_nodes = root_nodes;
leaf_nodes = [];
leaf_nodes = leaf_nodes;
ids = ids;
instrs = instrs;
exps = [(var_exp, ie_typ)]

@ -0,0 +1,63 @@
/*
* Copyright (c) 2015 - 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.
*/
int choose_lvalue(int a) {
int v1 = 0, v2 = 1;
int v3 = a ? v1 : v2;
return v3;
}
int choose_rvalue(int a) {
int v1 = 0;
int v3 = a ? v1 : 1;
return v3;
}
int assign_conditional(int a) {
int v1 = 0, v2 = 0;
(a ? v1 : v2) = 1;
return v1;
}
int div_temp_lvalue(int a, int b) {
const int &r = a ? b : 1;
return 1 / r;
}
int div0_choose_lvalue() {
return 1 / choose_lvalue(1);
}
int div1_choose_lvalue() {
return 1 / choose_lvalue(0);
}
int div0_choose_rvalue() {
return 1 / choose_rvalue(1);
}
int div1_choose_rvalue() {
return 1 / choose_rvalue(0);
}
int div0_assign_conditional() {
return 1 / assign_conditional(0);
}
int div1_assign_conditional() {
return 1 / assign_conditional(1);
}
int div0_temp_lvalue() {
return div_temp_lvalue(1, 0);
}
int div1_temp_lvalue() {
return div_temp_lvalue(0, 1);
}

@ -0,0 +1,254 @@
digraph iCFG {
65 [label="65: Return Stmt \n n$0=_fun_div_temp_lvalue(0:int ,1:int ) [line 62]\n *&return:int =n$0 [line 62]\n REMOVE_TEMPS(n$0); [line 62]\n APPLY_ABSTRACTION; [line 62]\n " shape="box"]
65 -> 64 ;
64 [label="64: Exit div1_temp_lvalue \n " color=yellow style=filled]
63 [label="63: Start div1_temp_lvalue\nFormals: \nLocals: \n DECLARE_LOCALS(&return); [line 61]\n " color=yellow style=filled]
63 -> 65 ;
62 [label="62: Return Stmt \n n$0=_fun_div_temp_lvalue(1:int ,0:int ) [line 58]\n *&return:int =n$0 [line 58]\n REMOVE_TEMPS(n$0); [line 58]\n APPLY_ABSTRACTION; [line 58]\n " shape="box"]
62 -> 61 ;
61 [label="61: Exit div0_temp_lvalue \n " color=yellow style=filled]
60 [label="60: Start div0_temp_lvalue\nFormals: \nLocals: \n DECLARE_LOCALS(&return); [line 57]\n " color=yellow style=filled]
60 -> 62 ;
59 [label="59: Return Stmt \n n$0=_fun_assign_conditional(1:int ) [line 54]\n *&return:int =(1 / n$0) [line 54]\n REMOVE_TEMPS(n$0); [line 54]\n APPLY_ABSTRACTION; [line 54]\n " shape="box"]
59 -> 58 ;
58 [label="58: Exit div1_assign_conditional \n " color=yellow style=filled]
57 [label="57: Start div1_assign_conditional\nFormals: \nLocals: \n DECLARE_LOCALS(&return); [line 53]\n " color=yellow style=filled]
57 -> 59 ;
56 [label="56: Return Stmt \n n$0=_fun_assign_conditional(0:int ) [line 50]\n *&return:int =(1 / n$0) [line 50]\n REMOVE_TEMPS(n$0); [line 50]\n APPLY_ABSTRACTION; [line 50]\n " shape="box"]
56 -> 55 ;
55 [label="55: Exit div0_assign_conditional \n " color=yellow style=filled]
54 [label="54: Start div0_assign_conditional\nFormals: \nLocals: \n DECLARE_LOCALS(&return); [line 49]\n " color=yellow style=filled]
54 -> 56 ;
53 [label="53: Return Stmt \n n$0=_fun_choose_rvalue(0:int ) [line 46]\n *&return:int =(1 / n$0) [line 46]\n REMOVE_TEMPS(n$0); [line 46]\n APPLY_ABSTRACTION; [line 46]\n " shape="box"]
53 -> 52 ;
52 [label="52: Exit div1_choose_rvalue \n " color=yellow style=filled]
51 [label="51: Start div1_choose_rvalue\nFormals: \nLocals: \n DECLARE_LOCALS(&return); [line 45]\n " color=yellow style=filled]
51 -> 53 ;
50 [label="50: Return Stmt \n n$0=_fun_choose_rvalue(1:int ) [line 42]\n *&return:int =(1 / n$0) [line 42]\n REMOVE_TEMPS(n$0); [line 42]\n APPLY_ABSTRACTION; [line 42]\n " shape="box"]
50 -> 49 ;
49 [label="49: Exit div0_choose_rvalue \n " color=yellow style=filled]
48 [label="48: Start div0_choose_rvalue\nFormals: \nLocals: \n DECLARE_LOCALS(&return); [line 41]\n " color=yellow style=filled]
48 -> 50 ;
47 [label="47: Return Stmt \n n$0=_fun_choose_lvalue(0:int ) [line 38]\n *&return:int =(1 / n$0) [line 38]\n REMOVE_TEMPS(n$0); [line 38]\n APPLY_ABSTRACTION; [line 38]\n " shape="box"]
47 -> 46 ;
46 [label="46: Exit div1_choose_lvalue \n " color=yellow style=filled]
45 [label="45: Start div1_choose_lvalue\nFormals: \nLocals: \n DECLARE_LOCALS(&return); [line 37]\n " color=yellow style=filled]
45 -> 47 ;
44 [label="44: Return Stmt \n n$0=_fun_choose_lvalue(1:int ) [line 34]\n *&return:int =(1 / n$0) [line 34]\n REMOVE_TEMPS(n$0); [line 34]\n APPLY_ABSTRACTION; [line 34]\n " shape="box"]
44 -> 43 ;
43 [label="43: Exit div0_choose_lvalue \n " color=yellow style=filled]
42 [label="42: Start div0_choose_lvalue\nFormals: \nLocals: \n DECLARE_LOCALS(&return); [line 33]\n " color=yellow style=filled]
42 -> 44 ;
41 [label="41: DeclStmt \n n$5=*&SIL_temp_conditional___36:int [line 29]\n NULLIFY(&SIL_temp_conditional___36,true); [line 29]\n *&SIL_materialize_temp__n$2:int =n$5 [line 29]\n *&r:int &=&SIL_materialize_temp__n$2 [line 29]\n REMOVE_TEMPS(n$5); [line 29]\n " shape="box"]
41 -> 35 ;
40 [label="40: ConditinalStmt Branch \n NULLIFY(&a,false); [line 29]\n NULLIFY(&b,false); [line 29]\n DECLARE_LOCALS(&SIL_temp_conditional___36); [line 29]\n *&SIL_temp_conditional___36:int =1 [line 29]\n APPLY_ABSTRACTION; [line 29]\n " shape="box"]
40 -> 36 ;
39 [label="39: ConditinalStmt Branch \n NULLIFY(&a,false); [line 29]\n n$4=*&b:int [line 29]\n DECLARE_LOCALS(&SIL_temp_conditional___36); [line 29]\n *&SIL_temp_conditional___36:int =n$4 [line 29]\n REMOVE_TEMPS(n$4); [line 29]\n NULLIFY(&b,false); [line 29]\n APPLY_ABSTRACTION; [line 29]\n " shape="box"]
39 -> 36 ;
38 [label="38: Prune (false branch) \n n$3=*&a:int [line 29]\n PRUNE((n$3 == 0), false); [line 29]\n REMOVE_TEMPS(n$3); [line 29]\n " shape="invhouse"]
38 -> 40 ;
37 [label="37: Prune (true branch) \n n$3=*&a:int [line 29]\n PRUNE((n$3 != 0), true); [line 29]\n REMOVE_TEMPS(n$3); [line 29]\n " shape="invhouse"]
37 -> 39 ;
36 [label="36: + \n " ]
36 -> 41 ;
35 [label="35: Return Stmt \n n$0=*&r:int & [line 30]\n n$1=*n$0:int [line 30]\n *&return:int =(1 / n$1) [line 30]\n REMOVE_TEMPS(n$0,n$1); [line 30]\n NULLIFY(&r,false); [line 30]\n NULLIFY(&SIL_materialize_temp__n$2,false); [line 30]\n APPLY_ABSTRACTION; [line 30]\n " shape="box"]
35 -> 34 ;
34 [label="34: Exit div_temp_lvalue \n " color=yellow style=filled]
33 [label="33: Start div_temp_lvalue\nFormals: a:int b:int \nLocals: r:int & SIL_materialize_temp__n$2:int \n DECLARE_LOCALS(&return,&r,&SIL_materialize_temp__n$2); [line 28]\n NULLIFY(&r,false); [line 28]\n " color=yellow style=filled]
33 -> 37 ;
33 -> 38 ;
32 [label="32: DeclStmt \n *&v1:int =0 [line 23]\n " shape="box"]
32 -> 31 ;
31 [label="31: DeclStmt \n *&v2:int =0 [line 23]\n " shape="box"]
31 -> 26 ;
31 -> 27 ;
30 [label="30: BinaryOperatorStmt: Assign \n n$2=*&SIL_temp_conditional___25:int & [line 24]\n NULLIFY(&SIL_temp_conditional___25,true); [line 24]\n *n$2:int =1 [line 24]\n REMOVE_TEMPS(n$2); [line 24]\n " shape="box"]
30 -> 24 ;
29 [label="29: ConditinalStmt Branch \n NULLIFY(&a,false); [line 24]\n DECLARE_LOCALS(&SIL_temp_conditional___25); [line 24]\n *&SIL_temp_conditional___25:int &=&v2 [line 24]\n APPLY_ABSTRACTION; [line 24]\n " shape="box"]
29 -> 25 ;
28 [label="28: ConditinalStmt Branch \n NULLIFY(&a,false); [line 24]\n DECLARE_LOCALS(&SIL_temp_conditional___25); [line 24]\n *&SIL_temp_conditional___25:int &=&v1 [line 24]\n APPLY_ABSTRACTION; [line 24]\n " shape="box"]
28 -> 25 ;
27 [label="27: Prune (false branch) \n n$1=*&a:int [line 24]\n PRUNE((n$1 == 0), false); [line 24]\n REMOVE_TEMPS(n$1); [line 24]\n " shape="invhouse"]
27 -> 29 ;
26 [label="26: Prune (true branch) \n n$1=*&a:int [line 24]\n PRUNE((n$1 != 0), true); [line 24]\n REMOVE_TEMPS(n$1); [line 24]\n " shape="invhouse"]
26 -> 28 ;
25 [label="25: + \n " ]
25 -> 30 ;
24 [label="24: Return Stmt \n n$0=*&v1:int [line 25]\n *&return:int =n$0 [line 25]\n REMOVE_TEMPS(n$0); [line 25]\n NULLIFY(&v1,false); [line 25]\n NULLIFY(&v2,false); [line 25]\n APPLY_ABSTRACTION; [line 25]\n " shape="box"]
24 -> 23 ;
23 [label="23: Exit assign_conditional \n " color=yellow style=filled]
22 [label="22: Start assign_conditional\nFormals: a:int \nLocals: v2:int v1:int \n DECLARE_LOCALS(&return,&v2,&v1); [line 22]\n " color=yellow style=filled]
22 -> 32 ;
21 [label="21: DeclStmt \n *&v1:int =0 [line 17]\n " shape="box"]
21 -> 16 ;
21 -> 17 ;
20 [label="20: DeclStmt \n n$3=*&SIL_temp_conditional___15:int [line 18]\n NULLIFY(&SIL_temp_conditional___15,true); [line 18]\n *&v3:int =n$3 [line 18]\n REMOVE_TEMPS(n$3); [line 18]\n " shape="box"]
20 -> 14 ;
19 [label="19: ConditinalStmt Branch \n NULLIFY(&a,false); [line 18]\n NULLIFY(&v1,false); [line 18]\n DECLARE_LOCALS(&SIL_temp_conditional___15); [line 18]\n *&SIL_temp_conditional___15:int =1 [line 18]\n APPLY_ABSTRACTION; [line 18]\n " shape="box"]
19 -> 15 ;
18 [label="18: ConditinalStmt Branch \n NULLIFY(&a,false); [line 18]\n n$2=*&v1:int [line 18]\n DECLARE_LOCALS(&SIL_temp_conditional___15); [line 18]\n *&SIL_temp_conditional___15:int =n$2 [line 18]\n REMOVE_TEMPS(n$2); [line 18]\n NULLIFY(&v1,false); [line 18]\n APPLY_ABSTRACTION; [line 18]\n " shape="box"]
18 -> 15 ;
17 [label="17: Prune (false branch) \n n$1=*&a:int [line 18]\n PRUNE((n$1 == 0), false); [line 18]\n REMOVE_TEMPS(n$1); [line 18]\n " shape="invhouse"]
17 -> 19 ;
16 [label="16: Prune (true branch) \n n$1=*&a:int [line 18]\n PRUNE((n$1 != 0), true); [line 18]\n REMOVE_TEMPS(n$1); [line 18]\n " shape="invhouse"]
16 -> 18 ;
15 [label="15: + \n " ]
15 -> 20 ;
14 [label="14: Return Stmt \n n$0=*&v3:int [line 19]\n *&return:int =n$0 [line 19]\n REMOVE_TEMPS(n$0); [line 19]\n NULLIFY(&v3,false); [line 19]\n APPLY_ABSTRACTION; [line 19]\n " shape="box"]
14 -> 13 ;
13 [label="13: Exit choose_rvalue \n " color=yellow style=filled]
12 [label="12: Start choose_rvalue\nFormals: a:int \nLocals: v3:int v1:int \n DECLARE_LOCALS(&return,&v3,&v1); [line 16]\n NULLIFY(&v1,false); [line 16]\n NULLIFY(&v3,false); [line 16]\n " color=yellow style=filled]
12 -> 21 ;
11 [label="11: DeclStmt \n *&v1:int =0 [line 11]\n " shape="box"]
11 -> 10 ;
10 [label="10: DeclStmt \n *&v2:int =1 [line 11]\n " shape="box"]
10 -> 5 ;
10 -> 6 ;
9 [label="9: DeclStmt \n n$2=*&SIL_temp_conditional___4:int & [line 12]\n NULLIFY(&SIL_temp_conditional___4,true); [line 12]\n n$3=*n$2:int [line 12]\n *&v3:int =n$3 [line 12]\n REMOVE_TEMPS(n$2,n$3); [line 12]\n " shape="box"]
9 -> 3 ;
8 [label="8: ConditinalStmt Branch \n NULLIFY(&a,false); [line 12]\n DECLARE_LOCALS(&SIL_temp_conditional___4); [line 12]\n *&SIL_temp_conditional___4:int &=&v2 [line 12]\n APPLY_ABSTRACTION; [line 12]\n " shape="box"]
8 -> 4 ;
7 [label="7: ConditinalStmt Branch \n NULLIFY(&a,false); [line 12]\n DECLARE_LOCALS(&SIL_temp_conditional___4); [line 12]\n *&SIL_temp_conditional___4:int &=&v1 [line 12]\n APPLY_ABSTRACTION; [line 12]\n " shape="box"]
7 -> 4 ;
6 [label="6: Prune (false branch) \n n$1=*&a:int [line 12]\n PRUNE((n$1 == 0), false); [line 12]\n REMOVE_TEMPS(n$1); [line 12]\n " shape="invhouse"]
6 -> 8 ;
5 [label="5: Prune (true branch) \n n$1=*&a:int [line 12]\n PRUNE((n$1 != 0), true); [line 12]\n REMOVE_TEMPS(n$1); [line 12]\n " shape="invhouse"]
5 -> 7 ;
4 [label="4: + \n " ]
4 -> 9 ;
3 [label="3: Return Stmt \n n$0=*&v3:int [line 13]\n *&return:int =n$0 [line 13]\n REMOVE_TEMPS(n$0); [line 13]\n NULLIFY(&v3,false); [line 13]\n NULLIFY(&v1,false); [line 13]\n NULLIFY(&v2,false); [line 13]\n APPLY_ABSTRACTION; [line 13]\n " shape="box"]
3 -> 2 ;
2 [label="2: Exit choose_lvalue \n " color=yellow style=filled]
1 [label="1: Start choose_lvalue\nFormals: a:int \nLocals: v3:int v2:int v1:int \n DECLARE_LOCALS(&return,&v3,&v2,&v1); [line 10]\n NULLIFY(&v3,false); [line 10]\n " color=yellow style=filled]
1 -> 11 ;
}

@ -0,0 +1,66 @@
/*
* Copyright (c) 2015 - 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.cpp;
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 LValueConditionalTest {
public static final String FILE =
"infer/tests/codetoanalyze/cpp/frontend/conditional/lvalue_conditional.cpp";
private static ImmutableList<String> inferCmd;
public static final String DIVIDE_BY_ZERO = "DIVIDE_BY_ZERO";
@ClassRule
public static DebuggableTemporaryFolder folder =
new DebuggableTemporaryFolder();
@BeforeClass
public static void runInfer() throws InterruptedException, IOException {
inferCmd = InferRunner.createCPPInferCommand(folder, FILE);
}
@Test
public void whenInferRunsOnDiv0MethodsErrorIsFound()
throws InterruptedException, IOException, InferException {
InferResults inferResults = InferRunner.runInferCPP(inferCmd);
String[] procedures = {
"div0_choose_lvalue",
"div0_choose_rvalue",
"div0_assign_conditional",
"div0_temp_lvalue",
};
assertThat(
"Results should contain the expected divide by zero",
inferResults,
containsExactly(
DIVIDE_BY_ZERO,
FILE,
procedures
)
);
}
}

@ -0,0 +1,37 @@
/*
* Copyright (c) 2013 - 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 frontend.cpp;
import org.junit.Rule;
import org.junit.Test;
import java.io.IOException;
import utils.DebuggableTemporaryFolder;
import utils.InferException;
import utils.ClangFrontendUtils;
public class ConditionalTest {
String basePath = "infer/tests/codetoanalyze/cpp/frontend/conditional/";
@Rule
public DebuggableTemporaryFolder folder = new DebuggableTemporaryFolder();
void frontendTest(String fileRelative) throws InterruptedException, IOException, InferException {
ClangFrontendUtils.createAndCompareCppDotFiles(folder, basePath + fileRelative);
}
@Test
public void testInlineMethodDotFilesMatch()
throws InterruptedException, IOException, InferException {
frontendTest("lvalue_conditional.cpp");
}
}
Loading…
Cancel
Save