From db63aa63e5d619c641e535a3b9e3c5c59f1036d0 Mon Sep 17 00:00:00 2001 From: ravi <ravi.kandhadai@epfl.ch> Date: Wed, 21 Oct 2015 19:09:26 +0200 Subject: [PATCH] Adding missing files --- .../invariant/engine/InferenceReport.scala | 7 +++++- .../transformations/InstProgSimplifier.scala | 5 +++- .../transformations/InstrumentationUtil.scala | 9 +++++-- .../transformations/IntToRealProgram.scala | 5 +++- .../NonlinearityEliminationPhase.scala | 6 +++-- .../SerialInstrumentationPhase.scala | 7 ++++-- .../regression/orb/OrbRegressionSuite.scala | 24 +++++++++++-------- 7 files changed, 44 insertions(+), 19 deletions(-) diff --git a/src/main/scala/leon/invariant/engine/InferenceReport.scala b/src/main/scala/leon/invariant/engine/InferenceReport.scala index c5984d28e..e18803b95 100644 --- a/src/main/scala/leon/invariant/engine/InferenceReport.scala +++ b/src/main/scala/leon/invariant/engine/InferenceReport.scala @@ -34,7 +34,12 @@ class InferenceCondition(invs: Seq[Expr], funDef: FunDef) simplifyArithmetic(InstUtil.replaceInstruVars(multToTimes(inv), fd))) match { case Seq() => None case Seq(inv) => Some(inv) - case invs => Some(And(invs)) + case invs => + invs.map(ExpressionTransformer.simplify _).filter(_ != tru) match { + case Seq() => Some(tru) + case Seq(ninv) => Some(ninv) + case ninvs => Some(And(ninvs)) + } } def status: String = prettyInv match { diff --git a/src/main/scala/leon/transformations/InstProgSimplifier.scala b/src/main/scala/leon/transformations/InstProgSimplifier.scala index ff7862db1..ab650449b 100644 --- a/src/main/scala/leon/transformations/InstProgSimplifier.scala +++ b/src/main/scala/leon/transformations/InstProgSimplifier.scala @@ -9,7 +9,10 @@ import purescala.ExprOps._ import purescala.Types._ import leon.purescala.ScalaPrinter import leon.utils._ -import invariant.util.Util._ +import invariant.util._ +import Util._ +import ProgramUtil._ +import PredicateUtil._ import invariant.util.ExpressionTransformer._ import invariant.structure.FunctionUtils._ import invariant.util.LetTupleSimplification._ diff --git a/src/main/scala/leon/transformations/InstrumentationUtil.scala b/src/main/scala/leon/transformations/InstrumentationUtil.scala index 427cac483..915defecf 100644 --- a/src/main/scala/leon/transformations/InstrumentationUtil.scala +++ b/src/main/scala/leon/transformations/InstrumentationUtil.scala @@ -8,6 +8,11 @@ import purescala.ExprOps._ import purescala.Extractors._ import purescala.Types._ import leon.utils.Library +import invariant.util._ +import invariant.util._ +import Util._ +import ProgramUtil._ +import PredicateUtil._ sealed abstract class Instrumentation { val getType: TypeTree @@ -73,7 +78,7 @@ object InstUtil { } def getInstMap(fd: FunDef) = { - val resvar = invariant.util.Util.getResId(fd).get.toVariable // note: every instrumented function has a postcondition + val resvar = getResId(fd).get.toVariable // note: every instrumented function has a postcondition val insts = fd.id.name.split("-").tail // split the name of the function w.r.t '-' (insts.zipWithIndex).foldLeft(Map[Expr, String]()) { case (acc, (instName, i)) => @@ -82,7 +87,7 @@ object InstUtil { } def getInstExpr(fd: FunDef, inst: Instrumentation) = { - val resvar = invariant.util.Util.getResId(fd).get.toVariable // note: every instrumented function has a postcondition + val resvar = getResId(fd).get.toVariable // note: every instrumented function has a postcondition val insts = fd.id.name.split("-").tail // split the name of the function w.r.t '-' val index = insts.indexOf(inst.name) if (index >= 0) diff --git a/src/main/scala/leon/transformations/IntToRealProgram.scala b/src/main/scala/leon/transformations/IntToRealProgram.scala index dc7ceb5a6..21229282b 100644 --- a/src/main/scala/leon/transformations/IntToRealProgram.scala +++ b/src/main/scala/leon/transformations/IntToRealProgram.scala @@ -10,7 +10,10 @@ import purescala.Types._ import leon.purescala.ScalaPrinter import invariant.factories._ -import invariant.util.Util._ +import invariant.util._ +import Util._ +import ProgramUtil._ +import PredicateUtil._ import invariant.structure._ abstract class ProgramTypeTransformer { diff --git a/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala b/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala index 77b88f71e..d17968dc0 100644 --- a/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala +++ b/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala @@ -2,7 +2,10 @@ package leon package transformations import invariant.factories._ -import invariant.util.Util._ +import invariant.util._ +import Util._ +import ProgramUtil._ +import PredicateUtil._ import invariant.structure.FunctionUtils._ import purescala.ScalaPrinter @@ -147,7 +150,6 @@ class NonlinearityEliminator(skipAxioms: Boolean, domain: TypeTree) { Some(replaceFun(simpBody)) } else None - //add a new postcondition newfd.postcondition = if (fd.postcondition.isDefined) { //we need to handle template and postWoTemplate specially diff --git a/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala b/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala index 20e3aa0e2..87c579583 100644 --- a/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala +++ b/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala @@ -10,6 +10,9 @@ import purescala.Types._ import leon.purescala.ScalaPrinter import leon.utils._ import invariant.util._ +import Util._ +import ProgramUtil._ +import PredicateUtil._ import invariant.util.CallGraphUtil import invariant.structure.FunctionUtils._ import scala.collection.mutable.{Map => MutableMap} @@ -68,7 +71,7 @@ class SerialInstrumenter(ctx: LeonContext, program: Program) { //create new functions. Augment the return type of a function iff the postcondition uses //the instrumentation variable or if the function is transitively called from such a function //note: need not instrument fields - val funMap = Util.functionsWOFields(program.definedFunctions).foldLeft(Map[FunDef, FunDef]()) { + val funMap = functionsWOFields(program.definedFunctions).foldLeft(Map[FunDef, FunDef]()) { case (accMap, fd: FunDef) if fd.isTheoryOperation => accMap + (fd -> fd) case (accMap, fd) => { @@ -160,7 +163,7 @@ class SerialInstrumenter(ctx: LeonContext, program: Program) { else List() }.toList.distinct - val newprog = Util.copyProgram(program, (defs: Seq[Definition]) => + val newprog = copyProgram(program, (defs: Seq[Definition]) => defs.map { case fd: FunDef if funMap.contains(fd) => funMap(fd) diff --git a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala b/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala index 79b15f3fc..85c898d81 100644 --- a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala +++ b/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala @@ -18,46 +18,50 @@ class OrbRegressionSuite extends LeonRegressionSuite { } } - private def testInference(f: File, bound: Int) { + private def testInference(f: File, bound: Option[Int] = None) { - val ctx = createLeonContext("--inferInv", "--minbounds", "--timeout="+bound) + val ctx = createLeonContext("--inferInv") val beginPipe = leon.frontends.scalac.ExtractionPhase andThen new leon.utils.PreprocessingPhase val (ctx2, program) = beginPipe.run(ctx, f.getAbsolutePath :: Nil) val processPipe = InferInvariantsPhase val (ctx3, report) = processPipe.run(ctx2, program) - val fails = report.conditions.filterNot(_.invariant.isDefined) - if (!fails.isEmpty) - fail(s"Inference failed for functions ${fails.map(_.fd).mkString("\n")}") + if (report.conditions.isEmpty) + fail(s"Nothing was solved") + else { + val fails = report.conditions.filterNot(_.prettyInv.isDefined) + if (!fails.isEmpty) + fail(s"Inference failed for functions ${fails.map(_.fd).mkString("\n")}") + } } forEachFileIn("regression/orb/timing") { f => test("Timing: " + f.getName) { - testInference(f, 200) + testInference(f) } } forEachFileIn("regression/orb/stack/") { f => test("Stack: " + f.getName) { - testInference(f, 200) + testInference(f) } } forEachFileIn("regression/orb//depth") { f => test("Depth: " + f.getName) { - testInference(f, 200) + testInference(f) } } forEachFileIn("regression/orb/numerical") { f => test("Numerical: " + f.getName) { - testInference(f, 200) + testInference(f) } } forEachFileIn("regression/orb/combined/") { f => test("Multiple Instrumentations: " + f.getName) { - testInference(f, 200) + testInference(f) } } } -- GitLab