module Language.Boogie.Util (
TypeBinding,
typeSubst,
renameTypeVars,
fromTVNames,
isFreeIn,
isTypeVar,
unifier,
freshTVName,
tupleType,
freeVarsTwoState,
freeVars,
freeOldVars,
VarBinding,
exprSubst,
paramSubst,
freeSelections,
applications,
preconditions,
postconditions,
modifies,
assumePreconditions,
assumePostconditions,
FSig (..),
fsigType,
fsigFromType,
FDef (..),
ConstraintSet,
AbstractStore,
asUnion,
PSig (..),
psigParams,
psigArgTypes,
psigRetTypes,
psigModifies,
psigRequires,
psigEnsures,
psigType,
PDef (..),
pdefLocals,
num, eneg, enot,
(|+|), (|-|), (|*|), (|/|), (|%|), (|=|), (|!=|), (|<|), (|<=|), (|>|), (|>=|), (|&|), (|||), (|=>|), (|<=>|),
conjunction,
assume,
interval,
fromRight,
deleteAll,
restrictDomain,
removeDomain,
mapItwType,
anyM,
changeState,
withLocalState,
internalError
) where
import Language.Boogie.AST
import Language.Boogie.Position
import Language.Boogie.Tokens
import Data.Maybe
import Data.List
import Data.Map (Map, (!))
import qualified Data.Map as M
import Data.Set (Set)
import qualified Data.Set as S
import Control.Applicative
import Control.Monad.State
import Control.Monad.Stream
import Control.Lens
type TypeBinding = Map Id Type
typeSubst :: TypeBinding -> Type -> Type
typeSubst _ BoolType = BoolType
typeSubst _ IntType = IntType
typeSubst binding (IdType id []) = case M.lookup id binding of
Just t -> t
Nothing -> IdType id []
typeSubst binding (IdType id args) = IdType id (map (typeSubst binding) args)
typeSubst binding (MapType bv domains range) = MapType bv (map (typeSubst removeBound) domains) (typeSubst removeBound range)
where removeBound = deleteAll bv binding
renameTypeVars :: [Id] -> [Id] -> TypeBinding -> TypeBinding
renameTypeVars tv newTV binding = let
tvMap = M.fromList $ zip tv newTV
replace tv = M.findWithDefault tv tv tvMap
tvToType = fromTVNames tv newTV
in M.map (typeSubst tvToType) (M.mapKeys replace binding)
isFreeIn :: Id -> Type -> Bool
x `isFreeIn` (IdType y []) = x == y
x `isFreeIn` (IdType y args) = any (x `isFreeIn`) args
x `isFreeIn` (MapType bv domains range) = x `notElem` bv && any (x `isFreeIn`) (range:domains)
_ `isFreeIn` _ = False
fromTVNames :: [Id] -> [Id] -> TypeBinding
fromTVNames tvs tvs' = M.fromList (zip tvs (map nullaryType tvs'))
freshTVName n = nonIdChar : (show n)
isTypeVar :: [Id] -> Id -> Bool
isTypeVar contextTypeVars v = head v == nonIdChar || v `elem` contextTypeVars
unifier :: [Id] -> [Type] -> [Type] -> Maybe TypeBinding
unifier _ [] [] = Just M.empty
unifier fv (IntType:xs) (IntType:ys) = unifier fv xs ys
unifier fv (BoolType:xs) (BoolType:ys) = unifier fv xs ys
unifier fv ((IdType id1 args1):xs) ((IdType id2 args2):ys) | id1 == id2 = unifier fv (args1 ++ xs) (args2 ++ ys)
unifier fv ((IdType id []):xs) (y:ys) | isTypeVar fv id =
if id `isFreeIn` y then Nothing
else M.insert id y <$> unifier fv (update xs) (update ys)
where update = map (typeSubst (M.singleton id y))
unifier fv (x:xs) ((IdType id []):ys) | isTypeVar fv id =
if id `isFreeIn` x then Nothing
else M.insert id x <$> unifier fv (update xs) (update ys)
where update = map (typeSubst (M.singleton id x))
unifier fv ((MapType bv1 domains1 range1):xs) ((MapType bv2 domains2 range2):ys) =
case forallUnifier fv bv1 (range1:domains1) bv2 (range2:domains2) of
Nothing -> Nothing
Just u -> M.union u <$> (unifier fv (update u xs) (update u ys))
where
update u = map (typeSubst u)
unifier _ _ _ = Nothing
removeClashesWith :: [Id] -> [Id] -> [Id]
removeClashesWith tvs tvs' = map changeName tvs
where
changeName tv = if tv `elem` tvs' then tv ++ replicate (level + 1) nonIdChar else tv
level = maximum [fromJust (findIndex (\c -> c /= nonIdChar) (reverse id)) | id <- tvs ++ tvs']
forallUnifier :: [Id] -> [Id] -> [Type] -> [Id] -> [Type] -> Maybe TypeBinding
forallUnifier fv bv1 xs bv2 ys = if length bv1 /= length bv2 || length xs /= length ys
then Nothing
else case unifier (fv ++ bv1) xs (map withFreshBV ys) of
Nothing -> Nothing
Just u -> let (boundU, freeU) = M.partitionWithKey (\k _ -> k `elem` bv1) u
in if all isFreshBV (M.elems boundU) && not (any hasFreshBV (M.elems freeU))
then Just freeU
else Nothing
where
freshBV = bv2 `removeClashesWith` bv1
withFreshBV = typeSubst (fromTVNames bv2 freshBV)
isFreshBV (IdType id []) = id `elem` freshBV
isFreshBV _ = False
hasFreshBV t = any (`isFreeIn` t) freshBV
tupleType ts = IdType "*Tuple" ts
freeVarsTwoState :: Expression -> ([Id], [Id])
freeVarsTwoState e = freeVarsTwoState' (node e)
freeVarsTwoState' FF = ([], [])
freeVarsTwoState' TT = ([], [])
freeVarsTwoState' (Numeral _) = ([], [])
freeVarsTwoState' (Var x) = ([x], [])
freeVarsTwoState' (Application name args) = over both (nub . concat) (unzip (map freeVarsTwoState args))
freeVarsTwoState' (MapSelection m args) = over both (nub . concat) (unzip (map freeVarsTwoState (m : args)))
freeVarsTwoState' (MapUpdate m args val) = over both (nub . concat) (unzip (map freeVarsTwoState (val : m : args)))
freeVarsTwoState' (Old e) = let (state, old) = freeVarsTwoState e in ([], state ++ old)
freeVarsTwoState' (IfExpr cond e1 e2) = over both (nub . concat) (unzip [freeVarsTwoState cond, freeVarsTwoState e1, freeVarsTwoState e2])
freeVarsTwoState' (Coercion e _) = freeVarsTwoState e
freeVarsTwoState' (UnaryExpression _ e) = freeVarsTwoState e
freeVarsTwoState' (BinaryExpression _ e1 e2) = over both (nub . concat) (unzip [freeVarsTwoState e1, freeVarsTwoState e2])
freeVarsTwoState' (Quantified _ _ boundVars e) = let (state, old) = freeVarsTwoState e in (state \\ map fst boundVars, old)
freeVars = fst . freeVarsTwoState
freeOldVars = snd . freeVarsTwoState
type VarBinding = Map Id BareExpression
exprSubst :: VarBinding -> Expression -> Expression
exprSubst binding (Pos pos e) = attachPos pos $ exprSubst' binding e
exprSubst' binding (Var id) = case M.lookup id binding of
Nothing -> Var id
Just e -> e
exprSubst' binding (Application id args) = Application id (map (exprSubst binding) args)
exprSubst' binding (MapSelection m args) = MapSelection (exprSubst binding m) (map (exprSubst binding) args)
exprSubst' binding (MapUpdate m args val) = MapUpdate (exprSubst binding m) (map (exprSubst binding) args) (exprSubst binding val)
exprSubst' binding (Old e) = Old (exprSubst binding e)
exprSubst' binding (IfExpr cond e1 e2) = IfExpr (exprSubst binding cond) (exprSubst binding e1) (exprSubst binding e2)
exprSubst' binding (Coercion e t) = Coercion (exprSubst binding e) t
exprSubst' binding (UnaryExpression op e) = UnaryExpression op (exprSubst binding e)
exprSubst' binding (BinaryExpression op e1 e2) = BinaryExpression op (exprSubst binding e1) (exprSubst binding e2)
exprSubst' binding (Quantified qop tv boundVars e) = Quantified qop tv boundVars (exprSubst binding' e)
where binding' = deleteAll (map fst boundVars) binding
exprSubst' _ e = e
paramBinding :: PSig -> PDef -> VarBinding
paramBinding sig def = M.fromList $ zip (sigIns ++ sigOuts) (defIns ++ defOuts)
where
sigIns = map itwId $ psigArgs sig
sigOuts = map itwId $ psigRets sig
defIns = map Var $ pdefIns def
defOuts = map Var $ pdefOuts def
paramSubst :: PSig -> PDef -> Expression -> Expression
paramSubst sig def = if not (pdefParamsRenamed def)
then id
else exprSubst (paramBinding sig def)
freeSelections :: Expression -> [(Id, [Expression])]
freeSelections expr = freeSelections' $ node expr
freeSelections' FF = []
freeSelections' TT = []
freeSelections' (Numeral _) = []
freeSelections' (Var x) = []
freeSelections' (Application name args) = nub . concat $ map freeSelections args
freeSelections' (MapSelection m args) = case node m of
Var name -> (name, args) : (nub . concat $ map freeSelections args)
_ -> nub . concat $ map freeSelections (m : args)
freeSelections' (MapUpdate m args val) = nub . concat $ map freeSelections (val : m : args)
freeSelections' (Old e) = internalError "freeSelections should only be applied in single-state context"
freeSelections' (IfExpr cond e1 e2) = nub . concat $ [freeSelections cond, freeSelections e1, freeSelections e2]
freeSelections' (Coercion e _) = freeSelections e
freeSelections' (UnaryExpression _ e) = freeSelections e
freeSelections' (BinaryExpression _ e1 e2) = nub . concat $ [freeSelections e1, freeSelections e2]
freeSelections' (Quantified _ _ boundVars e) = let boundVarNames = map fst boundVars
in [(m, args) | (m, args) <- freeSelections e, m `notElem` boundVarNames]
applications :: Expression -> [(Id, [Expression])]
applications expr = applications' $ node expr
applications' FF = []
applications' TT = []
applications' (Numeral _) = []
applications' (Var x) = []
applications' (Application name args) = (name, args) : (nub . concat $ map applications args)
applications' (MapSelection m args) = nub . concat $ map applications (m : args)
applications' (MapUpdate m args val) = nub . concat $ map applications (val : m : args)
applications' (Old e) = internalError "applications should only be applied in single-state context"
applications' (IfExpr cond e1 e2) = nub . concat $ [applications cond, applications e1, applications e2]
applications' (Coercion e _) = applications e
applications' (UnaryExpression _ e) = applications e
applications' (BinaryExpression _ e1 e2) = nub . concat $ [applications e1, applications e2]
applications' (Quantified _ _ _ e) = applications e
preconditions :: [Contract] -> [SpecClause]
preconditions specs = catMaybes (map extractPre specs)
where
extractPre (Requires f e) = Just (SpecClause Precondition f e)
extractPre _ = Nothing
postconditions :: [Contract] -> [SpecClause]
postconditions specs = catMaybes (map extractPost specs)
where
extractPost (Ensures f e) = Just (SpecClause Postcondition f e)
extractPost _ = Nothing
modifies :: [Contract] -> [Id]
modifies specs = (nub . concat . catMaybes) (map extractMod specs)
where
extractMod (Modifies _ ids) = Just ids
extractMod _ = Nothing
assumePreconditions :: PSig -> PSig
assumePreconditions sig = sig { psigContracts = map assumePrecondition (psigContracts sig) }
where
assumePrecondition (Requires _ e) = Requires True e
assumePrecondition c = c
assumePostconditions :: PSig -> PSig
assumePostconditions sig = sig { psigContracts = map assumePostcondition (psigContracts sig) }
where
assumePostcondition (Ensures _ e) = Ensures True e
assumePostcondition c = c
data FSig = FSig {
fsigName :: Id,
fsigTypeVars :: [Id],
fsigArgTypes :: [Type],
fsigRetType :: Type
}
fsigType sig = MapType (fsigTypeVars sig) (fsigArgTypes sig) (fsigRetType sig)
fsigFromType (MapType tv domainTypes rangeType) = FSig "" tv domainTypes rangeType
instance Eq FSig where
s1 == s2 = fsigName s1 == fsigName s2
data FDef = FDef {
fdefName :: Id,
fdefTV :: [Id],
fdefArgs :: [IdType],
fdefGuard :: Expression,
fdefBody :: Expression
}
type ConstraintSet = ([FDef], [FDef])
type AbstractStore = Map Id ConstraintSet
asUnion :: AbstractStore -> AbstractStore -> AbstractStore
asUnion s1 s2 = M.unionWith (\(d1, c1) (d2, c2) -> (d1 ++ d2, c1 ++ c2)) s1 s2
data PSig = PSig {
psigName :: Id,
psigTypeVars :: [Id],
psigArgs :: [IdTypeWhere],
psigRets :: [IdTypeWhere],
psigContracts :: [Contract]
}
instance Eq PSig where
s1 == s2 = psigName s1 == psigName s2
psigParams sig = psigArgs sig ++ psigRets sig
psigArgTypes = (map itwType) . psigArgs
psigRetTypes = (map itwType) . psigRets
psigType sig = MapType (psigTypeVars sig) (psigArgTypes sig) (tupleType $ psigRetTypes sig)
psigModifies = modifies . psigContracts
psigRequires = preconditions . psigContracts
psigEnsures = postconditions . psigContracts
data PDef = PDef {
pdefIns :: [Id],
pdefOuts :: [Id],
pdefParamsRenamed :: Bool,
pdefBody :: BasicBody,
pdefConstraints :: AbstractStore,
pdefPos :: SourcePos
}
pdefLocals def = pdefIns def ++ pdefOuts def ++ map itwId (fst (pdefBody def))
num i = gen $ Numeral i
eneg e = inheritPos (UnaryExpression Neg) e
enot e = inheritPos (UnaryExpression Not) e
e1 |+| e2 = inheritPos2 (BinaryExpression Plus) e1 e2
e1 |-| e2 = inheritPos2 (BinaryExpression Minus) e1 e2
e1 |*| e2 = inheritPos2 (BinaryExpression Times) e1 e2
e1 |/| e2 = inheritPos2 (BinaryExpression Div) e1 e2
e1 |%| e2 = inheritPos2 (BinaryExpression Mod) e1 e2
e1 |=| e2 = inheritPos2 (BinaryExpression Eq) e1 e2
e1 |!=| e2 = inheritPos2 (BinaryExpression Neq) e1 e2
e1 |<| e2 = inheritPos2 (BinaryExpression Ls) e1 e2
e1 |<=| e2 = inheritPos2 (BinaryExpression Leq) e1 e2
e1 |>| e2 = inheritPos2 (BinaryExpression Gt) e1 e2
e1 |>=| e2 = inheritPos2 (BinaryExpression Geq) e1 e2
e1 |&| e2 = inheritPos2 (BinaryExpression And) e1 e2
e1 ||| e2 = inheritPos2 (BinaryExpression Or) e1 e2
e1 |=>| e2 = inheritPos2 (BinaryExpression Implies) e1 e2
e1 |<=>| e2 = inheritPos2 (BinaryExpression Equiv) e1 e2
assume e = attachPos (position e) (Predicate (SpecClause Inline True e))
conjunction [] = gen TT
conjunction es = foldl1 (|&|) es
interval (lo, hi) = [lo..hi]
fromRight :: Either a b -> b
fromRight (Right x) = x
deleteAll :: Ord k => [k] -> Map k a -> Map k a
deleteAll keys m = foldr M.delete m keys
restrictDomain :: Ord k => Set k -> Map k a -> Map k a
restrictDomain keys m = M.filterWithKey (\k _ -> k `S.member` keys) m
removeDomain :: Ord k => Set k -> Map k a -> Map k a
removeDomain keys m = M.filterWithKey (\k _ -> k `S.notMember` keys) m
mapItwType f (IdTypeWhere i t w) = IdTypeWhere i (f t) w
anyM :: Monad m => (a -> m Bool) -> [a] -> m Bool
anyM _ [] = return False
anyM pred (x : xs) = do
res <- pred x
if res then return True else anyM pred xs
allM :: Monad m => (a -> m Bool) -> [a] -> m Bool
allM _ [] = return True
allM pred (x : xs) = do
res <- pred x
if not res then return False else allM pred xs
changeState :: Monad m => (s -> t) -> (t -> s -> s) -> StateT t m a -> StateT s m a
changeState getter modifier e = do
st <- gets getter
(res, st') <- lift $ runStateT e st
modify $ modifier st'
return res
withLocalState :: Monad m => (s -> t) -> StateT t m a -> StateT s m a
withLocalState localState e = changeState localState (flip const) e
internalError msg = error $ "Internal interpreter error (consider submitting a bug report):\n" ++ msg