improve 0.0.5 → 0.0.6

raw patch · 6 files changed

+120/−97 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 +15/−19
• Language/ImProve/Code.hs +5/−5
• Language/ImProve/Core.hs +8/−14
• Language/ImProve/Examples.hs +26/−22
• Language/ImProve/Verify.hs +65/−36
• improve.cabal +1/−1

@@ -49,7 +49,7 @@   , Stmt   -- ** Hierarchical Scope and Annotations   , scope-  , annotate+  , label   -- ** Variable Declarations   , bool   , bool'@@ -214,7 +214,7 @@ mux :: AllE a => E Bool -> E a -> E a -> E a mux = Mux --- | Creates a hierarchical scope.+-- | Creates a hierarchical scope for variable names. scope :: Name -> Stmt a -> Stmt a scope name stmt = do   (path0, stmt0) <- get@@ -224,15 +224,15 @@   put (path0, stmt1)   return a --- | Add an annotation to a statement.  Useful for requirement trace tags.-annotate :: Name -> Stmt a -> Stmt a-annotate name stmt = do+-- | Labels a statement.  Useful for requirement trace tags or other annotations.+label :: Name -> Stmt a -> Stmt a+label name stmt = do   (path0, stmt0) <- get   put (path0, Null)   a <- stmt   (_, stmt1) <- get   put (path0, stmt0)-  statement $ Annotate name stmt1+  statement $ Label name stmt1   return a    get :: Stmt ([Name], Statement)@@ -322,28 +322,24 @@ instance Assign Float where a <== b = statement $ AssignFloat a b  -- | Assert that a condition is true.-assert :: Name -> E Bool -> Stmt ()-assert a b = do-  path <- getPath-  statement $ Assert (path ++ [a]) b+assert :: E Bool -> Stmt ()+assert = statement . Assert  -- | Declare an assumption condition is true.-assume :: Name -> E Bool -> Stmt ()-assume a b = do-  path <- getPath-  statement $ Assume (path ++ [a]) b+assume :: E Bool -> Stmt ()+assume = statement . Assume  -- | Conditional if-else.-ifelse :: Name -> E Bool -> Stmt () -> Stmt () -> Stmt ()-ifelse name cond onTrue onFalse = do+ifelse :: E Bool -> Stmt () -> Stmt () -> Stmt ()+ifelse cond onTrue onFalse = do   path <- getPath   let (_, stmt1) = evalStmt path onTrue       (_, stmt2) = evalStmt path onFalse-  statement $ Branch (path ++ [name]) cond stmt1 stmt2+  statement $ Branch cond stmt1 stmt2  -- | Conditional if without the else.-if_ :: Name -> E Bool -> Stmt () -> Stmt()-if_ name cond stmt = ifelse name cond stmt $ return ()+if_ :: E Bool -> Stmt () -> Stmt()+if_ cond stmt = ifelse cond stmt $ return ()  -- | Verify a program. --

@@ -29,12 +29,12 @@   AssignBool  a b -> pathName a ++ " = " ++ codeExpr b ++ ";\n"   AssignInt   a b -> pathName a ++ " = " ++ codeExpr b ++ ";\n"   AssignFloat a b -> pathName a ++ " = " ++ codeExpr b ++ ";\n"-  Branch path a b Null -> "// if_ "    ++ pathName path ++ "\nif (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\n"-  Branch path a b c    -> "// ifelse " ++ pathName path ++ "\nif (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\nelse {\n" ++ indent (codeStmt c) ++ "}\n"+  Branch a b Null -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\n"+  Branch a b c    -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\nelse {\n" ++ indent (codeStmt c) ++ "}\n"   Sequence a b -> codeStmt a ++ codeStmt b-  Assert path a -> "// assert " ++ pathName path ++ "\nassert(" ++ codeExpr a ++ ");\n"-  Assume path a -> "// assume " ++ pathName path ++ "\nassert(" ++ codeExpr a ++ ");\n"-  Annotate name a -> "// annotate " ++ name ++ "\n" ++ indent (codeStmt a)+  Assert a -> "assert(" ++ codeExpr a ++ ");\n"+  Assume a -> "assert(" ++ codeExpr a ++ ");\n"+  Label  name a -> "// " ++ name ++ "\n" ++ indent (codeStmt a)   Null -> ""  codeExpr :: E a -> String

