README.md 3.78 KB
Newer Older
Eva Darulova's avatar
Eva Darulova committed
1
# Project Daisy
2 3


Eva Darulova's avatar
Eva Darulova committed
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
## 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 (and then some).
You can then run Daisy on an input file as follows:
```bash
$ ./daisy testcases/rosa/Doppler.scala
```

Heiko Becker's avatar
Heiko Becker committed
61 62
## Checking Interval Arithmetic Certificates

63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91
If you want to produce certificates to check them in either of the supported backends,
you have to call Daisy as with
```bash
$ ./daisy file --certificate=coq
```
or
```bash
$ ./daisy file --certificate=hol
```

The certificate can then be found in the folder `coq/output` or `hol/output`.

To check the Coq certificate, you need to enter 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.
If an additional certificate should be checked later on, it suffices to call the Coq compiler:
```bash
$ coqc -R ./ Daisy output/CERTIFICATE_FILE.v
```

To check the HOL-Light certificates, you need to enter the hol directory and then run
```bash
$ ./configure_hol.sh
$ ocaml output/CERTIFICATE_FILE.hl
```

Eva Darulova's avatar
Eva Darulova committed
92 93 94 95 96 97 98 99 100 101 102
## Additional Software

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).

* MPFR: Daisy uses a [Java binding](https://github.com/kframework/mpfr-java).
(TODO: figure out whether we used the static or dynamic binding)

103 104 105 106 107 108 109
* Coq: Version 8.5pl2 if you want to extract certificates for it, [install it](https://coq.inria.fr/download)

* HOL-Light: Git checkout (no later than 1.08.2016) if you want to extract certificates for it, [downloadit](https://github.com/jrh13/hol-light/)
  Afterwards configure the environment variable HOLLIGHT_HOME to point to the directory you downloaded HOL-Light into with
```
$ export HOLLIGHT_HOME=path_to_hol_light_git
```
Eva Darulova's avatar
Eva Darulova committed
110 111 112 113
## Documentation



114 115 116 117
Acknowledgements
----

A big portion of the infrastructure has been inspired by and sometimes
118
directly taken from the Leon project (see the LEON_LICENSE).
119

Eva Darulova's avatar
Eva Darulova committed
120 121 122
Especially the files in frontend, lang, solvers and utils bear more than
a passing resemblance to Leon's code.
Leon version used: 978a08cab28d3aa6414a47997dde5d64b942cd3e