forked from eurecom-s3/symcc
-
Notifications
You must be signed in to change notification settings - Fork 5
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
Merge Upstream #7
Merged
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 needs to be reverted once a proper fix is in place.
This is just the output of "clang-format -style=llvm -dump-config".
Clang now uses the new pass manager for the optimization pipeline, so we have to do the same to make Clang use our pass. Moreover, FileCheck now complains if a configured prefix doesn't appear in the checked file; added "ANY" in three tests where it was missing. Finally, printing arbitrary-precision integers in QSYM needed some changes.
We should really automate this...
Z3 doesn't always output model constants in the same order; make sure that our tests don't depend on it.
This commit adds the option to mark symbolic input by calling symcc_make_symbolic from the program under test. The refactoring that was required to add the new feature has had the pleasant side effect that the QSYM backend now doesn't require the entire input upfront anymore, making it much more convenient to feed symbolic data through stdin.
No need for "push": the "pull_request" event already triggers when new commits are pushed to the PR branch, and we expect all changes to go through a PR.
The program under test (or a wrapper around it) can now call symcc_set_test_case_handler to define a function that will be invoked for each newly generated test case.
Memory comes in as void*, so we should also return it with that type; users can cast the pointer to anything they want.
This commit closes eurecom-s3#114.
We weren't able to generate symbolic expressions for insertvalue instructions whose target operand was "undef".
We need to convert the corresponding expressions to/from bit-vectors before/after the operation.
eng/fuzz/symcc#1
Closes eng/fuzz/symcc#4.
This pass uses LLVM's `IntrinsicLowering` interface to lower supported intrinsics so that they can be symbolized.
Intrinsics, etc.
Perform conversion to/from the Boolean solver kind for insertvalue/extractvalue instructions the same way as for load/store, and extract the corresponding functionality into shared helpers.
This change exploits LLVM's target lowering and its ability to expand inline assembly into explicit LLVM code. Importantly, this expansion includes lifting `bswap` instructions to the `bswap` intrinsic, which can be symbolized with symcc. This fixes issue eurecom-s3#29 and does away with the hacks made in PR eurecom-s3#75
Fixes eng/fuzz/symcc#10.
It's now available in Ubuntu 22.04.
The original wrapper didn't do symbolization work, which will lose constraints.
Fixes eng/fuzz/symcc#12.
The removed commands are now executed automatically.
This is a reproducer for eurecom-s3#134.
This commit fixes eurecom-s3#140 by calling the test-case handler with the proper calling convention for instrumented code, i.e., setting parameter expressions before the call.
CI is failing because packages aren't available in the repositories.
These tests reproduce eurecom-s3#138. They show that we fail to generate expressions for struct literals containing floats/Booleans, as well as for the result of inserting symbolic floats/Booleans into structs.
This commit fixes two problems, both part of eurecom-s3#138: 1. When creating expressions for struct literals, we now convert expressions for floats and Booleans to bit-vector kind before attempting to concatenate them with the rest of the struct expression. 2. In "insertvalue" instructions with a symbolic target and a concrete value to insert we now make sure that the runtime call to create the expression for the inserted value isn't optimized out.
Since the QSYM backend doesn't support floating-point arithmetic, we don't ordinarily generate expressions for floats. This is a problem when we need to create expressions for structs containing floats. Add dummy runtime functions to prevent crashes in this case. Closes eurecom-s3#138.
This commit implements eng/fuzz/symcc#13.
Part of eng/toolchain/llvm-project#1.
There are quote a few new runtime functions in this PR. It seems as if it shouldn't be an issue though, because almost all of them are implemented in terms of already existing functions inside the common runtime. So this looks okay to me as long as the in libafl still pass. |
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.
No description provided.