pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

diverge on `throw`

Browse Source 
Summary:
Previously, we would translate `throw` with `return`. However, `throw` in
ObjC/C++ is often used to mean "abort". We now translate `throw` the same as
`exit` to prune these paths.

Reviewed By: akotulski

Differential Revision: D3594156

fbshipit-source-id: 81083bb
master
Jules Villard 9 years ago committed by Facebook Github Bot 3
parent fb7aed07c6
commit 10f10a90c6
10 changed files with 147 additions and 62 deletions
Show Stats Download Patch File Download Diff File

3
infer/src/backend/modelBuiltins.ml
Unescape View File

@ -1094,6 +1094,9 @@ let __set_unlocked_attribute = Builtin.register
let __delete_locked_attribute = Builtin.register
(* delete the locked attribute, when it exists *)
"__delete_locked_attribute" execute___delete_locked_attribute
let objc_cpp_throw = Builtin.register
(* model throwing exception in objc/c++ as divergence *)
"__infer_objc_cpp_throw" execute_exit
let _ = Builtin.register
"__throw" execute_skip
let __unwrap_exception = Builtin.register

1
infer/src/backend/modelBuiltins.mli
Unescape View File

@ -44,3 +44,4 @@ val __objc_cast : Procname.t
val __objc_dictionary_literal : Procname.t
val __cxx_typeid : Procname.t
val malloc_no_fail : Procname.t
val objc_cpp_throw : Procname.t

21
infer/src/clang/cTrans.ml
Unescape View File

@ -2197,24 +2197,29 @@ struct
| Some exp -> instruction trans_state exp
| None -> assert false
and gccAsmStmt_trans trans_state stmt_info stmts =
and call_function_with_args instr_name pname trans_state stmt_info stmts =
let sil_loc = CLocation.get_sil_location stmt_info trans_state.context in
let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in
let trans_state_param = { trans_state_pri with succ_nodes = [] } in
let res_trans_subexpr_list =
IList.map (exec_with_glvalue_as_reference instruction trans_state_param) stmts in
let params = collect_exprs res_trans_subexpr_list in
let fun_name = Procname.from_string_c_fun CFrontend_config.infer_skip_gcc_asm_stmt in
let sil_fun = Sil.Const (Const.Cfun fun_name) in
let sil_fun = Sil.Const (Const.Cfun pname) in
let call_instr = Sil.Call ([], sil_fun, params, sil_loc, CallFlags.default) in
let res_trans_call = { empty_res_trans with
instrs = [call_instr];
exps = []; } in
let all_res_trans = res_trans_subexpr_list @ [res_trans_call] in
let res_trans_to_parent = PriorityNode.compute_results_to_parent trans_state_pri sil_loc
"GCCAsmStmt" stmt_info all_res_trans in
instr_name stmt_info all_res_trans in
{ res_trans_to_parent with exps = res_trans_call.exps }
and gccAsmStmt_trans trans_state =
let pname = Procname.from_string_c_fun CFrontend_config.infer_skip_gcc_asm_stmt in
call_function_with_args "GCCAsmStmt" pname trans_state
and objc_cxx_throw_trans trans_state =
call_function_with_args "ObjCCPPThrow" ModelBuiltins.objc_cpp_throw trans_state
and cxxPseudoDestructorExpr_trans () =
let fun_name = Procname.from_string_c_fun CFrontend_config.infer_skip_fun in
{ empty_res_trans with exps = [(Sil.Const (Const.Cfun fun_name), Typ.Tvoid)] }
@ -2519,13 +2524,9 @@ struct
(Ast_utils.string_of_stmt instr);
compoundStmt_trans trans_state stmts)
| ObjCAtThrowStmt (stmt_info, stmts) ->
returnStmt_trans trans_state stmt_info stmts
| ObjCAtThrowStmt (stmt_info, stmts)
| CXXThrowExpr (stmt_info, stmts, _) ->
(Printing.log_stats
"\n!!!!WARNING: found statement %s. \nTranslation need to be improved.... \n"
(Ast_utils.string_of_stmt instr);
returnStmt_trans trans_state stmt_info stmts)
objc_cxx_throw_trans trans_state stmt_info stmts
| ObjCAtFinallyStmt (_, stmts) ->
compoundStmt_trans trans_state stmts

1
infer/tests/build_systems/build_integration_tests.py
Unescape View File

