Continued the static analysis for pbessymmetry #48

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open

mlaveaux wants to merge 40 commits into MERCorg:main from mlaveaux:feature/pbessymmetry

.gitmodules

-Original file line number
+Diff line change
@@ Expand Up / @@ -3,7 +3,7 @@ @@
     	url = https://github.com/mCRL2org/mCRL2.git
     [submodule "3rd-party/boost-include-only"]
     	path = 3rd-party/boost-include-only
-    	url = https://github.com/mlaveaux/boost-include-only.git
+    	url = https://github.com/MERCorg/boost-include-only.git
     [submodule "3rd-party/cpptrace"]
     	path = 3rd-party/cpptrace
     	url = https://github.com/jeremy-rifkin/cpptrace.git

tools/mcrl2/Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

tools/mcrl2/crates/mcrl2-macros/src/mcrl2_derive_terms.rs

-Original file line number
+Diff line change
@@ Expand Up @@
                             // Add the expected derive macros to the input struct.
                             object
                                 .attrs
-                                .push(parse_quote!(#[derive(Clone, Default, Debug, Hash, PartialEq, Eq, PartialOrd, Ord)]));
+                                .push(parse_quote!(#[derive(Clone, Default, Hash, PartialEq, Eq, PartialOrd, Ord)]));
                             // ALL structs in this module must contain the term.
                             assert!(
@@ Expand All @@
                             let name_ref = format_ident!("{}Ref", object.ident);
                             let generated: TokenStream = quote!(
                                 impl #name {
+                                    pub fn new(term: ATerm) -> #name {
+                                        #assertion;
+                                        #name {
+                                            term: term.into(),
+                                        }
+                                    }
                                     pub fn copy<'a>(&'a self) -> #name_ref<'a> {
                                         self.term.copy().into()
                                     }
@@ Expand Down Expand Up @@
                                     }
                                 }
-                                #[derive(Default, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)]
+                                impl ::std::fmt::Debug for #name {
+                                    fn fmt(&self, f: &mut ::std::fmt::Formatter<'_>) -> ::std::fmt::Result {
+                                        write!(f, "{:?}", self.term)
+                                    }
+                                }
+                                #[derive(Default, Eq, Hash, Ord, PartialEq, PartialOrd)]
                                 pub struct #name_ref<'a> {
                                     pub(crate) term: ATermRef<'a>
                                 }
                                 impl<'a> #name_ref<'a> {
+                                    pub fn new(term: ATermRef<'a>) -> #name_ref<'a> {
+                                        #assertion;
+                                        #name_ref {
+                                            term: term.into(),
+                                        }
+                                    }
                                     pub fn copy<'b>(&'b self) -> #name_ref<'b> {
                                         self.term.copy().into()
                                     }
@@ Expand Down Expand Up @@
                                     }
                                 }
+                                impl ::std::fmt::Debug for #name_ref<'_> {
+                                    fn fmt(&self, f: &mut ::std::fmt::Formatter<'_>) -> ::std::fmt::Result {
+                                        write!(f, "{:?}", self.term)
+                                    }
+                                }
                             );
                             added.push(Item::Verbatim(generated));
@@ Expand Down @@

tools/mcrl2/crates/mcrl2-sys/build.rs

-Original file line number
+Diff line change
@@ Expand Up / @@ -174,6 +174,7 @@ fn main() { @@
                 &utilities_source_files,
             ))
             .file("cpp/pbes.cpp")
+            .file("cpp/data.cpp")
             .file(mcrl2_workarounds_path.clone() + "mcrl2_syntax.c"); // This is to avoid generating the dparser grammer.
         #[cfg(feature = "mcrl2_jittyc")]
@@ Expand Down Expand Up / @@ -204,6 +205,7 @@ fn main() { @@
         rerun_if_changed!("cpp/atermpp.h");
         rerun_if_changed!("cpp/exception.h");
         rerun_if_changed!("cpp/data.h");
+        rerun_if_changed!("cpp/data.cpp");
         rerun_if_changed!("cpp/pbes.h");
         rerun_if_changed!("cpp/pbes.cpp");
         rerun_if_changed!("cpp/log.h");
@@ Expand Down @@

tools/mcrl2/crates/mcrl2-sys/cpp/atermpp.h

-Original file line number
+Diff line change
@@ Expand Up @@
       return 0;
     }
