Merge pull request #1055 from goblint/api-docs

Add odoc API documentation

.github/workflows/docs.yml

@@ -0,0 +1,68 @@
+name: docs
+
+on:
+  push:
+    branches:
+      - master
+
+  workflow_dispatch:
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+concurrency:
+  group: "pages"
+  cancel-in-progress: true
+
+jobs:
+  api-build:
+    strategy:
+      matrix:
+        os:
+          - ubuntu-latest
+        ocaml-compiler:
+          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          # don't add any other because they won't be used
+
+    runs-on: ${{ matrix.os }}
+
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v3
+
+      - name: Set up OCaml ${{ matrix.ocaml-compiler }}
+        env:
+          # otherwise setup-ocaml pins non-locked dependencies
+          # https://github.com/ocaml/setup-ocaml/issues/166
+          OPAMLOCKED: locked
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+
+      - name: Setup Pages
+        id: pages
+        uses: actions/configure-pages@v2
+
+      - name: Install dependencies
+        run: opam install . --deps-only --locked --with-doc
+
+      - name: Build API docs
+        run: opam exec -- dune build @doc
+
+      - name: Upload artifact
+        uses: actions/upload-pages-artifact@v1
+        with:
+          path: _build/default/_doc/_html/
+
+  api-deploy:
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    runs-on: ubuntu-latest
+    needs: api-build
+    steps:
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v1

mkdocs.yml

@@ -30,6 +30,7 @@ nav:
     - 👶 Your first analysis: developer-guide/firstanalysis.md
     - 🏫 Extending library: developer-guide/extending-library.md
     - 📢 Messaging: developer-guide/messaging.md
+    - 🗃️ API reference: https://goblint.github.io/analyzer/
     - 🚨 Testing: developer-guide/testing.md
     - 🪲 Debugging: developer-guide/debugging.md
     - 📉 Profiling: developer-guide/profiling.md

src/analyses/abortUnless.ml

@@ -1,4 +1,6 @@
-(** An analysis checking whether a function only returns if its only argument has a non-zero value. *)
+(** Analysis of [assume_abort_if_not]-style functions ([abortUnless]).
+
+    Such a function only returns if its only argument has a non-zero value. *)
 
 open GoblintCil
 open Analyses

src/analyses/accessAnalysis.ml

@@ -1,4 +1,4 @@
-(** Access analysis. *)
+(** Analysis of memory accesses ([access]). *)
 
 module LF = LibraryFunctions
 open GoblintCil

src/analyses/activeLongjmp.ml

@@ -1,4 +1,4 @@
-(** Analysis tracking which longjmp is currently active *)
+(** Analysis of active [longjmp] targets ([activeLongjmp]). *)
 
 open GoblintCil
 open Analyses

src/analyses/activeSetjmp.ml

@@ -1,4 +1,4 @@
-(** Analysis tracking which setjmp(s) are currently active *)
+(** Analysis of active [setjmp] buffers ([activeSetjmp]). *)
 
 open GoblintCil
 open Analyses

src/analyses/apron/affineEqualityAnalysis.apron.ml

