spacer
spacer search


Software Model Checking Framework

Search
spacer
header
Main Menu
Home
Team
Downloads
Papers
Documentation
API
Examples
Repository
Bug Reports
Licenses
Forums
Bogor Users Map
Site Map
Contact Us
Search
Login Form





Lost Password?
 
Home arrow Documentation arrow Bogor Input Representation (BIR) arrow BIR Concrete Syntax

BIR Concrete Syntax

An EBNF concrete syntax for BIR.

Authors: Robby, Matthew Hoosier

System

[1] <system> ::= "system" <system-id> "{" <system-member>* "}"  
[2] <system-member> ::= <const> | <enum> | <record> | <extension> | <type-alias> | <global-var> | <fsm> | <virtual-table> | <fun>  

Identifier

[3] <id> ::= <basic-id> | <bogor-id>  
[4] <basic-id> ::= <letter> (<letter> | <digit>)*  
[5] <bogor-id> ::= "{|" <bogor-id-char(})>* "|}" | "(|" <bogor-id-char())>* "|)" | "<|" <bogor-id-char(>)>* "|>" | "[|" <bogor-id-char(])>* "|]" | "/|" <bogor-id-char(\\)>* "|\\" | "\\|" <bogor-id-char(/)>* "|/" | "+|" <bogor-id-char(+)>* "|+" | ".|" <bogor-id-char(.)>* "|."  
[6] <type-var-id> ::= "`" <letter> (<letter> | <digit>)*  
[7] <bogor-id-char(x)> ::= -['|', '\n', '\t', '\r'] | '|' -['x']  
[8] <letter> ::= ['\u0024', '\u0041'-'\u005a', '\u005f', '\u0061'-'\u007a', '\u00c0'-'\u00d6', '\u00d8'-'\u00f6', '\u00f8'-'\u00ff', '\u0100'-'\u1fff', '\u3040'-'\u318f', '\u3300'-'\u337f', '\u3400'-'\u3d2d', '\u4e00'-'\u9fff', '\uf900'-'\ufaff']  
[9] <letter> ::= ['\u0030'-'\u0039', '\u0660'-'\u0669', '\u06f0'-'\u06f9', '\u0966'-'\u096f', '\u09e6'-'\u09ef', '\u0a66'-'\u0a6f', '\u0ae6'-'\u0aef', '\u0b66'-'\u0b6f', '\u0be7'-'\u0bef', '\u0c66'-'\u0c6f', '\u0ce6'-'\u0cef', '\u0d66'-'\u0d6f', '\u0e50'-'\u0e59', '\u0ed0'-'\u0ed9', '\u1040'-'\u1049']  

Type

[10] <type> ::= <basic-type> | <fun-type> | <generic-type>  
[11] <basic-type> ::= <prim-type> | <non-prim-type> | <alias-type>  
[12] <prim-type> ::= <boolean-type> | <integral-type> | <real-type> | <enum-type> | <thread-id-type> | <prim-ext-type>  
[13] <boolean-type> ::= "boolean"  
[14] <integral-type> ::= "int" <int-range>? | "long" <long-range>?  
[15] <int-range> ::= "wrap"? "(" <int-val> , <int-val> ")"  
[16] <int-val> ::= ("-" |"+")? <int-lit> | <const-id> "." <const-elem-id>  
[17] <long-range> ::= "wrap"? "(" <long-val> , <long-val> ")"  
[18] <long-val> ::= ("-" |"+")? (<int-lit> | <long-lit>) | <const-id> "." <const-elem-id>  
[19] <real-type> ::= "float" | "double"  
[20] <enum-type> ::= <enum-id>  
[21] <thread-id-type> ::= "tid"  
[22] <prim-ext-type> ::= <ext-id> "." <prim-ext-id> <type-args>?  
[23] <type-args> ::= "<" <basic-type> ("," <basic-type>)* ">"  
[24] <non-prim-type> ::= <record-type> | <array-type> | <string-type> | <lock-type> | <non-prim-ext-type>  
[25] <record-type> ::= <record-id>  
[26] <array-type> ::= <basic-type> "[" "]"  
[27] <string-type> ::= "string"  
[28] <lock-type> ::= "lock"  
[29] <non-prim-ext-type> ::= <ext-id> "." <non-prim-ext-id> <type-args>?  
[30] <alias-type> ::= <type-alias-id>  
[31] <fun-type> ::= ("unit" | <fun-type-args>) "->" <fun-type-arg>  
[32] <fun-type-args> ::= <fun-type-arg> ("*" <fun-type-arg>)*  
[33] <fun-type-arg> ::= <basic-type> | <generic-type>  
[34] <generic-type> ::= <ext-id> "." <prim-ext-type-id> <gen-type-args>? | <ext-id> "." <non-prim-ext-type-id> <gen-type-args>? | <generic-type> "[" "]"  
[35] <gen-type-args> ::= <gen-type-arg> ("*" <gen-type-arg>)*  
[36] <gen-type-arg> ::= <basic-type> | <generic-type> | <type-var-id>  

