1+ /**
2+ * @name Off-by-one in array access
3+ * @description TODO
4+ * @kind path-problem
5+ * @problem.severity error
6+ * @id cpp/off-by-one-array-access
7+ * @tags reliability
8+ * security
9+ */
10+
111import cpp
212import experimental.semmle.code.cpp.dataflow.ProductFlow
313import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysis
@@ -7,6 +17,21 @@ import semmle.code.cpp.ir.IR
717import semmle.code.cpp.valuenumbering.GlobalValueNumbering
818import semmle.code.cpp.models.interfaces.Allocation
919import semmle.code.cpp.ir.IRConfiguration
20+ import DataFlow:: PathGraph
21+
22+ // temporary - custom allocator for ffmpeg
23+ class AvBufferAlloc extends AllocationFunction {
24+ AvBufferAlloc ( ) { this .hasGlobalName ( [ "av_mallocz" , "av_malloc" ] ) }
25+
26+ override int getSizeArg ( ) { result = 0 }
27+ }
28+
29+ // temporary - custom allocator for php
30+ class PhpEmalloc extends AllocationFunction {
31+ PhpEmalloc ( ) { this .hasGlobalName ( [ "_emalloc" ] ) }
32+
33+ override int getSizeArg ( ) { result = 0 }
34+ }
1035
1136predicate bounded ( Instruction i , Bound b , int delta , boolean upper ) {
1237 // TODO: reason
@@ -17,18 +42,12 @@ class ArraySizeConfiguration extends ProductFlow::Configuration {
1742 ArraySizeConfiguration ( ) { this = "ArraySizeConfiguration" }
1843
1944 override predicate isSourcePair ( DataFlow:: Node source1 , DataFlow:: Node source2 ) {
20- exists ( GVN sizeGvn |
21- source1 .asConvertedExpr ( ) .( AllocationExpr ) .getSizeExpr ( ) = sizeGvn .getAnExpr ( ) and
22- source2 .asConvertedExpr ( ) = sizeGvn .getAnExpr ( )
23- )
45+ source1 .asConvertedExpr ( ) .( AllocationExpr ) .getSizeExpr ( ) = source2 .asConvertedExpr ( )
2446 }
2547
2648 override predicate isSinkPair ( DataFlow:: Node sink1 , DataFlow:: Node sink2 ) {
27- exists ( PointerAddInstruction pai , Instruction index , Bound b , int delta |
28- pai .getRight ( ) = index and
29- pai .getLeft ( ) = sink1 .asInstruction ( ) and
30- bounded ( index , b , delta , true ) and
31- sink2 .asInstruction ( ) = b .getInstruction ( ) and
49+ exists ( PointerAddInstruction pai , int delta |
50+ isSinkPair1 ( sink1 , sink2 , pai , delta ) and
3251 (
3352 delta = 0 and
3453 exists ( DataFlow:: Node paiNode , DataFlow:: Node derefNode |
@@ -43,9 +62,22 @@ class ArraySizeConfiguration extends ProductFlow::Configuration {
4362 }
4463}
4564
65+ pragma [ nomagic]
66+ predicate isSinkPair1 (
67+ DataFlow:: Node sink1 , DataFlow:: Node sink2 , PointerAddInstruction pai , int delta
68+ ) {
69+ exists ( Instruction index , ValueNumberBound b |
70+ pai .getRight ( ) = index and
71+ pai .getLeft ( ) = sink1 .asInstruction ( ) and
72+ bounded ( index , b , delta , true ) and
73+ sink2 .asInstruction ( ) = b .getInstruction ( )
74+ )
75+ }
76+
4677from
4778 ArraySizeConfiguration conf , DataFlow:: PathNode source1 , DataFlow2:: PathNode source2 ,
4879 DataFlow:: PathNode sink1 , DataFlow2:: PathNode sink2
4980where conf .hasFlowPath ( source1 , source2 , sink1 , sink2 )
5081// TODO: pull delta out and display it
51- select source1 , source2 , sink1 , sink2
82+ select sink1 .getNode ( ) , source1 , sink1 , "Off-by one error allocated at $@ bounded by $@." , source1 ,
83+ source1 .toString ( ) , sink2 , sink2 .toString ( )
0 commit comments