Shared: Improvements to content-sensitive model generation

This commit is contained in:
Tom Hvitved
2025-11-26 10:33:52 +01:00
parent 464d2cd5fc
commit 666855dbd7
3 changed files with 29 additions and 17 deletions

View File

@@ -299,8 +299,7 @@ impl<T> MyOption<T> {
} }
// summary=<test::option::MyOption>::insert;Argument[0];Argument[self].Reference.Field[test::option::MyOption::MySome(0)];value;dfc-generated // summary=<test::option::MyOption>::insert;Argument[0];Argument[self].Reference.Field[test::option::MyOption::MySome(0)];value;dfc-generated
// This summary is currently missing because of access path limit // summary=<test::option::MyOption>::insert;Argument[0];ReturnValue.Reference;value;dfc-generated
// summary-MISSING=<test::option::MyOption>::insert;Argument[0];ReturnValue.Reference;value;dfc-generated
// The content of `self` is overwritten so it does not flow to the return value. // The content of `self` is overwritten so it does not flow to the return value.
// SPURIOUS-summary=<test::option::MyOption>::insert;Argument[self].Reference.Field[test::option::MyOption::MySome(0)];ReturnValue.Reference;value;dfc-generated // SPURIOUS-summary=<test::option::MyOption>::insert;Argument[self].Reference.Field[test::option::MyOption::MySome(0)];ReturnValue.Reference;value;dfc-generated
pub fn insert(&mut self, value: T) -> &mut T { pub fn insert(&mut self, value: T) -> &mut T {
@@ -311,8 +310,7 @@ impl<T> MyOption<T> {
} }
// summary=<test::option::MyOption>::get_or_insert;Argument[0];Argument[self].Reference.Field[test::option::MyOption::MySome(0)];value;dfc-generated // summary=<test::option::MyOption>::get_or_insert;Argument[0];Argument[self].Reference.Field[test::option::MyOption::MySome(0)];value;dfc-generated
// This summary is currently missing because of access path limit // summary=<test::option::MyOption>::get_or_insert;Argument[0];ReturnValue.Reference;value;dfc-generated
// summary-MISSING=<test::option::MyOption>::get_or_insert;Argument[0];ReturnValue.Reference;value;dfc-generated
// summary=<test::option::MyOption>::get_or_insert;Argument[self].Reference.Field[test::option::MyOption::MySome(0)];ReturnValue.Reference;value;dfc-generated // summary=<test::option::MyOption>::get_or_insert;Argument[self].Reference.Field[test::option::MyOption::MySome(0)];ReturnValue.Reference;value;dfc-generated
pub fn get_or_insert(&mut self, value: T) -> &mut T { pub fn get_or_insert(&mut self, value: T) -> &mut T {
self.get_or_insert_with(|| value) self.get_or_insert_with(|| value)
@@ -328,7 +326,7 @@ impl<T> MyOption<T> {
// summary=<test::option::MyOption>::get_or_insert_with;Argument[self].Reference.Field[test::option::MyOption::MySome(0)];ReturnValue.Reference;value;dfc-generated // summary=<test::option::MyOption>::get_or_insert_with;Argument[self].Reference.Field[test::option::MyOption::MySome(0)];ReturnValue.Reference;value;dfc-generated
// summary=<test::option::MyOption>::get_or_insert_with;Argument[0].ReturnValue;Argument[self].Reference.Field[test::option::MyOption::MySome(0)];value;dfc-generated // summary=<test::option::MyOption>::get_or_insert_with;Argument[0].ReturnValue;Argument[self].Reference.Field[test::option::MyOption::MySome(0)];value;dfc-generated
// SPURIOUS-summary=<test::option::MyOption>::get_or_insert_with;Argument[0];Argument[self].Reference.Field[test::option::MyOption::MySome(0)];value;dfc-generated // summary=<test::option::MyOption>::get_or_insert_with;Argument[0].ReturnValue;ReturnValue.Reference;value;dfc-generated
pub fn get_or_insert_with<F>(&mut self, f: F) -> &mut T pub fn get_or_insert_with<F>(&mut self, f: F) -> &mut T
where where
F: FnOnce() -> T, F: FnOnce() -> T,

View File

@@ -75,6 +75,9 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
/** Gets a limit on the number of reads out of sources and number of stores into sinks. */ /** Gets a limit on the number of reads out of sources and number of stores into sinks. */
default int accessPathLimit() { result = Lang::accessPathLimit() } default int accessPathLimit() { result = Lang::accessPathLimit() }
/** Gets the access path limit used in the internal invocation of the standard data flow library. */
default int accessPathLimitInternal() { result = Lang::accessPathLimit() }
/** Holds if `c` is relevant for reads out of sources or stores into sinks. */ /** Holds if `c` is relevant for reads out of sources or stores into sinks. */
default predicate isRelevantContent(ContentSet c) { any() } default predicate isRelevantContent(ContentSet c) { any() }
} }
@@ -110,7 +113,7 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
FlowFeature getAFeature() { result = ContentConfig::getAFeature() } FlowFeature getAFeature() { result = ContentConfig::getAFeature() }
predicate accessPathLimit = ContentConfig::accessPathLimit/0; predicate accessPathLimit = ContentConfig::accessPathLimitInternal/0;
// needed to record reads/stores inside summarized callables // needed to record reads/stores inside summarized callables
predicate includeHiddenNodes() { any() } predicate includeHiddenNodes() { any() }
@@ -274,6 +277,16 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
) )
} }
/**
* Gets the length of this access path.
*/
int length() {
this = TAccessPathNil() and
result = 0
or
result = this.getTail().length() + 1
}
/** /**
* Gets the content set at index `i` in this access path, if any. * Gets the content set at index `i` in this access path, if any.
*/ */

