@@ -8,6 +8,7 @@ private import semmle.code.cpp.ir.internal.IntegerConstant as Ints
88private import semmle.code.cpp.ir.internal.IntegerInterval as Interval
99private import semmle.code.cpp.ir.implementation.internal.OperandTag
1010private import AliasConfiguration
11+ private import codeql.util.Boolean
1112
1213private class IntValue = Ints:: IntValue ;
1314
@@ -57,6 +58,86 @@ private predicate hasOperandMemoryAccess(
5758 else endBitOffset = Ints:: unknown ( )
5859}
5960
61+ private Allocation getAnAllocation ( AddressOperand address ) {
62+ hasResultMemoryAccess ( address , _, result , _, _, _, _, _, true ) or
63+ hasOperandMemoryAccess ( address , _, result , _, _, _, _, _, true )
64+ }
65+
66+ private module AllocationSet0 =
67+ QlBuiltins:: InternSets< AddressOperand , Allocation , getAnAllocation / 1 > ;
68+
69+ /**
70+ * A set of allocations containing at least 2 elements.
71+ */
72+ private class NonSingletonSets extends AllocationSet0:: Set {
73+ NonSingletonSets ( ) { strictcount ( Allocation var | this .contains ( var ) ) > 1 }
74+
75+ /** Gets an allocation from this set. */
76+ Allocation getAnAllocation ( ) { this .contains ( result ) }
77+
78+ /** Gets the string representation of this set. */
79+ string toString ( ) { result = "{" + strictconcat ( this .getAnAllocation ( ) .toString ( ) , ", " ) + "}" }
80+ }
81+
82+ /** Holds the instersection of `s1` and `s2` is non-empty. */
83+ private predicate hasOverlappingElement ( NonSingletonSets s1 , NonSingletonSets s2 ) {
84+ exists ( Allocation var |
85+ s1 .contains ( var ) and
86+ s2 .contains ( var )
87+ )
88+ }
89+
90+ private module AllocationSet =
91+ QlBuiltins:: EquivalenceRelation< NonSingletonSets , hasOverlappingElement / 2 > ;
92+
93+ /**
94+ * An equivalence class of a set of allocations.
95+ *
96+ * Any `VariableGroup` will be completely disjunct from any other
97+ * `VariableGroup`.
98+ */
99+ class VariableGroup extends AllocationSet:: EquivalenceClass {
100+ /** Gets the location of this set. */
101+ final Location getLocation ( ) { result = this .getIRFunction ( ) .getLocation ( ) }
102+
103+ /** Gets the enclosing `IRFunction` of this set. */
104+ final IRFunction getIRFunction ( ) {
105+ result = unique( | | this .getAnAllocation ( ) .getEnclosingIRFunction ( ) )
106+ }
107+
108+ /** Gets the type of elements contained in this set. */
109+ final Language:: LanguageType getType ( ) {
110+ strictcount ( Language:: LanguageType langType |
111+ exists ( Allocation var | var = this .getAnAllocation ( ) |
112+ hasResultMemoryAccess ( _, _, var , _, langType , _, _, _, true ) or
113+ hasOperandMemoryAccess ( _, _, var , _, langType , _, _, _, true )
114+ )
115+ ) = 1 and
116+ exists ( Allocation var | var = this .getAnAllocation ( ) |
117+ hasResultMemoryAccess ( _, _, var , _, result , _, _, _, true ) or
118+ hasOperandMemoryAccess ( _, _, var , _, result , _, _, _, true )
119+ )
120+ or
121+ strictcount ( Language:: LanguageType langType |
122+ exists ( Allocation var | var = this .getAnAllocation ( ) |
123+ hasResultMemoryAccess ( _, _, var , _, langType , _, _, _, true ) or
124+ hasOperandMemoryAccess ( _, _, var , _, langType , _, _, _, true )
125+ )
126+ ) > 1 and
127+ result = any ( IRUnknownType type ) .getCanonicalLanguageType ( )
128+ }
129+
130+ /** Gets an allocation of this set. */
131+ final Allocation getAnAllocation ( ) {
132+ exists ( AllocationSet0:: Set set |
133+ this = AllocationSet:: getEquivalenceClass ( set ) and
134+ set .contains ( result )
135+ )
136+ }
137+
138+ string toString ( ) { result = "{" + strictconcat ( this .getAnAllocation ( ) .toString ( ) , ", " ) + "}" }
139+ }
140+
60141private newtype TMemoryLocation =
61142 TVariableMemoryLocation (
62143 Allocation var , IRType type , Language:: LanguageType languageType , IntValue startBitOffset ,
@@ -83,6 +164,7 @@ private newtype TMemoryLocation =
83164 ) and
84165 ( isMayAccess = false or isMayAccess = true )
85166 } or
167+ TGroupedMemoryLocation ( VariableGroup vg , Boolean isMayAccess , Boolean isAll ) or
86168 TUnknownMemoryLocation ( IRFunction irFunc , boolean isMayAccess ) {
87169 isMayAccess = false or isMayAccess = true
88170 } or
@@ -126,7 +208,9 @@ abstract class MemoryLocation extends TMemoryLocation {
126208 /**
127209 * Gets an allocation associated with this `MemoryLocation`.
128210 *
129- * This always returns zero or one result.
211+ * This returns zero or one results in all cases except when `this` is an
212+ * instance of `GroupedMemoryLocation`. When `this` is an instance of
213+ * `GroupedMemoryLocation` this predicate always returns two or more results.
130214 */
131215 Allocation getAnAllocation ( ) { none ( ) }
132216
@@ -259,6 +343,73 @@ class VariableMemoryLocation extends TVariableMemoryLocation, AllocationMemoryLo
259343 }
260344}
261345
346+ /**
347+ * A group of allocations represented as a single memory location.
348+ *
349+ * If `isAll()` holds then this memory location represents all the enclosing
350+ * allocations, and if `isSome()` holds then this memory location represents
351+ * one or more of the enclosing allocations.
352+ *
353+ * For example, consider the following snippet:
354+ * ```
355+ * int* p;
356+ * int a, b;
357+ * if(b) {
358+ * p = &a;
359+ * } else {
360+ * p = &b;
361+ * }
362+ * *p = 42;
363+ * ```
364+ *
365+ * The write memory location associated with the write to `*p` writes to a
366+ * grouped memory location representing the _some_ allocation in the set
367+ * `{a, b}`, and the subsequent `Chi` instruction merges the new value of
368+ * `{a, b}` into a memory location that represents _all_ of the allocations
369+ * in the set.
370+ */
371+ class GroupedMemoryLocation extends TGroupedMemoryLocation , MemoryLocation {
372+ VariableGroup vg ;
373+ boolean isMayAccess ;
374+ boolean isAll ;
375+
376+ GroupedMemoryLocation ( ) { this = TGroupedMemoryLocation ( vg , isMayAccess , isAll ) }
377+
378+ final override Location getLocation ( ) { result = vg .getLocation ( ) }
379+
380+ final override IRFunction getIRFunction ( ) { result = vg .getIRFunction ( ) }
381+
382+ final override predicate isMayAccess ( ) { isMayAccess = true }
383+
384+ final override string getUniqueId ( ) {
385+ if this .isAll ( )
386+ then result = "All{" + strictconcat ( vg .getAnAllocation ( ) .getUniqueId ( ) , ", " ) + "}"
387+ else result = "Some{" + strictconcat ( vg .getAnAllocation ( ) .getUniqueId ( ) , ", " ) + "}"
388+ }
389+
390+ final override string toStringInternal ( ) { result = this .getUniqueId ( ) }
391+
392+ final override Language:: LanguageType getType ( ) { result = vg .getType ( ) }
393+
394+ final override VirtualVariable getVirtualVariable ( ) {
395+ if allocationEscapes ( this .getAnAllocation ( ) )
396+ then result = TAllAliasedMemory ( vg .getIRFunction ( ) , false )
397+ else result = TGroupedMemoryLocation ( vg , false , true )
398+ }
399+
400+ /** Gets an allocation of this memory location. */
401+ override Allocation getAnAllocation ( ) { result = vg .getAnAllocation ( ) }
402+
403+ /** Gets the set of allocations associated with this memory location. */
404+ VariableGroup getGroup ( ) { result = vg }
405+
406+ /** Holds if this memory location represents all the enclosing allocations. */
407+ predicate isAll ( ) { isAll = true }
408+
409+ /** Holds if this memory location represents one or more of the enclosing allocations. */
410+ predicate isSome ( ) { isAll = false }
411+ }
412+
262413class EntireAllocationMemoryLocation extends TEntireAllocationMemoryLocation ,
263414 AllocationMemoryLocation
264415{
@@ -294,6 +445,14 @@ class VariableVirtualVariable extends VariableMemoryLocation, VirtualVariable {
294445 }
295446}
296447
448+ class GroupedVirtualVariable extends GroupedMemoryLocation , VirtualVariable {
449+ GroupedVirtualVariable ( ) {
450+ forex ( Allocation var | var = this .getAnAllocation ( ) | not allocationEscapes ( var ) ) and
451+ not this .isMayAccess ( ) and
452+ this .isAll ( )
453+ }
454+ }
455+
297456/**
298457 * An access to memory that is not known to be confined to a specific `IRVariable`.
299458 */
0 commit comments