Skip to content

Commit 63a5b49

Browse files
MathiasVPMathiasVP
authored
Merge pull request github#15633 from MathiasVP/model-experiments
C++: Assume modelled functions always override buffers by default
2 parents fbc6892 + c7ee5b2 commit 63a5b49

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

43 files changed

+544
-116
lines changed

‎cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll

Lines changed: 1 addition & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -55,29 +55,12 @@ private newtype TIRDataFlowNode =
5555
TFinalParameterNode(Parameter p, int indirectionIndex) {
5656
exists(Ssa::FinalParameterUse use |
5757
use.getParameter() = p and
58-
use.getIndirectionIndex() = indirectionIndex and
59-
parameterIsRedefined(p)
58+
use.getIndirectionIndex() = indirectionIndex
6059
)
6160
} or
6261
TFinalGlobalValue(Ssa::GlobalUse globalUse) or
6362
TInitialGlobalValue(Ssa::GlobalDef globalUse)
6463

65-
/**
66-
* Holds if the value of `*p` (or `**p`, `***p`, etc.) is redefined somewhere in the body
67-
* of the enclosing function of `p`.
68-
*
69-
* Only parameters satisfying this predicate will generate a `FinalParameterNode` transferring
70-
* flow out of the function.
71-
*/
72-
private predicate parameterIsRedefined(Parameter p) {
73-
exists(Ssa::Def def |
74-
def.getSourceVariable().getBaseVariable().(Ssa::BaseIRVariable).getIRVariable().getAst() = p and
75-
def.getIndirectionIndex() = 0 and
76-
def.getIndirection() > 1 and
77-
not def.getValue().asInstruction() instanceof InitializeParameterInstruction
78-
)
79-
}
80-
8164
/**
8265
* An operand that is defined by a `FieldAddressInstruction`.
8366
*/

‎cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaInternals.qll

Lines changed: 58 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,11 @@ private import DataFlowUtil
44
private import DataFlowImplCommon as DataFlowImplCommon
55
private import semmle.code.cpp.models.interfaces.Allocation as Alloc
66
private import semmle.code.cpp.models.interfaces.DataFlow as DataFlow
7+
private import semmle.code.cpp.models.interfaces.Taint as Taint
8+
private import semmle.code.cpp.models.interfaces.PartialFlow as PartialFlow
9+
private import semmle.code.cpp.models.interfaces.FunctionInputsAndOutputs as FIO
710
private import semmle.code.cpp.ir.internal.IRCppLanguage
11+
private import semmle.code.cpp.ir.dataflow.internal.ModelUtil
812
private import DataFlowPrivate
913
private import ssa0.SsaInternals as SsaInternals0
1014
import SsaInternalsCommon
@@ -138,12 +142,11 @@ private newtype TDefOrUseImpl =
138142
isIteratorUse(container, iteratorAddress, _, indirectionIndex)
139143
} or
140144
TFinalParameterUse(Parameter p, int indirectionIndex) {
141-
// Avoid creating parameter nodes if there is no definitions of the variable other than the initializaion.
142-
exists(SsaInternals0::Def def |
143-
def.getSourceVariable().getBaseVariable().(BaseIRVariable).getIRVariable().getAst() = p and
144-
not def.getValue().asInstruction() instanceof InitializeParameterInstruction and
145-
underlyingTypeIsModifiableAt(p.getUnderlyingType(), indirectionIndex)
146-
)
145+
underlyingTypeIsModifiableAt(p.getUnderlyingType(), indirectionIndex) and
146+
// Only create an SSA read for the final use of a parameter if there's
147+
// actually a body of the enclosing function. If there's no function body
148+
// then we'll never need to flow out of the function anyway.
149+
p.getFunction().hasDefinition()
147150
}
148151

149152
private predicate isGlobalUse(
@@ -796,10 +799,58 @@ private Node getAPriorDefinition(SsaDefOrUse defOrUse) {
796799
)
797800
}
798801

