{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StrictData        #-}
-- | Finds `%s` conversions whose argument can be bytes with no NUL after
-- them, so that formatting it reads past the object they're in.
--
-- It reports only what it can show. The bytes the argument points to are a
-- copy of a runtime number of bytes, the copy can fill the object they're in
-- to its end, and nothing in the program writes a NUL into that object:
-- every use of it is one this understands. Where the argument is a
-- parameter, a caller shows it, and so on up. Anything else (an unknown use
-- of the object, a copy it can't bound, a function filling it) makes it say
-- nothing.
--
-- It also reports a call returning an unwritten buffer it was given, on a
-- path no caller decides, in builds where the `#if`s on the way can hold.
module Tokstyle.Linter.NulTerminated (descr) where

import           Control.Monad.State.Strict    (State, evalState, gets, modify)
import           Data.Fix                      (Fix (..))
import           Data.Foldable                 (toList)
import           Data.List                     (sortOn)
import           Data.Map.Strict               (Map)
import qualified Data.Map.Strict               as Map
import           Data.Maybe                    (fromMaybe, listToMaybe,
                                                mapMaybe, maybeToList)
import           Data.Set                      (Set)
import qualified Data.Set                      as Set
import           Data.Text                     (Text)
import qualified Data.Text                     as Text
import qualified Data.Text.Read                as Text
import           Language.Cimple               (AssignOp (..), BinaryOp (..),
                                                Lexeme (..), LiteralType (..),
                                                Node, NodeF (..), Scope (..),
                                                UnaryOp (..), lexemeText)
import           Language.Cimple.Diagnostics   (CimplePos, Diagnostic (..),
                                                DiagnosticLevel (..),
                                                DiagnosticSpan (..),
                                                nodePosAndLen)
import           Language.Cimple.Pretty        (ppNode)
import           Prettyprinter                 (Doc, concatWith, layoutCompact,
                                                pretty, unAnnotate, (<+>))
import           Prettyprinter.Render.Terminal (AnsiStyle)
import           Prettyprinter.Render.Text     (renderStrict)
import           Tokstyle.Common               (backticks, semEq)

type TranslationUnit = (FilePath, [Node (Lexeme Text)])

type Expr = Node (Lexeme Text)

-- * The program

-- | A function: static ones by the file they're in.
data FuncKey = FuncKey (Maybe FilePath) Text
    deriving (FuncKey -> FuncKey -> Bool
(FuncKey -> FuncKey -> Bool)
-> (FuncKey -> FuncKey -> Bool) -> Eq FuncKey
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FuncKey -> FuncKey -> Bool
== :: FuncKey -> FuncKey -> Bool
$c/= :: FuncKey -> FuncKey -> Bool
/= :: FuncKey -> FuncKey -> Bool
Eq, Eq FuncKey
Eq FuncKey =>
(FuncKey -> FuncKey -> Ordering)
-> (FuncKey -> FuncKey -> Bool)
-> (FuncKey -> FuncKey -> Bool)
-> (FuncKey -> FuncKey -> Bool)
-> (FuncKey -> FuncKey -> Bool)
-> (FuncKey -> FuncKey -> FuncKey)
-> (FuncKey -> FuncKey -> FuncKey)
-> Ord FuncKey
FuncKey -> FuncKey -> Bool
FuncKey -> FuncKey -> Ordering
FuncKey -> FuncKey -> FuncKey
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FuncKey -> FuncKey -> Ordering
compare :: FuncKey -> FuncKey -> Ordering
$c< :: FuncKey -> FuncKey -> Bool
< :: FuncKey -> FuncKey -> Bool
$c<= :: FuncKey -> FuncKey -> Bool
<= :: FuncKey -> FuncKey -> Bool
$c> :: FuncKey -> FuncKey -> Bool
> :: FuncKey -> FuncKey -> Bool
$c>= :: FuncKey -> FuncKey -> Bool
>= :: FuncKey -> FuncKey -> Bool
$cmax :: FuncKey -> FuncKey -> FuncKey
max :: FuncKey -> FuncKey -> FuncKey
$cmin :: FuncKey -> FuncKey -> FuncKey
min :: FuncKey -> FuncKey -> FuncKey
Ord, Int -> FuncKey -> ShowS
[FuncKey] -> ShowS
FuncKey -> FilePath
(Int -> FuncKey -> ShowS)
-> (FuncKey -> FilePath) -> ([FuncKey] -> ShowS) -> Show FuncKey
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FuncKey -> ShowS
showsPrec :: Int -> FuncKey -> ShowS
$cshow :: FuncKey -> FilePath
show :: FuncKey -> FilePath
$cshowList :: [FuncKey] -> ShowS
showList :: [FuncKey] -> ShowS
Show)

data Func = Func
    { Func -> Int
funcId     :: Int
      -- ^ Per definition: `#if`s can define a function more than once.
    , Func -> [Cond]
funcConds  :: [Cond]
    , Func -> FilePath
funcFile   :: FilePath
    , Func -> FuncKey
funcKey    :: FuncKey
    , Func -> Text
funcName   :: Text
    , Func -> [(Text, CType)]
funcParams :: [(Text, CType)]
    , Func -> Expr
funcBody   :: Expr
    , Func -> Map Text Var
funcVars   :: Map Text Var
    }

-- | A preprocessor condition in a file, and whether it holds.
data Cond = Cond FilePath Bool Expr

definitions :: FilePath -> [Cond] -> Expr -> [([Cond], Expr)]
definitions :: FilePath -> [Cond] -> Expr -> [([Cond], Expr)]
definitions FilePath
file [Cond]
conds Expr
n = case Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix Expr
n of
    FunctionDefn{} -> [([Cond]
conds, Expr
n)]
    PreprocDefine{} -> [([Cond]
conds, Expr
n)]
    PreprocIf Expr
c [Expr]
ts Expr
e -> Expr -> Bool -> [Expr] -> Expr -> [([Cond], Expr)]
forall {t :: * -> *}.
Foldable t =>
Expr -> Bool -> t Expr -> Expr -> [([Cond], Expr)]
branch Expr
c Bool
True [Expr]
ts Expr
e
    PreprocElif Expr
c [Expr]
ts Expr
e -> Expr -> Bool -> [Expr] -> Expr -> [([Cond], Expr)]
forall {t :: * -> *}.
Foldable t =>
Expr -> Bool -> t Expr -> Expr -> [([Cond], Expr)]
branch Expr
c Bool
True [Expr]
ts Expr
e
    PreprocIfdef Lexeme Text
l [Expr]
ts Expr
e -> Expr -> Bool -> [Expr] -> Expr -> [([Cond], Expr)]
forall {t :: * -> *}.
Foldable t =>
Expr -> Bool -> t Expr -> Expr -> [([Cond], Expr)]
branch (NodeF (Lexeme Text) Expr -> Expr
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (Lexeme Text -> NodeF (Lexeme Text) Expr
forall lexeme a. lexeme -> NodeF lexeme a
PreprocDefined Lexeme Text
l)) Bool
True [Expr]
ts Expr
e
    PreprocIfndef Lexeme Text
l [Expr]
ts Expr
e -> Expr -> Bool -> [Expr] -> Expr -> [([Cond], Expr)]
forall {t :: * -> *}.
Foldable t =>
Expr -> Bool -> t Expr -> Expr -> [([Cond], Expr)]
branch (NodeF (Lexeme Text) Expr -> Expr
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (Lexeme Text -> NodeF (Lexeme Text) Expr
forall lexeme a. lexeme -> NodeF lexeme a
PreprocDefined Lexeme Text
l)) Bool
False [Expr]
ts Expr
e
    NodeF (Lexeme Text) Expr
_ -> (Expr -> [([Cond], Expr)]) -> [Expr] -> [([Cond], Expr)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (FilePath -> [Cond] -> Expr -> [([Cond], Expr)]
definitions FilePath
file [Cond]
conds) (NodeF (Lexeme Text) Expr -> [Expr]
forall a. NodeF (Lexeme Text) a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix Expr
n))
  where
    branch :: Expr -> Bool -> t Expr -> Expr -> [([Cond], Expr)]
branch Expr
x Bool
holds t Expr
ts Expr
e =
        (Expr -> [([Cond], Expr)]) -> t Expr -> [([Cond], Expr)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (FilePath -> [Cond] -> Expr -> [([Cond], Expr)]
definitions FilePath
file (FilePath -> Bool -> Expr -> Cond
Cond FilePath
file Bool
holds Expr
x Cond -> [Cond] -> [Cond]
forall a. a -> [a] -> [a]
: [Cond]
conds)) t Expr
ts
        [([Cond], Expr)] -> [([Cond], Expr)] -> [([Cond], Expr)]
forall a. [a] -> [a] -> [a]
++ FilePath -> [Cond] -> Expr -> [([Cond], Expr)]
definitions FilePath
file (FilePath -> Bool -> Expr -> Cond
Cond FilePath
file (Bool -> Bool
not Bool
holds) Expr
x Cond -> [Cond] -> [Cond]
forall a. a -> [a] -> [a]
: [Cond]
conds) Expr
e

-- | Whether some build makes all of `conds` hold. A file's `#define X` under
-- `#if E` makes `defined(X)` follow from `E`.
satisfiable :: Program -> [Cond] -> Bool
satisfiable :: Program -> [Cond] -> Bool
satisfiable Program
prog [Cond]
conds = [Text] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Text]
atoms Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
16 Bool -> Bool -> Bool
&& ([Bool] -> Bool) -> [[Bool]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any [Bool] -> Bool
holdsAll ((Text -> [Bool]) -> [Text] -> [[Bool]]
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 ([Bool] -> Text -> [Bool]
forall a b. a -> b -> a
const [Bool
True, Bool
False]) [Text]
atoms)
  where
    atoms :: [Text]
atoms = Set Text -> [Text]
forall a. Set a -> [a]
Set.toList (Set Text -> [Text]) -> ([Text] -> Set Text) -> [Text] -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> Set Text
forall a. Ord a => [a] -> Set a
Set.fromList ([Text] -> [Text]) -> [Text] -> [Text]
forall a b. (a -> b) -> a -> b
$
        (Expr -> [Text]) -> [Expr] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Text]
atomsOf ([ Expr
x | Cond FilePath
_ Bool
_ Expr
x <- [Cond]
conds ] [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [ Expr
x | Cond FilePath
file Bool
_ Expr
_ <- [Cond]
conds, (Text
_, [Cond]
dconds) <- FilePath -> [(Text, [Cond])]
defines FilePath
file, Cond FilePath
_ Bool
_ Expr
x <- [Cond]
dconds ])

    defines :: FilePath -> [(Text, [Cond])]
defines FilePath
file = [(Text, [Cond])]
-> FilePath -> Map FilePath [(Text, [Cond])] -> [(Text, [Cond])]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] FilePath
file (Program -> Map FilePath [(Text, [Cond])]
progDefines Program
prog)

    holdsAll :: [Bool] -> Bool
holdsAll [Bool]
values =
        let env :: Map Text Bool
env = [(Text, Bool)] -> Map Text Bool
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([Text] -> [Bool] -> [(Text, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Text]
atoms [Bool]
values)
            global :: Text -> Bool
global Text
a = Bool -> Text -> Map Text Bool -> Bool
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Bool
False Text
a Map Text Bool
env
            definedIn :: FilePath -> Text -> Bool
definedIn FilePath
file Text
x = Text -> Bool
global (Text
"defined " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x)
                Bool -> Bool -> Bool
|| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ (Cond -> Bool) -> [Cond] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Cond FilePath
_ Bool
b Expr
e) -> (Text -> Bool) -> Expr -> Maybe Bool
eval Text -> Bool
global Expr
e Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b) [Cond]
dconds | (Text
d, [Cond]
dconds) <- FilePath -> [(Text, [Cond])]
defines FilePath
file, Text
d Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
x ]
        in (Cond -> Bool) -> [Cond] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Cond FilePath
file Bool
b Expr
e) -> (Text -> Bool) -> Expr -> Maybe Bool
eval (\Text
a -> Bool -> (Text -> Bool) -> Maybe Text -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Text -> Bool
global Text
a) (FilePath -> Text -> Bool
definedIn FilePath
file) (Text -> Text -> Maybe Text
Text.stripPrefix Text
"defined " Text
a)) Expr
e Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b) [Cond]
conds

    eval :: (Text -> Bool) -> Expr -> Maybe Bool
eval Text -> Bool
atom (Fix NodeF (Lexeme Text) Expr
e) = case NodeF (Lexeme Text) Expr
e of
        PreprocDefined Lexeme Text
l      -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Text -> Bool
atom (Text
"defined " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Lexeme Text -> Text
name Lexeme Text
l))
        ParenExpr Expr
x           -> (Text -> Bool) -> Expr -> Maybe Bool
eval Text -> Bool
atom Expr
x
        UnaryExpr UnaryOp
UopNot Expr
x    -> Bool -> Bool
not (Bool -> Bool) -> Maybe Bool -> Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Bool) -> Expr -> Maybe Bool
eval Text -> Bool
atom Expr
x
        BinaryExpr Expr
a BinaryOp
BopAnd Expr
b -> Bool -> Bool -> Bool
(&&) (Bool -> Bool -> Bool) -> Maybe Bool -> Maybe (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Bool) -> Expr -> Maybe Bool
eval Text -> Bool
atom Expr
a Maybe (Bool -> Bool) -> Maybe Bool -> Maybe Bool
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Text -> Bool) -> Expr -> Maybe Bool
eval Text -> Bool
atom Expr
b
        BinaryExpr Expr
a BinaryOp
BopOr Expr
b  -> Bool -> Bool -> Bool
(||) (Bool -> Bool -> Bool) -> Maybe Bool -> Maybe (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Bool) -> Expr -> Maybe Bool
eval Text -> Bool
atom Expr
a Maybe (Bool -> Bool) -> Maybe Bool -> Maybe Bool
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Text -> Bool) -> Expr -> Maybe Bool
eval Text -> Bool
atom Expr
b
        LiteralExpr LiteralType
Int Lexeme Text
l     -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Lexeme Text -> Text
name Lexeme Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
/= Text
"0")
        NodeF (Lexeme Text) Expr
_                     -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Text -> Bool
atom (Expr -> Text
render (NodeF (Lexeme Text) Expr -> Expr
forall (f :: * -> *). f (Fix f) -> Fix f
Fix NodeF (Lexeme Text) Expr
e)))

    atomsOf :: Expr -> [Text]
atomsOf (Fix NodeF (Lexeme Text) Expr
e) = case NodeF (Lexeme Text) Expr
e of
        PreprocDefined Lexeme Text
l      -> [Text
"defined " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Lexeme Text -> Text
name Lexeme Text
l]
        ParenExpr Expr
x           -> Expr -> [Text]
atomsOf Expr
x
        UnaryExpr UnaryOp
UopNot Expr
x    -> Expr -> [Text]
atomsOf Expr
x
        BinaryExpr Expr
a BinaryOp
BopAnd Expr
b -> Expr -> [Text]
atomsOf Expr
a [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++ Expr -> [Text]
atomsOf Expr
b
        BinaryExpr Expr
a BinaryOp
BopOr Expr
b  -> Expr -> [Text]
atomsOf Expr
a [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++ Expr -> [Text]
atomsOf Expr
b
        LiteralExpr LiteralType
Int Lexeme Text
_     -> []
        NodeF (Lexeme Text) Expr
_                     -> [Expr -> Text
render (NodeF (Lexeme Text) Expr -> Expr
forall (f :: * -> *). f (Fix f) -> Fix f
Fix NodeF (Lexeme Text) Expr
e)]

    render :: Expr -> Text
render = SimpleDocStream Any -> Text
forall ann. SimpleDocStream ann -> Text
renderStrict (SimpleDocStream Any -> Text)
-> (Expr -> SimpleDocStream Any) -> Expr -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc Any -> SimpleDocStream Any
forall ann1 ann2. Doc ann1 -> SimpleDocStream ann2
layoutCompact (Doc Any -> SimpleDocStream Any)
-> (Expr -> Doc Any) -> Expr -> SimpleDocStream Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc AnsiStyle -> Doc Any
forall ann xxx. Doc ann -> Doc xxx
unAnnotate (Doc AnsiStyle -> Doc Any)
-> (Expr -> Doc AnsiStyle) -> Expr -> Doc Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Doc AnsiStyle
forall a. Pretty a => Node (Lexeme a) -> Doc AnsiStyle
ppNode

-- | A local variable: its type, and initialiser.
data Var = Var
    { Var -> CType
varType :: CType
    , Var -> Maybe Expr
varInit :: Maybe Expr
    }

-- | As much of a C type as this needs.
data CType
    = TByte
    | TChar
    | TStruct Text
    | TPtr Bool CType
      -- ^ Whether what it points to is const.
    | TArray CType (Maybe Expr)
      -- ^ With its size.
    | TOther

data CallSite = CallSite
    { CallSite -> Func
csFunc :: Func
    , CallSite -> [Expr]
csArgs :: [Expr]
    }

data Program = Program
    { Program -> [Func]
progFuncs    :: [Func]
    , Program -> Set (FilePath, Text)
progStatics  :: Set (FilePath, Text)
    , Program -> Map Text [CallSite]
progCalls    :: Map Text [CallSite]
    , Program -> Map Text (Map Text CType)
progStructs  :: Map Text (Map Text CType)
    , Program -> Map Text CType
progTypedefs :: Map Text CType
    , Program -> Map Text Expr
progConsts   :: Map Text Expr
    , Program -> Map Text [CType]
progProtos   :: Map Text [CType]
      -- ^ The parameter types of every function declared or defined.
    , Program -> Map FilePath [(Text, [Cond])]
progDefines  :: Map FilePath [(Text, [Cond])]
    , Program -> Map Text (Int, Int)
progPrintf   :: Map Text (Int, Int)
      -- ^ The format and first value of functions declared with
      -- `GNU_PRINTF`, from 0.
    }

universe :: Expr -> [Expr]
universe :: Expr -> [Expr]
universe Expr
n = Expr
n Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
universe (NodeF (Lexeme Text) Expr -> [Expr]
forall a. NodeF (Lexeme Text) a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix Expr
n))

-- | Every node, with the nodes it's in, innermost first.
withParents :: Expr -> [(Expr, [Expr])]
withParents :: Expr -> [(Expr, [Expr])]
withParents = [Expr] -> Expr -> [(Expr, [Expr])]
forall {t :: * -> *}.
Foldable t =>
[Fix t] -> Fix t -> [(Fix t, [Fix t])]
go []
  where
    go :: [Fix t] -> Fix t -> [(Fix t, [Fix t])]
go [Fix t]
ps Fix t
n = (Fix t
n, [Fix t]
ps) (Fix t, [Fix t]) -> [(Fix t, [Fix t])] -> [(Fix t, [Fix t])]
forall a. a -> [a] -> [a]
: (Fix t -> [(Fix t, [Fix t])]) -> [Fix t] -> [(Fix t, [Fix t])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Fix t] -> Fix t -> [(Fix t, [Fix t])]
go (Fix t
n Fix t -> [Fix t] -> [Fix t]
forall a. a -> [a] -> [a]
: [Fix t]
ps)) (t (Fix t) -> [Fix t]
forall a. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Fix t -> t (Fix t)
forall (f :: * -> *). Fix f -> f (Fix f)
unFix Fix t
n))

