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

import           Control.Monad                 (forM_, when)
import           Data.Text                     (Text)
import qualified Data.Text                     as Text
import           Language.C.Analysis.SemRep    (FunDef, GlobalDecls)
import           Language.C.Analysis.TravMonad (Trav)
import           Language.C.Data.Node          (NodeInfo)
import           Language.C.Syntax.AST         (CAssignOp (..), CBinaryOp (..),
                                                annotation)
import           Prettyprinter                 (pretty, (<+>))
import           Tokstyle.C.Analysis.Interval  (Facts, IntTy (..), Origin (..),
                                                Range (..), Term (..),
                                                TermKind (..), canWrap, eval,
                                                subTermsWith)
import           Tokstyle.C.Env                (Env, recordLinterError)
import           Tokstyle.C.IntervalLinter     (analysedFunctions, exprDoc,
                                                recordWrap, valuesDoc)
import           Tokstyle.C.TravUtils          (backticks)


isComparison :: CBinaryOp -> Bool
isComparison :: CBinaryOp -> Bool
isComparison = (CBinaryOp -> [CBinaryOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CBinaryOp
CEqOp, CBinaryOp
CNeqOp, CBinaryOp
CLeOp, CBinaryOp
CGrOp, CBinaryOp
CLeqOp, CBinaryOp
CGeqOp])

isRelational :: CBinaryOp -> Bool
isRelational :: CBinaryOp -> Bool
isRelational = (CBinaryOp -> [CBinaryOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CBinaryOp
CLeOp, CBinaryOp
CGrOp, CBinaryOp
CLeqOp, CBinaryOp
CGeqOp])

compareWith :: CBinaryOp -> Integer -> Integer -> Bool
compareWith :: CBinaryOp -> Integer -> Integer -> Bool
compareWith = \case
    CBinaryOp
CEqOp  -> Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
(==)
    CBinaryOp
CNeqOp -> Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
(/=)
    CBinaryOp
CLeOp  -> Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
(<)
    CBinaryOp
CGrOp  -> Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
(>)
    CBinaryOp
CLeqOp -> Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
(<=)
    CBinaryOp
_      -> Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
(>=)

flipOp :: CBinaryOp -> CBinaryOp
flipOp :: CBinaryOp -> CBinaryOp
flipOp = \case
    CBinaryOp
CLeOp  -> CBinaryOp
CGrOp
    CBinaryOp
CGrOp  -> CBinaryOp
CLeOp
    CBinaryOp
CLeqOp -> CBinaryOp
CGeqOp
    CBinaryOp
CGeqOp -> CBinaryOp
CLeqOp
    CBinaryOp
op     -> CBinaryOp
op

-- | The values that wrapped around, with the expression where they did.
wrappedIn :: Facts -> Term -> [(Range, NodeInfo)]
wrappedIn :: Facts -> Term -> [(Range, NodeInfo)]
wrappedIn Facts
facts Term
t = [ (Range
r, NodeInfo
site) | Just [Range]
rs <- [Facts -> Term -> Maybe [Range]
eval Facts
facts Term
t], r :: Range
r@(Range Integer
_ Integer
_ (Wrapped NodeInfo
site)) <- [Range]
rs ]

-- | Warns if wrapping around makes one side of a comparison take values an
-- index reduced on the other side never has.
checkComparison :: Facts -> CBinaryOp -> Term -> Term -> Trav Env ()
checkComparison :: Facts -> CBinaryOp -> Term -> Term -> Trav Env ()
checkComparison Facts
facts CBinaryOp
op Term
wrapping Term
other = case Facts -> Term -> Maybe [Range]
eval Facts
facts Term
other of
    Just os :: [Range]
os@(Range
_ : [Range]
_) | (Range -> Bool) -> [Range] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
== Origin
Reduced) (Origin -> Bool) -> (Range -> Origin) -> Range -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Origin
origin) [Range]
os -> do
        let oLo :: Integer
oLo = [Integer] -> Integer
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ((Range -> Integer) -> [Range] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map Range -> Integer
lo [Range]
os)
            oHi :: Integer
