improve 0.3.2 → 0.3.3

raw patch · 11 files changed

+735/−466 lines, 11 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Language/ImProve.hs +21/−23
• Language/ImProve/Code.hs +20/−430
• Language/ImProve/Code/C.hs +100/−0
• Language/ImProve/Code/Common.hs +7/−0
• Language/ImProve/Code/Modelica.hs +154/−0
• Language/ImProve/Code/Simulink.hs +371/−0
• Language/ImProve/Core.hs +3/−3
• Language/ImProve/Examples.hs +4/−4
• Language/ImProve/Path.hs +42/−0
• Language/ImProve/Verify.hs +5/−3
• improve.cabal +8/−3

@@ -216,7 +216,10 @@   -- * Verification   , verify   -- * Code Generation+  , C.Target (..)   , code+  -- * General Analysis+  , analyze   ) where  import Control.Monad@@ -360,17 +363,8 @@ 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.+-- | Labels a statement and creates a new variable scope.+--   Labels are used in counter examples to help trace the program execution. (-|) :: Name -> Stmt a -> Stmt a name -| stmt = do   (id, path0, stmt0) <- get@@ -470,15 +464,17 @@ instance Assign Int   where a <== b = statement $ Assign a b instance Assign Float where a <== b = statement $ Assign a b --- | 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 :: 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 +-- | Assume a condition is true.+--   Assumptions are used as lemmas to other theorems.+assume :: Name -> E Bool -> Stmt Theorem+assume name a = do+  (id, path, stmt) <- get+  put (id + 1, path, Sequence stmt $ Label name $ Assume id a)+  return $ Theorem' id+ -- | Defines a new theorem. -- -- > theorem name k lemmas proposition@@ -520,13 +516,15 @@ -- -- > verify pathToYices program verify :: FilePath -> Stmt () -> IO ()-verify yices program = V.verify yices stmt-  where-  (_, _, stmt) = evalStmt 0 [] program+verify yices program = analyze (V.verify yices) program --- | Generate C and Simulink code.-code :: Name -> Stmt () -> IO ()-code name program = C.code name stmt+-- | Generate code.+code :: C.Target -> Name -> Stmt () -> IO ()+code target name program = analyze (C.code target name) program++-- | Generic program analysis.+analyze :: (Statement -> IO a) -> Stmt () -> IO a+analyze f program = f stmt   where   (_, _, stmt) = evalStmt 0 [] program 

