1Change log 2========== 3 4v2021.09.29 5----------- 6 7User-facing changes 8~~~~~~~~~~~~~~~~~~~ 9* Nothing relevant. 10 11Internal changes 12~~~~~~~~~~~~~~~~ 13* Bug fix: build errors when compiling with shared libraries due to symbol 14 visibility have been fixed (commit c73e8a28870d37a44bf16a1bd3701edfe82a2521) 15 16v2021.08.28 17----------- 18 19User-facing changes 20~~~~~~~~~~~~~~~~~~~ 21* Bug fix: code generation of loop overflow checks was incorrect in a number of 22 cases. This has now been fixed (commits 23 c1e46b1267bd52cbb445466b2fa1aa7ccaca9a26, 24 a2a45efb689968de5440a1b419f070077f84d306, 25 9c898780ea30652f4beeb1e5694c4077ea972ba8, 26 27a9f27f35ca024ea0de1ae2038a4e66535043b0, 27 d69c6b51209c3e78eee4808c15501b0cbc325e5f, 28 2feee3e0382a561bdbdee1f0186de0db8e277e8e). 29* A new experimental binary, ``murphi2uclid``, is provided for translating 30 Murphi models to the `Uclid5 prover`_. 31* Syntax errors now refer to operators (e.g. ``>>``) rather than their internal 32 names (e.g. ``RSH``) (commit 7cf378f9711bbd19b4c4bdc648357b0043a57fc7). 33* GCC 4.7 and GCC 4.8 are no longer supported. If using GCC, the minimum 34 baseline is now GCC 4.9. An attempt will be made to not break compilation with 35 GCC 4.7 and 4.8, but no guarantee is provided going forwards (commits 36 201a7cab8d90b78696197c365d42d70998f16bd8, 37 517c2151e7a1923d6e625e7256e5da78d063ad6a). 38* The minimum required version of Python has been *decreased* from Python 3.6 to 39 Python 3.4 (commits 25cc3303434d048066c75e1242e8ef556c09c9e4, 40 0b68a69a702f1c7b518f425061c6657437e0c004, 41 b3288d12bd5d67e2ed5c23d30f0412ca0bcdda8c, 42 a27329276aa00c5e15ba9b1831c26c950412e68b, 43 162355d42b9dda960624548b4c95c0b9f8008af8). 44* The previously deprecated ``--smt-logic`` command line option has been removed 45 (commit bf5b076bbba95c1423e9a7c5a2b64b8ced55fb73). 46 47Internal changes 48~~~~~~~~~~~~~~~~ 49* Librumur now includes API functions for sanitising rule names to be 50 symbol-like. This can be useful for code generators that want to emit symbols 51 corresponding to rule names (commit 5d57a5a13a6f0c93e31bbddc4f22a066edb40658). 52* Copy constructors and assignment operators are now protected on AST node 53 classes (commit 45b27dbac7082e2b2dee85ee4ff7bb2f0c54d063). 54* Visibility of librumur symbols is now set via attributes. The ``RUMUR_API`` 55 macro may be used to override this if necessary (commits 56 53344ec86e3a71725039de282d4307ca9af25fc0, 57 c0cdc06024adb23f94409449266fe220f3094de9). 58* A previously deprecated ``Model`` constructor has been removed (commit 59 902e4389fca623a68c9c6fbfe298e5561a6aef04). 60 61.. _`Uclid5 prover`: https://github.com/uclid-org/uclid 62 63v2020.12.20 64----------- 65 66User-facing changes 67~~~~~~~~~~~~~~~~~~~ 68* Bug fix: a number of issues in ``murphi2c`` translation of ``put`` statements 69 have been fixed (commits 60c804a6cc5d04191788fc1756d1c9046cb09091, 70 0df3eb85f3932eb91c92c43d94d02e11a5846629, 71 4b7b5dfd3534aabd266fb3614b55d047526bae26, 72 652b50b7fc9f811ed206aa50398a5656acae0eef). 73* Bug fix: ``murphi2c`` no longer produces malformed code when referencing a 74 record field within an alias statement where an alias has the same name as the 75 field (commit 43f0dec2e112ff0adc05ab6267b8752e683d591d). 76* Bug fix: ``murphi2c`` no longer produces malformed code when referencing a 77 record field within a function with a var parameter with the same name as the 78 field (commit 074946937005c908cb7ace5ef65f3779d12420d2). 79* ``murphi2c`` makes a best effort to preserve comments during translation, 80 emitting these as C comments. 81* Translated ``put`` statements by ``murphi2c`` no longer print a trailing 82 newline (commit 338fa7b38a2e3224b76c095b54ef6dd869a6dd32). 83 84Internal changes 85~~~~~~~~~~~~~~~~ 86* A new API ``parse_comments()`` has been introduced for extracting the source 87 comments from a Murphi model. 88 89v2020.09.06 90----------- 91 92User-facing changes 93~~~~~~~~~~~~~~~~~~~ 94* Bug fix: when using XML output (``--output-format machine-readable``) error 95 messages no longer have their last character truncated (commit 96 6133e71b65c53cec050cdf5d40f735f2b9b3b525). 97* Bug fix: ``clock_gettim64()`` is now allowed within a sandboxed checker, 98 fixing sandboxing on armel, armhf, and mipsel (commit 99 68683c4742b380421936a703c4b9262dac1e68dc). 100* Bug fix: ``clock_gettime()`` is now allowed within a sandboxed checker, fixing 101 sandboxing on mips64el (commit af121b2a9bb7f7dcdd63fbc2716b314c408abf2c). 102* Declarations, functions/procedures, and rules no longer need to appear in this 103 precise order within a model. E.g. a constant declaration can now appear in 104 the middle of your model, after the definition of some functions. Expressions 105 can still only refer to entities that have been defined prior in the source 106 file (commits a77dc6d63e5f8bed9c39aa37209ec0b430aff67d, 107 c99b0a604d45bedc9a1d8680912371d0a76783b6, 108 d984fb9ad4bbedc8e99ded8aa3081bf4eba9a0ef, 109 40114146920f6bef44b84532f5ff6ed1f24dd454, 110 0a1dd7c6f476df1d7dcdd760722bff5343762609, 111 501e02d288532c32c236875977e65b99bdb3ebb1, 112 aa2a9a8774af651fe46410aee2405385c23c1a28, 113 2d712b5838c638b6e90e0e0e34529d62b16319db, 114 92ca08a13ba5c40fe459733d10ae1819fc9f0796, 115 67a01344ad7a197887bc59ad3726847a2f2f530b). 116* The Murphi AST XML format emitted by ``murphi2xml`` now allows declarations, 117 functions, procedures, and rules as direct children of ``model``. This new 118 alternative hierarchy is what ``murphi2xml`` now emits (commits 119 d984fb9ad4bbedc8e99ded8aa3081bf4eba9a0ef, 120 40114146920f6bef44b84532f5ff6ed1f24dd454). 121* ``rumur`` gained a new command line flag, ``--pointer-bits``, for indicating 122 how many low bits of a pointer on the target platform are meaningful. You can 123 use this to get extra memory optimisations through pointer compression. See 124 the manpage for more information (commit 125 bc90b807687ac20af9fd025a46493832977ec9aa). 126* On x86-64 Linux, ``rumur-run`` now auto-detects when your CPU does not support 127 5-level paging and enables pointer compression optimisations (commit 128 b34bf4f2843c60c916bdafb9a95ad901f2aad5de). 129* In debug output during checking, the initial printing of state variables and 130 their offsets now lists them in the order they appeared in the source file, 131 regardless of whether they were rearranged for efficiency (commit 132 a77dc6d63e5f8bed9c39aa37209ec0b430aff67d). 133* There are some minor white space changes to the C code emitted by ``murphi2c`` 134 (commit 40114146920f6bef44b84532f5ff6ed1f24dd454). 135 136Internal changes 137~~~~~~~~~~~~~~~~ 138* The ``Model`` constructor, ``Model::Model`` that takes four arguments has been 139 deprecated in favour of a new constructor that takes two arguments (commits 140 501e02d288532c32c236875977e65b99bdb3ebb1, 141 f375d67d929e789d22f9df882c23d774f4e60518). 142* The AST node members of ``Model`` have been removed in favour of a new unified 143 collection, ``Model::children`` (commits 144 c99b0a604d45bedc9a1d8680912371d0a76783b6, 145 0a1dd7c6f476df1d7dcdd760722bff5343762609). 146 147v2020.07.28 148----------- 149 150User-facing changes 151~~~~~~~~~~~~~~~~~~~ 152* The permutations applied when shuffling scalarsets are now tracked and later 153 used to reconstruct symbolic scalarset values for counterexample traces and 154 print statements. The effect is that counterexample traces now make more 155 intuitive sense because symmetry reduction does not interfere with 156 interpreting scalarset values. This behaviour is controllable via the 157 ``--scalarset-schedules`` command line option. See the manpage for more 158 information. 159 160Internal changes 161~~~~~~~~~~~~~~~~ 162* ``Symtab::is_global_scope()`` which was previously deprecated has now been 163 removed (commit 7959973ce9345d16718a16b741d754c5e64bbc9e). 164 165v2020.07.11 166----------- 167 168User-facing changes 169~~~~~~~~~~~~~~~~~~~ 170* Bug fix: using ``&`` or ``|`` within a ``return`` statement would erroneously 171 cause the error “cannot retrieve the type of an unresolved '&' expression.” 172 This has now been corrected (commit 54c79e090a8bd5eb3939f15742e0c45d0c09187e). 173* Bug fix: similar to the above, this error would also occur when using ``&`` or 174 ``|`` within a right shift, ``>>``. This has now been corrected (commit 175 65f4d0d85ab1a1de530c9751a8a4af4b2da4b6b5). 176* Bug fix: similar to the above two items, this error would also occur when 177 using ``&`` or ``|`` within range bounds. This has now been corrected (commit 178 72d2ef5b7c12803af2d1102a11321cc19a77dd55). 179* Bug fix: defining an alias within an ``aliasrule`` whose target was another 180 alias previously defined in the same rule would result in generated code that 181 would not compile. This has now been corrected (commit 182 30408bde597f774330748309633e547f98041e0e). 183* Bug fix: During verification, certain shift operations would erroneously 184 return 0 on some platforms. These now return the correct value (commit 185 e065dcdda6d5d263b95a101ab2e353aed9e49c9f). 186* Printing an array within a model (using a ``put`` statement) results in more 187 efficient generated code (commit b2edcd1ae8408da6c647b7fa7698c2d37c2b8b73). 188 189Internal changes 190~~~~~~~~~~~~~~~~ 191* ``Node::operator==`` which was previously deprecated has now been removed 192 (commit df26837f4fea6a7da7fa24858ce3383367e33e82). 193 194v2020.06.20 195----------- 196 197User-facing changes 198~~~~~~~~~~~~~~~~~~~ 199* Bug fix: State variable offsets are now updated after reordering. Previously 200 this could cause erroneous reads or writes during checking (commit 201 3d8e551bf1c4873d570dc0a8adac7f52c0b9ea25). 202* Bug fix: fields within records are now reordered universally. Previously 203 inconsistencies could occur resulting in a record’s fields appearing in 204 differing orders across references to the same type (commits 205 cf03554574c7fd2fa78d461fbae95b97624b6f78, 206 8b74668d28cdc73718c7e5b8234c9a138456d3ce). 207* In light of bugs like the above two, there is a new command line argument, 208 ``--reorder-fields`` to control whether field reordering is enabled. This can 209 be used to turn it off in case further bugs are encountered. See the ``rumur`` 210 manpage for details (commit 9a33888f2303a3d1bf0e9339a2fddc4570945b02). 211* ``rumur-run`` now preferences the ``rumur`` binary in the same directory as 212 itself, ahead of any ``rumur`` binary in your ``$PATH`` (commit 213 1f03555f89090e7de3e07dc5677380017a3762e9). 214 215Internal changes 216~~~~~~~~~~~~~~~~ 217* Nothing relevant. 218 219v2020.05.27 220----------- 221 222User-facing changes 223~~~~~~~~~~~~~~~~~~~ 224* Bug fix: rumur-run’s check for whether libatomic is required is now more 225 accurate. Previously this would incorrectly detect that libatomic was not 226 required on some platforms (e.g. Linux ARM64), resulting in a link failure 227 (commit 620e514c1d322e05a9e67bb09cd0dc68cb810d38). 228 229Internal changes 230~~~~~~~~~~~~~~~~ 231* Nothing relevant. 232 233v2020.05.18 234----------- 235 236User-facing changes 237~~~~~~~~~~~~~~~~~~~ 238* Various bitwise operators are now supported in the input syntax. See 239 `doc/bitwise-operators.rst`_ for details. 240* Some more verbose messages are now printed when passing ``--debug`` to rumur 241 (commit 7f52532280054e32b1be72f44d0f4180d1a2dc86). 242* Progress output lines during verification are now skipped when there is heavy 243 contention on access to stdout. This reduces runtime bottlenecks in highly 244 multithreaded verifications (commit 4d47d9a9abf8882935011d20950c50fe75460657). 245 246Internal changes 247~~~~~~~~~~~~~~~~ 248* The variant of ``parse()`` that accepted a stream pointer was previously 249 deprecated and has now been removed. Clients should call the variant that 250 accepts a reference instead (commit dcabb240eeb7d505f673879c2ba68fbbb5d3fd96). 251 252.. _`doc/bitwise-operators.rst`: ./doc/bitwise-operators.rst 253 254v2020.04.26 255----------- 256 257User-facing changes 258~~~~~~~~~~~~~~~~~~~ 259* Bug fix: value type calculation (which C type to use for scalar values during 260 checking) now correctly assesses ``:= ... to ...`` for ranges. Previously the 261 presence of one of these expressions in the input model would pessimise the 262 calculation into selecting ``int64_t`` even if a narrower type would be 263 acceptable (commit 371fbc37047088c7f964dfdeedea2420cae46b1c). 264* Record field ordering and model variable ordering is now optimised for runtime 265 performance during checking (commit 2cb30e7c675d08837c26e0e204fa9f8457c40053). 266 267Internal changes 268~~~~~~~~~~~~~~~~ 269* ``IsUndefined`` now inherits from ``UnaryExpr`` (commit 270 523a021e059382e6fa76afab7bfa011638332360). 271 272v2020.04.05 273----------- 274 275User-facing changes 276~~~~~~~~~~~~~~~~~~~ 277* Bug fix: murphi2c should no longer confuse multiple enum types within a model 278 when generating its C output (commit 279 34b66de87e17909538ff25e6c090791d1738f1f6). 280* Bug fix: murphi2c now reports its name correctly in its ``--version`` output 281 instead of referring to Rumur (commit 282 8cf120cff76e1d58425be553b2a333c8c23482d9). 283* A new binary, murphi2murphi, has been added that serves as a preprocessor or 284 source-to-source translator for Murphi models. See its man page or ``--help`` 285 for more information. 286 287Internal changes 288~~~~~~~~~~~~~~~~ 289* A new API function, ``Expr::is_pure()`` has been added for determining whether 290 an expression is side-effect free (commit 291 499151975b8f6b25829e1bf2605943ab5e1832e0). 292* ``TypeExpr::equatable_with()`` that was previously deprecated, has been 293 removed. Clients should call ``TypeExpr::coerces_to()`` instead (commit 294 f7fc46cb7de8ead4ea840d249ae7ff0689e35abe). 295 296v2020.03.12 297----------- 298 299User-facing changes 300~~~~~~~~~~~~~~~~~~~ 301* Bug fix: ``time()`` and ``gettimeofday()`` are now permitted when generating a 302 sandboxed verifier on Linux. These were supposed to be allowed previously but 303 there was a typo when initially adding this. This is only relevant for Linux 304 platforms that do not implement these system calls in vDSO_ (commit 305 6cce8fe23796e459bb98021ccc172ba139745f46). 306* A new binary, murphi2c, has been added that translates a Murphi model into C 307 code suitable for integration into a C/C++ simulator. See its man page or 308 ``--help`` for more information. 309* A minor typo was corrected in the murphi2xml man page (commit 310 75dcef20a57ff939bf789bc98f6f2bd037fd1629). 311 312Internal changes 313~~~~~~~~~~~~~~~~ 314* ``VarDecl::state_variable`` that was previously deprecated, has been removed. 315 Clients should call ``VarDecl::is_in_state()`` as a replacement (commit 316 1776a4c6968e3c98861665af398bd042e435c096). 317* XCode < 8.3.3 is no longer supported as a development environment under macOS. 318 Users are recommended to upgrade to a newer version of XCode/macOS. 319 320v2020.02.17 321----------- 322 323User-facing changes 324~~~~~~~~~~~~~~~~~~~ 325* Bug fix: several latent bugs in the verifier’s state writing code have been 326 fixed. These only affected large scalar types (> 49-bit) which were not known 327 to be used in any existing real world models (commits 328 2d27f8b97aa2d24caf217a97a6df7de11e70b1b4, 329 7bbf8498c42ca8f19a059acc8169be2559b81427, 330 fa87b0a361b1f7dd9fc436c063ffa5a1d4529ee6, 331 5b4d7154902d8474f6d0233e5af9f3bd85b0a628, 332 410fdbe533c3597bc2029f63e0426f56250c52bf). 333* The ``rumur-ast-dump`` utility has been renamed to ``murphi2xml`` to more 334 obviously indicate its purpose (commit 335 d5cb6a6f88498e9d8c999540f66cc838ffe1707a). 336* When generating a sandboxed verifier (``--sandbox on``), some further 337 time-related system calls are now allowed. This allows the verifier to run 338 correctly on platforms that do not have these system calls implemented in 339 vDSO_ (commits 3ee7d3d3c2f4f35d86b59b6de7139feae8763b4c, 340 498853681c25272e23cf480c6c8d7269f23a974c). 341* The verifier’s state reading and writing functions now anticipate that the 342 host platform may be big endian. Full big endian support will require further 343 changes, but this is a first step (commit 344 8f7bb60c1bc82638dd4ed5f2248c44cd47436461). 345 346.. _vDSO: https://en.wikipedia.org/wiki/VDSO 347 348Internal changes 349~~~~~~~~~~~~~~~~ 350* Nothing relevant. 351 352v2020.01.27 353----------- 354 355User-facing changes 356~~~~~~~~~~~~~~~~~~~ 357* Bug fix: quantified expressions no longer result in malformed SMT problems in 358 the SMT simplification bridge. This previously prevented some optimisation 359 that could have otherwise occurred (commit 360 2a1b724d25817b1bf9f95932ed8a4f9bb65a2af9). 361* Bug fix: pointer compression is no longer incorrectly enabled when targeting 362 the x32 ABI on Linux. This would cause assertion failures or invalid memory 363 references on this platform (commit 37cfa28ad640757eb42d4e394974ad2630987089). 364* ``forall`` and ``exists`` expressions are now supported by the SMT bridge. The 365 only remaining unsupported expressions are function calls and ``isundefined`` 366 (commits 49a0d0df8d5ea67b1c26b549929f6eea361b879e, 367 5bb6144f684a905df44aa5955a8d04b37739e65c, 368 5b4e5e52e4bba0fb7ea03cb63d210701c5f3bc65, 369 5d4038c3933592b060203bda3e94b259a9ba9f43). 370* ``rumur-run`` now automatically detects whether your C compiler supports the 371 ``-mcx16`` flag and whether the checker needs to link against libatomic 372 (commits 6547e8b5022522732421ff337ab5113a19afb44a, 373 f7958a3fdad6a280360903108de5f05837fa1e5f). 374* Some compiler warnings on Linux on ARMEL have been suppressed (commit 375 b56cd94c6af0153dbdb983b8fd4177fc041526c8). 376 377Internal changes 378~~~~~~~~~~~~~~~~ 379* ``Model::assumption_count()`` which was previously deprecated has been removed 380 (commit ce2fe9d30db11dbce337355924986af48ee8878d). 381* ``Symtab::is_global_scope()`` has been deprecated and will be removed in a 382 future release (commit 7943b55ab80e0ecf3563158a2ff7b8100d60ca78). 383 384v2020.01.11 385----------- 386 387User-facing changes 388~~~~~~~~~~~~~~~~~~~ 389* Bug fix: negative literals no longer cause malformed problems to be sent to 390 the SMT bridge (commit 47f0207dcaee6909d59ddc5577f92b3bf97571b2). 391 392Internal changes 393~~~~~~~~~~~~~~~~ 394* Bug fix: a missing header is now shipped (commit 395 8cf196c3548962b15488abe293b4891740da4da0). 396 397v2020.01.07 398----------- 399 400User-facing changes 401~~~~~~~~~~~~~~~~~~~ 402* Bug fix: compile errors in the generated verifier on Linux on ARM and RISC-V 403 due to references to missing syscalls in the sandboxing code have been fixed 404 (commit f1af745c54346f74ec650b192e708234de603b58). 405* Bug fix: the syscalls ``fstat64()`` and ``mmap2()`` are allowed within the 406 verifier’s sandbox on Linux on i386, removing a spurious runtime error (commit 407 047f23b32e2510af15dd4021a3a63941a909d13f). 408* The state data structure in the generated verifier is now more aggressively 409 packed, leading to reduced memory usage during checking. The runtime speed of 410 the checker may be slightly degraded. However, see the next item (commits 411 c17f056efcb5d3ef0cbd2160df3762a29ee90530, 412 db0e25f04d9140242643f7c5ebf8b8e9fbc62d82, 413 3c8ba379e44085e772ada03c8607aac95be2ef30, 414 ae6d776609de0462601f9beb75a8c93ce718f658, 415 50cff5aef32fa02f096bb7fc161a93f10b829124, 416 299be2fab2588b3367e8dd3406c8c9c0f591ebc6, 417 46d495f31c202298aef9f9dcd6638295df3f3e88, 418 c423db32f4c34db11d671d4e9078a4211a237630, 419 c6a040344ef4415e1983bd67dec6bb146b020d5a, 420 f6df17322a787d268c5ba8e587070649533b82c5, 421 a30665fb0b71040c99a19201e37ff9946b77a628, 422 77b97767661d17bff8b70d42b03ac63ba28c1da6, 423 654156b1bde6cc8d9dd613053d20de70587827cc, 424 77c8a12a6d6293de89670d0cbc6c4dc05c6ca9f3, 425 1b3383e3d2064826f67d211890011d651bfae88d, 426 cff8c6c938cf9b491f136dcb31072d1fe8dcc00c). 427* ``rumur`` has a new command line option, ``--pack-state``, for controlling 428 the trade off between memory reduction and runtime speed in the generated 429 verifier. See the manpage for more information (commit 430 aca06ba25db9a6a8e6311c8eaec015750371b772). 431* ``rumur-run`` no longer uses the compiler flags ``-march=native`` and 432 ``-mtune=native`` if they are not supported. This is primarily relevant to 433 non-x86 platforms whose toolchains do not all have these options (commit 434 1dd341e29dd7033b1d7598af8af899c322880a50). 435* ``rumur-run`` passes toolchain flags to link against libatomic on 436 architectures that do not have a double-word compare-exchange instruction 437 (MIPS, PowerPC, s390, RISC-V). This causes queue operations that are lock-free 438 on other architectures to take a global mutex, but it seems not easily 439 avoidable (commit 4cd3ffef193e2a87d1dd58a642ebaf93541b70ab). 440* ``rumur-run`` now uses `Link-Time Optimisation`_ if it is supported (commit 441 0adcb633ec56b476505e22fa47126437f9665671). 442* Various minor performance improvements were made to the generated verifier 443 (commits 5af91bf0dfe0d8bef9f7045f5ae5692a179e9ca3, 444 dee407613c0b1fd0c7ab851c6f84cbcb184dbea4, 445 b517be6b83b5c17f97ab82bda448e62ecded9688, 446 fe49bea9af67f71763227e95009441438433522a, 447 fd04cb9c1b3f432cb35f66d6cfe0b0726ad84068). 448 449Internal changes 450~~~~~~~~~~~~~~~~ 451* ``validate_model()`` which was previously deprecated has been removed (commit 452 ba3a70ce8902c9baecdc94505f7c71d7dba6dca3). 453* ``Node::operator==`` and ``Node::operator!=`` have been deprecated and should 454 no longer be called. There is not a consistent notion of AST node equality and 455 these functions only implemented an approximation. They will be removed in a 456 future release (commits 019dbe9c4b2fdf24f8cf16028e73e6105e3336fe, 457 489947c7e3a01ae256d467565688eded2564f34e). 458* New functions, ``Expr::is_literal_true()`` and ``Expr::is_literal_false()`` 459 have been introduced for determining if an expression is the literal value 460 ``true`` or ``false``, respectively (commit 461 bd084b982b6f209ec2356bb56f69dc0622b9345b). 462* A new function, ``TypeExpr::is_boolean()`` has been introduced for determining 463 if a type is the built-in ``Boolean`` (commit 464 f4ad5d02161da0b6f2d5264b6a9db482c392e77e). 465* Some documentation on the use of C atomic APIs has been added in 466 doc/internals-atomics.rst (commits 85602619752cb8b173a0821bb7afe2a8c301f0e1, 467 7fb1f0266beafd58e7bf7f859204b0ce61f35b28). 468* Liveness is now documented as something beyond what is supported by CMurphi in 469 doc/vs-cmurphi.rst (commit 5c82890e2a11ccb5da5e155faba8c7b9c26544d5). 470 471.. _`Link-Time Optimisation`: https://en.wikipedia.org/wiki/Interprocedural_optimization#WPO_and_LTO 472 473v2019.12.22 474----------- 475 476User-facing changes 477~~~~~~~~~~~~~~~~~~~ 478* Bug fix: ``rumur-run`` no longer crashes during UTF-8 decoding in generated C 479 code (commit 7bbd50f6a7241475826e8d380b6a60bb3c6dfd18). 480* Support for Python 2 in ``rumur-run`` has been dropped. To use this script you 481 will now need at least Python 3.6 (commits 482 0c4d5f05ebcc937921edd924465827e50d345842, 483 ded15a4d8f23f1f1584566bd6e251679ba8f915c). 484* The final check of liveness properties now prints regular progress updates 485 (commits ce162be56035e726e1077bb6b6ecc89999e8607e, 486 2635dae9a4f27962f4ed951a54b3d6c54b9d62c6, 487 44e80dc6142205904dca188d2a0277b49ed0fb7f, 488 048a4b54fa7a1c2a7f48fdb8a7e470d396529200, 489 eef60ad5cf61d1a8cac2d1dbcf63581da2590e24). 490 491Internal changes 492~~~~~~~~~~~~~~~~ 493* Support for Python 2 in all scripts has been dropped. These now require at 494 least Python 3.6 (commits 5ad77dc6de53de9a78639faba5b65668e43c3ad8, 495 729a7f8a096369115bde345890bc14e03c5bd428, 496 6e0d248eae25a8a68b04bb5e99a3172e1e2ab453, 497 244b41225d36309f9e5985dbe594957782bef7fb). 498 499v2019.11.24 500----------- 501 502User-facing changes 503~~~~~~~~~~~~~~~~~~~ 504* ``rumur`` has a new command line option ``--smt-bitvectors`` for controlling 505 whether bitvectors are used in preference to integers when interacting with 506 SMT solvers. See the man page for more information (commits 507 37c84bbe255d3a7aa6d234a8334379edbb24ec3c, 508 9821bedfa4cdadda8cf1b9f065c07813854ea7d1). 509* ``rumur`` has a new command line option ``--smt-prelude`` for prepending text 510 to problems sent to SMT solvers. The ``--smt-logic`` command line option is 511 now deprecated and ``--smt-prelude`` should be used to set the logic instead. 512 See the man page for more information (commit 513 ad022eb0767250734562ec1ec932ef4d99ec1f5d). 514* The ``rumur`` option ``--smt-simplification`` is now automatically enabled if 515 you pass any of the other SMT related command line options (commit 516 39482d62009232477f18c7e5e295c633004e7b82). 517* A new tracing feature for memory usage in the generated checker has been 518 added, ``--trace memory_usage``. See the man page for how to use this (commit 519 4f9195707ae261ed4f6f94d1411579751deff618). 520* ``rumur-ast-dump`` now has a ``--version`` option to print out its version 521 (commit 76716edc76fbe608a013b0178b6e4d2d72614d08). 522* Some warnings when compiling generated code with recent versions of Clang have 523 been suppressed (commit 3e9efb2855be52c20023ef3cd03e02b183e22ff5). 524 525Internal changes 526~~~~~~~~~~~~~~~~ 527* A new ``version()`` function has been added to librumur for retrieving its 528 version as a string (commits 77ee1c40884627e5418e3c25f902c6d7d73f5f4f, 529 7f95b7491859548b27ec7d9226d7c28cdec380c0). 530 531v2019.11.09 532----------- 533 534User-facing changes 535~~~~~~~~~~~~~~~~~~~ 536* Bug fix: returning an expression of range type within a function with a return 537 type of a differing range is now accepted. This pattern was previously 538 rejected by ``rumur`` claiming the types were incompatible (commit 539 2279e30e74983c8288d097979f31ffecd25b9b4f). 540* Bug fix: the filename in the AST dump produced by ``rumur-ast-dump`` is now 541 XML-escaped. Previously characters like ``<`` were incorrectly printed as-is 542 (commit cec7f83ac781554a99e9018cef6a0285f67c8955). 543* ``rumur-ast-dump`` now shows source content in its output even when the input 544 model was supplied on stdin. Previously source content was only included if 545 the input came from an on-disk file (commits 546 ff36e8fec7750a921d4bdc57c509ca7d12fde8cb, 547 6fbc34e9a6cbee0e8c9f09c9b8dc5796fd3d2aaa, 548 8fc052d0c3d034ed057ec69aa3ebab95b60234b7). 549* ``rumur-ast-dump`` now gives the filename in its output as “<stdin>” when the 550 input model is supplied on stdin instead of omitting it. The ``filename`` 551 attribute of the head ``unit`` tag in the dump has now become mandatory 552 (commit f20463f3e00f5ae2de9871b6b24f83f7799ff4d2). 553 554Internal changes 555~~~~~~~~~~~~~~~~ 556* ``rumur::parse()`` now takes its argument as a reference instead of a pointer. 557 The old implementation remains for backwards compatibility but it is 558 deprecated (commit 947ae70c647a955ea6e24b651a6feead64bac787). 559 560v2019.10.27 561----------- 562 563User-facing changes 564~~~~~~~~~~~~~~~~~~~ 565* Bug fix: several problems with code generation related to statements of the 566 form ``for x := i to j by k ...`` have been fixed. Rumur now supports 567 arbitrary expressions for any of ``i``, ``j``, and ``k``, including reverse 568 (down-counting) loops (commits 569 1186e622868c124b21637f7ddb5f35f818b18f3b, 570 8b73384edfceb8c6f55dffdb1ae8d9952b5c8adb, 571 245887647ac4bfbf08685f97c99c0c84b581e8f8, 572 b7078e9b17fb572ff7126aa42930d3dd50a4577b, 573 df4264e5f72d7e4528211e74444512d58dd32048). 574* Bug fix: quantified variables are taken into account when calculating range 575 limits for values of simple type (commits 576 e4746dc130d3f69bf623bed503b88b0ba109b176, 577 3e0ac51a379a2b5612b6d72e3e286955f143e525). 578* Bug fix: overriding the automatically chosen value type (using 579 ``--value-type ...``) can no longer cause an assertion failure in the 580 generated checker. Forcing a value type that is too small previously violated 581 an assumption in the generated code. This now causes a runtime error (commit 582 77729447d3cfbb523e3a4a79654eb0a1b5fbd8e8). 583* Bug fix: the initial pool size of the arena allocator in the generated code 584 was being miscalculated and has now been corrected to approximate 8MB (commit 585 381f08975e2a0a70cd0a2210a9af12b374580075). 586* Bug fix: the SMT bridge now correctly detects a failure to start the child 587 process. The check for this was previously incorrect and it would look as if 588 the SMT solver malfunctioned (commit 589 d1cbfd41d3051d548186acf1f17acd85df7f96d8). 590* Blank (``""``) and unknown logics are now supported by the SMT bridge. Solvers 591 such as Z3 function best when given no ``set-logic`` command (commit 592 6c92a15f33da3804aaaba628ecc8450ac2fde13d). 593* The default SMT logic is now ``AUFLIA`` (commit 594 03ab27d04eccc18c142db7364f7000bf67c12a7f). 595* Some GCC warnings when compiling generated code have been suppressed (commit 596 bae9b849a781f97e690c8e52196512150aeae4ab). 597 598Internal changes 599~~~~~~~~~~~~~~~~ 600* Bug fix: Unresolved ``TypeExprIDs`` with differing names are now considered 601 unequal (commit 7fe656c7db5f2578db826ea1a39a200ece93f57f). 602* ``TypeExpr::equatable_with`` is deprecated, and replaced by 603 ``TypeExpr::coerces_to`` (commits aa1557bf044e62c8f3adaaca591fe272b30ca19a, 604 e45f214cd2097bbe710a2a3eed9ed196e9feace8, 605 befe6bb4a9b9c342ad3a7a8b96a8bff94c47319d). 606* ``Quantifier`` has a new member, ``decl``, that is a ``VarDecl`` for the 607 variable it represents (commits c079a460749b1b8e7ea9dd627d369fe3395aa204, 608 4aba73cb86885531a56228a145ad2529cf5fe2a0). 609* Quantifier expressions — the bounds of the quantifier — are now validated in 610 ``Quantifier::validate()`` (commit 1b7cd5aad63c8b3e55a266facb8100752946a59d). 611* The type of a ``TypeExprID`` that refers to a quantified variable is now a 612 persistent, valid ``VarDecl``. Previously it was a synthetic declaration with 613 an invalid ``unique_id`` (commit c567645c4778cbb33d9f696450e9c9c13f12896b). 614 615v2019.09.15 616----------- 617 618User-facing changes 619~~~~~~~~~~~~~~~~~~~ 620* Bug fix: an alias of a constant is now correctly recognised as constant 621 itself. This makes it possible to, for example, use such an alias as the lower 622 or upper bound of an integer range (commit 623 e4d139880498cfe140ae3298985c615d44f3930d). 624* The SMT bridge supports variable and type shadowing. For example, if your 625 model has a rule with a local variable with the same name as something in the 626 global state. Such models would previously cause malformed SMT problems to be 627 passed to the solver (commits 628 b2d5c1566530fa009c06b1c2710617b71f7c8c57, 629 4f5611986b12cbafa9663f1dd7b31f33d3211d25, 630 7b1718259185ff3e5ceabbb34fca41028da12010). 631* Smart quotes (“ and ”) can now be used as string delimiters in models (commit 632 82db1716e7b18259b00ea1941163c4808513793c). 633* Using an SMT logic without array support (for example, ``--smt-logic QF_LIA``) 634 suppresses SMT simplification in models with arrays. Previously this would 635 cause a malformed problem to be passed to the solver (commit 636 1100fae5b5c629b2d3e1f7dc386906ae16d7bd5a). 637 638Internal changes 639~~~~~~~~~~~~~~~~ 640* Breaking change: ``TypeExprID::referent`` is now a ``TypeDecl`` instead of a 641 ``TypeExpr``. The ``TypeExpr`` that would previously be stored here is 642 available via ``referent->value`` (commit 643 117ae412d6aa863f54d25fa87106265cced7f680). 644* A new method ``Function::is_pure`` is available for determining whether a 645 function is side effect free (commits 646 455acdc883a7080ad764524a7d22e8bf056c9e09, 647 ef5eb689d81bf96c183ad6f74a754eab47229095). 648 649v2019.09.07 650----------- 651 652User-facing changes 653~~~~~~~~~~~~~~~~~~~ 654* The SMT bridge now supports record types. This makes SMT simplification 655 (``--smt-simplification on``) realistically usable on real world models. 656 Simplification will still give up on some unsupported expressions (commits 657 787f074328874a470d595576ae9e8b16837582f4, 658 33d120df8fc7bedf1361a59f328930d311478376, 659 308a8239eee6dc42684c3bed21210ea95d0dd66e, 660 b9dd7f185d6f22c31d98dfbeb2af4418fb661b79, 661 13092b8d8c5e62da0178b71825328cc7e75bea5b). 662* Recursive functions and procedures are now supported. These are supported by 663 CMurphi, Rumur's precursor, but seemingly rarely used in real world models so 664 their absence in Rumur went unnoticed until recently. Mutual recursion is 665 still unsupported (commits e61b8a787ab46bde3c0ce14da885cd3005cc54c9, 666 a9bd211028e591d90e28e2410f5988700bc5efcd). 667* ``rumur-ast-dump --help`` now shows its manpage instead of abbreviated help 668 text (commits 4198edc67ed37c3dfa91031f90fdfb9e8a5190aa, 669 8cf86df9ef718d1e22d1ba47a63c9f1a6ba1ad78, 670 295b565f88660ecf4264ad1ace4e6f88423fab69, 671 8c612b898e9d42a17847cca3a9435fc575c58135, 672 577ae2862a45a1d89fe995c1a9bd7bb11fc7e34d, 673 38a61d670d748d7072162e506c873afa13e757ec). 674* Function or procedure parameters that shadow a return type are now supported. 675 Previously Rumur would reject such models (commit 676 ff5bbb8cd7a016fbe210757dd1c4b90093c44b4d). E.g.: 677 678.. code-block:: murphi 679 680 type t: 0 .. 1; 681 682 function foo(t: boolean): t; begin 683 ... 684 685* It is now valid to name two rules identically in a model. This can lead to 686 confusing counterexample traces, but sometimes it is natural to name multiple 687 rules the same so supporting this seemed reasonable (commit 688 a1d419c4d70f99d0945164e708ddd90379ddc858). 689 690Internal changes 691~~~~~~~~~~~~~~~~ 692* A new interface, ``Function::is_recursive()``, is available for querying 693 whether a function calls itself (commit 694 de4cd48cc2ff64b8ba8eb41163ea45fd1676658c). 695 696v2019.08.18 697----------- 698 699User-facing changes 700~~~~~~~~~~~~~~~~~~~ 701* Bug fix: Boolean literals (``false`` and ``true``) are now supported by the 702 SMT bridge. These previously led to a malformed SMT problem (commit 703 0c9917b87523db07b604c566e2f8e3481872857b). 704* Array types are now supported by the SMT bridge. The bridge is still of 705 limited use as there are many constructs it cannot handle, but it improves 706 incrementally (commits 424467a264b923c53a1b1738604630a05457315c, 707 5d4f1939ddc5d5d9336f0ce35e953c51e8b5aeca, 708 5e07b5527a910d12be558d665110a7809838360c). 709* The default logic for the SMT bridge has been changed to QF_ALIA. As before, 710 this is controllable via the ``--smt-logic`` command line option (commit 711 dc81631881a16764d55dea834ae39d8715b13e83). 712* Some compiler warnings in the generated verifier have been suppressed (commits 713 e60db38a76b2cd1ce169ad17b442b5285ee83b4c, 714 ef5dd68576dc37d109e2370c653f1a6286042f78, 715 a657bb19ae4ce589e64b217823b0e2c49b8b282e). 716 717Internal changes 718~~~~~~~~~~~~~~~~ 719* Nothing relevant. 720 721v2019.07.21 722----------- 723 724User-facing changes 725~~~~~~~~~~~~~~~~~~~ 726* Bug fix: quantified ranges that span 0 (e.g. ``-1 .. 1``) now iterate 727 correctly. Previously such loops would become no-ops which could cause the 728 verifier to incorrectly not explore some states. This bug was introduced in 729 v2019.04.28 (commit 2329056db14d87301bba9c56115cdd4539bed1af). 730* Bug fix: models that contain assume statements but no top level assumptions no 731 longer segfault. This bug was introduced in v2019.05.11 (commits 732 eab626a859982d55b2ebfae8ca216ce79aec25ee, 733 d4ae6d2c88cf0ca5a4e2a4f1f94b375d1405b2a5, 734 ad79600751bb017ff8f85ef34e2747924c0e6eca, 735 0fd8636f2eca1ed6d90545ab3ee91f4ebae1da85). 736* Bug fix: the file descriptors used to communicate with the SMT bridge were 737 being configured incorrectly. This caused inconsistent behaviour across 738 different Libc implementations. This bug was introduced in v2019.06.30. Thanks 739 to @wangqr for reporting this (commit 740 53f20cc00398eefd81a7a1d015517d3051b23548). 741* The dialect used to communicate with SMT solvers was backported from SMTLIB 742 2.5 to SMTLIB 2.0. This enables support for more diverse solvers (commit 743 e0e9c5d46c8c2192d6c70987de2a1d50889dc3fd). 744* There is a new option for specifying the logic in which to encode SMT problems 745 for the external solver, ``--smt-logic``. See the manpage for more information 746 (commits e6b76b518439c0667de0b4b575ec18e5e6994705, 747 6ba664c341f5796a99a7b4623f424ad4f33c9852, 748 07ff7f7df1f4e8473f4e5f63dc0654009abb18db). 749* The SMT bridge learned to understand type-declared ranges/scalarsets, integer 750 constants and enum types. It is still of limited use 751 because it does not understand records or arrays, but support for these will 752 arrive in future (commits c38a0f1188924622e716abbc4dcee924cb10ce52, 753 33ce2be1adf8c0922ea6fa7594ad9c783df35e20, 754 7d0146ead2cf30b15ed515beb3c56dd1da8464a8, 755 ca07c576bb272193c1177790c359b5984f636180). 756* The SMT bridge has increased support for division when using CVC4 (commit 757 e55c4c1b274dfd8797f71f49209d2e0e5eb799d7). 758* Some inconsistency in the XML output when using 759 ``--output-format machine-readable`` was corrected (commit 760 22a0c59054563116f6210a886dd538bdfd7cd90a). 761* Some ``-Wsign-compare`` warnings when compiling the verifier have been 762 suppressed (commits d2949e3516c613f6183ce3219d403e4b3e96add9, 763 1a7342956115a691118b315bf8ea1cb551f718f9). 764 765Internal changes 766~~~~~~~~~~~~~~~~ 767* ``Model::assumption_count()`` has been deprecated (commit 768 99529844092fcbe1bbbfb3170c7b9a8364a6d055). 769* ``VarDecl::state_variable`` has been deprecated (commits 770 39bf6a2661bb6a296fbd73d9f466f052c4865477, 771 175193b6e0a920f016545008796a99ec3a588bfa, 772 6a4f9ac363b8c90beac7d5b5ddacc152f5e329d4). 773* A RelaxNG schema is now included for the XML output of the verifier (commit 774 123e2507ddf6694ddb7d2bb1baf654e467f28e23). 775* The validation API has been extended and now also descends into referents. The 776 function ``validate_model()`` has been deprecated (commits 777 860f71d1db91e71bcab60a8fc8097ad37d3895a0, 778 499857ec7ab25886be5c4a76802889cb1fc034f8, 779 5d2449ac780c39cb72f21a03b498c766607fabb7, 780 45f095c97174b96df5612d0c762283f7187ba0f7). 781* The data members of referents (e.g. ``ExprID::value``) now have accurate 782 values. This avoids confusion as users can now access these and rely on 783 getting the same, e.g., ``offset`` as the target (commits 784 7268f636cd9187c30f6bc990abef8e4b493b0534, 785 c3d23559c40b1504bb1a284f76303891fafae23f). 786 787v2019.06.30 788----------- 789 790User-facing changes 791~~~~~~~~~~~~~~~~~~~ 792* Bug fix: duplicated semi-colons are now ignored. For example, an empty 793 statement no longer causes a syntax error (commit 794 7e0a3eeff15707e6a67515acd499dce9e598d9ee). 795* Rumur gained some rudimentary ability to interact with an SMT solver. See the 796 manpage or ``rumur --help`` for information on how to use this functionality. 797 This simplification performed via SMT will incrementally improve in future 798 releases. (commits 45f56b3d06759bd9a0e6343334b5fa2bf2161f2a, 799 1c75eefb8c9c1b3e1e543cefd992b91066929081, 800 0f8c1aa01f5ec517d4186ab8f65b81872dcc4374, 801 9aa75f12adc38efd7a107c90f659ca4d98e8d925, 802 dce3565a8d059e480efd34ff35c5d43134eed607, 803 4a0b72a25318e642a4648dbcb1082068f7c20354, 804 4bf443d4a1eb4f069998109f8f4e9380ad35ef6c, 805 c66061ffa216e291a325e3a33cb55fd6d911960b, 806 c32ed61d1b51439e760558712c5c3de5e8cc2a4c). 807 808Internal changes 809~~~~~~~~~~~~~~~~ 810* A new member of ``VarDecl`` has been added for determining whether a variable 811 declaration is part of the global state or not (commit 812 80e6154c748b3cbd36c3b9fb9e1164447e85246f). 813* ``True`` and ``False`` constants are available to use for comparison or 814 cloning when working with the librumur AST (commit 815 dcb3559fbe03014bdf353649f390fc368b7e813c). 816 817v2019.06.12 818----------- 819 820User-facing changes 821~~~~~~~~~~~~~~~~~~~ 822* Bug fix: an unlikely edge case was possible wherein the results of checking 823 could be reported inaccurately if one thread was exiting while other threads 824 decided to expand the seen state set. This was never seen in the wild, but has 825 been corrected in this release anyway (commit 826 8cf9d785c925554e6ec4b2a8a55e619f3ecc66f2). 827* The generated verifier no longer requires linking against libatomic on i386 828 platforms. This change means FreeBSD on i386 is now supported (commit 829 0da98254af604a4812201b8f06dc885dcebb9787). 830 831Internal changes 832~~~~~~~~~~~~~~~~ 833* Rumur now compiles correctly on platforms where ``size_t`` is not 834 ``unsigned long``. Thanks to Yuri Victorovich for reporting this (commit 835 38489a811f0abc4aaaf6f6425dd6321325f959a0). 836 837v2019.06.05 838----------- 839 840User-facing changes 841~~~~~~~~~~~~~~~~~~~ 842* Bug fix: when generating XML output from the verifier 843 (``--output-format machine-readable``) some text within error messages was not 844 correctly escaped, leading to invalid XML. This has now been corrected 845 (commit ca97a1eb90ac667f3e5f32b41ccbb59940804516). 846* Bug fix: FreeBSD compatibility which had been accidentally broken was 847 restored. Thanks to Yuri Victorovich for reporting this (commit 848 43054e83417e028c48b18739f6ac7916cfcbac47). 849 850Internal changes 851~~~~~~~~~~~~~~~~ 852* Bug fix: the test suite should now run successfully in a non-UTF-8 locale. As 853 for the above entry, thanks to Yuri Victorovich for reporting this (commits 854 a88c8d2faf2b003e2b65af26cc42b2bcdd82e819, 855 a9e327cd43f94ea22129244f514261ea3880eedb). 856 857v2019.06.01 858----------- 859 860User-facing changes 861~~~~~~~~~~~~~~~~~~~ 862* Bug fix: the output message for a syntax error on a line containing a tab 863 character previously indicated the wrong column offset with the underlining 864 caret. This has now been corrected (commit 865 323fda58984e1768b659298afddc5c022160c428). 866* ``rumur-run`` now exits cleanly and cleans up temporary directories when you 867 terminate it with Ctrl-C (commit 9acb49fd46d8eeddd59104d48621aa1a3c71cd34). 868* The default load factor of the seen state set has been changed from 65% to 869 75%. On most models, this decreases the runtime of the verifier. As before, it 870 is still possible to change this value with the ``--set-expand-threshold`` 871 command line option (commit 8ac5bf762d744fc68d8e64918fc7af120b4fc3c7). 872 873Internal changes 874~~~~~~~~~~~~~~~~ 875* The documentation available under doc/ has been extended (commits 876 63e0db1b8d67529e3f042e1b1ed7ffd65ca78cab, 877 49e8c6a857ba8f9b46d3cf36bb702268d7e822da, 878 f39447766ba43ccf2f218370d6a644024a3e1215, 879 ba0521cfcd2b30d19a125b319ade63775505c73f). 880 881v2019.05.11 882----------- 883 884User-facing changes 885~~~~~~~~~~~~~~~~~~~ 886* Bug fix: Counterexample traces using "diff" mode (the default) now correctly 887 only show the value of a variable if it has changed compared to the previous 888 state. Previously variables whose values did not change were sometimes 889 repeated (commit 94ef1dec8a82d643dba459d97af3870c9e325528). 890* Bug fix: Running with counterexample traces disabled 891 (``--counterexample-trace off``) is repaired. Previously this would result in 892 generated code that did not compile (commits 893 f78335f5d72c3fa5b4565103697c678ef62379cf, 894 58b7ac310caa008d57af71039080095c801956a2). 895* Bug fix: negative literals are taken into account when determining a type to 896 represent scalars. Previously Rumur would fail to notice that something like 897 ``-1`` in your model implied that values could be negative, and it might have 898 inferred that an unsigned type like ``uint8_t`` was suitable to store this in 899 (commit 2b27e22f00354080589815416b7796d06b37fb6c). 900* Bug fix: Using ``--max-errors`` with a value greater than ``1`` produces safe 901 code. Previously this would emit a call to ``sigsetjmp`` with live 902 non-volatile local variables. The result could lead to memory corruption or 903 an inaccurate fired rules count, but neither of these were observed in the 904 wild (commit 7dda120345da13f739427915fde630d71bae9ff5). 905* Bug fix: some spurious ``-Wtype-limits`` and ``-Wtautological-compare`` 906 warnings when building the generated verifier have been suppressed (commit 907 d82f251210560df694f03a6d8b6c5c2cbbe04886). 908* The concept of disabled properties has been removed. This feature was never 909 documented and had no use yet, so its removal is unlikely to affect any users 910 (commit 4e30098aee291414b5108936548218657fb47900). 911 912Internal changes 913~~~~~~~~~~~~~~~~ 914* Some spurious ``-Wsign-compare`` warnings when using older GCC versions have 915 been suppressed (commit 25847dca93e45a3b0616c9f2bd254eae1738f7a1). 916* The documentation available under doc/ has been extended (commits 917 5a56d259bf2b9e039ed18a4b48861b48083e730e, 918 7ab3e74ae2a63809ee657ea981cb2d9ae0da3fb4, 919 b6e8ed7c4c4818aa13d7ec24cc3f7fb40f1d9842, 920 d76467f065585a2cbc5f4f237ea20fb367140c26) 921 922v2019.04.28 923----------- 924 925User-facing changes 926~~~~~~~~~~~~~~~~~~~ 927* Bug fix: enum types that are printed in error messages now correctly have 928 their members separated by a comma and a space (commit 929 1107d95909bdd9df019f55f1208c857de5db7239). 930* Bug fix: one case where the size of the seen set was incorrectly read 931 non-atomically has been fixed. This would only have affected platforms where 932 naturally aligned reads are not already atomic (e.g. not x86). The result 933 would have been a rare chance of a miscalculation of when to expand the seen 934 set. (commit 02d2803ecb6a459a1a41f7d1c630d1b84d6d75ff). 935* Syntax error messages now provide more information about what token the lexer 936 was expecting to see (commit 06dfee962cb3541fcedf2f319ca4504f90ee0514). 937* Instead of unconditionally using ``int64_t`` to represent scalar values in the 938 generated verifier, the fastest type that can contain all scalar values in 939 your model is used. You can override automatic selection with the new 940 ``--value-type`` command line argument. This change has no immediate benefit 941 but it opens the way to optimisations using Single Instruction Multiple Data 942 (SIMD) or even SIMD Within A Register (SWAR). (commits 943 0a5129fb89358ea67ecc32fb07b1d768f655223e, 944 0933edbb4831c5fc9e483e865b202a6609090b54, 945 f5c8cc54a8a02338a62985aaf2190d7f5fc79ca0, 946 2fde1dbf0fff5c3776fb77e7468a2e83693a444b, 947 6d20e571685f18cdb2d9bf6dd77c615ce1ab5385, 948 e98a3d0041d64dd331a16e45897e9c3a789e0235, 949 f9a29ea64cccbc41155b689d80ea6eb3be9189e9, 950 c95df7007b48a89df981eec037679dd3cb87dab5, 951 5b33f977a55a4bd370aefea205548b1b0bf887d9, 952 5e5945535ff60ed01501d2b10282220b96b009bc, 953 5e1ee6dbe6e784516a1171996bb442e9936e426b, 954 79579fd5ee7cc3c120439b5d3187a09ffd5dcd6e). 955 956Internal changes 957~~~~~~~~~~~~~~~~ 958* Nothing relevant. 959 960v2019.04.13 961----------- 962 963User-facing changes 964~~~~~~~~~~~~~~~~~~~ 965* Bug fix: malicious models can no longer cause bad printf format strings to 966 be generated (commits 6b30d43f6672278db0c0d7c8dfd5dbe83785fad5, 967 a27c2391ede24c0833b045d0d4a138ecb829434b, 968 322d1e26b343cdc308efb50ce2d952bb26ad9ad8). 969* Bug fix: characters in text like rule names are no longer dropped when using 970 XML output (commit f119f745218ed9404f6922e95aa6076bc0bdf291). 971* Bug fix: unnamed invariants are now correctly numbered when they are referred 972 to (commit 450a2e7b9ced7f670eaf568e9ba484ea43a2dcb4). 973* Bug fix: with deadlock detection enabled (default) and multiple errors 974 (``--max-errors ...`` with a value > 1), deadlock counterexamples are no 975 longer duplicated in the error output (commit 976 17ebb307b68cb323ad0840903b96070ea1b6ca0a). 977* New syntax has been added for writing liveness properties. See 978 doc/properties.rst for how to use this (commits 979 e99fa1104ff578106075f6dc19c35b4ef2f7d986, 980 ee1aecd172edb9fa5be775548841e38c4aa547b0, 981 36fae15066562eedee594fa1fd77e60af19e13bd, 982 4c6ee24bc922955f419c05391fa1ddc49cbc122e, 983 53f80d8565af4217bfe11ac2bfe549d9b2ada0af, 984 b094269cfe516bad7bd3ab0993288ff7f3a8285a, 985 6ed296f61b7b942323974a7d40c2b20f7003ff26, 986 ac54ed1cef5326260128d189a3705679a3ba02aa, 987 85cbc94ac9b734572874d3564d9a4240f10614f9). 988* Support for macOS has been extended back to XCode 7.3 (commit 989 35e1803b370f8a47df84812eab19bbb01dcf4e41). 990 991Internal changes 992~~~~~~~~~~~~~~~~ 993* The test case tweak snippets (``-- ...`` Python comments at the beginning of 994 test cases) can now refer to whether XML output is in use or not (commit 995 af393a106773c98b79f283f02e250ec9ca9a73a5). 996* Using the ``-- checker_output: ...`` test case tweak no longer limits a test 997 case to running when XML output is not in use (commit 998 af393a106773c98b79f283f02e250ec9ca9a73a5). 999* There is a new API function for counting the liveness properties in a model 1000 (commit ee1aecd172edb9fa5be775548841e38c4aa547b0). 1001* The build dependency on ``xxd`` (bundled with Vim) has been removed (commits 1002 a8575179f9a5c956be5bb50c182bbb89f1d8d057, 1003 6b907684c4d7696acf6f9ea2a2ca566e5175da18, 1004 43759055bf873814ec18cb692ee9a6d9d6889d1a). 1005 1006v2019.03.30 1007----------- 1008 1009User-facing changes 1010~~~~~~~~~~~~~~~~~~~ 1011* Bug fix: an error when compiling the generated verifier on non-x86-64 was 1012 addressed (commit 7e59f1c25a71fd6c3444fc11adc6f932b32ce926). 1013* Bug fix: the Vim syntax extensions were missing the ``property`` keyword which 1014 has now been added (commit 9e70f6114899ca04556c3cdeb198928a65ab19fc). 1015* Errors when generating the verifier are now printed showing the relevant 1016 source line from the model. They are also colourised Clang-style when possible 1017 (commit e7f2b615cb432bf8fab55d3a00225f3b26e8d8d9). 1018* Support for sandboxing the generated verifier has been extended from Linux and 1019 macOS to include FreeBSD (using Capsicum) and OpenBSD (using ``pledge``) 1020 (commits b73b180dd7fedb2795f19e8a065eefe429f1177e, 1021 cb53074aaa1c898c6c0a3d6e962597b9c77c3785). 1022* Expansion of the set of seen states has been optimised, resulting in a ~4% 1023 decrease in the runtime of the verifier. This change reduced contention, so 1024 likely leads to greater speed ups on large, multicore platforms (commits 1025 022c3708b24b828a96f3a50c0f11c7cc1476a439, 1026 5f4bb2cd96660a48518680f992fee041566ac722, 1027 2e84387ec6f56c42f41ea21e17ba99eef501ab65, 1028 5b29f2c4cb96989ba862a19acfcae0912a19f86c, 1029 9287f5af063a430e83c8957d9f7282d1af33d6ba). 1030 1031Internal changes 1032~~~~~~~~~~~~~~~~ 1033* Nothing relevant. 1034 1035v2019.03.21 1036----------- 1037 1038User-facing changes 1039~~~~~~~~~~~~~~~~~~~ 1040* A new bounded model checking mode is available using the command line option 1041 ``--bound``. See the manpage or ``--help`` for more detailed information 1042 (commit e60697531ab636d374946d547ae65cd380b2ce0b). 1043* The names of quantifier variables are now included in the XML produced by 1044 ``rumur-ast-dump`` (commit 78539fa086bbdaf06c5a079e5e482637cf6f2e11). 1045* Some optimisation has been done to state handles, resulting in a ~9% decrease 1046 in the runtime of the generated verifier (commits 1047 d783655eae837b805b69185d1d198ea142825973, 1048 96268246ad3c9635998647fb31faf73e6721c83b). 1049* Support for GCC on Linux has been extended from 4.8 back to GCC 4.7. It is 1050 unlikely Rumur will ever support a lesser GCC version than this (commit 1051 76a97b5354cc10cbd5fd188c385eeb457b3fd2ab). 1052* All major BSD flavours (DragonFly, FreeBSD, NetBSD, OpenBSD) are supported. 1053 Rumur now runs on all major desktop operating systems except Windows (commits 1054 6524f1eaedc6724fb26462ec901c241ded7861e1, 1055 026c9a476ba5efea5dd4fd7a5a8bcec7588381e8, 1056 7e9addb34df01abe7449823c33772985e9f6172b). 1057 1058Internal changes 1059~~~~~~~~~~~~~~~~ 1060* Bug fix: a memory leak on passing invalid command line options has been 1061 removed. This is under "Internal changes" because the leak occurred 1062 immediately prior to program exit, so would only have affected users debugging 1063 or embedding Rumur (commit 4f89903e244c7c188577d082c204bdb344ed1af8). 1064* New options for scoping the range of tests that the test suite runs. This is 1065 mainly for use by the continuous integration setup (commit 1066 ba2377a3b7240774d6bfb6745bb3c424c67b9277). 1067 1068v2019.03.11 1069----------- 1070 1071User-facing changes 1072~~~~~~~~~~~~~~~~~~~ 1073* Bug fix: enums and booleans that were used as ruleset parameters would 1074 previously have their values printed numerically in counterexample traces. For 1075 example, ``false`` would be printed as ``0``. Both are now printed as their 1076 textual names (commit 40c281d80342e684401425769e8e91ec78e3b019). 1077* Support for "cover" properties has been introduced. These are described in 1078 doc/properties.rst (commits 22a865897d23e2281541fe43276277b4b980a14d, 1079 29ac671ca93a0eef79b4f2b85a43da624d10938f, 1080 f9fe9614a4beb930f54db50250e4004ad773cee5, 1081 b4c5ead18eb3d99d2434aad6732cfce305c629c2). 1082* State allocation has been optimised, resulting in a speed up of ~46% and 1083 peak memory usage reduction of ~9% in the generated verifier (commit 1084 7ddf00bbce10a5f0cdd994658ac4545b186826ac). 1085* When using GCC, the minimum required version has been reduced from 4.9 to 4.8 1086 (commits c84bad26079f49a40b4c9cbdcd50b508292a8689, 1087 657eea8b8b84d269916207268edab85d71aba532, 1088 ff5a32521e4f937bd4d81b3ac7ae7204c8f913ec, 1089 227f340a059ce704ac1dff9cff75d721b987e147, 1090 7ba30edd5657c94fe5fe8c559fbde179817c795b, 1091 554d37e47cc9f878f65161d3ae51f6fbb9345bd8, 1092 3c827ae7b0f20d3f3f10118f61adcf73e58ee701, 1093 e929000525239eb357ad780c95aa54008633c678, 1094 a1ece0ad453ef95decd6256dac69b2af99ced2ff, 1095 b18e0430c8cd1cb5f67827e8ca2a6b0ab4117147, 1096 4e04bb5a6333df60444710f949486ea34739acc0). 1097* A Vim extension is included in misc/murphi.vim to add support for syntax 1098 highlighting Rumur's Murphi extensions (commit 1099 6dbcd208025a4a07b94d818110613a69efc05e4a). 1100 1101Internal changes 1102~~~~~~~~~~~~~~~~ 1103* Bug fix: the test suite no longer attempts to output decoded UTF-8 data on 1104 stdout/stderr (commit 551d18398189cb11ba6274d708d3ff293af034c7). 1105 1106v2019.03.02 1107----------- 1108 1109User-facing changes 1110~~~~~~~~~~~~~~~~~~~ 1111* Bug fix: enum types with duplicate members are now rejected. Previously, 1112 members would silently shadow earlier duplicate members (commit 1113 b476ffbdb7f5afb245c933a89d8f3cf9ecc8a884). 1114* Bug fix: models that redeclare symbols are now rejected. Previously, 1115 definitions would silently shadow earlier same-named definitions (commit 1116 96b8acab16310f4e80008b92827f804ba6e3ae66). 1117* The generated verifier produces more context information in error messages 1118 (commits 45a63a9f26f531587d0c461da74467e2cc008c38, 1119 7238dcacbf676c2649cfe82c98df25dbe96af93d, 1120 9384c756477cbf164ea7f41227b053fca4c67fc5, 1121 063e92bd53a5dbbb642e1d5c302a9240afff5fbc, 1122 668c1d6ab02e9c55cfd8119e5a403c5595cd5b45, 1123 39d35f4344633c2e1280fc0d5b28e2356140229b, 1124 434fbf2f50d69b7824a224280bd5f7f3bcc2275d, 1125 6822bba8a280b70d53d6dbb470f631143df0b5c4). 1126* The implementation of the queue of pending states has been further optimised, 1127 resulting in a ~25% reduction in the runtime of the generated verifier 1128 (commits 8f0329c33343cfcf16675a110ed3211b9abc95e3, 1129 2153f1f9e0ac7e2d015aff58cd0d8007901de808). 1130* The warning emitted by Rumur when your model is missing a start state is now 1131 suppressed when you pass ``--quiet`` (commit 1132 55514d39e40b2c018379e15d2f706e0a1c56ed18). 1133 1134Internal changes 1135~~~~~~~~~~~~~~~~ 1136* Nothing relevant. 1137 1138v2019.02.14 1139----------- 1140 1141User-facing changes 1142~~~~~~~~~~~~~~~~~~~ 1143* Bug fix: calls of procedures (a.k.a. functions with no return type) are now 1144 rejected when appearing within an expression (commit 1145 72d9196308a8b0d3b43929566beb571029b7e006). 1146* Bug fix: unary negation that never worked correctly has been repaired (commit 1147 48228f32c43423cd956f988fb0567fca080b9b28). 1148* Between v2019.02.01 and v2019.02.04, there was an unintended performance 1149 regression in the runtime of the generated verifier (commit 1150 f5589751de2f860c3cca7d681f9710160d3c20a8). This has been addressed and the 1151 verifier runs faster than even v2019.02.01 (commit 1152 ccf410672326e04230331576a1c76003ad2ab1a3). 1153* Returning a range-typed expression within a function that returns a 1154 *different* range type is now supported (commit 1155 e196ed43199d6d47d36eb9f225017c2123e294c3). 1156 1157Internal changes 1158~~~~~~~~~~~~~~~~ 1159* ``Expr::type()`` returns a smart pointer that is never null (commits 1160 d89de1376abe5bbbef61d68b02c45a35c4f9a12f, 1161 beeffb42ad6514448e463e8a2d73d3a1d8b35898, 1162 e196ed43199d6d47d36eb9f225017c2123e294c3, 1163 5dcf10f2821ffb8a2080b297fc664485884747be). 1164 1165v2019.02.04 1166----------- 1167 1168User-facing changes 1169~~~~~~~~~~~~~~~~~~~ 1170* Bug fix: using a non-scalar (record or array) result of a function call as an 1171 input parameter to another function or procedure would previously cause an 1172 assertion failure during code generation. This has been addressed and correct 1173 code is now generated (commit 73dcbf237f747d8958528127f6a05442bd3bf2c0). 1174* Bug fix: the convenience wrapper ``rumur-run`` now correctly exits when one of 1175 its steps fails and also returns the correct exit status (commits 1176 9eae5c5a22a87507713a2ebc5b57120de00e6f10, 1177 46cc017ee8c6337453601c245e6e764254687f48, 1178 235fbc552addefc1f34e8840a9d80845b423d30e, 1179 80825dfb406eb6f39aaa01c9011eadd7b6ad9b05). 1180* Bug fix: column offset information in the XML produced by ``rumur-ast-dump`` 1181 was sometimes off by one. This is now corrected (commit 1182 7d8dc868d9e1c31243b15e3de116e4f0740a38b3). 1183* GCC 4.9 is now supported. Previously the oldest version of GCC we supported 1184 was 5 (commits 83ce80ad8bba3f48d4316dba29b4795c13facd03, 1185 0ed86df81586b5808be82c924ad964b25cb38447). 1186* The error message when a model assertion fails has been made more informative 1187 (commit 608fe69abfd7aa7ab724a42b1327bb055f7fb3ac). 1188 1189Internal changes 1190~~~~~~~~~~~~~~~~ 1191* Nothing relevant. 1192 1193v2019.02.01 1194----------- 1195 1196User-facing changes 1197~~~~~~~~~~~~~~~~~~~ 1198* The values of ruleset parameters are reported in counter-example traces 1199 (commits 37f742797d8c76523607f90e80a5d1cc0ff16226, 1200 f7a8b012bfce555f156d1682cfd1073e8ccfe462, 1201 ee2d85200708cc70c2df056409d3da1283da2218). 1202* The name of a failing invariant is given in the failure message (commit 1203 60e864ccd8abefd617f21af4e1a78c53d1a3a66e). 1204* Comparison of complex types using ``=`` or ``!=`` is supported in models 1205 (commits 107f6c4ac88ce4e2c6745507aa332aa17dfd3264, 1206 bbd3beebb6ce0a51475a241eff45d7c2a223bcbb). 1207* ``rumur-run`` passes ``-march=native -mtune=native`` to the C compiler (commit 1208 ad9e26bfafb1cdf3877f46dd31b4072e1efffb5d). 1209* Rulesets with non-constant parameters are rejected (commit 1210 90810e214e7fa200d683f4ee4b79ef489d9e3d34). 1211 1212Internal changes 1213~~~~~~~~~~~~~~~~ 1214* Various new interfaces were added to types and quantifiers (commits 1215 6ea740ec2f6518733a626805af6b0f7275fc9b86, 1216 41e01629c30293dc91dd460d0286b74763eba387, 1217 aea30d24234777a0b0698c1ce6f28f8267b15d9f, 1218 154885bac4950b70c80620566e37d5a2890d317e). 1219 1220v2019.01.12 1221----------- 1222 1223User-facing changes 1224~~~~~~~~~~~~~~~~~~~ 1225* Bug fix: an issue that could have led to the corruption of reference-counted 1226 pointers in the checker was addressed (commit 1227 04fede03a59624f3c08ee7b80d8f928dfc1e45be). 1228* The licence has been changed from the vague "public domain" to the Unlicense. 1229 This is just a clarification and does not indicate a change in the licensing 1230 intent (commit 592e0c62ff9b1b7bf1bada4e41fa058d2d669ab8). 1231* All Python components now work with Python 2 in addition to Python 3 (commits 1232 f04b1442af0b30581b17fc517aeecce99bd8f1ef, 1233 de4fcd64ed20b128e7dceb44dd57b757e15096c5). 1234* ``rumur-run`` and ``rumur-ast-dump`` now have accompanying manpages (commits 1235 fe484a28ac3f77766b7de30569c85350b499ffbd, 1236 3c2ba659f36e6b4cbedb8fd35b7f5c0f0af3be65). 1237* A Zsh completion script was added (commit 1238 aac9e7718f3849b66932e375d673ea6b80547ff8). 1239* Missing documentation for the ``--output`` option was added (commit 1240 3047fb45f4a1aee9c5064ee9bb260df25bf72c8e). 1241 1242Internal changes 1243~~~~~~~~~~~~~~~~ 1244* A RelaxNG schema was added for the format produced by the AST dumper (commit 1245 36d26f6c327dbbd541537ad12d07636aba55f502). 1246* Rumur should now be compilable with ``-pedantic`` in most environments 1247 (commits b4ef8c0e8bcc1af2a1afd00204e2df735928488f, 1248 526afa1fb9e00bb159caf8ce49f83e40c571f747). 1249 1250v2018.12.20 1251----------- 1252 1253User-facing changes 1254~~~~~~~~~~~~~~~~~~~ 1255* Bug fix: boolean constants are now usable in boolean expressions, rather than 1256 being considered ranges (commits 3f8e25eed1b2cd88b04aec973b84efea3737f16b, 1257 6ee751955a0781becae7dcc0e34a7477e668e462). 1258* Bug fix: indexing a non-array expression is now reported as an 1259 error, rather than causing an assertion failure (commits 1260 606657b7fc656fd4c304523b98c5e2828a896271, 1261 a31c9973f63a719b676be97e7a893dd21d451511, 1262 5222f6ddce51ea66ceda6ecb0e016a94308e835b). 1263* Bug fix: calling a function with incorrect arguments is now reported as an 1264 error, rather than causing an assertion failure or uncaught exception (commits 1265 705793e6b0f3646d30dcab247d27cdd3ac94430c, 1266 2427b74c4d6fb40115943dc01bbd66cc4ada7d17, 1267 fe9344f5b723608cd8916bd16c2688f9494ca92a). 1268* Bug fix: trying to access the field of a non-record expression is now reported 1269 as an error, rather than causing an assertion failure or uncaught exception 1270 (commits f72373b30e8031baa8c8e0e953c05e47874ae854, 1271 76d09b6bf77414b51af2bf1da0ecd099c25ad2e1, 1272 27b61a5f6b0be2e838a39c02e567c87b4ce80d76, 1273 b917ece31a209ba9586c7c44577ba34b19a2c0a7). 1274* Bug fix: The boolean literals ``true`` and ``false`` are now accepted in all 1275 possible casings (commits 121d724c00e2afc1d1fa6c525dad958646936fb1, 1276 68e9164ae8a5a17c6e6346266051b24780bbf203). 1277* The ``isundefined`` operator is now implemented (commits 1278 d12841246e207a5691159f8ed46faf08cb596dd5, 1279 8e3563a0309d57dc19dbd7f0d1c50a8f30878559). 1280* Range-typed expressions can now be passed in to functions as non-var 1281 parameters of a differing range type, where previously this scenario would 1282 only accept rvalues or identical range types (commits 1283 343e97eeeb8ccd4c59bf150c42c0b74f1b00ec6a, 1284 09cfec88a1e648eaa240404c2b215ed4cefec926, 1285 2324e3efc370a09a289a4998c677cf1bfb31a245, 1286 90a95c31d5c04a6083f753bc15f566658abcdf9d). 1287* If the generated verifier is multithreaded, it now prints a thread identifier 1288 in each progress line (commit b222b3bc5fad2ff6e8371d3b46ad28809daa2451). 1289* Some spurious compiler warnings when building the generated verifier have been 1290 suppressed (commits 8a05ab0d209c0b8cbfa7048d5775505c1f70f283, 1291 4f447fdcc44f694f8bc1d948bbc17d690ca3d59f, 1292 7885b611ef9d9e6d18629b1eb696def0183eed16). 1293 1294Internal changes 1295~~~~~~~~~~~~~~~~ 1296* The use of ``static_assert`` has been replaced with ``_Static_assert`` (commit 1297 ad26fe525f7ba99dfbf3d5c6bc248ef41602d9a5). 1298* ``Expr`` and ``Decl`` gained a new ``is_readonly`` method (commit 1299 47c27f217b035fa9881fe32576354c08669b0899) and the distinction between the 1300 concepts of "lvalue" and "writable" is now more accurate. 1301* The test suite has been backported so it also runs on Python 2 in addition to 1302 Python 3 (commit 7fe028271d376188d8b5d6353e0bca720d12e6b9). 1303 1304v2018.12.08 1305----------- 1306* Hello world! 1307