correct parsing rules for loop invariants (#214)

pontem-network · Oct 22, 2024 · 373aba6 · 373aba6
1 parent 2db094c
commit 373aba6
Show file tree

Hide file tree

Showing 13 changed files with 448 additions and 14 deletions.
diff --git a/src/main/grammars/MoveParser.bnf b/src/main/grammars/MoveParser.bnf
@@ -868,7 +868,8 @@ LetMslStmt ::= (let post?) Pat TypeAscription? Initializer? ';'
 }
 
 ExprStmt ::= (ExprStmt_expr !('}')) ';' { pin = 1 }
-private ExprStmt_expr ::= ItemSpecBlockExpr | Expr
+private ExprStmt_expr ::= Expr
+//private ExprStmt_expr ::= ItemSpecBlockExpr | Expr
 {
     recoverWhile = "ExprStmt_recover"
 }
@@ -973,6 +974,7 @@ private AtomExpr ::=
 //                    | RefExpr
                     | LambdaExpr
                     | LitExpr
+                    | SpecBlockExpr
                     | CodeBlockExpr
 
 
@@ -1182,15 +1184,15 @@ LoopExpr ::= loop AnyBlock {
     pin = 1
     implements = [ "org.move.lang.core.psi.MvLoopLike" ]
 }
-WhileExpr ::= while Condition AnyBlock {
+WhileExpr ::= while Condition AnyBlock SpecBlockExpr? {
     pin = 1
     implements = [ "org.move.lang.core.psi.MvLoopLike" ]
 }
 ForExpr ::= for ForIterCondition AnyBlock {
     pin = 1
     implements = [ "org.move.lang.core.psi.MvLoopLike" ]
 }
-ForIterCondition ::= '(' PatBinding in Expr ')' {
+ForIterCondition ::= '(' PatBinding in Expr SpecBlockExpr? ')' {
     pin = 1
 }
 
@@ -1462,11 +1464,12 @@ Schema ::= Attr* (spec schema) IDENTIFIER TypeParameterList? <<msl SpecCodeBlock
     hooks = [ leftBinder = "ADJACENT_LINE_COMMENTS" ]
 }
 
-ItemSpecBlockExpr ::= spec <<msl SpecCodeBlock>> {
+SpecBlockExpr ::= spec <<msl SpecCodeBlock>> {
     implements = [
         "org.move.lang.core.psi.ScopeMslOnlyElement"
     ]
 }
+ItemSpecBlockExpr ::= spec <<msl SpecCodeBlock>>
 
 SpecCodeBlock ::= '{' ItemSpecBlock_items '}'
 {

diff --git a/src/main/kotlin/org/move/ide/MvBreadcrumbsProvider.kt b/src/main/kotlin/org/move/ide/MvBreadcrumbsProvider.kt
@@ -5,6 +5,7 @@ import com.intellij.psi.PsiElement
 import com.intellij.ui.breadcrumbs.BreadcrumbsProvider
 import org.move.lang.MoveLanguage
 import org.move.lang.core.psi.*
+import org.move.lang.core.psi.ext.expr
 
 class MvBreadcrumbsProvider : BreadcrumbsProvider {
 

diff --git a/src/main/kotlin/org/move/lang/core/psi/ext/MvForLoopExpr.kt b/src/main/kotlin/org/move/lang/core/psi/ext/MvForLoopExpr.kt
@@ -0,0 +1,7 @@
+package org.move.lang.core.psi.ext
+
+import org.move.lang.core.psi.MvExpr
+import org.move.lang.core.psi.MvForIterCondition
+
+val MvForIterCondition.expr: MvExpr? get() = exprList.firstOrNull()
+val MvForIterCondition.specExpr: MvExpr? get() = exprList.drop(1).firstOrNull()
diff --git a/src/main/kotlin/org/move/lang/core/psi/ext/MvItemSpec.kt b/src/main/kotlin/org/move/lang/core/psi/ext/MvItemSpec.kt
@@ -32,7 +32,7 @@ fun MvModuleItemSpec.specInlineFunctions(): List<MvSpecInlineFunction> =
         .orEmpty()
 
 val MvItemSpec.itemSpecBlock: MvSpecCodeBlock? get() = this.childOfType()
-val MvItemSpecBlockExpr.specBlock: MvSpecCodeBlock? get() = this.childOfType()
+val MvSpecBlockExpr.specBlock: MvSpecCodeBlock? get() = this.childOfType()
 
 abstract class MvItemSpecMixin(node: ASTNode): MvElementImpl(node),
                                                MvItemSpec {

diff --git a/src/main/kotlin/org/move/lang/core/types/infer/InferenceContext.kt b/src/main/kotlin/org/move/lang/core/types/infer/InferenceContext.kt
@@ -236,10 +236,10 @@ class InferenceContext(
         when (owner) {
             is MvFunctionLike -> owner.anyBlock?.let { inference.inferFnBody(it) }
             is MvItemSpec -> {
-                owner.itemSpecBlock?.let { inference.inferSpec(it) }
+                owner.itemSpecBlock?.let { inference.inferSpecBlock(it) }
             }
-            is MvModuleItemSpec -> owner.itemSpecBlock?.let { inference.inferSpec(it) }
-            is MvSchema -> owner.specBlock?.let { inference.inferSpec(it) }
+            is MvModuleItemSpec -> owner.itemSpecBlock?.let { inference.inferSpecBlock(it) }
+            is MvSchema -> owner.specBlock?.let { inference.inferSpecBlock(it) }
         }
 
         fallbackUnresolvedTypeVarsIfPossible()

diff --git a/src/main/kotlin/org/move/lang/core/types/infer/TypeInferenceWalker.kt b/src/main/kotlin/org/move/lang/core/types/infer/TypeInferenceWalker.kt
@@ -79,7 +79,7 @@ class TypeInferenceWalker(
     }
 
     fun inferFnBody(block: AnyBlock): Ty = block.inferBlockCoercableTo(returnTy)
-    fun inferSpec(block: AnyBlock): Ty =
+    fun inferSpecBlock(block: AnyBlock): Ty =
         mslScope { block.inferBlockType(NoExpectation) }
 
     private fun AnyBlock.inferBlockCoercableTo(expectedTy: Ty): Ty {
@@ -240,7 +240,7 @@ class TypeInferenceWalker(
             is MvMoveExpr -> expr.expr?.inferType() ?: TyUnknown
             is MvCopyExpr -> expr.expr?.inferType() ?: TyUnknown
 
-            is MvItemSpecBlockExpr -> expr.specBlock?.let { inferSpec(it) } ?: TyUnknown
+            is MvSpecBlockExpr -> inferSpecBlockExprTy(expr)
 
             is MvCastExpr -> {
                 expr.expr.inferType()
@@ -640,6 +640,14 @@ class TypeInferenceWalker(
         return TyUnit
     }
 
+    private fun inferSpecBlockExprTy(specBlockExpr: MvSpecBlockExpr): Ty {
+        val specBlock = specBlockExpr.specBlock
+        if (specBlock != null) {
+            inferSpecBlock(specBlock)
+        }
+        return TyUnit
+    }
+
     /**
      * Unifies the output type with the expected type early, for more coercions
      * and forward type information on the input expressions

diff --git a/src/test/kotlin/org/move/lang/parser/CompleteParsingTest.kt b/src/test/kotlin/org/move/lang/parser/CompleteParsingTest.kt
@@ -56,6 +56,8 @@ class CompleteParsingTest: MvParsingTestCase("complete") {
     fun `test is expr`() = doTest()
     fun `test dot dot pattern`() = doTest()
 
+    fun `test loop invariants`() = doTest()
+
     // feature declaration is required here, as it's a parser-level feature
 //    @ResourceAccessControl()
 //    fun `test access control`() = doTest()

diff --git a/src/test/kotlin/org/move/lang/types/ExpressionTypesTest.kt b/src/test/kotlin/org/move/lang/types/ExpressionTypesTest.kt
@@ -2156,4 +2156,13 @@ module 0x1::main {
             }
         }        
     """)
+
+    fun `test spec block type`() = testExpr("""
+        module 0x1::m {
+            fun main() {
+                spec {}
+                //^ ()
+            }
+        }        
+    """)
 }
diff --git a/src/test/resources/org/move/lang/parser/complete/index_expr.txt b/src/test/resources/org/move/lang/parser/complete/index_expr.txt
@@ -536,7 +536,7 @@ FILE
           PsiElement(;)(';')
         PsiWhiteSpace('\n        ')
         MvExprStmtImpl(EXPR_STMT)
-          MvItemSpecBlockExprImpl(ITEM_SPEC_BLOCK_EXPR)
+          MvSpecBlockExprImpl(SPEC_BLOCK_EXPR)
             PsiElement(spec)('spec')
             PsiWhiteSpace(' ')
             MvSpecCodeBlockImpl(SPEC_CODE_BLOCK)

diff --git a/src/test/resources/org/move/lang/parser/complete/loop_invariants.move b/src/test/resources/org/move/lang/parser/complete/loop_invariants.move
@@ -0,0 +1,25 @@
+module 0x1::loop_invariants {
+    fun main() {
+        while (true) {} spec { assert true };
+        while (true) 1 + 1 spec { assert true };
+        // loop invariant is written in a spec block inside the loop condition
+        while ({spec {assert x < 42;}; n < 64}) {
+            spec {
+                assert x > 42;
+                assert 0 < x;
+            };
+            n = n + 1
+        };
+
+        // the following should parse successfully but fail typing
+        spec {} + 1;
+        spec {} && spec {};
+        &mut spec {};
+        (spec {}: ());
+
+        for (i in 1..10 spec { assert true }) {};
+        for (i in 0..1 spec {invariant y > 0;}) {
+            y = y + 1;
+        };
+    }
+}