From 9e626484bb7ad2754e6c8a483dbfe1089e4e1cce Mon Sep 17 00:00:00 2001 From: mario-bucev Date: Fri, 24 Mar 2023 16:55:46 +0100 Subject: [PATCH] Fix #1377 (#1392) --- .larabot.conf | 2 +- build.sbt | 2 +- .../stainless/codegen/CodeGeneration.scala | 88 ++++++--- .../stainless/codegen/CompilationUnit.scala | 4 +- .../evaluators/RecursiveEvaluator.scala | 27 ++- .../evaluators/adtFailure/ADTFailure.scala | 8 + .../evaluators/adtFailure/test_conf.json | 9 + .../benchmarks/evaluators/i1377/i1377.scala | 34 ++++ .../evaluators/i1377/test_conf.json | 10 + .../evaluators/postFailure/PostFailure.scala | 16 ++ .../evaluators/postFailure/test_conf.json | 9 + .../evaluators/preFailure/PreFailure.scala | 19 ++ .../evaluators/preFailure/test_conf.json | 9 + .../evaluators/EvaluatorComponentTest.scala | 176 ++++++++++++++++++ 14 files changed, 377 insertions(+), 36 deletions(-) create mode 100644 frontends/benchmarks/evaluators/adtFailure/ADTFailure.scala create mode 100644 frontends/benchmarks/evaluators/adtFailure/test_conf.json create mode 100644 frontends/benchmarks/evaluators/i1377/i1377.scala create mode 100644 frontends/benchmarks/evaluators/i1377/test_conf.json create mode 100644 frontends/benchmarks/evaluators/postFailure/PostFailure.scala create mode 100644 frontends/benchmarks/evaluators/postFailure/test_conf.json create mode 100644 frontends/benchmarks/evaluators/preFailure/PreFailure.scala create mode 100644 frontends/benchmarks/evaluators/preFailure/test_conf.json create mode 100644 frontends/common/src/it/scala/stainless/evaluators/EvaluatorComponentTest.scala diff --git a/.larabot.conf b/.larabot.conf index 7d322f3e57..86e075489a 100644 --- a/.larabot.conf +++ b/.larabot.conf @@ -1,6 +1,6 @@ commands = [ "sbt -batch -Dtest-parallelism=5 test" - "sbt -batch -Dtest-parallelism=5 \"it:testOnly stainless.GhostRewriteSuite stainless.GenCSuite stainless.ScalacExtractionSuite stainless.LibrarySuite stainless.verification.SMTZ3VerificationSuite stainless.verification.SMTZ3UncheckedSuite stainless.verification.TerminationVerificationSuite stainless.verification.ImperativeSuite stainless.verification.FullImperativeSuite stainless.verification.StrictArithmeticSuite stainless.verification.CodeGenVerificationSuite stainless.verification.SMTCVC4VerificationSuite stainless.verificatoin.SMTCVC4UncheckedSuite stainless.termination.TerminationSuite\"" + "sbt -batch -Dtest-parallelism=5 \"it:testOnly stainless.GhostRewriteSuite stainless.GenCSuite stainless.ScalacExtractionSuite stainless.LibrarySuite stainless.verification.SMTZ3VerificationSuite stainless.verification.SMTZ3UncheckedSuite stainless.verification.TerminationVerificationSuite stainless.verification.ImperativeSuite stainless.verification.FullImperativeSuite stainless.verification.StrictArithmeticSuite stainless.verification.CodeGenVerificationSuite stainless.verification.SMTCVC4VerificationSuite stainless.verificatoin.SMTCVC4UncheckedSuite stainless.termination.TerminationSuite stainless.evaluators.EvaluatorComponentTest\"" ] nightly { diff --git a/build.sbt b/build.sbt index d459c9acdb..d86494738e 100644 --- a/build.sbt +++ b/build.sbt @@ -275,7 +275,7 @@ val scriptSettings: Seq[Setting[_]] = Seq( def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}")) // lazy val inox = RootProject(file("../inox")) -lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "6efba92979cc420fd73dda8bfafa05102f0f4047") +lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "41ffe806b04769c0d6757ebfeb17a96c7d5efd8a") lazy val cafebabe = ghProject("https://github.com/epfl-lara/cafebabe.git", "616e639b34379e12b8ac202849de3ebbbd0848bc") // Allow integration test to use facilities from regular tests diff --git a/core/src/main/scala/stainless/codegen/CodeGeneration.scala b/core/src/main/scala/stainless/codegen/CodeGeneration.scala index 3ba0790a65..1f3251a22f 100644 --- a/core/src/main/scala/stainless/codegen/CodeGeneration.scala +++ b/core/src/main/scala/stainless/codegen/CodeGeneration.scala @@ -27,7 +27,7 @@ trait CodeGeneration { self: CompilationUnit => import program.symbols.{given, _} import program.trees.exprOps._ - lazy val ignoreContracts = options.findOptionOrDefault(inox.evaluators.optIgnoreContracts) + lazy val globallyIgnoreContracts = options.findOptionOrDefault(inox.evaluators.optIgnoreContracts) lazy val doInstrument = options.findOptionOrDefault(optInstrumentFields) lazy val smallArrays = options.findOptionOrDefault(optSmallArrays) lazy val recordInvocations = maxSteps >= 0 @@ -74,6 +74,8 @@ trait CodeGeneration { self: CompilationUnit => object NoLocals extends Locals(Map.empty, Map.empty, Map.empty, Seq.empty, Seq.empty) + case class ContractsCtx(locallyIgnored: Boolean) + lazy val monitorID = FreshIdentifier("__$monitor") lazy val tpsID = FreshIdentifier("__$tps") @@ -306,7 +308,7 @@ trait CodeGeneration { self: CompilationUnit => Seq(monitor) ++ tpsOpt ++ params }.toMap - val body = if (!ignoreContracts) { + val body = if (!globallyIgnoreContracts) { funDef.fullBody } else { funDef.body.getOrElse( @@ -324,11 +326,11 @@ trait CodeGeneration { self: CompilationUnit => .withTypeParameters(funDef.tparams.map(_.tp)) if (recordInvocations) { - loadImpl(monitorID, ch)(using locals) + loadImpl(monitorID, ch)(using locals, ContractsCtx(locallyIgnored = false)) ch << InvokeVirtual(MonitorClass, "onInvocation", "()V") } - mkExpr(body, ch)(using locals) + mkExpr(body, ch)(using locals, ContractsCtx(locallyIgnored = false)) funDef.getType match { case JvmIType() => @@ -348,7 +350,7 @@ trait CodeGeneration { self: CompilationUnit => private val typeParams: ListBuffer[TypeParameter] = new ListBuffer[TypeParameter] - protected def compileLambda(l: Lambda, params: Seq[ValDef]): + protected def compileLambda(l: Lambda, params: Seq[ValDef])(using contractsCtx: ContractsCtx): (String, Seq[(Identifier, String)], Seq[TypeParameter], String) = synchronized { assert(normalizeStructure(l)._1 == l) @@ -547,7 +549,7 @@ trait CodeGeneration { self: CompilationUnit => } // also makes tuples with 0/1 args - private def mkTuple(es: Seq[Expr], ch: CodeHandler)(using locals: Locals) : Unit = { + private def mkTuple(es: Seq[Expr], ch: CodeHandler)(using locals: Locals, contractsCtx: ContractsCtx) : Unit = { ch << New(TupleClass) << DUP ch << Ldc(es.size) ch << NewArray(s"$ObjectClass") @@ -560,7 +562,7 @@ trait CodeGeneration { self: CompilationUnit => ch << InvokeSpecial(TupleClass, constructorName, s"([L$ObjectClass;)V") } - private def loadTypes(tps: Seq[Type], ch: CodeHandler)(using locals: Locals): Unit = { + private def loadTypes(tps: Seq[Type], ch: CodeHandler)(using locals: Locals, contractsCtx: ContractsCtx): Unit = { if (tps.nonEmpty) { ch << Ldc(tps.size) ch << NewArray.primitive("T_INT") @@ -605,21 +607,27 @@ trait CodeGeneration { self: CompilationUnit => } private[codegen] def mkExpr(e: Expr, ch: CodeHandler, canDelegateToMkBranch: Boolean = true) - (using locals: Locals): Unit = e match { + (using locals: Locals, contractsCtx: ContractsCtx): Unit = e match { case v: Variable => load(v, ch) case Assert(cond, oerr, body) => - mkExpr(IfExpr(Not(cond), Error(body.getType, oerr.getOrElse("Assertion failed @"+e.getPos)), body), ch) + if (!ignoreContractsOn(e)) + mkExpr(IfExpr(Not(cond), Error(body.getType, oerr.getOrElse("Assertion failed @"+e.getPos)), body), ch) + else mkExpr(body, ch) case Assume(cond, body) => - mkExpr(IfExpr(Not(cond), Error(body.getType, "Assumption failed @"+e.getPos), body), ch) + if (!ignoreContractsOn(e)) + mkExpr(IfExpr(Not(cond), Error(body.getType, "Assumption failed @"+e.getPos), body), ch) + else mkExpr(body, ch) case en @ Ensuring(_, _) => mkExpr(en.toAssert, ch) case Require(pre, body) => - mkExpr(IfExpr(pre, body, Error(body.getType, "Precondition failed")), ch) + if (!ignoreContractsOn(e)) + mkExpr(IfExpr(pre, body, Error(body.getType, "Precondition failed")), ch) + else mkExpr(body, ch) case Decreases(measure, body) => mkExpr(body, ch) @@ -707,7 +715,7 @@ trait CodeGeneration { self: CompilationUnit => ch << InvokeSpecial(adtName, constructorName, adtApplySig) // check invariant (if it exists) - if (!ignoreContracts && cons.getSort.hasInvariant) { + if (!ignoreContractsOn(adt) && cons.getSort.hasInvariant) { ch << DUP val tfd = tcons.sort.invariant.get @@ -1236,13 +1244,17 @@ trait CodeGeneration { self: CompilationUnit => case m: Max => mkExpr(maxToIfThenElse(m), ch) - case Annotated(body, _) => - mkExpr(body, ch) + case Annotated(body, flags) => + val nctx = { + if (flags.contains(DropVCs) || flags.contains(DropConjunct)) contractsCtx.copy(locallyIgnored = true) + else contractsCtx + } + mkExpr(body, ch)(using locals, nctx) case _ => throw CompilationException("Unsupported expr " + e + " : " + e.getClass) } - private[codegen] def mkLambda(lambda: Lambda, ch: CodeHandler)(using locals: Locals): Unit = { + private[codegen] def mkLambda(lambda: Lambda, ch: CodeHandler)(using locals: Locals, contractsCtx: ContractsCtx): Unit = { val vars = variablesOf(lambda).toSeq val freshVars = vars.map(_.freshen) @@ -1308,7 +1320,7 @@ trait CodeGeneration { self: CompilationUnit => // Leaves on the stack a value equal to `e`, always of a type compatible with java.lang.Object. private[codegen] def mkBoxedExpr(e: Expr, ch: CodeHandler) - (using locals: Locals): Unit = e.getType match { + (using locals: Locals, contractsCtx: ContractsCtx): Unit = e.getType match { case Int8Type() => ch << New(BoxedByteClass) << DUP mkExpr(e, ch) @@ -1449,7 +1461,7 @@ trait CodeGeneration { self: CompilationUnit => } private[codegen] def mkBranch(cond: Expr, thenn: String, elze: String, ch: CodeHandler, canDelegateToMkExpr: Boolean = true) - (using locals: Locals): Unit = cond match { + (using locals: Locals, contractsCtx: ContractsCtx): Unit = cond match { case BooleanLiteral(true) => ch << Goto(thenn) @@ -1517,8 +1529,12 @@ trait CodeGeneration { self: CompilationUnit => mkExpr(other, ch, canDelegateToMkBranch = false) ch << IfEq(elze) << Goto(thenn) - case Annotated(condition, _) => - mkBranch(condition, thenn, elze, ch) + case Annotated(condition, flags) => + val nctx = { + if (flags.contains(DropVCs) || flags.contains(DropConjunct)) contractsCtx.copy(locallyIgnored = true) + else contractsCtx + } + mkBranch(condition, thenn, elze, ch)(using locals, nctx) case other => throw CompilationException("Unsupported branching expr. : " + other) } @@ -1579,7 +1595,7 @@ trait CodeGeneration { self: CompilationUnit => private def mkBVShift(l: Expr, r: Expr, ch: CodeHandler, iop: ByteCode, lop: ByteCode, op: String) - (using locals: Locals): Unit = { + (using locals: Locals, contractsCtx: ContractsCtx): Unit = { // NOTE for shift operations on Byte/Short/Int/Long: // the lhs operand can be either Int or Long, // the rhs operand must be an Int. @@ -1600,7 +1616,7 @@ trait CodeGeneration { self: CompilationUnit => private def mkCmpJump(cond: Expr, thenn: String, elze: String, l: Expr, r: Expr, ch: CodeHandler, iop: String => ControlOperator, lop: String => ControlOperator, op: String) - (using locals: Locals): Unit = { + (using locals: Locals, contractsCtx: ContractsCtx): Unit = { mkExpr(l, ch) mkExpr(r, ch) l.getType match { @@ -1625,13 +1641,13 @@ trait CodeGeneration { self: CompilationUnit => private def mkArithmeticBinary(l: Expr, r: Expr, ch: CodeHandler, iop: ByteCode, lop: ByteCode, op: String, bvOnly: Boolean) - (using locals: Locals): Unit = { + (using locals: Locals, contractsCtx: ContractsCtx): Unit = { mkArithmeticBinaryImpl(l, r, ch, { ch => ch << iop }, { ch => ch << lop }, op, bvOnly) } private def mkArithmeticBinaryImpl(l: Expr, r: Expr, ch: CodeHandler, iopGen: AbstractByteCodeGenerator, lopGen: AbstractByteCodeGenerator, op: String, bvOnly: Boolean) - (using locals: Locals): Unit = { + (using locals: Locals, contractsCtx: ContractsCtx): Unit = { ch << Comment(s"mkArithmeticBinary($op)") mkExpr(l, ch) mkExpr(r, ch) @@ -1688,13 +1704,13 @@ trait CodeGeneration { self: CompilationUnit => private def mkArithmeticUnary(e: Expr, ch: CodeHandler, iop: ByteCode, lop: ByteCode, op: String, bvOnly: Boolean) - (using locals: Locals): Unit = { + (using locals: Locals, contractsCtx: ContractsCtx): Unit = { mkArithmeticUnaryImpl(e, ch, { ch => ch << iop }, { ch => ch << lop }, op, bvOnly) } private def mkArithmeticUnaryImpl(e: Expr, ch: CodeHandler, iopGen: AbstractByteCodeGenerator, lopGen: AbstractByteCodeGenerator, op: String, bvOnly: Boolean) - (using locals: Locals): Unit = { + (using locals: Locals, contractsCtx: ContractsCtx): Unit = { ch << Comment(s"mkArithmeticUnary($op)") mkExpr(e, ch) @@ -1742,9 +1758,9 @@ trait CodeGeneration { self: CompilationUnit => } - private def load(v: Variable, ch: CodeHandler)(using locals: Locals): Unit = loadImpl(v.id, ch, Some(v.getType)) + private def load(v: Variable, ch: CodeHandler)(using locals: Locals, contractsCtx: ContractsCtx): Unit = loadImpl(v.id, ch, Some(v.getType)) - private def loadImpl(id: Identifier, ch: CodeHandler, tpe: Option[Type] = None)(using locals: Locals): Unit = { + private def loadImpl(id: Identifier, ch: CodeHandler, tpe: Option[Type] = None)(using locals: Locals, contractsCtx: ContractsCtx): Unit = { locals.varToArg(id) match { case Some(slot) => ch << ALoad(1) << Ldc(slot) << AALOAD @@ -1816,7 +1832,7 @@ trait CodeGeneration { self: CompilationUnit => val instrumentedField = "__read" def instrumentedGetField(ch: CodeHandler, cons: TypedADTConstructor, id: Identifier) - (using locals: Locals): Unit = { + (using locals: Locals, contractsCtx: ContractsCtx): Unit = { cons.definition.fields.zipWithIndex.find(_._1.id == id) match { case Some((f, i)) => val expType = cons.fields(i).getType @@ -1844,6 +1860,7 @@ trait CodeGeneration { self: CompilationUnit => } def compileADTConstructor(cons: ADTConstructor): Unit = { + given ContractsCtx = ContractsCtx(locallyIgnored = false) val cName = defConsToJVMName(cons) val pName = defSortToJVMName(cons.getSort) val tcons = cons.typed @@ -2041,6 +2058,21 @@ trait CodeGeneration { self: CompilationUnit => } + private def ignoreContractsOn(expr: Expr)(using contractsCtx: ContractsCtx): Boolean = { + def isAnnotatedDrop(e: Expr) = e match { + case Annotated(_, flags) => flags.contains(DropVCs) || flags.contains(DropConjunct) + case _ => false + } + + globallyIgnoreContracts || contractsCtx.locallyIgnored || (expr match { + case Assume(pred, _) => isAnnotatedDrop(pred) + case Assert(pred, _, _) => isAnnotatedDrop(pred) + case Require(pred, _) => isAnnotatedDrop(pred) + case Ensuring(_, pred) => isAnnotatedDrop(pred) || isAnnotatedDrop(pred.body) + case _ => isAnnotatedDrop(expr) + }) + } + private def internalErrorWithByteOrShort(e: Expr) = throw CompilationException(s"Unexpected expression involving Byte or Short: $e") } diff --git a/core/src/main/scala/stainless/codegen/CompilationUnit.scala b/core/src/main/scala/stainless/codegen/CompilationUnit.scala index c944da7866..e5bbadfabb 100644 --- a/core/src/main/scala/stainless/codegen/CompilationUnit.scala +++ b/core/src/main/scala/stainless/codegen/CompilationUnit.scala @@ -186,7 +186,7 @@ class CompilationUnit(val program: Program, val context: inox.Context)(using val case lambda: Lambda => val (l: Lambda, deps) = normalizeStructure(matchToIfThenElse(lambda, assumeExhaustive = false)): @unchecked if (deps.forall { case (_, e, conds) => isValue(e) && conds.isEmpty }) { - val (afName, closures, tparams, consSig) = compileLambda(l, Seq.empty) + val (afName, closures, tparams, consSig) = compileLambda(l, Seq.empty)(using ContractsCtx(locallyIgnored = false)) val depsMap = deps.map { case (v, dep, _) => v.id -> valueToJVM(dep) }.toMap val args = closures.map { case (id, _) => @@ -444,7 +444,7 @@ class CompilationUnit(val program: Program, val context: inox.Context)(using val case (v, i) => v.id -> (i + 1) }.toMap - mkExpr(e, ch)(using NoLocals.withVars(newMapping)) + mkExpr(e, ch)(using NoLocals.withVars(newMapping), ContractsCtx(locallyIgnored = false)) e.getType match { case JvmIType() => diff --git a/core/src/main/scala/stainless/evaluators/RecursiveEvaluator.scala b/core/src/main/scala/stainless/evaluators/RecursiveEvaluator.scala index c1f43ee0ad..0ea03ac214 100644 --- a/core/src/main/scala/stainless/evaluators/RecursiveEvaluator.scala +++ b/core/src/main/scala/stainless/evaluators/RecursiveEvaluator.scala @@ -14,7 +14,7 @@ abstract class RecursiveEvaluator(override val program: Program, override def e(expr: Expr)(using rctx: RC, gctx: GC): Expr = expr match { case Require(pred, body) => - if (!ignoreContracts && e(pred) != BooleanLiteral(true)) + if (!ignoreContractsOn(expr) && e(pred) != BooleanLiteral(true)) throw RuntimeError("Requirement did not hold @" + expr.getPos) e(body) @@ -25,7 +25,7 @@ abstract class RecursiveEvaluator(override val program: Program, e(body) case Assert(pred, err, body) => - if (!ignoreContracts && e(pred) != BooleanLiteral(true)) + if (!ignoreContractsOn(expr) && e(pred) != BooleanLiteral(true)) throw RuntimeError(err.getOrElse("Assertion failed @" + expr.getPos)) e(body) @@ -77,12 +77,31 @@ abstract class RecursiveEvaluator(override val program: Program, case NoTree(tpe) => throw RuntimeError("Reached empty tree in evaluation @" + expr.getPos) - case Annotated(body, _) => - e(body) + case Annotated(body, flags) => + val nrctx = { + if (flags.contains(DropVCs) || flags.contains(DropConjunct)) rctx.withLocallyIgnoredContracts + else rctx + } + e(body)(using nrctx) case _ => super.e(expr) } + override def ignoreContractsOn(expr: Expr)(using rctx: RC, gctx: GC): Boolean = { + def isAnnotatedDrop(e: Expr) = e match { + case Annotated(_, flags) => flags.contains(DropVCs) || flags.contains(DropConjunct) + case _ => false + } + + super.ignoreContractsOn(expr) || (expr match { + case Assume(pred, _) => isAnnotatedDrop(pred) + case Assert(pred, _, _) => isAnnotatedDrop(pred) + case Require(pred, _) => isAnnotatedDrop(pred) + case Ensuring(_, pred) => isAnnotatedDrop(pred) || isAnnotatedDrop(pred.body) + case _ => isAnnotatedDrop(expr) + }) + } + protected def matchesCase(scrut: Expr, caze: MatchCase) (using rctx: RC, gctx: GC): Option[Map[ValDef, Expr]] = { diff --git a/frontends/benchmarks/evaluators/adtFailure/ADTFailure.scala b/frontends/benchmarks/evaluators/adtFailure/ADTFailure.scala new file mode 100644 index 0000000000..101d471280 --- /dev/null +++ b/frontends/benchmarks/evaluators/adtFailure/ADTFailure.scala @@ -0,0 +1,8 @@ +object ADTFailure { + + case class MyADT(x: BigInt) { + require(0 <= x && x < 100) + } + + def ohno: BigInt = MyADT(42).x + MyADT(101).x +} \ No newline at end of file diff --git a/frontends/benchmarks/evaluators/adtFailure/test_conf.json b/frontends/benchmarks/evaluators/adtFailure/test_conf.json new file mode 100644 index 0000000000..9a323f21c7 --- /dev/null +++ b/frontends/benchmarks/evaluators/adtFailure/test_conf.json @@ -0,0 +1,9 @@ +{ + "recursive": true, + "codegen": true, + "failure": [ + { + "function": "ohno" + } + ] +} \ No newline at end of file diff --git a/frontends/benchmarks/evaluators/i1377/i1377.scala b/frontends/benchmarks/evaluators/i1377/i1377.scala new file mode 100644 index 0000000000..5f02fdf704 --- /dev/null +++ b/frontends/benchmarks/evaluators/i1377/i1377.scala @@ -0,0 +1,34 @@ +object i1377 { + sealed abstract class List[+A] { + def :: [B >: A](elem: B): List[B] = Cons(elem, this) + + def ++[B >: A](that: List[B]): List[B] = { + this match { + case Nil => that + case Cons(a, as) => a :: (as ++ that) + } + } + + def tail: List[A] = { + require(this != Nil) + this match { + case Cons(a, as) => as + } + } + + def head: A = { + require(this != Nil) + this match { + case Cons(a, as) => a + } + } + } + + case object Nil extends List[Nothing] + final case class Cons[+A](first: A, next: List[A]) extends List[A] + + def list: List[Int] = Cons(10, Cons(20, Cons(30, Nil))) + def list2: List[Int] = list ++ list + + def expectedList2: List[Int] = Cons(10, Cons(20, Cons(30, Cons(10, Cons(20, Cons(30, Nil)))))) +} \ No newline at end of file diff --git a/frontends/benchmarks/evaluators/i1377/test_conf.json b/frontends/benchmarks/evaluators/i1377/test_conf.json new file mode 100644 index 0000000000..ebaa6d341f --- /dev/null +++ b/frontends/benchmarks/evaluators/i1377/test_conf.json @@ -0,0 +1,10 @@ +{ + "recursive": true, + "codegen": true, + "successful": [ + { + "function": "list2", + "expected": "expectedList2" + } + ] +} \ No newline at end of file diff --git a/frontends/benchmarks/evaluators/postFailure/PostFailure.scala b/frontends/benchmarks/evaluators/postFailure/PostFailure.scala new file mode 100644 index 0000000000..d36dada637 --- /dev/null +++ b/frontends/benchmarks/evaluators/postFailure/PostFailure.scala @@ -0,0 +1,16 @@ +import stainless.collection._ + +object PostFailure { + + case class PostBox(letters: List[Letter]) + case class Letter(from: String, msg: String, to: String) + + def put(pb: PostBox, l: Letter): PostBox = { + pb + }.ensuring(_ == l :: pb.letters) // oh no, post fails :( + + def ohno: PostBox = put( + PostBox(Nil()), + Letter("Someone", ":)", "EPFL IC IINFCOM LARA") + ) +} \ No newline at end of file diff --git a/frontends/benchmarks/evaluators/postFailure/test_conf.json b/frontends/benchmarks/evaluators/postFailure/test_conf.json new file mode 100644 index 0000000000..9a323f21c7 --- /dev/null +++ b/frontends/benchmarks/evaluators/postFailure/test_conf.json @@ -0,0 +1,9 @@ +{ + "recursive": true, + "codegen": true, + "failure": [ + { + "function": "ohno" + } + ] +} \ No newline at end of file diff --git a/frontends/benchmarks/evaluators/preFailure/PreFailure.scala b/frontends/benchmarks/evaluators/preFailure/PreFailure.scala new file mode 100644 index 0000000000..82f786efb2 --- /dev/null +++ b/frontends/benchmarks/evaluators/preFailure/PreFailure.scala @@ -0,0 +1,19 @@ +import stainless.collection._ + +object PreFailure { + sealed trait Topping + case object Mozzarella extends Topping + case object Pineapple extends Topping + case object Capers extends Topping + + case class Pizza(size: BigInt, toppings: List[Topping]) + + def addTopping(p: Pizza, t: Topping): Pizza = { + require(t != Pineapple) + p.copy(toppings = t :: p.toppings) + } + + val base = Pizza(42, List(Mozzarella)) + def ohno: Pizza = + addTopping(addTopping(base, Capers), Pineapple) +} \ No newline at end of file diff --git a/frontends/benchmarks/evaluators/preFailure/test_conf.json b/frontends/benchmarks/evaluators/preFailure/test_conf.json new file mode 100644 index 0000000000..9a323f21c7 --- /dev/null +++ b/frontends/benchmarks/evaluators/preFailure/test_conf.json @@ -0,0 +1,9 @@ +{ + "recursive": true, + "codegen": true, + "failure": [ + { + "function": "ohno" + } + ] +} \ No newline at end of file diff --git a/frontends/common/src/it/scala/stainless/evaluators/EvaluatorComponentTest.scala b/frontends/common/src/it/scala/stainless/evaluators/EvaluatorComponentTest.scala new file mode 100644 index 0000000000..2608f78cca --- /dev/null +++ b/frontends/common/src/it/scala/stainless/evaluators/EvaluatorComponentTest.scala @@ -0,0 +1,176 @@ +package stainless +package evaluators + +import _root_.io.circe.JsonObject +import inox.{OptionValue, TestSilentReporter} +import org.scalatest.funsuite.AnyFunSuite +import stainless.equivchk.EquivalenceCheckingReport.Status +import stainless.extraction.utils.DebugSymbols +import stainless.extraction.xlang.{TreeSanitizer, extractor, trees as xt} +import stainless.extraction.{ExtractionSummary, extractionSemantics} +import stainless.utils.JsonUtils +import stainless.verification.* + +import java.io.File +import scala.concurrent.Await +import scala.concurrent.duration.* + +class EvaluatorComponentTest extends ComponentTestSuite { + override val component: EvaluatorComponent.type = EvaluatorComponent + + private def testConfName = "test_conf.json" + + override protected def optionsString(options: inox.Options): String = "" + + /////////////////////////////////////////////// + + for (benchmark <- getFolders("evaluators")) { + testEval(s"evaluators/$benchmark") + } + + /////////////////////////////////////////////// + + private def getFolders(dir: String): Seq[String] = { + Option(getClass.getResource(s"/$dir")).toSeq.flatMap { dirUrl => + val dirFile = new File(dirUrl.getPath) + Option(dirFile.listFiles().toSeq).getOrElse(Seq.empty).filter(_.isDirectory) + .map(_.getName) + }.sorted + } + + private def testEval(benchmarkDir: String): Unit = { + val files = resourceFiles(benchmarkDir, f => f.endsWith(".scala") || f.endsWith(".json")).sorted + if (files.isEmpty) return // Empty folder -- skip + + val scalaFiles = files.filter(_.getName.endsWith(".scala")) + val testConfFile = files.find(_.getName == testConfName) + .getOrElse(fail(s"Test configuration file $testConfName not found in $benchmarkDir")) + val testConf = parseTestConf(testConfFile) + + ///////////////////////////////////// + + val dummyCtx: inox.Context = inox.TestContext.empty + import dummyCtx.given + val (_, program) = loadFiles(scalaFiles.map(_.getPath)) + assert(dummyCtx.reporter.errorCount == 0, "There should be no error while loading the files") + + val userFiltering = new DebugSymbols { + val name = "UserFiltering" + val context = dummyCtx + val s: xt.type = xt + val t: xt.type = xt + } + + val programSymbols = userFiltering.debugWithoutSummary(frontend.UserFiltering().transform)(program.symbols)._1 + programSymbols.ensureWellFormed + + ///////////////////////////////////// + + for (evaluator <- testConf.evaluators) { + test(s"$benchmarkDir ($evaluator)") { ctx0 ?=> + val opt = evaluator match { + case Evaluator.Recursive => optCodeGen(false) + case Evaluator.Codegen => optCodeGen(true) + } + given ctx: inox.Context = ctx0.withOpts(opt) + + // Note that `run` must be defined here to pick the `ctx` with updated evaluator option. + val run = component.run(extraction.pipeline) + val exSymbols = run.extract(programSymbols)._1 + exSymbols.ensureWellFormed + assert(ctx.reporter.errorCount == 0, "There were errors during pipeline extraction") + + val fnsToEval = exSymbols.functions.keys.filter(testConf.needsEvaluation).toSeq + + val groundValues = testConf.expected.collect { + case EvalResult.SuccessfulEval(tested, ground) => + val groundFd = exSymbols.functions.find(_._1.name == ground) + .getOrElse(fail(s"Function for ground result $ground not found")) + ._2.fullBody + tested -> groundFd + }.toMap + + val report = Await.result(run.execute(fnsToEval, exSymbols, ExtractionSummary.NoSummary), Duration.Inf) + for { + res <- report.results + exp <- testConf.expected.find(_.testedFn == res.fd.id.name) + } { + exp match { + case EvalResult.SuccessfulEval(tested, _) => + res.status match { + case EvaluatorRun.NoPost(bodyValue) => + bodyValue shouldEqual groundValues(tested) + case EvaluatorRun.PostHeld(bodyValue) => + bodyValue shouldEqual groundValues(tested) + case _ => fail(s"Evaluation of ${res.fd.id} did not succeed: got ${res.status}") + } + case EvalResult.FailedEval(_) => + res.status match { + case EvaluatorRun.NoPost(_) | EvaluatorRun.PostHeld(_) => + fail(s"Evaluation of ${res.fd.id} should have failed, but has succeeded") + case _ => () + } + } + } + } + } + } + + private enum Evaluator { + case Recursive + case Codegen + } + + private enum EvalResult { + case SuccessfulEval(fn: String, ground: String) + case FailedEval(fn: String) + + def testedFn: String = this match { + case SuccessfulEval(fn, _) => fn + case FailedEval(fn) => fn + } + } + + private case class TestConf(evaluators: Seq[Evaluator], + expected: Seq[EvalResult]) { + def needsEvaluation(fn: Identifier): Boolean = expected.exists(_.testedFn == fn.name) + } + + private def parseTestConf(f: File): TestConf = { + val json = JsonUtils.parseFile(f) + val jsonObj = json.asObject.getOrCry("Expected top-level json to be an object") + val recEval = jsonObj("recursive").exists(_.asBoolean.getOrCry("Expected 'recursive' to be a boolean")) + val codegenEval = jsonObj("codegen").exists(_.asBoolean.getOrCry("Expected 'codegen' to be a boolean")) + if (!recEval && !codegenEval) { + fail("At least one of 'recursive' or 'codegen' evaluator option must be set to true") + } + val evaluators = (if (recEval) Seq(Evaluator.Recursive) else Seq.empty) ++ (if (codegenEval) Seq(Evaluator.Codegen) else Seq.empty) + + val successful = jsonObj("successful").map { succ => + val elems = succ.asArray.getOrCry("Expected 'successful' to be an array") + elems.map(_.asObject.getOrCry("Expected elements of 'successful' to be objects")).map { elem => + val fn = elem.getStringOrCry("function") + val exp = elem.getStringOrCry("expected") + EvalResult.SuccessfulEval(fn, exp) + } + }.getOrElse(Vector.empty) + val failures = jsonObj("failure").map { succ => + val elems = succ.asArray.getOrCry("Expected 'failure' to be an array") + elems.map(_.asObject.getOrCry("Expected elements of 'failure' to be objects")).map { elem => + val fn = elem.getStringOrCry("function") + EvalResult.FailedEval(fn) + } + }.getOrElse(Vector.empty) + TestConf(evaluators, successful ++ failures) + } + + extension[T] (o: Option[T]) { + private def getOrCry(msg: String): T = o.getOrElse(fail(msg)) + } + + extension (jsonObj: JsonObject) { + private def getStringOrCry(field: String): String = + jsonObj(field).getOrCry(s"Expected a '$field' field") + .asString.getOrCry(s"Expected '$field' to a string") + } +}