changeset 342:d67f0bb6aeeb

proof_burden: now proof-burdens are flow-dependent Only results that are visible from the output are given for simulating the values of outputs
author Sigurd Meldgaard <stm@daimi.au.dk>
date Wed, 07 Jul 2010 16:11:11 +0200
parents f02368b0944e
children ebbb77e339f8
files pysmcl/proof_burden.py
diffstat 1 files changed, 54 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/pysmcl/proof_burden.py	Wed Jul 07 14:33:30 2010 +0200
+++ b/pysmcl/proof_burden.py	Wed Jul 07 16:11:11 2010 +0200
@@ -1,21 +1,13 @@
 import pysmcl.ast_wrapper as ast
 import pysmcl.pretty_print
+import pysmcl.flow as flow
 import sys
 
 
-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, output):
         self.openings = []
-        self.results = []
         self.output = output
 
     def visit_While(self, node):
@@ -25,8 +17,6 @@
         if isinstance(node.func, ast.Name):
             if node.func.id == "output":
                 self.openings.append(node.args[0])
-            if node.func.id == "result":
-                self.results.append(node.args[0])
             elif node.func.id == "precondition":
                 print >>self.output, "  You can assume: " + (node.args[0].s)
             elif node.func.id == "invariant":
@@ -34,21 +24,67 @@
                 print >>self.output, (node.args[0].s)
 
 
+key = "available_results"
+
+
+def analyze_proof_burden(f):
+
+    def find_x_calls(stm, needle):
+        x = []
+        for i in ast.walk(stm):
+            if(isinstance(i, ast.Call)
+               and isinstance(i.func, ast.Name)
+               and i.func.id == needle):
+                x.append(i)
+        return x
+
+    def find_results(stm):
+        return find_x_calls(stm, "result")
+
+    def find_inputs(stm):
+        return find_x_calls(stm, "input")
+
+    init = frozenset(find_results(f)) # We can at most find every
+                                      # result-statement of the
+                                      # function
+    def join(children):
+        """
+        We take the intersection of the available results from the
+        children, because only results that are available in all
+        futures are available for the simulation of the output'ted
+        value.
+        """
+        if not children:
+            return frozenset()
+        return reduce(lambda x, y: x & y.out_values[key], children, init)
+
+    def combine(node, env):
+        if find_inputs(node):
+            return frozenset()
+        new_results = find_results(node)
+        return frozenset(new_results) | env
+
+    flow.analyze(f, join, combine, key, init,
+                 forward=False)
+
+
 def proof_burden(f, output=sys.stdout):
-    b = ProofBurden(output)
     print >>output, "For the function: " + f.name
+    analyze_proof_burden(f)
+    b = ProofBurden(output)
     b.visit(f)
-    if b.openings!=[]:
+    if b.openings:
         print >>output, " Show that you can compute:"
         for i in b.openings:
             print >>output, ("  The value of "
                              + pysmcl.pretty_print.expr_string(i)
                   + " in line " + str(i.lineno))
-        print >>output, (" From:")
-        for i in b.results:
-            print >>output, ("  The value of "
-                             + pysmcl.pretty_print.expr_string(i)
-                             + " in line " + str(i.lineno))
+            print >>output, (" From:")
+            for result in ast.get_ancestor(i, ast.stmt).out_values[key]:
+                print >>output, ("  The value of "
+                                 + pysmcl.pretty_print
+                                    .expr_string(result.args[0])
+                                 + " in line " + str(result.lineno))
     else:
         print >>output, " Nothing has to be proved"
     return f