module Language.Boogie.BasicBlocks (toBasicBlocks, startLabel) where
import Language.Boogie.AST
import Language.Boogie.Util
import Language.Boogie.Position
import Data.Map (Map, (!))
import qualified Data.Map as M
import Control.Monad.State
import Control.Applicative
toBasicBlocks :: Block -> [BasicBlock]
toBasicBlocks body = let
tbs = evalState (concat <$> (mapM (transform M.empty) (map node body))) 0
tbs' = attach startLabel (tbs ++ [justBareStatement Return])
append :: [BasicBlock] -> BareLStatement -> [BasicBlock]
append bbs ([l], Pos _ Skip) = (l, []) : bbs
append bbs ([l], s) = (l, [s]) : bbs
append ((l, ss) : bbs) ([], s) = (l, ss ++ [s]) : bbs
in
reverse (foldl append [] tbs')
startLabel = "00_start"
attach :: Id -> [BareLStatement] -> [BareLStatement]
attach l (([], stmts) : lsts) = ([l], stmts) : lsts
justBareStatement s = ([], gen s)
justStatement pos s = ([], Pos pos s)
justLabel l = ([l], gen Skip)
innermost = "innermost"
genFreshLabel :: String -> Int -> (String, Int)
genFreshLabel kind i = (show i ++ "_" ++ kind, i + 1)
transform :: Map Id Id -> BareLStatement -> State Int [BareLStatement]
transform m (l:lbs, Pos p Skip) = do
t <- transform m (lbs, Pos p Skip)
return $ (justBareStatement $ Goto [l]) : attach l t
transform m (l:lbs, stmt) = do
lDone <- state $ genFreshLabel "done"
t <- transform (M.insert l lDone m) (lbs, stmt)
return $ [justBareStatement $ Goto [l]] ++ attach l t ++ [justBareStatement $ Goto [lDone], justLabel lDone]
transform m ([], Pos p stmt) = case stmt of
Goto lbs -> do
lUnreach <- state $ genFreshLabel "unreachable"
return $ [justStatement p (Goto lbs), justLabel lUnreach]
Break (Just l) -> do
lUnreach <- state $ genFreshLabel "unreachable"
return $ [justStatement p (Goto [m ! l]), justLabel lUnreach]
Break Nothing -> do
lUnreach <- state $ genFreshLabel "unreachable"
return $ [justStatement p (Goto [m ! innermost]), justLabel lUnreach]
Return -> do
lUnreach <- state $ genFreshLabel "unreachable"
return $ [justStatement p Return, justLabel lUnreach]
If cond thenBlock Nothing -> transform m (justStatement p (If cond thenBlock (Just [])))
If we thenBlock (Just elseBlock) -> do
lThen <- state $ genFreshLabel "then"
lElse <- state $ genFreshLabel "else"
lDone <- state $ genFreshLabel "done"
t1 <- transBlock m thenBlock
t2 <- transBlock m elseBlock
case we of
Wildcard -> return $
[justBareStatement $ Goto [lThen, lElse]] ++
attach lThen (t1 ++ [justBareStatement $ Goto [lDone]]) ++
attach lElse (t2 ++ [justBareStatement $ Goto [lDone]]) ++
[justLabel lDone]
Expr e -> return $
[justBareStatement $ Goto [lThen, lElse]] ++
[([lThen], assume e)] ++ t1 ++ [justBareStatement $ Goto [lDone]] ++
[([lElse], assume (enot e))] ++ t2 ++ [justBareStatement $ Goto [lDone]] ++
[justLabel lDone]
While Wildcard invs body -> do
lHead <- state $ genFreshLabel "head"
lBody <- state $ genFreshLabel "body"
lDone <- state $ genFreshLabel "done"
t <- transBlock (M.insert innermost lDone m) body
return $
[justBareStatement $ Goto [lHead]] ++
attach lHead (map checkInvariant invs ++ [justBareStatement $ Goto [lBody, lDone]]) ++
attach lBody (t ++ [justBareStatement $ Goto [lHead]]) ++
[justLabel lDone]
While (Expr e) invs body -> do
lHead <- state $ genFreshLabel "head"
lBody <- state $ genFreshLabel "body"
lGDone <- state $ genFreshLabel "guarded_done"
lDone <- state $ genFreshLabel "done"
t <- transBlock (M.insert innermost lDone m) body
return $
[justBareStatement $ Goto [lHead]] ++
attach lHead (map checkInvariant invs ++ [justBareStatement $ Goto [lBody, lGDone]]) ++
[([lBody], assume e)] ++ t ++ [justBareStatement $ Goto [lHead]] ++
[([lGDone], assume (enot e))] ++ [justBareStatement $ Goto [lDone]] ++
[justLabel lDone]
_ -> return [justStatement p stmt]
where
transBlock m b = concat <$> mapM (transform m) (map node b)
checkInvariant inv = justStatement (position (specExpr inv)) (Predicate inv)