63 lines
3 KiB
Python
63 lines
3 KiB
Python
from fuzzingbook.Grammars import Grammar, is_valid_grammar, convert_ebnf_grammar
|
|
from isla.solver import ISLaSolver
|
|
|
|
GAZPREA_TOP_LEVEL: Grammar = {
|
|
# Top level elements
|
|
'<start>': ['<topBlock>'],
|
|
'<topBlock>': ['<XML_OPEN_TAG>block<XML_CLOSE_TAG><routine_list><main_routine><routine_list><XML_OPEN_SLASH>block<XML_CLOSE_TAG>'],
|
|
# TODO constants
|
|
|
|
# Routines
|
|
'<routine>': ['<function>', '<procedure>'], # TODO forward_declaration
|
|
'<function>': [
|
|
'<XML_OPEN_TAG>function name="_NAME_" return_type="_TYPE_" args="_ARGS_"<XML_CLOSE_TAG><return_block><XML_OPEN_SLASH>function<XML_CLOSE_TAG>'],
|
|
'<procedure>': [
|
|
'<XML_OPEN_TAG>procedure name="_NAME_" return_type="_TYPE_" args="_ARGS_"<XML_CLOSE_TAG><block><XML_OPEN_SLASH>procedure<XML_CLOSE_TAG>'],
|
|
'<main_routine>': [
|
|
'<XML_OPEN_TAG>procedure name="main" return_type="int" args="()"<XML_CLOSE_TAG><return_block><XML_OPEN_SLASH>procedure<XML_CLOSE_TAG>'],
|
|
'<routine_list>': ['<routine><routine_list><routine>', '<routine>'],
|
|
|
|
# Blocks
|
|
'<block>': ['<XML_OPEN_TAG>block<XML_CLOSE_TAG><statement_list><XML_OPEN_SLASH>block<XML_CLOSE_TAG>'],
|
|
'<return_block>': ['<XML_OPEN_TAG>block<XML_CLOSE_TAG><statement_list><return><XML_OPEN_SLASH>block<XML_CLOSE_TAG>'],
|
|
'<statement>': [
|
|
'<declaration>',
|
|
'<stream>',
|
|
# '<call>',
|
|
# '<return>', # TODO if/else, loop
|
|
],
|
|
'<statement_list>': ['<statement><statement_list><statement>', '<statement>'],
|
|
|
|
# Things that belong on their own lines
|
|
'<declaration>': ['<XML_OPEN_TAG>declaration<XML_CLOSE_TAG><variable><rhs><XML_OPEN_SLASH>declaration<XML_CLOSE_TAG>'],
|
|
'<stream>': ['<out_stream>'], #, '<in_stream>'],
|
|
'<return>': ['<XML_OPEN_TAG>return<XML_CLOSE_TAG><has_value><XML_OPEN_SLASH>return<XML_CLOSE_TAG>'],
|
|
|
|
'<out_stream>': ['<XML_OPEN_TAG>stream type="std_output"<XML_CLOSE_TAG><has_value><XML_OPEN_SLASH>stream<XML_CLOSE_TAG>'],
|
|
# '<in_stream>': ['<XML_OPEN_TAG>stream type="std_input"<XML_CLOSE_TAG><has_value><XML_OPEN_SLASH>stream<XML_CLOSE_TAG>'],
|
|
|
|
# Things that are part of lines
|
|
'<has_value>': ['<variable>', '<literal>', '<operator>'],
|
|
'<lhs>': ['<XML_OPEN_TAG>lhs<XML_CLOSE_TAG><has_value><XML_OPEN_SLASH>lhs<XML_CLOSE_TAG>'],
|
|
'<rhs>': ['<XML_OPEN_TAG>rhs<XML_CLOSE_TAG><has_value><XML_OPEN_SLASH>rhs<XML_CLOSE_TAG>'],
|
|
|
|
# Things that have values
|
|
'<operator>': ['<XML_OPEN_TAG>operator<XML_CLOSE_TAG><lhs><rhs><XML_OPEN_SLASH>operator<XML_CLOSE_TAG>'],
|
|
'<variable>': ['<XML_OPEN_TAG>variable mut="_MODIFIER_" type="_TYPE_" name="_NAME_"<XML_SLASH_TAG>'],
|
|
'<literal>': ['<XML_OPEN_TAG>literal type="_TYPE_" value="_VALUE_"<XML_SLASH_TAG>'],
|
|
|
|
# Helper rules
|
|
'<XML_OPEN_TAG>': ['<'],
|
|
'<XML_CLOSE_TAG>': ['>'],
|
|
'<XML_SLASH_TAG>': ['/>'],
|
|
'<XML_OPEN_SLASH>': ['</'],
|
|
}
|
|
|
|
if __name__ == "__main__":
|
|
assert is_valid_grammar(GAZPREA_TOP_LEVEL)
|
|
|
|
initial_grammar = convert_ebnf_grammar(GAZPREA_TOP_LEVEL)
|
|
solver = ISLaSolver(initial_grammar)
|
|
constants_tree_str = str(solver.solve())
|
|
print(constants_tree_str)
|