{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Strict #-}
{-# LANGUAGE ViewPatterns #-}
module Tokstyle.C.Linter.BorrowCheck (descr) where
import Control.Monad (foldM, forM_, mplus, unless,
when)
import Data.List (findIndex)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (fromMaybe, isNothing,
listToMaybe, mapMaybe)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Traversable (forM)
import Language.C.Analysis.AstAnalysis (ExprSide (..), tExpr)
import Language.C.Analysis.SemRep
import Language.C.Analysis.TravMonad (Trav, lookupObject)
import Language.C.Analysis.TypeUtils (canonicalType)
import Language.C.Data.Ident (Ident (..))
import Language.C.Data.Node (NodeInfo, nodeInfo)
import Language.C.Syntax.AST
import Prettyprinter (Pretty, pretty)
import qualified Prettyprinter as PP
import Prettyprinter.Render.Terminal (AnsiStyle)
import Tokstyle.Analysis.AccessPath
import Tokstyle.Analysis.Dataflow as Dataflow
import Tokstyle.C.Analysis.CFG as CFG
import Tokstyle.C.Analysis.Liveness (Liveness, liveness)
import Tokstyle.C.Env (DiagnosticLevel (..),
DiagnosticSpan (..), Env,
posAndLen, recordLinterError,
recordRichError)
data VarState
= StateUninitialized NodeInfo
| StateOwned NodeInfo
| StateSharedBorrowedFrom AccessPath NodeInfo
| StateMutableBorrowedFrom AccessPath NodeInfo
| StateMoved NodeInfo
| StateInconsistent NodeInfo NodeInfo
deriving (Int -> VarState -> ShowS
[VarState] -> ShowS
VarState -> String
(Int -> VarState -> ShowS)
-> (VarState -> String) -> ([VarState] -> ShowS) -> Show VarState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VarState] -> ShowS
$cshowList :: [VarState] -> ShowS
show :: VarState -> String
$cshow :: VarState -> String
showsPrec :: Int -> VarState -> ShowS
$cshowsPrec :: Int -> VarState -> ShowS
Show, VarState -> VarState -> Bool
(VarState -> VarState -> Bool)
-> (VarState -> VarState -> Bool) -> Eq VarState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VarState -> VarState -> Bool
$c/= :: VarState -> VarState -> Bool
== :: VarState -> VarState -> Bool
$c== :: VarState -> VarState -> Bool
Eq)
type Lattice = Map AccessPath VarState
data FunctionSummary = FunctionSummary
{ FunctionSummary -> Maybe AccessPath
summaryReturnProvenance :: Maybe AccessPath
} deriving (Int -> FunctionSummary -> ShowS
[FunctionSummary] -> ShowS
FunctionSummary -> String
(Int -> FunctionSummary -> ShowS)
-> (FunctionSummary -> String)
-> ([FunctionSummary] -> ShowS)
-> Show FunctionSummary
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FunctionSummary] -> ShowS
$cshowList :: [FunctionSummary] -> ShowS
show :: FunctionSummary -> String
$cshow :: FunctionSummary -> String
showsPrec :: Int -> FunctionSummary -> ShowS
$cshowsPrec :: Int -> FunctionSummary -> ShowS
Show, FunctionSummary -> FunctionSummary -> Bool
(FunctionSummary -> FunctionSummary -> Bool)
-> (FunctionSummary -> FunctionSummary -> Bool)
-> Eq FunctionSummary
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FunctionSummary -> FunctionSummary -> Bool
$c/= :: FunctionSummary -> FunctionSummary -> Bool
== :: FunctionSummary -> FunctionSummary -> Bool
$c== :: FunctionSummary -> FunctionSummary -> Bool
Eq)
data Effect
= Move AccessPath NodeInfo
| Use AccessPath NodeInfo
| Define AccessPath NodeInfo
| Declare AccessPath NodeInfo
| SharedBorrow AccessPath AccessPath NodeInfo
| MutableBorrow AccessPath AccessPath NodeInfo
deriving (Int -> Effect -> ShowS
[Effect] -> ShowS
Effect -> String
(Int -> Effect -> ShowS)
-> (Effect -> String) -> ([Effect] -> ShowS) -> Show Effect
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Effect] -> ShowS
$cshowList :: [Effect] -> ShowS
show :: Effect -> String
$cshow :: Effect -> String
showsPrec :: Int -> Effect -> ShowS
$cshowsPrec :: Int -> Effect -> ShowS
Show, Effect -> Effect -> Bool
(Effect -> Effect -> Bool)
-> (Effect -> Effect -> Bool) -> Eq Effect
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Effect -> Effect -> Bool
$c/= :: Effect -> Effect -> Bool
== :: Effect -> Effect -> Bool
$c== :: Effect -> Effect -> Bool
Eq)
type NodeEffects = Map Node [Effect]
typeAttrs :: Type -> Attributes
typeAttrs :: Type -> Attributes
typeAttrs = \case
DirectType TypeName
_ TypeQuals
_ Attributes
a -> Attributes
a
PtrType Type
_ TypeQuals
_ Attributes
a -> Attributes
a
ArrayType Type
_ ArraySize
_ TypeQuals
_ Attributes
a -> Attributes
a
FunctionType FunType
_ Attributes
a -> Attributes
a
TypeDefType (TypeDefRef Ident
_ Type
t NodeInfo
_) TypeQuals
_ Attributes
a -> Attributes
a Attributes -> Attributes -> Attributes
forall a. [a] -> [a] -> [a]
++ Type -> Attributes
typeAttrs Type
t
idName :: Ident -> String
idName :: Ident -> String
idName (Ident String
name Int
_ NodeInfo
_) = String
name
isOwnedCAttr :: CAttribute a -> Bool
isOwnedCAttr :: CAttribute a -> Bool
isOwnedCAttr (CAttr Ident
i [CExpression a]
_ a
_) = Ident -> String
idName Ident
i String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"owned", String
"__owned__"]
isOwnedAttr :: Attr -> Bool
isOwnedAttr :: Attr -> Bool
isOwnedAttr (Attr Ident
i [Expr]
_ NodeInfo
_) = Ident -> String
idName Ident
i String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"owned", String
"__owned__"]
isOwned :: Type -> Bool
isOwned :: Type -> Bool
isOwned Type
ty = case Type
ty of
PtrType {} -> (Attr -> Bool) -> Attributes -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Attr -> Bool
isOwnedAttr (Type -> Attributes
typeAttrs Type
ty)
ArrayType {} -> (Attr -> Bool) -> Attributes -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Attr -> Bool
isOwnedAttr (Type -> Attributes
typeAttrs Type
ty)
TypeDefType (TypeDefRef Ident
_ Type
t' NodeInfo
_) TypeQuals
_ Attributes
_ -> Type -> Bool
isOwned Type
t'
Type
_ -> Bool
False
isPointerType :: Type -> Bool
isPointerType :: Type -> Bool
isPointerType Type
ty = case Type -> Type
canonicalType Type
ty of
PtrType {} -> Bool
True
ArrayType {} -> Bool
True
Type
_ -> Bool
False
isSpecPointer :: GlobalDecls -> CDeclarationSpecifier a -> Bool
isSpecPointer :: GlobalDecls -> CDeclarationSpecifier a -> Bool
isSpecPointer GlobalDecls
d (CTypeSpec (CTypeDef Ident
i a
_)) =
case Ident -> Map Ident TypeDef -> Maybe TypeDef
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
i (GlobalDecls -> Map Ident TypeDef
gTypeDefs GlobalDecls
d) of
Just (TypeDef Ident
_ Type
t Attributes
_ NodeInfo
_) -> Type -> Bool
isPointerType Type
t
Maybe TypeDef
_ -> Bool
False
isSpecPointer GlobalDecls
_ CDeclarationSpecifier a
_ = Bool
False
isCDeclrPointer :: CDeclarator a -> Bool
isCDeclrPointer :: CDeclarator a -> Bool
isCDeclrPointer (CDeclr Maybe Ident
_ [CDerivedDeclarator a]
derived Maybe (CStringLiteral a)
_ [CAttribute a]
_ a
_) = (CDerivedDeclarator a -> Bool) -> [CDerivedDeclarator a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CDerivedDeclarator a -> Bool
forall a. CDerivedDeclarator a -> Bool
isDerivedPointer [CDerivedDeclarator a]
derived
isNullPtr :: AccessPath -> Bool
isNullPtr :: AccessPath -> Bool
isNullPtr (PathVar String
"nullptr") = Bool
True
isNullPtr AccessPath
_ = Bool
False
isDerivedPointer :: CDerivedDeclarator a -> Bool
isDerivedPointer :: CDerivedDeclarator a -> Bool
isDerivedPointer (CPtrDeclr {}) = Bool
True
isDerivedPointer (CArrDeclr {}) = Bool
True
isDerivedPointer CDerivedDeclarator a
_ = Bool
False
isOwnedDecl :: Attributes -> Type -> Bool
isOwnedDecl :: Attributes -> Type -> Bool
isOwnedDecl Attributes
attrs Type
ty = (Attr -> Bool) -> Attributes -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Attr -> Bool
isOwnedAttr Attributes
attrs Bool -> Bool -> Bool
|| Type -> Bool
isOwned Type
ty
isOwnedSpec :: CDeclarationSpecifier a -> Bool
isOwnedSpec :: CDeclarationSpecifier a -> Bool
isOwnedSpec (CTypeQual (CAttrQual CAttribute a
attr)) = CAttribute a -> Bool
forall a. CAttribute a -> Bool
isOwnedCAttr CAttribute a
attr
isOwnedSpec CDeclarationSpecifier a
_ = Bool
False
isConstSpec :: CDeclarationSpecifier a -> Bool
isConstSpec :: CDeclarationSpecifier a -> Bool
isConstSpec (CTypeQual (CConstQual a
_)) = Bool
True
isConstSpec CDeclarationSpecifier a
_ = Bool
False
isTypeMutable :: Type -> Bool
isTypeMutable :: Type -> Bool
isTypeMutable = \case
DirectType TypeName
_ TypeQuals
q Attributes
_ -> Bool -> Bool
not (TypeQuals -> Bool
constant TypeQuals
q)
PtrType Type
t TypeQuals
_ Attributes
_ -> Type -> Bool
isTypeMutable Type
t
ArrayType Type
t ArraySize
_ TypeQuals
_ Attributes
_ -> Type -> Bool
isTypeMutable Type
t
FunctionType FunType
_ Attributes
_ -> Bool
False
TypeDefType (TypeDefRef Ident
_ Type
t NodeInfo
_) TypeQuals
q Attributes
_ -> Bool -> Bool
not (TypeQuals -> Bool
constant TypeQuals
q) Bool -> Bool -> Bool
&& Type -> Bool
isTypeMutable Type
t
isCDeclrOwned :: CDeclarator a -> Bool
isCDeclrOwned :: CDeclarator a -> Bool
isCDeclrOwned (CDeclr Maybe Ident
_ [CDerivedDeclarator a]
derived Maybe (CStringLiteral a)
_ [CAttribute a]
attrs a
_) =
(CAttribute a -> Bool) -> [CAttribute a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CAttribute a -> Bool
forall a. CAttribute a -> Bool
isOwnedCAttr [CAttribute a]
attrs Bool -> Bool -> Bool
|| (CDerivedDeclarator a -> Bool) -> [CDerivedDeclarator a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CDerivedDeclarator a -> Bool
forall a. CDerivedDeclarator a -> Bool
isDerivedOwned [CDerivedDeclarator a]
derived
isCDeclrOwnedMutable :: CDeclarator a -> Bool
isCDeclrOwnedMutable :: CDeclarator a -> Bool
isCDeclrOwnedMutable (CDeclr Maybe Ident
_ [CDerivedDeclarator a]
derived Maybe (CStringLiteral a)
_ [CAttribute a]
_ a
_) =
Bool -> Bool
not ((CDerivedDeclarator a -> Bool) -> [CDerivedDeclarator a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CDerivedDeclarator a -> Bool
forall a. CDerivedDeclarator a -> Bool
isDerivedConst [CDerivedDeclarator a]
derived)
isDerivedOwned :: CDerivedDeclarator a -> Bool
isDerivedOwned :: CDerivedDeclarator a -> Bool
isDerivedOwned (CPtrDeclr [CTypeQualifier a]
quals a
_) = (CTypeQualifier a -> Bool) -> [CTypeQualifier a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CTypeQualifier a -> Bool
forall a. CTypeQualifier a -> Bool
isQualOwned [CTypeQualifier a]
quals
isDerivedOwned (CArrDeclr [CTypeQualifier a]
quals CArraySize a
_ a
_) = (CTypeQualifier a -> Bool) -> [CTypeQualifier a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CTypeQualifier a -> Bool
forall a. CTypeQualifier a -> Bool
isQualOwned [CTypeQualifier a]
quals
isDerivedOwned (CFunDeclr Either [Ident] ([CDeclaration a], Bool)
_ [CAttribute a]
attrs a
_) = (CAttribute a -> Bool) -> [CAttribute a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CAttribute a -> Bool
forall a. CAttribute a -> Bool
isOwnedCAttr [CAttribute a]
attrs
isDerivedConst :: CDerivedDeclarator a -> Bool
isDerivedConst :: CDerivedDeclarator a -> Bool
isDerivedConst (CPtrDeclr [CTypeQualifier a]
quals a
_) = (CTypeQualifier a -> Bool) -> [CTypeQualifier a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CTypeQualifier a -> Bool
forall a. CTypeQualifier a -> Bool
isQualConst [CTypeQualifier a]
quals
isDerivedConst (CArrDeclr [CTypeQualifier a]
quals CArraySize a
_ a
_) = (CTypeQualifier a -> Bool) -> [CTypeQualifier a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CTypeQualifier a -> Bool
forall a. CTypeQualifier a -> Bool
isQualConst [CTypeQualifier a]
quals
isDerivedConst (CFunDeclr Either [Ident] ([CDeclaration a], Bool)
_ [CAttribute a]
_ a
_) = Bool
False
isQualOwned :: CTypeQualifier a -> Bool
isQualOwned :: CTypeQualifier a -> Bool
isQualOwned (CAttrQual CAttribute a
attr) = CAttribute a -> Bool
forall a. CAttribute a -> Bool
isOwnedCAttr CAttribute a
attr
isQualOwned CTypeQualifier a
_ = Bool
False
isQualConst :: CTypeQualifier a -> Bool
isQualConst :: CTypeQualifier a -> Bool
isQualConst (CConstQual a
_) = Bool
True
isQualConst CTypeQualifier a
_ = Bool
False
exprPath :: CExpression a -> Maybe AccessPath
exprPath :: CExpression a -> Maybe AccessPath
exprPath = \case
CVar Ident
i a
_ -> AccessPath -> Maybe AccessPath
forall a. a -> Maybe a
Just (String -> AccessPath
PathVar (Ident -> String
idName Ident
i))
CUnary CUnaryOp
CIndOp CExpression a
e a
_ -> AccessPath -> AccessPath
PathDeref (AccessPath -> AccessPath) -> Maybe AccessPath -> Maybe AccessPath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpression a -> Maybe AccessPath
forall a. CExpression a -> Maybe AccessPath
exprPath CExpression a
e
CUnary CUnaryOp
CAdrOp CExpression a
e a
_ -> CExpression a -> Maybe AccessPath
forall a. CExpression a -> Maybe AccessPath
exprPath CExpression a
e
CMember CExpression a
e Ident
i Bool
_ a
_ -> AccessPath -> String -> AccessPath
PathField (AccessPath -> String -> AccessPath)
-> Maybe AccessPath -> Maybe (String -> AccessPath)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpression a -> Maybe AccessPath
forall a. CExpression a -> Maybe AccessPath
exprPath CExpression a
e Maybe (String -> AccessPath) -> Maybe String -> Maybe AccessPath
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> Maybe String
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ident -> String
idName Ident
i)
CBinary CBinaryOp
_ CExpression a
l CExpression a
r a
_ -> CExpression a -> Maybe AccessPath
forall a. CExpression a -> Maybe AccessPath
exprPath CExpression a
l Maybe AccessPath -> Maybe AccessPath -> Maybe AccessPath
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` CExpression a -> Maybe AccessPath
forall a. CExpression a -> Maybe AccessPath
exprPath CExpression a
r
CExpression a
_ -> Maybe AccessPath
forall a. Maybe a
Nothing
borrowProblem :: NodeEffects -> Dataflow Node EdgeType Lattice
borrowProblem :: NodeEffects -> Dataflow Node EdgeType Lattice
borrowProblem NodeEffects
nodeEffects = Dataflow :: forall node edge state.
(node -> state -> state)
-> (node -> edge -> state -> state)
-> (state -> state -> state)
-> state
-> Dataflow node edge state
Dataflow
{ transfer :: Node -> Lattice -> Lattice
transfer = Node -> Lattice -> Lattice
transferFunc
, edgeTransfer :: Node -> EdgeType -> Lattice -> Lattice
edgeTransfer = \Node
_ EdgeType
_ Lattice
l -> (AccessPath -> VarState -> Bool) -> Lattice -> Lattice
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\AccessPath
k VarState
_ -> Bool -> Bool
not (AccessPath -> Bool
isTemporary AccessPath
k)) Lattice
l
, merge :: Lattice -> Lattice -> Lattice
merge = (VarState -> VarState -> VarState) -> Lattice -> Lattice -> Lattice
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith VarState -> VarState -> VarState
mergeVar
, initial :: Lattice
initial = Lattice
forall k a. Map k a
Map.empty
}
where
mergeVar :: VarState -> VarState -> VarState
mergeVar VarState
s1 VarState
s2 | VarState
s1 VarState -> VarState -> Bool
forall a. Eq a => a -> a -> Bool
== VarState
s2 = VarState
s1
mergeVar (StateInconsistent NodeInfo
ni NodeInfo
mi) VarState
_ = NodeInfo -> NodeInfo -> VarState
StateInconsistent NodeInfo
ni NodeInfo
mi
mergeVar VarState
_ (StateInconsistent NodeInfo
ni NodeInfo
mi) = NodeInfo -> NodeInfo -> VarState
StateInconsistent NodeInfo
ni NodeInfo
mi
mergeVar (StateOwned NodeInfo
ni) (StateMoved NodeInfo
mi) = NodeInfo -> NodeInfo -> VarState
StateInconsistent NodeInfo
ni NodeInfo
mi
mergeVar (StateMoved NodeInfo
mi) (StateOwned NodeInfo
ni) = NodeInfo -> NodeInfo -> VarState
StateInconsistent NodeInfo
ni NodeInfo
mi
mergeVar (StateOwned NodeInfo
ni) (StateSharedBorrowedFrom AccessPath
_ NodeInfo
mi) = NodeInfo -> NodeInfo -> VarState
StateInconsistent NodeInfo
ni NodeInfo
mi
mergeVar (StateSharedBorrowedFrom AccessPath
_ NodeInfo
mi) (StateOwned NodeInfo
ni) = NodeInfo -> NodeInfo -> VarState
StateInconsistent NodeInfo
ni NodeInfo
mi
mergeVar (StateOwned NodeInfo
ni) (StateMutableBorrowedFrom AccessPath
_ NodeInfo
mi) = NodeInfo -> NodeInfo -> VarState
StateInconsistent NodeInfo
ni NodeInfo
mi
mergeVar (StateMutableBorrowedFrom AccessPath
_ NodeInfo
mi) (StateOwned NodeInfo
ni) = NodeInfo -> NodeInfo -> VarState
StateInconsistent NodeInfo
ni NodeInfo
mi
mergeVar VarState
s1 VarState
s2 = NodeInfo -> NodeInfo -> VarState
StateInconsistent (VarState -> NodeInfo
getNi VarState
s1) (VarState -> NodeInfo
getNi VarState
s2)
getNi :: VarState -> NodeInfo
getNi (StateUninitialized NodeInfo
ni) = NodeInfo
ni
getNi (StateOwned NodeInfo
ni) = NodeInfo
ni
getNi (StateSharedBorrowedFrom AccessPath
_ NodeInfo
ni) = NodeInfo
ni
getNi (StateMutableBorrowedFrom AccessPath
_ NodeInfo
ni) = NodeInfo
ni
getNi (StateMoved NodeInfo
ni) = NodeInfo
ni
getNi (StateInconsistent NodeInfo
ni NodeInfo
_) = NodeInfo
ni
transferFunc :: Node -> Lattice -> Lattice
transferFunc :: Node -> Lattice -> Lattice
transferFunc Node
node Lattice
lat =
let effects :: [Effect]
effects = [Effect] -> Node -> NodeEffects -> [Effect]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] Node
node NodeEffects
nodeEffects
in (Lattice -> Effect -> Lattice) -> Lattice -> [Effect] -> Lattice
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Lattice -> Effect -> Lattice
applyEffect Lattice
lat [Effect]
effects
applyEffect :: Lattice -> Effect -> Lattice
applyEffect Lattice
l (Move AccessPath
i NodeInfo
ni) = AccessPath -> VarState -> Lattice -> Lattice
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert AccessPath
i (NodeInfo -> VarState
StateMoved NodeInfo
ni) Lattice
l
applyEffect Lattice
l (Define AccessPath
i NodeInfo
ni) = AccessPath -> VarState -> Lattice -> Lattice
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert AccessPath
i (NodeInfo -> VarState
StateOwned NodeInfo
ni) Lattice
l
applyEffect Lattice
l (Declare AccessPath
i NodeInfo
ni) = AccessPath -> VarState -> Lattice -> Lattice
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert AccessPath
i (NodeInfo -> VarState
StateUninitialized NodeInfo
ni) Lattice
l
applyEffect Lattice
l (SharedBorrow AccessPath
q AccessPath
p NodeInfo
ni) =
let origin :: AccessPath
origin = AccessPath -> Lattice -> AccessPath
findOrigin AccessPath
p Lattice
l
in AccessPath -> VarState -> Lattice -> Lattice
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert AccessPath
q (AccessPath -> NodeInfo -> VarState
StateSharedBorrowedFrom AccessPath
origin NodeInfo
ni) Lattice
l
applyEffect Lattice
l (MutableBorrow AccessPath
q AccessPath
p NodeInfo
ni) =
let origin :: AccessPath
origin = AccessPath -> Lattice -> AccessPath
findOrigin AccessPath
p Lattice
l
in AccessPath -> VarState -> Lattice -> Lattice
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert AccessPath
q (AccessPath -> NodeInfo -> VarState
StateMutableBorrowedFrom AccessPath
origin NodeInfo
ni) Lattice
l
applyEffect Lattice
l (Use AccessPath
_ NodeInfo
_) = Lattice
l
findOrigin :: AccessPath -> Lattice -> AccessPath
findOrigin :: AccessPath -> Lattice -> AccessPath
findOrigin AccessPath
p Lattice
l = Set AccessPath -> AccessPath -> AccessPath
findOrigin' Set AccessPath
forall a. Set a
Set.empty AccessPath
p
where
findOrigin' :: Set AccessPath -> AccessPath -> AccessPath
findOrigin' Set AccessPath
visited AccessPath
curr
| AccessPath
curr AccessPath -> Set AccessPath -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set AccessPath
visited = AccessPath
curr
| Bool
otherwise = case AccessPath -> Lattice -> Maybe VarState
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup AccessPath
curr Lattice
l of
Just (StateSharedBorrowedFrom AccessPath
x NodeInfo
_) -> Set AccessPath -> AccessPath -> AccessPath
findOrigin' (AccessPath -> Set AccessPath -> Set AccessPath
forall a. Ord a => a -> Set a -> Set a
Set.insert AccessPath
curr Set AccessPath
visited) AccessPath
x
Just (StateMutableBorrowedFrom AccessPath
x NodeInfo
_) -> Set AccessPath -> AccessPath -> AccessPath
findOrigin' (AccessPath -> Set AccessPath -> Set AccessPath
forall a. Ord a => a -> Set a -> Set a
Set.insert AccessPath
curr Set AccessPath
visited) AccessPath
x
Maybe VarState
_ -> AccessPath
curr
isTemporary :: AccessPath -> Bool
isTemporary :: AccessPath -> Bool
isTemporary = \case
PathParam {} -> Bool
True
AccessPath
PathReturn -> Bool
True
AccessPath
_ -> Bool
False
summariseFunction :: IdentDecl -> Maybe (String, FunctionSummary)
summariseFunction :: IdentDecl -> Maybe (String, FunctionSummary)
summariseFunction = \case
FunctionDef (FunDef (VarDecl (VarName (Ident -> String
idName -> String
name) Maybe AsmName
_) DeclAttrs
_ (FunctionType (FunType Type
_ [ParamDecl]
params Bool
_) Attributes
_)) (CCompound [Ident]
_ [CCompoundBlockItem NodeInfo]
items NodeInfo
_) NodeInfo
_) ->
let provenance :: Maybe AccessPath
provenance = [AccessPath] -> Maybe AccessPath
forall a. [a] -> Maybe a
listToMaybe ([AccessPath] -> Maybe AccessPath)
-> [AccessPath] -> Maybe AccessPath
forall a b. (a -> b) -> a -> b
$ (CCompoundBlockItem NodeInfo -> Maybe AccessPath)
-> [CCompoundBlockItem NodeInfo] -> [AccessPath]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ([ParamDecl] -> CCompoundBlockItem NodeInfo -> Maybe AccessPath
forall a. [ParamDecl] -> CCompoundBlockItem a -> Maybe AccessPath
findReturnProvenance [ParamDecl]
params) [CCompoundBlockItem NodeInfo]
items
in (String, FunctionSummary) -> Maybe (String, FunctionSummary)
forall a. a -> Maybe a
Just (String
name, Maybe AccessPath -> FunctionSummary
FunctionSummary Maybe AccessPath
provenance)
IdentDecl
_ -> Maybe (String, FunctionSummary)
forall a. Maybe a
Nothing
where
findReturnProvenance :: [ParamDecl] -> CCompoundBlockItem a -> Maybe AccessPath
findReturnProvenance [ParamDecl]
params = \case
CBlockStmt (CReturn (Just CExpression a
e) a
_) -> [ParamDecl] -> AccessPath -> AccessPath
mapToParam [ParamDecl]
params (AccessPath -> AccessPath) -> Maybe AccessPath -> Maybe AccessPath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CExpression a -> Maybe AccessPath
forall a. CExpression a -> Maybe AccessPath
exprPath CExpression a
e
CBlockStmt (CCompound [Ident]
_ [CCompoundBlockItem a]
bis a
_) -> [AccessPath] -> Maybe AccessPath
forall a. [a] -> Maybe a
listToMaybe ([AccessPath] -> Maybe AccessPath)
-> [AccessPath] -> Maybe AccessPath
forall a b. (a -> b) -> a -> b
$ (CCompoundBlockItem a -> Maybe AccessPath)
-> [CCompoundBlockItem a] -> [AccessPath]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ([ParamDecl] -> CCompoundBlockItem a -> Maybe AccessPath
findReturnProvenance [ParamDecl]
params) [CCompoundBlockItem a]
bis
CCompoundBlockItem a
_ -> Maybe AccessPath
forall a. Maybe a
Nothing
mapToParam :: [ParamDecl] -> AccessPath -> AccessPath
mapToParam [ParamDecl]
params p :: AccessPath
p@(PathVar String
v) =
case (ParamDecl -> Bool) -> [ParamDecl] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex (String -> ParamDecl -> Bool
isParam String
v) [ParamDecl]
params of
Just Int
i -> Int -> AccessPath
PathParam Int
i
Maybe Int
Nothing -> AccessPath
p
mapToParam [ParamDecl]
_ p :: AccessPath
p@PathParam{} = AccessPath
p
mapToParam [ParamDecl]
_ AccessPath
PathReturn = AccessPath
PathReturn
mapToParam [ParamDecl]
params (PathDeref AccessPath
p) = AccessPath -> AccessPath
PathDeref ([ParamDecl] -> AccessPath -> AccessPath
mapToParam [ParamDecl]
params AccessPath
p)
mapToParam [ParamDecl]
params (PathField AccessPath
p String
f) = AccessPath -> String -> AccessPath
PathField ([ParamDecl] -> AccessPath -> AccessPath
mapToParam [ParamDecl]
params AccessPath
p) String
f
mapToParam [ParamDecl]
params (PathIndex AccessPath
p String
i) = AccessPath -> String -> AccessPath
PathIndex ([ParamDecl] -> AccessPath -> AccessPath
mapToParam [ParamDecl]
params AccessPath
p) String
i
isParam :: String -> ParamDecl -> Bool
isParam String
v (ParamDecl (VarDecl (VarName (Ident -> String
idName -> String
name) Maybe AsmName
_) DeclAttrs
_ Type
_) NodeInfo
_) = String
name String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
v
isParam String
_ ParamDecl
_ = Bool
False
isExprMutable :: CExpression NodeInfo -> Trav Env Bool
isExprMutable :: Expr -> Trav Env Bool
isExprMutable Expr
expr = do
Type
t <- [StmtCtx] -> ExprSide -> Expr -> TravT Env Identity Type
forall (m :: * -> *).
MonadTrav m =>
[StmtCtx] -> ExprSide -> Expr -> m Type
tExpr [] ExprSide
RValue Expr
expr
Bool -> Trav Env Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Trav Env Bool) -> Bool -> Trav Env Bool
forall a b. (a -> b) -> a -> b
$ Type -> Bool
isTypeMutable Type
t
analyse :: GlobalDecls -> Trav Env ()
analyse :: GlobalDecls -> Trav Env ()
analyse GlobalDecls
decls = do
let summaries :: Map String FunctionSummary
summaries = [(String, FunctionSummary)] -> Map String FunctionSummary
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(String, FunctionSummary)] -> Map String FunctionSummary)
-> [(String, FunctionSummary)] -> Map String FunctionSummary
forall a b. (a -> b) -> a -> b
$ (IdentDecl -> Maybe (String, FunctionSummary))
-> [IdentDecl] -> [(String, FunctionSummary)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe IdentDecl -> Maybe (String, FunctionSummary)
summariseFunction (Map Ident IdentDecl -> [IdentDecl]
forall k a. Map k a -> [a]
Map.elems (Map Ident IdentDecl -> [IdentDecl])
-> Map Ident IdentDecl -> [IdentDecl]
forall a b. (a -> b) -> a -> b
$ GlobalDecls -> Map Ident IdentDecl
gObjs GlobalDecls
decls)
[IdentDecl] -> (IdentDecl -> Trav Env ()) -> Trav Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map Ident IdentDecl -> [IdentDecl]
forall k a. Map k a -> [a]
Map.elems (Map Ident IdentDecl -> [IdentDecl])
-> Map Ident IdentDecl -> [IdentDecl]
forall a b. (a -> b) -> a -> b
$ GlobalDecls -> Map Ident IdentDecl
gObjs GlobalDecls
decls) ((IdentDecl -> Trav Env ()) -> Trav Env ())
-> (IdentDecl -> Trav Env ()) -> Trav Env ()
forall a b. (a -> b) -> a -> b
$ \case
FunctionDef fd :: FunDef
fd@(FunDef (VarDecl (VarName Ident
_ Maybe AsmName
_) DeclAttrs
_ (FunctionType (FunType Type
_ [ParamDecl]
params Bool
_) Attributes
_)) CStatement NodeInfo
_ NodeInfo
_) -> do
let (Node
entry, CFG
cfg) = FunDef -> (Node, CFG)
fromFunDef FunDef
fd
let localDecls :: Map String (Bool, Bool)
localDecls = GlobalDecls -> FunDef -> Map String (Bool, Bool)
collectDecls GlobalDecls
decls FunDef
fd
NodeEffects
effects <- GlobalDecls
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> [Node]
-> TravT Env Identity NodeEffects
forall t.
t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> [Node]
-> TravT Env Identity NodeEffects
computeNodeEffects GlobalDecls
decls Map String FunctionSummary
summaries Map String (Bool, Bool)
localDecls (CFG -> [Node]
forall k a. Map k a -> [k]
Map.keys CFG
cfg)
let initialLat :: Lattice
initialLat = [(AccessPath, VarState)] -> Lattice
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (String -> AccessPath
PathVar (Ident -> String
idName Ident
name), NodeInfo -> VarState
StateOwned (Ident -> NodeInfo
forall a. CNode a => a -> NodeInfo
nodeInfo Ident
name)) | ParamDecl (VarDecl (VarName Ident
name Maybe AsmName
_) (DeclAttrs FunctionAttrs
_ Storage
_ Attributes
attrs) Type
t) NodeInfo
_ <- [ParamDecl]
params, Attributes -> Type -> Bool
isOwnedDecl Attributes
attrs Type
t ]
let problem :: Dataflow Node EdgeType Lattice
problem = (NodeEffects -> Dataflow Node EdgeType Lattice
borrowProblem NodeEffects
effects) { initial :: Lattice
initial = Lattice
initialLat }
let result :: Map Node Lattice
result = Node -> CFG -> Dataflow Node EdgeType Lattice -> Map Node Lattice
forall node state edge.
(Ord node, Eq state) =>
node
-> Map node [(edge, node)]
-> Dataflow node edge state
-> Map node state
solve Node
entry CFG
cfg Dataflow Node EdgeType Lattice
problem
let live :: Map Node (Set AccessPath)
live = Map String (Bool, Bool)
-> [Node] -> CFG -> Map Node (Set AccessPath)
forall a.
Map String a -> [Node] -> CFG -> Map Node (Set AccessPath)
liveness Map String (Bool, Bool)
localDecls [Int -> NodeKind -> Node
Node Int
0 NodeKind
ExitNode] CFG
cfg
let isExpectedOwned :: AccessPath -> Bool
isExpectedOwned AccessPath
var = case AccessPath
var of
PathVar String
name -> Bool -> ((Bool, Bool) -> Bool) -> Maybe (Bool, Bool) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool, Bool) -> Bool
forall a b. (a, b) -> a
fst (String -> Map String (Bool, Bool) -> Maybe (Bool, Bool)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
name Map String (Bool, Bool)
localDecls)
AccessPath
PathReturn -> Bool
True
AccessPath
_ -> Bool
False
(AccessPath -> Bool)
-> Map Node (Set AccessPath)
-> NodeEffects
-> Map Node Lattice
-> Trav Env ()
forall k.
Ord k =>
(AccessPath -> Bool)
-> Map k (Set AccessPath)
-> Map k [Effect]
-> Map k Lattice
-> Trav Env ()
reportErrors AccessPath -> Bool
isExpectedOwned Map Node (Set AccessPath)
live NodeEffects
effects Map Node Lattice
result
(AccessPath -> Bool)
-> Map String (Bool, Bool)
-> NodeEffects
-> (Node -> Lattice -> Lattice)
-> Map Node Lattice
-> Trav Env ()
forall p p.
(AccessPath -> Bool)
-> p
-> p
-> (Node -> Lattice -> Lattice)
-> Map Node Lattice
-> Trav Env ()
checkLeaks AccessPath -> Bool
isExpectedOwned Map String (Bool, Bool)
localDecls NodeEffects
effects (Dataflow Node EdgeType Lattice -> Node -> Lattice -> Lattice
forall node edge state.
Dataflow node edge state -> node -> state -> state
transfer Dataflow Node EdgeType Lattice
problem) Map Node Lattice
result
IdentDecl
_ -> () -> Trav Env ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
collectDecls :: GlobalDecls -> FunDef -> Map String (Bool, Bool)
collectDecls GlobalDecls
d (FunDef (VarDecl VarName
_ DeclAttrs
_ (FunctionType (FunType Type
_ [ParamDecl]
params Bool
_) Attributes
_)) (CCompound [Ident]
_ [CCompoundBlockItem NodeInfo]
items NodeInfo
_) NodeInfo
_) =
let fromParams :: [(String, (Bool, Bool))]
fromParams = [ (Ident -> String
idName Ident
name, (Attributes -> Type -> Bool
isOwnedDecl Attributes
attrs Type
t, Type -> Bool
isPointerType Type
t)) | ParamDecl (VarDecl (VarName Ident
name Maybe AsmName
_) (DeclAttrs FunctionAttrs
_ Storage
_ Attributes
attrs) Type
t) NodeInfo
_ <- [ParamDecl]
params ]
fromItems :: [(String, (Bool, Bool))]
fromItems = (CCompoundBlockItem NodeInfo -> [(String, (Bool, Bool))])
-> [CCompoundBlockItem NodeInfo] -> [(String, (Bool, Bool))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (GlobalDecls
-> CCompoundBlockItem NodeInfo -> [(String, (Bool, Bool))]
forall a.
GlobalDecls -> CCompoundBlockItem a -> [(String, (Bool, Bool))]
collectBlockItemDecls GlobalDecls
d) [CCompoundBlockItem NodeInfo]
items
in [(String, (Bool, Bool))] -> Map String (Bool, Bool)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(String, (Bool, Bool))]
fromParams [(String, (Bool, Bool))]
-> [(String, (Bool, Bool))] -> [(String, (Bool, Bool))]
forall a. [a] -> [a] -> [a]
++ [(String, (Bool, Bool))]
fromItems)
collectDecls GlobalDecls
_ FunDef
_ = Map String (Bool, Bool)
forall k a. Map k a
Map.empty
collectBlockItemDecls :: GlobalDecls -> CCompoundBlockItem a -> [(String, (Bool, Bool))]
collectBlockItemDecls GlobalDecls
d = \case
CBlockStmt CStatement a
s -> GlobalDecls -> CStatement a -> [(String, (Bool, Bool))]
collectStatDecls GlobalDecls
d CStatement a
s
CBlockDecl (CDecl [CDeclarationSpecifier a]
specs [(Maybe (CDeclarator a), Maybe (CInitializer a),
Maybe (CExpression a))]
ds a
_) -> GlobalDecls
-> [CDeclarationSpecifier a]
-> [(Maybe (CDeclarator a), Maybe (CInitializer a),
Maybe (CExpression a))]
-> [(String, (Bool, Bool))]
forall (t :: * -> *) a a b c.
Foldable t =>
GlobalDecls
-> t (CDeclarationSpecifier a)
-> [(Maybe (CDeclarator a), b, c)]
-> [(String, (Bool, Bool))]
collectSingleDecl GlobalDecls
d [CDeclarationSpecifier a]
specs [(Maybe (CDeclarator a), Maybe (CInitializer a),
Maybe (CExpression a))]
ds
CCompoundBlockItem a
_ -> []
collectSingleDecl :: GlobalDecls
-> t (CDeclarationSpecifier a)
-> [(Maybe (CDeclarator a), b, c)]
-> [(String, (Bool, Bool))]
collectSingleDecl GlobalDecls
d t (CDeclarationSpecifier a)
specs [(Maybe (CDeclarator a), b, c)]
ds =
let declOwned :: Bool
declOwned = (CDeclarationSpecifier a -> Bool)
-> t (CDeclarationSpecifier a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CDeclarationSpecifier a -> Bool
forall a. CDeclarationSpecifier a -> Bool
isOwnedSpec t (CDeclarationSpecifier a)
specs
specsPtr :: Bool
specsPtr = (CDeclarationSpecifier a -> Bool)
-> t (CDeclarationSpecifier a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (GlobalDecls -> CDeclarationSpecifier a -> Bool
forall a. GlobalDecls -> CDeclarationSpecifier a -> Bool
isSpecPointer GlobalDecls
d) t (CDeclarationSpecifier a)
specs
in ((Maybe (CDeclarator a), b, c) -> Maybe (String, (Bool, Bool)))
-> [(Maybe (CDeclarator a), b, c)] -> [(String, (Bool, Bool))]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\case
(Just declr :: CDeclarator a
declr@(CDeclr (Just Ident
i) [CDerivedDeclarator a]
_ Maybe (CStringLiteral a)
_ [CAttribute a]
_ a
_), b
_, c
_) ->
(String, (Bool, Bool)) -> Maybe (String, (Bool, Bool))
forall a. a -> Maybe a
Just (Ident -> String
idName Ident
i, (Bool
declOwned Bool -> Bool -> Bool
|| CDeclarator a -> Bool
forall a. CDeclarator a -> Bool
isCDeclrOwned CDeclarator a
declr, Bool
specsPtr Bool -> Bool -> Bool
|| CDeclarator a -> Bool
forall a. CDeclarator a -> Bool
isCDeclrPointer CDeclarator a
declr))
(Maybe (CDeclarator a), b, c)
_ -> Maybe (String, (Bool, Bool))
forall a. Maybe a
Nothing) [(Maybe (CDeclarator a), b, c)]
ds
collectStatDecls :: GlobalDecls -> CStatement a -> [(String, (Bool, Bool))]
collectStatDecls GlobalDecls
d = \case
CCompound [Ident]
_ [CCompoundBlockItem a]
items a
_ -> (CCompoundBlockItem a -> [(String, (Bool, Bool))])
-> [CCompoundBlockItem a] -> [(String, (Bool, Bool))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (GlobalDecls -> CCompoundBlockItem a -> [(String, (Bool, Bool))]
collectBlockItemDecls GlobalDecls
d) [CCompoundBlockItem a]
items
CIf CExpression a
_ CStatement a
t Maybe (CStatement a)
e a
_ -> GlobalDecls -> CStatement a -> [(String, (Bool, Bool))]
collectStatDecls GlobalDecls
d CStatement a
t [(String, (Bool, Bool))]
-> [(String, (Bool, Bool))] -> [(String, (Bool, Bool))]
forall a. [a] -> [a] -> [a]
++ [(String, (Bool, Bool))]
-> (CStatement a -> [(String, (Bool, Bool))])
-> Maybe (CStatement a)
-> [(String, (Bool, Bool))]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (GlobalDecls -> CStatement a -> [(String, (Bool, Bool))]
collectStatDecls GlobalDecls
d) Maybe (CStatement a)
e
CWhile CExpression a
_ CStatement a
s Bool
_ a
_ -> GlobalDecls -> CStatement a -> [(String, (Bool, Bool))]
collectStatDecls GlobalDecls
d CStatement a
s
CFor Either (Maybe (CExpression a)) (CDeclaration a)
init' Maybe (CExpression a)
_ Maybe (CExpression a)
_ CStatement a
s a
_ ->
let fromInit :: [(String, (Bool, Bool))]
fromInit = case Either (Maybe (CExpression a)) (CDeclaration a)
init' of
Right CDeclaration a
dc -> GlobalDecls -> CCompoundBlockItem a -> [(String, (Bool, Bool))]
collectBlockItemDecls GlobalDecls
d (CDeclaration a -> CCompoundBlockItem a
forall a. CDeclaration a -> CCompoundBlockItem a
CBlockDecl CDeclaration a
dc)
Either (Maybe (CExpression a)) (CDeclaration a)
_ -> []
in [(String, (Bool, Bool))]
fromInit [(String, (Bool, Bool))]
-> [(String, (Bool, Bool))] -> [(String, (Bool, Bool))]
forall a. [a] -> [a] -> [a]
++ GlobalDecls -> CStatement a -> [(String, (Bool, Bool))]
collectStatDecls GlobalDecls
d CStatement a
s
CSwitch CExpression a
_ CStatement a
s a
_ -> GlobalDecls -> CStatement a -> [(String, (Bool, Bool))]
collectStatDecls GlobalDecls
d CStatement a
s
CStatement a
_ -> []
computeNodeEffects :: t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> [Node]
-> TravT Env Identity NodeEffects
computeNodeEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls [Node]
nodes = do
[(Node, [Effect])]
effectList <- [Node]
-> (Node -> TravT Env Identity (Node, [Effect]))
-> TravT Env Identity [(Node, [Effect])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Node]
nodes ((Node -> TravT Env Identity (Node, [Effect]))
-> TravT Env Identity [(Node, [Effect])])
-> (Node -> TravT Env Identity (Node, [Effect]))
-> TravT Env Identity [(Node, [Effect])]
forall a b. (a -> b) -> a -> b
$ \Node
node -> do
[Effect]
effs <- case Node
node of
Node Int
_ (StatNode CStatement NodeInfo
st) -> t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> CStatement NodeInfo
-> TravT Env Identity [Effect]
forall t.
t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> CStatement NodeInfo
-> TravT Env Identity [Effect]
collectStatEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls CStatement NodeInfo
st
Node Int
_ (ExprNode Expr
e) -> t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Expr
-> TravT Env Identity [Effect]
forall t.
t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Expr
-> TravT Env Identity [Effect]
collectExprEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
forall a. Maybe a
Nothing Expr
e
Node Int
_ (DeclNode CDecl
dc) -> t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> CDecl
-> TravT Env Identity [Effect]
forall t.
t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> CDecl
-> TravT Env Identity [Effect]
collectDeclEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls CDecl
dc
Node Int
_ (BranchNode Expr
e) -> t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Expr
-> TravT Env Identity [Effect]
forall t.
t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Expr
-> TravT Env Identity [Effect]
collectExprEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
forall a. Maybe a
Nothing Expr
e
Node
_ -> [Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return []
(Node, [Effect]) -> TravT Env Identity (Node, [Effect])
forall (m :: * -> *) a. Monad m => a -> m a
return (Node
node, [Effect]
effs)
NodeEffects -> TravT Env Identity NodeEffects
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeEffects -> TravT Env Identity NodeEffects)
-> NodeEffects -> TravT Env Identity NodeEffects
forall a b. (a -> b) -> a -> b
$ [(Node, [Effect])] -> NodeEffects
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Node, [Effect])]
effectList
collectStatEffects :: t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> CStatement NodeInfo
-> TravT Env Identity [Effect]
collectStatEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls = \case
CExpr (Just Expr
e) NodeInfo
_ -> t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Expr
-> TravT Env Identity [Effect]
forall t.
t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Expr
-> TravT Env Identity [Effect]
collectExprEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
forall a. Maybe a
Nothing Expr
e
CReturn (Just Expr
e) NodeInfo
_ -> t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Bool
-> Expr
-> TravT Env Identity [Effect]
forall t.
t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Bool
-> Expr
-> TravT Env Identity [Effect]
collectMoveEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
forall a. Maybe a
Nothing Bool
True Expr
e
CCompound [Ident]
_ [CCompoundBlockItem NodeInfo]
items NodeInfo
_ -> [[Effect]] -> [Effect]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Effect]] -> [Effect])
-> TravT Env Identity [[Effect]] -> TravT Env Identity [Effect]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CCompoundBlockItem NodeInfo -> TravT Env Identity [Effect])
-> [CCompoundBlockItem NodeInfo] -> TravT Env Identity [[Effect]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> CCompoundBlockItem NodeInfo
-> TravT Env Identity [Effect]
collectItemEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls) [CCompoundBlockItem NodeInfo]
items
CIf Expr
c CStatement NodeInfo
t Maybe (CStatement NodeInfo)
e NodeInfo
_ -> do
[Effect]
ce <- t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Expr
-> TravT Env Identity [Effect]
forall t.
t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Expr
-> TravT Env Identity [Effect]
collectExprEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
forall a. Maybe a
Nothing Expr
c
[Effect]
te <- t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> CStatement NodeInfo
-> TravT Env Identity [Effect]
collectStatEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls CStatement NodeInfo
t
[Effect]
ee <- TravT Env Identity [Effect]
-> (CStatement NodeInfo -> TravT Env Identity [Effect])
-> Maybe (CStatement NodeInfo)
-> TravT Env Identity [Effect]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return []) (t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> CStatement NodeInfo
-> TravT Env Identity [Effect]
collectStatEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls) Maybe (CStatement NodeInfo)
e
[Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Effect] -> TravT Env Identity [Effect])
-> [Effect] -> TravT Env Identity [Effect]
forall a b. (a -> b) -> a -> b
$ [Effect]
ce [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++ [Effect]
te [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++ [Effect]
ee
CStatement NodeInfo
_ -> [Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return []
collectItemEffects :: t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> CCompoundBlockItem NodeInfo
-> TravT Env Identity [Effect]
collectItemEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls = \case
CBlockStmt CStatement NodeInfo
st -> t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> CStatement NodeInfo
-> TravT Env Identity [Effect]
collectStatEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls CStatement NodeInfo
st
CBlockDecl CDecl
dc -> t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> CDecl
-> TravT Env Identity [Effect]
forall t.
t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> CDecl
-> TravT Env Identity [Effect]
collectDeclEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls CDecl
dc
CCompoundBlockItem NodeInfo
_ -> [Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return []
collectDeclEffects :: t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> CDecl
-> TravT Env Identity [Effect]
collectDeclEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls = \case
CDecl [CDeclarationSpecifier NodeInfo]
specs [(Maybe (CDeclarator NodeInfo), Maybe (CInitializer NodeInfo),
Maybe Expr)]
ds NodeInfo
_ ->
let declOwned :: Bool
declOwned = (CDeclarationSpecifier NodeInfo -> Bool)
-> [CDeclarationSpecifier NodeInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CDeclarationSpecifier NodeInfo -> Bool
forall a. CDeclarationSpecifier a -> Bool
isOwnedSpec [CDeclarationSpecifier NodeInfo]
specs
isConst :: Bool
isConst = (CDeclarationSpecifier NodeInfo -> Bool)
-> [CDeclarationSpecifier NodeInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CDeclarationSpecifier NodeInfo -> Bool
forall a. CDeclarationSpecifier a -> Bool
isConstSpec [CDeclarationSpecifier NodeInfo]
specs
in [[Effect]] -> [Effect]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Effect]] -> [Effect])
-> TravT Env Identity [[Effect]] -> TravT Env Identity [Effect]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Maybe (CDeclarator NodeInfo), Maybe (CInitializer NodeInfo),
Maybe Expr)]
-> ((Maybe (CDeclarator NodeInfo), Maybe (CInitializer NodeInfo),
Maybe Expr)
-> TravT Env Identity [Effect])
-> TravT Env Identity [[Effect]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Maybe (CDeclarator NodeInfo), Maybe (CInitializer NodeInfo),
Maybe Expr)]
ds (\case
(Just declr :: CDeclarator NodeInfo
declr@(CDeclr (Just Ident
i) [CDerivedDeclarator NodeInfo]
_ Maybe AsmName
_ [CAttribute NodeInfo]
_ NodeInfo
niDecl), Maybe (CInitializer NodeInfo)
mInit, Maybe Expr
_) -> do
let owned :: Bool
owned = Bool
declOwned Bool -> Bool -> Bool
|| CDeclarator NodeInfo -> Bool
forall a. CDeclarator a -> Bool
isCDeclrOwned CDeclarator NodeInfo
declr
let mutable :: Bool
mutable = Bool -> Bool
not Bool
isConst Bool -> Bool -> Bool
&& CDeclarator NodeInfo -> Bool
forall a. CDeclarator a -> Bool
isCDeclrOwnedMutable CDeclarator NodeInfo
declr
let pl :: AccessPath
pl = String -> AccessPath
PathVar (Ident -> String
idName Ident
i)
case Maybe (CInitializer NodeInfo)
mInit of
Just (CInitExpr Expr
e NodeInfo
_) -> do
Bool
lp <- Map String (Bool, Bool) -> Ident -> Trav Env Bool
forall (m :: * -> *) a.
(MonadCError m, MonadSymtab m) =>
Map String (a, Bool) -> Ident -> m Bool
isPointerDecl Map String (Bool, Bool)
localDecls Ident
i
let mBorrow :: Maybe (AccessPath, Bool)
mBorrow = if Bool
lp then (AccessPath, Bool) -> Maybe (AccessPath, Bool)
forall a. a -> Maybe a
Just (AccessPath
pl, Bool
mutable) else Maybe (AccessPath, Bool)
forall a. Maybe a
Nothing
[Effect]
re <- t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Bool
-> Expr
-> TravT Env Identity [Effect]
forall t.
t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Bool
-> Expr
-> TravT Env Identity [Effect]
collectMoveEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
mBorrow Bool
owned Expr
e
Bool
ro <- Map String (Bool, Bool) -> Expr -> Trav Env Bool
forall (m :: * -> *) b.
MonadTrav m =>
Map String (Bool, b) -> Expr -> m Bool
isExprOwned Map String (Bool, Bool)
localDecls Expr
e
let defEff :: [Effect]
defEff = if Bool
ro Bool -> Bool -> Bool
&& (Bool
owned Bool -> Bool -> Bool
|| Maybe AccessPath -> Bool
forall a. Maybe a -> Bool
isNothing (Expr -> Maybe AccessPath
forall a. CExpression a -> Maybe AccessPath
exprPath Expr
e)) then [AccessPath -> NodeInfo -> Effect
Define AccessPath
pl NodeInfo
niDecl] else []
let leakEff :: [Effect]
leakEff = if Bool
owned Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
ro then [AccessPath -> NodeInfo -> Effect
Define AccessPath
pl NodeInfo
niDecl, AccessPath -> NodeInfo -> Effect
Move AccessPath
pl NodeInfo
niDecl] else []
[Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Effect] -> TravT Env Identity [Effect])
-> [Effect] -> TravT Env Identity [Effect]
forall a b. (a -> b) -> a -> b
$ [Effect]
re [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++ [Effect]
defEff [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++ [Effect]
leakEff
Just (CInitList CInitializerList NodeInfo
_ NodeInfo
_) -> [Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return []
Maybe (CInitializer NodeInfo)
Nothing ->
if Bool
owned
then [Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return [AccessPath -> NodeInfo -> Effect
Declare AccessPath
pl NodeInfo
niDecl]
else [Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return []
(Maybe (CDeclarator NodeInfo), Maybe (CInitializer NodeInfo),
Maybe Expr)
_ -> [Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return []
)
CStaticAssert {} -> [Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return []
collectExprEffects :: t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Expr
-> TravT Env Identity [Effect]
collectExprEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
mBorrow Expr
expr = case Expr
expr of
CVar Ident
i NodeInfo
ni -> do
let p :: AccessPath
p = String -> AccessPath
PathVar (Ident -> String
idName Ident
i)
let borrowEff :: [Effect]
borrowEff = case Maybe (AccessPath, Bool)
mBorrow of
Just (dest, mut) | Bool -> Bool
not (AccessPath -> Bool
isNullPtr AccessPath
p) -> [if Bool
mut then AccessPath -> AccessPath -> NodeInfo -> Effect
MutableBorrow AccessPath
dest AccessPath
p NodeInfo
ni else AccessPath -> AccessPath -> NodeInfo -> Effect
SharedBorrow AccessPath
dest AccessPath
p NodeInfo
ni]
Maybe (AccessPath, Bool)
_ -> []
[Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Effect] -> TravT Env Identity [Effect])
-> [Effect] -> TravT Env Identity [Effect]
forall a b. (a -> b) -> a -> b
$ (AccessPath -> NodeInfo -> Effect
Use AccessPath
p NodeInfo
ni Effect -> [Effect] -> [Effect]
forall a. a -> [a] -> [a]
:) [Effect]
borrowEff
CUnary CUnaryOp
CIndOp Expr
e NodeInfo
ni -> do
[Effect]
ee <- t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Expr
-> TravT Env Identity [Effect]
collectExprEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
forall a. Maybe a
Nothing Expr
e
case Expr -> Maybe AccessPath
forall a. CExpression a -> Maybe AccessPath
exprPath Expr
expr of
Just AccessPath
p -> do
let borrowEff :: [Effect]
borrowEff = case Maybe (AccessPath, Bool)
mBorrow of
Just (dest, mut) | Bool -> Bool
not (AccessPath -> Bool
isNullPtr AccessPath
p) -> [if Bool
mut then AccessPath -> AccessPath -> NodeInfo -> Effect
MutableBorrow AccessPath
dest AccessPath
p NodeInfo
ni else AccessPath -> AccessPath -> NodeInfo -> Effect
SharedBorrow AccessPath
dest AccessPath
p NodeInfo
ni]
Maybe (AccessPath, Bool)
_ -> []
[Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Effect] -> TravT Env Identity [Effect])
-> [Effect] -> TravT Env Identity [Effect]
forall a b. (a -> b) -> a -> b
$ ([Effect]
ee [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++) ([Effect] -> [Effect])
-> ([Effect] -> [Effect]) -> [Effect] -> [Effect]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AccessPath -> NodeInfo -> Effect
Use AccessPath
p NodeInfo
ni Effect -> [Effect] -> [Effect]
forall a. a -> [a] -> [a]
:) ([Effect] -> [Effect]) -> [Effect] -> [Effect]
forall a b. (a -> b) -> a -> b
$ [Effect]
borrowEff
Maybe AccessPath
Nothing -> [Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return [Effect]
ee
CMember Expr
e Ident
_ Bool
_ NodeInfo
ni -> do
[Effect]
ee <- t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Expr
-> TravT Env Identity [Effect]
collectExprEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
forall a. Maybe a
Nothing Expr
e
case Expr -> Maybe AccessPath
forall a. CExpression a -> Maybe AccessPath
exprPath Expr
expr of
Just AccessPath
p -> do
let borrowEff :: [Effect]
borrowEff = case Maybe (AccessPath, Bool)
mBorrow of
Just (dest, mut) | Bool -> Bool
not (AccessPath -> Bool
isNullPtr AccessPath
p) -> [if Bool
mut then AccessPath -> AccessPath -> NodeInfo -> Effect
MutableBorrow AccessPath
dest AccessPath
p NodeInfo
ni else AccessPath -> AccessPath -> NodeInfo -> Effect
SharedBorrow AccessPath
dest AccessPath
p NodeInfo
ni]
Maybe (AccessPath, Bool)
_ -> []
[Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Effect] -> TravT Env Identity [Effect])
-> [Effect] -> TravT Env Identity [Effect]
forall a b. (a -> b) -> a -> b
$ ([Effect]
ee [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++) ([Effect] -> [Effect])
-> ([Effect] -> [Effect]) -> [Effect] -> [Effect]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AccessPath -> NodeInfo -> Effect
Use AccessPath
p NodeInfo
ni Effect -> [Effect] -> [Effect]
forall a. a -> [a] -> [a]
:) ([Effect] -> [Effect]) -> [Effect] -> [Effect]
forall a b. (a -> b) -> a -> b
$ [Effect]
borrowEff
Maybe AccessPath
Nothing -> [Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return [Effect]
ee
CUnary CUnaryOp
CAdrOp Expr
e NodeInfo
ni -> do
[Effect]
ee <- t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Expr
-> TravT Env Identity [Effect]
collectExprEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
forall a. Maybe a
Nothing Expr
e
case Expr -> Maybe AccessPath
forall a. CExpression a -> Maybe AccessPath
exprPath Expr
e of
Just AccessPath
p -> do
let borrowEff :: [Effect]
borrowEff = case Maybe (AccessPath, Bool)
mBorrow of
Just (dest, mut) | Bool -> Bool
not (AccessPath -> Bool
isNullPtr AccessPath
p) -> [if Bool
mut then AccessPath -> AccessPath -> NodeInfo -> Effect
MutableBorrow AccessPath
dest AccessPath
p NodeInfo
ni else AccessPath -> AccessPath -> NodeInfo -> Effect
SharedBorrow AccessPath
dest AccessPath
p NodeInfo
ni]
Maybe (AccessPath, Bool)
_ -> []
[Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Effect] -> TravT Env Identity [Effect])
-> [Effect] -> TravT Env Identity [Effect]
forall a b. (a -> b) -> a -> b
$ ([Effect]
ee [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++) ([Effect] -> [Effect])
-> ([Effect] -> [Effect]) -> [Effect] -> [Effect]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AccessPath -> NodeInfo -> Effect
Use AccessPath
p NodeInfo
ni Effect -> [Effect] -> [Effect]
forall a. a -> [a] -> [a]
:) ([Effect] -> [Effect]) -> [Effect] -> [Effect]
forall a b. (a -> b) -> a -> b
$ [Effect]
borrowEff
Maybe AccessPath
Nothing -> [Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return [Effect]
ee
CCall Expr
f [Expr]
args NodeInfo
ni -> do
Type
fTy <- [StmtCtx] -> ExprSide -> Expr -> TravT Env Identity Type
forall (m :: * -> *).
MonadTrav m =>
[StmtCtx] -> ExprSide -> Expr -> m Type
tExpr [] ExprSide
RValue Expr
f
let ([Bool]
paramOwned, [Bool]
paramMutable, [Bool]
paramIsPtr, Bool
rtOwned) = case Type
fTy of
FunctionType (FunType Type
rt [ParamDecl]
ps Bool
_) Attributes
_ -> ((ParamDecl -> Bool) -> [ParamDecl] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map ParamDecl -> Bool
isParamOwned [ParamDecl]
ps, (ParamDecl -> Bool) -> [ParamDecl] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map ParamDecl -> Bool
isParamMutable [ParamDecl]
ps, (ParamDecl -> Bool) -> [ParamDecl] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map ParamDecl -> Bool
isParamPointer [ParamDecl]
ps, Type -> Bool
isOwned Type
rt)
FunctionType (FunTypeIncomplete Type
rt) Attributes
_ -> ([], [], [], Type -> Bool
isOwned Type
rt)
PtrType (Type -> Type
canonicalType -> FunctionType (FunType Type
rt [ParamDecl]
ps Bool
_) Attributes
_) TypeQuals
_ Attributes
_ -> ((ParamDecl -> Bool) -> [ParamDecl] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map ParamDecl -> Bool
isParamOwned [ParamDecl]
ps, (ParamDecl -> Bool) -> [ParamDecl] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map ParamDecl -> Bool
isParamMutable [ParamDecl]
ps, (ParamDecl -> Bool) -> [ParamDecl] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map ParamDecl -> Bool
isParamPointer [ParamDecl]
ps, Type -> Bool
isOwned Type
rt)
PtrType (Type -> Type
canonicalType -> FunctionType (FunTypeIncomplete Type
rt) Attributes
_) TypeQuals
_ Attributes
_ -> ([], [], [], Type -> Bool
isOwned Type
rt)
Type
_ -> ([], [], [], Bool
False)
[[Effect]]
argEffs <- [(Int, Expr, Bool)]
-> ((Int, Expr, Bool) -> TravT Env Identity [Effect])
-> TravT Env Identity [[Effect]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Int] -> [Expr] -> [Bool] -> [(Int, Expr, Bool)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Int
0..] [Expr]
args [Bool]
paramOwned) (((Int, Expr, Bool) -> TravT Env Identity [Effect])
-> TravT Env Identity [[Effect]])
-> ((Int, Expr, Bool) -> TravT Env Identity [Effect])
-> TravT Env Identity [[Effect]]
forall a b. (a -> b) -> a -> b
$ \(Int
i, Expr
arg, Bool
owned) ->
let isPtr :: Bool
isPtr = Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
False ([Bool] -> Maybe Bool
forall a. [a] -> Maybe a
listToMaybe (Int -> [Bool] -> [Bool]
forall a. Int -> [a] -> [a]
drop Int
i [Bool]
paramIsPtr))
mArgBorrow :: Maybe (AccessPath, Bool)
mArgBorrow = if Bool -> Bool
not Bool
owned Bool -> Bool -> Bool
&& Bool
isPtr then (AccessPath, Bool) -> Maybe (AccessPath, Bool)
forall a. a -> Maybe a
Just (Int -> AccessPath
PathParam Int
i, Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
False ([Bool] -> Maybe Bool
forall a. [a] -> Maybe a
listToMaybe (Int -> [Bool] -> [Bool]
forall a. Int -> [a] -> [a]
drop Int
i [Bool]
paramMutable))) else Maybe (AccessPath, Bool)
forall a. Maybe a
Nothing
in t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Bool
-> Expr
-> TravT Env Identity [Effect]
collectMoveEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
mArgBorrow Bool
owned Expr
arg
let effs :: [Effect]
effs = [[Effect]] -> [Effect]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Effect]]
argEffs
let destInfo :: Maybe AccessPath
destInfo = case Maybe (AccessPath, Bool)
mBorrow of
Just (dest, _) -> AccessPath -> Maybe AccessPath
forall a. a -> Maybe a
Just AccessPath
dest
Maybe (AccessPath, Bool)
Nothing -> Maybe AccessPath
forall a. Maybe a
Nothing
let dest :: AccessPath
dest = AccessPath -> Maybe AccessPath -> AccessPath
forall a. a -> Maybe a -> a
fromMaybe AccessPath
PathReturn Maybe AccessPath
destInfo
let ([Effect]
provEffs, Bool
rtOwnedActual) = case Expr
f of
CVar (Ident String
name Int
_ NodeInfo
_) NodeInfo
_ -> case String -> Map String FunctionSummary -> Maybe FunctionSummary
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
name Map String FunctionSummary
s of
Just (FunctionSummary (Just AccessPath
prov)) ->
case AccessPath -> [Expr] -> Maybe AccessPath
forall a. AccessPath -> [CExpression a] -> Maybe AccessPath
applySummary AccessPath
prov [Expr]
args of
Just AccessPath
pSrc | Bool -> Bool
not (AccessPath -> Bool
isNullPtr AccessPath
pSrc) ->
case Maybe (AccessPath, Bool)
mBorrow of
Just (dest', mut) | AccessPath
dest' AccessPath -> AccessPath -> Bool
forall a. Eq a => a -> a -> Bool
/= AccessPath
pSrc -> ([if Bool
mut then AccessPath -> AccessPath -> NodeInfo -> Effect
MutableBorrow AccessPath
dest' AccessPath
pSrc NodeInfo
ni else AccessPath -> AccessPath -> NodeInfo -> Effect
SharedBorrow AccessPath
dest' AccessPath
pSrc NodeInfo
ni], Bool
rtOwned)
Maybe (AccessPath, Bool)
_ -> ([], Bool
rtOwned)
Maybe AccessPath
_ -> ([], Bool
rtOwned)
Maybe FunctionSummary
Nothing ->
let inputs :: [(AccessPath, Bool)]
inputs = [ (AccessPath
p, Bool
mut) | (Int
i, Expr
arg) <- [Int] -> [Expr] -> [(Int, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Expr]
args
, let owned :: Bool
owned = Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
False ([Bool] -> Maybe Bool
forall a. [a] -> Maybe a
listToMaybe (Int -> [Bool] -> [Bool]
forall a. Int -> [a] -> [a]
drop Int
i [Bool]
paramOwned))
, let mut :: Bool
mut = Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
False ([Bool] -> Maybe Bool
forall a. [a] -> Maybe a
listToMaybe (Int -> [Bool] -> [Bool]
forall a. Int -> [a] -> [a]
drop Int
i [Bool]
paramMutable))
, let isPtr :: Bool
isPtr = Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
False ([Bool] -> Maybe Bool
forall a. [a] -> Maybe a
listToMaybe (Int -> [Bool] -> [Bool]
forall a. Int -> [a] -> [a]
drop Int
i [Bool]
paramIsPtr))
, Bool -> Bool
not Bool
owned Bool -> Bool -> Bool
&& Bool
isPtr
, Just AccessPath
p <- [Expr -> Maybe AccessPath
forall a. CExpression a -> Maybe AccessPath
exprPath Expr
arg]
]
effs' :: [Effect]
effs' = case Maybe (AccessPath, Bool)
mBorrow of
Just (dest', mutDest) ->
[ if Bool
mutDest Bool -> Bool -> Bool
|| Bool
mutSrc then AccessPath -> AccessPath -> NodeInfo -> Effect
MutableBorrow AccessPath
dest' AccessPath
pSrc NodeInfo
ni else AccessPath -> AccessPath -> NodeInfo -> Effect
SharedBorrow AccessPath
dest' AccessPath
pSrc NodeInfo
ni
| (AccessPath
pSrc, Bool
mutSrc) <- [(AccessPath, Bool)]
inputs, AccessPath
dest' AccessPath -> AccessPath -> Bool
forall a. Eq a => a -> a -> Bool
/= AccessPath
pSrc
]
Maybe (AccessPath, Bool)
Nothing -> []
in ([Effect]
effs', Bool
rtOwned)
Maybe FunctionSummary
_ -> ([], Bool
rtOwned)
Expr
_ -> ([], Bool
rtOwned)
let retEff :: [Effect]
retEff = if Bool
rtOwnedActual Bool -> Bool -> Bool
&& Maybe AccessPath -> Bool
forall a. Maybe a -> Bool
isNothing Maybe AccessPath
destInfo then [AccessPath -> NodeInfo -> Effect
Define AccessPath
dest NodeInfo
ni] else []
[Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Effect] -> TravT Env Identity [Effect])
-> [Effect] -> TravT Env Identity [Effect]
forall a b. (a -> b) -> a -> b
$ [Effect]
effs [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++ [Effect]
provEffs [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++ [Effect]
retEff
CAssign CAssignOp
CAssignOp Expr
l Expr
r NodeInfo
ni -> do
Bool
lo <- Map String (Bool, Bool) -> Expr -> Trav Env Bool
forall (m :: * -> *) b.
MonadTrav m =>
Map String (Bool, b) -> Expr -> m Bool
isExprOwned Map String (Bool, Bool)
localDecls Expr
l
Bool
ro <- Map String (Bool, Bool) -> Expr -> Trav Env Bool
forall (m :: * -> *) b.
MonadTrav m =>
Map String (Bool, b) -> Expr -> m Bool
isExprOwned Map String (Bool, Bool)
localDecls Expr
r
Bool
mut <- Expr -> Trav Env Bool
isExprMutable Expr
l
case Expr -> Maybe AccessPath
forall a. CExpression a -> Maybe AccessPath
exprPath Expr
l of
Just AccessPath
pl -> do
Bool
lp <- Map String (Bool, Bool) -> Expr -> Trav Env Bool
forall (m :: * -> *) a.
MonadTrav m =>
Map String (a, Bool) -> Expr -> m Bool
isExprPointer Map String (Bool, Bool)
localDecls Expr
l
let mAssignBorrow :: Maybe (AccessPath, Bool)
mAssignBorrow = if Bool
lp then (AccessPath, Bool) -> Maybe (AccessPath, Bool)
forall a. a -> Maybe a
Just (AccessPath
pl, Bool
mut) else Maybe (AccessPath, Bool)
forall a. Maybe a
Nothing
[Effect]
re <- t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Bool
-> Expr
-> TravT Env Identity [Effect]
collectMoveEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
mAssignBorrow Bool
lo Expr
r
let defEff :: [Effect]
defEff = if Bool
ro Bool -> Bool -> Bool
&& (Bool
lo Bool -> Bool -> Bool
|| Maybe AccessPath -> Bool
forall a. Maybe a -> Bool
isNothing (Expr -> Maybe AccessPath
forall a. CExpression a -> Maybe AccessPath
exprPath Expr
r)) then [AccessPath -> NodeInfo -> Effect
Define AccessPath
pl NodeInfo
ni] else []
let leakEff :: [Effect]
leakEff = if Bool
lo Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
ro then [AccessPath -> NodeInfo -> Effect
Define AccessPath
pl NodeInfo
ni, AccessPath -> NodeInfo -> Effect
Move AccessPath
pl NodeInfo
ni] else []
[Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Effect] -> TravT Env Identity [Effect])
-> [Effect] -> TravT Env Identity [Effect]
forall a b. (a -> b) -> a -> b
$ [Effect]
re [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++ [Effect]
defEff [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++ [Effect]
leakEff
Maybe AccessPath
Nothing -> [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
(++) ([Effect] -> [Effect] -> [Effect])
-> TravT Env Identity [Effect]
-> TravT Env Identity ([Effect] -> [Effect])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Expr
-> TravT Env Identity [Effect]
collectExprEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
forall a. Maybe a
Nothing Expr
l TravT Env Identity ([Effect] -> [Effect])
-> TravT Env Identity [Effect] -> TravT Env Identity [Effect]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Bool
-> Expr
-> TravT Env Identity [Effect]
collectMoveEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
forall a. Maybe a
Nothing Bool
lo Expr
r
CAssign CAssignOp
_ Expr
l Expr
r NodeInfo
_ -> do
[Effect]
le <- t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Expr
-> TravT Env Identity [Effect]
collectExprEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
forall a. Maybe a
Nothing Expr
l
[Effect]
re <- t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Bool
-> Expr
-> TravT Env Identity [Effect]
collectMoveEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
forall a. Maybe a
Nothing Bool
False Expr
r
[Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Effect] -> TravT Env Identity [Effect])
-> [Effect] -> TravT Env Identity [Effect]
forall a b. (a -> b) -> a -> b
$ [Effect]
le [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++ [Effect]
re
CBinary CBinaryOp
_ Expr
l Expr
r NodeInfo
_ -> do
[Effect]
le <- t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Expr
-> TravT Env Identity [Effect]
collectExprEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
forall a. Maybe a
Nothing Expr
l
[Effect]
re <- t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Bool
-> Expr
-> TravT Env Identity [Effect]
collectMoveEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
forall a. Maybe a
Nothing Bool
False Expr
r
[Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Effect] -> TravT Env Identity [Effect])
-> [Effect] -> TravT Env Identity [Effect]
forall a b. (a -> b) -> a -> b
$ [Effect]
le [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++ [Effect]
re
CUnary CUnaryOp
_ Expr
e NodeInfo
_ -> do
[Effect]
ee <- t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Expr
-> TravT Env Identity [Effect]
collectExprEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
forall a. Maybe a
Nothing Expr
e
[Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return [Effect]
ee
Expr
_ -> [Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return []
where
applySummary :: AccessPath -> [CExpression a] -> Maybe AccessPath
applySummary (PathParam Int
i) [CExpression a]
args | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [CExpression a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CExpression a]
args = CExpression a -> Maybe AccessPath
forall a. CExpression a -> Maybe AccessPath
exprPath ([CExpression a]
args [CExpression a] -> Int -> CExpression a
forall a. [a] -> Int -> a
!! Int
i)
applySummary (PathDeref AccessPath
p) [CExpression a]
args = AccessPath -> AccessPath
PathDeref (AccessPath -> AccessPath) -> Maybe AccessPath -> Maybe AccessPath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AccessPath -> [CExpression a] -> Maybe AccessPath
applySummary AccessPath
p [CExpression a]
args
applySummary (PathField AccessPath
p String
f) [CExpression a]
args = AccessPath -> String -> AccessPath
PathField (AccessPath -> String -> AccessPath)
-> Maybe AccessPath -> Maybe (String -> AccessPath)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AccessPath -> [CExpression a] -> Maybe AccessPath
applySummary AccessPath
p [CExpression a]
args Maybe (String -> AccessPath) -> Maybe String -> Maybe AccessPath
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> Maybe String
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
f
applySummary AccessPath
_ [CExpression a]
_ = Maybe AccessPath
forall a. Maybe a
Nothing
isParamOwned :: ParamDecl -> Bool
isParamOwned (ParamDecl (VarDecl VarName
_ DeclAttrs
_ Type
t) NodeInfo
_) = Type -> Bool
isOwned Type
t
isParamOwned (AbstractParamDecl (VarDecl VarName
_ DeclAttrs
_ Type
t) NodeInfo
_) = Type -> Bool
isOwned Type
t
isParamMutable :: ParamDecl -> Bool
isParamMutable (ParamDecl (VarDecl VarName
_ DeclAttrs
_ Type
t) NodeInfo
_) = Type -> Bool
isPtrTargetMutable Type
t
isParamMutable (AbstractParamDecl (VarDecl VarName
_ DeclAttrs
_ Type
t) NodeInfo
_) = Type -> Bool
isPtrTargetMutable Type
t
isParamPointer :: ParamDecl -> Bool
isParamPointer (ParamDecl (VarDecl VarName
_ DeclAttrs
_ Type
t) NodeInfo
_) = Type -> Bool
isPointerType Type
t
isParamPointer (AbstractParamDecl (VarDecl VarName
_ DeclAttrs
_ Type
t) NodeInfo
_) = Type -> Bool
isPointerType Type
t
isExprPointer :: Map String (a, Bool) -> Expr -> m Bool
isExprPointer Map String (a, Bool)
localDecls Expr
expr = case Expr
expr of
CVar Ident
i NodeInfo
_ -> case String -> Map String (a, Bool) -> Maybe (a, Bool)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Ident -> String
idName Ident
i) Map String (a, Bool)
localDecls of
Just (a
_, Bool
ptr) -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ptr
Maybe (a, Bool)
Nothing -> Expr -> m Bool
forall (m :: * -> *). MonadTrav m => Expr -> m Bool
isExprPointerGlobal Expr
expr
Expr
_ -> Expr -> m Bool
forall (m :: * -> *). MonadTrav m => Expr -> m Bool
isExprPointerGlobal Expr
expr
isExprPointerGlobal :: Expr -> m Bool
isExprPointerGlobal Expr
expr = do
Type
t <- [StmtCtx] -> ExprSide -> Expr -> m Type
forall (m :: * -> *).
MonadTrav m =>
[StmtCtx] -> ExprSide -> Expr -> m Type
tExpr [] ExprSide
RValue Expr
expr
Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Type -> Bool
isPointerType (Type -> Type
canonicalType Type
t)
isPointerDecl :: Map String (a, Bool) -> Ident -> m Bool
isPointerDecl Map String (a, Bool)
localDecls Ident
i = do
case String -> Map String (a, Bool) -> Maybe (a, Bool)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Ident -> String
idName Ident
i) Map String (a, Bool)
localDecls of
Just (a
_, Bool
ptr) -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ptr
Maybe (a, Bool)
Nothing -> Ident -> m (Maybe IdentDecl)
forall (m :: * -> *).
(MonadCError m, MonadSymtab m) =>
Ident -> m (Maybe IdentDecl)
lookupObject Ident
i m (Maybe IdentDecl) -> (Maybe IdentDecl -> m Bool) -> m Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just (ObjectDef (ObjDef (VarDecl VarName
_ DeclAttrs
_ Type
t) Maybe (CInitializer NodeInfo)
_ NodeInfo
_)) -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Type -> Bool
isPointerType Type
t
Just (Declaration (Decl (VarDecl VarName
_ DeclAttrs
_ Type
t) NodeInfo
_)) -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Type -> Bool
isPointerType Type
t
Maybe IdentDecl
_ -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isPtrTargetMutable :: Type -> Bool
isPtrTargetMutable = \case
PtrType Type
t TypeQuals
_ Attributes
_ -> Type -> Bool
isTypeMutable Type
t
ArrayType Type
t ArraySize
_ TypeQuals
_ Attributes
_ -> Type -> Bool
isTypeMutable Type
t
Type
_ -> Bool
False
isExprOwned :: Map String (Bool, b) -> Expr -> m Bool
isExprOwned Map String (Bool, b)
localDecls = \case
CVar Ident
i NodeInfo
_ -> case String -> Map String (Bool, b) -> Maybe (Bool, b)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Ident -> String
idName Ident
i) Map String (Bool, b)
localDecls of
Just (Bool
owned, b
_) -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
owned
Maybe (Bool, b)
Nothing -> Ident -> m (Maybe IdentDecl)
forall (m :: * -> *).
(MonadCError m, MonadSymtab m) =>
Ident -> m (Maybe IdentDecl)
lookupObject Ident
i m (Maybe IdentDecl) -> (Maybe IdentDecl -> m Bool) -> m Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just (ObjectDef (ObjDef (VarDecl VarName
_ (DeclAttrs FunctionAttrs
_ Storage
_ Attributes
attrs) Type
_) Maybe (CInitializer NodeInfo)
_ NodeInfo
_)) -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ (Attr -> Bool) -> Attributes -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Attr -> Bool
isOwnedAttr Attributes
attrs
Just (Declaration (Decl (VarDecl VarName
_ (DeclAttrs FunctionAttrs
_ Storage
_ Attributes
attrs) Type
_) NodeInfo
_)) -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ (Attr -> Bool) -> Attributes -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Attr -> Bool
isOwnedAttr Attributes
attrs
Maybe IdentDecl
_ -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
CUnary CUnaryOp
CIndOp Expr
e NodeInfo
_ -> do
Type
t <- [StmtCtx] -> ExprSide -> Expr -> m Type
forall (m :: * -> *).
MonadTrav m =>
[StmtCtx] -> ExprSide -> Expr -> m Type
tExpr [] ExprSide
RValue Expr
e
case Type -> Type
canonicalType Type
t of
PtrType Type
t' TypeQuals
_ Attributes
_ -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Type -> Bool
isOwned Type
t'
Type
_ -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
CMember Expr
e Ident
i Bool
_ NodeInfo
_ -> do
Type
t <- [StmtCtx] -> ExprSide -> Expr -> m Type
forall (m :: * -> *).
MonadTrav m =>
[StmtCtx] -> ExprSide -> Expr -> m Type
tExpr [] ExprSide
RValue Expr
e
case Type -> Type
canonicalType Type
t of
DirectType (TyComp (CompTypeRef SUERef
sueref CompTyKind
_ NodeInfo
_)) TypeQuals
_ Attributes
_ -> SUERef -> Ident -> m Bool
forall (m :: * -> *). Monad m => SUERef -> Ident -> m Bool
isFieldOwned SUERef
sueref Ident
i
PtrType (DirectType (TyComp (CompTypeRef SUERef
sueref CompTyKind
_ NodeInfo
_)) TypeQuals
_ Attributes
_) TypeQuals
_ Attributes
_ -> SUERef -> Ident -> m Bool
forall (m :: * -> *). Monad m => SUERef -> Ident -> m Bool
isFieldOwned SUERef
sueref Ident
i
Type
_ -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
CCall Expr
f [Expr]
_ NodeInfo
_ -> do
Type
fTy <- [StmtCtx] -> ExprSide -> Expr -> m Type
forall (m :: * -> *).
MonadTrav m =>
[StmtCtx] -> ExprSide -> Expr -> m Type
tExpr [] ExprSide
RValue Expr
f
Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ case Type
fTy of
FunctionType (FunType Type
rt [ParamDecl]
_ Bool
_) Attributes
_ -> Type -> Bool
isOwned Type
rt
FunctionType (FunTypeIncomplete Type
rt) Attributes
_ -> Type -> Bool
isOwned Type
rt
PtrType (Type -> Type
canonicalType -> FunctionType (FunType Type
rt [ParamDecl]
_ Bool
_) Attributes
_) TypeQuals
_ Attributes
_ -> Type -> Bool
isOwned Type
rt
PtrType (Type -> Type
canonicalType -> FunctionType (FunTypeIncomplete Type
rt) Attributes
_) TypeQuals
_ Attributes
_ -> Type -> Bool
isOwned Type
rt
Type
_ -> Bool
False
Expr
_ -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isFieldOwned :: SUERef -> Ident -> m Bool
isFieldOwned SUERef
sueref Ident
i = do
case SUERef -> Map SUERef TagDef -> Maybe TagDef
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SUERef
sueref (GlobalDecls -> Map SUERef TagDef
gTags GlobalDecls
decls) of
Just (CompDef (CompType SUERef
_ CompTyKind
_ [MemberDecl]
members Attributes
_ NodeInfo
_)) ->
Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ (MemberDecl -> Bool) -> [MemberDecl] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Ident -> MemberDecl -> Bool
isMemberOwned Ident
i) [MemberDecl]
members
Maybe TagDef
_ -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isMemberOwned :: Ident -> MemberDecl -> Bool
isMemberOwned Ident
i (MemberDecl (VarDecl (VarName Ident
i' Maybe AsmName
_) (DeclAttrs FunctionAttrs
_ Storage
_ Attributes
attrs) Type
t) Maybe Expr
_ NodeInfo
_) =
Ident -> String
idName Ident
i String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Ident -> String
idName Ident
i' Bool -> Bool -> Bool
&& Attributes -> Type -> Bool
isOwnedDecl Attributes
attrs Type
t
isMemberOwned Ident
_ MemberDecl
_ = Bool
False
collectMoveEffects :: t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Bool
-> Expr
-> TravT Env Identity [Effect]
collectMoveEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
mBorrow Bool
owned Expr
expr = case Expr
expr of
(Expr -> Maybe AccessPath
forall a. CExpression a -> Maybe AccessPath
exprPath -> Just AccessPath
p) -> do
Bool
ro <- Map String (Bool, Bool) -> Expr -> Trav Env Bool
forall (m :: * -> *) b.
MonadTrav m =>
Map String (Bool, b) -> Expr -> m Bool
isExprOwned Map String (Bool, Bool)
localDecls Expr
expr
if Bool
owned Bool -> Bool -> Bool
&& Bool
ro
then [Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return [AccessPath -> NodeInfo -> Effect
Move AccessPath
p (Expr -> NodeInfo
forall a. CNode a => a -> NodeInfo
nodeInfo Expr
expr)]
else t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Expr
-> TravT Env Identity [Effect]
collectExprEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
mBorrow Expr
expr
Expr
_ -> do
[Effect]
ee <- t
-> Map String FunctionSummary
-> Map String (Bool, Bool)
-> Maybe (AccessPath, Bool)
-> Expr
-> TravT Env Identity [Effect]
collectExprEffects t
d Map String FunctionSummary
s Map String (Bool, Bool)
localDecls Maybe (AccessPath, Bool)
mBorrow Expr
expr
Bool
ro <- Map String (Bool, Bool) -> Expr -> Trav Env Bool
forall (m :: * -> *) b.
MonadTrav m =>
Map String (Bool, b) -> Expr -> m Bool
isExprOwned Map String (Bool, Bool)
localDecls Expr
expr
let dest :: AccessPath
dest = AccessPath -> Maybe AccessPath -> AccessPath
forall a. a -> Maybe a -> a
fromMaybe AccessPath
PathReturn ((AccessPath, Bool) -> AccessPath
forall a b. (a, b) -> a
fst ((AccessPath, Bool) -> AccessPath)
-> Maybe (AccessPath, Bool) -> Maybe AccessPath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (AccessPath, Bool)
mBorrow)
if Bool
owned Bool -> Bool -> Bool
&& Bool
ro Bool -> Bool -> Bool
&& Maybe (AccessPath, Bool) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (AccessPath, Bool)
mBorrow
then [Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Effect] -> TravT Env Identity [Effect])
-> [Effect] -> TravT Env Identity [Effect]
forall a b. (a -> b) -> a -> b
$ [Effect]
ee [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++ [AccessPath -> NodeInfo -> Effect
Move AccessPath
dest (Expr -> NodeInfo
forall a. CNode a => a -> NodeInfo
nodeInfo Expr
expr)]
else [Effect] -> TravT Env Identity [Effect]
forall (m :: * -> *) a. Monad m => a -> m a
return [Effect]
ee
reportErrors :: (AccessPath -> Bool)
-> Map k (Set AccessPath)
-> Map k [Effect]
-> Map k Lattice
-> Trav Env ()
reportErrors AccessPath -> Bool
isExpectedOwned Map k (Set AccessPath)
live Map k [Effect]
effects Map k Lattice
result =
[(k, Lattice)]
-> ((k, Lattice) -> TravT Env Identity Lattice) -> Trav Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map k Lattice -> [(k, Lattice)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k Lattice
result) (((k, Lattice) -> TravT Env Identity Lattice) -> Trav Env ())
-> ((k, Lattice) -> TravT Env Identity Lattice) -> Trav Env ()
forall a b. (a -> b) -> a -> b
$ \(k
node, Lattice
lattice) ->
let effs :: [Effect]
effs = [Effect] -> k -> Map k [Effect] -> [Effect]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] k
node Map k [Effect]
effects
nodeLive :: Set AccessPath
nodeLive = Set AccessPath -> k -> Map k (Set AccessPath) -> Set AccessPath
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set AccessPath
forall a. Set a
Set.empty k
node Map k (Set AccessPath)
live
in (Lattice -> Effect -> TravT Env Identity Lattice)
-> Lattice -> [Effect] -> TravT Env Identity Lattice
forall (m :: * -> *) t t.
Monad m =>
(t -> t -> m t) -> t -> [t] -> m t
foldM_ ((AccessPath -> Bool)
-> Set AccessPath
-> Lattice
-> Effect
-> TravT Env Identity Lattice
checkEffect AccessPath -> Bool
isExpectedOwned Set AccessPath
nodeLive) Lattice
lattice [Effect]
effs
mkSpan :: NodeInfo -> Doc AnsiStyle -> DiagnosticSpan Position
mkSpan NodeInfo
ni Doc AnsiStyle
label =
let (Position
pos, Int
len) = NodeInfo -> (Position, Int)
posAndLen NodeInfo
ni
in Position -> Int -> [Doc AnsiStyle] -> DiagnosticSpan Position
forall pos. pos -> Int -> [Doc AnsiStyle] -> DiagnosticSpan pos
DiagnosticSpan Position
pos Int
len [Doc AnsiStyle
label]
checkEffect :: (AccessPath -> Bool)
-> Set AccessPath
-> Lattice
-> Effect
-> TravT Env Identity Lattice
checkEffect AccessPath -> Bool
isExpectedOwned Set AccessPath
nodeLive Lattice
lattice = \case
Use AccessPath
i NodeInfo
ni -> do
case AccessPath -> Lattice -> Maybe VarState
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup AccessPath
i Lattice
lattice of
Just (StateMoved NodeInfo
niMove) ->
NodeInfo
-> DiagnosticLevel
-> Doc AnsiStyle
-> [DiagnosticSpan Position]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Trav Env ()
recordRichError NodeInfo
ni DiagnosticLevel
ErrorLevel (Doc AnsiStyle
"use after move: " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> AccessPath -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
pretty AccessPath
i)
[NodeInfo -> Doc AnsiStyle -> DiagnosticSpan Position
mkSpan NodeInfo
niMove Doc AnsiStyle
"variable moved here"] []
Just (StateInconsistent NodeInfo
_ NodeInfo
niMove) ->
Bool -> Trav Env () -> Trav Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (AccessPath -> Bool
isExpectedOwned AccessPath
i) (Trav Env () -> Trav Env ()) -> Trav Env () -> Trav Env ()
forall a b. (a -> b) -> a -> b
$
NodeInfo
-> DiagnosticLevel
-> Doc AnsiStyle
-> [DiagnosticSpan Position]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Trav Env ()
recordRichError NodeInfo
ni DiagnosticLevel
ErrorLevel (Doc AnsiStyle
"use of variable that may be moved: " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> AccessPath -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
pretty AccessPath
i)
[NodeInfo -> Doc AnsiStyle -> DiagnosticSpan Position
mkSpan NodeInfo
niMove Doc AnsiStyle
"variable may be moved here"] []
Just (StateUninitialized NodeInfo
niDef) ->
NodeInfo
-> DiagnosticLevel
-> Doc AnsiStyle
-> [DiagnosticSpan Position]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Trav Env ()
recordRichError NodeInfo
ni DiagnosticLevel
ErrorLevel (Doc AnsiStyle
"use of uninitialized variable: " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> AccessPath -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
pretty AccessPath
i)
[NodeInfo -> Doc AnsiStyle -> DiagnosticSpan Position
mkSpan NodeInfo
niDef Doc AnsiStyle
"variable declared here"] []
Maybe VarState
_ -> () -> Trav Env ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Lattice -> TravT Env Identity Lattice
forall (m :: * -> *) a. Monad m => a -> m a
return Lattice
lattice
Move AccessPath
i NodeInfo
ni -> do
case AccessPath -> Lattice -> Maybe VarState
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup AccessPath
i Lattice
lattice of
Just (StateMoved NodeInfo
niMove) ->
NodeInfo
-> DiagnosticLevel
-> Doc AnsiStyle
-> [DiagnosticSpan Position]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Trav Env ()
recordRichError NodeInfo
ni DiagnosticLevel
ErrorLevel (Doc AnsiStyle
"move of already moved variable: " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> AccessPath -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
pretty AccessPath
i)
[NodeInfo -> Doc AnsiStyle -> DiagnosticSpan Position
mkSpan NodeInfo
niMove Doc AnsiStyle
"variable first moved here"] []
Just (StateInconsistent NodeInfo
_ NodeInfo
niMove) ->
NodeInfo
-> DiagnosticLevel
-> Doc AnsiStyle
-> [DiagnosticSpan Position]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Trav Env ()
recordRichError NodeInfo
ni DiagnosticLevel
ErrorLevel (Doc AnsiStyle
"move of variable that may be moved: " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> AccessPath -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
pretty AccessPath
i)
[NodeInfo -> Doc AnsiStyle -> DiagnosticSpan Position
mkSpan NodeInfo
niMove Doc AnsiStyle
"variable may be moved here"] []
Just (StateUninitialized NodeInfo
niDef) ->
NodeInfo
-> DiagnosticLevel
-> Doc AnsiStyle
-> [DiagnosticSpan Position]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Trav Env ()
recordRichError NodeInfo
ni DiagnosticLevel
ErrorLevel (Doc AnsiStyle
"move of uninitialized variable: " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> AccessPath -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
pretty AccessPath
i)
[NodeInfo -> Doc AnsiStyle -> DiagnosticSpan Position
mkSpan NodeInfo
niDef Doc AnsiStyle
"variable declared here"] []
Maybe VarState
_ -> () -> Trav Env ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Set AccessPath
-> Lattice
-> AccessPath
-> Maybe AccessPath
-> NodeInfo
-> Doc AnsiStyle
-> Trav Env ()
checkBorrows Set AccessPath
nodeLive Lattice
lattice AccessPath
i Maybe AccessPath
forall a. Maybe a
Nothing NodeInfo
ni Doc AnsiStyle
"move"
Lattice -> TravT Env Identity Lattice
forall (m :: * -> *) a. Monad m => a -> m a
return (Lattice -> TravT Env Identity Lattice)
-> Lattice -> TravT Env Identity Lattice
forall a b. (a -> b) -> a -> b
$ AccessPath -> VarState -> Lattice -> Lattice
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert AccessPath
i (NodeInfo -> VarState
StateMoved NodeInfo
ni) Lattice
lattice
Define AccessPath
i NodeInfo
ni -> do
(AccessPath -> Bool)
-> Lattice -> AccessPath -> NodeInfo -> Trav Env ()
forall a.
(Ord a, Pretty a) =>
(a -> Bool) -> Map a VarState -> a -> NodeInfo -> Trav Env ()
checkOverwrite AccessPath -> Bool
isExpectedOwned Lattice
lattice AccessPath
i NodeInfo
ni
Set AccessPath
-> Lattice
-> AccessPath
-> Maybe AccessPath
-> NodeInfo
-> Doc AnsiStyle
-> Trav Env ()
checkBorrows Set AccessPath
nodeLive Lattice
lattice AccessPath
i (AccessPath -> Maybe AccessPath
forall a. a -> Maybe a
Just AccessPath
i) NodeInfo
ni Doc AnsiStyle
"overwrite"
Lattice -> TravT Env Identity Lattice
forall (m :: * -> *) a. Monad m => a -> m a
return (Lattice -> TravT Env Identity Lattice)
-> Lattice -> TravT Env Identity Lattice
forall a b. (a -> b) -> a -> b
$ AccessPath -> VarState -> Lattice -> Lattice
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert AccessPath
i (NodeInfo -> VarState
StateOwned NodeInfo
ni) Lattice
lattice
Declare AccessPath
i NodeInfo
ni -> Lattice -> TravT Env Identity Lattice
forall (m :: * -> *) a. Monad m => a -> m a
return (Lattice -> TravT Env Identity Lattice)
-> Lattice -> TravT Env Identity Lattice
forall a b. (a -> b) -> a -> b
$ AccessPath -> VarState -> Lattice -> Lattice
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert AccessPath
i (NodeInfo -> VarState
StateUninitialized NodeInfo
ni) Lattice
lattice
SharedBorrow AccessPath
q AccessPath
p NodeInfo
ni -> do
(AccessPath -> Bool)
-> Lattice -> AccessPath -> NodeInfo -> Trav Env ()
forall a.
(Ord a, Pretty a) =>
(a -> Bool) -> Map a VarState -> a -> NodeInfo -> Trav Env ()
checkOverwrite AccessPath -> Bool
isExpectedOwned Lattice
lattice AccessPath
q NodeInfo
ni
Set AccessPath
-> Lattice
-> AccessPath
-> Maybe AccessPath
-> NodeInfo
-> Doc AnsiStyle
-> Trav Env ()
checkMutableBorrows Set AccessPath
nodeLive Lattice
lattice AccessPath
p (AccessPath -> Maybe AccessPath
forall a. a -> Maybe a
Just AccessPath
q) NodeInfo
ni Doc AnsiStyle
"shared borrow"
let origin :: AccessPath
origin = AccessPath -> Lattice -> AccessPath
findOrigin AccessPath
p Lattice
lattice
Lattice -> TravT Env Identity Lattice
forall (m :: * -> *) a. Monad m => a -> m a
return (Lattice -> TravT Env Identity Lattice)
-> Lattice -> TravT Env Identity Lattice
forall a b. (a -> b) -> a -> b
$ AccessPath -> VarState -> Lattice -> Lattice
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert AccessPath
q (AccessPath -> NodeInfo -> VarState
StateSharedBorrowedFrom AccessPath
origin NodeInfo
ni) Lattice
lattice
MutableBorrow AccessPath
q AccessPath
p NodeInfo
ni -> do
(AccessPath -> Bool)
-> Lattice -> AccessPath -> NodeInfo -> Trav Env ()
forall a.
(Ord a, Pretty a) =>
(a -> Bool) -> Map a VarState -> a -> NodeInfo -> Trav Env ()
checkOverwrite AccessPath -> Bool
isExpectedOwned Lattice
lattice AccessPath
q NodeInfo
ni
Set AccessPath
-> Lattice
-> AccessPath
-> Maybe AccessPath
-> NodeInfo
-> Doc AnsiStyle
-> Trav Env ()
checkAnyBorrows Set AccessPath
nodeLive Lattice
lattice AccessPath
p (AccessPath -> Maybe AccessPath
forall a. a -> Maybe a
Just AccessPath
q) NodeInfo
ni Doc AnsiStyle
"mutable borrow"
let origin :: AccessPath
origin = AccessPath -> Lattice -> AccessPath
findOrigin AccessPath
p Lattice
lattice
Lattice -> TravT Env Identity Lattice
forall (m :: * -> *) a. Monad m => a -> m a
return (Lattice -> TravT Env Identity Lattice)
-> Lattice -> TravT Env Identity Lattice
forall a b. (a -> b) -> a -> b
$ AccessPath -> VarState -> Lattice -> Lattice
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert AccessPath
q (AccessPath -> NodeInfo -> VarState
StateMutableBorrowedFrom AccessPath
origin NodeInfo
ni) Lattice
lattice
checkOverwrite :: (a -> Bool) -> Map a VarState -> a -> NodeInfo -> Trav Env ()
checkOverwrite a -> Bool
isExpectedOwned Map a VarState
lattice a
i NodeInfo
ni =
case a -> Map a VarState -> Maybe VarState
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
i Map a VarState
lattice of
Just (StateOwned NodeInfo
niOld) ->
NodeInfo
-> DiagnosticLevel
-> Doc AnsiStyle
-> [DiagnosticSpan Position]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Trav Env ()
recordRichError NodeInfo
ni DiagnosticLevel
ErrorLevel (Doc AnsiStyle
"memory leak: " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> a -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
pretty a
i Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
" is overwritten")
[NodeInfo -> Doc AnsiStyle -> DiagnosticSpan Position
mkSpan NodeInfo
niOld Doc AnsiStyle
"variable defined here"] []
Just (StateInconsistent NodeInfo
niDef NodeInfo
_) ->
Bool -> Trav Env () -> Trav Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (a -> Bool
isExpectedOwned a
i) (Trav Env () -> Trav Env ()) -> Trav Env () -> Trav Env ()
forall a b. (a -> b) -> a -> b
$
NodeInfo
-> DiagnosticLevel
-> Doc AnsiStyle
-> [DiagnosticSpan Position]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Trav Env ()
recordRichError NodeInfo
ni DiagnosticLevel
ErrorLevel (Doc AnsiStyle
"memory leak: " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> a -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
pretty a
i Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
" may be leaked")
[NodeInfo -> Doc AnsiStyle -> DiagnosticSpan Position
mkSpan NodeInfo
niDef Doc AnsiStyle
"variable defined here"] []
Maybe VarState
_ -> () -> Trav Env ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkBorrows :: Liveness -> Lattice -> AccessPath -> Maybe AccessPath -> NodeInfo -> PP.Doc AnsiStyle -> Trav Env ()
checkBorrows :: Set AccessPath
-> Lattice
-> AccessPath
-> Maybe AccessPath
-> NodeInfo
-> Doc AnsiStyle
-> Trav Env ()
checkBorrows Set AccessPath
nodeLive Lattice
lattice AccessPath
p Maybe AccessPath
mIgnore NodeInfo
ni Doc AnsiStyle
action =
Set AccessPath
-> Lattice
-> AccessPath
-> Maybe AccessPath
-> NodeInfo
-> Doc AnsiStyle
-> Trav Env ()
checkAnyBorrows Set AccessPath
nodeLive Lattice
lattice AccessPath
p Maybe AccessPath
mIgnore NodeInfo
ni Doc AnsiStyle
action
checkAnyBorrows :: Liveness -> Lattice -> AccessPath -> Maybe AccessPath -> NodeInfo -> PP.Doc AnsiStyle -> Trav Env ()
checkAnyBorrows :: Set AccessPath
-> Lattice
-> AccessPath
-> Maybe AccessPath
-> NodeInfo
-> Doc AnsiStyle
-> Trav Env ()
checkAnyBorrows Set AccessPath
nodeLive Lattice
lattice AccessPath
p Maybe AccessPath
mIgnore NodeInfo
ni Doc AnsiStyle
action =
[(AccessPath, VarState)]
-> ((AccessPath, VarState) -> Trav Env ()) -> Trav Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Lattice -> [(AccessPath, VarState)]
forall k a. Map k a -> [(k, a)]
Map.toList Lattice
lattice) (((AccessPath, VarState) -> Trav Env ()) -> Trav Env ())
-> ((AccessPath, VarState) -> Trav Env ()) -> Trav Env ()
forall a b. (a -> b) -> a -> b
$ \(AccessPath
q, VarState
state) ->
Bool -> Trav Env () -> Trav Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool -> (AccessPath -> Bool) -> Maybe AccessPath -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (AccessPath -> AccessPath -> Bool
`isPathPrefixOf` AccessPath
q) Maybe AccessPath
mIgnore) (Trav Env () -> Trav Env ()) -> Trav Env () -> Trav Env ()
forall a b. (a -> b) -> a -> b
$
case VarState
state of
StateSharedBorrowedFrom AccessPath
p' NodeInfo
niBorrow | AccessPath
p AccessPath -> AccessPath -> Bool
`isPathPrefixOf` AccessPath
p' Bool -> Bool -> Bool
|| AccessPath
p' AccessPath -> AccessPath -> Bool
`isPathPrefixOf` AccessPath
p ->
Bool -> Trav Env () -> Trav Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (AccessPath
q AccessPath -> Set AccessPath -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set AccessPath
nodeLive) (Trav Env () -> Trav Env ()) -> Trav Env () -> Trav Env ()
forall a b. (a -> b) -> a -> b
$
NodeInfo
-> DiagnosticLevel
-> Doc AnsiStyle
-> [DiagnosticSpan Position]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Trav Env ()
recordRichError NodeInfo
ni DiagnosticLevel
ErrorLevel (Doc AnsiStyle
action Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
" of " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> AccessPath -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
pretty AccessPath
p Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
" while borrowed by " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> AccessPath -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
pretty AccessPath
q)
[NodeInfo -> Doc AnsiStyle -> DiagnosticSpan Position
mkSpan NodeInfo
niBorrow Doc AnsiStyle
"borrowed here"] []
StateMutableBorrowedFrom AccessPath
p' NodeInfo
niBorrow | AccessPath
p AccessPath -> AccessPath -> Bool
`isPathPrefixOf` AccessPath
p' Bool -> Bool -> Bool
|| AccessPath
p' AccessPath -> AccessPath -> Bool
`isPathPrefixOf` AccessPath
p ->
Bool -> Trav Env () -> Trav Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (AccessPath
q AccessPath -> Set AccessPath -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set AccessPath
nodeLive) (Trav Env () -> Trav Env ()) -> Trav Env () -> Trav Env ()
forall a b. (a -> b) -> a -> b
$
NodeInfo
-> DiagnosticLevel
-> Doc AnsiStyle
-> [DiagnosticSpan Position]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Trav Env ()
recordRichError NodeInfo
ni DiagnosticLevel
ErrorLevel (Doc AnsiStyle
action Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
" of " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> AccessPath -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
pretty AccessPath
p Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
" while borrowed by " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> AccessPath -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
pretty AccessPath
q)
[NodeInfo -> Doc AnsiStyle -> DiagnosticSpan Position
mkSpan NodeInfo
niBorrow Doc AnsiStyle
"borrowed here"] []
VarState
_ -> () -> Trav Env ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkMutableBorrows :: Liveness -> Lattice -> AccessPath -> Maybe AccessPath -> NodeInfo -> PP.Doc AnsiStyle -> Trav Env ()
checkMutableBorrows :: Set AccessPath
-> Lattice
-> AccessPath
-> Maybe AccessPath
-> NodeInfo
-> Doc AnsiStyle
-> Trav Env ()
checkMutableBorrows Set AccessPath
nodeLive Lattice
lattice AccessPath
p Maybe AccessPath
mIgnore NodeInfo
ni Doc AnsiStyle
action =
[(AccessPath, VarState)]
-> ((AccessPath, VarState) -> Trav Env ()) -> Trav Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Lattice -> [(AccessPath, VarState)]
forall k a. Map k a -> [(k, a)]
Map.toList Lattice
lattice) (((AccessPath, VarState) -> Trav Env ()) -> Trav Env ())
-> ((AccessPath, VarState) -> Trav Env ()) -> Trav Env ()
forall a b. (a -> b) -> a -> b
$ \(AccessPath
q, VarState
state) ->
Bool -> Trav Env () -> Trav Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool -> (AccessPath -> Bool) -> Maybe AccessPath -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (AccessPath -> AccessPath -> Bool
`isPathPrefixOf` AccessPath
q) Maybe AccessPath
mIgnore) (Trav Env () -> Trav Env ()) -> Trav Env () -> Trav Env ()
forall a b. (a -> b) -> a -> b
$
case VarState
state of
StateMutableBorrowedFrom AccessPath
p' NodeInfo
niBorrow | AccessPath
p AccessPath -> AccessPath -> Bool
`isPathPrefixOf` AccessPath
p' Bool -> Bool -> Bool
|| AccessPath
p' AccessPath -> AccessPath -> Bool
`isPathPrefixOf` AccessPath
p ->
Bool -> Trav Env () -> Trav Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (AccessPath
q AccessPath -> Set AccessPath -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set AccessPath
nodeLive) (Trav Env () -> Trav Env ()) -> Trav Env () -> Trav Env ()
forall a b. (a -> b) -> a -> b
$
NodeInfo
-> DiagnosticLevel
-> Doc AnsiStyle
-> [DiagnosticSpan Position]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Trav Env ()
recordRichError NodeInfo
ni DiagnosticLevel
ErrorLevel (Doc AnsiStyle
action Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
" of " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> AccessPath -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
pretty AccessPath
p Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
" while borrowed by " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> AccessPath -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
pretty AccessPath
q)
[NodeInfo -> Doc AnsiStyle -> DiagnosticSpan Position
mkSpan NodeInfo
niBorrow Doc AnsiStyle
"borrowed here"] []
VarState
_ -> () -> Trav Env ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkLeaks :: (AccessPath -> Bool)
-> p
-> p
-> (Node -> Lattice -> Lattice)
-> Map Node Lattice
-> Trav Env ()
checkLeaks AccessPath -> Bool
isExpectedOwned p
_ p
_ Node -> Lattice -> Lattice
transferFunc Map Node Lattice
result =
[(Node, Lattice)]
-> ((Node, Lattice) -> Trav Env ()) -> Trav Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map Node Lattice -> [(Node, Lattice)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Node Lattice
result) (((Node, Lattice) -> Trav Env ()) -> Trav Env ())
-> ((Node, Lattice) -> Trav Env ()) -> Trav Env ()
forall a b. (a -> b) -> a -> b
$ \(Node
node, Lattice
lattice) -> do
let isLeak :: AccessPath -> VarState -> Bool
isLeak AccessPath
var VarState
state = case VarState
state of
StateOwned NodeInfo
_ -> Bool
True
StateInconsistent NodeInfo
_ NodeInfo
_ -> AccessPath -> Bool
isExpectedOwned AccessPath
var
VarState
_ -> Bool
False
case Node
node of
Node Int
_ NodeKind
ExitNode ->
[(AccessPath, VarState)]
-> ((AccessPath, VarState) -> Trav Env ()) -> Trav Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Lattice -> [(AccessPath, VarState)]
forall k a. Map k a -> [(k, a)]
Map.toList Lattice
lattice) (((AccessPath, VarState) -> Trav Env ()) -> Trav Env ())
-> ((AccessPath, VarState) -> Trav Env ()) -> Trav Env ()
forall a b. (a -> b) -> a -> b
$ \(AccessPath
var, VarState
state) ->
Bool -> Trav Env () -> Trav Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (AccessPath -> Bool
isTemporary AccessPath
var) (Trav Env () -> Trav Env ()) -> Trav Env () -> Trav Env ()
forall a b. (a -> b) -> a -> b
$ case VarState
state of
StateOwned NodeInfo
ni ->
NodeInfo
-> DiagnosticLevel
-> Doc AnsiStyle
-> [DiagnosticSpan Position]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Trav Env ()
recordRichError NodeInfo
ni DiagnosticLevel
ErrorLevel (Doc AnsiStyle
"memory leak: " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> AccessPath -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
pretty AccessPath
var) [] []
StateInconsistent NodeInfo
ni NodeInfo
_ | AccessPath -> Bool
isExpectedOwned AccessPath
var ->
NodeInfo
-> DiagnosticLevel
-> Doc AnsiStyle
-> [DiagnosticSpan Position]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Trav Env ()
recordRichError NodeInfo
ni DiagnosticLevel
ErrorLevel (Doc AnsiStyle
"memory leak: " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> AccessPath -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
pretty AccessPath
var Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
" may be leaked")
[NodeInfo -> Doc AnsiStyle -> DiagnosticSpan Position
mkSpan NodeInfo
ni Doc AnsiStyle
"variable defined here"] []
VarState
_ -> () -> Trav Env ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Node
_ -> do
let nextLattice :: Lattice
nextLattice = Node -> Lattice -> Lattice
transferFunc Node
node Lattice
lattice
[(AccessPath, VarState)]
-> ((AccessPath, VarState) -> Trav Env ()) -> Trav Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Lattice -> [(AccessPath, VarState)]
forall k a. Map k a -> [(k, a)]
Map.toList Lattice
nextLattice) (((AccessPath, VarState) -> Trav Env ()) -> Trav Env ())
-> ((AccessPath, VarState) -> Trav Env ()) -> Trav Env ()
forall a b. (a -> b) -> a -> b
$ \(AccessPath
var, VarState
state) ->
Bool -> Trav Env () -> Trav Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (AccessPath -> Bool
isTemporary AccessPath
var Bool -> Bool -> Bool
&& AccessPath -> VarState -> Bool
isLeak AccessPath
var VarState
state) (Trav Env () -> Trav Env ()) -> Trav Env () -> Trav Env ()
forall a b. (a -> b) -> a -> b
$
NodeInfo
-> DiagnosticLevel
-> Doc AnsiStyle
-> [DiagnosticSpan Position]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Trav Env ()
recordRichError (VarState -> NodeInfo
getNi VarState
state) DiagnosticLevel
ErrorLevel (Doc AnsiStyle
"memory leak: " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> AccessPath -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
pretty AccessPath
var) [] []
where
getNi :: VarState -> NodeInfo
getNi (StateOwned NodeInfo
ni) = NodeInfo
ni
getNi (StateInconsistent NodeInfo
ni NodeInfo
_) = NodeInfo
ni
getNi (StateUninitialized NodeInfo
ni) = NodeInfo
ni
getNi (StateMoved NodeInfo
ni) = NodeInfo
ni
getNi (StateSharedBorrowedFrom AccessPath
_ NodeInfo
ni) = NodeInfo
ni
getNi (StateMutableBorrowedFrom AccessPath
_ NodeInfo
ni) = NodeInfo
ni
foldM_ :: (t -> t -> m t) -> t -> [t] -> m t
foldM_ t -> t -> m t
f t
a (t
x:[t]
xs) = t -> t -> m t
f t
a t
x m t -> (t -> m t) -> m t
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \t
a' -> (t -> t -> m t) -> t -> [t] -> m t
foldM_ t -> t -> m t
f t
a' [t]
xs
foldM_ t -> t -> m t
_ t
a [] = t -> m t
forall (m :: * -> *) a. Monad m => a -> m a
return t
a
descr :: (GlobalDecls -> Trav Env (), (Text, Text))
descr :: (GlobalDecls -> Trav Env (), (Text, Text))
descr = (GlobalDecls -> Trav Env ()
analyse, (Text
"borrow-check", [Text] -> Text
Text.unlines
[ Text
"Checks for borrow-checker violations in C code."
, Text
""
, Text
"This linter implements a Rust-like borrow checker for C. It tracks ownership,"
, Text
"moves, and borrows of pointers marked with `__attribute__((owned))`."
, Text
""
, Text
"It also makes conservative assumptions about un-annotated functions to ensure"
, Text
"soundness: it assumes the return value of a function borrows from all its"
, Text
"non-owned pointer arguments."
]))