improve 0.3.3 → 0.3.4

raw patch · 6 files changed

+166/−213 lines, 6 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Language/ImProve.hs +14/−6
• Language/ImProve/Code.hs +4/−1
• Language/ImProve/Code/Ada.hs +140/−0
• Language/ImProve/Core.hs +4/−4
• Language/ImProve/Examples.hs +0/−198
• improve.cabal +4/−4

@@ -154,6 +154,7 @@   , true   , false   , constant+  , zero   -- ** Variable Reference   , ref   -- ** Logical Operations@@ -192,6 +193,8 @@   -- ** Variable Hierarchical Scope and Statement Labeling    , (-|)   -- ** Variable Declarations+  , var+  , var'   , bool   , bool'   , int@@ -386,14 +389,22 @@   (_, path, _) <- get   return path +-- | Generic variable declaration. var :: AllE a => Name -> a -> Stmt (V a) var name init = do   path <- getPath   return $ V False (path ++ [name]) init +-- | Generic variable declaration and immediate assignment.+var' :: AllE a => Name -> E a -> Stmt (E a)+var' name value = do+  a <- var name zero+  a <== value+  return $ ref a+ -- | Input variable declaration.  Input variables are initialized to 0. input  :: AllE a => (Name -> a -> Stmt (V a)) -> Path -> E a-input f path = ref $ V True path $ zero f+input _ path = ref $ V True path zero  -- | Global variable declaration. global  :: AllE a => (Name -> a -> Stmt (V a)) -> Path -> a -> V a@@ -458,11 +469,8 @@ evalStmt :: Int -> [Name] -> Stmt () -> (Int, [Name], Statement) evalStmt id path (Stmt f) = snd $ f (id, path, Null) -class Assign a where-  (<==) :: V a -> E a -> Stmt ()-instance Assign Bool  where a <== b = statement $ Assign a b-instance Assign Int   where a <== b = statement $ Assign a b-instance Assign Float where a <== b = statement $ Assign a b+class Assign a where (<==) :: V a -> E a -> Stmt ()+instance AllE a => Assign a where a <== b = statement $ Assign a b  -- | Theorem to be proven or used as lemmas to assist proofs of other theorems. data Theorem = Theorem' Int

@@ -3,6 +3,7 @@   , code   ) where +import Language.ImProve.Code.Ada import Language.ImProve.Code.C import Language.ImProve.Code.Modelica import Language.ImProve.Code.Simulink@@ -10,7 +11,8 @@  -- | Code generation targets. data Target-  = C+  = Ada+  | C   | Modelica   | Simulink   deriving Eq@@ -20,6 +22,7 @@ code target name stmt = f name stmt   where   f = case target of+    Ada      -> codeAda     C        -> codeC     Modelica -> codeModelica     Simulink -> codeSimulink

@@ -0,0 +1,140 @@+module Language.ImProve.Code.Ada (codeAda) where++import Control.Monad.State+import Data.List+import Text.Printf++import Language.ImProve.Core+import Language.ImProve.Tree hiding (Branch)+import qualified Language.ImProve.Tree as T++-- | Generate Ada.+codeAda :: Name -> Statement -> IO ()+codeAda name stmt = do+  writeFile (name ++ ".ads") $ unlines+    [ "-- Generated by ImProve."+    , ""+    , "package " ++ name ++ " is"+    , ""+    , indent $ unlines+       [ codeVariables name scope+       , name ++ "_Variables : " ++ name ++ "_Record0;"+       , ""+       , "procedure " ++ name ++ ";"+       ]+    , "end " ++ name ++ ";"+    , ""+    ]+  writeFile (name ++ ".adb") $ unlines+    [ "-- Generated by ImProve."+    , ""+    , "with Ada.Assertions;"+    , ""+    , "package body " ++ name ++ " is"+    , ""+    , indent $ unlines+       [ "procedure " ++ name ++ " is"+       , "   use Ada.Assertions;"+       , "begin"+       , indent $ codeStmt name [] stmt+       , "end " ++ name ++ ";"+       , ""+       ]+    , "end " ++ name ++ ";"+    , ""+    ]+  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 ++ " then\n" ++ indent (codeStmt name path b) ++ "end if;\n"+  Branch a b c    -> "if " ++ codeExpr a ++ " then\n" ++ indent (codeStmt name path b) ++ "\nelse\n" ++ indent (codeStmt name path c) ++ "end if;\n"+  Sequence a b -> codeStmt name path a ++ codeStmt name path b+  Theorem _ _ _ a -> "Assert(" ++ codeExpr a ++ ", " ++ show (pathName path) ++ ");\n"+  Assume _ a      -> "Assert(" ++ codeExpr a ++ ", " ++ show (pathName path) ++ ");\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, "mod", showConst (const' b)]+    Not a     -> group ["not", codeExpr a]+    And a b   -> group [codeExpr a, "and",  codeExpr b]+    Or  a b   -> group [codeExpr a, "or",  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 ["if", codeExpr a, "then", codeExpr b, "else", codeExpr c] +    where+    group :: [String] -> String+    group a = "(" ++ intercalate " " a ++ ")"++indent :: String -> String+indent = unlines . map ("   " ++) . lines++type Rec = State (Int, String)++codeVariables :: Name -> Tree Name (Bool, Path, Const) -> String+codeVariables name a = indent s+  where+  (_, s) = execState (typ a) (0, "")+  typ :: Tree Name (Bool, Path, Const) -> Rec String+  typ a = case a of+    T.Branch _ items -> do+      i <- nextId+      fields <- mapM field items+      let typeName = printf "%s_Record%d" name i+      appendCode $ unlines+        [ printf "type %s is" typeName+        , indent $ unlines+          [ "record"+          , indent $ unlines $ fields+          , "end record;"+          ]+        ]+      return typeName+    Leaf _ (_, _, init) -> return $ printf "%s := %s" (showConstType init) (showConst init)++  field :: Tree Name (Bool, Path, Const) -> Rec String+  field a = do+    t <- typ a+    case a of+      T.Branch name _         -> return $ printf "%-30s : %s;"   name t+      Leaf name (input, _, _) -> return $ printf "%-30s : %s;%s" name t (if input then "  -- input" else "")++  nextId :: Rec Int+  nextId = do+    (i, s) <- get+    put (i + 1, s)+    return i+  +  appendCode :: String -> Rec ()+  appendCode s = modify $ \ (i, s') -> (i, s' ++ s)++showConst :: Const -> String+showConst a = case a of+  Bool  a  -> show a+  Int   a  -> show a+  Float a  -> show a++showConstType :: Const -> String+showConstType a = case a of+  Bool  _ -> "Boolean"+  Int   _ -> "Integer range -2147483648 .. 2147483647"+  Float _ -> "Float"+

