{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Strict            #-}
module Tokstyle.C.Linter.Memzero (descr) where

import           Control.Monad                 (forM, forM_)
import qualified Data.Map.Strict               as Map
import           Data.Maybe                    (fromMaybe)
import           Data.Set                      (Set)
import qualified Data.Set                      as Set
import           Data.Text                     (Text)
import qualified Data.Text                     as Text
import           Language.C.Analysis.SemRep    (FunDef (..), FunType (..),
                                                GlobalDecls (..),
                                                IdentDecl (..), Type (..),
                                                constant, declType)
import           Language.C.Analysis.TravMonad (Trav, lookupObject)
import           Language.C.Analysis.TypeUtils (canonicalType, typeQuals)
import           Language.C.Data.Ident         (Ident (..))
import           Language.C.Data.Node          (NodeInfo, posOfNode)
import           Language.C.Syntax.AST
import           Language.C.Syntax.Constants   (getCInteger)
import           Language.Cimple.Diagnostics   (DiagnosticSpan (..))
import           Prettyprinter                 (pretty, (<+>))
import           Tokstyle.Analysis.Dataflow    (Dataflow (..), solve)
import           Tokstyle.C.Analysis.CFG       (CFG, Node (..), NodeKind (..),
                                                fromFunDef)
import           Tokstyle.C.Analysis.Syntax    (initExprs, statExprs, stats)
import           Tokstyle.C.Env                (DiagnosticLevel (..), Env,
                                                posAndLen, recordRichError)
import           Tokstyle.C.TravUtils          (backticks)


-- | Functions that wipe the object their first argument points to.
wipers :: [String]
wipers :: [String]
wipers = [String
"crypto_memzero", String
"sodium_memzero"]

-- | Functions that take a writable pointer but leave its contents as they are.
keepContents :: [String]
keepContents :: [String]
keepContents = [String
"crypto_memlock", String
"crypto_memunlock", String
"sodium_mlock", String
"sodium_munlock"]

data Effect
    = Declare String
    | Write String
    | Wipe String NodeInfo

-- | Locals that may hold data not wiped since it was written.
type Unwiped = Set String

name :: Ident -> String
name :: Ident -> String
name (Ident String
n Int
_ NodeInfo
_) = String
n

-- | The local an argument of a wiper names, as in @x@ or @&x@.
wiped :: CExpr -> Maybe String
wiped :: CExpr -> Maybe String
wiped = \case
    CVar Ident
i NodeInfo
_          -> String -> Maybe String
forall a. a -> Maybe a
Just (Ident -> String
name Ident
i)
    CUnary CUnaryOp
CAdrOp CExpr
e NodeInfo
_ -> CExpr -> Maybe String
wiped CExpr
e
    CCast CDeclaration NodeInfo
_ CExpr
e NodeInfo
_       -> CExpr -> Maybe String
wiped CExpr
e
    CExpr
_                 -> Maybe String
forall a. Maybe a
Nothing

-- | The local whose contents an assignment to this expression changes.
assigned :: CExpr -> Maybe String
assigned :: CExpr -> Maybe String
assigned = \case
    CVar Ident
i NodeInfo
_          -> String -> Maybe String
forall a. a -> Maybe a
Just (Ident -> String
name Ident
i)
    CIndex CExpr
e CExpr
_ NodeInfo
_      -> CExpr -> Maybe String
assigned CExpr
e
    CMember CExpr
e Ident
_ Bool
_ NodeInfo
_   -> CExpr -> Maybe String
assigned CExpr
e
    CUnary CUnaryOp
CIndOp CExpr
e NodeInfo
_ -> CExpr -> Maybe String
assigned CExpr
e
    CExpr
_                 -> Maybe String
forall a. Maybe a
Nothing

subExprs :: CExpr -> [CExpr]
subExprs :: CExpr -> [CExpr]
subExprs = \case
    CComma [CExpr]
es NodeInfo
_      -> [CExpr]
es
    CAssign CAssignOp
_ CExpr
l CExpr
r NodeInfo
_  -> [CExpr
l, CExpr
r]
    CCond CExpr
c Maybe CExpr
t CExpr
e NodeInfo
_    -> CExpr
c CExpr -> [CExpr] -> [CExpr]
forall a. a -> [a] -> [a]
: [CExpr] -> (CExpr -> [CExpr]) -> Maybe CExpr -> [CExpr]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] CExpr -> [CExpr]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe CExpr
t [CExpr] -> [CExpr] -> [CExpr]
forall a. [a] -> [a] -> [a]
++ [CExpr
e]
    CBinary CBinaryOp
_ CExpr
l CExpr
r NodeInfo
_  -> [CExpr
l, CExpr
r]
    CCast CDeclaration NodeInfo
_ CExpr
e NodeInfo
_      -> [CExpr
e]
    CUnary CUnaryOp
_ CExpr
e NodeInfo
_     -> [CExpr
e]
    CIndex CExpr
b CExpr
i NodeInfo
_     -> [CExpr
b, CExpr
i]
    CCall CExpr
f [CExpr]
args NodeInfo
_   -> CExpr
f CExpr -> [CExpr] -> [CExpr]
forall a. a -> [a] -> [a]
: [CExpr]
args
    CMember CExpr
