@@ -4,44 +4,37 @@ import semmle.code.cpp.controlflow.ControlFlowGraph
4
4
signature class TargetNode extends ControlFlowNode ;
5
5
6
6
signature module DominatingSetConfigSig< TargetNode Target> {
7
- predicate isTargetBehavior ( ControlFlowNode behavior , Target target ) ;
7
+ predicate isTargetBehavior ( ControlFlowNode behavior , Target target ) ;
8
8
9
- default predicate isBlockingBehavior ( ControlFlowNode behavior , Target target ) {
10
- none ( )
11
- }
9
+ default predicate isBlockingBehavior ( ControlFlowNode behavior , Target target ) { none ( ) }
12
10
}
13
11
14
12
/**
15
13
* A module to find whether there exists a dominator set for a node which performs a relevant
16
14
* behavior.
17
- *
15
+ *
18
16
* For instance, we may wish to see that all paths leading to an `abort()` statement include a
19
17
* logging call. In this case, the `abort()` statement is the `Target` node, and the config module
20
18
* predicate `isTargetBehavior` logging statements.
21
- *
19
+ *
22
20
* Additionally, the config may specify `isBlockingBehavior` to prevent searching too far for the
23
21
* relevant behavior. For instance, if analyzing that all paths to an `fflush()` call are preceded
24
22
* by a write, we should ignore paths from write operations that have already been flushed through
25
23
* an intermediary `fflush()` call.
26
24
*/
27
25
module DominatingBehavioralSet< TargetNode Target, DominatingSetConfigSig< Target > Config> {
26
+ /**
27
+ * Holds if this search step can reach the entry or a blocking node, without passing through a
28
+ * target behavior, indicating that the target is has no relevant dominator set.
29
+ */
30
+ private predicate searchStep ( ControlFlowNode node , Target target ) {
31
+ Config:: isBlockingBehavior ( node , target )
32
+ or
33
+ not Config:: isTargetBehavior ( node , target ) and
34
+ exists ( ControlFlowNode prev | prev = node .getAPredecessor ( ) | searchStep ( prev , target ) )
35
+ }
28
36
29
- /**
30
- * Holds if this search step can reach the entry or a blocking node, without passing through a
31
- * target behavior, indicating that the target is has no relevant dominator set.
32
- */
33
- private predicate searchStep ( ControlFlowNode node , Target target ) {
34
- Config:: isBlockingBehavior ( node , target )
35
- or
36
- not Config:: isTargetBehavior ( node , target ) and
37
- exists ( ControlFlowNode prev | prev = node .getAPredecessor ( ) |
38
- searchStep ( prev , target )
39
- )
40
- }
41
-
42
- predicate isDominatedByBehavior ( Target target ) {
43
- forex ( ControlFlowNode prev | prev = target .getAPredecessor ( ) |
44
- not searchStep ( prev , target )
45
- )
46
- }
47
- }
37
+ predicate isDominatedByBehavior ( Target target ) {
38
+ forex ( ControlFlowNode prev | prev = target .getAPredecessor ( ) | not searchStep ( prev , target ) )
39
+ }
40
+ }
0 commit comments