PrincetonUniversity / ILAng

A Modeling and Verification Platform for SoCs using ILAs
https://bo-yuan-huang.gitbook.io/ilang/
MIT License
75 stars 18 forks source link

Allocation exception in unit tests #188

Closed Bo-Yuan-Huang closed 4 years ago

Bo-Yuan-Huang commented 4 years ago

Describe the bug C++ exception std::bad_alloc is found in several unit tests, e.g., TestVlgVerifInvSyn.SimpleCntCegar and TestSmtParse.ChcParse.

To Reproduce This issue seems to be platform dependent (lack of robustness). Within the early investigation, implicit and opened files seem to be relevant.

Environment (please complete the following information):

Additional context Will be address in the PR #187.

Bo-Yuan-Huang commented 4 years ago

Also, it seems to be a c++17 filesystem problem due to compiler library mismatch. https://stackoverflow.com/questions/56738708/c-stdbad-alloc-on-stdfilesystempath-append

(However, this issue only happens in OSX, not the Ubuntu as mentioned.)

Bo-Yuan-Huang commented 4 years ago

Error message:

unit_tests(59330,0x10937edc0) malloc: can't allocate region
:*** mach_vm_map(size=3758289336431292416, flags: 100) failed (error code=3)
unit_tests(59330,0x10937edc0) malloc: *** set a breakpoint in malloc_error_break to debug
unknown file: Failure
C++ exception with description "std::bad_alloc" thrown in the test body.

Using TestVlgVerifInvSyn.LoadInvFromBeginning as the entry point, the issue seems to happen at:

https://github.com/Bo-Yuan-Huang/ILAng/blob/c7d6f9921b07211fd16f65f4b2448703645f913b/src/smt-inout/chc_inv_in.cc#L926