e Ident
_ Bool
_ NodeInfo
_  -> [CExpr
e]
    CComplexReal CExpr
e NodeInfo
_ -> [CExpr
e]
    CComplexImag CExpr
e NodeInfo
_ -> [CExpr
e]
    CExpr
_                -> []

-- | The names an expression mentions, outside @sizeof@.
mentions :: CExpr -> [String]
mentions :: CExpr -> [String]
mentions = \case
    CVar Ident
i NodeInfo
_      -> [Ident -> String
name Ident
i]
    CSizeofExpr{} -> []
    CExpr
e             -> (CExpr -> [String]) -> [CExpr] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CExpr -> [String]
mentions (CExpr -> [CExpr]
subExprs CExpr
e)

-- | Locals whose address an expression keeps, beyond passing it to a call.
escapes :: CExpr -> [String]
escapes :: CExpr -> [String]
escapes = \case
    CVar Ident
i NodeInfo
_                    -> [Ident -> String
name Ident
i]
    CSizeofExpr{}               -> []
    CCall CExpr
f [CExpr]
_ NodeInfo
_                 -> CExpr -> [String]
escapes CExpr
f
    CIndex CExpr
b CExpr
i NodeInfo
_                -> CExpr -> [String]
base CExpr
b [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ CExpr -> [String]
escapes CExpr
i
    CMember CExpr
b Ident
_ Bool
_ NodeInfo
_             -> CExpr -> [String]
base CExpr
b
    CAssign CAssignOp
_ CExpr
l CExpr
r NodeInfo
_             -> CExpr -> [String]
base CExpr
l [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ CExpr -> [String]
escapes CExpr
r
    CUnary CUnaryOp
CIndOp CExpr
e NodeInfo
_           -> CExpr -> [String]
base CExpr
e
    CUnary CUnaryOp
op CExpr
e NodeInfo
_ | CUnaryOp -> Bool
isIncDec CUnaryOp
op -> CExpr -> [String]
base CExpr
e
    CExpr
e                           -> (CExpr -> [String]) -> [CExpr] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CExpr -> [String]
escapes (CExpr -> [CExpr]
subExprs CExpr
e)
  where
    base :: CExpr -> [String]
base CVar{} = []
    base CExpr
e      = CExpr -> [String]
escapes CExpr
e

isIncDec :: CUnaryOp -> Bool
isIncDec :: CUnaryOp -> Bool
isIncDec CUnaryOp
op = CUnaryOp
op CUnaryOp -> [CUnaryOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CUnaryOp
CPreIncOp, CUnaryOp
CPreDecOp, CUnaryOp
CPostIncOp, CUnaryOp
CPostDecOp]

-- | Whether a call's argument at each position can be written through.
writableParams :: CExpr -> Trav Env (Int -> Bool)
writableParams :: CExpr -> Trav Env (Int -> Bool)
writableParams = \case
    CVar Ident
i NodeInfo
_ -> Ident -> TravT Env Identity (Maybe IdentDecl)
forall (m :: * -> *).
(MonadCError m, MonadSymtab m) =>
Ident -> m (Maybe IdentDecl)
lookupObject Ident
i TravT Env Identity (Maybe IdentDecl)
-> (Maybe IdentDecl -> Trav Env (Int -> Bool))
-> Trav Env (Int -> Bool)
forall a b.
TravT Env Identity a
-> (a -> TravT Env Identity b) -> TravT Env Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just IdentDecl
d | FunctionType (FunType Type
_ [ParamDecl]
params Bool
_) Attributes
_ <- Type -> Type
canonicalType (IdentDecl -> Type
forall n. Declaration n => n -> Type
declType IdentDecl
d) ->
            let writable :: [Bool]
writable = (ParamDecl -> Bool) -> [ParamDecl] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Bool
isWritable (Type -> Bool) -> (ParamDecl -> Type) -> ParamDecl -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParamDecl -> Type
forall n. Declaration n => n -> Type
declType) [ParamDecl]
params
            in (Int -> Bool) -> Trav Env (Int -> Bool)
forall a. a -> TravT Env Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Int -> Bool) -> Trav Env (Int -> Bool))
-> (Int -> Bool) -> Trav Env (Int -> Bool)
forall a b. (a -> b) -> a -> b
$ \Int
n -> Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
True (Int -> [(Int, Bool)] -> Maybe Bool
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
n ([Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [Bool]
writable))
        Maybe IdentDecl
_ -> (Int -> Bool) -> Trav Env (Int -> Bool)
forall a. a -> TravT Env Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Int -> Bool
forall a b. a -> b -> a
const Bool
True)
    CExpr
_ -> (Int -> Bool) -> Trav Env (Int -> Bool)
forall a. a -> TravT Env Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Int -> Bool
forall a b. a -> b -> a
const Bool
True)
  where
    isWritable :: Type -> Bool
isWritable Type
ty = case Type -> Type
canonicalType Type
ty of
        PtrType Type
t TypeQuals
_ Attributes
_     -> Bool -> Bool
not (TypeQuals -> Bool
constant (Type -> TypeQuals
typeQuals Type
t))
        ArrayType Type
