Added library example for double arrays

.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
 

.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

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)

array.xml

@@ -0,0 +1,134 @@
+<?xml version="1.0" encoding="utf-8"?>
+<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.6//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_6.dtd'>
+<nta>
+	<declaration>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&amp; values[N], uint32_t size); /// Reads the stored data into a given array
+    void store_data(const double&amp; 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&amp; values[N], uint32_t size); /// Reads the stored data2 into a given array
+    void store_data2(const double&amp; values[N], uint32_t size); /// Stores into the data2
+
+    void load_both(double&amp; values[N], uint32_t size, double&amp; values2[N], uint32_t size2); /// Reads both data and data2
+    void store_both(const double&amp; values[N], uint32_t size, const double&amp; 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];
+</declaration>
+	<template>
+		<name x="5" y="5">P</name>
+		<declaration>clock x;</declaration>
+		<location id="id0" x="408" y="170">
+		</location>
+		<location id="id1" x="136" y="170">
+		</location>
+		<location id="id2" x="646" y="0">
+			<name x="636" y="-34">Done</name>
+		</location>
+		<location id="id3" x="-68" y="170">
+		</location>
+		<location id="id4" x="136" y="0">
+			<urgent/>
+		</location>
+		<location id="id5" x="-272" y="0">
+			<urgent/>
+		</location>
+		<location id="id6" x="-68" y="0">
+			<urgent/>
+		</location>
+		<location id="id7" x="408" y="0">
+			<urgent/>
+		</location>
+		<init ref="id5"/>
+		<transition id="id8">
+			<source ref="id7"/>
+			<target ref="id0"/>
+			<label kind="guard" x="425" y="51">size != N ||
+(exists(i:int[0,N-1])
+   in[i] != out2[i]) ||
+size2 != N ||
+(exists(i:int[0,N-1])
+   in2[i] != out[i])</label>
+		</transition>
+		<transition id="id9">
+			<source ref="id7"/>
+			<target ref="id2"/>
+			<label kind="guard" x="433" y="-127">size == N &amp;&amp;
+(forall(i:int[0,N-1])
+   in[i] == out2[i]) &amp;&amp;
+size2 == N &amp;&amp;
+(forall(i:int[0,N-1])
+   in2[i] == out[i])</label>
+		</transition>
+		<transition id="id10">
+			<source ref="id4"/>
+			<target ref="id7"/>
+			<label kind="guard" x="161" y="-119">size == N &amp;&amp;
+(forall(i:int[0,N-1])
+   in[i] == out[i]) &amp;&amp;
+size2 == N &amp;&amp;
+(forall(i:int[0,N-1])
+   in2[i] == out2[i])</label>
+			<label kind="assignment" x="161" y="0">store_both(in2, N, in, N),
+load_both(out, N, out2, N)</label>
+		</transition>
+		<transition id="id11">
+			<source ref="id4"/>
+			<target ref="id1"/>
+			<label kind="guard" x="153" y="51">size != N ||
+(exists(i:int[0,N-1])
+   in[i] != out[i]) ||
+size2 != N ||
+(exists(i:int[0,N-1])
+   in2[i] != out2[i])</label>
+		</transition>
+		<transition id="id12">
+			<source ref="id6"/>
+			<target ref="id3"/>
+			<label kind="guard" x="-59" y="93">size != N ||
+size2 != N</label>
+		</transition>
+		<transition id="id13">
+			<source ref="id6"/>
+			<target ref="id4"/>
+			<label kind="guard" x="-42" y="-42">size == N &amp;&amp;
+size2 == N</label>
+			<label kind="assignment" x="-42" y="0">load_data(out, N),
+size = get_size(),
+load_data2(out2, N),
+size2 = get_size2()</label>
+		</transition>
+		<transition id="id14">
+			<source ref="id5"/>
+			<target ref="id6"/>
+			<label kind="guard" x="-255" y="-42">init_size == 0 &amp;&amp;
+init_size == 0</label>
+			<label kind="assignment" x="-254" y="0">store_data(in, N),
+size = get_size(),
+store_data2(in2, N),
+size2 = get_size2()</label>
+		</transition>
+	</template>
+	<system>system P;</system>
+	<queries>
+		<query>
+			<formula>simulate [&lt;=1; 100] { size } : 100 : P.Done</formula>
+			<comment/>
+		</query>
+	</queries>
+</nta>

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)

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"

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)

src/array.cpp

@@ -0,0 +1,51 @@
+#include "array.hpp"
+#include <vector>
+
+static auto data = std::vector<double>{};
+
+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<std::size_t>(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<double>{};
+
+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<std::size_t>(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<std::size_t>(size), data.size());
+	auto sz2 = std::min(static_cast<std::size_t>(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);
+}

src/array.hpp

@@ -0,0 +1,33 @@
+#ifndef UPPAAL_LIBS_ARRAY_HPP
+#define UPPAAL_LIBS_ARRAY_HPP
+
+#include "dynlib.h"
+#include <cinttypes>
+
+/// 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