Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
branch: master
Fetching contributors…

Cannot retrieve contributors at this time

1204 lines (1105 sloc) 50.999 kB
-- Checking the AST, with appropriate handling.
-- Author: Ben Blum <bblum@andrew.cmu.edu>
{-# LANGUAGE ExistentialQuantification #-}
module Check where
import Control.Applicative ((<$>))
import Control.Monad.State
import qualified Data.Traversable as T (sequence,mapM)
import qualified Data.Map as Map
import Data.List (intercalate)
import qualified Data.Foldable as F (any)
import Data.Maybe (mapMaybe,catMaybes,fromMaybe,isNothing,fromJust)
import Data.Either (partitionEithers)
import Language.C.Data.Ident (Ident,builtinIdent,identToString)
import Language.C.Data.Node (NodeInfo,fileOfNode,posOfNode)
import Language.C.Data.Position (posRow) -- ,posColumn)
import Language.C.Syntax.AST
import Debug.Trace
import Rules
import Attributes
import Constraints
data TypeName = VarName Ident | StructName Ident | TypedefName Ident
deriving (Show,Eq,Ord)
data Type = Base
-- [Type]: arguments; Type: return type; Bool: isVariadic
| Arrow [Type] Type Bool (Either Annotation Unknown)
| Pointer Type
| Struct (Maybe Ident) (Map.Map Ident Type)
| IncompleteStruct Ident
deriving Eq
-- TODO: data Message
data MessageLine a = (Show a) => M String a
-- Symbolic context. The context at any point in the code flow may not
-- necessarily be known concretely, if (a) a fn with unknown Effect was called
-- previously, or (b) the current function's Rule is unknown, or of course both.
type SContext = (R, [E])
data Checker = Checker {
-- The current context of the code. If the list of EVs is empty, the
-- current context is known for sure. Otherwise, generate constraints.
context :: SContext,
-- identifier mappings
types :: Map.Map TypeName Type,
-- output
msgs :: [String],
-- value is "Left gs" if the label hasn't been hit yet (a list of all
-- contexts that the label is entered with), and "Right g" if it has (the
-- context that was decided upon for its entry, for future backwards gotos)
labels :: Map.Map Ident (Either [SContext] SContext),
-- break and continue targets. these represent the contexts encountered at
-- each break and continue statement, to be collected by the call at the
-- construct they belong to.
breaks :: [[SContext]],
continues :: [[SContext]],
-- The end contexts for all the case branches in a switch statement.
branches :: [[SContext]],
-- 'Return' tracking.
returned :: [[Bool]],
ends :: [[SContext]],
-- Constraint tracking.
constraints :: [Constraint], -- TODO: In this list, track "if fail" error msgs
nextRV :: Int, nextEV :: Int
}
builtinTypes = Map.fromList
[(TypedefName $ builtinIdent "__builtin_va_list", Base)]
defaultChecker = Checker undefined builtinTypes [] Map.empty [] [] [] [] [] [] 0 0
--
-- Instants.
--
instance Show Type where
show Base = "T"
show (Arrow args ret isVariadic a') =
let argstrs = map show args ++ (if isVariadic then ["..."] else [])
argstr = case args of [] -> "unit"
_ -> intercalate ", " argstrs
in "(" ++ argstr ++ " -> " ++ show ret
++ " {" ++ either show show a' ++ "})"
show (Pointer t) = show t ++ "*"
show (Struct (Just name) contence) =
"struct " ++ show name ++ " {" ++ show contence ++ "}"
show (Struct Nothing contence) = "struct {" ++ show contence ++ "}"
show (IncompleteStruct name) = "struct " ++ show name
instance Show (MessageLine a) where
show (M str a) = str ++ " \t" ++ show a
--
-- Flow control helpers.
--
enterLoop :: State Checker ()
enterLoop =
modify (\s -> s { breaks = []:(breaks s), continues = []:(continues s) })
-- Returns the broken contexts and the continued contexts, respectively.
exitLoop :: State Checker ([SContext], [SContext])
exitLoop =
do bs <- breaks <$> get
cs <- continues <$> get
case (bs,cs) of
(b:bs', c:cs') ->
do modify (\s -> s { breaks = bs', continues = cs' })
return (b,c)
_ -> error "inconsistent break/continue stack exiting loop"
breakLoop :: State Checker ()
breakLoop =
do g <- getContext
bs <- breaks <$> get
case bs of
(b:bs') -> modify (\s -> s { breaks = (g:b):bs' })
[] -> error "inconsistent break stack in break"
continueLoop :: State Checker ()
continueLoop =
do g <- getContext
cs <- continues <$> get
case cs of
(c:cs') -> modify (\s -> s { continues = (g:c):cs' })
[] -> error "inconsistent continue stack in continue"
-- Switch statemence
enterSwitch :: State Checker ()
enterSwitch =
modify (\s -> s { breaks = []:(breaks s), branches = []:(branches s),
returned = []:(returned s) })
exitSwitch :: State Checker [SContext]
exitSwitch =
do ks <- breaks <$> get
bs <- branches <$> get
rs <- returned <$> get
case (ks,bs,rs) of
(k:ks', b:bs', r:(r1:r1s):rs') ->
do modify (\s -> s { breaks = ks', branches = bs',
returned = ((and $ r1:r):r1s):rs' })
return k -- XXX FIXME: doesn't account for fallthrough;
_ -> error "inconsistent break or return stack exiting switch"
enterCase :: State Checker SContext
enterCase =
do rs <- returned <$> get
case rs of
(r:rs') -> modify (\s -> s { returned = (False:r):rs' })
[] -> error "inconsistent return stack entering case"
getContext
exitCase :: SContext -> State Checker ()
exitCase g0 =
do g <- getContext
ss <- branches <$> get
case ss of
(gs:ss') -> do modify (\s -> s { branches = (g:gs):ss' })
[] -> error "inconsistent branches stack exiting case"
setContext g0 -- XXX FIXME: this silently breaks in fall-through cases
-- If statemence
enterIf :: State Checker ()
enterIf =
modify (\s -> s { branches = []:(branches s), returned = []:(returned s) })
exitIf :: NodeInfo -> State Checker (Bool, Bool)
exitIf nobe =
do bs <- branches <$> get
rs <- returned <$> get
case (bs,rs) of
(b:bs', (r@[case1,case2]):(r1:r1s):rs') ->
do modify (\s -> s { branches = bs',
returned = ((and $ r1:r):r1s):rs' })
return (case1,case2)
_ -> error $ "inconsistent branch or return stack exiting if"
++ show (bs,rs) ++ show nobe
enterBranch :: State Checker SContext
enterBranch =
do rs <- returned <$> get
case rs of
(r:rs') -> modify (\s -> s { returned = (False:r):rs' })
[] -> error "inconsistent return stack entering branch"
getContext
exitBranch :: SContext -> State Checker SContext
exitBranch g0 =
do g <- getContext
ss <- branches <$> get
case ss of
(gs:ss') -> do modify (\s -> s { branches = (g:gs):ss' })
[] -> error "inconsistent branches stack exiting branch"
setContext g0
return g
-- Miscellaneous flow
doReturn :: NodeInfo -> State Checker () -- can't really call it 'return'
doReturn nobe =
do g <- getContext
endings <- ends <$> get
case endings of
(gs:rest) -> modify (\s -> s { ends = (g:gs):rest })
[] -> error "attempt to return outside of a function??"
rs <- returned <$> get
case rs of
((True:r1s):rs') -> do warn nobe "double return" emptyMsg
modify (\s -> s { returned = (True:r1s):rs' })
((False:r1s):rs') -> modify (\s -> s { returned = (True:r1s):rs' })
_ -> error "inconsistent returned stack"
isConcrete :: SContext -> Bool
isConcrete (RuleConst _, []) = True
isConcrete (RuleConst _, _) = False
isConcrete (RuleVar _, _) = False
toConcrete :: SContext -> Context
toConcrete (RuleConst (Rule g), []) = g
toConcrete _ = error "assert fail: tried to convert symbolic context to concrete one"
fromConcrete :: Context -> SContext
fromConcrete g = (RuleConst $ Rule g, [])
checkMergeContexts :: NodeInfo -> SContext -> [SContext] -> State Checker ()
checkMergeContexts nobe g0 gs =
let msg = if all isConcrete (g0:gs) then "merging flow"
else "merging symbolic flow"
in when (any (/= g0) gs) $
warn nobe "merging flow" $
[M "current context" g0] ++ map (M "incoming context") gs
-- ++ [M "most restrictive" $ minimum $ g0:gs]
mergeContexts :: NodeInfo -> SContext -> [SContext] -> State Checker SContext
mergeContexts nobe g0 gs =
do let g = if all isConcrete (g0:gs) then
fromConcrete $ minimum $ map toConcrete $ g0:gs
else
g0 -- don't bother; checkmerge will warn
checkMergeContexts nobe g0 gs
modify (\s -> s { context = g })
return g
mergeContexts_ nobe g0 gs = mergeContexts nobe g0 gs >> return ()
checkBackEdge :: NodeInfo -> SContext -> SContext -> State Checker ()
checkBackEdge nobe g0 g =
do g <- getContext
case (g0,g) of
((RuleConst (Rule g0'),[]),(RuleConst (Rule g'),[])) ->
-- old 799 case
when (g' < g0') $
warn nobe "backward jump with a more restrictive context"
[M "old context" g0, M "incoming context" g]
_ ->
when (g /= g0) $
warn nobe "backward jump with a symbolic context"
[M "old context" g0, M "incoming context" g]
gotoLabel :: NodeInfo -> SContext -> Ident -> State Checker ()
gotoLabel nobe g name =
do ls <- labels <$> get
case Map.lookup name ls of
Just (Left gs) ->
-- Append the new context to the list of incoming contexts.
do modify (\s -> s { labels = Map.insert name (Left $ g:gs) ls })
info nobe "forward goto to label with context"
[M "target" $ show name, M "incoming" $ show g]
Just (Right g0) ->
-- Check the new context against the already decided-upon one.
checkBackEdge nobe g0 g
Nothing ->
do modify (\s -> s { labels = Map.insert name (Left [g]) ls})
info nobe "forward goto to label with context"
[M "target" $ show name, M "incoming" $ show g]
meetLabel :: NodeInfo -> SContext -> Ident -> State Checker ()
meetLabel nobe g0 name =
do ls <- labels <$> get
case Map.lookup name ls of
Just (Left gs) ->
do g <- mergeContexts nobe g0 gs
modify (\s -> s { labels = Map.insert name (Right g) ls})
Just (Right _) ->
do err nobe "meeting an already-met label (duplicate label?)"
[M "label name" name]
modify (\s -> s { labels = Map.insert name (Right g0) ls})
Nothing ->
modify (\s -> s { labels = Map.insert name (Right g0) ls})
--
-- Helpers.
--
getType :: TypeName -> State Checker (Maybe Type)
getType name =
do t' <- Map.lookup name <$> types <$> get
-- strip outer "pointer" from function pointers. see also checkDeclr
case t' of Just (Pointer (x@(Arrow _ _ _ _))) -> return $ Just x
Just (IncompleteStruct sub) ->
do t2' <- Map.lookup (StructName sub) <$> types <$> get
case t2' of Just t2@(Struct _ _) -> return $ Just t2
_ -> return t'
_ -> return t'
getTypeOrBase :: NodeInfo -> TypeName -> State Checker Type
getTypeOrBase nobe name =
do t' <- getType name
case t' of Just t -> return t
Nothing -> do warn nobe "ident's type not in context" [name]
return Base
addType :: NodeInfo -> TypeName -> Type -> State Checker ()
addType nobe name t =
do prior' <- Map.lookup name <$> types <$> get
case prior' of
Just (IncompleteStruct _) ->
info nobe "incomplete struct being defined"
[M "named " $ show name, M "contence" $ show t]
Just t0 ->
if t == t0 then
info nobe "type is being shadowed (same type)"
[M "named" $ show name, M "type " $ show t]
else
warn nobe "type is being shadowed (different type)"
[M "named " $ show name, M "old type" $ show t0,
M "new type" $ show t]
Nothing -> return ()
modify (\s -> s { types = Map.insert name t $ types s })
getState :: State Checker Checker
getState = get
getContext :: State Checker SContext
getContext = context <$> get
restoreState :: Checker -> State Checker ()
restoreState oldstate =
modify (\s -> s { context = context oldstate, types = types oldstate })
-- This could well be deprecated. Only used when processing e1?e2:e3.
mergeState :: NodeInfo -> Checker -> Checker -> State Checker ()
mergeState nobe state1 state2 =
case (context state1, context state2) of
((RuleConst (Rule g1),[]),(RuleConst (Rule g2),[])) ->
-- old, nonsymbolic code
do when (g1 /= g2) $
warn nobe "context mismatch in flow control" [g1,g2]
-- use subbest type
modify (\s -> s { context = fromConcrete $ min g1 g2 })
(g1,g2) ->
do when (g1 /= g2) $
warn nobe "symbolic context mismatch in flow control" [g1,g2]
-- Arbitrary. Not much to be done here.
modify (\s -> s { context = g2 })
setContext :: SContext -> State Checker ()
setContext g = modify (\s -> s { context = g })
getTypes :: State Checker (Map.Map TypeName Type)
getTypes = types <$> get
setTypes :: Map.Map TypeName Type -> State Checker ()
setTypes ts = modify (\s -> s { types = ts })
--
-- Constraints
--
newRV :: String -> State Checker RV
newRV desc = do rv <- nextRV <$> get
modify (\s -> s { nextRV = rv + 1 })
return $ RV rv desc
newEV :: String -> State Checker EV
newEV desc = do ev <- nextEV <$> get
modify (\s -> s { nextEV = ev + 1 })
return $ EV ev desc
newUnknown :: String -> State Checker (RV,EV)
newUnknown desc = do rv <- newRV desc; ev <- newEV desc; return (rv,ev)
-- TODO: solve constraints progressively each time one is added?
addConstraint :: Constraint -> State Checker ()
addConstraint c = modify (\s -> s { constraints = c:(constraints s) })
-- Used to replace already-added symbolic variables when an annotated symbol
-- definition is encountered (usually functions, I guess?)
replaceVars :: NodeInfo -> (RV,EV) -> Annotation -> State Checker ()
replaceVars nobe (rv,ev) (Annotation (r,e)) =
let -- "traverse" functions
replaceR r1@(RuleVar rv1) = if rv == rv1 then RuleConst r else r1
replaceR r1 = r1
replaceE e1@(EffectVar ev1) = if ev == ev1 then EffectConst e else e1
replaceE e1 = e1
replaceSContext :: SContext -> SContext
replaceSContext (r1,es) = (replaceR r1, map replaceE es)
replaceType :: Type -> Type
replaceType Base = Base
replaceType t@(Arrow args rt b (Right (rv1,ev1))) =
if rv1 == rv && ev1 == ev then
Arrow args rt b (Left $ Annotation (r,e))
else if rv1 /= rv && ev1 /= ev then t
else error $ "incomplete match replacing arrow" ++ show t
replaceType t@(Arrow _ _ _ (Left _)) = t
replaceType (Pointer t) = Pointer $ replaceType t
replaceType (Struct i' types) =
Struct i' $ Map.map replaceType types
replaceType t@(IncompleteStruct _) = t
replaceConstraint :: Constraint -> Either (Maybe Constraint) Constraint
replaceConstraint (EffectConstraint e0 es) =
cfold $ EffectConstraint (replaceE e0) (map replaceE es)
replaceConstraint (RuleConstraint r0 r1 es) =
cfold $ RuleConstraint (replaceR r0) (replaceR r1) (map replaceE es)
replaceConstraint (InvariantConstraint r0 r1) =
cfold $ InvariantConstraint (replaceR r0) (replaceR r1)
replaceLabel :: Either [SContext] SContext -> Either [SContext] SContext
replaceLabel (Left gs) = Left $ map replaceSContext gs
replaceLabel (Right g) = Right $ replaceSContext g
in do -- This get is intentionally supposed to not compile if Checker changes.
-- Requires manual inspection for any new SContext, Type, RV, EV, etc.
Checker g ts ms ls bks conts brs rets es cs nrv nev <- get
let g' = replaceSContext g
let ts' = Map.map replaceType ts
let ls' = Map.map replaceLabel ls
let bks' = map (map replaceSContext) bks
let conts' = map (map replaceSContext) conts
let brs' = map (map replaceSContext) brs
let es' = map (map replaceSContext) es
-- In processing the constraints, some of them could fail! We need to
-- output the appropriate message if so.
let (cs',faileds) = partitionEithers $ map replaceConstraint cs
let cs'' = catMaybes cs'
mapM_ (\x -> err nobe "Impossible constraint"
[M "when replacing constraint vars" $ show (rv,ev),
M "with concrete annotation" $ show (r,e)]) faileds
put $ Checker g' ts' ms ls' bks' conts' brs' rets es' cs'' nrv nev
--
-- Messaging
--
emptyMsg = [] :: [String]
filerowcol :: NodeInfo -> String
filerowcol nobe =
let -- (row,col) = (posRow $ posOfNode nobe, posColumn $ posOfNode nobe)
row = posRow $ posOfNode nobe
-- Two different lines for two different version of Language.C.
-- Uncomment whichever one works.
--- file = case fileOfNode nobe of Just f -> f; Nothing -> "((unknown))"
file = fileOfNode nobe
in file ++ ":" ++ (show row)
msg :: (Show a) => String -> NodeInfo -> String -> [a] -> State Checker ()
msg prefix nobe str noobs =
let mess0 = prefix ++ ": at " ++ filerowcol nobe ++ ": " ++ str
mess = foldl (\output noob -> output ++ "\n\t" ++ show noob) mess0 noobs
in modify (\s -> s { msgs = mess:(msgs s) })
err :: (Show a) => NodeInfo -> String -> [a] -> State Checker ()
err = msg "ERROR" -- TODO: make this fail
warn :: (Show a) => NodeInfo -> String -> [a] -> State Checker ()
warn = msg "warning"
info :: (Show a) => NodeInfo -> String -> [a] -> State Checker ()
-- info = msg "(info)"
info _ _ _ = return () -- TODO: better msg datatype
--
-- Verification.
--
containsArrows :: Type -> Bool
containsArrows (Base) = False
containsArrows (Pointer t) = containsArrows t
containsArrows (Arrow _ _ _ _) = True
containsArrows (Struct _ contence) = F.any containsArrows contence
containsArrows (IncompleteStruct _) = False
-- if doDisjoin, then disjoin the types; else, intersect the types.
-- this comes into play when doing arrow annotations.
mergeType :: Bool -> NodeInfo -> Type -> Type -> State Checker Type
mergeType doDisjoin nobe (Base) (Base) = return Base
mergeType doDisjoin nobe (Pointer t1) (Pointer t2) =
Pointer <$> mergeType doDisjoin nobe t1 t2
mergeType doDisjoin nobe (Struct name1 m1) (Struct name2 m2) =
if (m1 == m2) then
-- would disjoin structs, but (a) technical difficulties and (b) stupid
liftM (Struct name1) $ T.sequence $
Map.intersectionWith (mergeType doDisjoin nobe) m1 m2
else
do warn nobe "incompatible structs during type intersection" [m1,m2]
return Base
mergeType doDisjoin nobe t1@(Arrow args1 ret1 iv1 a1) t2@(Arrow args2 ret2 iv2 a2) =
do -- contravariance on the disjoin/intersect operator
-- actually only theoretically sound because of the total ordering.
args <- zipWithM (mergeType (not doDisjoin) nobe) args1 args2
ret <- mergeType doDisjoin nobe ret1 ret2
when (iv1 /= iv2) $ warn nobe "variadicity mismatch in fn merge" emptyMsg
let iv = iv1 || iv2
case (a1,a2) of
-- We throw in the towel on merging constraints here. If one is symbolic,
-- we ignore it and take the other one; if both are, we take the left one.
-- I don't expect this will ever come up so I'm not bothering to support it.
(Left a1', Left a2') -> -- good case
case (if doDisjoin then disjoin else intersect) a1' a2' of
Just a -> return $ Arrow args ret iv $ Left a
Nothing -> do err nobe "unmergable annotations" [a1',a2']
return $ Arrow args ret iv (Left a1') -- boo
(a@(Left _), Right _) ->
do warn nobe "ignoring symbolic type for merge on right branch" [t1,t2]
return $ Arrow args ret iv a
(Right _, a@(Left _)) ->
do warn nobe "ignoring symbolic type for merge on left branch" [t1,t2]
return $ Arrow args ret iv a
(a@(Right _), Right _) ->
do warn nobe "arbitrarily merging symbolic types" [t1,t2]
return $ Arrow args ret iv a
mergeType doDisjoin nobe (IncompleteStruct _) t2 =
mergeType doDisjoin nobe Base t2
mergeType doDisjoin nobe t1 (IncompleteStruct _) =
mergeType doDisjoin nobe t1 Base
mergeType doDisjoin nobe t1 t2 =
do warn nobe "type mismatch during merge" [t1,t2]; return Base
toRE :: Either Annotation Unknown -> (R,E)
toRE (Left (Annotation(r,e))) = (RuleConst r, EffectConst e)
toRE (Right (rv,ev)) = (RuleVar rv, EffectVar ev)
-- TODO: need to worry about extra pointer indirections around arrows? &malloc
-- The bool argument expresses whether subtyping is allowed.
verifyAssign :: NodeInfo -> Bool -> Type -> Type -> State Checker ()
verifyAssign nobe subtyping t1@(Arrow args1 ret1 iv1 a1) t2@(Arrow args2 ret2 iv2 a2) =
let constrainAssignment (r1,e1) (r2,e2) =
do addConstraint $ EffectConstraint e1 [e2]
addConstraint $
if subtyping then RuleConstraint r1 r2 []
else InvariantConstraint r1 r2
verifyAnnotation =
case (a1,a2) of
(Left a1', Left a2') ->
if subtyping then
when (not $ subtype a1' a2') $
err nobe "illegal subtyped function pointer assignment"
[M "dest (req'd supertype)" a1',
M "src (req'd subtype)" a2']
else
when (a1' /= a2') $
err nobe "illegal invariant function pointer assignment"
[M "dest" a1', M "src" a2']
_ -> constrainAssignment (toRE a1) (toRE a2)
in do when (length args1 /= length args2) $
warn nobe "verification argument count mismatch" [t1,t2]
when (iv1 /= iv2) $
warn nobe "variadicity mismatch in fn verification" emptyMsg
verifyAnnotation
verifyAssign nobe subtyping ret1 ret2
mapM_ (uncurry $ verifyAssign nobe subtyping)
(zip args2 args1) -- contravariant!
info nobe "verified assignment" [M "dest type" t1, M "src type" t2]
-- Pointers
verifyAssign nobe subtyping (Pointer Base) (Pointer Base) = return ()
verifyAssign nobe subtyping (Pointer Base) t2 =
info nobe "allowing cast to void *" [t2]
verifyAssign nobe subtyping t1 (Pointer Base) =
info nobe "allowing cast from void *" [t1]
verifyAssign nobe subtyping (Pointer t1) (Pointer t2) =
verifyAssign nobe False t1 t2 -- Reference cells are invariant.
-- Structs
verifyAssign nobe subtyping (Struct _ m1) (Struct _ m2) =
mapM_ (uncurry $ verifyAssign nobe subtyping) -- Structs aren't quite refs.
(zip (Map.elems m1) (Map.elems m2))
verifyAssign nobe subtyping Base Base = return ()
verifyAssign nobe subtyping (IncompleteStruct _) t2 =
verifyAssign nobe subtyping Base t2 -- trying to resolve this causes stack overflow
verifyAssign nobe subtyping t1 (IncompleteStruct _) =
verifyAssign nobe subtyping t1 Base
-- No match
verifyAssign nobe subtyping t1 t2 =
if containsArrows t1 || containsArrows t2 then
warn nobe "verification type mismatch, with arrows" [t1,t2]
else
info nobe "verification type mismatch (no arrows)" [t1,t2]
verifyCall :: NodeInfo -> Either Annotation Unknown -> State Checker ()
verifyCall nobe au =
do (g,es) <- getContext
case (g,au,es) of
(RuleConst (Rule g), Left a, []) -> -- everything is known, wee
-- original 799 code here
do -- Check rule
when (not $ satisfies a g) $
err nobe "illegal function call"
[M "target function" $ show a, M "while in context" $ show g]
-- Check effect
case effect a g of
Just g2 -> do info nobe "changed context"
[g2]
setContext (RuleConst $ Rule g2, [])
Nothing -> err nobe "illegal context effect"
[M "attempted call " $ show a,
M "current context" $ show g]
(_,Left (Annotation (r,e)),_) -> -- need to generate a constraint
do addConstraint $
RuleConstraint (RuleConst r) g es
-- Effecting the context directly could screw up the ordering;
-- in cases of Enable(+inf)/Disable(-inf), commutativity fails
setContext (g, (EffectConst e):es)
(_,Right (rv,ev),_) -> -- need to generate a constraint
do addConstraint $
RuleConstraint (RuleVar rv) g es
setContext (g, (EffectVar ev):es)
-- Mashes an annotation into an arrow type that might already have one.
-- TODO constraint
injectAnnotation :: NodeInfo -> Type -> Maybe Annotation -> State Checker Type
injectAnnotation nobe (Arrow args ret iv (Left a0)) (Just a) =
do warn nobe "multiply-differently-annotated function" [a0,a]
return $ Arrow args ret iv (Left a)
injectAnnotation nobe (Arrow args ret iv (Right (rv,ev))) (Just a) =
-- Was previously symbolic, now concrete. Use the concrete value always.
do -- Need to filter over the existing constraints and substitute out the
-- concrete constraint for them.
replaceVars nobe (rv,ev) a
return $ Arrow args ret iv (Left a)
injectAnnotation nobe t (Just a) =
do warn nobe "ignoring annotation on non-function" [a]
return t
injectAnnotation nobe t (Nothing) = return t
--
-- Main iteration.
--
-- TODO: For multi-file checking, we probably need to return a global vars map.
check :: CTranslUnit -> ([String], [Constraint])
check (CTranslUnit decls nobe) =
let state = execState (mapM_ checkExtDecl decls) defaultChecker
in (reverse $ msgs $ state, reverse $ constraints $ state)
checkExtDecl :: CExtDecl -> State Checker ()
checkExtDecl (CDeclExt d) = checkDecl_ d
checkExtDecl (CFDefExt f) = checkFunDef f
checkExtDecl (CAsmExt _) = return ()
-- checkExtDecl (CAsmExt _ _) = return ()
checkFunDef :: CFunDef -> State Checker ()
checkFunDef (CFunDef specs declr oldstyle body nobe) =
let addFunc (Just name) t =
do told' <- getType (VarName name)
-- If previously declared, check that the defined type matches.
case told' of
Just told -> verifyAssign nobe True told t
Nothing -> addType nobe (VarName name) t
addFunc Nothing t = return () -- when does this happen?
in do (t0',a',_) <- checkDeclSpecs nobe specs -- 'typedef' never on functions
-- do add posible args to context.
oldstate <- getState
(name',t0) <- checkDeclr (fromMaybe Base t0') True declr
when (not $ null oldstyle) $
warn nobe "old-style args not supported in function def'n" [name']
t <- injectAnnotation nobe t0 a'
let a'' = case t of (Arrow _ _ _ x) -> x; _ -> error "Non-arrow func??"
-- add function name to context
-- this has to be done twice, for the function to be scoped inside
-- itself and also after dropping the type mappings from inside.
addFunc name' t
-- traverse function body; save old context in case of nested function
g <- case a'' of
Left a -> return $ (RuleConst $ Rule $ entryContext a, [])
Right (rv,ev) -> return $ (RuleVar rv, [])
info nobe "entering function with context" [g]
gold <- getContext
setContext g
modify (\s -> s { returned = [False]:(returned s), ends = []:(ends s)})
checkStat body
-- check exit context against advertised effect
gnew <- getContext
case a'' of
Left a ->
if isConcrete gnew then
-- original case
when (effect a (toConcrete g) /= Just (toConcrete gnew)) $
err nobe "exit context != advertised effect"
[M "entry context" $ toConcrete g,
M "exit context" $ toConcrete gnew]
else
let (Annotation (_,e)) = a
in addConstraint $ EffectConstraint (EffectConst e) (snd gnew)
Right (rv,ev) ->
do when (isConcrete gnew) $ error "...???"
addConstraint $ EffectConstraint (EffectVar ev) (snd gnew)
-- check all returned contexts against each other
endings <- ends <$> get
case endings of
(gs:rest) ->
do when (not $ all (== gnew) gs) $
err nobe "not all exit contexts match each other"
(gnew:gs)
modify (\s -> s { ends = rest })
_ -> error "inconsistent ends stack at function end"
-- restore old context and types mapping
restoreState oldstate
-- second time - make this function be scoped in future functions
-- The annotation needs to be injected again because the previous
-- inject's replacevars occurred under the temporary state, and needs
-- to be made permanent.
t <- injectAnnotation nobe t0 a'
addFunc name' t
checkDecl :: Bool -> CDecl -> State Checker [(Maybe Ident, Type)]
checkDecl remember (CDecl specs noobs nobe) =
let checkTriple a' kindName t0 (declr', val', bitfield') =
do -- Sometimes the noob is unnamed.
(name',t) <- maybe (return (Nothing,t0)) (checkDeclr t0 False) declr'
t2 <- injectAnnotation nobe t a'
-- Check the initialiser
maybe (return ()) (checkInit t) val'
maybe (return ()) checkExpr_ bitfield'
-- Record and return
when remember $
maybe (return ()) (\name -> addType nobe (kindName name) t2)
name'
return (name',t2)
in do (t',a',kindName) <- checkDeclSpecs nobe specs
let t = maybe Base id t'
mapM (checkTriple a' kindName t) noobs
checkDecl_ d = checkDecl True d >> return ()
checkOneDecl :: CDecl -> State Checker (Maybe Ident, Type)
checkOneDecl d@(CDecl _ _ nobe) =
do list <- checkDecl True d
case list of [] -> return (Nothing, Base) -- error "empty decl??"
[x] -> return x
x:rest -> do warn nobe "ignoring extra decls" rest; return x
checkStructUnion :: CStructUnion -> State Checker Type
checkStructUnion (CStruct tag (Just name) Nothing attrs nobe) =
do t' <- getType $ StructName name
case t' of -- Honour incomplete struct declarations
Just t -> return t
Nothing -> do addType nobe (StructName name) (IncompleteStruct name)
return $ IncompleteStruct name
checkStructUnion (CStruct tag name' (Just decls) attrs nobe) =
let namedOnly (Just x, y) = Just (x, y)
namedOnly (Nothing, _) = Nothing
in do contence <- Map.fromList <$> mapMaybe namedOnly <$>
concat <$> mapM (checkDecl False) decls
case name' of
Just name -> addType nobe (StructName name)
(Struct (Just name) contence)
Nothing -> return ()
return $ Struct name' contence
checkStructUnion (CStruct tag Nothing Nothing attrs nobe) =
do warn nobe "illegal struct structure" emptyMsg; return Base
checkEnum :: CEnum -> State Checker ()
checkEnum (CEnum _ Nothing _ _) = return ()
checkEnum (CEnum _ (Just list) _ _) =
mapM_ (\(_,x) -> T.mapM checkExpr x) list
-- Declaration specifiers
checkDeclSpec :: NodeInfo -> (Maybe Type, Maybe Annotation, Ident -> TypeName)
-> CDeclSpec
-> State Checker (Maybe Type, Maybe Annotation,
Ident -> TypeName)
checkDeclSpec nobe (t0',a0',_) (CStorageSpec (CTypedef _)) =
return (t0',a0',TypedefName) -- typedefs get different context constructors
checkDeclSpec nobe (t0',a0',x) (CStorageSpec _) = return (t0',a0',x)
checkDeclSpec nobe (t0',a0',x) (CTypeSpec spec) =
do t <- checkTypeSpec spec
case (t,t0') of
-- For qualifiers like "unsigned", "long", "double", etc.
(Base, Just Base) -> return (Just Base, a0', x)
(_, Just t0) ->
do warn nobe "multi-typed declspec!"
[M "overriding:" t0, M "with new type:" t]
return (Just t, a0', x)
(_, Nothing) -> return (Just t, a0', x)
checkDeclSpec nobe (t0',a0',x) (CTypeQual qual) =
do a' <- checkTypeQual qual
case (a0',a') of
(Just a0, Just a) ->
do warn nobe "multi-annotated declspec!"
[M"overriding:" a0, M "with new annotation:" a]
return (t0',a',x)
(Nothing, Just _) -> return (t0',a',x)
_ -> return (t0',a0',x)
checkDeclSpecs :: NodeInfo -> [CDeclSpec]
-> State Checker (Maybe Type, Maybe Annotation,
Ident -> TypeName)
checkDeclSpecs nobe specs =
foldM (checkDeclSpec nobe) (Nothing, Nothing, VarName) specs
-- Type specifiers
checkTypeSpec :: CTypeSpec -> State Checker Type
checkTypeSpec (CVoidType nobe) = return Base
checkTypeSpec (CCharType nobe) = return Base
checkTypeSpec (CShortType nobe) = return Base
checkTypeSpec (CIntType nobe) = return Base
checkTypeSpec (CLongType nobe) = return Base
checkTypeSpec (CFloatType nobe) = return Base
checkTypeSpec (CDoubleType nobe) = return Base
checkTypeSpec (CSignedType nobe) = return Base
checkTypeSpec (CUnsigType nobe) = return Base
checkTypeSpec (CBoolType nobe) = return Base
checkTypeSpec (CComplexType nobe) = return Base
checkTypeSpec (CSUType strux nobe) = checkStructUnion strux
checkTypeSpec (CEnumType enum nobe) = return Base
checkTypeSpec (CTypeDef name nobe) = getTypeOrBase nobe $ TypedefName name
checkTypeSpec (CTypeOfExpr e nobe) =
do warn nobe "using typeof(expr) may emit spurious warnings." emptyMsg
checkExpr e -- TODO
checkTypeSpec (CTypeOfType d nobe) =
do warn nobe "using typeof(type) may emit spurious warnings." emptyMsg
snd <$> checkOneDecl d -- TODO
checkTypeQual :: CTypeQual -> State Checker (Maybe Annotation)
checkTypeQual (CAttrQual a) = checkAttr a
checkTypeQual _ = return Nothing
checkAttr :: CAttr -> State Checker (Maybe Annotation)
checkAttr (attr@(CAttr name es nobe)) =
if attrIsAnnotation name then
do let a' = attrToAnnotation es
when (isNothing a') $ warn nobe "invalid annotation!" [show name]
return a'
else return Nothing
checkAttrs :: NodeInfo -> Maybe Ident -> [CAttr]
-> State Checker (Either Annotation Unknown)
checkAttrs nobe name' attrs =
let -- We decide either to allocate a new (RV,EV) or, if "name" is already
-- defined in the context, to reuse the annotation/unknown from before.
decideUnknown (Just name) =
do told' <- getType $ VarName name
case told' of
Just (Arrow _ _ _ x) -> return x
_ -> Right <$> (newUnknown $ identToString name ++ "@"
++ filerowcol nobe)
decideUnknown Nothing = Right <$> (newUnknown $ filerowcol nobe)
in do annos <- catMaybes <$> mapM checkAttr attrs
case annos of
[] -> decideUnknown name'
[a] -> return $ Left a
a:rest -> do warn nobe "ignoring extra annotations" rest
return $ Left a
-- Declarators
-- When called from fundef, need to add the args to the context. otherwise not.
checkDeclr :: Type -> Bool -> CDeclr -> State Checker (Maybe Ident, Type)
checkDeclr t0 addArgs (CDeclr name' deriveds asmname attrs nobe) =
do t' <- checkDerivedDeclrs t0 name' addArgs deriveds
-- strip the outermost "pointer" type derived-decl from function pointers.
-- see also: getType
let t = case t' of (Pointer x@(Arrow _ _ _ _)) -> x; _ -> t'
t2 <- case t of
(Arrow _ _ _ _) ->
-- only check attrs for functions, to not waste RVs/EVs
do a' <- checkAttrs nobe name' attrs
injectAnnotation nobe t
(case a' of Left a -> Just a; _ -> Nothing)
_ -> return t
return (name', t2)
checkDerivedDeclrs :: Type -> Maybe Ident -> Bool -> [CDerivedDeclr]
-> State Checker Type
checkDerivedDeclrs t0 name' addArgs [] = return t0
checkDerivedDeclrs t0 name' addArgs ((CPtrDeclr quals nobe):rest) =
Pointer <$> checkDerivedDeclrs t0 name' addArgs rest
checkDerivedDeclrs t0 name' addArgs ((CArrDeclr quals size nobe):rest) =
do checkArrSize size; Pointer <$> checkDerivedDeclrs t0 name' addArgs rest
checkDerivedDeclrs t0 name' addArgs ((CFunDeclr args'' attrs nobe):rest) =
do t <- checkDerivedDeclrs t0 name' addArgs rest
a' <- checkAttrs nobe name' attrs
(args,isVariadic) <-
case args'' of
Left oldstyle ->
do warn nobe "old-style args ignored" [Arrow [] t False a']
return ([],False)
Right (decls,isVariadic) ->
do args <- map snd <$> concat <$>
mapM (checkDecl addArgs) decls
return (args,isVariadic)
info nobe "processed FunDeclr" [Arrow args t isVariadic a']
-- XXX: some bug causes this to not like unnamed arguments.
return $ Arrow args t isVariadic a'
-- Misc
checkArrSize :: CArrSize -> State Checker ()
checkArrSize (CNoArrSize _) = return ()
checkArrSize (CArrSize _ e) = checkExpr_ e
checkInit :: Type -> CInit -> State Checker ()
checkInit t0 (CInitExpr e nobe) =
do t <- checkExpr e
verifyAssign nobe True t0 t
checkInit t0 (CInitList inits nobe) = mapM_ (checkInitListElem nobe t0) inits
checkInitListElem :: NodeInfo -> Type -> ([CDesignator], CInit)
-> State Checker ()
checkInitListElem nobe (Pointer t) ([], i) = checkInit t i
checkInitListElem nobe (Base) ([], i) = checkInit Base i -- dur
checkInitListElem nobe _ ([], i) =
do warn nobe "empty struct member designator not supported." emptyMsg
checkInit Base i
checkInitListElem nobe t0 (list, i) =
do t <- foldM checkDesignator t0 list
checkInit t i
checkDesignator :: Type -> CDesignator -> State Checker Type
checkDesignator t0 (CArrDesig e nobe) =
do checkExpr_ e
case t0 of (Pointer t) -> return t
_ -> do warn nobe "array designator in non-array type" [t0]
return Base
checkDesignator t0 (CRangeDesig e1 e2 nobe) =
do checkExpr_ e1
checkExpr_ e2
case t0 of (Pointer t) -> return t
_ -> do warn nobe "array designator in non-array type" [t0]
return Base
checkDesignator t0@(Struct _ contence) (CMemberDesig name nobe) =
case Map.lookup name contence of
Just t -> return t
Nothing -> do warn nobe "member designator not found in struct type"
[M "type" $ show t0, M "member" $ show name]
return Base
checkDesignator t0 (CMemberDesig name nobe) =
do warn nobe "member designator for non-struct type"
[M "type" $ show t0, M "member" $ show name]
return Base
-- Statemence.
checkStat :: CStat -> State Checker Type
checkStat (CLabel name s attrs nobe) =
do g0 <- getContext
meetLabel nobe g0 name
checkStat s
checkStat (CCase e s nobe) =
do g0 <- enterCase
checkExpr_ e
checkStat_ s
exitCase g0
return Base
checkStat (CCases e1 e2 s nobe) =
do g0 <- enterCase
checkExpr_ e1
checkExpr_ e2
checkStat_ s
exitCase g0
return Base
checkStat (CDefault s nobe) =
do g0 <- enterCase
checkStat_ s
exitCase g0
return Base
checkStat (CExpr e' nobe) = maybe (return Base) checkExpr e'
checkStat (CCompound labels blox nobe) =
do ts <- getTypes
mapM_ checkBlockItem blox
setTypes ts
return Base
checkStat (CIf e s1 s2' nobe) =
do checkExpr_ e
enterIf
g0 <- enterBranch
checkStat_ s1
g1 <- exitBranch g0
_ <- enterBranch
maybe (return ()) checkStat_ s2'
g2 <- exitBranch g0
(returned1,returned2) <- exitIf nobe -- See which branches did return or not.
case (returned1,returned2) of
(False,False) -> mergeContexts_ nobe g1 [g2]
(True,False) -> setContext g2
(False,True) -> setContext g1
_ -> return () -- Means we returned wholesale.
return Base
checkStat (CSwitch e s nobe) =
do checkExpr_ e
g0 <- getContext
enterSwitch
checkStat_ s
gs <- exitSwitch
mergeContexts_ nobe g0 gs
return Base
checkStat (CWhile e s isDoWhile nobe) =
do g0 <- getContext
when (not isDoWhile) $ checkExpr_ e
enterLoop
checkStat_ s
(bs,cs) <- exitLoop
when (isDoWhile) $ checkExpr_ e
g <- getContext
checkMergeContexts nobe g0 cs -- continues go backwards
checkBackEdge nobe g0 g
mergeContexts_ nobe g bs -- breaks go forwards
return Base
checkStat (CFor e1'' e2' e3' s nobe) =
do ts <- getTypes
case e1'' of
(Left Nothing) -> return ()
(Left (Just e)) -> checkExpr_ e
(Right d) -> checkDecl_ d
g0 <- getContext
maybe (return ()) checkExpr_ e2'
enterLoop
checkStat_ s
(bs,cs) <- exitLoop
g1 <- getContext
mergeContexts_ nobe g1 cs -- continues go forwards
maybe (return ()) checkExpr_ e3'
g2 <- getContext
checkBackEdge nobe g0 g2
mergeContexts_ nobe g2 bs -- breaks go even more forwards
return Base
checkStat (CGoto name nobe) =
do g <- getContext
gotoLabel nobe g name
return Base
checkStat (CGotoPtr e nobe) =
do warn nobe "dynamic pointer goto being ignored." emptyMsg
checkExpr_ e
return Base
checkStat (CCont nobe) = continueLoop >> return Base
checkStat (CBreak nobe) = breakLoop >> return Base
checkStat (CReturn e' nobe) =
do t <- maybe (return Base) checkExpr e'
doReturn nobe
return t
checkStat (CAsm asm nobe) = checkAsmStmt asm >> return Base
checkStat_ s = checkStat s >> return ()
checkBlockItem :: CBlockItem -> State Checker ()
checkBlockItem (CBlockStmt s) = checkStat_ s
checkBlockItem (CBlockDecl d) = checkDecl_ d
checkBlockItem (CNestedFunDef f) =
do s <- getState
checkFunDef f
restoreState s
checkAsmStmt :: CAsmStmt -> State Checker ()
checkAsmStmt (CAsmStmt qual asm outops inops clobbers nobe) =
do mapM_ checkAsmOperand outops; mapM_ checkAsmOperand inops
checkAsmOperand :: CAsmOperand -> State Checker ()
checkAsmOperand (CAsmOperand name constraint e nobe) = checkExpr_ e
-- Expressions.
checkExpr :: CExpr -> State Checker Type
checkExpr (CComma es nobe) = do mapM checkExpr_ es; return Base
checkExpr (CAssign _ e1 e2 nobe) =
do t1 <- checkExpr e1
t2 <- checkExpr e2
verifyAssign nobe True t1 t2
return t1
checkExpr (CCond e1 e2 e3 nobe) =
do t1 <- checkExpr e1
oldstate <- getState
(t2,state2,t3,state3) <-
case e2 of
Just e2' ->
do t2 <- checkExpr e2'
state2 <- getState
restoreState oldstate
t3 <- checkExpr e3
state3 <- getState
return (t2,state2,t3,state3)
Nothing -> -- "x ?: y" means "x ? x : y"
do _ <- checkExpr e1
t3 <- checkExpr e3
state3 <- getState
return (t1,oldstate,t3,state3)
mergeState nobe state2 state3
t23 <- mergeType True nobe t2 t3
info nobe "merged types" [M "left" t2, M "right" t3, M "result" t23]
return t23
checkExpr (CBinary _ e1 e2 nobe) =
do t1 <- checkExpr e1
t2 <- checkExpr e2
case (t1,t2) of
(Pointer t1', Pointer t2') -> return Base
(Pointer t1', _) -> return t1'
(_, Pointer t2') -> return t2'
(_, _) -> return Base
checkExpr (CCast d e nobe) =
do t1 <- snd <$> checkOneDecl d
t2 <- checkExpr e
verifyAssign nobe True t1 t2
return t1
checkExpr (CUnary o e nobe) =
do t <- checkExpr e
case o of -- check for &foo or *foo
CAdrOp -> return $ Pointer t
CIndOp ->
case t of Pointer t' -> return t'
_ -> do warn nobe "can't dereference type" [t]
return Base
_ -> return t
checkExpr (CSizeofExpr e nobe) = return Base
checkExpr (CSizeofType d nobe) = return Base
checkExpr (CAlignofExpr e nobe) = return Base
checkExpr (CAlignofType d nobe) = return Base
checkExpr (CComplexReal e nobe) = error "complexreal not supported yet"
checkExpr (CComplexImag e nobe) = error "compleximag not supported yet"
checkExpr (CIndex e1 e2 nobe) =
do t1 <- checkExpr e1
t2 <- checkExpr e2
case (t1,t2) of
(Pointer t1', Pointer t2') ->
do warn nobe "can't index pointer with pointer" [t1,t2]
return t1'
(Pointer t1', _) -> return t1'
(_, Pointer t2') -> return t2'
(_, _) ->
do warn nobe "can't index non-pointer with non-pointer" [t1,t2]
return Base
checkExpr (CCall e args nobe) =
let checkArg (t,e) =
do t0 <- checkExpr e; verifyAssign nobe True t t0; return t0
in do t <- checkExpr e
case t of
Arrow argtypes ret isVariadic a ->
do callargtypes <- mapM checkArg $ zip argtypes args
case isVariadic of
True ->
let varargs = drop (length argtypes) callargtypes
in when (any containsArrows varargs) $
warn nobe "variadic args contain arrows"
[M "... =" varargs]
False ->
when (length args /= length argtypes) $
warn nobe "argument number mismatch"
[M "expected" argtypes]
verifyCall nobe a
return ret
_ ->
do warn nobe "can't call non-arrow type" [t]
return Base
checkExpr (CMember e name isderef nobe) =
let memberType contence =
case Map.lookup name contence of
Just (Pointer (IncompleteStruct sub)) ->
do t <- getType $ StructName sub
maybe (return $ Pointer Base) (return . Pointer) t
Just (IncompleteStruct sub) ->
do t <- getType $ StructName sub
maybe (return Base) return t
Just t -> return t
Nothing ->
do warn nobe "missing struct member" [name]; return Base
in do t <- checkExpr e
case isderef of -- if/else didn't parse for some reason...
True ->
case t of Pointer (Struct _ contence) -> memberType contence
Pointer (IncompleteStruct sub) ->
do t2 <- getType $ StructName sub
case t2 of
Just (Struct _ contence) ->
memberType contence
_ ->
do warn nobe "bad incomplete->member"
[t]
return Base
_ -> do warn nobe "bad type for struct->member" [t]
return Base
False ->
case t of Struct _ contence -> memberType contence
IncompleteStruct sub ->
do t2 <- getType $ StructName sub
case t2 of
Just (Struct _ contence) ->
memberType contence
_ ->
do warn nobe "bad incomplete.member"
[t]
return Base
_ -> do warn nobe "bad type for struct.member" [t]
return Base
checkExpr (CVar name nobe) = getTypeOrBase nobe $ VarName name
checkExpr (CConst _) = return Base
checkExpr (CCompoundLit d inits nobe) =
do t <- snd <$> checkOneDecl d
mapM (checkInitListElem nobe t) inits
return t
checkExpr (CStatExpr s nobe) = checkStat s
checkExpr (CLabAddrExpr name nobe) = return Base
checkExpr (CBuiltinExpr b) = return Base
checkExpr_ e = checkExpr e >> return ()
Jump to Line
Something went wrong with that request. Please try again.