You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
63 lines
1.5 KiB
63 lines
1.5 KiB
#ifndef SYMBOLIC_INTERPRETER_H
|
|
#define SYMBOLIC_INTERPRETER_H
|
|
|
|
#include <cstdlib>
|
|
#include <map>
|
|
#include <stack>
|
|
#include <vector>
|
|
|
|
#include "z3++.h"
|
|
|
|
/// 结果输出目录
|
|
static const char *FormulaFile = "formula.smt2";
|
|
/// 输入读取目录
|
|
static const char *InputFile = "input.txt";
|
|
/// 日志：记录 Path Condition
|
|
static const char *LogFile = "log.txt";
|
|
/// 目前不清楚
|
|
static const char *BranchFile = "branch.txt";
|
|
|
|
class Address {
|
|
public:
|
|
enum Ty { Memory, Register };
|
|
Address(int *Ptr) : Type(Memory), Addr((uintptr_t)Ptr) {}
|
|
Address(int ID) : Type(Register), Addr(ID) {}
|
|
Address(z3::expr &R)
|
|
: Type(Register), Addr(std::stoi(R.to_string().substr(1))) {}
|
|
|
|
bool operator<(const Address &RHS) const {
|
|
return (Type < RHS.Type) || (Type == RHS.Type && Addr < RHS.Addr);
|
|
}
|
|
friend std::ostream &operator<<(std::ostream &OS, const Address &SE);
|
|
|
|
private:
|
|
Ty Type;
|
|
uintptr_t Addr;
|
|
};
|
|
|
|
using MemoryTy = std::map<Address, z3::expr>;
|
|
|
|
class SymbolicInterpreter {
|
|
public:
|
|
int NewInput(int *Ptr, int ID);
|
|
MemoryTy &getMemory() { return Mem; }
|
|
std::map<int, int> &getInputs() { return Inputs; }
|
|
z3::context &getContext() { return Ctx; }
|
|
std::stack<z3::expr> &getStack() { return Stack; }
|
|
std::vector<std::pair<int, z3::expr>> &getPathCondition() {
|
|
return PathCondition;
|
|
}
|
|
|
|
private:
|
|
MemoryTy Mem;
|
|
/// Inputs: <RegisteredId, Value>
|
|
std::map<int, int> Inputs;
|
|
int NumOfInputs = 0;
|
|
std::stack<z3::expr> Stack;
|
|
std::vector<std::pair<int, z3::expr>> PathCondition;
|
|
|
|
z3::context Ctx;
|
|
};
|
|
|
|
#endif // SYMBOLIC_INTERPRETER_H
|