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

[java] store specs files same as clang models

Browse Source 
Summary: Reduces complexity in Summary.ml (see next diff).

Reviewed By: skcho

Differential Revision: D20891116

fbshipit-source-id: d91c08e5f
master
Jules Villard 5 years ago committed by Facebook GitHub Bot
parent 4b4caea260
commit 224e0b7c52
9 changed files with 69 additions and 91 deletions
Show Stats Download Patch File Download Diff File

2
.gitignore vendored
Unescape View File

@ -117,7 +117,7 @@ buck-out/
/infer/src/base/Version.ml /infer/src/base/Version.ml
/infer/models/java/models/ /infer/models/java/models/
/infer/models/java/models.jar /infer/models/models.jar
/infer/lib/java/models.jar /infer/lib/java/models.jar
/infer/models/java/bootclasspath /infer/models/java/bootclasspath
/infer/models/c/out/ /infer/models/c/out/

8
Makefile.config
Unescape View File

@ -79,6 +79,9 @@ ifeq ($(BUILD_JAVA_ANALYZERS),yes)
JAVA_HOME=$(USER_JAVA_HOME) JAVA_HOME=$(USER_JAVA_HOME)
endif endif
# marker to keep track of when models have been rebuilt
MODELS_RESULTS_FILE = $(SPECS_LIB_DIR)/models
ANDROID_JAR = $(LIB_DIR)/java/android/android-23.jar ANDROID_JAR = $(LIB_DIR)/java/android/android-23.jar
GUAVA_JAR = $(DEPENDENCIES_DIR)/java/guava/guava-23.0.jar GUAVA_JAR = $(DEPENDENCIES_DIR)/java/guava/guava-23.0.jar
INFER_ANNOTATIONS_JAR = $(ANNOTATIONS_DIR)/annotations.jar INFER_ANNOTATIONS_JAR = $(ANNOTATIONS_DIR)/annotations.jar
@ -91,10 +94,7 @@ JAVA_DEPS_NO_MODELS = \
$(ANDROID_JAR) $(GUAVA_JAR) $(JACKSON_JAR) $(JSR_305_JAR) $(INFER_ANNOTATIONS_JAR) \ $(ANDROID_JAR) $(GUAVA_JAR) $(JACKSON_JAR) $(JSR_305_JAR) $(INFER_ANNOTATIONS_JAR) \
$(INFER_BIN) $(INFER_BIN)
JAVA_DEPS = $(JAVA_DEPS_NO_MODELS) $(JAVA_MODELS_JAR) JAVA_DEPS = $(JAVA_DEPS_NO_MODELS) $(JAVA_MODELS_JAR) $(MODELS_RESULTS_FILE)
# marker to keep track of when clang models have been rebuilt
MODELS_RESULTS_FILE = $(SPECS_LIB_DIR)/clang_models
CLANG_DEPS_NO_MODELS = $(INFER_BIN) CLANG_DEPS_NO_MODELS = $(INFER_BIN)

80
infer/models/Makefile
Unescape View File

