Skip to content

Add cdd predt operator#31

Merged
mikucionisaau merged 18 commits intoUPPAALModelChecker:mainfrom
Ecdar:add-cdd_predt
Jul 27, 2022
Merged

Add cdd predt operator#31
mikucionisaau merged 18 commits intoUPPAALModelChecker:mainfrom
Ecdar:add-cdd_predt

Conversation

@magoorden
Copy link
Copy Markdown
Contributor

No description provided.

magoorden and others added 11 commits July 15, 2022 09:35
Co-authored-by: Florian Lorber <florber@cs.aau.dk>

Co-authored-by: Florian Lorber <florber@cs.aau.dk>
Co-authored-by: Florian Lorber <florber@cs.aau.dk>
Co-authored-by: Florian Lorber <florber@cs.aau.dk>
Co-authored-by: Florian Lorber <florber@cs.aau.dk>
Co-authored-by: Florian Lorber <florber@cs.aau.dk>
Co-authored-by: Florian Lorber <florber@cs.aau.dk>
Copy link
Copy Markdown
Member

@mikucionisaau mikucionisaau left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There are some memory issues in cdd_predt_dbm and it also lacks unit tests to trigger some more interesting functionality.

Comment thread src/cppext.cpp Outdated
Comment thread src/cppext.cpp
Comment thread src/cppext.cpp
Comment thread src/cppext.cpp Outdated
Comment thread src/cppext.cpp Outdated
Comment thread src/cppext.cpp Outdated
Comment thread src/cppext.cpp Outdated
Comment thread src/cppext.cpp Outdated
Comment thread src/cppext.cpp
Comment thread test/test_cdd.cpp
Comment thread src/cppext.cpp Outdated
@magoorden
Copy link
Copy Markdown
Contributor Author

I noticed that I did not deinitialized the CDD library in the new test case. So I added in my code locally that

TEST_CASE("CDD timed predecessor static test")
{
  ...
  cdd expected = cdd_remove_negative(expected1 | expected2);

  REQUIRE(cdd_equiv(result, expected));
  cdd_done();
}

But now I get an unexpected 'heap-use-after-free' error from AddressSanitizer. It has something to do with cdd_remove_negative, since when I remove that one from the shown line above, the error is no longer present.

The full error description is

==10537==ERROR: AddressSanitizer: heap-use-after-free on address 0x7fb6edb73800 at pc 0x55d1e3892d5b bp 0x7ffd7b9d57f0 sp 0x7ffd7b9d57e0
WRITE of size 8 at 0x7fb6edb73800 thread T0
    #0 0x55d1e3892d5a in cdd_rec_deref /home/martijn/Documents/UCDD/src/kernel.c:439
    #1 0x55d1e3879e0b in cdd::~cdd() /home/martijn/Documents/UCDD/src/cppext.cpp:44
    #2 0x55d1e3822e06 in DOCTEST_ANON_FUNC_7 /home/martijn/Documents/UCDD/test/test_cdd.cpp:932
    #3 0x55d1e37ee076 in doctest::Context::run() /home/martijn/Documents/UCDD/libs/doctest/include/doctest/doctest.h:6727
    #4 0x55d1e37efe6e in main /home/martijn/Documents/UCDD/libs/doctest/include/doctest/doctest.h:6805
    #5 0x7fb6f123b082 in __libc_start_main ../csu/libc-start.c:308
    #6 0x55d1e37b76dd in _start (/home/martijn/Documents/UCDD/cmake-build-debug/test/test_cdd+0x1c6dd)

