-
Notifications
You must be signed in to change notification settings - Fork 601
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
MinGW-w64–compiled abc
segfaults when run in directory with at least one .exe
file
#154
Comments
Thank you for the report. A fix was added to the repository. However,
instead of the suggested
intptr_t hFile;
the following was used:
ABC_PTRINT_T hFile;
because "stdint.h" is not available on all Windows platforms while ABC
already has the type of integer equal to the pointer type (ABC_PTRINT_T)
defined.
Please note that the work-around for issue #136
echo "double Cudd_CountMinterm( DdManager * manager, DdNode * node,
int nvars ) { return 0.0; }" >> src/base/abci/abc.c
may not be needed because it was addressed since the report on Sep 7,
2021, and now |bc_CommandPrintMint()| is protected by |#ifdef
ABC_USE_CUDD / #endif
|
Thanks,
Alan
…On 2/17/2022 5:04 AM, Ryan Scott wrote:
In the |what4-solvers| <https://github.com/GaloisInc/what4-solvers>
repo, we're building a native Windows |abc| binary using MinGW-w64
<https://www.mingw-w64.org/>. Here is how we are building it at the
moment:
# Windows has no libdl
sed -i.bak -e's/-ldl//' Makefile
# Windows has no librt
sed -i.bak2 -e's/-lrt//' Makefile
# Work around #136
echo "double Cudd_CountMinterm( DdManager * manager, DdNode * node, int
nvars ) { return 0.0; }" >> src/base/abci/abc.c
make ABC_USE_NO_READLINE=1 ABC_USE_NO_PTHREADS=1 ABC_USE_NO_CUDD=1 CXXFLAGS="-fpermissive -DNT64 -DWIN32_NO_DLL" CFLAGS="-DNT64 -DWIN32_NO_DLL" LDFLAGS="-static" -j4 abc
This builds successfully, but if you try to run the resulting
|abc.exe| file in the same directory, it will segfault:
|$ ./abc.exe -S "%blast; &sweep -C 5000; &syn4; &cec -m -s" <
../what4-solvers/problems/mult_dist.smt2 Segmentation fault |
What's even stranger is that if you change to a directory that does
/not/ have any |.exe| files and run the same command, it will succeed:
|$ ../abc.exe -S "%blast; &sweep -C 5000; &syn4; &cec -m -s" <
../../what4-solvers/problems/mult_dist.smt2 unsat |
Here
<https://github.com/GaloisInc/what4-solvers/runs/5224960211?check_suite_focus=true#step:9:2544>
is the backtrace that |gdb| gives for the earlier segfault:
|+ gdb -ex 'run -S "%blast; &sweep -C 5000; &syn4; &cec -m -s" <
/d/a/what4-solvers/what4-solvers/problems/mult_dist.smt2' -ex bt -ex
quit ./abc.exe GNU gdb (GDB) 11.2 Copyright (C) 2022 Free Software
Foundation, Inc. License GPLv3+: GNU GPL version 3 or later
<http://gnu.org/licenses/gpl.html> This is free software: you are free
to change and redistribute it. There is NO WARRANTY, to the extent
permitted by law. Type "show copying" and "show warranty" for details.
This GDB was configured as "x86_64-w64-mingw32". Type "show
configuration" for configuration details. For bug reporting
instructions, please see: <https://www.gnu.org/software/gdb/bugs/>.
Find the GDB manual and other documentation resources online at:
<http://www.gnu.org/software/gdb/documentation/>. For help, type
"help". Type "apropos word" to search for commands related to
"word"... warning: Error in redirection: No such file or directory.
Reading symbols from ./abc.exe... Starting program:
D:\a\what4-solvers\what4-solvers\bin\abc.exe -S "%blast; &sweep -C
5000; &syn4; &cec -m -s" <
/d/a/what4-solvers/what4-solvers/problems/mult_dist.smt2 [New Thread
2488.0x1b8] + cd /d/a/what4-solvers/what4-solvers/bin Thread 1
received signal SIGSEGV, Segmentation fault. 0x00007ffa52bc437d in
ntdll!RtlEnterCriticalSection () from C:\Windows\SYSTEM32\ntdll.dll #0
0x00007ffa52bc437d in ntdll!RtlEnterCriticalSection () from
C:\Windows\SYSTEM32\ntdll.dll #1 0x00007ffa4f08ca55 in
KERNELBASE!FindNextFileW () from C:\Windows\System32\KernelBase.dll #2
0x00007ffa4f08c8f8 in KERNELBASE!FindNextFileA () from
C:\Windows\System32\KernelBase.dll #3 0x00007ffa50fa6e0a in
msvcrt!_findnext64 () from C:\Windows\System32\msvcrt.dll #4
0x00007ff68d948efc in _findnext64i32 (_FindData=0x83f5f6cc0,
_FindHandle=-1904445584) at D:/a/_temp/msys64/mingw64/include/io.h:261
#5 CmdCollectFileNames () at src/base/cmd/cmdLoad.c:126 #6
0x00007ff68d94902a in Load_Init ***@***.***=0x13e8e9a2d80) at
src/base/cmd/cmdLoad.c:168 #7 0x00007ff68d986ca4 in Abc_FrameInit
(pAbc=0x13e8e9a2d80) at src/base/main/mainInit.c:116 #8
0x00007ff68d986a1e in Abc_FrameGetGlobalFrame () at
src/base/main/mainFrame.c:649 #9 0x00007ff68d9871aa in Abc_RealMain
***@***.***=5, ***@***.***=0x13e8e7b26a0) at
src/base/main/mainReal.c:114 #10 0x00007ff68d9856ca in main (argc=5,
argv=0x13e8e7b26a0) at src/base/main/main.c:11 A debugging session is
active. Inferior 1 [process 2488] will be killed. Quit anyway? (y or
n) [answered Y; input not from terminal] |
This points to the following code in |abc| as the culprit:
https://github.com/berkeley-abc/abc/blob/796c29039a4983e92bf12051d73326758127162e/src/base/cmd/cmdLoad.c#L113-L129
In particular, the segfault occurs on the |_findnext| invocation. Upon
a closer reading of the documentation for |_findnext|
<https://docs.microsoft.com/en-us/cpp/c-runtime-library/reference/findnext-functions?view=msvc-170>,
the first argument should be an |intptr_t|, but |hFile| is instead
declared as a |long|. This actually makes a difference, since a |long|
is 4 bytes whereas an |intptr_t| is 8 bytes on MinGW-w64. If I apply
the following patch:
diff --git a/src/base/cmd/cmdLoad.c b/src/base/cmd/cmdLoad.c
index accd9440..ae484c41 100644
--- a/src/base/cmd/cmdLoad.c
+++ b/src/base/cmd/cmdLoad.c
@@ -98,6 +98,7 @@ int CmdCommandLoad( Abc_Frame_t * pAbc, int argc, char ** argv )
#include <direct.h>
#include <io.h>
+#include <stdint.h>
/**Function*************************************************************
@@ -114,7 +115,7 @@ Vec_Ptr_t * CmdCollectFileNames()
{
Vec_Ptr_t * vFileNames;
struct _finddata_t c_file;
- long hFile;
+ intptr_t hFile;
if( (hFile = _findfirst( "*.exe", &c_file )) == -1L )
{
// Abc_Print( 0, "No files with extention \"%s\" in the current directory.\n", "exe" );
That fixes the issue. There are many other places where a |long| is
being passed to |_findnext| and friends, however, such as here
<https://github.com/berkeley-abc/abc/blob/796c29039a4983e92bf12051d73326758127162e/src/base/cmd/cmd.c#L1263>.
A more thorough audit of each use of |_findnext| is likely warranted.
—
Reply to this email directly, view it on GitHub
<#154>, or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AI4DBXUX3WPDAK34AODH6GDU3TW7LANCNFSM5OUT47GQ>.
Triage notifications on the go with GitHub Mobile for iOS
<https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675>
or Android
<https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.
You are receiving this because you are subscribed to this
thread.Message ID: ***@***.***>
|
Thanks! Should
These are all passed to
Ah, I had missed commit bafd2a7. I'll check to see if that has resolved #136. |
The other uses of |
In the
what4-solvers
repo, we're building a native Windowsabc
binary using MinGW-w64. Here is how we are building it at the moment:This builds successfully, but if you try to run the resulting
abc.exe
file in the same directory, it will segfault:What's even stranger is that if you change to a directory that does not have any
.exe
files and run the same command, it will succeed:Here is the backtrace that
gdb
gives for the earlier segfault:This points to the following code in
abc
as the culprit:abc/src/base/cmd/cmdLoad.c
Lines 113 to 129 in 796c290
In particular, the segfault occurs on the
_findnext
invocation. Upon a closer reading of the documentation for_findnext
, the first argument should be anintptr_t
, buthFile
is instead declared as along
. This actually makes a difference, since along
is 4 bytes whereas anintptr_t
is 8 bytes on MinGW-w64. If I apply the following patch:That fixes the issue. There are many other places where a
long
is being passed to_findnext
and friends, however, such as here. A more thorough audit of each use of_findnext
is likely warranted.The text was updated successfully, but these errors were encountered: