[purity] Enable Clang in purity analysis

Reviewed By: mbouaziz

Differential Revision: D14437821

fbshipit-source-id: 4b5f761b2

Makefile

@@ -52,6 +52,7 @@ DIRECT_TESTS += \
   c_errors \
   c_frontend \
   c_performance \
+  c_purity \
   c_uninit \
   cpp_bufferoverrun \
   cpp_conflicts \

infer/src/checkers/invariantModels.ml

@@ -39,6 +39,7 @@ module ProcName = struct
     let open ProcnameDispatcher.ProcName in
     make_dispatcher
       [ +invariant_builtins <>--> VariantForHoisting
+      ; -"__variable_initialization" <>--> Invariant
       ; +(fun _ name -> BuiltinDecl.is_declared (Typ.Procname.from_string_c_fun name))
         <>--> Variant
       ; +PatternMatch.implements_android "text.TextUtils" &:: "isEmpty" <>--> VariantForHoisting

infer/src/checkers/purity.ml

@@ -36,7 +36,7 @@ module TransferFunctions = struct
   let get_alias_set inferbo_mem var =
     let default = ModifiedVarSet.empty in
     let alias_v = BufferOverrunDomain.Mem.find (AbsLoc.Loc.of_var var) inferbo_mem in
-    let pow_locs = BufferOverrunDomain.Val.get_pow_loc alias_v in
+    let pow_locs = BufferOverrunDomain.Val.get_all_locs alias_v in
     AbsLoc.PowLoc.fold
       (fun loc modified_acc ->
         AbsLoc.Loc.get_path loc
@@ -145,6 +145,8 @@ module TransferFunctions = struct
           else find_params_matching_modified_args inferbo_mem formals args callee_modified_params)
 
 
+  let modified_global ae = HilExp.AccessExpression.get_base ae |> fst |> Var.is_global
+
   let exec_instr (astate : Domain.t)
       {tenv; ProcData.extras= {inferbo_invariant_map; formals; get_callee_summary}}
       (node : CFG.Node.t) (instr : HilInstr.t) =
@@ -155,7 +157,8 @@ module TransferFunctions = struct
       Option.value_exn (BufferOverrunAnalysis.extract_post node_id inferbo_invariant_map)
     in
     match instr with
-    | Assign (ae, _, _) when is_heap_access ae ->
+    | Assign (ae, _, _)
+      when is_heap_access ae || (Language.curr_language_is Clang && modified_global ae) ->
         track_modified_params inferbo_mem formals ae |> Domain.join astate
     | Call (_, Direct called_pname, args, _, _) ->
         Domain.join astate
@@ -187,13 +190,16 @@ end
 module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions)
 
 let should_report pdesc =
-  match Procdesc.get_proc_name pdesc with
+  let proc_name = Procdesc.get_proc_name pdesc in
-  | Typ.Procname.Java java_pname as proc_name ->
   (not (Typ.Procname.is_constructor proc_name))
-      && (not (Typ.Procname.Java.is_class_initializer java_pname))
+  &&
-      && not (Typ.Procname.Java.is_access_method java_pname)
+  match proc_name with
+  | Typ.Procname.Java java_pname ->
+      not
+        ( Typ.Procname.Java.is_class_initializer java_pname
+        || Typ.Procname.Java.is_access_method java_pname )
   | _ ->
-      L.(die InternalError "Not supposed to run on non-Java code.")
+      true
 
 
 let report_errors pdesc astate summary =

infer/src/checkers/registerCheckers.ml

@@ -123,7 +123,8 @@ let all_checkers =
         ; (Cluster Starvation.reporting, Language.Clang) ] }
   ; { name= "purity"
     ; active= Config.purity || Config.loop_hoisting
-    ; callbacks= [(Procedure Purity.checker, Language.Java)] }
+    ; callbacks=
+        [(Procedure Purity.checker, Language.Java); (Procedure Purity.checker, Language.Clang)] }
   ; { name= "Class loading analysis"
     ; active= Config.class_loads
     ; callbacks= [(Procedure ClassLoads.analyze_procedure, Language.Java)] } ]

infer/tests/codetoanalyze/c/purity/Makefile

@@ -0,0 +1,13 @@
+# Copyright (c) 2019-present, Facebook, Inc.
+#
+# This source code is licensed under the MIT license found in the
+# LICENSE file in the root directory of this source tree.
+TESTS_DIR = ../../..
+
+CLANG_OPTIONS = -c
+INFER_OPTIONS = -F --project-root $(TESTS_DIR) --purity-only --function-pointer-specialization
+INFERPRINT_OPTIONS = --issues-tests
+
+SOURCES = $(wildcard *.c)
+
+include $(TESTS_DIR)/clang.make

infer/tests/codetoanalyze/c/purity/array.c

@@ -0,0 +1,39 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <stdio.h>
+#include <time.h>
+
+void swap_bad(int* array, int i, int j) {
+  int tmp = array[i];
+  array[i] = array[j];
+  array[j] = tmp;
+}
+
+void alias_mod_bad(int array[], int i, int j) {
+  int* a = array;
+  a[j] = i;
+}
+
+void fresh_arr_ok(int size) {
+  int arr[size];
+  for (int i = 0; i < size - 1; i++) {
+    arr[i] = 0;
+  }
+}
+
+void call_impure_with_local_ok(int size) {
+  int arr[size];
+  alias_mod_bad(arr, 0, 9);
+}
+
+void time_bad() {
+  time_t rawtime;
+  struct tm* timeinfo;
+
+  time(&rawtime);
+  timeinfo = localtime(&rawtime);
+}

infer/tests/codetoanalyze/c/purity/global_test.c

@@ -0,0 +1,29 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+int global;
+
+static int s;
+
+void static_incr_bad() { s += 1; }
+
+void global_write_bad(int x, int y) { global += x + y; }
+
+void call_impure_bad(int size) {
+  for (int i = 0; i < size; i++) {
+    global_write_bad(i, size);
+  }
+}
+
+int local_write_ok(int x, int y) {
+  int k = x + y;
+  k++;
+  return k;
+}
+
+// calls foo which modifies global var
+void call_set_bad() { static_incr_bad(); }

infer/tests/codetoanalyze/c/purity/issues.exp

@@ -0,0 +1,6 @@
+codetoanalyze/c/purity/array.c, call_impure_with_local_ok, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function call_impure_with_local_ok]
+codetoanalyze/c/purity/array.c, fresh_arr_ok, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function fresh_arr_ok]
+codetoanalyze/c/purity/global_test.c, local_write_ok, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function local_write_ok]
+codetoanalyze/c/purity/struct.c, set_fresh_ok, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function set_fresh_ok]
+codetoanalyze/c/purity/struct.c, set_fresh_primitive_ok, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function set_fresh_primitive_ok]
+codetoanalyze/c/purity/struct.c, variable_init_ok, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function variable_init_ok]

infer/tests/codetoanalyze/c/purity/struct.c

@@ -0,0 +1,35 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+typedef struct {
+  int i;
+} Foo;
+
+static int variable_init_ok(const int* x) {
+  const Foo* foo = (const Foo*)x;
+  return foo->i;
+}
+
+Foo* variable_init_bad(const int* x) {
+  Foo* foo = (const Foo*)x; // aliasing to x
+  foo->i = 0;
+  return foo;
+}
+
+void set_fresh_ok() {
+  Foo* foo = {0};
+  foo->i = 0;
+}
+
+void set_fresh_primitive_ok(int x) {
+  Foo* foo = {x};
+  foo->i = 0;
+}
+
+void set_alias_primitive_bad(int* x) {
+  Foo* foo = {x};
+  foo->i = 0;
+}