klee源码阅读笔记1--STPBuilder类

初始化过程中四个数据成员中的两个数据成员被初始化:

一、vc被初始化为STP提供的C调用接口函数vc_createValidityChecker();

二、optimizeDivides被初始化为false

重点探讨另外两个数据成员。


一、ExprHashMap constructed

ExprHashMap< std::pair<ExprHandle, unsigned> > constructed;

ExprHashMap为一个模板类, 继承unorderedmap,由于自定义Key的类型,因此需要自定义==和hash。

namespace klee {

  namespace util {
    struct ExprHash  {//定义hash
      unsigned operator()(const ref<Expr> e) const {
        return e->hash();
      }
    };
    
    struct ExprCmp {//定义==
      bool operator()(const ref<Expr> &a, const ref<Expr> &b) const {
        return a==b;
      }
    };
  }// namespace util
  
  template<class T> 
  class ExprHashMap : 

    public unordered_map<ref<Expr>,
                         T,
                         klee::util::ExprHash,
                         klee::util::ExprCmp> {
  }; 
  
  typedef unordered_set<ref<Expr>,
                        klee::util::ExprHash,
                        klee::util::ExprCmp> ExprHashSet;

} //namespace klee

1.1 unordered_map

template<class Key,                                            //The key type.
    class Ty,                                                  //The mapped type.
    class Hash = std::hash<Key>,                               //The hash function object type.
    class Pred = std::equal_to<Key>,                           //The equality comparison function object type.
    class Alloc = std::allocator<std::pair<const Key, Ty> > >  //The allocator class.
class unordered_map;
可以看到模板中Hash、Pred、Alloc在未指定的时候是有默认值的。
可以看出Klee中定义ExprHashMap类继承unordered_map类,使用klee::util::ExprHash作为Hash,使用klee::util::ExprCmp作为Pred。键Key的类型是ref<Expr>,T的类型作为模板参数,在实例化的时候具体指定。
博文地址:http://blog.csdn.net/lpstudy/article/details/54345050,c++ unordered_map/set自定义对象的hash,给出了示例代码:

(klee传入unordered_map模板的第三个和第四个参数均是funciton object type,在struct结构体中定义==和hash值)
#include <iostream>
#include <sstream>
#include <string>
#include <vector>
#include <list>
#include <stack>
#include <queue>
#include <algorithm>
#include <map>
#include <set>
#include <unordered_map>
#include <unordered_set>
#include <iomanip>

#include <cstring>
#include <cmath>
#include <cstdlib>
#include <cstdio>

using namespace std;

//改变这个启用不同的hash方案
#define  RECORD_NAMESPACE

struct Record
{
    string name;
    int val;
};

#ifdef RECORD_FUNCTION_OBJECT
struct RecordHash
{
    size_t operator()(const Record& rhs) const{
        return hash<string>()(rhs.name) ^ hash<int>()(rhs.val);
    }
};
struct RecordCmp
{
    bool operator()(const Record& lhs, const Record& rhs) const{
        return lhs.name == rhs.name && lhs.val == rhs.val;
    }
};
unordered_set<Record, RecordHash, RecordCmp> records = {
    { "b", 100 }, { "a", 80 }, { "cc", 70 }, { "d", 60 }, { "d", 60 }
};
#endif//RECORD_FUNCTION_OBJECT

#ifdef RECORD_C_FUNCTION
size_t RecordHash(const Record& rhs){
    return hash<string>()(rhs.name) ^ hash<int>()(rhs.val);
}
/*
小杰注释:return 后面定义了一个std::hash<std::string>临时变量(第一对圆括号),然后调用该临时变量函数operator()(第二对圆括号,这里是运算符重载),并传rhs.name作为参数。
*/
bool RecordCmp(const Record& lhs, const Record& rhs){ return lhs.name == rhs.name && lhs.val == rhs.val; } //直接使用成员初始化列表,vs2013不能编译通过 unordered_set<Record, decltype(&RecordHash), decltype(&RecordCmp)> records = { 10, RecordHash, RecordCmp }; struct RunBeforeMain { RunBeforeMain(){ records.insert({ "a", 100 }); } }; static RunBeforeMain dummyObject; #endif //RECORD_C_FUNCTION #ifdef RECORD_LAMBDA //直接使用auto RecordHash不能编译通过,vs2013 auto &RecordHash = [](const Record& rhs){ return hash<string>()(rhs.name) ^ hash<int>()(rhs.val); }; auto &RecordCmp = [](const Record& lhs, const Record& rhs){ return lhs.name == rhs.name && lhs.val == rhs.val; }; unordered_set<Record, decltype(RecordHash), decltype(RecordCmp)> records = { 10, RecordHash, RecordCmp }; struct RunBeforeMain { RunBeforeMain(){ records.insert({ "a", 100 }); } }; static RunBeforeMain dummyObject; #endif//RECORD_LAMBDA #ifdef RECORD_NAMESPACE namespace std{ template<> struct hash<Record> { size_t operator()(const Record& rhs) const{ return hash<string>()(rhs.name) ^ hash<int>()(rhs.val); } }; template<> struct equal_to < Record > { bool operator()(const Record& lhs, const Record& rhs) const{ return lhs.name == rhs.name && lhs.val == rhs.val; } }; } unordered_set<Record> records = { { "b", 100 }, { "a", 80 }, { "cc", 70 }, { "d", 60 }, { "d", 60 } }; #endif //RECORD_NAMESPACE int main() { auto showRecords = [](){ for (auto i : records) { cout << "{" << i.name << "," << i.val << "}" << endl; } }; showRecords(); return 0; }

