copilot-sbv 2.1.2 → 2.2.0

raw patch · 12 files changed

+1379/−143 lines, 12 filesdep +directorydep ~copilot-coredep ~sbvPVP ok

version bump matches the API change (PVP)

Dependencies added: directory

Dependency ranges changed: copilot-core, sbv

API changes (from Hackage documentation)

Files

• README.md +39/−3
• copilot-sbv.cabal +10/−6
• src/Copilot/Compile/SBV.hs +14/−1
• src/Copilot/Compile/SBV/ACSLexpr.hs +131/−0
• src/Copilot/Compile/SBV/ACSLproof.hs +305/−0
• src/Copilot/Compile/SBV/Code.hs +15/−4
• src/Copilot/Compile/SBV/Copilot2SBV.hs +75/−47
• src/Copilot/Compile/SBV/Driver.hs +215/−22
• src/Copilot/Compile/SBV/Makefile.hs +13/−2
• src/Copilot/Compile/SBV/MetaTable.hs +14/−12
• src/Copilot/Compile/SBV/Transform.hs +306/−0
• src/Copilot/Compile/SBV/Witness.hs +242/−46

@@ -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 =========

@@ -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 <http://hackage.haskell.org/package/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-  <https://github.com/niswegmann/copilot-discussion>.+  <https://github.com/Copilot-Language/copilot-discussion>.   .   Examples are available at-  <https://github.com/leepike/Copilot/tree/master/Examples>.+  <https://github.com/Copilot-Language/Copilot/tree/master/Examples>.  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

@@ -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)."   ]+  -------------------------------------------------------------------------------- 

@@ -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)+

@@ -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) 

@@ -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+

@@ -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

@@ -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 <inttypes.h>")-  wr (text "#include <stdbool.h>")-  wr (text "#include <stdint.h>")-  wr (text "#include <stdio.h>")   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."

@@ -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"

@@ -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+

@@ -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) 

@@ -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+ --------------------------------------------------------------------------------++