diff --git a/doc/c.md b/doc/c.md index 1763665..9d4e747 100644 --- a/doc/c.md +++ b/doc/c.md @@ -1,6 +1,6 @@ # C-based linters (`check-c`) -There are currently 14 linters implemented. +There are currently 15 linters implemented. ## `-Wbool-conversion` @@ -78,3 +78,19 @@ role-based types. ## `-Wvoid-call` Checks that the first statement of a function with a `void*` parameter casts it to a specific type. + +## `-Wwraparound` + +Checks for integer arithmetic that wraps around where it is used as an index: +compared to an index reduced with `%` or `&`, reduced with `%` by a size that +doesn't divide the type's range, or used to index an array it can be past the +end of. Also checks for the difference of two 16-bit values that wraps around +at 32 bits because integer promotion computes it in `int`. + +The checks follow values through locals and fields, take the conditions that +guard them into account, and know which values the program stores in struct +fields, returns from functions, and passes to static functions. + +**Reason:** in a ring buffer of size `N`, `(uint16_t)(start - 1)` wraps to +65535 when `start` is 0, not to `N - 1`. Comparing it to `id % N` then never +matches. Use `(start + N - 1) % N` instead. diff --git a/include/.gitignore b/include/.gitignore new file mode 100644 index 0000000..12dc135 --- /dev/null +++ b/include/.gitignore @@ -0,0 +1,2 @@ +/sodium +/sodium.h diff --git a/src/Tokstyle/C/Analysis/CFG.hs b/src/Tokstyle/C/Analysis/CFG.hs index bfec021..684daab 100644 --- a/src/Tokstyle/C/Analysis/CFG.hs +++ b/src/Tokstyle/C/Analysis/CFG.hs @@ -8,12 +8,15 @@ module Tokstyle.C.Analysis.CFG , fromFunDef ) where +import Control.Monad (unless) import Control.Monad.Reader import Control.Monad.State import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Language.C.Analysis.SemRep (FunDef (..)) import Language.C.Data.Ident (Ident) +import Language.C.Data.Name (Name) +import Language.C.Data.Node (NodeInfo, nameOfNode) import Language.C.Syntax.AST -- | A node in the Control Flow Graph. @@ -59,6 +62,7 @@ data BuildEnv = BuildEnv , envContinue :: Maybe Node , envReturn :: Node , envLabels :: Map Ident Node + , envCases :: Map Name Node } data BuildState = BuildState @@ -83,7 +87,7 @@ fromFunDef (FunDef _ (CCompound _ items _) _) = let (exitNode, s0) = runState (newNodeState ExitNode) (BuildState 0 Map.empty) (entryNode, s1) = runState (newNodeState EntryNode) s0 (labels, s2) = runState (execStateT (mapM_ collectBlockItem items) Map.empty) s1 - env = BuildEnv Nothing Nothing exitNode labels + env = BuildEnv Nothing Nothing exitNode labels Map.empty (actualEntry, s3) = runState (runReaderT (buildBlock items exitNode) env) s2 (_, s4) = runState (addEdgeM entryNode Unconditional actualEntry) s3 in (entryNode, stateEdges s4) @@ -99,6 +103,9 @@ fromFunDef (FunDef _ (CCompound _ items _) _) = CCompound _ bis _ -> mapM_ collectBlockItem bis CIf _ t e _ -> collectStat t >> maybe (return ()) collectStat e CSwitch _ s _ -> collectStat s + CCase _ s _ -> collectStat s + CCases _ _ s _ -> collectStat s + CDefault s _ -> collectStat s CWhile _ s _ _ -> collectStat s CFor _ _ _ s _ -> collectStat s _ -> return () @@ -150,14 +157,29 @@ buildStat stat next = case stat of lift $ addEdgeM node FalseBranch eEntry return node - CWhile cond s _ _ -> do + CWhile cond s isDo _ -> do node <- newNode (BranchNode cond) sEntry <- local (\env -> env { envBreak = Just next, envContinue = Just node }) $ buildStat s node lift $ addEdgeM node TrueBranch sEntry lift $ addEdgeM node FalseBranch next + return $ if isDo then sEntry else node + + CSwitch cond s _ -> do + node <- newNode (BranchNode cond) + labels <- caseLabels s + let cases = Map.fromList [ (n, c) | (Just n, _, c, _) <- labels ] + _ <- local (\env -> env { envBreak = Just next, envCases = cases }) $ + buildStat s next + mapM_ (\(_, edge, c, _) -> lift $ addEdgeM node edge c) labels + unless (or [ isDefault | (_, _, _, isDefault) <- labels ]) $ + lift $ addEdgeM node DefaultBranch next return node + CCase _ s ni -> caseStat s ni next + CCases _ _ s ni -> caseStat s ni next + CDefault s ni -> caseStat s ni next + CFor init' mCond mStep s _ -> do condNode <- case mCond of Just cond -> newNode (BranchNode cond) @@ -221,3 +243,31 @@ buildStat stat next = case stat of node <- newNode (StatNode stat) lift $ addEdgeM node Unconditional next return node + +-- | The labels of a switch body, not counting those of nested switches, with +-- the edges that lead to them and whether they are the @default@ label. +caseLabels :: CStat -> BuildM [(Maybe Name, EdgeType, Node, Bool)] +caseLabels = \case + CCase e s ni -> label ni (CaseBranch e) False s + CCases _ _ s ni -> label ni DefaultBranch False s + CDefault s ni -> label ni DefaultBranch True s + CLabel _ s _ _ -> caseLabels s + CCompound _ bis _ -> concat <$> mapM caseLabels [ s | CBlockStmt s <- bis ] + CIf _ t e _ -> (++) <$> caseLabels t <*> maybe (return []) caseLabels e + CWhile _ s _ _ -> caseLabels s + CFor _ _ _ s _ -> caseLabels s + _ -> return [] + where + label ni edge isDefault s = do + node <- newNode (StatNode (CExpr Nothing ni)) + ((nameOfNode ni, edge, node, isDefault) :) <$> caseLabels s + +-- | A case label: the node the switch jumps to, followed by its statement. +caseStat :: CStat -> NodeInfo -> Node -> BuildM Node +caseStat s ni next = do + sEntry <- buildStat s next + asks (\env -> nameOfNode ni >>= (`Map.lookup` envCases env)) >>= \case + Just node -> do + lift $ addEdgeM node Unconditional sEntry + return node + Nothing -> return sEntry diff --git a/src/Tokstyle/C/Analysis/Interval.hs b/src/Tokstyle/C/Analysis/Interval.hs new file mode 100644 index 0000000..61e9fee --- /dev/null +++ b/src/Tokstyle/C/Analysis/Interval.hs @@ -0,0 +1,1079 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE Strict #-} +-- | Interval analysis of the integer values in a function. +-- +-- Each value is a set of ranges, and each range remembers whether arithmetic +-- that wrapped around its type produced it. Branch conditions narrow the +-- ranges of the locals and fields they test. +module Tokstyle.C.Analysis.Interval + ( IntTy (..) + , Origin (..) + , Range (..) + , Term (..) + , TermKind (..) + , Facts + , Program (..) + , emptyProgram + , Function + , translate + , solveFunction + , dependsOn + , canWrap + , eval + , subTerms + , normalise + , convert + , intType + ) where + +import Control.Monad (foldM, forM, forM_) +import Data.List (sortOn) +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Data.Maybe (fromMaybe, mapMaybe) +import Data.Set (Set) +import qualified Data.Set as Set +import Language.C.Analysis.AstAnalysis (defineParams) +import Language.C.Analysis.ConstEval (constEval, iSize, intValue) +import Language.C.Analysis.DeclAnalysis (analyseTypeDecl) +import Language.C.Analysis.DefTable (defineScopedIdent) +import Language.C.Analysis.MachineDescs (x86_64) +import Language.C.Analysis.SemRep (ArraySize (..), + Enumerator (..), FunDef (..), + FunType (..), IdentDecl (..), + IntType (..), ParamDecl (..), + Type (..), TypeName (..), + VarDecl (..), VarName (..), + declIdent, declType) +import Language.C.Analysis.TravMonad (MonadTrav, catchTravError, + enterBlockScope, + enterFunctionScope, + leaveBlockScope, + leaveFunctionScope, + lookupObject, withDefTable) +import Language.C.Analysis.TypeUtils (canonicalType) +import Language.C.Data.Ident (identToString) +import Language.C.Data.Name (Name) +import Language.C.Data.Node (NodeInfo, nameOfNode, + undefNode) +import Language.C.Syntax.AST +import Language.C.Syntax.Constants (getCInteger) +import Tokstyle.Analysis.AccessPath (AccessPath (..), + isPathPrefixOf) +import Tokstyle.Analysis.Dataflow (Dataflow (..), solve) +import Tokstyle.C.Analysis.CFG (CFG, EdgeType (..), + Node (..), NodeKind (..), + fromFunDef) +import Tokstyle.C.Analysis.Syntax (exprChildren, initExprs, + localDecls, statExprs) +import Tokstyle.C.Analysis.Types (FieldKey, exprType, fieldKey, + funKey, funType) + + +-- | Whether an integer type is signed, and its number of bits. +data IntTy = IntTy + { tySigned :: Bool + , tyBits :: Integer + , tyRange :: Range + -- ^ The values the type can hold. + } + deriving (Eq, Show) + +-- | Where the values in a range come from. +data Origin + = Plain + -- ^ Any value of the type, or a constant. + | Reduced + -- ^ An index reduced with @%@ or @&@. + | Arith + -- ^ Arithmetic, which may leave the type's range. + | Wrapped NodeInfo + -- ^ Arithmetic that went below zero and wrapped around to the top of an + -- unsigned type's range, at the given expression. + | Overflowed + -- ^ Arithmetic that went past the top of an unsigned type's range and + -- wrapped around to zero. + deriving (Eq, Show) + +-- | Values from 'lo' to 'hi' an expression can have. +data Range = Range + { lo :: Integer + , hi :: Integer + , origin :: Origin + } + deriving (Eq, Show) + +-- | An expression, with the integer type of its value if it has one. +data Term = Term + { termExpr :: CExpr + , termTy :: Maybe IntTy + , termFact :: Maybe Fact + -- ^ The fact about the program that says what values the term can have. + , termDefault :: Maybe [Range] + -- ^ The values the term can have when nothing else is known about it. + , termKind :: TermKind + } + +data TermKind + = TConst Integer + | TLoad AccessPath + | TBin CBinaryOp Term Term + | TUnary CUnaryOp Term + | TCast Term + | TCond Term (Maybe Term) Term + | TAssign (Maybe AccessPath) CAssignOp Term Term + | TIndex Term Term (Maybe Integer) + -- ^ An array access, with the array's length if it is known. + | TCall Term [Term] + | TOther [Term] + | TUnknown + -- ^ An expression the analysis doesn't model, which may change anything. + +-- | The values of the locals and fields known at a point in a function. A +-- path that isn't in the map can have any value of its type. +data Facts = Facts + { factsChanges :: Int + , factsBackEdge :: Bool + -- ^ Whether the facts arrive at a loop head from the end of the loop. + , factsValues :: Map AccessPath (IntTy, [Range]) + , factsDiffs :: Map (AccessPath, AccessPath) Integer + -- ^ For paths @p@ and @q@, the most @p - q@ can be. + } + deriving (Eq) + +-- | What a node of the control flow graph evaluates. +data NodeTerms + = Evaluates [Term] + | Declares [(AccessPath, IntTy, Maybe Term)] [Term] [Term] + -- ^ The locals a declaration initialises, the initialisers it evaluates, + -- and the terms to check, in which an initialiser converted to the type + -- of an integer is an assignment to it. + | Opaque + -- ^ A statement the graph doesn't model, which may change anything. + +intType :: Type -> Maybe IntTy +intType ty = case canonicalType ty of + DirectType (TyIntegral TyBool) _ _ -> Just (intTy False 1) + DirectType (TyIntegral it) _ _ -> Just (intTy (isSigned it) (8 * iSize x86_64 it)) + DirectType (TyEnum _) _ _ -> Just (intTy True 32) + _ -> Nothing + where + isSigned = (`notElem` [TyUChar, TyUShort, TyUInt, TyUInt128, TyULong, TyULLong]) + +intTy :: Bool -> Integer -> IntTy +intTy True bits = IntTy True bits (Range (-(2 ^ (bits - 1))) (2 ^ (bits - 1) - 1) Plain) +intTy False bits = IntTy False bits (Range 0 (2 ^ bits - 1) Plain) + +isWrapped :: Origin -> Bool +isWrapped = \case + Wrapped _ -> True + _ -> False + +-- | The values a conversion to an integer type at an expression turns a +-- range into. +convert :: NodeInfo -> IntTy -> Range -> [Range] +convert _ t@IntTy{tySigned = True} r + | lo r >= lo full && hi r <= hi full = [r] + | otherwise = [full] + where full = tyRange t +convert site t@IntTy{tySigned = False} (Range l h o) + | h - l >= m = + [ Range (m + max l (-m)) (m - 1) (moved (-1)) | l < 0 ] + ++ [ Range (max l 0) (min h (m - 1)) o | l < m, h >= 0 ] + ++ [ Range 0 (min (h - m) (m - 1)) (moved 1) | h >= m ] + | ql == qh = [Range (l `mod` m) (h `mod` m) (moved ql)] + | otherwise = [Range (l `mod` m) (m - 1) (moved ql), Range 0 (h `mod` m) (moved qh)] + where + m = hi (tyRange t) + 1 + ql = l `div` m + qh = h `div` m + moved :: Integer -> Origin + moved q + | q == 0 || isWrapped o = o + | o `elem` [Plain, Reduced] = Plain + | q < 0 = Wrapped site + | otherwise = Overflowed + +joinOrigin :: Origin -> Origin -> Origin +joinOrigin a b + | a == b = a + | isWrapped a = a + | isWrapped b = b + | Arith `elem` [a, b] = Arith + | otherwise = Plain + +-- | How many ranges from the same place a value keeps before they become one. +maxRanges :: Int +maxRanges = 3 + +-- | Sorts ranges and merges those that overlap and come from the same place. +-- Ranges that come from different places can overlap. +normalise :: [Range] -> [Range] +normalise rs = concatMap (cap . mergeRuns . sortOn lo) (groupByOrigin rs) + where + groupByOrigin xs = [ [ x | x <- xs, origin x == o ] | o <- distinct (map origin xs) ] + distinct = foldr (\x seen -> if x `elem` seen then seen else x : seen) [] + mergeRuns (a : b : rest) + | lo b <= hi a + 1 = mergeRuns (Range (lo a) (max (hi a) (hi b)) (origin a) : rest) + | otherwise = a : mergeRuns (b : rest) + mergeRuns short = short + cap xs + | length xs > maxRanges = [hull xs] + | otherwise = xs + +hull :: [Range] -> Range +hull xs = Range (minimum (map lo xs)) (maximum (map hi xs)) (foldr1 joinOrigin (map origin xs)) + +------------------------------------------------------------------------------ +-- Translating expressions + +-- | A fact about the program: the values of a field, or what a function +-- returns. +data Fact = FieldFact FieldKey | ReturnFact String + +-- | What is known about the program as a whole. +data Program = Program + { progFields :: Map FieldKey [Range] + -- ^ The values each field can have, for the fields the program only + -- changes in ways the analysis sees. + , progReturns :: Map String [Range] + -- ^ The values each function the program defines can return. + , progParams :: Map String [Maybe [Range]] + -- ^ The values each parameter of a static function can have, for the + -- functions the program only calls directly. + } + deriving (Eq) + +emptyProgram :: Program +emptyProgram = Program Map.empty Map.empty Map.empty + +-- | Where a function is analysed: the locals it can track, which are its +-- parameters and the locals it declares once, as long as it never takes their +-- address; and the translation unit, which tells static functions apart. +data Scope = Scope + { trackable :: Set String + , scopeUnit :: FilePath + } + +pathOf :: Scope -> CExpr -> Maybe AccessPath +pathOf scope = \case + CVar i _ | identToString i `Set.member` trackable scope -> Just (PathVar (identToString i)) + CMember e f True _ -> PathField . PathDeref <$> basePath e <*> pure (identToString f) + CMember e f False _ -> PathField <$> pathOf scope e <*> pure (identToString f) + CIndex e (CConst (CIntConst k _)) _ -> PathIndex <$> basePath e <*> pure (show (getCInteger k)) + _ -> Nothing + where + basePath = \case + CVar i _ -> Just (PathVar (identToString i)) + e -> pathOf scope e + +-- | Whether the memory a path names can change behind the function's back. +isMemory :: AccessPath -> Bool +isMemory = \case + PathVar _ -> False + PathField p _ -> isMemory p + _ -> True + +constValue :: MonadTrav m => CExpr -> m (Maybe Integer) +constValue e = (intValue <$> constEval x86_64 Map.empty e) `catchTravError` const (return Nothing) + +-- | The value of a constant expression, as far as it can be found without +-- evaluating every subexpression again. +literal :: MonadTrav m => CExpr -> m (Maybe Integer) +literal = \case + CConst (CIntConst i _) -> return (Just (getCInteger i)) + e@(CConst CCharConst{}) -> constValue e + CUnary CMinOp e _ -> fmap negate <$> literal e + CUnary CPlusOp e _ -> literal e + e@CSizeofExpr{} -> constValue e + e@CSizeofType{} -> constValue e + e@CAlignofExpr{} -> constValue e + e@CAlignofType{} -> constValue e + CVar i _ -> (lookupObject i `catchTravError` const (return Nothing)) >>= \case + Just (EnumeratorDef (Enumerator _ v _ _)) -> constValue v + _ -> return Nothing + _ -> return Nothing + +term :: MonadTrav m => Scope -> CExpr -> m Term +term scope e = literal e >>= \case + Just v -> do + ty <- (>>= intType) <$> exprType e + return (Term e ty Nothing Nothing (TConst v)) + Nothing -> do + k <- kind + ty <- typeOf k + fact <- case (ty, e) of + (Just _, CMember{}) -> fmap FieldFact <$> fieldKey e + (Just _, CCall (CVar f _) _ _) -> fmap ReturnFact <$> funKey (scopeUnit scope) f + _ -> return Nothing + return . Term e ty fact Nothing $ case (pathOf scope e, ty) of + (Just p, Just _) -> TLoad p + _ -> k + where + sub = term scope + kind = case e of + CBinary op a b _ -> TBin op <$> sub a <*> sub b + CUnary op a _ -> TUnary op <$> sub a + CCast _ a _ -> TCast <$> sub a + CCond c t f _ -> TCond <$> sub c <*> traverse sub t <*> sub f + CAssign op l r _ -> TAssign (pathOf scope l) op <$> sub l <*> sub r + CIndex a i _ -> TIndex <$> sub a <*> sub i <*> arrayLength a + CCall f args _ -> TCall <$> sub f <*> mapM sub args + CComma es _ -> TOther <$> mapM sub es + CMember a _ _ _ -> TOther . pure <$> sub a + CStatExpr{} -> return TUnknown + _ -> return (TOther []) + + -- The integer type of the expression, from the types of its operands + -- where C's conversions give it, and from its named declarations. + typeOf k = case (e, k) of + (CBinary op _ _ _, TBin _ a b) + | Just x <- termTy a, Just y <- termTy b -> return (Just (binaryType op x y)) + (CUnary op _ _, TUnary _ a) + | op `elem` [CMinOp, CPlusOp, CCompOp], Just x <- termTy a -> return (Just (promote x)) + | op `elem` [CPreIncOp, CPreDecOp, CPostIncOp, CPostDecOp] -> return (termTy a) + | op == CNegOp -> return (Just int) + | op == CAdrOp -> return Nothing + (CCast d _ _, _) -> (>>= intType) <$> declaredType d + (CCond{}, TCond _ (Just t) f) + | Just x <- termTy t, Just y <- termTy f -> return (Just (usual (promote x) (promote y))) + (CAssign{}, TAssign _ _ l _) -> return (termTy l) + (CComma{}, TOther ts@(_ : _)) -> return (termTy (last ts)) + (CVar i _, _) -> objectType i + (CCall (CVar f _) _ _, _) -> declTypeOf f >>= \case + Just t | Just ft <- funType t -> return (intType (resultType ft)) + _ -> fallback + _ -> fallback + + fallback = (>>= intType) <$> exprType e + + objectType i = (>>= intType) <$> declTypeOf i + + declTypeOf i = (fmap declType <$> lookupObject i) `catchTravError` const (return Nothing) + + resultType = \case + FunType rt _ _ -> rt + FunTypeIncomplete rt -> rt + + declaredType d = (Just <$> analyseTypeDecl d) `catchTravError` const (return Nothing) + + arrayLength a = exprType a >>= \case + Just (ArrayType _ (ArraySize _ size) _ _) -> constValue size + _ -> return Nothing + +int :: IntTy +int = intTy True 32 + +-- | Type integer promotion gives a value of a type. +promote :: IntTy -> IntTy +promote t + | tyBits t < 32 = int + | otherwise = t + +-- | Type the usual arithmetic conversions give two promoted types. +usual :: IntTy -> IntTy -> IntTy +usual a b + | tySigned a == tySigned b = if tyBits a >= tyBits b then a else b + | otherwise = + let (u, sg) = if tySigned a then (b, a) else (a, b) + in if tyBits u >= tyBits sg then u else sg + +-- | Type of a binary operation on integers. +binaryType :: CBinaryOp -> IntTy -> IntTy -> IntTy +binaryType op a b + | op `elem` [CLeOp, CGrOp, CLeqOp, CGeqOp, CEqOp, CNeqOp, CLndOp, CLorOp] = int + | op `elem` [CShlOp, CShrOp] = promote a + | otherwise = usual (promote a) (promote b) + +subTerms :: Term -> [Term] +subTerms t = t : concatMap subTerms (children t) + +------------------------------------------------------------------------------ +-- Evaluating terms + + +-- | The values a term can have, if it is an integer. +eval :: Facts -> Term -> Maybe [Range] +eval facts t = do + ty <- termTy t + let unknown = fromMaybe [tyRange ty] (termDefault t) + return . normalise . concatMap (convert site ty) $ case termKind t of + TConst v -> [Range v v Plain] + TLoad p -> maybe unknown snd (Map.lookup p (factsValues facts)) + TBin op a b -> fromMaybe unknown (binary ty op a b) + TUnary op a -> fromMaybe unknown (unary op a) + TCast a -> fromMaybe unknown (eval facts a) + TCond _ m f -> fromMaybe unknown ((++) <$> maybe (Just []) (eval facts) m <*> eval facts f) + TAssign _ op l r -> fromMaybe unknown (assigned facts site op l r) + _ -> unknown + where + site = annotation (termExpr t) + + binary ty op a b + | op `elem` [CLeOp, CGrOp, CLeqOp, CGeqOp, CEqOp, CNeqOp, CLndOp, CLorOp] = Just [Range 0 1 Plain] + | otherwise = do + ra <- eval facts a + rb <- eval facts b + arith facts site ty op ra rb a b + + unary op a = case op of + CMinOp -> map (\r -> Range (negate (hi r)) (negate (lo r)) (arithOrigin r r)) <$> eval facts a + CPlusOp -> eval facts a + CNegOp -> Just [Range 0 1 Plain] + CPreIncOp -> step 1 + CPreDecOp -> step (-1) + CPostIncOp -> eval facts a + CPostDecOp -> eval facts a + _ -> Nothing + where step d = map (\r -> Range (lo r + d) (hi r + d) (arithOrigin r r)) <$> eval facts a + +arithOrigin :: Range -> Range -> Origin +arithOrigin x y + | isWrapped (origin x) = origin x + | isWrapped (origin y) = origin y + | all constant [x, y] = Plain + | otherwise = Arith + where + constant r = lo r == hi r && origin r == Plain + +-- | The ranges arithmetic produces, before converting them to its type. +arith :: Facts -> NodeInfo -> IntTy -> CBinaryOp -> [Range] -> [Range] -> Term -> Term -> Maybe [Range] +arith facts site ty op ra rb a b = case op of + CAddOp -> Just [ Range (lo x + lo y) (hi x + hi y) (arithOrigin x y) | x <- ra, y <- rb ] + CSubOp -> Just (difference [ Range (lo x - hi y) (hi x - lo y) (arithOrigin x y) | x <- ra, y <- rb ]) + CMulOp -> Just [ products x y | x <- ra, y <- rb ] + CRmdOp -> divisor >>= \n -> + if n > 0 && all ((>= 0) . lo) ra' + then Just [Range 0 (min (n - 1) (maximum (map hi ra'))) Reduced] + else Nothing + CDivOp -> divisor >>= \n -> + if n > 0 + then Just [ Range (lo x `quot` n) (hi x `quot` n) (origin x) | x <- ra' ] + else Nothing + CShrOp -> divisor >>= \n -> + if n >= 0 && n < tyBits ty && all ((>= 0) . lo) ra' + then Just [ Range (lo x `div` (2 ^ n)) (hi x `div` (2 ^ n)) (origin x) | x <- ra' ] + else Nothing + CAndOp -> case [ v | Range v v' _ <- ra ++ rb, v == v', v >= 0 ] of + v : _ -> Just [Range 0 v Reduced] + [] -> Nothing + _ -> Nothing + where + -- What is known about how the paths in the operands relate bounds their + -- difference. + difference rs = case (linear facts a, linear facts b) of + (Just (Just p, ka), Just (Just q, kb)) -> + let lower = maybe (lo (hull rs)) (\c -> ka - kb - c) (Map.lookup (q, p) (factsDiffs facts)) + upper = maybe (hi (hull rs)) (\c -> ka - kb + c) (Map.lookup (p, q) (factsDiffs facts)) + clipped = clipRanges lower upper rs + in if null clipped then rs else clipped + _ -> rs + + -- Division and shifts work on values converted to the result type. + ra' = concatMap (convert site ty) ra + divisor = case termKind b of + TConst v -> Just v + _ -> case eval facts b of + Just [Range v v' _] | v == v' -> Just v + _ -> Nothing + products x y = + let ps = [ p * q | p <- [lo x, hi x], q <- [lo y, hi y] ] + in Range (minimum ps) (maximum ps) (arithOrigin x y) + +-- | The value an assignment at an expression stores. +assigned :: Facts -> NodeInfo -> CAssignOp -> Term -> Term -> Maybe [Range] +assigned facts site op l r = do + lt <- termTy l + rr <- eval facts r + vals <- case compound op of + Nothing -> Just rr + Just bop -> do + rl <- eval facts l + arith facts site lt bop rl rr l r + return (concatMap (convert site lt) vals) + where + compound = \case + CAssignOp -> Nothing + CMulAssOp -> Just CMulOp + CDivAssOp -> Just CDivOp + CRmdAssOp -> Just CRmdOp + CAddAssOp -> Just CAddOp + CSubAssOp -> Just CSubOp + CShlAssOp -> Just CShlOp + CShrAssOp -> Just CShrOp + CAndAssOp -> Just CAndOp + CXorAssOp -> Just CXorOp + COrAssOp -> Just COrOp + +------------------------------------------------------------------------------ +-- Effects + +-- | Records what a branch tells about the values of a path. +narrowPath :: AccessPath -> IntTy -> [Range] -> Facts -> Facts +narrowPath p ty v facts = facts { factsValues = Map.insert p (ty, v) (factsValues facts) } + +-- | Records a write of the values to a path. +setPath :: AccessPath -> IntTy -> [Range] -> Facts -> Facts +setPath p ty v facts = narrowPath p ty v (forget p facts) + +-- | Records a write that adds a constant to a path, which keeps how it relates +-- to other paths. +shiftPath :: AccessPath -> IntTy -> [Range] -> Integer -> Facts -> Facts +shiftPath p ty v d facts = narrowPath p ty v shifted + where + others = forgetWhere (\q -> q /= p && overwrittenBy p q) facts + shifted = others { factsDiffs = Map.mapWithKey move (factsDiffs others) } + move (a, b) c + | a == p = c + d + | b == p = c - d + | otherwise = c + +-- | Whether writing the first path can change what the second holds: its +-- parts, and memory that may be the same. +overwrittenBy :: AccessPath -> AccessPath -> Bool +overwrittenBy p q = p `isPathPrefixOf` q || isMemory p && isMemory q && mayAlias p q + where + mayAlias (PathField _ f) (PathField _ g) = f == g + mayAlias _ _ = True + +-- | Forgets what is known about a path and what writing it can change. +forget :: AccessPath -> Facts -> Facts +forget p = forgetWhere (overwrittenBy p) + +forgetWhere :: (AccessPath -> Bool) -> Facts -> Facts +forgetWhere gone facts = facts + { factsValues = Map.filterWithKey (\q _ -> not (gone q)) (factsValues facts) + , factsDiffs = Map.filterWithKey (\(a, b) _ -> not (gone a || gone b)) (factsDiffs facts) + } + +forgetMemory :: Facts -> Facts +forgetMemory = forgetWhere isMemory + +forgetAll :: Facts -> Facts +forgetAll = forgetWhere (const True) + +-- | Records that @p - q@ is at most a constant, or 'Nothing' if what is known +-- says it can't be. +relate :: AccessPath -> AccessPath -> Integer -> Facts -> Maybe Facts +relate p q c facts + | p == q = if c >= 0 then Just facts else Nothing + | Just c' <- Map.lookup (q, p) (factsDiffs facts), c + c' < 0 = Nothing + | otherwise = Just facts { factsDiffs = Map.insertWith min (p, q) c (factsDiffs facts) } + +-- | A term whose value is a path plus a constant, or a constant, computed +-- without wrapping around. A path counts as itself even if its value wrapped. +linear :: Facts -> Term -> Maybe (Maybe AccessPath, Integer) +linear facts t = case termKind (stripCasts t) of + TLoad p -> Just (Just p, 0) + _ -> do + rs <- eval facts t + if any (wraps . origin) rs then Nothing else go t + where + wraps = \case + Wrapped _ -> True + Overflowed -> True + _ -> False + go u = case termKind (stripCasts u) of + TConst k -> Just (Nothing, k) + TLoad p -> Just (Just p, 0) + TBin CAddOp a b -> do + x <- go a + y <- go b + case (x, y) of + ((Just p, k), (Nothing, k')) -> Just (Just p, k + k') + ((Nothing, k), (Just p, k')) -> Just (Just p, k + k') + ((Nothing, k), (Nothing, k')) -> Just (Nothing, k + k') + _ -> Nothing + TBin CSubOp a b -> do + x <- go a + y <- go b + case (x, y) of + ((p, k), (Nothing, k')) -> Just (p, k - k') + _ -> Nothing + _ -> Nothing + +-- | Records how an assigned path relates to the path it was assigned from. +relateAssigned :: Facts -> AccessPath -> IntTy -> Term -> Facts -> Facts +relateAssigned before p ty r after = case (linear before r, eval before r) of + (Just (Just q, c), Just v) | q /= p, all (fitsIn ty) v -> + fromMaybe after (relate p q c after >>= relate q p (negate c)) + _ -> after + where + fitsIn t x = lo x >= lo (tyRange t) && hi x <= hi (tyRange t) + +clipRanges :: Integer -> Integer -> [Range] -> [Range] +clipRanges a b = mapMaybe $ \x -> + let x' = Range (max a (lo x)) (min b (hi x)) (origin x) + in if lo x' <= hi x' then Just x' else Nothing + +-- | What evaluating a term does to the facts. Writes that only happen on +-- some paths through the term forget the paths they write. +effects :: Bool -> Term -> Facts -> Facts +effects definite t facts = case termKind t of + TAssign mp op l r -> + let after = effects definite l (effects definite r facts) + in case (mp, termTy l) of + (Just p, Just ty) | definite, Just v <- assigned facts site op l r -> + let selfShift = case (op, linear facts r) of + (CAssignOp, Just (Just q, c)) | q == p -> Just c + (CAddAssOp, Just (Nothing, c)) -> Just c + (CSubAssOp, Just (Nothing, c)) -> Just (negate c) + _ -> Nothing + in case selfShift of + Just c | noWrap v -> shiftPath p ty v c after + _ | op == CAssignOp -> relateAssigned facts p ty r (setPath p ty v after) + _ -> setPath p ty v after + (Just p, _) -> forget p after + (Nothing, _) -> forgetWrite l after + TUnary op a | op `elem` [CPreIncOp, CPreDecOp, CPostIncOp, CPostDecOp] -> + let after = effects definite a facts + d = if op `elem` [CPreIncOp, CPostIncOp] then 1 else -1 + in case (termKind a, termTy a, eval facts a) of + (TLoad p, Just ty, Just v) | definite -> + let v' = normalise (concatMap (convert site ty) [ Range (lo r + d) (hi r + d) (arithOrigin r r) | r <- v ]) + in if noWrap v' then shiftPath p ty v' d after else setPath p ty v' after + (TLoad p, _, _) -> forget p after + _ -> forgetWrite a after + TCall f args -> forgetMemory (foldl (flip (effects definite)) (effects definite f facts) args) + TBin op a b | op `elem` [CLndOp, CLorOp] -> effects False b (effects definite a facts) + TCond c m f -> foldl (flip (effects False)) (effects definite c facts) (maybe [] pure m ++ [f]) + TUnknown -> forgetAll facts + _ -> foldl (flip (effects definite)) facts (children t) + where + site = annotation (termExpr t) + noWrap = all $ \x -> case origin x of + Wrapped _ -> False + Overflowed -> False + _ -> True + forgetWrite l = case termExpr l of + CMember _ f _ _ -> forgetField (identToString f) + _ -> forgetMemory + +-- | Forgets the field with this name of any object in memory, and memory it +-- may be part of. +forgetField :: String -> Facts -> Facts +forgetField f = forgetWhere $ \q -> isMemory q && case q of + PathField _ g -> g == f + _ -> True + +children :: Term -> [Term] +children t = case termKind t of + TBin _ a b -> [a, b] + TUnary _ a -> [a] + TCast a -> [a] + TCond c m f -> c : maybe [] pure m ++ [f] + TAssign _ _ l r -> [l, r] + TIndex a i _ -> [a, i] + TCall f args -> f : args + TOther ts -> ts + _ -> [] + +------------------------------------------------------------------------------ +-- Branch conditions + +-- | The comparison with its operands swapped. +swapOp :: CBinaryOp -> CBinaryOp +swapOp = \case + CLeOp -> CGrOp + CGrOp -> CLeOp + CLeqOp -> CGeqOp + CGeqOp -> CLeqOp + op -> op + +-- | The comparison that holds when this one doesn't. +negateOp :: CBinaryOp -> CBinaryOp +negateOp = \case + CLeOp -> CGeqOp + CGrOp -> CLeqOp + CLeqOp -> CGrOp + CGeqOp -> CLeOp + CEqOp -> CNeqOp + _ -> CEqOp + +joinFacts :: Facts -> Facts -> Facts +joinFacts a b = Facts + { factsChanges = max (factsChanges a) (factsChanges b) + , factsBackEdge = False + , factsValues = Map.intersectionWith (\(ty, x) (_, y) -> (ty, normalise (x ++ y))) (factsValues a) (factsValues b) + , factsDiffs = Map.intersectionWith max (factsDiffs a) (factsDiffs b) + } + +joinMaybe :: Maybe Facts -> Maybe Facts -> Maybe Facts +joinMaybe (Just a) (Just b) = Just (joinFacts a b) +joinMaybe a Nothing = a +joinMaybe Nothing b = b + +-- | The facts on the paths where a condition has the given truth value, or +-- 'Nothing' if it can't have it. +assume :: Bool -> Term -> Facts -> Maybe Facts +assume truth t facts = case termKind t of + TUnary CNegOp a -> assume (not truth) a facts + TBin CLndOp a b + | truth -> assume True a facts >>= assume True b + | otherwise -> assume False a facts `joinMaybe` (assume True a facts >>= assume False b) + TBin CLorOp a b + | truth -> assume True a facts `joinMaybe` (assume False a facts >>= assume True b) + | otherwise -> assume False a facts >>= assume False b + TBin op a b | op `elem` [CLeOp, CGrOp, CLeqOp, CGeqOp, CEqOp, CNeqOp] -> + let op' = if truth then op else negateOp op + in compareFacts op' a b facts + TCast a | Just v <- eval facts a, all (`fits` termTy t) v -> assume truth a facts + TLoad _ -> compareFacts (if truth then CNeqOp else CEqOp) t zero facts + _ -> Just facts + where + zero = Term (termExpr t) (termTy t) Nothing Nothing (TConst 0) + fits r = maybe False (\ty -> lo r >= lo (tyRange ty) && hi r <= hi (tyRange ty)) + +-- | Narrows the paths the sides of a comparison that holds read, and records +-- how they relate. +compareFacts :: CBinaryOp -> Term -> Term -> Facts -> Maybe Facts +compareFacts op l r facts = case (eval facts l, eval facts r) of + (Just lv@(_ : _), Just rv@(_ : _)) | exact lv rv -> + narrowSide op l lv rv facts >>= narrowSide (swapOp op) r rv lv >>= relateSides + _ -> Just facts + where + -- The comparison is between the values themselves, rather than values + -- converted to an unsigned type, if neither side can be negative. + exact lv rv = all ((>= 0) . lo) lv && all ((>= 0) . lo) rv + || all signed [l, r] + signed x = maybe False tySigned (termTy x) + + relateSides f = case (linear facts l, linear facts r) of + (Just (Just p, a), Just (Just q, b)) -> case op of + CLeOp -> relate p q (b - a - 1) f + CLeqOp -> relate p q (b - a) f + CGrOp -> relate q p (a - b - 1) f + CGeqOp -> relate q p (a - b) f + CEqOp -> relate p q (b - a) f >>= relate q p (a - b) + _ -> Just f + _ -> Just f + +-- | Narrows the path one side of a comparison that holds reads, given the +-- values of both sides, or 'Nothing' if the comparison can't hold. +narrowSide :: CBinaryOp -> Term -> [Range] -> [Range] -> Facts -> Maybe Facts +narrowSide op t tv ov facts = case (termKind (stripCasts t), termTy (stripCasts t)) of + (TLoad p, Just ty) | not (null narrowed) -> Just (narrowPath p ty narrowed facts) + | otherwise -> Nothing + where narrowed = narrow ty + _ | op == CEqOp, null (clipRanges ol oh tv) -> Nothing + | otherwise -> Just facts + where + Range ol oh _ = hull ov + narrow ty = case op of + CLeOp -> clipRanges (lo (tyRange ty)) (oh - 1) tv + CLeqOp -> clipRanges (lo (tyRange ty)) oh tv + CGrOp -> clipRanges (ol + 1) (hi (tyRange ty)) tv + CGeqOp -> clipRanges ol (hi (tyRange ty)) tv + CEqOp -> clipRanges ol oh tv + _ | ol == oh -> concatMap (remove ol) tv + | otherwise -> tv + remove v x + | v < lo x || v > hi x = [x] + | otherwise = [ y | y <- [Range (lo x) (v - 1) (origin x), Range (v + 1) (hi x) (origin x)], lo y <= hi y ] + +-- | The term a value-preserving cast converts. +stripCasts :: Term -> Term +stripCasts t = case termKind t of + TCast a | Just _ <- termTy a, termTy a == termTy t -> stripCasts a + _ -> t + +------------------------------------------------------------------------------ +-- The analysis + +-- | How many times the facts at a loop head can change before ranges that keep +-- growing widen to their type's range. +roundsBeforeWidening :: Int +roundsBeforeWidening = 3 + +-- | Joins the facts from two paths, widening at loop heads. +mergeFacts :: Maybe Facts -> Maybe Facts -> Maybe Facts +mergeFacts (Just old) (Just new) + | joined == old = Just old + | factsBackEdge new && factsChanges old >= roundsBeforeWidening = Just (widen old joined) + | otherwise = Just joined { factsChanges = factsChanges old + 1 } + where + joined = (joinFacts old new) { factsChanges = factsChanges old } +mergeFacts a b = joinMaybe a b + +widen :: Facts -> Facts -> Facts +widen old joined = joined + { factsChanges = factsChanges old + 1 + , factsValues = Map.mapWithKey grow (factsValues joined) + , factsDiffs = Map.filterWithKey steady (factsDiffs joined) + } + where + steady k c = maybe False (>= c) (Map.lookup k (factsDiffs old)) + grow p (ty, v) = case Map.lookup p (factsValues old) of + Just (_, ov) | v == ov -> (ty, v) + Just (_, ov) -> + let Range nl nh o = hull v + Range ol oh _ = hull ov + l = if nl < ol then lo (tyRange ty) else nl + h = if nh > oh then hi (tyRange ty) else nh + in (ty, [Range l h o]) + Nothing -> (ty, v) + +paramNames :: FunDef -> [String] +paramNames (FunDef (VarDecl _ _ ty) _ _) = case ty of + FunctionType (FunType _ params _) _ -> + [ identToString i | p <- params, VarName i _ <- [paramVarName p] ] + _ -> [] + +paramVarName :: ParamDecl -> VarName +paramVarName = \case + ParamDecl (VarDecl n _ _) _ -> n + AbstractParamDecl (VarDecl n _ _) _ -> n + +-- | The locals a function declares, once for each declaration. +declaredNames :: CStat -> [String] +declaredNames body = + [ identToString i | CDecl _ ds _ <- localDecls body, (Just (CDeclr (Just i) _ _ _ _), _, _) <- ds ] + +-- | The locals a function declares @static@ or @extern@, whose values outlive +-- a call. +storedElsewhere :: CStat -> Set String +storedElsewhere body = Set.fromList + [ identToString i + | CDecl specs ds _ <- localDecls body, any isStorage specs + , (Just (CDeclr (Just i) _ _ _ _), _, _) <- ds ] + where + isStorage = \case + CStorageSpec CStatic{} -> True + CStorageSpec CExtern{} -> True + _ -> False + +-- | The names whose address a statement takes. +addressTaken :: CStat -> Set String +addressTaken = Set.fromList . everything + where + everything s = concatMap exprAddrs (statExprs s) + exprAddrs = \case + CUnary CAdrOp e _ -> base e ++ exprAddrs e + CVar{} -> [] + e -> concatMap exprAddrs (exprChildren e) + base = \case + CVar i _ -> [identToString i] + CMember e _ _ _ -> base e + CIndex e _ _ -> base e + _ -> [] + +-- | Whether a function does anything that can make a value wrap around below +-- zero: subtract, decrement or negate. Values from the rest of the program +-- never come wrapped, so only these can. +canWrap :: FunDef -> Bool +canWrap (FunDef _ body _) = any (any wraps . everyExpr) (statExprs body) + where + everyExpr e = e : concatMap everyExpr (exprChildren e) + wraps = \case + CBinary CSubOp _ _ _ -> True + CAssign CSubAssOp _ _ _ -> True + CUnary CPreDecOp _ _ -> True + CUnary CPostDecOp _ _ -> True + CUnary CMinOp _ _ -> True + _ -> False + +nodeTermsOf :: MonadTrav m => Scope -> Node -> m NodeTerms +nodeTermsOf scope (Node _ kind) = case kind of + StatNode (CExpr e _) -> Evaluates <$> mapM (term scope) (maybe [] pure e) + StatNode (CReturn e _) -> Evaluates <$> mapM (term scope) (maybe [] pure e) + StatNode CBreak{} -> return (Evaluates []) + StatNode CCont{} -> return (Evaluates []) + StatNode CGoto{} -> return (Evaluates []) + StatNode CFor{} -> return (Evaluates []) + StatNode _ -> return Opaque + ExprNode e -> Evaluates . pure <$> term scope e + BranchNode e -> Evaluates . pure <$> term scope e + DeclNode (CDecl _ ds _) -> do + items <- forM ds $ \case + (Just (CDeclr (Just i) _ _ _ ni), Just (CInitExpr e _), _) -> do + ty <- (>>= intType) <$> exprType (CVar i ni) + t <- term scope e + let path = if identToString i `Set.member` trackable scope then Just (PathVar (identToString i)) else Nothing + var = Term (CVar i ni) ty Nothing Nothing (maybe (TOther []) TLoad path) + assign = Term (CAssign CAssignOp (CVar i ni) e ni) ty Nothing Nothing (TAssign path CAssignOp var t) + return ( [ (p, vt, Just t) | Just p <- [path], Just vt <- [ty] ], [t] + , [maybe t (const assign) ty] ) + (Just (CDeclr (Just i) _ _ _ ni), ini, _) -> do + ty <- (>>= intType) <$> exprType (CVar i ni) + ts <- mapM (term scope) (maybe [] initExprs ini) + return ( [ (PathVar (identToString i), vt, Nothing) | Just vt <- [ty], identToString i `Set.member` trackable scope ] + , ts, ts ) + (_, ini, _) -> do + ts <- mapM (term scope) (maybe [] initExprs ini) + return ([], ts, ts) + return $ Declares (concat [ v | (v, _, _) <- items ]) (concat [ e | (_, e, _) <- items ]) + (concat [ c | (_, _, c) <- items ]) + DeclNode _ -> return Opaque + EntryNode -> return (Evaluates []) + ExitNode -> return (Evaluates []) + +mapTerms :: (Term -> Term) -> NodeTerms -> NodeTerms +mapTerms f = \case + Evaluates ts -> Evaluates (map f ts) + Declares vars inits ts -> Declares [ (p, ty, f <$> t) | (p, ty, t) <- vars ] (map f inits) (map f ts) + Opaque -> Opaque + +termsOf :: NodeTerms -> [Term] +termsOf = \case + Evaluates ts -> ts + Declares _ _ ts -> ts + Opaque -> [] + +transferTerms :: NodeTerms -> Facts -> Facts +transferTerms nt facts = case nt of + Evaluates ts -> foldl (flip (effects True)) facts ts + Declares vars inits _ -> + let after = foldl (flip (effects True)) facts inits + in foldl (\f (p, ty, ini) -> case ini >>= eval facts of + Just v -> setPath p ty (normalise (concatMap (convert (initSite ini) ty) v)) f + Nothing -> forget p f) after vars + Opaque -> forgetAll facts + where + initSite = maybe undefNode (annotation . termExpr) + +-- | A function as the analysis sees it: its control flow graph and the terms +-- each node evaluates. +data Function = Function + { fnEntry :: Node + , fnCfg :: CFG + , fnTerms :: Map Node NodeTerms + , fnCases :: Map Name Integer + -- ^ The value of each case label. + , fnParams :: [Maybe (AccessPath, IntTy)] + -- ^ The paths of the parameters the analysis tracks. + , fnSelf :: Maybe String + } + +-- | A function in a translation unit, given the declarations of its locals as +-- analysing the translation unit found them. +translate :: MonadTrav m => FilePath -> [IdentDecl] -> FunDef -> m Function +translate unit locals fd@(FunDef decl _ ni) = do + enterFunctionScope + defineParams ni decl + enterBlockScope + forM_ locals $ \d -> withDefTable $ \dt -> ((), snd (defineScopedIdent (declIdent d) d dt)) + result <- translateBody unit fd + leaveBlockScope + leaveFunctionScope + return result + +translateBody :: MonadTrav m => FilePath -> FunDef -> m Function +translateBody unit fd@(FunDef (VarDecl self _ ty) body _) = do + let (entry, cfg) = fromFunDef fd + nodes = Set.toList . Set.fromList $ Map.keys cfg ++ [ n | es <- Map.elems cfg, (_, n) <- es ] + declared = paramNames fd ++ declaredNames body + counts = Map.fromListWith (+) [ (n, 1 :: Int) | n <- declared ] + scope = Scope + { trackable = Map.keysSet (Map.filter (== 1) counts) + `Set.difference` (addressTaken body <> storedElsewhere body) + , scopeUnit = unit + } + terms <- Map.fromList <$> forM nodes (\n -> (,) n <$> nodeTermsOf scope n) + selfKey <- case self of + VarName i _ -> funKey unit i + NoName -> return Nothing + caseValues <- caseConstants cfg + return Function + { fnEntry = entry + , fnCfg = cfg + , fnTerms = terms + , fnCases = caseValues + , fnParams = + [ case (paramVarName p, intType (declType p)) of + (VarName i _, Just t) | identToString i `Set.member` trackable scope -> Just (PathVar (identToString i), t) + _ -> Nothing + | FunctionType (FunType _ params _) _ <- [ty], p <- params ] + , fnSelf = selfKey + } + where + caseConstants :: MonadTrav m => CFG -> m (Map Name Integer) + caseConstants cfg = fmap (Map.fromList . concat) . forM [ v | es <- Map.elems cfg, (CaseBranch v, _) <- es ] $ \v -> + constValue v >>= \k -> return [ (n, x) | Just n <- [nameOfNode (annotation v)], Just x <- [k] ] + +-- | Whether what is known about the program says more about a function than +-- knowing nothing about it. +dependsOn :: Program -> Function -> Bool +dependsOn prog fn = maybe False (`Map.member` progParams prog) (fnSelf fn) + || any (maybe False known . termFact) (concatMap (concatMap subTerms . termsOf) (Map.elems (fnTerms fn))) + where + known = \case + FieldFact k -> k `Map.member` progFields prog + ReturnFact k -> k `Map.member` progReturns prog + +-- | A term with its defaults from what is known about the program. +withProgram :: Program -> Term -> Term +withProgram prog = go + where + go t = t { termDefault = termFact t >>= known, termKind = kind (termKind t) } + kind = \case + TBin op a b -> TBin op (go a) (go b) + TUnary op a -> TUnary op (go a) + TCast a -> TCast (go a) + TCond c m f -> TCond (go c) (go <$> m) (go f) + TAssign p op l r -> TAssign p op (go l) (go r) + TIndex a i n -> TIndex (go a) (go i) n + TCall f args -> TCall (go f) (map go args) + TOther ts -> TOther (map go ts) + k -> k + known = \case + FieldFact k -> Map.lookup k (progFields prog) + ReturnFact k -> Map.lookup k (progReturns prog) + +-- | The facts before each reachable node of a function, with the terms the +-- node evaluates, given what is known about the program. +solveFunction :: Program -> Function -> [(Node, Facts, [Term])] +solveFunction prog fn = [ (n, facts, termsOf (termsAt n)) | (n, Just facts) <- Map.toList result ] + where + entry = fnEntry fn + cfg = fnCfg fn + terms = Map.map (mapTerms (withProgram prog)) (fnTerms fn) + entryFacts = paramFacts (fnParams fn) (fnSelf fn >>= (`Map.lookup` progParams prog)) + termsAt n = Map.findWithDefault (Evaluates []) n terms + condOf n = case termsAt n of + Evaluates [c] | Node _ BranchNode{} <- n -> Just c + _ -> Nothing + back = backEdges entry cfg + isBack n e = or [ (n, v) `Set.member` back | (e', v) <- Map.findWithDefault [] n cfg, sameEdge e e' ] + edgeTransferNode n e s = (\f -> f { factsBackEdge = isBack n e }) <$> (s >>= \facts -> case (condOf n, e) of + (Just c, TrueBranch) -> assume True c facts + (Just c, FalseBranch) -> assume False c facts + (Just c, CaseBranch v) | Just k <- caseValue v -> + compareFacts CEqOp c (Term v (termTy c) Nothing Nothing (TConst k)) facts + (Just c, DefaultBranch) -> + foldM (\f (v, k) -> compareFacts CNeqOp c (Term v (termTy c) Nothing Nothing (TConst k)) f) facts + [ (v, k) | (CaseBranch v, _) <- Map.findWithDefault [] n cfg, Just k <- [caseValue v] ] + _ -> Just facts) + where caseValue v = nameOfNode (annotation v) >>= (`Map.lookup` fnCases fn) + problem = Dataflow + { transfer = \n s -> (\f -> (transferTerms (termsAt n) f) { factsBackEdge = False }) <$> s + , edgeTransfer = edgeTransferNode + , merge = mergeFacts + , initial = Just entryFacts + } + result = solve entry cfg problem + +sameEdge :: EdgeType -> EdgeType -> Bool +sameEdge (CaseBranch a) (CaseBranch b) = nameOfNode (annotation a) == nameOfNode (annotation b) +sameEdge a b = a == b + +-- | The edges that go back to a node the depth-first search from the entry is +-- still inside. Every cycle in the graph has one. +backEdges :: Node -> CFG -> Set (Node, Node) +backEdges entry cfg = snd (visit Set.empty entry (Set.empty, Set.empty)) + where + visit stack n acc@(done, back) + | n `Set.member` done = acc + | otherwise = + let stack' = Set.insert n stack + step acc'@(d, b) (_, m) + | m `Set.member` stack' = (d, Set.insert (n, m) b) + | otherwise = visit stack' m acc' + (done', back') = foldl step (Set.insert n done, back) (Map.findWithDefault [] n cfg) + in (done', back') + +-- | The facts at the entry of a function whose parameters are known to have +-- the given values. +paramFacts :: [Maybe (AccessPath, IntTy)] -> Maybe [Maybe [Range]] -> Facts +paramFacts params known = Facts 0 False values Map.empty + where + values = Map.fromList [ (p, (t, v)) | (Just (p, t), Just v) <- zip params (fromMaybe [] known) ] diff --git a/src/Tokstyle/C/Analysis/Program.hs b/src/Tokstyle/C/Analysis/Program.hs new file mode 100644 index 0000000..58a89c5 --- /dev/null +++ b/src/Tokstyle/C/Analysis/Program.hs @@ -0,0 +1,338 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE Strict #-} +-- | Facts about a whole program, found by analysing each of its translation +-- units without knowing anything about the rest, and joining what they show. +-- +-- A field's values are the values the program stores in it, as long as it +-- only changes the field in ways the analysis sees. A function's results are +-- the values it returns, and a static function's parameters are the values its +-- direct calls pass, as long as nothing takes its address. +module Tokstyle.C.Analysis.Program + ( Observed + , Analysed + , observe + , programFrom + ) where + +import Control.Monad (forM) +import Data.List (isPrefixOf) +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Data.Maybe (catMaybes, fromMaybe, isJust, + isNothing, maybeToList) +import qualified Data.Set as Set +import Language.C.Analysis.DeclAnalysis (analyseTypeDecl) +import Language.C.Analysis.SemRep (CompType (..), FunDef (..), + FunType (..), + GlobalDecls (..), + IdentDecl (..), ObjDef (..), + TagDef (..), Type (..), + TypeName (..), VarDecl (..), + VarName (..), constant, + declType) +import Language.C.Analysis.TravMonad (MonadTrav, catchTravError, + lookupObject) +import Language.C.Analysis.TypeUtils (canonicalType, typeQuals) +import Language.C.Data.Ident (SUERef (..), identToString) +import Language.C.Data.Node (posOfNode, undefNode) +import Language.C.Data.Position (isSourcePos, posFile) +import Language.C.Syntax.AST +import Language.C.Syntax.Constants (getCInteger) +import Tokstyle.C.Analysis.CFG (Node (..), NodeKind (..)) +import Tokstyle.C.Analysis.Interval (Facts, Function, IntTy (..), + Origin (..), Program (..), + Range (..), Term (..), + TermKind (..), canWrap, + convert, emptyProgram, eval, + intType, normalise, + solveFunction, subTerms, + translate) +import Tokstyle.C.Analysis.Syntax (exprChildren, initExprs, + localDecls, statExprs) +import Tokstyle.C.Analysis.Types (FieldKey, exprType, fieldKey, + funKey, funType, structTag) + + +-- | Values seen for a field, a result or a parameter, with their type if +-- known. +type Values = (Maybe IntTy, [Range]) + +-- | Something a translation unit shows about the program. +data Observation + = Stored FieldKey Values + -- ^ Values stored in a field. + | Escaped FieldKey + -- ^ A field changed in ways the analysis doesn't see. + | EscapedTag String + -- ^ A struct whose fields change in ways the analysis doesn't see. + | HandedTo String [String] + -- ^ Structs a function gets a pointer to that it may write through, or + -- returns. Unless the program defines the function, their fields change + -- in ways the analysis doesn't see. + | Returned String Values + | Passed String [Maybe Values] + -- ^ The values a static function gets for each parameter. + | Addressed String + -- ^ A function used other than by calling it. + | Defined String + +-- | Everything a translation unit shows about the program. +type Observed = [Observation] + +-- | A function, with the facts before each of its nodes when nothing is known +-- about the rest of the program. +type Analysed = (Function, [(Node, Facts, [Term])]) + +-- | External functions that don't change the objects their pointers point to +-- in ways the analysis needs to see. +harmless :: [String] +harmless = ["free", "memset", "memcpy", "memmove", "crypto_memzero", "sodium_memzero"] + +-- | Forgets where values came from: facts about the program carry bounds and +-- which values are reduced indices, not which ones wrapped around. +plain :: [Range] -> [Range] +plain = map $ \r -> if origin r == Reduced then r else r { origin = Plain } + +-- | The facts about the program its translation units show. Facts that say no +-- more than a value's type are left out. +programFrom :: Observed -> Program +programFrom obs = Program + { progFields = Map.fromList + [ (k, v) + | (k@(tag, _), (ty, vs)) <- Map.toList (Map.fromListWith joinValues [ (k', v) | Stored k' v <- obs ]) + , tag `Set.notMember` escapedTags + , k `Set.notMember` escaped + , let v = invariant vs + , not (trivial ty v) + ] + , progReturns = Map.fromList + [ (k, v) + | (k, (ty, vs)) <- Map.toList (Map.fromListWith joinValues [ (k', v) | Returned k' v <- obs ]) + , k `Set.member` defined + , let v = normalise vs + , not (trivial ty v) + ] + , progParams = Map.fromList + [ (k, ps) + | (k, args) <- Map.toList (Map.fromListWith (zipWith (\x y -> joinValues <$> x <*> y)) [ (k', a) | Passed k' a <- obs ]) + , k `Set.member` defined, k `Set.notMember` addressed + , let ps = map known args + , any isJust ps + ] + } + where + defined = Set.fromList [ f | Defined f <- obs ] + addressed = Set.fromList [ f | Addressed f <- obs ] + escaped = Set.fromList [ k | Escaped k <- obs ] + escapedTags = Set.fromList $ [ tag | EscapedTag tag <- obs ] + ++ [ tag | HandedTo f tags <- obs, f `Set.notMember` defined, tag <- tags ] + + joinValues (t1, a) (t2, b) = (maybe t2 Just t1, a ++ b) + + known = \case + Just (ty, vs) | let v = normalise vs, not (trivial ty v) -> Just v + _ -> Nothing + + trivial ty v = case (ty, v) of + (Just t, [Range l h Plain]) -> l <= lo (tyRange t) && h >= hi (tyRange t) + _ -> False + + -- Zero is always among a field's values: memory starts out zeroed. A + -- constant within an index range keeps it an index range. + invariant vs = + let vals = Range 0 0 Plain : vs + reduced = [ r | r <- vals, origin r == Reduced ] + absorbed r = lo r == hi r && origin r == Plain + && any (\x -> lo x <= lo r && hi r <= hi x) reduced + in normalise (filter (not . absorbed) vals) + +-- | What a translation unit shows about the program, and the analysis of its +-- functions that can wrap around. +observe :: MonadTrav m => FilePath -> Map String [IdentDecl] -> GlobalDecls -> m (Observed, [Analysed]) +observe unit locals decls = do + perFunction <- forM [ (i, fd) | FunctionDef fd@(FunDef (VarDecl (VarName i _) _ _) _ _) <- objs ] $ \(i, fd) -> do + (o, analysed) <- observeFunction unit (Map.findWithDefault [] (identToString i) locals) fd + return (o, [ analysed | canWrap fd ]) + perObject <- forM [ od | ObjectDef od <- objs ] (observeObject unit) + return ( concatMap fst perFunction ++ concat perObject ++ map EscapedTag (Set.toList externalTags) + , concatMap snd perFunction ) + where + objs = Map.elems (gObjs decls) + -- Structs the project doesn't define, like the system's, change in ways + -- the analysis doesn't see. + externalTags = Set.fromList + [ identToString i + | (NamedRef i, CompDef (CompType _ _ _ _ ni)) <- Map.toList (gTags decls) + , let pos = posOfNode ni + , not (isSourcePos pos) || "/" `isPrefixOf` posFile pos + ] + +observeObject :: MonadTrav m => FilePath -> ObjDef -> m Observed +observeObject unit (ObjDef (VarDecl _ _ ty) ini _) = case ini of + Just i -> (<>) <$> initializer ty i <*> foldMapM (observeExpr unit) (initExprs i) + Nothing -> return mempty + +foldMapM :: (Monad m, Monoid b) => (a -> m b) -> [a] -> m b +foldMapM f xs = mconcat <$> mapM f xs + +-- | What an initialiser for an object of a type stores in its fields. +initializer :: MonadTrav m => Type -> CInit -> m Observed +initializer ty = \case + CInitList items _ | Just tag <- structTag ty -> return $ mconcat (map (item tag) items) + _ -> return mempty + where + item tag = \case + ([CMemberDesig f _], CInitExpr e _) -> case literalValue e of + Just v -> [Stored (tag, identToString f) (Nothing, [Range v v Plain])] + Nothing -> [Escaped (tag, identToString f)] + ([], CInitExpr e _) | literalValue e == Just 0 -> mempty + _ -> [EscapedTag tag] + literalValue = \case + CConst (CIntConst i _) -> Just (getCInteger i) + _ -> Nothing + +observeFunction :: MonadTrav m => FilePath -> [IdentDecl] -> FunDef -> m (Observed, Analysed) +observeFunction unit locals fd@(FunDef (VarDecl self _ fty) body _) = do + key <- case self of + VarName i _ -> funKey unit i + NoName -> return Nothing + fn <- translate unit locals fd + let nodes = solveFunction emptyProgram fn + let retTy = case fty of + FunctionType (FunType rt _ _) _ -> intType rt + _ -> Nothing + perNode <- forM nodes $ \(n, facts, terms) -> do + stores <- foldMapM (store facts) (concatMap subTerms terms) + calls <- foldMapM (call facts) (concatMap subTerms terms) + let returned = case (n, retTy, key) of + (Node _ (StatNode CReturn{}), Just rt, Just k) -> + [Returned k (Just rt, + plain [ c | t <- terms, Just v <- [eval facts t], r <- v, c <- convert (annotation (termExpr t)) rt r ])] + _ -> mempty + return (stores <> calls <> returned) + syntactic <- foldMapM (observeExpr unit) (statExprs body) + inits <- foldMapM localInit [ (i, ni, ini) | CDecl _ ds _ <- localDecls body, (Just (CDeclr (Just i) _ _ _ ni), Just ini@CInitList{}, _) <- ds ] + return (concat perNode ++ syntactic ++ inits ++ map Defined (maybeToList key), (fn, nodes)) + where + localInit (i, ni, ini) = exprType (CVar i ni) >>= maybe (return mempty) (`initializer` ini) + + store facts t = case termKind t of + TAssign _ _ l _ | CMember{} <- termExpr l -> stored (termExpr l) (termTy l) (eval facts t) + TUnary op a | op `elem` [CPreIncOp, CPreDecOp, CPostIncOp, CPostDecOp], CMember{} <- termExpr a -> + let d = if op `elem` [CPreIncOp, CPostIncOp] then 1 else -1 + after = do + ty <- termTy a + v <- eval facts a + return [ c | r <- v, c <- convert (annotation (termExpr t)) ty (Range (lo r + d) (hi r + d) Arith) ] + in stored (termExpr a) (termTy a) after + _ -> return mempty + stored lhs ty value = fieldKey lhs >>= \k -> return $ case (k, value) of + (Just key, Just v) -> [Stored key (ty, plain v)] + (Just key, Nothing) -> [Escaped key] + _ -> mempty + call facts t = case termKind t of + TCall (Term (CVar f _) _ _ _ _) args -> funKey unit f >>= \case + Just k | (unit ++ ":") `isPrefixOf` k -> do + params <- calleeParams f + return $ case params of + Just ps | length ps == length args -> + [Passed k (zipWith (argValue facts) ps args)] + _ -> mempty + _ -> return mempty + _ -> return mempty + argValue facts p a = do + ty <- intType p + v <- eval facts a + return (Just ty, plain [ c | r <- v, c <- convert (annotation (termExpr a)) ty r ]) + calleeParams f = exprType (CVar f undefNode) >>= \case + Just ty | Just (FunType _ ps False) <- funType ty -> return (Just (map declType ps)) + _ -> return Nothing + +-- | What an expression shows, whatever the facts: fields whose address it +-- takes, structs it casts or hands to functions, functions it uses other than +-- by calling them, and what compound literals store. +observeExpr :: MonadTrav m => FilePath -> CExpr -> m Observed +observeExpr unit = go + where + go e = (<>) <$> here e <*> foldMapM go (children e) + + -- A function a call names isn't used other than by calling it. + children = \case + CCall CVar{} args _ -> args + e -> exprChildren e + + here = \case + CUnary CAdrOp e _ -> addressed e + CVar i _ -> map Addressed . maybeToList <$> funKey unit i + CCast d inner _ -> declaredType d >>= \case + -- Only pointer casts can let the program change fields unseen. + to@(Just t) | isJust (pointee t) -> do + from <- exprType inner + return $ map EscapedTag (catMaybes [castTag from to, castTag to from]) + _ -> return mempty + CCall f args _ -> do + callee <- case f of + CVar i _ -> Just <$> (fromMaybe (identToString i) <$> funKey unit i) + _ -> return Nothing + calleeTy <- case f of + CVar i _ -> fmap declType <$> (lookupObject i `catchTravError` const (return Nothing)) + _ -> exprType f + let calleeName = fromMaybe "" callee + sig = calleeTy >>= funType + written <- case sig of + Just (FunType _ params variadic) -> do + let paramTys = map (Just . declType) params ++ repeat Nothing + fmap catMaybes . forM (zip args paramTys) $ \(arg, pty) -> case pty of + -- A parameter's own type says what the callee can write, + -- unless it is a pointer to bytes or to anything. + Just t | Just p <- pointee t, isConst p -> return Nothing + Just t | Just p <- pointee t, isJust (structTag p) -> + return (writableTag t) + Just t | Nothing <- pointee t -> return Nothing + _ | isNothing pty && not variadic -> return Nothing + _ -> (>>= writableTag) <$> exprType arg + _ -> catMaybes . map (>>= writableTag) <$> mapM exprType args + let returned = case sig of + Just (FunType rt _ _) -> catMaybes [returnedTag rt] + _ -> [] + tags = if calleeName `elem` harmless then [] else written ++ returned + return [HandedTo calleeName tags] + CCompoundLit d i ni -> declaredType d >>= maybe (return mempty) (`initializer` CInitList i ni) + _ -> return mempty + + declaredType d = (Just <$> analyseTypeDecl d) `catchTravError` const (return Nothing) + + addressed e = case stripIndex e of + m@CMember{} -> map Escaped . maybeToList <$> fieldKey m + _ -> return mempty + + stripIndex = \case + CIndex b _ _ -> stripIndex b + e -> e + + -- A pointer to a struct cast to a pointer to anything but void or the + -- same struct lets the program change the struct's fields unseen. + castTag from to = do + f <- from >>= pointee + t <- to >>= pointee + tag <- structTag f + if isVoid t || structTag t == Just tag then Nothing else Just tag + + writableTag ty = do + p <- pointee ty + if isConst p then Nothing else structTag p + + returnedTag ty = structTag ty `orElse` (pointee ty >>= structTag) + + orElse (Just x) _ = Just x + orElse Nothing y = y + + pointee ty = case canonicalType ty of + PtrType p _ _ -> Just p + _ -> Nothing + + isConst = constant . typeQuals + + isVoid t = case canonicalType t of + DirectType TyVoid _ _ -> True + _ -> False diff --git a/src/Tokstyle/C/Analysis/Syntax.hs b/src/Tokstyle/C/Analysis/Syntax.hs new file mode 100644 index 0000000..cd23496 --- /dev/null +++ b/src/Tokstyle/C/Analysis/Syntax.hs @@ -0,0 +1,74 @@ +{-# LANGUAGE LambdaCase #-} +-- | The parts of statements and expressions. +module Tokstyle.C.Analysis.Syntax + ( exprChildren + , statExprs + , initExprs + , localDecls + ) where + +import Language.C.Syntax.AST + +exprChildren :: CExpr -> [CExpr] +exprChildren = \case + CComma es _ -> es + CAssign _ l r _ -> [l, r] + CCond c t e _ -> c : maybe [] pure t ++ [e] + CBinary _ l r _ -> [l, r] + CCast _ e _ -> [e] + CUnary _ e _ -> [e] + CIndex b i _ -> [b, i] + CCall f args _ -> f : args + CMember e _ _ _ -> [e] + CSizeofExpr e _ -> [e] + _ -> [] + +-- | Every expression a statement evaluates, including in nested statements. +statExprs :: CStat -> [CExpr] +statExprs = \case + CExpr e _ -> maybe [] pure e + CReturn e _ -> maybe [] pure e + CCompound _ items _ -> concatMap item items + CIf c t e _ -> c : statExprs t ++ maybe [] statExprs e + CSwitch c s _ -> c : statExprs s + CWhile c s _ _ -> c : statExprs s + CFor i c st s _ -> either (maybe [] pure) declExprs i ++ maybe [] pure c ++ maybe [] pure st ++ statExprs s + CLabel _ s _ _ -> statExprs s + CCase e s _ -> e : statExprs s + CCases a b s _ -> a : b : statExprs s + CDefault s _ -> statExprs s + _ -> [] + where + item = \case + CBlockDecl d -> declExprs d + CBlockStmt s -> statExprs s + _ -> [] + +declExprs :: CDecl -> [CExpr] +declExprs = \case + CDecl _ ds _ -> concat [ initExprs ini | (_, Just ini, _) <- ds ] + _ -> [] + +initExprs :: CInit -> [CExpr] +initExprs = \case + CInitExpr e _ -> [e] + CInitList l _ -> concatMap (initExprs . snd) l + +-- | The declarations in a function body, in the order they appear. +localDecls :: CStat -> [CDecl] +localDecls = \case + CCompound _ items _ -> concatMap item items + CIf _ t e _ -> localDecls t ++ maybe [] localDecls e + CSwitch _ s _ -> localDecls s + CWhile _ s _ _ -> localDecls s + CFor i _ _ s _ -> either (const []) pure i ++ localDecls s + CLabel _ s _ _ -> localDecls s + CCase _ s _ -> localDecls s + CCases _ _ s _ -> localDecls s + CDefault s _ -> localDecls s + _ -> [] + where + item = \case + CBlockDecl d -> [d] + CBlockStmt s -> localDecls s + _ -> [] diff --git a/src/Tokstyle/C/Analysis/Types.hs b/src/Tokstyle/C/Analysis/Types.hs new file mode 100644 index 0000000..2cdd53c --- /dev/null +++ b/src/Tokstyle/C/Analysis/Types.hs @@ -0,0 +1,72 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE Strict #-} +-- | The types of expressions, and the names the program knows fields and +-- functions by. +module Tokstyle.C.Analysis.Types + ( FieldKey + , exprType + , structTag + , fieldKey + , funType + , funKey + ) where + +import Language.C.Analysis.AstAnalysis (ExprSide (..), tExpr) +import Language.C.Analysis.SemRep (CompTyKind (..), + CompTypeRef (..), FunType, + Linkage (..), Storage (..), + Type (..), TypeName (..), + declStorage, declType) +import Language.C.Analysis.TravMonad (MonadTrav, catchTravError, + lookupObject) +import Language.C.Analysis.TypeUtils (canonicalType) +import Language.C.Data.Ident (Ident, SUERef (..), + identToString) +import Language.C.Syntax.AST + +-- | A field of a struct: the struct's tag and the field's name. +type FieldKey = (String, String) + +-- | The tag of a struct type. +structTag :: Type -> Maybe String +structTag ty = case canonicalType ty of + DirectType (TyComp (CompTypeRef (NamedRef i) StructTag _)) _ _ -> Just (identToString i) + _ -> Nothing + +-- | The field a member access reads or writes. +fieldKey :: MonadTrav m => CExpr -> m (Maybe FieldKey) +fieldKey = \case + CMember e f isArrow _ -> exprType e >>= \ty -> return $ do + t <- ty + tag <- structTag $ if isArrow then pointee t else t + return (tag, identToString f) + _ -> return Nothing + where + pointee t = case canonicalType t of + PtrType p _ _ -> p + other -> other + +-- | Type of a function, or of what a function pointer points to. +-- 'canonicalType' turns function types into function pointers. +funType :: Type -> Maybe FunType +funType ty = case canonicalType ty of + PtrType (FunctionType ft _) _ _ -> Just ft + FunctionType ft _ -> Just ft + _ -> Nothing + +-- | The name the program knows a function by, which for a static function +-- includes its translation unit. +funKey :: MonadTrav m => FilePath -> Ident -> m (Maybe String) +funKey unit i = (lookupObject i `catchTravError` const (return Nothing)) >>= \case + Just d | Just _ <- funType (declType d) -> + return . Just $ if isInternal (declStorage d) then unit ++ ":" ++ identToString i else identToString i + _ -> return Nothing + where + isInternal = \case + FunLinkage InternalLinkage -> True + Static InternalLinkage _ -> True + _ -> False + +-- | The type of an expression, if it has one. +exprType :: MonadTrav m => CExpr -> m (Maybe Type) +exprType e = (Just <$> tExpr [] RValue e) `catchTravError` const (return Nothing) diff --git a/src/Tokstyle/C/Env.hs b/src/Tokstyle/C/Env.hs index 66dbc10..064dcb7 100644 --- a/src/Tokstyle/C/Env.hs +++ b/src/Tokstyle/C/Env.hs @@ -23,7 +23,7 @@ module Tokstyle.C.Env import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Text (Text) -import Language.C.Analysis.SemRep (GlobalDecls, Type) +import Language.C.Analysis.SemRep (GlobalDecls, IdentDecl, Type) import Language.C.Analysis.TravMonad (Trav, getUserState, modifyUserState) import Language.C.Data.Ident (Ident, SUERef) @@ -36,6 +36,8 @@ import Language.Cimple.Diagnostics (Diagnostic (..), import Prettyprinter (Doc) import Prettyprinter.Render.Terminal (AnsiStyle) +import Tokstyle.C.Analysis.Interval (Program, emptyProgram) +import Tokstyle.C.Analysis.Program (Analysed) import Tokstyle.C.TravUtils (getJust) newtype CPosition = CPosition { unCPosition :: Position } @@ -58,10 +60,21 @@ data Env = Env , globalDecls :: Maybe GlobalDecls , linterErrors :: [LinterError] , currentFlag :: Maybe Text + , program :: Program + -- ^ What is known about the program the translation unit is part of. + , localsOf :: Map String [IdentDecl] + -- ^ The locals each function declares, as analysing the translation unit + -- found them. + , pendingLocals :: [IdentDecl] + -- ^ The locals of the function being analysed, in reverse. + , analysed :: [Analysed] + -- ^ The functions of the translation unit that can wrap around, analysed + -- knowing nothing about the rest of the program. } defaultEnv :: Env -defaultEnv = Env ["file"] Nothing [] Map.empty Map.empty Nothing [] Nothing +defaultEnv = Env ["file"] Nothing [] Map.empty Map.empty Nothing [] Nothing emptyProgram Map.empty [] [] + bracketUserState :: (Env -> Env) -> Trav Env a -> Trav Env a bracketUserState f act = do diff --git a/src/Tokstyle/C/Linter.hs b/src/Tokstyle/C/Linter.hs index 59da6bc..be80ac1 100644 --- a/src/Tokstyle/C/Linter.hs +++ b/src/Tokstyle/C/Linter.hs @@ -1,6 +1,8 @@ +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} module Tokstyle.C.Linter ( analyse + , analyseProgram , analyseText , allWarnings , markdown @@ -13,7 +15,9 @@ module Tokstyle.C.Linter , diagToText ) where +import Control.Parallel.Strategies (parMap, rpar) import qualified Data.ByteString as BS +import Data.Functor.Identity (Identity, runIdentity) import Data.List (sortBy) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map @@ -21,13 +25,20 @@ import Data.Text (Text) import qualified Data.Text as Text import qualified Data.Text.Encoding as Text import Language.C.Analysis.AstAnalysis (analyseAST) -import Language.C.Analysis.SemRep (GlobalDecls) +import Language.C.Analysis.SemRep (DeclEvent (..), + FunDef (..), GlobalDecls, + IdentDecl (..), + VarDecl (..), + VarName (..)) import Language.C.Analysis.TravMonad (CLanguage (..), Trav, TravOptions (..), - modifyOptions, + TravState, modifyOptions, modifyUserState, runTrav, - userState) + runTravTWithTravState, + userState, + withExtDeclHandler) import Language.C.Data.Error (CError, errorPos) +import Language.C.Data.Ident (identToString) import Language.C.Data.Position (isSourcePos) import qualified Language.C.Data.Position as C import Language.C.Syntax.AST (CTranslUnit) @@ -36,6 +47,9 @@ import Language.Cimple.Diagnostics (Diagnostic (..), IsPosition (..), diagToText) import qualified Language.Cimple.Diagnostics as Diagnostics +import Tokstyle.C.Analysis.Interval (Program, emptyProgram) +import Tokstyle.C.Analysis.Program (Analysed, Observed, + observe, programFrom) import Prettyprinter (Doc, pretty) import Prettyprinter.Render.Terminal (AnsiStyle) @@ -59,6 +73,7 @@ import qualified Tokstyle.C.Linter.SizeArg as SizeArg (descr) import qualified Tokstyle.C.Linter.Sizeof as Sizeof (descr) import qualified Tokstyle.C.Linter.StrictTypedef as StrictTypedef (descr) import qualified Tokstyle.C.Linter.VoidCall as VoidCall (descr) +import qualified Tokstyle.C.Linter.Wraparound as Wraparound (descr) type Linter = (GlobalDecls -> Trav Env (), (Text, Text)) @@ -79,6 +94,7 @@ linters = , Sizeof.descr , StrictTypedef.descr , VoidCall.descr + , Wraparound.descr ] @@ -92,20 +108,62 @@ runLinters flags tu = analyse :: [Text] -> CTranslUnit -> [LinterError] -analyse enabled tu = - case analysis of +analyse enabled tu = concat $ analyseProgram enabled [("test.c", tu)] + + +-- | The errors in each translation unit of a program. +analyseProgram :: [Text] -> [(FilePath, CTranslUnit)] -> [[LinterError]] +analyseProgram enabled units = parMap rpar check (zip analysed observed) + where + analysed = parMap rpar (\(file, tu) -> (file, analyseUnit tu)) units + + observed + | "wraparound" `elem` enabled = parMap rpar observeUnit analysed + | otherwise = map (const ([], [])) analysed + prog = programFrom (concatMap fst observed) + + check ((_, Left errs), _) = map toLinterError errs + check ((_, Right (decls, st)), (_, fns)) = case resume st prog fns (runLinters enabled decls) of Left errs -> map toLinterError errs Right (_, state) -> reverse . linterErrors $ userState state - where - analysis = runTrav defaultEnv $ do - modifyOptions (\opts -> opts { language = GNU99 }) - decls <- analyseAST tu - runLinters enabled decls toLinterError :: CError -> LinterError toLinterError err = Diagnostic (Env.CPosition (errorPos err)) 1 ErrorLevel (pretty (show err)) Nothing [] [] +-- | The declarations of a translation unit, with the state of their analysis +-- to go on from. +analyseUnit :: CTranslUnit -> Either [CError] (GlobalDecls, TravState Identity Env) +analyseUnit tu = runTrav defaultEnv $ do + modifyOptions (\opts -> opts { language = GNU99 }) + analyseAST tu `withExtDeclHandler` recordLocals + +-- | Remembers the locals each function declares, which language-c forgets +-- once it leaves the function. +recordLocals :: DeclEvent -> Trav Env () +recordLocals = \case + LocalEvent d -> modifyUserState $ \env -> env{Env.pendingLocals = d : Env.pendingLocals env} + DeclEvent (FunctionDef (FunDef (VarDecl (VarName i _) _ _) _ _)) -> modifyUserState $ \env -> env + { Env.localsOf = Map.insert (identToString i) (reverse (Env.pendingLocals env)) (Env.localsOf env) + , Env.pendingLocals = [] + } + _ -> return () + +-- | Goes on analysing a translation unit, knowing what is known about the +-- program, and with its functions analysed knowing nothing about it. +resume :: TravState Identity Env -> Program -> [Analysed] -> Trav Env a -> Either [CError] (a, TravState Identity Env) +resume st p fns act = runIdentity . runTravTWithTravState st $ do + modifyUserState $ \env -> env{Env.program = p, Env.analysed = fns} + act + +-- | 'observe' run on a translation unit, knowing nothing about the rest of the +-- program. +observeUnit :: (FilePath, Either [CError] (GlobalDecls, TravState Identity Env)) -> (Observed, [Analysed]) +observeUnit = \case + (file, Right (decls, st)) | Right (o, _) <- resume st emptyProgram [] (observe file (Env.localsOf (userState st)) decls) -> o + _ -> ([], []) + + analyseText :: [Text] -> CTranslUnit -> [Text] analyseText enabled tu = map diagToText (analyse enabled tu) diff --git a/src/Tokstyle/C/Linter/Wraparound.hs b/src/Tokstyle/C/Linter/Wraparound.hs new file mode 100644 index 0000000..d8def25 --- /dev/null +++ b/src/Tokstyle/C/Linter/Wraparound.hs @@ -0,0 +1,166 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE Strict #-} +module Tokstyle.C.Linter.Wraparound (descr) where + +import Control.Monad (forM_) +import Data.Text (Text) +import qualified Data.Text as Text +import Language.C.Analysis.SemRep (GlobalDecls) +import Language.C.Analysis.TravMonad (Trav, getUserState) +import Language.C.Data.Node (NodeInfo, posOfNode) +import Language.C.Data.Position (isSourcePos) +import qualified Language.C.Pretty as C +import Language.C.Syntax.AST (CAssignOp (..), CBinaryOp (..), + CExpr, annotation) +import Language.Cimple.Diagnostics (DiagnosticSpan (..)) +import Prettyprinter (Doc, pretty, (<+>)) +import Prettyprinter.Render.Terminal (AnsiStyle) +import Tokstyle.C.Analysis.Interval (Facts, IntTy (..), Origin (..), + Range (..), Term (..), + TermKind (..), dependsOn, eval, + solveFunction, subTerms) +import Tokstyle.C.Env (DiagnosticLevel (..), Env (..), + posAndLen, recordLinterError, + recordRichError) +import Tokstyle.C.TravUtils (backticks) + + +isComparison :: CBinaryOp -> Bool +isComparison = (`elem` [CEqOp, CNeqOp, CLeOp, CGrOp, CLeqOp, CGeqOp]) + +compareWith :: CBinaryOp -> Integer -> Integer -> Bool +compareWith = \case + CEqOp -> (==) + CNeqOp -> (/=) + CLeOp -> (<) + CGrOp -> (>) + CLeqOp -> (<=) + _ -> (>=) + +flipOp :: CBinaryOp -> CBinaryOp +flipOp = \case + CLeOp -> CGrOp + CGrOp -> CLeOp + CLeqOp -> CGeqOp + CGeqOp -> CLeqOp + op -> op + +exprDoc :: CExpr -> Doc a +exprDoc = backticks . pretty . show . C.pretty + +valuesDoc :: Range -> Doc a +valuesDoc (Range l h _) + | l == h = pretty l + | otherwise = "values from" <+> pretty l <+> "to" <+> pretty h + +-- | The values that wrapped around, with the expression where they did. +wrappedIn :: Facts -> Term -> [(Range, NodeInfo)] +wrappedIn facts t = [ (r, site) | Just rs <- [eval facts t], r@(Range _ _ (Wrapped site)) <- rs ] + +-- | Records an error at a term, pointing at where its value wrapped around if +-- that was elsewhere. +recordWrap :: Term -> NodeInfo -> Doc AnsiStyle -> Trav Env () +recordWrap t site msg = recordRichError ni ErrorLevel msg spans [] + where + ni = annotation (termExpr t) + spans = + [ DiagnosticSpan pos len ["wraps around here"] + | posOfNode site /= posOfNode ni, isSourcePos (posOfNode site) + , let (pos, len) = posAndLen site ] + +-- | 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 op wrapping other = case eval facts other of + Just os@(_ : _) | all ((== Reduced) . origin) os -> do + let oLo = minimum (map lo os) + oHi = maximum (map hi os) + case [ (w, site) | (w, site) <- wrappedIn facts wrapping, hi w < oLo || lo w > oHi ] of + (w, site) : _ -> recordWrap wrapping site $ + exprDoc (termExpr wrapping) <+> "can wrap around to" <+> valuesDoc w + <> ", but" <+> exprDoc (termExpr other) <+> "is always between" + <+> pretty oLo <+> "and" <+> pretty oHi + <> ", so the comparison is always" + <+> (if compareWith op (lo w) oLo then "true" else "false") + <+> "when it wraps" + [] -> return () + _ -> 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 a b = case (eval facts b, termTy a, wrappedIn facts a) of + (Just [Range n n' _], Just ty, (w, site) : _) | n == n', n > 0, (2 ^ tyBits ty) `mod` n /= 0 -> + recordWrap a site $ + exprDoc (termExpr a) <+> "can wrap around to" <+> valuesDoc w + <> ", and" <+> pretty (2 ^ tyBits ty :: Integer) <+> "is not a multiple of" + <+> pretty n <> ", so" <+> backticks ("%" <+> pretty n) + <+> "then gives a different index than it would without the wrap" + _ -> 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 arr i len = + case [ (w, site) | (w, site) <- wrappedIn facts i, hi w >= len ] of + (w, site) : _ -> recordWrap i site $ + exprDoc (termExpr i) <+> "can wrap around to" <+> valuesDoc w + <> ", past the end of" <+> exprDoc (termExpr arr) + <> ", which has" <+> pretty len <+> "elements" + [] -> 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 converted inner = case (termTy converted, termKind inner, termTy inner) of + (Just IntTy{tySigned = False, tyBits = bits}, TBin CSubOp x y, Just IntTy{tySigned = True}) + | Just w <- narrowest [x, y], w < bits + , (r, _) : _ <- wrappedIn facts converted -> + recordLinterError (annotation (termExpr inner)) $ + exprDoc (termExpr inner) <+> "can wrap around to" <+> valuesDoc r + <> ", because it is the difference of" <+> pretty w <> "-bit values but wraps around at" + <+> pretty bits <+> "bits here" + _ -> return () + where + narrowest ts = maximum <$> mapM width ts + width t = case (termKind t, termTy t) of + (TConst _, _) -> Nothing + (_, Just IntTy{tySigned = False, tyBits = b}) -> Just b + _ -> Nothing + +checkTerm :: Facts -> Term -> Trav Env () +checkTerm facts t = case termKind t of + TBin op l r | isComparison op -> do + checkComparison facts op l r + checkComparison facts (flipOp op) r l + TBin CRmdOp a b -> checkRemainder facts a b + TIndex arr i (Just len) -> checkIndex facts arr i len + TCast a -> checkPromoted facts t a + TAssign _ CAssignOp _ r -> checkPromoted facts t r + _ -> return () + +analyse :: GlobalDecls -> Trav Env () +analyse _ = do + env <- getUserState + forM_ (analysed env) $ \(fn, known) -> do + let nodes = if dependsOn (program env) fn then solveFunction (program env) fn else known + forM_ nodes $ \(_, facts, terms) -> mapM_ (checkTerm facts) (concatMap subTerms terms) + + +descr :: (GlobalDecls -> Trav Env (), (Text, Text)) +descr = (analyse, ("wraparound", Text.unlines + [ "Checks for integer arithmetic that wraps around where it is used as an index:" + , "compared to an index reduced with `%` or `&`, reduced with `%` by a size that" + , "doesn't divide the type's range, or used to index an array it can be past the" + , "end of. Also checks for the difference of two 16-bit values that wraps around" + , "at 32 bits because integer promotion computes it in `int`." + , "" + , "The checks follow values through locals and fields, take the conditions that" + , "guard them into account, and know which values the program stores in struct" + , "fields, returns from functions, and passes to static functions." + , "" + , "**Reason:** in a ring buffer of size `N`, `(uint16_t)(start - 1)` wraps to" + , "65535 when `start` is 0, not to `N - 1`. Comparing it to `id % N` then never" + , "matches. Use `(start + N - 1) % N` instead." + ])) diff --git a/test/Tokstyle/C/Linter/WraparoundSpec.hs b/test/Tokstyle/C/Linter/WraparoundSpec.hs new file mode 100644 index 0000000..d16b7be --- /dev/null +++ b/test/Tokstyle/C/Linter/WraparoundSpec.hs @@ -0,0 +1,358 @@ +{-# LANGUAGE OverloadedStrings #-} +module Tokstyle.C.Linter.WraparoundSpec (spec) where +import Data.Text (Text) +import Test.Hspec (Spec, it) + +import Tokstyle.C.LinterSpec (shouldAccept, shouldWarn) + + +shouldWarn' :: [Text] -> [[Text]] -> IO () +shouldWarn' = shouldWarn ["wraparound"] + + +shouldAccept' :: [Text] -> IO () +shouldAccept' = shouldAccept ["wraparound"] + + +prelude :: [Text] +prelude = + [ "typedef unsigned char uint8_t;" + , "typedef unsigned short uint16_t;" + , "typedef unsigned int uint32_t;" + , "typedef struct Conn { uint16_t start; uint32_t id; uint8_t slots[2048]; } Conn;" + ] + + +spec :: Spec +spec = do + it "warns about a ring index decremented modulo the wrong size" $ do + shouldWarn' (prelude ++ + [ "int full(const Conn *c) {" + , " return (c->id % 2048) == (uint16_t)(c->start - 1);" + , "}" + ]) + [[ "error: `(uint16_t) (c->start - 1)` can wrap around to 65535, but `c->id % 2048` is always between 0 and 2047, so the comparison is always false when it wraps [-Wwraparound]" + , " --> test.c:6:28" + , " |" + , " 6| return (c->id % 2048) == (uint16_t)(c->start - 1);" + , " | ^^^^^^^^^^^^^^^^^^^^^^^^" + ]] + + it "warns about unsigned subtraction without a cast" $ do + shouldWarn' (prelude ++ + [ "int full(uint32_t id, uint32_t start) {" + , " return start - 1 != id % 2048;" + , "}" + ]) + [[ "error: `start - 1` can wrap around to 4294967295, but `id % 2048` is always between 0 and 2047, so the comparison is always true when it wraps [-Wwraparound]" + , " --> test.c:6:10" + , " |" + , " 6| return start - 1 != id % 2048;" + , " | ^^^^^^^^^" + ]] + + it "follows wrapped values through locals" $ do + shouldWarn' (prelude ++ + [ "int full(const Conn *c) {" + , " const uint16_t prev = c->start - 1;" + , " const uint32_t idx = c->id % 2048;" + , " return idx == prev;" + , "}" + ]) + [[ "error: `prev` can wrap around to 65535, but `idx` is always between 0 and 2047, so the comparison is always false when it wraps [-Wwraparound]" + , " --> test.c:8:17" + , " |" + , " 6| const uint16_t prev = c->start - 1;" + , " | ^^^^^^^^^^^^" + , " | |" + , " | wraps around here" + , " 8| return idx == prev;" + , " | ^^^^" + ]] + + it "warns about a wrapped value reduced modulo a size that doesn't divide its range" $ do + shouldWarn' (prelude ++ + [ "int used(const uint8_t *relays, uint16_t counter) {" + , " int n = 0;" + , " for (unsigned i = 0; i < 24; ++i) {" + , " n += relays[(counter - (i + 1)) % (6 * 4)];" + , " }" + , " return n;" + , "}" + ]) + [[ "error: `counter - (i + 1)` can wrap around to values from 4294967272 to 4294967295, and 4294967296 is not a multiple of 24, so `% 24` then gives a different index than it would without the wrap [-Wwraparound]" + , " --> test.c:8:18" + , " |" + , " 8| n += relays[(counter - (i + 1)) % (6 * 4)];" + , " | ^^^^^^^^^^^^^^^^^" + ]] + + it "warns about a wrapped index past the end of an array" $ do + shouldWarn' (prelude ++ + [ "uint8_t last(const Conn *c) {" + , " return c->slots[(uint16_t)(c->start - 1)];" + , "}" + ]) + [[ "error: `(uint16_t) (c->start - 1)` can wrap around to 65535, past the end of `c->slots`, which has 2048 elements [-Wwraparound]" + , " --> test.c:6:19" + , " |" + , " 6| return c->slots[(uint16_t)(c->start - 1)];" + , " | ^^^^^^^^^^^^^^^^^^^^^^^^" + ]] + + it "forgets facts about fields when a call can change them" $ do + shouldWarn' (prelude ++ + [ "void reset(Conn *c);" + , "int full(Conn *c) {" + , " if (c->start == 0) {" + , " return 0;" + , " }" + , " reset(c);" + , " return (c->id % 2048) == (uint16_t)(c->start - 1);" + , "}" + ]) + [[ "error: `(uint16_t) (c->start - 1)` can wrap around to 65535, but `c->id % 2048` is always between 0 and 2047, so the comparison is always false when it wraps [-Wwraparound]" + , " --> test.c:11:28" + , " |" + , " 11| return (c->id % 2048) == (uint16_t)(c->start - 1);" + , " | ^^^^^^^^^^^^^^^^^^^^^^^^" + ]] + + it "doesn't assume a static local still has its initial value" $ do + shouldWarn' (prelude ++ + [ "int full(const Conn *c) {" + , " static uint16_t start = 1;" + , " const int r = (c->id % 2048) == (uint16_t)(start - 1);" + , " start = c->start;" + , " return r;" + , "}" + ]) + [[ "error: `(uint16_t) (start - 1)` can wrap around to 65535, but `c->id % 2048` is always between 0 and 2047, so the comparison is always false when it wraps [-Wwraparound]" + , " --> test.c:7:35" + , " |" + , " 7| const int r = (c->id % 2048) == (uint16_t)(start - 1);" + , " | ^^^^^^^^^^^^^^^^^^^^^" + ]] + + it "warns about the difference of 16-bit values wrapping around at 32 bits" $ do + shouldWarn' (prelude ++ + [ "int late(uint16_t seq, uint16_t bottom, uint32_t size) {" + , " return (uint32_t)(seq - bottom) > size;" + , "}" + ]) + [[ "error: `seq - bottom` can wrap around to values from 4294901761 to 4294967295, because it is the difference of 16-bit values but wraps around at 32 bits here [-Wwraparound]" + , " --> test.c:6:21" + , " |" + , " 6| return (uint32_t)(seq - bottom) > size;" + , " | ^^^^^^^^^^^^" + ]] + + it "accepts the difference of 16-bit values wrapping around at 16 bits" $ do + shouldAccept' (prelude ++ + [ "int late(uint16_t seq, uint16_t bottom, uint32_t size) {" + , " return (uint16_t)(seq - bottom) > size;" + , "}" + ]) + + it "knows a field holds an index another function reduces" $ do + shouldWarn' (prelude ++ + [ "void advance(Conn *c) {" + , " c->start = (c->start + 1) % 2048;" + , "}" + , "int full(const Conn *c, uint16_t id) {" + , " return c->start == (uint16_t)(id - 1);" + , "}" + ]) + [[ "error: `(uint16_t) (id - 1)` can wrap around to 65535, but `c->start` is always between 0 and 2047, so the comparison is always false when it wraps [-Wwraparound]" + , " --> test.c:9:22" + , " |" + , " 9| return c->start == (uint16_t)(id - 1);" + , " | ^^^^^^^^^^^^^^^^^^" + ]] + + it "forgets what a field holds once its address escapes" $ do + shouldAccept' (prelude ++ + [ "void load(uint16_t *value);" + , "void advance(Conn *c) {" + , " c->start = (c->start + 1) % 2048;" + , " load(&c->start);" + , "}" + , "int full(const Conn *c, uint16_t id) {" + , " return c->start == (uint16_t)(id - 1);" + , "}" + ]) + + it "forgets what a struct's fields hold once a function it doesn't see can write them" $ do + shouldAccept' (prelude ++ + [ "void load(Conn *c);" + , "void advance(Conn *c) {" + , " c->start = (c->start + 1) % 2048;" + , " load(c);" + , "}" + , "int full(const Conn *c, uint16_t id) {" + , " return c->start == (uint16_t)(id - 1);" + , "}" + ]) + + it "knows what a function returns" $ do + shouldWarn' (prelude ++ + [ "static uint16_t index_of(uint32_t id) {" + , " return id % 2048;" + , "}" + , "int full(uint32_t id, uint16_t start) {" + , " return index_of(id) == (uint16_t)(start - 1);" + , "}" + ]) + [[ "error: `(uint16_t) (start - 1)` can wrap around to 65535, but `index_of(id)` is always between 0 and 2047, so the comparison is always false when it wraps [-Wwraparound]" + , " --> test.c:9:26" + , " |" + , " 9| return index_of(id) == (uint16_t)(start - 1);" + , " | ^^^^^^^^^^^^^^^^^^^^^" + ]] + + it "knows what a static function's callers pass" $ do + shouldAccept' (prelude ++ + [ "static uint8_t before(const Conn *c, uint16_t i) {" + , " return c->slots[(uint16_t)(i - 1)];" + , "}" + , "uint8_t first(const Conn *c) {" + , " return before(c, 1);" + , "}" + ]) + + it "doesn't assume what callers pass to a function whose address escapes" $ do + shouldWarn' (prelude ++ + [ "static uint8_t before(const Conn *c, uint16_t i) {" + , " return c->slots[(uint16_t)(i - 1)];" + , "}" + , "uint8_t (*const get)(const Conn *c, uint16_t i) = before;" + , "uint8_t first(const Conn *c) {" + , " return before(c, 1);" + , "}" + ]) + [[ "error: `(uint16_t) (i - 1)` can wrap around to 65535, past the end of `c->slots`, which has 2048 elements [-Wwraparound]" + , " --> test.c:6:19" + , " |" + , " 6| return c->slots[(uint16_t)(i - 1)];" + , " | ^^^^^^^^^^^^^^^^^" + ]] + + it "knows a difference can't wrap after a guard relating its operands" $ do + shouldAccept' (prelude ++ + [ "uint8_t rest(const Conn *c, uint16_t size, uint16_t offset) {" + , " if (size < offset) {" + , " return 0;" + , " }" + , " return c->slots[(uint16_t)(size - offset)];" + , "}" + ]) + + it "knows a loop bound is past the index" $ do + shouldAccept' (prelude ++ + [ "uint8_t last(const Conn *c, uint16_t count) {" + , " uint8_t x = 0;" + , " for (uint16_t i = 0; i < count; ++i) {" + , " x = c->slots[(uint16_t)(count - i - 1)];" + , " }" + , " return x;" + , "}" + ]) + + it "forgets how paths relate after writing one of them" $ do + shouldWarn' (prelude ++ + [ "uint8_t rest(const Conn *c, uint16_t size, uint16_t offset, uint16_t other) {" + , " if (size < offset) {" + , " return 0;" + , " }" + , " offset = other;" + , " return c->slots[(uint16_t)(size - offset)];" + , "}" + ]) + [[ "error: `(uint16_t) (size - offset)` can wrap around to values from 1 to 65535, past the end of `c->slots`, which has 2048 elements [-Wwraparound]" + , " --> test.c:10:19" + , " |" + , " 10| return c->slots[(uint16_t)(size - offset)];" + , " | ^^^^^^^^^^^^^^^^^^^^^^^^^" + ]] + + it "accepts a decrement modulo the ring size" $ do + shouldAccept' (prelude ++ + [ "int full(const Conn *c) {" + , " return (c->id % 2048) == (c->start + 2048 - 1) % 2048;" + , "}" + ]) + + it "accepts a wrapped value reduced modulo a divisor of its range" $ do + shouldAccept' (prelude ++ + [ "int full(const Conn *c) {" + , " return (c->id % 2048) == (uint16_t)(c->start - 1) % 2048;" + , "}" + ]) + + it "accepts a decrement guarded against wrapping" $ do + shouldAccept' (prelude ++ + [ "int full(const Conn *c) {" + , " if (c->start == 0) {" + , " return 0;" + , " }" + , " return (c->id % 2048) == (uint16_t)(c->start - 1);" + , "}" + ]) + + it "accepts a decrement in a switch case that excludes wrapping" $ do + shouldAccept' (prelude ++ + [ "int full(const Conn *c) {" + , " switch (c->start) {" + , " case 0:" + , " return 0;" + , " default:" + , " return (c->id % 2048) == (uint16_t)(c->start - 1);" + , " }" + , "}" + ]) + + it "accepts a decrement in a loop that stops before wrapping" $ do + shouldAccept' (prelude ++ + [ "int find(const Conn *c, uint32_t n) {" + , " while (n > 0) {" + , " if ((c->id % 2048) == n - 1) {" + , " return 1;" + , " }" + , " --n;" + , " }" + , " return 0;" + , "}" + ]) + + it "checks the first iteration of a do-while loop before its condition" $ do + shouldWarn' (prelude ++ + [ "int find(const Conn *c, uint32_t n) {" + , " do {" + , " if ((c->id % 2048) == n - 1) {" + , " return 1;" + , " }" + , " } while (--n > 0);" + , " return 0;" + , "}" + ]) + [[ "error: `n - 1` can wrap around to 4294967295, but `c->id % 2048` is always between 0 and 2047, so the comparison is always false when it wraps [-Wwraparound]" + , " --> test.c:7:27" + , " |" + , " 7| if ((c->id % 2048) == n - 1) {" + , " | ^^^^^" + ]] + + it "accepts the unsigned range check idiom" $ do + shouldAccept' (prelude ++ + [ "extern const uint16_t UINT16_MAX;" + , "int fits(uint32_t length) {" + , " return length - 1 < UINT16_MAX;" + , "}" + ]) + + it "accepts comparisons where the other side can have any value" $ do + shouldAccept' (prelude ++ + [ "int next(uint16_t a, uint16_t b) {" + , " return a == (uint16_t)(b - 1);" + , "}" + ]) diff --git a/tokstyle.cabal b/tokstyle.cabal index 74bf23e..a208b94 100644 --- a/tokstyle.cabal +++ b/tokstyle.cabal @@ -25,6 +25,10 @@ library Tokstyle.Analysis.Dataflow Tokstyle.Analysis.Symbolic Tokstyle.C.Analysis.CFG + Tokstyle.C.Analysis.Interval + Tokstyle.C.Analysis.Program + Tokstyle.C.Analysis.Syntax + Tokstyle.C.Analysis.Types Tokstyle.C.Analysis.Liveness Tokstyle.Cimple.Analysis.CFG Tokstyle.Cimple.Analysis.Liveness @@ -42,6 +46,7 @@ library Tokstyle.C.Linter.Sizeof Tokstyle.C.Linter.StrictTypedef Tokstyle.C.Linter.VoidCall + Tokstyle.C.Linter.Wraparound Tokstyle.C.Patterns Tokstyle.C.TravUtils Tokstyle.C.TraverseAst @@ -193,6 +198,7 @@ test-suite testsuite Tokstyle.C.Linter.SizeofSpec Tokstyle.C.Linter.StrictTypedefSpec Tokstyle.C.Linter.VoidCallSpec + Tokstyle.C.Linter.WraparoundSpec Tokstyle.C.LinterSpec Tokstyle.Linter.AssertSpec Tokstyle.Linter.BooleanReturnSpec diff --git a/tools/check-c.hs b/tools/check-c.hs index cef53c1..aa34a83 100644 --- a/tools/check-c.hs +++ b/tools/check-c.hs @@ -4,11 +4,13 @@ module Main (main) where import Control.Monad (unless) import qualified Control.Monad.Parallel as Par +import Data.Either (lefts, rights) import Data.List (isPrefixOf, isSuffixOf) import Data.Text (Text) import qualified Data.Text as Text import qualified Data.Text.IO as Text -import Language.C (parseCFile, parseCFilePre) +import Language.C (CTranslUnit, parseCFile, + parseCFilePre) import Language.C.System.GCC (newGCC) import Options.Applicative import Prettyprinter (Doc, defaultLayoutOptions, @@ -18,7 +20,7 @@ import System.Exit (ExitCode (..), exitWith) import System.IO (hSetEncoding, stderr, stdout, utf8) import qualified Tokstyle.C.Linter as Linter -import Tokstyle.C.Linter (allWarnings, analyse) +import Tokstyle.C.Linter (allWarnings, analyseProgram) data Options = Options @@ -63,18 +65,14 @@ defaultCppOpts sysInclude = ] -processFile :: String -> String -> [Text] -> [String] -> FilePath -> IO (Bool, [Doc AnsiStyle]) -processFile cc sysInclude flags cppOpts file = do +parseFile :: String -> String -> [String] -> FilePath -> IO (Either (Doc AnsiStyle) (FilePath, CTranslUnit)) +parseFile cc sysInclude cppOpts file = do result <- if ".i" `isSuffixOf` file then parseCFilePre file else parseCFile (newGCC cc) Nothing (defaultCppOpts sysInclude ++ cppOpts) file - case result of - Left err -> return (False, [pretty file <> ": Parse Error: " <> pretty (show err)]) - Right tu -> do - errs <- Linter.renderIO $ analyse flags tu - case errs of - [] -> return (True, []) - _ -> return (False, errs) + return $ case result of + Left err -> Left (pretty file <> ": Parse Error: " <> pretty (show err)) + Right tu -> Right (file, tu) main :: IO () @@ -85,8 +83,10 @@ main = do if optMarkdown opts then Text.putStr Linter.markdown else do - result <- Par.mapM (processFile (optCC opts) (optInclude opts) (optWarnings opts) (optCppOptions opts)) (optFiles opts) - mapM_ (mapM_ render . snd) result - unless (all fst result) $ exitWith (ExitFailure 1) + parsed <- Par.mapM (parseFile (optCC opts) (optInclude opts) (optCppOptions opts)) (optFiles opts) + let parseErrors = lefts parsed + errs <- concat <$> mapM Linter.renderIO (analyseProgram (optWarnings opts) (rights parsed)) + mapM_ render (parseErrors ++ errs) + unless (null parseErrors && null errs) $ exitWith (ExitFailure 1) where render doc = renderIO stderr (layoutSmart defaultLayoutOptions doc) >> Text.hPutStrLn stderr ""