Module Goblint_lib

Main library.

Framework

module Maingoblint : sig ... end

Main external executable functionality: command-line, front-end and analysis execution.

module Control : sig ... end

Main internal functionality: analysis of the program by abstract interpretation via constraint solving.

module Server : sig ... end

Interactive server mode using JSON-RPC.

CFG

Control-flow graphs (CFGs) are used to represent each function.

module Node = Node
module Edge = Edge
module MyCFG = MyCFG
module CfgTools = CfgTools

Specification

Analyses are specified by domains and transfer functions. A dynamic composition of analyses is combined with CFGs to produce a constraint system.

module Analyses : sig ... end

Analysis specification signatures.

module Constraints : sig ... end

Construction of a constraint system from an analysis specification and CFGs. Transformatons of analysis specifications as functors.

module CompareConstraints : sig ... end
module AnalysisState = AnalysisState
module AnalysisStateUtil = AnalysisStateUtil
module ControlSpecC = ControlSpecC

Master control program (MCP) is the analysis specification for the dynamic product of activated analyses.

module MCP : sig ... end

MCP analysis specification.

module MCPRegistry : sig ... end

Registry of dynamically activatable analyses. Analysis specification modules for the dynamic product.

module MCPAccess : sig ... end

Memory access metadata module for MCP.

MCP allows activated analyses to query each other during the analysis. Query results from different analyses for the same query are met for precision.

module Queries : sig ... end

Queries and their result lattices.

MCP allows activated analyses to emit events to each other during the analysis.

module Events : sig ... end

Events.

Results

The following modules help query the constraint system solution using semantic information.

module AnalysisResult : sig ... end

Analysis results.

module ResultQuery : sig ... end

Perform queries on the constraint system solution.

Configuration

Runtime configuration is represented as JSON. Options are specified and documented by the JSON schema src/config/options.schema.json.

module GobConfig = GobConfig
module AfterConfig = AfterConfig
module AutoTune : sig ... end

Autotuning of the configuration based on syntactic heuristics.

module AutoSoundConfig : sig ... end

Automatically turning on analyses required to ensure soundness based on a given specification (e.g., SV-COMP specification) or programming idioms (e.g., longjmp) in the analyzed code, but only when it is possible to do so automatically. This does not fully exempt from the need for manual configuration.

module JsonSchema = JsonSchema
module Options = Options

Analyses

Analyses activatable under MCP.

Value

Analyses related to values of program variables.

module Base : sig ... end

Non-relational value analysis aka base analysis (base).

module RelationAnalysis : sig ... end

Abstract relational integer value analysis.

module ApronAnalysis : sig ... end

Relational integer value analysis using Apron domains (apron).

module AffineEqualityAnalysis : sig ... end

Relational integer value analysis using an OCaml implementation of the affine equalities domain (affeq).

module LinearTwoVarEqualityAnalysis : sig ... end

Relational integer value analysis using an OCaml implementation of the linear two-variable equalities domain (lin2vareq).

module VarEq : sig ... end

Symbolic expression equalities analysis (var_eq).

module CondVars : sig ... end

Symbolic variable - logical expression equalities analysis (condvars).

module TmpSpecial : sig ... end

Analysis that tracks which variables hold the results of calls to math library functions (tmpSpecial).

module C2poAnalysis : sig ... end

C-2PO: A Weakly-Relational Pointer Analysis for C based on 2 Pointer Logic. The analysis can infer equalities and disequalities between terms which are built from pointer variables, with the addition of constants and dereferencing. (c2po)

Heap

Analyses related to the heap.

module Region : sig ... end

Analysis of disjoint heap regions for dynamically allocated memory (region).

module MallocFresh : sig ... end

Analysis of unescaped (i.e. thread-local) heap locations (mallocFresh).

module Malloc_null : sig ... end

Helper analysis to be path-sensitive in failed dynamic memory allocations (malloc_null). It is not soundness critical, it only causes certain paths to be kept separate.

