Data.SBV.Program

This module implements an algorithm described in the "Component-based Synthesis Applied to Bitvector Programs" paper.

https://www.microsoft.com/en-us/research/wp-content/uploads/2010/02/bv.pdf

Given a program specification along with a library of available components it synthesizes an actual program using an off-the-shelf SMT-solver.

The specification is an arbitrary datatype that is an instance of the SynthSpec class. The library is a list of SynthComponent instances.

There are three entry points to this module: standardExAllProcedure, refinedExAllProcedure and exAllProcedure.

Definitions for specification and component classes and the resulting data type

module Data.SBV.Program.Types

Predefined components library

module Data.SBV.Program.SimpleLibrary

Various utility functions

module Data.SBV.Program.Utils

Package entry points

standardExAllProcedure

Arguments

:: forall a comp spec. (SymVal a, Show a, SynthSpec spec a, SynthComponent comp spec a)

=> [comp a]

Component library

-> spec a

Specification of program being synthesized

-> IO (Either SynthesisError (Program Location (comp a)))

An implementation of StandardExAllSolver presented in section 6.1 of the paper. As stated in the paper, this implementation boils down to exhaustive enumeration of possible solutions, and as such isn't effective. It can be used to better understand how the synthesis procedure works and provides a lot of debugging output. Do not use this procedure for solving real problems.

refinedExAllProcedure

Arguments

:: forall a comp spec. (SymVal a, SynthSpec spec a, SynthComponent comp spec a)

=> [comp a]

Component library

-> spec a

Specification of program being synthesized

-> IO (Either SynthesisError (Program Location (comp a)))

An implementation of RefinedExAllSolver presented in section 6.2 of the paper. This is an improved version of standardExAllProcedure. It only keeps input values \(|\vec I|\) in \(S\) and uses different synthesis constraints on synthesis and verification steps.

exAllProcedure

Arguments

:: forall a comp spec. (SymVal a, SynthSpec spec a, SynthComponent comp spec a)

=> [comp a]

Component library

-> spec a

Specification of program being synthesized

-> IO (Either SynthesisError (Program Location (comp a)))

This procedure is not part of the paper. It uses forall quantification directly when creating variables from the \(T\) set. As consequence it requires an SMT-solver than can handle foralls (for instance, Z3). This procedure is the easiest to understand.

Auxiliary functions that make up synthesis procedures

createProgramLocs :: forall a comp spec. (SymVal a, SynthSpec spec a, SynthComponent comp spec a) => [comp a] -> Word -> Symbolic (Program SLocation (comp a))

First step of each synthesis procedure. Given a library of components and a number of program's inputs, it creates existentially quantified location variables (members of set \(L\) in the paper) for each component and for the program itself.

constrainLocs

Arguments

:: (SynthSpec spec a, SynthComponent comp spec a)

=> Word

The \(M\) constant from the paper, which equals to \(N + |\vec I|\), where N is the size of the library.

-> Word

Number of program inputs \(|\vec I|\).

-> Program SLocation (comp a)

-> Symbolic ()

Second step of each synthesis procedure. It applies constraints on location variables from section 5 of the original paper. These constraints include well-formedness constraint \(ψ_{wfp}\), acyclicity constraint \(ψ_{acyc}\) and consistency constraint \(ψ_{cons}\). Constraints are not returned from this function, but are applied immediately. Section 5 of the paper also talks about connectivity constraint \(ψ_{conn}\), which is not created here.

createProgramVarsWith

Arguments

:: forall a comp spec. (SymVal a, SynthSpec spec a, SynthComponent comp spec a)

=> (String -> Symbolic (SBV a))

Variable creation function. Either sbvExists or sbvForall.

-> [comp a]

Component library.

-> Word

Number of program inputs \(|\vec I|\).

-> Symbolic (Program (SBV a) (comp a))

Third step of the synthesis process. It creates variables that represent actual inputs/outputs values (members of the set \(T\) in the paper). This function resembles createProgramLocs, but unlike it allows creating both existentially and universally quantified variables. Standard and Refined procedures pass sbvExists to create existentially quantified variables, while exAllProcedure uses sbvForall.

createVarsConstraints :: SynthComponent comp spec a => Program SLocation (comp a) -> Program (SBV a) (comp a) -> (SBool, SBool)

Last building block of the synthesis process. This function creates \(ψ_{conn}\) and \(φ_{lib}\) constraints and return them.