changeset 123:7b2b7c4f30c8

Merged with Sigurd.
author Thomas P Jakobsen <tpj@cs.au.dk>
date Mon, 26 Oct 2009 10:39:51 +0100
parents 562d1041a7b9 (current diff) e40f75de788d (diff)
children 035b670967c6
files
diffstat 5 files changed, 413 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- a/examples/while-loop.py	Mon Oct 26 10:34:45 2009 +0100
+++ b/examples/while-loop.py	Mon Oct 26 10:39:51 2009 +0100
@@ -1,17 +1,5 @@
-
 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):
@@ -21,12 +9,12 @@
     low = 0
     high = len(bids)
     while(low < high):
-        invariant("bids[high] >= 0 && 0 >= bids[low]")
+        invariant("bids[high] >= 0 and 0 >= bids[low]")
         mid = (low + high) // 2
         r = open(bids[mid] >= 0)
         if r:
             high = mid
         else:
-            low = mid
+            low = mid+1
     result(mid)
     return mid
--- a/pysmcl/emacs/info.py	Mon Oct 26 10:34:45 2009 +0100
+++ b/pysmcl/emacs/info.py	Mon Oct 26 10:39:51 2009 +0100
@@ -8,7 +8,6 @@
 def main():
     prog = ast.parse(file(sys.argv[1]).read())
     linenr = int(sys.argv[2]) if len(sys.argv) > 2 else 0
-    print "("
     for i in prog.body:
         if isinstance(i, ast.FunctionDef):
             secret_analysis(i)
@@ -18,13 +17,10 @@
                 if isinstance(j, ast.stmt):
                     e = j.out_values["secret"]
                 if isinstance(j, ast.expr):
-                    try:
-                        if expr_secret(j, e):
-                            output = StringIO.StringIO()
-                            print "(%d %d %d)" % (j.lineno, j.col_offset,
-                                                  len(expr_string(j)))
-                    except:
-                        pass
-    print ")"
+                    if expr_secret(j, e):
+                        output = StringIO.StringIO()
+                        print "%d %d %d" % (j.lineno, j.col_offset,
+                                              len(expr_string(j)))
+
 if __name__ == "__main__":
     main()
--- a/pysmcl/pretty_print.py	Mon Oct 26 10:34:45 2009 +0100
+++ b/pysmcl/pretty_print.py	Mon Oct 26 10:39:51 2009 +0100
@@ -209,7 +209,7 @@
         my_precedence = 1
         r = exp.id
     else:
-        print exp, isinstance(exp, _ast.Name)
+        print exp, isinstance(exp, ast.Name)
         assert False, "Not implemented of type %s" % type(exp)
 
     if my_precedence <= prec:
--- a/pysmcl/secret_annotator.py	Mon Oct 26 10:34:45 2009 +0100
+++ b/pysmcl/secret_annotator.py	Mon Oct 26 10:39:51 2009 +0100
@@ -38,6 +38,8 @@
             return True # but bad_calls will warn us
     elif isinstance(exp, ast.Str):
         return False
+    elif isinstance(exp, ast.Subscript):
+        return expr_secret(exp.value, secret_variables)
     else:
         assert False, "Not implemented of type %s" % type(exp)
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/pysmcl/simpl_print.py	Mon Oct 26 10:39:51 2009 +0100
@@ -0,0 +1,403 @@
+"""
+Pretty printing of the Python built-in ast-type as a program in the
+Simpl language embedded into Isabelle/HOL.
+
+The goal is to print a program with the exact same semantics as the
+program parsed into the ast.
+"""
+
+import ast
+import sys
+
+
+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 parameter_string(arguments):
+    """ Like the argument list, but followed by | RET_VAL
+    """
+    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 + "| RET_VAL::nat)"
+
+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: "div",
+           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 *
+    >>> import StringIO
+    >>> 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 = "\\<acute>"+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 = "CALL %s(%s)" % \
+            (exp.func.id,
+             ", ".join(args_list))
+    elif(isinstance(exp, dict)):
+        print >>output, 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
+    elif(isinstance(exp, ast.Tuple)):
+        my_precedence = 25
+        r = "("+", ".join(["%s" % (expr_string(i)) for i in exp.elts])+")"
+    elif(isinstance(exp, ast.Name)):
+        my_precedence = 1
+        r = exp.id
+    else:
+        print exp, isinstance(exp, _ast.Name)
+        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 __init__(self, output = sys.stdout):
+        self.output = output
+
+    def print_body(self, body):
+        self.indent += 1
+        self.last_statement = False
+        for i in body[:-1]:
+            self.visit(i)
+        self.last_statement = True
+        self.visit(body[-1])
+        self.indent -= 1
+
+    def print_indented(self, str):
+        print >>self.output, (" "*(self.indent*4))+str
+
+    def print_statement(self, str):
+        print >>self.output, (" "*(self.indent*4))+str,
+        if not self.last_statement:
+            print ";;"
+        else:
+            print
+
+    def visit_Return(self, node):
+        self.print_statement("\\<acute>RET_VAL :== %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_statement("%s :== %s" % (expr_string(node.targets[0]),
+                                         expr_string(node.value)))
+
+    def visit_AugAssign(self, node):
+        self.print_statement("%s = %s %s %s" %
+                            (expr_string(node.target),
+                             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_statement("print %s" % \
+                               (", ".join([expr_string(i)
+                                           for i in node.values])))
+
+    def visit_For(self, node):
+        self.print_statement("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) DO" % expr_string(node.test))
+        self.print_body(node.body)
+#        if(len(node.orelse)>0):
+#            self.print_indented("else:")
+#            self.print_body(node.orelse)
+        self.print_statement("OD")
+
+    def visit_If(self, node):
+        self.print_indented("IF (%s) THEN" % expr_string(node.test))
+        self.print_body(node.body)
+        if(len(node.orelse)>0):
+            self.print_indented("ELSE")
+            self.print_body(node.orelse)
+        self.print_statement("FI")
+
+    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_statement(expr_string(node.value))
+
+    def visit_Pass(self, node):
+        self.print_statement("SKIP")
+
+    def visit_Break(self, node):
+        self.print_statement("BREAK")
+
+    def visit_Continue(self, node):
+        self.print_statement("CONTINUE")
+
+    def visit_FunctionDef(self, node):
+#        for i in node.decorator_list:
+#            self.print_indented("@%s" % expr_string(i))
+        self.print_indented("procedures")
+        self.indent += 1
+        self.print_indented("%s%s" % (node.name,
+                                       parameter_string(node.args)))
+        self.print_body(node.body)
+        self.indent -= 1
+
+
+def pprint(module, output=sys.stdout):
+    """Pretty prints the module represented by the ast node in
+    ***module***
+    """
+    PrettyPrinter(output).visit(module)