- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Set aside the domain of affine spaces, for the time being.
by Roberto Bagnara 01 Aug '10

01 Aug '10

Module: ppl/ppl Branch: master Commit: 63f34f91afd96249825c7ba2371f3e973129e55e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=63f34f91afd9… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Aug 1 19:29:13 2010 +0200 Set aside the domain of affine spaces, for the time being. --- TODO | 2 +- src/Affine_Space.defs.hh | 4 ++-- src/Makefile.am | 4 ---- 3 files changed, 3 insertions(+), 7 deletions(-) diff --git a/TODO b/TODO index 76d679e..199ef0e 100644 --- a/TODO +++ b/TODO @@ -4,7 +4,7 @@ Enhancements for PPL 0.12 or later versions - Make all the *affine*image() methods uniform as far as the specification is concerned. -- Add the domain of circular linear progressions. +- Add the domains of bounded integers and affine spaces. - Finish the domain of intervals. - Intervals are best instantiated with checked numbers with particular policies: review all the interfaced boxes, diff --git a/src/Affine_Space.defs.hh b/src/Affine_Space.defs.hh index fa42333..99f0adb 100644 --- a/src/Affine_Space.defs.hh +++ b/src/Affine_Space.defs.hh @@ -129,7 +129,7 @@ bool operator!=(const Affine_Space& x, const Affine_Space& y); Variable y(1); \endcode - FIXME(0.11): revise the contents below this point of this comment block. + FIXME: revise the contents below this point of this comment block. \par Example 1 The following code builds an affine space corresponding to the even integer @@ -686,7 +686,7 @@ public: */ bool bounds_from_below(const Linear_Expression& expr) const; - // FIXME(0.11): revise all the comment blocks below this one. + // FIXME: revise all the comment blocks below this one. /*! \brief Returns <CODE>true</CODE> if and only if \p *this is not empty and diff --git a/src/Makefile.am b/src/Makefile.am index f726e90..06e9ad3 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -161,7 +161,6 @@ BHRZ03_Certificate.types.hh \ H79_Certificate.types.hh \ Grid_Certificate.types.hh \ Partial_Function.types.hh \ -Affine_Space.types.hh \ Polyhedron.types.hh \ C_Polyhedron.types.hh \ NNC_Polyhedron.types.hh \ @@ -291,8 +290,6 @@ Grid_Certificate.defs.hh \ Grid_Certificate.inlines.hh \ Partial_Function.defs.hh \ Partial_Function.inlines.hh \ -Affine_Space.defs.hh \ -Affine_Space.inlines.hh \ Polyhedron.defs.hh \ Ph_Status.inlines.hh \ Polyhedron.inlines.hh \ @@ -397,7 +394,6 @@ BHRZ03_Certificate.cc \ H79_Certificate.cc \ Grid_Certificate.cc \ Partial_Function.cc \ -Affine_Space.cc \ Polyhedron_nonpublic.cc \ Polyhedron_public.cc \ Polyhedron_chdims.cc \

1 0

[GIT] ppl/ppl(master): Implemented the constructors from generator systems.
by Roberto Bagnara 01 Aug '10

01 Aug '10

