Commit 3dd47a73 authored by Heiko Becker's avatar Heiko Becker

Merge with upstream daisy

parent 282f5ff0
......@@ -47,3 +47,5 @@ rawdata/*
.ensime*
last.log
output/*
!output/README
/doc/
image: localhost:5000/daisy
variables:
SBT_OPTS: "-Dsbt.global.base=sbt-cache/.sbtboot -Dsbt.boot.directory=sbt-cache/.boot -Dsbt.ivy.home=sbt-cache/.ivy"
SBT_CACHE_DIR: "sbt-cache/.ivy/cache"
cache:
paths:
- sbt-cache
stages:
- compile
- test
compile:
stage: compile
script: sbt clean compile
artifacts:
expire_in: 1h
paths:
- target/
- project/
unit:
stage: test
dependencies:
- compile
script: sbt "testOnly unit.*"
regression:
stage: test
dependencies:
- compile
script: sbt "testOnly regression.*"
FROM openjdk:8u141-jdk
RUN touch /usr/lib/jvm/java-8-openjdk-amd64/release
ENV SBT_VERSION 0.13.15
WORKDIR /root
# Install sbt
RUN \
curl -L -o sbt-$SBT_VERSION.deb https://dl.bintray.com/sbt/debian/sbt-$SBT_VERSION.deb && \
dpkg -i sbt-$SBT_VERSION.deb && \
rm sbt-$SBT_VERSION.deb && \
apt-get update && \
apt-get install sbt && \
sbt sbtVersion
# Install mpfr
RUN apt-get install libmpfr4
# Install Z3
RUN apt-get install libgomp1 z3
# Install dReal
RUN \
curl -fsL https://github.com/dreal/dreal3/releases/download/v3.16.09.01/dReal-3.16.09.01-linux.tar.gz | tar xz && \
ln -s ~/dReal-3.16.09.01-linux/bin/dReal /usr/bin/dReal
# Project Daisy
Daisy now also has an online interface: http://daisy.mpi-sws.org/.
It's a brand new feature, so please be patient while we work out all the kinks.
## First steps
......@@ -49,10 +52,16 @@ To see all command-line options:
```
If you don't want to run in interactive mode, you can also call all of the above
commands simply with 'sbt' prefixed, e.g. $ sbt compile.
commands simply with 'sbt' prefixed, e.g.
```
$ sbt compile
```
You can also run Daisy outside of sbt. For this use '$ sbt script' which will
generate a script called 'daisy' which includes all the necessary files (and then some).
You can also run Daisy outside of sbt. For this use
```
$ sbt script
```
which will generate a script called 'daisy' which includes all the necessary files.
You can then run Daisy on an input file as follows:
```bash
$ ./daisy testcases/rosa/Doppler.scala
......@@ -142,23 +151,31 @@ $ ./cake_checker < CERTIFICATE_FILE
Some features of Daisy require additional software to be installed.
Currently, this is
* Z3: if you want to compute ranges with the help of the SMT solver Z3, you need to
[install it first on your machine](https://github.com/Z3Prover/z3).
* An SMT solver which can be used to improve ranges: [Z3](https://github.com/Z3Prover/z3) \[[Linux](https://github.com/Z3Prover/z3/releases)\] \[[Mac](https://github.com/Z3Prover/z3/releases)\] and/or [dReal](https://github.com/dreal/dreal3) \[[Linux](https://github.com/dreal/dreal3/releases)\]
* [MPFR](http://www.mpfr.org/) for error under-approximation and transcendental calculations: \[`apt-get install libmpfr4`\] \[`brew install mpfr`\]
* MPFR: Daisy uses a [Java binding](https://github.com/kframework/mpfr-java).
(TODO: figure out whether we used the static or dynamic binding)
## Contributors
In no particular order: Saksham Sharma, Einar Horn, Debasmita Lohar, Heiko Becker, Ezequiel Postan,
Fabian Ritter, Anastasiia Izycheva, Raphael Monat, Fariha Nasir, and Robert Bastian.
* Coq: Version 8.5pl2 if you want to extract certificates for it, [install it](https://coq.inria.fr/download)
## Documentation
To come.
## Intellij Idea Setup
To run Daisy in Intellij Idea you first have to install Scala Plugin: Settings (Ctrl + Alt + S) -> Plugins. Choose Scala in the list and press "Install JetBrains Plugin ...". Then let Idea know where is your Scala (or make sure Scala SDK is already there): Project Structure -> Global Libraries -> New Global Library -> Scala SDK -> select the source folder for the SDk on your machine.
To run Daisy in Intellij Idea you first have to install the Scala Plugin: Settings (Ctrl + Alt + S) -> Plugins.
Choose Scala in the list and select "Install JetBrains Plugin ...".
Then let Idea know where is your Scala (or make sure Scala SDK is already there): Project Structure -> Global Libraries -> New Global Library -> Scala SDK -> select the source folder for the SDK on your machine.
Also make sure the Java SDK is set up for Idea (Project Structure -> SDKs -> check that your JDK is here or add it here).
Choose File -> New -> Project from Existing Source -> choose the path to the build.sbt file
Choose File -> New -> Project from Existing Source -> path-to-the-build.sbt-file
or
File -> New -> Project from Version Control -> Git -> put git-rts@gitlab.mpi-sws.org:AVA/daisy.git into the URL field and select the destination folder for source files to be copied.
File -> New -> Project from Version Control -> Git -> and put git-rts@gitlab.mpi-sws.org:AVA/daisy.git into the URL field and
select the destination folder for source files to be copied.
After the setup run Daisy in the Terminal of Intellij Idea using sbt as described above.
......
......@@ -4,20 +4,26 @@ version := "0.0"
organization := "org.mpi-sws.ava"
scalaVersion in ThisBuild := "2.11.6"
//enablePlugins(ScalaNativePlugin)
scalaVersion := "2.11.11"
scalacOptions ++= Seq(
"-deprecation",
"-unchecked",
"-feature")
"-feature",
"-Ywarn-unused-import",
"-Ywarn-unused",
"-Ywarn-dead-code",
"-Xlint:_,-adapted-args")
resolvers += "Typesafe Repository" at "http://repo.typesafe.com/typesafe/releases/"
resolvers += "Sonatype OSS Snapshots" at "https://oss.sonatype.org/content/repositories/snapshots"
libraryDependencies ++= Seq(
"org.scala-lang" % "scala-compiler" % "2.11.6",
"org.scala-lang" % "scala-compiler" % "2.11.11",
"org.scalatest" % "scalatest_2.11" % "2.2.4" % "test",
"com.storm-enroute" %% "scalameter" % "0.7",
"com.regblanc" % "scala-smtlib_2.11" % "0.2",
"org.fusesource.hawtjni" % "hawtjni-runtime" % "1.9" //for JNI
)
......@@ -38,6 +44,9 @@ lazy val Benchmark = config("bench") extend Test
testOptions in Test += Tests.Argument(scalaMeterFramework, "-silent")
ivyLoggingLevel in clean := UpdateLogging.Quiet
ivyLoggingLevel in Test := UpdateLogging.Quiet
parallelExecution in Test := false
logBuffered := false
......
@import url("basic.css");
/* -- page layout ----------------------------------------------------------- */
body {
font-family: 'goudy old style', 'minion pro', 'bell mt', Georgia, 'Hiragino Mincho Pro', serif;
font-size: 17px;
background-color: white;
color: #000;
margin: 0;
padding: 0;
}
div.document {
width: 940px;
margin: 30px auto 0 auto;
}
div.documentwrapper {
float: left;
width: 100%;
}
div.bodywrapper {
margin: 0 0 0 220px;
}
div.sphinxsidebar {
width: 220px;
}
hr {
border: 1px solid #B1B4B6;
}
div.body {
background-color: #ffffff;
color: #3E4349;
padding: 0 30px 0 30px;
}
div.footer {
width: 940px;
margin: 20px auto 30px auto;
font-size: 14px;
color: #888;
text-align: right;
}
div.footer a {
color: #888;
}
div.relations {
display: none;
}
div.sphinxsidebar a {
color: #444;
text-decoration: none;
border-bottom: 1px dotted #999;
}
div.sphinxsidebar a:hover {
border-bottom: 1px solid #999;
}
div.sphinxsidebar {
font-size: 14px;
line-height: 1.5;
}
div.sphinxsidebarwrapper {
padding: 18px 10px;
}
div.sphinxsidebarwrapper p.logo {
padding: 0;
margin: -10px 0 0 0px;
text-align: center;
}
div.sphinxsidebarwrapper h1.logo {
margin-top: -10px;
text-align: center;
margin-bottom: 5px;
text-align: left;
}
div.sphinxsidebarwrapper h1.logo-name {
margin-top: 0px;
}
div.sphinxsidebarwrapper p.blurb {
margin-top: 0;
font-style: normal;
}
div.sphinxsidebar h3,
div.sphinxsidebar h4 {
font-family: 'Garamond', 'Georgia', serif;
color: #444;
font-size: 24px;
font-weight: normal;
margin: 0 0 5px 0;
padding: 0;
}
div.sphinxsidebar h4 {
font-size: 20px;
}
div.sphinxsidebar h3 a {
color: #444;
}
div.sphinxsidebar p.logo a,
div.sphinxsidebar h3 a,
div.sphinxsidebar p.logo a:hover,
div.sphinxsidebar h3 a:hover {
border: none;
}
div.sphinxsidebar p {
color: #555;
margin: 10px 0;
}
div.sphinxsidebar ul {
margin: 10px 0;
padding: 0;
color: #000;
}
div.sphinxsidebar ul li.toctree-l1 > a {
font-size: 120%;
}
div.sphinxsidebar ul li.toctree-l2 > a {
font-size: 110%;
}
div.sphinxsidebar input {
border: 1px solid #CCC;
font-family: 'goudy old style', 'minion pro', 'bell mt', Georgia, 'Hiragino Mincho Pro', serif;
font-size: 1em;
}
div.sphinxsidebar hr {
border: none;
height: 1px;
color: #999;
background: #999;
text-align: left;
margin-left: 0;
width: 50%;
}
/* -- body styles ----------------------------------------------------------- */
a {
color: #004B6B;
text-decoration: underline;
}
a:hover {
color: #6D4100;
text-decoration: underline;
}
div.body h1,
div.body h2,
div.body h3,
div.body h4,
div.body h5,
div.body h6 {
font-family: 'Garamond', 'Georgia', serif;
font-weight: normal;
margin: 30px 0px 10px 0px;
padding: 0;
}
div.body h1 { margin-top: 0; padding-top: 0; font-size: 240%; }
div.body h2 { font-size: 180%; }
div.body h3 { font-size: 150%; }
div.body h4 { font-size: 130%; }
div.body h5 { font-size: 100%; }
div.body h6 { font-size: 100%; }
a.headerlink {
color: #DDD;
padding: 0 4px;
text-decoration: none;
}
a.headerlink:hover {
color: #444;
background: #EAEAEA;
}
div.body p, div.body dd, div.body li {
line-height: 1.4em;
}
div.admonition {
margin: 20px 0px;
padding: 10px 30px;
background-color: #FCC;
border: 1px solid #FAA;
}
div.admonition tt.xref, div.admonition a tt {
border-bottom: 1px solid #fafafa;
}
dd div.admonition {
margin-left: -60px;
padding-left: 60px;
}
div.admonition p.admonition-title {
font-family: 'Garamond', 'Georgia', serif;
font-weight: normal;
font-size: 24px;
margin: 0 0 10px 0;
padding: 0;
line-height: 1;
}
div.admonition p.last {
margin-bottom: 0;
}
div.highlight {
background-color: white;
}
dt:target, .highlight {
background: #FAF3E8;
}
div.note {
background-color: #EEE;
border: 1px solid #CCC;
}
div.seealso {
background-color: #EEE;
border: 1px solid #CCC;
}
div.topic {
background-color: #eee;
}
p.admonition-title {
display: inline;
}
p.admonition-title:after {
content: ":";
}
pre, tt, code {
font-family: 'Consolas', 'Menlo', 'Deja Vu Sans Mono', 'Bitstream Vera Sans Mono', monospace;
font-size: 0.9em;
}
.hll {
background-color: #FFC;
margin: 0 -12px;
padding: 0 12px;
display: block;
}
img.screenshot {
}
tt.descname, tt.descclassname, code.descname, code.descclassname {
font-size: 0.95em;
}
tt.descname, code.descname {
padding-right: 0.08em;
}
img.screenshot {
-moz-box-shadow: 2px 2px 4px #eee;
-webkit-box-shadow: 2px 2px 4px #eee;
box-shadow: 2px 2px 4px #eee;
}
table.docutils {
border: 1px solid #888;
-moz-box-shadow: 2px 2px 4px #eee;
-webkit-box-shadow: 2px 2px 4px #eee;
box-shadow: 2px 2px 4px #eee;
}
table.docutils td, table.docutils th {
border: 1px solid #888;
padding: 0.25em 0.7em;
}
table.field-list, table.footnote {
border: none;
-moz-box-shadow: none;
-webkit-box-shadow: none;
box-shadow: none;
}
table.footnote {
margin: 15px 0;
width: 100%;
border: 1px solid #EEE;
background: #FDFDFD;
font-size: 0.9em;
}
table.footnote + table.footnote {
margin-top: -15px;
border-top: none;
}
table.field-list th {
padding: 0 0.8em 0 0;
}
table.field-list td {
padding: 0;
}
table.footnote td.label {
width: 0px;
padding: 0.3em 0 0.3em 0.5em;
}
table.footnote td {
padding: 0.3em 0.5em;
}
dl {
margin: 0;
padding: 0;
}
dl dd {
margin-left: 30px;
}
blockquote {
margin: 0 0 0 30px;
padding: 0;
}
ul, ol {
margin: 10px 0 10px 30px;
padding: 0;
}
pre {
background: #EEE;
padding: 7px 30px;
margin: 15px 0px;
line-height: 1.3em;
}
dl pre, blockquote pre, li pre {
margin-left: 0;
padding-left: 30px;
}
dl dl pre {
margin-left: -90px;
padding-left: 90px;
}
tt, code {
background-color: #ecf0f3;
color: #222;
/* padding: 1px 2px; */
}
tt.xref, code.xref, a tt {
background-color: #FBFBFB;
border-bottom: 1px solid white;
}
a.reference {
text-decoration: none;
border-bottom: 1px dotted #004B6B;
}
a.reference:hover {
border-bottom: 1px solid #6D4100;
}
a.footnote-reference {
text-decoration: none;
font-size: 0.7em;
vertical-align: top;
border-bottom: 1px dotted #004B6B;
}
a.footnote-reference:hover {
border-bottom: 1px solid #6D4100;
}
a:hover tt, a:hover code {
background: #EEE;
}
@media screen and (max-width: 870px) {
div.sphinxsidebar {
display: none;
}
div.document {
width: 100%;
}
div.documentwrapper {
margin-left: 0;
margin-top: 0;
margin-right: 0;
margin-bottom: 0;
}
div.bodywrapper {
margin-top: 0;
margin-right: 0;
margin-bottom: 0;
margin-left: 0;
}
ul {
margin-left: 0;
}
.document {
width: auto;
}
.footer {
width: auto;
}
.bodywrapper {
margin: 0;
}
.footer {
width: auto;
}
.github {
display: none;
}
}
@media screen and (max-width: 875px) {
body {
margin: 0;
padding: 20px 30px;
}
div.documentwrapper {
float: none;
background: white;
}