Merge pull request #33 from Certora/semicolon_detection

CERT-5435 semicolon detection

Author: pickx

CHANGELOG.md

@@ -1,4 +1,8 @@
 # Changelog
+## [2.0.2] - 2024-03-13
+### Fixed
+- Semicolon not detected at the end of a `definition` statement.
+
 ## [2.0.1] - 2024-03-06
 ### Added
 - Now compiling to `linux-aarch64` aka ARM on Linux

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "cvldoc_parser_core"
-version = "2.0.1"
+version = "2.0.2"
 edition = "2021"
 
 [dependencies]

src/parse.rs

@@ -135,8 +135,8 @@ fn decl_parser() -> impl Parser<Token, Intermediate, Error = Simple<Token>> {
         let rhs = none_of(Token::Semicolon)
             .repeated()
             .at_least(1)
-            .then_ignore(just(Token::Semicolon))
-            .map_with_span(|_, span| span);
+            .map_with_span(|_, span| span)
+            .then_ignore(just(Token::Semicolon));
 
         just(Token::Definition)
             .ignore_then(ident())

src/parse/lexer.rs

@@ -48,6 +48,8 @@ pub fn cvl_lexer() -> impl Parser<char, Vec<(Token, Span)>, Error = Simple<char>
             ';' => Token::Semicolon,
             '=' => Token::Equals,
             '!' => Token::Excl,
+            '+' => Token::Plus,
+            '/' => Token::Slash,
         };
         let arrow = just("=>").to(Token::Arrow);
 

src/parse/tests/cvl2.rs

@@ -1,3 +1,5 @@
+use crate::parse::{cvl_parser, decl_parser};
+
 use super::*;
 use indoc::formatdoc;
 use itertools::Itertools;
@@ -573,3 +575,37 @@ fn persistent_ghosts() {
     check_ghost(&parsed[0], "pers", true);
     check_ghost(&parsed[1], "non_pers", false);
 }
+
+#[test]
+/// this shouldn't trip up the definition end detection:
+/// the semicolon should be detected even if it's not whitespace-separated from the previous token.
+fn definition_does_not_stop() {
+    let src = indoc! {"
+        methods {
+            function x() external returns uint envfree;
+            function i() external returns int envfree;
+        }
+        
+        // myInvariant: run0 pass run1 fail
+        
+        definition addBv(uint x, uint y) returns mathint = x+y;
+        
+        /**
+         * My amazing invariant (should be @title)
+         * @notice it is very amazing. Please notice
+         */
+        invariant myInvariant() addBv(x(),1) <= max_uint256 {
+            preserved setX(uint y) with (env e) {
+                require y < 1000;
+            }
+        }
+    "};
+
+    let parsed = Builder::new(src).build().unwrap();
+
+    assert_eq!(parsed.len(), 3);
+
+    assert_matches!(&parsed[0].ast, Ast::Methods { .. });
+    assert_matches!(&parsed[1].ast, Ast::Definition { definition, ..} if definition == "x+y");
+    assert_matches!(&parsed[2].ast, Ast::Invariant { .. });
+}

src/parse/types.rs

@@ -35,6 +35,8 @@ pub enum Token {
     Semicolon,
     Equals,
     Excl,
+    Plus,
+    Slash,
     Arrow,
     Axiom,
     Using,
@@ -86,6 +88,8 @@ impl Display for Token {
             Token::Semicolon => write!(f, ";"),
             Token::Equals => write!(f, "="),
             Token::Excl => write!(f, "!"),
+            Token::Plus => write!(f, "+"),
+            Token::Slash => write!(f, "/"),
             Token::Arrow => write!(f, "=>"),
             Token::Axiom => write!(f, "axiom"),
             Token::Using => write!(f, "using"),

src/python_wrapper/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "cvldoc_parser_py"
-version = "2.0.1"
+version = "2.0.2"
 edition = "2021"
 
 [lib]

src/python_wrapper/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "maturin"
 
 [project]
 name = "cvldoc_parser"
-version = "2.0.1"
+version = "2.0.2"
 requires-python = ">=3.9"
 classifiers = [
     "Programming Language :: Rust",