@@ -46,6 +46,11 @@ signature module ExtensionsSig {
4646 predicate neutralModel (
4747 string namespace , string type , string name , string signature , string kind , string provenance
4848 ) ;
49+
50+ /**
51+ * Holds if the package `package` is part of the group `group`.
52+ */
53+ predicate packageGrouping ( string group , string package ) ;
4954}
5055
5156signature module InputSig {
@@ -154,21 +159,44 @@ module ModelsAsData<ExtensionsSig Extensions, InputSig Input> {
154159 )
155160 }
156161
162+ /** Gets the prefix for a group of packages/namespaces. */
163+ private string groupPrefix ( ) { result = "group:" }
164+
165+ /**
166+ * Gets a package/namespace represented by `packageOrGroup`.
167+ *
168+ * If `packageOrGroup` is of the form `group:<groupname>` then `result` is a
169+ * package/namespace in the group `<groupname>`, as determined by `packageGrouping`.
170+ * Otherwise, `result` is `packageOrGroup`.
171+ */
172+ bindingset [ namespaceOrGroup]
173+ private string getNamespace ( string namespaceOrGroup ) {
174+ not exists ( string group | namespaceOrGroup = groupPrefix ( ) + group ) and
175+ result = namespaceOrGroup
176+ or
177+ exists ( string group |
178+ Extensions:: packageGrouping ( group , result ) and
179+ namespaceOrGroup = groupPrefix ( ) + group
180+ )
181+ }
182+
157183 /**
158184 * Holds if a source model exists for the given parameters.
159185 */
160186 predicate sourceModel (
161187 string namespace , string type , boolean subtypes , string name , string signature , string ext ,
162188 string output , string kind , string provenance , string model
163189 ) {
164- exists ( QlBuiltins:: ExtensionId madId |
165- Extensions:: sourceModel ( namespace , type , subtypes , name , signature , ext , output , kind ,
166- provenance , madId ) and
167- model = "MaD:" + madId .toString ( )
190+ exists ( string namespaceOrGroup | namespace = getNamespace ( namespaceOrGroup ) |
191+ exists ( QlBuiltins:: ExtensionId madId |
192+ Extensions:: sourceModel ( namespaceOrGroup , type , subtypes , name , signature , ext , output ,
193+ kind , provenance , madId ) and
194+ model = "MaD:" + madId .toString ( )
195+ )
196+ or
197+ Input:: additionalSourceModel ( namespaceOrGroup , type , subtypes , name , signature , ext , output ,
198+ kind , provenance , model )
168199 )
169- or
170- Input:: additionalSourceModel ( namespace , type , subtypes , name , signature , ext , output , kind ,
171- provenance , model )
172200 }
173201
174202 /**
@@ -178,14 +206,42 @@ module ModelsAsData<ExtensionsSig Extensions, InputSig Input> {
178206 string namespace , string type , boolean subtypes , string name , string signature , string ext ,
179207 string input , string kind , string provenance , string model
180208 ) {
181- exists ( QlBuiltins:: ExtensionId madId |
182- Extensions:: sinkModel ( namespace , type , subtypes , name , signature , ext , input , kind ,
209+ exists ( string namespaceOrGroup | namespace = getNamespace ( namespaceOrGroup ) |
210+ exists ( QlBuiltins:: ExtensionId madId |
211+ Extensions:: sinkModel ( namespaceOrGroup , type , subtypes , name , signature , ext , input , kind ,
212+ provenance , madId ) and
213+ model = "MaD:" + madId .toString ( )
214+ )
215+ or
216+ Input:: additionalSinkModel ( namespaceOrGroup , type , subtypes , name , signature , ext , input ,
217+ kind , provenance , model )
218+ )
219+ }
220+
221+ /** Holds if a barrier model exists for the given parameters. */
222+ predicate barrierModel (
223+ string namespace , string type , boolean subtypes , string name , string signature , string ext ,
224+ string output , string kind , string provenance , string model
225+ ) {
226+ exists ( string namespaceOrGroup , QlBuiltins:: ExtensionId madId |
227+ namespace = getNamespace ( namespaceOrGroup ) and
228+ Extensions:: barrierModel ( namespaceOrGroup , type , subtypes , name , signature , ext , output , kind ,
183229 provenance , madId ) and
184230 model = "MaD:" + madId .toString ( )
185231 )
186- or
187- Input:: additionalSinkModel ( namespace , type , subtypes , name , signature , ext , input , kind ,
188- provenance , model )
232+ }
233+
234+ /** Holds if a barrier guard model exists for the given parameters. */
235+ predicate barrierGuardModel (
236+ string namespace , string type , boolean subtypes , string name , string signature , string ext ,
237+ string input , string acceptingvalue , string kind , string provenance , string model
238+ ) {
239+ exists ( string namespaceOrGroup , QlBuiltins:: ExtensionId madId |
240+ namespace = getNamespace ( namespaceOrGroup ) and
241+ Extensions:: barrierGuardModel ( namespaceOrGroup , type , subtypes , name , signature , ext , input ,
242+ acceptingvalue , kind , provenance , madId ) and
243+ model = "MaD:" + madId .toString ( )
244+ )
189245 }
190246
191247 /**
@@ -195,14 +251,27 @@ module ModelsAsData<ExtensionsSig Extensions, InputSig Input> {
195251 string namespace , string type , boolean subtypes , string name , string signature , string ext ,
196252 string input , string output , string kind , string provenance , string model
197253 ) {
198- exists ( QlBuiltins:: ExtensionId madId |
199- Extensions:: summaryModel ( namespace , type , subtypes , name , signature , ext , input , output , kind ,
200- provenance , madId ) and
201- model = "MaD:" + madId .toString ( )
254+ exists ( string namespaceOrGroup | namespace = getNamespace ( namespaceOrGroup ) |
255+ exists ( QlBuiltins:: ExtensionId madId |
256+ Extensions:: summaryModel ( namespaceOrGroup , type , subtypes , name , signature , ext , input ,
257+ output , kind , provenance , madId ) and
258+ model = "MaD:" + madId .toString ( )
259+ )
260+ or
261+ Input:: additionalSummaryModel ( namespaceOrGroup , type , subtypes , name , signature , ext , input ,
262+ output , kind , provenance , model )
263+ )
264+ }
265+
266+ /**
267+ * Holds if a neutral model exists for the given parameters.
268+ */
269+ predicate neutralModel (
270+ string namespace , string type , string name , string signature , string kind , string provenance
271+ ) {
272+ exists ( string namespaceOrGroup | namespace = getNamespace ( namespaceOrGroup ) |
273+ Extensions:: neutralModel ( namespaceOrGroup , type , name , signature , kind , provenance )
202274 )
203- or
204- Input:: additionalSummaryModel ( namespace , type , subtypes , name , signature , ext , input , output ,
205- kind , provenance , model )
206275 }
207276
208277 private predicate relevantNamespace ( string namespace ) {
0 commit comments