Binary: Fix some consistency errors.

Author: MathiasVP

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

@@ -43,11 +43,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() = getStackPointer()
+    v.asSome() = this.getLocalVariable(X86RegisterTag(any(Raw::RspRegister sp)))
     or
     tag = InitFramePtrTag() and
     opcode instanceof Opcode::Init and
-    v.asSome() = getFramePointer()
+    v.asSome() = this.getLocalVariable(X86RegisterTag(any(Raw::RbpRegister fp)))
   }
 
   override Instruction getSuccessor(InstructionTag tag, SuccessorType succType) {
@@ -58,7 +58,7 @@ class TranslatedX86Function extends TranslatedFunction, TTranslatedX86Function {
     tag = InitStackPtrTag() and
     succType instanceof DirectSuccessor and
     result = getTranslatedInstruction(entry).getEntry()
-    }
+  }
 
   override predicate hasLocalVariable(LocalVariableTag tag) {
     tag = X86RegisterTag(any(Raw::RspRegister sp))

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

@@ -32,6 +32,10 @@ abstract class TranslatedX86Instruction extends TranslatedInstruction {
     or
     result = getTranslatedInstruction(instr.getAPredecessor()).getEnclosingFunction()
   }
+
+  final StackPointer getStackPointer() {
+    result = this.getLocalVariable(X86RegisterTag(any(Raw::RspRegister sp)))
+  }
 }
 
 abstract class TranslatedCilInstruction extends TranslatedInstruction {
@@ -600,7 +604,7 @@ class TranslatedX86Push extends TranslatedX86Instruction, TTranslatedX86Push {
     // esp = esp - x
     tag = PushSubTag() and
     opcode instanceof Opcode::Sub and
-    v.asSome() = getStackPointer()
+    v.asSome() = this.getStackPointer()
     or
     // store [esp], y
     tag = PushStoreTag() and
@@ -619,7 +623,7 @@ class TranslatedX86Push extends TranslatedX86Instruction, TTranslatedX86Push {
     tag = PushSubTag() and
     (
       operandTag = LeftTag() and
-      result = getStackPointer()
+      result = this.getStackPointer()
       or
       operandTag = RightTag() and
       result = this.getInstruction(PushSubConstTag()).getResultVariable()
@@ -631,7 +635,7 @@ class TranslatedX86Push extends TranslatedX86Instruction, TTranslatedX86Push {
       result = this.getTranslatedOperand().getResultVariable()
       or
       operandTag = StoreAddressTag() and
-      result = getStackPointer()
+      result = this.getStackPointer()
     )
   }
 
@@ -1050,7 +1054,7 @@ class TranslatedX86Pop extends TranslatedX86Instruction, TTranslatedX86Pop {
     // esp = esp + x
     tag = PopAddTag() and
     opcode instanceof Opcode::Add and
-    v.asSome() = getStackPointer()
+    v.asSome() = this.getStackPointer()
   }
 
   override int getConstantValue(InstructionTag tag) {
@@ -1062,13 +1066,13 @@ class TranslatedX86Pop extends TranslatedX86Instruction, TTranslatedX86Pop {
 
   override Variable getVariableOperand(InstructionTag tag, OperandTag operandTag) {
     tag = PopLoadTag() and
-    operandTag = UnaryTag() and
-    result = getStackPointer()
+    operandTag = LoadAddressTag() and
+    result = this.getStackPointer()
     or
     tag = PopAddTag() and
     (
       operandTag = LeftTag() and
-      result = getStackPointer()
+      result = this.getStackPointer()
       or
       operandTag = RightTag() and
       result = this.getInstruction(PopAddConstTag()).getResultVariable()
@@ -1766,7 +1770,9 @@ class TranslatedCilUnconditionalBranch extends TranslatedCilInstruction,
     result = this.getInstruction(CilUnconditionalBranchRefTag()).getResultVariable()
   }
 
-  override predicate hasTempVariable(TempVariableTag tag) { tag = CilUnconditionalBranchRefVarTag() }
+  override predicate hasTempVariable(TempVariableTag tag) {
+    tag = CilUnconditionalBranchRefVarTag()
+  }
 
   override Instruction getReferencedInstruction(InstructionTag tag) {
     tag = CilUnconditionalBranchRefTag() and

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

@@ -32,14 +32,10 @@ class StackPointer extends LocalVariable {
   StackPointer() { this.getTag() = X86RegisterTag(any(Raw::RspRegister sp)) }
 }
 
-Variable getStackPointer() { result instanceof StackPointer }
-
 class FramePointer extends LocalVariable {
   FramePointer() { this.getTag() = X86RegisterTag(any(Raw::RbpRegister fp)) }
 }
 
-Variable getFramePointer() { result instanceof FramePointer }
-
 class LocalVariable extends Variable, TLocalVariable {
   TranslatedFunction tf;
   LocalVariableTag tag;

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

@@ -285,18 +285,38 @@ module InstructionInput implements Transform<Instruction0>::TransformInputSig {
     )
   }
 
-  predicate isRemovedInstruction(Instruction0::Instruction instr) {
-    exists(TTranslatedLoad(instr))
-    or
-    exists(TTranslatedStore(instr))
+  private predicate isRemovedAddress0(Instruction0::Instruction instr) {
+    exists(Ssa::Definition def | instr = def.getInstruction() |
+      exists(Instruction0::LoadInstruction load |
+        exists(TTranslatedLoad(load)) and
+        load.getOperand() = unique(| | def.getARead())
+      )
+      or
+      exists(Instruction0::StoreInstruction store |
+        exists(TTranslatedStore(store)) and
+        store.getAddressOperand() = unique(| | def.getARead())
+      )
+    )
+  }
+
+  private predicate isRemovedAddress(Instruction0::Instruction instr) {
+    isRemovedAddress0(instr)
     or
     exists(Ssa::Definition def |
       def.getInstruction() = instr and
       def.getSourceVariable() instanceof Instruction0::TempVariable and
-      forex(Instruction0::Operand op | op = def.getARead() | isRemovedInstruction(op.getUse())) // TODO: Recursion through forex is bad for performance
+      forex(Instruction0::Operand op | op = def.getARead() | isRemovedAddress(op.getUse())) // TODO: Recursion through forex is bad for performance
     )
   }
 
+  predicate isRemovedInstruction(Instruction0::Instruction instr) {
+    exists(TTranslatedLoad(instr))
+    or
+    exists(TTranslatedStore(instr))
+    or
+    isRemovedAddress(instr)
+  }
+
   abstract class TranslatedElement extends TTranslatedElement {
     abstract EitherInstructionTranslatedElementTagPair getSuccessor(
       InstructionTag tag, SuccessorType succType

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

@@ -724,7 +724,16 @@ module Transform<InstructionSig Input> {
           result = getNewInstruction(oldSucc)
         )
         or
-        result = getInstructionSuccessor(old, succType)
+        exists(Instruction i | i = getInstructionSuccessor(old, succType) |
+          exists(Input::Instruction iOld | i = TOldInstruction(iOld) |
+            if TransformInput::isRemovedInstruction(iOld)
+            then result = TOldInstruction(getNonRemovedSuccessor(iOld, _))
+            else result = i
+          )
+          or
+          not i instanceof OldInstruction and
+          result = i
+        )
       }
 
       override Location getLocation() { result = old.getLocation() }