@@ -321,9 +321,11 @@ private class PrimaryArgumentNode extends ArgumentNode, OperandNode {
321321
322322private class SideEffectArgumentNode extends ArgumentNode , SideEffectOperandNode {
323323 override predicate argumentOf ( DataFlowCall dfCall , ArgumentPosition pos ) {
324- this .getCallInstruction ( ) = dfCall and
325- pos .( IndirectionPosition ) .getArgumentIndex ( ) = this .getArgumentIndex ( ) and
326- super .hasAddressOperandAndIndirectionIndex ( _, pos .( IndirectionPosition ) .getIndirectionIndex ( ) )
324+ exists ( int indirectionIndex |
325+ pos = TIndirectionPosition ( argumentIndex , pragma [ only_bind_into ] ( indirectionIndex ) ) and
326+ this .getCallInstruction ( ) = dfCall and
327+ super .hasAddressOperandAndIndirectionIndex ( _, pragma [ only_bind_into ] ( indirectionIndex ) )
328+ )
327329 }
328330}
329331
@@ -854,7 +856,73 @@ class DataFlowCall extends CallInstruction {
854856 Function getEnclosingCallable ( ) { result = this .getEnclosingFunction ( ) }
855857}
856858
857- predicate isUnreachableInCall ( Node n , DataFlowCall call ) { none ( ) } // stub implementation
859+ module IsUnreachableInCall {
860+ private import semmle.code.cpp.ir.ValueNumbering
861+ private import semmle.code.cpp.controlflow.IRGuards as G
862+
863+ private class ConstantIntegralTypeArgumentNode extends PrimaryArgumentNode {
864+ int value ;
865+
866+ ConstantIntegralTypeArgumentNode ( ) {
867+ value = op .getDef ( ) .( IntegerConstantInstruction ) .getValue ( ) .toInt ( )
868+ }
869+
870+ int getValue ( ) { result = value }
871+ }
872+
873+ pragma [ nomagic]
874+ private predicate ensuresEq ( Operand left , Operand right , int k , IRBlock block , boolean areEqual ) {
875+ any ( G:: IRGuardCondition guard ) .ensuresEq ( left , right , k , block , areEqual )
876+ }
877+
878+ pragma [ nomagic]
879+ private predicate ensuresLt ( Operand left , Operand right , int k , IRBlock block , boolean areEqual ) {
880+ any ( G:: IRGuardCondition guard ) .ensuresLt ( left , right , k , block , areEqual )
881+ }
882+
883+ predicate isUnreachableInCall ( Node n , DataFlowCall call ) {
884+ exists (
885+ DirectParameterNode paramNode , ConstantIntegralTypeArgumentNode arg ,
886+ IntegerConstantInstruction constant , int k , Operand left , Operand right , IRBlock block
887+ |
888+ // arg flows into `paramNode`
889+ DataFlowImplCommon:: viableParamArg ( call , paramNode , arg ) and
890+ left = constant .getAUse ( ) and
891+ right = valueNumber ( paramNode .getInstruction ( ) ) .getAUse ( ) and
892+ block = n .getBasicBlock ( )
893+ |
894+ // and there's a guard condition which ensures that the result of `left == right + k` is `areEqual`
895+ exists ( boolean areEqual |
896+ ensuresEq ( pragma [ only_bind_into ] ( left ) , pragma [ only_bind_into ] ( right ) ,
897+ pragma [ only_bind_into ] ( k ) , pragma [ only_bind_into ] ( block ) , areEqual )
898+ |
899+ // this block ensures that left = right + k, but it holds that `left != right + k`
900+ areEqual = true and
901+ constant .getValue ( ) .toInt ( ) != arg .getValue ( ) + k
902+ or
903+ // this block ensures that or `left != right + k`, but it holds that `left = right + k`
904+ areEqual = false and
905+ constant .getValue ( ) .toInt ( ) = arg .getValue ( ) + k
906+ )
907+ or
908+ // or there's a guard condition which ensures that the result of `left < right + k` is `isLessThan`
909+ exists ( boolean isLessThan |
910+ ensuresLt ( pragma [ only_bind_into ] ( left ) , pragma [ only_bind_into ] ( right ) ,
911+ pragma [ only_bind_into ] ( k ) , pragma [ only_bind_into ] ( block ) , isLessThan )
912+ |
913+ isLessThan = true and
914+ // this block ensures that `left < right + k`, but it holds that `left >= right + k`
915+ constant .getValue ( ) .toInt ( ) >= arg .getValue ( ) + k
916+ or
917+ // this block ensures that `left >= right + k`, but it holds that `left < right + k`
918+ isLessThan = false and
919+ constant .getValue ( ) .toInt ( ) < arg .getValue ( ) + k
920+ )
921+ )
922+ }
923+ }
924+
925+ import IsUnreachableInCall
858926
859927int accessPathLimit ( ) { result = 5 }
860928
0 commit comments