diff --git a/src/tricera/Main.scala b/src/tricera/Main.scala index c458d74..8830351 100644 --- a/src/tricera/Main.scala +++ b/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 => { diff --git a/src/tricera/concurrency/TriCeraPreprocessor.scala b/src/tricera/concurrency/TriCeraPreprocessor.scala index 1e5daa6..b7340e9 100644 --- a/src/tricera/concurrency/TriCeraPreprocessor.scala +++ b/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" + diff --git a/src/tricera/params/TriCeraParameters.scala b/src/tricera/params/TriCeraParameters.scala index 3dcbb1f..90fced1 100644 --- a/src/tricera/params/TriCeraParameters.scala +++ b/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: 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 + } } diff --git a/src/tricera/parsers/CommentPreprocessor.scala b/src/tricera/parsers/CommentPreprocessor.scala index 40a417d..686a967 100644 --- a/src/tricera/parsers/CommentPreprocessor.scala +++ b/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) {