Merge branch 'main' into generate-more-value-preserving-summaries-2

This commit is contained in:
Mathias Vorreiter Pedersen
2025-05-02 10:51:11 +01:00
240 changed files with 3011 additions and 1935 deletions

View File

@@ -16,7 +16,7 @@ signature module ModelPrintingLangSig {
}
module ModelPrintingImpl<ModelPrintingLangSig Lang> {
signature module ModelPrintingSig {
signature module ModelPrintingSummarySig {
/**
* The class of APIs relevant for model generation.
*/
@@ -24,6 +24,16 @@ module ModelPrintingImpl<ModelPrintingLangSig Lang> {
Lang::Callable lift();
}
/**
* Gets the string representation of the provenance of the models.
*/
string getProvenance();
}
signature module ModelPrintingSourceOrSinkSig {
/**
* The class of APIs relevant for model generation.
*/
class SourceOrSinkApi extends Lang::Callable;
/**
@@ -32,14 +42,14 @@ module ModelPrintingImpl<ModelPrintingLangSig Lang> {
string getProvenance();
}
module ModelPrinting<ModelPrintingSig Printing> {
/**
* Computes the first columns for MaD rows used for summaries, sources and sinks.
*/
private string asPartialModel(Lang::Callable api) {
result = strictconcat(int i | | Lang::partialModelRow(api, i), ";" order by i) + ";"
}
/**
* Computes the first columns for MaD rows used for summaries, sources and sinks.
*/
private string asPartialModel(Lang::Callable api) {
result = strictconcat(int i | | Lang::partialModelRow(api, i), ";" order by i) + ";"
}
module ModelPrintingSummary<ModelPrintingSummarySig Printing> {
/**
* Computes the first columns for neutral MaD rows.
*/
@@ -108,7 +118,9 @@ module ModelPrintingImpl<ModelPrintingLangSig Lang> {
preservesValue = false and
result = asSummaryModel(api, input, output, "taint", lift)
}
}
module ModelPrintingSourceOrSink<ModelPrintingSourceOrSinkSig Printing> {
/**
* Gets the sink model for `api` with `input` and `kind`.
*/