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