@ -12,22 +12,27 @@ JAVA_MODELS_DIR = java
OBJC_MODELS_DIR = objc/src OBJC_MODELS_DIR = objc/src
OBJCPP_MODELS_DIR = objcpp/src OBJCPP_MODELS_DIR = objcpp/src
MODELS_INFER_OUT = infer-out CLANG_RESULTS_DIR = infer-out-clang
MODELS_INFER_OPTIONS = --jobs 1 --biabduction-only --results-dir $(MODELS_INFER_OUT) --biabduction-models-mode CLANG_INFER_OPTIONS = --jobs 1 --biabduction-only --results-dir $(CLANG_RESULTS_DIR) --biabduction-models-mode
all: JAVA_MODELS_OUT = java/models
JAVA_RESULTS_DIR = infer-out-java
INFER_REPORT = $(JAVA_RESULTS_DIR)/report.json
MODELS_JAR = models.jar
JAVA_SOURCES = $(shell find $(JAVA_BUILTINS_DIR) $(JAVA_MODELS_DIR) -name "*.java")
MODELS_CLASSPATH = $(ANDROID_JAR):$(GUAVA_JAR):$(JACKSON_JAR):$(JSR_305_JAR):$(INFER_ANNOTATIONS_JAR)
.PHONY: all
all: $(MODELS_RESULTS_FILE)
.PHONY: clean_specs .PHONY: clean_specs
clean_specs: clean_specs:
$(REMOVE) $(SPECS_LIB_DIR)/*.specs $(MODELS_RESULTS_FILE) $(REMOVE) $(SPECS_LIB_DIR)/*.specs $(MODELS_RESULTS_FILE)
# clang models specs only for now clang:
# The clang deps have changed, so the models need to be rebuilt. If infer itself has changed, we $(QUIET)$(REMOVE_DIR) $(CLANG_RESULTS_DIR)
# need to nuke the previous specs files in case the serialization has changed, otherwise we might
# encounter a segfault reading them.
$(MODELS_RESULTS_FILE): $(MAKEFILE_LIST) $(CLANG_DEPS_NO_MODELS)
$(QUIET)$(MAKE) clean_specs
$(QUIET)$(REMOVE_DIR) $(MODELS_INFER_OUT)
# [make clean] each time to recompile all the models # [make clean] each time to recompile all the models
ifeq ($(BUILD_C_ANALYZERS),yes) ifeq ($(BUILD_C_ANALYZERS),yes)
$(QUIET)$(MAKE) -C $(C_MODELS_DIR) clean $(QUIET)$(MAKE) -C $(C_MODELS_DIR) clean
@ -37,38 +42,71 @@ ifeq (yes, $(HAS_OBJC))
$(QUIET)$(MAKE) -C $(OBJCPP_MODELS_DIR) clean $(QUIET)$(MAKE) -C $(OBJCPP_MODELS_DIR) clean
endif endif
$(QUIET)$(call silent_on_success,Capturing C models,\ $(QUIET)$(call silent_on_success,Capturing C models,\
$(INFER_BIN) capture $(MODELS_INFER_OPTIONS) --continue -- $(MAKE) -C $(C_MODELS_DIR) all) $(INFER_BIN) capture $(CLANG_INFER_OPTIONS) --continue -- $(MAKE) -C $(C_MODELS_DIR) all)
$(QUIET)$(call silent_on_success,Capturing C++ models,\ $(QUIET)$(call silent_on_success,Capturing C++ models,\
$(INFER_BIN) capture $(MODELS_INFER_OPTIONS) --continue -- $(MAKE) -C $(CPP_MODELS_DIR) all) $(INFER_BIN) capture $(CLANG_INFER_OPTIONS) --continue -- $(MAKE) -C $(CPP_MODELS_DIR) all)
ifeq (yes, $(HAS_OBJC)) ifeq (yes, $(HAS_OBJC))
$(QUIET)$(call silent_on_success,Capturing ObjCPP models,\ $(QUIET)$(call silent_on_success,Capturing ObjCPP models,\
$(INFER_BIN) capture $(MODELS_INFER_OPTIONS) --continue -- $(MAKE) -C $(OBJCPP_MODELS_DIR) all) $(INFER_BIN) capture $(CLANG_INFER_OPTIONS) --continue -- $(MAKE) -C $(OBJCPP_MODELS_DIR) all)
$(QUIET)$(call silent_on_success,Capturing ObjC models,\ $(QUIET)$(call silent_on_success,Capturing ObjC models,\
$(INFER_BIN) capture $(MODELS_INFER_OPTIONS) --continue -- $(MAKE) -C $(OBJC_MODELS_DIR) all) $(INFER_BIN) capture $(CLANG_INFER_OPTIONS) --continue -- $(MAKE) -C $(OBJC_MODELS_DIR) all)
endif endif
endif endif
$(QUIET)$(call silent_on_success,Analyzing clang models,\ $(QUIET)$(call silent_on_success,Analyzing clang models,\
$(INFER_BIN) analyze $(MODELS_INFER_OPTIONS)) $(INFER_BIN) analyze $(CLANG_INFER_OPTIONS))
$(QUIET)$(INSTALL_DATA) $(MODELS_INFER_OUT)/specs/*.specs $(SPECS_LIB_DIR) $(QUIET)$(INSTALL_DATA) $(CLANG_RESULTS_DIR)/specs/*.specs $(SPECS_LIB_DIR)
$(QUIET)touch $@
.PHONY: java .PHONY: java
java: java:
$(QUIET)$(MAKE) -C $@ install $(QUIET)rm -fr $(JAVA_MODELS_OUT)
$(QUIET)$(MKDIR_P) $(JAVA_MODELS_OUT)
$(QUIET)rm -f $(JAVA_MODELS_JAR)
$(QUIET)$(call silent_on_success,Building Java models,\
$(INFER_BIN) --biabduction-only --results-dir $(JAVA_RESULTS_DIR) --biabduction-models-mode -- \
$(JAVAC) -bootclasspath $(ANDROID_JAR) -d $(JAVA_MODELS_OUT) -classpath $(MODELS_CLASSPATH) \
$(JAVA_SOURCES) -source 7 -target 7)
cd $(JAVA_MODELS_OUT); jar cf ../../$(MODELS_JAR) *
# install .specs files into the models directory
$(QUIET)$(INSTALL_DATA) $(JAVA_RESULTS_DIR)/specs/*.specs $(SPECS_LIB_DIR)
# install the models.jar file too
$(INSTALL_DATA) -C $(MODELS_JAR) $(JAVA_MODELS_JAR)
$(QUIET)touch $(JAVA_MODELS_JAR)
ALL_MODELS=
ifeq ($(BUILD_C_ANALYZERS),yes) ifeq ($(BUILD_C_ANALYZERS),yes)
all: $(MODELS_RESULTS_FILE) ALL_MODELS += clang
endif
ifeq ($(BUILD_JAVA_ANALYZERS),yes)
ALL_MODELS += java
endif
# If the models deps have changed then 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.
$(MODELS_RESULTS_FILE): $(MAKEFILE_LIST)
# clean first
$(MAKE) clean_specs
# build java and clang models in parallel
$(MAKE) $(ALL_MODELS)
$(QUIET)touch $@
ifeq ($(BUILD_C_ANALYZERS),yes)
$(MODELS_RESULTS_FILE): $(CLANG_DEPS_NO_MODELS)
endif endif
ifeq ($(BUILD_JAVA_ANALYZERS),yes) ifeq ($(BUILD_JAVA_ANALYZERS),yes)
all: java $(MODELS_RESULTS_FILE): $(JAVA_DEPS_NO_MODELS) $(JAVA_SOURCES)
endif endif
.PHONY: clean .PHONY: clean
clean: clean_specs clean: clean_specs
$(QUIET)$(MAKE) -C $(JAVA_MODELS_DIR) clean
$(QUIET)$(MAKE) -C $(C_MODELS_DIR) clean $(QUIET)$(MAKE) -C $(C_MODELS_DIR) clean
$(QUIET)$(MAKE) -C $(CPP_MODELS_DIR) clean $(QUIET)$(MAKE) -C $(CPP_MODELS_DIR) clean
ifeq (yes, $(HAS_OBJC)) ifeq (yes, $(HAS_OBJC))
$(QUIET)$(MAKE) -C $(OBJC_MODELS_DIR) clean $(QUIET)$(MAKE) -C $(OBJC_MODELS_DIR) clean
$(QUIET)$(MAKE) -C $(OBJCPP_MODELS_DIR) clean $(QUIET)$(MAKE) -C $(OBJCPP_MODELS_DIR) clean
endif endif
$(QUIET)rm -rf $(CLANG_RESULTS_DIR) $(JAVA_RESULTS_DIR)
$(QUIET)rm -rf $(JAVA_MODELS_OUT)
$(QUIET)rm -f $(MODELS_JAR)
$(QUIET)rm -f $(JAVA_MODELS_JAR)

45
infer/models/java/Makefile
Unescape View File

@ -1,45 +0,0 @@
# Copyright (c) Facebook, Inc. and its affiliates.
#
# This source code is licensed under the MIT license found in the
# LICENSE file in the root directory of this source tree.
ROOT_DIR = ../../..
include $(ROOT_DIR)/Makefile.config
MODELS_OUT = models
INFER_RESULTS_DIR = $(MODELS_OUT)/infer
INFER_REPORT = $(INFER_RESULTS_DIR)/report.json
MODELS_JAR = models.jar
JAVA_SOURCES = $(shell find $(JAVA_BUILTINS_DIR) $(JAVA_MODELS_DIR) -name "*.java")
MODELS_CLASSPATH = $(ANDROID_JAR):$(GUAVA_JAR):$(JACKSON_JAR):$(JSR_305_JAR):$(INFER_ANNOTATIONS_JAR)
all: $(MODELS_JAR)
clean:
$(QUIET)rm -fr $(MODELS_OUT)
$(QUIET)rm -f $(MODELS_JAR)
$(QUIET)rm -f $(JAVA_MODELS_JAR)
compile:
$(JAVAC) -bootclasspath $(ANDROID_JAR) -d $(MODELS_OUT) -classpath $(MODELS_CLASSPATH) $(JAVA_SOURCES)
$(INFER_REPORT): $(JAVA_DEPS_NO_MODELS) $(JAVA_SOURCES) $(MAKEFILE_LIST)
$(QUIET)rm -fr $(MODELS_OUT)
$(QUIET)$(MKDIR_P) $(MODELS_OUT)
$(QUIET)rm -f $(JAVA_MODELS_JAR)
$(QUIET)$(call silent_on_success,Building Java models,\
$(INFER_BIN) --biabduction-only --results-dir $(INFER_RESULTS_DIR) --biabduction-models-mode -- \
$(JAVAC) -bootclasspath $(ANDROID_JAR) -d $(MODELS_OUT) -classpath $(MODELS_CLASSPATH) \
$(JAVA_SOURCES) -source 7 -target 7)
$(MODELS_JAR): $(INFER_REPORT)
cd $(MODELS_OUT); jar cf ../$(MODELS_JAR) *
$(JAVA_MODELS_JAR): $(MODELS_JAR)
$(INSTALL_DATA) -C $(MODELS_JAR) $(JAVA_MODELS_JAR)
install: $(JAVA_MODELS_JAR)
.PHONY: all clean install

2
infer/src/java/jFrontend.ml
Unescape View File

@ -141,7 +141,7 @@ let create_icfg source_file program tenv icfg cn node =
let translate m = let translate m =
let proc_name = JTransType.translate_method_name program tenv m in let proc_name = JTransType.translate_method_name program tenv m in
JClasspath.set_callee_translated program proc_name ; JClasspath.set_callee_translated program proc_name ;
if JModels.is_model proc_name then if BiabductionModels.mem proc_name then
(* do not translate the method if there is a model for it *) (* do not translate the method if there is a model for it *)
L.debug Capture Verbose "Skipping method with a model: %a@." Procname.pp proc_name L.debug Capture Verbose "Skipping method with a model: %a@." Procname.pp proc_name
else else

2
infer/src/java/jMain.ml
Unescape View File

@ -119,7 +119,7 @@ let main load_sources_and_classes =
| true, true -> | true, true ->
L.(die UserError) "Not expecting model file when analyzing the models" L.(die UserError) "Not expecting model file when analyzing the models"
| false, true -> | false, true ->
JModels.set_models ~jar_filename:Config.biabduction_models_jar ) ; JModels.load_models ~jar_filename:Config.biabduction_models_jar ) ;
JBasics.set_permissive true ; JBasics.set_permissive true ;
let JClasspath.{classpath; sources; classes} = let JClasspath.{classpath; sources; classes} =
match load_sources_and_classes with match load_sources_and_classes with

14
infer/src/java/jModels.ml
Unescape View File

@ -12,24 +12,14 @@ module L = Logging
let models_jar = ref None let models_jar = ref None
module StringHash = Caml.Hashtbl.Make (String)
let models_specs_filenames = StringHash.create 1
let models_classmap = ref JBasics.ClassMap.empty let models_classmap = ref JBasics.ClassMap.empty
let specs_file_extension = String.chop_prefix_exn ~prefix:"." Config.specs_files_suffix
let collect_specs_filenames jar_filename = let collect_specs_filenames jar_filename =
(* version of Javalib.get_class that does not spam stderr *) (* version of Javalib.get_class that does not spam stderr *)
let javalib_get_class = Utils.suppress_stderr2 Javalib.get_class in let javalib_get_class = Utils.suppress_stderr2 Javalib.get_class in
let classpath = Javalib.class_path jar_filename in let classpath = Javalib.class_path jar_filename in
let f classmap filename_with_extension = let f classmap filename_with_extension =
match Filename.split_extension filename_with_extension with match Filename.split_extension filename_with_extension with
| filename, Some extension when String.equal extension specs_file_extension ->
let proc_filename = Filename.basename filename in
StringHash.replace models_specs_filenames proc_filename () ;
classmap
| filename, Some extension when String.equal extension "class" -> ( | filename, Some extension when String.equal extension "class" -> (
let cn = JBasics.make_cn (String.map ~f:(function '/' -> '.' | c -> c) filename) in let cn = JBasics.make_cn (String.map ~f:(function '/' -> '.' | c -> c) filename) in
try JBasics.ClassMap.add cn (javalib_get_class classpath cn) classmap try JBasics.ClassMap.add cn (javalib_get_class classpath cn) classmap
@ -42,7 +32,7 @@ let collect_specs_filenames jar_filename =
Javalib.close_class_path classpath Javalib.close_class_path classpath
let set_models ~jar_filename = let load_models ~jar_filename =
match !models_jar with match !models_jar with
| None when match Sys.file_exists jar_filename with `Yes -> false | _ -> true -> | None when match Sys.file_exists jar_filename with `Yes -> false | _ -> true ->
L.die InternalError "Java model file not found@." L.die InternalError "Java model file not found@."
@ -56,6 +46,4 @@ let set_models ~jar_filename =
filename filename
let is_model procname = StringHash.mem models_specs_filenames (Procname.to_filename procname)
let get_classmap () = !models_classmap let get_classmap () = !models_classmap

5
infer/src/java/jModels.mli
Unescape View File

@ -9,11 +9,8 @@
open! IStd open! IStd
open Javalib_pack open Javalib_pack
val set_models : jar_filename:string -> unit val load_models : jar_filename:string -> unit
(** Sets the procnames in the given jar file as models *) (** Sets the procnames in the given jar file as models *)
val is_model : Procname.t -> bool
(** Check if there is a model for the given procname *)
val get_classmap : unit -> JCode.jcode Javalib.interface_or_class JBasics.ClassMap.t val get_classmap : unit -> JCode.jcode Javalib.interface_or_class JBasics.ClassMap.t
(** get map of model classes *) (** get map of model classes *)

2
infer/src/java/jTrans.ml
Unescape View File

@ -718,7 +718,7 @@ let method_invocation (context : JContext.t) loc pc var_opt cn ms sil_obj_opt ex
let instrs = let instrs =
match call_args with match call_args with
(* modeling a class bypasses the treatment of Closeable *) (* modeling a class bypasses the treatment of Closeable *)
| _ when Config.biabduction_models_mode || JModels.is_model callee_procname -> | _ when Config.biabduction_models_mode || BiabductionModels.mem callee_procname ->
call_instrs call_instrs
| ((_, {Typ.desc= Typ.Tptr ({desc= Tstruct typename}, _)}) as exp) :: _ | ((_, {Typ.desc= Typ.Tptr ({desc= Tstruct typename}, _)}) as exp) :: _
(* add a file attribute when calling the constructor of a subtype of Closeable *) (* add a file attribute when calling the constructor of a subtype of Closeable *)

Write Preview
Loading…
Cancel
Save