View File

@@ -703,14 +703,17 @@ module MakeModelGeneratorFactory<
} }
/** /**
* Holds if the access path `ap` is not a parameter or returnvalue of a callback * Holds if `ap` is valid for generating summary models.
* stored in a field.
* *
* That is, we currently don't include summaries that rely on parameters or return values * We currently don't include summaries that rely on parameters or return values
* of callbacks stored in fields. * of callbacks stored in fields, as those are not supported by the data flow
* library.
*
* We also exclude access paths with contents not supported by `printContent`.
*/ */
private predicate validateAccessPath(PropagateContentFlow::AccessPath ap) { private predicate validateAccessPath(PropagateContentFlow::AccessPath ap) {
not (mentionsField(ap) and mentionsCallback(ap)) not (mentionsField(ap) and mentionsCallback(ap)) and
forall(int i | i in [0 .. ap.length() - 1] | exists(getContent(ap, i)))
} }
private predicate apiFlow( private predicate apiFlow(
@@ -720,7 +723,9 @@ module MakeModelGeneratorFactory<
) { ) {
PropagateContentFlow::flow(p, reads, returnNodeExt, stores, preservesValue) and PropagateContentFlow::flow(p, reads, returnNodeExt, stores, preservesValue) and
getEnclosingCallable(returnNodeExt) = api and getEnclosingCallable(returnNodeExt) = api and
getEnclosingCallable(p) = api getEnclosingCallable(p) = api and
validateAccessPath(reads) and
validateAccessPath(stores)
} }
/** /**
@@ -763,9 +768,7 @@ module MakeModelGeneratorFactory<
PropagateContentFlow::AccessPath reads, ReturnNodeExt returnNodeExt, PropagateContentFlow::AccessPath reads, ReturnNodeExt returnNodeExt,
PropagateContentFlow::AccessPath stores, boolean preservesValue PropagateContentFlow::AccessPath stores, boolean preservesValue
) { ) {
PropagateContentFlow::flow(p, reads, returnNodeExt, stores, preservesValue) and apiFlow(api, p, reads, returnNodeExt, stores, preservesValue) and
getEnclosingCallable(returnNodeExt) = api and
getEnclosingCallable(p) = api and
p = api.getARelevantParameterNode() p = api.getARelevantParameterNode()
} }
@@ -956,8 +959,6 @@ module MakeModelGeneratorFactory<
input = parameterNodeAsExactInput(p) + printReadAccessPath(reads) and input = parameterNodeAsExactInput(p) + printReadAccessPath(reads) and
output = getExactOutput(returnNodeExt) + printStoreAccessPath(stores) and output = getExactOutput(returnNodeExt) + printStoreAccessPath(stores) and
input != output and input != output and
validateAccessPath(reads) and
validateAccessPath(stores) and
( (
if mentionsField(reads) or mentionsField(stores) if mentionsField(reads) or mentionsField(stores)
then lift = false and api.isRelevant() then lift = false and api.isRelevant()