@@ -14,20 +14,47 @@ private import TranslatedFunction
1414
1515class Opcode = Opcode:: Opcode ;
1616
17+ /**
18+ * Holds if the instruction `instr` should be translated into IR.
19+ */
1720private predicate shouldTranslateX86Instr ( Raw:: X86Instruction instr ) { any ( ) }
1821
22+ /**
23+ * Holds if the operand `operand` should be translated into IR.
24+ */
1925private predicate shouldTranslateX86Operand ( Raw:: X86Operand operand ) {
2026 // If it has a target we will synthesize an instruction reference instruction
2127 // instead of translating the operand directly.
2228 not exists ( operand .getUse ( ) .( Raw:: X86Jmp ) .getTarget ( ) )
2329}
2430
31+ /**
32+ * Holds if the instruction `instr` should be translated into IR.
33+ */
2534private predicate shouldTranslateCilInstr ( Raw:: CilInstruction instr ) { any ( ) }
2635
36+ /**
37+ * Holds if the method `m` should be translated into IR.
38+ */
2739private predicate shouldTranslateMethod ( Raw:: CilMethod m ) { any ( ) }
2840
41+ /**
42+ * Holds if the parameter `p` should be translated into IR.
43+ */
2944private predicate shouldTranslateCilParameter ( Raw:: CilParameter p ) { any ( ) }
3045
46+ /**
47+ * The "base type" for all translated elements.
48+ *
49+ * To add support for a new instruction do the following:
50+ * - Define a new branch of this type.
51+ * - Add a new class in `TranslatedInstruction.qll` that extends `TranslatedInstruction` (or
52+ * a more specific subclass such as `TranslatedX86Instruction`. `TranslatedCilInstruction`, etc).
53+ * - Implement the abstract predicates required by the base class. Pay special attention to whether
54+ * you also need to implement certain predicates that have a default `none()` implementation. This
55+ * is necessary when you want to define a new temporary variable or local variable that is written
56+ * to by the instruction.
57+ */
3158newtype TTranslatedElement =
3259 TTranslatedX86Function ( Raw:: X86Instruction entry ) {
3360 shouldTranslateX86Instr ( entry ) and
@@ -113,58 +140,152 @@ TranslatedCilInstruction getTranslatedCilInstruction(Raw::CilInstruction raw) {
113140}
114141
115142abstract class TranslatedElement extends TTranslatedElement {
143+ /**
144+ * Holds if this translated element generated an instruction with opcode `opcode` that stores
145+ * the result of the instruction in `v` (unless `v.isNone()` holds. In that case the instruction
146+ * does not produce a result).
147+ *
148+ * To obtain the instruction of this `TranslatedElement`, use `this.getInstruction(tag)`.
149+ */
116150 abstract predicate hasInstruction ( Opcode opcode , InstructionTag tag , Option< Variable > :: Option v ) ;
117151
152+ /**
153+ * Holds if this translated elements generates a temporary variable with the given tag.
154+ *
155+ * The variable is "temporary" in the sense that two different translated elements may reuse
156+ * the `tag` and they will refer to different variables. This is unlike local variables, which
157+ * are unique per function.
158+ */
118159 predicate hasTempVariable ( TempVariableTag tag ) { none ( ) }
119160
161+ /**
162+ * Holds if this translated element generates a `CJump` instruction when given the tag `tag`, and
163+ * the condition kind of the jump is `kind`.
164+ */
120165 predicate hasJumpCondition ( InstructionTag tag , Opcode:: ConditionKind kind ) { none ( ) }
121166
167+ /**
168+ * Holds if this translated element generates a local variable with the given tag.
169+ */
122170 predicate hasLocalVariable ( LocalVariableTag tag ) { none ( ) }
123171
172+ /**
173+ * Gets the local variable with the given tag.
174+ */
124175 final Variable getLocalVariable ( LocalVariableTag tag ) {
125176 result = TLocalVariable ( this .getEnclosingFunction ( ) , tag )
126177 }
127178
128- Variable getVariable ( TempVariableTag tag ) { result = TTempVariable ( this , tag ) }
179+ /**
180+ * Gets the temporary variable with the given tag.
181+ */
182+ Variable getTempVariable ( TempVariableTag tag ) { result = TTempVariable ( this , tag ) }
129183
184+ /**
185+ * Gets the instruction with the given tag.
186+ */
130187 final Instruction getInstruction ( InstructionTag tag ) { result = MkInstruction ( this , tag ) }
131188
189+ /**
190+ * Gets the constant value of the instruction with the given tag. This `tag` must refer to
191+ * a constant instruction (that is, an instruction for which `hasInstruction(Opcode::Const, tag, _)`
192+ * holds.).
193+ */
132194 int getConstantValue ( InstructionTag tag ) { none ( ) }
133195
196+ /**
197+ * Gets the string constant of the instruction with the given tag. This `tag` must refer to
198+ * a string constant instruction (that is, an instruction for which `hasInstruction(Opcode::Const, tag, _)`
199+ * holds.)
200+ */
134201 string getStringConstant ( InstructionTag tag ) { none ( ) }
135202
203+ /**
204+ * Gets the external name referenced by the instruction with the given tag. This `tag` must refer to
205+ * an `ExternalRef` (that is, an instruction for which `hasInstruction(Opcode::ExternalRef, tag, _)`
206+ * holds.)
207+ */
136208 string getExternalName ( InstructionTag tag ) { none ( ) }
137209
210+ /**
211+ * Gets the instruction referenced by the instruction with the given tag. This `tag` must refer to
212+ * an `InstrRef` (that is, an instruction for which `hasInstruction(Opcode::InstrRef, tag, _)` holds.)
213+ */
138214 Instruction getReferencedInstruction ( InstructionTag tag ) { none ( ) }
139215
216+ /**
217+ * Gets the raw element that this translated element is a translation of.
218+ *
219+ * This predicate is important for linking back to the original AST.
220+ */
140221 abstract Raw:: Element getRawElement ( ) ;
141222
223+ /**
224+ * Gets the instruction that should be the successor of the instruction with the given tag
225+ * and successor type. The successor type what kind of successor it is. In 99% of the cases
226+ * this will be a `DirectSuccessor` (to represent that we proceed to the next instruction in
227+ * the normal control flow). In case of conditional jumps, this may also be an
228+ * `BooleanSuccessor` to represent that we may proceed to one of two different instructions
229+ * depending on the value of a condition.
230+ */
142231 abstract Instruction getSuccessor ( InstructionTag tag , SuccessorType succType ) ;
143232
233+ /**
234+ * Gets the successor instruction of the given child translated element for the given successor type.
235+ * This predicate is rarely used for translating CIL instructions since they tend to not have children
236+ * (but rather have simple integer operands). For X86 instructions with complex operands (such as memory
237+ * operands) this predicate is used.
238+ */
144239 abstract Instruction getChildSuccessor ( TranslatedElement child , SuccessorType succType ) ;
145240
146241 /**
147- * Gets the variable that should be given as the operandTag operand of the instruction with the given tag.
242+ * Gets the variable referred to by the `operandTag` operand of the instruction with the given `tag`.
243+ * An operand _must_ refer to exactly 1 operand.
148244 */
149245 abstract Variable getVariableOperand ( InstructionTag tag , OperandTag operandTag ) ;
150246
247+ /**
248+ * Holds if this is the translated element that produces the result of an instruction/operand. For a given
249+ * instruction there should be exactly one `TranslatedElement` for which:
250+ * 1. `getRawElement()` returns the instruction, and
251+ * 2. ``producesResult()`` holds.
252+ */
151253 abstract predicate producesResult ( ) ;
152254
255+ /**
256+ * Gets the variable that holds the result after executing the instruction represented by this
257+ * translated element.
258+ */
153259 abstract Variable getResultVariable ( ) ;
154260
155261 abstract string toString ( ) ;
156262
157263 abstract string getDumpId ( ) ;
158264
265+ /**
266+ * Gets the `TranslatedFunction` that is called when `tag` represents a call instruction.
267+ */
159268 TranslatedFunction getStaticCallTarget ( InstructionTag tag ) { none ( ) }
160269
270+ /**
271+ * Gets the enclosing translated function of this translated element.
272+ */
161273 abstract TranslatedFunction getEnclosingFunction ( ) ;
162274}
163275
276+ /**
277+ * Holds if the translated element `te` has an instruction with the given `tag`.
278+ */
164279predicate hasInstruction ( TranslatedElement te , InstructionTag tag ) { te .hasInstruction ( _, tag , _) }
165280
281+ /**
282+ * Holds if the translated element `te` has a temporary variable with the given `tag`.
283+ */
166284predicate hasTempVariable ( TranslatedElement te , TempVariableTag tag ) { te .hasTempVariable ( tag ) }
167285
286+ /**
287+ * Holds if the translated element `te` has a local variable with the given `tag`.
288+ */
168289predicate hasLocalVariable ( TranslatedFunction tf , LocalVariableTag tag ) {
169290 exists ( TranslatedElement te |
170291 te .getEnclosingFunction ( ) = tf and
0 commit comments