oHi = [Integer] -> Integer
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ((Range -> Integer) -> [Range] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map Range -> Integer
hi [Range]
os)
        case [ (Range
w, NodeInfo
site) | (Range
w, NodeInfo
site) <- Facts -> Term -> [(Range, NodeInfo)]
wrappedIn Facts
facts Term
wrapping, Range -> Integer
hi Range
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
oLo Bool -> Bool -> Bool
|| Range -> Integer
lo Range
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
oHi ] of
            (Range
w, NodeInfo
site) : [(Range, NodeInfo)]
_ -> Term -> NodeInfo -> Doc AnsiStyle -> Trav Env ()
recordWrap Term
wrapping NodeInfo
site (Doc AnsiStyle -> Trav Env ()) -> Doc AnsiStyle -> Trav Env ()
forall a b. (a -> b) -> a -> b
$
                CExpr -> Doc AnsiStyle
forall a. CExpr -> Doc a
exprDoc (Term -> CExpr
termExpr Term
wrapping) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"can wrap around to" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Range -> Doc AnsiStyle
forall a. Range -> Doc a
valuesDoc Range
w
                Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
", but" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> CExpr -> Doc AnsiStyle
forall a. CExpr -> Doc a
exprDoc (Term -> CExpr
termExpr Term
other) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"is always between"
                Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc AnsiStyle
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
oLo 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
<+> Integer -> Doc AnsiStyle
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
oHi
                Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
", so the comparison is always"
                Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> (if CBinaryOp -> Integer -> Integer -> Bool
compareWith CBinaryOp
op (Range -> Integer
lo Range
w) Integer
oLo then Doc AnsiStyle
"true" else Doc AnsiStyle
"false")
                Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"when it wraps"
            [] -> () -> Trav Env ()
forall a. a -> TravT Env Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Maybe [Range]
_ -> () -> Trav Env ()
forall a. a -> TravT Env Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Warns if a value that wrapped around is reduced modulo a size that
-- doesn't divide the range it wrapped around.
checkRemainder :: Facts -> Term -> Term -> Trav Env ()
checkRemainder :: Facts -> Term -> Term -> Trav Env ()
checkRemainder Facts
facts Term
a Term
b = case (Facts -> Term -> Maybe [Range]
eval Facts
facts Term
b, Term -> Maybe IntTy
termTy Term
a, Facts -> Term -> [(Range, NodeInfo)]
wrappedIn Facts
facts Term
a) of
    (Just [Range Integer
n Integer
n' Origin
_], Just IntTy
ty, (Range
w, NodeInfo
site) : [(Range, NodeInfo)]
_) | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n', Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0, (Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ IntTy -> Integer
tyBits IntTy
ty) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 ->
        Term -> NodeInfo -> Doc AnsiStyle -> Trav Env ()
recordWrap Term
a NodeInfo
site (Doc AnsiStyle -> Trav Env ()) -> Doc AnsiStyle -> Trav Env ()
forall a b. (a -> b) -> a -> b
$
            CExpr -> Doc AnsiStyle
forall a. CExpr -> Doc a
exprDoc (Term -> CExpr
termExpr Term
a) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"can wrap around to" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Range -> Doc AnsiStyle
forall a. Range -> Doc a
valuesDoc Range
w
            Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
", and" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc AnsiStyle
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ IntTy -> Integer
tyBits IntTy
ty :: Integer) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"is not a multiple of"
            Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc AnsiStyle
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
n Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
", so" 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 (Doc AnsiStyle
"%" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc AnsiStyle
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
n)
            Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"then gives a different index than it would without the wrap"
    (Maybe [Range], Maybe IntTy, [(Range, NodeInfo)])
_ -> () -> Trav Env ()
forall a. a -> TravT Env Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Warns if an index that wrapped around can be past the end of an array.
checkIndex :: Facts -> Term -> Term -> Integer -> Trav Env ()
checkIndex :: Facts -> Term -> Term -> Integer -> Trav Env ()
checkIndex Facts
facts Term
arr Term
i Integer
len =
    case [ (Range
w, NodeInfo
site) | (Range
w, NodeInfo
site) <- Facts -> Term -> [(Range, NodeInfo)]
wrappedIn Facts
facts Term
i, Range -> Integer
hi Range
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
len ] of
        (Range
w, NodeInfo
site) : [(Range, NodeInfo)]
_ -> Term -> NodeInfo -> Doc AnsiStyle -> Trav Env ()
recordWrap Term
i NodeInfo
site (Doc AnsiStyle -> Trav Env ()) -> Doc AnsiStyle -> Trav Env ()
forall a b. (a -> b) -> a -> b
$
            CExpr -> Doc AnsiStyle