@@ -1,436 +1,26 @@-module Language.ImProve.Code (code) where--import Control.Monad.State-import Data.List-import Data.Maybe-import Text.Printf+module Language.ImProve.Code+  ( Target (..)+  , code+  ) where +import Language.ImProve.Code.C+import Language.ImProve.Code.Modelica+import Language.ImProve.Code.Simulink import Language.ImProve.Core-import Language.ImProve.Tree hiding (Branch)-import qualified Language.ImProve.Tree as T -infixr 0 :-, :=---- | Generate C and Simulink code.-code :: Name -> Statement -> IO ()-code name stmt = do-  writeFile (name ++ ".c") $-       "/* Generated by ImProve. */\n\n"-    ++ "#include <assert.h>\n\n"-    ++ codeVariables True scope ++ "\n"-    ++ "void " ++ name ++ "()\n{\n"-    ++ indent (codeStmt name [] stmt)-    ++ "}\n\n"-  writeFile (name ++ ".h") $-       "/* Generated by ImProve. */\n\n"-    ++ codeVariables False scope ++ "\n"-    ++ "void " ++ name ++ "(void);\n\n"-  codeMdl name stmt-  where-  scope = case tree (\ (_, path, _) -> path) $ stmtVars stmt of-    [] -> error "program contains no useful statements"-    a  -> T.Branch (name ++ "_variables") a--instance Show Statement where show = codeStmt "none" []--codeStmt :: Name -> [Name] -> Statement -> String-codeStmt name path a = case a of-  Assign a b -> name ++ "_variables." ++ pathName a ++ " = " ++ codeExpr b ++ ";\n"-  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 (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--  codeExpr :: E a -> String-  codeExpr a = case a of-    Ref a     -> name ++ "_variables." ++ pathName a-    Const a   -> showConst $ const' a-    Add a b   -> group [codeExpr a, "+", codeExpr b]-    Sub a b   -> group [codeExpr a, "-", codeExpr b]-    Mul a b   -> group [codeExpr a, "*", showConst (const' b)]-    Div a b   -> group [codeExpr a, "/", showConst (const' b)]-    Mod a b   -> group [codeExpr a, "%", showConst (const' b)]-    Not a     -> group ["!", codeExpr a]-    And a b   -> group [codeExpr a, "&&",  codeExpr b]-    Or  a b   -> group [codeExpr a, "||",  codeExpr b]-    Eq  a b   -> group [codeExpr a, "==",  codeExpr b]-    Lt  a b   -> group [codeExpr a, "<",   codeExpr b]-    Gt  a b   -> group [codeExpr a, ">",   codeExpr b]-    Le  a b   -> group [codeExpr a, "<=",  codeExpr b]-    Ge  a b   -> group [codeExpr a, ">=",  codeExpr b]-    Mux a b c -> group [codeExpr a, "?", codeExpr b, ":", codeExpr c] -    where-    group :: [String] -> String-    group a = "(" ++ intercalate " " a ++ ")"--indent :: String -> String-indent = unlines . map ("\t" ++) . lines--indent' :: String -> String-indent' a = case lines a of-  [] -> []-  (a:b) -> a ++ "\n" ++ indent (unlines b)--codeVariables :: Bool -> (Tree Name (Bool, Path, Const)) -> String-codeVariables define a = (if define then "" else "extern ") ++ init (init (f1 a)) ++ (if define then " =\n    " ++ f2 a else "") ++ ";\n"-  where-  f1 a = case a of-    T.Branch name items -> "struct {  /* " ++ name ++ " */\n" ++ indent (concatMap f1 items) ++ "} " ++ name ++ ";\n"-    Leaf name (input, _, init) -> printf "%-5s %-25s;%s\n" (showConstType init) name (if input then "  /* input */" else "")--  f2 a = case a of-    T.Branch name items -> indent' $ "{   " ++ (intercalate ",   " $ map f2 items) ++ "}  /* " ++ name ++ " */\n"-    Leaf name (_, _, init) -> printf "%-15s  /* %s */\n" (showConst init) name--showConst :: Const -> String-showConst a = case a of-  Bool  True  -> "1"-  Bool  False -> "0"-  Int   a     -> show a-  Float a     -> show a--showConstType :: Const -> String-showConstType a = case a of-  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 [] []) >>= return . removeNullEffect-  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--isSrc :: Block -> Bool-isSrc a = case a of-  Outport _ -> False-  Assertion -> False-  _         -> True+-- | Code generation targets.+data Target+  = C+  | Modelica+  | Simulink+  deriving Eq -removeNullEffect :: Netlist -> Netlist-removeNullEffect net = if null unused then net else removeNullEffect net { blocks = blocks', nets = nets' }+-- | Generate target code.+code :: Target -> Name -> Statement -> IO ()+code target name stmt = f name stmt   where-  unused = [ name | (name, block) <- blocks net, isSrc block, not $ any (\ (n, _) -> name == n) $ nets net ]-  blocks' = [ (name, block) | (name, block) <- blocks net, not $ elem name unused ]-  nets' = [ (src, (dest, port)) | (src, (dest, port)) <- nets net, not $ elem dest unused ]+  f = case target of+    C        -> codeC+    Modelica -> codeModelica+    Simulink -> codeSimulink 

@@ -0,0 +1,100 @@+module Language.ImProve.Code.C (codeC) where++import Data.List+import Text.Printf++import Language.ImProve.Code.Common+import Language.ImProve.Core+import Language.ImProve.Tree hiding (Branch)+import qualified Language.ImProve.Tree as T++-- | Generate C.+codeC :: Name -> Statement -> IO ()+codeC name stmt = do+  writeFile (name ++ ".c") $+       "/* Generated by ImProve. */\n\n"+    ++ "#include <assert.h>\n\n"+    ++ codeVariables True scope ++ "\n"+    ++ "void " ++ name ++ "()\n{\n"+    ++ indent (codeStmt name [] stmt)+    ++ "}\n\n"+  writeFile (name ++ ".h") $+       "/* Generated by ImProve. */\n\n"+    ++ "#ifdef __cplusplus\n"+    ++ "extern \"C\" {\n"+    ++ "#endif\n\n"+    ++ codeVariables False scope ++ "\n"+    ++ "void " ++ name ++ "(void);\n\n"+    ++ "#ifdef __cplusplus\n"+    ++ "}\n"+    ++ "#endif\n"+  where+  scope = case tree (\ (_, path, _) -> path) $ stmtVars stmt of+    [] -> error "program contains no useful statements"+    a  -> T.Branch (name ++ "_variables") a++instance Show Statement where show = codeStmt "none" []++codeStmt :: Name -> [Name] -> Statement -> String+codeStmt name path a = case a of+  Assign a b -> name ++ "_variables." ++ pathName a ++ " = " ++ codeExpr b ++ ";\n"+  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 (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++  codeExpr :: E a -> String+  codeExpr a = case a of+    Ref a     -> name ++ "_variables." ++ pathName a+    Const a   -> showConst $ const' a+    Add a b   -> group [codeExpr a, "+", codeExpr b]+    Sub a b   -> group [codeExpr a, "-", codeExpr b]+    Mul a b   -> group [codeExpr a, "*", showConst (const' b)]+    Div a b   -> group [codeExpr a, "/", showConst (const' b)]+    Mod a b   -> group [codeExpr a, "%", showConst (const' b)]+    Not a     -> group ["!", codeExpr a]+    And a b   -> group [codeExpr a, "&&",  codeExpr b]+    Or  a b   -> group [codeExpr a, "||",  codeExpr b]+    Eq  a b   -> group [codeExpr a, "==",  codeExpr b]+    Lt  a b   -> group [codeExpr a, "<",   codeExpr b]+    Gt  a b   -> group [codeExpr a, ">",   codeExpr b]+    Le  a b   -> group [codeExpr a, "<=",  codeExpr b]+    Ge  a b   -> group [codeExpr a, ">=",  codeExpr b]+    Mux a b c -> group [codeExpr a, "?", codeExpr b, ":", codeExpr c] +    where+    group :: [String] -> String+    group a = "(" ++ intercalate " " a ++ ")"++indent' :: String -> String+indent' a = case lines a of+  [] -> []+  (a:b) -> a ++ "\n" ++ indent (unlines b)++codeVariables :: Bool -> (Tree Name (Bool, Path, Const)) -> String+codeVariables define a = (if define then "" else "extern ") ++ init (init (f1 a)) ++ (if define then " =\n\t" ++ f2 a else "") ++ ";\n"+  where+  f1 a = case a of+    T.Branch name items -> "struct {  /* " ++ name ++ " */\n" ++ indent (concatMap f1 items) ++ "} " ++ name ++ ";\n"+    Leaf name (input, _, init) -> printf "%-5s %-25s;%s\n" (showConstType init) name (if input then "  /* input */" else "")++  f2 a = case a of+    T.Branch name items -> indent' $ "{   " ++ (intercalate ",   " $ map f2 items) ++ "}  /* " ++ name ++ " */\n"+    Leaf name (_, _, init) -> printf "%-15s  /* %s */\n" (showConst init) name++showConst :: Const -> String+showConst a = case a of+  Bool  True  -> "1"+  Bool  False -> "0"+  Int   a     -> show a+  Float a     -> show a++showConstType :: Const -> String+showConstType a = case a of+  Bool  _ -> "int"+  Int   _ -> "int"+  Float _ -> "float"+

@@ -0,0 +1,7 @@+module Language.ImProve.Code.Common+  ( indent+  ) where++indent :: String -> String+indent = unlines . map ("\t" ++) . lines+

@@ -0,0 +1,154 @@+module Language.ImProve.Code.Modelica (codeModelica) where++import Data.Function+import Data.List+import Data.Maybe+import Text.Printf++import Language.ImProve.Code.Simulink+import Language.ImProve.Core++-- Modelica generation.+codeModelica :: Name -> Statement -> IO ()+codeModelica name stmt = do+  net <- netlist stmt >>= return . moRename+  writeFile (name ++ ".mo") $ unlines $+    [ "// Generated by ImProve."+    , ""+    , "block " ++ name+    , "\tparameter Real Period=0.001;"+    ] +++    inputs net +++    outputs net +++    [ "protected" ] +++    states net +++    internals net +++    [ "equation"+    , "\twhen sample(0, Period) then"+    ] +++    equations net +++    [ "\tend when;"+    , "end " ++ name ++ ";"+    ]+  where+  inputs    net = [ printf "\tinput %s %s;"                 (constType a) name               | (name, Inport a)    <- sortedBlocks net ]+  outputs   net = [ printf "\tdiscrete output %s %s;"       (constType a) name               | (name, Outport a)   <- sortedBlocks net ]+  states    net = [ printf "\tdiscrete %s %s (start = %s);" (constType a) name (showConst a) | (name, UnitDelay a) <- sortedBlocks net ]+  internals net = [ printf "\tdiscrete %s %s;"           (constType $ netType net name) name | (name, block) <- sortedBlocks net, isInternal block ]+  equations net = mapMaybe (equation net) $ blocks net+  sortedBlocks net = sortBy (compare `on` fst) $ blocks net++equation :: Netlist -> (Name, Block) -> Maybe String+equation net (name, block) = case block of+  Inport  _      -> Nothing+  Outport _      -> f $ arg 0+  UnitDelay _    -> f $ arg 0+  Cast _         -> f $ printf "pre(%s)" $ arg 0+  Assertion      -> Just $ printf "\tassert(%s, \"%s\");" (arg 0) name+  Const' c       -> f $ showConst c+  Add'           -> f $ printf "%s + %s" (arg 0) (arg 1)+  Sub'           -> f $ printf "%s - %s" (arg 0) (arg 1)+  Mul'           -> f $ printf "%s * %s" (arg 0) (arg 1)+  Div'           -> case netType net name of+		      Bool  _ -> error "Modelica.equation: invalid netlist (1)"+                      Int   _ -> f $ printf "div(%s, %s)" (arg 0) (arg 1)+		      Float _ -> f $ printf "%s / %s"     (arg 0) (arg 1)+  Mod'           -> f $ printf "mod(%s, %s)" (arg 0) (arg 1)+  Not'           -> f $ printf "not %s" $ arg 0+  And'           -> f $ printf "%s and %s" (arg 0) (arg 1)+  Or'            -> f $ printf "%s or %s" (arg 0) (arg 1)+  Eq'            -> f $ printf "%s == %s" (arg 0) (arg 1)+  Lt'            -> f $ printf "%s < %s" (arg 0) (arg 1)+  Gt'            -> f $ printf "%s > %s" (arg 0) (arg 1)+  Le'            -> f $ printf "%s <= %s" (arg 0) (arg 1)+  Ge'            -> f $ printf "%s >= %s" (arg 0) (arg 1)+  Mux'           -> f $ printf "if %s then %s else %s" (arg 0) (arg 1) (arg 2)+  where+  f :: String -> Maybe String+  f a = Just $ printf "\t%s = %s;" name a+  arg i = case [ n | (n, (n1, p1)) <- nets net, n1 == name, p1 == i ] of+    [n] -> n+    _ -> error "Modelica.equation: invalid netlist (2)"++isInternal :: Block -> Bool+isInternal a = case a of+  Inport    _ -> False+  Outport   _ -> False+  UnitDelay _ -> False+  Assertion   -> False+  _           -> True++moRename :: Netlist -> Netlist+moRename net = net { env = map f $ env net, blocks = [ (f n, b) | (n, b) <- blocks net ], nets = [ (f a, (f b, i)) | (a, (b, i)) <- nets net ] }+  where+  f n = "`" ++ n ++ "`"++showConst :: Const -> String+showConst a = case a of+  Bool  True  -> "true"+  Bool  False -> "false"+  Int   a     -> show a+  Float a     -> show a++constType :: Const -> String+constType a = case a of+  Bool  _ -> "Boolean"+  Int   _ -> "Integer"+  Float _ -> "Real   "++netType :: Netlist -> Name -> Const+netType net name = case fromJust $ lookup name $ blocks net of+  Inport    a -> a+  UnitDelay a -> a+  Const'    a -> a+  Outport _ -> error "Modelica.netType: not expecting Outport"+  Assertion -> error "Modelica.netType: not expecting Assertion"+  Mod' -> Int 0+  Not' -> Bool False+  And' -> Bool False+  Or'  -> Bool False+  Eq'  -> Bool False+  Lt'  -> Bool False+  Gt'  -> Bool False+  Le'  -> Bool False+  Ge'  -> Bool False+  Mux' -> follow 1+  _    -> follow 0+  where+  follow :: Int -> Const+  follow p = case [ n | (n, (n1, p1)) <- nets net, n1 == name, p1 == p ] of+    [n] -> netType net n+    _   -> error "Modelica.netType: invalid netlist"++{-+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))]+  }+-}

