diff options
author | tomsmeding <tom.smeding@gmail.com> | 2017-08-19 11:05:43 +0200 |
---|---|---|
committer | tomsmeding <tom.smeding@gmail.com> | 2017-08-19 11:05:43 +0200 |
commit | 694ec05bcad01fd27606aace73b49cdade16945e (patch) | |
tree | 5c7a0433232f0860ef18f1634510d4f823ce5bdb /Verify.hs |
Initial
Diffstat (limited to 'Verify.hs')
-rw-r--r-- | Verify.hs | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/Verify.hs b/Verify.hs new file mode 100644 index 0000000..18f90ce --- /dev/null +++ b/Verify.hs @@ -0,0 +1,28 @@ +module Verify(verify) where + +import AST +import Defs +import Intermediate + + +verify :: IRProgram -> Error IRProgram +verify (IRProgram vars funcs) = IRProgram <$> mapM verifyVar vars <*> mapM verifyFunc funcs + +verifyVar :: DVar -> Error DVar +verifyVar dvar@(DVar _ n e) = case e of + ELit _ _ -> return dvar + _ -> Left $ "Initialisation of global variable " ++ n ++ " is not a literal" + +verifyFunc :: IRFunc -> Error IRFunc +verifyFunc irfunc@(IRFunc mrt name _ bbs _) = + let terms = map (\(BB _ _ term) -> term) bbs + (nret', nretr') = unzip $ flip map terms $ \term -> case term of + IRet -> (1, 0) + IRetr _ -> (0, 1) + _ -> (0, 0) + (nret, nretr) = (sum nret', sum nretr') :: (Int, Int) + in case (mrt, nret, nretr) of + (Nothing, _, 0) -> return irfunc + (Just _, 0, _) -> return irfunc + (Nothing, _, _) -> Left $ "Some code paths of void function '" ++ name ++ "' return a value" + (Just _, _, _) -> Left $ "Not all code paths of non-void function '" ++ name ++ "' return a value" |