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

Add an eval_int command to the remote API and Python interface #1660

Merged
merged 9 commits into from
May 9, 2022

Conversation

chameco
Copy link
Contributor

@chameco chameco commented May 6, 2022

Partially addresses #1642. I'm marking this as a draft because I intend to add equivalents for other types (or maybe one eval command that works on everything) before merging.

@chameco chameco marked this pull request as ready for review May 9, 2022 00:37
@chameco
Copy link
Contributor Author

chameco commented May 9, 2022

For now, eval_int and eval_bool are implemented. eval_size seems trickier, and maybe not even useful in the Python setting right now, because as far as I know there is no way to define a Cryptol type value through the API (something like SAWScript's {| ... |}).

eval_list returns a list of Terms, which doesn't map nicely to the API as designed currently - functions that would take a Term in SAWScript instead typically take a Cryptol expression. I'm not sure if eval_list is even useful in Python, necessarily - in my experience it is mostly used in SAWScript to get around a lack of list manipulation primitives.

Copy link
Contributor

@RyanGlScott RyanGlScott left a comment

Choose a reason for hiding this comment

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

Thanks, @chameco! I've left some minor suggestions inline, but otherwise this LGTM.

eval_size seems trickier, and maybe not even useful in the Python setting right now, because as far as I know there is no way to define a Cryptol type value through the API (something like SAWScript's {| ... |}).

Ah, good point. I do think we'll want to have a Python counterpart to {| ... |} at some point, so it would be worth opening an issue about that. I agree that we don't need to solve that problem in this PR, however.

saw-remote-api/python/tests/saw/test_eval.py Outdated Show resolved Hide resolved
saw-remote-api/src/SAWServer/Eval.hs Outdated Show resolved Hide resolved
saw-remote-api/python/tests/saw/test_eval.py Outdated Show resolved Hide resolved
saw-remote-api/python/saw_client/connection.py Outdated Show resolved Hide resolved
saw-remote-api/src/SAWServer/Eval.hs Outdated Show resolved Hide resolved
raise ValueError(str(v) + " is not an integer")
return v

def eval_bool(expr: cryptoltypes.CryptolJSON) -> int:
Copy link
Contributor

Choose a reason for hiding this comment

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

Suggested change
def eval_bool(expr: cryptoltypes.CryptolJSON) -> int:
def eval_bool(expr: cryptoltypes.CryptolJSON) -> bool:

Copy link
Contributor Author

Choose a reason for hiding this comment

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

It's curious that the Mypy run in CI didn't catch this. Testing locally: if I remove the isinstance check, I get the expected type error ("returning Any from a function declared to return bool"), but I don't get any error if the isinstance check mismatches the declared return type.

Choose a reason for hiding this comment

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

A bool is an int:

>>> isinstance(False, int)
True
>>> isinstance(True, int)
True
>>> issubclass(bool, int)
True

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Ah, that would explain it. TIL. Thanks!

@RyanGlScott
Copy link
Contributor

Also, can you update the changelogs for saw-remote-api and the SAW Python client to mention these changes? Thanks!

saw-remote-api/src/SAWServer/Eval.hs Outdated Show resolved Hide resolved
saw-remote-api/src/SAWServer/Eval.hs Outdated Show resolved Hide resolved
saw-remote-api/python/CHANGELOG.md Outdated Show resolved Hide resolved
saw-remote-api/CHANGELOG.md Show resolved Hide resolved
@chameco chameco added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label May 9, 2022
@mergify mergify bot merged commit e4c2c47 into master May 9, 2022
@mergify mergify bot deleted the sb/remote-eval-int branch May 9, 2022 19:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants