Translate GCCAsmStmt

Reviewed By: akotulski, sblackshear

Differential Revision: D3006192

fb-gh-sync-id: a81493b
shipit-source-id: a81493b

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"

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

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);

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;
+}

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;
+}

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 ;
+}

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
+        )
+    );
+  }
+
+}

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");
+  }
+
+}