diff --git a/Makefile b/Makefile index 5c6a086a1..8fb8f5247 100644 --- a/Makefile +++ b/Makefile @@ -629,7 +629,7 @@ opam.lock: opam # This is a magical version number that doesn't reinstall the world when added on top of what we # have in opam.lock. To upgrade this version number, manually try to install several utop versions # until you find one that doesn't recompile the world. TODO(t20828442): get rid of magic -OPAM_DEV_DEPS = ocamlformat.$$(grep version .ocamlformat | cut -d ' ' -f 2) ocp-indent merlin utop.2.1.0 +OPAM_DEV_DEPS = ocamlformat.$$(grep version .ocamlformat | cut -d ' ' -f 2) ocp-indent merlin utop.2.1.0 webbrowser ifneq ($(EMACS),no) OPAM_DEV_DEPS += tuareg @@ -706,6 +706,18 @@ devsetup: Makefile.autoconf echo '$(TERM_INFO) eval $$(opam config env)$(TERM_RESET)' >&2; \ fi +.PHONY: doc +doc: src_build_common + $(QUIET)$(call silent_on_success,Generating infer documentation,\ + $(MAKE_SOURCE) doc) + $(QUIET)$(call silent_on_success,Opening in browser,\ + browse $(SRC_DIR)/_build/$(BUILD_MODE)/_doc/_html/index.html) + $(QUIET)echo "Tip: you can generate the doc for all the opam dependencies of infer like this:" + $(QUIET)echo + $(QUIET)echo " odig odoc # takes a while, run it only when the dependencies change" + $(QUIET)echo " odig doc" + + # print list of targets .PHONY: show-targets show-targets: diff --git a/infer/src/IR/README.md b/infer/src/IR/README.md deleted file mode 100644 index 6a28bfcff..000000000 --- a/infer/src/IR/README.md +++ /dev/null @@ -1,12 +0,0 @@ -# Intermediate Representation - -The Intermediate Representation is a format used by the back-end for analysis. It is produced by one of the front-ends, one for each program analyzed. - -The main entry point is the intermediate language in [Sil](Sil.mli). - -The control flow graph module is [Cfg](Cfg.mli). - -The call graph module is [Cg](Cg.mli). - -The type environment module is [Tenv](Tenv.mli). - diff --git a/infer/src/IR/index.mld b/infer/src/IR/index.mld new file mode 100644 index 000000000..5f0ddb421 --- /dev/null +++ b/infer/src/IR/index.mld @@ -0,0 +1,11 @@ +{1 Library InferIR: Intermediate Representation} +The Intermediate Representation, called [SIL], is a format used by the back-end for analysis. It is produced by the front-ends. + +The entry point of this library is the module: +{!module-InferIR}. + +The main entry point is the intermediate language in {!module-InferIR.Sil}. + +The control flow graph module is {!module-InferIR.Cfg}. + +The type environment module is {!module-InferIR.Tenv}. diff --git a/infer/src/IR/jbuild.in b/infer/src/IR/jbuild.in index c839e2ae7..b231add18 100644 --- a/infer/src/IR/jbuild.in +++ b/infer/src/IR/jbuild.in @@ -4,11 +4,17 @@ {| (library ((name InferIR) + (public_name InferIR) (flags (%s -open Core -open InferStdlib -open IStd -open InferGenerated -open InferBase)) (ocamlopt_flags (%s)) (libraries (%s)) (preprocess (pps (ppx_compare))) )) + +(documentation + ((package InferIR) + (mld_files (index)) + )) |} (String.concat " " common_cflags) (String.concat " " common_optflags) diff --git a/infer/src/InferBase.opam b/infer/src/InferBase.opam new file mode 100644 index 000000000..e69de29bb diff --git a/infer/src/InferGenerated.opam b/infer/src/InferGenerated.opam new file mode 100644 index 000000000..e69de29bb diff --git a/infer/src/InferIR.opam b/infer/src/InferIR.opam new file mode 100644 index 000000000..e69de29bb diff --git a/infer/src/InferStdlib.opam b/infer/src/InferStdlib.opam new file mode 100644 index 000000000..e69de29bb diff --git a/infer/src/Makefile b/infer/src/Makefile index 70fe2226c..5b19d5e80 100644 --- a/infer/src/Makefile +++ b/infer/src/Makefile @@ -116,6 +116,10 @@ test: $(SRC_BUILD_COMMON) $(MAKEFILE_LIST) $(patsubst $(INFER_BUILD_DIR)/%.exe,_build/test/%.bc,$(INFER_CONFIG_TARGETS)) \ _build/test/scripts/checkCopyright.bc _build/test/$(INFERUNIT_MAIN).bc _build/test/infertop.bc +.PHONY: doc +doc: $(SRC_BUILD_COMMON) $(MAKEFILE_LIST) + $(QUIET)jbuilder build @$(INFER_BUILD_DIR)/doc + INFER_BIN_ALIASES = $(foreach alias,$(INFER_COMMANDS),$(BIN_DIR)/$(alias)) $(INFER_BIN_ALIASES): Makefile diff --git a/infer/src/absint/README.md b/infer/src/absint/README.md deleted file mode 100644 index 8b4129856..000000000 --- a/infer/src/absint/README.md +++ /dev/null @@ -1,3 +0,0 @@ -# AbsInt - -Code + utilities for the Infer.AI abstract interpretation framework. diff --git a/infer/src/atd/index.mld b/infer/src/atd/index.mld new file mode 100644 index 000000000..f30e3bc33 --- /dev/null +++ b/infer/src/atd/index.mld @@ -0,0 +1,5 @@ +{1 Library InferGenerated} +Source code that is generated from ATD definitions. + +The entry point of this library is the module: +{!module-InferGenerated}. diff --git a/infer/src/atd/jbuild.in b/infer/src/atd/jbuild.in index 96f613697..95d0e6f45 100644 --- a/infer/src/atd/jbuild.in +++ b/infer/src/atd/jbuild.in @@ -7,11 +7,17 @@ let cflags = common_cflags @ ["-w"; "-27-32-34-35-39"] {| (library ((name InferGenerated) + (public_name InferGenerated) (flags (%s)) (ocamlopt_flags (%s)) (libraries (atdgen core)) (preprocess (pps (ppx_compare))) )) + +(documentation + ((package InferGenerated) + (mld_files (index)) + )) |} (String.concat " " cflags) (String.concat " " common_optflags) diff --git a/infer/src/backend/README.md b/infer/src/backend/README.md deleted file mode 100644 index 389756202..000000000 --- a/infer/src/backend/README.md +++ /dev/null @@ -1,9 +0,0 @@ -# Back End - -The back end is responsible for the analysis of a project starting from an intermediate representation stored in the results directory, typically `infer-out`. - -The main entry point for infer binary is [infer.ml](infer.ml). - -Entry point for the analysis is module [InferAnalyze](InferAnalyze.ml). - -Module [InferPrint](InferPrint.ml) is used to export the analysis results. diff --git a/infer/src/base/README.md b/infer/src/base/index.mld similarity index 51% rename from infer/src/base/README.md rename to infer/src/base/index.mld index 6aadf2ac0..134d6d036 100644 --- a/infer/src/base/README.md +++ b/infer/src/base/index.mld @@ -1,2 +1,6 @@ +{1 Library InferBase} Utility modules that are somewhat specific to infer, usually because they depend on Config.ml. + +The entry point of this library is the module: +{!module-InferBase}. diff --git a/infer/src/base/jbuild.in b/infer/src/base/jbuild.in index 3b8375589..f8ed68760 100644 --- a/infer/src/base/jbuild.in +++ b/infer/src/base/jbuild.in @@ -4,11 +4,17 @@ {| (library ((name InferBase) + (public_name InferBase) (flags (%s -open Core -open InferStdlib -open IStd -open InferGenerated)) (ocamlopt_flags (%s)) (libraries (%s)) (preprocess (pps (ppx_compare))) )) + +(documentation + ((package InferBase) + (mld_files (index)) + )) |} (String.concat " " common_cflags) (String.concat " " common_optflags) diff --git a/infer/src/checkers/README.md b/infer/src/checkers/README.md deleted file mode 100644 index c98bee84a..000000000 --- a/infer/src/checkers/README.md +++ /dev/null @@ -1,3 +0,0 @@ -# Checkers - -Transfer functions, abstract domains, and checker configuration. \ No newline at end of file diff --git a/infer/src/checkers/accessPathDomains.mli b/infer/src/checkers/accessPathDomains.mli index 493ea2ff8..ccc605670 100644 --- a/infer/src/checkers/accessPathDomains.mli +++ b/infer/src/checkers/accessPathDomains.mli @@ -20,11 +20,11 @@ module Set : sig val of_list : AccessPath.Abs.t list -> astate val mem : AccessPath.Abs.t -> astate -> bool - (** return true if \gamma({ap}) \subseteq \gamma(aps). + (** return true if \gamma(\{ap\}) \subseteq \gamma(aps). note: this is worst-case linear in the size of the set *) val mem_fuzzy : AccessPath.Abs.t -> astate -> bool - (** more permissive version of [mem]; return true if \gamma({a}) \cap \gamma(aps) != {}. + (** more permissive version of [mem]; return true if \gamma(\{a\}) \cap \gamma(aps) != \{\}. note: this is worst-case linear in the size of the set *) val add : AccessPath.Abs.t -> astate -> astate diff --git a/infer/src/checkers/accessTree.mli b/infer/src/checkers/accessTree.mli index 4d32722e4..b8043f496 100644 --- a/infer/src/checkers/accessTree.mli +++ b/infer/src/checkers/accessTree.mli @@ -23,7 +23,7 @@ module type S = sig | Star (** special leaf for starred access paths *) (** map from base var -> access subtree. Here's how to represent a few different kinds of - trace * access path associations: + trace * access path associations: {[ (x, T) := { x |-> (T, Subtree {}) } (x.f, T) := { x |-> (empty, Subtree { f |-> (T, Subtree {}) }) } (x*, T) := { x |-> (T, Star) } @@ -31,6 +31,7 @@ module type S = sig (x, T1), (y, T2) := { x |-> (T1, Subtree {}), y |-> (T2, Subtree {}) } (x.f, T1), (x.g, T2) := { x |-> (empty, Subtree { f |-> (T1, Subtree {}), g |-> (T2, Subtree {}) }) } + ]} *) type t = node BaseMap.t diff --git a/infer/src/clang/README.md b/infer/src/clang/README.md deleted file mode 100644 index 2da130781..000000000 --- a/infer/src/clang/README.md +++ /dev/null @@ -1,29 +0,0 @@ -# Clang Front-End - -This is the front-end for the clang compiler. - -The main entry point is [`ClangWrapper`](ClangWrapper.ml). - -## General structure -1. Given a compilation command from the build system, sanitize it, attach `ASTExporter` clang plugin to the relevant commands and run it. -2. Parse the AST from Biniou format to OCaml data structure. -3. (optional) Invoke translation to `SIL` via [`CFrontend`](cFrontend.ml). -4. (optional) Invoke linters via [`CFrontend_checkers_main`](CFrontend_checkers_main.ml). [More on linters](http://fbinfer.com/docs/linters.html) - -## Format of the AST -OCaml data structure is defined in `atd` format. The `clang_ast_t.atd` file is generated from comments in [ASTExporter.h](https://github.com/facebook/facebook-clang-plugins/blob/master/libtooling/ASTExporter.h) file. - -For more information, refer to the relevant documentation in `facebook-clang-plugins`: -- [libtooling/ATD_GUIDELINES.md](https://github.com/facebook/facebook-clang-plugins/blob/master/libtooling/ATD_GUIDELINES.md) -- [clang-ocaml/README.md](https://github.com/facebook/facebook-clang-plugins/blob/master/clang-ocaml/README.md) - -## Hacking on `.atd` file -1. Create a simple example (`example.cpp`) source file with construct that needs to be exported. The smaller the better. -2. Export extra information by changing code in [`libtooling/ASTExporter.h`](https://github.com/facebook/facebook-clang-plugins/blob/master/libtooling/ASTExporter.h). For more information, refer to the [ATD_GUIDELINES](https://github.com/facebook/facebook-clang-plugins/blob/master/libtooling/ATD_GUIDELINES.md). -3. Compile Infer with the new version of `facebook-clang-plugins`. Running `make all` from top level of Infer repository will do that. Sometimes there may be compilation errors due to `.atd` file changes - they need to be fixed. -4. Use newly exported information information in the frontend. - -Tips & Tricks: -- To view the AST in a human readable version, Infer can generate `.bdump` file: `infer -g -- clang -c example.cpp && sh example.cpp.ast.sh`. Then open `example.cpp.ast.bdump` -- To inspect ast dump visually: `clang -c example.cpp -Xclang -ast-dump`. It doesn't include all the information that Infer sees, but it's pretty concise -- If running `bdump` is failing (it happens on huge sources sometimes), there is a way to view it in "Yojson" format. To do that, replace all occurrences of `BiniouASTExporter` with `YojsonASTExporter` in `.ast.sh` script. diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 2b3d7b618..5e7413906 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -75,7 +75,7 @@ module ThreadsDomain : sig etc.) *) | AnyThreadButSelf (** Current thread can run in parallel with other threads, but not with a copy of itself. - (concretization : { t | t \in TIDs ^ t != t_cur } ) *) + (concretization : \{ t | t \in TIDs ^ t != t_cur \} ) *) | AnyThread (** Current thread can run in parallel with any thread, including itself (concretization: set of all TIDs ) *) diff --git a/infer/src/eradicate/README.md b/infer/src/eradicate/README.md deleted file mode 100644 index 973467eb5..000000000 --- a/infer/src/eradicate/README.md +++ /dev/null @@ -1,5 +0,0 @@ -# Eradicate @Nullable Checker - -Eradicate is a type checker for `@Nullable` annotations for Java. The goal is to eradicate null pointer exceptions. See [Eradicate](http://fbinfer.com/docs/eradicate.html). - -The main entry point is module [Eradicate](eradicate.mli). \ No newline at end of file diff --git a/infer/src/index.mld b/infer/src/index.mld new file mode 100644 index 000000000..668ba9a1c --- /dev/null +++ b/infer/src/index.mld @@ -0,0 +1,63 @@ +{1 Library infer} +These are the modules used by infer that are not packaged into sub-libraries. + +The entry point of this library is the module: +{!module-InferModules}. + + +The modules are split into several directories in the source tree of infer. + +{2 absint/} +Code + utilities for the Infer.AI abstract interpretation framework. Start at {!module-InferModules.AbstractInterpreter}. + +{2 backend/} +The backend is responsible for the analysis of a project starting from an intermediate representation stored in the results directory, typically [infer-out]. + +The entry point for the analysis is the module {!module-InferModules.InferAnalyze}. + +The module {!module-InferModules.InferPrint} is used to export the analysis results. + +{2 checkers/} +Transfer functions, abstract domains, and checker configuration. + +{2 clang/} +This is the frontend for the clang compiler. The main entry point is {!module-InferModules.ClangWrapper}. + +{3 General structure} ++ Given a compilation command from the build system, sanitize it, attach [ASTExporter] clang plugin to the relevant commands and run it. ++ Parse the AST (Abstract Syntax Tree) from the Biniou format into an OCaml data structure. ++ If enabled, invoke translation to [SIL] via {!module-InferModules.CFrontend}. ++ If enabled, invoke linters via {!module-InferModules.CFrontend_checkers_main}. More on linters here: {:http://fbinfer.com/docs/linters.html}. + +{3 Format of the AST} +The OCaml data type is defined in [atd] format. The [clang_ast_t.atd] file is generated from the comments in the {{:https://github.com/facebook/facebook-clang-plugins/blob/master/libtooling/ASTExporter.h} [ASTExporter.h]} file. + +For more information, refer to the relevant documentation in [facebook-clang-plugins]: +- {{:https://github.com/facebook/facebook-clang-plugins/blob/master/libtooling/ATD_GUIDELINES.md} [libtooling/ATD_GUIDELINES.md]} +- {{:https://github.com/facebook/facebook-clang-plugins/blob/master/clang-ocaml/README.md} [clang-ocaml/README.md]} + +{3 Hacking on the [.atd] file} ++ Create a simple example ([example.cpp]) source file with construct that needs to be exported. The smaller the better. ++ Export the extra information by changing the code in {{:https://github.com/facebook/facebook-clang-plugins/blob/master/libtooling/ASTExporter.h} [libtooling/ASTExporter.h]}. For more information, refer to the {{:https://github.com/facebook/facebook-clang-plugins/blob/master/libtooling/ATD_GUIDELINES.md} [ATD_GUIDELINES]}. ++ Compile Infer with the new version of [facebook-clang-plugins]. Running [make] from top level of Infer repository will do that. Sometimes there may be compilation errors due to [.atd] file changes - they need to be fixed. ++ Use newly exported information information in the frontend. + +Tips & Tricks: +- To view the AST in a human readable version, Infer can generate [.bdump] file: [infer -g -- clang -c example.cpp && sh example.cpp.ast.sh]. Then open [example.cpp.ast.bdump]. +- To inspect AST dump visually: [clang -c example.cpp -Xclang -ast-dump]. It doesn't include all the information that Infer sees, but it's pretty concise +- If running [bdump] is failing (it happens on huge sources sometimes), there is a way to view it in "Yojson" format. To do that, replace all occurrences of [BiniouASTExporter] with [YojsonASTExporter] in the [.ast.sh] script. + +{2 eradicate/ } +Eradicate [@Nullable] Checker + +Eradicate is a type checker for [@Nullable] annotations for Java. The goal is to eradicate null pointer exceptions. See the online docs at {:http://fbinfer.com/docs/eradicate.html}. + +The main entry point is module {!module-InferModules.Eradicate}. + +{2 java/} +Java Frontend; this is the frontend for Java compilers. + +The main entry point is {!module-InferModules.JMain}. + +{2 infer executable} +You'll find the infer binary in infer.ml. It is not part of this library. diff --git a/infer/src/infer.opam b/infer/src/infer.opam new file mode 100644 index 000000000..e69de29bb diff --git a/infer/src/istd/Pp.mli b/infer/src/istd/Pp.mli index 7ab91d740..1a91607dd 100644 --- a/infer/src/istd/Pp.mli +++ b/infer/src/istd/Pp.mli @@ -9,7 +9,7 @@ open! IStd module F = Format -(** Pretty Printing} *) +(** Pretty Printing *) (** Colors supported in printing *) type color = Black | Blue | Green | Orange | Red [@@deriving compare] diff --git a/infer/src/istd/README.md b/infer/src/istd/index.mld similarity index 50% rename from infer/src/istd/README.md rename to infer/src/istd/index.mld index 0b0fd2b6b..08b261d98 100644 --- a/infer/src/istd/README.md +++ b/infer/src/istd/index.mld @@ -1,2 +1,6 @@ +{1 Library InferStdLib} Utility modules not specific to infer. In particular, nothing here should depend on Config.ml. + +The entry point of this library is the module: +{!module-InferStdlib}. diff --git a/infer/src/istd/jbuild.in b/infer/src/istd/jbuild.in index 5a7435bb3..e33305e60 100644 --- a/infer/src/istd/jbuild.in +++ b/infer/src/istd/jbuild.in @@ -4,11 +4,17 @@ {| (library ((name InferStdlib) + (public_name InferStdlib) (flags (%s -open Core)) (ocamlopt_flags (%s)) (libraries (%s)) (preprocess (pps (ppx_compare))) )) + +(documentation + ((package InferStdlib) + (mld_files (index)) + )) |} (String.concat " " common_cflags) (String.concat " " common_optflags) diff --git a/infer/src/java/README.md b/infer/src/java/README.md deleted file mode 100644 index 1150b2b35..000000000 --- a/infer/src/java/README.md +++ /dev/null @@ -1,5 +0,0 @@ -# Java Front-End - -This is the front-end for java compilers. - -The main entry point is [JMain](jMain.ml). diff --git a/infer/src/jbuild.in b/infer/src/jbuild.in index e36e91318..834a14050 100644 --- a/infer/src/jbuild.in +++ b/infer/src/jbuild.in @@ -52,12 +52,18 @@ let stanzas = {| (library ((name InferModules) + (public_name infer) (flags (%s)) (ocamlopt_flags (%s)) (libraries (%s)) (modules (:standard \ %s infertop)) (preprocess (pps (ppx_compare ppx_sexp_conv -no-check))) )) + +(documentation + ((package infer) + (mld_files (index)) + )) |} (String.concat " " infer_cflags) (String.concat " " common_optflags)