Merge branch 'xcfa-refactor' into interproc

subprojects/frontends/c-frontend/src/main/antlr/C.g4

@@ -933,7 +933,6 @@ LineDirective
 
 PragmaDirective
     :   '#' Whitespace? 'pragma' Whitespace ~[\r\n]*
-        -> skip
     ;
 
 Whitespace

subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibSolverInstaller.java

@@ -34,7 +34,9 @@
 import java.util.List;
 
 import static hu.bme.mit.theta.common.OsHelper.Architecture.X64;
-import static hu.bme.mit.theta.common.OsHelper.OperatingSystem.*;
+import static hu.bme.mit.theta.common.OsHelper.OperatingSystem.LINUX;
+import static hu.bme.mit.theta.common.OsHelper.OperatingSystem.MAC;
+import static hu.bme.mit.theta.common.OsHelper.OperatingSystem.WINDOWS;
 
 public class CVC5SmtLibSolverInstaller extends SmtLibSolverInstaller.Default {
     private final List<SemVer.VersionDecoder> versions;
@@ -68,6 +70,15 @@ protected void installSolver(final Path installDir, final String version) throws
         } catch (IOException e) {
             throw new SmtLibSolverInstallerException(e);
         }
+        try (
+                final var inputChannel = Channels.newChannel(getLicenseDownloadUrl().openStream());
+                final var outputChannel = new FileOutputStream(installDir.resolve("COPYING").toAbsolutePath().toString()).getChannel()
+        ) {
+            logger.write(Logger.Level.MAINSTEP, "Starting license download (%s)...\n", getLicenseDownloadUrl().toString());
+            outputChannel.transferFrom(inputChannel, 0, Long.MAX_VALUE);
+        } catch (IOException e) {
+            throw new SmtLibSolverInstallerException(e);
+        }
 
         logger.write(Logger.Level.MAINSTEP, "Download finished\n");
     }
@@ -108,6 +119,10 @@ version, getArchString(version)
         )).toURL();
     }
 
