copilot-cbmc 0.2 → 0.11

raw patch · 2 files changed

+31/−71 lines, 2 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• copilot-cbmc.cabal +1/−1
• src/Copilot/Tools/CBMC.hs +30/−70

@@ -1,6 +1,6 @@ cabal-version             : >= 1.10 name                      : copilot-cbmc-version                   : 0.2+version                   : 0.11 synopsis                  : Copilot interface to a C model-checker. description               : Depends on CBMC <http://www.cprover.org/cbmc/>.  Generates a driver to prove the Atom and SBV backends generate equivalent code. license                   : BSD3

@@ -4,14 +4,7 @@  {-# LANGUAGE GADTs #-} -module Copilot.Tools.CBMC -  ( Params (..)-  , defaultParams-  , genCBMC-  , atomPrefix-  , sbvPrefix-  , appendPrefix-  ) where+module Copilot.Tools.CBMC (Params (..), defaultParams, genCBMC) where  import Copilot.Core import qualified Copilot.Compile.C99 as C99@@ -19,48 +12,39 @@ 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+    C99.compile (C99.defaultParams { C99.prefix = Just "atm" }) spec+    SBV.compile (SBV.defaultParams { SBV.prefix = Just "sbv" }) 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 "#include \"atm_copilot.h\""+  , text "#include \"sbv_copilot/sbv_copilot.h\""   , text ""-  , declNonDets spec+  , text "int32_t nondet_bool();"+  , text "int32_t nondet_uint8_t();"+  , text "int32_t nondet_uint16_t();"+  , text "int32_t nondet_uint32_t();"+  , text "int32_t nondet_uint64_t();"+  , text "int32_t nondet_int8_t();"+  , text "int32_t nondet_int16_t();"+  , text "int32_t nondet_int32_t();"+  , text "int32_t nondet_int64_t();"+  , text "int32_t nondet_float();"+  , text "int32_t nondet_double();"   , text ""   , declExterns spec   , text ""@@ -75,8 +59,8 @@   , text "  for (i = 0; i < " <> int k <> text "; i++)"   , text "  {"   , text "    sampleExterns();"-  , text $ "    " ++ appendPrefix atomPrefix "step();"-  , text $ "    " ++ appendPrefix sbvPrefix "step();"+  , text "    atm_step();"+  , text "    sbv_step();"   , text "    verify_observers();"   , text "  }"   , text ""@@ -84,35 +68,13 @@   , 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 ---------------------------------------------------------------------------------+    declExtern :: ExtVar -> Doc+    declExtern (ExtVar name t) = typeSpec t <+> text name <> semi  sampleExterns :: Spec -> Doc sampleExterns spec = vcat@@ -124,11 +86,10 @@   ]    where-  sampleExtern :: ExtVar -> Doc-  sampleExtern ext@(ExtVar name _) =-    text name <+> text "=" <+> nonDetName ext ---------------------------------------------------------------------------------+    sampleExtern :: ExtVar -> Doc+    sampleExtern (ExtVar name t) =+      text name <+> text "=" <+> text "nondet_" <> typeSpec t <> text "();"  verifyObservers :: Spec -> Doc verifyObservers spec = vcat@@ -140,16 +101,17 @@   ]    where-  verifyObserver :: Observer -> Doc-  verifyObserver (Observer name _ _) =-    text "assert(" <> text (appendPrefix atomPrefix name) <+> text "==" -      <+> text (appendPrefix sbvPrefix name) <> text ");" ---------------------------------------------------------------------------------+    verifyObserver :: Observer -> Doc+    verifyObserver (Observer name _ _) =+      text "assert(" <> text "atm_" <> text name <+> text "==" <+> text "sbv_" <>+      text name <> text ");"  typeSpec :: UType -> Doc typeSpec UType { uTypeType = t } = text (typeSpec' t)+   where+   typeSpec' Bool   = "bool"   typeSpec' Int8   = "int8_t"   typeSpec' Int16  = "int16_t"@@ -161,5 +123,3 @@   typeSpec' Word64 = "uint64_t"   typeSpec' Float  = "float"   typeSpec' Double = "double"----------------------------------------------------------------------------------