Closures call slots: First analysis implementation #92

BenWeber42 · 2017-09-26T16:06:22Z

This change is

marcoeilers

Looks pretty good overall

marcoeilers · 2017-09-29T10:13:51Z

src/nagini_contracts/contracts.py

+    Decorator to mark a method as a call slot declaration.
+    """
+
+    def call_slot_handler(*args, **kwargs) -> Any:


Do you need this code here? Is it supposed to be an example usage or... what?

This code is needed for normal runs (without the verifier). It makes sure no code is run when Python comes accross a call slot application.
The way it works is that whenever there is a '@CallSlot' decorator on a function, that function will be replaced with 'call_slot_handler'. 'call_slot_handler' does nothing, but has to support both calls call_slot_handler(...) and call_slot_handler(...)(<<uq vars>>) (the latter is supported through the 'uq_handler').

Ah okay. It's fine to assume that there'll be some postprocessing to take the annotations out though; if it's any effort at all, you shouldn't have to worry about this, as long as you make sure that there's enough information in the annotated code to enable the postprocessing.

marcoeilers · 2017-09-29T10:15:04Z

src/nagini_contracts/contracts.py

+
+def ClosureCall(call: Any, justification: Any) -> Any:
+    """
+    Justifies a closure call by proving static dispatch (in contrast to using


Not quite sure I agree with the description here. What does "proving static dispatch" mean?

marcoeilers · 2017-09-29T10:18:38Z

src/nagini_translation/analyzer.py

@@ -453,6 +457,12 @@ 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)


This means that you create a new CallSlotAnalyzer for every call slot, right? Is that necessary?

Changed to reusing the same CallSlotAnalyzer in the Analyzer class.

marcoeilers · 2017-09-29T10:19:36Z

src/nagini_translation/analyzer.py

@@ -52,6 +52,7 @@
 )
 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


I'd have said from nagini_translation.call_slot_analyzers import CallSlotAnalyzer, CallSlotProofAnalyzer

Sounds good.

marcoeilers · 2017-09-29T10:28:44Z

src/nagini_translation/call_slot_analyzers.py

@@ -0,0 +1,280 @@
+import ast
+from typing import Union
+from nagini_translation import analyzer as analyzer_pkg


If you only need this for type annotations, I wouldn't bother, I would just write 'Analyzer' in the annotation. We're not using a type checker anyway, so it's only for documentation purposes, and it's clear what it refers to.

marcoeilers · 2017-09-29T11:23:22Z

src/nagini_translation/call_slot_analyzers.py

+            analyzer.outer_functions.pop()
+        analyzer.current_function = None
+
+    def _check_body(self, body):


Type annotations would be nice

marcoeilers · 2017-09-29T11:24:31Z

src/nagini_translation/call_slot_analyzers.py

+                self._check_call_declaration(child.value)
+
+            elif isinstance(child, ast.Assign):
+                self._check_call_declaration(child)


Does this work for methods that don't return anything? I guess it's possible that there are no target variables, right?

This should be handled by the if body above. If there are no target variables it shouldn't be an assignment, but an ast.Expr.

https://greentreesnakes.readthedocs.io/en/latest/nodes.html#Expr

Ah yeah, I overlooked that somehow.

marcoeilers · 2017-09-29T11:26:51Z

src/nagini_translation/call_slot_analyzers.py

+
+            assert len(node.targets) == 1
+
+            if isinstance(node.targets[0], ast.Name):


I think it would be fine, at the very least initially, to make your life a bit easier and require that you have at most one, normal target. Then you can replace that directly with Result in the generated method.

I think I'll try to support 'simple tuples' (without nesting) for now. It seems simple enough but should also cover the majority of use cases.

Fine by me, but if you drop anything for time reasons, this kind of stuff (syntactic niceties) would be the first thing I'd drop.

Changed as discussed in our last meeting (change not pushed yet).

marcoeilers · 2017-09-29T11:28:32Z

src/nagini_translation/call_slot_analyzers.py

+            ("Method '%s' contains illegal keyword parameters"
+                % method.node.name)
+        )
+    # TODO: what about defaults?


I'd forbid using defaults

Sounds good.

marcoeilers · 2017-09-29T11:29:27Z

src/nagini_translation/conftest.py