t ArraySize
_ TypeQuals
_ Attributes
_ -> Bool -> Bool
not (TypeQuals -> Bool
constant (Type -> TypeQuals
typeQuals Type
t))
        Type
_                 -> Bool
False

exprEffects :: CExpr -> Trav Env [Effect]
exprEffects :: CExpr -> Trav Env [Effect]
exprEffects = \case
    CCall (CVar Ident
f NodeInfo
_) (CExpr
target : [CExpr]
rest) NodeInfo
ni | Ident -> String
name Ident
f String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
wipers -> do
        [Effect]
effs <- [[Effect]] -> [Effect]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Effect]] -> [Effect])
-> TravT Env Identity [[Effect]] -> Trav Env [Effect]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CExpr -> Trav Env [Effect])
-> [CExpr] -> TravT Env Identity [[Effect]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CExpr -> Trav Env [Effect]
exprEffects [CExpr]
rest
        [Effect] -> Trav Env [Effect]
forall a. a -> TravT Env Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Effect] -> Trav Env [Effect]) -> [Effect] -> Trav Env [Effect]
forall a b. (a -> b) -> a -> b
$ [Effect]
effs [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++ [Effect] -> (String -> [Effect]) -> Maybe String -> [Effect]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\String
v -> [String -> NodeInfo -> Effect
Wipe String
v NodeInfo
ni]) (CExpr -> Maybe String
wiped CExpr
target)
    CCall (CVar Ident
f NodeInfo
_) [CExpr]
args NodeInfo
_ | Ident -> String
name Ident
f String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
keepContents ->
        [[Effect]] -> [Effect]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Effect]] -> [Effect])
-> TravT Env Identity [[Effect]] -> Trav Env [Effect]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CExpr -> Trav Env [Effect])
-> [CExpr] -> TravT Env Identity [[Effect]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CExpr -> Trav Env [Effect]
exprEffects [CExpr]
args
    CCall CExpr
f [CExpr]
args NodeInfo
_ -> do
        Int -> Bool
writable <- CExpr -> Trav Env (Int -> Bool)
writableParams CExpr
f
        [[Effect]]
effs <- [(Int, CExpr)]
-> ((Int, CExpr) -> Trav Env [Effect])
-> TravT Env Identity [[Effect]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Int] -> [CExpr] -> [(Int, CExpr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [CExpr]
args) (((Int, CExpr) -> Trav Env [Effect])
 -> TravT Env Identity [[Effect]])
-> ((Int, CExpr) -> Trav Env [Effect])
-> TravT Env Identity [[Effect]]
forall a b. (a -> b) -> a -> b
$ \(Int
n, CExpr
arg) -> do
            [Effect]
inner <- CExpr -> Trav Env [Effect]
exprEffects CExpr
arg
            [Effect] -> Trav Env [Effect]
forall a. a -> TravT Env Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Effect] -> Trav Env [Effect]) -> [Effect] -> Trav Env [Effect]
forall a b. (a -> b) -> a -> b
$ [Effect]
inner [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++ if Int -> Bool
writable Int
n then (String -> Effect) -> [String] -> [Effect]
forall a b. (a -> b) -> [a] -> [b]
map String -> Effect
Write (CExpr -> [String]
mentions CExpr
arg) else []
        [Effect] -> Trav Env [Effect]
forall a. a -> TravT Env Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Effect] -> Trav Env [Effect]) -> [Effect] -> Trav Env [Effect]
forall a b. (a -> b) -> a -> b
$ [[Effect]] -> [Effect]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Effect]]
effs
    CAssign CAssignOp
_ CExpr
l CExpr
r NodeInfo
_ -> do
        [Effect]
effs <- [[Effect]] -> [Effect]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Effect]] -> [Effect])
-> TravT Env Identity [[Effect]] -> Trav Env [Effect]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CExpr -> Trav Env [Effect])
-> [CExpr] -> TravT Env Identity [[Effect]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CExpr -> Trav Env [Effect]
exprEffects [CExpr
r, CExpr
l]
        [Effect] -> Trav Env [Effect]
forall a. a -> TravT Env Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Effect] -> Trav Env [Effect]) -> [Effect] -> Trav Env [Effect]
forall a b. (a -> b) -> a -> b
$ [Effect]
effs [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++ [Effect] -> (String -> [Effect]) -> Maybe String -> [Effect]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (Effect -> [Effect]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Effect -> [Effect]) -> (String -> Effect) -> String -> [Effect]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Effect
Write) (CExpr -> Maybe String
assigned CExpr
l)
    CUnary CUnaryOp
op CExpr
e NodeInfo
_ | CUnaryOp -> Bool
isIncDec CUnaryOp
op -> do
        [Effect]
effs <- CExpr -> Trav Env [Effect]
exprEffects CExpr
e
        [Effect] -> Trav Env [Effect]
forall a. a -> TravT Env Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Effect] -> Trav Env [Effect]) -> [Effect] -> Trav Env [Effect]
forall a b. (a -> b) -> a -> b
$ [Effect]
effs [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++ [Effect] -> (String -> [Effect]) -> Maybe String -> [Effect]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (Effect -> [Effect]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Effect -> [Effect]) -> (String -> Effect) -> String -> [Effect]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Effect
Write) (CExpr -> Maybe String
assigned CExpr
e)
    CSizeofExpr{} -> [Effect] -> Trav Env [Effect]
