[doc] add `make doc` target for building html API doc

Summary:
`make doc` will use `jbuilder` (which in turn uses `odoc`) to generate the
documentation for infer's modules. This is useful to browse the APIs of infer
and gives a more discoverable place to host more general documentation about
infer's internals.

Besides the actual plumbing necessary to generate the docs, this diff also
- Moves the various infer/src/*/README.md to index.mld files that make it to the generated docs
- Fixes some doc comments that would anger `ocamldoc`

Closes #435

Reviewed By: mbouaziz

Differential Revision: D8314572

fbshipit-source-id: 4a5c70e
master
Jules Villard 7 years ago committed by Facebook Github Bot
parent aee02e27ef
commit 710dae8ee4

@ -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:

@ -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).

@ -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}.

@ -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)

@ -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

@ -1,3 +0,0 @@
# AbsInt
Code + utilities for the Infer.AI abstract interpretation framework.

@ -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}.

@ -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)

@ -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.

@ -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}.

@ -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)

@ -1,3 +0,0 @@
# Checkers
Transfer functions, abstract domains, and checker configuration.

@ -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

@ -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

@ -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.

@ -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 ) *)

@ -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).

@ -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.

@ -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]

@ -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}.

@ -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)

@ -1,5 +0,0 @@
# Java Front-End
This is the front-end for java compilers.
The main entry point is [JMain](jMain.ml).

@ -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)

Loading…
Cancel
Save