Fix -logSimplified, new -dumpSimplified option, bump version.

uuverifiers · Jun 26, 2024 · d5f1955 · d5f1955
1 parent d1e803f
commit d5f1955
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 11 deletions.
diff --git a/build.sbt b/build.sbt
@@ -5,7 +5,7 @@ import java.nio.file.attribute.PosixFilePermission._
 lazy val commonSettings = Seq(
     name                 := "TriCera",
     organization         := "uuverifiers",
-    version              := "0.3",
+    version              := "0.3.1",
     homepage             := Some(url("https://github.com/uuverifiers/tricera")),
     licenses             := Seq("BSD-3-Clause" -> url("https://opensource.org/licenses/BSD-3-Clause")),
     description          := "TriCera is a model checker for C programs.",
@@ -98,7 +98,7 @@ settings(
                                       }}).value,
   resolvers += "uuverifiers" at "https://eldarica.org/maven/",
   libraryDependencies += "uuverifiers" %% "eldarica" % "2.1",
-  libraryDependencies += "uuverifiers" %% "horn-concurrency" % "2.1",
+  libraryDependencies += "uuverifiers" %% "horn-concurrency" % "2.1.1",
   libraryDependencies += "net.jcazevedo" %% "moultingyaml" % "0.4.2",
   libraryDependencies += "org.scalactic" %% "scalactic" % "3.2.12",
   libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.12" % "test",

diff --git a/src/tricera/Main.scala b/src/tricera/Main.scala
@@ -33,16 +33,12 @@ package tricera
 import java.io.{FileOutputStream, PrintStream}
 import java.nio.file.{Files, Paths}
 import sys.process._
-
 import ap.parser.IExpression.{ConstantTerm, Predicate}
 import ap.parser.{IAtom, IConstant, IFormula, VariableSubstVisitor}
-
 import hornconcurrency.ParametricEncoder
-
 import lazabs.horn.bottomup.HornClauses.Clause
 import lazabs.horn.Util.NullStream
 import lazabs.prover._
-
 import tricera.concurrency.{CCReader, TriCeraPreprocessor}
 import tricera.Util.{SourceInfo, printlnDebug}
 import tricera.benchmarking.Benchmarking._
