KLEE实现——类的概览

组件对应类代码分析

./lib/Core/CoreStats.h //统计数据
./lib/Core/StatsTracker.h//状态追踪
./lib/Core/AddressSpace.h//地址空间 MemoryObject->ObjectState
./lib/Core/ExternalDispatcher.h//外部引用处理
./lib/Core/Memory.h//对象存储，类MemoryObject，类ObjectState
./lib/Core/Searcher.h//选择下一状态
./lib/Core/PTree.h//state存储为树状结构
./lib/Core/MemoryManager.h//管理MemoryObject
./lib/Core/TimingSolver.h//约束求解
./lib/Core/ImpliedValue.h//计算具体表达式嵌入的具体值
./lib/Core/SeedInfo.h//种子信息，getNextInput
./lib/Core/Executor.h//interpreter的具体类，管理state的执行
./lib/Core/ObjectHolder.h//对ObjectState的持有管理
./lib/Core/CallPathManager.h//调用路径管理
./lib/Core/Context.h//存储KLEE run全局信息的辅助类
./lib/Core/SpecialFunctionHandler.h//特殊函数处理，prepare,bind
./lib/Core/ExecutorTimerInfo.h//计时器
./lib/Core/UserSearcher.h//用户定制搜索？？？
./lib/Solver/STPBuilder.h
./lib/Solver/STPSolver.h
./lib/Solver/QueryLoggingSolver.h
./lib/Solver/Z3Solver.h
./lib/Solver/ConstantDivision.h
./lib/Solver/Z3Builder.h
./lib/Solver/MetaSMTSolver.h
./lib/Solver/MetaSMTBuilder.h
./lib/Module/Passes.h
./runtime/POSIX/fd.h//文件符号化
./tools/klee-replay/klee-replay.h
./test/Feature/utils.h
./include/expr/Lexer.h
./include/expr/Parser.h
./include/klee/SolverImpl.h
./include/klee/Internal/Support/ErrorHandling.h
./include/klee/Internal/Support/Debug.h
./include/klee/Internal/Support/CompressionStream.h
./include/klee/Internal/Support/IntEvaluation.h
./include/klee/Internal/Support/FileHandling.h
./include/klee/Internal/Support/FloatEvaluation.h
./include/klee/Internal/Support/Timer.h
./include/klee/Internal/Support/PrintVersion.h
./include/klee/Internal/Support/QueryLog.h
./include/klee/Internal/Support/ModuleUtil.h
./include/klee/Internal/System/Time.h
./include/klee/Internal/System/MemoryUsage.h
./include/klee/Internal/ADT/ImmutableTree.h//不可变树结构
./include/klee/Internal/ADT/ImmutableMap.h//不可变map结构
./include/klee/Internal/ADT/TreeStream.h
./include/klee/Internal/ADT/KTest.h//测试用例
./include/klee/Internal/ADT/DiscretePDF.h
./include/klee/Internal/ADT/ImmutableSet.h
./include/klee/Internal/ADT/MapOfSets.h
./include/klee/Internal/ADT/RNG.h
./include/klee/Internal/Module/LLVMPassManager.h
./include/klee/Internal/Module/KInstruction.h//对llvm::Instruction进行封装，得到struct KInstruction
./include/klee/Internal/Module/KInstIterator.h
./include/klee/Internal/Module/Cell.h
./include/klee/Internal/Module/KModule.h//LLVM bytecode被加载为module
./include/klee/Internal/Module/InstructionInfoTable.h//包含指令及其debug信息
./include/klee/util/Assignment.h
./include/klee/util/ExprPPrinter.h
./include/klee/util/ExprUtil.h
./include/klee/util/ExprHashMap.h
./include/klee/util/Ref.h
./include/klee/util/ExprVisitor.h
./include/klee/util/ExprSMTLIBPrinter.h
./include/klee/util/ExprRangeEvaluator.h
./include/klee/util/ArrayExprHash.h
./include/klee/util/Bits.h
./include/klee/util/PrintContext.h
./include/klee/util/ArrayCache.h//Array缓存
./include/klee/util/ExprEvaluator.h//表达式求解
./include/klee/util/BitArray.h
./include/klee/util/GetElementPtrTypeIterator.h
./include/klee/Constraints.h//约束
./include/klee/klee.h
./include/klee/Common.h//一些关于查询的参数
./include/klee/ExecutionState.h//程序状态，即一条执行路径
./include/klee/Config/Version.h
./include/klee/Solver.h//求解器
./include/klee/Statistic.h//统计信息
./include/klee/Statistics.h
./include/klee/Interpreter.h//解释器，抽象类
./include/klee/ExprBuilder.h
./include/klee/Expr.h//表达式
./include/klee/IncompleteSolver.h
./include/klee/SolverStats.h
./include/klee/TimerStatIncrementer.h
./include/klee/CommandLine.h//命令行参数