0x7fb6edb73800 is located 0 bytes inside of 160000-byte region [0x7fb6edb73800,0x7fb6edb9a900)
freed by thread T0 here:
    #0 0x7fb6f186240f in __interceptor_free ../../../../src/libsanitizer/asan/asan_malloc_linux.cc:122
    #1 0x55d1e3891f59 in cdd_done /home/martijn/Documents/UCDD/src/kernel.c:286
    #2 0x55d1e3822dfa in DOCTEST_ANON_FUNC_7 /home/martijn/Documents/UCDD/test/test_cdd.cpp:937
    #3 0x55d1e37ee076 in doctest::Context::run() /home/martijn/Documents/UCDD/libs/doctest/include/doctest/doctest.h:6727
    #4 0x55d1e37efe6e in main /home/martijn/Documents/UCDD/libs/doctest/include/doctest/doctest.h:6805
    #5 0x7fb6f123b082 in __libc_start_main ../csu/libc-start.c:308

previously allocated by thread T0 here:
    #0 0x7fb6f1862808 in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cc:144
    #1 0x55d1e38919a1 in cdd_init /home/martijn/Documents/UCDD/src/kernel.c:197
    #2 0x55d1e3821afe in DOCTEST_ANON_FUNC_7 /home/martijn/Documents/UCDD/test/test_cdd.cpp:891
    #3 0x55d1e37ee076 in doctest::Context::run() /home/martijn/Documents/UCDD/libs/doctest/include/doctest/doctest.h:6727
    #4 0x55d1e37efe6e in main /home/martijn/Documents/UCDD/libs/doctest/include/doctest/doctest.h:6805
    #5 0x7fb6f123b082 in __libc_start_main ../csu/libc-start.c:308

@mikucionisaau
Copy link
Copy Markdown
Member

I noticed that I did not deinitialized the CDD library in the new test case. So I added in my code locally that

TEST_CASE("CDD timed predecessor static test")
{
  ...
  cdd expected = cdd_remove_negative(expected1 | expected2);

  REQUIRE(cdd_equiv(result, expected));
  cdd_done();
}

But now I get an unexpected 'heap-use-after-free' error from AddressSanitizer. It has something to do with cdd_remove_negative, since when I remove that one from the shown line above, the error is no longer present.

I guess that cdd_done() frees all cdd instances, but then you have one expected left, which results in double-free.
Try putting your expected into a separate scope instead, like:

  {  
     cdd expected = cdd_remove_negative(expected1 | expected2);
     REQUIRE(cdd_equiv(result, expected));
  }
  cdd_done();

This will guarantee that expected is destroyed before cdd_done().
I am not entirely sure why cdd_done() is needed, looks like another hack with global variables :-(

@mikucionisaau mikucionisaau merged commit 870e053 into UPPAALModelChecker:main Jul 27, 2022
@magoorden
Copy link
Copy Markdown
Contributor Author

I guess that cdd_done() frees all cdd instances, but then you have one expected left, which results in double-free. Try putting your expected into a separate scope instead, like:

  {  
     cdd expected = cdd_remove_negative(expected1 | expected2);
     REQUIRE(cdd_equiv(result, expected));
  }
  cdd_done();

This will guarantee that expected is destroyed before cdd_done(). I am not entirely sure why cdd_done() is needed, looks like another hack with global variables :-(

Doing this will push the error message further back into the test case. It only works when I do

TEST_CASE("CDD timed predecessor static test")
{
    cdd_init(100000, 10000, 10000);
    cdd_add_clocks(4);
    cdd_add_bddvar(3);
    {
      // Actual content of the test case.
    }
    cdd_done();
}

This is not what I expected of using cdd_done(), see other test cases (like "CDD intersection with size 3") where there is no need for putting the content of the test case within a name space.

@magoorden magoorden deleted the add-cdd_predt branch July 27, 2022 08:42
@magoorden
Copy link
Copy Markdown
Contributor Author

I am not entirely sure why cdd_done() is needed, looks like another hack with global variables :-(

Yes, not performing cdd_done() messes up with global variables, like the number of clocks and boolean variables in the library. Subsequent test cases have problems when the previous test case does not perform the cdd_done(). I'll make a new pull request to add this to the test case before I push new stuff.

magoorden added a commit to Ecdar/UCDD that referenced this pull request Jul 27, 2022
To prevent memory issues, the actual test case is placed into its own namespace, see UPPAALModelChecker#31 and UPPAALModelChecker#36.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants