improve 0.0.6 → 0.0.7

raw patch · 4 files changed

+76/−29 lines, 4 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Language/ImProve/Core.hs +1/−1
• Language/ImProve/Examples.hs +3/−7
• Language/ImProve/Verify.hs +71/−20
• improve.cabal +1/−1

@@ -98,7 +98,7 @@   = Bool  Bool   | Int   Int   | Float Float-  deriving Eq+  deriving (Eq, Ord)  type VarInfo = (Bool, Path, Const) 

@@ -99,13 +99,9 @@                         ||. not_ grantA &&. not_ grantB &&. not_ grantC      -- No grants without requests.-  --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)+  label "NotRequestedA" $ assert $ imply (not_ requestA) (not_ grantA)+  label "NotRequestedB" $ assert $ imply (not_ requestB) (not_ grantB)+  label "NotRequestedC" $ assert $ imply (not_ requestC) (not_ grantC)    -- Grants to single requests.   label "OnlyRequestA" $ assert $ imply (     requestA &&. not_ requestB &&. not_ requestC) grantA

@@ -1,6 +1,7 @@ module Language.ImProve.Verify (verify) where  import Control.Monad.State+import Data.List import Math.SMT.Yices.Pipe import Math.SMT.Yices.Syntax import System.IO@@ -11,24 +12,25 @@ -- | 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+verify yices maxK program' = do   mapM_ (verifyProgram yices format maxK) $ trimAssertions program   where+  program = labelAssertions program'   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 ]--trimAssertions' :: Statement -> [Statement]-trimAssertions' a = case a of-  Sequence a b -> [ Sequence a (removeAssertions b) | a <- trimAssertions' a ]-               ++ [ Sequence (removeAssertions a) b | b <- trimAssertions' b ]-  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]+trimAssertions program = [ a | a <- trimAssertions program, length (assertions a) == 1 ]+  where+  trimAssertions :: Statement -> [Statement]+  trimAssertions a = case a of+    Sequence a b -> [ Sequence a (removeAssertions b) | a <- trimAssertions a ]+                 ++ [ Sequence (removeAssertions a) b | b <- trimAssertions b ]+    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@@ -39,12 +41,11 @@   Label name a -> Label name $ removeAssertions a   a -> a -{---- | Ensures all assertions are labed, though not uniquely.+-- | Ensure all assertions are uniquely labed. labelAssertions :: Statement -> Statement-labelAssertions program = evalState (f program) 1+labelAssertions program = evalState (f program) ([], [], 1)   where-  f :: Statement -> State Int Statement+  f :: Statement -> State (Path, [Path], Int) Statement   f a = case a of     Branch a b c -> do       b <- f b@@ -55,14 +56,22 @@       b <- f b       return $ Sequence a b     Assert a -> do-      n <- get-      put $ n + 1-      return $ Label (show n) $ Assert a+      (path, paths, n) <- get+      if elem path paths+        then do+          put (path, paths, n + 1)+          f $ Label (show n) $ Assert a+        else do+          put (path, path : paths, n)+          return $ Assert a     Label name a -> do+      (path, paths, n) <- get+      put (path ++ [name], paths, n)       a <- f a+      (_, paths, n) <- get+      put (path, paths, n)       return $ Label name a     a -> return a--}  -- | Paths of all assertions. assertions :: Statement -> [Path]@@ -78,7 +87,49 @@  -- | Trim all unneeded stuff from a program. trimProgram :: Statement -> Statement-trimProgram = id --XXX+trimProgram program = program+  where+  vars = fixPoint []+  fixPoint :: [VarInfo] -> [VarInfo]+  fixPoint a = if sort (nub a) == sort (nub b) then sort (nub a) else fixPoint b+    where+    b = requiredVars program 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+    Branch a b c    -> case (trim b, trim c) of+      (Null, Null) -> Null+      (b, c)       -> Branch a b c+    Sequence a b    -> case (trim a, trim b) of+      (Null, a) -> a+      (a, Null) -> a+      (a, b)    -> Sequence a b+    Assert a -> if any (flip elem vars) (exprVars a) then Assert a else Null+    Assume a -> if any (flip elem vars) (exprVars a) then Assume a else Null+    Label name a -> case trim a of+      Null -> Null+      a    -> Label name a++requiredVars :: Statement -> [VarInfo] -> [VarInfo]+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+  Branch a b c    -> if (not $ null $ reqB \\ required) || (not $ null $ reqC \\ required)+    then nub $ exprVars a ++ requiredVars b (requiredVars c required)+    else required+    where+    reqB = requiredVars b required+    reqC = requiredVars c required+  Sequence a b    -> requiredVars a (requiredVars b required)+  Assert a        -> nub $ exprVars a ++ required+  Assume a        -> if any (flip elem required) (exprVars a) then nub $ exprVars a ++ required else required+  Label  _ a      -> requiredVars a required+  Null            -> required+  -- | Verify a trimmed program. verifyProgram :: FilePath -> String -> Int -> Statement -> IO ()

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