improve 0.2.3 → 0.3.0

raw patch · 5 files changed

+381/−46 lines, 5 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Language/ImProve.hs +15/−6
• Language/ImProve/Code.hs +331/−4
• Language/ImProve/Core.hs +29/−31
• Language/ImProve/Verify.hs +4/−4
• improve.cabal +2/−1

@@ -57,13 +57,13 @@ /Assertion Statements/  @-assert(condition);        'assert' condition+assert(condition);        'theorem' name k lemmas condition @  /Statement Labels/  @-label: {                  \"label\" '|' do+label: {                  \"label\" '-|' do     a();                      a     b();                      b }@@ -78,7 +78,7 @@ false                     'false' 0                         0 100                       100-1.0                       1     -- float+1.0                       1 3.14                      3.14  /Variable Reference/@@ -225,6 +225,7 @@ import qualified Language.ImProve.Verify as V import qualified Language.ImProve.Code   as C +--infixl 9 !, !. infixl 7 *., /., `div_`, `mod_` infix  4 ==., /=., <., <=., >., >=. infixl 3 &&.@@ -342,7 +343,7 @@ mod_ _ 0 = error "divide by zero (mod_)" mod_ a b = Mod a b --- | Linear interpolation and extrapolation between two points.+-- | Linear interpolation and extrapolation of two points. linear :: (Float, Float) -> (Float, Float) -> E Float -> E Float linear (x1, y1) (x2, y2) a = a *. slope + constant inter   where@@ -359,6 +360,14 @@ mux :: AllE a => E Bool -> E a -> E a -> E a mux = Mux +-- | Array index to a variable.+--(!) :: AllE a => A a -> E Int -> V a+--(!) a i = VArray a i++-- | Array index to an expression.+--(!.) :: AllE a => A a -> E Int -> E a+--(!.) a i = ref $ a ! i+ -- | Labels a statement and creates a variable scope. --   Labels are used in counter examples to trace the program execution. --   And assertion names, and hence counter example trace file names, are produce from labels.@@ -464,8 +473,8 @@ -- | Declare an assumption condition is true. --   Assumptions expressions must contain variables directly or indirectly related --   to the assertion under verification, otherwise they will be ignored.-assume :: E Bool -> Stmt ()-assume a = statement $ Assume a+assume :: Name -> E Bool -> Stmt ()+assume name a = statement $ Label name $ Assume a  -- | Theorem to be proven or used as lemmas to assist proofs of other theorems. data Theorem = Theorem' Int

@@ -1,13 +1,17 @@ module Language.ImProve.Code (code) where +import Control.Monad.State import Data.List+import Data.Maybe import Text.Printf  import Language.ImProve.Core import Language.ImProve.Tree hiding (Branch) import qualified Language.ImProve.Tree as T --- | Generate C code.+infixr 0 :-, :=++-- | Generate C and Simulink code. code :: Name -> Statement -> IO () code name stmt = do   writeFile (name ++ ".c") $@@ -21,8 +25,9 @@        "/* Generated by ImProve. */\n\n"     ++ codeVariables False scope ++ "\n"     ++ "void " ++ name ++ "(void);\n\n"+  codeMdl name stmt   where-  scope = case tree (\ (_, path, _) -> path) $ map varInfo $ stmtVars stmt of+  scope = case tree (\ (_, path, _) -> path) $ stmtVars stmt of     [] -> error "program contains no useful statements"     a  -> T.Branch (name ++ "_variables") a @@ -34,8 +39,8 @@   Branch a b Null -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt name path b) ++ "}\n"   Branch a b c    -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt name path b) ++ "}\nelse {\n" ++ indent (codeStmt name path c) ++ "}\n"   Sequence a b -> codeStmt name path a ++ codeStmt name path b-  Theorem _ _ _ a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n"-  Assume a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n"+  Theorem _ _ _ a -> "assert((" ++ show (pathName path) ++ ", " ++ codeExpr a ++ "));\n"+  Assume a -> "assert((" ++ show (pathName path) ++ ", " ++ codeExpr a ++ "));\n"   Label name' a -> "/*" ++ name' ++ "*/\n" ++ indent (codeStmt name (path ++ [name']) a)   Null -> ""   where@@ -93,4 +98,326 @@   Bool  _ -> "int"   Int   _ -> "int"   Float _ -> "float"+++type Net = StateT Netlist IO++data Block+  = Inport  Const+  | Outport Const+  | UnitDelay Const+  | Cast String+  | Assertion+  | Const' Const+  | Add'+  | Sub'+  | Mul'+  | Div'+  | Mod'+  | Not'+  | And'+  | Or'+  | Eq'+  | Lt'+  | Gt'+  | Le'+  | Ge'+  | Mux'++data Netlist = Netlist+  { nextId :: Int+  , path   :: Path+  , vars   :: [Path]+  , env    :: [Name]+  , blocks :: [(Name, Block)]+  , nets   :: [(Name, (Name, Int))]+  }++-- Simulink generation.+codeMdl :: Name -> Statement -> IO ()+codeMdl name stmt = do+  net <- execStateT all (Netlist 0 [] paths env [] [])+  writeFile (name ++ ".mdl") $ show $ mdl name $ (mdlBlocks $ blocks net) ++ (mdlLines $ nets net)+  where+  vars = stmtVars stmt+  paths = [ path | (_, path, _) <- vars ]+  env = [ error $ "variable " ++ pathName a ++ " does not have a source" | a <- vars ]++  all :: Net ()+  all = do+    inputs <- mapM input vars+    elaborate stmt+    mapM_ output $ zip vars inputs++  input :: VarInfo -> Net Name+  input (input, path, const) = if input+    then do+      a <- block' (pathName path) (Inport const)+      updateEnv path a+      return a+    else do+      a <- block $ UnitDelay const+      b <- block $ Cast $ constType const+      net a (b, 0)+      updateEnv path b+      return a+  +  output :: (VarInfo, Name) -> Net ()+  output ((True, _, _), _) = return ()+  output ((False, path, const), delay) = do+    a <- block' (pathName path) $ Outport const+    src <- getNet path+    net src (a, 0)+    net src (delay, 0)++newName :: Net Name+newName = do+  net <- get+  put net { nextId = nextId net + 1 }+  return $ "b" ++ show (nextId net)++-- New unnamed block.+block :: Block -> Net Name+block a = do+  name <- newName+  modify $ \ net -> net { blocks = (name, a) : blocks net }+  return name++-- New named block.+block' :: Name -> Block -> Net Name+block' name a = do+  modify $ \ net -> net { blocks = (name, a) : blocks net }+  return name++-- New net.+net :: Name -> (Name, Int) -> Net ()+net src (dest, port) = modify $ \ net -> net { nets = (src, (dest, port)) : nets net }++updateEnv :: Path -> Name -> Net ()+updateEnv path name = do+  net <- get+  let i = fromJust $ elemIndex path $ vars net+      pre = take i $ env net+      post = drop (i + 1) $ env net+  put net { env = pre ++ [name] ++ post }++getNet :: Path -> Net Name+getNet path = do+  net <- get+  return $ env net !! (fromJust $ elemIndex path $ vars net)++getPathName :: Net Name+getPathName = do+  net <- get+  return $ pathName $ path net++-- Elaborate netlist.+elaborate :: Statement -> Net ()+elaborate a = case a of ++  Assign (V _ path _) b -> do+    b <- evalExpr b+    updateEnv path b++  Branch a b c -> do+    cond <- evalExpr a+    net0 <- get++    elaborate b+    net1 <- get+    modify $ \ net -> net { env = env net0 }++    elaborate c+    net2 <- get+    modify $ \ net -> net { env = env net0 }++    names <- mergeEnvs cond (env net1) (env net2)+    modify $ \ net -> net { env = names }++    where++    mergeEnvs :: Name -> [Name] -> [Name] -> Net [Name]+    mergeEnvs _ [] [] = return []+    mergeEnvs cond (a : as) (b : bs) = do+      names <- mergeEnvs cond as bs+      name <- if a == b then return a else do+        switch <- block Mux'+        net a    (switch, 0)+        net cond (switch, 1)+        net b    (switch, 2)+        return switch+      return $ name : names+    mergeEnvs _ _ _ = error "unbalanced environments"++  Sequence a b    -> elaborate a >> elaborate b++  Theorem _ _ _ a -> do+    a <- evalExpr a+    name <- getPathName+    assert <- block' name Assertion+    net a (assert, 0)++  Assume a -> do+    a <- evalExpr a+    name <- getPathName+    assert <- block' name Assertion+    net a (assert, 0)++  Label name a -> do+    modify $ \ net -> net { path = path net ++ [name] }+    elaborate a+    modify $ \ net -> net { path = init $ path net }++  Null            -> return ()++evalExpr :: E a -> Net Name+evalExpr a = case a of+  Ref (V _ path _) -> getNet path+  Const a   -> block $ Const' $ const' a+  Add a b   -> f2 Add' a b+  Sub a b   -> f2 Sub' a b+  Mul a b   -> do+    b <- block $ Const' $ const' b+    f2' Mul' a b+  Div a b   -> do+    b <- block $ Const' $ const' b+    f2' Div' a b+  Mod a b   -> do+    b <- block $ Const' $ const' b+    f2' Mod' a b+  Not a     -> f1 Not' a+  And a b   -> f2 And' a b+  Or  a b   -> f2 Or'  a b+  Eq  a b   -> f2 Eq'  a b+  Lt  a b   -> f2 Lt'  a b+  Gt  a b   -> f2 Gt'  a b+  Le  a b   -> f2 Le'  a b+  Ge  a b   -> f2 Ge'  a b+  Mux a b c -> f3 Mux' b a c+  where+  f1 :: Block -> E a -> Net Name+  f1 b a1 = do+    a1 <- evalExpr a1+    b  <- block b+    net a1 (b, 0)+    return b++  f2 :: Block -> E a -> E b -> Net Name+  f2 b a1 a2 = do+    a1 <- evalExpr a1+    a2 <- evalExpr a2+    b  <- block b+    net a1 (b, 0)+    net a2 (b, 1)+    return b++  f2' :: Block -> E a -> Name -> Net Name+  f2' b a1 a2 = do+    a1 <- evalExpr a1+    b  <- block b+    net a1 (b, 0)+    net a2 (b, 1)+    return b++  f3 :: Block -> E a -> E b -> E c -> Net Name+  f3 b a1 a2 a3 = do+    a1 <- evalExpr a1+    a2 <- evalExpr a2+    a3 <- evalExpr a3+    b  <- block b+    net a1 (b, 0)+    net a2 (b, 1)+    net a3 (b, 2)+    return b++data Mdl+  = String :- String+  | String := [Mdl]++instance Show Mdl where+  show a = case a of+    name :- value -> name ++ "\t" ++ show value ++ "\n"+    name := items -> name ++ " {\n" ++ indent (concatMap show items) ++ "}\n"+    where+    indent = unlines . map ('\t' :) . lines++mdl :: Name -> [Mdl] -> Mdl+mdl name blocks = "Library" :=+  [ "Name" :- name+  , "System" :=+    [ "Name" :- name+    , "Block" :=+      [ "BlockType" :- "SubSystem"+      , "Name" :- name+      , "TreatAsAtomicUnit" :- "on"+      , "System" := ("Name" :- name) : blocks+      ]+    ]+  ]++mdlLines :: [(Name, (Name, Int))] -> [Mdl]+mdlLines nets = map branch branches+  where+  branches :: [(Name, [(Name, Int)])]+  branches = [ (src, [ dest | (src', dest) <- nets, src == src' ]) | src <- nub $ fst $ unzip nets ]+  branch :: (Name, [(Name, Int)]) -> Mdl+  branch (src, dests) = "Line" :=+    [ "SrcBlock" :- src+    , "SrcPort"  :- "1"+    ] ++ (if length dests == 1 then head dests' else map ("Branch" :=) dests')+    where+    dests' = [ ["DstBlock" :- dest, "DstPort" :- show $ port + 1] | (dest, port) <- dests ]++mdlBlocks :: [(Name, Block)] -> [Mdl]+mdlBlocks blocks = map (port "Inport") inputs ++ map blk others ++ map (port "Outport") outputs+  where+  inputs  = zip [1 ..] $ sortBy (\ (a, _) (b, _) -> compare a b) [ (name, constType init) | (name, Inport  init) <- blocks ]+  outputs = zip [1 ..] $ sortBy (\ (a, _) (b, _) -> compare a b) [ (name, constType init) | (name, Outport init) <- blocks ]+  others  = [ (name, block) | (name, block) <- blocks, not $ isPort block ]+  port :: String -> (Int, (Name, String)) -> Mdl+  port direction (port, (name, typ)) = mdlBlock direction name+    [ "Port" :- show port+    , "DataType" :- typ+    ]+  isPort :: Block -> Bool+  isPort (Inport  _) = True+  isPort (Outport _) = True+  isPort _           = False++mdlBlock :: String -> Name -> [Mdl] -> Mdl+mdlBlock blockType name fields = "Block" :=+  [ "BlockType" :- blockType+  , "Name"      :- name+  ] ++ fields++constType :: Const -> String+constType a = case a of+  Bool  _ -> "boolean"+  Int   _ -> "int32"+  Float _ -> "single"++blk :: (Name, Block) -> Mdl+blk (name, a) = case a of+  Inport  _ -> undefined+  Outport _ -> undefined+  UnitDelay init -> f "UnitDelay"          ["X0" :- showConst init, "SampleTime" :- "-1"]+  Cast t         -> f "DataTypeConversion" ["OutDataTypeMode" :- t]+  Assertion      -> f "Assertion"          ["StopWhenAssertionFail" :- "off", "SampleTime" :- "-1", "Enabled" :- "on"]+  Const' c       -> f "Constant"           ["Value" :- showConst c, "OutDataTypeMode" :- constType c]+  Add'           -> f "Sum"                ["Inputs" :- "++"]+  Sub'           -> f "Sum"                ["Inputs" :- "+-"]+  Mul'           -> f "Product"            ["Inputs" :- "**"]+  Div'           -> f "Product"            ["Inputs" :- "*/"]+  Mod'           -> f "Math"               ["Operator" :- "mod"]+  Not'           -> f "Logic"              ["Operator" :- "NOT", "Inputs" :- "1"]+  And'           -> f "Logic"              ["Operator" :- "AND", "Inputs" :- "2"]+  Or'            -> f "Logic"              ["Operator" :- "OR",  "Inputs" :- "2"]+  Eq'            -> f "RelationalOperator" ["Operator" :- "==", "LogicOutDataTypeMode" :- "boolean"]+  Lt'            -> f "RelationalOperator" ["Operator" :- "<" , "LogicOutDataTypeMode" :- "boolean"]+  Gt'            -> f "RelationalOperator" ["Operator" :- ">" , "LogicOutDataTypeMode" :- "boolean"]+  Le'            -> f "RelationalOperator" ["Operator" :- "<=", "LogicOutDataTypeMode" :- "boolean"]+  Ge'            -> f "RelationalOperator" ["Operator" :- ">=", "LogicOutDataTypeMode" :- "boolean"]+  Mux'           -> f "Switch"             ["Criteria" :- "u2 ~= 0"]+  where+  f typ args = mdlBlock typ name args 

@@ -1,7 +1,7 @@ module Language.ImProve.Core   ( E (..)   , V (..)-  , UV (..)+  , A (..)   , Name   , Path   , UID@@ -13,7 +13,7 @@   , VarInfo   , varInfo   , stmtVars-  , exprVars+  , arrayLength   , theorems   ) where @@ -27,39 +27,41 @@ type UID = Int  -- | A mutable variable.-data V a = V Bool [Name] a deriving (Eq, Ord)+data V a+  = V Bool Path a+  deriving Eq --- | An untyped variable.-data UV-  = UVBool  (V Bool)-  | UVInt   (V Int)-  | UVFloat (V Float)-  deriving (Eq, Ord)+-- | A mutable array.+data A a = A Bool Path [a] deriving (Eq, Ord) -class    PathName a         where pathName :: a -> String-instance PathName Path      where pathName = intercalate "."-instance PathName (V a)     where pathName (V _ path _) = pathName path-instance PathName VarInfo   where pathName (_, path, _) = pathName path+-- | Length of array.+arrayLength :: A a -> Int+arrayLength (A _ _ a) = length a +class    PathName a       where pathName :: a -> String+instance PathName Path    where pathName = intercalate "."+instance PathName (V a)   where+  pathName a = case a of+    V _ path _ -> pathName path+    -- VArray a _ -> pathName a+instance PathName (A a)   where pathName (A _ a _) = pathName a+instance PathName VarInfo where pathName (_, path, _) = pathName path+ class Eq a => AllE a where   zero   :: (Name -> a -> m (V a)) -> a   const' :: a -> Const-  untype :: V a -> UV  instance AllE Bool where   zero = const False   const' = Bool-  untype = UVBool  instance AllE Int where   zero = const 0   const' = Int-  untype = UVInt    instance AllE Float where   zero = const 0   const' = Float-  untype = UVFloat  class    AllE a => NumE a instance NumE Int@@ -111,25 +113,21 @@   Null     :: Statement  data Const-  = Bool  Bool-  | Int   Int-  | Float Float+  = Bool   Bool+  | Int    Int+  | Float  Float   deriving (Show, Eq, Ord)  type VarInfo = (Bool, Path, Const) -class VarInfo' a where varInfo :: a -> VarInfo-instance AllE a => VarInfo' (V a) where varInfo (V input path init) = (input, path, const' init)-instance VarInfo' UV where-  varInfo a = case a of-    UVBool a  -> varInfo a-    UVInt  a  -> varInfo a-    UVFloat a -> varInfo a+varInfo :: AllE a => V a -> VarInfo+varInfo a = case a of+  V input path init -> (input, path, const' init)  -- | Variables in a program.-stmtVars :: Statement -> [UV]+stmtVars :: Statement -> [VarInfo] stmtVars a = case a of-  Assign a b   -> nub $ untype a : exprVars b+  Assign a b   -> nub $ varInfo a : exprVars b   Branch a b c -> nub $ exprVars a ++ stmtVars b ++ stmtVars c   Sequence a b -> nub $ stmtVars a ++ stmtVars b   Theorem _ _ _ a -> exprVars a@@ -138,9 +136,9 @@   Null         -> []  -- | Variables in an expression.-exprVars :: E a -> [UV]+exprVars :: E a -> [VarInfo] exprVars a = case a of-  Ref a     -> [untype a]+  Ref a     -> [varInfo a]   Const _   -> []   Add a b   -> exprVars a ++ exprVars b   Sub a b   -> exprVars a ++ exprVars b

@@ -69,8 +69,8 @@   step :: Y ()   step = do       addTrace $ Step' 0-      sequence_ [ getVar' a >>= addTrace . State' (pathName path) | a@(input, path, _) <- sortBy f $ map varInfo $ stmtVars program, not input ]-      sequence_ [ addVar' a >>= addTrace . Input' (pathName path) | a@(input, path, _) <- sortBy f $ map varInfo $ stmtVars program,     input ]+      sequence_ [ getVar' a >>= addTrace . State' (pathName path) | a@(input, path, _) <- sortBy f $ stmtVars program, not input ]+      sequence_ [ addVar' a >>= addTrace . Input' (pathName path) | a@(input, path, _) <- sortBy f $ stmtVars program,     input ]       evalStmt theorem lemmas (LitB True) program   f (_, a, _) (_, b, _) = compare a b @@ -92,7 +92,7 @@   env <- get   r <- liftIO $ quickCheckY' yices [] $ reverse (cmds env)           ++ [ASSERT $ NOT $ AND $ asserts env]-          ++ [ ASSERT $ VarE (var env0 a) := evalConst' c | a@(input, _, c) <- map varInfo $ stmtVars program, not input ]+          ++ [ ASSERT $ VarE (var env0 a) := evalConst' c | a@(input, _, c) <- stmtVars program, not input ]           ++ [CHECK]   return $ result r @@ -234,7 +234,7 @@   }   initEnv :: Statement -> IO Env-initEnv program = execStateT (sequence_ [ addVar' a | a@(input, _, _) <- map varInfo $ stmtVars program, not input ]) Env+initEnv program = execStateT (sequence_ [ addVar' a | a@(input, _, _) <- stmtVars program, not input ]) Env   { nextId  = 0   , var     = \ v -> error $ "variable not found in environment: " ++ pathName v   , cmds    = []

@@ -1,5 +1,5 @@ name:    improve-version: 0.2.3+version: 0.3.0  category: Language, Formal Methods, Embedded @@ -9,6 +9,7 @@   ImProve is an imperative programming language for high assurance applications.   ImProve uses infinite state, unbounded model checking to verify programs adhere   to specifications.  Yices (required) is the backend SMT solver.+  ImProve compiles to C and Simulink.  author:     Tom Hawkins <tomahawkins@gmail.com> maintainer: Tom Hawkins <tomahawkins@gmail.com>