@@ -73,11 +73,42 @@ predicate isSink(DataFlow::Node sink, BufferWrite bw, boolean qualifier) {
73
73
unboundedWriteSource ( sink .asDefiningArgument ( ) , bw , qualifier )
74
74
}
75
75
76
+ /**
77
+ * A configuration that specifies flow from a `FlowSource` to a relational
78
+ * comparison.
79
+ *
80
+ * This configuration is used to speed up the barrier computations in Config.
81
+ */
82
+ module BarrierConfig implements DataFlow:: ConfigSig {
83
+ predicate isSource ( DataFlow:: Node source ) { isSource ( source , _) }
84
+
85
+ predicate isSink ( DataFlow:: Node sink ) {
86
+ comparesEq ( sink .asOperand ( ) , _, _, true , _) or
87
+ comparesLt ( sink .asOperand ( ) , _, _, true , _)
88
+ }
89
+ }
90
+
91
+ module BarrierFlow = TaintTracking:: Global< BarrierConfig > ;
92
+
93
+ import semmle.code.cpp.ir.dataflow.internal.DataFlowImplCommon as DataFlowImplCommon
94
+
95
+ /**
96
+ * Holds if `left` is a left operand of some relational comparison that may
97
+ * depend on user input.
98
+ */
99
+ predicate interestingLessThanOrEqual ( Operand left ) {
100
+ exists ( DataFlowImplCommon:: NodeEx node |
101
+ node .asNode ( ) .asOperand ( ) = left and
102
+ BarrierFlow:: Stages:: Stage1:: sinkNode ( node , _)
103
+ )
104
+ }
105
+
76
106
predicate lessThanOrEqual ( IRGuardCondition g , Expr e , boolean branch ) {
77
107
exists ( Operand left |
78
108
g .comparesLt ( left , _, _, true , branch ) or
79
109
g .comparesEq ( left , _, _, true , branch )
80
110
|
111
+ interestingLessThanOrEqual ( left ) and
81
112
left .getDef ( ) .getUnconvertedResultExpression ( ) = e
82
113
)
83
114
}
0 commit comments