October 30, 2003
CPSC 410: Verification and Validation Data-flow Approaches • By the end of this lecture, you will be able to: • Perform various data-flow analyses by hand • Describe how such analyses can aid verification activities • Generate test cases that satisfy various data-flow coverage criteria for a given routine
Other Questions We’d Like to Answer • There are many other useful questions we can ask about source code: • Is this variable used before it is defined? • Is this variable defined more than once before being used? • Is this code reachable?
• Compilers often perform these checks
October 30, 2003
3
© 2003, G. Murphy. All rights reserved.
Static Analysis
Data-flow Analysis
• Verification is often associated with dynamic analysis (i.e., testing) • One difficulty with dynamic analysis is choosing appropriate inputs • Static analysis approaches can help us find anomalies by analyzing, not executing, an artifact • Call graphs are one kind of static analysis
• We cannot answer these questions with control-flow information alone • We need to understand how data propagates through the system, called data-flow analysis • Essentially, we want to understand where variables are defined and where they are used • We are going to look at this in terms of nonOO (Cish) code to make it simpler
• What kind of “anomaly” can a call graph help find?
• What is another form of static analysis you are all used to using in Java, C++, etc.? October 30, 2003
2
C P S C 410 © 2 0 0 3 , G. M u r p h y. All rights reserved.
© 2003, G. Murphy. All rights reserved.
October 30, 2003
4
© 2003, G. Murphy. All rights reserved.
1
October 30, 2003
Data-flow Analysis: The Basic Idea
Reaching Definitions
• 1: void foo() { 2: int i = 2; 3: int j; 4: if ( i > 2 ) 5: j = i+1; 6: else 7: j = i - 1; 8: printf( “%d”, j ); 9: }
• 1: void foo() { 2: int i = 2; 3: int j; 4: if ( i > 2 ) 5: j = i+1; 6: else 7: j = i - 1; 8: printf( “%d”, j ); 9: }
Uses should be carried forward, just Defs: {(2,i)} no room!
Defs: {(2,i)} Uses: {(4, i)} Defs: {(2,i),(5,j)} Uses: {(5,i)} Defs: {(2,i),(7,j)} Uses: {(7,i)} Defs: {(2,i),(5,j),(7,j) Uses: {(8,j)}
At Line 8, where is j possibly defined? October 30, 2003
Line 55 or Line 7
© 2003, G. Murphy. All rights reserved.
Data-flow Analysis Requires Control-flow Graph
Formalizing It • Let’s consider the reaching definitions problem (i.e., previous slide) • The idea with reaching definitions is to find out what definitions may reach a particular use • At each statement of the program, we want to evaluate: • OUT(S) = GEN(S) ∪ ( IN(S) - KILL (S) )
• To perform data-flow analysis, we need the control-flow graph S: 2,3
We must always make the conservative choice.
S: 4 t
6
C P S C 410 © 2 0 0 3 , G. M u r p h y. All rights reserved.
© 2003, G. Murphy. All rights reserved.
S: 5 Call this S1t IN(S1t) = OUT(S1) October 30, 2003
Call this S1 f S: 7
S: 8 October 30, 2003
© 2003, G. Murphy. All rights reserved.
7
October 30, 2003
8
Call this S1f IN(S1f) = OUT(S1)
Call this S2 G. Murphy. IN(S2) = OUT(S1t©) 2003, merge All rights reserved. OUT(S1f)
2
October 30, 2003
Another Example
Live Variables
• void foo() { int i = 10; int j=0; while ( j < i ) { j = j + 1; } printf(“%d”, j); }
• Live variables are when a variable is assigned some value but then the variable is not used in any later computation
October 30, 2003
What are the values of OUT for each statement if we are calculating reaching definitions? Hint: With loops, we keep merging iterating until OUT does not change any longer.
9
© 2003, G. Murphy. All rights reserved.
x = a; … code where x is never used x = b; • Maybe the first assignment is a mistake October 30, 2003
11
© 2003, G. Murphy. All rights reserved.
Use Before Def
Data-flow Testing Criteria
• How can we use the reaching definitions to determine if a variable is used before it is defined?
• Basic idea: Ensure the definitions of variables and their subsequent use is tested • Based on a definition-use (def/use) graph
• Compute reaching definitions • Visit each statement and see if there is a use without a reaching definition
October 30, 2003
10
C P S C 410 © 2 0 0 3 , G. M u r p h y. All rights reserved.
© 2003, G. Murphy. All rights reserved.
• Essentially, compute reaching definitions and then form links from uses to potential defs
• Distinguish two forms of use: • c-use: computational use of a variable • p-use: predicate use of a variable (involves control transfer)
October 30, 2003
12
© 2003, G. Murphy. All rights reserved.
3
October 30, 2003
Def/Use Graph • 1: void foo() { 2: int i = 2; 3: int j; 4: if ( i <= 2 ) 5: j = i+1; 6: else 7: j = i - 1; C-use of i 8: printf( “%d”, j ); 9: }
Example of All-Defs 2: i=2 P-use of i f
4: i <= 2 t 5: j=i+1
7: j=i-1 C-use of i 8: print j C-use of j
October 30, 2003
13
© 2003, G. Murphy. All rights reserved.
• 1: void foo(int i) { 2: int j; 3: if ( i > 2 ) 4: j = i+1; 5: else 6: j = i - 1; C-use of i 7: printf( “%d”, j ); 8: }
1: i as parm
4: i > 2 t 5: j=i+1
{ (i=1),(i=3) }
7: j=i-1 C-use of i 8: print j
What test cases would satisfy all-defs? October 30, 2003
P-use of i f
C-use of j 15
© 2003, G. Murphy. All rights reserved.
Data-flow Testing Criteria: All-defs
Example: Determine Test Cases That Provide All-Defs
• Let P be a set of complete paths of the def/use graph (i.e., a complete path represents a complete execution of the program) • P satisfies the all-defs criterion if for the def of every variable, one of its uses (either c-use or p-use) is included on a path • What is the net effect?
void doit(int i, int j, int k) { i = j + 1; while ( i < k ) { if ( i % 2 ) i = k – 2; else i = k – 1; i++; } }
• Make sure a use of every def is checked October 30, 2003
14
C P S C 410 © 2 0 0 3 , G. M u r p h y. All rights reserved.
© 2003, G. Murphy. All rights reserved.
October 30, 2003
Does your test case also satisfy all-uses?
16
© 2003, G. Murphy. All rights reserved.
4
October 30, 2003
Some Other Criterion
Another Example
• All-P-Uses:
void sort(int a[], int length) { • What is the CFG? for (int i = 0; i < length; i++ ) { • Test cases for: • branch coverage for (int j = 0; j < length-1; j++) { • all-defs coverage if ( a[j] > a[j+1] ) { • all-uses coverage int tmp = a[j]; a[j] = a[j+1]; a[j+1] = tmp; } } } © 2003, G. Murphy. 19 } 30, 2003 October All rights reserved.
All-paths (path coverage)
• Test all the p-uses of all the definitions
All-uses
• All-Uses: • All p-uses and all c-uses of a definition must be exercised.
All-c-uses/ All-p-uses/ Some p-uses Some c-uses All-defs
All-p-uses
All-edges (branch coverage)
October 30, 2003
© 2003, G. Murphy. All-nodes (statement coverage) 17
All rights reserved.
Data-flow Analysis Example
Summary
• scanf(x,y); if ( y < 0 ) pow = 0 - y; else pow = y; z = 1.0; while ( pow != 0 ) { z = z * x; pow = pow - 1; } if ( y < 0 ) z = 1.0/z printf (z);
• Described how to do data-flow analysis
October 30, 2003
• What is the CFG? • Test cases for: • branch coverage • all-defs coverage • all-uses coverage
18
C P S C 410 © 2 0 0 3 , G. M u r p h y. All rights reserved.
© 2003, G. Murphy. All rights reserved.
• Reaching definitions • Live variable analysis
• Described testing criteria based on data-flow
October 30, 2003
20
© 2003, G. Murphy. All rights reserved.
5