@@ -4,44 +4,37 @@ import semmle.code.cpp.controlflow.ControlFlowGraph
44signature class TargetNode extends ControlFlowNode ;
55
66signature module DominatingSetConfigSig< TargetNode Target> {
7- predicate isTargetBehavior ( ControlFlowNode behavior , Target target ) ;
7+ predicate isTargetBehavior ( ControlFlowNode behavior , Target target ) ;
88
9- default predicate isBlockingBehavior ( ControlFlowNode behavior , Target target ) {
10- none ( )
11- }
9+ default predicate isBlockingBehavior ( ControlFlowNode behavior , Target target ) { none ( ) }
1210}
1311
1412/**
1513 * A module to find whether there exists a dominator set for a node which performs a relevant
1614 * behavior.
17- *
15+ *
1816 * For instance, we may wish to see that all paths leading to an `abort()` statement include a
1917 * logging call. In this case, the `abort()` statement is the `Target` node, and the config module
2018 * predicate `isTargetBehavior` logging statements.
21- *
19+ *
2220 * Additionally, the config may specify `isBlockingBehavior` to prevent searching too far for the
2321 * relevant behavior. For instance, if analyzing that all paths to an `fflush()` call are preceded
2422 * by a write, we should ignore paths from write operations that have already been flushed through
2523 * an intermediary `fflush()` call.
2624 */
2725module 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+ }
2836
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