module Copilot.Tools.CBMC
( Params (..)
, defaultParams
, genCBMC
, atomPrefix
, sbvPrefix
, appendPrefix
) where
import Copilot.Core
import qualified Copilot.Compile.C99 as C99
import qualified Copilot.Compile.SBV as SBV
import qualified System.IO as I
import Text.PrettyPrint.HughesPJ
data Params = Params
{ numIterations :: Int }
defaultParams :: Params
defaultParams = Params
{ numIterations = 10 }
atomPrefix, sbvPrefix :: Maybe String
atomPrefix = Just "atm"
sbvPrefix = Just "sbv"
appendPrefix :: Maybe String -> String -> String
appendPrefix (Just pre) name = pre ++ "_" ++ name
appendPrefix Nothing name = name
genCBMC :: Params -> Spec -> IO ()
genCBMC params spec =
do
C99.compile (C99.defaultParams { C99.prefix = atomPrefix }) spec
SBV.compile (SBV.defaultParams { SBV.prefix = sbvPrefix }) spec
h <- I.openFile "cbmc_driver.c" I.WriteMode
I.hPutStrLn h (render (driver params spec))
driver :: Params -> Spec -> Doc
driver Params { numIterations = k } spec = vcat
[ text "#include <stdbool.h>"
, text "#include <stdint.h>"
, text "#include <assert.h>"
, include atomPrefix C99.c99DirName C99.c99FileRoot
, include sbvPrefix SBV.sbvDirName "copilot"
, text ""
, declNonDets spec
, text ""
, declExterns spec
, text ""
, sampleExterns spec
, text ""
, verifyObservers spec
, text ""
, text "int main (int argc, char const *argv[])"
, text "{"
, text " int i;"
, text ""
, text " for (i = 0; i < " <> int k <> text "; i++)"
, text " {"
, text " sampleExterns();"
, text $ " " ++ appendPrefix atomPrefix "step();"
, text $ " " ++ appendPrefix sbvPrefix "step();"
, text " verify_observers();"
, text " }"
, text ""
, text " return 0;"
, text "}"
]
where
include prefix dir header = text "#include" <+> doubleQuotes
( text (appendPrefix prefix dir) <> text"/"
<> text (appendPrefix prefix (header ++ ".h"))
)
declNonDets :: Spec -> Doc
declNonDets = vcat . map declNonDet . externVars
where
declNonDet :: ExtVar -> Doc
declNonDet ext@(ExtVar _ t) = typeSpec t <+> nonDetName ext
nonDetName :: ExtVar -> Doc
nonDetName (ExtVar name t) =
text ("nondet_" ++ name ++ "_") <> (typeSpec t) <> text "();"
declExterns :: Spec -> Doc
declExterns = vcat . map declExtern . externVars
where
declExtern :: ExtVar -> Doc
declExtern (ExtVar name t) = typeSpec t <+> text name <> semi
sampleExterns :: Spec -> Doc
sampleExterns spec = vcat
[ text "void sampleExterns()"
, text "{"
, text ""
, nest 2 (vcat $ map sampleExtern (externVars spec))
, text "}"
]
where
sampleExtern :: ExtVar -> Doc
sampleExtern ext@(ExtVar name _) =
text name <+> text "=" <+> nonDetName ext
verifyObservers :: Spec -> Doc
verifyObservers spec = vcat
[ text "void verify_observers()"
, text "{"
, text ""
, nest 2 (vcat $ map verifyObserver (specObservers spec))
, text "}"
]
where
verifyObserver :: Observer -> Doc
verifyObserver (Observer name _ _) =
text "assert(" <> text (appendPrefix atomPrefix name) <+> text "=="
<+> text (appendPrefix sbvPrefix name) <> text ");"
typeSpec :: UType -> Doc
typeSpec UType { uTypeType = t } = text (typeSpec' t)
where
typeSpec' Bool = "bool"
typeSpec' Int8 = "int8_t"
typeSpec' Int16 = "int16_t"
typeSpec' Int32 = "int32_t"
typeSpec' Int64 = "int64_t"
typeSpec' Word8 = "uint8_t"
typeSpec' Word16 = "uint16_t"
typeSpec' Word32 = "uint32_t"
typeSpec' Word64 = "uint64_t"
typeSpec' Float = "float"
typeSpec' Double = "double"