@@ -40,3 +40,70 @@ class PreprocessorIfOrElif extends PreprocessorBranch {
4040 this instanceof PreprocessorElif
4141 }
4242}
43+
44+ /**
45+ * Holds if the preprocessor directive `m` is located at `filepath` and `startline`.
46+ */
47+ private predicate hasPreprocessorLocation ( PreprocessorDirective m , string filepath , int startline ) {
48+ m .getLocation ( ) .hasLocationInfo ( filepath , startline , _, _, _)
49+ }
50+
51+ /**
52+ * Holds if `first` and `second` are a pair of branch directives in the same file, such that they
53+ * share the same root if condition.
54+ */
55+ pragma [ noinline]
56+ private predicate isBranchDirectivePair (
57+ PreprocessorBranchDirective first , PreprocessorBranchDirective second , string filepath ,
58+ int b1StartLocation , int b2StartLocation
59+ ) {
60+ first .getIf ( ) = second .getIf ( ) and
61+ not first = second and
62+ hasPreprocessorLocation ( first , filepath , b1StartLocation ) and
63+ hasPreprocessorLocation ( second , filepath , b2StartLocation ) and
64+ b1StartLocation < b2StartLocation
65+ }
66+
67+ /**
68+ * Holds if `bd` is a branch directive in the range `filepath`, `startline`, `endline`.
69+ */
70+ pragma [ noinline]
71+ predicate isBranchDirectiveRange (
72+ PreprocessorBranchDirective bd , string filepath , int startline , int endline
73+ ) {
74+ hasPreprocessorLocation ( bd , filepath , startline ) and
75+ exists ( PreprocessorBranchDirective next |
76+ next = bd .getNext ( ) and
77+ // Avoid referencing filepath here, otherwise the optimiser will try to join
78+ // on it
79+ hasPreprocessorLocation ( next , _, endline )
80+ )
81+ }
82+
83+ /**
84+ * Holds if the macro `m` is defined within the branch directive `bd`.
85+ */
86+ pragma [ noinline]
87+ predicate isMacroDefinedWithinBranch ( PreprocessorBranchDirective bd , Macro m ) {
88+ exists ( string filepath , int startline , int endline , int macroline |
89+ isBranchDirectiveRange ( bd , filepath , startline , endline ) and
90+ hasPreprocessorLocation ( m , filepath , macroline ) and
91+ startline < macroline and
92+ endline > macroline
93+ )
94+ }
95+
96+ /**
97+ * Holds if the pair of macros are "conditional" i.e. only one of the macros is followed in any
98+ * particular compilation of the containing file.
99+ */
100+ predicate mutuallyExclusiveMacros ( Macro firstMacro , Macro secondMacro ) {
101+ exists (
102+ PreprocessorBranchDirective b1 , PreprocessorBranchDirective b2 , string filepath ,
103+ int b1StartLocation , int b2StartLocation
104+ |
105+ isBranchDirectivePair ( b1 , b2 , filepath , b1StartLocation , b2StartLocation ) and
106+ isMacroDefinedWithinBranch ( b1 , firstMacro ) and
107+ isMacroDefinedWithinBranch ( b2 , secondMacro )
108+ )
109+ }
0 commit comments