Merge branch 'master' into oskar-heap-translation

src/tricera/Main.scala

@@ -135,18 +135,14 @@ class Main (args: Array[String]) {
     val cppFileName = if (cPreprocessor) {
       val preprocessedFile = File.createTempFile("tri-", ".i")
       System.setOut(new PrintStream(new FileOutputStream(preprocessedFile)))
-      val cmdLine = "cpp " + fileName + " -E -P -CC"
-      try {
-        cmdLine !
-      }
+      val cmdLine = Seq("cpp", fileName, "-E", "-P", "-CC")
+      try Process(cmdLine) !
       catch {
         case _: Throwable =>
-          throw new Main.MainException("The preprocessor could not" +
-            " be executed. This might be due to TriCera preprocessor binary " +
-            "not being in the current directory. Alternatively, use the " +
-            "-noPP switch to disable the preprocessor.\n" +
-            "Preprocessor command: " + cmdLine
-          )
+          throw new Main.MainException("The C preprocessor could not" +
+            " be executed (option -cpp). This might be due cpp not being " +
+            "installed in the system.\n" + "Attempted command: " +
+            cmdLine.mkString(" "))
       }
       preprocessedFile.deleteOnExit()
       preprocessedFile.getAbsolutePath
@@ -391,11 +387,19 @@ class Main (args: Array[String]) {
     val verificationLoop =
       try {
         Console.withOut(outStream) {
-          new hornconcurrency.VerificationLoop(smallSystem, null,
-            printIntermediateClauseSets, fileName + ".smt2",
-            expectedStatus = expectedStatus, log = needFullSolution,
+          new hornconcurrency.VerificationLoop(
+            system = smallSystem,
+            initialInvariants = null,
+            printIntermediateClauseSets = printIntermediateClauseSets,
+            fileName = fileName + ".smt2",
+            expectedStatus = expectedStatus,
+            log = needFullSolution,
             templateBasedInterpolation = templateBasedInterpolation,
-            templateBasedInterpolationTimeout = templateBasedInterpolationTimeout)
+            templateBasedInterpolationTimeout = templateBasedInterpolationTimeout,
+            symbolicExecutionEngine = symexEngine,
+            symbolicExecutionDepth = symexMaxDepth,
+            logSymbolicExecution = log
+          )
         }
       } catch {
         case TimeoutException => {

src/tricera/concurrency/TriCeraPreprocessor.scala

@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2021-2022 Zafer Esen. All rights reserved.
+ * Copyright (c) 2021-2023 Zafer Esen. All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -32,7 +32,7 @@ package tricera.concurrency
 import tricera.Main
 
 import sys.process._
-import java.nio.file.{Paths, Files}
+import java.nio.file.{Files, Paths}
 
 class TriCeraPreprocessor(val inputFilePath   : String,
                           val outputFilePath  : String,
@@ -50,21 +50,16 @@ class TriCeraPreprocessor(val inputFilePath   : String,
         "variable TRI_PP_PATH is exported and points to the preprocessor's" +
         " base directory")
   }
-  private val cmdLine = List(
-    ppPath,
-    inputFilePath,
-    "-o " + outputFilePath,
-    if(quiet) "-q" else "",
-    "-m " + entryFunction,
-    "--",
-    "-xc",
-    if(displayWarnings) "" else "-Wno-everything"
-    ).mkString(" ")
-  val returnCode =
-    try { cmdLine !}
+  private val cmdLine : Seq[String] =
+    Seq(ppPath.toString, inputFilePath,"-o", outputFilePath) ++
+    (if(quiet) Seq("-q") else Nil) ++
+    Seq("-m", entryFunction, "--", "-xc") ++
+    (if(displayWarnings) Nil else Seq("-Wno-everything"))
+  private val returnCode =
+    try { Process(cmdLine) ! }
     catch {
       case _: Throwable =>
-        throw new Main.MainException("The preprocessor could not" +
+        throw new Main.MainException("TriCera preprocessor could not" +
           " be executed. This might be due to TriCera preprocessor binary " +
           "not being in the current directory. Alternatively, use the " +
           "-noPP switch to disable the preprocessor.\n" +

src/tricera/params/TriCeraParameters.scala

@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2015-2022 Zafer Esen, Philipp Ruemmer. All rights reserved.
+ * Copyright (c) 2015-2023 Zafer Esen, Philipp Ruemmer. All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -93,7 +93,7 @@ class TriCeraParameters extends GlobalParameters {
 
   private val greeting =
     "TriCera v" + version + ".\n(C) Copyright " +
-      "2012-2022 Zafer Esen and Philipp Ruemmer\n" +
+      "2012-2023 Zafer Esen and Philipp Ruemmer\n" +
     "Contributors: Pontus Ernstedt, Hossein Hojjat"
 
   private def parseArgs(args: List[String], shouldExecute : Boolean = true): Boolean =
@@ -238,11 +238,28 @@ class TriCeraParameters extends GlobalParameters {
     case "-dev" :: rest => devMode = true; showVarLineNumbersInTerms = true; parseArgs(rest)
     case "-debug" :: rest => printDebugMessages = true; parseArgs(rest)
     case "-varLines" :: rest => showVarLineNumbersInTerms = true; parseArgs(rest)
-    case "-v" :: rest => println(version); false
-    case "-h" :: rest => println(greeting + "\n\nUsage: tri [options] file\n\n" +
+    case "-sym" :: rest      =>
+      symexEngine = GlobalParameters.SymexEngine.BreadthFirstForward
+      parseArgs(rest)
+    case symexOpt :: rest if (symexOpt.startsWith("-sym:")) =>
+      symexEngine = symexOpt.drop("-sym:".length) match {
+        case "dfs" => GlobalParameters.SymexEngine.DepthFirstForward
+        case "bfs" => GlobalParameters.SymexEngine.BreadthFirstForward
+        case _     =>
+          println("Unknown argument for -sym:, defaulting to bfs.")
+          GlobalParameters.SymexEngine.BreadthFirstForward
+      }
+      parseArgs(rest)
+    case symexDepthOpt :: rest if (symexDepthOpt.startsWith("-symDepth:")) =>
+      symexMaxDepth = Some(symexDepthOpt.drop("-symDepth:".length).toInt)
+      parseArgs(rest)
+    case arg :: rest if Set("-v", "--version").contains(arg) =>
+      println(version); false
+    case arg :: rest if Set("-h", "--help").contains(arg) =>
+      println(greeting + "\n\nUsage: tri [options] file\n\n" +
       "General options:\n" +
-      " -h\t\tShow this information\n" +
-      " -v\t\tPrint version number\n" +
+      " -h, --help\t\tShow this information\n" +
+      " -v, --version\tPrint version number\n" +
       " -arithMode:t\tInteger semantics: math (default), ilp32, lp64, llp64\n" +
       " -mathArrays:t\tUse mathematical arrays for modeling program arrays (no implicit memory safety properties))\n" +
       " -memtrack\tCheck that there are no memory leaks in the input program \n" +
@@ -256,8 +273,9 @@ class TriCeraParameters extends GlobalParameters {
       " -acsl\t\tPrint inferred ACSL annotations\n" +
       " -log:n            Display progress based on verbosity level n (0 <= n <= 3)\n" +
       "                     1: Statistics only\n" +
-      "                     2: Invariants included\n" +
-      "                     3: Includes counterexamples\n" +
+      "                     2: Include invariants\n" +
+      "                     3: Include counterexamples\n" +
+      "                     (When using -sym, n > 1 displays derived clauses.) \n" +
       " -statistics       Equivalent to -log:1; displays statistics only\n" +
       " -log              Equivalent to -log:2; displays progress and invariants\n" +
       " -logPreds:<preds> Log only predicates containing the specified substrings,\n" +
@@ -274,6 +292,12 @@ class TriCeraParameters extends GlobalParameters {
       " -varLines\tPrint program variables in clauses together with their line numbers (e.g., x:42)\n" +
       "\n" +
       "Horn engine options (Eldarica):\n" +
+      " -sym            (Experimental) Use symbolic execution with the default engine (bfs)\n" +
+      " -sym:x          Use symbolic execution where x : {dfs, bfs}\n" +
+      "                      dfs: depth-first forward (does not support non-linear clauses)\n" +
+      "                      bfs: breadth-first forward\n" +
+      " -symDepth:n     Set a max depth for symbolic execution (underapproximate)\n" +
+      "                     (currently only supported with bfs)\n" +
       " -disj\t\tUse disjunctive interpolation\n" +
       " -stac\t\tStatic acceleration of loops\n" +
       " -lbe\t\tDisable preprocessor (e.g., clause inlining)\n" +
@@ -316,8 +340,20 @@ class TriCeraParameters extends GlobalParameters {
     if (args isEmpty) {
       doNotExecute = true
       showHelp
-    } else if (!parseArgs(args)) {
+    } else if (!parseArgs(reconstructSpaceSeparatedArgs(args))) {
       doNotExecute = true
     }
   }
+
+  private def reconstructSpaceSeparatedArgs(args: List[String]): List[String] = {
+    args.foldLeft((List[String](), Option.empty[String])) {
+      case ((acc, Some(buffer)), arg) => (acc :+ (buffer + " " + arg), None)
+      case ((acc, None), arg) =>
+        if (arg.endsWith("\\")) {
+          (acc, Some(arg.dropRight(1)))
+        } else {
+          (acc :+ arg, None)
+        }
+    }._1
+  }
 }

src/tricera/parsers/CommentPreprocessor.scala

@@ -41,7 +41,7 @@ object CommentPreprocessor {
     var isInComment = false
 
     var line: String = reader.readLine
-    var newLine = new scala.collection.mutable.StringBuilder(line.length)
+    val newLine = new scala.collection.mutable.StringBuilder(line.length)
     var curInd = 0
 
     while (line != null) {