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 support for more Int types & Refactor files #27

Merged
merged 7 commits into from
Feb 23, 2023

Conversation

JustinReiter
Copy link
Collaborator

@JustinReiter JustinReiter commented Feb 22, 2023

Simplifies the logic for creating Integer types for call LLVM instructions and LLVM Arithmetic intrinsic functions. Any signed integer type that is 64 bits and below is currently supported (i8, i16, i32, i64 and isize).

TODO: add support for unsigned type. In theory, this should be very similar to signed integers (requires modification of constraints and z3 variables).

Update: support for unsigned types are trickier than expected. LLVM does not preserve the type and lifts all unsigned to be signed values. Intrinsic functions still use the unsigned counterparts, but use signed arguments (and handles the operations correctly). There still seems to be a notion of unsigned type when running the program, but unclear where this is from. (Look at README for a stack overflow article)

Testing framework also updated to create the temp test directory if it does not already exist (otherwise there will be a panic).

TODO: update the temp test dir logic to be deleted afterwards (possibly).

Update: Added new tests for each signed type that is currently supported (i8, i16, i32 & i64). i128 is not currently implemented due to the Z3 binding working with values up to i64 easily (whereas, a different conversion to a Z3 Int would be needed for larger int types).

Lastly, files and modules refactored into a nested structure. Lib and imports have been rearranged.

@JustinReiter JustinReiter changed the title [DRAFT] Add support for more Int types & Refactor files Add support for more Int types & Refactor files Feb 23, 2023
Copy link
Owner

@wu-benjamin wu-benjamin left a comment

Choose a reason for hiding this comment

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

Looks good to me for the most part!

It would be nice to use is_int_type when constraining inputs in symbolic_execution.rs for consistency instead of checking for a prefix i though this is a non-blocking issue.

Feel free to merge or fix and merge.

src/utils/var_utils.rs Show resolved Hide resolved
src/symbolic_execution.rs Outdated Show resolved Hide resolved
src/codegen/codegen_call.rs Show resolved Hide resolved
@wu-benjamin
Copy link
Owner

Just a note that we can probably support i128 in the future by creating the Z3::ast::Int with the from_str function.

@wu-benjamin wu-benjamin linked an issue Feb 23, 2023 that may be closed by this pull request
@JustinReiter JustinReiter merged commit 6c7d85e into master Feb 23, 2023
@JustinReiter JustinReiter deleted the jr-nested-files-variable-ints branch February 23, 2023 04:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Handle variable type domain restrictions
2 participants