From 4b2c8b65073905ec6a324a7777ce33081150c877 Mon Sep 17 00:00:00 2001 From: Christian Klinger Date: Tue, 31 Jul 2018 15:01:15 +0200 Subject: [PATCH 1/5] wip --- Annotator.hs | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 Annotator.hs diff --git a/Annotator.hs b/Annotator.hs new file mode 100644 index 0000000..e5bc309 --- /dev/null +++ b/Annotator.hs @@ -0,0 +1,6 @@ +module VDiff.Annotator where + +import VDiff.Prelude + +annotate :: CTranslationUnit NodeInfo -> CTranslationUnit SemPhase +annotate tu = undefined From 8fa241b5698c82337f59e881e72619c8a0c974f9 Mon Sep 17 00:00:00 2001 From: Christian Klinger Date: Wed, 1 Aug 2018 10:23:02 +0200 Subject: [PATCH 2/5] complete but (very) unsound typechecker. --- Annotator.hs | 6 - .../src/Language/C/Analysis/AstAnalysis2.hs | 6 +- vdiff/app/vdiff-take/Main.hs | 2 +- vdiff/src/VDiff/Diff.hs | 9 +- vdiff/src/VDiff/Instrumentation.hs | 9 +- vdiff/src/VDiff/Prelude/Types.hs | 2 + vdiff/src/VDiff/SimpleTypecheck.hs | 351 ++++++++++++++++++ 7 files changed, 368 insertions(+), 17 deletions(-) delete mode 100644 Annotator.hs create mode 100644 vdiff/src/VDiff/SimpleTypecheck.hs diff --git a/Annotator.hs b/Annotator.hs deleted file mode 100644 index e5bc309..0000000 --- a/Annotator.hs +++ /dev/null @@ -1,6 +0,0 @@ -module VDiff.Annotator where - -import VDiff.Prelude - -annotate :: CTranslationUnit NodeInfo -> CTranslationUnit SemPhase -annotate tu = undefined diff --git a/language-c-extensible/src/Language/C/Analysis/AstAnalysis2.hs b/language-c-extensible/src/Language/C/Analysis/AstAnalysis2.hs index 70b6edc..ebe65dd 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 @@ -68,8 +68,8 @@ analyseAST (CTranslUnit decls _file_node) = do -- check we are in global scope afterwards getDefTable >>= \dt -> unless (inFileScope dt) $ error "Internal Error: Not in filescope after analysis" - gld <- globalDefs <$> getDefTable - return $ CTranslUnit decls' (_file_node, gld) + -- gld <- globalDefs <$> getDefTable + 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..36f1fe1 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/src/VDiff/Diff.hs b/vdiff/src/VDiff/Diff.hs index c541b70..f850d24 100644 --- a/vdiff/src/VDiff/Diff.hs +++ b/vdiff/src/VDiff/Diff.hs @@ -26,6 +26,7 @@ import VDiff.ArithmeticExpressions (evalExpr) import VDiff.Data import VDiff.Execute import VDiff.Instrumentation +import qualified VDiff.SimpleTypecheck as SimpleTypechecker import VDiff.Strategy import VDiff.Util.ResourcePool import VDiff.Verifier @@ -43,7 +44,7 @@ cmdDiff seed params = do liftIO $ setStdGen $ mkStdGen s - mAst <- openCFile (params ^. inputFile) + mAst <- openCFile defaultTypechecker (params ^. inputFile) case mAst of Nothing -> liftIO exitFailure Just ast -> do @@ -55,7 +56,7 @@ 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 fn = openCFile SimpleTypechecker.check fn >>= \case Nothing -> liftIO exitFailure Just ast -> liftIO $ putStrLn $ render $ pretty ast @@ -63,12 +64,12 @@ cmdParseTest fn = openCFile fn >>= \case cmdMarkReads :: HasLogFunc env => SearchMode -> FilePath -> RIO env () cmdMarkReads mode fn = do logDebug $ "mode is " <> display (tshow mode) - (Just ast) <- openCFile fn + (Just ast) <- openCFile defaultTypechecker 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..762f204 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 @@ -57,10 +58,12 @@ import qualified VDiff.Instrumentation.Fragments as Fragments import VDiff.Instrumentation.Reads +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 => Typechecker -> FilePath -> RIO env (Maybe TU) +openCFile typechecker 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" @@ -71,7 +74,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..35c8dcc 100644 --- a/vdiff/src/VDiff/Prelude/Types.hs +++ b/vdiff/src/VDiff/Prelude/Types.hs @@ -54,6 +54,8 @@ data Strategy = RandomWalkStrategy data SearchMode = IdentOnly | Subexpressions deriving Show +type Typechecker = CTranslationUnit NodeInfo -> Either [CError] ((CTranslationUnit SemPhase), [CError]) + 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..8004579 --- /dev/null +++ b/vdiff/src/VDiff/SimpleTypecheck.hs @@ -0,0 +1,351 @@ +{-# LANGUAGE LambdaCase #-} +-- I don't care about GNU extensions, so statements are always of type void + +module VDiff.SimpleTypecheck where + +import Data.Coerce +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, []) + +newtype TrivialM a = TrivialM { unTrivialM :: Either [CError] (a, [CError])} + deriving (Functor) + +instance Applicative TrivialM where + pure x = TrivialM (Right (x, [])) + tf <*> ta = case unTrivialM tf of + Left errs -> TrivialM $ Left errs + Right (f, errs) -> case unTrivialM ta of + Left errs -> TrivialM $ Left errs + Right (a, errs') -> TrivialM $ Right (f a, errs ++ errs') + + +instance Monad TrivialM where + ta >>= f = case unTrivialM ta of + Left err -> TrivialM $ Left err + Right (a, errs) -> case unTrivialM (f a) of + Left err -> TrivialM $ Left err + Right (b, errs') -> TrivialM $ Right (b, errs ++ errs') + +check :: Typechecker +check = unTrivialM .translationUnit + +-- | annotate every expression with type "int" +translationUnit :: CTranslationUnit NodeInfo -> TrivialM (CTranslationUnit SemPhase) +translationUnit (CTranslUnit declrs ni) = CTranslUnit <$> mapM externalDeclaration declrs <*> pure ni + + +externalDeclaration :: CExternalDeclaration NodeInfo -> TrivialM (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 -> TrivialM (CFunctionDef SemPhase) +functionDefinition (CFunDef specs declr oldStyleParams body ni) = do + specs' <- mapM declarationSpecifier specs + declr' <- declarator declr + oldStyleParams' <- mapM declaration oldStyleParams + body' <- statement body + return $ CFunDef specs' declr' oldStyleParams' body' ni + +declaration :: CDeclaration NodeInfo -> TrivialM (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 + return $ CDecl specs' initDeclrs' ni + + +initializedDeclarator :: (Maybe (CDeclarator NodeInfo), Maybe (CInitializer NodeInfo), Maybe (CExpression NodeInfo)) + -> TrivialM (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 -> TrivialM (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) -> TrivialM ([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 -> TrivialM (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 -> TrivialM (CFunctionSpecifier SemPhase) +functionSpecifier (CInlineQual ni) = return $ CInlineQual ni +functionSpecifier (CNoreturnQual ni) = return $ CNoreturnQual ni + +storageSpecifier :: CStorageSpecifier NodeInfo -> TrivialM (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 -> TrivialM (CAlignmentSpecifier SemPhase) +alignmentSpecifier (CAlignAsType decl ni) = CAlignAsType <$> declaration decl <*> pure ni +alignmentSpecifier (CAlignAsExpr e ni) = CAlignAsExpr <$> expression e <*> pure ni + +typeSpecifier :: CTypeSpecifier NodeInfo -> TrivialM (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 -> TrivialM (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 -> TrivialM (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 -> TrivialM (CStringLiteral SemPhase) +stringLiteral (CStrLit s ni) = return $ CStrLit s ni + +derivedDeclarator :: CDerivedDeclarator NodeInfo -> TrivialM (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 -> TrivialM (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 -> TrivialM (CArraySize SemPhase) +arraySize (CNoArrSize b) = return $ CNoArrSize b +arraySize (CArrSize b e) = CArrSize b <$> expression e + +attribute :: CAttribute NodeInfo -> TrivialM (CAttribute SemPhase) +attribute (CAttr i exprs ni) = CAttr i <$> mapM expression exprs <*> pure ni + +statement :: CStatement NodeInfo -> TrivialM (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 -> TrivialM (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 + ty <- unify [getType e1', getType e2'] + return $ CAssign op e1' e2' (ni, ty) + +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 <- 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 + return $ CIndex e1' e2' (ni, simpleInt) -- TODO + +expression (CCall f ps ni) = do + f' <- expression f + ps' <- mapM expression ps + return $ CCall f' ps' (ni, simpleInt) -- TODO + +expression (CMember e n b ni) = do + e' <- expression e + return $ CMember e' n b (ni, simpleInt) -- TODO + +expression (CVar v ni) = return $ CVar v (ni, simpleInt) -- TODO: lookup + +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 -> TrivialM (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 -> TrivialM (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] -> TrivialM Type +unify types = return $ P.head types -- TODO: Do some unification + +-- unifies the given types +unifyArithmetic :: [Type] -> TrivialM Type +unifyArithmetic = unify -- TODO: Do some unification, but make sure that it is numeric + + +-- 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 From b6f6a4a376a89d06e1436333c2edca17e4784a1f Mon Sep 17 00:00:00 2001 From: Christian Klinger Date: Thu, 2 Aug 2018 23:03:52 +0200 Subject: [PATCH 3/5] much more precise now. Agrees on expression types with the default typechecker on a wide range of files. Still has problems with implicit int to float conversions, but that should be easiliy fixable. --- .../src/Language/C/Analysis/AstAnalysis2.hs | 2 +- vdiff/assets/test/typecheck/benghazi.c | 24 ++ ...n_1_3_true-unreach-call_true-termination.c | 58 +++ .../standard_copy9_true-unreach-call_ground.i | 52 +++ ...sum10_true-unreach-call_true-termination.c | 57 +++ ...rox_false-unreach-call2_true-termination.c | 20 ++ vdiff/src/VDiff/Diff.hs | 4 +- vdiff/src/VDiff/Prelude/Types.hs | 2 +- vdiff/src/VDiff/SimpleTypecheck.hs | 339 +++++++++++++++--- .../regression/InstrumentationProperties.hs | 2 +- vdiff/test/regression/Lens.hs | 2 +- vdiff/test/regression/Query.hs | 12 +- vdiff/test/regression/Regression.hs | 2 + vdiff/test/regression/SimpleTypeCheck.hs | 43 +++ vdiff/test/regression/Util.hs | 14 +- 15 files changed, 561 insertions(+), 72 deletions(-) create mode 100644 vdiff/assets/test/typecheck/benghazi.c create mode 100644 vdiff/assets/test/typecheck/newton_1_3_true-unreach-call_true-termination.c create mode 100644 vdiff/assets/test/typecheck/standard_copy9_true-unreach-call_ground.i create mode 100644 vdiff/assets/test/typecheck/sum10_true-unreach-call_true-termination.c create mode 100644 vdiff/assets/test/typecheck/underapprox_false-unreach-call2_true-termination.c create mode 100644 vdiff/test/regression/SimpleTypeCheck.hs diff --git a/language-c-extensible/src/Language/C/Analysis/AstAnalysis2.hs b/language-c-extensible/src/Language/C/Analysis/AstAnalysis2.hs index ebe65dd..bc63dc9 100644 --- a/language-c-extensible/src/Language/C/Analysis/AstAnalysis2.hs +++ b/language-c-extensible/src/Language/C/Analysis/AstAnalysis2.hs @@ -68,7 +68,7 @@ analyseAST (CTranslUnit decls _file_node) = do -- check we are in global scope afterwards getDefTable >>= \dt -> unless (inFileScope dt) $ error "Internal Error: Not in filescope after analysis" - -- gld <- globalDefs <$> getDefTable + gld <- globalDefs <$> getDefTable return $ CTranslUnit decls' (_file_node) 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 FilePath -> RIO env () -cmdParseTest fn = openCFile SimpleTypechecker.check fn >>= \case +cmdParseTest fn = openCFile simpleTypechecker fn >>= \case Nothing -> liftIO exitFailure Just ast -> liftIO $ putStrLn $ render $ pretty ast diff --git a/vdiff/src/VDiff/Prelude/Types.hs b/vdiff/src/VDiff/Prelude/Types.hs index 35c8dcc..7d0f680 100644 --- a/vdiff/src/VDiff/Prelude/Types.hs +++ b/vdiff/src/VDiff/Prelude/Types.hs @@ -32,7 +32,7 @@ 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 diff --git a/vdiff/src/VDiff/SimpleTypecheck.hs b/vdiff/src/VDiff/SimpleTypecheck.hs index 8004579..1eb8216 100644 --- a/vdiff/src/VDiff/SimpleTypecheck.hs +++ b/vdiff/src/VDiff/SimpleTypecheck.hs @@ -1,9 +1,15 @@ {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiWayIf #-} -- I don't care about GNU extensions, so statements are always of type void -module VDiff.SimpleTypecheck where +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, @@ -13,67 +19,205 @@ import VDiff.Prelude hiding (declarator, expression, return' a = Right (a, []) -newtype TrivialM a = TrivialM { unTrivialM :: Either [CError] (a, [CError])} - deriving (Functor) -instance Applicative TrivialM where - pure x = TrivialM (Right (x, [])) - tf <*> ta = case unTrivialM tf of - Left errs -> TrivialM $ Left errs - Right (f, errs) -> case unTrivialM ta of - Left errs -> TrivialM $ Left errs - Right (a, errs') -> TrivialM $ Right (f a, errs ++ errs') - - -instance Monad TrivialM where - ta >>= f = case unTrivialM ta of - Left err -> TrivialM $ Left err - Right (a, errs) -> case unTrivialM (f a) of - Left err -> TrivialM $ Left err - Right (b, errs') -> TrivialM $ Right (b, errs ++ errs') - -check :: Typechecker -check = unTrivialM .translationUnit +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 -> TrivialM (CTranslationUnit SemPhase) +translationUnit :: CTranslationUnit NodeInfo -> AnalysisM (CTranslationUnit SemPhase) translationUnit (CTranslUnit declrs ni) = CTranslUnit <$> mapM externalDeclaration declrs <*> pure ni -externalDeclaration :: CExternalDeclaration NodeInfo -> TrivialM (CExternalDeclaration SemPhase) +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 -> TrivialM (CFunctionDef SemPhase) +functionDefinition :: CFunctionDef NodeInfo -> AnalysisM (CFunctionDef SemPhase) functionDefinition (CFunDef specs declr oldStyleParams body ni) = do specs' <- mapM declarationSpecifier specs - declr' <- declarator declr - oldStyleParams' <- mapM declaration oldStyleParams - body' <- statement body - return $ CFunDef specs' declr' oldStyleParams' body' ni - -declaration :: CDeclaration NodeInfo -> TrivialM (CDeclaration SemPhase) + (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 +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)) - -> TrivialM (Maybe (CDeclarator SemPhase), Maybe (CInitializer SemPhase), Maybe (CExpression SemPhase)) + -> 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 -> TrivialM (CInitializer SemPhase) +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) -> TrivialM ([CPartDesignator SemPhase], CInitializer SemPhase) + initPart :: ([CPartDesignator NodeInfo], CInitializer NodeInfo) -> AnalysisM ([CPartDesignator SemPhase], CInitializer SemPhase) initPart (prts, init) = do prts' <- mapM partDesignator prts init' <- initializer init @@ -83,18 +227,18 @@ initializer (CInitList iniList ni) = CInitList <$> mapM initPart iniList <*> pur partDesignator (CRangeDesig e1 e2 ni) = CRangeDesig <$> expression e1 <*> expression e2 <*> pure ni -declarationSpecifier :: CDeclarationSpecifier NodeInfo -> TrivialM (CDeclarationSpecifier SemPhase) +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 -> TrivialM (CFunctionSpecifier SemPhase) +functionSpecifier :: CFunctionSpecifier NodeInfo -> AnalysisM (CFunctionSpecifier SemPhase) functionSpecifier (CInlineQual ni) = return $ CInlineQual ni functionSpecifier (CNoreturnQual ni) = return $ CNoreturnQual ni -storageSpecifier :: CStorageSpecifier NodeInfo -> TrivialM (CStorageSpecifier SemPhase) +storageSpecifier :: CStorageSpecifier NodeInfo -> AnalysisM (CStorageSpecifier SemPhase) storageSpecifier (CAuto ni) = return $ CAuto ni storageSpecifier (CRegister ni) = return $ CRegister ni storageSpecifier (CStatic ni) = return $ CStatic ni @@ -102,11 +246,11 @@ storageSpecifier (CExtern ni) = return $ CExtern ni storageSpecifier (CTypedef ni) = return $ CTypedef ni storageSpecifier (CThread ni) = return $ CThread ni -alignmentSpecifier :: CAlignmentSpecifier NodeInfo -> TrivialM (CAlignmentSpecifier SemPhase) +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 -> TrivialM (CTypeSpecifier SemPhase) +typeSpecifier :: CTypeSpecifier NodeInfo -> AnalysisM (CTypeSpecifier SemPhase) typeSpecifier (CVoidType ni) = return $ CVoidType ni typeSpecifier (CCharType ni) = return $ CCharType ni typeSpecifier (CShortType ni) = return $ CShortType ni @@ -136,13 +280,13 @@ enumeration (CEnum mi elems attrs ni) = CEnum mi <$> maybeM enumElements elems < e' <- expression e return (n, Just e') -structOrUnion :: CStructureUnion NodeInfo -> TrivialM (CStructureUnion SemPhase) +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 -> TrivialM (CDeclarator SemPhase) +declarator :: CDeclarator NodeInfo -> AnalysisM (CDeclarator SemPhase) declarator (CDeclr mi derivedDeclrs mAsm attrs ni) = do derivedDeclrs' <- mapM derivedDeclarator derivedDeclrs attrs' <- mapM attribute attrs @@ -150,10 +294,10 @@ declarator (CDeclr mi derivedDeclrs mAsm attrs ni) = do return $ CDeclr mi derivedDeclrs' Nothing attrs' ni -stringLiteral :: CStringLiteral NodeInfo -> TrivialM (CStringLiteral SemPhase) +stringLiteral :: CStringLiteral NodeInfo -> AnalysisM (CStringLiteral SemPhase) stringLiteral (CStrLit s ni) = return $ CStrLit s ni -derivedDeclarator :: CDerivedDeclarator NodeInfo -> TrivialM (CDerivedDeclarator SemPhase) +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 @@ -165,7 +309,7 @@ derivedDeclarator (CFunDeclr (Right (decls,b)) attrs ni) = do attrs' <- mapM attribute attrs return $ CFunDeclr (Right (decls', b)) attrs' ni -typeQualifier :: CTypeQualifier NodeInfo -> TrivialM (CTypeQualifier SemPhase) +typeQualifier :: CTypeQualifier NodeInfo -> AnalysisM (CTypeQualifier SemPhase) typeQualifier(CConstQual ni) = return $ CConstQual ni typeQualifier(CVolatQual ni) = return $ CVolatQual ni typeQualifier(CRestrQual ni) = return $ CRestrQual ni @@ -174,14 +318,14 @@ typeQualifier(CAttrQual attr) = CAttrQual <$> attribute attr typeQualifier(CNullableQual ni) = return $ CNullableQual ni typeQualifier(CNonnullQual ni) = return $ CNonnullQual ni -arraySize :: CArraySize NodeInfo -> TrivialM (CArraySize SemPhase) +arraySize :: CArraySize NodeInfo -> AnalysisM (CArraySize SemPhase) arraySize (CNoArrSize b) = return $ CNoArrSize b arraySize (CArrSize b e) = CArrSize b <$> expression e -attribute :: CAttribute NodeInfo -> TrivialM (CAttribute SemPhase) +attribute :: CAttribute NodeInfo -> AnalysisM (CAttribute SemPhase) attribute (CAttr i exprs ni) = CAttr i <$> mapM expression exprs <*> pure ni -statement :: CStatement NodeInfo -> TrivialM (CStatement SemPhase) +statement :: CStatement NodeInfo -> AnalysisM (CStatement SemPhase) statement (CLabel lbl stmt attrs ni) = do stmt' <- statement stmt attrs' <- mapM attribute attrs @@ -242,7 +386,7 @@ statement (CReturn me ni) = do statement (CAsm asmStmt ni) = undefined -expression :: CExpression NodeInfo -> TrivialM (CExpression SemPhase) +expression :: CExpression NodeInfo -> AnalysisM (CExpression SemPhase) expression (CComma exprs ni) = do exprs' <- mapM expression exprs let ty = getType (P.head exprs') @@ -251,8 +395,7 @@ expression (CComma exprs ni) = do expression (CAssign op e1 e2 ni) = do e1' <- expression e1 e2' <- expression e2 - ty <- unify [getType e1', getType e2'] - return $ CAssign op e1' e2' (ni, ty) + return $ CAssign op e1' e2' (ni, getType e1') expression (CCond e1 me2 e3 ni) = do e1' <- expression e1 @@ -265,7 +408,9 @@ expression (CCond e1 me2 e3 ni) = do expression (CBinary op e1 e2 ni) = do e1' <- expression e1 e2' <- expression e2 - ty <- unifyArithmetic [getType e1', getType 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 @@ -288,18 +433,22 @@ expression (CComplexImag e ni) = CComplexImag <$> expression e <*> pure (ni, voi expression (CIndex e1 e2 ni) = do e1' <- expression e1 e2' <- expression e2 - return $ CIndex e1' e2' (ni, simpleInt) -- TODO + 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 - return $ CCall f' ps' (ni, simpleInt) -- TODO + 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) = return $ CVar v (ni, simpleInt) -- TODO: lookup +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 @@ -311,14 +460,14 @@ expression (CStatExpr stmt ni) = do expression (CLabAddrExpr n ni) = undefined -- a GNU C address of label expression (CBuiltinExpr builtin) = CBuiltinExpr <$> builtinThing builtin -constant :: CConstant NodeInfo -> TrivialM (CConstant SemPhase) +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 -> TrivialM (CBuiltinThing SemPhase) +builtinThing :: CBuiltinThing NodeInfo -> AnalysisM (CBuiltinThing SemPhase) builtinThing (CBuiltinVaArg e decl ni) = do e' <- expression e decl' <- declaration decl @@ -328,12 +477,36 @@ builtinThing (CBuiltinTypesCompatible decl1 decl2 ni) = undefined builtinThing (CBuiltinConvertVector e decl ni) = undefined -- unifies the given types -unify :: [Type] -> TrivialM Type +unify :: [Type] -> AnalysisM Type unify types = return $ P.head types -- TODO: Do some unification -- unifies the given types -unifyArithmetic :: [Type] -> TrivialM Type -unifyArithmetic = unify -- TODO: Do some unification, but make sure that it is numeric +unifyArithmetic :: [Type] -> AnalysisM Type +unifyArithmetic = return . P.foldl1 unifyArithmetic' -- TODO: Do some unification, but make sure that it is numeric + where + unifyArithmetic' t u = + let t' = getIntType t + u' = getIntType u + in 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 + + +-- 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 @@ -349,3 +522,53 @@ 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 + +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 -> IntType +getIntType (DirectType (TyIntegral ty) _ _) = ty +getIntType _ = error "getIntType on non-int type" 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" From 57afa9d8bc6e7fdec26a2689e0610d215070ae5b Mon Sep 17 00:00:00 2001 From: Christian Klinger Date: Fri, 3 Aug 2018 00:06:14 +0200 Subject: [PATCH 4/5] implicit int to float conversion. --- vdiff/src/VDiff/SimpleTypecheck.hs | 43 +++++++++++++++++++++--------- 1 file changed, 31 insertions(+), 12 deletions(-) diff --git a/vdiff/src/VDiff/SimpleTypecheck.hs b/vdiff/src/VDiff/SimpleTypecheck.hs index 1eb8216..a612b26 100644 --- a/vdiff/src/VDiff/SimpleTypecheck.hs +++ b/vdiff/src/VDiff/SimpleTypecheck.hs @@ -484,15 +484,24 @@ unify types = return $ P.head types -- TODO: Do some unification unifyArithmetic :: [Type] -> AnalysisM Type unifyArithmetic = return . P.foldl1 unifyArithmetic' -- TODO: Do some unification, but make sure that it is numeric where - unifyArithmetic' t u = - let t' = getIntType t - u' = getIntType u - in 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 + 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 @@ -553,6 +562,12 @@ 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 @@ -569,6 +584,10 @@ isSigned TyULong = False isSigned TyLLong = True isSigned TyULLong = False -getIntType :: Type -> IntType -getIntType (DirectType (TyIntegral ty) _ _) = ty -getIntType _ = error "getIntType on non-int type" +getIntType :: Type -> Maybe IntType +getIntType (DirectType (TyIntegral ty) _ _) = Just ty +getIntType _ = Nothing + +getFloatType :: Type -> Maybe FloatType +getFloatType (DirectType (TyFloating ty) _ _) = Just ty +getFloatType _ = Nothing From b726ff4479a205ac48abb835c9cfca32b798e05f Mon Sep 17 00:00:00 2001 From: Christian Klinger Date: Sun, 5 Aug 2018 11:07:48 +0200 Subject: [PATCH 5/5] added switch for typechecker. --- vdiff/app/vdiff-take/Main.hs | 2 +- vdiff/app/vdiff/Main.hs | 18 +++++++++--------- vdiff/src/VDiff/Arguments.hs | 8 ++++++++ vdiff/src/VDiff/Diff.hs | 17 ++++++++--------- vdiff/src/VDiff/Instrumentation.hs | 14 ++++++++++++-- vdiff/src/VDiff/Prelude/Types.hs | 6 +++++- vdiff/src/VDiff/SimpleTypecheck.hs | 2 ++ 7 files changed, 45 insertions(+), 22 deletions(-) diff --git a/vdiff/app/vdiff-take/Main.hs b/vdiff/app/vdiff-take/Main.hs index 36f1fe1..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 defaultTypechecker 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/src/VDiff/Arguments.hs b/vdiff/src/VDiff/Arguments.hs index c4b3028..ef7cb54 100644 --- a/vdiff/src/VDiff/Arguments.hs +++ b/vdiff/src/VDiff/Arguments.hs @@ -121,6 +121,14 @@ resources = do "GB" -> 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 53154bd..77aa004 100644 --- a/vdiff/src/VDiff/Diff.hs +++ b/vdiff/src/VDiff/Diff.hs @@ -33,8 +33,8 @@ 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 @@ -43,8 +43,7 @@ cmdDiff seed params = do logInfo $ "seed for random generator: " <> display s liftIO $ setStdGen $ mkStdGen s - - mAst <- openCFile defaultTypechecker (params ^. inputFile) + mAst <- openCFile tcFlag (params ^. inputFile) case mAst of Nothing -> liftIO exitFailure Just ast -> do @@ -55,16 +54,16 @@ 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 simpleTypechecker 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 defaultTypechecker fn + (Just ast) <- openCFile tc fn let ast' = markAllReads mode ast liftIO . putStrLn . render . pretty $ ast' diff --git a/vdiff/src/VDiff/Instrumentation.hs b/vdiff/src/VDiff/Instrumentation.hs index 762f204..fecbab6 100644 --- a/vdiff/src/VDiff/Instrumentation.hs +++ b/vdiff/src/VDiff/Instrumentation.hs @@ -56,17 +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 => Typechecker -> FilePath -> RIO env (Maybe TU) -openCFile typechecker 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 diff --git a/vdiff/src/VDiff/Prelude/Types.hs b/vdiff/src/VDiff/Prelude/Types.hs index 7d0f680..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 (analyseAST, getType, maybeM) +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 @@ -56,6 +57,9 @@ data SearchMode = IdentOnly | Subexpressions 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 index a612b26..e79d166 100644 --- a/vdiff/src/VDiff/SimpleTypecheck.hs +++ b/vdiff/src/VDiff/SimpleTypecheck.hs @@ -169,7 +169,9 @@ analyseTypeSpecifier (CVoidType _) = return $ Left $ DirectType TyV 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