Mercurial > pysmcl

changeset 18:429e347be685

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Moved files to source code repository.
author Janus Dam Nielsen <janus.nielsen@alexandra.dk>
date Fri, 22 May 2009 16:50:47 +0200
parents e83209448370
children 0652f6e02dc8 eec6a42fc1c6
files compatibility_check.py doctests.py flow.py graph.py ideal_functionality.py pretty_print.py proof_burden.py pysmcl/compatibility_check.py pysmcl/flow.py pysmcl/graph.py pysmcl/ideal_functionality.py pysmcl/pretty_print.py pysmcl/proof_burden.py pysmcl/secret_annotator.py pysmcl/secret_ifs.py pysmcl/test/unit/doctests.py pysmcl/test/unit/test.py pysmcl/util.py secret_annotator.py secret_ifs.py test.py util.py
diffstat 22 files changed, 898 insertions(+), 887 deletions(-) [+]
line wrap: on
line diff
--- a/compatibility_check.py	Fri May 22 16:32:37 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-import ast
-
-from util import error
-
-"""
-We only want to treat a small subset of Python in our
-analysis.
-
-Therefore we run it though this Visitor ruling out any
-constructs that we do not treat yet.
-
-In all other phases we assume that the functions treated are confined
-to this subset.
-"""
-
-
-class CompatibilityChecker(ast.NodeVisitor):
-
-    def __init__(self):
-        self.inside_function_def = False
-
-    def visit_BoolOp(self, node):
-        if not len(node.values) == 2:
-            error("Too many arguments", node)
-
-    def visit_Compare(self, node):
-        if len(node.ops)>1:
-            error("Too many arguments", node)
-        if len(node.comparators)>1:
-            error("Too many arguments", node)
-
-    def visit_Lambda(self, node):
-        error("Not implemented", node)
-
-    def visit_IfExp(self, node):
-        error("Not implemented", node)
-
-    def visit_ListComp(self, node):
-        error("Not implemented", node)
-
-    def visit_Yield(self, node):
-        error("Not implemented", node)
-
-    def visit_FunctionDef(self, node):
-        if self.inside_function_def:
-            error("Nested functions not allowed", node)
-        self.inside_function_def = True
-        self.generic_visit(node)
-        self.inside_function_def = False
-
-    def visit_TryExcept(self, node):
-        error("Not implemented", node)
-
-    def visit_TryFinally(self, node):
-        error("Not implemented", node)
-
-    def visit_Delete(self, node):
-        error("Not implemented", node)
--- a/doctests.py	Fri May 22 16:32:37 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-from doctest import testfile
-
-for i in ["secret_ifs.py",
-          "pretty_print.py"]:
-    testfile(i)
-
-
--- a/flow.py	Fri May 22 16:32:37 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-import inspect
-import ast
-import pretty_print
-import secret_ifs
-
-
-def analyze(node, join, combine, key):
-    """
-    Doing a simple forward analysis using the iterative worklist
-    algorithm. Parametrized by the functions join and combine, and
-    with the value initial.  The lattice-points are stored in each
-    statement-node in_values and out_values, under the *key*.
-    """
-    # initialization
-    worklist = []
-
-    Flow().flow(node)
-    for child in ast.walk(node):
-        if(isinstance(child, ast.stmt)):
-            child.in_values[key] = combine(child, set())
-            worklist.append(child)
-
-    # main cycle
-    while len(worklist) != 0:
-        x = worklist.pop()
-        oldout = x.out_values[key]
-        x.out_values[key] = combine(x, join(x.parents))
-        if oldout != x.out_values[key]:
-            for child in x.children:
-                worklist.append(child)
-                child.in_values[key] = x.out_values[key]
-
-
-class Flow():
-
-    def __init__(self):
-        self.to_loop_exit = set()
-        self.to_function_exit = set()
-
-    def flow(self, function):
-        #function.body.append(ast.Pass)
-        self.flow_body(function.body)
-        # Todo - edges from function returns...
-        # Neccesary?
-
-    def make_edge(self, from_nodes, to_node):
-        for from_node in from_nodes:
-            from_node.children = from_node.children | set([to_node])
-            to_node.parents = to_node.parents | set([from_node])
-
-    def flow_body(self, body=None,
-                  entry=None):
-        if not entry:
-            entry = set()
-        current = entry
-        for stm in body:
-            self.make_edge(current, stm)
-            if isinstance(stm, ast.If):
-                out_of_then = self.flow_body(stm.body, current)
-                out_of_else = self.flow_body(stm.orelse, current)
-                current = out_of_then | out_of_else
-            elif isinstance(stm, ast.While):
-                # TODO, does not express the condition being evaluated twice
-                # We have to rewrite the expression to make it right.
-                before = current
-                out_of_while = self.flow_body(stm.body, current)
-                self.make_edge(out_of_while, stm)
-                current = before | out_of_while | self.to_loop_exit
-                self.to_loop_exit = set()
-            elif isinstance(stm, ast.Break):
-                self.to_loop_exit = self.to_loop_exit | set([stm])
-                return set()
-            elif isinstance(stm, ast.Return):
-                self.to_loop_exit = self.to_loop_exit | set([stm])
-                return set()
-            else:
-                current = set([stm])
-        return current
-
-
--- a/graph.py	Fri May 22 16:32:37 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-
-
-class Node:
-    count = 0
-
-    def __init__(self, msg = ""):
-        self.out=[]
-        Node.count += 1
-        self.nr = str(Node.count)
-        self.msg = msg
-
-
-class Graph:
-
-    def __init__(self, entry, ex):
-        self.entry = entry
-        self.ex = ex
-
-    def to_dot(self):
-        taken = set()
-        print "digraph G {"
-        print "  in -> %s" % self.entry.nr
-        print '  in [shape = plaintext, label=""]'
-        print "  %s -> out" % self.ex.nr
-        print '  out [shape = plaintext, label=""]'
-        stack = [self.entry]
-        while(True):
-            while(True):
-                if len(stack)==0:
-                    current = None
-                    break
-                current = stack.pop()
-                if current not in taken:
-                    break
-            if not current:
-                break
-            print '    %s [label="%s"]' % (current.nr, current.msg)
-            taken.add(current)
-            for i in current.out:
-                print "    %s->%s;" % (current.nr, i.nr)
-
-            stack += current.out # list concatenation
-        print "}"
--- a/ideal_functionality.py	Fri May 22 16:32:37 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-import inspect
-import ast
-from collections import defaultdict
-
-import pretty_print
-import secret_annotator
-import secret_ifs
-import compatibility_check
-import proof_burden
-
-
-def init_statements(node):
-    """
-    Prepares all statements under node for further analysis.
-    """
-    for child in ast.walk(node):
-        if(isinstance(child, ast.stmt)):
-            # children and parents are used for flow-graph edges
-            child.children = set()
-            child.parents = set()
-            # in_values and out_values are used for storing
-            # lattice-points in for static analyses using the monotone
-            # framework.
-            child.in_values = defaultdict(set)
-            child.out_values = defaultdict(set)
-
-
-def ideal_functionality(f):
-    source_str = inspect.getsource(f)
-    source_ast = ast.parse(source_str) # Returns a module
-    function_ast = source_ast.body[0] # We want only the function
-    #pretty_print.PrettyPrinter().visit(source_ast)
-    init_statements(function_ast)
-    # We don't want recursive applications of this decorator
-    #function_ast.decorator_list.remove[0]
-    print "-"*80
-    compatibility_check.CompatibilityChecker().visit(function_ast)
-    secret_annotator.secret_analysis(function_ast)
-    t = secret_ifs.TransformIfs().visit(function_ast)
-    t.decorator_list.pop()
-    proof_burden.proof_burden(t)
-    exec compile(ast.Module([t]), "<string>", "exec")
-    #pretty_print.PrettyPrinter().visit(t)
-    return eval(function_ast.name)
--- a/pretty_print.py	Fri May 22 16:32:37 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,368 +0,0 @@
-"""
-Pretty printing of the Python built-in ast-type.
-
-The goal is to print a program with the exact same semantics as the
-program parsed into the ast.
-"""
-
-import ast
-
-
-def arguments_string(arguments):
-    """ Returns a string representing the argument list, surrounded by
-    parenthesis.
-    """
-    if(arguments.vararg):
-        assert False, "Not implemented"
-    if(arguments.kwarg):
-        assert False, "Not implemented"
-    args = ", ".join([i.id for i in arguments.args])
-    return "(" + args + ")"
-
-
-def op_string(op):
-    """ Returns a string representing the operator *op*.
-    """
-    ops = {ast.Add: "+",
-           ast.Sub: "-",
-           ast.Mult: "*",
-           ast.Div: "/",
-           ast.Mod: "%",
-           ast.Pow: "**",
-           ast.LShift: "<<",
-           ast.RShift: ">>",
-           ast.BitOr: "|",
-           ast.BitXor: "^",
-           ast.BitAnd: "&",
-           ast.FloorDiv: "//",
-           ast.Invert: "~",
-           ast.Not: "not",
-           ast.UAdd: "+",
-           ast.USub: "-",
-           ast.Eq: "==",
-           ast.NotEq: "!=",
-           ast.Lt: "<",
-           ast.LtE: "<=",
-           ast.Gt: ">",
-           ast.GtE: ">=",
-           ast.Is: "is",
-           ast.IsNot: "is not",
-           ast.In: "in",
-           ast.NotIn: "not in",
-           ast.And: "and",
-           ast.Or: "or",
-           }
-    assert op.__class__ in ops, "Not implemented %s" % op
-    return ops[op.__class__]
-
-
-def op_precedence(op):
-    """ Returns the operator precedence of *op*
-    Made after the reference found here:
-    http://www.ibiblio.org/g2swap/byteofpython/read/operator-precedence.html
-    """
-
-    ops = {
-        ast.Or: 2,
-        ast.And: 3,
-        ast.Not: 4,
-        ast.In: 5,
-        ast.NotIn: 5,
-        ast.Is: 6,
-        ast.IsNot: 6,
-        ast.NotEq: 7,
-        ast.Lt: 7,
-        ast.LtE: 7,
-        ast.Gt: 7,
-        ast.GtE: 7,
-        ast.Eq: 7,
-        ast.BitOr: 8,
-        ast.BitXor: 9,
-        ast.BitAnd: 10,
-        ast.LShift: 11,
-        ast.RShift: 11,
-        ast.Add: 12,
-        ast.Sub: 12,
-        ast.Mult: 13,
-        ast.Div: 13,
-        ast.Mod: 13,
-        ast.FloorDiv: 13,
-        ast.UAdd: 14,
-        ast.USub: 14,
-        ast.Invert: 15,
-        ast.Pow: 16,
-           }
-    return ops[op.__class__]
-
-
-def slice_string(slice):
-    if(isinstance(slice, ast.Ellipsis)):
-        return "..."
-    elif(isinstance(slice, ast.Index)):
-        return expr_string(slice.value)
-    elif(isinstance(slice, ast.Slice)):
-        #TODO: handle null lower/upper
-        #TODO: handle steps
-        return "%s:%s" % \
-            (expr_string(slice.lower),
-             expr_string(slice.upper))
-    else:
-        #TODO: handle several slices
-        assert False
-
-
-def expr_string(exp, prec=1):
-    """Returns a string representation of the expression.
-    *prec* is the precedence of the surrounding of the expression,
-    and determines if parenthesis are neccesary.
-    >>> from ast import *
-    >>> from pretty_print import *
-    >>> expr_string(BinOp(op=Mult(), left=BinOp(op=Add(), left=Num(1),
-    ... right=Num(4)), right=Num(2)))
-    '(1 + 4) * 2'
-
-    """
-    if hasattr(exp, "op"):
-        my_precedence = op_precedence(exp.op)
-    if(isinstance(exp, ast.BoolOp)):
-        assert len(exp.values) == 2, "Not implemented"
-
-        r = "%s %s %s" % \
-                 (expr_string(exp.values[0], my_precedence),
-                  op_string(exp.op),
-                  expr_string(exp.values[1]), my_precedence),
-    elif(isinstance(exp, ast.BinOp)):
-        r = "%s %s %s" % \
-                    (expr_string(exp.left, my_precedence),
-                     op_string(exp.op),
-                     expr_string(exp.right, my_precedence))
-    elif(isinstance(exp, ast.Compare)):
-        my_precedence = op_precedence(exp.ops[0])
-        if len(exp.ops)>1:
-            assert False, "Not implemented"
-        if len(exp.comparators)>1:
-            assert False, "Not implemented"
-        r = "%s %s %s" % \
-            (expr_string(exp.left), op_string(exp.ops[0]),
-             expr_string(exp.comparators[0]))
-    elif(isinstance(exp, ast.UnaryOp)):
-        r = " %s (%s)" % \
-            (op_string(exp.op), expr_string(exp.operand),
-             op_precedence(exp.op))
-    elif(isinstance(exp, ast.Lambda)):
-        my_precedence = 1
-        r = "lambda%s : %s" % \
-            (arguments_string(exp.args),
-             expr_string(exp.body, my_precedence))
-    elif(isinstance(exp, ast.IfExp)):
-        assert False, "Not implemented"
-    elif(isinstance(exp, ast.Dict)):
-        my_precedence = 25
-        r = "{"+" ".join(["%s : %s" % (expr_string(i),
-                                       expr_string(j)) for (i, j) in
-                          zip(exp.keys, exp.values)])+"}"
-    elif(isinstance(exp, ast.ListComp)):
-        assert False, "Not implemented"
-    elif(isinstance(exp, ast.Name)):
-        my_precedence = 100
-        r = exp.id
-    elif(isinstance(exp, ast.Num)):
-        my_precedence = 100
-        r = str(exp.n)
-    elif(isinstance(exp, ast.Yield)):
-        my_precedence = 22 # Binds like a function call, Is this correct?
-        r = "yield(%s)" % expr_string(exp.value)
-    elif(isinstance(exp, ast.Call)):
-        my_precedence = 22
-        args_list = []
-        if len(exp.args)>0:
-            args_list.append(", ".join([expr_string(i, 1)
-                                        for i in exp.args]))
-        if len(exp.keywords)>0:
-            args_list.append(", ".join([i.arg +
-                                        "=" + expr_string(i.value, 1)
-                                        for i in exp.keywords]))
-        if exp.starargs:
-            args_list.append("*"+expr_string(exp.starargs, 1))
-        if exp.kwargs:
-            args_list.append("**"+expr_string(exp.kwargs, 1))
-        r = "%s(%s)" % \
-            (expr_string(exp.func, my_precedence),
-             ", ".join(args_list))
-    elif(isinstance(exp, dict)):
-        print exp
-        assert False, "Type error"
-    elif(isinstance(exp, ast.Subscript)):
-        my_precedence = 21
-        r = "%s[%s]" % \
-            (expr_string(exp.value, my_precedence), slice_string(exp.slice))
-    elif(isinstance(exp, ast.Str)):
-        my_precedence = 100
-        r = '"%s"' % exp.s
-    else:
-        assert False, "Not implemented of type %s" % type(exp)
-
-    if my_precedence <= prec:
-        return "(" + r + ")"
-    else:
-        return r
-    # TODO:
-#             | GeneratorExp(expr elt, comprehension* generators)
-#             | Repr(expr value)
-#             | Num(object n) -- a number as a PyObject.
-#             | Str(string s) -- need to specify raw, unicode, etc?
-#             -- other literals? bools?
-#
-#             -- the following expression can appear in assignment context
-#             | Attribute(expr value, identifier attr, expr_context ctx)
-#             | Subscript(expr value, slice slice, expr_context ctx)
-#             | Name(identifier id, expr_context ctx)
-#             | List(expr* elts, expr_context ctx)
-#             | Tuple(expr* elts, expr_context ctx)
-#
-#              attributes (int lineno, int col_offset)
-#
-#        expr_context = Load | Store | Del | AugLoad | AugStore | Param
-#
-#        slice = Ellipsis | Slice(expr? lower, expr? upper, expr? step)
-#              | ExtSlice(slice* dims)
-#              | Index(expr value)
-#
-#
-#        comprehension = (expr target, expr iter, expr* ifs)
-#
-#        -- not sure what to call the first argument for raise and except
-#        excepthandler = ExceptHandler(expr? type, expr? name, stmt* body)
-#                        attributes (int lineno, int col_offset)
-#
-#        arguments = (expr* args, identifier? vararg,
-#                    identifier? kwarg, expr* defaults)
-#
-#        -- keyword arguments supplied to call
-#        keyword = (identifier arg, expr value)
-#
-#        -- import name with optional 'as' alias.
-#        alias = (identifier name, identifier? asname)
-
-
-class PrettyPrinter(ast.NodeVisitor):
-    indent = 0
-
-    def print_body(self, body):
-        self.indent += 1
-        for i in body:
-            self.visit(i)
-        self.indent -= 1
-
-    def print_indented(self, str):
-        print (" "*(self.indent*4))+str
-
-    def visit_ClassDef(self, node):
-        for i in node.decorator_list:
-            self.print_indented("@%s" % expr_string(i))
-        self.print_indented("class %s(%s)" % (node.name,
-                                              [i.name for i in node.bases]))
-        self.print_body(node.body)
-
-    def visit_Return(self, node):
-        self.print_indented("return %s" % expr_string(node.value))
-
-    def visit_Delete(self, node):
-        assert False, "Not implemented"
-
-    def visit_Assign(self, node):
-        assert len(node.targets) == 1, "Not implemented"
-        self.print_indented("%s = %s" % (expr_string(node.targets[0]),
-                                         expr_string(node.value)))
-
-    def visit_AugAssign(self, node):
-        self.print_indented("%s %s= %s" % (expr_string(node.target),
-                                           op_string(node.op),
-                                           expr_string(node.value)))
-
-    def visit_Print(self, node):
-        if node.dest or not node.nl:
-            assert False, "Not implemented"
-        else:
-            self.print_indented("print %s" % \
-                               (", ".join([expr_string(i)
-                                           for i in node.values])))
-
-    def visit_For(self, node):
-        self.print_indented("for %s in %s:" % (expr_string(node.target),
-                                              expr_string(node.iter)))
-        self.print_body(node.body)
-        if(len(node.orelse)>0):
-            self.print_indented("else:")
-            self.print_body(node.orelse)
-
-    def visit_While(self, node):
-        self.print_indented("while(%s):" % expr_string(node.test))
-        self.print_body(node.body)
-        if(len(node.orelse)>0):
-            self.print_indented("else:")
-            self.print_body(node.orelse)
-
-    def visit_If(self, node):
-        self.print_indented("if(%s):" % expr_string(node.test))
-        self.print_body(node.body)
-        if(len(node.orelse)>0):
-            self.print_indented("else:")
-            self.print_body(node.orelse)
-
-    def visit_With(self, node):
-        assert False, "Not implemented"
-
-    def visit_Raise(self, node):
-        assert False, "Not implemented"
-
-    def visit_TryExcept(self, node):
-        assert False, "Not implemented"
-
-    def visit_TryFinally(self, node):
-        assert False, "Not implemented"
-
-    def visit_Assert(self, node):
-        if(node.msg):
-            self.print_indented("assert %s : %s", (expr_string(node.test),
-                                                   expr_string(node.msg)))
-        else:
-            self.print_indented("assert %s", expr_string(node.test))
-
-    def visit_Import(self, node):
-        assert False, "Not implemented"
-
-    def visit_ImportFrom(self, node):
-        assert False, "Not implemented"
-
-    def visit_Exec(self, node):
-        assert False, "Not implemented"
-
-    def visit_Global(self, node):
-        self.print_indented("global " + ", ".join(node.names))
-
-    def visit_Expr(self, node):
-        self.print_indented(expr_string(node.value))
-
-    def visit_Pass(self, node):
-        self.print_indented("pass")
-
-    def visit_Break(self, node):
-        self.print_indented("break")
-
-    def visit_Continue(self, node):
-        self.print_indented("continue")
-
-    def visit_FunctionDef(self, node):
-        for i in node.decorator_list:
-            self.print_indented("@%s" % expr_string(i))
-        self.print_indented("def %s%s:" % (node.name,
-                                             arguments_string(node.args)))
-        self.print_body(node.body)
-
-
-def pprint(module):
-    """Pretty prints the module represented by the ast node in
-    ***module***
-    """
-    PrettyPrinter().visit(module)
--- a/proof_burden.py	Fri May 22 16:32:37 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-import ast
-import inspect
-import pretty_print
-
-
-class FindInvariant(ast.NodeVisitor):
-
-    def visit_Call(self, node):
-        if isinstance(node.func, ast.Name):
-            if node.func.id == "invariant":
-                print "Invariant: " + (node.args[0].s)
-
-
-class ProofBurden(ast.NodeVisitor):
-
-    def __init__(self):
-        self.openings = []
-        self.results = []
-
-    def visit_While(self, node):
-        print "Prove the invariant is true in the initial case"
-        FindInvariant().visit(node)
-        print "Prove the invariant still holds given:"
-        FindInvariant().visit(node)
-        print "And", pretty_print.expr_string(node.test)
-        print "And this code is run:"
-        pretty_print.pprint(node)
-        self.generic_visit(node)
-
-    def visit_Call(self, node):
-        if isinstance(node.func, ast.Name):
-            if node.func.id == "open":
-                self.openings.append(pretty_print.expr_string(node.args[0]))
-            if node.func.id == "result":
-                self.results.append(pretty_print.expr_string(node.args[0]))
-            elif node.func.id == "precondition":
-                print "You can assume: " + (node.args[0].s)
-            elif node.func.id == "invariant":
-                print "Invariant"
-                print (node.args[0].s)
-
-
-def proof_burden(f):
-    b = ProofBurden()
-    b.visit(f)
-    print ("Show that you can compute:")
-    for i in b.openings:
-        print i
-    print ("From:")
-    for i in b.results:
-        print i
-
-    return f
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/pysmcl/compatibility_check.py	Fri May 22 16:50:47 2009 +0200
@@ -0,0 +1,59 @@
+import ast
+
+# Import PySMCL packages.
+from pysmcl.util import error
+
+"""
+We only want to treat a small subset of Python in our
+analysis.
+
+Therefore we run it though this Visitor ruling out any
+constructs that we do not treat yet.
+
+In all other phases we assume that the functions treated are confined
+to this subset.
+"""
+
+
+class CompatibilityChecker(ast.NodeVisitor):
+
+    def __init__(self):
+        self.inside_function_def = False
+
+    def visit_BoolOp(self, node):
+        if not len(node.values) == 2:
+            error("Too many arguments", node)
+
+    def visit_Compare(self, node):
+        if len(node.ops)>1:
+            error("Too many arguments", node)
+        if len(node.comparators)>1:
+            error("Too many arguments", node)
+
+    def visit_Lambda(self, node):
+        error("Not implemented", node)
+
+    def visit_IfExp(self, node):
+        error("Not implemented", node)
+
+    def visit_ListComp(self, node):
+        error("Not implemented", node)
+
+    def visit_Yield(self, node):
+        error("Not implemented", node)
+
+    def visit_FunctionDef(self, node):
+        if self.inside_function_def:
+            error("Nested functions not allowed", node)
+        self.inside_function_def = True
+        self.generic_visit(node)
+        self.inside_function_def = False
+
+    def visit_TryExcept(self, node):
+        error("Not implemented", node)
+
+    def visit_TryFinally(self, node):
+        error("Not implemented", node)
+
+    def visit_Delete(self, node):
+        error("Not implemented", node)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/pysmcl/flow.py	Fri May 22 16:50:47 2009 +0200
@@ -0,0 +1,82 @@
+import inspect
+import ast
+
+# Import PySMCL packages.
+import pysmcl.pretty_print
+import pysmcl.secret_ifs
+
+
+def analyze(node, join, combine, key):
+    """
+    Doing a simple forward analysis using the iterative worklist
+    algorithm. Parametrized by the functions join and combine, and
+    with the value initial.  The lattice-points are stored in each
+    statement-node in_values and out_values, under the *key*.
+    """
+    # initialization
+    worklist = []
+
+    Flow().flow(node)
+    for child in ast.walk(node):
+        if(isinstance(child, ast.stmt)):
+            child.in_values[key] = combine(child, set())
+            worklist.append(child)
+
+    # main cycle
+    while len(worklist) != 0:
+        x = worklist.pop()
+        oldout = x.out_values[key]
+        x.out_values[key] = combine(x, join(x.parents))
+        if oldout != x.out_values[key]:
+            for child in x.children:
+                worklist.append(child)
+                child.in_values[key] = x.out_values[key]
+
+
+class Flow():
+
+    def __init__(self):
+        self.to_loop_exit = set()
+        self.to_function_exit = set()
+
+    def flow(self, function):
+        #function.body.append(ast.Pass)
+        self.flow_body(function.body)
+        # Todo - edges from function returns...
+        # Neccesary?
+
+    def make_edge(self, from_nodes, to_node):
+        for from_node in from_nodes:
+            from_node.children = from_node.children | set([to_node])
+            to_node.parents = to_node.parents | set([from_node])
+
+    def flow_body(self, body=None,
+                  entry=None):
+        if not entry:
+            entry = set()
+        current = entry
+        for stm in body:
+            self.make_edge(current, stm)
+            if isinstance(stm, ast.If):
+                out_of_then = self.flow_body(stm.body, current)
+                out_of_else = self.flow_body(stm.orelse, current)
+                current = out_of_then | out_of_else
+            elif isinstance(stm, ast.While):
+                # TODO, does not express the condition being evaluated twice
+                # We have to rewrite the expression to make it right.
+                before = current
+                out_of_while = self.flow_body(stm.body, current)
+                self.make_edge(out_of_while, stm)
+                current = before | out_of_while | self.to_loop_exit
+                self.to_loop_exit = set()
+            elif isinstance(stm, ast.Break):
+                self.to_loop_exit = self.to_loop_exit | set([stm])
+                return set()
+            elif isinstance(stm, ast.Return):
+                self.to_loop_exit = self.to_loop_exit | set([stm])
+                return set()
+            else:
+                current = set([stm])
+        return current
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/pysmcl/graph.py	Fri May 22 16:50:47 2009 +0200
@@ -0,0 +1,43 @@
+
+
+class Node:
+    count = 0
+
+    def __init__(self, msg = ""):
+        self.out=[]
+        Node.count += 1
+        self.nr = str(Node.count)
+        self.msg = msg
+
+
+class Graph:
+
+    def __init__(self, entry, ex):
+        self.entry = entry
+        self.ex = ex
+
+    def to_dot(self):
+        taken = set()
+        print "digraph G {"
+        print "  in -> %s" % self.entry.nr
+        print '  in [shape = plaintext, label=""]'
+        print "  %s -> out" % self.ex.nr
+        print '  out [shape = plaintext, label=""]'
+        stack = [self.entry]
+        while(True):
+            while(True):
+                if len(stack)==0:
+                    current = None
+                    break
+                current = stack.pop()
+                if current not in taken:
+                    break
+            if not current:
+                break
+            print '    %s [label="%s"]' % (current.nr, current.msg)
+            taken.add(current)
+            for i in current.out:
+                print "    %s->%s;" % (current.nr, i.nr)
+
+            stack += current.out # list concatenation
+        print "}"
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/pysmcl/ideal_functionality.py	Fri May 22 16:50:47 2009 +0200
@@ -0,0 +1,45 @@
+import inspect
+import ast
+from collections import defaultdict
+
+# Import PySMCL packages.
+import pysmcl.pretty_print
+import pysmcl.secret_annotator
+import pysmcl.secret_ifs
+import pysmcl.compatibility_check
+import pysmcl.proof_burden
+
+
+def init_statements(node):
+    """
+    Prepares all statements under node for further analysis.
+    """
+    for child in ast.walk(node):
+        if(isinstance(child, ast.stmt)):
+            # children and parents are used for flow-graph edges
+            child.children = set()
+            child.parents = set()
+            # in_values and out_values are used for storing
+            # lattice-points in for static analyses using the monotone
+            # framework.
+            child.in_values = defaultdict(set)
+            child.out_values = defaultdict(set)
+
+
+def ideal_functionality(f):
+    source_str = inspect.getsource(f)
+    source_ast = ast.parse(source_str) # Returns a module
+    function_ast = source_ast.body[0] # We want only the function
+    #pretty_print.PrettyPrinter().visit(source_ast)
+    init_statements(function_ast)
+    # We don't want recursive applications of this decorator
+    #function_ast.decorator_list.remove[0]
+    print "-"*80
+    pysmcl.compatibility_check.CompatibilityChecker().visit(function_ast)
+    pysmcl.secret_annotator.secret_analysis(function_ast)
+    t = pysmcl.secret_ifs.TransformIfs().visit(function_ast)
+    t.decorator_list.pop()
+    pysmcl.proof_burden.proof_burden(t)
+    exec compile(ast.Module([t]), "<string>", "exec")
+    #pretty_print.PrettyPrinter().visit(t)
+    return eval(function_ast.name)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/pysmcl/pretty_print.py	Fri May 22 16:50:47 2009 +0200
@@ -0,0 +1,368 @@
+"""
+Pretty printing of the Python built-in ast-type.
+
+The goal is to print a program with the exact same semantics as the
+program parsed into the ast.
+"""
+
+import ast
+
+
+def arguments_string(arguments):
+    """ Returns a string representing the argument list, surrounded by
+    parenthesis.
+    """
+    if(arguments.vararg):
+        assert False, "Not implemented"
+    if(arguments.kwarg):
+        assert False, "Not implemented"
+    args = ", ".join([i.id for i in arguments.args])
+    return "(" + args + ")"
+
+
+def op_string(op):
+    """ Returns a string representing the operator *op*.
+    """
+    ops = {ast.Add: "+",
+           ast.Sub: "-",
+           ast.Mult: "*",
+           ast.Div: "/",
+           ast.Mod: "%",
+           ast.Pow: "**",
+           ast.LShift: "<<",
+           ast.RShift: ">>",
+           ast.BitOr: "|",
+           ast.BitXor: "^",
+           ast.BitAnd: "&",
+           ast.FloorDiv: "//",
+           ast.Invert: "~",
+           ast.Not: "not",
+           ast.UAdd: "+",
+           ast.USub: "-",
+           ast.Eq: "==",
+           ast.NotEq: "!=",
+           ast.Lt: "<",
+           ast.LtE: "<=",
+           ast.Gt: ">",
+           ast.GtE: ">=",
+           ast.Is: "is",
+           ast.IsNot: "is not",
+           ast.In: "in",
+           ast.NotIn: "not in",
+           ast.And: "and",
+           ast.Or: "or",
+           }
+    assert op.__class__ in ops, "Not implemented %s" % op
+    return ops[op.__class__]
+
+
+def op_precedence(op):
+    """ Returns the operator precedence of *op*
+    Made after the reference found here:
+    http://www.ibiblio.org/g2swap/byteofpython/read/operator-precedence.html
+    """
+
+    ops = {
+        ast.Or: 2,
+        ast.And: 3,
+        ast.Not: 4,
+        ast.In: 5,
+        ast.NotIn: 5,
+        ast.Is: 6,
+        ast.IsNot: 6,
+        ast.NotEq: 7,
+        ast.Lt: 7,
+        ast.LtE: 7,
+        ast.Gt: 7,
+        ast.GtE: 7,
+        ast.Eq: 7,
+        ast.BitOr: 8,
+        ast.BitXor: 9,
+        ast.BitAnd: 10,
+        ast.LShift: 11,
+        ast.RShift: 11,
+        ast.Add: 12,
+        ast.Sub: 12,
+        ast.Mult: 13,
+        ast.Div: 13,
+        ast.Mod: 13,
+        ast.FloorDiv: 13,
+        ast.UAdd: 14,
+        ast.USub: 14,
+        ast.Invert: 15,
+        ast.Pow: 16,
+           }
+    return ops[op.__class__]
+
+
+def slice_string(slice):
+    if(isinstance(slice, ast.Ellipsis)):
+        return "..."
+    elif(isinstance(slice, ast.Index)):
+        return expr_string(slice.value)
+    elif(isinstance(slice, ast.Slice)):
+        #TODO: handle null lower/upper
+        #TODO: handle steps
+        return "%s:%s" % \
+            (expr_string(slice.lower),
+             expr_string(slice.upper))
+    else:
+        #TODO: handle several slices
+        assert False
+
+
+def expr_string(exp, prec=1):
+    """Returns a string representation of the expression.
+    *prec* is the precedence of the surrounding of the expression,
+    and determines if parenthesis are neccesary.
+    >>> from ast import *
+    >>> from pysmcl.pretty_print import *
+    >>> expr_string(BinOp(op=Mult(), left=BinOp(op=Add(), left=Num(1),
+    ... right=Num(4)), right=Num(2)))
+    '(1 + 4) * 2'
+
+    """
+    if hasattr(exp, "op"):
+        my_precedence = op_precedence(exp.op)
+    if(isinstance(exp, ast.BoolOp)):
+        assert len(exp.values) == 2, "Not implemented"
+
+        r = "%s %s %s" % \
+                 (expr_string(exp.values[0], my_precedence),
+                  op_string(exp.op),
+                  expr_string(exp.values[1]), my_precedence),
+    elif(isinstance(exp, ast.BinOp)):
+        r = "%s %s %s" % \
+                    (expr_string(exp.left, my_precedence),
+                     op_string(exp.op),
+                     expr_string(exp.right, my_precedence))
+    elif(isinstance(exp, ast.Compare)):
+        my_precedence = op_precedence(exp.ops[0])
+        if len(exp.ops)>1:
+            assert False, "Not implemented"
+        if len(exp.comparators)>1:
+            assert False, "Not implemented"
+        r = "%s %s %s" % \
+            (expr_string(exp.left), op_string(exp.ops[0]),
+             expr_string(exp.comparators[0]))
+    elif(isinstance(exp, ast.UnaryOp)):
+        r = " %s (%s)" % \
+            (op_string(exp.op), expr_string(exp.operand),
+             op_precedence(exp.op))
+    elif(isinstance(exp, ast.Lambda)):
+        my_precedence = 1
+        r = "lambda%s : %s" % \
+            (arguments_string(exp.args),
+             expr_string(exp.body, my_precedence))
+    elif(isinstance(exp, ast.IfExp)):
+        assert False, "Not implemented"
+    elif(isinstance(exp, ast.Dict)):
+        my_precedence = 25
+        r = "{"+" ".join(["%s : %s" % (expr_string(i),
+                                       expr_string(j)) for (i, j) in
+                          zip(exp.keys, exp.values)])+"}"
+    elif(isinstance(exp, ast.ListComp)):
+        assert False, "Not implemented"
+    elif(isinstance(exp, ast.Name)):
+        my_precedence = 100
+        r = exp.id
+    elif(isinstance(exp, ast.Num)):
+        my_precedence = 100
+        r = str(exp.n)
+    elif(isinstance(exp, ast.Yield)):
+        my_precedence = 22 # Binds like a function call, Is this correct?
+        r = "yield(%s)" % expr_string(exp.value)
+    elif(isinstance(exp, ast.Call)):
+        my_precedence = 22
+        args_list = []
+        if len(exp.args)>0:
+            args_list.append(", ".join([expr_string(i, 1)
+                                        for i in exp.args]))
+        if len(exp.keywords)>0:
+            args_list.append(", ".join([i.arg +
+                                        "=" + expr_string(i.value, 1)
+                                        for i in exp.keywords]))
+        if exp.starargs:
+            args_list.append("*"+expr_string(exp.starargs, 1))
+        if exp.kwargs:
+            args_list.append("**"+expr_string(exp.kwargs, 1))
+        r = "%s(%s)" % \
+            (expr_string(exp.func, my_precedence),
+             ", ".join(args_list))
+    elif(isinstance(exp, dict)):
+        print exp
+        assert False, "Type error"
+    elif(isinstance(exp, ast.Subscript)):
+        my_precedence = 21
+        r = "%s[%s]" % \
+            (expr_string(exp.value, my_precedence), slice_string(exp.slice))
+    elif(isinstance(exp, ast.Str)):
+        my_precedence = 100
+        r = '"%s"' % exp.s
+    else:
+        assert False, "Not implemented of type %s" % type(exp)
+
+    if my_precedence <= prec:
+        return "(" + r + ")"
+    else:
+        return r
+    # TODO:
+#             | GeneratorExp(expr elt, comprehension* generators)
+#             | Repr(expr value)
+#             | Num(object n) -- a number as a PyObject.
+#             | Str(string s) -- need to specify raw, unicode, etc?
+#             -- other literals? bools?
+#
+#             -- the following expression can appear in assignment context
+#             | Attribute(expr value, identifier attr, expr_context ctx)
+#             | Subscript(expr value, slice slice, expr_context ctx)
+#             | Name(identifier id, expr_context ctx)
+#             | List(expr* elts, expr_context ctx)
+#             | Tuple(expr* elts, expr_context ctx)
+#
+#              attributes (int lineno, int col_offset)
+#
+#        expr_context = Load | Store | Del | AugLoad | AugStore | Param
+#
+#        slice = Ellipsis | Slice(expr? lower, expr? upper, expr? step)
+#              | ExtSlice(slice* dims)
+#              | Index(expr value)
+#
+#
+#        comprehension = (expr target, expr iter, expr* ifs)
+#
+#        -- not sure what to call the first argument for raise and except
+#        excepthandler = ExceptHandler(expr? type, expr? name, stmt* body)
+#                        attributes (int lineno, int col_offset)
+#
+#        arguments = (expr* args, identifier? vararg,
+#                    identifier? kwarg, expr* defaults)
+#
+#        -- keyword arguments supplied to call
+#        keyword = (identifier arg, expr value)
+#
+#        -- import name with optional 'as' alias.
+#        alias = (identifier name, identifier? asname)
+
+
+class PrettyPrinter(ast.NodeVisitor):
+    indent = 0
+
+    def print_body(self, body):
+        self.indent += 1
+        for i in body:
+            self.visit(i)
+        self.indent -= 1
+
+    def print_indented(self, str):
+        print (" "*(self.indent*4))+str
+
+    def visit_ClassDef(self, node):
+        for i in node.decorator_list:
+            self.print_indented("@%s" % expr_string(i))
+        self.print_indented("class %s(%s)" % (node.name,
+                                              [i.name for i in node.bases]))
+        self.print_body(node.body)
+
+    def visit_Return(self, node):
+        self.print_indented("return %s" % expr_string(node.value))
+
+    def visit_Delete(self, node):
+        assert False, "Not implemented"
+
+    def visit_Assign(self, node):
+        assert len(node.targets) == 1, "Not implemented"
+        self.print_indented("%s = %s" % (expr_string(node.targets[0]),
+                                         expr_string(node.value)))
+
+    def visit_AugAssign(self, node):
+        self.print_indented("%s %s= %s" % (expr_string(node.target),
+                                           op_string(node.op),
+                                           expr_string(node.value)))
+
+    def visit_Print(self, node):
+        if node.dest or not node.nl:
+            assert False, "Not implemented"
+        else:
+            self.print_indented("print %s" % \
+                               (", ".join([expr_string(i)
+                                           for i in node.values])))
+
+    def visit_For(self, node):
+        self.print_indented("for %s in %s:" % (expr_string(node.target),
+                                              expr_string(node.iter)))
+        self.print_body(node.body)
+        if(len(node.orelse)>0):
+            self.print_indented("else:")
+            self.print_body(node.orelse)
+
+    def visit_While(self, node):
+        self.print_indented("while(%s):" % expr_string(node.test))
+        self.print_body(node.body)
+        if(len(node.orelse)>0):
+            self.print_indented("else:")
+            self.print_body(node.orelse)
+
+    def visit_If(self, node):
+        self.print_indented("if(%s):" % expr_string(node.test))
+        self.print_body(node.body)
+        if(len(node.orelse)>0):
+            self.print_indented("else:")
+            self.print_body(node.orelse)
+
+    def visit_With(self, node):
+        assert False, "Not implemented"
+
+    def visit_Raise(self, node):
+        assert False, "Not implemented"
+
+    def visit_TryExcept(self, node):
+        assert False, "Not implemented"
+
+    def visit_TryFinally(self, node):
+        assert False, "Not implemented"
+
+    def visit_Assert(self, node):
+        if(node.msg):
+            self.print_indented("assert %s : %s", (expr_string(node.test),
+                                                   expr_string(node.msg)))
+        else:
+            self.print_indented("assert %s", expr_string(node.test))
+
+    def visit_Import(self, node):
+        assert False, "Not implemented"
+
+    def visit_ImportFrom(self, node):
+        assert False, "Not implemented"
+
+    def visit_Exec(self, node):
+        assert False, "Not implemented"
+
+    def visit_Global(self, node):
+        self.print_indented("global " + ", ".join(node.names))
+
+    def visit_Expr(self, node):
+        self.print_indented(expr_string(node.value))
+
+    def visit_Pass(self, node):
+        self.print_indented("pass")
+
+    def visit_Break(self, node):
+        self.print_indented("break")
+
+    def visit_Continue(self, node):
+        self.print_indented("continue")
+
+    def visit_FunctionDef(self, node):
+        for i in node.decorator_list:
+            self.print_indented("@%s" % expr_string(i))
+        self.print_indented("def %s%s:" % (node.name,
+                                             arguments_string(node.args)))
+        self.print_body(node.body)
+
+
+def pprint(module):
+    """Pretty prints the module represented by the ast node in
+    ***module***
+    """
+    PrettyPrinter().visit(module)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/pysmcl/proof_burden.py	Fri May 22 16:50:47 2009 +0200
@@ -0,0 +1,55 @@
+import ast
+import inspect
+
+# Import PySMCL packages.
+import pysmcl.pretty_print
+
+
+class FindInvariant(ast.NodeVisitor):
+
+    def visit_Call(self, node):
+        if isinstance(node.func, ast.Name):
+            if node.func.id == "invariant":
+                print "Invariant: " + (node.args[0].s)
+
+
+class ProofBurden(ast.NodeVisitor):
+
+    def __init__(self):
+        self.openings = []
+        self.results = []
+
+    def visit_While(self, node):
+        print "Prove the invariant is true in the initial case"
+        FindInvariant().visit(node)
+        print "Prove the invariant still holds given:"
+        FindInvariant().visit(node)
+        print "And", pysmcl.pretty_print.expr_string(node.test)
+        print "And this code is run:"
+        pysmcl.pretty_print.pprint(node)
+        self.generic_visit(node)
+
+    def visit_Call(self, node):
+        if isinstance(node.func, ast.Name):
+            if node.func.id == "open":
+                self.openings.append(pysmcl.pretty_print.expr_string(node.args[0]))
+            if node.func.id == "result":
+                self.results.append(pysmcl.pretty_print.expr_string(node.args[0]))
+            elif node.func.id == "precondition":
+                print "You can assume: " + (node.args[0].s)
+            elif node.func.id == "invariant":
+                print "Invariant"
+                print (node.args[0].s)
+
+
+def proof_burden(f):
+    b = ProofBurden()
+    b.visit(f)
+    print ("Show that you can compute:")
+    for i in b.openings:
+        print i
+    print ("From:")
+    for i in b.results:
+        print i
+
+    return f
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/pysmcl/secret_annotator.py	Fri May 22 16:50:47 2009 +0200
@@ -0,0 +1,86 @@
+import util
+import ast
+
+# Import PySMCL packages.
+import pysmcl.flow
+
+
+def expr_secret(exp, secret_variables):
+    """
+    Returns True if the expression exp should be considered secret
+    given that the variables in *secret_variables* are secret.
+    """
+    non_compromising_functions = set(["len", "open", "result"])
+    if(isinstance(exp, ast.BoolOp)):
+        return (expr_secret(exp.values[0], secret_variables)
+                 or expr_secret(exp.values[1], secret_variables))
+    elif(isinstance(exp, ast.BinOp)):
+        return (expr_secret(exp.left, secret_variables)
+                 or expr_secret(exp.right, secret_variables))
+    elif(isinstance(exp, ast.Compare)):
+        return (expr_secret(exp.left, secret_variables)
+                or expr_secret(exp.comparators[0], secret_variables))
+    elif(isinstance(exp, ast.UnaryOp)):
+            return (expr_secret(exp.operand, secret_variables))
+    elif(isinstance(exp, ast.Dict)):
+        return any([expr_secret(i, secret_variables) for i in exp.values])
+    elif(isinstance(exp, ast.Name)):
+        return exp.id in secret_variables
+    elif(isinstance(exp, ast.Num)):
+        return False
+    elif(isinstance(exp, ast.Call)):
+        if(not isinstance(exp.func, ast.Name)):
+            if(any([expr_secret(i, secret_variables) for i in exp.args])):
+                util.error("Call of non-fixed function with secret argument",
+                           exp)
+        if(exp.func.id in non_compromising_functions):
+            return False
+        func = eval(exp.func.id)
+        if(func.secret):
+            return True
+        elif(any([expr_secret(i, secret_variables) for i in exp.args])):
+            util.error("Call of non-secret\
+ function with secret argument", exp)
+        else:
+            return True # For now
+    else:
+        assert False, "Not implemented of type %s" % type(exp)
+
+
+def secret_join(in_nodes):
+    """This is a may-analysis, so take the union"""
+    r = set()
+    for i in in_nodes:
+        r|=i.out_values["secret"]
+    return r
+
+
+def secret_combine(node, ins):
+    """
+    If this is an assignment, check if the computed expression is
+    secret, if that is the case, the assigned variable is secret as
+    well. Otherwise it becomes non-secret.
+
+    All other statements just pass their value through.
+    """
+    ins
+    if(getattr(node, "imported_secrets", False)):
+        ins = ins | node.imported_secrets
+    if(isinstance(node, ast.Assign)):
+        if(expr_secret(node.value, ins)):
+            ins = ins | set([node.targets[0].id])
+        else:
+            ins = ins - set([node.targets[0].id])
+    if(isinstance(node, ast.Expr) and
+       isinstance(node.value, ast.Call) and
+       isinstance(node.value.func, ast.Name) and
+       node.value.func.id == "mark_secret"):
+        # Todo - handle non-names...
+        ins = ins | set([i.id for i in node.value.args])
+    return ins
+
+
+def secret_analysis(function):
+    arguments = set(i.id for i in function.args.args)
+    function.body[0].imported_secrets = arguments
+    pysmcl.flow.analyze(function, secret_join, secret_combine, "secret")
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/pysmcl/secret_ifs.py	Fri May 22 16:50:47 2009 +0200
@@ -0,0 +1,109 @@
+"""
+Defines an ast-transformer *TransformIfs* finding *if*s branching on
+secret values, and transforming them into equivalent series of
+assignments
+"""
+
+import ast
+
+# Import PySMCL packages.
+from pysmcl.util import error
+import pysmcl.secret_annotator
+
+
+class Assignments(ast.NodeVisitor):
+
+    def __init__(self):
+        self.assigned={}
+
+    def visit_Assign(self, node):
+        varname = node.targets[0].id
+        if varname in self.assigned:
+            error("Error: cannot assign several times"+
+                  "to \"%s\" in a secret if" % varname, node)
+        ## TODO only single-target assignment
+        self.assigned[varname] = node.value
+
+
+def get_assignments(body):
+    visitor = Assignments()
+    [visitor.visit(i) for i in body]
+    return visitor.assigned
+
+
+def only_assignments(body):
+    for i in body:
+        if not (isinstance(i, ast.Assign) or
+                isinstance(i, ast.Pass)):
+            error("Error,\
+ inside secret if statements, we only allow \
+assignments, but found a %s." % type(i),
+                  i)
+
+
+class TransformIfs(ast.NodeTransformer):
+    """
+    >>> from ast import *
+    >>> from pysmcl.pretty_print import *
+    >>> from pysmcl.ideal_functionality import init_statements
+    >>> from pysmcl.secret_ifs import TransformIfs
+    >>> from pysmcl.secret_annotator import secret_analysis
+    >>> prog = parse("def f(x):\n\tif(x):\n\t\ta=1\n\telse:\n\t\ta=2")
+    >>> trans = TransformIfs()
+    >>> init_statements(prog)
+    >>> secret_analysis(prog.body[0])
+    >>> prog = trans.visit(prog)
+    >>> pprint(prog)
+    def f(x):
+        cond0 = x
+        a = cond0 * 1 + (1 - cond0) * 2
+
+    """
+    cond_counter = 0
+
+    def __init__(self):
+        self.changed = False
+
+    def reset(self):
+        self.changed = False
+
+    def visit_While(self, node):
+        if(pysmcl.secret_annotator.expr_secret(node.test, node.in_values["secret"])):
+            error("While is not possible on a secret value", node)
+        return node
+
+    def visit_If(self, node):
+        if(pysmcl.secret_annotator.expr_secret(node.test, node.in_values["secret"])):
+            self.changed = True
+
+            only_assignments(node.body)
+            assigned_then = get_assignments(node.body)
+            assigned_else = get_assignments(node.orelse)
+            all_assigned = set(assigned_then.keys() + assigned_else.keys())
+            r = []
+            # Todo: correct gensyms
+            condname = ast.Name(id="cond%d" % self.cond_counter)
+            self.cond_counter += 1
+            r.append(ast.Assign(targets=[condname],
+                                value=node.test))
+            for i in all_assigned:
+                then_value = assigned_then.get(i, ast.Name(id=i))
+                else_value = assigned_else.get(i, ast.Name(id=i))
+                r.append(ast.Assign(targets=[ast.Name(id=i)], value=
+                                    ast.BinOp(left=
+                                              ast.BinOp(left=condname,
+                                                        op=ast.Mult(),
+                                                        right=then_value),
+                                              op=ast.Add(),
+                                              right=
+                                              ast.BinOp(left=
+                                                        ast.BinOp(left=
+                                                                  ast.Num(1),
+                                                                  op=ast.Sub(),
+                                                                  right=
+                                                                  condname),
+                                                        op=ast.Mult(),
+                                                        right=else_value))))
+            return r # A list of statements will be merged into the list
+        else:
+            return node
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/pysmcl/test/unit/doctests.py	Fri May 22 16:50:47 2009 +0200
@@ -0,0 +1,8 @@
+
+from doctest import testfile
+
+for i in ["../../secret_ifs.py",
+          "../../pretty_print.py"]:
+    testfile(i)
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/pysmcl/test/unit/test.py	Fri May 22 16:50:47 2009 +0200
@@ -0,0 +1,32 @@
+
+from pysmcl.ideal_functionality import ideal_functionality
+
+#@proof_burden
+#@ideal_functionality
+def a(c):
+    precondition("c == 5")
+    y = 4
+    a = open(c)
+    if(c>c):
+        pass
+    else:
+        y = 3
+
+
+@ideal_functionality
+def auction(bids):
+    precondition("a >= b <=> bids[a] >= bids[b]")
+    precondition("0 >= bids[0]")
+    precondition("bids[len(bids)-1] >= 0")
+    low = 0
+    high = len(bids)
+    while(low < high):
+        invariant("bids[high] >= 0 && 0 >= bids[low]")
+        mid = (low + high) // 2
+        r = open(bids[mid] >= 0)
+        if r:
+            high = mid
+        else:
+            low = mid
+    result(mid)
+    return mid
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/pysmcl/util.py	Fri May 22 16:50:47 2009 +0200
@@ -0,0 +1,11 @@
+""" Utilities for the static analysis tool
+"""
+
+def error(msg, loc=None):
+    """Print the error message.
+    *loc* is an ast-node at the given location."""
+    loc_tuple = (loc.lineno, loc.col_offset)
+    print ast.dump(loc)
+    if loc:
+        print "at %s" % (loc_tuple, ),
+    print msg
--- a/secret_annotator.py	Fri May 22 16:32:37 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,84 +0,0 @@
-import util
-import ast
-import flow
-
-
-def expr_secret(exp, secret_variables):
-    """
-    Returns True if the expression exp should be considered secret
-    given that the variables in *secret_variables* are secret.
-    """
-    non_compromising_functions = set(["len", "open", "result"])
-    if(isinstance(exp, ast.BoolOp)):
-        return (expr_secret(exp.values[0], secret_variables)
-                 or expr_secret(exp.values[1], secret_variables))
-    elif(isinstance(exp, ast.BinOp)):
-        return (expr_secret(exp.left, secret_variables)
-                 or expr_secret(exp.right, secret_variables))
-    elif(isinstance(exp, ast.Compare)):
-        return (expr_secret(exp.left, secret_variables)
-                or expr_secret(exp.comparators[0], secret_variables))
-    elif(isinstance(exp, ast.UnaryOp)):
-            return (expr_secret(exp.operand, secret_variables))
-    elif(isinstance(exp, ast.Dict)):
-        return any([expr_secret(i, secret_variables) for i in exp.values])
-    elif(isinstance(exp, ast.Name)):
-        return exp.id in secret_variables
-    elif(isinstance(exp, ast.Num)):
-        return False
-    elif(isinstance(exp, ast.Call)):
-        if(not isinstance(exp.func, ast.Name)):
-            if(any([expr_secret(i, secret_variables) for i in exp.args])):
-                util.error("Call of non-fixed function with secret argument",
-                           exp)
-        if(exp.func.id in non_compromising_functions):
-            return False
-        func = eval(exp.func.id)
-        if(func.secret):
-            return True
-        elif(any([expr_secret(i, secret_variables) for i in exp.args])):
-            util.error("Call of non-secret\
- function with secret argument", exp)
-        else:
-            return True # For now
-    else:
-        assert False, "Not implemented of type %s" % type(exp)
-
-
-def secret_join(in_nodes):
-    """This is a may-analysis, so take the union"""
-    r = set()
-    for i in in_nodes:
-        r|=i.out_values["secret"]
-    return r
-
-
-def secret_combine(node, ins):
-    """
-    If this is an assignment, check if the computed expression is
-    secret, if that is the case, the assigned variable is secret as
-    well. Otherwise it becomes non-secret.
-
-    All other statements just pass their value through.
-    """
-    ins
-    if(getattr(node, "imported_secrets", False)):
-        ins = ins | node.imported_secrets
-    if(isinstance(node, ast.Assign)):
-        if(expr_secret(node.value, ins)):
-            ins = ins | set([node.targets[0].id])
-        else:
-            ins = ins - set([node.targets[0].id])
-    if(isinstance(node, ast.Expr) and
-       isinstance(node.value, ast.Call) and
-       isinstance(node.value.func, ast.Name) and
-       node.value.func.id == "mark_secret"):
-        # Todo - handle non-names...
-        ins = ins | set([i.id for i in node.value.args])
-    return ins
-
-
-def secret_analysis(function):
-    arguments = set(i.id for i in function.args.args)
-    function.body[0].imported_secrets = arguments
-    flow.analyze(function, secret_join, secret_combine, "secret")
--- a/secret_ifs.py	Fri May 22 16:32:37 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,108 +0,0 @@
-"""
-Defines an ast-transformer *TransformIfs* finding *if*s branching on
-secret values, and transforming them into equivalent series of
-assignments
-"""
-
-import ast
-
-from util import error
-import secret_annotator
-
-
-class Assignments(ast.NodeVisitor):
-
-    def __init__(self):
-        self.assigned={}
-
-    def visit_Assign(self, node):
-        varname = node.targets[0].id
-        if varname in self.assigned:
-            error("Error: cannot assign several times"+
-                  "to \"%s\" in a secret if" % varname, node)
-        ## TODO only single-target assignment
-        self.assigned[varname] = node.value
-
-
-def get_assignments(body):
-    visitor = Assignments()
-    [visitor.visit(i) for i in body]
-    return visitor.assigned
-
-
-def only_assignments(body):
-    for i in body:
-        if not (isinstance(i, ast.Assign) or
-                isinstance(i, ast.Pass)):
-            error("Error,\
- inside secret if statements, we only allow \
-assignments, but found a %s." % type(i),
-                  i)
-
-
-class TransformIfs(ast.NodeTransformer):
-    """
-    >>> from ast import *
-    >>> from pretty_print import *
-    >>> from ideal_functionality import init_statements
-    >>> from secret_ifs import TransformIfs
-    >>> from secret_annotator import secret_analysis
-    >>> prog = parse("def f(x):\n\tif(x):\n\t\ta=1\n\telse:\n\t\ta=2")
-    >>> trans = TransformIfs()
-    >>> init_statements(prog)
-    >>> secret_analysis(prog.body[0])
-    >>> prog = trans.visit(prog)
-    >>> pprint(prog)
-    def f(x):
-        cond0 = x
-        a = cond0 * 1 + (1 - cond0) * 2
-
-    """
-    cond_counter = 0
-
-    def __init__(self):
-        self.changed = False
-
-    def reset(self):
-        self.changed = False
-
-    def visit_While(self, node):
-        if(secret_annotator.expr_secret(node.test, node.in_values["secret"])):
-            error("While is not possible on a secret value", node)
-        return node
-
-    def visit_If(self, node):
-        if(secret_annotator.expr_secret(node.test, node.in_values["secret"])):
-            self.changed = True
-
-            only_assignments(node.body)
-            assigned_then = get_assignments(node.body)
-            assigned_else = get_assignments(node.orelse)
-            all_assigned = set(assigned_then.keys() + assigned_else.keys())
-            r = []
-            # Todo: correct gensyms
-            condname = ast.Name(id="cond%d" % self.cond_counter)
-            self.cond_counter += 1
-            r.append(ast.Assign(targets=[condname],
-                                value=node.test))
-            for i in all_assigned:
-                then_value = assigned_then.get(i, ast.Name(id=i))
-                else_value = assigned_else.get(i, ast.Name(id=i))
-                r.append(ast.Assign(targets=[ast.Name(id=i)], value=
-                                    ast.BinOp(left=
-                                              ast.BinOp(left=condname,
-                                                        op=ast.Mult(),
-                                                        right=then_value),
-                                              op=ast.Add(),
-                                              right=
-                                              ast.BinOp(left=
-                                                        ast.BinOp(left=
-                                                                  ast.Num(1),
-                                                                  op=ast.Sub(),
-                                                                  right=
-                                                                  condname),
-                                                        op=ast.Mult(),
-                                                        right=else_value))))
-            return r # A list of statements will be merged into the list
-        else:
-            return node
--- a/test.py	Fri May 22 16:32:37 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-from ideal_functionality import ideal_functionality
-
-#@proof_burden
-#@ideal_functionality
-def a(c):
-    precondition("c == 5")
-    y = 4
-    a = open(c)
-    if(c>c):
-        pass
-    else:
-        y = 3
-
-
-@ideal_functionality
-def auction(bids):
-    precondition("a >= b <=> bids[a] >= bids[b]")
-    precondition("0 >= bids[0]")
-    precondition("bids[len(bids)-1] >= 0")
-    low = 0
-    high = len(bids)
-    while(low < high):
-        invariant("bids[high] >= 0 && 0 >= bids[low]")
-        mid = (low + high) // 2
-        r = open(bids[mid] >= 0)
-        if r:
-            high = mid
-        else:
-            low = mid
-    result(mid)
-    return mid
--- a/util.py	Fri May 22 16:32:37 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-""" Utilities for the static analysis tool
-"""
-
-def error(msg, loc=None):
-    """Print the error message.
-    *loc* is an ast-node at the given location."""
-    loc_tuple = (loc.lineno, loc.col_offset)
-    print ast.dump(loc)
-    if loc:
-        print "at %s" % (loc_tuple, ),
-    print msg