diff --git a/core/src/main/scala/stainless/ast/Deconstructors.scala b/core/src/main/scala/stainless/ast/Deconstructors.scala index 16fd0895f5..67c8b74bff 100644 --- a/core/src/main/scala/stainless/ast/Deconstructors.scala +++ b/core/src/main/scala/stainless/ast/Deconstructors.scala @@ -226,7 +226,6 @@ trait TreeDeconstructor extends inox.ast.TreeDeconstructor { case s.PartialEval => (Seq(), Seq(), Seq(), (_, _, _) => t.PartialEval) case s.Wrapping => (Seq(), Seq(), Seq(), (_, _, _) => t.Wrapping) case s.Template => (Seq(), Seq(), Seq(), (_, _, _) => t.Template) - case s.ImplPrivate => (Seq(), Seq(), Seq(), (_, _, _) => t.ImplPrivate) case s.TerminationStatus(status) => (Seq(), Seq(), Seq(), (_, _, _) => t.TerminationStatus(status)) case _ => super.deconstruct(f) } diff --git a/core/src/main/scala/stainless/ast/Definitions.scala b/core/src/main/scala/stainless/ast/Definitions.scala index 793b614c8f..cc6a986ff0 100644 --- a/core/src/main/scala/stainless/ast/Definitions.scala +++ b/core/src/main/scala/stainless/ast/Definitions.scala @@ -29,7 +29,6 @@ trait Definitions extends inox.ast.Definitions { self: Trees => case object PartialEval extends Flag("partialEval", Seq()) case object Wrapping extends Flag("wrapping", Seq.empty) case object Template extends Flag("template", Seq.empty) - case object ImplPrivate extends Flag("implPrivate", Seq.empty) case class Derived(idOpt: Option[Identifier]) extends Flag("derived", idOpt.toSeq) case class IsField(isLazy: Boolean) extends Flag("field", Seq.empty) @@ -53,7 +52,6 @@ trait Definitions extends inox.ast.Definitions { self: Trees => case ("wrapping", Seq()) => Wrapping case ("template", Seq()) => Template case ("inlineInvariant", Seq()) => InlineInvariant - case ("implPrivate", Seq()) => ImplPrivate case _ => Annotation(name, args) } diff --git a/core/src/main/scala/stainless/extraction/package.scala b/core/src/main/scala/stainless/extraction/package.scala index ada15ac58f..c92de8e1f1 100644 --- a/core/src/main/scala/stainless/extraction/package.scala +++ b/core/src/main/scala/stainless/extraction/package.scala @@ -59,7 +59,6 @@ package object extraction { "MeasureInference" -> "Infer and inject measures in recursive functions", "PartialEvaluation" -> "Partially evaluate marked function calls", "AssertionInjector" -> "Insert assertions which verify array accesses, casts, division by zero, etc.", - "ImplPrivateInlining" -> "Inline @implPrivate functions ahead of VC generation", "ChooseInjector" -> "Insert chooses where necessary", "ComputeDependencies" -> "(GenC) Compute the dependencies of a given definition", diff --git a/core/src/main/scala/stainless/solvers/InoxEncoder.scala b/core/src/main/scala/stainless/solvers/InoxEncoder.scala index 8fd9cc1f71..2f05866286 100644 --- a/core/src/main/scala/stainless/solvers/InoxEncoder.scala +++ b/core/src/main/scala/stainless/solvers/InoxEncoder.scala @@ -20,8 +20,7 @@ trait InoxEncoder extends ProgramEncoder { private[this] def keepFlag(flag: Flag): Boolean = flag match { case DropVCs | DropConjunct | Library | Synthetic | PartialEval | Extern => false case Opaque | Private | Final | Law | Ghost | Erasable | Wrapping | Lazy => false - case Derived(_) | IsField(_) | IsUnapply(_, _) | IndexedAt(_) | ClassParamInit(_) | - ImplPrivate => false + case Derived(_) | IsField(_) | IsUnapply(_, _) | IndexedAt(_) | ClassParamInit(_) => false case TerminationStatus(_) => false case InlineInvariant | Template => false case _ => true diff --git a/core/src/main/scala/stainless/utils/Serialization.scala b/core/src/main/scala/stainless/utils/Serialization.scala index b9e3e5593b..5652b187c7 100644 --- a/core/src/main/scala/stainless/utils/Serialization.scala +++ b/core/src/main/scala/stainless/utils/Serialization.scala @@ -19,9 +19,9 @@ class StainlessSerializer(override val trees: ast.Trees, serializeProducts: Bool /** An extension to the set of registered classes in the `InoxSerializer`. * occur within Stainless programs. * - * The new identifiers in the mapping range from 120 to 172. + * The new identifiers in the mapping range from 120 to 171. * - * NEXT ID: 173 + * NEXT ID: 172 */ override protected def classSerializers: Map[Class[_], Serializer[_]] = super.classSerializers ++ Map( @@ -88,7 +88,6 @@ class StainlessSerializer(override val trees: ast.Trees, serializeProducts: Bool classSerializer[InlineInvariant.type](166), classSerializer[Lazy.type] (167), classSerializer[Template.type] (169), - classSerializer[ImplPrivate.type](172), ) } diff --git a/core/src/main/scala/stainless/verification/ImplPrivateInlining.scala b/core/src/main/scala/stainless/verification/ImplPrivateInlining.scala deleted file mode 100644 index 0b777c3533..0000000000 --- a/core/src/main/scala/stainless/verification/ImplPrivateInlining.scala +++ /dev/null @@ -1,94 +0,0 @@ -/* Copyright 2009-2020 EPFL, Lausanne */ - -package stainless -package verification - -/** - * Inline functions marked ImplPrivate. - **/ -trait ImplPrivateInlining extends transformers.TreeTransformer { - val s: ast.Trees - val t: s.type - - val context: inox.Context - - implicit val symbols: s.Symbols - - import symbols._ - import t._ - - override def transform(expr: s.Expr): t.Expr = expr match { - case fi: FunctionInvocation if fi.tfd.flags.contains(ImplPrivate) => - inlineFunctionInvocations(fi.copy(args = fi.args map transform).copiedFrom(fi)).copiedFrom(fi) - - case _ => super.transform(expr) - } - - private def inlineFunctionInvocations(fi: FunctionInvocation): Expr = { - val (tfd, args) = (fi.tfd, fi.args) - - import exprOps._ - val specced = BodyWithSpecs(tfd.fullBody) - - if (specced.getSpec(PreconditionKind).isDefined) { - context.reporter.internalError(s"Unexpected precondition on @implPrivate function ${fi.tfd.id}") - return fi - } - if (specced.getSpec(PostconditionKind).isDefined) { - context.reporter.internalError(s"Unexpected postcondition on @implPrivate function ${fi.tfd.id}") - return fi - } - - val result = (tfd.params zip args).foldRight(specced.body) { - case ((vd, e), body) => let(vd, e, body).setPos(fi) - } - - val freshened = exprOps.freshenLocals(result) - - // NOTE: We assume that there is nothing further to IP-inline in ImplPrivate bodies - freshened - } -} - -object ImplPrivateInlining { - def apply(p: Program, ctx: inox.Context): inox.transformers.SymbolTransformer { - val s: p.trees.type - val t: p.trees.type - } = new inox.transformers.SymbolTransformer { - val s: p.trees.type = p.trees - val t: p.trees.type = p.trees - - def transform(syms: s.Symbols): t.Symbols = { - object inlining extends ImplPrivateInlining { - val s: p.trees.type = p.trees - val t: p.trees.type = p.trees - val symbols: p.symbols.type = p.symbols - val context: inox.Context = ctx - } - - t.NoSymbols - .withFunctions(syms.functions.values.toSeq.collect { - case fd if fd.flags.contains(t.ImplPrivate) => - // We assume there is nothing to IP-inline in ImplPrivate functions - fd - - case fd => - val specced = s.exprOps.BodyWithSpecs(fd.fullBody) - val newSpecced = specced.copy( - specs = specced.specs.map(_.transform(inlining.transform(_))), - body = inlining.transform(specced.body) - ) - - new t.FunDef( - fd.id, - fd.tparams map inlining.transform, - fd.params map inlining.transform, - inlining.transform(fd.returnType), - newSpecced.reconstructed, - fd.flags map inlining.transform - ).copiedFrom(fd) - }) - .withSorts(syms.sorts.values.toSeq.map(inlining.transform)) - } - } -} diff --git a/core/src/main/scala/stainless/verification/VerificationComponent.scala b/core/src/main/scala/stainless/verification/VerificationComponent.scala index acae6de7d9..d0095f95a5 100644 --- a/core/src/main/scala/stainless/verification/VerificationComponent.scala +++ b/core/src/main/scala/stainless/verification/VerificationComponent.scala @@ -75,13 +75,6 @@ class VerificationRun(override val pipeline: StainlessPipeline) val t: self.trees.type = self.trees } - private[this] val debugImplPrivateInlining = new DebugSymbols { - val name = "ImplPrivateInlining" - val context = self.context - val s: self.trees.type = self.trees - val t: self.trees.type = self.trees - } - private[this] val debugChooses = new DebugSymbols { val name = "ChooseInjector" val context = self.context @@ -100,18 +93,9 @@ class VerificationRun(override val pipeline: StainlessPipeline) val assertions = AssertionInjector(p, context) val chooses = ChooseInjector(p) - val implPrivateInlining = ImplPrivateInlining(p, context) - - // Inline implementation private functions - val implPrivateEncoder = inox.transformers.ProgramEncoder(p)(implPrivateInlining) - - if (debugImplPrivateInlining.isEnabled) { - debugImplPrivateInlining.debugEncoder(implPrivateEncoder) - } - // We do not need to encode empty trees as chooses when generating the VCs, // as we rely on having empty trees to filter out some VCs. - val assertionEncoder = inox.transformers.ProgramEncoder(implPrivateEncoder.targetProgram)(assertions) + val assertionEncoder = inox.transformers.ProgramEncoder(p)(assertions) if (debugAssertions.isEnabled) { debugAssertions.debugEncoder(assertionEncoder) @@ -128,7 +112,7 @@ class VerificationRun(override val pipeline: StainlessPipeline) reporter.debug(s"Generating VCs for functions: ${functions map { _.uniqueName } mkString ", "}") } - val vcGenEncoder = implPrivateEncoder andThen assertionEncoder + val vcGenEncoder = assertionEncoder val vcs = if (context.options.findOptionOrDefault(optTypeChecker)) context.timers.verification.get("type-checker").run {