search

MPI-SWS / genmc

Generic model checker for concurrent C programs (mirror repository)
https://plv.mpi-sws.org/genmc
GNU General Public License v3.0
104 stars 17 forks source link

Compiling with optimizations disabled results in runtime error #57

Open matteo-meluzzi opened 7 months ago

matteo-meluzzi commented 7 months ago

When running a genmc executable compiled with optimizations disabled, I get a runtime error. When running genmc with the default compiler flags, everything runs smoothly.

How to reproduce: 1) checkout master branch 2) autoreconf -i to generate the configure script 3) ./configure AR=llvm-ar CXXFLAGS="-O0 -g" to generate Makefile 4) make genmc to generate genmc executable 5) ./genmc --print-exec-graphs tests/correct/litmus/LB2/variants/lb0.c outputs:

GenMC v0.10.0 (LLVM 15.0.7)
Copyright (C) 2023 MPI-SWS. All rights reserved.

*** Compilation complete.
*** Transformation complete.
Tip: Estimating state-space size. For better performance, you can use --disable-estimation.
libc++abi: terminating due to uncaught exception of type std::length_error: vector
zsh: abort      ./genmc --print-exec-graphs tests/correct/litmus/LB2/variants/lb0.c

In contrast the same steps except for 3) ./configure AR=llvm-ar outputs

No errors were detected.
Number of complete executions explored: 3
Total wall-clock time: 0.11s

I am using MacOS 14, llvm@15 installed

JonasOberhauser commented 6 months ago

unlikely to be fixed. IIRC llvm requires at least -O2

matteo-meluzzi commented 5 months ago

I see. Thank you for the reply! Is there any online resources that explain why this is the case?

JonasOberhauser commented 4 months ago

Can't find anything now. Heck maybe I dreamed the whole thing up, or it has been fixed since Iooked at it 4 years ago?

But as I remember, llvm used some... uh... not so sound things that break under -O0.

Maybe @michaliskok can weigh in and provide some clarity

JonasOberhauser commented 4 months ago

Also just for the sake of it, try downgrading to LLVM 15.0.0