Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closures call slots: First analysis implementation #92

Open
wants to merge 32 commits into
base: master
Choose a base branch
from
Open
Changes from 14 commits
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
c0f605c
Added call slot annotations to nagini_contracts
BenWeber42 Sep 5, 2017
8b15121
Started modifying the Analyzer for call slots
BenWeber42 Sep 6, 2017
a94c5a4
Progressed with call slot analyzer
BenWeber42 Sep 6, 2017
d409705
Updated contracts for new ClosureCall syntax and __all__ bugfix
BenWeber42 Sep 26, 2017
6b0c529
Enabled Callable types in TypeVisitor
BenWeber42 Sep 26, 2017
ff68f77
Progressed with analyzation stage of call slots
BenWeber42 Sep 26, 2017
edf787f
Added 'closures' test suite to test framework
BenWeber42 Sep 26, 2017
816de82
Added method_name_collision test
BenWeber42 Sep 26, 2017
fde4d72
Changes from PR
BenWeber42 Sep 30, 2017
2f55236
Patch to make debugging with pdb better
BenWeber42 Sep 30, 2017
c90cdce
Progressed with CallSlotAnalyzer
BenWeber42 Oct 2, 2017
e9ae8b4
Added more tests
BenWeber42 Oct 2, 2017
273d926
Added CallSlotProofAnalyzer & check_closure_call
BenWeber42 Oct 11, 2017
9720119
Added more tests for call slots
BenWeber42 Oct 11, 2017
01d3193
Removed local variables check inside call slot proofs
BenWeber42 Oct 13, 2017
b07399f
Added example a from the project description to the tests
BenWeber42 Oct 15, 2017
b74779d
Fixed a typing error in a test case
BenWeber42 Oct 15, 2017
6f7c156
Progressed with translation of call slots
BenWeber42 Oct 15, 2017
e24e4c7
Fixed the static code example
BenWeber42 Oct 17, 2017
6ce2752
First version that can translate the static code example
BenWeber42 Oct 17, 2017
cf8a64e
Finished minimal implementation for static code example
BenWeber42 Oct 21, 2017
11afaeb
Implemented Old expressions
BenWeber42 Oct 21, 2017
a0ce593
Activated all tests and added basic old expressions test
BenWeber42 Oct 21, 2017
5427ebe
First version of pure call slots
BenWeber42 Oct 21, 2017
6ba95f4
Minor bugfix in translate_Return
BenWeber42 Oct 21, 2017
979f66c
Added pure test and example b from the project description
BenWeber42 Oct 21, 2017
e8bf2a5
Some bugfixes
BenWeber42 Oct 22, 2017
67539a1
Added pure, while loop and n times examples
BenWeber42 Oct 22, 2017
1d46890
Minor changes to the tests
BenWeber42 Nov 16, 2017
55053ce
Adapted to Viper changes
marcoeilers Nov 20, 2017
53d787d
Attempted merge
marcoeilers Mar 13, 2018
29ee893
Fixed some things
marcoeilers Mar 16, 2018
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
48 changes: 46 additions & 2 deletions src/nagini_contracts/contracts.py
Original file line number Diff line number Diff line change
@@ -20,7 +20,8 @@
CONTRACT_FUNCS = ['Assume', 'Assert', 'Old', 'Result', 'Implies', 'Forall',
'Exists', 'Low', 'Acc', 'Rd', 'Fold', 'Unfold', 'Unfolding',
'Previous', 'RaisedException', 'Sequence', 'ToSeq', 'MaySet',
'MayCreate',]
'MayCreate', 'CallSlot', 'CallSlotProof',
'UniversallyQuantified', 'ClosureCall', ]

T = TypeVar('T')
V = TypeVar('V')
@@ -254,7 +255,7 @@ def ContractOnly(func: T) -> T:
"""
return func


def GhostReturns(start_index: int) -> Callable[[T], T]:
"""
Decorator for functions which specifies which return values are ghost
@@ -271,6 +272,45 @@ def wrap(func: T) -> T:
return wrap


def CallSlot(call_slot: Callable[..., None]) -> Callable[..., Any]:
"""
Decorator to mark a method as a call slot declaration.
"""

def call_slot_handler(*args, **kwargs) -> Any:
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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').

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


def uq_handler(*args, **kwargs) -> None:
pass

return uq_handler

return call_slot_handler


def UniversallyQuantified(uq: Callable[..., None]) -> None:
"""
Decorator to mark a method as introducing universally quantified
variables inside a call slot.
"""
pass


def CallSlotProof(call_slot: Callable[..., Any]) -> Callable[[Callable[..., None]], None]:
"""
Decorator to mark a method as a proof for a call slot.
"""
pass


def ClosureCall(call: Any, justification: Any) -> Any:
"""
Justifies a closure call through either
* a CallSlot (justification == the callslot instance)
* proofing static dispatch (justification == the static method)
"""
pass


