class BoogieLanguage
prechigh left 'forall' 'exists' left 'old' nonassoc '[' ']' nonassoc '!' left '*' '/' '%' left '+' '-' left '++' left '==' '!=' '<' '>' '<=' '>=' '<:' left '&&' left '||' left '==>' left '<==>' left 'if' 'then' 'else' left ':' nonassoc '(' ')' preclow options no_result_var token IDENTIFIER NUMBER BITVECTOR STRING BVTYPE token PARSE_DECL PARSE_PARAM PARSE_SPEC PARSE_BLOCKS PARSE_STMT PARSE_EXPR PARSE_TYPE
rule
target: program | PARSE_DECL decl { val[1] } | PARSE_PARAM param_decl { val[1] } | PARSE_SPEC spec { val[1] } | PARSE_BLOCKS blocks { val[1] } | PARSE_STMT stmt { val[1] } | PARSE_EXPR expr { val[1] } | PARSE_TYPE type { val[1] } name: IDENTIFIER { val[0] } names: name { [val[0]] } | name ',' names { [val[0]] + val[2] } ident: IDENTIFIER { {name: val[0]} } ident_opt: { nil } | ident idents: ident { [val[0]] } | ident ',' idents { [val[0]] + val[2] } idents_opt: { [] } | idents literal: bool_lit { BooleanLiteral.new value: val[0] } | BITVECTOR { BitvectorLiteral.new val[0] } | NUMBER { IntegerLiteral.new value: val[0] } bool_lit: 'true' { true } | 'false' { false } string: STRING type: type_atom | map_type | name tc_args { CustomType.new name: val[0], arguments: val[1] } type_atom: 'bool' { Type::Boolean } | 'int' { Type::Integer } | BVTYPE { BitvectorType.new width: val[0] } | '(' type ')' { val[1] } map_type: type_args '[' types ']' type { MapType.new arguments: val[0], domain: val[2], range: val[4] } tc_args: { [] } | type_atom tc_args { [val[0]] + val[1] } | name tc_args { [(CustomType.new name: val[0], arguments: val[1])] } | map_type { [val[0]] } types: type { [val[0]] } | type ',' types { [val[0]] + val[2] } type_args: { [] } | '<' names '>' { val[1] } expr: expr '<==>' expr { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] } | expr '==>' expr { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] } | expr '||' expr { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] } | expr '&&' expr { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] } | expr '==' expr { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] } | expr '!=' expr { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] } | expr '<' expr { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] } | expr '>' expr { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] } | expr '<=' expr { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] } | expr '>=' expr { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] } | expr '<:' expr { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] } | expr '++' expr { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] } | expr '+' expr { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] } | expr '-' expr { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] } | expr '*' expr { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] } | expr '/' expr { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] } | expr '%' expr { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] } | '!' expr { LogicalNegation.new expression: val[1] } | '-' expr { ArithmeticNegation.new expression: val[1] } | expr '[' exprs ']' { MapSelect.new map: val[0], indexes: val[2] } | expr '[' exprs ':=' expr ']' { MapUpdate.new map: val[0], indexes: val[2], value: val[4] } | expr '[' NUMBER ':' NUMBER ']' { BitvectorExtract.new bitvector: val[0], msb: val[2], lsb: val[4] } | 'if' expr 'then' expr 'else' expr { IfExpression.new condition: val[1], then: val[3], else: val[5] } | '|' body '|' { CodeExpression.new body: val[1] } | literal | ident '(' exprs_opt ')' { id = FunctionIdentifier.new val[0] FunctionApplication.new function: id, arguments: val[2] } | ident { StorageIdentifier.new val[0] } | 'old' '(' expr ')' { OldExpression.new expression: val[2] } | '(' quantifier type_args param_decls '::' ants expr ')' { QuantifiedExpression.new quantifier: val[1], type_arguments: val[2], variables: val[3], attributes: val[5].select{|a| a.is_a?(Hash)}, triggers: val[5].select{|es| es.is_a?(Array)}.map{|es| Trigger.new(expressions: es)}, expression: val[6] } | '(' expr ')' { val[1] } exprs: expr { [val[0]] } | expr ',' exprs { [val[0]] + val[2] } exprs_opt: { [] } | exprs quantifier: 'forall' {'forall'} | 'exists' {'exists'} attr: '{:' name enss_opt '}' { Attribute.new key: val[1].to_sym, values: val[2] } attrs: { [] } | attr attrs { [val[0]] + val[1] } trigger: '{' exprs '}' { val[1] } ant: attr | trigger ants: { [] } | ant ants { [val[0]] + val[1] } ens: expr | string enss: ens { [val[0]] } | ens ',' enss { [val[0]] + val[2] } enss_opt: { [] } | enss stmt: 'assert' attrs expr ';' { AssertStatement.new attributes: val[1], expression: val[2], token: val[0] } | 'assume' attrs expr ';' { AssumeStatement.new attributes: val[1], expression: val[2], token: val[0] } | 'havoc' idents ';' { ids = val[1].map{|id| StorageIdentifier.new id} HavocStatement.new identifiers: ids, token: val[0] } | lhss ':=' exprs ';' { AssignStatement.new lhs: val[0], rhs: val[2] } | 'call' attrs call_lhs '(' exprs_opt ')' ';' { CallStatement.new attributes: val[1], assignments: val[2][:rets], procedure: val[2][:name], arguments: val[4], token: val[0] } | 'call' 'forall' ident '(' wc_exprs_opt ')' ';' { id = ProcedureIdentifier.new val[2] CallStatement.new assignments: nil, procedure: id, arguments: val[4], token: val[0] } | if_stmt | 'while' '(' wc_expr ')' loop_invs '{' blocks '}' { WhileStatement.new condition: val[2], invariants: val[4], blocks: val[6], token: val[0] } | 'break' ident_opt ';' { id = LabelIdentifier.new(val[1]) if val[1] BreakStatement.new identifier: id, token: val[0] } | 'return' ';' { ReturnStatement.new token: val[0] } | 'return' expr ';' { ReturnStatement.new expression: val[1], token: val[0] } | 'goto' idents ';' { ids = val[1].map{|id| LabelIdentifier.new id} GotoStatement.new identifiers: ids, token: val[0] } stmts: stmt { [val[0]] } | stmt stmts { [val[0]] + val[1] } call_lhs: ident { {name: ProcedureIdentifier.new(val[0]), rets: []} } | idents ':=' ident { ids = val[0].map{|id| StorageIdentifier.new id} id = ProcedureIdentifier.new val[2] {name: id, rets: ids} } if_stmt: 'if' '(' wc_expr ')' '{' blocks '}' else_stmt { IfStatement.new condition: val[2], blocks: val[5], else: val[7], token: val[0] } else_stmt: { nil } | 'else' '{' blocks '}' { val[2] } | 'else' if_stmt { val[1] } lhs: ident selects { id = StorageIdentifier.new val[0] val[1].reduce(id){|m,x| MapSelect.new map: m, indexes: x} } lhss: lhs { [val[0]] } | lhs ',' lhss { [val[0]] + val[2] } select: '[' exprs ']' { val[1] } selects: { [] } | select selects { [val[0]] + val[1] } wc_expr: expr | '*' { Expression::Wildcard } wc_exprs: wc_expr { [val[0]] } | wc_expr ',' wc_exprs { [val[0]] + val[2] } wc_exprs_opt: { [] } | wc_exprs loop_inv: free_opt 'invariant' expr ';' { LoopInvariant.new free: val[0], expression: val[2] } loop_invs: { [] } | loop_inv loop_invs { [val[0]] + val[1] } free_opt: { false } | 'free' { true } blocks: { [Block.new(names: [], statements: [])] } | name ':' blocks { bs = val[2] bs.first.prepend_children(:names,val[0]) bs } | stmt blocks { bs = val[1] bs.unshift(Block.new(names: [], statements: [])) unless bs.first.names.empty? bs.first.prepend_children(:statements,val[0]) bs } body: '{' var_decls blocks '}' { Body.new locals: val[1], blocks: val[2] } decl: type_decl | const_decl | func_decl | axiom_decl | var_decl | proc_decl | impl_decl decls: { [] } | decl decls { [val[0]] + val[1] } type_decl: 'type' attrs finite_opt name tc_params type_syn ';' { if val[5] && val[2] abort "Illegal declaration of type #{([val[3]] + val[4]) * " "}" end TypeDeclaration.new attributes: val[1], finite: val[2], name: val[3], arguments: val[4], type: val[5] } finite_opt: { false } | 'finite' { true } tc_params: { [] } | name tc_params { [val[0]] + val[1] } type_syn: { nil } | '=' type { val[1] } const_decl: 'const' attrs unique_opt typed_ids order_spec ';' { ConstantDeclaration.new(val[3].merge({attributes: val[1], unique: val[2], order_spec: val[4]})) } unique_opt: { false } | 'unique' { true } order_spec: parent_info complete_opt { [val[0],val[1]] } parent_info: { nil } | '<:' parent_edges_opt { val[1] } parent_edge: unique_opt ident { id = StorageIdentifier.new val[1] [val[0],id] } parent_edges: parent_edge { [val[0]] } | parent_edge ',' parent_edges { [val[0]] + val[2] } parent_edges_opt: { [] } | parent_edges complete_opt: { false } | 'complete' { true } func_decl: 'function' attrs name type_args '(' fargs_opt ')' 'returns' '(' farg ')' fbody { FunctionDeclaration.new attributes: val[1], name: val[2], type_arguments: val[3], arguments: val[5], return: val[9], body: val[11] } farg: typed_ids { StorageDeclaration.new val[0] } | type { StorageDeclaration.new(names: [], type: val[0]) } fargs: type { [{names: [], type: val[0]}] } | type ',' fargs { if val[2].first[:names].empty? [{names: [], type: val[0]}] + val[2] else val[2].first[:names].unshift(val[0]) val[2] end } | type ':' fargs { # assert val[2].first[:names].empty? unless val[0].respond_to?(:name) raise ParseError, "parse error on value #{val[0]}: expecting name." end if val[2].first[:names].empty? val[2].first[:names].unshift(val[0]) val[2] else [{names: [val[0]], type: val[2].first[:names].shift}] + val[2] end } fargs_opt: { [] } | fargs { val[0].map do |x| x[:names].map!{|t| t.name} StorageDeclaration.new(x) end } fbody: ';' { nil } | '{' expr '}' { val[1] } axiom_decl: 'axiom' attrs expr ';' { AxiomDeclaration.new attributes: val[1], expression: val[2] } var_decl: 'var' attrs typed_ids_where ';' { VariableDeclaration.new(val[2].merge({attributes: val[1]})) } typed_ids: names ':' type { {names: val[0], type: val[2]} } typed_ids_where: typed_ids where_clause { val[0].merge(val[1]) } var_decls: { [] } | var_decl var_decls { [val[0]] + val[1] } where_clause: { {} } | 'where' expr { {where: val[1]} } proc_decl: 'procedure' attrs name type_args '(' param_decls_opt ')' out_params pspec { ProcedureDeclaration.new attributes: val[1], name: val[2], type_arguments: val[3], parameters: val[5], returns: val[7], specifications: val[8][:specs], body: val[8][:body] } out_params: { [] } | 'returns' '(' param_decls_opt ')' { val[2] } pspec: ';' specs { {specs: val[1], body: nil} } | specs body { {specs: val[0], body: val[1]} } param_decl: typed_ids_where { StorageDeclaration.new val[0] } param_decls: param_decl { [val[0]] } | param_decl ',' param_decls { [val[0]] + val[2] } param_decls_opt: { [] } | param_decls spec: free_opt 'requires' attrs expr ';' { RequiresClause.new free: val[0], attributes: val[2], expression: val[3] } | free_opt 'modifies' attrs idents ';' { ids = val[3].map{|id| StorageIdentifier.new id} ModifiesClause.new free: val[0], attributes: val[2], identifiers: ids } | free_opt 'ensures' attrs expr ';' { EnsuresClause.new free: val[0], attributes: val[2], expression: val[3] } specs: { [] } | spec specs { [val[0]] + val[1] } impl_decl: 'implementation' attrs name type_args '(' param_decls_opt ')' out_params body { ImplementationDeclaration.new attributes: val[1], name: val[2], type_arguments: val[3], parameters: val[5], returns: val[7], specifications: [], body: val[8] } program: decls { Program.new declarations: val[0] }
end
—- header require_relative 'lexer.rex' require_relative 'ast/token' require_relative 'ast/program' require_relative 'ast/declaration' require_relative 'ast/specification' require_relative 'ast/statement' require_relative 'ast/expression' require_relative 'ast/type' include Bpl::AST
—- inner def parse(input)
scan_str(input)
end
def parse_special(str, kind)
scan_setup("$$PARSE_#{kind.upcase}$$ " + str) do_parse
end
def parse_decl(str) parse_special(str, :decl) end def parse_param(str) parse_special(str, :param) end def parse_spec(str) parse_special(str, :spec) end def parse_blocks(str) parse_special(str, :blocks) end def parse_block(str) parse_special(str, :blocks).first end def parse_stmt(str) parse_special(str, :stmt) end def parse_expr(str) parse_special(str, :expr) end def parse_type(str) parse_special(str, :type) end
def parse_str(str)
case str when /\b(type|const|function|axiom|var|procedure|implementation)\b/ parse_decl(str) when /\A\s*#{Bpl::IDENTIFIER}:.*;.*\s+#{Bpl::IDENTIFIER}:/m parse_blocks(str) when /\A\s*#{Bpl::IDENTIFIER}:.*;/m parse_block(str) when /\b(assert|assume|havoc|call|if|while|break|goto|return)\b|:=/ parse_stmt(str) when /\b(requires|ensures|modifies|invariant)\b/ parse_spec(str) when /[^<:]:[^:]/ parse_param(str) else parse_expr(str) end
end
—- footer