1 /* Utilities for termination analysis: declarations. 2 Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it> 3 Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com) 4 5 This file is part of the Parma Polyhedra Library (PPL). 6 7 The PPL is free software; you can redistribute it and/or modify it 8 under the terms of the GNU General Public License as published by the 9 Free Software Foundation; either version 3 of the License, or (at your 10 option) any later version. 11 12 The PPL is distributed in the hope that it will be useful, but WITHOUT 13 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or 14 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License 15 for more details. 16 17 You should have received a copy of the GNU General Public License 18 along with this program; if not, write to the Free Software Foundation, 19 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. 20 21 For the most up-to-date information see the Parma Polyhedra Library 22 site: http://bugseng.com/products/ppl/ . */ 23 24 #ifndef PPL_termination_defs_hh 25 #define PPL_termination_defs_hh 1 26 27 #include "termination_types.hh" 28 29 #include "Generator_types.hh" 30 #include "C_Polyhedron_types.hh" 31 #include "NNC_Polyhedron_types.hh" 32 #include "Constraint_System_types.hh" 33 34 namespace Parma_Polyhedra_Library { 35 36 class Termination_Helpers { 37 public: 38 static void 39 all_affine_ranking_functions_PR(const Constraint_System& cs_before, 40 const Constraint_System& cs_after, 41 NNC_Polyhedron& mu_space); 42 static bool 43 one_affine_ranking_function_PR(const Constraint_System& cs_before, 44 const Constraint_System& cs_after, 45 Generator& mu); 46 static bool 47 one_affine_ranking_function_PR_original(const Constraint_System& cs, 48 Generator& mu); 49 static void 50 all_affine_ranking_functions_PR_original(const Constraint_System& cs, 51 NNC_Polyhedron& mu_space); 52 53 template <typename PSET> 54 static void 55 assign_all_inequalities_approximation(const PSET& pset_before, 56 const PSET& pset_after, 57 Constraint_System& cs); 58 }; // class Termination_Helpers 59 60 //! \name Functions for the Synthesis of Linear Rankings 61 //@{ 62 63 /*! \ingroup PPL_CXX_interface \brief 64 Termination test using an improvement of the method by Mesnard and 65 Serebrenik \ref BMPZ10 "[BMPZ10]". 66 67 \tparam PSET 68 Any pointset supported by the PPL that provides the 69 <CODE>minimized_constraints()</CODE> method. 70 71 \param pset 72 A pointset approximating the behavior of a loop whose termination 73 is being analyzed. The variables indices are allocated as follows: 74 - \f$ x'_1, \ldots, x'_n \f$ go onto space dimensions 75 \f$ 0, \ldots, n-1 \f$, 76 - \f$ x_1, \ldots, x_n \f$ go onto space dimensions 77 \f$ n, \ldots, 2n-1 \f$, 78 . 79 where unprimed variables represent the values of the loop-relevant 80 program variables before the update performed in the loop body, 81 and primed variables represent the values of those program variables 82 after the update. 83 84 \return 85 <CODE>true</CODE> if any loop approximated by \p pset definitely 86 terminates; <CODE>false</CODE> if the test is inconclusive. 87 However, if \p pset <EM>precisely</EM> characterizes the effect 88 of the loop body onto the loop-relevant program variables, 89 then <CODE>true</CODE> is returned <EM>if and only if</EM> 90 the loop terminates. 91 */ 92 template <typename PSET> 93 bool 94 termination_test_MS(const PSET& pset); 95 96 /*! \ingroup PPL_CXX_interface \brief 97 Termination test using an improvement of the method by Mesnard and 98 Serebrenik \ref BMPZ10 "[BMPZ10]". 99 100 \tparam PSET 101 Any pointset supported by the PPL that provides the 102 <CODE>minimized_constraints()</CODE> method. 103 104 \param pset_before 105 A pointset approximating the values of loop-relevant variables 106 <EM>before</EM> the update performed in the loop body that is being 107 analyzed. The variables indices are allocated as follows: 108 - \f$ x_1, \ldots, x_n \f$ go onto space dimensions 109 \f$ 0, \ldots, n-1 \f$. 110 111 \param pset_after 112 A pointset approximating the values of loop-relevant variables 113 <EM>after</EM> the update performed in the loop body that is being 114 analyzed. The variables indices are allocated as follows: 115 - \f$ x'_1, \ldots, x'_n \f$ go onto space dimensions 116 \f$ 0, \ldots, n-1 \f$, 117 - \f$ x_1, \ldots, x_n \f$ go onto space dimensions 118 \f$ n, \ldots, 2n-1 \f$, 119 120 Note that unprimed variables represent the values of the loop-relevant 121 program variables before the update performed in the loop body, 122 and primed variables represent the values of those program variables 123 after the update. Note also that unprimed variables are assigned 124 to different space dimensions in \p pset_before and \p pset_after. 125 126 \return 127 <CODE>true</CODE> if any loop approximated by \p pset definitely 128 terminates; <CODE>false</CODE> if the test is inconclusive. 129 However, if \p pset_before and \p pset_after <EM>precisely</EM> 130 characterize the effect of the loop body onto the loop-relevant 131 program variables, then <CODE>true</CODE> is returned 132 <EM>if and only if</EM> the loop terminates. 133 */ 134 template <typename PSET> 135 bool 136 termination_test_MS_2(const PSET& pset_before, const PSET& pset_after); 137 138 /*! \ingroup PPL_CXX_interface \brief 139 Termination test with witness ranking function using an improvement 140 of the method by Mesnard and Serebrenik \ref BMPZ10 "[BMPZ10]". 141 142 \tparam PSET 143 Any pointset supported by the PPL that provides the 144 <CODE>minimized_constraints()</CODE> method. 145 146 \param pset 147 A pointset approximating the behavior of a loop whose termination 148 is being analyzed. The variables indices are allocated as follows: 149 - \f$ x'_1, \ldots, x'_n \f$ go onto space dimensions 150 \f$ 0, \ldots, n-1 \f$, 151 - \f$ x_1, \ldots, x_n \f$ go onto space dimensions 152 \f$ n, \ldots, 2n-1 \f$, 153 . 154 where unprimed variables represent the values of the loop-relevant 155 program variables before the update performed in the loop body, 156 and primed variables represent the values of those program variables 157 after the update. 158 159 \param mu 160 When <CODE>true</CODE> is returned, this is assigned a point 161 of space dimension \f$ n+1 \f$ encoding one (not further specified) 162 affine ranking function for the loop being analyzed. 163 The ranking function is of the form \f$ \mu_0 + \sum_{i=1}^n \mu_i x_i \f$ 164 where \f$ \mu_0, \mu_1, \ldots, \mu_n \f$ are the coefficients 165 of \p mu corresponding to the space dimensions \f$ n, 0, \ldots, n-1 \f$, 166 respectively. 167 168 \return 169 <CODE>true</CODE> if any loop approximated by \p pset definitely 170 terminates; <CODE>false</CODE> if the test is inconclusive. 171 However, if \p pset <EM>precisely</EM> characterizes the effect 172 of the loop body onto the loop-relevant program variables, 173 then <CODE>true</CODE> is returned <EM>if and only if</EM> 174 the loop terminates. 175 */ 176 template <typename PSET> 177 bool 178 one_affine_ranking_function_MS(const PSET& pset, Generator& mu); 179 180 /*! \ingroup PPL_CXX_interface \brief 181 Termination test with witness ranking function using an improvement 182 of the method by Mesnard and Serebrenik \ref BMPZ10 "[BMPZ10]". 183 184 \tparam PSET 185 Any pointset supported by the PPL that provides the 186 <CODE>minimized_constraints()</CODE> method. 187 188 \param pset_before 189 A pointset approximating the values of loop-relevant variables 190 <EM>before</EM> the update performed in the loop body that is being 191 analyzed. The variables indices are allocated as follows: 192 - \f$ x_1, \ldots, x_n \f$ go onto space dimensions 193 \f$ 0, \ldots, n-1 \f$. 194 195 \param pset_after 196 A pointset approximating the values of loop-relevant variables 197 <EM>after</EM> the update performed in the loop body that is being 198 analyzed. The variables indices are allocated as follows: 199 - \f$ x'_1, \ldots, x'_n \f$ go onto space dimensions 200 \f$ 0, \ldots, n-1 \f$, 201 - \f$ x_1, \ldots, x_n \f$ go onto space dimensions 202 \f$ n, \ldots, 2n-1 \f$, 203 204 Note that unprimed variables represent the values of the loop-relevant 205 program variables before the update performed in the loop body, 206 and primed variables represent the values of those program variables 207 after the update. Note also that unprimed variables are assigned 208 to different space dimensions in \p pset_before and \p pset_after. 209 210 \param mu 211 When <CODE>true</CODE> is returned, this is assigned a point 212 of space dimension \f$ n+1 \f$ encoding one (not further specified) 213 affine ranking function for the loop being analyzed. 214 The ranking function is of the form \f$ \mu_0 + \sum_{i=1}^n \mu_i x_i \f$ 215 where \f$ \mu_0, \mu_1, \ldots, \mu_n \f$ are the coefficients 216 of \p mu corresponding to the space dimensions \f$ n, 0, \ldots, n-1 \f$, 217 respectively. 218 219 \return 220 <CODE>true</CODE> if any loop approximated by \p pset definitely 221 terminates; <CODE>false</CODE> if the test is inconclusive. 222 However, if \p pset_before and \p pset_after <EM>precisely</EM> 223 characterize the effect of the loop body onto the loop-relevant 224 program variables, then <CODE>true</CODE> is returned 225 <EM>if and only if</EM> the loop terminates. 226 */ 227 template <typename PSET> 228 bool 229 one_affine_ranking_function_MS_2(const PSET& pset_before, 230 const PSET& pset_after, 231 Generator& mu); 232 233 /*! \ingroup PPL_CXX_interface \brief 234 Termination test with ranking function space using an improvement 235 of the method by Mesnard and Serebrenik \ref BMPZ10 "[BMPZ10]". 236 237 \tparam PSET 238 Any pointset supported by the PPL that provides the 239 <CODE>minimized_constraints()</CODE> method. 240 241 \param pset 242 A pointset approximating the behavior of a loop whose termination 243 is being analyzed. The variables indices are allocated as follows: 244 - \f$ x'_1, \ldots, x'_n \f$ go onto space dimensions 245 \f$ 0, \ldots, n-1 \f$, 246 - \f$ x_1, \ldots, x_n \f$ go onto space dimensions 247 \f$ n, \ldots, 2n-1 \f$, 248 . 249 where unprimed variables represent the values of the loop-relevant 250 program variables before the update performed in the loop body, 251 and primed variables represent the values of those program variables 252 after the update. 253 254 \param mu_space 255 This is assigned a closed polyhedron of space dimension \f$ n+1 \f$ 256 representing the space of all the affine ranking functions for the loops 257 that are precisely characterized by \p pset. 258 These ranking functions are of the form 259 \f$ \mu_0 + \sum_{i=1}^n \mu_i x_i \f$ 260 where \f$ \mu_0, \mu_1, \ldots, \mu_n \f$ identify any point of the 261 \p mu_space polyhedron. 262 The variables \f$ \mu_0, \mu_1, \ldots, \mu_n \f$ 263 correspond to the space dimensions of \p mu_space 264 \f$ n, 0, \ldots, n-1 \f$, respectively. 265 When \p mu_space is empty, it means that the test is inconclusive. 266 However, if \p pset <EM>precisely</EM> characterizes the effect 267 of the loop body onto the loop-relevant program variables, 268 then \p mu_space is empty <EM>if and only if</EM> 269 the loop does <EM>not</EM> terminate. 270 */ 271 template <typename PSET> 272 void 273 all_affine_ranking_functions_MS(const PSET& pset, C_Polyhedron& mu_space); 274 275 /*! \ingroup PPL_CXX_interface \brief 276 Termination test with ranking function space using an improvement 277 of the method by Mesnard and Serebrenik \ref BMPZ10 "[BMPZ10]". 278 279 \tparam PSET 280 Any pointset supported by the PPL that provides the 281 <CODE>minimized_constraints()</CODE> method. 282 283 \param pset_before 284 A pointset approximating the values of loop-relevant variables 285 <EM>before</EM> the update performed in the loop body that is being 286 analyzed. The variables indices are allocated as follows: 287 - \f$ x_1, \ldots, x_n \f$ go onto space dimensions 288 \f$ 0, \ldots, n-1 \f$. 289 290 \param pset_after 291 A pointset approximating the values of loop-relevant variables 292 <EM>after</EM> the update performed in the loop body that is being 293 analyzed. The variables indices are allocated as follows: 294 - \f$ x'_1, \ldots, x'_n \f$ go onto space dimensions 295 \f$ 0, \ldots, n-1 \f$, 296 - \f$ x_1, \ldots, x_n \f$ go onto space dimensions 297 \f$ n, \ldots, 2n-1 \f$, 298 299 Note that unprimed variables represent the values of the loop-relevant 300 program variables before the update performed in the loop body, 301 and primed variables represent the values of those program variables 302 after the update. Note also that unprimed variables are assigned 303 to different space dimensions in \p pset_before and \p pset_after. 304 305 \param mu_space 306 This is assigned a closed polyhedron of space dimension \f$ n+1 \f$ 307 representing the space of all the affine ranking functions for the loops 308 that are precisely characterized by \p pset. 309 These ranking functions are of the form 310 \f$ \mu_0 + \sum_{i=1}^n \mu_i x_i \f$ 311 where \f$ \mu_0, \mu_1, \ldots, \mu_n \f$ identify any point of the 312 \p mu_space polyhedron. 313 The variables \f$ \mu_0, \mu_1, \ldots, \mu_n \f$ 314 correspond to the space dimensions of \p mu_space 315 \f$ n, 0, \ldots, n-1 \f$, respectively. 316 When \p mu_space is empty, it means that the test is inconclusive. 317 However, if \p pset_before and \p pset_after <EM>precisely</EM> 318 characterize the effect of the loop body onto the loop-relevant 319 program variables, then \p mu_space is empty <EM>if and only if</EM> 320 the loop does <EM>not</EM> terminate. 321 */ 322 template <typename PSET> 323 void 324 all_affine_ranking_functions_MS_2(const PSET& pset_before, 325 const PSET& pset_after, 326 C_Polyhedron& mu_space); 327 328 /*! \ingroup PPL_CXX_interface \brief 329 Computes the spaces of affine \e quasi ranking functions 330 using an improvement of the method by Mesnard and Serebrenik 331 \ref BMPZ10 "[BMPZ10]". 332 333 \tparam PSET 334 Any pointset supported by the PPL that provides the 335 <CODE>minimized_constraints()</CODE> method. 336 337 \param pset 338 A pointset approximating the behavior of a loop whose termination 339 is being analyzed. The variables indices are allocated as follows: 340 - \f$ x'_1, \ldots, x'_n \f$ go onto space dimensions 341 \f$ 0, \ldots, n-1 \f$, 342 - \f$ x_1, \ldots, x_n \f$ go onto space dimensions 343 \f$ n, \ldots, 2n-1 \f$, 344 . 345 where unprimed variables represent the values of the loop-relevant 346 program variables before the update performed in the loop body, 347 and primed variables represent the values of those program variables 348 after the update. 349 350 \param decreasing_mu_space 351 This is assigned a closed polyhedron of space dimension \f$ n+1 \f$ 352 representing the space of all the decreasing affine functions 353 for the loops that are precisely characterized by \p pset. 354 355 \param bounded_mu_space 356 This is assigned a closed polyhedron of space dimension \f$ n+1 \f$ 357 representing the space of all the lower bounded affine functions 358 for the loops that are precisely characterized by \p pset. 359 360 These quasi-ranking functions are of the form 361 \f$ \mu_0 + \sum_{i=1}^n \mu_i x_i \f$ 362 where \f$ \mu_0, \mu_1, \ldots, \mu_n \f$ identify any point of the 363 \p decreasing_mu_space and \p bounded_mu_space polyhedrons. 364 The variables \f$ \mu_0, \mu_1, \ldots, \mu_n \f$ 365 correspond to the space dimensions \f$ n, 0, \ldots, n-1 \f$, respectively. 366 When \p decreasing_mu_space (resp., \p bounded_mu_space) is empty, 367 it means that the test is inconclusive. 368 However, if \p pset <EM>precisely</EM> characterizes the effect 369 of the loop body onto the loop-relevant program variables, 370 then \p decreasing_mu_space (resp., \p bounded_mu_space) will be empty 371 <EM>if and only if</EM> there is no decreasing (resp., lower bounded) 372 affine function, so that the loop does not terminate. 373 */ 374 template <typename PSET> 375 void 376 all_affine_quasi_ranking_functions_MS(const PSET& pset, 377 C_Polyhedron& decreasing_mu_space, 378 C_Polyhedron& bounded_mu_space); 379 380 /*! \ingroup PPL_CXX_interface \brief 381 Computes the spaces of affine \e quasi ranking functions 382 using an improvement of the method by Mesnard and Serebrenik 383 \ref BMPZ10 "[BMPZ10]". 384 385 \tparam PSET 386 Any pointset supported by the PPL that provides the 387 <CODE>minimized_constraints()</CODE> method. 388 389 \param pset_before 390 A pointset approximating the values of loop-relevant variables 391 <EM>before</EM> the update performed in the loop body that is being 392 analyzed. The variables indices are allocated as follows: 393 - \f$ x_1, \ldots, x_n \f$ go onto space dimensions 394 \f$ 0, \ldots, n-1 \f$. 395 396 \param pset_after 397 A pointset approximating the values of loop-relevant variables 398 <EM>after</EM> the update performed in the loop body that is being 399 analyzed. The variables indices are allocated as follows: 400 - \f$ x'_1, \ldots, x'_n \f$ go onto space dimensions 401 \f$ 0, \ldots, n-1 \f$, 402 - \f$ x_1, \ldots, x_n \f$ go onto space dimensions 403 \f$ n, \ldots, 2n-1 \f$, 404 405 Note that unprimed variables represent the values of the loop-relevant 406 program variables before the update performed in the loop body, 407 and primed variables represent the values of those program variables 408 after the update. Note also that unprimed variables are assigned 409 to different space dimensions in \p pset_before and \p pset_after. 410 411 \param decreasing_mu_space 412 This is assigned a closed polyhedron of space dimension \f$ n+1 \f$ 413 representing the space of all the decreasing affine functions 414 for the loops that are precisely characterized by \p pset. 415 416 \param bounded_mu_space 417 This is assigned a closed polyhedron of space dimension \f$ n+1 \f$ 418 representing the space of all the lower bounded affine functions 419 for the loops that are precisely characterized by \p pset. 420 421 These ranking functions are of the form 422 \f$ \mu_0 + \sum_{i=1}^n \mu_i x_i \f$ 423 where \f$ \mu_0, \mu_1, \ldots, \mu_n \f$ identify any point of the 424 \p decreasing_mu_space and \p bounded_mu_space polyhedrons. 425 The variables \f$ \mu_0, \mu_1, \ldots, \mu_n \f$ 426 correspond to the space dimensions \f$ n, 0, \ldots, n-1 \f$, respectively. 427 When \p decreasing_mu_space (resp., \p bounded_mu_space) is empty, 428 it means that the test is inconclusive. 429 However, if \p pset_before and \p pset_after <EM>precisely</EM> 430 characterize the effect of the loop body onto the loop-relevant 431 program variables, then \p decreasing_mu_space (resp., \p bounded_mu_space) 432 will be empty <EM>if and only if</EM> there is no decreasing 433 (resp., lower bounded) affine function, so that the loop does not terminate. 434 */ 435 template <typename PSET> 436 void 437 all_affine_quasi_ranking_functions_MS_2(const PSET& pset_before, 438 const PSET& pset_after, 439 C_Polyhedron& decreasing_mu_space, 440 C_Polyhedron& bounded_mu_space); 441 442 /*! \ingroup PPL_CXX_interface \brief 443 Like termination_test_MS() but using the method by Podelski and 444 Rybalchenko \ref BMPZ10 "[BMPZ10]". 445 */ 446 template <typename PSET> 447 bool 448 termination_test_PR(const PSET& pset); 449 450 /*! \ingroup PPL_CXX_interface \brief 451 Like termination_test_MS_2() but using an alternative formalization 452 of the method by Podelski and Rybalchenko \ref BMPZ10 "[BMPZ10]". 453 */ 454 template <typename PSET> 455 bool 456 termination_test_PR_2(const PSET& pset_before, const PSET& pset_after); 457 458 /*! \ingroup PPL_CXX_interface \brief 459 Like one_affine_ranking_function_MS() but using the method by Podelski 460 and Rybalchenko \ref BMPZ10 "[BMPZ10]". 461 */ 462 template <typename PSET> 463 bool 464 one_affine_ranking_function_PR(const PSET& pset, Generator& mu); 465 466 /*! \ingroup PPL_CXX_interface \brief 467 Like one_affine_ranking_function_MS_2() but using an alternative 468 formalization of the method by Podelski and Rybalchenko 469 \ref BMPZ10 "[BMPZ10]". 470 */ 471 template <typename PSET> 472 bool 473 one_affine_ranking_function_PR_2(const PSET& pset_before, 474 const PSET& pset_after, 475 Generator& mu); 476 477 /*! \ingroup PPL_CXX_interface \brief 478 Like all_affine_ranking_functions_MS() but using the method by Podelski 479 and Rybalchenko \ref BMPZ10 "[BMPZ10]". 480 */ 481 template <typename PSET> 482 void 483 all_affine_ranking_functions_PR(const PSET& pset, NNC_Polyhedron& mu_space); 484 485 /*! \ingroup PPL_CXX_interface \brief 486 Like all_affine_ranking_functions_MS_2() but using an alternative 487 formalization of the method by Podelski and Rybalchenko 488 \ref BMPZ10 "[BMPZ10]". 489 */ 490 template <typename PSET> 491 void 492 all_affine_ranking_functions_PR_2(const PSET& pset_before, 493 const PSET& pset_after, 494 NNC_Polyhedron& mu_space); 495 496 //@} // Functions for the Synthesis of Linear Rankings 497 498 } // namespace Parma_Polyhedra_Library 499 500 #include "termination_templates.hh" 501 502 #endif // !defined(PPL_termination_defs_hh) 503