Sireum Kekinian is the most recent evolution of the Sireum platform whose core components are being built using the Sireum programming language -- Slang.
Slang is an OO/FP programming language with contract and proof languages designed for formal verification and analyses; that is, it serves as the basis for the next generation Logika verifier and proof checker, as well as for other formal method-based analysis techniques. It is currently a subset of Scala 2.x with different memory models enabled via Scala's macro and compiler plugin facilities, with support for IntelliJ.
With the exception of a small part of its runtime library and its parser that uses scalameta, the runtime library and the Slang codebase itself (and analyses on top of it) are written using Slang.
Slang programs run on the JVM (Java 8+), in the browser or Node.js
(via Scala.js Javascript translation), and natively
via Graal and also via compilation to C.
The generated C code is both Slang source-traceable and
in the form that is structurally close to the Slang source;
in addition to gcc
and clang
, it can also be compiled using the
CompCert Verified C Compiler
to provide a high-assurance toolchain for program correctness down to machine code.
Sireum is available as pre-built binaries/installers or from source. The main advantage of using the source distribution is that updates can be done incrementally while the binary distribution requires complete re-installation. On the other hand, source distribution requires more setup.
Sireum binary distribution files are 7z self-extracting archives (SFX) with command-line installers to (optionally) configure where Sireum should be installed.
Below are the installation instructions for 64-bit (amd64) macOS, Linux, and
Windows (or, one can simply download the distribution files from the
GitHub releases page
and extract them using a program capable of uncompressing 7z
archive).
-
macOS: run the following command in a terminal:
(sd=sireum-dev-mac.sfx && curl -JLo $sd -c /dev/null http://mac.distro.sireum.org && chmod +x $sd && p=$(pwd) && cd /tmp && $p/$sd)
-
Linux: download and run sireum-dev-linux.sfx, or run the following command in a terminal if you have
curl
installed:(sd=sireum-dev-linux.sfx && curl -JLo $sd -c /dev/null http://linux.distro.sireum.org && chmod +x $sd && p=$(pwd) && cd /tmp && $p/$sd)
-
Windows: download and run sireum-dev-win.exe
If you want to ensure that the downloaded files are genuine, download the appropriate Minisign signature files for the specific platforms for macOS, Linux, and Windows, then run:
minisign -P RWShRZe/1tMRHAcQ2162Wq5FhU2ptktJdQxzUxvK0MwVjDYRC4JY87Fb -Vm <installer-file>
Alternatively, you can also use a port of OpenBSD's signify for your
operating system (e.g., signify-openbsd
in Ubuntu) instead of minisign
as follows:
signify-openbsd -V -p sireum.pub -x <installer-file>.minisig -m <installer-file>
where sireum.pub
's content is:
untrusted comment: Sireum
RWShRZe/1tMRHAcQ2162Wq5FhU2ptktJdQxzUxvK0MwVjDYRC4JY87Fb
-
macOS: none
-
Linux:
curl
andgit
-
Windows: Developer Mode enabled and
git
(Git For Windows, MSYS2, or Cygwin)
In a console terminal:
-
macOs/Linux:
git clone --recursive https://github.com/sireum/kekinian kekinian/bin/build.cmd setup # for non-POSIX shell, prefix with sh
-
Windows:
git clone --recursive https://github.com/sireum/kekinian kekinian\bin\build.cmd setup
Set the SIREUM_HOME
env var to the kekinian
path above.
To update later on, simply do a git pull --recurse-submodules
and re-run
build.cmd setup
(or simply build.cmd
to rebuild Sireum CLI tools).
If rebuilding Sireum somehow failed, try cleaning the repo:
-
macOS/Linux:
${SIREUM_HOME}/bin/clean.sh
-
Windows:
%SIREUM_HOME%\bin\clean.bat
and re-run build.cmd setup
.
To generate a "hello world" Slang script project in the current directory and launch Sireum IVE:
-
macOS:
# Generates ./hello project directory with ./hello/src/script.sc ${SIREUM_HOME}/bin/sireum tools ivegen . open ${SIREUM_HOME}/bin/mac/idea/IVE.app
-
Linux:
# Generates ./hello project directory with ./hello/src/script.sc ${SIREUM_HOME}/bin/sireum tools ivegen . ${SIREUM_HOME}/bin/linux/idea/bin/IVE.sh
-
Windows:
REM Generates .\hello project directory with .\hello\src\script.sc %SIREUM_HOME%\bin\sireum.bat tools ivegen . cmd /C %SIREUM_HOME%\bin\win\idea\bin\IVE.exe
Once Sireum IVE is running, open the hello
directory as a project,
then open the script.sc
file for editing.
(When asked to add Ammonite
dependencies, choose Ignore
for now; you can add
the dependencies but it might take a while to download the packages.)
To run the script, click on the green ► button at the top-left part of the editor (or click on the green ► button on the right side of "Run script.sc" at the top-right part of the window).
If you would like to learn Slang quickly, you can read and use the IVE to experiment with several examples designed to highlight various Slang language features:
https://github.com/sireum/slang-by-examples
Slang App Example Mill Project
To generate a "hello world" Slang app project in the current directory and launch Sireum IVE:
-
macOS:
# Generates ./hello-app project directory with ./hello-app/hello-app/src/app.scala ${SIREUM_HOME}/bin/sireum tools ivegen -m mill -n hello-app .
-
Linux:
# Generates ./hello-app project directory with ./hello-app/hello-app/src/app.scala ${SIREUM_HOME}/bin/sireum tools ivegen -m mill -n hello-app .
-
Windows:
REM Generates .\hello-app project directory with .\hello-app\hello-app\src\app.scala %SIREUM_HOME%\bin\sireum.bat tools ivegen -m mill -n hello-app .
Open the hello-app
directory as a project in Sireum IVE, open the app.scala
file for editing. To run it, click on the green ► button near the definition of
object app
in the editor.
Note that mill
(or mill.bat
under Windows) is available under the bin
directory of SIREUM_HOME
.
Sireum is best developed (browsed/edited) by using Sireum IVE itself.
The build.cmd setup
command above setup IVE for Sireum development.
If you want to re-run just the IVE project re-generation, do the following in
a terminal:
-
macOS/Linux:
${SIREUM_HOME}/bin/build.cmd project
-
Windows:
%SIREUM_HOME%\bin\build.cmd project
Then open the SIREUM_HOME
directory as a project in Sireum IVE.
To have the codebase and its test suites recompiled upon changes, run:
-
macOS/Linux:
cd ${SIREUM_HOME} && bin/mill -w cli.tests.compile
and to build its assembly/CLI tool:
${SIREUM_HOME}/bin/build.cmd
-
Windows:
cd %SIREUM_HOME% && bin\mill.bat -w cli.tests.compile
and to build its assembly/CLI tool:
%SIREUM_HOME%\bin\build.cmd
It is recommended to compile Sireum and its Slash build scripts to native as it speeds up build tasks.
First, install GraalVM native-image
's prerequisites
(note: native-image
for Windows requires Visual Studio 2017 or 2019);
then, to build Sireum native executable:
-
macOS/Linux:
${SIREUM_HOME}/bin/build.cmd native
-
Windows:
-
Visual Studio 2017 Community
call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Community\VC\Auxiliary\Build\vcvars64.bat" %SIREUM_HOME%\bin\build.cmd native
-
Visual Studio 2019 Community
call "C:\Program Files (x86)\Microsoft Visual Studio\2019\Community\VC\Auxiliary\Build\vcvars64.bat" %SIREUM_HOME%\bin\build.cmd native
-
To run:
-
macOS:
${SIREUM_HOME}/bin/mac/sireum
-
Linux:
${SIREUM_HOME}/bin/linux/sireum
-
Windows:
%SIREUM_HOME%\bin\win\sireum.exe
Note that once the native version is available (and has a newer timestamp),
sireum
and sireum.bat
in bin
call the native version.
This is also similar for build.cmd
in bin
and bin/mill-build/bin
.