Binary: Add public-facing SSA predicates.

Author: MathiasVP

binary/ql/lib/semmle/code/binary/ast/ir/IR.qll

@@ -3,6 +3,7 @@ import codeql.controlflow.SuccessorType
 private import semmle.code.binary.ast.ir.internal.Opcode
 private import semmle.code.binary.ast.ir.internal.Tags
 private import codeql.controlflow.BasicBlock as BB
+private import semmle.code.binary.dataflow.Ssa
 
 private module FinalInstruction {
   private import internal.Instruction2.Instruction2::Instruction2 as Instruction
@@ -33,6 +34,10 @@ private module FinalInstruction {
     OperandTag getOperandTag() { result = super.getOperandTag() }
 
     Location getLocation() { result = super.getLocation() }
+
+    Ssa::Definition getDef() { result.getARead() = this }
+
+    Instruction getAnyDef() { result = this.getDef().getAnUltimateDefinition().asInstruction() }
   }
 
   class StoreValueOperand extends Operand instanceof Instruction::StoreValueOperand { }
@@ -227,6 +232,8 @@ private module FinalInstruction {
     InstructionTag getInstructionTag() { result = super.getInstructionTag() }
 
     Operand getFirstOperand() { result = super.getFirstOperand() }
+
+    Operand getAUse() { result.getDef().asInstruction() = this }
   }
 
   class RetInstruction extends Instruction instanceof Instruction::RetInstruction { }

binary/ql/lib/semmle/code/binary/dataflow/Ssa.qll

@@ -9,8 +9,6 @@ module Ssa {
   private import semmle.code.binary.ast.ir.IR
   private import internal.SsaImpl as SsaImpl
 
-  class Variable = SsaImpl::SsaInput::SourceVariable;
-
   /** A static single assignment (SSA) definition. */
   class Definition extends SsaImpl::Definition {
     final ControlFlowNode getControlFlowNode() {
@@ -28,6 +26,8 @@ module Ssa {
       not result instanceof PhiDefinition
     }
 
+    Instruction asInstruction() { result = this.getControlFlowNode().asInstruction() }
+
     /** Gets the function of this SSA definition. */
     Function getFunction() { result = this.getBasicBlock().getEnclosingFunction() }
   }
@@ -45,9 +45,7 @@ module Ssa {
     /** Gets the underlying write access. */
     final Instruction getWriteAccess() { result = write }
 
-    predicate assigns(Operand value) {
-      value = write.(CopyInstruction).getOperand()
-    }
+    predicate assigns(Operand value) { value = write.(CopyInstruction).getOperand() }
   }
 
   class PhiDefinition extends Definition, SsaImpl::PhiDefinition {

binary/ql/lib/semmle/code/binary/dataflow/internal/SsaImpl.qll

@@ -6,21 +6,15 @@ private predicate variableReadCertain(BasicBlock bb, int i, Operand va, Variable
   va = v.getAnAccess()
 }
 
-module SsaInput implements SsaImplCommon::InputSig<Location, BinaryCfg::BasicBlock> {
+private module SsaInput implements SsaImplCommon::InputSig<Location, BasicBlock> {
   class SourceVariable = Variable;
 
-  predicate variableWrite(BinaryCfg::BasicBlock bb, int i, SourceVariable v, boolean certain) {
-    v = bb.getNode(i).asInstruction().getResultVariable() and
+  predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
+    bb.getNode(i).asInstruction().getResultVariable() = v and
     certain = true
-    // or
-    // certain = true and
-    // bb.isFunctionEntryBasicBlock() and
-    // i = -1 and
-    // // TODO: Generalize beyond rsp
-    // v.(RegisterVariable).getRegister().toString() = "rsp"
   }
 
-  predicate variableRead(BinaryCfg::BasicBlock bb, int i, SourceVariable v, boolean certain) {
+  predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
     variableReadCertain(bb, i, _, v) and certain = true
   }
 }