Literal

[37] <lit> ::= <boolean-lit> | <char-lit> | (("+" | "-")? <int-lit> | <real-lit>) | <string-lit> | <null-lit>  
[38] <boolean-lit> ::= "true" | "false"  
[39] <char-lit> ::= "'" <char> "'"  
[40] <int-lit> ::= <dec> | <oct> | <hex>  
[41] <long-lit> ::= (<dec> | <oct> | <hex>) ['l', 'L']  
[42] <real-lit> ::= <float-lit> | <double-lit>  
[43] <float-lit> ::= <dec-digit>+ '.' <dec-digit>* <exponent>? ['f', 'F'] | '.' <dec-digit>+ <exponent>? ['f', 'F'] | <dec-digit>+ <exponent>? ['f', 'F'] | "NaNf" | "pINFf" | "nINFf"  
[44] <double-lit> ::= <dec-digit>+ '.' <dec-digit>* <exponent>? ['d', 'D']? | '.' <dec-digit>+ <exponent>? ['d', 'D']? | <dec-digit>+ <exponent>? ['d', 'D']? | "NaNd" | "pINFd" | "nINFd"  
[45] <string-lit> ::= '"' <char>* '"'  
[46] <null-lit> ::= "null"  
[47] <char> ::= -[''','\\', '\n','\r'] | ('\\' (['n','t','b','r','f', '\\',''','"'] | <oct-digit> <oct-digit>? | <zero-three-digit> <oct-digit> <oct-digit>))  
[48] <dec> ::= <one-nine-digit><dec-digit>  
[49] <oct> ::= '0' <oct-digit>*  
[50] <hex> ::= '0' ('x' | 'X') <hex-digit>+  
[51] <oct-digit> ::= ['0'-'7']  
[52] <zero-three-digit> ::= ['0'-'3']  
[53] <dec-digit> ::= ['0'-'9']  
[54] <one-nine-digit> ::= ['1'-'9']  
[55] <hex-digit> ::= ['1'-'9', 'a'-'f', 'A'-'F']  
[56] <exponent> ::= ['e','E'] ['+','-']? <dec-digit>+  

Constant

[57] <const> ::= "const" <const-id> "{" (<const-elem-id> "=" <const-cast>? <lit> ";")* "}"  
[58] <const-cast> ::= "(" <basic-type> ")"  

Enum

[59] <enum> ::= "enum" <enum-id> "{" <enum-elems> "}"  
[60] <enum-elems> ::= <enum-elem-id> ("," <enum-elem-id>)*  

Record

[61] <record> ::= "top"? "throwable"? "record" <record-id> <super>? "{" <record-field>* "}"  
[62] <super> ::= "extends" <record-id> ("," <record-id>)*  
[63] <record-field> ::= <basic-type> <record-field-id> ";"  

Extension

