Skip to content

GitLab

F
FloVer
Commit 040f86fa authored by Heiko Becker's avatar Heiko Becker
Browse files
Options

Update README

parent ff37cc07
Hide whitespace changes
Inline Side-by-side
Showing with 35 additions and 130 deletions
README.md
View file @ 040f86fa
# 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.
# Project FloVer
## First steps
Daisy is set up to work with the [simple build tool (sbt)](http://www.scala-sbt.org/).
Once you have sbt, type in daisy's home directory:
```
$ sbt
```
This will run sbt in interactive mode. Note, if you run sbt for the first time,
*this operation may take a substantial amount of time* (heaven knows why). SBT helpfully
prints what it is doing in the process. If you feel like nothing has happened for an unreasonable
amount of time, abort and retry. This usually fixes the problem, otherwise try the old trick: restart.
To compile daisy:
```bash
> compile
```
To Daisy run an example:
```
> run testcases/rosa/Doppler.scala
```
Note that Daisy currently supports only one input file at a time.
The above command should produce an output such as (your own timing information will naturally vary):
```
Extracting program
[ Info ]
[ Info ] Starting specs preprocessing phase
[ Info ] Finished specs preprocessing phase
[ Info ]
[ Info ]
[ Info ] Starting range-error phase
[ Info ] Finished range-error phase
[ Info ]
[ Info ] Starting info phase
[ Info ] doppler
[ Info ] error: 4.1911988101104756e-13, range: [-158.7191444098274, -0.02944244059231351]
[ Info ] Finished info phase
[ Info ] time:
[ Info ] info: 6 ms, rangeError: 360 ms, analysis: 6 ms, frontend: 2902 ms,
```
To see all command-line options:
```
> run --help
```
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
```
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
```
## Generating Error Bound Certificates
If you want to produce certificates to check them in either of the supported backends,
you have to call Daisy as with
If you want to generate error bound certificates, you have to install Daisy from [https://github.com/malyzajko/daisy/tree/certified].
You then have to call Daisy with
```bash
$ ./daisy file --certificate=coq
```
......@@ -82,60 +17,64 @@ or for one of the binaries
```bash
$ ./daisy file --certificate=binary
```
The certificate can then be found in the folder `coq/output`, `hol4/output` or `output` for binary certificates.
The certificate will be generated in the output folder of Daisy.
To make sure that the certificate can be validated in the logics, please use
`--errorMethod=interval` and either `--rangeMethod=interval` or `--rangeMethod=affine`.
Unfortunately, affine polynomials are currently only supported on the branch `affine_arithmetic`.
Full support for fixed-point programs is also only available in `affine_arithmetic`.
## Checking Coq certificates
To check the Coq certificate, you need to enter the `coq` directory and then run
FloVer is known to compile with coq `8.7.2` and `8.8.0`.
To check the Coq certificate, you need to enter the `coq` directory.
Place any certificate you want to have checked into the `output` folder in the
coq directory and then run
```bash
$ ./configure_coq.sh
$ make
```
This will compile all coq files and then in the end the certificate in the output directory.
The coq binaries are build in the directory `coq/binary` and you can compile them by running
either `make native` or make byte` in the directory.
The coq binary is build in the directory `coq/binary` and you can compile it by
running `make native` in the directory.
If an additional certificate should be checked later on, it suffices to call the Coq compiler:
```bash
$ coqc -R ./ Daisy output/CERTIFICATE_FILE.v
$ coqc -R ./ Flover output/CERTIFICATE_FILE.v
```
where `./` is FloVer's `coq` folder.
The generated binaries can be run with `coq_checker_{native/byte} CERTIFICATE_FILE`.
The generated binary can be run with `coq_checker_native CERTIFICATE_FILE`.
## Checking HOL4 certificates
If you haven't updated your HOL4 installation in a while, update it first:
```bash
$ cd path/to/HOL
$ bin/build cleanAll
$ poly < tools/smart-configure.sml
$ bin/build
```
Then, back in the Daisy home directory, if you haven't done so before:
As only some versions of HOL4 are known to compile with CakeML, we provide a
configure script that sets up HOL4 accordingly:
```bash
$ git submodule init
$ cd hol4
$ ./configure_hol.sh --init
```
(If successfull, you should see a message like ```Submodule 'hol4/cakeml' (https://github.com/CakeML/cakeml.git) registered for path 'hol4/cakeml'```)
This will initialize the CakeML submodule and check out a HOL4 version that is
known to be compatible with it in your `$HOLDIR`.
Then, initialize the CakeML submodule and start compilation:
Then, you can start compilation:
```bash
$ git submodule update --recursive
$ cd hol4/
$ Holmake
```
Note that this may take some time, since it also builds all files from CakeML on which the binary code extraction depends.
If you don't want to wait for so long, you can cheat the compilation:
Note that this may take some time, since it also builds all files from CakeML on
which the binary code extraction depends. If you don't want to wait for so long,
you can cheat the compilation:
```bash
$ Holmake --fast
```
To check the HOL4 certificates, enter the `hol4/output` directory and run
To check HOL4 certificates, put them in the `hol4/output` directory , `cd` there
and run
```bash
$ Holmake ${CERTIFICATE_FILE/Script.sml/Theory.sig}
```
The HOL4 binary is build by entering the directory `hol4/binary`. Then one needs to run
The HOL4 binary is build by entering the directory `hol4/binary`. Then one needs
to run
```bash
$ Holmake checkerBinaryTheory.sig
$ Holmake
......@@ -143,49 +82,15 @@ $ Holmake
The generated file `cake_checker` is the binary.
It can be run by
```bash
$ ./cake_checker < CERTIFICATE_FILE
$ ./cake_checker CERTIFICATE_FILE
```
## Additional Software
Some features of Daisy require additional software to be installed.
Currently, this is
* 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`\]
## 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 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 -> path-to-the-build.sbt-file
or
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.
In no particular order: Raphael Monat, Nikita Zyuzin, Heiko Becker
Acknowledgements
----
A big portion of the infrastructure has been inspired by and sometimes
directly taken from the Leon project (see the LEON_LICENSE).
Especially the files in frontend, lang, solvers and utils bear more than
a passing resemblance to Leon's code.
Leon version used: 978a08cab28d3aa6414a47997dde5d64b942cd3e
We would like to thank Jacques-Henri Jourdan for the many insightful discussions
and technical help while working on the initial version of FloVer.
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment