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

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",

regression-tests/horn-hcc-2/Answers

@@ -255,9 +255,6 @@ UNSAFE
 
 switch2.hcc
 Warning: no definition of function "nondet" available
-Warning: no definition of function "nondet" available
-Warning: no definition of function "nondet" available
-Warning: no definition of function "nondet" available
 SAFE
 
 hints.hcc

regression-tests/toh-contract-translation/Answers

@@ -1,7 +1,6 @@
 
 get-1.c
 Warning: no definition of function "non_det_int" available
-Warning: no definition of function "non_det_int" available
 Warning: no definition of function "non_det_int_ptr" available
 
 Inferred ACSL annotations
@@ -17,8 +16,6 @@ SAFE
 
 incdec-1.c
 Warning: no definition of function "non_det_int" available
-Warning: no definition of function "non_det_int" available
-Warning: no definition of function "non_det_int_ptr" available
 Warning: no definition of function "non_det_int_ptr" available
 
 Inferred ACSL annotations
@@ -60,9 +57,6 @@ SAFE
 max-1.c
 Warning: no definition of function "non_det_int" available
 Warning: no definition of function "non_det_int_ptr" available
-Warning: no definition of function "non_det_int_ptr" available
-Warning: no definition of function "non_det_int" available
-Warning: no definition of function "non_det_int" available
 
 Inferred ACSL annotations
 ================================================================================
@@ -77,9 +71,6 @@ SAFE
 
 max-2.c
 Warning: no definition of function "non_det_int_ptr" available
-Warning: no definition of function "non_det_int_ptr" available
-Warning: no definition of function "non_det_int_ptr" available
-Warning: no definition of function "non_det_int" available
 Warning: no definition of function "non_det_int" available
 
 Inferred ACSL annotations
@@ -95,9 +86,6 @@ SAFE
 
 multadd-1.c
 Warning: no definition of function "non_det_int_ptr" available
-Warning: no definition of function "non_det_int_ptr" available
-Warning: no definition of function "non_det_int_ptr" available
-Warning: no definition of function "non_det_int" available
 Warning: no definition of function "non_det_int" available
 Warning: The following clause has different terms with the same name (term: b:12)
 main_12(@h_post, a_post, b_post, result_post, a_init_post, b_init_post) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13), addTwoNumbers_post(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13, @h_post, a_post, b_post, result_post, a_init_post, b_init_post).

regression-tests/uninterpreted-predicates/Answers

@@ -1,15 +1,10 @@
 
 pred-hint.c
 Warning: no definition of function "nondet" available
-Warning: no definition of function "nondet" available
 SAFE
 
 pred-hint-loop.c
 Warning: no definition of function "nondet" available
-Warning: no definition of function "nondet" available
-Warning: no definition of function "nondet" available
-Warning: no definition of function "nondet" available
-Warning: no definition of function "nondet" available
 SAFE
 
 unint-pred-simple-false.c

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 {

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(

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