Module: ppl/ppl Branch: master Commit: 39c378347808c8a522f00b53cc8eac1123486229 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=39c378347808… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Aug 1 18:30:57 2010 +0200 Implemented the constructors from generator systems. --- src/Affine_Space.cc | 76 +++++++++++++++++++++++++++++++------------ src/Affine_Space.defs.hh | 39 +--------------------- src/Affine_Space.inlines.hh | 29 ++++++++++++---- 3 files changed, 79 insertions(+), 65 deletions(-) diff --git a/src/Affine_Space.cc b/src/Affine_Space.cc index cfd81e1..75087b7 100644 --- a/src/Affine_Space.cc +++ b/src/Affine_Space.cc @@ -23,33 +23,67 @@ site: http://www.cs.unipr.it/ppl/ . */ #include <ppl-config.h> #include "Affine_Space.defs.hh" -#if 0 -#include "Topology.hh" -#include "Scalar_Products.defs.hh" - -#include "assert.hh" -#endif #include <iostream> namespace PPL = Parma_Polyhedra_Library; -PPL::Affine_Space::Affine_Space(const Affine_Space& y, - Complexity_Class complexity) - : gr(y.gr, complexity) { -} - -PPL::Affine_Space::Affine_Space(const Constraint_System& cs) - : gr(cs) { -} - -PPL::Affine_Space::Affine_Space(Constraint_System& cs, Recycle_Input ri) - : gr(cs, ri) { +PPL::Affine_Space::Affine_Space(const Generator_System& gs) { + dimension_type space_dim = gs.space_dimension(); + // First find a point or closure point and convert it to a + // grid point and add to the (initially empty) set of grid generators. + Grid_Generator_System ggs(space_dim); + Linear_Expression point_expr; + PPL_DIRTY_TEMP_COEFFICIENT(point_divisor); + for (Generator_System::const_iterator g = gs.begin(), + gs_end = gs.end(); g != gs_end; ++g) { + if (g->is_ray()) + throw std::invalid_argument("Affine_Space::Affine_Space(gs):\n" + "gs contains rays."); + else if (g->is_point() || g->is_closure_point()) { + for (dimension_type i = space_dim; i-- > 0; ) { + const Variable v(i); + point_expr += g->coefficient(v) * v; + point_divisor = g->divisor(); + } + ggs.insert(grid_point(point_expr, point_divisor)); + goto non_empty; + } + } + // No (closure) point was found. + Grid(EMPTY).swap(gr); + return; + + non_empty: + // Add a grid line for each line. If the generator is a (closure) + // point, the grid line must have the direction given by a line + // that joins the grid point already inserted and the new point. + PPL_DIRTY_TEMP_COEFFICIENT(coeff); + PPL_DIRTY_TEMP_COEFFICIENT(g_divisor); + for (Generator_System::const_iterator g = gs.begin(), + gs_end = gs.end(); g != gs_end; ++g) { + Linear_Expression e; + if (g->is_point() || g->is_closure_point()) { + g_divisor = g->divisor(); + for (dimension_type i = space_dim; i-- > 0; ) { + const Variable v(i); + coeff = point_expr.coefficient(v) * g_divisor; + coeff -= g->coefficient(v) * point_divisor; + e += coeff * v; + } + if (e.all_homogeneous_terms_are_zero()) + continue; + } + else + for (dimension_type i = space_dim; i-- > 0; ) { + const Variable v(i); + e += g->coefficient(v) * v; + } + ggs.insert(grid_line(e)); + } + Grid(ggs).swap(gr); + PPL_ASSERT(OK()); } -PPL::Affine_Space::Affine_Space(const Polyhedron& ph, - Complexity_Class complexity) - : gr(ph, complexity) { -} PPL::Affine_Space& PPL::Affine_Space::operator=(const Affine_Space& y) { diff --git a/src/Affine_Space.defs.hh b/src/Affine_Space.defs.hh index c7bc820..fa42333 100644 --- a/src/Affine_Space.defs.hh +++ b/src/Affine_Space.defs.hh @@ -24,30 +24,20 @@ site: http://www.cs.unipr.it/ppl/ . */ #define PPL_Affine_Space_defs_hh 1 #include "Affine_Space.types.hh" -#if 0 -#include "globals.defs.hh" #include "Variable.defs.hh" #include "Variables_Set.types.hh" -#include "Linear_Expression.defs.hh" -#include "Constraint.defs.hh" +#include "Linear_Expression.types.hh" +#include "Constraint.types.hh" #include "Constraint_System.defs.hh" #include "Constraint_System.inlines.hh" #include "Congruence_System.defs.hh" #include "Congruence_System.inlines.hh" -#include "Grid_Generator_System.defs.hh" -#include "Grid_Generator_System.inlines.hh" -#include "Grid_Generator.types.hh" #include "Poly_Con_Relation.defs.hh" #include "Poly_Gen_Relation.defs.hh" -#include "Grid_Certificate.types.hh" #include "Box.types.hh" -#include "Polyhedron.defs.hh" #include "Polyhedron.types.hh" -#include "Polyhedron.inlines.hh" #include "BD_Shape.types.hh" #include "Octagonal_Shape.types.hh" -#include <vector> -#endif #include "Grid.defs.hh" #include <iosfwd> @@ -1696,31 +1686,6 @@ protected: void throw_dimension_incompatible(const char* method, const char* as_name, const Affine_Space& as) const; -#if 0 - void throw_dimension_incompatible(const char* method, - const char* e_name, - const Linear_Expression& e) const; - void throw_dimension_incompatible(const char* method, - const char* cg_name, - const Congruence& cg) const; - void throw_dimension_incompatible(const char* method, - const char* c_name, - const Constraint& c) const; - void throw_dimension_incompatible(const char* method, - const char* g_name, - const Generator& g) const; - void throw_dimension_incompatible(const char* method, - const char* cgs_name, - const Congruence_System& cgs) const; - void throw_dimension_incompatible(const char* method, - const char* cs_name, - const Constraint_System& cs) const; - void throw_dimension_incompatible(const char* method, - const char* var_name, - Variable var) const; - void throw_dimension_incompatible(const char* method, - dimension_type required_space_dim) const; -#endif // Note: it has to be a static method, because it can be called inside // constructors (before actually constructing the grid object). diff --git a/src/Affine_Space.inlines.hh b/src/Affine_Space.inlines.hh index 97a65d2..1b4f595 100644 --- a/src/Affine_Space.inlines.hh +++ b/src/Affine_Space.inlines.hh @@ -37,16 +37,31 @@ Affine_Space::Affine_Space(dimension_type num_dimensions, } inline -Affine_Space::Affine_Space(const Generator_System& /*gs*/) { - // FIXME(0.11): implement by building the grid generators. - // Throw std::invalid_argument if `gs' contains rays. - abort(); +Affine_Space::Affine_Space(const Affine_Space& y, + Complexity_Class complexity) + : gr(y.gr, complexity) { +} + +inline +Affine_Space::Affine_Space(const Constraint_System& cs) + : gr(cs) { +} + +inline +Affine_Space::Affine_Space(Constraint_System& cs, Recycle_Input ri) + : gr(cs, ri) { +} + +inline +Affine_Space::Affine_Space(const Polyhedron& ph, + Complexity_Class complexity) + : gr(ph, complexity) { } inline -Affine_Space::Affine_Space(Generator_System& /*gs*/, Recycle_Input) { - // FIXME(0.11): implement by building the grid generators. - abort(); +Affine_Space::Affine_Space(Generator_System& gs, Recycle_Input) + : gr(EMPTY) { + Affine_Space(gs).swap(*this); } template <typename U>