name :: Lexeme Text -> Text
name :: Lexeme Text -> Text
name = Lexeme Text -> Text
forall text. Lexeme text -> text
lexemeText

readInt :: Text -> Maybe Int
readInt :: Text -> Maybe Int
readInt Text
t = case Reader Int
forall a. Integral a => Reader a
Text.decimal Text
t of
    Right (Int
n, Text
rest) | Text -> Bool
Text.null Text
rest -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
n
    Either FilePath (Int, Text)
_                                -> Maybe Int
forall a. Maybe a
Nothing

buildProgram :: [TranslationUnit] -> Program
buildProgram :: [TranslationUnit] -> Program
buildProgram [TranslationUnit]
tus = Program
    { progFuncs :: [Func]
progFuncs = [Func]
funcs
    , progStatics :: Set (FilePath, Text)
progStatics = [(FilePath, Text)] -> Set (FilePath, Text)
forall a. Ord a => [a] -> Set a
Set.fromList
        [ (FilePath
file, Lexeme Text -> Text
name Lexeme Text
fname)
        | (FilePath
file, Fix (FunctionDefn Scope
Static (Fix (FunctionPrototype Expr
_ Lexeme Text
fname [Expr]
_)) Expr
_)) <- [(FilePath, Expr)]
nodes
        ]
    , progCalls :: Map Text [CallSite]
progCalls = ([CallSite] -> [CallSite] -> [CallSite])
-> [(Text, [CallSite])] -> Map Text [CallSite]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith (([CallSite] -> [CallSite] -> [CallSite])
-> [CallSite] -> [CallSite] -> [CallSite]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [CallSite] -> [CallSite] -> [CallSite]
forall a. [a] -> [a] -> [a]
(++))
        [ (Lexeme Text -> Text
name Lexeme Text
callee, [Func -> [Expr] -> CallSite
CallSite Func
f [Expr]
args])
        | Func
f <- [Func]
funcs
        , Fix (FunctionCall (Fix (VarExpr Lexeme Text
callee)) [Expr]
args) <- Expr -> [Expr]
universe (Func -> Expr
funcBody Func
f)
        ]
    , progStructs :: Map Text (Map Text CType)
progStructs = (Map Text CType -> Map Text CType -> Map Text CType)
-> [(Text, Map Text CType)] -> Map Text (Map Text CType)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Map Text CType -> Map Text CType -> Map Text CType
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union
        [ (Lexeme Text -> Text
name Lexeme Text
sname, [(Text, CType)] -> Map Text CType
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ((Expr -> Maybe (Text, CType)) -> [Expr] -> [(Text, CType)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Expr -> Maybe (Text, CType)
member [Expr]
members))
        | (FilePath
_, Fix (Struct Lexeme Text
sname [Expr]
members)) <- [(FilePath, Expr)]
nodes
        ]
    , progTypedefs :: Map Text CType
progTypedefs = Map Text CType
typedefs
    , progConsts :: Map Text Expr
progConsts = [(Text, Expr)] -> Map Text Expr
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Text, Expr)] -> Map Text Expr)
-> [(Text, Expr)] -> Map Text Expr
forall a b. (a -> b) -> a -> b
$
        [ (Lexeme Text -> Text
name Lexeme Text
c, Expr
value) | (FilePath
_, Fix (PreprocDefineConst Lexeme Text
c Expr
value)) <- [(FilePath, Expr)]
nodes ]
        [(Text, Expr)] -> [(Text, Expr)] -> [(Text, Expr)]
forall a. [a] -> [a] -> [a]
++ [ (Lexeme Text -> Text
name Lexeme Text
c, Expr
value) | (FilePath
_, Fix (Enumerator Lexeme Text
c (Just Expr
value))) <- [(FilePath, Expr)]
nodes ]
        [(Text, Expr)] -> [(Text, Expr)] -> [(Text, Expr)]
forall a. [a] -> [a] -> [a]
++ [ (Lexeme Text -> Text
name Lexeme Text
c, Expr
value) | (FilePath
_, Fix (ConstDefn Scope
_ Expr
_ Lexeme Text
c Expr
value)) <- [(FilePath, Expr)]
nodes ]
    , progProtos :: Map Text [CType]
progProtos = [(Text, [CType])] -> Map Text [CType]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
        [ (Lexeme Text -> Text
name Lexeme Text
fname, [ CType -> [Expr] -> CType
withArrays (Expr -> CType
ty' Expr
ty) [Expr]
arrs | Fix (VarDecl Expr
ty Lexeme Text
_ [Expr]
arrs) <- [Expr]
params ])
        | (FilePath
_, Fix (FunctionPrototype Expr
_ Lexeme Text
fname [Expr]
params)) <- [(FilePath, Expr)]
nodes
        ]
    , progDefines :: Map FilePath [(Text, [Cond])]
progDefines = ([(Text, [Cond])] -> [(Text, [Cond])] -> [(Text, [Cond])])
-> [(FilePath, [(Text, [Cond])])] -> Map FilePath [(Text, [Cond])]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith (([(Text, [Cond])] -> [(Text, [Cond])] -> [(Text, [Cond])])
-> [(Text, [Cond])] -> [(Text, [Cond])] -> [(Text, [Cond])]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [(Text, [Cond])] -> [(Text, [Cond])] -> [(Text, [Cond])]
forall a. [a] -> [a] -> [a]
(++))
        [ (FilePath
file, [(Lexeme Text -> Text
name Lexeme Text
d, [Cond]
conds)])
        | (FilePath
file, [Expr]
top) <- [TranslationUnit]
tus, Expr
t <- [Expr]
top, ([Cond]
conds, Fix (PreprocDefine Lexeme Text
d)) <- FilePath -> [Cond] -> Expr -> [([Cond], Expr)]
definitions FilePath
file [] Expr
t
        ]
    , progPrintf :: Map Text (Int, Int)
progPrintf = [(Text, (Int, Int))] -> Map Text (Int, Int)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
        [ (Lexeme Text -> Text
name Lexeme Text
fname, (Int
fmt Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1, Int
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
        | (FilePath
_, Fix (AttrPrintf Lexeme Text
fmtL Lexeme Text
argsL Expr
decl)) <- [(FilePath, Expr)]
nodes
        , Just Int
fmt <- [Text -> Maybe Int
readInt (Lexeme Text -> Text
name Lexeme Text
fmtL)]
        , Just Int
args <- [Text -> Maybe Int
readInt (Lexeme Text -> Text
name Lexeme Text
argsL)]
        , Fix (FunctionPrototype Expr
_ Lexeme Text
fname [Expr]
_) <- Expr -> [Expr]
universe Expr
decl
        ]
    }
  where
    nodes :: [(FilePath, Expr)]
nodes = [ (FilePath
file, Expr
n) | (FilePath
file, [Expr]
top) <- [TranslationUnit]
tus, Expr
t <- [Expr]
top, Expr
n <- Expr -> [Expr]
universe Expr
t ]

    ty' :: Expr -> CType
ty' = Map Text CType -> Expr -> CType
cimpleType Map Text CType
typedefs

    typedefs :: Map Text CType
typedefs = [(Text, CType)] -> Map Text CType
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Text, CType)] -> Map Text CType)
-> [(Text, CType)] -> Map Text CType
forall a b. (a -> b) -> a -> b
$
        [ (Lexeme Text -> Text
name Lexeme Text
tname, Text -> CType
TStruct (Lexeme Text -> Text
name Lexeme Text
sname))
        | (FilePath
_, Fix (Typedef (Fix (Struct Lexeme Text
sname [Expr]
_)) Lexeme Text
tname [Expr]
_)) <- [(FilePath, Expr)]
nodes ]
        [(Text, CType)] -> [(Text, CType)] -> [(Text, CType)]
forall a. [a] -> [a] -> [a]
++ [ (Lexeme Text -> Text
name Lexeme Text
tname, Text -> CType
TStruct (Lexeme Text -> Text
name Lexeme Text
sname))
           | (FilePath
_, Fix (Typedef (Fix (TyStruct Lexeme Text
sname)) Lexeme Text
tname [Expr]
_)) <- [(FilePath, Expr)]
nodes ]
        [(Text, CType)] -> [(Text, CType)] -> [(Text, CType)]
forall a. [a] -> [a] -> [a]
++ [ (Lexeme Text -> Text
name Lexeme Text
tname, Map Text CType -> Expr -> CType
cimpleType Map Text CType
forall k a. Map k a
Map.empty Expr
ty)
           | (FilePath
_, Fix (Typedef Expr
ty Lexeme Text
tname [Expr]
_)) <- [(FilePath, Expr)]
nodes
           , Bool -> Bool
not (Expr -> Bool
forall {lexeme}. Fix (NodeF lexeme) -> Bool
isStruct Expr
ty)
           ]
    isStruct :: Fix (NodeF lexeme) -> Bool
isStruct = \case
        Fix Struct{}   -> Bool
True
        Fix TyStruct{} -> Bool
True
        Fix (NodeF lexeme)
_              -> Bool
False

    member :: Expr -> Maybe (Text, CType)
member (Fix (MemberDecl (Fix (VarDecl Expr
ty Lexeme Text
fname [Expr]
arrs)) Maybe (Lexeme Text)
_)) =
        (Text, CType) -> Maybe (Text, CType)
forall a. a -> Maybe a
Just (Lexeme Text -> Text
name Lexeme Text
fname, CType -> [Expr] -> CType
withArrays (Expr -> CType
ty' Expr
ty) [Expr]
arrs)
    member Expr
_ = Maybe (Text, CType)
forall a. Maybe a
Nothing

    funcs :: [Func]
funcs =
        [ Func
            { funcId :: Int
funcId = Int
i
            , funcConds :: [Cond]
funcConds = [Cond]
conds
            , funcFile :: FilePath
funcFile = FilePath
file
            , funcKey :: FuncKey
funcKey = Maybe FilePath -> Text -> FuncKey
FuncKey (if Scope
scope Scope -> Scope -> Bool
forall a. Eq a => a -> a -> Bool
== Scope
Static then FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
file else Maybe FilePath
forall a. Maybe a
Nothing) (Lexeme Text -> Text
name Lexeme Text
fname)
            , funcName :: Text
funcName = Lexeme Text -> Text
name Lexeme Text
fname
            , funcParams :: [(Text, CType)]
funcParams = [ (Lexeme Text -> Text
name Lexeme Text
p, CType -> [Expr] -> CType
withArrays (Expr -> CType
ty' Expr
ty) [Expr]
arrs) | Fix (VarDecl Expr
ty Lexeme Text
p [Expr]
arrs) <- [Expr]
params ]
            , funcBody :: Expr
funcBody = Expr
body
            , funcVars :: Map Text Var
funcVars = [Expr] -> Expr -> Map Text Var
locals [Expr]
params Expr
body
            }
        | (Int
i, (FilePath
file, [Cond]
conds, Fix (FunctionDefn Scope
scope (Fix (FunctionPrototype Expr
_ Lexeme Text
fname [Expr]
params)) Expr
body))) <-
            [Int]
-> [(FilePath, [Cond], Expr)] -> [(Int, (FilePath, [Cond], Expr))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [ (FilePath
file, [Cond]
conds, Expr
d) | (FilePath
file, [Expr]
top) <- [TranslationUnit]
tus, Expr
t <- [Expr]
top, ([Cond]
conds, d :: Expr
d@(Fix FunctionDefn{})) <- FilePath -> [Cond] -> Expr -> [([Cond], Expr)]
definitions FilePath
file [] Expr
t ]
        ]

    -- A name declared more than once in a function, or also a parameter,
    -- is left out: which one a use means isn't known.
    locals :: [Expr] -> Expr -> Map Text Var
locals [Expr]
params Expr
body =
        let decls :: [(Text, Var)]
decls = [ (Lexeme Text -> Text
name Lexeme Text
v, CType -> Maybe Expr -> Var
Var (CType -> [Expr] -> CType
withArrays (Expr -> CType
ty' Expr
ty) [Expr]
arrs) Maybe Expr
i)
                    | Fix (VarDeclStmt (Fix (VarDecl Expr
ty Lexeme Text
v [Expr]
arrs)) Maybe Expr
i) <- Expr -> [Expr]
universe Expr
body ]
                 [(Text, Var)] -> [(Text, Var)] -> [(Text, Var)]
forall a. [a] -> [a] -> [a]
++ [ (Lexeme Text -> Text
name Lexeme Text
v, CType -> Maybe Expr -> Var
Var (CType -> Maybe Expr -> CType
TArray (Expr -> CType
ty' Expr
ty) (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
size)) Maybe Expr
forall a. Maybe a
Nothing)
                    | Fix (VLA Expr
ty Lexeme Text
v Expr
size) <- Expr -> [Expr]
universe Expr
body ]
            counts :: Map Text Int
counts = (Int -> Int -> Int) -> [(Text, Int)] -> Map Text 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
(+) ([(Text, Int)] -> Map Text Int) -> [(Text, Int)] -> Map Text Int
forall a b. (a -> b) -> a -> b
$
                [ (Text
v, Int
1 :: Int) | (Text
v, Var
_) <- [(Text, Var)]
decls ]
                [(Text, Int)] -> [(Text, Int)] -> [(Text, Int)]
forall a. [a] -> [a] -> [a]
++ [ (Lexeme Text -> Text
name Lexeme Text
p, Int
1) | Fix (VarDecl Expr
_ Lexeme Text
p [Expr]
_) <- [Expr]
params ]
        in [(Text, Var)] -> Map Text Var
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Text, Var)
d | d :: (Text, Var)
d@(Text
v, Var
_) <- [(Text, Var)]
decls, Text -> Map Text Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
v Map Text Int
counts Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1 ]

withArrays :: CType -> [Expr] -> CType
withArrays :: CType -> [Expr] -> CType
withArrays = (Expr -> CType -> CType) -> CType -> [Expr] -> CType
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Expr -> CType -> CType
arr
  where
    arr :: Expr -> CType -> CType
arr (Fix (DeclSpecArray Nullability
_ Maybe Expr
size)) CType
t = CType -> Maybe Expr -> CType
TArray CType
t Maybe Expr
size
    arr Expr
_ CType
t                            = CType
t

cimpleType :: Map Text CType -> Expr -> CType
cimpleType :: Map Text CType -> Expr -> CType
cimpleType Map Text CType
typedefs (Fix NodeF (Lexeme Text) Expr
ty) = case NodeF (Lexeme Text) Expr
ty of
    TyConst Expr
t       -> Map Text CType -> Expr -> CType
cimpleType Map Text CType
typedefs Expr
t
    TyNonnull Expr
t     -> Map Text CType -> Expr -> CType
cimpleType Map Text CType
typedefs Expr
t
    TyNullable Expr
t    -> Map Text CType -> Expr -> CType
cimpleType Map Text CType
typedefs Expr
t
    TyOwner Expr
t       -> Map Text CType -> Expr -> CType
cimpleType Map Text CType
typedefs Expr
t
    TyBitwise Expr
