-
-
[原创]有意思的除法优化及成本低廉的不透明谓词构造
-
发表于: 2021-4-7 13:07
-
好久没灌水了，发贴冒个泡~
最近在科研搬砖的过程中发现了一个有意思的东西 —— 编译器对于除法与求模运算的优化
用图1说明这个优化的事
求模运算的优化分为两步：1.求商；2.被除数 - 除数 * 商 = 余数。求商的过程是编译优化的结果
0xCCCCCCCD这个Magic Number怎么算出来的可以参考《算法心得：高效算法的秘密》的第10章，见图2
图1
图2
吊诡的事情就是，我用Z3尝试解这个优化后的求商运算的最大值，并发现Z3解不出（在实验室服务器上挂了快二十分钟没跑出来
贴个我的求解脚本说明问题
[注意]传递专业知识、拓宽行业人脉——看雪讲师团队等你加入！
最后于 2021-4-7 13:18
被天水姜伯约编辑
，原因：
