Move error check right after making call to Z3 #373
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This commit introduces a simple helper class to write source code. It's basically a string-like object to which more code can be added via += (as it was done before) but with some helpers to manage indentation. This is merely a preparation for next commit which would generate more complex code and managing indentation by hand (as it was done up to now) becomes too much. The changes in `Z3` class are all whitespace changes - the new code does not output trailing tab and I did not care to complicate logic in apigen.py to make write bit-to-bit output.
During debugging of weird failure in `Z3CAPITest >> testEnum` we realized that the call to Z3 failed but did not fail in `#errorCheck` as one would expect. Instead, the code failed trying to extract value from output parameter (which was luckily NULL!). This is because call to `#errorCheck` was made too late, after extracting and freeing output parameters. The correct thing is to call `#errorCheck` right after the call to Z3 API. However, this is not that simple! If there are array arguments, we have to free them in ensure (otherwise we'd leak them). To make it more complicated, some arrays are out or in/out parameters, so we have to extract the value after # errorCheck but NOT in #ensure: block in case call fails. Yet another 'complication' comes from the fact, that few Z3 API do not require error check (have no context) but use out and/or in/out parameters. This commit updates `apigen.py` so it generates ensure when needed and updates code in class `Z3` accordingly.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
During debugging of weird failure in
Z3CAPITest >> testEnumwerealized that the call to Z3 failed but did not fail in
#errorCheckas one would expect. Instead, the code failed trying to extract value
from output parameter (which was luckily NULL!).
This is because call to
#errorCheckwas made too late, afterextracting and freeing output parameters.
The correct thing is to call
#errorCheckright after the call to Z3API. However, this is not that simple! If there are array arguments,
we have to free them in ensure (otherwise we'd leak them). To make it
more complicated, some arrays are out or in/out parameters, so we have
to extract the value after # errorCheck but NOT in #ensure: block in
case call fails.
Yet another 'complication' comes from the fact, that few Z3 API do not
require error check (have no context) but use out and/or in/out
parameters.
This PR updates
apigen.pyso it generates ensure when neededand updates code in class
Z3accordingly.