1 0

[GIT] ppl/ppl(master): Inclusions fixed.
by Roberto Bagnara 01 Aug '10

01 Aug '10

Module: ppl/ppl Branch: master Commit: 5e53ad77d4ca05be5707ee31cde1e42e9db130fe URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5e53ad77d4ca… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Aug 1 18:25:59 2010 +0200 Inclusions fixed. --- src/Grid.defs.hh | 4 +--- src/Grid_public.cc | 2 +- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Grid.defs.hh b/src/Grid.defs.hh index c51ffd0..8ce547c 100644 --- a/src/Grid.defs.hh +++ b/src/Grid.defs.hh @@ -28,7 +28,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Variable.defs.hh" #include "Variables_Set.types.hh" #include "Linear_Expression.defs.hh" -#include "Constraint.defs.hh" +#include "Constraint.types.hh" #include "Constraint_System.defs.hh" #include "Constraint_System.inlines.hh" #include "Congruence_System.defs.hh" @@ -40,9 +40,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Poly_Gen_Relation.defs.hh" #include "Grid_Certificate.types.hh" #include "Box.types.hh" -#include "Polyhedron.defs.hh" #include "Polyhedron.types.hh" -#include "Polyhedron.inlines.hh" #include "BD_Shape.types.hh" #include "Octagonal_Shape.types.hh" #include <vector> diff --git a/src/Grid_public.cc b/src/Grid_public.cc index ac0ac43..10c7843 100644 --- a/src/Grid_public.cc +++ b/src/Grid_public.cc @@ -25,7 +25,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Grid.defs.hh" #include "Topology.hh" #include "Scalar_Products.defs.hh" - +#include "Polyhedron.defs.hh" #include "assert.hh" #include <iostream>