+    inline const detail::_aterm* mcrl2_aterm_create_int(std::uint64_t value)
+    {
+      atermpp::unprotected_aterm_core result(nullptr);
+      make_aterm_int(reinterpret_cast<aterm_int&>(result), static_cast<std::size_t>(value));
+      return detail::address(result);
+    }
     inline std::unique_ptr<aterm> mcrl2_aterm_from_string(rust::Str text)
     {
       return std::make_unique<aterm>(read_term_from_string(static_cast<std::string>(text)));
@@ Expand Down @@

tools/mcrl2/crates/mcrl2-sys/cpp/data.cpp

-Original file line number
+Diff line change
@@ -0,0 +1,31 @@
+    #include "atermpp.h"
+    #include "mcrl2/data/substitutions/mutable_map_substitution.h"
+    #include "mcrl2/data/replace.h"
+    #include "mcrl2-sys/cpp/data.h"
+    #include "mcrl2-sys/src/data.rs.h"
+    namespace mcrl2::data
+    {
+    std::unique_ptr<atermpp::aterm> mcrl2_data_expression_replace_variables(const atermpp::detail::_aterm& term,
+        const rust::Vec<assignment_pair>& sigma)
+    {
+      atermpp::unprotected_aterm_core tmp_expr(&term);
+      MCRL2_ASSERT(is_data_expression(atermpp::down_cast<atermpp::aterm>(tmp_expr)));
+      data::mutable_map_substitution<> tmp;
+      for (const auto& assign : sigma)
+      {
+        atermpp::unprotected_aterm_core tmp_lhs(assign.lhs);
+        atermpp::unprotected_aterm_core tmp_rhs(assign.rhs);
+        tmp[atermpp::down_cast<data::variable>(tmp_lhs)]
+            = atermpp::down_cast<data::data_expression>(tmp_rhs);
+      }
+      return std::make_unique<atermpp::aterm>(
+          replace_variables(atermpp::down_cast<data_expression>(tmp_expr), tmp));
+    }
+    }

tools/mcrl2/crates/mcrl2-sys/cpp/data.h

-Original file line number
+Diff line change
@@ Expand Up / @@ -23,6 +23,10 @@ @@
     namespace mcrl2::data
     {
+    // Forward declaration
+    struct assignment_pair;
     inline
     std::unique_ptr<data_specification> mcrl2_data_specification_from_string(rust::Str input)
     {
@@ Expand All @@
     #endif
+    std::unique_ptr<atermpp::aterm> mcrl2_data_expression_replace_variables(const atermpp::detail::_aterm& term,
+        const rust::Vec<assignment_pair>& sigma);
+    inline
     bool mcrl2_data_expression_is_variable(const atermpp::detail::_aterm& input)
     {
       atermpp::unprotected_aterm_core tmp(&input);
       return data::is_variable(atermpp::down_cast<atermpp::aterm>(tmp));
     }
+    inline
     bool mcrl2_data_expression_is_application(const atermpp::detail::_aterm& input)
     {
       atermpp::unprotected_aterm_core tmp(&input);
       return data::is_application(atermpp::down_cast<atermpp::aterm>(tmp));
     }
+    inline
     bool mcrl2_data_expression_is_abstraction(const atermpp::detail::_aterm& input)
     {
       atermpp::unprotected_aterm_core tmp(&input);
       return data::is_abstraction(atermpp::down_cast<atermpp::aterm>(tmp));
     }
+    inline
     bool mcrl2_data_expression_is_function_symbol(const atermpp::detail::_aterm& input)
     {
       atermpp::unprotected_aterm_core tmp(&input);
       return data::is_function_symbol(atermpp::down_cast<atermpp::aterm>(tmp));
     }
+    inline
     bool mcrl2_data_expression_is_where_clause(const atermpp::detail::_aterm& input)
     {
       atermpp::unprotected_aterm_core tmp(&input);
       return data::is_where_clause(atermpp::down_cast<atermpp::aterm>(tmp));
     }
+    inline
     bool mcrl2_data_expression_is_machine_number(const atermpp::detail::_aterm& input)
     {
       atermpp::unprotected_aterm_core tmp(&input);
       return data::is_machine_number(atermpp::down_cast<atermpp::aterm>(tmp));
     }
+    inline
     bool mcrl2_data_expression_is_untyped_identifier(const atermpp::detail::_aterm& input)
     {
       atermpp::unprotected_aterm_core tmp(&input);
       return data::is_untyped_identifier(atermpp::down_cast<atermpp::aterm>(tmp));
     }
+    inline
     bool mcrl2_data_expression_is_data_expression(const atermpp::detail::_aterm& input)
     {
       atermpp::unprotected_aterm_core tmp(&input);
       return data::is_data_expression(atermpp::down_cast<atermpp::aterm>(tmp));
     }
+    inline
     bool mcrl2_is_data_sort_expression(const atermpp::detail::_aterm& input)
     {
       atermpp::unprotected_aterm_core tmp(&input);
       return data::is_sort_expression(atermpp::down_cast<atermpp::aterm>(tmp));
     }
+    inline
     rust::String mcrl2_data_expression_to_string(const atermpp::detail::_aterm& input)
     {
       atermpp::unprotected_aterm_core tmp(&input);
@@ Expand Down @@

tools/mcrl2/crates/mcrl2-sys/cpp/pbes.h

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -27,6 +27,7 @@ namespace mcrl2::pbes_system
  
    /// Alias for templated type.

    using srf_equation = detail::pre_srf_equation<false>;

    // Forward declaration

    struct vertex_outgoing_edge;

    struct assignment_pair;

    @@ -63,6 +64,18 @@ std::unique_ptr<data::data_specification> mcrl2_pbes_data_specification(const pb
  
      return std::make_unique<data::data_specification>(pbesspec.data());

    }

    inline

    void mcrl2_pbes_normalize(pbes& pbesspec)

    {

      algorithms::normalize(pbesspec);

    }

    inline

    bool mcrl2_pbes_is_well_typed(const pbes& pbesspec)

    {

      return pbesspec.is_well_typed();

    }

    inline

    rust::String mcrl2_pbes_to_string(const pbes& pbesspec)

    {

    @@ -72,10 +85,11 @@ rust::String mcrl2_pbes_to_string(const pbes& pbesspec)
  
    }

    inline

    rust::String mcrl2_pbes_expression_to_string(const atermpp::aterm& expr)

    rust::String mcrl2_pbes_expression_to_string(const atermpp::detail::_aterm& expr)

    {

      atermpp::unprotected_aterm_core tmp(&expr);

      std::stringstream ss;

      ss << expr;

      ss << atermpp::down_cast<pbes_system::pbes_expression>(tmp);

      return ss.str();

    }

    @@ -85,7 +99,7 @@ class stategraph_algorithm : private detail::stategraph_local_algorithm
  
    public:

      stategraph_algorithm(const pbes& input)

          : super(input, pbesstategraph_options{.print_influence_graph = true})

          : super(input, pbesstategraph_options{.cache_marking_updates = true})

      {}

      void run() override

    @@ -309,13 +323,71 @@ const atermpp::detail::_aterm* mcrl2_srf_summand_variable(const srf_summand& sum
  
    inline

    const atermpp::detail::_aterm* mcrl2_srf_summand_condition(const srf_summand& summand)

    {

      return atermpp::detail::address(summand.variable());

      return atermpp::detail::address(summand.condition());

    }

    std::unique_ptr<atermpp::aterm> mcrl2_pbes_expression_replace_variables(const atermpp::detail::_aterm& expr, const rust::Vec<assignment_pair>& sigma);

    std::unique_ptr<atermpp::aterm> mcrl2_pbes_expression_replace_propositional_variables(const atermpp::detail::_aterm& expr, const rust::Vec<std::size_t>& pi);

    /// mcrl2::pbes_system::pbes_expression

    inline

    bool mcrl2_pbes_is_pbes_expression(const atermpp::detail::_aterm& variable)

    {

      atermpp::unprotected_aterm_core tmp(&variable);

      return pbes_system::is_pbes_expression(atermpp::down_cast<atermpp::aterm>(tmp));

    }

    inline

    bool mcrl2_pbes_is_propositional_variable_instantiation(const atermpp::detail::_aterm& variable)

    {

      atermpp::unprotected_aterm_core tmp(&variable);

      return pbes_system::is_propositional_variable_instantiation(atermpp::down_cast<atermpp::aterm>(tmp));

    }

    inline

    bool mcrl2_pbes_is_not(const atermpp::detail::_aterm& variable)

    {

      atermpp::unprotected_aterm_core tmp(&variable);

      return pbes_system::is_not(atermpp::down_cast<atermpp::aterm>(tmp));

    }

    inline

    bool mcrl2_pbes_is_and(const atermpp::detail::_aterm& variable)

    {

      atermpp::unprotected_aterm_core tmp(&variable);

      return pbes_system::is_and(atermpp::down_cast<atermpp::aterm>(tmp));

    }

    inline

    bool mcrl2_pbes_is_or(const atermpp::detail::_aterm& variable)

    {

      atermpp::unprotected_aterm_core tmp(&variable);

      return pbes_system::is_or(atermpp::down_cast<atermpp::aterm>(tmp));

    }

    inline

    bool mcrl2_pbes_is_imp(const atermpp::detail::_aterm& variable)

    {

      atermpp::unprotected_aterm_core tmp(&variable);

      return pbes_system::is_imp(atermpp::down_cast<atermpp::aterm>(tmp));

    }

    inline

    bool mcrl2_pbes_is_forall(const atermpp::detail::_aterm& variable)

    {

      atermpp::unprotected_aterm_core tmp(&variable);

      return pbes_system::is_forall(atermpp::down_cast<atermpp::aterm>(tmp));

    }

    inline

    bool mcrl2_pbes_is_exists(const atermpp::detail::_aterm& variable)

    {

      atermpp::unprotected_aterm_core tmp(&variable);

      return pbes_system::is_exists(atermpp::down_cast<atermpp::aterm>(tmp));

    }

    } // namespace mcrl2::pbes_system

    #endif // MCRL2_SYS_CPP_PBES_H

tools/mcrl2/crates/mcrl2-sys/src/atermpp.rs

-Original file line number
+Diff line change
@@ Expand Up / @@ -71,6 +71,9 @@ pub mod ffi { @@
             /// garbage collection marks the terms, which is done atomically.
             unsafe fn mcrl2_aterm_create(function: &_function_symbol, arguments: &[*const _aterm]) -> *const _aterm;
+            /// Creates an aterm_int from the given value.
+            fn mcrl2_aterm_create_int(value: u64) -> *const _aterm;
             /// Parses the given string and returns an aterm
             fn mcrl2_aterm_from_string(text: &str) -> Result<UniquePtr<aterm>>;
@@ Expand Down @@

tools/mcrl2/crates/mcrl2-sys/src/data.rs

-Original file line number
+Diff line change
@@ -1,5 +1,12 @@
     #[cxx::bridge(namespace = "mcrl2::data")]
     pub mod ffi {
+        /// A helper struct for std::pair<pbes_expression, pbes_expression>>
+        struct assignment_pair {
+            pub lhs: *const _aterm,
+            pub rhs: *const _aterm,
+        }
         unsafe extern "C++" {
             include!("mcrl2-sys/cpp/data.h");
             include!("mcrl2-sys/cpp/exception.h");
@@ Expand All / @@ -26,6 +33,15 @@ pub mod ffi { @@
             #[namespace = "atermpp::detail"]
             type _aterm = crate::atermpp::ffi::_aterm;
+            #[namespace = "atermpp"]
+            type aterm = crate::atermpp::ffi::aterm;
+            /// Replace variables in the given data expression according to the given substitution sigma.
+            fn mcrl2_data_expression_replace_variables(
+                input: &_aterm,
+                sigma: &Vec<assignment_pair>,
+            ) -> UniquePtr<aterm>;
             // Recognizers for the various variants of data expressions.
             fn mcrl2_data_expression_is_variable(input: &_aterm) -> bool;
             fn mcrl2_data_expression_is_application(input: &_aterm) -> bool;
@@ Expand Down @@

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Continued the static analysis for pbessymmetry #48

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Uh oh!

Uh oh!

Continued the static analysis for pbessymmetry #48

Are you sure you want to change the base?

Uh oh!

Continued the static analysis for pbessymmetry #48

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Uh oh!

Uh oh!