t     -> Map Text CType -> Expr -> CType
cimpleType Map Text CType
typedefs Expr
t
    TyForce Expr
t       -> Map Text CType -> Expr -> CType
cimpleType Map Text CType
typedefs Expr
t
    TyPointer Expr
t     -> Bool -> CType -> CType
TPtr (Expr -> Bool
forall {lexeme}. Fix (NodeF lexeme) -> Bool
isConst Expr
t) (Map Text CType -> Expr -> CType
cimpleType Map Text CType
typedefs Expr
t)
    TyStd Lexeme Text
t | Lexeme Text -> Text
name Lexeme Text
t Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"uint8_t" -> CType
TByte
            | Lexeme Text -> Text
name Lexeme Text
t Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"char" -> CType
TChar
    TyStruct Lexeme Text
s      -> Text -> CType
TStruct (Lexeme Text -> Text
name Lexeme Text
s)
    TyUserDefined Lexeme Text
t -> CType -> Maybe CType -> CType
forall a. a -> Maybe a -> a
fromMaybe CType
TOther (Text -> Map Text CType -> Maybe CType
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Lexeme Text -> Text
name Lexeme Text
t) Map Text CType
typedefs)
    NodeF (Lexeme Text) Expr
_               -> CType
TOther
  where
    isConst :: Fix (NodeF lexeme) -> Bool
isConst = \case
        Fix (TyConst Fix (NodeF lexeme)
_)    -> Bool
True
        Fix (TyNonnull Fix (NodeF lexeme)
t)  -> Fix (NodeF lexeme) -> Bool
isConst Fix (NodeF lexeme)
t
        Fix (TyNullable Fix (NodeF lexeme)
t) -> Fix (NodeF lexeme) -> Bool
isConst Fix (NodeF lexeme)
t
        Fix (TyOwner Fix (NodeF lexeme)
t)    -> Fix (NodeF lexeme) -> Bool
isConst Fix (NodeF lexeme)
t
        Fix (NodeF lexeme)
_                  -> Bool
False

keyFor :: Program -> FilePath -> Text -> FuncKey
keyFor :: Program -> FilePath -> Text -> FuncKey
keyFor Program
prog FilePath
file Text
fn
    | (FilePath, Text) -> Set (FilePath, Text) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (FilePath
file, Text
fn) (Program -> Set (FilePath, Text)
progStatics Program
prog) = Maybe FilePath -> Text -> FuncKey
FuncKey (FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
file) Text
fn
    | Bool
otherwise = Maybe FilePath -> Text -> FuncKey
FuncKey Maybe FilePath
forall a. Maybe a
Nothing Text
fn

callersOf :: Program -> Func -> [CallSite]
callersOf :: Program -> Func -> [CallSite]
callersOf Program
prog Func
f =
    [ CallSite
cs
    | CallSite
cs <- [CallSite] -> Text -> Map Text [CallSite] -> [CallSite]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] (Func -> Text
funcName Func
f) (Program -> Map Text [CallSite]
progCalls Program
prog)
    , Program -> FilePath -> Text -> FuncKey
keyFor Program
prog (Func -> FilePath
funcFile (CallSite -> Func
csFunc CallSite
cs)) (Func -> Text
funcName Func
f) FuncKey -> FuncKey -> Bool
forall a. Eq a => a -> a -> Bool
== Func -> FuncKey
funcKey Func
f
    ]

definitionsOf :: Program -> FilePath -> Text -> [Func]
definitionsOf :: Program -> FilePath -> Text -> [Func]
definitionsOf Program
prog FilePath
file Text
fn =
    [ Func
g | Func
g <- Program -> [Func]
progFuncs Program
prog, Func -> Text
funcName Func
g Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
fn, Func -> FuncKey
funcKey Func
g FuncKey -> FuncKey -> Bool
forall a. Eq a => a -> a -> Bool
== Program -> FilePath -> Text -> FuncKey
keyFor Program
prog FilePath
file Text
fn ]

-- * Expressions

stripCasts :: Expr -> Expr
stripCasts :: Expr -> Expr
stripCasts = \case
    Fix (ParenExpr Expr
e)  -> Expr -> Expr
stripCasts Expr
e
    Fix (CastExpr Expr
_ Expr
e) -> Expr -> Expr
stripCasts Expr
e
    Expr
e                  -> Expr
e

typeIn :: Program -> Func -> Expr -> CType
typeIn :: Program -> Func -> Expr -> CType
typeIn Program
prog Func
f (Fix NodeF (Lexeme Text) Expr
e) = case NodeF (Lexeme Text) Expr
e of
    VarExpr Lexeme Text
v -> case Text -> Map Text Var -> Maybe Var
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Lexeme Text -> Text
name Lexeme Text
v) (Func -> Map Text Var
funcVars Func
f) of
        Just Var
var -> Var -> CType
varType Var
var
        Maybe Var
Nothing  -> CType -> Maybe CType -> CType
forall a. a -> Maybe a -> a
fromMaybe CType
TOther (Text -> [(Text, CType)] -> Maybe CType
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Lexeme Text -> Text
name Lexeme Text
v) (Func -> [(Text, CType)]
funcParams Func
f))
    ParenExpr Expr
x -> Program -> Func -> Expr -> CType
typeIn Program
prog Func
f Expr
x
    CastExpr Expr
ty Expr
_ -> Map Text CType -> Expr -> CType
cimpleType (Program -> Map Text CType
progTypedefs Program
prog) Expr
ty
    PointerAccess Expr
b Lexeme Text
fld -> case Program -> Func -> Expr -> CType
typeIn Program
prog Func
f Expr
b of
        TPtr Bool
_ (TStruct Text
s)   -> Program -> Text -> Text -> CType
fieldType Program
prog Text
s (Lexeme Text -> Text
name Lexeme Text
fld)
        TArray (TStruct Text
s) Maybe Expr
_ -> Program -> Text -> Text -> CType
fieldType Program
prog Text
s (Lexeme Text -> Text
name Lexeme Text
fld)
        CType
_                    -> CType
TOther
    MemberAccess Expr
b Lexeme Text
fld -> case Program -> Func -> Expr -> CType
typeIn Program
prog Func
f Expr
b of
        TStruct Text
s -> Program -> Text -> Text -> CType
fieldType Program
prog Text
s (Lexeme Text -> Text
name Lexeme Text
fld)
        CType
_         -> CType
TOther
    ArrayAccess Expr
b Expr
_ -> CType -> CType
element (Program -> Func -> Expr -> CType
typeIn Program
prog Func
f Expr
b)
    UnaryExpr UnaryOp
UopDeref Expr
x -> CType -> CType
element (Program -> Func -> Expr -> CType
typeIn Program
prog Func
f Expr
x)
    UnaryExpr UnaryOp
UopAddress Expr
x -> Bool -> CType -> CType
TPtr Bool
False (Program -> Func -> Expr -> CType
typeIn Program
prog Func
f Expr
x)
    BinaryExpr Expr
a BinaryOp
BopPlus Expr
_ -> Program -> Func -> Expr -> CType
typeIn Program
prog Func
f Expr
a
    NodeF (Lexeme Text) Expr
_ -> CType
TOther
  where
    element :: CType -> CType
element = \case
        TPtr Bool
_ CType
t   -> CType
t
        TArray CType
t Maybe Expr
_ -> CType
t
        CType
_          -> CType
TOther

fieldType :: Program -> Text -> Text -> CType
fieldType :: Program -> Text -> Text -> CType
fieldType Program
prog Text
s Text
fld = CType -> Maybe CType -> CType
forall a. a -> Maybe a -> a
fromMaybe CType
TOther (Maybe CType -> CType) -> Maybe CType -> CType
forall a b. (a -> b) -> a -> b
$ Text -> Map Text CType -> Maybe CType
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
fld (Map Text CType -> Maybe CType)
-> Maybe (Map Text CType) -> Maybe CType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Text -> Map Text (Map Text CType) -> Maybe (Map Text CType)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
s (Program -> Map Text (Map Text CType)
progStructs Program
prog)

-- | The struct field an expression is: `x->f` or `x.f`, by struct and field.
fieldOf :: Program -> Func -> Expr -> Maybe (Text, Text)
fieldOf :: Program -> Func -> Expr -> Maybe (Text, Text)
fieldOf Program
prog Func
f Expr
e = case Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix Expr
e of
    PointerAccess Expr
b Lexeme Text
fld -> case Program -> Func -> Expr -> CType
typeIn Program
prog Func
f Expr
b of
        TPtr Bool
_ (TStruct Text
s)   -> (Text, Text) -> Maybe (Text, Text)
forall a. a -> Maybe a
Just (Text
s, Lexeme Text -> Text
name Lexeme Text
fld)
        TArray (TStruct Text
s) Maybe Expr
_ -> (Text, Text) -> Maybe (Text, Text)
forall a. a -> Maybe a
Just (Text
s, Lexeme Text -> Text
name Lexeme Text
fld)
        CType
_                    -> Maybe (Text, Text)
forall a. Maybe a
Nothing
    MemberAccess Expr
b Lexeme Text
fld -> case Program -> Func -> Expr -> CType
typeIn Program
prog Func
f Expr
b of
        TStruct Text
s -> (Text, Text) -> Maybe (Text, Text)
forall a. a -> Maybe a
Just (Text
s, Lexeme Text -> Text
name Lexeme Text
fld)
        CType
_         -> Maybe (Text, Text)
forall a. Maybe a
Nothing
    NodeF (Lexeme Text) Expr
_ -> Maybe (Text, Text)
forall a. Maybe a
Nothing

evalConst :: Program -> Expr -> Maybe Integer
evalConst :: Program -> Expr -> Maybe Integer
evalConst Program
prog = Int -> Expr -> Maybe Integer
forall {t}. (Eq t, Num t) => t -> Expr -> Maybe Integer
go (Int
32 :: Int)
  where
    go :: t -> Expr -> Maybe Integer
go t
0 Expr
_ = Maybe Integer
forall a. Maybe a
Nothing
    go t
d (Fix NodeF (Lexeme Text) Expr
e) = case NodeF (Lexeme Text) Expr
e of
        LiteralExpr LiteralType
Int Lexeme Text
l     -> Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Maybe Int -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Maybe Int
readInt (Lexeme Text -> Text
name Lexeme Text
l)
        LiteralExpr LiteralType
ConstId Lexeme Text
l -> t -> Expr -> Maybe Integer
go (t
d t -> t -> t
forall a. Num a => a -> a -> a
- t
1) (Expr -> Maybe Integer) -> Maybe Expr -> Maybe Integer
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Text -> Map Text Expr -> Maybe Expr
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Lexeme Text -> Text
name Lexeme Text
l) (Program -> Map Text Expr
progConsts Program
prog)
        ParenExpr Expr
x           -> t -> Expr -> Maybe Integer
go t
d Expr
x
        CastExpr Expr
_ Expr
x          -> t -> Expr -> Maybe Integer
go t
d Expr
x
        BinaryExpr Expr
