From 2c8d3345df583c685f629754dc7b6062e81bd624 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 11 Jun 2024 17:45:30 +0200 Subject: [PATCH 1/3] Allow domain axioms to use functions that have requires clauses but no real preconditions --- .../scala/viper/silver/parser/Resolver.scala | 8 ++- .../resources/all/issues/silicon/0847.vpr | 68 +++++++++++++++++++ 2 files changed, 75 insertions(+), 1 deletion(-) create mode 100644 src/test/resources/all/issues/silicon/0847.vpr diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala index c3280c3a3..f562aed7c 100644 --- a/src/main/scala/viper/silver/parser/Resolver.scala +++ b/src/main/scala/viper/silver/parser/Resolver.scala @@ -7,6 +7,7 @@ package viper.silver.parser import viper.silver.FastMessaging +import viper.silver.parser.PKw.Requires import scala.collection.mutable @@ -685,8 +686,13 @@ case class TypeChecker(names: NameAnalyser) { check(fd.typ) fd.formalArgs foreach (a => check(a.typ)) } - if (pfa.isDescendant[PAxiom] && pfn.pres.length != 0) + if (pfa.isDescendant[PAxiom] && pfn.pres.toSeq.exists(pre => pre.k.rs == Requires)) { + // A domain axiom, which must always be well-defined, is calling a function that has at least + // one real precondition (i.e., not just a requires clause or something similar that's + // temporarily represented as a precondition), which means that the call may not always be + // well-defined. This is not allowed. issueError(func, s"Cannot use function ${func.name}, which has preconditions, inside axiom") + } case pdf: PDomainFunction => val domain = pdf.domain diff --git a/src/test/resources/all/issues/silicon/0847.vpr b/src/test/resources/all/issues/silicon/0847.vpr new file mode 100644 index 000000000..1b531f583 --- /dev/null +++ b/src/test/resources/all/issues/silicon/0847.vpr @@ -0,0 +1,68 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + + +function f1(i: Int): Int + decreases i + requires i > -2 +{ + i > 0 ? 1 + f1(i - 1) : 0 +} + +function f2(i: Int): Int + decreases i +{ + i > 0 ? 1 + f2(i - 1) : 0 +} + +function f3(i: Int): Int + decreases i + ensures result >= 0 +{ + i > 0 ? 1 + f3(i - 1) : 0 +} + +function f4(i: Int): Int + ensures result >= 0 + decreases _ +{ + i > 0 ? 1 + f4(i - 1) : 0 +} + +function f5(i: Int): Int + requires i > -2 + decreases i + ensures result >= 0 +{ + i > 0 ? 1 + f5(i - 1) : 0 +} + +domain t { + function fAlias1(Int): Int + function fAlias2(Int): Int + function fAlias3(Int): Int + function fAlias4(Int): Int + function fAlias5(Int): Int + + axiom { + //:: ExpectedOutput(typechecker.error) + forall i: Int :: f1(i) == fAlias1(i) + } + + axiom { + forall i: Int :: f2(i) == fAlias2(i) + } + + axiom { + forall i: Int :: f3(i) == fAlias3(i) + } + + axiom { + forall i: Int :: f4(i) == fAlias4(i) + } + + axiom { + //:: ExpectedOutput(typechecker.error) + forall i: Int :: f5(i) == fAlias5(i) + } +} \ No newline at end of file From 50606bb264b71122a6349a4261e0c84706002d82 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 12 Jun 2024 17:54:13 +0200 Subject: [PATCH 2/3] Fixing issue #803 --- .../viper/silver/parser/MacroExpander.scala | 61 +++++++++++++++++-- src/test/resources/all/issues/silver/0803.vpr | 30 +++++++++ 2 files changed, 86 insertions(+), 5 deletions(-) create mode 100644 src/test/resources/all/issues/silver/0803.vpr diff --git a/src/main/scala/viper/silver/parser/MacroExpander.scala b/src/main/scala/viper/silver/parser/MacroExpander.scala index 5cc216f37..f070f0097 100644 --- a/src/main/scala/viper/silver/parser/MacroExpander.scala +++ b/src/main/scala/viper/silver/parser/MacroExpander.scala @@ -7,9 +7,10 @@ package viper.silver.parser import viper.silver.ast.{FilePosition, Position, SourcePosition} -import viper.silver.ast.utility.rewriter.{ContextA, ParseTreeDuplicationError, PartialContextC, StrategyBuilder} +import viper.silver.ast.utility.rewriter.{ContextA, ParseTreeDuplicationError, PartialContextC, StrategyBuilder, Traverse} import viper.silver.verifier.{ParseError, ParseReport, ParseWarning} +import java.util import scala.collection.mutable case class MacroException(msg: String, pos: (Position, Position)) extends Exception @@ -178,9 +179,16 @@ object MacroExpander { // Store the replacements from normal variable to freshly generated variable val renamesMap = mutable.Map.empty[String, String] var scopeAtMacroCall = Set.empty[String] - val scopeOfExpandedMacros = mutable.Set.empty[String] + val scopeOfExpandedMacros = new util.IdentityHashMap[PScope, mutable.Set[String]]() + var currentMacroScope: PScope = null - def scope: Set[String] = scopeAtMacroCall ++ scopeOfExpandedMacros + def scope: Set[String] = { + if (scopeOfExpandedMacros.containsKey(currentMacroScope)) { + scopeAtMacroCall ++ scopeOfExpandedMacros.get(currentMacroScope) + } else { + scopeAtMacroCall + } + } // Handy method to get a macro from its name string def getMacroByName(name: PIdnUse): PDefine = getMacro(name) match { @@ -279,7 +287,7 @@ object MacroExpander { val freshVarName = getFreshVarName(varDecl.name) // Update scope - scopeOfExpandedMacros += freshVarName + scopeOfExpandedMacros.get(currentMacroScope) += freshVarName renamesMap += varDecl.name -> freshVarName // Create a variable with new name to substitute the previous one @@ -289,7 +297,7 @@ object MacroExpander { } else { // Update scope - scopeOfExpandedMacros += varDecl.name + scopeOfExpandedMacros.get(currentMacroScope) += varDecl.name // Return the same variable varDecl @@ -380,6 +388,49 @@ object MacroExpander { val newNode = try { scopeAtMacroCall = NameAnalyser().namesInScope(program, Some(macroCall)) + ctx.parent match { + case s: PScope => currentMacroScope = s + case n => currentMacroScope = customGetEnclosingScope(n).get + } + if (!scopeOfExpandedMacros.containsKey(currentMacroScope)) { + scopeOfExpandedMacros.put(currentMacroScope, mutable.Set.empty) + } + + // Since we're working on a parse AST that is in the process of being rewritten, some nodes don't have + // their parent node set (or they have it set incorrectly). As a result, n.getEnclosingScope may not + // work properly. Since we need this functionality, we re-implement it here using information from the + // context, in particular, the ancestors of the current node. + def customGetEnclosingScope(target: PNode): Option[PScope] = { + var foundTarget = false + for (current <- ctx.ancestorList.reverseIterator) { + if (foundTarget) { + current match { + case s: PScope => return Some(s) + case _ => + } + } else { + if (current eq target) { + foundTarget = true + } + } + } + return None + } + + def allExpandedNamesOfAllSuperScopes(s: PScope): Unit = { + if (scopeOfExpandedMacros.containsKey(s)) { + scopeOfExpandedMacros.get(currentMacroScope) ++= scopeOfExpandedMacros.get(s) + } + customGetEnclosingScope(s) match { + case Some(s) => allExpandedNamesOfAllSuperScopes(s) + case _ => + } + } + + // If scopeOfExpandedMacros contains superscopes of s, these names are also visible in the current scope, + // and we have to add them to scopeOfExpandedMacros for the current scope. + allExpandedNamesOfAllSuperScopes(currentMacroScope) + arguments.foreach(_.foreach( StrategyBuilder.SlimVisitor[PNode] { case id: PIdnDef => scopeAtMacroCall += id.name diff --git a/src/test/resources/all/issues/silver/0803.vpr b/src/test/resources/all/issues/silver/0803.vpr new file mode 100644 index 000000000..f78dabcde --- /dev/null +++ b/src/test/resources/all/issues/silver/0803.vpr @@ -0,0 +1,30 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +define m1(res) { + res := var_m2 +} + +define m2(res) { + var var_m2: Int + + var v0_1: Int + { + m1(v0_1) + } + + res := var_m2 +} + +method caller() returns (value: Int) +{ + var res: Int + { + m2(res) + } + var value2: Int + { + m2(res) + } + value := res +} \ No newline at end of file From 9ee856f05532ea20ca8ae6988660ab651a8a1a33 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 12 Jun 2024 19:44:14 +0200 Subject: [PATCH 3/3] Removed unused import --- src/main/scala/viper/silver/parser/MacroExpander.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/parser/MacroExpander.scala b/src/main/scala/viper/silver/parser/MacroExpander.scala index f070f0097..0a5bcfee9 100644 --- a/src/main/scala/viper/silver/parser/MacroExpander.scala +++ b/src/main/scala/viper/silver/parser/MacroExpander.scala @@ -7,7 +7,7 @@ package viper.silver.parser import viper.silver.ast.{FilePosition, Position, SourcePosition} -import viper.silver.ast.utility.rewriter.{ContextA, ParseTreeDuplicationError, PartialContextC, StrategyBuilder, Traverse} +import viper.silver.ast.utility.rewriter.{ContextA, ParseTreeDuplicationError, PartialContextC, StrategyBuilder} import viper.silver.verifier.{ParseError, ParseReport, ParseWarning} import java.util