802+
private predicate inOut(FIO::FunctionInput input, FIO::FunctionOutput output) {
803+
exists(int indirectionIndex |
804+
input.isQualifierObject(indirectionIndex) and
805+
output.isQualifierObject(indirectionIndex)
806+
or
807+
exists(int i |
808+
input.isParameterDeref(i, indirectionIndex) and
809+
output.isParameterDeref(i, indirectionIndex)
810+
)
811+
)
812+
}
813+
814+
/**
815+
* Holds if there should not be use-use flow out of `n`. That is, `n` is
816+
* an out-barrier to use-use flow. This includes:
817+
*
818+
* - an input to a call that would be assumed to have use-use flow to the same
819+
* argument as an output, but this flow should be blocked because the
820+
* function is modeled with another flow to that output (for example the
821+
* first argument of `strcpy`).
822+
* - a conversion that flows to such an input.
823+
*/
824+
private predicate modeledFlowBarrier(Node n) {
825+
exists(
826+
FIO::FunctionInput input, FIO::FunctionOutput output, CallInstruction call,
827+
PartialFlow::PartialFlowFunction partialFlowFunc
828+
|
829+
n = callInput(call, input) and
830+
inOut(input, output) and
831+
exists(callOutput(call, output)) and
832+
partialFlowFunc = call.getStaticCallTarget() and
833+
not partialFlowFunc.isPartialWrite(output)
834+
|
835+
call.getStaticCallTarget().(DataFlow::DataFlowFunction).hasDataFlow(_, output)
836+
or
837+
call.getStaticCallTarget().(Taint::TaintFunction).hasTaintFlow(_, output)
838+
)
839+
or
840+
exists(Operand operand, Instruction instr, Node n0, int indirectionIndex |
841+
modeledFlowBarrier(n0) and
842+
nodeHasInstruction(n0, instr, indirectionIndex) and
843+
conversionFlow(operand, instr, false, _) and
844+
nodeHasOperand(n, operand, indirectionIndex)
845+
)
846+
}
847+
799848
/** Holds if there is def-use or use-use flow from `nodeFrom` to `nodeTo`. */
800849
predicate ssaFlow(Node nodeFrom, Node nodeTo) {
801850
exists(Node nFrom, boolean uncertain, SsaDefOrUse defOrUse |
802-
ssaFlowImpl(defOrUse, nFrom, nodeTo, uncertain) and nodeFrom != nodeTo
851+
ssaFlowImpl(defOrUse, nFrom, nodeTo, uncertain) and
852+
not modeledFlowBarrier(nFrom) and
853+
nodeFrom != nodeTo
803854
|
804855
if uncertain = true then nodeFrom = [nFrom, getAPriorDefinition(defOrUse)] else nodeFrom = nFrom
805856
)

‎cpp/ql/lib/semmle/code/cpp/models/implementations/GetDelim.qll

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,8 @@ private class GetDelimFunction extends TaintFunction, AliasFunction, SideEffectF
1515
i.isParameter(3) and o.isParameterDeref(0)
1616
}
1717

18+
override predicate isPartialWrite(FunctionOutput o) { o.isParameterDeref(3) }
19+
1820
override predicate parameterNeverEscapes(int index) { index = [0, 1, 3] }
1921

2022
override predicate parameterEscapesOnlyViaReturn(int index) { none() }

‎cpp/ql/lib/semmle/code/cpp/models/implementations/Gets.qll

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,8 @@ private class FgetsFunction extends DataFlowFunction, TaintFunction, ArrayFuncti
2727
output.isReturnValue()
2828
}
2929

30+
override predicate isPartialWrite(FunctionOutput output) { output.isParameterDeref(2) }
31+
3032
override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
3133
input.isParameter(2) and
3234
output.isParameterDeref(0)

‎cpp/ql/lib/semmle/code/cpp/models/implementations/Inet.qll

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,8 @@ private class InetAton extends TaintFunction, ArrayFunction {
2020
output.isParameterDeref(1)
2121
}
2222

