diff --git a/Makefile.config b/Makefile.config index 784ad0fb1..290842a42 100644 --- a/Makefile.config +++ b/Makefile.config @@ -94,10 +94,8 @@ JAVA_DEPS_NO_MODELS = \ JAVA_DEPS = $(JAVA_DEPS_NO_MODELS) $(JAVA_MODELS_JAR) -# markers to keep track of when clang models have been rebuilt -C_MODELS_FILE = $(SPECS_LIB_DIR)/c_models -CPP_MODELS_FILE = $(SPECS_LIB_DIR)/cpp_models -OBJC_MODELS_FILE = $(SPECS_LIB_DIR)/objc_models +# marker to keep track of when clang models have been rebuilt +MODELS_RESULTS_FILE = $(SPECS_LIB_DIR)/clang_models CLANG_DEPS_NO_MODELS = \ $(addprefix $(PYTHON_LIB_DIR)/, \ @@ -105,13 +103,9 @@ CLANG_DEPS_NO_MODELS = \ $(addprefix $(CAPTURE_LIB_DIR)/, util.py) \ $(INFER_BIN) -CLANG_DEPS = $(CLANG_DEPS_NO_MODELS) $(C_MODELS_FILE) $(CPP_MODELS_FILE) \ +CLANG_DEPS = $(CLANG_DEPS_NO_MODELS) $(MODELS_RESULTS_FILE) \ $(shell find $(MODELS_DIR)/cpp/include -type f) -ifneq ($(XCODE_SELECT),no) -CLANG_DEPS += $(OBJC_MODELS_FILE) -endif - INTERACTIVE = $(shell [ -t 0 ] && echo 1) # remove "jobserver-fds" because it contains "s"... SILENT = $(findstring s,$(subst jobserver-fds,,$(MAKEFLAGS))) diff --git a/infer/models/Makefile b/infer/models/Makefile index d649c362f..76b6b48a4 100644 --- a/infer/models/Makefile +++ b/infer/models/Makefile @@ -8,59 +8,60 @@ ROOT_DIR = ../.. include $(ROOT_DIR)/Makefile.config -C_MODELS_DIR = c -CPP_MODELS_DIR = cpp +C_MODELS_DIR = c/src +CPP_MODELS_DIR = cpp/src JAVA_MODELS_DIR = java -OBJC_MODELS_DIR = objc +OBJC_MODELS_DIR = objc/src -CLANG_MODELS_FILE = $(SPECS_LIB_DIR)/clang_models - -CLANG_SUBDIRS = $(C_MODELS_DIR) $(CPP_MODELS_DIR) -ifneq (no, $(XCODE_SELECT)) -CLANG_SUBDIRS += $(OBJC_MODELS_DIR) -endif +MODELS_INFER_OUT = infer-out +MODELS_INFER_OPTIONS = --biabduction-only --results-dir $(MODELS_INFER_OUT) --models-mode all: -ifeq ($(BUILD_C_ANALYZERS),yes) -all: clang -endif -ifeq ($(BUILD_JAVA_ANALYZERS),yes) -all: java -endif - -.PHONY: java clang clean clean_specs $(CLANG_SUBDIRS) +.PHONY: clean_specs clean_specs: - $(REMOVE) $(SPECS_LIB_DIR)/*.specs $(C_MODELS_FILE) $(CPP_MODELS_FILE) $(OBJC_MODELS_FILE) - -$(CLANG_SUBDIRS): - $(QUIET)$(MAKE) -C $@ out/report.json + $(REMOVE) $(SPECS_LIB_DIR)/*.specs $(MODELS_RESULTS_FILE) +# clang models specs only for now # The clang deps have changed, so the models need to be rebuilt. If infer itself has changed, we # need to nuke the previous specs files in case the serialization has changed, otherwise we might # encounter a segfault reading them. -$(CLANG_MODELS_FILE): $(CLANG_DEPS_NO_MODELS) +$(MODELS_RESULTS_FILE): $(MAKEFILE_LIST) $(CLANG_DEPS_NO_MODELS) $(QUIET)$(MAKE) clean_specs -# Since [CLANG_DEPS_NO_MODELS] is newer than [CLANG_MODELS_FILE], it is also newer than the -# previously built clang models, so they will all be rebuilt by the subdirs' Makefiles. - $(QUIET)$(MAKE) $(CLANG_SUBDIRS) -# Run the installs sequentially as the models shared some of the C procedures. This can cause -# race conditions when copying specs files inside lib/specs/ - $(QUIET)for clang_dir in $(CLANG_SUBDIRS); do $(MAKE) -C "$$clang_dir" install; done -# Maintain the invariant that [CLANG_MODELS_FILE] is newer than the clang models. + $(QUIET)$(REMOVE_DIR) $(MODELS_INFER_OUT) +# [make clean] each time to recompile all the models +ifeq ($(BUILD_C_ANALYZERS),yes) + $(QUIET)$(MAKE) -C $(C_MODELS_DIR) clean + $(QUIET)$(MAKE) -C $(CPP_MODELS_DIR) clean +ifneq (no, $(XCODE_SELECT)) + $(QUIET)$(MAKE) -C $(OBJC_MODELS_DIR) clean +endif + $(QUIET)$(call silent_on_success,Capturing C models,\ + $(INFER_BIN) capture $(MODELS_INFER_OPTIONS) --continue -- $(MAKE) -C $(C_MODELS_DIR) all) + $(QUIET)$(call silent_on_success,Capturing C++ models,\ + $(INFER_BIN) capture $(MODELS_INFER_OPTIONS) --continue -- $(MAKE) -C $(CPP_MODELS_DIR) all) +ifneq (no, $(XCODE_SELECT)) + $(QUIET)$(call silent_on_success,Capturing ObjC models,\ + $(INFER_BIN) capture $(MODELS_INFER_OPTIONS) --continue -- $(MAKE) -C $(OBJC_MODELS_DIR) all) +endif +endif + $(QUIET)$(call silent_on_success,Analyzing clang models,\ + $(INFER_BIN) analyze $(MODELS_INFER_OPTIONS)) + $(QUIET)$(INSTALL_DATA) $(MODELS_INFER_OUT)/specs/*.specs $(SPECS_LIB_DIR) $(QUIET)touch $@ -clang: $(CLANG_MODELS_FILE) -# Run the sub-makes unconditionally since they know more about when they need to be -# rebuilt. For instance, they need to be rebuilt when their source files change, which is not -# taken into account by the dependencies of the $(CLANG_MODELS_FILE) target. If we rebuilt -# $(CLANG_MODELS_FILE) already, then the command below will be a no-op (so we don't rebuild -# the models twice). - $(QUIET)$(MAKE) $(CLANG_SUBDIRS) - +.PHONY: java java: $(QUIET)$(MAKE) -C $@ install +ifeq ($(BUILD_C_ANALYZERS),yes) +all: $(MODELS_RESULTS_FILE) +endif +ifeq ($(BUILD_JAVA_ANALYZERS),yes) +all: java +endif + +.PHONY: clean clean: clean_specs $(QUIET)$(MAKE) -C $(JAVA_MODELS_DIR) clean $(QUIET)$(MAKE) -C $(C_MODELS_DIR) clean diff --git a/infer/models/c/Makefile b/infer/models/c/Makefile deleted file mode 100644 index 688fccc67..000000000 --- a/infer/models/c/Makefile +++ /dev/null @@ -1,32 +0,0 @@ -# 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. - -ROOT_DIR = ../../.. -include $(ROOT_DIR)/Makefile.config - -C_MODELS_SOURCES = $(shell find src/ -name "*.[ch]") -INFER_RESULTS = out/report.json - -all: install - -$(INFER_RESULTS): $(C_MODELS_SOURCES) $(CLANG_DEPS_NO_MODELS) $(MAKEFILE_LIST) -# make clean in src/ to recompile all the models - $(QUIET)$(call silent_on_success,Building C models,\ - $(INFER_BIN) -a checkers --biabduction-only -o $(@D) --models-mode -- $(MAKE) -C src clean all) - -$(C_MODELS_FILE): $(INFER_RESULTS) - $(QUIET)$(INSTALL_DATA) $(dir $(INFER_RESULTS))/specs/*.specs $(SPECS_LIB_DIR) - $(QUIET)touch $@ - -install: $(C_MODELS_FILE) - -clean: - $(REMOVE) $(C_MODELS_FILE) - $(REMOVE_DIR) $(dir $(INFER_RESULTS)) - $(QUIET)$(MAKE) -C src clean - -.PHONY: all clean install diff --git a/infer/models/cpp/Makefile b/infer/models/cpp/Makefile deleted file mode 100644 index 13c9d521b..000000000 --- a/infer/models/cpp/Makefile +++ /dev/null @@ -1,34 +0,0 @@ -# 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. - -ROOT_DIR = ../../.. -include $(ROOT_DIR)/Makefile.config - -MODELS_SOURCES = $(shell find src/ -name "*.cpp") \ - $(shell find src/c_src/ -name "*.[ch]") \ - $(shell find include -type f) -INFER_RESULTS = out/report.json - -all: install - -$(INFER_RESULTS): $(MODELS_SOURCES) $(CLANG_DEPS_NO_MODELS) $(MAKEFILE_LIST) -# make clean in src/ to recompile all the models - $(QUIET)$(call silent_on_success,Building C++ models,\ - $(INFER_BIN) -a checkers --biabduction-only -o $(@D) --models-mode -- $(MAKE) -C src clean all) - -$(CPP_MODELS_FILE): $(INFER_RESULTS) - $(QUIET)$(INSTALL_DATA) $(dir $(INFER_RESULTS))/specs/*.specs $(SPECS_LIB_DIR) - $(QUIET)touch $@ - -install: $(CPP_MODELS_FILE) - -clean: - $(REMOVE) $(CPP_MODELS_FILE) - $(REMOVE_DIR) $(dir $(INFER_RESULTS)) - $(QUIET)$(MAKE) -C src clean - -.PHONY: all clean install diff --git a/infer/models/objc/Makefile b/infer/models/objc/Makefile deleted file mode 100644 index 2106e8c3d..000000000 --- a/infer/models/objc/Makefile +++ /dev/null @@ -1,32 +0,0 @@ -# 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. - -ROOT_DIR = ../../.. -include $(ROOT_DIR)/Makefile.config - -OBJC_MODELS_SOURCES = $(shell find src/ -name "*.[chm]") -INFER_RESULTS = out/report.json - -all: install - -$(INFER_RESULTS): $(OBJC_MODELS_SOURCES) $(CLANG_DEPS_NO_MODELS) $(MAKEFILE_LIST) -# make clean in src/ to recompile all the models - $(QUIET)$(call silent_on_success,Building Objective-C models,\ - $(INFER_BIN) -a checkers --biabduction-only -o $(@D) --models-mode -- $(MAKE) -C src clean all) - -$(OBJC_MODELS_FILE): $(INFER_RESULTS) - $(QUIET)$(INSTALL_DATA) $(dir $(INFER_RESULTS))/specs/*.specs $(SPECS_LIB_DIR) - $(QUIET)touch $@ - -install: $(OBJC_MODELS_FILE) - -clean: - $(REMOVE) $(OBJC_MODELS_FILE) - $(REMOVE_DIR) $(dir $(INFER_RESULTS)) - $(QUIET)$(MAKE) -C src clean - -.PHONY: all clean install diff --git a/infer/src/IR/Cfg.ml b/infer/src/IR/Cfg.ml index 79c1b5090..8163b41b9 100644 --- a/infer/src/IR/Cfg.ml +++ b/infer/src/IR/Cfg.ml @@ -203,3 +203,8 @@ let pp_proc_signatures fmt cfg = F.fprintf fmt "METHOD SIGNATURES@\n@." ; let sorted_procs = List.sort ~compare:Procdesc.compare (get_all_proc_descs cfg) in List.iter ~f:(fun pdesc -> F.fprintf fmt "%a@." Procdesc.pp_signature pdesc) sorted_procs + + +let merge ~src ~dst = + Typ.Procname.Hash.iter (fun pname cfg -> Typ.Procname.Hash.replace dst pname cfg) src ; + dst diff --git a/infer/src/IR/Cfg.mli b/infer/src/IR/Cfg.mli index 6cbdaeb8e..960f22736 100644 --- a/infer/src/IR/Cfg.mli +++ b/infer/src/IR/Cfg.mli @@ -41,6 +41,10 @@ val save_attributes : SourceFile.t -> t -> unit val inline_java_synthetic_methods : t -> unit (** Inline the java synthetic methods in the cfg (in-place) *) +val merge : src:t -> dst:t -> t +(** Best-effort merge of [src] into [dst]. If a procedure is both in [dst] and [src], the one in + [src] will get overwritten. *) + val pp_proc_signatures : Format.formatter -> t -> unit module SQLite : SqliteUtils.Data with type t = t diff --git a/infer/src/IR/SourceFiles.ml b/infer/src/IR/SourceFiles.ml index bc6b1c7dc..acdaa0f2a 100644 --- a/infer/src/IR/SourceFiles.ml +++ b/infer/src/IR/SourceFiles.ml @@ -16,8 +16,46 @@ let store_statement = VALUES (:source, :cfgs, :tenv, :proc_names, :freshly_captured) |} +let select_existing_statement = + ResultsDatabase.register_statement + "SELECT cfgs, type_environment FROM source_files WHERE source_file = :source AND \ + freshly_captured = 1" + + +let get_existing_data source_file = + ResultsDatabase.with_registered_statement select_existing_statement ~f:(fun db stmt -> + SourceFile.SQLite.serialize source_file |> Sqlite3.bind stmt 1 + (* :source *) + |> SqliteUtils.check_sqlite_error db ~log:"get_existing_data bind source file" ; + match Sqlite3.step stmt with + | Sqlite3.Rc.ROW -> + (* the operation returned a result, get it *) + let cfgs = Sqlite3.column stmt 0 |> Cfg.SQLite.deserialize + and tenv = Sqlite3.column stmt 1 |> Tenv.SQLite.deserialize in + (match Sqlite3.step stmt with DONE -> () | _ -> assert false) ; + Some (cfgs, tenv) + | DONE -> + None + | err -> + L.die InternalError "Looking for pre-existing cfgs: %s (%s)" (Sqlite3.Rc.to_string err) + (Sqlite3.errmsg db) ) + + let add source_file cfg tenv = Cfg.inline_java_synthetic_methods cfg ; + let cfg, tenv = + (* The same source file may get captured several times in a single capture event, for instance + because it is compiled with different options, or from different symbolic links. This may + generate different procedures in each phase, so make an attempt to merge them into the same + CFG. *) + match get_existing_data source_file with + | Some (old_cfg, old_tenv) -> + L.debug Capture Quiet "Merging capture data for already-captured '%a'@\n" SourceFile.pp + source_file ; + (Cfg.merge ~dst:old_cfg ~src:cfg, Tenv.merge ~dst:old_tenv ~src:tenv) + | None -> + (cfg, tenv) + in (* NOTE: it's important to write attribute files to disk before writing cfgs to disk. OndemandCapture module relies on it - it uses existance of the cfg as a barrier to make sure that all attributes were written to disk (but not necessarily flushed) *) diff --git a/infer/src/IR/Tenv.ml b/infer/src/IR/Tenv.ml index 0c7da1589..8a8faea94 100644 --- a/infer/src/IR/Tenv.ml +++ b/infer/src/IR/Tenv.ml @@ -8,6 +8,7 @@ *) open! IStd module Hashtbl = Caml.Hashtbl +module L = Logging (** Module for Type Environments. *) @@ -92,6 +93,17 @@ module SQLite : SqliteUtils.Data with type t = per_file = struct FileLocal (Marshal.from_string b 0) end +let merge ~src ~dst = + match (src, dst) with + | Global, Global -> + Global + | FileLocal src_tenv, FileLocal dst_tenv -> + TypenameHash.iter (fun pname cfg -> TypenameHash.replace dst_tenv pname cfg) src_tenv ; + FileLocal dst_tenv + | Global, FileLocal _ | FileLocal _, Global -> + L.die InternalError "Cannot merge Global tenv with FileLocal tenv" + + let load_statement = ResultsDatabase.register_statement "SELECT type_environment FROM source_files WHERE source_file = :k" diff --git a/infer/src/IR/Tenv.mli b/infer/src/IR/Tenv.mli index 4b4a759b1..094a14840 100644 --- a/infer/src/IR/Tenv.mli +++ b/infer/src/IR/Tenv.mli @@ -48,4 +48,8 @@ val language_is : t -> Language.t -> bool type per_file = Global | FileLocal of t +val merge : src:per_file -> dst:per_file -> per_file +(** Best-effort merge of [src] into [dst]. If a procedure is both in [dst] and [src], the one in + [src] will get overwritten. *) + module SQLite : SqliteUtils.Data with type t = per_file