diff --git a/CHANGELOG.rst b/CHANGELOG.rst index aa8be3fb..1ec4ca9c 100644 --- a/CHANGELOG.rst +++ b/CHANGELOG.rst @@ -1,6 +1,90 @@ Change log ========== +v2026.08.30 +----------- + +User-facing changes +~~~~~~~~~~~~~~~~~~~ +* Bug fix: passing a ``--value-type`` containing spaces to ``murphi2c`` no + longer results in malformed code (commits + 7feb6e0aa0b2b079c2e4f00cc5ceb519d9dac6e6, + e38ce1b5f02beb7f996fac5ff5e64673ca323f20, + a1d416ec999af9c24de218942b35fa3cb7f6fbbb). +* Bug fix: ``murphi-format`` more correctly handles ``==>`` followed by + ``begin`` with multiple newlines in-between (commit + 70173dbe7adb55faa6de5e3fba24522fa3beb4e6). +* Bug fix: monitoring of subprocesses (SMT solvers) was corrected, avoiding a + previous possible deadlock (commit 67c545f43eb8a71fc59465d8f2d9227a9dd7d631). +* Bug fix: ``murphi-format`` recognises the command line option ``-h`` (commit + dc03b1031931030fd0cb9b7074a4ad345dee5bb5). +* Bug fix: ``murphi-format`` recognises the command line option ``-t`` (commit + 9e47b916f8f208a4bfe36ffdafc094caa37745d9). +* Bug fix: when passing a very small number to ``--set-capacity``, malformed + code is no longer generated (commit 80f9ac2acbe3db43bb09fd8fba4e87b4f85fd57b). +* Bug fix: ``murphi-format`` recognises and responds to failures to rewind file + pointers (commits 52eed93e005726fd39b7ad7327c35acba1afc386, + 79be8baacb001a3180c77f5ef89ffccb309a5641). +* The ``undefined`` keyword is now supported (commits + 1c419e523f625b8ff4d31cd33f9a9fb021f6ed42, + dd3bc59f781c8ae587f3a5753b80ed06ac033c8b). +* The ``union`` type is now supported during parsing and type checking. It is + still not possible to generate a checker from a model containing unions but + some auxiliary tools like ``murphi2xml`` fully support unions. The main + purpose of this addition is to support third-party code using librumur to + parse union-containing models (commits + 7ecea100928755fb5f5cb37b638799177b3114c1, + 3b58aa9dbfae7082c01b36368785fea530717e31, + d6b7949fea8c9da3bdbd08d0311b60fca04683cc, + 62a8c4931edc787401726f2e17d40d4832836d0d, + c8720b77e298e51350be5486829f16f2c2bf15e8, + c89bd8afdaa1aad2089cecfb7a77d2e28fab68a4, + 5a2545ee489faf4b730e00797b97979e53b3fab2). +* The ``multiset`` type is now supported during parsing and type checking. It is + still not possible to generate a checker from a model containing multisets but + some auxiliary tools like ``murphi2xml`` fully support multisets. The main + purpose of this addition is to support third-party code using librumur to + parse multiset-containing models (commits + 9f55ca0ed6fbf0b841130f2c71e5bbf69d4957d0, + 0b3e81a6b425d10f5847e8907cf36487944cc017, + 0639e869deb55f9930e485a5029c82316eafc950, + 1942fbaab08493e2a02a02cb1ef3af40b1901cd9, + b9d77afccfc01ce9be1287580714c8dd3934493c, + dbd173eefe7ab88b329330d58c214169133aca46, + df05e0f8df35146f535cc42cc134cd2efbb47735, + c12c449c53600e8de09fb40459f67590d8399990, + ba7239c495f448f60977c6059af2f14d16fb509a, + 8eb2b08949f5c2c97ee3dc5f22594c5ffbd1fc39, + 1076e5f55a0e164824a4e1c23f0ad0fd33528dd1, + d1cfbdd8a8b1cf96e9f265bcc4061b2ecb26205f, + d70d11730bd472b36f96fc6539a4a05b2c881fd4, + 67127631f48b6f495d858bae6a52de4b0dcaf0ae, + e534adfddbfa43ee0d572a96a3aa718d8a7bfec2, + 745ce5eec26b43a123ba27e9f7403fd511022307, + 666b89cdfb62af4d39fb292ebe74625715c7a69b, + 2a686b72ac14948168f58957bff44a7898891cec, + f6617bef7bab564139822149caafd67b0c722614). +* ``--help`` ignores ``$TMPDIR`` when it points to an unusable directory (commit + b873e30df7b7f14af3529dd0a2355f8b91d6956e). +* A false positive ``-Wshift-count-overflow`` compiler warning when building the + generated checker with GCC ≥ 15 has been suppressed (commit + 11347fc61465d5aa7c46fb21721a8cf579739e38). + +Internal changes +~~~~~~~~~~~~~~~~ +* Bug fix: array indexing (``Element``) is considered impure (``is_pure()`` + returns ``false``) if its indexing expression is impure (commit + 2eb8c356927601e6ac4ef0120746da9ebb702ea8). +* Bug fix: array indexing (``Element``) is considered impure (``is_pure()`` + returns ``false``) if its array expression is impure (commit + b0aa51f9631457fb9992d0ef19229197678a9c2f). +* Bug fix: record field selection (``Field``) is considered impure + (``is_pure()`` returns ``false``) if its left-hand side is impure (commit + d6c04d2a15021338e29e5c80bb940e0993c87a1c). +* The ``lower_bound`` and ``upper_bound`` member functions on AST nodes now + return ``mpz_class`` values instead of ``std::string`` values (commit + fd2a59a25af8c4a45f6ec85303c6bad9260a069e). + v2026.03.11 ----------- diff --git a/share/CMakeLists.txt b/share/CMakeLists.txt index 8e8dc2d8..0a22ce89 100644 --- a/share/CMakeLists.txt +++ b/share/CMakeLists.txt @@ -20,3 +20,6 @@ install(DIRECTORY v2025.08.31 install(DIRECTORY v2026.03.11 DESTINATION ${CMAKE_INSTALL_DATAROOTDIR}/rumur/lib ) +install(DIRECTORY v2026.08.30 + DESTINATION ${CMAKE_INSTALL_DATAROOTDIR}/rumur/lib +) diff --git a/share/v2026.08.30/_list b/share/v2026.08.30/_list new file mode 100644 index 00000000..fa7115ae --- /dev/null +++ b/share/v2026.08.30/_list @@ -0,0 +1,232 @@ +dnl template for a statically sized list/queue/stack +dnl +dnl This file defines, as an M4¹ template, a type-generic Murphi list data +dnl structure. To use this, include the template and then call the macro "_list" +dnl with 4 parameters: +dnl • "name" – a prefix for the generated list data structure and its +dnl supporting functions +dnl • "index_t" – a Murphi type for indexing the list +dnl • "elem_t" – a Murphi type for the elements of the list +dnl • "size" – one more than the number of elements in type "index_t", +dnl defaulting to 2³¹-1 (see discussion of this below) +dnl E.g.: +dnl +dnl include(`_list')dnl +dnl +dnl type +dnl int: 0..32; +dnl +dnl _list(`ints', `0..10', `int')dnl +dnl +dnl Pre-process your model with M4: +dnl +dnl $ m4 --include=/path/to/rumur/install/share/rumur/lib model.m >out.m +dnl +dnl This generates a type and some supporting functions: +dnl +dnl type +dnl ints_t: … +dnl +dnl function ints_is_empty(list_: ints_t): boolean; +dnl function ints_is_full(list_: ints_t): boolean; +dnl function ints_size(list_: ints_t): 0..2147483647; +dnl procedure ints_push_back(var list_: ints_t; elem_: int); +dnl function ints_try_push_back(var list_: ints_t; elem_: int): boolean; +dnl function ints_pop_front(var list_: ints_t): int; +dnl function ints_pop_back(var list_: ints_t): int; +dnl +dnl You can then go on to use the "ints_t" type in your handwritten model code. +dnl +dnl "index_t" can be an arbitrary type; the only requirement is that it is +dnl iterable. It can be a previously defined type or a type literal. The +dnl underlying type could be boolean, a range, a scalarset, or an enum. Though +dnl it is unlikely anything except a range makes sense. +dnl +dnl "elem_t" can be an arbitrary type. It can be a previously defined type or a +dnl type literal, though you probably want to name it in order to more easily +dnl use the push and pop functions. +dnl +dnl "size" does not need to be supplied unless (a) your indexing type "index_t" +dnl has more than 2³¹-2 elements or (b) you are trying to optimise your model by +dnl using a value type narrower than "int32_t". In either case, you still do not +dnl need to supply "size" if you never call the "*_size()" function; it is not +dnl used internally within this template. If you call "*_size()" and your usage +dnl falls into the (a) or (b) cases above, supply a "size" that is the number of +dnl elements in "index_t" plus 1. Note that, e.g. if your indexing type is +dnl "0..255", your size will need to be ≥ 256, preventing you using the value +dnl type "uint8_t" which is not large enough to hold the value 256. +dnl +dnl This template is in the public domain. You may use it for any purpose and +dnl its inclusion in a model does not affect the legal status of that model. +dnl +dnl ¹ https://en.wikipedia.org/wiki/M4_(computer_language) +dnl +define(`_list', `dnl +------------------------------------------------------------------------------- +-- interface for $1_t, a list of $3 values indexed by $2 +------------------------------------------------------------------------------- + +type + $1_t: array[$2] of record + -- Does this slot hold an item? The type 1..1 is used to model a boolean + -- without incurring an extra bit for the undefined value. I.e. + -- false = isundefined(is_populated_) + -- true = !isundefined(is_populated_) + is_populated_: 1..1; + -- the contents of the slot, if !isundefined(is_populated_) + value_: $3; + end; + +function $1_is_empty(list_: $1_t): boolean; +begin + -- use a single-iteration loop to check the first element to avoid assuming + -- the lower bound of type $2 + for i_: $2 do + if !isundefined(list_[i_].is_populated_) then + return false; + else + return true; + end; + end; + -- in the edge case where $2 is an empty type, consider the list always empty + return true; +end; + +-- get the number of elements present in a list +function $1_size(list_: $1_t): 0..ifelse(`$4', `', `2147483647', `$4'); + var count_: 0..ifelse(`$4', `', `2147483647', `$4'); +begin + -- We have no easy way of checking the number of members in the type $2 at + -- generation time. So we use a runtime sanity check here that our return type + -- is large enough to represent the maximum size. A decent compiler will + -- constant fold and eliminate this in the common case where the type is + -- indeed large enough. + count_ := 0; + for i_: $2 do + assert + "0..ifelse(`$4', `', `2147483647', `$4') too small to represent $1_t size" + count_ < ifelse(`$4', `', `2147483647', `$4'); + count_ := count_ + 1; + end; + + count_ := 0; + for i_: $2 do + if !isundefined(list_[i_].is_populated_) then + count_ := count_ + 1; + end; + end; + return count_; +end; + +function $1_is_full(list_: $1_t): boolean; +begin + -- use a loop to check the last element to avoid assuming the upper bound of + -- type $2 + for i_: $2 do + if isundefined(list_[i_].is_populated_) then + return false; + end; + end; + return true; +end; + +-- Treating a $1_t as a first-in-first-out queue, enqueue an item. Or +-- equivalently, treating a $1_t as a last-in-first-out stack, stack an item. +procedure $1_push_back(var list_: $1_t; elem_: $3); +begin + assert "attempting to push into a full $1_t" !$1_is_full(list_); + -- use a loop to find the first empty slot to avoid assuming the upper bound + -- of type $2 + for i_: $2 do + if isundefined(list_[i_].is_populated_) then + list_[i_].value_ := elem_; + list_[i_].is_populated_ := 1; + return; + end; + end; + assert "unreachable code executed" false; +end; + +-- Treating a $1_t as a first-in-first-out queue, enqueue an item and return +-- true if possible. Or equivalently, treating a $1_t as a last-in-first-out +-- stack, stack an item and return true if possible. If it is not possible to +-- insert the new item, do nothing and return false. +function $1_try_push_back(var list_: $1_t; elem_: $3): boolean; +begin + if $1_is_full(list_) then + return false; + end; + $1_push_back(list_, elem_); + return true; +end; + +-- treating a $1_t as a first-in-first-out queue, dequeue an item +function $1_pop_front(var list_: $1_t): $3; +var + first_: $3; + successor_: boolean; +begin + assert "attempting to pop from an empty $1_t" !$1_is_empty(list_); + for i_: $2 do + + -- extract the first element + assert "corrupted list" !isundefined(list_[i_].is_populated_); + first_ := list_[i_].value_; + + -- Shuffle the remaining elements forwards. We do this with an unorthodox + -- double loop to avoid assuming anything about the bounds of $2 or + -- even whether its members are orderable. + for j_: $2 do + undefine list_[j_]; + successor_ := false; + for k_: $2 do + if j_ = k_ then + assert "incorrect shuffle logic" !successor_; + successor_ := true; + elsif successor_ then + list_[j_] := list_[k_]; + successor_ := false; + end; + end; + end; + + return first_; + end; +end; + +-- treating a $1_t as a last-in-first-out stack, unstack an item +function $1_pop_back(var list_: $1_t): $3; +var + last_: $3; + has_successor_: boolean; + successor_: boolean; +begin + assert "attempting to pop from an empty $1_t" !$1_is_empty(list_); + for i_: $2 do + + -- Is this element the last? We do this with an unorthodox loop to avoid + -- assuming anything about the bounds of $2 or even whether its members + -- are orderable. + has_successor_ := false; + for j_: $2 do + if i_ = j_ then + successor_ := true; + elsif successor_ then + has_successor_ := !isundefined(list_[j_].is_populated_); + successor_ := false; + end; + end; + + -- if this is the last element, extract and return it + if !has_successor_ then + last_ := list_[i_].value_; + undefine list_[i_]; + return last_; + end; + end; +end; + +------------------------------------------------------------------------------- +-- end interface for $1_t +------------------------------------------------------------------------------- +')dnl diff --git a/share/v2026.08.30/_set b/share/v2026.08.30/_set new file mode 100644 index 00000000..85749ed1 --- /dev/null +++ b/share/v2026.08.30/_set @@ -0,0 +1,100 @@ +dnl template for an unordered set +dnl +dnl This file defines, as an M4¹ template, a type-generic Murphi set data +dnl structure. To use this, include the template and then call the macro "_set" +dnl with 2 parameters: +dnl • "name" – a prefix for the generated set data structure and its +dnl supporting functions +dnl • "elem_t" – a Murphi type for the elements of the set +dnl E.g.: +dnl +dnl include(`_set')dnl +dnl +dnl type +dnl int: 0..32; +dnl +dnl _set(`ints', `int')dnl +dnl +dnl Pre-process your model with M4: +dnl +dnl $ m4 --include=/path/to/rumur/install/share/rumur/lib model.m >out.m +dnl +dnl This generates a type and some supporting functions: +dnl +dnl type +dnl ints_t: … +dnl +dnl function ints_is_empty(set_: ints_t): boolean; +dnl function ints_is_full(set_: ints_t): boolean; +dnl function ints_add(var set_: ints_t; elem_: int): boolean; +dnl function ints_remove(var set_: ints_t; elem_: int): boolean; +dnl function ints_contains(set_: ints_t; elem_: int): boolean; +dnl +dnl You can then go on to use the "ints_t" type in your handwritten model code. +dnl +dnl "elem_t" can be an arbitrary scalar type. It can be a previously defined +dnl type or a type literal. +dnl +dnl This template is in the public domain. You may use it for any purpose and +dnl its inclusion in a model does not affect the legal status of that model. +dnl +dnl ¹ https://en.wikipedia.org/wiki/M4_(computer_language) +dnl +define(`_set', `dnl +------------------------------------------------------------------------------- +-- interface for $1_t, a set of $2 +------------------------------------------------------------------------------- + +type + $1_t: array[$2] of 1..1; + +function $1_is_empty(set_: $1_t): boolean; +begin + for i_: $2 do + if !isundefined(set_[i_]) then + return false; + end; + end; + return true; +end; + +function $1_is_full(set_: $1_t): boolean; +begin + for i_: $2 do + if isundefined(set_[i_]) then + return false; + end; + end; + return true; +end; + +-- insert a value into the set, returning true if it was already present +function $1_add(var set_: $1_t; elem_: $2): boolean; +var + rc_: boolean; +begin + rc_ := !isundefined(set_[elem_]); + set_[elem_] := 1; + return rc_; +end; + +-- remove a value from the set, returning true if it was present +function $1_remove(var set_: $1_t; elem_: $2): boolean; +var + rc_: boolean; +begin + rc_ := !isundefined(set_[elem_]); + undefine set_[elem_]; + return rc_; +end; + +-- test the existence of an element in the set +function $1_contains(set_: $1_t; elem_: $2): boolean; +begin + return !isundefined(set_[elem_]); +end; + +------------------------------------------------------------------------------- +-- end interface for $1_t +------------------------------------------------------------------------------- +')dnl