23+
override predicate isPartialWrite(FunctionOutput output) { output.isParameterDeref(1) }
24+
2325
override predicate hasArrayInput(int bufParam) { bufParam = 0 }
2426

2527
override predicate hasArrayOutput(int bufParam) { bufParam = 1 }

‎cpp/ql/lib/semmle/code/cpp/models/implementations/StdContainer.qll

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -118,6 +118,8 @@ private class StdSequenceContainerData extends TaintFunction {
118118
input.isReturnValueDeref() and
119119
output.isQualifierObject()
120120
}
121+
122+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
121123
}
122124

123125
/**
@@ -147,6 +149,8 @@ private class StdSequenceContainerPushModel extends StdSequenceContainerPush, Ta
147149
input.isParameterDeref(0) and
148150
output.isQualifierObject()
149151
}
152+
153+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
150154
}
151155

152156
/**
@@ -207,6 +211,8 @@ private class StdSequenceContainerInsertModel extends StdSequenceContainerInsert
207211
output.isReturnValue()
208212
)
209213
}
214+
215+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
210216
}
211217

212218
/**
@@ -263,6 +269,8 @@ private class StdSequenceContainerAt extends TaintFunction {
263269
input.isReturnValueDeref() and
264270
output.isQualifierObject()
265271
}
272+
273+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
266274
}
267275

268276
/**
@@ -297,6 +305,8 @@ private class StdSequenceEmplaceModel extends StdSequenceEmplace, TaintFunction
297305
output.isReturnValue()
298306
)
299307
}
308+
309+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
300310
}
301311

302312
/**
@@ -335,6 +345,8 @@ private class StdSequenceEmplaceBackModel extends StdSequenceEmplaceBack, TaintF
335345
input.isParameterDeref([0 .. this.getNumberOfParameters() - 1]) and
336346
output.isQualifierObject()
337347
}
348+
349+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
338350
}
339351

340352
/**

‎cpp/ql/lib/semmle/code/cpp/models/implementations/StdMap.qll

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
*/
44

55
import semmle.code.cpp.models.interfaces.Taint
6+
import semmle.code.cpp.models.interfaces.DataFlow
67
import semmle.code.cpp.models.interfaces.Iterator
78

89
/**
@@ -53,6 +54,8 @@ private class StdMapInsert extends TaintFunction {
5354
output.isReturnValue()
5455
)
5556
}
57+
58+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
5659
}
5760

5861
/**
@@ -75,6 +78,8 @@ private class StdMapEmplace extends TaintFunction {
7578
input.isQualifierObject() and
7679
output.isReturnValue()
7780
}
81+
82+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
7883
}
7984

8085
/**
@@ -102,6 +107,8 @@ private class StdMapTryEmplace extends TaintFunction {
102107
input.isQualifierObject() and
103108
output.isReturnValue()
104109
}
110+
111+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
105112
}
106113

107114
/**
@@ -115,6 +122,8 @@ private class StdMapMerge extends TaintFunction {
115122
input.isParameterDeref(0) and
116123
output.isQualifierObject()
117124
}
125+
126+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
118127
}
119128

120129
/**
@@ -132,6 +141,8 @@ private class StdMapAt extends TaintFunction {
132141
input.isReturnValueDeref() and
133142
output.isQualifierObject()
134143
}
144+
145+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
135146
}
136147

137148
/**

‎cpp/ql/lib/semmle/code/cpp/models/implementations/StdSet.qll

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,8 @@ private class StdSetInsert extends TaintFunction {
6161
output.isReturnValue()
6262
)
6363
}
64+
65+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
6466
}
6567

6668
/**
@@ -82,6 +84,8 @@ private class StdSetEmplace extends TaintFunction {
8284
input.isQualifierObject() and
8385
output.isReturnValue()
8486
}
87+
88+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
8589
}
8690

8791
/**
@@ -95,6 +99,8 @@ private class StdSetMerge extends TaintFunction {
9599
input.isParameterDeref(0) and
96100
output.isQualifierObject()
97101
}
102+
103+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
98104
}
99105

100106
/**

‎cpp/ql/lib/semmle/code/cpp/models/implementations/StdString.qll

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -129,6 +129,8 @@ private class StdStringDataModel extends StdStringData, StdStringTaintFunction {
129129
input.isReturnValueDeref() and
130130
output.isQualifierObject()
131131
}
132+
133+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
132134
}
133135

134136
/**
@@ -142,6 +144,8 @@ private class StdStringPush extends StdStringTaintFunction {
142144
input.isParameter(0) and
143145
output.isQualifierObject()
144146
}
147+
148+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
145149
}
146150

147151
/**
@@ -204,6 +208,8 @@ private class StdStringAppend extends StdStringTaintFunction {
204208
input.isReturnValueDeref() and
205209
output.isQualifierObject()
206210
}
211+
212+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
207213
}
208214

209215
/**
@@ -237,6 +243,8 @@ private class StdStringInsert extends StdStringTaintFunction {
237243
input.isReturnValueDeref() and
238244
output.isQualifierObject()
239245
}
246+
247+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
240248
}
241249

242250
/**
@@ -305,6 +313,8 @@ private class StdStringAt extends StdStringTaintFunction {
305313
input.isReturnValueDeref() and
306314
output.isQualifierObject()
307315
}
316+
317+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
308318
}
309319

310320
/**
@@ -338,6 +348,8 @@ private class StdIStreamIn extends DataFlowFunction, TaintFunction {
338348
input.isReturnValueDeref() and
339349
output.isQualifierObject()
340350
}
351+
352+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
341353
}
342354

343355
/**
@@ -358,6 +370,8 @@ private class StdIStreamInNonMember extends DataFlowFunction, TaintFunction {
358370
output.isReturnValueDeref()
359371
}
360372

373+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
374+
361375
override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
362376
// flow from first parameter to second parameter
363377
input.isParameterDeref(0) and
@@ -403,6 +417,8 @@ private class StdIStreamRead extends DataFlowFunction, TaintFunction {
403417
output.isReturnValueDeref()
404418
}
405419

420+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
421+
406422
override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
407423
// flow from qualifier to first parameter
408424
input.isQualifierObject() and
@@ -442,6 +458,8 @@ private class StdIStreamPutBack extends DataFlowFunction, TaintFunction {
442458
output.isReturnValueDeref()
443459
}
444460

461+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
462+
445463
override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
446464
// flow from first parameter (value or pointer) to qualifier
447465
input.isParameter(0) and
@@ -478,6 +496,8 @@ private class StdIStreamGetLine extends DataFlowFunction, TaintFunction {
478496
output.isReturnValueDeref()
479497
}
480498

499+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
500+
481501
override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
482502
// flow from qualifier to first parameter
483503
input.isQualifierObject() and
@@ -540,6 +560,8 @@ private class StdOStreamOut extends DataFlowFunction, TaintFunction {
540560
output.isReturnValueDeref()
541561
}
542562

563+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
564+
543565
override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
544566
// flow from first parameter (value or pointer) to qualifier
545567
input.isParameter(0) and
@@ -579,6 +601,8 @@ private class StdOStreamOutNonMember extends DataFlowFunction, TaintFunction {
579601
output.isReturnValueDeref()
580602
}
581603

604+
override predicate isPartialWrite(FunctionOutput output) { output.isParameterDeref(0) }
605+
582606
override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
583607
// flow from second parameter to first parameter
584608
input.isParameterDeref(1) and
@@ -672,6 +696,8 @@ private class StdStreamFunction extends DataFlowFunction, TaintFunction {
672696
output.isReturnValueDeref()
673697
}
674698

699+
override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
700+
675701
override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
676702
// reverse flow from returned reference to the qualifier
677703
input.isReturnValueDeref() and

0 commit comments

Comments
 (0)