Skip to content
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

Closed
RyanGlScott opened this issue Feb 17, 2022 · 3 comments

Comments

@RyanGlScott
Copy link

In the what4-solvers repo, we're building a native Windows abc binary using MinGW-w64. 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 https://github.com/berkeley-abc/abc/issues/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 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 (pAbc=pAbc@entry=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 (argc=argc@entry=5, 
    argv=argv@entry=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:

abc/src/base/cmd/cmdLoad.c

Lines 113 to 129 in 796c290

Vec_Ptr_t * CmdCollectFileNames()
{
Vec_Ptr_t * vFileNames;
struct _finddata_t c_file;
long hFile;
if( (hFile = _findfirst( "*.exe", &c_file )) == -1L )
{
// Abc_Print( 0, "No files with extention \"%s\" in the current directory.\n", "exe" );
return NULL;
}
vFileNames = Vec_PtrAlloc( 100 );
do {
Vec_PtrPush( vFileNames, Extra_UtilStrsav( c_file.name ) );
} while( _findnext( hFile, &c_file ) == 0 );
_findclose( hFile );
return vFileNames;
}

In particular, the segfault occurs on the _findnext invocation. Upon a closer reading of the documentation for _findnext, 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. A more thorough audit of each use of _findnext is likely warranted.

RyanGlScott added a commit to GaloisInc/what4-solvers that referenced this issue Feb 17, 2022
RyanGlScott added a commit to GaloisInc/what4-solvers that referenced this issue Feb 17, 2022
@alanminko
Copy link
Contributor

alanminko commented Feb 18, 2022 via email

@RyanGlScott
Copy link
Author

Thank you for the report. A fix was added to the repository.

Thanks! Should long hFile also be changed to ABC_PTRINT_T hFile in these locations as well?

These are all passed to _findnext at some point, and are therefore subject to the same issue.

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

Ah, I had missed commit bafd2a7. I'll check to see if that has resolved #136.

@RyanGlScott
Copy link
Author

The other uses of long hFile were changed to ABC_PTRINT_T hFile in 31519bd, so this is now resolved.

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

No branches or pull requests

2 participants