ychen added a comment. In D97915#2728377 <https://reviews.llvm.org/D97915#2728377>, @ChuanqiXu wrote:
> This code snippets confused me before: > > coro.alloc.align: ; preds = > %coro.check.align > %mask = sub i64 %11, 1 > %intptr = ptrtoint i8* %call to i64 > %over_boundary = add i64 %intptr, %mask > %inverted_mask = xor i64 %mask, -1 > %aligned_intptr = and i64 %over_boundary, %inverted_mask > %diff = sub i64 %aligned_intptr, %intptr > %aligned_result = getelementptr inbounds i8, i8* %call, i64 %diff > > This code implies that `%diff > 0`. Formally, given `Align = 2^m, m > 4` and > `Address=16n`, we need to prove that: > > (Address + Align -16)&(~(Align-1)) >= Address > > `&(~Align-1)` would make the lowest `m` bit to 0. And `Align-16` equals to > `2^m - 16`, which is `16*(2^(m-4)-1)`. Then `Address + Align -16` could be > `16*(n+2^(m-4)-1)`. > Then we call `X` for the value of the lowest `m` bit of `Address + Align > -16`. > Because `X` has `m` bit, so `X <= 2^m - 1`. Noticed that `X` should be 16 > aligned, so the lowest 4 bit should be zero. > Now, > > X <= 2^m - 1 -1 - 2 - 4 - 8 = 2^m - 16 > > So the inequality we need prove now should be: > > 16*(n+2^(m-4)-1) - X >= 16n > > Given X has the largest value wouldn't affect the inequality, so: > > 16*(n+2^(m-4)-1) - 2^m + 16 >= 16n > > which is very easy now. > > The overall prove looks non-travel to me. I spent some time to figure it out. > I guess there must be some other people who can't get it immediately. I > strongly recommend to add comment and corresponding prove for this code. The code is equivalent to (Address + Align -1)&(~(Align-1)) >= Address which should be correct. It is implemented by `CodeGenFunction::EmitBuiltinAlignTo`. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D97915/new/ https://reviews.llvm.org/D97915 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
