bedrock2 C code is incompatible with BoringSSL #821
Comments
|
The issue with pointer types is rather fundamental, bedrock2 does not have a notion of pointers at all. I don't have a satisfying plan for it. Given that bottleneck, I think the immediate path forward would be to perhaps reconcile the argument order, disable all the warnings, and make a patch for boringssl to remove the workaround returning a single scalar through a pointer. This won't be clean enough to be upstreamed, but we could at least test it. |
|
If you all decide to swap the input/output order, we can certainly adapt. Although matching our order is certainly more convenient! (We put outputs first because that tends to be what C does, e.g. IIRC, C only promises that going from pointer to sufficiently-large-integer to pointer works if the integer is the exact value you get out. What happens you do arithmetic in the integer space and cast back to pointer is implementation-defined. (That said, GCC does promise that arithmetic in the integer space commutes with pointer casts.) The other nuisance is it's not obvious from the generated code that the data needs to be declared as an array of I could also believe that the compiler does some silly things when you do sufficiently complicated things with pointers, or hopefully it's smart enough given all the function bodies are available. (Compilers have to play escape analysis games when deciding whether something can be promoted to a register, etc.) |
|
I was able to successfully run BoringSSL tests locally for curve25519 with a pretty straightforward manual changes. I kept the BoringSSL function signature, replaced the body with bedrock2, and:
So, for instance, given the BoringSSL function signature:
and the bedrock2-as-C code: I would do: For plain integers I just used a cast, e.g. I think the best way forward is to automate this transformation or use wrapper functions, rather than play tricks with pointer arithmetic. However, it's pretty straightforward to put outputs before inputs in the calling convention if that's helpful. Returning an integer through a pointer is also a possible change, but not one I'm convinced I want to do for every case. As for the tautological compare, it should surely be addressed with rewrite rules, no? Why does it need #679? |
|
If we want to support compilation with strict aliasing enabled (probably a requirement for BoringSSL?), we can't do this:
Hopefully we can do mit-plv/bedrock2#159, otherwise we will have to require code calling us to declare the field element type as
|
I would appreciate this change.
What about having a flag that controls this behavior? Or, perhaps more generally, what's the argument against? I believe I did this originally because treating input and output uniformly made writing the code for printing the function declarations and comments addressing bounds, pre/postconditions, etc, significantly simpler. I could backtrack on this, but it's not clear to me what the benefit of the non-pointer-based version is.
Yes, I mistyped, and meant to type #769. The tricky bit is that the rewriter doesn't support non-linear occurrences of non-constants, so we need to add variants of the original rules to not generate tautological compares in the first place. |
I believe not needlessly passing information through the heap when it can be passed directly makes generating and verifying functions much simpler; it is also considered a good practice in normal C code. For me, that last part is the main benefit -- unnecessarily using an indirection looks jarring, even if it is fine, even if it is non-uniform when compared to passing arrays. |
FWIW, I think it's fine to have opinions on how the field element type is declared. You have opinions on its memory layout, after all. And the current generated code does believe the field elements should be Having an opinion is probably better than using |
|
We discussed this in the fiat-crypto meeting today. I think we said
|
|
I guess another strategy would be to use inferred C types where they are available, and fall back to bytewise access when not... I think this would be legal wrt strict aliasing, and it would make the inherent incompleteness of the type inference less pressing. I can't think of a similar standard fallback for pointer arithmetic, though -- but I don't particularly care about supporting any implementation-defined behavior other than flat single address space anyway. |
|
Here's the patch file for replacing boringssl curve25519_64.h function bodies with bedrock2 implementations using the method I described in #821 (comment) |
|
This article reminded me of the |
There are a number of issues, some more major than others:
fiat_p256_nonzero) still use pointers, but in bedrock2, this is not the case.Move language-specific cast-insertion to bounds analysis pass #679Improve bedrock2 rewrite rules so we don't need-Wno-error=tautological-compare#769 means the code isn't clean enough for BoringSSL, probably (since it needs-Wno-error=tautological-compare)-Wno-error=unused-but-set-variablemight also mean the code is insufficiently cleanuintptr_twhile BoringSSL needs pointersuintptr_t(also, "note: expected ‘uintptr_t {aka long unsigned int}’ but argument is of type ‘fiat_p256_limb_t * {aka long unsigned int *}’")How much of this is fixable (easily? with effort?) @jadephilipoom @andres-erbsen ?
This is a blocker for #811
Build log from PR run
The text was updated successfully, but these errors were encountered: