Binary/CIL: Fix enclosing callable of branch target.

Author: MathiasVP

binary/ql/lib/semmle/code/binary/ast/internal/CilInstructions.qll

@@ -366,6 +366,7 @@ abstract class CilBranchInstruction extends CilInstruction {
   CilInstruction getABranchTarget() {
     exists(CilMethod m, int delta |
       il_branch_target(this, delta) and
+      this.getEnclosingMethod() = m and
       hasMethodAndOffset(m, delta, result)
     )
   }

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

@@ -28,4 +28,16 @@ module StagedConsistencyInput<InstructionSig Input> {
     exists(i.getAPredecessor()) and
     not exists(i.getASuccessor())
   }
+
+  query predicate nonLocalSuccessor(Input::Function f1, Input::Function f2, Input::Instruction i, SuccessorType t) {
+    i.getEnclosingFunction() = f1 and
+    i.getSuccessor(t).getEnclosingFunction() = f2 and
+    f1 != f2
+  }
+
+  query predicate successorMissingFunction(Input::Function f, Input::Instruction i1, Input::Instruction i2, SuccessorType t) {
+    i1.getEnclosingFunction() = f and
+    i1.getSuccessor(t) = i2 and
+    not exists(i2.getEnclosingFunction())
+  }
 }

binary/ql/lib/semmle/code/binary/ast/ir/internal/Instruction0/Consistency.ql

@@ -1,5 +1,6 @@
 private import Instruction0
 import semmle.code.binary.ast.ir.internal.Consistency
+private import codeql.controlflow.SuccessorType
 import StagedConsistencyInput<Instruction0>
 private import TranslatedInstruction
 private import TranslatedFunction
@@ -30,3 +31,13 @@ query predicate nonUniqueResultVariable0(
   strictcount(ti.getResultVariable()) = k and
   k > 1
 }
+
+query predicate nonUniqueSuccessor0(
+  TranslatedFunction tf, InstructionTag tag, TranslatedInstruction ti, string s, SuccessorType t,
+  int k
+) {
+  tf = ti.getEnclosingFunction() and
+  s = concat(ti.getAQlClass().toString(), ", ") and
+  strictcount(ti.getSuccessor(tag, t)) = k and
+  k > 1
+}