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

Daisy is set up to work with the simple build tool (sbt). 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:

> 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:

$ ./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

$ ./daisy file --certificate=coq

or

$ ./daisy file --certificate=hol4

or for one of the binaries

$ ./daisy file --certificate=binary

The certificate can then be found in the folder coq/output, hol4/output or output for binary certificates.

Checking Coq certificates

To check the Coq certificate, you need to enter the coq directory and then run

$ ./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.

If an additional certificate should be checked later on, it suffices to call the Coq compiler:

$ coqc -R ./ Daisy output/CERTIFICATE_FILE.v

The generated binaries can be run with coq_checker_{native/byte} CERTIFICATE_FILE.

Checking HOL4 certificates

If you haven't updated your HOL4 installation in a while, update it first:

$ 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:

$ git submodule init

(If successfull, you should see a message like Submodule 'hol4/cakeml' (https://github.com/CakeML/cakeml.git) registered for path 'hol4/cakeml')

Then, initialize the CakeML submodule and start compilation:

$ 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:

$ Holmake --fast

To check the HOL4 certificates, enter the hol4/output directory and run

$ Holmake ${CERTIFICATE_FILE/Script.sml/Theory.sig}

The HOL4 binary is build by entering the directory hol4/binary. Then one needs to run

$ Holmake checkerBinaryTheory.sig
$ Holmake

The generated file cake_checker is the binary. It can be run by

$ ./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 [Linux] [Mac] and/or dReal [Linux]

• MPFR 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

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.

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