Kind 2 Developer's Documentation

Developers' Documentation

Overall system architecture.

Configuration

• Flags Parsing of command line arguments

Communication and Logging

• Log Logging and messaging
• KEvent Event logging and communication

Analysis and Strategies

• Strategy A strategy returns an Analysis.param option which is None if done. It takes
• Analysis Interface between strategy and low-level analysis
• InvarManager Invariant manager
• PostAnalysis
• Kind2Flow

Terms

• Decimal Arbitrary precision real numbers
• Numeral Arbitrary precision integers
• Hexadecimal Arbitrary precision hexa-decimals
• Bitvector Bit-vectors
• Symbol Kind's symbols
• Type Types of terms
• UfSymbol Uninterpreted function symbols
• StateVar State variables
• Var Variables in terms
• Ident Managing of identifier to avoid clashes
• Ltree Abstract syntax trees with binders and quantifiers
• TermAttr Attributes for annotated terms
• Term Term representation
• Model
• Eval Term evaluator

Transition System Construction

• Scope Managing of scopes to avoid clashes
• InputSystem Delegate to concrete functions for input formats.
• Property
• Invs Invariants are stored in two hash tables mapping them to their certificate. One table is for one-state invariants, the other is for two-state invariants.
• SubSystem Abstract system
• TransSys Representation of a transition system
• Simplify Term simplifier
• ModelElement Manpulation of sets of equations and model elements (equations, assertions, assumptions, guarantees, node calls). Make the link between TransSys-level equations and Lustre model elements.

Verification Engines

k-induction

• Actlit
• Base
• Compress Path compression for k-induction
• Step
• Step2

IC3

• Clause Clause, properties and activation literals for IC3
• CooperQE Cooper quantifier elimination
• Extract Extract an active path from a formula given a model
• IC3 Property-directed reachability (aka IC3)
• Poly Polynomials
• Presburger Conversions from and to Presburger arithmetic formulas
• QE Quantifier elimination

Invariant Generators

Implication Graph-based Invariant Generation

• InvGenDomain
• InvGenMiner
• LockStepDriver Lock Step Driver (LSD).
• InvGenGraph Graph representing equivalence classes and ordering between some terms.
• InvGen Generic invariant generation.

C2I (machine-learning based invariant generation)

• C2I C2I is a machine-learning-based invariant generation technique.
• C2ICandidate Wraps the candidate invariants with info about their cost etc.
• C2Imodel Handles models for the C2I algorithm.

Interpreter

• InputParser
• Interpreter Interpreter for Lustre programs

Input Modules

Lustre

Source files live in the subdirectory lustre

Dependency graph of modules

• LustreLexer Lexer for Lustre input
• LustreParser
• LustreAst Minimally simplified Lustre abstract syntax tree
• LustreAstHelpers Some helper functions on the surface level parsed AST
• LustreAstDependencies Graph analysis on Lustre Ast Declarations.
• TypeCheckerContext The type checker context used for typechecking the surface level language
• LustreTypeChecker Functions for type checking surface syntax LustreAst
• LustreIdent Lustre identifier
• LustreIndex Indexes for lists, records, tuples and arrays in Lustre
• LustreExpr Internal reperesentation of a Lustre expression
• LustreNode Internal representation of a Lustre node
• LustreContract
• LustreGlobals Global declarations for Lustre input
• LustreSlicing Cone of influence reduction and dependency ordering of equations
• LustreTransSys
• LustreInput Parse Lustre input into the intermediate Lustre format
• LustrePath Conversion of a counterexample to a Lustre model
• LustreDesugarIfBlocks Code for desugaring imperative-style if blocks to functional ITEs.
• LustreDesugarFrameBlocks This file desugars frame blocks into a list of node items (equations), completing two major steps: 1. Fill in any oracles within the frame block (for unguarded pres or undefined variables in if blocks). 2. Generate node equations for variables left completely undefined in frame blocks.

Native

Source files live in subdirectory nativeInput

• NativeInput Parse a file in native input format into a transition system

SMT Solver Interface

Source files live in subdirectory SMTSolver

• SMTExpr Datatypes and helper function for the SMT solver interface
• SMTLIBSolver An interface to any SMT solver that accepts the SMTLIB2 command language
• SMTSolver High-level methods for an SMT solver
• SolverDriver
• SolverResponse
• SolverSig

SMTLIB Interface

• GenericSMTLIBDriver
• CVC5Driver
• BitwuzlaDriver
• MathSATDriver
• Yices2SMT2Driver
• Z3Driver

Yices Interface

• YicesDriver
• YicesLexer
• YicesParser
• YicesNative An interface to the Yices SMT solver in native format.
• YicesResponse

S-expressions

• HStringSExpr
• SExprBase S-Expressions
• SExprLexer Lexer: Lexer Specification for S-expressions
• StringSExpr S-Expressions over string atoms

Inductive Validity Cores / Minimal Cut Sets

• IvcMcs Computation of Inductive Validity Cores and Maximal Unsafe Abstractions / Minimal Cut Sets

Contract Checker

• ContractChecker Checking of realizability of contracts and other sanity checks over contracts

Test generation

• TestgenDF
• TestgenIO
• TestgenModes
• TestgenSolver Wraps a solver and provides a convenient interface for test generation.
• TestgenTree

Proof certificates

• Certificate Certificates for Kind 2. This contains the base type as well as some combinators for certificates.
• CertifChecker
• Proof

Contract Generation and Translation

• LustreContractGen
• ContractsToProps

Utilities

• Lib General-purpose library functions
• Res
• Debug Debug ouput, controlled by Flags.
• FileId
• Hashcons Hash tables for hash consing
• HashconsWeak Hash tables for hash consing
• HashconsStrong Hash tables for hash consing
• HString Perfect shared strings by hashconsing
• Messaging Low-level handling of messages between the supervisor and the engines of an analysis.
• Pretty Functions for pretty ascii output (colors, etc.)
• Stat Statistics
• TermLib Utilty functions for transition systems
• Graph A poor person's directed graph and some graph traversal implementations
• Trie Trie over lists of values
• Version Static and autoconfigured defaults
• Unroller Very basic helper functions for unrolling. More precisely, asserting one- and two-state invariants.
• JkindParser Extract the transition system from the dumpfiles of jKind

Howto

Documentation

To add a module, edit this file src/doc/index.mld and add it to one of the sections above.