Created
September 29, 2022 14:41
-
-
Save bazzargh/c4c7ed95e6824c06864d6798df1d257d to your computer and use it in GitHub Desktop.
abstract interpreter following lecture 16 of http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www/
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import ast | |
| import math | |
| import enum | |
| # implement the abstract interpreter used in lecture 16 of http://web.mit.edu/16.399/www/ | |
| # abstraction of sets of machine integers by initialization and simple sign | |
| class Value(enum.Enum): | |
| BOT = 0 | |
| NEG = 1 | |
| ZERO = 2 | |
| POS = 3 | |
| INI = 4 | |
| ERR = 5 | |
| TOP = 6 | |
| def opAdd(a, b): | |
| tbl = [[ Value.BOT, Value.BOT, Value.BOT , Value.BOT, Value.BOT, Value.BOT, Value.BOT ], | |
| [ Value.BOT, Value.NEG, Value.NEG , Value.INI, Value.INI, Value.ERR, Value.TOP ], | |
| [ Value.BOT, Value.NEG, Value.ZERO, Value.POS, Value.INI, Value.ERR, Value.TOP ], | |
| [ Value.BOT, Value.INI, Value.POS , Value.POS, Value.INI, Value.ERR, Value.TOP ], | |
| [ Value.BOT, Value.INI, Value.INI , Value.INI, Value.INI, Value.ERR, Value.TOP ], | |
| [ Value.ERR, Value.ERR, Value.ERR , Value.ERR, Value.ERR, Value.ERR, Value.ERR ], | |
| [ Value.ERR, Value.TOP, Value.TOP , Value.TOP, Value.TOP, Value.ERR, Value.TOP ]] | |
| return tbl[a.value][b.value] | |
| def opSub(a, b): | |
| tbl = [[ Value.BOT, Value.BOT, Value.BOT , Value.BOT, Value.BOT, Value.BOT, Value.BOT ], | |
| [ Value.BOT, Value.INI, Value.NEG , Value.NEG, Value.INI, Value.ERR, Value.TOP ], | |
| [ Value.BOT, Value.POS, Value.ZERO, Value.NEG, Value.INI, Value.ERR, Value.TOP ], | |
| [ Value.BOT, Value.POS, Value.POS , Value.INI, Value.INI, Value.ERR, Value.TOP ], | |
| [ Value.BOT, Value.INI, Value.INI , Value.INI, Value.INI, Value.ERR, Value.TOP ], | |
| [ Value.ERR, Value.ERR, Value.ERR , Value.ERR, Value.ERR, Value.ERR, Value.ERR ], | |
| [ Value.ERR, Value.TOP, Value.TOP , Value.TOP, Value.TOP, Value.ERR, Value.TOP ]] | |
| return tbl[a.value][b.value] | |
| def opMult(a, b): | |
| tbl = [[ Value.BOT, Value.BOT, Value.BOT , Value.BOT, Value.BOT, Value.BOT, Value.BOT ], | |
| [ Value.BOT, Value.POS, Value.ZERO, Value.NEG, Value.INI, Value.ERR, Value.TOP ], | |
| [ Value.BOT, Value.ZERO, Value.ZERO, Value.ZERO, Value.ZERO, Value.ERR, Value.TOP ], | |
| [ Value.BOT, Value.NEG, Value.ZERO, Value.POS, Value.INI, Value.ERR, Value.TOP ], | |
| [ Value.BOT, Value.INI, Value.ZERO, Value.INI, Value.INI, Value.ERR, Value.TOP ], | |
| [ Value.ERR, Value.ERR, Value.ERR , Value.ERR, Value.ERR, Value.ERR, Value.ERR ], | |
| [ Value.ERR, Value.TOP, Value.TOP , Value.TOP, Value.TOP, Value.ERR, Value.TOP ]] | |
| return tbl[a.value][b.value] | |
| def opDiv(a, b): | |
| tbl = [[ Value.BOT, Value.BOT, Value.BOT, Value.BOT, Value.BOT, Value.BOT, Value.BOT ], | |
| [ Value.BOT, Value.BOT, Value.BOT, Value.BOT, Value.BOT, Value.BOT, Value.BOT ], | |
| [ Value.BOT, Value.BOT, Value.BOT, Value.ZERO, Value.POS, Value.ERR, Value.TOP ], | |
| [ Value.BOT, Value.BOT, Value.BOT, Value.INI, Value.INI, Value.ERR, Value.TOP ], | |
| [ Value.BOT, Value.BOT, Value.BOT, Value.INI, Value.INI, Value.ERR, Value.TOP ], | |
| [ Value.ERR, Value.ERR, Value.ERR, Value.ERR, Value.ERR, Value.ERR, Value.ERR ], | |
| [ Value.ERR, Value.ERR, Value.ERR, Value.TOP, Value.TOP, Value.ERR, Value.TOP ]] | |
| return tbl[a.value][b.value] | |
| def opMod(a, b): | |
| tbl = [[ Value.BOT, Value.BOT, Value.BOT, Value.BOT , Value.BOT , Value.BOT, Value.BOT ], | |
| [ Value.BOT, Value.BOT, Value.BOT, Value.BOT , Value.BOT , Value.BOT, Value.BOT ], | |
| [ Value.BOT, Value.BOT, Value.BOT, Value.ZERO, Value.ZERO, Value.ERR, Value.TOP ], | |
| [ Value.BOT, Value.BOT, Value.BOT, Value.INI , Value.INI , Value.ERR, Value.TOP ], | |
| [ Value.BOT, Value.BOT, Value.BOT, Value.INI , Value.INI , Value.ERR, Value.TOP ], | |
| [ Value.ERR, Value.ERR, Value.ERR, Value.ERR , Value.ERR , Value.ERR, Value.ERR ], | |
| [ Value.ERR, Value.ERR, Value.ERR, Value.TOP , Value.TOP , Value.ERR, Value.TOP ]] | |
| return tbl[a.value][b.value] | |
| def opEq(a, b): | |
| tbl = [[ False, False, False, False, False, False, False ], | |
| [ False, True , False, False, True , False, True ], | |
| [ False, False, True , False, True , False, True ], | |
| [ False, False, False, True , True , False, True ], | |
| [ False, True , True , True , True , False, True ], | |
| [ False, False, False, False, False, False, False ], | |
| [ False, True , True , True , True , False, True ]] | |
| return tbl[a.value][b.value] | |
| def opNotEq(a, b): | |
| return not a.opEq(b) | |
| def opLt(a, b): | |
| tbl = [[ False, False, False, False, False, False, False ], | |
| [ False, True , True , True , True , False, True ], | |
| [ False, False, True , True , True , False, True ], | |
| [ False, False, False, True , True , False, True ], | |
| [ False, True , True , True , True , False, True ], | |
| [ False, False, False, False, False, False, False ], | |
| [ False, True , True , True , True , False, True ]] | |
| return tbl[a.value][b.value] | |
| def opLtE(a, b): | |
| tbl = [[ True, True, True, True, True, True, True ], | |
| [ False, True, False, False, True, False, True ], | |
| [ False, False, True, False, True, False, True ], | |
| [ False, False, False, True, True, False, True ], | |
| [ False, False, False, False, True, False, True ], | |
| [ False, False, False, False, False, True, True ], | |
| [ False, False, False, False, False, False, True ]] | |
| return tbl[a.value][b.value] | |
| def opGt(a, b): | |
| return b.opLt(a) | |
| def opGtE(a, b): | |
| return b.opLtE(a) | |
| def opUAdd(a, *b): | |
| return a | |
| def opUSub(a, *b): | |
| return [Value.BOT, Value.POS, Value.ZERO, Value.NEG, Value.INI, Value.ERR, Value.TOP][a.value] | |
| # implementation of a language similar to SIL from | |
| # http://web.mit.edu/16.399/www/lecture_05-op-sem/Cousot_MIT_2005_Course_05_4-1.pdf | |
| # but with a pythonesque syntax. | |
| class AbstractInterpreter(ast.NodeVisitor): | |
| MAXINT = 9 | |
| def __init__(self): | |
| self.env = {} | |
| def __repr__(self): | |
| return str(self.env) | |
| def visit_Constant(self, node): | |
| if not isinstance(node.value, int): | |
| return Value.ERR | |
| elif node.value == 0: | |
| return Value.ZERO | |
| elif -AbstractInterpreter.MAXINT - 1 <= node.value and node.value < 0: | |
| return Value.NEG | |
| elif 0 < node.value and node.value <= AbstractInterpreter.MAXINT: | |
| return Value.POS | |
| else: | |
| return Value.BOT | |
| def op(self, op, a, *b): | |
| opname = f'op{type(op).__name__}' | |
| # handle boolean operations directly | |
| match opname: | |
| case "opNot": | |
| return not self.visit(a) | |
| case "opAnd": | |
| return self.visit(a) and all([self.visit(c) for c in b]) | |
| case "opOr": | |
| return self.visit(a) or any([self.visit(c) for c in b]) | |
| case _: | |
| return getattr(self.visit(a), opname)(*[self.visit(c) for c in b]) | |
| def visit_UnaryOp(self, node): | |
| return self.op(node.op, node.operand) | |
| def visit_BinOp(self, node): | |
| return self.op(node.op, node.left, node.right) | |
| def visit_BoolOp(self, node): | |
| return self.op(node.op, node.values[0], *node.values[1:]) | |
| def visit_Module(self, node): | |
| for expr in node.body: | |
| self.visit(expr) | |
| print(f'{expr.lineno}: {ast.unparse(node)} => {self.env}') | |
| def visit_If(self, node): | |
| body = node.body if self.visit(node.test) else node.orelse | |
| for expr in body: | |
| self.visit(expr) | |
| print(f'{expr.lineno}: {ast.unparse(node)} => {self.env}') | |
| def visit_While(self, node): | |
| while self.visit(node.test): | |
| for expr in node.body: | |
| self.visit(expr) | |
| print(f'{expr.lineno}: {ast.unparse(node)} => {self.env}') | |
| def visit_Compare(self, node): | |
| return self.op(node.ops[0], node.left, node.comparators[0]) | |
| def visit_Assign(self, node): | |
| self.env[node.targets[0].id] = self.visit(node.value) | |
| def visit_Name(self, node): | |
| return Value.INI if node.id == "random" else self.env[node.id] | |
| examples = [ | |
| # example 00 | |
| "pass", | |
| # example 01 | |
| """ | |
| x = 1 | |
| while (x < 100): | |
| x = x + 1 | |
| """, | |
| # example 02 | |
| """ | |
| x = (-1073741823 - 1) | |
| y = (x - 1) | |
| """, | |
| # example 03 | |
| """ | |
| x = 0 | |
| y = 1 | |
| """, | |
| # example 04 | |
| """ | |
| if True: | |
| x = 1 | |
| else: | |
| x = 0 | |
| """, | |
| # example 05 | |
| """ | |
| if False: | |
| x = 1 | |
| else: | |
| x = 0 | |
| """, | |
| # example 06 | |
| """ | |
| x = -1073741824 | |
| """, | |
| # example 07 | |
| """ | |
| x = 1 | |
| while ((x < 10) or (x == 10)): | |
| x = x + 1 | |
| """, | |
| # example 08 | |
| """ | |
| x = 1073741823 | |
| """, | |
| # example 09 | |
| """ | |
| x = (-536870912 * 2) | |
| y = (536870912 * 2) | |
| z = ((-1073741823 - 1) * 1) | |
| t = ((-1073741823 - 1) * 1073741823) | |
| """, | |
| # example 10 | |
| """ | |
| x = random | |
| if (x < (-1073741823 - 1)): | |
| x = 1 | |
| else: | |
| x = 0 | |
| """, | |
| # example 11 | |
| """ | |
| x = 1; | |
| while (0 < 1073741824): | |
| x = (x + 1) | |
| """, | |
| ] | |
| print("EXAMPLES") | |
| for i in [0, 1, 2, 3, 4, 5, 7]: | |
| print(f'Example {i}') | |
| interpreter = AbstractInterpreter() | |
| tree = ast.parse(examples[i]) | |
| #print(ast.dump(tree)) | |
| interpreter.visit(tree) | |
| print(interpreter) | |
| print("\nERRORS") | |
| for i in [6,8,9,10,11]: | |
| print(f'Example {i}') | |
| interpreter = AbstractInterpreter() | |
| tree = ast.parse(examples[i]) | |
| #print(ast.dump(tree)) | |
| interpreter.visit(tree) | |
| print(interpreter) | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
the above is completely wrong! I've read through the course notes some more and understand it a bit better now. Working on a fix. The simple stuff is fine, but the implementations of 'if' and 'while' in particular should join the possible results, which means that a single 'environment' for variables isn't right - in the Ocaml implementation an environment is passed in to each step, but to do that with the python visitor infrastructure means multiple visitors or a stack. The code above is also missing the join/meet implementations. Anyway... fixing