From e53d797fa042a7c466ca838ea21abbd3890a39ba Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 16 Dec 2021 06:29:10 -0800 Subject: [PATCH] Explicitly disallow `mkConst(Rational)` (#7818) The Rational payload can be associated with two kinds (CONST_INTEGER and CONST_RATIONAL), so we should never call NodeManager::mkConst(Rational), but instead use NodeManager::mkConstInt() and NodeManager::mkConstReal(). Currently, calling NodeManager::mkConst(Rational) silently creates an integer constant, which is dangerous. This commit makes it a compile-time error instead. --- src/expr/CMakeLists.txt | 13 +++++++++++- src/expr/mkmetakind | 21 +++++++++++++++++-- src/expr/node_manager_template.cpp | 6 ------ ...node_manager.h => node_manager_template.h} | 4 ++++ src/theory/arith/kinds | 6 +++--- src/theory/strings/sequences_rewriter.cpp | 2 +- 6 files changed, 39 insertions(+), 13 deletions(-) rename src/expr/{node_manager.h => node_manager_template.h} (99%) diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 9a89dfbe6..e00e938e0 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -47,7 +47,6 @@ libcvc5_add_sources( node_builder.h node_converter.cpp node_converter.h - node_manager.h node_manager_attributes.h node_self_iterator.h node_trie.cpp @@ -104,6 +103,7 @@ libcvc5_add_sources(GENERATED metakind.cpp metakind.h node_manager.cpp + node_manager.h type_checker.cpp type_properties.cpp type_properties.h @@ -177,6 +177,16 @@ add_custom_command( DEPENDS mkmetakind metakind_template.cpp metakind.h ${KINDS_FILES} ) +add_custom_command( + OUTPUT node_manager.h + COMMAND + ${mkmetakind_script} + ${CMAKE_CURRENT_LIST_DIR}/node_manager_template.h + ${KINDS_FILES} + > ${CMAKE_CURRENT_BINARY_DIR}/node_manager.h + DEPENDS mkmetakind node_manager_template.h ${KINDS_FILES} +) + add_custom_command( OUTPUT node_manager.cpp COMMAND @@ -204,6 +214,7 @@ add_custom_target(gen-expr metakind.cpp metakind.h node_manager.cpp + node_manager.h type_checker.cpp type_properties.cpp type_properties.h diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index d5f6d9b1a..3ee7dc59b 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -54,6 +54,7 @@ metakind_ubchildren= metakind_lbchildren= metakind_operatorKinds= metakind_mkConst= +metakind_mkConstDelete= seen_theory=false seen_theory_builtin=false @@ -295,8 +296,23 @@ TypeNode NodeManager::mkTypeConst<${class}>(const ${class}& val) } " metakind_mkConst="${metakind_mkConst} -template -Node NodeManager::mkConst(Kind k, const ${class}& val); +template<> +Node NodeManager::mkConst(Kind k, const ${class}& val) +{ + return mkConstInternal(k, val); +} +" + elif [[ "${payload_seen}" != true ]]; then + metakind_mkConstDelete="${metakind_mkConstDelete} +template<> +Node NodeManager::mkConst<${class}>(const ${class}& val) = delete; +" + metakind_mkConst="${metakind_mkConst} +template<> +Node NodeManager::mkConst(Kind k, const ${class}& val) +{ + return mkConstInternal(k, val); +} " fi @@ -442,6 +458,7 @@ for var in \ metakind_lbchildren \ metakind_operatorKinds \ metakind_mkConst \ + metakind_mkConstDelete \ template \ ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index 4f235a53a..944d7fe66 100644 --- a/src/expr/node_manager_template.cpp +++ b/src/expr/node_manager_template.cpp @@ -1158,12 +1158,6 @@ TNode NodeManager::operatorOf(Kind k) return d_operators[k]; } -template -Node NodeManager::mkConst(Kind k, const T& val) -{ - return mkConstInternal(k, val); -} - template NodeClass NodeManager::mkConstInternal(Kind k, const T& val) { diff --git a/src/expr/node_manager.h b/src/expr/node_manager_template.h similarity index 99% rename from src/expr/node_manager.h rename to src/expr/node_manager_template.h index b2682661e..073077344 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager_template.h @@ -1206,6 +1206,10 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind, return NodeBuilder(this, kind).append(children).constructTypeNode(); } +// clang-format off +${metakind_mkConstDelete} +// clang-format off + } // namespace cvc5 #endif /* CVC5__NODE_MANAGER_H */ diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index f577b4109..e496cf335 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -54,13 +54,13 @@ constant DIVISIBLE_OP \ sort REAL_TYPE \ Cardinality::REALS \ well-founded \ - "NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0))" \ + "NodeManager::currentNM()->mkConstReal(Rational(0))" \ "expr/node_manager.h" \ "real type" sort INTEGER_TYPE \ Cardinality::INTEGERS \ well-founded \ - "NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0))" \ + "NodeManager::currentNM()->mkConstInt(Rational(0))" \ "expr/node_manager.h" \ "integer type" @@ -73,7 +73,7 @@ constant CONST_RATIONAL \ constant CONST_INTEGER \ class \ - Rational \ + Rational+ \ ::cvc5::RationalHashFunction \ "util/rational.h" \ "a multiple-precision integer constant; payload is an instance of the cvc5::Rational class" diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 11cc52ad4..aadca9904 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -2090,7 +2090,7 @@ Node SequencesRewriter::rewriteUpdate(Node node) NodeManager* nm = NodeManager::currentNM(); Node idx = nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, s), - nm->mkNode(PLUS, i, nm->mkConst(Rational(1)))); + nm->mkNode(PLUS, i, nm->mkConstInt(Rational(1)))); Node ret = nm->mkNode(STRING_REV, nm->mkNode(STRING_UPDATE, s, idx, x)); return returnRewrite(node, ret, Rewrite::UPD_REV); } -- 2.30.2