improve 0.1.5 → 0.1.6

raw patch · 6 files changed

+120/−100 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 +4/−4
• Language/ImProve/Code.hs +17/−16
• Language/ImProve/Core.hs +41/−28
• Language/ImProve/Narrow.hs +35/−18
• Language/ImProve/Verify.hs +22/−33
• improve.cabal +1/−1

@@ -456,9 +456,9 @@  class Assign a where   (<==) :: V a -> E a -> Stmt ()-instance Assign Bool  where a <== b = statement $ AssignBool  a b-instance Assign Int   where a <== b = statement $ AssignInt   a b-instance Assign Float where a <== b = statement $ AssignFloat a b+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  -- | Assert that a condition is true. assert :: E Bool -> Stmt ()@@ -497,7 +497,7 @@  -- | Verify a program. ----- ^ verify pathToYices maxK program+-- > verify pathToYices maxK program verify :: FilePath -> Int -> Stmt () -> IO () verify yices maxK program = V.verify yices maxK $ snd $ evalStmt [] program 

@@ -15,30 +15,31 @@     ++ "#include <assert.h>\n\n"     ++ codeVariables True scope ++ "\n"     ++ "void " ++ name ++ "()\n{\n"-    ++ indent (codeStmt [] stmt)+    ++ indent (codeStmt name [] stmt)     ++ "}\n\n"   writeFile (name ++ ".h") $        "/* Generated by ImProve. */\n\n"     ++ codeVariables False scope ++ "\n"     ++ "void " ++ name ++ "(void);\n\n"   where-  scope = case tree (\ (_, path, _) -> path) $ stmtVars stmt of-    [] -> error "program contains no usefull statements"+  scope = case tree (\ (_, path, _) -> path) $ map varInfo $ stmtVars stmt of+    [] -> error "program contains no useful statements"     a  -> T.Branch (name ++ "_variables") a -  codeStmt :: [Name] -> Statement -> String-  codeStmt path a = case a of-    AssignBool  a b -> name ++ "_variables." ++ pathName a ++ " = " ++ codeExpr b ++ ";\n"-    AssignInt   a b -> name ++ "_variables." ++ pathName a ++ " = " ++ codeExpr b ++ ";\n"-    AssignFloat a b -> name ++ "_variables." ++ pathName a ++ " = " ++ codeExpr b ++ ";\n"-    Branch a b Null -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt path b) ++ "}\n"-    Branch a b c    -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt path b) ++ "}\nelse {\n" ++ indent (codeStmt path c) ++ "}\n"-    Sequence a b -> codeStmt path a ++ codeStmt path b-    Assert a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n"-    Assume a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n"-    Label  name a -> "/*" ++ name ++ "*/\n" ++ indent (codeStmt (path ++ [name]) a)-    Null -> ""-  +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+  Assert a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n"+  Assume a -> "assert((" ++ show (intercalate "." 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

@@ -1,6 +1,7 @@ module Language.ImProve.Core   ( E (..)   , V (..)+  , UV (..)   , Name   , Path   , PathName (..)@@ -22,28 +23,39 @@ type Path = [Name]  -- | A mutable variable.-data V a = V Bool [Name] a deriving Eq+data V a = V Bool [Name] a deriving (Eq, Ord) +-- | An untyped variable.+data UV+  = UVBool  (V Bool)+  | UVInt   (V Int)+  | UVFloat (V Float)+  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 -class AllE a where+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@@ -85,16 +97,14 @@   recip a = 1 / a   fromRational r = Const $ fromInteger (numerator r) / fromInteger (denominator r) -data Statement-  = AssignBool  (V Bool ) (E Bool )-  | AssignInt   (V Int  ) (E Int  )-  | AssignFloat (V Float) (E Float)-  | Branch      (E Bool) Statement Statement-  | Sequence    Statement Statement-  | Assert      (E Bool)-  | Assume      (E Bool)-  | Label       Name Statement-  | Null+data Statement where+  Assign   :: AllE a => V a -> E a -> Statement+  Branch   :: E Bool -> Statement -> Statement -> Statement+  Sequence :: Statement -> Statement -> Statement+  Assert   :: E Bool -> Statement+  Assume   :: E Bool -> Statement+  Label    :: Name -> Statement -> Statement+  Null     :: Statement  data Const   = Bool  Bool@@ -104,26 +114,29 @@  type VarInfo = (Bool, Path, Const) -varInfo :: AllE a => V a -> VarInfo-varInfo (V input path init) = (input, path, const' init)+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 --- Information about all of a program's variables.-stmtVars :: Statement -> [VarInfo]+-- Variables in a program.+stmtVars :: Statement -> [UV] stmtVars a = case a of-  AssignBool  a b -> nub $ varInfo a : exprVars b-  AssignInt   a b -> nub $ varInfo a : exprVars b-  AssignFloat 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-  Assert a        -> exprVars a-  Assume a        -> exprVars a-  Label  _ a      -> stmtVars a-  Null            -> []+  Assign a b   -> nub $ untype a : exprVars b+  Branch a b c -> nub $ exprVars a ++ stmtVars b ++ stmtVars c+  Sequence a b -> nub $ stmtVars a ++ stmtVars b+  Assert a     -> exprVars a+  Assume a     -> exprVars a+  Label  _ a   -> stmtVars a+  Null         -> [] --- Information about all of an expressions's variables.-exprVars :: E a -> [VarInfo]+-- Variables in an expression.+exprVars :: E a -> [UV] exprVars a = case a of-  Ref a     -> [varInfo a]+  Ref a     -> [untype a]   Const _   -> []   Add a b   -> exprVars a ++ exprVars b   Sub a b   -> exprVars a ++ exprVars b

@@ -11,40 +11,38 @@   assumes = foldl Sequence Null [ Label lab $ Assume assume | (lab, opt) <- optimizations, assume <- opt stmt ]   optimizations =     [ ("constantAssigns", constantAssigns)+    , ("timerRanges",     timerRanges)     ]  constantAssigns :: Statement -> [E Bool] constantAssigns stmt = mapMaybe f1 $ stmtVars stmt   where-  f1 :: VarInfo -> Maybe (E Bool)-  f1 info@(input, path, init)+  f1 :: UV -> Maybe (E Bool)+  f1 uv     | input = Nothing     | otherwise = do-      assigns <- lastConstAssign info stmt+      assigns <- lastConstAssign uv stmt       case (init, nub $ init : assigns) of         (Bool _, [_, _]) -> Nothing 	(_, a) -> return $ foldl1 Or $ map f2 a-      where-      f2 :: Const -> E Bool-      f2 assign = case (init, assign) of-        (Bool  a, Bool  b) -> Eq (Ref (V input path a)) (Const b)-        (Int   a, Int   b) -> Eq (Ref (V input path a)) (Const b)-        (Float a, Float b) -> Eq (Ref (V input path a)) (Const b)-        _ -> undefined+    where+    f2 :: Const -> E Bool+    f2 assign = case (init, assign) of+      (Bool  a, Bool  b) -> Eq (Ref (V input path a)) (Const b)+      (Int   a, Int   b) -> Eq (Ref (V input path a)) (Const b)+      (Float a, Float b) -> Eq (Ref (V input path a)) (Const b)+      _ -> undefined+    (input, path, init) = varInfo uv -lastConstAssign :: VarInfo -> Statement -> Maybe [Const]-lastConstAssign info a = do+lastConstAssign :: UV -> Statement -> Maybe [Const]+lastConstAssign uv a = do   (_, a) <- lastConstAssign a   return $ nub a   where   lastConstAssign :: Statement -> Maybe (Bool, [Const])   lastConstAssign a = case a of-    AssignBool  v (Const a) | varInfo v == info -> Just (True, [const' a])-    AssignInt   v (Const a) | varInfo v == info -> Just (True, [const' a])-    AssignFloat v (Const a) | varInfo v == info -> Just (True, [const' a])-    AssignBool  v _ | varInfo v == info -> Nothing-    AssignInt   v _ | varInfo v == info -> Nothing-    AssignFloat v _ | varInfo v == info -> Nothing+    Assign v (Const a) | untype v == uv -> Just (True, [const' a])+    Assign v _         | untype v == uv -> Nothing     Branch _ a b -> do       (aDone, a) <- lastConstAssign a       (bDone, b) <- lastConstAssign b@@ -58,4 +56,23 @@           return (aDone, a ++ b)     Label  _ a -> lastConstAssign a     _ -> Just (False, [])++timerRanges :: Statement -> [E Bool]+timerRanges stmt = [] --XXX+  where+  intCode :: [(VarInfo, Statement)]+  intCode = [ (varInfo a, assignedVar a stmt) | a@(UVInt _) <- stmtVars stmt ]++-- | Reduces a program only to assignments of a certain variable.+assignedVar :: UV -> Statement -> Statement+assignedVar v a = case a of+  Assign v' _ | v == untype v' -> a+  Branch cond a b -> case (assignedVar v a, assignedVar v b) of+    (Null, Null) -> Null+    (a, b)       -> Branch cond a b+  Sequence a b -> case (assignedVar v a, assignedVar v b) of+    (Null, Null) -> Null+    (a, b)       -> Sequence a b+  Label a b -> Label a $ assignedVar v b+  _ -> Null 

@@ -7,20 +7,18 @@ import System.IO import Text.Printf -import Language.ImProve.Code+import Language.ImProve.Code () import Language.ImProve.Core import Language.ImProve.Narrow  -- | Verify a program with k-induction. verify :: FilePath -> Int -> Statement -> IO () verify _ maxK _ | maxK < 1 = error "max k can not be less than 1"-verify yices maxK program' = do-  code "narrowing" narrowing-  mapM_ (verifyProgram yices format maxK) $ trimAssertions program+verify yices maxK program = do+  putStrLn "state variable narrowing ..."+  print $ narrow program+  mapM_ (verifyProgram yices format maxK $ narrow program) $ trimAssertions $ labelAssertions program   where-  --XXX Not efficient.  Constraints will get added on every stage.  Only needed at the begining.-  narrowing = narrow program'-  program = labelAssertions $ Sequence narrowing program'   format = "verifying %-" ++ show (maximum [ length $ pathName path | path <- assertions program ]) ++ "s    "  -- | Set of statements containing only one assertion.@@ -90,20 +88,18 @@     _ -> []  -- | Trim all unneeded stuff from a program.-trimProgram :: Statement -> Statement-trimProgram program = trim program+trimProgram :: Statement -> Statement -> Statement+trimProgram base program = trim program   where   vars = fixPoint []-  fixPoint :: [VarInfo] -> [VarInfo]+  fixPoint :: [UV] -> [UV]   fixPoint a = if sort (nub a) == sort (nub b) then sort (nub a) else fixPoint b     where-    b = requiredVars program a+    b = requiredVars base a   trim :: Statement -> Statement   trim a = case a of     Null -> Null-    AssignBool  b _ -> if elem (varInfo b) vars then a else Null-    AssignInt   b _ -> if elem (varInfo b) vars then a else Null-    AssignFloat b _ -> if elem (varInfo b) vars then a else Null+    Assign b _ -> if elem (untype b) vars then a else Null     Branch a b c    -> case (trim b, trim c) of       (Null, Null) -> Null       (b, c)       -> Branch a b c@@ -117,11 +113,9 @@       Null -> Null       a    -> Label name a -requiredVars :: Statement -> [VarInfo] -> [VarInfo]+requiredVars :: Statement -> [UV] -> [UV] requiredVars a required = case a of-  AssignBool  a b -> if elem (varInfo a) required then nub $ varInfo a : exprVars b ++ required else required-  AssignInt   a b -> if elem (varInfo a) required then nub $ varInfo a : exprVars b ++ required else required-  AssignFloat a b -> if elem (varInfo a) required then nub $ varInfo a : exprVars b ++ required else required+  Assign a b -> if elem (untype a) required then nub $ untype a : exprVars b ++ required else required   Branch a b c    -> if any (flip elem $ modifiedVars b ++ modifiedVars c) required || (not $ null $ requiredVars b []) || (not $ null $ requiredVars c [])     then nub $ exprVars a ++ requiredVars b (requiredVars c required)     else required@@ -131,11 +125,9 @@   Label  _ a      -> requiredVars a required   Null            -> required -modifiedVars :: Statement -> [VarInfo]+modifiedVars :: Statement -> [UV] modifiedVars a = case a of-  AssignBool  a _ -> [varInfo a]-  AssignInt   a _ -> [varInfo a]-  AssignFloat a _ -> [varInfo a]+  Assign a _      -> [untype a]   Branch _ b c    -> modifiedVars b ++ modifiedVars c   Sequence a b    -> modifiedVars a ++ modifiedVars b   Assert _        -> []@@ -144,16 +136,15 @@   Null            -> []  -- | Verify a trimmed program.-verifyProgram :: FilePath -> String -> Int -> Statement -> IO ()-verifyProgram yices format maxK program' = do+verifyProgram :: FilePath -> String -> Int -> Statement -> Statement -> IO ()+verifyProgram yices format maxK narrowing program' = do   printf format name   hFlush stdout-  env0 <- initEnv program+  env0 <- initEnv program  --XXX Need to add narrowing assumptions.   execStateT (check yices name maxK program env0 1) env0   return ()   where-  program = trimProgram program'-  --program = program'+  program = Sequence (trimProgram program' narrowing) (trimProgram program' program')   name = pathName $ head' "a1" $ assertions program  head' msg a = if null a then error msg else head a@@ -191,13 +182,13 @@   env <- get   r <- liftIO $ quickCheckY' yices [] $ reverse (cmds env)           ++ [ASSERT $ NOT $ AND $ asserts env]-          ++ [ ASSERT $ VarE (var env0 a) := evalConst' c | a@(input, _, c) <- stmtVars program, not input ]+          ++ [ ASSERT $ VarE (var env0 a) := evalConst' c | a@(input, _, c) <- map varInfo $ stmtVars program, not input ]           ++ [CHECK]   return $ result r  -- | Insert new input variables. inputs :: Statement -> Y ()-inputs program = sequence_ [ addVar' a >>= addTrace . Input' (pathName path) | a@(input, path, _) <- stmtVars program, input ]+inputs program = sequence_ [ addVar' a >>= addTrace . Input' (pathName path) | a@(input, path, _) <- map varInfo $ stmtVars program, input ]  result :: ResY -> Result result a = case a of@@ -211,9 +202,7 @@ evalStmt enabled a = case a of   Null -> return ()   Sequence a b -> evalStmt enabled a >> evalStmt enabled b-  AssignBool  a b -> assign a b-  AssignInt   a b -> assign a b-  AssignFloat a b -> assign a b+  Assign a b -> assign a b   Assert a -> do     a <- evalExpr a     b <- newBoolVar@@ -334,7 +323,7 @@   }   initEnv :: Statement -> IO Env-initEnv program = execStateT (sequence_ [ addVar' a >>= addTrace . Init' (pathName path) | a@(input, path, _) <- stmtVars program, not input ]) Env+initEnv program = execStateT (sequence_ [ addVar' a >>= addTrace . Init' (pathName path) | a@(input, path, _) <- map varInfo $ 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.1.5+version: 0.1.6  category: Language, Formal Methods, Embedded