From 65f60c3b96a9dd19be31294eb45a1dd857718cd4 Mon Sep 17 00:00:00 2001 From: Zafer Esen Date: Wed, 18 Oct 2023 15:37:15 +0200 Subject: [PATCH] Add -debug option for printing debug messages and clean up some debug printing. --- src/tricera/Main.scala | 99 ++++++++++++++-------- src/tricera/Util.scala | 5 ++ src/tricera/params/TriCeraParameters.scala | 2 + 3 files changed, 71 insertions(+), 35 deletions(-) diff --git a/src/tricera/Main.scala b/src/tricera/Main.scala index 66138db..c458d74 100644 --- a/src/tricera/Main.scala +++ b/src/tricera/Main.scala @@ -34,10 +34,9 @@ import hornconcurrency.ParametricEncoder import java.io.{FileOutputStream, PrintStream} import lazabs.horn.bottomup.HornClauses.Clause -import lazabs.horn.bottomup.Util.DagNode import tricera.concurrency.{CCReader, TriCeraPreprocessor} import lazabs.prover._ -import tricera.Util.SourceInfo +import tricera.Util.{SourceInfo, printlnDebug} import tricera.benchmarking.Benchmarking._ import tricera.concurrency.CCReader.CCClause import tricera.concurrency.ccreader.CCExceptions._ @@ -509,21 +508,32 @@ class Main (args: Array[String]) { def applyProcessor(processor: ContractProcessor, solution: SolutionProcessor.Solution ): SolutionProcessor.Solution = { - println("----- Applying " + processor + " to " + fun + ".") - val (newPrecondition, newPostcondition) = processor(solution, fun, ctx) - println("----- Precondition: \n" + solution(ctx.prePred.pred)) - println("----- New Precondition: \n" + newPrecondition) - println("----- Postcondition: \n" + solution(ctx.postPred.pred)) - println("----- New Postcondition: \n" + newPostcondition + "\n") - solution + (ctx.prePred.pred -> newPrecondition) + (ctx.postPred.pred -> newPostcondition) + printlnDebug(s"----- Applying $processor to $fun.") + val (newPrecondition, newPostcondition) = + processor(solution, fun, ctx) + printlnDebug("----- Precondition:") + printlnDebug(solution(ctx.prePred.pred).toString) + printlnDebug("----- New Precondition:") + printlnDebug(newPrecondition.toString) + printlnDebug("----- Postcondition:") + printlnDebug(solution(ctx.postPred.pred).toString) + printlnDebug("----- New Postcondition:") + printlnDebug(newPostcondition.toString) + solution + (ctx.prePred.pred -> newPrecondition) + + (ctx.postPred.pred -> newPostcondition) } import ap.parser.IFormula import ap.parser.IExpression.Predicate - def addClauses(clauses: Option[IFormula], predicate: Predicate, solution: SolutionProcessor.Solution): SolutionProcessor.Solution = { + def addClauses(clauses: Option[IFormula], + predicate: Predicate, + solution: SolutionProcessor.Solution) + : SolutionProcessor.Solution = { clauses match { case Some(clauseFormula) => - val newContractCondition = solution(predicate).asInstanceOf[IFormula] & clauseFormula + val newContractCondition = + solution(predicate).asInstanceOf[IFormula] & + clauseFormula solution + (predicate -> newContractCondition) case None => solution @@ -540,20 +550,36 @@ class Main (args: Array[String]) { for (prsor <- heapPropProcessors) { val contractInfo = ContractInfo(solution, fun, ctx) - val preCCI = ContractConditionInfo(ctx.prePred.pred, contractInfo) - val postCCI = ContractConditionInfo(ctx.postPred.pred, contractInfo) - - println("----- Applying " + prsor + " to precondition of " + fun) - println("----- Precondition: \n" + preCCI.contractCondition) - val preClauses = prsor.getClauses(preCCI.contractCondition, preCCI) - println("Result: \n" + preClauses) - acslProcessedSolution = addClauses(preClauses, ctx.prePred.pred, acslProcessedSolution) - - println("----- Applying " + prsor + " to postcondition of " + fun) - println("----- Postcondition: \n" + postCCI.contractCondition) - val postClauses = prsor.getClauses(postCCI.contractCondition, postCCI) - println("----- Result: \n" + postClauses) - acslProcessedSolution = addClauses(postClauses, ctx.prePred.pred, acslProcessedSolution) + val preCCI = + ContractConditionInfo(ctx.prePred.pred, contractInfo) + val postCCI = + ContractConditionInfo(ctx.postPred.pred, contractInfo) + + printlnDebug(s"----- Applying $prsor to precondition of $fun") + printlnDebug("----- Precondition:") + printlnDebug(preCCI.contractCondition.toString) + + val preClauses = + prsor.getClauses(preCCI.contractCondition, preCCI) + + printlnDebug("Result:") + printlnDebug(preClauses.toString) + + acslProcessedSolution = addClauses( + preClauses, ctx.prePred.pred, acslProcessedSolution) + + printlnDebug(s"----- Applying $prsor to postcondition of $fun") + printlnDebug("----- Postcondition:") + printlnDebug(postCCI.contractCondition.toString) + + val postClauses = + prsor.getClauses(postCCI.contractCondition, postCCI) + + printlnDebug("----- Result:") + printlnDebug(postClauses.toString) + + acslProcessedSolution = addClauses( + postClauses,ctx.prePred.pred, acslProcessedSolution) } val printHeapExprProcessors = Seq( @@ -569,13 +595,20 @@ class Main (args: Array[String]) { } } - println("----- Applying ACSLLineariser to precondition: \n" + acslProcessedSolution(ctx.prePred.pred)) - val fPre = ACSLLineariser asString acslProcessedSolution(ctx.prePred.pred) - println("----- Result: \n " + fPre) - - println("----- Applying ACSLLineariser to postcondition: \n" + acslProcessedSolution(ctx.postPred.pred)) + printlnDebug("----- Applying ACSLLineariser to precondition:") + printlnDebug(acslProcessedSolution(ctx.prePred.pred).toString) + + val fPre = ACSLLineariser asString + acslProcessedSolution(ctx.prePred.pred) + + printlnDebug("----- Result:") + printlnDebug(fPre.toString) + printlnDebug("----- Applying ACSLLineariser to postcondition:") + printlnDebug(acslProcessedSolution(ctx.postPred.pred).toString) + val fPost = ACSLLineariser asString acslProcessedSolution(ctx.postPred.pred) - println("----- Result: \n " + fPost) + printlnDebug("----- Result:") + printlnDebug(fPost) // todo: implement replaceArgs as a solution processor // replaceArgs does a simple string replacement (see above def) @@ -612,10 +645,6 @@ class Main (args: Array[String]) { case Right(cex) => { println("UNSAFE") - import hornconcurrency.VerificationLoop._ - import tricera.Util.SourceInfo - import lazabs.horn.bottomup.HornClauses - val clauseToUnmergedRichClauses : Map[Clause, Seq[CCClause]] = cex._2.iterator.map { case (_, clause) => val richClauses : Seq[CCClause]= mergedToOriginal get clause match { diff --git a/src/tricera/Util.scala b/src/tricera/Util.scala index da89282..7a9ad67 100644 --- a/src/tricera/Util.scala +++ b/src/tricera/Util.scala @@ -46,6 +46,11 @@ object Util { def warn(msg : String) : Unit = Console.err.println("Warning: " + msg) + def printlnDebug(msg : String) : Unit = { + if (params.TriCeraParameters.get.printDebugMessages) + println(msg) + } + case class SourceInfo (line : Int, col : Int, offset : Int) private def getIntegerField(obj: Any, fieldName: String): Int = { diff --git a/src/tricera/params/TriCeraParameters.scala b/src/tricera/params/TriCeraParameters.scala index 680d7d1..3dcbb1f 100644 --- a/src/tricera/params/TriCeraParameters.scala +++ b/src/tricera/params/TriCeraParameters.scala @@ -64,6 +64,7 @@ class TriCeraParameters extends GlobalParameters { var useArraysForHeap : Boolean = false var devMode : Boolean = false + var printDebugMessages : Boolean = false var displayACSL = false var inferLoopInvariants = false @@ -235,6 +236,7 @@ class TriCeraParameters extends GlobalParameters { case "-assert" :: rest => TriCeraParameters.get.assertions = true; parseArgs(rest) case "-assertNoVerify" :: rest => TriCeraParameters.get.assertions = true; TriCeraParameters.get.fullSolutionOnAssert = false; parseArgs(rest) 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" +