diff --git a/.gitignore b/.gitignore index 3e9dcb3..a98134d 100644 --- a/.gitignore +++ b/.gitignore @@ -162,4 +162,7 @@ cython_debug/ # Extra files and hidden folder. testcases/ -build/ \ No newline at end of file +build/ + +virtual/ +.vscode/ \ No newline at end of file diff --git a/ChironCore/ChironAST/ChironAST.py b/ChironCore/ChironAST/ChironAST.py index f86c5da..3f3b8f8 100644 --- a/ChironCore/ChironAST/ChironAST.py +++ b/ChironCore/ChironAST/ChironAST.py @@ -36,6 +36,13 @@ def __init__(self, condition): def __str__(self): return self.cond.__str__() +class AnalysisCommand(Instruction): + def __init__(self, statement, condition): + self.stmt = statement + self.cond = condition + def __str__(self): + return self.stmt + " (" + self.cond.__str__() + ")" + class MoveCommand(Instruction): def __init__(self, motion, expr): self.direction = motion @@ -126,6 +133,10 @@ class Div(BinArithOp): def __init__(self, lexpr, rexpr): super().__init__(lexpr, rexpr, "/") +class Mod(BinArithOp): + def __init__(self, lexpr, rexpr): + super().__init__(lexpr, rexpr, "%") + # --Boolean Expressions----------------------------------------------- diff --git a/ChironCore/ChironAST/builder.py b/ChironCore/ChironAST/builder.py index b38265e..2f59ea1 100644 --- a/ChironCore/ChironAST/builder.py +++ b/ChironCore/ChironAST/builder.py @@ -88,6 +88,8 @@ def visitMulExpr(self, ctx:tlangParser.MulExprContext): return ChironAST.Mult(left, right) elif ctx.multiplicative().DIV(): return ChironAST.Div(left, right) + elif ctx.multiplicative().MOD(): + return ChironAST.Mod(left, right) # Visit a parse tree produced by tlangParser#parenExpr. @@ -97,7 +99,7 @@ def visitParenExpr(self, ctx:tlangParser.ParenExprContext): def visitCondition(self, ctx:tlangParser.ConditionContext): if ctx.PENCOND(): - return ChironAST.PenStatus(); + return ChironAST.PenStatus() if ctx.NOT(): expr1 = self.visit(ctx.condition(0)) @@ -172,3 +174,34 @@ def visitMoveCommand(self, ctx:tlangParser.MoveCommandContext): def visitPenCommand(self, ctx:tlangParser.PenCommandContext): return [(ChironAST.PenCommand(ctx.getText()), 1)] + + def visitAnalysisCommand(self, ctx:tlangParser.AnalysisCommandContext): + analysisCommand = ctx.analysisStatement().getText() + analysisCondition = self.visit(ctx.condition()) + return [(ChironAST.AnalysisCommand(analysisCommand, analysisCondition), 1)] + +class astGenPassSMTLIB(astGenPass): + def __init__(self): + super().__init__() + self.repeatInstrCount = 0 # keeps count for no of 'repeat' instructions + + def visitIfConditional(self, ctx:tlangParser.IfConditionalContext): + condObj = ChironAST.ConditionCommand(self.visit(ctx.condition())) + thenInstrList = self.visit(ctx.strict_ilist()) + boolFalse = ChironAST.ConditionCommand(ChironAST.BoolFalse()) + elseInstrList = [(boolFalse, 1)] + jumpOverElseBlock = [(ChironAST.ConditionCommand(ChironAST.BoolFalse()), len(elseInstrList) + 1)] + return [(condObj, len(thenInstrList) + 2)] + thenInstrList + jumpOverElseBlock + elseInstrList + + def visitMoveCommand(self, ctx): + mvcommand = ctx.moveOp().getText() + mvexpr = self.visit(ctx.expression()) + if mvcommand == "forward" or mvcommand == "backward": + return [(ChironAST.MoveCommand(mvcommand, mvexpr), 1), (ChironAST.NoOpCommand(), 1)] + else: + return super().visitMoveCommand(ctx) + + def visitGotoCommand(self, ctx): + return [(super().visitGotoCommand(ctx)), (ChironAST.NoOpCommand(), 1)] + + \ No newline at end of file diff --git a/ChironCore/ProofEngine/Docs/Compiler_Project_Description.pdf b/ChironCore/ProofEngine/Docs/Compiler_Project_Description.pdf new file mode 100644 index 0000000..b3e7ad4 Binary files /dev/null and b/ChironCore/ProofEngine/Docs/Compiler_Project_Description.pdf differ diff --git a/ChironCore/ProofEngine/Docs/Final_Report.pdf b/ChironCore/ProofEngine/Docs/Final_Report.pdf new file mode 100644 index 0000000..d302679 Binary files /dev/null and b/ChironCore/ProofEngine/Docs/Final_Report.pdf differ diff --git a/ChironCore/ProofEngine/Docs/Report1.pdf b/ChironCore/ProofEngine/Docs/Report1.pdf new file mode 100644 index 0000000..e81d4b8 Binary files /dev/null and b/ChironCore/ProofEngine/Docs/Report1.pdf differ diff --git a/ChironCore/ProofEngine/Docs/Report2.pdf b/ChironCore/ProofEngine/Docs/Report2.pdf new file mode 100644 index 0000000..0ac0faa Binary files /dev/null and b/ChironCore/ProofEngine/Docs/Report2.pdf differ diff --git a/ChironCore/ProofEngine/Infix_To_Prefix.py b/ChironCore/ProofEngine/Infix_To_Prefix.py new file mode 100644 index 0000000..9cd2e9c --- /dev/null +++ b/ChironCore/ProofEngine/Infix_To_Prefix.py @@ -0,0 +1,159 @@ +import ast +import re + +""" +This module provides functionality to convert infix expressions into prefix (SMT-LIB) format. +It uses Python's `ast` module to parse expressions and a custom visitor class to traverse +the abstract syntax tree (AST) and generate the corresponding prefix notation. +""" + +class PrefixNotationConverter(ast.NodeVisitor): + """ + A custom AST visitor class to convert infix expressions into prefix notation. + """ + + def visit_BinOp(self, node): + """ + Handles binary operations (e.g., +, -, *, /). + Converts them into prefix notation (e.g., (+ left right)). + """ + op = self.get_operator(node.op) + left = self.visit(node.left) + right = self.visit(node.right) + return f"({op} {left} {right})" + + def visit_Compare(self, node): + """ + Handles comparison operations (e.g., ==, !=, >, <, >=, <=). + Converts them into prefix notation. + Special handling for "!=" to represent it as (not (= left right)). + """ + op = self.get_operator(node.ops[0]) + left = self.visit(node.left) + right = self.visit(node.comparators[0]) + if op == '!=': # Handle "!=" as (not (= expr1 expr2)) + return f"(not (= {left} {right}))" + else: + return f"({op} {left} {right})" + + def visit_BoolOp(self, node): + """ + Handles boolean operations (e.g., and, or). + Converts them into prefix notation (e.g., (and expr1 expr2 ...)). + """ + op = self.get_operator(node.op) + values = " ".join(self.visit(value) for value in node.values) + return f"({op} {values})" + + def visit_UnaryOp(self, node): + """ + Handles unary operations (e.g., not, -). + Converts them into prefix notation (e.g., (not operand)). + """ + op = self.get_operator(node.op) + operand = self.visit(node.operand) + return f"({op} {operand})" + + def visit_Name(self, node): + """ + Handles variable names. + Returns the variable name as is. + """ + return node.id + + def visit_Constant(self, node): + """ + Handles constant values (e.g., numbers, strings). + Returns the constant value as a string. + """ + return str(node.value) + + def get_operator(self, op): + """ + Maps Python AST operators to their corresponding SMT-LIB operators. + """ + operators = { + ast.Add: '+', + ast.Sub: '-', + ast.Mult: '*', + ast.Div: 'div', + ast.Gt: '>', + ast.Lt: '<', + ast.GtE: '>=', + ast.LtE: '<=', + ast.Eq: '=', + ast.NotEq: '!=', + ast.Mod: 'mod', + ast.And: 'and', + ast.Or: 'or', + ast.Not: '~', + ast.Assign: '=', + ast.USub: '-', # Unary subtraction + } + return operators[type(op)] + +def preprocess_expression(expr: str, replace_eq): + """ + Preprocesses the input expression to make it compatible with Python's `ast` module. + - Replaces variable prefixes (e.g., ":var" -> "var"). + - Removes spaces. + - Optionally replaces single "=" with "==" for equality checks. + + Args: + expr (str): The input infix expression. + replace_eq (bool): Whether to replace "=" with "==" for equality. + + Returns: + str: The preprocessed expression. + """ + expr = re.sub(r":(\w+)", r"\1", expr) # Remove ":" prefix from variables + expr = expr.replace(" ", "") # Remove spaces + if replace_eq: + expr = re.sub(r"(?=!])=(?!=)", "==", expr) # Replace "=" with "==" for equality + return expr + +def Construct_AST(expr: str, replace_eq): + """ + Constructs an abstract syntax tree (AST) from the given infix expression. + + Args: + expr (str): The input infix expression. + replace_eq (bool): Whether to preprocess the expression to replace "=" with "==". + + Returns: + ast.AST: The constructed AST. + + Raises: + Exception: If there is a syntax error in the input expression. + """ + expr = preprocess_expression(expr, replace_eq) + # print(expr) # Debugging print for the preprocessed expression + try: + tree = ast.parse(expr, mode='eval') # Parse the expression in evaluation mode + return tree + except SyntaxError as e: + print(expr) # Debugging print for the expression causing the error + raise Exception(f"Syntax Error: {e}") + +def Infix_To_Prefix(expr: str, replace_eq=False): + """ + Converts an infix expression into prefix notation. + + Args: + expr (str): The input infix expression. + replace_eq (bool): Whether to preprocess the expression to replace "=" with "==". + + Returns: + str: The prefix notation of the expression, or None if the input is empty. + """ + if expr: + tree = Construct_AST(expr, replace_eq) + if tree: + converter = PrefixNotationConverter() + expr = converter.visit(tree.body) # Visit the root of the AST + return expr + else: + return None + else: + return None + diff --git a/ChironCore/ProofEngine/README.md b/ChironCore/ProofEngine/README.md new file mode 100644 index 0000000..c15b950 --- /dev/null +++ b/ChironCore/ProofEngine/README.md @@ -0,0 +1,151 @@ +# Description +ProofEngine is tool for program verification built upon the chiron framework. It allows the user to add analysis statements in the source code for deductive verification. It takes the analysis source code as input and generates a SMTLIB code, which is then checked for satisfiabilty using an integrated Z3 Solver. + +# How to Run +Ensure you have Python Z3 solver installed. + +```bash +pip install z3-solver +``` +Open the folder in the main directory. +```bash +cd ChironCore +``` +Use `-smt/--smtlib` flag for running ProofEngine. +```bash +python3 chiron.py -smt +python3 chiron.py --smtlib +``` + +# Examples +## Example1 +Consider a toy program which checks if the cubic identity \((a-b)3 = a3 - 3a2b + 3ab2 - b3\) is correct (`./examples/cube.tl`) + +``` +assume(1==1) +:c1 = :a*:a*:a - 3*:a*:a*:b + 3*:a*:b*:b - :b*:b*:b +:c2 = (:a-:b)*(:a-:b)*(:a-:b) +assert(:c1 == :c2) +``` + + +```bash +python3 chiron.py -smt ./examples/cube.tl +``` +The output should looks like this +```stdout +======Z3 Output:====== + +Condition verified :) +``` + +Let us introduce a bug (`./examples/cube_buggy.tl) +``` +assume(1==1) +:c1 = :a*:a*:a - 3*:a*:a*:b - 3*:a*:b*:b + :b*:b*:b +:c2 = (:a-:b)*(:a-:b)*(:a-:b) +assert(:c1 == :c2) +``` + +Use the `-smt\--smtlib` flag for running ProofEngine + +```bash +python3 chiron.py -smt ./examples/cube_buggy.tl +``` +The output should looks like this +```stdout +======Z3 Output:====== + +Condition verification failed :( +Counterexample: +a_0_0 : -1 +c2_0_1 : -8 +c1_0_1 : 0 +b_0_0 : 1 + +Please refer to "control_flow_graph.png" for variable names. +``` +Not only we see that the verification fails, but we also get the set of values for which the program will fail. + +## Example2 +Consider a program for sum of an arithmetic progression +``` +:s = 0 +:i = :a +repeat :n [ + :s = :s + :i + :i = :i + :d +] +``` +We want to prove that the program is correct. For programs with a loop, we need to provide an invariant of the loop. We can insert analysis code as follows - +``` +assume(:s==0 && :i==:a) +repeat :n [ + invariant(:s == (((:n-:REPCOUNTER)*(2*:a + (:n-:REPCOUNTER-1)*:d))/2) && (:i == :a + (:n-:REPCOUNTER)*:d) ) + :s = :s + :i + :i = :i + :d +] +assert(:s == ((:n*(2*:a + (:n-1)*:d))/2)) +``` +This test case is present in `./examples/arithmetic_progression.tl`. + +```bash +python3 chiron.py -smt ./examples/arithmetic_progression.tl +``` +The output should looks like this +```stdout +======Z3 Output:====== + +Initialization Condition verified :) + +Loop Condition verified :) + +Final Condition verified :) +``` +If there is a bug in the code, output will show which condition failed and also the list of values for which the condition fails. +```stdout +======Z3 Output:====== + +Initialization Condition verified :) + +Loop Condition verified :) + +Final Condition verification failed :( +Counterexample: + +``` + +## Example3 +We can also use it for more complicated programs which use the turtle commands. For example, we can prove iff the turtle starts in the inner box, it will not step outside the outer box (see `home.tl` for analysis code and `home_src.tl` for source code)- + +
+ +
+ +
+ +
+ +
+ +**Please refer to `./examples/` directory for more interesting testcases.** + +# Use Cases +1. **Proving program correctness :** We can use ProofEngine to prove that a program is correct or that a program shows a certain behaviour/property by inserting suitable analysis code. +2. **Finding bugs :** If a program is incorrect, we can find a counterexample to prove that the program is incorrect. +3. **Proving two programs are equivalent :** We can write the analysis code suitably to prove that two programs always behave the same. See `./examples/leapyear.tl` for example testcase. +4. **Proving correctness for unbounded loops :** Since ProofEngine utilizes __invariant__, we can do deductive verification and prove correctness for unbounded loops, i.e.,conditions like P is true ∀ n can be proven. +5. **Path Feasibility :** We can check if a certain execution path in the program is feasible. + +# Other Details +For writing the constraints on the turtle's state, following variables are reserved, which the user can use - + +- TURTLEX : for turtle's x-coordinate +- TURTLEY : for turtle's y-coordinate +- TURTLEANGLE : for turtle's angle of direction +- TURTLEPEN : for turtle's penstatus (0 for pendown, 1 for penup) + +For loops, repcounter, REPCOUNTER can be used. + diff --git a/ChironCore/ProofEngine/Smtlib_Helper.py b/ChironCore/ProofEngine/Smtlib_Helper.py new file mode 100644 index 0000000..bd01294 --- /dev/null +++ b/ChironCore/ProofEngine/Smtlib_Helper.py @@ -0,0 +1,158 @@ +import sys +import re + +""" +This module provides helper functions for generating SMT-LIB code, extracting variables, +and converting conditions and code bodies into SMT-LIB format. It also includes functionality +to parse the program, generate IR, and build the control flow graph (CFG). +""" + +# Add necessary paths for importing modules +sys.path.insert(0, "../cfg/") +sys.path.insert(0, "../ChironAST/") +sys.path.insert(0, "../ProofEngine/") + +from ChironAST.builder import astGenPassSMTLIB +from ProofEngine.TurtleCommandsCompiler import TurtleCommandsCompiler +from ProofEngine.Infix_To_Prefix import Infix_To_Prefix +from cfg import cfgBuilder as cfgB + +def generate_cfg_and_ir(parseTree, irHandler): + """ + Parses the program, generates IR, compiles it into a new IR list, and builds the CFG. + + Args: + parseTree: The parse tree of the program. + irHandler: The IRHandler instance to manage the IR. + + Returns: + tuple: A tuple containing the CFG and the number of loops in the program. + """ + # Parse the program and generate IR + astgen = astGenPassSMTLIB() + ir = astgen.visitStart(parseTree) + num_loops = astgen.repeatInstrCount + irHandler.setIR(ir) + + # Compile the IR into a new IR list + new_irList = [] + turt_compiler = TurtleCommandsCompiler() + for entry in irHandler.ir: + new_stmt = turt_compiler.compile(entry[0]) + for stmt in new_stmt: + new_irList.append((stmt, entry[1])) + + # Build the CFG + cfg = cfgB.buildCFG(new_irList, "control_flow_graph", False) + + return cfg, num_loops + +def list_to_smtlib_stmt(L): + """ + Converts a list of statements into SMT-LIB format. + + Args: + L (list): A list of infix expressions. + + Returns: + str: The SMT-LIB formatted string representing the list of statements. + """ + if len(L) == 1: + return Infix_To_Prefix(L[0], True) + smtlib_stmt = "(and " + for stmt in L: + stmt = Infix_To_Prefix(stmt, True) + smtlib_stmt += f"{stmt} " + smtlib_stmt += ")\n" + return smtlib_stmt + +def extract_variables(expression: str): + """ + Extracts variables from a given expression. + + Args: + expression (str): The input expression. + + Returns: + list: A sorted list of variables found in the expression. + """ + tokens = re.findall(r'[a-zA-Z_]\w*', expression) + keywords = {"ite", "and", "or", "not", "assert", "div", "true", "false", "mod"} + variables = {token for token in tokens if token not in keywords and not token.isdigit()} + return sorted(variables) + +def generate_smtlib_code(pre_condition, post_condition, loop_condition=None, invariant_in=None, invariant_out=None, loop_body=None, loop_false_condition=None): + """ + Generates SMT-LIB code based on the given conditions and loop structure. + + Args: + pre_condition (str): The pre-condition in SMT-LIB format. + post_condition (str): The post-condition in SMT-LIB format. + loop_condition (str, optional): The loop condition in SMT-LIB format. + invariant_in (str, optional): The loop invariant before the loop body. + invariant_out (str, optional): The loop invariant after the loop body. + loop_body (str, optional): The loop body in SMT-LIB format. + loop_false_condition (str, optional): The condition when the loop exits. + + Returns: + str: The generated SMT-LIB code. + """ + smtlib_code = "" + all_vars = set() + + if loop_condition is None: # No loop + check = f"(=> (and {pre_condition} {loop_body}) {post_condition})" + all_vars.update(extract_variables(check)) + smtlib_code += "".join([f"(declare-fun {var} () Int)\n" for var in all_vars]) + smtlib_code += f"(assert (not {check}))\n" + smtlib_code += "(check-sat)\n(get-model)\n" + else: # With loop + first_check = f"(=> {pre_condition} {invariant_in})" + second_check = f"(=> (and {invariant_in} {loop_body} {loop_condition}) {invariant_out})" + third_check = f"(=> (and {invariant_out} {loop_false_condition}) {post_condition})" + + all_vars.update(extract_variables(first_check)) + all_vars.update(extract_variables(second_check)) + all_vars.update(extract_variables(third_check)) + + smtlib_code += "".join([f"(declare-fun {var} () Int)\n" for var in all_vars]) + smtlib_code += "(push 1)\n" + smtlib_code += f"(assert (not {first_check}))\n" + smtlib_code += "(check-sat)\n(get-model)\n(pop 1)\n" + smtlib_code += "(push 1)\n" + smtlib_code += f"(assert (not {second_check}))\n" + smtlib_code += "(check-sat)\n(get-model)\n(pop 1)\n" + smtlib_code += "(push 1)\n" + smtlib_code += f"(assert (not {third_check}))\n" + smtlib_code += "(check-sat)\n(get-model)\n(pop 1)\n" + + return smtlib_code + +def generate_code_body(code_body_list): + """ + Generates the SMT-LIB code body from the given code body list. + + Args: + code_body_list (list): A list of code body entries, where each entry is a tuple + representing an assignment or an if-else block. + + Returns: + str: The SMT-LIB formatted code body as a string. + """ + code_body = "(and " + for entry in code_body_list: + if entry[0] == "assign": + for stmt in entry[1]: + code_body += Infix_To_Prefix(stmt, True) + elif entry[0] == "if-else": + condition = entry[1] + then_part = entry[2] + else_part = entry[3] + then_stmt = list_to_smtlib_stmt(then_part) + else_stmt = list_to_smtlib_stmt(else_part) + cond_stmt = list_to_smtlib_stmt([condition]) + then_stmt = f"(and {cond_stmt} {then_stmt})" + else_stmt = f"(and (not {cond_stmt}) {else_stmt})" + code_body += f"(or {then_stmt} {else_stmt})" + code_body += "true)\n" + return code_body diff --git a/ChironCore/ProofEngine/TraverseCFG.py b/ChironCore/ProofEngine/TraverseCFG.py new file mode 100644 index 0000000..fc4e4b8 --- /dev/null +++ b/ChironCore/ProofEngine/TraverseCFG.py @@ -0,0 +1,789 @@ +from ChironAST import ChironAST +from cfg import ChironCFG +import networkx as nx +import re +import cfg.cfgBuilder as cfgB + +""" +This module provides functionality to traverse and process the control flow graph (CFG). +It includes methods for extracting variables, renaming variables, processing basic blocks, and verifying the CFG format for programs with or without loops. +""" + +def extract_variables_assign(stmt): + """ + Extracts variables from an assignment statement. + + Args: + stmt (str): The assignment statement in the form "lhs = rhs". + + Returns: + tuple: A tuple containing: + - rhs_vars (list): Variables found in the right-hand side (RHS) of the statement. + - rhs_expr (str): The RHS expression as a string. + - lhs_vars (list): Variables found in the left-hand side (LHS) of the statement. + - lhs_expr (str): The LHS expression as a string. + + Raises: + ValueError: If the input statement does not contain an "=" sign, indicating it is not a valid assignment. + """ + # Remove leading and trailing whitespace from the statement + stmt = stmt.strip() + + # Check if the statement contains an "=" sign; raise an error if not + if "=" not in stmt: + raise ValueError(f"Invalid assignment statement: {stmt}") + + # Split the statement into LHS (left-hand side) and RHS (right-hand side) at the "=" sign + lhs_expr, rhs_expr = stmt.split("=", 1) + + # Remove leading and trailing whitespace from both LHS and RHS + lhs_expr = lhs_expr.strip() + rhs_expr = rhs_expr.strip() + + # Use regex to extract variables from the LHS and RHS + # Variables are identified by the pattern ":" + lhs_vars = re.findall(r'(:[a-zA-Z_][a-zA-Z0-9_]*)', lhs_expr) + rhs_vars = re.findall(r'(:[a-zA-Z_][a-zA-Z0-9_]*)', rhs_expr) + + # Return the extracted variables and expressions as a tuple + return rhs_vars, rhs_expr, lhs_vars, lhs_expr + +def extract_variables_others(stmt): + """ + Extracts variables from non-assignment statements. + + Args: + stmt (str): The statement from which variables need to be extracted. + + Returns: + list: A list of variables found in the statement. + + Explanation: + - This function uses a regular expression to identify variables in the statement. + - Variables are expected to follow the pattern ":", where + starts with a letter or underscore and can be followed by alphanumeric characters or underscores. + """ + # Use regex to find all variables in the statement + variables = re.findall(r'(:[a-zA-Z_][a-zA-Z0-9_]*)', stmt) + return variables + + +def rename_vars(ir): + """ + Renames variables in the intermediate representation (IR) to ensure uniqueness. + + Args: + ir (list): The intermediate representation (IR) as a list of statements. + Each statement is a tuple where the first element is the statement string + and the second element is the type of the statement (e.g., "assign"). + + Returns: + tuple: A tuple containing: + - rename_map (dict): A mapping of variables to their renamed versions. + - updated_ir (list): The updated IR with renamed variables. + + Explanation: + - This function processes each statement in the IR to rename variables for uniqueness. + - Variables in the right-hand side (RHS) and left-hand side (LHS) are renamed using a counter. + - The renaming ensures that variables are uniquely identified across the IR. + + Steps: + 1. Extract variables from the RHS and LHS of each statement. + 2. Rename RHS variables using the `rename_map` dictionary. + 3. Rename LHS variables and increment their counters in `rename_map`. + 4. Combine the renamed LHS and RHS into a new statement and add it to the updated IR. + """ + updated_ir = [] # List to store the updated IR with renamed variables + rename_map = {} # Dictionary to map variables to their renamed versions + + for stmt in ir: + lexpr = "" # Left-hand side expression + rexpr = "" # Right-hand side expression + rhs_vars = [] # Variables in the RHS + lhs_vars = [] # Variables in the LHS + + # print(stmt) # Debugging print for the current statement + + # Process assignment statements + if stmt[1] == "assign": + vars = extract_variables_assign(stmt[0]) # Extract variables from the assignment + rhs_vars = vars[0] # Variables in the RHS + rexpr = vars[1] # RHS expression + lhs_vars = vars[2] # Variables in the LHS + lexpr = vars[3] # LHS expression + else: + # Process non-assignment statements + vars = extract_variables_others(stmt[0]) # Extract variables from the statement + # print(vars) # Debugging print for extracted variables + rhs_vars = vars # Variables in the RHS + rexpr = stmt[0] # RHS expression + lhs_vars = [] # No LHS for non-assignment statements + lexpr = "" # No LHS expression + + # print(rhs_vars, rexpr, lhs_vars, lexpr) # Debugging print for extracted variables and expressions + + # Rename RHS variables + for var in rhs_vars: + if var not in rename_map: + rename_map[var] = 0 # Initialize the variable in the rename map + # raise ValueError(f"Variable '{var}' not initialised before first use!") # Uncomment for strict checks + # Replace the variable in the RHS with its renamed version + rexpr = re.sub(rf'{var}\b', f'{var}_{rename_map[var]}', rexpr) + + # Rename LHS variables + for var in lhs_vars: + if var not in rename_map: + rename_map[var] = 1 # Initialize the variable in the rename map + else: + rename_map[var] += 1 # Increment the counter for the variable + # Replace the variable in the LHS with its renamed version + lexpr = re.sub(rf'{var}\b', f'{var}_{rename_map[var]}', lexpr) + + # Combine the renamed LHS and RHS into a single statement + if lexpr != "": + lexpr += '=' # Add the "=" sign to the LHS + updated_ir.append([lexpr + rexpr, stmt[1]]) # Add the renamed statement to the updated IR + else: + updated_ir.append([rexpr, stmt[1]]) # Add the renamed RHS-only statement to the updated IR + + # print(updated_ir) # Debugging print for the updated IR + return rename_map, updated_ir + + +def process_bb1(node: ChironCFG.BasicBlock): + """ + Processes a basic block to extract and classify instructions. + + Args: + node (ChironCFG.BasicBlock): The basic block to process. + + Returns: + None + + Explanation: + - This function processes the instructions in a basic block and classifies them into types such as "assign", + "condition", "assert", "assume", or "invariant". + - It also renames special variables (e.g., TURTLEX, TURTLEY) to their internal representations (e.g., __turtleX, __turtleY). + - Variables are further renamed to include the block ID for uniqueness. + - The processed instructions are stored back in the `instrlist` of the node. + + Steps: + 1. Iterate through the instructions in the basic block. + 2. Classify each instruction based on its type (e.g., assignment, condition, analysis commands). + 3. Replace special variables with their internal representations. + 4. Append the processed instruction to the new instruction list. + 5. Update the node's `instrlist` with the processed instructions. + """ + new_instrlist = [] # List to store the processed instructions + block_id = node.irID # Block ID for variable renaming + + for entry in node.instrlist: + stmt = str(entry[0]) # Convert the instruction to a string + if stmt == "False" or stmt == "True": + continue # Skip boolean literals + + type = None # Initialize the type of the instruction + + # Classify the instruction based on its type + if isinstance(entry[0], ChironAST.AssignmentCommand): + type = "assign" + elif isinstance(entry[0], ChironAST.ConditionCommand): + type = "condition" + elif isinstance(entry[0], ChironAST.AnalysisCommand): + if entry[0].stmt == "assert": + stmt = stmt.split("assert")[-1].strip() # Extract the assertion statement + type = "assert" + elif entry[0].stmt == "assume": + stmt = stmt.split("assume")[-1].strip() # Extract the assumption statement + type = "assume" + elif entry[0].stmt == "invariant": + stmt = stmt.split("invariant")[-1].strip() # Extract the invariant statement + type = "invariant" + else: + raise ValueError(f"Unknown type of AnalysisCommand: {entry[0].stmt}") + # else: + # raise ValueError(f"Unknown type of instruction: {entry[0]}") + + # Extract variables from the statement + stmt_vars = re.findall(r':([a-zA-Z_][a-zA-Z0-9_]*)', stmt) + + # Replace special variables with their internal representations + for var in stmt_vars: + if var == "TURTLEX": + stmt = re.sub(rf':{var}\b', f':__turtleX', stmt) + var = f"__turtleX" + if var == "TURTLEY": + stmt = re.sub(rf':{var}\b', f':__turtleY', stmt) + var = f"__turtleY" + if var == "TURTLEANGLE": + stmt = re.sub(rf':{var}\b', f':__turtleW', stmt) + var = f"__turtleW" + if var == "TURTLEPEN": + stmt = re.sub(rf':{var}\b', f':__turtleZ', stmt) + var = f"__turtleZ" + if var == "REPCOUNTER": + stmt = re.sub(rf':{var}\b', f':__rep_counter_1', stmt) + var = f"__rep_counter_1" + + # Append the block ID to the variable for uniqueness + stmt = re.sub(rf':{var}\b', f':{var}_{block_id}', stmt) + + # Append the processed instruction to the new instruction list + new_instrlist.append([stmt, type]) + + # print(f"Block ID: {block_id}") # Debugging print for the block ID + # print(f"New Instruction List: {new_instrlist}") # Debugging print for the new instruction list + + # Update the node's instruction list with the processed instructions + node.instrlist = new_instrlist + return + +def process_bb2(node, successors): + """ + Processes a basic block to handle variable renaming across its successors. + + Args: + node (ChironCFG.BasicBlock): The current basic block being processed. + successors (list): A list of successor nodes of the current basic block. + + Returns: + None + + Explanation: + - This function ensures that variables used in successor nodes are properly renamed + to maintain consistency and uniqueness across the control flow graph (CFG). + - It uses the `rename_map` of the current node to determine the latest version of each variable. + - For each successor node, it identifies variables used without assignment and generates + new assignment statements to propagate the correct variable values. + + Steps: + 1. Retrieve the `rename_map` of the current node to track variable versions. + 2. Iterate through each successor node. + 3. For each successor, identify variables used without assignment. + 4. Generate new assignment statements to propagate the correct variable values. + 5. Append the new assignment statements to the instruction list of the current node. + 6. Update the `instrlist` of the current node with the modified instruction list. + """ + new_instrlist = node.instrlist # Get the instruction list of the current node + block_id = node.irID # Get the block ID of the current node + + # Retrieve the rename map for the current node + rename_map = node_to_rename_map[node] + primary_var_to_id = {} # Map to store the latest version of each primary variable + + # Populate the primary variable to ID map from the rename map + for var, id in rename_map.items(): + primary_var = "_".join(var.split("_")[0:-1]) # Extract the primary variable name + primary_var_to_id[primary_var] = id + + # Iterate through each successor node + for succ in successors: + if succ.irID <= block_id: + continue # Skip successors with a lower or equal block ID + + # Process each instruction in the successor's instruction list + for entry in succ.instrlist: + stmt = str(entry[0]) # Convert the instruction to a string + + # If the instruction is an assignment, extract variables from the RHS + if entry[1] == "assign": + vars = extract_variables_assign(stmt) + stmt = vars[1] # Use the RHS expression for further processing + + # Find all variables used in the statement without assignment + stmt_vars = re.findall(r'(:[a-zA-Z_][a-zA-Z0-9_]*_0)', stmt) + for var in stmt_vars: + primary_var = "_".join(var.split("_")[0:-2]) # Extract the primary variable name + + # Generate a new assignment statement to propagate the correct variable value + if primary_var in primary_var_to_id: + new_stmt = f"{primary_var}_{succ.irID}_0 = {primary_var}_{block_id}_{primary_var_to_id[primary_var]}" + else: + new_stmt = f"{primary_var}_{succ.irID}_0 = {primary_var}_{block_id}_0" + + # Create a new entry for the assignment statement + new_entry = [new_stmt, "assign"] + + # Append the new entry to the instruction list if it doesn't already exist + if new_entry not in new_instrlist: + new_instrlist.append([new_stmt, "assign"]) + + # Update the instruction list of the current node + node.instrlist = new_instrlist + return + +def process_bb3(node): + """ + Processes a basic block to extract assignment statements and the condition. + + Args: + node (ChironCFG.BasicBlock): The basic block to process. + + Returns: + tuple: A tuple containing: + - new_instrlist (list): A list of assignment statements extracted from the block. + - condition (str or None): The condition statement if present, otherwise None. + + Explanation: + - This function iterates through the instructions in the basic block. + - It separates assignment statements and identifies the condition statement, if any. + - The extracted assignments are stored in `new_instrlist`, and the condition is stored in `condition`. + """ + new_instrlist = [] # List to store assignment statements + condition = None # Variable to store the condition statement + + # Iterate through the instructions in the block + for entry in node.instrlist: + if entry[1] == "assign": + # Add assignment statements to the list + new_instrlist.append(entry[0]) + elif entry[1] == "condition": + # Set the condition statement + condition = entry[0] + + # Return the extracted assignments and condition + return new_instrlist, condition + +""" +A dictionary that maps block types (e.g., "assume", "assert", "invariant", "loop condition") +to their corresponding nodes in the control flow graph (CFG). +This is used to identify and access specific blocks in the CFG based on their type. +""" +block_type_to_node = {} + +""" +A dictionary that maps nodes in the CFG to their variable rename maps. +Each node's rename map tracks the latest version of variables within that node. +""" +node_to_rename_map = {} + +def check_cfg_format_with_loop(cfg: ChironCFG.ChironCFG): + """ + Verifies the format and structure of a control flow graph (CFG) for programs with loops. + + Args: + cfg (ChironCFG.ChironCFG): The control flow graph to check. + + Returns: + None + + Explanation: + - This function ensures that the CFG contains all required blocks: assume, assert, invariant, and loop condition. + - It validates the presence of these blocks and ensures their positions and relationships in the CFG are correct. + - It also checks for duplicate blocks of the same type and raises errors if the CFG format is invalid. + + Steps: + 1. Iterate through all nodes in the CFG to identify and classify blocks (assume, assert, invariant, loop condition). + 2. Ensure that there is exactly one block of each required type. + 3. Validate the positions and relationships of the blocks in the CFG. + 4. Check for unexpected or invalid statements in the blocks. + 5. Ensure that the loop condition and loop end are correctly defined and connected. + + Raises: + ValueError: If the CFG is missing required blocks, contains duplicate blocks, or has invalid relationships or statements. + """ + nodes_list = list(cfg.nxgraph.nodes) # Get the list of nodes in the CFG + + """ + Check if all required blocks are present: assume, assert, invariant, loop condition + """ + for node in nodes_list: + instrList = node.instrlist # Get the instruction list for the current node + + # Classify blocks based on their type + for entry in instrList: + if entry[1] == "assume": + if "assume" in block_type_to_node.keys(): + raise ValueError(f"More than one assume statement is not allowed") + else: + block_type_to_node["assume"] = node + + elif entry[1] == "assert": + if "assert" in block_type_to_node.keys(): + raise ValueError(f"More than one assert statement is not allowed") + else: + block_type_to_node["assert"] = node + + elif entry[1] == "invariant": + if "invariant" in block_type_to_node.keys(): + raise ValueError(f"More than one invariant statement is not allowed") + else: + block_type_to_node["invariant"] = node + + # Identify the loop condition block based on its predecessors and successors + predecessors = list(cfg.predecessors(node)) + successors = list(cfg.successors(node)) + + if len(predecessors) == 2 and len(successors) == 2: + if predecessors[0].irID > node.irID or predecessors[1].irID > node.irID: + if "loop condition" in block_type_to_node.keys(): + raise ValueError(f"More than one loop is not allowed") + else: + block_type_to_node["loop condition"] = node + + # Ensure all required blocks are present + if "assume" not in block_type_to_node.keys(): + raise ValueError("Assume statement is missing") + if "assert" not in block_type_to_node.keys(): + raise ValueError("Assert statement is missing") + if "invariant" not in block_type_to_node.keys(): + raise ValueError("Invariant statement is missing") + if "loop condition" not in block_type_to_node.keys(): + raise ValueError("Loop condition is missing") + + """ + Check if the positions of blocks in the CFG and the format of individual blocks are correct + """ + assume_node = block_type_to_node["assume"] + assert_node = block_type_to_node["assert"] + invariant_node = block_type_to_node["invariant"] + loop_condition_node = block_type_to_node["loop condition"] + + # Validate the assume block + if assume_node.irID != 0 or assume_node.instrlist[0][1] != "assume": + raise ValueError("Assume statement should be the first statement") + if len(assume_node.instrlist) > 2: + raise ValueError("Unexpected statement(s) after assume") + if assume_node not in cfg.predecessors(loop_condition_node): + raise ValueError("Loop condition should have assume as predecessor") + if loop_condition_node not in cfg.successors(assume_node): + raise ValueError("Assume should have loop condition as successor") + + # Validate the invariant block + if invariant_node not in cfg.successors(loop_condition_node) or invariant_node.instrlist[0][1] != "invariant": + raise ValueError("Loop body should start with invariant") + + # Validate the assert block + if assert_node not in cfg.successors(loop_condition_node): + raise ValueError("Assert should be after the loop body ends") + if len(assert_node.instrlist) > 1: + raise ValueError("Unexpected statement(s) after assert") + + # Validate the loop condition block + if len(loop_condition_node.instrlist) > 1: + raise ValueError("Unexpected statement(s) after loop condition") + if "__rep_counter_1_1 > 0" not in loop_condition_node.instrlist[0][0]: + raise ValueError(f"Invalid Loop condition: {loop_condition_node.instrlist[0][0]}") + + # Identify the loop end block + for pred in cfg.predecessors(loop_condition_node): + if pred.irID != 0: + for entry in pred.instrlist: + if (f"__rep_counter_1_{pred.irID}" in entry[0]) and (entry[1] == "assign"): + block_type_to_node["loop end"] = pred + break + + # Ensure the loop end block is present + if "loop end" not in block_type_to_node.keys(): + raise ValueError("Could not find loop end statement") + + return + +def check_cfg_format_without_loop(cfg: ChironCFG.ChironCFG): + """ + Verifies the format and structure of a control flow graph (CFG) for programs without loops. + + Args: + cfg (ChironCFG.ChironCFG): The control flow graph to check. + + Returns: + None + + Explanation: + - This function ensures that the CFG contains the required blocks: assume and assert. + - It validates the presence of these blocks and ensures their positions and relationships in the CFG are correct. + - It also checks for duplicate blocks of the same type and raises errors if the CFG format is invalid. + + Steps: + 1. Iterate through all nodes in the CFG to identify and classify blocks (assume, assert). + 2. Ensure that there is exactly one block of each required type. + 3. Validate the positions and relationships of the blocks in the CFG. + 4. Check for unexpected or invalid statements in the blocks. + + Raises: + ValueError: If the CFG is missing required blocks, contains duplicate blocks, or has invalid relationships or statements. + """ + nodes_list = list(cfg.nxgraph.nodes) # Get the list of nodes in the CFG + + """ + Check if all required blocks are present: assume, assert + """ + for node in nodes_list: + instrList = node.instrlist # Get the instruction list for the current node + + # Classify blocks based on their type + for entry in instrList: + if entry[1] == "assume": + if "assume" in block_type_to_node.keys(): + raise ValueError(f"More than one assume statement is not allowed") + else: + block_type_to_node["assume"] = node + + elif entry[1] == "assert": + if "assert" in block_type_to_node.keys(): + raise ValueError(f"More than one assert statement is not allowed") + else: + block_type_to_node["assert"] = node + + # Ensure all required blocks are present + if "assume" not in block_type_to_node.keys(): + raise ValueError("Assume statement is missing") + if "assert" not in block_type_to_node.keys(): + raise ValueError("Assert statement is missing") + + """ + Check if the positions of blocks in the CFG and the format of individual blocks are correct + """ + assume_node = block_type_to_node["assume"] + assert_node = block_type_to_node["assert"] + + # Validate the assume block + if assume_node.irID != 0 or assume_node.instrlist[0][1] != "assume": + raise ValueError("Assume statement should be the first statement") + + # Validate the assert block + for succ in cfg.successors(assert_node): + if succ.irID != float('inf'): + raise ValueError("Assert should be the last statement") + if assert_node.instrlist[-1][1] != "assert": + raise ValueError("Assert statement should be the last statement") + + return + +def process_and_rename_nodes(sorted_nodes): + """ + Processes and renames variables in the instruction lists of nodes in the control flow graph (CFG). + + Args: + sorted_nodes (list): A list of nodes in the CFG, sorted by their `irID`. + + Returns: + None + + Explanation: + - This function iterates through the sorted nodes of the CFG and renames variables in their instruction lists. + - It skips the "END" node as it does not require processing. + - For each node, the `rename_vars` function is called to rename variables in the instruction list. + - The renamed instruction list is then updated in the node, and the rename map for the node is stored in `node_to_rename_map`. + """ + for node in sorted_nodes: + if node.name == "END": + continue # Skip END node as it does not require processing + + # Rename variables in the instruction list of the current node + node_to_rename_map[node], new_instrlist = rename_vars(node.instrlist) + + # Update the node's instruction list with the renamed instructions + node.instrlist = new_instrlist + +def extract_and_replace_variables(stmt, block_type, target_block_type): + """ + Extracts variables from a statement and replaces their block-specific suffixes. + + Args: + stmt (str): The statement to process. + block_type (str): The source block type (e.g., "invariant", "loop condition"). + target_block_type (str): The target block type (e.g., "assert"). + + Returns: + str: The updated statement with replaced variables. + """ + stmt_vars = extract_variables_others(stmt) + for var in stmt_vars: + primary_var = "_".join(var.split("_")[0:-1]) + stmt = re.sub(rf'{primary_var}_{block_type_to_node[block_type].irID}\b', + f'{primary_var}_{block_type_to_node[target_block_type].irID}', stmt) + return stmt + +def TraverseCFG(cfg: ChironCFG.ChironCFG, has_loop: bool = True): + """ + Traverses and processes the control flow graph (CFG) to extract preconditions, postconditions, + and other relevant information for programs with or without loops. + + Args: + cfg (ChironCFG.ChironCFG): The control flow graph to process. + has_loop (bool): Indicates whether the CFG contains a loop. + + Returns: + tuple: Extracted preconditions, postconditions, and other relevant information. + + Explanation: + - This function processes the CFG by assigning special IDs to nodes, sorting them, and processing them. + - For CFGs with loops, it validates the CFG format, extracts loop-related information, and processes nodes. + - For CFGs without loops, it validates the CFG format and extracts preconditions, postconditions, and code body. + """ + # Assign special irID values for START and END nodes + for node in cfg.nxgraph.nodes: + if node.name == "START": + node.irID = 0 # Assign 0 to the START node + elif node.name == "END": + node.irID = float('inf') # Assign infinity to the END node + + # Sort nodes by irID in ascending order + sorted_nodes = sorted(cfg.nxgraph.nodes, key=lambda node: node.irID) + + # Process nodes in sorted order + for node in sorted_nodes: + if node.name == "END": + continue # Skip processing for the END node + process_bb1(node) # Process the basic block + + if has_loop: + # Check CFG format for loops + check_cfg_format_with_loop(cfg) + + # Extract and replace variables for invariant and loop condition + stmt1 = block_type_to_node["invariant"].instrlist[0][0] + stmt1 = extract_and_replace_variables(stmt1, "invariant", "assert") + + stmt2 = block_type_to_node["loop condition"].instrlist[0][0] + stmt2 = extract_and_replace_variables(stmt2, "loop condition", "assert") + stmt2 = stmt2.replace(">", "==") # Replace ">" with "==" for loop false condition + + # Add extra statements to the assert block + extra_stmts = [[stmt1, "invariant_out"], [stmt2, "loop_false_condition"]] + block_type_to_node["assert"].instrlist = extra_stmts + block_type_to_node["assert"].instrlist + + stmt = block_type_to_node["loop condition"].instrlist[0][0] + stmt = extract_and_replace_variables(stmt, "loop condition", "invariant") + block_type_to_node["loop condition"].instrlist[0][0] = stmt # Update the loop condition statement + + # Rename variables in nodes + process_and_rename_nodes(sorted_nodes) + + # Process nodes for further renaming and linking + for node in sorted_nodes[::-1]: + if (node.irID > block_type_to_node["loop end"].irID) or \ + (node.irID <= block_type_to_node["loop condition"].irID): + continue # Skip nodes outside the loop range + successors = list(cfg.nxgraph.successors(node)) + if node == block_type_to_node["loop end"]: + successors.append(block_type_to_node["assert"]) # Add assert block as a successor + process_bb2(node, successors) + + # Process the assume block with its successors + process_bb2( + block_type_to_node["assume"], + [block_type_to_node["invariant"], block_type_to_node["loop condition"]], + ) + + # Extract preconditions, postconditions, and loop-related information + pre_condition = [] + post_condition = [] + loop_condition = [] + invariant_in = [] + invariant_out = [] + loop_body = [] + loop_false_condition = [] + + # Extract preconditions from the assume block + for stmt in block_type_to_node["assume"].instrlist: + pre_condition.append(stmt[0]) + + # Extract postconditions from the assert block + for stmt in block_type_to_node["assert"].instrlist: + if stmt[1] == "assert": + post_condition.append(stmt[0]) + + # Extract loop condition statements + for stmt in block_type_to_node["loop condition"].instrlist: + loop_condition.append(stmt[0]) + + # Extract invariant input + invariant_in.append(block_type_to_node["invariant"].instrlist[0][0]) + + # Extract invariant output and loop false condition + for stmt in block_type_to_node["assert"].instrlist: + if stmt[1] == "invariant_out": + invariant_out.append(stmt[0]) + if stmt[1] == "loop_false_condition": + loop_false_condition.append(stmt[0]) + + # Process nodes to extract loop body + node_to_stmt_list = {} + for node in sorted_nodes: + if (node.irID > block_type_to_node["loop end"].irID) or \ + (node.irID <= block_type_to_node["loop condition"].irID): + continue # Skip nodes outside the loop range + new_instrlist, condition = process_bb3(node) + node_to_stmt_list[node] = [new_instrlist, condition] + + # Build the loop body + visited = set() + for node in sorted_nodes: + if (node.irID > block_type_to_node["loop end"].irID) or \ + (node.irID <= block_type_to_node["loop condition"].irID) or \ + (node in visited): + continue # Skip nodes outside the loop range or already visited + instrList, condition = node_to_stmt_list[node] + loop_body.append(["assign", instrList]) # Add assignments to the loop body + visited.add(node) + if condition is not None: + # Process if-else conditions in the loop body + successors = sorted(list(cfg.nxgraph.successors(node)), key=lambda x: x.irID) + instrList1 = node_to_stmt_list[successors[0]][0] + instrList2 = node_to_stmt_list[successors[1]][0] + loop_body.append(["if-else", condition, instrList1, instrList2]) + visited.add(successors[0]) + visited.add(successors[1]) + + # Return extracted information for loops + return pre_condition, post_condition, loop_condition, invariant_in, invariant_out, loop_body, loop_false_condition + + else: + # Check CFG format for programs without loops + check_cfg_format_without_loop(cfg) + + # Rename variables in nodes + process_and_rename_nodes(sorted_nodes) + + # Process nodes for further renaming and linking + for node in sorted_nodes[::-1]: + if node.name == "END": + continue # Skip the END node + successors = list(cfg.nxgraph.successors(node)) + process_bb2(node, successors) + + # Extract preconditions, postconditions, and code body + pre_condition = [] + post_condition = [] + code_body = [] + + # Process nodes to extract statements and conditions + node_to_stmt_list = {} + for node in sorted_nodes: + if node.name == "END": + continue # Skip the END node + new_instrlist, condition = process_bb3(node) + node_to_stmt_list[node] = [new_instrlist, condition] + + # Extract preconditions from the assume block + for stmt in block_type_to_node["assume"].instrlist: + if stmt[1] == "assume": + pre_condition.append(stmt[0]) + + # Extract postconditions from the assert block + for stmt in block_type_to_node["assert"].instrlist: + if stmt[1] == "assert": + post_condition.append(stmt[0]) + + # Build the code body + visited = set() + for node in sorted_nodes: + if node.name == "END" or (node in visited): + continue # Skip the END node or already visited nodes + instrList, condition = node_to_stmt_list[node] + code_body.append(["assign", instrList]) # Add assignments to the code body + visited.add(node) + if condition is not None: + # Process if-else conditions in the code body + successors = sorted(list(cfg.nxgraph.successors(node)), key=lambda x: x.irID) + instrList1 = node_to_stmt_list[successors[0]][0] + instrList2 = node_to_stmt_list[successors[1]][0] + code_body.append(["if-else", condition, instrList1, instrList2]) + visited.add(successors[0]) + visited.add(successors[1]) + + # Return extracted information for programs without loops + return pre_condition, post_condition, code_body + diff --git a/ChironCore/ProofEngine/TurtleCommandsCompiler.py b/ChironCore/ProofEngine/TurtleCommandsCompiler.py new file mode 100644 index 0000000..2b6d366 --- /dev/null +++ b/ChironCore/ProofEngine/TurtleCommandsCompiler.py @@ -0,0 +1,178 @@ +from ChironAST import ChironAST + +class TurtleCommandsCompiler(): + """ + A compiler for Turtle commands that translates high-level commands into low-level + ChironAST commands for execution. + + Attributes: + x (ChironAST.Var): Represents the x-coordinate of the turtle. + y (ChironAST.Var): Represents the y-coordinate of the turtle. + z (ChironAST.Var): Represents the pen status of the turtle (up or down). + w (ChironAST.Var): Represents the direction/angle of the turtle. + """ + + def __init__(self): + """ + Initializes the TurtleCommandsCompiler with variables representing the turtle's state. + """ + self.x = ChironAST.Var(":__turtleX") + self.y = ChironAST.Var(":__turtleY") + self.z = ChironAST.Var(":__turtleZ") + self.w = ChironAST.Var(":__turtleW") + + def compile_move_command(self, command: ChironAST.MoveCommand): + """ + Compiles a MoveCommand into ChironAST commands. + + Args: + command (ChironAST.MoveCommand): The move command to compile. + + Returns: + list: A list of ChironAST commands representing the move operation. + """ + new_command = ChironAST.NoOpCommand() # Default to a no-op command + + # Handle left turn + if(command.direction == "left"): + lexpr = self.w + rexpr = ChironAST.Sum(self.w, command.expr) + num = ChironAST.Num(360) + rexpr = ChironAST.Mod(rexpr, num) # Ensure the angle stays within 0-360 + new_command = ChironAST.AssignmentCommand(lexpr, rexpr) + + # Handle right turn + if(command.direction == "right"): + lexpr = self.w + rexpr = ChironAST.Diff(self.w, command.expr) + num = ChironAST.Num(360) + rexpr = ChironAST.Mod(rexpr, num) # Ensure the angle stays within 0-360 + new_command = ChironAST.AssignmentCommand(lexpr, rexpr) + + # Handle forward movement + if(command.direction == "forward"): + commands = [] + + # Calculate the new x and y coordinates based on the direction + n = ChironAST.Div(self.w, ChironAST.Num(90)) # Determine the quadrant + n_mod2 = ChironAST.Mod(n, ChironAST.Num(2)) + n_div2 = ChironAST.Div(n, ChironAST.Num(2)) + term2 = ChironAST.Diff(ChironAST.Num(1), ChironAST.Mult(ChironAST.Num(2), n_div2)) + term1 = ChironAST.Diff(ChironAST.Num(1), n_mod2) + + # Update x-coordinate + commands.append( + ChironAST.AssignmentCommand( + self.x, + ChironAST.Sum( + self.x, + ChironAST.Mult(command.expr, ChironAST.Mult(term1, term2)) + ) + ) + ) + + # Update y-coordinate + commands.append( + ChironAST.AssignmentCommand( + self.y, + ChironAST.Sum( + self.y, + ChironAST.Mult(command.expr, ChironAST.Mult(n_mod2, term2)) + ) + ) + ) + return commands + + # Handle backward movement + if(command.direction == "backward"): + commands = [] + + # Calculate the new x and y coordinates based on the direction + n = ChironAST.Div(self.w, ChironAST.Num(90)) # Determine the quadrant + n_mod2 = ChironAST.Mod(n, ChironAST.Num(2)) + n_div2 = ChironAST.Div(n, ChironAST.Num(2)) + term2 = ChironAST.Diff(ChironAST.Mult(ChironAST.Num(2), n_div2), ChironAST.Num(1)) + term1 = ChironAST.Diff(ChironAST.Num(1), n_mod2) + + # Update x-coordinate + commands.append( + ChironAST.AssignmentCommand( + self.x, + ChironAST.Sum( + self.x, + ChironAST.Mult(command.expr, ChironAST.Mult(term1, term2)) + ) + ) + ) + + # Update y-coordinate + commands.append( + ChironAST.AssignmentCommand( + self.y, + ChironAST.Sum( + self.y, + ChironAST.Mult(command.expr, ChironAST.Mult(n_mod2, term2)) + ) + ) + ) + return commands + + return [new_command] + + def compile_goto_command(self, command: ChironAST.GotoCommand): + """ + Compiles a GotoCommand into ChironAST commands. + + Args: + command (ChironAST.GotoCommand): The goto command to compile. + + Returns: + list: A list of ChironAST commands to set the turtle's x and y coordinates. + """ + new_command1 = ChironAST.AssignmentCommand(self.x, command.xcor) # Set x-coordinate + new_command2 = ChironAST.AssignmentCommand(self.y, command.ycor) # Set y-coordinate + return [new_command1, new_command2] + + def compile_pen_command(self, command: ChironAST.PenCommand): + """ + Compiles a PenCommand into ChironAST commands. + + Args: + command (ChironAST.PenCommand): The pen command to compile. + + Returns: + list: A list of ChironAST commands to update the pen status. + """ + new_penstat = 0 if command.status == 'pendown' else 1 # Map pen status to 0 or 1 + new_penstat = ChironAST.Num(new_penstat) + new_command = ChironAST.AssignmentCommand(self.z, new_penstat) # Update pen status + return [new_command] + + def compile(self, command): + """ + Compiles a generic command into ChironAST commands. + + Args: + command: The command to compile. + + Returns: + list: A list of ChironAST commands representing the compiled command. + """ + # Handle NoOpCommand + if (type(command) == ChironAST.NoOpCommand): + return [] + + # Handle MoveCommand + if(type(command) == ChironAST.MoveCommand): + return self.compile_move_command(command) + + # Handle GotoCommand + if(type(command) == ChironAST.GotoCommand): + return self.compile_goto_command(command) + + # Handle PenCommand + if(type(command) == ChironAST.PenCommand): + return self.compile_pen_command(command) + + # Return the command as-is if no specific compilation is required + return [command] diff --git a/ChironCore/ProofEngine/Z3Integration.py b/ChironCore/ProofEngine/Z3Integration.py new file mode 100644 index 0000000..fd0579c --- /dev/null +++ b/ChironCore/ProofEngine/Z3Integration.py @@ -0,0 +1,143 @@ +import subprocess +import os +import re + +def Z3Solver(smtlib_code): + """ + Executes Z3 with the given SMT-LIB code string and processes the output. + + Args: + smtlib_code (str): The SMT-LIB code to be solved by Z3. + + Returns: + str: A formatted string containing the verification results and counterexamples (if any). + + Explanation: + - This function writes the SMT-LIB code to a temporary file and runs Z3 as a subprocess. + - It processes the Z3 output to determine whether the conditions are verified or not. + - If a condition fails, it extracts the counterexample and formats it for output. + - The function handles both single-condition and multi-condition verification scenarios. + """ + # Write the SMT-LIB code to a temporary file + temp_file = "temp.smt2" + with open(temp_file, "w") as f: + f.write(smtlib_code) + + # Run Z3 as a subprocess + try: + result = subprocess.run(['z3', temp_file], capture_output=True, text=True) + + # Clean up the temporary file + os.remove(temp_file) + + # Process the Z3 output + results, models = split_sat_blocks_and_extract_models(result.stdout) + + output = "" + if(len(results) == 3): # Handle multi-condition verification (e.g., Initialization, Loop, Final) + conditions = ["Initialization", "Loop", "Final"] + + for i, condition in enumerate(conditions): + if results[i] == "unsat": + output += f"{condition} Condition verified :)\n" + elif results[i] == "sat": + output += f"{condition} Condition verification failed :(\n" + output += "Counterexample:\n" + for var, val in models[i].items(): + output += f"{var} : {val}\n" + output += "\n" + + elif len(results) == 1: # Handle single-condition verification + if results[0] == "unsat": + output += "Condition verified :)\n" + elif results[0] == "sat": + output += "Condition verification failed :(\n" + output += "Counterexample:\n" + for var, val in models[0].items(): + output += f"{var} : {val}\n" + output += "\n" + + # Add a note if any condition fails + if "sat" in results: + output += "Please refer to \"control_flow_graph.png\" for variable names.\n" + return output + + except FileNotFoundError: + # Handle the case where Z3 is not installed or not in the PATH + os.remove(temp_file) + raise RuntimeError("Error: Z3 is not installed or not in PATH. Try running `z3 -h` to check.") + + +def split_sat_blocks_and_extract_models(input_string): + """ + Splits the Z3 output into blocks based on "sat" and "unsat" results and extracts models for "sat" blocks. + + Args: + input_string (str): The raw output from Z3. + + Returns: + tuple: A tuple containing: + - results (list): A list of "sat" or "unsat" results for each block. + - sat_models (list): A list of models (dictionaries) for "sat" blocks or "UNSAT" for "unsat" blocks. + + Explanation: + - This function parses the Z3 output to separate "sat" and "unsat" blocks. + - For "sat" blocks, it extracts variable assignments (models) from the output. + - Each model is represented as a dictionary mapping variable names to their values. + """ + # Split the input into lines + lines = input_string.strip().splitlines() + + results = [] # List to store "sat" or "unsat" results + blocks = [] # List to store corresponding blocks of output + + current_block = [] # Temporary storage for the current block + current_result = None # Temporary storage for the current result ("sat" or "unsat") + + # Iterate through each line of the Z3 output + for line in lines: + line = line.strip() + if line == "sat" or line == "unsat": # Check for result indicators + if current_result is not None: + # Store the previous result and block + results.append(current_result) + blocks.append(current_block) + current_block = [] # Reset the current block + current_result = line # Update the current result + else: + # Add the line to the current block + current_block.append(line) + + # Add the last result and block (if any) + if current_result is not None: + results.append(current_result) + blocks.append(current_block) + + # Extract variables from "sat" blocks + sat_models = [] + for result, block in zip(results, blocks): + if result == "sat": # Process "sat" blocks to extract models + model = {} + i = 0 + while i < len(block): + line = block[i] + # Match variable definitions in the block + match = re.match(r"\(define-fun (\S+) \(\) Int", line) + if match and i + 1 < len(block): + var_name = match.group(1) # Extract the variable name + value_line = block[i + 1].strip(" )") # Extract the value + + # Normalize negative numbers + if value_line.startswith("(-"): + value_line = "-" + value_line[3:].strip(" )") + + model[var_name] = value_line # Add the variable and its value to the model + i += 2 # Skip the next line as it's already processed + else: + i += 1 # Move to the next line + sat_models.append(model) # Add the model to the list of models + else: + sat_models.append("UNSAT") # Add "UNSAT" for unsat blocks + + return results, sat_models + diff --git a/ChironCore/ProofEngine/examples/arithmetic_progression.tl b/ChironCore/ProofEngine/examples/arithmetic_progression.tl new file mode 100644 index 0000000..7c6e424 --- /dev/null +++ b/ChironCore/ProofEngine/examples/arithmetic_progression.tl @@ -0,0 +1,7 @@ +assume(:s==0 && :i==:a) +repeat :n [ + invariant(:s == (((:n-:REPCOUNTER)*(2*:a + (:n-:REPCOUNTER-1)*:d))/2) && (:i == :a + (:n-:REPCOUNTER)*:d) ) + :s = :s + :i + :i = :i + :d +] +assert(:s == ((:n*(2*:a + (:n-1)*:d))/2)) \ No newline at end of file diff --git a/ChironCore/ProofEngine/examples/cube.tl b/ChironCore/ProofEngine/examples/cube.tl new file mode 100644 index 0000000..410a4e4 --- /dev/null +++ b/ChironCore/ProofEngine/examples/cube.tl @@ -0,0 +1,4 @@ +assume(1==1) +:c1 = :a*:a*:a - 3*:a*:a*:b + 3*:a*:b*:b - :b*:b*:b +:c2 = (:a-:b)*(:a-:b)*(:a-:b) +assert(:c1 == :c2) \ No newline at end of file diff --git a/ChironCore/ProofEngine/examples/cube_buggy.tl b/ChironCore/ProofEngine/examples/cube_buggy.tl new file mode 100644 index 0000000..67334eb --- /dev/null +++ b/ChironCore/ProofEngine/examples/cube_buggy.tl @@ -0,0 +1,4 @@ +assume(1==1) +:c1 = :a*:a*:a - 3*:a*:a*:b - 3*:a*:b*:b + :b*:b*:b +:c2 = (:a-:b)*(:a-:b)*(:a-:b) +assert(:c1 == :c2) \ No newline at end of file diff --git a/ChironCore/ProofEngine/examples/home.tl b/ChironCore/ProofEngine/examples/home.tl new file mode 100644 index 0000000..f2c8255 --- /dev/null +++ b/ChironCore/ProofEngine/examples/home.tl @@ -0,0 +1,38 @@ +assume(:xstart <= 150 && :ystart <= 150 && :xstart >= -150 && :ystart >= -150 && :TURTLEX == :xstart && :TURTLEY == :ystart && :TURTLEANGLE == 0 && :step == 10 && :TURTLEPEN == 1 && :n >= 0 && :outgone == 0) +repeat 5 [ + invariant( + ( + (:TURTLEX <= 200 && :TURTLEX >= -200 && :TURTLEY <= 200 && :TURTLEY >= -200 && :outgone == 0) || ((:TURTLEX > 200 || :TURTLEX < -200 || :TURTLEY > 200 || :TURTLEY < -200) && :outgone == 1) + ) && + + (:TURTLEX == :xstart+10*(:REPCOUNTER-5) && :TURTLEY == :ystart+10*(:REPCOUNTER-5) && :step == 110-20*:REPCOUNTER && :TURTLEANGLE == 0 && :TURTLEPEN == 1 && :step > 0 && :xstart <= 150 && :ystart <= 150 && :xstart >= -150 && :ystart >= -150) + ) + pendown + forward :step + if(:TURTLEX > 200 || :TURTLEX < -200 || :TURTLEY > 200 || :TURTLEY < -200)[ + :outgone = 1 + ] + left 90 + forward :step + if(:TURTLEX > 200 || :TURTLEX < -200 || :TURTLEY > 200 || :TURTLEY < -200)[ + :outgone = 1 + ] + left 90 + :step = :step + 10 + forward :step + if(:TURTLEX > 200 || :TURTLEX < -200 || :TURTLEY > 200 || :TURTLEY < -200)[ + :outgone = 1 + ] + left 90 + forward :step + if(:TURTLEX > 200 || :TURTLEX < -200 || :TURTLEY > 200 || :TURTLEY < -200)[ + :outgone = 1 + ] + left 90 + :step = :step + 10 + if(:TURTLEX > 200 || :TURTLEX < -200 || :TURTLEY > 200 || :TURTLEY < -200)[ + :outgone = 1 + ] + penup +] +assert(:outgone != 1) \ No newline at end of file diff --git a/ChironCore/ProofEngine/examples/home_src.tl b/ChironCore/ProofEngine/examples/home_src.tl new file mode 100644 index 0000000..ac20ecf --- /dev/null +++ b/ChironCore/ProofEngine/examples/home_src.tl @@ -0,0 +1,42 @@ +:step = 10 + +penup +goto (-150, -150) +pendown +forward 300 +left 90 +forward 300 +left 90 +forward 300 +left 90 +forward 300 +left 90 + +penup +goto (-200, -200) +pendown +forward 400 +left 90 +forward 400 +left 90 +forward 400 +left 90 +forward 400 +left 90 + +penup +goto (:xstart, :ystart) +repeat 5 [ + pendown + forward :step + left 90 + forward :step + left 90 + :step = :step + 10 + forward :step + left 90 + forward :step + left 90 + :step = :step + 10 + penup +] \ No newline at end of file diff --git a/ChironCore/ProofEngine/examples/leapyear.tl b/ChironCore/ProofEngine/examples/leapyear.tl new file mode 100644 index 0000000..ef7edce --- /dev/null +++ b/ChironCore/ProofEngine/examples/leapyear.tl @@ -0,0 +1,31 @@ +assume(:year > 0) +:mod4 = (:year-1) - ((:year-1)/4)*4 +:mod100 = (:year-1) - ((:year-1)/100)*100 +:mod400 = (:year-1) - ((:year-1)/400)*400 +:isLeap1 = (:mod4+1)/4 - (:mod100+1)/100 + (:mod400+1)/400 + +:mod4n = :year - (:year/4)*4 +:mod100n = :year - (:year/100)*100 +:mod400n = :year - (:year/400)*400 + +if (:mod4n == 0) [ + :isDivby4 = 1 +] else [ + :isDivby4 = 0 +] +if (:mod100n == 0) [ + :isDivby100 = 1 +] else [ + :isDivby100 = 0 +] +if (:mod400n == 0)[ + :isDivby400 = 1 +] else [ + :isDivby400 = 0 +] +if ((:isDivby4 == 1 && :isDivby100 != 1) || (:isDivby400 == 1)) [ + :isLeap2 = 1 +] else [ + :isLeap2 = 0 +] +assert(:isLeap1 == :isLeap2) \ No newline at end of file diff --git a/ChironCore/ProofEngine/examples/park.tl b/ChironCore/ProofEngine/examples/park.tl new file mode 100644 index 0000000..371a748 --- /dev/null +++ b/ChironCore/ProofEngine/examples/park.tl @@ -0,0 +1,9 @@ +assume(:xstart <= 100 && :ystart <= 100 && :xstart >= -100 && :ystart >= -100 && :TURTLEX == :xstart && :TURTLEY == :ystart && :TURTLEANGLE == 0 && :step == 50) +repeat 10 [ + invariant (:TURTLEX == :xstart+50*(10-:REPCOUNTER) && :TURTLEY == :ystart+50*(10-:REPCOUNTER) && :step == 50 && :TURTLEANGLE == 0 && :xstart <= 100 && :ystart <= 100 && :xstart >= -100 && :ystart >= -100) + forward :step + left 90 + forward :step + right 90 +] +assert((:TURTLEX <= 600 && :TURTLEX >= 400) && (:TURTLEY <=600 && :TURTLEY >= 400) && :TURTLEANGLE==0 && :xstart <= 100 && :ystart <= 100 && :xstart >= -100 && :ystart >= -100) \ No newline at end of file diff --git a/ChironCore/ProofEngine/examples/park_src.tl b/ChironCore/ProofEngine/examples/park_src.tl new file mode 100644 index 0000000..233295f --- /dev/null +++ b/ChironCore/ProofEngine/examples/park_src.tl @@ -0,0 +1,35 @@ +penup +goto (-50,-50) +pendown +forward 100 +left 90 +forward 100 +left 90 +forward 100 +left 90 +forward 100 +left 90 + +penup +goto (200,200) +pendown +forward 100 +left 90 +forward 100 +left 90 +forward 100 +left 90 +forward 100 +left 90 +penup + +:step = 25 + +goto (13,-30) +pendown +repeat 10 [ + forward :step + left 90 + forward :step + right 90 +] \ No newline at end of file diff --git a/ChironCore/ProofEngine/examples/river.tl b/ChironCore/ProofEngine/examples/river.tl new file mode 100644 index 0000000..bf26df3 --- /dev/null +++ b/ChironCore/ProofEngine/examples/river.tl @@ -0,0 +1,45 @@ +assume(:i==1 && :TURTLEPEN==0 && :xstart==0 && :ystart==40 && :TURTLEANGLE==0 && :TURTLEX==:xstart && :TURTLEY==:ystart && :inriver==0) +repeat :n[ + invariant(:TURTLEX==:xstart+30*(:n-:REPCOUNTER) && :TURTLEY==:ystart+30*(:n-:REPCOUNTER) && :TURTLEPEN==0 && :i==1 && :TURTLEANGLE==0 && :inriver == 0 && :xstart == 0 && :ystart == 40) + penup + forward 40 + right 90 + forward 40 + pendown + forward :i*15 + if(:TURTLEX==:TURTLEY)[ + :inriver = 1 + ] + :i = :i +1 + penup + forward 40 + right 90 + forward 40 + pendown + forward :i*15 + if(:TURTLEX==:TURTLEY)[ + :inriver = 1 + ] + :i = :i +1 + penup + forward 40 + right 90 + forward 40 + pendown + forward :i*15 + if(:TURTLEX==:TURTLEY)[ + :inriver = 1 + ] + :i = :i +1 + penup + forward 40 + right 90 + forward 40 + pendown + forward :i*15 + if(:TURTLEX==:TURTLEY)[ + :inriver = 1 + ] + :i = 1 +] +assert(:inriver==0) \ No newline at end of file diff --git a/ChironCore/ProofEngine/examples/river_src.tl b/ChironCore/ProofEngine/examples/river_src.tl new file mode 100644 index 0000000..ee764b8 --- /dev/null +++ b/ChironCore/ProofEngine/examples/river_src.tl @@ -0,0 +1,32 @@ +:i = 1 +:n = 10 +repeat :n[ + penup + forward 40 + right 90 + forward 40 + pendown + forward :i*15 + :i = :i +1 + penup + forward 40 + right 90 + forward 40 + pendown + forward :i*15 + :i = :i +1 + penup + forward 40 + right 90 + forward 40 + pendown + forward :i*15 + :i = :i +1 + penup + forward 40 + right 90 + forward 40 + pendown + forward :i*15 + :i = 1 +] \ No newline at end of file diff --git a/ChironCore/ProofEngine/examples/run_images/home_in.png b/ChironCore/ProofEngine/examples/run_images/home_in.png new file mode 100644 index 0000000..a7dcfa5 Binary files /dev/null and b/ChironCore/ProofEngine/examples/run_images/home_in.png differ diff --git a/ChironCore/ProofEngine/examples/run_images/home_out.png b/ChironCore/ProofEngine/examples/run_images/home_out.png new file mode 100644 index 0000000..96ce13a Binary files /dev/null and b/ChironCore/ProofEngine/examples/run_images/home_out.png differ diff --git a/ChironCore/ProofEngine/examples/run_images/park.png b/ChironCore/ProofEngine/examples/run_images/park.png new file mode 100644 index 0000000..6444e98 Binary files /dev/null and b/ChironCore/ProofEngine/examples/run_images/park.png differ diff --git a/ChironCore/ProofEngine/examples/run_images/river.png b/ChironCore/ProofEngine/examples/run_images/river.png new file mode 100644 index 0000000..75f5e7f Binary files /dev/null and b/ChironCore/ProofEngine/examples/run_images/river.png differ diff --git a/ChironCore/ProofEngine/examples/run_images/spiral_in.png b/ChironCore/ProofEngine/examples/run_images/spiral_in.png new file mode 100644 index 0000000..8108ddb Binary files /dev/null and b/ChironCore/ProofEngine/examples/run_images/spiral_in.png differ diff --git a/ChironCore/ProofEngine/examples/run_images/spiral_out.png b/ChironCore/ProofEngine/examples/run_images/spiral_out.png new file mode 100644 index 0000000..5c6ad73 Binary files /dev/null and b/ChironCore/ProofEngine/examples/run_images/spiral_out.png differ diff --git a/ChironCore/ProofEngine/examples/signum.tl b/ChironCore/ProofEngine/examples/signum.tl new file mode 100644 index 0000000..a4fc837 --- /dev/null +++ b/ChironCore/ProofEngine/examples/signum.tl @@ -0,0 +1,10 @@ +assume(1==1) +if (:x > 0)[ + :sign = 1 +] else [ + :sign = 0 +] +if (:x < 0)[ + :sign = -1 +] +assert((:x > 0 && :sign == 1) || (:x < 0 && :sign < 0) || (:x == 0 && :sign == 0)) \ No newline at end of file diff --git a/ChironCore/ProofEngine/examples/signum_buggy.tl b/ChironCore/ProofEngine/examples/signum_buggy.tl new file mode 100644 index 0000000..ddda7c1 --- /dev/null +++ b/ChironCore/ProofEngine/examples/signum_buggy.tl @@ -0,0 +1,7 @@ +assume(1==1) +if (:x > 0)[ + :sign = 1 +] else [ + :sign = -1 +] +assert((:x > 0 && :sign == 1) || (:x < 0 && :sign == -1) || (:x == 0 && :sign == 0)) diff --git a/ChironCore/ProofEngine/examples/sort.tl b/ChironCore/ProofEngine/examples/sort.tl new file mode 100644 index 0000000..7367cd7 --- /dev/null +++ b/ChironCore/ProofEngine/examples/sort.tl @@ -0,0 +1,17 @@ +assume(1==1) +if (:x > :y)[ + :t = :x + :x = :y + :y = :t +] +if (:y > :z)[ + :t = :y + :y = :z + :z = :t +] +if (:x > :y)[ + :t = :x + :x = :y + :y = :t +] +assert((:x <= :y) && (:y <= :z)) \ No newline at end of file diff --git a/ChironCore/ProofEngine/examples/sort_buggy.tl b/ChironCore/ProofEngine/examples/sort_buggy.tl new file mode 100644 index 0000000..2aa1581 --- /dev/null +++ b/ChironCore/ProofEngine/examples/sort_buggy.tl @@ -0,0 +1,17 @@ +assume(1==1) +if (:x > :y)[ + :t = :x + :x = :y + :y = :t +] +if (:y > :z)[ + :t = :y + :y = :z + :z = :t +] +if (:x > :z)[ + :t = :x + :x = :z + :z = :t +] +assert((:x <= :y) && (:y <= :z)) \ No newline at end of file diff --git a/ChironCore/ProofEngine/examples/spiral.tl b/ChironCore/ProofEngine/examples/spiral.tl new file mode 100644 index 0000000..fc29f3f --- /dev/null +++ b/ChironCore/ProofEngine/examples/spiral.tl @@ -0,0 +1,17 @@ +assume(:TURTLEX == 0 && :TURTLEY == 0 && :TURTLEANGLE == 0 && :step == 1 && :TURTLEPEN == 1 && :n >= 0) +repeat :n [ + invariant(:TURTLEX == :REPCOUNTER-:n && :TURTLEY == :REPCOUNTER-:n && (:step == ((2*:n) + 1)-2*:REPCOUNTER) && :TURTLEANGLE == 0 && :TURTLEPEN == 1 && :step > 0) + pendown + forward :step + left 90 + forward :step + left 90 + :step = :step + 1 + forward :step + left 90 + forward :step + left 90 + :step = :step + 1 + penup +] +assert(:TURTLEX<:n+1 && :TURTLEX>-:n-1 && :TURTLEY<(:n+1) && :TURTLEY>(-:n-1) && :TURTLEPEN == 1 && :TURTLEANGLE == 0 && :step == ((2*:n) + 1)) \ No newline at end of file diff --git a/ChironCore/ProofEngine/examples/spiral_src.tl b/ChironCore/ProofEngine/examples/spiral_src.tl new file mode 100644 index 0000000..5c0b84c --- /dev/null +++ b/ChironCore/ProofEngine/examples/spiral_src.tl @@ -0,0 +1,30 @@ +:step = 40 + +penup +goto (-230, -230) +pendown +forward 460 +left 90 +forward 460 +left 90 +forward 460 +left 90 +forward 460 +left 90 + +penup +goto (0,0) +repeat :n [ + pendown + forward :step + left 90 + forward :step + left 90 + :step = :step + 40 + forward :step + left 90 + forward :step + left 90 + :step = :step + 40 + penup +] \ No newline at end of file diff --git a/ChironCore/ProofEngine/requirements.txt b/ChironCore/ProofEngine/requirements.txt new file mode 100644 index 0000000..fb454e4 --- /dev/null +++ b/ChironCore/ProofEngine/requirements.txt @@ -0,0 +1 @@ +z3-solver==4.13.4.0 diff --git a/ChironCore/chiron.py b/ChironCore/chiron.py index 2eca801..5d36249 100755 --- a/ChironCore/chiron.py +++ b/ChironCore/chiron.py @@ -2,13 +2,16 @@ Release = "Chiron v1.0.4" import ast +import re import sys from ChironAST.builder import astGenPass + import abstractInterpretation as AI import dataFlowAnalysis as DFA from sbfl import testsuiteGenerator sys.path.insert(0, "../Submission/") +sys.path.insert(0, "../ProofEngine/") sys.path.insert(0, "ChironAST/") sys.path.insert(0, "cfg/") @@ -26,6 +29,12 @@ from sbflSubmission import computeRanks import csv +from ProofEngine.Z3Integration import Z3Solver +from ProofEngine.TraverseCFG import TraverseCFG +from ProofEngine.Smtlib_Helper import generate_cfg_and_ir +from ProofEngine.Smtlib_Helper import list_to_smtlib_stmt +from ProofEngine.Smtlib_Helper import generate_smtlib_code +from ProofEngine.Smtlib_Helper import generate_code_body def cleanup(): pass @@ -35,6 +44,7 @@ def stopTurtle(): turtle.bye() + if __name__ == "__main__": print(Release) print( @@ -195,6 +205,13 @@ def stopTurtle(): default=True, type=bool, ) + cmdparser.add_argument( + "-smt", + "--smtlib", + help="Generate code for SMT-LIB generation", + action="store_true" + ) + args = cmdparser.parse_args() ir = "" @@ -219,7 +236,7 @@ def stopTurtle(): # generate control_flow_graph from IR statements. if args.control_flow: - cfg = cfgB.buildCFG(ir, "control_flow_graph", True) + cfg = cfgB.buildCFG(ir, "control_flow_graph", False) irHandler.setCFG(cfg) else: irHandler.setCFG(None) @@ -392,3 +409,89 @@ def stopTurtle(): writer = csv.writer(file) writer.writerows(spectrum) print("DONE..") + + if args.smtlib: + """ + Parse the program and generate CFG and IR + """ + cfg, num_loops = generate_cfg_and_ir(parseTree, irHandler) + + """ + Handle programs with or without loops + """ + if num_loops > 1: + """ + Raise an error if the program contains more than one loop. + This version of Chiron only supports programs with a single loop + when using the --smtlib/-smt flag. + """ + raise RuntimeError("This version of Chiron only supports programs with a single loop with --smtlib/-smt flag.") + elif num_loops == 0: + """ + Handle programs without loops: + - Traverse the CFG to extract pre-conditions, post-conditions, and the code body. + - Dump the CFG for visualization or debugging. + - Convert the extracted conditions and code body into SMT-LIB format. + """ + pre_condition_list, post_condition_list, code_body_list = TraverseCFG(cfg, has_loop=False) + cfgB.dumpCFG(cfg, "control_flow_graph") + + # Convert pre-condition and post-condition lists to SMT-LIB format + pre_condition = list_to_smtlib_stmt(pre_condition_list) + post_condition = list_to_smtlib_stmt(post_condition_list) + + # Generate the SMT-LIB code body from the code body list + code_body = generate_code_body(code_body_list) + + # Debugging prints for conditions and code body + # print("Pre-condition: ", pre_condition) + # print("Post-condition: ", post_condition) + # print("Code-body: ", code_body) + + # Generate SMT-LIB code for the program without loops + smtlib_code = generate_smtlib_code(pre_condition, post_condition, loop_body=code_body) + + elif num_loops == 1: + """ + Handle programs with a single loop: + - Traverse the CFG to extract pre-conditions, post-conditions, loop conditions, + invariants, loop body, and loop false conditions. + - Dump the CFG for visualization or debugging. + - Convert the extracted conditions and loop body into SMT-LIB format. + """ + pre_condition_list, post_condition_list, loop_condition_list, invariant_in_list, invariant_out_list, loop_body_list, loop_false_condition_list = TraverseCFG(cfg, has_loop=True) + cfgB.dumpCFG(cfg, "control_flow_graph") + + # Convert pre-condition, post-condition, and loop-related conditions to SMT-LIB format + pre_condition = list_to_smtlib_stmt(pre_condition_list) + post_condition = list_to_smtlib_stmt(post_condition_list) + loop_condition = list_to_smtlib_stmt(loop_condition_list) + invariant_in = list_to_smtlib_stmt(invariant_in_list) + invariant_out = list_to_smtlib_stmt(invariant_out_list) + loop_false_condition = list_to_smtlib_stmt(loop_false_condition_list) + + # Generate the SMT-LIB loop body from the loop body list + loop_body = generate_code_body(loop_body_list) + + # Debugging prints for conditions and loop body + # print("Pre-condition: ", pre_condition) + # print("Post-condition: ", post_condition) + # print("Loop-condition: ", loop_condition) + # print("Invariant-in: ", invariant_in) + # print("Invariant-out: ", invariant_out) + # print("Loop-false-condition: ", loop_false_condition) + # print("Loop-body: ", loop_body) + + # Generate SMT-LIB code for the program with a loop + smtlib_code = generate_smtlib_code(pre_condition, post_condition, loop_condition, invariant_in, invariant_out, loop_body, loop_false_condition) + + """ + Solve the SMT-LIB code using Z3 and print the output. + """ + # print(smtlib_code) # Debugging print for the generated SMT-LIB code + output = Z3Solver(smtlib_code) + print("\n======Z3 Output:======\n") + print(output) + + + diff --git a/ChironCore/control_flow_graph.png b/ChironCore/control_flow_graph.png new file mode 100644 index 0000000..ef31ea7 Binary files /dev/null and b/ChironCore/control_flow_graph.png differ diff --git a/ChironCore/example/control_flow_graph.png b/ChironCore/example/control_flow_graph.png deleted file mode 100644 index 4560280..0000000 Binary files a/ChironCore/example/control_flow_graph.png and /dev/null differ diff --git a/ChironCore/turtparse/tlang.g4 b/ChironCore/turtparse/tlang.g4 index ff3a2f6..31986af 100644 --- a/ChironCore/turtparse/tlang.g4 +++ b/ChironCore/turtparse/tlang.g4 @@ -17,6 +17,7 @@ instruction : assignment | penCommand | gotoCommand | pauseCommand + | analysisCommand ; conditional : ifConditional | ifElseConditional ; @@ -39,6 +40,9 @@ penCommand : 'penup' | 'pendown' ; pauseCommand : 'pause' ; +analysisCommand : analysisStatement '(' condition ')' ; +analysisStatement : 'assert' | 'invariant' | 'assume' ; + expression : unaryArithOp expression #unaryExpr | expression multiplicative expression #mulExpr @@ -47,7 +51,7 @@ expression : | '(' expression ')' #parenExpr ; -multiplicative : MUL | DIV; +multiplicative : MUL | DIV | MOD; additive : PLUS | MINUS; unaryArithOp : MINUS ; @@ -56,6 +60,7 @@ PLUS : '+' ; MINUS : '-' ; MUL : '*' ; DIV : '/' ; +MOD : '%' ; // TODO : diff --git a/ChironCore/turtparse/tlang.interp b/ChironCore/turtparse/tlang.interp index f3cba53..de481bf 100644 --- a/ChironCore/turtparse/tlang.interp +++ b/ChironCore/turtparse/tlang.interp @@ -17,10 +17,14 @@ null 'penup' 'pendown' 'pause' +'assert' +'invariant' +'assume' '+' '-' '*' '/' +'%' 'pendown?' '<' '>' @@ -55,10 +59,14 @@ null null null null +null +null +null PLUS MINUS MUL DIV +MOD PENCOND LT GT @@ -89,6 +97,8 @@ moveCommand moveOp penCommand pauseCommand +analysisCommand +analysisStatement expression multiplicative additive @@ -100,4 +110,4 @@ value atn: -[3, 24715, 42794, 33075, 47597, 16764, 15335, 30598, 22884, 3, 37, 175, 4, 2, 9, 2, 4, 3, 9, 3, 4, 4, 9, 4, 4, 5, 9, 5, 4, 6, 9, 6, 4, 7, 9, 7, 4, 8, 9, 8, 4, 9, 9, 9, 4, 10, 9, 10, 4, 11, 9, 11, 4, 12, 9, 12, 4, 13, 9, 13, 4, 14, 9, 14, 4, 15, 9, 15, 4, 16, 9, 16, 4, 17, 9, 17, 4, 18, 9, 18, 4, 19, 9, 19, 4, 20, 9, 20, 4, 21, 9, 21, 4, 22, 9, 22, 4, 23, 9, 23, 3, 2, 3, 2, 3, 2, 3, 3, 7, 3, 51, 10, 3, 12, 3, 14, 3, 54, 11, 3, 3, 4, 6, 4, 57, 10, 4, 13, 4, 14, 4, 58, 3, 5, 3, 5, 3, 5, 3, 5, 3, 5, 3, 5, 3, 5, 5, 5, 68, 10, 5, 3, 6, 3, 6, 5, 6, 72, 10, 6, 3, 7, 3, 7, 3, 7, 3, 7, 3, 7, 3, 7, 3, 8, 3, 8, 3, 8, 3, 8, 3, 8, 3, 8, 3, 8, 3, 8, 3, 8, 3, 8, 3, 9, 3, 9, 3, 9, 3, 9, 3, 9, 3, 9, 3, 10, 3, 10, 3, 10, 3, 10, 3, 10, 3, 10, 3, 10, 3, 11, 3, 11, 3, 11, 3, 11, 3, 12, 3, 12, 3, 12, 3, 13, 3, 13, 3, 14, 3, 14, 3, 15, 3, 15, 3, 16, 3, 16, 3, 16, 3, 16, 3, 16, 3, 16, 3, 16, 3, 16, 3, 16, 5, 16, 125, 10, 16, 3, 16, 3, 16, 3, 16, 3, 16, 3, 16, 3, 16, 3, 16, 3, 16, 7, 16, 135, 10, 16, 12, 16, 14, 16, 138, 11, 16, 3, 17, 3, 17, 3, 18, 3, 18, 3, 19, 3, 19, 3, 20, 3, 20, 3, 20, 3, 20, 3, 20, 3, 20, 3, 20, 3, 20, 3, 20, 3, 20, 3, 20, 3, 20, 5, 20, 158, 10, 20, 3, 20, 3, 20, 3, 20, 3, 20, 7, 20, 164, 10, 20, 12, 20, 14, 20, 167, 11, 20, 3, 21, 3, 21, 3, 22, 3, 22, 3, 23, 3, 23, 3, 23, 2, 4, 30, 38, 24, 2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38, 40, 42, 44, 2, 9, 3, 2, 13, 16, 3, 2, 17, 18, 3, 2, 22, 23, 3, 2, 20, 21, 3, 2, 25, 30, 3, 2, 31, 32, 3, 2, 34, 35, 2, 169, 2, 46, 3, 2, 2, 2, 4, 52, 3, 2, 2, 2, 6, 56, 3, 2, 2, 2, 8, 67, 3, 2, 2, 2, 10, 71, 3, 2, 2, 2, 12, 73, 3, 2, 2, 2, 14, 79, 3, 2, 2, 2, 16, 89, 3, 2, 2, 2, 18, 95, 3, 2, 2, 2, 20, 102, 3, 2, 2, 2, 22, 106, 3, 2, 2, 2, 24, 109, 3, 2, 2, 2, 26, 111, 3, 2, 2, 2, 28, 113, 3, 2, 2, 2, 30, 124, 3, 2, 2, 2, 32, 139, 3, 2, 2, 2, 34, 141, 3, 2, 2, 2, 36, 143, 3, 2, 2, 2, 38, 157, 3, 2, 2, 2, 40, 168, 3, 2, 2, 2, 42, 170, 3, 2, 2, 2, 44, 172, 3, 2, 2, 2, 46, 47, 5, 4, 3, 2, 47, 48, 7, 2, 2, 3, 48, 3, 3, 2, 2, 2, 49, 51, 5, 8, 5, 2, 50, 49, 3, 2, 2, 2, 51, 54, 3, 2, 2, 2, 52, 50, 3, 2, 2, 2, 52, 53, 3, 2, 2, 2, 53, 5, 3, 2, 2, 2, 54, 52, 3, 2, 2, 2, 55, 57, 5, 8, 5, 2, 56, 55, 3, 2, 2, 2, 57, 58, 3, 2, 2, 2, 58, 56, 3, 2, 2, 2, 58, 59, 3, 2, 2, 2, 59, 7, 3, 2, 2, 2, 60, 68, 5, 20, 11, 2, 61, 68, 5, 10, 6, 2, 62, 68, 5, 16, 9, 2, 63, 68, 5, 22, 12, 2, 64, 68, 5, 26, 14, 2, 65, 68, 5, 18, 10, 2, 66, 68, 5, 28, 15, 2, 67, 60, 3, 2, 2, 2, 67, 61, 3, 2, 2, 2, 67, 62, 3, 2, 2, 2, 67, 63, 3, 2, 2, 2, 67, 64, 3, 2, 2, 2, 67, 65, 3, 2, 2, 2, 67, 66, 3, 2, 2, 2, 68, 9, 3, 2, 2, 2, 69, 72, 5, 12, 7, 2, 70, 72, 5, 14, 8, 2, 71, 69, 3, 2, 2, 2, 71, 70, 3, 2, 2, 2, 72, 11, 3, 2, 2, 2, 73, 74, 7, 3, 2, 2, 74, 75, 5, 38, 20, 2, 75, 76, 7, 4, 2, 2, 76, 77, 5, 6, 4, 2, 77, 78, 7, 5, 2, 2, 78, 13, 3, 2, 2, 2, 79, 80, 7, 3, 2, 2, 80, 81, 5, 38, 20, 2, 81, 82, 7, 4, 2, 2, 82, 83, 5, 6, 4, 2, 83, 84, 7, 5, 2, 2, 84, 85, 7, 6, 2, 2, 85, 86, 7, 4, 2, 2, 86, 87, 5, 6, 4, 2, 87, 88, 7, 5, 2, 2, 88, 15, 3, 2, 2, 2, 89, 90, 7, 7, 2, 2, 90, 91, 5, 44, 23, 2, 91, 92, 7, 4, 2, 2, 92, 93, 5, 6, 4, 2, 93, 94, 7, 5, 2, 2, 94, 17, 3, 2, 2, 2, 95, 96, 7, 8, 2, 2, 96, 97, 7, 9, 2, 2, 97, 98, 5, 30, 16, 2, 98, 99, 7, 10, 2, 2, 99, 100, 5, 30, 16, 2, 100, 101, 7, 11, 2, 2, 101, 19, 3, 2, 2, 2, 102, 103, 7, 35, 2, 2, 103, 104, 7, 12, 2, 2, 104, 105, 5, 30, 16, 2, 105, 21, 3, 2, 2, 2, 106, 107, 5, 24, 13, 2, 107, 108, 5, 30, 16, 2, 108, 23, 3, 2, 2, 2, 109, 110, 9, 2, 2, 2, 110, 25, 3, 2, 2, 2, 111, 112, 9, 3, 2, 2, 112, 27, 3, 2, 2, 2, 113, 114, 7, 19, 2, 2, 114, 29, 3, 2, 2, 2, 115, 116, 8, 16, 1, 2, 116, 117, 5, 36, 19, 2, 117, 118, 5, 30, 16, 7, 118, 125, 3, 2, 2, 2, 119, 125, 5, 44, 23, 2, 120, 121, 7, 9, 2, 2, 121, 122, 5, 30, 16, 2, 122, 123, 7, 11, 2, 2, 123, 125, 3, 2, 2, 2, 124, 115, 3, 2, 2, 2, 124, 119, 3, 2, 2, 2, 124, 120, 3, 2, 2, 2, 125, 136, 3, 2, 2, 2, 126, 127, 12, 6, 2, 2, 127, 128, 5, 32, 17, 2, 128, 129, 5, 30, 16, 7, 129, 135, 3, 2, 2, 2, 130, 131, 12, 5, 2, 2, 131, 132, 5, 34, 18, 2, 132, 133, 5, 30, 16, 6, 133, 135, 3, 2, 2, 2, 134, 126, 3, 2, 2, 2, 134, 130, 3, 2, 2, 2, 135, 138, 3, 2, 2, 2, 136, 134, 3, 2, 2, 2, 136, 137, 3, 2, 2, 2, 137, 31, 3, 2, 2, 2, 138, 136, 3, 2, 2, 2, 139, 140, 9, 4, 2, 2, 140, 33, 3, 2, 2, 2, 141, 142, 9, 5, 2, 2, 142, 35, 3, 2, 2, 2, 143, 144, 7, 21, 2, 2, 144, 37, 3, 2, 2, 2, 145, 146, 8, 20, 1, 2, 146, 147, 7, 33, 2, 2, 147, 158, 5, 38, 20, 7, 148, 149, 5, 30, 16, 2, 149, 150, 5, 40, 21, 2, 150, 151, 5, 30, 16, 2, 151, 158, 3, 2, 2, 2, 152, 158, 7, 24, 2, 2, 153, 154, 7, 9, 2, 2, 154, 155, 5, 38, 20, 2, 155, 156, 7, 11, 2, 2, 156, 158, 3, 2, 2, 2, 157, 145, 3, 2, 2, 2, 157, 148, 3, 2, 2, 2, 157, 152, 3, 2, 2, 2, 157, 153, 3, 2, 2, 2, 158, 165, 3, 2, 2, 2, 159, 160, 12, 5, 2, 2, 160, 161, 5, 42, 22, 2, 161, 162, 5, 38, 20, 6, 162, 164, 3, 2, 2, 2, 163, 159, 3, 2, 2, 2, 164, 167, 3, 2, 2, 2, 165, 163, 3, 2, 2, 2, 165, 166, 3, 2, 2, 2, 166, 39, 3, 2, 2, 2, 167, 165, 3, 2, 2, 2, 168, 169, 9, 6, 2, 2, 169, 41, 3, 2, 2, 2, 170, 171, 9, 7, 2, 2, 171, 43, 3, 2, 2, 2, 172, 173, 9, 8, 2, 2, 173, 45, 3, 2, 2, 2, 11, 52, 58, 67, 71, 124, 134, 136, 157, 165] \ No newline at end of file +[3, 24715, 42794, 33075, 47597, 16764, 15335, 30598, 22884, 3, 41, 187, 4, 2, 9, 2, 4, 3, 9, 3, 4, 4, 9, 4, 4, 5, 9, 5, 4, 6, 9, 6, 4, 7, 9, 7, 4, 8, 9, 8, 4, 9, 9, 9, 4, 10, 9, 10, 4, 11, 9, 11, 4, 12, 9, 12, 4, 13, 9, 13, 4, 14, 9, 14, 4, 15, 9, 15, 4, 16, 9, 16, 4, 17, 9, 17, 4, 18, 9, 18, 4, 19, 9, 19, 4, 20, 9, 20, 4, 21, 9, 21, 4, 22, 9, 22, 4, 23, 9, 23, 4, 24, 9, 24, 4, 25, 9, 25, 3, 2, 3, 2, 3, 2, 3, 3, 7, 3, 55, 10, 3, 12, 3, 14, 3, 58, 11, 3, 3, 4, 6, 4, 61, 10, 4, 13, 4, 14, 4, 62, 3, 5, 3, 5, 3, 5, 3, 5, 3, 5, 3, 5, 3, 5, 3, 5, 5, 5, 73, 10, 5, 3, 6, 3, 6, 5, 6, 77, 10, 6, 3, 7, 3, 7, 3, 7, 3, 7, 3, 7, 3, 7, 3, 8, 3, 8, 3, 8, 3, 8, 3, 8, 3, 8, 3, 8, 3, 8, 3, 8, 3, 8, 3, 9, 3, 9, 3, 9, 3, 9, 3, 9, 3, 9, 3, 10, 3, 10, 3, 10, 3, 10, 3, 10, 3, 10, 3, 10, 3, 11, 3, 11, 3, 11, 3, 11, 3, 12, 3, 12, 3, 12, 3, 13, 3, 13, 3, 14, 3, 14, 3, 15, 3, 15, 3, 16, 3, 16, 3, 16, 3, 16, 3, 16, 3, 17, 3, 17, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 5, 18, 137, 10, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 7, 18, 147, 10, 18, 12, 18, 14, 18, 150, 11, 18, 3, 19, 3, 19, 3, 20, 3, 20, 3, 21, 3, 21, 3, 22, 3, 22, 3, 22, 3, 22, 3, 22, 3, 22, 3, 22, 3, 22, 3, 22, 3, 22, 3, 22, 3, 22, 5, 22, 170, 10, 22, 3, 22, 3, 22, 3, 22, 3, 22, 7, 22, 176, 10, 22, 12, 22, 14, 22, 179, 11, 22, 3, 23, 3, 23, 3, 24, 3, 24, 3, 25, 3, 25, 3, 25, 2, 4, 34, 42, 26, 2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38, 40, 42, 44, 46, 48, 2, 10, 3, 2, 13, 16, 3, 2, 17, 18, 3, 2, 20, 22, 3, 2, 25, 27, 3, 2, 23, 24, 3, 2, 29, 34, 3, 2, 35, 36, 3, 2, 38, 39, 2, 180, 2, 50, 3, 2, 2, 2, 4, 56, 3, 2, 2, 2, 6, 60, 3, 2, 2, 2, 8, 72, 3, 2, 2, 2, 10, 76, 3, 2, 2, 2, 12, 78, 3, 2, 2, 2, 14, 84, 3, 2, 2, 2, 16, 94, 3, 2, 2, 2, 18, 100, 3, 2, 2, 2, 20, 107, 3, 2, 2, 2, 22, 111, 3, 2, 2, 2, 24, 114, 3, 2, 2, 2, 26, 116, 3, 2, 2, 2, 28, 118, 3, 2, 2, 2, 30, 120, 3, 2, 2, 2, 32, 125, 3, 2, 2, 2, 34, 136, 3, 2, 2, 2, 36, 151, 3, 2, 2, 2, 38, 153, 3, 2, 2, 2, 40, 155, 3, 2, 2, 2, 42, 169, 3, 2, 2, 2, 44, 180, 3, 2, 2, 2, 46, 182, 3, 2, 2, 2, 48, 184, 3, 2, 2, 2, 50, 51, 5, 4, 3, 2, 51, 52, 7, 2, 2, 3, 52, 3, 3, 2, 2, 2, 53, 55, 5, 8, 5, 2, 54, 53, 3, 2, 2, 2, 55, 58, 3, 2, 2, 2, 56, 54, 3, 2, 2, 2, 56, 57, 3, 2, 2, 2, 57, 5, 3, 2, 2, 2, 58, 56, 3, 2, 2, 2, 59, 61, 5, 8, 5, 2, 60, 59, 3, 2, 2, 2, 61, 62, 3, 2, 2, 2, 62, 60, 3, 2, 2, 2, 62, 63, 3, 2, 2, 2, 63, 7, 3, 2, 2, 2, 64, 73, 5, 20, 11, 2, 65, 73, 5, 10, 6, 2, 66, 73, 5, 16, 9, 2, 67, 73, 5, 22, 12, 2, 68, 73, 5, 26, 14, 2, 69, 73, 5, 18, 10, 2, 70, 73, 5, 28, 15, 2, 71, 73, 5, 30, 16, 2, 72, 64, 3, 2, 2, 2, 72, 65, 3, 2, 2, 2, 72, 66, 3, 2, 2, 2, 72, 67, 3, 2, 2, 2, 72, 68, 3, 2, 2, 2, 72, 69, 3, 2, 2, 2, 72, 70, 3, 2, 2, 2, 72, 71, 3, 2, 2, 2, 73, 9, 3, 2, 2, 2, 74, 77, 5, 12, 7, 2, 75, 77, 5, 14, 8, 2, 76, 74, 3, 2, 2, 2, 76, 75, 3, 2, 2, 2, 77, 11, 3, 2, 2, 2, 78, 79, 7, 3, 2, 2, 79, 80, 5, 42, 22, 2, 80, 81, 7, 4, 2, 2, 81, 82, 5, 6, 4, 2, 82, 83, 7, 5, 2, 2, 83, 13, 3, 2, 2, 2, 84, 85, 7, 3, 2, 2, 85, 86, 5, 42, 22, 2, 86, 87, 7, 4, 2, 2, 87, 88, 5, 6, 4, 2, 88, 89, 7, 5, 2, 2, 89, 90, 7, 6, 2, 2, 90, 91, 7, 4, 2, 2, 91, 92, 5, 6, 4, 2, 92, 93, 7, 5, 2, 2, 93, 15, 3, 2, 2, 2, 94, 95, 7, 7, 2, 2, 95, 96, 5, 48, 25, 2, 96, 97, 7, 4, 2, 2, 97, 98, 5, 6, 4, 2, 98, 99, 7, 5, 2, 2, 99, 17, 3, 2, 2, 2, 100, 101, 7, 8, 2, 2, 101, 102, 7, 9, 2, 2, 102, 103, 5, 34, 18, 2, 103, 104, 7, 10, 2, 2, 104, 105, 5, 34, 18, 2, 105, 106, 7, 11, 2, 2, 106, 19, 3, 2, 2, 2, 107, 108, 7, 39, 2, 2, 108, 109, 7, 12, 2, 2, 109, 110, 5, 34, 18, 2, 110, 21, 3, 2, 2, 2, 111, 112, 5, 24, 13, 2, 112, 113, 5, 34, 18, 2, 113, 23, 3, 2, 2, 2, 114, 115, 9, 2, 2, 2, 115, 25, 3, 2, 2, 2, 116, 117, 9, 3, 2, 2, 117, 27, 3, 2, 2, 2, 118, 119, 7, 19, 2, 2, 119, 29, 3, 2, 2, 2, 120, 121, 5, 32, 17, 2, 121, 122, 7, 9, 2, 2, 122, 123, 5, 42, 22, 2, 123, 124, 7, 11, 2, 2, 124, 31, 3, 2, 2, 2, 125, 126, 9, 4, 2, 2, 126, 33, 3, 2, 2, 2, 127, 128, 8, 18, 1, 2, 128, 129, 5, 40, 21, 2, 129, 130, 5, 34, 18, 7, 130, 137, 3, 2, 2, 2, 131, 137, 5, 48, 25, 2, 132, 133, 7, 9, 2, 2, 133, 134, 5, 34, 18, 2, 134, 135, 7, 11, 2, 2, 135, 137, 3, 2, 2, 2, 136, 127, 3, 2, 2, 2, 136, 131, 3, 2, 2, 2, 136, 132, 3, 2, 2, 2, 137, 148, 3, 2, 2, 2, 138, 139, 12, 6, 2, 2, 139, 140, 5, 36, 19, 2, 140, 141, 5, 34, 18, 7, 141, 147, 3, 2, 2, 2, 142, 143, 12, 5, 2, 2, 143, 144, 5, 38, 20, 2, 144, 145, 5, 34, 18, 6, 145, 147, 3, 2, 2, 2, 146, 138, 3, 2, 2, 2, 146, 142, 3, 2, 2, 2, 147, 150, 3, 2, 2, 2, 148, 146, 3, 2, 2, 2, 148, 149, 3, 2, 2, 2, 149, 35, 3, 2, 2, 2, 150, 148, 3, 2, 2, 2, 151, 152, 9, 5, 2, 2, 152, 37, 3, 2, 2, 2, 153, 154, 9, 6, 2, 2, 154, 39, 3, 2, 2, 2, 155, 156, 7, 24, 2, 2, 156, 41, 3, 2, 2, 2, 157, 158, 8, 22, 1, 2, 158, 159, 7, 37, 2, 2, 159, 170, 5, 42, 22, 7, 160, 161, 5, 34, 18, 2, 161, 162, 5, 44, 23, 2, 162, 163, 5, 34, 18, 2, 163, 170, 3, 2, 2, 2, 164, 170, 7, 28, 2, 2, 165, 166, 7, 9, 2, 2, 166, 167, 5, 42, 22, 2, 167, 168, 7, 11, 2, 2, 168, 170, 3, 2, 2, 2, 169, 157, 3, 2, 2, 2, 169, 160, 3, 2, 2, 2, 169, 164, 3, 2, 2, 2, 169, 165, 3, 2, 2, 2, 170, 177, 3, 2, 2, 2, 171, 172, 12, 5, 2, 2, 172, 173, 5, 46, 24, 2, 173, 174, 5, 42, 22, 6, 174, 176, 3, 2, 2, 2, 175, 171, 3, 2, 2, 2, 176, 179, 3, 2, 2, 2, 177, 175, 3, 2, 2, 2, 177, 178, 3, 2, 2, 2, 178, 43, 3, 2, 2, 2, 179, 177, 3, 2, 2, 2, 180, 181, 9, 7, 2, 2, 181, 45, 3, 2, 2, 2, 182, 183, 9, 8, 2, 2, 183, 47, 3, 2, 2, 2, 184, 185, 9, 9, 2, 2, 185, 49, 3, 2, 2, 2, 11, 56, 62, 72, 76, 136, 146, 148, 169, 177] \ No newline at end of file diff --git a/ChironCore/turtparse/tlang.tokens b/ChironCore/turtparse/tlang.tokens index 78f9526..d44a02b 100644 --- a/ChironCore/turtparse/tlang.tokens +++ b/ChironCore/turtparse/tlang.tokens @@ -15,24 +15,28 @@ T__13=14 T__14=15 T__15=16 T__16=17 -PLUS=18 -MINUS=19 -MUL=20 -DIV=21 -PENCOND=22 -LT=23 -GT=24 -EQ=25 -NEQ=26 -LTE=27 -GTE=28 -AND=29 -OR=30 -NOT=31 -NUM=32 -VAR=33 -NAME=34 -Whitespace=35 +T__17=18 +T__18=19 +T__19=20 +PLUS=21 +MINUS=22 +MUL=23 +DIV=24 +MOD=25 +PENCOND=26 +LT=27 +GT=28 +EQ=29 +NEQ=30 +LTE=31 +GTE=32 +AND=33 +OR=34 +NOT=35 +NUM=36 +VAR=37 +NAME=38 +Whitespace=39 'if'=1 '['=2 ']'=3 @@ -50,17 +54,21 @@ Whitespace=35 'penup'=15 'pendown'=16 'pause'=17 -'+'=18 -'-'=19 -'*'=20 -'/'=21 -'pendown?'=22 -'<'=23 -'>'=24 -'=='=25 -'!='=26 -'<='=27 -'>='=28 -'&&'=29 -'||'=30 -'!'=31 +'assert'=18 +'invariant'=19 +'assume'=20 +'+'=21 +'-'=22 +'*'=23 +'/'=24 +'%'=25 +'pendown?'=26 +'<'=27 +'>'=28 +'=='=29 +'!='=30 +'<='=31 +'>='=32 +'&&'=33 +'||'=34 +'!'=35 diff --git a/ChironCore/turtparse/tlangLexer.interp b/ChironCore/turtparse/tlangLexer.interp index 106eae4..aa16b2b 100644 --- a/ChironCore/turtparse/tlangLexer.interp +++ b/ChironCore/turtparse/tlangLexer.interp @@ -17,10 +17,14 @@ null 'penup' 'pendown' 'pause' +'assert' +'invariant' +'assume' '+' '-' '*' '/' +'%' 'pendown?' '<' '>' @@ -55,10 +59,14 @@ null null null null +null +null +null PLUS MINUS MUL DIV +MOD PENCOND LT GT @@ -92,10 +100,14 @@ T__13 T__14 T__15 T__16 +T__17 +T__18 +T__19 PLUS MINUS MUL DIV +MOD PENCOND LT GT @@ -119,4 +131,4 @@ mode names: DEFAULT_MODE atn: -[3, 24715, 42794, 33075, 47597, 16764, 15335, 30598, 22884, 2, 37, 219, 8, 1, 4, 2, 9, 2, 4, 3, 9, 3, 4, 4, 9, 4, 4, 5, 9, 5, 4, 6, 9, 6, 4, 7, 9, 7, 4, 8, 9, 8, 4, 9, 9, 9, 4, 10, 9, 10, 4, 11, 9, 11, 4, 12, 9, 12, 4, 13, 9, 13, 4, 14, 9, 14, 4, 15, 9, 15, 4, 16, 9, 16, 4, 17, 9, 17, 4, 18, 9, 18, 4, 19, 9, 19, 4, 20, 9, 20, 4, 21, 9, 21, 4, 22, 9, 22, 4, 23, 9, 23, 4, 24, 9, 24, 4, 25, 9, 25, 4, 26, 9, 26, 4, 27, 9, 27, 4, 28, 9, 28, 4, 29, 9, 29, 4, 30, 9, 30, 4, 31, 9, 31, 4, 32, 9, 32, 4, 33, 9, 33, 4, 34, 9, 34, 4, 35, 9, 35, 4, 36, 9, 36, 3, 2, 3, 2, 3, 2, 3, 3, 3, 3, 3, 4, 3, 4, 3, 5, 3, 5, 3, 5, 3, 5, 3, 5, 3, 6, 3, 6, 3, 6, 3, 6, 3, 6, 3, 6, 3, 6, 3, 7, 3, 7, 3, 7, 3, 7, 3, 7, 3, 8, 3, 8, 3, 9, 3, 9, 3, 10, 3, 10, 3, 11, 3, 11, 3, 12, 3, 12, 3, 12, 3, 12, 3, 12, 3, 12, 3, 12, 3, 12, 3, 13, 3, 13, 3, 13, 3, 13, 3, 13, 3, 13, 3, 13, 3, 13, 3, 13, 3, 14, 3, 14, 3, 14, 3, 14, 3, 14, 3, 15, 3, 15, 3, 15, 3, 15, 3, 15, 3, 15, 3, 16, 3, 16, 3, 16, 3, 16, 3, 16, 3, 16, 3, 17, 3, 17, 3, 17, 3, 17, 3, 17, 3, 17, 3, 17, 3, 17, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 19, 3, 19, 3, 20, 3, 20, 3, 21, 3, 21, 3, 22, 3, 22, 3, 23, 3, 23, 3, 23, 3, 23, 3, 23, 3, 23, 3, 23, 3, 23, 3, 23, 3, 24, 3, 24, 3, 25, 3, 25, 3, 26, 3, 26, 3, 26, 3, 27, 3, 27, 3, 27, 3, 28, 3, 28, 3, 28, 3, 29, 3, 29, 3, 29, 3, 30, 3, 30, 3, 30, 3, 31, 3, 31, 3, 31, 3, 32, 3, 32, 3, 33, 6, 33, 196, 10, 33, 13, 33, 14, 33, 197, 3, 34, 3, 34, 3, 34, 7, 34, 203, 10, 34, 12, 34, 14, 34, 206, 11, 34, 3, 35, 6, 35, 209, 10, 35, 13, 35, 14, 35, 210, 3, 36, 6, 36, 214, 10, 36, 13, 36, 14, 36, 215, 3, 36, 3, 36, 2, 2, 37, 3, 3, 5, 4, 7, 5, 9, 6, 11, 7, 13, 8, 15, 9, 17, 10, 19, 11, 21, 12, 23, 13, 25, 14, 27, 15, 29, 16, 31, 17, 33, 18, 35, 19, 37, 20, 39, 21, 41, 22, 43, 23, 45, 24, 47, 25, 49, 26, 51, 27, 53, 28, 55, 29, 57, 30, 59, 31, 61, 32, 63, 33, 65, 34, 67, 35, 69, 36, 71, 37, 3, 2, 7, 3, 2, 50, 59, 5, 2, 67, 92, 97, 97, 99, 124, 5, 2, 50, 59, 67, 92, 99, 124, 4, 2, 67, 92, 99, 124, 5, 2, 11, 12, 15, 15, 34, 34, 2, 222, 2, 3, 3, 2, 2, 2, 2, 5, 3, 2, 2, 2, 2, 7, 3, 2, 2, 2, 2, 9, 3, 2, 2, 2, 2, 11, 3, 2, 2, 2, 2, 13, 3, 2, 2, 2, 2, 15, 3, 2, 2, 2, 2, 17, 3, 2, 2, 2, 2, 19, 3, 2, 2, 2, 2, 21, 3, 2, 2, 2, 2, 23, 3, 2, 2, 2, 2, 25, 3, 2, 2, 2, 2, 27, 3, 2, 2, 2, 2, 29, 3, 2, 2, 2, 2, 31, 3, 2, 2, 2, 2, 33, 3, 2, 2, 2, 2, 35, 3, 2, 2, 2, 2, 37, 3, 2, 2, 2, 2, 39, 3, 2, 2, 2, 2, 41, 3, 2, 2, 2, 2, 43, 3, 2, 2, 2, 2, 45, 3, 2, 2, 2, 2, 47, 3, 2, 2, 2, 2, 49, 3, 2, 2, 2, 2, 51, 3, 2, 2, 2, 2, 53, 3, 2, 2, 2, 2, 55, 3, 2, 2, 2, 2, 57, 3, 2, 2, 2, 2, 59, 3, 2, 2, 2, 2, 61, 3, 2, 2, 2, 2, 63, 3, 2, 2, 2, 2, 65, 3, 2, 2, 2, 2, 67, 3, 2, 2, 2, 2, 69, 3, 2, 2, 2, 2, 71, 3, 2, 2, 2, 3, 73, 3, 2, 2, 2, 5, 76, 3, 2, 2, 2, 7, 78, 3, 2, 2, 2, 9, 80, 3, 2, 2, 2, 11, 85, 3, 2, 2, 2, 13, 92, 3, 2, 2, 2, 15, 97, 3, 2, 2, 2, 17, 99, 3, 2, 2, 2, 19, 101, 3, 2, 2, 2, 21, 103, 3, 2, 2, 2, 23, 105, 3, 2, 2, 2, 25, 113, 3, 2, 2, 2, 27, 122, 3, 2, 2, 2, 29, 127, 3, 2, 2, 2, 31, 133, 3, 2, 2, 2, 33, 139, 3, 2, 2, 2, 35, 147, 3, 2, 2, 2, 37, 153, 3, 2, 2, 2, 39, 155, 3, 2, 2, 2, 41, 157, 3, 2, 2, 2, 43, 159, 3, 2, 2, 2, 45, 161, 3, 2, 2, 2, 47, 170, 3, 2, 2, 2, 49, 172, 3, 2, 2, 2, 51, 174, 3, 2, 2, 2, 53, 177, 3, 2, 2, 2, 55, 180, 3, 2, 2, 2, 57, 183, 3, 2, 2, 2, 59, 186, 3, 2, 2, 2, 61, 189, 3, 2, 2, 2, 63, 192, 3, 2, 2, 2, 65, 195, 3, 2, 2, 2, 67, 199, 3, 2, 2, 2, 69, 208, 3, 2, 2, 2, 71, 213, 3, 2, 2, 2, 73, 74, 7, 107, 2, 2, 74, 75, 7, 104, 2, 2, 75, 4, 3, 2, 2, 2, 76, 77, 7, 93, 2, 2, 77, 6, 3, 2, 2, 2, 78, 79, 7, 95, 2, 2, 79, 8, 3, 2, 2, 2, 80, 81, 7, 103, 2, 2, 81, 82, 7, 110, 2, 2, 82, 83, 7, 117, 2, 2, 83, 84, 7, 103, 2, 2, 84, 10, 3, 2, 2, 2, 85, 86, 7, 116, 2, 2, 86, 87, 7, 103, 2, 2, 87, 88, 7, 114, 2, 2, 88, 89, 7, 103, 2, 2, 89, 90, 7, 99, 2, 2, 90, 91, 7, 118, 2, 2, 91, 12, 3, 2, 2, 2, 92, 93, 7, 105, 2, 2, 93, 94, 7, 113, 2, 2, 94, 95, 7, 118, 2, 2, 95, 96, 7, 113, 2, 2, 96, 14, 3, 2, 2, 2, 97, 98, 7, 42, 2, 2, 98, 16, 3, 2, 2, 2, 99, 100, 7, 46, 2, 2, 100, 18, 3, 2, 2, 2, 101, 102, 7, 43, 2, 2, 102, 20, 3, 2, 2, 2, 103, 104, 7, 63, 2, 2, 104, 22, 3, 2, 2, 2, 105, 106, 7, 104, 2, 2, 106, 107, 7, 113, 2, 2, 107, 108, 7, 116, 2, 2, 108, 109, 7, 121, 2, 2, 109, 110, 7, 99, 2, 2, 110, 111, 7, 116, 2, 2, 111, 112, 7, 102, 2, 2, 112, 24, 3, 2, 2, 2, 113, 114, 7, 100, 2, 2, 114, 115, 7, 99, 2, 2, 115, 116, 7, 101, 2, 2, 116, 117, 7, 109, 2, 2, 117, 118, 7, 121, 2, 2, 118, 119, 7, 99, 2, 2, 119, 120, 7, 116, 2, 2, 120, 121, 7, 102, 2, 2, 121, 26, 3, 2, 2, 2, 122, 123, 7, 110, 2, 2, 123, 124, 7, 103, 2, 2, 124, 125, 7, 104, 2, 2, 125, 126, 7, 118, 2, 2, 126, 28, 3, 2, 2, 2, 127, 128, 7, 116, 2, 2, 128, 129, 7, 107, 2, 2, 129, 130, 7, 105, 2, 2, 130, 131, 7, 106, 2, 2, 131, 132, 7, 118, 2, 2, 132, 30, 3, 2, 2, 2, 133, 134, 7, 114, 2, 2, 134, 135, 7, 103, 2, 2, 135, 136, 7, 112, 2, 2, 136, 137, 7, 119, 2, 2, 137, 138, 7, 114, 2, 2, 138, 32, 3, 2, 2, 2, 139, 140, 7, 114, 2, 2, 140, 141, 7, 103, 2, 2, 141, 142, 7, 112, 2, 2, 142, 143, 7, 102, 2, 2, 143, 144, 7, 113, 2, 2, 144, 145, 7, 121, 2, 2, 145, 146, 7, 112, 2, 2, 146, 34, 3, 2, 2, 2, 147, 148, 7, 114, 2, 2, 148, 149, 7, 99, 2, 2, 149, 150, 7, 119, 2, 2, 150, 151, 7, 117, 2, 2, 151, 152, 7, 103, 2, 2, 152, 36, 3, 2, 2, 2, 153, 154, 7, 45, 2, 2, 154, 38, 3, 2, 2, 2, 155, 156, 7, 47, 2, 2, 156, 40, 3, 2, 2, 2, 157, 158, 7, 44, 2, 2, 158, 42, 3, 2, 2, 2, 159, 160, 7, 49, 2, 2, 160, 44, 3, 2, 2, 2, 161, 162, 7, 114, 2, 2, 162, 163, 7, 103, 2, 2, 163, 164, 7, 112, 2, 2, 164, 165, 7, 102, 2, 2, 165, 166, 7, 113, 2, 2, 166, 167, 7, 121, 2, 2, 167, 168, 7, 112, 2, 2, 168, 169, 7, 65, 2, 2, 169, 46, 3, 2, 2, 2, 170, 171, 7, 62, 2, 2, 171, 48, 3, 2, 2, 2, 172, 173, 7, 64, 2, 2, 173, 50, 3, 2, 2, 2, 174, 175, 7, 63, 2, 2, 175, 176, 7, 63, 2, 2, 176, 52, 3, 2, 2, 2, 177, 178, 7, 35, 2, 2, 178, 179, 7, 63, 2, 2, 179, 54, 3, 2, 2, 2, 180, 181, 7, 62, 2, 2, 181, 182, 7, 63, 2, 2, 182, 56, 3, 2, 2, 2, 183, 184, 7, 64, 2, 2, 184, 185, 7, 63, 2, 2, 185, 58, 3, 2, 2, 2, 186, 187, 7, 40, 2, 2, 187, 188, 7, 40, 2, 2, 188, 60, 3, 2, 2, 2, 189, 190, 7, 126, 2, 2, 190, 191, 7, 126, 2, 2, 191, 62, 3, 2, 2, 2, 192, 193, 7, 35, 2, 2, 193, 64, 3, 2, 2, 2, 194, 196, 9, 2, 2, 2, 195, 194, 3, 2, 2, 2, 196, 197, 3, 2, 2, 2, 197, 195, 3, 2, 2, 2, 197, 198, 3, 2, 2, 2, 198, 66, 3, 2, 2, 2, 199, 200, 7, 60, 2, 2, 200, 204, 9, 3, 2, 2, 201, 203, 9, 4, 2, 2, 202, 201, 3, 2, 2, 2, 203, 206, 3, 2, 2, 2, 204, 202, 3, 2, 2, 2, 204, 205, 3, 2, 2, 2, 205, 68, 3, 2, 2, 2, 206, 204, 3, 2, 2, 2, 207, 209, 9, 5, 2, 2, 208, 207, 3, 2, 2, 2, 209, 210, 3, 2, 2, 2, 210, 208, 3, 2, 2, 2, 210, 211, 3, 2, 2, 2, 211, 70, 3, 2, 2, 2, 212, 214, 9, 6, 2, 2, 213, 212, 3, 2, 2, 2, 214, 215, 3, 2, 2, 2, 215, 213, 3, 2, 2, 2, 215, 216, 3, 2, 2, 2, 216, 217, 3, 2, 2, 2, 217, 218, 8, 36, 2, 2, 218, 72, 3, 2, 2, 2, 7, 2, 197, 204, 210, 215, 3, 8, 2, 2] \ No newline at end of file +[3, 24715, 42794, 33075, 47597, 16764, 15335, 30598, 22884, 2, 41, 253, 8, 1, 4, 2, 9, 2, 4, 3, 9, 3, 4, 4, 9, 4, 4, 5, 9, 5, 4, 6, 9, 6, 4, 7, 9, 7, 4, 8, 9, 8, 4, 9, 9, 9, 4, 10, 9, 10, 4, 11, 9, 11, 4, 12, 9, 12, 4, 13, 9, 13, 4, 14, 9, 14, 4, 15, 9, 15, 4, 16, 9, 16, 4, 17, 9, 17, 4, 18, 9, 18, 4, 19, 9, 19, 4, 20, 9, 20, 4, 21, 9, 21, 4, 22, 9, 22, 4, 23, 9, 23, 4, 24, 9, 24, 4, 25, 9, 25, 4, 26, 9, 26, 4, 27, 9, 27, 4, 28, 9, 28, 4, 29, 9, 29, 4, 30, 9, 30, 4, 31, 9, 31, 4, 32, 9, 32, 4, 33, 9, 33, 4, 34, 9, 34, 4, 35, 9, 35, 4, 36, 9, 36, 4, 37, 9, 37, 4, 38, 9, 38, 4, 39, 9, 39, 4, 40, 9, 40, 3, 2, 3, 2, 3, 2, 3, 3, 3, 3, 3, 4, 3, 4, 3, 5, 3, 5, 3, 5, 3, 5, 3, 5, 3, 6, 3, 6, 3, 6, 3, 6, 3, 6, 3, 6, 3, 6, 3, 7, 3, 7, 3, 7, 3, 7, 3, 7, 3, 8, 3, 8, 3, 9, 3, 9, 3, 10, 3, 10, 3, 11, 3, 11, 3, 12, 3, 12, 3, 12, 3, 12, 3, 12, 3, 12, 3, 12, 3, 12, 3, 13, 3, 13, 3, 13, 3, 13, 3, 13, 3, 13, 3, 13, 3, 13, 3, 13, 3, 14, 3, 14, 3, 14, 3, 14, 3, 14, 3, 15, 3, 15, 3, 15, 3, 15, 3, 15, 3, 15, 3, 16, 3, 16, 3, 16, 3, 16, 3, 16, 3, 16, 3, 17, 3, 17, 3, 17, 3, 17, 3, 17, 3, 17, 3, 17, 3, 17, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 19, 3, 19, 3, 19, 3, 19, 3, 19, 3, 19, 3, 19, 3, 20, 3, 20, 3, 20, 3, 20, 3, 20, 3, 20, 3, 20, 3, 20, 3, 20, 3, 20, 3, 21, 3, 21, 3, 21, 3, 21, 3, 21, 3, 21, 3, 21, 3, 22, 3, 22, 3, 23, 3, 23, 3, 24, 3, 24, 3, 25, 3, 25, 3, 26, 3, 26, 3, 27, 3, 27, 3, 27, 3, 27, 3, 27, 3, 27, 3, 27, 3, 27, 3, 27, 3, 28, 3, 28, 3, 29, 3, 29, 3, 30, 3, 30, 3, 30, 3, 31, 3, 31, 3, 31, 3, 32, 3, 32, 3, 32, 3, 33, 3, 33, 3, 33, 3, 34, 3, 34, 3, 34, 3, 35, 3, 35, 3, 35, 3, 36, 3, 36, 3, 37, 6, 37, 230, 10, 37, 13, 37, 14, 37, 231, 3, 38, 3, 38, 3, 38, 7, 38, 237, 10, 38, 12, 38, 14, 38, 240, 11, 38, 3, 39, 6, 39, 243, 10, 39, 13, 39, 14, 39, 244, 3, 40, 6, 40, 248, 10, 40, 13, 40, 14, 40, 249, 3, 40, 3, 40, 2, 2, 41, 3, 3, 5, 4, 7, 5, 9, 6, 11, 7, 13, 8, 15, 9, 17, 10, 19, 11, 21, 12, 23, 13, 25, 14, 27, 15, 29, 16, 31, 17, 33, 18, 35, 19, 37, 20, 39, 21, 41, 22, 43, 23, 45, 24, 47, 25, 49, 26, 51, 27, 53, 28, 55, 29, 57, 30, 59, 31, 61, 32, 63, 33, 65, 34, 67, 35, 69, 36, 71, 37, 73, 38, 75, 39, 77, 40, 79, 41, 3, 2, 7, 3, 2, 50, 59, 5, 2, 67, 92, 97, 97, 99, 124, 5, 2, 50, 59, 67, 92, 99, 124, 4, 2, 67, 92, 99, 124, 5, 2, 11, 12, 15, 15, 34, 34, 2, 256, 2, 3, 3, 2, 2, 2, 2, 5, 3, 2, 2, 2, 2, 7, 3, 2, 2, 2, 2, 9, 3, 2, 2, 2, 2, 11, 3, 2, 2, 2, 2, 13, 3, 2, 2, 2, 2, 15, 3, 2, 2, 2, 2, 17, 3, 2, 2, 2, 2, 19, 3, 2, 2, 2, 2, 21, 3, 2, 2, 2, 2, 23, 3, 2, 2, 2, 2, 25, 3, 2, 2, 2, 2, 27, 3, 2, 2, 2, 2, 29, 3, 2, 2, 2, 2, 31, 3, 2, 2, 2, 2, 33, 3, 2, 2, 2, 2, 35, 3, 2, 2, 2, 2, 37, 3, 2, 2, 2, 2, 39, 3, 2, 2, 2, 2, 41, 3, 2, 2, 2, 2, 43, 3, 2, 2, 2, 2, 45, 3, 2, 2, 2, 2, 47, 3, 2, 2, 2, 2, 49, 3, 2, 2, 2, 2, 51, 3, 2, 2, 2, 2, 53, 3, 2, 2, 2, 2, 55, 3, 2, 2, 2, 2, 57, 3, 2, 2, 2, 2, 59, 3, 2, 2, 2, 2, 61, 3, 2, 2, 2, 2, 63, 3, 2, 2, 2, 2, 65, 3, 2, 2, 2, 2, 67, 3, 2, 2, 2, 2, 69, 3, 2, 2, 2, 2, 71, 3, 2, 2, 2, 2, 73, 3, 2, 2, 2, 2, 75, 3, 2, 2, 2, 2, 77, 3, 2, 2, 2, 2, 79, 3, 2, 2, 2, 3, 81, 3, 2, 2, 2, 5, 84, 3, 2, 2, 2, 7, 86, 3, 2, 2, 2, 9, 88, 3, 2, 2, 2, 11, 93, 3, 2, 2, 2, 13, 100, 3, 2, 2, 2, 15, 105, 3, 2, 2, 2, 17, 107, 3, 2, 2, 2, 19, 109, 3, 2, 2, 2, 21, 111, 3, 2, 2, 2, 23, 113, 3, 2, 2, 2, 25, 121, 3, 2, 2, 2, 27, 130, 3, 2, 2, 2, 29, 135, 3, 2, 2, 2, 31, 141, 3, 2, 2, 2, 33, 147, 3, 2, 2, 2, 35, 155, 3, 2, 2, 2, 37, 161, 3, 2, 2, 2, 39, 168, 3, 2, 2, 2, 41, 178, 3, 2, 2, 2, 43, 185, 3, 2, 2, 2, 45, 187, 3, 2, 2, 2, 47, 189, 3, 2, 2, 2, 49, 191, 3, 2, 2, 2, 51, 193, 3, 2, 2, 2, 53, 195, 3, 2, 2, 2, 55, 204, 3, 2, 2, 2, 57, 206, 3, 2, 2, 2, 59, 208, 3, 2, 2, 2, 61, 211, 3, 2, 2, 2, 63, 214, 3, 2, 2, 2, 65, 217, 3, 2, 2, 2, 67, 220, 3, 2, 2, 2, 69, 223, 3, 2, 2, 2, 71, 226, 3, 2, 2, 2, 73, 229, 3, 2, 2, 2, 75, 233, 3, 2, 2, 2, 77, 242, 3, 2, 2, 2, 79, 247, 3, 2, 2, 2, 81, 82, 7, 107, 2, 2, 82, 83, 7, 104, 2, 2, 83, 4, 3, 2, 2, 2, 84, 85, 7, 93, 2, 2, 85, 6, 3, 2, 2, 2, 86, 87, 7, 95, 2, 2, 87, 8, 3, 2, 2, 2, 88, 89, 7, 103, 2, 2, 89, 90, 7, 110, 2, 2, 90, 91, 7, 117, 2, 2, 91, 92, 7, 103, 2, 2, 92, 10, 3, 2, 2, 2, 93, 94, 7, 116, 2, 2, 94, 95, 7, 103, 2, 2, 95, 96, 7, 114, 2, 2, 96, 97, 7, 103, 2, 2, 97, 98, 7, 99, 2, 2, 98, 99, 7, 118, 2, 2, 99, 12, 3, 2, 2, 2, 100, 101, 7, 105, 2, 2, 101, 102, 7, 113, 2, 2, 102, 103, 7, 118, 2, 2, 103, 104, 7, 113, 2, 2, 104, 14, 3, 2, 2, 2, 105, 106, 7, 42, 2, 2, 106, 16, 3, 2, 2, 2, 107, 108, 7, 46, 2, 2, 108, 18, 3, 2, 2, 2, 109, 110, 7, 43, 2, 2, 110, 20, 3, 2, 2, 2, 111, 112, 7, 63, 2, 2, 112, 22, 3, 2, 2, 2, 113, 114, 7, 104, 2, 2, 114, 115, 7, 113, 2, 2, 115, 116, 7, 116, 2, 2, 116, 117, 7, 121, 2, 2, 117, 118, 7, 99, 2, 2, 118, 119, 7, 116, 2, 2, 119, 120, 7, 102, 2, 2, 120, 24, 3, 2, 2, 2, 121, 122, 7, 100, 2, 2, 122, 123, 7, 99, 2, 2, 123, 124, 7, 101, 2, 2, 124, 125, 7, 109, 2, 2, 125, 126, 7, 121, 2, 2, 126, 127, 7, 99, 2, 2, 127, 128, 7, 116, 2, 2, 128, 129, 7, 102, 2, 2, 129, 26, 3, 2, 2, 2, 130, 131, 7, 110, 2, 2, 131, 132, 7, 103, 2, 2, 132, 133, 7, 104, 2, 2, 133, 134, 7, 118, 2, 2, 134, 28, 3, 2, 2, 2, 135, 136, 7, 116, 2, 2, 136, 137, 7, 107, 2, 2, 137, 138, 7, 105, 2, 2, 138, 139, 7, 106, 2, 2, 139, 140, 7, 118, 2, 2, 140, 30, 3, 2, 2, 2, 141, 142, 7, 114, 2, 2, 142, 143, 7, 103, 2, 2, 143, 144, 7, 112, 2, 2, 144, 145, 7, 119, 2, 2, 145, 146, 7, 114, 2, 2, 146, 32, 3, 2, 2, 2, 147, 148, 7, 114, 2, 2, 148, 149, 7, 103, 2, 2, 149, 150, 7, 112, 2, 2, 150, 151, 7, 102, 2, 2, 151, 152, 7, 113, 2, 2, 152, 153, 7, 121, 2, 2, 153, 154, 7, 112, 2, 2, 154, 34, 3, 2, 2, 2, 155, 156, 7, 114, 2, 2, 156, 157, 7, 99, 2, 2, 157, 158, 7, 119, 2, 2, 158, 159, 7, 117, 2, 2, 159, 160, 7, 103, 2, 2, 160, 36, 3, 2, 2, 2, 161, 162, 7, 99, 2, 2, 162, 163, 7, 117, 2, 2, 163, 164, 7, 117, 2, 2, 164, 165, 7, 103, 2, 2, 165, 166, 7, 116, 2, 2, 166, 167, 7, 118, 2, 2, 167, 38, 3, 2, 2, 2, 168, 169, 7, 107, 2, 2, 169, 170, 7, 112, 2, 2, 170, 171, 7, 120, 2, 2, 171, 172, 7, 99, 2, 2, 172, 173, 7, 116, 2, 2, 173, 174, 7, 107, 2, 2, 174, 175, 7, 99, 2, 2, 175, 176, 7, 112, 2, 2, 176, 177, 7, 118, 2, 2, 177, 40, 3, 2, 2, 2, 178, 179, 7, 99, 2, 2, 179, 180, 7, 117, 2, 2, 180, 181, 7, 117, 2, 2, 181, 182, 7, 119, 2, 2, 182, 183, 7, 111, 2, 2, 183, 184, 7, 103, 2, 2, 184, 42, 3, 2, 2, 2, 185, 186, 7, 45, 2, 2, 186, 44, 3, 2, 2, 2, 187, 188, 7, 47, 2, 2, 188, 46, 3, 2, 2, 2, 189, 190, 7, 44, 2, 2, 190, 48, 3, 2, 2, 2, 191, 192, 7, 49, 2, 2, 192, 50, 3, 2, 2, 2, 193, 194, 7, 39, 2, 2, 194, 52, 3, 2, 2, 2, 195, 196, 7, 114, 2, 2, 196, 197, 7, 103, 2, 2, 197, 198, 7, 112, 2, 2, 198, 199, 7, 102, 2, 2, 199, 200, 7, 113, 2, 2, 200, 201, 7, 121, 2, 2, 201, 202, 7, 112, 2, 2, 202, 203, 7, 65, 2, 2, 203, 54, 3, 2, 2, 2, 204, 205, 7, 62, 2, 2, 205, 56, 3, 2, 2, 2, 206, 207, 7, 64, 2, 2, 207, 58, 3, 2, 2, 2, 208, 209, 7, 63, 2, 2, 209, 210, 7, 63, 2, 2, 210, 60, 3, 2, 2, 2, 211, 212, 7, 35, 2, 2, 212, 213, 7, 63, 2, 2, 213, 62, 3, 2, 2, 2, 214, 215, 7, 62, 2, 2, 215, 216, 7, 63, 2, 2, 216, 64, 3, 2, 2, 2, 217, 218, 7, 64, 2, 2, 218, 219, 7, 63, 2, 2, 219, 66, 3, 2, 2, 2, 220, 221, 7, 40, 2, 2, 221, 222, 7, 40, 2, 2, 222, 68, 3, 2, 2, 2, 223, 224, 7, 126, 2, 2, 224, 225, 7, 126, 2, 2, 225, 70, 3, 2, 2, 2, 226, 227, 7, 35, 2, 2, 227, 72, 3, 2, 2, 2, 228, 230, 9, 2, 2, 2, 229, 228, 3, 2, 2, 2, 230, 231, 3, 2, 2, 2, 231, 229, 3, 2, 2, 2, 231, 232, 3, 2, 2, 2, 232, 74, 3, 2, 2, 2, 233, 234, 7, 60, 2, 2, 234, 238, 9, 3, 2, 2, 235, 237, 9, 4, 2, 2, 236, 235, 3, 2, 2, 2, 237, 240, 3, 2, 2, 2, 238, 236, 3, 2, 2, 2, 238, 239, 3, 2, 2, 2, 239, 76, 3, 2, 2, 2, 240, 238, 3, 2, 2, 2, 241, 243, 9, 5, 2, 2, 242, 241, 3, 2, 2, 2, 243, 244, 3, 2, 2, 2, 244, 242, 3, 2, 2, 2, 244, 245, 3, 2, 2, 2, 245, 78, 3, 2, 2, 2, 246, 248, 9, 6, 2, 2, 247, 246, 3, 2, 2, 2, 248, 249, 3, 2, 2, 2, 249, 247, 3, 2, 2, 2, 249, 250, 3, 2, 2, 2, 250, 251, 3, 2, 2, 2, 251, 252, 8, 40, 2, 2, 252, 80, 3, 2, 2, 2, 7, 2, 231, 238, 244, 249, 3, 8, 2, 2] \ No newline at end of file diff --git a/ChironCore/turtparse/tlangLexer.py b/ChironCore/turtparse/tlangLexer.py index fc951de..9400e6f 100644 --- a/ChironCore/turtparse/tlangLexer.py +++ b/ChironCore/turtparse/tlangLexer.py @@ -5,93 +5,108 @@ import sys + def serializedATN(): with StringIO() as buf: - buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2%") - buf.write("\u00db\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7") + buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2)") + buf.write("\u00fd\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7") buf.write("\t\7\4\b\t\b\4\t\t\t\4\n\t\n\4\13\t\13\4\f\t\f\4\r\t\r") buf.write("\4\16\t\16\4\17\t\17\4\20\t\20\4\21\t\21\4\22\t\22\4\23") buf.write("\t\23\4\24\t\24\4\25\t\25\4\26\t\26\4\27\t\27\4\30\t\30") buf.write("\4\31\t\31\4\32\t\32\4\33\t\33\4\34\t\34\4\35\t\35\4\36") - buf.write("\t\36\4\37\t\37\4 \t \4!\t!\4\"\t\"\4#\t#\4$\t$\3\2\3") - buf.write("\2\3\2\3\3\3\3\3\4\3\4\3\5\3\5\3\5\3\5\3\5\3\6\3\6\3\6") - buf.write("\3\6\3\6\3\6\3\6\3\7\3\7\3\7\3\7\3\7\3\b\3\b\3\t\3\t\3") - buf.write("\n\3\n\3\13\3\13\3\f\3\f\3\f\3\f\3\f\3\f\3\f\3\f\3\r\3") - buf.write("\r\3\r\3\r\3\r\3\r\3\r\3\r\3\r\3\16\3\16\3\16\3\16\3\16") - buf.write("\3\17\3\17\3\17\3\17\3\17\3\17\3\20\3\20\3\20\3\20\3\20") - buf.write("\3\20\3\21\3\21\3\21\3\21\3\21\3\21\3\21\3\21\3\22\3\22") - buf.write("\3\22\3\22\3\22\3\22\3\23\3\23\3\24\3\24\3\25\3\25\3\26") - buf.write("\3\26\3\27\3\27\3\27\3\27\3\27\3\27\3\27\3\27\3\27\3\30") - buf.write("\3\30\3\31\3\31\3\32\3\32\3\32\3\33\3\33\3\33\3\34\3\34") - buf.write("\3\34\3\35\3\35\3\35\3\36\3\36\3\36\3\37\3\37\3\37\3 ") - buf.write("\3 \3!\6!\u00c4\n!\r!\16!\u00c5\3\"\3\"\3\"\7\"\u00cb") - buf.write("\n\"\f\"\16\"\u00ce\13\"\3#\6#\u00d1\n#\r#\16#\u00d2\3") - buf.write("$\6$\u00d6\n$\r$\16$\u00d7\3$\3$\2\2%\3\3\5\4\7\5\t\6") - buf.write("\13\7\r\b\17\t\21\n\23\13\25\f\27\r\31\16\33\17\35\20") - buf.write("\37\21!\22#\23%\24\'\25)\26+\27-\30/\31\61\32\63\33\65") - buf.write("\34\67\359\36;\37= ?!A\"C#E$G%\3\2\7\3\2\62;\5\2C\\aa") - buf.write("c|\5\2\62;C\\c|\4\2C\\c|\5\2\13\f\17\17\"\"\2\u00de\2") - buf.write("\3\3\2\2\2\2\5\3\2\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3") - buf.write("\2\2\2\2\r\3\2\2\2\2\17\3\2\2\2\2\21\3\2\2\2\2\23\3\2") - buf.write("\2\2\2\25\3\2\2\2\2\27\3\2\2\2\2\31\3\2\2\2\2\33\3\2\2") - buf.write("\2\2\35\3\2\2\2\2\37\3\2\2\2\2!\3\2\2\2\2#\3\2\2\2\2%") - buf.write("\3\2\2\2\2\'\3\2\2\2\2)\3\2\2\2\2+\3\2\2\2\2-\3\2\2\2") - buf.write("\2/\3\2\2\2\2\61\3\2\2\2\2\63\3\2\2\2\2\65\3\2\2\2\2\67") - buf.write("\3\2\2\2\29\3\2\2\2\2;\3\2\2\2\2=\3\2\2\2\2?\3\2\2\2\2") - buf.write("A\3\2\2\2\2C\3\2\2\2\2E\3\2\2\2\2G\3\2\2\2\3I\3\2\2\2") - buf.write("\5L\3\2\2\2\7N\3\2\2\2\tP\3\2\2\2\13U\3\2\2\2\r\\\3\2") - buf.write("\2\2\17a\3\2\2\2\21c\3\2\2\2\23e\3\2\2\2\25g\3\2\2\2\27") - buf.write("i\3\2\2\2\31q\3\2\2\2\33z\3\2\2\2\35\177\3\2\2\2\37\u0085") - buf.write("\3\2\2\2!\u008b\3\2\2\2#\u0093\3\2\2\2%\u0099\3\2\2\2") - buf.write("\'\u009b\3\2\2\2)\u009d\3\2\2\2+\u009f\3\2\2\2-\u00a1") - buf.write("\3\2\2\2/\u00aa\3\2\2\2\61\u00ac\3\2\2\2\63\u00ae\3\2") - buf.write("\2\2\65\u00b1\3\2\2\2\67\u00b4\3\2\2\29\u00b7\3\2\2\2") - buf.write(";\u00ba\3\2\2\2=\u00bd\3\2\2\2?\u00c0\3\2\2\2A\u00c3\3") - buf.write("\2\2\2C\u00c7\3\2\2\2E\u00d0\3\2\2\2G\u00d5\3\2\2\2IJ") - buf.write("\7k\2\2JK\7h\2\2K\4\3\2\2\2LM\7]\2\2M\6\3\2\2\2NO\7_\2") - buf.write("\2O\b\3\2\2\2PQ\7g\2\2QR\7n\2\2RS\7u\2\2ST\7g\2\2T\n\3") - buf.write("\2\2\2UV\7t\2\2VW\7g\2\2WX\7r\2\2XY\7g\2\2YZ\7c\2\2Z[") - buf.write("\7v\2\2[\f\3\2\2\2\\]\7i\2\2]^\7q\2\2^_\7v\2\2_`\7q\2") - buf.write("\2`\16\3\2\2\2ab\7*\2\2b\20\3\2\2\2cd\7.\2\2d\22\3\2\2") - buf.write("\2ef\7+\2\2f\24\3\2\2\2gh\7?\2\2h\26\3\2\2\2ij\7h\2\2") - buf.write("jk\7q\2\2kl\7t\2\2lm\7y\2\2mn\7c\2\2no\7t\2\2op\7f\2\2") - buf.write("p\30\3\2\2\2qr\7d\2\2rs\7c\2\2st\7e\2\2tu\7m\2\2uv\7y") - buf.write("\2\2vw\7c\2\2wx\7t\2\2xy\7f\2\2y\32\3\2\2\2z{\7n\2\2{") - buf.write("|\7g\2\2|}\7h\2\2}~\7v\2\2~\34\3\2\2\2\177\u0080\7t\2") - buf.write("\2\u0080\u0081\7k\2\2\u0081\u0082\7i\2\2\u0082\u0083\7") - buf.write("j\2\2\u0083\u0084\7v\2\2\u0084\36\3\2\2\2\u0085\u0086") - buf.write("\7r\2\2\u0086\u0087\7g\2\2\u0087\u0088\7p\2\2\u0088\u0089") - buf.write("\7w\2\2\u0089\u008a\7r\2\2\u008a \3\2\2\2\u008b\u008c") - buf.write("\7r\2\2\u008c\u008d\7g\2\2\u008d\u008e\7p\2\2\u008e\u008f") - buf.write("\7f\2\2\u008f\u0090\7q\2\2\u0090\u0091\7y\2\2\u0091\u0092") - buf.write("\7p\2\2\u0092\"\3\2\2\2\u0093\u0094\7r\2\2\u0094\u0095") - buf.write("\7c\2\2\u0095\u0096\7w\2\2\u0096\u0097\7u\2\2\u0097\u0098") - buf.write("\7g\2\2\u0098$\3\2\2\2\u0099\u009a\7-\2\2\u009a&\3\2\2") - buf.write("\2\u009b\u009c\7/\2\2\u009c(\3\2\2\2\u009d\u009e\7,\2") - buf.write("\2\u009e*\3\2\2\2\u009f\u00a0\7\61\2\2\u00a0,\3\2\2\2") - buf.write("\u00a1\u00a2\7r\2\2\u00a2\u00a3\7g\2\2\u00a3\u00a4\7p") - buf.write("\2\2\u00a4\u00a5\7f\2\2\u00a5\u00a6\7q\2\2\u00a6\u00a7") - buf.write("\7y\2\2\u00a7\u00a8\7p\2\2\u00a8\u00a9\7A\2\2\u00a9.\3") - buf.write("\2\2\2\u00aa\u00ab\7>\2\2\u00ab\60\3\2\2\2\u00ac\u00ad") - buf.write("\7@\2\2\u00ad\62\3\2\2\2\u00ae\u00af\7?\2\2\u00af\u00b0") - buf.write("\7?\2\2\u00b0\64\3\2\2\2\u00b1\u00b2\7#\2\2\u00b2\u00b3") - buf.write("\7?\2\2\u00b3\66\3\2\2\2\u00b4\u00b5\7>\2\2\u00b5\u00b6") - buf.write("\7?\2\2\u00b68\3\2\2\2\u00b7\u00b8\7@\2\2\u00b8\u00b9") - buf.write("\7?\2\2\u00b9:\3\2\2\2\u00ba\u00bb\7(\2\2\u00bb\u00bc") - buf.write("\7(\2\2\u00bc<\3\2\2\2\u00bd\u00be\7~\2\2\u00be\u00bf") - buf.write("\7~\2\2\u00bf>\3\2\2\2\u00c0\u00c1\7#\2\2\u00c1@\3\2\2") - buf.write("\2\u00c2\u00c4\t\2\2\2\u00c3\u00c2\3\2\2\2\u00c4\u00c5") - buf.write("\3\2\2\2\u00c5\u00c3\3\2\2\2\u00c5\u00c6\3\2\2\2\u00c6") - buf.write("B\3\2\2\2\u00c7\u00c8\7<\2\2\u00c8\u00cc\t\3\2\2\u00c9") - buf.write("\u00cb\t\4\2\2\u00ca\u00c9\3\2\2\2\u00cb\u00ce\3\2\2\2") - buf.write("\u00cc\u00ca\3\2\2\2\u00cc\u00cd\3\2\2\2\u00cdD\3\2\2") - buf.write("\2\u00ce\u00cc\3\2\2\2\u00cf\u00d1\t\5\2\2\u00d0\u00cf") - buf.write("\3\2\2\2\u00d1\u00d2\3\2\2\2\u00d2\u00d0\3\2\2\2\u00d2") - buf.write("\u00d3\3\2\2\2\u00d3F\3\2\2\2\u00d4\u00d6\t\6\2\2\u00d5") - buf.write("\u00d4\3\2\2\2\u00d6\u00d7\3\2\2\2\u00d7\u00d5\3\2\2\2") - buf.write("\u00d7\u00d8\3\2\2\2\u00d8\u00d9\3\2\2\2\u00d9\u00da\b") - buf.write("$\2\2\u00daH\3\2\2\2\7\2\u00c5\u00cc\u00d2\u00d7\3\b\2") - buf.write("\2") + buf.write("\t\36\4\37\t\37\4 \t \4!\t!\4\"\t\"\4#\t#\4$\t$\4%\t%") + buf.write("\4&\t&\4\'\t\'\4(\t(\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\3") + buf.write("\5\3\5\3\5\3\5\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\7\3\7\3\7") + buf.write("\3\7\3\7\3\b\3\b\3\t\3\t\3\n\3\n\3\13\3\13\3\f\3\f\3\f") + buf.write("\3\f\3\f\3\f\3\f\3\f\3\r\3\r\3\r\3\r\3\r\3\r\3\r\3\r\3") + buf.write("\r\3\16\3\16\3\16\3\16\3\16\3\17\3\17\3\17\3\17\3\17\3") + buf.write("\17\3\20\3\20\3\20\3\20\3\20\3\20\3\21\3\21\3\21\3\21") + buf.write("\3\21\3\21\3\21\3\21\3\22\3\22\3\22\3\22\3\22\3\22\3\23") + buf.write("\3\23\3\23\3\23\3\23\3\23\3\23\3\24\3\24\3\24\3\24\3\24") + buf.write("\3\24\3\24\3\24\3\24\3\24\3\25\3\25\3\25\3\25\3\25\3\25") + buf.write("\3\25\3\26\3\26\3\27\3\27\3\30\3\30\3\31\3\31\3\32\3\32") + buf.write("\3\33\3\33\3\33\3\33\3\33\3\33\3\33\3\33\3\33\3\34\3\34") + buf.write("\3\35\3\35\3\36\3\36\3\36\3\37\3\37\3\37\3 \3 \3 \3!\3") + buf.write("!\3!\3\"\3\"\3\"\3#\3#\3#\3$\3$\3%\6%\u00e6\n%\r%\16%") + buf.write("\u00e7\3&\3&\3&\7&\u00ed\n&\f&\16&\u00f0\13&\3\'\6\'\u00f3") + buf.write("\n\'\r\'\16\'\u00f4\3(\6(\u00f8\n(\r(\16(\u00f9\3(\3(") + buf.write("\2\2)\3\3\5\4\7\5\t\6\13\7\r\b\17\t\21\n\23\13\25\f\27") + buf.write("\r\31\16\33\17\35\20\37\21!\22#\23%\24\'\25)\26+\27-\30") + buf.write("/\31\61\32\63\33\65\34\67\359\36;\37= ?!A\"C#E$G%I&K\'") + buf.write("M(O)\3\2\7\3\2\62;\5\2C\\aac|\5\2\62;C\\c|\4\2C\\c|\5") + buf.write("\2\13\f\17\17\"\"\2\u0100\2\3\3\2\2\2\2\5\3\2\2\2\2\7") + buf.write("\3\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\2\17\3\2") + buf.write("\2\2\2\21\3\2\2\2\2\23\3\2\2\2\2\25\3\2\2\2\2\27\3\2\2") + buf.write("\2\2\31\3\2\2\2\2\33\3\2\2\2\2\35\3\2\2\2\2\37\3\2\2\2") + buf.write("\2!\3\2\2\2\2#\3\2\2\2\2%\3\2\2\2\2\'\3\2\2\2\2)\3\2\2") + buf.write("\2\2+\3\2\2\2\2-\3\2\2\2\2/\3\2\2\2\2\61\3\2\2\2\2\63") + buf.write("\3\2\2\2\2\65\3\2\2\2\2\67\3\2\2\2\29\3\2\2\2\2;\3\2\2") + buf.write("\2\2=\3\2\2\2\2?\3\2\2\2\2A\3\2\2\2\2C\3\2\2\2\2E\3\2") + buf.write("\2\2\2G\3\2\2\2\2I\3\2\2\2\2K\3\2\2\2\2M\3\2\2\2\2O\3") + buf.write("\2\2\2\3Q\3\2\2\2\5T\3\2\2\2\7V\3\2\2\2\tX\3\2\2\2\13") + buf.write("]\3\2\2\2\rd\3\2\2\2\17i\3\2\2\2\21k\3\2\2\2\23m\3\2\2") + buf.write("\2\25o\3\2\2\2\27q\3\2\2\2\31y\3\2\2\2\33\u0082\3\2\2") + buf.write("\2\35\u0087\3\2\2\2\37\u008d\3\2\2\2!\u0093\3\2\2\2#\u009b") + buf.write("\3\2\2\2%\u00a1\3\2\2\2\'\u00a8\3\2\2\2)\u00b2\3\2\2\2") + buf.write("+\u00b9\3\2\2\2-\u00bb\3\2\2\2/\u00bd\3\2\2\2\61\u00bf") + buf.write("\3\2\2\2\63\u00c1\3\2\2\2\65\u00c3\3\2\2\2\67\u00cc\3") + buf.write("\2\2\29\u00ce\3\2\2\2;\u00d0\3\2\2\2=\u00d3\3\2\2\2?\u00d6") + buf.write("\3\2\2\2A\u00d9\3\2\2\2C\u00dc\3\2\2\2E\u00df\3\2\2\2") + buf.write("G\u00e2\3\2\2\2I\u00e5\3\2\2\2K\u00e9\3\2\2\2M\u00f2\3") + buf.write("\2\2\2O\u00f7\3\2\2\2QR\7k\2\2RS\7h\2\2S\4\3\2\2\2TU\7") + buf.write("]\2\2U\6\3\2\2\2VW\7_\2\2W\b\3\2\2\2XY\7g\2\2YZ\7n\2\2") + buf.write("Z[\7u\2\2[\\\7g\2\2\\\n\3\2\2\2]^\7t\2\2^_\7g\2\2_`\7") + buf.write("r\2\2`a\7g\2\2ab\7c\2\2bc\7v\2\2c\f\3\2\2\2de\7i\2\2e") + buf.write("f\7q\2\2fg\7v\2\2gh\7q\2\2h\16\3\2\2\2ij\7*\2\2j\20\3") + buf.write("\2\2\2kl\7.\2\2l\22\3\2\2\2mn\7+\2\2n\24\3\2\2\2op\7?") + buf.write("\2\2p\26\3\2\2\2qr\7h\2\2rs\7q\2\2st\7t\2\2tu\7y\2\2u") + buf.write("v\7c\2\2vw\7t\2\2wx\7f\2\2x\30\3\2\2\2yz\7d\2\2z{\7c\2") + buf.write("\2{|\7e\2\2|}\7m\2\2}~\7y\2\2~\177\7c\2\2\177\u0080\7") + buf.write("t\2\2\u0080\u0081\7f\2\2\u0081\32\3\2\2\2\u0082\u0083") + buf.write("\7n\2\2\u0083\u0084\7g\2\2\u0084\u0085\7h\2\2\u0085\u0086") + buf.write("\7v\2\2\u0086\34\3\2\2\2\u0087\u0088\7t\2\2\u0088\u0089") + buf.write("\7k\2\2\u0089\u008a\7i\2\2\u008a\u008b\7j\2\2\u008b\u008c") + buf.write("\7v\2\2\u008c\36\3\2\2\2\u008d\u008e\7r\2\2\u008e\u008f") + buf.write("\7g\2\2\u008f\u0090\7p\2\2\u0090\u0091\7w\2\2\u0091\u0092") + buf.write("\7r\2\2\u0092 \3\2\2\2\u0093\u0094\7r\2\2\u0094\u0095") + buf.write("\7g\2\2\u0095\u0096\7p\2\2\u0096\u0097\7f\2\2\u0097\u0098") + buf.write("\7q\2\2\u0098\u0099\7y\2\2\u0099\u009a\7p\2\2\u009a\"") + buf.write("\3\2\2\2\u009b\u009c\7r\2\2\u009c\u009d\7c\2\2\u009d\u009e") + buf.write("\7w\2\2\u009e\u009f\7u\2\2\u009f\u00a0\7g\2\2\u00a0$\3") + buf.write("\2\2\2\u00a1\u00a2\7c\2\2\u00a2\u00a3\7u\2\2\u00a3\u00a4") + buf.write("\7u\2\2\u00a4\u00a5\7g\2\2\u00a5\u00a6\7t\2\2\u00a6\u00a7") + buf.write("\7v\2\2\u00a7&\3\2\2\2\u00a8\u00a9\7k\2\2\u00a9\u00aa") + buf.write("\7p\2\2\u00aa\u00ab\7x\2\2\u00ab\u00ac\7c\2\2\u00ac\u00ad") + buf.write("\7t\2\2\u00ad\u00ae\7k\2\2\u00ae\u00af\7c\2\2\u00af\u00b0") + buf.write("\7p\2\2\u00b0\u00b1\7v\2\2\u00b1(\3\2\2\2\u00b2\u00b3") + buf.write("\7c\2\2\u00b3\u00b4\7u\2\2\u00b4\u00b5\7u\2\2\u00b5\u00b6") + buf.write("\7w\2\2\u00b6\u00b7\7o\2\2\u00b7\u00b8\7g\2\2\u00b8*\3") + buf.write("\2\2\2\u00b9\u00ba\7-\2\2\u00ba,\3\2\2\2\u00bb\u00bc\7") + buf.write("/\2\2\u00bc.\3\2\2\2\u00bd\u00be\7,\2\2\u00be\60\3\2\2") + buf.write("\2\u00bf\u00c0\7\61\2\2\u00c0\62\3\2\2\2\u00c1\u00c2\7") + buf.write("\'\2\2\u00c2\64\3\2\2\2\u00c3\u00c4\7r\2\2\u00c4\u00c5") + buf.write("\7g\2\2\u00c5\u00c6\7p\2\2\u00c6\u00c7\7f\2\2\u00c7\u00c8") + buf.write("\7q\2\2\u00c8\u00c9\7y\2\2\u00c9\u00ca\7p\2\2\u00ca\u00cb") + buf.write("\7A\2\2\u00cb\66\3\2\2\2\u00cc\u00cd\7>\2\2\u00cd8\3\2") + buf.write("\2\2\u00ce\u00cf\7@\2\2\u00cf:\3\2\2\2\u00d0\u00d1\7?") + buf.write("\2\2\u00d1\u00d2\7?\2\2\u00d2<\3\2\2\2\u00d3\u00d4\7#") + buf.write("\2\2\u00d4\u00d5\7?\2\2\u00d5>\3\2\2\2\u00d6\u00d7\7>") + buf.write("\2\2\u00d7\u00d8\7?\2\2\u00d8@\3\2\2\2\u00d9\u00da\7@") + buf.write("\2\2\u00da\u00db\7?\2\2\u00dbB\3\2\2\2\u00dc\u00dd\7(") + buf.write("\2\2\u00dd\u00de\7(\2\2\u00deD\3\2\2\2\u00df\u00e0\7~") + buf.write("\2\2\u00e0\u00e1\7~\2\2\u00e1F\3\2\2\2\u00e2\u00e3\7#") + buf.write("\2\2\u00e3H\3\2\2\2\u00e4\u00e6\t\2\2\2\u00e5\u00e4\3") + buf.write("\2\2\2\u00e6\u00e7\3\2\2\2\u00e7\u00e5\3\2\2\2\u00e7\u00e8") + buf.write("\3\2\2\2\u00e8J\3\2\2\2\u00e9\u00ea\7<\2\2\u00ea\u00ee") + buf.write("\t\3\2\2\u00eb\u00ed\t\4\2\2\u00ec\u00eb\3\2\2\2\u00ed") + buf.write("\u00f0\3\2\2\2\u00ee\u00ec\3\2\2\2\u00ee\u00ef\3\2\2\2") + buf.write("\u00efL\3\2\2\2\u00f0\u00ee\3\2\2\2\u00f1\u00f3\t\5\2") + buf.write("\2\u00f2\u00f1\3\2\2\2\u00f3\u00f4\3\2\2\2\u00f4\u00f2") + buf.write("\3\2\2\2\u00f4\u00f5\3\2\2\2\u00f5N\3\2\2\2\u00f6\u00f8") + buf.write("\t\6\2\2\u00f7\u00f6\3\2\2\2\u00f8\u00f9\3\2\2\2\u00f9") + buf.write("\u00f7\3\2\2\2\u00f9\u00fa\3\2\2\2\u00fa\u00fb\3\2\2\2") + buf.write("\u00fb\u00fc\b(\2\2\u00fcP\3\2\2\2\7\2\u00e7\u00ee\u00f4") + buf.write("\u00f9\3\b\2\2") return buf.getvalue() @@ -118,24 +133,28 @@ class tlangLexer(Lexer): T__14 = 15 T__15 = 16 T__16 = 17 - PLUS = 18 - MINUS = 19 - MUL = 20 - DIV = 21 - PENCOND = 22 - LT = 23 - GT = 24 - EQ = 25 - NEQ = 26 - LTE = 27 - GTE = 28 - AND = 29 - OR = 30 - NOT = 31 - NUM = 32 - VAR = 33 - NAME = 34 - Whitespace = 35 + T__17 = 18 + T__18 = 19 + T__19 = 20 + PLUS = 21 + MINUS = 22 + MUL = 23 + DIV = 24 + MOD = 25 + PENCOND = 26 + LT = 27 + GT = 28 + EQ = 29 + NEQ = 30 + LTE = 31 + GTE = 32 + AND = 33 + OR = 34 + NOT = 35 + NUM = 36 + VAR = 37 + NAME = 38 + Whitespace = 39 channelNames = [ u"DEFAULT_TOKEN_CHANNEL", u"HIDDEN" ] @@ -144,20 +163,22 @@ class tlangLexer(Lexer): literalNames = [ "", "'if'", "'['", "']'", "'else'", "'repeat'", "'goto'", "'('", "','", "')'", "'='", "'forward'", "'backward'", "'left'", "'right'", - "'penup'", "'pendown'", "'pause'", "'+'", "'-'", "'*'", "'/'", - "'pendown?'", "'<'", "'>'", "'=='", "'!='", "'<='", "'>='", - "'&&'", "'||'", "'!'" ] + "'penup'", "'pendown'", "'pause'", "'assert'", "'invariant'", + "'assume'", "'+'", "'-'", "'*'", "'/'", "'%'", "'pendown?'", + "'<'", "'>'", "'=='", "'!='", "'<='", "'>='", "'&&'", "'||'", + "'!'" ] symbolicNames = [ "", - "PLUS", "MINUS", "MUL", "DIV", "PENCOND", "LT", "GT", "EQ", - "NEQ", "LTE", "GTE", "AND", "OR", "NOT", "NUM", "VAR", "NAME", - "Whitespace" ] + "PLUS", "MINUS", "MUL", "DIV", "MOD", "PENCOND", "LT", "GT", + "EQ", "NEQ", "LTE", "GTE", "AND", "OR", "NOT", "NUM", "VAR", + "NAME", "Whitespace" ] ruleNames = [ "T__0", "T__1", "T__2", "T__3", "T__4", "T__5", "T__6", "T__7", "T__8", "T__9", "T__10", "T__11", "T__12", "T__13", - "T__14", "T__15", "T__16", "PLUS", "MINUS", "MUL", "DIV", - "PENCOND", "LT", "GT", "EQ", "NEQ", "LTE", "GTE", "AND", - "OR", "NOT", "NUM", "VAR", "NAME", "Whitespace" ] + "T__14", "T__15", "T__16", "T__17", "T__18", "T__19", + "PLUS", "MINUS", "MUL", "DIV", "MOD", "PENCOND", "LT", + "GT", "EQ", "NEQ", "LTE", "GTE", "AND", "OR", "NOT", "NUM", + "VAR", "NAME", "Whitespace" ] grammarFileName = "tlang.g4" diff --git a/ChironCore/turtparse/tlangLexer.tokens b/ChironCore/turtparse/tlangLexer.tokens index 78f9526..d44a02b 100644 --- a/ChironCore/turtparse/tlangLexer.tokens +++ b/ChironCore/turtparse/tlangLexer.tokens @@ -15,24 +15,28 @@ T__13=14 T__14=15 T__15=16 T__16=17 -PLUS=18 -MINUS=19 -MUL=20 -DIV=21 -PENCOND=22 -LT=23 -GT=24 -EQ=25 -NEQ=26 -LTE=27 -GTE=28 -AND=29 -OR=30 -NOT=31 -NUM=32 -VAR=33 -NAME=34 -Whitespace=35 +T__17=18 +T__18=19 +T__19=20 +PLUS=21 +MINUS=22 +MUL=23 +DIV=24 +MOD=25 +PENCOND=26 +LT=27 +GT=28 +EQ=29 +NEQ=30 +LTE=31 +GTE=32 +AND=33 +OR=34 +NOT=35 +NUM=36 +VAR=37 +NAME=38 +Whitespace=39 'if'=1 '['=2 ']'=3 @@ -50,17 +54,21 @@ Whitespace=35 'penup'=15 'pendown'=16 'pause'=17 -'+'=18 -'-'=19 -'*'=20 -'/'=21 -'pendown?'=22 -'<'=23 -'>'=24 -'=='=25 -'!='=26 -'<='=27 -'>='=28 -'&&'=29 -'||'=30 -'!'=31 +'assert'=18 +'invariant'=19 +'assume'=20 +'+'=21 +'-'=22 +'*'=23 +'/'=24 +'%'=25 +'pendown?'=26 +'<'=27 +'>'=28 +'=='=29 +'!='=30 +'<='=31 +'>='=32 +'&&'=33 +'||'=34 +'!'=35 diff --git a/ChironCore/turtparse/tlangParser.py b/ChironCore/turtparse/tlangParser.py index b02d4a2..0c2a8e2 100644 --- a/ChironCore/turtparse/tlangParser.py +++ b/ChironCore/turtparse/tlangParser.py @@ -5,71 +5,78 @@ from typing.io import TextIO import sys + def serializedATN(): with StringIO() as buf: - buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3%") - buf.write("\u00af\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") + buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3)") + buf.write("\u00bb\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") buf.write("\4\b\t\b\4\t\t\t\4\n\t\n\4\13\t\13\4\f\t\f\4\r\t\r\4\16") buf.write("\t\16\4\17\t\17\4\20\t\20\4\21\t\21\4\22\t\22\4\23\t\23") - buf.write("\4\24\t\24\4\25\t\25\4\26\t\26\4\27\t\27\3\2\3\2\3\2\3") - buf.write("\3\7\3\63\n\3\f\3\16\3\66\13\3\3\4\6\49\n\4\r\4\16\4:") - buf.write("\3\5\3\5\3\5\3\5\3\5\3\5\3\5\5\5D\n\5\3\6\3\6\5\6H\n\6") - buf.write("\3\7\3\7\3\7\3\7\3\7\3\7\3\b\3\b\3\b\3\b\3\b\3\b\3\b\3") - buf.write("\b\3\b\3\b\3\t\3\t\3\t\3\t\3\t\3\t\3\n\3\n\3\n\3\n\3\n") - buf.write("\3\n\3\n\3\13\3\13\3\13\3\13\3\f\3\f\3\f\3\r\3\r\3\16") - buf.write("\3\16\3\17\3\17\3\20\3\20\3\20\3\20\3\20\3\20\3\20\3\20") - buf.write("\3\20\5\20}\n\20\3\20\3\20\3\20\3\20\3\20\3\20\3\20\3") - buf.write("\20\7\20\u0087\n\20\f\20\16\20\u008a\13\20\3\21\3\21\3") - buf.write("\22\3\22\3\23\3\23\3\24\3\24\3\24\3\24\3\24\3\24\3\24") - buf.write("\3\24\3\24\3\24\3\24\3\24\5\24\u009e\n\24\3\24\3\24\3") - buf.write("\24\3\24\7\24\u00a4\n\24\f\24\16\24\u00a7\13\24\3\25\3") - buf.write("\25\3\26\3\26\3\27\3\27\3\27\2\4\36&\30\2\4\6\b\n\f\16") - buf.write("\20\22\24\26\30\32\34\36 \"$&(*,\2\t\3\2\r\20\3\2\21\22") - buf.write("\3\2\26\27\3\2\24\25\3\2\31\36\3\2\37 \3\2\"#\2\u00a9") - buf.write("\2.\3\2\2\2\4\64\3\2\2\2\68\3\2\2\2\bC\3\2\2\2\nG\3\2") - buf.write("\2\2\fI\3\2\2\2\16O\3\2\2\2\20Y\3\2\2\2\22_\3\2\2\2\24") - buf.write("f\3\2\2\2\26j\3\2\2\2\30m\3\2\2\2\32o\3\2\2\2\34q\3\2") - buf.write("\2\2\36|\3\2\2\2 \u008b\3\2\2\2\"\u008d\3\2\2\2$\u008f") - buf.write("\3\2\2\2&\u009d\3\2\2\2(\u00a8\3\2\2\2*\u00aa\3\2\2\2") - buf.write(",\u00ac\3\2\2\2./\5\4\3\2/\60\7\2\2\3\60\3\3\2\2\2\61") - buf.write("\63\5\b\5\2\62\61\3\2\2\2\63\66\3\2\2\2\64\62\3\2\2\2") - buf.write("\64\65\3\2\2\2\65\5\3\2\2\2\66\64\3\2\2\2\679\5\b\5\2") - buf.write("8\67\3\2\2\29:\3\2\2\2:8\3\2\2\2:;\3\2\2\2;\7\3\2\2\2") - buf.write("D\5\20\t\2?D\5\26\f\2@D\5\32\16") - buf.write("\2AD\5\22\n\2BD\5\34\17\2C<\3\2\2\2C=\3\2\2\2C>\3\2\2") - buf.write("\2C?\3\2\2\2C@\3\2\2\2CA\3\2\2\2CB\3\2\2\2D\t\3\2\2\2") - buf.write("EH\5\f\7\2FH\5\16\b\2GE\3\2\2\2GF\3\2\2\2H\13\3\2\2\2") - buf.write("IJ\7\3\2\2JK\5&\24\2KL\7\4\2\2LM\5\6\4\2MN\7\5\2\2N\r") - buf.write("\3\2\2\2OP\7\3\2\2PQ\5&\24\2QR\7\4\2\2RS\5\6\4\2ST\7\5") - buf.write("\2\2TU\7\6\2\2UV\7\4\2\2VW\5\6\4\2WX\7\5\2\2X\17\3\2\2") - buf.write("\2YZ\7\7\2\2Z[\5,\27\2[\\\7\4\2\2\\]\5\6\4\2]^\7\5\2\2") - buf.write("^\21\3\2\2\2_`\7\b\2\2`a\7\t\2\2ab\5\36\20\2bc\7\n\2\2") - buf.write("cd\5\36\20\2de\7\13\2\2e\23\3\2\2\2fg\7#\2\2gh\7\f\2\2") - buf.write("hi\5\36\20\2i\25\3\2\2\2jk\5\30\r\2kl\5\36\20\2l\27\3") - buf.write("\2\2\2mn\t\2\2\2n\31\3\2\2\2op\t\3\2\2p\33\3\2\2\2qr\7") - buf.write("\23\2\2r\35\3\2\2\2st\b\20\1\2tu\5$\23\2uv\5\36\20\7v") - buf.write("}\3\2\2\2w}\5,\27\2xy\7\t\2\2yz\5\36\20\2z{\7\13\2\2{") - buf.write("}\3\2\2\2|s\3\2\2\2|w\3\2\2\2|x\3\2\2\2}\u0088\3\2\2\2") - buf.write("~\177\f\6\2\2\177\u0080\5 \21\2\u0080\u0081\5\36\20\7") - buf.write("\u0081\u0087\3\2\2\2\u0082\u0083\f\5\2\2\u0083\u0084\5") - buf.write("\"\22\2\u0084\u0085\5\36\20\6\u0085\u0087\3\2\2\2\u0086") - buf.write("~\3\2\2\2\u0086\u0082\3\2\2\2\u0087\u008a\3\2\2\2\u0088") - buf.write("\u0086\3\2\2\2\u0088\u0089\3\2\2\2\u0089\37\3\2\2\2\u008a") - buf.write("\u0088\3\2\2\2\u008b\u008c\t\4\2\2\u008c!\3\2\2\2\u008d") - buf.write("\u008e\t\5\2\2\u008e#\3\2\2\2\u008f\u0090\7\25\2\2\u0090") - buf.write("%\3\2\2\2\u0091\u0092\b\24\1\2\u0092\u0093\7!\2\2\u0093") - buf.write("\u009e\5&\24\7\u0094\u0095\5\36\20\2\u0095\u0096\5(\25") - buf.write("\2\u0096\u0097\5\36\20\2\u0097\u009e\3\2\2\2\u0098\u009e") - buf.write("\7\30\2\2\u0099\u009a\7\t\2\2\u009a\u009b\5&\24\2\u009b") - buf.write("\u009c\7\13\2\2\u009c\u009e\3\2\2\2\u009d\u0091\3\2\2") - buf.write("\2\u009d\u0094\3\2\2\2\u009d\u0098\3\2\2\2\u009d\u0099") - buf.write("\3\2\2\2\u009e\u00a5\3\2\2\2\u009f\u00a0\f\5\2\2\u00a0") - buf.write("\u00a1\5*\26\2\u00a1\u00a2\5&\24\6\u00a2\u00a4\3\2\2\2") - buf.write("\u00a3\u009f\3\2\2\2\u00a4\u00a7\3\2\2\2\u00a5\u00a3\3") - buf.write("\2\2\2\u00a5\u00a6\3\2\2\2\u00a6\'\3\2\2\2\u00a7\u00a5") - buf.write("\3\2\2\2\u00a8\u00a9\t\6\2\2\u00a9)\3\2\2\2\u00aa\u00ab") - buf.write("\t\7\2\2\u00ab+\3\2\2\2\u00ac\u00ad\t\b\2\2\u00ad-\3\2") - buf.write("\2\2\13\64:CG|\u0086\u0088\u009d\u00a5") + buf.write("\4\24\t\24\4\25\t\25\4\26\t\26\4\27\t\27\4\30\t\30\4\31") + buf.write("\t\31\3\2\3\2\3\2\3\3\7\3\67\n\3\f\3\16\3:\13\3\3\4\6") + buf.write("\4=\n\4\r\4\16\4>\3\5\3\5\3\5\3\5\3\5\3\5\3\5\3\5\5\5") + buf.write("I\n\5\3\6\3\6\5\6M\n\6\3\7\3\7\3\7\3\7\3\7\3\7\3\b\3\b") + buf.write("\3\b\3\b\3\b\3\b\3\b\3\b\3\b\3\b\3\t\3\t\3\t\3\t\3\t\3") + buf.write("\t\3\n\3\n\3\n\3\n\3\n\3\n\3\n\3\13\3\13\3\13\3\13\3\f") + buf.write("\3\f\3\f\3\r\3\r\3\16\3\16\3\17\3\17\3\20\3\20\3\20\3") + buf.write("\20\3\20\3\21\3\21\3\22\3\22\3\22\3\22\3\22\3\22\3\22") + buf.write("\3\22\3\22\5\22\u0089\n\22\3\22\3\22\3\22\3\22\3\22\3") + buf.write("\22\3\22\3\22\7\22\u0093\n\22\f\22\16\22\u0096\13\22\3") + buf.write("\23\3\23\3\24\3\24\3\25\3\25\3\26\3\26\3\26\3\26\3\26") + buf.write("\3\26\3\26\3\26\3\26\3\26\3\26\3\26\5\26\u00aa\n\26\3") + buf.write("\26\3\26\3\26\3\26\7\26\u00b0\n\26\f\26\16\26\u00b3\13") + buf.write("\26\3\27\3\27\3\30\3\30\3\31\3\31\3\31\2\4\"*\32\2\4\6") + buf.write("\b\n\f\16\20\22\24\26\30\32\34\36 \"$&(*,.\60\2\n\3\2") + buf.write("\r\20\3\2\21\22\3\2\24\26\3\2\31\33\3\2\27\30\3\2\35\"") + buf.write("\3\2#$\3\2&\'\2\u00b4\2\62\3\2\2\2\48\3\2\2\2\6<\3\2\2") + buf.write("\2\bH\3\2\2\2\nL\3\2\2\2\fN\3\2\2\2\16T\3\2\2\2\20^\3") + buf.write("\2\2\2\22d\3\2\2\2\24k\3\2\2\2\26o\3\2\2\2\30r\3\2\2\2") + buf.write("\32t\3\2\2\2\34v\3\2\2\2\36x\3\2\2\2 }\3\2\2\2\"\u0088") + buf.write("\3\2\2\2$\u0097\3\2\2\2&\u0099\3\2\2\2(\u009b\3\2\2\2") + buf.write("*\u00a9\3\2\2\2,\u00b4\3\2\2\2.\u00b6\3\2\2\2\60\u00b8") + buf.write("\3\2\2\2\62\63\5\4\3\2\63\64\7\2\2\3\64\3\3\2\2\2\65\67") + buf.write("\5\b\5\2\66\65\3\2\2\2\67:\3\2\2\28\66\3\2\2\289\3\2\2") + buf.write("\29\5\3\2\2\2:8\3\2\2\2;=\5\b\5\2<;\3\2\2\2=>\3\2\2\2") + buf.write("><\3\2\2\2>?\3\2\2\2?\7\3\2\2\2@I\5\24\13\2AI\5\n\6\2") + buf.write("BI\5\20\t\2CI\5\26\f\2DI\5\32\16\2EI\5\22\n\2FI\5\34\17") + buf.write("\2GI\5\36\20\2H@\3\2\2\2HA\3\2\2\2HB\3\2\2\2HC\3\2\2\2") + buf.write("HD\3\2\2\2HE\3\2\2\2HF\3\2\2\2HG\3\2\2\2I\t\3\2\2\2JM") + buf.write("\5\f\7\2KM\5\16\b\2LJ\3\2\2\2LK\3\2\2\2M\13\3\2\2\2NO") + buf.write("\7\3\2\2OP\5*\26\2PQ\7\4\2\2QR\5\6\4\2RS\7\5\2\2S\r\3") + buf.write("\2\2\2TU\7\3\2\2UV\5*\26\2VW\7\4\2\2WX\5\6\4\2XY\7\5\2") + buf.write("\2YZ\7\6\2\2Z[\7\4\2\2[\\\5\6\4\2\\]\7\5\2\2]\17\3\2\2") + buf.write("\2^_\7\7\2\2_`\5\60\31\2`a\7\4\2\2ab\5\6\4\2bc\7\5\2\2") + buf.write("c\21\3\2\2\2de\7\b\2\2ef\7\t\2\2fg\5\"\22\2gh\7\n\2\2") + buf.write("hi\5\"\22\2ij\7\13\2\2j\23\3\2\2\2kl\7\'\2\2lm\7\f\2\2") + buf.write("mn\5\"\22\2n\25\3\2\2\2op\5\30\r\2pq\5\"\22\2q\27\3\2") + buf.write("\2\2rs\t\2\2\2s\31\3\2\2\2tu\t\3\2\2u\33\3\2\2\2vw\7\23") + buf.write("\2\2w\35\3\2\2\2xy\5 \21\2yz\7\t\2\2z{\5*\26\2{|\7\13") + buf.write("\2\2|\37\3\2\2\2}~\t\4\2\2~!\3\2\2\2\177\u0080\b\22\1") + buf.write("\2\u0080\u0081\5(\25\2\u0081\u0082\5\"\22\7\u0082\u0089") + buf.write("\3\2\2\2\u0083\u0089\5\60\31\2\u0084\u0085\7\t\2\2\u0085") + buf.write("\u0086\5\"\22\2\u0086\u0087\7\13\2\2\u0087\u0089\3\2\2") + buf.write("\2\u0088\177\3\2\2\2\u0088\u0083\3\2\2\2\u0088\u0084\3") + buf.write("\2\2\2\u0089\u0094\3\2\2\2\u008a\u008b\f\6\2\2\u008b\u008c") + buf.write("\5$\23\2\u008c\u008d\5\"\22\7\u008d\u0093\3\2\2\2\u008e") + buf.write("\u008f\f\5\2\2\u008f\u0090\5&\24\2\u0090\u0091\5\"\22") + buf.write("\6\u0091\u0093\3\2\2\2\u0092\u008a\3\2\2\2\u0092\u008e") + buf.write("\3\2\2\2\u0093\u0096\3\2\2\2\u0094\u0092\3\2\2\2\u0094") + buf.write("\u0095\3\2\2\2\u0095#\3\2\2\2\u0096\u0094\3\2\2\2\u0097") + buf.write("\u0098\t\5\2\2\u0098%\3\2\2\2\u0099\u009a\t\6\2\2\u009a") + buf.write("\'\3\2\2\2\u009b\u009c\7\30\2\2\u009c)\3\2\2\2\u009d\u009e") + buf.write("\b\26\1\2\u009e\u009f\7%\2\2\u009f\u00aa\5*\26\7\u00a0") + buf.write("\u00a1\5\"\22\2\u00a1\u00a2\5,\27\2\u00a2\u00a3\5\"\22") + buf.write("\2\u00a3\u00aa\3\2\2\2\u00a4\u00aa\7\34\2\2\u00a5\u00a6") + buf.write("\7\t\2\2\u00a6\u00a7\5*\26\2\u00a7\u00a8\7\13\2\2\u00a8") + buf.write("\u00aa\3\2\2\2\u00a9\u009d\3\2\2\2\u00a9\u00a0\3\2\2\2") + buf.write("\u00a9\u00a4\3\2\2\2\u00a9\u00a5\3\2\2\2\u00aa\u00b1\3") + buf.write("\2\2\2\u00ab\u00ac\f\5\2\2\u00ac\u00ad\5.\30\2\u00ad\u00ae") + buf.write("\5*\26\6\u00ae\u00b0\3\2\2\2\u00af\u00ab\3\2\2\2\u00b0") + buf.write("\u00b3\3\2\2\2\u00b1\u00af\3\2\2\2\u00b1\u00b2\3\2\2\2") + buf.write("\u00b2+\3\2\2\2\u00b3\u00b1\3\2\2\2\u00b4\u00b5\t\7\2") + buf.write("\2\u00b5-\3\2\2\2\u00b6\u00b7\t\b\2\2\u00b7/\3\2\2\2\u00b8") + buf.write("\u00b9\t\t\2\2\u00b9\61\3\2\2\2\138>HL\u0088\u0092\u0094") + buf.write("\u00a9\u00b1") return buf.getvalue() @@ -86,17 +93,18 @@ class tlangParser ( Parser ): literalNames = [ "", "'if'", "'['", "']'", "'else'", "'repeat'", "'goto'", "'('", "','", "')'", "'='", "'forward'", "'backward'", "'left'", "'right'", "'penup'", "'pendown'", - "'pause'", "'+'", "'-'", "'*'", "'/'", "'pendown?'", - "'<'", "'>'", "'=='", "'!='", "'<='", "'>='", "'&&'", - "'||'", "'!'" ] + "'pause'", "'assert'", "'invariant'", "'assume'", "'+'", + "'-'", "'*'", "'/'", "'%'", "'pendown?'", "'<'", "'>'", + "'=='", "'!='", "'<='", "'>='", "'&&'", "'||'", "'!'" ] symbolicNames = [ "", "", "", "", "", "", "", "", "", "", "", "", "", "", "", "", - "", "", "PLUS", "MINUS", "MUL", - "DIV", "PENCOND", "LT", "GT", "EQ", "NEQ", "LTE", - "GTE", "AND", "OR", "NOT", "NUM", "VAR", "NAME", "Whitespace" ] + "", "", "", "", + "", "PLUS", "MINUS", "MUL", "DIV", "MOD", + "PENCOND", "LT", "GT", "EQ", "NEQ", "LTE", "GTE", + "AND", "OR", "NOT", "NUM", "VAR", "NAME", "Whitespace" ] RULE_start = 0 RULE_instruction_list = 1 @@ -112,21 +120,23 @@ class tlangParser ( Parser ): RULE_moveOp = 11 RULE_penCommand = 12 RULE_pauseCommand = 13 - RULE_expression = 14 - RULE_multiplicative = 15 - RULE_additive = 16 - RULE_unaryArithOp = 17 - RULE_condition = 18 - RULE_binCondOp = 19 - RULE_logicOp = 20 - RULE_value = 21 + RULE_analysisCommand = 14 + RULE_analysisStatement = 15 + RULE_expression = 16 + RULE_multiplicative = 17 + RULE_additive = 18 + RULE_unaryArithOp = 19 + RULE_condition = 20 + RULE_binCondOp = 21 + RULE_logicOp = 22 + RULE_value = 23 ruleNames = [ "start", "instruction_list", "strict_ilist", "instruction", "conditional", "ifConditional", "ifElseConditional", "loop", "gotoCommand", "assignment", "moveCommand", "moveOp", - "penCommand", "pauseCommand", "expression", "multiplicative", - "additive", "unaryArithOp", "condition", "binCondOp", - "logicOp", "value" ] + "penCommand", "pauseCommand", "analysisCommand", "analysisStatement", + "expression", "multiplicative", "additive", "unaryArithOp", + "condition", "binCondOp", "logicOp", "value" ] EOF = Token.EOF T__0=1 @@ -146,24 +156,28 @@ class tlangParser ( Parser ): T__14=15 T__15=16 T__16=17 - PLUS=18 - MINUS=19 - MUL=20 - DIV=21 - PENCOND=22 - LT=23 - GT=24 - EQ=25 - NEQ=26 - LTE=27 - GTE=28 - AND=29 - OR=30 - NOT=31 - NUM=32 - VAR=33 - NAME=34 - Whitespace=35 + T__17=18 + T__18=19 + T__19=20 + PLUS=21 + MINUS=22 + MUL=23 + DIV=24 + MOD=25 + PENCOND=26 + LT=27 + GT=28 + EQ=29 + NEQ=30 + LTE=31 + GTE=32 + AND=33 + OR=34 + NOT=35 + NUM=36 + VAR=37 + NAME=38 + Whitespace=39 def __init__(self, input:TokenStream, output:TextIO = sys.stdout): super().__init__(input, output) @@ -173,6 +187,7 @@ def __init__(self, input:TokenStream, output:TextIO = sys.stdout): + class StartContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -204,9 +219,9 @@ def start(self): self.enterRule(localctx, 0, self.RULE_start) try: self.enterOuterAlt(localctx, 1) - self.state = 44 + self.state = 48 self.instruction_list() - self.state = 45 + self.state = 49 self.match(tlangParser.EOF) except RecognitionException as re: localctx.exception = re @@ -216,6 +231,7 @@ def start(self): self.exitRule() return localctx + class Instruction_listContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -248,13 +264,13 @@ def instruction_list(self): self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 50 + self.state = 54 self._errHandler.sync(self) _la = self._input.LA(1) - while (((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << tlangParser.T__0) | (1 << tlangParser.T__4) | (1 << tlangParser.T__5) | (1 << tlangParser.T__10) | (1 << tlangParser.T__11) | (1 << tlangParser.T__12) | (1 << tlangParser.T__13) | (1 << tlangParser.T__14) | (1 << tlangParser.T__15) | (1 << tlangParser.T__16) | (1 << tlangParser.VAR))) != 0): - self.state = 47 + while (((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << tlangParser.T__0) | (1 << tlangParser.T__4) | (1 << tlangParser.T__5) | (1 << tlangParser.T__10) | (1 << tlangParser.T__11) | (1 << tlangParser.T__12) | (1 << tlangParser.T__13) | (1 << tlangParser.T__14) | (1 << tlangParser.T__15) | (1 << tlangParser.T__16) | (1 << tlangParser.T__17) | (1 << tlangParser.T__18) | (1 << tlangParser.T__19) | (1 << tlangParser.VAR))) != 0): + self.state = 51 self.instruction() - self.state = 52 + self.state = 56 self._errHandler.sync(self) _la = self._input.LA(1) @@ -266,6 +282,7 @@ def instruction_list(self): self.exitRule() return localctx + class Strict_ilistContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -298,16 +315,16 @@ def strict_ilist(self): self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 54 + self.state = 58 self._errHandler.sync(self) _la = self._input.LA(1) while True: - self.state = 53 + self.state = 57 self.instruction() - self.state = 56 + self.state = 60 self._errHandler.sync(self) _la = self._input.LA(1) - if not ((((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << tlangParser.T__0) | (1 << tlangParser.T__4) | (1 << tlangParser.T__5) | (1 << tlangParser.T__10) | (1 << tlangParser.T__11) | (1 << tlangParser.T__12) | (1 << tlangParser.T__13) | (1 << tlangParser.T__14) | (1 << tlangParser.T__15) | (1 << tlangParser.T__16) | (1 << tlangParser.VAR))) != 0)): + if not ((((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << tlangParser.T__0) | (1 << tlangParser.T__4) | (1 << tlangParser.T__5) | (1 << tlangParser.T__10) | (1 << tlangParser.T__11) | (1 << tlangParser.T__12) | (1 << tlangParser.T__13) | (1 << tlangParser.T__14) | (1 << tlangParser.T__15) | (1 << tlangParser.T__16) | (1 << tlangParser.T__17) | (1 << tlangParser.T__18) | (1 << tlangParser.T__19) | (1 << tlangParser.VAR))) != 0)): break except RecognitionException as re: @@ -318,6 +335,7 @@ def strict_ilist(self): self.exitRule() return localctx + class InstructionContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -352,6 +370,10 @@ def pauseCommand(self): return self.getTypedRuleContext(tlangParser.PauseCommandContext,0) + def analysisCommand(self): + return self.getTypedRuleContext(tlangParser.AnalysisCommandContext,0) + + def getRuleIndex(self): return tlangParser.RULE_instruction @@ -369,44 +391,49 @@ def instruction(self): localctx = tlangParser.InstructionContext(self, self._ctx, self.state) self.enterRule(localctx, 6, self.RULE_instruction) try: - self.state = 65 + self.state = 70 self._errHandler.sync(self) token = self._input.LA(1) if token in [tlangParser.VAR]: self.enterOuterAlt(localctx, 1) - self.state = 58 + self.state = 62 self.assignment() pass elif token in [tlangParser.T__0]: self.enterOuterAlt(localctx, 2) - self.state = 59 + self.state = 63 self.conditional() pass elif token in [tlangParser.T__4]: self.enterOuterAlt(localctx, 3) - self.state = 60 + self.state = 64 self.loop() pass elif token in [tlangParser.T__10, tlangParser.T__11, tlangParser.T__12, tlangParser.T__13]: self.enterOuterAlt(localctx, 4) - self.state = 61 + self.state = 65 self.moveCommand() pass elif token in [tlangParser.T__14, tlangParser.T__15]: self.enterOuterAlt(localctx, 5) - self.state = 62 + self.state = 66 self.penCommand() pass elif token in [tlangParser.T__5]: self.enterOuterAlt(localctx, 6) - self.state = 63 + self.state = 67 self.gotoCommand() pass elif token in [tlangParser.T__16]: self.enterOuterAlt(localctx, 7) - self.state = 64 + self.state = 68 self.pauseCommand() pass + elif token in [tlangParser.T__17, tlangParser.T__18, tlangParser.T__19]: + self.enterOuterAlt(localctx, 8) + self.state = 69 + self.analysisCommand() + pass else: raise NoViableAltException(self) @@ -418,6 +445,7 @@ def instruction(self): self.exitRule() return localctx + class ConditionalContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -449,18 +477,18 @@ def conditional(self): localctx = tlangParser.ConditionalContext(self, self._ctx, self.state) self.enterRule(localctx, 8, self.RULE_conditional) try: - self.state = 69 + self.state = 74 self._errHandler.sync(self) la_ = self._interp.adaptivePredict(self._input,3,self._ctx) if la_ == 1: self.enterOuterAlt(localctx, 1) - self.state = 67 + self.state = 72 self.ifConditional() pass elif la_ == 2: self.enterOuterAlt(localctx, 2) - self.state = 68 + self.state = 73 self.ifElseConditional() pass @@ -473,6 +501,7 @@ def conditional(self): self.exitRule() return localctx + class IfConditionalContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -505,15 +534,15 @@ def ifConditional(self): self.enterRule(localctx, 10, self.RULE_ifConditional) try: self.enterOuterAlt(localctx, 1) - self.state = 71 + self.state = 76 self.match(tlangParser.T__0) - self.state = 72 + self.state = 77 self.condition(0) - self.state = 73 + self.state = 78 self.match(tlangParser.T__1) - self.state = 74 + self.state = 79 self.strict_ilist() - self.state = 75 + self.state = 80 self.match(tlangParser.T__2) except RecognitionException as re: localctx.exception = re @@ -523,6 +552,7 @@ def ifConditional(self): self.exitRule() return localctx + class IfElseConditionalContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -558,23 +588,23 @@ def ifElseConditional(self): self.enterRule(localctx, 12, self.RULE_ifElseConditional) try: self.enterOuterAlt(localctx, 1) - self.state = 77 + self.state = 82 self.match(tlangParser.T__0) - self.state = 78 + self.state = 83 self.condition(0) - self.state = 79 + self.state = 84 self.match(tlangParser.T__1) - self.state = 80 + self.state = 85 self.strict_ilist() - self.state = 81 + self.state = 86 self.match(tlangParser.T__2) - self.state = 82 + self.state = 87 self.match(tlangParser.T__3) - self.state = 83 + self.state = 88 self.match(tlangParser.T__1) - self.state = 84 + self.state = 89 self.strict_ilist() - self.state = 85 + self.state = 90 self.match(tlangParser.T__2) except RecognitionException as re: localctx.exception = re @@ -584,6 +614,7 @@ def ifElseConditional(self): self.exitRule() return localctx + class LoopContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -616,15 +647,15 @@ def loop(self): self.enterRule(localctx, 14, self.RULE_loop) try: self.enterOuterAlt(localctx, 1) - self.state = 87 + self.state = 92 self.match(tlangParser.T__4) - self.state = 88 + self.state = 93 self.value() - self.state = 89 + self.state = 94 self.match(tlangParser.T__1) - self.state = 90 + self.state = 95 self.strict_ilist() - self.state = 91 + self.state = 96 self.match(tlangParser.T__2) except RecognitionException as re: localctx.exception = re @@ -634,6 +665,7 @@ def loop(self): self.exitRule() return localctx + class GotoCommandContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -665,17 +697,17 @@ def gotoCommand(self): self.enterRule(localctx, 16, self.RULE_gotoCommand) try: self.enterOuterAlt(localctx, 1) - self.state = 93 + self.state = 98 self.match(tlangParser.T__5) - self.state = 94 + self.state = 99 self.match(tlangParser.T__6) - self.state = 95 + self.state = 100 self.expression(0) - self.state = 96 + self.state = 101 self.match(tlangParser.T__7) - self.state = 97 + self.state = 102 self.expression(0) - self.state = 98 + self.state = 103 self.match(tlangParser.T__8) except RecognitionException as re: localctx.exception = re @@ -685,6 +717,7 @@ def gotoCommand(self): self.exitRule() return localctx + class AssignmentContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -716,11 +749,11 @@ def assignment(self): self.enterRule(localctx, 18, self.RULE_assignment) try: self.enterOuterAlt(localctx, 1) - self.state = 100 + self.state = 105 self.match(tlangParser.VAR) - self.state = 101 + self.state = 106 self.match(tlangParser.T__9) - self.state = 102 + self.state = 107 self.expression(0) except RecognitionException as re: localctx.exception = re @@ -730,6 +763,7 @@ def assignment(self): self.exitRule() return localctx + class MoveCommandContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -762,9 +796,9 @@ def moveCommand(self): self.enterRule(localctx, 20, self.RULE_moveCommand) try: self.enterOuterAlt(localctx, 1) - self.state = 104 + self.state = 109 self.moveOp() - self.state = 105 + self.state = 110 self.expression(0) except RecognitionException as re: localctx.exception = re @@ -774,6 +808,7 @@ def moveCommand(self): self.exitRule() return localctx + class MoveOpContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -800,7 +835,7 @@ def moveOp(self): self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 107 + self.state = 112 _la = self._input.LA(1) if not((((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << tlangParser.T__10) | (1 << tlangParser.T__11) | (1 << tlangParser.T__12) | (1 << tlangParser.T__13))) != 0)): self._errHandler.recoverInline(self) @@ -815,6 +850,7 @@ def moveOp(self): self.exitRule() return localctx + class PenCommandContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -841,7 +877,7 @@ def penCommand(self): self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 109 + self.state = 114 _la = self._input.LA(1) if not(_la==tlangParser.T__14 or _la==tlangParser.T__15): self._errHandler.recoverInline(self) @@ -856,6 +892,7 @@ def penCommand(self): self.exitRule() return localctx + class PauseCommandContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -881,7 +918,7 @@ def pauseCommand(self): self.enterRule(localctx, 26, self.RULE_pauseCommand) try: self.enterOuterAlt(localctx, 1) - self.state = 111 + self.state = 116 self.match(tlangParser.T__16) except RecognitionException as re: localctx.exception = re @@ -891,6 +928,98 @@ def pauseCommand(self): self.exitRule() return localctx + + class AnalysisCommandContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def analysisStatement(self): + return self.getTypedRuleContext(tlangParser.AnalysisStatementContext,0) + + + def condition(self): + return self.getTypedRuleContext(tlangParser.ConditionContext,0) + + + def getRuleIndex(self): + return tlangParser.RULE_analysisCommand + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitAnalysisCommand" ): + return visitor.visitAnalysisCommand(self) + else: + return visitor.visitChildren(self) + + + + + def analysisCommand(self): + + localctx = tlangParser.AnalysisCommandContext(self, self._ctx, self.state) + self.enterRule(localctx, 28, self.RULE_analysisCommand) + try: + self.enterOuterAlt(localctx, 1) + self.state = 118 + self.analysisStatement() + self.state = 119 + self.match(tlangParser.T__6) + self.state = 120 + self.condition(0) + self.state = 121 + self.match(tlangParser.T__8) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class AnalysisStatementContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + + def getRuleIndex(self): + return tlangParser.RULE_analysisStatement + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitAnalysisStatement" ): + return visitor.visitAnalysisStatement(self) + else: + return visitor.visitChildren(self) + + + + + def analysisStatement(self): + + localctx = tlangParser.AnalysisStatementContext(self, self._ctx, self.state) + self.enterRule(localctx, 30, self.RULE_analysisStatement) + self._la = 0 # Token type + try: + self.enterOuterAlt(localctx, 1) + self.state = 123 + _la = self._input.LA(1) + if not((((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << tlangParser.T__17) | (1 << tlangParser.T__18) | (1 << tlangParser.T__19))) != 0)): + self._errHandler.recoverInline(self) + else: + self._errHandler.reportMatch(self) + self.consume() + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + class ExpressionContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -1012,11 +1141,11 @@ def expression(self, _p:int=0): _parentState = self.state localctx = tlangParser.ExpressionContext(self, self._ctx, _parentState) _prevctx = localctx - _startState = 28 - self.enterRecursionRule(localctx, 28, self.RULE_expression, _p) + _startState = 32 + self.enterRecursionRule(localctx, 32, self.RULE_expression, _p) try: self.enterOuterAlt(localctx, 1) - self.state = 122 + self.state = 134 self._errHandler.sync(self) token = self._input.LA(1) if token in [tlangParser.MINUS]: @@ -1024,34 +1153,34 @@ def expression(self, _p:int=0): self._ctx = localctx _prevctx = localctx - self.state = 114 + self.state = 126 self.unaryArithOp() - self.state = 115 + self.state = 127 self.expression(5) pass elif token in [tlangParser.NUM, tlangParser.VAR]: localctx = tlangParser.ValueExprContext(self, localctx) self._ctx = localctx _prevctx = localctx - self.state = 117 + self.state = 129 self.value() pass elif token in [tlangParser.T__6]: localctx = tlangParser.ParenExprContext(self, localctx) self._ctx = localctx _prevctx = localctx - self.state = 118 + self.state = 130 self.match(tlangParser.T__6) - self.state = 119 + self.state = 131 self.expression(0) - self.state = 120 + self.state = 132 self.match(tlangParser.T__8) pass else: raise NoViableAltException(self) self._ctx.stop = self._input.LT(-1) - self.state = 134 + self.state = 146 self._errHandler.sync(self) _alt = self._interp.adaptivePredict(self._input,6,self._ctx) while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER: @@ -1059,37 +1188,37 @@ def expression(self, _p:int=0): if self._parseListeners is not None: self.triggerExitRuleEvent() _prevctx = localctx - self.state = 132 + self.state = 144 self._errHandler.sync(self) la_ = self._interp.adaptivePredict(self._input,5,self._ctx) if la_ == 1: localctx = tlangParser.MulExprContext(self, tlangParser.ExpressionContext(self, _parentctx, _parentState)) self.pushNewRecursionContext(localctx, _startState, self.RULE_expression) - self.state = 124 + self.state = 136 if not self.precpred(self._ctx, 4): from antlr4.error.Errors import FailedPredicateException raise FailedPredicateException(self, "self.precpred(self._ctx, 4)") - self.state = 125 + self.state = 137 self.multiplicative() - self.state = 126 + self.state = 138 self.expression(5) pass elif la_ == 2: localctx = tlangParser.AddExprContext(self, tlangParser.ExpressionContext(self, _parentctx, _parentState)) self.pushNewRecursionContext(localctx, _startState, self.RULE_expression) - self.state = 128 + self.state = 140 if not self.precpred(self._ctx, 3): from antlr4.error.Errors import FailedPredicateException raise FailedPredicateException(self, "self.precpred(self._ctx, 3)") - self.state = 129 + self.state = 141 self.additive() - self.state = 130 + self.state = 142 self.expression(4) pass - self.state = 136 + self.state = 148 self._errHandler.sync(self) _alt = self._interp.adaptivePredict(self._input,6,self._ctx) @@ -1101,6 +1230,7 @@ def expression(self, _p:int=0): self.unrollRecursionContexts(_parentctx) return localctx + class MultiplicativeContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -1113,6 +1243,9 @@ def MUL(self): def DIV(self): return self.getToken(tlangParser.DIV, 0) + def MOD(self): + return self.getToken(tlangParser.MOD, 0) + def getRuleIndex(self): return tlangParser.RULE_multiplicative @@ -1128,13 +1261,13 @@ def accept(self, visitor:ParseTreeVisitor): def multiplicative(self): localctx = tlangParser.MultiplicativeContext(self, self._ctx, self.state) - self.enterRule(localctx, 30, self.RULE_multiplicative) + self.enterRule(localctx, 34, self.RULE_multiplicative) self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 137 + self.state = 149 _la = self._input.LA(1) - if not(_la==tlangParser.MUL or _la==tlangParser.DIV): + if not((((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << tlangParser.MUL) | (1 << tlangParser.DIV) | (1 << tlangParser.MOD))) != 0)): self._errHandler.recoverInline(self) else: self._errHandler.reportMatch(self) @@ -1147,6 +1280,7 @@ def multiplicative(self): self.exitRule() return localctx + class AdditiveContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -1174,11 +1308,11 @@ def accept(self, visitor:ParseTreeVisitor): def additive(self): localctx = tlangParser.AdditiveContext(self, self._ctx, self.state) - self.enterRule(localctx, 32, self.RULE_additive) + self.enterRule(localctx, 36, self.RULE_additive) self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 139 + self.state = 151 _la = self._input.LA(1) if not(_la==tlangParser.PLUS or _la==tlangParser.MINUS): self._errHandler.recoverInline(self) @@ -1193,6 +1327,7 @@ def additive(self): self.exitRule() return localctx + class UnaryArithOpContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -1217,10 +1352,10 @@ def accept(self, visitor:ParseTreeVisitor): def unaryArithOp(self): localctx = tlangParser.UnaryArithOpContext(self, self._ctx, self.state) - self.enterRule(localctx, 34, self.RULE_unaryArithOp) + self.enterRule(localctx, 38, self.RULE_unaryArithOp) try: self.enterOuterAlt(localctx, 1) - self.state = 141 + self.state = 153 self.match(tlangParser.MINUS) except RecognitionException as re: localctx.exception = re @@ -1230,6 +1365,7 @@ def unaryArithOp(self): self.exitRule() return localctx + class ConditionContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -1280,46 +1416,46 @@ def condition(self, _p:int=0): _parentState = self.state localctx = tlangParser.ConditionContext(self, self._ctx, _parentState) _prevctx = localctx - _startState = 36 - self.enterRecursionRule(localctx, 36, self.RULE_condition, _p) + _startState = 40 + self.enterRecursionRule(localctx, 40, self.RULE_condition, _p) try: self.enterOuterAlt(localctx, 1) - self.state = 155 + self.state = 167 self._errHandler.sync(self) la_ = self._interp.adaptivePredict(self._input,7,self._ctx) if la_ == 1: - self.state = 144 + self.state = 156 self.match(tlangParser.NOT) - self.state = 145 + self.state = 157 self.condition(5) pass elif la_ == 2: - self.state = 146 + self.state = 158 self.expression(0) - self.state = 147 + self.state = 159 self.binCondOp() - self.state = 148 + self.state = 160 self.expression(0) pass elif la_ == 3: - self.state = 150 + self.state = 162 self.match(tlangParser.PENCOND) pass elif la_ == 4: - self.state = 151 + self.state = 163 self.match(tlangParser.T__6) - self.state = 152 + self.state = 164 self.condition(0) - self.state = 153 + self.state = 165 self.match(tlangParser.T__8) pass self._ctx.stop = self._input.LT(-1) - self.state = 163 + self.state = 175 self._errHandler.sync(self) _alt = self._interp.adaptivePredict(self._input,8,self._ctx) while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER: @@ -1329,15 +1465,15 @@ def condition(self, _p:int=0): _prevctx = localctx localctx = tlangParser.ConditionContext(self, _parentctx, _parentState) self.pushNewRecursionContext(localctx, _startState, self.RULE_condition) - self.state = 157 + self.state = 169 if not self.precpred(self._ctx, 3): from antlr4.error.Errors import FailedPredicateException raise FailedPredicateException(self, "self.precpred(self._ctx, 3)") - self.state = 158 + self.state = 170 self.logicOp() - self.state = 159 + self.state = 171 self.condition(4) - self.state = 165 + self.state = 177 self._errHandler.sync(self) _alt = self._interp.adaptivePredict(self._input,8,self._ctx) @@ -1349,6 +1485,7 @@ def condition(self, _p:int=0): self.unrollRecursionContexts(_parentctx) return localctx + class BinCondOpContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -1388,11 +1525,11 @@ def accept(self, visitor:ParseTreeVisitor): def binCondOp(self): localctx = tlangParser.BinCondOpContext(self, self._ctx, self.state) - self.enterRule(localctx, 38, self.RULE_binCondOp) + self.enterRule(localctx, 42, self.RULE_binCondOp) self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 166 + self.state = 178 _la = self._input.LA(1) if not((((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << tlangParser.LT) | (1 << tlangParser.GT) | (1 << tlangParser.EQ) | (1 << tlangParser.NEQ) | (1 << tlangParser.LTE) | (1 << tlangParser.GTE))) != 0)): self._errHandler.recoverInline(self) @@ -1407,6 +1544,7 @@ def binCondOp(self): self.exitRule() return localctx + class LogicOpContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -1434,11 +1572,11 @@ def accept(self, visitor:ParseTreeVisitor): def logicOp(self): localctx = tlangParser.LogicOpContext(self, self._ctx, self.state) - self.enterRule(localctx, 40, self.RULE_logicOp) + self.enterRule(localctx, 44, self.RULE_logicOp) self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 168 + self.state = 180 _la = self._input.LA(1) if not(_la==tlangParser.AND or _la==tlangParser.OR): self._errHandler.recoverInline(self) @@ -1453,6 +1591,7 @@ def logicOp(self): self.exitRule() return localctx + class ValueContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -1480,11 +1619,11 @@ def accept(self, visitor:ParseTreeVisitor): def value(self): localctx = tlangParser.ValueContext(self, self._ctx, self.state) - self.enterRule(localctx, 42, self.RULE_value) + self.enterRule(localctx, 46, self.RULE_value) self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 170 + self.state = 182 _la = self._input.LA(1) if not(_la==tlangParser.NUM or _la==tlangParser.VAR): self._errHandler.recoverInline(self) @@ -1504,8 +1643,8 @@ def value(self): def sempred(self, localctx:RuleContext, ruleIndex:int, predIndex:int): if self._predicates == None: self._predicates = dict() - self._predicates[14] = self.expression_sempred - self._predicates[18] = self.condition_sempred + self._predicates[16] = self.expression_sempred + self._predicates[20] = self.condition_sempred pred = self._predicates.get(ruleIndex, None) if pred is None: raise Exception("No predicate with index:" + str(ruleIndex)) diff --git a/ChironCore/turtparse/tlangVisitor.py b/ChironCore/turtparse/tlangVisitor.py index 7ac289a..0784283 100644 --- a/ChironCore/turtparse/tlangVisitor.py +++ b/ChironCore/turtparse/tlangVisitor.py @@ -79,6 +79,16 @@ def visitPauseCommand(self, ctx:tlangParser.PauseCommandContext): return self.visitChildren(ctx) + # Visit a parse tree produced by tlangParser#analysisCommand. + def visitAnalysisCommand(self, ctx:tlangParser.AnalysisCommandContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by tlangParser#analysisStatement. + def visitAnalysisStatement(self, ctx:tlangParser.AnalysisStatementContext): + return self.visitChildren(ctx) + + # Visit a parse tree produced by tlangParser#unaryExpr. def visitUnaryExpr(self, ctx:tlangParser.UnaryExprContext): return self.visitChildren(ctx)