Kind 2 Developer's Documentation

Developers' Documentation

Overall system architecture.

Configuration


Flags
Parsing of command line arguments

Communication and Logging


Log
Logging and messaging
Event
Event logging and communication

Analysis and Strategies


Strategy
A strategy returns an Analysis.param option which is None if done.
Analysis
Interface between strategy and low-level analysis
InvarManager
Invariant manager
PostAnalysis
Signature of modules for post-analysis treatment.
Kind2Flow
Runs the analyses produced by the strategy module.
Kind2
Top level of the Kind 2 model-checker.

Terms


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
Term or lambda expression
Eval
Term evaluator

Transition System Construction


Scope
Managing of scopes to avoid clashes
InputSystem
Delegate to concrete functions for input formats.
Property
Current status of a property
SubSystem
Abstract system
TransSys
Representation of a transition system
Simplify
Term simplifier

Verification Engines

k-induction


Actlit
Creates a fresh actlit as a bool UF constant.
Base
Clean up before exit
Compress
Path compression for k-induction
Step
Clean up before exit

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
Exception thrown when a domain is asked to build a trivial implication.
InvGenMiner
Module generating candidate terms for invariant generation.
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
C2ICandidate
C2Icnf
C2Imodel

Interpreter


InputParser
Parser for a CSV input file
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
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
LustreContext
Context information used in and obtained from parsing
LustreContract
Wraps a state variable for use in a contract.
LustreDeclarations
Convert a Lustre abstract syntax tree to an intermediate Lustre model
LustreSimplify
Simplify a Lustre AST to normalized Lustre nodes
LustreSlicing
Cone of influence reduction and dependency ordering of equations
LustreTransSys
Convert a Lustre node to a transition system
LustreInput
Parse Lustre input into the intermediate Lustre format
LustrePath
Conversion of a counterexample to a Lustre model

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
Solver configuration options
SolverResponse
Solver commands and responses
SolverSig
Solver paramters

SMTLIB Interface


CVC4Driver
GenericSMTLIBDriver
MathSAT5Driver
Z3Driver

Yices Interface


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

Lustre to Rust


LustreToRust
Compilation from LustreNode.t to Rust.

Test generation


TestgenDF
Prefix for logging testgen related things.
TestgenIO
Stores IO things to log testcases to xml.
TestgenModes
TestgenSolver
Wraps a solver and provides a convenient interface for test generation.
TestgenStrategies
Gathers the contracts, the actions a strategy can perform on the underlying smt solver used for test generation, and some data a strategy generates tests from.
TestgenTree
A depth is just a numeral.
TestgenLib
Turns an actlit uf in a term.

Utilities


Lib
General-purpose library functions
Res
A result for some type.
Debug
Debug ouput, controlled by Flags.
Decimal
Arbitrary precision real numbers
Hashcons
Hash tables for hash consing
HString
Perfect shared strings by hashconsing
HStringSExpr
Kind2Config
Messaging
Low-level handling of messages
Numeral
Arbitrary precision integers
Pretty
Functions for pretty ascii output (colors, etc.)
SExprBase
S-Expressions
SExprLexer
Lexer: Lexer Specification for S-expressions
Stat
Statistics
TermLib
Utilty functions for transition systems
Trie
Trie over lists of values
Version
Static and autoconfigured defaults
Unroller
Very basic helper functions for unrolling.

Howto

Documentation

Edit this file doc/doc_into.txt and add the module to one section above in, then add it to kind2.odocl.

Add a new subdirectory

To add a new subdirectory feature edit the _tags file to include the line

<feature>: include

Indexes