Binary: Add support for two new instructions (return with value and instruction references. These are needed for CIL translation.

Author: MathiasVP

binary/ql/lib/semmle/code/binary/ast/ir/internal/Instruction0/Instruction.qll

@@ -131,6 +131,12 @@ class RetInstruction extends Instruction {
   override Opcode::Ret opcode;
 }
 
+class RetValueInstruction extends Instruction {
+  override Opcode::RetValue opcode;
+
+  UnaryOperand getReturnValueOperand() { result = this.getAnOperand() }
+}
+
 class InitInstruction extends Instruction {
   override Opcode::Init opcode;
 }
@@ -163,6 +169,21 @@ class CallInstruction extends Instruction {
   override string getImmediateValue() { result = this.getStaticTarget().getName() }
 }
 
+class InstrRefInstruction extends Instruction {
+  override Opcode::InstrRef opcode;
+
+  Instruction getReferencedInstruction() { result = te.getReferencedInstruction(tag) }
+
+  final override string getImmediateValue() {
+    exists(Instruction ref | ref = this.getReferencedInstruction() |
+      result = ref.getResultVariable().toString()
+      or
+      not exists(ref.getResultVariable()) and
+      result = "<reference to instruction without result>"
+    )
+  }
+}
+
 class BinaryInstruction extends Instruction {
   override Opcode::BinaryOpcode opcode;
 

binary/ql/lib/semmle/code/binary/ast/ir/internal/Instruction0/TranslatedElement.qll

@@ -14,7 +14,11 @@ class Opcode = Opcode::Opcode;
 
 private predicate shouldTranslateX86Instr(Raw::X86Instruction instr) { any() }
 
-private predicate shouldTranslateX86Operand(Raw::X86Operand operand) { any() }
+private predicate shouldTranslateX86Operand(Raw::X86Operand operand) {
+  // If it has a target we will synthesize an instruction reference instruction
+  // instead of translating the operand directly.
+  not exists(operand.getUse().(Raw::X86Jmp).getTarget())
+}
 
 newtype TTranslatedElement =
   TTranslatedX86Function(Raw::X86Instruction entry) {
@@ -88,6 +92,8 @@ abstract class TranslatedElement extends TTranslatedElement {
 
   int getConstantValue(InstructionTag tag) { none() }
 
+  Instruction getReferencedInstruction(InstructionTag tag) { none() }
+
   abstract Raw::Element getRawElement();
 
   abstract Instruction getSuccessor(InstructionTag tag, SuccessorType succType);

binary/ql/lib/semmle/code/binary/ast/ir/internal/Instruction0/TranslatedInstruction.qll

@@ -333,40 +333,66 @@ class TranslatedX86Jmp extends TranslatedX86Instruction, TTranslatedX86Jmp {
   final override predicate hasInstruction(
     Opcode opcode, InstructionTag tag, Option<Variable>::Option v
   ) {
-    tag = SingleTag() and
+    tag = X86JumpTag() and
     opcode instanceof Opcode::Jump and
     v.isNone() // A jump has no result
+    or
+    exists(instr.getTarget()) and
+    tag = X86JumpInstrRefTag() and
+    opcode instanceof Opcode::InstrRef and
+    v.asSome() = this.getVariable(X86JumpInstrRefVarTag())
   }
 
   override predicate producesResult() { any() }
 
+  override predicate hasTempVariable(VariableTag tag) {
+    exists(instr.getTarget()) and
+    tag = X86JumpInstrRefVarTag()
+  }
+
+  override Instruction getReferencedInstruction(InstructionTag tag) {
+    tag = X86JumpInstrRefTag() and
+    result = getTranslatedInstruction(instr.getTarget()).getEntry()
+  }
+
   override Variable getVariableOperand(InstructionTag tag, OperandTag operandTag) {
-    tag = SingleTag() and
+    tag = X86JumpTag() and
     operandTag = JumpTargetTag() and
-    result = this.getTranslatedOperand().getResultVariable()
+    if exists(instr.getTarget())
+    then result = this.getInstruction(X86JumpInstrRefTag()).getResultVariable()
+    else result = this.getTranslatedOperand().getResultVariable()
   }
 
   TranslatedOperand getTranslatedOperand() { result = getTranslatedOperand(instr.getOperand(0)) }
 
   override Instruction getChildSuccessor(TranslatedElement child, SuccessorType succType) {
+    not exists(instr.getTarget()) and
     child = this.getTranslatedOperand() and
     succType instanceof DirectSuccessor and
-    result = this.getInstruction(SingleTag())
+    result = this.getInstruction(X86JumpTag())
   }
 
   override Instruction getSuccessor(InstructionTag tag, SuccessorType succType) {
-    tag = SingleTag() and
+    exists(instr.getTarget()) and
+    tag = X86JumpInstrRefTag() and
+    succType instanceof DirectSuccessor and
+    result = this.getInstruction(X86JumpTag())
+    or
+    tag = X86JumpTag() and
     succType instanceof DirectSuccessor and
     result = getTranslatedInstruction(instr.getTarget()).getEntry()
   }
 
   override Instruction getEntry() {
-    exists(Option<Instruction>::Option op | op = this.getTranslatedOperand().getEntry() |
-      result = op.asSome()
-      or
-      op.isNone() and
-      result = this.getInstruction(SingleTag())
-    )
+    if exists(instr.getTarget())
+    then result = this.getInstruction(X86JumpInstrRefTag())
+    else
+      exists(Option<Instruction>::Option op | op = this.getTranslatedOperand().getEntry() |
+        result = op.asSome()
+        or
+        op.isNone() and
+        result = this.getInstruction(X86JumpTag())
+      )
   }
 
   override Variable getResultVariable() { none() }
@@ -728,13 +754,18 @@ class TranslatedX86ConditionalJump extends TranslatedX86Instruction, TTranslated
   final override predicate hasInstruction(
     Opcode opcode, InstructionTag tag, Option<Variable>::Option v
   ) {
+    exists(instr.getTarget()) and
+    tag = X86CJumpInstrRefTag() and
+    opcode instanceof Opcode::InstrRef and
+    v.asSome() = this.getVariable(X86CJumpInstrRefVarTag())
+    or
     opcode instanceof Opcode::CJump and
-    tag = SingleTag() and
+    tag = X86CJumpTag() and
     v.isNone() // A jump has no result
   }
 
   override predicate hasJumpCondition(InstructionTag tag, Opcode::ConditionKind kind) {
-    tag = SingleTag() and
+    tag = X86CJumpTag() and
     (
       instr instanceof Raw::X86Jb and kind = Opcode::LT()
       or
@@ -762,15 +793,29 @@ class TranslatedX86ConditionalJump extends TranslatedX86Instruction, TTranslated
     )
   }
 
+  override predicate hasTempVariable(VariableTag tag) {
+    exists(instr.getTarget()) and
+    tag = X86CJumpInstrRefVarTag()
+  }
+
+  override Instruction getReferencedInstruction(InstructionTag tag) {
+    tag = X86CJumpInstrRefTag() and
+    result = getTranslatedInstruction(instr.getTarget()).getEntry()
+  }
+
   override predicate hasSynthVariable(SynthRegisterTag tag) { tag = CmpRegisterTag() }
 
   override predicate producesResult() { any() }
 
   override Variable getVariableOperand(InstructionTag tag, OperandTag operandTag) {
-    tag = SingleTag() and
+    tag = X86CJumpTag() and
     (
       operandTag = CondJumpTargetTag() and
-      result = this.getTranslatedOperand().getResultVariable()
+      (
+        if exists(instr.getTarget())
+        then result = this.getInstruction(X86CJumpInstrRefTag()).getResultVariable()
+        else result = this.getTranslatedOperand().getResultVariable()
+      )
       or
       operandTag = CondTag() and
       result = getTranslatedVariableSynth(CmpRegisterTag())
@@ -780,13 +825,19 @@ class TranslatedX86ConditionalJump extends TranslatedX86Instruction, TTranslated
   TranslatedOperand getTranslatedOperand() { result = getTranslatedOperand(instr.getOperand(0)) }
 
   override Instruction getChildSuccessor(TranslatedElement child, SuccessorType succType) {
+    not exists(instr.getTarget()) and
     child = this.getTranslatedOperand() and
     succType instanceof DirectSuccessor and
-    result = this.getInstruction(SingleTag())
+    result = this.getInstruction(X86CJumpTag())
   }
 
   override Instruction getSuccessor(InstructionTag tag, SuccessorType succType) {
-    tag = SingleTag() and
+    exists(instr.getTarget()) and
+    tag = X86CJumpInstrRefTag() and
+    succType instanceof DirectSuccessor and
+    result = this.getInstruction(X86CJumpTag())
+    or
+    tag = X86CJumpTag() and
     (
       succType.(BooleanSuccessor).getValue() = true and
       result = getTranslatedInstruction(instr.getTarget()).getEntry()
@@ -797,12 +848,15 @@ class TranslatedX86ConditionalJump extends TranslatedX86Instruction, TTranslated
   }
 
   override Instruction getEntry() {
-    exists(Option<Instruction>::Option op | op = this.getTranslatedOperand().getEntry() |
-      result = op.asSome()
-      or
-      op.isNone() and
-      result = this.getInstruction(SingleTag())
-    )
+    if exists(instr.getTarget())
+    then result = this.getInstruction(X86CJumpInstrRefTag())
+    else
+      exists(Option<Instruction>::Option op | op = this.getTranslatedOperand().getEntry() |
+        result = op.asSome()
+        or
+        op.isNone() and
+        result = this.getInstruction(X86CJumpTag())
+      )
   }
 
   override Variable getResultVariable() { none() }
@@ -941,8 +995,6 @@ class TranslatedX86Lea extends TranslatedX86Instruction, TTranslatedX86Lea {
   override Variable getResultVariable() {
     result = this.getTranslatedDestOperand().getResultVariable()
   }
-
-  override string toString() { result = TranslatedX86Instruction.super.toString() }
 }
 
 class TranslatedX86Pop extends TranslatedX86Instruction, TTranslatedX86Pop {

binary/ql/lib/semmle/code/binary/ast/ir/internal/Instruction1/Instruction1.qll

@@ -289,6 +289,8 @@ private module InstructionInput implements Transform<Instruction0>::TransformInp
       InstructionTag tag, SuccessorType succType
     );
 
+    EitherInstructionTranslatedElementTagPair getReferencedInstruction(InstructionTag tag) { none() }
+
     abstract EitherInstructionTranslatedElementTagPair getInstructionSuccessor(
       Instruction0::Instruction i, SuccessorType succType
     );

binary/ql/lib/semmle/code/binary/ast/ir/internal/Instruction2/Instruction2.qll

@@ -259,6 +259,10 @@ module InstructionInput implements Transform<Instruction1>::TransformInputSig {
 
     int getConstantValue(InstructionTag tag) { none() }
 
+    EitherInstructionTranslatedElementTagPair getReferencedInstruction(InstructionTag tag) {
+      none()
+    }
+
     predicate hasJumpCondition(InstructionTag tag, ConditionKind kind) { none() }
 
     predicate hasTempVariable(VariableTag tag) { none() }

binary/ql/lib/semmle/code/binary/ast/ir/internal/InstructionSig.qll

@@ -110,6 +110,10 @@ signature module InstructionSig {
 
   class RetInstruction extends Instruction;
 
+  class RetValueInstruction extends Instruction {
+    UnaryOperand getReturnValueOperand();
+  }
+
   class BinaryInstruction extends Instruction {
     LeftOperand getLeftOperand();
 
@@ -148,6 +152,10 @@ signature module InstructionSig {
     JumpTargetOperand getJumpTargetOperand();
   }
 
+  class InstrRefInstruction extends Instruction {
+    Instruction getReferencedInstruction();
+  }
+
   class CopyInstruction extends Instruction {
     UnaryOperand getOperand();
   }

binary/ql/lib/semmle/code/binary/ast/ir/internal/InstructionTag.qll

@@ -2,6 +2,10 @@ private import Opcode
 
 newtype TInstructionTag =
   SingleTag() or
+  X86JumpInstrRefTag() or
+  X86JumpTag() or
+  X86CJumpInstrRefTag() or
+  X86CJumpTag() or
   WriteTag() or
   InitFramePtrTag() or
   InitStackPtrTag() or
@@ -42,6 +46,18 @@ class InstructionTag extends TInstructionTag {
     this = SingleTag() and
     result = "Single"
     or
+    this = X86JumpInstrRefTag() and
+    result = "X86JumpInstrRef"
+    or
+    this = X86JumpTag() and
+    result = "X86Jump"
+    or
+    this = X86CJumpInstrRefTag() and
+    result = "X86CJumpInstrRef"
+    or
+    this = X86CJumpTag() and
+    result = "X86CJump"
+    or
     this = WriteTag() and
     result = "Write"
     or
@@ -134,6 +150,8 @@ class InstructionTag extends TInstructionTag {
 }
 
 newtype VariableTag =
+  X86JumpInstrRefVarTag() or
+  X86CJumpInstrRefVarTag() or
   TestVarTag() or
   ZeroVarTag() or
   ImmediateOperandVarTag() or
@@ -162,6 +180,12 @@ string stringOfSynthRegisterTag(SynthRegisterTag tag) {
 }
 
 string stringOfVariableTag(VariableTag tag) {
+  tag = X86JumpInstrRefVarTag() and
+  result = "j_ir"
+  or
+  tag = X86CJumpInstrRefVarTag() and
+  result = "cj_ir"
+  or
   tag = TestVarTag() and
   result = "t"
   or

binary/ql/lib/semmle/code/binary/ast/ir/internal/Opcode.qll

@@ -19,10 +19,12 @@ private newtype TOpcode =
   TCopy() or
   TJump() or
   TCJump() or
+  TRetValue() or
   TRet() or
   TNop() or
   TNot() or
-  TInit()
+  TInit() or
+  TInstrRef()
 
 class Opcode extends TOpcode {
   string toString() { none() }
@@ -116,6 +118,10 @@ class Ret extends Opcode, TRet {
   override string toString() { result = "Ret" }
 }
 
+class RetValue extends Opcode, TRetValue {
+  override string toString() { result = "RetValue" }
+}
+
 class Nop extends Opcode, TNop {
   override string toString() { result = "Nop" }
 }
@@ -124,6 +130,10 @@ class Not extends Opcode, TNot {
   override string toString() { result = "Not" }
 }
 
+class InstrRef extends Opcode, TInstrRef {
+  override string toString() { result = "InstrRef" }
+}
+
 class Init extends Opcode, TInit {
   override string toString() { result = "Init" }
 }