@@ -259,7 +255,10 @@ class Main (args: Array[String]) {
     if (princess)
       Prover.setProver(lazabs.prover.TheoremProver.PRINCESS)
     val outStream =
-      if (logStat) Console.err else NullStream
+      if (logStat || printHornSimplified || printHornSimplifiedSMT)
+        Console.err
+      else
+        NullStream
 
     Console.withOut(outStream) {
       println(
@@ -491,7 +490,8 @@ class Main (args: Array[String]) {
           new hornconcurrency.VerificationLoop(
             system = smallSystem,
             initialInvariants = null,
-            printIntermediateClauseSets = printIntermediateClauseSets,
+            dumpIntermediateClauses = printIntermediateClauseSets,
+            dumpSimplifiedClauses = dumpSimplifiedClauses,
             fileName = smtFileName,
             expectedStatus = expectedStatus,
             log = needFullSolution,
@@ -515,7 +515,8 @@ class Main (args: Array[String]) {
 
     val result = verificationLoop.result
 
-    if (printIntermediateClauseSets)
+    if (printIntermediateClauseSets || dumpSimplifiedClauses ||
+        printHornSimplified || printHornSimplifiedSMT)
       return ExecutionSummary(DidNotExecute, Map(), modelledHeap, 0, preprocessTimer.s)
 
     val executionResult = result match {

diff --git a/src/tricera/concurrency/CCReader.scala b/src/tricera/concurrency/CCReader.scala
@@ -361,6 +361,7 @@ class CCReader private (prog              : Program,
 
   private val functionDefs  = new MHashMap[String, Function_def]
   private val functionDecls = new MHashMap[String, (Direct_declarator, CCType)]
+  private val warnedFunctionNames = new MHashSet[String]
   private val functionContexts = new MHashMap[String, FunctionContext]
   private val functionPostOldArgs = new MHashMap[String, Seq[CCVar]]
   private val functionClauses =
@@ -3903,8 +3904,11 @@ private def collectVarDecls(dec                    : Dec,
           resetFields(functionExit)
         case None => (functionDecls get name) match {
           case Some((fundecl, typ)) =>
-            if (!(name contains "__VERIFIER_nondet" ))
+            if (!name.contains("__VERIFIER_nondet") &&
+                !warnedFunctionNames.contains(name)) {
               warn("no definition of function \"" + name + "\" available")
+              warnedFunctionNames += name
+            }
             pushFormalVal(typ, Some(getSourceInfo(fundecl)))
           case None =>
             throw new TranslationException(

diff --git a/src/tricera/params/TriCeraParameters.scala b/src/tricera/params/TriCeraParameters.scala
@@ -55,6 +55,8 @@ class TriCeraParameters extends GlobalParameters {
 
   var cPreprocessor : Boolean = false
 
+  var dumpSimplifiedClauses : Boolean = false
+
   var showVarLineNumbersInTerms : Boolean = false
 
   /**
@@ -121,7 +123,7 @@ class TriCeraParameters extends GlobalParameters {
   override def withAndWOTemplates : Seq[TriCeraParameters] =
     for (p <- super.withAndWOTemplates) yield p.asInstanceOf[TriCeraParameters]
 
-  private val version = "0.3"
+  private val version = "0.3.1"
 
   private val greeting =
     "TriCera v" + version + ".\n(C) Copyright " +
@@ -143,6 +145,7 @@ class TriCeraParameters extends GlobalParameters {
     case "-noPP" :: rest => noPP = true; parseArgs(rest)
     case "-cpp"  :: rest => cPreprocessor = true; parseArgs(rest)
     case "-dumpClauses" :: rest => printIntermediateClauseSets = true; parseArgs(rest)
+    case "-dumpSimplified" :: rest => dumpSimplifiedClauses = true; parseArgs(rest)
     case "-sp" :: rest => smtPrettyPrint = true; parseArgs(rest)
     //      case "-pnts" :: rest => ntsPrint = true; arguments(rest)
     case "-disj" :: rest => disjunctive = true; parseArgs(rest)
@@ -258,6 +261,7 @@ class TriCeraParameters extends GlobalParameters {
                                     .split(",").toSet
       parseArgs(rest)
     case "-logSimplified" :: rest => printHornSimplified = true; parseArgs(rest)
+    case "-logSimplifiedSMT" :: rest => printHornSimplifiedSMT = true; parseArgs(rest)
     case "-dot" :: str :: rest => dotSpec = true; dotFile = str; parseArgs(rest)
     case "-pngNo" :: rest => pngNo = true; parseArgs(rest)
     case "-dotCEX" :: rest => pngNo = false; parseArgs(rest)
@@ -339,6 +343,8 @@ class TriCeraParameters extends GlobalParameters {
     |-pDot              Pretty-print Horn clauses, output in dot format and display it
     |-sp                Pretty-print the Horn clauses in SMT-LIB format
     |-dumpClauses       Write the Horn clauses in SMT-LIB format to input filename.smt2
+    |-dumpSimplified    Write simplified Horn clauses in SMT-LIB format to input filename.smt2
+    |                   The printed clauses are the ones after Eldarica's default preprocessor
     |-varLines          Print program variables in clauses together with their line numbers (e.g., x:42)
 
     |Horn engine options (Eldarica):
@@ -362,6 +368,8 @@ class TriCeraParameters extends GlobalParameters {
     |-splitClauses:n    Aggressiveness when splitting disjunctions in clauses
     |                     (0 <= n <= 2, default: 1)
     |-pHints            Print initial predicates and abstraction templates
+    |-logSimplified     Show clauses after Eldarica preprocessing in Prolog format
+    |-logSimplifiedSMT  Show clauses after Eldarica preprocessing in SMT-LIB format
 
     |TriCera preprocessor:
     |-printPP           Print the output of the TriCera preprocessor to stdout