From a7a332ea5147a2beb045dc6e996d951a3ccc0055 Mon Sep 17 00:00:00 2001 From: Andrzej Kotulski Date: Mon, 26 Oct 2015 06:58:08 -0700 Subject: [PATCH] add different handling for C++ increment/decrement operators Summary: public In C pre-increment/decrement returns rvalue, but in C++ it returns lvalue. Make translation aware of the difference and treat these cases differently. Reviewed By: ddino Differential Revision: D2575136 fb-gh-sync-id: 952c095 --- infer/src/clang/cArithmetic_trans.ml | 12 ++++- .../nestedoperators/assign_with_increment.c | 16 +++++++ .../assign_with_increment.c.dot | 29 ++++++++++++ .../nestedoperators/assign_with_increment.cpp | 1 + .../assign_with_increment.cpp.dot | 29 ++++++++++++ .../cpp/frontend/reference/increment.cpp | 21 +++++++++ .../cpp/frontend/reference/increment.cpp.dot | 44 +++++++++++++++++++ .../tests/frontend/c/NestedOperatorsTest.java | 5 +++ .../frontend/cpp/NestedOperatorsTest.java | 7 +++ infer/tests/frontend/cpp/ReferenceTest.java | 6 +++ 10 files changed, 168 insertions(+), 2 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/frontend/nestedoperators/assign_with_increment.c create mode 100644 infer/tests/codetoanalyze/c/frontend/nestedoperators/assign_with_increment.c.dot create mode 120000 infer/tests/codetoanalyze/c/frontend/nestedoperators/assign_with_increment.cpp create mode 100644 infer/tests/codetoanalyze/c/frontend/nestedoperators/assign_with_increment.cpp.dot create mode 100644 infer/tests/codetoanalyze/cpp/frontend/reference/increment.cpp create mode 100644 infer/tests/codetoanalyze/cpp/frontend/reference/increment.cpp.dot diff --git a/infer/src/clang/cArithmetic_trans.ml b/infer/src/clang/cArithmetic_trans.ml index 32ab28b62..ed31970ce 100644 --- a/infer/src/clang/cArithmetic_trans.ml +++ b/infer/src/clang/cArithmetic_trans.ml @@ -151,7 +151,11 @@ let unary_operation_instruction uoi e typ loc = let id = Ident.create_fresh Ident.knormal in let instr1 = Sil.Letderef (id, e, typ, loc) in let e_plus_1 = Sil.BinOp(Sil.PlusA, Sil.Var id, Sil.Const(Sil.Cint (Sil.Int.one))) in - ([id], e_plus_1, instr1::[Sil.Set (e, typ, e_plus_1, loc)]) + let exp = if General_utils.is_cpp_translation !CFrontend_config.language then + e + else + e_plus_1 in + ([id], exp, instr1::[Sil.Set (e, typ, e_plus_1, loc)]) | `PostDec -> let id = Ident.create_fresh Ident.knormal in let instr1 = Sil.Letderef (id, e, typ, loc) in @@ -161,7 +165,11 @@ let unary_operation_instruction uoi e typ loc = let id = Ident.create_fresh Ident.knormal in let instr1 = Sil.Letderef (id, e, typ, loc) in let e_minus_1 = Sil.BinOp(Sil.MinusA, Sil.Var id, Sil.Const(Sil.Cint (Sil.Int.one))) in - ([id], e_minus_1, instr1::[Sil.Set (e, typ, e_minus_1, loc)]) + let exp = if General_utils.is_cpp_translation !CFrontend_config.language then + e + else + e_minus_1 in + ([id], exp, instr1::[Sil.Set (e, typ, e_minus_1, loc)]) | `Not -> ([], un_exp (Sil.BNot), []) | `Minus -> ([], un_exp (Sil.Neg), []) | `Plus -> ([], e, []) diff --git a/infer/tests/codetoanalyze/c/frontend/nestedoperators/assign_with_increment.c b/infer/tests/codetoanalyze/c/frontend/nestedoperators/assign_with_increment.c new file mode 100644 index 000000000..b3233060f --- /dev/null +++ b/infer/tests/codetoanalyze/c/frontend/nestedoperators/assign_with_increment.c @@ -0,0 +1,16 @@ +/* +* 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 test() { + int a = 3; + int b = ++a; + int c = a++; + int d = --a; + int e = a--; +} diff --git a/infer/tests/codetoanalyze/c/frontend/nestedoperators/assign_with_increment.c.dot b/infer/tests/codetoanalyze/c/frontend/nestedoperators/assign_with_increment.c.dot new file mode 100644 index 000000000..769f402a3 --- /dev/null +++ b/infer/tests/codetoanalyze/c/frontend/nestedoperators/assign_with_increment.c.dot @@ -0,0 +1,29 @@ +digraph iCFG { +7 [label="7: DeclStmt \n *&a:int =3 [line 11]\n " shape="box"] + + + 7 -> 6 ; +6 [label="6: DeclStmt \n n$3=*&a:int [line 12]\n *&a:int =(n$3 + 1) [line 12]\n *&b:int =(n$3 + 1) [line 12]\n REMOVE_TEMPS(n$3); [line 12]\n NULLIFY(&b,false); [line 12]\n " shape="box"] + + + 6 -> 5 ; +5 [label="5: DeclStmt \n n$2=*&a:int [line 13]\n *&a:int =(n$2 + 1) [line 13]\n *&c:int =n$2 [line 13]\n REMOVE_TEMPS(n$2); [line 13]\n NULLIFY(&c,false); [line 13]\n " shape="box"] + + + 5 -> 4 ; +4 [label="4: DeclStmt \n n$1=*&a:int [line 14]\n *&a:int =(n$1 - 1) [line 14]\n *&d:int =(n$1 - 1) [line 14]\n REMOVE_TEMPS(n$1); [line 14]\n NULLIFY(&d,false); [line 14]\n " shape="box"] + + + 4 -> 3 ; +3 [label="3: DeclStmt \n n$0=*&a:int [line 15]\n *&a:int =(n$0 - 1) [line 15]\n *&e:int =n$0 [line 15]\n REMOVE_TEMPS(n$0); [line 15]\n NULLIFY(&a,false); [line 15]\n NULLIFY(&e,false); [line 15]\n APPLY_ABSTRACTION; [line 15]\n " shape="box"] + + + 3 -> 2 ; +2 [label="2: Exit test \n " color=yellow style=filled] + + +1 [label="1: Start test\nFormals: \nLocals: e:int d:int c:int b:int a:int \n DECLARE_LOCALS(&return,&e,&d,&c,&b,&a); [line 10]\n NULLIFY(&a,false); [line 10]\n NULLIFY(&b,false); [line 10]\n NULLIFY(&c,false); [line 10]\n NULLIFY(&d,false); [line 10]\n NULLIFY(&e,false); [line 10]\n " color=yellow style=filled] + + + 1 -> 7 ; +} diff --git a/infer/tests/codetoanalyze/c/frontend/nestedoperators/assign_with_increment.cpp b/infer/tests/codetoanalyze/c/frontend/nestedoperators/assign_with_increment.cpp new file mode 120000 index 000000000..4ae435508 --- /dev/null +++ b/infer/tests/codetoanalyze/c/frontend/nestedoperators/assign_with_increment.cpp @@ -0,0 +1 @@ +assign_with_increment.c \ No newline at end of file diff --git a/infer/tests/codetoanalyze/c/frontend/nestedoperators/assign_with_increment.cpp.dot b/infer/tests/codetoanalyze/c/frontend/nestedoperators/assign_with_increment.cpp.dot new file mode 100644 index 000000000..ead90f928 --- /dev/null +++ b/infer/tests/codetoanalyze/c/frontend/nestedoperators/assign_with_increment.cpp.dot @@ -0,0 +1,29 @@ +digraph iCFG { +7 [label="7: DeclStmt \n *&a:int =3 [line 11]\n " shape="box"] + + + 7 -> 6 ; +6 [label="6: DeclStmt \n n$4=*&a:int [line 12]\n *&a:int =(n$4 + 1) [line 12]\n n$5=*&a:int [line 12]\n *&b:int =n$5 [line 12]\n REMOVE_TEMPS(n$4,n$5); [line 12]\n NULLIFY(&b,false); [line 12]\n " shape="box"] + + + 6 -> 5 ; +5 [label="5: DeclStmt \n n$3=*&a:int [line 13]\n *&a:int =(n$3 + 1) [line 13]\n *&c:int =n$3 [line 13]\n REMOVE_TEMPS(n$3); [line 13]\n NULLIFY(&c,false); [line 13]\n " shape="box"] + + + 5 -> 4 ; +4 [label="4: DeclStmt \n n$1=*&a:int [line 14]\n *&a:int =(n$1 - 1) [line 14]\n n$2=*&a:int [line 14]\n *&d:int =n$2 [line 14]\n REMOVE_TEMPS(n$1,n$2); [line 14]\n NULLIFY(&d,false); [line 14]\n " shape="box"] + + + 4 -> 3 ; +3 [label="3: DeclStmt \n n$0=*&a:int [line 15]\n *&a:int =(n$0 - 1) [line 15]\n *&e:int =n$0 [line 15]\n REMOVE_TEMPS(n$0); [line 15]\n NULLIFY(&a,false); [line 15]\n NULLIFY(&e,false); [line 15]\n APPLY_ABSTRACTION; [line 15]\n " shape="box"] + + + 3 -> 2 ; +2 [label="2: Exit test \n " color=yellow style=filled] + + +1 [label="1: Start test\nFormals: \nLocals: e:int d:int c:int b:int a:int \n DECLARE_LOCALS(&return,&e,&d,&c,&b,&a); [line 10]\n NULLIFY(&a,false); [line 10]\n NULLIFY(&b,false); [line 10]\n NULLIFY(&c,false); [line 10]\n NULLIFY(&d,false); [line 10]\n NULLIFY(&e,false); [line 10]\n " color=yellow style=filled] + + + 1 -> 7 ; +} diff --git a/infer/tests/codetoanalyze/cpp/frontend/reference/increment.cpp b/infer/tests/codetoanalyze/cpp/frontend/reference/increment.cpp new file mode 100644 index 000000000..e62fd674c --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/frontend/reference/increment.cpp @@ -0,0 +1,21 @@ +/* +* 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. +*/ + +void using_value() { + int v = 3; + int &r = ++v; + int &q = --v; +} + +void using_ref() { + int v = 3; + int &vr = v; + int &r = ++vr; + int &q = --vr; +} diff --git a/infer/tests/codetoanalyze/cpp/frontend/reference/increment.cpp.dot b/infer/tests/codetoanalyze/cpp/frontend/reference/increment.cpp.dot new file mode 100644 index 000000000..92f46b5b3 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/frontend/reference/increment.cpp.dot @@ -0,0 +1,44 @@ +digraph iCFG { +11 [label="11: DeclStmt \n *&v:int =3 [line 17]\n " shape="box"] + + + 11 -> 10 ; +10 [label="10: DeclStmt \n *&vr:int &=&v [line 18]\n " shape="box"] + + + 10 -> 9 ; +9 [label="9: DeclStmt \n n$2=*&vr:int & [line 19]\n n$3=*n$2:int [line 19]\n *n$2:int =(n$3 + 1) [line 19]\n *&r:int &=n$2 [line 19]\n REMOVE_TEMPS(n$2,n$3); [line 19]\n NULLIFY(&r,false); [line 19]\n " shape="box"] + + + 9 -> 8 ; +8 [label="8: DeclStmt \n n$0=*&vr:int & [line 20]\n n$1=*n$0:int [line 20]\n *n$0:int =(n$1 - 1) [line 20]\n *&q:int &=n$0 [line 20]\n REMOVE_TEMPS(n$0,n$1); [line 20]\n NULLIFY(&q,false); [line 20]\n NULLIFY(&vr,false); [line 20]\n NULLIFY(&v,false); [line 20]\n APPLY_ABSTRACTION; [line 20]\n " shape="box"] + + + 8 -> 7 ; +7 [label="7: Exit using_ref \n " color=yellow style=filled] + + +6 [label="6: Start using_ref\nFormals: \nLocals: q:int & r:int & vr:int & v:int \n DECLARE_LOCALS(&return,&q,&r,&vr,&v); [line 16]\n NULLIFY(&q,false); [line 16]\n NULLIFY(&r,false); [line 16]\n NULLIFY(&vr,false); [line 16]\n " color=yellow style=filled] + + + 6 -> 11 ; +5 [label="5: DeclStmt \n *&v:int =3 [line 11]\n " shape="box"] + + + 5 -> 4 ; +4 [label="4: DeclStmt \n n$1=*&v:int [line 12]\n *&v:int =(n$1 + 1) [line 12]\n *&r:int &=&v [line 12]\n REMOVE_TEMPS(n$1); [line 12]\n NULLIFY(&r,false); [line 12]\n " shape="box"] + + + 4 -> 3 ; +3 [label="3: DeclStmt \n n$0=*&v:int [line 13]\n *&v:int =(n$0 - 1) [line 13]\n *&q:int &=&v [line 13]\n REMOVE_TEMPS(n$0); [line 13]\n NULLIFY(&q,false); [line 13]\n NULLIFY(&v,false); [line 13]\n APPLY_ABSTRACTION; [line 13]\n " shape="box"] + + + 3 -> 2 ; +2 [label="2: Exit using_value \n " color=yellow style=filled] + + +1 [label="1: Start using_value\nFormals: \nLocals: q:int & r:int & v:int \n DECLARE_LOCALS(&return,&q,&r,&v); [line 10]\n NULLIFY(&q,false); [line 10]\n NULLIFY(&r,false); [line 10]\n " color=yellow style=filled] + + + 1 -> 5 ; +} diff --git a/infer/tests/frontend/c/NestedOperatorsTest.java b/infer/tests/frontend/c/NestedOperatorsTest.java index f2044b470..9765af6ba 100644 --- a/infer/tests/frontend/c/NestedOperatorsTest.java +++ b/infer/tests/frontend/c/NestedOperatorsTest.java @@ -49,4 +49,9 @@ public class NestedOperatorsTest { frontendTest("assign_in_condition.c"); } + @Test + public void whenCaptureRunAssignWithIncrementThenDotFilesAreTheSame() + throws InterruptedException, IOException, InferException { + frontendTest("assign_with_increment.c"); + } } diff --git a/infer/tests/frontend/cpp/NestedOperatorsTest.java b/infer/tests/frontend/cpp/NestedOperatorsTest.java index 71fdb69df..b81d4f386 100644 --- a/infer/tests/frontend/cpp/NestedOperatorsTest.java +++ b/infer/tests/frontend/cpp/NestedOperatorsTest.java @@ -56,4 +56,11 @@ public class NestedOperatorsTest { frontendTest("assign_in_condition.cpp"); } + @Test + public void whenCaptureRunAssignWithIncrementThenDotFilesAreTheSame() + throws InterruptedException, IOException, InferException { + // .dot file differs, but it's semantically equivalent to one produced by + // C compiler + frontendTest("assign_with_increment.cpp"); + } } diff --git a/infer/tests/frontend/cpp/ReferenceTest.java b/infer/tests/frontend/cpp/ReferenceTest.java index c9d4c0cee..48651222b 100644 --- a/infer/tests/frontend/cpp/ReferenceTest.java +++ b/infer/tests/frontend/cpp/ReferenceTest.java @@ -64,6 +64,12 @@ public class ReferenceTest { throws InterruptedException, IOException, InferException { frontendTest("nested_assignment.cpp"); } + + @Test + public void testIncrementDotFilesMatch() + throws InterruptedException, IOException, InferException { + frontendTest("increment.cpp"); + } @Test public void testReferenceTypeE2EDotFilesMatch()