forall a. a -> TravT Env Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    CExpr
e -> [[Effect]] -> [Effect]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Effect]] -> [Effect])
-> TravT Env Identity [[Effect]] -> Trav Env [Effect]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CExpr -> Trav Env [Effect])
-> [CExpr] -> TravT Env Identity [[Effect]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CExpr -> Trav Env [Effect]
exprEffects (CExpr -> [CExpr]
subExprs CExpr
e)

declItems :: CDecl -> [(Ident, CDeclr, Maybe CInit)]
declItems :: CDeclaration NodeInfo -> [(Ident, CDeclr, Maybe CInit)]
declItems = \case
    CDecl [CDeclarationSpecifier NodeInfo]
_ [(Maybe CDeclr, Maybe CInit, Maybe CExpr)]
ds NodeInfo
_ -> [ (Ident
i, CDeclr
d, Maybe CInit
ini) | (Just d :: CDeclr
d@(CDeclr (Just Ident
i) [CDerivedDeclarator NodeInfo]
_ Maybe (CStringLiteral NodeInfo)
_ [CAttribute NodeInfo]
_ NodeInfo
_), Maybe CInit
ini, Maybe CExpr
_) <- [(Maybe CDeclr, Maybe CInit, Maybe CExpr)]
ds ]
    CDeclaration NodeInfo
_            -> []

isZero :: CInit -> Bool
isZero :: CInit -> Bool
isZero = \case
    CInitExpr (CConst (CIntConst CInteger
i NodeInfo
_)) NodeInfo
_ -> CInteger -> Integer
getCInteger CInteger
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
    CInitList CInitializerList NodeInfo
l NodeInfo
_                        -> (([CPartDesignator NodeInfo], CInit) -> Bool)
-> CInitializerList NodeInfo -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (CInit -> Bool
isZero (CInit -> Bool)
-> (([CPartDesignator NodeInfo], CInit) -> CInit)
-> ([CPartDesignator NodeInfo], CInit)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([CPartDesignator NodeInfo], CInit) -> CInit
forall a b. (a, b) -> b
snd) CInitializerList NodeInfo
l
    CInit
_                                    -> Bool
False

-- | The expressions a node evaluates, or 'Nothing' if the graph doesn't model
-- the statement it stands for.
nodeExprs :: Node -> Maybe [CExpr]
nodeExprs :: Node -> Maybe [CExpr]
nodeExprs (Node Int
_ NodeKind
kind) = case NodeKind
kind of
    StatNode (CExpr Maybe CExpr
e NodeInfo
_)   -> [CExpr] -> Maybe [CExpr]
forall a. a -> Maybe a
Just ([CExpr] -> (CExpr -> [CExpr]) -> Maybe CExpr -> [CExpr]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] CExpr -> [CExpr]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe CExpr
e)
    StatNode (CReturn Maybe CExpr
e NodeInfo
_) -> [CExpr] -> Maybe [CExpr]
forall a. a -> Maybe a
Just ([CExpr] -> (CExpr -> [CExpr]) -> Maybe CExpr -> [CExpr]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] CExpr -> [CExpr]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe CExpr
e)
    StatNode CBreak{}      -> [CExpr] -> Maybe [CExpr]
forall a. a -> Maybe a
Just []
    StatNode CCont{}       -> [CExpr] -> Maybe [CExpr]
forall a. a -> Maybe a
Just []
    StatNode CGoto{}       -> [CExpr] -> Maybe [CExpr]
forall a. a -> Maybe a
Just []
    StatNode CFor{}        -> [CExpr] -> Maybe [CExpr]
forall a. a -> Maybe a
Just []
    StatNode CStatement NodeInfo
_             -> Maybe [CExpr]
forall a. Maybe a
Nothing
    ExprNode CExpr
e             -> [CExpr] -> Maybe [CExpr]
forall a. a -> Maybe a
Just [CExpr
e]
    BranchNode CExpr
e           -> [CExpr] -> Maybe [CExpr]
forall a. a -> Maybe a
Just [CExpr
e]
    DeclNode CDeclaration NodeInfo
d             -> [CExpr] -> Maybe [CExpr]
forall a. a -> Maybe a
Just ([[CExpr]] -> [CExpr]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [CExpr] -> (CInit -> [CExpr]) -> Maybe CInit -> [CExpr]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] CInit -> [CExpr]
initExprs Maybe CInit
ini | (Ident
_, CDeclr
_, Maybe CInit
ini) <- CDeclaration NodeInfo -> [(Ident, CDeclr, Maybe CInit)]
declItems CDeclaration NodeInfo
d ])
    NodeKind
EntryNode              -> [CExpr] -> Maybe [CExpr]
forall a. a -> Maybe a
Just []
    NodeKind
ExitNode               -> [CExpr] -> Maybe [CExpr]
forall a. a -> Maybe a
Just []

nodeEffects :: Node -> Trav Env [Effect]
nodeEffects :: Node -> Trav Env [Effect]
nodeEffects node :: Node
node@(Node Int
_ NodeKind
kind) = case NodeKind
kind of
    DeclNode CDeclaration NodeInfo
d -> [[Effect]] -> [Effect]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Effect]] -> [Effect])
-> TravT Env Identity [[Effect]] -> Trav Env [Effect]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Ident, CDeclr, Maybe CInit)]
-> ((Ident, CDeclr, Maybe CInit) -> Trav Env [Effect])
-> TravT Env Identity [[Effect]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (CDeclaration NodeInfo -> [(Ident, CDeclr, Maybe CInit)]
declItems CDeclaration NodeInfo
d) (\(Ident
i, CDeclr
_, Maybe CInit
ini) -> do
        [Effect]
effs <- [[Effect]] -> [Effect]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Effect]] -> [Effect])
-> TravT Env Identity [[Effect]] -> Trav Env [Effect]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CExpr -> Trav Env [Effect])
-> [CExpr] -> TravT Env Identity [[Effect]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CExpr -> Trav Env [Effect]
exprEffects ([CExpr] -> (CInit -> [CExpr]) -> Maybe CInit -> [CExpr]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] CInit -> [CExpr]
initExprs Maybe CInit
ini)
        let written :: [Effect]
written = [ String -> Effect
Write (Ident -> String
name Ident
i) | Just CInit
v <- [Maybe CInit
ini], Bool -> Bool
not (CInit -> Bool
isZero CInit
v) ]
        [Effect] -> Trav Env [Effect]
forall a. a -> TravT Env Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Effect] -> Trav Env [Effect]) -> [Effect] -> Trav Env [Effect]
forall a b. (a -> b) -> a -> b
$ [Effect]
effs [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++ String -> Effect
Declare (Ident -> String
name Ident
i) Effect -> [Effect] -> [Effect]
forall a. a -> [a] -> [a]
: [Effect]
written)
    NodeKind
_ -> [[Effect]] -> [Effect]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Effect]] -> [Effect])
-> TravT Env Identity [[Effect]] -> Trav Env [Effect]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CExpr -> Trav Env [Effect])
-> [CExpr] -> TravT Env Identity [[Effect]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CExpr -> Trav Env [Effect]
exprEffects ([CExpr] -> Maybe [CExpr] -> [CExpr]
forall a. a -> Maybe a -> a
fromMaybe [] (Node -> Maybe [CExpr]
nodeExprs Node
node))

apply :: Unwiped -> Effect -> Unwiped
apply :: Unwiped -> Effect -> Unwiped
apply Unwiped
s = \case
    Declare String
v -> String -> Unwiped -> Unwiped
forall a. Ord a => a -> Set a -> Set a
Set.delete String
v Unwiped
s
    Write String
v   -> String -> Unwiped -> Unwiped
forall a. Ord a => a -> Set a -> Set a
Set.insert String
v Unwiped
s
    Wipe String
v NodeInfo
_  -> String -> Unwiped -> Unwiped
forall a. Ord a => a -> Set a -> Set a
Set.delete String
v Unwiped
s

isWrite :: Effect -> Bool
isWrite :: Effect -> Bool
isWrite = \case
    Write{} -> Bool
True
    Effect
_       -> Bool
False

-- | Whether no path from this node looks at the local again. A call in a
-- branch condition that fails often takes such a path, and need not have
-- written the local.
untouchedFrom :: CFG -> String -> Node -> Bool
untouchedFrom :: CFG -> String -> Node -> Bool
untouchedFrom CFG
cfg String
v Node
start = (Node -> Bool) -> [Node] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Node -> Bool
untouched (Set Node -> [Node]
forall a. Set a -> [a]
Set.toList (Set Node -> [Node] -> Set Node
reachable Set Node
forall a. Set a
Set.empty [Node
start]))
  where
    reachable :: Set Node -> [Node] -> Set Node
reachable Set Node
seen [] = Set Node
seen
    reachable Set Node
seen (Node
n : [Node]
ns)
        | Node
n Node -> Set Node -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Node
seen = Set Node -> [Node] -> Set Node
reachable Set Node
seen [Node]
ns
        | Bool
otherwise = Set Node -> [Node] -> Set Node
reachable (Node -> Set Node -> Set Node
forall a. Ord a => a -> Set a -> Set a
Set.insert Node
n Set Node
seen) (((EdgeType, Node) -> Node) -> [(EdgeType, Node)] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (EdgeType, Node) -> Node
forall a b. (a, b) -> b
snd ([(EdgeType, Node)] -> Node -> CFG -> [(EdgeType, Node)]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] Node
n CFG
cfg) [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ [Node]
ns)
    untouched :: Node -> Bool
untouched Node
n = Bool -> ([CExpr] -> Bool) -> Maybe [CExpr] -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem String
v ([String] -> Bool) -> ([CExpr] -> [String]) -> [CExpr] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CExpr -> [String]) -> [CExpr] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CExpr -> [String]
mentions) (Node -> Maybe [CExpr]
nodeExprs Node
n)

