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

Allow configuring Crucible's lax-pointer-ordering option from SAW #1308

Closed
RyanGlScott opened this issue May 24, 2021 · 0 comments · Fixed by #1309
Closed

Allow configuring Crucible's lax-pointer-ordering option from SAW #1308

RyanGlScott opened this issue May 24, 2021 · 0 comments · Fixed by #1309
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm type: feature request Issues requesting a new feature or capability

Comments

@RyanGlScott
Copy link
Contributor

There are some scenarios where LLVM is prone to generate code that compares pointers from different allocation blocks. For example, LLVM's strength reduction passes can generate comparisons between pointers with -O2 or higher, as seen in GaloisInc/crucible#149. Here is another example, distilled from BoringSSL:

#include <stdint.h>
#include <stdlib.h>

uint64_t constant_time_select_w(uint64_t mask, uint64_t a, uint64_t b) {
  return (mask & a) | (~mask & b);
}

void bn_select_words(uint64_t *r, uint64_t mask, const uint64_t *a, const uint64_t *b, size_t num) {
  for (size_t i = 0; i < num; i++) {
    r[i] = constant_time_select_w(mask, a[i], b[i]);
  }
}

These examples work when Crucible's lax-pointer-ordering option is enabled. This option is off by default, however, and SAW does not offer a way to change the default setting. We should offer functionality to do so, much like we offer functionality to configure lax-arithmetic.

@RyanGlScott RyanGlScott added subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm type: feature request Issues requesting a new feature or capability labels May 24, 2021
@RyanGlScott RyanGlScott changed the title Allow configuring Crucible's lax-pointer-arithmetic option from SAW Allow configuring Crucible's lax-pointer-ordering option from SAW May 25, 2021
RyanGlScott added a commit that referenced this issue May 25, 2021
RyanGlScott added a commit that referenced this issue Jun 17, 2021
@mergify mergify bot closed this as completed in #1309 Jun 17, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm type: feature request Issues requesting a new feature or capability
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant