abstract interpreter following lecture 16 of http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www/

signs.py

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)

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