Changes from PR

src/nagini_contracts/contracts.py

@@ -303,8 +303,9 @@ def CallSlotProof(call_slot: Callable[..., Any]) -> Callable[[Callable[..., None
 
 def ClosureCall(call: Any, justification: Any) -> Any:
     """
-    Justifies a closure call by proving static dispatch (in contrast to using
-    a call slot).
+    Justifies a closure call through either
+     * a CallSlot (justification == the callslot instance)
+     * proofing static dispatch (justification == the static method)
     """
     pass
 

src/nagini_translation/analyzer.py

@@ -52,7 +52,12 @@
 )
 from nagini_translation.lib.views import PythonModuleView
 from typing import Any, Callable, Dict, List, Optional, Set, Tuple, Union
-from nagini_translation import call_slot_analyzers
+from nagini_translation.call_slot_analyzers import (
+    CallSlotAnalyzer,
+    is_call_slot,
+    CallSlotProofAnalyzer,
+    is_call_slot_proof
+)
 
 
 logger = logging.getLogger('nagini_translation.analyzer')
@@ -86,6 +91,8 @@ def __init__(self, types: TypeInfo, path: str, selected: Set[str]):
         self._aliases = {}  # Dict[str, PythonBaseVar]
         self.current_loop_invariant = None
         self.selected = selected
+        self.call_slot_analyzer = CallSlotAnalyzer(self)
+        self.call_slot_proof_analyzer = CallSlotProofAnalyzer(self)
 
     @property
     def node_factory(self):
@@ -457,11 +464,11 @@ def _is_illegal_magic_method_name(self, name: str) -> bool:
         return False
 
     def visit_FunctionDef(self, node: ast.FunctionDef) -> None:
-        if call_slot_analyzers.is_call_slot(node):
-            call_slot_analyzers.CallSlotAnalyzer(self).analyze(node)
+        if is_call_slot(node):
+            self.call_slot_analyzer.analyze(node)
             return
-        if call_slot_analyzers.is_call_slot_proof(node):
-            call_slot_analyzers.CallSlotProofAnalyzer(self).analyze(node)
+        if is_call_slot_proof(node):
+            self.call_slot_proof_analyzer.analyze(node)
             return
         if self.current_function:
             raise UnsupportedException(node, 'nested function declaration')

src/nagini_translation/call_slot_analyzers.py

@@ -1,10 +1,8 @@
 import ast
-from typing import Union
-from nagini_translation import analyzer as analyzer_pkg
+from typing import Union, List
 from nagini_translation.lib.program_nodes import (
     PythonModule,
-    PythonMethod,
-    CallSlot
+    PythonMethod
 )
 from nagini_translation.lib.util import (
     UnsupportedException,
@@ -14,7 +12,7 @@
 
 class CallSlotAnalyzer:
 
-    def __init__(self, analyzer: 'analyzer_pkg.Analyzer') -> None:
+    def __init__(self, analyzer: 'Analyzer') -> None:
         self.analyzer = analyzer
         self.call_slot = None  # type: CallSlot
 
@@ -90,7 +88,7 @@ def analyze(self, node: ast.FunctionDef) -> None:
             analyzer.outer_functions.pop()
         analyzer.current_function = None
 
-    def _check_body(self, body):
+    def _check_body(self, body: List[ast.stmt]):
         self.has_call = False
         for child in body:
 
@@ -140,8 +138,17 @@ def _check_call_declaration(self, node: Union[ast.Call, ast.Assign]) -> None:
             if isinstance(node.targets[0], ast.Name):
                 self.call_slot.return_variables = [node.targets[0]]
             elif isinstance(node.targets[0], ast.Tuple):
-                # FIXME: doesn't work with nested destructuring
+
+                # NOTE: could add support for nested destructuring
                 # e.g., `a, (b, c), d = f(1, 2, 3)`
+                # currently we only support simple tuple assignments
+                for target in node.targets[0].elts:
+                    if not isinstance(target, ast.Name):
+                        raise UnsupportedException(
+                            target,
+                            "Callslots only support simple tuple assignments"
+                        )
+
                 self.call_slot.return_variables = node.targets[0].elts
             else:
                 raise UnsupportedException(
@@ -178,6 +185,25 @@ def analyze(self, node: ast.FunctionDef) -> None:
         pass  # FIXME: implement
 
 
+class _LimitedVariablesChecker(ast.NodeVisitor):
+
+    def __init__(self, variables: List[str]) -> None:
+        self.variables = variables
+        self.offending_nodes = []  # type: List
+
+    def check_name(self, name: str) -> None:
+        if name.id not in self.variables:
+            self.offending_nodes.append(name)
+
+    def visit_Name(self, name: ast.Name) -> None:
+        self.check_name(name.id)
+        self.generic_visit(name)
+
+    # TODO: check other node types
+    # ast.Arg for lambdas
+    # ast.Call for calls (?)
+
+
 def _check_method_declaration(method: PythonMethod, analyzer: 'analyzer_pkg.Analyzer') -> None:
     """
     Checks whether `node' is a method declaration valid for a call slot or
@@ -204,6 +230,13 @@ def _check_method_declaration(method: PythonMethod, analyzer: 'analyzer_pkg.Anal
             "Method '%s' doesn't return 'None'" % method.node.name
         )
 
+    if 0 < len(method.node.args.defaults):
+        raise InvalidProgramException(
+            method.node.args.defaults[0],
+            'call_slots.parameters.default',
+            "Method '%s' has a default parameter" % method.node.name
+        )
+
     analyzer.visit(method.node.args, method.node)
 
     if method.var_arg is not None:
@@ -221,7 +254,6 @@ def _check_method_declaration(method: PythonMethod, analyzer: 'analyzer_pkg.Anal
             ("Method '%s' contains illegal keyword parameters"
                 % method.node.name)
         )
-    # TODO: what about defaults?
 
 
 def _is_uq_vars(body) -> bool: