Enrico Oliosi wrote:

Dear Ppl group, I finished my parser using the Ppl Lib and my last work has been the while statement. I read about widening operator in your user's manual (page 9) and I read that there are some differences between your operator and Halbwachs one. I would like to know if you will implement this operator in next version of the Ppl Lib or if there exists a way to approximate the Halbwachs operator (now I introduce a token which terminates the cicle after 10 iterations).

Dear Enrico,

I assume you are working with PPL 0.5, and that by "[our] operator" you mean the BHRZ03 widening. If so, notice that the widening proposed in the PhD thesis of Nicholas Halbwachs (which is a refinement of the one proposed by Patrick Cousot and Halbwachs himself in their POPL'78 paper) is already present in the version of the library you have, where it is called H79. So implementation of the Cousot & Halbwachs widening and extrapolation operators are provided by methods

void H79_widening_assign(const Polyhedron& y, unsigned* tp = 0); void limited_H79_extrapolation_assign(const Polyhedron& y, const ConSys& cs, unsigned* tp = 0); void bounded_H79_extrapolation_assign(const Polyhedron& y, const ConSys& cs, unsigned* tp = 0);

whereas our improved versions (improved because on a single application we get a result that is never worse) are made available by the methods

void BHRZ03_widening_assign(const Polyhedron& y, unsigned* tp = 0); void limited_BHRZ03_extrapolation_assign(const Polyhedron& y, const ConSys& cs, unsigned* tp = 0);

void bounded_BHRZ03_extrapolation_assign(const Polyhedron& y, const ConSys& cs, unsigned* tp = 0);

Please, do not hesitate to come back to us if I have misunderstood your question.

I want to thank all you for your help which was very important for me and for my thesis.

Glad to be useful.

Your group will be cited in the thanks of my thesis.

Thanks! When your thesis is finished, please do not forget to send us an electronic copy. As soon as we know more about the work you have been doing, we would like to list it in our credits' page at http://www.cs.unipr.it/ppl/Credits/ All the best,

Roberto

P.S. We will be releasing PPL 0.6 in a couple of days. If you are not subscribed already, please subscribe to the (strictly moderated) PPL-announce mailing list to get the announcement. This can be easily done at http://www.cs.unipr.it/mailman/listinfo/ppl-announce

Enrico Oliosi wrote:

yes I use PPL 0.5. I used exactly H79 widening operator, I have, i.e., two polyhedra:

ph1 : -A - 2*B >= -6, B >= 0, A - 2*B >= 2.

ph2: -A - 2*B >= -10, B >= 0, A - 2*B >= 2.

if I call the function ph1.H79_widening_assign(ph2) the result is -A - 2*B >= -6, B >= 0, A - 2*B >= 2

which is the first one (ph1). In the Cousot & Halbwachs's article the same example gives a different result: B >= 0, A - 2*B >= 2

Maybe I wrong something when I invoke these functions.

Dear Enrico,

you are calling H79_widening_assign() with the arguments reversed. If you look at the documentation, in fact, you will see that an invocation of the form

x.H79_widening_assign(y)

is valid only if y is contained in x. In your example, you have that ph2 is not contained in ph1, but the other way around. So what you want is

ph2.H79_widening_assign(ph1)

and the result, in ph2, will be what you expect. Actually, applying the widening by Cousot and Halbwachs to polyhedra that do not satisfy the required inclusion property is a very common mistake (but don't tell this anyone!).

In order to detect this kind of mistakes, let me suggest you to configure the PPL with the `--enable-assertions' while you are still debugging your application. Your program will be (much) slower, but you will detect bugs in your code (or perhaps in the PPL itself) more quickly. Later, when you will require more speed you can reconfigure the library without the `--enable-assertions' option and recompile. I hope this helps: let us know how it goes. Cheers,

Roberto

Enrico Oliosi wrote:

I have a last question: when I define my variables in my toy language and print the constraints the library print their dimensions and not the variables. I.e.:

myvar := 1 becomes A = 1

I tried to replace the dimension with var-names but I couldn't do it. Is there a way to do it or I can only print the dimensions?

Dear Enrico,

I believe you are confusing the variables in your program, with dimensions, variables and their printed names in the PPL.

Let me try to explain.

A dimension in the PPL is simply an unsigned integer.

A PPL variable is given by an object of type Variable that essentially corresponds to a dimension. The class Variable in the PPL is there only to help with good software engineering practices. To summarize, if you write

Variable x(1);

then `x' is a C++ variable of type `Variable' that corresponds to the dimension numbered 1 (i.e., the second dimension, as dimensions are numbered starting from 0). If you then write

cout << x;

the output will be "B" because the default output function will print "A" for a (any) variable corresponding to dimension 0, "B" for a (any) variable corresponding to dimension 1, then "C", ..., "Z", "A1", "B1", ..., "Z1", "A2", ...

If you don't like this output function you can change it. See the documentation and the source file `writevariable1.cc' in the `tests' subdirectories for the exact details and examples.

The let us come to your example. If I understand correctly, you have written a static analyzer that reads a program containing the statement

myvar := 1

Presumably you associate this variable instance in the analyzed program with dimensions 0 of some polyhedron. When you print the constraint(s) corresponding to the program point just after the assignment, you obtain

A = 1

that, in the light of the explanation above, should now be unsurprising.

If you want

myvar = 1

to be printed instead, then you should be able to reverse the process whereby you associated a variable named "myvar" in your program to dimension 0 of the polyhedron corresponding to that program point. Then you can set the output function for Variable (see the documentation of Variable::set_output_function()) so as to obtain what you want. Alternatively, you may even not use the PPL output operator and build yours, even though this is probably not worth the effort in your case. All the best,

Roberto