-
Notifications
You must be signed in to change notification settings - Fork 0
/
Klee.hs
148 lines (133 loc) · 5.71 KB
/
Klee.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
{-# LANGUAGE NamedFieldPuns #-}
module Klee where
import System.Exit
import System.Process
import System.Directory
import System.FilePath
import Text.Printf
import Control.Monad.Writer
import Control.Applicative
import Data.Maybe
import Data.List
import Data.List.Split
data KleeFlags = KleeFlags
{ libc :: Maybe String
, emitAllErrors :: Bool
, posixRuntime :: Bool
, outputDirectory :: Maybe FilePath
, maxTime :: Maybe Int
, optimize :: Bool
}
data KleeReport = KleeReport
{ completedPaths :: Integer
, exploredPaths :: Integer
, generatedTests :: Integer
, testCases :: [ FilePath ]
, errors :: [ FilePath ]
, statistics :: Maybe KleeStats
}
exhaustive :: KleeReport -> Bool
exhaustive = (==) <$> completedPaths <*> exploredPaths
instance Show KleeReport where
show r = snd $ runWriter $ do
tell $ printf "Number of completed paths: \t%d\n" (completedPaths r)
tell $ printf "Number of explored paths: \t%d\n" (exploredPaths r)
tell $ printf "Number of generated tests: \t%d\n" (generatedTests r)
--tell $ printf "The test is \t%s\n" $ if exhaustive r then "EXHAUSTIVE" else "NONEXHAUSTIVE"
tell $ printf "\n"
tell $ printf "Test cases: \t%s\n" (intercalate ", " $ testCases r)
tell $ printf "Errors: \t%s\n" (intercalate ", " $ errors r)
tell $ printf "Support for performance statistics not yet available\n"
return ()
data KleeStats = KleeStats
{ instructions :: Integer
, fullBranches :: Integer
, partialBranches :: Integer
, numBranches :: Integer
, userTime :: Double
, numStates :: Integer
, mallocUsage :: Integer
, numQueries :: Integer
, numQueryConstructs :: Integer
, numObjects :: Integer
, wallTime :: Double
, coveredInstructions :: Integer
, uncoveredInstructions :: Integer
, queryTime :: Double
, solverTime :: Double
, cexCacheTime :: Double
, forkTime :: Double
, resolveTime :: Double
}
whenJust :: (Monad m) => Maybe a -> (a -> m ()) -> m ()
whenJust Nothing _ = return ()
whenJust (Just a) f = f a
toFlags :: FilePath -> KleeFlags -> [String]
toFlags input flags = snd $ runWriter $ do
whenJust (libc flags) $ \c -> tell ["-libc=" ++ c]
whenJust (outputDirectory flags) $ \d -> tell ["-output-dir=" ++ d]
when (posixRuntime flags) $ tell ["--posix-runtime"]
when (emitAllErrors flags) $ tell ["-emit-all-errors"]
whenJust (maxTime flags) $ \i -> tell ["-max-time=" ++ show i]
when (optimize flags) $ tell ["--optimize"]
tell [input]
reportKleeFailure :: Int -> String -> String -> String -> IO ()
reportKleeFailure errno input out err = do
printf "Error verifying file %s\n" input
printf "Error code %d\n" errno
printf "STDOUT:\n%s\n" out
printf "STDERR:\n%s\n" err
reportKTestToolFailure :: Int -> String -> String -> String -> IO ()
reportKTestToolFailure errno input out err = do
printf "Error reading report %s\n" input
printf "Error code %d\n" errno
printf "STDOUT:\n%s\n" out
printf "STDERR:\n%s\n" err
readKleeInfoFile :: FilePath -> IO (Integer, Integer, Integer)
readKleeInfoFile path = do
attributes <- map (\ [a, b] -> (a, b))
<$> map (splitOn " = ")
<$> map (drop (length prefix))
<$> filter ((== prefix) . take (length prefix))
<$> lines
<$> readFile (path </> "info")
return ( read $ fromJust $ lookup "explored paths" attributes
, read $ fromJust $ lookup "completed paths" attributes
, read $ fromJust $ lookup "generated tests" attributes
)
where prefix = "KLEE: done: "
readKleeResults :: FilePath -> IO KleeReport
readKleeResults path = do
kleeResults <- getDirectoryContents path
let testCases = sort $ (path </>) <$> filter ((== ".ktest") . snd . splitExtension) kleeResults
let errors = sort $ (path </>) <$> filter ((== ".err") . snd . splitExtension) kleeResults
let statistics = Nothing
(exploredPaths, completedPaths, generatedTests) <- readKleeInfoFile path
return KleeReport { testCases
, errors
, generatedTests
, completedPaths
, exploredPaths
, statistics }
runKlee :: KleeFlags -> FilePath -> IO (Maybe KleeReport)
runKlee flags filename = do
whenJust (outputDirectory flags) $ \dir -> do
exists <- doesDirectoryExist dir
when exists $ removeDirectoryRecursive dir
printf "Command: %s %s\n" "klee" (unwords kleeFlags)
(exitCode, out, err) <- readProcessWithExitCode "klee" kleeFlags ""
case exitCode of
ExitFailure errno -> do
reportKleeFailure errno filename out err
return Nothing
ExitSuccess -> Just <$> readKleeResults ("klee-last" `fromMaybe` outputDirectory flags)
where kleeFlags = toFlags filename flags
runKTestTool :: FilePath -> IO (Maybe [String])
runKTestTool filename = do
(exitCode, out, err) <- readProcessWithExitCode "ktest-tool" [filename, "--write-ints"] ""
case exitCode of
ExitFailure errno -> do
reportKTestToolFailure errno filename out err
return Nothing
ExitSuccess ->
return $ Just (lines out)