From 5417faf500b63b1334ccacc2f395422f698ad159 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Mon, 17 Nov 2025 17:19:36 +0100 Subject: [PATCH 1/6] added clang preprocessing option --- .../grammar/expression/ExpressionVisitor.java | 3 ++ .../mit/theta/xcfa/cli/params/ExitCodes.kt | 3 ++ .../mit/theta/xcfa/cli/params/XcfaConfig.kt | 2 + .../mit/theta/xcfa/cli/utils/XcfaParser.kt | 43 ++++++++++++++++++- 4 files changed, 50 insertions(+), 1 deletion(-) diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java index cf4440d1ef..2be385d386 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java @@ -736,6 +736,9 @@ public Expr visitGccPrettyFunc(CParser.GccPrettyFuncContext ctx) { @Override public Expr visitPrimaryExpressionId(CParser.PrimaryExpressionIdContext ctx) { + if(ctx.getText().equals("NULL") || ctx.getText().equals("nullptr")) { + return new CPointer(null, null, parseContext).getNullValue(); + } final var variable = getVar(ctx.Identifier().getText()); return variable.getRef(); } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ExitCodes.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ExitCodes.kt index 05bea34b93..92340ff040 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ExitCodes.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ExitCodes.kt @@ -72,6 +72,9 @@ fun exitOnError(stacktrace: Boolean, throwDontExit: Boolean, body: () -> T): } catch (e: Z3Exception) { e.printCauseAndTrace(stacktrace) exitProcess(throwDontExit, e, ExitCodes.SOLVER_ERROR.code) + } catch (e: com.microsoft.z3legacy.Z3Exception) { + e.printCauseAndTrace(stacktrace) + exitProcess(throwDontExit, e, ExitCodes.SOLVER_ERROR.code) } catch (e: ClassCastException) { e.printCauseAndTrace(stacktrace) if (e.message?.contains("com.microsoft.z3") == true) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt index 456b2833e4..0e4c75a5b4 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt @@ -175,6 +175,8 @@ data class CFrontendConfig( description = "Architecture (see https://unix.org/whitepapers/64bit.html)", ) var architecture: ArchitectureConfig.ArchitectureType = ArchitectureConfig.ArchitectureType.LP64, + @Parameter(names = ["--use-cir"], description = "Use ClangIR to preprocess files") + var useCir: Boolean = false, ) : SpecFrontendConfig data class CHCFrontendConfig( diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt index 7786ccc22b..278112f7eb 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt @@ -32,6 +32,7 @@ import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.ArithmeticTra import hu.bme.mit.theta.llvm2xcfa.ArithmeticType import hu.bme.mit.theta.llvm2xcfa.XcfaUtils import hu.bme.mit.theta.xcfa.XcfaProperty +import hu.bme.mit.theta.xcfa.cli.params.CFrontendConfig import hu.bme.mit.theta.xcfa.cli.params.CHCFrontendConfig import hu.bme.mit.theta.xcfa.cli.params.ExitCodes import hu.bme.mit.theta.xcfa.cli.params.InputType @@ -43,9 +44,11 @@ import hu.bme.mit.theta.xcfa.passes.ProcedurePassManager import java.io.File import java.io.FileInputStream import java.io.FileReader +import java.util.concurrent.TimeUnit import javax.script.ScriptEngine import javax.script.ScriptEngineManager import kotlin.io.path.Path +import kotlin.io.path.createTempDirectory import kotlin.jvm.optionals.getOrNull import org.antlr.v4.runtime.CharStreams @@ -70,6 +73,7 @@ fun getXcfa( InputType.C -> { parseC( + config.frontendConfig.specConfig as CFrontendConfig, config.inputConfig.input!!, config.inputConfig.property, parseContext, @@ -148,13 +152,14 @@ private fun CFA.toXcfa(): XCFA { } private fun parseC( + frontendConfig: CFrontendConfig, input: File, property: XcfaProperty, parseContext: ParseContext, logger: Logger, uniqueWarningLogger: Logger, ): XCFA { - val input = + var input = if (input.name.endsWith(".yml")) { try { val parsedYaml = Yaml.default.parseToYamlNode(input.readText()) @@ -186,6 +191,34 @@ private fun parseC( } else { input } + + input = + if (frontendConfig.useCir) { + val temp = createTempDirectory() + val copied = temp.resolve("input.c").toFile() + var curlyBraceCount = 0 + input.readLines().forEach { line -> + line.forEach { c -> if(c == '{') curlyBraceCount++ else if(c == '}') curlyBraceCount-- } + val newLine = if(curlyBraceCount == 0 && '{' !in line) { + "([^(]*)\\(\\s*\\)".toRegex().replace(line) { + it.groups[1]!!.value + "(void)" + } + } else { + line + } + copied.appendText(newLine) + copied.appendText(System.lineSeparator()) + } + + "./clang ${copied.absolutePath} -Xclang -emit-cir-flat -fsyntax-only".runCommand() + val mlir = temp.resolve("input.mlir").toFile() + val transformed = temp.resolve("input-transformed.c").toFile() + "./xcfa-mapper ${mlir.absolutePath} ${transformed.absolutePath}".runCommand() + transformed + } else { + input + } + val xcfaFromC = try { val stream = FileInputStream(input) @@ -245,3 +278,11 @@ private fun parseChc( } return xcfaBuilder.build() } + +private fun String.runCommand() { + ProcessBuilder(*split(" ").toTypedArray()) + .redirectOutput(ProcessBuilder.Redirect.INHERIT) + .redirectError(ProcessBuilder.Redirect.INHERIT) + .start() + .waitFor(60, TimeUnit.SECONDS) +} From 870b5d6f230897d43021a94f9704730b4bc18057 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Mon, 17 Nov 2025 17:31:03 +0100 Subject: [PATCH 2/6] Added config option for cir path --- .../java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt | 2 ++ .../java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt | 7 ++++--- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt index 0e4c75a5b4..3e9a8e4ff4 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt @@ -177,6 +177,8 @@ data class CFrontendConfig( var architecture: ArchitectureConfig.ArchitectureType = ArchitectureConfig.ArchitectureType.LP64, @Parameter(names = ["--use-cir"], description = "Use ClangIR to preprocess files") var useCir: Boolean = false, + @Parameter(names = ["--cir-dir", "--cir-directory"], description = "Folder with clang and mapper binaries") + var cirDir: File = File(".") ) : SpecFrontendConfig data class CHCFrontendConfig( diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt index 278112f7eb..0b7d24ea84 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt @@ -210,10 +210,10 @@ private fun parseC( copied.appendText(System.lineSeparator()) } - "./clang ${copied.absolutePath} -Xclang -emit-cir-flat -fsyntax-only".runCommand() + "./clang ${copied.absolutePath} -Xclang -emit-cir-flat -fsyntax-only".runCommand(frontendConfig.cirDir) val mlir = temp.resolve("input.mlir").toFile() val transformed = temp.resolve("input-transformed.c").toFile() - "./xcfa-mapper ${mlir.absolutePath} ${transformed.absolutePath}".runCommand() + "./xcfa-mapper ${mlir.absolutePath} ${transformed.absolutePath}".runCommand(frontendConfig.cirDir) transformed } else { input @@ -279,8 +279,9 @@ private fun parseChc( return xcfaBuilder.build() } -private fun String.runCommand() { +private fun String.runCommand(wd: File) { ProcessBuilder(*split(" ").toTypedArray()) + .directory(wd) .redirectOutput(ProcessBuilder.Redirect.INHERIT) .redirectError(ProcessBuilder.Redirect.INHERIT) .start() From 2103d2775f4cf9043b12c7665eaa2687ba1fe2a9 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Mon, 17 Nov 2025 18:02:47 +0100 Subject: [PATCH 3/6] format --- .../grammar/expression/ExpressionVisitor.java | 6 +++--- .../mit/theta/xcfa/cli/params/XcfaConfig.kt | 7 +++++-- .../mit/theta/xcfa/cli/utils/XcfaParser.kt | 19 ++++++++++--------- 3 files changed, 18 insertions(+), 14 deletions(-) diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java index 2be385d386..8054e5a672 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java @@ -736,9 +736,9 @@ public Expr visitGccPrettyFunc(CParser.GccPrettyFuncContext ctx) { @Override public Expr visitPrimaryExpressionId(CParser.PrimaryExpressionIdContext ctx) { - if(ctx.getText().equals("NULL") || ctx.getText().equals("nullptr")) { - return new CPointer(null, null, parseContext).getNullValue(); - } + if (ctx.getText().equals("NULL") || ctx.getText().equals("nullptr")) { + return new CPointer(null, null, parseContext).getNullValue(); + } final var variable = getVar(ctx.Identifier().getText()); return variable.getRef(); } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt index 3e9a8e4ff4..c597c99a91 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt @@ -177,8 +177,11 @@ data class CFrontendConfig( var architecture: ArchitectureConfig.ArchitectureType = ArchitectureConfig.ArchitectureType.LP64, @Parameter(names = ["--use-cir"], description = "Use ClangIR to preprocess files") var useCir: Boolean = false, - @Parameter(names = ["--cir-dir", "--cir-directory"], description = "Folder with clang and mapper binaries") - var cirDir: File = File(".") + @Parameter( + names = ["--cir-dir", "--cir-directory"], + description = "Folder with clang and mapper binaries", + ) + var cirDir: File = File("."), ) : SpecFrontendConfig data class CHCFrontendConfig( diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt index 0b7d24ea84..2082c63f3d 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt @@ -198,22 +198,23 @@ private fun parseC( val copied = temp.resolve("input.c").toFile() var curlyBraceCount = 0 input.readLines().forEach { line -> - line.forEach { c -> if(c == '{') curlyBraceCount++ else if(c == '}') curlyBraceCount-- } - val newLine = if(curlyBraceCount == 0 && '{' !in line) { - "([^(]*)\\(\\s*\\)".toRegex().replace(line) { - it.groups[1]!!.value + "(void)" + line.forEach { c -> if (c == '{') curlyBraceCount++ else if (c == '}') curlyBraceCount-- } + val newLine = + if (curlyBraceCount == 0 && '{' !in line) { + "([^(]*)\\(\\s*\\)".toRegex().replace(line) { it.groups[1]!!.value + "(void)" } + } else { + line } - } else { - line - } copied.appendText(newLine) copied.appendText(System.lineSeparator()) } - "./clang ${copied.absolutePath} -Xclang -emit-cir-flat -fsyntax-only".runCommand(frontendConfig.cirDir) + "./clang ${copied.absolutePath} -Xclang -emit-cir-flat -fsyntax-only" + .runCommand(frontendConfig.cirDir) val mlir = temp.resolve("input.mlir").toFile() val transformed = temp.resolve("input-transformed.c").toFile() - "./xcfa-mapper ${mlir.absolutePath} ${transformed.absolutePath}".runCommand(frontendConfig.cirDir) + "./xcfa-mapper ${mlir.absolutePath} ${transformed.absolutePath}" + .runCommand(frontendConfig.cirDir) transformed } else { input From 0f3be9b3c6726cf3c1471a38ef9d0a6ad4f1be72 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Mon, 17 Nov 2025 22:17:27 +0100 Subject: [PATCH 4/6] Added lager timeout to clang and xcfa-mapper --- .../src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt index 2082c63f3d..90e91a55ba 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt @@ -286,5 +286,5 @@ private fun String.runCommand(wd: File) { .redirectOutput(ProcessBuilder.Redirect.INHERIT) .redirectError(ProcessBuilder.Redirect.INHERIT) .start() - .waitFor(60, TimeUnit.SECONDS) + .waitFor(15, TimeUnit.MINUTES) } From 4b8024a47beb321c222cff3498ec28453202455e Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Fri, 27 Mar 2026 12:51:13 +0100 Subject: [PATCH 5/6] spotless --- .run/verif-example-locks142.run.xml | 14 ++++++++++++++ .../grammar/expression/ExpressionVisitor.java | 2 +- .../hu/bme/mit/theta/xcfa/cli/params/ExitCodes.kt | 2 +- .../hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt | 4 ++-- .../hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt | 2 +- 5 files changed, 19 insertions(+), 5 deletions(-) create mode 100644 .run/verif-example-locks142.run.xml diff --git a/.run/verif-example-locks142.run.xml b/.run/verif-example-locks142.run.xml new file mode 100644 index 0000000000..cad564fed3 --- /dev/null +++ b/.run/verif-example-locks142.run.xml @@ -0,0 +1,14 @@ + + + + \ No newline at end of file diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java index 8054e5a672..08b62a42e1 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java @@ -1,5 +1,5 @@ /* - * Copyright 2025 Budapest University of Technology and Economics + * Copyright 2025-2026 Budapest University of Technology and Economics * * Licensed under the Apache License, Version 2.0 (the "License"); * you may not use this file except in compliance with the License. diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ExitCodes.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ExitCodes.kt index 92340ff040..31af57f0a1 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ExitCodes.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ExitCodes.kt @@ -1,5 +1,5 @@ /* - * Copyright 2025 Budapest University of Technology and Economics + * Copyright 2025-2026 Budapest University of Technology and Economics * * Licensed under the Apache License, Version 2.0 (the "License"); * you may not use this file except in compliance with the License. diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt index c597c99a91..333d67d27f 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt @@ -1,5 +1,5 @@ /* - * Copyright 2025 Budapest University of Technology and Economics + * Copyright 2025-2026 Budapest University of Technology and Economics * * Licensed under the Apache License, Version 2.0 (the "License"); * you may not use this file except in compliance with the License. @@ -181,7 +181,7 @@ data class CFrontendConfig( names = ["--cir-dir", "--cir-directory"], description = "Folder with clang and mapper binaries", ) - var cirDir: File = File("."), + var cirDir: File = File("./clang/bin"), ) : SpecFrontendConfig data class CHCFrontendConfig( diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt index 90e91a55ba..9953270f6e 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt @@ -1,5 +1,5 @@ /* - * Copyright 2025 Budapest University of Technology and Economics + * Copyright 2025-2026 Budapest University of Technology and Economics * * Licensed under the Apache License, Version 2.0 (the "License"); * you may not use this file except in compliance with the License. From 9140957a5faaee53554a9079834f854287273a27 Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Fri, 27 Mar 2026 12:51:55 +0100 Subject: [PATCH 6/6] intellij run config dir in gitignore --- .gitignore | 1 + .run/verif-example-locks142.run.xml | 14 -------------- 2 files changed, 1 insertion(+), 14 deletions(-) delete mode 100644 .run/verif-example-locks142.run.xml diff --git a/.gitignore b/.gitignore index a72bb48ba5..6e3dc80a2c 100644 --- a/.gitignore +++ b/.gitignore @@ -13,6 +13,7 @@ dest/ .classpath # Intellij +.run/** .idea/** *.iml *.iws diff --git a/.run/verif-example-locks142.run.xml b/.run/verif-example-locks142.run.xml deleted file mode 100644 index cad564fed3..0000000000 --- a/.run/verif-example-locks142.run.xml +++ /dev/null @@ -1,14 +0,0 @@ - - - - \ No newline at end of file