[models] avoid race conditions when building and installing the models

Summary:
Saw these two types of errors before (but they're hard to reproduce locally) when building the models:

- `ERROR: Zip.Error("/mnt/btrfs/trunk-git-infer-739-1503054473/infer/bin/../lib/java/models.jar", "", "end of central directory not found, not a ZIP file")`. I think this means infer reads a partially-written models jar. We shouldn't try to load this in models mode.
- `install` would complain that the destination already exists. I think this can only happen if there's a race and the file gets created between when install first checks and when it tries to write to it.

This made me realise that the some of the models are computed in C and C++ mode
and we pick one computed spec arbitrarily. That sounds a bit dodgy but at least
now we do so in a non-racy way.

Reviewed By: jeremydubreil

Differential Revision: D5658389

fbshipit-source-id: 8077279
master
Jules Villard 7 years ago committed by Facebook Github Bot
parent 30d2822846
commit a34fcebc59

@ -34,7 +34,7 @@ clean_specs:
$(REMOVE) $(SPECS_LIB_DIR)/*.specs $(C_MODELS_FILE) $(CPP_MODELS_FILE) $(OBJC_MODELS_FILE) $(REMOVE) $(SPECS_LIB_DIR)/*.specs $(C_MODELS_FILE) $(CPP_MODELS_FILE) $(OBJC_MODELS_FILE)
$(CLANG_SUBDIRS): $(CLANG_SUBDIRS):
$(QUIET)$(MAKE) -C $@ install $(QUIET)$(MAKE) -C $@ out/report.json
# The clang deps have changed, so the models need to be rebuilt. If infer itself has changed, we # 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 # need to nuke the previous specs files in case the serialization has changed, otherwise we might
@ -44,6 +44,9 @@ $(CLANG_MODELS_FILE): $(CLANG_DEPS_NO_MODELS)
# Since [CLANG_DEPS_NO_MODELS] is newer than [CLANG_MODELS_FILE], it is also newer than the # 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. # previously built clang models, so they will all be rebuilt by the subdirs' Makefiles.
$(QUIET)$(MAKE) $(CLANG_SUBDIRS) $(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. # Maintain the invariant that [CLANG_MODELS_FILE] is newer than the clang models.
$(QUIET)touch $@ $(QUIET)touch $@

@ -32,7 +32,7 @@ $(INFER_REPORT): $(JAVA_DEPS_NO_MODELS) $(JAVA_SOURCES)
$(QUIET)$(MKDIR_P) $(MODELS_OUT) $(QUIET)$(MKDIR_P) $(MODELS_OUT)
$(QUIET)rm -f $(JAVA_MODELS_JAR) $(QUIET)rm -f $(JAVA_MODELS_JAR)
$(QUIET)$(call silent_on_success,Building Java models,\ $(QUIET)$(call silent_on_success,Building Java models,\
$(INFER_BIN) --jobs 1 --results-dir $(INFER_RESULTS_DIR) --models-mode -- \ $(INFER_BIN) --results-dir $(INFER_RESULTS_DIR) --models-mode -- \
$(JAVAC) -bootclasspath $(ANDROID_JAR) -d $(MODELS_OUT) -classpath $(MODELS_CLASSPATH) \ $(JAVAC) -bootclasspath $(ANDROID_JAR) -d $(MODELS_OUT) -classpath $(MODELS_CLASSPATH) \
$(JAVA_SOURCES)) $(JAVA_SOURCES))

@ -78,7 +78,7 @@ let zip_libraries =
in in
List.fold ~f:add_zip ~init:[] Config.specs_library List.fold ~f:add_zip ~init:[] Config.specs_library
in in
if Config.biabduction && Sys.file_exists Config.models_jar = `Yes then if Config.biabduction && not Config.models_mode && Sys.file_exists Config.models_jar = `Yes then
mk_zip_lib true Config.models_jar :: zip_libs mk_zip_lib true Config.models_jar :: zip_libs
else zip_libs) ) else zip_libs) )

Loading…
Cancel
Save