module Lava.Fixit
( fixit
)
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(..))
fixit :: Checkable a => a -> IO ProofResult
fixit :: a -> IO ProofResult
fixit 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.circ"
writeDefinitions :: FilePath -> [Signal Bool] -> IO ()
writeDefinitions :: String -> [Signal Bool] -> IO ()
writeDefinitions file :: String
file props :: [Signal Bool]
props =
do Handle
han <- String -> IOMode -> IO Handle
openFile String
file IOMode
WriteMode
IORef Integer
var <- Integer -> IO (IORef Integer)
forall a. a -> IO (IORef a)
newIORef 0
Handle -> String -> IO ()
hPutStr Handle
han "INTERNALS{low := FALSE;}\n"
Handle -> String -> IO ()
hPutStr Handle
han "INTERNALS{high := TRUE;}\n"
Handle -> String -> IO ()
hPutStr Handle
han "LATCHES{initt := low (high);}\n"
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
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 ("w" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n')
define :: String -> S String -> IO ()
define v :: String
v s :: S String
s =
do Handle -> String -> IO ()
hPutStr Handle
han (String
def String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n")
where
def :: String
def =
case S String
s of
Bool True -> String -> String
prop (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "TRUE"
Bool False -> String -> String
prop (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "FALSE"
Inv x -> String -> String
prop (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "~" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x
And xs -> String -> String
prop (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String -> String
ops "&" [String]
xs "TRUE"
Or xs -> String -> String
prop (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String -> String
ops "#" [String]
xs "FALSE"
Xor xs -> String -> String
prop (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
xorlist [String]
xs
VarBool s -> String -> String
var String
s
DelayBool x y -> String -> String -> String
latch String
x String
y
_ -> Error -> String
forall a. Error -> a
wrong Error
Lava.Error.NoArithmetic
prop :: String -> String
prop form :: String
form =
"INTERNALS{" 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
form String -> String -> String
forall a. [a] -> [a] -> [a]
++ ";}"
var :: String -> String
var s :: String
s =
String -> String
prop String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " PSEUDOS{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ";}"
latch :: String -> String -> String
latch x :: String
x y :: String
y =
"LATCHES{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_x := " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ " (low);}\n"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ "INTERNALS{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ " := (initt & " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x
String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") # (~initt & " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_x);}"
ops :: String -> [String] -> String -> String
ops op :: String
op [] nul :: String
nul = String
nul
ops op :: String
op [x :: String
x] nul :: String
nul = String
x
ops op :: String
op xs :: [String]
xs nul :: String
nul =
"(" 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 -> String -> String
forall a. [a] -> [a] -> [a]
++ String
op String -> String -> String
forall a. [a] -> [a] -> [a]
++ " ") [String]
xs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
xorlist :: [String] -> String
xorlist [] = "FALSE"
xorlist [x :: String
x] = String
x
xorlist [x :: String
x,y :: String
y] = String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ " #! " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y
xorlist (x :: String
x:xs :: [String]
xs) = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x_not_xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") # (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
not_x_xor_xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
where
x_not_xs :: String
x_not_xs = String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> String) -> [String] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (" & ~" String -> String -> String
forall a. [a] -> [a] -> [a]
++) [String]
xs
not_x_xor_xs :: String
not_x_xor_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
xorlist [String]
xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
~(Compound vs :: [Struct String]
vs) <- 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)
String -> S String -> IO ()
define "bad" ([String] -> S String
forall s. [s] -> S s
And [ "~" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v | Object v :: String
v <- [Struct String]
vs ])
Handle -> IO ()
hClose Handle
han
proveFile :: FilePath -> IO () -> IO ProofResult
proveFile :: String -> IO () -> IO ProofResult
proveFile file :: String
file before :: IO ()
before =
do String -> IO ()
putStr "Fixit: "
IO ()
before
String -> IO ()
putStr "... "
String -> IO ExitCode
system ("rm -f " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
verifyDir String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/fixit.lock")
String
lavadir <- IO String
getLavaDir
ExitCode
x <- String -> IO ExitCode
system ( String
lavadir
String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/Scripts/fixit.wrapper "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file
String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -showTime -dir=forward -sat=prove"
)
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