sireum / kekinian

Sireum: A High Assurance System Engineering Platform

Sireum: A High Assurance System Engineering Platform

Sireum Kekinian is the most recent evolution of the Sireum platform. For more information, please visit Sireum's website:

https://sireum.org (Download/Getting Started)

Dependencies

Sireum depends on open source software libraries and applications (the specific versions are listed in versions.properties).

Library Dependencies

Library	Maven	License
ANTLR3 Runtime	(link)	BSD3
ANTLR4 Runtime	(link)	BSD3
Apache Common Compress	(link)	Apache 2.0
ASM	(link)	BSD3
Automaton	(link)	BSD3
GitHub API	(link)	MIT
NuProcess	(link)	Apache 2.0
OS-Lib	(link)	MIT
JavaFX for Presentasi	(link)	BSD2
Scala	(link)	Apache 2.0
Scalafmt	(link)	Apache 2.0
Scalameta	(link)	BSD3
ScalaTest	(link)	Apache 2.0
Scala Java 8 Compatibility Kit	(link)	Apache 2.0
Scala Parallel Collection	(link)	Apache 2.0
Scala.js	(link)	Apache 2.0
Scala.js: DOM	(link)	MIT
Scala.js: Scalatags	(link)	MIT
SMT-LIB Parser	(link)	MIT
SysML v2 Parser for HAMR	(link)	LGPL3

In addition, Sireum includes adaptations of the following artifacts:

Source	Adaptation	License
ANTLRv3.g	SireumAntlr3.g	BSD3
diff_match_patch.java	DiffMatchPatch	Apache 2.0
Geny	Jen & MJen	MIT
JetBrains Mono & FiraCode	Sireum Mono	OFL & OFL
SHA3IUF	SHA3	MIT
UnsafeUtils	UnsafeUtils	MIT

Application Dependencies

Application	License
Liberica JDK (Full)	GPL v2 with "Classpath" exception
CVC4/5	BSD3
Coursier	Apache 2.0
JaCoCo	EPL 2.0
Z3	MIT

Sireum stores small, pre-built binary executables in its submodule repositories for macOS, Linux, and Windows (please see the respective repository for virus analysis results).

Pre-built Executable	License
7z	LGPL v2, BSD3, unRAR restriction

Optional Applications

Application	License
checkstack.pl	GPL v2
pts-tiny-7z-sfx	GPL v2
ACL2	BSD3
Alt-Ergo	OCamlPro-Non-Commercial-License
Brave Browser	MPL 2.0
CompCert	INRIA Non-Commercial License Agreement
Coq	LGPL 2.1
CLion	Commercial
FM Workbench	BSD3
GraalVM (OpenJDK)	GPL v2 with "Classpath" exception
IntelliJ	Apache 2.0
Isabelle	BSD3
Mill	MIT
Oracle GraalVM	GFTC
OSATE2	EPL 2.0
Rust	MIT
RustRover	Non-Commercial
VSCodium	MIT

IntelliJ/CLion/RustRover Plugin	License
ANTLR4	BSD3
ASM	Apache 2.0
GitLab	JetBrains User Agreement (Free)
JDT AstView	BSD2
Native Debugging Support	Commercial (Ultimate only)
PDF Viewer	MIT
PlantUML Integration	Apache 2.0
Rust	Ultimate/Commercial/Non-Commercial
Scala	Apache 2.0
Sireum	BSD2
Slang Injector	BSD2
Terminal	Apache 2.0
TeXiFy IDEA	MIT
Toml	MIT

VSCodium Extension	License
clangd	MIT
markdownlint	MIT
ANTLR4 grammar syntax support	MIT
Bash IDE	MIT
ESLint	MIT
Git Graph	MIT w/ non-derivative work restrictions
HTML CSS	MIT
Hugo Utilities	MIT
Java	EPL 2.0
Jest	MIT
Langium	MIT
LaTeX Workshop	MIT
PlantUML	MIT
Prettier - Code Formatter	MIT
Python	MIT
Rust Analyzer	MIT & Apache 2.0
Scala Metals	Apache 2.0
SysIDE CE	EPL 2.0
VerilogHDL/SystemVerilog/Bluespec SystemVerilog	MIT
XML	EPL 2.0
YAML	MIT
Zip Tools	MIT

kekinian's Issues

HAMR does not build for ARM64 target

Hello @jasonbelt !

We are attempting to build a ARM64 docker image with FMIDE + HAMR, because a lot of folks at Galois are not using M1/M2 Macs.

Sireum installs just fine for ARM64, but when I attempt to run:

RUN ${SIREUM_HOME}/bin/install/fmide.cmd --verbose

I get the following error:

11 [ 7/10] RUN /opt/Sireum/bin/install/fmide.cmd --verbose
#11 3.526 FMIDE is based on OSATE v2.10.x however ARM architectures require OSATE 2.11+. Sireum Phantom can be used
#11 3.526 to install the Sireum OSATE plugins into a more recent version of OSATE. For more information invoke
#11 3.526 

What would it take to upgrade HAMR to work with OSATE 2.11+ (ideally OSATE 2.12)?

[bug] Installing HAMR in Docker seems to stall

When following the installation instructions from here and attempting to install FMIDE in a Ubuntu:22.04 docker container, the install seems to stall at bin/install/fmide.cmd:

Sireum-dev IVE can now be launched by running /opt/Sireum/bin/linux/idea/bin/IVE.sh
Java Development Kit (JDK) is available at /opt/Sireum/bin/linux/java
Scala is available at /opt/Sireum/bin/scala
Removing intermediate container f61440012bb1
 ---> 2a039dee7028
Step 9/9 : RUN bin/install/fmide.cmd
 ---> Running in 5a6663e40370
Installing FMIDE (this will take a while) ...
# seems to hang up - no CPU activity, no updates for > 30min

Is it possible to install HAMR in a docker container, or is it not a supported/recommended way?