module MemLeak : sig ... end

An analysis for the detection of memory leaks (memLeak).

module UseAfterFree : sig ... end

An analysis for the detection of use-after-free vulnerabilities (useAfterFree).

module MemOutOfBounds : sig ... end

An analysis for the detection of out-of-bounds memory accesses (memOutOfBounds).

Concurrency

Analyses related to concurrency.

Locks

Analyses related to locking.

module MutexEventsAnalysis : sig ... end

Mutex locking and unlocking analysis (mutexEvents).

module LocksetAnalysis : sig ... end

Basic lockset analyses.

module MutexTypeAnalysis : sig ... end

An analysis tracking the type of a mutex (pthreadMutexType).

module MutexAnalysis : sig ... end

Must lockset and protecting lockset analysis (mutex).

module MayLocks : sig ... end

May lockset analysis and analysis of double locking (maylocks).

module SymbLocks : sig ... end

Symbolic lockset analysis for per-element (field or index) locking patterns (symb_locks).

module Deadlock : sig ... end

Deadlock analysis (deadlock).

module MutexGhosts : sig ... end

Analysis for generating ghost variables corresponding to mutexes (mutexGhosts).

Threads

Analyses related to threads.

module ThreadFlag : sig ... end

Multi-threadedness analysis (threadflag).

module ThreadId : sig ... end

Current thread ID analysis (threadid).

module ThreadAnalysis : sig ... end

Created threads and their uniqueness analysis (thread).

module ThreadJoins : sig ... end

Joined threads analysis (threadJoins).

module MHPAnalysis : sig ... end

May-happen-in-parallel (MHP) analysis for memory accesses (mhp).

module ThreadReturn : sig ... end

Thread returning analysis which abstracts a thread's call stack by a boolean, indicating whether it is at the topmost call stack frame or not (threadreturn).

Other

module RaceAnalysis : sig ... end

Data race analysis (race).

module BasePriv : sig ... end

Non-relational thread-modular value analyses for Base.

module RelationPriv : sig ... end

Relational thread-modular value analyses for RelationAnalysis, i.e. ApronAnalysis and AffineEqualityAnalysis.

module ThreadEscape : sig ... end

Escape analysis for thread-local variables (escape).

module PthreadSignals : sig ... end

Must received signals analysis for Pthread condition variables (pthreadSignals).

module PthreadBarriers : sig ... end

Must have waited barriers for Pthread barriers (pthreadBarriers).

module ExtractPthread : sig ... end

Promela extraction analysis for Pthread programs (extract-pthread).

module PthreadOnce : sig ... end

Must active and have passed pthreadOnce calls (pthreadOnce).

Longjmp

Analyses related to longjmp and setjmp.

module ActiveSetjmp : sig ... end

Analysis of active setjmp buffers (activeSetjmp).

module ModifiedSinceSetjmp : sig ... end

Analysis of variables modified since setjmp (modifiedSinceSetjmp).

module ActiveLongjmp : sig ... end

Analysis of active longjmp targets (activeLongjmp).

module PoisonVariables : sig ... end

Taint analysis of variables that were modified between setjmp and longjmp and not yet overwritten. (poisonVariables).

module Vla : sig ... end

Analysis of variable-length arrays (VLAs) in scope (vla).

Tutorial

Analyses for didactic purposes.

module Constants : sig ... end

Simple intraprocedural integer constants analysis example (constants).

module Signs : sig ... end

Simple intraprocedural integer signs analysis template (signs).

module Taint : sig ... end

Simple interprocedural taint analysis template (taint).

module UnitAnalysis : sig ... end

Simplest possible analysis with unit domain (unit).

Other

module Assert : sig ... end

Analysis of assert results (assert).

module LoopTermination : sig ... end

Termination analysis for loops and goto statements (termination).

module Callstring : sig ... end

Call String analysis call_string and/or Call Site analysis call_site. The call string limitation for both approaches can be adjusted with the "callString_length" option. By adding new implementations of the CallstringType, additional analyses can be added.

