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机制的核心），所以暂时不讨论。

该随笔会持续更新。

				


				
时间： 2024-10-10 15:07:06 

		


		


	

	
	

		


		
klee源码阅读笔记1--STPBuilder类的相关文章


								

		

			

                CI框架源码阅读笔记3 全局函数Common.php
			

		

		

									

				从本篇开始,将深入CI框架的内部,一步步去探索这个框架的实现.结构和设计. Common.php文件定义了一系列的全局函数(一般来说,全局函数具有最高的加载优先权,因此大多数的框架中BootStrap引导文件都会最先引入全局函数,以便于之后的处理工作). 打开Common.php中,第一行代码就非常诡异: if ( ! defined('BASEPATH')) exit('No direct script access allowed'); 上一篇(CI框架源码阅读笔记2 一切的入口 index			

		

	

				

		

			

                源码阅读笔记 - 1 MSVC2015中的std::sort
			

		

		

									

				大约寒假开始的时候我就已经把std::sort的源码阅读完毕并理解其中的做法了,到了寒假结尾,姑且把它写出来 这是我的第一篇源码阅读笔记,以后会发更多的,包括算法和库实现,源码会按照我自己的代码风格格式化,去掉或者展开用于条件编译或者debug检查的宏,依重要程度重新排序函数,但是不会改变命名方式(虽然MSVC的STL命名实在是我不能接受的那种),对于代码块的解释会在代码块前(上面)用注释标明. template<class _RanIt, class _Diff, class _Pr> in			

		

	

				

		

			

                CI框架源码阅读笔记5 基准测试 BenchMark.php
			

		

		

									

				上一篇博客(CI框架源码阅读笔记4 引导文件CodeIgniter.php)中,我们已经看到:CI中核心流程的核心功能都是由不同的组件来完成的.这些组件类似于一个一个单独的模块,不同的模块完成不同的功能,各模块之间可以相互调用,共同构成了CI的核心骨架. 从本篇开始,将进一步去分析各组件的实现细节,深入CI核心的黑盒内部(研究之后,其实就应该是白盒了,仅仅对于应用来说,它应该算是黑盒),从而更好的去认识.把握这个框架. 按照惯例,在开始之前,我们贴上CI中不完全的核心组件图: 由于BenchMa			

		

	

				

		

			

                CI框架源码阅读笔记4 引导文件CodeIgniter.php
			

		

		

									

				到了这里,终于进入CI框架的核心了.既然是"引导"文件,那么就是对用户的请求.参数等做相应的导向,让用户请求和数据流按照正确的线路各就各位.例如,用户的请求url: http://you.host.com/usr/reg 经过引导文件,实际上会交给Application中的UsrController控制器的reg方法去处理. 这之中,CodeIgniter.php做了哪些工作?我们一步步来看. 1.    导入预定义常量.框架环境初始化 之前的一篇博客(CI框架源码阅读笔记2 一切的入			

		

	

				

		

			

                IOS测试框架之：athrun的InstrumentDriver源码阅读笔记
			

		

		

									

				athrun的InstrumentDriver源码阅读笔记 作者:唯一 athrun是淘宝的开源测试项目,InstrumentDriver是ios端的实现,之前在公司项目中用过这个框架,没有深入了解,现在回来记录下. 官方介绍:http://code.taobao.org/p/athrun/wiki/instrumentDriver/ 优点:这个框架是对UIAutomation的java实现,在代码提示.用例维护方面比UIAutomation强多了,借junit4的光,我们可以通过junit4的			

		

	

				

		

			

                jdk源码阅读笔记之java集合框架（二）（ArrayList）
			

		

		

									

				关于ArrayList的分析,会从且仅从其添加(add)与删除(remove)方法入手. ArrayList类定义: p.p1 { margin: 0.0px 0.0px 0.0px 0.0px; font: 18.0px Monaco } span.s1 { color: #931a68 } public class ArrayList<E> extends AbstractList<E> implements List<E> ArrayList基本属性: /** *			

		

	

				

		

			

                Yii源码阅读笔记 - 日志组件
			

		

		

									

				?使用 Yii框架为开发者提供两个静态方法进行日志记录: Yii::log($message, $level, $category);Yii::trace($message, $category); 两者的区别在于后者依赖于应用开启调试模式,即定义常量YII_DEBUG: defined('YII_DEBUG') or define('YII_DEBUG', true); Yii::log方法的调用需要指定message的level和category.category是格式为“xxx.yyy.z			

		

	

				

		

			

                CI框架源码阅读笔记2 一切的入口 index.php
			

		

		

									

				上一节(CI框架源码阅读笔记1 - 环境准备.基本术语和框架流程)中,我们提到了CI框架的基本流程,这里这次贴出流程图,以备参考: 作为CI框架的入口文件,源码阅读,自然由此开始.在源码阅读的过程中,我们并不会逐行进行解释,而只解释核心的功能和实现. 1.       设置应用程序环境 define('ENVIRONMENT', 'development'); 这里的development可以是任何你喜欢的环境名称(比如dev,再如test),相对应的,你要在下面的switch case代码块中			

		

	

				

		

			

                Apache Storm源码阅读笔记
			

		

		

									

				欢迎转载,转载请注明出处. 楔子 自从建了Spark交流的QQ群之后,热情加入的同学不少,大家不仅对Spark很热衷对于Storm也是充满好奇.大家都提到一个问题就是有关storm内部实现机理的资料比较少,理解起来非常费劲. 尽管自己也陆续对storm的源码走读发表了一些博文,当时写的时候比较匆忙,有时候衔接的不是太好,此番做了一些整理,主要是针对TridentTopology部分,修改过的内容采用pdf格式发布,方便打印. 文章中有些内容的理解得益于徐明明和fxjwind两位的指点,非常感谢.