@@ -0,0 +1,371 @@+module Language.ImProve.Code.Simulink+  ( codeSimulink+  , Netlist (..)+  , Block   (..)+  , netlist+  ) where++import Control.Monad.State+import Data.List+import Data.Maybe++import Language.ImProve.Code.Common+import Language.ImProve.Core++infixr 0 :-, :=++showConst :: Const -> String+showConst a = case a of+  Bool  True  -> "1"+  Bool  False -> "0"+  Int   a     -> show a+  Float a     -> show a++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.+codeSimulink :: Name -> Statement -> IO ()+codeSimulink name stmt = do+  net <- netlist stmt+  writeFile (name ++ ".mdl") $ show $ mdl name $ (mdlBlocks $ blocks net) ++ (mdlLines $ nets net)++-- | Builds a netlist.+netlist :: Statement -> IO Netlist+netlist stmt' = execStateT all (Netlist 0 [] paths env [] []) >>= return . removeNullEffect+  where+  stmt = lowerConditionals (Const True) stmt'+  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+    evalStmt 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)++-- Pushes conditionals down to theorems and assumptions.+lowerConditionals :: E Bool -> Statement -> Statement+lowerConditionals cond a = case a of+  Assign   a b     -> Assign a b+  Branch   a b c   -> Branch a (lowerConditionals (And cond a) b) (lowerConditionals (And cond $ Not a) c)+  Sequence a b     -> Sequence (lowerConditionals cond a) (lowerConditionals cond b)+  Theorem  a b c d -> Theorem a b c $ Or (Not cond) d+  Assume   i a     -> Assume i $ Or (Not cond) a+  Label    a b     -> Label a $ lowerConditionals cond b+  Null             -> Null++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.+evalStmt :: Statement -> Net ()+evalStmt 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++    evalStmt b+    net1 <- get+    modify $ \ net -> net { env = env net0 }++    evalStmt 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    -> evalStmt a >> evalStmt 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] }+    evalStmt 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"++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++isSrc :: Block -> Bool+isSrc a = case a of+  Outport _ -> False+  Assertion -> False+  _         -> True++removeNullEffect :: Netlist -> Netlist+removeNullEffect net = if null unused then net else removeNullEffect net { blocks = blocks', nets = nets' }+  where+  unused = [ name | (name, block) <- blocks net, isSrc block, not $ any (\ (n, _) -> name == n) $ nets net ]+  blocks' = [ (name, block) | (name, block) <- blocks net, not $ elem name unused ]+  nets' = [ (src, (dest, port)) | (src, (dest, port)) <- nets net, not $ elem dest unused ]+

@@ -108,7 +108,7 @@   Branch   :: E Bool -> Statement -> Statement -> Statement   Sequence :: Statement -> Statement -> Statement   Theorem  :: Int -> Int -> [Int] -> E Bool -> Statement -- Theorem id k lemmas expr-  Assume   :: E Bool -> Statement+  Assume   :: Int -> E Bool -> Statement                 -- Assume id expr   Label    :: Name -> Statement -> Statement   Null     :: Statement @@ -131,7 +131,7 @@   Branch a b c -> nub $ exprVars a ++ stmtVars b ++ stmtVars c   Sequence a b -> nub $ stmtVars a ++ stmtVars b   Theorem _ _ _ a -> exprVars a-  Assume a     -> exprVars a+  Assume  _ a     -> exprVars a   Label  _ a   -> stmtVars a   Null         -> [] @@ -162,7 +162,7 @@   Assign _ _   -> []   Branch _ a b -> theorems a ++ theorems b   Sequence a b -> theorems a ++ theorems b-  Assume _     -> []+  Assume _ _   -> []   Label  _ a   -> theorems a   Null         -> [] 