forall a. CExpr -> Doc a
exprDoc (Term -> CExpr
termExpr Term
i) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"can wrap around to" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Range -> Doc AnsiStyle
forall a. Range -> Doc a
valuesDoc Range
w
            Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
", past the end of" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> CExpr -> Doc AnsiStyle
forall a. CExpr -> Doc a
exprDoc (Term -> CExpr
termExpr Term
arr)
            Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
", which has" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc AnsiStyle
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
len Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"elements"
        [] -> () -> Trav Env ()
forall a. a -> TravT Env Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Warns if the difference of two narrow unsigned values, computed in @int@
-- after integer promotion, wraps around at the size of the wider unsigned type
-- it is converted to.
checkPromoted :: Facts -> Term -> Term -> Trav Env ()
checkPromoted :: Facts -> Term -> Term -> Trav Env ()
checkPromoted Facts
facts Term
converted Term
inner = case (Term -> Maybe IntTy
termTy Term
converted, Term -> TermKind
termKind Term
inner, Term -> Maybe IntTy
termTy Term
inner) of
    (Just IntTy{tySigned :: IntTy -> Bool
tySigned = Bool
False, tyBits :: IntTy -> Integer
tyBits = Integer
bits}, TBin CBinaryOp
CSubOp Term
x Term
y, Just IntTy{tySigned :: IntTy -> Bool
tySigned = Bool
True})
        | Just Integer
w <- [Term] -> Maybe Integer
narrowest [Term
x, Term
y], Integer
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
bits
        , (Range
r, NodeInfo
_) : [(Range, NodeInfo)]
_ <- Facts -> Term -> [(Range, NodeInfo)]
wrappedIn Facts
facts Term
converted ->
            NodeInfo -> Doc AnsiStyle -> Trav Env ()
recordLinterError (CExpr -> NodeInfo
forall a. CExpression a -> a
forall (ast :: * -> *) a. Annotated ast => ast a -> a
annotation (Term -> CExpr
termExpr Term
inner)) (Doc AnsiStyle -> Trav Env ()) -> Doc AnsiStyle -> Trav Env ()
forall a b. (a -> b) -> a -> b
$
                CExpr -> Doc AnsiStyle
forall a. CExpr -> Doc a
exprDoc (Term -> CExpr
termExpr Term
inner) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"can wrap around to" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Range -> Doc AnsiStyle
forall a. Range -> Doc a
valuesDoc Range
r
                Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
", because it is the difference of" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc AnsiStyle
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
w Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
"-bit values but wraps around at"
                Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc AnsiStyle
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
bits Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"bits here"
    (Maybe IntTy, TermKind, Maybe IntTy)
_ -> () -> Trav Env ()
forall a. a -> TravT Env Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | The width of the widest of some narrow unsigned values, if none of them is
-- a constant.
narrowest :: [Term] -> Maybe Integer
narrowest :: [Term] -> Maybe Integer
narrowest [Term]
ts = [Integer] -> Integer
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Integer] -> Integer) -> Maybe [Integer] -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Maybe Integer) -> [Term] -> Maybe [Integer]
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 Term -> Maybe Integer
width [Term]
ts
  where
    width :: Term -> Maybe Integer
width Term
t = case (Term -> TermKind
termKind Term
t, Term -> Maybe IntTy
termTy Term
t) of
        (TConst Integer
_, Maybe IntTy
_)                                 -> Maybe Integer
forall a. Maybe a
Nothing
        (TermKind
_, Just IntTy{tySigned :: IntTy -> Bool
tySigned = Bool
False, tyBits :: IntTy -> Integer
tyBits = Integer
b}) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
b
        (TermKind, Maybe IntTy)
_                                             -> Maybe Integer
forall a. Maybe a
Nothing