@@ -27,12 +27,6 @@ instance PathName Path      where pathName = intercalate "." instance PathName (V a)     where pathName (V _ path _) = pathName path instance PathName VarInfo   where pathName (_, path, _) = pathName path-instance PathName Statement where-  pathName a = case a of-    Branch p _ _ _ -> pathName p-    Assert p _     -> pathName p-    Assume p _     -> pathName p-    _ -> undefined  class AllE a where   zero   :: (Name -> a -> m (V a)) -> a@@ -93,11 +87,11 @@   = AssignBool  (V Bool ) (E Bool )   | AssignInt   (V Int  ) (E Int  )   | AssignFloat (V Float) (E Float)-  | Branch      Path (E Bool) Statement Statement+  | Branch      (E Bool) Statement Statement   | Sequence    Statement Statement-  | Assert      Path (E Bool)-  | Assume      Path (E Bool)-  | Annotate    Name Statement+  | Assert      (E Bool)+  | Assume      (E Bool)+  | Label       Name Statement   | Null  data Const@@ -117,11 +111,11 @@   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+  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-  Annotate _ a    -> stmtVars a+  Assert a        -> exprVars a+  Assume a        -> exprVars a+  Label  _ a      -> stmtVars a   Null            -> []  -- Information about all of an expressions's variables.

@@ -25,18 +25,18 @@   b1 <- int "b1" 0  -- Working copy of 'b'.    -- A new input to process.-  if_ "startNew" (a /=. ref a0 ||. b /=. ref b0) $ do+  label "startNew" $ if_ (a /=. ref a0 ||. b /=. ref b0) $ do     a0 <== a     b0 <== b     a1 <== a     b1 <== b    -- Reduce a1.-  if_ "reduceA" (ref a1 >. ref b1) $ do+  label "reduceA" $ if_ (ref a1 >. ref b1) $ do     a1 <== ref a1 - ref b1    -- Reduce b1.-  if_ "reduceB" (ref b1 >. ref a1) $ do+  label "reduceB" $ if_ (ref b1 >. ref a1) $ do     b1 <== ref b1 - ref a1    -- Done if a1 == b1.@@ -72,11 +72,11 @@   counter <- int "counter" 0    -- Specification.-  assert "GreaterThanOrEqualTo0" $ ref counter >=. 0-  assert "LessThan10"            $ ref counter <.  10+  label "GreaterThanOrEqualTo0" $ assert $ ref counter >=. 0+  label "LessThan10"            $ assert $ ref counter <.  10    -- Implementation.-  ifelse "ResetCounter" (ref counter ==. 10) (counter <== 0) (counter <== ref counter + 1)+  ifelse (ref counter ==. 10) (counter <== 0) (counter <== ref counter + 1)    -- Alternatives to try.   --ifelse "ResetCounter" (ref counter >=. 9) (counter <== 0) (counter <== ref counter + 1)@@ -93,25 +93,29 @@ arbiterSpec (requestA, requestB, requestC) (grantA, grantB, grantC) = do    -- Mutual exclusion.  At most, only one requester granted at a time.-  assert "OneHot" $      grantA &&. not_ grantB &&. not_ grantC-                ||. not_ grantA &&.      grantB &&. not_ grantC-                ||. not_ grantA &&. not_ grantB &&.      grantC-                ||. not_ grantA &&. not_ grantB &&. not_ grantC+  label "OneHot" $ assert $      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.-  assert "NotRequestedA" $ imply (not_ requestA) (not_ grantA)-  assert "NotRequestedB" $ imply (not_ requestB) (not_ grantB)-  assert "NotRequestedC" $ imply (not_ requestC) (not_ grantC)+  --label "NotRequestedA" $ assert $ imply (not_ requestA) (not_ grantA)+  --label "NotRequestedB" $ assert $ imply (not_ requestB) (not_ grantB)+  --label "NotRequestedC" $ assert $ imply (not_ requestC) (not_ grantC)+  label "test" $ label "test2" $ do+    assert $ imply (not_ requestA) (not_ grantA)+    assert $ imply (not_ requestB) (not_ grantB)+    assert $ imply (not_ requestC) (not_ grantC)    -- Grants to single requests.-  assert "OnlyRequestA" $ imply (     requestA &&. not_ requestB &&. not_ requestC) grantA-  assert "OnlyRequestB" $ imply (not_ requestA &&.      requestB &&. not_ requestC) grantB-  assert "OnlyRequestC" $ imply (not_ requestA &&. not_ requestB &&.      requestC) grantC+  label "OnlyRequestA" $ assert $ imply (     requestA &&. not_ requestB &&. not_ requestC) grantA+  label "OnlyRequestB" $ assert $ imply (not_ requestA &&.      requestB &&. not_ requestC) grantB+  label "OnlyRequestC" $ assert $ imply (not_ requestA &&. not_ requestB &&.      requestC) grantC    -- Priority.-  assert "Highest" $ imply requestA grantA-  assert "Medium"  $ imply (not_ requestA &&. requestB) grantB-  assert "Lowest"  $ imply (not_ requestA &&. not_ requestB &&. requestC) grantC+  label "Highest" $ assert $ imply requestA grantA+  label "Medium"  $ assert $ imply (not_ requestA &&. requestB) grantB+  label "Lowest"  $ assert $ imply (not_ requestA &&. not_ requestB &&. requestC) grantC  -- | An arbiter implementation. arbiter1 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)@@ -128,9 +132,9 @@   grantB <- bool "grantB" False   grantC <- bool "grantC" False -  if_ "GrantA" (requestA)                                     (grantA <== true)-  if_ "GrantB" (not_ requestA &&. requestB)                   (grantB <== true)-  if_ "GrantC" (not_ requestA &&. not_ requestB &&. requestC) (grantC <== true)+  label "GrantA" $ if_ (requestA)                                     (grantA <== true)+  label "GrantB" $ if_ (not_ requestA &&. requestB)                   (grantB <== true)+  label "GrantC" $ if_ (not_ requestA &&. not_ requestB &&. requestC) (grantC <== true)    return (ref grantA, ref grantB, ref grantC) 

