module Lava.Smv
  ( smv
  )
 where

import Lava.Signal
import Lava.Netlist
import Lava.Generic
import Lava.Sequent
import Lava.Property
import Lava.Error
import Lava.LavaDir
import Lava.Verification

import Data.List
  ( intersperse
  , nub
  )

import System.IO
  ( openFile
  , IOMode(..)
  , hPutStr
  , hClose
  )

import Lava.IOBuffering
  ( noBuffering
  )

import Data.IORef

import System.Process (system)
import System.Exit (ExitCode(..))

----------------------------------------------------------------
-- smv

smv :: Checkable a => a -> IO ProofResult
smv :: a -> IO ProofResult
smv a :: a
a =
  do IO ()
checkVerifyDir
     IO ()
noBuffering
     (props :: [Signal Bool]
props,_) <- a -> IO ([Signal Bool], Model -> [[String]])
forall a.
Checkable a =>
a -> IO ([Signal Bool], Model -> [[String]])
properties a
a
     String -> IO () -> IO ProofResult
proveFile String
defsFile (String -> [Signal Bool] -> IO ()
writeDefinitions String
defsFile [Signal Bool]
props)
 where
  defsFile :: String
defsFile = String
verifyDir String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/circuit.smv"

----------------------------------------------------------------
-- definitions

writeDefinitions :: FilePath -> [Signal Bool] -> IO ()
writeDefinitions :: String -> [Signal Bool] -> IO ()
writeDefinitions file :: String
file props :: [Signal Bool]
props =
  do Handle
firstHandle  <- String -> IOMode -> IO Handle
openFile String
firstFile IOMode
WriteMode
     Handle
secondHandle <- String -> IOMode -> IO Handle
openFile String
secondFile IOMode
WriteMode
     IORef Integer
var <- Integer -> IO (IORef Integer)
forall a. a -> IO (IORef a)
newIORef 0

     Handle -> String -> IO ()
hPutStr Handle
firstHandle (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
       [ "-- Generated by Lava"
       , ""
       , "MODULE main"
       ]

     let new :: IO String
new =
           do Integer
n <- IORef Integer -> IO Integer
forall a. IORef a -> IO a
readIORef IORef Integer
var
              let n' :: Integer
n' = Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+1; v :: String
v = "w" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n'
              Integer
n' Integer -> IO () -> IO ()
forall a b. a -> b -> b
`seq` IORef Integer -> Integer -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Integer
var Integer
n'
              String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
v

         define :: String -> S String -> IO ()
define v :: String
v s :: S String
s =
           case S String
s of
             Bool True     -> String -> IO ()
op0 "1"
             Bool False    -> String -> IO ()
op0 "0"
             Inv x :: String
x         -> String -> String -> IO ()
op1 "!" String
x

             And []        -> String -> S String -> IO ()
define String
v (Bool -> S String
forall s. Bool -> S s
Bool Bool
True)
             And [x :: String
x]       -> String -> IO ()
op0 String
x
             And xs :: [String]
xs        -> String -> [String] -> IO ()
opl "&" [String]
xs

             Or  []        -> String -> S String -> IO ()
define String
v (Bool -> S String
forall s. Bool -> S s
Bool Bool
False)
             Or  [x :: String
x]       -> String -> IO ()
op0 String
x
             Or  xs :: [String]
xs        -> String -> [String] -> IO ()
opl "|" [String]
xs

             Xor  []       -> String -> S String -> IO ()
define String
v (Bool -> S String
forall s. Bool -> S s
Bool Bool
False)
             Xor  xs :: [String]
xs       -> String -> IO ()
op0 ([String] -> String
xor [String]
xs)

             VarBool s :: String
s     -> do String -> IO ()
op0 String
s
                                 Handle -> String -> IO ()
hPutStr Handle
firstHandle ("VAR " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " : boolean;\n")
             DelayBool x :: String
x y :: String
y -> String -> String -> IO ()
delay String
x String
y

             _             -> Error -> IO ()
forall a. Error -> a
wrong Error
Lava.Error.NoArithmetic
           where
            w :: a -> String
w i :: a
i = String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i

            op0 :: String -> IO ()
op0 s :: String
s =
              Handle -> String -> IO ()
hPutStr Handle
secondHandle (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
                "DEFINE " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ " := " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ";\n"

            op1 :: String -> String -> IO ()
op1 op :: String
op s :: String
s =
              String -> IO ()
op0 (String
op String -> String -> String
forall a. [a] -> [a] -> [a]
++ "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")")

            opl :: String -> [String] -> IO ()
opl op :: String
op xs :: [String]
xs =
              String -> IO ()
op0 ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse (" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
op String -> String -> String
forall a. [a] -> [a] -> [a]
++ " ") [String]
xs))

            xor :: [String] -> String