a BinaryOp
BopPlus Expr
b  -> Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> Expr -> Maybe Integer
go t
d Expr
a Maybe (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> Expr -> Maybe Integer
go t
d Expr
b
        BinaryExpr Expr
a BinaryOp
BopMinus Expr
b -> (-) (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> Expr -> Maybe Integer
go t
d Expr
a Maybe (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> Expr -> Maybe Integer
go t
d Expr
b
        BinaryExpr Expr
a BinaryOp
BopMul Expr
b   -> Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*) (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> Expr -> Maybe Integer
go t
d Expr
a Maybe (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> Expr -> Maybe Integer
go t
d Expr
b
        NodeF (Lexeme Text) Expr
_                     -> Maybe Integer
forall a. Maybe a
Nothing

-- | Whether two expressions are the same number.
sameValue :: Program -> Expr -> Expr -> Bool
sameValue :: Program -> Expr -> Expr -> Bool
sameValue Program
prog Expr
a Expr
b = Expr -> Expr -> Bool
semEq Expr
a Expr
b Bool -> Bool -> Bool
|| case (Program -> Expr -> Maybe Integer
evalConst Program
prog Expr
a, Program -> Expr -> Maybe Integer
evalConst Program
prog Expr
b) of
    (Just Integer
x, Just Integer
y) -> Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
y
    (Maybe Integer, Maybe Integer)
_                -> Bool
False

isNull :: Expr -> Bool
isNull :: Expr -> Bool
isNull Expr
e = case Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix (Expr -> Expr
stripCasts Expr
e) of
    LiteralExpr LiteralType
ConstId Lexeme Text
l -> Lexeme Text -> Text
name Lexeme Text
l Text -> [Text] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text
"nullptr", Text
"NULL"]
    LiteralExpr LiteralType
Int Lexeme Text
l     -> Lexeme Text -> Text
name Lexeme Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"0"
    NodeF (Lexeme Text) Expr
_                     -> Bool
False

callName :: Expr -> Maybe Text
callName :: Expr -> Maybe Text
callName = \case
    Fix (VarExpr Lexeme Text
f)             -> Text -> Maybe Text
forall a. a -> Maybe a
Just (Lexeme Text -> Text
name Lexeme Text
f)
    Fix (LiteralExpr LiteralType
ConstId Lexeme Text
f) -> Text -> Maybe Text
forall a. a -> Maybe a
Just (Lexeme Text -> Text
name Lexeme Text
f)
    Expr
_                           -> Maybe Text
forall a. Maybe a
Nothing

-- | The size an allocation call asks for.
allocationSize :: Expr -> Maybe Expr
allocationSize :: Expr -> Maybe Expr
allocationSize Expr
e = case Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix (Expr -> Expr
stripCasts Expr
e) of
    FunctionCall Expr
callee [Expr]
args -> case (Expr -> Maybe Text
callName Expr
callee, [Expr]
args) of
        (Just Text
"mem_balloc", [Expr
_, Expr
size]) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
size
        (Just Text
"mem_alloc", [Expr
_, Expr
size])  -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
size
        (Just Text
"malloc", [Expr
size])        -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
size
        (Maybe Text, [Expr])
_                              -> Maybe Expr
forall a. Maybe a
Nothing
    NodeF (Lexeme Text) Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing

-- * Uses

-- | What one use of an object does with it.
data Use
    = Copy Expr Expr
      -- ^ `memcpy(it, src, n)`: the call, and `n`.
    | Store Expr Expr
      -- ^ `it = value`: the assignment, and the value.
    | Read
      -- ^ Reads it, or keeps, compares or frees the pointer, but doesn't
      -- write through it.
    | Unknown
      -- ^ Anything else: writing a byte of it, or giving it to a function
      -- that may.

-- | Functions that read what they're given, or free it.
readers :: [Text]
readers :: [Text]
readers = [Text
"memcmp", Text
"memcpy", Text
"memmove", Text
"mem_delete", Text
"free", Text
"crypto_memcmp", Text
"strlen", Text
"strnlen"]

-- | What each use, in `f`, of the object the nodes `isIt` picks name does.
usesIn :: Program -> Func -> (Expr -> Bool) -> [Use]
usesIn :: Program -> Func -> (Expr -> Bool) -> [Use]
usesIn Program
prog Func
f Expr -> Bool
isIt =
    [ Expr -> [Expr] -> Use
classify Expr
n ([Expr] -> [Expr]
forall {lexeme}. [Fix (NodeF lexeme)] -> [Fix (NodeF lexeme)]
dropWrappers [Expr]
ps) | (Expr
n, [Expr]
ps) <- Expr -> [(Expr, [Expr])]
withParents (Func -> Expr
funcBody Func
f), Expr -> Bool
isIt Expr
n ]
  where
    dropWrappers :: [Fix (NodeF lexeme)] -> [Fix (NodeF lexeme)]
dropWrappers = \case
        Fix ParenExpr{} : [Fix (NodeF lexeme)]
ps -> [Fix (NodeF lexeme)] -> [Fix (NodeF lexeme)]
dropWrappers [Fix (NodeF lexeme)]
ps
        Fix CastExpr{} : [Fix (NodeF lexeme)]
ps  -> [Fix (NodeF lexeme)] -> [Fix (NodeF lexeme)]
dropWrappers [Fix (NodeF lexeme)]
ps
        [Fix (NodeF lexeme)]
ps                   -> [Fix (NodeF lexeme)]
ps

    classify :: Expr -> [Expr] -> Use
classify Expr
n = \case
        c :: Expr
c@(Fix (FunctionCall Expr
callee [Expr]
args)) : [Expr]
_ -> Expr -> Expr -> Expr -> [Expr] -> Use
call Expr
n Expr
c Expr
callee ((Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
stripCasts [Expr]
args)
        assign :: Expr
assign@(Fix (AssignExpr Expr
lhs AssignOp
AopEq Expr
rhs)) : [Expr]
_
            | Expr -> Expr
stripCasts Expr
lhs Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
n -> Expr -> Expr -> Use
Store Expr
assign Expr
rhs
            | Bool
otherwise -> Use
Read
        Fix (AssignExpr Expr
lhs AssignOp
_ Expr
_) : [Expr]
_ | Expr -> Expr
stripCasts Expr
lhs Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
n -> Use
Unknown
        access :: Expr
access@(Fix (ArrayAccess Expr
base Expr
_)) : [Expr]
ps | Expr -> Expr
stripCasts Expr
base Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
n -> case [Expr] -> [Expr]
forall {lexeme}. [Fix (NodeF lexeme)] -> [Fix (NodeF lexeme)]
dropWrappers [Expr]
ps of
            Fix (AssignExpr Expr
lhs AssignOp
_ Expr
_) : [Expr]
_ | Expr -> Expr
stripCasts Expr
lhs Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
access -> Use
Unknown
            Fix (UnaryExpr UnaryOp
op Expr
_) : [Expr]
_ | UnaryOp
op UnaryOp -> [UnaryOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [UnaryOp
UopAddress, UnaryOp
UopIncr, UnaryOp
UopDecr] -> Use
Unknown
            [Expr]
_ -> Use
Read
        Fix ArrayAccess{} : [Expr]
_ -> Use
Read
        Fix (BinaryExpr Expr
_ BinaryOp
op Expr
_) : [Expr]
_ | BinaryOp
op BinaryOp -> [BinaryOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BinaryOp
BopEq, BinaryOp
BopNe, BinaryOp
BopAnd, BinaryOp
BopOr] -> Use
Read
        Fix (UnaryExpr UnaryOp
UopNot Expr
_) : [Expr]
_ -> Use
Read
        Fix (IfStmt Expr
c Expr
_ Maybe Expr
_) : [Expr]
_ | Expr -> Expr
stripCasts Expr
c Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
n -> Use
Read
        Fix SizeofExpr{} : [Expr]
_ -> Use
Read
        Fix (VarDeclStmt (Fix (VarDecl Expr
ty Lexeme Text
_ [Expr]
_)) Maybe Expr
_) : [Expr]
_ | TPtr Bool
True CType
_ <- Map Text CType -> Expr -> CType
cimpleType (Program -> Map Text CType
progTypedefs Program
prog) Expr
ty -> Use
Read
        [Expr]
_ -> Use
Unknown

    call :: Expr -> Expr -> Expr -> [Expr] -> Use
call Expr
n Expr
c Expr
callee [Expr]
args = case Expr -> Maybe Text
callName Expr
callee of
        Just Text
"memcpy" | [Expr
dst, Expr
_, Expr
size] <- [Expr]
args, Expr
dst Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
n -> Expr -> Expr -> Use
Copy Expr
c Expr
size
        Just Text
fn
            | Text
fn Text -> [Text] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text]
readers -> Use
Read
            | Just (Int
fmt, Int
_) <- Program -> Text -> Maybe (Int, Int)
formatOf Program
prog Text
fn
            , (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
fmt) [ Int
i | (Int
i, Expr
a) <- [Int] -> [Expr] -> [(Int, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [Expr]
args, Expr
a Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
n ] -> Use
Read
            | Just [CType]
params <- Text -> Map Text [CType] -> Maybe [CType]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
fn (Program -> Map Text [CType]
progProtos Program
prog)
            , [Int
i] <- [ Int
i | (Int
i, Expr
a) <- [Int] -> [Expr] -> [(Int, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] [Expr]
args, Expr
a Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
n ]
            , TPtr Bool
True CType
_ <- CType -> Maybe CType -> CType
forall a. a -> Maybe a -> a
fromMaybe CType
TOther ([CType] -> Maybe CType
forall a. [a] -> Maybe a
listToMaybe (Int -> [CType] -> [CType]
forall a. Int -> [a] -> [a]
drop Int
i [CType]
params)) -> Use
Read
        Maybe Text
_ -> Use
Unknown

isVar :: Text -> Expr -> Bool
isVar :: Text -> Expr -> Bool
isVar Text
v = \case
    Fix (VarExpr Lexeme Text
v') -> Lexeme Text -> Text
name Lexeme Text
v' Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
v
    Expr
_                -> Bool
False

-- * Proofs

-- | A step of a proof: a place, and what it shows.
data Step = Step FilePath Expr (Doc AnsiStyle)

data Key = KParam FuncKey Int | KField Text Text
    deriving (Key -> Key -> Bool
(Key -> Key -> Bool) -> (Key -> Key -> Bool) -> Eq Key
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Key -> Key -> Bool
== :: Key -> Key -> Bool
$c/= :: Key -> Key -> Bool
/= :: Key -> Key -> Bool
Eq, Eq Key
Eq Key =>
(Key -> Key -> Ordering)
-> (Key -> Key -> Bool)
-> (Key -> Key -> Bool)
-> (Key -> Key -> Bool)
-> (Key -> Key -> Bool)
-> (Key -> Key -> Key)
-> (Key -> Key -> Key)
-> Ord Key
Key -> Key -> Bool
Key -> Key -> Ordering
Key -> Key -> Key
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Key -> Key -> Ordering
compare :: Key -> Key -> Ordering
$c< :: Key -> Key -> Bool
< :: Key -> Key -> Bool
$c<= :: Key -> Key -> Bool
<= :: Key -> Key -> Bool
$c> :: Key -> Key -> Bool
> :: Key -> Key -> Bool
$c>= :: Key -> Key -> Bool
>= :: Key -> Key -> Bool
$cmax :: Key -> Key -> Key
max :: Key -> Key -> Key
$cmin :: Key -> Key -> Key
min :: Key -> Key -> Key
Ord)

data UnwrittenKey = UnwrittenKey Int Int (Maybe Text)
    deriving (UnwrittenKey -> UnwrittenKey -> Bool
(UnwrittenKey -> UnwrittenKey -> Bool)
-> (UnwrittenKey -> UnwrittenKey -> Bool) -> Eq UnwrittenKey
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UnwrittenKey -> UnwrittenKey -> Bool
== :: UnwrittenKey -> UnwrittenKey -> Bool
$c/= :: UnwrittenKey -> UnwrittenKey -> Bool
/= :: UnwrittenKey -> UnwrittenKey -> Bool
Eq, Eq UnwrittenKey
Eq UnwrittenKey =>
(UnwrittenKey -> UnwrittenKey -> Ordering)
-> (UnwrittenKey -> UnwrittenKey -> Bool)
-> (UnwrittenKey -> UnwrittenKey -> Bool)
-> (UnwrittenKey -> UnwrittenKey -> Bool)
-> (UnwrittenKey -> UnwrittenKey -> Bool)
-> (UnwrittenKey -> UnwrittenKey -> UnwrittenKey)
-> (UnwrittenKey -> UnwrittenKey -> UnwrittenKey)
-> Ord UnwrittenKey
UnwrittenKey -> UnwrittenKey -> Bool
UnwrittenKey -> UnwrittenKey -> Ordering
UnwrittenKey -> UnwrittenKey -> UnwrittenKey
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: UnwrittenKey -> UnwrittenKey -> Ordering
compare :: UnwrittenKey -> UnwrittenKey -> Ordering
$c< :: UnwrittenKey -> UnwrittenKey -> Bool
< :: UnwrittenKey -> UnwrittenKey -> Bool
$c<= :: UnwrittenKey -> UnwrittenKey -> Bool
<= :: UnwrittenKey -> UnwrittenKey -> Bool
$c> :: UnwrittenKey -> UnwrittenKey -> Bool
> :: UnwrittenKey -> UnwrittenKey -> Bool
$c>= :: UnwrittenKey -> UnwrittenKey -> Bool
>= :: UnwrittenKey -> UnwrittenKey -> Bool
$cmax :: UnwrittenKey -> UnwrittenKey -> UnwrittenKey
max :: UnwrittenKey -> UnwrittenKey -> UnwrittenKey
$cmin :: UnwrittenKey -> UnwrittenKey -> UnwrittenKey
min :: UnwrittenKey -> UnwrittenKey -> UnwrittenKey
Ord)

type Proof = ([Step], [Cond])

data Memo = Memo
    { Memo -> Map UnwrittenKey (Maybe Proof)
memoUnwritten  :: Map UnwrittenKey (Maybe Proof)
    , Memo -> Set UnwrittenKey
memoBusy       :: Set UnwrittenKey
    , Memo -> Map Key (Maybe [Step])
memoDone       :: Map Key (Maybe [Step])
    , Memo -> Set Key
memoInProgress :: Set Key
    }

type M = State Memo

remember :: Key -> M (Maybe [Step]) -> M (Maybe [Step])
remember :: Key -> M (Maybe [Step]) -> M (Maybe [Step])
remember Key
key M (Maybe [Step])
act = do
    Maybe (Maybe [Step])
done <- (Memo -> Maybe (Maybe [Step]))
-> StateT Memo Identity (Maybe (Maybe [Step]))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Key -> Map Key (Maybe [Step]) -> Maybe (Maybe [Step])
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Key
key (Map Key (Maybe [Step]) -> Maybe (Maybe [Step]))
-> (Memo -> Map Key (Maybe [Step])) -> Memo -> Maybe (Maybe [Step])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Memo -> Map Key (Maybe [Step])
memoDone)
    Bool
busy <- (Memo -> Bool) -> StateT Memo Identity Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Key -> Set Key -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Key
key (Set Key -> Bool) -> (Memo -> Set Key) -> Memo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Memo -> Set Key
memoInProgress)
    case Maybe (Maybe [Step])
done of
        Just Maybe [Step]
r -> Maybe [Step] -> M (Maybe [Step])
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [Step]
r
        Maybe (Maybe [Step])
Nothing | Bool
busy -> Maybe [Step] -> M (Maybe [Step])
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [Step]
forall a. Maybe a
Nothing
        Maybe (Maybe [Step])
Nothing -> do
            (Memo -> Memo) -> StateT Memo Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Memo -> Memo) -> StateT Memo Identity ())
-> (Memo -> Memo) -> StateT Memo Identity ()
forall a b. (a -> b) -> a -> b
$ \Memo
m -> Memo
m{memoInProgress = Set.insert key (memoInProgress m)}
            Maybe [Step]
r <- M (Maybe [Step])
act
            (Memo -> Memo) -> StateT Memo Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Memo -> Memo) -> StateT Memo Identity ())
-> (Memo -> Memo) -> StateT Memo Identity ()
forall a b. (a -> b) -> a -> b
$ \Memo
m -> Memo
m{memoDone = Map.insert key r (memoDone m), memoInProgress = Set.delete key (memoInProgress m)}
            Maybe [Step] -> M (Maybe [Step])
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [Step]
r

firstJust :: [M (Maybe a)] -> M (Maybe a)
firstJust :: forall a. [M (Maybe a)] -> M (Maybe a)
firstJust [] = Maybe a -> M (Maybe a)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe a
forall a. Maybe a
Nothing
firstJust (M (Maybe a)
x:[M (Maybe a)]
xs) = M (Maybe a)
x M (Maybe a) -> (Maybe a -> M (Maybe a)) -> M (Maybe a)
forall a b.
StateT Memo Identity a
-> (a -> StateT Memo Identity b) -> StateT Memo Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just a
r  -> Maybe a -> M (Maybe a)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Maybe a
forall a. a -> Maybe a
Just a
r)
    Maybe a
Nothing -> [M (Maybe a)] -> M (Maybe a)
forall a. [M (Maybe a)] -> M (Maybe a)
firstJust [M (Maybe a)]
xs

maxDepth :: Int
maxDepth :: Int
maxDepth = Int
12

-- | How the bytes `e` points to, in `f`, can have no NUL after them before
-- the end of the object they're in: the steps that show it.
unterminated :: Program -> Int -> Func -> Expr -> M (Maybe [Step])
unterminated :: Program -> Int -> Func -> Expr -> M (Maybe [Step])
unterminated Program
_ Int
0 Func
_ Expr
_ = Maybe [Step] -> M (Maybe [Step])
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [Step]
forall a. Maybe a
Nothing
unterminated Program
prog Int
depth Func
f Expr
e0 = case Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix Expr
e of
    VarExpr Lexeme Text
v
        | Just Var
var <- Text -> Map Text Var -> Maybe Var
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Lexeme Text -> Text
name Lexeme Text
v) (Func -> Map Text Var
funcVars Func
f) -> Text -> Var -> M (Maybe [Step])
local (Lexeme Text -> Text
name Lexeme Text
v) Var
var
        | Just Int
i <- Text -> [(Text, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Lexeme Text -> Text
name Lexeme Text
v) ([Text] -> [Int] -> [(Text, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Text, CType) -> Text) -> [(Text, CType)] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (Text, CType) -> Text
forall a b. (a, b) -> a
fst (Func -> [(Text, CType)]
funcParams Func
f)) [Int
0 ..]) -> Text -> Int -> M (Maybe [Step])
param (Lexeme Text -> Text
name Lexeme Text
v) Int
i
    -- What's after the start of such bytes is such bytes too.
    BinaryExpr Expr
base BinaryOp
BopPlus Expr
_ -> Program -> Int -> Func -> Expr -> M (Maybe [Step])
unterminated Program
prog Int
depth Func
f Expr
base
    UnaryExpr UnaryOp
UopAddress (Fix (ArrayAccess Expr
base Expr
_)) -> Program -> Int -> Func -> Expr -> M (Maybe [Step])
unterminated Program
prog Int
depth Func
f Expr
base
    NodeF (Lexeme Text) Expr
_ | Just (Text, Text)
fld <- Program -> Func -> Expr -> Maybe (Text, Text)
fieldOf Program
prog Func
f Expr
e -> (Text, Text) -> M (Maybe [Step])
field (Text, Text)
fld
    NodeF (Lexeme Text) Expr
_ -> Maybe [Step] -> M (Maybe [Step])
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [Step]
forall a. Maybe a
Nothing
  where
    e :: Expr
e = Expr -> Expr
stripCasts Expr
e0
    file :: FilePath
file = Func -> FilePath
funcFile Func
f
    next :: Func -> Expr -> M (Maybe [Step])
next = Program -> Int -> Func -> Expr -> M (Maybe [Step])
unterminated Program
prog (Int
depth Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

    -- A parameter: shown by a caller, if `f` doesn't change it or write
    -- what it points to. Nothing writes through a pointer to const.
    param :: Text -> Int -> M (Maybe [Step])
param Text
v Int
i
        | (Use -> Bool) -> [Use] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not (Bool -> Bool) -> (Use -> Bool) -> Use -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Use -> Bool
unchanged) (Program -> Func -> (Expr -> Bool) -> [Use]
usesIn Program
prog Func
f (Text -> Expr -> Bool
isVar Text
v)) = Maybe [Step] -> M (Maybe [Step])
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [Step]
forall a. Maybe a
Nothing
        | Bool
otherwise = Key -> M (Maybe [Step]) -> M (Maybe [Step])
remember (FuncKey -> Int -> Key
KParam (Func -> FuncKey
funcKey Func
f) Int
i) (M (Maybe [Step]) -> M (Maybe [Step]))
-> M (Maybe [Step]) -> M (Maybe [Step])
forall a b. (a -> b) -> a -> b
$ [M (Maybe [Step])] -> M (Maybe [Step])
forall a. [M (Maybe a)] -> M (Maybe a)
firstJust
            [ ([Step] -> [Step]) -> Maybe [Step] -> Maybe [Step]
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FilePath -> Expr -> Doc AnsiStyle -> Step
Step (Func -> FilePath
funcFile (CallSite -> Func
csFunc CallSite
cs)) Expr
arg (Doc AnsiStyle
"passed to" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (Text -> Doc AnsiStyle
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Func -> Text
funcName Func
f)) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"as" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (Text -> Doc AnsiStyle
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
v) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"here") Step -> [Step] -> [Step]
forall a. a -> [a] -> [a]
:)
                (Maybe [Step] -> Maybe [Step])
-> M (Maybe [Step]) -> M (Maybe [Step])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Func -> Expr -> M (Maybe [Step])
next (CallSite -> Func
csFunc CallSite
cs) Expr
arg
            | CallSite
cs <- (CallSite -> FilePath) -> [CallSite] -> [CallSite]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (Func -> FilePath
funcFile (Func -> FilePath) -> (CallSite -> Func) -> CallSite -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallSite -> Func
csFunc) (Program -> Func -> [CallSite]
callersOf Program
prog Func
f)
            , Expr
arg <- Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
1 (Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
drop Int
i (CallSite -> [Expr]
csArgs CallSite
cs))
            ]

    unchanged :: Use -> Bool
unchanged = \case
        Use
Read                               -> Bool
True
        Use
Unknown | TPtr Bool
True CType
_ <- CType
paramType -> Bool
True
        Use
_                                  -> Bool
False
      where
        paramType :: CType
paramType = CType -> Maybe CType -> CType
forall a. a -> Maybe a -> a
fromMaybe CType
TOther (Text -> [(Text, CType)] -> Maybe CType
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Expr -> Text
nameOf Expr
e) (Func -> [(Text, CType)]
funcParams Func
f))
        nameOf :: Expr -> Text
nameOf = \case
            Fix (VarExpr Lexeme Text
l) -> Lexeme Text -> Text
name Lexeme Text
l
            Expr
_               -> Text
""

    local :: Text -> Var -> M (Maybe [Step])
local Text
v Var
var = case Var -> CType
varType Var
var of
        TArray CType
