The syntox command invokes an "abstract debugger" used to determine the run-time value range of scalar and real variables of Pascal programs. This debugger is interprocedural (information is propagated along procedure calls) and performs forward and backward analyses (information is back-propagated from the end to the beginning of the program).
Invariant assertions, such as {% x > 0 %}, can be inserted in the source code to enforce conditions on the run-time values of the program's variables. The debugger will determine necessary conditions for the program to satisfy these assertions without exiting on a run-time error. So for instance, inserting {% false %} at a given control point will determine necessary conditions for the program not to reach this point. In particular, insterting {% false %} at the end of the program will determine necessary conditions for the program to diverge.
Similarly, intermittent assertions, such as {% x = 0 ? %} can be inserted at a given control point of the source code to determine necessary conditions for the program to reach this point and satisfy the specified condition. It is thus possible to determine necessary conditions for the program to terminate by inserting the intermittent assertion {% true ? %} at the end of the program. Note that the intermittent assertion {% false ? %} will determine the condition "false" (there's no way for a program to reach a control point and to satisfy "false").
Moreover, invariant and intermittent assertions can be freely mixed to answer questions such as "are there conditions for the program to reach this point without going through this point while satisfying this condition at this other point".
Finally, bear in mind that the conditions determined by syntox are only necessary. In particular, syntox will never prove termination, but only non-termination (since the negation of a necessary condition is a sufficient condition).
This analyser is a research prototype and a test-bed for new ideas, and is not fully implemented yet. In particular, pointers, records and arrays are accepted, but they are not always handled correctly. Only standard procedures and functions (readln, writeln, trunc...) are supported, and procedure parameters are not allowed. The with construct and variant records are not recognized. However, programs with only scalar variables, procedures with "value" or "var" parameters, and local or non-local "gotos" should be handled correctly.
The following options are processed by the syntox command itself:
Program Names;
var x : integer;
procedure foo(y : integer);
procedure bar(z : integer);
begin ... end;
begin ... end;
begin ... end.
This interface has an edit window, where you can either read an existing Pascal program or directly type small programs. After clicking on the "Analyze" button, you simply click on a line and get a window displaying the values of the accessible variables.
If you click on any of these variables, you get a popup window showing, for each procedure activation, the location bound to this variable by the environment, and the value of this location.
syntox displays the value of pseudo-variables used as temporaries for the evaluation of complex expressions with function calls. These variables are named: $1, $2 ...etc. As an example, the following statement:
would be expanded to:
Invariant assertion of the form {% x <> 0 %} and intermittent assertions of the form {% x <> 0 ? %} can be inserted BEFORE every instruction. As an example, consider the following program, computing MacCarthy's 91-function:
Program MacCarthy;
var m, n : integer;
function MacCarthy(n : integer) : integer;
begin
if n > 100 then
MacCarthy := n - 10
else
MacCarthy := MacCarthy(MacCarthy(n + 11))
end;
begin
{1}
m := MacCarthy(n);
{2}
end.
This function is well known to be equal to n-10 if n > 100 and to 91
otherwise. If no assertion is inserted, syntox will prove that m is in
[91..hi-10] at control point {2}. However, if the intermittent assertion:
{% m = 91 ? %}
is inserted at control point {2}, then syntox will show that it n must be in the range [lo..101] at control point {1} to insure that the result m equals 91 at control point {2} as stated in the assertion. Similarly, if the intermittent assertion:
{% m <> 91 ? %}
is inserted at control point {2}, then syntox will prove that n must be greater or equal to 102. Combining the two results, it has been shown that if "n <= 101" then either the program loops or else it terminates with "m=91".
The information given by syntox has one of the following forms :
"not reached" <variable> <lb> <value> <ub> <set> <variable> top <set> <variable> <lb> [<min>..<max>] <ub> <set><lb> and <ub> can either by empty or equal to `*'. If <lb> equals `*', it is a warning to the programmer : a test on the lower bound should be inserted in the Pascal code to insure that the program will not crash and will satisfy the programmer's assertions. Differently stated, if the assertion on the lower bound is not satisfied at run time, then the program will either crash or will fail to satisfy some assertions. A similar rule applies to the upper bound <ub>.
If <set> equals to `?', than the identifier was not set, and calculations were possibly performed on his value. If a variable is not set, then its value is `top?', which is a shorthand for `[lo..hi]?'.
If <set> equals to `(?)', than the value is the result of a join between an unset value and a `regular' range.
Information on arrays has a slightly different semantics : when none of its elements have been assigned, an array has value `top ?'. But if at least one of its elements has been assigned, then the range is `[min..max]' meaning that every element that has been assigned is between `min' and `max' whereas the others have undefined values. As an example, the information given by syntox at control point {1} for MacCarthy's program is:
n in *[lo..101]?
Finally, the meaning of "not reached" at a given control point is that this control point can never be reached. For instance, the following program never terminates:
program Loop;
var x : integer;
begin
{1} x := 1;
while x > 0 do
x := x + 1;
{% true? %}
{2} end.
In such a case,
syntox
sets every control point to "not reached", to show that this program
never
terminates correctly.
The method used to deal with aliases uses so called `pseudo-locations'. A pseudo-location is basically the set of identifiers bound to that location by the environment in a given procedure activation. Pseudo-locations are used as call-by-value-result parameters. Consider for instance the following program:
Program Aliases;
var x, y : integer;
procedure P1(var i1, j1 : integer);
begin
...
end;
procedure P2(var i2:integer);
procedure P3(var i3:integer);
var x3 : integer;
begin
P1(x3, i3);
P1(i2, i3);
end;
begin
P3(i2);
end;
begin
x := 0;
P2(y);
end.
It can be shown that procedure P1 is called with the alias sets:
{x} {i1, j1, y}
{x} {i1} {j1, y}
In the latter case, we have one pseudo-location {i1}. The set {j1, y} is
not
a pseudo-location for `y' is a global variable, and therefore `j1' is a
pure lexical alias of `y'. Moreover, the pseudo-location {i1} is an alias of
the `hidden' location {x3} of procedure P3. This is displayed by
syntox
as : {i1} -> x3.
Similarly, procedure P2 is called with the single alias set:
{x} {i2, y}
Procedure P3 is called with the single alias set:
{x} {i2, i3, y} {x3}
Possibly many!
Name: Francois Bourdoncle Organization: Ecole des Mines de Paris Email: Francois.Bourdoncle@ensmp.fr