diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index a07ca54..f020a75 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -29,7 +29,7 @@ jobs:
- name: Install clang-format
run: sudo apt-get update && sudo apt-get -qqy install clang-format
- name: Checkout source
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
with:
fetch-depth: 0
- name: Check Formatting
@@ -48,7 +48,7 @@ jobs:
steps:
- name: Checkout source
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
with:
fetch-depth: 0
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index 92f77c9..1284483 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -26,7 +26,7 @@ jobs:
steps:
- name: Checkout
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
with:
fetch-depth: 0
@@ -59,7 +59,7 @@ jobs:
cp "$BUILD_DIR/src/libtable.so" "$TARGET/libtable${SUFFIX}.so"
- name: Upload Artifacts
- uses: actions/upload-artifact@v3
+ uses: actions/upload-artifact@v4
with:
name: ${{ env.TARGET }}
path: ${{ env.TARGET }}
@@ -70,7 +70,7 @@ jobs:
runs-on: ubuntu-latest
steps:
- name: Download Windows Artifacts
- uses: actions/download-artifact@v3
+ uses: actions/download-artifact@v4
with:
name: windows-msvc
path: windows-msvc
@@ -79,7 +79,7 @@ jobs:
run: ls -R .. && zip -r9 ../uppaal-libs-windows-msvc.zip *
- name: Download macOS Artifacts
- uses: actions/download-artifact@v3
+ uses: actions/download-artifact@v4
with:
name: macos
path: macos
@@ -88,7 +88,7 @@ jobs:
run: ls -R .. && zip -r9 ../uppaal-libs-macos.zip *
- name: Download Linux Artifacts
- uses: actions/download-artifact@v3
+ uses: actions/download-artifact@v4
with:
name: linux
path: linux
diff --git a/CMakeLists.txt b/CMakeLists.txt
index b53d656..5f4d2f2 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,6 +1,5 @@
cmake_minimum_required(VERSION 3.15)
-
-project(uppaal_libs)
+project(uppaal_libs LANGUAGES C CXX)
include(cmake/stdcpp.cmake)
include(cmake/sanitizers.cmake)
diff --git a/array.xml b/array.xml
new file mode 100644
index 0000000..06ab35e
--- /dev/null
+++ b/array.xml
@@ -0,0 +1,134 @@
+
+
+
+ typedef int[0,INT32_MAX] uint32_t;
+const uint32_t N = 3;
+
+import "/tmp/uppaal-libs/libarray.so"
+{
+ uint32_t get_size(); /// size of stored data array
+ void set_size(uint32_t size); /// resize the storage
+ void load_data(double& values[N], uint32_t size); /// Reads the stored data into a given array
+ void store_data(const double& values[N], uint32_t size); /// Stores the data
+
+ uint32_t get_size2(); /// size of stored data2 array
+ void set_size2(uint32_t size); /// resize the data2 array
+ void load_data2(double& values[N], uint32_t size); /// Reads the stored data2 into a given array
+ void store_data2(const double& values[N], uint32_t size); /// Stores into the data2
+
+ void load_both(double& values[N], uint32_t size, double& values2[N], uint32_t size2); /// Reads both data and data2
+ void store_both(const double& values[N], uint32_t size, const double& values2[N], uint32_t size2); /// Store into both data and data2
+};
+
+uint32_t init_size = get_size();
+uint32_t init_size2 = get_size2();
+
+uint32_t size;
+uint32_t size2;
+const double in[N] = { 2.1718, 3.1415, 42.0 };
+const double in2[N] = { 42.0, 2.1718, 3.1415 };
+double out[N];
+double out2[N];
+
+
+ P
+ clock x;
+
+
+
+
+
+ Done
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ system P;
+
+
+ simulate [<=1; 100] { size } : 100 : P.Done
+
+
+
+
diff --git a/cmake/sanitizers.cmake b/cmake/sanitizers.cmake
index 48e138d..9c2c293 100644
--- a/cmake/sanitizers.cmake
+++ b/cmake/sanitizers.cmake
@@ -1,6 +1,7 @@
# Various sanitizers (runtime checks) for debugging
option(SSP "Stack Smashing Protector (GCC/Clang/ApplClang on Unix)" OFF) # Available on Windows too
option(UBSAN "Undefined Behavior Sanitizer (GCC/Clang/AppleClang on Unix)" OFF)
+option(LSAN "Leak Sanitizer (GCC/Clang/AppleClang on Unix)" OFF)
option(ASAN "Address Sanitizer (GCC/Clang/AppleClang on Unix, MSVC on Windows)" OFF)
option(TSAN "Thread Sanitizer (GCC/Clang/AppleClang on Unix)" OFF)
option(RTC_C "Runtime Checks for Conversions (MSVC on Windows)" OFF)
@@ -15,7 +16,7 @@ else (SSP)
message(STATUS "Disabled Stack Smashing Protector")
endif(SSP)
-if (ASAN OR UBSAN OR TSAN)
+if (LSAN OR ASAN OR UBSAN OR TSAN)
if (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
else()
add_compile_options(-fno-omit-frame-pointer)
@@ -36,6 +37,18 @@ else (UBSAN)
message(STATUS "Disabled Undefined Behavior Sanitizer")
endif(UBSAN)
+if (LSAN)
+ if (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
+ add_compile_options(/fsanitize=leak)
+ else()
+ add_compile_options(-fsanitize=leak)
+ add_link_options(-fsanitize=leak)
+ endif()
+ message(STATUS "Enabled Leak Sanitizer")
+else(LSAN)
+ message(STATUS "Disabled Leak Sanitizer")
+endif(LSAN)
+
if (ASAN)
if (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
add_compile_options(/fsanitize=address)
diff --git a/compile.sh b/compile.sh
index a52f34e..73f596a 100755
--- a/compile.sh
+++ b/compile.sh
@@ -151,6 +151,13 @@ for target in $targets ; do
x86_64*mingw32)
extension=dll
SANITIZE="-DSSP=ON"
+ libgcc_path=$($target-g++ --print-file-name=libgcc_s_seh-1.dll)
+ libgcc_path=$(realpath "$libgcc_path")
+ libgcc_path=$(dirname "$libgcc_path")
+ libwinpthread_path=$($target-g++ --print-file-name=libwinpthread-1.dll)
+ libwinpthread_path=$(realpath "$libwinpthread_path")
+ libwinpthread_path=$(dirname "$libwinpthread_path")
+ export WINEPATH="$libwinpthread_path;$libgcc_path"
;;
*)
echo "Unknown target platform: $target"
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 76e6d0c..425410c 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -9,15 +9,23 @@ add_library(table SHARED table.cpp)
target_link_libraries(table PRIVATE errors)
add_dependencies(table data)
+add_library(array SHARED array.cpp)
+target_link_libraries(array PRIVATE errors)
+
if (UPPAALLIBS_WITH_TESTS)
- add_executable(test_table test_table.cpp)
- target_link_libraries(test_table PRIVATE doctest::doctest_with_main)
- add_dependencies(test_table table)
- add_test(NAME test_table COMMAND test_table)
+ add_executable(array_test array_test.cpp)
+ target_link_libraries(array_test PRIVATE doctest::doctest_with_main)
+ add_dependencies(array_test array)
+ add_test(NAME array_test COMMAND array_test)
+
+ add_executable(table_test table_test.cpp)
+ target_link_libraries(table_test PRIVATE doctest::doctest_with_main)
+ add_dependencies(table_test table)
+ add_test(NAME table_test COMMAND table_test)
if (CMAKE_BUILD_TYPE STREQUAL "Debug")
- add_executable(test_errors test_errors.cpp)
- target_link_libraries(test_errors PRIVATE errors doctest::doctest_with_main)
- add_test(NAME test_errors COMMAND test_errors)
+ add_executable(errors_test errors_test.cpp)
+ target_link_libraries(errors_test PRIVATE errors doctest::doctest_with_main)
+ add_test(NAME errors_test COMMAND errors_test)
endif()
endif (UPPAALLIBS_WITH_TESTS)
\ No newline at end of file
diff --git a/src/array.cpp b/src/array.cpp
new file mode 100644
index 0000000..7a5f4b2
--- /dev/null
+++ b/src/array.cpp
@@ -0,0 +1,51 @@
+#include "array.hpp"
+#include
+
+static auto data = std::vector{};
+
+C_PUBLIC uint32_t get_size() { return data.size(); }
+
+C_PUBLIC void set_size(uint32_t size) { data.resize(size); }
+
+C_PUBLIC void load_data(double values[], uint32_t size)
+{
+ auto sz = std::min(static_cast(size), data.size());
+ std::copy(data.data(), data.data() + sz, values);
+}
+
+C_PUBLIC void store_data(const double values[], uint32_t size)
+{
+ data.assign(values, values + size);
+}
+
+static auto data2 = std::vector{};
+
+C_PUBLIC uint32_t get_size2() { return data2.size(); }
+
+C_PUBLIC void set_size2(uint32_t size) { data2.resize(size); }
+
+C_PUBLIC void load_data2(double values[], uint32_t size)
+{
+ auto sz = std::min(static_cast(size), data2.size());
+ std::copy(data2.data(), data2.data() + sz, values);
+}
+
+C_PUBLIC void store_data2(const double values[], uint32_t size)
+{
+ data2.assign(values, values + size);
+}
+
+C_PUBLIC void load_both(double values[], uint32_t size, double values2[], uint32_t size2)
+{
+ auto sz1 = std::min(static_cast(size), data.size());
+ auto sz2 = std::min(static_cast(size2), data2.size());
+ std::copy(data.data(), data.data() + sz1, values);
+ std::copy(data2.data(), data2.data() + sz2, values2);
+}
+
+C_PUBLIC void store_both(const double values[], uint32_t size, const double values2[],
+ uint32_t size2)
+{
+ data.assign(values, values + size);
+ data2.assign(values2, values2 + size2);
+}
diff --git a/src/array.hpp b/src/array.hpp
new file mode 100644
index 0000000..94b0048
--- /dev/null
+++ b/src/array.hpp
@@ -0,0 +1,33 @@
+#ifndef UPPAAL_LIBS_ARRAY_HPP
+#define UPPAAL_LIBS_ARRAY_HPP
+
+#include "dynlib.h"
+#include
+
+/// Demonstrates data exchange via arrays
+
+/// Returns the last saved data array size
+C_PUBLIC uint32_t get_size();
+/// Resized the stored data array
+C_PUBLIC void set_size(uint32_t size);
+/// Reads the stored data into a given array
+C_PUBLIC void load_data(double values[], uint32_t size);
+/// Writes data from a given array to storage
+C_PUBLIC void store_data(const double values[], uint32_t size);
+
+/// Returns the last saved data2 array size
+C_PUBLIC uint32_t get_size2();
+/// Resized the stored data2 array
+C_PUBLIC void set_size2(uint32_t size);
+/// Reads the stored data2 into a given array
+C_PUBLIC void load_data2(double values[], uint32_t size);
+/// Writes a given array into data2
+C_PUBLIC void store_data2(const double values[], uint32_t size);
+
+/// Reads the stored data2 into a given array
+C_PUBLIC void load_both(double values1[], uint32_t size1, double values2[], uint32_t size2);
+/// Writes a given array into data2
+C_PUBLIC void store_both(const double values1[], uint32_t size1, const double values2[],
+ uint32_t size2);
+
+#endif // UPPAAL_LIBS_ARRAY_HPP
diff --git a/src/array_test.cpp b/src/array_test.cpp
new file mode 100644
index 0000000..aada1de
--- /dev/null
+++ b/src/array_test.cpp
@@ -0,0 +1,110 @@
+#include "library.hpp"
+
+#include
+
+#include
+#include
+#include
+
+#if defined(__linux__)
+const auto array_path = std::filesystem::current_path() / "libarray.so";
+#elif defined(__APPLE__)
+const auto array_path = std::filesystem::current_path() / "libarray.dylib";
+#elif defined(__MINGW32__)
+const auto array_path = std::filesystem::current_path() / "libarray.dll";
+#elif defined(_WIN32)
+const auto array_path = [] {
+ // CMake on Windows puts Release binaries into CMAKE_CURRENT_BINARY_DIR/Release
+ // otherwise binaries are in CMAKE_CURRENT_BINARY_DIR
+ auto buffer = std::string(1024, '\0');
+ auto size = GetModuleFileNameA(
+ NULL, buffer.data(), static_cast(buffer.size())); // path to current executable
+ while (size >= buffer.size()) {
+ buffer.resize(buffer.size() * 2, '\0');
+ size = GetModuleFileNameA(NULL, buffer.data(), static_cast(buffer.size()));
+ }
+ buffer.resize(size); // truncate the path
+ return std::filesystem::path{buffer}.parent_path() / "array.dll";
+}();
+#else
+#error("Unknown platform")
+#endif
+
+TEST_CASE("Array storage")
+{
+ using get_size_fn = uint32_t (*)();
+ using set_size_fn = void (*)(uint32_t);
+ using load_data_fn = void (*)(double[], uint32_t);
+ using store_data_fn = void (*)(const double[], uint32_t);
+ using load_both_fn = void (*)(double[], uint32_t, double[], uint32_t);
+ using store_both_fn = void (*)(const double[], uint32_t, const double[], uint32_t);
+ try {
+ auto lib = Library{array_path.string()};
+ auto get_size = lib.lookup("get_size");
+ auto set_size = lib.lookup("set_size");
+ auto load_data = lib.lookup("load_data");
+ auto store_data = lib.lookup("store_data");
+
+ auto get_size2 = lib.lookup("get_size2");
+ auto set_size2 = lib.lookup("set_size2");
+ auto load_data2 = lib.lookup("load_data2");
+ auto store_data2 = lib.lookup("store_data2");
+
+ auto load_both = lib.lookup("load_both");
+ auto store_both = lib.lookup("store_both");
+
+ /// Test access to the first array:
+ CHECK(get_size() == 0);
+ set_size(2);
+ CHECK(get_size() == 2);
+ const auto input = std::vector{2.1718, 3.1415, 42.0};
+ auto output = std::vector(3, 0.0);
+ load_data(output.data(), output.size());
+ CHECK(get_size() == 2);
+ CHECK(output[0] == 0);
+ CHECK(output[1] == 0);
+ store_data(input.data(), input.size());
+ CHECK(get_size() == 3);
+ load_data(output.data(), output.size());
+ REQUIRE(get_size() == 3);
+ CHECK(output[0] == 2.1718);
+ CHECK(output[1] == 3.1415);
+ CHECK(output[2] == 42.0);
+
+ /// Test access to the second array:
+ CHECK(get_size2() == 0);
+ set_size2(2);
+ CHECK(get_size2() == 2);
+ load_data2(output.data(), output.size());
+ REQUIRE(get_size2() == 2);
+ CHECK(output[0] == 0);
+ CHECK(output[1] == 0);
+ store_data2(input.data(), input.size());
+ REQUIRE(get_size2() == 3);
+ load_data2(output.data(), output.size());
+ CHECK(get_size2() == 3);
+ CHECK(output[0] == 2.1718);
+ CHECK(output[1] == 3.1415);
+ CHECK(output[2] == 42.0);
+
+ /// Test access to both arrays at once:
+ const auto input2 = std::vector{42.0, 2.1718, 3.1415};
+ auto output2 = std::vector(3, 0.0);
+ load_both(output.data(), output.size(), output2.data(), output2.size());
+ CHECK(output == input);
+ CHECK(output2 == input);
+ set_size(2);
+ set_size2(2);
+ CHECK(get_size() == 2);
+ CHECK(get_size2() == 2);
+ store_both(input2.data(), input2.size(), input2.data(), input2.size());
+ REQUIRE(get_size() == 3);
+ REQUIRE(get_size2() == 3);
+ load_both(output.data(), output.size(), output2.data(), output2.size());
+ CHECK(output == input2);
+ CHECK(output2 == input2);
+ } catch (std::exception& e) {
+ std::cerr << e.what() << std::endl;
+ REQUIRE(false);
+ }
+}
\ No newline at end of file
diff --git a/src/test_errors.cpp b/src/errors_test.cpp
similarity index 91%
rename from src/test_errors.cpp
rename to src/errors_test.cpp
index fa204ee..70046a6 100644
--- a/src/test_errors.cpp
+++ b/src/errors_test.cpp
@@ -26,8 +26,8 @@ TEST_CASE("Error message")
CHECK(message == "Testing: errors 42 3.141000");
const auto at_pos = content.find(" at ", in_pos + 1);
REQUIRE(at_pos != std::string_view::npos);
- const auto test_errors_pos = content.find("test_errors.cpp", at_pos + 4);
+ const auto test_errors_pos = content.find("errors_test.cpp", at_pos + 4);
REQUIRE(test_errors_pos != std::string_view::npos);
const auto location = content.substr(test_errors_pos);
- CHECK(location == "test_errors.cpp:12\n");
+ CHECK(location == "errors_test.cpp:12\n");
}
\ No newline at end of file
diff --git a/src/library.hpp b/src/library.hpp
index b5c9c1e..4ec3cec 100644
--- a/src/library.hpp
+++ b/src/library.hpp
@@ -18,7 +18,7 @@ class Library
void* handle; // library handle
public:
- Library(const char* filepath): handle{dlopen(filepath, RTLD_LAZY | RTLD_LOCAL)}
+ Library(const std::string& filepath): handle{dlopen(filepath.c_str(), RTLD_LAZY | RTLD_LOCAL)}
{
if (!handle)
throw std::runtime_error{dlerror()};
@@ -55,7 +55,7 @@ class Library
HMODULE handle; // library handle
public:
- Library(const char* filepath): handle{LoadLibrary(TEXT(filepath))}
+ Library(const std::string& filepath): handle{LoadLibrary(TEXT(filepath.c_str()))}
{
if (!handle) {
auto err_no = static_cast(::GetLastError());
diff --git a/src/test_table.cpp b/src/table_test.cpp
similarity index 96%
rename from src/test_table.cpp
rename to src/table_test.cpp
index cdb04fb..c5f328d 100644
--- a/src/test_table.cpp
+++ b/src/table_test.cpp
@@ -50,9 +50,8 @@ TEST_CASE("load libtable")
auto approx = doctest::Approx{0}.epsilon(0.00001);
try {
- auto lib_path_str = table_path.string();
- std::cout << "Loading " << lib_path_str << std::endl;
- auto lib = Library{lib_path_str.c_str()}; // may throw upon errors
+ std::cout << "Loading " << table_path << std::endl;
+ auto lib = Library{table_path.string()}; // may throw upon errors
auto table_new_int [[maybe_unused]] = lib.lookup("table_new_int");
auto table_new_double = lib.lookup("table_new_double");
auto table_resize_int [[maybe_unused]] = lib.lookup("table_resize_int");
diff --git a/table.xml b/table.xml
index 937bb7c..71ff154 100644
--- a/table.xml
+++ b/table.xml
@@ -1,24 +1,24 @@
-
+
import "/tmp/uppaal-libs/libtable-dbg.so" {
int table_new_int(int rows, int cols, int value); // creates a new table and returns its id
int table_new_double(int rows, int cols, double value); // creates a new table and returns its id
int table_read_csv(const string& filename, int skip_lines); // reads table from csv file and returns id
- int table_write_csv(int id, const string& filename); // writes table to csv file and returns number of rows
+ int table_write_csv(int id, const string& filename); // writes table to csv file and returns number of rows
int table_copy(int id); // creates a new table copy and returns its id
int table_clear(int id); // releases resources associated with the table and returns id
int table_resize_int(int id, int rows, int cols, int value); // resizes the table with given dimensions
int table_rows(int id); // number of rows in the table
int table_cols(int id); // number of columns in the table
- int read_int(int id, int row, int col); // read integer at row:col
- double read_double(int id, int row, int col); // read double at row:col
+ int read_int(int id, int row, int col); // read integer at row:col
+ double read_double(int id, int row, int col); // read double at row:col
// interpolated look up for key in key_column (sorted in ascending order) and returns value_column
double interpolate(int id, double key, int key_column, int value_column);
- void write_int(int id, int row, int col, int value); // write integer at row:col
- void write_double(int id, int row, int col, double value); // write double at row:col
- void read_int_col(int id, int row, int col, int& items[4], int offset, int count); // read column
- void read_int_row(int id, int row, int col, int& items[3], int offset, int count); // read row
+ void write_int(int id, int row, int col, int value); // write integer at row:col
+ void write_double(int id, int row, int col, double value); // write double at row:col
+ void read_int_col(int id, int row, int col, int& items[4], int offset, int count); // read column
+ void read_int_row(int id, int row, int col, int& items[4], int offset, int count); // read row
};
const int id = table_read_csv("/tmp/uppaal-libs/table_input.csv", 0);
@@ -42,23 +42,20 @@ int table[rows][cols];
void read_all()
{
if (rows>0 && cols>0) {
- for (i : int[0,rows-1])
- for (j : int[0,cols-1])
- table[i][j] = read_int(_id, i, j);
+ for (r : int[0,rows-1])
+ for (c : int[0,cols-1])
+ table[r][c] = read_int(_id, r, c);
}
}
void read_by_row()
{
-// crash
-// for (r : int[0,rows-1])
-/*
- const int r = 0;
- //row_t row;
- int row[3];
+ for (r : int[0,rows-1]) {
+ int row[4];
read_int_row(id, r, 0, row, 0, cols);
- table[r] = row;
-*/
+ for (c : int[0,cols-1])
+ table[r][c] = row[c];
+ }
}
@@ -109,82 +106,15 @@ system Process;
- simulate 1 [<=1] { id, rows, cols, len }
+ simulate [<=1] { id, rows, cols, len }
- simulate 1 [<=10] { interpolate(id, t, 0, 1), interpolate(id, t, 0, 3) }
+ simulate [<=10] { interpolate(id, t, 0, 1), interpolate(id, t, 0, 3) }
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- 0.0,0.0
-0.0,5.0
-0.9414457301025632,5.0
-1.0349100048926037,5.034910004892604
-3.9656626646137303,7.96566266461373
-4.06031870243298,8.0
-10.0,8.0
-
- 0.0,0.0
-0.0,1.0
-0.9414457301025632,1.0
-1.0349100048926037,1.1047299959958121
-1.9780855313525585,3.934256580691863
-2.072691053829776,4.3634551890810505
-2.924455899968412,8.622279417106203
-3.019109181427911,9.13376428914594
-3.9656626646137303,15.75963853437155
-4.06031870243298,16.0
-10.0,16.0
-
-
-
-
- //simulate 1 [<=10] {table[0][0], table[0][1], table[0,2]}
+ //simulate [<=10] {table[0][0], table[0][1], table[0,2]}