diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala index 304de1bcf..df179325a 100644 --- a/src/main/scala/viper/silver/ast/Ast.scala +++ b/src/main/scala/viper/silver/ast/Ast.scala @@ -6,16 +6,17 @@ package viper.silver.ast -import scala.collection.mutable -import scala.reflect.ClassTag -import pretty.FastPrettyPrinter -import utility._ +import viper.silver.ast.pretty.FastPrettyPrinter +import viper.silver.ast.utility._ import viper.silver.ast.utility.rewriter.Traverse.Traverse import viper.silver.ast.utility.rewriter.{Rewritable, StrategyBuilder, Traverse} import viper.silver.parser.PNode import viper.silver.verifier.errors.ErrorNode import viper.silver.verifier.{AbstractVerificationError, ConsistencyError, ErrorReason} +import scala.collection.mutable +import scala.reflect.ClassTag + /* This is the Viper abstract syntax description. diff --git a/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala b/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala index e3587c590..ff39a8834 100644 --- a/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala +++ b/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala @@ -227,7 +227,7 @@ object ImpureAssumeRewriter { }).execute(p) val pAssume: Program = ViperStrategy.Slim({ - case a: Assume => rewriteInhale(Inhale(rewrite(a.exp, pInvs))(a.pos)) + case a: Assume => rewriteInhale(Inhale(rewrite(a.exp, pInvs))(a.pos, a.info, a.errT)) }).execute(pInvs) if (funcs.isEmpty && domains.isEmpty) { diff --git a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala index 5d99d4e62..176b43a97 100644 --- a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala +++ b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala @@ -9,6 +9,7 @@ package viper.silver.ast.utility import scala.collection.mutable import scala.language.postfixOps import viper.silver.ast._ +import viper.silver.dependencyAnalysis.AnalysisSourceInfo /** Utility methods for quantified predicate permissions. */ object QuantifiedPermissions { @@ -164,7 +165,7 @@ object QuantifiedPermissions { def desugarSourceQuantifiedPermissionSyntax(source: Forall): Seq[Forall] = { - source match { + val res = source match { case SourceQuantifiedPermissionAssertion(_, Implies(cond, rhs)) if (!rhs.isPure) => /* Source forall denotes a quantified permission assertion that potentially * needs to be desugared @@ -272,5 +273,7 @@ object QuantifiedPermissions { */ Seq(source) } + + res.map(e => e.withMeta(e.pos, MakeInfoPair(AnalysisSourceInfo.createAnalysisSourceInfo(e), e.info), e.errT)) } } diff --git a/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala b/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala index 434c2ccf4..7a78a6585 100644 --- a/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala +++ b/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala @@ -6,8 +6,9 @@ package viper.silver.ast.utility.rewriter +import viper.silver.ast._ import viper.silver.parser.PNode -import viper.silver.ast.{AtomicType, BackendFuncApp, DomainFuncApp, ErrorTrafo, FuncApp, Info, Node, Position} +import viper.silver.plugin.standard.adt.{AdtConstructor, AdtConstructorApp, AdtDestructorApp, AdtDiscriminatorApp} import scala.reflect.runtime.{universe => reflection} @@ -45,7 +46,7 @@ trait Rewritable extends Product { // Add additional arguments to constructor call, besides children val firstArgList = children var secondArgList = Seq.empty[Any] - import viper.silver.ast.{DomainType, DomainAxiom, FuncApp, DomainFunc, DomainFuncApp} + import viper.silver.ast.{DomainAxiom, DomainFunc, DomainFuncApp, DomainType, FuncApp} this match { // TODO: remove the following cases by implementing `HasExtraValList` on the respective classes case dt: DomainType => secondArgList = Seq(dt.typeParameters) @@ -112,6 +113,12 @@ trait Rewritable extends Product { val arguments = this match { case fa: FuncApp => this.children ++ Seq(pos, info, fa.typ, trafo) case df: DomainFuncApp => this.children ++ Seq(pos, info, df.typ, df.domainName, trafo) + case bfa: BackendFuncApp => this.children ++ Seq(pos, info, bfa.typ, bfa.interpretation, trafo) + case dm: DomainMember => this.children ++ Seq(pos, info, dm.domainName, trafo) + case d: AdtDiscriminatorApp => this.children ++ Seq(pos, info, d.adtName, trafo) + case d: AdtConstructor => this.children ++ Seq(pos, info, d.typ, d.adtName, trafo) + case d: AdtConstructorApp => this.children ++ Seq(pos, info, d.typ, d.adtName, trafo) + case d: AdtDestructorApp => this.children ++ Seq(pos, info, d.typ, d.adtName, trafo) case _ => this.children ++ Seq(pos, info, trafo) } diff --git a/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala b/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala index b7ca5648b..360e162e4 100644 --- a/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala +++ b/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala @@ -10,8 +10,8 @@ import viper.silver.ast._ import viper.silver.cfg._ import viper.silver.cfg.silver.SilverCfg.{SilverBlock, SilverEdge} import viper.silver.cfg.utility.{CfgSimplifier, IdInfo, LoopDetector} -import java.util.concurrent.atomic.AtomicInteger +import java.util.concurrent.atomic.AtomicInteger import scala.collection.mutable /** diff --git a/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala b/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala new file mode 100644 index 000000000..daafdcf0a --- /dev/null +++ b/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala @@ -0,0 +1,80 @@ +package viper.silver.dependencyAnalysis + +import viper.silver.ast +import viper.silver.ast._ + +object AnalysisSourceInfo { + def extractPositionString(p: Position): String = { + p match { + case NoPosition => "???" + case filePos: AbstractSourcePosition => filePos.file.getFileName.toString + " @ line " + filePos.line + case filePos: FilePosition => filePos.file.getFileName.toString + " @ line " + filePos.line + case lineColumn: HasLineColumn => "line " + lineColumn.line.toString + case VirtualPosition(identifier) => "label " + identifier + } + } + + def createAnalysisSourceInfo(node: ast.Node): AnalysisSourceInfo = { + node match { + case stmt: ast.Stmt => StmtAnalysisSourceInfo(stmt, stmt.pos) + case exp: ast.Exp => ExpAnalysisSourceInfo(exp, exp.pos) + case _ => createAnalysisSourceInfo("Unknown", NoPosition) + } + } + + def createAnalysisSourceInfo(description: String, pos: Position): AnalysisSourceInfo = StringAnalysisSourceInfo(description, pos) + +} + +trait AnalysisSourceInfo extends ast.Info { + override def toString: String = getPositionString + + def getDescription: String + + def getLineNumber: Option[Int] = getPosition match { + case column: HasLineColumn => Some(column.line) + case _ => None + } + + def getPositionString: String = { + AnalysisSourceInfo.extractPositionString(getPosition) + } + + def getPosition: Position + + override def comment: Seq[String] = Nil + override def isCached: Boolean = false +} + +case class NoAnalysisSourceInfo() extends AnalysisSourceInfo { + override def getPosition: Position = NoPosition + + override def getDescription: String = "" + + override def equals(obj: Any): Boolean = false +} + +case class ExpAnalysisSourceInfo(source: ast.Exp, pos: Position) extends AnalysisSourceInfo { + + override def toString: String = getDescription + " (" + super.toString + ")" + + override def getPosition: Position = pos + + override def getDescription: String = source.toString.replaceAll("\n", "\t") +} + +case class StmtAnalysisSourceInfo(source: ast.Stmt, pos: Position) extends AnalysisSourceInfo { + + override def toString: String = getDescription + " (" + super.toString + ")" + override def getPosition: Position = pos + + override def getDescription: String = source.toString().replaceAll("\n", "\t") +} + +case class StringAnalysisSourceInfo(description: String, position: Position) extends AnalysisSourceInfo { + override def toString: String = getDescription + " (" + getPositionString + ")" + override def getPosition: Position = position + + override def getDescription: String = description.replaceAll("\n", "\t") +} + diff --git a/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala b/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala new file mode 100644 index 000000000..fcf28efc0 --- /dev/null +++ b/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala @@ -0,0 +1,114 @@ +package viper.silver.dependencyAnalysis + +import viper.silver.ast +import viper.silver.dependencyAnalysis.DependencyType._ +import viper.silver.dependencyAnalysis.EdgeType.EdgeType +import viper.silver.dependencyAnalysis.JoinType.JoinType + +object DependencyTypeInfo { + def getDependencyTypeInfo(stmt: ast.Stmt): DependencyTypeInfo = { + val depType = stmt match { + case _: ast.MethodCall => MethodCall + case _: ast.NewStmt | _: ast.AbstractAssign => SourceCode + case _: ast.Exhale | _: ast.Assert => ExplicitAssertion + case _: ast.Inhale | _: ast.Assume => ExplicitAssumption + case _: ast.Fold | _: ast.Unfold | _: ast.Package | _: ast.Apply => Rewrite + case _: ast.Quasihavoc | _: ast.Quasihavocall => DependencyType.SourceCode + case _ => DependencyType.make(AssumptionType.Unknown) /* TODO: should not happen */ + } + DependencyTypeInfo(depType) + } +} + +case class DependencyTypeInfo(dependencyType: DependencyType) extends ast.Info { + + override def comment: Seq[String] = Nil + override def isCached: Boolean = false +} + +object JoinType extends Enumeration { + type JoinType = Value + val Source, Sink = Value +} + +object EdgeType extends Enumeration { + type EdgeType = Value + val Up, Down = Value +} + +/** + * Represent the piece of information to be stored in dependency nodes in order to join dependency graphs of + * individual verification components. Nodes with matching join information are connected by an interprocedural edge. + */ +trait DependencyAnalysisJoinInfo extends ast.Info { + override def comment: Seq[String] = Nil + override def isCached: Boolean = false + + def matches(dependencyAnalysisJoinInfo: DependencyAnalysisJoinInfo) = { + (this, dependencyAnalysisJoinInfo) match { + case (SimpleDependencyAnalysisJoin(sourceInfo, joinType, edgeType), SimpleDependencyAnalysisJoin(sourceInfo1, joinType1, edgeType1)) => + sourceInfo.equals(sourceInfo1) && edgeType.equals(edgeType1) + } + } +} + +case class EvalStackDependencyAnalysisJoin(joinType: JoinType, edgeType: EdgeType) extends DependencyAnalysisJoinInfo + +case class SimpleDependencyAnalysisJoin(sourceInfo: AnalysisSourceInfo, joinType: JoinType, edgeType: EdgeType) extends DependencyAnalysisJoinInfo + +/** + * Represent the piece of information to be stored in dependency nodes in order to finalize the intraprocedural + * dependency graph. Nodes with matching merge information are connected by an intraprocedural edge. + */ +trait DependencyAnalysisMergeInfo extends ast.Info { + + def isMerge: Boolean + + override def comment: Seq[String] = Nil + override def isCached: Boolean = false +} + +case class NoDependencyAnalysisMerge() extends DependencyAnalysisMergeInfo { + override def isMerge: Boolean = false +} + +case class SimpleDependencyAnalysisMerge(sourceInfo: AnalysisSourceInfo) extends DependencyAnalysisMergeInfo { + override def isMerge: Boolean = true +} + +case class CompositeDependencyAnalysisMergeInfo(sourceInfo1: AnalysisSourceInfo, sourceInfo2: AnalysisSourceInfo) extends DependencyAnalysisMergeInfo { + override def isMerge: Boolean = true +} + +object DependencyAnalysisMergeInfo { + def attachExpMergeInfo(exps: Seq[ast.Exp], sourceInfo2: Option[AnalysisSourceInfo]): Seq[ast.Exp] = { + exps.map(attachExpMergeInfo(_, sourceInfo2)) + } + + def attachExpMergeInfo(exp: ast.Exp, sourceInfo2: Option[AnalysisSourceInfo]): ast.Exp = { + val expSourceInfo = AnalysisSourceInfo.createAnalysisSourceInfo(exp) + attachExpMergeInfo(exp, expSourceInfo, sourceInfo2) + } + + def attachExpMergeInfo(exp: ast.Exp, mergeInfo: DependencyAnalysisMergeInfo): ast.Exp = { + exp.withMeta((exp.pos, ast.MakeInfoPair(mergeInfo, exp.info), exp.errT)) + } + + def attachExpMergeInfo(exp: ast.Exp, sourceInfo1: AnalysisSourceInfo, sourceInfo2: Option[AnalysisSourceInfo]): ast.Exp = { + val mergeInfo = if(sourceInfo2.isDefined) + CompositeDependencyAnalysisMergeInfo(sourceInfo1, sourceInfo2.get) + else + SimpleDependencyAnalysisMerge(sourceInfo1) + exp.withMeta((exp.pos, ast.MakeInfoPair(mergeInfo, exp.info), exp.errT)) + } +} + +trait AdditionalDependencyNodeInfo extends ast.Info { + + override def comment: Seq[String] = Nil + override def isCached: Boolean = false +} + +case class AdditionalAssertionNode() extends AdditionalDependencyNodeInfo + +case class AdditionalAssumptionNode() extends AdditionalDependencyNodeInfo diff --git a/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala new file mode 100644 index 000000000..cffd2dbf3 --- /dev/null +++ b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala @@ -0,0 +1,54 @@ +package viper.silver.dependencyAnalysis + +object AssumptionType extends Enumeration { + type AssumptionType = Value + val Explicit, LoopInvariant, PathCondition, Rewrite, SourceCode, DomainAxiom, Implicit, Internal, Trigger, ExplicitPostcondition, ImplicitPostcondition, ImportedPostcondition, MethodCall, FunctionBody, Precondition, Ghost, Annotation, Unknown = Value + + def fromString(s: String): Option[Value] = values.find(_.toString == s) + + def explicitAssumptionTypes: Set[AssumptionType] = Set(Explicit, ExplicitPostcondition) + def postconditionTypes: Set[AssumptionType] = Set(ImplicitPostcondition, ExplicitPostcondition, ImportedPostcondition) + def preconditionTypes: Set[AssumptionType] = Set(Precondition) + def explicitAssertionTypes: Set[AssumptionType] = Set(Explicit, ImplicitPostcondition, ExplicitPostcondition) + def internalTypes: Set[AssumptionType] = Set(Internal, Trigger) // will always be hidden from user + def importedTypes: Set[AssumptionType] = Set(ImportedPostcondition) + def verificationAnnotationTypes: Set[AssumptionType] = Set(FunctionBody /* TODO ake: review */, LoopInvariant, Rewrite, ExplicitPostcondition, ImplicitPostcondition, ImportedPostcondition, Precondition, Explicit, DomainAxiom, Annotation) + + + def getPostcondType(isAbstractFunction: Boolean, dependencyType: Option[DependencyType]=None, isImported: Boolean=false): AssumptionType = { + if(isImported) return ImportedPostcondition + + dependencyType.flatMap(_.assertionType match { + case AssumptionType.Explicit | AssumptionType.ExplicitPostcondition => Some(AssumptionType.ExplicitPostcondition) + case AssumptionType.ImportedPostcondition => Some(AssumptionType.ImportedPostcondition) + case AssumptionType.ImplicitPostcondition => Some(AssumptionType.ImplicitPostcondition) + case AssumptionType.Internal => Some(AssumptionType.Internal) + case AssumptionType.Annotation | AssumptionType.Ghost => None + case _ => None + }).getOrElse( + if(isAbstractFunction) AssumptionType.ExplicitPostcondition else AssumptionType.ImplicitPostcondition + ) + } +} + +import viper.silver.dependencyAnalysis.AssumptionType.AssumptionType + +object DependencyType { + val SourceCode: DependencyType = make(AssumptionType.SourceCode) + val Explicit: DependencyType = make(AssumptionType.Explicit) + val ExplicitAssertion: DependencyType = DependencyType(AssumptionType.Internal, AssumptionType.Explicit) + val ExplicitAssumption: DependencyType = DependencyType(AssumptionType.Explicit, AssumptionType.Implicit) + val PathCondition: DependencyType = make(AssumptionType.PathCondition) + val Invariant: DependencyType = make(AssumptionType.LoopInvariant) + val Rewrite: DependencyType = make(AssumptionType.Rewrite) + val Internal: DependencyType = make(AssumptionType.Internal) + val Trigger: DependencyType = make(AssumptionType.Trigger) + val MethodCall: DependencyType = make(AssumptionType.MethodCall) + val Ghost: DependencyType = make(AssumptionType.Ghost) + val Annotation: DependencyType = make(AssumptionType.Annotation) + val Axiom: DependencyType = make(AssumptionType.DomainAxiom) + + def make(singleType: AssumptionType): DependencyType = DependencyType(singleType, singleType) +} + +case class DependencyType(assumptionType: AssumptionType, assertionType: AssumptionType) diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala index a09b825bd..9babebff6 100644 --- a/src/main/scala/viper/silver/parser/Translator.scala +++ b/src/main/scala/viper/silver/parser/Translator.scala @@ -9,6 +9,7 @@ package viper.silver.parser import viper.silver.FastMessaging import viper.silver.ast.utility._ import viper.silver.ast.{SourcePosition, _} +import viper.silver.dependencyAnalysis._ import viper.silver.plugin.standard.adt.{Adt, AdtType} import scala.collection.mutable @@ -82,7 +83,9 @@ case class Translator(program: PProgram) { val newBody = body.map(actualBody => stmt(actualBody).asInstanceOf[Seqn]) - val finalMethod = m.copy(pres = pres.toSeq map (p => exp(p.e)), posts = posts.toSeq map (p => exp(p.e)), body = newBody)(m.pos, m.info, m.errT) + val postconditionType = if(body.isDefined) DependencyType.make(AssumptionType.ImplicitPostcondition) else DependencyType.make(AssumptionType.ExplicitPostcondition) + + val finalMethod = m.copy(pres = pres.toSeq map (p => exp(p.e, Some(DependencyType.make(AssumptionType.Precondition)))), posts = posts.toSeq map (p => exp(p.e, Some(postconditionType))), body = newBody)(m.pos, m.info, m.errT) members(m.name) = finalMethod @@ -98,17 +101,27 @@ case class Translator(program: PProgram) { dd } - private def translate(a: PAxiom): DomainAxiom = a match { - case pa@PAxiom(anns, _, Some(name), e) => - NamedDomainAxiom(name.name, exp(e.e.inner))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name) - case pa@PAxiom(anns, _, None, e) => - AnonymousDomainAxiom(exp(e.e.inner))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name) + private def translate(a: PAxiom): DomainAxiom = { + def attachInfo(axiom: DomainAxiom) = { + val info = ConsInfo(axiom.info, ConsInfo(ConsInfo(AnalysisSourceInfo.createAnalysisSourceInfo(axiom.exp), DependencyTypeInfo(DependencyType.Axiom)), SimpleDependencyAnalysisJoin(AnalysisSourceInfo.createAnalysisSourceInfo(axiom.exp), JoinType.Source, EdgeType.Down))) + axiom.withMeta(axiom.pos, info, axiom.errT) + } + + a match { + case pa@PAxiom(anns, _, Some(name), e) => + val axiom = NamedDomainAxiom(name.name, exp(e.e.inner, Some(DependencyType.Axiom)))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name) + attachInfo(axiom) + case pa@PAxiom(anns, _, None, e) => + val axiom = AnonymousDomainAxiom(exp(e.e.inner, Some(DependencyType.Axiom)))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name) + attachInfo(axiom) + } } private def translate(f: PFunction): Function = f match { case PFunction(_, _, idndef, _, _, _, pres, posts, body) => val f = findFunction(idndef) - val ff = f.copy( pres = pres.toSeq map (p => exp(p.e)), posts = posts.toSeq map (p => exp(p.e)), body = body map (_.e.inner) map exp)(f.pos, f.info, f.errT) + val postconditionType = if(body.isDefined) DependencyType.make(AssumptionType.ImplicitPostcondition) else DependencyType.make(AssumptionType.ExplicitPostcondition) + val ff = f.copy( pres = pres.toSeq map (p => exp(p.e, Some(DependencyType.make(AssumptionType.Precondition)))), posts = posts.toSeq map (p => exp(p.e, Some(postconditionType))), body = body map (_.e.inner) map (exp(_, Some(DependencyType.make(AssumptionType.FunctionBody)))))(f.pos, f.info, f.errT) members(f.name) = ff ff } @@ -116,7 +129,7 @@ case class Translator(program: PProgram) { private def translate(p: PPredicate): Predicate = p match { case PPredicate(_, _, idndef, _, body) => val p = findPredicate(idndef) - val pp = p.copy(body = body map (_.e.inner) map exp)(p.pos, p.info, p.errT) + val pp = p.copy(body = body map (_.e.inner) map (exp(_, Some(DependencyType.Rewrite))))(p.pos, p.info, p.errT) members(p.name) = pp pp } @@ -176,7 +189,7 @@ case class Translator(program: PProgram) { val (s, annotations) = extractAnnotationFromStmt(pStmt) val sourcePNodeInfo = SourcePNodeInfo(pStmt) val info = if (annotations.isEmpty) sourcePNodeInfo else ConsInfo(sourcePNodeInfo, AnnotationInfo(annotations)) - s match { + val resS = s match { case PAssign(targets, _, PCall(method, args, _)) if members(method.name).isInstanceOf[Method] => methodCallAssign(s, targets.toSeq, ts => MethodCall(findMethod(method), args.inner.toSeq map exp, ts)(pos, info)) case PAssign(targets, _, _) if targets.length != 1 => @@ -206,34 +219,34 @@ case class Translator(program: PProgram) { }.flatten Seqn(seqn filterNot (_.isInstanceOf[PSkip]) map stmt, locals)(pos, info) case PFold(_, e) => - Fold(exp(e).asInstanceOf[PredicateAccessPredicate])(pos, info) + Fold(exp(e, Some(DependencyType.Rewrite)).asInstanceOf[PredicateAccessPredicate])(pos, info) case PUnfold(_, e) => - Unfold(exp(e).asInstanceOf[PredicateAccessPredicate])(pos, info) + Unfold(exp(e, Some(DependencyType.Rewrite)).asInstanceOf[PredicateAccessPredicate])(pos, info) case PPackageWand(_, e, proofScript) => - val wand = exp(e).asInstanceOf[MagicWand] + val wand = exp(e, Some(DependencyType.Rewrite)).asInstanceOf[MagicWand] Package(wand, proofScript map (stmt(_).asInstanceOf[Seqn]) getOrElse Statements.EmptyStmt)(pos, info) case PApplyWand(_, e) => - Apply(exp(e).asInstanceOf[MagicWand])(pos, info) + Apply(exp(e, Some(DependencyType.Rewrite)).asInstanceOf[MagicWand])(pos, info) case PInhale(_, e) => - Inhale(exp(e))(pos, info) + Inhale(exp(e, Some(DependencyType.ExplicitAssumption)))(pos, info) case PAssume(_, e) => - Assume(exp(e))(pos, info) + Assume(exp(e, Some(DependencyType.ExplicitAssumption)))(pos, info) case PExhale(_, e) => - Exhale(exp(e))(pos, info) + Exhale(exp(e, Some(DependencyType.ExplicitAssertion)))(pos, info) case PAssert(_, e) => - Assert(exp(e))(pos, info) + Assert(exp(e, Some(DependencyType.ExplicitAssertion)))(pos, info) case PLabel(_, name, invs) => Label(name.name, invs.toSeq map (_.e) map exp)(pos, info) case PGoto(_, label) => Goto(label.name)(pos, info) case PIf(_, cond, thn, els) => - If(exp(cond.inner), stmt(thn).asInstanceOf[Seqn], els map (stmt(_) match { + If(exp(cond.inner, Some(DependencyType.PathCondition)), stmt(thn).asInstanceOf[Seqn], els map (stmt(_) match { case s: Seqn => s case s => Seqn(Seq(s), Nil)(s.pos, s.info) }) getOrElse Statements.EmptyStmt)(pos, info) case PElse(_, els) => stmt(els) case PWhile(_, cond, invs, body) => - While(exp(cond.inner), invs.toSeq map (inv => exp(inv.e)), stmt(body).asInstanceOf[Seqn])(pos, info) + While(exp(cond.inner, Some(DependencyType.PathCondition)), invs.toSeq map (inv => exp(inv.e, Some(DependencyType.Invariant))), stmt(body).asInstanceOf[Seqn])(pos, info) case PQuasihavoc(_, lhs, e) => val (newLhs, newE) = havocStmtHelper(lhs, e) Quasihavoc(newLhs, newE)(pos, info) @@ -245,6 +258,7 @@ case class Translator(program: PProgram) { case _: PDefine | _: PSkip => sys.error(s"Found unexpected intermediate statement $s (${s.getClass.getName}})") } + resS.withMeta(resS.pos, MakeInfoPair(MakeInfoPair(AnalysisSourceInfo.createAnalysisSourceInfo(resS), DependencyTypeInfo.getDependencyTypeInfo(resS)), resS.info), resS.errT) } /** @@ -342,17 +356,23 @@ case class Translator(program: PProgram) { } } + def exp(parseExp: PExp): Exp = exp(parseExp, None) + /** Takes a `PExp` and turns it into an `Exp`. */ - def exp(parseExp: PExp): Exp = { + def exp(parseExp: PExp, dependencyType: Option[DependencyType]): Exp = { val pos = parseExp val (pexp, annotationMap) = extractAnnotation(parseExp) val sourcePNodeInfo = SourcePNodeInfo(parseExp) - val info = if (annotationMap.isEmpty) sourcePNodeInfo else ConsInfo(sourcePNodeInfo, AnnotationInfo(annotationMap)) - expInternal(pexp, pos, info) + val info0 = if (annotationMap.isEmpty) sourcePNodeInfo else ConsInfo(sourcePNodeInfo, AnnotationInfo(annotationMap)) + val info = if(dependencyType.isDefined) MakeInfoPair(info0, DependencyTypeInfo(dependencyType.get)) else info0 + expInternal(pexp, pos, info, dependencyType) } - protected def expInternal(pexp: PExp, pos: PExp, info: Info): Exp = { - pexp match { + protected def expInternal(pexp: PExp, pos: PExp, info: Info, dependencyType: Option[DependencyType]): Exp = { + + def goExp(parseExp: PExp) = exp(parseExp, dependencyType) + + val expr = pexp match { case PIdnUseExp(piu) => piu.decl match { case Some(_: PTypedVarDecl) => LocalVar(piu.name, ttyp(pexp.typ))(pos, info) @@ -361,7 +381,7 @@ case class Translator(program: PProgram) { case _ => sys.error("should not occur in type-checked program") } case pbe @ PBinExp(left, op, right) => - val (l, r) = (exp(left), exp(right)) + val (l, r) = (goExp(left), goExp(right)) op.rs match { case PSymOp.Plus => r.typ match { @@ -454,7 +474,7 @@ case class Translator(program: PProgram) { case _ => sys.error(s"unexpected operator $op") } case PUnExp(op, pe) => - val e = exp(pe) + val e = goExp(pe) op.rs match { case PSymOp.Neg => e.typ match { @@ -465,7 +485,7 @@ case class Translator(program: PProgram) { case PSymOp.Not => Not(e)(pos, info) } case PInhaleExhaleExp(_, in, _, ex, _) => - InhaleExhaleExp(exp(in), exp(ex))(pos, info) + InhaleExhaleExp(goExp(in), goExp(ex))(pos, info) case PIntLit(i) => IntLit(i)(pos, info) case p@PResultLit(_) => @@ -477,13 +497,13 @@ case class Translator(program: PProgram) { case PNullLit(_) => NullLit()(pos, info) case PFieldAccess(rcv, _, idn) => - FieldAccess(exp(rcv), findField(idn))(pos, info) - case PMagicWandExp(left, _, right) => MagicWand(exp(left), exp(right))(pos, info) + FieldAccess(goExp(rcv), findField(idn))(pos, info) + case PMagicWandExp(left, _, right) => MagicWand(goExp(left), goExp(right))(pos, info) case pfa@PCall(func, args, _) => members(func.name) match { - case f: Function => FuncApp(f, args.inner.toSeq map exp)(pos, info) + case f: Function => FuncApp(f, args.inner.toSeq map goExp)(pos, info) case f @ DomainFunc(_, _, _, _, _) => - val actualArgs = args.inner.toSeq map exp + val actualArgs = args.inner.toSeq map goExp /* TODO: Not used - problem?*/ type TypeSubstitution = Map[TypeVar, Type] val so : Option[TypeSubstitution] = pfa.domainSubstitution match{ @@ -503,33 +523,33 @@ case class Translator(program: PProgram) { case _ => sys.error("type unification error - should report and not crash") } case _: Predicate => - val inner = PredicateAccess(args.inner.toSeq map exp, findPredicate(func).name) (pos, info) + val inner = PredicateAccess(args.inner.toSeq map goExp, findPredicate(func).name) (pos, info) PredicateAccessPredicate(inner, None) (pos, info) case _ => sys.error("unexpected reference to non-function") } case PNewExp(_, _) => sys.error("unexpected `new` expression") case PUnfolding(_, loc, _, e) => - Unfolding(exp(loc).asInstanceOf[PredicateAccessPredicate], exp(e))(pos, info) + Unfolding(goExp(loc).asInstanceOf[PredicateAccessPredicate], goExp(e))(pos, info) case PApplying(_, wand, _, e) => - Applying(exp(wand).asInstanceOf[MagicWand], exp(e))(pos, info) + Applying(goExp(wand).asInstanceOf[MagicWand], goExp(e))(pos, info) case PAsserting(_, a, _, e) => - Asserting(exp(a), exp(e))(pos, info) + Asserting(goExp(a), goExp(e))(pos, info) case pl@PLet(_, _, _, exp1, _, PLetNestedScope(body)) => - Let(liftLogicalDecl(pl.decl), exp(exp1.inner), exp(body))(pos, info) + Let(liftLogicalDecl(pl.decl), goExp(exp1.inner), goExp(body))(pos, info) case _: PLetNestedScope => sys.error("unexpected node PLetNestedScope, should only occur as a direct child of PLet nodes") case PExists(_, vars, _, triggers, e) => - val ts = triggers map (t => Trigger((t.exp.inner.toSeq map exp) map (e => e match { + val ts = triggers map (t => Trigger((t.exp.inner.toSeq map goExp) map (e => e match { case PredicateAccessPredicate(inner, _) => inner case _ => e }))(t)) - Exists(vars.toSeq map liftLogicalDecl, ts, exp(e))(pos, info) + Exists(vars.toSeq map liftLogicalDecl, ts, goExp(e))(pos, info) case PForall(_, vars, _, triggers, e) => - val ts = triggers map (t => Trigger((t.exp.inner.toSeq map exp) map (e => e match { + val ts = triggers map (t => Trigger((t.exp.inner.toSeq map goExp) map (e => e match { case PredicateAccessPredicate(inner, _) => inner case _ => e }))(t)) - val fa = Forall(vars.toSeq map liftLogicalDecl, ts, exp(e))(pos, info) + val fa = Forall(vars.toSeq map liftLogicalDecl, ts, goExp(e))(pos, info) if (fa.isPure) { fa } else { @@ -539,21 +559,21 @@ case class Translator(program: PProgram) { } case fp@PForPerm(_, vars, _, _, e) => val varList = vars.toSeq map liftLogicalDecl - exp(fp.accessRes) match { - case PredicateAccessPredicate(inner, _) => ForPerm(varList, inner, exp(e))(pos, info) - case f : FieldAccess => ForPerm(varList, f, exp(e))(pos, info) - case p : PredicateAccess => ForPerm(varList, p, exp(e))(pos, info) - case w : MagicWand => ForPerm(varList, w, exp(e))(pos, info) + goExp(fp.accessRes) match { + case PredicateAccessPredicate(inner, _) => ForPerm(varList, inner, goExp(e))(pos, info) + case f : FieldAccess => ForPerm(varList, f, goExp(e))(pos, info) + case p : PredicateAccess => ForPerm(varList, p, goExp(e))(pos, info) + case w : MagicWand => ForPerm(varList, w, goExp(e))(pos, info) case other => sys.error(s"Internal Error: Unexpectedly found $other in forperm") } case POldExp(_, lbl, e) => - val ee = exp(e.inner) + val ee = goExp(e.inner) lbl.map(l => LabelledOld(ee, l.inner.fold(_.rs.keyword, _.name))(pos, info)).getOrElse(Old(ee)(pos, info)) case PCondExp(cond, _, thn, _, els) => - CondExp(exp(cond), exp(thn), exp(els))(pos, info) + CondExp(goExp(cond), goExp(thn), goExp(els))(pos, info) case PCurPerm(_, res) => - exp(res.inner) match { + goExp(res.inner) match { case PredicateAccessPredicate(inner, _) => CurrentPerm(inner)(pos, info) case x: FieldAccess => CurrentPerm(x)(pos, info) case x: PredicateAccess => CurrentPerm(x)(pos, info) @@ -569,8 +589,8 @@ case class Translator(program: PProgram) { case PEpsilon(_) => EpsilonPerm()(pos, info) case acc: PAccPred => - val p = acc.permExp.map(exp) - exp(acc.loc) match { + val p = acc.permExp.map(goExp) + goExp(acc.loc) match { case loc@FieldAccess(_, _) => FieldAccessPredicate(loc, p)(pos, info) case loc@PredicateAccess(_, _) => @@ -582,58 +602,59 @@ case class Translator(program: PProgram) { case _: PEmptySeq => EmptySeq(ttyp(pexp.typ.asInstanceOf[PSeqType].elementType.inner))(pos, info) case PExplicitSeq(_, elems) => - ExplicitSeq(elems.inner.toSeq map exp)(pos, info) + ExplicitSeq(elems.inner.toSeq map goExp)(pos, info) case PRangeSeq(_, low, _, high, _) => - RangeSeq(exp(low), exp(high))(pos, info) + RangeSeq(goExp(low), goExp(high))(pos, info) case PLookup(base, _, index, _) => base.typ match { - case _: PSeqType => SeqIndex(exp(base), exp(index))(pos, info) - case _: PMapType => MapLookup(exp(base), exp(index))(pos, info) + case _: PSeqType => SeqIndex(goExp(base), goExp(index))(pos, info) + case _: PMapType => MapLookup(goExp(base), goExp(index))(pos, info) case t => sys.error(s"unexpected type $t") } case PSeqSlice(seq, _, s, _, e, _) => - val es = exp(seq) - val ss = e.map(exp).map(SeqTake(es, _)(pos, info)).getOrElse(es) - s.map(exp).map(SeqDrop(ss, _)(pos, info)).getOrElse(ss) + val es = goExp(seq) + val ss = e.map(goExp).map(SeqTake(es, _)(pos, info)).getOrElse(es) + s.map(goExp).map(SeqDrop(ss, _)(pos, info)).getOrElse(ss) case PUpdate(base, _, key, _, value, _) => base.typ match { - case _: PSeqType => SeqUpdate(exp(base), exp(key), exp(value))(pos, info) - case _: PMapType => MapUpdate(exp(base), exp(key), exp(value))(pos, info) + case _: PSeqType => SeqUpdate(goExp(base), goExp(key), goExp(value))(pos, info) + case _: PMapType => MapUpdate(goExp(base), goExp(key), goExp(value))(pos, info) case t => sys.error(s"unexpected type $t") } case PSize(_, base, _) => base.typ match { - case _: PSeqType => SeqLength(exp(base))(pos, info) - case _: PMapType => MapCardinality(exp(base))(pos, info) - case _: PSetType | _: PMultisetType => AnySetCardinality(exp(base))(pos, info) + case _: PSeqType => SeqLength(goExp(base))(pos, info) + case _: PMapType => MapCardinality(goExp(base))(pos, info) + case _: PSetType | _: PMultisetType => AnySetCardinality(goExp(base))(pos, info) case t => sys.error(s"unexpected type $t") } case _: PEmptySet => EmptySet(ttyp(pexp.typ.asInstanceOf[PSetType].elementType.inner))(pos, info) case PExplicitSet(_, elems) => - ExplicitSet(elems.inner.toSeq map exp)(pos, info) + ExplicitSet(elems.inner.toSeq map goExp)(pos, info) case _: PEmptyMultiset => EmptyMultiset(ttyp(pexp.typ.asInstanceOf[PMultisetType].elementType.inner))(pos, info) case PExplicitMultiset(_, elems) => - ExplicitMultiset(elems.inner.toSeq map exp)(pos, info) + ExplicitMultiset(elems.inner.toSeq map goExp)(pos, info) case _: PEmptyMap => EmptyMap( ttyp(pexp.typ.asInstanceOf[PMapType].keyType), ttyp(pexp.typ.asInstanceOf[PMapType].valueType) )(pos, info) case PExplicitMap(_, elems) => - ExplicitMap(elems.inner.toSeq map exp)(pos, info) + ExplicitMap(elems.inner.toSeq map goExp)(pos, info) case PMaplet(key, _, value) => - Maplet(exp(key), exp(value))(pos, info) + Maplet(goExp(key), goExp(value))(pos, info) case PMapDomain(_, base) => - MapDomain(exp(base.inner))(pos, info) + MapDomain(goExp(base.inner))(pos, info) case PMapRange(_, base) => - MapRange(exp(base.inner))(pos, info) + MapRange(goExp(base.inner))(pos, info) case t: PExtender => t.translateExp(this) } + expr.withMeta((expr.pos, MakeInfoPair(AnalysisSourceInfo.createAnalysisSourceInfo(expr), expr.info), expr.errT)) } implicit def liftPos(node: Where): SourcePosition = Translator.liftWhere(node) diff --git a/src/main/scala/viper/silver/plugin/standard/termination/transformation/DecreasesCheck.scala b/src/main/scala/viper/silver/plugin/standard/termination/transformation/DecreasesCheck.scala index 48c959f53..88bbda1e3 100644 --- a/src/main/scala/viper/silver/plugin/standard/termination/transformation/DecreasesCheck.scala +++ b/src/main/scala/viper/silver/plugin/standard/termination/transformation/DecreasesCheck.scala @@ -65,7 +65,8 @@ trait DecreasesCheck extends ProgramManager with ErrorReporter { * @param tupleCondition for which tuple decreasing should be checked (default: true) * @param errTrafo for termination related assertions * @param reasonTrafoFactory for termination related assertion reasons - * @return termination check as a Assert Stmt (if decreasing and bounded are defined, otherwise EmptyStmt) + * @return termination check as a + * Stmt (if decreasing and bounded are defined, otherwise EmptyStmt) */ protected def createTupleCheck(tupleCondition: Option[Exp], biggerTuple: Seq[Exp], smallerTuple: Seq[Exp], errTrafo: ErrTrafo, reasonTrafoFactory: ReasonTrafoFactory): Stmt = { @@ -87,11 +88,11 @@ trait DecreasesCheck extends ProgramManager with ErrorReporter { val decreasesSimpleReasonTrafo = reasonTrafoFactory.generateTupleSimpleFalse() val tupleImplies = tupleCondition match { - case Some(c) => Implies(c, lexCheck)(errT = decreasesSimpleReasonTrafo) + case Some(c) => Implies(c, lexCheck)(lexCheck.pos, lexCheck.info, decreasesSimpleReasonTrafo) case None => lexCheck } - val tupleAssert = Assert(tupleImplies)(errT = errTrafo) + val tupleAssert = Assert(tupleImplies)(lexCheck.pos, lexCheck.info, errTrafo) tupleAssert } @@ -158,13 +159,13 @@ trait DecreasesCheck extends ProgramManager with ErrorReporter { argTypeVarsDecr.last -> bigger.typ ))(errT = boundReTrafo) - val andPart = And(dec, bound)(errT = simpleReTrafo) + val andPart = And(dec, bound)(smaller.pos, smaller.info,simpleReTrafo) - val eq = EqCmp(smaller, bigger)(errT = decreasesReTrafo) + val eq = EqCmp(smaller, bigger)(smaller.pos, smaller.info, decreasesReTrafo) val next = createExp(bTuple.tail, sTuple.tail) - val nextPart = And(eq, next)(errT = simpleReTrafo) - Or(andPart, nextPart)(errT = simpleReTrafo) + val nextPart = And(eq, next)(eq.pos, eq.info, simpleReTrafo) + Or(andPart, nextPart)(smaller.pos, smaller.info, simpleReTrafo) } } }