[PATCH] D97915: [Coroutines] Handle overaligned frame allocation
Chuanqi Xu via Phabricator via llvm-commits
llvm-commits at lists.llvm.org
Fri Apr 30 02:30:07 PDT 2021
ChuanqiXu added a comment.
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.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D97915/new/
https://reviews.llvm.org/D97915
More information about the llvm-commits
mailing list