September 2004 - PPL-devel - BUGSENG Mailman

w3ppl/htdocs/Bugs Makefile
by Roberto Bagnara 13 Sep '04

13 Sep '04

CVSROOT: /cvs/ppl Module name: w3ppl Changes by: roberto(a)cs.unipr.it 2004-09-13 12:03:24 Modified files: htdocs/Bugs : Makefile Log message: Install all patches. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/Bugs/Makefile.diff?c…

1 0

w3ppl/htdocs/Bugs patch_ppl-0-6-1_ppl-20040808
by Roberto Bagnara 13 Sep '04

13 Sep '04

CVSROOT: /cvs/ppl Module name: w3ppl Changes by: roberto(a)cs.unipr.it 2004-09-13 12:00:17 Added files: htdocs/Bugs : patch_ppl-0-6-1_ppl-20040808 Log message: Patch for PPL 0.6.1 that fixes a bug in GenSys::satisfied_by_all_generators(). Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/Bugs/patch_ppl-0-6-1…

1 0

Re: Fixpoint + Widening in PPL
by J. Nunez Fontarnau 13 Sep '04

13 Sep '04

This is the code I am using to obtain a fixpoint for append. Note that no widening is applied: so far the code is aimed at producing a (possibly) infinite 'iteration'. Though so it does, the polyhedra produced are always the same. Note also that a query to 'fixpoint' will terminate in the base case. (?) Only by changing the order of occurrence of the inductive and base 'fixpoint' clauses, infinite recursive calls are obtained. Please help. Javier % Iteration to Post-Fixpoint for Append. %verbosity(0). verbosity(1). wappend :- % Base case make_vars(6, [A, B, C, D, E, F]), ppl_new_Polyhedron_from_dimension(c, 6, Base), ppl_Polyhedron_add_constraints(Base, [A = 0, B >= 0, C = B]), ppl_Polyhedron_get_constraints(Base, BConstr), display_message(['Base constraints ...']), display_message(BConstr), % Inductive case ppl_new_Polyhedron_from_dimension(c, 6, Induc), ppl_Polyhedron_add_constraints(Induc, [A + F = C + D, B = E, C + D >= A, D >= 0, B >= 0, A >= D + 1]), ppl_Polyhedron_get_constraints(Induc, IConstr), display_message(['Inductive constraints ...']), display_message(IConstr), % Empty polyhedron ppl_new_Polyhedron_empty_from_dimension(c, 6, Empty), display_message(['Querying fixpoint/4 ...']), fixpoint(Induc, Empty, Base, Fixpoint), ppl_Polyhedron_get_constraints(Fixpoint, FConstr), display_message(['Post-Fixpoint ...']), display_message(FConstr), display_message(['Deleting Base ...']), ppl_delete_Polyhedron(Base), display_message(['Deleting Induc ...']), ppl_delete_Polyhedron(Induc), display_message(['Deleting Empty ...']), ppl_delete_Polyhedron(Empty). %%%%%%%%%%%%%%%%%%%%%%%%%%% % Post-fixpoint calculation % Base case fixpoint(_, Previous, Current, Fixpoint) :- ppl_Polyhedron_contains_Polyhedron(Current, Previous), ppl_Polyhedron_get_constraints(Current, FCurrent), display_message(['Base case: Current ...']), display_message(FCurrent), ppl_Polyhedron_get_constraints(Previous, FPrevious), display_message(['Base case: Previous ...']), display_message(FPrevious), ppl_new_Polyhedron_from_Polyhedron(c, Current, c, Fixpoint), !. % Inductive case fixpoint(Induc, Previous, Current, Fixpoint) :- ppl_delete_Polyhedron(Previous), ppl_new_Polyhedron_from_Polyhedron(c, Current, c, Current1), ppl_Polyhedron_get_constraints(Current1, FCurrent1), display_message(['Inductive case: Current 1 ...']), display_message(FCurrent1), ppl_Polyhedron_get_constraints(Induc, FInduc), display_message(['Inductive case: Induc ...']), display_message(FInduc), % computations over current1 ppl_Polyhedron_poly_hull_assign(Current1, Induc), ppl_Polyhedron_get_constraints(Current1, FCurrent1a), display_message(['Current 1 after convex hull ...']), display_message(FCurrent1a), ppl_Polyhedron_get_constraints(CS_P, Current1), ppl_Polyhedra_get_constraints(CS_Q, Induc), widen_extrapolation_init(P, CS_P, Topology), widen_extrapolation_init(Q, CS_Q, Topology), ppl_Polyhedron_H79_widening_assign(P, Q), display_message(['Recursive query to fixpoint ...']), fixpoint(Induc, Current, Current1, Fixpoint). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % make_var_list(+I,+Dimension,?VariableList) % constructs a list of variables with indices from I to Dimension - 1. % It is assumed that I =< Dimension. make_vars(Dim, VarList):- make_var_list(0, Dim, VarList). make_var_list(Dim,Dim,[]):- !. make_var_list(I,Dim,['$VAR'(I)|VarList]):- I1 is I + 1, make_var_list(I1,Dim,VarList). %%%%%%%%%%%%%%%%%% % Output messages. display_message(Message):- verbosity(1), !, nl, write_all(Message), nl. display_message(_). write_all([]). write_all([Phrase|Phrases]):- write(Phrase), write(' '), write_all(Phrases). > On Tue, 7 Sep 2004 10:10:06 +0100 (BST), P M Hill wrote > > Hi Javier, > > > > Have a look in ppl/interfaces/Prolog/pl_check.pl > > > > There are tests for the ppl Prolog widening predicates > > such as ppl_Polyhedron_H79_widening_assign/2. > > > > I have written some longer code that uses the widening to ensure > > convergence in some analysis but it will not be in the ppl sources. > > > > I'll see if I can find it. > > > > Pat > > On Tue, 7 Sep 2004, Enea Zaffanella wrote: > > > > > J. Nunez Fontarnau wrote: > > > > Hi Enea > > > > How are you ? > > > > > > > > I need to ask you about fixpoint calculations and widenings in PPL. As > you are > > > > the expertise in all the implementation stuff, I would like to ask > whether there > > > > is any examples on fixpoint calculation with PPL and widening for > Prolog (not > > > > C++). I've noticed a file append?.cc that calculates the fixpoint for > append. I > > > > am trying to rewrite it in Prolog, but I am a bit lost with > the 'reassignment' > > > > of polyhedra 'Previous' and 'Current' > > > > > > > > Any suggestions on how to implement this in Prolog would be very much > > > > appreciated. > > > > > > > > Thanks, > > > > Javier > > > > > > Dear Javier, > > > > > > I am not sure I have understood your question. > > > As I see it, you are going in the wrong direction, since it seems that > > > you want to repeat the iterative control flow of append*.cc into your > > > Prolog program, whereas I would suggest to go for a more canonical > > > recursive solution. > > > > > > Namely, your solution sould be something similar to the following > pattern: > > > > > > %% base case > > > upward_iteration_sequence(Previous, Current, Inductive, Current) :- > > > ppl_Polyhedron_contains_Polyhedron(Previous, Current), > > > !. > > > > > > %% inductive case. > > > upward_iteration_sequence(Previous, Current, Inductive, Result) :- > > > ppl_delete_Polyhedron(Previous), > > > ppl_new_Polyhedron_from_Polyhedron(c, Current, c, Current1), > > > %% perform the required computation modifying Current1. > > > ...., > > > upward_iteration_sequence(Current, Current1, Inductive, Result). > > > > > > > > > I hope this is enough. Anyway, Pat is much more expert than me on the > > > Prolog interface of PPL. > > > > > > Ciao, > > > Enea. > > > > > > > > > -- > Prof. Roberto Bagnara > Computer Science Group > Department of Mathematics, University of Parma, Italy > http://www.cs.unipr.it/~bagnara/ > mailto:bagnara@cs.unipr.it > > -- Javier Nunez Fontarnau, School of Computing, Phone: (+44) 113 3431075 University of Leeds, LS2 9JT, Leeds, UK. Fax: (+44) 113 3435468 http://www.comp.leeds.ac.uk/javier

3 6

ppl NEWS
by Enea Zaffanella 13 Sep '04

13 Sep '04

CVSROOT: /cvs/ppl Module name: ppl Changes by: zaffanella(a)cs.unipr.it 2004-09-13 07:49:55 Modified files: . : NEWS Log message: Mentioned the bug just corrected. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/NEWS.diff?cvsroot=ppl&r1=1.10…

1 0

ppl/tests Makefile.am
by Roberto Bagnara 12 Sep '04

12 Sep '04

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2004-09-12 18:09:37 Modified files: tests : Makefile.am Log message: Use h79widening8.cc also with NNC polyhedra. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/tests/Makefile.am.diff?cvsroo…

1 0

w3ppl/htdocs/Bugs Bugs.raw archive.raw
by Enea Zaffanella 09 Sep '04

09 Sep '04

CVSROOT: /cvs/ppl Module name: w3ppl Changes by: zaffanella(a)cs.unipr.it 2004-09-09 11:36:16 Modified files: htdocs/Bugs : Bugs.raw archive.raw Log message: The bug affecting PPL 0.5 put in the archive. A new bug affecting PPL 0.6.1 has been found and corrected. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/Bugs/Bugs.raw.diff?c… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/Bugs/archive.raw.dif…

1 0

ppl/src GenSys.cc
by Enea Zaffanella 08 Sep '04

