Emergentheta

.gitignore

@@ -13,6 +13,7 @@ dest/
 .classpath
 
 # Intellij
+.run/**
 .idea/**
 *.iml
 *.iws

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.
@@ -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();
     }

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.
@@ -72,6 +72,9 @@ fun <T> 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)

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.
@@ -175,6 +175,13 @@ 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,
+  @Parameter(
+    names = ["--cir-dir", "--cir-directory"],
+    description = "Folder with clang and mapper binaries",
+  )
+  var cirDir: File = File("./clang/bin"),
 ) : SpecFrontendConfig
 
 data class CHCFrontendConfig(

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.
@@ -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,35 @@ 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(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)
+      transformed
+    } else {
+      input
+    }
+
   val xcfaFromC =
     try {
       val stream = FileInputStream(input)
@@ -245,3 +279,12 @@ private fun parseChc(
     }
   return xcfaBuilder.build()
 }
+
+private fun String.runCommand(wd: File) {
+  ProcessBuilder(*split(" ").toTypedArray())
+    .directory(wd)
+    .redirectOutput(ProcessBuilder.Redirect.INHERIT)
+    .redirectError(ProcessBuilder.Redirect.INHERIT)
+    .start()
+    .waitFor(15, TimeUnit.MINUTES)
+}