diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,8 +1,11 @@ +[![Build Status](https://travis-ci.org/Copilot-Language/copilot-sbv.svg?branch=master)](https://travis-ci.org/Copilot-Language/copilot-sbv) + Overview ======== [copilot-sbv](http://hackage.haskell.org/package/copilot-sbv) Another back-end that translates to [SBV](http://hackage.haskell.org/package/sbv), using its code -generator to generate hard real-time C code as well. The ad +generator to generate hard real-time C code as well, with ACSL contracts, +for the value-analysis plugin and compiling the code with CompCert. 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 @@ -31,8 +34,41 @@ Dependencies ============= -copilot-sbv depends on the [SBV](http://hackage.haskell.org/package/sbv) library -to generate hard real-time C code. +copilot-sbv depends on the latest [SBV](http://hackage.haskell.org/package/sbv) library +to generate hard real-time C code. It is recommanded to obtain it from the git +[repository](https://github.com/LeventErkok/sbv/), and compile it yourself (ghc 7.10 needed). + +For the [ACSL](http://frama-c.com/acsl.html) , you need an up-to-date frama-c (Sodium), +and the value analysis plugin that goes with. Run to verify : + + make fval + +For compiling it with [CompCert](http://compcert.inria.fr/), +you need to install it, install the Standard [C library](http://compcert.inria.fr/man/manual002.html) for it, +wait until SBV allows you to change the compiler (or do it manually by changing the makefile generated), and +run the following command : + + make all + +There is also a [splint](http://www.splint.org/) support for the project. You need to install splint and run : + + make splint + +More about ACSL +============== +copilot-sbv generates automatic ACSL contracts for all functions and for global variables (in the form of +global invariants, which needs an up to date value analysis plugin for frama-c). The most important part of +generating contracts is transforming an expression about queues (such as drop 1 s1 + 3) into a ACSL contract. +This is done by a pretty printer, which translates each construct of the language into its ACSL equivalent. +However, some features are not implemented in the plugin yet, but are specified by ACSL (logical predicates ...). +This may result in a verification status "unknown" for predicates containing these expressions. Some are not specified +at all (asinh, ...), hence it compiles in a predicate that has to be user defined when implemented. + +Casts are badly supported (unknown status), hence it is recommanded to avoid them. Remember, your computer has more than +8kb of memory since 1980, use it ! + +Floats are very badly supported by SBV (only constant floats can be operands of floating functions). +Some issues are beeing fixed about that. Resources ========= diff --git a/copilot-sbv.cabal b/copilot-sbv.cabal --- a/copilot-sbv.cabal +++ b/copilot-sbv.cabal @@ -1,6 +1,6 @@ cabal-version : >= 1.10 name : copilot-sbv -version : 2.1.2 +version : 2.2.0 synopsis : A compiler for CoPilot targeting SBV. description : The Copilot back-end targeting SBV . @@ -9,10 +9,10 @@ Haskell that compiles into embedded C. Copilot contains an interpreter, multiple back-end compilers, and other verification tools. A tutorial, bug reports, and todos are available at - . + . . Examples are available at - . + . license : BSD3 license-file : LICENSE @@ -36,16 +36,19 @@ default-language : Haskell2010 hs-source-dirs : src ghc-options : -Wall -fwarn-tabs - ghc-prof-options : -auto-all -caf-all +-- ghc-prof-options : -auto-all -caf-all - build-depends : sbv >= 2.1 + build-depends : sbv >= 5.0 , base >= 4.0 && < 5 , containers >= 0.4 - , copilot-core >= 0.2.4 + , copilot-core == 2.2.0 + , directory >= 1.2.1 , pretty >= 1 , filepath >= 1.1 exposed-modules : Copilot.Compile.SBV + , Copilot.Compile.SBV.ACSLexpr + , Copilot.Compile.SBV.ACSLproof , Copilot.Compile.SBV.Code , Copilot.Compile.SBV.Common , Copilot.Compile.SBV.Copilot2SBV @@ -54,4 +57,5 @@ , Copilot.Compile.SBV.Queue , Copilot.Compile.SBV.Witness , Copilot.Compile.SBV.Driver + , Copilot.Compile.SBV.Transform , Copilot.Compile.SBV.Makefile diff --git a/src/Copilot/Compile/SBV.hs b/src/Copilot/Compile/SBV.hs --- a/src/Copilot/Compile/SBV.hs +++ b/src/Copilot/Compile/SBV.hs @@ -4,12 +4,15 @@ module Copilot.Compile.SBV ( compile + , proofACSL , compileWithSBV , sbvDirName , module Copilot.Compile.SBV.Params ) where import qualified Copilot.Core as C +import qualified Copilot.Core.PrettyPrint as C +import qualified Copilot.Core.PrettyDot as C import Copilot.Compile.Header.C99 (c99HeaderName, genC99Header) import qualified Data.SBV as S @@ -20,8 +23,11 @@ (updateStates, updateObservers, fireTriggers, getExtArrs, getExtFuns) import Copilot.Compile.SBV.MetaTable (allocMetaTable) import Copilot.Compile.SBV.Params +import qualified Copilot.Compile.SBV.Transform as T +import qualified Copilot.Compile.SBV.ACSLproof as T import System.FilePath (combine) +import qualified Debug.Trace as DB -------------------------------------------------------------------------------- @@ -30,8 +36,13 @@ sbvDirName :: String sbvDirName = "copilot-sbv-codegen" +proofACSL :: Params -> C.Spec -> IO () +proofACSL p s = do + writeFile "main.gv" (C.prettyPrintDot $ (s)) + compileWithSBV p [] (T.transformProofACSL s) + compile :: Params -> C.Spec -> IO () -compile p s = compileWithSBV p [] s +compile p s = compileWithSBV p [] (T.transform s) -- | sbvs are optional additional SBVCodeGens to generate. compileWithSBV :: Params -> [(String, S.SBVCodeGen ())] -> C.Spec -> IO () @@ -82,6 +93,7 @@ , "" , "To build, you will need to ensure that all external variables and triggers are visible." , "Also, modify driver.c to include a main() function." + , "Also, modify copilot_stdint.h to include your own definition of uint 8, 16, 32, 64 and int 8, 16, 32, 64." , "Once you have a valid C program, execute" , "" , " > make driver" @@ -90,6 +102,7 @@ , "" , "Please report bugs to lee pike at gmail . com (remove all spaces)." ] + -------------------------------------------------------------------------------- diff --git a/src/Copilot/Compile/SBV/ACSLexpr.hs b/src/Copilot/Compile/SBV/ACSLexpr.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/SBV/ACSLexpr.hs @@ -0,0 +1,131 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +-- | A pretty printer for Copilot specifications. + +{-# LANGUAGE GADTs #-} + +module Copilot.Compile.SBV.ACSLexpr + ( ppExpr + ) where + +import Copilot.Core +import Copilot.Core.Type.Show (showWithType, ShowType(..), showType) +import Prelude hiding (id) +import Text.PrettyPrint.HughesPJ +import Copilot.Compile.SBV.Common +import Copilot.Compile.SBV.MetaTable as MT hiding (ExternFun) +import qualified Data.Map as M +import Data.List (intersperse) + +-------------------------------------------------------------------------------- + +strmName :: Int -> Doc +strmName id = text "queue_" <> int id + + +ptrName :: Int -> Doc +ptrName id = text "ptr_" <> int id + +-------------------------------------------------------------------------------- + +ppExpr :: MT.MetaTable -> Expr a -> Doc +ppExpr meta e0 = parens $ case e0 of + Const t x -> text (showWithType Haskell t x) + Drop _ 0 id -> + let aa = M.lookup id (MT.streamInfoMap meta) + in case aa of + Just Stream { streamBuffer = ll } -> + let streamSize = (length ll) in + case streamSize of + 1 -> strmName id <> lbrack <> (text "0") <> rbrack + _ -> strmName id <> lbrack <> (ptrName id) <> rbrack + Drop _ i id -> + let aa = M.lookup id (MT.streamInfoMap meta) + in case aa of + Just Stream { streamBuffer = ll } -> + let streamSize = (length ll) in + strmName id <> lbrack <> lparen <> ptrName id <> text (" + " ++ show i) <> rparen <> text " % " <> int streamSize <> rbrack + ExternVar _ name _ -> text $ mkExtTmpVar name + ExternFun _ name _ _ tag -> (text $ mkExtTmpTag name tag) + ExternArray _ _ name + _ _ _ tag -> (text $ mkExtTmpTag name tag) + Local _ _ name e1 e2 -> text "\\let" <+> (text name) <+> equals + <+> (ppExpr meta e1) <+> text ";" <+> (ppExpr meta e2) + Var _ name -> (text name) + Op1 op e -> ppOp1 op (ppExpr meta e) + Op2 op e1 e2 -> ppOp2 op (ppExpr meta e1) (ppExpr meta e2) + Op3 op e1 e2 e3 -> ppOp3 op (ppExpr meta e1) (ppExpr meta e2) (ppExpr meta e3) + Label t s e -> (ppExpr meta e) + +ppUExpr :: MT.MetaTable -> UExpr -> Doc +ppUExpr meta UExpr { uExprExpr = e0 } = ppExpr meta e0 + +ppOp1 :: Op1 a b -> Doc -> Doc +ppOp1 op = case op of + Not -> ppPrefix "!" + Abs _ -> \x -> ((parens $ x <> (text " > 0")) <> text "? " <> x <> text " : -" <> x ) + Sign _ -> \x -> ((parens $ x <> (text " > 0")) <> text "? 1 : ") <> (parens $ x <> (text " < 0 ? -1 : ") <> x) + Recip _ -> ppPrefix "\\recip" + Exp _ -> ppPrefix "\\exp" + Sqrt _ -> ppPrefix "\\sqrt" + Log _ -> ppPrefix "\\log" + Sin _ -> ppPrefix "\\sin" + Tan _ -> ppPrefix "\\tan" + Cos _ -> ppPrefix "\\cos" + Asin _ -> ppPrefix "\\asin" + Atan _ -> ppPrefix "\\atan" + Acos _ -> ppPrefix "\\acos" + Sinh _ -> ppPrefix "\\sinh" + Tanh _ -> ppPrefix "\\tanh" + Cosh _ -> ppPrefix "\\cosh" + Asinh _ -> ppPrefix "\\asinh" + Atanh _ -> ppPrefix "\\atanh" + Acosh _ -> ppPrefix "\\acosh" + BwNot _ -> ppPrefix "~" + Cast _ _ -> ppPrefix "" + +ppOp2 :: Op2 a b c -> Doc -> Doc -> Doc +ppOp2 op = case op of + And -> ppInfix "&&" + Or -> ppInfix "||" + Add _ -> ppInfix "+" + Sub _ -> ppInfix "-" + Mul _ -> ppInfix "*" + Div _ -> ppInfix "/" + Mod _ -> ppInfix "%" + Fdiv _ -> ppInfix "/" + Pow _ -> ppPrefix2 "\\pow" + Logb _ -> \ a b -> (text "(\\log" <> (a) <> (text ") / ( \\log") <> (b) <> text ")") + Eq _ -> ppInfix "==" + Ne _ -> ppInfix "!=" + Le _ -> ppInfix "<=" + Ge _ -> ppInfix ">=" + Lt _ -> ppInfix "<" + Gt _ -> ppInfix ">" + BwAnd _ -> ppInfix "&" + BwOr _ -> ppInfix "|" + BwXor _ -> ppInfix "^" + BwShiftL _ _ -> ppInfix "<<" + BwShiftR _ _ -> ppInfix ">>" + +ppOp3 :: Op3 a b c d -> Doc -> Doc -> Doc -> Doc +ppOp3 op = case op of + Mux _ -> \ doc1 doc2 doc3 -> + text "(" <+> doc1 <+> + text "?" <+> doc2 <+> + text ":" <+> doc3 <> text ")" + +-------------------------------------------------------------------------------- + +ppInfix :: String -> Doc -> Doc -> Doc +ppInfix cs doc1 doc2 = parens $ doc1 <+> text cs <+> doc2 + + +ppPrefix2 :: String -> Doc -> Doc -> Doc +ppPrefix2 cs doc1 doc2 = parens $ text cs <+> doc1 <> text "," <+> doc2 + +ppPrefix :: String -> Doc -> Doc +ppPrefix cs doc = (text cs <+> lparen <> doc <> rparen) + diff --git a/src/Copilot/Compile/SBV/ACSLproof.hs b/src/Copilot/Compile/SBV/ACSLproof.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/SBV/ACSLproof.hs @@ -0,0 +1,305 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +{-# LANGUAGE GADTs, ExistentialQuantification #-} + +module Copilot.Compile.SBV.ACSLproof + ( transformProofACSL + ) +where + +import Prelude hiding (id) +import Data.Map (Map) +import qualified Data.Map as M + +import qualified Data.SBV as S +--import qualified Data.SBV.Internals as S + +import qualified Copilot.Compile.SBV.Queue as Q +import qualified Copilot.Compile.SBV.Witness as W + +import Copilot.Core +import Copilot.Core.Type +import Copilot.Core.Error (impossible) +import Copilot.Core.Type.Equality ((=~=), coerce, cong) + + +-------------------------------------------------------------------------------- +-- | A stream. +--data Stream = forall a. Typed a => Stream +-- { streamId :: Id +-- , streamBuffer :: [a] +-- , streamExpr :: Expr a +-- , streamExprType :: Type a } + +transformStream :: Stream -> Stream +transformStream Stream + { streamId = id + , streamBuffer = xs + , streamExpr = e + , streamExprType = t } = + Stream + { streamId = id + , streamBuffer = xs + , streamExpr = transformExpr e + , streamExprType = t } + +-------------------------------------------------------------------------------- + +-- | An observer. +--data Observer = forall a. Observer +-- { observerName :: Name +-- , observerExpr :: Expr a +-- , observerExprType :: Type a } + +transformObserver :: Observer -> Observer +transformObserver Observer + { observerName = name + , observerExpr = e + , observerExprType = t } = + Observer + { observerName = name + , observerExpr = transformExpr e + , observerExprType = t } + +-------------------------------------------------------------------------------- + +-- | A trigger. +--data Trigger = Trigger +-- { triggerName :: Name +-- , triggerGuard :: Expr Bool +-- , triggerArgs :: [UExpr] } + +transformTrigger :: Trigger -> Trigger +transformTrigger Trigger + { triggerName = name + , triggerGuard = guard + , triggerArgs = uexprl } = + Trigger + { triggerName = name + , triggerGuard = transformExpr guard + , triggerArgs = map transformUExpr uexprl } +-------------------------------------------------------------------------------- + +-- | A property. +--data Property = Property +-- { propertyName :: Name +-- , propertyExpr :: Expr Bool } + + +transformProperty :: Property -> Property +transformProperty Property + { propertyName = name + , propertyExpr = bexpr } = + Property + { propertyName = name + , propertyExpr = transformExpr bexpr } + +-------------------------------------------------------------------------------- + +-- | A Copilot specification consists of a list of variables bound to anonymous +-- streams, a lost of anomymous streams, a list of observers, and a list of +-- triggers. +--data Spec = Spec +-- { specStreams :: [Stream] +-- , specObservers :: [Observer] +-- , specTriggers :: [Trigger] +-- , specProperties :: [Property] } + +transformProofACSL :: Spec -> Spec +transformProofACSL Spec + { specStreams = strms + , specObservers = obsvs + , specTriggers = trigs + , specProperties = props + } = + Spec + { specStreams = map transformStream strms + , specObservers = map transformObserver obsvs + , specTriggers = map transformTrigger trigs + , specProperties = map transformProperty props + } + + + +-------------------------------------------------------------------------------- +--data UExpr = forall a. UExpr +-- { uExprType :: Type a +-- , uExprExpr :: Expr a } +transformUExpr :: UExpr -> UExpr +transformUExpr UExpr { uExprExpr = e, uExprType = t } = + UExpr { uExprExpr = transformExpr e, uExprType = t } + + +-------------------------------------------------------------------------------- +-- Expr transformation +-- +-- NO TREPASSING BEYOND THIS LINE +-- +-------------------------------------------------------------------------------- + +--data Expr a where +-- Const :: Type a -> a -> Expr a +-- Drop :: Type a -> DropIdx -> Id -> Expr a +-- Local :: Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b +-- Var :: Type a -> Name -> Expr a +-- ExternVar :: Type a -> Name -> Maybe [a] -> Expr a +-- ExternFun :: Type a -> Name -> [UExpr] -> Maybe (Expr a) +-- -> Maybe Tag -> Expr a +-- ExternArray :: Integral a => Type a -> Type b -> Name -> Int -> Expr a +-- -> Maybe [[b]] -> Maybe Tag -> Expr b +-- Op1 :: Op1 a b -> Expr a -> Expr b +-- Op2 :: Op2 a b c -> Expr a -> Expr b -> Expr c +-- Op3 :: Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d + +transformExpr :: Expr a -> Expr a +transformExpr e0 = case e0 of + Const t x -> Const t x + Drop t k id -> Drop t k id + Local t1 t2 name e1 e2 -> Local t1 t2 name (transformExpr e1) (transformExpr e2) + Var t name -> Var t name + ExternVar t name e -> ExternVar t name e + ExternFun t name args contxt yy-> ExternFun t name (map transformUExpr args) contxt yy + ExternArray t1 t2 name + size idx context yy-> ExternArray t1 t2 name size (transformExpr idx) context yy + Op1 op e -> transformOp1 op e + Op2 op e1 e2 -> transformOp2 op e1 e2 + Op3 op e1 e2 e3 -> transformOp3 op e1 e2 e3 + + Label t s e -> case s of + '?':m -> ExternFun t ("ident_"++(showType t)) [UExpr {uExprExpr = transformExpr $ Label t m $ e, uExprType = t}] Nothing Nothing + _ -> Label t s $ transformExpr e + + +showType :: Type a -> String +showType t = case t of + Bool -> "bool" + Int8 -> "int8" + Int16 -> "int16" + Int32 -> "int32" + Int64 -> "int64" + Word8 -> "word8" + Word16-> "word16" + Word32-> "word32" + Word64-> "word64" + Float -> "float" + Double-> "double" + +transformOp1 :: Op1 a b -> Expr a -> Expr b +transformOp1 op e = case op of + -- Boolean operators. + Not -> Op1 Not $ transformExpr e + -- Numeric operators. + Abs t -> Op2 (Mul t) (transformExpr e) (transformExpr $ Label t "?absolute_value_splitting" $ Op1 (Sign t) $ e) + Sign t -> Op1 (Sign t) $ transformExpr e + -- Fractional operators. + Recip a -> Op2 (Fdiv a) (Const a 1.0) (transformExpr e) + -- Floating operators. + Exp Float -> ExternFun Float "expf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Exp Double -> ExternFun Double "exp" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Sqrt Float -> ExternFun Float "sqrtf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Sqrt Double -> ExternFun Double "sqrt" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Log Float -> ExternFun Float "logf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Log Double -> ExternFun Double "log" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Sin Float -> ExternFun Float "sinf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Sin Double -> ExternFun Double "sin" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Cos Float -> ExternFun Float "cosf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Cos Double -> ExternFun Double "cos" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Tan Float -> ExternFun Float "tanf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Tan Double -> ExternFun Double "tan" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Asin Float -> ExternFun Float "asinf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Asin Double -> ExternFun Double "asin" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Acos Float -> ExternFun Float "acosf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Acos Double -> ExternFun Double "acos" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Atan Float -> ExternFun Float "atanf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Atan Double -> ExternFun Double "atan" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Sinh Float -> ExternFun Float "sinhf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Sinh Double -> ExternFun Double "sinh" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Cosh Float -> ExternFun Float "coshf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Cosh Double -> ExternFun Double "cosh" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Tanh Float -> ExternFun Float "tanhf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Tanh Double -> ExternFun Double "tanh" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Asinh Float -> ExternFun Float "asinhf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Asinh Double -> ExternFun Double "asinh" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Acosh Float -> ExternFun Float "acoshf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Acosh Double -> ExternFun Double "acosh" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Atanh Float -> ExternFun Float "atanhf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Atanh Double -> ExternFun Double "atanh" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + -- Bitwise operators. + BwNot t -> Op1 (BwNot t) $ transformExpr e + -- Casting operator. + Cast t s -> Op1 (Cast t s) $ transformExpr e + +transformOp2 :: Op2 a b c -> Expr a -> Expr b -> Expr c +transformOp2 op e1 e2 = case op of + -- Boolean operators. + And -> Op2 And (transformExpr e1) (transformExpr e2) + Or -> Op2 Or (transformExpr e1) (transformExpr e2) + -- Numeric operators. + Add t -> Op2 (Add t) (transformExpr e1) (transformExpr e2) + Sub t -> Op2 (Sub t) (transformExpr e1) (transformExpr e2) + Mul t -> Op2 (Mul t) (transformExpr e1) (transformExpr e2) + -- Integral operators. + Mod t -> Op2 (Mod t) (transformExpr e1) (transformExpr e2) + Div t -> Op2 (Div t) (transformExpr e1) (transformExpr e2) + -- Fractional operators. + Fdiv t -> Op2 (Fdiv t) (transformExpr e1) (transformExpr e2) + -- Floating operators. + Pow Float -> ExternFun Float "powf" + [UExpr { uExprExpr = transformExpr e1, uExprType = Float } + , UExpr { uExprExpr = transformExpr e2, uExprType = Float }] Nothing Nothing + Pow Double-> ExternFun Double "pow" + [UExpr { uExprExpr = transformExpr e1, uExprType = Double } + , UExpr { uExprExpr = transformExpr e2, uExprType = Double }] Nothing Nothing + Logb t -> Op2 (Fdiv t) (transformExpr $ Op1 (Log t) e1) (transformExpr $ Op1 (Log t) e2) + -- Equality operators. + Eq t -> Op2 (Eq t) (transformExpr e1) (transformExpr e2) + Ne t -> Op2 (Ne t) (transformExpr e1) (transformExpr e2) + -- Relational operators. + Le t -> Op2 (Le t) (transformExpr e1) (transformExpr e2) + Ge t -> Op2 (Ge t) (transformExpr e1) (transformExpr e2) + Lt t -> Op2 (Lt t) (transformExpr e1) (transformExpr e2) + Gt t -> Op2 (Gt t) (transformExpr e1) (transformExpr e2) + -- Bitwise operators. + BwAnd t -> Op2 (BwAnd t) (transformExpr e1) (transformExpr e2) + BwOr t -> Op2 (BwOr t) (transformExpr e1) (transformExpr e2) + BwXor t -> Op2 (BwXor t) (transformExpr e1) (transformExpr e2) + BwShiftL t s -> Op2 (BwShiftL t s) (transformExpr e1) (transformExpr e2) + BwShiftR t s -> Op2 (BwShiftR t s) (transformExpr e1) (transformExpr e2) + + +transformOp3 :: Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d +transformOp3 op e1 e2 e3 = case op of + Mux Bool -> Op2 Or (transformExpr $ Op2 And (e2) (e1)) (transformExpr $ Op2 And (e3) (Op1 Not e1)) + Mux t -> Op3 (Mux t) (transformExpr e1) (transformExpr e2) (transformExpr e3) diff --git a/src/Copilot/Compile/SBV/Code.hs b/src/Copilot/Compile/SBV/Code.hs --- a/src/Copilot/Compile/SBV/Code.hs +++ b/src/Copilot/Compile/SBV/Code.hs @@ -17,7 +17,11 @@ import Copilot.Compile.SBV.MetaTable import qualified Copilot.Compile.SBV.Witness as W import Copilot.Compile.SBV.Common +import Copilot.Compile.SBV.ACSLexpr +import qualified Copilot.Core.PrettyDot as PD +import qualified Text.PrettyPrint.HughesPJ as PJ + import qualified Copilot.Core as C import Copilot.Core.Type.Equality ((=~=), coerce, cong) @@ -43,10 +47,12 @@ where updateStreamState :: C.Stream -> SBVFunc updateStreamState C.Stream { C.streamId = id + , C.streamBuffer = buffer , C.streamExpr = e , C.streamExprType = t1 } = mkSBVFunc (mkUpdateStFn id) $ do + S.cgAddDecl [("/*test 001*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False e) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\result == " ++ (PJ.render $ ppExpr meta e) ++ ";\n*/")] inputs <- mkInputs meta (c2Args e) let e' = c2sExpr inputs e let Just strmInfo = M.lookup id (streamInfoMap meta) @@ -76,6 +82,7 @@ where mkSBVExp = do + S.cgAddDecl [("/*test 005*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False e) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\result == " ++ (PJ.render $ ppExpr meta e) ++ ";\n*/")] inputs <- mkInputs meta (c2Args e) let e' = c2sExpr inputs e W.SymWordInst <- return (W.symWordInst t) @@ -98,6 +105,7 @@ where go (i,e) = mkArgCall meta (mkTriggerArgFn i name) e mkSBVExp = do + S.cgAddDecl [("/*test 006*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False guard) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\result == " ++ (PJ.render $ ppExpr meta guard) ++ ";\n*/")] inputs <- mkInputs meta (c2Args guard) let e = c2sExpr inputs guard S.cgReturn e @@ -111,6 +119,7 @@ mkSBVFunc fnCallName mkExpr where mkExpr = do + S.cgAddDecl [("/*test 003*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False e) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\result == " ++ (PJ.render $ ppExpr meta e) ++ ";\n*/")] inputs <- mkInputs meta (c2Args e) let e' = c2sExpr inputs e W.SymWordInst <- return (W.symWordInst t) @@ -135,6 +144,7 @@ where mkSBVExpr :: S.SBVCodeGen () mkSBVExpr = do + S.cgAddDecl [("/*test 002*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False idx) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\result == " ++ (PJ.render $ ppExpr meta idx) ++ ";\n*/")] inputs <- mkInputs meta (c2Args idx) W.SymWordInst <- return (W.symWordInst t) W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t) @@ -143,7 +153,7 @@ -------------------------------------------------------------------------------- -- Generate an SBV function that calculates the Copilot expression to get the --- next index to sample an external array. +-- next index to sample an external function. getExtFuns :: MetaTable -> [SBVFunc] getExtFuns meta@(MetaTable { externFunInfoMap = exts }) = concatMap mkExtF (M.toList exts) @@ -180,7 +190,7 @@ -- External variables argToInput acc (Extern name) = let extInfos = externVarInfoMap meta in - let Just extInfo = M.lookup name extInfos in + let Just extInfo = M.lookup (name) extInfos in mkExtInput extInfo where @@ -204,7 +214,7 @@ mkExtInput C.ExtArray { C.externArrayElemType = t } = do v <- mkExtInput_ t (mkExtTmpTag name (Just tag)) - return acc { extArrs = (name, ExtInput + return acc { extArrs = ((mkExtTmpTag name (Just tag)), ExtInput { extInput = v , extType = t } ) : extArrs acc } @@ -222,7 +232,7 @@ mkExtInput C.ExtFun { C.externFunType = t } = do v <- mkExtInput_ t (mkExtTmpTag name (Just tag)) - return acc { extFuns = (name, ExtInput + return acc { extFuns = ((mkExtTmpTag name (Just tag)), ExtInput { extInput = v , extType = t } ) : extFuns acc } @@ -263,3 +273,4 @@ W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t) ext <- S.cgInput name return ext + diff --git a/src/Copilot/Compile/SBV/Copilot2SBV.hs b/src/Copilot/Compile/SBV/Copilot2SBV.hs --- a/src/Copilot/Compile/SBV/Copilot2SBV.hs +++ b/src/Copilot/Compile/SBV/Copilot2SBV.hs @@ -2,7 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- -{-# LANGUAGE GADTs, ExistentialQuantification #-} +{-# LANGUAGE GADTs, ExistentialQuantification, ScopedTypeVariables #-} module Copilot.Compile.SBV.Copilot2SBV ( c2sExpr @@ -22,13 +22,16 @@ import qualified Data.SBV as S --import qualified Data.SBV.Internals as S +import Copilot.Compile.SBV.Common import qualified Copilot.Compile.SBV.Queue as Q import qualified Copilot.Compile.SBV.Witness as W import Copilot.Core (Op1 (..), Op2 (..), Op3 (..), badUsage) import qualified Copilot.Core as C -import Copilot.Core.Error (impossible) +import qualified Copilot.Core.Type as C +import Copilot.Core.Error (badUsage, impossible) import Copilot.Core.Type.Equality ((=~=), coerce, cong) +import Data.Maybe (fromJust) -------------------------------------------------------------------------------- @@ -134,7 +137,7 @@ where ext :: ExtInput - ext = lookupInput name (extVars inputs) + ext = lookupInput name (extVars inputs) getSBV :: C.Type a -> ExtInput -> S.SBV a getSBV t1 ExtInput { extInput = ext' @@ -144,12 +147,12 @@ ---------------------------------------------------- - C.ExternArray _ t name _ _ _ _ -> + C.ExternArray _ t name _ _ _ tag -> getSBV t getExtArr where getExtArr :: ExtInput - getExtArr = lookupInput name (extArrs inputs) + getExtArr = lookupInput (mkExtTmpTag name (tag)) (extArrs inputs) getSBV t1 ExtInput { extInput = v , extType = t2 } @@ -158,12 +161,12 @@ ---------------------------------------------------- - C.ExternFun t name _ _ _ -> + C.ExternFun t name _ _ tag -> getSBV t getExtFun where getExtFun :: ExtInput - getExtFun = lookupInput name (extFuns inputs) + getExtFun = lookupInput (mkExtTmpTag name (tag)) (extFuns inputs) getSBV t1 ExtInput { extType = t2 , extInput = v } @@ -191,18 +194,21 @@ let res3 = c2sExpr_ e3 env inputs in c2sOp3 op res1 res2 res3 + C.Label t s e -> case W.symWordInst t of + W.SymWordInst -> S.label s (c2sExpr_ e env inputs) + -------------------------------------------------------------------------------- noFloatOpsErr :: String -> a noFloatOpsErr op = - badUsage ("Floating/Double operators not supported for the SBV backend: " - ++ "operator " ++ op ++ " not supported.") + badUsage ("The operation you used is not supported by the SBV backend: " + ++ "operator " ++ op ++ " not supported. Please change it with your math skills to something supported.") -------------------------------------------------------------------------------- c2sOp1 :: C.Op1 a b -> S.SBV a -> S.SBV b c2sOp1 op = case op of - Not -> \x -> S.ite (x S..== S.false) S.true S.false + Not -> (S.bnot) Abs t -> case W.symWordInst t of W.SymWordInst -> abs Sign t -> case W.symWordInst t of @@ -213,33 +219,45 @@ Cast t0 t1 -> case W.castInst t0 t1 of W.CastInst -> W.sbvCast - Recip _ -> noFloatOpsErr "recip" - Exp _ -> noFloatOpsErr "exp" - Sqrt _ -> noFloatOpsErr "sqrt" - Log _ -> noFloatOpsErr "log" - Sin _ -> noFloatOpsErr "sin" - Tan _ -> noFloatOpsErr "tan" - Cos _ -> noFloatOpsErr "cos" - Asin _ -> noFloatOpsErr "asin" - Atan _ -> noFloatOpsErr "atan" - Acos _ -> noFloatOpsErr "acos" - Sinh _ -> noFloatOpsErr "sinh" - Tanh _ -> noFloatOpsErr "tanh" - Cosh _ -> noFloatOpsErr "cosh" - Asinh _ -> noFloatOpsErr "asinh" - Atanh _ -> noFloatOpsErr "atanh" - Acosh _ -> noFloatOpsErr "acosh" + Recip _ -> noFloatOpsErr "recip" + Exp C.Float -> exp + Exp C.Double -> exp + Sqrt C.Float -> sqrt + Sqrt C.Double -> sqrt + Log C.Float -> log + Log C.Double -> log + Sin C.Float -> sin + Sin C.Double -> sin + Cos C.Float -> cos + Cos C.Double -> cos + Tan C.Float -> tan + Tan C.Double -> tan + Asin C.Float -> asin + Asin C.Double -> asin + Acos C.Float -> acos + Acos C.Double -> acos + Atan C.Float -> atan + Atan C.Double -> atan + Sinh C.Float -> sinh + Sinh C.Double -> sinh + Cosh C.Float -> cosh + Cosh C.Double -> cosh + Tanh C.Float -> tanh + Tanh C.Double -> tanh + Asinh C.Float -> asinh + Asinh C.Double -> asinh + Acosh C.Float -> acosh + Acosh C.Double -> acosh + Atanh C.Float -> atanh + Atanh C.Double -> atanh + -------------------------------------------------------------------------------- c2sOp2 :: C.Op2 a b c -> S.SBV a -> S.SBV b -> S.SBV c c2sOp2 op = case op of - And -> \x y -> S.ite (x S..== S.false) - S.false - (S.ite (y S..== S.false) S.false S.true) - Or -> \x y -> S.ite (x S..== S.false) - (S.ite (y S..== S.false) S.false S.true) - S.true + And -> (S.&&&) + Or -> (S.|||) Add t -> case W.symWordInst t of W.SymWordInst -> (+) Sub t -> case W.symWordInst t of W.SymWordInst -> (-) Mul t -> case W.symWordInst t of W.SymWordInst -> (*) @@ -260,23 +278,33 @@ BwOr t -> case W.bitsInst t of W.BitsInst -> (S..|.) BwXor t -> case W.bitsInst t of W.BitsInst -> (S.xor) BwShiftL tvec tidx -> - case W.bitsInst tvec of - W.BitsInst -> - \vec idx -> case W.symWordInst tidx of - W.SymWordInst -> case S.unliteral idx of - Nothing -> badUsage "Using the SBV backend, shiftL only supports constant shift indicies" - Just x -> S.shiftL vec (fromIntegral x) + case W.integralInst tvec of + W.IntegralInst -> + \vec idx -> case (W.integralInst tidx) of + W.IntegralInst -> S.sShiftLeft vec idx + --case S.unliteral idx of + -- Nothing -> badUsage "Using the SBV backend, shiftL only supports constant shift indicies" + -- Just x -> S.shiftL vec (fromIntegral x) BwShiftR tvec tidx -> - case W.bitsInst tvec of - W.BitsInst -> - \vec idx -> case W.symWordInst tidx of - W.SymWordInst -> case S.unliteral idx of - Nothing -> badUsage "Using the SBV backend, shiftR only supports constant shift indicies" - Just x -> S.shiftR vec (fromIntegral x) + case W.integralInst tvec of + W.IntegralInst -> + \vec idx -> case (W.integralInst tidx) of + W.IntegralInst -> S.sShiftRight vec idx - Fdiv _ -> noFloatOpsErr "fdiv" - Pow _ -> noFloatOpsErr "pow" - Logb _ -> noFloatOpsErr "logb" +-- case W.bitsInst tvec of +-- W.BitsInst -> +-- \vec idx -> case W.symWordInst tidx of +-- W.SymWordInst -> case S.unliteral idx of +-- Nothing -> badUsage "Using the SBV backend, shiftR only supports constant shift indicies" +-- Just x -> S.shiftR vec (fromIntegral x) + + Fdiv C.Float -> case W.numInst C.Float of W.NumInst -> (/) + Fdiv C.Double -> case W.numInst C.Double of W.NumInst -> (/) + Pow C.Float -> (**) + Pow C.Double -> (**) + Logb C.Float -> logBase + Logb C.Double -> logBase + c2sOp3 :: C.Op3 a b c d -> S.SBV a -> S.SBV b -> S.SBV c -> S.SBV d c2sOp3 op = case op of diff --git a/src/Copilot/Compile/SBV/Driver.hs b/src/Copilot/Compile/SBV/Driver.hs --- a/src/Copilot/Compile/SBV/Driver.hs +++ b/src/Copilot/Compile/SBV/Driver.hs @@ -19,6 +19,7 @@ import Data.List (intersperse) import qualified System.IO as I import Text.PrettyPrint.HughesPJ +import System.Directory import Copilot.Compile.SBV.MetaTable import Copilot.Compile.SBV.Queue (QueueSize) @@ -55,8 +56,9 @@ driver :: Params -> MetaTable -> C.Spec -> String -> String -> IO () driver params meta (C.Spec streams observers _ _) dir fileName = do let filePath = dir ++ '/' : driverName params - h <- I.openFile filePath I.WriteMode - let wr doc = I.hPutStrLn h (mkStyle doc) + let wr doc = I.appendFile filePath ((mkStyle doc) ++ "\n") + wr (text "a") + removeFile filePath wr ( text "/*" <+> text "Driver for SBV program generated from Copilot." @@ -64,10 +66,6 @@ wr (text "/*" <+> text "Edit as you see fit" <+> text "*/") wr (text "") - wr (text "#include ") - wr (text "#include ") - wr (text "#include ") - wr (text "#include ") wr (text "#include" <+> doubleQuotes (text fileName <> text ".h")) wr (text "#include" <+> doubleQuotes (text $ c99HeaderName (prefix params))) wr (text "") @@ -77,12 +75,30 @@ wr (text "") wr (text "/* Variables */") + wr (varDecls meta) +-- wr (writeACSLqueues meta) wr (text "") wr copilot + + wr (text "/* Idents */\n") + wr (text "/*@\n assigns \\nothing;\n */\nSBool ident_bool(SBool a) {return a;}") + wr (text "/*@\n assigns \\nothing;\n */\nSWord8 ident_word8(SWord8 a) {return a;}") + wr (text "/*@\n assigns \\nothing;\n */\nSWord16 ident_word16(SWord16 a) {return a;}") + wr (text "/*@\n assigns \\nothing;\n */\nSWord32 ident_word32(SWord32 a) {return a;}") + wr (text "/*@\n assigns \\nothing;\n */\nSWord64 ident_word64(SWord64 a) {return a;}") + wr (text "/*@\n assigns \\nothing;\n */\nSInt8 ident_int8(SInt8 a) {return a;}") + wr (text "/*@\n assigns \\nothing;\n */\nSInt16 ident_int16(SInt16 a) {return a;}") + wr (text "/*@\n assigns \\nothing;\n */\nSInt32 ident_int32(SInt32 a) {return a;}") + wr (text "/*@\n assigns \\nothing;\n */\nSInt64 ident_int64(SInt64 a) {return a;}") + wr (text "/*@\n assigns \\nothing;\n */\nSFloat ident_float(SFloat a) {return a;}") + wr (text "/*@\n assigns \\nothing;\n */\nSDouble ident_double(SDouble a) {return a;}") + wr (text "") wr driverFn + wr (text "") + wr testFn where mkStyle :: Doc -> String @@ -98,6 +114,11 @@ $$ mkFuncCall updateBuffersF [] <> semi $$ mkFuncCall updatePtrsF [] <> semi ) + testFn :: Doc + testFn = + mkFunc (withPrefix (prefix params) "testing") + ( text "for(;;) step()"<> semi + ) copilot = vcat $ intersperse (text "") [ sampleExts meta @@ -185,7 +206,7 @@ varDecl :: Decl -> Doc varDecl Decl { retT = t, declVar = v, initVal = i } = - t <+> v <+> equals <+> i <> semi + text "static"<+> t <+> v <+> equals <+> i <> semi cShow :: String -> String cShow "True" = show (1::Int) @@ -216,16 +237,36 @@ -- the assignment of extVars in the definition of extArrs. The Analyzer.hs -- copilot-core prevents arrays or functions from being used in arrays or -- functions. - mkFunc sampleExtsF $ vcat (extVars ++ extArrs ++ extFuns) + --extACSL $$ + (mkFunc ("static " ++ sampleExtsF) $ vcat (extVars ++ extArrs ++ extFuns)) where + --ll = sampleVExtACSL extVMap ++ sampleAExtACSL extAMap ++ sampleFExtACSL extFMap + --extACSL = vcat [text "/*@", +-- (case ll of + -- [] -> text " assigns \\nothing;" +-- _ -> vcat $ ll) +-- ,text "*/"] extVars = map sampleVExt ((fst . unzip . M.toList) extVMap) +-- extADecl = map sampleAExt1 (M.toList extAMap) +-- extFDecl = map sampleFExt1 (M.toList extFMap) extArrs = map sampleAExt (M.toList extAMap) extFuns = map sampleFExt (M.toList extFMap) -------------------------------------------------------------------------------- -- Variables + +--sampleVExtACSL :: M.Map C.Name C.ExtVar -> [Doc] +--sampleVExtACSL extVMap = +-- (map sampleVExtACSL1 ((fst . unzip . M.toList) extVMap)) ++ (map sampleVExtACSL2 ((fst . unzip . M.toList) extVMap)) +--sampleVExtACSL1 :: C.Name -> Doc +--sampleVExtACSL1 name = +-- text " assigns" <+> text (mkExtTmpVar name) <> semi +--sampleVExtACSL2 :: C.Name -> Doc +--sampleVExtACSL2 name = +-- text " //ensures" <+> text (mkExtTmpVar name) <+> text "==" <+> text name <> semi + sampleVExt :: C.Name -> Doc sampleVExt name = text (mkExtTmpVar name) <+> equals <+> text name <> semi @@ -236,13 +277,48 @@ -- Currenty, Analyze.hs in copilot-language forbids recurssion in external -- arrays or functions (i.e., an external array can't use another external array -- to compute it's index). +--sampleAExtACSL :: M.Map C.Tag C.ExtArray -> [Doc] +--sampleAExtACSL extAMap = +-- (map sampleAExtACSL1 (M.toList extAMap)) ++ (map sampleAExtACSL2 (M.toList extAMap)) +-- +--sampleAExtACSL1 :: (Int, C.ExtArray) -> Doc +--sampleAExtACSL1 (_, C.ExtArray { C.externArrayName = name +-- , C.externArrayIdx = idx +-- , C.externArrayTag = t }) +-- = +-- text " assigns" <+> text (mkExtTmpTag name t) <+> semi + + +--sampleAExtACSL2 :: (Int, C.ExtArray) -> Doc +--sampleAExtACSL2 (_, C.ExtArray { C.externArrayName = name +-- , C.externArrayIdx = idx +-- , C.externArrayTag = t }) +-- = +-- text " //ensures" <+> text (mkExtTmpTag name t) <+> text "==" <+> text ("tmp_"++(mkExtTmpTag name t)) <> semi + +--sampleAExt1 :: (Int, C.ExtArray) -> Doc +--sampleAExt1 (_, C.ExtArray { C.externArrayName = name +-- , C.externArrayIdx = idx +-- , C.externArrayElemType = tttt +-- , C.externArrayTag = t }) +-- = (retType tttt) <+> text ("tmp_"++(mkExtTmpTag name t)) <+> equals <+> arrIdx name idx +-- +-- where +-- arrIdx :: C.Name -> C.Expr a -> Doc +-- arrIdx name' e = text name' <> lbrack <> idxFCall e <> rbrack <> semi + + -- Ok, because the analyzer disallows arrays or function calls in index + -- expressions, and we assign all variables before arrays. +-- idxFCall :: C.Expr a -> Doc +-- idxFCall e = +-- mkFuncCall (mkExtArrFn name) (map text $ collectArgs e) + sampleAExt :: (Int, C.ExtArray) -> Doc sampleAExt (_, C.ExtArray { C.externArrayName = name , C.externArrayIdx = idx + , C.externArrayElemType = tttt , C.externArrayTag = t }) - = - text (mkExtTmpTag name t) <+> equals <+> arrIdx name idx - + = text (mkExtTmpTag name t) <+> equals <+> arrIdx name idx <> semi where arrIdx :: C.Name -> C.Expr a -> Doc arrIdx name' e = text name' <> lbrack <> idxFCall e <> rbrack <> semi @@ -255,17 +331,50 @@ -------------------------------------------------------------------------------- +--sampleFExtACSL :: M.Map C.Tag C.ExtFun -> [Doc] +--sampleFExtACSL extFMap = +-- (map sampleFExtACSL1 (M.toList extFMap)) ++ (map sampleFExtACSL2 (M.toList extFMap)) + +--sampleFExtACSL1 :: (Int, C.ExtFun) -> Doc +--sampleFExtACSL1 (_, C.ExtFun { C.externFunName = name +-- , C.externFunArgs = args +-- , C.externFunTag = tag }) +-- = +-- text " assigns" <+> text (mkExtTmpTag name tag) <> semi +--sampleFExtACSL2 :: (Int, C.ExtFun) -> Doc +--sampleFExtACSL2 (_, C.ExtFun { C.externFunName = name +-- , C.externFunArgs = args +-- , C.externFunTag = tag }) +-- = +-- text " //ensures" <+> text (mkExtTmpTag name tag) <+> text "==" <+> text ("tmp_"++(mkExtTmpTag name tag)) <> semi + + -- External functions +--sampleFExt1 :: (Int, C.ExtFun) -> Doc +--sampleFExt1 (_, C.ExtFun { C.externFunName = name +-- , C.externFunArgs = args +-- , C.externFunType = tttt +-- , C.externFunTag = tag }) +-- = +-- (retType tttt) <+> text ("tmp_"++(mkExtTmpTag name tag)) <+> equals <+> text name <> lparen +-- <> hsep (punctuate comma $ map mkArgCall (zip [(0 :: Int) ..] args)) +-- <> rparen <> semi +-- +-- where +-- mkArgCall :: (Int, C.UExpr) -> Doc +-- mkArgCall (i, C.UExpr { C.uExprExpr = e }) = +-- mkFuncCall (mkExtFunArgFn i name tag) (map text $ collectArgs e) + sampleFExt :: (Int, C.ExtFun) -> Doc sampleFExt (_, C.ExtFun { C.externFunName = name , C.externFunArgs = args + , C.externFunType = tttt , C.externFunTag = tag }) = text (mkExtTmpTag name tag) <+> equals <+> text name <> lparen <> hsep (punctuate comma $ map mkArgCall (zip [(0 :: Int) ..] args)) <> rparen <> semi - - where + where mkArgCall :: (Int, C.UExpr) -> Doc mkArgCall (i, C.UExpr { C.uExprExpr = e }) = mkFuncCall (mkExtFunArgFn i name tag) (map text $ collectArgs e) @@ -273,8 +382,7 @@ -------------------------------------------------------------------------------- updateStates :: [C.Stream] -> Doc -updateStates streams = - mkFunc updateStatesF $ vcat $ map updateSt streams +updateStates [] = (text "/*@\n assigns \\nothing;\n */") $$ (mkFunc ("static " ++ updateStatesF) $ vcat $ map updateSt []) where updateSt :: C.Stream -> Doc updateSt C.Stream { C.streamId = id @@ -284,13 +392,38 @@ (map text $ collectArgs e) <> semi +updateStates streams = (text "/*@\n") <> (hcat $ map updateStACSL (streams)) <+> (text "*/") $$ + (mkFunc ("static " ++ updateStatesF) $ vcat $ map updateSt streams) + where + updateStACSL :: C.Stream -> Doc + updateStACSL C.Stream { C.streamId = id + , C.streamExpr = e } = + text " assigns "<> text (mkTmpStVar id) <> semi <> text "\n" + + + updateSt :: C.Stream -> Doc + updateSt C.Stream { C.streamId = id + , C.streamExpr = e } = + text (mkTmpStVar id) <+> equals + <+> mkFuncCall (mkUpdateStFn id) + (map text $ collectArgs e) + <> semi + -------------------------------------------------------------------------------- updateObservers :: Params -> MetaTable -> Doc updateObservers params MetaTable { observerInfoMap = observers } - = - mkFunc observersF $ vcat $ map updateObsv (M.toList observers) + = let ll = M.toList observers + in (case ll of + [] -> text "/*@\n assigns \\nothing;\n */" + _ -> (text "/*@\n") <> (hcat $ map updateObsvACSL (ll)) <+> (text "*/") + )$$ + (mkFunc ("static " ++ observersF) $ vcat $ map updateObsv (ll)) where + updateObsvACSL :: (C.Name, ObserverInfo) -> Doc + updateObsvACSL (name, ObserverInfo { observerArgs = args }) = + text " assigns" <+> text (withPrefix (prefix params) name) <> semi <> text "\n" + updateObsv :: (C.Name, ObserverInfo) -> Doc updateObsv (name, ObserverInfo { observerArgs = args }) = text (withPrefix (prefix params) name) <+> text "=" <+> @@ -300,8 +433,8 @@ fireTriggers :: MetaTable -> Doc fireTriggers MetaTable { triggerInfoMap = triggers } - = - mkFunc triggersF $ vcat $ map fireTrig (M.toList triggers) + = -- text "/*@\n assigns \\nothing; \n*/" $$ + (mkFunc ("static " ++ triggersF) $ vcat $ map fireTrig (M.toList triggers)) where -- if (guard) trigger(args); @@ -324,12 +457,51 @@ -------------------------------------------------------------------------------- +writeACSLqueues :: MetaTable -> Doc +writeACSLqueues MetaTable { streamInfoMap = strMap } = + let ll = M.toList strMap + in + + vcat $ (text "/*ACSL following*/\n"):(case ll of + [] -> [text ""] + _ -> (text "/*@" :(map varAndUpdate (ll) ++ [(text "*/")])) + ) + + where + varAndUpdate :: (C.Id, C.Stream) -> Doc + varAndUpdate (id, C.Stream { C.streamBuffer = que }) = + updateFunc (mkQueueVar id) (fromIntegral $ length que) (mkQueuePtrVar id) + + -- idx = (idx + 1) % queueSize; + updateFunc :: String -> QueueSize -> String -> Doc + updateFunc que sz ptr = + text (" global invariant a_bound_"++ ptr ++":") <+>text ptr <+> text "<" <+> int (fromIntegral sz) <+> semi <+> + text ("\n global invariant a_pos_"++ ptr ++":") <+>text ptr <+> text ">=" <+> int (0) <+> semi <+> + text ("\n global invariant a_valid_"++ ptr ++": \\valid") <+> lparen <> text que <+> text "+" <+> lparen <> text "0.." <+> int ((fromIntegral sz) - 1) <+> rparen <> rparen <> semi + +-------------------------------------------------------------------------------- + updateBuffers :: MetaTable -> Doc updateBuffers MetaTable { streamInfoMap = strMap } - = - mkFunc updateBuffersF $ vcat $ map updateBuf (M.toList strMap) + = let ll = M.toList strMap + in (case ll of + [] -> text "/*@\n assigns \\nothing;\n */" + _ -> (text "/*@\n") <> (hcat $ map updateBufACSL (ll)) <+> (text "*/") + )$$ + (mkFunc ("static " ++ updateBuffersF) $ vcat $ map updateBuf (ll)) where + + updateBufACSL :: (C.Id, C.Stream) -> Doc + updateBufACSL (id, _) = + updateFuncACSL (mkQueueVar id) (mkQueuePtrVar id) (mkTmpStVar id) + + -- queue_strX[ptr] = newVal; + updateFuncACSL :: String -> String -> String -> Doc + updateFuncACSL que ptr tmp = + text " assigns" <+> text que <> lbrack <> text ptr <> rbrack <> semi <> + (text "\n ensures" <+> text que <> lbrack <> text ptr <> rbrack <+> text "==" <+> text tmp <> semi <> text "\n") + updateBuf :: (C.Id, C.Stream) -> Doc updateBuf (id, _) = updateFunc (mkQueueVar id) (mkQueuePtrVar id) (mkTmpStVar id) @@ -343,9 +515,27 @@ updatePtrs :: MetaTable -> Doc updatePtrs MetaTable { streamInfoMap = strMap } = - mkFunc updatePtrsF $ vcat $ map varAndUpdate (M.toList strMap) + let ll = M.toList strMap + in (case ll of + [] -> text "/*@\n assigns \\nothing;\n */" + _ -> (text "/*@\n") <> (hcat $ map varAndUpdateACSL (ll)) <+> (text "*/") + )$$ + (mkFunc ("static " ++ updatePtrsF) $ vcat $ map varAndUpdate (ll)) where + + varAndUpdateACSL :: (C.Id, C.Stream) -> Doc + varAndUpdateACSL (id, C.Stream { C.streamBuffer = que }) = + updateFuncACSL (fromIntegral $ length que) (mkQueuePtrVar id) + + -- idx = (idx + 1) % queueSize; + updateFuncACSL :: QueueSize -> String -> Doc + updateFuncACSL sz ptr = + text " assigns" <+> text ptr <> semi <> (text "\n ensures" <+> text ptr <+> text "==" + <+> lparen <> text "\\old (" <> text ptr <+> text ") +" <+> int 1 <> rparen + <+> text "%" <+> int (fromIntegral sz) <> semi <> text "\n") + + varAndUpdate :: (C.Id, C.Stream) -> Doc varAndUpdate (id, C.Stream { C.streamBuffer = que }) = updateFunc (fromIntegral $ length que) (mkQueuePtrVar id) @@ -384,5 +574,8 @@ C.Word16 -> "SWord16" C.Word32 -> "SWord32" C.Word64 -> "SWord64" + + C.Float -> "SFloat" + C.Double -> "SDouble" _ -> C.badUsage "You've tried to compile a Copilot program to SBV with a type SBV does not support. SBV does not support floats or doubles. To compile programs using these types, use the copilot-c99 (Atom) backend. See README.md for more information." diff --git a/src/Copilot/Compile/SBV/Makefile.hs b/src/Copilot/Compile/SBV/Makefile.hs --- a/src/Copilot/Compile/SBV/Makefile.hs +++ b/src/Copilot/Compile/SBV/Makefile.hs @@ -12,6 +12,8 @@ import Text.PrettyPrint.HughesPJ import qualified System.IO as I +import System.Directory + -------------------------------------------------------------------------------- makefileName :: Params -> String @@ -23,9 +25,12 @@ makefile params dir sbvName = do let filePath = dir ++ '/' : (makefileName params) fileName = "copilot" - h <- I.openFile filePath I.WriteMode - let wr doc = I.hPutStrLn h (mkStyle doc) + let wr doc = I.appendFile filePath ((mkStyle doc) ++ "\n") + + wr (text "a") + removeFile filePath wr (text "# Makefile rules for the Copilot driver.") + wr (text "\nCCFLAGS=-fnone \nCC=ccomp\nSHELL := /bin/bash") wr (text "") wr $ text "driver" <> colon <+> text (driverName params) <+> text (withPre fileName) <> text ".h" @@ -37,6 +42,12 @@ , text "-o" , text "$@" , archive]) + wr $ text "\nfval" <> colon + <+> text ("\n\tframa-c -val -main testing -slevel 10000000 *.h *.c | tee logval") + wr $ text "\nfwp" <> colon + <+> text ("\n\tparallel frama-c -wp -wp-out . -wp-timeout 20 -wp-prover CVC4 -wp-split {} ::: *.c | tee >logfwp >(grep 'Proved\\|Unknown\\|Timeout\\|Failed\\|Qed:\\s\\|CVC4:\\s\\|Parsing .*\\.c' > logfwpcompact) >(grep 'Proved\\|Qed:\\s\\|CVC4:\\s\\|Unknown\\|Timeout\\|Failed\\|Parsing .*\\.c')") + wr $ text "\nsplint" <> colon + <+> text ("\n\tsplint -comment-char % *.h *.c | tee logsplint") where archive = text sbvName <> text ".a" diff --git a/src/Copilot/Compile/SBV/MetaTable.hs b/src/Copilot/Compile/SBV/MetaTable.hs --- a/src/Copilot/Compile/SBV/MetaTable.hs +++ b/src/Copilot/Compile/SBV/MetaTable.hs @@ -25,6 +25,7 @@ import Data.Map (Map) import Data.List (nub) +import Data.Maybe (fromJust) import qualified Data.Map as M import Prelude hiding (id) @@ -125,19 +126,19 @@ -------------------------------------------------------------------------------- -- Kinds of arguments to SBV functions -data Arg = Extern C.Name - | ExternFun C.Name C.Tag - | ExternArr C.Name C.Tag - | Queue C.Id +data Arg = Extern C.Name + | ExternFun C.Name C.Tag + | ExternArr C.Name C.Tag + | Queue C.Id deriving Eq -- | Normal argument calls. argToCall :: Arg -> [String] -argToCall (Extern name) = [mkExtTmpVar name] -argToCall (ExternArr name tag) = [mkExtTmpTag name (Just tag)] -argToCall (ExternFun name tag) = [mkExtTmpTag name (Just tag)] -argToCall (Queue id) = [ mkQueueVar id - , mkQueuePtrVar id ] +argToCall (Extern name) = [mkExtTmpVar name] +argToCall (ExternArr name tag) = [mkExtTmpTag name (Just tag)] +argToCall (ExternFun name tag) = [mkExtTmpTag name (Just tag)] +argToCall (Queue id) = [ mkQueueVar id + , mkQueuePtrVar id ] -------------------------------------------------------------------------------- @@ -170,7 +171,7 @@ C.Var _ _ -> [] - C.ExternVar _ name _ -> [Extern name] + C.ExternVar _ name _ -> [Extern name] C.ExternFun _ name args _ tag -> (ExternFun name (tagExtract tag)) : @@ -178,7 +179,7 @@ -> c2Args expr) args - C.ExternArray _ _ name _ _ _ tag -> [ExternArr name (tagExtract tag)] + C.ExternArray _ _ name _ _ _ tag ->[ExternArr name (tagExtract tag)] C.Op1 _ e -> c2Args_ e @@ -186,4 +187,5 @@ C.Op3 _ e1 e2 e3 -> c2Args_ e1 ++ c2Args_ e2 ++ c2Args_ e3 --------------------------------------------------------------------------------- + C.Label _ _ e -> c2Args_ e + diff --git a/src/Copilot/Compile/SBV/Transform.hs b/src/Copilot/Compile/SBV/Transform.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/SBV/Transform.hs @@ -0,0 +1,306 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +{-# LANGUAGE GADTs, ExistentialQuantification #-} + +module Copilot.Compile.SBV.Transform + ( transform + ) +where + +import Prelude hiding (id) +import Data.Map (Map) +import qualified Data.Map as M + +import qualified Data.SBV as S +--import qualified Data.SBV.Internals as S + +import qualified Copilot.Compile.SBV.Queue as Q +import qualified Copilot.Compile.SBV.Witness as W + +import Copilot.Core +import Copilot.Core.Type +import Copilot.Core.Error (impossible) +import Copilot.Core.Type.Equality ((=~=), coerce, cong) + + +-------------------------------------------------------------------------------- +-- | A stream. +--data Stream = forall a. Typed a => Stream +-- { streamId :: Id +-- , streamBuffer :: [a] +-- , streamExpr :: Expr a +-- , streamExprType :: Type a } + +transformStream :: Stream -> Stream +transformStream Stream + { streamId = id + , streamBuffer = xs + , streamExpr = e + , streamExprType = t } = + Stream + { streamId = id + , streamBuffer = xs + , streamExpr = transformExpr e + , streamExprType = t } + +-------------------------------------------------------------------------------- + +-- | An observer. +--data Observer = forall a. Observer +-- { observerName :: Name +-- , observerExpr :: Expr a +-- , observerExprType :: Type a } + +transformObserver :: Observer -> Observer +transformObserver Observer + { observerName = name + , observerExpr = e + , observerExprType = t } = + Observer + { observerName = name + , observerExpr = transformExpr e + , observerExprType = t } + +-------------------------------------------------------------------------------- + +-- | A trigger. +--data Trigger = Trigger +-- { triggerName :: Name +-- , triggerGuard :: Expr Bool +-- , triggerArgs :: [UExpr] } + +transformTrigger :: Trigger -> Trigger +transformTrigger Trigger + { triggerName = name + , triggerGuard = guard + , triggerArgs = uexprl } = + Trigger + { triggerName = name + , triggerGuard = transformExpr guard + , triggerArgs = map transformUExpr uexprl } +-------------------------------------------------------------------------------- + +-- | A property. +--data Property = Property +-- { propertyName :: Name +-- , propertyExpr :: Expr Bool } + + +transformProperty :: Property -> Property +transformProperty Property + { propertyName = name + , propertyExpr = bexpr } = + Property + { propertyName = name + , propertyExpr = transformExpr bexpr } + +-------------------------------------------------------------------------------- + +-- | A Copilot specification consists of a list of variables bound to anonymous +-- streams, a lost of anomymous streams, a list of observers, and a list of +-- triggers. +--data Spec = Spec +-- { specStreams :: [Stream] +-- , specObservers :: [Observer] +-- , specTriggers :: [Trigger] +-- , specProperties :: [Property] } + +transform :: Spec -> Spec +transform Spec + { specStreams = strms + , specObservers = obsvs + , specTriggers = trigs + , specProperties = props + } = + Spec + { specStreams = map transformStream strms + , specObservers = map transformObserver obsvs + , specTriggers = map transformTrigger trigs + , specProperties = map transformProperty props + } + + + +-------------------------------------------------------------------------------- +--data UExpr = forall a. UExpr +-- { uExprType :: Type a +-- , uExprExpr :: Expr a } +transformUExpr :: UExpr -> UExpr +transformUExpr UExpr { uExprExpr = e, uExprType = t } = + UExpr { uExprExpr = transformExpr e, uExprType = t } + +transformSExpr :: (Name, UExpr) -> (Name, UExpr) +transformSExpr (name, UExpr { uExprExpr = e, uExprType = t }) = + (name, transformUExpr UExpr { uExprExpr = e, uExprType = t }) + + +-------------------------------------------------------------------------------- +-- Expr transformation +-- +-- NO TREPASSING BEYOND THIS LINE +-- +-------------------------------------------------------------------------------- + +--data Expr a where +-- Const :: Type a -> a -> Expr a +-- Drop :: Type a -> DropIdx -> Id -> Expr a +-- Local :: Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b +-- Var :: Type a -> Name -> Expr a +-- ExternVar :: Type a -> Name -> Maybe [a] -> Expr a +-- ExternFun :: Type a -> Name -> [UExpr] -> Maybe (Expr a) +-- -> Maybe Tag -> Expr a +-- ExternArray :: Integral a => Type a -> Type b -> Name -> Int -> Expr a +-- -> Maybe [[b]] -> Maybe Tag -> Expr b +-- Op1 :: Op1 a b -> Expr a -> Expr b +-- Op2 :: Op2 a b c -> Expr a -> Expr b -> Expr c +-- Op3 :: Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d + +transformExpr :: Expr a -> Expr a +transformExpr e0 = case e0 of + Const t x -> Const t x + Drop t k id -> Drop t k id + Local t1 t2 name e1 e2 -> Local t1 t2 name (transformExpr e1) (transformExpr e2) + Var t name -> Var t name + ExternVar t name e -> ExternVar t name e + ExternFun t name args contxt yy-> ExternFun t name (map transformUExpr args) contxt yy + ExternArray t1 t2 name + size idx context yy-> ExternArray t1 t2 name size (transformExpr idx) context yy + Op1 op e -> transformOp1 op e + Op2 op e1 e2 -> transformOp2 op e1 e2 + Op3 op e1 e2 e3 -> transformOp3 op e1 e2 e3 + + Label t s e -> Label t s $ transformExpr e + + +{-showType :: Type a -> String +showType t = case t of + Bool -> "bool" + Int8 -> "int8" + Int16 -> "int16" + Int32 -> "int32" + Int64 -> "int64" + Word8 -> "word8" + Word16-> "word16" + Word32-> "word32" + Word64-> "word64" + Float -> "float" + Double-> "double"-} + +transformOp1 :: Op1 a b -> Expr a -> Expr b +transformOp1 op e = case op of + -- Boolean operators. + Not -> Op1 Not $ transformExpr e + -- Numeric operators. + Abs t -> Op1 (Abs t) (transformExpr e) + Sign t -> Op1 (Sign t) $ transformExpr e + -- Fractional operators. + Recip a -> Op2 (Fdiv a) (Const a 1.0) (transformExpr e) + -- Floating operators. + Exp Float -> ExternFun Float "expf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Exp Double -> ExternFun Double "exp" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Sqrt Float -> ExternFun Float "sqrtf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Sqrt Double -> ExternFun Double "sqrt" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Log Float -> ExternFun Float "logf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Log Double -> ExternFun Double "log" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Sin Float -> ExternFun Float "sinf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Sin Double -> ExternFun Double "sin" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Cos Float -> ExternFun Float "cosf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Cos Double -> ExternFun Double "cos" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Tan Float -> ExternFun Float "tanf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Tan Double -> ExternFun Double "tan" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Asin Float -> ExternFun Float "asinf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Asin Double -> ExternFun Double "asin" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Acos Float -> ExternFun Float "acosf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Acos Double -> ExternFun Double "acos" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Atan Float -> ExternFun Float "atanf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Atan Double -> ExternFun Double "atan" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Sinh Float -> ExternFun Float "sinhf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Sinh Double -> ExternFun Double "sinh" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Cosh Float -> ExternFun Float "coshf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Cosh Double -> ExternFun Double "cosh" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Tanh Float -> ExternFun Float "tanhf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Tanh Double -> ExternFun Double "tanh" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Asinh Float -> ExternFun Float "asinhf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Asinh Double -> ExternFun Double "asinh" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Acosh Float -> ExternFun Float "acoshf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Acosh Double -> ExternFun Double "acosh" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + Atanh Float -> ExternFun Float "atanhf" + [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing + Atanh Double -> ExternFun Double "atanh" + [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing + -- Bitwise operators. + BwNot t -> Op1 (BwNot t) $ transformExpr e + -- Casting operator. + Cast t s -> Op1 (Cast t s) $ transformExpr e + +transformOp2 :: Op2 a b c -> Expr a -> Expr b -> Expr c +transformOp2 op e1 e2 = case op of + -- Boolean operators. + And -> Op2 And (transformExpr e1) (transformExpr e2) + Or -> Op2 Or (transformExpr e1) (transformExpr e2) + -- Numeric operators. + Add t -> Op2 (Add t) (transformExpr e1) (transformExpr e2) + Sub t -> Op2 (Sub t) (transformExpr e1) (transformExpr e2) + Mul t -> Op2 (Mul t) (transformExpr e1) (transformExpr e2) + -- Integral operators. + Mod t -> Op2 (Mod t) (transformExpr e1) (transformExpr e2) + Div t -> Op2 (Div t) (transformExpr e1) (transformExpr e2) + -- Fractional operators. + Fdiv t -> Op2 (Fdiv t) (transformExpr e1) (transformExpr e2) + -- Floating operators. + Pow Float -> ExternFun Float "powf" + [UExpr { uExprExpr = transformExpr e1, uExprType = Float } + , UExpr { uExprExpr = transformExpr e2, uExprType = Float }] Nothing Nothing + Pow Double-> ExternFun Double "pow" + [UExpr { uExprExpr = transformExpr e1, uExprType = Double } + , UExpr { uExprExpr = transformExpr e2, uExprType = Double }] Nothing Nothing + Logb t -> Op2 (Fdiv t) (transformExpr $ Op1 (Log t) e1) (transformExpr $ Op1 (Log t) e2) + -- Equality operators. + Eq t -> Op2 (Eq t) (transformExpr e1) (transformExpr e2) + Ne t -> Op2 (Ne t) (transformExpr e1) (transformExpr e2) + -- Relational operators. + Le t -> Op2 (Le t) (transformExpr e1) (transformExpr e2) + Ge t -> Op2 (Ge t) (transformExpr e1) (transformExpr e2) + Lt t -> Op2 (Lt t) (transformExpr e1) (transformExpr e2) + Gt t -> Op2 (Gt t) (transformExpr e1) (transformExpr e2) + -- Bitwise operators. + BwAnd t -> Op2 (BwAnd t) (transformExpr e1) (transformExpr e2) + BwOr t -> Op2 (BwOr t) (transformExpr e1) (transformExpr e2) + BwXor t -> Op2 (BwXor t) (transformExpr e1) (transformExpr e2) + BwShiftL t s -> Op2 (BwShiftL t s) (transformExpr e1) (transformExpr e2) + BwShiftR t s -> Op2 (BwShiftR t s) (transformExpr e1) (transformExpr e2) + + +transformOp3 :: Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d +transformOp3 op e1 e2 e3 = case op of + Mux t -> Op3 (Mux t) (transformExpr e1) (transformExpr e2) (transformExpr e3) diff --git a/src/Copilot/Compile/SBV/Witness.hs b/src/Copilot/Compile/SBV/Witness.hs --- a/src/Copilot/Compile/SBV/Witness.hs +++ b/src/Copilot/Compile/SBV/Witness.hs @@ -14,6 +14,7 @@ , OrdInst(..) , ordInst , MergeableInst(..) , mergeableInst , BitsInst(..) , bitsInst + , IntegralInst(..) , integralInst ) where import qualified Data.SBV as S @@ -28,6 +29,9 @@ badInst :: a badInst = error "Fatal cast in the witnesses of SBV in copilot-sbv. Are you sure that SBV supports the type you are using? (It doesn't support floats or doubles.) If you you are, or you don't understand the error, email leepike @ gmail . com (remove spaces) or file a bug report on github.com" +badFloat :: a +badFloat = error "Fatal error : You did something illegal with floating points numbers (a mod b, or something like that)" + -------------------------------------------------------------------------------- data SymWordInst a = S.SymWord a => SymWordInst @@ -40,8 +44,8 @@ C.Int32 -> SymWordInst ; C.Int64 -> SymWordInst C.Word8 -> SymWordInst ; C.Word16 -> SymWordInst C.Word32 -> SymWordInst ; C.Word64 -> SymWordInst - C.Float -> badInst - C.Double -> badInst + C.Float -> SymWordInst + C.Double -> SymWordInst -------------------------------------------------------------------------------- @@ -55,8 +59,8 @@ C.Int32 -> NumInst ; C.Int64 -> NumInst C.Word8 -> NumInst ; C.Word16 -> NumInst C.Word32 -> NumInst ; C.Word64 -> NumInst - C.Float -> badInst - C.Double -> badInst + C.Float -> NumInst + C.Double -> NumInst -------------------------------------------------------------------------------- @@ -74,8 +78,8 @@ C.Word16 -> HasSignAndSizeInst C.Word32 -> HasSignAndSizeInst C.Word64 -> HasSignAndSizeInst - C.Float -> badInst - C.Double -> badInst + C.Float -> HasSignAndSizeInst + C.Double -> HasSignAndSizeInst -------------------------------------------------------------------------------- @@ -89,8 +93,8 @@ C.Int32 -> EqInst ; C.Int64 -> EqInst C.Word8 -> EqInst ; C.Word16 -> EqInst C.Word32 -> EqInst ; C.Word64 -> EqInst - C.Float -> badInst - C.Double -> badInst + C.Float -> EqInst + C.Double -> EqInst -------------------------------------------------------------------------------- @@ -108,8 +112,8 @@ C.Word16 -> BVDivisibleInst C.Word32 -> BVDivisibleInst C.Word64 -> BVDivisibleInst - C.Float -> badInst - C.Double -> badInst + C.Float -> badFloat + C.Double -> badFloat -------------------------------------------------------------------------------- @@ -123,8 +127,8 @@ C.Int32 -> OrdInst ; C.Int64 -> OrdInst C.Word8 -> OrdInst ; C.Word16 -> OrdInst C.Word32 -> OrdInst ; C.Word64 -> OrdInst - C.Float -> badInst - C.Double -> badInst + C.Float -> OrdInst + C.Double -> OrdInst -------------------------------------------------------------------------------- @@ -138,8 +142,8 @@ C.Int32 -> MergeableInst ; C.Int64 -> MergeableInst C.Word8 -> MergeableInst ; C.Word16 -> MergeableInst C.Word32 -> MergeableInst ; C.Word64 -> MergeableInst - C.Float -> badInst - C.Double -> badInst + C.Float -> MergeableInst + C.Double -> MergeableInst -------------------------------------------------------------------------------- @@ -153,11 +157,26 @@ C.Int32 -> BitsInst ; C.Int64 -> BitsInst C.Word8 -> BitsInst ; C.Word16 -> BitsInst C.Word32 -> BitsInst ; C.Word64 -> BitsInst - C.Float -> badInst - C.Double -> badInst + C.Float -> badFloat + C.Double -> badFloat -------------------------------------------------------------------------------- +data IntegralInst a = S.SIntegral a => IntegralInst + +integralInst :: C.Type a -> IntegralInst a +integralInst t = + case t of + C.Bool -> badInst + C.Int8 -> IntegralInst ; C.Int16 -> IntegralInst + C.Int32 -> IntegralInst ; C.Int64 -> IntegralInst + C.Word8 -> IntegralInst ; C.Word16 -> IntegralInst + C.Word32 -> IntegralInst ; C.Word64 -> IntegralInst + C.Float -> badFloat + C.Double -> badFloat + +-------------------------------------------------------------------------------- + data CastInst a b = SBVCast a b => CastInst castInst :: C.Type a -> C.Type b -> CastInst a b @@ -180,43 +199,97 @@ C.Word16 -> CastInst C.Word32 -> CastInst C.Word64 -> CastInst + C.Int8 -> CastInst C.Int16 -> CastInst C.Int32 -> CastInst C.Int64 -> CastInst + C.Float -> CastInst + C.Double -> CastInst _ -> badInst C.Word16 -> case t1 of + C.Word8 -> CastInst C.Word16 -> CastInst C.Word32 -> CastInst C.Word64 -> CastInst + C.Int8 -> CastInst + C.Int16 -> CastInst C.Int32 -> CastInst C.Int64 -> CastInst + C.Float -> CastInst + C.Double -> CastInst _ -> badInst C.Word32 -> case t1 of + C.Word8 -> CastInst + C.Word16 -> CastInst C.Word32 -> CastInst C.Word64 -> CastInst + C.Int8 -> CastInst + C.Int16 -> CastInst + C.Int32 -> CastInst C.Int64 -> CastInst + C.Float -> CastInst + C.Double -> CastInst _ -> badInst C.Word64 -> case t1 of + C.Word8 -> CastInst + C.Word16 -> CastInst + C.Word32 -> CastInst C.Word64 -> CastInst + C.Int8 -> CastInst + C.Int16 -> CastInst + C.Int32 -> CastInst + C.Int64 -> CastInst + C.Float -> CastInst + C.Double -> CastInst _ -> badInst C.Int8 -> case t1 of + C.Word8 -> CastInst + C.Word16 -> CastInst + C.Word32 -> CastInst + C.Word64 -> CastInst C.Int8 -> CastInst C.Int16 -> CastInst C.Int32 -> CastInst C.Int64 -> CastInst + C.Float -> CastInst + C.Double -> CastInst _ -> badInst C.Int16 -> case t1 of + C.Word8 -> CastInst + C.Word16 -> CastInst + C.Word32 -> CastInst + C.Word64 -> CastInst + C.Int8 -> CastInst C.Int16 -> CastInst C.Int32 -> CastInst C.Int64 -> CastInst + C.Float -> CastInst + C.Double -> CastInst _ -> badInst C.Int32 -> case t1 of + C.Word8 -> CastInst + C.Word16 -> CastInst + C.Word32 -> CastInst + C.Word64 -> CastInst + C.Int8 -> CastInst + C.Int16 -> CastInst C.Int32 -> CastInst C.Int64 -> CastInst + C.Float -> CastInst + C.Double -> CastInst _ -> badInst C.Int64 -> case t1 of + C.Word8 -> CastInst + C.Word16 -> CastInst + C.Word32 -> CastInst + C.Word64 -> CastInst + C.Int8 -> CastInst + C.Int16 -> CastInst + C.Int32 -> CastInst C.Int64 -> CastInst + C.Float -> CastInst + C.Double -> CastInst _ -> badInst C.Float -> badInst C.Double -> badInst @@ -252,92 +325,215 @@ sbvCast = castBool instance SBVCast Bool Int8 where - sbvCast = castErr + sbvCast = castBool instance SBVCast Bool Int16 where - sbvCast = castErr + sbvCast = castBool instance SBVCast Bool Int32 where - sbvCast = castErr + sbvCast = castBool instance SBVCast Bool Int64 where - sbvCast = castErr + sbvCast = castBool -------------------------------------------------------------------------------- instance SBVCast Word8 Word8 where - sbvCast = id + sbvCast = S.sFromIntegral instance SBVCast Word8 Word16 where - sbvCast = S.extend + sbvCast = S.sFromIntegral instance SBVCast Word8 Word32 where - sbvCast = S.extend . S.extend + sbvCast = S.sFromIntegral instance SBVCast Word8 Word64 where - sbvCast = S.extend . S.extend . S.extend + sbvCast = S.sFromIntegral +instance SBVCast Word8 Int8 where + sbvCast = S.sFromIntegral instance SBVCast Word8 Int16 where - sbvCast = castErr + sbvCast = S.sFromIntegral instance SBVCast Word8 Int32 where - sbvCast = castErr + sbvCast = S.sFromIntegral instance SBVCast Word8 Int64 where - sbvCast = castErr + sbvCast = S.sFromIntegral +instance SBVCast Word8 Float where + sbvCast = S.toSFloat S.sRoundNearestTiesToEven +instance SBVCast Word8 Double where + sbvCast = S.toSDouble S.sRoundNearestTiesToEven + -------------------------------------------------------------------------------- +instance SBVCast Word16 Word8 where + sbvCast = S.sFromIntegral instance SBVCast Word16 Word16 where - sbvCast = id + sbvCast = S.sFromIntegral instance SBVCast Word16 Word32 where - sbvCast = S.extend + sbvCast = S.sFromIntegral instance SBVCast Word16 Word64 where - sbvCast = S.extend . S.extend + sbvCast = S.sFromIntegral +instance SBVCast Word16 Int8 where + sbvCast = S.sFromIntegral +instance SBVCast Word16 Int16 where + sbvCast = S.sFromIntegral instance SBVCast Word16 Int32 where - sbvCast = castErr + sbvCast = S.sFromIntegral instance SBVCast Word16 Int64 where - sbvCast = castErr + sbvCast = S.sFromIntegral +instance SBVCast Word16 Float where + sbvCast = S.toSFloat S.sRoundNearestTiesToEven +instance SBVCast Word16 Double where + sbvCast = S.toSDouble S.sRoundNearestTiesToEven + -------------------------------------------------------------------------------- +instance SBVCast Word32 Word8 where + sbvCast = S.sFromIntegral +instance SBVCast Word32 Word16 where + sbvCast = S.sFromIntegral instance SBVCast Word32 Word32 where - sbvCast = id + sbvCast = S.sFromIntegral instance SBVCast Word32 Word64 where - sbvCast = S.extend + sbvCast = S.sFromIntegral +instance SBVCast Word32 Int8 where + sbvCast = S.sFromIntegral +instance SBVCast Word32 Int16 where + sbvCast = S.sFromIntegral +instance SBVCast Word32 Int32 where + sbvCast = S.sFromIntegral instance SBVCast Word32 Int64 where - sbvCast = castErr + sbvCast = S.sFromIntegral +instance SBVCast Word32 Float where + sbvCast = S.toSFloat S.sRoundNearestTiesToEven +instance SBVCast Word32 Double where + sbvCast = S.toSDouble S.sRoundNearestTiesToEven + -------------------------------------------------------------------------------- +instance SBVCast Word64 Word8 where + sbvCast = S.sFromIntegral +instance SBVCast Word64 Word16 where + sbvCast = S.sFromIntegral +instance SBVCast Word64 Word32 where + sbvCast = S.sFromIntegral instance SBVCast Word64 Word64 where - sbvCast = id + sbvCast = S.sFromIntegral +instance SBVCast Word64 Int8 where + sbvCast = S.sFromIntegral +instance SBVCast Word64 Int16 where + sbvCast = S.sFromIntegral +instance SBVCast Word64 Int32 where + sbvCast = S.sFromIntegral +instance SBVCast Word64 Int64 where + sbvCast = S.sFromIntegral + +instance SBVCast Word64 Float where + sbvCast = S.toSFloat S.sRoundNearestTiesToEven +instance SBVCast Word64 Double where + sbvCast = S.toSDouble S.sRoundNearestTiesToEven + -------------------------------------------------------------------------------- instance SBVCast Int8 Int8 where - sbvCast = castErr + sbvCast = S.sFromIntegral instance SBVCast Int8 Int16 where - sbvCast = castErr + sbvCast = S.sFromIntegral instance SBVCast Int8 Int32 where - sbvCast = castErr + sbvCast = S.sFromIntegral instance SBVCast Int8 Int64 where - sbvCast = castErr + sbvCast = S.sFromIntegral +instance SBVCast Int8 Word8 where + sbvCast = S.sFromIntegral +instance SBVCast Int8 Word16 where + sbvCast = S.sFromIntegral +instance SBVCast Int8 Word32 where + sbvCast = S.sFromIntegral +instance SBVCast Int8 Word64 where + sbvCast = S.sFromIntegral + +instance SBVCast Int8 Float where + sbvCast = S.toSFloat S.sRoundNearestTiesToEven +instance SBVCast Int8 Double where + sbvCast = S.toSDouble S.sRoundNearestTiesToEven + -------------------------------------------------------------------------------- +instance SBVCast Int16 Int8 where + sbvCast = S.sFromIntegral instance SBVCast Int16 Int16 where - sbvCast = castErr + sbvCast = S.sFromIntegral instance SBVCast Int16 Int32 where - sbvCast = castErr + sbvCast = S.sFromIntegral instance SBVCast Int16 Int64 where - sbvCast = castErr + sbvCast = S.sFromIntegral +instance SBVCast Int16 Word8 where + sbvCast = S.sFromIntegral +instance SBVCast Int16 Word16 where + sbvCast = S.sFromIntegral +instance SBVCast Int16 Word32 where + sbvCast = S.sFromIntegral +instance SBVCast Int16 Word64 where + sbvCast = S.sFromIntegral + +instance SBVCast Int16 Float where + sbvCast = S.toSFloat S.sRoundNearestTiesToEven +instance SBVCast Int16 Double where + sbvCast = S.toSDouble S.sRoundNearestTiesToEven + -------------------------------------------------------------------------------- +instance SBVCast Int32 Int8 where + sbvCast = S.sFromIntegral +instance SBVCast Int32 Int16 where + sbvCast = S.sFromIntegral instance SBVCast Int32 Int32 where - sbvCast = castErr + sbvCast = S.sFromIntegral instance SBVCast Int32 Int64 where - sbvCast = castErr + sbvCast = S.sFromIntegral +instance SBVCast Int32 Word8 where + sbvCast = S.sFromIntegral +instance SBVCast Int32 Word16 where + sbvCast = S.sFromIntegral +instance SBVCast Int32 Word32 where + sbvCast = S.sFromIntegral +instance SBVCast Int32 Word64 where + sbvCast = S.sFromIntegral + +instance SBVCast Int32 Float where + sbvCast = S.toSFloat S.sRoundNearestTiesToEven +instance SBVCast Int32 Double where + sbvCast = S.toSDouble S.sRoundNearestTiesToEven + -------------------------------------------------------------------------------- +instance SBVCast Int64 Int8 where + sbvCast = S.sFromIntegral +instance SBVCast Int64 Int16 where + sbvCast = S.sFromIntegral +instance SBVCast Int64 Int32 where + sbvCast = S.sFromIntegral instance SBVCast Int64 Int64 where - sbvCast = castErr + sbvCast = S.sFromIntegral +instance SBVCast Int64 Word8 where + sbvCast = S.sFromIntegral +instance SBVCast Int64 Word16 where + sbvCast = S.sFromIntegral +instance SBVCast Int64 Word32 where + sbvCast = S.sFromIntegral +instance SBVCast Int64 Word64 where + sbvCast = S.sFromIntegral + +instance SBVCast Int64 Float where + sbvCast = S.toSFloat S.sRoundNearestTiesToEven +instance SBVCast Int64 Double where + sbvCast = S.toSDouble S.sRoundNearestTiesToEven + -------------------------------------------------------------------------------- + +