module LoopfreeCallstring : sig ... end
module Uninit : sig ... end

Analysis of initialized local variables (uninit).

module Expsplit : sig ... end

Path-sensitive analysis according to values of arbitrary given expressions (expsplit).

module BranchSet : sig ... end

Helper analysis to be path-sensitive in set of taken branches.

module StackTrace : sig ... end

Call stack analyses (stack_trace, stack_trace_set, stack_loc).

Helper

Analyses which only support other analyses.

module AccessAnalysis : sig ... end

Analysis of memory accesses (access).

module WrapperFunctionAnalysis : sig ... end

Family of analyses which provide symbolic locations for special library functions. Provides symbolic heap locations for dynamic memory allocations and symbolic thread identifiers for thread creation (mallocWrapper, threadCreateWrapper).

module TaintPartialContexts : sig ... end

Taint analysis of variables modified in a function (taintPartialContexts).

module UnassumeAnalysis : sig ... end

Unassume analysis (unassume).

module ExpRelation : sig ... end

Stateless symbolic comparison expression analysis (expRelation).

module AbortUnless : sig ... end

Analysis of assume_abort_if_not-style functions (abortUnless).

module PtranalAnalysis : sig ... end

CIL's GoblintCil.Ptranal for function pointer evaluation (ptranal).

module StartStateAnalysis : sig ... end

Remembers the abstract address value of each parameter at the beginning of each function by adding a ghost variable for each parameter. Used by the c2po analysis.

module SingleThreadedLifter : sig ... end

This lifter takes an analysis that only works for single-threaded code and allows it to run on multi-threaded programs by returning top when the code might be multi-threaded.

Analysis lifters

Transformations of analyses into extended analyses.

module SpecLifters : sig ... end

Various simple and old analysis lifters.

module LongjmpLifter : sig ... end

Analysis lifter for longjmp and setjmp support.

module RecursionTermLifter : sig ... end

Cycle detection in the context-sensitive dynamic function call graph of an analysis.

module ContextGasLifter : sig ... end

Lifts a Spec with the context gas variable. The gas variable limits the number of context-sensitively analyzed function calls in a call stack. For every function call the gas is reduced. If the gas is zero, the remaining function calls are analyzed without context-information

module WideningDelay : sig ... end

Standard widening delay with counters.

module WideningToken : sig ... end

Widening token for WideningTokenLifter.

module WideningTokenLifter : sig ... end

Widening tokens are a generic and dynamic mechanism for delaying widening.

Domains

Domains used by analysis specifications and constraint systems are lattices.

Besides lattice operations, their elements can also be compared and output (in various formats). Those operations are specified by Printable.S.

module Printable = Printable
module Lattice = Lattice

General

Standard general-purpose domains and domain functors.

module BoolDomain = BoolDomain
module SetDomain = SetDomain
module MapDomain = MapDomain
module TrieDomain = TrieDomain
module DisjointDomain = DisjointDomain
module HoareDomain = HoareDomain
module PartitionDomain = PartitionDomain
module FlagHelper = FlagHelper

Analysis-specific

Domains for specific analyses.

Value

Non-relational

Domains for Base analysis.

Numeric
module IntDomain = IntDomain
module FloatDomain = FloatDomain
Addresses

Memory locations are identified by mvalues, which consist of a variable and an offset. Mvalues are used throughout Goblint, not just the Base analysis.

Addresses extend mvalues with NULL, unknown pointers and string literals.

module Mval = Mval
module Offset = Offset
module StringDomain = StringDomain
module AddressDomain = AddressDomain
Complex
module StructDomain = StructDomain
module UnionDomain = UnionDomain
module ArrayDomain = ArrayDomain
module NullByteSet = NullByteSet
module JmpBufDomain = JmpBufDomain
Combined

These combine the above domains together for Base analysis.

module BaseDomain : sig ... end

