q.py

import lattice
import sys
import itertools


# --[ signed/unsigned lattice L ] --

# pretty printer for each set
class L_Elem(frozenset):
    def __str__(self):
        #return "{" + (",".join( [ str(x) for x in self ] )) + "}"
        return "X" # Why does it not print this in the Q lattice? XXX

L_pow = [ L_Elem(), L_Elem(['s']), L_Elem(['u']), L_Elem(['s', 'u']) ]

def L_join(l1, l2): return l1 | l2
def L_meet(l1, l2): return l1 & l2

L_poset = lattice.Lattice(L_pow, L_join, L_meet)

# --[ Bit vector lattice, B ]--

class B_Elem(tuple):
    def __str__(self):
        return "<" + ",".join([str(x) for x in self]) + ">"

bit_set = [0, 1]
num_flags = 2
#B_pow = [[x1, x2, x3] for x1 in bit_set for x2 in bit_set for x3 in bit_set ]
B_pow = list(itertools.product(bit_set, repeat=num_flags))

def B_join(b1, b2):
    return B_Elem( b1[i] | b2[i] for i in range(len(b1)) )

def B_meet(b1, b2):
    return B_Elem( b1[i] & b2[i] for i in range(len(b1)) )

B_poset = lattice.Lattice(B_pow, B_join, B_meet)

# --[ Registers mapping lattice ]--

class A_Elem(dict):
    def __str__(self):
        return ",".join("{ %s -> %s }" % (k, v) for (k,v) in self.items())

R = set(["r1", "r2"]) # Just two registers for now
A_pow = [ A_Elem(zip(R, x)) for x in itertools.product(L_pow, repeat=len(R)) ]

def A_join(a1, a2):
    new = {}
    for k in a1.keys():
        new[k] = a1[k] | a2[k]
    return new

def A_meet(a1, a2):
    new = {}
    for k in a1.keys():
        new[k] = a1[k] & a2[k]
    return new

A_poset = lattice.Lattice(A_pow, A_join, A_meet)

# Finally Q, the entire abstract domain : A x B

Q_pow = [ (A_Elem(x), B_Elem(y)) for x in A_pow for y in B_pow ]

def Q_join(q1, q2):
    (q1_a, q1_b) = q1
    (q2_a, q2_b) = q2
    return (A_join(q1_a, q2_a), B_join(q1_b, q2_b))

def Q_meet(q1, q2):
    (q1_a, q1_b) = q1
    (q2_a, q2_b) = q2
    return (A_meet(q1_a, q2_a), B_meet(q1_b, q2_b))

Q_poset = lattice.Lattice(Q_pow, Q_join, Q_meet)

# ---- Throw out graphviz code to make diagrams
with open("/tmp/L.dot", "w") as f:
    f.write(L_poset.Hasse())

with open("/tmp/B.dot", "w") as f:
    f.write(B_poset.Hasse())

with open("/tmp/A.dot", "w") as f:
    f.write(A_poset.Hasse())

with open("/tmp/Q.dot", "w") as f:
    f.write(Q_poset.Hasse())