packages feed

horname (empty) → 0.1.0.0

raw patch · 10 files changed

+439/−0 lines, 10 filesdep +basedep +containersdep +hornamesetup-changed

Dependencies added: base, containers, horname, megaparsec, optparse-applicative, text, these, uniplate, wl-pprint-text

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Moritz Kiefer (c) 2016++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * 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.++    * Neither the name of Moritz Kiefer nor the names of other+      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+OWNER 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.
+ README.md view
@@ -0,0 +1,13 @@+# horname++[![Build Status](https://travis-ci.com/cocreature/horname.svg?token=k5tv9VjJ9pj7ynzqQyjR&branch=master)](https://travis-ci.com/cocreature/horname)++Parses `define-fun` clauses output by SMT solvers+and renames the variables according to annotations of the form++```+; :annot (INV_MAIN_42 i j n i j)+```++in the original SMT. The SMT-LIB standard itself does not allow naming+arguments in a function declaration.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ app/Main.hs view
@@ -0,0 +1,18 @@+{-# LANGUAGE OverloadedStrings #-}+module Main where++import qualified Data.Text.IO as Text+import           Horname+import           Options+import           Options.Applicative hiding (Parser, runParser)++main :: IO ()+main = do+  Opts outp inp <- execParser opts+  outContent <- Text.readFile outp+  inContent <- Text.readFile inp+  case extractRenamedInvariants inp inContent outp outContent of+    Left errs -> print errs+    Right invariants -> mapM_ (Text.putStrLn . ppDefineFun) invariants+  where+    opts = info (helper <*> optsParser) (header "horname")
+ app/Options.hs view
@@ -0,0 +1,18 @@+module Options+  ( Opts(..)+  , optsParser+  ) where++import Data.Monoid+import Options.Applicative++data Opts = Opts+  { solverOuptutFile :: !FilePath+  , solverInputFile :: !FilePath+  } deriving (Show, Eq, Ord)++optsParser :: Parser Opts+optsParser =+  Opts <$>+  strOption (long "smt-output" <> help "Path to the solver output") <*>+  strOption (long "smt-input" <> help "Path to the input smt file")
+ horname.cabal view
@@ -0,0 +1,42 @@+name:                horname+version:             0.1.0.0+synopsis:            Rename function definitions returned by SMT solvers+description:         Please see README.md+homepage:            https://github.com/cocreature/horname#readme+license:             BSD3+license-file:        LICENSE+author:              Moritz Kiefer+maintainer:          value+copyright:           (C) 2016 Moritz Kiefer+category:            Web+build-type:          Simple+cabal-version:       >=1.10+extra-source-files:  README.md+tested-with:         GHC == 8.0.1++executable horname+  hs-source-dirs:      app+  other-modules:       Options+  main-is:             Main.hs+  default-language:    Haskell2010+  build-depends:       base >= 4.9 && < 5+                     , horname+                     , optparse-applicative >= 0.12 && < 0.14+                     , text >= 1.2 && < 1.3+  ghc-options:         -Wall++library+    hs-source-dirs:   src+    exposed-modules:  Horname+                      Horname.Internal.SMT+                      Horname.Internal.SMT.Parser+                      Horname.Internal.SMT.Pretty+    default-language: Haskell2010+    build-depends:    base >= 4.9 && < 5+                    , containers >= 0.5 && < 0.6+                    , megaparsec >= 5.0 && < 5.2+                    , text >= 1.2 && < 1.3+                    , these >= 0.7 && < 0.8+                    , uniplate >= 1.6 && < 1.7+                    , wl-pprint-text >= 1.1 && < 1.2+    ghc-options:      -Wall
+ src/Horname.hs view
@@ -0,0 +1,39 @@+module Horname+  ( extractRenamedInvariants+  , DefineFun(..)+  , ppDefineFun+  , SExpr(..)+  , VarName(..)+  , Sort(..)+  , Arg(..)+  ) where++import           Data.Text (Text)+import qualified Data.Text.Lazy as Text+import           Data.These+import           Horname.Internal.SMT+import           Horname.Internal.SMT.Parser+import qualified Horname.Internal.SMT.Pretty as Pretty+import           Text.Megaparsec+import           Text.PrettyPrint.Leijen.Text++extractRenamedInvariants+  :: FilePath {- ^ input filename -}+  -> Text {- ^ solver input -}+  -> FilePath {- ^ output filename -}+  -> Text {- ^ solver output -}+  -> Either (These String String) [DefineFun]+extractRenamedInvariants inpFile inp outpFile outp =+  let outpResult = runParser parseDefineFuns outpFile outp+      inpResult = runParser parseDeclareFuns inpFile inp+  in case (outpResult, inpResult) of+       (Left err, Left err') ->+         Left (These (parseErrorPretty err) (parseErrorPretty err'))+       (Left err, _) -> Left (This (parseErrorPretty err))+       (_, Left err) -> Left (That (parseErrorPretty err))+       (Right defineFuns, Right declareFuns) ->+         Right (extractDefinitions declareFuns defineFuns)++-- The magi numbers here are taken from hPutDoc+ppDefineFun :: DefineFun -> Text+ppDefineFun = Text.toStrict . displayT . renderPretty 0.4 80 . Pretty.ppDefineFun
+ src/Horname/Internal/SMT.hs view
@@ -0,0 +1,149 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE LambdaCase #-}+module Horname.Internal.SMT where++import           Data.Data+import           Data.List (foldl', find)+import           Data.Map (Map)+import qualified Data.Map as Map+import           Data.Maybe+import           Data.Text (Text)++newtype VarName =+  VarName Text+  deriving (Show, Eq, Ord, Data)++newtype Sort =+  Sort Text+  deriving (Show, Eq, Ord, Data)++data Arg = Arg+  { argName :: !VarName+  , argSort :: !Sort+  } deriving (Show, Eq, Ord, Data)++data DefineFun = DefineFun+  { funName :: !Text+  , arguments :: ![Arg]+  , returnSort :: !Sort+  , body :: !SExpr+  } deriving (Show, Eq, Ord, Data)++data SExpr+  = IntLit !Integer+  | StringLit !Text+  | List ![SExpr]+  deriving (Show, Eq, Ord, Data)++renameDefineFun :: [Text] -> DefineFun -> DefineFun+renameDefineFun newNames (DefineFun n args retSort expr) =+  DefineFun n renamedArgs retSort (renameInBody varMap expr)+  where+    renamedArgs =+      zipWith (\(Arg _ sort) name -> Arg (VarName name) sort) args newNames+    varMap :: Map Text Text+    varMap =+      Map.fromList $ zip (map (\(Arg (VarName name) _) -> name) args) newNames+    renameInBody :: Map Text Text -> SExpr -> SExpr+    renameInBody m (StringLit s) =+      case Map.lookup s m of+        Just s' -> StringLit s'+        Nothing -> StringLit s+    renameInBody _ (IntLit i) = IntLit i+    renameInBody m (List exprs) = List (map (renameInBody m) exprs)++insertBindings :: Map Text SExpr -> [SExpr] -> Map Text SExpr+insertBindings m bindings = foldl' insertBinding m bindings++insertBinding :: Map Text SExpr -> SExpr -> Map Text SExpr+insertBinding m (List [StringLit key, val]) = Map.insert key val m+insertBinding _ _ = error "Syntax error in let bindings"++-- | This is not correct in the presence of nested lets but these+-- should never occur in the Z3 output and Eldarica doesn’t include+-- any lets.+inlineLets :: SExpr -> SExpr+inlineLets = inlineLets' Map.empty++inlineLets' :: Map Text SExpr -> SExpr -> SExpr+inlineLets' _ (IntLit i) = IntLit i+inlineLets' m (StringLit t) =+  case Map.lookup t m of+    Just val -> val+    Nothing -> StringLit t+inlineLets' m (List [StringLit "let", List bindings, expr]) =+  inlineLets' (insertBindings m bindings) expr+inlineLets' m (List args) = List (map (inlineLets' m) args)++comparisonOps :: [Text]+comparisonOps = ["=", "<", "<=", ">", ">="]++partitionPosNeg :: SExpr -> ([SExpr],[SExpr])+partitionPosNeg (List (StringLit "+":args)) =+  partition+    (\case+       (List [StringLit "-", e]) -> Right e+       e -> Left e)+    args+partitionPosNeg e = ([e],[])++partition               :: (a -> Either b c) -> [a] -> ([b],[c])+partition p xs = foldr (select p) ([],[]) xs++select :: (a -> Either b c) -> a -> ([b], [c]) -> ([b], [c])+select p x (bs,cs) =+  case p x of+    Left b -> (b:bs,cs)+    Right c -> (bs, c:cs)++nonZero :: SExpr -> Bool+nonZero (IntLit 0) = False+nonZero _ = True++sumExprs :: [SExpr] -> SExpr+sumExprs [] = IntLit 0+sumExprs [e] = e+sumExprs args = List (StringLit "+" : args)++simplify :: SExpr -> SExpr+-- (* (- 1) x) → x+simplify (List [StringLit "*", List [StringLit "-", IntLit 1], expr]) =+  List [StringLit "-", expr]+-- merge nested ands+simplify (List (StringLit "and":args)) =+  List (StringLit "and" : (andArgs ++ others))+  where+    (ands, others) =+      partition+        (\case+           List (StringLit "and":args') -> Left args'+           e -> Right e)+        args+    andArgs = concat ands+-- Move negative and positive arguments to the same side of a comparison+simplify (List [StringLit opName, arg1, arg2])+  | opName `elem` comparisonOps =+    case (partitionPosNeg arg1, partitionPosNeg arg2) of+      ((posLeft, negLeft), (posRight, negRight)) ->+        List+          [ StringLit opName+          , sumExprs . filter nonZero $ (posLeft ++ negRight)+          , sumExprs . filter nonZero $ (posRight ++ negLeft)+          ]+-- Transform (+ a (- b c)) to (+ a b (- c))+simplify (List (StringLit "+":args)) =+  List (StringLit "+" : (sepSubtraction =<< args))+  where+    sepSubtraction :: SExpr -> [SExpr]+    sepSubtraction (List [StringLit "-", arg1, arg2]) =+      [arg1, List [StringLit "-", arg2]]+    sepSubtraction e = [e]+simplify e = e++extractDefinitions :: Map Text [Text] -> [DefineFun] -> [DefineFun]+extractDefinitions decls defs =+  mapMaybe+    (\(name, argNames) ->+       renameDefineFun argNames <$> find ((== name) . funName) defs)+    (Map.toList decls)
+ src/Horname/Internal/SMT/Parser.hs view
@@ -0,0 +1,88 @@+{-# LANGUAGE OverloadedStrings #-}+module Horname.Internal.SMT.Parser where++import           Data.Char+import           Data.Generics.Uniplate.Data+import           Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import           Data.Text (Text)+import qualified Data.Text as Text+import           Horname.Internal.SMT+import           Text.Megaparsec+import           Text.Megaparsec.Text++parseName :: Parser Text+parseName = Text.pack <$> some (noneOf [' ', '\n', ')'])++parseSort :: Parser Sort+parseSort = Sort . Text.pack <$> some (noneOf [' ', '\n', ')'])++parseArg :: Parser Arg+parseArg = do+  _ <- char '('+  name <- parseName+  someSpace+  sort <- parseSort+  _ <- char ')'+  pure (Arg (VarName name) sort)++parseArgs :: Parser [Arg]+parseArgs = do+  _ <- char '('+  args <- sepBy parseArg someSpace+  _ <- char ')'+  pure args++someSpace :: Parser ()+someSpace = skipSome spaceChar++parseSExpr :: Parser SExpr+parseSExpr = do+  c <- char '(' <|> satisfy (not . isSpace)+  case c of+    '(' -> do+      space+      args <- sepBy parseSExpr someSpace+      space+      _ <- char ')'+      pure (List args)+    alphaNum+      | isDigit alphaNum -> do+        digits <- many digitChar+        pure (IntLit (read (alphaNum : digits)))+      | otherwise -> do+        rest <- many (noneOf [' ', ')'])+        pure . StringLit . Text.pack $ alphaNum : rest++parseDefineFun :: Parser DefineFun+parseDefineFun = do+  _ <- manyTill anyChar (string "(define-fun")+  someSpace+  name <- parseName+  someSpace+  args <- parseArgs+  someSpace+  retSort <- parseSort+  someSpace+  expr <- parseSExpr+  space+  _ <- char ')'+  pure (DefineFun name args retSort (transform simplify $ inlineLets expr))++parseDefineFuns :: Parser [DefineFun]+parseDefineFuns = many (try parseDefineFun)++parseDeclareFun :: Parser (Text, [Text])+parseDeclareFun = do+  _ <- manyTill anyChar (string "; :annot (")+  name <- parseName+  someSpace+  args <-+    map (Text.replace "_0" "") <$>+    sepBy parseName someSpace+  space+  _ <- char ')'+  pure (name, args)++parseDeclareFuns :: Parser (Map Text [Text])+parseDeclareFuns = Map.fromList <$> many (try parseDeclareFun)
+ src/Horname/Internal/SMT/Pretty.hs view
@@ -0,0 +1,40 @@+{-# LANGUAGE OverloadedStrings #-}+module Horname.Internal.SMT.Pretty where++import           Data.Text (Text)+import qualified Data.Text.Lazy as Text+import           Horname.Internal.SMT+import           Text.PrettyPrint.Leijen.Text++dontIndent :: [Text]+dontIndent = ["+", "-", "*", "=", "<=", "<", ">=", ">"]++ppSExpr :: SExpr -> Doc+ppSExpr (IntLit i) = text . Text.pack $ show i+ppSExpr (StringLit s) = text . Text.fromStrict $ s+ppSExpr (List args'@(StringLit name:args))+  | name `elem` dontIndent = parens $ hsep (map ppSExpr args')+  | otherwise =+    parens $ text (Text.fromStrict name) <+> align (vsep (map ppSExpr args))+ppSExpr (List args) =+  parens $ align (vsep (map ppSExpr args))++ppSort :: Sort -> Doc+ppSort (Sort t) = text (Text.fromStrict t)++ppVarName :: VarName -> Doc+ppVarName (VarName t) = text (Text.fromStrict t)++ppArg :: Arg -> Doc+ppArg (Arg name sort) = parens (ppVarName name <+> ppSort sort)++ppDefineFun :: DefineFun -> Doc+ppDefineFun (DefineFun name args retType expr) =+  parens $+  text "define-fun" <+>+  align+    (vsep+       [ text (Text.fromStrict name)+       , parens (hsep (map ppArg args)) <+> ppSort retType+       , ppSExpr expr+       ])