/
RELEASENOTES
197 lines (159 loc) · 7.46 KB
/
RELEASENOTES
1
2
3
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
61
62
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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
Hackage: <http://hackage.haskell.org/package/sbv>
GitHub: <http://github.com/LeventErkok/sbv>
======================================================================
Version 0.9.22, 2011-11-13
The major change in this release is the support for quantifiers. The
SBV library *no* longer assumes all variables are universals in a proof,
(and correspondingly existential in a sat) call. Instead, the user
marks free-variables appropriately using forall/exists functions, and the
solver translates them accordingly. Note that this is a non-backwards
compatible change in sat calls, as the semantics of formulas is essentially
changing. While this is unfortunate, it's more uniform and simpler to understand
in general.
This release also adds support for the Z3 solver, which is the main
SMT-solver used for solving formulas involving quantifiers. More formally,
we use the new AUFBV/ABV/UFBV logics when quantifiers are involved. Also,
the communication with Z3 is now done via SMT-Lib2 format. Eventually
the SMTLib1 connection will be severed.
The other main change is the support for C code generation with
uninterpreted functions enabling users to interface with external
C functions defined elsewhere. See below for details.
Other changes:
Code:
* Change getModel, so it returns an Either value to indicate
something went wrong; instead of throwing an error
* Add support for computing CRCs directly (without needing
polynomial division).
Code generation:
* Add "cgGenerateDriver" function, which can be used to turn
on/off driver program generation. Default is to generate
a driver. (Issue "cgGenerateDriver False" to skip the driver.)
For a library, a driver will be generated if any of the
constituent parts has a driver. Otherwise it'll be skipped.
* Fix a bug in C code generation where "Not" over booleans were
incorrectly getting translated due to need for masking.
* Add support for compilation with uninterpreted functions. Users
can now specify the corresponding C code and SBV will simply
call the "native" functions instead of generating it. This
enables interfacing with other C programs. See the functions:
cgAddPrototype, cgAddDecl, and cgAddLDFlags.
Examples:
* Add CRC polynomial generation example via existentials
* Add USB CRC code generation example, both via polynomials and
using the internal CRC functionality
======================================================================
Version 0.9.21, 2011-08-05
Code generation:
* Allow for inclusion of user makefiles
* Allow for CCFLAGS to be set by the user
* Other minor clean-up
======================================================================
Version 0.9.20, 2011-06-05
* Regression on 0.9.19; add missing file to cabal
======================================================================
Version 0.9.19, 2011-06-05
Code:
* Add SignCast class for conversion between signed/unsigned
quantities for same-sized bit-vectors
* Add full-binary trees that can be indexed symbolically (STree). The
advantage of this type is that the reads and writes take
logarithmic time. Suitable for implementing faster symbolic look-up.
* Expose HasSignAndSize class through Data.SBV.Internals
* Many minor improvements, file re-orgs
Examples:
* Add sentence-counting example
* Add an implementation of RC4
======================================================================
Version 0.9.18, 2011-04-07
Code:
* Re-engineer code-generation, and compilation to C.
In particular, allow arrays of inputs to be specified,
both as function arguments and output reference values.
* Add support for generation of generation of C-libraries,
allowing code generation for a set of functions that
work together.
Examples:
* Update code-generation examples to use the new API.
* Include a library-generation example for doing 128-bit
AES encryption
======================================================================
Version 0.9.17, 2011-03-29
Code:
* Simplify and reorganize the test suite
Examples:
* Improve AES decryption example, by using
table-lookups in InvMixColumns.
======================================================================
Version 0.9.16, 2011-03-28
Code:
* Further optimizations on Bits instance of SBV
Examples:
* Add AES algorithm as an example, showing how
encryption algorithms are particularly suitable
for use with the code-generator
======================================================================
Version 0.9.15, 2011-03-24
Bug fixes:
* Fix rotateL/rotateR instances on concrete
words. Previous versions was bogus since
it relied on the Integer instance, which
does the wrong thing after normalization.
* Fix conversion of signed numbers from bits,
previous version did not handle two's
complement layout correctly
Testing:
* Add a sleuth of concrete test cases on
arithmetic to catch bugs. (There are many
of them, ~30K, but they run quickly.)
======================================================================
Version 0.9.14, 2011-03-19
- Reimplement sharing using Stable names, inspired
by the Data.Reify techniques. This avoids tricks
with unsafe memory stashing, and hence is safe.
Thus, issues with respect to CAFs are now resolved.
======================================================================
Version 0.9.13, 2011-03-16
Bug fixes:
* Make sure SBool short-cut evaluations are done
as early as possible, as these help with coding
recursion-depth based algorithms, when dealing
with symbolic termination issues.
Examples:
* Add fibonacci code-generation example, original
code by Lee Pike.
* Add a GCD code-generation/verification example
======================================================================
Version 0.9.12, 2011-03-10
New features:
* Add support for compilation to C
* Add a mechanism for offline saving of SMT-Lib files
Bug fixes:
* Output naming bug, reported by Josef Svenningsson
* Specification bug in Legato's multipler example
======================================================================
Version 0.9.11, 2011-02-16
* Make ghc-7.0 happy, minor re-org on the cabal file/Setup.hs
======================================================================
Version 0.9.10, 2011-02-15
* Integrate commits from Iavor: Generalize SBV's to keep
track the integer directly without resorting to different
leaf types
* Remove the unnecessary CLC instruction from the Legato example
* More tests
======================================================================
Version 0.9.9, 2011-01-23
* Support for user-defined SMT-Lib axioms to be
specified for uninterpreted constants/functions
* Move to using doctest style inline tests
======================================================================
Version 0.9.8, 2011-01-22
* Better support for uninterpreted-functions
* Support counter-examples with SArray's
* Ladner-Fischer scheme example
* Documentation updates
======================================================================
Version 0.9.7, 2011-01-18
* First stable public hackage release
======================================================================
Versions 0.X.X - 0.9.6
* Basic infrastructure, design exploration