[64] <extension> ::= "extension" <ext-id> <ext-impl> "{" <ext-def>* "}"  
[65] <ext-impl> ::= "for" <java-class-name>  
[66] <java-class-name> ::= <basic-id> ("." <basic-id>)*  
[67] <ext-def> ::= <ext-type-def> | <ext-exp-def> | <ext-action-def>  
[68] <ext-type-def> ::= "ptypedef" <prim-ext-type-id> <type-params>? ";" | "typedef" <non-prim-ext-type-id> <type-params>? ";"  
[69] <type-params> ::= "<" <type-var-id> ("," <type-var-id>)* ">"  
[70] <ext-exp-def> ::= "expdef" <ext-ret-type> <ext-exp-id> <type-params>? "(" <ext-params>? ")" ";"  
[71] <ext-ret-type> ::= <basic-type> | <generic-type> | <type-var-id>  
[72] <ext-exp-id> ::= <basic-id>  
[73] <ext-params> ::= <ext-param-type> <param-id>? ("," <ext-param-type> <param-id>?)* ("," <ext-param-type> "...")? | <ext-param-type> "..."  
[74] <ext-param-type> ::= "lazy"? (<basic-type> | <generic-type> | <type-var-id>) | <fun-type>  
[75] <ext-action-def> ::= "actiondef" <ext-action-id> <type-params>? "(" <ext-params>? ")" ";"  
[76] <ext-action-id> ::= <basic-id>  

Type Alias

[77] <type-alias> ::= "typealias" <type-alias-id> <basic-type> ";"  

Global Variable

[78] <global-var> ::= "transient"? <basic-type> <global-var-id> <global-var-init>? ";"  
[79] <global-var-init> ::= ":=" <global-var-init-cast>? <lit>  
[80] <global-var-init-cast> ::= "(" <basic-type> ")"  

Thread and Function

[81] <fsm> ::= <thread> | <function>  
[82] <thread> ::= ("active" ("[" <num-active> "]")?)? "thread" <thread-id> "(" <params>? ")" "{" <local-var>* (<low-level-body> | <high-level-body>) "}"  
[83] <num-active> ::= <int-lit> | <const-id> "." <const-elem-positive-int-id>  
[84] <function> ::= "function" <thread-id> "(" <params>? ")" ("returns" <basic-type>)? "{" <local-var>* (<low-level-body> | <high-level-body>) "}"  
[85] <params> ::= <basic-type> <local-id> ("," <basic-type> <local-id>)*  
[86] <local-var> ::= "transient"? <basic-type> <local-id> <local-var-init>? ";"  
[87] <local-var-init> ::= ":=" <local-var-init-cast>? <lit>  
[88] <local-var-init-cast> ::= "(" <basic-type> ")"  

Low-level Thread and Function Body

[89] <low-level-body> ::= <location>+ <catch>*  
[90] <location> ::= "loc" <loc-id> ":" <live-set>? <transformation>+  
[91] <live-set> ::= "live" "{" ( <local-id> ("," <local-id>)*)? "}"  
[92] <transformation> ::= <guard>? "do" <visibility>? "{" <action>* "}" <jump> ";" | <guard>? (<local-id> ":=")? <visibility>? "invoke" ("virtual"? <virtual-or-function-id> | "reflect") "(" <args>* ")" <jump> ";"  
[93] <guard> ::= "when" <exp>  
[94] <visibility> ::= "visible" | "invisible"  
[95] <args> ::= <exp> ("," <exp>)*  
[96] <jump> ::= "goto" <loc-id> | "return" <local-id>?  
[97] <catch> ::= "catch" <record-id> <local-id> "at" <loc-id> ("," <loc-id>)* <jump> ";"  

High-level Thread and Function Body

[98] <high-level-body> ::= <statement>+  
[99] <statement> ::= <atomic-statement> | <while-statement> | <if-statement> | <choose-statement> | <try-statement> | <return-statement> | <action-statement> | <atomic-action-statement> | <skip-statement>  
[100] <atomic-statement> ::= "atomic" <statement>+ "end"  
[101] <while-statement> ::= "while" <exp> "do" <statement>+ "end"  
[102] <if-statement> ::= "if" <exp> "do" <statement>+ ("elseif" <exp> "do" <statement>+)* ("else" "do" <statement>+)? "end"  
[103] <choose-statement> ::= "choose" (("when" "<" <exp> ">")? "do" <statement>+)+ ("else" "do" <statement>+)? "end"  
[104] <try-statement> ::= "try" <statement>+ ("catch" "(" <throwable-record-id> <local-var-id> ")" <statement>+)+ "end"  
[105] <return-statement> ::= "return" <exp>? ";"  
[106] <action-statement> ::= <action>  
[107] <atomic-action-statement> ::= "<" <action> ">"  
[108] <skip-statement> ::= "skip" ";"  

Viurtual Table

