diff --git a/language-c-extensible/src/Language/C/Analysis/AstAnalysis2.hs b/language-c-extensible/src/Language/C/Analysis/AstAnalysis2.hs index 70b6edc..bc63dc9 100644 --- a/language-c-extensible/src/Language/C/Analysis/AstAnalysis2.hs +++ b/language-c-extensible/src/Language/C/Analysis/AstAnalysis2.hs @@ -38,7 +38,7 @@ import Prelude hiding (mapM, mapM_) data SemPhase -type instance AnnTranslationUnit SemPhase = (NodeInfo, GlobalDecls) +type instance AnnTranslationUnit SemPhase = NodeInfo type instance AnnFunctionDef SemPhase = NodeInfo type instance AnnAsmExt SemPhase = NodeInfo type instance AnnStringLiteral SemPhase = NodeInfo @@ -69,7 +69,7 @@ analyseAST (CTranslUnit decls _file_node) = do getDefTable >>= \dt -> unless (inFileScope dt) $ error "Internal Error: Not in filescope after analysis" gld <- globalDefs <$> getDefTable - return $ CTranslUnit decls' (_file_node, gld) + return $ CTranslUnit decls' (_file_node) analyseExt :: (MonadTrav m) => CExternalDeclaration NodeInfo -> m (CExternalDeclaration SemPhase) diff --git a/vdiff/app/vdiff-take/Main.hs b/vdiff/app/vdiff-take/Main.hs index dce4b39..8fc6fc7 100644 --- a/vdiff/app/vdiff-take/Main.hs +++ b/vdiff/app/vdiff-take/Main.hs @@ -148,7 +148,7 @@ testParse :: FilePath -> IO Bool testParse f = timeoutM (5 * 1000 * 1000) testParse' `catch` (\(_ :: IOException) -> return False) where testParse' = do - res <- liftIO $ runRIO NoLogging $ openCFile f + res <- liftIO $ runRIO NoLogging $ openCFile DefaultTypechecker f case force $ prettyp <$> res of Nothing -> return False Just _ -> return True diff --git a/vdiff/app/vdiff/Main.hs b/vdiff/app/vdiff/Main.hs index 5b86bd9..5326338 100644 --- a/vdiff/app/vdiff/Main.hs +++ b/vdiff/app/vdiff/Main.hs @@ -14,17 +14,17 @@ infos = fullDesc <> progDesc "vdiff - a simple tool to compare program verifiers main :: IO () main = runVDiffApp parseMainParameters infos $ \case - (CmdRun seed dp) -> cmdDiff seed dp - (CmdParseTest fn) -> cmdParseTest fn - (CmdMarkReads mode fn) -> cmdMarkReads mode fn + (CmdRun tc seed dp) -> cmdDiff tc seed dp + (CmdParseTest tc fn) -> cmdParseTest tc fn + (CmdMarkReads mode tc fn) -> cmdMarkReads mode tc fn CmdVersions -> cmdVersions CmdRunVerifiers dp -> cmdRunVerifiers dp -data Cmd = CmdRun (Maybe Int) DiffParameters -- first parameter is the seed +data Cmd = CmdRun TypecheckerFlag (Maybe Int) DiffParameters -- first parameter is the seed | CmdRunVerifiers DiffParameters - | CmdParseTest FilePath - | CmdMarkReads SearchMode FilePath + | CmdParseTest TypecheckerFlag FilePath + | CmdMarkReads SearchMode TypecheckerFlag FilePath | CmdVersions @@ -32,8 +32,8 @@ parseMainParameters :: Parser Cmd parseMainParameters = hsubparser $ mconcat [versionCommand, parseCommand, markCommand, runCommand, diffCommand] where versionCommand = command "versions" (info (pure CmdVersions) (progDesc "display the versions of the integrated verifiers")) - parseCommand = command "parse" (info (CmdParseTest <$> cFile) (progDesc "parses and prints the given file")) - markCommand = command "mark-reads" (info (CmdMarkReads <$> Args.searchMode <*> cFile) (progDesc "marks the reads in the given file")) + parseCommand = command "parse" (info (CmdParseTest <$> Args.typechecker <*> cFile) (progDesc "parses and prints the given file")) + markCommand = command "mark-reads" (info (CmdMarkReads <$> Args.searchMode <*> Args.typechecker <*> cFile) (progDesc "marks the reads in the given file")) runCommand = command "run" (info (CmdRunVerifiers <$> Args.diffParameters) (progDesc "execute verifiers")) - diffCommand = command "diff" (info (CmdRun <$> Args.seed <*> Args.diffParameters) (progDesc "diff verifiers")) + diffCommand = command "diff" (info (CmdRun <$> Args.typechecker <*> Args.seed <*> Args.diffParameters) (progDesc "diff verifiers")) diff --git a/vdiff/assets/test/typecheck/benghazi.c b/vdiff/assets/test/typecheck/benghazi.c new file mode 100644 index 0000000..9695ceb --- /dev/null +++ b/vdiff/assets/test/typecheck/benghazi.c @@ -0,0 +1,24 @@ +/* + * Date: 06/07/2015 + * Created by: Ton Chanh Le (chanhle@comp.nus.edu.sg) + * Adapted from Benghazi_true-termination.c + */ + +typedef enum {false, true} bool; + +extern int __VERIFIER_nondet_int(void); + +int main() +{ + int x, d1, d2, d1old; + x = __VERIFIER_nondet_int(); + d1 = __VERIFIER_nondet_int(); + d2 = __VERIFIER_nondet_int(); + while (x >= 0) { + x = x - d1; + d1old = d1; + d1 = d2 + 1; + d2 = d1old + 1; + } + return 0; +} diff --git a/vdiff/assets/test/typecheck/newton_1_3_true-unreach-call_true-termination.c b/vdiff/assets/test/typecheck/newton_1_3_true-unreach-call_true-termination.c new file mode 100644 index 0000000..fd8bd5a --- /dev/null +++ b/vdiff/assets/test/typecheck/newton_1_3_true-unreach-call_true-termination.c @@ -0,0 +1,58 @@ +extern void __VERIFIER_error(void); +extern void __VERIFIER_assume(int); +extern float __VERIFIER_nondet_float(void); + +#define NR 3 + +#if NR == 1 +#define VAL 0.2f +#elif NR == 2 +#define VAL 0.4f +#elif NR == 3 +#define VAL 0.6f +#elif NR == 4 +#define VAL 0.8f +#elif NR == 5 +#define VAL 1.0f +#elif NR == 6 +#define VAL 1.2f +#elif NR == 7 +#define VAL 1.4f +#elif NR == 8 +#define VAL 2.0f +#endif + +#define ITERATIONS 1 + +#if !(ITERATIONS >= 1 && ITERATIONS <= 3) +#error Number of iterations must be between 1 and 3 +#endif + +float f(float x) +{ + return x - (x*x*x)/6.0f + (x*x*x*x*x)/120.0f + (x*x*x*x*x*x*x)/5040.0f; +} + +float fp(float x) +{ + return 1 - (x*x)/2.0f + (x*x*x*x)/24.0f + (x*x*x*x*x*x)/720.0f; +} + +int main() +{ + float IN = __VERIFIER_nondet_float(); + __VERIFIER_assume(IN > -VAL && IN < VAL); + + float x = IN - f(IN)/fp(IN); +#if ITERATIONS > 1 + x = x - f(x)/fp(x); +#if ITERATIONS > 2 + x = x - f(x)/fp(x); +#endif +#endif + + if(!(x < 0.1)) + __VERIFIER_error(); + + return 0; +} diff --git a/vdiff/assets/test/typecheck/standard_copy9_true-unreach-call_ground.i b/vdiff/assets/test/typecheck/standard_copy9_true-unreach-call_ground.i new file mode 100644 index 0000000..a3287ed --- /dev/null +++ b/vdiff/assets/test/typecheck/standard_copy9_true-unreach-call_ground.i @@ -0,0 +1,52 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(); +int main( ) { + int a1[100000]; + int a2[100000]; + int a3[100000]; + int a4[100000]; + int a5[100000]; + int a6[100000]; + int a7[100000]; + int a8[100000]; + int a9[100000]; + int a0[100000]; + int a; + for ( a = 0 ; a < 100000 ; a++ ) { + a1[a] = __VERIFIER_nondet_int(); + } + int i; + for ( i = 0 ; i < 100000 ; i++ ) { + a2[i] = a1[i]; + } + for ( i = 0 ; i < 100000 ; i++ ) { + a3[i] = a2[i]; + } + for ( i = 0 ; i < 100000 ; i++ ) { + a4[i] = a3[i]; + } + for ( i = 0 ; i < 100000 ; i++ ) { + a5[i] = a4[i]; + } + for ( i = 0 ; i < 100000 ; i++ ) { + a6[i] = a5[i]; + } + for ( i = 0 ; i < 100000 ; i++ ) { + a7[i] = a6[i]; + } + for ( i = 0 ; i < 100000 ; i++ ) { + a8[i] = a7[i]; + } + for ( i = 0 ; i < 100000 ; i++ ) { + a9[i] = a8[i]; + } + for ( i = 0 ; i < 100000 ; i++ ) { + a0[i] = a9[i]; + } + int x; + for ( x = 0 ; x < 100000 ; x++ ) { + __VERIFIER_assert( a1[x] == a0[x] ); + } + return 0; +} diff --git a/vdiff/assets/test/typecheck/sum10_true-unreach-call_true-termination.c b/vdiff/assets/test/typecheck/sum10_true-unreach-call_true-termination.c new file mode 100644 index 0000000..f04ad25 --- /dev/null +++ b/vdiff/assets/test/typecheck/sum10_true-unreach-call_true-termination.c @@ -0,0 +1,57 @@ +/* + * Benchmarks used in the paper "Commutativity of Reducers" + * which was published at TACAS 2015 and + * written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang. + * http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9 + * + * We checks if a function is "deterministic" w.r.t. all possible permutations + * of an input array. Such property is desirable for reducers in the + * map-reduce programming model. It ensures that the program always computes + * the same results on the same input data set. + */ + +#define N 10 +#define fun sum + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern int __VERIFIER_nondet_int(); + +int sum (int x[N]) +{ + int i; + long long ret; + ret = 0; + for (i = 0; i < N; i++) { + ret = ret + x[i]; + } + return ret; +} + +int main () +{ + int x[N]; + int temp; + int ret; + int ret2; + int ret5; + + for (int i = 0; i < N; i++) { + x[i] = __VERIFIER_nondet_int(); + } + + ret = fun(x); + + temp=x[0];x[0] = x[1]; x[1] = temp; + ret2 = fun(x); + temp=x[0]; + for(int i =0 ; i GB + +typechecker :: Parser TypecheckerFlag +typechecker = option tc (long "typechecker" <> value DefaultTypechecker) + where + tc = str >>= \case + "default" -> return DefaultTypechecker + "simple" -> return SimpleTypechecker + -- | The verifier list is a space separated list of verifiers. A verifier can be indicated by either: -- * its name, e.g. @smack@ -- * its name with a combination of parameters @smack(--loop-unroll=1)@ diff --git a/vdiff/src/VDiff/Diff.hs b/vdiff/src/VDiff/Diff.hs index c541b70..77aa004 100644 --- a/vdiff/src/VDiff/Diff.hs +++ b/vdiff/src/VDiff/Diff.hs @@ -26,14 +26,15 @@ import VDiff.ArithmeticExpressions (evalExpr) import VDiff.Data import VDiff.Execute import VDiff.Instrumentation +import VDiff.SimpleTypecheck (simpleTypechecker) import VDiff.Strategy import VDiff.Util.ResourcePool import VDiff.Verifier -cmdDiff :: HasMainEnv a => Maybe Int -> DiffParameters -> RIO a () -cmdDiff seed params = do +cmdDiff :: HasMainEnv a => TypecheckerFlag -> Maybe Int -> DiffParameters -> RIO a () +cmdDiff tcFlag seed params = do logInfo "starting diff" s <- case seed of @@ -42,8 +43,7 @@ cmdDiff seed params = do logInfo $ "seed for random generator: " <> display s liftIO $ setStdGen $ mkStdGen s - - mAst <- openCFile (params ^. inputFile) + mAst <- openCFile tcFlag (params ^. inputFile) case mAst of Nothing -> liftIO exitFailure Just ast -> do @@ -54,21 +54,21 @@ cmdDiff seed params = do -- | parses the file, runs the semantic analysis (type checking), and pretty-prints the resulting semantic AST. -- Use this to test the modified language-c-extensible library. -cmdParseTest :: HasLogFunc env => FilePath -> RIO env () -cmdParseTest fn = openCFile fn >>= \case +cmdParseTest :: HasLogFunc env => TypecheckerFlag -> FilePath -> RIO env () +cmdParseTest tc fn = openCFile tc fn >>= \case Nothing -> liftIO exitFailure Just ast -> liftIO $ putStrLn $ render $ pretty ast -cmdMarkReads :: HasLogFunc env => SearchMode -> FilePath -> RIO env () -cmdMarkReads mode fn = do +cmdMarkReads :: HasLogFunc env => SearchMode -> TypecheckerFlag -> FilePath -> RIO env () +cmdMarkReads mode tc fn = do logDebug $ "mode is " <> display (tshow mode) - (Just ast) <- openCFile fn + (Just ast) <- openCFile tc fn let ast' = markAllReads mode ast liftIO . putStrLn . render . pretty $ ast' cmdVersions :: RIO a () -cmdVersions = liftIO $ forM_ (sortBy (comparing (^. name)) allVerifiers) $ \verifier -> do +cmdVersions = liftIO $ forM_ (L.sortOn (^. name) allVerifiers) $ \verifier -> do T.putStr $ verifier ^. name putStr ": " sv <- try (verifier ^. version) >>= \case diff --git a/vdiff/src/VDiff/Instrumentation.hs b/vdiff/src/VDiff/Instrumentation.hs index 1d0dbe1..fecbab6 100644 --- a/vdiff/src/VDiff/Instrumentation.hs +++ b/vdiff/src/VDiff/Instrumentation.hs @@ -9,6 +9,7 @@ module VDiff.Instrumentation ( -- * Handling C files openCFile + , defaultTypechecker , preprocess , maskAsserts , defineAssert @@ -55,15 +56,27 @@ import UnliftIO.Directory import VDiff.Instrumentation.Browser import qualified VDiff.Instrumentation.Fragments as Fragments import VDiff.Instrumentation.Reads +import VDiff.SimpleTypecheck +defaultTypechecker :: Typechecker +defaultTypechecker tu = runTrav_ (analyseAST tu) -- | short-hand for open, parse and type annotate, will log parse and type checking errors and warnings. -openCFile :: HasLogFunc env => FilePath -> RIO env (Maybe TU) -openCFile fn = do +openCFile :: HasLogFunc env => TypecheckerFlag -> FilePath -> RIO env (Maybe TU) +openCFile tcFlag fn = do -- we need GCC to remove preprocessor tokens and comments, -- unfortunately, GCC only works on files with .c ending. Hence this hack. let templateName = takeFileName $ replaceExtension fn ".c" + + typechecker <- case tcFlag of + DefaultTypechecker -> do + logInfo "using default typechecker (language-c)" + return defaultTypechecker + SimpleTypechecker -> do + logInfo "using simple typechecker" + return simpleTypechecker + withSystemTempFile templateName $ \fnC _ -> do copyFile fn fnC x <- liftIO $ parseCFile (newGCC "gcc") Nothing [] fnC @@ -71,7 +84,7 @@ openCFile fn = do Left parseError -> do logError $ "parse error: " <> displayShow parseError return Nothing - Right tu -> case runTrav_ (analyseAST tu) of + Right tu -> case typechecker tu of Left typeError -> do logError $ "type error: " <> displayShow typeError return Nothing diff --git a/vdiff/src/VDiff/Prelude/Types.hs b/vdiff/src/VDiff/Prelude/Types.hs index 3f8f5a9..e082ddf 100644 --- a/vdiff/src/VDiff/Prelude/Types.hs +++ b/vdiff/src/VDiff/Prelude/Types.hs @@ -32,7 +32,8 @@ import qualified Database.SQLite.Simple as SQL import Docker.Client (MemoryConstraint) import Language.C hiding (LevelError, LevelWarn, execParser) -import Language.C.Analysis.AstAnalysis2 +import Language.C.Analysis.AstAnalysis2 (analyseAST, getType, + maybeM) import Language.C.Analysis.SemRep hiding (Stmt) import Language.C.Analysis.TypeUtils (voidType) import Language.C.Data.Lens @@ -54,6 +55,11 @@ data Strategy = RandomWalkStrategy data SearchMode = IdentOnly | Subexpressions deriving Show +type Typechecker = CTranslationUnit NodeInfo -> Either [CError] ((CTranslationUnit SemPhase), [CError]) + + +data TypecheckerFlag = DefaultTypechecker | SimpleTypechecker + type Microseconds = Int -- | Every verifier is supposed to run in this environment diff --git a/vdiff/src/VDiff/SimpleTypecheck.hs b/vdiff/src/VDiff/SimpleTypecheck.hs new file mode 100644 index 0000000..e79d166 --- /dev/null +++ b/vdiff/src/VDiff/SimpleTypecheck.hs @@ -0,0 +1,595 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiWayIf #-} +-- I don't care about GNU extensions, so statements are always of type void + +module VDiff.SimpleTypecheck + ( simpleTypechecker + ) where + +import Control.Monad.Except +import Control.Monad.State +import Data.Coerce +import qualified Data.Map as Map +import Language.C.Analysis.SemRep hiding (constant) +import qualified Prelude as P +import VDiff.Prelude hiding (declarator, expression, + externalDeclaration, + functionDefinition, + translationUnit) + +return' a = Right (a, []) + + +data Scope + = Scope + { variables :: Map Ident Type + , typedefs :: Map Ident Type + } deriving (Show) + +addVarToScope :: Ident -> Type -> Scope -> Scope +addVarToScope n ty s = s { variables = Map.insert n ty (variables s)} +addTypedefToScope :: Ident -> Type -> Scope -> Scope +addTypedefToScope n decls s = s { typedefs = Map.insert n decls (typedefs s) } + + +data AnalysisState = AnalysisState + { scope :: Scope + , structures :: Map.Map Ident (Map.Map Ident Type) + } deriving (Show) + +newtype AnalysisM a + = AnalysisM + { unAnalysisM :: StateT Scope (Except [CError]) a + } deriving (Functor, Applicative, Monad) + +getScope :: AnalysisM Scope +getScope = AnalysisM get + +putScope :: Scope -> AnalysisM () +putScope s = AnalysisM (put s) + +defaultScope :: Scope +defaultScope = Scope Map.empty Map.empty + +declare :: Ident -> Type -> AnalysisM () +declare n ty = do + traceM $ "declaring " <> tshow (identToString n) <> " :: " <> tshow ty + s <- getScope + let s' = addVarToScope n ty s + putScope s' + +-- This one will never throw an error. If it is not found it returns the "int" as type +lookupVar :: Ident -> AnalysisM Type +lookupVar n = do + s <- getScope + case Map.lookup n (variables s) of + Nothing -> trace ("failed lookup for " <> tshow (identToString n)) $ return simpleInt + Just ty -> return ty + +lookupTypedef :: Ident -> AnalysisM Type +lookupTypedef n = do + s <- getScope + case Map.lookup n (typedefs s) of + Nothing -> trace ("failed lookup for " <> tshow (identToString n)) $ return simpleInt + Just ty -> return ty + +-- enters a new scope, names declared inside will not be declared outside +enterScope :: AnalysisM a -> AnalysisM a +enterScope action = do + s <- getScope + x <- action + putScope s + return x + +simpleTypechecker :: Typechecker +simpleTypechecker tu = case runExcept (runStateT (unAnalysisM (translationUnit tu)) defaultScope) of + Left errs -> Left errs + Right (a,_) -> Right (a,[]) + +-- | annotate every expression with type "int" +translationUnit :: CTranslationUnit NodeInfo -> AnalysisM (CTranslationUnit SemPhase) +translationUnit (CTranslUnit declrs ni) = CTranslUnit <$> mapM externalDeclaration declrs <*> pure ni + + +externalDeclaration :: CExternalDeclaration NodeInfo -> AnalysisM (CExternalDeclaration SemPhase) +externalDeclaration (CDeclExt declr) = CDeclExt <$> declaration declr +externalDeclaration (CFDefExt fdef ) = CFDefExt <$> functionDefinition fdef +externalDeclaration (CAsmExt blk ni) = fail "ASM blocks not implemented" + +functionDefinition :: CFunctionDef NodeInfo -> AnalysisM (CFunctionDef SemPhase) +functionDefinition (CFunDef specs declr oldStyleParams body ni) = do + specs' <- mapM declarationSpecifier specs + (f, n,ty) <- enterScope $ do + declr' <- declarator declr + Just (n,ty) <- calculateTypeOfDeclarator specs' declr' + oldStyleParams' <- mapM declaration oldStyleParams + body' <- statement body + return (CFunDef specs' declr' oldStyleParams' body' ni, n, ty) + declare n ty + return f + +declaration :: CDeclaration NodeInfo -> AnalysisM (CDeclaration SemPhase) +declaration (CStaticAssert expr lit ni) = fail "static asserts not implemented" +declaration (CDecl specs initDeclrs ni) = do + specs' <- mapM declarationSpecifier specs + initDeclrs' <- mapM initializedDeclarator initDeclrs + forM_ initDeclrs' $ \(mdeclr,_,_) -> + case mdeclr of + Just declr -> do + calculateTypeOfDeclarator specs' declr >>= \case + Just (n,ty) -> declare n ty + Nothing -> return () + _ -> return () + + return $ CDecl specs' initDeclrs' ni + +calculateTypeOfDeclarator :: [CDeclarationSpecifier SemPhase] -> CDeclarator SemPhase -> AnalysisM (Maybe (Ident, Type)) +calculateTypeOfDeclarator specs (CDeclr (Just n) derived _ _ _) = do + start <- calculateTypeFromSpecs (getTypeSpecs specs) + let ty = foldF (map analyseDerivedDeclarator derived) start + return $ Just (n, ty) +calculateTypeOfDeclarator specs (CDeclr Nothing derived _ _ _) = return Nothing + + +-- apply a bunch a functions sequentially. +foldF :: [a -> a] -> a -> a +foldF [] x = x +foldF (f:fs) x = f (foldF fs x) + + +getTypeSpecs :: [CDeclarationSpecifier a] -> [CTypeSpecifier a] +getTypeSpecs = (\(_,_,_,x,_,_) -> x) . partitionDeclSpecs + +calculateTypeFromSpecs :: [CTypeSpecifier SemPhase] -> AnalysisM Type +calculateTypeFromSpecs specs = do + specs' <- mapM analyseTypeSpecifier specs + return $ f specs' + where + f [] = trace "defaulting to int" $ simpleInt + f [Left ty] = ty + f (Right fty : l) = fty (f l) + f _ = trace "oops" $ simpleInt + + +-- turns a 'DerivedDeclarator' into a function that transforms the type. E.g. +-- Given a @CPtrDeclr []@, this turns into a function that turns a type T into +-- the type *T. +-- TODO: I'm ignoring TypeQuals here +analyseDerivedDeclarator :: CDerivedDeclarator SemPhase -> Type -> Type +analyseDerivedDeclarator (CPtrDeclr quals _) t = PtrType t noTypeQuals [] +analyseDerivedDeclarator (CFunDeclr x attrs ni) t = + case x of + Left ns -> FunctionType (FunType t [] False) noAttributes + Right (params,b) -> FunctionType (FunType t [] b) noAttributes + +analyseDerivedDeclarator (CArrDeclr _ _ _ ) t = ArrayType t (UnknownArraySize False) noTypeQuals noAttributes -- TODO + +analyseTypeSpecifier :: CTypeSpecifier SemPhase -> AnalysisM (Either Type (Type -> Type)) +analyseTypeSpecifier (CVoidType _) = return $ Left $ DirectType TyVoid noTypeQuals noAttributes +analyseTypeSpecifier (CCharType _) = return $ Left $ DirectType (TyIntegral TyChar) noTypeQuals noAttributes +analyseTypeSpecifier (CIntType _) = return $ Left $ DirectType (TyIntegral TyInt) noTypeQuals noAttributes +analyseTypeSpecifier (CShortType _) = return $ Left $ DirectType (TyIntegral TyShort) noTypeQuals noAttributes +-- long is a little special as it can also be combined with others +analyseTypeSpecifier (CLongType _) = return $ Left $ DirectType (TyIntegral TyLong) noTypeQuals noAttributes + +analyseTypeSpecifier (CFloatType _) = return $ Left $ DirectType (TyFloating TyFloat) noTypeQuals noAttributes +analyseTypeSpecifier (CFloat128Type _) = return $ Left $ DirectType (TyFloating TyFloat128) noTypeQuals noAttributes +analyseTypeSpecifier (CDoubleType _ ) = return $ Left $ DirectType (TyFloating TyDouble) noTypeQuals noAttributes +analyseTypeSpecifier (CSignedType _ ) = return $ Right id +analyseTypeSpecifier (CUnsigType _ ) = return $ Right unsignType +analyseTypeSpecifier (CBoolType _ ) = return $ Left $ DirectType (TyIntegral TyBool) noTypeQuals noAttributes +analyseTypeSpecifier (CComplexType _) = return $ undefined +analyseTypeSpecifier (CInt128Type _) = return $ undefined + +analyseTypeSpecifier (CSUType sue _) = do + let (CStruct tag mi mdecls attrs ni) = sue + let sueRef = case mi of + Nothing -> NamedRef (internalIdent "someEnum") + Just i -> NamedRef i + let compType = case tag of + CStructTag -> StructTag + CUnionTag -> UnionTag + return $ Left $ DirectType (TyComp $ CompTypeRef sueRef compType ni) noTypeQuals noAttributes + +analyseTypeSpecifier (CEnumType enum ni) = do + let (CEnum mi ml attrs enumNi) = enum + let sueRef = case mi of + Nothing -> NamedRef (internalIdent "someEnum") + Just i -> NamedRef i + return $ Left $ DirectType (TyEnum (EnumTypeRef sueRef ni) ) noTypeQuals noAttributes +analyseTypeSpecifier (CTypeDef n _) = do + ty <- lookupTypedef n + return $ Left ty +analyseTypeSpecifier (CTypeOfExpr expr _) = return $ Left $ getType expr +analyseTypeSpecifier (CTypeOfType decl _) = return $ undefined +analyseTypeSpecifier (CAtomicType decl _) = return $ undefined + + + + +initializedDeclarator :: (Maybe (CDeclarator NodeInfo), Maybe (CInitializer NodeInfo), Maybe (CExpression NodeInfo)) + -> AnalysisM (Maybe (CDeclarator SemPhase), Maybe (CInitializer SemPhase), Maybe (CExpression SemPhase)) +initializedDeclarator (md, mi, me) = do + md' <- maybeM declarator md + mi' <- maybeM initializer mi + me' <- maybeM expression me + return (md', mi', me') + +initializer :: CInitializer NodeInfo -> AnalysisM (CInitializer SemPhase) +initializer (CInitExpr e ni) = CInitExpr <$> expression e <*> pure ni +initializer (CInitList iniList ni) = CInitList <$> mapM initPart iniList <*> pure ni + where + initPart :: ([CPartDesignator NodeInfo], CInitializer NodeInfo) -> AnalysisM ([CPartDesignator SemPhase], CInitializer SemPhase) + initPart (prts, init) = do + prts' <- mapM partDesignator prts + init' <- initializer init + return (prts', init') + partDesignator (CArrDesig e ni) = CArrDesig <$> expression e <*> pure ni + partDesignator (CMemberDesig n ni) = return $ CMemberDesig n ni + partDesignator (CRangeDesig e1 e2 ni) = CRangeDesig <$> expression e1 <*> expression e2 <*> pure ni + + +declarationSpecifier :: CDeclarationSpecifier NodeInfo -> AnalysisM (CDeclarationSpecifier SemPhase) +declarationSpecifier (CStorageSpec sspec) = CStorageSpec <$> storageSpecifier sspec +declarationSpecifier (CTypeSpec tspec) = CTypeSpec <$> typeSpecifier tspec +declarationSpecifier (CFunSpec fspec) = CFunSpec <$> functionSpecifier fspec +declarationSpecifier (CTypeQual tqual) = CTypeQual <$> typeQualifier tqual +declarationSpecifier (CAlignSpec aspec) = CAlignSpec <$> alignmentSpecifier aspec + +functionSpecifier :: CFunctionSpecifier NodeInfo -> AnalysisM (CFunctionSpecifier SemPhase) +functionSpecifier (CInlineQual ni) = return $ CInlineQual ni +functionSpecifier (CNoreturnQual ni) = return $ CNoreturnQual ni + +storageSpecifier :: CStorageSpecifier NodeInfo -> AnalysisM (CStorageSpecifier SemPhase) +storageSpecifier (CAuto ni) = return $ CAuto ni +storageSpecifier (CRegister ni) = return $ CRegister ni +storageSpecifier (CStatic ni) = return $ CStatic ni +storageSpecifier (CExtern ni) = return $ CExtern ni +storageSpecifier (CTypedef ni) = return $ CTypedef ni +storageSpecifier (CThread ni) = return $ CThread ni + +alignmentSpecifier :: CAlignmentSpecifier NodeInfo -> AnalysisM (CAlignmentSpecifier SemPhase) +alignmentSpecifier (CAlignAsType decl ni) = CAlignAsType <$> declaration decl <*> pure ni +alignmentSpecifier (CAlignAsExpr e ni) = CAlignAsExpr <$> expression e <*> pure ni + +typeSpecifier :: CTypeSpecifier NodeInfo -> AnalysisM (CTypeSpecifier SemPhase) +typeSpecifier (CVoidType ni) = return $ CVoidType ni +typeSpecifier (CCharType ni) = return $ CCharType ni +typeSpecifier (CShortType ni) = return $ CShortType ni +typeSpecifier (CIntType ni) = return $ CIntType ni +typeSpecifier (CLongType ni) = return $ CLongType ni +typeSpecifier (CFloatType ni) = return $ CFloatType ni +typeSpecifier (CFloat128Type ni) = return $ CFloat128Type ni +typeSpecifier (CDoubleType ni) = return $ CDoubleType ni +typeSpecifier (CSignedType ni) = return $ CSignedType ni +typeSpecifier (CUnsigType ni) = return $ CUnsigType ni +typeSpecifier (CBoolType ni) = return $ CBoolType ni +typeSpecifier (CComplexType ni) = return $ CComplexType ni +typeSpecifier (CInt128Type ni) = return $ CInt128Type ni +typeSpecifier (CSUType strun ni) = CSUType <$> structOrUnion strun <*> pure ni +typeSpecifier (CEnumType enum ni) = CEnumType <$> enumeration enum <*> pure ni +typeSpecifier (CTypeDef n ni) = return $ CTypeDef n ni +typeSpecifier (CTypeOfExpr e ni) = CTypeOfExpr <$> expression e <*> pure ni +typeSpecifier (CTypeOfType decl ni) = CTypeOfType <$> declaration decl <*> pure ni +typeSpecifier (CAtomicType decl ni) = CAtomicType <$> declaration decl <*> pure ni + + +enumeration (CEnum mi elems attrs ni) = CEnum mi <$> maybeM enumElements elems <*> mapM attribute attrs <*> pure ni + where + enumElements = mapM enumElement + enumElement (n, Nothing) = return (n, Nothing) + enumElement (n, Just e) = do + e' <- expression e + return (n, Just e') + +structOrUnion :: CStructureUnion NodeInfo -> AnalysisM (CStructureUnion SemPhase) +structOrUnion (CStruct tag mi mdecls attrs ni) = do + mdecls' <- maybeM (mapM declaration) mdecls + attrs' <- mapM attribute attrs + return $ CStruct tag mi mdecls' attrs' ni + +declarator :: CDeclarator NodeInfo -> AnalysisM (CDeclarator SemPhase) +declarator (CDeclr mi derivedDeclrs mAsm attrs ni) = do + derivedDeclrs' <- mapM derivedDeclarator derivedDeclrs + attrs' <- mapM attribute attrs + mAsm' <- maybeM stringLiteral mAsm + return $ CDeclr mi derivedDeclrs' Nothing attrs' ni + + +stringLiteral :: CStringLiteral NodeInfo -> AnalysisM (CStringLiteral SemPhase) +stringLiteral (CStrLit s ni) = return $ CStrLit s ni + +derivedDeclarator :: CDerivedDeclarator NodeInfo -> AnalysisM (CDerivedDeclarator SemPhase) +derivedDeclarator (CPtrDeclr typequals ni) = CPtrDeclr <$> mapM typeQualifier typequals <*> pure ni +derivedDeclarator (CArrDeclr typequals arrsize ni) = CArrDeclr <$> mapM typeQualifier typequals <*> arraySize arrsize <*> pure ni +derivedDeclarator (CFunDeclr (Left ns) attrs ni) = do + attrs' <- mapM attribute attrs + return $ CFunDeclr (Left ns) attrs' ni + +derivedDeclarator (CFunDeclr (Right (decls,b)) attrs ni) = do + decls' <- mapM declaration decls + attrs' <- mapM attribute attrs + return $ CFunDeclr (Right (decls', b)) attrs' ni + +typeQualifier :: CTypeQualifier NodeInfo -> AnalysisM (CTypeQualifier SemPhase) +typeQualifier(CConstQual ni) = return $ CConstQual ni +typeQualifier(CVolatQual ni) = return $ CVolatQual ni +typeQualifier(CRestrQual ni) = return $ CRestrQual ni +typeQualifier(CAtomicQual ni) = return $ CAtomicQual ni +typeQualifier(CAttrQual attr) = CAttrQual <$> attribute attr +typeQualifier(CNullableQual ni) = return $ CNullableQual ni +typeQualifier(CNonnullQual ni) = return $ CNonnullQual ni + +arraySize :: CArraySize NodeInfo -> AnalysisM (CArraySize SemPhase) +arraySize (CNoArrSize b) = return $ CNoArrSize b +arraySize (CArrSize b e) = CArrSize b <$> expression e + +attribute :: CAttribute NodeInfo -> AnalysisM (CAttribute SemPhase) +attribute (CAttr i exprs ni) = CAttr i <$> mapM expression exprs <*> pure ni + +statement :: CStatement NodeInfo -> AnalysisM (CStatement SemPhase) +statement (CLabel lbl stmt attrs ni) = do + stmt' <- statement stmt + attrs' <- mapM attribute attrs + return $ CLabel lbl stmt' attrs' (ni, getType stmt') + +statement (CCase e stmt ni) = CCase <$> expression e <*> statement stmt <*> pure (ni, voidType) +statement (CCases e1 e2 stmt ni) = CCases <$> expression e1 <*> expression e2 <*> statement stmt <*> pure (ni, voidType) +statement (CDefault stmt ni) = CDefault <$> statement stmt <*> pure (ni, voidType) +statement (CExpr me ni) = + case me of + Nothing -> return $ CExpr Nothing (ni, voidType) + Just e -> do + e' <- expression e + return $ CExpr (Just e') (ni, getType e') + +statement (CCompound ns blkItems ni) = do + blkItems' <- forM blkItems $ \case + CBlockStmt stmt -> CBlockStmt <$> statement stmt + CBlockDecl decl -> CBlockDecl <$> declaration decl + CNestedFunDef fdef -> CNestedFunDef <$> functionDefinition fdef + return $ CCompound ns blkItems' (ni, voidType) + +statement (CIf e thenStmt mElseStmt ni) = do + e' <- expression e + thenStmt' <- statement thenStmt + mElseStmt' <- maybeM statement mElseStmt + return $ CIf e' thenStmt' mElseStmt' (ni, voidType) + + +statement (CSwitch e stmt ni) = do + e' <- expression e + stmt' <- statement stmt + return $ CSwitch e' stmt' (ni, voidType) + +statement (CWhile e stmt b ni) = do + e' <- expression e + stmt' <- statement stmt + return $ CWhile e' stmt' b (ni, voidType) + +statement (CFor initOrDecl me1 me2 stmt ni) = do + initOrDecl' <- case initOrDecl of + Left me -> Left <$> maybeM expression me + Right decl -> Right <$> declaration decl + me1' <- maybeM expression me1 + me2' <- maybeM expression me2 + stmt' <- statement stmt + return $ CFor initOrDecl' me1' me2' stmt' (ni, voidType) + +statement (CGoto n ni) = return $ CGoto n (ni, voidType) +statement (CGotoPtr e ni) = CGotoPtr <$> expression e <*> pure (ni, voidType) +statement (CCont ni) = return $ CCont (ni, voidType) +statement (CBreak ni) = return $ CBreak (ni, voidType) +statement (CReturn me ni) = do + me' <- case me of + Nothing -> return Nothing + Just e -> Just <$> expression e + return $ CReturn me' (ni, voidType) +statement (CAsm asmStmt ni) = undefined + + +expression :: CExpression NodeInfo -> AnalysisM (CExpression SemPhase) +expression (CComma exprs ni) = do + exprs' <- mapM expression exprs + let ty = getType (P.head exprs') + return $ CComma exprs' (ni, ty) + +expression (CAssign op e1 e2 ni) = do + e1' <- expression e1 + e2' <- expression e2 + return $ CAssign op e1' e2' (ni, getType e1') + +expression (CCond e1 me2 e3 ni) = do + e1' <- expression e1 + me2' <- case me2 of + Just e2 -> Just <$> expression e2 + Nothing -> return Nothing + e3' <- expression e3 + return $ CCond e1' me2' e3' (ni, getType e1') + +expression (CBinary op e1 e2 ni) = do + e1' <- expression e1 + e2' <- expression e2 + ty <- if + | isBooleanOp op -> return simpleInt -- TODO: Make this a 'int refined to bool' + | otherwise -> unifyArithmetic [getType e1', getType e2'] + return $ CBinary op e1' e2' (ni, ty) + +expression (CCast decl e ni) = CCast <$> declaration decl <*> expression e <*> pure (ni, voidType) -- TODO: wrong type +expression (CUnary op e ni) = do + e' <- expression e + return $ CUnary op e' (ni, getType e') -- TODO: Check for casting from boolean to int? + +expression (CSizeofExpr e ni) = CSizeofExpr <$> expression e <*> pure (ni, simpleInt) + +expression (CSizeofType decl ni) = CSizeofType <$> declaration decl <*> pure (ni, simpleInt) + +expression (CAlignofExpr e ni) = CAlignofExpr <$> expression e <*> pure (ni, simpleInt) + +expression (CAlignofType decl ni) = CAlignofType <$> declaration decl <*> pure (ni, simpleInt) + +expression (CComplexReal e ni) = CComplexReal <$> expression e <*> pure (ni, voidType) -- TODO + +expression (CComplexImag e ni) = CComplexImag <$> expression e <*> pure (ni, voidType) -- TODO + +expression (CIndex e1 e2 ni) = do + e1' <- expression e1 + e2' <- expression e2 + ty <- applyIndexType (getType e1') (getType e2') + return $ CIndex e1' e2' (ni, ty) + +expression (CCall f ps ni) = do + f' <- expression f + ps' <- mapM expression ps + ty <- applyType (getType f') + return $ CCall f' ps' (ni, ty) + +expression (CMember e n b ni) = do + e' <- expression e + return $ CMember e' n b (ni, simpleInt) -- TODO + +expression (CVar v ni) = do + ty <- lookupVar v + return $ CVar v (ni, ty) + +expression (CConst const) = CConst <$> constant const -- integer, character, floating point and string constants + +expression (CCompoundLit decl initList ni) = undefined -- a C99 compound literal +expression (CGenericSelection e ml ni) = undefined -- a C11 generic selection +expression (CStatExpr stmt ni) = do + stmt' <- statement stmt + return $ CStatExpr stmt' (ni, getType stmt') +expression (CLabAddrExpr n ni) = undefined -- a GNU C address of label +expression (CBuiltinExpr builtin) = CBuiltinExpr <$> builtinThing builtin + +constant :: CConstant NodeInfo -> AnalysisM (CConstant SemPhase) +constant (CIntConst c ni) = return $ CIntConst c (ni, simpleInt) +constant (CCharConst c ni) = return $ CCharConst c (ni, charType) +constant (CFloatConst c ni) = return $ CFloatConst c (ni, floatType) +constant (CStrConst c ni) = return $ CStrConst c (ni, stringType) + + +builtinThing :: CBuiltinThing NodeInfo -> AnalysisM (CBuiltinThing SemPhase) +builtinThing (CBuiltinVaArg e decl ni) = do + e' <- expression e + decl' <- declaration decl + return $ CBuiltinVaArg e' decl' ni -- TODO: those things should have a type probably +builtinThing (CBuiltinOffsetOf decl prts ni) = undefined +builtinThing (CBuiltinTypesCompatible decl1 decl2 ni) = undefined +builtinThing (CBuiltinConvertVector e decl ni) = undefined + +-- unifies the given types +unify :: [Type] -> AnalysisM Type +unify types = return $ P.head types -- TODO: Do some unification + +-- unifies the given types +unifyArithmetic :: [Type] -> AnalysisM Type +unifyArithmetic = return . P.foldl1 unifyArithmetic' -- TODO: Do some unification, but make sure that it is numeric + where + unifyArithmetic' t u + -- choose most-precise integer type + | (Just t') <- getIntType u, (Just u') <- getIntType u = + if | integralPrecision t' < integralPrecision u' -> u + | integralPrecision t' > integralPrecision u' -> t + | isSigned t' && not (isSigned u') -> u + | not (isSigned t') && isSigned u' -> t + | otherwise -> u + -- choose most-precise float type + | (Just t') <- getFloatType t, (Just u') <- getFloatType u = + if | floatPrecision t' < floatPrecision u' -> u + | floatPrecision t' > floatPrecision u' -> t + | otherwise -> u + -- go for float if one is integral + | (Just t') <- getFloatType t, (Just u') <- getIntType u = t + | (Just t') <- getIntType t, (Just u') <- getFloatType u = u + | otherwise = error "unify arithmetic oops" + + + +-- Does not throw an error on type mismatch +applyType :: Type -> AnalysisM Type +applyType (FunctionType (FunType tyReturn _ _) attrs) = return tyReturn +applyType (FunctionType (FunTypeIncomplete tyReturn) attrs) = return tyReturn +applyType ty = do + traceM $ "Warning: applying a function of type " <> tshow ty + return simpleInt + +applyIndexType :: Type -> Type -> AnalysisM Type +applyIndexType (ArrayType ty _ _ _) _ = return ty +applyIndexType t _ = trace ("Warning: applying an index to type " <> tshow t) $ return simpleInt + + + +-- a few shortcuts + +simpleInt :: Type +simpleInt = DirectType (TyIntegral TyInt) noTypeQuals noAttributes + +charType :: Type +charType = DirectType (TyIntegral TyChar) noTypeQuals noAttributes + +floatType :: Type +floatType = DirectType (TyFloating TyFloat) noTypeQuals noAttributes + +stringType :: Type +stringType = PtrType charType noTypeQuals noAttributes + +isBooleanOp :: CBinaryOp -> Bool +isBooleanOp x = x `elem` [CGrOp, CLeOp, CLeqOp, CGeqOp, CEqOp, CNeqOp, CLndOp, CLorOp] + +unsignType :: Type -> Type +unsignType (DirectType (TyIntegral intType) quals attrs) = DirectType (TyIntegral (unsignIntType intType)) quals attrs + where + unsignIntType TyShort = TyUShort + unsignIntType TyInt = TyUInt + unsignIntType TyInt128 = TyUInt128 + unsignIntType TyLong = TyULong + unsignIntType TyLLong = TyULLong + unsignIntType TyChar = TyUChar + unsignIntType t = error $ "unsigning int type: " <> show t + +integralPrecision :: IntType -> Int +integralPrecision TyBool = 1 +integralPrecision TyChar = 8 +integralPrecision TySChar = 8 +integralPrecision TyUChar = 8 +integralPrecision TyShort = 16 +integralPrecision TyUShort = 16 +integralPrecision TyInt = 32 +integralPrecision TyUInt = 32 +integralPrecision TyInt128 = 128 +integralPrecision TyUInt128 = 128 +integralPrecision TyLong = 64 +integralPrecision TyULong = 64 +integralPrecision TyLLong = 128 +integralPrecision TyULLong = 128 + +-- the numbers don't matter, only the order +floatPrecision TyFloat = 1 +floatPrecision TyDouble = 2 +floatPrecision TyLDouble = 3 +floatPrecision TyFloat128 = 4 + +isSigned :: IntType -> Bool +isSigned TyBool = False +isSigned TyChar = False +isSigned TySChar = True +isSigned TyUChar = False +isSigned TyShort = True +isSigned TyUShort = False +isSigned TyInt = True +isSigned TyUInt = False +isSigned TyInt128 = True +isSigned TyUInt128 = False +isSigned TyLong = True +isSigned TyULong = False +isSigned TyLLong = True +isSigned TyULLong = False + +getIntType :: Type -> Maybe IntType +getIntType (DirectType (TyIntegral ty) _ _) = Just ty +getIntType _ = Nothing + +getFloatType :: Type -> Maybe FloatType +getFloatType (DirectType (TyFloating ty) _ _) = Just ty +getFloatType _ = Nothing diff --git a/vdiff/test/regression/InstrumentationProperties.hs b/vdiff/test/regression/InstrumentationProperties.hs index d497894..9a66b31 100644 --- a/vdiff/test/regression/InstrumentationProperties.hs +++ b/vdiff/test/regression/InstrumentationProperties.hs @@ -47,7 +47,7 @@ genTranslationUnit :: FilePath -> PropertyT IO (CTranslationUnit SemPhase) genTranslationUnit dir = do cFiles <- lift $ findByExtension [".c"] dir cFile <- forAll $ Gen.element cFiles - (Just tu) <- runRIO NoLogging $ openCFile cFile + (Just tu) <- runRIO NoLogging $ openCFile defaultTypechecker cFile return tu -- | test property: Any walk does not change the file diff --git a/vdiff/test/regression/Lens.hs b/vdiff/test/regression/Lens.hs index 51286ca..dd03107 100644 --- a/vdiff/test/regression/Lens.hs +++ b/vdiff/test/regression/Lens.hs @@ -17,7 +17,7 @@ testLenses = testGroup "lenses" <$> sequence [ pure testIndex testIndex :: TestTree testIndex = goldenVsString "index main" "assets/test/lenses/functions.c.golden" act where act = do - (Just ast) <- runRIO NoLogging $ openCFile "assets/test/lenses/functions.c" + (Just ast) <- runRIO NoLogging $ openCFile defaultTypechecker "assets/test/lenses/functions.c" let dummyBody = CCompound [] [CBlockStmt (dummyStmt "dummy")] (undefNode, voidType) ast' = (ix "main" . functionDefinition . body ) .~ dummyBody $ ast return $ LC8.pack $ prettyp ast' diff --git a/vdiff/test/regression/Query.hs b/vdiff/test/regression/Query.hs index 5b61a67..bb526b8 100644 --- a/vdiff/test/regression/Query.hs +++ b/vdiff/test/regression/Query.hs @@ -1,13 +1,14 @@ {-# LANGUAGE NoMonomorphismRestriction #-} -{-# LANGUAGE ParallelListComp #-} module Query (testQueries) where +import Data.List (repeat, sort) import PersistenceTestHelper +import System.IO import Test.Tasty import Test.Tasty.HUnit -import Data.List (sort, repeat) -import System.IO + +import Util import Database.Beam import VDiff.Data @@ -16,10 +17,6 @@ import VDiff.Prelude import qualified VDiff.Query2 as Q2 -assertListEqual :: HasCallStack => (Eq a, Show a) => [a] -> [a] -> IO () -assertListEqual l r - | length l == length r = sequence_ [assertEqual ("at index " ++ show i ++ " equal") x y | x <- l | y <- r | i <- [0..]] - | otherwise = assertFailure "list of unequal length cannot be equal" testQueries :: TestTree testQueries = testGroup "Query" @@ -68,6 +65,7 @@ testAllFindings = testCase "allFindings" $ withTestEnv $ do ] liftIO $ assertListEqual (sort expected) (sort fs) + testIncompleteFindings :: TestTree testIncompleteFindings = testCase "incompleteFindings" $ withTestEnv $ do runBeam $ do diff --git a/vdiff/test/regression/Regression.hs b/vdiff/test/regression/Regression.hs index bf39122..a617016 100644 --- a/vdiff/test/regression/Regression.hs +++ b/vdiff/test/regression/Regression.hs @@ -10,6 +10,7 @@ import TimedTest import Persistence import Query +import SimpleTypeCheck import Strategy.Common @@ -28,6 +29,7 @@ constructTree = do , pure testCommon , pure testPersistence , pure testQueries + , testSimpleTypecheck ] return $ testGroup "vdiff" tree diff --git a/vdiff/test/regression/SimpleTypeCheck.hs b/vdiff/test/regression/SimpleTypeCheck.hs new file mode 100644 index 0000000..3813816 --- /dev/null +++ b/vdiff/test/regression/SimpleTypeCheck.hs @@ -0,0 +1,43 @@ +module SimpleTypeCheck where + +import Test.Tasty +import Test.Tasty.Golden +import Test.Tasty.HUnit +import VDiff.Prelude + +import Util + +import Data.Generics.Uniplate.Operations +import Language.C.Analysis.SemRep +import VDiff.Instrumentation +import VDiff.SimpleTypecheck + +testSimpleTypecheck :: IO TestTree +testSimpleTypecheck = do + ts <- sequence [testAgainstDefault] + return $ testGroup "simple typecheck" ts + + + +testAgainstDefault :: IO TestTree +testAgainstDefault = do + fs <- findByExtension [".c"] "assets/test/typecheck" + return $ testGroup "against default" [runTest f | f <- fs] + where + runTest cf = testCase cf $ runRIO NoLogging $ + openCFile defaultTypechecker cf >>= \case + Nothing -> traceM "okay, even the default cannot check it" + Just defAst -> do + (Just simpleAst) <- openCFile simpleTypechecker cf + -- since we are only interested in expressions, we only compare expressions + liftIO $ assertListEqualWith equalExpr (getExpressions defAst) (getExpressions simpleAst) + +equalExpr :: CExpression SemPhase -> (String, Text) +equalExpr e = (prettyp e, simplifyType (getType e)) + where + simplifyType (FunctionType (FunType ty _ _) _) = " * -> " <> tshow ty + simplifyType (FunctionType (FunTypeIncomplete ty) _) = " * -> " <> tshow ty + simplifyType x = tshow x + +getExpressions :: TU -> [CExpression SemPhase] +getExpressions = universeBi diff --git a/vdiff/test/regression/Util.hs b/vdiff/test/regression/Util.hs index 5ec5965..e5538e0 100644 --- a/vdiff/test/regression/Util.hs +++ b/vdiff/test/regression/Util.hs @@ -1,4 +1,6 @@ {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE ParallelListComp #-} + module Util ( module Util , module Language.C @@ -36,7 +38,7 @@ dummyStmt s = CExpr (Just var) (undefNode, voidType) vsGoldenFile :: FilePath -> String -> (CTranslationUnit SemPhase-> IO LBS.ByteString) -> TestTree vsGoldenFile fn name act = goldenVsString fn (replaceExtension fn ( "." ++ name ++ "-golden" )) (openAndParse >>= act ) where openAndParse = do - c <- runRIO NoLogging $ openCFile fn + c <- runRIO NoLogging $ openCFile defaultTypechecker fn case c of Nothing -> assertFailure $ "should be able to open, parse, and typecheck file" ++ fn Just ast -> return ast @@ -55,3 +57,13 @@ parseAndAnalyseFile bs = case runTrav_ (analyseAST ast) of Left _ -> assertFailure "should be typeable" Right (ast', _) -> return ast' + +assertListEqual :: HasCallStack => (Eq a, Show a) => [a] -> [a] -> IO () +assertListEqual l r + | length l == length r = sequence_ [assertEqual ("at index " ++ show i ++ " equal") x y | x <- l | y <- r | i <- [0..]] + | otherwise = assertFailure "list of unequal length cannot be equal" + +assertListEqualWith :: HasCallStack => (Eq b, Show b) => (a -> b) -> [a] -> [a] -> IO () +assertListEqualWith f l r + | length l == length r = sequence_ [assertEqual ("at index " ++ show i ++ " equal") (f x) (f y) | x <- l | y <- r | i <- [0..]] + | otherwise = assertFailure "list of unequal length cannot be equal"