diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,9 @@ +Copyright (c) 2023 Gleb Popov <6yearold@gmail.com>. + +Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: + + 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. + 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. + 3. Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,11 @@ +# Component-based synthesis of loop-free programs + +This package implements a library for synthesizing programs as described in the +[Component-based Synthesis Applied to Bitvector Programs](https://www.microsoft.com/en-us/research/wp-content/uploads/2010/02/bv.pdf) paper. +It uses an off-the-shelf SMT solver via [sbv](https://hackage.haskell.org/package/sbv) library. + +See [Examples.hs](https://github.com/arrowd/sbv-program/blob/master/src/Data/SBV/Program/Examples.hs) file to quickly get at how to use this. +For deeper understanding of library's internals see the Haddock documentation. + +The code is structured and commented in such way that it follows variable naming +of the original paper. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/sbv-program.cabal b/sbv-program.cabal new file mode 100644 --- /dev/null +++ b/sbv-program.cabal @@ -0,0 +1,51 @@ +cabal-version: >= 1.10 + +name: sbv-program +version: 1.0.0.0 +category: SMT, Symbolic Computation, Bit vectors, Formal Methods +synopsis: Component-based program synthesis using SBV +description: Given a library of available componen functions, synthesize a program implementing a specification. +homepage: https://github.com/arrowd/sbv-program +bug-reports: https://github.com/arrowd/sbv-program/issues +author: Gleb Popov +maintainer: 6yearold@gmail.com +copyright: 2023 Gleb Popov +license: BSD3 +license-file: LICENSE +build-type: Simple +extra-source-files: + README.md + +source-repository head + type: git + location: https://github.com/arrowd/sbv-program + +library + exposed-modules: + Data.SBV.Program + Data.SBV.Program.Examples + Data.SBV.Program.SimpleLibrary + Data.SBV.Program.Types + Data.SBV.Program.Utils + hs-source-dirs: + src + build-depends: + base < 5 + , bifunctors + , containers + , pretty-simple + , sbv + default-extensions: + RecordWildCards + default-language: Haskell2010 + +test-suite smoketest + hs-source-dirs: + test + main-is: SmokeTest.hs + build-depends: + base + , sbv + , sbv-program + type: exitcode-stdio-1.0 + default-language: Haskell2010 diff --git a/src/Data/SBV/Program.hs b/src/Data/SBV/Program.hs new file mode 100644 --- /dev/null +++ b/src/Data/SBV/Program.hs @@ -0,0 +1,387 @@ +-- +-- | 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'. +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE RecordWildCards #-} + +module Data.SBV.Program ( + -- * 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 #entry# + + standardExAllProcedure, + refinedExAllProcedure, + exAllProcedure, + + -- * Auxiliary functions that make up synthesis procedures #aux# + + createProgramLocs, + constrainLocs, + createProgramVarsWith, + createVarsConstraints, + ) +where + +import Control.Monad +import Control.Monad.IO.Class +import Data.Either +import Data.Foldable +import Data.List +import Data.Maybe +import Data.Ord (comparing) +import Data.Traversable (for) +import Data.SBV hiding (STuple) +import Data.SBV.Control + +import Data.SBV.Program.SimpleLibrary +import Data.SBV.Program.Types +import Data.SBV.Program.Utils + +import Text.Pretty.Simple (pPrint) + + +-- | Represents a failed run in 'standardExAllProcedure'. Corresponds to +-- __program variable__ \(S\) in the paper. +data STuple a = STuple { + s_ios :: IOs a, + s_comps :: [IOs a] + } + deriving Show + + +-- | 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. +standardExAllProcedure :: forall a comp spec . + (SymVal a, Show a, SynthSpec spec a, SynthComponent comp spec a) => + -- | Component library + [comp a] + -- | Specification of program being synthesized + -> spec a + -> IO (Either SynthesisError (Program Location (comp a))) +standardExAllProcedure library spec = do + -- generate a seed for S + mbRes <- sampleSpec spec + case mbRes of + Nothing -> return $ Left ErrorSeedingFailed + Just i0 -> do + putStrLn "Seeding done, result:" + print i0 + go 1 [STuple (i0 :: IOs a) []] + where + n = genericLength library + numInputs = specArity spec + m = n + numInputs + go step s = do + putStrLn "=============" + putStrLn "Synthesizing with s = " + pPrint s + -- Finite synthesis part + r <- runSMT $ do + progLocs <- createProgramLocs library numInputs + + constrainLocs m numInputs progLocs + + -- Unlike 'exAllProcedure' we call 'createProgramVarsWith' here multiple times + -- Since we aren't using forall quantifier, we have to create variables + -- for each STuple item in s. + manyProgVars <- forM s $ \(STuple {..}) -> do + let numInputs = genericLength $ _ins s_ios + progVars <- createProgramVarsWith sbvExists library numInputs + + -- pin input/output variables (members of I and O sets) to values from S + constrain $ fmap literal s_ios .== programIOs progVars + -- on the first run we don't have values for component locations (members of T set in the paper) + unless (null s_comps) $ + constrain $ map (fmap literal) s_comps .== map instructionIOs (programInstructions progVars) + + return progVars + + forM_ manyProgVars $ \progVars -> do + let (IOs inputVars outputVar) = programIOs progVars + (psi_conn, phi_lib) = createVarsConstraints progLocs progVars + constrain $ (phi_lib .&& psi_conn) .=> specFunc spec inputVars outputVar + + query $ do + r <- checkSat + case r of + Sat -> do + solution <- mapM getValue (programIOs progLocs) + componentLocVals <- traverse (bimapM getValue pure) (programInstructions progLocs) + return $ Right (Program solution componentLocVals) + Unsat -> return $ Left ErrorUnsat + Unk -> Left . ErrorUnknown . show <$> getUnknownReason + -- Verification part + -- At this stage the 'currL' program represents a solution that is known to + -- work for all values from S. We now check if this solution works for all + -- values possible. + fmap join $ for r $ \currL -> runSMT $ do + liftIO $ do + putStrLn "Synthesis step done, current solution:" + putStrLn $ writePseudocode currL + + progLocs <- createProgramLocs library numInputs + + -- In the verification part we pin location variables L + constrain $ (literal <$> programIOs currL) .== programIOs progLocs + constrain $ sAnd $ zipWith (\x y -> literal x .== y) (concatMap (toList .instructionIOs) (programInstructions currL)) (concatMap (toList .instructionIOs) (programInstructions progLocs)) + + progVars <- createProgramVarsWith sbvExists library numInputs + + let Program (IOs inputVars outputVar) componentVars = progVars + (psi_conn, phi_lib) = createVarsConstraints progLocs progVars + + constrain $ sNot $ (phi_lib .&& psi_conn) .=> specFunc spec inputVars outputVar + + query $ do + r <- checkSat + io $ putStrLn "Verification step done" + case r of + Unsat -> do + io $ do + putStrLn "=============" + putStrLn ("Solution found after " ++ show step ++ " iterations") + return $ Right currL + Sat -> do + io $ putStrLn "Solution does not work for all inputs" + inputVals <- mapM getValue inputVars + outputVal <- getValue outputVar + componentVals <- mapM (traverse getValue . instructionIOs) componentVars + io $ go (step + 1) $ STuple (IOs inputVals outputVal) componentVals : s + + +-- | 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. +refinedExAllProcedure :: forall a comp spec . + (SymVal a, SynthSpec spec a, SynthComponent comp spec a) => + -- | Component library + [comp a] + -- | Specification of program being synthesized + -> spec a + -> IO (Either SynthesisError (Program Location (comp a))) +refinedExAllProcedure library spec = do + mbRes <- sampleSpec spec + case mbRes of + Nothing -> return $ Left ErrorSeedingFailed + Just r -> go 1 ([_ins r] :: [[a]]) + where + n = genericLength library + numInputs = specArity spec + m = n + numInputs + go step s = do + -- Finite synthesis part + r <- runSMT $ do + progLocs <- createProgramLocs library numInputs + + constrainLocs m numInputs progLocs + + -- Unlike 'exAllProcedure' here we call 'createProgramVarsWith' multiple times + -- Since we aren't using forall quantifier, we have to create variables + -- for each I vector in s. + manyProgVars <- forM s $ \inputVars_s -> do + let numInputs = genericLength inputVars_s + progVars <- createProgramVarsWith sbvExists library numInputs + + -- pin input variables (members of I set) to values from S + constrain $ fmap literal inputVars_s .== _ins (programIOs progVars) + + return progVars + + forM_ manyProgVars $ \progVars -> do + let (IOs inputVars outputVar) = programIOs progVars + (psi_conn, phi_lib) = createVarsConstraints progLocs progVars + constrain $ (phi_lib .&& psi_conn) .&& specFunc spec inputVars outputVar + + query $ do + r <- checkSat + case r of + Sat -> Right <$> bitraverse getValue pure progLocs + _ -> return $ Left ErrorUnsat + -- Verification part + -- At this stage the 'currL' program represents a solution that is known to + -- work for all values from S. We now check if this solution works for all + -- values possible. + fmap join $ for r $ \currL -> runSMT $ do + progLocs <- createProgramLocs library numInputs + + -- In the verification part we pin location variables L + constrain $ (literal <$> programIOs currL) .== programIOs progLocs + constrain $ sAnd $ zipWith (\x y -> literal x .== y) (concatMap (toList .instructionIOs) (programInstructions currL)) (concatMap (toList .instructionIOs) (programInstructions progLocs)) + + progVars <- createProgramVarsWith sbvExists library numInputs + + let (Program (IOs inputVars outputVar) componentVars) = progVars + (psi_conn, phi_lib) = createVarsConstraints progLocs progVars + + constrain $ (phi_lib .&& psi_conn) .&& sNot (specFunc spec inputVars outputVar) + + query $ do + r <- checkSat + case r of + Unsat -> return $ Right currL + Sat -> do + inputVals <- mapM getValue inputVars + outputVal <- getValue outputVar + componentVals <- mapM (traverse getValue . instructionIOs) componentVars + io $ go (step + 1) $ inputVals : s + +-- | 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. +exAllProcedure :: forall a comp spec . + (SymVal a, SynthSpec spec a, SynthComponent comp spec a) => + -- | Component library + [comp a] + -- | Specification of program being synthesized + -> spec a + -> IO (Either SynthesisError (Program Location (comp a))) +exAllProcedure library spec = + -- run SBV with 'allowQuantifiedQueries' to silence warnings about entering + -- 'query' mode in presence of universally quantified variables + runSMTWith (defaultSMTCfg {allowQuantifiedQueries = True}) $ do + let n = genericLength library + numInputs = specArity spec + m = n + numInputs + + progLocs <- createProgramLocs library numInputs + + constrainLocs m numInputs progLocs + + progVars <- createProgramVarsWith sbvForall library numInputs + + let (Program (IOs inputVars outputVar) _) = progVars + (psi_conn, phi_lib) = createVarsConstraints progLocs progVars + + constrain $ (phi_lib .&& psi_conn) .=> specFunc spec inputVars outputVar + + query $ do + r <- checkSat + case r of + Sat -> do + inputLocVals <- mapM getValue (_ins $ programIOs progLocs) + outputLocVal <- getValue (_out $ programIOs progLocs) + componentLocVals <- traverse (bimapM getValue pure) (programInstructions progLocs) + return $ Right $ Program (IOs inputLocVals outputLocVal) (sortOn (_out . instructionIOs) componentLocVals) + Unsat -> return $ Left ErrorUnsat + Unk -> do + reason <- getUnknownReason + return $ Left $ ErrorUnknown $ "Unknown: " ++ show reason + + +-- | 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. +createProgramLocs :: forall a comp spec . (SymVal a, SynthSpec spec a, SynthComponent comp spec a) => [comp a] -> Word -> Symbolic (Program SLocation (comp a)) +createProgramLocs library numInputs = do + inputLocs <- mapM sbvExists $ genericTake numInputs ["InputLoc" ++ show i | i <- [1..]] :: Symbolic [SLocation] + outputLoc <- sbvExists "OutputLoc" :: Symbolic SLocation + + componentsWithLocs <- forM library $ \component -> do + let n' = specArity $ compSpec component + compInputLocs <- mapM sbvExists $ genericTake n' [mkInputLocName (compName component) i | i <- [1..]] + compOutputLoc <- sbvExists $ mkOutputLocName $ compName component + return $ Instruction (IOs compInputLocs compOutputLoc) component :: Symbolic (Instruction SLocation (comp a)) + + return $ Program (IOs inputLocs outputLoc) componentsWithLocs + + +-- | 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. +constrainLocs :: (SynthSpec spec a, SynthComponent comp spec a) => + -- | 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|\). + -> Word + -> Program SLocation (comp a) -> Symbolic () +constrainLocs m numInputs (Program {..}) = do + -- program inputs are assigned locations from 0 to numInputs + forM_ (zip [0..] (_ins programIOs)) $ \(i, inputLoc) -> do + constrain $ inputLoc .== literal i + -- program output location should not be greater than the number of instructions + constrain $ _out programIOs .< fromIntegral m + + forM_ programInstructions $ \(Instruction (IOs compInputLocs compOutputLoc) comp) -> do + forM_ compInputLocs $ \inputLoc -> do + -- psi_wfp for component inputs + constrain $ inputLoc .>= literal 0 + constrain $ inputLoc .<= literal (fromIntegral $ m-1) + -- psi_acyc + constrain $ inputLoc .< compOutputLoc + + -- psi_wfp for component outputs + constrain $ compOutputLoc .>= literal (fromIntegral numInputs) + constrain $ compOutputLoc .<= literal (fromIntegral $ m-1) + + -- extra constraints supplied by user + forM_ (extraLocConstrs comp) $ \extraConstr -> + constrain $ extraConstr compInputLocs compOutputLoc + + -- psi_cons + constrain $ distinct $ map (_out . instructionIOs) programInstructions + + +-- | 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'. +createProgramVarsWith :: forall a comp spec . (SymVal a, SynthSpec spec a, SynthComponent comp spec a) => + -- | Variable creation function. Either 'sbvExists' or 'sbvForall'. + (String -> Symbolic (SBV a)) + -- | Component library. + -> [comp a] + -- | Number of program inputs \(|\vec I|\). + -> Word + -> Symbolic (Program (SBV a) (comp a)) +createProgramVarsWith sbvMakeFunc library numInputs = do + inputVars <- mapM sbvMakeFunc $ genericTake numInputs ["Input" ++ show i | i <- [1..]] + outputVar <- sbvMakeFunc "Output" + + componentVars <- forM library $ \comp -> do + let n' = specArity $ compSpec comp + compInputVars <- mapM sbvMakeFunc $ genericTake n' [mkInputVarName (compName comp) i | i <- [1..]] + compOutputVar <- sbvMakeFunc $ mkOutputVarName $ compName comp + return $ Instruction (IOs compInputVars compOutputVar) comp + + return $ Program (IOs inputVars outputVar) componentVars + + +-- | Last building block of the synthesis process. This function creates +-- \(ψ_{conn}\) and \(φ_{lib}\) constraints and return them. +createVarsConstraints :: SynthComponent comp spec a => Program SLocation (comp a) -> Program (SBV a) (comp a) -> (SBool, SBool) +createVarsConstraints progLocs progVars = (psi_conn, phi_lib) + where + allVarsWithLocs = zip (toIOsList progVars) (toIOsList progLocs) + psi_conn = sAnd [(xLoc .== yLoc) .=> (x .== y) | (x, xLoc) <- allVarsWithLocs, (y, yLoc) <- allVarsWithLocs] + phi_lib = sAnd $ flip map (programInstructions progVars) $ + \(Instruction (IOs inputVars outputVar) comp) -> specFunc (compSpec comp) inputVars outputVar + diff --git a/src/Data/SBV/Program/Examples.hs b/src/Data/SBV/Program/Examples.hs new file mode 100644 --- /dev/null +++ b/src/Data/SBV/Program/Examples.hs @@ -0,0 +1,34 @@ +module Data.SBV.Program.Examples( + -- * Reset most significant set bit + paperRunningExampleSpec, + paperRunningExample, + -- * Quadratic equation + quadEquExampleSpec, + quadEquExample +) where + +import Data.List + +import Data.SBV +import Data.SBV.Program +import Data.SBV.Program.SimpleLibrary as Lib + +-- | A running example from the original paper. The function should reset the +-- least significant set bit of a 8-byte word: +-- >>> 0001 0010 -> 0000 0010 +paperRunningExampleSpec :: SimpleSpec Word8 +paperRunningExampleSpec = SimpleSpec 1 $ \[i] o -> sAnd $ flip map [7,6..0] $ \t -> + (sTestBit i t .&& sAnd (flip map [t-1,t-2..0] $ \j -> sNot $ sTestBit i j)) + .=> + (sNot (sTestBit o t) .&& sAnd (flip map (t `delete` [7,6..0]) $ \j -> sTestBit i j .== sTestBit o j)) + +paperRunningExample = refinedExAllProcedure [Lib.and, Lib.dec] paperRunningExampleSpec + +-- | Synthesizes a formula for the quadratic equation \(x^2 - 2*x + 1 = 0\) +quadEquExampleSpec :: SimpleSpec Int32 +quadEquExampleSpec = SimpleSpec 1 $ \[i] o -> sAnd [ + i .== 1 .=> o .== 0, + i .== 4 .=> o .== 9 + ] + +quadEquExample = refinedExAllProcedure [Lib.mul, Lib.add, Lib.sub, Lib.inc] quadEquExampleSpec diff --git a/src/Data/SBV/Program/SimpleLibrary.hs b/src/Data/SBV/Program/SimpleLibrary.hs new file mode 100644 --- /dev/null +++ b/src/Data/SBV/Program/SimpleLibrary.hs @@ -0,0 +1,58 @@ +module Data.SBV.Program.SimpleLibrary( + -- * Arithmetic components + inc, + dec, + add, + sub, + mul, + + -- * Bitwise logic components + Data.SBV.Program.SimpleLibrary.and, + Data.SBV.Program.SimpleLibrary.or, + Data.SBV.Program.SimpleLibrary.not, + + -- * Logic components + bXor, + bEquiv + ) +where + +import Data.SBV +import Data.SBV.Program.Types + + +inc :: (SymVal a, Ord a, Num a) => SimpleComponent a +inc = SimpleComponent "inc" $ SimpleSpec 1 $ \[i] o -> o .== (i+1) + +dec :: (SymVal a, Ord a, Num a) => SimpleComponent a +dec = SimpleComponent "dec" $ SimpleSpec 1 $ \[i] o -> o .== (i-1) + +add :: (SymVal a, Ord a, Num a) => SimpleComponent a +add = SimpleComponent "add" $ SimpleSpec 2 $ \[i1,i2] o -> o .== (i1 + i2) + +sub :: (SymVal a, Ord a, Num a) => SimpleComponent a +sub = SimpleComponent "sub" $ SimpleSpec 2 $ \[i1,i2] o -> o .== (i1 - i2) + +mul :: (SymVal a, Ord a, Num a) => SimpleComponent a +mul = SimpleComponent "mul" $ SimpleSpec 2 $ \[i1,i2] o -> o .== (i1 * i2) + + +and :: (SymVal a, Ord a, Num a, Bits a) => SimpleComponent a +and = SimpleComponent "and" $ SimpleSpec 2 $ \[i1,i2] o -> o .== (i1 .&. i2) + +or :: (SymVal a, Ord a, Num a, Bits a) => SimpleComponent a +or = SimpleComponent "or" $ SimpleSpec 2 $ \[i1,i2] o -> o .== (i1 .|. i2) + +not :: (SymVal a, Ord a, Num a, Bits a) => SimpleComponent a +not = SimpleComponent "not" $ SimpleSpec 1 $ \[i1] o -> o .== complement i1 + + +bXor = SimpleComponent "bXor" $ SimpleSpec 2 $ \[i1,i2] o -> o .== i1 .<+> i2 + +-- | Logical equivalence implemented in "tabular" style +bEquiv = SimpleComponent "bEquiv" $ SimpleSpec 2 $ \[i1,i2] o -> sAnd [ + sNot i1 .&& sNot i2 .=> o, + i1 .&& sNot i2 .=> sNot o, + sNot i1 .&& i2 .=> sNot o, + i1 .&& i2 .=> o + ] diff --git a/src/Data/SBV/Program/Types.hs b/src/Data/SBV/Program/Types.hs new file mode 100644 --- /dev/null +++ b/src/Data/SBV/Program/Types.hs @@ -0,0 +1,201 @@ +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} + +module Data.SBV.Program.Types ( + module Data.Biapplicative, + module Data.Bifoldable, + module Data.Bitraversable, + + Location, + SLocation, + + SynthSpec(..), + SynthComponent(..), + + SimpleSpec(..), + SimpleComponent(..), + + SynthesisError(..), + + IOs(..), + Instruction(..), + Program(..), + toIOsList, + sortInstructions, + + ProgramTree(..), + buildProgramTree, + buildForestResult, + ) +where + +import Data.Biapplicative +import Data.Bifoldable +import Data.Bitraversable +import Data.Foldable +import Data.List +import qualified Data.Map as M +import qualified Data.Set as S +import Data.SBV + + +-- | Type used to represent a value from the __set of location variables__ \(l_x \in L\). +type Location = Word64 +-- | Symbolic 'Location'. +type SLocation = SWord64 + + +-- | Class for a program or a component __specification__ \(φ(\vec I, O)\). Type +-- variable 'a' stands for function's domain type. +class SynthSpec s a where + -- | Number of inputs the specification function takes. + specArity :: s a -> Word + -- | An equation that relates input variables to the output one. The equation is + -- build up either using '(.==)' or in a "tabular" way using multiple '(.=>)' + -- expressions. See definitions from the Data.SBV.Program.SimpleLibrary module + -- for examples. + specFunc :: s a + -- | Input variables. The list should be of 'specArity' size. + -> [SBV a] + -- | Output variable. + -> SBV a + -> SBool + +-- | A class for a __library component__. +class SynthSpec spec a => SynthComponent comp spec a | comp -> spec where + -- | Component name (optional). Used for naming SBV variables and when rendering the resulting program. + compName :: comp a -> String + -- | Component's __specification__. + compSpec :: comp a -> spec a + -- | Optional constraints to set on __location variables__ \(l_x \in L\). + extraLocConstrs :: comp a -> [[SLocation] -> SLocation -> SBool] + + compName = const "" + extraLocConstrs = const [] + + +-- | A simplest __specification__ datatype possible. Type variable 'a' stands +-- for function's domain type. +data SimpleSpec a = SimpleSpec { + simpleArity :: Word + , simpleFunc :: [SBV a] -> SBV a -> SBool + } + +instance SynthSpec SimpleSpec a where + specArity = simpleArity + specFunc = simpleFunc + +-- | A simplest __library component__ datatype possible. +data SimpleComponent a = SimpleComponent { + simpleName :: String + , simpleSpec :: SimpleSpec a + } + +instance SynthComponent SimpleComponent SimpleSpec a where + compName = simpleName + compSpec = simpleSpec + extraLocConstrs = const [] + +instance Show (SimpleComponent spec) where + show = compName + + +-- | Possible failure reasons during synthesis operation. +data SynthesisError = ErrorUnsat + | ErrorUnknown String + | ErrorZeroResultsRequested + | ErrorSeedingFailed + deriving Show + + +-- | A datatype holding inputs and output of something. Usual types for 'l' are 'Location' and 'SLocation'. +data IOs l = IOs { + _ins :: [l], + _out :: l + } + deriving (Show, Eq, Ord, Functor) + +instance Foldable IOs where + foldMap f (IOs {..}) = mconcat (map f _ins) `mappend` f _out + +instance Traversable IOs where + traverse f (IOs {..}) = IOs <$> traverse f _ins <*> f _out + +instance EqSymbolic l => EqSymbolic (IOs l) where + l .== r = toList l .== toList r + + +-- | A datatype that holds a 'SynthComponent' with inputs and output locations. +data Instruction l a = Instruction { + instructionIOs :: IOs l, + instructionComponent :: a + } + deriving (Show, Eq, Ord) + +instance Bifunctor Instruction where + bimap iosF compF (Instruction {..}) = Instruction (fmap iosF instructionIOs) (compF instructionComponent) + +instance Bitraversable Instruction where + bitraverse iosF compF (Instruction ios comp) = Instruction <$> traverse iosF ios <*> compF comp + +instance Bifoldable Instruction where + bifoldMap f1 f2 (Instruction {..}) = foldMap f1 instructionIOs `mappend` f2 instructionComponent + + +-- | A datatype that unites program instructions with 'IOs' of the program itself. +data Program l a = Program { + programIOs :: IOs l, + programInstructions :: [Instruction l a] + } + deriving (Show, Eq, Ord) + +instance Bifunctor Program where + bimap iosF compF (Program {..}) = Program (fmap iosF programIOs) (map (bimap iosF compF) programInstructions) + +instance Bitraversable Program where + bitraverse iosF compF (Program ios instrs) = Program <$> traverse iosF ios <*> traverse (bitraverse iosF compF) instrs + +instance Bifoldable Program where + bifoldMap f1 f2 (Program {..}) = foldMap f1 programIOs `mappend` foldMap (bifoldMap f1 f2) programInstructions + +-- | Extract all locations from the program as a list, including locations of instructions. +toIOsList :: Program l a -> [l] +toIOsList = bifoldMap (:[]) (const mempty) + +-- | Sorts program's instructions by their output location. +sortInstructions :: Ord l => Program l a -> Program l a +sortInstructions p = p { programInstructions = sortOn (_out . instructionIOs) (programInstructions p) } + + +-- | A `Program` converted into a tree-like structure. +data ProgramTree a = InstructionNode a [ProgramTree a] + | InputLeaf Location + deriving (Show, Eq, Ord, Functor) + +instance Foldable ProgramTree where + foldMap _ (InputLeaf _) = mempty + foldMap f (InstructionNode comp children) = foldMap (foldMap f) children <> f comp + +-- | Create a 'ProgramTree' for a given 'Program' by resolving its 'Location's. +-- This function effectively performs dead code elimination. +buildProgramTree :: Program Location a -> ProgramTree a +buildProgramTree prog = buildProgramTree' prog (_out $ programIOs prog) + +-- | A variant of 'buildProgramTree' that builds from a specified starting point. +buildProgramTree' :: Program Location a -> Location -> ProgramTree a +buildProgramTree' prog@(Program {..}) startingOutputLoc = + if startingOutputLoc `notElem` _ins programIOs + then InstructionNode + (instructionComponent (instsMap M.! startingOutputLoc)) + (map (buildProgramTree' prog) $ _ins $ instructionIOs (instsMap M.! startingOutputLoc)) + else InputLeaf startingOutputLoc + where + instsMap = M.fromList $ map (\inst -> (_out $ instructionIOs inst, inst)) programInstructions + +-- | Create a 'ProgramTree' for each unused output in the 'Program' +buildForestResult sr@(Program {..}) = map (buildProgramTree' sr) rootOutputs + where + inputsSet = S.fromList $ _ins programIOs ++ concatMap (_ins . instructionIOs) programInstructions + rootOutputs = filter isRootOutput $ map (_out . instructionIOs) programInstructions + isRootOutput o = o `S.notMember` inputsSet diff --git a/src/Data/SBV/Program/Utils.hs b/src/Data/SBV/Program/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Data/SBV/Program/Utils.hs @@ -0,0 +1,78 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} + +module Data.SBV.Program.Utils ( + sampleSpec, + + mkVarName, + mkInputLocName, + mkOutputLocName, + mkInputVarName, + mkOutputVarName, + + writePseudocode, + ) +where + +import Data.List (intercalate) +import Data.SBV +import Data.SBV.Control +import Data.SBV.Program.Types + + +-- | Given a 'SynthSpec' tries to generate a set of input/output values that satisfy the specification. +-- Uses solver under the hood. +sampleSpec :: forall a comp spec . (SymVal a, SynthSpec spec a) => spec a -> IO (Maybe (IOs a)) +sampleSpec spec = runSMT $ do + -- use solver to create initial values for I + ins <- mkExistVars @a $ fromIntegral $ specArity spec + out <- sbvExists_ + constrain $ specFunc spec ins out + query $ do + r <- checkSat + case r of + Sat -> Just <$> (IOs <$> mapM getValue ins <*> getValue out) + _ -> pure Nothing + + +-- | Creates sanitized variable name suitable for SBV. +mkVarName :: String -- ^ Base name, which can be an empty string, in which case \"UnnamedComponent\" value will be used. + -> Bool -- ^ Setting 'isLocation' to 'True' will append \"Loc\" to the name. + -> Bool -- ^ If 'isOutput' is 'False' the value of 'i' is also appended to the name. + -> Word -- ^ Number of an input. Can be 'undefined' for an output. + -> String +mkVarName compName isLocation isOutput i = name1 ++ name2 ++ if not isOutput then show i else "" + where + name1 = if null compName then "UnnamedComponent" else compName + name2 = (if isOutput then "Output" else "Input") ++ if isLocation then "Loc" else "" + +-- | Shortcut for the more general 'mkVarName' function. +mkInputLocName compName = mkVarName compName True False +-- | Shortcut for the more general 'mkVarName' function. +mkOutputLocName compName = mkVarName compName True True undefined +-- | Shortcut for the more general 'mkVarName' function. +mkInputVarName compName = mkVarName compName False False +-- | Shortcut for the more general 'mkVarName' function. +mkOutputVarName compName = mkVarName compName False True undefined + + +-- | Renders the solution in SSA style. +writePseudocode :: SynthComponent comp spec a => Program Location (comp a) -> String +writePseudocode prog = unlines (header : body ++ ret) + where + prog' = sortInstructions prog + header = concat [ + "function(", + intercalate ", " $ map writeArg (_ins $ programIOs prog'), + "):" + ] + body = flip map (programInstructions prog') $ \(Instruction (IOs {..}) comp) -> concat [ + "\t%", + show _out, + " = ", + compName comp, + " ", + intercalate ", " $ map writeArg _ins + ] + ret = ["\treturn " ++ writeArg (_out $ programIOs prog')] + writeArg loc = '%' : show loc diff --git a/test/SmokeTest.hs b/test/SmokeTest.hs new file mode 100644 --- /dev/null +++ b/test/SmokeTest.hs @@ -0,0 +1,36 @@ +import Control.Monad +import Data.List +import Data.SBV +import Data.SBV.Program +import Data.SBV.Program.Examples +import Data.SBV.Program.SimpleLibrary as Lib + +main :: IO () +main = do + putStrLn "===== exAllProcedure ======" + r <- exAllProcedure [Lib.and, dec] paperRunningExampleSpec + case r of + Right r -> do + putStrLn $ writePseudocode r + assert $ solutionCorrect (toIOsList $ sortInstructions r) + Left e -> error $ show e + + putStrLn "===== standardExAllProcedure ======" + r <- standardExAllProcedure [Lib.and, dec] paperRunningExampleSpec + case r of + Right r -> do + putStrLn $ writePseudocode r + assert $ solutionCorrect (toIOsList $ sortInstructions r) + Left e -> error $ show e + + putStrLn "===== refinedExAllProcedure ======" + r <- refinedExAllProcedure [Lib.and, dec] paperRunningExampleSpec + case r of + Right r -> do + putStrLn $ writePseudocode r + assert $ solutionCorrect (toIOsList $ sortInstructions r) + _ -> error "refinedExAllProcedure" + +solutionCorrect s = [0,2] `isPrefixOf` s && ([1,0,2] `isSuffixOf` s || [0,1,2] `isSuffixOf` s) + +assert cond = unless cond (error "assertion failed")