Examples in Program Analysis (Solution I)

1 Dangling Else
1.1 Solution
1.2 Further Questions
1.3 Output files
2 Switch Case Labels
2.1 Solution
2.2 Further Questions
2.3 Output files
3 Loop Enumeration
3.1 Solution
3.2 Further Questions
3.3 Output files

1 Dangling Else

The else part of if statements is optional. Nested if statements like the following are errorprone:
dangling.in[1]==
{   
  int i, z;
  i = read();
  if (i>=0)
  if (i<10) z = 5+i;
  else      z = 0;
  print (z);
}
This macro is attached to an output file.
C defines that the else belongs to the inner if (i<10). The programmer might have intended to associate it to the outer if (i>=0). Hence the style guide requires to avoid such situations, e.g. by additional curly braces. Your analysis tool shall emit a warning if such a dangling else occurs:
dangling.out[2]==
"dangling.in", line 5:3 WARNING: beware of dangling else!
This macro is attached to an output file.
The following questions may help to focus your attention on the significant aspects of this problem:

1. Which are the adjacent tree contexts that will cause the warning?

2. In which context is the warning issued, and what is its precondition?

1.1 Solution

A warning is issued if the Stmt subtree of a one-sided if statement is a two-sided if statement. In order to produce the warning in the lower context we associate an attribute WarnSingleIf to Stmt. It indicates whether this Stmt occurs immediately below a one-sided if context. There it is set to 1. In all other contexts where Stmt occurs on the righthand side it is set to 0.

Using a default SYMBOL computation for Stmt avoids to take care of any other Stmt context. It is overridden by the RULE computation in the one-sided if context.

dangling else computations[3]==
ATTR WarnSingleIf: int;

SYMBOL Stmt COMPUTE INH.WarnSingleIf = 0; END;

RULE: Stmt ::= 'if' '(' Expr ')' Stmt COMPUTE
  Stmt[2].WarnSingleIf = 1;
END;

RULE: Stmt ::= 'if' '(' Expr ')' Stmt 'else' Stmt COMPUTE
  IF (Stmt[1].WarnSingleIf,
  message (WARNING, "beware of dangling else!", 0, COORDREF));
END;
This macro is invoked in definition 4.

1.2 Further Questions

1. Did you get messages on missing computations? If so, explain why.

2. Reconsider your solution when you have learned about SYMBOL computations. How can you use them to simplify your solution?

1.3 Output files

dangling.lido[4]==
dangling else computations[3]
This macro is attached to an output file.

2 Switch Case Labels

Switch statements sometimes span over a wide range of case label values, and only a few case labels are stated for the non-default cases. A poor C compiler might then produce a large jump table with only a few non-default entries. Hence the style guide requires not to waste storage by sparse switch cases.

You decide to suggest to your manager that this requirement should be removed, because today's C compiler automatically translate sparse switch cases into cascades of conditional jumps.

In order to strengthen your argument by figures, your analysis tool will compute the number of the case labels in a switch statement and the range of their values.

For a program like

switch.in[5]==
{ int i, z;
  i = read();
  switch (i)
  {
   case 0:   z = 1;
             break;
   case 99:
   case 100: z = 2;
             break;
   default:  z = 0;
  }
  print (z);
}
This macro is attached to an output file.
the tool will produce the output:
switch.out[6]==
switch in line 3 has 3 case labels in the range 0 to 100
This macro is attached to an output file.
The following questions may help to focus your attention on the significant aspects of this problem:

1. How do you access the case label values from the switch statement context?

2. Which functions do you need to combine the values?

3. How do you handle nested switch statements?

2.1 Solution

For each SwStmt the number of its CaseLit occurrences and their smalles and largest value are computed by three CONSTITUENTS constructs, each combining the CaseLit values by an appropriate triple of functions: ADD, ARGTOONE, ZERO or MIN, IDENTICAL, f_INT_MAX or MAX, IDENTICAL, f_INT_MIN.

The functions f2, f1, f0 are chosen such that f1 yields the appropriate value of a single item, and for any x the equation f2 (x, f0()) = x holds.

The first CONSTITUENTS doesn't use the values of CaseLit.Sym at all for counting, since ARGTOONE is a constant (unary!) function, that yields 1 for any argument. f_INT_MAX and f_INT_MIN are constant functions that yield the largest repectively the smallest int value.

In case of nested switch statements the CONSTITUENTS do not access CaseLit occurrences of inner switch statements. This fact could be made explicit by using

