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

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

2021-4-7 13:07
6524

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


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


用图1说明这个优化的事


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


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


图1


图2


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


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


[培训]内核驱动高级班,冲击BAT一流互联网大厂工作,每周日13:00-18:00直播授课

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

有意思,mark了

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