diff --git a/.gitignore b/.gitignore index 3e9dcb3..d42b920 100644 --- a/.gitignore +++ b/.gitignore @@ -162,4 +162,6 @@ cython_debug/ # Extra files and hidden folder. testcases/ -build/ \ No newline at end of file +build/ + +*.png \ No newline at end of file diff --git a/BMC.md b/BMC.md new file mode 100644 index 0000000..200f1c1 --- /dev/null +++ b/BMC.md @@ -0,0 +1,100 @@ +# Bounded Model Checker (BMC) of Chiron + +## Introduction + +A Bounded Model Checker (BMC) engine is a verification tool used to check the satisfiability of a condition within a given bound without actually running the code. It systematically explores all possible states of a system up to a specified depth to detect errors. + +The BMC engine works by encoding the system's behavior and the properties to be verified into a logical formula. This formula is then solved using a SAT (Satisfiability) solver. If the solver finds a solution within the bounds, it indicates a counterexample that demonstrates a violation of the property being checked. If no solution is found within the given bound, the system is considered correct up to the bounds. + +### What makes BMC interesting + +The BMC engine provides an automated approach to verify the correctness of complex systems. Unlike traditional testing, which relies on specific test cases, BMC explores all possible states within a given bound, ensuring thorough coverage. This makes it particularly effective in uncovering subtle bugs that might be missed by conventional methods. + +The use of SAT solvers to encode and solve logical formulas demonstrates the power of combining formal methods with computational tools. The ability to detect counterexamples and provide concrete scenarios where a property fails is invaluable for debugging and improving system reliability. + +Moreover, BMC's ability to handle constraints, conditions, and configurations, including loop unrolling and custom angle restrictions, makes it a versatile tool for diverse software verification applications. + +## How to use Chiron BMC + +### Adding Bounds +We can restrict the domain of variables by `assume` statements. For example: +- `assume :x >= 0` bounds the domain of variable `:x` in the positive side of number line +- `assume :x*:x + :y*:y <= r*r` restricts the point `(:x, :y)` inside the circle of radius `r`. + +### Adding Conditions +We add the conditions to be checked by `assert` statements. For example: +- `assert :x >= 0 && :y >= 0` checks whether the point `(:x, :y)` lies in the first quadrant +- `assert :x*:x + :y*:y >= r*r` checks whether the point `(:x, :y)` lies outside the circle of radius `r`. + +### Handling Loops + +Loops in the code are managed through a technique called **loop unrolling**. Loop unrolling involves replicating the loop's body multiple times, constrained by a specified unroll bound. For the purpose of understaning unrolling, we store the unrolled code in file `unrolled_code.tl`. + +### Adding Loop Unroll Bound +`-ub ` is used to set the unroll bound of loops. By default, it is set to 10. + +A custom unroll bound for a particular loop can be set by using the `@unroll` decorator. For example, +```c +@unroll repeat [ + ... +] +``` + +### Tracking Position of Turtle +We assume that turle starts at position $(0, 0)$ and facing at $0^\circ$ angle with respect to the positive direction of $x$-axis. The position of turtle is maintained by the variables `:turtleX` ($x$-coordinate), `:turtleY` ($y$-coordinate) and `:turtleThetaDeg` (angle in degrees). + +### Adding Angle Constraints +By default, the turtle can face towards $0^\circ$, $90^\circ$, $180^\circ$ and $270^\circ$. Custom angles can be added by maintaining a configuration file that specifies the angles along with their cosine and sine values in the following format: + +```plaintext +, , +, , +... +``` + +This configuration file is then passed to the BMC engine using the `-aconf ` argument. + +### Tracking Pen State +The variable `:turtlePen` is used to maintain the up/down state of pen. +- `:turtlePen = 0` indicates pendown state +- `:turtlePen = 1` indicates penup state + +At the start of the program, pen is in pendown state. + +## Examples +Examples demonstrating working of the BMC engine with explaination are provided in the `/ChironCore/bmc_examples/` directory. To run the BMC engine on these test cases, navigate to the `ChironCore` directory and execute the following command: + +```bash +./chiron.py -bmc -ub -aconf +``` +where `-ub` and `-aconf` are optional arguments + +## Implementation Methodology +We have added support for `assume` statement, `assert` statement, `modulo` operator, `float` numbers, `single line comments` and `multi-line comments` to Chiron. We have also added code to convert Chiron Intermediate Representation (IR) into Three Address Code (TAC) and Static Single Assignment (SSA). + +The working of BMC engine is explained as follows: + +1. **Loop Unrolling**: + All the loops of the code are unrolled based on the unroll bound and the unrolled code is used for further processing. + +2. **Converting Chiron IR into TAC**: + The Chiron IR of the unrolled code is generated and is transformed into TAC to simplify the representation of operations and facilitate further analysis. We show the TAC in `tac_cfg.png`. + +3. **Generating SSA**: + The TAC is converted into SSA form to simplify data flow analysis and accurately track variable dependencies and states throughout the program. We show the SSA in `ssa_cfg.png`. + +4. **SAT Solver Integration**: + The SSA form is translated into SMT-LIB statements. This process encodes the constraints, conditions, and properties into a series of logical assertions and declarations to accurately represent the program's semantics. These statements are then checked for satisfiability using the Z3 solver. + +5. **Reporting Results**: + - **Checking tightness of bounds**: + The BMC engine verifies if a solution exists within the given bounds. If no solution is found, it suggests relaxing the bounds. + + - **Checking satisfiability under all bounds**: + The BMC engine checks satisfiability until either a counterexample is found or all possible states of the program within the specified bounds are exhausted. If no violations are detected, the system is considered correct up to the given bounds. + + - **Counter Example generation**: + If the BMC engine detects a violation, it generates a counterexample for the input variables. + +## Acknowledgement +We express our gratitude to Professor Subhajit Roy and Chiron team for their unwavering guidance and support throughout the duration of this project. Their assistance significantly influenced the course of our journey, making it markedly distinct from what it would have been otherwise. \ No newline at end of file diff --git a/ChironCore/ChironAST/ChironAST.py b/ChironCore/ChironAST/ChironAST.py index f86c5da..5380ebc 100644 --- a/ChironCore/ChironAST/ChironAST.py +++ b/ChironCore/ChironAST/ChironAST.py @@ -28,7 +28,6 @@ def __init__(self, condition): def __str__(self): return self.cond.__str__() -# Not Implemented Yet. class AssertCommand(Instruction): def __init__(self, condition): self.cond = condition @@ -36,6 +35,13 @@ def __init__(self, condition): def __str__(self): return self.cond.__str__() +class AssumeCommand(Instruction): + def __init__(self, condition): + self.cond = condition + + def __str__(self): + return self.cond.__str__() + class MoveCommand(Instruction): def __init__(self, motion, expr): self.direction = motion @@ -126,6 +132,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----------------------------------------------- @@ -221,7 +231,7 @@ class Value(Expression): class Num(Value): def __init__(self, v): - self.val = int(v) + self.val = float(v) def __str__(self): return str(self.val) diff --git a/ChironCore/ChironAST/builder.py b/ChironCore/ChironAST/builder.py index b38265e..80ce294 100644 --- a/ChironCore/ChironAST/builder.py +++ b/ChironCore/ChironAST/builder.py @@ -88,6 +88,14 @@ def visitMulExpr(self, ctx:tlangParser.MulExprContext): return ChironAST.Mult(left, right) elif ctx.multiplicative().DIV(): return ChironAST.Div(left, right) + + + # Visit a parse tree produced by tlangParser#valueExpr. + def visitModExpr(self, ctx:tlangParser.ModExprContext): + left = self.visit(ctx.expression(0)) + right = self.visit(ctx.expression(1)) + if ctx.modulo().MOD(): + return ChironAST.Mod(left, right) # Visit a parse tree produced by tlangParser#parenExpr. @@ -142,6 +150,8 @@ def visitCondition(self, ctx:tlangParser.ConditionContext): def visitValue(self, ctx:tlangParser.ValueContext): if ctx.NUM(): return ChironAST.Num(ctx.NUM().getText()) + elif ctx.FLOAT(): + return ChironAST.Num(ctx.FLOAT().getText()) elif ctx.VAR(): return ChironAST.Var(ctx.VAR().getText()) @@ -172,3 +182,10 @@ def visitMoveCommand(self, ctx:tlangParser.MoveCommandContext): def visitPenCommand(self, ctx:tlangParser.PenCommandContext): return [(ChironAST.PenCommand(ctx.getText()), 1)] + + def visitAssertionCommand(self, ctx:tlangParser.AssertionCommandContext): + return [(ChironAST.AssertCommand(self.visit(ctx.condition())), 1)] + + def visitAssumeCommand(self, ctx:tlangParser.AssumeCommandContext): + return [(ChironAST.AssumeCommand(self.visit(ctx.condition())), 1)] + diff --git a/ChironCore/ChironSSA/ChironSSA.py b/ChironCore/ChironSSA/ChironSSA.py new file mode 100644 index 0000000..80d6632 --- /dev/null +++ b/ChironCore/ChironSSA/ChironSSA.py @@ -0,0 +1,225 @@ +# Static Single Assignment (SSA) generation for Chiron +class SSA(object): + pass + +# Instruction Classes +class Instruction(SSA): + pass + +class CosCommand(Instruction): + def __init__(self, lvar, rvar): # lvar = cos(rvar) + self.lvar = lvar + self.rvar = rvar + + def __str__(self): + return self.lvar.__str__() + " = cos(" + self.rvar.__str__() + ")" + +class SinCommand(Instruction): + def __init__(self, lvar, rvar): # lvar = sin(rvar) + self.lvar = lvar + self.rvar = rvar + + def __str__(self): + return self.lvar.__str__() + " = sin(" + self.rvar.__str__() + ")" + +class PhiCommand(Instruction): + def __init__(self, lvar, rvars): + self.lvar = lvar + self.rvars = rvars + + def __str__(self): + return self.lvar.__str__() + " = PHI (" + ", ".join([var.__str__() for var in list(self.rvars)]) + ")" + +class AssignmentCommand(Instruction): + def __init__(self, lvar, rvar1, rvar2, op): + self.lvar = lvar + self.rvar1 = rvar1 + self.rvar2 = rvar2 + self.op = op + + def __str__(self): + return self.lvar.__str__() + " = " + self.rvar1.__str__() + " " + self.op + " " + self.rvar2.__str__() + +class ConditionCommand(Instruction): + def __init__(self, condition): + self.cond = condition + + def __str__(self): + return "BRANCH: " + self.cond.__str__() + +class AssertCommand(Instruction): + def __init__(self, condition): + self.cond = condition + + def __str__(self): + return "ASSERT: " + self.cond.__str__() + +class AssumeCommand(Instruction): + def __init__(self, condition): + self.cond = condition + + def __str__(self): + return "ASSUME: " + self.cond.__str__() + +class MoveCommand(Instruction): + def __init__(self, motion, var): + self.direction = motion + self.var = var + + def __str__(self): + return "MOVE: " + self.direction + " " + self.var.__str__() + +class PenCommand(Instruction): + def __init__(self, penstat): + self.status = penstat + + def __str__(self): + return "PEN: " + self.status + +class GotoCommand(Instruction): + def __init__(self, x, y): + self.xcor = x + self.ycor = y + + def __str__(self): + return "goto " + str(self.xcor) + " " + str(self.ycor) + +class NoOpCommand(Instruction): + def __str__(self): + return "NoOp" + +class PauseCommand(Instruction): + def __str__(self): + return "Pause" + + +class Expression(SSA): + pass +# -- Arithmetic Expressions ------------------------------------------ +class ArithExpr(Expression): + pass + +class BinArithOp(ArithExpr): + def __init__(self, lvar, rvar, op): + self.lvar = lvar + self.rvar = rvar + self.op = op + + def __str__(self): + return self.lvar.__str__() + " " + self.op + " " + self.rvar.__str__() + +class Sum(BinArithOp): + def __init__(self, lvar, rvar): + BinArithOp.__init__(self, lvar, rvar, "+") + +class Sub(BinArithOp): + def __init__(self, lvar, rvar): + BinArithOp.__init__(self, lvar, rvar, "-") + +class Mul(BinArithOp): + def __init__(self, lvar, rvar): + BinArithOp.__init__(self, lvar, rvar, "*") + +class Div(BinArithOp): + def __init__(self, lvar, rvar): + BinArithOp.__init__(self, lvar, rvar, "/") + + +class UnaryArithOp(ArithExpr): + def __init__(self, op, var): + self.op = op + self.var = var + + def __str__(self): + return self.op + " " + self.var.__str__() + +class UMinus(UnaryArithOp): + def __init__(self, var): + UnaryArithOp.__init__(self, "-", var) + + +# -- Boolean Expressions -------------------------------------------- +class BoolExpr(Expression): + pass + +class BinBoolOp(BoolExpr): + def __init__(self, lvar, rvar, op): + self.lvar = lvar + self.rvar = rvar + self.op = op + + def __str__(self): + return self.lvar.__str__() + " " + self.op + " " + self.rvar.__str__() + +class And(BinBoolOp): + def __init__(self, lvar, rvar): + BinBoolOp.__init__(self, lvar, rvar, "and") + +class Or(BinBoolOp): + def __init__(self, lvar, rvar): + BinBoolOp.__init__(self, lvar, rvar, "or") + +class LT(BinBoolOp): + def __init__(self, lvar, rvar): + BinBoolOp.__init__(self, lvar, rvar, "<") + +class GT(BinBoolOp): + def __init__(self, lvar, rvar): + BinBoolOp.__init__(self, lvar, rvar, ">") + +class LTE(BinBoolOp): + def __init__(self, lvar, rvar): + BinBoolOp.__init__(self, lvar, rvar, "<=") + +class GTE(BinBoolOp): + def __init__(self, lvar, rvar): + BinBoolOp.__init__(self, lvar, rvar, ">=") + +class EQ(BinBoolOp): + def __init__(self, lvar, rvar): + BinBoolOp.__init__(self, lvar, rvar, "==") + +class NEQ(BinBoolOp): + def __init__(self, lvar, rvar): + BinBoolOp.__init__(self, lvar, rvar, "!=") + +class Not(BoolExpr): + def __init__(self, var): + self.var = var + + def __str__(self): + return "not " + self.var.__str__() + +class PenStatus(Expression): + def __str__(self): + return "penstatus" + +class BoolTrue(Expression): + def __str__(self): + return "true" + +class BoolFalse(Expression): + def __str__(self): + return "false" + +# -- Value Expressions ---------------------------------------------- +class Value(Expression): + pass + +class Num(Value): + def __init__(self, value): + self.value = value + + def __str__(self): + return str(self.value) + +class Var(Value): + def __init__(self, name): + self.name = name + + def __str__(self): + return self.name + +class Unused(Value): + def __str__(self): + return "" diff --git a/ChironCore/ChironSSA/builder.py b/ChironCore/ChironSSA/builder.py new file mode 100644 index 0000000..3b03789 --- /dev/null +++ b/ChironCore/ChironSSA/builder.py @@ -0,0 +1,251 @@ + +from numpy import format_float_scientific +from ChironSSA import ChironSSA +from cfg import cfgBuilder +import ChironTAC.ChironTAC as ChironTAC +import ChironSSA.ChironSSA as ChironSSA +import cfg.ChironCFG as ChironCFG +import networkx as nx +import copy +import collections + +class SSABuilder: + def __init__(self, ir): + self.convert(ir) + self.cfg, self.line2BlockMap = cfgBuilder.buildCFG(ir) + self.globals = set() + self.blocksMap = collections.defaultdict(set) + self.counter = collections.defaultdict(int) + self.stack = collections.defaultdict(list) + + def build(self): + self.cfg.compute_dominance() + self.insert_phi_nodes() + self.rename_variables() + self.remove_empty_and_duplicate_phi() + + return self.cfg + + def remove_empty_and_duplicate_phi(self): + for block in self.cfg.nodes(): + for instr, _ in block.instrlist: + if isinstance(instr, ChironSSA.PhiCommand): + if len(instr.rvars) == 0: + block.instrlist.remove((instr, None)) + else: + rvars = [[int(rvar.name.split('$')[-1]), rvar.name] for rvar in instr.rvars] + rvars.sort(key=lambda x: x[0]) + instr.rvars = [ChironSSA.Var(rvars[0][1])] + for i in range(1, len(rvars)): + if rvars[i][1] != rvars[i-1][1]: + instr.rvars.append(ChironSSA.Var(rvars[i][1])) + + def rename_variables(self): + for var in self.globals: + self.counter[var] = 0 + self.stack[var] = [] + + entry = None + for block in self.cfg.nodes(): + if block.name == "START": + entry = block + break + + self.rename(entry) + + def rename(self, block): + temp = set() + for instr, _ in block.instrlist: + if isinstance(instr, ChironSSA.PhiCommand): + temp.add(instr.lvar.name) + instr.lvar = self.new_name(instr.lvar.name) + + elif isinstance(instr, ChironSSA.AssignmentCommand): + if isinstance(instr.rvar1, ChironSSA.Var): + instr.rvar1 = ChironSSA.Var(instr.rvar1.name + "$" + str(self.stack[instr.rvar1.name][-1])) + if isinstance(instr.rvar2, ChironSSA.Var): + instr.rvar2 = ChironSSA.Var(instr.rvar2.name + "$" + str(self.stack[instr.rvar2.name][-1])) + temp.add(instr.lvar.name) + instr.lvar = self.new_name(instr.lvar.name) + + elif isinstance(instr, ChironSSA.AssertCommand): + if isinstance(instr.cond, ChironSSA.Var): + instr.cond = ChironSSA.Var(instr.cond.name + "$" + str(self.stack[instr.cond.name][-1])) + + elif isinstance(instr, ChironSSA.AssumeCommand): + if isinstance(instr.cond, ChironSSA.Var): + instr.cond = ChironSSA.Var(instr.cond.name + "$" + str(self.stack[instr.cond.name][-1])) + + elif isinstance(instr, ChironSSA.ConditionCommand): + if isinstance(instr.cond, ChironSSA.Var): + instr.cond = ChironSSA.Var(instr.cond.name + "$" + str(self.stack[instr.cond.name][-1])) + + elif isinstance(instr, ChironSSA.MoveCommand): + if isinstance(instr.var, ChironSSA.Var): + instr.var = ChironSSA.Var(instr.var.name + "$" + str(self.stack[instr.var.name][-1])) + + elif isinstance(instr, ChironSSA.GotoCommand): + if isinstance(instr.xcor, ChironSSA.Var): + instr.xcor = ChironSSA.Var(instr.xcor.name + "$" + str(self.stack[instr.xcor.name][-1])) + if isinstance(instr.ycor, ChironSSA.Var): + instr.ycor = ChironSSA.Var(instr.ycor.name + "$" + str(self.stack[instr.ycor.name][-1])) + + elif isinstance(instr, ChironSSA.SinCommand): + temp.add(instr.lvar.name) + instr.lvar = self.new_name(instr.lvar.name) + if isinstance(instr.rvar, ChironSSA.Var): + instr.rvar = ChironSSA.Var(instr.rvar.name + "$" + str(self.stack[instr.rvar.name][-1])) + + elif isinstance(instr, ChironSSA.CosCommand): + temp.add(instr.lvar.name) + instr.lvar = self.new_name(instr.lvar.name) + if isinstance(instr.rvar, ChironSSA.Var): + instr.rvar = ChironSSA.Var(instr.rvar.name + "$" + str(self.stack[instr.rvar.name][-1])) + + visited = set() + def phi_dfs(curr, var): + visited.add(curr) + flag = False + for instr, _ in curr.instrlist: + if isinstance(instr, ChironSSA.PhiCommand): + if instr.lvar.name == var: + instr.rvars.append(ChironSSA.Var(instr.lvar.name + "$" + str(self.stack[instr.lvar.name][-1]))) + flag = True + if isinstance(instr, ChironSSA.AssignmentCommand): + if instr.lvar.name == var: + flag = True + + if not flag: + for next in self.cfg.successors(curr): + if next in visited: + continue + phi_dfs(next, var) + + for next in self.cfg.successors(block): + for var in temp: + visited.clear() + phi_dfs(next, var) + + for next in self.cfg.dominator_tree[block]: + self.rename(next) + + for var in temp: + self.stack[var].pop() + + def new_name(self, var): + i = self.counter[var] + self.counter[var] += 1 + self.stack[var].append(i) + return ChironSSA.Var(var + "$" + str(i)) + + def insert_phi_nodes(self): + for var in self.get_globals(): + if var not in self.blocksMap: + continue + + worklist = self.blocksMap[var] + while len(worklist) > 0: + block = worklist.pop() + for next in self.cfg.df[block]: + found = False + for instr, _ in next.instrlist: + if isinstance(instr, ChironSSA.PhiCommand) and instr.lvar.name == var: + found = True + break + + if not found: + phi = ChironSSA.PhiCommand(ChironSSA.Var(var), []) + next.instrlist.insert(0, (phi, None)) + worklist.add(next) + + def get_globals(self): + if len(self.globals) > 0: + return self.globals + + for block in self.cfg.nodes(): + varkill = set() + for instr, _ in block.instrlist: + if isinstance(instr, ChironSSA.AssignmentCommand): + if isinstance(instr.rvar1, ChironSSA.Var) and instr.rvar1.name not in varkill: + self.globals.add(instr.rvar1.name) + if isinstance(instr.rvar2, ChironSSA.Var) and instr.rvar2.name not in varkill: + self.globals.add(instr.rvar2.name) + + varkill.add(instr.lvar.name) + self.blocksMap[instr.lvar.name].add(block) + + elif isinstance(instr, ChironSSA.AssertCommand): + if isinstance(instr.cond, ChironSSA.Var) and instr.cond.name not in varkill: + self.globals.add(instr.cond.name) + + elif isinstance(instr, ChironSSA.AssumeCommand): + if isinstance(instr.cond, ChironSSA.Var) and instr.cond.name not in varkill: + self.globals.add(instr.cond.name) + + elif isinstance(instr, ChironSSA.ConditionCommand): + if isinstance(instr.cond, ChironSSA.Var) and instr.cond.name not in varkill: + self.globals.add(instr.cond.name) + + elif isinstance(instr, ChironSSA.MoveCommand): + if isinstance(instr.var, ChironSSA.Var) and instr.var.name not in varkill: + self.globals.add(instr.var.name) + + elif isinstance(instr, ChironSSA.GotoCommand): + if isinstance(instr.xcor, ChironSSA.Var) and instr.xcor.name not in varkill: + self.globals.add(instr.xcor.name) + if isinstance(instr.ycor, ChironSSA.Var) and instr.ycor.name not in varkill: + self.globals.add(instr.ycor.name) + + return self.globals + + def convert(self, ir): + # convert each statement from ChironTAC to ChironSSA + for instr, tgt in ir: + if isinstance(instr, ChironTAC.AssignmentCommand): + lvar = ChironSSA.Var(instr.lvar.name) + rvar1 = ChironSSA.Var(instr.rvar1.name) if isinstance(instr.rvar1, ChironTAC.Var) else ChironSSA.Num(instr.rvar1.value) if isinstance(instr.rvar1, ChironTAC.Num) else ChironSSA.Unused() + rvar2 = ChironSSA.Var(instr.rvar2.name) if isinstance(instr.rvar2, ChironTAC.Var) else ChironSSA.Num(instr.rvar2.value) if isinstance(instr.rvar2, ChironTAC.Num) else ChironSSA.Unused() + ir[ir.index((instr, tgt))] = (ChironSSA.AssignmentCommand(lvar, rvar1, rvar2, instr.op), tgt) + + elif isinstance(instr, ChironTAC.AssertCommand): + cond = ChironSSA.Var(instr.cond.name) if isinstance(instr.cond, ChironTAC.Var) else ChironSSA.BoolTrue() if isinstance(instr.cond, ChironTAC.BoolTrue) else ChironSSA.BoolFalse() + ir[ir.index((instr, tgt))] = (ChironSSA.AssertCommand(cond), tgt) + + elif isinstance(instr, ChironTAC.AssumeCommand): + cond = ChironSSA.Var(instr.cond.name) if isinstance(instr.cond, ChironTAC.Var) else ChironSSA.BoolTrue() if isinstance(instr.cond, ChironTAC.BoolTrue) else ChironSSA.BoolFalse() + ir[ir.index((instr, tgt))] = (ChironSSA.AssumeCommand(cond), tgt) + + elif isinstance(instr, ChironTAC.ConditionCommand): + cond = ChironSSA.Var(instr.cond.name) if isinstance(instr.cond, ChironTAC.Var) else ChironSSA.BoolTrue() if isinstance(instr.cond, ChironTAC.BoolTrue) else ChironSSA.BoolFalse() + ir[ir.index((instr, tgt))] = (ChironSSA.ConditionCommand(cond), tgt) + + elif isinstance(instr, ChironTAC.MoveCommand): + var = ChironSSA.Var(instr.var.name) if isinstance(instr.var, ChironTAC.Var) else ChironSSA.Num(instr.var.value) + ir[ir.index((instr, tgt))] = (ChironSSA.MoveCommand(instr.direction, var), tgt) + + elif isinstance(instr, ChironTAC.GotoCommand): + xcor = ChironSSA.Var(instr.xcor.name) if isinstance(instr.xcor, ChironTAC.Var) else ChironSSA.Num(instr.xcor.value) + ycor = ChironSSA.Var(instr.ycor.name) if isinstance(instr.ycor, ChironTAC.Var) else ChironSSA.Num(instr.ycor.value) + ir[ir.index((instr, tgt))] = (ChironSSA.GotoCommand(xcor, ycor), tgt) + + elif isinstance(instr, ChironTAC.SinCommand): + lvar = ChironSSA.Var(instr.lvar.name) + rvar = ChironSSA.Var(instr.rvar.name) if isinstance(instr.rvar, ChironTAC.Var) else ChironSSA.Num(instr.rvar.value) + ir[ir.index((instr, tgt))] = (ChironSSA.SinCommand(lvar, rvar), tgt) + + elif isinstance(instr, ChironTAC.CosCommand): + lvar = ChironSSA.Var(instr.lvar.name) + rvar = ChironSSA.Var(instr.rvar.name) if isinstance(instr.rvar, ChironTAC.Var) else ChironSSA.Num(instr.rvar.value) + ir[ir.index((instr, tgt))] = (ChironSSA.CosCommand(lvar, rvar), tgt) + + elif isinstance(instr, ChironTAC.PenCommand): + ir[ir.index((instr, tgt))] = (ChironSSA.PenCommand(instr.status), tgt) + + elif isinstance(instr, ChironTAC.PauseCommand): + ir[ir.index((instr, tgt))] = (ChironSSA.PauseCommand(), tgt) + + elif isinstance(instr, ChironTAC.NoOpCommand): + ir[ir.index((instr, tgt))] = (ChironSSA.NoOpCommand(), tgt) + + + diff --git a/ChironCore/ChironTAC/ChironTAC.py b/ChironCore/ChironTAC/ChironTAC.py new file mode 100644 index 0000000..d792f23 --- /dev/null +++ b/ChironCore/ChironTAC/ChironTAC.py @@ -0,0 +1,217 @@ +# Three Address Code (TAC) generation for Chiron +class TAC(object): + pass + +# Instruction Classes +class Instruction(TAC): + pass + +class CosCommand(Instruction): + def __init__(self, lvar, rvar): # lvar = cos(rvar) + self.lvar = lvar + self.rvar = rvar + + def __str__(self): + return self.lvar.__str__() + " = cos(" + self.rvar.__str__() + ")" + +class SinCommand(Instruction): + def __init__(self, lvar, rvar): # lvar = sin(rvar) + self.lvar = lvar + self.rvar = rvar + + def __str__(self): + return self.lvar.__str__() + " = sin(" + self.rvar.__str__() + ")" + +class AssignmentCommand(Instruction): + def __init__(self, lvar, rvar1, rvar2, op): + self.lvar = lvar + self.rvar1 = rvar1 + self.rvar2 = rvar2 + self.op = op + + def __str__(self): + return self.lvar.__str__() + " = " + self.rvar1.__str__() + " " + self.op + " " + self.rvar2.__str__() + +class ConditionCommand(Instruction): + def __init__(self, condition): + self.cond = condition + + def __str__(self): + return "BRANCH: " + self.cond.__str__() + +class AssertCommand(Instruction): + def __init__(self, condition): + self.cond = condition + + def __str__(self): + return "ASSERT: " + self.cond.__str__() + +class AssumeCommand(Instruction): + def __init__(self, condition): + self.cond = condition + + def __str__(self): + return "ASSUME: " + self.cond.__str__() + +class MoveCommand(Instruction): + def __init__(self, motion, var): + self.direction = motion + self.var = var + + def __str__(self): + return "MOVE: " + self.direction + " " + self.var.__str__() + +class PenCommand(Instruction): + def __init__(self, penstat): + self.status = penstat + + def __str__(self): + return "PEN: " + self.status + +class GotoCommand(Instruction): + def __init__(self, x, y): + self.xcor = x + self.ycor = y + + def __str__(self): + return "goto " + str(self.xcor) + " " + str(self.ycor) + +class NoOpCommand(Instruction): + def __str__(self): + return "NoOp" + +class PauseCommand(Instruction): + def __str__(self): + return "Pause" + + +class Expression(TAC): + pass +# -- Arithmetic Expressions ------------------------------------------ +class ArithExpr(Expression): + pass + +class BinArithOp(ArithExpr): + def __init__(self, lvar, rvar, op): + self.lvar = lvar + self.rvar = rvar + self.op = op + + def __str__(self): + return self.lvar.__str__() + " " + self.op + " " + self.rvar.__str__() + +class Sum(BinArithOp): + def __init__(self, lvar, rvar): + BinArithOp.__init__(self, lvar, rvar, "+") + +class Sub(BinArithOp): + def __init__(self, lvar, rvar): + BinArithOp.__init__(self, lvar, rvar, "-") + +class Mul(BinArithOp): + def __init__(self, lvar, rvar): + BinArithOp.__init__(self, lvar, rvar, "*") + +class Div(BinArithOp): + def __init__(self, lvar, rvar): + BinArithOp.__init__(self, lvar, rvar, "/") + + +class UnaryArithOp(ArithExpr): + def __init__(self, op, var): + self.op = op + self.var = var + + def __str__(self): + return self.op + " " + self.var.__str__() + +class UMinus(UnaryArithOp): + def __init__(self, var): + UnaryArithOp.__init__(self, "-", var) + + +# -- Boolean Expressions -------------------------------------------- +class BoolExpr(Expression): + pass + +class BinBoolOp(BoolExpr): + def __init__(self, lvar, rvar, op): + self.lvar = lvar + self.rvar = rvar + self.op = op + + def __str__(self): + return self.lvar.__str__() + " " + self.op + " " + self.rvar.__str__() + +class And(BinBoolOp): + def __init__(self, lvar, rvar): + BinBoolOp.__init__(self, lvar, rvar, "and") + +class Or(BinBoolOp): + def __init__(self, lvar, rvar): + BinBoolOp.__init__(self, lvar, rvar, "or") + +class LT(BinBoolOp): + def __init__(self, lvar, rvar): + BinBoolOp.__init__(self, lvar, rvar, "<") + +class GT(BinBoolOp): + def __init__(self, lvar, rvar): + BinBoolOp.__init__(self, lvar, rvar, ">") + +class LTE(BinBoolOp): + def __init__(self, lvar, rvar): + BinBoolOp.__init__(self, lvar, rvar, "<=") + +class GTE(BinBoolOp): + def __init__(self, lvar, rvar): + BinBoolOp.__init__(self, lvar, rvar, ">=") + +class EQ(BinBoolOp): + def __init__(self, lvar, rvar): + BinBoolOp.__init__(self, lvar, rvar, "==") + +class NEQ(BinBoolOp): + def __init__(self, lvar, rvar): + BinBoolOp.__init__(self, lvar, rvar, "!=") + +class Not(BoolExpr): + def __init__(self, var): + self.var = var + + def __str__(self): + return "not " + self.var.__str__() + +class PenStatus(Expression): + def __str__(self): + return "penstatus" + +class BoolTrue(Expression): + def __str__(self): + return "true" + +class BoolFalse(Expression): + def __str__(self): + return "false" + +# -- Value Expressions ---------------------------------------------- +class Value(Expression): + pass + +class Num(Value): + def __init__(self, value): + self.value = value + + def __str__(self): + return str(self.value) + +class Var(Value): + def __init__(self, name): + self.name = name + + def __str__(self): + return self.name + +class Unused(Value): + def __str__(self): + return "" diff --git a/ChironCore/ChironTAC/builder.py b/ChironCore/ChironTAC/builder.py new file mode 100644 index 0000000..1e68f68 --- /dev/null +++ b/ChironCore/ChironTAC/builder.py @@ -0,0 +1,479 @@ +""" +Class for converting IR to Three Address Code (TAC) +""" + +from ChironAST import ChironAST +from ChironTAC import ChironTAC +import cfg.cfgBuilder as cfgB +import z3 + +class TACGenerator: + def __init__(self, ir): + self.ir = ir + self.tac = [] + self.tempCount = 0 + self.branchCount = 0 + self.assertCount = 0 + self.assumeCount = 0 + self.moveCount = 0 + self.gotoCount = 0 + self.ast_to_tac_line = {} + self.line = 0 + self.freeVars = set() + self.tacCfg = None + self.bbConditions = {} # bbConditions[bb] = condition for bb + self.varConditions = {} # varConditions[var] = condition for var + + def parseExpresssion(self, expr, dest): + """ + Parse the expression and return the TAC for the expression. + """ + if isinstance(expr, ChironAST.BinArithOp): + left = None + right = None + if isinstance(expr.lexpr, ChironAST.Num): + left = ChironTAC.Num(expr.lexpr.val) + elif isinstance(expr.lexpr, ChironAST.Var): + left = ChironTAC.Var(expr.lexpr.varname) + else: + temp = ChironTAC.Var(f":__temp_{self.tempCount}") + self.tempCount += 1 + left = temp + self.parseExpresssion(expr.lexpr, temp) + + if isinstance(expr.rexpr, ChironAST.Num): + right = ChironTAC.Num(expr.rexpr.val) + elif isinstance(expr.rexpr, ChironAST.Var): + right = ChironTAC.Var(expr.rexpr.varname) + else: + temp = ChironTAC.Var(f":__temp_{self.tempCount}") + self.tempCount += 1 + right = temp + self.parseExpresssion(expr.rexpr, temp) + + self.line += 1 + self.tac.append( + (ChironTAC.AssignmentCommand(dest, left, right, expr.symbol), 1) + ) + elif isinstance(expr, ChironAST.UMinus): + if isinstance(expr.expr, ChironAST.Num): + self.line += 1 + self.tac.append( + ( + ChironTAC.AssignmentCommand( + dest, + ChironTAC.Num(0), + ChironTAC.Num(expr.expr.val), + "-", + ), + 1, + ), + ) + elif isinstance(expr.expr, ChironAST.Var): + self.line += 1 + self.tac.append( + ( + ChironTAC.AssignmentCommand( + dest, + ChironTAC.Num(0), + ChironTAC.Var(expr.expr.varname), + "-", + ), + 1, + ), + ) + else: + temp = ChironTAC.Var(f":__temp_{self.tempCount}") + self.tempCount += 1 + self.parseExpresssion(expr.expr, temp) + self.line += 1 + self.tac.append( + ( + ChironTAC.AssignmentCommand( + dest, ChironTAC.Num(0), temp, "-" + ), + 1, + ) + ) + elif isinstance(expr, ChironAST.BinCondOp) and not ( + isinstance(expr, ChironAST.AND) + or isinstance(expr, ChironAST.OR) + or isinstance(expr, ChironAST.NOT) + ): + left = None + right = None + if isinstance(expr.lexpr, ChironAST.Num): + left = ChironTAC.Num(expr.lexpr.val) + elif isinstance(expr.lexpr, ChironAST.Var): + left = ChironTAC.Var(expr.lexpr.varname) + else: + temp = ChironTAC.Var(f":__temp_{self.tempCount}") + self.tempCount += 1 + left = temp + self.parseExpresssion(expr.lexpr, temp) + + if isinstance(expr.rexpr, ChironAST.Num): + right = ChironTAC.Num(expr.rexpr.val) + elif isinstance(expr.rexpr, ChironAST.Var): + right = ChironTAC.Var(expr.rexpr.varname) + else: + temp = ChironTAC.Var(f":__temp_{self.tempCount}") + self.tempCount += 1 + right = temp + self.parseExpresssion(expr.rexpr, temp) + + self.line += 1 + self.tac.append( + (ChironTAC.AssignmentCommand(dest, left, right, expr.symbol), 1) + ) + elif isinstance(expr, ChironAST.AND) or isinstance(expr, ChironAST.OR): + left = None + right = None + if isinstance(expr.lexpr, ChironAST.BoolTrue): + left = ChironTAC.BoolTrue() + elif isinstance(expr.lexpr, ChironAST.BoolFalse): + left = ChironTAC.BoolFalse() + elif isinstance(expr.lexpr, ChironAST.Var): + left = ChironTAC.Var(expr.lexpr.varname) + else: + temp = ChironTAC.Var(f":__temp_{self.tempCount}") + self.tempCount += 1 + left = temp + self.parseExpresssion(expr.lexpr, temp) + + if isinstance(expr.rexpr, ChironAST.BoolTrue): + right = ChironTAC.BoolTrue() + elif isinstance(expr.rexpr, ChironAST.BoolFalse): + right = ChironTAC.BoolFalse() + elif isinstance(expr.rexpr, ChironAST.Var): + right = ChironTAC.Var(expr.rexpr.varname) + else: + temp = ChironTAC.Var(f":__temp_{self.tempCount}") + self.tempCount += 1 + right = temp + self.parseExpresssion(expr.rexpr, temp) + + self.line += 1 + self.tac.append( + (ChironTAC.AssignmentCommand(dest, left, right, expr.symbol), 1) + ) + elif isinstance(expr, ChironAST.NOT): + if isinstance(expr.expr, ChironAST.BoolTrue): + self.line += 1 + self.tac.append( + ( + ChironTAC.AssignmentCommand( + dest, + ChironTAC.Unused(), + ChironTAC.BoolTrue(), + "not", + ), + 1, + ) + ) + elif isinstance(expr.expr, ChironAST.BoolFalse): + self.line += 1 + self.tac.append( + ( + ChironTAC.AssignmentCommand( + dest, + ChironTAC.Unused(), + ChironTAC.BoolFalse(), + "not", + ), + 1, + ) + ) + elif isinstance(expr.expr, ChironAST.Var): + self.line += 1 + self.tac.append( + ( + ChironTAC.AssignmentCommand( + dest, + ChironTAC.Unused(), + ChironTAC.Var(expr.expr.varname), + "not", + ), + 1, + ) + ) + else: + temp = ChironTAC.Var(f":__temp_{self.tempCount}") + self.tempCount += 1 + self.parseExpresssion(expr.expr, temp) + self.line += 1 + self.tac.append( + (ChironTAC.AssignmentCommand(dest, None, temp, "not"), 1) + ) + elif isinstance(expr, ChironAST.Var): + self.line += 1 + self.tac.append( + ( + ChironTAC.AssignmentCommand( + dest, ChironTAC.Num(0), ChironTAC.Var(expr.varname), "+" + ), + 1, + ) + ) + elif isinstance(expr, ChironAST.Num): + self.line += 1 + self.tac.append( + ( + ChironTAC.AssignmentCommand( + dest, ChironTAC.Num(0), ChironTAC.Num(expr.val), "+" + ), + 1, + ) + ) + elif isinstance(expr, ChironAST.BoolTrue): + self.line += 1 + self.tac.append( + ( + ChironTAC.AssignmentCommand( + dest, ChironTAC.Unused(), ChironTAC.BoolTrue(), "" + ), + 1, + ) + ) + elif isinstance(expr, ChironAST.BoolFalse): + self.line += 1 + self.tac.append( + ( + ChironTAC.AssignmentCommand( + dest, ChironTAC.Unused(), ChironTAC.BoolFalse(), "" + ), + 1, + ) + ) + else: + raise NotImplementedError( + "Unknown expression: %s, %s." % (type(expr), expr) + ) + + def generateTAC(self): + line_number = 0 + for stmt, tgt in self.ir: + self.ast_to_tac_line[line_number] = self.line + line_number += 1 + + if isinstance(stmt, ChironAST.AssignmentCommand): + self.parseExpresssion(stmt.rexpr, ChironTAC.Var(stmt.lvar.varname)) + + elif isinstance(stmt, ChironAST.ConditionCommand): + branchvar = None + if isinstance(stmt.cond, ChironAST.BoolTrue): + branchvar = ChironTAC.BoolTrue() + elif isinstance(stmt.cond, ChironAST.BoolFalse): + branchvar = ChironTAC.BoolFalse() + elif isinstance(stmt.cond, ChironAST.Var): + branchvar = ChironTAC.Var(stmt.cond.varname) + else: + branchvar = ChironTAC.Var(f":__branch_{self.branchCount}") + self.branchCount += 1 + self.parseExpresssion(stmt.cond, branchvar) + newtgt = line_number - 1 + tgt # Adjusted later + self.line += 1 + self.tac.append((ChironTAC.ConditionCommand(branchvar), newtgt)) + + elif isinstance(stmt, ChironAST.AssertCommand): + assertvar = ChironTAC.Var(f":__assert_{self.assertCount}") + self.assertCount += 1 + self.parseExpresssion(stmt.cond, assertvar) + self.line += 1 + self.tac.append((ChironTAC.AssertCommand(assertvar), 1)) + + elif isinstance(stmt, ChironAST.AssumeCommand): + assumevar = ChironTAC.Var(f":__assume_{self.assumeCount}") + self.assumeCount += 1 + self.parseExpresssion(stmt.cond, assumevar) + self.line += 1 + self.tac.append((ChironTAC.AssumeCommand(assumevar), 1)) + + elif isinstance(stmt, ChironAST.MoveCommand): + movevar = None + if isinstance(stmt.expr, ChironAST.Num): + movevar = ChironTAC.Num(stmt.expr.val) + elif isinstance(stmt.expr, ChironAST.Var): + movevar = ChironTAC.Var(stmt.expr.varname) + else: + movevar = ChironTAC.Var(f":__move_{self.moveCount}") + self.moveCount += 1 + self.parseExpresssion(stmt.expr, movevar) + + if (stmt.direction == "forward" or stmt.direction == "backward"): + self.line += 6 + self.tac.append((ChironTAC.CosCommand(ChironTAC.Var(":__cos_theta"), ChironTAC.Var(":turtleThetaDeg")), 1)) + self.tac.append((ChironTAC.SinCommand(ChironTAC.Var(":__sin_theta"), ChironTAC.Var(":turtleThetaDeg")), 1)) + self.tac.append((ChironTAC.AssignmentCommand(ChironTAC.Var(":__delta_x"), movevar, ChironTAC.Var(":__cos_theta"), "*"), 1)) + self.tac.append((ChironTAC.AssignmentCommand(ChironTAC.Var(":__delta_y"), movevar, ChironTAC.Var(":__sin_theta"), "*"), 1)) + if (stmt.direction == "forward"): + self.tac.append((ChironTAC.AssignmentCommand(ChironTAC.Var(":turtleX"), ChironTAC.Var(":turtleX"), ChironTAC.Var(":__delta_x"), "+"), 1)) + self.tac.append((ChironTAC.AssignmentCommand(ChironTAC.Var(":turtleY"), ChironTAC.Var(":turtleY"), ChironTAC.Var(":__delta_y"), "+"), 1)) + elif (stmt.direction == "backward"): + self.tac.append((ChironTAC.AssignmentCommand(ChironTAC.Var(":turtleX"), ChironTAC.Var(":turtleX"), ChironTAC.Var(":__delta_x"), "-"), 1)) + self.tac.append((ChironTAC.AssignmentCommand(ChironTAC.Var(":turtleY"), ChironTAC.Var(":turtleY"), ChironTAC.Var(":__delta_y"), "-"), 1)) + elif (stmt.direction == "left"): + self.line += 2 + self.tac.append((ChironTAC.AssignmentCommand(ChironTAC.Var(":turtleThetaDeg"), ChironTAC.Var(":turtleThetaDeg"), movevar, "+"), 1)) + self.tac.append((ChironTAC.AssignmentCommand(ChironTAC.Var(":turtleThetaDeg"), ChironTAC.Var(":turtleThetaDeg"), ChironTAC.Num(360), "%"), 1)) + elif (stmt.direction == "right"): + self.line += 2 + self.tac.append((ChironTAC.AssignmentCommand(ChironTAC.Var(":turtleThetaDeg"), ChironTAC.Var(":turtleThetaDeg"), movevar, "-"), 1)) + self.tac.append((ChironTAC.AssignmentCommand(ChironTAC.Var(":turtleThetaDeg"), ChironTAC.Var(":turtleThetaDeg"), ChironTAC.Num(360), "%"), 1)) + else: + raise NotImplementedError("Unknown move direction: %s, %s." % (type(stmt), stmt)) + + self.line += 1 + self.tac.append((ChironTAC.MoveCommand(stmt.direction, movevar), 1)) + + elif isinstance(stmt, ChironAST.PenCommand): + self.line += 2 + if (stmt.status == "penup"): + self.tac.append((ChironTAC.AssignmentCommand(ChironTAC.Var(":turtlePen"), ChironTAC.Num(1), ChironTAC.Num(0), "+"), 1)) + elif (stmt.status == "pendown"): + self.tac.append((ChironTAC.AssignmentCommand(ChironTAC.Var(":turtlePen"), ChironTAC.Num(0), ChironTAC.Num(0), "+"), 1)) + else: + raise NotImplementedError("Unknown pen status: %s, %s." % (type(stmt), stmt)) + self.tac.append((ChironTAC.PenCommand(stmt.status), 1)) + + elif isinstance(stmt, ChironAST.GotoCommand): + xvar = None + yvar = None + if isinstance(stmt.xcor, ChironAST.Num): + xvar = ChironTAC.Num(stmt.xcor.val) + elif isinstance(stmt.xcor, ChironAST.Var): + xvar = ChironTAC.Var(stmt.xcor.varname) + else: + xvar = ChironTAC.Var(f":__x_{self.gotoCount}") + self.gotoCount += 1 + self.parseExpresssion(stmt.xcor, xvar) + if isinstance(stmt.ycor, ChironAST.Num): + yvar = ChironTAC.Num(stmt.ycor.val) + elif isinstance(stmt.ycor, ChironAST.Var): + yvar = ChironTAC.Var(stmt.ycor.varname) + else: + yvar = ChironTAC.Var(f":__y_{self.gotoCount}") + self.gotoCount += 1 + self.parseExpresssion(stmt.ycor, yvar) + self.line += 3 + self.tac.append((ChironTAC.AssignmentCommand(ChironTAC.Var(":turtleX"), xvar, ChironTAC.Num(0), "+"), 1)) + self.tac.append((ChironTAC.AssignmentCommand(ChironTAC.Var(":turtleY"), yvar, ChironTAC.Num(0), "+"), 1)) + self.tac.append((ChironTAC.GotoCommand(xvar, yvar), 1)) + + elif isinstance(stmt, ChironAST.NoOpCommand): + self.line += 1 + self.tac.append((ChironTAC.NoOpCommand(), 1)) + + elif isinstance(stmt, ChironAST.PauseCommand): + self.line += 1 + self.tac.append((ChironTAC.PauseCommand(), 1)) + + else: + raise NotImplementedError( + "Unknown instruction: %s, %s." % (type(stmt), stmt) + ) + + self.ast_to_tac_line[line_number] = self.line + + for i in range(len(self.tac)): + stmt, tgt = self.tac[i] + if isinstance(stmt, ChironTAC.ConditionCommand): + newtgt = self.ast_to_tac_line[tgt] - i + self.tac[i] = (stmt, newtgt) + + self.handleMoveVariables() + + self.tacCfg, _ = cfgB.buildCFG(self.tac, "control_flow_graph", False) # Building CFG + for bb in self.tacCfg: + self.bbConditions[bb] = None + self.buildConditions() + + self.handleFreeVariables() + + def buildConditions(self): + topological_order = list(self.tacCfg.get_topological_order()) + start = topological_order[0] + start.set_condition(z3.BoolVal(True)) + topological_order.pop(0) + for node in topological_order: + for pred in self.tacCfg.predecessors(node): + instr = pred.instrlist[-1][0] + current_cond = node.get_condition() + if isinstance(instr, ChironTAC.ConditionCommand) and type(instr.cond) == ChironTAC.Var: + cond = z3.Bool(instr.cond.name) + label = self.tacCfg.get_edge_label(pred, node) + if label == 'Cond_True': + node.set_condition(z3.Or(current_cond, z3.And(pred.get_condition(), cond))) + elif label == 'Cond_False': + node.set_condition(z3.Or(current_cond, z3.And(pred.get_condition(), z3.Not(cond)))) + else: + node.set_condition(z3.Or(pred.get_condition(), current_cond)) + + t = z3.Tactic('ctx-simplify').apply(node.get_condition()).as_expr() + node.set_condition(t) + self.bbConditions[node] = node.get_condition() + + for bb in self.tacCfg.nodes(): + for stmt, _ in bb.instrlist: + if isinstance(stmt, (ChironTAC.AssignmentCommand, ChironTAC.SinCommand, ChironTAC.CosCommand)): + self.varConditions[stmt.lvar.name] = self.bbConditions[bb] if self.bbConditions[bb] is not None else z3.BoolVal(True) + + def handleFreeVariables(self): + self.freeVars = self.getFreeVariables() + + for var in self.freeVars: + self.tac.insert(0, (ChironTAC.AssignmentCommand(ChironTAC.Var(var), ChironTAC.Unused(), ChironTAC.Unused(), ""), 1)) + + def handleMoveVariables(self): + self.tac.insert(0, (ChironTAC.AssignmentCommand(ChironTAC.Var(":turtleX"), ChironTAC.Num(0), ChironTAC.Num(0), "+"), 1)) + self.tac.insert(0, (ChironTAC.AssignmentCommand(ChironTAC.Var(":turtleY"), ChironTAC.Num(0), ChironTAC.Num(0), "+"), 1)) + self.tac.insert(0, (ChironTAC.AssignmentCommand(ChironTAC.Var(":turtleThetaDeg"), ChironTAC.Num(0), ChironTAC.Num(0), "+"), 1)) + self.tac.insert(0, (ChironTAC.AssignmentCommand(ChironTAC.Var(":turtlePen"), ChironTAC.Num(0), ChironTAC.Num(0), "+"), 1)) # 0->down 1->up + + def getFreeVariables(self): + """ + Returns free variables in TAC. + """ + if len(self.freeVars) > 0: + return self.freeVars + + boundVars = set() + for (stmt, _), _ in zip(self.tac, range(len(self.tac))): + if isinstance(stmt, ChironTAC.AssignmentCommand): + if isinstance(stmt.rvar1, ChironTAC.Var) and stmt.rvar1.__str__() not in boundVars: + self.freeVars.add(stmt.rvar1.__str__()) + if isinstance(stmt.rvar2, ChironTAC.Var) and stmt.rvar2.__str__() not in boundVars: + self.freeVars.add(stmt.rvar2.__str__()) + boundVars.add(stmt.lvar.__str__()) + elif isinstance(stmt, ChironTAC.ConditionCommand): + if isinstance(stmt.cond, ChironTAC.Var) and stmt.cond.__str__() not in boundVars: + self.freeVars.add(stmt.cond.__str__()) + elif isinstance(stmt, ChironTAC.AssertCommand): + if isinstance(stmt.cond, ChironTAC.Var) and stmt.cond.__str__() not in boundVars: + self.freeVars.add(stmt.cond.__str__()) + elif isinstance(stmt, ChironTAC.AssumeCommand): + if isinstance(stmt.cond, ChironTAC.Var) and stmt.cond.__str__() not in boundVars: + self.freeVars.add(stmt.cond.__str__()) + elif isinstance(stmt, ChironTAC.MoveCommand): + if isinstance(stmt.var, ChironTAC.Var) and stmt.var.__str__() not in boundVars: + self.freeVars.add(stmt.var.__str__()) + elif isinstance(stmt, ChironTAC.GotoCommand): + if isinstance(stmt.xcor, ChironTAC.Var) and stmt.xcor.__str__() not in boundVars: + self.freeVars.add(stmt.xcor.__str__()) + if isinstance(stmt.ycor, ChironTAC.Var) and stmt.ycor.__str__() not in boundVars: + self.freeVars.add(stmt.ycor.__str__()) + elif isinstance(stmt, ChironTAC.SinCommand): + if isinstance(stmt.rvar, ChironTAC.Var) and stmt.rvar.__str__() not in boundVars: + self.freeVars.add(stmt.rvar.__str__()) + boundVars.add(stmt.lvar.__str__()) + elif isinstance(stmt, ChironTAC.CosCommand): + if isinstance(stmt.rvar, ChironTAC.Var) and stmt.rvar.__str__() not in boundVars: + self.freeVars.add(stmt.rvar.__str__()) + boundVars.add(stmt.lvar.__str__()) + + return self.freeVars + + + def printTAC(self): + for (stmt, tgt), line in zip(self.tac, range(len(self.tac))): + print(f"[L{line}]".rjust(5), stmt, f"[{tgt}]") diff --git a/ChironCore/angles.conf b/ChironCore/angles.conf new file mode 100644 index 0000000..1fb9a50 --- /dev/null +++ b/ChironCore/angles.conf @@ -0,0 +1,8 @@ +0,1,0 +45,0.707,0.707 +90,0,1 +135,-0.707,0.707 +180,-1,0 +225,-0.707,-0.707 +270,0,-1 +315,0.707,-0.707 \ No newline at end of file diff --git a/ChironCore/bmc.py b/ChironCore/bmc.py new file mode 100644 index 0000000..791dc79 --- /dev/null +++ b/ChironCore/bmc.py @@ -0,0 +1,326 @@ +''' +This file is used to convert the SSA IR to SMT-LIB format. +''' +import z3 +from ChironSSA import ChironSSA +from cfg import cfgBuilder + +class BMC: + def __init__(self, cfg, angle_conf): + self.solver = z3.Solver() + self.solver_without_cond = z3.Solver() + self.angle_conditions = z3.BoolVal(True) + self.assert_conditions = z3.BoolVal(True) + self.assume_conditions = z3.BoolVal(True) + self.cfg = cfg + self.angle_conf = angle_conf + + self.bbConditions = {} # bbConditions[bb] = condition for bb + for bb in self.cfg: + self.bbConditions[bb] = None + + self.buildConditions() + + self.varConditions = {} # varConditions[var] = condition for var + for bb in self.cfg.nodes(): + for stmt, _ in bb.instrlist: + if isinstance(stmt, (ChironSSA.PhiCommand, ChironSSA.AssignmentCommand, ChironSSA.SinCommand, ChironSSA.CosCommand)): + self.varConditions[stmt.lvar.name] = self.bbConditions[bb] if self.bbConditions[bb] is not None else z3.BoolVal(True) + + def buildConditions(self): + topological_order = list(self.cfg.get_topological_order()) + start = topological_order[0] + start.set_condition(z3.BoolVal(True)) + topological_order.pop(0) + for node in topological_order: + for pred in self.cfg.predecessors(node): + instr = pred.instrlist[-1][0] + current_cond = node.get_condition() + if isinstance(instr, ChironSSA.ConditionCommand) and type(instr.cond) == ChironSSA.Var: + cond = z3.Bool(instr.cond.name) + label = self.cfg.get_edge_label(pred, node) + if label == 'Cond_True': + node.set_condition(z3.Or(current_cond, z3.And(pred.get_condition(), cond))) + elif label == 'Cond_False': + node.set_condition(z3.Or(current_cond, z3.And(pred.get_condition(), z3.Not(cond)))) + else: + node.set_condition(z3.Or(pred.get_condition(), current_cond)) + + t = z3.Tactic('ctx-simplify').apply(node.get_condition()).as_expr() + node.set_condition(t) + self.bbConditions[node] = node.get_condition() + + def convertSSAtoSMT(self): + for bb in self.cfg.nodes(): + for stmt, _ in bb.instrlist: + if isinstance(stmt, ChironSSA.PhiCommand): + lvar = z3.Real(stmt.lvar.name) + rvars = [z3.Real(rvar.name) for rvar in stmt.rvars] + + rhs_expr = rvars[0] + for i in range(1, len(stmt.rvars)): + rhs_expr = z3.If(self.varConditions[stmt.rvars[i].name], rvars[i], (rhs_expr)) + + if self.varConditions[stmt.lvar.name] not in (None, True, False): + self.solver.add(z3.Implies(self.varConditions[stmt.lvar.name], lvar == rhs_expr)) + elif self.varConditions[stmt.lvar.name] is not False: + self.solver.add(lvar == rhs_expr) + + elif isinstance(stmt, ChironSSA.AssignmentCommand): + lvar = None + rvar1 = ChironSSA.Unused() + rvar2 = ChironSSA.Unused() + + if stmt.op in ["+", "-", "*", "/", "%"]: + lvar = z3.Real(stmt.lvar.name) + if isinstance(stmt.rvar1, ChironSSA.Var): + rvar1 = z3.Real(stmt.rvar1.name) + elif isinstance(stmt.rvar1, ChironSSA.Num): + rvar1 = z3.RealVal(stmt.rvar1.value) + if isinstance(stmt.rvar2, ChironSSA.Var): + rvar2 = z3.Real(stmt.rvar2.name) + elif isinstance(stmt.rvar2, ChironSSA.Num): + rvar2 = z3.RealVal(stmt.rvar2.value) + elif stmt.op in ["<", ">", "<=", ">=", "==", "!="]: + lvar = z3.Bool(stmt.lvar.name) + if isinstance(stmt.rvar1, ChironSSA.Var): + rvar1 = z3.Real(stmt.rvar1.name) + elif isinstance(stmt.rvar1, ChironSSA.Num): + rvar1 = z3.RealVal(stmt.rvar1.value) + if isinstance(stmt.rvar2, ChironSSA.Var): + rvar2 = z3.Real(stmt.rvar2.name) + elif isinstance(stmt.rvar2, ChironSSA.Num): + rvar2 = z3.RealVal(stmt.rvar2.value) + elif stmt.op in ["and", "or"]: + lvar = z3.Bool(stmt.lvar.name) + if isinstance(stmt.rvar1, ChironSSA.Var): + rvar1 = z3.Bool(stmt.rvar1.name) + elif isinstance(stmt.rvar1, ChironSSA.BoolTrue): + rvar1 = z3.BoolVal(True) + if isinstance(stmt.rvar2, ChironSSA.Var): + rvar2 = z3.Bool(stmt.rvar2.name) + elif isinstance(stmt.rvar2, ChironSSA.BoolFalse): + rvar2 = z3.BoolVal(False) + elif stmt.op == "not": + lvar = z3.Bool(stmt.lvar.name) + if isinstance(stmt.rvar2, ChironSSA.Var): + rvar2 = z3.Bool(stmt.rvar2.name) + elif isinstance(stmt.rvar2, ChironSSA.BoolTrue): + rvar2 = z3.BoolVal(True) + elif isinstance(stmt.rvar2, ChironSSA.BoolFalse): + rvar2 = z3.BoolVal(False) + elif stmt.op == "": + continue + else: + raise Exception("Unknown SSA instruction") + + if stmt.op == "+": + if self.varConditions[stmt.lvar.name] not in (None, True, False): + self.solver.add(z3.Implies(self.varConditions[stmt.lvar.name], lvar == (rvar1 + rvar2))) + elif self.varConditions[stmt.lvar.name] is not False: + self.solver.add(lvar == (rvar1 + rvar2)) + elif stmt.op == "-": + if self.varConditions[stmt.lvar.name] not in (None, True, False): + self.solver.add(z3.Implies(self.varConditions[stmt.lvar.name], lvar == (rvar1 - rvar2))) + elif self.varConditions[stmt.lvar.name] is not False: + self.solver.add(lvar == (rvar1 - rvar2)) + elif stmt.op == "*": + if self.varConditions[stmt.lvar.name] not in (None, True, False): + self.solver.add(z3.Implies(self.varConditions[stmt.lvar.name], lvar == (rvar1 * rvar2))) + elif self.varConditions[stmt.lvar.name] is not False: + self.solver.add(lvar == (rvar1 * rvar2)) + elif stmt.op == "/": + if self.varConditions[stmt.lvar.name] not in (None, True, False): + self.solver.add(z3.Implies(self.varConditions[stmt.lvar.name], lvar == (rvar1 / rvar2))) + elif self.varConditions[stmt.lvar.name] is not False: + self.solver.add(lvar == (rvar1 / rvar2)) + elif stmt.op == "%": + if self.varConditions[stmt.lvar.name] not in (None, True, False): + self.solver.add(z3.Implies(self.varConditions[stmt.lvar.name], lvar == (z3.ToInt(rvar1) % z3.ToInt(rvar2)))) + if stmt.lvar.name.startswith(":turtleThetaDeg$"): + condition = z3.BoolVal(False) + for (angle, _, _) in self.angle_conf: + condition = z3.Or(condition, lvar == angle) + self.angle_conditions = z3.And(self.angle_conditions, z3.Implies(self.varConditions[stmt.lvar.name], condition)) + elif self.varConditions[stmt.lvar.name] is not False: + self.solver.add(lvar == (z3.ToInt(rvar1) % z3.ToInt(rvar2))) + if stmt.lvar.name.startswith(":turtleThetaDeg$"): + condition = z3.BoolVal(False) + for (angle, _, _) in self.angle_conf: + condition = z3.Or(condition, lvar == angle) + self.angle_conditions = z3.And(self.angle_conditions, condition) + + elif stmt.op == "<": + if self.varConditions[stmt.lvar.name] not in (None, True, False): + self.solver.add(z3.Implies(self.varConditions[stmt.lvar.name], lvar == (rvar1 < rvar2))) + elif self.varConditions[stmt.lvar.name] is not False: + self.solver.add(lvar == (rvar1 < rvar2)) + elif stmt.op == ">": + if self.varConditions[stmt.lvar.name] not in (None, True, False): + self.solver.add(z3.Implies(self.varConditions[stmt.lvar.name], lvar == (rvar1 > rvar2))) + elif self.varConditions[stmt.lvar.name] is not False: + self.solver.add(lvar == (rvar1 > rvar2)) + elif stmt.op == "<=": + if self.varConditions[stmt.lvar.name] not in (None, True, False): + self.solver.add(z3.Implies(self.varConditions[stmt.lvar.name], lvar == (rvar1 <= rvar2))) + elif self.varConditions[stmt.lvar.name] is not False: + self.solver.add(lvar == (rvar1 <= rvar2)) + elif stmt.op == ">=": + if self.varConditions[stmt.lvar.name] not in (None, True, False): + self.solver.add(z3.Implies(self.varConditions[stmt.lvar.name], lvar == (rvar1 >= rvar2))) + elif self.varConditions[stmt.lvar.name] is not False: + self.solver.add(lvar == (rvar1 >= rvar2)) + elif stmt.op == "==": + if self.varConditions[stmt.lvar.name] not in (None, True, False): + self.solver.add(z3.Implies(self.varConditions[stmt.lvar.name], lvar == (rvar1 == rvar2))) + elif self.varConditions[stmt.lvar.name] is not False: + self.solver.add(lvar == (rvar1 == rvar2)) + elif stmt.op == "!=": + if self.varConditions[stmt.lvar.name] not in (None, True, False): + self.solver.add(z3.Implies(self.varConditions[stmt.lvar.name], lvar == (rvar1 != rvar2))) + elif self.varConditions[stmt.lvar.name] is not False: + self.solver.add(lvar == (rvar1 != rvar2)) + elif stmt.op == "and": + if self.varConditions[stmt.lvar.name] not in (None, True, False): + self.solver.add(z3.Implies(self.varConditions[stmt.lvar.name], lvar == z3.And(rvar1, rvar2))) + elif self.varConditions[stmt.lvar.name] is not False: + self.solver.add(lvar == z3.And(rvar1, rvar2)) + elif stmt.op == "or": + if self.varConditions[stmt.lvar.name] not in (None, True, False): + self.solver.add(z3.Implies(self.varConditions[stmt.lvar.name], lvar == z3.Or(rvar1, rvar2))) + elif self.varConditions[stmt.lvar.name] is not False: + self.solver.add(lvar == z3.Or(rvar1, rvar2)) + elif stmt.op == "not": + if self.varConditions[stmt.lvar.name] not in (None, True, False): + self.solver.add(z3.Implies(self.varConditions[stmt.lvar.name], lvar == z3.Not(rvar2))) + elif self.varConditions[stmt.lvar.name] is not False: + self.solver.add(lvar == z3.Not(rvar2)) + + elif isinstance(stmt, ChironSSA.AssertCommand): + cond = None + if isinstance(stmt.cond, ChironSSA.BoolTrue): + cond = z3.BoolVal(True) + elif isinstance(stmt.cond, ChironSSA.BoolFalse): + cond = z3.BoolVal(False) + elif isinstance(stmt.cond, ChironSSA.Var): + cond = z3.Bool(stmt.cond.name) + if self.varConditions[stmt.cond.name] not in (None, True, False): + self.assert_conditions = z3.And(self.assert_conditions, z3.Implies(self.varConditions[stmt.cond.name], cond)) + elif self.varConditions[stmt.cond.name] is not False: + self.assert_conditions = z3.And(self.assert_conditions, cond) + + elif isinstance(stmt, ChironSSA.AssumeCommand): + cond = None + if isinstance(stmt.cond, ChironSSA.BoolTrue): + cond = z3.BoolVal(True) + elif isinstance(stmt.cond, ChironSSA.BoolFalse): + cond = z3.BoolVal(False) + elif isinstance(stmt.cond, ChironSSA.Var): + cond = z3.Bool(stmt.cond.name) + if self.varConditions[stmt.cond.name] not in (None, True, False): + self.assume_conditions = z3.And(self.assume_conditions, z3.Implies(self.varConditions[stmt.cond.name], cond)) + elif self.varConditions[stmt.cond.name] is not False: + self.assume_conditions = z3.And(self.assume_conditions, cond) + + elif isinstance(stmt, ChironSSA.CosCommand): # Only for angles given in angle_conf + rvar = z3.Real(stmt.rvar.name) + # rhs_expr = z3.If(rvar == 0, 1, z3.If(rvar == 90, 0, z3.If(rvar == 180, -1, 0))) + rhs_expr = 0 + for (angle, cos, _) in self.angle_conf: + rhs_expr = z3.If(rvar == angle, cos, rhs_expr) + if self.varConditions[stmt.lvar.name] not in (None, True, False): + self.solver.add(z3.Implies(self.varConditions[stmt.lvar.name], z3.Real(stmt.lvar.name) == rhs_expr)) + elif self.varConditions[stmt.lvar.name] is not False: + self.solver.add(z3.Real(stmt.lvar.name) == rhs_expr) + + elif isinstance(stmt, ChironSSA.SinCommand): + rvar = z3.Real(stmt.rvar.name) + # rhs_expr = z3.If(rvar == 0, 0, z3.If(rvar == 90, 1, z3.If(rvar == 180, 0, -1))) + rhs_expr = 0 + for (angle, _, sin) in self.angle_conf: + rhs_expr = z3.If(rvar == angle, sin, rhs_expr) + + if self.varConditions[stmt.lvar.name] not in (None, True, False): + self.solver.add(z3.Implies(self.varConditions[stmt.lvar.name], z3.Real(stmt.lvar.name) == rhs_expr)) + elif self.varConditions[stmt.lvar.name] is not False: + self.solver.add(z3.Real(stmt.lvar.name) == rhs_expr) + + elif isinstance(stmt, ChironSSA.MoveCommand): + pass + elif isinstance(stmt, ChironSSA.PenCommand): + pass + elif isinstance(stmt, ChironSSA.GotoCommand): + pass + elif isinstance(stmt, ChironSSA.ConditionCommand): + pass + elif isinstance(stmt, ChironSSA.NoOpCommand): + pass + elif isinstance(stmt, ChironSSA.PauseCommand): + pass + else: + raise Exception("Unknown SSA instruction") + + self.solver_without_cond.add(self.solver.assertions()) + self.assert_conditions = z3.Tactic('ctx-simplify').apply(self.assert_conditions).as_expr() + self.angle_conditions = z3.Tactic('ctx-simplify').apply(self.angle_conditions).as_expr() + self.assume_conditions = z3.Tactic('ctx-simplify').apply(self.assume_conditions).as_expr() + + def solve(self, inputVars): + # Uncomment following lines if input variables are restricted to be integers. + # for var in inputVars: + # # should be integer + # varname = var + "$0" + # self.solver_without_cond.add(z3.ToInt(z3.Real(varname)) == z3.Real(varname)) + # self.solver.add(z3.ToInt(z3.Real(varname)) == z3.Real(varname)) + + + checker_with_assume = z3.Solver() + checker_with_assume.add(self.solver_without_cond.assertions()) + checker_with_assume.add(self.assume_conditions) + + assume_check = checker_with_assume.check() + if assume_check == z3.unsat: + print("The program cannot execute within the provided bounds. Consider increasing the bounds and trying again..") + return + elif assume_check == z3.unknown: + print("Cannot determine if bounds are sufficient") + return + + checker_with_angles = z3.Solver() + checker_with_angles.add(self.solver_without_cond.assertions()) + checker_with_angles.add(self.angle_conditions) + checker_with_angles.add(self.assume_conditions) + + angles_check = checker_with_angles.check() + if angles_check == z3.unsat: + print("Angle not in angles.conf for all cases") + return + elif angles_check == z3.unknown: + print("Cannot determine if angles are as per configuration file") + return + + self.solver.add(z3.Not(self.assert_conditions)) + self.solver.add(self.angle_conditions) + self.solver.add(self.assume_conditions) + + sat = self.solver.check() + + if sat == z3.sat: + print("Condition not satisfied!") + model = self.solver.model() + + solution = {} + for var in model: + varname, index = str(var).split("$") + if varname in inputVars and index == "0": + solution[varname] = model[var] + if len(solution) > 0: + print("Bug found for the following input:") + for var in solution: + print(var + " = " + str(solution[var])) + + elif sat == z3.unsat: + print("Condition satisfied for all inputs!") + else: + print("Unknown") + diff --git a/ChironCore/bmc_examples/bmc1.tl b/ChironCore/bmc_examples/bmc1.tl new file mode 100644 index 0000000..105f204 --- /dev/null +++ b/ChironCore/bmc_examples/bmc1.tl @@ -0,0 +1,13 @@ +:y = :x * :x +assert :y >= 0 + + +/* +Explaination: + +Run this program by: +./chiron.py bmc_examples/bmc1.tl -bmc + +In this program :x is the free input variable. Since :y is square of :x, :y is positive hence the BMC engine outputs that consition is always satified. +If we change the assert statement to :y >= 1, then the BMC gives us a counter example of :x such that :y < 1. Eg: :x = 0 is a counter example. +*/ \ No newline at end of file diff --git a/ChironCore/bmc_examples/bmc2.tl b/ChironCore/bmc_examples/bmc2.tl new file mode 100644 index 0000000..0594d96 --- /dev/null +++ b/ChironCore/bmc_examples/bmc2.tl @@ -0,0 +1,18 @@ +:t = 1 +// assume :x > 0 +repeat 2 [ + :t = :t * :x + assert :t >= 0 +] + + +/* +Explaination: + +Run this program by: +./chiron.py bmc_examples/bmc2.tl -bmc + +In this program, :x is a free input variable. After the 1st iteration, :t = :x and after the 2nd iteration, :t = :x * :x. +In the case when assume statement is commented, :t >= 0 is violated for any :x < 0. Thus the BMC outputs a negative :x as a counter example. +In the case when assume statement is uncommented, the domain of :x is restricted among the positive real numbers. Hence, the assert consition always holds true. +*/ \ No newline at end of file diff --git a/ChironCore/bmc_examples/bmc3.tl b/ChironCore/bmc_examples/bmc3.tl new file mode 100644 index 0000000..dbfce08 --- /dev/null +++ b/ChironCore/bmc_examples/bmc3.tl @@ -0,0 +1,32 @@ +:r = 1 +repeat 4 [ + :r = :r * :x +] + +:s = 1 +@unroll 6 repeat :m [ + if (:m % 2 == 0) [ + :s = :s * :x + ] else [ + repeat 3 [ + :s = :s * 2 * :x + ] + ] +] + +:z = 5*:r - 7*:s +assert :z > -1000 + + +/* +Explaination: + +Run this program by: +./chiron.py bmc_examples/bmc3.tl -bmc -ub 3 +This would give an error because the 1st loops iterates 4 times, which is more the specified unroll bound 3. So, we loosen the bound. + +Run this program by: +./chiron.py bmc_examples/bmc3.tl -bmc -ub 7 +In this case, there exists a counter example (for free input variable :x and :m) to the condition that gets printed. +Eg: take :x = 3 and :m = 1. +*/ \ No newline at end of file diff --git a/ChironCore/bmc_examples/bmc4.tl b/ChironCore/bmc_examples/bmc4.tl new file mode 100644 index 0000000..5f1d0e1 --- /dev/null +++ b/ChironCore/bmc_examples/bmc4.tl @@ -0,0 +1,32 @@ +:a = 2 +:y = 0 +:x = 0 + +if (:a > 0) [ + :x = :y + 45 +] +if (:a > 1) [ + :x = :y + 135 +] + +// :x = 135, :y = 0 + +assert :turtleX == 0 && :turtleY == 0 + +goto (:x, :y) +right :x + +assert :turtleX == 135 && :turtleY == 0 + + +/* +Explaination: + +Run this program by: +./chiron.py bmc_examples/bmc4.tl -bmc +This gives error because right :x rotates turtle by 135 deg, which is not in default angle. + +Run this program by: +./chiron.py bmc_examples/bmc4.tl -bmc -aconf angles.conf +In this case, 135 deg is in angle.conf and thus all conditions are satisfied. +*/ \ No newline at end of file diff --git a/ChironCore/bmc_examples/bmc5.tl b/ChironCore/bmc_examples/bmc5.tl new file mode 100644 index 0000000..c009a88 --- /dev/null +++ b/ChironCore/bmc_examples/bmc5.tl @@ -0,0 +1,19 @@ +forward 10 +left 90 +forward :t // turtle is at (10, :t) +:r = 20 +assert :turtleX*:turtleX + :turtleY*:turtleY <= :r*:r +// assume -17 <= :t && :t <= 17 + + +/* +Explaination: + +Run this program by: +./chiron.py bmc_examples/bmc5.tl -bmc +Here, we are checking whether turtle lies in the circle of radius :r = 20. The program outputs a counter example of this case (for free variable :t). Eg: :t = -18 + +Now uncomment the assert statement and run this program by: +./chiron.py bmc_examples/bmc5.tl -bmc +Now, we restrict :t between [-17, 17], then the turtle does not go outside the circle and condition is satisfied. +*/ diff --git a/ChironCore/bmc_examples/bmc6.tl b/ChironCore/bmc_examples/bmc6.tl new file mode 100644 index 0000000..b1f9404 --- /dev/null +++ b/ChironCore/bmc_examples/bmc6.tl @@ -0,0 +1,37 @@ +assume :t > 0 +assert !(:turtleX*:turtleX + :turtleY*:turtleY > 20*20 && :turtlePen == 0) + +repeat 7 [ + pendown + assert !(:turtleX*:turtleX + :turtleY*:turtleY > 20*20 && :turtlePen == 0) + + forward :t + assert !(:turtleX*:turtleX + :turtleY*:turtleY > 20*20 && :turtlePen == 0) + + left 45 + assert !(:turtleX*:turtleX + :turtleY*:turtleY > 20*20 && :turtlePen == 0) + + penup + assert !(:turtleX*:turtleX + :turtleY*:turtleY > 20*20 && :turtlePen == 0) + + forward :t + assert !(:turtleX*:turtleX + :turtleY*:turtleY > 20*20 && :turtlePen == 0) + + left 45 + assert !(:turtleX*:turtleX + :turtleY*:turtleY > 20*20 && :turtlePen == 0) +] + + +/* +Explaination: + +Run this program by: +./chiron.py bmc_examples/bmc6.tl -bmc -aconf angles.conf + +Consider the circle of radius 20 and center at (0,0) +Note that assert condition is not(turtle outside circle and pendown). We place the condition after every instruction. +So, we are asserting that turtle should not draw anything outside circle at any instance. + +But for large :t, turtle draws outside circle and a counter example of free input variable :t is given by BMC. +Eg: :t = 21 +*/ \ No newline at end of file diff --git a/ChironCore/bmc_examples/bmc7.tl b/ChironCore/bmc_examples/bmc7.tl new file mode 100644 index 0000000..2c874e7 --- /dev/null +++ b/ChironCore/bmc_examples/bmc7.tl @@ -0,0 +1,24 @@ +assume :step > 0 && :step < 50 +assume :iterations > 0 + +:count = 0 +:inc = 2 + +repeat :iterations [ + forward :step + + if :count % 2 == 0 [ + left 90 + ] else [ + right 90 + ] + + :count = :count + 1 + :step = :step + :inc + + if (:count + 1) % 8 == 0 [ + :inc = - :inc + ] +] + +assert :turtleX * :turtleX + :turtleY * :turtleY <= 100 diff --git a/ChironCore/bmc_examples/path_planning.tl b/ChironCore/bmc_examples/path_planning.tl new file mode 100644 index 0000000..c7a1958 --- /dev/null +++ b/ChironCore/bmc_examples/path_planning.tl @@ -0,0 +1,73 @@ + +// max steps = 5, max obstacles = 2 + +assume :s1 == 0 || :s1 == 1 || :s1 == 2 || :s1 == 3 || :s1 == 4 +assume :s2 == 0 || :s2 == 1 || :s2 == 2 || :s2 == 3 || :s2 == 4 +assume :s3 == 0 || :s3 == 1 || :s3 == 2 || :s3 == 3 || :s3 == 4 +assume :s4 == 0 || :s4 == 1 || :s4 == 2 || :s4 == 3 || :s4 == 4 +assume :s5 == 0 || :s5 == 1 || :s5 == 2 || :s5 == 3 || :s5 == 4 + +:step = 50 + +:targetX = 3 * :step +:targetY = 5 * :step + +:obs1x = 1 * :step +:obs1y = 1 * :step + +:obs2x = 0 * :step +:obs2y = 1 * :step + +assume !(:turtleX == :obs1x && :turtleY == :obs1y) +assume !(:turtleX == :obs2x && :turtleY == :obs2y) + +if (:s1 == 1) [forward :step] +if (:s1 == 2) [left 90 forward :step right 90] +if (:s1 == 3) [backward :step] +if (:s1 == 4) [left 90 backward :step right 90] + +assume !(:turtleX == :obs1x && :turtleY == :obs1y) +assume !(:turtleX == :obs2x && :turtleY == :obs2y) + +if (:s2 == 1) [forward :step] +if (:s2 == 2) [left 90 forward :step right 90] +if (:s2 == 3) [backward :step] +if (:s2 == 4) [left 90 backward :step right 90] + +assume !(:turtleX == :obs1x && :turtleY == :obs1y) +assume !(:turtleX == :obs2x && :turtleY == :obs2y) + +if (:s3 == 1) [forward :step] +if (:s3 == 2) [left 90 forward :step right 90] +if (:s3 == 3) [backward :step] +if (:s3 == 4) [left 90 backward :step right 90] + +assume !(:turtleX == :obs1x && :turtleY == :obs1y) +assume !(:turtleX == :obs2x && :turtleY == :obs2y) + +if (:s4 == 1) [forward :step] +if (:s4 == 2) [left 90 forward :step right 90] +if (:s4 == 3) [backward :step] +if (:s4 == 4) [left 90 backward :step right 90] + +assume !(:turtleX == :obs1x && :turtleY == :obs1y) +assume !(:turtleX == :obs2x && :turtleY == :obs2y) + +if (:s5 == 1) [forward :step] +if (:s5 == 2) [left 90 forward :step right 90] +if (:s5 == 3) [backward :step] +if (:s5 == 4) [left 90 backward :step right 90] + +assume !(:turtleX == :obs1x && :turtleY == :obs1y) +assume !(:turtleX == :obs2x && :turtleY == :obs2y) + +assert !(:turtleX == :targetX && :turtleY == :targetY) + + +/* +This code assumes that the turtle can move in a 2D grid in 4 directions, moving :steps amount of distance at a time. +We check whether there is a path from (0, 0) to (:targetX, :targetY) that is reachable in at most 5 steps, also avoiding the 2 obstacles. +In each step, turtle decides to not move or move in +x, +y, -x, -y directions (corresponding to values 0, 1, 2, 3, 4 respectively). +We assert that the turtle is unable to reach the target. If there exists a path then the assertion is false and BMC returns a path. +*/ + diff --git a/ChironCore/bmc_examples/shortest_path.tl b/ChironCore/bmc_examples/shortest_path.tl new file mode 100644 index 0000000..d9d2ef6 --- /dev/null +++ b/ChironCore/bmc_examples/shortest_path.tl @@ -0,0 +1,83 @@ + +// max steps = 5, max obstacles = 2 + +assume :s1 == 0 || :s1 == 1 || :s1 == 2 || :s1 == 3 || :s1 == 4 +assume :s2 == 0 || :s2 == 1 || :s2 == 2 || :s2 == 3 || :s2 == 4 +assume :s3 == 0 || :s3 == 1 || :s3 == 2 || :s3 == 3 || :s3 == 4 +assume :s4 == 0 || :s4 == 1 || :s4 == 2 || :s4 == 3 || :s4 == 4 +assume :s5 == 0 || :s5 == 1 || :s5 == 2 || :s5 == 3 || :s5 == 4 + +assume !(:s4 == 0) || (:s5 == 0) +assume !(:s3 == 0) || (:s5 == 0 && :s4 == 0) +assume !(:s2 == 0) || (:s5 == 0 && :s4 == 0 && :s3 == 0) +assume !(:s1 == 0) || (:s5 == 0 && :s4 == 0 && :s3 == 0 && :s2 == 0) + +:step = 50 + +:length = 0 + +:targetX = 3 * :step +:targetY = 0 * :step + +:obs1x = 1 * :step +:obs1y = 1 * :step + +:obs2x = 0 * :step +:obs2y = 1 * :step + +assume !(:turtleX == :obs1x && :turtleY == :obs1y) +assume !(:turtleX == :obs2x && :turtleY == :obs2y) + +if (:s1 == 1) [forward :step] +if (:s1 == 2) [left 90 forward :step right 90] +if (:s1 == 3) [backward :step] +if (:s1 == 4) [left 90 backward :step right 90] +if (:s1 != 0) [:length = :length + 1] + +assume !(:turtleX == :obs1x && :turtleY == :obs1y) +assume !(:turtleX == :obs2x && :turtleY == :obs2y) + +if (:s2 == 1) [forward :step] +if (:s2 == 2) [left 90 forward :step right 90] +if (:s2 == 3) [backward :step] +if (:s2 == 4) [left 90 backward :step right 90] +if (:s2 != 0) [:length = :length + 1] + +assume !(:turtleX == :obs1x && :turtleY == :obs1y) +assume !(:turtleX == :obs2x && :turtleY == :obs2y) + +if (:s3 == 1) [forward :step] +if (:s3 == 2) [left 90 forward :step right 90] +if (:s3 == 3) [backward :step] +if (:s3 == 4) [left 90 backward :step right 90] +if (:s3 != 0) [:length = :length + 1] + +assume !(:turtleX == :obs1x && :turtleY == :obs1y) +assume !(:turtleX == :obs2x && :turtleY == :obs2y) + +if (:s4 == 1) [forward :step] +if (:s4 == 2) [left 90 forward :step right 90] +if (:s4 == 3) [backward :step] +if (:s4 == 4) [left 90 backward :step right 90] +if (:s4 != 0) [:length = :length + 1] + +assume !(:turtleX == :obs1x && :turtleY == :obs1y) +assume !(:turtleX == :obs2x && :turtleY == :obs2y) + +if (:s5 == 1) [forward :step] +if (:s5 == 2) [left 90 forward :step right 90] +if (:s5 == 3) [backward :step] +if (:s5 == 4) [left 90 backward :step right 90] +if (:s5 != 0) [:length = :length + 1] + +assume !(:turtleX == :obs1x && :turtleY == :obs1y) +assume !(:turtleX == :obs2x && :turtleY == :obs2y) + +assert !(:turtleX == :targetX && :turtleY == :targetY && :length <= 2) + + +/* +Similar to the path planning code, this code gives us a path that has least distance to travel. +Only the assert statement is changed. Rest of the code is same. +*/ + diff --git a/ChironCore/cfg/ChironCFG.py b/ChironCore/cfg/ChironCFG.py index f0230be..7bcb3c5 100644 --- a/ChironCore/cfg/ChironCFG.py +++ b/ChironCore/cfg/ChironCFG.py @@ -1,11 +1,14 @@ #!/usr/bin/python3.8 import networkx as nx +import z3 +import collections class BasicBlock: def __init__(self, bbname): self.name = bbname self.instrlist = [] + self.condition = z3.BoolVal(False) if bbname == "START" or bbname == "END": self.irID = bbname else: @@ -20,9 +23,15 @@ def append(self, instruction): def extend(self, instructions): self.instrlist.extend(instructions) + def set_condition(self, condition): + self.condition = condition + + def get_condition(self): + return self.condition + def label(self): if len(self.instrlist): - return '\n'.join(str(instr[0])+'; L'+ str(instr[1]) for instr in self.instrlist) + return self.name + '\n' + '\n'.join(str(instr[0])+'; L'+ str(instr[1]) for instr in self.instrlist) else: return self.name @@ -38,6 +47,9 @@ def __init__(self, gname='cfg'): self.nxgraph = nx.DiGraph(name=gname) self.entry = "0" self.exit = "END" + self.df = None + self.idom = None + self.dominator_tree = collections.defaultdict(list) def __iter__(self): return self.nxgraph.__iter__() @@ -86,4 +98,24 @@ def get_edge_label(self, u, v): edata = self.nxgraph.get_edge_data(u,v) return edata['label'] if len(edata) else 'T' + def compute_dominance(self): + entry = None + for node in self.nxgraph.nodes(): + if node.name == "START": + entry = node + break + + if entry is None: + raise ValueError("CFG does not have an entry node") + + self.idom = nx.immediate_dominators(self.nxgraph, entry) + self.df = nx.dominance_frontiers(self.nxgraph, entry) + + # build the dominator tree + for i in self.nodes(): + if i != entry: + self.dominator_tree[self.idom[i]].append(i) + + def get_topological_order(self): + return list(nx.topological_sort(self.nxgraph)) # TODO: add more methods to expose other methods of the Networkx.DiGraph diff --git a/ChironCore/cfg/cfgBuilder.py b/ChironCore/cfg/cfgBuilder.py index 1bc5460..21ec892 100644 --- a/ChironCore/cfg/cfgBuilder.py +++ b/ChironCore/cfg/cfgBuilder.py @@ -5,6 +5,8 @@ from cfg.ChironCFG import * import ChironAST.ChironAST as ChironAST +import ChironTAC.ChironTAC as ChironTAC +import ChironSSA.ChironSSA as ChironSSA import networkx as nx from networkx.drawing.nx_agraph import to_agraph @@ -28,7 +30,7 @@ def buildCFG(ir, cfgName="", isSingle=False): # finding leaders in the IR for idx, item in enumerate(ir): #print(idx, item) - if isinstance(item[0], ChironAST.ConditionCommand) or isSingle: + if isinstance(item[0], ChironAST.ConditionCommand) or isinstance(item[0], ChironTAC.ConditionCommand) or isinstance(item[0], ChironSSA.ConditionCommand) or isSingle: # updating then branch meta data if idx + 1 < len(ir) and (idx + 1 not in leaderIndices): leaderIndices.add(idx + 1) @@ -36,8 +38,7 @@ def buildCFG(ir, cfgName="", isSingle=False): leader2IndicesMap[thenBranchLeader] = idx + 1 indices2LeadersMap[idx + 1] = thenBranchLeader - if idx + item[1] < len(ir) and (idx + item[1] - not in leaderIndices) and (isinstance(item[0], ChironAST.ConditionCommand)): + if idx + item[1] < len(ir) and (idx + item[1] not in leaderIndices) and (isinstance(item[0], ChironAST.ConditionCommand) or isinstance(item[0], ChironTAC.ConditionCommand) or isinstance(item[0], ChironSSA.ConditionCommand)): leaderIndices.add(idx + item[1]) elseBranchLeader = BasicBlock(str(idx + item[1])) leader2IndicesMap[elseBranchLeader] = idx + item[1] @@ -66,13 +67,13 @@ def buildCFG(ir, cfgName="", isSingle=False): irIdx = (node.instrlist[-1])[1] lastInstr = (node.instrlist[-1])[0] # print (irIdx, lastInstr, type(lastInstr), isinstance(lastInstr, ChironAST.ConditionCommand)) - if isinstance(lastInstr, ChironAST.ConditionCommand): - if not isinstance(lastInstr.cond, ChironAST.BoolFalse): + if isinstance(lastInstr, ChironAST.ConditionCommand) or isinstance(lastInstr, ChironTAC.ConditionCommand) or isinstance(lastInstr, ChironSSA.ConditionCommand): + if not (isinstance(lastInstr.cond, ChironAST.BoolFalse) or isinstance(lastInstr.cond, ChironTAC.BoolFalse) or isinstance(lastInstr.cond, ChironSSA.BoolFalse)): thenIdx = irIdx + 1 if (irIdx + 1 < len(ir)) else len(ir) thenBB = indices2LeadersMap[thenIdx] cfg.add_edge(node, thenBB, label='Cond_True', color='green') - if not isinstance(lastInstr.cond, ChironAST.BoolTrue): + if not (isinstance(lastInstr.cond, ChironAST.BoolTrue) or isinstance(lastInstr.cond, ChironTAC.BoolTrue) or isinstance(lastInstr.cond, ChironSSA.BoolTrue)): elseIdx = irIdx + ir[irIdx][1] if (irIdx + ir[irIdx][1] < len(ir)) else len(ir) elseBB = indices2LeadersMap[elseIdx] cfg.add_edge(node, elseBB, label='Cond_False', color='red') @@ -80,8 +81,16 @@ def buildCFG(ir, cfgName="", isSingle=False): nextBB = indices2LeadersMap[irIdx + 1] if (irIdx + 1 < len(ir)) else endBB cfg.add_edge(node, nextBB, label='flow_edge', color='blue') - return cfg + line2BlockMap = {} + last_block = None + for line in range(len(ir)): + if line in indices2LeadersMap.keys(): + last_block = indices2LeadersMap[line] + line2BlockMap[line] = last_block + line2BlockMap[len(ir)] = endBB + + return cfg, line2BlockMap def dumpCFG(cfg, filename="out"): diff --git a/ChironCore/chiron.py b/ChironCore/chiron.py index 2eca801..2310fc9 100755 --- a/ChironCore/chiron.py +++ b/ChironCore/chiron.py @@ -3,6 +3,8 @@ import ast import sys + +from antlr4 import InputStream from ChironAST.builder import astGenPass import abstractInterpretation as AI import dataFlowAnalysis as DFA @@ -21,6 +23,10 @@ from fuzzer import * import sExecution as se import cfg.cfgBuilder as cfgB +import bmc as bmc +import unroll as unroll +from ChironTAC.builder import * +from ChironSSA.builder import * import submissionDFA as DFASub import submissionAI as AISub from sbflSubmission import computeRanks @@ -196,12 +202,36 @@ def stopTurtle(): type=bool, ) + cmdparser.add_argument( # example usage: ./chiron.py -bmc -ub 20 -aconf + "-bmc", + "--bmc", + action="store_true", + help="Run Bounded Model Checking on a Chiron Program", + ) + + cmdparser.add_argument( + "-ub", + "--unroll-bound", + type=int, + default=10, + help="Unroll bound for the BMC engine. Default is 10", + ) + + cmdparser.add_argument( # By default we take angles 0, 90, 180 and 270 + "-aconf", + "--angle-conf", + type=str, + default="", + help="Angle configuration file for BMC", + ) + args = cmdparser.parse_args() ir = "" if not (type(args.params) is dict): raise ValueError("Wrong type for command line arguement '-d' or '--params'.") + # Instantiate the irHandler # this object is passed around everywhere. irHandler = IRHandler(ir) @@ -392,3 +422,64 @@ def stopTurtle(): writer = csv.writer(file) writer.writerows(spectrum) print("DONE..") + + if args.bmc: + print("\nBounded Model Checking...") + unroll_bound = args.unroll_bound + + angle_conf = [[0, 1, 0], [90, 0, 1], [180, -1, 0], [270, 0, -1]] + if args.angle_conf: + with open(args.angle_conf, "r") as f: + angle_conf = f.read() + # csv format (angle,cos,sin) + angle_conf = [x.split(",") for x in angle_conf.split("\n") if x] + angle_conf = [ + (int(x[0]), float(x[1]), float(x[2])) for x in angle_conf + ] + + print("Valid angles: ", angle_conf) + + if unroll_bound < 1: + print("Invalid unroll bound. Exiting...") + exit(1) + + unrolled_code = unroll.UnrollLoops(unroll_bound).visitStart(getParseTree(args.progfl)) + + with open("unrolled_code.tl", "w") as f: # Saving unrolled code to file unrolled_code.tl + f.write(unrolled_code) + + try: + lexer = tlangLexer(InputStream(unrolled_code)) + stream = antlr4.CommonTokenStream(lexer) + lexer._listeners = [SyntaxErrorListener()] + tparser = tlangParser(stream) + tparser._listeners = [SyntaxErrorListener()] + parseTree = tparser.start() + except Exception as e: + print("\033[91m\n====================") + print(e.__str__() + "\033[0m\n") + exit(1) + + astgen = astGenPass() + ir = astgen.visitStart(parseTree) + + tacGen = TACGenerator(ir) # Converting IR to TAC + tacGen.generateTAC() + # tacGen.printTAC() # for printing TAC + + if tacGen.assertCount == 0: + print("No conditions found in the program. Exiting...") + exit(1) + + cfgB.dumpCFG(tacGen.tacCfg, 'tac_cfg') # Saving TAC CFG to file tac_cfg.png + + ssa = SSABuilder(tacGen.tac) # Converting TAC to SSA + ssaCfg = ssa.build() + + cfgB.dumpCFG(ssaCfg, 'ssa_cfg') # Saving SSA Form of the program to file ssa_cfg.png + + print("\nConverting program to SMT-LIB format...\n") + smt = bmc.BMC(ssaCfg, angle_conf) + smt.convertSSAtoSMT() + smt.solve(tacGen.getFreeVariables()) + print("DONE...") diff --git a/ChironCore/example/example1.tl b/ChironCore/example/example1.tl index 7d15f80..9e64a04 100644 --- a/ChironCore/example/example1.tl +++ b/ChironCore/example/example1.tl @@ -35,4 +35,6 @@ repeat 3 [ :z = :z + 10 ] -penup \ No newline at end of file +penup + +assert :turtleX > 0 diff --git a/ChironCore/interpreter.py b/ChironCore/interpreter.py index bb30bcb..ec56cf5 100644 --- a/ChironCore/interpreter.py +++ b/ChironCore/interpreter.py @@ -107,6 +107,10 @@ def interpret(self): ntgt = self.handleGotoCommand(stmt, tgt) elif isinstance(stmt, ChironAST.NoOpCommand): ntgt = self.handleNoOpCommand(stmt, tgt) + elif isinstance(stmt, ChironAST.AssertCommand): + ntgt = self.handleAssertCommand(stmt, tgt) + elif isinstance(stmt, ChironAST.AssumeCommand): + ntgt = self.handleAssumeCommand(stmt, tgt) else: raise NotImplementedError("Unknown instruction: %s, %s."%(type(stmt), stmt)) @@ -164,3 +168,28 @@ def handleGotoCommand(self, stmt, tgt): ycor = addContext(stmt.ycor) exec("self.trtl.goto(%s, %s)" % (xcor, ycor)) return 1 + + def handleAssertCommand(self, stmt, tgt): + print(" AssertCommand") + print(" Asserting: ", stmt.cond) + try: + exec("self.cond_eval = %s" % (addContext(stmt.cond))) + if not self.cond_eval: + raise AssertionError("Assertion Failed!") + except Exception as e: + print("Exception: ", e) + + return 1 + + def handleAssumeCommand(self, stmt, tgt): + print(" AssumeCommand") + print(" Assuming: ", stmt.cond) + try: + exec("self.cond_eval = %s" % (addContext(stmt.cond))) + if not self.cond_eval: + raise AssertionError("Assumption Failed!") + except Exception as e: + print("Exception: ", e) + + return 1 + diff --git a/ChironCore/irhandler.py b/ChironCore/irhandler.py index 56e60de..3e0af2a 100644 --- a/ChironCore/irhandler.py +++ b/ChironCore/irhandler.py @@ -10,7 +10,7 @@ def getParseTree(progfl): input_stream = antlr4.FileStream(progfl) - print(input_stream) + # print(input_stream) try: lexer = tlangLexer(input_stream) stream = antlr4.CommonTokenStream(lexer) @@ -114,7 +114,7 @@ def removeInstruction(self, stmtList, pos): print("[Skip] Instruction Type not supported for removal. \n") return - if "__rep_counter_" in str(stmtList[pos][0]): + if ":__rep_counter_" in str(stmtList[pos][0]): print("[Skip] Instruction affecting loop counter. \n") return @@ -123,10 +123,14 @@ def removeInstruction(self, stmtList, pos): def pretty_print(self, irList): """ - We pass a IR list and print it here. + We pass a IR list and print it here. """ print("\n========== Chiron IR ==========\n") - print("The first label before the opcode name represents the IR index or label \non the control flow graph for that node.\n") - print("The number after the opcode name represents the jump offset \nrelative to that statement.\n") + print( + "The first label before the opcode name represents the IR index or label \non the control flow graph for that node.\n" + ) + print( + "The number after the opcode name represents the jump offset \nrelative to that statement.\n" + ) for idx, item in enumerate(irList): - print(f"[L{idx}]".rjust(5), item[0], f"[{item[1]}]") \ No newline at end of file + print(f"[L{idx}]".rjust(5), item[0], f"[{item[1]}]") diff --git a/ChironCore/turtparse/tlang.g4 b/ChironCore/turtparse/tlang.g4 index ff3a2f6..f840290 100644 --- a/ChironCore/turtparse/tlang.g4 +++ b/ChironCore/turtparse/tlang.g4 @@ -17,6 +17,8 @@ instruction : assignment | penCommand | gotoCommand | pauseCommand + | assertionCommand + | assumeCommand ; conditional : ifConditional | ifElseConditional ; @@ -25,7 +27,8 @@ ifConditional : 'if' condition '[' strict_ilist ']' ; ifElseConditional : 'if' condition '[' strict_ilist ']' 'else' '[' strict_ilist ']' ; -loop : 'repeat' value '[' strict_ilist ']' ; +loop : 'repeat' value '[' strict_ilist ']' + | '@unroll' NUM 'repeat' value '[' strict_ilist ']' ; gotoCommand : 'goto' '(' expression ',' expression ')'; @@ -39,16 +42,22 @@ penCommand : 'penup' | 'pendown' ; pauseCommand : 'pause' ; +assertionCommand : 'assert' condition ; + +assumeCommand : 'assume' condition ; + expression : unaryArithOp expression #unaryExpr | expression multiplicative expression #mulExpr | expression additive expression #addExpr + | expression modulo expression #modExpr | value #valueExpr | '(' expression ')' #parenExpr ; multiplicative : MUL | DIV; additive : PLUS | MINUS; +modulo : MOD; unaryArithOp : MINUS ; @@ -56,6 +65,7 @@ PLUS : '+' ; MINUS : '-' ; MUL : '*' ; DIV : '/' ; +MOD : '%' ; // TODO : @@ -85,14 +95,20 @@ AND: '&&'; OR : '||'; NOT: '!' ; -value : NUM +value : NUM | VAR + | FLOAT ; NUM : [0-9]+ ; +FLOAT : NUM '.' NUM ; + VAR : ':'[a-zA-Z_] [a-zA-Z0-9]* ; NAME : [a-zA-Z]+ ; -Whitespace: [ \t\n\r]+ -> skip; +Whitespace : [ \t\n\r]+ -> skip; + +COMMENT_LINE : '//' ~[\r\n]* -> skip; +COMMENT_BLOCK : '/*' .*? '*/' -> skip; diff --git a/ChironCore/turtparse/tlang.interp b/ChironCore/turtparse/tlang.interp index f3cba53..007a475 100644 --- a/ChironCore/turtparse/tlang.interp +++ b/ChironCore/turtparse/tlang.interp @@ -5,6 +5,7 @@ null ']' 'else' 'repeat' +'@unroll' 'goto' '(' ',' @@ -17,10 +18,13 @@ null 'penup' 'pendown' 'pause' +'assert' +'assume' '+' '-' '*' '/' +'%' 'pendown?' '<' '>' @@ -35,6 +39,9 @@ null null null null +null +null +null token symbolic names: null @@ -55,10 +62,14 @@ null null null null +null +null +null PLUS MINUS MUL DIV +MOD PENCOND LT GT @@ -70,9 +81,12 @@ AND OR NOT NUM +FLOAT VAR NAME Whitespace +COMMENT_LINE +COMMENT_BLOCK rule names: start @@ -89,9 +103,12 @@ moveCommand moveOp penCommand pauseCommand +assertionCommand +assumeCommand expression multiplicative additive +modulo unaryArithOp condition binCondOp @@ -100,4 +117,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, 44, 205, 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, 3, 2, 3, 2, 3, 2, 3, 3, 7, 3, 57, 10, 3, 12, 3, 14, 3, 60, 11, 3, 3, 4, 6, 4, 63, 10, 4, 13, 4, 14, 4, 64, 3, 5, 3, 5, 3, 5, 3, 5, 3, 5, 3, 5, 3, 5, 3, 5, 3, 5, 5, 5, 76, 10, 5, 3, 6, 3, 6, 5, 6, 80, 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, 9, 3, 9, 3, 9, 3, 9, 3, 9, 3, 9, 3, 9, 3, 9, 5, 9, 112, 10, 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, 17, 3, 17, 3, 17, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 5, 18, 149, 10, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 3, 18, 7, 18, 163, 10, 18, 12, 18, 14, 18, 166, 11, 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, 23, 3, 23, 3, 23, 5, 23, 188, 10, 23, 3, 23, 3, 23, 3, 23, 3, 23, 7, 23, 194, 10, 23, 12, 23, 14, 23, 197, 11, 23, 3, 24, 3, 24, 3, 25, 3, 25, 3, 26, 3, 26, 3, 26, 2, 4, 34, 44, 27, 2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38, 40, 42, 44, 46, 48, 50, 2, 9, 3, 2, 14, 17, 3, 2, 18, 19, 3, 2, 25, 26, 3, 2, 23, 24, 3, 2, 29, 34, 3, 2, 35, 36, 3, 2, 38, 40, 2, 200, 2, 52, 3, 2, 2, 2, 4, 58, 3, 2, 2, 2, 6, 62, 3, 2, 2, 2, 8, 75, 3, 2, 2, 2, 10, 79, 3, 2, 2, 2, 12, 81, 3, 2, 2, 2, 14, 87, 3, 2, 2, 2, 16, 111, 3, 2, 2, 2, 18, 113, 3, 2, 2, 2, 20, 120, 3, 2, 2, 2, 22, 124, 3, 2, 2, 2, 24, 127, 3, 2, 2, 2, 26, 129, 3, 2, 2, 2, 28, 131, 3, 2, 2, 2, 30, 133, 3, 2, 2, 2, 32, 136, 3, 2, 2, 2, 34, 148, 3, 2, 2, 2, 36, 167, 3, 2, 2, 2, 38, 169, 3, 2, 2, 2, 40, 171, 3, 2, 2, 2, 42, 173, 3, 2, 2, 2, 44, 187, 3, 2, 2, 2, 46, 198, 3, 2, 2, 2, 48, 200, 3, 2, 2, 2, 50, 202, 3, 2, 2, 2, 52, 53, 5, 4, 3, 2, 53, 54, 7, 2, 2, 3, 54, 3, 3, 2, 2, 2, 55, 57, 5, 8, 5, 2, 56, 55, 3, 2, 2, 2, 57, 60, 3, 2, 2, 2, 58, 56, 3, 2, 2, 2, 58, 59, 3, 2, 2, 2, 59, 5, 3, 2, 2, 2, 60, 58, 3, 2, 2, 2, 61, 63, 5, 8, 5, 2, 62, 61, 3, 2, 2, 2, 63, 64, 3, 2, 2, 2, 64, 62, 3, 2, 2, 2, 64, 65, 3, 2, 2, 2, 65, 7, 3, 2, 2, 2, 66, 76, 5, 20, 11, 2, 67, 76, 5, 10, 6, 2, 68, 76, 5, 16, 9, 2, 69, 76, 5, 22, 12, 2, 70, 76, 5, 26, 14, 2, 71, 76, 5, 18, 10, 2, 72, 76, 5, 28, 15, 2, 73, 76, 5, 30, 16, 2, 74, 76, 5, 32, 17, 2, 75, 66, 3, 2, 2, 2, 75, 67, 3, 2, 2, 2, 75, 68, 3, 2, 2, 2, 75, 69, 3, 2, 2, 2, 75, 70, 3, 2, 2, 2, 75, 71, 3, 2, 2, 2, 75, 72, 3, 2, 2, 2, 75, 73, 3, 2, 2, 2, 75, 74, 3, 2, 2, 2, 76, 9, 3, 2, 2, 2, 77, 80, 5, 12, 7, 2, 78, 80, 5, 14, 8, 2, 79, 77, 3, 2, 2, 2, 79, 78, 3, 2, 2, 2, 80, 11, 3, 2, 2, 2, 81, 82, 7, 3, 2, 2, 82, 83, 5, 44, 23, 2, 83, 84, 7, 4, 2, 2, 84, 85, 5, 6, 4, 2, 85, 86, 7, 5, 2, 2, 86, 13, 3, 2, 2, 2, 87, 88, 7, 3, 2, 2, 88, 89, 5, 44, 23, 2, 89, 90, 7, 4, 2, 2, 90, 91, 5, 6, 4, 2, 91, 92, 7, 5, 2, 2, 92, 93, 7, 6, 2, 2, 93, 94, 7, 4, 2, 2, 94, 95, 5, 6, 4, 2, 95, 96, 7, 5, 2, 2, 96, 15, 3, 2, 2, 2, 97, 98, 7, 7, 2, 2, 98, 99, 5, 50, 26, 2, 99, 100, 7, 4, 2, 2, 100, 101, 5, 6, 4, 2, 101, 102, 7, 5, 2, 2, 102, 112, 3, 2, 2, 2, 103, 104, 7, 8, 2, 2, 104, 105, 7, 38, 2, 2, 105, 106, 7, 7, 2, 2, 106, 107, 5, 50, 26, 2, 107, 108, 7, 4, 2, 2, 108, 109, 5, 6, 4, 2, 109, 110, 7, 5, 2, 2, 110, 112, 3, 2, 2, 2, 111, 97, 3, 2, 2, 2, 111, 103, 3, 2, 2, 2, 112, 17, 3, 2, 2, 2, 113, 114, 7, 9, 2, 2, 114, 115, 7, 10, 2, 2, 115, 116, 5, 34, 18, 2, 116, 117, 7, 11, 2, 2, 117, 118, 5, 34, 18, 2, 118, 119, 7, 12, 2, 2, 119, 19, 3, 2, 2, 2, 120, 121, 7, 40, 2, 2, 121, 122, 7, 13, 2, 2, 122, 123, 5, 34, 18, 2, 123, 21, 3, 2, 2, 2, 124, 125, 5, 24, 13, 2, 125, 126, 5, 34, 18, 2, 126, 23, 3, 2, 2, 2, 127, 128, 9, 2, 2, 2, 128, 25, 3, 2, 2, 2, 129, 130, 9, 3, 2, 2, 130, 27, 3, 2, 2, 2, 131, 132, 7, 20, 2, 2, 132, 29, 3, 2, 2, 2, 133, 134, 7, 21, 2, 2, 134, 135, 5, 44, 23, 2, 135, 31, 3, 2, 2, 2, 136, 137, 7, 22, 2, 2, 137, 138, 5, 44, 23, 2, 138, 33, 3, 2, 2, 2, 139, 140, 8, 18, 1, 2, 140, 141, 5, 42, 22, 2, 141, 142, 5, 34, 18, 8, 142, 149, 3, 2, 2, 2, 143, 149, 5, 50, 26, 2, 144, 145, 7, 10, 2, 2, 145, 146, 5, 34, 18, 2, 146, 147, 7, 12, 2, 2, 147, 149, 3, 2, 2, 2, 148, 139, 3, 2, 2, 2, 148, 143, 3, 2, 2, 2, 148, 144, 3, 2, 2, 2, 149, 164, 3, 2, 2, 2, 150, 151, 12, 7, 2, 2, 151, 152, 5, 36, 19, 2, 152, 153, 5, 34, 18, 8, 153, 163, 3, 2, 2, 2, 154, 155, 12, 6, 2, 2, 155, 156, 5, 38, 20, 2, 156, 157, 5, 34, 18, 7, 157, 163, 3, 2, 2, 2, 158, 159, 12, 5, 2, 2, 159, 160, 5, 40, 21, 2, 160, 161, 5, 34, 18, 6, 161, 163, 3, 2, 2, 2, 162, 150, 3, 2, 2, 2, 162, 154, 3, 2, 2, 2, 162, 158, 3, 2, 2, 2, 163, 166, 3, 2, 2, 2, 164, 162, 3, 2, 2, 2, 164, 165, 3, 2, 2, 2, 165, 35, 3, 2, 2, 2, 166, 164, 3, 2, 2, 2, 167, 168, 9, 4, 2, 2, 168, 37, 3, 2, 2, 2, 169, 170, 9, 5, 2, 2, 170, 39, 3, 2, 2, 2, 171, 172, 7, 27, 2, 2, 172, 41, 3, 2, 2, 2, 173, 174, 7, 24, 2, 2, 174, 43, 3, 2, 2, 2, 175, 176, 8, 23, 1, 2, 176, 177, 7, 37, 2, 2, 177, 188, 5, 44, 23, 7, 178, 179, 5, 34, 18, 2, 179, 180, 5, 46, 24, 2, 180, 181, 5, 34, 18, 2, 181, 188, 3, 2, 2, 2, 182, 188, 7, 28, 2, 2, 183, 184, 7, 10, 2, 2, 184, 185, 5, 44, 23, 2, 185, 186, 7, 12, 2, 2, 186, 188, 3, 2, 2, 2, 187, 175, 3, 2, 2, 2, 187, 178, 3, 2, 2, 2, 187, 182, 3, 2, 2, 2, 187, 183, 3, 2, 2, 2, 188, 195, 3, 2, 2, 2, 189, 190, 12, 5, 2, 2, 190, 191, 5, 48, 25, 2, 191, 192, 5, 44, 23, 6, 192, 194, 3, 2, 2, 2, 193, 189, 3, 2, 2, 2, 194, 197, 3, 2, 2, 2, 195, 193, 3, 2, 2, 2, 195, 196, 3, 2, 2, 2, 196, 45, 3, 2, 2, 2, 197, 195, 3, 2, 2, 2, 198, 199, 9, 6, 2, 2, 199, 47, 3, 2, 2, 2, 200, 201, 9, 7, 2, 2, 201, 49, 3, 2, 2, 2, 202, 203, 9, 8, 2, 2, 203, 51, 3, 2, 2, 2, 12, 58, 64, 75, 79, 111, 148, 162, 164, 187, 195] \ No newline at end of file diff --git a/ChironCore/turtparse/tlang.tokens b/ChironCore/turtparse/tlang.tokens index 78f9526..39f4806 100644 --- a/ChironCore/turtparse/tlang.tokens +++ b/ChironCore/turtparse/tlang.tokens @@ -15,52 +15,63 @@ 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 +FLOAT=37 +VAR=38 +NAME=39 +Whitespace=40 +COMMENT_LINE=41 +COMMENT_BLOCK=42 'if'=1 '['=2 ']'=3 'else'=4 'repeat'=5 -'goto'=6 -'('=7 -','=8 -')'=9 -'='=10 -'forward'=11 -'backward'=12 -'left'=13 -'right'=14 -'penup'=15 -'pendown'=16 -'pause'=17 -'+'=18 -'-'=19 -'*'=20 -'/'=21 -'pendown?'=22 -'<'=23 -'>'=24 -'=='=25 -'!='=26 -'<='=27 -'>='=28 -'&&'=29 -'||'=30 -'!'=31 +'@unroll'=6 +'goto'=7 +'('=8 +','=9 +')'=10 +'='=11 +'forward'=12 +'backward'=13 +'left'=14 +'right'=15 +'penup'=16 +'pendown'=17 +'pause'=18 +'assert'=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..4829228 100644 --- a/ChironCore/turtparse/tlangLexer.interp +++ b/ChironCore/turtparse/tlangLexer.interp @@ -5,6 +5,7 @@ null ']' 'else' 'repeat' +'@unroll' 'goto' '(' ',' @@ -17,10 +18,13 @@ null 'penup' 'pendown' 'pause' +'assert' +'assume' '+' '-' '*' '/' +'%' 'pendown?' '<' '>' @@ -35,6 +39,9 @@ null null null null +null +null +null token symbolic names: null @@ -55,10 +62,14 @@ null null null null +null +null +null PLUS MINUS MUL DIV +MOD PENCOND LT GT @@ -70,9 +81,12 @@ AND OR NOT NUM +FLOAT VAR NAME Whitespace +COMMENT_LINE +COMMENT_BLOCK rule names: T__0 @@ -92,10 +106,14 @@ T__13 T__14 T__15 T__16 +T__17 +T__18 +T__19 PLUS MINUS MUL DIV +MOD PENCOND LT GT @@ -107,9 +125,12 @@ AND OR NOT NUM +FLOAT VAR NAME Whitespace +COMMENT_LINE +COMMENT_BLOCK channel names: DEFAULT_TOKEN_CHANNEL @@ -119,4 +140,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, 44, 286, 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, 4, 41, 9, 41, 4, 42, 9, 42, 4, 43, 9, 43, 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, 7, 3, 7, 3, 7, 3, 8, 3, 8, 3, 8, 3, 8, 3, 8, 3, 9, 3, 9, 3, 10, 3, 10, 3, 11, 3, 11, 3, 12, 3, 12, 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, 14, 3, 14, 3, 14, 3, 14, 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, 18, 3, 18, 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, 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, 234, 10, 37, 13, 37, 14, 37, 235, 3, 38, 3, 38, 3, 38, 3, 38, 3, 39, 3, 39, 3, 39, 7, 39, 245, 10, 39, 12, 39, 14, 39, 248, 11, 39, 3, 40, 6, 40, 251, 10, 40, 13, 40, 14, 40, 252, 3, 41, 6, 41, 256, 10, 41, 13, 41, 14, 41, 257, 3, 41, 3, 41, 3, 42, 3, 42, 3, 42, 3, 42, 7, 42, 266, 10, 42, 12, 42, 14, 42, 269, 11, 42, 3, 42, 3, 42, 3, 43, 3, 43, 3, 43, 3, 43, 7, 43, 277, 10, 43, 12, 43, 14, 43, 280, 11, 43, 3, 43, 3, 43, 3, 43, 3, 43, 3, 43, 3, 278, 2, 44, 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, 81, 42, 83, 43, 85, 44, 3, 2, 8, 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, 4, 2, 12, 12, 15, 15, 2, 291, 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, 2, 81, 3, 2, 2, 2, 2, 83, 3, 2, 2, 2, 2, 85, 3, 2, 2, 2, 3, 87, 3, 2, 2, 2, 5, 90, 3, 2, 2, 2, 7, 92, 3, 2, 2, 2, 9, 94, 3, 2, 2, 2, 11, 99, 3, 2, 2, 2, 13, 106, 3, 2, 2, 2, 15, 114, 3, 2, 2, 2, 17, 119, 3, 2, 2, 2, 19, 121, 3, 2, 2, 2, 21, 123, 3, 2, 2, 2, 23, 125, 3, 2, 2, 2, 25, 127, 3, 2, 2, 2, 27, 135, 3, 2, 2, 2, 29, 144, 3, 2, 2, 2, 31, 149, 3, 2, 2, 2, 33, 155, 3, 2, 2, 2, 35, 161, 3, 2, 2, 2, 37, 169, 3, 2, 2, 2, 39, 175, 3, 2, 2, 2, 41, 182, 3, 2, 2, 2, 43, 189, 3, 2, 2, 2, 45, 191, 3, 2, 2, 2, 47, 193, 3, 2, 2, 2, 49, 195, 3, 2, 2, 2, 51, 197, 3, 2, 2, 2, 53, 199, 3, 2, 2, 2, 55, 208, 3, 2, 2, 2, 57, 210, 3, 2, 2, 2, 59, 212, 3, 2, 2, 2, 61, 215, 3, 2, 2, 2, 63, 218, 3, 2, 2, 2, 65, 221, 3, 2, 2, 2, 67, 224, 3, 2, 2, 2, 69, 227, 3, 2, 2, 2, 71, 230, 3, 2, 2, 2, 73, 233, 3, 2, 2, 2, 75, 237, 3, 2, 2, 2, 77, 241, 3, 2, 2, 2, 79, 250, 3, 2, 2, 2, 81, 255, 3, 2, 2, 2, 83, 261, 3, 2, 2, 2, 85, 272, 3, 2, 2, 2, 87, 88, 7, 107, 2, 2, 88, 89, 7, 104, 2, 2, 89, 4, 3, 2, 2, 2, 90, 91, 7, 93, 2, 2, 91, 6, 3, 2, 2, 2, 92, 93, 7, 95, 2, 2, 93, 8, 3, 2, 2, 2, 94, 95, 7, 103, 2, 2, 95, 96, 7, 110, 2, 2, 96, 97, 7, 117, 2, 2, 97, 98, 7, 103, 2, 2, 98, 10, 3, 2, 2, 2, 99, 100, 7, 116, 2, 2, 100, 101, 7, 103, 2, 2, 101, 102, 7, 114, 2, 2, 102, 103, 7, 103, 2, 2, 103, 104, 7, 99, 2, 2, 104, 105, 7, 118, 2, 2, 105, 12, 3, 2, 2, 2, 106, 107, 7, 66, 2, 2, 107, 108, 7, 119, 2, 2, 108, 109, 7, 112, 2, 2, 109, 110, 7, 116, 2, 2, 110, 111, 7, 113, 2, 2, 111, 112, 7, 110, 2, 2, 112, 113, 7, 110, 2, 2, 113, 14, 3, 2, 2, 2, 114, 115, 7, 105, 2, 2, 115, 116, 7, 113, 2, 2, 116, 117, 7, 118, 2, 2, 117, 118, 7, 113, 2, 2, 118, 16, 3, 2, 2, 2, 119, 120, 7, 42, 2, 2, 120, 18, 3, 2, 2, 2, 121, 122, 7, 46, 2, 2, 122, 20, 3, 2, 2, 2, 123, 124, 7, 43, 2, 2, 124, 22, 3, 2, 2, 2, 125, 126, 7, 63, 2, 2, 126, 24, 3, 2, 2, 2, 127, 128, 7, 104, 2, 2, 128, 129, 7, 113, 2, 2, 129, 130, 7, 116, 2, 2, 130, 131, 7, 121, 2, 2, 131, 132, 7, 99, 2, 2, 132, 133, 7, 116, 2, 2, 133, 134, 7, 102, 2, 2, 134, 26, 3, 2, 2, 2, 135, 136, 7, 100, 2, 2, 136, 137, 7, 99, 2, 2, 137, 138, 7, 101, 2, 2, 138, 139, 7, 109, 2, 2, 139, 140, 7, 121, 2, 2, 140, 141, 7, 99, 2, 2, 141, 142, 7, 116, 2, 2, 142, 143, 7, 102, 2, 2, 143, 28, 3, 2, 2, 2, 144, 145, 7, 110, 2, 2, 145, 146, 7, 103, 2, 2, 146, 147, 7, 104, 2, 2, 147, 148, 7, 118, 2, 2, 148, 30, 3, 2, 2, 2, 149, 150, 7, 116, 2, 2, 150, 151, 7, 107, 2, 2, 151, 152, 7, 105, 2, 2, 152, 153, 7, 106, 2, 2, 153, 154, 7, 118, 2, 2, 154, 32, 3, 2, 2, 2, 155, 156, 7, 114, 2, 2, 156, 157, 7, 103, 2, 2, 157, 158, 7, 112, 2, 2, 158, 159, 7, 119, 2, 2, 159, 160, 7, 114, 2, 2, 160, 34, 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, 36, 3, 2, 2, 2, 169, 170, 7, 114, 2, 2, 170, 171, 7, 99, 2, 2, 171, 172, 7, 119, 2, 2, 172, 173, 7, 117, 2, 2, 173, 174, 7, 103, 2, 2, 174, 38, 3, 2, 2, 2, 175, 176, 7, 99, 2, 2, 176, 177, 7, 117, 2, 2, 177, 178, 7, 117, 2, 2, 178, 179, 7, 103, 2, 2, 179, 180, 7, 116, 2, 2, 180, 181, 7, 118, 2, 2, 181, 40, 3, 2, 2, 2, 182, 183, 7, 99, 2, 2, 183, 184, 7, 117, 2, 2, 184, 185, 7, 117, 2, 2, 185, 186, 7, 119, 2, 2, 186, 187, 7, 111, 2, 2, 187, 188, 7, 103, 2, 2, 188, 42, 3, 2, 2, 2, 189, 190, 7, 45, 2, 2, 190, 44, 3, 2, 2, 2, 191, 192, 7, 47, 2, 2, 192, 46, 3, 2, 2, 2, 193, 194, 7, 44, 2, 2, 194, 48, 3, 2, 2, 2, 195, 196, 7, 49, 2, 2, 196, 50, 3, 2, 2, 2, 197, 198, 7, 39, 2, 2, 198, 52, 3, 2, 2, 2, 199, 200, 7, 114, 2, 2, 200, 201, 7, 103, 2, 2, 201, 202, 7, 112, 2, 2, 202, 203, 7, 102, 2, 2, 203, 204, 7, 113, 2, 2, 204, 205, 7, 121, 2, 2, 205, 206, 7, 112, 2, 2, 206, 207, 7, 65, 2, 2, 207, 54, 3, 2, 2, 2, 208, 209, 7, 62, 2, 2, 209, 56, 3, 2, 2, 2, 210, 211, 7, 64, 2, 2, 211, 58, 3, 2, 2, 2, 212, 213, 7, 63, 2, 2, 213, 214, 7, 63, 2, 2, 214, 60, 3, 2, 2, 2, 215, 216, 7, 35, 2, 2, 216, 217, 7, 63, 2, 2, 217, 62, 3, 2, 2, 2, 218, 219, 7, 62, 2, 2, 219, 220, 7, 63, 2, 2, 220, 64, 3, 2, 2, 2, 221, 222, 7, 64, 2, 2, 222, 223, 7, 63, 2, 2, 223, 66, 3, 2, 2, 2, 224, 225, 7, 40, 2, 2, 225, 226, 7, 40, 2, 2, 226, 68, 3, 2, 2, 2, 227, 228, 7, 126, 2, 2, 228, 229, 7, 126, 2, 2, 229, 70, 3, 2, 2, 2, 230, 231, 7, 35, 2, 2, 231, 72, 3, 2, 2, 2, 232, 234, 9, 2, 2, 2, 233, 232, 3, 2, 2, 2, 234, 235, 3, 2, 2, 2, 235, 233, 3, 2, 2, 2, 235, 236, 3, 2, 2, 2, 236, 74, 3, 2, 2, 2, 237, 238, 5, 73, 37, 2, 238, 239, 7, 48, 2, 2, 239, 240, 5, 73, 37, 2, 240, 76, 3, 2, 2, 2, 241, 242, 7, 60, 2, 2, 242, 246, 9, 3, 2, 2, 243, 245, 9, 4, 2, 2, 244, 243, 3, 2, 2, 2, 245, 248, 3, 2, 2, 2, 246, 244, 3, 2, 2, 2, 246, 247, 3, 2, 2, 2, 247, 78, 3, 2, 2, 2, 248, 246, 3, 2, 2, 2, 249, 251, 9, 5, 2, 2, 250, 249, 3, 2, 2, 2, 251, 252, 3, 2, 2, 2, 252, 250, 3, 2, 2, 2, 252, 253, 3, 2, 2, 2, 253, 80, 3, 2, 2, 2, 254, 256, 9, 6, 2, 2, 255, 254, 3, 2, 2, 2, 256, 257, 3, 2, 2, 2, 257, 255, 3, 2, 2, 2, 257, 258, 3, 2, 2, 2, 258, 259, 3, 2, 2, 2, 259, 260, 8, 41, 2, 2, 260, 82, 3, 2, 2, 2, 261, 262, 7, 49, 2, 2, 262, 263, 7, 49, 2, 2, 263, 267, 3, 2, 2, 2, 264, 266, 10, 7, 2, 2, 265, 264, 3, 2, 2, 2, 266, 269, 3, 2, 2, 2, 267, 265, 3, 2, 2, 2, 267, 268, 3, 2, 2, 2, 268, 270, 3, 2, 2, 2, 269, 267, 3, 2, 2, 2, 270, 271, 8, 42, 2, 2, 271, 84, 3, 2, 2, 2, 272, 273, 7, 49, 2, 2, 273, 274, 7, 44, 2, 2, 274, 278, 3, 2, 2, 2, 275, 277, 11, 2, 2, 2, 276, 275, 3, 2, 2, 2, 277, 280, 3, 2, 2, 2, 278, 279, 3, 2, 2, 2, 278, 276, 3, 2, 2, 2, 279, 281, 3, 2, 2, 2, 280, 278, 3, 2, 2, 2, 281, 282, 7, 44, 2, 2, 282, 283, 7, 49, 2, 2, 283, 284, 3, 2, 2, 2, 284, 285, 8, 43, 2, 2, 285, 86, 3, 2, 2, 2, 9, 2, 235, 246, 252, 257, 267, 278, 3, 8, 2, 2] \ No newline at end of file diff --git a/ChironCore/turtparse/tlangLexer.py b/ChironCore/turtparse/tlangLexer.py index fc951de..95d0321 100644 --- a/ChironCore/turtparse/tlangLexer.py +++ b/ChironCore/turtparse/tlangLexer.py @@ -5,93 +5,124 @@ 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("\u011e\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("\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(\4)\t)\4*\t*\4+\t+\3\2\3\2\3\2\3\3") + buf.write("\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") + buf.write("\6\3\6\3\7\3\7\3\7\3\7\3\7\3\7\3\7\3\7\3\b\3\b\3\b\3\b") + buf.write("\3\b\3\t\3\t\3\n\3\n\3\13\3\13\3\f\3\f\3\r\3\r\3\r\3\r") + buf.write("\3\r\3\r\3\r\3\r\3\16\3\16\3\16\3\16\3\16\3\16\3\16\3") + buf.write("\16\3\16\3\17\3\17\3\17\3\17\3\17\3\20\3\20\3\20\3\20") + buf.write("\3\20\3\20\3\21\3\21\3\21\3\21\3\21\3\21\3\22\3\22\3\22") + buf.write("\3\22\3\22\3\22\3\22\3\22\3\23\3\23\3\23\3\23\3\23\3\23") + buf.write("\3\24\3\24\3\24\3\24\3\24\3\24\3\24\3\25\3\25\3\25\3\25") + buf.write("\3\25\3\25\3\25\3\26\3\26\3\27\3\27\3\30\3\30\3\31\3\31") + buf.write("\3\32\3\32\3\33\3\33\3\33\3\33\3\33\3\33\3\33\3\33\3\33") + buf.write("\3\34\3\34\3\35\3\35\3\36\3\36\3\36\3\37\3\37\3\37\3 ") + buf.write("\3 \3 \3!\3!\3!\3\"\3\"\3\"\3#\3#\3#\3$\3$\3%\6%\u00ea") + buf.write("\n%\r%\16%\u00eb\3&\3&\3&\3&\3\'\3\'\3\'\7\'\u00f5\n\'") + buf.write("\f\'\16\'\u00f8\13\'\3(\6(\u00fb\n(\r(\16(\u00fc\3)\6") + buf.write(")\u0100\n)\r)\16)\u0101\3)\3)\3*\3*\3*\3*\7*\u010a\n*") + buf.write("\f*\16*\u010d\13*\3*\3*\3+\3+\3+\3+\7+\u0115\n+\f+\16") + buf.write("+\u0118\13+\3+\3+\3+\3+\3+\3\u0116\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("\34\67\359\36;\37= ?!A\"C#E$G%I&K\'M(O)Q*S+U,\3\2\b\3") + buf.write("\2\62;\5\2C\\aac|\5\2\62;C\\c|\4\2C\\c|\5\2\13\f\17\17") + buf.write("\"\"\4\2\f\f\17\17\2\u0123\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\2Q\3\2\2\2\2S\3\2\2\2\2U\3\2\2\2\3W\3\2\2\2\5Z") + buf.write("\3\2\2\2\7\\\3\2\2\2\t^\3\2\2\2\13c\3\2\2\2\rj\3\2\2\2") + buf.write("\17r\3\2\2\2\21w\3\2\2\2\23y\3\2\2\2\25{\3\2\2\2\27}\3") + buf.write("\2\2\2\31\177\3\2\2\2\33\u0087\3\2\2\2\35\u0090\3\2\2") + buf.write("\2\37\u0095\3\2\2\2!\u009b\3\2\2\2#\u00a1\3\2\2\2%\u00a9") + buf.write("\3\2\2\2\'\u00af\3\2\2\2)\u00b6\3\2\2\2+\u00bd\3\2\2\2") + buf.write("-\u00bf\3\2\2\2/\u00c1\3\2\2\2\61\u00c3\3\2\2\2\63\u00c5") + buf.write("\3\2\2\2\65\u00c7\3\2\2\2\67\u00d0\3\2\2\29\u00d2\3\2") + buf.write("\2\2;\u00d4\3\2\2\2=\u00d7\3\2\2\2?\u00da\3\2\2\2A\u00dd") + buf.write("\3\2\2\2C\u00e0\3\2\2\2E\u00e3\3\2\2\2G\u00e6\3\2\2\2") + buf.write("I\u00e9\3\2\2\2K\u00ed\3\2\2\2M\u00f1\3\2\2\2O\u00fa\3") + buf.write("\2\2\2Q\u00ff\3\2\2\2S\u0105\3\2\2\2U\u0110\3\2\2\2WX") + buf.write("\7k\2\2XY\7h\2\2Y\4\3\2\2\2Z[\7]\2\2[\6\3\2\2\2\\]\7_") + buf.write("\2\2]\b\3\2\2\2^_\7g\2\2_`\7n\2\2`a\7u\2\2ab\7g\2\2b\n") + buf.write("\3\2\2\2cd\7t\2\2de\7g\2\2ef\7r\2\2fg\7g\2\2gh\7c\2\2") + buf.write("hi\7v\2\2i\f\3\2\2\2jk\7B\2\2kl\7w\2\2lm\7p\2\2mn\7t\2") + buf.write("\2no\7q\2\2op\7n\2\2pq\7n\2\2q\16\3\2\2\2rs\7i\2\2st\7") + buf.write("q\2\2tu\7v\2\2uv\7q\2\2v\20\3\2\2\2wx\7*\2\2x\22\3\2\2") + buf.write("\2yz\7.\2\2z\24\3\2\2\2{|\7+\2\2|\26\3\2\2\2}~\7?\2\2") + buf.write("~\30\3\2\2\2\177\u0080\7h\2\2\u0080\u0081\7q\2\2\u0081") + buf.write("\u0082\7t\2\2\u0082\u0083\7y\2\2\u0083\u0084\7c\2\2\u0084") + buf.write("\u0085\7t\2\2\u0085\u0086\7f\2\2\u0086\32\3\2\2\2\u0087") + buf.write("\u0088\7d\2\2\u0088\u0089\7c\2\2\u0089\u008a\7e\2\2\u008a") + buf.write("\u008b\7m\2\2\u008b\u008c\7y\2\2\u008c\u008d\7c\2\2\u008d") + buf.write("\u008e\7t\2\2\u008e\u008f\7f\2\2\u008f\34\3\2\2\2\u0090") + buf.write("\u0091\7n\2\2\u0091\u0092\7g\2\2\u0092\u0093\7h\2\2\u0093") + buf.write("\u0094\7v\2\2\u0094\36\3\2\2\2\u0095\u0096\7t\2\2\u0096") + buf.write("\u0097\7k\2\2\u0097\u0098\7i\2\2\u0098\u0099\7j\2\2\u0099") + buf.write("\u009a\7v\2\2\u009a \3\2\2\2\u009b\u009c\7r\2\2\u009c") + buf.write("\u009d\7g\2\2\u009d\u009e\7p\2\2\u009e\u009f\7w\2\2\u009f") + buf.write("\u00a0\7r\2\2\u00a0\"\3\2\2\2\u00a1\u00a2\7r\2\2\u00a2") + buf.write("\u00a3\7g\2\2\u00a3\u00a4\7p\2\2\u00a4\u00a5\7f\2\2\u00a5") + buf.write("\u00a6\7q\2\2\u00a6\u00a7\7y\2\2\u00a7\u00a8\7p\2\2\u00a8") + buf.write("$\3\2\2\2\u00a9\u00aa\7r\2\2\u00aa\u00ab\7c\2\2\u00ab") + buf.write("\u00ac\7w\2\2\u00ac\u00ad\7u\2\2\u00ad\u00ae\7g\2\2\u00ae") + buf.write("&\3\2\2\2\u00af\u00b0\7c\2\2\u00b0\u00b1\7u\2\2\u00b1") + buf.write("\u00b2\7u\2\2\u00b2\u00b3\7g\2\2\u00b3\u00b4\7t\2\2\u00b4") + buf.write("\u00b5\7v\2\2\u00b5(\3\2\2\2\u00b6\u00b7\7c\2\2\u00b7") + buf.write("\u00b8\7u\2\2\u00b8\u00b9\7u\2\2\u00b9\u00ba\7w\2\2\u00ba") + buf.write("\u00bb\7o\2\2\u00bb\u00bc\7g\2\2\u00bc*\3\2\2\2\u00bd") + buf.write("\u00be\7-\2\2\u00be,\3\2\2\2\u00bf\u00c0\7/\2\2\u00c0") + buf.write(".\3\2\2\2\u00c1\u00c2\7,\2\2\u00c2\60\3\2\2\2\u00c3\u00c4") + buf.write("\7\61\2\2\u00c4\62\3\2\2\2\u00c5\u00c6\7\'\2\2\u00c6\64") + buf.write("\3\2\2\2\u00c7\u00c8\7r\2\2\u00c8\u00c9\7g\2\2\u00c9\u00ca") + buf.write("\7p\2\2\u00ca\u00cb\7f\2\2\u00cb\u00cc\7q\2\2\u00cc\u00cd") + buf.write("\7y\2\2\u00cd\u00ce\7p\2\2\u00ce\u00cf\7A\2\2\u00cf\66") + buf.write("\3\2\2\2\u00d0\u00d1\7>\2\2\u00d18\3\2\2\2\u00d2\u00d3") + buf.write("\7@\2\2\u00d3:\3\2\2\2\u00d4\u00d5\7?\2\2\u00d5\u00d6") + buf.write("\7?\2\2\u00d6<\3\2\2\2\u00d7\u00d8\7#\2\2\u00d8\u00d9") + buf.write("\7?\2\2\u00d9>\3\2\2\2\u00da\u00db\7>\2\2\u00db\u00dc") + buf.write("\7?\2\2\u00dc@\3\2\2\2\u00dd\u00de\7@\2\2\u00de\u00df") + buf.write("\7?\2\2\u00dfB\3\2\2\2\u00e0\u00e1\7(\2\2\u00e1\u00e2") + buf.write("\7(\2\2\u00e2D\3\2\2\2\u00e3\u00e4\7~\2\2\u00e4\u00e5") + buf.write("\7~\2\2\u00e5F\3\2\2\2\u00e6\u00e7\7#\2\2\u00e7H\3\2\2") + buf.write("\2\u00e8\u00ea\t\2\2\2\u00e9\u00e8\3\2\2\2\u00ea\u00eb") + buf.write("\3\2\2\2\u00eb\u00e9\3\2\2\2\u00eb\u00ec\3\2\2\2\u00ec") + buf.write("J\3\2\2\2\u00ed\u00ee\5I%\2\u00ee\u00ef\7\60\2\2\u00ef") + buf.write("\u00f0\5I%\2\u00f0L\3\2\2\2\u00f1\u00f2\7<\2\2\u00f2\u00f6") + buf.write("\t\3\2\2\u00f3\u00f5\t\4\2\2\u00f4\u00f3\3\2\2\2\u00f5") + buf.write("\u00f8\3\2\2\2\u00f6\u00f4\3\2\2\2\u00f6\u00f7\3\2\2\2") + buf.write("\u00f7N\3\2\2\2\u00f8\u00f6\3\2\2\2\u00f9\u00fb\t\5\2") + buf.write("\2\u00fa\u00f9\3\2\2\2\u00fb\u00fc\3\2\2\2\u00fc\u00fa") + buf.write("\3\2\2\2\u00fc\u00fd\3\2\2\2\u00fdP\3\2\2\2\u00fe\u0100") + buf.write("\t\6\2\2\u00ff\u00fe\3\2\2\2\u0100\u0101\3\2\2\2\u0101") + buf.write("\u00ff\3\2\2\2\u0101\u0102\3\2\2\2\u0102\u0103\3\2\2\2") + buf.write("\u0103\u0104\b)\2\2\u0104R\3\2\2\2\u0105\u0106\7\61\2") + buf.write("\2\u0106\u0107\7\61\2\2\u0107\u010b\3\2\2\2\u0108\u010a") + buf.write("\n\7\2\2\u0109\u0108\3\2\2\2\u010a\u010d\3\2\2\2\u010b") + buf.write("\u0109\3\2\2\2\u010b\u010c\3\2\2\2\u010c\u010e\3\2\2\2") + buf.write("\u010d\u010b\3\2\2\2\u010e\u010f\b*\2\2\u010fT\3\2\2\2") + buf.write("\u0110\u0111\7\61\2\2\u0111\u0112\7,\2\2\u0112\u0116\3") + buf.write("\2\2\2\u0113\u0115\13\2\2\2\u0114\u0113\3\2\2\2\u0115") + buf.write("\u0118\3\2\2\2\u0116\u0117\3\2\2\2\u0116\u0114\3\2\2\2") + buf.write("\u0117\u0119\3\2\2\2\u0118\u0116\3\2\2\2\u0119\u011a\7") + buf.write(",\2\2\u011a\u011b\7\61\2\2\u011b\u011c\3\2\2\2\u011c\u011d") + buf.write("\b+\2\2\u011dV\3\2\2\2\t\2\u00eb\u00f6\u00fc\u0101\u010b") + buf.write("\u0116\3\b\2\2") return buf.getvalue() @@ -118,46 +149,55 @@ 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 + FLOAT = 37 + VAR = 38 + NAME = 39 + Whitespace = 40 + COMMENT_LINE = 41 + COMMENT_BLOCK = 42 channelNames = [ u"DEFAULT_TOKEN_CHANNEL", u"HIDDEN" ] modeNames = [ "DEFAULT_MODE" ] literalNames = [ "", - "'if'", "'['", "']'", "'else'", "'repeat'", "'goto'", "'('", - "','", "')'", "'='", "'forward'", "'backward'", "'left'", "'right'", - "'penup'", "'pendown'", "'pause'", "'+'", "'-'", "'*'", "'/'", - "'pendown?'", "'<'", "'>'", "'=='", "'!='", "'<='", "'>='", - "'&&'", "'||'", "'!'" ] + "'if'", "'['", "']'", "'else'", "'repeat'", "'@unroll'", "'goto'", + "'('", "','", "')'", "'='", "'forward'", "'backward'", "'left'", + "'right'", "'penup'", "'pendown'", "'pause'", "'assert'", "'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", "FLOAT", + "VAR", "NAME", "Whitespace", "COMMENT_LINE", "COMMENT_BLOCK" ] 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", + "FLOAT", "VAR", "NAME", "Whitespace", "COMMENT_LINE", + "COMMENT_BLOCK" ] grammarFileName = "tlang.g4" diff --git a/ChironCore/turtparse/tlangLexer.tokens b/ChironCore/turtparse/tlangLexer.tokens index 78f9526..39f4806 100644 --- a/ChironCore/turtparse/tlangLexer.tokens +++ b/ChironCore/turtparse/tlangLexer.tokens @@ -15,52 +15,63 @@ 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 +FLOAT=37 +VAR=38 +NAME=39 +Whitespace=40 +COMMENT_LINE=41 +COMMENT_BLOCK=42 'if'=1 '['=2 ']'=3 'else'=4 'repeat'=5 -'goto'=6 -'('=7 -','=8 -')'=9 -'='=10 -'forward'=11 -'backward'=12 -'left'=13 -'right'=14 -'penup'=15 -'pendown'=16 -'pause'=17 -'+'=18 -'-'=19 -'*'=20 -'/'=21 -'pendown?'=22 -'<'=23 -'>'=24 -'=='=25 -'!='=26 -'<='=27 -'>='=28 -'&&'=29 -'||'=30 -'!'=31 +'@unroll'=6 +'goto'=7 +'('=8 +','=9 +')'=10 +'='=11 +'forward'=12 +'backward'=13 +'left'=14 +'right'=15 +'penup'=16 +'pendown'=17 +'pause'=18 +'assert'=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..fce79b5 100644 --- a/ChironCore/turtparse/tlangParser.py +++ b/ChironCore/turtparse/tlangParser.py @@ -5,71 +5,87 @@ 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("\u00cd\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\4\32\t\32\3\2\3\2\3\2\3\3\7\39\n\3\f\3\16\3<\13") + buf.write("\3\3\4\6\4?\n\4\r\4\16\4@\3\5\3\5\3\5\3\5\3\5\3\5\3\5") + buf.write("\3\5\3\5\5\5L\n\5\3\6\3\6\5\6P\n\6\3\7\3\7\3\7\3\7\3\7") + buf.write("\3\7\3\b\3\b\3\b\3\b\3\b\3\b\3\b\3\b\3\b\3\b\3\t\3\t\3") + buf.write("\t\3\t\3\t\3\t\3\t\3\t\3\t\3\t\3\t\3\t\3\t\3\t\5\tp\n") + 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("\21\3\21\3\21\3\22\3\22\3\22\3\22\3\22\3\22\3\22\3\22") + buf.write("\3\22\5\22\u0095\n\22\3\22\3\22\3\22\3\22\3\22\3\22\3") + buf.write("\22\3\22\3\22\3\22\3\22\3\22\7\22\u00a3\n\22\f\22\16\22") + buf.write("\u00a6\13\22\3\23\3\23\3\24\3\24\3\25\3\25\3\26\3\26\3") + buf.write("\27\3\27\3\27\3\27\3\27\3\27\3\27\3\27\3\27\3\27\3\27") + buf.write("\3\27\5\27\u00bc\n\27\3\27\3\27\3\27\3\27\7\27\u00c2\n") + buf.write("\27\f\27\16\27\u00c5\13\27\3\30\3\30\3\31\3\31\3\32\3") + buf.write("\32\3\32\2\4\",\33\2\4\6\b\n\f\16\20\22\24\26\30\32\34") + buf.write("\36 \"$&(*,.\60\62\2\t\3\2\16\21\3\2\22\23\3\2\31\32\3") + buf.write("\2\27\30\3\2\35\"\3\2#$\3\2&(\2\u00c8\2\64\3\2\2\2\4:") + buf.write("\3\2\2\2\6>\3\2\2\2\bK\3\2\2\2\nO\3\2\2\2\fQ\3\2\2\2\16") + buf.write("W\3\2\2\2\20o\3\2\2\2\22q\3\2\2\2\24x\3\2\2\2\26|\3\2") + buf.write("\2\2\30\177\3\2\2\2\32\u0081\3\2\2\2\34\u0083\3\2\2\2") + buf.write("\36\u0085\3\2\2\2 \u0088\3\2\2\2\"\u0094\3\2\2\2$\u00a7") + buf.write("\3\2\2\2&\u00a9\3\2\2\2(\u00ab\3\2\2\2*\u00ad\3\2\2\2") + buf.write(",\u00bb\3\2\2\2.\u00c6\3\2\2\2\60\u00c8\3\2\2\2\62\u00ca") + buf.write("\3\2\2\2\64\65\5\4\3\2\65\66\7\2\2\3\66\3\3\2\2\2\679") + buf.write("\5\b\5\28\67\3\2\2\29<\3\2\2\2:8\3\2\2\2:;\3\2\2\2;\5") + buf.write("\3\2\2\2<:\3\2\2\2=?\5\b\5\2>=\3\2\2\2?@\3\2\2\2@>\3\2") + buf.write("\2\2@A\3\2\2\2A\7\3\2\2\2BL\5\24\13\2CL\5\n\6\2DL\5\20") + buf.write("\t\2EL\5\26\f\2FL\5\32\16\2GL\5\22\n\2HL\5\34\17\2IL\5") + buf.write("\36\20\2JL\5 \21\2KB\3\2\2\2KC\3\2\2\2KD\3\2\2\2KE\3\2") + buf.write("\2\2KF\3\2\2\2KG\3\2\2\2KH\3\2\2\2KI\3\2\2\2KJ\3\2\2\2") + buf.write("L\t\3\2\2\2MP\5\f\7\2NP\5\16\b\2OM\3\2\2\2ON\3\2\2\2P") + buf.write("\13\3\2\2\2QR\7\3\2\2RS\5,\27\2ST\7\4\2\2TU\5\6\4\2UV") + buf.write("\7\5\2\2V\r\3\2\2\2WX\7\3\2\2XY\5,\27\2YZ\7\4\2\2Z[\5") + buf.write("\6\4\2[\\\7\5\2\2\\]\7\6\2\2]^\7\4\2\2^_\5\6\4\2_`\7\5") + buf.write("\2\2`\17\3\2\2\2ab\7\7\2\2bc\5\62\32\2cd\7\4\2\2de\5\6") + buf.write("\4\2ef\7\5\2\2fp\3\2\2\2gh\7\b\2\2hi\7&\2\2ij\7\7\2\2") + buf.write("jk\5\62\32\2kl\7\4\2\2lm\5\6\4\2mn\7\5\2\2np\3\2\2\2o") + buf.write("a\3\2\2\2og\3\2\2\2p\21\3\2\2\2qr\7\t\2\2rs\7\n\2\2st") + buf.write("\5\"\22\2tu\7\13\2\2uv\5\"\22\2vw\7\f\2\2w\23\3\2\2\2") + buf.write("xy\7(\2\2yz\7\r\2\2z{\5\"\22\2{\25\3\2\2\2|}\5\30\r\2") + buf.write("}~\5\"\22\2~\27\3\2\2\2\177\u0080\t\2\2\2\u0080\31\3\2") + buf.write("\2\2\u0081\u0082\t\3\2\2\u0082\33\3\2\2\2\u0083\u0084") + buf.write("\7\24\2\2\u0084\35\3\2\2\2\u0085\u0086\7\25\2\2\u0086") + buf.write("\u0087\5,\27\2\u0087\37\3\2\2\2\u0088\u0089\7\26\2\2\u0089") + buf.write("\u008a\5,\27\2\u008a!\3\2\2\2\u008b\u008c\b\22\1\2\u008c") + buf.write("\u008d\5*\26\2\u008d\u008e\5\"\22\b\u008e\u0095\3\2\2") + buf.write("\2\u008f\u0095\5\62\32\2\u0090\u0091\7\n\2\2\u0091\u0092") + buf.write("\5\"\22\2\u0092\u0093\7\f\2\2\u0093\u0095\3\2\2\2\u0094") + buf.write("\u008b\3\2\2\2\u0094\u008f\3\2\2\2\u0094\u0090\3\2\2\2") + buf.write("\u0095\u00a4\3\2\2\2\u0096\u0097\f\7\2\2\u0097\u0098\5") + buf.write("$\23\2\u0098\u0099\5\"\22\b\u0099\u00a3\3\2\2\2\u009a") + buf.write("\u009b\f\6\2\2\u009b\u009c\5&\24\2\u009c\u009d\5\"\22") + buf.write("\7\u009d\u00a3\3\2\2\2\u009e\u009f\f\5\2\2\u009f\u00a0") + buf.write("\5(\25\2\u00a0\u00a1\5\"\22\6\u00a1\u00a3\3\2\2\2\u00a2") + buf.write("\u0096\3\2\2\2\u00a2\u009a\3\2\2\2\u00a2\u009e\3\2\2\2") + buf.write("\u00a3\u00a6\3\2\2\2\u00a4\u00a2\3\2\2\2\u00a4\u00a5\3") + buf.write("\2\2\2\u00a5#\3\2\2\2\u00a6\u00a4\3\2\2\2\u00a7\u00a8") + buf.write("\t\4\2\2\u00a8%\3\2\2\2\u00a9\u00aa\t\5\2\2\u00aa\'\3") + buf.write("\2\2\2\u00ab\u00ac\7\33\2\2\u00ac)\3\2\2\2\u00ad\u00ae") + buf.write("\7\30\2\2\u00ae+\3\2\2\2\u00af\u00b0\b\27\1\2\u00b0\u00b1") + buf.write("\7%\2\2\u00b1\u00bc\5,\27\7\u00b2\u00b3\5\"\22\2\u00b3") + buf.write("\u00b4\5.\30\2\u00b4\u00b5\5\"\22\2\u00b5\u00bc\3\2\2") + buf.write("\2\u00b6\u00bc\7\34\2\2\u00b7\u00b8\7\n\2\2\u00b8\u00b9") + buf.write("\5,\27\2\u00b9\u00ba\7\f\2\2\u00ba\u00bc\3\2\2\2\u00bb") + buf.write("\u00af\3\2\2\2\u00bb\u00b2\3\2\2\2\u00bb\u00b6\3\2\2\2") + buf.write("\u00bb\u00b7\3\2\2\2\u00bc\u00c3\3\2\2\2\u00bd\u00be\f") + buf.write("\5\2\2\u00be\u00bf\5\60\31\2\u00bf\u00c0\5,\27\6\u00c0") + buf.write("\u00c2\3\2\2\2\u00c1\u00bd\3\2\2\2\u00c2\u00c5\3\2\2\2") + buf.write("\u00c3\u00c1\3\2\2\2\u00c3\u00c4\3\2\2\2\u00c4-\3\2\2") + buf.write("\2\u00c5\u00c3\3\2\2\2\u00c6\u00c7\t\6\2\2\u00c7/\3\2") + buf.write("\2\2\u00c8\u00c9\t\7\2\2\u00c9\61\3\2\2\2\u00ca\u00cb") + buf.write("\t\b\2\2\u00cb\63\3\2\2\2\f:@KOo\u0094\u00a2\u00a4\u00bb") + buf.write("\u00c3") return buf.getvalue() @@ -84,19 +100,21 @@ class tlangParser ( Parser ): sharedContextCache = PredictionContextCache() literalNames = [ "", "'if'", "'['", "']'", "'else'", "'repeat'", - "'goto'", "'('", "','", "')'", "'='", "'forward'", - "'backward'", "'left'", "'right'", "'penup'", "'pendown'", - "'pause'", "'+'", "'-'", "'*'", "'/'", "'pendown?'", - "'<'", "'>'", "'=='", "'!='", "'<='", "'>='", "'&&'", - "'||'", "'!'" ] + "'@unroll'", "'goto'", "'('", "','", "')'", "'='", + "'forward'", "'backward'", "'left'", "'right'", "'penup'", + "'pendown'", "'pause'", "'assert'", "'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", "FLOAT", "VAR", "NAME", + "Whitespace", "COMMENT_LINE", "COMMENT_BLOCK" ] RULE_start = 0 RULE_instruction_list = 1 @@ -112,21 +130,25 @@ 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_assertionCommand = 14 + RULE_assumeCommand = 15 + RULE_expression = 16 + RULE_multiplicative = 17 + RULE_additive = 18 + RULE_modulo = 19 + RULE_unaryArithOp = 20 + RULE_condition = 21 + RULE_binCondOp = 22 + RULE_logicOp = 23 + RULE_value = 24 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", "assertionCommand", "assumeCommand", + "expression", "multiplicative", "additive", "modulo", + "unaryArithOp", "condition", "binCondOp", "logicOp", + "value" ] EOF = Token.EOF T__0=1 @@ -146,24 +168,31 @@ 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 + FLOAT=37 + VAR=38 + NAME=39 + Whitespace=40 + COMMENT_LINE=41 + COMMENT_BLOCK=42 def __init__(self, input:TokenStream, output:TextIO = sys.stdout): super().__init__(input, output) @@ -173,6 +202,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 +234,9 @@ def start(self): self.enterRule(localctx, 0, self.RULE_start) try: self.enterOuterAlt(localctx, 1) - self.state = 44 + self.state = 50 self.instruction_list() - self.state = 45 + self.state = 51 self.match(tlangParser.EOF) except RecognitionException as re: localctx.exception = re @@ -216,6 +246,7 @@ def start(self): self.exitRule() return localctx + class Instruction_listContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -248,13 +279,13 @@ def instruction_list(self): self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 50 + self.state = 56 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__6) | (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 = 53 self.instruction() - self.state = 52 + self.state = 58 self._errHandler.sync(self) _la = self._input.LA(1) @@ -266,6 +297,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 +330,16 @@ def strict_ilist(self): self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 54 + self.state = 60 self._errHandler.sync(self) _la = self._input.LA(1) while True: - self.state = 53 + self.state = 59 self.instruction() - self.state = 56 + self.state = 62 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__6) | (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 +350,7 @@ def strict_ilist(self): self.exitRule() return localctx + class InstructionContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -352,6 +385,14 @@ def pauseCommand(self): return self.getTypedRuleContext(tlangParser.PauseCommandContext,0) + def assertionCommand(self): + return self.getTypedRuleContext(tlangParser.AssertionCommandContext,0) + + + def assumeCommand(self): + return self.getTypedRuleContext(tlangParser.AssumeCommandContext,0) + + def getRuleIndex(self): return tlangParser.RULE_instruction @@ -369,44 +410,54 @@ def instruction(self): localctx = tlangParser.InstructionContext(self, self._ctx, self.state) self.enterRule(localctx, 6, self.RULE_instruction) try: - self.state = 65 + self.state = 73 self._errHandler.sync(self) token = self._input.LA(1) if token in [tlangParser.VAR]: self.enterOuterAlt(localctx, 1) - self.state = 58 + self.state = 64 self.assignment() pass elif token in [tlangParser.T__0]: self.enterOuterAlt(localctx, 2) - self.state = 59 + self.state = 65 self.conditional() pass - elif token in [tlangParser.T__4]: + elif token in [tlangParser.T__4, tlangParser.T__5]: self.enterOuterAlt(localctx, 3) - self.state = 60 + self.state = 66 self.loop() pass - elif token in [tlangParser.T__10, tlangParser.T__11, tlangParser.T__12, tlangParser.T__13]: + elif token in [tlangParser.T__11, tlangParser.T__12, tlangParser.T__13, tlangParser.T__14]: self.enterOuterAlt(localctx, 4) - self.state = 61 + self.state = 67 self.moveCommand() pass - elif token in [tlangParser.T__14, tlangParser.T__15]: + elif token in [tlangParser.T__15, tlangParser.T__16]: self.enterOuterAlt(localctx, 5) - self.state = 62 + self.state = 68 self.penCommand() pass - elif token in [tlangParser.T__5]: + elif token in [tlangParser.T__6]: self.enterOuterAlt(localctx, 6) - self.state = 63 + self.state = 69 self.gotoCommand() pass - elif token in [tlangParser.T__16]: + elif token in [tlangParser.T__17]: self.enterOuterAlt(localctx, 7) - self.state = 64 + self.state = 70 self.pauseCommand() pass + elif token in [tlangParser.T__18]: + self.enterOuterAlt(localctx, 8) + self.state = 71 + self.assertionCommand() + pass + elif token in [tlangParser.T__19]: + self.enterOuterAlt(localctx, 9) + self.state = 72 + self.assumeCommand() + pass else: raise NoViableAltException(self) @@ -418,6 +469,7 @@ def instruction(self): self.exitRule() return localctx + class ConditionalContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -449,18 +501,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 = 77 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 = 75 self.ifConditional() pass elif la_ == 2: self.enterOuterAlt(localctx, 2) - self.state = 68 + self.state = 76 self.ifElseConditional() pass @@ -473,6 +525,7 @@ def conditional(self): self.exitRule() return localctx + class IfConditionalContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -505,15 +558,15 @@ def ifConditional(self): self.enterRule(localctx, 10, self.RULE_ifConditional) try: self.enterOuterAlt(localctx, 1) - self.state = 71 + self.state = 79 self.match(tlangParser.T__0) - self.state = 72 + self.state = 80 self.condition(0) - self.state = 73 + self.state = 81 self.match(tlangParser.T__1) - self.state = 74 + self.state = 82 self.strict_ilist() - self.state = 75 + self.state = 83 self.match(tlangParser.T__2) except RecognitionException as re: localctx.exception = re @@ -523,6 +576,7 @@ def ifConditional(self): self.exitRule() return localctx + class IfElseConditionalContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -558,23 +612,23 @@ def ifElseConditional(self): self.enterRule(localctx, 12, self.RULE_ifElseConditional) try: self.enterOuterAlt(localctx, 1) - self.state = 77 + self.state = 85 self.match(tlangParser.T__0) - self.state = 78 + self.state = 86 self.condition(0) - self.state = 79 + self.state = 87 self.match(tlangParser.T__1) - self.state = 80 + self.state = 88 self.strict_ilist() - self.state = 81 + self.state = 89 self.match(tlangParser.T__2) - self.state = 82 + self.state = 90 self.match(tlangParser.T__3) - self.state = 83 + self.state = 91 self.match(tlangParser.T__1) - self.state = 84 + self.state = 92 self.strict_ilist() - self.state = 85 + self.state = 93 self.match(tlangParser.T__2) except RecognitionException as re: localctx.exception = re @@ -584,6 +638,7 @@ def ifElseConditional(self): self.exitRule() return localctx + class LoopContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -598,6 +653,9 @@ def strict_ilist(self): return self.getTypedRuleContext(tlangParser.Strict_ilistContext,0) + def NUM(self): + return self.getToken(tlangParser.NUM, 0) + def getRuleIndex(self): return tlangParser.RULE_loop @@ -615,17 +673,42 @@ def loop(self): localctx = tlangParser.LoopContext(self, self._ctx, self.state) self.enterRule(localctx, 14, self.RULE_loop) try: - self.enterOuterAlt(localctx, 1) - self.state = 87 - self.match(tlangParser.T__4) - self.state = 88 - self.value() - self.state = 89 - self.match(tlangParser.T__1) - self.state = 90 - self.strict_ilist() - self.state = 91 - self.match(tlangParser.T__2) + self.state = 109 + self._errHandler.sync(self) + token = self._input.LA(1) + if token in [tlangParser.T__4]: + self.enterOuterAlt(localctx, 1) + self.state = 95 + self.match(tlangParser.T__4) + self.state = 96 + self.value() + self.state = 97 + self.match(tlangParser.T__1) + self.state = 98 + self.strict_ilist() + self.state = 99 + self.match(tlangParser.T__2) + pass + elif token in [tlangParser.T__5]: + self.enterOuterAlt(localctx, 2) + self.state = 101 + self.match(tlangParser.T__5) + self.state = 102 + self.match(tlangParser.NUM) + self.state = 103 + self.match(tlangParser.T__4) + self.state = 104 + self.value() + self.state = 105 + self.match(tlangParser.T__1) + self.state = 106 + self.strict_ilist() + self.state = 107 + self.match(tlangParser.T__2) + pass + else: + raise NoViableAltException(self) + except RecognitionException as re: localctx.exception = re self._errHandler.reportError(self, re) @@ -634,6 +717,7 @@ def loop(self): self.exitRule() return localctx + class GotoCommandContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -665,18 +749,18 @@ def gotoCommand(self): self.enterRule(localctx, 16, self.RULE_gotoCommand) try: self.enterOuterAlt(localctx, 1) - self.state = 93 - self.match(tlangParser.T__5) - self.state = 94 + self.state = 111 self.match(tlangParser.T__6) - self.state = 95 - self.expression(0) - self.state = 96 + self.state = 112 self.match(tlangParser.T__7) - self.state = 97 + self.state = 113 self.expression(0) - self.state = 98 + self.state = 114 self.match(tlangParser.T__8) + self.state = 115 + self.expression(0) + self.state = 116 + self.match(tlangParser.T__9) except RecognitionException as re: localctx.exception = re self._errHandler.reportError(self, re) @@ -685,6 +769,7 @@ def gotoCommand(self): self.exitRule() return localctx + class AssignmentContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -716,11 +801,11 @@ def assignment(self): self.enterRule(localctx, 18, self.RULE_assignment) try: self.enterOuterAlt(localctx, 1) - self.state = 100 + self.state = 118 self.match(tlangParser.VAR) - self.state = 101 - self.match(tlangParser.T__9) - self.state = 102 + self.state = 119 + self.match(tlangParser.T__10) + self.state = 120 self.expression(0) except RecognitionException as re: localctx.exception = re @@ -730,6 +815,7 @@ def assignment(self): self.exitRule() return localctx + class MoveCommandContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -762,9 +848,9 @@ def moveCommand(self): self.enterRule(localctx, 20, self.RULE_moveCommand) try: self.enterOuterAlt(localctx, 1) - self.state = 104 + self.state = 122 self.moveOp() - self.state = 105 + self.state = 123 self.expression(0) except RecognitionException as re: localctx.exception = re @@ -774,6 +860,7 @@ def moveCommand(self): self.exitRule() return localctx + class MoveOpContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -800,9 +887,9 @@ def moveOp(self): self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 107 + self.state = 125 _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)): + if not((((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << tlangParser.T__11) | (1 << tlangParser.T__12) | (1 << tlangParser.T__13) | (1 << tlangParser.T__14))) != 0)): self._errHandler.recoverInline(self) else: self._errHandler.reportMatch(self) @@ -815,6 +902,7 @@ def moveOp(self): self.exitRule() return localctx + class PenCommandContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -841,9 +929,9 @@ def penCommand(self): self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 109 + self.state = 127 _la = self._input.LA(1) - if not(_la==tlangParser.T__14 or _la==tlangParser.T__15): + if not(_la==tlangParser.T__15 or _la==tlangParser.T__16): self._errHandler.recoverInline(self) else: self._errHandler.reportMatch(self) @@ -856,6 +944,7 @@ def penCommand(self): self.exitRule() return localctx + class PauseCommandContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -881,8 +970,49 @@ def pauseCommand(self): self.enterRule(localctx, 26, self.RULE_pauseCommand) try: self.enterOuterAlt(localctx, 1) - self.state = 111 - self.match(tlangParser.T__16) + self.state = 129 + self.match(tlangParser.T__17) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class AssertionCommandContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def condition(self): + return self.getTypedRuleContext(tlangParser.ConditionContext,0) + + + def getRuleIndex(self): + return tlangParser.RULE_assertionCommand + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitAssertionCommand" ): + return visitor.visitAssertionCommand(self) + else: + return visitor.visitChildren(self) + + + + + def assertionCommand(self): + + localctx = tlangParser.AssertionCommandContext(self, self._ctx, self.state) + self.enterRule(localctx, 28, self.RULE_assertionCommand) + try: + self.enterOuterAlt(localctx, 1) + self.state = 131 + self.match(tlangParser.T__18) + self.state = 132 + self.condition(0) except RecognitionException as re: localctx.exception = re self._errHandler.reportError(self, re) @@ -891,6 +1021,48 @@ def pauseCommand(self): self.exitRule() return localctx + + class AssumeCommandContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def condition(self): + return self.getTypedRuleContext(tlangParser.ConditionContext,0) + + + def getRuleIndex(self): + return tlangParser.RULE_assumeCommand + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitAssumeCommand" ): + return visitor.visitAssumeCommand(self) + else: + return visitor.visitChildren(self) + + + + + def assumeCommand(self): + + localctx = tlangParser.AssumeCommandContext(self, self._ctx, self.state) + self.enterRule(localctx, 30, self.RULE_assumeCommand) + try: + self.enterOuterAlt(localctx, 1) + self.state = 134 + self.match(tlangParser.T__19) + self.state = 135 + self.condition(0) + 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): @@ -943,6 +1115,29 @@ def accept(self, visitor:ParseTreeVisitor): return visitor.visitChildren(self) + class ModExprContext(ExpressionContext): + + def __init__(self, parser, ctx:ParserRuleContext): # actually a tlangParser.ExpressionContext + super().__init__(parser) + self.copyFrom(ctx) + + def expression(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(tlangParser.ExpressionContext) + else: + return self.getTypedRuleContext(tlangParser.ExpressionContext,i) + + def modulo(self): + return self.getTypedRuleContext(tlangParser.ModuloContext,0) + + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitModExpr" ): + return visitor.visitModExpr(self) + else: + return visitor.visitChildren(self) + + class AddExprContext(ExpressionContext): def __init__(self, parser, ctx:ParserRuleContext): # actually a tlangParser.ExpressionContext @@ -1012,11 +1207,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 = 146 self._errHandler.sync(self) token = self._input.LA(1) if token in [tlangParser.MINUS]: @@ -1024,74 +1219,87 @@ def expression(self, _p:int=0): self._ctx = localctx _prevctx = localctx - self.state = 114 + self.state = 138 self.unaryArithOp() - self.state = 115 - self.expression(5) + self.state = 139 + self.expression(6) pass - elif token in [tlangParser.NUM, tlangParser.VAR]: + elif token in [tlangParser.NUM, tlangParser.FLOAT, tlangParser.VAR]: localctx = tlangParser.ValueExprContext(self, localctx) self._ctx = localctx _prevctx = localctx - self.state = 117 + self.state = 141 self.value() pass - elif token in [tlangParser.T__6]: + elif token in [tlangParser.T__7]: localctx = tlangParser.ParenExprContext(self, localctx) self._ctx = localctx _prevctx = localctx - self.state = 118 - self.match(tlangParser.T__6) - self.state = 119 + self.state = 142 + self.match(tlangParser.T__7) + self.state = 143 self.expression(0) - self.state = 120 - self.match(tlangParser.T__8) + self.state = 144 + self.match(tlangParser.T__9) pass else: raise NoViableAltException(self) self._ctx.stop = self._input.LT(-1) - self.state = 134 + self.state = 162 self._errHandler.sync(self) - _alt = self._interp.adaptivePredict(self._input,6,self._ctx) + _alt = self._interp.adaptivePredict(self._input,7,self._ctx) while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER: if _alt==1: if self._parseListeners is not None: self.triggerExitRuleEvent() _prevctx = localctx - self.state = 132 + self.state = 160 self._errHandler.sync(self) - la_ = self._interp.adaptivePredict(self._input,5,self._ctx) + la_ = self._interp.adaptivePredict(self._input,6,self._ctx) if la_ == 1: localctx = tlangParser.MulExprContext(self, tlangParser.ExpressionContext(self, _parentctx, _parentState)) self.pushNewRecursionContext(localctx, _startState, self.RULE_expression) - self.state = 124 - if not self.precpred(self._ctx, 4): + self.state = 148 + if not self.precpred(self._ctx, 5): from antlr4.error.Errors import FailedPredicateException - raise FailedPredicateException(self, "self.precpred(self._ctx, 4)") - self.state = 125 + raise FailedPredicateException(self, "self.precpred(self._ctx, 5)") + self.state = 149 self.multiplicative() - self.state = 126 - self.expression(5) + self.state = 150 + self.expression(6) 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 = 152 + if not self.precpred(self._ctx, 4): + from antlr4.error.Errors import FailedPredicateException + raise FailedPredicateException(self, "self.precpred(self._ctx, 4)") + self.state = 153 + self.additive() + self.state = 154 + self.expression(5) + pass + + elif la_ == 3: + localctx = tlangParser.ModExprContext(self, tlangParser.ExpressionContext(self, _parentctx, _parentState)) + self.pushNewRecursionContext(localctx, _startState, self.RULE_expression) + self.state = 156 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.additive() - self.state = 130 + self.state = 157 + self.modulo() + self.state = 158 self.expression(4) pass - self.state = 136 + self.state = 164 self._errHandler.sync(self) - _alt = self._interp.adaptivePredict(self._input,6,self._ctx) + _alt = self._interp.adaptivePredict(self._input,7,self._ctx) except RecognitionException as re: localctx.exception = re @@ -1101,6 +1309,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): @@ -1128,11 +1337,11 @@ 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 = 165 _la = self._input.LA(1) if not(_la==tlangParser.MUL or _la==tlangParser.DIV): self._errHandler.recoverInline(self) @@ -1147,6 +1356,7 @@ def multiplicative(self): self.exitRule() return localctx + class AdditiveContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -1174,11 +1384,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 = 167 _la = self._input.LA(1) if not(_la==tlangParser.PLUS or _la==tlangParser.MINUS): self._errHandler.recoverInline(self) @@ -1193,6 +1403,45 @@ def additive(self): self.exitRule() return localctx + + class ModuloContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def MOD(self): + return self.getToken(tlangParser.MOD, 0) + + def getRuleIndex(self): + return tlangParser.RULE_modulo + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitModulo" ): + return visitor.visitModulo(self) + else: + return visitor.visitChildren(self) + + + + + def modulo(self): + + localctx = tlangParser.ModuloContext(self, self._ctx, self.state) + self.enterRule(localctx, 38, self.RULE_modulo) + try: + self.enterOuterAlt(localctx, 1) + self.state = 169 + self.match(tlangParser.MOD) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + class UnaryArithOpContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -1217,10 +1466,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, 40, self.RULE_unaryArithOp) try: self.enterOuterAlt(localctx, 1) - self.state = 141 + self.state = 171 self.match(tlangParser.MINUS) except RecognitionException as re: localctx.exception = re @@ -1230,6 +1479,7 @@ def unaryArithOp(self): self.exitRule() return localctx + class ConditionContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -1280,48 +1530,48 @@ 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 = 42 + self.enterRecursionRule(localctx, 42, self.RULE_condition, _p) try: self.enterOuterAlt(localctx, 1) - self.state = 155 + self.state = 185 self._errHandler.sync(self) - la_ = self._interp.adaptivePredict(self._input,7,self._ctx) + la_ = self._interp.adaptivePredict(self._input,8,self._ctx) if la_ == 1: - self.state = 144 + self.state = 174 self.match(tlangParser.NOT) - self.state = 145 + self.state = 175 self.condition(5) pass elif la_ == 2: - self.state = 146 + self.state = 176 self.expression(0) - self.state = 147 + self.state = 177 self.binCondOp() - self.state = 148 + self.state = 178 self.expression(0) pass elif la_ == 3: - self.state = 150 + self.state = 180 self.match(tlangParser.PENCOND) pass elif la_ == 4: - self.state = 151 - self.match(tlangParser.T__6) - self.state = 152 + self.state = 181 + self.match(tlangParser.T__7) + self.state = 182 self.condition(0) - self.state = 153 - self.match(tlangParser.T__8) + self.state = 183 + self.match(tlangParser.T__9) pass self._ctx.stop = self._input.LT(-1) - self.state = 163 + self.state = 193 self._errHandler.sync(self) - _alt = self._interp.adaptivePredict(self._input,8,self._ctx) + _alt = self._interp.adaptivePredict(self._input,9,self._ctx) while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER: if _alt==1: if self._parseListeners is not None: @@ -1329,17 +1579,17 @@ 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 = 187 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 = 188 self.logicOp() - self.state = 159 + self.state = 189 self.condition(4) - self.state = 165 + self.state = 195 self._errHandler.sync(self) - _alt = self._interp.adaptivePredict(self._input,8,self._ctx) + _alt = self._interp.adaptivePredict(self._input,9,self._ctx) except RecognitionException as re: localctx.exception = re @@ -1349,6 +1599,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 +1639,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, 44, self.RULE_binCondOp) self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 166 + self.state = 196 _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 +1658,7 @@ def binCondOp(self): self.exitRule() return localctx + class LogicOpContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -1434,11 +1686,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, 46, self.RULE_logicOp) self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 168 + self.state = 198 _la = self._input.LA(1) if not(_la==tlangParser.AND or _la==tlangParser.OR): self._errHandler.recoverInline(self) @@ -1453,6 +1705,7 @@ def logicOp(self): self.exitRule() return localctx + class ValueContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -1465,6 +1718,9 @@ def NUM(self): def VAR(self): return self.getToken(tlangParser.VAR, 0) + def FLOAT(self): + return self.getToken(tlangParser.FLOAT, 0) + def getRuleIndex(self): return tlangParser.RULE_value @@ -1480,13 +1736,13 @@ 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, 48, self.RULE_value) self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 170 + self.state = 200 _la = self._input.LA(1) - if not(_la==tlangParser.NUM or _la==tlangParser.VAR): + if not((((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << tlangParser.NUM) | (1 << tlangParser.FLOAT) | (1 << tlangParser.VAR))) != 0)): self._errHandler.recoverInline(self) else: self._errHandler.reportMatch(self) @@ -1504,8 +1760,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[21] = self.condition_sempred pred = self._predicates.get(ruleIndex, None) if pred is None: raise Exception("No predicate with index:" + str(ruleIndex)) @@ -1514,15 +1770,19 @@ def sempred(self, localctx:RuleContext, ruleIndex:int, predIndex:int): def expression_sempred(self, localctx:ExpressionContext, predIndex:int): if predIndex == 0: - return self.precpred(self._ctx, 4) + return self.precpred(self._ctx, 5) if predIndex == 1: + return self.precpred(self._ctx, 4) + + + if predIndex == 2: return self.precpred(self._ctx, 3) def condition_sempred(self, localctx:ConditionContext, predIndex:int): - if predIndex == 2: + if predIndex == 3: return self.precpred(self._ctx, 3) diff --git a/ChironCore/turtparse/tlangVisitor.py b/ChironCore/turtparse/tlangVisitor.py index 7ac289a..8305cdf 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#assertionCommand. + def visitAssertionCommand(self, ctx:tlangParser.AssertionCommandContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by tlangParser#assumeCommand. + def visitAssumeCommand(self, ctx:tlangParser.AssumeCommandContext): + return self.visitChildren(ctx) + + # Visit a parse tree produced by tlangParser#unaryExpr. def visitUnaryExpr(self, ctx:tlangParser.UnaryExprContext): return self.visitChildren(ctx) @@ -89,6 +99,11 @@ def visitValueExpr(self, ctx:tlangParser.ValueExprContext): return self.visitChildren(ctx) + # Visit a parse tree produced by tlangParser#modExpr. + def visitModExpr(self, ctx:tlangParser.ModExprContext): + return self.visitChildren(ctx) + + # Visit a parse tree produced by tlangParser#addExpr. def visitAddExpr(self, ctx:tlangParser.AddExprContext): return self.visitChildren(ctx) @@ -114,6 +129,11 @@ def visitAdditive(self, ctx:tlangParser.AdditiveContext): return self.visitChildren(ctx) + # Visit a parse tree produced by tlangParser#modulo. + def visitModulo(self, ctx:tlangParser.ModuloContext): + return self.visitChildren(ctx) + + # Visit a parse tree produced by tlangParser#unaryArithOp. def visitUnaryArithOp(self, ctx:tlangParser.UnaryArithOpContext): return self.visitChildren(ctx) diff --git a/ChironCore/unroll.py b/ChironCore/unroll.py new file mode 100644 index 0000000..a413156 --- /dev/null +++ b/ChironCore/unroll.py @@ -0,0 +1,110 @@ +#!/usr/bin/python3 +# -*- coding: utf-8 -*- +# ChironLang Abstract Syntax Tree Builder +from turtparse.tlangParser import tlangParser +from turtparse.tlangVisitor import tlangVisitor + +class UnrollLoops(tlangVisitor): + def __init__(self, bound): + self.bound = bound + self.repeatVariablesCounter = 0 + + def visitStart(self, ctx:tlangParser.StartContext): + stmtList = self.visit(ctx.instruction_list()) + return stmtList + + def visitInstruction_list(self, ctx:tlangParser.Instruction_listContext): + code = "" + for instr in ctx.instruction(): + code += self.visit(instr) + "\n" + + return code + + def visitStrict_ilist(self, ctx:tlangParser.Strict_ilistContext): + code = "" + for instr in ctx.instruction(): + code += self.visit(instr) + "\n" + + return code + + + def visitAssignment(self, ctx:tlangParser.AssignmentContext): + return ctx.getText() + + def visitIfConditional(self, ctx:tlangParser.IfConditionalContext): + condition = self.visit(ctx.condition()) + ifBlock = self.visit(ctx.strict_ilist()) + return "if (" + condition + ") [\n" + ifBlock + "\n]" + + def visitIfElseConditional(self, ctx:tlangParser.IfElseConditionalContext): + condition = self.visit(ctx.condition()) + ifBlock = self.visit(ctx.strict_ilist(0)) + elseBlock = self.visit(ctx.strict_ilist(1)) + return "if (" + condition + ") [\n" + ifBlock + "\n] else [\n" + elseBlock + "\n]" + + def visitGotoCommand(self, ctx:tlangParser.GotoCommandContext): + xcor = self.visit(ctx.expression(0)) + ycor = self.visit(ctx.expression(1)) + return "goto (" + xcor + ", " + ycor + ")" + + # Visit a parse tree produced by tlangParser#unaryExpr. + def visitUnaryExpr(self, ctx:tlangParser.UnaryExprContext): + return ctx.getText() + + # Visit a parse tree produced by tlangParser#addExpr. + def visitAddExpr(self, ctx:tlangParser.AddExprContext): + return ctx.getText() + + # Visit a parse tree produced by tlangParser#mulExpr. + def visitMulExpr(self, ctx:tlangParser.MulExprContext): + return ctx.getText() + + # Visit a parse tree produced by tlangParser#valueExpr. + def visitModExpr(self, ctx:tlangParser.ModExprContext): + return ctx.getText() + + # Visit a parse tree produced by tlangParser#parenExpr. + def visitParenExpr(self, ctx:tlangParser.ParenExprContext): + return ctx.getText() + + def visitCondition(self, ctx:tlangParser.ConditionContext): + return ctx.getText() + + def visitValue(self, ctx:tlangParser.ValueContext): + return ctx.getText() + + def visitLoop(self, ctx:tlangParser.LoopContext): + unrollCount = self.bound + if ctx.NUM() is not None: + unrollCount = int(ctx.NUM().getText()) + repeatCount = self.visit(ctx.value()) + loopBlock = self.visit(ctx.strict_ilist()) + code = "" + if (repeatCount[0] != ":"): + # constant number of iterations + code += "assume " + str(repeatCount) + " <= " + str(unrollCount) +"\n" + for i in range(min(int(repeatCount), unrollCount)): + code += loopBlock + "\n" + else: + # variable number of iterations + repeatVariable = ":_repeat" + str(self.repeatVariablesCounter) + code += repeatVariable + " = " + repeatCount + "\n" + code += "assume " + repeatVariable + " <= " + str(unrollCount) +" \n" + for i in range(unrollCount): + code += "if (" + repeatVariable + " > " + str(i) + ") [\n" + loopBlock + "\n]\n" + self.repeatVariablesCounter += 1 + + return code + + def visitMoveCommand(self, ctx:tlangParser.MoveCommandContext): + return ctx.getText() + + def visitPenCommand(self, ctx:tlangParser.PenCommandContext): + return ctx.getText() + + def visitAssertionCommand(self, ctx:tlangParser.AssertionCommandContext): + return ctx.getText() + + def visitAssumeCommand(self, ctx:tlangParser.AssumeCommandContext): + return ctx.getText() + diff --git a/ChironCore/unrolled_code.tl b/ChironCore/unrolled_code.tl new file mode 100644 index 0000000..ae4bd6f --- /dev/null +++ b/ChironCore/unrolled_code.tl @@ -0,0 +1,150 @@ +assume:s1==0||:s1==1||:s1==2||:s1==3||:s1==4 +assume:s2==0||:s2==1||:s2==2||:s2==3||:s2==4 +assume:s3==0||:s3==1||:s3==2||:s3==3||:s3==4 +assume:s4==0||:s4==1||:s4==2||:s4==3||:s4==4 +assume:s5==0||:s5==1||:s5==2||:s5==3||:s5==4 +assume!(:s4==0)||(:s5==0) +assume!(:s3==0)||(:s5==0&&:s4==0) +assume!(:s2==0)||(:s5==0&&:s4==0&&:s3==0) +assume!(:s1==0)||(:s5==0&&:s4==0&&:s3==0&&:s2==0) +:step=50 +:length=0 +:targetX=3*:step +:targetY=0*:step +:obs1x=1*:step +:obs1y=1*:step +:obs2x=0*:step +:obs2y=1*:step +assume!(:turtleX==:obs1x&&:turtleY==:obs1y) +assume!(:turtleX==:obs2x&&:turtleY==:obs2y) +if ((:s1==1)) [ +forward:step + +] +if ((:s1==2)) [ +left90 +forward:step +right90 + +] +if ((:s1==3)) [ +backward:step + +] +if ((:s1==4)) [ +left90 +backward:step +right90 + +] +if ((:s1!=0)) [ +:length=:length+1 + +] +assume!(:turtleX==:obs1x&&:turtleY==:obs1y) +assume!(:turtleX==:obs2x&&:turtleY==:obs2y) +if ((:s2==1)) [ +forward:step + +] +if ((:s2==2)) [ +left90 +forward:step +right90 + +] +if ((:s2==3)) [ +backward:step + +] +if ((:s2==4)) [ +left90 +backward:step +right90 + +] +if ((:s2!=0)) [ +:length=:length+1 + +] +assume!(:turtleX==:obs1x&&:turtleY==:obs1y) +assume!(:turtleX==:obs2x&&:turtleY==:obs2y) +if ((:s3==1)) [ +forward:step + +] +if ((:s3==2)) [ +left90 +forward:step +right90 + +] +if ((:s3==3)) [ +backward:step + +] +if ((:s3==4)) [ +left90 +backward:step +right90 + +] +if ((:s3!=0)) [ +:length=:length+1 + +] +assume!(:turtleX==:obs1x&&:turtleY==:obs1y) +assume!(:turtleX==:obs2x&&:turtleY==:obs2y) +if ((:s4==1)) [ +forward:step + +] +if ((:s4==2)) [ +left90 +forward:step +right90 + +] +if ((:s4==3)) [ +backward:step + +] +if ((:s4==4)) [ +left90 +backward:step +right90 + +] +if ((:s4!=0)) [ +:length=:length+1 + +] +assume!(:turtleX==:obs1x&&:turtleY==:obs1y) +assume!(:turtleX==:obs2x&&:turtleY==:obs2y) +if ((:s5==1)) [ +forward:step + +] +if ((:s5==2)) [ +left90 +forward:step +right90 + +] +if ((:s5==3)) [ +backward:step + +] +if ((:s5==4)) [ +left90 +backward:step +right90 + +] +if ((:s5!=0)) [ +:length=:length+1 + +] +assume!(:turtleX==:obs1x&&:turtleY==:obs1y) +assume!(:turtleX==:obs2x&&:turtleY==:obs2y) +assert!(:turtleX==:targetX&&:turtleY==:targetY&&:length<=2) diff --git a/README.md b/README.md index 74ca21d..95a5c61 100644 --- a/README.md +++ b/README.md @@ -41,8 +41,8 @@ If you want to cite this work, you may use this. ### Installing Dependencies ```bash -$ pip install antlr4-python3-runtime==4.7.2 networkx z3-solver numpy -$ sudo apt-get install python3-tk +pip install antlr4-python3-runtime==4.7.2 networkx z3-solver numpy pygraphviz +sudo apt-get install python3-tk ``` ### Generating the ANTLR files. @@ -51,8 +51,8 @@ The `antlr` files need to be rebuilt if any changes are made to the `tlang.g4` f We use a visitor pattern to generate the AST from parsing. ``` -$ cd ChironCore/turtparse -$ java -cp ../extlib/antlr-4.7.2-complete.jar org.antlr.v4.Tool \ +cd ChironCore/turtparse +java -cp ../extlib/antlr-4.7.2-complete.jar org.antlr.v4.Tool \ -Dlanguage=Python3 -visitor -no-listener tlang.g4 ``` @@ -62,8 +62,8 @@ The main directory for source files is `ChironCore`. We have examples of the tur To pass parameters (input params) for running a turtle program, use the `-d` flag. Pass the parameters as a python dictionary. ```bash -$ cd ChironCore -$ ./chiron.py -r ./example/example1.tl -d '{":x": 20, "y": 30, ":z": 20, ":p": 40}' +cd ChironCore +./chiron.py -r ./example/example1.tl -d '{":x": 20, "y": 30, ":z": 20, ":p": 40}' ``` ### See help for other command line options @@ -84,7 +84,7 @@ Chiron v1.0.1 ------------ usage: chiron.py [-h] [-p] [-r] [-gr] [-b] [-z] [-t TIMEOUT] [-d PARAMS] [-c CONSTPARAMS] [-se] [-ai] [-dfa] [-sbfl] [-bg BUGGY] [-vars INPUTVARSLIST] [-nt NTESTS] [-pop POPSIZE] [-cp CXPB] [-mp MUTPB] [-ng NGEN] - [-vb VERBOSE] + [-vb VERBOSE] [-bmc] [-ub UNROLL_BOUND] [-aconf ANGLE_CONF] progfl Program Analysis Framework for ChironLang Programs. @@ -131,5 +131,10 @@ options: number of times Genetic Algorithm iterates -vb VERBOSE, --verbose VERBOSE To display computation to Console + -bmc, --bmc Run Bounded Model Checking on a Chiron Program + -ub UNROLL_BOUND, --unroll-bound UNROLL_BOUND + Unroll bound for the BMC engine. Default is 10 + -aconf ANGLE_CONF, --angle-conf ANGLE_CONF + Angle configuration file for BMC ```