CONSTITUENTS CaseLit.Sym SHIELD (SwStmt) WITH ...

The SYMBOL computation for CaseLit acesses the value of the terminal Number.

Switch case label computation[7]==
ATTR Sym: int;

SYMBOL SwStmt COMPUTE
  printf ("switch in line %d has %d case labels in the range %d to %d\n",
        LINE,
        CONSTITUENTS CaseLit.Sym WITH (int, ADD, ARGTOONE, ZERO),
        CONSTITUENTS CaseLit.Sym WITH (int, MIN, IDENTICAL, f_INT_MAX),
        CONSTITUENTS CaseLit.Sym WITH (int, MAX, IDENTICAL, f_INT_MIN));
END;

SYMBOL CaseLit COMPUTE SYNT.Sym = TERM; END;
This macro is invoked in definition 9.
ADD, ZERO, ARGTOONE, and IDENTICAL are predefined macros in LIDO. The other functions are supplied by the following cpp macros:
Cpp macro definitions[8]==
#include <limits.h>
#define MIN(x,y)        ((x)<=(y) ? (x) : (y))
#define MAX(x,y)        ((x)>=(y) ? (x) : (y))
#define f_INT_MIN()     INT_MIN
#define f_INT_MAX()     INT_MAX
This macro is invoked in definition 10.

2.2 Further Questions

1. Does your solution work for nested switch statements? Explain why.

2. Explain why the f0 functions are needed (look at the grammar).

3. Can you make any assumption about the order in which the functions are called?

4. Reconsider your solution when you have learned about SYMBOL computations. How can you use them to simplify your solution?

2.3 Output files

switch.lido[9]==
Switch case label computation[7]
This macro is attached to an output file.
switch.head[10]==
Cpp macro definitions[8]
This macro is attached to an output file.

3 Loop Enumeration

The program analyzer shall derive information about for loops in the program: The loops are counted from left to right throughout the program. For each loop its number, its nesting depth, and its line number is to be printed.

For example the following program

loops.in[11]==
{
  int i, k, j, s;
  s = 0;
  for (i=1; i<10; i=i+1)
    for (j=i; j<10; j=j+1)
      s = s + j;
  for (k=0; k<5; k=k+2)
    s = s - k;
  print (s);
}
This macro is attached to an output file.
shall produce output like
loops.out[12]==
for loop number 1 in line 4 has depth 1
for loop number 2 in line 5 has depth 2
for loop number 3 in line 7 has depth 1
This macro is attached to an output file.
The following questions may help to focus your attention on the significant aspects of this problem:

What is the computational pattern for left-to-right enumeration? In which context and with which value do you start the enumeration?

What is the computational pattern for nesting depth? How is the recursive nesting being founded?

3.1 Solution

A chain is used to propagate the loop numbers left-to-right through the program. The chain is started in the root context with the number of the first loop. Each for loop increments the incoming chain value and passes it down (HEAD).
Loop enumeration[13]==
CHAIN LoopNo: int;

SYMBOL Prog COMPUTE
  CHAINSTART HEAD.LoopNo = 1;
END;

SYMBOL ForStmt COMPUTE
  HEAD.LoopNo = ADD (THIS.LoopNo, 1);
END;
This macro is invoked in definition 16.
We use an INCLUDING construct to access the nesting depth of the next outer loop. The recursion is founded at the root symbol.
Loop nesting depth[14]==
ATTR LoopDepth: int;

SYMBOL Prog COMPUTE
  SYNT.LoopDepth = 0;
END;

SYMBOL ForStmt COMPUTE
  SYNT.LoopDepth =
    ADD (1, INCLUDING (ForStmt.LoopDepth, Prog.LoopDepth));
END;
This macro is invoked in definition 16.
In the ForStmt context the incoming chain value and the LoopDepth attribute is printed:
Loop information[15]==
SYMBOL ForStmt COMPUTE
  printf ("for loop number %d in line %d has depth %d\n",
          THIS.LoopNo, LINE, THIS.LoopDepth);
END;
This macro is invoked in definition 16.

3.2 Further Questions

Reconsider your solution when you have learned about SYMBOL computations. Which of the computations can be turned into SYMBOL computations? Explain why.

3.3 Output files

loops.lido[16]==
Loop enumeration[13]
Loop nesting depth[14]
Loop information[15]
This macro is attached to an output file.