08 Sep '04

CVSROOT: /cvs/ppl Module name: ppl Branch: ppl-0_6-branch Changes by: zaffanella(a)cs.unipr.it 2004-09-08 17:14:09 Modified files: src : GenSys.cc Log message: Corrected a bug reported by Sriram. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/GenSys.cc.diff?cvsroot=pp…

1 0

Bug in PPL?
by Roberto Bagnara 08 Sep '04

08 Sep '04

Dear Roberto, If you run lsting invcheck < berkeley.in, you will notice that the output of CH79 fails to be inductive. The bug only happens when you compile the code with the boring diagnostic messages turned off. I also noticed that adding the line ConSys cs = my_poly.constraints(); just before I widen my_poly (InvariantMap.cc Line 94) corrects this problem. I am still clueless about this. It is not like I use "cs" for anything else. It is just a dummy call. Does it have to do with the fact that the widening may not work properly if the constraint representation is stale or missing, or something? I noticed this "fix" because I turned the printing diagnostics on, and the bug disappeared. The only extra thing I do when I print is to ask for the constraints and pretty print them. As usual, I could be missing something obvious :-) , or it could be a bug. If you could point me out to the right direction, I am very grateful. In the meantime, the release I sent you has the same bug which is absent in the older version. So please ignore the code. I will send you a new version when I fix this bug. Thanks, Sriram

2 1

ppl/tests h79widening8.cc
by Enea Zaffanella 08 Sep '04

08 Sep '04

CVSROOT: /cvs/ppl Module name: ppl Changes by: zaffanella(a)cs.unipr.it 2004-09-08 16:17:06 Modified files: tests : h79widening8.cc Log message: Made silent. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/tests/h79widening8.cc.diff?cv…

1 0

ppl/src GenSys.cc
by Enea Zaffanella 08 Sep '04

08 Sep '04

CVSROOT: /cvs/ppl Module name: ppl Changes by: zaffanella(a)cs.unipr.it 2004-09-08 16:15:26 Modified files: src : GenSys.cc Log message: Corrected a bug in GenSys::satisfied_by_all_generators(), which was revealed by the test h79widening8.cc. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/GenSys.cc.diff?cvsroot=pp…

1 0