def list_pred(l: List[T]) -> bool:
"""
Special, predefined predicate that represents the permissions belonging
@@ -328,6 +368,10 @@ def dict_pred(d: Dict[T, V]) -> bool:
'set_pred',
'Sequence',
'ToSeq',
'CallSlot',
'UniversallyQuantified',
'CallSlotProof',
'ClosureCall',
'MaySet',
'MayCreate',
]
44 changes: 39 additions & 5 deletions src/nagini_translation/analyzer.py
Original file line number Diff line number Diff line change
@@ -52,6 +52,14 @@
)
from nagini_translation.lib.views import PythonModuleView
from typing import Any, Callable, Dict, List, Optional, Set, Tuple, Union
from nagini_translation.call_slot_analyzers import (
CallSlotAnalyzer,
is_call_slot,
CallSlotProofAnalyzer,
is_call_slot_proof,
is_closure_call,
check_closure_call
)


logger = logging.getLogger('nagini_translation.analyzer')
@@ -71,6 +79,7 @@ def __init__(self, types: TypeInfo, path: str, selected: Set[str]):
self.global_module,
sil_names=self.global_module.sil_names)
self.current_class = None
self.outer_functions = [] # type: List[PythonMethod]
self.current_function = None
self.current_scopes = []
self.contract_only = False
@@ -84,6 +93,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):
@@ -110,7 +121,9 @@ def define_new(self, container: Union[PythonModule, PythonClass],
name in container.methods or
name in container.predicates or
(isinstance(container, PythonClass) and
name in container.static_methods)):
name in container.static_methods) or
(isinstance(container, PythonModule) and
name in container.call_slots)):
raise InvalidProgramException(node, 'multiple.definitions')

def collect_imports(self, abs_path: str) -> None:
@@ -453,6 +466,12 @@ def _is_illegal_magic_method_name(self, name: str) -> bool:
return False

def visit_FunctionDef(self, node: ast.FunctionDef) -> None:
if is_call_slot(node):
self.call_slot_analyzer.analyze(node)
return
if is_call_slot_proof(node):
self.call_slot_proof_analyzer.analyze(node)
return
if self.current_function:
raise UnsupportedException(node, 'nested function declaration')
name = node.name
@@ -714,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)
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could probably return after this?

if (isinstance(node.func, ast.Name) and
node.func.id in CONTRACT_WRAPPER_FUNCS):
if not self.current_function or self.current_function.predicate:
@@ -826,8 +847,15 @@ def visit_Name(self, node: ast.Name) -> None:
raise UnsupportedException(assign, msg)
var.value = assign.value
self.module.global_vars[node.id] = var
var = self.module.global_vars[node.id]
self.track_access(node, var)
if node.id in self.module.global_vars:
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
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

When can this happen?

raise UnsupportedException(
node,
"Unsupported reference '%s'" % node.id
)
else:
# Node is a static field.
if isinstance(node.ctx, ast.Load):
@@ -851,7 +879,7 @@ def visit_Name(self, node: ast.Name) -> None:
# again now that we now it's actually static.
del self.current_class.fields[node.id]
return
if not isinstance(self.get_target(node, self.module), PythonGlobalVar):
if not isinstance(self.get_target(node, self.module), (PythonGlobalVar, PythonMethod)):
# Node is a local variable, lambda argument, or a global variable
# that hasn't been encountered yet
var = None
@@ -1009,6 +1037,7 @@ def get_alt_types(self, node: ast.AST) -> Dict[int, PythonType]:
context = []
if self.current_class is not None:
context.append(self.current_class.name)
context.extend(map(lambda method: method.name, self.outer_functions))
if self.current_function is not None:
context.append(self.current_function.name)
name = node.id if isinstance(node, ast.Name) else node.arg
@@ -1033,6 +1062,7 @@ def typeof(self, node: ast.AST) -> PythonType:
context = []
if self.current_class is not None:
context.append(self.current_class.name)
context.extend(map(lambda method: method.name, self.outer_functions))
if self.current_function is not None:
context.append(self.current_function.name)
context.extend(self.current_scopes)
@@ -1061,6 +1091,7 @@ def typeof(self, node: ast.AST) -> PythonType:
context = []
if self.current_class is not None:
context.append(self.current_class.name)
context.extend(map(lambda method: method.name, self.outer_functions))
context.append(self.current_function.name)
context.extend(self.current_scopes)
type, _ = self.module.get_type(context, node.arg)
@@ -1159,7 +1190,10 @@ def visit_Try(self, node: ast.Try) -> None:
def _incompatible_decorators(self, decorators) -> bool:
return ((('Predicate' in decorators) and ('Pure' in decorators)) or
(('IOOperation' in decorators) and (len(decorators) != 1)) or
(('property' in decorators) and (len(decorators) != 1)))
(('property' in decorators) and (len(decorators) != 1)) or
(('CallSlot' in decorators) and (len(decorators) != 1)) or
(('UniversallyQuantified' in decorators) and (len(decorators) != 1)) or
(('CallSlotProof' in decorators) and (len(decorators) != 1)))

def is_declared_contract_only(self, func: ast.FunctionDef) -> bool:
"""
Loading