首页
社区
课程
招聘
[原创]有意思的除法优化及成本低廉的不透明谓词构造
发表于: 2021-4-7 13:07 6510

[原创]有意思的除法优化及成本低廉的不透明谓词构造

2021-4-7 13:07
6510

好久没灌水了,发贴冒个泡~


最近在科研搬砖的过程中发现了一个有意思的东西 —— 编译器对于除法与求模运算的优化


用图1说明这个优化的事


求模运算的优化分为两步:1.求商;2.被除数 - 除数 * 商 = 余数。求商的过程是编译优化的结果


0xCCCCCCCD这个Magic Number怎么算出来的可以参考《算法心得:高效算法的秘密》的第10章,见图2


图1


图2


吊诡的事情就是,我用Z3尝试解这个优化后的求商运算的最大值,并发现Z3解不出(在实验室服务器上挂了快二十分钟没跑出来


贴个我的求解脚本说明问题


[注意]传递专业知识、拓宽行业人脉——看雪讲师团队等你加入!

最后于 2021-4-7 13:18 被天水姜伯约编辑 ,原因:
收藏
免费 1
支持
分享
最新回复 (1)
雪    币: 8427
活跃值: (5021)
能力值: ( LV4,RANK:45 )
在线值:
发帖
回帖
粉丝
2

有意思,mark了

最后于 2021-4-7 18:08 被v0id_编辑 ,原因:
2021-4-7 18:07
1
游客
登录 | 注册 方可回帖
返回
//