diff --git a/doc/vs-cmurphi.rst b/doc/vs-cmurphi.rst index 39896992..2f986ac9 100644 --- a/doc/vs-cmurphi.rst +++ b/doc/vs-cmurphi.rst @@ -37,7 +37,21 @@ Type System ----------- CMurphi supports real arithmetic using the ``real`` data type. Rumur does not support this type and there are no plans to implement this or any floating point -support. Similarly, Rumur does not support the ``multiset`` type. +support. + +Multisets +^^^^^^^^^ +Models that use the ``multiset`` type can be parsed with librumur, but +generation of a checker using ``rumur`` is not supported. Some of the Rumur +tools fully support multiset types, e.g. ``murphi2xml``, but others reject +models with multiset types, e.g. ``murphi2uclid``. + +CMurphi requires the index of multiset to be a scalarset bound. Rumur supports +any constant expression as a bound. + +This limitation of syntax-only support applies also to the multiset constructs +``Choose``, ``MultisetAdd``, ``MultisetCount``, ``MultisetRemove``, and +``MultisetRemovePred``. Unions ^^^^^^ diff --git a/librumur/include/rumur/Expr.h b/librumur/include/rumur/Expr.h index 88e86350..65c2b03f 100644 --- a/librumur/include/rumur/Expr.h +++ b/librumur/include/rumur/Expr.h @@ -710,4 +710,24 @@ struct RUMUR_API_WITH_RTTI IsUndefined : public UnaryExpr { void to_stream(std::ostream &out) const override; }; +struct RUMUR_API_WITH_RTTI MultisetCount : public Expr { + std::string identifier; + Ptr container; + Ptr predicate; + + MultisetCount(const std::string &identifier_, const Ptr &container_, + const Ptr &predicate_, const location &loc_); + MultisetCount *clone() const override; + + void visit(BaseTraversal &visitor) override; + void visit(ConstBaseTraversal &visitor) const override; + + bool constant() const override; + Ptr type() const override; + mpz_class constant_fold() const override; + void validate() const override; + void to_stream(std::ostream &out) const override; + bool is_pure() const override; +}; + } // namespace rumur diff --git a/librumur/include/rumur/Rule.h b/librumur/include/rumur/Rule.h index a06b93ae..0f54e7f5 100644 --- a/librumur/include/rumur/Rule.h +++ b/librumur/include/rumur/Rule.h @@ -106,4 +106,20 @@ struct RUMUR_API_WITH_RTTI Ruleset : public Rule { std::vector> flatten() const override; }; +struct RUMUR_API_WITH_RTTI Choose : public Rule { + std::string identifier; + Ptr container; + std::vector> rules; + + Choose(const std::string &identifier_, const Ptr &container_, + const std::vector> &rules_, const location &loc_); + Choose *clone() const override; + void validate() const override; + + void visit(BaseTraversal &visitor) override; + void visit(ConstBaseTraversal &visitor) const override; + + std::vector> flatten() const override; +}; + } // namespace rumur diff --git a/librumur/include/rumur/Stmt.h b/librumur/include/rumur/Stmt.h index 1a8a4c25..c22967c2 100644 --- a/librumur/include/rumur/Stmt.h +++ b/librumur/include/rumur/Stmt.h @@ -130,6 +130,44 @@ struct RUMUR_API_WITH_RTTI If : public Stmt { void visit(ConstBaseTraversal &visitor) const override; }; +struct RUMUR_API_WITH_RTTI MultisetAdd : public Stmt { + Ptr arg0; + Ptr arg1; + + MultisetAdd(const Ptr &arg0_, const Ptr &arg1_, + const location &loc_); + MultisetAdd *clone() const override; + void validate() const override; + void visit(BaseTraversal &visitor) override; + void visit(ConstBaseTraversal &visitor) const override; +}; + +struct RUMUR_API_WITH_RTTI MultisetRemove : public Stmt { + Ptr arg0; + Ptr arg1; + + MultisetRemove(const Ptr &arg0_, const Ptr &arg1_, + const location &loc_); + MultisetRemove *clone() const override; + void validate() const override; + void visit(BaseTraversal &visitor) override; + void visit(ConstBaseTraversal &visitor) const override; +}; + +struct RUMUR_API_WITH_RTTI MultisetRemovePred : public Stmt { + std::string identifier; + Ptr container; + Ptr predicate; + + MultisetRemovePred(const std::string &identifier_, + const Ptr &container_, const Ptr &predicate_, + const location &loc_); + MultisetRemovePred *clone() const override; + void validate() const override; + void visit(BaseTraversal &visitor) override; + void visit(ConstBaseTraversal &visitor) const override; +}; + struct RUMUR_API_WITH_RTTI ProcedureCall : public Stmt { FunctionCall call; diff --git a/librumur/include/rumur/TypeExpr.h b/librumur/include/rumur/TypeExpr.h index f7d90160..ab1dc000 100644 --- a/librumur/include/rumur/TypeExpr.h +++ b/librumur/include/rumur/TypeExpr.h @@ -166,6 +166,23 @@ struct RUMUR_API_WITH_RTTI Array : public TypeExpr { void to_stream(std::ostream &out) const override; }; +struct RUMUR_API_WITH_RTTI Multiset : public TypeExpr { + Ptr index_bound; + Ptr element_type; + + Multiset(const Ptr &index_bound_, const Ptr &element_type_, + const location &loc_); + Multiset *clone() const override; + + void visit(BaseTraversal &visitor) override; + void visit(ConstBaseTraversal &visitor) const override; + + mpz_class width() const override; + mpz_class count() const override; + void validate() const override; + void to_stream(std::ostream &out) const override; +}; + struct RUMUR_API_WITH_RTTI TypeExprID : public TypeExpr { std::string name; diff --git a/librumur/include/rumur/indexer.h b/librumur/include/rumur/indexer.h index 5aac00bc..d0fb3447 100644 --- a/librumur/include/rumur/indexer.h +++ b/librumur/include/rumur/indexer.h @@ -33,6 +33,7 @@ class RUMUR_API_WITH_RTTI Indexer : public BaseTraversal { void visit_band(Band &n) override; void visit_bnot(Bnot &n) override; void visit_bor(Bor &n) override; + void visit_choose(Choose &n) override; void visit_clear(Clear &n) override; void visit_constdecl(ConstDecl &n) override; void visit_div(Div &n) override; @@ -60,6 +61,11 @@ class RUMUR_API_WITH_RTTI Indexer : public BaseTraversal { void visit_model(Model &n) override; void visit_mod(Mod &n) override; void visit_mul(Mul &n) override; + void visit_multiset(Multiset &n) override; + void visit_multisetadd(MultisetAdd &n) override; + void visit_multisetcount(MultisetCount &n) override; + void visit_multisetremove(MultisetRemove &n) override; + void visit_multisetremovepred(MultisetRemovePred &n) override; void visit_negative(Negative &n) override; void visit_neq(Neq &n) override; void visit_not(Not &n) override; diff --git a/librumur/include/rumur/traverse.h b/librumur/include/rumur/traverse.h index c92bd0e8..01272571 100644 --- a/librumur/include/rumur/traverse.h +++ b/librumur/include/rumur/traverse.h @@ -79,6 +79,7 @@ class RUMUR_API_WITH_RTTI BaseTraversal { virtual void visit_band(Band &n) = 0; virtual void visit_bnot(Bnot &n) = 0; virtual void visit_bor(Bor &n) = 0; + virtual void visit_choose(Choose &n) = 0; virtual void visit_clear(Clear &n) = 0; virtual void visit_constdecl(ConstDecl &n) = 0; virtual void visit_div(Div &n) = 0; @@ -106,6 +107,11 @@ class RUMUR_API_WITH_RTTI BaseTraversal { virtual void visit_model(Model &n) = 0; virtual void visit_mod(Mod &n) = 0; virtual void visit_mul(Mul &n) = 0; + virtual void visit_multiset(Multiset &n) = 0; + virtual void visit_multisetadd(MultisetAdd &n) = 0; + virtual void visit_multisetcount(MultisetCount &n) = 0; + virtual void visit_multisetremove(MultisetRemove &n) = 0; + virtual void visit_multisetremovepred(MultisetRemovePred &n) = 0; virtual void visit_negative(Negative &n) = 0; virtual void visit_neq(Neq &n) = 0; virtual void visit_not(Not &n) = 0; @@ -167,6 +173,7 @@ class RUMUR_API_WITH_RTTI Traversal : public BaseTraversal { void visit_band(Band &n) override; void visit_bnot(Bnot &n) override; void visit_bor(Bor &n) override; + void visit_choose(Choose &n) override; void visit_clear(Clear &n) override; void visit_constdecl(ConstDecl &n) override; void visit_div(Div &n) override; @@ -194,6 +201,11 @@ class RUMUR_API_WITH_RTTI Traversal : public BaseTraversal { void visit_model(Model &n) override; void visit_mod(Mod &n) override; void visit_mul(Mul &n) override; + void visit_multiset(Multiset &n) override; + void visit_multisetadd(MultisetAdd &n) override; + void visit_multisetcount(MultisetCount &n) override; + void visit_multisetremove(MultisetRemove &n) override; + void visit_multisetremovepred(MultisetRemovePred &n) override; void visit_negative(Negative &n) override; void visit_neq(Neq &n) override; void visit_not(Not &n) override; @@ -247,6 +259,7 @@ class RUMUR_API_WITH_RTTI ConstBaseTraversal { virtual void visit_band(const Band &n) = 0; virtual void visit_bnot(const Bnot &n) = 0; virtual void visit_bor(const Bor &n) = 0; + virtual void visit_choose(const Choose &n) = 0; virtual void visit_clear(const Clear &n) = 0; virtual void visit_constdecl(const ConstDecl &n) = 0; virtual void visit_div(const Div &n) = 0; @@ -274,6 +287,11 @@ class RUMUR_API_WITH_RTTI ConstBaseTraversal { virtual void visit_model(const Model &n) = 0; virtual void visit_mod(const Mod &n) = 0; virtual void visit_mul(const Mul &n) = 0; + virtual void visit_multiset(const Multiset &n) = 0; + virtual void visit_multisetadd(const MultisetAdd &n) = 0; + virtual void visit_multisetcount(const MultisetCount &n) = 0; + virtual void visit_multisetremove(const MultisetRemove &n) = 0; + virtual void visit_multisetremovepred(const MultisetRemovePred &n) = 0; virtual void visit_negative(const Negative &n) = 0; virtual void visit_neq(const Neq &n) = 0; virtual void visit_not(const Not &n) = 0; @@ -327,6 +345,7 @@ class RUMUR_API_WITH_RTTI ConstTraversal : public ConstBaseTraversal { void visit_band(const Band &n) override; void visit_bnot(const Bnot &n) override; void visit_bor(const Bor &n) override; + void visit_choose(const Choose &n) override; void visit_clear(const Clear &n) override; void visit_constdecl(const ConstDecl &n) override; void visit_div(const Div &n) override; @@ -354,6 +373,11 @@ class RUMUR_API_WITH_RTTI ConstTraversal : public ConstBaseTraversal { void visit_model(const Model &n) override; void visit_mod(const Mod &n) override; void visit_mul(const Mul &n) override; + void visit_multiset(const Multiset &n) override; + void visit_multisetadd(const MultisetAdd &n) override; + void visit_multisetcount(const MultisetCount &n) override; + void visit_multisetremove(const MultisetRemove &n) override; + void visit_multisetremovepred(const MultisetRemovePred &n) override; void visit_negative(const Negative &n) override; void visit_neq(const Neq &n) override; void visit_not(const Not &n) override; @@ -405,6 +429,7 @@ class RUMUR_API_WITH_RTTI ConstExprTraversal : public ConstBaseTraversal { void visit_aliasstmt(const AliasStmt &n) final; void visit_array(const Array &n) final; void visit_assignment(const Assignment &n) final; + void visit_choose(const Choose &n) final; void visit_clear(const Clear &n) final; void visit_constdecl(const ConstDecl &n) final; void visit_enum(const Enum &n) final; @@ -414,6 +439,10 @@ class RUMUR_API_WITH_RTTI ConstExprTraversal : public ConstBaseTraversal { void visit_if(const If &n) final; void visit_ifclause(const IfClause &n) final; void visit_model(const Model &n) final; + void visit_multiset(const Multiset &n) final; + void visit_multisetadd(const MultisetAdd &n) final; + void visit_multisetremove(const MultisetRemove &n) override; + void visit_multisetremovepred(const MultisetRemovePred &n) override; void visit_procedurecall(const ProcedureCall &n) final; void visit_property(const Property &n) final; void visit_propertyrule(const PropertyRule &n) final; @@ -452,6 +481,7 @@ class RUMUR_API_WITH_RTTI ConstStmtTraversal : public ConstBaseTraversal { void visit_band(const Band &n) final; void visit_bnot(const Bnot &n) final; void visit_bor(const Bor &n) final; + void visit_choose(const Choose &n) final; void visit_constdecl(const ConstDecl &n) final; void visit_div(const Div &n) final; void visit_element(const Element &n) final; @@ -475,6 +505,8 @@ class RUMUR_API_WITH_RTTI ConstStmtTraversal : public ConstBaseTraversal { void visit_model(const Model &n) final; void visit_mod(const Mod &n) final; void visit_mul(const Mul &n) final; + void visit_multiset(const Multiset &n) final; + void visit_multisetcount(const MultisetCount &n) final; void visit_negative(const Negative &n) final; void visit_neq(const Neq &n) final; void visit_not(const Not &n) final; @@ -517,6 +549,7 @@ class RUMUR_API_WITH_RTTI ConstTypeTraversal : public ConstBaseTraversal { void visit_band(const Band &n) final; void visit_bnot(const Bnot &n) final; void visit_bor(const Bor &n) final; + void visit_choose(const Choose &n) final; void visit_clear(const Clear &n) final; void visit_constdecl(const ConstDecl &n) final; void visit_div(const Div &n) final; @@ -543,6 +576,10 @@ class RUMUR_API_WITH_RTTI ConstTypeTraversal : public ConstBaseTraversal { void visit_model(const Model &n) final; void visit_mod(const Mod &n) final; void visit_mul(const Mul &n) final; + void visit_multisetadd(const MultisetAdd &n) final; + void visit_multisetcount(const MultisetCount &n) final; + void visit_multisetremove(const MultisetRemove &n) override; + void visit_multisetremovepred(const MultisetRemovePred &n) override; void visit_negative(const Negative &n) final; void visit_neq(const Neq &n) final; void visit_not(const Not &n) final; diff --git a/librumur/src/Expr.cc b/librumur/src/Expr.cc index c4b9138f..170d90d5 100644 --- a/librumur/src/Expr.cc +++ b/librumur/src/Expr.cc @@ -12,6 +12,7 @@ #include #include #include +#include #include #include #include @@ -1287,14 +1288,24 @@ bool Element::constant() const { return false; } Ptr Element::type() const { const Ptr t = array->type()->resolve(); - const Array *a = dynamic_cast(t.get()); - // if we are called during symbol resolution on a malformed expression, our - // left hand side may not be an array - if (a == nullptr) - throw Error("array reference based on something that is not an array", loc); + { + auto a = dynamic_cast(t.get()); + if (a != nullptr) + return a->element_type; + } + + { + auto m = dynamic_cast(t.get()); + if (m != nullptr) + return m->element_type; + } - return a->element_type; + // if we are called during symbol resolution on a malformed expression, our + // left hand side may not be an array or a multiset + throw Error("array reference based on something that is neither an array nor " + "a multiset", + loc); } mpz_class Element::constant_fold() const { @@ -1305,13 +1316,30 @@ void Element::validate() const { const Ptr t = array->type()->resolve(); - if (!isa(t)) - throw Error("array index on an expression that is not an array", loc); + { + auto a = dynamic_cast(t.get()); + if (a != nullptr) { - auto a = dynamic_cast(*t); + if (!index->type()->coerces_to(*a->index_type)) + throw Error("array indexed using an expression of incorrect type", loc); + return; + } + } - if (!index->type()->coerces_to(*a.index_type)) - throw Error("array indexed using an expression of incorrect type", loc); + { + auto m = dynamic_cast(t.get()); + if (m != nullptr) { + const Scalarset s{m->index_bound, m->index_bound->loc}; + if (!index->type()->coerces_to(s)) + throw Error("multiset indexed using an expression of incorrect type", + loc); + return; + } + } + + throw Error( + "array index on an expression that is neither an array nor a multiset", + loc); } bool Element::is_lvalue() const { return array->is_lvalue(); } @@ -1744,4 +1772,56 @@ void IsUndefined::to_stream(std::ostream &out) const { out << "isundefined(" << *rhs << ')'; } +MultisetCount::MultisetCount(const std::string &identifier_, + const Ptr &container_, + const Ptr &predicate_, const location &loc_) + : Expr(loc_), identifier(identifier_), container(container_), + predicate(predicate_) {} + +MultisetCount *MultisetCount::clone() const { return new MultisetCount(*this); } + +void MultisetCount::visit(BaseTraversal &visitor) { + visitor.visit_multisetcount(*this); +} + +void MultisetCount::visit(ConstBaseTraversal &visitor) const { + visitor.visit_multisetcount(*this); +} + +bool MultisetCount::constant() const { return false; } + +Ptr MultisetCount::type() const { + const Ptr c = container->type()->resolve(); + auto m = dynamic_cast(c.get()); + if (m == nullptr) + throw Error("multisetcount container is not a multiset", container->loc); + + const Ptr lb = Ptr::make(0, loc); + const Ptr ub = + Ptr::make(m->index_bound->constant_fold() - 1, loc); + return Ptr::make(lb, ub, loc); +} + +mpz_class MultisetCount::constant_fold() const { + throw Error("multisetcount used in constant expression", loc); +} + +void MultisetCount::validate() const { + const Ptr c = container->type()->resolve(); + if (!isa(c)) + throw Error("multisetcount container is not a multiset", container->loc); + + const Ptr p = predicate->type()->resolve(); + if (!p->is_boolean()) + throw Error("multisetcount predicate is not a boolean expression", + predicate->loc); +} + +void MultisetCount::to_stream(std::ostream &out) const { + out << "multisetcount(" << identifier << ": " << *container << ", " + << *predicate << ')'; +} + +bool MultisetCount::is_pure() const { return true; } + } // namespace rumur diff --git a/librumur/src/Function.cc b/librumur/src/Function.cc index a1bb2c92..ae705e5f 100644 --- a/librumur/src/Function.cc +++ b/librumur/src/Function.cc @@ -141,6 +141,24 @@ bool Function::is_pure() const { pure &= n.function->is_pure(); } + void visit_multisetadd(const MultisetAdd &n) final { + dispatch(*n.arg0); + dispatch(*n.arg1); + pure &= !is_global_ref(*n.arg1); + } + + void visit_multisetremove(const MultisetRemove &n) final { + dispatch(*n.arg0); + dispatch(*n.arg1); + pure &= !is_global_ref(*n.arg1); + } + + void visit_multisetremovepred(const MultisetRemovePred &n) final { + dispatch(*n.container); + dispatch(*n.predicate); + pure &= !is_global_ref(*n.container); + } + void visit_propertystmt(const PropertyStmt &) final { // treat any property statement as a side effect pure = false; diff --git a/librumur/src/Model.cc b/librumur/src/Model.cc index 4bcee137..0886e2ff 100644 --- a/librumur/src/Model.cc +++ b/librumur/src/Model.cc @@ -66,6 +66,27 @@ mpz_class Model::liveness_count() const { mpz_class count = 0; mpz_class multiplier = 1; + void visit_choose(const Choose &n) final { + // adjust the multiplier for the number of copies of the contained rules + // we will eventually generate + const Ptr t = n.container->type()->resolve(); + auto m = dynamic_cast(t.get()); + if (m == nullptr) + throw Error("container in choose rule is not a multiset", + n.container->loc); + const mpz_class bound = m->index_bound->constant_fold(); + if (bound > 0) + multiplier *= bound; + + // descend into our rule children + for (const Ptr &r : n.rules) + dispatch(*r); + + // undo the multiplier effect + if (bound > 0) + multiplier /= bound; + } + void visit_ruleset(const Ruleset &n) final { /* Adjust the multiplier for the number of copies of the contained rules * we will eventually generate. diff --git a/librumur/src/Rule.cc b/librumur/src/Rule.cc index af54ffc1..6bcb5f86 100644 --- a/librumur/src/Rule.cc +++ b/librumur/src/Rule.cc @@ -1,6 +1,8 @@ +#include "../../common/isa.h" #include "location.hh" #include #include +#include #include #include #include @@ -9,6 +11,7 @@ #include #include #include +#include #include #include #include @@ -162,4 +165,40 @@ std::vector> Ruleset::flatten() const { return rs; } +Choose::Choose(const std::string &identifier_, const Ptr &container_, + const std::vector> &rules_, const location &loc_) + : Rule("", loc_), identifier(identifier_), container(container_), + rules(rules_) {} + +Choose *Choose::clone() const { return new Choose(*this); } + +void Choose::validate() const { + const Ptr t = container->type()->resolve(); + if (!isa(t)) + throw Error("choose rule container is not a multiset", container->loc); +} + +void Choose::visit(BaseTraversal &visitor) { visitor.visit_choose(*this); } + +void Choose::visit(ConstBaseTraversal &visitor) const { + visitor.visit_choose(*this); +} + +std::vector> Choose::flatten() const { + const Ptr t = container->type()->resolve(); + auto m = dynamic_cast(t.get()); + if (m == nullptr) + throw Error("container in choose rule is not a multiset", container->loc); + const mpz_class multiplier = m->index_bound->constant_fold(); + + std::vector> rs; + for (const Ptr &r : rules) { + for (Ptr &f : r->flatten()) { + for (mpz_class i = 0; i < multiplier; ++i) + rs.push_back(f); + } + } + return rs; +} + } // namespace rumur diff --git a/librumur/src/Stmt.cc b/librumur/src/Stmt.cc index adad9287..4b6162f9 100644 --- a/librumur/src/Stmt.cc +++ b/librumur/src/Stmt.cc @@ -155,6 +155,90 @@ void If::visit(BaseTraversal &visitor) { visitor.visit_if(*this); } void If::visit(ConstBaseTraversal &visitor) const { visitor.visit_if(*this); } +MultisetAdd::MultisetAdd(const Ptr &arg0_, const Ptr &arg1_, + const location &loc_) + : Stmt(loc_), arg0(arg0_), arg1(arg1_) {} + +MultisetAdd *MultisetAdd::clone() const { return new MultisetAdd(*this); } + +void MultisetAdd::validate() const { + const Ptr t1 = arg1->type()->resolve(); + auto m = dynamic_cast(t1.get()); + if (m == nullptr) + throw Error("second argument to multisetadd is not a multiset", arg1->loc); + + if (!arg0->type()->coerces_to(*m->element_type)) + throw Error("incompatible multisetadd arguments", loc); +} + +void MultisetAdd::visit(BaseTraversal &visitor) { + visitor.visit_multisetadd(*this); +} + +void MultisetAdd::visit(ConstBaseTraversal &visitor) const { + visitor.visit_multisetadd(*this); +} + +MultisetRemove::MultisetRemove(const Ptr &arg0_, const Ptr &arg1_, + const location &loc_) + : Stmt(loc_), arg0(arg0_), arg1(arg1_) {} + +MultisetRemove *MultisetRemove::clone() const { + return new MultisetRemove(*this); +} + +void MultisetRemove::validate() const { + const Ptr t1 = arg1->type()->resolve(); + auto m = dynamic_cast(t1.get()); + if (m == nullptr) + throw Error("second argument to MultisetRemove is not a multiset", + arg1->loc); + + const Scalarset s{m->index_bound, m->index_bound->loc}; + + if (!arg0->type()->coerces_to(s)) + throw Error("incompatible MultisetRemove arguments", loc); +} + +void MultisetRemove::visit(BaseTraversal &visitor) { + visitor.visit_multisetremove(*this); +} + +void MultisetRemove::visit(ConstBaseTraversal &visitor) const { + visitor.visit_multisetremove(*this); +} + +MultisetRemovePred::MultisetRemovePred(const std::string &identifier_, + const Ptr &container_, + const Ptr &predicate_, + const location &loc_) + : Stmt(loc_), identifier(identifier_), container(container_), + predicate(predicate_) {} + +MultisetRemovePred *MultisetRemovePred::clone() const { + return new MultisetRemovePred(*this); +} + +void MultisetRemovePred::validate() const { + const Ptr t = container->type()->resolve(); + auto m = dynamic_cast(t.get()); + if (m == nullptr) + throw Error("container in MultisetRemovePred is not a multiset", + container->loc); + + if (!predicate->type()->resolve()->is_boolean()) + throw Error("MultisetRemovePred predicate is not a boolean expression", + predicate->loc); +} + +void MultisetRemovePred::visit(BaseTraversal &visitor) { + visitor.visit_multisetremovepred(*this); +} + +void MultisetRemovePred::visit(ConstBaseTraversal &visitor) const { + visitor.visit_multisetremovepred(*this); +} + ProcedureCall::ProcedureCall(const std::string &name, const std::vector> &arguments, const location &loc_) diff --git a/librumur/src/TypeExpr.cc b/librumur/src/TypeExpr.cc index ff31dd9f..f8f30182 100644 --- a/librumur/src/TypeExpr.cc +++ b/librumur/src/TypeExpr.cc @@ -109,6 +109,18 @@ static bool equal(const TypeExpr &t1, const TypeExpr &t2) { } } + void visit_multiset(const Multiset &n) final { + if (auto m = dynamic_cast(t.get())) { + if (m->index_bound->constant_fold() != n.index_bound->constant_fold()) { + result = false; + } else if (!equal(*m->element_type, *n.element_type)) { + result = false; + } + } else { + result = false; + } + } + void visit_range(const Range &n) final { if (auto r = dynamic_cast(t.get())) { result = r->min->constant_fold() == n.min->constant_fold() && @@ -443,6 +455,51 @@ void Array::to_stream(std::ostream &out) const { out << "array [" << *index_type << "] of " << *element_type; } +Multiset::Multiset(const Ptr &index_bound_, + const Ptr &element_type_, const location &loc_) + : TypeExpr(loc_), index_bound(index_bound_), element_type(element_type_) {} + +Multiset *Multiset::clone() const { return new Multiset(*this); } + +void Multiset::visit(BaseTraversal &visitor) { visitor.visit_multiset(*this); } + +void Multiset::visit(ConstBaseTraversal &visitor) const { + visitor.visit_multiset(*this); +} + +mpz_class Multiset::width() const { + const mpz_class indices = index_bound->constant_fold(); + const mpz_class element_width = element_type->width(); + return indices * element_width; +} + +mpz_class Multiset::count() const { + const mpz_class indices = index_bound->constant_fold(); + + if (indices == 0) + return 0; + + const mpz_class element_count = element_type->count(); + + mpz_class s = 1; + for (mpz_class i = 0; i < indices; ++i) + s *= element_count; + return s; +} + +void Multiset::validate() const { + if (!index_bound->constant()) + throw Error("multiset bound is not a constant", index_bound->loc); + + const mpz_class b = index_bound->constant_fold(); + if (b < 0) + throw Error("multiset bound is negative, " + b.get_str(), index_bound->loc); +} + +void Multiset::to_stream(std::ostream &out) const { + out << "multiset [" << *index_bound << "] of " << *element_type; +} + TypeExprID::TypeExprID(const std::string &name_, const Ptr &referent_, const location &loc_) : TypeExpr(loc_), name(name_), referent(referent_) {} diff --git a/librumur/src/indexer.cc b/librumur/src/indexer.cc index e2cf265e..9b871d67 100644 --- a/librumur/src/indexer.cc +++ b/librumur/src/indexer.cc @@ -67,6 +67,13 @@ void Indexer::visit_bexpr(BinaryExpr &n) { dispatch(*n.rhs); } +void Indexer::visit_choose(Choose &n) { + n.unique_id = next++; + dispatch(*n.container); + for (Ptr &r : n.rules) + dispatch(*r); +} + void Indexer::visit_clear(Clear &n) { n.unique_id = next++; dispatch(*n.rhs); @@ -185,6 +192,36 @@ void Indexer::visit_model(Model &n) { void Indexer::visit_mul(Mul &n) { visit_bexpr(n); } +void Indexer::visit_multiset(Multiset &n) { + n.unique_id = next++; + dispatch(*n.index_bound); + dispatch(*n.element_type); +} + +void Indexer::visit_multisetadd(MultisetAdd &n) { + n.unique_id = next++; + dispatch(*n.arg0); + dispatch(*n.arg1); +} + +void Indexer::visit_multisetcount(MultisetCount &n) { + n.unique_id = next++; + dispatch(*n.container); + dispatch(*n.predicate); +} + +void Indexer::visit_multisetremove(MultisetRemove &n) { + n.unique_id = next++; + dispatch(*n.arg0); + dispatch(*n.arg1); +} + +void Indexer::visit_multisetremovepred(MultisetRemovePred &n) { + n.unique_id = next++; + dispatch(*n.container); + dispatch(*n.predicate); +} + void Indexer::visit_negative(Negative &n) { visit_uexpr(n); } void Indexer::visit_neq(Neq &n) { visit_bexpr(n); } diff --git a/librumur/src/lexer.l b/librumur/src/lexer.l index e5bc910b..219e20bd 100644 --- a/librumur/src/lexer.l +++ b/librumur/src/lexer.l @@ -60,66 +60,74 @@ throw rumur::Error("real types are not supported", *loc); } -alias { return rumur::parser::token::ALIAS; } -array { return rumur::parser::token::ARRAY; } -assert { return rumur::parser::token::ASSERT; } -assume { return rumur::parser::token::ASSUME; } -begin { return rumur::parser::token::BEGIN_TOK; } -boolean { return rumur::parser::token::BOOLEAN; } -by { return rumur::parser::token::BY; } -case { return rumur::parser::token::CASE; } -clear { return rumur::parser::token::CLEAR; } -const { return rumur::parser::token::CONST; } -cover { return rumur::parser::token::COVER; } -do { return rumur::parser::token::DO; } -else { return rumur::parser::token::ELSE; } -elsif { return rumur::parser::token::ELSIF; } -end { return rumur::parser::token::END; } -endalias { return rumur::parser::token::ENDALIAS; } -endexists { return rumur::parser::token::ENDEXISTS; } -endfor { return rumur::parser::token::ENDFOR; } -endforall { return rumur::parser::token::ENDFORALL; } -endfunction { return rumur::parser::token::ENDFUNCTION; } -endif { return rumur::parser::token::ENDIF; } -endprocedure { return rumur::parser::token::ENDPROCEDURE; } -endrecord { return rumur::parser::token::ENDRECORD; } -endrule { return rumur::parser::token::ENDRULE; } -endruleset { return rumur::parser::token::ENDRULESET; } -endstartstate { return rumur::parser::token::ENDSTARTSTATE; } -endswitch { return rumur::parser::token::ENDSWITCH; } -endwhile { return rumur::parser::token::ENDWHILE; } -enum { return rumur::parser::token::ENUM; } -error { return rumur::parser::token::ERROR; } -exists { return rumur::parser::token::EXISTS; } -for { return rumur::parser::token::FOR; } -forall { return rumur::parser::token::FORALL; } -function { return rumur::parser::token::FUNCTION; } -if { return rumur::parser::token::IF; } -invariant { return rumur::parser::token::INVARIANT; } -ismember { return rumur::parser::token::ISMEMBER; } -isundefined { return rumur::parser::token::ISUNDEFINED; } -liveness { return rumur::parser::token::LIVENESS; } -of { return rumur::parser::token::OF; } -procedure { return rumur::parser::token::PROCEDURE; } -put { return rumur::parser::token::PUT; } -real { throw rumur::Error("real types are not supported", *loc); } -record { return rumur::parser::token::RECORD; } -return { return rumur::parser::token::RETURN; } -rule { return rumur::parser::token::RULE; } -ruleset { return rumur::parser::token::RULESET; } -scalarset { return rumur::parser::token::SCALARSET; } -startstate { return rumur::parser::token::STARTSTATE; } -switch { return rumur::parser::token::SWITCH; } -then { return rumur::parser::token::THEN; } -to { return rumur::parser::token::TO; } -type { return rumur::parser::token::TYPE; } -undefine { return rumur::parser::token::UNDEFINE; } -union { return rumur::parser::token::UNION; } -var { return rumur::parser::token::VAR; } -while { return rumur::parser::token::WHILE; } - -"∀" { return rumur::parser::token::FORALL; } -"∃" { return rumur::parser::token::EXISTS; } +alias { return rumur::parser::token::ALIAS; } +array { return rumur::parser::token::ARRAY; } +assert { return rumur::parser::token::ASSERT; } +assume { return rumur::parser::token::ASSUME; } +begin { return rumur::parser::token::BEGIN_TOK; } +boolean { return rumur::parser::token::BOOLEAN; } +by { return rumur::parser::token::BY; } +case { return rumur::parser::token::CASE; } +choose { return rumur::parser::token::CHOOSE; } +clear { return rumur::parser::token::CLEAR; } +const { return rumur::parser::token::CONST; } +cover { return rumur::parser::token::COVER; } +do { return rumur::parser::token::DO; } +else { return rumur::parser::token::ELSE; } +elsif { return rumur::parser::token::ELSIF; } +end { return rumur::parser::token::END; } +endalias { return rumur::parser::token::ENDALIAS; } +endchoose { return rumur::parser::token::ENDCHOOSE; } +endexists { return rumur::parser::token::ENDEXISTS; } +endfor { return rumur::parser::token::ENDFOR; } +endforall { return rumur::parser::token::ENDFORALL; } +endfunction { return rumur::parser::token::ENDFUNCTION; } +endif { return rumur::parser::token::ENDIF; } +endprocedure { return rumur::parser::token::ENDPROCEDURE; } +endrecord { return rumur::parser::token::ENDRECORD; } +endrule { return rumur::parser::token::ENDRULE; } +endruleset { return rumur::parser::token::ENDRULESET; } +endstartstate { return rumur::parser::token::ENDSTARTSTATE; } +endswitch { return rumur::parser::token::ENDSWITCH; } +endwhile { return rumur::parser::token::ENDWHILE; } +enum { return rumur::parser::token::ENUM; } +error { return rumur::parser::token::ERROR; } +exists { return rumur::parser::token::EXISTS; } +for { return rumur::parser::token::FOR; } +forall { return rumur::parser::token::FORALL; } +function { return rumur::parser::token::FUNCTION; } +if { return rumur::parser::token::IF; } +invariant { return rumur::parser::token::INVARIANT; } +ismember { return rumur::parser::token::ISMEMBER; } +isundefined { return rumur::parser::token::ISUNDEFINED; } +liveness { return rumur::parser::token::LIVENESS; } +multiset { return rumur::parser::token::MULTISET; } +multisetadd { return rumur::parser::token::MULTISETADD; } +multisetcount { return rumur::parser::token::MULTISETCOUNT; } +multisetremove { return rumur::parser::token::MULTISETREMOVE; } +multisetremovepred { return rumur::parser::token::MULTISETREMOVEPRED; } +of { return rumur::parser::token::OF; } +procedure { return rumur::parser::token::PROCEDURE; } +put { return rumur::parser::token::PUT; } +real { throw rumur::Error("real types are not supported", *loc); } +record { return rumur::parser::token::RECORD; } +return { return rumur::parser::token::RETURN; } +rule { return rumur::parser::token::RULE; } +ruleset { return rumur::parser::token::RULESET; } +scalarset { return rumur::parser::token::SCALARSET; } +startstate { return rumur::parser::token::STARTSTATE; } +switch { return rumur::parser::token::SWITCH; } +then { return rumur::parser::token::THEN; } +to { return rumur::parser::token::TO; } +type { return rumur::parser::token::TYPE; } +undefine { return rumur::parser::token::UNDEFINE; } +undefined { return rumur::parser::token::UNDEFINED; } +union { return rumur::parser::token::UNION; } +var { return rumur::parser::token::VAR; } +while { return rumur::parser::token::WHILE; } + +"∀" { return rumur::parser::token::FORALL; } +"∃" { return rumur::parser::token::EXISTS; } /* Recognise true and false explicitly rather than as generic IDs (below). The * purpose of this is so that we match them case-insensitively. diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy index 724fdc8b..6a21264f 100644 --- a/librumur/src/parser.yy +++ b/librumur/src/parser.yy @@ -120,6 +120,7 @@ %token BOOLEAN %token BY %token CASE +%token CHOOSE %token CLEAR %token COLON_EQ ":=" %token CONST @@ -131,6 +132,7 @@ %token ELSIF %token END %token ENDALIAS +%token ENDCHOOSE %token ENDEXISTS %token ENDFOR %token ENDFORALL @@ -161,6 +163,11 @@ %token LIVENESS %token LOR "∨" %token LSH "<<" +%token MULTISET +%token MULTISETADD +%token MULTISETCOUNT +%token MULTISETREMOVE +%token MULTISETREMOVEPRED %token NEQ "!=" %token NUMBER %token OF @@ -186,6 +193,7 @@ %token TO %token TYPE %token UNDEFINE +%token UNDEFINED %token UNION %token VAR %token WHILE @@ -206,6 +214,7 @@ %type > aliasrule %type > category +%type > choose %type >> decl %type >> decls %type >> decls_header @@ -215,8 +224,10 @@ %type > expr %type , rumur::location>>> exprdecl %type , rumur::location>>> exprdecls -%type >> exprlist -%type >> exprlist_cont +%type >> exprlist_fn +%type >> exprlist_fn_cont +%type >> exprlist_sw +%type >> exprlist_sw_cont %type > guard_opt %type >> id_list %type >> id_list_opt @@ -307,6 +318,10 @@ category: ASSERT { $$ = std::make_shared(rumur::Property::LIVENESS); }; +choose: CHOOSE ID ':' expr DO rules endchoose { + $$ = rumur::Ptr::make($2, $4, $6, @$); +}; + comma_opt: ',' | %empty; decl: CONST exprdecls { @@ -351,6 +366,7 @@ elsifs: elsifs ELSIF expr THEN stmts { }; endalias: END | ENDALIAS; +endchoose: END | ENDCHOOSE; endexists: END | ENDEXISTS; endfor: END | ENDFOR; endforall: END | ENDFORALL; @@ -435,12 +451,14 @@ expr: expr '?' expr ':' expr { } | '(' expr ')' { $$ = $2; $$->loc = @$; -} | ID '(' exprlist ')' { +} | ID '(' exprlist_fn ')' { $$ = rumur::Ptr::make($1, $3, @$); } | ISMEMBER '(' expr ',' typeexpr ')' { $$ = rumur::Ptr::make($3, $5, @$); } | ISUNDEFINED '(' designator ')' { $$ = rumur::Ptr::make($3, @$); +} | MULTISETCOUNT '(' ID ':' expr ',' expr ')' { + $$ = rumur::Ptr::make($3, $5, $7, @$); }; exprdecl: id_list_opt ':' expr { @@ -456,13 +474,31 @@ exprdecls: exprdecls exprdecl semi_opt { /* nothing required */ }; -exprlist: exprlist_cont expr comma_opt { +exprlist_fn: exprlist_fn_cont expr comma_opt { $$ = $1; $$.push_back($2); +} | exprlist_fn_cont UNDEFINED comma_opt { + $$ = $1; + $$.push_back(rumur::Ptr::make("undefined", nullptr, @2)); } | %empty { }; -exprlist_cont: exprlist_cont expr ',' { +exprlist_fn_cont: exprlist_fn_cont expr ',' { + $$ = $1; + $$.push_back($2); +} | exprlist_fn_cont UNDEFINED ',' { + $$ = $1; + $$.push_back(rumur::Ptr::make("undefined", nullptr, @2)); +} | %empty { +}; + +exprlist_sw: exprlist_sw_cont expr comma_opt { + $$ = $1; + $$.push_back($2); +} | %empty { +}; + +exprlist_sw_cont: exprlist_sw_cont expr ',' { $$ = $1; $$.push_back($2); } | %empty { @@ -548,6 +584,8 @@ rule: startstate { $$ = $1; } | aliasrule { $$ = $1; +} | choose { + $$ = $1; }; rules: rules rule semi_opt { @@ -580,6 +618,8 @@ stmt: category STRING expr { $$ = rumur::Ptr::make(p, $3, @$); } | designator COLON_EQ expr { $$ = rumur::Ptr::make($1, $3, @$); +} | designator COLON_EQ UNDEFINED { + $$ = rumur::Ptr::make($1, @$); } | ALIAS exprdecls DO stmts endalias { std::vector> decls; for (const std::tuple, rumur::location> &d : $2) { @@ -598,6 +638,12 @@ stmt: category STRING expr { cs.insert(cs.end(), $5.begin(), $5.end()); cs.insert(cs.end(), $6.begin(), $6.end()); $$ = rumur::Ptr::make(cs, @$); +} | MULTISETADD '(' expr ',' expr ')' { + $$ = rumur::Ptr::make($3, $5, @$); +} | MULTISETREMOVE '(' expr ',' expr ')' { + $$ = rumur::Ptr::make($3, $5, @$); +} | MULTISETREMOVEPRED '(' ID ':' expr ',' expr ')' { + $$ = rumur::Ptr::make($3, $5, $7, @$); } | PUT STRING { $$ = rumur::Ptr::make($2, @$); } | PUT expr { @@ -608,7 +654,7 @@ stmt: category STRING expr { $$ = rumur::Ptr::make($2, @$); } | UNDEFINE designator { $$ = rumur::Ptr::make($2, @$); -} | ID '(' exprlist ')' { +} | ID '(' exprlist_fn ')' { $$ = rumur::Ptr::make($1, $3, @$); } | WHILE expr DO stmts endwhile { $$ = rumur::Ptr::make($2, $4, @$); @@ -644,7 +690,7 @@ switchcases: switchcases_cont ELSE stmts { $$ = $1; }; -switchcases_cont: switchcases_cont CASE exprlist ':' stmts { +switchcases_cont: switchcases_cont CASE exprlist_sw ':' stmts { $$ = $1; $$.push_back(rumur::SwitchCase($3, $5, @$)); } | %empty { @@ -680,6 +726,8 @@ typeexpr: BOOLEAN { $$ = rumur::Ptr::make($2, @$); } | ARRAY '[' typeexpr ']' OF typeexpr { $$ = rumur::Ptr::make($3, $6, @$); +} | MULTISET '[' expr ']' OF typeexpr { + $$ = rumur::Ptr::make($3, $6, @$); } | SCALARSET '(' expr ')' { $$ = rumur::Ptr::make($3, @$); } | UNION '{' typeexprs '}' { diff --git a/librumur/src/resolve-symbols.cc b/librumur/src/resolve-symbols.cc index 6c243b71..5f58bf04 100644 --- a/librumur/src/resolve-symbols.cc +++ b/librumur/src/resolve-symbols.cc @@ -124,6 +124,27 @@ class Resolver : public Traversal { void visit_bor(Bor &n) final { visit_bexpr(n); } + void visit_choose(Choose &n) final { + dispatch(*n.container); + + // register our quantified variable + symtab.open_scope(); + const Ptr t = n.container->type()->resolve(); + auto m = dynamic_cast(t.get()); + if (m == nullptr) + throw Error("container of choose rule is not a multiset", + n.container->loc); + const Ptr s = + Ptr::make(m->index_bound, n.container->loc); + VarDecl *const i = make(n.identifier, s, n.loc); + symtab.declare(n.identifier, i); + + for (Ptr &r : n.rules) + dispatch(*r); + + symtab.close_scope(); + } + void visit_clear(Clear &n) final { dispatch(*n.rhs); disambiguate(n.rhs); @@ -239,8 +260,23 @@ class Resolver : public Traversal { n.function = f; } - for (auto &a : n.arguments) + + size_t i = 0; + for (auto &a : n.arguments) { + symtab.open_scope(); + + // if this argument is `undefined`, create something it can resolve to + auto id = dynamic_cast(a.get()); + if (id != nullptr && id->id == "undefined") { + VarDecl *const undef = + make("undefined", n.function->parameters[i]->type, n.loc); + symtab.declare("undefined", undef); + } + dispatch(*a); + symtab.close_scope(); + ++i; + } for (Ptr &a : n.arguments) disambiguate(a); @@ -325,6 +361,68 @@ class Resolver : public Traversal { void visit_mul(Mul &n) final { visit_bexpr(n); } + void visit_multiset(Multiset &n) final { + dispatch(*n.index_bound); + dispatch(*n.element_type); + disambiguate(n.index_bound); + } + + void visit_multisetadd(MultisetAdd &n) final { + dispatch(*n.arg0); + disambiguate(n.arg0); + dispatch(*n.arg1); + disambiguate(n.arg1); + } + + void visit_multisetcount(MultisetCount &n) final { + dispatch(*n.container); + disambiguate(n.container); + + symtab.open_scope(); + + const Ptr id_type = n.container->type()->resolve(); + auto m = dynamic_cast(id_type.get()); + if (m == nullptr) + throw Error("multisetcount container is not a multiset", + n.container->loc); + const Ptr s = Ptr::make(m->index_bound, n.loc); + VarDecl *const i = make(n.identifier, s, n.loc); + symtab.declare(n.identifier, i); + + dispatch(*n.predicate); + symtab.close_scope(); + + disambiguate(n.predicate); + } + + void visit_multisetremove(MultisetRemove &n) final { + dispatch(*n.arg0); + disambiguate(n.arg0); + dispatch(*n.arg1); + disambiguate(n.arg1); + } + + void visit_multisetremovepred(MultisetRemovePred &n) final { + dispatch(*n.container); + disambiguate(n.container); + + symtab.open_scope(); + + const Ptr id_type = n.container->type()->resolve(); + auto m = dynamic_cast(id_type.get()); + if (m == nullptr) + throw Error("multisetremovepred container is not a multiset", + n.container->loc); + const Ptr s = Ptr::make(m->index_bound, n.loc); + VarDecl *const i = make(n.identifier, s, n.loc); + symtab.declare(n.identifier, i); + + dispatch(*n.predicate); + symtab.close_scope(); + + disambiguate(n.predicate); + } + void visit_negative(Negative &n) final { visit_uexpr(n); } void visit_neq(Neq &n) final { visit_bexpr(n); } diff --git a/librumur/src/sanitise_rule_names.cc b/librumur/src/sanitise_rule_names.cc index 73b1d953..a76d9274 100644 --- a/librumur/src/sanitise_rule_names.cc +++ b/librumur/src/sanitise_rule_names.cc @@ -52,6 +52,12 @@ class RuleNamer : public Traversal { } } + void visit_choose(Choose &n) final { + name(n, "choose"); + for (Ptr &r : n.rules) + dispatch(*r); + } + void visit_propertyrule(PropertyRule &n) final { name(n, "property"); } void visit_ruleset(Ruleset &n) final { diff --git a/librumur/src/traverse.cc b/librumur/src/traverse.cc index e3dca41b..40f6ae48 100644 --- a/librumur/src/traverse.cc +++ b/librumur/src/traverse.cc @@ -66,6 +66,12 @@ void Traversal::visit_bexpr(BinaryExpr &n) { dispatch(*n.rhs); } +void Traversal::visit_choose(Choose &n) { + dispatch(*n.container); + for (Ptr &r : n.rules) + dispatch(*r); +} + void Traversal::visit_clear(Clear &n) { dispatch(*n.rhs); } void Traversal::visit_constdecl(ConstDecl &n) { dispatch(*n.value); } @@ -159,6 +165,31 @@ void Traversal::visit_model(Model &n) { void Traversal::visit_mul(Mul &n) { visit_bexpr(n); } +void Traversal::visit_multiset(Multiset &n) { + dispatch(*n.index_bound); + dispatch(*n.element_type); +} + +void Traversal::visit_multisetadd(MultisetAdd &n) { + dispatch(*n.arg0); + dispatch(*n.arg1); +} + +void Traversal::visit_multisetcount(MultisetCount &n) { + dispatch(*n.container); + dispatch(*n.predicate); +} + +void Traversal::visit_multisetremove(MultisetRemove &n) { + dispatch(*n.arg0); + dispatch(*n.arg1); +} + +void Traversal::visit_multisetremovepred(MultisetRemovePred &n) { + dispatch(*n.container); + dispatch(*n.predicate); +} + void Traversal::visit_negative(Negative &n) { visit_uexpr(n); } void Traversal::visit_neq(Neq &n) { visit_bexpr(n); } @@ -345,6 +376,12 @@ void ConstTraversal::visit_bexpr(const BinaryExpr &n) { dispatch(*n.rhs); } +void ConstTraversal::visit_choose(const Choose &n) { + dispatch(*n.container); + for (const Ptr &r : n.rules) + dispatch(*r); +} + void ConstTraversal::visit_clear(const Clear &n) { dispatch(*n.rhs); } void ConstTraversal::visit_constdecl(const ConstDecl &n) { dispatch(*n.value); } @@ -438,6 +475,31 @@ void ConstTraversal::visit_model(const Model &n) { void ConstTraversal::visit_mul(const Mul &n) { visit_bexpr(n); } +void ConstTraversal::visit_multiset(const Multiset &n) { + dispatch(*n.index_bound); + dispatch(*n.element_type); +} + +void ConstTraversal::visit_multisetadd(const MultisetAdd &n) { + dispatch(*n.arg0); + dispatch(*n.arg1); +} + +void ConstTraversal::visit_multisetcount(const MultisetCount &n) { + dispatch(*n.container); + dispatch(*n.predicate); +} + +void ConstTraversal::visit_multisetremove(const MultisetRemove &n) { + dispatch(*n.arg0); + dispatch(*n.arg1); +} + +void ConstTraversal::visit_multisetremovepred(const MultisetRemovePred &n) { + dispatch(*n.container); + dispatch(*n.predicate); +} + void ConstTraversal::visit_negative(const Negative &n) { visit_uexpr(n); } void ConstTraversal::visit_neq(const Neq &n) { visit_bexpr(n); } @@ -603,6 +665,12 @@ void ConstExprTraversal::visit_assignment(const Assignment &n) { dispatch(*n.rhs); } +void ConstExprTraversal::visit_choose(const Choose &n) { + dispatch(*n.container); + for (const Ptr &r : n.rules) + dispatch(*r); +} + void ConstExprTraversal::visit_clear(const Clear &n) { dispatch(*n.rhs); } void ConstExprTraversal::visit_constdecl(const ConstDecl &n) { @@ -647,6 +715,26 @@ void ConstExprTraversal::visit_model(const Model &n) { dispatch(*c); } +void ConstExprTraversal::visit_multiset(const Multiset &n) { + dispatch(*n.index_bound); + dispatch(*n.element_type); +} + +void ConstExprTraversal::visit_multisetadd(const MultisetAdd &n) { + dispatch(*n.arg0); + dispatch(*n.arg1); +} + +void ConstExprTraversal::visit_multisetremove(const MultisetRemove &n) { + dispatch(*n.arg0); + dispatch(*n.arg1); +} + +void ConstExprTraversal::visit_multisetremovepred(const MultisetRemovePred &n) { + dispatch(*n.container); + dispatch(*n.predicate); +} + void ConstExprTraversal::visit_procedurecall(const ProcedureCall &n) { dispatch(n.call); } @@ -795,6 +883,12 @@ void ConstStmtTraversal::visit_bexpr(const BinaryExpr &n) { dispatch(*n.rhs); } +void ConstStmtTraversal::visit_choose(const Choose &n) { + dispatch(*n.container); + for (const Ptr &r : n.rules) + dispatch(*r); +} + void ConstStmtTraversal::visit_constdecl(const ConstDecl &n) { dispatch(*n.value); } @@ -879,6 +973,16 @@ void ConstStmtTraversal::visit_model(const Model &n) { void ConstStmtTraversal::visit_mul(const Mul &n) { visit_bexpr(n); } +void ConstStmtTraversal::visit_multiset(const Multiset &n) { + dispatch(*n.index_bound); + dispatch(*n.element_type); +} + +void ConstStmtTraversal::visit_multisetcount(const MultisetCount &n) { + dispatch(*n.container); + dispatch(*n.predicate); +} + void ConstStmtTraversal::visit_negative(const Negative &n) { visit_uexpr(n); } void ConstStmtTraversal::visit_neq(const Neq &n) { visit_bexpr(n); } @@ -1026,6 +1130,12 @@ void ConstTypeTraversal::visit_bexpr(const BinaryExpr &n) { dispatch(*n.rhs); } +void ConstTypeTraversal::visit_choose(const Choose &n) { + dispatch(*n.container); + for (const Ptr &r : n.rules) + dispatch(*r); +} + void ConstTypeTraversal::visit_clear(const Clear &n) { dispatch(*n.rhs); } void ConstTypeTraversal::visit_constdecl(const ConstDecl &n) { @@ -1123,6 +1233,26 @@ void ConstTypeTraversal::visit_model(const Model &n) { void ConstTypeTraversal::visit_mul(const Mul &n) { visit_bexpr(n); } +void ConstTypeTraversal::visit_multisetadd(const MultisetAdd &n) { + dispatch(*n.arg0); + dispatch(*n.arg1); +} + +void ConstTypeTraversal::visit_multisetcount(const MultisetCount &n) { + dispatch(*n.container); + dispatch(*n.predicate); +} + +void ConstTypeTraversal::visit_multisetremove(const MultisetRemove &n) { + dispatch(*n.arg0); + dispatch(*n.arg1); +} + +void ConstTypeTraversal::visit_multisetremovepred(const MultisetRemovePred &n) { + dispatch(*n.container); + dispatch(*n.predicate); +} + void ConstTypeTraversal::visit_negative(const Negative &n) { visit_uexpr(n); } void ConstTypeTraversal::visit_neq(const Neq &n) { visit_bexpr(n); } diff --git a/librumur/src/validate.cc b/librumur/src/validate.cc index 31c7f785..9f387946 100644 --- a/librumur/src/validate.cc +++ b/librumur/src/validate.cc @@ -95,6 +95,12 @@ class Validator : public ConstBaseTraversal { n.validate(); } + void visit_choose(const Choose &n) final { + dispatch(*n.container); + for (const Ptr &r : n.rules) + dispatch(*r); + } + void visit_clear(const Clear &n) final { dispatch(*n.rhs); n.validate(); @@ -254,6 +260,36 @@ class Validator : public ConstBaseTraversal { n.validate(); } + void visit_multiset(const Multiset &n) final { + dispatch(*n.index_bound); + dispatch(*n.element_type); + n.validate(); + } + + void visit_multisetadd(const MultisetAdd &n) final { + dispatch(*n.arg0); + dispatch(*n.arg1); + n.validate(); + } + + void visit_multisetcount(const MultisetCount &n) final { + dispatch(*n.container); + dispatch(*n.predicate); + n.validate(); + } + + void visit_multisetremove(const MultisetRemove &n) final { + dispatch(*n.arg0); + dispatch(*n.arg1); + n.validate(); + } + + void visit_multisetremovepred(const MultisetRemovePred &n) final { + dispatch(*n.container); + dispatch(*n.predicate); + n.validate(); + } + void visit_negative(const Negative &n) final { dispatch(*n.rhs); n.validate(); diff --git a/misc/murphi2xml.rng b/misc/murphi2xml.rng index ad6fe4f2..42ac9e11 100644 --- a/misc/murphi2xml.rng +++ b/misc/murphi2xml.rng @@ -83,6 +83,14 @@ + + + + + + + + @@ -160,6 +168,22 @@ + + + + + + + + + + + + + + + + @@ -297,6 +321,7 @@ + @@ -419,11 +444,7 @@ - - - - - + @@ -595,6 +616,7 @@ + @@ -612,6 +634,67 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -825,6 +908,7 @@ + @@ -989,6 +1073,9 @@ + + + @@ -1096,6 +1183,7 @@ + diff --git a/murphi-format/src/format.c b/murphi-format/src/format.c index 75939879..e3524b17 100644 --- a/murphi-format/src/format.c +++ b/murphi-format/src/format.c @@ -232,6 +232,8 @@ static bool is_keyword(const char *text) { return true; if (streq(text, "case")) return true; + if (streq(text, "choose")) + return true; if (streq(text, "clear")) return true; if (streq(text, "const")) @@ -248,6 +250,8 @@ static bool is_keyword(const char *text) { return true; if (streq(text, "endalias")) return true; + if (streq(text, "endchoose")) + return true; if (streq(text, "endexists")) return true; if (streq(text, "endfor")) @@ -298,6 +302,23 @@ static bool is_keyword(const char *text) { #endif if (streq(text, "liveness")) return true; +#if 0 + // it is more intuitive to suppress space between `multiset` and `[` + if (streq(text, "multiset")) + return true; + // `multisetadd` is a keyword, but is used as if it were a function + if (streq(text, "multisetadd")) + return true; + // `multisetcount` is a keyword, but is used as if it were a function + if (streq(text, "multisetcount")) + return true; + // `multisetremove` is a keyword, but is used as if it were a function + if (streq(text, "multisetremove")) + return true; + // `multisetremovepred` is a keyword, but is used as if it were a function + if (streq(text, "multisetremovepred")) + return true; +#endif if (streq(text, "of")) return true; if (streq(text, "procedure")) @@ -377,6 +398,8 @@ static bool is_block_starter(state_t st, const char *text) { return true; if (streq(text, "case")) return true; + if (streq(text, "choose")) + return true; if (streq(text, "const")) return true; if (streq(text, "invariant")) @@ -442,6 +465,8 @@ static bool is_dedenter(const char *text) { return true; if (streq(text, "endalias")) return true; + if (streq(text, "endchoose")) + return true; if (streq(text, "endexists")) return true; if (streq(text, "endfor")) diff --git a/murphi2c/src/CLikeGenerator.cc b/murphi2c/src/CLikeGenerator.cc index 013d8639..8949c167 100644 --- a/murphi2c/src/CLikeGenerator.cc +++ b/murphi2c/src/CLikeGenerator.cc @@ -181,6 +181,11 @@ void CLikeGenerator::visit_bor(const Bor &n) { *this << "(" << *n.lhs << " | " << *n.rhs << ")"; } +void CLikeGenerator::visit_choose(const Choose &) { + assert(!"choose was not rejected during check()"); + __builtin_unreachable(); +} + void CLikeGenerator::visit_clear(const Clear &n) { *this << indentation() << "memset(&" << *n.rhs << ", 0, sizeof(" << *n.rhs << "));"; @@ -200,6 +205,7 @@ void CLikeGenerator::visit_element(const Element &n) { // find the type of the array expression const Ptr t = n.array->type()->resolve(); + assert(!isa(t) && "multiset was not rejected during check()"); auto a = dynamic_cast(t.get()); assert(a != nullptr && "non-array on LHS of array indexing expression"); @@ -430,6 +436,31 @@ void CLikeGenerator::visit_mul(const Mul &n) { *this << "(" << *n.lhs << " * " << *n.rhs << ")"; } +void CLikeGenerator::visit_multiset(const Multiset &) { + assert(!"multiset was not rejected during check()"); + __builtin_unreachable(); +} + +void CLikeGenerator::visit_multisetadd(const MultisetAdd &) { + assert(!"multisetadd was not rejected during check()"); + __builtin_unreachable(); +} + +void CLikeGenerator::visit_multisetcount(const MultisetCount &) { + assert(!"multisetcount was not rejected during check()"); + __builtin_unreachable(); +} + +void CLikeGenerator::visit_multisetremove(const MultisetRemove &) { + assert(!"multisetremove was not rejected during check()"); + __builtin_unreachable(); +} + +void CLikeGenerator::visit_multisetremovepred(const MultisetRemovePred &) { + assert(!"multisetremovepred was not rejected during check()"); + __builtin_unreachable(); +} + void CLikeGenerator::visit_negative(const Negative &n) { *this << "(-" << *n.rhs << ")"; } @@ -526,6 +557,8 @@ void CLikeGenerator::print(const std::string &suffix, const TypeExpr &t, const Ptr type = t.resolve(); + assert(!isa(type) && + "multiset type was not rejected during check()"); assert(!isa(type) && "union type was not rejected during check()"); // if this is boolean, handle it separately to other Enums to avoid diff --git a/murphi2c/src/CLikeGenerator.h b/murphi2c/src/CLikeGenerator.h index fe0d6d09..4470c02d 100644 --- a/murphi2c/src/CLikeGenerator.h +++ b/murphi2c/src/CLikeGenerator.h @@ -47,6 +47,7 @@ class __attribute__((visibility("hidden"))) CLikeGenerator void visit_band(const rumur::Band &n) final; void visit_bnot(const rumur::Bnot &n) final; void visit_bor(const rumur::Bor &n) final; + void visit_choose(const rumur::Choose &n) final; void visit_clear(const rumur::Clear &n) final; void visit_div(const rumur::Div &n) final; void visit_element(const rumur::Element &n) final; @@ -72,6 +73,11 @@ class __attribute__((visibility("hidden"))) CLikeGenerator void visit_mod(const rumur::Mod &n) final; void visit_model(const rumur::Model &n) final; void visit_mul(const rumur::Mul &n) final; + void visit_multiset(const rumur::Multiset &n) final; + void visit_multisetadd(const rumur::MultisetAdd &n) final; + void visit_multisetcount(const rumur::MultisetCount &n) final; + void visit_multisetremove(const rumur::MultisetRemove &n) final; + void visit_multisetremovepred(const rumur::MultisetRemovePred &n) final; void visit_negative(const rumur::Negative &n) final; void visit_neq(const rumur::Neq &n) final; void visit_not(const rumur::Not &n) final; diff --git a/murphi2c/src/check.cc b/murphi2c/src/check.cc index b57f824d..f7231a86 100644 --- a/murphi2c/src/check.cc +++ b/murphi2c/src/check.cc @@ -13,6 +13,13 @@ class Check : public ConstTraversal { public: bool ok = true; + void visit_choose(const Choose &) final { + if (ok) { + std::cerr << "choose rules are not supported\n"; + ok = false; + } + } + void visit_ismember(const IsMember &) final { if (ok) { std::cerr << "ismember expressions are not supported\n"; @@ -27,6 +34,41 @@ class Check : public ConstTraversal { } } + void visit_multiset(const Multiset &) final { + if (ok) { + std::cerr << "multiset types are not supported\n"; + ok = false; + } + } + + void visit_multisetadd(const MultisetAdd &) final { + if (ok) { + std::cerr << "multiset types are not supported\n"; + ok = false; + } + } + + void visit_multisetcount(const MultisetCount &) final { + if (ok) { + std::cerr << "multiset types are not supported\n"; + ok = false; + } + } + + void visit_multisetremove(const MultisetRemove &) final { + if (ok) { + std::cerr << "multiset types are not supported\n"; + ok = false; + } + } + + void visit_multisetremovepred(const MultisetRemovePred &) final { + if (ok) { + std::cerr << "multiset types are not supported\n"; + ok = false; + } + } + void visit_union(const Union &) final { if (ok) { std::cerr << "union types are not supported\n"; diff --git a/murphi2murphi/src/DecomposeComplexComparisons.cc b/murphi2murphi/src/DecomposeComplexComparisons.cc index 83eb7f44..4c2d65d2 100644 --- a/murphi2murphi/src/DecomposeComplexComparisons.cc +++ b/murphi2murphi/src/DecomposeComplexComparisons.cc @@ -67,9 +67,9 @@ static std::string explode(std::unordered_set &ids, const Ptr t = type.resolve(); - // if this is a union, assume there is no reasonable way to decompose its - // comparison - if (isa(t)) { + // if this is a multiset or union, assume there is no reasonable way to + // decompose its comparison + if (isa(t) || isa(t)) { buf << prefix_a << stem << (is_eq ? " = " : " != ") << prefix_b << stem; return buf.str(); } @@ -114,6 +114,12 @@ void DecomposeComplexComparisons::rewrite(const EquatableBinaryExpr &n, return; } + // if either side is of multiset type, we cannot decompose this + if (isa(lhs_type) || isa(rhs_type)) { + next.dispatch(n); + return; + } + // if either side is of union type, we cannot decompose this if (isa(lhs_type) || isa(rhs_type)) { next.dispatch(n); diff --git a/murphi2murphi/src/ExplicitSemicolons.cc b/murphi2murphi/src/ExplicitSemicolons.cc index d146dc0f..4c699d89 100644 --- a/murphi2murphi/src/ExplicitSemicolons.cc +++ b/murphi2murphi/src/ExplicitSemicolons.cc @@ -63,6 +63,10 @@ void ExplicitSemicolons::visit_aliasrule(const AliasRule &n) { next.visit_aliasrule(n); set_pending_semi(); } +void ExplicitSemicolons::visit_choose(const Choose &n) { + next.visit_choose(n); + set_pending_semi(); +} void ExplicitSemicolons::visit_constdecl(const ConstDecl &n) { next.visit_constdecl(n); set_pending_semi(); diff --git a/murphi2murphi/src/ExplicitSemicolons.h b/murphi2murphi/src/ExplicitSemicolons.h index d069b65e..a23e9948 100644 --- a/murphi2murphi/src/ExplicitSemicolons.h +++ b/murphi2murphi/src/ExplicitSemicolons.h @@ -25,6 +25,7 @@ class ExplicitSemicolons : public IntermediateStage { // override visitors for all nodes that can have an omitted semicolon void visit_aliasrule(const rumur::AliasRule &n) final; + void visit_choose(const rumur::Choose &n) final; void visit_constdecl(const rumur::ConstDecl &n) final; void visit_function(const rumur::Function &n) final; void visit_propertyrule(const rumur::PropertyRule &n) final; diff --git a/murphi2murphi/src/Printer.cc b/murphi2murphi/src/Printer.cc index aba94151..e7ec8ac9 100644 --- a/murphi2murphi/src/Printer.cc +++ b/murphi2murphi/src/Printer.cc @@ -82,6 +82,17 @@ void Printer::visit_assignment(const Assignment &n) { top->sync_to(n.loc.end); } +void Printer::visit_choose(const Choose &n) { + top->sync_to(n); + top->sync_to(*n.container); + top->dispatch(*n.container); + for (const Ptr &r : n.rules) { + top->sync_to(*r); + top->dispatch(*r); + } + top->sync_to(n.loc.end); +} + void Printer::visit_clear(const Clear &n) { top->sync_to(n); top->sync_to(*n.rhs); @@ -269,6 +280,51 @@ void Printer::visit_model(const Model &n) { void Printer::visit_mul(const Mul &n) { visit_bexpr(n); } +void Printer::visit_multiset(const Multiset &n) { + top->sync_to(n); + top->sync_to(*n.index_bound); + top->dispatch(*n.index_bound); + top->sync_to(*n.element_type); + top->dispatch(*n.element_type); + top->sync_to(n.loc.end); +} + +void Printer::visit_multisetadd(const MultisetAdd &n) { + top->sync_to(n); + top->sync_to(*n.arg0); + top->dispatch(*n.arg0); + top->sync_to(*n.arg1); + top->dispatch(*n.arg1); + top->sync_to(n.loc.end); +} + +void Printer::visit_multisetcount(const MultisetCount &n) { + top->sync_to(n); + top->sync_to(*n.container); + top->dispatch(*n.container); + top->sync_to(*n.predicate); + top->dispatch(*n.predicate); + top->sync_to(n.loc.end); +} + +void Printer::visit_multisetremove(const MultisetRemove &n) { + top->sync_to(n); + top->sync_to(*n.arg0); + top->dispatch(*n.arg0); + top->sync_to(*n.arg1); + top->dispatch(*n.arg1); + top->sync_to(n.loc.end); +} + +void Printer::visit_multisetremovepred(const MultisetRemovePred &n) { + top->sync_to(n); + top->sync_to(*n.container); + top->dispatch(*n.container); + top->sync_to(*n.predicate); + top->dispatch(*n.predicate); + top->sync_to(n.loc.end); +} + void Printer::visit_negative(const Negative &n) { visit_uexpr(n); } void Printer::visit_neq(const Neq &n) { visit_bexpr(n); } diff --git a/murphi2murphi/src/Printer.h b/murphi2murphi/src/Printer.h index c1bc53d6..9a428531 100644 --- a/murphi2murphi/src/Printer.h +++ b/murphi2murphi/src/Printer.h @@ -28,6 +28,7 @@ class Printer : public Stage { void visit_band(const rumur::Band &n) final; void visit_bnot(const rumur::Bnot &n) final; void visit_bor(const rumur::Bor &n) final; + void visit_choose(const rumur::Choose &n) final; void visit_clear(const rumur::Clear &n) final; void visit_constdecl(const rumur::ConstDecl &n) final; void visit_div(const rumur::Div &n) final; @@ -55,6 +56,11 @@ class Printer : public Stage { void visit_mod(const rumur::Mod &n) final; void visit_model(const rumur::Model &n) final; void visit_mul(const rumur::Mul &n) final; + void visit_multiset(const rumur::Multiset &n) final; + void visit_multisetadd(const rumur::MultisetAdd &n) final; + void visit_multisetremove(const rumur::MultisetRemove &n) final; + void visit_multisetremovepred(const rumur::MultisetRemovePred &n) final; + void visit_multisetcount(const rumur::MultisetCount &n) final; void visit_negative(const rumur::Negative &n) final; void visit_neq(const rumur::Neq &n) final; void visit_not(const rumur::Not &n) final; diff --git a/murphi2murphi/src/Stage.cc b/murphi2murphi/src/Stage.cc index 51839870..9ff638a7 100644 --- a/murphi2murphi/src/Stage.cc +++ b/murphi2murphi/src/Stage.cc @@ -87,6 +87,7 @@ void IntermediateStage::visit_assignment(const Assignment &n) { void IntermediateStage::visit_band(const Band &n) { next.visit_band(n); } void IntermediateStage::visit_bnot(const Bnot &n) { next.visit_bnot(n); } void IntermediateStage::visit_bor(const Bor &n) { next.visit_bor(n); } +void IntermediateStage::visit_choose(const Choose &n) { next.visit_choose(n); } void IntermediateStage::visit_clear(const Clear &n) { next.visit_clear(n); } void IntermediateStage::visit_constdecl(const ConstDecl &n) { next.visit_constdecl(n); @@ -132,6 +133,21 @@ void IntermediateStage::visit_lt(const Lt &n) { next.visit_lt(n); } void IntermediateStage::visit_mod(const Mod &n) { next.visit_mod(n); } void IntermediateStage::visit_model(const Model &n) { next.visit_model(n); } void IntermediateStage::visit_mul(const Mul &n) { next.visit_mul(n); } +void IntermediateStage::visit_multiset(const Multiset &n) { + next.visit_multiset(n); +} +void IntermediateStage::visit_multisetadd(const MultisetAdd &n) { + next.visit_multisetadd(n); +} +void IntermediateStage::visit_multisetcount(const MultisetCount &n) { + next.visit_multisetcount(n); +} +void IntermediateStage::visit_multisetremove(const MultisetRemove &n) { + next.visit_multisetremove(n); +} +void IntermediateStage::visit_multisetremovepred(const MultisetRemovePred &n) { + next.visit_multisetremovepred(n); +} void IntermediateStage::visit_negative(const Negative &n) { next.visit_negative(n); } diff --git a/murphi2murphi/src/Stage.h b/murphi2murphi/src/Stage.h index 635d736f..c0db88c9 100644 --- a/murphi2murphi/src/Stage.h +++ b/murphi2murphi/src/Stage.h @@ -70,6 +70,7 @@ class IntermediateStage : public Stage { void visit_band(const rumur::Band &n) override; void visit_bnot(const rumur::Bnot &n) override; void visit_bor(const rumur::Bor &n) override; + void visit_choose(const rumur::Choose &n) override; void visit_clear(const rumur::Clear &n) override; void visit_constdecl(const rumur::ConstDecl &n) override; void visit_div(const rumur::Div &n) override; @@ -97,6 +98,11 @@ class IntermediateStage : public Stage { void visit_mod(const rumur::Mod &n) override; void visit_model(const rumur::Model &n) override; void visit_mul(const rumur::Mul &n) override; + void visit_multiset(const rumur::Multiset &n) override; + void visit_multisetadd(const rumur::MultisetAdd &n) override; + void visit_multisetcount(const rumur::MultisetCount &n) override; + void visit_multisetremove(const rumur::MultisetRemove &n) override; + void visit_multisetremovepred(const rumur::MultisetRemovePred &n) override; void visit_negative(const rumur::Negative &n) override; void visit_neq(const rumur::Neq &n) override; void visit_not(const rumur::Not &n) override; diff --git a/murphi2smv/doc/murphi2smv.1 b/murphi2smv/doc/murphi2smv.1 index 0238859a..1b0e139a 100644 --- a/murphi2smv/doc/murphi2smv.1 +++ b/murphi2smv/doc/murphi2smv.1 @@ -83,6 +83,8 @@ placeholder comment: .IP \[bu] \fBisundefined\fR statements .IP \[bu] +\fBmultiset\fR types +.IP \[bu] \fBproperty\fR statements .IP \[bu] quantifiers diff --git a/murphi2smv/src/codegen.cc b/murphi2smv/src/codegen.cc index 0abd922a..481c3502 100644 --- a/murphi2smv/src/codegen.cc +++ b/murphi2smv/src/codegen.cc @@ -109,6 +109,11 @@ class Printer : public ConstBaseTraversal { *this << '(' << *n.lhs << " | " << *n.rhs << ')'; } + void visit_choose(const Choose &) final { + *this << tab() + << "/-- FIXME: Murphi choose rules have no equivalent in SMV --/\n"; + } + void visit_clear(const Clear &) final { *this << tab() @@ -296,6 +301,38 @@ class Printer : public ConstBaseTraversal { *this << '(' << *n.lhs << " * " << *n.rhs << ')'; } + void visit_multiset(const Multiset &n) final { + *this << "/-- FIXME: Murphi multiset types have no equivalent in SMV --/ " + "index: " + << *n.index_bound << "; element type: " << *n.element_type + << " /-- FIXME: end of Murphi multiset type --/"; + } + + void visit_multisetadd(const MultisetAdd &n) final { + *this << "/-- FIXME: Murphi multiset types have no equivalent in SMV --/ " + "MultisetAdd(" + << *n.arg0 << ", " << *n.arg1 << ')'; + } + + void visit_multisetcount(const MultisetCount &n) final { + *this << "/-- FIXME: Murphi multiset types have no equivalent in SMV --/ " + "MultisetCount(" + << n.identifier << ": " << *n.container << ", " << *n.predicate + << ')'; + } + + void visit_multisetremove(const MultisetRemove &n) final { + *this << "/-- FIXME: Murphi multiset types have no equivalent in SMV --/ " + "MultisetRemove(" + << *n.arg0 << ", " << *n.arg1 << ')'; + } + + void visit_multisetremovepred(const MultisetRemovePred &n) final { + *this << "/-- FIXME: Murphi multiset types have no equivalent in SMV --/ " + "MultisetRemovePred(" + << *n.container << ", " << *n.predicate << ')'; + } + void visit_negative(const Negative &n) final { *this << '-' << *n.rhs; } void visit_neq(const Neq &n) final { diff --git a/murphi2uclid/doc/murphi2uclid.1 b/murphi2uclid/doc/murphi2uclid.1 index 1a353fc3..b3896f64 100644 --- a/murphi2uclid/doc/murphi2uclid.1 +++ b/murphi2uclid/doc/murphi2uclid.1 @@ -67,6 +67,8 @@ Aliases, in the form of declarations statements or rules .IP \[bu] The \fBisundefined\fR operator .IP \[bu] +\fBmultiset\fR types +.IP \[bu] \fBunion\fR types .IP \[bu] The modulo operator, \fB%\fR diff --git a/murphi2uclid/src/check.cc b/murphi2uclid/src/check.cc index 4a65a048..90d0e3bd 100644 --- a/murphi2uclid/src/check.cc +++ b/murphi2uclid/src/check.cc @@ -32,6 +32,10 @@ class Checker : public ConstTraversal { throw Error("Uclid5 has no equivalent of alias statements", n.loc); } + void visit_choose(const Choose &n) final { + throw Error("Uclid5 has no equivalent of choose rules", n.loc); + } + void visit_clear(const Clear &n) final { const Ptr type = n.rhs->type(); @@ -131,6 +135,26 @@ class Checker : public ConstTraversal { throw Error("Uclid5 has no equivalent of the modulo operator", n.loc); } + void visit_multiset(const Multiset &n) final { + throw Error("Uclid5 has no equivalent of the multiset type", n.loc); + } + + void visit_multisetadd(const MultisetAdd &n) final { + throw Error("Uclid5 has no equivalent of the multiset type", n.loc); + } + + void visit_multisetcount(const MultisetCount &n) final { + throw Error("Uclid5 has no equivalent of the multiset type", n.loc); + } + + void visit_multisetremove(const MultisetRemove &n) final { + throw Error("Uclid5 has no equivalent of the multiset type", n.loc); + } + + void visit_multisetremovepred(const MultisetRemovePred &n) final { + throw Error("Uclid5 has no equivalent of the multiset type", n.loc); + } + void visit_propertyrule(const PropertyRule &n) final { if (n.property.category == Property::COVER) throw Error("cover properties have no LTL equivalent in Uclid5", n.loc); diff --git a/murphi2uclid/src/codegen.cc b/murphi2uclid/src/codegen.cc index f9d56bfa..b91dc481 100644 --- a/murphi2uclid/src/codegen.cc +++ b/murphi2uclid/src/codegen.cc @@ -114,6 +114,11 @@ class Printer : public ConstBaseTraversal { *this << "(" << *n.lhs << " | " << *n.rhs << ")"; } + void visit_choose(const Choose &) final { + assert(!"choose rule not rejected during check()"); + __builtin_unreachable(); + } + void visit_clear(const Clear &n) final { const Ptr type = n.rhs->type()->resolve(); @@ -486,6 +491,31 @@ class Printer : public ConstBaseTraversal { *this << "(" << *n.lhs << " * " << *n.rhs << ")"; } + void visit_multiset(const Multiset &) final { + assert(!"multiset not rejected during check()"); + __builtin_unreachable(); + } + + void visit_multisetadd(const MultisetAdd &) final { + assert(!"multisetadd not rejected during check()"); + __builtin_unreachable(); + } + + void visit_multisetcount(const MultisetCount &) final { + assert(!"multisetcount not rejected during check()"); + __builtin_unreachable(); + } + + void visit_multisetremove(const MultisetRemove &) final { + assert(!"multisetremove not rejected during check()"); + __builtin_unreachable(); + } + + void visit_multisetremovepred(const MultisetRemovePred &) final { + assert(!"multisetremovepred not rejected during check()"); + __builtin_unreachable(); + } + void visit_negative(const Negative &n) final { *this << "-" << *n.rhs; } void visit_neq(const Neq &n) final { diff --git a/murphi2xml/src/XMLPrinter.cc b/murphi2xml/src/XMLPrinter.cc index 0dad71c5..1a447a6c 100644 --- a/murphi2xml/src/XMLPrinter.cc +++ b/murphi2xml/src/XMLPrinter.cc @@ -156,6 +156,26 @@ void XMLPrinter::visit_bnot(const Bnot &n) { visit_uexpr("bnot", n); } void XMLPrinter::visit_bor(const Bor &n) { visit_bexpr("bor", n); } +void XMLPrinter::visit_choose(const Choose &n) { + sync_to(n); + o << "'; + sync_to(*n.container); + dispatch(*n.container); + if (!n.rules.empty()) { + sync_to(*n.rules[0]); + o << ""; + for (const Ptr &r : n.rules) { + sync_to(*r); + dispatch(*r); + } + o << ""; + } + sync_to(n.loc.end); + o << ""; +} + void XMLPrinter::visit_clear(const Clear &n) { sync_to(n); o << "'; + sync_to(*n.index_bound); + dispatch(*n.index_bound); + sync_to(*n.element_type); + dispatch(*n.element_type); + sync_to(n.loc.end); + o << ""; +} + +void XMLPrinter::visit_multisetadd(const MultisetAdd &n) { + sync_to(n); + o << "'; + sync_to(*n.arg0); + o << ""; + dispatch(*n.arg0); + o << ""; + sync_to(*n.arg1); + o << ""; + dispatch(*n.arg1); + o << ""; + sync_to(n.loc.end); + o << ""; +} + +void XMLPrinter::visit_multisetcount(const MultisetCount &n) { + sync_to(n); + o << "'; + sync_to(*n.container); + o << ""; + dispatch(*n.container); + o << ""; + sync_to(*n.predicate); + o << ""; + dispatch(*n.predicate); + o << ""; + sync_to(n.loc.end); + o << ""; +} + +void XMLPrinter::visit_multisetremove(const MultisetRemove &n) { + sync_to(n); + o << "'; + sync_to(*n.arg0); + o << ""; + dispatch(*n.arg0); + o << ""; + sync_to(*n.arg1); + o << ""; + dispatch(*n.arg1); + o << ""; + sync_to(n.loc.end); + o << ""; +} + +void XMLPrinter::visit_multisetremovepred(const MultisetRemovePred &n) { + sync_to(n); + o << "'; + sync_to(*n.container); + o << ""; + dispatch(*n.container); + o << ""; + sync_to(*n.predicate); + o << ""; + dispatch(*n.predicate); + o << ""; + sync_to(n.loc.end); + o << ""; +} + void XMLPrinter::visit_negative(const Negative &n) { visit_uexpr("negative", n); } diff --git a/murphi2xml/src/XMLPrinter.h b/murphi2xml/src/XMLPrinter.h index 2f333577..c6700ef6 100644 --- a/murphi2xml/src/XMLPrinter.h +++ b/murphi2xml/src/XMLPrinter.h @@ -27,6 +27,7 @@ class XMLPrinter : public rumur::ConstBaseTraversal { void visit_band(const rumur::Band &n) final; void visit_bnot(const rumur::Bnot &n) final; void visit_bor(const rumur::Bor &n) final; + void visit_choose(const rumur::Choose &n) final; void visit_clear(const rumur::Clear &n) final; void visit_constdecl(const rumur::ConstDecl &n) final; void visit_div(const rumur::Div &n) final; @@ -54,6 +55,11 @@ class XMLPrinter : public rumur::ConstBaseTraversal { void visit_mod(const rumur::Mod &n) final; void visit_model(const rumur::Model &n) final; void visit_mul(const rumur::Mul &n) final; + void visit_multiset(const rumur::Multiset &n) final; + void visit_multisetadd(const rumur::MultisetAdd &n) final; + void visit_multisetcount(const rumur::MultisetCount &n) final; + void visit_multisetremove(const rumur::MultisetRemove &n) final; + void visit_multisetremovepred(const rumur::MultisetRemovePred &n) final; void visit_negative(const rumur::Negative &n) final; void visit_neq(const rumur::Neq &n) final; void visit_not(const rumur::Not &n) final; diff --git a/rumur/src/check.cc b/rumur/src/check.cc index 25558b47..15aa511d 100644 --- a/rumur/src/check.cc +++ b/rumur/src/check.cc @@ -8,10 +8,34 @@ namespace { class Check : public ConstTraversal { public: + void visit_choose(const Choose &n) final { + throw Error("choose rules are not supported", n.loc); + } + void visit_ismember(const IsMember &n) final { throw Error("ismember expressions are not supported", n.loc); } + void visit_multiset(const Multiset &n) final { + throw Error("multiset types are not supported", n.loc); + } + + void visit_multisetadd(const MultisetAdd &n) final { + throw Error("multiset types are not supported", n.loc); + } + + void visit_multisetcount(const MultisetCount &n) final { + throw Error("multiset types are not supported", n.loc); + } + + void visit_multisetremove(const MultisetRemove &n) final { + throw Error("multiset types are not supported", n.loc); + } + + void visit_multisetremovepred(const MultisetRemovePred &n) final { + throw Error("multiset types are not supported", n.loc); + } + void visit_union(const Union &n) final { throw Error("union types are not supported", n.loc); } diff --git a/rumur/src/generate-expr.cc b/rumur/src/generate-expr.cc index e78fa04c..69adb4d7 100644 --- a/rumur/src/generate-expr.cc +++ b/rumur/src/generate-expr.cc @@ -84,6 +84,9 @@ class Generator : public ConstExprTraversal { const Ptr t2 = t1->resolve(); assert(t2 != nullptr && "array with invalid type"); + assert(!isa(t2) && + "multiset not rejected prior to code generation"); + auto a = dynamic_cast(*t2); mpz_class element_width = a.element_type->width(); @@ -267,22 +270,23 @@ class Generator : public ConstExprTraversal { } } - /* Now for each parameter we need to consider five distinct methods, based - * on the parameter's circumstance as described in the following table: + /* Now for each parameter we need to consider six distinct methods, based on + * the parameter’s circumstance as described in the following table: * - * ┌──────┬────────────────┬─────────┬────────────╥────────┐ - * │ var? │ simple/complex │ lvalue? │ read-only? ║ method │ - * ├──────┼────────────────┼─────────┼────────────╫────────┤ - * │ no │ simple │ no │ - ║ 1 │ - * │ no │ simple │ yes │ no ║ 2 │ - * │ no │ simple │ yes │ yes ║ 2 │ - * │ no │ complex │ no │ - ║ 5 │ - * │ no │ complex │ yes │ no ║ 3 │ - * │ no │ complex │ yes │ yes ║ 3 │ - * │ yes │ simple │ no │ no ║ 1 │ - * │ yes │ simple │ yes │ no ║ 4 │ - * │ yes │ complex │ yes │ no ║ 4 │ - * └──────┴────────────────┴─────────┴────────────╨────────┘ + * ┌──────┬────────────────┬─────────┬────────────┬────────────╥────────┐ + * │ var? │ simple/complex │ lvalue? │ read-only? │ undefined? ║ method │ + * ├──────┼────────────────┼─────────┼────────────┼────────────╫────────┤ + * │ no │ simple │ no │ - │ no ║ 1 │ + * │ no │ simple │ yes │ no │ no ║ 2 │ + * │ no │ simple │ yes │ yes │ no ║ 2 │ + * │ no │ complex │ no │ - │ no ║ 5 │ + * │ no │ complex │ yes │ no │ no ║ 3 │ + * │ no │ complex │ yes │ yes │ no ║ 3 │ + * │ yes │ simple │ no │ no │ no ║ 1 │ + * │ yes │ simple │ yes │ no │ no ║ 4 │ + * │ yes │ complex │ yes │ no │ no ║ 4 │ + * │ - │ - │ - │ - │ yes ║ 6 │ + * └──────┴────────────────┴─────────┴────────────┴────────────╨────────┘ * * 1. We can create a temporary handle and backing storage, then extract * the value of the argument as an rvalue and write it to this @@ -304,6 +308,8 @@ class Generator : public ConstExprTraversal { * 4. We just pass the original handle, the lvalue of the argument. * * 5. We pass the original (rvalue) handle. + * + * 6. We pass a zeroed C99 compound literal. */ // clang-format off @@ -315,15 +321,19 @@ class Generator : public ConstExprTraversal { bool is_lvalue = argument->is_lvalue(); bool readonly = argument->is_readonly(); - if (!var && simple && !is_lvalue ) return 1; - if (!var && simple && is_lvalue && !readonly) return 2; - if (!var && simple && is_lvalue && readonly) return 2; - if (!var && !simple && !is_lvalue ) return 5; - if (!var && !simple && is_lvalue && !readonly) return 3; - if (!var && !simple && is_lvalue && readonly) return 3; - if ( var && simple && !is_lvalue ) return 1; - if ( var && simple && is_lvalue && !readonly) return 4; - if ( var && !simple && !readonly) return 4; + auto id = dynamic_cast(argument.get()); + const bool is_undef = id != nullptr && id->id == "undefined"; + + if (!var && simple && !is_lvalue && !is_undef) return 1; + if (!var && simple && is_lvalue && !readonly && !is_undef) return 2; + if (!var && simple && is_lvalue && readonly && !is_undef) return 2; + if (!var && !simple && !is_lvalue && !is_undef) return 5; + if (!var && !simple && is_lvalue && !readonly && !is_undef) return 3; + if (!var && !simple && is_lvalue && readonly && !is_undef) return 3; + if ( var && simple && !is_lvalue && !is_undef) return 1; + if ( var && simple && is_lvalue && !readonly && !is_undef) return 4; + if ( var && !simple && !readonly && !is_undef) return 4; + if ( is_undef) return 6; assert(!"unreachable"); __builtin_unreachable(); @@ -343,7 +353,7 @@ class Generator : public ConstExprTraversal { "v" + std::to_string(n.unique_id) + "_" + std::to_string(index); auto method = get_method(p, a); - assert(method >= 1 && method <= 5); + assert(method >= 1 && method <= 6); if (method == 1 || method == 2 || method == 3) *out << "unsigned char " << storage << "[BITS_TO_BYTES(" << p->width() @@ -435,6 +445,11 @@ class Generator : public ConstExprTraversal { generate_rvalue(*out, *a); break; + case 6: + *out << "((struct handle){ .base = (unsigned char[BITS_TO_BYTES(" + << p->width() << ")]){0}, .width = " << p->width() << "ull })"; + break; + default: *out << handle; break; @@ -512,6 +527,11 @@ class Generator : public ConstExprTraversal { << ", s, " << *n.lhs << ", " << *n.rhs << ")"; } + void visit_multisetcount(const MultisetCount &) final { + assert(!"multisetcount not rejected before code generation"); + __builtin_unreachable(); + } + void visit_negative(const Negative &n) final { if (lvalue) invalid(n); diff --git a/rumur/src/generate-print.cc b/rumur/src/generate-print.cc index 0c25e4e2..181a3427 100644 --- a/rumur/src/generate-print.cc +++ b/rumur/src/generate-print.cc @@ -317,6 +317,8 @@ class Generator : public ConstTypeTraversal { return; } + assert(!isa(t) && + "multiset type not rejected before code generation"); assert(!isa(t) && "union type not rejected before code generation"); assert(!"non-range, non-enum used as array index"); @@ -361,6 +363,10 @@ class Generator : public ConstTypeTraversal { << "}\n"; } + void visit_multiset(const Multiset &n) final { + throw Error("multiset types are not supported", n.loc); + } + void visit_range(const Range &n) final { const std::string lb = "VALUE_C(" + n.lower_bound().get_str() + ")"; diff --git a/rumur/src/generate-stmt.cc b/rumur/src/generate-stmt.cc index ed3bdd28..ccb6c43a 100644 --- a/rumur/src/generate-stmt.cc +++ b/rumur/src/generate-stmt.cc @@ -79,6 +79,9 @@ static void clear(std::ostream &out, const TypeExpr &t, clear(out, *m, offset, depth); } + assert(!isa(type) && + "multiset not rejected prior to code generation"); + assert(!"unreachable"); } @@ -205,6 +208,21 @@ class Generator : public ConstStmtTraversal { } } + void visit_multisetadd(const MultisetAdd &) final { + assert(!"multisetadd not rejected during check()"); + __builtin_unreachable(); + } + + void visit_multisetremove(const MultisetRemove &) final { + assert(!"multisetremove not rejected during check()"); + __builtin_unreachable(); + } + + void visit_multisetremovepred(const MultisetRemovePred &) final { + assert(!"multisetremovepred not rejected during check()"); + __builtin_unreachable(); + } + void visit_procedurecall(const ProcedureCall &s) final { generate_rvalue(*out, s.call); } diff --git a/rumur/src/smt/define-enum-members.cc b/rumur/src/smt/define-enum-members.cc index 4f1948d3..9bafbc28 100644 --- a/rumur/src/smt/define-enum-members.cc +++ b/rumur/src/smt/define-enum-members.cc @@ -49,6 +49,11 @@ class Definer : public ConstTypeTraversal { } } + void visit_multiset(const Multiset &n) final { + // define any enum members that occur within the multiset element type + dispatch(*n.element_type); + } + void visit_range(const Range &) final { // as a primitive, ranges can't contain any enum members } diff --git a/rumur/src/smt/define-records.cc b/rumur/src/smt/define-records.cc index 49db5700..ea47eccb 100644 --- a/rumur/src/smt/define-records.cc +++ b/rumur/src/smt/define-records.cc @@ -29,6 +29,11 @@ class Definer : public ConstTypeTraversal { // nothing to do } + void visit_multiset(const Multiset &n) final { + // define any records that are defined within this multiset + dispatch(*n.element_type); + } + void visit_range(const Range &) final { // nothing to do } diff --git a/rumur/src/smt/simplify.cc b/rumur/src/smt/simplify.cc index 647ce14b..61f94390 100644 --- a/rumur/src/smt/simplify.cc +++ b/rumur/src/smt/simplify.cc @@ -84,6 +84,25 @@ class Simplifier : public BaseTraversal { void visit_bnot(Bnot &n) final { visit_uexpr(n); } void visit_bor(Bor &n) final { visit_bexpr(n); } + void visit_choose(Choose &n) final { + dispatch(*n.container); + simplify(n.container); + + solver->open_scope(); + const Ptr t = n.container->type()->resolve(); + auto m = dynamic_cast(t.get()); + if (m == nullptr) + throw Error("container in choose rule is not a multiset", + n.container->loc); + const Scalarset s{m->index_bound, n.container->loc}; + declare_var(n.identifier, n.unique_id, s); + + for (Ptr &r : n.rules) + dispatch(*r); + + solver->close_scope(); + } + void visit_clear(Clear &n) final { dispatch(*n.rhs); @@ -220,6 +239,53 @@ class Simplifier : public BaseTraversal { } void visit_mul(Mul &n) final { visit_bexpr(n); } + + void visit_multiset(Multiset &n) final { + dispatch(*n.index_bound); + simplify(n.index_bound); + dispatch(*n.element_type); + } + + void visit_multisetadd(MultisetAdd &n) final { + dispatch(*n.arg0); + simplify(n.arg0); + dispatch(*n.arg1); + simplify(n.arg1); + } + + void visit_multisetcount(MultisetCount &n) final { + dispatch(*n.container); + simplify(n.container); + + solver->open_scope(); + + const Ptr c = n.container->type()->resolve(); + auto m = dynamic_cast(c.get()); + if (m == nullptr) + throw Error("multisetcount container is not a multiset", + n.container->loc); + const Scalarset s{m->index_bound, n.loc}; + declare_var(n.identifier, n.unique_id, s); + + dispatch(*n.predicate); + simplify(n.predicate); + solver->close_scope(); + } + + void visit_multisetremove(MultisetRemove &n) final { + dispatch(*n.arg0); + simplify(n.arg0); + dispatch(*n.arg1); + simplify(n.arg1); + } + + void visit_multisetremovepred(MultisetRemovePred &n) final { + dispatch(*n.container); + simplify(n.container); + dispatch(*n.predicate); + simplify(n.predicate); + } + void visit_negative(Negative &n) final { visit_uexpr(n); } void visit_neq(Neq &n) final { visit_bexpr(n); } void visit_not(Not &n) final { visit_uexpr(n); } @@ -569,6 +635,8 @@ class Simplifier : public BaseTraversal { *solver << "(assert (" << lt() << " " << name << " " << size << "))\n"; } + void visit_multiset(const Multiset &) final { throw Unsupported(); } + void visit_range(const Range &n) final { // if this range's bounds are static, make them known to the solver diff --git a/rumur/src/smt/translate.cc b/rumur/src/smt/translate.cc index 42412d90..b16f8651 100644 --- a/rumur/src/smt/translate.cc +++ b/rumur/src/smt/translate.cc @@ -128,6 +128,10 @@ class Translator : public ConstExprTraversal { *this << "(" << mul() << " " << *n.lhs << " " << *n.rhs << ")"; } + void visit_multisetcount(const MultisetCount &n) final { + throw Unsupported(n); + } + void visit_negative(const Negative &n) final { *this << "(" << neg() << " " << *n.rhs << ")"; } diff --git a/rumur/src/smt/typeexpr-to-smt.cc b/rumur/src/smt/typeexpr-to-smt.cc index 13105337..4bca7452 100644 --- a/rumur/src/smt/typeexpr-to-smt.cc +++ b/rumur/src/smt/typeexpr-to-smt.cc @@ -49,6 +49,10 @@ class Translator : public ConstTypeTraversal { *this << integer_type(); } + void visit_multiset(const Multiset &) final { + throw Unsupported("multiset types are not supported in SMT translation"); + } + void visit_range(const Range &) final { /* we assume our caller will eventually set the lower and upper bound * constraints for this integer if it is relevant to them diff --git a/rumur/src/symmetry-reduction.cc b/rumur/src/symmetry-reduction.cc index b48a0613..e512c5eb 100644 --- a/rumur/src/symmetry-reduction.cc +++ b/rumur/src/symmetry-reduction.cc @@ -113,6 +113,8 @@ static void generate_apply_swap(std::ostream &out, const std::string &offset_a, return; } + assert(!isa(t) && + "multiset type not rejected before symmetry reduction"); assert(!isa(t) && "union type not rejected before symmetry reduction"); assert(!"missed case in generate_apply_swap"); @@ -200,6 +202,8 @@ static void generate_swap_chunk(std::ostream &out, const TypeExpr &t, return; } + assert(!isa(type) && + "multiset type not rejected before symmetry reduction"); assert(!isa(type) && "union type not rejected before symmetry reduction"); @@ -472,6 +476,8 @@ static void generate_apply_compare(std::ostream &out, const TypeExpr &type, return; } + assert(!isa(t) && + "multiset type not rejected before symmetry reduction"); assert(!isa(t) && "union type not rejected before symmetry reduction"); assert(!"missed case in generate_apply_compare"); @@ -583,6 +589,8 @@ static void generate_compare_chunk(std::ostream &out, const TypeExpr &t, return; } + assert(!isa(type) && + "multiset type not rejected before symmetry reduction"); assert(!isa(type) && "union type not rejected before symmetry reduction"); diff --git a/tests/tests.py b/tests/tests.py index 2d53071e..d616ecbd 100644 --- a/tests/tests.py +++ b/tests/tests.py @@ -1552,6 +1552,11 @@ def test_murphi2uclid(model, tmp_path): "scalarset-cex.m", "scalarset-schedules-off.m", "scalarset-schedules-off-2.m", + "undefined-assign.m", + "undefined-call.m", + "undefined-call-complex.m", + "undefined-var-call.m", + "undefined-var-call-complex.m", # contains `put` "for-step-0-dynamic.m", "put-stmt.m", diff --git a/tests/undefined-assign.m b/tests/undefined-assign.m new file mode 100644 index 00000000..fb4819ce --- /dev/null +++ b/tests/undefined-assign.m @@ -0,0 +1,19 @@ +-- can we handle the 'undefined' token in an assignment? +-- +-- This seems to be an extension added to CMurphi after its initial release. + +var + x: boolean; + +startstate begin + x := false; +end; + +rule + var y: boolean; +begin + y := x; + x := undefined; + assert isundefined(x); + x := !y; +end; diff --git a/tests/undefined-call-complex.m b/tests/undefined-call-complex.m new file mode 100644 index 00000000..b3886b1a --- /dev/null +++ b/tests/undefined-call-complex.m @@ -0,0 +1,22 @@ +-- a model that passes `undefined` to a function taking complex type + +type + t: record + a: 0..1; + end; + +var + x: boolean; + +function foo(y: t): boolean; begin + assert isundefined(y.a); + return !x; +end; + +startstate begin + x := false; +end; + +rule begin + x := foo(undefined); +end; diff --git a/tests/undefined-call.m b/tests/undefined-call.m new file mode 100644 index 00000000..17cbede7 --- /dev/null +++ b/tests/undefined-call.m @@ -0,0 +1,45 @@ +-- a model that passes `undefined` to a function + +var + x: boolean; + +function foo(y: 0..1): boolean; begin + assert isundefined(y); + return !x; +end; + +function bar(a: boolean; y: 0..1): boolean; begin + assert isundefined(y); + return !a; +end; + +function baz(y: 0..1; a: boolean): boolean; begin + assert isundefined(y); + return !a; +end; + +function qux(a: boolean; y: 0..1; b: boolean): boolean; begin + assert isundefined(y); + assert a = b; + return !a; +end; + +startstate begin + x := false; +end; + +rule begin + x := foo(undefined); +end; + +rule begin + x := bar(x, undefined); +end; + +rule begin + x := baz(undefined, x); +end; + +rule begin + x := qux(x, undefined, x); +end; diff --git a/tests/undefined-var-call-complex.m b/tests/undefined-var-call-complex.m new file mode 100644 index 00000000..b41b26de --- /dev/null +++ b/tests/undefined-var-call-complex.m @@ -0,0 +1,22 @@ +-- a model that passes `undefined` to a function taking complex type + +type + t: record + a: 0..1; + end; + +var + x: boolean; + +function foo(var y: t): boolean; begin + assert isundefined(y.a); + return !x; +end; + +startstate begin + x := false; +end; + +rule begin + x := foo(undefined); +end; diff --git a/tests/undefined-var-call.m b/tests/undefined-var-call.m new file mode 100644 index 00000000..78122b83 --- /dev/null +++ b/tests/undefined-var-call.m @@ -0,0 +1,45 @@ +-- a model that passes `undefined` to a function as a `var` parameter + +var + x: boolean; + +function foo(var y: 0..1): boolean; begin + assert isundefined(y); + return !x; +end; + +function bar(a: boolean; var y: 0..1): boolean; begin + assert isundefined(y); + return !a; +end; + +function baz(var y: 0..1; a: boolean): boolean; begin + assert isundefined(y); + return !a; +end; + +function qux(a: boolean; var y: 0..1; b: boolean): boolean; begin + assert isundefined(y); + assert a = b; + return !a; +end; + +startstate begin + x := false; +end; + +rule begin + x := foo(undefined); +end; + +rule begin + x := bar(x, undefined); +end; + +rule begin + x := baz(undefined, x); +end; + +rule begin + x := qux(x, undefined, x); +end;