@@ -60,7 +60,7 @@  -- | Build the gcdMain code (i.e. gcd.c, gcd.h). buildGCD :: IO ()-buildGCD = code "gcd" gcdMain+buildGCD = code C "gcd" gcdMain   @@ -176,13 +176,13 @@ buildArbiters :: IO () buildArbiters = do   putStrLn "\nBuilding arbiter1 (arbiter1.c/h) ..."-  code "arbiter1" $ arbiter "arbiter1" arbiter1+  code C "arbiter1" $ arbiter "arbiter1" arbiter1    putStrLn "\nBuilding arbiter2 (arbiter2.c/h) ..."-  code "arbiter2" $ arbiter "arbiter2" arbiter2+  code C "arbiter2" $ arbiter "arbiter2" arbiter2    putStrLn "\nBuilding arbiter3 (arbiter3.c/h) ..."-  code "arbiter3" $ arbiter "arbiter3" arbiter3+  code C "arbiter3" $ arbiter "arbiter3" arbiter3  -- | Run all examples. runAll :: IO ()

@@ -0,0 +1,42 @@+module Language.ImProve.Path+  ( totalPaths+  ) where++import Language.ImProve.Core++totalPaths :: Name -> Statement -> IO ()+totalPaths name stmt = do+  putStrLn $ "total paths: " ++ show (paths stmt)+  writeFile (name ++ ".dot") (dot stmt)++paths :: Statement -> Integer+paths a = case a of+  Assign _ _      -> 1+  Branch _ a b    -> paths a + paths b+  Sequence a b    -> paths a * paths b+  Theorem _ _ _ _ -> 1+  Assume  _ _     -> 1+  Label  _ a      -> paths a+  Null            -> 1++dot :: Statement -> String+dot stmt = unlines $ ["digraph {"] ++ links ++ ["}"]+  where+  (_, _, links) = d 0 1 stmt++d :: Int -> Int -> Statement -> (Int, Int, [String])+d src id a = case a of+  Branch _ a b -> (id2, id2 + 1, link src id ++ a' ++ b' ++ link srcA id2 ++ link srcB id2)+    where+    (srcA, id1, a') = d id (id + 1)  a+    (srcB, id2, b') = d id  id1      b+  Sequence a b -> (srcB, id2, a' ++ b')+    where+    (srcA, id1, a') = d src id  a+    (srcB, id2, b') = d srcA id1 b+  Label  _ a -> d src id a+  _ -> (src, id, [])+  where+  link :: Int -> Int -> [String]+  link a b = ["  " ++ show a ++ " -> " ++ show b]+

@@ -122,9 +122,11 @@       put env { asserts = VarE b : asserts env }       addTrace $ Assert' b     | otherwise -> return ()-  Assume a -> do-    a <- evalExpr a-    addCmd $ ASSERT (enabled :=> a)+  Assume id a+    | elem id lemmas -> do+      a <- evalExpr a+      addCmd $ ASSERT (enabled :=> a)+    | otherwise -> return ()   Branch a onTrue onFalse -> do     a <- evalExpr a     b <- newBoolVar

@@ -1,5 +1,5 @@ name:    improve-version: 0.3.2+version: 0.3.3  category: Language, Formal Methods, Embedded @@ -9,7 +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.+  ImProve compiles to C, Simulink, and Modelica.  author:     Tom Hawkins <tomahawkins@gmail.com> maintainer: Tom Hawkins <tomahawkins@gmail.com>@@ -17,7 +17,7 @@ license:      BSD3 license-file: LICENSE -homepage: http://tomahawkins.org+homepage: http://github.com/tomahawkins/improve/wiki/ImProve  build-type:    Simple cabal-version: >= 1.6@@ -31,8 +31,13 @@     exposed-modules:         Language.ImProve         Language.ImProve.Code+        Language.ImProve.Code.C+        Language.ImProve.Code.Common+        Language.ImProve.Code.Modelica+        Language.ImProve.Code.Simulink         Language.ImProve.Core         Language.ImProve.Examples+        Language.ImProve.Path         Language.ImProve.Tree         Language.ImProve.Verify