diff --git a/.gitignore b/.gitignore index a865a417d..9c31b154a 100644 --- a/.gitignore +++ b/.gitignore @@ -163,6 +163,7 @@ infer/src/.project /infer/dune-workspace /infer/src/dune.common /infer/src/dune +/infer/src/java/dune /infer/src/opensource/dune .merlin diff --git a/infer/src/Makefile b/infer/src/Makefile index a867c8a65..938761e30 100644 --- a/infer/src/Makefile +++ b/infer/src/Makefile @@ -76,7 +76,7 @@ GENERATED_FROM_AUTOCONF = dune.common ../dune-workspace base/Version.ml .PHONY: dune-workspace dune-workspace: ../dune-workspace -GENERATED_DUNES += dune opensource/dune +GENERATED_DUNES += dune java/dune opensource/dune SRC_BUILD_COMMON = $(GENERATED_FROM_AUTOCONF) $(GENERATED_DUNES) $(OCAML_SOURCES) ifeq ($(BUILD_C_ANALYZERS),yes) @@ -153,7 +153,7 @@ roots:=Infer ifeq ($(IS_FACEBOOK_TREE),yes) roots += $(INFER_CREATE_TRACEVIEW_LINKS_MODULE) endif -clusters:=absint al atd backend base biabduction bufferoverrun checkers clang clang_stubs concurrency cost c_stubs deadcode integration IR istd java java_stubs labs llvm nullsafe opensource pulse quandary scripts test_determinator third-party topl unit +clusters:=absint al atd backend base biabduction bufferoverrun checkers clang clang_stubs concurrency cost c_stubs deadcode integration IR istd java labs llvm nullsafe opensource pulse quandary scripts test_determinator third-party topl unit ml_src_files:=$(shell find . -not -path "./*stubs*" -regex '\./[a-zA-Z].*\.ml\(i\)*') inc_flags:=$(foreach dir,$(shell find . -not -path './_build*' -type d),-I $(dir)) @@ -243,6 +243,7 @@ $(GENERATED_DUNES): dune.common dune: dune.in deadcode/dune: deadcode/dune.in +java/dune: java/dune.in opensource/dune: opensource/dune.in .PHONY: clean diff --git a/infer/src/absint/SubtypingCheck.ml b/infer/src/absint/SubtypingCheck.ml new file mode 100644 index 000000000..399449e74 --- /dev/null +++ b/infer/src/absint/SubtypingCheck.ml @@ -0,0 +1,115 @@ +(* + * Copyright (c) 2009-2013, Monoidics ltd. + * 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. + *) + +open! IStd + +let rec is_java_class tenv (typ : Typ.t) = + match typ.desc with + | Tstruct name -> + Typ.Name.Java.is_class name + | Tarray {elt= inner_typ} | Tptr (inner_typ, _) -> + is_java_class tenv inner_typ + | _ -> + false + + +(** check that t1 and t2 are the same primitive type *) +let check_subtype_basic_type t1 t2 = + match t2.Typ.desc with + | Typ.Tint Typ.IInt + | Typ.Tint Typ.IBool + | Typ.Tint Typ.IChar + | Typ.Tfloat Typ.FDouble + | Typ.Tfloat Typ.FFloat + | Typ.Tint Typ.ILong + | Typ.Tint Typ.IShort -> + Typ.equal t1 t2 + | _ -> + false + + +(** check if t1 is a subtype of t2, in Java *) +let rec check_subtype_java tenv (t1 : Typ.t) (t2 : Typ.t) = + match (t1.Typ.desc, t2.Typ.desc) with + | Tstruct (JavaClass _ as cn1), Tstruct (JavaClass _ as cn2) -> + Subtype.is_known_subtype tenv cn1 cn2 + | Tarray {elt= dom_type1}, Tarray {elt= dom_type2} -> + check_subtype_java tenv dom_type1 dom_type2 + | Tptr (dom_type1, _), Tptr (dom_type2, _) -> + check_subtype_java tenv dom_type1 dom_type2 + | Tarray _, Tstruct (JavaClass _ as cn2) -> + Typ.Name.equal cn2 Typ.Name.Java.java_io_serializable + || Typ.Name.equal cn2 Typ.Name.Java.java_lang_cloneable + || Typ.Name.equal cn2 Typ.Name.Java.java_lang_object + | _ -> + check_subtype_basic_type t1 t2 + + +(** check if t1 is a subtype of t2 *) +let check_subtype tenv t1 t2 = + if is_java_class tenv t1 then check_subtype_java tenv t1 t2 + else + match (Typ.name t1, Typ.name t2) with + | Some cn1, Some cn2 -> + Subtype.is_known_subtype tenv cn1 cn2 + | _ -> + false + + +let rec case_analysis_type tenv ((t1 : Typ.t), st1) ((t2 : Typ.t), st2) = + match (t1.desc, t2.desc) with + | Tstruct (JavaClass _ as cn1), Tstruct (JavaClass _ as cn2) -> + Subtype.case_analysis tenv (cn1, st1) (cn2, st2) + | Tstruct (JavaClass _ as cn1), Tarray _ + when ( Typ.Name.equal cn1 Typ.Name.Java.java_io_serializable + || Typ.Name.equal cn1 Typ.Name.Java.java_lang_cloneable + || Typ.Name.equal cn1 Typ.Name.Java.java_lang_object ) + && not (Subtype.equal st1 Subtype.exact) -> + (Some st1, None) + | Tstruct cn1, Tstruct cn2 + (* cn1 <: cn2 or cn2 <: cn1 is implied in Java when we get two types compared *) + (* that get through the type system, but not in C++ because of multiple inheritance, *) + (* and not in ObjC because of being weakly typed, *) + (* and the algorithm will only work correctly if this is the case *) + when Subtype.is_known_subtype tenv cn1 cn2 || Subtype.is_known_subtype tenv cn2 cn1 -> + Subtype.case_analysis tenv (cn1, st1) (cn2, st2) + | Tarray {elt= dom_type1}, Tarray {elt= dom_type2} -> + case_analysis_type tenv (dom_type1, st1) (dom_type2, st2) + | Tptr (dom_type1, _), Tptr (dom_type2, _) -> + case_analysis_type tenv (dom_type1, st1) (dom_type2, st2) + | _ when check_subtype_basic_type t1 t2 -> + (Some st1, None) + | _ -> + (* The case analysis did not succeed *) + (None, Some st1) + + +(** perform case analysis on [texp1 <: texp2], and return the updated types in the true and false + case, if they are possible *) +let subtype_case_analysis tenv texp1 texp2 = + match (texp1, texp2) with + | Exp.Sizeof sizeof1, Exp.Sizeof sizeof2 -> + let pos_opt, neg_opt = + case_analysis_type tenv (sizeof1.typ, sizeof1.subtype) (sizeof2.typ, sizeof2.subtype) + in + let pos_type_opt = + match pos_opt with + | None -> + None + | Some subtype -> + if check_subtype tenv sizeof1.typ sizeof2.typ then + Some (Exp.Sizeof {sizeof1 with subtype}) + else Some (Exp.Sizeof {sizeof2 with subtype}) + in + let neg_type_opt = + match neg_opt with None -> None | Some subtype -> Some (Exp.Sizeof {sizeof1 with subtype}) + in + (pos_type_opt, neg_type_opt) + | _ -> + (* don't know, consider both possibilities *) + (Some texp1, Some texp1) diff --git a/infer/src/absint/SubtypingCheck.mli b/infer/src/absint/SubtypingCheck.mli new file mode 100644 index 000000000..4a03df5ca --- /dev/null +++ b/infer/src/absint/SubtypingCheck.mli @@ -0,0 +1,18 @@ +(* + * Copyright (c) 2009-2013, Monoidics ltd. + * 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. + *) + +open! IStd + +(** {2 Subtype checking} *) + +val check_subtype : Tenv.t -> Typ.t -> Typ.t -> bool +(** check_subtype t1 t2 checks whether t1 is a subtype of t2, given the type environment tenv. *) + +val subtype_case_analysis : Tenv.t -> Exp.t -> Exp.t -> Exp.t option * Exp.t option +(** subtype_case_analysis tenv tecp1 texp2 performs case analysis on [texp1 <: texp2], and returns + the updated types in the true and false case, if they are possible *) diff --git a/infer/src/biabduction/BuiltinDefn.ml b/infer/src/biabduction/BuiltinDefn.ml index 3c5f683aa..5513e58e5 100644 --- a/infer/src/biabduction/BuiltinDefn.ml +++ b/infer/src/biabduction/BuiltinDefn.ml @@ -282,7 +282,7 @@ let execute___instanceof_cast ~instof |> Option.map ~f:(function | Predicates.Hpointsto (_, _, texp1) -> ( let pos_type_opt, neg_type_opt = - Prover.Subtyping_check.subtype_case_analysis tenv texp1 texp2 + SubtypingCheck.subtype_case_analysis tenv texp1 texp2 in let mk_res type_opt res_e = match type_opt with diff --git a/infer/src/biabduction/Prover.ml b/infer/src/biabduction/Prover.ml index eab2a70cd..22f1a70af 100644 --- a/infer/src/biabduction/Prover.ml +++ b/infer/src/biabduction/Prover.ml @@ -1792,114 +1792,12 @@ let expand_hpred_pointer = expand false calc_index_frame hpred -module Subtyping_check = struct - (** check that t1 and t2 are the same primitive type *) - let check_subtype_basic_type t1 t2 = - match t2.Typ.desc with - | Typ.Tint Typ.IInt - | Typ.Tint Typ.IBool - | Typ.Tint Typ.IChar - | Typ.Tfloat Typ.FDouble - | Typ.Tfloat Typ.FFloat - | Typ.Tint Typ.ILong - | Typ.Tint Typ.IShort -> - Typ.equal t1 t2 - | _ -> - false - - - (** check if t1 is a subtype of t2, in Java *) - let rec check_subtype_java tenv (t1 : Typ.t) (t2 : Typ.t) = - match (t1.Typ.desc, t2.Typ.desc) with - | Tstruct (JavaClass _ as cn1), Tstruct (JavaClass _ as cn2) -> - Subtype.is_known_subtype tenv cn1 cn2 - | Tarray {elt= dom_type1}, Tarray {elt= dom_type2} -> - check_subtype_java tenv dom_type1 dom_type2 - | Tptr (dom_type1, _), Tptr (dom_type2, _) -> - check_subtype_java tenv dom_type1 dom_type2 - | Tarray _, Tstruct (JavaClass _ as cn2) -> - Typ.Name.equal cn2 Typ.Name.Java.java_io_serializable - || Typ.Name.equal cn2 Typ.Name.Java.java_lang_cloneable - || Typ.Name.equal cn2 Typ.Name.Java.java_lang_object - | _ -> - check_subtype_basic_type t1 t2 - - - (** check if t1 is a subtype of t2 *) - let check_subtype tenv t1 t2 = - if is_java_class tenv t1 then check_subtype_java tenv t1 t2 - else - match (Typ.name t1, Typ.name t2) with - | Some cn1, Some cn2 -> - Subtype.is_known_subtype tenv cn1 cn2 - | _ -> - false - - - let rec case_analysis_type tenv ((t1 : Typ.t), st1) ((t2 : Typ.t), st2) = - match (t1.desc, t2.desc) with - | Tstruct (JavaClass _ as cn1), Tstruct (JavaClass _ as cn2) -> - Subtype.case_analysis tenv (cn1, st1) (cn2, st2) - | Tstruct (JavaClass _ as cn1), Tarray _ - when ( Typ.Name.equal cn1 Typ.Name.Java.java_io_serializable - || Typ.Name.equal cn1 Typ.Name.Java.java_lang_cloneable - || Typ.Name.equal cn1 Typ.Name.Java.java_lang_object ) - && not (Subtype.equal st1 Subtype.exact) -> - (Some st1, None) - | Tstruct cn1, Tstruct cn2 - (* cn1 <: cn2 or cn2 <: cn1 is implied in Java when we get two types compared *) - (* that get through the type system, but not in C++ because of multiple inheritance, *) - (* and not in ObjC because of being weakly typed, *) - (* and the algorithm will only work correctly if this is the case *) - when Subtype.is_known_subtype tenv cn1 cn2 || Subtype.is_known_subtype tenv cn2 cn1 -> - Subtype.case_analysis tenv (cn1, st1) (cn2, st2) - | Tarray {elt= dom_type1}, Tarray {elt= dom_type2} -> - case_analysis_type tenv (dom_type1, st1) (dom_type2, st2) - | Tptr (dom_type1, _), Tptr (dom_type2, _) -> - case_analysis_type tenv (dom_type1, st1) (dom_type2, st2) - | _ when check_subtype_basic_type t1 t2 -> - (Some st1, None) - | _ -> - (* The case analysis did not succeed *) - (None, Some st1) - - - (** perform case analysis on [texp1 <: texp2], and return the updated types in the true and false - case, if they are possible *) - let subtype_case_analysis tenv texp1 texp2 = - match (texp1, texp2) with - | Exp.Sizeof sizeof1, Exp.Sizeof sizeof2 -> - let pos_opt, neg_opt = - case_analysis_type tenv (sizeof1.typ, sizeof1.subtype) (sizeof2.typ, sizeof2.subtype) - in - let pos_type_opt = - match pos_opt with - | None -> - None - | Some subtype -> - if check_subtype tenv sizeof1.typ sizeof2.typ then - Some (Exp.Sizeof {sizeof1 with subtype}) - else Some (Exp.Sizeof {sizeof2 with subtype}) - in - let neg_type_opt = - match neg_opt with - | None -> - None - | Some subtype -> - Some (Exp.Sizeof {sizeof1 with subtype}) - in - (pos_type_opt, neg_type_opt) - | _ -> - (* don't know, consider both possibilities *) - (Some texp1, Some texp1) -end - let cast_exception tenv texp1 texp2 e1 subs = ( match (texp1, texp2) with | Exp.Sizeof {typ= t1}, Exp.Sizeof {typ= t2; subtype= st2} -> if Config.developer_mode - || (Subtype.is_cast st2 && not (Subtyping_check.check_subtype tenv t1 t2)) + || (Subtype.is_cast st2 && not (SubtypingCheck.check_subtype tenv t1 t2)) then ProverState.checks := Class_cast_check (texp1, texp2, e1) :: !ProverState.checks | _ -> () ) ; @@ -1935,7 +1833,7 @@ let texp_imply tenv subs texp1 texp2 e1 calc_missing = false in if types_subject_to_dynamic_cast then - let pos_type_opt, neg_type_opt = Subtyping_check.subtype_case_analysis tenv texp1 texp2 in + let pos_type_opt, neg_type_opt = SubtypingCheck.subtype_case_analysis tenv texp1 texp2 in let has_changed = match pos_type_opt with | Some texp1' -> @@ -2008,9 +1906,9 @@ let handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2 when not (is_allocated_lhs e1') -> ( match type_rhs e2' with | Some sizeof_data2 -> ( - if (not (Typ.equal t1 t2)) && Subtyping_check.check_subtype tenv t1 t2 then + if (not (Typ.equal t1 t2)) && SubtypingCheck.check_subtype tenv t1 t2 then let pos_type_opt, _ = - Subtyping_check.subtype_case_analysis tenv + SubtypingCheck.subtype_case_analysis tenv (Exp.Sizeof {typ= t1; nbytes= None; dynamic_length= None; subtype= Subtype.subtypes}) (Exp.Sizeof sizeof_data2) in diff --git a/infer/src/biabduction/Prover.mli b/infer/src/biabduction/Prover.mli index 7ab6db7d1..07a132ad1 100644 --- a/infer/src/biabduction/Prover.mli +++ b/infer/src/biabduction/Prover.mli @@ -97,14 +97,3 @@ val check_implication_for_footprint : val find_minimum_pure_cover : Tenv.t -> (atom list * 'a) list -> (atom list * 'a) list option (** Find minimum set of pi's in [cases] whose disjunction covers true *) - -(** {2 Subtype checking} *) - -module Subtyping_check : sig - val check_subtype : Tenv.t -> Typ.t -> Typ.t -> bool - (** check_subtype t1 t2 checks whether t1 is a subtype of t2, given the type environment tenv. *) - - val subtype_case_analysis : Tenv.t -> Exp.t -> Exp.t -> Exp.t option * Exp.t option - (** subtype_case_analysis tenv tecp1 texp2 performs case analysis on [texp1 <: texp2], and returns - the updated types in the true and false case, if they are possible *) -end diff --git a/infer/src/deadcode/Makefile b/infer/src/deadcode/Makefile index dd3d79aa5..594217e77 100644 --- a/infer/src/deadcode/Makefile +++ b/infer/src/deadcode/Makefile @@ -50,8 +50,8 @@ endif # Note that we run find under _build directory. Since we copy some # sources from subfolders to src/ folder to avoid duplicates we use # $(DEPTH_ONE) and iteration over main and library folders. -LIBRARY_FOLDERS = . ./IR ./absint ./atd ./backend ./base ./biabduction ./bufferoverrun ./c_stubs ./checkers ./concurrency ./cost ./istd ./labs ./nullsafe ./pulse ./quandary ./scripts ./topl -INCLUDE_FOLDERS = -I absint -I IR -I atd -I backend -I base -I biabduction -I bufferoverrun -I c_stubs -I checkers -I concurrency -I cost -I istd -I labs -I nullsafe -I pulse -I quandary -I scripts -I topl +LIBRARY_FOLDERS = . ./IR ./absint ./atd ./backend ./base ./biabduction ./bufferoverrun ./c_stubs ./checkers ./concurrency ./cost ./istd ./java ./labs ./nullsafe ./pulse ./quandary ./scripts ./topl +INCLUDE_FOLDERS = -I absint -I IR -I atd -I backend -I base -I biabduction -I bufferoverrun -I c_stubs -I checkers -I concurrency -I cost -I istd -I java -I labs -I nullsafe -I pulse -I quandary -I scripts -I topl ml_src_files:=$(shell \ cd $(INFER_BUILD_DIR); \ @@ -191,12 +191,13 @@ detect_dead_code: .PHONY: detect_dead_src_file detect_dead_src_file: function is_in_blacklist { \ - if [ "$$1" = "infertop.ml" ] \ - || [ "$$1" = "deadcode/all_infer_in_one_file.ml" ] \ - || [ "$$1" = "deadcode/all_infer_in_one_file.mli" ] \ - || [[ "$$1" =~ ^"labs/" ]] \ - || [[ "$$1" =~ ^"llvm/" ]] \ - || [[ "$$1" =~ ^"opensource/" ]]; then \ + if [ $$1 = infertop.ml ] \ + || [ $$1 = deadcode/all_infer_in_one_file.ml ] \ + || [ $$1 = deadcode/all_infer_in_one_file.mli ] \ + || [[ $$1 =~ .*FrontendStubs.mli?$$ ]] \ + || [[ $$1 =~ ^labs/ ]] \ + || [[ $$1 =~ ^llvm/ ]] \ + || [[ $$1 =~ ^opensource/ ]]; then \ exit 0; \ else \ exit 1; \ diff --git a/infer/src/dune.in b/infer/src/dune.in index 9e41ea54e..25948ea28 100644 --- a/infer/src/dune.in +++ b/infer/src/dune.in @@ -11,11 +11,7 @@ let ( ^/ ) = Filename.concat let source_dirs = (if clang then ["al"; "clang"; "unit" ^/ "clang"] else ["clang_stubs"; "unit" ^/ "clang_stubs"]) - @ [ (if java then "java" else "java_stubs") - ; "integration" - ; "test_determinator" - ; "unit" - ; "unit" ^/ "nullsafe" ] + @ ["integration"; "test_determinator"; "unit"; "unit" ^/ "nullsafe"] let infer_binaries = ["infer"; "inferunit"] @ if facebook then ["InferCreateTraceViewLinks"] else [] @@ -42,46 +38,49 @@ let clang_lexer_stanzas = let infer_cflags = - [ "-open" - ; "Core" - ; "-open" - ; "Biabduction" - ; "-open" - ; "Bo" - ; "-open" - ; "Nullsafe" - ; "-open" - ; "Pulselib" - ; "-open" - ; "Checkers" - ; "-open" - ; "Costlib" - ; "-open" - ; "Quandary" - ; "-open" - ; "TOPLlib" - ; "-open" - ; "Concurrency" - ; "-open" - ; "Labs" - ; "-open" - ; "Absint" - ; "-open" - ; "OpenSource" - ; "-open" - ; "InferStdlib" - ; "-open" - ; "IStd" - ; "-open" - ; "InferGenerated" - ; "-open" - ; "InferIR" - ; "-open" - ; "InferBase" - ; "-open" - ; "InferCStubs" - ; "-open" - ; "Backend" ] + ( [ "-open" + ; "Core" + ; "-open" + ; "Biabduction" + ; "-open" + ; "Bo" + ; "-open" + ; "Nullsafe" + ; "-open" + ; "Pulselib" + ; "-open" + ; "Checkers" + ; "-open" + ; "Costlib" + ; "-open" + ; "Quandary" + ; "-open" + ; "TOPLlib" + ; "-open" + ; "Concurrency" + ; "-open" + ; "Labs" + ; "-open" + ; "Absint" + ; "-open" + ; "OpenSource" + ; "-open" + ; "InferStdlib" + ; "-open" + ; "IStd" + ; "-open" + ; "InferGenerated" + ; "-open" + ; "InferIR" + ; "-open" + ; "InferBase" + ; "-open" + ; "InferCStubs" + ; "-open" + ; "Backend" + ; "-open" + ; "JavaFrontend" ] + @ if java then [] else ["-open"; "JavaFrontendStubs"] ) |> String.concat " " @@ -99,7 +98,8 @@ let main_lib_stanza = |} infer_cflags (String.concat " " - ( common_libraries + (* we need JavaFrontend first to avoid clashes around base64 vs extlib *) + ( ("JavaFrontend" :: common_libraries) @ [ "InferIR" ; "InferCStubs" ; "absint" @@ -123,7 +123,7 @@ let infer_exe_stanza = (executables (names %s) (modes byte_complete exe) - (flags (:standard %s -open InferModules)) + (flags (:standard -open InferModules %s)) (libraries InferModules) (modules %s) (preprocess (pps ppx_compare ppx_fields_conv ppx_hash ppx_sexp_conv ppx_variants_conv -no-check)) @@ -152,8 +152,6 @@ let infertop_stanza = infer_cflags -let java_sources_lexer = if java then ["(ocamllex jSourceFileInfo)"] else [] - let flatten_sources_stanzas = List.map (fun source_dir -> @@ -168,7 +166,7 @@ let flatten_sources_stanzas = (** The build stanzas to be passed to dune *) let stanzas = (env_stanza :: main_lib_stanza :: infer_exe_stanza :: infertop_stanza :: clang_lexer_stanzas) - @ java_sources_lexer @ flatten_sources_stanzas + @ flatten_sources_stanzas ;; diff --git a/infer/src/java_stubs/jMain.ml b/infer/src/java/JavaFrontendStubs.ml similarity index 70% rename from infer/src/java_stubs/jMain.ml rename to infer/src/java/JavaFrontendStubs.ml index 0c22616fb..f265f2bdc 100644 --- a/infer/src/java_stubs/jMain.ml +++ b/infer/src/java/JavaFrontendStubs.ml @@ -7,6 +7,8 @@ open! IStd -let from_arguments _ = () +module JMain = struct + let from_arguments _ = () -let from_verbose_out _ = () + let from_verbose_out _ = () +end diff --git a/infer/src/java/JavaFrontendStubs.mli b/infer/src/java/JavaFrontendStubs.mli new file mode 100644 index 000000000..c650460f9 --- /dev/null +++ b/infer/src/java/JavaFrontendStubs.mli @@ -0,0 +1,22 @@ +(* + * Copyright (c) 2009-2013, Monoidics ltd. + * 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. + *) + +open! IStd + +(** ****DO NOT USE DIRECTLY**** + + This module is automatically [open]'d by the build system when compiling infer without Java + support. The stubs implemented here do nothing. *) + +module JMain : sig + val from_arguments : string -> unit + (** loads the source files from command line arguments and translates them *) + + val from_verbose_out : string -> unit + (** loads the source files from javac's verbose output translates them *) +end diff --git a/infer/src/java/dune.in b/infer/src/java/dune.in new file mode 100644 index 000000000..83514b46f --- /dev/null +++ b/infer/src/java/dune.in @@ -0,0 +1,31 @@ +(* -*- tuareg -*- *) +(* + * 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. + *) +(* NOTE: prepend dune.common to this file! *) + +let lexer = "(ocamllex jSourceFileInfo)" + +let java = + Printf.sprintf + {|(library + (name JavaFrontend) + (public_name infer.JavaFrontend) + (modules %s) + (flags + (:standard + -open Core -open InferStdlib -open IStd -open OpenSource -open InferGenerated + -open InferBase -open InferIR -open Absint)) + (libraries %s core InferStdlib InferGenerated InferBase InferIR absint) + (preprocess (pps ppx_compare)) +)|} + (if java then ":standard \\ JavaFrontendStubs" else "JavaFrontendStubs") + (* do not add dependencies on javalib and sawja to the non-Java builds *) + (if java then "javalib sawja" else "") + + +;; +Jbuild_plugin.V1.send (String.concat " " [lexer; java]) diff --git a/infer/src/java/jContext.ml b/infer/src/java/jContext.ml index 6d3d29b73..cfefb7b3f 100644 --- a/infer/src/java/jContext.ml +++ b/infer/src/java/jContext.ml @@ -49,10 +49,8 @@ let get_or_set_pvar_type context var typ = try let pvar, otyp, _ = JBir.VarMap.find var var_map in let tenv = get_tenv context in - if - Prover.Subtyping_check.check_subtype tenv typ otyp - || Prover.Subtyping_check.check_subtype tenv otyp typ - then set_var_map context (JBir.VarMap.add var (pvar, otyp, typ) var_map) + if SubtypingCheck.check_subtype tenv typ otyp || SubtypingCheck.check_subtype tenv otyp typ then + set_var_map context (JBir.VarMap.add var (pvar, otyp, typ) var_map) else set_var_map context (JBir.VarMap.add var (pvar, typ, typ) var_map) ; (pvar, typ) with Caml.Not_found -> diff --git a/infer/src/java_stubs/jMain.mli b/infer/src/java_stubs/jMain.mli deleted file mode 120000 index a94f776cf..000000000 --- a/infer/src/java_stubs/jMain.mli +++ /dev/null @@ -1 +0,0 @@ -../java/jMain.mli \ No newline at end of file