_ (Just Expr
size) -> Maybe [Step] -> M (Maybe [Step])
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe [Step] -> M (Maybe [Step]))
-> Maybe [Step] -> M (Maybe [Step])
forall a b. (a -> b) -> a -> b
$ Text -> [Use] -> Expr -> Maybe [Step]
forall {a}. Pretty a => a -> [Use] -> Expr -> Maybe [Step]
filled Text
v (Program -> Func -> (Expr -> Bool) -> [Use]
usesIn Program
prog Func
f (Text -> Expr -> Bool
isVar Text
v)) Expr
size
        TPtr Bool
toConst CType
_ -> case (Program -> Func -> (Expr -> Bool) -> [Use]
usesIn Program
prog Func
f (Text -> Expr -> Bool
isVar Text
v), Text -> Var -> [Expr]
values Text
v Var
var) of
            ([Use]
uses, [Expr
value]) | Bool
toConst Bool -> Bool -> Bool
|| (Use -> Bool) -> [Use] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Use -> Bool
knownPointerUse [Use]
uses -> case Expr -> Maybe Expr
allocationSize Expr
value of
                Just Expr
size -> Maybe [Step] -> M (Maybe [Step])
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe [Step] -> M (Maybe [Step]))
-> Maybe [Step] -> M (Maybe [Step])
forall a b. (a -> b) -> a -> b
$ Text -> [Use] -> Expr -> Maybe [Step]
forall {a}. Pretty a => a -> [Use] -> Expr -> Maybe [Step]
filled Text
v [Use]
uses Expr
size
                Maybe Expr
Nothing -> ([Step] -> [Step]) -> Maybe [Step] -> Maybe [Step]
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FilePath -> Expr -> Doc AnsiStyle -> Step
Step FilePath
file Expr
value (Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (Text -> Doc AnsiStyle
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
v) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"is" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (Expr -> Doc AnsiStyle
forall a. Pretty a => Node (Lexeme a) -> Doc AnsiStyle
ppNode Expr
value) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"here") Step -> [Step] -> [Step]
forall a. a -> [a] -> [a]
:)
                    (Maybe [Step] -> Maybe [Step])
-> M (Maybe [Step]) -> M (Maybe [Step])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Func -> Expr -> M (Maybe [Step])
next Func
f Expr
value
            ([Use], [Expr])
_ -> Maybe [Step] -> M (Maybe [Step])
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [Step]
forall a. Maybe a
Nothing
        CType
_ -> Maybe [Step] -> M (Maybe [Step])
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [Step]
forall a. Maybe a
Nothing

    values :: Text -> Var -> [Expr]
values Text
v Var
var = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Bool
isNull) ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$
        Maybe Expr -> [Expr]
forall a. Maybe a -> [a]
maybeToList (Var -> Maybe Expr
varInit Var
var) [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [ Expr
value | Store Expr
_ Expr
value <- Program -> Func -> (Expr -> Bool) -> [Use]
usesIn Program
prog Func
f (Text -> Expr -> Bool
isVar Text
v) ]

    knownPointerUse :: Use -> Bool
knownPointerUse = \case
        Use
Unknown -> Bool
False
        Use
_       -> Bool
True

    -- An object filled to its `size` by a copy, and not otherwise written.
    filled :: a -> [Use] -> Expr -> Maybe [Step]
filled a
v [Use]
uses Expr
size
        | (Use -> Bool) -> [Use] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Use -> Bool
isUnknown [Use]
uses = Maybe [Step]
forall a. Maybe a
Nothing
        | Bool
otherwise = [[Step]] -> Maybe [Step]
forall a. [a] -> Maybe a
listToMaybe
            [ [ FilePath -> Expr -> Doc AnsiStyle -> Step
Step FilePath
file Expr
copy (Doc AnsiStyle
"filled with" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (Expr -> Doc AnsiStyle
forall a. Pretty a => Node (Lexeme a) -> Doc AnsiStyle
ppNode Expr
n) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"bytes here, as many as" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (a -> Doc AnsiStyle
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
v) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"holds")
              ] [Step] -> [Step] -> [Step]
forall a. [a] -> [a] -> [a]
++ [Step]
guardSteps
            | Copy Expr
copy Expr
n <- [Use]
uses
            , Program -> Func -> Expr -> Bool
copiesBytes Program
prog Func
f Expr
copy
            , Just [Step]
guardSteps <- [Program -> Func -> Expr -> Expr -> Expr -> Maybe [Step]
reaches Program
prog Func
f Expr
copy Expr
n Expr
size]
            ]

    isUnknown :: Use -> Bool
isUnknown = \case
        Use
Unknown -> Bool
True
        Use
_       -> Bool
False

    -- A field: every use of it in the program understood, and one that
    -- fills it.
    field :: (Text, Text) -> M (Maybe [Step])
field (Text
s, Text
fld) = Key -> M (Maybe [Step]) -> M (Maybe [Step])
remember (Text -> Text -> Key
KField Text
s Text
fld) (M (Maybe [Step]) -> M (Maybe [Step]))
-> M (Maybe [Step]) -> M (Maybe [Step])
forall a b. (a -> b) -> a -> b
$ do
        let uses :: [(Func, Use)]
uses = [ (Func
g, Use
u) | Func
g <- Program -> [Func]
progFuncs Program
prog, Use
u <- Program -> Func -> (Expr -> Bool) -> [Use]
usesIn Program
prog Func
g (Func -> Expr -> Bool
isField Func
g) ]
            isField :: Func -> Expr -> Bool
isField Func
g Expr
n = case Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix Expr
n of
                PointerAccess{} -> Program -> Func -> Expr -> Maybe (Text, Text)
fieldOf Program
prog Func
g Expr
n Maybe (Text, Text) -> Maybe (Text, Text) -> Bool
forall a. Eq a => a -> a -> Bool
== (Text, Text) -> Maybe (Text, Text)
forall a. a -> Maybe a
Just (Text
s, Text
fld)
                MemberAccess{}  -> Program -> Func -> Expr -> Maybe (Text, Text)
fieldOf Program
prog Func
g Expr
n Maybe (Text, Text) -> Maybe (Text, Text) -> Bool
forall a. Eq a => a -> a -> Bool
== (Text, Text) -> Maybe (Text, Text)
forall a. a -> Maybe a
Just (Text
s, Text
fld)
                NodeF (Lexeme Text) Expr
_               -> Bool
False
            describe :: Doc ann
describe = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
backticks (Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
s Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"." Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
fld)
        if ((Func, Use) -> Bool) -> [(Func, Use)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Use -> Bool
isUnknown (Use -> Bool) -> ((Func, Use) -> Use) -> (Func, Use) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Func, Use) -> Use
forall a b. (a, b) -> b
snd) [(Func, Use)]
uses then Maybe [Step] -> M (Maybe [Step])
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [Step]
forall a. Maybe a
Nothing else case Program -> Text -> Text -> CType
fieldType Program
prog Text
s Text
fld of
            TArray CType
_ (Just Expr
size) -> Maybe [Step] -> M (Maybe [Step])
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe [Step] -> M (Maybe [Step]))
-> Maybe [Step] -> M (Maybe [Step])
forall a b. (a -> b) -> a -> b
$ [[Step]] -> Maybe [Step]
forall a. [a] -> Maybe a
listToMaybe
                [ FilePath -> Expr -> Doc AnsiStyle -> Step
Step (Func -> FilePath
funcFile Func
g) Expr
copy (Doc AnsiStyle
"filled with" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (Expr -> Doc AnsiStyle
forall a. Pretty a => Node (Lexeme a) -> Doc AnsiStyle
ppNode Expr
n) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"bytes here, as many as" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
forall {ann}. Doc ann
describe Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"holds") Step -> [Step] -> [Step]
forall a. a -> [a] -> [a]
: [Step]
guardSteps
                | (Func
g, Copy Expr
copy Expr
n) <- [(Func, Use)]
uses
                , Program -> Func -> Expr -> Bool
copiesBytes Program
prog Func
g Expr
copy
                , Just [Step]
guardSteps <- [Program -> Func -> Expr -> Expr -> Expr -> Maybe [Step]
reaches Program
prog Func
g Expr
copy Expr
n Expr
size]
                ]
            TPtr Bool
_ CType
_ -> [M (Maybe [Step])] -> M (Maybe [Step])
forall a. [M (Maybe a)] -> M (Maybe a)
firstJust
                [ ([Step] -> [Step]) -> Maybe [Step] -> Maybe [Step]
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FilePath -> Expr -> Doc AnsiStyle -> Step
Step (Func -> FilePath
funcFile Func
g) Expr
assign (Doc AnsiStyle
"stored in" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
forall {ann}. Doc ann
describe Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"here") Step -> [Step] -> [Step]
forall a. a -> [a] -> [a]
:) (Maybe [Step] -> Maybe [Step])
-> M (Maybe [Step]) -> M (Maybe [Step])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Func -> Expr -> M (Maybe [Step])
next Func
g Expr
value
                | (Func
g, Store Expr
assign Expr
value) <- [(Func, Use)]
uses
                , Bool -> Bool
not (Expr -> Bool
isNull Expr
value)
                ]
            CType
_ -> Maybe [Step] -> M (Maybe [Step])
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [Step]
forall a. Maybe a
Nothing

-- | Whether the copy `copy` of `n` bytes, in `f`, can fill `size` bytes: `n`
-- is `size`, or is only kept from being more than it.
reaches :: Program -> Func -> Expr -> Expr -> Expr -> Maybe [Step]
reaches :: Program -> Func -> Expr -> Expr -> Expr -> Maybe [Step]
reaches Program
prog Func
f Expr
copy Expr
n Expr
size
    | Program -> Expr -> Expr -> Bool
sameValue Program
prog Expr
n Expr
size = [Step] -> Maybe [Step]
forall a. a -> Maybe a
Just []
    | Fix (VarExpr Lexeme Text
v) <- Expr -> Expr
stripCasts Expr
n = [[Step]] -> Maybe [Step]
forall a. [a] -> Maybe a
listToMaybe
        [ [ FilePath -> Expr -> Doc AnsiStyle -> Step
Step (Func -> FilePath
funcFile Func
f) Expr
guard (Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (Text -> Doc AnsiStyle
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Lexeme Text -> Text
name Lexeme Text
v)) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"can be" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (Expr -> Doc AnsiStyle
forall a. Pretty a => Node (Lexeme a) -> Doc AnsiStyle
ppNode Expr
bound) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"after this") ]
        | Fix (IfStmt Expr
cond Expr
body Maybe Expr
_) <- (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
forall {lexeme}. Fix (NodeF lexeme) -> Fix (NodeF lexeme)
uncomment (Expr -> [Expr]
earlier Expr
copy)
        , Expr -> Bool
forall {lexeme}. Fix (NodeF lexeme) -> Bool
exits Expr
body
        , Expr
guard <- Expr -> [Expr]
disjuncts Expr
cond
        , Just Expr
bound <- [Text -> Expr -> Maybe Expr
atMost (Lexeme Text -> Text
name Lexeme Text
v) Expr
guard]
        , Program -> Expr -> Expr -> Bool
sameValue Program
prog Expr
bound Expr
size
        ]
    | Bool
otherwise = Maybe [Step]
forall a. Maybe a
Nothing
  where
    uncomment :: Fix (NodeF lexeme) -> Fix (NodeF lexeme)
uncomment = \case
        Fix (Commented Fix (NodeF lexeme)
_ Fix (NodeF lexeme)
stmt) -> Fix (NodeF lexeme) -> Fix (NodeF lexeme)
uncomment Fix (NodeF lexeme)
stmt
        Fix (NodeF lexeme)
stmt                   -> Fix (NodeF lexeme)
stmt

    -- The statements before `node` in the blocks it's in: run before it.
    earlier :: Expr -> [Expr]
earlier Expr
node =
        [ Expr
stmt
        | (Expr
found, [Expr]
ps) <- Int -> [(Expr, [Expr])] -> [(Expr, [Expr])]
forall a. Int -> [a] -> [a]
take Int
1 [ (Expr, [Expr])
p | p :: (Expr, [Expr])
p@(Expr
n', [Expr]
_) <- Expr -> [(Expr, [Expr])]
withParents (Func -> Expr
funcBody Func
f), Expr
n' Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
node ]
        , (Expr
child, Fix (CompoundStmt [Expr]
stmts)) <- [Expr] -> [Expr] -> [(Expr, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Expr
found Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr]
ps) [Expr]
ps
        , Expr
stmt <- (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
child) [Expr]
stmts
        ]

    atMost :: Text -> Expr -> Maybe Expr
atMost Text
v (Fix (BinaryExpr Expr
a BinaryOp
BopGt Expr
b)) | Text -> Expr -> Bool
isVar Text
v (Expr -> Expr
stripCasts Expr
a) = Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
b
    atMost Text
v (Fix (BinaryExpr Expr
a BinaryOp
BopLt Expr
b)) | Text -> Expr -> Bool
isVar Text
v (Expr -> Expr
stripCasts Expr
b) = Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
a
    atMost Text
_ Expr
_ = Maybe Expr
forall a. Maybe a
Nothing

    disjuncts :: Expr -> [Expr]
disjuncts Expr
x = case Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix (Expr -> Expr
stripCasts Expr
x) of
        BinaryExpr Expr
a BinaryOp
BopOr Expr
b -> Expr -> [Expr]
disjuncts Expr
a [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ Expr -> [Expr]
disjuncts Expr
b
        NodeF (Lexeme Text) Expr
_                    -> [Expr -> Expr
stripCasts Expr
x]

    exits :: Fix (NodeF lexeme) -> Bool
exits = \case
        Fix (CompoundStmt [Fix (NodeF lexeme)]
stmts) | Bool -> Bool
not ([Fix (NodeF lexeme)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Fix (NodeF lexeme)]
stmts) -> Fix (NodeF lexeme) -> Bool
exits ([Fix (NodeF lexeme)] -> Fix (NodeF lexeme)
forall a. HasCallStack => [a] -> a
last [Fix (NodeF lexeme)]
stmts)
        Fix Return{}                                -> Bool
True
        Fix Goto{}                                  -> Bool
True
        Fix (NodeF lexeme)
_                                           -> Bool
False


-- | Whether the `memcpy` call `copy`, in `f`, copies from bytes, not text,
-- which could bring a NUL of its own.
copiesBytes :: Program -> Func -> Expr -> Bool
copiesBytes :: Program -> Func -> Expr -> Bool
copiesBytes Program
prog Func
f = \case
    Fix (FunctionCall Expr
_ [Expr
_, Expr
src, Expr
_]) -> case Program -> Func -> Expr -> CType
typeIn Program
prog Func
f (Expr -> Expr
stripCasts Expr
src) of
        TPtr Bool
_ CType
TByte   -> Bool
True
        TArray CType
TByte Maybe Expr
_ -> Bool
True
        CType
_              -> Bool
False
    Expr
_ -> Bool
False

-- * Bytes nothing writes

-- | How `arg`, in `f`, can point to bytes nothing wrote.
unwritten :: Program -> Func -> Expr -> M (Maybe Proof)
unwritten :: Program -> Func -> Expr -> M (Maybe Proof)
unwritten Program
prog Func
f Expr
arg = case Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix (Expr -> Expr
stripCasts Expr
arg) of
    FunctionCall Expr
callee [Expr]
args | Just Text
fn <- Expr -> Maybe Text
callName Expr
callee -> [M (Maybe Proof)] -> M (Maybe Proof)
forall a. [M (Maybe a)] -> M (Maybe a)
firstJust
        [ (Proof -> Proof) -> Maybe Proof -> Maybe Proof
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\([Step]
steps, [Cond]
conds) -> (FilePath -> Expr -> Doc AnsiStyle -> Step
Step (Func -> FilePath
funcFile Func
f) Expr
a (Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (Text -> Doc AnsiStyle
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
o) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"is passed here before anything writes it") Step -> [Step] -> [Step]
forall a. a -> [a] -> [a]
: FilePath -> Expr -> Doc AnsiStyle -> Step
Step (Func -> FilePath
funcFile Func
g) Expr
ret (Doc AnsiStyle
"returning" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (Expr -> Doc AnsiStyle
forall a. Pretty a => Node (Lexeme a) -> Doc AnsiStyle
ppNode Expr
retVal)) Step -> [Step] -> [Step]
forall a. a -> [a] -> [a]
: [Step]
steps, Func -> [Cond]
funcConds Func
f [Cond] -> [Cond] -> [Cond]
forall a. [a] -> [a] -> [a]
++ [Cond]
inside [Cond] -> [Cond] -> [Cond]
forall a. [a] -> [a] -> [a]
++ [Cond]
conds))
            (Maybe Proof -> Maybe Proof) -> M (Maybe Proof) -> M (Maybe Proof)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Program -> Func -> Int -> Maybe Text -> M (Maybe Proof)
unwrittenIn Program
prog Func
g Int
i Maybe Text
fld
        | Func
g <- Program -> FilePath -> Text -> [Func]
definitionsOf Program
prog (Func -> FilePath
funcFile Func
f) Text
fn
        , Just (Int
i, Maybe Text
fld, Expr
ret, Expr
retVal) <- [Program -> Func -> Maybe (Int, Maybe Text, Expr, Expr)
returnsParam Program
prog Func
g]
        , Expr
a <- Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
1 (Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
drop Int
i [Expr]
args)
        , Just Text
o <- [Maybe Text -> Expr -> Maybe Text
forall {a}. Maybe a -> Expr -> Maybe Text
fresh Maybe Text
fld (Expr -> Expr
stripCasts Expr
a)]
        ]
    NodeF (Lexeme Text) Expr