@@ -1,5 +1,7 @@
-(* Ref: Affine Relationships Among Variables of a Program, Michael Karr 1976
-    https://link.springer.com/content/pdf/10.1007/BF00268497.pdf *)
+(** {{!RelationAnalysis} Relational integer value analysis} using an OCaml implementation of the affine equalities domain ([affeq]).
+
+    @see <https://doi.org/10.1007/BF00268497> Karr, M. Affine relationships among variables of a program. *)
+
 open Analyses
 
 include RelationAnalysis

src/analyses/apron/apronAnalysis.apron.ml

@@ -1,4 +1,5 @@
-(** Analysis using Apron for integer variables. *)
+(** {{!RelationAnalysis} Relational integer value analysis} using {!Apron} domains ([apron]). *)
+
 open Analyses
 
 include RelationAnalysis

src/analyses/apron/relationAnalysis.apron.ml

@@ -1,3 +1,7 @@
+(** Abstract relational {e integer} value analysis.
+
+    See {!ApronAnalysis} and {!AffineEqualityAnalysis}. *)
+
 (** Contains most of the implementation of the original apronDomain, but now solely operates with functions provided by relationDomain. *)
 
 open Batteries

src/analyses/apron/relationPriv.apron.ml

@@ -1,4 +1,6 @@
-(** Has been modified to work with any domain that uses the functions provided relationDomain. *)
+(** Relational thread-modular value analyses for {!RelationAnalysis}, i.e. {!ApronAnalysis} and {!AffineEqualityAnalysis}.
+
+    @see <https://doi.org/10.1007/978-3-031-30044-8_2> Schwarz, M., Saan, S., Seidl, H., Erhard, J., Vojdani, V. Clustered Relational Thread-Modular Abstract Interpretation with Local Traces. *)
 
 open Batteries
 open GoblintCil

src/analyses/assert.ml

@@ -1,3 +1,5 @@
+(** Analysis of [assert] results ([assert]). *)
+
 open Batteries
 open GoblintCil
 open Analyses

src/analyses/base.ml

@@ -1,4 +1,4 @@
-(** Value analysis.  *)
+(** Non-relational value analysis aka {e base analysis} ([base]). *)
 
 open Batteries
 open GoblintCil

src/analyses/baseInvariant.ml

@@ -1,3 +1,5 @@
+(** {!Analyses.Spec.branch} refinement for {!Base} analysis. *)
+
 open GoblintCil
 
 module M = Messages

src/analyses/basePriv.mli

@@ -1,3 +1,7 @@
+(** Non-relational thread-modular value analyses for {!Base}.
+
+    @see <https://doi.org/10.1007/978-3-030-88806-0_18> Schwarz, M., Saan, S., Seidl, H., Apinis, K., Erhard, J., Vojdani, V. Improving Thread-Modular Abstract Interpretation. *)
+
 open GoblintCil
 (* Cannot use local module substitutions because ppx_import is still stuck at 4.07 AST: https://github.com/ocaml-ppx/ppx_import/issues/50#issuecomment-775817579. *)
 (* TODO: try again, because ppx_import is now removed *)

src/analyses/baseUtil.mli

@@ -1,3 +1,5 @@
+(** Basic analysis utilities. *)
+
 open GoblintCil
 
 val is_global: Queries.ask -> varinfo -> bool

src/analyses/commonPriv.ml

@@ -1,3 +1,5 @@
+(** Thread-modular value analysis utilities for {!BasePriv} and {!RelationPriv}. *)
+
 open Batteries
 open GoblintCil
 open Analyses

src/analyses/condVars.ml

@@ -1,4 +1,4 @@
-(** Must equality between variables and logical expressions. *)
+(** Symbolic variable - logical expression equalities analysis ([condvars]). *)
 (* TODO: unused, what is this analysis? *)
 
 open Batteries

src/analyses/deadlock.ml

@@ -1,4 +1,4 @@
-(** Deadlock analysis. *)
+(** Deadlock analysis ([deadlock]). *)
 
 open Batteries
 open GoblintCil

src/analyses/expRelation.ml

@@ -1,6 +1,8 @@
+(** Stateless symbolic comparison expression analysis ([expRelation]). *)
+
 (** An analysis specification to answer questions about how two expressions relate to each other.   *)
-(** Currently this works purely syntactically on the expressions, and only for =_{must}.            *)
-(** Does not keep state, this is only formulated as an analysis to integrate well into framework    *)
+(** Currently this works purely syntactically on the expressions, and only for {m =_{must}}. *)
+(** Does not keep state, this is only formulated as an analysis to integrate well into the framework.  *)
 
 open GoblintCil
 open Analyses

src/analyses/expsplit.ml

@@ -1,3 +1,5 @@
+(** Path-sensitive analysis according to values of arbitrary given expressions ([expsplit]). *)
+
 open Batteries
 open GoblintCil
 open Analyses

src/analyses/extractPthread.ml

@@ -1,4 +1,4 @@
-(** Tracking of pthread lib code. Output to promela. *)
+(** Promela extraction analysis for Pthread programs ([extract-pthread]). *)
 
 open GoblintCil
 open Pretty

src/analyses/fileUse.ml

@@ -1,4 +1,6 @@
-(** An analysis for checking correct use of file handles. *)
+(** Analysis of correct file handle usage ([file]).
+
+    @see <https://www2.in.tum.de/hp/file?fid=1323> Vogler, R. Verifying Regular Safety Properties of C Programs Using the Static Analyzer Goblint. Section 3.*)
 
 open Batteries
 open GoblintCil

src/analyses/libraryDesc.ml

@@ -1,4 +1,5 @@
 (** Library function descriptor (specification). *)
+
 module Cil = GoblintCil
 
 (** Pointer argument access specification. *)

src/analyses/libraryDsl.mli

@@ -18,11 +18,11 @@ type ('k, 'r) args_desc =
   | (::): ('k, _, 'm) arg_desc * ('m, 'r) args_desc -> ('k, 'r) args_desc (** Cons one argument descriptor. Argument must occur. *)
 
 
-(** Create library function descriptor from arguments descriptor and continuation function, which takes as many arguments as are captured using {!__} and returns the corresponding {!LibraryDesc.special}. *)
+(** Create library function descriptor from arguments descriptor and continuation function, which takes as many arguments as are captured using {!__} and returns the corresponding {!LibraryDesc.type-special}. *)
 val special: ?attrs:LibraryDesc.attr list -> ('k, LibraryDesc.special) args_desc -> 'k -> LibraryDesc.t
 
-(** Create library function descriptor from arguments descriptor, which must {!drop} all arguments, and continuation function, which takes as an {!unit} argument and returns the corresponding {!LibraryDesc.special}.
-    Unlike {!special}, this allows the {!LibraryDesc.special} of an argumentless function to depend on options, such that they aren't evaluated at initialization time in {!LibraryFunctions}.  *)
+(** Create library function descriptor from arguments descriptor, which must {!drop} all arguments, and continuation function, which takes as an {!unit} argument and returns the corresponding {!LibraryDesc.type-special}.
+    Unlike {!special}, this allows the {!LibraryDesc.type-special} of an argumentless function to depend on options, such that they aren't evaluated at initialization time in {!LibraryFunctions}.  *)
 val special': ?attrs:LibraryDesc.attr list -> (LibraryDesc.special, LibraryDesc.special) args_desc -> (unit -> LibraryDesc.special) -> LibraryDesc.t
 
 (** Create unknown library function descriptor from arguments descriptor, which must {!drop} all arguments. *)

src/analyses/libraryFunctions.mli

@@ -1,4 +1,5 @@
-(** This allows us to query information about library functions. *)
+(** Hard-coded database of library function specifications. *)
+
 open GoblintCil
 
 val add_lib_funs : string list -> unit

src/analyses/mCP.ml

@@ -1,4 +1,4 @@
-(** Master Control Program *)
+(** MCP analysis specification. *)
 
 open Batteries
 open GoblintCil

src/analyses/mCPAccess.ml

@@ -1,3 +1,4 @@
+(** {{!Analyses.MCPA} Memory access metadata module} for MCP. *)
 
 open MCPRegistry
 module Pretty = GoblintCil.Pretty

src/analyses/mCPRegistry.ml

@@ -1,3 +1,6 @@
+(** Registry of dynamically activatable analyses.
+    Analysis specification modules for the dynamic product. *)
+
 open Batteries
 open GoblintCil
 open Pretty

src/analyses/mHPAnalysis.ml

@@ -1,4 +1,5 @@
-(** MHP access analysis. *)
+(** May-happen-in-parallel (MHP) analysis for memory accesses ([mhp]). *)
+
 open Analyses
 
 module Spec =

src/analyses/mallocFresh.ml

@@ -1,3 +1,5 @@
+(** Analysis of unescaped (i.e. thread-local) heap locations ([mallocFresh]). *)
+
 open GoblintCil
 open Analyses
 

src/analyses/mallocWrapperAnalysis.ml

@@ -1,4 +1,7 @@
-(** An analysis that handles the case when malloc is called from a wrapper function all over the code. *)
+(** Analysis which provides symbolic heap locations for dynamic memory allocations. ([mallocWrapper]).
+
+  Provided heap locations are based on the node and thread ID.
+  Considers [malloc] wrapper functions and a number of unique heap locations for additional precision. *)
 
 open GoblintCil
 open Analyses

src/analyses/malloc_null.ml

@@ -1,4 +1,4 @@
-(** Path-sensitive analysis that verifies checking the result of the malloc function. *)
+(** Path-sensitive analysis of failed dynamic memory allocations ([malloc_null]). *)
 
 module AD = ValueDomain.AD
 module IdxDom = ValueDomain.IndexDomain

src/analyses/mayLocks.ml

@@ -1,4 +1,6 @@
-(** May lockset analysis (unused). *)
+(** May lockset analysis ([maylocks]). *)
+
+(* TODO: unused *)
 
 open Analyses
 

src/analyses/modifiedSinceLongjmp.ml

@@ -1,4 +1,6 @@
-(** Locally track the variables that may have been written since the corresponding jumpbuffer was set *)
+(** Analysis of variables modified since [setjmp] ([modifiedSinceLongjmp]). *)
+
+(* TODO: this name is wrong *)
 
 open GoblintCil
 open Analyses

src/analyses/mutexAnalysis.ml

@@ -1,4 +1,4 @@
-(** Protecting mutex analysis. Must locksets locally and for globals. *)
+(** Must lockset and protecting lockset analysis ([mutex]). *)
 
 module M = Messages
 module Addr = ValueDomain.Addr

src/analyses/mutexEventsAnalysis.ml

@@ -1,4 +1,6 @@
-(** Mutex events analysis (Lock and Unlock). *)
+(** Mutex locking and unlocking analysis ([mutexEvents]).
+
+    Emits {!Events.Lock} and {!Events.Unlock} to other analyses. *)
 
 module M = Messages
 module Addr = ValueDomain.Addr

src/analyses/poisonVariables.ml

@@ -1,3 +1,5 @@
+(** Taint analysis of variables that were modified between [setjmp] and [longjmp] and not yet overwritten. ([poisonVariables]). *)
+
 open Batteries
 open GoblintCil
 open Analyses

src/analyses/pthreadSignals.ml

@@ -1,4 +1,4 @@
-(** Analysis of must-received pthread_signals. *)
+(** Must received signals analysis for Pthread condition variables ([pthreadSignals]). *)
 
 open GoblintCil
 open Analyses

src/analyses/raceAnalysis.ml

@@ -1,4 +1,4 @@
-(** Data race analysis. *)
+(** Data race analysis ([race]). *)
 
 open GoblintCil
 open Analyses

src/analyses/region.ml

@@ -1,4 +1,6 @@
-(** Assigning static regions to dynamic memory. *)
+(** Analysis of disjoint heap regions for dynamically allocated memory ([region]).
+
+    @see <https://doi.org/10.1007/978-3-642-03237-0_13> Seidl, H., Vojdani, V. Region Analysis for Race Detection. *)
 
 open Batteries
 open GoblintCil

src/analyses/spec.ml

@@ -1,4 +1,8 @@
-(** Analysis by specification file. *)
+(** Analysis using finite automaton specification file ([spec]).
+
+    @author Ralf Vogler
+
+    @see <https://www2.in.tum.de/hp/file?fid=1323> Vogler, R. Verifying Regular Safety Properties of C Programs Using the Static Analyzer Goblint. Section 4. *)
 
 open Batteries
 open GoblintCil

src/analyses/stackTrace.ml

@@ -1,4 +1,4 @@
-(** Stack-trace "analyses". *)
+(** Call stack analyses ([stack_trace], [stack_trace_set], [stack_loc]). *)
 
 open GoblintCil
 open Analyses

src/analyses/symbLocks.ml

@@ -1,6 +1,6 @@
-(** Symbolic lock-sets for use in per-element patterns.
+(** Symbolic lockset analysis for per-element (field or index) locking patterns ([symb_locks]).
 
-    See Section 5 and 6 in https://dl.acm.org/doi/10.1145/2970276.2970337 for more details. *)
+    @see <https://doi.org/10.1145/2970276.2970337> Static race detection for device drivers: the Goblint approach. Section 5 and 6. *)
 
 module LF = LibraryFunctions
 module LP = SymbLocksDomain.LockingPattern

src/analyses/taintPartialContexts.ml

@@ -1,3 +1,5 @@
+(** Taint analysis of variables modified in a function ([taintPartialContexts]). *)
+
 (* TaintPartialContexts: Set of Lvalues, which are tainted at a specific Node. *)
 (* An Lvalue is tainted, if its Rvalue might have been altered in the context of the current function,
    implying that the Rvalue of any Lvalue not in the set has definitely not been changed within the current context. *)

src/analyses/termination.ml

@@ -1,4 +1,4 @@
-(** Termination of loops. *)
+(** Termination analysis of loops using counter variables ([term]). *)
 
 open Batteries
 open GoblintCil

src/analyses/threadAnalysis.ml

@@ -1,4 +1,4 @@
-(** Thread creation and uniqueness analyses. *)
+(** Created threads and their uniqueness analysis ([thread]). *)
 
 open GoblintCil
 open Analyses

src/analyses/threadEscape.ml

@@ -1,4 +1,4 @@
-(** Variables that escape threads using the last argument from pthread_create. *)
+(** Escape analysis for thread-local variables ([escape]). *)
 
 open GoblintCil
 open Analyses