1 //===-- KInstruction.h ------------------------------------------*- C++ -*-===//
2 //
3 //                     The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #ifndef KLEE_KINSTRUCTION_H
11 #define KLEE_KINSTRUCTION_H
12 
13 #include "klee/Config/Version.h"
14 #include "klee/Module/InstructionInfoTable.h"
15 
16 #include "llvm/Support/DataTypes.h"
17 #include "llvm/Support/raw_ostream.h"
18 
19 #include <vector>
20 
21 namespace llvm {
22   class Instruction;
23 }
24 
25 namespace klee {
26   class Executor;
27   struct InstructionInfo;
28   class KModule;
29 
30 
31   /// KInstruction - Intermediate instruction representation used
32   /// during execution.
33   struct KInstruction {
34     llvm::Instruction *inst;
35     const InstructionInfo *info;
36 
37     /// Value numbers for each operand. -1 is an invalid value,
38     /// otherwise negative numbers are indices (negated and offset by
39     /// 2) into the module constant table and positive numbers are
40     /// register indices.
41     int *operands;
42     /// Destination register index.
43     unsigned dest;
44 
45   public:
46     virtual ~KInstruction();
47     std::string getSourceLocation() const;
48 
49   };
50 
51   struct KGEPInstruction : KInstruction {
52     /// indices - The list of variable sized adjustments to add to the pointer
53     /// operand to execute the instruction. The first element is the operand
54     /// index into the GetElementPtr instruction, and the second element is the
55     /// element size to multiple that index by.
56     std::vector< std::pair<unsigned, uint64_t> > indices;
57 
58     /// offset - A constant offset to add to the pointer operand to execute the
59     /// instruction.
60     uint64_t offset;
61   };
62 }
63 
64 #endif /* KLEE_KINSTRUCTION_H */
65