Mercurial > pysmcl
changeset 18:429e347be685
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