C++: fix duplicated UnreachedInstruction in raw IR

cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/internal/SSAConstruction.qll

@@ -34,9 +34,13 @@ private module Cached {
 
   cached
   predicate hasUnreachedInstructionCached(IRFunction irFunc) {
-    exists(OldInstruction oldInstruction |
+    exists(OldIR::Instruction oldInstruction |
       irFunc = oldInstruction.getEnclosingIRFunction() and
-      Reachability::isInfeasibleInstructionSuccessor(oldInstruction, _)
+      (
+        Reachability::isInfeasibleInstructionSuccessor(oldInstruction, _)
+        or
+        oldInstruction.getOpcode() instanceof Opcode::Unreached
+      )
     )
   }
 
@@ -366,21 +370,19 @@ private module Cached {
     then
       result = getChi(getOldInstruction(instruction)) and
       kind instanceof GotoEdge
-    else (
+    else
       exists(OldInstruction oldInstruction |
-        oldInstruction = getOldInstruction(instruction) and
+        (
+          oldInstruction = getOldInstruction(instruction)
+          or
+          instruction = getChi(oldInstruction)
+        ) and
         (
           if Reachability::isInfeasibleInstructionSuccessor(oldInstruction, kind)
           then result = unreachedInstruction(instruction.getEnclosingIRFunction())
           else result = getNewInstruction(oldInstruction.getSuccessor(kind))
         )
       )
-      or
-      exists(OldInstruction oldInstruction |
-        instruction = getChi(oldInstruction) and
-        result = getNewInstruction(oldInstruction.getSuccessor(kind))
-      )
-    )
   }
 
   cached

cpp/ql/lib/semmle/code/cpp/ir/implementation/internal/TInstruction.qll

@@ -19,6 +19,9 @@ newtype TInstruction =
   ) {
     IRConstruction::Raw::hasInstruction(tag1, tag2)
   } or
+  TRawUnreachedInstruction(IRFunctionBase irFunc) {
+    IRConstruction::hasUnreachedInstruction(irFunc)
+  } or
   TUnaliasedSsaPhiInstruction(
     TRawInstruction blockStartInstr, UnaliasedSsa::Ssa::MemoryLocation memoryLocation
   ) {

cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/IRConstruction.qll

@@ -171,9 +171,9 @@ module Raw {
   }
 }
 
-class TStageInstruction = TRawInstruction;
+class TStageInstruction = TRawInstruction or TRawUnreachedInstruction;
 
-predicate hasInstruction(TRawInstruction instr) { any() }
+predicate hasInstruction(TStageInstruction instr) { any() }
 
 predicate hasModeledMemoryResult(Instruction instruction) { none() }
 
@@ -361,6 +361,11 @@ private predicate isStrictlyForwardGoto(GotoStmt goto) {
 
 Locatable getInstructionAst(TStageInstruction instr) {
   result = getInstructionTranslatedElement(instr).getAst()
+  or
+  exists(IRFunction irFunc |
+    instr = TRawUnreachedInstruction(irFunc) and
+    result = irFunc.getFunction()
+  )
 }
 
 /** DEPRECATED: Alias for getInstructionAst */
@@ -370,14 +375,22 @@ deprecated Locatable getInstructionAST(TStageInstruction instr) {
 
 CppType getInstructionResultType(TStageInstruction instr) {
   getInstructionTranslatedElement(instr).hasInstruction(_, getInstructionTag(instr), result)
+  or
+  instr instanceof TRawUnreachedInstruction and
+  result = getVoidType()
 }
 
 predicate getInstructionOpcode(Opcode opcode, TStageInstruction instr) {
   getInstructionTranslatedElement(instr).hasInstruction(opcode, getInstructionTag(instr), _)
+  or
+  instr instanceof TRawUnreachedInstruction and
+  opcode instanceof Opcode::Unreached
 }
 
 IRFunctionBase getInstructionEnclosingIRFunction(TStageInstruction instr) {
   result.getFunction() = getInstructionTranslatedElement(instr).getFunction()
+  or
+  instr = TRawUnreachedInstruction(result)
 }
 
 Instruction getPrimaryInstructionForSideEffect(SideEffectInstruction instruction) {
@@ -386,6 +399,16 @@ Instruction getPrimaryInstructionForSideEffect(SideEffectInstruction instruction
         .getPrimaryInstructionForSideEffect(getInstructionTag(instruction))
 }
 
+predicate hasUnreachedInstruction(IRFunction func) {
+  exists(Call c |
+    c.getEnclosingFunction() = func.getFunction() and
+    any(Options opt).exits(c.getTarget())
+  ) and
+  not exists(TranslatedUnreachableReturnStmt return |
+    return.getEnclosingFunction().getFunction() = func.getFunction()
+  )
+}
+
 import CachedForDebugging
 
 cached

cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/InstructionTag.qll

@@ -34,6 +34,7 @@ newtype TInstructionTag =
   CallTargetTag() or
   CallTag() or
   CallSideEffectTag() or
+  CallNoReturnTag() or
   AllocationSizeTag() or
   AllocationElementSizeTag() or
   AllocationExtentConvertTag() or

cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll

@@ -8,6 +8,7 @@ private import SideEffects
 private import TranslatedElement
 private import TranslatedExpr
 private import TranslatedFunction
+private import DefaultOptions as DefaultOptions
 
 /**
  * Gets the `CallInstruction` from the `TranslatedCallExpr` for the specified expression.
@@ -66,7 +67,13 @@ abstract class TranslatedCall extends TranslatedExpr {
     )
     or
     child = getSideEffects() and
-    result = getParent().getChildSuccessor(this)
+    if this.isNoReturn()
+    then
+      result =
+        any(UnreachedInstruction instr |
+          this.getEnclosingFunction().getFunction() = instr.getEnclosingFunction()
+        )
+    else result = this.getParent().getChildSuccessor(this)
   }
 
   override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
@@ -161,6 +168,8 @@ abstract class TranslatedCall extends TranslatedExpr {
    */
   abstract predicate hasArguments();
 
+  predicate isNoReturn() { none() }
+
   final TranslatedSideEffects getSideEffects() { result.getExpr() = expr }
 }
 
@@ -266,6 +275,8 @@ abstract class TranslatedCallExpr extends TranslatedNonConstantExpr, TranslatedC
   }
 
   final override int getNumberOfArguments() { result = expr.getNumberOfArguments() }
+
+  final override predicate isNoReturn() { any(Options opt).exits(expr.getTarget()) }
 }
 
 /**

cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/reachability/ReachableBlock.qll

@@ -7,6 +7,9 @@ predicate isInfeasibleInstructionSuccessor(Instruction instr, EdgeKind kind) {
     conditionValue = getConstantValue(instr.(ConditionalBranchInstruction).getCondition()) and
     if conditionValue = 0 then kind instanceof TrueEdge else kind instanceof FalseEdge
   )
+  or
+  instr.getSuccessor(kind) instanceof UnreachedInstruction and
+  kind instanceof GotoEdge
 }
 
 pragma[noinline]
@@ -41,7 +44,9 @@ class ReachableBlock extends IRBlockBase {
  * An instruction that is contained in a reachable block.
  */
 class ReachableInstruction extends Instruction {
-  ReachableInstruction() { this.getBlock() instanceof ReachableBlock }
+  ReachableInstruction() {
+    this.getBlock() instanceof ReachableBlock and not this instanceof UnreachedInstruction
+  }
 }
 
 module Graph {

cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/SSAConstruction.qll

@@ -34,9 +34,13 @@ private module Cached {
 
   cached
   predicate hasUnreachedInstructionCached(IRFunction irFunc) {
-    exists(OldInstruction oldInstruction |
+    exists(OldIR::Instruction oldInstruction |
       irFunc = oldInstruction.getEnclosingIRFunction() and
-      Reachability::isInfeasibleInstructionSuccessor(oldInstruction, _)
+      (
+        Reachability::isInfeasibleInstructionSuccessor(oldInstruction, _)
+        or
+        oldInstruction.getOpcode() instanceof Opcode::Unreached
+      )
     )
   }
 
@@ -366,21 +370,19 @@ private module Cached {
     then
       result = getChi(getOldInstruction(instruction)) and
       kind instanceof GotoEdge
-    else (
+    else
       exists(OldInstruction oldInstruction |
-        oldInstruction = getOldInstruction(instruction) and
+        (
+          oldInstruction = getOldInstruction(instruction)
+          or
+          instruction = getChi(oldInstruction)
+        ) and
         (
           if Reachability::isInfeasibleInstructionSuccessor(oldInstruction, kind)
           then result = unreachedInstruction(instruction.getEnclosingIRFunction())
           else result = getNewInstruction(oldInstruction.getSuccessor(kind))
         )
       )
-      or
-      exists(OldInstruction oldInstruction |
-        instruction = getChi(oldInstruction) and
-        result = getNewInstruction(oldInstruction.getSuccessor(kind))
-      )
-    )
   }
 
   cached

cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/reachability/ReachableBlock.qll

@@ -7,6 +7,9 @@ predicate isInfeasibleInstructionSuccessor(Instruction instr, EdgeKind kind) {
     conditionValue = getConstantValue(instr.(ConditionalBranchInstruction).getCondition()) and
     if conditionValue = 0 then kind instanceof TrueEdge else kind instanceof FalseEdge
   )
+  or
+  instr.getSuccessor(kind) instanceof UnreachedInstruction and
+  kind instanceof GotoEdge
 }
 
 pragma[noinline]
@@ -41,7 +44,9 @@ class ReachableBlock extends IRBlockBase {
  * An instruction that is contained in a reachable block.
  */
 class ReachableInstruction extends Instruction {
-  ReachableInstruction() { this.getBlock() instanceof ReachableBlock }
+  ReachableInstruction() {
+    this.getBlock() instanceof ReachableBlock and not this instanceof UnreachedInstruction
+  }
 }
 
 module Graph {

cpp/ql/test/library-tests/ir/ir/PrintAST.expected

@@ -14377,6 +14377,60 @@ ir.cpp:
 # 1885|             Type = [ClassTemplateInstantiation,Struct] Bar2<int>
 # 1885|             ValueCategory = lvalue
 # 1886|     getStmt(2): [ReturnStmt] return ...
+# 1889| [TopLevelFunction] void noreturnFunc()
+# 1889|   <params>: 
+# 1891| [TopLevelFunction] int noreturnTest(int)
+# 1891|   <params>: 
+# 1891|     getParameter(0): [Parameter] x
+# 1891|         Type = [IntType] int
+# 1891|   getEntryPoint(): [BlockStmt] { ... }
+# 1892|     getStmt(0): [IfStmt] if (...) ... 
+# 1892|       getCondition(): [LTExpr] ... < ...
+# 1892|           Type = [BoolType] bool
+# 1892|           ValueCategory = prvalue
+# 1892|         getLesserOperand(): [VariableAccess] x
+# 1892|             Type = [IntType] int
+# 1892|             ValueCategory = prvalue(load)
+# 1892|         getGreaterOperand(): [Literal] 10
+# 1892|             Type = [IntType] int
+# 1892|             Value = [Literal] 10
+# 1892|             ValueCategory = prvalue
+# 1892|       getThen(): [BlockStmt] { ... }
+# 1893|         getStmt(0): [ReturnStmt] return ...
+# 1893|           getExpr(): [VariableAccess] x
+# 1893|               Type = [IntType] int
+# 1893|               ValueCategory = prvalue(load)
+# 1894|       getElse(): [BlockStmt] { ... }
+# 1895|         getStmt(0): [ExprStmt] ExprStmt
+# 1895|           getExpr(): [FunctionCall] call to noreturnFunc
+# 1895|               Type = [VoidType] void
+# 1895|               ValueCategory = prvalue
+# 1897|     getStmt(1): [ReturnStmt] return ...
+# 1899| [TopLevelFunction] int noreturnTest2(int)
+# 1899|   <params>: 
+# 1899|     getParameter(0): [Parameter] x
+# 1899|         Type = [IntType] int
+# 1899|   getEntryPoint(): [BlockStmt] { ... }
+# 1900|     getStmt(0): [IfStmt] if (...) ... 
+# 1900|       getCondition(): [LTExpr] ... < ...
+# 1900|           Type = [BoolType] bool
+# 1900|           ValueCategory = prvalue
+# 1900|         getLesserOperand(): [VariableAccess] x
+# 1900|             Type = [IntType] int
+# 1900|             ValueCategory = prvalue(load)
+# 1900|         getGreaterOperand(): [Literal] 10
+# 1900|             Type = [IntType] int
+# 1900|             Value = [Literal] 10
+# 1900|             ValueCategory = prvalue
+# 1900|       getThen(): [BlockStmt] { ... }
+# 1901|         getStmt(0): [ExprStmt] ExprStmt
+# 1901|           getExpr(): [FunctionCall] call to noreturnFunc
+# 1901|               Type = [VoidType] void
+# 1901|               ValueCategory = prvalue
+# 1903|     getStmt(1): [ReturnStmt] return ...
+# 1903|       getExpr(): [VariableAccess] x
+# 1903|           Type = [IntType] int
+# 1903|           ValueCategory = prvalue(load)
 perf-regression.cpp:
 #    4| [CopyAssignmentOperator] Big& Big::operator=(Big const&)
 #    4|   <params>: 

cpp/ql/test/library-tests/ir/ir/ir.cpp

@@ -1886,4 +1886,21 @@ namespace missing_declaration_entries {
     }
 }
 
+[[noreturn]] void noreturnFunc();
+
+int noreturnTest(int x) {
+    if (x < 10) {
+        return x;
+    } else {
+        noreturnFunc();
+    }
+}
+
+int noreturnTest2(int x) {
+    if (x < 10) {
+        noreturnFunc();
+    }
+    return x;
+}
+
 // semmle-extractor-options: -std=c++17 --clang

cpp/ql/test/library-tests/ir/ir/operand_locations.expected

@@ -8741,6 +8741,44 @@
 | ir.cpp:1885:11:1885:50 | ChiPartial | partial:m1885_4 |
 | ir.cpp:1885:11:1885:50 | ChiTotal | total:m1883_4 |
 | ir.cpp:1885:11:1885:50 | SideEffect | ~m1883_4 |
+| ir.cpp:1891:5:1891:16 | Address | &:r1891_7 |
+| ir.cpp:1891:5:1891:16 | ChiPartial | partial:m1891_3 |
+| ir.cpp:1891:5:1891:16 | ChiTotal | total:m1891_2 |
+| ir.cpp:1891:5:1891:16 | Load | m1893_4 |
+| ir.cpp:1891:5:1891:16 | SideEffect | m1891_3 |
+| ir.cpp:1891:22:1891:22 | Address | &:r1891_5 |
+| ir.cpp:1892:9:1892:9 | Address | &:r1892_1 |
+| ir.cpp:1892:9:1892:9 | Left | r1892_2 |
+| ir.cpp:1892:9:1892:9 | Load | m1891_6 |
+| ir.cpp:1892:9:1892:14 | Condition | r1892_4 |
+| ir.cpp:1892:13:1892:14 | Right | r1892_3 |
+| ir.cpp:1893:9:1893:17 | Address | &:r1893_1 |
+| ir.cpp:1893:16:1893:16 | Address | &:r1893_2 |
+| ir.cpp:1893:16:1893:16 | Load | m1891_6 |
+| ir.cpp:1893:16:1893:16 | StoreValue | r1893_3 |
+| ir.cpp:1895:9:1895:20 | CallTarget | func:r1895_1 |
+| ir.cpp:1895:9:1895:20 | ChiPartial | partial:m1895_3 |
+| ir.cpp:1895:9:1895:20 | ChiTotal | total:m1891_4 |
+| ir.cpp:1895:9:1895:20 | SideEffect | ~m1891_4 |
+| ir.cpp:1899:5:1899:17 | Address | &:r1899_8 |
+| ir.cpp:1899:5:1899:17 | ChiPartial | partial:m1899_3 |
+| ir.cpp:1899:5:1899:17 | ChiTotal | total:m1899_2 |
+| ir.cpp:1899:5:1899:17 | Load | m1903_4 |
+| ir.cpp:1899:5:1899:17 | SideEffect | m1899_3 |
+| ir.cpp:1899:23:1899:23 | Address | &:r1899_5 |
+| ir.cpp:1900:9:1900:9 | Address | &:r1900_1 |
+| ir.cpp:1900:9:1900:9 | Left | r1900_2 |
+| ir.cpp:1900:9:1900:9 | Load | m1899_6 |
+| ir.cpp:1900:9:1900:14 | Condition | r1900_4 |
+| ir.cpp:1900:13:1900:14 | Right | r1900_3 |
+| ir.cpp:1901:9:1901:20 | CallTarget | func:r1901_1 |
+| ir.cpp:1901:9:1901:20 | ChiPartial | partial:m1901_3 |
+| ir.cpp:1901:9:1901:20 | ChiTotal | total:m1899_4 |
+| ir.cpp:1901:9:1901:20 | SideEffect | ~m1899_4 |
+| ir.cpp:1903:5:1903:13 | Address | &:r1903_1 |
+| ir.cpp:1903:12:1903:12 | Address | &:r1903_2 |
+| ir.cpp:1903:12:1903:12 | Load | m1899_6 |
+| ir.cpp:1903:12:1903:12 | StoreValue | r1903_3 |
 | perf-regression.cpp:6:3:6:5 | Address | &:r6_5 |
 | perf-regression.cpp:6:3:6:5 | Address | &:r6_5 |
 | perf-regression.cpp:6:3:6:5 | Address | &:r6_7 |

cpp/ql/test/library-tests/ir/ir/raw_ir.expected

@@ -10035,6 +10035,68 @@ ir.cpp:
 # 1883|     v1883_5(void)             = AliasedUse                                                : ~m?
 # 1883|     v1883_6(void)             = ExitFunction                                              : 
 
+# 1891| int noreturnTest(int)
+# 1891|   Block 0
+# 1891|     v1891_1(void)       = EnterFunction          : 
+# 1891|     mu1891_2(unknown)   = AliasedDefinition      : 
+# 1891|     mu1891_3(unknown)   = InitializeNonLocal     : 
+# 1891|     r1891_4(glval<int>) = VariableAddress[x]     : 
+# 1891|     mu1891_5(int)       = InitializeParameter[x] : &:r1891_4
+# 1892|     r1892_1(glval<int>) = VariableAddress[x]     : 
+# 1892|     r1892_2(int)        = Load[x]                : &:r1892_1, ~m?
+# 1892|     r1892_3(int)        = Constant[10]           : 
+# 1892|     r1892_4(bool)       = CompareLT              : r1892_2, r1892_3
+# 1892|     v1892_5(void)       = ConditionalBranch      : r1892_4
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+# 1893|   Block 1
+# 1893|     r1893_1(glval<int>) = VariableAddress[#return] : 
+# 1893|     r1893_2(glval<int>) = VariableAddress[x]       : 
+# 1893|     r1893_3(int)        = Load[x]                  : &:r1893_2, ~m?
+# 1893|     mu1893_4(int)       = Store[#return]           : &:r1893_1, r1893_3
+# 1891|     r1891_6(glval<int>) = VariableAddress[#return] : 
+# 1891|     v1891_7(void)       = ReturnValue              : &:r1891_6, ~m?
+# 1891|     v1891_8(void)       = AliasedUse               : ~m?
+# 1891|     v1891_9(void)       = ExitFunction             : 
+
+# 1895|   Block 2
+# 1895|     r1895_1(glval<unknown>) = FunctionAddress[noreturnFunc] : 
+# 1895|     v1895_2(void)           = Call[noreturnFunc]            : func:r1895_1
+# 1895|     mu1895_3(unknown)       = ^CallSideEffect               : ~m?
+# 1897|     v1897_1(void)           = Unreached                     : 
+
+# 1899| int noreturnTest2(int)
+# 1899|   Block 0
+# 1899|     v1899_1(void)       = EnterFunction          : 
+# 1899|     mu1899_2(unknown)   = AliasedDefinition      : 
+# 1899|     mu1899_3(unknown)   = InitializeNonLocal     : 
+# 1899|     r1899_4(glval<int>) = VariableAddress[x]     : 
+# 1899|     mu1899_5(int)       = InitializeParameter[x] : &:r1899_4
+# 1900|     r1900_1(glval<int>) = VariableAddress[x]     : 
+# 1900|     r1900_2(int)        = Load[x]                : &:r1900_1, ~m?
+# 1900|     r1900_3(int)        = Constant[10]           : 
+# 1900|     r1900_4(bool)       = CompareLT              : r1900_2, r1900_3
+# 1900|     v1900_5(void)       = ConditionalBranch      : r1900_4
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+# 1901|   Block 1
+# 1901|     r1901_1(glval<unknown>) = FunctionAddress[noreturnFunc] : 
+# 1901|     v1901_2(void)           = Call[noreturnFunc]            : func:r1901_1
+# 1901|     mu1901_3(unknown)       = ^CallSideEffect               : ~m?
+# 1899|     v1899_6(void)           = Unreached                     : 
+
+# 1903|   Block 2
+# 1903|     r1903_1(glval<int>) = VariableAddress[#return] : 
+# 1903|     r1903_2(glval<int>) = VariableAddress[x]       : 
+# 1903|     r1903_3(int)        = Load[x]                  : &:r1903_2, ~m?
+# 1903|     mu1903_4(int)       = Store[#return]           : &:r1903_1, r1903_3
+# 1899|     r1899_7(glval<int>) = VariableAddress[#return] : 
+# 1899|     v1899_8(void)       = ReturnValue              : &:r1899_7, ~m?
+# 1899|     v1899_9(void)       = AliasedUse               : ~m?
+# 1899|     v1899_10(void)      = ExitFunction             : 
+
 perf-regression.cpp:
 #    6| void Big::Big()
 #    6|   Block 0

cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ir.expected

@@ -2091,3 +2091,69 @@ ssa.cpp:
 #  417|     v417_5(void)             = ReturnVoid         : 
 #  417|     v417_6(void)             = AliasedUse         : m417_3
 #  417|     v417_7(void)             = ExitFunction       : 
+
+#  423| int noreturnTest(int)
+#  423|   Block 0
+#  423|     v423_1(void)       = EnterFunction          : 
+#  423|     m423_2(unknown)    = AliasedDefinition      : 
+#  423|     m423_3(unknown)    = InitializeNonLocal     : 
+#  423|     m423_4(unknown)    = Chi                    : total:m423_2, partial:m423_3
+#  423|     r423_5(glval<int>) = VariableAddress[x]     : 
+#  423|     m423_6(int)        = InitializeParameter[x] : &:r423_5
+#  424|     r424_1(glval<int>) = VariableAddress[x]     : 
+#  424|     r424_2(int)        = Load[x]                : &:r424_1, m423_6
+#  424|     r424_3(int)        = Constant[10]           : 
+#  424|     r424_4(bool)       = CompareLT              : r424_2, r424_3
+#  424|     v424_5(void)       = ConditionalBranch      : r424_4
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#  425|   Block 1
+#  425|     r425_1(glval<int>) = VariableAddress[#return] : 
+#  425|     r425_2(glval<int>) = VariableAddress[x]       : 
+#  425|     r425_3(int)        = Load[x]                  : &:r425_2, m423_6
+#  425|     m425_4(int)        = Store[#return]           : &:r425_1, r425_3
+#  423|     r423_7(glval<int>) = VariableAddress[#return] : 
+#  423|     v423_8(void)       = ReturnValue              : &:r423_7, m425_4
+#  423|     v423_9(void)       = AliasedUse               : m423_3
+#  423|     v423_10(void)      = ExitFunction             : 
+
+#  427|   Block 2
+#  427|     r427_1(glval<unknown>) = FunctionAddress[noreturnFunc] : 
+#  427|     v427_2(void)           = Call[noreturnFunc]            : func:r427_1
+#  427|     m427_3(unknown)        = ^CallSideEffect               : ~m423_4
+#  427|     m427_4(unknown)        = Chi                           : total:m423_4, partial:m427_3
+#  423|     v423_11(void)          = Unreached                     : 
+
+#  431| int noreturnTest2(int)
+#  431|   Block 0
+#  431|     v431_1(void)       = EnterFunction          : 
+#  431|     m431_2(unknown)    = AliasedDefinition      : 
+#  431|     m431_3(unknown)    = InitializeNonLocal     : 
+#  431|     m431_4(unknown)    = Chi                    : total:m431_2, partial:m431_3
+#  431|     r431_5(glval<int>) = VariableAddress[x]     : 
+#  431|     m431_6(int)        = InitializeParameter[x] : &:r431_5
+#  432|     r432_1(glval<int>) = VariableAddress[x]     : 
+#  432|     r432_2(int)        = Load[x]                : &:r432_1, m431_6
+#  432|     r432_3(int)        = Constant[10]           : 
+#  432|     r432_4(bool)       = CompareLT              : r432_2, r432_3
+#  432|     v432_5(void)       = ConditionalBranch      : r432_4
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#  433|   Block 1
+#  433|     r433_1(glval<unknown>) = FunctionAddress[noreturnFunc] : 
+#  433|     v433_2(void)           = Call[noreturnFunc]            : func:r433_1
+#  433|     m433_3(unknown)        = ^CallSideEffect               : ~m431_4
+#  433|     m433_4(unknown)        = Chi                           : total:m431_4, partial:m433_3
+#  431|     v431_7(void)           = Unreached                     : 
+
+#  435|   Block 2
+#  435|     r435_1(glval<int>) = VariableAddress[#return] : 
+#  435|     r435_2(glval<int>) = VariableAddress[x]       : 
+#  435|     r435_3(int)        = Load[x]                  : &:r435_2, m431_6
+#  435|     m435_4(int)        = Store[#return]           : &:r435_1, r435_3
+#  431|     r431_8(glval<int>) = VariableAddress[#return] : 
+#  431|     v431_9(void)       = ReturnValue              : &:r431_8, m435_4
+#  431|     v431_10(void)      = AliasedUse               : m431_3
+#  431|     v431_11(void)      = ExitFunction             : 

cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ir_unsound.expected

@@ -2080,3 +2080,69 @@ ssa.cpp:
 #  417|     v417_5(void)             = ReturnVoid         : 
 #  417|     v417_6(void)             = AliasedUse         : m417_3
 #  417|     v417_7(void)             = ExitFunction       : 
+
+#  423| int noreturnTest(int)
+#  423|   Block 0
+#  423|     v423_1(void)       = EnterFunction          : 
+#  423|     m423_2(unknown)    = AliasedDefinition      : 
+#  423|     m423_3(unknown)    = InitializeNonLocal     : 
+#  423|     m423_4(unknown)    = Chi                    : total:m423_2, partial:m423_3
+#  423|     r423_5(glval<int>) = VariableAddress[x]     : 
+#  423|     m423_6(int)        = InitializeParameter[x] : &:r423_5
+#  424|     r424_1(glval<int>) = VariableAddress[x]     : 
+#  424|     r424_2(int)        = Load[x]                : &:r424_1, m423_6
+#  424|     r424_3(int)        = Constant[10]           : 
+#  424|     r424_4(bool)       = CompareLT              : r424_2, r424_3
+#  424|     v424_5(void)       = ConditionalBranch      : r424_4
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#  425|   Block 1
+#  425|     r425_1(glval<int>) = VariableAddress[#return] : 
+#  425|     r425_2(glval<int>) = VariableAddress[x]       : 
+#  425|     r425_3(int)        = Load[x]                  : &:r425_2, m423_6
+#  425|     m425_4(int)        = Store[#return]           : &:r425_1, r425_3
+#  423|     r423_7(glval<int>) = VariableAddress[#return] : 
+#  423|     v423_8(void)       = ReturnValue              : &:r423_7, m425_4
+#  423|     v423_9(void)       = AliasedUse               : m423_3
+#  423|     v423_10(void)      = ExitFunction             : 
+
+#  427|   Block 2
+#  427|     r427_1(glval<unknown>) = FunctionAddress[noreturnFunc] : 
+#  427|     v427_2(void)           = Call[noreturnFunc]            : func:r427_1
+#  427|     m427_3(unknown)        = ^CallSideEffect               : ~m423_4
+#  427|     m427_4(unknown)        = Chi                           : total:m423_4, partial:m427_3
+#  423|     v423_11(void)          = Unreached                     : 
+
+#  431| int noreturnTest2(int)
+#  431|   Block 0
+#  431|     v431_1(void)       = EnterFunction          : 
+#  431|     m431_2(unknown)    = AliasedDefinition      : 
+#  431|     m431_3(unknown)    = InitializeNonLocal     : 
+#  431|     m431_4(unknown)    = Chi                    : total:m431_2, partial:m431_3
+#  431|     r431_5(glval<int>) = VariableAddress[x]     : 
+#  431|     m431_6(int)        = InitializeParameter[x] : &:r431_5
+#  432|     r432_1(glval<int>) = VariableAddress[x]     : 
+#  432|     r432_2(int)        = Load[x]                : &:r432_1, m431_6
+#  432|     r432_3(int)        = Constant[10]           : 
+#  432|     r432_4(bool)       = CompareLT              : r432_2, r432_3
+#  432|     v432_5(void)       = ConditionalBranch      : r432_4
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#  433|   Block 1
+#  433|     r433_1(glval<unknown>) = FunctionAddress[noreturnFunc] : 
+#  433|     v433_2(void)           = Call[noreturnFunc]            : func:r433_1
+#  433|     m433_3(unknown)        = ^CallSideEffect               : ~m431_4
+#  433|     m433_4(unknown)        = Chi                           : total:m431_4, partial:m433_3
+#  431|     v431_7(void)           = Unreached                     : 
+
+#  435|   Block 2
+#  435|     r435_1(glval<int>) = VariableAddress[#return] : 
+#  435|     r435_2(glval<int>) = VariableAddress[x]       : 
+#  435|     r435_3(int)        = Load[x]                  : &:r435_2, m431_6
+#  435|     m435_4(int)        = Store[#return]           : &:r435_1, r435_3
+#  431|     r431_8(glval<int>) = VariableAddress[#return] : 
+#  431|     v431_9(void)       = ReturnValue              : &:r431_8, m435_4
+#  431|     v431_10(void)      = AliasedUse               : m431_3
+#  431|     v431_11(void)      = ExitFunction             : 

cpp/ql/test/library-tests/ir/ssa/ssa.cpp

@@ -417,3 +417,20 @@ void vla(int n1, int n2, int n3, bool b1) {
 void nested_array_designators() {
   int x[1][2] = {[0][0] = 1234, [0][1] = 5678};
 }
+
+[[noreturn]] void noreturnFunc();
+
+int noreturnTest(int x) {
+    if (x < 10) {
+        return x;
+    } else {
+        noreturnFunc();
+    }
+}
+
+int noreturnTest2(int x) {
+    if (x < 10) {
+        noreturnFunc();
+    }
+    return x;
+}

cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ir.expected

@@ -1940,3 +1940,65 @@ ssa.cpp:
 #  417|     v417_4(void)             = ReturnVoid         : 
 #  417|     v417_5(void)             = AliasedUse         : ~m?
 #  417|     v417_6(void)             = ExitFunction       : 
+
+#  423| int noreturnTest(int)
+#  423|   Block 0
+#  423|     v423_1(void)       = EnterFunction          : 
+#  423|     mu423_2(unknown)   = AliasedDefinition      : 
+#  423|     mu423_3(unknown)   = InitializeNonLocal     : 
+#  423|     r423_4(glval<int>) = VariableAddress[x]     : 
+#  423|     m423_5(int)        = InitializeParameter[x] : &:r423_4
+#  424|     r424_1(glval<int>) = VariableAddress[x]     : 
+#  424|     r424_2(int)        = Load[x]                : &:r424_1, m423_5
+#  424|     r424_3(int)        = Constant[10]           : 
+#  424|     r424_4(bool)       = CompareLT              : r424_2, r424_3
+#  424|     v424_5(void)       = ConditionalBranch      : r424_4
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#  425|   Block 1
+#  425|     r425_1(glval<int>) = VariableAddress[#return] : 
+#  425|     r425_2(glval<int>) = VariableAddress[x]       : 
+#  425|     r425_3(int)        = Load[x]                  : &:r425_2, m423_5
+#  425|     m425_4(int)        = Store[#return]           : &:r425_1, r425_3
+#  423|     r423_6(glval<int>) = VariableAddress[#return] : 
+#  423|     v423_7(void)       = ReturnValue              : &:r423_6, m425_4
+#  423|     v423_8(void)       = AliasedUse               : ~m?
+#  423|     v423_9(void)       = ExitFunction             : 
+
+#  427|   Block 2
+#  427|     r427_1(glval<unknown>) = FunctionAddress[noreturnFunc] : 
+#  427|     v427_2(void)           = Call[noreturnFunc]            : func:r427_1
+#  427|     mu427_3(unknown)       = ^CallSideEffect               : ~m?
+#  423|     v423_10(void)          = Unreached                     : 
+
+#  431| int noreturnTest2(int)
+#  431|   Block 0
+#  431|     v431_1(void)       = EnterFunction          : 
+#  431|     mu431_2(unknown)   = AliasedDefinition      : 
+#  431|     mu431_3(unknown)   = InitializeNonLocal     : 
+#  431|     r431_4(glval<int>) = VariableAddress[x]     : 
+#  431|     m431_5(int)        = InitializeParameter[x] : &:r431_4
+#  432|     r432_1(glval<int>) = VariableAddress[x]     : 
+#  432|     r432_2(int)        = Load[x]                : &:r432_1, m431_5
+#  432|     r432_3(int)        = Constant[10]           : 
+#  432|     r432_4(bool)       = CompareLT              : r432_2, r432_3
+#  432|     v432_5(void)       = ConditionalBranch      : r432_4
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#  433|   Block 1
+#  433|     r433_1(glval<unknown>) = FunctionAddress[noreturnFunc] : 
+#  433|     v433_2(void)           = Call[noreturnFunc]            : func:r433_1
+#  433|     mu433_3(unknown)       = ^CallSideEffect               : ~m?
+#  431|     v431_6(void)           = Unreached                     : 
+
+#  435|   Block 2
+#  435|     r435_1(glval<int>) = VariableAddress[#return] : 
+#  435|     r435_2(glval<int>) = VariableAddress[x]       : 
+#  435|     r435_3(int)        = Load[x]                  : &:r435_2, m431_5
+#  435|     m435_4(int)        = Store[#return]           : &:r435_1, r435_3
+#  431|     r431_7(glval<int>) = VariableAddress[#return] : 
+#  431|     v431_8(void)       = ReturnValue              : &:r431_7, m435_4
+#  431|     v431_9(void)       = AliasedUse               : ~m?
+#  431|     v431_10(void)      = ExitFunction             : 

cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ir_unsound.expected

@@ -1940,3 +1940,65 @@ ssa.cpp:
 #  417|     v417_4(void)             = ReturnVoid         : 
 #  417|     v417_5(void)             = AliasedUse         : ~m?
 #  417|     v417_6(void)             = ExitFunction       : 
+
+#  423| int noreturnTest(int)
+#  423|   Block 0
+#  423|     v423_1(void)       = EnterFunction          : 
+#  423|     mu423_2(unknown)   = AliasedDefinition      : 
+#  423|     mu423_3(unknown)   = InitializeNonLocal     : 
+#  423|     r423_4(glval<int>) = VariableAddress[x]     : 
+#  423|     m423_5(int)        = InitializeParameter[x] : &:r423_4
+#  424|     r424_1(glval<int>) = VariableAddress[x]     : 
+#  424|     r424_2(int)        = Load[x]                : &:r424_1, m423_5
+#  424|     r424_3(int)        = Constant[10]           : 
+#  424|     r424_4(bool)       = CompareLT              : r424_2, r424_3
+#  424|     v424_5(void)       = ConditionalBranch      : r424_4
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#  425|   Block 1
+#  425|     r425_1(glval<int>) = VariableAddress[#return] : 
+#  425|     r425_2(glval<int>) = VariableAddress[x]       : 
+#  425|     r425_3(int)        = Load[x]                  : &:r425_2, m423_5
+#  425|     m425_4(int)        = Store[#return]           : &:r425_1, r425_3
+#  423|     r423_6(glval<int>) = VariableAddress[#return] : 
+#  423|     v423_7(void)       = ReturnValue              : &:r423_6, m425_4
+#  423|     v423_8(void)       = AliasedUse               : ~m?
+#  423|     v423_9(void)       = ExitFunction             : 
+
+#  427|   Block 2
+#  427|     r427_1(glval<unknown>) = FunctionAddress[noreturnFunc] : 
+#  427|     v427_2(void)           = Call[noreturnFunc]            : func:r427_1
+#  427|     mu427_3(unknown)       = ^CallSideEffect               : ~m?
+#  423|     v423_10(void)          = Unreached                     : 
+
+#  431| int noreturnTest2(int)
+#  431|   Block 0
+#  431|     v431_1(void)       = EnterFunction          : 
+#  431|     mu431_2(unknown)   = AliasedDefinition      : 
+#  431|     mu431_3(unknown)   = InitializeNonLocal     : 
+#  431|     r431_4(glval<int>) = VariableAddress[x]     : 
+#  431|     m431_5(int)        = InitializeParameter[x] : &:r431_4
+#  432|     r432_1(glval<int>) = VariableAddress[x]     : 
+#  432|     r432_2(int)        = Load[x]                : &:r432_1, m431_5
+#  432|     r432_3(int)        = Constant[10]           : 
+#  432|     r432_4(bool)       = CompareLT              : r432_2, r432_3
+#  432|     v432_5(void)       = ConditionalBranch      : r432_4
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#  433|   Block 1
+#  433|     r433_1(glval<unknown>) = FunctionAddress[noreturnFunc] : 
+#  433|     v433_2(void)           = Call[noreturnFunc]            : func:r433_1
+#  433|     mu433_3(unknown)       = ^CallSideEffect               : ~m?
+#  431|     v431_6(void)           = Unreached                     : 
+
+#  435|   Block 2
+#  435|     r435_1(glval<int>) = VariableAddress[#return] : 
+#  435|     r435_2(glval<int>) = VariableAddress[x]       : 
+#  435|     r435_3(int)        = Load[x]                  : &:r435_2, m431_5
+#  435|     m435_4(int)        = Store[#return]           : &:r435_1, r435_3
+#  431|     r431_7(glval<int>) = VariableAddress[#return] : 
+#  431|     v431_8(void)       = ReturnValue              : &:r431_7, m435_4
+#  431|     v431_9(void)       = AliasedUse               : ~m?
+#  431|     v431_10(void)      = ExitFunction             : 

csharp/ql/src/experimental/ir/implementation/internal/TInstruction.qll

@@ -19,6 +19,9 @@ newtype TInstruction =
   ) {
     IRConstruction::Raw::hasInstruction(tag1, tag2)
   } or
+  TRawUnreachedInstruction(IRFunctionBase irFunc) {
+    IRConstruction::hasUnreachedInstruction(irFunc)
+  } or
   TUnaliasedSsaPhiInstruction(
     TRawInstruction blockStartInstr, UnaliasedSsa::Ssa::MemoryLocation memoryLocation
   ) {

csharp/ql/src/experimental/ir/implementation/raw/internal/IRConstruction.qll

@@ -414,6 +414,8 @@ private module Cached {
   }
 }
 
+predicate hasUnreachedInstruction(IRFunction func) { none() }
+
 import CachedForDebugging
 
 cached

csharp/ql/src/experimental/ir/implementation/unaliased_ssa/internal/SSAConstruction.qll

@@ -34,9 +34,13 @@ private module Cached {
 
   cached
   predicate hasUnreachedInstructionCached(IRFunction irFunc) {
-    exists(OldInstruction oldInstruction |
+    exists(OldIR::Instruction oldInstruction |
       irFunc = oldInstruction.getEnclosingIRFunction() and
-      Reachability::isInfeasibleInstructionSuccessor(oldInstruction, _)
+      (
+        Reachability::isInfeasibleInstructionSuccessor(oldInstruction, _)
+        or
+        oldInstruction.getOpcode() instanceof Opcode::Unreached
+      )
     )
   }
 
@@ -366,21 +370,19 @@ private module Cached {
     then
       result = getChi(getOldInstruction(instruction)) and
       kind instanceof GotoEdge
-    else (
+    else
       exists(OldInstruction oldInstruction |
-        oldInstruction = getOldInstruction(instruction) and
+        (
+          oldInstruction = getOldInstruction(instruction)
+          or
+          instruction = getChi(oldInstruction)
+        ) and
         (
           if Reachability::isInfeasibleInstructionSuccessor(oldInstruction, kind)
           then result = unreachedInstruction(instruction.getEnclosingIRFunction())
           else result = getNewInstruction(oldInstruction.getSuccessor(kind))
         )
       )
-      or
-      exists(OldInstruction oldInstruction |
-        instruction = getChi(oldInstruction) and
-        result = getNewInstruction(oldInstruction.getSuccessor(kind))
-      )
-    )
   }
 
   cached