1 0

[GIT] ppl/ppl(master): Useless assignment removed.
by Roberto Bagnara 01 Aug '10

01 Aug '10

Module: ppl/ppl Branch: master Commit: 4f98fc584f6ce346558401b96a759684f5133b33 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4f98fc584f6c… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Aug 1 17:12:52 2010 +0200 Useless assignment removed. --- src/Grid_public.cc | 1 - 1 files changed, 0 insertions(+), 1 deletions(-) diff --git a/src/Grid_public.cc b/src/Grid_public.cc index fcf89c0..ac0ac43 100644 --- a/src/Grid_public.cc +++ b/src/Grid_public.cc @@ -184,7 +184,6 @@ PPL::Grid::Grid(const Polyhedron& ph, construct(cgs); } else { - gen_sys = Grid_Generator_System(space_dim); // First find a point or closure point and convert it to a // grid point and add to the (initially empty) set of grid generators. PPL_ASSERT(ph.generators_are_up_to_date());

1 0

[GIT] ppl/ppl(master): Comment fixed.
by Roberto Bagnara 01 Aug '10

01 Aug '10

Module: ppl/ppl Branch: master Commit: c9b370c2c65a3c0f23e25d492d520a7ce61ecb1c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c9b370c2c65a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Aug 1 17:10:31 2010 +0200 Comment fixed. --- src/Grid_Generator_System.defs.hh | 10 +++++----- 1 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Grid_Generator_System.defs.hh b/src/Grid_Generator_System.defs.hh index 7ad7960..1fe1e4a 100644 --- a/src/Grid_Generator_System.defs.hh +++ b/src/Grid_Generator_System.defs.hh @@ -251,16 +251,16 @@ public: The following code prints the system of generators of the grid <CODE>gr</CODE>: \code - const Grid_Generator_System& gs = gr.generators(); - for (Grid_Generator_System::const_iterator i = gs.begin(), - gs_end = gs.end(); i != gs_end; ++i) + const Grid_Generator_System& ggs = gr.generators(); + for (Grid_Generator_System::const_iterator i = ggs.begin(), + ggs_end = ggs.end(); i != ggs_end; ++i) cout << *i << endl; \endcode The same effect can be obtained more concisely by using more features of the STL: \code - const Generator_System& gs = gr.generators(); - copy(gs.begin(), gs.end(), ostream_iterator<Grid_Generator>(cout, "\n")); + const Grid_Generator_System& ggs = gr.generators(); + copy(ggs.begin(), ggs.end(), ostream_iterator<Grid_Generator>(cout, "\n")); \endcode */ class const_iterator

1 0

[GIT] ppl/ppl(master): Removed spurious semicolon.
by Abramo Bagnara 01 Aug '10

01 Aug '10

Module: ppl/ppl Branch: master Commit: f6ed02b5218888557099dfa1ea0aefee070a03c4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f6ed02b52188… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Sun Aug 1 14:37:00 2010 +0200 Removed spurious semicolon. --- src/Interval_Restriction.defs.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Interval_Restriction.defs.hh b/src/Interval_Restriction.defs.hh index 22a7d9e..b3dfc32 100644 --- a/src/Interval_Restriction.defs.hh +++ b/src/Interval_Restriction.defs.hh @@ -131,7 +131,7 @@ class Interval_Restriction_None : public Interval_Restriction_None_Base, public Base { public: Interval_Restriction_None() { - }; + } template <typename T> Interval_Restriction_None(const T& init) : Base(init) {

1 0

[GIT] ppl/ppl(floating_point): Rewritten test06 and test07.
by Fabio Bossi 31 Jul '10

31 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 17105335ca1841766bd314c9275649e87475e931 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=17105335ca18… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Sat Jul 31 16:08:03 2010 +0200 Rewritten test06 and test07. --- tests/Concrete_Expression/digitalfilters1.cc | 442 +++++++++++++++++++++++++- 1 files changed, 440 insertions(+), 2 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=17105335…

1 0

[GIT] ppl/ppl(floating_point): Do not perform interval analysis on an assignment
by Fabio Bossi 31 Jul '10

31 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 41ec2a4972b2682d0237880e2c3f5f2df238bb5c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=41ec2a4972b2… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Sat Jul 31 15:39:01 2010 +0200 Do not perform interval analysis on an assignment before linearization. --- tests/Concrete_Expression/digitalfilters1.cc | 379 ++------------------------ 1 files changed, 17 insertions(+), 362 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=41ec2a49…

1 0

[GIT] ppl/ppl(floating_point): Float:
by Fabio Bossi 31 Jul '10

31 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 1c9679165d7d9719426ed316f6b26dcaace36b58 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1c9679165d7d… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Sat Jul 31 12:53:20 2010 +0200 Float: Added a few functions that operate on linear form abstract stores. linearize.cc: test05 now consistently utilizes linear form abstract stores. --- src/Float.defs.hh | 32 ++++++++++++++ src/Float.inlines.hh | 14 ++++++ src/Float.templates.hh | 52 +++++++++++++++++++++++ tests/Concrete_Expression/digitalfilters1.cc | 57 ++++++++++++++++++++----- 4 files changed, 143 insertions(+), 12 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=1c967916…

1 0

[GIT] ppl/ppl(floating_point): Rewritten test05 ( still lacks proper use of the linear
by Fabio Bossi 30 Jul '10

30 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 3b3495a1556330ec9ae4cf72c00398db01a10c46 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3b3495a15563… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Jul 30 19:21:33 2010 +0200 Rewritten test05 (still lacks proper use of the linear form abstract store). --- tests/Concrete_Expression/digitalfilters1.cc | 87 +++++++++++++------------- 1 files changed, 44 insertions(+), 43 deletions(-) diff --git a/tests/Concrete_Expression/digitalfilters1.cc b/tests/Concrete_Expression/digitalfilters1.cc index 204ef54..75deac5 100644 --- a/tests/Concrete_Expression/digitalfilters1.cc +++ b/tests/Concrete_Expression/digitalfilters1.cc @@ -21,6 +21,7 @@ For the most up-to-date information see the Parma Polyhedra Library site: http://www.cs.unipr.it/ppl/ . */ #include "ppl_test.hh" +#include "C_Expr.defs.hh" namespace { @@ -423,7 +424,7 @@ test04() { return (tmp.lower() == -128 && tmp.upper() == 128); } -/* + // Tests rate limiter using bounded differences and linearization of // floating point expressions. // In order to improve the analysis, the interval domain is used @@ -459,23 +460,22 @@ test05() { cs.insert(Y <= M); cs.insert(Y >= -M); - Con_FP_Expression con_y("0"); + Floating_Point_Constant<C_Expr> con_y("0", 2); // The constant floating point expression con_y is linearized into // the interval linear form lk. If linearization succeeded, we model // the assignment Y = 0, invoking affine_form_image method. - // FIXME: In order to refine the analysis, all the transer function are + // In order to refine the analysis, all the transer function are // performed in parallel in the interval domain and in the bounded // differences domain. // Then, we consider the intersection between these abstract domains. interval_store.affine_form_image(Y, FP_Linear_Form(tmp)); - if (con_y.linearize(interval_store, lf_abstract_store, lk)) + if (linearize(con_y, interval_store, lf_abstract_store, lk)) bd.affine_form_image(Y, lk); else - bd.affine_form_image(Y, FP_Linear_Form(interval_store.get_interval(Y))); + bd.intersection_assign(FP_BD_Shape(interval_store)); interval_store.intersection_assign(FP_Interval_Abstract_Store(bd)); - // This loop iterate until a fixed point is reached. do { @@ -489,74 +489,73 @@ test05() { tmp.lower() = -128; tmp.upper() = 128; interval_store.affine_form_image(X, FP_Linear_Form(tmp)); - Con_FP_Expression con_x(-128, 128); - if (con_x.linearize(interval_store, lf_abstract_store, lk)) - bd.affine_form_image(X, lk); - else - bd.affine_form_image(X, FP_Linear_Form(interval_store.get_interval(X))); + bd.affine_form_image(X, FP_Linear_Form(tmp)); interval_store.intersection_assign(FP_Interval_Abstract_Store(bd)); // D = [0, 16]; tmp.lower() = 0; tmp.upper() = 16; interval_store.affine_form_image(D, FP_Linear_Form(tmp)); - Con_FP_Expression con_d(0, 16); - if (con_d.linearize(interval_store, lf_abstract_store, lk)) - bd.affine_form_image(D, lk); - else - bd.affine_form_image(D, FP_Linear_Form(interval_store.get_interval(D))); + bd.affine_form_image(D, FP_Linear_Form(tmp)); interval_store.intersection_assign(FP_Interval_Abstract_Store(bd)); // S = Y; interval_store.affine_form_image(S, FP_Linear_Form(Y)); - Var_FP_Expression var_y(Y.id()); - if (var_y.linearize(interval_store, lf_abstract_store, ly)) + Approximable_Reference<C_Expr> var_y(FP_Type, Int_Interval(mpz_class(0)), + Y.id()); + if (linearize(var_y, interval_store, lf_abstract_store, ly)) bd.affine_form_image(S, ly); else - bd.affine_form_image(S, FP_Linear_Form(interval_store.get_interval(S))); + bd.intersection_assign(FP_BD_Shape(interval_store)); interval_store.intersection_assign(FP_Interval_Abstract_Store(bd)); // R = X - S; - Var_FP_Expression* px = new Var_FP_Expression(X.id()); - Var_FP_Expression* ps = new Var_FP_Expression(S.id()); - Dif_FP_Expression x_dif_s(px, ps); + Approximable_Reference<C_Expr> px(FP_Type, Int_Interval(mpz_class(0)), + X.id()); + Approximable_Reference<C_Expr> ps(FP_Type, Int_Interval(mpz_class(0)), + S.id()); + Binary_Operator<C_Expr> x_dif_s(FP_Type, Binary_Operator<C_Expr>::SUB, + &px, &ps); interval_store.affine_form_image(R, FP_Linear_Form(X - S)); - if (x_dif_s.linearize(interval_store, lf_abstract_store, lr)) + if (linearize(x_dif_s, interval_store, lf_abstract_store, lr)) bd.affine_form_image(R, lr); else - bd.affine_form_image(R, FP_Linear_Form(interval_store.get_interval(R))); + bd.intersection_assign(FP_BD_Shape(interval_store)); interval_store.intersection_assign(FP_Interval_Abstract_Store(bd)); // Y = X; - Var_FP_Expression var_x(X.id()); interval_store.affine_form_image(Y, FP_Linear_Form(X)); - if (var_x.linearize(interval_store, lf_abstract_store, lx)) + if (linearize(px, interval_store, lf_abstract_store, lx)) bd.affine_form_image(Y, lx); else - bd.affine_form_image(Y, FP_Linear_Form(interval_store.get_interval(Y))); + bd.intersection_assign(FP_BD_Shape(interval_store)); interval_store.intersection_assign(FP_Interval_Abstract_Store(bd)); // if (R <= -D) FP_BD_Shape bd_then(bd); FP_Interval_Abstract_Store is_then(interval_store); is_then.refine_with_constraint(R <= -D); - bd_then.refine_with_linear_form_inequality(lr, -lk); + bd_then.refine_with_linear_form_inequality(FP_Linear_Form(R), + -FP_Linear_Form(D)); is_then.intersection_assign(FP_Interval_Abstract_Store(bd_then)); // then Y = S - D; - Var_FP_Expression* pd = new Var_FP_Expression(D.id()); - Var_FP_Expression* ps2 = new Var_FP_Expression(S.id()); - Dif_FP_Expression s_dif_d(ps2, pd); + Approximable_Reference<C_Expr> pd(FP_Type, Int_Interval(mpz_class(0)), + D.id()); + Binary_Operator<C_Expr> s_dif_d(FP_Type, Binary_Operator<C_Expr>::SUB, + &ps, &pd); is_then.affine_form_image(Y, FP_Linear_Form(S - D)); - if (s_dif_d.linearize(is_then, lf_abstract_store, ly)) + if (linearize(s_dif_d, is_then, lf_abstract_store, ly)) bd_then.affine_form_image(Y, ly); else - bd_then.affine_form_image(Y, FP_Linear_Form(is_then.get_interval(Y))); + bd_then.intersection_assign(FP_BD_Shape(is_then)); is_then.intersection_assign(FP_Interval_Abstract_Store(bd_then)); // else skip; interval_store.refine_with_constraint(R > -D); - bd.refine_with_linear_form_inequality(-lk, lr); + bd.refine_with_linear_form_inequality(-FP_Linear_Form(D), + FP_Linear_Form(R)); + bd.intersection_assign(FP_BD_Shape(interval_store)); interval_store.intersection_assign(FP_Interval_Abstract_Store(bd)); // LUB between then and else branches. @@ -568,22 +567,23 @@ test05() { bd_then = bd; is_then = interval_store; is_then.refine_with_constraint(R >= D); - bd_then.refine_with_linear_form_inequality(lk, lr); + bd_then.refine_with_linear_form_inequality(FP_Linear_Form(D), + FP_Linear_Form(R)); is_then.intersection_assign(FP_Interval_Abstract_Store(bd_then)); // then Y = S + D; - Var_FP_Expression* pd1 = new Var_FP_Expression(D.id()); - Var_FP_Expression* ps3 = new Var_FP_Expression(S.id()); - Sum_FP_Expression s_sum_d(ps3, pd1); + Binary_Operator<C_Expr> s_sum_d(FP_Type, Binary_Operator<C_Expr>::ADD, + &ps, &pd); is_then.affine_form_image(Y, FP_Linear_Form(S + D)); - if (s_sum_d.linearize(is_then, lf_abstract_store, ly)) + if (linearize(s_sum_d, is_then, lf_abstract_store, ly)) bd_then.affine_form_image(Y, ly); else - bd_then.affine_form_image(Y, FP_Linear_Form(is_then.get_interval(Y))); + bd_then.intersection_assign(FP_BD_Shape(is_then)); is_then.intersection_assign(FP_Interval_Abstract_Store(bd_then)); // else skip; - bd.refine_with_linear_form_inequality(lr, lk); + bd.refine_with_linear_form_inequality(FP_Linear_Form(R), + FP_Linear_Form(D)); interval_store.refine_with_constraint(R < D); bd.intersection_assign(FP_BD_Shape(interval_store)); interval_store.intersection_assign(FP_Interval_Abstract_Store(bd)); @@ -612,7 +612,7 @@ test05() { return (tmp.lower() == -144 && tmp.upper() == 144); } - +/* // Tests rate limiter using octagonal shapes and linearization of // floating point expressions. // In order to improve the analysis, the interval domain is used @@ -990,7 +990,7 @@ BEGIN_MAIN DO_TEST_F8(test02); DO_TEST_F8(test03); DO_TEST_F64A(test04); -/* + #define COND_float PPL_CPP_EQ(PPL_CPP_FP_FORMAT(ANALYZER_FP_FORMAT), 1) #define COND_double PPL_CPP_EQ(PPL_CPP_FP_FORMAT(ANALYZER_FP_FORMAT), 2) #define COND_float_or_double PPL_CPP_OR(COND_float, COND_double) @@ -1002,6 +1002,7 @@ BEGIN_MAIN PPL_CPP_OR(COND_F64, PPL_CPP_OR(PPL_CUSTOM_COND_32, PPL_CUSTOM_COND_64)) COND_DO_TEST(PPL_CUSTOM_COND, test05); +/* COND_DO_TEST(PPL_CUSTOM_COND, test06); DO_TEST_F64(test07);

1 0