@@ -20,6 +20,7 @@
 _SIF_TESTS_DIR = 'tests/sif/'
 _IO_TESTS_DIR = 'tests/io/'
 _OBLIGATIONS_TESTS_DIR = 'tests/obligations/'
+_CLOSURES_TESTS_DIR = 'tests/closures/'


Great, this is all really neat. Nice.

First attempt through an external 'CallSlotAnalyzer'. Might not work so well, might need to modify the Analyzer directly.

Progressed with CallSlotAnalyzer

marcoeilers · 2017-10-11T23:30:29Z

src/nagini_translation/analyzer.py

@@ -731,6 +733,8 @@ def visit_Call(self, node: ast.Call) -> None:
        Collects preconditions, postconditions, raised exceptions and
        invariants.
        """
+        if is_closure_call(node):
+            check_closure_call(node)


Could probably return after this?

marcoeilers · 2017-10-11T23:31:04Z

src/nagini_translation/analyzer.py

+                    var = self.module.global_vars[node.id]
+                    self.track_access(node, var)
+                elif not node.id in self.module.methods:
+                    # Node is neither a global variable nor a global method


When can this happen?

marcoeilers · 2017-10-11T23:33:16Z

src/nagini_translation/call_slot_analyzers.py

@@ -1,95 +1,292 @@
 import ast
-from typing import Union, List
+from typing import Union, List, Set


Generally we sort imports alphabetically. First all import statements, then all from ... import ... statements, sorted by the name of the module, and then the imported names sorted by name.

marcoeilers · 2017-10-11T23:37:39Z

src/nagini_translation/call_slot_analyzers.py

+                "Illegal reference to non-local name '%s'" % illegal_variable_uses[0].id
+            )
+
+    class _AllowedVariablesChecker(ast.NodeVisitor):


Does this have to be a nested class?

marcoeilers · 2017-10-11T23:40:30Z

src/nagini_translation/call_slot_analyzers.py

+        set correctly.
+
+        * No magic name ('__...__')
+        * Return type = None


Is there a reason why we need to enforce this return type?

marcoeilers · 2017-10-11T23:56:07Z

src/nagini_translation/call_slot_analyzers.py

+                'call_slots.call_declaration.invalid_target',
+                "Callslot '%s' has an invalid call target" % self.call_slot.node.name
+            )
+        if call.func.id not in self.call_slot.args:


It doesn't seem like you need two different cases for this.

marcoeilers · 2017-10-11T23:57:47Z

src/nagini_translation/call_slot_analyzers.py


+        self.call_slot = self.analyzer.node_factory.create_call_slot_proof(


It's a bit weird that you store a proof object in a field called call_slot

marcoeilers · 2017-10-12T00:01:32Z

src/nagini_translation/call_slot_analyzers.py

+                elif (
+                    len(self.call_slot.return_variables) != 1 or
+                    self.call_slot.return_variables[0].id != node.targets[0].id
+                ):


This looks.... weird. I'm not sure how to do it instead, but to me, this looks weird.

marcoeilers · 2017-10-12T00:05:30Z

src/nagini_translation/call_slot_analyzers.py

+                "ClosureCall's justification has to instatiate uq variables if it's a call slot"
+            )
+
+        if not isinstance(justification.func.func, ast.Name):


I'm not sure if that would already work at this point (maybe you're still building up the necessary data structures), but in principle, you should be able to say get_target(justification) and make sure that it gives you e.g. a PythonMethod or a CallSlot object. Then you don't have to bother with checking that it uses an ast.Name etc.

marcoeilers · 2017-10-12T00:10:07Z

tests/closures/translation/closure_call/test_simple.py

+F_Type = Callable[[int, int], int]
+
+
+#:: IgnoreFile(42)


IIRC the number here should refer to an issue in the issue tracker because of which this file should be ignored. If this one isn't ready yet and depends on not-yet-implemented features, IMO the test just shouldn't be in the PR yet.

Also, IgnoreFile should generally be at the top of the file, and this seems like it should eventually be a verification test, not a translation test.

BenWeber42 requested a review from marcoeilers September 26, 2017 16:08

marcoeilers reviewed Sep 29, 2017

View reviewed changes

BenWeber42 force-pushed the closures_call_slots branch from f1406f0 to 3222cc0 Compare September 30, 2017 16:26

BenWeber42 added 8 commits September 30, 2017 18:28

Added call slot annotations to nagini_contracts

c0f605c

Started modifying the Analyzer for call slots

8b15121

First attempt through an external 'CallSlotAnalyzer'. Might not work so well, might need to modify the Analyzer directly.

Progressed with call slot analyzer

a94c5a4

Updated contracts for new ClosureCall syntax and __all__ bugfix

d409705

Enabled Callable types in TypeVisitor

6b0c529

Progressed with analyzation stage of call slots

ff68f77

Added 'closures' test suite to test framework

edf787f

Added method_name_collision test

816de82

BenWeber42 force-pushed the closures_call_slots branch from 3222cc0 to f03106f Compare September 30, 2017 17:24

BenWeber42 added 2 commits September 30, 2017 22:08

Changes from PR

fde4d72

Patch to make debugging with pdb better

2f55236

BenWeber42 force-pushed the closures_call_slots branch from f03106f to 2f55236 Compare September 30, 2017 20:08

BenWeber42 added 4 commits October 2, 2017 22:37

Progressed with CallSlotAnalyzer

c90cdce

Added more tests

e9ae8b4

Added CallSlotProofAnalyzer & check_closure_call

273d926

Progressed with CallSlotAnalyzer

Added more tests for call slots

9720119

marcoeilers reviewed Oct 12, 2017

View reviewed changes

BenWeber42 added 10 commits October 13, 2017 15:54

Removed local variables check inside call slot proofs

01d3193

Added example a from the project description to the tests

b07399f

Fixed a typing error in a test case

b74779d

Progressed with translation of call slots

6f7c156

Fixed the static code example

e24e4c7

First version that can translate the static code example

6ce2752

Finished minimal implementation for static code example

cf8a64e

Implemented Old expressions

11afaeb

Activated all tests and added basic old expressions test

a0ce593

First version of pure call slots

5427ebe

BenWeber42 and others added 8 commits October 21, 2017 17:30

Minor bugfix in translate_Return

6ba95f4

Added pure test and example b from the project description

979f66c

Some bugfixes

e8bf2a5

Added pure, while loop and n times examples

67539a1

Minor changes to the tests

1d46890

Adapted to Viper changes

55053ce

Attempted merge

53d787d

Fixed some things

29ee893

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Closures call slots: First analysis implementation #92

Closures call slots: First analysis implementation #92

BenWeber42 commented Sep 26, 2017 •

edited by marcoeilers

Loading

marcoeilers left a comment

marcoeilers Sep 29, 2017

BenWeber42 Sep 30, 2017

marcoeilers Oct 2, 2017

marcoeilers Sep 29, 2017

BenWeber42 Sep 30, 2017

marcoeilers Sep 29, 2017

BenWeber42 Sep 30, 2017

marcoeilers Sep 29, 2017

BenWeber42 Sep 30, 2017

marcoeilers Sep 29, 2017

BenWeber42 Sep 30, 2017

marcoeilers Sep 29, 2017

BenWeber42 Sep 30, 2017

marcoeilers Sep 29, 2017

BenWeber42 Sep 30, 2017

marcoeilers Oct 2, 2017

marcoeilers Sep 29, 2017

BenWeber42 Sep 30, 2017

marcoeilers Oct 2, 2017

BenWeber42 Oct 4, 2017

marcoeilers Sep 29, 2017

BenWeber42 Sep 30, 2017

marcoeilers Sep 29, 2017

marcoeilers Oct 11, 2017

marcoeilers Oct 11, 2017

marcoeilers Oct 11, 2017

marcoeilers Oct 11, 2017

marcoeilers Oct 11, 2017

marcoeilers Oct 11, 2017

marcoeilers Oct 11, 2017

marcoeilers Oct 12, 2017

marcoeilers Oct 12, 2017

marcoeilers Oct 12, 2017


		assert len(node.targets) == 1

		if isinstance(node.targets[0], ast.Name):


		self.call_slot = self.analyzer.node_factory.create_call_slot_proof(

Closures call slots: First analysis implementation #92

Are you sure you want to change the base?

Closures call slots: First analysis implementation #92

Conversation

BenWeber42 commented Sep 26, 2017 • edited by marcoeilers Loading

marcoeilers left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

BenWeber42 commented Sep 26, 2017 •

edited by marcoeilers

Loading