C++: Add a read and store step that replace ArrayContent with FieldContent when we realize that the target of a store is a field.

This commit is contained in:
Mathias Vorreiter Pedersen
2020-09-18 17:12:09 +02:00
parent dff9f8264b
commit b6b17fe95e
2 changed files with 107 additions and 7 deletions

View File

@@ -211,10 +211,17 @@ private predicate fieldStoreStepNoChi(Node node1, FieldContent f, PostUpdateNode
)
}
private FieldAddressInstruction getFieldInstruction(Instruction instr) {
result = instr or
result = instr.(CopyValueInstruction).getUnary()
}
pragma[noinline]
private predicate getWrittenField(StoreInstruction store, Field f, Class c) {
private predicate getWrittenField(Instruction instr, Field f, Class c) {
exists(FieldAddressInstruction fa |
fa = store.getDestinationAddress() and
fa =
getFieldInstruction([any(StoreInstruction store | instr = store).getDestinationAddress(),
any(WriteSideEffectInstruction write | instr = write).getDestinationAddress()]) and
f = fa.getField() and
c = f.getDeclaringType()
)
@@ -265,7 +272,23 @@ private predicate arrayStoreStepChi(Node node1, ArrayContent a, PostUpdateNode n
predicate storeStep(Node node1, Content f, PostUpdateNode node2) {
fieldStoreStepNoChi(node1, f, node2) or
fieldStoreStepChi(node1, f, node2) or
arrayStoreStepChi(node1, f, node2)
arrayStoreStepChi(node1, f, node2) or
fieldStoreStepAfterArraySuppression(node1, f, node2)
}
// This predicate pushes the correct `FieldContent` onto the access path when the
// `suppressArrayRead` predicate has popped off an `ArrayContent`.
private predicate fieldStoreStepAfterArraySuppression(
Node node1, FieldContent f, PostUpdateNode node2
) {
exists(BufferMayWriteSideEffectInstruction write, ChiInstruction chi, Class c |
not chi.isResultConflated() and
node1.asInstruction() = chi and
node2.asInstruction() = chi and
chi.getPartial() = write and
getWrittenField(write, f.getAField(), c) and
f.hasOffset(c, _, _)
)
}
bindingset[result, i]
@@ -302,11 +325,53 @@ private predicate fieldReadStep(Node node1, FieldContent f, Node node2) {
)
}
predicate suppressArrayRead(Node node1, ArrayContent a, Node node2) {
a = TArrayContent() and
exists(BufferMayWriteSideEffectInstruction write, ChiInstruction chi |
node1.asInstruction() = write and
node2.asInstruction() = chi and
chi.getPartial() = write and
getWrittenField(write, _, _)
)
}
private class ArrayToPointerConvertInstruction extends ConvertInstruction {
ArrayToPointerConvertInstruction() {
this.getUnary().getResultType() instanceof ArrayType and
this.getResultType() instanceof PointerType
}
}
private predicate arrayReadStep(Node node1, ArrayContent a, Node node2) {
a = TArrayContent() and
exists(LoadInstruction load |
node1.asInstruction() = load.getSourceValueOperand().getAnyDef() and
load = node2.asInstruction()
(
// In cases such as:
// ```cpp
// void f(int* pa) {
// *pa = source();
// }
// ...
// int x;
// f(&x);
// use(x);
// ```
// the load on `x` in `use(x)` will exactly overlap with its definition (in this case the definition
// is a `BufferMayWriteSideEffect`).
exists(LoadInstruction load |
node1.asInstruction() = load.getSourceValue() and
load = node2.asInstruction()
)
or
// Explicit dereferences such as `*p` or `p[i]` where `p` is a pointer or array.
exists(LoadInstruction load |
node1.asInstruction() = load.getSourceValueOperand().getAnyDef() and
load = node2.asInstruction() and
(
load.getSourceAddress() instanceof LoadInstruction or
load.getSourceAddress() instanceof ArrayToPointerConvertInstruction or
load.getSourceAddress() instanceof PointerAddInstruction
)
)
)
}
@@ -317,7 +382,19 @@ private predicate arrayReadStep(Node node1, ArrayContent a, Node node2) {
*/
predicate readStep(Node node1, Content f, Node node2) {
fieldReadStep(node1, f, node2) or
arrayReadStep(node1, f, node2)
arrayReadStep(node1, f, node2) or
// When a store step happens in a function that looks like an array write such as:
// ```cpp
// void f(int* pa) {
// *pa = source();
// }
// ```
// it can be a write to an array, but it can also happen that `f` is called as `f(&a.x)`. If that is
// the case, the `ArrayContent` that was written by the call to `f` should be popped off the access
// path, and a `FieldContent` containing `x` should be pushed instead.
// So this case pops `ArrayContent` off the access path, and the `fieldStoreStepAfterArraySuppression`
// predicate in `storeStep` ensures that we push the right `FieldContent` onto the access path.
suppressArrayRead(node1, f, node2)
}
/**

View File

@@ -389,6 +389,29 @@ private class ExplicitSingleFieldStoreQualifierNode extends PartialDefinitionNod
}
}
private FieldAddressInstruction getFieldInstruction(Instruction instr) {
result = instr or
result = instr.(CopyValueInstruction).getUnary()
}
private class BufferMayWriteSideEffectFieldStoreQualifierNode extends PartialDefinitionNode {
override ChiInstruction instr;
BufferMayWriteSideEffectInstruction write;
FieldAddressInstruction field;
BufferMayWriteSideEffectFieldStoreQualifierNode() {
not instr.isResultConflated() and
instr.getPartial() = write and
field = getFieldInstruction(write.getDestinationAddress())
}
override Node getPreUpdateNode() { result.asOperand() = instr.getTotalOperand() }
override Expr getDefinedExpr() {
result = field.getObjectAddress().getUnconvertedResultExpression()
}
}
/**
* The `PostUpdateNode` that is the target of a `arrayStoreStepChi` store step. The overriden
* `ChiInstruction` corresponds to the instruction represented by `node2` in `arrayStoreStepChi`.