Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
Updated todos and tutorial bib.
  • Loading branch information
Lee Pike committed Jan 23, 2012
1 parent 9c617c4 commit 9394eb6
Show file tree
Hide file tree
Showing 2 changed files with 43 additions and 53 deletions.
94 changes: 42 additions & 52 deletions todo.md
@@ -1,81 +1,71 @@
TODOs
=====

* Add instances for IntegPow to the two backends and to the QC.
* Add instances for IntegPow to the two backends and to the QC.

* Testing: record and compare against "golden value" outputs, at least for
interpreter.
* Testing: record and compare against "golden value" outputs, at least for
interpreter.

* Use tags for external functions in SBV backend.
* Use tags for external functions in SBV backend.

* In interpretation, external functions need to take Stream arguments.
* In interpretation, external functions need to take Stream arguments.

* Fix SBV's makefile generation.
* Fix SBV's makefile generation.

* Generate SBV checks, particularly for array out of bounds.
* Generate SBV checks, particularly for array out of bounds.

* QuickCheck:
* QuickCheck:

* Generate external arrays and functions.
* Generate external arrays and functions.

* Remove stream guards(?).
* Remove stream guards(?).

* Implement casting for SBV backend.
* Implement casting for SBV backend.

* Remove Tests/... and have the regression execute everything in Examples
* Remove Tests/... and have the regression execute everything in Examples

* Need Graph.hs in copilot-language?
* Need Graph.hs in copilot-language?

* Replicate Interface.hs from the "old Copilot".
* Replicate Interface.hs from the "old Copilot".

* Comments, especially at the beginning of modules and on module exports.
* Comments, especially at the beginning of modules and on module exports.

* Make Copilot operator precedence match Haskell operator precedence.
(make binary operators associative, for now we have to write 'a && ( b && c )'
with parens).
* Make Copilot operator precedence match Haskell operator precedence. (make
binary operators associative, for now we have to write 'a && ( b && c )' with
parens).

* Add casts to the language. Add casts that are able to construct a floating
point stream out of 4 Word8, 2 Word16, 1 Word32 and so on (architecture
specific), to help protocol monitoring
* Add casts to the language. Add casts that are able to construct a floating
point stream out of 4 Word8, 2 Word16, 1 Word32 and so on (architecture
specific), to help protocol monitoring

* Add a backend to Feldspar.
* Add a backend to Feldspar.


KNOWN BUGS
====

* In the interpreter, the same symbol '--' is used for the trigger guard being
false and even if its true, if there are no arguments. Use a different
symbol for no arguments.
* The interpreter computes all output before printing to screen. This can mean
it takes a long time to print the output from large expressions.

* SBV will generate an internal.h header that equates SBool to uint8 rather than
bool. This can mess up CBMC. Just at #include stdbool.h and redefine
SBool.
* SBV: external array indicies can depend on external variables. Need to do a
causality analysis to ensure we're not using an updated value during sampling.
E.g.:

* SBV: external array indicies can depend on external variables. Need to do a
causality analysis to ensure we're not using an updated value during
sampling. E.g.:
void sampleExts(void) {
ext_idx2 = idx2;
ext_arr1 = arr1[mk_ext_arr_arr1(queue_0, ptr_0)];
ext_arr2 = arr2[mk_ext_arr_arr2(ext_idx2)];
}

void sampleExts(void) {
ext_idx2 = idx2;
ext_arr1 = arr1[mk_ext_arr_arr1(queue_0, ptr_0)];
ext_arr2 = arr2[mk_ext_arr_arr2(ext_idx2)];
}
(Check what's done in the copilot-c99 backend.)

(Check what's done in the copilot-c99 backend.)
* We use stable names
(http://www.haskell.org/ghc/docs/latest/html/libraries/base-4.4.1.0/System-Mem-StableName.html)
for sharing, which can't determine that a name is stable for polymorphic
functions that have type constraints. This is because the type gets turned
into a dictionary, and so each application is a new thunk. For example,
consider the small example at https://gist.github.com/1385118

* RegExpExamples.hs (and possibly other monitors) use up all memory with the
interpreter (not sure if still the case).

* 'even' is not hidden Language.Copilot (from the Test suite, I think).

* We use stable names
(http://www.haskell.org/ghc/docs/latest/html/libraries/base-4.4.1.0/System-Mem-StableName.html)
for sharing, which can't determine that a name is stable for polymorphic
functions that have type constraints. This is because the type gets turned
into a dictionary, and so each application is a new thunk. For example,
consider the small example at https://gist.github.com/1385118

Thus, we require the restriction that all Copilot stream definitions have
top-level definitions that are monomorphic (the monomorphic functions can
all polymorphic functions though).
Thus, we require the restriction that all Copilot stream definitions have
top-level definitions that are monomorphic (the monomorphic functions can all
polymorphic functions though).
2 changes: 1 addition & 1 deletion tutorial/mybib.bib
Expand Up @@ -49,7 +49,7 @@ @inbook{smt
title = "Satisfiability Modulo Theories",
chapter = 26,
pages = "825--885",
Title = {Handbook of Satisfiability},
booktitle = {Handbook of Satisfiability},
Publisher = {IOS Press},
Year = {2009},
Series = {Frontiers in Artificial Intelligence and Applications}
Expand Down

0 comments on commit 9394eb6

Please sign in to comment.