When I try to get the windows version of esbmc to support boolector sovler is runs into problems. about esbmc

[rafaelsamenezes]

I'm actually trying to get a cross-compilation to MingGW working and the only thing missing is a Clang-build. Is there one or do I have to compile my own?

Nice! I tried this once but I had some issues with fixing our operational models. IIRC this is the mingw build that I used, just try a small example first as I am not sure if this was linking properly.

My main issue of compiling ESBMC with mingw is that the operational models are going to be generated with mingw headers instead of MSVC. Not sure how compatible they are, but I know of a few benchmarks that we can not parse in Linux but can parse in Windows.

There is also another approach: make ESBMC only support GOTO inputs. The frontends could be split into separate binaries.

[hanxiatu-github]

Hi @hanxiatu-github! Many thanks for trying it out, it seems to be working so that's good news.

ESBMC doesn't bundle all the system headers, because that would make results between compiling locally and interpreting the C program locally differ (the build headers might not be the same as those on the host running ESBMC). Instead of the --idirafter parameter, I would recommend to use --sysroot "C:\Program Files\mingw64". This puts the include paths into the correct position with respect to the other -I, --idirafter, etc. options.

In case you don't want to specify this option manually everytime, you could either

• set the ESBMC_OPTS environment variable to contain --sysroot "C:\Program Files\mingw64", or
• use a wrapper script (is it still .bat on Windows? Haven't used it for a long time myself).

--sysroot "C:\Program Files\mingw64" is ok。

I decided to use'where gcc' to find gcc, which on my machine is "C:\Program Files\mingw64\bin," and then I could auto-configure --sysroot "C:\Program Files\mingw64".

Also, why would I want to be able to use esbmc which supports boolector on the windows version. Because I found that boolector's performance is much better than z3's in our inspection scenario.

Thank you very much for your support.

[hanxiatu-github]

How to build the esbmc windows version? What are the dependencies on windows, like linux?

Linux:
sudo apt-get update && sudo apt-get install build-essential git gperf libgmp-dev cmake bison curl flex g++-multilib linux-libc-dev libboost-all-dev libtinfo-dev ninja-build python3-setuptools unzip wget python3-pip openjdk-8-jre

[hanxiatu-github]

Or ask such a question, I do not know the possibility and cost of supporting --smtlib --smtlib-solver-prog CMD on Windows.

If it can be done, then I can use --smtlib --smtlib-solver-prog "boolector --incremental" directly for my purposes.

[rafaelsamenezes]

Hi @hanxiatu-github. Sadly you reached some parts of ESBMC that are limited and need a bit more dev time. I will try to answer the questions. Just for context, ESBMC is an old project (almost 15 years) and Windows support was only added a few years ago. Which means that the previous devs implemented some features thinking of Unix systems only.

Windows Build

The Windows build process is a bit hacky. It depends on:

• winflexbison
• boost
• MSVC
• A static build of LLVM

Our CI is currently using this script to download the dependencies: https://github.com/esbmc/esbmc/blob/master/scripts/build.ps1. For the LLVM bit we rely on using -DDOWNLOAD_DEPENDENCIES=1.

Boolector on Windows

Regarding boolector, their guide describes how to generate a MinGW build of it while ESBMC is built using MSVC (due to the LLVM). Linking a MinGW library into a MSVC project... is not as trivial as it should.

SMTLIB

Regarding the SMTLIB, the design relied on Unix pipes for the communaction with the solver. This needs to be ported to work with Windows processes.

[fbrausse]

I'm actually trying to get a cross-compilation to MingGW working and the only thing missing is a Clang-build. Is there one or do I have to compile my own?

[fbrausse]

I've managed to produce a mingw64 build including Z3 and Boolector. If you feel courageous enough, could I ask you to give this a try? If it works, we can update our CI to automatically build these releases.

https://github.com/esbmc/esbmc/releases/tag/v7.5%2Bexp-mingw64

[hanxiatu-github]

I've managed to produce a mingw64 build including Z3 and Boolector. If you feel courageous enough, could I ask you to give this a try? If it works, we can update our CI to automatically build these releases.

https://github.com/esbmc/esbmc/releases/tag/v7.5%2Bexp-mingw64

When I try to use your version, I get the error "fatal error: 'stdio.h' file not found." These errors were also encountered when I used the windows version of cbmc, and were resolved by specifying --gcc (which then gave other errors).

---

Now I try add set --idirafter "C:\Program Files\mingw64\x86_64-w64-mingw32\include" to solve problem。But I would like to know how to solve this problem in a generic way.

[fbrausse]

Hi @hanxiatu-github! Many thanks for trying it out, it seems to be working so that's good news.

ESBMC doesn't bundle all the system headers, because that would make results between compiling locally and interpreting the C program locally differ (the build headers might not be the same as those on the host running ESBMC). Instead of the --idirafter parameter, I would recommend to use --sysroot "C:\Program Files\mingw64". This puts the include paths into the correct position with respect to the other -I, --idirafter, etc. options.

In case you don't want to specify this option manually everytime, you could either

• set the ESBMC_OPTS environment variable to contain --sysroot "C:\Program Files\mingw64", or
• use a wrapper script (is it still .bat on Windows? Haven't used it for a long time myself).

[fbrausse]

My main issue of compiling ESBMC with mingw is that the operational models are going to be generated with mingw headers instead of MSVC. Not sure how compatible they are, but I know of a few benchmarks that we can not parse in Linux but can parse in Windows.

@rafaelsamenezes Indeed, that will be a problem. It seems so far people were using the MSVC headers and models, is that correct?

Instead of including builds for all the several different versions of OMs into the binary, we could compile the OMs with c2goto on the host and store it in ~/.cache or whatever the equivalent on Windows is. For each combination of the architecture related options in #1585 (comment) as well as --fixedbv/--floatbv and the flavor (such as "gnu" or "msvc"), there would be one pre-compiled OM file in the cache.

[hanxiatu-github]

@fbrausse
In more testing, I ran into the following error with the experimental version you provided (with --sysroot C:\Program Files\mingw64 set):

In file included from C:\Users[username]\AppData\Local\Temp\esbmc-headers-92ea-c0c0-cf95/float.h:32:
C:\Program Files\mingw64/x86_64-w64-mingw32/include/float.h:28:15: fatal error: 'float.h' file not found
#include_next <float.h>

---

It seems to be a compatibility issue with my version of mingw

https://stackoverflow.com/questions/57166340/how-do-i-compile-code-using-clang-with-the-mingw-c-c-library-particular-issu

[fbrausse]

@hanxiatu-github This is strange. When I look into Clang's <float.h> (which is bundled and put into your temp-dir as esbmc-headers-92ea-c0c0-cf95/float.h), the corresponding excerpt is this:

#ifndef __CLANG_FLOAT_H
#define __CLANG_FLOAT_H

/* If we're on MinGW, fall back to the system's float.h, which might have
 * additional definitions provided for Windows.
 * For more details see http://msdn.microsoft.com/en-us/library/y0ybw9fy.aspx
 *
 * Also fall back on Darwin and AIX to allow additional definitions and
 * implementation-defined values.
 */
#if (defined(__APPLE__) || defined(__MINGW32__) || defined(_MSC_VER) ||        \
     defined(_AIX)) &&                                                         \
    __STDC_HOSTED__ && __has_include_next(<float.h>)

/* Prior to Apple's 10.7 SDK, float.h SDK header used to apply an extra level
 * of #include_next<float.h> to keep Metrowerks compilers happy. Avoid this
 * extra indirection.
 */
#ifdef __APPLE__
#define _FLOAT_H_
#endif

#  include_next <float.h>

The last line is line 32, corresponding to the first line of your error message.
On my mingw installation, in /usr/x86_64-w64-mingw32/usr/include/float.h, I find around line 28:

#if !defined(_FLOAT_H___) && !defined(__FLOAT_H) && !defined(__CLANG_FLOAT_H)
#include_next <float.h>
#endif

Note how the check for !defined(__CLANG_FLOAT_H) should avoid invoking #include_next, because Clang's header above already defined the include guard __CLANG_FLOAT_H. Something must be different on your system. I'm guessing the MinGW version.

Edit: I'm using MinGW-11.0.0.

[hanxiatu-github]

@hanxiatu-github This is strange. When I look into Clang's <float.h> (which is bundled and put into your temp-dir as esbmc-headers-92ea-c0c0-cf95/float.h), the corresponding excerpt is this:

#ifndef __CLANG_FLOAT_H
#define __CLANG_FLOAT_H

/* If we're on MinGW, fall back to the system's float.h, which might have
 * additional definitions provided for Windows.
 * For more details see http://msdn.microsoft.com/en-us/library/y0ybw9fy.aspx
 *
 * Also fall back on Darwin and AIX to allow additional definitions and
 * implementation-defined values.
 */
#if (defined(__APPLE__) || defined(__MINGW32__) || defined(_MSC_VER) ||        \
     defined(_AIX)) &&                                                         \
    __STDC_HOSTED__ && __has_include_next(<float.h>)

/* Prior to Apple's 10.7 SDK, float.h SDK header used to apply an extra level
 * of #include_next<float.h> to keep Metrowerks compilers happy. Avoid this
 * extra indirection.
 */
#ifdef __APPLE__
#define _FLOAT_H_
#endif

#  include_next <float.h>

The last line is line 32, corresponding to the first line of your error message. On my mingw installation, in /usr/x86_64-w64-mingw32/usr/include/float.h, I find around line 28:

#if !defined(_FLOAT_H___) && !defined(__FLOAT_H) && !defined(__CLANG_FLOAT_H)
#include_next <float.h>
#endif

Note how the check for !defined(__CLANG_FLOAT_H) should avoid invoking #include_next, because Clang's header above already defined the include guard __CLANG_FLOAT_H. Something must be different on your system. I'm guessing the MinGW version.

Edit: I'm using MinGW-11.0.0.

yes，my version is：

#if !defined(_FLOAT_H___) && !defined(__FLOAT_H)
#include_next <float.h>
#endif

after change to

#if !defined(_FLOAT_H___) && !defined(__FLOAT_H) && !defined(__CLANG_FLOAT_H)
#include_next <float.h>
#endif

the problem is solved