_ -> Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Proof
forall a. Maybe a
Nothing
  where
    inside :: [Cond]
inside =
        [ FilePath -> Bool -> Expr -> Cond
Cond (Func -> FilePath
funcFile Func
f) Bool
holds Expr
c
        | (Expr
found, [Expr]
ps) <- Int -> [(Expr, [Expr])] -> [(Expr, [Expr])]
forall a. Int -> [a] -> [a]
take Int
1 [ (Expr, [Expr])
x | x :: (Expr, [Expr])
x@(Expr
n, [Expr]
_) <- Expr -> [(Expr, [Expr])]
withParents (Func -> Expr
funcBody Func
f), Expr
n Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
arg ]
        , (Expr
child, Expr
parent) <- [Expr] -> [Expr] -> [(Expr, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Expr
found Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr]
ps) [Expr]
ps
        , (Expr
c, [Expr]
ts, Bool
holds') <- case Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix Expr
parent of
            PreprocIf Expr
c [Expr]
ts Expr
_     -> [(Expr
c, [Expr]
ts, Bool
True)]
            PreprocElif Expr
c [Expr]
ts Expr
_   -> [(Expr
c, [Expr]
ts, Bool
True)]
            PreprocIfdef Lexeme Text
l [Expr]
ts Expr
_  -> [(NodeF (Lexeme Text) Expr -> Expr
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (Lexeme Text -> NodeF (Lexeme Text) Expr
forall lexeme a. lexeme -> NodeF lexeme a
PreprocDefined Lexeme Text
l), [Expr]
ts, Bool
True)]
            PreprocIfndef Lexeme Text
l [Expr]
ts Expr
_ -> [(NodeF (Lexeme Text) Expr -> Expr
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (Lexeme Text -> NodeF (Lexeme Text) Expr
forall lexeme a. lexeme -> NodeF lexeme a
PreprocDefined Lexeme Text
l), [Expr]
ts, Bool
False)]
            NodeF (Lexeme Text) Expr
_                    -> []
        , let holds :: Bool
holds = if Expr
child Expr -> [Expr] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Expr]
ts then Bool
holds' else Bool -> Bool
not Bool
holds'
        ]

    fresh :: Maybe a -> Expr -> Maybe Text
fresh Maybe a
fld Expr
a = case (Maybe a
fld, Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix Expr
a) of
        (Just a
_, UnaryExpr UnaryOp
UopAddress v :: Expr
v@(Fix (VarExpr Lexeme Text
o)))
            | Just (TStruct Text
_, Expr
decl) <- Text -> Expr -> Maybe (CType, Expr)
declaration (Lexeme Text -> Text
name Lexeme Text
o) Expr
v, Expr -> Expr -> Bool
unusedSince Expr
decl Expr
v -> Text -> Maybe Text
forall a. a -> Maybe a
Just (Lexeme Text -> Text
name Lexeme Text
o)
        (Maybe a
Nothing, VarExpr Lexeme Text
o)
            | Just (TArray{}, Expr
decl) <- Text -> Expr -> Maybe (CType, Expr)
declaration (Lexeme Text -> Text
name Lexeme Text
o) Expr
a, Expr -> Expr -> Bool
unusedSince Expr
decl Expr
a -> Text -> Maybe Text
forall a. a -> Maybe a
Just (Lexeme Text -> Text
name Lexeme Text
o)
        (Maybe a, NodeF (Lexeme Text) Expr)
_ -> Maybe Text
forall a. Maybe a
Nothing

    declaration :: Text -> Expr -> Maybe (CType, Expr)
declaration Text
o Expr
use = case
        [ (Expr
ty, [Expr]
arrs, Maybe Expr
i, Expr
d)
        | (Expr
found, [Expr]
ps) <- Int -> [(Expr, [Expr])] -> [(Expr, [Expr])]
forall a. Int -> [a] -> [a]
take Int
1 [ (Expr, [Expr])
x | x :: (Expr, [Expr])
x@(Expr
n, [Expr]
_) <- Expr -> [(Expr, [Expr])]
withParents (Func -> Expr
funcBody Func
f), Expr
n Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
use ]
        , (Expr
child, Fix (CompoundStmt [Expr]
stmts)) <- [Expr] -> [Expr] -> [(Expr, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Expr
found Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr]
ps) [Expr]
ps
        , d :: Expr
d@(Fix (VarDeclStmt (Fix (VarDecl Expr
ty Lexeme Text
v [Expr]
arrs)) Maybe Expr
i)) <- [Expr] -> [Expr]
forall a. [a] -> [a]
reverse ((Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
child) [Expr]
stmts)
        , Lexeme Text -> Text
name Lexeme Text
v Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
o
        ] of
        (Expr
ty, [Expr]
arrs, Maybe Expr
Nothing, Expr
d) : [(Expr, [Expr], Maybe Expr, Expr)]
_ -> (CType, Expr) -> Maybe (CType, Expr)
forall a. a -> Maybe a
Just (CType -> [Expr] -> CType
withArrays (Map Text CType -> Expr -> CType
cimpleType (Program -> Map Text CType
progTypedefs Program
prog) Expr
ty) [Expr]
arrs, Expr
d)
        [(Expr, [Expr], Maybe Expr, Expr)]
_                          -> Maybe (CType, Expr)
forall a. Maybe a
Nothing

    unusedSince :: Expr -> Expr -> Bool
unusedSince Expr
decl Expr
use = [Expr] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null
        [ Expr
n
        | Expr
n <- Expr -> [Expr]
universe (Func -> Expr
funcBody Func
f)
        , Text -> Expr -> Bool
isVar (Expr -> Text
varName Expr
use) Expr
n
        , Expr
n Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
use
        , Expr -> CimplePos
pos Expr
decl CimplePos -> CimplePos -> Bool
forall a. Ord a => a -> a -> Bool
< Expr -> CimplePos
pos Expr
n, Expr -> CimplePos
pos Expr
n CimplePos -> CimplePos -> Bool
forall a. Ord a => a -> a -> Bool
< Expr -> CimplePos
pos Expr
use
        ]
    varName :: Expr -> Text
varName = \case
        Fix (VarExpr Lexeme Text
v) -> Lexeme Text -> Text
name Lexeme Text
v
        Expr
_               -> Text
""
    pos :: Expr -> CimplePos
pos = (CimplePos, Int) -> CimplePos
forall a b. (a, b) -> a
fst ((CimplePos, Int) -> CimplePos)
-> (Expr -> (CimplePos, Int)) -> Expr -> CimplePos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Expr -> (CimplePos, Int)
nodePosAndLen FilePath
""

-- | The parameter (and field) every `return` of `g` returns.
returnsParam :: Program -> Func -> Maybe (Int, Maybe Text, Expr, Expr)
returnsParam :: Program -> Func -> Maybe (Int, Maybe Text, Expr, Expr)
returnsParam Program
prog Func
g = case [ (Expr
r, Expr
v) | r :: Expr
r@(Fix (Return (Just Expr
v))) <- Expr -> [Expr]
universe (Func -> Expr
funcBody Func
g) ] of
    returns :: [(Expr, Expr)]
returns@((Expr
ret, Expr
retVal) : [(Expr, Expr)]
_) -> case ((Expr, Expr) -> Maybe (Int, Maybe Text))
-> [(Expr, Expr)] -> [Maybe (Int, Maybe Text)]
forall a b. (a -> b) -> [a] -> [b]
map (Expr -> Maybe (Int, Maybe Text)
aliasOf (Expr -> Maybe (Int, Maybe Text))
-> ((Expr, Expr) -> Expr)
-> (Expr, Expr)
-> Maybe (Int, Maybe Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
stripCasts (Expr -> Expr) -> ((Expr, Expr) -> Expr) -> (Expr, Expr) -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, Expr) -> Expr
forall a b. (a, b) -> b
snd) [(Expr, Expr)]
returns of
        Just (Int, Maybe Text)
alias : [Maybe (Int, Maybe Text)]
rest | (Maybe (Int, Maybe Text) -> Bool)
-> [Maybe (Int, Maybe Text)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe (Int, Maybe Text) -> Maybe (Int, Maybe Text) -> Bool
forall a. Eq a => a -> a -> Bool
== (Int, Maybe Text) -> Maybe (Int, Maybe Text)
forall a. a -> Maybe a
Just (Int, Maybe Text)
alias) [Maybe (Int, Maybe Text)]
rest -> let (Int
i, Maybe Text
fld) = (Int, Maybe Text)
alias in (Int, Maybe Text, Expr, Expr)
-> Maybe (Int, Maybe Text, Expr, Expr)
forall a. a -> Maybe a
Just (Int
i, Maybe Text
fld, Expr
ret, Expr
retVal)
        [Maybe (Int, Maybe Text)]
_ -> Maybe (Int, Maybe Text, Expr, Expr)
forall a. Maybe a
Nothing
    [] -> Maybe (Int, Maybe Text, Expr, Expr)
forall a. Maybe a
Nothing
  where
    params :: [(Text, Int)]
params = [Text] -> [Int] -> [(Text, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Text, CType) -> Text) -> [(Text, CType)] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (Text, CType) -> Text
forall a b. (a, b) -> a
fst (Func -> [(Text, CType)]
funcParams Func
g)) [Int
0 ..]
    aliasOf :: Expr -> Maybe (Int, Maybe Text)
aliasOf = \case
        Fix (VarExpr Lexeme Text
p) -> (\Int
i -> (Int
i, Maybe Text
forall a. Maybe a
Nothing)) (Int -> (Int, Maybe Text)) -> Maybe Int -> Maybe (Int, Maybe Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> [(Text, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Lexeme Text -> Text
name Lexeme Text
p) [(Text, Int)]
params
        Fix (PointerAccess (Fix (VarExpr Lexeme Text
p)) Lexeme Text
fld)
            | Just Int
i <- Text -> [(Text, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Lexeme Text -> Text
name Lexeme Text
p) [(Text, Int)]
params
            , TPtr Bool
_ (TStruct Text
s) <- (Text, CType) -> CType
forall a b. (a, b) -> b
snd (Func -> [(Text, CType)]
funcParams Func
g [(Text, CType)] -> Int -> (Text, CType)
forall a. HasCallStack => [a] -> Int -> a
!! Int
i)
            , TArray{} <- Program -> Text -> Text -> CType
fieldType Program
prog Text
s (Lexeme Text -> Text
name Lexeme Text
fld) -> (Int, Maybe Text) -> Maybe (Int, Maybe Text)
forall a. a -> Maybe a
Just (Int
i, Text -> Maybe Text
forall a. a -> Maybe a
Just (Lexeme Text -> Text
name Lexeme Text
fld))
        Expr
_ -> Maybe (Int, Maybe Text)
forall a. Maybe a
Nothing

-- | How `g` can return without writing what parameter `i` (field `fld`)
-- points to, on a path no caller decides.
unwrittenIn :: Program -> Func -> Int -> Maybe Text -> M (Maybe Proof)
unwrittenIn :: Program -> Func -> Int -> Maybe Text -> M (Maybe Proof)
unwrittenIn Program
prog Func
g Int
i Maybe Text
fld = case Int -> [(Text, CType)] -> [(Text, CType)]
forall a. Int -> [a] -> [a]
drop Int
i (Func -> [(Text, CType)]
funcParams Func
g) of
    [] -> Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Proof
forall a. Maybe a
Nothing
    (Text
p, CType
_) : [(Text, CType)]
_ -> do
        let key :: UnwrittenKey
key = Int -> Int -> Maybe Text -> UnwrittenKey
UnwrittenKey (Func -> Int
funcId Func
g) Int
i Maybe Text
fld
        Maybe (Maybe Proof)
done <- (Memo -> Maybe (Maybe Proof))
-> StateT Memo Identity (Maybe (Maybe Proof))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (UnwrittenKey
-> Map UnwrittenKey (Maybe Proof) -> Maybe (Maybe Proof)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup UnwrittenKey
key (Map UnwrittenKey (Maybe Proof) -> Maybe (Maybe Proof))
-> (Memo -> Map UnwrittenKey (Maybe Proof))
-> Memo
-> Maybe (Maybe Proof)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Memo -> Map UnwrittenKey (Maybe Proof)
memoUnwritten)
        Bool
busy <- (Memo -> Bool) -> StateT Memo Identity Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (UnwrittenKey -> Set UnwrittenKey -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member UnwrittenKey
key (Set UnwrittenKey -> Bool)
-> (Memo -> Set UnwrittenKey) -> Memo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Memo -> Set UnwrittenKey
memoBusy)
        case Maybe (Maybe Proof)
done of
            Just Maybe Proof
r -> Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Proof
r
            Maybe (Maybe Proof)
Nothing | Bool
busy -> Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Proof
forall a. Maybe a
Nothing
            Maybe (Maybe Proof)
Nothing -> do
                (Memo -> Memo) -> StateT Memo Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Memo -> Memo) -> StateT Memo Identity ())
-> (Memo -> Memo) -> StateT Memo Identity ()
forall a b. (a -> b) -> a -> b
$ \Memo
m -> Memo
m{memoBusy = Set.insert key (memoBusy m)}
                Maybe Proof
r <- (Proof -> Proof) -> Maybe Proof -> Maybe Proof
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\([Step]
steps, [Cond]
conds) -> ([Step]
steps, Func -> [Cond]
funcConds Func
g [Cond] -> [Cond] -> [Cond]
forall a. [a] -> [a] -> [a]
++ [Cond]
conds)) (Maybe Proof -> Maybe Proof) -> M (Maybe Proof) -> M (Maybe Proof)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> [Expr] -> M (Maybe Proof) -> M (Maybe Proof)
through Text
p [Func -> Expr
funcBody Func
g] (Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof -> Maybe Proof
forall a. a -> Maybe a
Just Proof
forall a. Monoid a => a
mempty))
                (Memo -> Memo) -> StateT Memo Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Memo -> Memo) -> StateT Memo Identity ())
-> (Memo -> Memo) -> StateT Memo Identity ()
forall a b. (a -> b) -> a -> b
$ \Memo
m -> Memo
m{memoUnwritten = Map.insert key r (memoUnwritten m), memoBusy = Set.delete key (memoBusy m)}
                Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Proof
r
  where
    file :: FilePath
file = Func -> FilePath
funcFile Func
g

    through :: Text -> [Expr] -> M (Maybe Proof) -> M (Maybe Proof)
    through :: Text -> [Expr] -> M (Maybe Proof) -> M (Maybe Proof)
through Text
_ [] M (Maybe Proof)
k = M (Maybe Proof)
k
    through Text
p (Expr
st : [Expr]
ss) M (Maybe Proof)
k = case Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix Expr
st of
        Commented Expr
_ Expr
st' -> Text -> [Expr] -> M (Maybe Proof) -> M (Maybe Proof)
through Text
p (Expr
st' Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr]
ss) M (Maybe Proof)
k
        CompoundStmt [Expr]
xs -> Text -> [Expr] -> M (Maybe Proof) -> M (Maybe Proof)
through Text
p [Expr]
xs (Text -> [Expr] -> M (Maybe Proof) -> M (Maybe Proof)
through Text
p [Expr]
ss M (Maybe Proof)
k)
        ExprStmt Expr
e -> Text -> Expr -> M (Maybe Proof)
effects Text
p Expr
e M (Maybe Proof) -> M (Maybe Proof) -> M (Maybe Proof)
forall {m :: * -> *} {a}.
(Monad m, Semigroup a) =>
m (Maybe a) -> m (Maybe a) -> m (Maybe a)
`andThen` Text -> [Expr] -> M (Maybe Proof) -> M (Maybe Proof)
through Text
p [Expr]
ss M (Maybe Proof)
k
        VarDeclStmt (Fix (VarDecl Expr
ty Lexeme Text
_ [Expr]
_)) (Just Expr
e)
            | Text -> Expr -> Bool
aliases Text
p Expr
e, Bool -> Bool
not (Expr -> Bool
readOnly Expr
ty) -> Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Proof
forall a. Maybe a
Nothing
            | Bool
otherwise -> Text -> Expr -> M (Maybe Proof)
effects Text
p Expr
e M (Maybe Proof) -> M (Maybe Proof) -> M (Maybe Proof)
forall {m :: * -> *} {a}.
(Monad m, Semigroup a) =>
m (Maybe a) -> m (Maybe a) -> m (Maybe a)
`andThen` Text -> [Expr] -> M (Maybe Proof) -> M (Maybe Proof)
through Text
p [Expr]
ss M (Maybe Proof)
k
        Return (Just Expr
e) -> Text -> Expr -> M (Maybe Proof)
effects Text
p Expr
e M (Maybe Proof) -> M (Maybe Proof) -> M (Maybe Proof)
forall {m :: * -> *} {a}.
(Monad m, Semigroup a) =>
m (Maybe a) -> m (Maybe a) -> m (Maybe a)
`andThen` Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof -> Maybe Proof
forall a. a -> Maybe a
Just Proof
forall a. Monoid a => a
mempty)
        Return Maybe Expr
