From 3222cc00d14100478a4d5f7743ee8b800f7f7932 Mon Sep 17 00:00:00 2001 From: Ben Weber Date: Sat, 30 Sep 2017 18:03:38 +0200 Subject: [PATCH] Changes from PR --- src/nagini_contracts/contracts.py | 5 +- src/nagini_translation/analyzer.py | 17 +++++-- src/nagini_translation/call_slot_analyzers.py | 48 +++++++++++++++---- 3 files changed, 55 insertions(+), 15 deletions(-) diff --git a/src/nagini_contracts/contracts.py b/src/nagini_contracts/contracts.py index c00d1fcb..82e29950 100644 --- a/src/nagini_contracts/contracts.py +++ b/src/nagini_contracts/contracts.py @@ -288,8 +288,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 diff --git a/src/nagini_translation/analyzer.py b/src/nagini_translation/analyzer.py index ea44fe2b..c74d33f4 100644 --- a/src/nagini_translation/analyzer.py +++ b/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') diff --git a/src/nagini_translation/call_slot_analyzers.py b/src/nagini_translation/call_slot_analyzers.py index 59f56cfa..c61d3079 100644 --- a/src/nagini_translation/call_slot_analyzers.py +++ b/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: