search

microsoft / WSL

Issues found on WSL
https://docs.microsoft.com/windows/wsl
MIT License
17.26k stars 812 forks source link

NuSMV crashes with Segmentation Fault #10071

Open lwrage opened 1 year ago

lwrage commented 1 year ago

Windows Version

Microsoft Windows [Version 10.0.22621.1555]

WSL Version

WSL version: 1.2.5.0 Kernel version: 5.15.90.1 WSLg version: 1.0.51 MSRDC version: 1.2.3770 Direct3D version: 1.608.2-61064218 DXCore version: 10.0.25131.1002-220531-1700.rs-onecore-base2-hyp Windows version: 10.0.22621.1555

Are you using WSL 1 or WSL 2?

Kernel Version

5.15.90.1-microsoft-standard-WSL2

Distro Version

Ubuntu 22.04

Other Software

NuSMV 2.6.0 64bit, downloaded from https://nusmv.fbk.eu/distrib/NuSMV-2.6.0-linux64.tar.gz

Repro Steps

extract zip file, cd NuSMV-2.6.0-Linux/bin directory run the program ./NuSMV -int at the propmpt type help, then Enter

Expected Behavior

display a list of available NuSMV commands

Actual Behavior

Segmentation fault

Diagnostic Logs

Running the above steps with strace NuSMV -int contains the error: socket(AF_NETLINK, SOCK_RAW, NETLINK_AUDIT) = -1 EPROTONOSUPPORT (Protocol not supported)

Full output:

execve("./NuSMV", ["./NuSMV", "-int"], 0x7ffe5aa27028 /* 30 vars */) = 0
uname({sysname="Linux", nodename="RM-CANANGA", ...}) = 0
brk(NULL)                               = 0x1919000
brk(0x191a1a0)                          = 0x191a1a0
arch_prctl(ARCH_SET_FS, 0x1919880)      = 0
brk(0x193b1a0)                          = 0x193b1a0
brk(0x193c000)                          = 0x193c000
mmap(NULL, 397312, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f3524e6b000
rt_sigprocmask(SIG_BLOCK, NULL, [], 8)  = 0
rt_sigprocmask(SIG_BLOCK, NULL, [], 8)  = 0
rt_sigprocmask(SIG_BLOCK, NULL, [], 8)  = 0
rt_sigprocmask(SIG_BLOCK, NULL, [], 8)  = 0
mmap(NULL, 397312, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f3524e0a000
brk(0x195d000)                          = 0x195d000
getrlimit(RLIMIT_DATA, {rlim_cur=RLIM64_INFINITY, rlim_max=RLIM64_INFINITY}) = 0
mmap(NULL, 528384, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f3524d89000
mmap(NULL, 8392704, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f3524588000
mmap(NULL, 1052672, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f3524487000
rt_sigaction(SIGUSR1, {sa_handler=0x4059d0, sa_mask=[USR1], sa_flags=SA_RESTORER|SA_RESTART, sa_restorer=0x6e75a0}, {sa_handler=SIG_DFL, sa_mask=[], sa_flags=0}, 8) = 0
getrusage(RUSAGE_SELF, {ru_utime={tv_sec=0, tv_usec=4192}, ru_stime={tv_sec=0, tv_usec=4192}, ...}) = 0
brk(0x197e000)                          = 0x197e000
fstat(1, {st_mode=S_IFCHR|0620, st_rdev=makedev(0x88, 0x6), ...}) = 0
mmap(NULL, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f3524486000
write(1, "*** This is NuSMV 2.6.0 (compile"..., 63*** This is NuSMV 2.6.0 (compiled on Wed Oct 14 15:36:56 2015)
) = 63
write(1, "*** Enabled addons are: compass\n", 32*** Enabled addons are: compass
) = 32
write(1, "*** For more information on NuSM"..., 60*** For more information on NuSMV see <http://nusmv.fbk.eu>
) = 60
write(1, "*** or email to <nusmv-users@lis"..., 43*** or email to <nusmv-users@list.fbk.eu>.
) = 43
write(1, "*** Please report bugs to <Pleas"..., 72*** Please report bugs to <Please report bugs to <nusmv-users@fbk.eu>>

) = 72
write(1, "*** Copyright (c) 2010-2014, Fon"..., 55*** Copyright (c) 2010-2014, Fondazione Bruno Kessler

) = 55
write(1, "*** This version of NuSMV is lin"..., 70*** This version of NuSMV is linked to the CUDD library version 2.4.1
) = 70
write(1, "*** Copyright (c) 1995-2004, Reg"..., 68*** Copyright (c) 1995-2004, Regents of the University of Colorado

) = 68
write(1, "*** This version of NuSMV is lin"..., 64*** This version of NuSMV is linked to the MiniSat SAT solver. 
) = 64
write(1, "*** See http://minisat.se/MiniSa"..., 39*** See http://minisat.se/MiniSat.html
) = 39
write(1, "*** Copyright (c) 2003-2006, Nik"..., 105*** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
*** Copyright (c) 2007-2010, Niklas Sorensson

) = 105
rt_sigaction(SIGINT, {sa_handler=SIG_IGN, sa_mask=[INT], sa_flags=SA_RESTORER|SA_RESTART, sa_restorer=0x6e75a0}, {sa_handler=SIG_DFL, sa_mask=[], sa_flags=0}, 8) = 0
rt_sigaction(SIGINT, {sa_handler=0x401960, sa_mask=[INT], sa_flags=SA_RESTORER|SA_RESTART, sa_restorer=0x6e75a0}, {sa_handler=SIG_IGN, sa_mask=[INT], sa_flags=SA_RESTORER|SA_RESTART, sa_restorer=0x6e75a0}, 8) = 0
rt_sigprocmask(SIG_BLOCK, NULL, [], 8)  = 0
access("/home/wsl/nusmv/master.nusmvrc", R_OK) = -1 ENOENT (No such file or directory)
access("/home/wsl/nusmv//home/wsl/nusmv/master.nusmvrc", R_OK) = -1 ENOENT (No such file or directory)
access("/home/wsl/nusmv//home/wsl/nusmv/master.nusmvrc", R_OK) = -1 ENOENT (No such file or directory)
open("/home/wsl/nusmv/master.nusmvrc", O_RDONLY) = -1 ENOENT (No such file or directory)
rt_sigaction(SIGINT, {sa_handler=SIG_IGN, sa_mask=[INT], sa_flags=SA_RESTORER|SA_RESTART, sa_restorer=0x6e75a0}, {sa_handler=0x401960, sa_mask=[INT], sa_flags=SA_RESTORER|SA_RESTART, sa_restorer=0x6e75a0}, 8) = 0
access("/home/wsl/.nusmvrc", F_OK)   = -1 ENOENT (No such file or directory)
access(".nusmvrc", F_OK)                = -1 ENOENT (No such file or directory)
rt_sigaction(SIGINT, {sa_handler=SIG_IGN, sa_mask=[INT], sa_flags=SA_RESTORER|SA_RESTART, sa_restorer=0x6e75a0}, {sa_handler=SIG_IGN, sa_mask=[INT], sa_flags=SA_RESTORER|SA_RESTART, sa_restorer=0x6e75a0}, 8) = 0
rt_sigaction(SIGINT, {sa_handler=0x401960, sa_mask=[INT], sa_flags=SA_RESTORER|SA_RESTART, sa_restorer=0x6e75a0}, {sa_handler=SIG_IGN, sa_mask=[INT], sa_flags=SA_RESTORER|SA_RESTART, sa_restorer=0x6e75a0}, 8) = 0
rt_sigprocmask(SIG_BLOCK, NULL, [], 8)  = 0
ioctl(0, TCGETS, {B38400 opost isig icanon echo ...}) = 0
ioctl(1, TCGETS, {B38400 opost isig icanon echo ...}) = 0
stat("/home/wsl/.terminfo", 0x7fff0a520bd0) = -1 ENOENT (No such file or directory)
stat("/usr/local/share/terminfo", 0x7fff0a520bd0) = -1 ENOENT (No such file or directory)
ioctl(0, TIOCGWINSZ, {ws_row=58, ws_col=239, ws_xpixel=0, ws_ypixel=0}) = 0
ioctl(0, TIOCGWINSZ, {ws_row=58, ws_col=239, ws_xpixel=0, ws_ypixel=0}) = 0
ioctl(0, TIOCSWINSZ, {ws_row=58, ws_col=239, ws_xpixel=0, ws_ypixel=0}) = 0
ioctl(0, TCGETS, {B38400 opost isig icanon echo ...}) = 0
open("/usr/lib/locale/locale-archive", O_RDONLY) = -1 ENOENT (No such file or directory)
open("/usr/share/locale/locale.alias", O_RDONLY) = 3
fstat(3, {st_mode=S_IFREG|0644, st_size=2996, ...}) = 0
mmap(NULL, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f3524485000
read(3, "# Locale name alias data base.\n#"..., 4096) = 2996
read(3, "", 4096)                       = 0
close(3)                                = 0
munmap(0x7f3524485000, 4096)            = 0
open("/usr/lib/locale/C.UTF-8/LC_CTYPE", O_RDONLY) = -1 ENOENT (No such file or directory)
open("/usr/lib/locale/C.utf8/LC_CTYPE", O_RDONLY) = 3
fstat(3, {st_mode=S_IFREG|0644, st_size=353616, ...}) = 0
mmap(NULL, 353616, PROT_READ, MAP_PRIVATE, 3, 0) = 0x7f352442f000
close(3)                                = 0
open("/usr/lib64/gconv/gconv-modules.cache", O_RDONLY) = -1 ENOENT (No such file or directory)
open("/usr/lib64/gconv/gconv-modules", O_RDONLY) = -1 ENOENT (No such file or directory)
stat("/home/wsl/.inputrc", 0x7fff0a521cc0) = -1 ENOENT (No such file or directory)
stat("/etc/inputrc", {st_mode=S_IFREG|0644, st_size=1748, ...}) = 0
open("/etc/inputrc", O_RDONLY)          = 3
read(3, "# /etc/inputrc - global inputrc "..., 1748) = 1748
close(3)                                = 0
rt_sigprocmask(SIG_BLOCK, [INT], [], 8) = 0
ioctl(0, TIOCGWINSZ, {ws_row=58, ws_col=239, ws_xpixel=0, ws_ypixel=0}) = 0
ioctl(0, TIOCSWINSZ, {ws_row=58, ws_col=239, ws_xpixel=0, ws_ypixel=0}) = 0
ioctl(0, TCGETS, {B38400 opost isig icanon echo ...}) = 0
ioctl(0, SNDCTL_TMR_STOP or TCSETSW, {B38400 opost isig -icanon -echo ...}) = 0
rt_sigprocmask(SIG_SETMASK, [], NULL, 8) = 0
rt_sigprocmask(SIG_BLOCK, [INT QUIT ALRM TERM TSTP TTIN TTOU], [], 8) = 0
rt_sigaction(SIGINT, {sa_handler=0x5b71f0, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, {sa_handler=0x401960, sa_mask=[INT], sa_flags=SA_RESTORER|SA_RESTART, sa_restorer=0x6e75a0}, 8) = 0
rt_sigaction(SIGTERM, {sa_handler=0x5b71f0, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, {sa_handler=SIG_DFL, sa_mask=[], sa_flags=0}, 8) = 0
rt_sigaction(SIGQUIT, {sa_handler=0x5b71f0, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, {sa_handler=SIG_DFL, sa_mask=[], sa_flags=0}, 8) = 0
rt_sigaction(SIGALRM, {sa_handler=0x5b71f0, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, {sa_handler=SIG_DFL, sa_mask=[], sa_flags=0}, 8) = 0
rt_sigaction(SIGTSTP, {sa_handler=0x5b71f0, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, {sa_handler=SIG_DFL, sa_mask=[], sa_flags=0}, 8) = 0
rt_sigaction(SIGTTOU, {sa_handler=0x5b71f0, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, {sa_handler=SIG_DFL, sa_mask=[], sa_flags=0}, 8) = 0
rt_sigaction(SIGTTIN, {sa_handler=0x5b71f0, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, {sa_handler=SIG_DFL, sa_mask=[], sa_flags=0}, 8) = 0
rt_sigprocmask(SIG_SETMASK, [], NULL, 8) = 0
rt_sigaction(SIGWINCH, {sa_handler=0x5b70f0, sa_mask=[], sa_flags=SA_RESTORER|SA_RESTART, sa_restorer=0x6e75a0}, {sa_handler=SIG_DFL, sa_mask=[], sa_flags=0}, 8) = 0
rt_sigprocmask(SIG_BLOCK, [INT], [], 8) = 0
write(1, "NuSMV > ", 8NuSMV > )                 = 8
rt_sigprocmask(SIG_SETMASK, [], NULL, 8) = 0
rt_sigprocmask(SIG_BLOCK, NULL, [], 8)  = 0
read(0, "h", 1)                         = 1
rt_sigprocmask(SIG_BLOCK, [INT], [], 8) = 0
write(1, "h", 1h)                        = 1
rt_sigprocmask(SIG_SETMASK, [], NULL, 8) = 0
rt_sigprocmask(SIG_BLOCK, NULL, [], 8)  = 0
read(0, "e", 1)                         = 1
rt_sigprocmask(SIG_BLOCK, [INT], [], 8) = 0
write(1, "e", 1e)                        = 1
rt_sigprocmask(SIG_SETMASK, [], NULL, 8) = 0
rt_sigprocmask(SIG_BLOCK, NULL, [], 8)  = 0
read(0, "l", 1)                         = 1
rt_sigprocmask(SIG_BLOCK, [INT], [], 8) = 0
write(1, "l", 1l)                        = 1
rt_sigprocmask(SIG_SETMASK, [], NULL, 8) = 0
rt_sigprocmask(SIG_BLOCK, NULL, [], 8)  = 0
read(0, "p", 1)                         = 1
rt_sigprocmask(SIG_BLOCK, [INT], [], 8) = 0
write(1, "p", 1p)                        = 1
rt_sigprocmask(SIG_SETMASK, [], NULL, 8) = 0
rt_sigprocmask(SIG_BLOCK, NULL, [], 8)  = 0
read(0, "\r", 1)                        = 1
write(1, "\n", 1
)                       = 1
rt_sigprocmask(SIG_BLOCK, [INT], [], 8) = 0
ioctl(0, SNDCTL_TMR_STOP or TCSETSW, {B38400 opost isig icanon echo ...}) = 0
rt_sigprocmask(SIG_SETMASK, [], NULL, 8) = 0
rt_sigaction(SIGINT, {sa_handler=0x401960, sa_mask=[INT], sa_flags=SA_RESTORER|SA_RESTART, sa_restorer=0x6e75a0}, {sa_handler=0x5b71f0, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, 8) = 0
rt_sigaction(SIGTERM, {sa_handler=SIG_DFL, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, {sa_handler=0x5b71f0, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, 8) = 0
rt_sigaction(SIGQUIT, {sa_handler=SIG_DFL, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, {sa_handler=0x5b71f0, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, 8) = 0
rt_sigaction(SIGALRM, {sa_handler=SIG_DFL, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, {sa_handler=0x5b71f0, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, 8) = 0
rt_sigaction(SIGTSTP, {sa_handler=SIG_DFL, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, {sa_handler=0x5b71f0, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, 8) = 0
rt_sigaction(SIGTTOU, {sa_handler=SIG_DFL, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, {sa_handler=0x5b71f0, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, 8) = 0
rt_sigaction(SIGTTIN, {sa_handler=SIG_DFL, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, {sa_handler=0x5b71f0, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, 8) = 0
rt_sigaction(SIGWINCH, {sa_handler=SIG_DFL, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x6e75a0}, {sa_handler=0x5b70f0, sa_mask=[], sa_flags=SA_RESTORER|SA_RESTART, sa_restorer=0x6e75a0}, 8) = 0
socket(AF_NETLINK, SOCK_RAW, NETLINK_AUDIT) = -1 EPROTONOSUPPORT (Protocol not supported)
--- SIGSEGV {si_signo=SIGSEGV, si_code=SEGV_MAPERR, si_addr=0xffffffffff600400} ---
+++ killed by SIGSEGV +++
Segmentation fault
elsaco commented 1 year ago

@lwrage you need a kernel with CONFIG_AUDIT enabled. The WSL kernel has # CONFIG_AUDIT is not set:

https://github.com/microsoft/WSL2-Linux-Kernel/blob/a733b4e7e4db00d1647ee23022fbcfce33835c61/Microsoft/config-wsl#L45

elsaco commented 1 year ago

The latest WSL2 kernel (https://github.com/microsoft/WSL2-Linux-Kernel/releases/tag/linux-msft-wsl-6.1.21.2) has auditing support enabled, however NuSMV still crashes:

socket(AF_NETLINK, SOCK_RAW, NETLINK_AUDIT) = 3
sendmsg(3, {msg_name={sa_family=AF_NETLINK, nl_pad=0xac, nl_pid=0, nl_groups=00000000}, msg_namelen=12, msg_iov=[{iov_base={nlmsg_len=21, nlmsg_type=0x464 /* NLMSG_??? */, nlmsg_flags=NLM_F_REQUEST, nlmsg_seq=0, nlmsg_pid=0}, iov_len=16}, {iov_base="\x68\x65\x6c\x70\x00", iov_len=5}], msg_iovlen=2, msg_controllen=0, msg_flags=0}, 0) = 21
close(3)                                = 0
--- SIGSEGV {si_signo=SIGSEGV, si_code=SEGV_MAPERR, si_addr=0xffffffffff600400} ---
+++ killed by SIGSEGV +++

and this is from dmesg output:

[Tue May  9 21:14:22 2023] NuSMV[712] vsyscall attempted with vsyscall=none ip:ffffffffff600400 cs:33 sp:7ffe79d07978 ax:ffffffffff600400 si:190 di:0
[Tue May  9 21:14:22 2023] NuSMV[712]: segfault at ffffffffff600400 ip ffffffffff600400 sp 00007ffe79d07978 error 15 likely on CPU 3 (core 1, socket 0)
[Tue May  9 21:14:22 2023] Code: Unable to access opcode bytes at 0xffffffffff6003d6.
[Tue May  9 21:14:22 2023] potentially unexpected fatal signal 11.
[Tue May  9 21:14:22 2023] CPU: 3 PID: 712 Comm: NuSMV Not tainted 6.1.21.2-wsl2-custom #2
[Tue May  9 21:14:22 2023] RIP: 0033:0xffffffffff600400
[Tue May  9 21:14:22 2023] Code: Unable to access opcode bytes at 0xffffffffff6003d6.
[Tue May  9 21:14:22 2023] RSP: 002b:00007ffe79d07978 EFLAGS: 00010202
[Tue May  9 21:14:22 2023] RAX: ffffffffff600400 RBX: 00007ffe79d07990 RCX: 00000000000001a1
[Tue May  9 21:14:22 2023] RDX: 00000000027ba680 RSI: 0000000000000190 RDI: 0000000000000000
[Tue May  9 21:14:22 2023] RBP: 00000000027a7fc0 R08: 0000000000aed788 R09: 0000000000000001
[Tue May  9 21:14:22 2023] R10: 0000000000000190 R11: 0000000000000246 R12: 000000000279bc70
[Tue May  9 21:14:22 2023] R13: 0000000000000001 R14: 0000000002798120 R15: 00007ffe79d07b90
[Tue May  9 21:14:22 2023] FS:  0000000002756880 GS:  0000000000000000

Time to invoke gdb!

mamadgit commented 11 months ago

Hi @lwrage I am having the exact same problem. did you manage to fix it?