IA159 Formal Methods for Software Analysis Program Slicing and Points-to Analysis Jan Strejˇcek Faculty of Informatics Masaryk University Focus and sources focus slicing via dependence graphs points-to analysis static single assignment (SSA) data dependencies control dependencies sources M. Chalupa: Program Slicing and Symbolic Execution for Verification, PhD thesis, 2021. B.Alpern, M. N. Wegman, and F. K. Zadeck: Detecting equality of variables in programs, POPL 1988. IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 2/65 Program slicing Program slicing reduces a given program by removing statements that are irrelevant for a given slicing criterion. IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 3/65 Program slicing Program slicing reduces a given program by removing statements that are irrelevant for a given slicing criterion. A typical slicing criterion is a specific statement or a set of statements. Sliced program should preserve all executions of these statements, i.e., preserve the reachability of these statements and all data they process. IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 4/65 Program slicing Program slicing reduces a given program by removing statements that are irrelevant for a given slicing criterion. A typical slicing criterion is a specific statement or a set of statements. Sliced program should preserve all executions of these statements, i.e., preserve the reachability of these statements and all data they process. introduced in M. D. Weiser: Program Slicing, ICSE 1981 the approach based on dependence graphs presented in K. J. Ottenstein and L. M. Ottenstein: The Program Dependence Graph in a Software Development Environment, SDE 1984 IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 5/65 Applications of program slicing program debugging code comprehension code optimization including automatic parallelization software verification . . . IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 6/65 Applications of program slicing program debugging code comprehension code optimization including automatic parallelization software verification . . . a typical application in software verification (implemented in Symbiotic) 1 find potentially erroneous statements by a cheap analysis 2 slice the program to preserve all executions of these statements 3 verify the sliced program IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 7/65 Simple example Which statements are irrelevant for the assert? 1 z = z + 3; 2 if (z > 0) { 3 x = z + 1; 4 z = 3 * x; 5 } else { 6 y = z + 5; 7 x = x * x - z; 8 } 9 if (x > y) 10 z = x - 1; 11 assert(x > 0); IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 8/65 Simple example Which statements are irrelevant for the assert? 1 z = z + 3; 2 if (z > 0) { 3 x = z + 1; 4 z = 3 * x; 5 } else { 6 y = z + 5; 7 x = x * x - z; 8 } 9 if (x > y) 10 z = x - 1; 11 assert(x > 0); 1 z = z + 3; 2 if (z > 0) { 3 x = z + 1; 4 5 } else { 6 7 x = x * x - z; 8 } 9 10 11 assert(x > 0); IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 9/65 Basic slicing algorithm 1 build a dependence graph for the given program nodes are statements edges correspond to data and control dependencies 2 sliced program corresponds to the nodes that are backward reachable from the slicing criterion(s) intuitive meanings a statement r is data dependent on a statement w if there exists a program execution where r reads a value from a memory that has been written by w a statement n is control dependent on a statement b if b is the closest point where a program execution may go some way that misses n in practice, we compute overapproximations IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 10/65 Simple dependency graph 1 z = z + 3; 2 if (z > 0) { 3 x = z + 1; 4 5 } else { 6 7 x = x * x - z; 8 } 9 10 11 assert(x > 0); z = 3 * x; y = z + 5; if (x > y) z = x - 1; IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 11/65 Simple dependency graph 1 z = z + 3; 2 if (z > 0) { 3 x = z + 1; 4 5 } else { 6 7 x = x * x - z; 8 } 9 10 11 assert(x > 0); z = 3 * x; y = z + 5; if (x > y) z = x - 1; 1: z = z + 3 2: if (z > 0) 3: x = z + 1 4: z = 3 * x 6: y = z + 5 7: x = x * x - z 9: if (x > y) 10: z = x - 1 11: assert(x > 0) r is data dependent on w if there exists a program execution where r reads a value from a memory that has been written by w w r n is control dependent on b if b is the closest point where the program may go some way that misses n b n IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 12/65 Simple dependency graph 1 z = z + 3; 2 if (z > 0) { 3 x = z + 1; 4 5 } else { 6 7 x = x * x - z; 8 } 9 10 11 assert(x > 0); z = 3 * x; y = z + 5; if (x > y) z = x - 1; 1: z = z + 3 2: if (z > 0) 3: x = z + 1 4: z = 3 * x 6: y = z + 5 7: x = x * x - z 9: if (x > y) 10: z = x - 1 11: assert(x > 0) r is data dependent on w if there exists a program execution where r reads a value from a memory that has been written by w w r n is control dependent on b if b is the closest point where the program may go some way that misses n b n IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 13/65 Simple dependency graph 1 z = z + 3; 2 if (z > 0) { 3 x = z + 1; 4 5 } else { 6 7 x = x * x - z; 8 } 9 10 11 assert(x > 0); z = 3 * x; y = z + 5; if (x > y) z = x - 1; 1: z = z + 3 2: if (z > 0) 3: x = z + 1 4: z = 3 * x 6: y = z + 5 7: x = x * x - z 9: if (x > y) 10: z = x - 1 11: assert(x > 0) r is data dependent on w if there exists a program execution where r reads a value from a memory that has been written by w w r n is control dependent on b if b is the closest point where the program may go some way that misses n b n IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 14/65 Simple dependency graph 1 z = z + 3; 2 if (z > 0) { 3 x = z + 1; 4 5 } else { 6 7 x = x * x - z; 8 } 9 10 11 assert(x > 0); z = 3 * x; y = z + 5; if (x > y) z = x - 1; 1: z = z + 3 2: if (z > 0) 3: x = z + 1 4: z = 3 * x 6: y = z + 5 7: x = x * x - z 9: if (x > y) 10: z = x - 1 11: assert(x > 0) r is data dependent on w if there exists a program execution where r reads a value from a memory that has been written by w w r n is control dependent on b if b is the closest point where the program may go some way that misses n b n 11: assert(x > 0) IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 15/65 Simple dependency graph 1 z = z + 3; 2 if (z > 0) { 3 x = z + 1; 4 5 } else { 6 7 x = x * x - z; 8 } 9 10 11 assert(x > 0); z = 3 * x; y = z + 5; if (x > y) z = x - 1; 1: z = z + 3 2: if (z > 0) 3: x = z + 1 4: z = 3 * x 6: y = z + 5 7: x = x * x - z 9: if (x > y) 10: z = x - 1 11: assert(x > 0) r is data dependent on w if there exists a program execution where r reads a value from a memory that has been written by w w r n is control dependent on b if b is the closest point where the program may go some way that misses n b n 11: assert(x > 0) 1: z = z + 3 2: if (z > 0) 3: x = z + 1 7: x = x * x - z IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 16/65 Simple dependency graph 1 z = z + 3; 2 if (z > 0) { 3 x = z + 1; 4 5 } else { 6 7 x = x * x - z; 8 } 9 10 11 assert(x > 0); 1: z = z + 3 2: if (z > 0) 3: x = z + 1 4: z = 3 * x 6: y = z + 5 7: x = x * x - z 9: if (x > y) 10: z = x - 1 11: assert(x > 0) r is data dependent on w if there exists a program execution where r reads a value from a memory that has been written by w w r n is control dependent on b if b is the closest point where the program may go some way that misses n b n 11: assert(x > 0) 1: z = z + 3 2: if (z > 0) 3: x = z + 1 7: x = x * x - z IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 17/65 Points-to analysis aka pointer analysis Motivation How data dependencies look like? 1 int x; 2 int *p; 3 int *q; 4 x = 5; 5 p = &x; 6 q = p; 7 *q = 7; 8 assert(x > 6); IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 19/65 Motivation How data dependencies look like? 1 int x; 2 int *p; 3 int *q; 4 x = 5; 5 p = &x; 6 q = p; 7 *q = 7; 8 assert(x > 6); ... 4: x = 5 5: p = &x 6: q = p 7: *q = 7 8: assert(x > 6) IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 20/65 Motivation How data dependencies look like? 1 int x; 2 int *p; 3 int *q; 4 x = 5; 5 p = &x; 6 q = p; 7 *q = 7; 8 assert(x > 6); ... 4: x = 5 5: p = &x 6: q = p 7: *q = 7 8: assert(x > 6) where this data dependency edge starts? IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 21/65 Motivation How data dependencies look like? 1 int x; 2 int *p; 3 int *q; 4 x = 5; 5 p = &x; 6 q = p; 7 *q = 7; 8 assert(x > 6); ... 4: x = 5 5: p = &x 6: q = p 7: *q = 7 8: assert(x > 6) points-to analysis needed IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 22/65 Points-to analysis assigns to each pointer p the points-to set that contains all memory locations p may point to memory locations are abstractions of concrete objects located in memory during program execution often identified with allocation statements like 1: int x or 35: malloc(128) can represent more concrete objects, e.g., for malloc in cycle IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 23/65 Points-to analysis assigns to each pointer p the points-to set that contains all memory locations p may point to memory locations are abstractions of concrete objects located in memory during program execution often identified with allocation statements like 1: int x or 35: malloc(128) can represent more concrete objects, e.g., for malloc in cycle we use two additional memory locations null representing a pointer value NULL unknown saying that the pointer can point anywhere additionally, it tracks which memory locations represent one concrete memory object and which are abstract can be computed by an abstract interpretation IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 24/65 Points-to analysis can be flow sensitive or insensitive flow sensitive analysis assigns a points-to set to a pointer and a program location (more precise but more expensive) flow insensitive analysis used mainly for programs in static single assignment (SSA) form 1 int y; 2 int *data = malloc(40); 3 ... 4 int *p = &y; 5 if (y > 2) { 6 p = NULL; 7 } else { 8 p = data + 2; 9 } 10 int *q = p; IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 25/65 Points-to analysis can be flow sensitive or insensitive flow sensitive analysis assigns a points-to set to a pointer and a program location (more precise but more expensive) flow insensitive analysis used mainly for programs in static single assignment (SSA) form 1 int y; 2 int *data = malloc(40); 3 ... 4 int *p = &y; 5 if (y > 2) { 6 p = NULL; 7 } else { 8 p = data + 2; 9 } 10 int *q = p; flow sensitive IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 26/65 Points-to analysis can be flow sensitive or insensitive flow sensitive analysis assigns a points-to set to a pointer and a program location (more precise but more expensive) flow insensitive analysis used mainly for programs in static single assignment (SSA) form 1 int y; 2 int *data = malloc(40); 3 ... 4 int *p = &y; 5 if (y > 2) { 6 p = NULL; 7 } else { 8 p = data + 2; 9 } 10 int *q = p; flow sensitive p → {1: int y} IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 27/65 Points-to analysis can be flow sensitive or insensitive flow sensitive analysis assigns a points-to set to a pointer and a program location (more precise but more expensive) flow insensitive analysis used mainly for programs in static single assignment (SSA) form 1 int y; 2 int *data = malloc(40); 3 ... 4 int *p = &y; 5 if (y > 2) { 6 p = NULL; 7 } else { 8 p = data + 2; 9 } 10 int *q = p; flow sensitive p → {1: int y} p → {null} IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 28/65 Points-to analysis can be flow sensitive or insensitive flow sensitive analysis assigns a points-to set to a pointer and a program location (more precise but more expensive) flow insensitive analysis used mainly for programs in static single assignment (SSA) form 1 int y; 2 int *data = malloc(40); 3 ... 4 int *p = &y; 5 if (y > 2) { 6 p = NULL; 7 } else { 8 p = data + 2; 9 } 10 int *q = p; flow sensitive p → {1: int y} p → {null} p → {2: malloc(40)} IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 29/65 Points-to analysis can be flow sensitive or insensitive flow sensitive analysis assigns a points-to set to a pointer and a program location (more precise but more expensive) flow insensitive analysis used mainly for programs in static single assignment (SSA) form 1 int y; 2 int *data = malloc(40); 3 ... 4 int *p = &y; 5 if (y > 2) { 6 p = NULL; 7 } else { 8 p = data + 2; 9 } 10 int *q = p; flow sensitive p → {1: int y} p → {null} p → {2: malloc(40)} q → {null, 2: malloc(40)} IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 30/65 Points-to analysis can be flow sensitive or insensitive flow sensitive analysis assigns a points-to set to a pointer and a program location (more precise but more expensive) flow insensitive analysis used mainly for programs in static single assignment (SSA) form 1 int y; 2 int *data = malloc(40); 3 ... 4 int *p = &y; 5 if (y > 2) { 6 p = NULL; 7 } else { 8 p = data + 2; 9 } 10 int *q = p; flow sensitive p → {1: int y} p → {null} p → {2: malloc(40)} q → {null, 2: malloc(40)} flow insensitive IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 31/65 Points-to analysis can be flow sensitive or insensitive flow sensitive analysis assigns a points-to set to a pointer and a program location (more precise but more expensive) flow insensitive analysis used mainly for programs in static single assignment (SSA) form 1 int y; 2 int *data = malloc(40); 3 ... 4 int *p = &y; 5 if (y > 2) { 6 p = NULL; 7 } else { 8 p = data + 2; 9 } 10 int *q = p; flow sensitive p → {1: int y} p → {null} p → {2: malloc(40)} q → {null, 2: malloc(40)} flow insensitive p, q → {1: int y, null, 2: malloc(40)} IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 32/65 Points-to analysis can be flow sensitive or insensitive flow sensitive analysis assigns a points-to set to a pointer and a program location (more precise but more expensive) flow insensitive analysis used mainly for programs in static single assignment (SSA) form can be field insensitive or sensitive field sensitive analysis tracks also offsets field sensitive analysis is more precise but more expensive 1 int y; 2 int *data = malloc(40); 3 ... 4 int *p = &y; 5 if (y > 2) { 6 p = NULL; 7 } else { 8 p = data + 2; 9 } 10 int *q = p; flow sensitive p → {1: int y} p → {null} p → {2: malloc(40)} q → {null, 2: malloc(40)} flow insensitive p, q → {1: int y, null, 2: malloc(40)} field insensitive field insensitive IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 33/65 Points-to analysis can be flow sensitive or insensitive flow sensitive analysis assigns a points-to set to a pointer and a program location (more precise but more expensive) flow insensitive analysis used mainly for programs in static single assignment (SSA) form can be field insensitive or sensitive field sensitive analysis tracks also offsets field sensitive analysis is more precise but more expensive 1 int y; 2 int *data = malloc(40); 3 ... 4 int *p = &y; 5 if (y > 2) { 6 p = NULL; 7 } else { 8 p = data + 2; 9 } 10 int *q = p; flow sensitive p → {null} flow insensitive field sensitive field sensitive p → {(1: int y, 0)} p → {(2: malloc(40), 8)} q → {null, (2: malloc(40), 8)} p, q → {(1: int y, 0), null, (2: malloc(40), 8)} IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 34/65 Notes a popular algorithm for points-to analysis presented in L. O. Andersen: Program Analysis and Specialization for the C Programming Language, PhD thesis, 1994 applications of points-to analysis can prove that a program is memory safe, i.e., it contains no invalid pointer dereference and no invalid memory deallocation can be used for computation of data dependencies can help to identify functions called via a function pointer . . . IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 35/65 Static single assignment (SSA) Static single assignment (SSA) a program form with only one assignment statement for each variable the assignment statement can be evaluated repeatedly special instructions called ϕ-nodes added IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 37/65 Static single assignment (SSA) a program form with only one assignment statement for each variable the assignment statement can be evaluated repeatedly special instructions called ϕ-nodes added 1 x = input(); 2 z = x + 3; 3 if (z > 0) { 4 x = z + 1; 5 z = 3 * x; 6 } else { 7 z = z + 5; 8 } 9 10 11 z = z + x; IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 38/65 Static single assignment (SSA) a program form with only one assignment statement for each variable the assignment statement can be evaluated repeatedly special instructions called ϕ-nodes added 1 x = input(); 2 z = x + 3; 3 if (z > 0) { 4 x = z + 1; 5 z = 3 * x; 6 } else { 7 z = z + 5; 8 } 9 10 11 z = z + x; 1 x1 = input(); 2 z1 = x1 + 3; 3 if (z1 > 0) { 4 x2 = z1 + 1; 5 z2 = 3 * x2; 6 } else { 7 z3 = z1 + 5; 8 } 9 x3 = ϕ(x2,x1); 10 z4 = ϕ(z2,z3); 11 z5 = z4 + x3; IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 39/65 Applications of SSA simplifies static analysis without SSA, x may have different values in different locations with SSA, xi has the same value everywhere flow-insensitive analyses provide better results for programs in SSA used in many verification tools and also in compilers LLVM IR also uses SSA (sort of) IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 40/65 Data dependence Data dependence Consider a fixed control flow graph (CFG) with nodes V. We assume that for each node n ∈ V, we have sets: sdef(n) of memory locations that must be written by n wdef(n) of memory locations that may be written by n ref(n) of memory locations that may be read by n IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 42/65 Data dependence Consider a fixed control flow graph (CFG) with nodes V. We assume that for each node n ∈ V, we have sets: sdef(n) of memory locations that must be written by n wdef(n) of memory locations that may be written by n ref(n) of memory locations that may be read by n null, unknown ̸∈ sdef(n) and null ̸∈ wdef(n) ∪ ref(n) sdef(n) ⊆ wdef(n) sdef(n) contains only memory locations that represent one concrete object each time n is executed the sets can be computed by a field-sensitive points-to analysis IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 43/65 Data dependence Definition (data dependence) Let V be the set of nodes of a CFG. A node nr ∈ V is data dependent on a node nw ∈ V if there is a path nw = n1, n2, . . . , nk = nr in the CFG such that unknown ̸∈ wdef(nw ) ∪ ref(nr ) and wdef(nw ) ∩ ref(nr ) ̸⊆ 1= n) { 5 i++; 6 } 7 assert(false); IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 50/65 Motivation Which statements are irrelevant for the assert? 1 2 3 4 5 6 7 assert(false); 1 unsigned int i,n; 2 n = input(); 3 i = 0; 4 while (i >= n) { 5 i++; 6 } 7 assert(false); IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 51/65 Motivation Which statements are irrelevant for the assert? 1 2 3 4 5 6 7 assert(false); 1 unsigned int i,n; 2 n = input(); 3 i = 0; 4 while (i >= n) { 5 i++; 6 } 7 assert(false); removing a potentially non-terminating cycle can transform an unrechable code into a reachable line 7 on the right is unreachable if input() always returns 0 IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 52/65 Two notions of control dependence Intuitively, a statement n is control dependent on a statement b if b is the closest point where the program may go some way that misses n. IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 53/65 Two notions of control dependence Intuitively, a statement n is control dependent on a statement b if b is the closest point where the program may go some way that misses n. weak control dependence assumes that every execution is finite an instance: standard control dependence IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 54/65 Two notions of control dependence Intuitively, a statement n is control dependent on a statement b if b is the closest point where the program may go some way that misses n. weak control dependence assumes that every execution is finite an instance: standard control dependence strong control dependence sensitive to program non-termination: there can be a dependence between two statements if one can infinitely delay the execution of the other an instance: non-termination sensitive control dependence IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 55/65 Standard control dependence An exit-CFG is a CFG with a unique exit node that is reachable from every other node. IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 56/65 Standard control dependence An exit-CFG is a CFG with a unique exit node that is reachable from every other node. Definition (post-dominance) Given an exit-CFG, its node b post-dominates a node a if b is on every path from a to exit. If a ̸= b, we say that b strictly post-dominates a. IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 57/65 Standard control dependence An exit-CFG is a CFG with a unique exit node that is reachable from every other node. Definition (post-dominance) Given an exit-CFG, its node b post-dominates a node a if b is on every path from a to exit. If a ̸= b, we say that b strictly post-dominates a. Definition (standard control dependence) Given an exit-CFG, we say that node n is standard control dependent (SCD) on node b if 1 there exists a non-trivial path π from b to n with any node on π (excluding b) post-dominated by n and 2 b is not strictly post-dominated by n. IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 58/65 Standard control dependence 1 2 3 4 5 exit IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 59/65 Standard control dependence 1 2 3 4 5 exit the SCD relation for an exit-CFG (V, E) can be computed in time O(|E|) using the algorithm of J. Ferrante et al.: The Program Dependence Graph and Its Use in Optimization, TOPLAS 1987 each CFG can be transformed into an exit-CFG IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 60/65 Non-termination sensitive control dependence predicate nodes in CFG are nodes corresponding to branching statements maximal path is a path that cannot be further prolonged, i.e., it is infinite or it ends in a node without any successor IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 61/65 Non-termination sensitive control dependence predicate nodes in CFG are nodes corresponding to branching statements maximal path is a path that cannot be further prolonged, i.e., it is infinite or it ends in a node without any successor Definition (non-termination sensitive control dependence) Given a CFG, a node n is non-termination sensitive control dependent (NTSCD) on a predicate node p if p has two successors s1 and s2 such that 1 all maximal paths from s1 contain n and 2 there exists a maximal path from s2 that does not contain n. IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 62/65 Non-termination sensitive control dependence 1 2 3 4 5 exit IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 63/65 Non-termination sensitive control dependence 1 2 3 4 5 exit the NTSCD relation for a CFG (V, E) can be computed in time O(|V|2) using the algorithm of M. Chalupa et al.: Fast Computation of Strong Control Dependencies, CAV 2021 NTSCD treats every program cycle as potentialy non-terminating IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 64/65 Notes we used program dependence graphs for programs without procedure calls there are also system dependence graphs for programs with procedure calls both NTSCD and SCD have applications in program slicing for software verification: SCD leads to smaller sliced programs and can only lead to produce false alarms, but not to false negatives there are other notions of control dependence, e.g., decisive order dependence (DOD) points-to analysis and slicer for LLVM implemented in DG https://github.com/mchalupa/dg IA159 Formal Methods for Software Analysis: Program Slicing and Points-to Analysis 65/65