target (empty) → 0.1.0.0
raw patch · 15 files changed
+2276/−0 lines, 15 filesdep +QuickCheckdep +SafeSemaphoredep +aesonsetup-changed
Dependencies added: QuickCheck, SafeSemaphore, aeson, array, base, bytestring, cassava, containers, data-timeout, deepseq, directory, exceptions, filepath, ghc, ghc-paths, ghc-prim, liquid-fixpoint, liquidhaskell, mtl, pretty, process, random, smallcheck, syb, tagged, target, tasty, tasty-hunit, template-haskell, text, text-format, time, transformers, unordered-containers, vector, xml-conduit
Files
- LICENSE +21/−0
- Setup.hs +2/−0
- bench/Main.hs +227/−0
- cbits/fpstring.c +82/−0
- src/Test/Target.hs +73/−0
- src/Test/Target/Eval.hs +172/−0
- src/Test/Target/Expr.hs +68/−0
- src/Test/Target/Monad.hs +270/−0
- src/Test/Target/Targetable.hs +543/−0
- src/Test/Target/Targetable/Function.hs +177/−0
- src/Test/Target/Testable.hs +197/−0
- src/Test/Target/Types.hs +71/−0
- src/Test/Target/Util.hs +140/−0
- target.cabal +161/−0
- test/Main.hs +72/−0
+ LICENSE view
@@ -0,0 +1,21 @@+The MIT License (MIT)++Copyright (c) 2014 Eric Seidel++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in+all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN+THE SOFTWARE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ bench/Main.hs view
@@ -0,0 +1,227 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeSynonymInstances #-}+module Main where++import Test.Target+import qualified Test.QuickCheck as QC+import qualified Test.SmallCheck as SC+import qualified Test.SmallCheck.Drivers as SC++import Control.Applicative+import Control.Concurrent.Timeout+import Control.Exception+import Control.Monad+import qualified Data.ByteString as B+import qualified Data.ByteString.Char8 as B8+import qualified Data.ByteString.Lazy as LB+import Data.Csv+import qualified Data.List as L+import Data.IORef+import Data.Monoid+import Data.Time.Clock.POSIX+import Data.Timeout+import qualified Data.Vector as V+import System.IO+import Text.Printf++-- import qualified Expr+-- import qualified ExprBench as Expr+import qualified List+import qualified ListBench as List+import qualified Map as Map+import qualified MapBench as Map+import qualified RBTree+import qualified RBTreeBench as RBTree+import qualified XMonad.Properties as XMonad++import qualified LazySmallCheck as LSC++data Outcome = TimeOut+ | Complete !Int+ | GaveUp !Int+ deriving (Read, Show)++data TestResult+ = TestResult { testName :: !String+ , liquid :: ![(Int,Double,Outcome)]+ , small :: ![(Int,Double,Outcome)]+ , lazysmall :: ![(Int,Double,Outcome)]+ , lazysmall_slow :: !(Maybe [(Int,Double,Outcome)])+ , quick :: !(Double,Outcome)+ } deriving (Read, Show)++testResultRecords :: TestResult -> [NamedRecord]+testResultRecords (TestResult name l s ls lss _)+ = [ namedRecord $ [ "Benchmark" .= B8.pack name+ , "Tool" .= B8.pack "Target" ]+ ++ [ bshow d .= toResult t o | d <- [2..20], let (t,o) = lookup3 d l ]+ , namedRecord $ [ "Benchmark" .= B8.pack name+ , "Tool" .= B8.pack "SmallCheck" ]+ ++ [ bshow d .= toResult t o | d <- [2..20], let (t,o) = lookup3 d s ]+ , namedRecord $ [ "Benchmark" .= B8.pack name+ , "Tool" .= B8.pack "Lazy-SmallCheck" ]+ ++ [ bshow d .= toResult t o | d <- [2..20], let (t,o) = lookup3 d ls ]+ ]+ ++ maybe [] (\ss ->+ [ namedRecord $ [ "Benchmark" .= B8.pack name+ , "Tool" .= B8.pack "Lazy-SmallCheck-slow" ]+ ++ [ bshow d .= toResult t o | d <- [2..20], let (t,o) = lookup3 d ss ]+ ]) lss++bshow :: Show a => a -> B.ByteString+bshow = B8.pack . show++lookup3 :: Int -> [(Int,Double,Outcome)] -> (Double,Outcome)+lookup3 x xs = case L.find (\(a,b,c) -> a == x) xs of+ Nothing -> (0, TimeOut)+ Just (i,d,o) -> (d,o)++toResult :: Double -> Outcome -> B.ByteString+toResult d TimeOut = "X"+toResult d (Complete i) = bshow d++header :: V.Vector B.ByteString+header = V.fromList $ ["Benchmark", "Tool"] ++ [bshow d | d <- [2..20]]++logCsv f r = withFile f WriteMode $ \h -> do+ LB.hPutStr h $ encodeByName header $ testResultRecords r+ return r++main :: IO ()+main = do+ print =<< logCsv "bench/List.insert.csv" =<< listInsertTests+ print =<< logCsv "bench/RBTree.add.csv" =<< rbTreeAddTests+ -- print =<< logCsv "bench/Expr.subst.csv" =<< exprSubstTests+ print =<< logCsv "bench/Map.delete.csv" =<< mapDeleteTests+ print =<< logCsv "bench/Map.difference.csv" =<< mapDifferenceTests+ print =<< logCsv "bench/XMonad.focus_left.csv" =<< xmonadFocusLeftTests++listInsertTests = do+ let n = 'List.insert+ l <- checkTarget List.insert n "examples/List.hs"+ s <- checkSmall List.prop_insert_sc n+ ls <- checkLazySmall List.prop_insert_lsc n+ q <- checkQuick List.prop_insert_qc n+ return $ TestResult (show n) l s ls Nothing q++rbTreeAddTests = do+ let n = 'RBTree.add+ l <- checkTarget RBTree.prop_add_lc n "examples/RBTree.hs"+ s <- checkSmall RBTree.prop_add_sc n+ ls <- checkLazySmall RBTree.prop_add_lsc n+ lss <- checkLazySmall RBTree.prop_add_lsc_slow n+ q <- checkQuick RBTree.prop_add_qc n+ return $ TestResult (show n) l s ls (Just lss) q++-- exprSubstTests = do+-- l <- checkTarget Expr.subst "Expr.subst" "examples/Expr.hs"+-- s <- checkSmall Expr.prop_subst_sc "Expr.subst"+-- ls <- checkLazySmall Expr.prop_subst_lsc "Expr.subst"+-- q <- checkQuick Expr.prop_subst_qc "Expr.subst"+-- return $ TestResult "Expr.subst" l s ls Nothing q++mapDeleteTests = do+ let n = 'Map.delete+ l <- checkTarget Map.prop_delete_lc n "examples/Map.hs"+ s <- checkSmall Map.prop_delete_sc n+ ls <- checkLazySmall Map.prop_delete_lsc n+ lss <- checkLazySmall Map.prop_delete_lsc_slow n+ q <- checkQuick Map.prop_delete_qc n+ return $ TestResult (show n) l s ls (Just lss) q++mapDifferenceTests = do+ let n = 'Map.difference+ l <- checkTarget Map.prop_difference_lc n "examples/Map.hs"+ s <- checkSmall Map.prop_difference_sc n+ ls <- checkLazySmall Map.prop_difference_lsc n+ lss <- checkLazySmall Map.prop_difference_lsc_slow n+ q <- checkQuick Map.prop_difference_qc n+ return $ TestResult (show n) l s ls (Just lss) q++xmonadFocusLeftTests = do+ let n = 'XMonad.prop_focus_left_master_lc+ l <- checkTarget XMonad.prop_focus_left_master_lc n "examples/XMonad/Properties.hs"+ s <- checkSmall XMonad.prop_focus_left_master_sc n+ ls <- checkLazySmall XMonad.prop_focus_left_master_lsc n+ q <- checkQuick XMonad.prop_focus_left_master_qc n+ return $ TestResult (show n) l s ls Nothing q+++myTimeout :: IO a -> IO (Maybe a)+myTimeout = timeout (60 # Minute)++getTime :: IO Double+getTime = realToFrac `fmap` getPOSIXTime++timed x = do start <- getTime+ v <- x+ end <- getTime+ return (end-start, v)++resultPassed (Passed i) = i++-- checkTarget :: CanTest f => f -> String -> FilePath -> IO [(Int,Double,Outcome)]+checkTarget f n m = checkMany (show n++"/Target")+ (\d max -> resultPassed <$>+ targetResultWith f n m (mkOpts d max))+ where mkOpts d max = defaultOpts { depth = d, maxSuccess = Just max, scDepth = True }++checkSmall p n = checkMany (show n++"/SmallCheck")+ (\d n -> fromIntegral.fst.fst <$> runTestWithStats d n (p d))++checkLazySmall p n = checkMany (show n++"/LazySmallCheck")+ (\d n -> LSC.depthCheckResult d n (p d))++-- checkQuick :: QC.Testable f => f -> String -> IO (Double,Outcome)+checkQuick p n = timed $ do+ putStrNow $ printf "Testing %s/QuickCheck.. " (show n)+ r <- QC.quickCheckWithResult (QC.stdArgs {QC.chatty = False}) p+ putStrNow "done!\n"+ return $ case r of+ QC.Success {..} -> Complete numTests+ QC.GaveUp {..} -> GaveUp numTests++checkMany :: String -> (Int -> Int -> IO Int) -> IO [(Int, Double, Outcome)]+checkMany name bench = do+ putStrNow $ printf "Testing %s.. " name+ r <- go 2+ putStrNow "done!\n"+ return r+ where+ go n + | n > 20+ = return []+ | otherwise+ = putStrNow (printf "%d " n) >> timed (myTimeout (bench n 1000)) >>= \case+ (d,Nothing) -> return [(n,d,TimeOut)]+ (d,Just i) -> ((n,d,Complete i):) <$> go (n+1)+++putStrNow s = putStr s >> hFlush stdout++runTestWithStats :: SC.Testable IO a => SC.Depth -> Int -> a+ -> IO ((Integer,Integer), Maybe SC.PropertyFailure)+runTestWithStats d n prop = do+ good <- newIORef 0+ bad <- newIORef 0++ let+ hook SC.GoodTest = do modifyIORef' good (+1)+ n' <- readIORef good+ when (n' == fromIntegral n) $ throw ()+ hook SC.BadTest = modifyIORef' bad (+1)++ r <- SC.smallCheckWithHook d hook prop `catch` \() -> return Nothing++ goodN <- readIORef good+ badN <- readIORef bad++ return ((goodN, badN), r)++-- instance Exception ()
+ cbits/fpstring.c view
@@ -0,0 +1,82 @@+/*+ * Copyright (c) 2003 David Roundy+ * Copyright (c) 2005-6 Don Stewart+ *+ * All rights reserved.+ *+ * 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 names of the authors or the names of any contributors+ * may be used to endorse or promote products derived from this software+ * without specific prior written permission.+ *+ * THIS SOFTWARE IS PROVIDED BY THE REGENTS 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 AUTHORS 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.+ */++#include "fpstring.h"++/* copy a string in reverse */+void fps_reverse(unsigned char *q, unsigned char *p, unsigned long n) {+ p += n-1;+ while (n-- != 0)+ *q++ = *p--;+}++/* duplicate a string, interspersing the character through the elements+ of the duplicated string */+void fps_intersperse(unsigned char *q,+ unsigned char *p,+ unsigned long n,+ unsigned char c) {++ while (n > 1) {+ *q++ = *p++;+ *q++ = c;+ n--;+ }+ if (n == 1)+ *q = *p;+}++/* find maximum char in a packed string */+unsigned char fps_maximum(unsigned char *p, unsigned long len) {+ unsigned char *q, c = *p;+ for (q = p; q < p + len; q++)+ if (*q > c)+ c = *q;+ return c;+}++/* find minimum char in a packed string */+unsigned char fps_minimum(unsigned char *p, unsigned long len) {+ unsigned char *q, c = *p;+ for (q = p; q < p + len; q++)+ if (*q < c)+ c = *q;+ return c;+}++/* count the number of occurences of a char in a string */+unsigned long fps_count(unsigned char *p, unsigned long len, unsigned char w) {+ unsigned long c;+ for (c = 0; len-- != 0; ++p)+ if (*p == w)+ ++c;+ return c;+}
+ src/Test/Target.hs view
@@ -0,0 +1,73 @@+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE ViewPatterns #-}+module Test.Target+ ( target, targetResult, targetWith, targetResultWith+ -- , targetTH+ , Result(..), Testable+ , TargetOpts(..), defaultOpts+ , Test(..)+ ) where++import Control.Applicative+import Control.Monad+import Control.Monad.Catch+import Control.Monad.State+import qualified Language.Haskell.TH as TH+import System.Process (terminateProcess)+import Text.Printf (printf)++import Language.Fixpoint.Names+import Language.Fixpoint.SmtLib2 hiding (verbose)++import Test.Target.Monad+import Test.Target.Targetable ()+import Test.Target.Targetable.Function ()+import Test.Target.Testable+import Test.Target.Types+import Test.Target.Util++-- | Test whether a function inhabits its refinement type by enumerating valid+-- inputs and calling the function.+target :: Testable f+ => f -- ^ the function+ -> TH.Name -- ^ the name of the function+ -> FilePath -- ^ the path to the module that defines the function+ -> IO ()+target f name path+ = targetWith f name path defaultOpts++-- targetTH :: TH.ExpQ -- (TH.TExp (Testable f => f -> TH.Name -> IO ()))+-- targetTH = TH.location >>= \TH.Loc {..} ->+-- [| \ f n -> target f (show n) loc_filename |]++-- | Like 'target', but returns the 'Result' instead of printing to standard out.+targetResult :: Testable f => f -> TH.Name -> FilePath -> IO Result+targetResult f name path+ = targetResultWith f name path defaultOpts++-- | Like 'target', but accepts options to control the enumeration depth,+-- solver, and verbosity.+targetWith :: Testable f => f -> TH.Name -> FilePath -> TargetOpts -> IO ()+targetWith f name path opts+ = do res <- targetResultWith f name path opts+ case res of+ Passed n -> printf "OK. Passed %d tests\n\n" n+ Failed x -> printf "Found counter-example: %s\n\n" x+ Errored x -> printf "Error! %s\n\n" x++-- | Like 'targetWith', but returns the 'Result' instead of printing to standard out.+targetResultWith :: Testable f => f -> TH.Name -> FilePath -> TargetOpts -> IO Result+targetResultWith f (show -> name) path opts+ = do when (verbose opts) $+ printf "Testing %s\n" name+ sp <- getSpec path+ ctx <- mkContext (solver opts)+ runTarget opts (initState path sp ctx) (do+ ty <- safeFromJust "targetResultWith" . lookup (symbol name) <$> gets sigs+ test f ty)+ `finally` killContext ctx+ where+ mkContext = if logging opts then makeContext else makeContextNoLog+ killContext ctx = terminateProcess (pId ctx) >> cleanupContext ctx++data Test = forall t. Testable t => T t
+ src/Test/Target/Eval.hs view
@@ -0,0 +1,172 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-}+module Test.Target.Eval ( eval, evalWith ) where++import Control.Arrow (second)+import Control.Applicative+import Control.Monad.Catch+import Control.Monad.State+import qualified Data.HashMap.Strict as M+import Data.List+import Data.Maybe+import Text.Printf++import qualified GHC+import Language.Fixpoint.SmtLib2+import Language.Fixpoint.Types hiding (R)+import Language.Haskell.Liquid.Types hiding (var)++import Test.Target.Expr+import Test.Target.Monad+import Test.Target.Types++-- import Debug.Trace++-- | Evaluate a refinement with the given expression substituted for the value+-- variable.+eval :: Reft -> Expr -> Target Bool+eval r e = do+ cts <- gets freesyms+ evalWith (M.fromList $ map (second (`app` [])) cts) r e++-- | Evaluate a refinement with the given expression substituted for the value+-- variable, in the given environment of free symbols.+evalWith :: M.HashMap Symbol Expr -> Reft -> Expr -> Target Bool+evalWith m (Reft (v, rs)) x+ = and <$> sequence [ evalPred p (M.insert v x m) | RConc p <- rs ]++evalPred :: Pred -> M.HashMap Symbol Expr -> Target Bool+evalPred PTrue _ = return True+evalPred PFalse _ = return False+evalPred (PAnd ps) m = and <$> sequence [evalPred p m | p <- ps]+evalPred (POr ps) m = or <$> sequence [evalPred p m | p <- ps]+evalPred (PNot p) m = not <$> evalPred p m+evalPred (PImp p q) m = do pv <- evalPred p m+ if pv+ then evalPred q m+ else return True+evalPred (PIff p q) m = and <$> sequence [ evalPred (p `imp` q) m+ , evalPred (q `imp` p) m+ ]+evalPred (PAtom b e1 e2) m = evalBrel b <$> evalExpr e1 m <*> evalExpr e2 m+evalPred (PBexp e) m = (==0) <$> evalExpr e m+evalPred p _ = throwM $ EvalError $ "evalPred: " ++ show p+-- evalPred (PAll ss p) m = undefined+-- evalPred PTop m = undefined++evalBrel :: Brel -> Expr -> Expr -> Bool+evalBrel Eq = (==)+evalBrel Ne = (/=)+evalBrel Ueq = (==)+evalBrel Une = (/=)+evalBrel Gt = (>)+evalBrel Ge = (>=)+evalBrel Lt = (<)+evalBrel Le = (<=)++applyMeasure :: Measure SpecType GHC.DataCon -> Expr -> M.HashMap Symbol Expr -> Target Expr+applyMeasure m (EApp c xs) env+ = meq >>= \eq -> evalBody eq xs env+ where+ ct = symbolString $ case val c of+ "GHC.Types.[]" -> "[]"+ "GHC.Types.:" -> ":"+ "GHC.Tuple.(,)" -> "(,)"+ "GHC.Tuple.(,,)" -> "(,,)"+ "GHC.Tuple.(,,,)" -> "(,,,)"+ "GHC.Tuple.(,,,,)" -> "(,,,,)"+ x -> x+ meq = case find ((==ct) . show . ctor) $ eqns m of+ Nothing -> throwM $ EvalError $ printf "applyMeasure(%s): no equation for %s" (show m) (show ct)+ Just x -> return x++applyMeasure m e _+ = throwM $ EvalError $ printf "applyMeasure(%s, %s)" (showpp m) (showpp e)++setSym :: Symbol+setSym = "LC_SET"++nubSort :: [Expr] -> [Expr]+nubSort = nub . Data.List.sort++mkSet :: [Expr] -> Expr+mkSet = app setSym . nubSort++evalSet :: Symbol -> [Expr] -> Target Expr+evalSet "Set_emp" [e]+ = return $ if e == app setSym [] then 0 else 1+evalSet "Set_sng" [e]+ = return $ mkSet [e]+evalSet "Set_add" [e1, EApp _ e2]+ = return $ mkSet $ e1:e2+evalSet "Set_cap" [EApp _ e1, EApp _ e2]+ = return $ mkSet $ intersect e1 e2+evalSet "Set_cup" [EApp _ e1, EApp _ e2]+ = return $ mkSet $ e1 ++ e2+evalSet "Set_dif" [EApp _ e1, EApp _ e2]+ = return $ mkSet $ e1 \\ e2+evalSet "Set_sub" [EApp _ e1, EApp _ e2]+ = return $ if null (e1 \\ e2) then 0 else 1+evalSet "Set_mem" [e1, EApp f e2] | val f == setSym+ = return $ if e1 `elem` e2 then 0 else 1+evalSet f es = throwM $ EvalError $ printf "evalSet(%s, %s)" (show f) (show es)++evalBody+ :: Language.Haskell.Liquid.Types.Def ctor+ -> [Expr] -> M.HashMap Symbol Expr -> Target Expr+evalBody eq xs env = go $ body eq+ where+ go (E e) = evalExpr (subst su e) env+ go (P p) = evalPred (subst su p) env >>= \b -> return $ if b then 0 else 1+ go (R v p) = do e <- evalRel v (subst su p) env+ case e of+ Nothing -> throwM $ EvalError $ "evalBody can't handle: " ++ show (R v p)+ Just e -> return e+ --go (R v (PBexp (EApp f e))) | val f == "Set_emp" = return $ app setSym []+ ----FIXME: figure out how to handle the general case..+ --go (R v p) = return (ECon (I 0))+ su = mkSubst $ zip (binds eq) xs++evalRel :: Symbol -> Pred -> M.HashMap Symbol Expr -> Target (Maybe Expr)+evalRel v (PAnd ps) m = Just . head . catMaybes <$> sequence [evalRel v p m | p <- ps]+evalRel v (PImp p q) m = do pv <- evalPred p m+ if pv+ then evalRel v q m+ else return Nothing+evalRel v (PAtom Eq (EVar v') e2) m+ | v == v'+ = Just <$> evalExpr e2 m+evalRel v (PBexp (EApp f [EVar v'])) _+ | v == v' && val f == "Set_emp"+ = return $ Just $ app setSym []+evalRel _ p _+ = throwM $ EvalError $ "evalRel: " ++ show p++evalExpr :: Expr -> M.HashMap Symbol Expr -> Target Expr+evalExpr (ECon i) _ = return $ ECon i+evalExpr (EVar x) m = return $ m M.! x+evalExpr (ESym s) _ = return $ ESym s+evalExpr (EBin b e1 e2) m = evalBop b <$> evalExpr e1 m <*> evalExpr e2 m+evalExpr (EApp f es) m+ | val f == "Set_emp" || val f == "Set_sng" || val f `M.member` smt_set_funs+ = mapM (`evalExpr` m) es >>= \es' -> evalSet (val f) es'+ | otherwise+ = find ((==f) . name) <$> gets measEnv >>= \case+ Nothing -> EApp f <$> mapM (`evalExpr` m) es+ --FIXME: should really extend this to multi-param measures..+ Just ms -> do e' <- evalExpr (head es) m+ applyMeasure ms e' m+evalExpr (EIte p e1 e2) m+ = do b <- evalPred p m+ if b+ then evalExpr e1 m+ else evalExpr e2 m+evalExpr e _ = throwM $ EvalError $ printf "evalExpr(%s)" (show e)++evalBop :: Bop -> Expr -> Expr -> Expr+evalBop Plus (ECon (I x)) (ECon (I y)) = ECon . I $ x + y+evalBop Minus (ECon (I x)) (ECon (I y)) = ECon . I $ x - y+evalBop Times (ECon (I x)) (ECon (I y)) = ECon . I $ x * y+evalBop Div (ECon (I x)) (ECon (I y)) = ECon . I $ x `div` y+evalBop Mod (ECon (I x)) (ECon (I y)) = ECon . I $ x `mod` y+evalBop b e1 e2 = error $ printf "evalBop(%s, %s, %s)" (show b) (show e1) (show e2)
+ src/Test/Target/Expr.hs view
@@ -0,0 +1,68 @@+module Test.Target.Expr where++import Language.Fixpoint.Types+++eq :: Expr -> Expr -> Pred+eq = PAtom Eq+infix 4 `eq`++ge :: Expr -> Expr -> Pred+ge = PAtom Ge+infix 5 `ge`++le :: Expr -> Expr -> Pred+le = PAtom Le+infix 5 `le`++gt :: Expr -> Expr -> Pred+gt = PAtom Gt+infix 5 `gt`++lt :: Expr -> Expr -> Pred+lt = PAtom Lt+infix 5 `lt`++iff :: Pred -> Pred -> Pred+iff = PIff+infix 3 `iff`++imp :: Pred -> Pred -> Pred+imp = PImp+infix 3 `imp`+++app :: Symbolic a => a -> [Expr] -> Expr+app f es = EApp (dummyLoc $ symbol f) es++var :: Symbolic a => a -> Expr+var = EVar . symbol++-- prop :: Symbolic a => a -> Pred+-- prop = PBexp . EVar . symbol+prop :: Expr -> Pred+prop = PBexp++instance Num Expr where+ fromInteger = ECon . I . fromInteger+ (+) = EBin Plus+ (-) = EBin Minus+ (*) = EBin Times+ abs = error "abs of Liquid.Fixpoint.Types.Expr"+ signum = error "signum of Liquid.Fixpoint.Types.Expr"++instance Real Expr where+ toRational (ECon (I i)) = fromIntegral i+ toRational x = error $ "toRational: " ++ show x++instance Enum Expr where+ toEnum = ECon . I . fromIntegral+ fromEnum (ECon (I i)) = fromInteger i+ fromEnum x = error $ "fromEnum: " ++ show x++instance Integral Expr where+ div = EBin Div+ mod = EBin Mod+ quotRem x y = (x `div` y, x `mod` y)+ toInteger (ECon (I i)) = i+ toInteger x = error $ "toInteger: " ++ show x
+ src/Test/Target/Monad.hs view
@@ -0,0 +1,270 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RecordWildCards #-}+module Test.Target.Monad+ ( whenVerbose+ , noteUsed+ , addDep+ , addConstraint+ , addConstructor+ , inModule+ , making+ , lookupCtor+ , guarded+ , fresh+ , freshChoice+ , freshInt+ , getValue+ , Target, runTarget+ , TargetState(..), initState+ , TargetOpts(..), defaultOpts+ ) where++import Control.Applicative+import Control.Arrow (first, (***))+import qualified Control.Exception as Ex+import Control.Monad+import Control.Monad.Catch+import Control.Monad.Reader+import Control.Monad.State+import Data.Generics (Data, everywhere, mkT)+import qualified Data.HashMap.Strict as M+import qualified Data.HashSet as S+import Data.IORef+import Data.List hiding (sort)+import Data.Monoid+import qualified Data.Text.Lazy as LT+import System.IO.Unsafe+import Text.Printf++import Language.Fixpoint.Config (SMTSolver (..))+import Language.Fixpoint.Names+import Language.Fixpoint.SmtLib2 hiding (verbose)+import Language.Fixpoint.Types+import Language.Haskell.Liquid.PredType+import Language.Haskell.Liquid.RefType+import Language.Haskell.Liquid.Tidy+import Language.Haskell.Liquid.Types hiding (var, Target)++import qualified GHC++import Test.Target.Types+import Test.Target.Util++-- import Debug.Trace+++instance Symbolic LT.Text where+ symbol = symbol . LT.toStrict++newtype Target a = Target (StateT TargetState (ReaderT TargetOpts IO) a)+ deriving ( Functor, Applicative, Monad, MonadIO, Alternative+ , MonadState TargetState, MonadCatch, MonadReader TargetOpts )+instance MonadThrow Target where+ throwM = Ex.throw++runTarget :: TargetOpts -> TargetState -> Target a -> IO a+runTarget opts st (Target x) = runReaderT (evalStateT x st) opts++-- evalTarget :: TargetOpts -> TargetState -> Target a -> IO a+-- evalTarget o s (Target x) = runReaderT (evalStateT x s) o++-- execTarget :: GhcSpec -> Target a -> IO TargetState+-- execTarget e (Target x) = execStateT x (initGS e)++seed :: IORef Int+seed = unsafePerformIO $ newIORef 0+{-# NOINLINE seed #-}++freshInt :: Target Int+freshInt = liftIO $ do+ n <- readIORef seed+ modifyIORef' seed (+1)+ return n++data TargetOpts = TargetOpts+ { depth :: !Int+ , solver :: !SMTSolver+ , verbose :: !Bool+ , logging :: !Bool+ , keepGoing :: !Bool+ -- ^ whether to keep going after finding a counter-example, useful for+ -- checking coverage+ , maxSuccess :: !(Maybe Int)+ -- ^ whether to stop after a certain number of successful tests, or+ -- enumerate the whole input space+ , scDepth :: !Bool+ -- ^ whether to use SmallCheck's notion of depth+ }++defaultOpts :: TargetOpts+defaultOpts = TargetOpts+ { depth = 5+ , solver = Z3+ , verbose = False+ , logging = True+ , keepGoing = False+ , maxSuccess = Nothing+ , scDepth = False+ }++data TargetState = TargetState+ { variables :: ![Variable]+ , choices :: ![Variable]+ , constraints :: !Constraint+ , deps :: !(M.HashMap Symbol [Symbol])+ , realized :: ![(Symbol, Value)]+ , dconEnv :: ![(Symbol, DataConP)]+ , ctorEnv :: !DataConEnv+ , measEnv :: !MeasureEnv+ , embEnv :: !(TCEmb GHC.TyCon)+ , tyconInfo :: !(M.HashMap GHC.TyCon RTyCon)+ , freesyms :: ![(Symbol,Symbol)]+ , constructors :: ![Variable] -- (S.HashSet Variable) --[(String, String)]+ , sigs :: ![(Symbol, SpecType)]+ , chosen :: !(Maybe Symbol)+ , sorts :: !(S.HashSet Sort)+ , modName :: !Symbol+ , filePath :: !FilePath+ , makingTy :: !Sort+ , smtContext :: !Context+ }++initState :: FilePath -> GhcSpec -> Context -> TargetState+initState fp sp ctx = TargetState+ { variables = []+ , choices = []+ , constraints = []+ , deps = mempty+ , realized = []+ , dconEnv = dcons+ , ctorEnv = cts+ , measEnv = meas+ , embEnv = tcEmbeds sp+ , tyconInfo = tyi+ , freesyms = free+ , constructors = []+ , sigs = sigs+ , chosen = Nothing+ , sorts = S.empty+ , modName = ""+ , filePath = fp+ , makingTy = FObj ""+ , smtContext = ctx+ }+ where+ dcons = tidy $ map (first symbol) (dconsP sp)+ cts = tidy $ map (symbol *** val) (ctors sp)+ tyi = tidy $ makeTyConInfo (tconsP sp)+ free = tidy $ map (symbol *** symbol) $ freeSyms sp+ sigs = tidy $ map (symbol *** val) $ tySigs sp+ meas = tidy $ measures sp+ tidy :: forall a. Data a => a -> a+ tidy = everywhere (mkT tidySymbol)++whenVerbose :: Target () -> Target ()+whenVerbose x+ = do v <- asks verbose+ when v x++noteUsed :: (Symbol, Value) -> Target ()+noteUsed (v,x) = modify $ \s@(TargetState {..}) -> s { realized = (v,x) : realized }++-- TODO: does this type make sense? should it be Symbol -> Symbol -> Target ()?+addDep :: Symbol -> Expr -> Target ()+addDep from (EVar to) = modify $ \s@(TargetState {..}) ->+ s { deps = M.insertWith (flip (++)) from [to] deps }+addDep _ _ = return ()++addConstraint :: Pred -> Target ()+addConstraint p = modify $ \s@(TargetState {..}) -> s { constraints = p:constraints }++addConstructor :: Variable -> Target ()+addConstructor c+ = do -- modify $ \s@(TargetState {..}) -> s { constructors = S.insert c constructors }+ modify $ \s@(TargetState {..}) -> s { constructors = nub $ c:constructors }++inModule :: Symbol -> Target a -> Target a+inModule m act+ = do m' <- gets modName+ modify $ \s -> s { modName = m }+ r <- act+ modify $ \s -> s { modName = m' }+ return r++making :: Sort -> Target a -> Target a+making ty act+ = do ty' <- gets makingTy+ modify $ \s -> s { makingTy = ty }+ r <- act+ modify $ \s -> s { makingTy = ty' }+ return r++-- | Find the refined type of a data constructor.+lookupCtor :: Symbol -> Target SpecType+lookupCtor c+ = do mt <- lookup c <$> gets ctorEnv+ m <- gets filePath+ case mt of+ Just t -> return t+ Nothing -> do+ t <- io $ runGhc $ do+ _ <- loadModule m+ t <- GHC.exprType (printf "(%s)" (symbolString c))+ return (ofType t)+ modify $ \s@(TargetState {..}) -> s { ctorEnv = (c,t) : ctorEnv }+ return t++-- | Given a data constructor @d@ and an action, create a new choice variable+-- @c@ and execute the action while guarding any generated constraints with+-- @c@. Returns @(action-result, c)@.+guarded :: String -> Target Expr -> Target (Expr, Expr)+guarded cn act+ = do c <- freshChoice cn+ mc <- gets chosen+ modify $ \s -> s { chosen = Just c }+ x <- act+ modify $ \s -> s { chosen = mc }+ return (x, EVar c)++-- | Generate a fresh variable of the given 'Sort'.+fresh :: Sort -> Target Symbol+fresh sort+ = do n <- freshInt+ let sorts' = sortTys sort+ modify $ \s@(TargetState {..}) -> s { sorts = S.union (S.fromList (arrowize sort : sorts')) sorts }+ let x = symbol $ LT.unpack (LT.intercalate "->" $ map (LT.fromStrict.symbolText.unObj) sorts') ++ show n+ modify $ \s@(TargetState {..}) -> s { variables = (x,sort) : variables }+ return x++sortTys :: Sort -> [Sort]+sortTys (FFunc _ ts) = concatMap sortTys ts+sortTys t = [t]++arrowize :: Sort -> Sort+arrowize = FObj . symbol . LT.intercalate "->" . map (LT.fromStrict . symbolText . unObj) . sortTys++unObj :: Sort -> Symbol+unObj FInt = "Int"+unObj (FObj s) = s+unObj s = error $ "unObj: " ++ show s++-- | Given a data constructor @d@, create a new choice variable corresponding to+-- @d@.+freshChoice :: String -> Target Symbol+freshChoice cn+ = do n <- freshInt+ modify $ \s@(TargetState {..}) -> s { sorts = S.insert choicesort sorts }+ let x = symbol $ LT.unpack (smt2 choicesort) ++ "-" ++ cn ++ "-" ++ show n+ modify $ \s@(TargetState {..}) -> s { variables = (x,choicesort) : variables }+ return x++-- | Ask the SMT solver for the 'Value' of the given variable.+getValue :: Symbol -> Target Value+getValue v = do+ ctx <- gets smtContext+ Values [x] <- io $ ensureValues $ command ctx (GetValue [v])+ noteUsed x+ return (snd x)+
+ src/Test/Target/Targetable.hs view
@@ -0,0 +1,543 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-}+module Test.Target.Targetable+ ( Targetable(..)+ , unfold, apply, unapply+ , oneOf, whichOf+ , constrain, ofReft+ ) where++import Control.Applicative+import Control.Arrow (second)+import qualified Control.Monad.Catch as Ex+import Control.Monad.Reader+import Control.Monad.State+import Data.Char+import qualified Data.HashMap.Strict as M+import Data.List+import Data.Maybe+import Data.Monoid+import Data.Proxy+import qualified Data.Text as T+import Data.Word (Word8)+import GHC.Generics++import Language.Fixpoint.Types hiding (prop, ofReft)+import Language.Haskell.Liquid.RefType+import Language.Haskell.Liquid.Types hiding (var)++import Test.Target.Expr+import Test.Target.Eval+import Test.Target.Monad+import Test.Target.Types+import Test.Target.Util++-- import Debug.Trace++--------------------------------------------------------------------------------+--- Constrainable Data+--------------------------------------------------------------------------------+-- | A class of datatypes for which we can efficiently generate constrained+-- values by querying an SMT solver.+--+-- If possible, instances should not be written by hand, but rather by using the+-- default implementations via "GHC.Generics", e.g.+--+-- > import GHC.Generics+-- > import Test.Target.Targetable+-- >+-- > data Foo = ... deriving Generic+-- > instance Targetable Foo+class Targetable a where+ -- | Construct an SMT query describing all values of the given type up to the+ -- given 'Depth'.+ query :: Proxy a -> Depth -> SpecType -> Target Symbol++ -- | Reconstruct a Haskell value from the SMT model.+ decode :: Symbol+ -- ^ the symbolic variable corresponding to the root of the value+ -> SpecType+ -- ^ the type of values we're generating (you can probably ignore this)+ -> Target a++ -- | Check whether a Haskell value inhabits the given type. Also returns a+ -- logical expression corresponding to the Haskell value.+ check :: a -> SpecType -> Target (Bool, Expr)++ -- | Translate a Haskell value into a logical expression.+ toExpr :: a -> Expr++ -- | What is the Haskell type? (Mainly used to make the SMT queries more+ -- readable).+ getType :: Proxy a -> Sort++ default getType :: (Generic a, Rep a ~ D1 d f, Datatype d)+ => Proxy a -> Sort+ getType _ = FObj $ qualifiedDatatypeName (undefined :: Rep a a)++ default query :: (Generic a, GQuery (Rep a))+ => Proxy a -> Int -> SpecType -> Target Symbol+ query p = gquery (reproxyRep p)++ default toExpr :: (Generic a, GToExpr (Rep a))+ => a -> Expr+ toExpr = gtoExpr . from++ default decode :: (Generic a, GDecode (Rep a))+ => Symbol -> SpecType -> Target a+ decode v _ = do+ x <- whichOf v+ (c, fs) <- unapply x+ to <$> gdecode c fs++ default check :: (Generic a, GCheck (Rep a))+ => a -> SpecType -> Target (Bool, Expr)+ check v t = gcheck (from v) t++reproxy :: proxy a -> Proxy b+reproxy _ = Proxy+{-# INLINE reproxy #-}++-- | Given a data constuctor @d@ and a refined type for @d@s output,+-- return a list of types representing suitable arguments for @d@.+unfold :: Symbol -> SpecType -> Target [(Symbol, SpecType)]+unfold cn t = do+ dcp <- lookupCtor cn+ tyi <- gets tyconInfo+ emb <- gets embEnv+ let ts = applyPreds (addTyConInfo emb tyi t) dcp+ return ts++-- | Given a data constructor @d@ and a list of expressions @xs@, construct a+-- new expression corresponding to @d xs@.+apply :: Symbol -> [Expr] -> Target Expr+apply c vs = do + mc <- gets chosen+ case mc of+ Just ch -> mapM_ (addDep ch) vs+ Nothing -> return ()+ let x = app c vs+ t <- lookupCtor c+ let (xs, _, rt) = bkArrowDeep t+ su = mkSubst $ zip (map symbol xs) vs+ addConstructor (c, rTypeSort mempty t)+ constrain $ ofReft (subst su $ reft rt) x+ return x++-- | Split a symbolic variable representing the application of a data+-- constructor into a pair of the data constructor and the sub-variables.+unapply :: Symbol -> Target (Symbol, [Symbol])+unapply c = do+ let [_,cn,_] = T.splitOn "-" $ symbolText c+ deps <- gets deps+ return (symbol cn, M.lookupDefault [] c deps)++-- | Given a symbolic variable and a list of @(choice, var)@ pairs,+-- @oneOf x choices@ asserts that @x@ must equal one of the @var@s in+-- @choices@.+oneOf :: Symbol -> [(Expr,Expr)] -> Target ()+oneOf x cs+ = do cs <- forM cs $ \(y,c) -> do+ addDep x c+ constrain $ prop c `imp` (var x `eq` y)+ return $ prop c+ constrain $ pOr cs+ constrain $ pAnd [ PNot $ pAnd [x, y]+ | [x, y] <- filter ((==2) . length) $ subsequences cs ]++-- | Given a symbolic variable @x@, figure out which of @x@s choice varaibles+-- was picked and return it.+whichOf :: Symbol -> Target Symbol+whichOf v = do+ deps <- gets deps+ let Just cs = M.lookup v deps+ [c] <- catMaybes <$> forM cs (\c -> do+ val <- getValue c+ if val == "true"+ then return (Just c)+ else return Nothing)+ return c+++-- | Assert a logical predicate, guarded by the current choice variable.+constrain :: Pred -> Target ()+constrain p = do+ mc <- gets chosen+ case mc of+ Nothing -> addConstraint p+ Just c -> let p' = prop (var c) `imp` p+ in addConstraint p'++-- | Given a refinement @{v | p}@ and an expression @e@, construct+-- the predicate @p[e/v]@.+ofReft :: Reft -> Expr -> Pred+ofReft (Reft (v, rs)) e+ = let x = mkSubst [(v, e)]+ in pAnd [subst x p | RConc p <- rs]++--------------------------------------------------------------------------------+--- Instances+--------------------------------------------------------------------------------+instance Targetable () where+ getType _ = FObj "GHC.Tuple.()"+ query _ _ _ = fresh (FObj "GHC.Tuple.()")+ -- this is super fiddly, but seemingly required since GHC.exprType chokes on "GHC.Tuple.()"+ toExpr _ = app ("()" :: Symbol) []++ decode _ _ = return ()+ check _ t = do+ let e = app ("()" :: Symbol) []+ b <- eval (reft t) e+ return (b,e)++instance Targetable Int where+ getType _ = FObj "GHC.Types.Int"+ query _ d t = fresh FInt >>= \x ->+ do constrain $ ofReft (reft t) (var x)+ -- use the unfolding depth to constrain the range of Ints, like QuickCheck+ constrain $ var x `ge` fromIntegral (negate d)+ constrain $ var x `le` fromIntegral d+ return x+ toExpr i = ECon $ I $ fromIntegral i++ decode v _ = read . T.unpack <$> getValue v++ check v t = do+ let e = fromIntegral v+ b <- eval (reft t) e+ return (b, e)++instance Targetable Integer where+ getType _ = FObj "GHC.Integer.Type.Integer"+ query _ d t = query (Proxy :: Proxy Int) d t+ toExpr x = toExpr (fromIntegral x :: Int)++ decode v t = decode v t >>= \(x::Int) -> return . fromIntegral $ x++ check v t = do+ let e = fromIntegral v+ b <- eval (reft t) e+ return (b, e)++instance Targetable Char where+ getType _ = FObj "GHC.Types.Char"+ query _ d t = fresh FInt >>= \x ->+ do constrain $ var x `ge` 0+ constrain $ var x `le` fromIntegral d+ constrain $ ofReft (reft t) (var x)+ return x+ toExpr c = ESym $ SL $ T.singleton c++ decode v t = decode v t >>= \(x::Int) -> return . chr $ x + ord 'a'++ check v t = do+ let e = ESym $ SL $ T.singleton v+ b <- eval (reft t) e+ return (b, e)++instance Targetable Word8 where+ getType _ = FObj "GHC.Word.Word8"+ query _ d t = fresh FInt >>= \x ->+ do _ <- asks depth+ constrain $ var x `ge` 0+ constrain $ var x `le` fromIntegral d+ constrain $ ofReft (reft t) (var x)+ return x+ toExpr i = ECon $ I $ fromIntegral i++ decode v t = decode v t >>= \(x::Int) -> return $ fromIntegral x++ check v t = do+ let e = fromIntegral v+ b <- eval (reft t) e+ return (b, e)++instance Targetable Bool where+ getType _ = FObj "GHC.Types.Bool"+ query _ _ t = fresh boolsort >>= \x ->+ do constrain $ ofReft (reft t) (var x)+ return x++ decode v _ = getValue v >>= \case+ "true" -> return True+ "false" -> return False+ x -> Ex.throwM (SmtError $ "expected boolean, got: " ++ T.unpack x)+++instance Targetable a => Targetable [a]+instance Targetable a => Targetable (Maybe a)+instance (Targetable a, Targetable b) => Targetable (Either a b)+instance (Targetable a, Targetable b) => Targetable (a,b)+instance (Targetable a, Targetable b, Targetable c) => Targetable (a,b,c)+instance (Targetable a, Targetable b, Targetable c, Targetable d) => Targetable (a,b,c,d)+++-- instance (Num a, Integral a, Targetable a) => Targetable (Ratio a) where+-- getType _ = FObj "GHC.Real.Ratio"+-- query _ d t = query (Proxy :: Proxy Int) d t+-- decode v t= decode v t >>= \ (x::Int) -> return (fromIntegral x)+-- -- query _ d t = fresh (FObj "GHC.Real.Ratio") >>= \x ->+-- -- do query (Proxy :: Proxy Int) d t+-- -- query (Proxy :: Proxy Int) d t+-- -- return x+-- -- stitch d t = do x :: Int <- stitch d t+-- -- y' :: Int <- stitch d t+-- -- -- we should really modify `t' above to have Z3 generate non-zero denoms+-- -- let y = if y' == 0 then 1 else y'+-- -- let toA z = fromIntegral z :: a+-- -- return $ toA x % toA y+-- toExpr x = EApp (dummyLoc "GHC.Real.:%") [toExpr (numerator x), toExpr (denominator x)]+-- check = undefined+++reproxyRep :: Proxy a -> Proxy (Rep a a)+reproxyRep = reproxy+++--------------------------------------------------------------------------------+--- Sums of Products+--------------------------------------------------------------------------------+class GToExpr f where+ gtoExpr :: f a -> Expr++class GQuery f where+ gquery :: Proxy (f a) -> Int -> SpecType -> Target Symbol++class GDecode f where+ gdecode :: Symbol -> [Symbol] -> Target (f a)++class GCheck f where+ gcheck :: f a -> SpecType -> Target (Bool, Expr)++reproxyGElem :: Proxy (M1 d c f a) -> Proxy (f a)+reproxyGElem = reproxy++instance (Datatype c, GToExprCtor f) => GToExpr (D1 c f) where+ gtoExpr (M1 x) = app (qualify mod (symbolString $ val d)) xs+ where+ mod = GHC.Generics.moduleName (undefined :: D1 c f a)+ (EApp d xs) = gtoExprCtor x++instance (Datatype c, GQueryCtors f) => GQuery (D1 c f) where+ gquery p d t = inModule mod . making sort $ do+ xs <- gqueryCtors (reproxyGElem p) d t+ x <- fresh sort+ oneOf x xs+ constrain $ ofReft (reft t) (var x)+ return x+ where+ mod = symbol $ GHC.Generics.moduleName (undefined :: D1 c f a)+ sort = FObj $ qualifiedDatatypeName (undefined :: D1 c f a)++instance (Datatype c, GDecode f) => GDecode (D1 c f) where+ gdecode c vs = M1 <$> making sort (gdecode c vs)+ where+ sort = FObj $ qualifiedDatatypeName (undefined :: D1 c f a)++instance (Datatype c, GCheck f) => GCheck (D1 c f) where+ gcheck (M1 x) t = inModule mod . making sort $ gcheck x t+ where+ mod = symbol $ GHC.Generics.moduleName (undefined :: D1 c f a)+ sort = FObj $ qualifiedDatatypeName (undefined :: D1 c f a)+++instance (Targetable a) => GToExpr (K1 i a) where+ gtoExpr (K1 x) = toExpr x++instance (Targetable a) => GQuery (K1 i a) where+ gquery p d t = do + let p' = reproxy p :: Proxy a+ ty <- gets makingTy+ depth <- asks depth+ sc <- asks scDepth+ let d' = if getType p' == ty || sc+ then d+ else depth+ query p' d' t++instance Targetable a => GDecodeFields (K1 i a) where+ gdecodeFields (v:vs) = do+ x <- decode v undefined+ return (vs, K1 x)+ gdecodeFields _ = error "gdecodeFields []"++instance Targetable a => GCheckFields (K1 i a) where+ gcheckFields (K1 x) ((f,t):ts) = do+ (b, v) <- check x t+ return (b, [v], subst (mkSubst [(f, v)]) ts)+ gcheckFields _ _ = error "gcheckFields _ []"++qualify :: String -> String -> String+qualify m x = m ++ ('.':x)+{-# INLINE qualify #-}++qualifiedDatatypeName :: Datatype d => D1 d f a -> Symbol+qualifiedDatatypeName d = symbol $ qualify m (datatypeName d)+ where m = GHC.Generics.moduleName d+{-# INLINE qualifiedDatatypeName #-}++--------------------------------------------------------------------------------+--- Sums+--------------------------------------------------------------------------------+class GToExprCtor f where+ gtoExprCtor :: f a -> Expr++class GQueryCtors f where+ gqueryCtors :: Proxy (f a) -> Int -> SpecType -> Target [(Expr, Expr)]++reproxyLeft :: Proxy ((c (f :: * -> *) (g :: * -> *)) a) -> Proxy (f a)+reproxyLeft = reproxy++reproxyRight :: Proxy ((c (f :: * -> *) (g :: * -> *)) a) -> Proxy (g a)+reproxyRight = reproxy++instance (GToExprCtor f, GToExprCtor g) => GToExprCtor (f :+: g) where+ gtoExprCtor (L1 x) = gtoExprCtor x+ gtoExprCtor (R1 x) = gtoExprCtor x++instance (GQueryCtors f, GQueryCtors g) => GQueryCtors (f :+: g) where+ gqueryCtors p d t = do + xs <- gqueryCtors (reproxyLeft p) d t+ ys <- gqueryCtors (reproxyRight p) d t+ return $! xs++ys++instance (GDecode f, GDecode g) => GDecode (f :+: g) where+ gdecode c vs = L1 <$> gdecode c vs+ <|> R1 <$> gdecode c vs++instance (GCheck f, GCheck g) => GCheck (f :+: g) where+ gcheck (L1 x) t = gcheck x t+ gcheck (R1 x) t = gcheck x t+++instance (Constructor c, GToExprFields f) => GToExprCtor (C1 c f) where+ gtoExprCtor c@(M1 x) = app (symbol $ conName c) (gtoExprFields x)++instance (Constructor c, GRecursive f, GQueryFields f) => GQueryCtors (C1 c f) where+ gqueryCtors p d t | d <= 0+ = do ty <- gets makingTy+ if gisRecursive p ty+ then return []+ else pure <$> gqueryCtor p 0 t+ gqueryCtors p d t = pure <$> gqueryCtor p d t++instance (Constructor c, GDecodeFields f) => GDecode (C1 c f) where+ gdecode c vs+ | c == symbol (conName (undefined :: C1 c f a))+ = M1 . snd <$> gdecodeFields vs+ | otherwise+ = empty++instance (Constructor c, GCheckFields f) => GCheck (C1 c f) where+ gcheck (M1 x) t = do+ mod <- symbolString <$> gets modName+ let cn = symbol $ qualify mod (conName (undefined :: C1 c f a))+ ts <- unfold cn t+ (b, vs, _) <- gcheckFields x ts+ let v = app cn vs+ b' <- eval (reft t) v+ return (b && b', v)++gisRecursive :: (Constructor c, GRecursive f)+ => Proxy (C1 c f a) -> Sort -> Bool+gisRecursive (p :: Proxy (C1 c f a)) t+ = t `elem` gconArgTys (reproxyGElem p)++gqueryCtor :: (Constructor c, GQueryFields f)+ => Proxy (C1 c f a) -> Int -> SpecType -> Target (Expr, Expr)+gqueryCtor (p :: Proxy (C1 c f a)) d t+ = guarded cn $ do+ mod <- symbolString <$> gets modName+ ts <- unfold (symbol $ qualify mod cn) t+ xs <- gqueryFields (reproxyGElem p) d ts+ apply (symbol $ qualify mod cn) xs+ where+ cn = conName (undefined :: C1 c f a)++--------------------------------------------------------------------------------+--- Products+--------------------------------------------------------------------------------+class GToExprFields f where+ gtoExprFields :: f a -> [Expr]++class GRecursive f where+ gconArgTys :: Proxy (f a) -> [Sort]++class GQueryFields f where+ gqueryFields :: Proxy (f a) -> Int -> [(Symbol,SpecType)] -> Target [Expr]++class GDecodeFields f where+ gdecodeFields :: [Symbol] -> Target ([Symbol], f a)++class GCheckFields f where+ gcheckFields :: f a -> [(Symbol, SpecType)]+ -> Target (Bool, [Expr], [(Symbol, SpecType)])+++instance (GToExprFields f, GToExprFields g) => GToExprFields (f :*: g) where+ gtoExprFields (f :*: g) = gtoExprFields f ++ gtoExprFields g++instance (GRecursive f, GRecursive g) => GRecursive (f :*: g) where+ gconArgTys p = gconArgTys (reproxyLeft p) ++ gconArgTys (reproxyRight p)++instance (GQueryFields f, GQueryFields g) => GQueryFields (f :*: g) where+ gqueryFields p d ts = do + xs <- gqueryFields (reproxyLeft p) d ts+ let su = mkSubst $ zipWith (\x t -> (fst t, x)) xs ts+ let ts' = drop (length xs) ts+ ys <- gqueryFields (reproxyRight p) d (map (second (subst su)) ts')+ return $ xs ++ ys++instance (GDecodeFields f, GDecodeFields g) => GDecodeFields (f :*: g) where+ gdecodeFields vs = do+ (vs', ls) <- gdecodeFields vs+ (vs'', rs) <- gdecodeFields vs'+ return (vs'', ls :*: rs)++instance (GCheckFields f, GCheckFields g) => GCheckFields (f :*: g) where+ gcheckFields (f :*: g) ts = do+ (bl,fs,ts') <- gcheckFields f ts+ (br,gs,ts'') <- gcheckFields g ts'+ return (bl && br, fs ++ gs, ts'')+++instance (GToExpr f) => GToExprFields (S1 c f) where+ gtoExprFields (M1 x) = [gtoExpr x]++instance Targetable a => GRecursive (S1 c (K1 i a)) where+ gconArgTys _ = [getType (Proxy :: Proxy a)]++instance (GQuery f) => GQueryFields (S1 c f) where+ gqueryFields p d (t:_) = sequence [var <$> gquery (reproxyGElem p) (d-1) (snd t)]+ gqueryFields _ _ _ = error "gqueryfields _ _ []"++instance GDecodeFields f => GDecodeFields (S1 c f) where+ gdecodeFields vs = do+ (vs', x) <- gdecodeFields vs+ return (vs', M1 x)++instance (GCheckFields f) => GCheckFields (S1 c f) where+ gcheckFields (M1 x) ts = gcheckFields x ts++instance GToExprFields U1 where+ gtoExprFields _ = []++instance GRecursive U1 where+ gconArgTys _ = []++instance GQueryFields U1 where+ gqueryFields _ _ _ = return []++instance GDecodeFields U1 where+ gdecodeFields vs = return (vs, U1)++instance GCheckFields U1 where+ gcheckFields _ ts = return (True, [], ts)
+ src/Test/Target/Targetable/Function.hs view
@@ -0,0 +1,177 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE OverlappingInstances #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ViewPatterns #-}++module Test.Target.Targetable.Function () where++import Control.Applicative+import Control.Arrow (second)+import Control.Monad+import qualified Control.Monad.Catch as Ex+import Control.Monad.Reader+import Control.Monad.State+import Data.Char+import qualified Data.HashMap.Strict as M+import Data.IORef+import Data.Monoid+import Data.Proxy+import qualified Data.Text as T+import qualified GHC+import Language.Fixpoint.SmtLib2+import Language.Fixpoint.Types hiding (ofReft)+import Language.Haskell.Liquid.GhcMisc (qualifiedNameSymbol)+import Language.Haskell.Liquid.RefType (addTyConInfo, rTypeSort)+import Language.Haskell.Liquid.Types hiding (var)+import System.IO.Unsafe++import Test.Target.Targetable+import Test.Target.Eval+import Test.Target.Expr+import Test.Target.Monad+import Test.Target.Types+import Test.Target.Util+++getCtors :: SpecType -> [GHC.DataCon]+getCtors (RApp c _ _ _) = GHC.tyConDataCons $ rtc_tc c+getCtors (RAppTy t _ _) = getCtors t+getCtors (RFun _ i o _) = getCtors i ++ getCtors o+getCtors (RVar _ _) = []+getCtors t = error $ "getCtors: " ++ showpp t++dataConSymbol_noUnique :: GHC.DataCon -> Symbol+dataConSymbol_noUnique = qualifiedNameSymbol . GHC.getName++genFun :: Targetable a => Proxy a -> t -> SpecType -> Target Symbol+genFun p _ (stripQuals -> t)+ = do forM_ (getCtors t) $ \dc -> do+ let c = dataConSymbol_noUnique dc+ t <- lookupCtor c+ addConstructor (c, rTypeSort mempty t)+ fresh (getType p)++stitchFun :: forall f. (Targetable (Res f))+ => Proxy f -> SpecType -> Target ([Expr] -> Res f)+stitchFun _ (bkArrowDeep . stripQuals -> (vs, tis, to))+ = do mref <- io $ newIORef []+ d <- asks depth+ state' <- get+ opts <- ask+ let st = state' { variables = [], choices = [], constraints = []+ , deps = mempty, constructors = [] }+ return $ \es -> unsafePerformIO $ runTarget opts st $ do+ -- let es = map toExpr xs+ mv <- lookup es <$> io (readIORef mref)+ case mv of+ Just v -> return v+ Nothing -> do+ cts <- gets freesyms+ let env = map (second (`app` [])) cts+ bs <- zipWithM (evalType (M.fromList env)) tis es+ case and bs of+ --FIXME: better error message+ False -> Ex.throwM $ PreconditionCheckFailed $ show $ zip es tis+ True -> do+ ctx <- gets smtContext+ _ <- io $ command ctx Push+ xes <- mapM genExpr es+ let su = mkSubst $ zipWith (\v e -> (v, var e)) vs xes+ xo <- query (Proxy :: Proxy (Res f)) d (subst su to)+ vs <- gets variables+ mapM_ (\x -> io . command ctx $ Declare (symbol x) [] (snd x)) vs+ cs <- gets constraints+ mapM_ (\c -> io . command ctx $ Assert Nothing c) cs++ resp <- io $ command ctx CheckSat+ when (resp == Unsat) $ Ex.throwM SmtFailedToProduceOutput++ o <- decode xo to+ -- whenVerbose $ io $ printf "%s -> %s\n" (show es) (show o)+ io (modifyIORef' mref ((es,o):))+ _ <- io $ command ctx Pop+ return o+ +genExpr :: Expr -> Target Symbol+genExpr (EApp (val -> c) es)+ = do xes <- mapM genExpr es+ (xs, _, to) <- bkArrowDeep . stripQuals <$> lookupCtor c+ let su = mkSubst $ zip xs $ map var xes+ to' = subst su to+ x <- fresh $ FObj $ symbol $ rtc_tc $ rt_tycon to'+ addConstraint $ ofReft (reft to') (var x)+ return x+genExpr (ECon (I i))+ = do x <- fresh FInt+ addConstraint $ var x `eq` expr i+ return x+genExpr (ESym (SL s)) | T.length s == 1+ -- This is a Char, so encode it as an Int+ = do x <- fresh FInt+ addConstraint $ var x `eq` expr (ord $ T.head s)+ return x+genExpr e = error $ "genExpr: " ++ show e++evalType :: M.HashMap Symbol Expr -> SpecType -> Expr -> Target Bool+evalType m t e@(EApp c xs)+ = do dcp <- lookupCtor (val c)+ tyi <- gets tyconInfo+ vts <- freshen $ applyPreds (addTyConInfo M.empty tyi t) dcp+ liftM2 (&&) (evalWith m (toReft $ rt_reft t) e) (evalTypes m vts xs)+evalType m t e+ = evalWith m (toReft $ rt_reft t) e++freshen :: [(Symbol, SpecType)] -> Target [(Symbol, SpecType)]+freshen [] = return []+freshen ((v,t):vts)+ = do n <- freshInt+ let v' = symbol . (++show n) . symbolString $ v+ su = mkSubst [(v,var v')]+ t' = subst su t+ vts' <- freshen $ subst su vts+ return ((v',t'):vts')++evalTypes+ :: M.HashMap Symbol Expr+ -> [(Symbol, SpecType)] -> [Expr] -> Target Bool+evalTypes _ [] [] = return True+evalTypes m ((v,t):ts) (x:xs)+ = liftM2 (&&) (evalType m' t x) (evalTypes m' ts xs)+ where+ m' = M.insert v x m+evalTypes _ _ _ = error "evalTypes called with lists of unequal length!"++instance (Targetable a, Targetable b, b ~ Res (a -> b))+ => Targetable (a -> b) where+ getType _ = FFunc 0 [getType (Proxy :: Proxy a), getType (Proxy :: Proxy b)]+ query = genFun+ decode _ t+ = do f <- stitchFun (Proxy :: Proxy (a -> b)) t+ return $ \a -> f [toExpr a]+ toExpr _ = var ("FUNCTION" :: Symbol)+ check _ _ = error "can't check a function!"++instance (Targetable a, Targetable b, Targetable c, c ~ Res (a -> b -> c))+ => Targetable (a -> b -> c) where+ getType _ = FFunc 0 [getType (Proxy :: Proxy a), getType (Proxy :: Proxy b)+ ,getType (Proxy :: Proxy c)]+ query = genFun+ decode _ t+ = do f <- stitchFun (Proxy :: Proxy (a -> b -> c)) t+ return $ \a b -> f [toExpr a, toExpr b]+ toExpr _ = var ("FUNCTION" :: Symbol)+ check _ _ = error "can't check a function!"++instance (Targetable a, Targetable b, Targetable c, Targetable d, d ~ Res (a -> b -> c -> d))+ => Targetable (a -> b -> c -> d) where+ getType _ = FFunc 0 [getType (Proxy :: Proxy a), getType (Proxy :: Proxy b)+ ,getType (Proxy :: Proxy c), getType (Proxy :: Proxy d)]+ query = genFun+ decode _ t+ = do f <- stitchFun (Proxy :: Proxy (a -> b -> c -> d)) t+ return $ \a b c -> f [toExpr a, toExpr b, toExpr c]+ toExpr _ = var ("FUNCTION" :: Symbol)+ check _ _ = error "can't check a function!"
+ src/Test/Target/Testable.hs view
@@ -0,0 +1,197 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DoAndIfThenElse #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverlappingInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ViewPatterns #-}+module Test.Target.Testable (test, Testable) where++import Control.Applicative+import Control.Exception (AsyncException, evaluate)+import Control.Monad+import Control.Monad.Catch+import Control.Monad.Reader+import Control.Monad.State+import qualified Data.HashMap.Strict as M+import qualified Data.HashSet as S+import Data.Proxy+import qualified Data.Text as T+import Data.Text.Format hiding (print)+import qualified Data.Text.Lazy as LT+import Text.Printf++import Language.Fixpoint.SmtLib2+import Language.Fixpoint.Types+import Language.Haskell.Liquid.RefType+import Language.Haskell.Liquid.Types hiding (Result (..), env, var)++import Test.Target.Targetable hiding (apply)+-- import Test.Target.Eval+import Test.Target.Expr+import Test.Target.Monad+import Test.Target.Types+import Test.Target.Util++-- import Debug.Trace++-- | Test that a function inhabits the given refinement type by enumerating+-- valid inputs and calling the function on the inputs.+test :: Testable f => f -> SpecType -> Target Result+test f t+ = do d <- asks depth+ vs <- queryArgs f d t+ setup+ let (xs, tis, to) = bkArrowDeep $ stripQuals t+ ctx <- gets smtContext+ try (process f ctx vs (zip xs tis) to) >>= \case+ Left (e :: TargetException) -> return $ Errored $ show e+ Right r -> return r++process :: Testable f+ => f -> Context -> [Symbol] -> [(Symbol,SpecType)] -> SpecType+ -> Target Result+process f ctx vs xts to = go 0 =<< io (command ctx CheckSat)+ where+ go !n Unsat = return $ Passed n+ go _ (Error e)= throwM $ SmtError $ T.unpack e+ go !n Sat = do+ when (n `mod` 100 == 0) $ whenVerbose $ io $ printf "Checked %d inputs\n" n+ let n' = n + 1+ xs <- decodeArgs f vs (map snd xts)+ whenVerbose $ io $ print xs+ er <- io $ try $ evaluate (apply f xs)+ -- whenVerbose $ io $ print er+ case er of+ Left (e :: SomeException)+ -- DON'T catch AsyncExceptions since they are used by @timeout@+ | Just (_ :: AsyncException) <- fromException e -> throwM e+ | Just (SmtError _) <- fromException e -> throwM e+ | Just (ExpectedValues _) <- fromException e -> throwM e+ | otherwise -> mbKeepGoing xs n+ Right r -> do+ real <- gets realized+ modify $ \s@(TargetState {..}) -> s { realized = [] }+ let su = mkSubst $ mkExprs f (map fst xts) xs+ (sat, _) <- check r (subst su to)++ -- refute model *after* checking output in case we have HOFs, which+ -- need to query the solver. if this is the last set of inputs, e.g.+ -- refuting the current model forces the solver to return unsat next+ -- time, the solver will return unsat when the HOF queries for an output,+ -- causing us to return a spurious error+ _ <- io $ command ctx $ Assert Nothing $ PNot $ pAnd+ [ ESym (SL $ symbolText x) `eq` ESym (SL v) | (x,v) <- real ]+ -- let env = map (second (`app` [])) cts ++ mkExprs f (map fst xts) xs+ -- sat <- evalType (M.fromList env) to (toExpr r)+ case sat of+ False -> mbKeepGoing xs n'+ True ->+ asks maxSuccess >>= \case+ Nothing -> go n' =<< io (command ctx CheckSat)+ Just m | m == n' -> return $ Passed m+ | otherwise -> go n' =<< io (command ctx CheckSat)+ go _ r = error $ "go _ " ++ show r+ mbKeepGoing xs n = do+ kg <- asks keepGoing+ if kg+ then go n =<< io (command ctx CheckSat)+ else return (Failed $ show xs)++-- | A class of functions that Target can test. A function is @Testable@ /iff/+-- all of its component types are 'Targetable' and all of its argument types are+-- 'Show'able.+--+-- You should __never__ have to define a new 'Testable' instance.+class (AllHave Targetable (Args f), Targetable (Res f)+ ,AllHave Show (Args f)) => Testable f where+ queryArgs :: f -> Int -> SpecType -> Target [Symbol]+ decodeArgs :: f -> [Symbol] -> [SpecType] -> Target (HList (Args f))+ apply :: f -> HList (Args f) -> Res f+ mkExprs :: f -> [Symbol] -> HList (Args f) -> [(Symbol,Expr)]++instance (Show a, Targetable a, Testable b) => Testable (a -> b) where+ queryArgs f d (stripQuals -> (RFun _ i o _))+ = liftM2 (:) (query (Proxy :: Proxy a) d i) (queryArgs (f undefined) d o)+ queryArgs _ _ t = error $ "queryArgs called with non-function type: " ++ show t+ decodeArgs f (v:vs) (t:ts)+ = liftM2 (:::) (decode v t) (decodeArgs (f undefined) vs ts)+ decodeArgs _ _ _ = error "decodeArgs called with empty list"+ apply f (x ::: xs)+ = apply (f x) xs+ apply _ _ = error "apply called with empty list"+ mkExprs f (v:vs) (x ::: xs)+ = (v, toExpr x) : mkExprs (f undefined) vs xs+ mkExprs _ _ _ = error "mkExprs called with empty list"++instance (Targetable a, Args a ~ '[], Res a ~ a) => Testable a where+ queryArgs _ _ _ = return []+ decodeArgs _ _ _ = return Nil+ apply f _ = f+ mkExprs _ _ _ = []+++makeDecl :: Symbol -> Sort -> Command+-- FIXME: hack..+makeDecl x _ | x `M.member` smt_set_funs = Assert Nothing PTrue+makeDecl x (FFunc _ ts) = Declare x (init ts) (last ts)+makeDecl x t = Declare x [] t++func :: Sort -> Bool+func (FFunc _ _) = True+func _ = False++setup :: Target ()+setup = {-# SCC "setup" #-} do+ ctx <- gets smtContext+ emb <- gets embEnv+ -- declare sorts+ ss <- S.toList <$> gets sorts+ let defSort b e = io $ smtWrite ctx (format "(define-sort {} () {})" (b,e))+ -- FIXME: combine this with the code in `fresh`+ forM_ ss $ \case+ FObj "Int" -> return ()+ FInt -> return ()+ FObj "GHC.Types.Bool" -> defSort ("GHC.Types.Bool" :: T.Text) ("Bool" :: T.Text)+ FObj "CHOICE" -> defSort ("CHOICE" :: T.Text) ("Bool" :: T.Text)+ s -> defSort (LT.toStrict $ smt2 s) ("Int" :: T.Text)+ -- declare constructors+ cts <- gets constructors+ mapM_ (\ (c,t) -> io . command ctx $ makeDecl (symbol c) t) cts+ let nullary = [var c | (c,t) <- cts, not (func t)]+ unless (null nullary) $+ void $ io $ command ctx $ Distinct nullary+ -- declare variables+ vs <- gets variables+ mapM_ (\ x -> io . command ctx $ Declare (symbol x) [] (arrowize $ snd x)) vs+ -- declare measures+ ms <- gets measEnv+ mapM_ (\m -> io . command ctx $ makeDecl (val $ name m) (rTypeSort emb $ sort m)) ms+ -- assert constraints+ cs <- gets constraints+ --mapM_ (\c -> do {i <- gets seed; modify $ \s@(GS {..}) -> s { seed = seed + 1 };+ -- io . command ctx $ Assert (Just i) c})+ -- cs+ mapM_ (\c -> io . command ctx $ Assert Nothing c) cs+ -- deps <- V.fromList . map (symbol *** symbol) <$> gets deps+ -- io $ generateDepGraph "deps" deps cs+ -- return (ctx,vs,deps)++sortTys :: Sort -> [Sort]+sortTys (FFunc _ ts) = concatMap sortTys ts+sortTys t = [t]++arrowize :: Sort -> Sort+arrowize = FObj . symbol . LT.intercalate "->" . map (LT.fromStrict . symbolText . unObj) . sortTys++unObj :: Sort -> Symbol+unObj FInt = "Int"+unObj (FObj s) = s+unObj s = error $ "unObj: " ++ show s
+ src/Test/Target/Types.hs view
@@ -0,0 +1,71 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeSynonymInstances #-}+module Test.Target.Types where++import qualified Control.Monad.Catch as Ex+import qualified Data.Text as T+import Data.Typeable++import Language.Fixpoint.SmtLib2+import Language.Fixpoint.Types+import Language.Haskell.Liquid.Types++import GHC+++data TargetException+ = SmtFailedToProduceOutput+ | SmtError String+ | ExpectedValues Response+ | PreconditionCheckFailed String+ | EvalError String+ deriving Typeable++instance Show TargetException where+ show SmtFailedToProduceOutput+ = "The SMT solver was unable to produce an output value."+ show (SmtError s)+ = "Unexpected error from the solver: " ++ s+ show (ExpectedValues r)+ = "Expected a Values response from the solver, got: " ++ show r+ show (PreconditionCheckFailed e)+ = "The pre-condition check for a generated function failed: " ++ e+ show (EvalError s)+ = "Couldn't evaluate a concrete refinement: " ++ s++instance Ex.Exception TargetException++ensureValues :: Ex.MonadThrow m => m Response -> m Response+ensureValues x = do+ a <- x+ case a of+ Values _ -> return a+ r -> Ex.throwM $ ExpectedValues r++type Constraint = [Pred]+type Variable = ( Symbol -- the name+ , Sort -- the `Sort'+ )+type Value = T.Text++instance Symbolic Variable where+ symbol (x, _) = symbol x++instance SMTLIB2 Constraint where+ smt2 = smt2 . PAnd++type DataConEnv = [(Symbol, SpecType)]+type MeasureEnv = [Measure SpecType DataCon]++boolsort, choicesort :: Sort+boolsort = FObj "Bool"+choicesort = FObj "CHOICE"++data Result = Passed !Int+ | Failed !String+ | Errored !String+ deriving (Show)++-- resultPassed (Passed i) = i
+ src/Test/Target/Util.hs view
@@ -0,0 +1,140 @@+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ParallelListComp #-}+module Test.Target.Util where++import Control.Applicative+import Control.Monad.IO.Class+import Data.List+import Data.Maybe+import Data.Monoid+import Data.Generics (everywhere, mkT)+import Debug.Trace++import qualified DynFlags as GHC+import qualified GhcMonad as GHC+import qualified GHC+import qualified GHC.Exts as GHC+import qualified GHC.Paths+import qualified HscTypes as GHC++import Language.Fixpoint.Types hiding (prop)+import Language.Haskell.Liquid.CmdLine+import Language.Haskell.Liquid.GhcInterface+import Language.Haskell.Liquid.PredType+import Language.Haskell.Liquid.RefType+import Language.Haskell.Liquid.Types hiding (var)++type Depth = Int++io :: MonadIO m => IO a -> m a+io = liftIO++myTrace :: Show a => String -> a -> a+myTrace s x = trace (s ++ ": " ++ show x) x++reft :: SpecType -> Reft+reft = toReft . rt_reft++data HList (a :: [*]) where+ Nil :: HList '[]+ (:::) :: a -> HList bs -> HList (a ': bs)++instance AllHave Show as => Show (HList as) where+ show Nil = "()"+ show (x ::: Nil) = show x+ show (x ::: xs) = show x ++ ", " ++ show xs++type family Map (f :: a -> b) (xs :: [a]) :: [b] where+ Map f '[] = '[]+ Map f (x ': xs) = f x ': Map f xs++type family Constraints (cs :: [GHC.Constraint]) :: GHC.Constraint+type instance Constraints '[] = ()+type instance Constraints (c ': cs) = (c, Constraints cs)++type AllHave (c :: k -> GHC.Constraint) (xs :: [k]) = Constraints (Map c xs)++type family Args a where+ Args (a -> b) = a ': Args b+ Args a = '[]++type family Res a where+ Res (a -> b) = Res b+ Res a = a++safeFromJust :: String -> Maybe a -> a+safeFromJust msg Nothing = error $ "safeFromJust: " ++ msg+safeFromJust _ (Just x) = x++applyPreds :: SpecType -> SpecType -> [(Symbol,SpecType)]+applyPreds sp' dc = zip xs (map tx ts)+ where+ sp = removePreds <$> sp'+ removePreds (U r _ _) = U r mempty mempty+ (as, ps, _, t) = bkUniv dc+ (xs, ts, _) = bkArrow . snd $ bkClass t+ -- args = reverse tyArgs+ su = [(tv, toRSort t, t) | tv <- as | t <- rt_args sp]+ sup = [(p, r) | p <- ps | r <- rt_pargs sp]+ tx = (\t -> replacePreds "applyPreds" t sup) . everywhere (mkT $ propPsToProp sup) . subsTyVars_meet su++propPsToProp+ :: [(PVar t3, Ref t (UReft t2) t1)]+ -> Ref t (UReft t2) t1 -> Ref t (UReft t2) t1+propPsToProp su r = foldr propPToProp r su++propPToProp+ :: (PVar t3, Ref t (UReft t2) t1)+ -> Ref t (UReft t2) t1 -> Ref t (UReft t2) t1+propPToProp (p, r) (RPropP _ (U _ (Pr [up]) _))+ | pname p == pname up+ = r+propPToProp _ m = m+++stripQuals :: SpecType -> SpecType+stripQuals = snd . bkClass . fourth4 . bkUniv++fourth4 :: (t, t1, t2, t3) -> t3+fourth4 (_,_,_,d) = d++getSpec :: FilePath -> IO GhcSpec+getSpec target+ = do cfg <- mkOpts mempty+ info <- getGhcInfo cfg target+ case info of+ Left err -> error $ show err+ Right i -> return $ spec i++runGhc :: GHC.Ghc a -> IO a+runGhc x = GHC.runGhc (Just GHC.Paths.libdir) $ do+ df <- GHC.getSessionDynFlags+ let df' = df { GHC.ghcMode = GHC.CompManager+ , GHC.ghcLink = GHC.NoLink --GHC.LinkInMemory+ , GHC.hscTarget = GHC.HscNothing --GHC.HscInterpreted+ -- , GHC.optLevel = 0 --2+ , GHC.log_action = \_ _ _ _ _ -> return ()+ , GHC.importPaths = GHC.importPaths df+ } `GHC.gopt_set` GHC.Opt_ImplicitImportQualified+ `GHC.xopt_set` GHC.Opt_MagicHash+ _ <- GHC.setSessionDynFlags df'+ x++loadModule :: FilePath -> GHC.Ghc GHC.ModSummary+loadModule f = do target <- GHC.guessTarget f Nothing+ --lcheck <- GHC.guessTarget "src/Test/Target.hs" Nothing+ GHC.setTargets [target] -- [target,lcheck]+ _ <- GHC.load GHC.LoadAllTargets+ modGraph <- GHC.getModuleGraph+ let m = fromJust $ find ((==f) . GHC.msHsFilePath) modGraph+ GHC.setContext [ GHC.IIModule (GHC.ms_mod_name m)+ --, GHC.IIDecl $ GHC.simpleImportDecl+ -- $ GHC.mkModuleName "Test.Target"+ ]+ return m
+ target.cabal view
@@ -0,0 +1,161 @@+name: target+version: 0.1.0.0+synopsis: Generate test-suites from refinement types.++description: Target is a library for testing Haskell functions based on+ properties encoded as refinement types.+ .+ The programmer specifies the expected behavior of a+ function with a refinement type, and Target then checks+ that the function satisfies the specification by+ enumerating valid inputs up to some size, calling the+ function, and validating the output. Target excels when the+ space of valid inputs is a sparse subset of all possible+ inputs, e.g. when dealing with dataypes with complex+ invariants like red-black trees.+ .+ "Test.Target" is the main entry point and should contain+ everything you need to use Target with types from the+ "Prelude". "Test.Target.Targetable" will also be useful if+ you want to test functions that use other types.+ .+ For information on how to /specify/ interesting properties+ with refinement types, we have a series of+ <http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/categories/basic/ blog posts>+ as well as an+ <http://github.com/ucsd-progsys/liquidhaskell/tree/master/docs/tutorial evolving tutorial>.+ Target uses the same specification language as LiquidHaskell,+ so the examples should carry over.+ .+ Finally, Target requires either <https://z3.codeplex.com/ Z3> + (@>=4.3@) or <http://cvc4.cs.nyu.edu/web/ CVC4> (@>=1.4@) to + be present in your @PATH@.++license: MIT+license-file: LICENSE+author: Eric Seidel+maintainer: eseidel@cs.ucsd.edu+category: Testing+build-type: Simple+cabal-version: >=1.10++source-repository head+ type: git+ location: git://github.com/gridaphobe/target.git++library+ default-language: Haskell2010+ hs-source-dirs: src+ ghc-options: -Wall -fno-warn-name-shadowing -fno-warn-orphans+ ghc-prof-options: -fprof-auto+ exposed-modules: Test.Target,+ Test.Target.Eval,+ Test.Target.Expr,+ Test.Target.Monad,+ Test.Target.Targetable,+ Test.Target.Targetable.Function,+ Test.Target.Testable,+ Test.Target.Types,+ Test.Target.Util++ build-depends: base >=4.6 && <5+ , containers >= 0.5.0.0+ , directory >= 1.2.0.1+ , exceptions >= 0.6+ , filepath >= 1.3.0.1+ , ghc >= 7.8.3+ , ghc-paths+ , liquid-fixpoint >= 0.2.1.1+ , liquidhaskell >= 0.2+ , mtl >= 2.1.2+ , pretty+ , process+ , syb >= 0.4.2+ , tagged >= 0.7+ , template-haskell+ , text >= 1.0+ , text-format+ , transformers >= 0.3+ , unordered-containers >= 0.2.3.0+ , vector++benchmark bench+ type: exitcode-stdio-1.0+ default-language: Haskell2010+ hs-source-dirs: bench+ ghc-options: -O2+ ghc-prof-options: -fprof-auto+ main-is: Main.hs+ build-depends: base,+ aeson,+ bytestring,+ cassava,+ SafeSemaphore,+ vector,+ xml-conduit,+ data-timeout >= 0.3,+ -- for XMonad+ -- X11,+ containers,+ random,+ tagged,+ ghc,+ unordered-containers,+ mtl,+ -- for Data.Map+ deepseq,+ --+ --criterion,+ --hastache,+ --statistics,+ time,+ target,+ template-haskell,+ liquidhaskell >= 0.2,+ liquid-fixpoint,+ QuickCheck >= 2.6,+ smallcheck >= 1.1++test-suite test+ type: exitcode-stdio-1.0+ default-language: Haskell2010+ hs-source-dirs: test+ ghc-options: -O2+ main-is: Main.hs+ c-sources: cbits/fpstring.c+ include-dirs: include+ includes: fpstring.h+ build-depends: base,+ target,+ ghc,+ tasty >= 0.8,+ tasty-hunit >= 0.8,+ -- for Data.Map+ containers,+ deepseq,+ -- for ByteString+ array,+ tagged,+ mtl,+ ghc-prim,+ liquid-fixpoint,+ liquidhaskell,+ template-haskell,+ unordered-containers++-- executable liquid-check+-- default-language: Haskell2010+-- hs-source-dirs: bin+-- main-is: Target.hs+-- build-depends: base,+-- Target,+-- liquid-fixpoint,+-- data-timeout >= 0.3,+-- ghc,+-- ghc-paths,+-- directory,+-- filepath,+-- process,+-- text,+-- time,+-- transformers
+ test/Main.hs view
@@ -0,0 +1,72 @@+{-# LANGUAGE TemplateHaskell #-}+module Main where++import Control.Exception+import GHC.IO.Handle+import qualified Language.Haskell.TH as TH+import System.IO+import Test.Tasty+import Test.Tasty.HUnit++import Test.Target++-- import qualified Data.ByteString.Internal as ByteString+import qualified HOFs+import List (List)+import qualified List+import qualified MapTest as Map+import qualified RBTree+import qualified RBTreeTest as RBTree+++main = defaultMain tests++tests, pos, neg :: TestTree++tests = testGroup "Tests" [pos, neg]++pos = testGroup "Pos" $+ [ mkSuccess (List.insert :: Int -> List Int -> List Int)+ 'List.insert "test/List.hs" 3+ -- FIXME: doesn't work with SMT-based checking of post-condition+ , mkSuccess List.mymap 'List.mymap "test/List.hs" 3+ ]+ ++ [ mkSuccess f name "test/HOFs.hs" 3 | (name, T f) <- hofsTests]+ ++ [ mkSuccess f name "test/RBTree.hs" 5 | (name, T f) <- RBTree.liquidTests]+ ++ [ mkSuccess f name "test/Map.hs" 4 | (name, T f) <- Map.liquidTests]+ --FIXME: need a better solution for checking equality that respects custom Eq instances+ -- ++ [ mkSuccess f ("Data.ByteString.Internal."++name) "test/Data/ByteString/Internal.hs" 4 | (name, T f) <- ByteString.liquidTests]++neg = testGroup "Neg" $+ [ mkFailure (List.insert_bad :: Int -> List Int -> List Int)+ 'List.insert "test/List.hs" 3+ ]+ ++ [ mkFailure f name "test/HOFs.hs" 3 | (name, T f) <- hofsTests_bad]+ ++ [ mkFailure f name "test/RBTree.hs" 5 | (name, T f) <- RBTree.liquidTests_bad]+ ++ [ mkFailure f name "test/Map.hs" 4 | (name, T f) <- Map.liquidTests_bad]++-- liquidTests, liquidTests_bad :: [(String,Test)]+hofsTests = [('HOFs.foo, T HOFs.foo), ('HOFs.list_foo, T HOFs.list_foo)]+hofsTests_bad = [('HOFs.foo, T HOFs.foo_bad), ('HOFs.list_foo, T HOFs.list_foo_bad)]++mkSuccess :: Testable f => f -> TH.Name -> String -> Int -> TestTree+mkSuccess f n fp d+ = testCase (show n ++ "/" ++ show d) $ shouldSucceed d f n fp++mkFailure :: Testable f => f -> TH.Name -> String -> Int -> TestTree+mkFailure f n fp d+ = testCase (show n ++ "/" ++ show d) $ shouldFail d f n fp++shouldSucceed d f name file+ = do r <- targetResultWith f name file (defaultOpts {depth = d})+ assertString $ case r of+ Passed _ -> ""+ Failed s -> "Unexpected counter-example: " ++ s+ Errored s -> "Unexpected error: " ++ s++shouldFail d f name file+ = do r <- targetResultWith f name file (defaultOpts {depth = d})+ assertBool "Expected counter-example" $ case r of+ Passed _ -> False+ _ -> True+