blob: 40e04389ddcceb97e5a317fd63b48206b49dcc27 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
//===-- Tree.h --------------------------------------------------*- C++ -*-===//
//
// The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
#pragma once
#include "klee/Core/BranchTypes.h"
#include "klee/Core/TerminationTypes.h"
#include <filesystem>
#include <string>
#include <unordered_map>
#include <unordered_set>
#include <variant>
#include <vector>
inline std::unordered_set<BranchType> validBranchTypes;
inline std::unordered_set<StateTerminationType> validTerminationTypes;
inline std::unordered_map<BranchType, std::string> branchTypeNames;
inline std::unordered_map<StateTerminationType, std::string>
terminationTypeNames;
///@brief A Tree node representing an ExecutionTreeNode
struct Node final {
std::uint32_t left{0};
std::uint32_t right{0};
std::uint32_t stateID{0};
std::uint32_t asmLine{0};
std::variant<BranchType, StateTerminationType> kind{BranchType::NONE};
};
///@brief An in-memory representation of a complete execution tree
class Tree final {
/// Creates branchTypeNames and terminationTypeNames maps
static void initialiseTypeNames();
/// Creates validBranchTypes and validTerminationTypes sets
static void initialiseValidTypes();
/// Checks tree properties (e.g. valid branch/termination types)
void sanityCheck();
public:
/// sorted vector of Nodes default initialised with BranchType::NONE
std::vector<Node> nodes; // ExecutionTree node IDs start with 1!
/// Reads complete exec-tree.db into memory
explicit Tree(const std::filesystem::path &path);
~Tree() = default;
};
|
