diff --git a/trunk/examples/CParser/include/directoryHeaderOne.h b/trunk/examples/CParser/include/directoryHeaderOne.h new file mode 100644 index 00000000000..4daf72e5cb8 --- /dev/null +++ b/trunk/examples/CParser/include/directoryHeaderOne.h @@ -0,0 +1,19 @@ +/* + * Header file that can be included as source file in test C programs where + * this source file is located using one of the + * + * # include "q-char-sequence" new-line + * # include new-line + * + * preprocessor directives (see C standard, section 6.10.2). + */ + +typedef struct ret { + int code; +} ret_t; + +static inline ret_t funcFromDirectoryHeaderOne(void) +{ + ret_t ret = { .code = 2 }; + return ret; +} diff --git a/trunk/examples/CParser/include/directoryHeaderTwo.h b/trunk/examples/CParser/include/directoryHeaderTwo.h new file mode 100644 index 00000000000..4704e905fd0 --- /dev/null +++ b/trunk/examples/CParser/include/directoryHeaderTwo.h @@ -0,0 +1,15 @@ +/* + * Header file that can be included as source file in test C programs where + * this source file is located using one of the + * + * # include "q-char-sequence" new-line + * # include new-line + * + * preprocessor directives (see C standard, section 6.10.2). + */ + +static inline int funcFromDirectoryHeaderTwo(void) +{ + int var = 4; + return var; +} diff --git a/trunk/examples/CParser/include/subdirectory/additionalHeader.h b/trunk/examples/CParser/include/subdirectory/additionalHeader.h new file mode 100644 index 00000000000..5feada07dac --- /dev/null +++ b/trunk/examples/CParser/include/subdirectory/additionalHeader.h @@ -0,0 +1,11 @@ +/* + * Header file that can be included as source file in test C programs where + * this source file is located using one of the + * + * # include "q-char-sequence" new-line + * # include new-line + * + * preprocessor directives (see C standard, section 6.10.2). + */ + +int groundTruth = 17; diff --git a/trunk/examples/CParser/includeHeadersLocal.c b/trunk/examples/CParser/includeHeadersLocal.c new file mode 100644 index 00000000000..50035108986 --- /dev/null +++ b/trunk/examples/CParser/includeHeadersLocal.c @@ -0,0 +1,32 @@ +//#Safe +/** + * This test program includes a named header file that is searched for in an + * implementation-defined manner (see C standard, section 6.10.2): + * + * # include new-line + * # include "q-char-sequence" new-line + * + * The first directive searches a sequence of implementation-defined places for + * a header identified uniquely by the specified sequence between the '<' and + * '>' delimiters. The second directive causes the replacement of that + * directive by the entire contents of the source file identified by the + * specified sequence between the '"' delimiters. The named source file is + * searched for in an implementation-defined manner. + * + * As usual, a C preprocessor searches for the named source file first in the + * directory containing the current file, then in the same directories + * specified with a sequence between the '<' and '>' delimiters. + */ + +#include "localHeaderOne.h" +#include "localHeaderTwo.h" + +int main(void) +{ + status_t funcOneRet = funcFromLocalHeaderOne(); + int funcOneVal = funcOneRet.retval; + //@ assert(funcOneVal == 3); + int funcTwoVal = funcFromLocalHeaderTwo(); + //@ assert(funcTwoVal == 5); + return funcOneVal + funcTwoVal; +} diff --git a/trunk/examples/CParser/includeHeadersNonRecursiveSimple.c b/trunk/examples/CParser/includeHeadersNonRecursiveSimple.c new file mode 100644 index 00000000000..b7d17e5e6d6 --- /dev/null +++ b/trunk/examples/CParser/includeHeadersNonRecursiveSimple.c @@ -0,0 +1,32 @@ +//#Safe +/** + * This test program includes a named header file that is searched for in an + * implementation-defined manner (see C standard, section 6.10.2): + * + * # include new-line + * # include "q-char-sequence" new-line + * + * The first directive searches a sequence of implementation-defined places for + * a header identified uniquely by the specified sequence between the '<' and + * '>' delimiters. The second directive causes the replacement of that + * directive by the entire contents of the source file identified by the + * specified sequence between the '"' delimiters. The named source file is + * searched for in an implementation-defined manner. + * + * As usual, a C preprocessor searches for the named source file first in the + * directory containing the current file, then in the same directories + * specified with a sequence between the '<' and '>' delimiters. + */ + +#include +#include + +int main(void) +{ + ret_t funcOneRet = funcFromDirectoryHeaderOne(); + int funcOneVal = funcOneRet.code; + //@ assert(funcOneVal == 2); + int funcTwoVal = funcFromDirectoryHeaderTwo(); + //@ assert(funcTwoVal == 4); + return funcOneVal + funcTwoVal; +} diff --git a/trunk/examples/CParser/includeHeadersNonRecursiveSubdirectory.c b/trunk/examples/CParser/includeHeadersNonRecursiveSubdirectory.c new file mode 100644 index 00000000000..afe7cacacc2 --- /dev/null +++ b/trunk/examples/CParser/includeHeadersNonRecursiveSubdirectory.c @@ -0,0 +1,34 @@ +//#Safe +/** + * This test program includes a named header file that is searched for in an + * implementation-defined manner (see C standard, section 6.10.2): + * + * # include new-line + * # include "q-char-sequence" new-line + * + * The first directive searches a sequence of implementation-defined places for + * a header identified uniquely by the specified sequence between the '<' and + * '>' delimiters. The second directive causes the replacement of that + * directive by the entire contents of the source file identified by the + * specified sequence between the '"' delimiters. The named source file is + * searched for in an implementation-defined manner. + * + * As usual, a C preprocessor searches for the named source file first in the + * directory containing the current file, then in the same directories + * specified with a sequence between the '<' and '>' delimiters. + */ + +#include +#include +#include + +int main(void) +{ + ret_t funcOneRet = funcFromDirectoryHeaderOne(); + int funcOneVal = funcOneRet.code; + //@ assert(funcOneVal == 2); + int funcTwoVal = funcFromDirectoryHeaderTwo(); + //@ assert(funcTwoVal == 4); + //@ assert(groundTruth == 17); + return funcOneVal + funcTwoVal + groundTruth; +} diff --git a/trunk/examples/CParser/includeHeadersRecursive.c b/trunk/examples/CParser/includeHeadersRecursive.c new file mode 100644 index 00000000000..afe7cacacc2 --- /dev/null +++ b/trunk/examples/CParser/includeHeadersRecursive.c @@ -0,0 +1,34 @@ +//#Safe +/** + * This test program includes a named header file that is searched for in an + * implementation-defined manner (see C standard, section 6.10.2): + * + * # include new-line + * # include "q-char-sequence" new-line + * + * The first directive searches a sequence of implementation-defined places for + * a header identified uniquely by the specified sequence between the '<' and + * '>' delimiters. The second directive causes the replacement of that + * directive by the entire contents of the source file identified by the + * specified sequence between the '"' delimiters. The named source file is + * searched for in an implementation-defined manner. + * + * As usual, a C preprocessor searches for the named source file first in the + * directory containing the current file, then in the same directories + * specified with a sequence between the '<' and '>' delimiters. + */ + +#include +#include +#include + +int main(void) +{ + ret_t funcOneRet = funcFromDirectoryHeaderOne(); + int funcOneVal = funcOneRet.code; + //@ assert(funcOneVal == 2); + int funcTwoVal = funcFromDirectoryHeaderTwo(); + //@ assert(funcTwoVal == 4); + //@ assert(groundTruth == 17); + return funcOneVal + funcTwoVal + groundTruth; +} diff --git a/trunk/examples/CParser/localHeaderOne.h b/trunk/examples/CParser/localHeaderOne.h new file mode 100644 index 00000000000..f803cafc610 --- /dev/null +++ b/trunk/examples/CParser/localHeaderOne.h @@ -0,0 +1,18 @@ +/* + * Header file that can be included as source file in test C programs where + * this source file is located using the + * + * # include "q-char-sequence" new-line + * + * preprocessor directive (see C standard, section 6.10.2). + */ + +typedef struct status { + int retval; +} status_t; + +static inline status_t funcFromLocalHeaderOne(void) +{ + status_t ret = { .retval = 3 }; + return ret; +} diff --git a/trunk/examples/CParser/localHeaderTwo.h b/trunk/examples/CParser/localHeaderTwo.h new file mode 100644 index 00000000000..422bb92f374 --- /dev/null +++ b/trunk/examples/CParser/localHeaderTwo.h @@ -0,0 +1,14 @@ +/* + * Header file that can be included as source file in test C programs where + * this source file is located using the + * + * # include "q-char-sequence" new-line + * + * preprocessor directive (see C standard, section 6.10.2). + */ + +static inline int funcFromLocalHeaderTwo(void) +{ + int var = 5; + return var; +} diff --git a/trunk/examples/programs/regression/c/preprocessor/preprocessor-conditionals_safe.c b/trunk/examples/programs/regression/c/preprocessor/preprocessor-conditionals_safe.c new file mode 100644 index 00000000000..4932900cc4d --- /dev/null +++ b/trunk/examples/programs/regression/c/preprocessor/preprocessor-conditionals_safe.c @@ -0,0 +1,34 @@ +//#Safe +/*----------------------------------------------------------------------------- + * C program with preprocessor macros to test macro parsing and substitution + *----------------------------------------------------------------------------- + * Author: Manuel Bentele + * Date: 2023-09-25 + *---------------------------------------------------------------------------*/ + +#undef SELECT_FUNC_ONE + +#define VALUE 100 + +int compute_one(int num) +{ + return num - VALUE; +} + +int compute_two(int num) +{ + return num + VALUE; +} + +#ifdef SELECT_FUNC_ONE +#define FUNC(VAL) compute_one(VAL) +#else +#define FUNC(VAL) compute_two(VAL) +#endif + +int main(void) +{ + int ret = FUNC(VALUE); + //@ assert(ret == 100 + 100); + return ret; +} diff --git a/trunk/examples/programs/regression/c/preprocessor/preprocessor-conditionals_unsafe.c b/trunk/examples/programs/regression/c/preprocessor/preprocessor-conditionals_unsafe.c new file mode 100644 index 00000000000..fac46637e11 --- /dev/null +++ b/trunk/examples/programs/regression/c/preprocessor/preprocessor-conditionals_unsafe.c @@ -0,0 +1,34 @@ +//#Unafe +/*----------------------------------------------------------------------------- + * C program with preprocessor macros to test macro parsing and substitution + *----------------------------------------------------------------------------- + * Author: Manuel Bentele + * Date: 2023-09-25 + *---------------------------------------------------------------------------*/ + +#define SELECT_FUNC_ONE + +#define VALUE 100 + +int compute_one(int num) +{ + return num - VALUE; +} + +int compute_two(int num) +{ + return num + VALUE; +} + +#ifdef SELECT_FUNC_ONE +#define FUNC(VAL) compute_one(VAL) +#else +#define FUNC(VAL) compute_two(VAL) +#endif + +int main(void) +{ + int ret = FUNC(VALUE); + //@ assert(ret == 100 + 100); + return ret; +} diff --git a/trunk/examples/programs/regression/c/preprocessor/preprocessor-error.c b/trunk/examples/programs/regression/c/preprocessor/preprocessor-error.c new file mode 100644 index 00000000000..734e3f52777 --- /dev/null +++ b/trunk/examples/programs/regression/c/preprocessor/preprocessor-error.c @@ -0,0 +1,14 @@ +//#Unafe +/*----------------------------------------------------------------------------- + * C program with preprocessor error statement + *----------------------------------------------------------------------------- + * Author: Manuel Bentele + * Date: 2025-01-17 + *---------------------------------------------------------------------------*/ + +#error This is an preprocessor error in the program + +int main(void) +{ + return 0; +} diff --git a/trunk/examples/programs/regression/c/preprocessor/preprocessor-macro_safe.c b/trunk/examples/programs/regression/c/preprocessor/preprocessor-macro_safe.c new file mode 100644 index 00000000000..2f764e72699 --- /dev/null +++ b/trunk/examples/programs/regression/c/preprocessor/preprocessor-macro_safe.c @@ -0,0 +1,16 @@ +//#Safe +/*----------------------------------------------------------------------------- + * C program with preprocessor macro to test macro parsing and substitution + *----------------------------------------------------------------------------- + * Author: Manuel Bentele + * Date: 2023-09-25 + *---------------------------------------------------------------------------*/ + +#define VALUE 100 + +int main(void) +{ + int ret = VALUE; + //@ assert(ret == 100); + return ret; +} diff --git a/trunk/examples/programs/regression/c/preprocessor/preprocessor-macro_unsafe.c b/trunk/examples/programs/regression/c/preprocessor/preprocessor-macro_unsafe.c new file mode 100644 index 00000000000..4c6fc5c4abf --- /dev/null +++ b/trunk/examples/programs/regression/c/preprocessor/preprocessor-macro_unsafe.c @@ -0,0 +1,16 @@ +//#Unsafe +/*----------------------------------------------------------------------------- + * C program with preprocessor macro to test macro parsing and substitution + *----------------------------------------------------------------------------- + * Author: Manuel Bentele + * Date: 2023-09-25 + *---------------------------------------------------------------------------*/ + +#define VALUE 100 + +int main(void) +{ + int ret = VALUE; + //@ assert(ret == 200); + return ret; +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/PreprocessorHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/PreprocessorHandler.java index 386258a1edd..4cbdb9127e0 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/PreprocessorHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/PreprocessorHandler.java @@ -35,16 +35,18 @@ import org.eclipse.cdt.core.dom.ast.IASTPreprocessorElseStatement; import org.eclipse.cdt.core.dom.ast.IASTPreprocessorEndifStatement; import org.eclipse.cdt.core.dom.ast.IASTPreprocessorErrorStatement; +import org.eclipse.cdt.core.dom.ast.IASTPreprocessorFunctionStyleMacroDefinition; import org.eclipse.cdt.core.dom.ast.IASTPreprocessorIfStatement; import org.eclipse.cdt.core.dom.ast.IASTPreprocessorIfdefStatement; import org.eclipse.cdt.core.dom.ast.IASTPreprocessorIfndefStatement; import org.eclipse.cdt.core.dom.ast.IASTPreprocessorIncludeStatement; import org.eclipse.cdt.core.dom.ast.IASTPreprocessorMacroDefinition; +import org.eclipse.cdt.core.dom.ast.IASTPreprocessorObjectStyleMacroDefinition; import org.eclipse.cdt.core.dom.ast.IASTPreprocessorPragmaStatement; import org.eclipse.cdt.core.dom.ast.IASTPreprocessorUndefStatement; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.LocationFactory; -import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.exception.IncorrectSyntaxException; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.exception.PreprocessorErrorException; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.exception.UnsupportedSyntaxException; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.Result; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.SkipResult; @@ -75,56 +77,38 @@ public Result visit(final IDispatcher main, final IASTNode node) { @Override public Result visit(final IDispatcher main, final IASTPreprocessorElifStatement node) { - final String msg = "PreprocessorHandler: Not yet implemented: " + node.toString(); - final ILocation loc = mLocationFactory.createCLocation(node); - mReporter.unsupportedSyntax(loc, msg); return new SkipResult(); } @Override public Result visit(final IDispatcher main, final IASTPreprocessorElseStatement node) { - final String msg = "PreprocessorHandler: Not yet implemented: " + node.toString(); - final ILocation loc = mLocationFactory.createCLocation(node); - mReporter.unsupportedSyntax(loc, msg); return new SkipResult(); } @Override public Result visit(final IDispatcher main, final IASTPreprocessorEndifStatement node) { - final String msg = "PreprocessorHandler: Not yet implemented: " + node.toString(); - final ILocation loc = mLocationFactory.createCLocation(node); - mReporter.unsupportedSyntax(loc, msg); return new SkipResult(); } @Override public Result visit(final IDispatcher main, final IASTPreprocessorErrorStatement node) { - final String msg = "PreprocessorHandler: There was an error while parsing the preprocessor statements!"; + final String msg = "PreprocessorHandler: " + node.toString(); final ILocation loc = mLocationFactory.createCLocation(node); - throw new IncorrectSyntaxException(loc, msg); + throw new PreprocessorErrorException(loc, msg); } @Override public Result visit(final IDispatcher main, final IASTPreprocessorIfdefStatement node) { - final String msg = "PreprocessorHandler: Not yet implemented: " + node.toString(); - final ILocation loc = mLocationFactory.createCLocation(node); - mReporter.unsupportedSyntax(loc, msg); return new SkipResult(); } @Override public Result visit(final IDispatcher main, final IASTPreprocessorIfndefStatement node) { - final String msg = "PreprocessorHandler: Not yet implemented: " + node.toString(); - final ILocation loc = mLocationFactory.createCLocation(node); - mReporter.unsupportedSyntax(loc, msg); return new SkipResult(); } @Override public Result visit(final IDispatcher main, final IASTPreprocessorIfStatement node) { - final String msg = "PreprocessorHandler: Not yet implemented: " + node.toString(); - final ILocation loc = mLocationFactory.createCLocation(node); - mReporter.unsupportedSyntax(loc, msg); return new SkipResult(); } @@ -135,21 +119,33 @@ public Result visit(final IDispatcher main, final IASTPreprocessorIncludeStateme @Override public Result visit(final IDispatcher main, final IASTPreprocessorMacroDefinition node) { - // this was already handled by the CDT parser... + if (node instanceof IASTPreprocessorFunctionStyleMacroDefinition) { + return visit(main, (IASTPreprocessorFunctionStyleMacroDefinition) node); + } else if (node instanceof IASTPreprocessorObjectStyleMacroDefinition) { + return visit(main, (IASTPreprocessorObjectStyleMacroDefinition) node); + } + + return new SkipResult(); + } + + public Result visit(final IDispatcher main, final IASTPreprocessorFunctionStyleMacroDefinition node) { + return new SkipResult(); + } + + public Result visit(final IDispatcher main, final IASTPreprocessorObjectStyleMacroDefinition node) { return new SkipResult(); } @Override public Result visit(final IDispatcher main, final IASTPreprocessorPragmaStatement node) { - mReporter.warn(mLocationFactory.createCLocation(node), "Ignoring preprocessor pragma"); + final String msg = "PreprocessorHandler: Ignoring preprocessor pragma " + node.toString(); + final ILocation loc = mLocationFactory.createCLocation(node); + mReporter.warn(loc, msg); return new SkipResult(); } @Override public Result visit(final IDispatcher main, final IASTPreprocessorUndefStatement node) { - final String msg = "PreprocessorHandler: Not yet implemented: " + node.toString(); - final ILocation loc = mLocationFactory.createCLocation(node); - mReporter.unsupportedSyntax(loc, msg); return new SkipResult(); } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/exception/PreprocessorErrorException.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/exception/PreprocessorErrorException.java new file mode 100644 index 00000000000..549bb211680 --- /dev/null +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/exception/PreprocessorErrorException.java @@ -0,0 +1,50 @@ +/* + * Copyright (C) 2025 Manuel Bentele (bentele@informatik.uni-freiburg.de) + * + * This file is part of the ULTIMATE CACSL2BoogieTranslator plug-in. + * + * The ULTIMATE CACSL2BoogieTranslator plug-in is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE CACSL2BoogieTranslator plug-in is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE CACSL2BoogieTranslator plug-in. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE CACSL2BoogieTranslator plug-in, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission + * to convey the resulting work. + */ +package de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.exception; + +import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; + +/** + * Exception for a preprocessor #error statement. + * + * @author Manuel Bentele (bentele@informatik.uni-freiburg.de) + */ +public class PreprocessorErrorException extends CACSL2BoogieTranslationException { + + private static final long serialVersionUID = 1L; + + /** + * Create a new exception for a preprocessor #error statement. + * + * @param location + * Location of the preprocessor statement. + * @param msg + * Detailed error message. + */ + public PreprocessorErrorException(final ILocation location, final String msg) { + super(location, msg); + } +} diff --git a/trunk/source/CDTParser/META-INF/MANIFEST.MF b/trunk/source/CDTParser/META-INF/MANIFEST.MF index e69c1a15667..4b0f58d73ec 100644 --- a/trunk/source/CDTParser/META-INF/MANIFEST.MF +++ b/trunk/source/CDTParser/META-INF/MANIFEST.MF @@ -16,5 +16,6 @@ Require-Bundle: de.uni_freiburg.informatik.ultimate.lib.core, Bundle-ActivationPolicy: lazy Bundle-RequiredExecutionEnvironment: JavaSE-21 Export-Package: de.uni_freiburg.informatik.ultimate.cdt.parser, + de.uni_freiburg.informatik.ultimate.cdt.parser.preferences, de.uni_freiburg.informatik.ultimate.cdt.decorator Automatic-Module-Name: de.uni.freiburg.informatik.ultimate.cdt.parser diff --git a/trunk/source/CDTParser/src/de/uni_freiburg/informatik/ultimate/cdt/parser/CDTParser.java b/trunk/source/CDTParser/src/de/uni_freiburg/informatik/ultimate/cdt/parser/CDTParser.java index 6a3cd1fbb8e..0ea8a13087f 100644 --- a/trunk/source/CDTParser/src/de/uni_freiburg/informatik/ultimate/cdt/parser/CDTParser.java +++ b/trunk/source/CDTParser/src/de/uni_freiburg/informatik/ultimate/cdt/parser/CDTParser.java @@ -32,12 +32,18 @@ import java.io.ByteArrayOutputStream; import java.io.File; +import java.io.FileFilter; +import java.io.FilenameFilter; +import java.io.IOException; import java.io.OutputStream; import java.io.PrintStream; +import java.util.ArrayDeque; import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; +import java.util.LinkedHashSet; import java.util.List; +import java.util.Set; import java.util.UUID; import java.util.function.BiConsumer; import java.util.stream.Collectors; @@ -130,14 +136,30 @@ public class CDTParser implements ISource { private static final IProgressMonitor NULL_MONITOR = new NullProgressMonitor(); private final String[] mFileTypes; + private final String mIncludeFileType; + private final FilenameFilter mIncludeFilesFilter; + private final FileFilter mIncludeDirectoriesFilter; private ILogger mLogger; private List mFileNames; private IUltimateServiceProvider mServices; private IProject mProject; public CDTParser() { - mFileTypes = new String[] { ".c", ".i", ".h", ".inl" }; + mIncludeFileType = new String(".h"); + mFileTypes = new String[] { ".c", ".i", mIncludeFileType, ".inl" }; mCdtPProjectHierachyFlag = "FLAG" + UUID.randomUUID().toString().substring(0, 10).replace("-", ""); + mIncludeFilesFilter = new FilenameFilter() { + @Override + public boolean accept(final File directory, final String name) { + return name.toLowerCase().endsWith(mIncludeFileType); + } + }; + mIncludeDirectoriesFilter = new FileFilter() { + @Override + public boolean accept(final File pathname) { + return pathname.isDirectory(); + } + }; } @Override @@ -276,19 +298,7 @@ private ICProject createCompleteCdtProject(final File[] files) throws CoreExcept final ICProject cProject = CoreModel.getDefault().create(mProject); cProject.setRawPathEntries(new IPathEntry[] { sourceEntry }, NULL_MONITOR); - // TODO: this adds includes and makes them resolvable, but seems like the wrong way - final String includes = - mServices.getPreferenceProvider(Activator.PLUGIN_ID).getString(PreferenceInitializer.INCLUDE_PATHS); - for (final String includePath : includes.split(";")) { - if (!new File(includePath).exists()) { - continue; - } - mLogger.info("Adding includes from " + includePath + " as file "); - final File[] includeFiles = new File(includePath).listFiles(); - for (final File f : includeFiles) { - addLinkToFolder(sourceFolder, f); - } - } + addIncludeFiles(sourceFolder, computeIncludePaths(files)); // TODO: The indexer is empty and I dont know why -- reindexing does not help // CCorePlugin.getIndexManager().reindex(cProject); @@ -303,6 +313,74 @@ private ICProject createCompleteCdtProject(final File[] files) throws CoreExcept return cProject; } + private Collection computeIncludePaths(final File[] files) { + // Include all parent dirs of the source files and all dirs from the settings afterwards + final List rawPaths = Arrays.stream(files).map(File::getParentFile).collect(Collectors.toList()); + final String includesFromSettings = + mServices.getPreferenceProvider(Activator.PLUGIN_ID).getString(PreferenceInitializer.INCLUDE_PATHS); + for (final String include : includesFromSettings.split(";")) { + final File includeDir = new File(include); + if (includeDir.isAbsolute()) { + rawPaths.add(includeDir); + continue; + } + for (final File f : files) { + try { + rawPaths.add(new File(f.getParentFile(), include).getCanonicalFile()); + } catch (final IOException e) { + // Invalid path, do nothing + continue; + } + } + } + // Exclude all duplicate and invalid paths, but keep their order. + final Collection validPaths = + rawPaths.stream().filter(File::isDirectory).collect(Collectors.toCollection(LinkedHashSet::new)); + final boolean recursive = + mServices.getPreferenceProvider(Activator.PLUGIN_ID).getBoolean(PreferenceInitializer.RECURSIVE); + if (!recursive) { + return validPaths; + } + // Add the paths recursively + final ArrayDeque queue = new ArrayDeque<>(validPaths); + final Set result = new LinkedHashSet<>(); + while (!queue.isEmpty()) { + final File f = queue.pop(); + if (result.add(f)) { + queue.addAll(Arrays.asList(f.listFiles(mIncludeDirectoriesFilter))); + } + } + return result; + } + + /** + * Add files from specified include paths to the project source folder. + * + * @param sourceFolder + * project source folder + * @param includePaths + * absolute path names where include files are located + */ + private void addIncludeFiles(final IFolder sourceFolder, final Collection includePaths) throws CoreException { + for (final File includePath : includePaths) { + // check if current include path is valid + final boolean includePathValid = includePath.exists() && includePath.isDirectory(); + if (!includePathValid) { + // skip adding invalid include path + continue; + } + + mLogger.info("Adding include files from include path " + includePath); + + // add all include files from the current include path + final File[] includeFiles = includePath.listFiles(mIncludeFilesFilter); + for (final File includeFile : includeFiles) { + mLogger.info("Adding include file " + includeFile); + addLinkToFolder(sourceFolder, includeFile); + } + } + } + /** * Print all currently available {@link ICLanguageSettingEntry}s to debug certain language settings, e.g., those * generated by org.eclipse.cdt.managedbuilder.core.GCCBuiltinSpecsDetector diff --git a/trunk/source/CDTParser/src/de/uni_freiburg/informatik/ultimate/cdt/parser/preferences/PreferenceInitializer.java b/trunk/source/CDTParser/src/de/uni_freiburg/informatik/ultimate/cdt/parser/preferences/PreferenceInitializer.java index 36cf716aeee..f171eb82241 100644 --- a/trunk/source/CDTParser/src/de/uni_freiburg/informatik/ultimate/cdt/parser/preferences/PreferenceInitializer.java +++ b/trunk/source/CDTParser/src/de/uni_freiburg/informatik/ultimate/cdt/parser/preferences/PreferenceInitializer.java @@ -39,9 +39,14 @@ public PreferenceInitializer() { @Override protected UltimatePreferenceItem[] initDefaultPreferences() { - return new UltimatePreferenceItem[] { new UltimatePreferenceItem<>(INCLUDE_PATHS, "", PreferenceType.Path) }; + // @formatter:off + return new UltimatePreferenceItem[] { + new UltimatePreferenceItem<>(INCLUDE_PATHS, "", PreferenceType.String), + new UltimatePreferenceItem<>(RECURSIVE, false, PreferenceType.Boolean) + }; + // @formatter:on } public static final String INCLUDE_PATHS = "Please specify include paths that will be parsed with the given C-File"; - + public static final String RECURSIVE = "Add include files recursively from subdirectories of include paths as well"; } diff --git a/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/PreferenceType.java b/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/PreferenceType.java index 08b93aaa9df..00f1c4e7b8c 100644 --- a/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/PreferenceType.java +++ b/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/PreferenceType.java @@ -77,8 +77,10 @@ public enum PreferenceType { */ Double, /** - * A string representing one or multiple paths to a file or directory on the system. If multiple paths are specified - * by the user, they are separated by a semicolon. + * A string representing one or multiple paths to a file or directory on the system. If multiple paths are + * specified by the user, they are separated by the system-dependent path-separator character (defined by + * {@link java.io.File#pathSeparator}). On UNIX systems, this character is ':'; on Microsoft Windows systems + * it is ';'. */ Path, /** diff --git a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ParserTestResultDecider.java b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ParserTestResultDecider.java new file mode 100644 index 00000000000..93c38e25db0 --- /dev/null +++ b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ParserTestResultDecider.java @@ -0,0 +1,47 @@ +/* + * Copyright (C) 2023 Manuel Bentele + * + * This file is part of the ULTIMATE Test Library. + * + * The ULTIMATE Test Library is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE Test Library is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE Test Library. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE Test Library, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE Test Library grant you additional permission + * to convey the resulting work. + */ + +package de.uni_freiburg.informatik.ultimate.test.decider; + +import de.uni_freiburg.informatik.ultimate.test.UltimateRunDefinition; + +/** + * A decider for parser test results based on the {@link NoErrorTestResultDecider}. + * + * @author Manuel Bentele + */ +public class ParserTestResultDecider extends NoErrorTestResultDecider { + + /** + * Construct a decider for parser test results based on the {@link NoErrorTestResultDecider}. + * + * @param urd + * Ultimate run definition of the test suite. + */ + public ParserTestResultDecider(UltimateRunDefinition urd) { + super(urd); + } +} diff --git a/trunk/source/UltimateCLI/src/de/uni_freiburg/informatik/ultimate/cli/options/OptionBuilder.java b/trunk/source/UltimateCLI/src/de/uni_freiburg/informatik/ultimate/cli/options/OptionBuilder.java index 2e2a5305d3d..ca0c26bf8c0 100644 --- a/trunk/source/UltimateCLI/src/de/uni_freiburg/informatik/ultimate/cli/options/OptionBuilder.java +++ b/trunk/source/UltimateCLI/src/de/uni_freiburg/informatik/ultimate/cli/options/OptionBuilder.java @@ -287,7 +287,8 @@ private static String createDescription(final UltimatePreferenceItem item) { break; case Path: sb.append(" is a string representing one or multiple paths to a file or directory on the system. "); - sb.append("If multiple paths are specified by the user, they are separated by a semicolon. "); + sb.append("If multiple paths are specified by the user, they are separated by the system-dependent path separator. "); + sb.append("On UNIX systems, this character is ':'; on Microsoft Windows systems it is ';'. "); break; case Integer: sb.append(" is a string representing an integer. "); diff --git a/trunk/source/UltimateTest/src/de/uni_freiburg/informatik/ultimate/ultimatetest/suites/AbstractParserTestSuite.java b/trunk/source/UltimateTest/src/de/uni_freiburg/informatik/ultimate/ultimatetest/suites/AbstractParserTestSuite.java new file mode 100644 index 00000000000..8596e0ede04 --- /dev/null +++ b/trunk/source/UltimateTest/src/de/uni_freiburg/informatik/ultimate/ultimatetest/suites/AbstractParserTestSuite.java @@ -0,0 +1,61 @@ +/* + * Copyright (C) 2023 Manuel Bentele + * + * This file is part of the ULTIMATE Test Library. + * + * The ULTIMATE Test Library is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE Test Library is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE Test Library. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE Test Library, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE Test Library grant you additional permission + * to convey the resulting work. + */ + +package de.uni_freiburg.informatik.ultimate.ultimatetest.suites; + +import de.uni_freiburg.informatik.ultimate.test.UltimateRunDefinition; +import de.uni_freiburg.informatik.ultimate.test.decider.ITestResultDecider; +import de.uni_freiburg.informatik.ultimate.test.decider.ParserTestResultDecider; +import de.uni_freiburg.informatik.ultimate.test.logs.summaries.ColumnDefinition; +import de.uni_freiburg.informatik.ultimate.test.logs.summaries.ConversionContext; +import de.uni_freiburg.informatik.ultimate.test.logs.summaries.ColumnDefinition.Aggregate; + +/** + * An {@link AbstractParserTestSuite} is a {@link AbstractEvalTestSuite} that provides a test generation functionality + * for parser tests. + * + * @author Manuel Bentele + */ +public abstract class AbstractParserTestSuite extends AbstractEvalTestSuite { + + @Override + protected ITestResultDecider constructITestResultDecider(final UltimateRunDefinition urd) { + return new ParserTestResultDecider(urd); + } + + @Override + protected ColumnDefinition[] getColumnDefinitions() { + // @formatter:off + return new ColumnDefinition[] { + new ColumnDefinition("Runtime (ns)", "Avg. runtime", + ConversionContext.Divide(1000000000, 2, " s"), Aggregate.Sum, Aggregate.Average), + new ColumnDefinition("Allocated memory end (bytes)", "Alloc. Memory", + ConversionContext.Divide(1048576, 2, " MB"), Aggregate.Max, Aggregate.Average), + new ColumnDefinition("Peak memory consumption (bytes)", "Peak Memory", + ConversionContext.Divide(1048576, 2, " MB"), Aggregate.Max, Aggregate.Average) }; + // @formatter:on + } +} diff --git a/trunk/source/UltimateTest/src/de/uni_freiburg/informatik/ultimate/ultimatetest/suites/parser/CDTParserTestSuite.java b/trunk/source/UltimateTest/src/de/uni_freiburg/informatik/ultimate/ultimatetest/suites/parser/CDTParserTestSuite.java new file mode 100644 index 00000000000..ae4a750889b --- /dev/null +++ b/trunk/source/UltimateTest/src/de/uni_freiburg/informatik/ultimate/ultimatetest/suites/parser/CDTParserTestSuite.java @@ -0,0 +1,168 @@ +/* + * Copyright (C) 2023 Manuel Bentele + * + * This file is part of the ULTIMATE Test Library. + * + * The ULTIMATE Test Library is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE Test Library is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE Test Library. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE Test Library, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE Test Library grant you additional permission + * to convey the resulting work. + */ + +package de.uni_freiburg.informatik.ultimate.ultimatetest.suites.parser; + +import java.io.File; +import java.util.Arrays; +import java.util.Collection; +import java.util.function.UnaryOperator; + +import de.uni_freiburg.informatik.ultimate.cdt.parser.preferences.PreferenceInitializer; +import de.uni_freiburg.informatik.ultimate.core.model.preferences.IPreferenceProvider; +import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider; +import de.uni_freiburg.informatik.ultimate.test.UltimateTestCase; +import de.uni_freiburg.informatik.ultimate.test.util.DirectoryFileEndingsPair; +import de.uni_freiburg.informatik.ultimate.test.util.UltimateRunDefinitionGenerator; +import de.uni_freiburg.informatik.ultimate.ultimatetest.suites.AbstractParserTestSuite; + +/** + * Test suite for the CDTParser to test parsing of C projects. + * + * @author Manuel Bentele + */ +public class CDTParserTestSuite extends AbstractParserTestSuite { + + private static final String[] ALL_C = { ".c" }; + private static final int DEFAULT_LIMIT = Integer.MAX_VALUE; + + /** + * Relative path to the standard test include directory starting from trunk. + */ + // @formatter:off + private static final String[] INCLUDE_STD_DIR = { + "examples/CParser/include" + }; + // @formatter:on + + /** + * Relative path to the extended test include directories starting from trunk. + */ + // @formatter:off + private static final String[] INCLUDE_EXD_DIRS = { + "examples/CParser/include", + "examples/CParser/include/subdirectory" + }; + // @formatter:on + + /** + * List of toolchains on which CDT parser test cases should be executed. + */ + // @formatter:off + private static final String[] TOOLCHAINS = { + "CTranslationAndBoogiePreprocessor.xml" + }; + // @formatter:on + + @Override + protected long getTimeout() { + return 10 * 1000; + } + + @Override + public Collection createTestCases() { + // @formatter:off + /** + * Test program includes local header files that are located in the same directory as the program itself. + */ + addParserTestCase("examples/CParser/includeHeadersLocal.c"); + /** + * Test program includes header files that are located in the specified {@link INCLUDE_STD_DIR}. + */ + addParserTestCase("examples/CParser/includeHeadersNonRecursiveSimple.c", false, INCLUDE_STD_DIR); + /** + * Test program includes header files that are located in the specified {@link INCLUDE_EXD_DIRS}. This test + * case corresponds to the command call 'gcc -I ${INCLUDE_EXD_DIRS[0]} -I ${INCLUDE_EXD_DIRS[1]} ...'. + */ + addParserTestCase("examples/CParser/includeHeadersNonRecursiveSubdirectory.c", false, INCLUDE_EXD_DIRS); + /** + * Test program includes header files that are located in the specified include directory and its + * subdirectories. This test case corresponds to the command call 'gcc -I ${INCLUDE_STD_DIR[0]} ...'. + */ + addParserTestCase("examples/CParser/includeHeadersRecursive.c", true, INCLUDE_STD_DIR); + // @formatter:on + + return super.createTestCases(); + } + + /** + * Add simple CDT parser test case for an input C-file. + * + * The test case commands the CDT implementation to parse the input C-file while the parser does not consider any + * include paths and their recursive header file search. + * + * @param inputFilename + * Relative file name to the input C-file starting from trunk. + */ + protected void addParserTestCase(final String inputFilename) { + addParserTestCase(inputFilename, false, new String[] {}); + } + + /** + * Add CDT parser test case for an input C-file while considering include paths and their recursive header file + * search. + * + * The test case commands the CDT implementation to parse the input C-file while the parser considers the specified + * include paths and their recursive header file search. + * + * @param inputFilename + * Relative file name to the input file starting from trunk. + * @param recursive + * Add include files recursively from subdirectories of include paths for parsing as well. + * @param includeDirectories + * List of include paths that will be parsed with the given input C-file. + */ + protected void addParserTestCase(final String inputFilename, final boolean recursive, + final String[] includeDirectories) { + + // determine absolute file paths of include paths + final String[] absolutePathsIncDirs = Arrays.stream(includeDirectories).map(includeDir -> { + final File includeDirectoryFile = UltimateRunDefinitionGenerator.getFileFromTrunkDir(includeDir); + return includeDirectoryFile.getAbsolutePath().toString(); + }).toArray(String[]::new); + + // define function to dynamically customize CDT parser settings for each test case + final UnaryOperator customizeCdtParserSettings = services -> { + final String cdtParserPluginId = de.uni_freiburg.informatik.ultimate.cdt.parser.Activator.PLUGIN_ID; + final IUltimateServiceProvider overlay = services.registerPreferenceLayer(getClass(), cdtParserPluginId); + final IPreferenceProvider prefProvider = overlay.getPreferenceProvider(cdtParserPluginId); + + final String includePaths = String.join(";", absolutePathsIncDirs); + + prefProvider.put(PreferenceInitializer.INCLUDE_PATHS, includePaths); + prefProvider.put(PreferenceInitializer.RECURSIVE, recursive); + + return overlay; + }; + + // add test case with customized CDT parser settings (include paths, etc.) for all toolchains + for (final String toolchain : TOOLCHAINS) { + final DirectoryFileEndingsPair[] inputFiles = + { new DirectoryFileEndingsPair(inputFilename, ALL_C, DEFAULT_LIMIT) }; + addTestCase(toolchain, null, inputFiles, customizeCdtParserSettings); + } + } +}