-- | The width of the narrow unsigned values a term is the difference of, if
-- integer promotion computes it in @int@ and it can be negative there.
negativeDifference :: Facts -> Term -> Maybe Integer
negativeDifference :: Facts -> Term -> Maybe Integer
negativeDifference Facts
facts Term
d = case (Term -> TermKind
termKind Term
d, Term -> Maybe IntTy
termTy Term
d) of
    (TBin CBinaryOp
CSubOp Term
x Term
y, Just IntTy{tySigned :: IntTy -> Bool
tySigned = Bool
True, tyBits :: IntTy -> Integer
tyBits = Integer
bits})
        | Just Integer
w <- [Term] -> Maybe Integer
narrowest [Term
x, Term
y], Integer
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
bits
        , Just [Range]
rs <- Facts -> Term -> Maybe [Range]
eval Facts
facts Term
d, (Range -> Bool) -> [Range] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0) (Integer -> Bool) -> (Range -> Integer) -> Range -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Integer
lo) [Range]
rs -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
w
    (TermKind, Maybe IntTy)
_ -> Maybe Integer
forall a. Maybe a
Nothing

-- | Warns if a difference of narrow unsigned values that is negative where it
-- would wrap around at their width is compared with another value that isn't
-- known.
checkSignedComparison :: Facts -> Term -> Term -> Trav Env ()
checkSignedComparison :: Facts -> Term -> Term -> Trav Env ()
checkSignedComparison Facts
facts Term
l Term
r =
    case [ (Term
d, Term
other, Integer
w) | (Term
d, Term
other) <- [(Term
l, Term
r), (Term
r, Term
l)], Just Integer
w <- [Facts -> Term -> Maybe Integer
negativeDifference Facts
facts Term
d] ] of
        (Term
d, Term
other, Integer
w) : [(Term, Term, Integer)]
_ | Bool -> Bool
not (Term -> Bool
known Term
other) ->
            NodeInfo -> Doc AnsiStyle -> Trav Env ()
recordLinterError (CExpr -> NodeInfo
forall a. CExpression a -> a
forall (ast :: * -> *) a. Annotated ast => ast a -> a
annotation (Term -> CExpr
termExpr Term
d)) (Doc AnsiStyle -> Trav Env ()) -> Doc AnsiStyle -> Trav Env ()
forall a b. (a -> b) -> a -> b
$
                CExpr -> Doc AnsiStyle
forall a. CExpr -> Doc a
exprDoc (Term -> CExpr
termExpr Term
d) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"is the difference of" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc AnsiStyle
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
w
                Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
"-bit values, computed in `int` where it can be negative instead of wrapping around at"
                Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc AnsiStyle
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
w Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"bits, so comparing it with" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> CExpr -> Doc AnsiStyle
forall a. CExpr -> Doc a
exprDoc (Term -> CExpr
termExpr Term
other)
                Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc AnsiStyle
"gives a different result than comparing the" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc AnsiStyle
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
w Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
"-bit differences"
        [(Term, Term, Integer)]
_ -> () -> Trav Env ()
forall a. a -> TravT Env Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where
    known :: Term -> Bool
known Term
t = case Facts -> Term -> Maybe [Range]
eval Facts
facts Term
t of
        Just [Range Integer
n Integer
n' Origin
_] -> Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n'
        Maybe [Range]
_                   -> Bool
False

checkTerm :: Facts -> Term -> Trav Env ()
checkTerm :: Facts -> Term -> Trav Env ()
checkTerm Facts
facts Term
t = case Term -> TermKind
termKind Term
t of
    TBin CBinaryOp
op Term
l Term
r | CBinaryOp -> Bool
isComparison CBinaryOp
op -> do
        Facts -> CBinaryOp -> Term -> Term -> Trav Env ()
checkComparison Facts
facts CBinaryOp
op Term
l Term
r
        Facts -> CBinaryOp -> Term -> Term -> Trav Env ()
checkComparison Facts
facts (CBinaryOp -> CBinaryOp
flipOp CBinaryOp
op) Term
r Term
l
        Bool -> Trav Env () -> Trav Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (CBinaryOp -> Bool
isRelational CBinaryOp
op) (Trav Env () -> Trav Env ()) -> Trav Env () -> Trav Env ()
forall a b. (a -> b) -> a -> b
$ Facts -> Term -> Term -> Trav Env ()
checkSignedComparison Facts
facts Term
l Term
r
    TBin CBinaryOp
