How can I use polyspace-configure on builds performed by the Bazel build system?

I would like to use polyspace-configure to create a Polyspace project for a project configured with the Bazel build system.
When I run the command that works for other build systems, I get different errors like:polyspace-configure does not find any source filewarnings related to unsupported gcc options

Answer 1

[MathWorks Support Team]

There are 3 main points to consider about the Bazel build environment that interfere with how polyspace-configure works.

1) Bazel is a client/server build system.

The bazel client command connects to a daemon and waits for the latter to perform the build.  The daemon caches previous build results.  When the daemon is already started (the nominal case) polyspace-configure sniffs only the client and comes back empty-handed.

• Symptoms in the polyspace-configure log:
  • polyspace-configure reports that no compilation units were found.
• Solution:
  • Stop the server to force the client command to start it again.  In this case, the daemon is a child process of the client command and is sniffed by polyspace-configure alongside all compilation processes.
  • Run the following command in the directory containing the WORKSPACE file before polyspace-configure to force a full build and kill the daemon:

                        bazel clean –-expunge

2) Bazel dynamically probes gcc for supported options

Bazel calls gcc on a dummy empty.cc file with various options (e.g. "-fcolorized-diagnostics") to check which ones are supported.  This confuses polyspace-configure that thinks empty.cc is a genuine source file and that the options probed are valid.

• Symptoms in the polyspace-configure log:
  • Warning and error when polyspace-configure reinvokes gcc with unsupported options.
  • Warning because empty.cc was detected several times
• Solution:
  • Pass "-exclude-sources empty.cc" to polyspace-configure

3) Bazel calls compilers in a sandbox environment by default

Bazel copies source files in a temporary directory, turns it into a sandbox, and deletes this directory when the build completes.

• Symptoms in the polyspace-configure log:
  • polyspace-configure does not find any source file (besides the aforementioned empty.cc) because the sandbox directories are gone.
  • There is no diagnostic by default but enabling -debug shows the issue.
• Solution:
  • Pass "–-spawn_strategy standalone" to Bazel to disable sandboxes.

 

Tutorial showing the procedure to sniff a Bazel build:

This tutorial was validated on Debian 11 with Bazel 8.0.1

1. Install Bazel on Linux.
2. Download or clone the Bazel C++ tutorial repository from https://github.com/bazelbuild/examples.
3. Enter the correct directory: cd examples/cpp-tutorial/stage1
4. Clean the build files and stop the Bazel server: bazel clean --expunge
5. Run polyspace-configure: polyspace-configure -exclude-sources empty.cc bazel build –-spawn_strategy standalone //main:hello-world
6. Repeat previous steps for stage2 and stage3

Additional notes:

• Bazel emits a “ignoring LD_PRELOAD in the environment” warning but polyspace-configure can work around this.
• Make sure to use a local daemon rather than a remote one.