@@ -147,7 +147,7 @@ abstract class Indirection extends Type {
147147 *
148148 * `certain` is `true` if this write is guaranteed to write to the address.
149149 */
150- predicate isAdditionalWrite ( Node0Impl value , Operand address , boolean certain ) { none ( ) }
150+ predicate isAdditionalWrite ( Node0Impl value , Operand address , Certainty certain ) { none ( ) }
151151
152152 /**
153153 * Gets the base type of this indirection, after specifiers have been deeply
@@ -198,11 +198,11 @@ private module IteratorIndirections {
198198 baseType = super .getValueType ( )
199199 }
200200
201- override predicate isAdditionalWrite ( Node0Impl value , Operand address , boolean certain ) {
201+ override predicate isAdditionalWrite ( Node0Impl value , Operand address , Certainty certain ) {
202202 exists ( CallInstruction call | call .getArgumentOperand ( 0 ) = value .asOperand ( ) |
203203 this = call .getStaticCallTarget ( ) .( Function ) .getClassAndName ( "operator=" ) and
204204 address = call .getThisArgumentOperand ( ) and
205- certain = false
205+ certain instanceof AlwaysUncertain
206206 )
207207 }
208208
@@ -271,10 +271,41 @@ predicate isDereference(Instruction deref, Operand address, boolean additional)
271271 additional = false
272272}
273273
274- predicate isWrite ( Node0Impl value , Operand address , boolean certain ) {
274+ private newtype TCertainty =
275+ TCertainWhenAddressIsCertain ( ) or
276+ TAlwaysCertain ( ) or
277+ TAlwaysUncertain ( )
278+
279+ abstract private class Certainty extends TCertainty {
280+ abstract predicate isCertain ( boolean addressIsCertain ) ;
281+
282+ abstract string toString ( ) ;
283+ }
284+
285+ private class CertainWhenAddressIsCertain extends Certainty , TCertainWhenAddressIsCertain {
286+ override predicate isCertain ( boolean addressIsCertain ) { addressIsCertain = true }
287+
288+ override string toString ( ) { result = "CertainWhenAddressIsCertain" }
289+ }
290+
291+ private class AlwaysCertain extends Certainty , TAlwaysCertain {
292+ override predicate isCertain ( boolean addressIsCertain ) {
293+ addressIsCertain = true or addressIsCertain = false
294+ }
295+
296+ override string toString ( ) { result = "AlwaysCertain" }
297+ }
298+
299+ private class AlwaysUncertain extends Certainty , TAlwaysUncertain {
300+ override predicate isCertain ( boolean addressIsCertain ) { none ( ) }
301+
302+ override string toString ( ) { result = "AlwaysUncertain" }
303+ }
304+
305+ predicate isWrite ( Node0Impl value , Operand address , Certainty certain ) {
275306 any ( Indirection ind ) .isAdditionalWrite ( value , address , certain )
276307 or
277- certain = true and
308+ certain instanceof CertainWhenAddressIsCertain and
278309 (
279310 exists ( StoreInstruction store |
280311 value .asInstruction ( ) = store and
@@ -718,16 +749,18 @@ private module Cached {
718749 int indirectionIndex
719750 ) {
720751 exists (
721- boolean writeIsCertain , boolean addressIsCertain , int ind0 , CppType type , int lower , int upper
752+ Certainty writeIsCertain , boolean addressIsCertain , int ind0 , CppType type , int lower ,
753+ int upper
722754 |
723755 isWrite ( value , address , writeIsCertain ) and
724756 isDefImpl ( address , base , ind0 , addressIsCertain ) and
725- certain = writeIsCertain .booleanAnd ( addressIsCertain ) and
726757 type = getLanguageType ( address ) and
727758 upper = countIndirectionsForCppType ( type ) and
728759 ind = ind0 + [ lower .. upper ] and
729760 indirectionIndex = ind - ( ind0 + lower ) and
730761 lower = getMinIndirectionsForType ( any ( Type t | type .hasUnspecifiedType ( t , _) ) )
762+ |
763+ if writeIsCertain .isCertain ( addressIsCertain ) then certain = true else certain = false
731764 )
732765 }
733766
0 commit comments