diff --git a/infer/src/clang/cFrontend_config.ml b/infer/src/clang/cFrontend_config.ml index d925bab16..70255880d 100644 --- a/infer/src/clang/cFrontend_config.ml +++ b/infer/src/clang/cFrontend_config.ml @@ -168,3 +168,5 @@ let infer = "infer" let block = "block" let atomic_att = "<\"Atomic\">" + +let infer_skip_gcc_ast_stmt = "__infer_skip_gcc_ast_stmt" diff --git a/infer/src/clang/cFrontend_config.mli b/infer/src/clang/cFrontend_config.mli index f576dcb54..7ee5420a6 100644 --- a/infer/src/clang/cFrontend_config.mli +++ b/infer/src/clang/cFrontend_config.mli @@ -163,3 +163,5 @@ val infer : string val block : string val atomic_att : string + +val infer_skip_gcc_ast_stmt : string diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 6d6ed6f1f..2fc5b416d 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -1995,6 +1995,25 @@ struct | Some exp -> instruction trans_state exp | None -> assert false + and gccAstStmt_trans 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_ast_stmt in + let sil_fun = Sil.Const (Sil.Cfun fun_name) in + let call_instr = Sil.Call ([], sil_fun, params, sil_loc, Sil.cf_default) in + let res_trans_call = { empty_res_trans with + ids = []; + 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 + "GCCAstStmt" stmt_info all_res_trans in + { res_trans_to_parent with exps = res_trans_call.exps } + (* Translates a clang instruction into SIL instructions. It takes a *) (* a trans_state containing current info on the translation and it returns *) (* a result_state.*) @@ -2256,6 +2275,9 @@ struct | GenericSelectionExpr _ -> (* to be fixed when we dump the right info in the ast *) { empty_res_trans with exps = [(Sil.exp_get_undefined false, Sil.Tvoid)] } + | GCCAsmStmt (stmt_info, stmts) -> + gccAstStmt_trans trans_state stmt_info stmts + | s -> (Printing.log_stats "\n!!!!WARNING: found statement %s. \nACTION REQUIRED: Translation need to be defined. Statement ignored.... \n" (Ast_utils.string_of_stmt s); diff --git a/infer/tests/codetoanalyze/c/errors/null_dereference/asm_angelism.c b/infer/tests/codetoanalyze/c/errors/null_dereference/asm_angelism.c new file mode 100644 index 000000000..f59f94239 --- /dev/null +++ b/infer/tests/codetoanalyze/c/errors/null_dereference/asm_angelism.c @@ -0,0 +1,17 @@ +/* + * 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. + */ + +int test2() { + int* x = 0; + int y; + int z; + int h; + asm("cpuid " : "=a"(x), "=b"(y), "=c"(z), "=d"(h) : "0"(0)); + return *x; +} diff --git a/infer/tests/codetoanalyze/c/frontend/unusual_stmts/asm.c b/infer/tests/codetoanalyze/c/frontend/unusual_stmts/asm.c new file mode 100644 index 000000000..9e8bffd31 --- /dev/null +++ b/infer/tests/codetoanalyze/c/frontend/unusual_stmts/asm.c @@ -0,0 +1,29 @@ +/* + * 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. + */ + +int test() { + int x; + int y; + int z; + int h; + asm("cpuid " : "=a"(x), "=b"(y), "=c"(z), "=d"(h) : "0"(0)); + return 0; +} + +int main() { + int src = 1; + int dst; + + asm( + "mov %1, %0\n\t" + "add $1, %0" + : "=r"(dst) + : "r"(src)); + return 0; +} diff --git a/infer/tests/codetoanalyze/c/frontend/unusual_stmts/asm.c.dot b/infer/tests/codetoanalyze/c/frontend/unusual_stmts/asm.c.dot new file mode 100644 index 000000000..0131eb708 --- /dev/null +++ b/infer/tests/codetoanalyze/c/frontend/unusual_stmts/asm.c.dot @@ -0,0 +1,36 @@ +digraph iCFG { +9 [label="9: DeclStmt \n *&src:int =1 [line 20]\n " shape="box"] + + + 9 -> 8 ; +8 [label="8: GCCAstStmt \n n$0=*&src:int [line 27]\n _fun___infer_skip_gcc_ast_stmt(&dst:int &,n$0:int ) [line 23]\n REMOVE_TEMPS(n$0); [line 23]\n NULLIFY(&src,false); [line 23]\n " shape="box"] + + + 8 -> 7 ; +7 [label="7: Return Stmt \n *&return:int =0 [line 28]\n NULLIFY(&dst,false); [line 28]\n APPLY_ABSTRACTION; [line 28]\n " shape="box"] + + + 7 -> 6 ; +6 [label="6: Exit main \n " color=yellow style=filled] + + +5 [label="5: Start main\nFormals: \nLocals: dst:int src:int \n DECLARE_LOCALS(&return,&dst,&src); [line 19]\n NULLIFY(&src,false); [line 19]\n " color=yellow style=filled] + + + 5 -> 9 ; +4 [label="4: GCCAstStmt \n _fun___infer_skip_gcc_ast_stmt(&x:int &,&y:int &,&z:int &,&h:int &,0:int ) [line 15]\n " shape="box"] + + + 4 -> 3 ; +3 [label="3: Return Stmt \n *&return:int =0 [line 16]\n NULLIFY(&h,false); [line 16]\n NULLIFY(&x,false); [line 16]\n NULLIFY(&y,false); [line 16]\n NULLIFY(&z,false); [line 16]\n APPLY_ABSTRACTION; [line 16]\n " shape="box"] + + + 3 -> 2 ; +2 [label="2: Exit test \n " color=yellow style=filled] + + +1 [label="1: Start test\nFormals: \nLocals: h:int z:int y:int x:int \n DECLARE_LOCALS(&return,&h,&z,&y,&x); [line 10]\n " color=yellow style=filled] + + + 1 -> 4 ; +} diff --git a/infer/tests/endtoend/c/AsmAngelismTest.java b/infer/tests/endtoend/c/AsmAngelismTest.java new file mode 100644 index 000000000..e8b6c8cc1 --- /dev/null +++ b/infer/tests/endtoend/c/AsmAngelismTest.java @@ -0,0 +1,52 @@ +/* + * 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 endtoend.c; + +import static org.hamcrest.MatcherAssert.assertThat; +import static utils.matchers.ResultContainsExactly.containsExactly; + +import org.junit.BeforeClass; +import org.junit.Test; + +import java.io.IOException; + +import utils.InferException; +import utils.InferResults; + +public class AsmAngelismTest { + + public static final String SOURCE_FILE = "null_dereference/asm_angelism.c"; + + public static final String NULL_DEREFERENCE = "NULL_DEREFERENCE"; + + private static InferResults inferResults; + + @BeforeClass + public static void runInfer() throws InterruptedException, IOException { + inferResults = InferResults.loadCInferResults( + AsmAngelismTest.class, + SOURCE_FILE); + } + + @Test + public void angelismNPETest() throws InterruptedException, IOException, InferException { + String[] procedures = {}; + assertThat( + "Results should not contain null pointer dereference error", + inferResults, + containsExactly( + NULL_DEREFERENCE, + SOURCE_FILE, + procedures + ) + ); + } + +} diff --git a/infer/tests/frontend/c/UnusualStmtsTest.java b/infer/tests/frontend/c/UnusualStmtsTest.java new file mode 100644 index 000000000..c72965772 --- /dev/null +++ b/infer/tests/frontend/c/UnusualStmtsTest.java @@ -0,0 +1,39 @@ +/* + * 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.c; + +import org.junit.Rule; +import org.junit.Test; + +import java.io.IOException; + +import utils.DebuggableTemporaryFolder; +import utils.InferException; +import utils.ClangFrontendUtils; + +public class UnusualStmtsTest { + + String boolBasePath = "infer/tests/codetoanalyze/c/frontend/unusual_stmts/"; + + @Rule + public DebuggableTemporaryFolder folder = new DebuggableTemporaryFolder(); + + void frontendTest(String fileRelative) throws InterruptedException, IOException, InferException { + ClangFrontendUtils.createAndCompareCDotFiles(folder, boolBasePath + fileRelative); + } + + + @Test + public void whenCaptureRunCommaThenDotFilesAreTheSame() + throws InterruptedException, IOException, InferException { + frontendTest("asm.c"); + } + +}