so as a little side project I've been trying to synthesize abstract transfer functions for the "known bits" domain that LLVM leans heavily on.
a fun finding is that I can get a maximally precise function for subtracting known bits!
Conversation
Replying to
for signed division I can make a function that gets 57% of maximum precision, which is nice since LLVM doesn't even make an effort on this one, just returns top unconditionally
1
9
this function produces known zeroes for the subtract operator. it is about as readable as synthesized code gets, some of the stuff I've seen is much worse.
3
6
Replying to
Any hints on how that subtraction works? I once did a similar thing for addition (without proving maximal precision though) so it might be fun to compare notes
1
1
Replying to
well, I've worked out the details before, but it was a while ago. this synthesized code is more or less a black box except for really simple cases.
code is here:
1
Show replies
Replying to
is that a function that, given a,b such that a=knownbits(A) and b=knownbits(B), returns knownbits(A-B)? or something else?
1
Show replies
Replying to
This is a really interesting application of program synthesis... I messed around with bit-twiddling in the "known bits" domain a while ago and this reminded me to finish writing up my results, thanks!
1
3
i guess the key to impact is to make even your "side projects" something that sounds like cool research to everyone else.
1
2
now I'm just sitting here, looking at my "side project" of making the perfect French toast, and realizing why I still haven't achieved my goals.
2
4
Show replies