@@ -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
@@ -651,13 +653,16 @@ predicate jumpStep(Node n1, Node n2) {
651653 * Holds if data can flow from `node1` to `node2` via an assignment to `f`.
652654 * Thus, `node2` references an object with a field `f` that contains the
653655 * value of `node1`.
656+ *
657+ * The boolean `certain` is true if the destination address does not involve
658+ * any pointer arithmetic, and false otherwise.
654659 */
655- predicate storeStep ( Node node1 , Content c , PostFieldUpdateNode node2 ) {
660+ predicate storeStepImpl ( Node node1 , Content c , PostFieldUpdateNode node2 , boolean certain ) {
656661 exists ( int indirectionIndex1 , int numberOfLoads , StoreInstruction store |
657662 nodeHasInstruction ( node1 , store , pragma [ only_bind_into ] ( indirectionIndex1 ) ) and
658663 node2 .getIndirectionIndex ( ) = 1 and
659664 numberOfLoadsFromOperand ( node2 .getFieldAddress ( ) , store .getDestinationAddressOperand ( ) ,
660- numberOfLoads )
665+ numberOfLoads , certain )
661666 |
662667 exists ( FieldContent fc | fc = c |
663668 fc .getField ( ) = node2 .getUpdatedField ( ) and
@@ -671,35 +676,51 @@ predicate storeStep(Node node1, Content c, PostFieldUpdateNode node2) {
671676 )
672677}
673678
679+ /**
680+ * Holds if data can flow from `node1` to `node2` via an assignment to `f`.
681+ * Thus, `node2` references an object with a field `f` that contains the
682+ * value of `node1`.
683+ */
684+ predicate storeStep ( Node node1 , Content c , PostFieldUpdateNode node2 ) {
685+ storeStepImpl ( node1 , c , node2 , _)
686+ }
687+
674688/**
675689 * Holds if `operandFrom` flows to `operandTo` using a sequence of conversion-like
676690 * operations and exactly `n` `LoadInstruction` operations.
677691 */
678- private predicate numberOfLoadsFromOperandRec ( Operand operandFrom , Operand operandTo , int ind ) {
692+ private predicate numberOfLoadsFromOperandRec (
693+ Operand operandFrom , Operand operandTo , int ind , boolean certain
694+ ) {
679695 exists ( Instruction load | Ssa:: isDereference ( load , operandFrom ) |
680- operandTo = operandFrom and ind = 0
696+ operandTo = operandFrom and ind = 0 and certain = true
681697 or
682- numberOfLoadsFromOperand ( load .getAUse ( ) , operandTo , ind - 1 )
698+ numberOfLoadsFromOperand ( load .getAUse ( ) , operandTo , ind - 1 , certain )
683699 )
684700 or
685- exists ( Operand op , Instruction instr |
701+ exists ( Operand op , Instruction instr , boolean isPointerArith , boolean certain0 |
686702 instr = op .getDef ( ) and
687- conversionFlow ( operandFrom , instr , _, _) and
688- numberOfLoadsFromOperand ( op , operandTo , ind )
703+ conversionFlow ( operandFrom , instr , isPointerArith , _) and
704+ numberOfLoadsFromOperand ( op , operandTo , ind , certain0 )
705+ |
706+ if isPointerArith = true then certain = false else certain = certain0
689707 )
690708}
691709
692710/**
693711 * Holds if `operandFrom` flows to `operandTo` using a sequence of conversion-like
694712 * operations and exactly `n` `LoadInstruction` operations.
695713 */
696- private predicate numberOfLoadsFromOperand ( Operand operandFrom , Operand operandTo , int n ) {
697- numberOfLoadsFromOperandRec ( operandFrom , operandTo , n )
714+ private predicate numberOfLoadsFromOperand (
715+ Operand operandFrom , Operand operandTo , int n , boolean certain
716+ ) {
717+ numberOfLoadsFromOperandRec ( operandFrom , operandTo , n , certain )
698718 or
699719 not Ssa:: isDereference ( _, operandFrom ) and
700720 not conversionFlow ( operandFrom , _, _, _) and
701721 operandFrom = operandTo and
702- n = 0
722+ n = 0 and
723+ certain = true
703724}
704725
705726// Needed to join on both an operand and an index at the same time.
@@ -729,7 +750,7 @@ predicate readStep(Node node1, Content c, Node node2) {
729750 // The `1` here matches the `node2.getIndirectionIndex() = 1` conjunct
730751 // in `storeStep`.
731752 nodeHasOperand ( node1 , fa1 .getObjectAddressOperand ( ) , 1 ) and
732- numberOfLoadsFromOperand ( fa1 , operand , numberOfLoads )
753+ numberOfLoadsFromOperand ( fa1 , operand , numberOfLoads , _ )
733754 |
734755 exists ( FieldContent fc | fc = c |
735756 fc .getField ( ) = fa1 .getField ( ) and
@@ -747,7 +768,33 @@ predicate readStep(Node node1, Content c, Node node2) {
747768 * Holds if values stored inside content `c` are cleared at node `n`.
748769 */
749770predicate clearsContent ( Node n , Content c ) {
750- none ( ) // stub implementation
771+ n =
772+ any ( PostUpdateNode pun , Content d | d .impliesClearOf ( c ) and storeStepImpl ( _, d , pun , true ) | pun )
773+ .getPreUpdateNode ( ) and
774+ (
775+ // The crement operations and pointer addition and subtraction self-assign. We do not
776+ // want to clear the contents if it is indirectly pointed at by any of these operations,
777+ // as part of the contents might still be accessible afterwards. If there is no such
778+ // indirection clearing the contents is safe.
779+ not exists ( Operand op , Cpp:: Operation p |
780+ n .( IndirectOperand ) .hasOperandAndIndirectionIndex ( op , _) and
781+ (
782+ p instanceof Cpp:: AssignPointerAddExpr or
783+ p instanceof Cpp:: AssignPointerSubExpr or
784+ p instanceof Cpp:: CrementOperation
785+ )
786+ |
787+ p .getAnOperand ( ) = op .getUse ( ) .getAst ( )
788+ )
789+ or
790+ forex ( PostUpdateNode pun , Content d |
791+ pragma [ only_bind_into ] ( d ) .impliesClearOf ( pragma [ only_bind_into ] ( c ) ) and
792+ storeStepImpl ( _, d , pun , true ) and
793+ pun .getPreUpdateNode ( ) = n
794+ |
795+ c .getIndirectionIndex ( ) = d .getIndirectionIndex ( )
796+ )
797+ )
751798}
752799
753800/**
@@ -809,7 +856,73 @@ class DataFlowCall extends CallInstruction {
809856 Function getEnclosingCallable ( ) { result = this .getEnclosingFunction ( ) }
810857}
811858
812- 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
813926
814927int accessPathLimit ( ) { result = 5 }
815928
0 commit comments