[109] <virtual-table> ::= "virtual" <vtable-id> <vtable-on-enum>? "{" <vtable-entry>+ "}"  
[110] <vtable-on-enum> ::= "on" <enum-id>  
[111] <vtable-entry> ::= <record-or-enum-id> "->" <function-id>  

Functional Expression (fun)

[112] <fun> ::= "fun" <fun-id> "(" <fun-params>? ")" "returns" <basic-type> "=" <exp> ";"  
[113] <fun-params> ::= <basic-type> <fun-local-id> ("," <basic-type> <fun-local-id>)*  

Expression

[114] <exp> ::= <lit-exp> | <var-exp> | <unary-exp> | <binary-exp> | <cond-exp> | <paren-exp> | <atomic-exp> | <new-exp> | <field-exp> | <array-exp> | <cast-exp> | <kindof-exp> | <instanceof-exp> | <lock-test-exp> | <thread-test-exp> | <let-exp> | <apply-exp> | <ext-exp>  
[115] <lit-exp> ::= <lit>  
[116] <var-exp> ::= <local-id> | <global-id> | <let-local-id> | <fun-id>  
[117] <unary-exp> ::= <unary-op><exp>  
[118] <unary-op> ::= "+" | "-" | "!"  
[119] <binary-exp> ::= <exp><binary-op><exp>  
[120] <binary-op> ::= "+" | "-" | "*" | "/" | "%" | "shl" | "shr" | "ushr" | "==" | "!=" | ">" | ">=" | "<" | "<=" | | "&&" | "||" | "=>" | "&" | "|" | "^"  
[121] <cond-exp> ::= <exp> "?" <exp> ":" <exp>  
[122] <paren-exp> ::= "(" <exp> ")"  
[123] <atomic-exp> ::= "<" <exp> ">"  
[124] <new-exp> ::= "new" <record-type> | "new" <lock-type> | "new" <record-type> ("[" <exp> "]")+ ("[" "]")*  
[125] <field-exp> ::= <exp> "." ( <record-field-id> | <array-length-id> ) | <const-id> <const-elem-id> | <enum-id> <enum-elem-id>  
[126] <array-exp> ::= <exp> "[" <exp> "]"  
[127] <cast-exp> ::= "(" <basic-type> ")" <exp>  
[128] <kindof-exp> ::= <exp> "kindof" <basic-type>  
[129] <instanceof-exp> ::= <exp> "instanceof" <basic-type>  
[130] <lock-test-exp> ::= <lock-test-op> "(" <exp> ")"  
[131] <lock-test-op> ::= "lockAvailable" | "hasLock" | "wasNotified"  
[132] <thread-test-exp> ::= <thread-test-op> "(" <exp> ")"  
[133] <thread-test-op> ::= "threadTerminated"  
[134] <let-exp> ::= "let" <name-binding>+ "in" <exp>  
[135] <name-binding> ::= <basic-type> <let-local-id> "=" <exp>  
[136] <apply-exp> ::= <fun-id> "(" <args>? ")"  
[137] <ext-exp> ::= <ext-id> "." <ext-exp-or-action-id> <type-args>? "(" <args>? ")"  

Action

[138] <action> ::= <assign-action> | <assert-action> | <assume-action> | <lock-op-action> | <throw-action> | <start-action> | <exit-action> | <ext-action>  
[139] <assign-action> ::= <lhs> ":=" <exp> ";"  
[140] <lhs> ::= <var-exp> | <field-exp> | <array-exp>  
[141] <assert-action> ::= "assert" "(" <exp> ")" ";"  
[142] <assume-action> ::= "assume" "(" <exp> ")" ";"  
[143] <lock-op-action> ::= <lock-op> "(" <exp> ")" ";"  
[144] <throw-action> ::= "throw" <exp> ";"  
[145] <lock-op> ::= "lock" | "unlock" | "wait" | "unwait" | "notify" | "notifyAll"  
[146] <start-action> ::= (<lhs> ":=")? "start" <thread-id> "(" <args>? ")" ";"  
[147] <exit-action> ::= "exit" ";"  
[148] <ext-action> ::= <ext-id> "." <ext-action-id> <type-args> "(" <args>? ")" ";"  
 
< Prev
[ Back ]
spacer
Popular
Newsflash

 
(c) SAnToS Laboratory, Kansas State University, 2002-2006
spacer