好久没灌水了,发贴冒个泡~
最近在科研搬砖的过程中发现了一个有意思的东西 —— 编译器对于除法与求模运算的优化
用图1说明这个优化的事
求模运算的优化分为两步:1.求商;2.被除数 - 除数 * 商 = 余数。求商的过程是编译优化的结果
0xCCCCCCCD这个Magic Number怎么算出来的可以参考《算法心得:高效算法的秘密》的第10章,见图2
图1
图2
吊诡的事情就是,我用Z3尝试解这个优化后的求商运算的最大值,并发现Z3解不出(在实验室服务器上挂了快二十分钟没跑出来
贴个我的求解脚本说明问题
[培训]内核驱动高级班,冲击BAT一流互联网大厂工作,每周日13:00-18:00直播授课
有意思,mark了