Add support for reflected arithmetic magic functions #183
Conversation
|
This should be ready to merge. The only test failures are caused by missing dunder methods in the allowed whitelist. I've mixed up the commit order, and they are added to the whitelist in #182. |
|
|
||
| param_types = [arg.type for arg in func.get_args()] | ||
| if len(param_types) != len(arg_types): | ||
| return None |
There was a problem hiding this comment.
Is this case ever supposed to happen or would it indicate an internal error?
There was a problem hiding this comment.
Thinking about this again, I'm not sure if this could ever even happen at all.
Checking for matching argument types is still necessary though.
| Requires(False) | ||
| assert False | ||
|
|
||
| r3 = E() + E() |
There was a problem hiding this comment.
Like for the other PR, it would be great if you could also add a few statements that should lead to verification errors. Since you'll only get at most one error per function and one error for all top-level statements in Silicon, that might require putting some of the top-level statements here into separate functions.
Python allows types to define "reflected" arithmetic magic functions (e.g. __radd__). These functions are used under certain conditions when the original magic functions (e.g. __add__) don't support a certain operand type. To correctly support these functions in Nagini, the correct calls to the right functions need to be dispatched during the translation step. (See https://docs.python.org/3.8/reference/datamodel.html#object.__radd__ for specifications on when these functions are called)
If the right operand of a binary operation is a subtype of the left operand, and the right operand type provides its own implementation of the matching reflected magic function, this reflected function should be used regardless of whether it overrides the left operands magic function or the left operand type doesn't implement that function.
Binary operations between ints and floats are implemented by adding reflected arithmetic magic functions to the float type definition
PascalDevenoge
force-pushed
the
right_operand_magic_functions
branch
from
0456310 to
5be9001
Compare
| c = a + b | ||
|
|
||
| assert c.i == 57 | ||
| #:: ExpectedOutput(assert.failed:assertion.false) |
There was a problem hiding this comment.
I've added a few cases that are expected to produce verification failures. They're not much more that some basic smoke tests. Did you have anything more specific in mind?
There was a problem hiding this comment.
No, this is exactly what I meant, thanks. Just something to make sure e.g. the correct preconditions are actually being checked and we'd catch it if there was an accidental assume false somewhere in the encoding.
Implements support for reflected magic functions (radd etc.) Haven't looked into getting in place versions (iadd) to work yet.
This change is