Nothing -> Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof -> Maybe Proof
forall a. a -> Maybe a
Just Proof
forall a. Monoid a => a
mempty)
        IfStmt Expr
c Expr
t Maybe Expr
e -> Text -> Expr -> M (Maybe Proof)
effects Text
p Expr
c M (Maybe Proof) -> M (Maybe Proof) -> M (Maybe Proof)
forall {m :: * -> *} {a}.
(Monad m, Semigroup a) =>
m (Maybe a) -> m (Maybe a) -> m (Maybe a)
`andThen` do
            Maybe Proof
rest <- Text -> [Expr] -> M (Maybe Proof) -> M (Maybe Proof)
through Text
p [Expr]
ss M (Maybe Proof)
k
            if Text -> Expr -> Bool
untouched Text
p Expr
st then Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Proof
rest
            else if Expr -> Bool
uncontrolled Expr
c then [M (Maybe Proof)] -> M (Maybe Proof)
forall a. [M (Maybe a)] -> M (Maybe a)
firstJust
                [ Text -> [Expr] -> M (Maybe Proof) -> M (Maybe Proof)
through Text
p (Maybe Expr -> [Expr]
forall a. Maybe a -> [a]
maybeToList Maybe Expr
e) (Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Proof
rest) M (Maybe Proof) -> Step -> M (Maybe Proof)
forall {f :: * -> *} {f :: * -> *} {a} {b}.
(Functor f, Functor f) =>
f (f ([a], b)) -> a -> f (f ([a], b))
`withStep` FilePath -> Expr -> Doc AnsiStyle -> Step
Step FilePath
file Expr
c (Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (Expr -> Doc AnsiStyle
forall a. Pretty a => Node (Lexeme a) -> Doc AnsiStyle
ppNode Expr
c) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"can be false here")
                , Text -> [Expr] -> M (Maybe Proof) -> M (Maybe Proof)
through Text
p [Expr
t] (Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Proof
rest) M (Maybe Proof) -> Step -> M (Maybe Proof)
forall {f :: * -> *} {f :: * -> *} {a} {b}.
(Functor f, Functor f) =>
f (f ([a], b)) -> a -> f (f ([a], b))
`withStep` FilePath -> Expr -> Doc AnsiStyle -> Step
Step FilePath
file Expr
c (Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (Expr -> Doc AnsiStyle
forall a. Pretty a => Node (Lexeme a) -> Doc AnsiStyle
ppNode Expr
c) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"can be true here")
                ]
            else Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Proof
forall a. Maybe a
Nothing
        NodeF (Lexeme Text) Expr
_ | Text -> Expr -> Bool
untouched Text
p Expr
st -> Text -> [Expr] -> M (Maybe Proof) -> M (Maybe Proof)
through Text
p [Expr]
ss M (Maybe Proof)
k
        NodeF (Lexeme Text) Expr
_ -> Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Proof
forall a. Maybe a
Nothing

    withStep :: f (f ([a], b)) -> a -> f (f ([a], b))
withStep f (f ([a], b))
act a
st = (([a], b) -> ([a], b)) -> f ([a], b) -> f ([a], b)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\([a]
steps, b
conds) -> (a
st a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
steps, b
conds)) (f ([a], b) -> f ([a], b)) -> f (f ([a], b)) -> f (f ([a], b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f ([a], b))
act

    andThen :: m (Maybe a) -> m (Maybe a) -> m (Maybe a)
andThen m (Maybe a)
a m (Maybe a)
b = m (Maybe a)
a m (Maybe a) -> (Maybe a -> m (Maybe a)) -> m (Maybe a)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe a
Nothing -> Maybe a -> m (Maybe a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe a
forall a. Maybe a
Nothing
        Just a
x  -> (a -> a) -> Maybe a -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
<>) (Maybe a -> Maybe a) -> m (Maybe a) -> m (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe a)
b

    readOnly :: Expr -> Bool
readOnly Expr
ty = case Map Text CType -> Expr -> CType
cimpleType (Program -> Map Text CType
progTypedefs Program
prog) Expr
ty of
        TPtr Bool
True CType
_ -> Bool
True
        CType
_           -> Bool
False

    into :: Text -> Expr -> Bool
into Text
p Expr
x = case (Maybe Text
fld, Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix (Expr -> Expr
stripCasts Expr
x)) of
        (Maybe Text
Nothing, VarExpr Lexeme Text
v) -> Lexeme Text -> Text
name Lexeme Text
v Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
p
        (Just Text
f, PointerAccess (Fix (VarExpr Lexeme Text
v)) Lexeme Text
f') -> Lexeme Text -> Text
name Lexeme Text
v Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
p Bool -> Bool -> Bool
&& Lexeme Text -> Text
name Lexeme Text
f' Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
f
        (Maybe Text
_, BinaryExpr Expr
base BinaryOp
BopPlus Expr
_) -> Text -> Expr -> Bool
into Text
p Expr
base
        (Maybe Text
_, UnaryExpr UnaryOp
UopAddress (Fix (ArrayAccess Expr
base Expr
_))) -> Text -> Expr -> Bool
into Text
p Expr
base
        (Maybe Text, NodeF (Lexeme Text) Expr)
_ -> Bool
False
    whole :: Text -> Expr -> Bool
whole Text
p Expr
x = case (Maybe Text
fld, Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix (Expr -> Expr
stripCasts Expr
x)) of
        (Just Text
_, VarExpr Lexeme Text
v) -> Lexeme Text -> Text
name Lexeme Text
v Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
p
        (Maybe Text, NodeF (Lexeme Text) Expr)
_                   -> Bool
False
    aliases :: Text -> Expr -> Bool
aliases Text
p Expr
x = Text -> Expr -> Bool
into Text
p Expr
x Bool -> Bool -> Bool
|| Text -> Expr -> Bool
whole Text
p Expr
x

    writes :: Text -> Expr -> Bool
writes Text
p Expr
lhs = case Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix (Expr -> Expr
stripCasts Expr
lhs) of
        VarExpr Lexeme Text
v               -> Lexeme Text -> Text
name Lexeme Text
v Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
p
        ArrayAccess Expr
base Expr
_      -> Text -> Expr -> Bool
into Text
p Expr
base
        UnaryExpr UnaryOp
UopDeref Expr
base -> Text -> Expr -> Bool
aliases Text
p Expr
base
        NodeF (Lexeme Text) Expr
_                       -> Bool
False

    untouched :: Text -> Expr -> Bool
untouched Text
p Expr
st = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
        [ case Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix Expr
n of
            AssignExpr Expr
lhs AssignOp
_ Expr
_ -> Bool -> Bool
not (Text -> Expr -> Bool
writes Text
p Expr
lhs)
            UnaryExpr UnaryOp
op Expr
x | UnaryOp
op UnaryOp -> [UnaryOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [UnaryOp
UopIncr, UnaryOp
UopDecr] -> Bool -> Bool
not (Text -> Expr -> Bool
writes Text
p Expr
x)
            FunctionCall Expr
_ [Expr]
args -> Bool -> Bool
not ((Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Text -> Expr -> Bool
aliases Text
p) [Expr]
args)
            VarDeclStmt (Fix (VarDecl Expr
ty Lexeme Text
_ [Expr]
_)) (Just Expr
e) -> Expr -> Bool
readOnly Expr
ty Bool -> Bool -> Bool
|| Bool -> Bool
not (Text -> Expr -> Bool
aliases Text
p Expr
e)
            NodeF (Lexeme Text) Expr
_ -> Bool
True
        | Expr
n <- Expr -> [Expr]
universe Expr
st
        ]

    -- On `errno`, or on what functions outside the program returned.
    uncontrolled :: Expr -> Bool
uncontrolled Expr
c = case Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix (Expr -> Expr
stripCasts Expr
c) of
        LiteralExpr{} -> Bool
True
        VarExpr Lexeme Text
v
            | Lexeme Text -> Text
name Lexeme Text
v Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"errno" -> Bool
True
            | Just (Var CType
_ (Just Expr
e)) <- Text -> Map Text Var -> Maybe Var
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Lexeme Text -> Text
name Lexeme Text
v) (Func -> Map Text Var
funcVars Func
g) -> Expr -> Bool
outside Expr
e Bool -> Bool -> Bool
&& Bool -> Bool
not (Text -> Bool
assigned (Lexeme Text -> Text
name Lexeme Text
v))
        FunctionCall{} -> Expr -> Bool
outside Expr
c
        NodeF (Lexeme Text) Expr
x -> Bool -> Bool
not (NodeF (Lexeme Text) Expr -> Bool
forall a. NodeF (Lexeme Text) a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null NodeF (Lexeme Text) Expr
x) Bool -> Bool -> Bool
&& (Expr -> Bool) -> NodeF (Lexeme Text) Expr -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
uncontrolled NodeF (Lexeme Text) Expr
x
    outside :: Expr -> Bool
outside Expr
e = case Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix (Expr -> Expr
stripCasts Expr
e) of
        FunctionCall Expr
callee [Expr]
args | Just Text
fn <- Expr -> Maybe Text
callName Expr
callee -> [Func] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Program -> FilePath -> Text -> [Func]
definitionsOf Program
prog FilePath
file Text
fn) Bool -> Bool -> Bool
&& (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
uncontrolled [Expr]
args
        NodeF (Lexeme Text) Expr
_ -> Bool
False
    assigned :: Text -> Bool
assigned Text
v = Bool -> Bool
not ([()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ () | Fix (AssignExpr Expr
lhs AssignOp
_ Expr
_) <- Expr -> [Expr]
universe (Func -> Expr
funcBody Func
g), Text -> Expr -> Bool
isVar Text
v Expr
lhs ])

    effects :: Text -> Expr -> M (Maybe Proof)
effects Text
p Expr
e = (Expr -> M (Maybe Proof) -> M (Maybe Proof))
-> M (Maybe Proof) -> [Expr] -> M (Maybe Proof)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (M (Maybe Proof) -> M (Maybe Proof) -> M (Maybe Proof)
forall {m :: * -> *} {a}.
(Monad m, Semigroup a) =>
m (Maybe a) -> m (Maybe a) -> m (Maybe a)
andThen (M (Maybe Proof) -> M (Maybe Proof) -> M (Maybe Proof))
-> (Expr -> M (Maybe Proof))
-> Expr
-> M (Maybe Proof)
-> M (Maybe Proof)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Expr -> M (Maybe Proof)
effect Text
p) (Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof -> Maybe Proof
forall a. a -> Maybe a
Just Proof
forall a. Monoid a => a
mempty)) (Expr -> [Expr]
universe Expr
e)

    effect :: Text -> Expr -> M (Maybe Proof)
effect Text
p Expr
n = case Expr -> NodeF (Lexeme Text) Expr
forall (f :: * -> *). Fix f -> f (Fix f)
unFix Expr
n of
        AssignExpr Expr
lhs AssignOp
_ Expr
_ | Text -> Expr -> Bool
writes Text
p Expr
lhs -> Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Proof
forall a. Maybe a
Nothing
        UnaryExpr UnaryOp
op Expr
x | UnaryOp
op UnaryOp -> [UnaryOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [UnaryOp
UopIncr, UnaryOp
UopDecr], Text -> Expr -> Bool
writes Text
p Expr
x -> Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Proof
forall a. Maybe a
Nothing
        FunctionCall Expr
callee [Expr]
args -> (M (Maybe Proof) -> M (Maybe Proof) -> M (Maybe Proof))
-> M (Maybe Proof) -> [M (Maybe Proof)] -> M (Maybe Proof)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr M (Maybe Proof) -> M (Maybe Proof) -> M (Maybe Proof)
forall {m :: * -> *} {a}.
(Monad m, Semigroup a) =>
m (Maybe a) -> m (Maybe a) -> m (Maybe a)
andThen (Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof -> Maybe Proof
forall a. a -> Maybe a
Just Proof
forall a. Monoid a => a
mempty))
            [ Expr -> Expr -> Int -> Expr -> M (Maybe Proof)
passed Expr
n Expr
callee Int
j Expr
a | (Int
j, Expr
a) <- [Int] -> [Expr] -> [(Int, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [Expr]
args, Text -> Expr -> Bool
aliases Text
p Expr
a ]
        NodeF (Lexeme Text) Expr
_ -> Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof -> Maybe Proof
forall a. a -> Maybe a
Just Proof
forall a. Monoid a => a
mempty)
      where
        passed :: Expr -> Expr -> Int -> Expr -> M (Maybe Proof)
passed Expr
call Expr
callee Int
j Expr
a = case Expr -> Maybe Text
callName Expr
callee of
            Just Text
fn
                | Text
fn Text -> [Text] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text
"strlen", Text
"strnlen", Text
"memcmp", Text
"crypto_memcmp", Text
"assert"] -> Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof -> Maybe Proof
forall a. a -> Maybe a
Just Proof
forall a. Monoid a => a
mempty)
                | Text
fn Text -> [Text] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text
"memcpy", Text
"memmove"], Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0 -> Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof -> Maybe Proof
forall a. a -> Maybe a
Just Proof
forall a. Monoid a => a
mempty)
                | Just (Int
fmt, Int
_) <- Program -> Text -> Maybe (Int, Int)
formatOf Program
prog Text
fn, Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
fmt -> Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof -> Maybe Proof
forall a. a -> Maybe a
Just Proof
forall a. Monoid a => a
mempty)
                | Text
fn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"strerror_r", Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1, Expr -> Bool
gnu Expr
call -> Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Proof -> M (Maybe Proof)) -> Maybe Proof -> M (Maybe Proof)
forall a b. (a -> b) -> a -> b
$ Proof -> Maybe Proof
forall a. a -> Maybe a
Just
                    ([ FilePath -> Expr -> Doc AnsiStyle -> Step
Step FilePath
file Expr
call (Doc AnsiStyle
"with `_GNU_SOURCE`, this can return its own string without writing" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (Expr -> Doc AnsiStyle
forall a. Pretty a => Node (Lexeme a) -> Doc AnsiStyle
ppNode Expr
a)) ], [])
                | variants :: [Func]
variants@(Func
_ : [Func]
_) <- Program -> FilePath -> Text -> [Func]
definitionsOf Program
prog FilePath
file Text
fn -> [M (Maybe Proof)] -> M (Maybe Proof)
forall a. [M (Maybe a)] -> M (Maybe a)
firstJust
                    [ (Proof -> Proof) -> Maybe Proof -> Maybe Proof
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\([Step]
steps, [Cond]
conds) -> (FilePath -> Expr -> Doc AnsiStyle -> Step
Step FilePath
file Expr
a (Doc AnsiStyle
"passed to" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (Text -> Doc AnsiStyle
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
fn) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"here") Step -> [Step] -> [Step]
forall a. a -> [a] -> [a]
: [Step]
steps, [Cond]
conds))
                        (Maybe Proof -> Maybe Proof) -> M (Maybe Proof) -> M (Maybe Proof)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Program -> Func -> Int -> Maybe Text -> M (Maybe Proof)
unwrittenIn Program
prog Func
h Int
j (if Text -> Expr -> Bool
into Text
p Expr
a then Maybe Text
forall a. Maybe a
Nothing else Maybe Text
fld)
                    | Func
h <- [Func]
variants
                    ]
            Maybe Text
_ -> Maybe Proof -> M (Maybe Proof)
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Proof
forall a. Maybe a
Nothing

    -- GNU `strerror_r` returns a string; the other one returns an int.
    gnu :: Expr -> Bool
gnu Expr
call = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or
        [ Expr -> Expr
stripCasts Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
call Bool -> Bool -> Bool
&& Expr -> Bool
pointer Expr
ty
        | Fix (VarDeclStmt (Fix (VarDecl Expr
ty Lexeme Text
_ [Expr]
_)) (Just Expr
e)) <- Expr -> [Expr]
universe (Func -> Expr
funcBody Func
g)
        ]
    pointer :: Expr -> Bool
pointer Expr
ty = case Map Text CType -> Expr -> CType
cimpleType (Program -> Map Text CType
progTypedefs Program
prog) Expr
ty of
        TPtr Bool
_ CType
_ -> Bool
True
        CType
_        -> Bool
False

-- * Formats

-- | Where the format and the first value are, in calls of `fn`.
formatOf :: Program -> Text -> Maybe (Int, Int)
formatOf :: Program -> Text -> Maybe (Int, Int)
formatOf Program
prog Text
fn
    | Text
fn Text -> [Text] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text
"LOGGER_TRACE", Text
"LOGGER_DEBUG", Text
"LOGGER_INFO", Text
"LOGGER_WARNING", Text
"LOGGER_ERROR", Text
"LOGGER_FATAL"] = (Int, Int) -> Maybe (Int, Int)
forall a. a -> Maybe a
Just (Int
1, Int
2)
    | Text
fn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"LOGGER_ASSERT" = (Int, Int) -> Maybe (Int, Int)
forall a. a -> Maybe a
Just (Int
2, Int
3)
    | Text
fn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"printf" = (Int, Int) -> Maybe (Int, Int)
forall a. a -> Maybe a
Just (Int
0, Int
1)
    | Text
fn Text -> [Text] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text
"fprintf", Text
"sprintf"] = (Int, Int) -> Maybe (Int, Int)
forall a. a -> Maybe a
Just (Int
1, Int
2)
    | Text
fn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"snprintf" = (Int, Int) -> Maybe (Int, Int)
forall a. a -> Maybe a
Just (Int
2, Int
3)
    | Bool
otherwise = Text -> Map Text (Int, Int) -> Maybe (Int, Int)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
fn (Program -> Map Text (Int, Int)
progPrintf Program
prog)

-- | The values, by their place after the format, that `%s` conversions
-- without a precision read; `Nothing` for a format this doesn't follow.
unboundedStrings :: Text -> Maybe [Int]
unboundedStrings :: Text -> Maybe [Int]
unboundedStrings = Int -> FilePath -> Maybe [Int]
forall {a}. Num a => a -> FilePath -> Maybe [a]
go Int
0 (FilePath -> Maybe [Int])
-> (Text -> FilePath) -> Text -> Maybe [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
Text.unpack
  where
    go :: a -> FilePath -> Maybe [a]
go a
_ [] = [a] -> Maybe [a]
forall a. a -> Maybe a
Just []
    go a
i (Char
'%':Char
'%':FilePath
rest) = a -> FilePath -> Maybe [a]
go a
i FilePath
rest
    go a
i (Char
'%':FilePath
rest) =
        let afterFlags :: FilePath
afterFlags = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> FilePath -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (FilePath
"-+ #0'" :: String)) FilePath
rest
            (a
i', FilePath
afterWidth) = a -> FilePath -> (a, FilePath)
forall {a}. Num a => a -> FilePath -> (a, FilePath)
number a
i FilePath
afterFlags
            (Bool
precise, a
i'', FilePath
afterPrecision) = case FilePath
afterWidth of
                Char
'.':FilePath
r -> let (a
j, FilePath
r') = a -> FilePath -> (a, FilePath)
forall {a}. Num a => a -> FilePath -> (a, FilePath)
number a
i' FilePath
r in (Bool
True, a
j, FilePath
r')
                FilePath
r     -> (Bool
False, a
i', FilePath
r)
            afterLength :: FilePath
afterLength = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> FilePath -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (FilePath
"hlLqjzt" :: String)) FilePath
afterPrecision
        in case FilePath
afterLength of
            Char
c:FilePath
r | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
's' -> ([ a
i'' | Bool -> Bool
not Bool
precise ] [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++) ([a] -> [a]) -> Maybe [a] -> Maybe [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> FilePath -> Maybe [a]
go (a
i'' a -> a -> a
forall a. Num a => a -> a -> a
+ a
1) FilePath
r
                | Char
c Char -> FilePath -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (FilePath
"diouxXcpeEfFgGaAn" :: String) -> a -> FilePath -> Maybe [a]
go (a
i'' a -> a -> a
forall a. Num a => a -> a -> a
+ a
1) FilePath
r
            FilePath
_ -> Maybe [a]
forall a. Maybe a
Nothing
    go a
i (Char
_:FilePath
rest) = a -> FilePath -> Maybe [a]
go a
i FilePath
rest

    -- A width or precision: `*` takes a value.
    number :: a -> FilePath -> (a, FilePath)
number a
i = \case
        Char
'*':FilePath
r -> (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ a
1, FilePath
r)
        FilePath
r     -> (a
i, (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> FilePath -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Char
'0' .. Char
'9']) FilePath
r)

-- | The arguments of `%s` conversions without a precision, in `f`.
stringArgs :: Program -> Func -> [(Expr, Expr)]
stringArgs :: Program -> Func -> [(Expr, Expr)]
stringArgs Program
prog Func
f =
    [ (Expr
call, Expr
arg)
    | call :: Expr
call@(Fix (FunctionCall Expr
callee [Expr]
args)) <- Expr -> [Expr]
universe (Func -> Expr
funcBody Func
f)
    , Just Text
fn <- [Expr -> Maybe Text
callName Expr
callee]
    , Just (Int
fmtAt, Int
valuesAt) <- [Program -> Text -> Maybe (Int, Int)
formatOf Program
prog Text
fn]
    , Fix (LiteralExpr LiteralType
String Lexeme Text
fmt) <- Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
1 (Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
drop Int
fmtAt [Expr]
args)
    , Just [Int]
strings <- [Text -> Maybe [Int]
unboundedStrings (Int -> Text -> Text
Text.drop Int
1 (Int -> Text -> Text
Text.dropEnd Int
1 (Lexeme Text -> Text
name Lexeme Text
fmt)))]
    , Int
i <- [Int]
strings
    , Expr
arg <- Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
1 (Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
drop (Int
valuesAt Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i) [Expr]
args)
    ]

-- * The linter

analyse :: [TranslationUnit] -> [Diagnostic CimplePos]
analyse :: [TranslationUnit] -> [Diagnostic CimplePos]
analyse [TranslationUnit]
tus = (State Memo [Diagnostic CimplePos]
 -> Memo -> [Diagnostic CimplePos])
-> Memo
-> State Memo [Diagnostic CimplePos]
-> [Diagnostic CimplePos]
forall a b c. (a -> b -> c) -> b -> a -> c
flip State Memo [Diagnostic CimplePos] -> Memo -> [Diagnostic CimplePos]
forall s a. State s a -> s -> a
evalState (Map UnwrittenKey (Maybe Proof)
-> Set UnwrittenKey -> Map Key (Maybe [Step]) -> Set Key -> Memo
Memo Map UnwrittenKey (Maybe Proof)
forall k a. Map k a
Map.empty Set UnwrittenKey
forall a. Set a
Set.empty Map Key (Maybe [Step])
forall k a. Map k a
Map.empty Set Key
forall a. Set a
Set.empty) (State Memo [Diagnostic CimplePos] -> [Diagnostic CimplePos])
-> State Memo [Diagnostic CimplePos] -> [Diagnostic CimplePos]
forall a b. (a -> b) -> a -> b
$ [[Diagnostic CimplePos]] -> [Diagnostic CimplePos]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Diagnostic CimplePos]] -> [Diagnostic CimplePos])
-> StateT Memo Identity [[Diagnostic CimplePos]]
-> State Memo [Diagnostic CimplePos]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [State Memo [Diagnostic CimplePos]]
-> StateT Memo Identity [[Diagnostic CimplePos]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
    [ Program -> Int -> Func -> Expr -> M (Maybe [Step])
unterminated Program
prog Int
maxDepth Func
f Expr
arg M (Maybe [Step])
-> (Maybe [Step] -> State Memo [Diagnostic CimplePos])
-> State Memo [Diagnostic CimplePos]
forall a b.
StateT Memo Identity a
-> (a -> StateT Memo Identity b) -> StateT Memo Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just [Step]
steps -> [Diagnostic CimplePos] -> State Memo [Diagnostic CimplePos]
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Func -> Expr -> [Step] -> Diagnostic CimplePos
diagnostic Func
f Expr
arg [Step]
steps]
        Maybe [Step]
Nothing -> Program -> Func -> Expr -> M (Maybe Proof)
unwritten Program
prog Func
f Expr
arg M (Maybe Proof)
-> (Maybe Proof -> State Memo [Diagnostic CimplePos])
-> State Memo [Diagnostic CimplePos]
forall a b.
StateT Memo Identity a
-> (a -> StateT Memo Identity b) -> StateT Memo Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Just ([Step]
steps, [Cond]
conds) | Program -> [Cond] -> Bool
satisfiable Program
prog [Cond]
conds -> [Diagnostic CimplePos] -> State Memo [Diagnostic CimplePos]
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Func -> Expr -> [Step] -> [Cond] -> Diagnostic CimplePos
unwrittenDiagnostic Func
f Expr
arg [Step]
steps [Cond]
conds]
            Maybe Proof
_ -> [Diagnostic CimplePos] -> State Memo [Diagnostic CimplePos]
forall a. a -> StateT Memo Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    | Func
f <- (Func -> FilePath) -> [Func] -> [Func]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn Func -> FilePath
funcFile (Program -> [Func]
progFuncs Program
prog)
    , (Expr
_, Expr
arg) <- Program -> Func -> [(Expr, Expr)]
stringArgs Program
prog Func
f
    ]
  where
    prog :: Program
prog = [TranslationUnit] -> Program
buildProgram [TranslationUnit]
tus

diagnostic :: Func -> Expr -> [Step] -> Diagnostic CimplePos
diagnostic :: Func -> Expr -> [Step] -> Diagnostic CimplePos
diagnostic Func
f Expr
arg [Step]
steps =
    CimplePos
-> Int
-> DiagnosticLevel
-> Doc AnsiStyle
-> Maybe Text
-> [DiagnosticSpan CimplePos]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Diagnostic CimplePos
forall pos.
pos
-> Int
-> DiagnosticLevel
-> Doc AnsiStyle
-> Maybe Text
-> [DiagnosticSpan pos]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Diagnostic pos
Diagnostic CimplePos
pos Int
len DiagnosticLevel
WarningLevel
        (Doc AnsiStyle
"`%s` reads" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (Expr -> Doc AnsiStyle
forall a. Pretty a => Node (Lexeme a) -> Doc AnsiStyle
ppNode Expr
arg) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"up to a NUL byte, and there can be none before the end of the object it points into")
        (Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"nul-terminated")
        (CimplePos -> Int -> [Doc AnsiStyle] -> DiagnosticSpan CimplePos
forall pos. pos -> Int -> [Doc AnsiStyle] -> DiagnosticSpan pos
DiagnosticSpan CimplePos
pos Int
len [Doc AnsiStyle
"read up to a NUL here"]
            DiagnosticSpan CimplePos
-> [DiagnosticSpan CimplePos] -> [DiagnosticSpan CimplePos]
forall a. a -> [a] -> [a]
: [ CimplePos -> Int -> [Doc AnsiStyle] -> DiagnosticSpan CimplePos
forall pos. pos -> Int -> [Doc AnsiStyle] -> DiagnosticSpan pos
DiagnosticSpan CimplePos
p Int
l [Doc AnsiStyle
note] | Step FilePath
file Expr
n Doc AnsiStyle
note <- [Step]
steps, let (CimplePos
p, Int
l) = FilePath -> Expr -> (CimplePos, Int)
nodePosAndLen FilePath
file Expr
n ])
        [ (DiagnosticLevel
NoteLevel, Doc AnsiStyle
"its bytes are a copy that can fill the object to its end, and nothing writes a NUL into it")
        , (DiagnosticLevel
HelpLevel, Doc AnsiStyle
"print it with `%.*s` and its length, or don't print its bytes")
        ]
  where
    (CimplePos
pos, Int
len) = FilePath -> Expr -> (CimplePos, Int)
nodePosAndLen (Func -> FilePath
funcFile Func
f) Expr
arg

unwrittenDiagnostic :: Func -> Expr -> [Step] -> [Cond] -> Diagnostic CimplePos
unwrittenDiagnostic :: Func -> Expr -> [Step] -> [Cond] -> Diagnostic CimplePos
unwrittenDiagnostic Func
f Expr
arg [Step]
steps [Cond]
conds =
    CimplePos
-> Int
-> DiagnosticLevel
-> Doc AnsiStyle
-> Maybe Text
-> [DiagnosticSpan CimplePos]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Diagnostic CimplePos
forall pos.
pos
-> Int
-> DiagnosticLevel
-> Doc AnsiStyle
-> Maybe Text
-> [DiagnosticSpan pos]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> Diagnostic pos
Diagnostic CimplePos
pos Int
len DiagnosticLevel
WarningLevel
        (Doc AnsiStyle
"`%s` reads" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (Expr -> Doc AnsiStyle
forall a. Pretty a => Node (Lexeme a) -> Doc AnsiStyle
ppNode Expr
arg) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"up to a NUL byte, and those bytes can be ones nothing wrote")
        (Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"nul-terminated")
        (CimplePos -> Int -> [Doc AnsiStyle] -> DiagnosticSpan CimplePos
forall pos. pos -> Int -> [Doc AnsiStyle] -> DiagnosticSpan pos
DiagnosticSpan CimplePos
pos Int
len [Doc AnsiStyle
"read up to a NUL here"]
            DiagnosticSpan CimplePos
-> [DiagnosticSpan CimplePos] -> [DiagnosticSpan CimplePos]
forall a. a -> [a] -> [a]
: [ CimplePos -> Int -> [Doc AnsiStyle] -> DiagnosticSpan CimplePos
forall pos. pos -> Int -> [Doc AnsiStyle] -> DiagnosticSpan pos
DiagnosticSpan CimplePos
p Int
l [Doc AnsiStyle
note] | Step FilePath
file Expr
n Doc AnsiStyle
note <- [Step]
steps, let (CimplePos
p, Int
l) = FilePath -> Expr -> (CimplePos, Int)
nodePosAndLen FilePath
file Expr
n ])
        ([ (DiagnosticLevel
NoteLevel, Doc AnsiStyle
"they're whatever was in that memory, which may have no NUL before its end") ]
         [(DiagnosticLevel, Doc AnsiStyle)]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> [(DiagnosticLevel, Doc AnsiStyle)]
forall a. [a] -> [a] -> [a]
++ [ (DiagnosticLevel
NoteLevel, Doc AnsiStyle
"this is where" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> (Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle)
-> [Doc AnsiStyle] -> Doc AnsiStyle
forall (t :: * -> *) ann.
Foldable t =>
(Doc ann -> Doc ann -> Doc ann) -> t (Doc ann) -> Doc ann
concatWith (\Doc AnsiStyle
a Doc AnsiStyle
b -> Doc AnsiStyle
a Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"and" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
b) ((Cond -> Doc AnsiStyle) -> [Cond] -> [Doc AnsiStyle]
forall a b. (a -> b) -> [a] -> [b]
map Cond -> Doc AnsiStyle
cond ([Cond] -> [Cond]
dedupe [Cond]
conds))) | Bool -> Bool
not ([Cond] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Cond]
conds) ]
         [(DiagnosticLevel, Doc AnsiStyle)]
-> [(DiagnosticLevel, Doc AnsiStyle)]
-> [(DiagnosticLevel, Doc AnsiStyle)]
forall a. [a] -> [a] -> [a]
++ [ (DiagnosticLevel
HelpLevel, Doc AnsiStyle
"write the bytes on every path, or return the string that was written") ])
  where
    (CimplePos
pos, Int
len) = FilePath -> Expr -> (CimplePos, Int)
nodePosAndLen (Func -> FilePath
funcFile Func
f) Expr
arg
    cond :: Cond -> Doc AnsiStyle
cond (Cond FilePath
_ Bool
True Expr
c)  = Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (Expr -> Doc AnsiStyle
forall a. Pretty a => Node (Lexeme a) -> Doc AnsiStyle
ppNode Expr
c) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"holds"
    cond (Cond FilePath
_ Bool
False Expr
c) = Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
backticks (Expr -> Doc AnsiStyle
forall a. Pretty a => Node (Lexeme a) -> Doc AnsiStyle
ppNode Expr
c) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"doesn't"
    dedupe :: [Cond] -> [Cond]
dedupe = (Cond -> [Cond] -> [Cond]) -> [Cond] -> [Cond] -> [Cond]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\c :: Cond
c@(Cond FilePath
_ Bool
a Expr
x) [Cond]
acc -> if (Cond -> Bool) -> [Cond] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(Cond FilePath
_ Bool
b Expr
y) -> Bool
a Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b Bool -> Bool -> Bool
&& Expr -> Expr -> Bool
semEq Expr
x Expr
y) [Cond]
acc then [Cond]
acc else Cond
c Cond -> [Cond] -> [Cond]
forall a. a -> [a] -> [a]
: [Cond]
acc) []

descr :: ([TranslationUnit] -> [Diagnostic CimplePos], (Text, Text))
descr :: ([TranslationUnit] -> [Diagnostic CimplePos], (Text, Text))
descr = ([TranslationUnit] -> [Diagnostic CimplePos]
analyse, (Text
"nul-terminated", [Text] -> Text
Text.unlines
    [ Text
"Checks that `%s` conversions get NUL-terminated strings."
    , Text
""
    , Text
"It warns where it can show that the argument's bytes can have no NUL before"
    , Text
"the end of the object they're in: they're a copy of a runtime number of"
    , Text
"bytes, that copy can fill the object to its end, and nothing writes a NUL"
    , Text
"into it. Where the argument is a parameter, a caller shows it."
    , Text
""
    , Text
"It also warns where the argument is a call returning a buffer it was given,"
    , Text
"the caller gives it one nothing has written, and the function has a path"
    , Text
"that doesn't write it, decided only by things like `errno` (e.g. GNU"
    , Text
"`strerror_r`, which can return its own string). It says which `#if`s have"
    , Text
"to hold for that, and says nothing where they can't hold together."
    , Text
""
    , Text
"**Reason:** `%s` reads until it finds a NUL byte, past the end of the object"
    , Text
"if there's none in it. Byte arrays with a length, such as names and"
    , Text
"messages from the network, have no NUL of their own, and memory nothing"
    , Text
"wrote holds whatever was there before."
    ]))