September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): Removed trailing whitespace.
by Fabio Bossi 09 Sep '09

09 Sep '09

Module: ppl/ppl Branch: floating_point Commit: a77be211bad2e751dded38345ad38bf11cc7dc56 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a77be211bad2… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 9 10:20:06 2009 +0200 Removed trailing whitespace. --- doc/definitions.dox | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index aaa0f11..4f241cd 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2653,7 +2653,7 @@ in the documentation for the sake of simplicity, with the exception of unbounded intervals that have \f$\infty\f$ boundaries. We denote the set of all linear forms on \f$\mathbb{F}_a\f$ by \f$\mathbb{L}_a\f$. -The \link Parma_Polyhedra_Library::Linear_Form \c Linear_Form \endlink class +The \link Parma_Polyhedra_Library::Linear_Form \c Linear_Form \endlink class provides common algebraic operations on linear forms: you can add or subtract two linear forms, and multiply or divide a linear form by a scalar. We are writing only about interval linear forms in this section, so our

1 0

[GIT] ppl/ppl(floating_point): More documentation.
by Fabio Bossi 09 Sep '09

09 Sep '09

Module: ppl/ppl Branch: floating_point Commit: faab1d298643299aa7cd3a38aa02c33f643946ff URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=faab1d298643… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 9 10:19:02 2009 +0200 More documentation. --- doc/definitions.dox | 53 ++++++++++++++++++++++++++++++++++++++++++++++++++- 1 files changed, 52 insertions(+), 1 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index 8aba517..aaa0f11 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2653,6 +2653,50 @@ in the documentation for the sake of simplicity, with the exception of unbounded intervals that have \f$\infty\f$ boundaries. We denote the set of all linear forms on \f$\mathbb{F}_a\f$ by \f$\mathbb{L}_a\f$. +The \link Parma_Polyhedra_Library::Linear_Form \c Linear_Form \endlink class +provides common algebraic operations on linear forms: you can add or +subtract two linear forms, and multiply or divide a linear form by a scalar. +We are writing only about interval linear forms in this section, so our +scalars will always be intervals with floating point boundaries. +The operations on interval linear forms are intuitively defined as follows: + +\f[ + + \left(i + \sum_{v \in V}i_{v}v\right) + \aslf + \left(i' + \sum_{v \in V}i'_{v}v\right) + = + \left(i \asifp i'\right) + + \sum_{v \in V}\left(i_{v} \asifp i'_{v}\right)v, + + \left(i + \sum_{v \in V}i_{v}v\right) + \adlf + \left(i' + \sum_{v \in V}i'_{v}v\right) + = + \left(i \adifp i'\right) + + \sum_{v \in V}\left(i_{v} \adifp i'_{v}\right)v, + + i + \amlf + \left(i' + \sum_{v \in V}i'_{v}v\right) + = + \left(i \amifp i'\right) + + \sum_{v \in V}\left(i \amifp i'_{v}\right)v, + + \left(i + \sum_{v \in V}i_{v}v\right) + \adivlf + i' + = + \left(i \adivifp i'\right) + + \sum_{v \in V}\left(i_{v} \adivifp i'\right)v. + +\f] + +Where \f$\asifp, \adifp, \amifp,\f$ and \f$\adivifp\f$ are the corresponding +operations on intervals. Note that these operations always round the +interval's lower bound towards \f$-\infty\f$ and the upper bound towards +\f$+\infty\f$ in order to obtain a correct overapproximation. + A (composite) floating point abstract store is used to associate each floating point variable with its currently known approximation. The store is composed by two parts: @@ -2662,9 +2706,16 @@ composed by two parts: associating each variable with its current approximating linear form. Both stores are represented by maps of the Standard Template Library and are -needed for performing linearization. Please see the documentation of floating +required by the linearize method. Please see the documentation of floating point expression classes for more information. +The linearization of a floating point expression \f$e\f$ in the composite +abstract store \f$\left \langle \rho, \rho_l \right \rangle\f$ will be denoted +by \f$\f$. There are two ways a linearization attempt can fail: + - whenever an interval boundary overflows to \f$+\infty\f$ or \f$-\infty\f$, + and + - when we try to divide by an interval that contains \f$0\f$. + \section use_of_library Using the Library \subsection A_Note_on_the_Implementation_of_the_Operators A Note on the Implementation of the Operators

1 0

[GIT] ppl/ppl(floating_point): Fixed a bug in operator==.
by Fabio Bossi 09 Sep '09

09 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 940b8bf4bf2442aec711f75c885e1fa8ea39e9f5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=940b8bf4bf24… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 9 10:17:52 2009 +0200 Fixed a bug in operator==. --- src/Linear_Form.templates.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Linear_Form.templates.hh b/src/Linear_Form.templates.hh index ffa6772..e7c12f9 100644 --- a/src/Linear_Form.templates.hh +++ b/src/Linear_Form.templates.hh @@ -330,7 +330,7 @@ operator==(const Linear_Form<C>& x, const Linear_Form<C>& y) { if (x[i] != y[i]) return false; - for (dimension_type i = x_size; --i > y_size; ) + for (dimension_type i = x_size; --i >= y_size; ) if (x[i] != x.zero) return false; @@ -340,7 +340,7 @@ operator==(const Linear_Form<C>& x, const Linear_Form<C>& y) { if (x[i] != y[i]) return false; - for (dimension_type i = y_size; --i > x_size; ) + for (dimension_type i = y_size; --i >= x_size; ) if (y[i] != x.zero) return false;

1 0

[GIT] ppl/ppl(floating_point): Added new macros into doc/ppl.sty
by Fabio Biselli 09 Sep '09

09 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 867f1eaf166ffb70cd727683c4977cea44a6ac92 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=867f1eaf166f… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Wed Sep 9 12:01:58 2009 +0200 Added new macros into doc/ppl.sty --- doc/ppl.sty | 3 +++ 1 files changed, 3 insertions(+), 0 deletions(-) diff --git a/doc/ppl.sty b/doc/ppl.sty index 87b3207..27055c5 100644 --- a/doc/ppl.sty +++ b/doc/ppl.sty @@ -191,3 +191,6 @@ \newcommand*{\adlf}{\boxminus^{\#}_{\mathbf{f}}} \newcommand*{\adivlf}{\boxslash^{\#}_{\mathbf{f}}} \newcommand*{\amlf}{\boxtimes^{\#}_{\mathbf{f}}} +\def\llexpr{(\kern-.1667em|} +\def\rlexpr{|\kern-.1667em)} +\newcommand*{\linexpr}[1]{\llexpr #1 \rlexpr}

1 0

[GIT] ppl/ppl(floating_point): Added Linear_Form into doxyconf file
by Fabio Biselli 08 Sep '09

08 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 18fcb47fba6d6754d0c963c5235851acf817896a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=18fcb47fba6d… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Tue Sep 8 20:30:46 2009 +0200 Added Linear_Form into doxyconf file Fixed few typos in Linear_Form Minor Documentations updates --- doc/devref.doxyconf-html.in | 5 +++ src/Linear_Form.defs.hh | 42 ++++++++++++++-------------- src/Sum_Floating_Point_Expression.defs.hh | 18 +++++++----- 3 files changed, 37 insertions(+), 28 deletions(-) diff --git a/doc/devref.doxyconf-html.in b/doc/devref.doxyconf-html.in index 23938aa..7ecb038 100644 --- a/doc/devref.doxyconf-html.in +++ b/doc/devref.doxyconf-html.in @@ -338,6 +338,11 @@ INPUT = @srcdir@/definitions.dox \ @srcdir@/../src/Variable_Floating_Point_Expression.types.hh \ @srcdir@/../src/Variable_Floating_Point_Expression.defs.hh \ @srcdir@/../src/Variable_Floating_Point_Expression.inlines.hh \ + @srcdir@/../src/Linear_Form.types.hh \ + @srcdir@/../src/Linear_Form.defs.hh \ + @srcdir@/../src/Linear_Form.inlines.hh \ + @srcdir@/../src/Linear_Form.templates.hh \ + @srcdir@/../src/Linear_Form.cc \ @srcdir@/gpl.dox \ @srcdir@/fdl.dox INPUT_ENCODING = UTF-8 diff --git a/src/Linear_Form.defs.hh b/src/Linear_Form.defs.hh index e66fe2d..cf90398 100644 --- a/src/Linear_Form.defs.hh +++ b/src/Linear_Form.defs.hh @@ -31,97 +31,97 @@ site: http://www.cs.unipr.it/ppl/ . */ namespace Parma_Polyhedra_Library { // Put them in the namespace here to declare them friend later. -//! Returns the linear form \p e1 + \p e2. +//! Returns the linear form \p f1 + \p f2. /*! \relates Linear_Form */ template <typename C> Linear_Form<C> operator+(const Linear_Form<C>& f1, const Linear_Form<C>& f2); -//! Returns the linear form \p v + \p e. +//! Returns the linear form \p v + \p f. /*! \relates Linear_Form */ template <typename C> Linear_Form<C> operator+(Variable v, const Linear_Form<C>& f); -//! Returns the linear form \p e + \p v. +//! Returns the linear form \p f + \p v. /*! \relates Linear_Form */ template <typename C> Linear_Form<C> operator+(const Linear_Form<C>& f, Variable v); -//! Returns the linear form \p n + \p e. +//! Returns the linear form \p n + \p f. /*! \relates Linear_Form */ template <typename C> Linear_Form<C> operator+(const C& n, const Linear_Form<C>& f); -//! Returns the linear form \p e + \p n. +//! Returns the linear form \p f + \p n. /*! \relates Linear_Form */ template <typename C> Linear_Form<C> operator+(const Linear_Form<C>& f, const C& n); -//! Returns the linear form \p e. +//! Returns the linear form \p f. /*! \relates Linear_Form */ template <typename C> Linear_Form<C> operator+(const Linear_Form<C>& f); -//! Returns the linear form - \p e. +//! Returns the linear form - \p f. /*! \relates Linear_Form */ template <typename C> Linear_Form<C> operator-(const Linear_Form<C>& f); -//! Returns the linear form \p e1 - \p e2. +//! Returns the linear form \p f1 - \p f2. /*! \relates Linear_Form */ template <typename C> Linear_Form<C> operator-(const Linear_Form<C>& f1, const Linear_Form<C>& f2); -//! Returns the linear form \p v - \p e. +//! Returns the linear form \p v - \p f. /*! \relates Linear_Form */ template <typename C> Linear_Form<C> operator-(Variable v, const Linear_Form<C>& f); -//! Returns the linear form \p e - \p v. +//! Returns the linear form \p f - \p v. /*! \relates Linear_Form */ template <typename C> Linear_Form<C> operator-(const Linear_Form<C>& f, Variable v); -//! Returns the linear form \p n - \p e. +//! Returns the linear form \p n - \p f. /*! \relates Linear_Form */ template <typename C> Linear_Form<C> operator-(const C& n, const Linear_Form<C>& f); -//! Returns the linear form \p e - \p n. +//! Returns the linear form \p f - \p n. /*! \relates Linear_Form */ template <typename C> Linear_Form<C> operator-(const Linear_Form<C>& f, const C& n); -//! Returns the linear form \p n * \p e. +//! Returns the linear form \p n * \p f. /*! \relates Linear_Form */ template <typename C> Linear_Form<C> operator*(const C& n, const Linear_Form<C>& f); -//! Returns the linear form \p e * \p n. +//! Returns the linear form \p f * \p n. /*! \relates Linear_Form */ template <typename C> Linear_Form<C> operator*(const Linear_Form<C>& f, const C& n); -//! Returns the linear form \p e1 + \p e2 and assigns it to \p e1. +//! Returns the linear form \p f1 + \p f2 and assigns it to \p e1. /*! \relates Linear_Form */ template <typename C> Linear_Form<C>& operator+=(Linear_Form<C>& f1, const Linear_Form<C>& f2); -//! Returns the linear form \p e + \p v and assigns it to \p e. +//! Returns the linear form \p f + \p v and assigns it to \p f. /*! \relates Linear_Form \exception std::length_error Thrown if the space dimension of \p v exceeds @@ -131,19 +131,19 @@ template <typename C> Linear_Form<C>& operator+=(Linear_Form<C>& f, Variable v); -//! Returns the linear form \p e + \p n and assigns it to \p e. +//! Returns the linear form \p f + \p n and assigns it to \p f. /*! \relates Linear_Form */ template <typename C> Linear_Form<C>& operator+=(Linear_Form<C>& f, const C& n); -//! Returns the linear form \p e1 - \p e2 and assigns it to \p e1. +//! Returns the linear form \p f1 - \p f2 and assigns it to \p f1. /*! \relates Linear_Form */ template <typename C> Linear_Form<C>& operator-=(Linear_Form<C>& f1, const Linear_Form<C>& f2); -//! Returns the linear form \p e - \p v and assigns it to \p e. +//! Returns the linear form \p f - \p v and assigns it to \p f. /*! \relates Linear_Form \exception std::length_error Thrown if the space dimension of \p v exceeds @@ -153,13 +153,13 @@ template <typename C> Linear_Form<C>& operator-=(Linear_Form<C>& f, Variable v); -//! Returns the linear form \p e - \p n and assigns it to \p e. +//! Returns the linear form \p f - \p n and assigns it to \p f. /*! \relates Linear_Form */ template <typename C> Linear_Form<C>& operator-=(Linear_Form<C>& f, const C& n); -//! Returns the linear form \p n * \p e and assigns it to \p e. +//! Returns the linear form \p n * \p f and assigns it to \p f. /*! \relates Linear_Form */ template <typename C> Linear_Form<C>& diff --git a/src/Sum_Floating_Point_Expression.defs.hh b/src/Sum_Floating_Point_Expression.defs.hh index dab7cb9..ed58cfa 100644 --- a/src/Sum_Floating_Point_Expression.defs.hh +++ b/src/Sum_Floating_Point_Expression.defs.hh @@ -57,18 +57,22 @@ namespace Parma_Polyhedra_Library { \par Linearizations of floating-point sum expressions - Let \f$i + \sum_{v \in V}i_{v}v \f$ be a linear form we define an abstract - operator \f$\aslf\f$: + Let \f$i + \sum_{v \in \cV}i_{v}v \f$ and + \f$i' + \sum_{v \in \cV}i'_{v}v \f$ + be two linear forms and \f$\aslf\f$ a sound abstract operator on linear + form such that: \f[ - \begin{left} - \left(i + \sum_{v \in V}i_{v}v\right) + \left(i + \sum_{v \in \cV}i_{v}v\right) \aslf - \left(i' + \sum_{v \in V}i'_{v}v\right) + \left(i' + \sum_{v \in \cV}i'_{v}v\right) = \left(i \asifp i'\right) + - \sum_{v \in V}\left(i_{v} \asifp i'_{v}\right)v - \end{left} + \sum_{v \in \cV}\left(i_{v} \asifp i'_{v}\right)v \f] + Given an expression \f$\textrm{expr}_{\mathbf{f}}\f$ and an interval + abstract store \f$\rho^{\#}\f$, we construct the interval linear form + \f$\left(\textrm{expr}_{\mathbf{f}}\right)\rho^{\#}\f$ on \f$\cV\f$ as + follow: */ template <typename FP_Interval_Type, typename FP_Format> class Sum_Floating_Point_Expression

1 0

[GIT] ppl/ppl(floating_point): Added and modified tests in order to reach the coverage of 100%
by Roberto Amadini 08 Sep '09

08 Sep '09

Module: ppl/ppl Branch: floating_point Commit: b3919a859f9bb911753bee7bb9059dea1095d99a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b3919a859f9b… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Tue Sep 8 17:25:56 2009 +0200 Added and modified tests in order to reach the coverage of 100% in Floating_Point_Expression class and its derived classes. --- .../floatingpointexpr1.cc | 101 ++++++++++++++++++- 1 files changed, 95 insertions(+), 6 deletions(-) diff --git a/tests/Floating_Point_Expression/floatingpointexpr1.cc b/tests/Floating_Point_Expression/floatingpointexpr1.cc index 4575fdc..1553458 100644 --- a/tests/Floating_Point_Expression/floatingpointexpr1.cc +++ b/tests/Floating_Point_Expression/floatingpointexpr1.cc @@ -110,7 +110,7 @@ test02() { div.linearize(sstr(), lsstr(), result); } catch (Linearization_Failed e) { - nout << "Division by zero." << endl; + nout << "*** Linearization failed due to division by zero. ***" << endl; return true; } return false; @@ -160,9 +160,39 @@ test03() { return ok_fl && ok_db; } -// Tests the linearization of A + B. +// Tests the linearization of variables in a given linear form abstract store. bool test04() { + lsdtr store_fl; + Variable A(0); + Float_Interval_Linear_Form known_result_fl = Float_Interval_Linear_Form(A); + store_fl[0] = known_result_fl; + var_fpesd var_fl(0); + Float_Interval_Linear_Form result_fl; + var_fl.linearize(sdtr(), store_fl, result_fl); + + nout << "*** known_result_fl ***" << endl + << known_result_fl << endl; + bool ok_fl = (result_fl == known_result_fl); + + lddtr store_db; + Double_Interval_Linear_Form known_result_db = + Double_Interval_Linear_Form(A); + store_db[0] = known_result_db; + var_fpedd var_db(0); + Double_Interval_Linear_Form result_db; + var_db.linearize(ddtr(), store_db, result_db); + + nout << "*** known_result_db ***" << endl + << known_result_db << endl; + bool ok_db = (result_db == known_result_db); + + return ok_fl && ok_db; +} + +// Tests the linearization of A + B. +bool +test05() { dstr store; db_r_oc tmp; store[0] = tmp; @@ -192,7 +222,7 @@ test04() { // Tests the linearization of A - B. bool -test05() { +test06() { sstr store; fl_r_oc tmp; store[0] = tmp; @@ -222,7 +252,7 @@ test05() { // Tests the linearization of A * B where A = [0, 1] and B = [2, 2]. bool -test06() { +test07() { sstr store; fl_r_oc tmp(0); tmp.join_assign(1); @@ -251,7 +281,7 @@ test06() { // Tests the linearization of A / B where A = [1, 4] and B = [2, 2]. bool -test07() { +test08() { ddtr store; db_r_oc tmp(0); tmp.join_assign(1); @@ -280,7 +310,7 @@ test07() { // Tests the linearization of [1/4, 1/2] * (-A) where A = [1, 10]. bool -test08() { +test09() { sdtr store; fl_r_oc tmp(1); tmp.join_assign(10); @@ -307,6 +337,63 @@ test08() { return result == known_result; } +// Tests linearization of multiplication by unbounded operands. +bool +test10() { + float max_fl = std::numeric_limits<float>::max(); + fl_r_oc min_fl = fl_r_oc(-std::numeric_limits<float>::denorm_min()); + min_fl.join_assign(std::numeric_limits<float>::denorm_min()); + Float_Interval_Linear_Form known_result1 = + Float_Interval_Linear_Form(min_fl); + con_fpess* con1 = new con_fpess(0, 0); + con_fpess* con2 = new con_fpess(0, max_fl); + sum_fpess* sum = new sum_fpess(con1, con2); + con_fpess* con3 = new con_fpess(0, 0); + mul_fpess mul(con3, sum); + Float_Interval_Linear_Form result; + mul.linearize(sstr(), lsstr(), result); + + nout << "*** known_result1 ***" << endl + << known_result1 << endl; + bool ok1 = (known_result1 == result); + + double max_db = std::numeric_limits<double>::max(); + db_r_oc min_db = db_r_oc(-std::numeric_limits<double>::denorm_min()); + min_db.join_assign(std::numeric_limits<double>::denorm_min()); + Double_Interval_Linear_Form known_result2 = + Double_Interval_Linear_Form(min_db); + con_fpedd* con4 = new con_fpedd(0, 0); + con_fpedd* con5 = new con_fpedd(0, max_db); + sum_fpedd* sum2 = new sum_fpedd(con4, con5); + con_fpedd* con6 = new con_fpedd(0, 0); + mul_fpedd mul2(sum2, con6); + Double_Interval_Linear_Form result2; + mul2.linearize(ddtr(), lddtr(), result2); + + nout << "*** known_result2 ***" << endl + << known_result2 << endl; + bool ok2 = (known_result2 == result2); + + con_fpedd* con7 = new con_fpedd(0, 0); + con_fpedd* con8 = new con_fpedd(0, max_db); + sum_fpedd* sum3 = new sum_fpedd(con7, con8); + con_fpedd* con9 = new con_fpedd(0, 0); + con_fpedd* con10 = new con_fpedd(0, max_db); + sum_fpedd* sum4 = new sum_fpedd(con9, con10); + mul_fpedd mul3(sum3, sum4); + + bool ok3 = false; + try { + mul3.linearize(ddtr(), lddtr(), result2); + } + catch (Linearization_Failed e) { + nout << "*** Linearization failed due to overflow. ***" << endl; + ok3 = true; + } + + return ok1 && ok2 && ok3; +} + } // namespace BEGIN_MAIN @@ -318,4 +405,6 @@ BEGIN_MAIN DO_TEST(test06); DO_TEST(test07); DO_TEST(test08); + DO_TEST(test09); + DO_TEST(test10); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Fixed pedix.
by Fabio Bossi 08 Sep '09

08 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 2f3c39f2d78530507d9669db2f570ee90555124c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2f3c39f2d785… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 8 16:54:51 2009 +0200 Fixed pedix. --- doc/definitions.dox | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index c2f1eb9..8aba517 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2658,7 +2658,7 @@ floating point variable with its currently known approximation. The store is composed by two parts: - an interval abstract store \f$\fund{\rho}{\cV}{\mathbb{I}_a}\f$ associating each variable with its current approximating interval, and - - a linear form abstract store \f$\fund{\rho}{\cV}{\mathbb{L}_a}\f$ + - a linear form abstract store \f$\fund{\rho_l}{\cV}{\mathbb{L}_a}\f$ associating each variable with its current approximating linear form. Both stores are represented by maps of the Standard Template Library and are

1 0

[GIT] ppl/ppl(floating_point): Fixed an error in command invocation.
by Fabio Bossi 08 Sep '09

08 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 994b555a8cd9a79d9f8303b32209998b8830c13a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=994b555a8cd9… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 8 16:46:23 2009 +0200 Fixed an error in command invocation. --- doc/definitions.dox | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index 4da0008..c2f1eb9 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2656,9 +2656,9 @@ forms on \f$\mathbb{F}_a\f$ by \f$\mathbb{L}_a\f$. A (composite) floating point abstract store is used to associate each floating point variable with its currently known approximation. The store is composed by two parts: - - an interval abstract store \f$\fund{\rho,\cV,\mathbb{I}_a}\f$ + - an interval abstract store \f$\fund{\rho}{\cV}{\mathbb{I}_a}\f$ associating each variable with its current approximating interval, and - - a linear form abstract store \f$\fund{\rho,\cV,\mathbb{L}_a}\f$ + - a linear form abstract store \f$\fund{\rho}{\cV}{\mathbb{L}_a}\f$ associating each variable with its current approximating linear form. Both stores are represented by maps of the Standard Template Library and are

1 0

[GIT] ppl/ppl(floating_point): Added some documentation.
by Fabio Bossi 08 Sep '09

08 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 4a1d25bd5a05e759dcc4d1f6a0b9f1204435bda7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4a1d25bd5a05… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 8 16:29:40 2009 +0200 Added some documentation. --- doc/definitions.dox | 71 +++++++++++++++++++++++++++++++++++++++++++++++++++ doc/ppl.sty | 1 - 2 files changed, 71 insertions(+), 1 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index ff19299..4da0008 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2594,6 +2594,77 @@ to see that the widening operator is actually compatible with a given convergence certificate. If such a requirement is not met, then an extrapolation operator will be obtained. +\section floating_point Analysis of floating point computations + +This section describes the PPL abstract domains that are used for +approximating floating point computations in software analysis. We follow +the approch described in \ref Min04 "[Min04]" and more detailedly in +\ref Min05 "[Min05]". We will denote by \f$\cV\f$ the set of all floating +point variables in the analyzed program. We will also denote by +\f$\mathbb{F}_a\f$ the set of floating point numbers in the format used by the +analyzer (that is, the machine running the PPL) and by \f$\mathbb{F}_t\f$ +the set of floating point numbers in the format used by the machine that is +expected to run the analyzed program. Recall that floating point numbers +include the infinities \f$-\infty\f$ and \f$+\infty\f$. + +\subsection interval_linear_forms Linear forms with interval coefficients + +Generic concrete floating point expressions on \f$\mathbb{F}_t\f$ are +represented by the \link Parma_Polyhedra_Library::Floating_Point_Expression +\c Floating_Point_Expression \endlink abstract class. Its concrete derivate +classes are: + - \link Parma_Polyhedra_Library::Constant_Floating_Point_Expression \c + Constant_Floating_Point_Expression \endlink, + - \link Parma_Polyhedra_Library::Variable_Floating_Point_Expression \c + Variable_Floating_Point_Expression \endlink, + - \link Parma_Polyhedra_Library::Opposite_Floating_Point_Expression \c + Variable_Floating_Point_Expression \endlink, that is the negation + (unary minus) of a floating point expression, + - \link Parma_Polyhedra_Library::Sum_Floating_Point_Expression \c + Sum_Floating_Point_Expression \endlink, that is the sum of two floating + point expressions, + - \link Parma_Polyhedra_Library::Difference_Floating_Point_Expression \c + Difference_Floating_Point_Expression \endlink, that is the difference of + two floating point expressions, + - \link Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression \c + Multiplication_Floating_Point_Expression \endlink, that is the product of + two floating point expressions, and + - \link Parma_Polyhedra_Library::Division_Floating_Point_Expression \c + Division_Floating_Point_Expression \endlink, that is the division of + two floating point expressions. + +The set of all the possible values in \f$\mathbb{F}_t\f$ of a floating point +expression at a given program point in a given abstract store can be +overapproximated by a linear form with interval coefficients, that is +a linear expression of this kind: + +\f[ + i + \sum_{v \in \cV}i_{v}v, +\f] + +where all \f$v\f$ are free floating point variables and \f$i\f$ and all +\f$i_{v}\f$ are elements of \f$\mathbb{I}_a\f$, defined as the set of all +intervals with boundaries in \f$\mathbb{F}_a\f$. This operation is called +linearization and is performed by the method linearize of floating +point expression classes. + +Even though the intervals may be open, we will always use closed intervals +in the documentation for the sake of simplicity, with the exception of unbounded +intervals that have \f$\infty\f$ boundaries. We denote the set of all linear +forms on \f$\mathbb{F}_a\f$ by \f$\mathbb{L}_a\f$. + +A (composite) floating point abstract store is used to associate each +floating point variable with its currently known approximation. The store is +composed by two parts: + - an interval abstract store \f$\fund{\rho,\cV,\mathbb{I}_a}\f$ + associating each variable with its current approximating interval, and + - a linear form abstract store \f$\fund{\rho,\cV,\mathbb{L}_a}\f$ + associating each variable with its current approximating linear form. + +Both stores are represented by maps of the Standard Template Library and are +needed for performing linearization. Please see the documentation of floating +point expression classes for more information. + \section use_of_library Using the Library \subsection A_Note_on_the_Implementation_of_the_Operators A Note on the Implementation of the Operators diff --git a/doc/ppl.sty b/doc/ppl.sty index 0015104..87b3207 100644 --- a/doc/ppl.sty +++ b/doc/ppl.sty @@ -191,4 +191,3 @@ \newcommand*{\adlf}{\boxminus^{\#}_{\mathbf{f}}} \newcommand*{\adivlf}{\boxslash^{\#}_{\mathbf{f}}} \newcommand*{\amlf}{\boxtimes^{\#}_{\mathbf{f}}} -

1 0

[GIT] ppl/ppl(floating_point): Update variale and constant documentations
by Fabio Biselli 08 Sep '09

08 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 606ec45118cc8866cff182d49498fb641eb44c95 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=606ec45118cc… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Tue Sep 8 16:59:35 2009 +0200 Update variale and constant documentations --- src/Constant_Floating_Point_Expression.defs.hh | 20 +++++++++++++------- src/Variable_Floating_Point_Expression.defs.hh | 18 +++++++++++------- 2 files changed, 24 insertions(+), 14 deletions(-) diff --git a/src/Constant_Floating_Point_Expression.defs.hh b/src/Constant_Floating_Point_Expression.defs.hh index 0ddfbbf..6fd3ee1 100644 --- a/src/Constant_Floating_Point_Expression.defs.hh +++ b/src/Constant_Floating_Point_Expression.defs.hh @@ -43,8 +43,10 @@ void swap(Parma_Polyhedra_Library::Constant_Floating_Point_Expression< namespace Parma_Polyhedra_Library { -//! A generic Constant Floating Point Expression -/*! \ingroup PPL_CXX_interface +/*! \brief + A generic Constant Floating Point Expression. + + \ingroup PPL_CXX_interface \par Template type parameters @@ -109,11 +111,15 @@ public: // FIXME: Modify documentation when exceptions are fixed. /*! \brief - Modifies a linear form \p result in the abstract store \p store - corresponding to an inhomogenous term which over-approximates - *this.value. - \param store The abstract store. - \param result The linear form that will be modified. + Linearizes the expression in a given astract state. + + Modifies a linear form \p result in the abstract store \p store + corresponding to an inhomogenous term which over-approximates + *this.value. + + \param int_store Interval floating-point store. + \param lf_store Linear form store. + \param result The modified linear form. \exception Parma_Polyhedra_Library::Linearization_Failed Thrown if the method <CODE>linearize</CODE> fails. diff --git a/src/Variable_Floating_Point_Expression.defs.hh b/src/Variable_Floating_Point_Expression.defs.hh index cb1c300..bffb35b 100644 --- a/src/Variable_Floating_Point_Expression.defs.hh +++ b/src/Variable_Floating_Point_Expression.defs.hh @@ -43,8 +43,10 @@ void swap(Parma_Polyhedra_Library::Variable_Floating_Point_Expression< namespace Parma_Polyhedra_Library { -//! A generic Variable Floating Point Expression -/*! \ingroup PPL_CXX_interface +/*! \brief + A generic Variable Floating Point Expression. + +\ingroup PPL_CXX_interface \par Template type parameters @@ -106,13 +108,15 @@ public: //@} // Constructors and Destructor - //! Linearization of a variable. /*! \brief - Modifies a linear form \p result in the abstract store \p store - corresponding to <CODE>this</CODE> variable with coefficent \f$[1,1]\f$. + Linearization of a variable. + + Modifies a linear form \p result in the abstract store \p store + corresponding to <CODE>this</CODE> variable with coefficent \f$[1,1]\f$. - \param store The abstract store. - \param result The linear form that will be modified. + \param int_store Interval floating-point store. + \param lf_store Linear form store. + \param result The modfied linear form. */ void linearize(const FP_Interval_Abstract_Store& int_store, const FP_Linear_Form_Abstract_Store& lf_store,

1 0