@@ -1,6 +1,6 @@ module Language.ImProve.Verify (verify) where -import Control.Monad.State hiding (State)+import Control.Monad.State import Math.SMT.Yices.Pipe import Math.SMT.Yices.Syntax import System.IO@@ -16,6 +16,7 @@   where   format = "verifying %-" ++ show (maximum [ length $ pathName path | path <- assertions program ]) ++ "s    " + -- | Set of statements containing only one assertion. trimAssertions :: Statement -> [Statement] trimAssertions program = [ a | a <- trimAssertions' program, length (assertions a) == 1 ]@@ -24,28 +25,56 @@ trimAssertions' a = case a of   Sequence a b -> [ Sequence a (removeAssertions b) | a <- trimAssertions' a ]                ++ [ Sequence (removeAssertions a) b | b <- trimAssertions' b ]-  Branch path cond a b -> [ Branch path cond a (removeAssertions b) | a <- trimAssertions' a ]-                       ++ [ Branch path cond (removeAssertions a) b | b <- trimAssertions' b ]-  Annotate name a -> [ Annotate name a | a <- trimAssertions a ]+  Branch cond a b -> [ Branch cond a (removeAssertions b) | a <- trimAssertions' a ]+                  ++ [ Branch cond (removeAssertions a) b | b <- trimAssertions' b ]+  Label name a -> [ Label name a | a <- trimAssertions' a ]   a -> [a]  -- | Remove all assertions. removeAssertions :: Statement -> Statement removeAssertions a = case a of-  Assert _ _ -> Null+  Assert _ -> Null   Sequence a b -> Sequence (removeAssertions a) (removeAssertions b)-  Branch path cond a b -> Branch path cond (removeAssertions a) (removeAssertions b)-  Annotate name a -> Annotate name $ removeAssertions a+  Branch cond a b -> Branch cond (removeAssertions a) (removeAssertions b)+  Label name a -> Label name $ removeAssertions a   a -> a +{-+-- | Ensures all assertions are labed, though not uniquely.+labelAssertions :: Statement -> Statement+labelAssertions program = evalState (f program) 1+  where+  f :: Statement -> State Int Statement+  f a = case a of+    Branch a b c -> do+      b <- f b+      c <- f c+      return $ Branch a b c+    Sequence a b -> do+      a <- f a+      b <- f b+      return $ Sequence a b+    Assert a -> do+      n <- get+      put $ n + 1+      return $ Label (show n) $ Assert a+    Label name a -> do+      a <- f a+      return $ Label name a+    a -> return a+-}+ -- | Paths of all assertions. assertions :: Statement -> [Path]-assertions a = case a of-  Assert path _  -> [path]-  Sequence a b   -> assertions a ++ assertions b-  Branch _ _ a b -> assertions a ++ assertions b-  Annotate _ a   -> assertions a-  _ -> []+assertions = assertions []+  where+  assertions :: Path -> Statement -> [Path]+  assertions path a = case a of+    Assert _ -> [path]+    Sequence a b -> assertions path a ++ assertions path b+    Branch _ a b -> assertions path a ++ assertions path b+    Label name a -> assertions (path ++ [name]) a+    _ -> []  -- | Trim all unneeded stuff from a program. trimProgram :: Statement -> Statement@@ -75,13 +104,13 @@   evalStmt (LitB True) program   resultBasis <- checkBasis yices program env0   case resultBasis of-    Fail a  -> liftIO (printf "FAILED: disproved basis in k = %d (see trace)\n" k) >> writeTrace name a+    Fail a  -> liftIO (printf "FAILED: disproved basis in k = %d (see %s.trace)\n" k name) >> writeTrace name a     Problem -> error "Verify.check1"     Pass -> do       resultStep <- checkStep yices       case resultStep of         Fail a | k < maxK  -> check yices name maxK program env0 (k + 1)-               | otherwise -> liftIO (printf "inconclusive: unable to proved step up to max k = %d (see trace)\n" k) >> writeTrace name a+               | otherwise -> liftIO (printf "inconclusive: unable to proved step up to max k = %d (see %s.trace)\n" k name) >> writeTrace name a         Problem -> error "Verify.check2"         Pass    -> liftIO $ printf "passed: proved step in k = %d\n" k         @@ -121,17 +150,17 @@   AssignBool  a b -> assign a b   AssignInt   a b -> assign a b   AssignFloat a b -> assign a b-  Assert path a -> do+  Assert a -> do     a <- evalExpr a     b <- newBoolVar     addCmd $ ASSERT (VarE b := (enabled :=> a))     env <- get     put env { asserts = VarE b : asserts env }-    addTrace $ Assert' (pathName path) b-  Assume _ a -> do+    addTrace $ Assert' b+  Assume a -> do     a <- evalExpr a     addCmd $ ASSERT (enabled :=> a)-  Branch path a onTrue onFalse -> do+  Branch a onTrue onFalse -> do     a <- evalExpr a     b <- newBoolVar     addCmd $ ASSERT (VarE b := a)@@ -142,13 +171,13 @@     put env1 { trace = [] }     evalStmt (AND [enabled, NOT a]) onFalse     env2 <- get-    put env2 { trace = Branch' (pathName path) b (reverse $ trace env1) (reverse $ trace env2) : trace env0 }-  Annotate name a -> do+    put env2 { trace = Branch' b (reverse $ trace env1) (reverse $ trace env2) : trace env0 }+  Label name a -> do     env0 <- get     put env0 { trace = [] }     evalStmt enabled a     env1 <- get-    put env1 { trace = Annotate' name (reverse $ trace env1) : trace env0 }+    put env1 { trace = Label' name (reverse $ trace env1) : trace env0 }   where   assign :: AllE a => V a -> E a -> Y ()   assign a b = do@@ -250,13 +279,13 @@   }  data Trace-  = Init'     Name Var-  | Cycle'    Int-  | Input'    Name Var-  | Assign'   Name Var-  | Assert'   Name Var-  | Branch'   Name Var [Trace] [Trace] -  | Annotate' Name [Trace]+  = Init'   Name Var+  | Cycle'  Int+  | Input'  Name Var+  | Assign' Name Var+  | Assert' Var+  | Branch' Var [Trace] [Trace] +  | Label'  Name [Trace]  addVar' :: VarInfo -> Y String addVar' v = do@@ -316,15 +345,15 @@     Assign' path var -> case lookup var table of       Nothing -> ""       Just value -> path ++ " <== " ++ value ++ "\n"-    Assert' path var -> case lookup var table of-      Just "true"  -> "assertion passed: " ++ path ++ "\n"-      Just "false" -> "assertion FAILED: " ++ path ++ "\n"+    Assert' var -> case lookup var table of+      Just "true"  -> "assertion passed\n"+      Just "false" -> "assertion FAILED\n"       _ -> ""-    Branch' path cond onTrue onFalse -> case lookup cond table of-      Just "true"  -> "ifelse " ++ path ++ " true\n"  ++ indent (concatMap f onTrue)-      Just "false" -> "ifelse " ++ path ++ " false\n" ++ indent (concatMap f onFalse)+    Branch' cond onTrue onFalse -> case lookup cond table of+      Just "true"  -> "ifelse true:\n"  ++ indent (concatMap f onTrue)+      Just "false" -> "ifelse false:\n" ++ indent (concatMap f onFalse)       _ -> ""-    Annotate' name traces -> "annotate " ++ name ++ "\n" ++ indent (concatMap f traces)+    Label' name traces -> name ++ ":\n" ++ indent (concatMap f traces)  indent :: String -> String indent = unlines . map ("    " ++) . lines

@@ -1,5 +1,5 @@ name:    improve-version: 0.0.5+version: 0.0.6  category: Language