Creating an API to get the value/index size from a 'Type'
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
diff --git a/bindings/python/stp/stp.py.in b/bindings/python/stp/stp.py.in
index fb4a6a7..61aef6d 100644
--- a/bindings/python/stp/stp.py.in
+++ b/bindings/python/stp/stp.py.in
@@ -3,7 +3,7 @@
Copyright (c) 2008 Vijay Ganesh
2014 Jurriaan Bremer, jurriaanbremer@gmail.com
- 2018-2019 Andrew V. Jones, andrewvaughanj@gmail.com
+ 2018-2021 Andrew V. Jones, andrewvaughanj@gmail.com
Permission is hereby granted, free of charge, to any person obtaining
a copy of this software and associated documentation files (the
@@ -128,6 +128,8 @@
_set_func('getBVUnsignedLongLong', c_uint64, _Expr)
_set_func('vc_bvType', _Type, _VC, c_int32)
_set_func('vc_bv32Type', _Type, _VC)
+_set_func('vc_getValueSize', c_int32, _VC, _Type)
+_set_func('vc_getIndexSize', c_int32, _VC, _Type)
_set_func('vc_bvConstExprFromDecStr', _Expr, _VC, c_int32, c_char_p)
_set_func('vc_bvConstExprFromStr', _Expr, _VC, c_char_p)
_set_func('vc_bvConstExprFromInt', _Expr, _VC, c_int32, c_uint32)
diff --git a/include/stp/c_interface.h b/include/stp/c_interface.h
index 5bc8190..09c5dba 100644
--- a/include/stp/c_interface.h
+++ b/include/stp/c_interface.h
@@ -576,6 +576,14 @@
//!
DLL_PUBLIC Type vc_bv32Type(VC vc);
+//! \brief Returns the value size for the given type.
+//!
+DLL_PUBLIC int vc_getValueSize(VC /* vc */, Type type);
+
+//! \brief Returns the index size for the given type.
+//!
+DLL_PUBLIC int vc_getIndexSize(VC /* vc */, Type type);
+
//Const expressions for string, int, long-long, etc
//! \brief Parses the given string and returns an associated bitvector expression.
diff --git a/lib/Interface/c_interface.cpp b/lib/Interface/c_interface.cpp
index ab56033..0d1539a 100644
--- a/lib/Interface/c_interface.cpp
+++ b/lib/Interface/c_interface.cpp
@@ -44,6 +44,41 @@
using std::fdostream;
using std::endl;
+namespace /* anonymous namespace for static */
+{
+
+/* this method is purposefully not public! */
+std::pair<unsigned int, unsigned int> getTypeSizes(Type type)
+{
+ unsigned int indexWidth = 0;
+ unsigned int valueWidth = 0;
+
+ stp::ASTNode* a = (stp::ASTNode*)type;
+
+ switch (a->GetKind())
+ {
+ case stp::BITVECTOR:
+ indexWidth = 0;
+ valueWidth = (*a)[0].GetUnsignedConst();
+ break;
+ case stp::ARRAY:
+ indexWidth = (*a)[0].GetUnsignedConst();
+ valueWidth = (*a)[1].GetUnsignedConst();
+ break;
+ case stp::BOOLEAN:
+ indexWidth = 0;
+ valueWidth = 0;
+ break;
+ default:
+ stp::FatalError("CInterface: vc_varExpr: Unsupported type", *a);
+ assert(false);
+ exit(-1);
+ break;
+ }
+ return std::make_pair(valueWidth, indexWidth);
+}
+} // namespace
+
// GLOBAL FUNCTION: parser
extern int cvcparse(void*);
extern int smtparse(void*);
@@ -719,31 +754,9 @@
{
stp::STP* stp_i = (stp::STP*)vc;
stp::STPMgr* b = stp_i->bm;
- stp::ASTNode* a = (stp::ASTNode*)type;
-
- unsigned indexWidth;
- unsigned valueWidth;
-
- switch (a->GetKind())
- {
- case stp::BITVECTOR:
- indexWidth = 0;
- valueWidth = (*a)[0].GetUnsignedConst();
- break;
- case stp::ARRAY:
- indexWidth = (*a)[0].GetUnsignedConst();
- valueWidth = (*a)[1].GetUnsignedConst();
- break;
- case stp::BOOLEAN:
- indexWidth = 0;
- valueWidth = 0;
- break;
- default:
- stp::FatalError("CInterface: vc_varExpr: Unsupported type", *a);
- assert(false);
- exit(-1);
- break;
- }
+ std::pair<unsigned int, unsigned int> typeSizes(getTypeSizes(type));
+ unsigned int valueWidth = typeSizes.first;
+ unsigned int indexWidth = typeSizes.second;
stp::ASTNode o = b->CreateSymbol(name, indexWidth, valueWidth);
stp::ASTNode* output = new stp::ASTNode(o);
@@ -1054,6 +1067,20 @@
return vc_bvType(vc, 32);
}
+int vc_getValueSize(VC /* vc */, Type type)
+{
+ std::pair<unsigned int, unsigned int> typeSizes(getTypeSizes(type));
+ unsigned int valueWidth = typeSizes.first;
+ return valueWidth;
+}
+
+int vc_getIndexSize(VC /* vc */, Type type)
+{
+ std::pair<unsigned int, unsigned int> typeSizes(getTypeSizes(type));
+ unsigned int indexWidth = typeSizes.second;
+ return indexWidth;
+}
+
Expr vc_bvConstExprFromDecStr(VC vc, int width, const char* decimalInput)
{
stp::STP* stp_i = (stp::STP*)vc;
diff --git a/tests/api/C/CMakeLists.txt b/tests/api/C/CMakeLists.txt
index 2830eef..82486c3 100644
--- a/tests/api/C/CMakeLists.txt
+++ b/tests/api/C/CMakeLists.txt
@@ -64,3 +64,4 @@
AddSTPGTest(counter-example-reading.cpp)
AddSTPGTest(failing_solvermap.cpp)
AddSTPGTest(bit_string.cpp)
+AddSTPGTest(check_sizes.cpp)
diff --git a/tests/api/C/check_sizes.cpp b/tests/api/C/check_sizes.cpp
new file mode 100644
index 0000000..8182a3d
--- /dev/null
+++ b/tests/api/C/check_sizes.cpp
@@ -0,0 +1,110 @@
+/***********
+AUTHORS: Andrew V. Jones
+
+BEGIN DATE: January 2021
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+THE SOFTWARE.
+**********************/
+
+#include "stp/c_interface.h"
+#include <gtest/gtest.h>
+#include <stdio.h>
+
+void check_bool()
+{
+ VC vc;
+
+ vc = vc_createValidityChecker();
+ Type boolType = vc_boolType(vc);
+
+ ASSERT_EQ(vc_getValueSize(vc, boolType), 0);
+ ASSERT_EQ(vc_getIndexSize(vc, boolType), 0);
+}
+
+void check_bv(int bvSize)
+{
+ VC vc;
+
+ vc = vc_createValidityChecker();
+ Type bvType = vc_bvType(vc, bvSize);
+
+ ASSERT_EQ(vc_getValueSize(vc, bvType), bvSize);
+ ASSERT_EQ(vc_getIndexSize(vc, bvType), 0);
+}
+
+void check_array(int indexSize, int valueSize)
+{
+ VC vc;
+
+ vc = vc_createValidityChecker();
+ Type indexType = vc_bvType(vc, indexSize);
+ Type valueType = vc_bvType(vc, valueSize);
+
+ Type arrayType = vc_arrayType(vc, indexType, valueType);
+
+ ASSERT_EQ(vc_getIndexSize(vc, arrayType), indexSize);
+ ASSERT_EQ(vc_getValueSize(vc, arrayType), valueSize);
+}
+
+TEST(stp_test, bool)
+{
+ check_bool();
+}
+
+TEST(stp_test, bv8)
+{
+ check_bv(8);
+}
+
+TEST(stp_test, bv16)
+{
+ check_bv(16);
+}
+
+TEST(stp_test, bv32)
+{
+ check_bv(32);
+}
+
+TEST(stp_test, bv64)
+{
+ check_bv(64);
+}
+
+TEST(stp_test, arr8_4)
+{
+ check_array(8, 4);
+}
+
+TEST(stp_test, arr16_8)
+{
+ check_array(16, 8);
+}
+
+TEST(stp_test, arr32_16)
+{
+ check_array(32, 16);
+}
+
+TEST(stp_test, arr64_32)
+{
+ check_array(64, 32);
+}
+
+// EOF