-- | The locals a body declares, with their declarators.
localDecls :: CStat -> [(Ident, CDeclr)]
localDecls :: CStatement NodeInfo -> [(Ident, CDeclr)]
localDecls CStatement NodeInfo
body = (CStatement NodeInfo -> [(Ident, CDeclr)])
-> [CStatement NodeInfo] -> [(Ident, CDeclr)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CStatement NodeInfo -> [(Ident, CDeclr)]
own (CStatement NodeInfo -> [CStatement NodeInfo]
stats CStatement NodeInfo
body)
  where
    own :: CStatement NodeInfo -> [(Ident, CDeclr)]
own = \case
        CCompound [Ident]
_ [CCompoundBlockItem NodeInfo]
items NodeInfo
_    -> [[(Ident, CDeclr)]] -> [(Ident, CDeclr)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ CDeclaration NodeInfo -> [(Ident, CDeclr)]
decl CDeclaration NodeInfo
d | CBlockDecl CDeclaration NodeInfo
d <- [CCompoundBlockItem NodeInfo]
items ]
        CFor (Right CDeclaration NodeInfo
d) Maybe CExpr
_ Maybe CExpr
_ CStatement NodeInfo
_ NodeInfo
_ -> CDeclaration NodeInfo -> [(Ident, CDeclr)]
decl CDeclaration NodeInfo
d
        CStatement NodeInfo
_                      -> []
    decl :: CDeclaration NodeInfo -> [(Ident, CDeclr)]
decl CDeclaration NodeInfo
d = [ (Ident
i, CDeclr
declr) | (Ident
i, CDeclr
declr, Maybe CInit
_) <- CDeclaration NodeInfo -> [(Ident, CDeclr, Maybe CInit)]
declItems CDeclaration NodeInfo
d ]

wipeTargets :: CExpr -> [String]
wipeTargets :: CExpr -> [String]
wipeTargets CExpr
e = case CExpr
e of
    CCall (CVar Ident
f NodeInfo
_) (CExpr
target : [CExpr]
_) NodeInfo
_ | Ident -> String
name Ident
f String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
wipers -> [String] -> (String -> [String]) -> Maybe String -> [String]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] String -> [String]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CExpr -> Maybe String
wiped CExpr
target)
    CExpr
_ -> (CExpr -> [String]) -> [CExpr] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CExpr -> [String]
wipeTargets (CExpr -> [CExpr]
subExprs CExpr
e)

-- | Locals wiped where the graph doesn't follow the paths: in a @switch@,
-- which it takes as one statement, and in a @do@ loop, which it takes as one
-- that may not run.
unmodelledWipes :: CStat -> [String]
unmodelledWipes :: CStatement NodeInfo -> [String]
unmodelledWipes CStatement NodeInfo
body = (CStatement NodeInfo -> [String])
-> [CStatement NodeInfo] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CStatement NodeInfo -> [String]
own (CStatement NodeInfo -> [CStatement NodeInfo]
stats CStatement NodeInfo
body)
  where
    own :: CStatement NodeInfo -> [String]
own = \case
        CSwitch CExpr
_ CStatement NodeInfo
t NodeInfo
_     -> (CExpr -> [String]) -> [CExpr] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CExpr -> [String]
wipeTargets (CStatement NodeInfo -> [CExpr]
statExprs CStatement NodeInfo
t)
        CWhile CExpr
_ CStatement NodeInfo
t Bool
True NodeInfo
_ -> (CExpr -> [String]) -> [CExpr] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CExpr -> [String]
wipeTargets (CStatement NodeInfo -> [CExpr]
statExprs CStatement NodeInfo
t)
        CStatement NodeInfo
_                 -> []

checkFunction :: FunDef -> Trav Env ()
checkFunction :: FunDef -> Trav Env ()
checkFunction fd :: FunDef
fd@(FunDef VarDecl
_ CStatement NodeInfo
body NodeInfo
_) = do
    let (Node
entry, CFG
cfg) = FunDef -> (Node, CFG)
fromFunDef FunDef
fd
        nodes :: [Node]
nodes = Set Node -> [Node]
forall a. Set a -> [a]
Set.toList (Set Node -> [Node]) -> ([Node] -> Set Node) -> [Node] -> [Node]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Node] -> Set Node
forall a. Ord a => [a] -> Set a
Set.fromList ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ CFG -> [Node]
forall k a. Map k a -> [k]
Map.keys CFG
cfg [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ [ Node
n | [(EdgeType, Node)]
es <- CFG -> [[(EdgeType, Node)]]
forall k a. Map k a -> [a]
Map.elems CFG
cfg, (EdgeType
_, Node
n) <- [(EdgeType, Node)]
es ]
    Map Node [Effect]
effects <- [(Node, [Effect])] -> Map Node [Effect]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Node, [Effect])] -> Map Node [Effect])
-> TravT Env Identity [(Node, [Effect])]
-> TravT Env Identity (Map Node [Effect])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [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
n -> (,) Node
n ([Effect] -> (Node, [Effect]))
-> Trav Env [Effect] -> TravT Env Identity (Node, [Effect])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Node -> Trav Env [Effect]
nodeEffects Node
n)
    let decls :: [(Ident, CDeclr)]
decls = CStatement NodeInfo -> [(Ident, CDeclr)]
localDecls CStatement NodeInfo
body
        counts :: Map String Int
counts = (Int -> Int -> Int) -> [(String, Int)] -> Map String Int
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) [ (Ident -> String
name Ident
i, Int
1 :: Int) | (Ident
i, CDeclr
_) <- [(Ident, CDeclr)]
decls ]
        isObject :: CDeclarator a -> Bool