说明:对于上述代码中的四种方式,klee使用的是第一种方式。其余三种方式,如何理解?究竟什么含义,这里暂时不深究,我也没有搞明白。引用博文作者的话如下:

平时很少用到unordered_set的自定义对象,常用的都是unordered_map<int>, unordered_map<string>之类的内建数据类型。前段时间在写一个编码库的时候,用到了自定义对象,却无从下手,在此对其进行总结。

unordered_map/set是采用hash散列进行存储的,因此存储的对象必须提供两个方法,1,hash告知此容器如何生成hash的值,2,equal_to 告知容器当出现hash冲突的时候,如何区分hash值相同的不同对象

假定要存储的对象的类名为Object,则具体有4种方案: 
1,定义两个函数对象ObjectHash,以及ObjectEqu,分别实现对Object进行hash,以及比较两个对象是否相同 
2,定义两个普通的c类型的函数,实现hahs以及对象比较,与1不同的是,普通函数在构建unordered_map/set的时候,需要decltype来减少显示声明它的类型(当前可以手动指定类型,很长) 
例如: std::function<size_t(const Object&)>说明hash类型,或者std::function<bool (const Object&, const Object&)>说明比较类型 
3,定义两个lambda表达式(仿函数),与2类似 
4,对Object对象进行模板特化


 

1.2 hash和==的定义

    struct ExprHash  {//定义hash
      unsigned operator()(const ref<Expr> e) const {
        return e->hash();
      }
    };
    
    struct ExprCmp {//定义==
      bool operator()(const ref<Expr> &a, const ref<Expr> &b) const {
        return a==b;
      }
    };

ref类的主要成员是:

template<class T>
class ref {
  T *ptr;

其实ref<Expr>就是定义了一个指针指向Expr类型的实例化对象。

  • 首先,Hash值获取:

e->hash调用的就是Expr的hash函数,具体是:

virtual unsigned hash() const { return hashValue; }hashValue是Expr的数据成员,通过computeHash等函数计算得出。

  • 其次,==

ref模板类中有如下系列定义:

bool operator==(const ref &rhs) const { return compare(rhs)==0; }

int compare(const ref &rhs) const {

    assert(!isNull() && !rhs.isNull() && "Invalid call to compare()");

    return get()->compare(*rhs.get());

}//为什么是*rhs.get?因为rhs.get()返回的是一个指向T类型对象的指针,(模板参数实例化为Expr),也就是指向Expr类型对象的指针。由于,Expr的compare的参数(见下文),使用的是const Expr &b,因此必须使用解引用符号*,
//将指针指向的具体的Expr类型的对象作为参数传入。然后b就是对改参数的引用。这类似于函数参数类型是int &b,然后你现在有的是int *a,你传入的实际参数肯定是*a。

  bool isNull() const { return ptr == 0; }

  T *get () const {

    return ptr;

  }

实际上ref <Expr>类的函数compare,调用的还是T类型对象ptr的compare函数,也就是Expr的compare函数,具体内容在Expr.cpp中:

int Expr::compare(const Expr &b) const {
  static ExprEquivSet equivs;
  int r = compare(b, equivs);
  equivs.clear();
  return r;
}

其中,ExprEquivSet的定义是:

 typedef llvm::DenseSet<std::pair<const Expr *, const Expr *> > ExprEquivSet;

其次,compare(b, equivs)调用的函数compare的定义是:

int Expr::compare(const Expr &b, ExprEquivSet &equivs) const {
  if (this == &b) return 0;//this返回的是当前对象的地址(指向当前对象的指针).如果a和b都引用的是同一个对象的地址,那么肯定是相等的;对象地址不同,我们才开始进行比较。

  const Expr *ap, *bp;
  if (this < &b) {
    ap = this; bp = &b;
  } else {
    ap = &b; bp = this;
  }

  if (equivs.count(std::make_pair(ap, bp)))
    return 0;

  Kind ak = getKind(), bk = b.getKind();
  if (ak!=bk)
    return (ak < bk) ? -1 : 1;

  if (hashValue != b.hashValue) 
    return (hashValue < b.hashValue) ? -1 : 1;

  if (int res = compareContents(b)) 
    return res;

  unsigned aN = getNumKids();
  for (unsigned i=0; i<aN; i++)
    if (int res = getKid(i)->compare(*b.getKid(i), equivs))
      return res;

  equivs.insert(std::make_pair(ap, bp));
  return 0;
}

后续的比较过程,由于对Expr类还没有进行深入了解(这是klee表达式Expression机制的核心),所以暂时不讨论。

该随笔会持续更新。

 



原文地址:https://www.cnblogs.com/xiaojieshisilang/p/6918564.html