spike on an abstract interpreter for a simple python subset using multiinterval arithmetic

binop.py

import ast
import math

class Interval:
  def __init__(self, value1, value2 = None):
    self.low = value1
    self.high = value1 if value2 is None else value2

  def __repr__(self):
    return f"[{self.low}, {self.high}]"

  def __add__(self, other):
    return Interval(self.low + other.low, self.high + other.high)

  def __sub__(self, other):
    return Interval(self.low - other.high, self.high - other.low)

  def __mul__(self, other):
    products = [self.low * other.low, self.low * other.high, self.high * other.low, self.high*other.high]
    return Interval(min(products), max(products))

  def __truediv__(self, other):
    result = []
    if other.low == 0:
      if other.high == 0:
        result.append(self * Interval(-math.inf, math.inf))
      else:
        result.append(self * Interval(1/other.high, math.inf))
    elif other.high == 0:
      result.append(self * Interval(-math.inf, 1/other.low))
    elif other.low < 0 and 0 < other.high:
      result.append(self * Interval(-math.inf, 1/other.low), self * Interval(1/other.high, math.inf))
    else:
      result.append(self * Interval(1/other.high, 1/other.low))
    return result

# multi-interval arithmetic on constants (so far)
class AbstractInterpreter(ast.NodeVisitor):
  def visit_Constant(self, node):
    return [Interval(node.value)]

  def visit_Module(self, node):
    for expr in node.body:
      value = self.visit(expr)
    return value

  def visit_Expr(self, node):
    return self.visit(node.value)

  def visit_BinOp(self, node):
    left = self.visit(node.left)
    right = self.visit(node.right)
    match type(node.op).__name__:
      case "Add":
        return [a + b for a in left for b in right]
      case "Sub":
        return [a - b for a in left for b in right]
      case "Mult":
        return [a * b for a in left for b in right]
      case "Div":
        return [d for a in left for b in right for d in a/b]
      case _:
        raise NotImplementedError()

interpreter = AbstractInterpreter()
tree = ast.parse("1 + 2 + 3 / 4")
print(ast.dump(tree))
print(interpreter.visit(tree))

sil.py

import ast
import math
import random

# Simple value wrapper where we will define semantics
class Value:
  def __init__(self, value):
    self.value = value
  def __repr__(a):
    return str(a.value)
  def opAdd(a, b):
    return Value(a.value + b.value)
  def opSub(a, b):
    return Value(a.value - b.value)
  def opMul(a, b):
    return Value(a.value * b.value)
  def opDiv(a, b):
    return Value(a.value // b.value)
  def opMod(a, b):
    return Value(a.value % b.value)
  def opAnd(a, *b):
    return Value(a.value and all([c.value for c in b]))
  def opOr(a, *b):
    return Value(a.value or any([c.value for c in b]))
  def opEq(a, b):
    return Value(a.value == b.value)
  def opNotEq(a, b):
    return Value(a.value != b.value)
  def opLt(a, b):
    return Value(a.value < b.value)
  def opLtE(a, b):
    return Value(a.value <= b.value)
  def opGt(a, b):
    return Value(a.value > b.value)
  def opGtE(a, b):
    return Value(a.value >= b.value)
  def opNot(a, *b):
    return Value(not a.value)
  def opUAdd(a, *b):
    return a
  def opUSub(a, *b):
    return Value(-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):
  def __init__(self):
    self.env = {}

  def __repr__(self):
    return str(self.env)

  def visit_Constant(self, node):
    return Value(node.value)

  def op(self, op, a, *b):
    return getattr(self.visit(a), f'op{type(op).__name__}')(*[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_If(self, node):
    body = node.body if self.visit(node.test).value else node.orelse
    for expr in body:
      self.visit(expr)

  def visit_While(self, node):
    while self.visit(node.test).value:
      for expr in node.body:
        self.visit(expr)

  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(random.randint(0, 9)) if node.id == "random" else self.env[node.id]

interpreter = AbstractInterpreter()
tree = ast.parse("""
x = 13 % 4
""")
print(ast.dump(tree))
interpreter.visit(tree)
print(interpreter)