@@ -48,19 +48,19 @@ instance PathName VarInfo where pathName (_, path, _) = pathName path  class Eq a => AllE a where-  zero   :: (Name -> a -> m (V a)) -> a+  zero   :: a   const' :: a -> Const  instance AllE Bool where-  zero = const False+  zero = False   const' = Bool  instance AllE Int where-  zero = const 0+  zero = 0   const' = Int    instance AllE Float where-  zero = const 0+  zero = 0   const' = Float  class    AllE a => NumE a

@@ -1,198 +0,0 @@--- | ImProve examples.-module Language.ImProve.Examples-  ( buildGCD-  , counter-  , verifyCounter-  , arbiterSpec-  , arbiter-  , arbiter1-  , arbiter2-  , arbiter3-  , verifyArbiters-  , buildArbiters-  , runAll-  ) where--import Language.ImProve---- | Computes the greatest common divison of two integers.---   Returns true if the computation is done, and the result.-gcd' :: E Int -> E Int -> Stmt (E Bool, E Int)-gcd' a b = do-  a0 <- int "a0" 0  -- Copy of input 'a'.-  b0 <- int "b0" 0  -- Copy of input 'b'.-  a1 <- int "a1" 0  -- Working copy of 'a'.-  b1 <- int "b1" 0  -- Working copy of 'b'.--  -- A new input to process.-  "startNew" -| if_ (a /=. ref a0 ||. b /=. ref b0) $ do-    a0 <== a-    b0 <== b-    a1 <== a-    b1 <== b--  -- Reduce a1.-  "reduceA" -| if_ (ref a1 >. ref b1) $ do-    a1 <== ref a1 - ref b1--  -- Reduce b1.-  "reduceB" -| if_ (ref b1 >. ref a1) $ do-    b1 <== ref b1 - ref a1--  -- Done if a1 == b1.-  return (ref a1 ==. ref b1, ref a1)----- | A top level wrapper for gcd'.-gcdMain :: Stmt ()-gcdMain = do-  let a = input int ["a"]  -- Input variable 'a'.-      b = input int ["b"]  -- Input variable 'b'.-  done   <- bool "done"   False  -- Variable signalling completion.-  result <- int  "result" 0      -- Result of GCD.--  -- Call gcd' in its own scope.  (Scopes prevent variable name collisions.)-  (done', result') <- "gcd" -| gcd' a b--  -- Bind the results to the output variables.-  done   <== done'-  result <== result'---- | Build the gcdMain code (i.e. gcd.c, gcd.h).-buildGCD :: IO ()-buildGCD = code C "gcd" gcdMain------ | A rolling counter verification example.-counter :: Stmt ()-counter = do-  -- The counter variable.-  counter <- int "counter" 0--  -- Specification.-  theorem "GreaterThanOrEqualTo0" 1 [] $ ref counter >=. 0-  theorem "LessThan10"            1 [] $ ref counter <=. 9--  -- Implementation.-  ifelse (ref counter ==. 9) (counter <== 0) (counter <== ref counter + 1)---- | Verify the 'counter' example.-verifyCounter :: IO ()-verifyCounter = verify "yices" counter------ | Arbiter specification.-arbiterSpec :: (E Bool, E Bool, E Bool) -> (E Bool, E Bool, E Bool) -> Stmt ()-arbiterSpec (requestA, requestB, requestC) (grantA, grantB, grantC) = do--  -- Mutual exclusion.  At most, only one requester granted at a time.-  theorem "OneHot" 1 [] $      grantA &&. not_ grantB &&. not_ grantC-                      ||. not_ grantA &&.      grantB &&. not_ grantC-                      ||. not_ grantA &&. not_ grantB &&.      grantC-                      ||. not_ grantA &&. not_ grantB &&. not_ grantC-  -  -- No grants without requests.-  theorem "NotRequestedA" 1 [] $ not_ requestA --> not_ grantA-  theorem "NotRequestedB" 1 [] $ not_ requestB --> not_ grantB-  theorem "NotRequestedC" 1 [] $ not_ requestC --> not_ grantC--  -- Grants to single requests.-  theorem "OnlyRequestA" 1 [] $ (     requestA &&. not_ requestB &&. not_ requestC) --> grantA-  theorem "OnlyRequestB" 1 [] $ (not_ requestA &&.      requestB &&. not_ requestC) --> grantB-  theorem "OnlyRequestC" 1 [] $ (not_ requestA &&. not_ requestB &&.      requestC) --> grantC--  -- Priority.-  theorem "Highest" 1 [] $ requestA --> grantA-  theorem "Medium"  1 [] $ (not_ requestA &&. requestB) --> grantB-  theorem "Lowest"  1 [] $ (not_ requestA &&. not_ requestB &&. requestC) --> grantC--  return ()---- | An arbiter implementation.-arbiter1 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)-arbiter1 (requestA, requestB, requestC) = do-  let grantA = requestA-      grantB = requestB-      grantC = requestC-  return (grantA, grantB, grantC)---- | An another arbiter implementation.-arbiter2 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)-arbiter2 (requestA, requestB, requestC) = do-  grantA <- bool "grantA" False-  grantB <- bool "grantB" False-  grantC <- bool "grantC" False--  "GrantA" -| if_ (requestA)                                     (grantA <== true)-  "GrantB" -| if_ (not_ requestA &&. requestB)                   (grantB <== true)-  "GrantC" -| if_ (not_ requestA &&. not_ requestB &&. requestC) (grantC <== true)--  return (ref grantA, ref grantB, ref grantC)---- | Yet another arbiter implementation.-arbiter3 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)-arbiter3 (requestA, requestB, requestC) = do-  let grantA = requestA-      grantB = not_ requestA &&. requestB-      grantC = not_ requestA &&. not_ requestB &&. requestC-  return (grantA, grantB, grantC)---- | Binding an arbiter implemenation to the arbiter specification.-arbiter :: Name -> ((E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)) -> Stmt ()-arbiter name implementation = name -| do-  -- Create input variables.-  let requestA = input bool ["requestA"]-      requestB = input bool ["requestB"]-      requestC = input bool ["requestC"]-  let requests = (requestA, requestB, requestC)--  -- Instantiate implementation.-  grants@(grantA, grantB, grantC) <- "impl" -| implementation requests--  -- Bind specification.-  arbiterSpec requests grants--  -- Create output variables.-  bool' "grantA" grantA-  bool' "grantB" grantB-  bool' "grantC" grantC-  return ()---- | Verify the different arbiter implementations.-verifyArbiters :: IO ()-verifyArbiters = do-  putStrLn "\nVerifying arbiter1 ..."-  verify "yices" $ arbiter "arbiter1" arbiter1--  putStrLn "\nVerifying arbiter2 ..."-  verify "yices" $ arbiter "arbiter2" arbiter2--  putStrLn "\nVerifying arbiter2 ..."-  verify "yices" $ arbiter "arbiter3" arbiter3---- | Build the different arbiter implementations.-buildArbiters :: IO ()-buildArbiters = do-  putStrLn "\nBuilding arbiter1 (arbiter1.c/h) ..."-  code C "arbiter1" $ arbiter "arbiter1" arbiter1--  putStrLn "\nBuilding arbiter2 (arbiter2.c/h) ..."-  code C "arbiter2" $ arbiter "arbiter2" arbiter2--  putStrLn "\nBuilding arbiter3 (arbiter3.c/h) ..."-  code C "arbiter3" $ arbiter "arbiter3" arbiter3---- | Run all examples.-runAll :: IO ()-runAll = do-  putStrLn "\nBuilding GCD (gcd.c, gcd.h) ..."-  buildGCD-  putStrLn "\nVerifying counter ..."-  verifyCounter-  putStrLn "\nVerifying arbiters ..."-  verifyArbiters-  putStrLn "\nBuilding arbiters ..."-  buildArbiters-

@@ -1,5 +1,5 @@ name:    improve-version: 0.3.3+version: 0.3.4  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, Simulink, and Modelica.+  ImProve compiles to C, Ada, Simulink, and Modelica.  author:     Tom Hawkins <tomahawkins@gmail.com> maintainer: Tom Hawkins <tomahawkins@gmail.com>@@ -31,17 +31,17 @@     exposed-modules:         Language.ImProve         Language.ImProve.Code+        Language.ImProve.Code.Ada         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 -    extensions: GADTs, FlexibleInstances, TypeSynonymInstances+    extensions: GADTs, FlexibleInstances, TypeSynonymInstances, UndecidableInstances      ghc-options: -W