CRmdOp Term
a Term
b -> Facts -> Term -> Term -> Trav Env ()
checkRemainder Facts
facts Term
a Term
b
    TIndex Term
arr Term
i (Just Integer
len) -> Facts -> Term -> Term -> Integer -> Trav Env ()
checkIndex Facts
facts Term
arr Term
i Integer
len
    TCast Term
a -> Facts -> Term -> Term -> Trav Env ()
checkPromoted Facts
facts Term
t Term
a
    TAssign Maybe AccessPath
_ CAssignOp
CAssignOp Term
_ Term
r -> Facts -> Term -> Term -> Trav Env ()
checkPromoted Facts
facts Term
t Term
r
    TermKind
_ -> () -> Trav Env ()
forall a. a -> TravT Env Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | The functions the check looks at: those that can wrap around.
looksAt :: FunDef -> Bool
looksAt :: FunDef -> Bool
looksAt = FunDef -> Bool
canWrap

analyse :: GlobalDecls -> Trav Env ()
analyse :: GlobalDecls -> Trav Env ()
analyse GlobalDecls
_ = do
    [(FunDef, [(Node, Facts, [Term])])]
functions <- (FunDef -> Bool) -> Trav Env [(FunDef, [(Node, Facts, [Term])])]
analysedFunctions FunDef -> Bool
looksAt
    [(FunDef, [(Node, Facts, [Term])])]
-> ((FunDef, [(Node, Facts, [Term])]) -> Trav Env ())
-> Trav Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(FunDef, [(Node, Facts, [Term])])]
functions (((FunDef, [(Node, Facts, [Term])]) -> Trav Env ()) -> Trav Env ())
-> ((FunDef, [(Node, Facts, [Term])]) -> Trav Env ())
-> Trav Env ()
forall a b. (a -> b) -> a -> b
$ \(FunDef
_, [(Node, Facts, [Term])]
nodes) ->
        [(Node, Facts, [Term])]
-> ((Node, Facts, [Term]) -> Trav Env ()) -> Trav Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Node, Facts, [Term])]
nodes (((Node, Facts, [Term]) -> Trav Env ()) -> Trav Env ())
-> ((Node, Facts, [Term]) -> Trav Env ()) -> Trav Env ()
forall a b. (a -> b) -> a -> b
$ \(Node
_, Facts
facts, [Term]
terms) -> ((Facts, Term) -> Trav Env ()) -> [(Facts, Term)] -> Trav Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Facts -> Term -> Trav Env ()) -> (Facts, Term) -> Trav Env ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Facts -> Term -> Trav Env ()
checkTerm) ((Term -> [(Facts, Term)]) -> [Term] -> [(Facts, Term)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Facts -> Term -> [(Facts, Term)]
subTermsWith Facts
facts) [Term]
terms)


descr :: (GlobalDecls -> Trav Env (), (Text, Text))
descr :: (GlobalDecls -> Trav Env (), (Text, Text))
descr = (GlobalDecls -> Trav Env ()
analyse, (Text
"wraparound", [Text] -> Text
Text.unlines
    [ Text
"Checks for integer arithmetic that wraps around where it is used as an index:"
    , Text
"compared to an index reduced with `%` or `&`, reduced with `%` by a size that"
    , Text
"doesn't divide the type's range, or used to index an array it can be past the"
    , Text
"end of. Also checks for the difference of two 16-bit values that wraps around"
    , Text
"at 32 bits because integer promotion computes it in `int`, and for such a"
    , Text
"difference compared in `int`, where it is negative instead of wrapping around."
    , Text
""
    , Text
"The checks follow values through locals and fields, take the conditions that"
    , Text
"guard them into account, and know which values the program stores in struct"
    , Text
"fields, returns from functions, and passes to static functions."
    , Text
""
    , Text
"**Reason:** in a ring buffer of size `N`, `(uint16_t)(start - 1)` wraps to"
    , Text
"65535 when `start` is 0, not to `N - 1`. Comparing it to `id % N` then never"
    , Text
"matches. Use `(start + N - 1) % N` instead."
    ]))