This file gives an overview of the different components that make up the framework. The intention is to provide necessary pointers for understanding and extending the codebase. Instructions geared towards using the library can be found in the USING file instead.
| File | Description |
|---|---|
| Context.v | Variable contexts. They are used to describe both program and logic variables that are in scope. Moreover, contexts are used as just a list of types to define the fields of records, tuples, and the argument types of user-defined predicates. |
| Environment.v | Environments are mappings of variables to data like local variable stores, valuations and substitution. This is also used as the representation of tuples and of the arguments (shallow and symbolic) of predicates. |
| Bitvector.v | Contains the definition of length-indexed bitvectors and supporting functions. |
| Notation.v | Contains a non-exhaustive list of reserved notations that are used in the codebase. |
| Tactics.v | General-purpose tactics that are used in the implementation. |
| Prelude.v | General-purpose definitions around equality and finite typeclasses and automation for reasoning about the option monad. |
| Base.v | This file defines the signature of user-defined Base modules that most of the library is paremterized over. This essentially instantiates the background theory of the μSail langauge with user-defined types. |
Additionally, the availablre registers on a machine are defined in this module. The subsequent files list functionality that mixed into the Base module. |
|
| Syntax/BinOps.v | Defines the binary operations of the μSail language and their semantics. |
| Syntax/Patterns.v | Defines patterns for records, tuples and pairs and defines their pattern-matching semantics. |
| Syntax/Registers.v | Declares the signature of RegDeclKit, a subset of the Base module and a default implementation that can be used as a mixin. |
| Syntax/TypeDecl.v | This file contains the definition of records (TypeDeclKit, TypeDenoteKit, TypeDefKit) that define the user-provided enum, union and record types and gives enough information about these types to essentially perform datatype-generic programm. |
Based on this, the file defines a universe of types Ty and their values Val. |
|
| Syntax/Variables.v | This defines a Class VarKit for the representation of names which the rest of the library is parameterized over. The default implementation uses strings for both program and logic variable names. |
| Syntax/Expressions.v | Expressions are defined in this file and are one part of the stratified syntax of programs. Essentially, expressions contain everything that has no observable side effect. This does include a case for program variables. |
| Syntax/Terms.v | This file deifnes symbolic terms (also called symbolic values and symbolic expressions in the paper), which use logic variables as opposed to program variables in expressions. Furthermore, this file also defines substitutions and a plethora of infrastructure lemmas for substitutions. |
| Program.v | The signature of the user-defined Program module is defined in this file. It contains everything that would constitute a complete Sail program that is not already part of the Base module, such as the definition of functions etc. The subsequent files are included in Program. |
| Syntax/Statements.v | This file contains the definition of statements Stm, that are used to define functions, and notations for them. |
| Syntax/FunDecl.v | The FunDeclKit module defined here is a subset of the Program module that contains the signatures of μSail and foreign functions and ghost lemmas, i.e. it represents the declaration of all of these. |
| Syntax/FunDef.v | The FunDefKit module contains the user-provided definitions of functions given by statements for every μSail function and a stepping relation for foreign functions, i.e. each foreign function call evaluates in one step. Morever, FunDefKit also specifies a type that represents a machine's memory, which is given to foreign functions. |
| SmallStep/Step.v | This file defines a small-step operational semantics based on a Program module. |
| SmallStep/Inversion.v | This file contains several inversion lemmas for the multistep relation. |
| SmallStep/Progress.v | Shows the progress property for the operational semantics. Since the semantics is type-preserving by construction it effectively shows type-safety. |
| Semantics/Registers.v | Defines the state of all registers as a function from registers to values of the correct type. This is used in the step relation. |
| Signature.v | The Signature module defines the pure and spatial predicates that can be used in specifications. The subsequent files define modules that are subsets of Signature that are either user-defined or defined by the library as mixins that the user has to include. |
| Syntax/Predicates.v | Contains the signature of user-provided abstract pure and spatial predicates. Moreover, it also contains meta-information about spatial predicates such as duplicability and preciseness. |
| Syntax/Chunks.v | This file defines chunks, i.e. the elements of the abstract shallow and symbolic heaps. |
| Syntax/Formulas.v | Formulas are the representation of pure symbolic propositions used in contracts. This includes user-defined predicates. It also includes enough cases to represent the constraints of every possible control flow branch of programs. |
| Syntax/Assertions.v | The Assertion language defines structured propositions that are used to define the pre- and postconditions of function contracts. It has chunks and formulas as base cases but also allows for structured ifs and pattern matching. |
| Specification.v | The Specification module defined here contains all the user-provided contracts (triples) for function and ghost lemmas. |
| Sep/Logic.v | This file contains a structure that represents a shallowly-embedded type of seperation logic propositions together with its logical connectives and laws for all the connectives. Furthermore, we derive some laws. |
| Sep/Hoare.v | This contains the axiomatic program logic for a given Program defined by a set of rules for triples. |
| Shallow/Executor.v | This contains the definition of the shallow version of the pure predicate transformer monads and its state-transformed variant. This is then used to define the executor for statements and assertions from which a shallow verfication condition generator (VCG) is derived. |
| Shallow/Soundness.v | This contains the soundness lemma of the shallow VCG w.r.t. the axiomatic program logic. |
| Symbolic/Propositions.v | This defines symbolic propositions, i.e. the propositions that are constructed by the symbolic executor / VCG. This is the type of propositions that is later used to define the symbolic predicate transformer monads. Furthermore, this file contains the simplifications that make up the postprocessing phase. |
| Symbolic/PartialEvaluation.v | This file defines "partial evaluation" of symbolic terms that is used in the executor and the solver. This currently consists mainly of constant foldings and some simple rewrites for (incomplete) canonicalization. |
| Symbolic/OccursCheck.v | Defines an occurs check for every piece of symbolic data. This is used by the solver to turn variable equations into substitutions. |
| Symbolic/Solver.v | Defines a generic solver for some of the background theory of a Base. It is very incomplete but takes care of the bulk of proof obligations. Currently, it provides functionality that is comparable to inversion, discriminate, reflexivity, assumption, subst and contains some rewrites that encode computation steps for some of the binops. |
| This is augmented by another solver that the user defines for his own predicates and ad-hoc cases not covered by the generic solver. | |
| symbolic/Worlds.v | This defines the kripke worlds used to structure computations that depend on allocated logic variables and in the context of a set of path constraints. It also defines the accessibility relation between worlds. |
| symbolic/Executor.v | The symbolic version of the executor and VCG are defined in here. |
| Symbolic/Soundness.v | Contains the definition of the logical relation used to prove soundness of the symbolic VCG w.r.t. to the shallow one. It then goes on to show this soundness by relating all symbolic and shallow definitions. |
| Iris/Model.v | This file contains a model of the axiomatic program logic implemented using the Iris separation logic framework. This file defines only the operational model that is independent of a specific sets of contracts. The model itself is parameterized over parts that the user needs to define or prove. See USING.md and the file itself. |
| Iris/Logic.v | This file defines the remainder of the Iris model that is dependent on the user-defined predicates and function contracts. It can be instantiated multiple times to use the same base operational model with multiple different sets of contracts. |
The framework extensively uses Coq modules for parametrization, which has several tradeoffs.
The downside is the general complexity of the modules, their duck-typed nature, and the fact that they are second-class.
The benefits include that hiding parameters even when using Set Printing Implicit.
We currently consider the modules a necessary evil because they help (or rather seem to help because I don't fully understand their impact) with the performance of the executors.
Essentially, putting definitions into a module as opposed to a dependent record that is passed around delays delta expansion of the fields of the module.
There is currently no other way to control evaluation order in this fashion.
A downside of the approach is a larger memory footprint of the library.
To remedy this, we have started moving parts of the library out of the modules and into records instead.
See, for example, the TypeDeclKit, TypeDenoteKit and TypeDefKit of the Base module.
However, this is fragile, and subsequent changes to the module / record hierarchy should be evaluated for their impact on running time.
For instance, merging TypeDenoteKit and TypeDefKit results in a 1.3x slowdown which is still acceptable, but merging all three of the Type*Kits results in a 10x slowdown.
We make heavy use of the stdpp and equations library. Sometimes the notations defined in these libraries clash, so we prefer to import them in sections selectively.
A huge downside of the stdpp library is that many of the definitions are opaque and supposed to be used in combination with vm_compute.
For some reason, in most cases, when we run our symbolic executor, vm_compute is slower than compute (and vm_compute; reflexivity slower than reflexivity).
Therefore, we are currently avoiding using stdpp in the context of symbolic execution when an opaque definition could block computation.
The library is currently axiom-free (not even fun.ext. or prop.ext.). So try to keep it that way and avoid introducing axioms when possible. But let's be pragmatic; if there is a good reason to assume an axiom, we allow it.