+    private URL getLicenseDownloadUrl() throws SmtLibSolverInstallerException, MalformedURLException {
+        return URI.create("https://raw.githubusercontent.com/cvc5/cvc5/main/COPYING").toURL();
+    }
+
     private String getArchString(final String version) throws SmtLibSolverInstallerException {
         final var semVer = SemVer.of(version);
         String archStr = null;

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExitCodes.kt

@@ -18,6 +18,7 @@ package hu.bme.mit.theta.xcfa.cli
 
 import com.microsoft.z3.Z3Exception
 import hu.bme.mit.theta.common.exception.NotSolvableException
+import hu.bme.mit.theta.solver.UnknownSolverStatusException
 import hu.bme.mit.theta.solver.smtlib.solver.SmtLibSolverException
 import hu.bme.mit.theta.solver.validator.SolverValidationException
 import kotlin.system.exitProcess
@@ -75,9 +76,12 @@ fun <T> exitOnError(stacktrace: Boolean, debug: Boolean, body: () -> T): T {
     } catch (e: OutOfMemoryError) {
         e.printCauseAndTrace(stacktrace)
         exitProcess(debug, e, ExitCodes.OUT_OF_MEMORY.code);
+    } catch (e: UnknownSolverStatusException) {
+        e.printCauseAndTrace(stacktrace)
+        exitProcess(debug, e, ExitCodes.SOLVER_ERROR.code);
     } catch (e: RuntimeException) {
         e.printCauseAndTrace(stacktrace)
-        if (e.message?.contains("Solver problem") == true) {
+        if (e.message?.contains("Solver problem") == true || e.message?.contains("Z3") == true) {
             exitProcess(debug, e, ExitCodes.SOLVER_ERROR.code);
         } else {
             exitProcess(debug, e, ExitCodes.SERVER_ERROR.code);

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt

@@ -225,6 +225,8 @@ data class XcfaCegarConfig(
         logger: Logger, parseContext: ParseContext, argdebug: Boolean): () -> SafetyResult<*, *> {
         val pb = NuProcessBuilder(listOf(
             getJavaExecutable(),
+            "-Xss120m",
+            "-Xmx14210m",
             "-cp",
             File(XcfaCegarServer::class.java.protectionDomain.codeSource.location.toURI()).absolutePath,
             XcfaCegarServer::class.qualifiedName,

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt

@@ -45,6 +45,7 @@ import hu.bme.mit.theta.frontend.ParseContext
 import hu.bme.mit.theta.frontend.chc.ChcFrontend
 import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig
 import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig.ArithmeticType
+import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.ArithmeticTrait
 import hu.bme.mit.theta.llvm2xcfa.XcfaUtils.fromFile
 import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager
 import hu.bme.mit.theta.xcfa.analysis.ErrorDetection
@@ -242,7 +243,7 @@ class XcfaCli(private val args: Array<String>) {
         stopwatch.reset().start()
 
         val safetyResult: SafetyResult<*, *> =
-            if (xcfa.procedures.all { it.errorLoc.isEmpty && explicitProperty != ErrorDetection.NO_ERROR }) {
+            if (xcfa.procedures.all { it.errorLoc.isEmpty && explicitProperty == ErrorDetection.ERROR_LOCATION }) {
                 registerAllSolverManagers(solverHome, logger)
                 SafetyResult.safe(ARG.create { _, _ -> false })
             } else if (backend == Backend.CEGAR) {
@@ -471,8 +472,10 @@ class XcfaCli(private val args: Array<String>) {
                             parseContext.arithmetic = ArchitectureConfig.ArithmeticType.bitvector
                             logger.write(Logger.Level.INFO, "Retrying parsing with bitvector arithmetic...\n")
                             val stream = FileInputStream(input!!)
-                            getXcfaFromC(stream, parseContext, false,
+                            val xcfa = getXcfaFromC(stream, parseContext, false,
                                 explicitProperty == ErrorDetection.OVERFLOW, uniqueWarningLogger).first
+                            parseContext.arithmeticTraits.add(ArithmeticTrait.BITWISE)
+                            xcfa
                         } else {
                             throw e
                         }

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt

@@ -74,25 +74,22 @@ fun complexPortfolio24(
         }
     }
     val timeoutTrigger = ExceptionTrigger(
-        ErrorCodeException(ExitCodes.TIMEOUT.code),
-        ErrorCodeException(ExitCodes.VERIFICATION_STUCK.code),
-        ErrorCodeException(ExitCodes.OUT_OF_MEMORY.code),
-        ErrorCodeException(ExitCodes.GENERIC_ERROR.code),
+        fallthroughExceptions = setOf(
+            ErrorCodeException(ExitCodes.SOLVER_ERROR.code),
+            ErrorCodeException(ExitCodes.SERVER_ERROR.code),
+        ),
         label = "TimeoutOrGenericError"
     )
 
     val timeoutOrSolverError = ExceptionTrigger(
-        ErrorCodeException(ExitCodes.SOLVER_ERROR.code),
-        ErrorCodeException(ExitCodes.TIMEOUT.code),
-        ErrorCodeException(ExitCodes.VERIFICATION_STUCK.code),
-        ErrorCodeException(ExitCodes.OUT_OF_MEMORY.code),
-        ErrorCodeException(ExitCodes.GENERIC_ERROR.code),
+        fallthroughExceptions = setOf(
+            ErrorCodeException(ExitCodes.SERVER_ERROR.code),
+        ),
         label = "TimeoutOrSolverError"
     )
 
     val solverError = ExceptionTrigger(
         ErrorCodeException(ExitCodes.SOLVER_ERROR.code),
-        ErrorCodeException(ExitCodes.VERIFICATION_STUCK.code),
         label = "SolverError"
     )