xor [x :: String
x]    = String
x
            xor [x :: String
x,y :: String
y]  = "!(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ " <-> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
            xor (x :: String
x:xs :: [String]
xs) = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ " & !("
                      String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse " | " [String]
xs)
                      String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") | (!" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ " & (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
xor [String]
xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")))"

            delay :: String -> String -> IO ()
delay x :: String
x y :: String
y =
              do Handle -> String -> IO ()
hPutStr Handle
firstHandle ("VAR " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ " : boolean;\n")
                 Handle -> String -> IO ()
hPutStr Handle
secondHandle (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
                      "ASSIGN init(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") := " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ ";\n"
                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ "ASSIGN next(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") := " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ ";\n"

     Struct String
outvs <- IO String
-> (String -> S String -> IO ())
-> Struct Symbol
-> IO (Struct String)
forall (f :: * -> *) v.
Sequent f =>
IO v -> (v -> S v -> IO ()) -> f Symbol -> IO (f v)
netlistIO IO String
new String -> S String -> IO ()
define ([Signal Bool] -> Struct Symbol
forall a. Generic a => a -> Struct Symbol
struct [Signal Bool]
props)
     Handle -> String -> IO ()
hPutStr Handle
secondHandle (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
       [ "SPEC AG " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
outv
       | String
outv <- Struct String -> [String]
forall a. Struct a -> [a]
flatten Struct String
outvs
       ]

     Handle -> IO ()
hClose Handle
firstHandle
     Handle -> IO ()
hClose Handle
secondHandle

     String -> IO ExitCode
system ("cat " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
firstFile String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
secondFile String -> String -> String
forall a. [a] -> [a] -> [a]
++ " > " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file)
     String -> IO ExitCode
system ("rm " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
firstFile String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
secondFile)
     () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
 where
  firstFile :: String
firstFile  = String
file String -> String -> String
forall a. [a] -> [a] -> [a]
++ "-1"
  secondFile :: String
secondFile = String
file String -> String -> String
forall a. [a] -> [a] -> [a]
++ "-2"

----------------------------------------------------------------
-- primitive proving

proveFile :: FilePath -> IO () -> IO ProofResult
proveFile :: String -> IO () -> IO ProofResult
proveFile file :: String
file before :: IO ()
before =
  do String -> IO ()
putStr "Smv: "
     IO ()
before
     String -> IO ()
putStr "... "
     String
lavadir <- IO String
getLavaDir
     ExitCode
x <- String -> IO ExitCode
system ( String
lavadir
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/Scripts/smv.wrapper "
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -showTime"
                 )
     let res :: ProofResult
res = case ExitCode
x of
                 ExitSuccess   -> ProofResult
Valid
                 ExitFailure 1 -> ProofResult
Indeterminate
                 ExitFailure _ -> ProofResult
Falsifiable
     String -> IO ()
putStrLn (ProofResult -> String
forall a. Show a => a -> String
show ProofResult
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".")
     ProofResult -> IO ProofResult
forall (m :: * -> *) a. Monad m => a -> m a
return ProofResult
res

----------------------------------------------------------------
-- the end.