copilot-cbmc (empty) → 0.1
raw patch · 5 files changed
+271/−0 lines, 5 filesdep +basedep +bytestringdep +copilot-c99build-type:Customsetup-changed
Dependencies added: base, bytestring, copilot-c99, copilot-core, copilot-sbv, directory, pretty, process
Files
- LICENSE +29/−0
- README.md +57/−0
- Setup.hs +21/−0
- copilot-cbmc.cabal +39/−0
- src/Copilot/Tools/CBMC.hs +125/−0
+ LICENSE view
@@ -0,0 +1,29 @@+2009+BSD3 License terms++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++Redistributions of source code must retain the above copyright+notice, this list of conditions and the following disclaimer.++Redistributions in binary form must reproduce the above copyright+notice, this list of conditions and the following disclaimer in the+documentation and/or other materials provided with the distribution.++Neither the name of the developers nor the names of its contributors+may be used to endorse or promote products derived from this software+without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,57 @@+Overview+========+[copilot-cbmc](http://hackage.haskell.org/package/copilot-cbmc) A tool to+generate a driver using CBMC, a third-party tool (see Dependencies below) that+proves that the code generated by different C back-ends is equivalent.+Currently, this includes the C99 back-end and the SBV back-end.++Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in+Haskell that compiles into embedded C. Copilot is similar in spirit to+languages like Lustre. Copilot contains an interpreter, multiple back-end+compilers, and other verification tools.++Examples+=========+Please see the files under the Examples directory in the+[Copilot](http://hackage.haskell.org/package/copilot) for a number of examples+showing the syntax, use of libraries, and use of the interpreter and back-ends.+The examples is the best way to start.++Installation+============+The Copilot library is cabalized. Assuming you have cabal and the GHC compiler+installed (the [Haskell Platform](http://hackage.haskell.org/platform/) is the+easiest way to obtain these), it should merely be a matter of running + + cabal install copilot-cbmc++However, we strongly recommend you install Copilot, which installs copilot-c99+and other packages automatically. Execute++ cabal install copilot++Dependencies+=============+copilot-cbmc depends on the C model-checker, CBMC.+[CBMC](http://www.cprover.org/cbmc/) is a bounded model-checker for C code. We+use CBMC to prove that two back-ends generating C generate semantically+equivalent C, to help detect bugs in C back-ends.++Resources+=========+[copilot-cbmc](http://hackage.haskell.org/package/copilot-cbmc) is available on+Hackage.++**Sources** for each package are available on Github as well. Just go to+[Github](github.com) and search for the package of interest. Feel free to fork!++Copyright, License+==================+Copilot is distributed with the BSD3 license. The license file contains the+[BSD3](http://en.wikipedia.org/wiki/BSD_licenses) verbiage.++Thanks+======+We are grateful for NASA Contract NNL08AD13T to [Galois,+Inc](http://corp.galois.com/) and the [National Institute of+Aerospace](http://www.nianet.org/), which partially supported this work.
+ Setup.hs view
@@ -0,0 +1,21 @@+module Main ( main ) where++import System.Directory (findExecutable)+import Distribution.Simple (defaultMainWithHooks, simpleUserHooks, postInst)+import System.Directory (findExecutable)+import System.Exit (exitWith, ExitCode(..))++main :: IO ()+main = defaultMainWithHooks simpleUserHooks{ postInst = checkDefSolver }+ where checkDefSolver _ _ _ _ = do+ mbP <- findExecutable "cbmc"+ case mbP of+ Nothing -> do putStrLn "***"+ putStrLn "*** The copilot-cbmc library requires the solver cbcm to be installed."+ putStrLn "*** The executable CBMC must be in your path."+ putStrLn "*** Please install CBMC and put it in your path!"+ putStrLn "*** CBMC can downloaded at http://www.cprover.org/cbmc/"+ putStrLn "***"+ Just _ -> return ()+ exitWith ExitSuccess+
+ copilot-cbmc.cabal view
@@ -0,0 +1,39 @@+cabal-version : >= 1.10+name : copilot-cbmc+version : 0.1+synopsis : .+description : .+license : BSD3+license-file : LICENSE+maintainer : leepike@galois.com+stability : Experimental+category : Language, Embedded+build-type : Custom+extra-source-files : README.md++author : Lee Pike+ , Robin Morisset+ , Alwyn Goodloe+ , Sebastian Niller+ , Nis Nordby Wegmann++source-repository head+ type: git+ location: git://github.com/niswegmann/copilot-cbmc.git++library+ default-language : Haskell2010+ hs-source-dirs : src+ ghc-options : -Wall -fwarn-tabs+ ghc-prof-options : -auto-all -caf-all++ build-depends : base >= 4.3 && < 5+ , bytestring+ , copilot-core+ , directory >= 1.1+ , process >= 1.0+ , pretty+ , copilot-sbv+ , copilot-c99++ exposed-modules : Copilot.Tools.CBMC
+ src/Copilot/Tools/CBMC.hs view
@@ -0,0 +1,125 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++{-# LANGUAGE GADTs #-}++module Copilot.Tools.CBMC (Params (..), defaultParams, genCBMC) 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 }++genCBMC :: Params -> Spec -> IO ()+genCBMC params spec =+ do+ 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 \"atm_copilot.h\""+ , text "#include \"sbv_copilot/sbv_copilot.h\""+ , text ""+ , 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 ""+ , 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 " atm_step();"+ , text " sbv_step();"+ , text " verify_observers();"+ , text " }"+ , text ""+ , text " return 0;"+ , 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 (ExtVar name t) =+ text name <+> text "=" <+> text "nondet_" <> typeSpec t <> text "();"++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 "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"+ 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"