isObject (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
isPtrOrFun [CDerivedDeclarator a]
derived)
        isPtrOrFun :: CDerivedDeclarator a -> Bool
isPtrOrFun = \case
            CPtrDeclr{} -> Bool
True
            CFunDeclr{} -> Bool
True
            CDerivedDeclarator a
_           -> Bool
False
        objects :: Unwiped
objects = [String] -> Unwiped
forall a. Ord a => [a] -> Set a
Set.fromList [ Ident -> String
name Ident
i | (Ident
i, CDeclr
d) <- [(Ident, CDeclr)]
decls, CDeclr -> Bool
forall {a}. CDeclarator a -> Bool
isObject CDeclr
d, Map String Int
counts Map String Int -> String -> Int
forall k a. Ord k => Map k a -> k -> a
Map.! Ident -> String
name Ident
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 ]
        wipes :: Map String NodeInfo
wipes = (NodeInfo -> NodeInfo -> NodeInfo)
-> [(String, NodeInfo)] -> Map String NodeInfo
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith (\NodeInfo
a NodeInfo
b -> if NodeInfo -> Position
posOfNode NodeInfo
a Position -> Position -> Bool
forall a. Ord a => a -> a -> Bool
< NodeInfo -> Position
posOfNode NodeInfo
b then NodeInfo
a else NodeInfo
b)
            [ (String
v, NodeInfo
ni) | [Effect]
effs <- Map Node [Effect] -> [[Effect]]
forall k a. Map k a -> [a]
Map.elems Map Node [Effect]
effects, Wipe String
v NodeInfo
ni <- [Effect]
effs ]
        excluded :: Unwiped
excluded = [String] -> Unwiped
forall a. Ord a => [a] -> Set a
Set.fromList ([String] -> Unwiped) -> [String] -> Unwiped
forall a b. (a -> b) -> a -> b
$ CStatement NodeInfo -> [String]
unmodelledWipes CStatement NodeInfo
body [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (CExpr -> [String]) -> [CExpr] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CExpr -> [String]
escapes (CStatement NodeInfo -> [CExpr]
statExprs CStatement NodeInfo
body)
        candidates :: Unwiped
candidates = (Unwiped
objects Unwiped -> Unwiped -> Unwiped
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Map String NodeInfo -> Unwiped
forall k a. Map k a -> Set k
Map.keysSet Map String NodeInfo
wipes) Unwiped -> Unwiped -> Unwiped
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Unwiped
excluded
        effectsOf :: Node -> [Effect]
effectsOf Node
n = [Effect] -> Node -> Map Node [Effect] -> [Effect]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] Node
n Map Node [Effect]
effects
        transferNode :: Node -> Unwiped -> Unwiped
transferNode Node
n Unwiped
s = case Node
n of
            Node Int
_ BranchNode{} -> (Unwiped -> Effect -> Unwiped) -> Unwiped -> [Effect] -> Unwiped
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Unwiped -> Effect -> Unwiped
apply Unwiped
s ((Effect -> Bool) -> [Effect] -> [Effect]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Effect -> Bool) -> Effect -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Effect -> Bool
isWrite) (Node -> [Effect]
effectsOf Node
n))
            Node
_                   -> (Unwiped -> Effect -> Unwiped) -> Unwiped -> [Effect] -> Unwiped
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Unwiped -> Effect -> Unwiped
apply Unwiped
s (Node -> [Effect]
effectsOf Node
n)
        edgeTransferNode :: Node -> EdgeType -> Unwiped -> Unwiped
edgeTransferNode Node
n EdgeType
e Unwiped
s = case Node
n of
            Node Int
_ BranchNode{} ->
                let target :: Maybe Node
target = EdgeType -> [(EdgeType, Node)] -> Maybe Node
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup EdgeType
e ([(EdgeType, Node)] -> Node -> CFG -> [(EdgeType, Node)]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] Node
n CFG
cfg)
                    written :: String -> Bool
written String
v = Bool -> (Node -> Bool) -> Maybe Node -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (Bool -> Bool
not (Bool -> Bool) -> (Node -> Bool) -> Node -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CFG -> String -> Node -> Bool
untouchedFrom CFG
cfg String
v) Maybe Node
target
                in (Unwiped -> Effect -> Unwiped) -> Unwiped -> [Effect] -> Unwiped
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Unwiped -> Effect -> Unwiped
apply Unwiped
s [ Effect
w | w :: Effect
w@(Write String
v) <- Node -> [Effect]
effectsOf Node
n, String -> Bool
written String
v ]
            Node
_ -> Unwiped
s
        problem :: Dataflow Node EdgeType Unwiped
problem = Dataflow
            { transfer :: Node -> Unwiped -> Unwiped
transfer     = Node -> Unwiped -> Unwiped
transferNode
            , edgeTransfer :: Node -> EdgeType -> Unwiped -> Unwiped
edgeTransfer = Node -> EdgeType -> Unwiped -> Unwiped
edgeTransferNode
            , merge :: Unwiped -> Unwiped -> Unwiped
merge        = Unwiped -> Unwiped -> Unwiped
forall a. Ord a => Set a -> Set a -> Set a
Set.union
            , initial :: Unwiped
initial      = Unwiped
forall a. Set a
Set.empty
            }
        result :: Map Node Unwiped