Full domain of Base analysis.

module ValueDomain = ValueDomain
module ValueDomainQueries = ValueDomainQueries
Relational

Domains for RelationAnalysis.

module RelationDomain : sig ... end

Signatures for relational value domains.

module ApronDomain : sig ... end

Apron domains.

module AffineEqualityDomain : sig ... end

OCaml implementation of the affine equalities domain.

module AffineEqualityDenseDomain : sig ... end

OCaml implementation of the affine equalities domain.

module LinearTwoVarEqualityDomain : sig ... end

OCaml implementation of the linear two-variable equality domain.

module CongruenceClosure : sig ... end
module UnionFind : sig ... end
module C2poDomain : sig ... end

Domain for weakly relational pointer analysis C-2PO.

Concurrency

module MutexAttrDomain = MutexAttrDomain
module LockDomain : sig ... end

Lockset domains.

module SymbLocksDomain : sig ... end

Symbolic lockset domain.

module DeadlockDomain : sig ... end

Deadlock domain.

module ThreadFlagDomain : sig ... end

Multi-threadedness flag domains.

module ThreadIdDomain = ThreadIdDomain
module ConcDomain = ConcDomain
module MHP : sig ... end

May-happen-in-parallel (MHP) domain.

module EscapeDomain : sig ... end

Domain for escaped thread-local variables.

module PthreadDomain : sig ... end

Domains for extraction of Pthread programs.

Other

module Basetype = Basetype
module Lval = Lval
module Access : sig ... end

Memory accesses and their manipulation.

module AccessDomain : sig ... end

Domain for memory accesses.

module MusteqDomain : sig ... end

Symbolic lvalue equalities domain.

module RegionDomain : sig ... end

Domains for disjoint heap regions.

module StackDomain : sig ... end

Call stack domains.

Testing

Modules related to (property-based) testing of domains.

module DomainProperties : sig ... end

QCheck properties for lattice properties.

module AbstractionDomainProperties : sig ... end

QCheck properties for abstract operations.

module IntDomainProperties : sig ... end

QCheck properties for IntDomain.

Incremental

Incremental analysis is for analyzing multiple versions of the same program and reusing as many results as possible.

module CompareCIL = CompareCIL
module CompareAST = CompareAST
module CompareCFG = CompareCFG
module UpdateCil = UpdateCil
module MaxIdUtil = MaxIdUtil
module Serialize = Serialize
module CilMaps = CilMaps

I/O

Various input/output interfaces and formats.

module Messages = Messages
module Logs = Goblint_logs.Logs

Front-end

The following modules handle program input.

module Preprocessor : sig ... end

Detection of suitable C preprocessor.

module CompilationDatabase : sig ... end

Input program from a real-world project using a compilation database.

module MakefileUtil = MakefileUtil
module TerminationPreprocessing : sig ... end

Results

module AnalysisResultOutput : sig ... end

Analysis result output.

module XsltResultOutput : sig ... end

XSLT analysis result output.

Witnesses

Witnesses are an exchangeable format for analysis results.

module Witness : sig ... end

Output of ARG as GraphML.

module Svcomp : sig ... end

SV-COMP tasks and results.

module SvcompSpec : sig ... end

SV-COMP specification strings and files.

module Invariant = Invariant
module InvariantCil = InvariantCil
module WitnessUtil : sig ... end

Utilities for witness generation and witness invariants.

YAML

Entry-based YAML witnesses to be used in SV-COMP.

module YamlWitness : sig ... end

YAML witness generation and validation.

module YamlWitnessType : sig ... end

YAML witness format types.

module YamlWitnessVersion : sig ... end

YAML witness format version.

module WitnessGhost : sig ... end

Ghost variables for YAML witnesses.

SARIF

module Sarif : sig ... end

SARIF output of Messages.

module SarifType : sig ... end

SARIF format types.

module SarifRules : sig ... end

SARIF rule definitions for Goblint.

ARG

