added promela frontend project

settings.gradle.kts

@@ -22,6 +22,7 @@ include(
     "common/grammar",
 
     "frontends/c-frontend",
+    "frontends/promela-frontend",
     "frontends/chc-frontend",
     "frontends/llvm",
 

subprojects/frontends/promela-frontend/README.md

@@ -0,0 +1,3 @@
+# ANTLR-Based Promela Frontend for Verification
+
+This subproject adds an ANTLR-grammar based Promela frontend to Theta. This is independent of any formalism, and aims to be as widely applicable as possible.

subprojects/frontends/promela-frontend/build.gradle.kts

@@ -0,0 +1,24 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+plugins {
+    id("kotlin-common")
+    id("antlr-grammar")
+}
+dependencies {
+    implementation(project(":theta-core"))
+    implementation(project(":theta-common"))
+    implementation(project(":theta-grammar"))
+}

subprojects/frontends/promela-frontend/src/main/antlr/promela.g4

@@ -0,0 +1,69 @@
+grammar promela;
+
+spec : module+ EOF;
+module : proctype | init | mtype | decl_lst;
+separator : ';' | '->';
+
+proctype: ('active' ('[' constant ']')?)? 'proctype' name '(' (decl_lst)? ')' '{' sequence* '}';
+init: 'init' '{' sequence* '}';
+mtype : 'mtype' ('=' )? '{' name (',' name)* '}' (';')?;
+decl_lst : one_decl (';' one_decl)* (';')?;
+one_decl: typeID ivar (',' ivar)*;
+typeID: 'boolean' | 'int' | 'mtype' | 'chan' | 'short' | 'byte' | 'bit' | 'pid';
+
+sequence: step (separator step)* (';')?;
+step : one_decl | stmnt;
+ivar: name ('[' any_expr ']')? ('=' any_expr | '=' ch_init)?;
+
+ch_init : '[' any_expr ']' 'of' '{' typeID (',' typeID)* '}';
+varref : name ('[' any_expr ']')? ('.' name)?;
+
+send_args: arg_lst | any_expr '(' (arg_lst)? ')';
+receive : varref '?' recv_args;
+arg_lst : any_expr (',' any_expr)*;
+assignx: varref ('=' any_expr | '++' | '--' | '!' send_args | '?' recv_args);
+
+stmnt
+    : 'if' ifoption 'fi'
+    | 'do' dooption 'od'
+    | 'atomic' '{' sequence '}'
+    | '{' sequence '}'
+    | assignx
+    | 'printf' '(' '"' name '"' ')'
+    | 'goto' name
+    | 'skip'
+    | 'break'
+    | name ':' stmnt
+    | 'run' name '(' (arg_lst)? ')'
+    | 'assert' any_expr;
+
+recv_args: recv_arg (',' recv_arg)* | recv_arg '(' recv_args ')';
+recv_arg: varref | 'eval' '(' varref ')' | ('-'?) constant;
+
+dooption : ':' ':' (guard '->')? sequence (':' ':' (guard '->')? sequence)*;
+ifoption: ':' ':' (guard '->')? sequence (':' ':' (guard '->')? sequence);
+guard: any_expr | receive | 'else';
+
+binarop: '+' | '-' | '*' | '/' | '>' ('=')? | '<' ('=')? | '==' | '!=' | '&' ('&')? | MOD | '^' | '||';
+unarop: '~' | '-' | '!';
+
+any_expr: '(' any_expr ('->' any_expr ':' any_expr)? ')' (binarop any_expr)?
+    | unarop any_expr (binarop any_expr)?
+    | 'len' '(' varref ')' (binarop any_expr)?
+    | varref ('?' '[' recv_args ']')? (binarop any_expr)?
+    | constant (binarop any_expr)?
+    | 'timeout' (binarop any_expr)?
+    | chanpoll (binarop any_expr)?;
+
+chanpoll: 'full' '(' varref ')'
+    | 'empty' '(' varref ')'
+    | 'nfull' '(' varref ')'
+    | 'nempty' '(' varref ')' ;
+name: ID (ID | NUMBER)*;
+
+WS : (' '|'\t'|'\n'|'\r')+ {skip();} ;
+ID : ('a'..'z' |'A'..'Z' |'_' )+ ;
+NUMBER : '0'..'9'+;
+MOD : '%';
+
+constant : 'true' | 'false' | 'skip' | NUMBER;