result = Node -> CFG -> Dataflow Node EdgeType Unwiped -> Map Node Unwiped
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 Unwiped
problem
    [(Node, Unwiped)]
-> ((Node, Unwiped) -> Trav Env ()) -> Trav Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map Node Unwiped -> [(Node, Unwiped)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Node Unwiped
result) (((Node, Unwiped) -> Trav Env ()) -> Trav Env ())
-> ((Node, Unwiped) -> Trav Env ()) -> Trav Env ()
forall a b. (a -> b) -> a -> b
$ \(Node
n, Unwiped
s) -> do
        let unwiped :: Unwiped
unwiped = [Unwiped] -> Unwiped
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
                [ Node -> EdgeType -> Unwiped -> Unwiped
edgeTransferNode Node
n EdgeType
e (Node -> Unwiped -> Unwiped
transferNode Node
n Unwiped
s)
                | (EdgeType
e, Node Int
_ NodeKind
ExitNode) <- [(EdgeType, Node)] -> Node -> CFG -> [(EdgeType, Node)]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] Node
n CFG
cfg ]
        [String] -> (String -> Trav Env ()) -> Trav Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Unwiped -> [String]
forall a. Set a -> [a]
Set.toList (Unwiped
unwiped Unwiped -> Unwiped -> Unwiped
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Unwiped
candidates)) ((String -> Trav Env ()) -> Trav Env ())
-> (String -> Trav Env ()) -> Trav Env ()
forall a b. (a -> b) -> a -> b
$ \String
v -> Maybe NodeInfo -> (NodeInfo -> Trav Env ()) -> Trav Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Node -> Maybe NodeInfo
nodeInfoOf Node
n) ((NodeInfo -> Trav Env ()) -> Trav Env ())
-> (NodeInfo -> Trav Env ()) -> Trav Env ()
forall a b. (a -> b) -> a -> b
$ \NodeInfo
ni ->
            NodeInfo
-> DiagnosticLevel
-> Doc AnsiStyle
-> [DiagnosticSpan Position]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Trav Env ()
recordRichError NodeInfo
ni DiagnosticLevel
ErrorLevel
                (Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (String -> Doc AnsiStyle
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
v) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"is wiped on other paths, but not before the function returns here")
                [NodeInfo -> Doc AnsiStyle -> DiagnosticSpan Position
mkSpan (Map String NodeInfo
wipes Map String NodeInfo -> String -> NodeInfo
forall k a. Ord k => Map k a -> k -> a
Map.! String
v) Doc AnsiStyle
"wiped here"] []
  where
    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]

nodeInfoOf :: Node -> Maybe NodeInfo
nodeInfoOf :: Node -> Maybe NodeInfo
nodeInfoOf (Node Int
_ NodeKind
kind) = case NodeKind
kind of
    StatNode CStatement NodeInfo
s   -> NodeInfo -> Maybe NodeInfo
forall a. a -> Maybe a
Just (CStatement NodeInfo -> NodeInfo
forall a. CStatement a -> a
forall (ast :: * -> *) a. Annotated ast => ast a -> a
annotation CStatement NodeInfo
s)
    ExprNode CExpr
e   -> NodeInfo -> Maybe NodeInfo
forall a. a -> Maybe a
Just (CExpr -> NodeInfo
forall a. CExpression a -> a
forall (ast :: * -> *) a. Annotated ast => ast a -> a
annotation CExpr
e)
    BranchNode CExpr
e -> NodeInfo -> Maybe NodeInfo
forall a. a -> Maybe a
Just (CExpr -> NodeInfo
forall a. CExpression a -> a
forall (ast :: * -> *) a. Annotated ast => ast a -> a
annotation CExpr
e)
    DeclNode CDeclaration NodeInfo
d   -> NodeInfo -> Maybe NodeInfo
forall a. a -> Maybe a
Just (CDeclaration NodeInfo -> NodeInfo
forall a. CDeclaration a -> a
forall (ast :: * -> *) a. Annotated ast => ast a -> a
annotation CDeclaration NodeInfo
d)
    NodeKind
_            -> Maybe NodeInfo
forall a. Maybe a
Nothing

analyse :: GlobalDecls -> Trav Env ()
analyse :: GlobalDecls -> Trav Env ()
analyse 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 (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 FunDef
fd -> FunDef -> Trav Env ()
checkFunction FunDef
fd
    IdentDecl
_              -> () -> Trav Env ()
forall a. a -> TravT Env Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()


descr :: (GlobalDecls -> Trav Env (), (Text, Text))
descr :: (GlobalDecls -> Trav Env (), (Text, Text))
descr = (GlobalDecls -> Trav Env ()
analyse, (Text
"memzero", [Text] -> Text
Text.unlines
    [ Text
"Checks that a local wiped with `crypto_memzero` on some paths through a"
    , Text
"function is wiped on every path that returns after writing it."
    , Text
""
    , Text
"**Reason:** a wipe says the local holds a secret, such as a key or a"
    , Text
"password. An early return that skips the wipe, often on an error path,"
    , Text
"leaves that secret on the stack."
    ]))