首页
社区
课程
招聘
[原创]Klee 路径选择算法汇总
发表于: 2022-6-5 19:58 5615

[原创]Klee 路径选择算法汇总

2022-6-5 19:58
5615

Klee 路径选择算法

最近写论文,需要用到klee,因此对其路径选择算法进行汇总。内容来自网络以及个人理解,因为还在学习阶段,可能理解上会有偏差,希望各位师傅不吝赐教!!!

 

通过对Klee repo中Searcher.hSearcher.cpp两个与klee路径选择算法相关的文件的分析,可知klee用于九种路径选择算法。

  1. DFSSearcher
    该算法实现了深度优先的路径探索。所有的状态都维持着插入的顺序,最后一个状态被选择为进一步的探索。
  2. BFSSearcher
    该算法实现了宽度优先的路径探索。 When KLEE branches multiple times for a single instruction, all new states have the same depth.进程树 (PTree) 是二叉树,因此该树中的状态及其在 BFS 期间的分支深度是不同的。
  3. RandomSearcher
    该算法随机选择一个状态。
  4. WeightedRandomSearcher
    该算法使用DiscretePDF作为数据结构。
    有七种权重计算方法(Depth, RP, QueryCost, InstCount, CPInstCount, MinDistToUncovered, CoveringNew),需要后面进一步分析。
  • MinDistToUncovered
    初始化每个未覆盖的指令 min-distance-to-uncovered 值为 1,每条覆盖指令的 min-distance-to-uncovered 值为 0。从它的继任者开始,迭代每条指令,继承 min-distance-to-uncovered 值,直到不再有 min-distance-to-uncovered 值改变。然后就可以得到每一个指令的最小距离。
  1. RandomPathSearcher
    该算法通过随机遍历PTree来选择一个状态。PTree是一个全局数据结构,该算法有时只能从所有状态的一个子集中选择(取决于更新调用)。
  2. MergingSearcher
    暂时不了解。
  3. BatchingSearcher
    该算法从底层searcher中选择一个状态并返回该状态在给定时间或给定数量的指令内进行进一步探索。
  4. IterativeDeepeningTimeSearcher
    该算法基于时间实现。状态是从基础searcher中选择的。当状态达到其时间限制时,它会暂停(从底层searcher中删除)。当底层searcher用完状态时,时间预算增加并全部暂停状态恢复(添加到底​​层searcher)。
  5. InterleavedSearcher
    该算法在循环中从一组searcher中选择状态方式。它是KLEE 的默认策略,在它之间切换具有 CoveringNew 指标的 RandomPathSearcher 和WeightedRandomSearcher。

RandomSearcher 和 RandomPathSearcher的区别?

假设 KLEE 有 3 个状态:一个路径为假(在第一个分支),一个路径为真(在第一个分支),假(在第二个分支),一个路径为真(在第一个分支),真(在第二个分支)。 RandomSearcher 给每个状态一个 1/3 的概率,但是有两个以 True 开头的状态,只有一个以 False 开头的状态,所以有 2/3 的概率选择以 True 开头的状态。因此,州之间是公平的,但在某种意义上,路径之间是不公平的。

 

RandomPathSearcher 从根开始,并在每个分支处以相等的概率选择一个随机方向。它继续运行,直到找到一个状态。所以它有0.5的概率选择False,选择False状态;如果它选择 True,它会为第二个分支做出另一个随机选择,因此总共有 0.25 的概率选择 True、False 状态,对于 True、True 状态也是如此。所以 RandomPathSearcher 在状态之间是不公平的,但在路径之间是公平的。

名词解释

state

解释器里的几个重要流程的操作对象都是状态。状态的组成包含很多信息(如pc、栈约束条件),代码在ExecutionState.cpp

关于state的操作

1
2
3
4
5
6
7
branch *// 处理分支情况,实际就是复制条件为false的状态*
pushFrame 
popFrame
addSymbolic
merge *//合并状态* ,逻辑比较复杂
dumpStack
addConstraint *//调用约束管理器添加约束

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

收藏
免费 4
支持
分享
最新回复 (2)
雪    币: 2466
活跃值: (4550)
能力值: ( LV2,RANK:10 )
在线值:
发帖
回帖
粉丝
2
正好最近在头疼dse的路径策略,参考一下klee
2022-6-6 10:09
0
雪    币: 17
能力值: ( LV1,RANK:0 )
在线值:
发帖
回帖
粉丝
3
默NJ 正好最近在头疼dse的路径策略,参考一下klee
一起学习
2022-6-6 12:57
0
游客
登录 | 注册 方可回帖
返回
//