Abstract reachability graphs (ARGs). Used to be for automaton-based GraphML witnesses used in SV-COMP, now for abstract debugging.

module MyARG : sig ... end

Abstract reachability graph.

module ArgConstraints : sig ... end

Analysis specification transformation for ARG construction.

module ArgTools : sig ... end

Construction of ARGs from constraint system solutions.

Violation

Experimental refinement with observer automata.

module Violation : sig ... end

Violation checking in an ARG.

module ViolationZ3 : sig ... end

ARG path feasibility checking using weakest precondition and Z3 (not installed!).

module ObserverAutomaton : sig ... end

Finite automaton for matching an infeasible ARG path.

module ObserverAnalysis : sig ... end

Path-sensitive analysis using an ObserverAutomaton.

module Refinement : sig ... end

Experimental analysis refinement.

Transformations

Transformations can be activated to transform the program using analysis results.

module Transform : sig ... end

Signatures and registry for transformations.

module DeadCode : sig ... end

Dead code elimination transformation (remove_dead_code).

module EvalAssert : sig ... end

Transformation for instrumenting the program with computed invariants as assertions (assert).

module ExpressionEvaluation : sig ... end

Transformation for evaluating expressions on the analysis results (expeval). Hack for Gobview.

Utilities

module Timing = Timing
module GoblintDir : sig ... end

Intermediate data directory.

General

module IntOps = IntOps
module FloatOps = FloatOps
module LazyEval = LazyEval
module ResettableLazy = ResettableLazy
module ProcessPool : sig ... end

Process pool for running processes in parallel.

module Timeout : sig ... end

Timeout utilities.

module TimeUtil : sig ... end

Date and time utilities.

module MessageUtil = MessageUtil
module AnsiColors = Goblint_logs.AnsiColors
module CodeHighlighter : sig ... end

C code highlighting.

module XmlUtil = XmlUtil
module GobExn : sig ... end

Exception utilities.

CIL

module CilType = CilType
module Cilfacade = Cilfacade
module CilLocation = CilLocation
module RichVarinfo = RichVarinfo
module DuplicateVars : sig ... end
module CilCfg : sig ... end

Creation of CIL CFGs.

module LoopUnrolling : sig ... end

Syntactic loop unrolling.

Library specification

For more precise analysis of C standard library, etc functions, whose definitions are not available, custom specifications can be added.

module AccessKind = AccessKind
module LibraryDesc = LibraryDesc
module LibraryDsl = LibraryDsl
module LibraryFunctions = LibraryFunctions

Analysis-specific

module BaseUtil : sig ... end

Basic analysis utilities.

module PrecisionUtil = PrecisionUtil
module ContextUtil = ContextUtil
module ReturnUtil : sig ... end

Special variable for return value.

module BaseInvariant : sig ... end

Analyses.Spec.branch refinement for Base analysis.

module CommonPriv : sig ... end

Thread-modular value analysis utilities for BasePriv and RelationPriv.

module WideningThresholds = WideningThresholds
module Vector : sig ... end
module Matrix : sig ... end
module ArrayVector : sig ... end
module ArrayMatrix : sig ... end
module SparseVector : sig ... end
module ListMatrix : sig ... end
module RatOps : sig ... end
module RelationCil : sig ... end

CIL utilities for relational analyses.

module SharedFunctions : sig ... end
module GobApron : sig ... end

Precision comparison

module PrecCompare : sig ... end

Precision comparison.

module PrecCompareUtil : sig ... end

Signatures for precision comparison.

module PrivPrecCompareUtil : sig ... end

BasePriv precision comparison.

module RelationPrecCompareUtil : sig ... end

RelationPriv precision comparison.

module ApronPrecCompareUtil : sig ... end

ApronDomain precision comparison.

Library extensions

OCaml library extensions which are completely independent of Goblint.

See Goblint_std.

Standard library

OCaml standard library extensions which are not provided by Batteries.

module GobFormat = GobFormat