From 8f2fa05a504c28a823725ac817241cf17a2c6329 Mon Sep 17 00:00:00 2001 From: Johannes Gasser Date: Mon, 15 Jul 2024 15:28:29 +0200 Subject: [PATCH] add test, fix positioning & block placement --- src/main/scala/viper/silver/parser/ParseAst.scala | 2 +- .../standard/reasoning/ReasoningPASTExtension.scala | 6 +++--- .../plugin/standard/reasoning/ReasoningPlugin.scala | 4 ++-- .../reasoning/universal_introduction/ui_func.vpr | 11 +++++++++++ 4 files changed, 17 insertions(+), 6 deletions(-) diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala index 539a80fa8..614548a5e 100644 --- a/src/main/scala/viper/silver/parser/ParseAst.scala +++ b/src/main/scala/viper/silver/parser/ParseAst.scala @@ -1467,7 +1467,7 @@ case class PNewExp(keyword: PKw.New, fields: PGrouped.Paren[Either[PSym.Star, PD def forceSubstitution(ts: PTypeSubstitution) = {} } -sealed trait PScope extends PNode { +trait PScope extends PNode { val scopeId = PScope.uniqueId() } diff --git a/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPASTExtension.scala index ae82d4df4..063f5a2e3 100644 --- a/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPASTExtension.scala @@ -9,7 +9,7 @@ package viper.silver.plugin.standard.reasoning import viper.silver.FastMessaging import viper.silver.ast.{Exp, ExtensionExp, LocalVar, LocalVarDecl, Position, Seqn, Stmt, Trigger} import viper.silver.parser.TypeHelper.Bool -import viper.silver.parser.{NameAnalyser, PAssignTarget, PCall, PCallable, PDelimited, PExp, PExtender, PGrouped, PIdnRef, PIdnUseExp, PKeywordLang, PKeywordStmt, PKw, PLabel, PLocalVarDecl, PReserved, PSeqn, PStmt, PSym, PSymOp, PTrigger, PType, PTypeSubstitution, Translator, TypeChecker} +import viper.silver.parser.{NameAnalyser, PAssignTarget, PCall, PCallable, PDelimited, PExp, PExtender, PGrouped, PIdnRef, PIdnUseExp, PKeywordLang, PKeywordStmt, PKw, PLabel, PLocalVarDecl, PReserved, PScope, PSeqn, PStmt, PSym, PSymOp, PTrigger, PType, PTypeSubstitution, Translator, TypeChecker} case object PObtainKeyword extends PKw("obtain") with PKeywordLang with PKeywordStmt case object PWhereKeyword extends PKw("where") with PKeywordLang @@ -42,7 +42,7 @@ case class PExistentialElim(obtainKw: PReserved[PObtainKeyword.type], delimitedV } } -case class PUniversalIntro(proveKw: PReserved[PProveKeyword.type], forallKw: PKw.Forall, delimitedVarDecls: PDelimited[PLocalVarDecl, PSym.Comma], triggers: Seq[PTrigger], assumingKw: PReserved[PAssumingKeyword.type], e1: PExp, impliesKw: PReserved[PImpliesKeyword.type], e2: PExp, block: PSeqn)(val pos: (Position, Position)) extends PExtender with PStmt { +case class PUniversalIntro(proveKw: PReserved[PProveKeyword.type], forallKw: PKw.Forall, delimitedVarDecls: PDelimited[PLocalVarDecl, PSym.Comma], triggers: Seq[PTrigger], assumingKw: PReserved[PAssumingKeyword.type], e1: PExp, impliesKw: PReserved[PImpliesKeyword.type], e2: PExp, block: PSeqn)(val pos: (Position, Position)) extends PExtender with PStmt with PScope { lazy val varDecls: Seq[PLocalVarDecl] = delimitedVarDecls.toSeq override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { @@ -60,7 +60,7 @@ case class PUniversalIntro(proveKw: PReserved[PProveKeyword.type], forallKw: PKw triggers.map { t1 => Trigger(t1.exp.inner.toSeq.map { t2 => t.exp(t2) })(t.liftPos(t1)) }, t.exp(e1), t.exp(e2), - t.stmt(block).asInstanceOf[Seqn])(t.liftPos(e1)) + t.stmt(block).asInstanceOf[Seqn])(t.liftPos(block)) } } diff --git a/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPlugin.scala b/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPlugin.scala index 9e19a3bc6..ef5114531 100644 --- a/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPlugin.scala @@ -237,7 +237,7 @@ class ReasoningPlugin(@unused reporter: viper.silver.reporter.Reporter, Seq(Inhale(u.assumingExp)(u.assumingExp.pos)), Seq.empty)(u.assumingExp.pos), Seqn(Seq.empty, Seq.empty)(u.assumingExp.pos) - )(u.assumingExp.pos), + )(u.pos), // execute block u.block, // conditionally assert imply expression @@ -245,7 +245,7 @@ class ReasoningPlugin(@unused reporter: viper.silver.reporter.Reporter, Inhale(Forall(quantifiedVars, newTrigs, Implies(LabelledOld(newExp1, lbl)(u.implyingExp.pos), newExp2)(u.implyingExp.pos))(u.implyingExp.pos))(u.implyingExp.pos) ), Seq(boolvar) ++ u.varList - )(u.assumingExp.pos) + )(u.pos) } override def beforeVerify(input: Program): Program = { diff --git a/src/test/resources/reasoning/universal_introduction/ui_func.vpr b/src/test/resources/reasoning/universal_introduction/ui_func.vpr index 33cd76512..58ae73f0f 100644 --- a/src/test/resources/reasoning/universal_introduction/ui_func.vpr +++ b/src/test/resources/reasoning/universal_introduction/ui_func.vpr @@ -32,3 +32,14 @@ method mFunctionNOK() y := func1(x) } } + +function func2(e: Ref): Ref { + e +} + +method mFunction2NOK() { + var x: Ref + prove forall i:Ref assuming true implies i == x { + x := test(i) + } +} \ No newline at end of file