Commit 4c33724b authored by Eva Darulova's avatar Eva Darulova

some documentation

parent 6e4c66fe
Project Daisy
# Project Daisy
## 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
```
## 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)
## Documentation
Daisy uses Sphinx for (currently mostly developer) documentation.
To install Sphinx, [follow these instructions](http://www.sphinx-doc.org/en/stable/tutorial.html).
To build the html version of the documentation, navigate to src/sphinx/ and type
```bash
$ make html
```
You can, of course, read the documentation in raw markup format as well.
Acknowledgements
----
......@@ -12,5 +91,3 @@ a passing resemblance to Leon's code.
Leon version used: 978a08cab28d3aa6414a47997dde5d64b942cd3e
First steps
----
......@@ -142,7 +142,7 @@ html_theme = 'alabaster'
# Add any paths that contain custom static files (such as style sheets) here,
# relative to this directory. They are copied after the builtin static files,
# so a file named "default.css" will overwrite the builtin "default.css".
html_static_path = ['_static']
#html_static_path = ['_static']
# Add any extra paths that contain custom files (such as robots.txt or
# .htaccess) here, relative to this directory. These files are copied
......
.. _contributing:
============
Contributing
==============
============
Here is some (random) information that may help you if you want to extend or modify Daisy.
IMPORTANT:
Please always do
import scala.collection.immutable.Seq
if you use Seq's. By default Seq is mutable, so if you forget the import,
you will a) make your code potentially unsafe b) you risk a bunch of fun
type errors with not matching Seq's.
Scala Sequences
---------------
While most of Scala's data structures are immutable by default (i.e. when you do not import any
specific one), this is unfortunately not the case for the 'Seq' type.
Please ::
import scala.collection.immutable.Seq
Daisy is built on the idea of phases.
Currently available phases (check their assumptions and what they promise before use):
- SpecsProcessingPhase: processes the precondition of each method and attaches the extracted information to the corresponding vriable's nodes.
if you use Seq's. If you don't, you may get funny and unexpected results because you will
use the mutable version, or your code may simply not compile because of a mismatch
with the other immutable 'Seq's.
- RangePhase: propagates the ranges added by the SpecsprocessingPhase up the AST with classic interval arithmetic or affine arithmetic.
Creating a New Phase
--------------------
If you want to create a new phase, you may find the following template useful::
In addition to the phases, Daisy also features an interface through smt-lib to currently just one (Z3) SMT solver.
package daisy
package analysis
If you want to create a new phase, you may find the following template useful:
import lang.Trees.Program
package daisy
package analysis
/**
??? Description goes here
import lang.Trees.Program
/**
??? Description goes here
Prerequisites:
- ...
*/
object TemplatePhase extends DaisyPhase {
override val name = ""
override val description = ""
override val definedOptions: Set[CmdLineOptionDef] = Set()
Prerequisites:
- SpecsProcessingPhase
*/
object TemplatePhase extends DaisyPhase {
implicit val debugSection = ???
override val name = ""
override val description = ""
override val definedOptions: Set[CmdLineOptionDef] = Set()
var reporter: Reporter = null
implicit val debugSection = ???
override def run(ctx: Context, prg: Program): (Context, Program) = {
reporter = ctx.reporter
reporter.info(s"\nStarting $name")
val timer = ctx.timers.???.start
var reporter: Reporter = null
override def run(ctx: Context, prg: Program): (Context, Program) = {
reporter = ctx.reporter
reporter.info(s"\nStarting $name")
val timer = ctx.timers.???.start
timer.stop
ctx.reporter.info(s"Finished $name")
(ctx, prg)
}
}
\ No newline at end of file
timer.stop
ctx.reporter.info(s"Finished $name")
(ctx, prg)
}
}
\ No newline at end of file
......@@ -12,21 +12,22 @@ Contents:
:maxdepth: 2
intro
repo_navigation
contributing
installation
testing
trees
phases
code_optimizations
errors
dynamic_phase
troubleshooting
internals
utils
.. phases
.. code_optimizations
.. errors
.. dynamic_phase
.. troubleshooting
Indices and tables
==================
.. Indices and tables
.. ==================
* :ref:`genindex`
* :ref:`modindex`
* :ref:`search`
.. * :ref:`genindex`
.. * :ref:`modindex`
.. * :ref:`search`
Installation instructions
========
You will need the following:
* sbt (simple-build-tool)
* a local copy of scala-abide, where you run sbt publish-local
* sphinx, if you want to compile this documentation
===============
Daisy Internals
===============
---------------------------
Intermediate Representation
---------------------------
Daisy's AST is defined in lang/Trees.scala. The trees and their structure is heavily inspired
by Leon (or simply copied in many places). This has been done on purpose so that
Daisy can re-use much of Leon's functionality easily.
Trees are types, and you will find the type in lang/Types.scala. The objects TreeOps and TypeOps
contain a number of useful operations on trees and types, respectively, such as traversal,
size-of etc.
Each variable (which is also a tree node) has a unique (integer) identifier.
Certain (numerical) tree nodes extend the 'NumAnnotation' trait, which allows
the nodes to be annotated with a range and an absolute error. This annotation is
write-once, i.e. each subsequent annotation attempt will result in an exception being thrown.
The reason for using this impure way is mostly to allow for fixed-point code generation
without having to re-compute the range information. (For generating fixed-point code,
the range of values at each intermediate node has to be known.)
.. Adding a new Node
.. ^^^^^^^^^^^^^^^^^
.. If you want to add a new AST node, you have to do these steps:
.. 1:
.. if (real-leon can extract new node)
.. then
.. skip
.. else
.. modify real-leon to do the extraction
.. package real-leon and update the jar files in daisy/lib/
.. 2: add a new node in lang/Trees
.. 3: extract new node from real-leon in frontends/ScalaExtraction
.. 4: update lang/PrettyPrinter
.. 5: update Extractors and check the functions in lang/TreeOps
.. 6: if your tree node is/can be involved in a call to a solver, make sure
.. it's translation o SMTLib is supported (solvers/Solver.scala)
.. Modifying real-leon
.. ---------------------
.. If you want to add a new function to be parsed, say 'asin',
.. then usually you will need to modify
.. frontends.scalac.ASTExtractors
.. frontends.scalac.CodeExtraction
.. purescala.Extractors
.. Try to search for a tree already present, such as 'Sqrt'.
.. To test your modifications:
.. > run --real library/annotation/package.scala library/daisy/Real.scala testcases/RealTest.scala
\ No newline at end of file
.. _intro:
=====
Intro
==============
=====
Daisy is (or will be) a framework for verifying, approximating and
synthesizing correct numerical programs.
synthesizing numerical programs. Currently, it's more of a building site,
with holes everywhere, but with basic functionality already working.
Its goal is to provide a modular framework that allows quick and easy
experimenting with new techniques and ideas. To this end, it provides basic
infrastructure such as parsing and type checking of inputs as well as
basic utilities such as interval arithmetic or interfaces to solvers.
While performance is, of course, a consideration, the first priority is
ease of understanding, reasoning about and extending the code.
--------------
Input Programs
--------------
Daisy accepts one input file which must follow the following basic structure::
import daisy.lang._
import Real._
object TestObject {
def function(x: Real): Real = {
require(...)
val z = x + x
z * x
}
}
Input programs are written over a real-valued, not executable data type 'Real'
and consist of a top-level object and a number of function definitions.
Currently, each function is analyzed in isolation, but we hope to change
this in the future and instead allow for a designated 'main' method together
with a number of helper methods.
Function bodies may consist of arithmetic expressions, including square root,
and let-like immutable variable definitions ('val z = ').
-----------------
Daisy's Structure
-----------------
Daisy is intended to work in phases (as much as possible) - similarly to a compiler -
for modularity's sake. Currently, working phases are
* SpecsProcessingPhase: parse the 'require' clause
* RangeErrorPhase: compute ranges and absolute (roundoff) errors of all (intermediate) values
* InfoPhase: print out interesting results about the input program
There is more work in progress, and it will be added here, once it's more mature.
The goal is to build a modular framework which allows easy extension and
(re-)combination of different techniques. To achieve this, Daisy works in
'phases', each of which performs one self-contained analysis, verification or
synthesis pass.
\ No newline at end of file
.. _repo_navigation:
=========================
Navigating the Repository
=========================
Some of these are rather empty for now; the most interesting folders for
the average developer are listed in bold.
*benchmarking/*: code which benchmarks timing of a few functions written in C
*data/*: some experiments generate data and when this should persist, it belongs in here
*lib/*: jar files that Daisy requires
*library/*: definition of the 'Real' data type used in the specification language
*project/*: sbt configuration
*rawdata/*: folder where Daisy may spit out outputs (instead of polluting the home directory). In contrast to the data/ folder the files
in rawdata/ are not persistent.
*scripts/*: various bash scripts, used for random experiments
*src/bench/*: performance benchmarks using the ScalaMeter framework
**src/main/**: Daisy's source code
**src/sphinx/**: documentation
**src/test/**: unit tests using the ScalaTest framework
*target/*: sbt-generated folder with class files
**testcases/**: testcases, as the name says
=======
Testing
==========
=======
Each function or collection of functions that provide a particular
functionality should be accompanied by at least a unit test.
......@@ -7,10 +9,12 @@ functionality should be accompanied by at least a unit test.
These are located in src/test/scala/unit and are integrated with sbt with
ScalaTest.
To run all tests:
> test
To run all tests (in sbt interactive mode)::
> test
All tests should pass, if not please report or fix.
To run a specific testcase:
test-only daisy.test.NameOfTest
To run a specific testcase::
> test-only daisy.test.NameOfTest
Trees
============
Daisy's AST is defined in lang/Trees. The trees and heir structure is heavily inspired
by Leon (or simply copied in many places). This has been done on purpose so that
Daisy can re-use much of Leon's functionality easily.
If you want to add a new AST node, you have to do these steps:
1:
if (real-leon can extract new node)
then
skip
else
modify real-leon to do the extraction
package real-leon and update the jar files in daisy/lib/
2: add a new node in lang/Trees
3: extract new node from real-leon in frontends/ScalaExtraction
4: update lang/PrettyPrinter
5: update Extractors and check the functions in lang/TreeOps
6: if your tree node is/can be involved in a call to a solver, make sure
it's translation o SMTLib is supported (solvers/Solver.scala)
Modifying real-leon
---------------------
If you want to add a new function to be parsed, say 'asin',
then usually you will need to modify
frontends.scalac.ASTExtractors
frontends.scalac.CodeExtraction
purescala.Extractors
Try to search for a tree already present, such as 'Sqrt'.
To test your modifications:
> run --real library/annotation/package.scala library/daisy/Real.scala testcases/RealTest.scala
\ No newline at end of file
=========
Utilities
=========
Daisy provides a number of utilities which are useful in their own right.
AffineForm
----------
An implementation of affine arithmetic over rationals.
Interval
--------
A standard implementation of intervals over rationals.
MPFRFloat
---------
A Scala wrapper around the Java wrapper around the C MPFR arbitrary precision
library. (May require the MPFR library to be installed locally.)
Rational
--------
A straight-forward implementation of a rational data type on top of
Java's BigIntegers. The square root operation cannot be computed
exactly in rationals; our implementation provides a (hacky) approximation.
SMTRange
--------
A combination of interval arithmetic and SMT solving to compute tighter
ranges. Requires Z3 to be installed.
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