@@ -14,7 +14,7 @@ import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysi
1414import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
1515import semmle.code.cpp.ir.IR
1616import semmle.code.cpp.ir.dataflow.DataFlow
17- import StitchedPathGraph
17+ import FieldAddressToDerefFlow :: PathGraph
1818
1919pragma [ nomagic]
2020Instruction getABoundIn ( SemBound b , IRFunction func ) {
@@ -42,21 +42,6 @@ bindingset[b]
4242pragma [ inline_late]
4343predicate bounded2 ( Instruction i , Instruction b , int delta ) { boundedImpl ( i , b , delta ) }
4444
45- module FieldAddressToPointerArithmeticConfig implements DataFlow:: ConfigSig {
46- predicate isSource ( DataFlow:: Node source ) { isFieldAddressSource ( _, source ) }
47-
48- predicate isSink ( DataFlow:: Node sink ) {
49- exists ( PointerAddInstruction pai | pai .getLeft ( ) = sink .asInstruction ( ) )
50- }
51- }
52-
53- module FieldAddressToPointerArithmeticFlow =
54- DataFlow:: Global< FieldAddressToPointerArithmeticConfig > ;
55-
56- predicate isFieldAddressSource ( Field f , DataFlow:: Node source ) {
57- source .asInstruction ( ) .( FieldAddressInstruction ) .getField ( ) = f
58- }
59-
6045bindingset [ delta]
6146predicate isInvalidPointerDerefSinkImpl (
6247 int delta , Instruction i , AddressOperand addr , string operation
@@ -93,56 +78,61 @@ predicate isInvalidPointerDerefSink2(DataFlow::Node sink, Instruction i, string
9378 )
9479}
9580
96- predicate isConstantSizeOverflowSource ( Field f , FieldAddressToPointerArithmeticFlow:: PathNode fieldSource , PointerAddInstruction pai , int delta ) {
97- exists ( int size , int bound , FieldAddressToPointerArithmeticFlow:: PathNode sink |
98- FieldAddressToPointerArithmeticFlow:: flowPath ( fieldSource , sink ) and
99- isFieldAddressSource ( f , fieldSource .getNode ( ) ) and
100- pai .getLeft ( ) = sink .getNode ( ) .( DataFlow:: InstructionNode ) .asInstruction ( ) and
101- pai .getElementSize ( ) = f .getUnspecifiedType ( ) .( ArrayType ) .getBaseType ( ) .getSize ( ) and
102- f .getUnspecifiedType ( ) .( ArrayType ) .getArraySize ( ) = size and
103- semBounded ( getSemanticExpr ( pai .getRight ( ) ) , any ( SemZeroBound b ) , bound , true , _) and
104- delta = bound - size and
105- delta >= 0 and
106- size != 0 and
107- size != 1
108- )
81+ predicate pointerArithOverflow (
82+ PointerArithmeticInstruction pai , Field f , int size , int bound , int delta
83+ ) {
84+ pai .getElementSize ( ) = f .getUnspecifiedType ( ) .( ArrayType ) .getBaseType ( ) .getSize ( ) and
85+ f .getUnspecifiedType ( ) .( ArrayType ) .getArraySize ( ) = size and
86+ semBounded ( getSemanticExpr ( pai .getRight ( ) ) , any ( SemZeroBound b ) , bound , true , _) and
87+ delta = bound - size
10988}
11089
111- module PointerArithmeticToDerefConfig implements DataFlow:: ConfigSig {
112- predicate isSource ( DataFlow :: Node source ) {
113- isConstantSizeOverflowSource ( _ , _ , source . asInstruction ( ) , _ )
114- }
90+ module FieldAddressToDerefConfig implements DataFlow:: StateConfigSig {
91+ newtype FlowState =
92+ additional TArray ( Field f ) or
93+ additional TOverflowArithmetic ( PointerArithmeticInstruction pai )
11594
116- pragma [ inline]
117- predicate isSink ( DataFlow:: Node sink ) { isInvalidPointerDerefSink1 ( sink , _, _) }
118- }
119-
120- module MergedPathGraph = DataFlow:: MergePathGraph< PointerArithmeticToDerefFlow:: PathNode , FieldAddressToPointerArithmeticFlow:: PathNode , PointerArithmeticToDerefFlow:: PathGraph , FieldAddressToPointerArithmeticFlow:: PathGraph > ;
121- class PathNode = MergedPathGraph:: PathNode ;
122- module StitchedPathGraph implements DataFlow:: PathGraphSig< PathNode > {
123- query predicate edges ( PathNode a , PathNode b ) {
124- MergedPathGraph:: PathGraph:: edges ( a , b )
125- or
126- a .asPathNode2 ( ) .getNode ( ) .( DataFlow:: InstructionNode ) .asInstruction ( ) = b .asPathNode1 ( ) .getNode ( ) .( DataFlow:: InstructionNode ) .asInstruction ( ) .( PointerAddInstruction ) .getLeft ( )
95+ predicate isSource ( DataFlow:: Node source , FlowState state ) {
96+ exists ( Field f |
97+ source .asInstruction ( ) .( FieldAddressInstruction ) .getField ( ) = f and
98+ state = TArray ( f )
99+ )
127100 }
128101
129- query predicate nodes ( PathNode n , string key , string val ) {
130- MergedPathGraph:: PathGraph:: nodes ( n , key , val )
102+ predicate isSink ( DataFlow:: Node sink , FlowState state ) {
103+ isInvalidPointerDerefSink1 ( sink , _, _) and
104+ state instanceof TOverflowArithmetic
131105 }
132106
133- query predicate subpaths ( PathNode arg , PathNode par , PathNode ret , PathNode out ) {
134- MergedPathGraph:: PathGraph:: subpaths ( arg , par , ret , out )
107+ predicate isBarrier ( DataFlow:: Node node , FlowState state ) { none ( ) }
108+
109+ predicate isAdditionalFlowStep (
110+ DataFlow:: Node node1 , FlowState state1 , DataFlow:: Node node2 , FlowState state2
111+ ) {
112+ exists ( PointerArithmeticInstruction pai , Field f , int size , int delta |
113+ state1 = TArray ( f ) and
114+ state2 = TOverflowArithmetic ( pai ) and
115+ pai .getLeft ( ) = node1 .asInstruction ( ) and
116+ node2 .asInstruction ( ) = pai and
117+ pointerArithOverflow ( pai , f , size , _, delta ) and
118+ delta >= 0 and
119+ size != 0 and
120+ size != 1
121+ )
135122 }
136123}
137- module PointerArithmeticToDerefFlow = DataFlow:: Global< PointerArithmeticToDerefConfig > ;
124+
125+ module FieldAddressToDerefFlow = DataFlow:: GlobalWithState< FieldAddressToDerefConfig > ;
138126
139127from
140- Field f , PathNode fieldSource , PathNode paiNode ,
141- PathNode sink , Instruction deref , string operation , int delta
128+ Field f , FieldAddressToDerefFlow :: PathNode source , PointerArithmeticInstruction pai ,
129+ FieldAddressToDerefFlow :: PathNode sink , Instruction deref , string operation , int delta
142130where
143- PointerArithmeticToDerefFlow :: flowPath ( paiNode . asPathNode1 ( ) , sink . asPathNode1 ( ) ) and
131+ FieldAddressToDerefFlow :: flowPath ( source , sink ) and
144132 isInvalidPointerDerefSink2 ( sink .getNode ( ) , deref , operation ) and
145- isConstantSizeOverflowSource ( f , fieldSource .asPathNode2 ( ) , paiNode .getNode ( ) .asInstruction ( ) , delta )
146- select paiNode , fieldSource , sink ,
133+ source .getState ( ) = FieldAddressToDerefConfig:: TArray ( f ) and
134+ sink .getState ( ) = FieldAddressToDerefConfig:: TOverflowArithmetic ( pai ) and
135+ pointerArithOverflow ( pai , f , _, _, delta )
136+ select pai , source , sink ,
147137 "This pointer arithmetic may have an off-by-" + ( delta + 1 ) +
148138 " error allowing it to overrun $@ at this $@." , f , f .getName ( ) , deref , operation
0 commit comments