This repository shows you how to build and customize a Docker image for Polyspace Bug Finder™ Server™ and Polyspace Code Prover™ Server™, using the MATLAB® Package Manager (mpm).
You can use this image as a scalable and reproducible method to run Polyspace analyses in containers.
- A valid Polyspace Bug Finder or Code Prover Server license
- The port and host name of a Network License Manager or the path of a
network.lic
license file. See Use Network License Manager. - Linux® Operating System
- Docker
- Git
Use these commands to clone this repository and build the Docker image:
# Clone this repository to your machine.
git clone https://github.com/mathworks-ref-arch/polyspace-bug-finder-server-dockerfile.git
# Navigate to the downloaded folder.
cd polyspace-bug-finder-server-dockerfile
# Select a base image for the container you want to build, for example, Ubuntu, and copy it to a Dockerfile.
cp Dockerfile.ubuntu22.04 Dockerfile
# Build container with a name and tag of your choice.
docker build . -t polyspace-bug-finder-server:r2024b
The build
command looks for the Dockerfile
in the current directory and builds an image with the name and tag specified by the -t
option.
If you list the docker images and filter for polyspace*
after the docker build
command completes, you see the polyspace-bug-finder-server image.
$ docker images -f=reference=polyspace*
REPOSITORY TAG IMAGE ID CREATED SIZE
polyspace-bug-finder-server r2024b a7c749b717c1 About a minute ago 4.56GB
After you build the image, create a file to analyze and a folder where you store the analysis results.
# Create a source and results folder and make them accessible from the running container
mkdir -p src ps_results
chmod 777 src ps_results
# Create a test file to analyze
echo 'int main(){int a; return a;}'> src/simple_niv.c
The following docker run
command:
- Creates and runs a container from the image that you built in the previous section.
- Sets the environment variable
MLM_LICENSE_FILE
, which enables the container to communicate with the license manager.
Specify this variable asportNumber@hostname
. The variable is mandatory unless you provide the license server information when you build the container.
See Specify License Server Information in Build Image. - Maps the current folder to the
/work
folder inside the container. - Runs the analysis command (
polyspace-bug-finder -sources...
) from the docker container on the test file you created.
# Run the container to analyze the test file.
docker run --rm \
-e MLM_LICENSE_FILE=27000@MyServerName.example.com \
-v "$(pwd):/work" polyspace-bug-finder-server:r2024b \
polyspace-bug-finder-server -sources /work/src/simple_niv.c -results-dir /work/ps_results
Docker automatically cleans up the container and removes its file system when the container exits (--rm
option).
The Dockerfile supports these Docker build-time variables.
Argument Name | Default value | Description |
---|---|---|
MATLAB_RELEASE | r2024b | The Polyspace Server release you want to install. Must be lower-case, for example: r2022b . |
LICENSE_SERVER | unset | The port and hostname of the machine that is running the Network License Manager, using the port@hostname syntax. For example: 27000@MyServerName . |
To customize the docker image, use these arguments with the docker build
command or edit the default values of these arguments directly in the Dockerfile.
if you include the license manager information when you run the docker build
command, you do not have to specify the MLM_LICENSE_FILE
variable when you run the container using the docker run
command.
# Build container and specify LICENSE_SERVER variable
docker build -t polyspace-bug-finder-server:r2024b --build-arg LICENSE_SERVER=27000@MyServerName.example.com .
# Run the container without specifying the MLM_LICENSE_FILE variable
docker run --rm \
-v "$(pwd):/work" polyspace-bug-finder-server:r2024b \
polyspace-bug-finder-server -sources /work/src/simple_niv.c -results-dir /work/ps_results
Note: If you specify the value of the LICENSE_SERVER variable in the Dockerfile, you can omit it when running the
docker build
command.
The Polyspace Bug Finder Server and Polyspace Code Prover Server products use a concurrent license which requires a Network License Manager to manage license checkouts.
To enable the container to communicate with the license manager, you must provide the port and hostname of the machine where you installed the license manager or the path to the network.lic
file.
Contact your license administrator to obtain the address of your license server, for instance:
27000@MyServerName.example.com
, or the path to the network.lic
file.
You can also get the license manager port and hostname from the SERVER
line of the network.lic
file or the license.dat
file.
# Sample network.lic
SERVER MyServerName.example.com <optional-mac-address> 27000
USE_SERVER
# Snippet from sample license.dat
SERVER MyServerName.example.com <mac-address> 27000
...
To pass the license manager address (portNumber@hostname
) to the:
docker build
command, assign the address to the LICENSE_SERVER build variable.docker run
command, assign the address to the MLM_LICENSE_FILE environment variable.
To use the network.lic
file instead:
-
Copy the file to the same folder as the
Dockerfile
. -
Uncomment the line
COPY network.lic /opt/matlab/licenses/
in the Dockerfile.You do not need to specify the
LICENSE_SERVER
build variable when running thedocker build
command:# Example docker build -t polyspace-bug-finder-server:r2024b .
While docker cleans up containers on exit, the docker image persists in your file system until you explicitely delete it. To delete a docker image, run the docker image rm
command and specify the name of the container. For instance:
docker image rm polyspace-bug-finder-server:r2024b
- Explore prebuilt MATLAB Docker Containers on Docker Hub:
- MATLAB Containers on Docker Hub hosts container images for multiple MATLAB releases.
- MATLAB Deep Learning Container Docker Hub repository hosts container images with toolboxes suitable for deep learning.
If you encounter a technical issue or have an enhancement request after trying this repository with your environment, create an issue here.
Copyright (c) 2022-2024 The MathWorks, Inc. All rights reserved.