From 094ab38915f1826c8857da5e4e2cadc3aa4dcdf7 Mon Sep 17 00:00:00 2001 From: Zafer Esen Date: Wed, 26 Jun 2024 03:15:30 +0200 Subject: [PATCH] Fix -logSimplified, new -dumpSimplified option, bump version. --- build.sbt | 4 ++-- regression-tests/horn-hcc-2/Answers | 3 --- regression-tests/toh-contract-translation/Answers | 12 ------------ regression-tests/uninterpreted-predicates/Answers | 5 ----- src/tricera/Main.scala | 15 ++++++++------- src/tricera/concurrency/CCReader.scala | 6 +++++- src/tricera/params/TriCeraParameters.scala | 10 +++++++++- 7 files changed, 24 insertions(+), 31 deletions(-) diff --git a/build.sbt b/build.sbt index d06bea2..55dd612 100644 --- 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/regression-tests/horn-hcc-2/Answers b/regression-tests/horn-hcc-2/Answers index 7f7205a..d02c0ca 100644 --- a/regression-tests/horn-hcc-2/Answers +++ b/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 diff --git a/regression-tests/toh-contract-translation/Answers b/regression-tests/toh-contract-translation/Answers index f0ade9c..d531743 100644 --- a/regression-tests/toh-contract-translation/Answers +++ b/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). diff --git a/regression-tests/uninterpreted-predicates/Answers b/regression-tests/uninterpreted-predicates/Answers index 29daa0c..39a68f9 100644 --- a/regression-tests/uninterpreted-predicates/Answers +++ b/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 diff --git a/src/tricera/Main.scala b/src/tricera/Main.scala index 2ccd6fb..64f6f93 100644 --- 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 index 6e4fce8..beef2b0 100644 --- 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 index 16082ac..55443c3 100644 --- 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