x86: Abstract away rsp and rbp.

Author: MathiasVP

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

@@ -42,11 +42,11 @@ class TranslatedX86Function extends TranslatedFunction, TTranslatedX86Function {
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, Option<Variable>::Option v) {
     tag = InitStackPtrTag() and
     opcode instanceof Opcode::Init and
-    v.asSome() = getTranslatedVariableReal(any(Raw::RspRegister r)) // TODO: This assumes rsp is present in the DB
+    v.asSome() = getStackPointer()
     or
     tag = InitFramePtrTag() and
     opcode instanceof Opcode::Init and
-    v.asSome() = getTranslatedVariableReal(any(Raw::RbpRegister r)) // TODO: This assumes rsp is present in the DB
+    v.asSome() = getFramePointer()
   }
 
   override Instruction getSuccessor(InstructionTag tag, SuccessorType succType) {

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

@@ -525,8 +525,6 @@ class TranslatedX86Movdqa extends TranslatedCopy, TTranslatedX86Movdqa {
   TranslatedX86Movdqa() { this = TTranslatedX86Movdqa(instr) }
 }
 
-private Variable getEspVariable() { result = getTranslatedVariableReal(any(Raw::RspRegister r)) }
-
 class TranslatedX86Push extends TranslatedX86Instruction, TTranslatedX86Push {
   override Raw::X86Push instr;
 
@@ -545,7 +543,7 @@ class TranslatedX86Push extends TranslatedX86Instruction, TTranslatedX86Push {
     // esp = esp - x
     tag = PushSubTag() and
     opcode instanceof Opcode::Sub and
-    v.asSome() = getEspVariable()
+    v.asSome() = getStackPointer()
     or
     // store [esp], y
     tag = PushStoreTag() and
@@ -564,7 +562,7 @@ class TranslatedX86Push extends TranslatedX86Instruction, TTranslatedX86Push {
     tag = PushSubTag() and
     (
       operandTag = LeftTag() and
-      result = getEspVariable()
+      result = getStackPointer()
       or
       operandTag = RightTag() and
       result = this.getInstruction(PushSubConstTag()).getResultVariable()
@@ -576,7 +574,7 @@ class TranslatedX86Push extends TranslatedX86Instruction, TTranslatedX86Push {
       result = this.getTranslatedOperand().getResultVariable()
       or
       operandTag = StoreAddressTag() and
-      result = getEspVariable()
+      result = getStackPointer()
     )
   }
 
@@ -969,7 +967,7 @@ class TranslatedX86Pop extends TranslatedX86Instruction, TTranslatedX86Pop {
     // esp = esp + x
     tag = PopAddTag() and
     opcode instanceof Opcode::Add and
-    v.asSome() = getEspVariable()
+    v.asSome() = getStackPointer()
   }
 
   override int getConstantValue(InstructionTag tag) {
@@ -982,12 +980,12 @@ class TranslatedX86Pop extends TranslatedX86Instruction, TTranslatedX86Pop {
   override Variable getVariableOperand(InstructionTag tag, OperandTag operandTag) {
     tag = PopLoadTag() and
     operandTag = UnaryTag() and
-    result = getEspVariable()
+    result = getStackPointer()
     or
     tag = PopAddTag() and
     (
       operandTag = LeftTag() and
-      result = getEspVariable()
+      result = getStackPointer()
       or
       operandTag = RightTag() and
       result = this.getInstruction(PopAddConstTag()).getResultVariable()

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

@@ -6,7 +6,12 @@ private import Operand
 
 newtype TVariable =
   TTempVariable(TranslatedElement te, Tags::VariableTag tag) { hasTempVariable(te, tag) } or
-  TRegisterVariableReal(Raw::X86Register r) or
+  TStackPointer() or
+  TFramePointer() or
+  TRegisterVariableReal(Raw::X86Register r) {
+    not r instanceof Raw::RbpRegister and // Handled by FramePointer
+    not r instanceof Raw::RspRegister // Handled by StackPointer
+  } or
   TRegisterVariableSynth(Tags::SynthRegisterTag tag) { hasSynthVariable(tag) }
 
 abstract class Variable extends TVariable {
@@ -26,6 +31,18 @@ class TempVariable extends Variable, TTempVariable {
   override string toString() { result = te.getDumpId() + "." + Tags::stringOfVariableTag(tag) }
 }
 
+class StackPointer extends Variable, TStackPointer {
+  override string toString() { result = "sp" }
+}
+
+Variable getStackPointer() { result instanceof StackPointer }
+
+class FramePointer extends Variable, TFramePointer {
+  override string toString() { result = "fp" }
+}
+
+Variable getFramePointer() { result instanceof FramePointer }
+
 class TRegisterVariable = TRegisterVariableReal or TRegisterVariableSynth;
 
 class RegisterVariable extends Variable, TRegisterVariable {
@@ -46,7 +63,13 @@ private class RegisterVariableReal extends RegisterVariable, TRegisterVariableRe
   override Raw::X86Register getRegister() { result = r }
 }
 
-RegisterVariable getTranslatedVariableReal(Raw::X86Register r) { result.getRegister() = r }
+Variable getTranslatedVariableReal(Raw::X86Register r) {
+  result.(RegisterVariable).getRegister() = r
+  or
+  r instanceof Raw::RspRegister and result instanceof StackPointer
+  or
+  r instanceof Raw::RbpRegister and result instanceof FramePointer
+}
 
 private class RegisterVariableSynth extends RegisterVariable, TRegisterVariableSynth {
   Tags::SynthRegisterTag tag;