@ -125,7 +125,6 @@ def run_analysis(clean_cmds, build_cmds, env=None):
extra_args +
['--'] +
build_cmd['compile'])
print(str(infer_cmd))
# Only record the output of the last build command. We record
# all of them but each command overwrites the output of the
# previous one.

26
infer/tests/codetoanalyze/cpp/errors/npe/throw_as_assert.cpp
Unescape View File

@ -0,0 +1,26 @@
/*
* 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.
*/
#include <stdlib.h>
#include <cstddef>
struct foo {
void check_condition(bool cond) {
if (!cond) {
throw 1;
}
}
void test_that_throw_prunes_condition() {
int* p = (int*)malloc(sizeof(int));
check_condition(p != nullptr);
*p = 42;
free(p);
}
};

82
infer/tests/codetoanalyze/cpp/errors/subtyping/cast_with_enforce.cpp.dot
Unescape View File

@ -1,89 +1,81 @@
/* @generated */
digraph iCFG {
40 [label="40: DeclStmt \n _fun_Base_Base(&base:class Base *) [line 52]\n " shape="box"]
40 -> 39 ;
39 [label="39: DeclStmt \n n$2=_fun___cast(&base:class Base *,sizeof(class Derived ( sub )(cast)):void ) [line 53]\n *&derived:class Derived *=n$2 [line 53]\n " shape="box"]
39 -> 38 ;
38 [label="38: Return Stmt \n n$0=*&derived:class Derived * [line 54]\n n$1=*n$0.a:int [line 54]\n *&return:int =n$1 [line 54]\n " shape="box"]
38 [label="38: DeclStmt \n _fun_Base_Base(&base:class Base *) [line 52]\n " shape="box"]
38 -> 37 ;
37 [label="37: Exit cast_with_npe \n " color=yellow style=filled]
37 [label="37: DeclStmt \n n$2=_fun___cast(&base:class Base *,sizeof(class Derived ( sub )(cast)):void ) [line 53]\n *&derived:class Derived *=n$2 [line 53]\n " shape="box"]
36 [label="36: Start cast_with_npe\nFormals: \nLocals: derived:class Derived * base:class Base \n DECLARE_LOCALS(&return,&derived,&base); [line 51]\n " color=yellow style=filled]
37 -> 36 ;
36 [label="36: Return Stmt \n n$0=*&derived:class Derived * [line 54]\n n$1=*n$0.a:int [line 54]\n *&return:int =n$1 [line 54]\n " shape="box"]
36 -> 40 ;
35 [label="35: DeclStmt \n _fun_Base_Base(&base:class Base *) [line 44]\n " shape="box"]
36 -> 35 ;
35 [label="35: Exit cast_with_npe \n " color=yellow style=filled]
35 -> 34 ;
34 [label="34: DeclStmt \n n$9=_fun___cast(&base:class Base *,sizeof(class Derived ( sub )(cast)):void ) [line 45]\n *&derived:class Derived *=n$9 [line 45]\n " shape="box"]
34 [label="34: Start cast_with_npe\nFormals: \nLocals: derived:class Derived * base:class Base \n DECLARE_LOCALS(&return,&derived,&base); [line 51]\n " color=yellow style=filled]
34 -> 33 ;
33 [label="33: DeclStmt \n *&_tmp:class Derived *&=&derived [line 46]\n " shape="box"]
34 -> 38 ;
33 [label="33: DeclStmt \n _fun_Base_Base(&base:class Base *) [line 44]\n " shape="box"]
33 -> 28 ;
33 -> 29 ;
32 [label="32: ConditinalStmt Branch \n *&0$?%__sil_tmpSIL_temp_conditional___n$2:class Derived *&=-1 [line 46]\n " shape="box"]
33 -> 32 ;
32 [label="32: DeclStmt \n n$10=_fun___cast(&base:class Base *,sizeof(class Derived ( sub )(cast)):void ) [line 45]\n *&derived:class Derived *=n$10 [line 45]\n " shape="box"]
32 -> 27 ;
31 [label="31: Return Stmt \n _fun_WrongParameterException_WrongParameterException(&0$?%__sil_tmpSIL_materialize_temp__n$6:class WrongParameterException *,\"derived\":_Bool ,\"Base is not Derived\":char *) [line 46]\n _fun_WrongParameterException_WrongParameterException(&return:int *,&0$?%__sil_tmpSIL_materialize_temp__n$6:class WrongParameterException &) [line 46]\n " shape="box"]
32 -> 31 ;
31 [label="31: DeclStmt \n *&_tmp:class Derived *&=&derived [line 46]\n " shape="box"]
31 -> 25 ;
30 [label="30: ConditinalStmt Branch \n n$5=*&_tmp:class Derived *& [line 46]\n *&0$?%__sil_tmpSIL_temp_conditional___n$2:class Derived *&=n$5 [line 46]\n " shape="box"]
31 -> 27 ;
31 -> 28 ;
30 [label="30: ConditinalStmt Branch \n _fun_WrongParameterException_WrongParameterException(&0$?%__sil_tmpSIL_materialize_temp__n$7:class WrongParameterException *,\"derived\":_Bool ,\"Base is not Derived\":char *) [line 46]\n _fun_WrongParameterException_WrongParameterException(&0$?%__sil_tmp__temp_construct_n$6:class WrongParameterException *,&0$?%__sil_tmpSIL_materialize_temp__n$7:class WrongParameterException &) [line 46]\n _fun___infer_objc_cpp_throw(&0$?%__sil_tmp__temp_construct_n$6:class WrongParameterException ) [line 46]\n *&0$?%__sil_tmpSIL_temp_conditional___n$2:class Derived *&=-1 [line 46]\n " shape="box"]
30 -> 27 ;
29 [label="29: Prune (false branch) \n n$3=*&_tmp:class Derived *& [line 46]\n n$4=*n$3:class Derived * [line 46]\n PRUNE((n$4 == 0), false); [line 46]\n " shape="invhouse"]
30 -> 26 ;
29 [label="29: ConditinalStmt Branch \n n$5=*&_tmp:class Derived *& [line 46]\n *&0$?%__sil_tmpSIL_temp_conditional___n$2:class Derived *&=n$5 [line 46]\n " shape="box"]
29 -> 31 ;
28 [label="28: Prune (true branch) \n n$3=*&_tmp:class Derived *& [line 46]\n n$4=*n$3:class Derived * [line 46]\n PRUNE((n$4 != 0), true); [line 46]\n " shape="invhouse"]
29 -> 26 ;
28 [label="28: Prune (false branch) \n n$3=*&_tmp:class Derived *& [line 46]\n n$4=*n$3:class Derived * [line 46]\n PRUNE((n$4 == 0), false); [line 46]\n " shape="invhouse"]
28 -> 30 ;
27 [label="27: + \n " ]
27 [label="27: Prune (true branch) \n n$3=*&_tmp:class Derived *& [line 46]\n n$4=*n$3:class Derived * [line 46]\n PRUNE((n$4 != 0), true); [line 46]\n " shape="invhouse"]
27 -> 26 ;
26 [label="26: Return Stmt \n n$0=*&derived:class Derived * [line 47]\n n$1=*n$0.a:int [line 47]\n *&return:int =n$1 [line 47]\n " shape="box"]
27 -> 29 ;
26 [label="26: + \n " ]
26 -> 25 ;
25 [label="25: Exit cast_with_npe_avoided_by_enforce \n " color=yellow style=filled]
25 [label="25: Return Stmt \n n$0=*&derived:class Derived * [line 47]\n n$1=*n$0.a:int [line 47]\n *&return:int =n$1 [line 47]\n " shape="box"]
24 [label="24: Start cast_with_npe_avoided_by_enforce\nFormals: \nLocals: 0$?%__sil_tmpSIL_temp_conditional___n$2:class Derived *& 0$?%__sil_tmpSIL_materialize_temp__n$6:class WrongParameterException _tmp:class Derived *& derived:class Derived * base:class Base \n DECLARE_LOCALS(&return,&0$?%__sil_tmpSIL_temp_conditional___n$2,&0$?%__sil_tmpSIL_materialize_temp__n$6,&_tmp,&derived,&base); [line 43]\n " color=yellow style=filled]
25 -> 24 ;
24 [label="24: Exit cast_with_npe_avoided_by_enforce \n " color=yellow style=filled]
24 -> 35 ;
23 [label="23: DeclStmt \n n$9=*&certificate:class Base & [line 38]\n n$10=_fun___cast(n$9:class Base *,sizeof(class Derived ( sub )(cast)):void ) [line 38]\n *&cert:class Derived *=n$10 [line 38]\n " shape="box"]
23 [label="23: Start cast_with_npe_avoided_by_enforce\nFormals: \nLocals: 0$?%__sil_tmpSIL_temp_conditional___n$2:class Derived *& 0$?%__sil_tmp__temp_construct_n$6:class WrongParameterException 0$?%__sil_tmpSIL_materialize_temp__n$7:class WrongParameterException _tmp:class Derived *& derived:class Derived * base:class Base \n DECLARE_LOCALS(&return,&0$?%__sil_tmpSIL_temp_conditional___n$2,&0$?%__sil_tmp__temp_construct_n$6,&0$?%__sil_tmpSIL_materialize_temp__n$7,&_tmp,&derived,&base); [line 43]\n " color=yellow style=filled]
23 -> 22 ;
22 [label="22: DeclStmt \n *&_tmp:class Derived *&=&cert [line 39]\n " shape="box"]
23 -> 33 ;
22 [label="22: DeclStmt \n n$10=*&certificate:class Base & [line 38]\n n$11=_fun___cast(n$10:class Base *,sizeof(class Derived ( sub )(cast)):void ) [line 38]\n *&cert:class Derived *=n$11 [line 38]\n " shape="box"]
22 -> 17 ;
22 -> 18 ;
21 [label="21: ConditinalStmt Branch \n *&0$?%__sil_tmpSIL_temp_conditional___n$2:class Derived *&=-1 [line 39]\n " shape="box"]
22 -> 21 ;
21 [label="21: DeclStmt \n *&_tmp:class Derived *&=&cert [line 39]\n " shape="box"]
21 -> 16 ;
20 [label="20: Return Stmt \n _fun_WrongParameterException_WrongParameterException(&0$?%__sil_tmpSIL_materialize_temp__n$6:class WrongParameterException *,\"cert\":_Bool ,\"Base is not Derived\":char *) [line 39]\n _fun_WrongParameterException_WrongParameterException(&return:int *,&0$?%__sil_tmpSIL_materialize_temp__n$6:class WrongParameterException &) [line 39]\n " shape="box"]
21 -> 17 ;
21 -> 18 ;
20 [label="20: ConditinalStmt Branch \n _fun_WrongParameterException_WrongParameterException(&0$?%__sil_tmpSIL_materialize_temp__n$7:class WrongParameterException *,\"cert\":_Bool ,\"Base is not Derived\":char *) [line 39]\n _fun_WrongParameterException_WrongParameterException(&0$?%__sil_tmp__temp_construct_n$6:class WrongParameterException *,&0$?%__sil_tmpSIL_materialize_temp__n$7:class WrongParameterException &) [line 39]\n _fun___infer_objc_cpp_throw(&0$?%__sil_tmp__temp_construct_n$6:class WrongParameterException ) [line 39]\n *&0$?%__sil_tmpSIL_temp_conditional___n$2:class Derived *&=-1 [line 39]\n " shape="box"]
20 -> 14 ;
20 -> 16 ;
19 [label="19: ConditinalStmt Branch \n n$5=*&_tmp:class Derived *& [line 39]\n *&0$?%__sil_tmpSIL_temp_conditional___n$2:class Derived *&=n$5 [line 39]\n " shape="box"]
@ -107,10 +99,10 @@ digraph iCFG {
14 [label="14: Exit cast_with_no_npe \n " color=yellow style=filled]
13 [label="13: Start cast_with_no_npe\nFormals: certificate:class Base &\nLocals: 0$?%__sil_tmpSIL_temp_conditional___n$2:class Derived *& 0$?%__sil_tmpSIL_materialize_temp__n$6:class WrongParameterException _tmp:class Derived *& cert:class Derived * \n DECLARE_LOCALS(&return,&0$?%__sil_tmpSIL_temp_conditional___n$2,&0$?%__sil_tmpSIL_materialize_temp__n$6,&_tmp,&cert); [line 37]\n " color=yellow style=filled]
13 [label="13: Start cast_with_no_npe\nFormals: certificate:class Base &\nLocals: 0$?%__sil_tmpSIL_temp_conditional___n$2:class Derived *& 0$?%__sil_tmp__temp_construct_n$6:class WrongParameterException 0$?%__sil_tmpSIL_materialize_temp__n$7:class WrongParameterException _tmp:class Derived *& cert:class Derived * \n DECLARE_LOCALS(&return,&0$?%__sil_tmpSIL_temp_conditional___n$2,&0$?%__sil_tmp__temp_construct_n$6,&0$?%__sil_tmpSIL_materialize_temp__n$7,&_tmp,&cert); [line 37]\n " color=yellow style=filled]
13 -> 23 ;
13 -> 22 ;
12 [label="12: Exit Base_Base \n " color=yellow style=filled]

4
infer/tests/codetoanalyze/cpp/frontend/exceptions/Exceptions.cpp.dot
Unescape View File

@ -33,10 +33,10 @@ digraph iCFG {
9 -> 11 ;
8 [label="8: Return Stmt \n *&return:int =\"Null pointer!\" [line 12]\n " shape="box"]
8 [label="8: ObjCCPPThrow \n _fun___infer_objc_cpp_throw(\"Null pointer!\":char *) [line 12]\n " shape="box"]
8 -> 2 ;
8 -> 4 ;
7 [label="7: Prune (false branch) \n PRUNE(((n$2 == 0) == 0), false); [line 11]\n " shape="invhouse"]

4
infer/tests/codetoanalyze/objc/frontend/exceptions/ExceptionExample.dot
Unescape View File

@ -5,10 +5,10 @@ digraph iCFG {
12 -> 9 ;
12 -> 10 ;
11 [label="11: Return Stmt \n n$4=_fun_NSString_stringWithUTF8String:(\"Something is not right exception\":char *) [line 31]\n n$5=_fun_NSString_stringWithUTF8String:(\"Can't perform this operation because of this or that\":char *) [line 33]\n n$6=_fun_NSException_exceptionWithName:reason:userInfo:(n$4:class NSString *,n$5:class NSString *,0:class NSDictionary *) [line 30]\n *&return:void =n$6 [line 30]\n " shape="box"]
11 [label="11: ObjCCPPThrow \n n$4=_fun_NSString_stringWithUTF8String:(\"Something is not right exception\":char *) [line 31]\n n$5=_fun_NSString_stringWithUTF8String:(\"Can't perform this operation because of this or that\":char *) [line 33]\n n$6=_fun_NSException_exceptionWithName:reason:userInfo:(n$4:class NSString *,n$5:class NSString *,0:class NSDictionary *) [line 30]\n _fun___infer_objc_cpp_throw(n$6:class NSException *) [line 30]\n " shape="box"]
11 -> 6 ;
11 -> 7 ;
10 [label="10: Prune (false branch) \n n$3=*&s:class NSString * [line 29]\n PRUNE((n$3 == 0), false); [line 29]\n " shape="invhouse"]

4
infer/tests/endtoend/cpp/infer/ThisNotNullTest.java
Unescape View File

@ -44,14 +44,14 @@ public class ThisNotNullTest {
}
@Test
public void whenInferRunsOnMethodNoThisNullDerefErrorIsFound()
public void whenInferRunsNoNullDerefErrorIsFound()
throws InterruptedException, IOException, InferException {
InferResults inferResults = InferRunner.runInferCPP(inferCmd);
String[] proceduresWithNullDeref = {
/* nothing should be reported */
};
assertThat(
"Results should contain the no null dereference",
"Results should not contain any null dereference",
inferResults,
containsExactly(
NULL_DEREFERENCE,

63
infer/tests/endtoend/cpp/infer/ThrowAsAssertTest.java
Unescape View File

@ -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.
*/
package endtoend.cpp.infer;
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 ThrowAsAssertTest {
public static final String FILE =
"infer/tests/codetoanalyze/cpp/errors/npe/throw_as_assert.cpp";
private static ImmutableList<String> inferCmd;
public static final String NULL_DEREFERENCE = "NULL_DEREFERENCE";
@ClassRule
public static DebuggableTemporaryFolder folder =
new DebuggableTemporaryFolder();
@BeforeClass
public static void runInfer() throws InterruptedException, IOException {
inferCmd = InferRunner.createCPPInferCommand(folder, FILE);
}
@Test
public void whenInferRunsOnMethodNoThisNullDerefErrorIsFound()
throws InterruptedException, IOException, InferException {
InferResults inferResults = InferRunner.runInferCPP(inferCmd);
String[] proceduresWithNullDeref = {
/* nothing should be reported */
};
assertThat(
"Results should not contain any null dereference",
inferResults,
containsExactly(
NULL_DEREFERENCE,
FILE,
proceduresWithNullDeref
)
);
}
}
Write Preview
Loading…
Cancel
Save