Lang.hs

{-# LANGUAGE ScopedTypeVariables #-}

module Main (main) where

import qualified Data.SBV           as S
import qualified Data.SBV.Dynamic   as S hiding (satWith)
import qualified Data.SBV.Internals as S

import Data.List  (sort, nub)
import Data.Maybe (fromMaybe)
import qualified Data.Map as M

import Control.Exception as C

-- Support <, >, ==
data CmpOp = Gt | Lt | Eq

-- Support +/*
data BOp = Plus | Times

-- Basic language; add constructs as necessary
data L = Leaf   S.SVal
       | LVar   String
       | LIf    L L L
       | LCmp   CmpOp L L
       | LArith BOp   L L

-- Kind of signed-32 bit values
i32 :: S.Kind
i32 = S.KBounded True 32

-- Sample program
--  if (x > 5) (if (x > 10) a b) ((if (x == 0) c d) * (if (y == 0) a b))
test :: L
test = ite (x `gt` five)
           (ite (x `gt` ten) a b)
           (ite (x `eq` zero) c d `times` ite (y `eq` zero) a b)
 where x     = LVar "x"
       y     = LVar "y"
       a     = LVar "a"
       b     = LVar "b"
       c     = LVar "c"
       d     = LVar "d"
       gt    = LCmp Gt
       eq    = LCmp Eq
       zero  = Leaf (S.svInteger i32 0)
       five  = Leaf (S.svInteger i32 5)
       ten   = Leaf (S.svInteger i32 10)
       ite   = LIf
       times = LArith Times

-- Interpreter environment
type Env  = M.Map String S.SVal

-- Collect the "decision" variables; i.e., those that are under some "If" test-statement
getVars :: L -> [String]
getVars = sort . nub . collect False []
  where collect True  sofar (LVar   s)     = s:sofar
        collect False sofar (LVar   _)     = sofar
        collect pick  sofar (LIf    i t e) = collect pick (collect pick (collect True sofar i) t) e
        collect pick  sofar (LCmp   _ a b) = collect pick (collect pick sofar a) b
        collect pick  sofar (LArith _ a b) = collect pick (collect pick sofar a) b
        collect _     sofar (Leaf _)       = sofar

-- Create a symbolic variable. We assume everything is Int32. If other types
-- are needed SVal can support them so long as you've enough info in your data-type around.
free32 :: String -> S.Symbolic S.SVal
free32 nm = S.svMkSymVar Nothing i32 (Just nm)

-- Cover points. This will keep track of the boolean condition as we descend down program.
-- We only need two cases here, since there's only one branching instruction in L. In general
-- you'll have a separate case for each decision point.
data Cov = CLeaf S.SVal
         | CMul [Cov]            -- multiple different ways of proceeding
         | CIf  S.SVal Cov Cov   -- Conditional proceeding
         deriving Show

-- An alternative interpreter, which creates coverage data from a program
coverPaths :: Env -> L -> S.Symbolic Cov
coverPaths varEnv pgm = do let (cov, _) = go (CLeaf S.svTrue) pgm
                           return cov
  where -- The leaf case is simple; we terminate here
        go path (Leaf v) = (path, v)

        -- Ditto for variable look-up
        go path (LVar s) = let v = fromMaybe (error $ "Impossible, unfound reference to: " ++ s) 
                                             (s `M.lookup` varEnv)
                           in (path, v)

        -- Ite is the interesting case; we simply create the corresponding paths
        -- down to the branches
        go path (LIf b t e)   = let -- First compute the ways we can compute b, t, and e
                                    (_ , bv) = go path b
                                    (tp, tv) = go path t
                                    (ep, ev) = go path e

                                    -- Now combine all the possibilities together
                                in (CIf bv tp ep, S.svIte bv tv ev)

        -- comparison, simply descend down
        go path (LCmp c a b)  = let (ap, x) = go path a
                                    (bp, y) = go path b
                                in case c of
                                     Gt -> (CMul [ap, bp], x `S.svGreaterThan` y)
                                     Lt -> (CMul [ap, bp], x `S.svLessThan`    y)
                                     Eq -> (CMul [ap, bp], x `S.svEqual`       y)

        -- same for arithmetic
        go path (LArith o a b) = let (ap, x) = go path a
                                     (bp, y) = go path b
                                 in case o of
                                      Plus  -> (CMul [ap, bp], x `S.svPlus`  y)
                                      Times -> (CMul [ap, bp], x `S.svTimes` y)

-- Given a Cov, serialize it to create a boolean for each path representing the reachability of that path
serialize :: Cov -> [S.SBool]
serialize = filter (not . S.isConcrete) . map S.SBV . go
  where go (CLeaf s)    = [s]
        go (CMul cs)    = concatMap go cs
        go (CIf bv t e) =    map (        bv `S.svAnd`) (go t)
                          ++ map (S.svNot bv `S.svAnd`) (go e)

-- Find the cover points for a program. This is a bit hackish since
-- we are forced to run the symbolic simulation repeatedly and quit
-- when we realize we covered all the paths. It can be done better
-- if we add a corresponding combinator to SBV itself; but it should
-- do for the time being. (Let me know if this becomes a problem.)
cover :: L -> IO [S.SatResult]
cover pgm = loop 0 []
  where vs = getVars pgm
        loop i sofar = do
                mbR <- (Just `fmap` S.sat (do ss <- mapM free32 vs
                                              c <- coverPaths (M.fromList (zip vs ss)) pgm
                                              case drop i (serialize c) of
                                                 []    -> error "exhausted"
                                                 (h:_) -> return h))
                      `C.catch` (\(_ :: C.SomeException) -> return Nothing)
                case mbR of
                  Nothing -> return sofar
                  Just r  -> loop (i+1) (r:sofar)

main :: IO ()
main = do ss <- cover test
          mapM_ print ss
          putStrLn $ "Total coverage points: " ++ show (length ss)

Output.txt

$ ghci Lang.hs
GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( Lang.hs, interpreted )
Ok, modules loaded: Main.
*Main> main
Satisfiable. Model:
  x =  5 :: Int32
  y = -1 :: Int32
Satisfiable. Model:
  x = 5 :: Int32
  y = 0 :: Int32
Satisfiable. Model:
  x = 2 :: Int32
  y = 0 :: Int32
Satisfiable. Model:
  x = 0 :: Int32
  y = 0 :: Int32
Satisfiable. Model:
  x = 8 :: Int32
  y = 0 :: Int32
Satisfiable. Model:
  x = 15 :: Int32
  y =  0 :: Int32
Total coverage points: 6