GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 04:44:39 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into feature/repl-bindings

Browse Source 
Conflicts:
	cryptol/REPL/Command.hs
	src/Cryptol/Symbolic.hs

Fixed up Value -> Expr conversion to account for a change in those
types. Reworked sat and prove results to account for changes in that
API.
This commit is contained in:
Adam C. Foltzer 2014-08-19 11:32:59 -07:00
commit 5a3c01afc4
67 changed files with 4882 additions and 1733 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
cryptol.cabal
View File

@ -22,6 +22,7 @@ flag notebook
library
Build-depends: base >= 4.6,
array >= 0.4,
async >= 2.0,
containers >= 0.5,
deepseq >= 1.3,
directory >= 1.2,
@ -29,7 +30,7 @@ library
filepath >= 1.3,
GraphSCC >= 1.0.4,
monadLib >= 3.7.2,
mtl >= 2.1,
mtl >= 2.2.1,
old-time >= 1.1,
presburger >= 1.1,
pretty >= 1.1,
@ -86,6 +87,7 @@ library
Cryptol.TypeCheck.PP,
Cryptol.TypeCheck.Solve,
Cryptol.TypeCheck.TypeMap,
Cryptol.TypeCheck.TypeOf,
Cryptol.TypeCheck.Defaulting,
Cryptol.TypeCheck.Solver.Eval,
@ -116,15 +118,17 @@ library
Cryptol.Symbolic.Prims
Cryptol.Symbolic.Value
Other-modules: Cryptol.Parser.LexerUtils,
Cryptol.Parser.ParserUtils,
Data.SBV,
Data.SBV.Bridge.Boolector,
Data.SBV.Bridge.CVC4,
Data.SBV.Bridge.MathSAT,
Data.SBV.Bridge.Yices,
Data.SBV.Bridge.Z3,
Data.SBV.Internals,
Data.SBV.Tools.Polynomial
Other-modules: Cryptol.Parser.LexerUtils,
Cryptol.Parser.ParserUtils,
Data.SBV.BitVectors.AlgReals,
Data.SBV.BitVectors.Data,
Data.SBV.BitVectors.Model,
@ -144,10 +148,10 @@ library
Data.SBV.Provers.CVC4,
Data.SBV.Provers.Yices,
Data.SBV.Provers.Z3,
Data.SBV.Provers.MathSAT,
Data.SBV.Tools.ExpectedValue,
Data.SBV.Tools.GenTest,
Data.SBV.Tools.Optimize,
Data.SBV.Tools.Polynomial,
Data.SBV.Utils.Boolean,
Data.SBV.Utils.TDiff,
Data.SBV.Utils.Lib,

85
cryptol/REPL/Command.hs
View File

@ -332,20 +332,28 @@ proveCmd str = do
EnvString proverName <- getUser "prover"
EnvBool iteSolver <- getUser "iteSolver"
EnvBool verbose <- getUser "debug"
mcx <- liftModuleCmd $ Cryptol.Symbolic.prove (proverName, iteSolver, verbose, str)
(M.deDecls denv)
(expr, schema)
-- bind the counterexamples, if any, to `it`
for_ mcx $ \cxexprs -> do
case cxexprs of
[] -> return ()
-- if there's only one argument, just bind it
[(cxty, cxexpr)] -> bindItVariable cxexpr cxty
-- if there are more than one, tuple them up
_ -> do
let tty = T.tTuple (map fst cxexprs)
texp = T.ETuple (map snd cxexprs)
bindItVariable texp tty
result <- liftModuleCmd $ Cryptol.Symbolic.prove (proverName, iteSolver, verbose)
(M.deDecls denv)
(expr, schema)
ppOpts <- getPPValOpts
case result of
Left msg -> io $ putStrLn msg
Right Nothing -> io $ putStrLn "Q.E.D."
Right (Just tevs) -> do
let vs = map (\(_,_,v) -> v) tevs
tes = map (\(t,e,_) -> (t,e)) tevs
doc = ppPrec 3 parseExpr -- function application has precedence 3
docs = map (pp . E.WithBase ppOpts) vs
io $ print $ hsep (doc : docs) <+> text "= False"
-- bind the counterexamples to `it`
case tes of
[] -> return ()
-- if there's only one argument, just bind it
[(t, e)] -> bindItVariable e t
-- if there are more than one, tuple them up
_ -> bindItVariable texp tty
where tty = T.tTuple (map fst tes)
texp = T.ETuple (map snd tes)
satCmd :: String -> REPL ()
satCmd str = do
@ -355,20 +363,28 @@ satCmd str = do
EnvString proverName <- getUser "prover"
EnvBool iteSolver <- getUser "iteSolver"
EnvBool verbose <- getUser "debug"
msat <- liftModuleCmd $ Cryptol.Symbolic.sat (proverName, iteSolver, verbose, str)
(M.deDecls denv)
(expr, schema)
-- bind the satisfying assignment, if any, to `it`
for_ msat $ \satexprs -> do
case satexprs of
[] -> return ()
-- if there's only one argument, just bind it
[(satty, satexpr)] -> bindItVariable satexpr satty
-- if there are more than one, tuple them up
_ -> do
let tty = T.tTuple (map fst satexprs)
texp = T.ETuple (map snd satexprs)
bindItVariable texp tty
result <- liftModuleCmd $ Cryptol.Symbolic.sat (proverName, iteSolver, verbose)
(M.deDecls denv)
(expr, schema)
ppOpts <- getPPValOpts
case result of
Left msg -> io $ putStrLn msg
Right Nothing -> io $ putStrLn "Unsatisfiable."
Right (Just tevs) -> do
let vs = map (\(_,_,v) -> v) tevs
tes = map (\(t,e,_) -> (t,e)) tevs
doc = ppPrec 3 parseExpr -- function application has precedence 3
docs = map (pp . E.WithBase ppOpts) vs
io $ print $ hsep (doc : docs) <+> text "= True"
-- bind the satisfying assignment to `it`
case tes of
[] -> return ()
-- if there's only one argument, just bind it
[(t, e)] -> bindItVariable e t
-- if there are more than one, tuple them up
_ -> bindItVariable texp tty
where tty = T.tTuple (map fst tes)
texp = T.ETuple (map snd tes)
specializeCmd :: String -> REPL ()
specializeCmd str = do
@ -512,7 +528,7 @@ browseVars pfx = do
setOptionCmd :: String -> REPL ()
setOptionCmd str
| Just value <- mbValue = setUser (mkKey key) value
| Just value <- mbValue = setUser key value
| null key = mapM_ (describe . optName) (leaves userOptions)
| otherwise = describe key
where
@ -522,18 +538,17 @@ setOptionCmd str
_ : stuff -> Just (trim stuff)
_ -> Nothing
mkKey = takeWhile (not . isSpace)
describe k = do
ev <- tryGetUser (mkKey k)
ev <- tryGetUser k
io $ case ev of
Just (EnvString s) -> putStrLn (k ++ " = " ++ s)
Just (EnvNum n) -> putStrLn (k ++ " = " ++ show n)
Just (EnvBool True) -> putStrLn (k ++ " = on")
Just (EnvBool False) -> putStrLn (k ++ " = off")
Nothing -> putStrLn ("Unknown user option: `" ++ k ++ "`")
Nothing -> do putStrLn ("Unknown user option: `" ++ k ++ "`")
when (any isSpace k) $ do
let (k1, k2) = break isSpace k
putStrLn ("Did you mean: `:set " ++ k1 ++ " =" ++ k2 ++ "`?")
helpCmd :: String -> REPL ()

12
cryptol/REPL/Monad.hs
View File

@ -60,6 +60,7 @@ import qualified Cryptol.TypeCheck.AST as T
import Cryptol.Utils.PP
import Cryptol.Utils.Panic (panic)
import qualified Cryptol.Parser.AST as P
import Cryptol.Symbolic (proverNames)
import Control.Applicative (Applicative(..))
import Control.Monad (ap,unless,when)
@ -434,8 +435,8 @@ userOptions = mkOptionMap
"The number of elements to display for infinite sequences."
, OptionDescr "tests" (EnvNum 100) (const Nothing)
"The number of random tests to try."
, OptionDescr "prover" (EnvString "cvc4") checkProver
"The external smt solver for :prove and :sat (cvc4, yices, or z3)."
, OptionDescr "prover" (EnvString "cvc4") checkProver $
"The external smt solver for :prove and :sat (" ++ proverListString ++ ")."
, OptionDescr "iteSolver" (EnvBool False) (const Nothing)
"Use smt solver to filter conditional branches in proofs."
, OptionDescr "warnDefaulting" (EnvBool True) (const Nothing)
@ -460,10 +461,13 @@ checkInfLength val = case val of
checkProver :: EnvVal -> Maybe String
checkProver val = case val of
EnvString s
| s `elem` ["cvc4", "yices", "z3"] -> Nothing
| otherwise -> Just "prover must be cvc4, yices, or z3"
| s `elem` proverNames -> Nothing
| otherwise -> Just $ "prover must be " ++ proverListString
_ -> Just "unable to parse a value for prover"
proverListString :: String
proverListString = concatMap (++ ", ") (init proverNames) ++ "or " ++ last proverNames
-- Environment Utilities -------------------------------------------------------
whenDebug :: REPL () -> REPL ()

BIN
docs/ProgrammingCryptol.pdf
View File

Binary file not shown.

387
docs/ProgrammingCryptol/appendices/Syntax.tex Normal file
View File

@ -0,0 +1,387 @@
\section{Layout}\label{layout}
Groups of declarations are organized based on indentation. Declarations
with the same indentation belong to the same group. Lines of text that
are indented more than the beginning of a declaration belong to that
declaration, while lines of text that are indented less terminate a
group of declaration. Groups of declarations appear at the top level of
a Cryptol file, and inside \texttt{where} blocks in expressions. For
example, consider the following declaration group
\begin{verbatim}
f x = x + y + z
where
y = x * x
z = x + y
g y = y
\end{verbatim}
This group has two declaration, one for \texttt{f} and one for
\texttt{g}. All the lines between \texttt{f} and \texttt{g} that are
indented more then \texttt{f} belong to \texttt{f}.
This example also illustrates how groups of declarations may be nested
within each other. For example, the \texttt{where} expression in the
definition of \texttt{f} starts another group of declarations,
containing \texttt{y} and \texttt{z}. This group ends just before
\texttt{g}, because \texttt{g} is indented less than \texttt{y} and
\texttt{z}.
\section{Comments}\label{comments}
Cryptol supports block comments, which start with \texttt{/*} and end
with \texttt{*/}, and line comments, which start with \texttt{//} and
terminate at the end of the line. Block comments may be nested
arbitrarily.
Examples:
\begin{verbatim}
/* This is a block comment */
// This is a line comment
/* This is a /* Nested */ block comment */
\end{verbatim}
\section{Identifiers}\label{identifiers}
Cryptol identifiers consist of one or more characters. The first
character must be either an English letter or underscore (\texttt{\_}).
The following characters may be an English letter, a decimal digit,
underscore (\texttt{\_}), or a prime (\texttt{'}). Some identifiers have
special meaning in the language, so they may not be used in
programmer-defined names (see
\hyperref[keywords-and-built-in-operators]{Keywords}).
Examples:
\begin{verbatim}
name name1 name' longer_name
Name Name2 Name'' longerName
\end{verbatim}
\hyperdef{}{keywords-and-built-in-operators}{\section{Keywords and
Built-in Operators}\label{keywords-and-built-in-operators}}
The following identifiers have special meanings in Cryptol, and may not
be used for programmer defined names:
\begin{verbatim}
Arith Inf extern inf module then
Bit True fin lg2 newtype type
Cmp else if max pragma where
False export import min property width
\end{verbatim}
The following table contains Cryptol's operators and their associativity
with lowest precedence operators first, and highest precedence last.
\begin{longtable}[c]{@{}ll@{}}
\toprule\addlinespace
Operator & Associativity
\\\addlinespace
\midrule\endhead
\texttt{\textbar{}\textbar{}} & left
\\\addlinespace
\texttt{\^{}} & left
\\\addlinespace
\texttt{\&\&} & left
\\\addlinespace
\texttt{-\textgreater{}} (types) & right
\\\addlinespace
\texttt{!=} \texttt{==} & not associative
\\\addlinespace
\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=}
\texttt{\textgreater{}=} & not associative
\\\addlinespace
\texttt{\#} & right
\\\addlinespace
\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}}
\texttt{\textgreater{}\textgreater{}\textgreater{}}
\texttt{\textless{}\textless{}\textless{}} & left
\\\addlinespace
\texttt{+} \texttt{-} & left
\\\addlinespace
\texttt{*} \texttt{/} \texttt{\%} & left
\\\addlinespace
\texttt{\^{}\^{}} & right
\\\addlinespace
\texttt{!} \texttt{!!} \texttt{@} \texttt{@@} & left
\\\addlinespace
(unary) \texttt{-} \texttt{\textasciitilde{}} & right
\\\addlinespace
\bottomrule
\addlinespace
\caption{Operator precedences.}
\end{longtable}
\section{Numeric Literals}\label{numeric-literals}
Numeric literals may be written in binary, octal, decimal, or
hexadecimal notation. The base of a literal is determined by its prefix:
\texttt{0b} for binary, \texttt{0o} for octal, no special prefix for
decimal, and \texttt{0x} for hexadecimal.
Examples:
\begin{verbatim}
254 // Decimal literal
0254 // Decimal literal
0b11111110 // Binary literal
0o376 // Octal literal
0xFE // Hexadecimal literal
0xfe // Hexadecimal literal
\end{verbatim}
Numeric literals represent finite bit sequences (i.e., they have type
\texttt{{[}n{]}}). Using binary, octal, and hexadecimal notation results
in bit sequences of a fixed length, depending on the number of digits in
the literal. Decimal literals are overloaded, and so the length of the
sequence is inferred from context in which the literal is used.
Examples:
\begin{verbatim}
0b1010 // : [4], 1 * number of digits
0o1234 // : [12], 3 * number of digits
0x1234 // : [16], 4 * number of digits
10 // : {n}. (fin n, n >= 4) => [n]
// (need at least 4 bits)
0 // : {n}. (fin n) => [n]
\end{verbatim}
\section{Bits}\label{bits}
The type \texttt{Bit} has two inhabitants: \texttt{True} and
\texttt{False}. These values may be combined using various logical
operators, or constructed as results of comparisons.
\begin{longtable}[c]{@{}lll@{}}
\toprule\addlinespace
Operator & Associativity & Description
\\\addlinespace
\midrule\endhead
\texttt{\textbar{}\textbar{}} & left & Logical or
\\\addlinespace
\texttt{\^{}} & left & Exclusive-or
\\\addlinespace
\texttt{\&\&} & left & Logical and
\\\addlinespace
\texttt{!=} \texttt{==} & none & Not equals, equals
\\\addlinespace
\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=}
\texttt{\textgreater{}=} & none & Comparisons
\\\addlinespace
\texttt{\textasciitilde{}} & right & Logical negation
\\\addlinespace
\bottomrule
\addlinespace
\caption{Bit operations.}
\end{longtable}
\section{If Then Else with Multiway}\label{if-then-else-with-multiway}
\texttt{If then else} has been extended to support multi-way
conditionals. Examples:
\begin{verbatim}
x = if y % 2 == 0 then 22 else 33
x = if y % 2 == 0 then 1
| y % 3 == 0 then 2
| y % 5 == 0 then 3
else 7
\end{verbatim}
\section{Tuples and Records}\label{tuples-and-records}
Tuples and records are used for packaging multiples values together.
Tuples are enclosed in parenthesis, while records are enclosed in
braces. The components of both tuples and records are separated by
commas. The components of tuples are expressions, while the components
of records are a label and a value separated by an equal sign. Examples:
\begin{verbatim}
(1,2,3) // A tuple with 3 component
() // A tuple with no components
{ x = 1, y = 2 } // A record with two fields, `x` and `y`
{} // A record with no fileds
\end{verbatim}
The components of tuples are identified by position, while the
components of records are identified by their label, and so the ordering
of record components is not important. Examples:
\begin{verbatim}
(1,2) == (1,2) // True
(1,2) == (2,1) // False
{ x = 1, y = 2 } == { x = 1, y = 2 } // True
{ x = 1, y = 2 } == { y = 2, x = 1 } // True
\end{verbatim}
The components of a record or a tuple may be accessed in two ways: via
pattern matching or by using explicit component selectors. Explicit
component selectors are written as follows:
\begin{verbatim}
(15, 20).1 == 15
(15, 20).2 == 20
{ x = 15, y = 20 }.x == 15
\end{verbatim}
Explicit record selectors may be used only if the program contains
sufficient type information to determine the shape of the tuple or
record. For example:
\begin{verbatim}
type T = { sign :: Bit, number :: [15] }
// Valid defintion:
// the type of the record is known.
isPositive : T -> Bit
isPositive x = x.sign
// Invalid defintion:
// insufficient type information.
badDef x = x.f
\end{verbatim}
The components of a tuple or a record may also be access by using
pattern matching. Patterns for tuples and records mirror the syntax for
constructing values: tuple patterns use parenthesis, while record
patterns use braces. Examples:
\begin{verbatim}
getFst (x,_) = x
distance2 { x = xPos, y = yPos } = xPos ^^ 2 + yPos ^^ 2
f x = fst + snd where
\end{verbatim}
\section{Sequences}\label{sequences}
A sequence is a fixed-length collection of element of the same type. The
type of a finite sequence of length \texttt{n}, with elements of type
\texttt{a} is \texttt{{[}n{]} a}. Often, a finite sequence of bits,
\texttt{{[}n{]} Bit}, is called a \emph{word}. We may abbreviate the
type \texttt{{[}n{]} Bit} as \texttt{{[}n{]}}. An infinite sequence with
elements of type \texttt{a} has type \texttt{{[}inf{]} a}, and
\texttt{{[}inf{]}} is an infinite stream of bits.
\begin{verbatim}
[e1,e2,e3] // A sequence with three elements
[t .. ] // Sequence enumerations
[t1, t2 .. ] // Step by t2 - t1
[t1 .. t3 ]
[t1, t2 .. t3 ]
[e1 ... ] // Infinite sequence starting at e1
[e1, e2 ... ] // Infinite sequence stepping by e2-e1
[ e | p11 <- e11, p12 <- e12 // Sequence comprehensions
| p21 <- e21, p22 <- e22 ]
\end{verbatim}
Note: the bounds in finite unbounded (those with ..) sequences are type
expressions, while the bounds in bounded-finite and infinite sequences
are value expressions.
\begin{longtable}[c]{@{}ll@{}}
\toprule\addlinespace
Operator & Description
\\\addlinespace
\midrule\endhead
\texttt{\#} & Sequence concatenation
\\\addlinespace
\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}} &
Shift (right,left)
\\\addlinespace
\texttt{\textgreater{}\textgreater{}\textgreater{}}
\texttt{\textless{}\textless{}\textless{}} & Rotate (right,left)
\\\addlinespace
\texttt{@} \texttt{!} & Access elements (front,back)
\\\addlinespace
\texttt{@@} \texttt{!!} & Access sub-sequence (front,back)
\\\addlinespace
\bottomrule
\addlinespace
\caption{Sequence operations.}
\end{longtable}
There are also lifted point-wise operations.
\begin{verbatim}
[p1, p2, p3, p4] // Sequence pattern
p1 # p2 // Split sequence pattern
\end{verbatim}
\section{Functions}\label{functions}
\begin{verbatim}
\p1 p2 -> e // Lambda expression
f p1 p2 = e // Function definition
\end{verbatim}
\section{Local Declarations}\label{local-declarations}
\begin{verbatim}
e where ds
\end{verbatim}
\section{Explicit Type Instantiation}\label{explicit-type-instantiation}
If \texttt{f} is a polymorphic value with type:
\begin{verbatim}
f : { tyParam }
f `{ tyParam = t }
\end{verbatim}
\section{Demoting Numeric Types to
Values}\label{demoting-numeric-types-to-values}
The value corresponding to a numeric type may be accessed using the
following notation:
\begin{verbatim}
`{t}
\end{verbatim}
Here \texttt{t} should be a type expression with numeric kind. The
resulting expression is a finite word, which is sufficiently large to
accomodate the value of the type:
\begin{verbatim}
`{t} :: {w >= width t}. [w]
\end{verbatim}
\section{Explicit Type Annotations}\label{explicit-type-annotations}
Explicit type annotations may be added on expressions, patterns, and in
argument definitions.
\begin{verbatim}
e : t
p : t
f (x : t) = ...
\end{verbatim}
\section{Type Signatures}\label{type-signatures}
\begin{verbatim}
f,g : {a,b} (fin a) => [a] b
\end{verbatim}
\section{Type Synonym Declarations}\label{type-synonym-declarations}
\begin{verbatim}
type T a b = [a] b
\end{verbatim}

11
docs/ProgrammingCryptol/appendices/grammar.tex
View File

@ -1,15 +1,16 @@
\chapter{The Cryptol Syntax and Grammar}
\label{cha:crypt-synt-gramm}
\chapter{Cryptol Syntax}
\label{cha:crypt-synt}
\todo[inline]{To be written or, preferably, generated.}
%=====================================================================
\section{A Cryptol syntax summary}
\label{sec:crypt-synt-summ}
\input{appendices/Syntax.tex}
%=====================================================================
\section{The Cryptol Grammar}
\label{sec:cryptol-grammar}
\chapter{The Cryptol Grammar}
\label{cha:cryptol-grammar}
%% \input{appendices/CryptolEBNF.tex}
%%% Local Variables:
%%% mode: latex

16
docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
View File

@ -624,7 +624,7 @@ Try the following infinite enumerations:
by putting $\ldots$ at the end\footnote{You can change this behavior
by setting the {\tt infLength} variable, like so: {\tt Cryptol>
:set infLength=10} will show the first 10 elements of infinite
lists}. Here are the responses:
sequences}. Here are the responses:
\begin{Verbatim}
[1, 2, 3, 4, 5, ...]
[1, 3, 5, 7, 9, ...]
@ -789,7 +789,7 @@ and finally the shape description. In this case, Cryptol's {\tt
[b][c][a]} is telling us that the result will be a sequence of {\tt
b} things, each of which is a sequence of {\tt c} things, each of
which is a word of size {\tt a}. The type constraints tell us that
{\tt a} is at least 4, because the maximum element of the list is 12,
{\tt a} is at least 4, because the maximum element of the sequence is 12,
and it takes at least 4 bits to represent the value 12. The
constraints are that {\tt b * c == 12}, which means we should
completely cover the entire input, and that the lengths {\tt a} and
@ -1512,7 +1512,7 @@ as opposed to {\tt [0, 1, 0, 1, 0 ..]}, as one might
expect\footnote{This is one of the subtle changes from Cryptol 1. The
previous behavior can be achieved by dropping the first element from
{\tt [1 ... ]}.}. This behavior follows from the specification that
the width of the elements of the list are derived from the width of
the width of the elements of the sequence are derived from the width of
the elements in the seed, which in this case is 0.
\end{Answer}
@ -1580,11 +1580,11 @@ like. So, you can talk about 2-bit quantities {\tt [2]}, as well as
depending on the needs of your application. When we want to be
explicit about the type of a value, we say {\tt 5:[8]}. If we do not
specify a size, Cryptol's type inference engine will pick the
``appropriate'' value depending on the context.\indTypeInference
appropriate value depending on the context.\indTypeInference
Recall from Section~\ref{sec:words2} that a word is, in fact, a
sequence of bits. Hence, an equivalent (but verbose) way to write the
type {\tt [17]} is {\tt [1][17]Bit}, which we would say in English as
``a list of length one, whose element size is 17 bits long.''
type {\tt [17]} is {\tt [17]Bit}, which we would say in English as
``a sequence of length 17, whose elements are Bits.''
\paragraph*{Tuples}\indTheTupleType A tuple is a heterogeneous
collection of arbitrary number of
@ -1836,7 +1836,7 @@ the Cryptol primitive {\tt take}\indTake:
The type of {\tt take} says that it is parameterized over {\tt front}
and {\tt back}, {\tt front} must be a finite value,\indFin it takes a
list {\tt front + back} long, and returns a list {\tt front} long.
sequence {\tt front + back} long, and returns a sequence {\tt front} long.
The impact of this predicate shows up when we try to take more than
what is available:
@ -1876,7 +1876,7 @@ Here is another way, more direct but somewhat less satisfying:
\begin{verbatim}
{k} ((k - 128) * (k - 192) * (k - 256) == 0) => [k]
\end{verbatim}
Note that Cryptol's types do not include {\em or} predicates,
Note that Cryptol's type constraints do not include {\em or} predicates,
hence we cannot just list the possibilities in a list.
\end{Answer}

20
docs/ProgrammingCryptol/installation/Install.tex
View File

@ -255,19 +255,19 @@ aliases you have defined, along with their types.
\begin{center}
\begin{tabular*}{0.75\textwidth}[h]{c|c|l}
\hline
| \textbf{Option} | \textbf{Default value} | \textbf{Meaning} | \\
\textbf{Option} & \textbf{Default value} & \textbf{Meaning} \\
\hline
| \texttt{ascii} | \texttt{off} | \quad | \\
| \texttt{base} | \texttt{} | \quad | \\
| \texttt{debug} | \texttt{} | \quad | \\
| \texttt{infLength} | \texttt{} | \quad | \\
| \texttt{iteSolver} | \texttt{} | \todo[inline]{Talk to Brian.} | \\
| \texttt{prover} | \texttt{} | \quad | \\
| \texttt{tests} | \texttt{} | \quad | \\
| \texttt{warnDefaulting} | \texttt{} | \quad | \\
\texttt{ascii} & \texttt{off} & print sequences of bytes as a string \\
\texttt{base} & \texttt{10} & numeric base for printing words \\
\texttt{debug} & \texttt{off} & whether to print verbose debugging information \\
\texttt{infLength} & \texttt{5} & number of elements to show from an infinite sequence \\
\texttt{iteSolver} & \texttt{off} & whether \texttt{:prove} calls out for help on recursive functions \\
\texttt{prover} & \texttt{cvc4} & which SMT solver to use for \texttt{:prove} \\
\texttt{tests} & \texttt{100} & number of tests to run for \texttt{:check} \\
\texttt{warnDefaulting} & \texttt{on} & \todo[inline]{talk to Iavor} \\
\hline
\label{tab:set_options}
\end{tabular*}
\label{tab:set_options}
\end{center}
\paragraph*{Environment options}
A variety of environment options are set through the use of the

2
docs/ProgrammingCryptol/main/Cryptol.tex
View File

@ -14,6 +14,8 @@
\usepackage{graphicx}
\usepackage{lastpage}
\usepackage{makeidx}
\usepackage{longtable}
\usepackage{booktabs}
\usepackage[disable]{todonotes}
\usepackage[myheadings]{fullpage}
\usepackage{verbatim}

2198
examples/ChaChaPolyCryptolIETF.md Executable file
View File

File diff suppressed because it is too large Load Diff

2
examples/Salsa20.cry
View File

@ -3,6 +3,8 @@
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
// see http://cr.yp.to/snuffle/spec.pdf
module Salsa20 where
quarterround : [4][32] -> [4][32]

BIN
examples/doc/Salsa20_spec.pdf
View File

Binary file not shown.

7
examples/maliciousSHA/eve1.sh Executable file
View File

@ -0,0 +1,7 @@
#‘4@ ØM¦ÓTá+¸…[Gx&½ý7+îæP,uKW8¿Ø¥à²D”Q*Í6¢þ⊟2U™ª´zí‚
if [ `od -t x1 -j3 -N1 -An "${0}"` -eq "91" ]; then
echo "Cryptol";
else
echo "Galois";
fi

7
examples/maliciousSHA/eve2.sh Executable file
View File

@ -0,0 +1,7 @@
#’@ ¬˜M¦Ó¼áIp…ox&¹½7+¬®PjýKU8¿Ì­à²Fº”Q~E6¢~⊟šU™©zíâ
if [ `od -t x1 -j3 -N1 -An "${0}"` -eq "91" ]; then
echo "Cryptol";
else
echo "Galois";
fi

175
examples/maliciousSHA/malicious_SHA1.cry Executable file
View File

@ -0,0 +1,175 @@
/*
* Copyright (c) 2004, 2013-2014 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
// Description of SHA1 at http://www.itl.nist.gov/fipspubs/fip180-4.htm
/* WARNING: This file represents a collision in a malicious SHA-1. It is modified
* to take initialization as an input. This interface to SHA-1 should not
* be used. The collision presented here, description, and paper can be found
* at http://malicioussha1.github.io/
* The Malicious SHA-1 project is a joint work of
* Ange Albertini (Corkami, Germany)
* Jean-Philippe Aumasson (Kudelski Security, Switzerland)
* Maria Eichlseder (Graz University of Technology, Austria)
* Florian Mendel (Graz University of Technology, Austria)
* Martin Schlaeffer (Graz University of Technology, Austria)
*
* Research paper at http://malicioussha1.github.io/doc/malsha1.pdf
*/
malicious_sha1 msg k = malicious_sha1' rmsg k
where
rmsg = pad(join(reverse (groupBy`{8} (join (reverse eve1)))))
malicious_sha1' : {chunks} (fin chunks) => [chunks][512] -> [4][32] -> [160]
malicious_sha1' pmsg k = join (Hs!0)
where
Hs = [[0x67452301, 0xefcdab89, 0x98badcfe, 0x10325476, 0xc3d2e1f0]] #
[ malicious_block (H, split(M)) k
| H <- Hs
| M <- pmsg
]
//hexdump of file available at http://malicioussha1.github.io/pocs/eve1.sh
//when executed will print an ascii cow
eve1 = [
0x1d23, 0x911b, 0x4034, 0xd809, 0x4d10, 0xd3a6, 0xe154, 0x2b10,
0x85b8, 0x5b12, 0x7847, 0xbd26, 0x37fd, 0xee2b, 0x50e6, 0x2c08,
0x4b75, 0x5716, 0x1138, 0xd8bf, 0xe0a5, 0x44b2, 0x941a, 0x2a51,
0x36cd, 0x04a2, 0xe2fe, 0x9f8a, 0x5532, 0xaa99, 0x7ab4, 0x82ed,
0x0a0a, 0x6669, 0x5b20, 0x6020, 0x646f, 0x2d20, 0x2074, 0x3178,
0x2d20, 0x336a, 0x2d20, 0x314e, 0x2d20, 0x6e41, 0x2220, 0x7b24,
0x7d30, 0x6022, 0x2d20, 0x7165, 0x2220, 0x3139, 0x2022, 0x3b5d,
0x7420, 0x6568, 0x206e, 0x200a, 0x6520, 0x6863, 0x206f, 0x2022,
0x2020, 0x2020, 0x2020, 0x2020, 0x5f28, 0x295f, 0x6e5c, 0x2020,
0x2020, 0x2020, 0x2020, 0x2820, 0x6f6f, 0x5c29, 0x206e, 0x2f20,
0x2d2d, 0x2d2d, 0x2d2d, 0x5c2d, 0x2f5c, 0x6e5c, 0x2f20, 0x7c20,
0x2020, 0x2020, 0x7c20, 0x5c7c, 0x2a6e, 0x2020, 0x7c7c, 0x2d2d,
0x2d2d, 0x7c7c, 0x6e5c, 0x2020, 0x5e20, 0x205e, 0x2020, 0x5e20,
0x225e, 0x0a3b, 0x6c65, 0x6573, 0x200a, 0x6520, 0x6863, 0x206f,
0x4822, 0x6c65, 0x6f6c, 0x5720, 0x726f, 0x646c, 0x222e, 0x0a3b,
0x6966, 0x000a]
//hexdump of file available at http://malicioussha1.github.io/pocs/eve2.sh
//when executed will print "hello world"
//The ascii cow and hello world can be switched out in both files
//and the hashes will still collide. The next example shows this
eve2 = [
0x1d23, 0x921b, 0x4014, 0xac09, 0x4d98, 0xd3a6, 0xe1bc, 0x4910,
0x8570, 0x1812, 0x786f, 0xb926, 0x37bd, 0xac2b, 0x50ae, 0x6a08,
0x4bfd, 0x5516, 0x1138, 0xccbf, 0xe0ad, 0x46b2, 0x94ba, 0x7e51,
0x3645, 0x06a2, 0xe27e, 0x9f8a, 0x559a, 0xa999, 0x7a1c, 0xe2ed,
0x0a0a, 0x6669, 0x5b20, 0x6020, 0x646f, 0x2d20, 0x2074, 0x3178,
0x2d20, 0x336a, 0x2d20, 0x314e, 0x2d20, 0x6e41, 0x2220, 0x7b24,
0x7d30, 0x6022, 0x2d20, 0x7165, 0x2220, 0x3139, 0x2022, 0x3b5d,
0x7420, 0x6568, 0x206e, 0x200a, 0x6520, 0x6863, 0x206f, 0x2022,
0x2020, 0x2020, 0x2020, 0x2020, 0x5f28, 0x295f, 0x6e5c, 0x2020,
0x2020, 0x2020, 0x2020, 0x2820, 0x6f6f, 0x5c29, 0x206e, 0x2f20,
0x2d2d, 0x2d2d, 0x2d2d, 0x5c2d, 0x2f5c, 0x6e5c, 0x2f20, 0x7c20,
0x2020, 0x2020, 0x7c20, 0x5c7c, 0x2a6e, 0x2020, 0x7c7c, 0x2d2d,
0x2d2d, 0x7c7c, 0x6e5c, 0x2020, 0x5e20, 0x205e, 0x2020, 0x5e20,
0x225e, 0x0a3b, 0x6c65, 0x6573, 0x200a, 0x6520, 0x6863, 0x206f,
0x4822, 0x6c65, 0x6f6c, 0x5720, 0x726f, 0x646c, 0x222e, 0x0a3b,
0x6966, 0x000a]
//K from proof-of-concept section of http://malicioussha1.github.io/#downloads
malicious_k1 = [0x5a827999, 0x88e8ea68, 0x578059de, 0x54324a39]
bad_sha_eve1 = malicious_sha1 eve1 malicious_k1
bad_sha_eve2 = malicious_sha1 eve2 malicious_k1
property malicious_sha1_collision1 = eve1 != eve2 && bad_sha_eve1 == bad_sha_eve2
//hexdump malicious/eve1.sh
eve1_galois = [
0x1d23, 0x911b, 0x4034, 0xd809, 0x4d10, 0xd3a6, 0xe154, 0x2b10,
0x85b8, 0x5b12, 0x7847, 0xbd26, 0x37fd, 0xee2b, 0x50e6, 0x2c08,
0x4b75, 0x5716, 0x1138, 0xd8bf, 0xe0a5, 0x44b2, 0x941a, 0x2a51,
0x36cd, 0x04a2, 0xe2fe, 0x9f8a, 0x5532, 0xaa99, 0x7ab4, 0x82ed,
0x0a0a, 0x6669, 0x5b20, 0x6020, 0x646f, 0x2d20, 0x2074, 0x3178,
0x2d20, 0x336a, 0x2d20, 0x314e, 0x2d20, 0x6e41, 0x2220, 0x7b24,
0x7d30, 0x6022, 0x2d20, 0x7165, 0x2220, 0x3139, 0x2022, 0x3b5d,
0x7420, 0x6568, 0x206e, 0x200a, 0x6520, 0x6863, 0x206f, 0x4322,
0x7972, 0x7470, 0x6c6f, 0x3b22, 0x650a, 0x736c, 0x0a65, 0x2020,
0x6365, 0x6f68, 0x2220, 0x6147, 0x6f6c, 0x7369, 0x3b22, 0x660a,
0x0a69]
//hexdump malicious/eve1.sh
eve2_galois = [
0x1d23, 0x921b, 0x4014, 0xac09, 0x4d98, 0xd3a6, 0xe1bc, 0x4910,
0x8570, 0x1812, 0x786f, 0xb926, 0x37bd, 0xac2b, 0x50ae, 0x6a08,
0x4bfd, 0x5516, 0x1138, 0xccbf, 0xe0ad, 0x46b2, 0x94ba, 0x7e51,
0x3645, 0x06a2, 0xe27e, 0x9f8a, 0x559a, 0xa999, 0x7a1c, 0xe2ed,
0x0a0a, 0x6669, 0x5b20, 0x6020, 0x646f, 0x2d20, 0x2074, 0x3178,
0x2d20, 0x336a, 0x2d20, 0x314e, 0x2d20, 0x6e41, 0x2220, 0x7b24,
0x7d30, 0x6022, 0x2d20, 0x7165, 0x2220, 0x3139, 0x2022, 0x3b5d,
0x7420, 0x6568, 0x206e, 0x200a, 0x6520, 0x6863, 0x206f, 0x4322,
0x7972, 0x7470, 0x6c6f, 0x3b22, 0x650a, 0x736c, 0x0a65, 0x2020,
0x6365, 0x6f68, 0x2220, 0x6147, 0x6f6c, 0x7369, 0x3b22, 0x660a,
0x0a69]
bad_sha_eve_galois1 = malicious_sha1 eve1_galois malicious_k1
bad_sha_eve_galois2 = malicious_sha1 eve2_galois malicious_k1
property malicious_sha1_collision2 = eve1_galois != eve2_galois && bad_sha_eve_galois1 == bad_sha_eve_galois2
property all_same_hashes = bad_sha_eve_galois1 == bad_sha_eve1 && malicious_sha1_collision1 && malicious_sha1_collision2
/*
As a summary, a "1" followed by m "0"s followed by a 64-
bit integer are appended to the end of the message to produce a
padded message of length 512 * n. The 64-bit integer is the length
of the original message. The padded message is then processed by the
SHA-1 as n 512-bit blocks.
*/
pad : {msgLen,contentLen,chunks,padding}
( fin msgLen
, 64 >= width msgLen // message width fits in a word
, contentLen == msgLen + 65 // message + header
, chunks == (contentLen+511) / 512
, padding == (512 - contentLen % 512) % 512 // prettier if type #'s could be < 0
, msgLen == 512 * chunks - (65 + padding) // redundant, but Cryptol can't yet do the math
)
=> [msgLen] -> [chunks][512]
pad msg = split (msg # [True] # (zero:[padding]) # (`msgLen:[64]))
f : ([8], [32], [32], [32]) -> [32]
f (t, x, y, z) =
if (0 <= t) && (t <= 19) then (x && y) ^ (~x && z)
| (20 <= t) && (t <= 39) then x ^ y ^ z
| (40 <= t) && (t <= 59) then (x && y) ^ (x && z) ^ (y && z)
| (60 <= t) && (t <= 79) then x ^ y ^ z
else error "f: t out of range"
Ks : [4][32] -> [80][32]
Ks k = [ k@0 | t <- [0..19] ]
# [ k@1 | t <- [20..39] ]
# [ k@2 | t <- [40..59] ]
# [ k@3 | t <- [60..79] ]
malicious_block : ([5][32], [16][32]) -> [4][32]-> [5][32]
malicious_block ([H0, H1, H2, H3, H4], M) k =
[(H0+As@80), (H1+Bs@80), (H2+Cs@80), (H3+Ds@80), (H4+Es@80)]
where
Ws : [80][32]
Ws = M # [ (W3 ^ W8 ^ W14 ^ W16) <<< 1
| W16 <- drop`{16 - 16} Ws
| W14 <- drop`{16 - 14} Ws
| W8 <- drop`{16 - 8} Ws
| W3 <- drop`{16 - 3} Ws
| t <- [16..79]
]
As = [H0] # TEMP
Bs = [H1] # As
Cs = [H2] # [ B <<< 30 | B <- Bs ]
Ds = [H3] # Cs
Es = [H4] # Ds
TEMP : [80][32]
TEMP = [ (A <<< 5) + f(t, B, C, D) + E + W + K
| A <- As | B <- Bs | C <- Cs | D <- Ds | E <- Es
| W <- Ws | K <- (Ks k)
| t <- [0..79]
]

193
sbv/Data/SBV.hs
View File

@ -40,7 +40,7 @@
--
-- * 'SInt8', 'SInt16', 'SInt32', 'SInt64': Symbolic Ints (signed).
--
-- * 'SArray', 'SFunArray': Flat arrays of symbolic values.
-- * 'SInteger': Unbounded signed integers.
--
-- * 'SReal': Algebraic-real numbers
--
@ -48,6 +48,8 @@
--
-- * 'SDouble': IEEE-754 double-precision floating point values
--
-- * 'SArray', 'SFunArray': Flat arrays of symbolic values.
--
-- * Symbolic polynomials over GF(2^n), polynomial arithmetic, and CRCs.
--
-- * Uninterpreted constants and functions over symbolic values, with user
@ -92,10 +94,18 @@
--
-- * Boolector from Johannes Kepler University: <http://fmv.jku.at/boolector/>
--
-- * MathSAT from Fondazione Bruno Kessler and DISI-University of Trento: <http://mathsat.fbk.eu/>
--
-- SBV also allows calling these solvers in parallel, either getting results from multiple solvers
-- or returning the fastest one. (See 'proveWithAll', 'proveWithAny', etc.)
--
-- Support for other compliant solvers can be added relatively easily, please
-- get in touch if there is a solver you'd like to see included.
---------------------------------------------------------------------------------
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverlappingInstances #-}
module Data.SBV (
-- * Programming with symbolic values
-- $progIntro
@ -113,7 +123,7 @@ module Data.SBV (
, SInteger
-- *** IEEE-floating point numbers
-- $floatingPoints
, SFloat, SDouble, RoundingMode(..), nan, infinity, sNaN, sInfinity, fusedMA
, SFloat, SDouble, RoundingMode(..), nan, infinity, sNaN, sInfinity, fusedMA, isSNaN, isFPPoint
-- *** Signed algebraic reals
-- $algReals
, SReal, AlgReal, toSReal
@ -173,10 +183,8 @@ module Data.SBV (
, Predicate, Provable(..), Equality(..)
-- ** Proving properties
, prove, proveWith, isTheorem, isTheoremWith
, internalProveWith, internalIsTheoremWith, internalIsTheorem
-- ** Checking satisfiability
, sat, satWith, isSatisfiable, isSatisfiableWith
, internalSatWith, internalIsSatisfiable, internalIsSatisfiableWith
-- ** Finding all satisfying assignments
, allSat, allSatWith
-- ** Satisfying a sequence of boolean conditions
@ -187,6 +195,10 @@ module Data.SBV (
-- ** Checking constraint vacuity
, isVacuous, isVacuousWith
-- * Proving properties using multiple solvers
-- $multiIntro
, proveWithAll, proveWithAny, satWithAll, satWithAny, allSatWithAll, allSatWithAny
-- * Optimization
-- $optimizeIntro
, minimize, maximize, optimize
@ -205,9 +217,10 @@ module Data.SBV (
-- ** Programmable model extraction
-- $programmableExtraction
, SatModel(..), Modelable(..), displayModels, extractModels
, getModelDictionaries, getModelValues, getModelUninterpretedValues
-- * SMT Interface: Configurations and solvers
, SMTConfig(..), OptimizeOpts(..), SMTSolver(..), boolector, cvc4, yices, z3, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation
, SMTConfig(..), SMTLibLogic(..), Logic(..), OptimizeOpts(..), Solver(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers
-- * Symbolic computations
, Symbolic, output, SymWord(..)
@ -253,6 +266,10 @@ module Data.SBV (
, module Data.Ratio
) where
import Control.Monad (filterM)
import Control.Concurrent.Async (async, waitAny, waitAnyCancel)
import System.IO.Unsafe (unsafeInterleaveIO) -- only used safely!
import Data.SBV.BitVectors.AlgReals
import Data.SBV.BitVectors.Data
import Data.SBV.BitVectors.Model
@ -280,6 +297,140 @@ import Data.Word
sbvCurrentSolver :: SMTConfig
sbvCurrentSolver = z3
-- | Note that the floating point value NaN does not compare equal to itself,
-- so we need a special recognizer for that. Haskell provides the isNaN predicate
-- with the `RealFrac` class, which unfortunately is not currently implementable for
-- symbolic cases. (Requires trigonometric functions etc.) Thus, we provide this
-- recognizer separately. Note that the definition simply tests equality against
-- itself, which fails for NaN. Who said equality for floating point was reflexive?
isSNaN :: (Floating a, SymWord a) => SBV a -> SBool
isSNaN x = x ./= x
-- | We call a FP number FPPoint if it is neither NaN, nor +/- infinity.
isFPPoint :: (Floating a, SymWord a) => SBV a -> SBool
isFPPoint x = x .== x -- gets rid of NaN's
&&& x .< sInfinity -- gets rid of +inf
&&& x .> -sInfinity -- gets rid of -inf
-- | Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing
-- problems with constraints, like the following:
--
-- @
-- do [x, y, z] <- sIntegers [\"x\", \"y\", \"z\"]
-- solve [x .> 5, y + z .< x]
-- @
solve :: [SBool] -> Symbolic SBool
solve = return . bAnd
-- | Check whether the given solver is installed and is ready to go. This call does a
-- simple call to the solver to ensure all is well.
sbvCheckSolverInstallation :: SMTConfig -> IO Bool
sbvCheckSolverInstallation cfg = do ThmResult r <- proveWith cfg $ \x -> (x+x) .== ((x*2) :: SWord8)
case r of
Unsatisfiable _ -> return True
_ -> return False
-- The default configs
defaultSolverConfig :: Solver -> SMTConfig
defaultSolverConfig Z3 = z3
defaultSolverConfig Yices = yices
defaultSolverConfig Boolector = boolector
defaultSolverConfig CVC4 = cvc4
defaultSolverConfig MathSAT = mathSAT
-- | Return the known available solver configs, installed on your machine.
sbvAvailableSolvers :: IO [SMTConfig]
sbvAvailableSolvers = filterM sbvCheckSolverInstallation (map defaultSolverConfig [minBound .. maxBound])
sbvWithAny :: Provable a => [SMTConfig] -> (SMTConfig -> a -> IO b) -> a -> IO (Solver, b)
sbvWithAny [] _ _ = error "SBV.withAny: No solvers given!"
sbvWithAny solvers what a = snd `fmap` (mapM try solvers >>= waitAnyCancel)
where try s = async $ what s a >>= \r -> return (name (solver s), r)
sbvWithAll :: Provable a => [SMTConfig] -> (SMTConfig -> a -> IO b) -> a -> IO [(Solver, b)]
sbvWithAll solvers what a = mapM try solvers >>= (unsafeInterleaveIO . go)
where try s = async $ what s a >>= \r -> return (name (solver s), r)
go [] = return []
go as = do (d, r) <- waitAny as
rs <- unsafeInterleaveIO $ go (filter (/= d) as)
return (r : rs)
-- | Prove a property with multiple solvers, running them in separate threads. The
-- results will be returned in the order produced.
proveWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, ThmResult)]
proveWithAll = (`sbvWithAll` proveWith)
-- | Prove a property with multiple solvers, running them in separate threads. Only
-- the result of the first one to finish will be returned, remaining threads will be killed.
proveWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, ThmResult)
proveWithAny = (`sbvWithAny` proveWith)
-- | Find a satisfying assignment to a property with multiple solvers, running them in separate threads. The
-- results will be returned in the order produced.
satWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, SatResult)]
satWithAll = (`sbvWithAll` satWith)
-- | Find a satisfying assignment to a property with multiple solvers, running them in separate threads. Only
-- the result of the first one to finish will be returned, remaining threads will be killed.
satWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, SatResult)
satWithAny = (`sbvWithAny` satWith)
-- | Find all satisfying assignments to a property with multiple solvers, running them in separate threads. Only
-- the result of the first one to finish will be returned, remaining threads will be killed.
allSatWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, AllSatResult)]
allSatWithAll = (`sbvWithAll` allSatWith)
-- | Find all satisfying assignments to a property with multiple solvers, running them in separate threads. Only
-- the result of the first one to finish will be returned, remaining threads will be killed.
allSatWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, AllSatResult)
allSatWithAny = (`sbvWithAny` allSatWith)
-- | Equality as a proof method. Allows for
-- very concise construction of equivalence proofs, which is very typical in
-- bit-precise proofs.
infix 4 ===
class Equality a where
(===) :: a -> a -> IO ThmResult
instance (SymWord a, EqSymbolic z) => Equality (SBV a -> z) where
k === l = prove $ \a -> k a .== l a
instance (SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) where
k === l = prove $ \a b -> k a b .== l a b
instance (SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) where
k === l = prove $ \a b -> k (a, b) .== l (a, b)
instance (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) where
k === l = prove $ \a b c -> k a b c .== l a b c
instance (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) where
k === l = prove $ \a b c -> k (a, b, c) .== l (a, b, c)
instance (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) where
k === l = prove $ \a b c d -> k a b c d .== l a b c d
instance (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) where
k === l = prove $ \a b c d -> k (a, b, c, d) .== l (a, b, c, d)
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) where
k === l = prove $ \a b c d e -> k a b c d e .== l a b c d e
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) where
k === l = prove $ \a b c d e -> k (a, b, c, d, e) .== l (a, b, c, d, e)
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) where
k === l = prove $ \a b c d e f -> k a b c d e f .== l a b c d e f
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) where
k === l = prove $ \a b c d e f -> k (a, b, c, d, e, f) .== l (a, b, c, d, e, f)
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) where
k === l = prove $ \a b c d e f g -> k a b c d e f g .== l a b c d e f g
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) where
k === l = prove $ \a b c d e f g -> k (a, b, c, d, e, f, g) .== l (a, b, c, d, e, f, g)
-- Haddock section documentation
{- $progIntro
The SBV library is really two things:
@ -309,12 +460,32 @@ design goal is to let SMT solvers be used without any knowledge of how SMT solve
or how different logics operate. The details are hidden behind the SBV framework, providing
Haskell programmers with a clean API that is unencumbered by the details of individual solvers.
To that end, we use the SMT-Lib standard (<http://goedel.cs.uiowa.edu/smtlib/>)
to communicate with arbitrary SMT solvers. Unfortunately,
the SMT-Lib version 1.X does not standardize how models are communicated back from solvers, so
there is some work in parsing individual SMT solver output. The 2.X version of the SMT-Lib
standard (not yet implemented by SMT solvers widely, unfortunately) will bring new standard features
for getting models; at which time the SBV framework can be modified into a truly plug-and-play
system where arbitrary SMT solvers can be used.
to communicate with arbitrary SMT solvers.
-}
{- $multiIntro
On a multi-core machine, it might be desirable to try a given property using multiple SMT solvers,
using parallel threads. Even with machines with single-cores, threading can be helpful if you
want to try out multiple-solvers but do not know which one would work the best
for the problem at hand ahead of time.
The functions in this section allow proving/satisfiability-checking with multiple
backends at the same time. Each function comes in two variants, one that
returns the results from all solvers, the other that returns the fastest one.
The @All@ variants, (i.e., 'proveWithAll', 'satWithAll', 'allSatWithAll') run all solvers and
return all the results. SBV internally makes sure that the result is lazily generated; so,
the order of solvers given does not matter. In other words, the order of results will follow
the order of the solvers as they finish, not as given by the user. These variants are useful when you
want to make sure multiple-solvers agree (or disagree!) on a given problem.
The @Any@ variants, (i.e., 'proveWithAny', 'satWithAny', 'allSatWithAny') will run all the solvers
in parallel, and return the results of the first one finishing. The other threads will then be killed. These variants
are useful when you do not care if the solvers produce the same result, but rather want to get the
solution as quickly as possible, taking advantage of modern many-core machines.
Note that the function 'sbvAvailableSolvers' will return all the installed solvers, which can be
used as the first argument to all these functions, if you simply want to try all available solvers on a machine.
-}
{- $optimizeIntro

2
sbv/Data/SBV/BitVectors/AlgReals.hs
View File

@ -49,7 +49,7 @@ mkPolyReal (Left (exact, str))
mkPolyReal (Right (k, coeffs))
= AlgPolyRoot (k, Polynomial (normalize coeffs)) Nothing
where normalize :: [(Integer, Integer)] -> [(Integer, Integer)]
normalize = merge . reverse . sortBy (compare `on` snd)
normalize = merge . sortBy (flip compare `on` snd)
merge [] = []
merge [x] = [x]
merge ((a, b):r@((c, d):xs))

285
sbv/Data/SBV/BitVectors/Data.hs
View File

@ -17,33 +17,36 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE NamedFieldPuns #-}
module Data.SBV.BitVectors.Data
( SBool, SWord8, SWord16, SWord32, SWord64
, SInt8, SInt16, SInt32, SInt64, SInteger, SReal, SFloat, SDouble
, nan, infinity, sNaN, sInfinity, RoundingMode(..), smtLibSquareRoot, smtLibFusedMA
, SymWord(..)
, CW(..), CWVal(..), cwSameType, cwIsBit, cwToBool, normCW
, CW(..), CWVal(..), AlgReal(..), cwSameType, cwIsBit, cwToBool
, mkConstCW ,liftCW2, mapCW, mapCW2
, SW(..), trueSW, falseSW, trueCW, falseCW
, SW(..), trueSW, falseSW, trueCW, falseCW, normCW
, SBV(..), NodeId(..), mkSymSBV, mkSymSBVWithRandom
, ArrayContext(..), ArrayInfo, SymArray(..), SFunArray(..), mkSFunArray, SArray(..), arrayUIKind
, sbvToSW, sbvToSymSW
, sbvToSW, sbvToSymSW, forceSWArg
, SBVExpr(..), newExpr
, cache, Cached, uncache, uncacheAI, HasKind(..)
, Op(..), NamedSymVar, UnintKind(..), getTableIndex, SBVPgm(..), Symbolic, runSymbolic, runSymbolic', State, inProofMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..)
, readResult, getResult
, Op(..), NamedSymVar, UnintKind(..), getTableIndex, SBVPgm(..), Symbolic, runSymbolic, runSymbolic', State, getPathCondition, extendPathCondition
, inProofMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..)
, Logic(..), SMTLibLogic(..)
, getTraceInfo, getConstraints, addConstraint
, SBVType(..), newUninterpreted, unintFnUIKind, addAxiom
, Quantifier(..), needsExistentials
, SMTLibPgm(..), SMTLibVersion(..)
, SolverCapabilities(..)
, extractSymbolicSimulationState
, SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..), getSBranchRunConfig
) where
import Control.Applicative (Applicative)
import Control.DeepSeq (NFData(..))
import Control.Applicative (Applicative)
import Control.Monad (when)
import Control.Monad.Fix (MonadFix)
import Control.Monad.Reader (MonadReader, ReaderT, ask, runReaderT)
import Control.Monad.Trans (MonadIO, liftIO)
import Data.Char (isAlpha, isAlphaNum)
@ -60,6 +63,7 @@ import qualified Data.Set as Set (Set, empty, toList, insert)
import qualified Data.Foldable as F (toList)
import qualified Data.Sequence as S (Seq, empty, (|>))
import System.Exit (ExitCode(..))
import System.Mem.StableName
import System.Random
@ -130,8 +134,8 @@ cwSameType x y = cwKind x == cwKind y
-- | Is this a bit?
cwIsBit :: CW -> Bool
cwIsBit x = case cwKind x of
KBounded False 1 -> True
_ -> False
KBool -> True
_ -> False
-- | Convert a CW to a Haskell boolean (NB. Assumes input is well-kinded)
cwToBool :: CW -> Bool
@ -152,7 +156,8 @@ normCW c@(CW (KBounded signed sz) (CWInteger v)) = c { cwVal = CWInteger norm }
normCW c = c
-- | Kind of symbolic value
data Kind = KBounded Bool Int
data Kind = KBool
| KBounded Bool Int
| KUnbounded
| KReal
| KUninterpreted String
@ -161,7 +166,7 @@ data Kind = KBounded Bool Int
deriving (Eq, Ord)
instance Show Kind where
show (KBounded False 1) = "SBool"
show KBool = "SBool"
show (KBounded False n) = "SWord" ++ show n
show (KBounded True n) = "SInt" ++ show n
show KUnbounded = "SInteger"
@ -176,6 +181,12 @@ newtype NodeId = NodeId Int deriving (Eq, Ord)
-- | A symbolic word, tracking it's signedness and size.
data SW = SW Kind NodeId deriving (Eq, Ord)
-- | Forcing an argument; this is a necessary evil to make sure all the arguments
-- to an uninterpreted function and sBranch test conditions are evaluated before called;
-- the semantics of uinterpreted functions is necessarily strict; deviating from Haskell's
forceSWArg :: SW -> IO ()
forceSWArg (SW k n) = k `seq` n `seq` return ()
-- | Quantifiers: forall or exists. Note that we allow
-- arbitrary nestings.
data Quantifier = ALL | EX deriving Eq
@ -186,19 +197,19 @@ needsExistentials = (EX `elem`)
-- | Constant False as a SW. Note that this value always occupies slot -2.
falseSW :: SW
falseSW = SW (KBounded False 1) $ NodeId (-2)
falseSW = SW KBool $ NodeId (-2)
-- | Constant False as a SW. Note that this value always occupies slot -1.
trueSW :: SW
trueSW = SW (KBounded False 1) $ NodeId (-1)
trueSW = SW KBool $ NodeId (-1)
-- | Constant False as a CW. We represent it using the integer value 0.
falseCW :: CW
falseCW = CW (KBounded False 1) (CWInteger 0)
falseCW = CW KBool (CWInteger 0)
-- | Constant True as a CW. We represent it using the integer value 1.
trueCW :: CW
trueCW = CW (KBounded False 1) (CWInteger 1)
trueCW = CW KBool (CWInteger 1)
-- | A simple type for SBV computations, used mainly for uninterpreted constants.
-- We keep track of the signedness/size of the arguments. A non-function will
@ -265,6 +276,7 @@ class HasKind a where
showType :: a -> String
-- defaults
hasSign x = case kindOf x of
KBool -> False
KBounded b _ -> b
KUnbounded -> True
KReal -> True
@ -272,13 +284,14 @@ class HasKind a where
KDouble -> True
KUninterpreted{} -> False
intSizeOf x = case kindOf x of
KBool -> error "SBV.HasKind.intSizeOf((S)Bool)"
KBounded _ s -> s
KUnbounded -> error "SBV.HasKind.intSizeOf((S)Integer)"
KReal -> error "SBV.HasKind.intSizeOf((S)Real)"
KFloat -> error "SBV.HasKind.intSizeOf((S)Float)"
KDouble -> error "SBV.HasKind.intSizeOf((S)Double)"
KUninterpreted s -> error $ "SBV.HasKind.intSizeOf: Uninterpreted sort: " ++ s
isBoolean x | KBounded False 1 <- kindOf x = True
isBoolean x | KBool{} <- kindOf x = True
| True = False
isBounded x | KBounded{} <- kindOf x = True
| True = False
@ -298,7 +311,7 @@ class HasKind a where
default kindOf :: Data a => a -> Kind
kindOf = KUninterpreted . tyconUQname . dataTypeName . dataTypeOf
instance HasKind Bool where kindOf _ = KBounded False 1
instance HasKind Bool where kindOf _ = KBool
instance HasKind Int8 where kindOf _ = KBounded True 8
instance HasKind Word8 where kindOf _ = KBounded False 8
instance HasKind Int16 where kindOf _ = KBounded True 16
@ -421,7 +434,7 @@ data UnintKind = UFun Int String | UArr Int String -- in each case, arity a
-- | Result of running a symbolic computation
data Result = Result (Set.Set Kind) -- kinds used in the program
[(String, CW)] -- quick-check counter-example information (if any)
[(String, [String])] -- uninterpreted code segments
[(String, [String])] -- uninterpeted code segments
[(Quantifier, NamedSymVar)] -- inputs (possibly existential)
[(SW, CW)] -- constants
[((Int, Kind, Kind), [SW])] -- tables (automatically constructed) (tableno, index-type, result-type) elts
@ -540,9 +553,9 @@ arrayUIKind (i, (nm, _, ctx))
external (ArrayMerge{}) = False
-- | Different means of running a symbolic piece of code
data SBVRunMode = Proof Bool -- ^ Symbolic simulation mode, for proof purposes. Bool is True if it's a sat instance
| CodeGen -- ^ Code generation mode
| Concrete StdGen -- ^ Concrete simulation mode. The StdGen is for the pConstrain acceptance in cross runs
data SBVRunMode = Proof (Bool, Maybe SMTConfig) -- ^ Symbolic simulation mode, for proof purposes. Bool is True if it's a sat instance. SMTConfig is used for 'sBranch' calls.
| CodeGen -- ^ Code generation mode
| Concrete StdGen -- ^ Concrete simulation mode. The StdGen is for the pConstrain acceptance in cross runs
-- | Is this a concrete run? (i.e., quick-check or test-generation like)
isConcreteMode :: SBVRunMode -> Bool
@ -552,6 +565,7 @@ isConcreteMode CodeGen = False
-- | The state of the symbolic interpreter
data State = State { runMode :: SBVRunMode
, pathCond :: SBool
, rStdGen :: IORef StdGen
, rCInfo :: IORef [(String, CW)]
, rctr :: IORef Int
@ -571,6 +585,14 @@ data State = State { runMode :: SBVRunMode
, rAICache :: IORef (Cache Int)
}
-- | Get the current path condition
getPathCondition :: State -> SBool
getPathCondition = pathCond
-- | Extend the path condition with the given test value.
extendPathCondition :: State -> (SBool -> SBool) -> State
extendPathCondition st f = st{pathCond = f (pathCond st)}
-- | Are we running in proof mode?
inProofMode :: State -> Bool
inProofMode s = case runMode s of
@ -578,6 +600,12 @@ inProofMode s = case runMode s of
CodeGen -> False
Concrete{} -> False
-- | If in proof mode, get the underlying configuration (used for 'sBranch')
getSBranchRunConfig :: State -> Maybe SMTConfig
getSBranchRunConfig st = case runMode st of
Proof (_, s) -> s
_ -> Nothing
-- | The "Symbolic" value. Either a constant (@Left@) or a symbolic
-- value (@Right Cached@). Note that caching is essential for making
-- sure sharing is preserved. The parameter 'a' is phantom, but is
@ -636,7 +664,7 @@ infinity = 1/0
-- | Symbolic variant of Not-A-Number. This value will inhabit both
-- 'SDouble' and 'SFloat'.
sNaN :: (Floating a, SymWord a) => SBV a
sNaN = literal nan
sNaN = literal nan
-- | Symbolic variant of infinity. This value will inhabit both
-- 'SDouble' and 'SFloat'.
@ -744,6 +772,7 @@ getTableIndex st at rt elts = do
-- | Create a constant word from an integral
mkConstCW :: Integral a => Kind -> a -> CW
mkConstCW KBool a = normCW $ CW KBool (CWInteger (toInteger a))
mkConstCW k@(KBounded{}) a = normCW $ CW k (CWInteger (toInteger a))
mkConstCW KUnbounded a = normCW $ CW KUnbounded (CWInteger (toInteger a))
mkConstCW KReal a = normCW $ CW KReal (CWAlgReal (fromInteger (toInteger a)))
@ -776,28 +805,27 @@ sbvToSW st (SBV _ (Right f)) = uncache f st
-- state of the computation, layered on top of IO for creating unique
-- references to hold onto intermediate results.
newtype Symbolic a = Symbolic (ReaderT State IO a)
deriving (Functor, Applicative, Monad, MonadFix, MonadIO, MonadReader State)
deriving (Applicative, Functor, Monad, MonadIO, MonadReader State)
-- | Create a symbolic value, based on the quantifier we have. If an explicit quantifier is given, we just use that.
-- If not, then we pick existential for SAT calls and universal for everything else.
mkSymSBV :: forall a. (Random a, SymWord a) => Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a)
mkSymSBV = mkSymSBVWithRandom randomIO
mkSymSBVWithRandom :: forall a. SymWord a =>
IO (SBV a) -> Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a)
mkSymSBVWithRandom random mbQ k mbNm = do
mkSymSBVWithRandom :: forall a. SymWord a => IO (SBV a) -> Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a)
mkSymSBVWithRandom rand mbQ k mbNm = do
st <- ask
let q = case (mbQ, runMode st) of
(Just x, _) -> x -- user given, just take it
(Nothing, Concrete{}) -> ALL -- concrete simulation, pick universal
(Nothing, Proof True) -> EX -- sat mode, pick existential
(Nothing, Proof False) -> ALL -- proof mode, pick universal
(Nothing, CodeGen) -> ALL -- code generation, pick universal
(Just x, _) -> x -- user given, just take it
(Nothing, Concrete{}) -> ALL -- concrete simulation, pick universal
(Nothing, Proof (True, _)) -> EX -- sat mode, pick existential
(Nothing, Proof (False, _)) -> ALL -- proof mode, pick universal
(Nothing, CodeGen) -> ALL -- code generation, pick universal
case runMode st of
Concrete _ | q == EX -> case mbNm of
Nothing -> error $ "Cannot quick-check in the presence of existential variables, type: " ++ showType (undefined :: SBV a)
Just nm -> error $ "Cannot quick-check in the presence of existential variable " ++ nm ++ " :: " ++ showType (undefined :: SBV a)
Concrete _ -> do v@(SBV _ (Left cw)) <- liftIO random
Concrete _ -> do v@(SBV _ (Left cw)) <- liftIO rand
liftIO $ modifyIORef (rCInfo st) ((maybe "_" id mbNm, cw):)
return v
_ -> do (sw, internalName) <- liftIO $ newSW st k
@ -868,7 +896,7 @@ addAxiom nm ax = do
-- | Run a symbolic computation in Proof mode and return a 'Result'. The boolean
-- argument indicates if this is a sat instance or not.
runSymbolic :: Bool -> Symbolic a -> IO Result
runSymbolic :: (Bool, Maybe SMTConfig) -> Symbolic a -> IO Result
runSymbolic b c = snd `fmap` runSymbolic' (Proof b) c
-- | Run a symbolic computation, and return a extra value paired up with the 'Result'
@ -894,6 +922,7 @@ runSymbolic' currentRunMode (Symbolic c) = do
Concrete g -> newIORef g
_ -> newStdGen >>= newIORef
let st = State { runMode = currentRunMode
, pathCond = SBV KBool (Left trueCW)
, rStdGen = rGen
, rCInfo = cInfo
, rctr = ctr
@ -912,34 +941,32 @@ runSymbolic' currentRunMode (Symbolic c) = do
, rAICache = aiCache
, rConstraints = cstrs
}
_ <- newConst st (mkConstCW (KBounded False 1) (0::Integer)) -- s(-2) == falseSW
_ <- newConst st (mkConstCW (KBounded False 1) (1::Integer)) -- s(-1) == trueSW
_ <- newConst st falseCW -- s(-2) == falseSW
_ <- newConst st trueCW -- s(-1) == trueSW
r <- runReaderT c st
res <- readResult st
return $ (r, res)
res <- extractSymbolicSimulationState st
return (r, res)
readResult :: State -> IO Result
readResult st = do
rpgm <- readIORef (spgm st)
inpsO <- reverse `fmap` readIORef (rinps st)
outsO <- reverse `fmap` readIORef (routs st)
let swap (a, b) = (b, a)
cmp (a, _) (b, _) = a `compare` b
cnsts <- (sortBy cmp . map swap . Map.toList) `fmap` readIORef (rconstMap st)
tbls <- (sortBy (\((x, _, _), _) ((y, _, _), _) -> x `compare` y) . map swap . Map.toList) `fmap` readIORef (rtblMap st)
arrs <- IMap.toAscList `fmap` readIORef (rArrayMap st)
unint <- Map.toList `fmap` readIORef (rUIMap st)
axs <- reverse `fmap` readIORef (raxioms st)
knds <- readIORef (rUsedKinds st)
cgMap <- Map.toList `fmap` readIORef (rCgMap st)
traceVals <- reverse `fmap` readIORef (rCInfo st)
extraCstrs <- reverse `fmap` readIORef (rConstraints st)
return $ Result knds traceVals cgMap inpsO cnsts tbls arrs unint axs rpgm extraCstrs outsO
getResult :: Symbolic Result
getResult = do
st <- ask
liftIO $ readResult st
-- | Grab the program from a running symbolic simulation state. This is useful for internal purposes, for
-- instance when implementing 'sBranch'.
extractSymbolicSimulationState :: State -> IO Result
extractSymbolicSimulationState st@State{ spgm=pgm, rinps=inps, routs=outs, rtblMap=tables, rArrayMap=arrays, rUIMap=uis, raxioms=axioms
, rUsedKinds=usedKinds, rCgMap=cgs, rCInfo=cInfo, rConstraints = cstrs} = do
SBVPgm rpgm <- readIORef pgm
inpsO <- reverse `fmap` readIORef inps
outsO <- reverse `fmap` readIORef outs
let swap (a, b) = (b, a)
cmp (a, _) (b, _) = a `compare` b
cnsts <- (sortBy cmp . map swap . Map.toList) `fmap` readIORef (rconstMap st)
tbls <- (sortBy (\((x, _, _), _) ((y, _, _), _) -> x `compare` y) . map swap . Map.toList) `fmap` readIORef tables
arrs <- IMap.toAscList `fmap` readIORef arrays
unint <- Map.toList `fmap` readIORef uis
axs <- reverse `fmap` readIORef axioms
knds <- readIORef usedKinds
cgMap <- Map.toList `fmap` readIORef cgs
traceVals <- reverse `fmap` readIORef cInfo
extraCstrs <- reverse `fmap` readIORef cstrs
return $ Result knds traceVals cgMap inpsO cnsts tbls arrs unint axs (SBVPgm rpgm) extraCstrs outsO
-------------------------------------------------------------------------------
-- * Symbolic Words
@ -1024,11 +1051,11 @@ class (HasKind a, Ord a) => SymWord a where
let k = KUninterpreted sortName
liftIO $ registerKind st k
let q = case (mbQ, runMode st) of
(Just x, _) -> x
(Nothing, Proof True) -> EX
(Nothing, Proof False) -> ALL
(Nothing, Concrete{}) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in concrete simulation mode."
(Nothing, CodeGen) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in code-generation mode."
(Just x, _) -> x
(Nothing, Proof (True, _)) -> EX
(Nothing, Proof (False, _)) -> ALL
(Nothing, Concrete{}) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in concrete simulation mode."
(Nothing, CodeGen) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in code-generation mode."
ctr <- liftIO $ incCtr st
let sw = SW k (NodeId ctr)
nm = maybe ('s':show ctr) id mbNm
@ -1264,6 +1291,55 @@ instance NFData a => NFData (SBV a) where
rnf (SBV x y) = rnf x `seq` rnf y `seq` ()
instance NFData SBVPgm
instance NFData SMTResult where
rnf (Unsatisfiable _) = ()
rnf (Satisfiable _ xs) = rnf xs `seq` ()
rnf (Unknown _ xs) = rnf xs `seq` ()
rnf (ProofError _ xs) = rnf xs `seq` ()
rnf (TimeOut _) = ()
instance NFData SMTModel where
rnf (SMTModel assocs unints uarrs) = rnf assocs `seq` rnf unints `seq` rnf uarrs `seq` ()
-- | SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the
-- user can override this choice using the 'useLogic' parameter to the configuration. This is especially handy if
-- one is experimenting with custom logics that might be supported on new solvers.
data SMTLibLogic
= AUFLIA -- ^ Formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values
| AUFLIRA -- ^ Linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value
| AUFNIRA -- ^ Formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value
| LRA -- ^ Linear formulas in linear real arithmetic
| UFLRA -- ^ Linear real arithmetic with uninterpreted sort and function symbols.
| UFNIA -- ^ Non-linear integer arithmetic with uninterpreted sort and function symbols.
| QF_ABV -- ^ Quantifier-free formulas over the theory of bitvectors and bitvector arrays
| QF_AUFBV -- ^ Quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols
| QF_AUFLIA -- ^ Quantifier-free linear formulas over the theory of integer arrays extended with free sort and function symbols
| QF_AX -- ^ Quantifier-free formulas over the theory of arrays with extensionality
| QF_BV -- ^ Quantifier-free formulas over the theory of fixed-size bitvectors
| QF_IDL -- ^ Difference Logic over the integers. Boolean combinations of inequations of the form x - y < b where x and y are integer variables and b is an integer constant
| QF_LIA -- ^ Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables
| QF_LRA -- ^ Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables.
| QF_NIA -- ^ Quantifier-free integer arithmetic.
| QF_NRA -- ^ Quantifier-free real arithmetic.
| QF_RDL -- ^ Difference Logic over the reals. In essence, Boolean combinations of inequations of the form x - y < b where x and y are real variables and b is a rational constant.
| QF_UF -- ^ Unquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols.
| QF_UFBV -- ^ Unquantified formulas over bitvectors with uninterpreted sort function and symbols.
| QF_UFIDL -- ^ Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols.
| QF_UFLIA -- ^ Unquantified linear integer arithmetic with uninterpreted sort and function symbols.
| QF_UFLRA -- ^ Unquantified linear real arithmetic with uninterpreted sort and function symbols.
| QF_UFNRA -- ^ Unquantified non-linear real arithmetic with uninterpreted sort and function symbols.
| QF_FPABV -- ^ Quantifier-free formulas over the theory of floating point numbers, arrays, and bit-vectors
| QF_FPA -- ^ Quantifier-free formulas over the theory of floating point numbers
deriving Show
-- | Chosen logic for the solver
data Logic = PredefinedLogic SMTLibLogic -- ^ Use one of the logics as defined by the standard
| CustomLogic String -- ^ Use this name for the logic
instance Show Logic where
show (PredefinedLogic l) = show l
show (CustomLogic s) = s
-- | Translation tricks needed for specific capabilities afforded by each solver
data SolverCapabilities = SolverCapabilities {
capSolverName :: String -- ^ Name of the solver
@ -1277,3 +1353,84 @@ data SolverCapabilities = SolverCapabilities {
, supportsFloats :: Bool -- ^ Does the solver support single-precision floating point numbers?
, supportsDoubles :: Bool -- ^ Does the solver support double-precision floating point numbers?
}
-- | Solver configuration. See also 'z3', 'yices', 'cvc4', 'boolector', 'mathSAT', etc. which are instantiations of this type for those solvers, with
-- reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as @z3{verbose=True}@.)
--
-- Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does
-- not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to
-- emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite
-- precision value on the screen. The field 'printRealPrec' controls the printing precision, by specifying the number of digits after
-- the decimal point. The default value is 16, but it can be set to any positive integer.
--
-- When printing, SBV will add the suffix @...@ at the and of a real-value, if the given bound is not sufficient to represent the real-value
-- exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it
-- is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation
-- of the real value is not finite, i.e., if it is not rational.
data SMTConfig = SMTConfig {
verbose :: Bool -- ^ Debug mode
, timing :: Bool -- ^ Print timing information on how long different phases took (construction, solving, etc.)
, sBranchTimeOut :: Maybe Int -- ^ How much time to give to the solver for each call of 'sBranch' check. (In seconds. Default: No limit.)
, timeOut :: Maybe Int -- ^ How much time to give to the solver. (In seconds. Default: No limit.)
, printBase :: Int -- ^ Print integral literals in this base (2, 8, and 10, and 16 are supported.)
, printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16)
, solverTweaks :: [String] -- ^ Additional lines of script to give to the solver (user specified)
, satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics.
, smtFile :: Maybe FilePath -- ^ If Just, the generated SMT script will be put in this file (for debugging purposes mostly)
, useSMTLib2 :: Bool -- ^ If True, we'll treat the solver as using SMTLib2 input format. Otherwise, SMTLib1
, solver :: SMTSolver -- ^ The actual SMT solver.
, roundingMode :: RoundingMode -- ^ Rounding mode to use for floating-point conversions
, useLogic :: Maybe Logic -- ^ If Nothing, pick automatically. Otherwise, either use the given one, or use the custom string.
}
instance Show SMTConfig where
show = show . solver
-- | A model, as returned by a solver
data SMTModel = SMTModel {
modelAssocs :: [(String, CW)] -- ^ Mapping of symbolic values to constants.
, modelArrays :: [(String, [String])] -- ^ Arrays, very crude; only works with Yices.
, modelUninterps :: [(String, [String])] -- ^ Uninterpreted funcs; very crude; only works with Yices.
}
deriving Show
-- | The result of an SMT solver call. Each constructor is tagged with
-- the 'SMTConfig' that created it so that further tools can inspect it
-- and build layers of results, if needed. For ordinary uses of the library,
-- this type should not be needed, instead use the accessor functions on
-- it. (Custom Show instances and model extractors.)
data SMTResult = Unsatisfiable SMTConfig -- ^ Unsatisfiable
| Satisfiable SMTConfig SMTModel -- ^ Satisfiable with model
| Unknown SMTConfig SMTModel -- ^ Prover returned unknown, with a potential (possibly bogus) model
| ProofError SMTConfig [String] -- ^ Prover errored out
| TimeOut SMTConfig -- ^ Computation timed out (see the 'timeout' combinator)
-- | A script, to be passed to the solver.
data SMTScript = SMTScript {
scriptBody :: String -- ^ Initial feed
, scriptModel :: Maybe String -- ^ Optional continuation script, if the result is sat
}
-- | An SMT engine
type SMTEngine = SMTConfig -> Bool -> [(Quantifier, NamedSymVar)] -> [(String, UnintKind)] -> [Either SW (SW, [SW])] -> String -> IO SMTResult
-- | Solvers that SBV is aware of
data Solver = Z3
| Yices
| Boolector
| CVC4
| MathSAT
deriving (Show, Enum, Bounded)
-- | An SMT solver
data SMTSolver = SMTSolver {
name :: Solver -- ^ The solver in use
, executable :: String -- ^ The path to its executable
, options :: [String] -- ^ Options to provide to the solver
, engine :: SMTEngine -- ^ The solver engine, responsible for interpreting solver output
, xformExitCode :: ExitCode -> ExitCode -- ^ Should we re-interpret exit codes. Most solvers behave rationally, i.e., id will do. Some (like CVC4) don't.
, capabilities :: SolverCapabilities -- ^ Various capabilities of the solver
}
instance Show SMTSolver where
show = show . name

335
sbv/Data/SBV/BitVectors/Model.hs
View File

@ -23,7 +23,7 @@
module Data.SBV.BitVectors.Model (
Mergeable(..), EqSymbolic(..), OrdSymbolic(..), SDivisible(..), Uninterpreted(..), SIntegral
, sbvTestBit, sbvPopCount, setBitTo, sbvShiftLeft, sbvShiftRight, sbvSignedShiftArithRight
, sbvRotateLeft, sbvRotateRight
, sbvRotateLeft, sbvRotateRight, mkUninterpreted
, allEqual, allDifferent, inRange, sElem, oneIf, blastBE, blastLE, fullAdder, fullMultiplier
, lsb, msb, genVar, genVar_, forall, forall_, exists, exists_
, constrain, pConstrain, sBool, sBools, sWord8, sWord8s, sWord16, sWord16s, sWord32
@ -52,6 +52,23 @@ import Data.SBV.BitVectors.AlgReals
import Data.SBV.BitVectors.Data
import Data.SBV.Utils.Boolean
import Data.SBV.Provers.Prover (isSBranchFeasibleInState)
-- The following two imports are only needed because of the doctest expressions we have. Sigh..
-- It might be a good idea to reorg some of the content to avoid this.
import Data.SBV.Provers.Prover (isVacuous, prove)
import Data.SBV.SMT.SMT (ThmResult)
-- | Newer versions of GHC (Starting with 7.8 I think), distinguishes between FiniteBits and Bits classes.
-- We should really use FiniteBitSize for SBV which would make things better. In the interim, just work
-- around pesky warnings..
ghcBitSize :: Bits a => a -> Int
#if __GLASGOW_HASKELL__ >= 708
ghcBitSize x = maybe (error "SBV.ghcBitSize: Unexpected non-finite usage!") id (bitSizeMaybe x)
#else
ghcBitSize = bitSize
#endif
noUnint :: String -> a
noUnint x = error $ "Unexpected operation called on uninterpreted value: " ++ show x
@ -76,20 +93,20 @@ liftSym2 opS _ _ _ _ _ a@(SBV k _) b
liftSym2B :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> Bool) -> (Integer -> Integer -> Bool) -> (Float -> Float -> Bool) -> (Double -> Double -> Bool) -> SBV b -> SBV b -> SBool
liftSym2B _ okCW opCR opCI opCF opCD (SBV _ (Left a)) (SBV _ (Left b)) | okCW a b = literal (liftCW2 opCR opCI opCF opCD noUnint2 a b)
liftSym2B opS _ _ _ _ _ a b = SBV (KBounded False 1) $ Right $ liftSW2 opS (KBounded False 1) a b
liftSym2B opS _ _ _ _ _ a b = SBV KBool $ Right $ liftSW2 opS KBool a b
liftSym1Bool :: (State -> Kind -> SW -> IO SW) -> (Bool -> Bool) -> SBool -> SBool
liftSym1Bool _ opC (SBV _ (Left a)) = literal $ opC $ cwToBool a
liftSym1Bool opS _ a = SBV (KBounded False 1) $ Right $ cache c
liftSym1Bool opS _ a = SBV KBool $ Right $ cache c
where c st = do sw <- sbvToSW st a
opS st (KBounded False 1) sw
opS st KBool sw
liftSym2Bool :: (State -> Kind -> SW -> SW -> IO SW) -> (Bool -> Bool -> Bool) -> SBool -> SBool -> SBool
liftSym2Bool _ opC (SBV _ (Left a)) (SBV _ (Left b)) = literal (cwToBool a `opC` cwToBool b)
liftSym2Bool opS _ a b = SBV (KBounded False 1) $ Right $ cache c
liftSym2Bool opS _ a b = SBV KBool $ Right $ cache c
where c st = do sw1 <- sbvToSW st a
sw2 <- sbvToSW st b
opS st (KBounded False 1) sw1 sw2
opS st KBool sw1 sw2
mkSymOpSC :: (SW -> SW -> Maybe SW) -> Op -> State -> Kind -> SW -> SW -> IO SW
mkSymOpSC shortCut op st k a b = maybe (newExpr st k (SBVApp op [a, b])) return (shortCut a b)
@ -128,8 +145,8 @@ genMkSymVar k mbq Nothing = genVar_ mbq k
genMkSymVar k mbq (Just s) = genVar mbq k s
instance SymWord Bool where
mkSymWord = genMkSymVar (KBounded False 1)
literal x = genLiteral (KBounded False 1) (if x then (1::Integer) else 0)
mkSymWord = genMkSymVar KBool
literal x = genLiteral KBool (if x then (1::Integer) else 0)
fromCW = cwToBool
mbMaxBound = Just maxBound
mbMinBound = Just minBound
@ -755,10 +772,12 @@ instance ({-Num a,-} Bits a, SymWord a) => Bits (SBV a) where
| True = liftSym2 (mkSymOp XOr) (const (const True)) (noReal "xor") xor (noFloat "xor") (noDouble "xor") x y
complement = liftSym1 (mkSymOp1 Not) (noRealUnary "complement") complement (noFloatUnary "complement") (noDoubleUnary "complement")
bitSize x = case kindOf x of KBounded _ w -> w
#if __GLASGOW_HASKELL__ >= 708
bitSizeMaybe _ = Just $ intSizeOf (undefined :: a)
#endif
isSigned x = case kindOf x of KBounded s _ -> s
bit i = 1 `shiftL` i
setBit x i = x .|. sbvFromInteger (kindOf x) (bit i)
--BH TODO: implement setBit, clearBit, etc. separately.
shiftL x y
| y < 0 = shiftR x (-y)
| y == 0 = x
@ -770,12 +789,12 @@ instance ({-Num a,-} Bits a, SymWord a) => Bits (SBV a) where
rotateL x y
| y < 0 = rotateR x (-y)
| y == 0 = x
| isBounded x = let sz = bitSize x in liftSym1 (mkSymOp1 (Rol (y `mod` sz))) (noRealUnary "rotateL") (rot True sz y) (noFloatUnary "rotateL") (noDoubleUnary "rotateL") x
| isBounded x = let sz = ghcBitSize x in liftSym1 (mkSymOp1 (Rol (y `mod` sz))) (noRealUnary "rotateL") (rot True sz y) (noFloatUnary "rotateL") (noDoubleUnary "rotateL") x
| True = shiftL x y -- for unbounded Integers, rotateL is the same as shiftL in Haskell
rotateR x y
| y < 0 = rotateL x (-y)
| y == 0 = x
| isBounded x = let sz = bitSize x in liftSym1 (mkSymOp1 (Ror (y `mod` sz))) (noRealUnary "rotateR") (rot False sz y) (noFloatUnary "rotateR") (noDoubleUnary "rotateR") x
| isBounded x = let sz = ghcBitSize x in liftSym1 (mkSymOp1 (Ror (y `mod` sz))) (noRealUnary "rotateR") (rot False sz y) (noFloatUnary "rotateR") (noDoubleUnary "rotateR") x
| True = shiftR x y -- for unbounded integers, rotateR is the same as shiftR in Haskell
-- NB. testBit is *not* implementable on non-concrete symbolic words
x `testBit` i
@ -835,7 +854,7 @@ setBitTo x i b = ite b (setBit x i) (clearBit x i)
sbvShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
sbvShiftLeft x i
| isSigned i = error "sbvShiftLeft: shift amount should be unsigned"
| True = select [x `shiftL` k | k <- [0 .. bitSize x - 1]] z i
| True = select [x `shiftL` k | k <- [0 .. ghcBitSize x - 1]] z i
where z = sbvFromInteger (kindOf x) 0
-- | Generalization of 'shiftR', when the shift-amount is symbolic. Since Haskell's
@ -848,7 +867,7 @@ sbvShiftLeft x i
sbvShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
sbvShiftRight x i
| isSigned i = error "sbvShiftRight: shift amount should be unsigned"
| True = select [x `shiftR` k | k <- [0 .. bitSize x - 1]] z i
| True = select [x `shiftR` k | k <- [0 .. ghcBitSize x - 1]] z i
where z = sbvFromInteger (kindOf x) 0
-- | Arithmetic shift-right with a symbolic unsigned shift amount. This is equivalent
@ -870,7 +889,7 @@ sbvSignedShiftArithRight x i
sbvRotateLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
sbvRotateLeft x i
| isSigned i = error "sbvRotateLeft: shift amount should be unsigned"
| True = select [x `rotateL` k | k <- [0 .. bitSize x - 1]] z i
| True = select [x `rotateL` k | k <- [0 .. ghcBitSize x - 1]] z i
where z = sbvFromInteger (kindOf x) 0
-- | Generalization of 'rotateR', when the shift-amount is symbolic. Since Haskell's
@ -879,7 +898,7 @@ sbvRotateLeft x i
sbvRotateRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
sbvRotateRight x i
| isSigned i = error "sbvRotateRight: shift amount should be unsigned"
| True = select [x `rotateR` k | k <- [0 .. bitSize x - 1]] z i
| True = select [x `rotateR` k | k <- [0 .. ghcBitSize x - 1]] z i
where z = sbvFromInteger (kindOf x) 0
-- | Full adder. Returns the carry-out from the addition.
@ -902,14 +921,14 @@ fullAdder a b
fullMultiplier :: SIntegral a => SBV a -> SBV a -> (SBV a, SBV a)
fullMultiplier a b
| isSigned a = error "fullMultiplier: only works on unsigned numbers"
| True = (go (bitSize a) 0 a, a*b)
| True = (go (ghcBitSize a) 0 a, a*b)
where go 0 p _ = p
go n p x = let (c, p') = ite (lsb x) (fullAdder p b) (false, p)
(o, p'') = shiftIn c p'
(_, x') = shiftIn o x
in go (n-1) p'' x'
shiftIn k v = (lsb v, mask .|. (v `shiftR` 1))
where mask = ite k (bit (bitSize v - 1)) 0
where mask = ite k (bit (ghcBitSize v - 1)) 0
-- | Little-endian blasting of a word into its bits. Also see the 'FromBits' class.
blastLE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool]
@ -1071,12 +1090,11 @@ instance SDivisible Integer where
instance SDivisible CW where
sQuotRem a b
| CWInteger x <- cwVal a, CWInteger y <- cwVal b
= let (r1, r2) = sQuotRem x y in (a { cwVal = CWInteger r1 }, b { cwVal = CWInteger r2 })
--BH FIXME: -2^(n-1) `div` (-1) can overflow.
= let (r1, r2) = sQuotRem x y in (normCW a{ cwVal = CWInteger r1 }, normCW b{ cwVal = CWInteger r2 })
sQuotRem a b = error $ "SBV.sQuotRem: impossible, unexpected args received: " ++ show (a, b)
sDivMod a b
| CWInteger x <- cwVal a, CWInteger y <- cwVal b
= let (r1, r2) = sDivMod x y in (a { cwVal = CWInteger r1 }, b { cwVal = CWInteger r2 })
= let (r1, r2) = sDivMod x y in (normCW a { cwVal = CWInteger r1 }, normCW b { cwVal = CWInteger r2 })
sDivMod a b = error $ "SBV.sDivMod: impossible, unexpected args received: " ++ show (a, b)
instance SDivisible SWord64 where
@ -1177,6 +1195,24 @@ class Mergeable a where
-- The idea is that use symbolicMerge if you know the condition is symbolic,
-- otherwise use ite, if there's a chance it might be concrete.
ite :: SBool -> a -> a -> a
-- | Branch on a condition, much like 'ite'. The exception is that SBV will
-- check to make sure if the test condition is feasible by making an external
-- call to the SMT solver. Note that this can be expensive, thus we shall use
-- a time-out value ('sBranchTimeOut'). There might be zero, one, or two such
-- external calls per 'sBranch' call:
--
-- - If condition is statically known to be True/False: 0 calls
-- - In this case, we simply constant fold..
--
-- - If condition is determined to be unsatisfiable : 1 call
-- - In this case, we know then-branch is infeasible, so just take the else-branch
--
-- - If condition is determined to be satisfable : 2 calls
-- - In this case, we know then-branch is feasible, but we still have to check if the else-branch is
--
-- In summary, 'sBranch' calls can be expensive, but they can help with the so-called symbolic-termination
-- problem. See "Data.SBV.Examples.Misc.SBranch" for an example.
sBranch :: SBool -> a -> a -> a
-- | Total indexing operation. @select xs default index@ is intuitively
-- the same as @xs !! index@, except it evaluates to @default@ if @index@
-- overflows
@ -1185,6 +1221,7 @@ class Mergeable a where
ite s a b
| Just t <- unliteral s = if t then a else b
| True = symbolicMerge s a b
sBranch s = ite (reduceInPathCondition s)
-- NB. Earlier implementation of select used the binary-search trick
-- on the index to chop down the search space. While that is a good trick
-- in general, it doesn't work for SBV since we do not have any notion of
@ -1200,86 +1237,14 @@ class Mergeable a where
-- SBV
instance SymWord a => Mergeable (SBV a) where
-- the strict match and checking of literal equivalence is essential below,
-- as otherwise we risk hanging onto huge closures and blow stack! This is
-- against the feel that merging shouldn't look at branches if the test
-- expression is constant. However, it's OK to do it this way since we
-- expect "ite" to be used in such cases which already checks for that. That
-- is the use case of the symbolicMerge should be when the test is symbolic.
-- Of course, we do not have a way of enforcing that in the user code, but
-- at least our library code respects that invariant.
symbolicMerge t a@(SBV{}) b@(SBV{})
| Just av <- unliteral a, Just bv <- unliteral b, rationalSBVCheck a b, av == bv
= a
| True
= SBV k $ Right $ cache c
where k = kindOf a
c st = do swt <- sbvToSW st t
case () of
() | swt == trueSW -> sbvToSW st a -- these two cases should never be needed as we expect symbolicMerge to be
() | swt == falseSW -> sbvToSW st b -- called with symbolic tests, but just in case..
() -> do {- It is tempting to record the choice of the test expression here as we branch down to the 'then' and 'else' branches. That is,
when we evaluate 'a', we can make use of the fact that the test expression is True, and similarly we can use the fact that it
is False when b is evaluated. In certain cases this can cut down on symbolic simulation significantly, for instance if
repetitive decisions are made in a recursive loop. Unfortunately, the implementation of this idea is quite tricky, due to
our sharing based implementation. As the 'then' branch is evaluated, we will create many expressions that are likely going
to be "reused" when the 'else' branch is executed. But, it would be *dead wrong* to share those values, as they were "cached"
under the incorrect assumptions. To wit, consider the following:
foo x y = ite (y .== 0) k (k+1)
where k = ite (y .== 0) x (x+1)
When we reduce the 'then' branch of the first ite, we'd record the assumption that y is 0. But while reducing the 'then' branch, we'd
like to share 'k', which would evaluate (correctly) to 'x' under the given assumption. When we backtrack and evaluate the 'else'
branch of the first ite, we'd see 'k' is needed again, and we'd look it up from our sharing map to find (incorrectly) that its value
is 'x', which was stored there under the assumption that y was 0, which no longer holds. Clearly, this is unsound.
A sound implementation would have to precisely track which assumptions were active at the time expressions get shared. That is,
in the above example, we should record that the value of 'k' was cached under the assumption that 'y' is 0. While sound, this
approach unfortunately leads to significant loss of valid sharing when the value itself had nothing to do with the assumption itself.
To wit, consider:
foo x y = ite (y .== 0) k (k+1)
where k = x+5
If we tracked the assumptions, we would recompute 'k' twice, since the branch assumptions would differ. Clearly, there is no need to
re-compute 'k' in this case since its value is independent of y. Note that the whole SBV performance story is based on agressive sharing,
and losing that would have other significant ramifications.
The "proper" solution would be to track, with each shared computation, precisely which assumptions it actually *depends* on, rather
than blindly recording all the assumptions present at that time. SBV's symbolic simulation engine clearly has all the info needed to do this
properly, but the implementation is not straightforward at all. For each subexpression, we would need to chase down its dependencies
transitively, which can require a lot of scanning of the generated program causing major slow-down; thus potentially defeating the
whole purpose of sharing in the first place.
Design choice: Keep it simple, and simply do not track the assumption at all. This will maximize sharing, at the cost of evaluating
unreachable branches. I think the simplicity is more important at this point than efficiency.
Also note that the user can avoid most such issues by properly combining if-then-else's with common conditions together. That is, the
first program above should be written like this:
foo x y = ite (y .== 0) x (x+2)
In general, the following transformations should be done whenever possible:
ite e1 (ite e1 e2 e3) e4 --> ite e1 e2 e4
ite e1 e2 (ite e1 e3 e4) --> ite e1 e2 e4
This is in accordance with the general rule-of-thumb stating conditionals should be avoided as much as possible. However, we might prefer
the following:
ite e1 (f e2 e4) (f e3 e5) --> f (ite e1 e2 e3) (ite e1 e4 e5)
especially if this expression happens to be inside 'f's body itself (i.e., when f is recursive), since it reduces the number of
recursive calls. Clearly, programming with symbolic simulation in mind is another kind of beast alltogether.
-}
swa <- sbvToSW st a -- evaluate 'then' branch
swb <- sbvToSW st b -- evaluate 'else' branch
case () of -- merge:
() | swa == swb -> return swa
() | swa == trueSW && swb == falseSW -> return swt
() | swa == falseSW && swb == trueSW -> newExpr st k (SBVApp Not [swt])
() -> newExpr st k (SBVApp Ite [swt, swa, swb])
-- sBranch is essentially the default method, but we are careful in not forcing the
-- arguments as ite does, since sBranch is expected to be used when one of the
-- branches is likely to be in a branch that's recursively evaluated.
sBranch s a b
| Just t <- unliteral sReduced = if t then a else b
| True = symbolicWordMerge False sReduced a b
where sReduced = reduceInPathCondition s
symbolicMerge = symbolicWordMerge True
-- Custom version of select that translates to SMT-Lib tables at the base type of words
select xs err ind
| SBV _ (Left c) <- ind = case cwVal c of
@ -1299,6 +1264,86 @@ instance SymWord a => Mergeable (SBV a) where
let len = length xs
newExpr st kElt (SBVApp (LkUp (idx, kInd, kElt, len) swi swe) [])
-- symbolically merge two SBV words, based on the boolean condition given.
-- The first argument controls whether we want to reduce the branches
-- separately first, which avoids hanging onto huge thunks, and is usually
-- the right thing to do for ite. But we precisely do not want to do that
-- in case of sBranch, which is the case when one of the branches (typically
-- the "else" branch is hanging off of a recursive call.
symbolicWordMerge :: SymWord a => Bool -> SBool -> SBV a -> SBV a -> SBV a
symbolicWordMerge force t a b
| force, Just av <- unliteral a, Just bv <- unliteral b, rationalSBVCheck a b, av == bv
= a
| True
= SBV k $ Right $ cache c
where k = kindOf a
c st = do swt <- sbvToSW st t
case () of
() | swt == trueSW -> sbvToSW st a -- these two cases should never be needed as we expect symbolicMerge to be
() | swt == falseSW -> sbvToSW st b -- called with symbolic tests, but just in case..
() -> do {- It is tempting to record the choice of the test expression here as we branch down to the 'then' and 'else' branches. That is,
when we evaluate 'a', we can make use of the fact that the test expression is True, and similarly we can use the fact that it
is False when b is evaluated. In certain cases this can cut down on symbolic simulation significantly, for instance if
repetitive decisions are made in a recursive loop. Unfortunately, the implementation of this idea is quite tricky, due to
our sharing based implementation. As the 'then' branch is evaluated, we will create many expressions that are likely going
to be "reused" when the 'else' branch is executed. But, it would be *dead wrong* to share those values, as they were "cached"
under the incorrect assumptions. To wit, consider the following:
foo x y = ite (y .== 0) k (k+1)
where k = ite (y .== 0) x (x+1)
When we reduce the 'then' branch of the first ite, we'd record the assumption that y is 0. But while reducing the 'then' branch, we'd
like to share 'k', which would evaluate (correctly) to 'x' under the given assumption. When we backtrack and evaluate the 'else'
branch of the first ite, we'd see 'k' is needed again, and we'd look it up from our sharing map to find (incorrectly) that its value
is 'x', which was stored there under the assumption that y was 0, which no longer holds. Clearly, this is unsound.
A sound implementation would have to precisely track which assumptions were active at the time expressions get shared. That is,
in the above example, we should record that the value of 'k' was cached under the assumption that 'y' is 0. While sound, this
approach unfortunately leads to significant loss of valid sharing when the value itself had nothing to do with the assumption itself.
To wit, consider:
foo x y = ite (y .== 0) k (k+1)
where k = x+5
If we tracked the assumptions, we would recompute 'k' twice, since the branch assumptions would differ. Clearly, there is no need to
re-compute 'k' in this case since its value is independent of y. Note that the whole SBV performance story is based on agressive sharing,
and losing that would have other significant ramifications.
The "proper" solution would be to track, with each shared computation, precisely which assumptions it actually *depends* on, rather
than blindly recording all the assumptions present at that time. SBV's symbolic simulation engine clearly has all the info needed to do this
properly, but the implementation is not straightforward at all. For each subexpression, we would need to chase down its dependencies
transitively, which can require a lot of scanning of the generated program causing major slow-down; thus potentially defeating the
whole purpose of sharing in the first place.
Design choice: Keep it simple, and simply do not track the assumption at all. This will maximize sharing, at the cost of evaluating
unreachable branches. I think the simplicity is more important at this point than efficiency.
Also note that the user can avoid most such issues by properly combining if-then-else's with common conditions together. That is, the
first program above should be written like this:
foo x y = ite (y .== 0) x (x+2)
In general, the following transformations should be done whenever possible:
ite e1 (ite e1 e2 e3) e4 --> ite e1 e2 e4
ite e1 e2 (ite e1 e3 e4) --> ite e1 e2 e4
This is in accordance with the general rule-of-thumb stating conditionals should be avoided as much as possible. However, we might prefer
the following:
ite e1 (f e2 e4) (f e3 e5) --> f (ite e1 e2 e3) (ite e1 e4 e5)
especially if this expression happens to be inside 'f's body itself (i.e., when f is recursive), since it reduces the number of
recursive calls. Clearly, programming with symbolic simulation in mind is another kind of beast alltogether.
-}
swa <- sbvToSW (st `extendPathCondition` (&&& t)) a -- evaluate 'then' branch
swb <- sbvToSW (st `extendPathCondition` (&&& bnot t)) b -- evaluate 'else' branch
case () of -- merge:
() | swa == swb -> return swa
() | swa == trueSW && swb == falseSW -> return swt
() | swa == falseSW && swb == trueSW -> newExpr st k (SBVApp Not [swt])
() -> newExpr st k (SBVApp Ite [swt, swa, swb])
-- Unit
instance Mergeable () where
symbolicMerge _ _ _ = ()
@ -1400,10 +1445,10 @@ instance (SymWord a, Bounded a) => Bounded (SBV a) where
-- SArrays are both "EqSymbolic" and "Mergeable"
instance EqSymbolic (SArray a b) where
(SArray _ a) .== (SArray _ b) = SBV (KBounded False 1) $ Right $ cache c
(SArray _ a) .== (SArray _ b) = SBV KBool $ Right $ cache c
where c st = do ai <- uncacheAI a st
bi <- uncacheAI b st
newExpr st (KBounded False 1) (SBVApp (ArrEq ai bi) [])
newExpr st KBool (SBVApp (ArrEq ai bi) [])
instance SymWord b => Mergeable (SArray a b) where
symbolicMerge = mergeArrays
@ -1450,6 +1495,15 @@ class Uninterpreted a where
uninterpret = sbvUninterpret Nothing
cgUninterpret nm code v = sbvUninterpret (Just (code, v)) nm
mkUninterpreted :: [Kind] -> [SBV ()] -> String -> SBV a
mkUninterpreted ks args nm = SBV ka $ Right $ cache result where
ka = last ks
result st = do
newUninterpreted st nm (SBVType ks) Nothing
sws <- mapM (sbvToSW st) args
mapM_ forceSWArg sws
newExpr st ka $ SBVApp (Uninterpreted nm) sws
-- Plain constants
instance HasKind a => Uninterpreted (SBV a) where
sbvUninterpret mbCgData nm
@ -1460,12 +1514,6 @@ instance HasKind a => Uninterpreted (SBV a) where
| True = do newUninterpreted st nm (SBVType [ka]) (fst `fmap` mbCgData)
newExpr st ka $ SBVApp (Uninterpreted nm) []
-- Forcing an argument; this is a necessary evil to make sure all the arguments
-- to an uninterpreted function are evaluated before called; the semantics of
-- such functions is necessarily strict; deviating from Haskell's
forceArg :: SW -> IO ()
forceArg (SW k n) = k `seq` n `seq` return ()
-- Functions of one argument
instance (SymWord b, HasKind a) => Uninterpreted (SBV b -> SBV a) where
sbvUninterpret mbCgData nm = f
@ -1479,7 +1527,7 @@ instance (SymWord b, HasKind a) => Uninterpreted (SBV b -> SBV a) where
result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0)
| True = do newUninterpreted st nm (SBVType [kb, ka]) (fst `fmap` mbCgData)
sw0 <- sbvToSW st arg0
mapM_ forceArg [sw0]
mapM_ forceSWArg [sw0]
newExpr st ka $ SBVApp (Uninterpreted nm) [sw0]
-- Functions of two arguments
@ -1497,7 +1545,7 @@ instance (SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV c -> SBV b -> S
| True = do newUninterpreted st nm (SBVType [kc, kb, ka]) (fst `fmap` mbCgData)
sw0 <- sbvToSW st arg0
sw1 <- sbvToSW st arg1
mapM_ forceArg [sw0, sw1]
mapM_ forceSWArg [sw0, sw1]
newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1]
-- Functions of three arguments
@ -1517,7 +1565,7 @@ instance (SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV d ->
sw0 <- sbvToSW st arg0
sw1 <- sbvToSW st arg1
sw2 <- sbvToSW st arg2
mapM_ forceArg [sw0, sw1, sw2]
mapM_ forceSWArg [sw0, sw1, sw2]
newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2]
-- Functions of four arguments
@ -1539,7 +1587,7 @@ instance (SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterprete
sw1 <- sbvToSW st arg1
sw2 <- sbvToSW st arg2
sw3 <- sbvToSW st arg3
mapM_ forceArg [sw0, sw1, sw2, sw3]
mapM_ forceSWArg [sw0, sw1, sw2, sw3]
newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3]
-- Functions of five arguments
@ -1563,7 +1611,7 @@ instance (SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => U
sw2 <- sbvToSW st arg2
sw3 <- sbvToSW st arg3
sw4 <- sbvToSW st arg4
mapM_ forceArg [sw0, sw1, sw2, sw3, sw4]
mapM_ forceSWArg [sw0, sw1, sw2, sw3, sw4]
newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4]
-- Functions of six arguments
@ -1589,7 +1637,7 @@ instance (SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasK
sw3 <- sbvToSW st arg3
sw4 <- sbvToSW st arg4
sw5 <- sbvToSW st arg5
mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5]
mapM_ forceSWArg [sw0, sw1, sw2, sw3, sw4, sw5]
newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5]
-- Functions of seven arguments
@ -1618,7 +1666,7 @@ instance (SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymW
sw4 <- sbvToSW st arg4
sw5 <- sbvToSW st arg5
sw6 <- sbvToSW st arg6
mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6]
mapM_ forceSWArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6]
newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5, sw6]
-- Uncurried functions of two arguments
@ -1655,7 +1703,39 @@ instance (SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymW
sbvUninterpret mbCgData nm = let f = sbvUninterpret (uc7 `fmap` mbCgData) nm in \(arg0, arg1, arg2, arg3, arg4, arg5, arg6) -> f arg0 arg1 arg2 arg3 arg4 arg5 arg6
where uc7 (cs, fn) = (cs, \a b c d e f g -> fn (a, b, c, d, e, f, g))
-- | Adding arbitrary constraints.
-- | Adding arbitrary constraints. When adding constraints, one has to be careful about
-- making sure they are not inconsistent. The function 'isVacuous' can be use for this purpose.
-- Here is an example. Consider the following predicate:
--
-- >>> let pred = do { x <- forall "x"; constrain $ x .< x; return $ x .>= (5 :: SWord8) }
--
-- This predicate asserts that all 8-bit values are larger than 5, subject to the constraint that the
-- values considered satisfy @x .< x@, i.e., they are less than themselves. Since there are no values that
-- satisfy this constraint, the proof will pass vacuously:
--
-- >>> prove pred
-- Q.E.D.
--
-- We can use 'isVacuous' to make sure to see that the pass was vacuous:
--
-- >>> isVacuous pred
-- True
--
-- While the above example is trivial, things can get complicated if there are multiple constraints with
-- non-straightforward relations; so if constraints are used one should make sure to check the predicate
-- is not vacuously true. Here's an example that is not vacuous:
--
-- >>> let pred' = do { x <- forall "x"; constrain $ x .> 6; return $ x .>= (5 :: SWord8) }
--
-- This time the proof passes as expected:
--
-- >>> prove pred'
-- Q.E.D.
--
-- And the proof is not vacuous:
--
-- >>> isVacuous pred'
-- False
constrain :: SBool -> Symbolic ()
constrain c = addConstraint Nothing c (bnot c)
@ -1665,6 +1745,25 @@ constrain c = addConstraint Nothing c (bnot c)
pConstrain :: Double -> SBool -> Symbolic ()
pConstrain t c = addConstraint (Just t) c (bnot c)
-- | Boolean symbolic reduction. See if we can reduce a boolean condition to true/false
-- using the path context information, by making external calls to the SMT solvers. Used in the
-- implementation of 'sBranch'.
reduceInPathCondition :: SBool -> SBool
reduceInPathCondition b
| isConcrete b = b -- No reduction is needed, already a concrete value
| True = SBV k $ Right $ cache c
where k = kindOf b
c st = do -- Now that we know our boolean is not obviously true/false. Need to make an external
-- call to the SMT solver to see if we can prove it is necessarily one of those
let pc = getPathCondition st
satTrue <- isSBranchFeasibleInState st "then" (pc &&& b)
if not satTrue
then return falseSW -- condition is not satisfiable; so it must be necessarily False.
else do satFalse <- isSBranchFeasibleInState st "else" (pc &&& bnot b)
if not satFalse -- negation of the condition is not satisfiable; so it must be necessarily True.
then return trueSW
else sbvToSW st b -- condition is not necessarily always True/False. So, keep symbolic.
-- Quickcheck interface on symbolic-booleans..
instance Testable SBool where
property (SBV _ (Left b)) = property (cwToBool b)
@ -1703,5 +1802,9 @@ slet x f = SBV k $ Right $ cache r
res = f xsbv
sbvToSW st res
-- We use 'isVacuous' and 'prove' only for the "test" section in this file, and GHC complains about that. So, this shuts it up.
__unused :: a
__unused = error "__unused" (isVacuous :: SBool -> IO Bool) (prove :: SBool -> IO ThmResult)
{-# ANN module "HLint: ignore Eta reduce" #-}
{-# ANN module "HLint: ignore Reduce duplication" #-}

1
sbv/Data/SBV/BitVectors/PrettyNum.hs
View File

@ -27,7 +27,6 @@ import Data.Word (Word8, Word16, Word32, Word64)
import Numeric (showIntAtBase, showHex, readInt)
import Data.SBV.BitVectors.Data
import Data.SBV.BitVectors.Model () -- instances only
-- | PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers.
--

2
sbv/Data/SBV/BitVectors/SignCast.hs
View File

@ -81,6 +81,7 @@ genericSign x
| Just c <- unliteral x = literal $ fromIntegral c
| True = SBV k (Right (cache y))
where k = case kindOf x of
KBool -> error "Data.SBV.SignCast.genericSign: Called on boolean value"
KBounded False n -> KBounded True n
KBounded True _ -> error "Data.SBV.SignCast.genericSign: Called on signed value"
KUnbounded -> error "Data.SBV.SignCast.genericSign: Called on unbounded value"
@ -97,6 +98,7 @@ genericUnsign x
| Just c <- unliteral x = literal $ fromIntegral c
| True = SBV k (Right (cache y))
where k = case kindOf x of
KBool -> error "Data.SBV.SignCast.genericUnSign: Called on boolean value"
KBounded True n -> KBounded False n
KBounded False _ -> error "Data.SBV.SignCast.genericUnSign: Called on unsigned value"
KUnbounded -> error "Data.SBV.SignCast.genericUnSign: Called on unbounded value"

4
sbv/Data/SBV/Bridge/Boolector.hs
View File

@ -14,10 +14,12 @@
-- - "Data.SBV.Bridge.Z3"
--
-- - "Data.SBV.Bridge.CVC4"
--
-- - "Data.SBV.Bridge.MathSAT"
---------------------------------------------------------------------------------
module Data.SBV.Bridge.Boolector (
-- * CVC4 specific interface
-- * Boolector specific interface
sbvCurrentSolver
-- ** Proving and checking satisfiability
, prove, sat, allSat, isVacuous, isTheorem, isSatisfiable

2
sbv/Data/SBV/Bridge/CVC4.hs
View File

@ -14,6 +14,8 @@
-- - "Data.SBV.Bridge.Z3"
--
-- - "Data.SBV.Bridge.Boolector"
--
-- - "Data.SBV.Bridge.MathSAT"
---------------------------------------------------------------------------------
module Data.SBV.Bridge.CVC4 (

107
sbv/Data/SBV/Bridge/MathSAT.hs Normal file
View File

@ -0,0 +1,107 @@
---------------------------------------------------------------------------------
-- |
-- Module : Data.SBV.Bridge.MathSAT
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--
-- Interface to the MathSAT SMT solver. Import this module if you want to use the
-- MathSAT SMT prover as your backend solver. Also see:
--
-- - "Data.SBV.Bridge.Yices"
--
-- - "Data.SBV.Bridge.Z3"
--
-- - "Data.SBV.Bridge.CVC4"
--
-- - "Data.SBV.Bridge.Boolector"
---------------------------------------------------------------------------------
module Data.SBV.Bridge.MathSAT (
-- * MathSAT specific interface
sbvCurrentSolver
-- ** Proving and checking satisfiability
, prove, sat, allSat, isVacuous, isTheorem, isSatisfiable
-- ** Optimization routines
, optimize, minimize, maximize
-- * Non-MathSAT specific SBV interface
-- $moduleExportIntro
, module Data.SBV
) where
import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)
-- | Current solver instance, pointing to cvc4.
sbvCurrentSolver :: SMTConfig
sbvCurrentSolver = mathSAT
-- | Prove theorems, using the CVC4 SMT solver
prove :: Provable a
=> a -- ^ Property to check
-> IO ThmResult -- ^ Response from the SMT solver, containing the counter-example if found
prove = proveWith sbvCurrentSolver
-- | Find satisfying solutions, using the CVC4 SMT solver
sat :: Provable a
=> a -- ^ Property to check
-> IO SatResult -- ^ Response of the SMT Solver, containing the model if found
sat = satWith sbvCurrentSolver
-- | Find all satisfying solutions, using the CVC4 SMT solver
allSat :: Provable a
=> a -- ^ Property to check
-> IO AllSatResult -- ^ List of all satisfying models
allSat = allSatWith sbvCurrentSolver
-- | Check vacuity of the explicit constraints introduced by calls to the 'constrain' function, using the CVC4 SMT solver
isVacuous :: Provable a
=> a -- ^ Property to check
-> IO Bool -- ^ True if the constraints are unsatisifiable
isVacuous = isVacuousWith sbvCurrentSolver
-- | Check if the statement is a theorem, with an optional time-out in seconds, using the CVC4 SMT solver
isTheorem :: Provable a
=> Maybe Int -- ^ Optional time-out, specify in seconds
-> a -- ^ Property to check
-> IO (Maybe Bool) -- ^ Returns Nothing if time-out expires
isTheorem = isTheoremWith sbvCurrentSolver
-- | Check if the statement is satisfiable, with an optional time-out in seconds, using the CVC4 SMT solver
isSatisfiable :: Provable a
=> Maybe Int -- ^ Optional time-out, specify in seconds
-> a -- ^ Property to check
-> IO (Maybe Bool) -- ^ Returns Nothing if time-out expiers
isSatisfiable = isSatisfiableWith sbvCurrentSolver
-- | Optimize cost functions, using the CVC4 SMT solver
optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)
=> OptimizeOpts -- ^ Parameters to optimization (Iterative, Quantified, etc.)
-> (SBV c -> SBV c -> SBool) -- ^ Betterness check: This is the comparison predicate for optimization
-> ([SBV a] -> SBV c) -- ^ Cost function
-> Int -- ^ Number of inputs
-> ([SBV a] -> SBool) -- ^ Validity function
-> IO (Maybe [a]) -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution
optimize = optimizeWith sbvCurrentSolver
-- | Minimize cost functions, using the CVC4 SMT solver
minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)
=> OptimizeOpts -- ^ Parameters to optimization (Iterative, Quantified, etc.)
-> ([SBV a] -> SBV c) -- ^ Cost function to minimize
-> Int -- ^ Number of inputs
-> ([SBV a] -> SBool) -- ^ Validity function
-> IO (Maybe [a]) -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution
minimize = minimizeWith sbvCurrentSolver
-- | Maximize cost functions, using the CVC4 SMT solver
maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)
=> OptimizeOpts -- ^ Parameters to optimization (Iterative, Quantified, etc.)
-> ([SBV a] -> SBV c) -- ^ Cost function to maximize
-> Int -- ^ Number of inputs
-> ([SBV a] -> SBool) -- ^ Validity function
-> IO (Maybe [a]) -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution
maximize = maximizeWith sbvCurrentSolver
{- $moduleExportIntro
The remainder of the SBV library that is common to all back-end SMT solvers, directly coming from the "Data.SBV" module.
-}

2
sbv/Data/SBV/Bridge/Yices.hs
View File

@ -14,6 +14,8 @@
-- - "Data.SBV.Bridge.CVC4"
--
-- - "Data.SBV.Bridge.Z3"
--
-- - "Data.SBV.Bridge.MathSAT"
---------------------------------------------------------------------------------
module Data.SBV.Bridge.Yices (

2
sbv/Data/SBV/Bridge/Z3.hs
View File

@ -14,6 +14,8 @@
-- - "Data.SBV.Bridge.CVC4"
--
-- - "Data.SBV.Bridge.Yices"
--
-- - "Data.SBV.Bridge.MathSAT"
---------------------------------------------------------------------------------
module Data.SBV.Bridge.Z3 (

9
sbv/Data/SBV/Compilers/C.hs
View File

@ -24,7 +24,6 @@ import System.Random
import Text.PrettyPrint.HughesPJ
import Data.SBV.BitVectors.Data
import Data.SBV.BitVectors.AlgReals
import Data.SBV.BitVectors.PrettyNum (shex, showCFloat, showCDouble)
import Data.SBV.Compilers.CodeGen
@ -162,6 +161,7 @@ showCType = show . kindOf
-- | The printf specifier for the type
specifier :: CgConfig -> SW -> Doc
specifier cfg sw = case kindOf sw of
KBool -> spec (False, 1)
KBounded b i -> spec (b, i)
KUnbounded -> spec (True, fromJust (cgInteger cfg))
KReal -> specF (fromJust (cgReal cfg))
@ -443,7 +443,7 @@ genCProg cfg fn proto (Result kindInfo _tvals cgs ins preConsts tbls arrs _ _ (S
len (KFloat{}) = 6 -- SFloat
len (KDouble{}) = 7 -- SDouble
len (KUnbounded{}) = 8
len (KBounded False 1) = 5 -- SBool
len KBool = 5 -- SBool
len (KBounded False n) = 5 + length (show n) -- SWordN
len (KBounded True n) = 4 + length (show n) -- SIntN
len (KUninterpreted s) = die $ "Uninterpreted sort: " ++ s
@ -499,8 +499,8 @@ ppExpr cfg consts (SBVApp op opArgs) = p op (map (showSW cfg consts) opArgs)
p (Shr i) [a] = shift False i a (head opArgs)
p Not [a] = case kindOf (head opArgs) of
-- be careful about booleans, bitwise complement is not correct for them!
KBounded False 1 -> text "!" <> a
_ -> text "~" <> a
KBool -> text "!" <> a
_ -> text "~" <> a
p Ite [a, b, c] = a <+> text "?" <+> b <+> text ":" <+> c
p (LkUp (t, k, _, len) ind def) []
| not rtc = lkUp -- ignore run-time-checks per user request
@ -517,6 +517,7 @@ ppExpr cfg consts (SBVApp op opArgs) = p op (map (showSW cfg consts) opArgs)
canOverflow True sz = (2::Integer)^(sz-1)-1 >= fromIntegral len
canOverflow False sz = (2::Integer)^sz -1 >= fromIntegral len
(needsCheckL, needsCheckR) = case k of
KBool -> (False, canOverflow False (1::Int))
KBounded sg sz -> (sg, canOverflow sg sz)
KReal -> die "array index with real value"
KFloat -> die "array index with float value"

6
sbv/Data/SBV/Compilers/CodeGen.hs
View File

@ -16,6 +16,7 @@ module Data.SBV.Compilers.CodeGen where
import Control.Monad.Trans
import Control.Monad.State.Lazy
import Control.Applicative (Applicative)
import Data.Char (toLower, isSpace)
import Data.List (nub, isPrefixOf, intercalate, (\\))
import System.Directory (createDirectory, doesDirectoryExist, doesFileExist)
@ -75,7 +76,7 @@ initCgState = CgState {
-- reference parameters (for returning composite values in languages such as C),
-- and return values.
newtype SBVCodeGen a = SBVCodeGen (StateT CgState Symbolic a)
deriving (Monad, MonadIO, MonadState CgState)
deriving (Applicative, Functor, Monad, MonadIO, MonadState CgState)
-- | Reach into symbolic monad from code-generation
liftSymbolic :: Symbolic a -> SBVCodeGen a
@ -109,7 +110,7 @@ data CgSRealType = CgFloat -- ^ @float@
| CgLongDouble -- ^ @long double@
deriving Eq
-- As they would be used in a C program
-- | 'Show' instance for 'cgSRealType' displays values as they would be used in a C program
instance Show CgSRealType where
show CgFloat = "float"
show CgDouble = "double"
@ -217,6 +218,7 @@ isCgMakefile :: CgPgmKind -> Bool
isCgMakefile CgMakefile{} = True
isCgMakefile _ = False
-- | A simple way to print bundles, mostly for debugging purposes.
instance Show CgPgmBundle where
show (CgPgmBundle _ fs) = intercalate "\n" $ map showFile fs
where showFile :: (FilePath, (CgPgmKind, [Doc])) -> String

11
sbv/Data/SBV/Internals.hs
View File

@ -15,16 +15,13 @@ module Data.SBV.Internals (
-- * Running symbolic programs /manually/
Result, SBVRunMode(..), runSymbolic, runSymbolic'
-- * Other internal structures useful for low-level programming
, SBV(..), slet, CW, mkConstCW, genVar, genVar_
, mkSymSBVWithRandom
, Quantifier(..)
, SBV(..), slet, CW(..), Kind(..), CWVal(..), AlgReal(..), mkConstCW, genVar, genVar_
, liftQRem, liftDMod
-- * Compilation to C
, compileToC', compileToCLib', CgPgmBundle(..), CgPgmKind(..)
, mkUninterpreted, compileToC', compileToCLib', CgPgmBundle(..), CgPgmKind(..)
) where
import Data.SBV.BitVectors.Data (Result, SBVRunMode(..), runSymbolic, runSymbolic'
, SBV(..), CW, mkConstCW, Quantifier(..), mkSymSBVWithRandom)
import Data.SBV.BitVectors.Model (genVar, genVar_, slet, liftQRem, liftDMod)
import Data.SBV.BitVectors.Data (Result, SBVRunMode(..), runSymbolic, runSymbolic', SBV(..), CW(..), Kind(..), CWVal(..), AlgReal(..), mkConstCW)
import Data.SBV.BitVectors.Model (genVar, genVar_, slet, liftQRem, liftDMod, mkUninterpreted)
import Data.SBV.Compilers.C (compileToC', compileToCLib')
import Data.SBV.Compilers.CodeGen (CgPgmBundle(..), CgPgmKind(..))

4
sbv/Data/SBV/Provers/Boolector.hs
View File

@ -26,10 +26,10 @@ import Data.SBV.SMT.SMTLib
-- | The description of the Boolector SMT solver
-- The default executable is @\"boolector\"@, which must be in your path. You can use the @SBV_BOOLECTOR@ environment variable to point to the executable on your system.
-- The default options are @\"--lang smt\"@. You can use the @SBV_BOOLECTOR_OPTIONS@ environment variable to override the options.
-- The default options are @\"-m --smt2\"@. You can use the @SBV_BOOLECTOR_OPTIONS@ environment variable to override the options.
boolector :: SMTSolver
boolector = SMTSolver {
name = "boolector"
name = Boolector
, executable = "boolector"
, options = ["-m", "--smt2"]
, engine = \cfg _isSat qinps modelMap _skolemMap pgm -> do

4
sbv/Data/SBV/Provers/CVC4.hs
View File

@ -30,7 +30,7 @@ import Data.SBV.SMT.SMTLib
-- The default options are @\"--lang smt\"@. You can use the @SBV_CVC4_OPTIONS@ environment variable to override the options.
cvc4 :: SMTSolver
cvc4 = SMTSolver {
name = "cvc4"
name = CVC4
, executable = "cvc4"
, options = ["--lang", "smt"]
, engine = \cfg isSat qinps modelMap skolemMap pgm -> do
@ -57,7 +57,7 @@ cvc4 = SMTSolver {
}
}
where zero :: Kind -> String
zero (KBounded False 1) = "#b0"
zero KBool = "false"
zero (KBounded _ sz) = "#x" ++ replicate (sz `div` 4) '0'
zero KUnbounded = "0"
zero KReal = "0.0"

92
sbv/Data/SBV/Provers/MathSAT.hs Normal file
View File

@ -0,0 +1,92 @@
-----------------------------------------------------------------------------
-- |
-- Module : Data.SBV.Provers.MathSAT
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--
-- The connection to the MathSAT SMT solver
-----------------------------------------------------------------------------
{-# LANGUAGE ScopedTypeVariables #-}
module Data.SBV.Provers.MathSAT(mathSAT) where
import qualified Control.Exception as C
import Data.Function (on)
import Data.List (sortBy, intercalate)
import System.Environment (getEnv)
import Data.SBV.BitVectors.Data
import Data.SBV.SMT.SMT
import Data.SBV.SMT.SMTLib
-- | The description of the MathSAT SMT solver
-- The default executable is @\"mathsat\"@, which must be in your path. You can use the @SBV_MATHSAT@ environment variable to point to the executable on your system.
-- The default options are @\"-input=smt2\"@. You can use the @SBV_MATHSAT_OPTIONS@ environment variable to override the options.
mathSAT :: SMTSolver
mathSAT = SMTSolver {
name = MathSAT
, executable = "mathsat"
, options = ["-input=smt2"]
, engine = \cfg _isSat qinps modelMap skolemMap pgm -> do
execName <- getEnv "SBV_MATHSAT" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))
execOpts <- (words `fmap` getEnv "SBV_MATHSAT_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg)))
let cfg' = cfg { solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts}
}
tweaks = case solverTweaks cfg' of
[] -> ""
ts -> unlines $ "; --- user given solver tweaks ---" : ts ++ ["; --- end of user given tweaks ---"]
script = SMTScript {scriptBody = tweaks ++ pgm, scriptModel = Just (cont skolemMap)}
standardSolver cfg' script id (ProofError cfg') (interpretSolverOutput cfg' (extractMap (map snd qinps) modelMap))
, xformExitCode = id
, capabilities = SolverCapabilities {
capSolverName = "MathSAT"
, mbDefaultLogic = Nothing
, supportsMacros = False
, supportsProduceModels = True
, supportsQuantifiers = True
, supportsUninterpretedSorts = True
, supportsUnboundedInts = True
, supportsReals = True
, supportsFloats = False
, supportsDoubles = False
}
}
where zero :: Kind -> String
zero KBool = "false"
zero (KBounded _ sz) = "#x" ++ replicate (sz `div` 4) '0'
zero KUnbounded = "0"
zero KReal = "0.0"
zero KFloat = error "SBV.MathSAT.zero: Unexpected sort SFloat"
zero KDouble = error "SBV.MathSAT.zero: Unexpected sort SDouble"
zero (KUninterpreted s) = error $ "SBV.MathSAT.zero: Unexpected uninterpreted sort: " ++ s
cont skolemMap = intercalate "\n" $ concatMap extract skolemMap
where -- In the skolemMap:
-- * Left's are universals: i.e., the model should be true for
-- any of these. So, we simply "echo 0" for these values.
-- * Right's are existentials. If there are no dependencies (empty list), then we can
-- simply use get-value to extract it's value. Otherwise, we have to apply it to
-- an appropriate number of 0's to get the final value.
extract (Left s) = ["(echo \"((" ++ show s ++ " " ++ zero (kindOf s) ++ "))\")"]
extract (Right (s, [])) = ["(get-value (" ++ show s ++ "))"]
extract (Right (s, ss)) = let g = "(get-value ((" ++ show s ++ concat [' ' : zero (kindOf a) | a <- ss] ++ ")))" in [g]
addTimeOut Nothing o = o
addTimeOut (Just _) _ = error "MathSAT: Timeout values are not supported by MathSat"
extractMap :: [NamedSymVar] -> [(String, UnintKind)] -> [String] -> SMTModel
extractMap inps _modelMap solverLines =
SMTModel { modelAssocs = map snd $ sortByNodeId $ concatMap (interpretSolverModelLine inps . cvt) solverLines
, modelUninterps = []
, modelArrays = []
}
where sortByNodeId :: [(Int, a)] -> [(Int, a)]
sortByNodeId = sortBy (compare `on` fst)
cvt :: String -> String
cvt s = case words s of
[var, val] -> "((" ++ var ++ " #b" ++ map tr val ++ "))"
_ -> s -- good-luck..
where tr 'x' = '0'
tr x = x

271
sbv/Data/SBV/Provers/Prover.hs
View File

@ -18,55 +18,51 @@ module Data.SBV.Provers.Prover (
SMTSolver(..), SMTConfig(..), Predicate, Provable(..)
, ThmResult(..), SatResult(..), AllSatResult(..), SMTResult(..)
, isSatisfiable, isSatisfiableWith, isTheorem, isTheoremWith
, Equality(..)
, prove, proveWith
, sat, satWith
, allSat, allSatWith
, isVacuous, isVacuousWith
, solve
, SatModel(..), Modelable(..), displayModels, extractModels
, boolector, cvc4, yices, z3, defaultSMTCfg
, getModelDictionaries, getModelValues, getModelUninterpretedValues
, boolector, cvc4, yices, z3, mathSAT, defaultSMTCfg
, compileToSMTLib, generateSMTBenchmarks
, sbvCheckSolverInstallation
, internalSatWith, internalIsSatisfiableWith, internalIsSatisfiable
, internalProveWith, internalIsTheoremWith, internalIsTheorem
, isSBranchFeasibleInState
) where
import qualified Control.Exception as E
import Control.Concurrent (forkIO, newChan, writeChan, getChanContents)
import Control.Monad (when, unless, void)
import Control.Monad.Trans(liftIO)
import Data.List (intercalate)
import Data.Maybe (fromJust, isJust, mapMaybe)
import System.FilePath (addExtension)
import System.Time (getClockTime)
import Control.Monad (when, unless)
import Control.Monad.Trans (liftIO)
import Data.List (intercalate)
import Data.Maybe (mapMaybe, fromMaybe)
import System.FilePath (addExtension, splitExtension)
import System.Time (getClockTime)
import System.IO.Unsafe (unsafeInterleaveIO)
import qualified Data.Set as Set (Set, toList)
import Data.SBV.BitVectors.Data
import Data.SBV.BitVectors.Model
import Data.SBV.SMT.SMT
import Data.SBV.SMT.SMTLib
import qualified Data.SBV.Provers.Boolector as Boolector
import qualified Data.SBV.Provers.CVC4 as CVC4
import qualified Data.SBV.Provers.Yices as Yices
import qualified Data.SBV.Provers.Z3 as Z3
import qualified Data.SBV.Provers.MathSAT as MathSAT
import Data.SBV.Utils.TDiff
import Data.SBV.Utils.Boolean
mkConfig :: SMTSolver -> Bool -> [String] -> SMTConfig
mkConfig s isSMTLib2 tweaks = SMTConfig { verbose = False
, timing = False
, timeOut = Nothing
, printBase = 10
, printRealPrec = 16
, smtFile = Nothing
, solver = s
, solverTweaks = tweaks
, useSMTLib2 = isSMTLib2
, satCmd = "(check-sat)"
, roundingMode = RoundNearestTiesToEven
mkConfig s isSMTLib2 tweaks = SMTConfig { verbose = False
, timing = False
, sBranchTimeOut = Nothing
, timeOut = Nothing
, printBase = 10
, printRealPrec = 16
, smtFile = Nothing
, solver = s
, solverTweaks = tweaks
, useSMTLib2 = isSMTLib2
, satCmd = "(check-sat)"
, roundingMode = RoundNearestTiesToEven
, useLogic = Nothing
}
-- | Default configuration for the Boolector SMT solver
@ -83,8 +79,11 @@ yices = mkConfig Yices.yices False []
-- | Default configuration for the Z3 SMT solver
z3 :: SMTConfig
--z3 = mkConfig Z3.z3 True ["(set-option :smt.mbqi true) ; use model based quantifier instantiation"]
z3 = mkConfig Z3.z3 True []
z3 = mkConfig Z3.z3 True ["(set-option :smt.mbqi true) ; use model based quantifier instantiation"]
-- | Default configuration for the MathSAT SMT solver
mathSAT :: SMTConfig
mathSAT = mkConfig MathSAT.mathSAT True []
-- | The default solver used by SBV. This is currently set to z3.
defaultSMTCfg :: SMTConfig
@ -233,16 +232,6 @@ prove = proveWith defaultSMTCfg
sat :: Provable a => a -> IO SatResult
sat = satWith defaultSMTCfg
-- | Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing
-- problems with constraints, like the following:
--
-- @
-- do [x, y, z] <- sIntegers [\"x\", \"y\", \"z\"]
-- solve [x .> 5, y + z .< x]
-- @
solve :: [SBool] -> Symbolic SBool
solve = return . bAnd
-- | Return all satisfying assignments for a predicate, equivalent to @'allSatWith' 'defaultSMTCfg'@.
-- Satisfying assignments are constructed lazily, so they will be available as returned by the solver
-- and on demand.
@ -254,40 +243,8 @@ solve = return . bAnd
allSat :: Provable a => a -> IO AllSatResult
allSat = allSatWith defaultSMTCfg
-- | Check if the given constraints are satisfiable, equivalent to @'isVacuousWith' 'defaultSMTCfg'@. This
-- call can be used to ensure that the specified constraints (via 'constrain') are satisfiable, i.e., that
-- the proof involving these constraints is not passing vacuously. Here is an example. Consider the following
-- predicate:
--
-- >>> let pred = do { x <- forall "x"; constrain $ x .< x; return $ x .>= (5 :: SWord8) }
--
-- This predicate asserts that all 8-bit values are larger than 5, subject to the constraint that the
-- values considered satisfy @x .< x@, i.e., they are less than themselves. Since there are no values that
-- satisfy this constraint, the proof will pass vacuously:
--
-- >>> prove pred
-- Q.E.D.
--
-- We can use 'isVacuous' to make sure to see that the pass was vacuous:
--
-- >>> isVacuous pred
-- True
--
-- While the above example is trivial, things can get complicated if there are multiple constraints with
-- non-straightforward relations; so if constraints are used one should make sure to check the predicate
-- is not vacuously true. Here's an example that is not vacuous:
--
-- >>> let pred' = do { x <- forall "x"; constrain $ x .> 6; return $ x .>= (5 :: SWord8) }
--
-- This time the proof passes as expected:
--
-- >>> prove pred'
-- Q.E.D.
--
-- And the proof is not vacuous:
--
-- >>> isVacuous pred'
-- False
-- | Check if the given constraints are satisfiable, equivalent to @'isVacuousWith' 'defaultSMTCfg'@.
-- See the function 'constrain' for an example use of 'isVacuous'.
isVacuous :: Provable a => a -> IO Bool
isVacuous = isVacuousWith defaultSMTCfg
@ -323,30 +280,6 @@ isTheorem = isTheoremWith defaultSMTCfg
isSatisfiable :: Provable a => Maybe Int -> a -> IO (Maybe Bool)
isSatisfiable = isSatisfiableWith defaultSMTCfg
internalIsTheoremWith :: SMTConfig -> Maybe Int -> SBool -> Symbolic (Maybe Bool)
internalIsTheoremWith cfg mbTo p = do
r <- internalProveWith cfg{timeOut = mbTo} p
case r of
ThmResult (Unsatisfiable _) -> return $ Just True
ThmResult (Satisfiable _ _) -> return $ Just False
ThmResult (TimeOut _) -> return Nothing
_ -> error $ "SBV.isTheorem: Received:\n" ++ show r
internalIsTheorem :: Maybe Int -> SBool -> Symbolic (Maybe Bool)
internalIsTheorem = internalIsTheoremWith defaultSMTCfg
internalIsSatisfiableWith :: SMTConfig -> Maybe Int -> SBool -> Symbolic (Maybe Bool)
internalIsSatisfiableWith cfg mbTo p = do
r <- internalSatWith cfg{timeOut = mbTo} p
case r of
SatResult (Satisfiable _ _) -> return $ Just True
SatResult (Unsatisfiable _) -> return $ Just False
SatResult (TimeOut _) -> return Nothing
_ -> error $ "SBV.isSatisfiable: Received: " ++ show r
internalIsSatisfiable :: Maybe Int -> SBool -> Symbolic (Maybe Bool)
internalIsSatisfiable = internalIsSatisfiableWith defaultSMTCfg
-- | Compiles to SMT-Lib and returns the resulting program as a string. Useful for saving
-- the result to a file for off-line analysis, for instance if you have an SMT solver that's not natively
-- supported out-of-the box by the SBV library. It takes two booleans:
@ -393,28 +326,10 @@ satWith :: Provable a => SMTConfig -> a -> IO SatResult
satWith config a = simulate cvt config True [] a >>= callSolver True "Checking Satisfiability.." SatResult config
where cvt = if useSMTLib2 config then toSMTLib2 else toSMTLib1
internalProveWith :: SMTConfig -> SBool -> Symbolic ThmResult
internalProveWith config b = do
sw <- sbvToSymSW b
Result ki tr uic is cs ts as uis ax asgn cstr _ <- getResult
let res = Result ki tr uic is cs ts as uis ax asgn cstr [sw]
let cvt = if useSMTLib2 config then toSMTLib2 else toSMTLib1
problem <- liftIO $ runProofOn cvt config False [] res
liftIO $ callSolver True "Checking Satisfiability.." ThmResult config problem
internalSatWith :: SMTConfig -> SBool -> Symbolic SatResult
internalSatWith config b = do
sw <- sbvToSymSW b
Result ki tr uic is cs ts as uis ax asgn cstr _ <- getResult
let res = Result ki tr uic is cs ts as uis ax asgn cstr [sw]
let cvt = if useSMTLib2 config then toSMTLib2 else toSMTLib1
problem <- liftIO $ runProofOn cvt config True [] res
liftIO $ callSolver True "Checking Satisfiability.." SatResult config problem
-- | Determine if the constraints are vacuous using the given SMT-solver
isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool
isVacuousWith config a = do
Result ki tr uic is cs ts as uis ax asgn cstr _ <- runSymbolic True $ forAll_ a >>= output
Result ki tr uic is cs ts as uis ax asgn cstr _ <- runSymbolic (True, Just config) $ forAll_ a >>= output
case cstr of
[] -> return False -- no constraints, no need to check
_ -> do let is' = [(EX, i) | (_, i) <- is] -- map all quantifiers to "exists" for the constraint check
@ -435,45 +350,40 @@ allSatWith config p = do
msg "Checking Satisfiability, all solutions.."
sbvPgm@(qinps, _, _, ki, _) <- simulate converter config True [] p
let usorts = [s | KUninterpreted s <- Set.toList ki]
unless (null usorts) $ error $ "SBV.allSat: All-sat calls are not supported in the presence of uninterpreted sorts: " ++ unwords usorts
++ "\n Only 'sat' and 'prove' calls are available when uninterpreted sorts are used."
resChan <- newChan
let add = writeChan resChan . Just
stop = writeChan resChan Nothing
final r = add r >> stop
die m = final (ProofError config [m])
-- only fork if non-verbose.. otherwise stdout gets garbled
fork io = if verbose config then io else void (forkIO io)
fork $ E.catch (go sbvPgm add stop final (1::Int) [])
(\e -> die (show (e::E.SomeException)))
results <- getChanContents resChan
unless (null usorts) $ msg $ "SBV.allSat: Uninterpreted sorts present: " ++ unwords usorts
++ "\n SBV will use equivalence classes to generate all-satisfying instances."
results <- unsafeInterleaveIO $ go sbvPgm (1::Int) []
-- See if there are any existentials below any universals
-- If such is the case, then the solutions are unique upto prefix existentials
let w = ALL `elem` map fst qinps
return $ AllSatResult (w, map fromJust (takeWhile isJust results))
return $ AllSatResult (w, results)
where msg = when (verbose config) . putStrLn . ("** " ++)
go sbvPgm add stop final = loop
go sbvPgm = loop
where loop !n nonEqConsts = do
curResult <- invoke nonEqConsts n sbvPgm
case curResult of
Nothing -> stop
Just (SatResult r) -> case r of
Satisfiable _ (SMTModel [] _ _) -> final r
Unknown _ (SMTModel [] _ _) -> final r
ProofError _ _ -> final r
TimeOut _ -> stop
Unsatisfiable _ -> stop
Satisfiable _ model -> add r >> loop (n+1) (modelAssocs model : nonEqConsts)
Unknown _ model -> add r >> loop (n+1) (modelAssocs model : nonEqConsts)
Nothing -> return []
Just (SatResult r) -> let cont model = do rest <- unsafeInterleaveIO $ loop (n+1) (modelAssocs model : nonEqConsts)
return (r : rest)
in case r of
Satisfiable _ (SMTModel [] _ _) -> return [r]
Unknown _ (SMTModel [] _ _) -> return [r]
ProofError _ _ -> return [r]
TimeOut _ -> return []
Unsatisfiable _ -> return []
Satisfiable _ model -> cont model
Unknown _ model -> cont model
invoke nonEqConsts n (qinps, modelMap, skolemMap, _, smtLibPgm) = do
msg $ "Looking for solution " ++ show n
case addNonEqConstraints (roundingMode config) qinps nonEqConsts smtLibPgm of
Nothing -> -- no new constraints added, stop
return Nothing
Just finalPgm -> do msg $ "Generated SMTLib program:\n" ++ finalPgm
smtAnswer <- engine (solver config) config True qinps modelMap skolemMap finalPgm
smtAnswer <- engine (solver config) (updateName (n-1) config) True qinps modelMap skolemMap finalPgm
msg "Done.."
return $ Just $ SatResult smtAnswer
updateName i cfg = cfg{smtFile = upd `fmap` smtFile cfg}
where upd nm = let (b, e) = splitExtension nm in b ++ "_allSat_" ++ show i ++ e
type SMTProblem = ( [(Quantifier, NamedSymVar)] -- inputs
, [(String, UnintKind)] -- model-map
@ -497,7 +407,7 @@ simulate converter config isSat comments predicate = do
let msg = when (verbose config) . putStrLn . ("** " ++)
isTiming = timing config
msg "Starting symbolic simulation.."
res <- timeIf isTiming "problem construction" $ runSymbolic isSat $ (if isSat then forSome_ else forAll_) predicate >>= output
res <- timeIf isTiming "problem construction" $ runSymbolic (isSat, Just config) $ (if isSat then forSome_ else forAll_) predicate >>= output
msg $ "Generated symbolic trace:\n" ++ show res
msg "Translating to SMT-Lib.."
runProofOn converter config isSat comments res
@ -507,7 +417,7 @@ runProofOn converter config isSat comments res =
let isTiming = timing config
solverCaps = capabilities (solver config)
in case res of
Result ki _qcInfo _codeSegs is consts tbls arrs uis axs pgm cstrs [o@(SW (KBounded False 1) _)] ->
Result ki _qcInfo _codeSegs is consts tbls arrs uis axs pgm cstrs [o@(SW KBool _)] ->
timeIf isTiming "translation"
$ let uiMap = mapMaybe arrayUIKind arrs ++ map unintFnUIKind uis
skolemMap = skolemize (if isSat then is else map flipQ is)
@ -518,7 +428,7 @@ runProofOn converter config isSat comments res =
where go [] (_, sofar) = reverse sofar
go ((ALL, (v, _)):rest) (us, sofar) = go rest (v:us, Left v : sofar)
go ((EX, (v, _)):rest) (us, sofar) = go rest (us, Right (v, reverse us) : sofar)
in return (is, uiMap, skolemMap, ki, converter (roundingMode config) solverCaps ki isSat comments is skolemMap consts tbls arrs uis axs pgm cstrs o)
in return (is, uiMap, skolemMap, ki, converter (roundingMode config) (useLogic config) solverCaps ki isSat comments is skolemMap consts tbls arrs uis axs pgm cstrs o)
Result _kindInfo _qcInfo _codeSegs _is _consts _tbls _arrs _uis _axs _pgm _cstrs os -> case length os of
0 -> error $ "Impossible happened, unexpected non-outputting result\n" ++ show res
1 -> error $ "Impossible happened, non-boolean output in " ++ show os
@ -527,56 +437,23 @@ runProofOn converter config isSat comments res =
++ "\nDetected while generating the trace:\n" ++ show res
++ "\n*** Check calls to \"output\", they are typically not needed!"
-- | Check whether the given solver is installed and is ready to go. This call does a
-- simple call to the solver to ensure all is well.
sbvCheckSolverInstallation :: SMTConfig -> IO Bool
sbvCheckSolverInstallation cfg = do ThmResult r <- proveWith cfg $ \x -> (x+x) .== ((x*2) :: SWord8)
case r of
Unsatisfiable _ -> return True
_ -> return False
-- | Equality as a proof method. Allows for
-- very concise construction of equivalence proofs, which is very typical in
-- bit-precise proofs.
infix 4 ===
class Equality a where
(===) :: a -> a -> IO ThmResult
instance (SymWord a, EqSymbolic z) => Equality (SBV a -> z) where
k === l = prove $ \a -> k a .== l a
instance (SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) where
k === l = prove $ \a b -> k a b .== l a b
instance (SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) where
k === l = prove $ \a b -> k (a, b) .== l (a, b)
instance (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) where
k === l = prove $ \a b c -> k a b c .== l a b c
instance (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) where
k === l = prove $ \a b c -> k (a, b, c) .== l (a, b, c)
instance (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) where
k === l = prove $ \a b c d -> k a b c d .== l a b c d
instance (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) where
k === l = prove $ \a b c d -> k (a, b, c, d) .== l (a, b, c, d)
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) where
k === l = prove $ \a b c d e -> k a b c d e .== l a b c d e
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) where
k === l = prove $ \a b c d e -> k (a, b, c, d, e) .== l (a, b, c, d, e)
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) where
k === l = prove $ \a b c d e f -> k a b c d e f .== l a b c d e f
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) where
k === l = prove $ \a b c d e f -> k (a, b, c, d, e, f) .== l (a, b, c, d, e, f)
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) where
k === l = prove $ \a b c d e f g -> k a b c d e f g .== l a b c d e f g
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) where
k === l = prove $ \a b c d e f g -> k (a, b, c, d, e, f, g) .== l (a, b, c, d, e, f, g)
-- | Check if a branch condition is feasible in the current state
isSBranchFeasibleInState :: State -> String -> SBool -> IO Bool
isSBranchFeasibleInState st branch cond = do
let cfg = let pickedConfig = fromMaybe defaultSMTCfg (getSBranchRunConfig st)
in pickedConfig { timeOut = sBranchTimeOut pickedConfig }
msg = when (verbose cfg) . putStrLn . ("** " ++)
sw <- sbvToSW st cond
() <- forceSWArg sw
Result ki tr uic is cs ts as uis ax asgn cstr _ <- liftIO $ extractSymbolicSimulationState st
let -- Construct the corresponding sat-checker for the branch. Note that we need to
-- forget about the quantifiers and just use an "exist", as we're looking for a
-- point-satisfiability check here; whatever the original program was.
pgm = Result ki tr uic [(EX, n) | (_, n) <- is] cs ts as uis ax asgn cstr [sw]
cvt = if useSMTLib2 cfg then toSMTLib2 else toSMTLib1
check <- runProofOn cvt cfg True [] pgm >>= callSolver True ("sBranch: Checking " ++ show branch ++ " feasibility") SatResult cfg
res <- case check of
SatResult (Unsatisfiable _) -> return False
_ -> return True -- No risks, even if it timed-our or anything else, we say it's feasible
msg $ "sBranch: Conclusion: " ++ if res then "Feasible" else "Unfeasible"
return res

7
sbv/Data/SBV/Provers/SExpr.hs
View File

@ -11,10 +11,9 @@
module Data.SBV.Provers.SExpr where
import Control.Monad.Error () -- for Monad (Either String) instance
import Data.Char (isDigit, ord)
import Data.List (isPrefixOf)
import Numeric (readInt, readDec, readHex, fromRat)
import Data.Char (isDigit, ord)
import Data.List (isPrefixOf)
import Numeric (readInt, readDec, readHex, fromRat)
import Data.SBV.BitVectors.AlgReals
import Data.SBV.BitVectors.Data (nan, infinity)

2
sbv/Data/SBV/Provers/Yices.hs
View File

@ -31,7 +31,7 @@ import Data.SBV.SMT.SMTLib
-- The default options are @\"-m -f\"@, which is valid for Yices 2.1 series. You can use the @SBV_YICES_OPTIONS@ environment variable to override the options.
yices :: SMTSolver
yices = SMTSolver {
name = "Yices"
name = Yices
, executable = "yices-smt"
-- , options = ["-tc", "-smt", "-e"] -- For Yices1
, options = ["-m", "-f"] -- For Yices2

34
sbv/Data/SBV/Provers/Z3.hs
View File

@ -23,6 +23,7 @@ import qualified System.Info as S(os)
import Data.SBV.BitVectors.AlgReals
import Data.SBV.BitVectors.Data
import Data.SBV.BitVectors.PrettyNum
import Data.SBV.SMT.SMT
import Data.SBV.SMT.SMTLib
@ -38,7 +39,7 @@ optionPrefix
-- The default options are @\"-in -smt2\"@, which is valid for Z3 4.1. You can use the @SBV_Z3_OPTIONS@ environment variable to override the options.
z3 :: SMTSolver
z3 = SMTSolver {
name = "z3"
name = Z3
, executable = "z3"
, options = map (optionPrefix:) ["in", "smt2"]
, engine = \cfg isSat qinps modelMap skolemMap pgm -> do
@ -49,8 +50,8 @@ z3 = SMTSolver {
[] -> ""
ts -> unlines $ "; --- user given solver tweaks ---" : ts ++ ["; --- end of user given tweaks ---"]
dlim = printRealPrec cfg'
--ppDecLim = "(set-option :pp.decimal_precision " ++ show dlim ++ ")\n"
script = SMTScript {scriptBody = tweaks ++ {- ppDecLim ++ -} pgm, scriptModel = Just (cont skolemMap)}
ppDecLim = "(set-option :pp.decimal_precision " ++ show dlim ++ ")\n"
script = SMTScript {scriptBody = tweaks ++ ppDecLim ++ pgm, scriptModel = Just (cont (roundingMode cfg) skolemMap)}
if dlim < 1
then error $ "SBV.Z3: printRealPrec value should be at least 1, invalid value received: " ++ show dlim
else standardSolver cfg' script cleanErrs (ProofError cfg') (interpretSolverOutput cfg' (extractMap isSat qinps modelMap))
@ -68,28 +69,27 @@ z3 = SMTSolver {
, supportsDoubles = True
}
}
where -- Get rid of the following when z3_4.0 is out
cleanErrs = intercalate "\n" . filter (not . junk) . lines
where cleanErrs = intercalate "\n" . filter (not . junk) . lines
junk = ("WARNING:" `isPrefixOf`)
zero :: Kind -> String
zero (KBounded False 1) = "#b0"
zero (KBounded _ sz) = "#x" ++ replicate (sz `div` 4) '0'
zero KUnbounded = "0"
zero KReal = "0.0"
zero KFloat = error "Z3:TBD: Figure out how to write float constants!"
zero KDouble = error "Z3:TBD: Figure out how to write double constants!"
zero (KUninterpreted s) = error $ "SBV.Z3.zero: Unexpected uninterpreted sort: " ++ s
cont skolemMap = intercalate "\n" $ concatMap extract skolemMap
zero :: RoundingMode -> Kind -> String
zero _ KBool = "false"
zero _ (KBounded _ sz) = "#x" ++ replicate (sz `div` 4) '0'
zero _ KUnbounded = "0"
zero _ KReal = "0.0"
zero rm KFloat = showSMTFloat rm 0
zero rm KDouble = showSMTDouble rm 0
zero _ (KUninterpreted s) = error $ "SBV.Z3.zero: Unexpected uninterpreted sort: " ++ s
cont rm skolemMap = intercalate "\n" $ concatMap extract skolemMap
where -- In the skolemMap:
-- * Left's are universals: i.e., the model should be true for
-- any of these. So, we simply "echo 0" for these values.
-- * Right's are existentials. If there are no dependencies (empty list), then we can
-- simply use get-value to extract it's value. Otherwise, we have to apply it to
-- an appropriate number of 0's to get the final value.
extract (Left s) = ["(echo \"((" ++ show s ++ " " ++ zero (kindOf s) ++ "))\")"]
extract (Left s) = ["(echo \"((" ++ show s ++ " " ++ zero rm (kindOf s) ++ "))\")"]
extract (Right (s, [])) = let g = "(get-value (" ++ show s ++ "))" in getVal (kindOf s) g
extract (Right (s, ss)) = let g = "(get-value ((" ++ show s ++ concat [' ' : zero (kindOf a) | a <- ss] ++ ")))" in getVal (kindOf s) g
getVal KReal g = ["(set-option :pp.decimal false)", g, "(set-option :pp.decimal true)", g]
extract (Right (s, ss)) = let g = "(get-value ((" ++ show s ++ concat [' ' : zero rm (kindOf a) | a <- ss] ++ ")))" in getVal (kindOf s) g
getVal KReal g = ["(set-option :pp.decimal false) " ++ g, "(set-option :pp.decimal true) " ++ g]
getVal _ g = [g]
addTimeOut Nothing o = o
addTimeOut (Just i) o

244
sbv/Data/SBV/SMT/SMT.hs
View File

@ -16,88 +16,23 @@ module Data.SBV.SMT.SMT where
import qualified Control.Exception as C
import Control.Concurrent (newEmptyMVar, takeMVar, putMVar, forkIO)
import Control.DeepSeq (NFData(..))
import Control.Monad (when, zipWithM)
import Data.Char (isSpace)
import Data.Int (Int8, Int16, Int32, Int64)
import Data.List (intercalate, isPrefixOf, isInfixOf)
import Data.Maybe (isNothing, fromJust)
import Data.Word (Word8, Word16, Word32, Word64)
import System.Directory (findExecutable)
import System.Process (readProcessWithExitCode, runInteractiveProcess, waitForProcess)
import System.Process (runInteractiveProcess, waitForProcess, terminateProcess)
import System.Exit (ExitCode(..))
import System.IO (hClose, hFlush, hPutStr, hGetContents, hGetLine)
import qualified Data.Map as M
import Data.SBV.BitVectors.AlgReals
import Data.SBV.BitVectors.Data
import Data.SBV.BitVectors.PrettyNum
import Data.SBV.Utils.TDiff
-- | Solver configuration. See also 'z3', 'yices', 'cvc4', and 'boolector, which are instantiations of this type for those solvers, with
-- reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as @z3{verbose=True}@.)
--
-- Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does
-- not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to
-- emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite
-- precision value on the screen. The field 'printRealPrec' controls the printing precision, by specifying the number of digits after
-- the decimal point. The default value is 16, but it can be set to any positive integer.
--
-- When printing, SBV will add the suffix @...@ at the and of a real-value, if the given bound is not sufficient to represent the real-value
-- exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it
-- is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation
-- of the real value is not finite, i.e., if it is not rational.
data SMTConfig = SMTConfig {
verbose :: Bool -- ^ Debug mode
, timing :: Bool -- ^ Print timing information on how long different phases took (construction, solving, etc.)
, timeOut :: Maybe Int -- ^ How much time to give to the solver. (In seconds)
, printBase :: Int -- ^ Print integral literals in this base (2, 8, and 10, and 16 are supported.)
, printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16)
, solverTweaks :: [String] -- ^ Additional lines of script to give to the solver (user specified)
, satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics.
, smtFile :: Maybe FilePath -- ^ If Just, the generated SMT script will be put in this file (for debugging purposes mostly)
, useSMTLib2 :: Bool -- ^ If True, we'll treat the solver as using SMTLib2 input format. Otherwise, SMTLib1
, solver :: SMTSolver -- ^ The actual SMT solver.
, roundingMode :: RoundingMode -- ^ Rounding mode to use for floating-point conversions
}
-- | An SMT engine
type SMTEngine = SMTConfig -> Bool -> [(Quantifier, NamedSymVar)] -> [(String, UnintKind)] -> [Either SW (SW, [SW])] -> String -> IO SMTResult
-- | An SMT solver
data SMTSolver = SMTSolver {
name :: String -- ^ Printable name of the solver
, executable :: String -- ^ The path to its executable
, options :: [String] -- ^ Options to provide to the solver
, engine :: SMTEngine -- ^ The solver engine, responsible for interpreting solver output
, xformExitCode :: ExitCode -> ExitCode -- ^ Should we re-interpret exit codes. Most solvers behave rationally, i.e., id will do. Some (like CVC4) don't.
, capabilities :: SolverCapabilities -- ^ Various capabilities of the solver
}
-- | A model, as returned by a solver
data SMTModel = SMTModel {
modelAssocs :: [(String, CW)]
, modelArrays :: [(String, [String])] -- very crude!
, modelUninterps :: [(String, [String])] -- very crude!
}
deriving Show
-- | The result of an SMT solver call. Each constructor is tagged with
-- the 'SMTConfig' that created it so that further tools can inspect it
-- and build layers of results, if needed. For ordinary uses of the library,
-- this type should not be needed, instead use the accessor functions on
-- it. (Custom Show instances and model extractors.)
data SMTResult = Unsatisfiable SMTConfig -- ^ Unsatisfiable
| Satisfiable SMTConfig SMTModel -- ^ Satisfiable with model
| Unknown SMTConfig SMTModel -- ^ Prover returned unknown, with a potential (possibly bogus) model
| ProofError SMTConfig [String] -- ^ Prover errored out
| TimeOut SMTConfig -- ^ Computation timed out (see the 'timeout' combinator)
-- | A script, to be passed to the solver.
data SMTScript = SMTScript {
scriptBody :: String -- ^ Initial feed
, scriptModel :: Maybe String -- ^ Optional continuation script, if the result is sat
}
-- | Extract the final configuration from a result
resultConfig :: SMTResult -> SMTConfig
resultConfig (Unsatisfiable c) = c
@ -106,16 +41,6 @@ resultConfig (Unknown c _) = c
resultConfig (ProofError c _) = c
resultConfig (TimeOut c) = c
instance NFData SMTResult where
rnf (Unsatisfiable _) = ()
rnf (Satisfiable _ xs) = rnf xs `seq` ()
rnf (Unknown _ xs) = rnf xs `seq` ()
rnf (ProofError _ xs) = rnf xs `seq` ()
rnf (TimeOut _) = ()
instance NFData SMTModel where
rnf (SMTModel assocs unints uarrs) = rnf assocs `seq` rnf unints `seq` rnf uarrs `seq` ()
-- | A 'prove' call results in a 'ThmResult'
newtype ThmResult = ThmResult SMTResult
@ -127,17 +52,19 @@ newtype SatResult = SatResult SMTResult
-- we should warn the user about prefix-existentials.
newtype AllSatResult = AllSatResult (Bool, [SMTResult])
-- | User friendly way of printing theorem results
instance Show ThmResult where
show (ThmResult r) = showSMTResult "Q.E.D."
"Unknown" "Unknown. Potential counter-example:\n"
"Falsifiable" "Falsifiable. Counter-example:\n" r
-- | User friendly way of printing satisfiablity results
instance Show SatResult where
show (SatResult r) = showSMTResult "Unsatisfiable"
"Unknown" "Unknown. Potential model:\n"
"Satisfiable" "Satisfiable. Model:\n" r
-- NB. The Show instance of AllSatResults have to be careful in being lazy enough
-- | The Show instance of AllSatResults. Note that we have to be careful in being lazy enough
-- as the typical use case is to pull results out as they become available.
instance Show AllSatResult where
show (AllSatResult (e, xs)) = go (0::Int) xs
@ -178,51 +105,73 @@ genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW])
genParse k (x@(CW _ (CWInteger i)):r) | kindOf x == k = Just (fromIntegral i, r)
genParse _ _ = Nothing
-- Base case, that comes in handy if there are no real variables
-- | Base case for 'SatModel' at unit type. Comes in handy if there are no real variables.
instance SatModel () where
parseCWs xs = return ((), xs)
-- | 'Bool' as extracted from a model
instance SatModel Bool where
parseCWs xs = do (x, r) <- genParse (KBounded False 1) xs
parseCWs xs = do (x, r) <- genParse KBool xs
return ((x :: Integer) /= 0, r)
-- | 'Word8' as extracted from a model
instance SatModel Word8 where
parseCWs = genParse (KBounded False 8)
-- | 'Int8' as extracted from a model
instance SatModel Int8 where
parseCWs = genParse (KBounded True 8)
-- | 'Word16' as extracted from a model
instance SatModel Word16 where
parseCWs = genParse (KBounded False 16)
-- | 'Int16' as extracted from a model
instance SatModel Int16 where
parseCWs = genParse (KBounded True 16)
-- | 'Word32' as extracted from a model
instance SatModel Word32 where
parseCWs = genParse (KBounded False 32)
-- | 'Int32' as extracted from a model
instance SatModel Int32 where
parseCWs = genParse (KBounded True 32)
-- | 'Word64' as extracted from a model
instance SatModel Word64 where
parseCWs = genParse (KBounded False 64)
-- | 'Int64' as extracted from a model
instance SatModel Int64 where
parseCWs = genParse (KBounded True 64)
-- | 'Integer' as extracted from a model
instance SatModel Integer where
parseCWs = genParse KUnbounded
-- | 'AlgReal' as extracted from a model
instance SatModel AlgReal where
parseCWs (CW KReal (CWAlgReal i) : r) = Just (i, r)
parseCWs _ = Nothing
-- | 'Float' as extracted from a model
instance SatModel Float where
parseCWs (CW KFloat (CWFloat i) : r) = Just (i, r)
parseCWs _ = Nothing
-- | 'Double' as extracted from a model
instance SatModel Double where
parseCWs (CW KDouble (CWDouble i) : r) = Just (i, r)
parseCWs _ = Nothing
instance SatModel CW where
parseCWs (cw : r) = Just (cw, r)
parseCWs [] = Nothing
-- when reading a list; go as long as we can (maximal-munch)
-- note that this never fails..
-- | A list of values as extracted from a model. When reading a list, we
-- go as long as we can (maximal-munch). Note that this never fails, as
-- we can always return the empty list!
instance SatModel a => SatModel [a] where
parseCWs [] = Just ([], [])
parseCWs xs = case parseCWs xs of
@ -231,31 +180,37 @@ instance SatModel a => SatModel [a] where
Nothing -> Just ([], ys)
Nothing -> Just ([], xs)
-- | Tuples extracted from a model
instance (SatModel a, SatModel b) => SatModel (a, b) where
parseCWs as = do (a, bs) <- parseCWs as
(b, cs) <- parseCWs bs
return ((a, b), cs)
-- | 3-Tuples extracted from a model
instance (SatModel a, SatModel b, SatModel c) => SatModel (a, b, c) where
parseCWs as = do (a, bs) <- parseCWs as
((b, c), ds) <- parseCWs bs
return ((a, b, c), ds)
-- | 4-Tuples extracted from a model
instance (SatModel a, SatModel b, SatModel c, SatModel d) => SatModel (a, b, c, d) where
parseCWs as = do (a, bs) <- parseCWs as
((b, c, d), es) <- parseCWs bs
return ((a, b, c, d), es)
-- | 5-Tuples extracted from a model
instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e) => SatModel (a, b, c, d, e) where
parseCWs as = do (a, bs) <- parseCWs as
((b, c, d, e), fs) <- parseCWs bs
return ((a, b, c, d, e), fs)
-- | 6-Tuples extracted from a model
instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f) => SatModel (a, b, c, d, e, f) where
parseCWs as = do (a, bs) <- parseCWs as
((b, c, d, e, f), gs) <- parseCWs bs
return ((a, b, c, d, e, f), gs)
-- | 7-Tuples extracted from a model
instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f, SatModel g) => SatModel (a, b, c, d, e, f, g) where
parseCWs as = do (a, bs) <- parseCWs as
((b, c, d, e, f, g), hs) <- parseCWs bs
@ -268,6 +223,19 @@ class Modelable a where
-- | Extract a model, the result is a tuple where the first argument (if True)
-- indicates whether the model was "probable". (i.e., if the solver returned unknown.)
getModel :: SatModel b => a -> Either String (Bool, b)
-- | Extract a model dictionary. Extract a dictionary mapping the variables to
-- their respective values as returned by the SMT solver. Also see `getModelDictionaries`.
getModelDictionary :: a -> M.Map String CW
-- | Extract a model value for a given element. Also see `getModelValues`.
getModelValue :: SymWord b => String -> a -> Maybe b
getModelValue v r = fromCW `fmap` (v `M.lookup` getModelDictionary r)
-- | Extract a representative name for the model value of an uninterpreted kind.
-- This is supposed to correspond to the value as computed internally by the
-- SMT solver; and is unportable from solver to solver. Also see `getModelUninterpretedValues`.
getModelUninterpretedValue :: String -> a -> Maybe String
getModelUninterpretedValue v r = case v `M.lookup` getModelDictionary r of
Just (CW _ (CWUninterpreted s)) -> Just s
_ -> Nothing
-- | A simpler variant of 'getModel' to get a model out without the fuss.
extractModel :: SatModel b => a -> Maybe b
@ -280,14 +248,31 @@ class Modelable a where
extractModels :: SatModel a => AllSatResult -> [a]
extractModels (AllSatResult (_, xs)) = [ms | Right (_, ms) <- map getModel xs]
-- | Get dictionaries from an all-sat call. Similar to `getModelDictionary`.
getModelDictionaries :: AllSatResult -> [M.Map String CW]
getModelDictionaries (AllSatResult (_, xs)) = map getModelDictionary xs
-- | Extract value of a variable from an all-sat call. Similar to `getModelValue`.
getModelValues :: SymWord b => String -> AllSatResult -> [Maybe b]
getModelValues s (AllSatResult (_, xs)) = map (s `getModelValue`) xs
-- | Extract value of an uninterpreted variable from an all-sat call. Similar to `getModelUninterpretedValue`.
getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String]
getModelUninterpretedValues s (AllSatResult (_, xs)) = map (s `getModelUninterpretedValue`) xs
-- | 'ThmResult' as a generic model provider
instance Modelable ThmResult where
getModel (ThmResult r) = getModel r
modelExists (ThmResult r) = modelExists r
getModel (ThmResult r) = getModel r
modelExists (ThmResult r) = modelExists r
getModelDictionary (ThmResult r) = getModelDictionary r
-- | 'SatResult' as a generic model provider
instance Modelable SatResult where
getModel (SatResult r) = getModel r
modelExists (SatResult r) = modelExists r
getModel (SatResult r) = getModel r
modelExists (SatResult r) = modelExists r
getModelDictionary (SatResult r) = getModelDictionary r
-- | 'SMTResult' as a generic model provider
instance Modelable SMTResult where
getModel (Unsatisfiable _) = Left "SBV.getModel: Unsatisfiable result"
getModel (Unknown _ m) = Right (True, parseModelOut m)
@ -297,6 +282,11 @@ instance Modelable SMTResult where
modelExists (Satisfiable{}) = True
modelExists (Unknown{}) = False -- don't risk it
modelExists _ = False
getModelDictionary (Unsatisfiable _) = M.empty
getModelDictionary (Unknown _ m) = M.fromList (modelAssocs m)
getModelDictionary (ProofError _ _) = M.empty
getModelDictionary (TimeOut _) = M.empty
getModelDictionary (Satisfiable _ m) = M.fromList (modelAssocs m)
-- | Extract a model out, will throw error if parsing is unsuccessful
parseModelOut :: SatModel a => SMTModel -> a
@ -357,8 +347,9 @@ shUA (f, cases) = (" -- array: " ++ f) : map shC cases
where shC s = " " ++ s
-- | Helper function to spin off to an SMT solver.
pipeProcess :: SMTConfig -> String -> String -> [String] -> SMTScript -> (String -> String) -> IO (Either String [String])
pipeProcess cfg nm execName opts script cleanErrs = do
pipeProcess :: SMTConfig -> String -> [String] -> SMTScript -> (String -> String) -> IO (Either String [String])
pipeProcess cfg execName opts script cleanErrs = do
let nm = show (name (solver cfg))
mbExecPath <- findExecutable execName
case mbExecPath of
Nothing -> return $ Left $ "Unable to locate executable for " ++ nm
@ -397,13 +388,13 @@ standardSolver config script cleanErrs failure success = do
exec = executable smtSolver
opts = options smtSolver
isTiming = timing config
nmSolver = name smtSolver
nmSolver = show (name smtSolver)
msg $ "Calling: " ++ show (unwords (exec:opts))
case smtFile config of
Nothing -> return ()
Just f -> do putStrLn $ "** Saving the generated script in file: " ++ show f
Just f -> do msg $ "Saving the generated script in file: " ++ show f
writeFile f (scriptBody script)
contents <- timeIf isTiming nmSolver $ pipeProcess config nmSolver exec opts script cleanErrs
contents <- timeIf isTiming nmSolver $ pipeProcess config exec opts script cleanErrs
msg $ nmSolver ++ " output:\n" ++ either id (intercalate "\n") contents
case contents of
Left e -> return $ failure (lines e)
@ -413,41 +404,46 @@ standardSolver config script cleanErrs failure success = do
-- and can speak SMT-Lib2 (just a little).
runSolver :: SMTConfig -> FilePath -> [String] -> SMTScript -> IO (ExitCode, String, String)
runSolver cfg execPath opts script
| isNothing $ scriptModel script
= let checkCmd | useSMTLib2 cfg = '\n' : satCmd cfg
| True = ""
in readProcessWithExitCode execPath opts (scriptBody script ++ checkCmd)
| True
= do (send, ask, cleanUp) <- do
= do (send, ask, cleanUp, pid) <- do
(inh, outh, errh, pid) <- runInteractiveProcess execPath opts Nothing Nothing
let send l = hPutStr inh (l ++ "\n") >> hFlush inh
recv = hGetLine outh `C.catch` (\(_ :: C.SomeException) -> return "")
recv = hGetLine outh
ask l = send l >> recv
cleanUp r = do outMVar <- newEmptyMVar
out <- hGetContents outh
_ <- forkIO $ C.evaluate (length out) >> putMVar outMVar ()
err <- hGetContents errh
_ <- forkIO $ C.evaluate (length err) >> putMVar outMVar ()
hClose inh
takeMVar outMVar
takeMVar outMVar
hClose outh
hClose errh
ex <- waitForProcess pid
-- if the status is unknown, prepare for the possibility of not having a model
-- TBD: This is rather crude and potentially Z3 specific
return $ if "unknown" `isPrefixOf` r && "error" `isInfixOf` (out ++ err)
then (ExitSuccess, r , "")
else (ex, r ++ "\n" ++ out, err)
return (send, ask, cleanUp)
mapM_ send (lines (scriptBody script))
r <- ask $ satCmd cfg
when (any (`isPrefixOf` r) ["sat", "unknown"]) $ do
let mls = lines (fromJust (scriptModel script))
when (verbose cfg) $ do putStrLn "** Sending the following model extraction commands:"
mapM_ putStrLn mls
mapM_ send mls
cleanUp r
cleanUp response
= do hClose inh
outMVar <- newEmptyMVar
out <- hGetContents outh
_ <- forkIO $ C.evaluate (length out) >> putMVar outMVar ()
err <- hGetContents errh
_ <- forkIO $ C.evaluate (length err) >> putMVar outMVar ()
takeMVar outMVar
takeMVar outMVar
hClose outh
hClose errh
ex <- waitForProcess pid
return $ case response of
Nothing -> (ex, out, err)
Just (r, vals) -> -- if the status is unknown, prepare for the possibility of not having a model
-- TBD: This is rather crude and potentially Z3 specific
let finalOut = intercalate "\n" (r : vals)
in if "unknown" `isPrefixOf` r && "error" `isInfixOf` (out ++ err)
then (ExitSuccess, finalOut , "")
else (ex, finalOut ++ "\n" ++ out, err)
return (send, ask, cleanUp, pid)
let executeSolver = do mapM_ send (lines (scriptBody script))
response <- case scriptModel script of
Nothing -> do send $ satCmd cfg
return Nothing
Just ls -> do r <- ask $ satCmd cfg
vals <- if any (`isPrefixOf` r) ["sat", "unknown"]
then do let mls = lines ls
when (verbose cfg) $ do putStrLn "** Sending the following model extraction commands:"
mapM_ putStrLn mls
mapM ask mls
else return []
return $ Just (r, vals)
cleanUp response
executeSolver `C.onException` terminateProcess pid
-- | In case the SMT-Lib solver returns a response over multiple lines, compress them so we have
-- each S-Expression spanning only a single line. We'll ignore things line parentheses inside quotes

6
sbv/Data/SBV/SMT/SMTLib.hs
View File

@ -14,7 +14,6 @@ module Data.SBV.SMT.SMTLib(SMTLibPgm, SMTLibConverter, toSMTLib1, toSMTLib2, add
import Data.Char (isDigit)
import Data.SBV.BitVectors.Data
import Data.SBV.SMT.SMT
import Data.SBV.Provers.SExpr
import qualified Data.SBV.SMT.SMTLib1 as SMT1
import qualified Data.SBV.SMT.SMTLib2 as SMT2
@ -23,6 +22,7 @@ import qualified Data.Set as Set (Set, member, toList)
-- | An instance of SMT-Lib converter; instantiated for SMT-Lib v1 and v2. (And potentially for newer versions in the future.)
type SMTLibConverter = RoundingMode -- ^ User selected rounding mode to be used for floating point arithmetic
-> Maybe Logic -- ^ User selected logic to use. If Nothing, pick automatically.
-> SolverCapabilities -- ^ Capabilities of the backend solver targeted
-> Set.Set Kind -- ^ Kinds used in the problem
-> Bool -- ^ is this a sat problem?
@ -45,7 +45,7 @@ toSMTLib1 :: SMTLibConverter
-- | Convert to SMTLib-2 format
toSMTLib2 :: SMTLibConverter
(toSMTLib1, toSMTLib2) = (cvt SMTLib1, cvt SMTLib2)
where cvt v roundMode solverCaps kindInfo isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out
where cvt v roundMode smtLogic solverCaps kindInfo isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out
| KUnbounded `Set.member` kindInfo && not (supportsUnboundedInts solverCaps)
= unsupported "unbounded integers"
| KReal `Set.member` kindInfo && not (supportsReals solverCaps)
@ -64,7 +64,7 @@ toSMTLib2 :: SMTLibConverter
unsupported w = error $ "SBV: Given problem needs " ++ w ++ ", which is not supported by SBV for the chosen solver: " ++ capSolverName solverCaps
aliasTable = map (\(_, (x, y)) -> (y, x)) qinps
converter = if v == SMTLib1 then SMT1.cvt else SMT2.cvt
(pre, post) = converter roundMode solverCaps kindInfo isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out
(pre, post) = converter roundMode smtLogic solverCaps kindInfo isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out
needsFloats = KFloat `Set.member` kindInfo
needsDoubles = KDouble `Set.member` kindInfo
needsQuantifiers

8
sbv/Data/SBV/SMT/SMTLib1.hs
View File

@ -42,6 +42,7 @@ nonEq (s, c) = "(not (= " ++ s ++ " " ++ cvtCW c ++ "))"
-- | Translate a problem into an SMTLib1 script
cvt :: RoundingMode -- ^ User selected rounding mode to be used for floating point arithmetic
-> Maybe Logic -- ^ SMT-Lib logic, if requested by the user
-> SolverCapabilities -- ^ capabilities of the current solver
-> Set.Set Kind -- ^ kinds used
-> Bool -- ^ is this a sat problem?
@ -57,8 +58,9 @@ cvt :: RoundingMode -- ^ User selected rounding mode to be used
-> [SW] -- ^ extra constraints
-> SW -- ^ output variable
-> ([String], [String])
cvt _roundingMode _solverCaps _kindInfo isSat comments qinps _skolemInps consts tbls arrs uis axs asgnsSeq cstrs out = (pre, post)
cvt _roundingMode smtLogic _solverCaps _kindInfo isSat comments qinps _skolemInps consts tbls arrs uis axs asgnsSeq cstrs out = (pre, post)
where logic
| Just l <- smtLogic = show l
| null tbls && null arrs && null uis = "QF_BV"
| True = "QF_AUFBV"
inps = map (fst . snd) qinps
@ -152,7 +154,7 @@ cvtCnst (s, c) = " :assumption (= " ++ show s ++ " " ++ cvtCW c ++ ")"
-- no need to worry about Int/Real here as we don't support them with the SMTLib1 interface..
cvtCW :: CW -> String
cvtCW (CW (KBounded False 1) (CWInteger v)) = if v == 0 then "false" else "true"
cvtCW (CW KBool (CWInteger v)) = if v == 0 then "false" else "true"
cvtCW x@(CW _ (CWInteger v)) | not (hasSign x) = "bv" ++ show v ++ "[" ++ show (intSizeOf x) ++ "]"
-- signed numbers (with 2's complement representation) is problematic
-- since there's no way to put a bvneg over a positive number to get minBound..
@ -261,7 +263,7 @@ cvtType (SBVType []) = error "SBV.SMT.SMTLib1.cvtType: internal: received an emp
cvtType (SBVType xs) = unwords $ map kindType xs
kindType :: Kind -> String
kindType (KBounded False 1) = "Bool"
kindType KBool = "Bool"
kindType (KBounded _ s) = "BitVec[" ++ show s ++ "]"
kindType KUnbounded = die "unbounded Integer"
kindType KReal = die "real value"

63
sbv/Data/SBV/SMT/SMTLib2.hs
View File

@ -12,13 +12,15 @@
module Data.SBV.SMT.SMTLib2(cvt, addNonEqConstraints) where
import Data.Bits (bit)
import Data.Char (intToDigit)
import Data.Bits (bit)
import Data.Char (intToDigit)
import Data.Function (on)
import Data.Ord (comparing)
import qualified Data.Foldable as F (toList)
import qualified Data.Map as M
import qualified Data.IntMap as IM
import qualified Data.Set as Set
import Data.List (intercalate, partition)
import Data.List (intercalate, partition, groupBy, sortBy)
import Numeric (showIntAtBase, showHex)
import Data.SBV.BitVectors.AlgReals
@ -36,7 +38,7 @@ addNonEqConstraints rm qinps allNonEqConstraints (SMTLibPgm _ (aliasTable, pre,
| True
= Just $ intercalate "\n" $ pre
++ [ "; --- refuted-models ---" ]
++ concatMap (nonEqs rm) (map (map intName) nonEqConstraints)
++ refutedModel
++ post
where refutedModel = concatMap (nonEqs rm) (map (map intName) nonEqConstraints)
intName (s, c)
@ -47,11 +49,27 @@ addNonEqConstraints rm qinps allNonEqConstraints (SMTLibPgm _ (aliasTable, pre,
topUnivs = [s | (_, (_, s)) <- takeWhile (\p -> fst p == EX) qinps]
nonEqs :: RoundingMode -> [(String, CW)] -> [String]
nonEqs _ [] = []
nonEqs rm [sc] = ["(assert " ++ nonEq rm sc ++ ")"]
nonEqs rm (sc:r) = ["(assert (or " ++ nonEq rm sc]
++ map ((" " ++) . nonEq rm) r
++ [" ))"]
nonEqs rm scs = format $ interp ps ++ disallow (map eqClass uninterpClasses)
where (ups, ps) = partition (isUninterpreted . snd) scs
format [] = []
format [m] = ["(assert " ++ m ++ ")"]
format (m:ms) = ["(assert (or " ++ m]
++ map (" " ++) ms
++ [" ))"]
-- Regular (or interpreted) sorts simply get a constraint that we disallow the current assignment
interp = map $ nonEq rm
-- Determine the equivalnce classes of uninterpreted sorts:
uninterpClasses = filter (\l -> length l > 1) -- Only need this class if it has at least two members
. map (map fst) -- throw away sorts, we only need the names
. groupBy ((==) `on` snd) -- make sure they belong to the same sort and have the same value
. sortBy (comparing snd) -- sort them according to their sorts first
$ ups -- take the uninterpreted sorts
-- Uninterpreted sorts get a constraint that says the equivalence classes as determined by the solver are disallowed:
eqClass :: [String] -> String
eqClass [] = error "SBV.allSat.nonEqs: Impossible happened, disallow received an empty list"
eqClass cs = "(= " ++ unwords cs ++ ")"
-- Now, take the conjunction of equivalence classes and assert it's negation:
disallow = map $ \ec -> "(not " ++ ec ++ ")"
nonEq :: RoundingMode -> (String, CW) -> String
nonEq rm (s, c) = "(not (= " ++ s ++ " " ++ cvtCW rm c ++ "))"
@ -61,6 +79,7 @@ tbd e = error $ "SBV.SMTLib2: Not-yet-supported: " ++ e
-- | Translate a problem into an SMTLib2 script
cvt :: RoundingMode -- ^ User selected rounding mode to be used for floating point arithmetic
-> Maybe Logic -- ^ SMT-Lib logic, if requested by the user
-> SolverCapabilities -- ^ capabilities of the current solver
-> Set.Set Kind -- ^ kinds used
-> Bool -- ^ is this a sat problem?
@ -76,7 +95,7 @@ cvt :: RoundingMode -- ^ User selected rounding mode to be used
-> [SW] -- ^ extra constraints
-> SW -- ^ output variable
-> ([String], [String])
cvt rm solverCaps kindInfo isSat comments inputs skolemInps consts tbls arrs uis axs (SBVPgm asgnsSeq) cstrs out = (pre, [])
cvt rm smtLogic solverCaps kindInfo isSat comments inputs skolemInps consts tbls arrs uis axs (SBVPgm asgnsSeq) cstrs out = (pre, [])
where -- the logic is an over-approaximation
hasInteger = KUnbounded `Set.member` kindInfo
hasReal = KReal `Set.member` kindInfo
@ -85,6 +104,8 @@ cvt rm solverCaps kindInfo isSat comments inputs skolemInps consts tbls arrs uis
hasBVs = not $ null [() | KBounded{} <- Set.toList kindInfo]
sorts = [s | KUninterpreted s <- Set.toList kindInfo]
logic
| Just l <- smtLogic
= ["(set-logic " ++ show l ++ ") ; NB. User specified."]
| hasDouble || hasFloat -- NB. We don't check for quantifiers here, we probably should..
= if hasBVs
then ["(set-logic QF_FPABV)"]
@ -244,7 +265,7 @@ swFunType :: [SW] -> SW -> String
swFunType ss s = "(" ++ unwords (map swType ss) ++ ") " ++ swType s
smtType :: Kind -> String
smtType (KBounded False 1) = "Bool"
smtType KBool = "Bool"
smtType (KBounded _ sz) = "(_ BitVec " ++ show sz ++ ")"
smtType KUnbounded = "Int"
smtType KReal = "Real"
@ -267,14 +288,16 @@ cvtSW skolemMap s
| True
= show s
-- SMTLib2 requires the width of literals to match the type exactly;
-- hexadecimal works only for sizes that are multiples of 4.
-- Carefully code hex numbers, SMTLib is picky about lengths of hex constants. For the time
-- being, SBV only supports sizes that are multiples of 4, but the below code is more robust
-- in case of future extensions to support arbitrary sizes.
hex :: Int -> Integer -> String
hex 1 v = "#b" ++ show v
hex sz v
| sz `mod` 4 == 0 = "#x" ++ pad (sz `div` 4) (showHex v "")
| otherwise = "#b" ++ pad sz (showBin v "")
where pad n s = replicate (n - length s) '0' ++ s
showBin = showIntAtBase 2 intToDigit
| True = "#b" ++ pad sz (showBin v "")
where pad n s = replicate (n - length s) '0' ++ s
showBin = showIntAtBase 2 intToDigit
cvtCW :: RoundingMode -> CW -> String
cvtCW rm x
@ -318,7 +341,8 @@ cvtExp rm skolemMap tableMap expr@(SBVApp _ arguments) = sh expr
boolOp = all isBoolean arguments
bad | intOp = error $ "SBV.SMTLib2: Unsupported operation on unbounded integers: " ++ show expr
| True = error $ "SBV.SMTLib2: Unsupported operation on real values: " ++ show expr
ensureBV = bvOp || bad
ensureBVOrBool = bvOp || boolOp || bad
ensureBV = bvOp || bad
addRM s = s ++ " " ++ smtRoundingMode rm
lift2 o _ [x, y] = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")"
lift2 o _ sbvs = error $ "SBV.SMTLib2.sh.lift2: Unexpected arguments: " ++ show (o, sbvs)
@ -351,6 +375,7 @@ cvtExp rm skolemMap tableMap expr@(SBVApp _ arguments) = sh expr
| needsCheck = "(ite " ++ cond ++ ssw e ++ " " ++ lkUp ++ ")"
| True = lkUp
where needsCheck = case aKnd of
KBool -> (2::Integer) > fromIntegral l
KBounded _ n -> (2::Integer)^n > fromIntegral l
KUnbounded -> True
KReal -> error "SBV.SMT.SMTLib2.cvtExp: unexpected real valued index"
@ -362,6 +387,7 @@ cvtExp rm skolemMap tableMap expr@(SBVApp _ arguments) = sh expr
| hasSign i = "(or " ++ le0 ++ " " ++ gtl ++ ") "
| True = gtl ++ " "
(less, leq) = case aKnd of
KBool -> error "SBV.SMT.SMTLib2.cvtExp: unexpected boolean valued index"
KBounded{} -> if hasSign i then ("bvslt", "bvsle") else ("bvult", "bvule")
KUnbounded -> ("<", "<=")
KReal -> ("<", "<=")
@ -402,7 +428,7 @@ cvtExp rm skolemMap tableMap expr@(SBVApp _ arguments) = sh expr
| intOp = "(div " ++ ssw a ++ " " ++ show (bit i :: Integer) ++ ")" -- Implement shiftR by division by 2^i
| True = bad
sh (SBVApp op args)
| Just f <- lookup op smtBVOpTable, ensureBV
| Just f <- lookup op smtBVOpTable, ensureBVOrBool
= f (any hasSign args) (map ssw args)
where -- The first 4 operators below do make sense for Integer's in Haskell, but there's
-- no obvious counterpart for them in the SMTLib translation.
@ -446,6 +472,7 @@ cvtExp rm skolemMap tableMap expr@(SBVApp _ arguments) = sh expr
, (Rem, lift2 "mod")
]
smtOpFloatDoubleTable = smtIntRealShared
++ [(Quot, lift2WM "/")]
smtIntRealShared = [ (Plus, lift2WM "+")
, (Minus, lift2WM "-")
, (Times, lift2WM "*")

8
sbv/Data/SBV/Tools/ExpectedValue.hs
View File

@ -22,13 +22,13 @@ import Data.SBV.BitVectors.Data
-- warm-up count and the convergence factor. Maximum iteration count can also
-- be specified, at which point convergence won't be sought. The boolean controls verbosity.
expectedValueWith :: Outputtable a => Bool -> Int -> Maybe Int -> Double -> Symbolic a -> IO [Double]
expectedValueWith verbose warmupCount mbMaxIter epsilon m
expectedValueWith chatty warmupCount mbMaxIter epsilon m
| warmupCount < 0 || epsilon < 0
= error $ "SBV.expectedValue: warmup count and epsilon both must be non-negative, received: " ++ show (warmupCount, epsilon)
| True
= warmup warmupCount (repeat 0) >>= go warmupCount
where progress s | not verbose = return ()
| True = putStr $ "\r*** " ++ s
where progress s | not chatty = return ()
| True = putStr $ "\r*** " ++ s
warmup :: Int -> [Integer] -> IO [Integer]
warmup 0 v = do progress $ "Warmup complete, performed " ++ show warmupCount ++ " rounds.\n"
return v
@ -42,7 +42,7 @@ expectedValueWith verbose warmupCount mbMaxIter epsilon m
let cval o = case o `lookup` cs of
Nothing -> error "SBV.expectedValue: Cannot compute expected-values in the presence of uninterpreted constants!"
Just cw -> case (cwKind cw, cwVal cw) of
(KBounded False 1, _) -> if cwToBool cw then 1 else 0
(KBool, _) -> if cwToBool cw then 1 else 0
(KBounded{}, CWInteger v) -> v
(KUnbounded, CWInteger v) -> v
(KReal, _) -> error "Cannot compute expected-values for real valued results."

16
sbv/Data/SBV/Tools/GenTest.hs
View File

@ -111,7 +111,7 @@ haskell vname vs = intercalate "\n" $ [ "-- Automatically generated by SBV. Do n
valOf [x] = s x
valOf xs = "[" ++ intercalate ", " (map s xs) ++ "]"
t cw = case kindOf cw of
KBounded False 1 -> "Bool"
KBool -> "Bool"
KBounded False 8 -> "Word8"
KBounded False 16 -> "Word16"
KBounded False 32 -> "Word32"
@ -127,7 +127,7 @@ haskell vname vs = intercalate "\n" $ [ "-- Automatically generated by SBV. Do n
KUninterpreted us -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us
_ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw
s cw = case cwKind cw of
KBounded False 1 -> take 5 (show (cwToBool cw) ++ repeat ' ')
KBool -> take 5 (show (cwToBool cw) ++ repeat ' ')
KBounded sgn sz -> let CWInteger w = cwVal cw in shex False True (sgn, sz) w
KUnbounded -> let CWInteger w = cwVal cw in shexI False True w
KFloat -> let CWFloat w = cwVal cw in showHFloat w
@ -198,7 +198,7 @@ c n vs = intercalate "\n" $
]
where mkField p cw i = " " ++ t ++ " " ++ p ++ show i ++ ";"
where t = case cwKind cw of
KBounded False 1 -> "SBool"
KBool -> "SBool"
KBounded False 8 -> "SWord8"
KBounded False 16 -> "SWord16"
KBounded False 32 -> "SWord32"
@ -215,7 +215,7 @@ c n vs = intercalate "\n" $
_ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw
mkLine (is, os) = "{{" ++ intercalate ", " (map v is) ++ "}, {" ++ intercalate ", " (map v os) ++ "}}"
v cw = case cwKind cw of
KBounded False 1 -> if cwToBool cw then "true " else "false"
KBool -> if cwToBool cw then "true " else "false"
KBounded sgn sz -> let CWInteger w = cwVal cw in shex False True (sgn, sz) w
KUnbounded -> let CWInteger w = cwVal cw in shexI False True w
KFloat -> let CWFloat w = cwVal cw in showCFloat w
@ -231,11 +231,11 @@ c n vs = intercalate "\n" $
inp cw i = mkBool cw (n ++ "[i].input.i" ++ show i)
out cw i = mkBool cw (n ++ "[i].output.o" ++ show i)
mkBool cw s = case cwKind cw of
KBounded False 1 -> "(" ++ s ++ " == true) ? \"true \" : \"false\""
_ -> s
KBool -> "(" ++ s ++ " == true) ? \"true \" : \"false\""
_ -> s
fmtString = unwords (map fmt is) ++ " -> " ++ unwords (map fmt os)
fmt cw = case cwKind cw of
KBounded False 1 -> "%s"
KBool -> "%s"
KBounded False 8 -> "0x%02\"PRIx8\""
KBounded False 16 -> "0x%04\"PRIx16\"U"
KBounded False 32 -> "0x%08\"PRIx32\"UL"
@ -267,7 +267,7 @@ forte vname bigEndian ss vs = intercalate "\n" $ [ "// Automatically generated b
toF True = '1'
toF False = '0'
blast cw = case cwKind cw of
KBounded False 1 -> [toF (cwToBool cw)]
KBool -> [toF (cwToBool cw)]
KBounded False 8 -> xlt 8 (cwVal cw)
KBounded False 16 -> xlt 16 (cwVal cw)
KBounded False 32 -> xlt 32 (cwVal cw)

2
sbv/Data/SBV/Tools/Optimize.hs
View File

@ -19,7 +19,7 @@ import Data.Maybe (fromJust)
import Data.SBV.BitVectors.Data
import Data.SBV.BitVectors.Model (OrdSymbolic(..), EqSymbolic(..))
import Data.SBV.Provers.Prover (satWith, defaultSMTCfg)
import Data.SBV.SMT.SMT (SatModel, getModel, SMTConfig(..))
import Data.SBV.SMT.SMT (SatModel, getModel)
import Data.SBV.Utils.Boolean
-- | Optimizer configuration. Note that iterative and quantified approaches are in general not interchangeable.

7
sbv/Data/SBV/Tools/Polynomial.hs
View File

@ -9,12 +9,13 @@
-- Implementation of polynomial arithmetic
-----------------------------------------------------------------------------
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Data.SBV.Tools.Polynomial {-(Polynomial(..), crc, crcBV)-} where
module Data.SBV.Tools.Polynomial (Polynomial(..), crc, crcBV, ites, addPoly, mdp) where
import Data.Bits (Bits(..))
import Data.List (genericTake)
@ -100,7 +101,11 @@ sp st a
| True = foldr (\x y -> sh x ++ " + " ++ y) (sh (last cs)) (init cs) ++ t
where t | st = " :: GF(2^" ++ show n ++ ")"
| True = ""
#if __GLASGOW_HASKELL__ >= 708
n = maybe (error "SBV.Polynomial.sp: Unexpected non-finite usage!") id (bitSizeMaybe a)
#else
n = bitSize a
#endif
is = [n-1, n-2 .. 0]
cs = map fst $ filter snd $ zip is (map (testBit a) is)
sh 0 = "1"

4
src/Cryptol/Eval.hs
View File

@ -45,7 +45,7 @@ evalExpr env expr = case expr of
EList es ty -> evalList env es (evalType env ty)
ETuple es -> VTuple (length es) (map eval es)
ETuple es -> VTuple (map eval es)
ERec fields -> VRecord [ (f,eval e) | (f,e) <- fields ]
@ -139,7 +139,7 @@ evalSel env e sel = case sel of
tupleSel n v =
case v of
VTuple _ vs -> vs !! (n - 1)
VTuple vs -> vs !! (n - 1)
VSeq False vs -> VSeq False [ tupleSel n v1 | v1 <- vs ]
VStream vs -> VStream [ tupleSel n v1 | v1 <- vs ]
VFun f -> VFun (\x -> tupleSel n (f x))

97
src/Cryptol/Eval/Value.hs
View File

@ -74,20 +74,25 @@ finTValue tval =
-- Values ----------------------------------------------------------------------
data Value
= VRecord [(Name,Value)] -- @ { .. } @
| VTuple Int [Value] -- @ ( .. ) @
| VBit Bool -- @ Bit @
| VSeq Bool [Value] -- @ [n]a @
-- The boolean parameter indicates whether or not
-- this is a sequence of bits.
| VWord Integer Integer -- @ [n]Bit @ width,value.
-- The value may contain junk bits
| VStream [Value] -- @ [inf]a @
| VFun (Value -> Value) -- functions
| VPoly (TValue -> Value) -- polymorphic values (kind *)
data BV = BV !Integer !Integer -- ^ width, value
-- The value may contain junk bits
-- | Generic value type, parameterized by bit and word types.
data GenValue b w
= VRecord [(Name, GenValue b w)] -- @ { .. } @
| VTuple [GenValue b w] -- @ ( .. ) @
| VBit b -- @ Bit @
| VSeq Bool [GenValue b w] -- @ [n]a @
-- The boolean parameter indicates whether or not
-- this is a sequence of bits.
| VWord w -- @ [n]Bit @
| VStream [GenValue b w] -- @ [inf]a @
| VFun (GenValue b w -> GenValue b w) -- functions
| VPoly (TValue -> GenValue b w) -- polymorphic values (kind *)
type Value = GenValue Bool BV
-- | An evaluated type.
-- These types do not contain type variables, type synonyms, or type functions.
newtype TValue = TValue { tValTy :: Type }
@ -114,13 +119,13 @@ ppValue opts = loop
VRecord fs -> braces (sep (punctuate comma (map ppField fs)))
where
ppField (f,r) = pp f <+> char '=' <+> loop r
VTuple _ vals -> parens (sep (punctuate comma (map loop vals)))
VTuple vals -> parens (sep (punctuate comma (map loop vals)))
VBit b | b -> text "True"
| otherwise -> text "False"
VSeq isWord vals
| isWord -> uncurry (ppWord opts) (fromVWord val)
| isWord -> ppWord opts (fromVWord val)
| otherwise -> ppWordSeq vals
VWord w i -> ppWord opts w (mask w i)
VWord (BV w i) -> ppWord opts (BV w (mask w i))
VStream vals -> brackets $ fsep
$ punctuate comma
( take (useInfLength opts) (map loop vals)
@ -149,8 +154,8 @@ data WithBase a = WithBase PPOpts a
instance PP (WithBase Value) where
ppPrec _ (WithBase opts v) = ppValue opts v
ppWord :: PPOpts -> Integer -> Integer -> Doc
ppWord opts width i
ppWord :: PPOpts -> BV -> Doc
ppWord opts (BV width i)
| base > 36 = integer i -- not sure how to rule this out
| asciiMode opts width = text (show (toEnum (fromInteger i) :: Char))
| otherwise = prefix <> text value
@ -186,8 +191,8 @@ mask w i = i .&. ((1 `shiftL` fromInteger w) - 1)
-- NOTE this assumes that the sequence of bits is big-endian and finite, so the
-- first element of the list will be the most significant bit.
packWord :: [Bool] -> (Integer,Integer)
packWord bits = (toInteger w,a)
packWord :: [Bool] -> BV
packWord bits = BV (toInteger w) a
where
w = length bits
a = foldl set 0 (zip [w - 1, w - 2 .. 0] bits)
@ -196,8 +201,8 @@ packWord bits = (toInteger w,a)
-- NOTE this produces a list of bits that represent a big-endian word, so the
-- most significant bit is the first element of the list.
unpackWord :: Integer -> Integer -> [Bool]
unpackWord w a = [ testBit a n | n <- [w' - 1, w' - 2 .. 0] ]
unpackWord :: BV -> [Bool]
unpackWord (BV w a) = [ testBit a n | n <- [w' - 1, w' - 2 .. 0] ]
where
w' = fromInteger w
@ -206,29 +211,29 @@ unpackWord w a = [ testBit a n | n <- [w' - 1, w' - 2 .. 0] ]
-- | Create a packed word of n bits.
word :: Integer -> Integer -> Value
word n i = VWord n (mask n i)
word n i = VWord (BV n (mask n i))
lam :: (Value -> Value) -> Value
lam :: (GenValue b w -> GenValue b w) -> GenValue b w
lam = VFun
-- | A type lambda that expects a @Type@.
tlam :: (TValue -> Value) -> Value
tlam :: (TValue -> GenValue b w) -> GenValue b w
tlam = VPoly
-- | Generate a stream.
toStream :: [Value] -> Value
toStream :: [GenValue b w] -> GenValue b w
toStream = VStream
toFinSeq :: TValue -> [Value] -> Value
toFinSeq :: TValue -> [GenValue b w] -> GenValue b w
toFinSeq elty = VSeq (isTBit elty)
-- | This is strict!
boolToWord :: [Bool] -> Value
boolToWord = uncurry VWord . packWord
boolToWord = VWord . packWord
-- | Construct either a finite sequence, or a stream. In the finite case,
-- record whether or not the elements were bits, to aid pretty-printing.
toSeq :: TValue -> TValue -> [Value] -> Value
toSeq :: TValue -> TValue -> [GenValue b w] -> GenValue b w
toSeq len elty vals = case numTValue len of
Nat n -> toFinSeq elty (genericTake n vals)
Inf -> toStream vals
@ -254,7 +259,7 @@ toPackedSeq len elty vals = case numTValue len of
-- Value Destructors -----------------------------------------------------------
-- | Extract a bit value.
fromVBit :: Value -> Bool
fromVBit :: GenValue b w -> b
fromVBit val = case val of
VBit b -> b
_ -> evalPanic "fromVBit" ["not a Bit"]
@ -263,7 +268,7 @@ fromVBit val = case val of
fromSeq :: Value -> [Value]
fromSeq val = case val of
VSeq _ vs -> vs
VWord w a -> map VBit (unpackWord w a)
VWord bv -> map VBit (unpackWord bv)
VStream vs -> vs
_ -> evalPanic "fromSeq" ["not a sequence"]
@ -272,16 +277,16 @@ fromStr = map (toEnum . fromInteger . fromWord) . fromSeq
-- | Extract a packed word.
-- Note that this does not clean-up any junk bits in the word.
fromVWord :: Value -> (Integer,Integer)
fromVWord :: Value -> BV
fromVWord val = case val of
VWord w a -> (w,a) -- this should always mask
VWord bv -> bv -- this should always mask
VSeq isWord bs | isWord -> packWord (map fromVBit bs)
_ -> evalPanic "fromVWord"
["not a word", show $ ppValue defaultPPOpts val]
vWordLen :: Value -> Maybe Integer
vWordLen val = case val of
VWord w _ -> Just w
VWord (BV w _) -> Just w
VSeq isWord bs | isWord -> Just (toInteger (length bs))
_ -> Nothing
@ -290,28 +295,34 @@ vWordLen val = case val of
fromWord :: Value -> Integer
fromWord val = mask w a
where
(w,a) = fromVWord val
BV w a = fromVWord val
-- | Extract a function from a value.
fromVFun :: Value -> (Value -> Value)
fromVFun :: GenValue b w -> (GenValue b w -> GenValue b w)
fromVFun val = case val of
VFun f -> f
_ -> evalPanic "fromVFun" ["not a function"]
-- | Extract a polymorphic function from a value.
fromVPoly :: GenValue b w -> (TValue -> GenValue b w)
fromVPoly val = case val of
VPoly f -> f
_ -> evalPanic "fromVPoly" ["not a polymorphic value"]
-- | Extract a tuple from a value.
fromVTuple :: Value -> (Int,[Value])
fromVTuple :: GenValue b w -> [GenValue b w]
fromVTuple val = case val of
VTuple len vs -> (len,vs)
_ -> evalPanic "fromVTuple" ["not a tuple"]
VTuple vs -> vs
_ -> evalPanic "fromVTuple" ["not a tuple"]
-- | Extract a record from a value.
fromVRecord :: Value -> [(Name,Value)]
fromVRecord :: GenValue b w -> [(Name, GenValue b w)]
fromVRecord val = case val of
VRecord fs -> fs
_ -> evalPanic "fromVRecord" ["not a record"]
-- | Lookup a field in a record.
lookupRecord :: Name -> Value -> Value
lookupRecord :: Name -> GenValue b w -> GenValue b w
lookupRecord f rec = case lookup f (fromVRecord rec) of
Just val -> val
Nothing -> evalPanic "lookupRecord" ["malformed record"]
@ -329,8 +340,8 @@ toExpr ty val = case (ty, val) of
guard (map fst tfs == fns)
fes <- zipWithM toExpr (map snd tfs) (map snd vfs)
return $ ERec (zip fns fes)
(TCon (TC (TCTuple tl)) ts, VTuple l tvs) -> do
guard (tl == l)
(TCon (TC (TCTuple tl)) ts, VTuple tvs) -> do
guard (tl == (length tvs))
ETuple `fmap` zipWithM toExpr ts tvs
(TCon (TC TCBit) [], VBit True ) -> return $ ECon ECTrue
(TCon (TC TCBit) [], VBit False) -> return $ ECon ECFalse
@ -341,7 +352,7 @@ toExpr ty val = case (ty, val) of
guard (a == tNum (length svs))
ses <- mapM (toExpr b) svs
return $ EList ses b
(TCon (TC TCSeq) [a,(TCon (TC TCBit) [])], VWord w v) -> do
(TCon (TC TCSeq) [a,(TCon (TC TCBit) [])], VWord (BV w v)) -> do
guard (a == tNum w)
return $ ETApp (ETApp (ECon ECDemote) (tNum v)) (tNum w)
(_, VStream _) -> fail "cannot construct infinite expressions"

6
src/Cryptol/ModuleSystem.hs
View File

@ -57,10 +57,10 @@ loadModuleByPath path = do
return m
-- | Load the given parsed module.
loadModule :: P.Module -> ModuleCmd T.Module
loadModule m env = runModuleM env $ do
loadModule :: FilePath -> P.Module -> ModuleCmd T.Module
loadModule path m env = runModuleM env $ do
let n = P.thing (P.mName m)
m' <- loadingModule n (Base.loadModule m)
m' <- loadingModule n (Base.loadModule path m)
setFocusedModule (T.mName m')
return m'

20
src/Cryptol/ModuleSystem/Base.hs
View File

@ -11,6 +11,7 @@ module Cryptol.ModuleSystem.Base where
import Cryptol.ModuleSystem.Env (DynamicEnv(..), deIfaceDecls)
import Cryptol.ModuleSystem.Interface
import Cryptol.ModuleSystem.Monad
import Cryptol.ModuleSystem.Env (lookupModule, LoadedModule(..))
import qualified Cryptol.Eval as E
import qualified Cryptol.Eval.Value as E
import qualified Cryptol.ModuleSystem.Renamer as R
@ -106,7 +107,16 @@ loadModuleByPath :: FilePath -> ModuleM T.Module
loadModuleByPath path = do
pm <- parseModule path
let n = thing (P.mName pm)
loadingModule n (loadModule pm)
-- Check whether this module name has already been loaded from a different file
env <- getModuleEnv
case lookupModule n env of
Nothing -> loadingModule n (loadModule path pm)
Just lm
| path == path' -> return (lmModule lm)
| otherwise -> duplicateModuleName n path path'
where path' = lmFilePath lm
-- | Load the module specified by an import.
loadImport :: Located P.Import -> ModuleM ()
@ -124,12 +134,12 @@ loadImport li = do
-- make sure that this module is the one we expect
unless (n == thing (P.mName pm)) (moduleNameMismatch n (mName pm))
_ <- loadModule pm
_ <- loadModule path pm
return ()
-- | Load dependencies, typecheck, and add to the eval environment.
loadModule :: P.Module -> ModuleM T.Module
loadModule pm = do
loadModule :: FilePath -> P.Module -> ModuleM T.Module
loadModule path pm = do
let pm' = addPrelude pm
loadDeps pm'
@ -142,7 +152,7 @@ loadModule pm = do
-- extend the eval env
modifyEvalEnv (E.moduleEnv tcm)
loadedModule tcm
loadedModule path tcm
return tcm

6
src/Cryptol/ModuleSystem/Env.hs
View File

@ -110,6 +110,7 @@ instance Monoid LoadedModules where
data LoadedModule = LoadedModule
{ lmName :: ModName
, lmFilePath :: FilePath
, lmInterface :: Iface
, lmModule :: T.Module
} deriving (Show)
@ -120,13 +121,14 @@ isLoaded mn lm = any ((mn ==) . lmName) (getLoadedModules lm)
lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule
lookupModule mn env = List.find ((mn ==) . lmName) (getLoadedModules (meLoadedModules env))
addLoadedModule :: T.Module -> LoadedModules -> LoadedModules
addLoadedModule tm lm
addLoadedModule :: FilePath -> T.Module -> LoadedModules -> LoadedModules
addLoadedModule path tm lm
| isLoaded (T.mName tm) lm = lm
| otherwise = LoadedModules (getLoadedModules lm ++ [loaded])
where
loaded = LoadedModule
{ lmName = T.mName tm
, lmFilePath = path
, lmInterface = genIface tm
, lmModule = tm
}

18
src/Cryptol/ModuleSystem/Monad.hs
View File

@ -72,6 +72,9 @@ data ModuleError
| OtherFailure String
-- ^ Problems after type checking, eg. specialization
| ModuleNameMismatch P.ModName (Located P.ModName)
-- ^ Module loaded by 'import' statement has the wrong module name
| DuplicateModuleName P.ModName FilePath FilePath
-- ^ Two modules loaded from different files have the same module name
deriving (Show)
instance PP ModuleError where
@ -106,6 +109,11 @@ instance PP ModuleError where
, text "Expected:" <+> pp expected
])
DuplicateModuleName name path1 path2 ->
hang (text "[error] module" <+> pp name <+>
text "is defined in multiple files:")
4 (vcat [text path1, text path2])
OtherFailure x -> text x
@ -148,6 +156,10 @@ moduleNameMismatch :: P.ModName -> Located P.ModName -> ModuleM a
moduleNameMismatch expected found =
ModuleT (raise (ModuleNameMismatch expected found))
duplicateModuleName :: P.ModName -> FilePath -> FilePath -> ModuleM a
duplicateModuleName name path1 path2 =
ModuleT (raise (DuplicateModuleName name path1 path2))
-- Warnings --------------------------------------------------------------------
@ -298,10 +310,10 @@ setNameSeeds seeds = ModuleT $ do
env <- get
set $! env { meNameSeeds = seeds }
loadedModule :: T.Module -> ModuleM ()
loadedModule m = ModuleT $ do
loadedModule :: FilePath -> T.Module -> ModuleM ()
loadedModule path m = ModuleT $ do
env <- get
set $! env { meLoadedModules = addLoadedModule m (meLoadedModules env) }
set $! env { meLoadedModules = addLoadedModule path m (meLoadedModules env) }
modifyEvalEnv :: (EvalEnv -> EvalEnv) -> ModuleM ()
modifyEvalEnv f = ModuleT $ do

4
src/Cryptol/Parser/AST.hs
View File

@ -580,7 +580,7 @@ ppNumLit n info =
PolyLit w -> text "<|" <+> poly w <+> text "|>"
where
pad base pref w =
let txt = showIntAtBase base ("0123456789ABCDEF" !!) n ""
let txt = showIntAtBase base ("0123456789abcdef" !!) n ""
in text pref <> text (replicate (w - length txt) '0') <> text txt
poly w = let (res,deg) = bits Nothing [] 0 n
@ -657,7 +657,7 @@ instance PP Expr where
-- atoms
EVar x -> pp x
ECon x -> pp x
ECon x -> ppPrefix x
ELit x -> pp x
ETuple es -> parens (commaSep (map pp es))
ERecord fs -> braces (commaSep (map (ppNamed "=") fs))

26
src/Cryptol/Parser/Unlit.hs
View File

@ -8,7 +8,7 @@
--
-- Convert a literate source file into an ordinary source file.
{-# LANGUAGE OverloadedStrings, Safe #-}
{-# LANGUAGE OverloadedStrings, Safe, PatternGuards #-}
module Cryptol.Parser.Unlit
( unLit, PreProc(..), guessPreProc, knownExts
) where
@ -81,24 +81,28 @@ markdown = blanks []
blanks current [] = mk Comment current
blanks current (l : ls)
| isCodeLine l = mk Comment current ++ code [l] ls
| isOpenFence l = mk Comment (l : current) ++ fenced [] ls
| isBlank l = blanks (l : current) ls
| otherwise = comment (l : current) ls
| isCodeLine l = mk Comment current ++ code [l] ls
| Just op <- isOpenFence l = mk Comment (l : current) ++ fenced op [] ls
| isBlank l = blanks (l : current) ls
| otherwise = comment (l : current) ls
code current [] = mk Code current
code current (l : ls)
| isCodeLine l = code (l : current) ls
| otherwise = mk Code current ++ comment [] (l : ls)
fenced current [] = mk Code current -- XXX should this be an error?
fenced current (l : ls)
| isCloseFence l = mk Code current ++ comment [l] ls
| otherwise = fenced (l : current) ls
fenced op current [] = mk op current -- XXX should this be an error?
fenced op current (l : ls)
| isCloseFence l = mk op current ++ comment [l] ls
| otherwise = fenced op (l : current) ls
-- XXX: the fences may be indented.
isOpenFence l = "```cryptol" `Text.isPrefixOf` l
isOpenFence l | "```cryptol" == l' = Just Code
| "```" == l' = Just Code
| "```" `Text.isPrefixOf` l' = Just Comment
| otherwise = Nothing
where
l' = Text.dropWhile isSpace l
isCloseFence l = "```" `Text.isPrefixOf` l
isBlank l = Text.all isSpace l
isCodeLine l = "\t" `Text.isPrefixOf` l || " " `Text.isPrefixOf` l

81
src/Cryptol/Prims/Eval.hs
View File

@ -206,7 +206,7 @@ ecDemoteV :: Value
ecDemoteV = tlam $ \valT ->
tlam $ \bitT ->
case (numTValue valT, numTValue bitT) of
(Nat v, Nat bs) -> VWord bs v
(Nat v, Nat bs) -> VWord (BV bs v)
_ -> evalPanic "Cryptol.Eval.Prim.evalConst"
["Unexpected Inf in constant."
, show valT
@ -276,16 +276,18 @@ doubleAndAdd base0 expMask modulus = go 1 base0 expMask
-- Operation Lifting -----------------------------------------------------------
type Binary = TValue -> Value -> Value -> Value
type GenBinary b w = TValue -> GenValue b w -> GenValue b w -> GenValue b w
type Binary = GenBinary Bool BV
binary :: Binary -> Value
binary :: GenBinary b w -> GenValue b w
binary f = tlam $ \ ty ->
lam $ \ a ->
lam $ \ b -> f ty a b
type Unary = TValue -> Value -> Value
type GenUnary b w = TValue -> GenValue b w -> GenValue b w
type Unary = GenUnary Bool BV
unary :: Unary -> Value
unary :: GenUnary b w -> GenValue b w
unary f = tlam $ \ ty ->
lam $ \ a -> f ty a
@ -306,7 +308,7 @@ arithBinary op = loop
| Just (len,a) <- isTSeq ty = case numTValue len of
-- words and finite sequences
Nat w | isTBit a -> VWord w (op w (fromWord l) (fromWord r))
Nat w | isTBit a -> VWord (BV w (op w (fromWord l) (fromWord r)))
| otherwise -> VSeq False (zipWith (loop a) (fromSeq l) (fromSeq r))
-- streams
@ -318,9 +320,9 @@ arithBinary op = loop
-- tuples
| Just (_,tys) <- isTTuple ty =
let (len,ls) = fromVTuple l
(_,rs) = fromVTuple r
in VTuple len (zipWith3 loop tys ls rs)
let ls = fromVTuple l
rs = fromVTuple r
in VTuple (zipWith3 loop tys ls rs)
-- records
| Just fs <- isTRec ty =
@ -337,7 +339,7 @@ arithUnary op = loop
| Just (len,a) <- isTSeq ty = case numTValue len of
-- words and finite sequences
Nat w | isTBit a -> VWord w (op (fromWord x))
Nat w | isTBit a -> VWord (BV w (op (fromWord x)))
| otherwise -> VSeq False (map (loop a) (fromSeq x))
Inf -> toStream (map (loop a) (fromSeq x))
@ -348,8 +350,8 @@ arithUnary op = loop
-- tuples
| Just (_,tys) <- isTTuple ty =
let (len,as) = fromVTuple x
in VTuple len (zipWith loop tys as)
let as = fromVTuple x
in VTuple (zipWith loop tys as)
-- records
| Just fs <- isTRec ty =
@ -388,7 +390,7 @@ lexCompare ty l r
-- tuples
| Just (_,etys) <- isTTuple ty =
zipLexCompare etys (snd (fromVTuple l)) (snd (fromVTuple r))
zipLexCompare etys (fromVTuple l) (fromVTuple r)
-- records
| Just fields <- isTRec ty =
@ -456,8 +458,8 @@ zeroV ty
lam (\ _ -> zeroV bty)
-- tuples
| Just (len,tys) <- isTTuple ty =
VTuple len (map zeroV tys)
| Just (_,tys) <- isTTuple ty =
VTuple (map zeroV tys)
-- records
| Just fields <- isTRec ty =
@ -479,12 +481,12 @@ splitAtV front back a val =
-- needs to be first, assuming that we're on a little-endian machine.
Nat rightWidth | aBit ->
let i = fromWord val
in VTuple 2 [ word leftWidth (i `shiftR` fromInteger rightWidth)
, word rightWidth i ]
in VTuple [ word leftWidth (i `shiftR` fromInteger rightWidth)
, word rightWidth i ]
_ ->
let (ls,rs) = splitAt (fromInteger leftWidth) (fromSeq val)
in VTuple 2 [VSeq aBit ls, toSeq back a rs]
in VTuple [VSeq aBit ls, toSeq back a rs]
where
@ -508,12 +510,12 @@ ecSplitV =
(Inf , Nat e) -> toStream $ mkChunks (infChunksOf e)
_ -> evalPanic "splitV" ["invalid type arguments to split"]
-- | Split into infinately many chunks
-- | Split into infinitely many chunks
infChunksOf :: Integer -> [a] -> [[a]]
infChunksOf each xs = let (as,bs) = genericSplitAt each xs
in as : infChunksOf each bs
-- | Split into finately many chunks
-- | Split into finitely many chunks
finChunksOf :: Integer -> Integer -> [a] -> [[a]]
finChunksOf 0 _ _ = []
finChunksOf parts each xs = let (as,bs) = genericSplitAt each xs
@ -535,7 +537,7 @@ logicBinary op = loop
case numTValue len of
-- words or finite sequences
Nat w | isTBit aty -> VWord w (op (fromWord l) (fromWord r))
Nat w | isTBit aty -> VWord (BV w (op (fromWord l) (fromWord r)))
| otherwise -> VSeq False (zipWith (loop aty) (fromSeq l)
(fromSeq r))
@ -543,9 +545,9 @@ logicBinary op = loop
Inf -> toStream (zipWith (loop aty) (fromSeq l) (fromSeq r))
| Just (_,etys) <- isTTuple ty =
let (s,ls) = fromVTuple l
(_,rs) = fromVTuple r
in VTuple s (zipWith3 loop etys ls rs)
let ls = fromVTuple l
rs = fromVTuple r
in VTuple (zipWith3 loop etys ls rs)
| Just (_,bty) <- isTFun ty =
lam $ \ a -> loop bty (fromVFun l a) (fromVFun r a)
@ -564,15 +566,20 @@ logicUnary op = loop
loop ty val
| isTBit ty = VBit (op (fromVBit val))
| Just (_,b) <- isTSeq ty
, isTBit b = let (w,a) = fromVWord val
in VWord w (op a)
| Just (len,ety) <- isTSeq ty =
| Just (len,ety) <- isTSeq ty = toSeq len ety (map (loop ety) (fromSeq val))
case numTValue len of
-- words or finite sequences
Nat w | isTBit ety -> VWord (BV w (op (fromWord val)))
| otherwise -> VSeq False (map (loop ety) (fromSeq val))
-- streams
Inf -> toStream (map (loop ety) (fromSeq val))
| Just (_,etys) <- isTTuple ty =
let (s,as) = fromVTuple val
in VTuple s (zipWith loop etys as)
let as = fromVTuple val
in VTuple (zipWith loop etys as)
| Just (_,bty) <- isTFun ty =
lam $ \ a -> loop bty (fromVFun val a)
@ -596,8 +603,8 @@ logicShift opW opS
lam $ \ r ->
if isTBit c
then -- words
let (w,i) = fromVWord l
in VWord w (opW w i (fromInteger (fromWord r)))
let BV w i = fromVWord l
in VWord (BV w (opW w i (fromInteger (fromWord r))))
else toSeq a c (opS a c (fromSeq l) (fromInteger (fromWord r)))
@ -665,7 +672,7 @@ indexPrimOne :: (Maybe Integer -> [Value] -> Integer -> Value) -> Value
indexPrimOne op =
tlam $ \ n ->
tlam $ \ _a ->
tlam $ \ _m ->
tlam $ \ _i ->
lam $ \ l ->
lam $ \ r ->
let vs = fromSeq l
@ -715,7 +722,7 @@ fromThenV =
case (first, next, len, bits) of
(Nat first', Nat next', Nat len', Nat bits') ->
let nums = enumFromThen first' next'
in VSeq False (genericTake len' (map (VWord bits') nums))
in VSeq False (genericTake len' (map (VWord . BV bits') nums))
_ -> evalPanic "fromThenV" ["invalid arguments"]
-- @[ 0 .. 10 ]@
@ -729,7 +736,7 @@ fromToV =
(Nat first', Nat lst', Nat bits') ->
let nums = enumFromThenTo first' (first' + 1) lst'
len = 1 + (lst' - first')
in VSeq False (genericTake len (map (VWord bits') nums))
in VSeq False (genericTake len (map (VWord . BV bits') nums))
_ -> evalPanic "fromThenV" ["invalid arguments"]
@ -745,7 +752,7 @@ fromThenToV =
(Nat first', Nat next', Nat lst', Nat len', Nat bits') ->
let nums = enumFromThenTo first' next' lst'
in VSeq False (genericTake len' (map (VWord bits') nums))
in VSeq False (genericTake len' (map (VWord . BV bits') nums))
_ -> evalPanic "fromThenV" ["invalid arguments"]
@ -763,5 +770,5 @@ randomV ty seed =
-- Miscellaneous ---------------------------------------------------------------
tlamN :: (Nat' -> Value) -> Value
tlamN :: (Nat' -> GenValue b w) -> GenValue b w
tlamN f = VPoly (\x -> f (numTValue x))

12
src/Cryptol/Prims/Types.hs
View File

@ -218,29 +218,29 @@ typeOf econ =
ECAt ->
let n = var 0 KNum
a = var 1 KType
m = var 2 KNum
in forAll [n,a,m] [] (tSeq n a `tFun` tWord m `tFun` a)
i = var 2 KNum
in forAll [n,a,i] [ pFin i ] (tSeq n a `tFun` tWord i `tFun` a)
ECAtRange ->
let n = var 0 KNum
a = var 1 KType
m = var 2 KNum
i = var 3 KNum
in forAll [n,a,m,i] [pFin i]
in forAll [n,a,m,i] [ pFin i ]
(tSeq n a `tFun` tSeq m (tWord i) `tFun` tSeq m a)
ECAtBack ->
let n = var 0 KNum
a = var 1 KType
m = var 2 KNum
in forAll [n,a,m] [ pFin n ] (tSeq n a `tFun` tWord m `tFun` a)
i = var 2 KNum
in forAll [n,a,i] [ pFin n, pFin i ] (tSeq n a `tFun` tWord i `tFun` a)
ECAtRangeBack ->
let n = var 0 KNum
a = var 1 KType
m = var 2 KNum
i = var 3 KNum
in forAll [n,a,m,i] [ pFin n ]
in forAll [n,a,m,i] [ pFin n, pFin i ]
(tSeq n a `tFun` tSeq m (tWord i) `tFun` tSeq m a)
-- {a,b,c} (fin a) => [a+b] c -> ([a]c,[b]c)

413
src/Cryptol/Symbolic.hs
View File

@ -7,20 +7,21 @@
-- Portability : portable
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PatternGuards #-}
module Cryptol.Symbolic where
import Control.Applicative
import Control.Monad (foldM, liftM2, replicateM, when, zipWithM)
import Control.Monad.Fix (mfix)
import Control.Monad (replicateM, when, zipWithM)
import Control.Monad.IO.Class
import Control.Monad.Reader (ask, local)
import Data.List (transpose)
import qualified Data.Map as Map
import Data.Monoid (Monoid(..))
import Data.Traversable (traverse)
import qualified Control.Exception as X
import qualified Data.SBV as SBV
import Data.SBV (SBool)
import Data.SBV (Symbolic)
import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem.Env as M
@ -30,7 +31,6 @@ import Cryptol.Symbolic.Prims
import Cryptol.Symbolic.Value
import qualified Cryptol.Eval.Value as Eval
import Cryptol.Eval.Value (TValue, isTSeq)
import qualified Cryptol.Eval.Type (evalType)
import qualified Cryptol.Eval.Env (EvalEnv(..))
import Cryptol.TypeCheck.AST
@ -39,102 +39,85 @@ import Cryptol.Utils.Panic(panic)
-- External interface ----------------------------------------------------------
lookupProver :: String -> SBV.SMTConfig
lookupProver "cvc4" = SBV.cvc4
lookupProver "yices" = SBV.yices
lookupProver "z3" = SBV.z3
lookupProver s = error $ "invalid prover: " ++ s
proverConfigs :: [(String, SBV.SMTConfig)]
proverConfigs =
[ ("cvc4" , SBV.cvc4 )
, ("yices" , SBV.yices )
, ("z3" , SBV.z3 )
, ("boolector", SBV.boolector)
, ("mathsat" , SBV.mathSAT )
]
proverNames :: [String]
proverNames = map fst proverConfigs
lookupProver :: String -> SBV.SMTConfig
lookupProver s =
case lookup s proverConfigs of
Just cfg -> cfg
Nothing -> error $ "invalid prover: " ++ s
-- | A prover result is either an error message, or potentially a
-- counterexample or satisfying assignment.
type ProverResult = Either String (Maybe [(Type, Expr, Eval.Value)])
-- | TODO: document more
prove :: (String, Bool, Bool, String)
prove :: (String, Bool, Bool)
-> [DeclGroup]
-> (Expr, Schema)
-> M.ModuleCmd (Maybe [(Type, Expr)]) -- ^ Returns a list of arguments for a counterexample
prove (proverName, useSolverIte, verbose, input) edecls (expr, schema) = protectStack useSolverIte $ \modEnv -> do
-> M.ModuleCmd ProverResult
prove (proverName, useSolverIte, verbose) edecls (expr, schema) = protectStack useSolverIte $ \modEnv -> do
let extDgs = allDeclGroups modEnv ++ edecls
let prover = lookupProver proverName
case predArgTypes schema of
Left msg -> do putStrLn msg
return (Right (Nothing, modEnv), [])
Left msg -> return (Right (Left msg, modEnv), [])
Right ts -> do when verbose $ putStrLn "Simulating..."
let runE = do args <- mapM forallFinType ts
env <- evalDecls emptyEnv extDgs
v <- evalExpr env expr
b <- foldM vApply v args
return (fromVBit b)
let simenv = SimEnv
{ simConfig = prover
, simPath = SBV.true
, simIteSolver = useSolverIte
, simVerbose = verbose
}
let env = evalDecls (emptyEnv useSolverIte) extDgs
let v = evalExpr env expr
result <- SBV.proveWith prover $ do
b <- runTheMonad runE simenv
args <- mapM forallFinType ts
b <- return $! fromVBit (foldl fromVFun v args)
when verbose $ liftIO $ putStrLn $ "Calling " ++ proverName ++ "..."
return b
mcxexprs <- case result of
SBV.ThmResult (SBV.Satisfiable {}) -> do
let Right (_, cws) = SBV.getModel result
let (vs, _) = parseValues ts cws
let ppOpts = Eval.defaultPPOpts
let doc = hsep (text input : map (pp . Eval.WithBase ppOpts) vs)
print $ doc <+> text "= False"
let cxtys = unFinType <$> ts
cxexprs = zipWithM Eval.toExpr cxtys vs
return (zip cxtys <$> cxexprs)
SBV.ThmResult (SBV.Unsatisfiable {}) -> do
putStrLn "Q.E.D."
return Nothing
SBV.ThmResult _ -> do
print result
return Nothing
return $ Right (zip3 cxtys <$> cxexprs <*> pure vs)
SBV.ThmResult (SBV.Unsatisfiable {}) -> return $ Right Nothing
SBV.ThmResult _ -> return $ Left (show result)
return (Right (mcxexprs, modEnv), [])
sat :: (String, Bool, Bool, String)
sat :: (String, Bool, Bool)
-> [DeclGroup]
-> (Expr, Schema)
-> M.ModuleCmd (Maybe [(Type, Expr)]) -- ^ Returns a list of arguments for a satisfying assignment
sat (proverName, useSolverIte, verbose, input) edecls (expr, schema) = protectStack useSolverIte $ \modEnv -> do
-> M.ModuleCmd ProverResult -- ^ Returns a list of arguments for a satisfying assignment
sat (proverName, useSolverIte, verbose) edecls (expr, schema) = protectStack useSolverIte $ \modEnv -> do
let extDgs = allDeclGroups modEnv ++ edecls
let prover = lookupProver proverName
case predArgTypes schema of
Left msg -> do putStrLn msg
return (Right (Nothing, modEnv), [])
Left msg -> return (Right (Left msg, modEnv), [])
Right ts -> do when verbose $ putStrLn "Simulating..."
let runE = do args <- mapM existsFinType ts
env <- evalDecls emptyEnv extDgs
v <- evalExpr env expr
b <- foldM vApply v args
return (fromVBit b)
let simenv = SimEnv
{ simConfig = prover
, simPath = SBV.true
, simIteSolver = useSolverIte
, simVerbose = verbose
}
let env = evalDecls (emptyEnv useSolverIte) extDgs
let v = evalExpr env expr
result <- SBV.satWith prover $ do
b <- runTheMonad runE simenv
args <- mapM existsFinType ts
b <- return $! fromVBit (foldl fromVFun v args)
when verbose $ liftIO $ putStrLn $ "Calling " ++ proverName ++ "..."
return b
msatexprs <- case result of
SBV.SatResult (SBV.Satisfiable {}) -> do
let Right (_, cws) = SBV.getModel result
let (vs, _) = parseValues ts cws
let ppOpts = Eval.defaultPPOpts
let doc = hsep (text input : map (pp . Eval.WithBase ppOpts) vs)
print $ doc <+> text "= True"
let sattys = unFinType <$> ts
satexprs = zipWithM Eval.toExpr sattys vs
return (zip sattys <$> satexprs)
SBV.SatResult (SBV.Unsatisfiable {}) -> do
putStrLn "Unsatisfiable."
return Nothing
SBV.SatResult _ -> do
print result
return Nothing
return $ Right (zip3 sattys <$> satexprs <*> pure vs)
SBV.SatResult (SBV.Unsatisfiable {}) -> return $ Right Nothing
SBV.SatResult _ -> return $ Left (show result)
return (Right (msatexprs, modEnv), [])
protectStack :: Bool -> M.ModuleCmd (Maybe a) -> M.ModuleCmd (Maybe a)
protectStack :: Bool -> M.ModuleCmd ProverResult -> M.ModuleCmd ProverResult
protectStack usingITE cmd modEnv = X.catchJust isOverflow (cmd modEnv) handler
where isOverflow X.StackOverflow = Just ()
isOverflow _ = Nothing
@ -142,8 +125,7 @@ protectStack usingITE cmd modEnv = X.catchJust isOverflow (cmd modEnv) handler
| otherwise = msgBase ++ "\n" ++
"Using ':set iteSolver=on' might help."
msgBase = "Symbolic evaluation failed to terminate."
handler () = do putStrLn msg
return (Right (Nothing, modEnv), [])
handler () = return (Right (Left msg, modEnv), [])
parseValues :: [FinType] -> [SBV.CW] -> ([Eval.Value], [SBV.CW])
parseValues [] cws = ([], cws)
@ -154,14 +136,15 @@ parseValues (t : ts) cws = (v : vs, cws'')
parseValue :: FinType -> [SBV.CW] -> (Eval.Value, [SBV.CW])
parseValue FTBit [] = error "parseValue"
parseValue FTBit (cw : cws) = (Eval.VBit (SBV.fromCW cw), cws)
parseValue (FTSeq 0 FTBit) cws = (Eval.VWord (Eval.BV 0 0), cws)
parseValue (FTSeq n FTBit) (cw : cws)
| SBV.isBounded cw = (Eval.VWord (toInteger n) (SBV.fromCW cw), cws)
| SBV.isBounded cw = (Eval.VWord (Eval.BV (toInteger n) (SBV.fromCW cw)), cws)
| otherwise = error "parseValue"
parseValue (FTSeq n FTBit) cws = (Eval.VSeq True vs, cws')
where (vs, cws') = parseValues (replicate n FTBit) cws
parseValue (FTSeq n t) cws = (Eval.VSeq False vs, cws')
where (vs, cws') = parseValues (replicate n t) cws
parseValue (FTTuple ts) cws = (Eval.VTuple (length vs) vs, cws')
parseValue (FTTuple ts) cws = (Eval.VTuple vs, cws')
where (vs, cws') = parseValues ts cws
parseValue (FTRecord fs) cws = (Eval.VRecord (zip ns vs), cws')
where (ns, ts) = unzip fs
@ -216,57 +199,56 @@ predArgTypes schema@(Forall ts ps ty)
go (TUser _ _ t) = go t
go _ = Nothing
forallFinType :: FinType -> TheMonad Value
forallFinType :: FinType -> Symbolic Value
forallFinType ty =
case ty of
FTBit -> VBit <$> liftSymbolic SBV.forall_
FTSeq n FTBit -> VWord <$> liftSymbolic (forallBV_ n)
FTSeq n t -> vSeq <$> replicateM n (mkThunk t)
FTTuple ts -> VTuple <$> mapM mkThunk ts
FTRecord fs -> VRecord <$> mapM (traverseSnd mkThunk) fs
where
mkThunk :: FinType -> TheMonad Thunk
mkThunk t = Ready <$> forallFinType t
FTBit -> VBit <$> SBV.forall_
FTSeq 0 FTBit -> return $ VWord (SBV.literal (bv 0 0))
FTSeq n FTBit -> VWord <$> (forallBV_ n)
FTSeq n t -> VSeq False <$> replicateM n (forallFinType t)
FTTuple ts -> VTuple <$> mapM forallFinType ts
FTRecord fs -> VRecord <$> mapM (traverseSnd forallFinType) fs
existsFinType :: FinType -> TheMonad Value
existsFinType :: FinType -> Symbolic Value
existsFinType ty =
case ty of
FTBit -> VBit <$> liftSymbolic SBV.exists_
FTSeq n FTBit -> VWord <$> liftSymbolic (existsBV_ n)
FTSeq n t -> vSeq <$> replicateM n (mkThunk t)
FTTuple ts -> VTuple <$> mapM mkThunk ts
FTRecord fs -> VRecord <$> mapM (traverseSnd mkThunk) fs
where
mkThunk :: FinType -> TheMonad Thunk
mkThunk t = Ready <$> existsFinType t
FTBit -> VBit <$> SBV.exists_
FTSeq 0 FTBit -> return $ VWord (SBV.literal (bv 0 0))
FTSeq n FTBit -> VWord <$> existsBV_ n
FTSeq n t -> VSeq False <$> replicateM n (existsFinType t)
FTTuple ts -> VTuple <$> mapM existsFinType ts
FTRecord fs -> VRecord <$> mapM (traverseSnd existsFinType) fs
-- Simulation environment ------------------------------------------------------
data Env = Env
{ envVars :: Map.Map QName Thunk
{ envVars :: Map.Map QName Value
, envTypes :: Map.Map TVar TValue
, envIteSolver :: Bool
}
instance Monoid Env where
mempty = Env
{ envVars = Map.empty
, envTypes = Map.empty
, envIteSolver = False
}
mappend l r = Env
{ envVars = Map.union (envVars l) (envVars r)
, envTypes = Map.union (envTypes l) (envTypes r)
, envIteSolver = envIteSolver l || envIteSolver r
}
emptyEnv :: Env
emptyEnv = Env Map.empty Map.empty
emptyEnv :: Bool -> Env
emptyEnv useIteSolver = Env Map.empty Map.empty useIteSolver
-- | Bind a variable in the evaluation environment.
bindVar :: (QName, Thunk) -> Env -> Env
bindVar :: (QName, Value) -> Env -> Env
bindVar (n, thunk) env = env { envVars = Map.insert n thunk (envVars env) }
-- | Lookup a variable in the environment.
lookupVar :: QName -> Env -> Maybe Thunk
lookupVar :: QName -> Env -> Maybe Value
lookupVar n env = Map.lookup n (envVars env)
-- | Bind a type variable of kind *.
@ -277,235 +259,114 @@ bindType p ty env = env { envTypes = Map.insert p ty (envTypes env) }
lookupType :: TVar -> Env -> Maybe TValue
lookupType p env = Map.lookup p (envTypes env)
-- Path conditions -------------------------------------------------------------
thenBranch :: SBool -> TheMonad a -> TheMonad a
thenBranch s = local $ \e -> e { simPath = (SBV.&&&) s (simPath e) }
elseBranch :: SBool -> TheMonad a -> TheMonad a
elseBranch s = thenBranch (SBV.bnot s)
isFeasible :: SBool -> TheMonad Bool
isFeasible path
| path `SBV.isConcretely` (== False) = return False
| path `SBV.isConcretely` (== True) = return True
| otherwise = do
useSolverIte <- simIteSolver <$> ask
verbose <- simVerbose <$> ask
config <- simConfig <$> ask
if useSolverIte then do
when verbose $ liftIO $ putStrLn "Testing branch condition with solver..."
res <- liftSymbolic $ SBV.internalIsTheoremWith config (Just 5) (SBV.bnot path)
case res of
Just isThm -> do let msg = if isThm then "Infeasible." else "Feasible."
when verbose $ liftIO $ putStrLn msg
return (not isThm)
Nothing -> do when verbose $ liftIO $ putStrLn "Undetermined."
return True
else return True
evalIf :: SBool -> TheMonad Value -> TheMonad Value -> TheMonad Value
evalIf s m1 m2 = do
path <- simPath <$> ask
let path1 = (SBV.&&&) path s
let path2 = (SBV.&&&) path (SBV.bnot s)
c1 <- isFeasible path1
if not c1
then elseBranch s m2
else do
c2 <- isFeasible path2
if not c2
then thenBranch s m1
else do
v1 <- thenBranch s m1
v2 <- elseBranch s m2
ite s v1 v2
-- Expressions -----------------------------------------------------------------
evalExpr :: Env -> Expr -> TheMonad Value
evalExpr :: Env -> Expr -> Value
evalExpr env expr =
case expr of
ECon econ -> return $ evalECon econ
EList es _ty -> vSeq <$> traverse eval' es
ETuple es -> VTuple <$> traverse eval' es
ERec fields -> VRecord <$> traverse (traverseSnd eval') fields
ESel e sel -> evalSel sel =<< eval e
EIf b e1 e2 -> do
VBit s <- evalExpr env b
evalIf s (evalExpr env e1) (evalExpr env e2)
ECon econ -> evalECon econ
EList es ty -> VSeq (tIsBit ty) (map eval es)
ETuple es -> VTuple (map eval es)
ERec fields -> VRecord [ (f, eval e) | (f, e) <- fields ]
ESel e sel -> evalSel sel (eval e)
EIf b e1 e2 -> evalIf (fromVBit (eval b)) (eval e1) (eval e2)
where evalIf = if envIteSolver env then SBV.sBranch else SBV.ite
EComp ty e mss -> evalComp env (evalType env ty) e mss
EVar n -> force $ case lookupVar n env of
Just x -> x
_ -> panic "Cryptol.Symbolic.evalExpr" [ "Variable " ++ show n ++ " not found" ]
EVar n -> case lookupVar n env of
Just x -> x
_ -> panic "Cryptol.Symbolic.evalExpr" [ "Variable " ++ show n ++ " not found" ]
-- TODO: how to deal with uninterpreted functions?
ETAbs tv e -> return $ VPoly $ \ty -> evalExpr (bindType (tpVar tv) ty env) e
ETApp e ty -> do VPoly f <- eval e
f (evalType env ty)
EApp e1 e2 -> do VFun f <- eval e1
f =<< eval' e2
EAbs n _ty e -> return $ VFun $ \th -> evalExpr (bindVar (n, th) env) e
ETAbs tv e -> VPoly $ \ty -> evalExpr (bindType (tpVar tv) ty env) e
ETApp e ty -> fromVPoly (eval e) (evalType env ty)
EApp e1 e2 -> fromVFun (eval e1) (eval e2)
EAbs n _ty e -> VFun $ \x -> evalExpr (bindVar (n, x) env) e
EProofAbs _prop e -> eval e
EProofApp e -> eval e
ECast e _ty -> eval e
EWhere e ds -> do env' <- evalDecls env ds
evalExpr env' e
EWhere e ds -> evalExpr (evalDecls env ds) e
where
eval e = evalExpr env e
eval' e = delay (evalExpr env e)
evalType :: Env -> Type -> TValue
evalType env ty = Cryptol.Eval.Type.evalType env' ty
where env' = Cryptol.Eval.Env.EvalEnv Map.empty (envTypes env)
evalSel :: Selector -> Value -> TheMonad Value
evalSel :: Selector -> Value -> Value
evalSel sel v =
case sel of
TupleSel n _ ->
case v of
VTuple xs -> force $ xs !! (n - 1) -- 1-based indexing
VNil -> return VNil
VCons {} -> liftList v
VFun f -> return $ VFun $ \x -> evalSel sel =<< f x
_ -> panic "Cryptol.Symbolic.evalSel" [ "Tuple selector applied to non-tuple" ]
VTuple xs -> xs !! (n - 1) -- 1-based indexing
VSeq b xs -> VSeq b (map (evalSel sel) xs)
VStream xs -> VStream (map (evalSel sel) xs)
VFun f -> VFun (\x -> evalSel sel (f x))
_ -> panic "Cryptol.Symbolic.evalSel" [ "Tuple selector applied to incompatible type" ]
RecordSel n _ ->
case v of
VRecord bs -> force $ case lookup n bs of
Just x -> x
_ -> panic "Cryptol.Symbolic.evalSel" [ "Selector " ++ show n ++ " not found" ]
VNil -> return VNil
VCons {} -> liftList v
VFun f -> return $ VFun $ \x -> evalSel sel =<< f x
VRecord bs -> case lookup n bs of
Just x -> x
_ -> panic "Cryptol.Symbolic.evalSel" [ "Selector " ++ show n ++ " not found" ]
VSeq b xs -> VSeq b (map (evalSel sel) xs)
VStream xs -> VStream (map (evalSel sel) xs)
VFun f -> VFun (\x -> evalSel sel (f x))
_ -> panic "Cryptol.Symbolic.evalSel" [ "Record selector applied to non-record" ]
ListSel n _ -> case v of
--VSeq xs -> force $ xs !! n -- 0-based indexing
VWord s -> return $ VBit (SBV.sbvTestBit s n)
_ -> let go :: Int -> Value -> TheMonad Thunk
go 0 (VCons x _) = return x
go i (VCons _ y) = go (i - 1) =<< force y
go _ _ = error "internal error"
in force =<< go n v
where
liftList VNil = return VNil
liftList (VCons x xs) = do x' <- delay (evalSel sel =<< force x)
xs' <- delay (liftList =<< force xs)
return (VCons x' xs')
liftList _ = panic "Cryptol.Symbolic.evalSel"
["Malformed list, while lifting selector"]
VWord s -> VBit (SBV.sbvTestBit s n)
_ -> fromSeq v !! n -- 0-based indexing
-- Declarations ----------------------------------------------------------------
evalDecls :: Env -> [DeclGroup] -> TheMonad Env
evalDecls = foldM evalDeclGroup
evalDecls :: Env -> [DeclGroup] -> Env
evalDecls = foldl evalDeclGroup
evalDeclGroup :: Env -> DeclGroup -> TheMonad Env
evalDeclGroup :: Env -> DeclGroup -> Env
evalDeclGroup env dg =
case dg of
NonRecursive d -> do binding <- evalDecl env d
return $ bindVar binding env
Recursive ds -> mfix $ \env' -> do
bindings <- traverse (evalDecl env') ds
return $ foldr bindVar env bindings
NonRecursive d -> bindVar (evalDecl env d) env
Recursive ds -> let env' = foldr bindVar env bindings
bindings = map (evalDecl env') ds
in env'
evalDecl :: Env -> Decl -> TheMonad (QName, Thunk)
evalDecl env d = do
thunk <- delay $ evalExpr env (dDefinition d)
return (dName d, thunk)
evalDecl :: Env -> Decl -> (QName, Value)
evalDecl env d = (dName d, evalExpr env (dDefinition d))
-- List Comprehensions ---------------------------------------------------------
data LazySeq a = LSNil | LSCons a (MLazySeq a)
type MLazySeq a = TheMonad (LazySeq a)
-- | Evaluate a comprehension.
evalComp :: Env -> TValue -> Expr -> [[Match]] -> Value
evalComp env seqty body ms
| Just (len,el) <- isTSeq seqty = toSeq len el [ evalExpr e body | e <- envs ]
| otherwise = evalPanic "Cryptol.Eval" [ "evalComp given a non sequence"
, show seqty
]
instance Functor LazySeq where
fmap _ LSNil = LSNil
fmap f (LSCons x xs) = LSCons (f x) (fmap f <$> xs)
-- XXX we could potentially print this as a number if the type was available.
where
-- generate a new environment for each iteration of each parallel branch
benvs = map (branchEnvs env) ms
singleLS :: a -> LazySeq a
singleLS x = LSCons x (return LSNil)
-- take parallel slices of each environment. when the length of the list
-- drops below the number of branches, one branch has terminated.
allBranches es = length es == length ms
slices = takeWhile allBranches (transpose benvs)
zipWithLS :: (a -> b -> c) -> LazySeq a -> LazySeq b -> LazySeq c
zipWithLS f (LSCons x xs) (LSCons y ys) = LSCons (f x y) (liftM2 (zipWithLS f) xs ys)
zipWithLS _ _ _ = LSNil
repeatLS :: a -> LazySeq a
repeatLS x = xs where xs = LSCons x (return xs)
transposeLS :: [LazySeq a] -> LazySeq [a]
transposeLS = foldr (zipWithLS (:)) (repeatLS [])
appendLS :: LazySeq a -> LazySeq a -> LazySeq a
appendLS LSNil ys = ys
appendLS (LSCons x xs') ys =
LSCons x $ do
xs <- xs'
return (appendLS xs ys)
appendMLS :: MLazySeq a -> MLazySeq a -> MLazySeq a
appendMLS xs ys = do
l <- xs
case l of
LSNil -> ys
LSCons x xs' -> return (LSCons x (appendMLS xs' ys))
bindMLS :: MLazySeq a -> (a -> MLazySeq b) -> MLazySeq b
bindMLS xs k = do
l <- xs
case l of
LSNil -> return LSNil
LSCons x xs' -> appendMLS (k x) (bindMLS xs' k)
toLazySeq :: Value -> LazySeq Thunk
toLazySeq (VCons th1 th2) = LSCons th1 (toLazySeq <$> force th2)
toLazySeq VNil = LSNil
toLazySeq (VWord w) = go (SBV.bitSize w - 1)
where go i | i < 0 = LSNil
| otherwise = LSCons (Ready (VBit (SBV.sbvTestBit w i))) (return (go (i - 1)))
toLazySeq _ = error "toLazySeq"
toSeq :: LazySeq Thunk -> TheMonad Value
toSeq LSNil = return VNil
toSeq (LSCons x xs) = VCons x <$> delay (toSeq =<< xs)
evalComp :: Env -> TValue -> Expr -> [[Match]] -> TheMonad Value
evalComp env seqty body ms =
case isTSeq seqty of
Nothing -> evalPanic "Cryptol.Eval" [ "evalComp given a non sequence", show seqty ]
Just (_len, _el) -> do
-- generate a new environment for each iteration of each parallel branch
(benvs :: [LazySeq Env]) <- mapM (branchEnvs env) ms
-- take parallel slices of each environment.
let slices :: LazySeq [Env]
slices = transposeLS benvs
-- join environments to produce environments at each step through the process.
let envs :: LazySeq Env
envs = fmap mconcat slices
thunks <- bindMLS (return envs) (\e -> singleLS <$> delay (evalExpr e body))
toSeq thunks
-- join environments to produce environments at each step through the process.
envs = map mconcat slices
-- | Turn a list of matches into the final environments for each iteration of
-- the branch.
branchEnvs :: Env -> [Match] -> MLazySeq Env
branchEnvs :: Env -> [Match] -> [Env]
branchEnvs env matches =
case matches of
[] -> return (singleLS env)
m : ms -> bindMLS (evalMatch env m) (\env' -> branchEnvs env' ms)
[] -> [env]
m : ms -> do env' <- evalMatch env m
branchEnvs env' ms
-- | Turn a match into the list of environments it represents.
evalMatch :: Env -> Match -> MLazySeq Env
evalMatch :: Env -> Match -> [Env]
evalMatch env m = case m of
From n _ty expr -> do
ths <- toLazySeq <$> evalExpr env expr
return $ fmap (\th -> bindVar (n, th) env) ths
Let d -> do
binding <- evalDecl env d
return $ singleLS (bindVar binding env)
From n _ty expr -> [ bindVar (n, v) env | v <- fromSeq (evalExpr env expr) ]
Let d -> [ bindVar (evalDecl env d) env ]

114
src/Cryptol/Symbolic/BitVector.hs
View File

@ -8,17 +8,14 @@
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Cryptol.Symbolic.BitVector where
import Data.Bits
import Control.Monad (replicateM)
import Control.Monad.IO.Class
import Control.Monad.Reader (MonadReader, ReaderT, ask, runReaderT)
import Data.Bits
import Data.IORef
import System.Random
import Test.QuickCheck (quickCheck)
import Data.SBV.Bridge.Yices
import Data.SBV.Internals
@ -26,7 +23,7 @@ import Data.SBV.BitVectors.Data
-- BitVector type --------------------------------------------------------------
data BitVector = BV { width :: !Int, val :: !Integer }
data BitVector = BV { signedcxt :: Bool, width :: !Int, val :: !Integer }
deriving (Eq, Ord, Show)
-- ^ Invariant: BV w x requires that 0 <= w and 0 <= x < 2^w.
@ -35,44 +32,64 @@ bitMask w = bit w - 1
-- | Smart constructor for bitvectors.
bv :: Int -> Integer -> BitVector
bv w x = BV w (x .&. bitMask w)
bv = sbv False
unsigned :: BitVector -> Integer
unsigned = val
sbv :: Bool -> Int -> Integer -> BitVector
sbv b w x = BV b w (x .&. bitMask w)
signed :: BitVector -> Integer
signed (BV w x)
unsigned :: Int -> Integer -> Integer
unsigned w x = x + bit w
signed :: Int -> Integer -> Integer
signed w x
| w > 0 && testBit x (w - 1) = x - bit w
| otherwise = x
same :: Int -> Int -> Int
same m n = if m == n then m else error $ "BitVector size mismatch: " ++ show (m, n)
instance SignCast SWord SWord where
signCast (SBV (KBounded _ w) (Left (cwVal -> (CWInteger x)))) =
SBV k (Left (CW k (CWInteger (signed w x)))) where
k = KBounded True w
signCast x@(SBV (KBounded _ w) _) = SBV k (Right (cache y)) where
k = KBounded True w
y st = do xsw <- sbvToSW st x
newExpr st k (SBVApp (Extract (intSizeOf x-1) 0) [xsw])
signCast _ = error "SignCast not called on BitVector value"
unsignCast (SBV (KBounded _ w) (Left (cwVal -> (CWInteger x)))) =
SBV k (Left (CW k (CWInteger (unsigned w x)))) where
k = KBounded False w
unsignCast x@(SBV (KBounded _ w) _) = SBV k (Right (cache y)) where
k = KBounded False w
y st = do xsw <- sbvToSW st x
newExpr st k (SBVApp (Extract (intSizeOf x-1) 0) [xsw])
instance Num BitVector where
fromInteger n = error $ "fromInteger " ++ show n ++ " :: BitVector"
BV m x + BV n y = bv (same m n) (x + y)
BV m x - BV n y = bv (same m n) (x - y)
BV m x * BV n y = bv (same m n) (x * y)
negate (BV m x) = bv m (- x)
BV s m x + BV _ n y = sbv s (same m n) (x + y)
BV s m x - BV _ n y = sbv s (same m n) (x - y)
BV s m x * BV _ n y = sbv s (same m n) (x * y)
negate (BV s m x) = sbv s m (- x)
abs = id
signum (BV m _) = bv m 1
signum (BV s m _) = sbv s m 1
instance Bits BitVector where
BV m x .&. BV n y = BV (same m n) (x .&. y)
BV m x .|. BV n y = BV (same m n) (x .|. y)
BV m x `xor` BV n y = BV (same m n) (x `xor` y)
complement (BV m x) = BV m (x `xor` bitMask m)
shift (BV m x) i = bv m (shift x i)
rotate (BV m x) i = bv m (shift x j .|. shift x (j - m))
where j = i `mod` m
bit _i = error "bit: can't determine width"
setBit (BV m x) i = BV m (setBit x i)
clearBit (BV m x) i = BV m (clearBit x i)
complementBit (BV m x) i = BV m (complementBit x i)
testBit (BV _ x) i = testBit x i
bitSize (BV m _) = m
isSigned _ = False
popCount (BV _ x) = popCount x
BV s m x .&. BV _ n y = BV s (same m n) (x .&. y)
BV s m x .|. BV _ n y = BV s (same m n) (x .|. y)
BV s m x `xor` BV _ n y = BV s (same m n) (x `xor` y)
complement (BV s m x) = BV s m (x `xor` bitMask m)
shift (BV s m x) i = sbv s m (shift x i)
rotate (BV s m x) i = sbv s m (shift x j .|. shift x (j - m))
where j = i `mod` m
bit _i = error "bit: can't determine width"
setBit (BV s m x) i = BV s m (setBit x i)
clearBit (BV s m x) i = BV s m (clearBit x i)
complementBit (BV s m x) i = BV s m (complementBit x i)
testBit (BV _ _ x) i = testBit x i
bitSize (BV _ m _) = m
isSigned (BV s _ _) = s
popCount (BV _ _ x) = popCount x
--------------------------------------------------------------------------------
-- SBV class instances
@ -80,12 +97,12 @@ instance Bits BitVector where
type SWord = SBV BitVector
instance HasKind BitVector where
kindOf (BV w _) = KBounded False w
kindOf (BV s w _) = KBounded s w
instance SymWord BitVector where
literal (BV w x) = SBV k (Left (mkConstCW k x))
where k = KBounded False w
fromCW c@(CW (KBounded False w) _) = BV w (fromCW c)
literal (BV s w x) = SBV k (Left (mkConstCW k x))
where k = KBounded s w
fromCW c@(CW (KBounded s w) _) = BV s w (fromCW c)
fromCW c = error $ "fromCW: Unsupported non-integral value: " ++ show c
mkSymWord _ _ = error "mkSymWord unimplemented for type BitVector"
@ -97,10 +114,10 @@ instance FromBits (SBV BitVector) where
go !acc !i (x:xs) = go (ite x (setBit acc i) acc) (i+1) xs
instance SDivisible BitVector where
sQuotRem (BV m x) (BV n y) = (BV w q, BV w r)
sQuotRem (BV _ m x) (BV _ n y) = (BV False w q, BV False w r)
where (q, r) = quotRem x y
w = same m n
sDivMod (BV m x) (BV n y) = (BV w q, BV w r)
sDivMod (BV _ m x) (BV _ n y) = (BV False w q, BV False w r)
where (q, r) = divMod x y
w = same m n
@ -109,8 +126,9 @@ instance SDivisible (SBV BitVector) where
sDivMod = liftDMod
extract :: Int -> Int -> SWord -> SWord
extract i j x =
extract i j x@(SBV (KBounded s _) _) =
case x of
_ | i < j -> SBV k (Left (CW k (CWInteger 0)))
SBV _ (Left cw) ->
case cw of
CW _ (CWInteger v) -> SBV k (Left (normCW (CW k (CWInteger (v `shiftR` j)))))
@ -119,7 +137,7 @@ extract i j x =
where y st = do sw <- sbvToSW st x
newExpr st k (SBVApp (Extract i j) [sw])
where
k = KBounded False (i - j + 1)
k = KBounded s (i - j + 1)
cat :: SWord -> SWord -> SWord
cat x y | bitSize x == 0 = y
@ -137,23 +155,23 @@ cat x y = SBV k (Right (cache z))
newExpr st k (SBVApp Join [xsw, ysw])
randomSBVBitVector :: Int -> IO (SBV BitVector)
randomSBVBitVector width = do
bs <- replicateM width randomIO
randomSBVBitVector w = do
bs <- replicateM w randomIO
let x = sum [ bit i | (i, b) <- zip [0..] bs, b ]
return (literal (bv width x))
return (literal (bv w x))
mkSymBitVector :: Maybe Quantifier -> Maybe String -> Int -> Symbolic (SBV BitVector)
mkSymBitVector mbQ mbNm width =
mkSymSBVWithRandom (randomSBVBitVector width) mbQ (KBounded False width) mbNm
mkSymBitVector mbQ mbNm w =
mkSymSBVWithRandom (randomSBVBitVector w) mbQ (KBounded False w) mbNm
forallBV :: String -> Int -> Symbolic (SBV BitVector)
forallBV name width = mkSymBitVector (Just ALL) (Just name) width
forallBV nm w = mkSymBitVector (Just ALL) (Just nm) w
forallBV_ :: Int -> Symbolic (SBV BitVector)
forallBV_ width = mkSymBitVector (Just ALL) Nothing width
forallBV_ w = mkSymBitVector (Just ALL) Nothing w
existsBV :: String -> Int -> Symbolic (SBV BitVector)
existsBV name width = mkSymBitVector (Just EX) (Just name) width
existsBV nm w = mkSymBitVector (Just EX) (Just nm) w
existsBV_ :: Int -> Symbolic (SBV BitVector)
existsBV_ width = mkSymBitVector (Just EX) Nothing width
existsBV_ w = mkSymBitVector (Just EX) Nothing w

825
src/Cryptol/Symbolic/Prims.hs
View File

File diff suppressed because it is too large Load Diff

168
src/Cryptol/Symbolic/Value.hs
View File

@ -6,141 +6,73 @@
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Cryptol.Symbolic.Value where
{-# LANGUAGE TypeSynonymInstances #-}
module Cryptol.Symbolic.Value
( Value
, TValue, numTValue, toNumTValue, finTValue, isTBit, isTFun, isTSeq, isTTuple, isTRec, tvSeq
, GenValue(..), lam, tlam, toStream, toFinSeq, toSeq
, fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord
, fromSeq, fromWord
, evalPanic
)
where
import Control.Applicative
import Control.Monad.Fix (MonadFix)
import Control.Monad.IO.Class
import Control.Monad.Reader (MonadReader, ReaderT, runReaderT)
import Control.Monad.Trans (lift)
import Data.Bits (bitSize)
import Data.IORef
import Data.Traversable
import Cryptol.Eval.Value (TValue)
import Cryptol.Eval.Value (TValue, numTValue, toNumTValue, finTValue, isTBit, isTFun, isTSeq, isTTuple, isTRec, tvSeq,
GenValue(..), lam, tlam, toStream, toFinSeq, toSeq,
fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord)
import Cryptol.Symbolic.BitVector
import Cryptol.TypeCheck.AST
import Cryptol.Utils.Panic (panic)
import Data.SBV (Symbolic, SBool, SMTConfig, fromBitsBE, sbvTestBit)
import Data.SBV (SBool, fromBitsBE, sbvTestBit, Mergeable(..))
-- Symbolic Simulator Monad ----------------------------------------------------
-- Values ----------------------------------------------------------------------
data SimEnv = SimEnv
{ simConfig :: SMTConfig
, simPath :: SBool
, simIteSolver :: Bool
, simVerbose :: Bool
}
type Value = GenValue SBool SWord
newtype TheMonad a = TheMonad (ReaderT SimEnv Symbolic a)
deriving (Functor, Applicative, Monad, MonadFix, MonadIO, MonadReader SimEnv)
-- Symbolic Conditionals -------------------------------------------------------
-- ^ The SBool environment parameter models the path condition, i.e.
-- an assertion derived from the context of surrounding if-then-else
-- statements. It is used to determine whether new if-then-else
-- branches are reachable. It is important to include this within the
-- monad so that a conditional in a function body will be evaluated
-- relative to the path condition where the function is applied,
-- rather than with the path condition where the function was defined.
instance Mergeable Value where
symbolicMerge c v1 v2 =
case (v1, v2) of
(VRecord fs1, VRecord fs2) -> VRecord $ zipWith mergeField fs1 fs2
(VTuple vs1 , VTuple vs2 ) -> VTuple $ zipWith (symbolicMerge c) vs1 vs2
(VBit b1 , VBit b2 ) -> VBit $ symbolicMerge c b1 b2
(VWord w1 , VWord w2 ) -> VWord $ symbolicMerge c w1 w2
(VSeq b1 vs1, VSeq _ vs2 ) -> VSeq b1 $ symbolicMerge c vs1 vs2
(VStream vs1, VStream vs2) -> VStream $ symbolicMerge c vs1 vs2
(VFun f1 , VFun f2 ) -> VFun $ symbolicMerge c f1 f2
(VPoly f1 , VPoly f2 ) -> VPoly $ symbolicMerge c f1 f2
(VWord w1 , _ ) -> VWord $ symbolicMerge c w1 (fromWord v2)
(_ , VWord w2 ) -> VWord $ symbolicMerge c (fromWord v1) w2
(_ , _ ) -> error "symbolicMerge: incompatible values"
where
mergeField (n1, x1) (n2, x2)
| n1 == n2 = (n1, symbolicMerge c x1 x2)
| otherwise = error "symbolicMerge: incompatible values"
runTheMonad :: TheMonad a -> SimEnv -> Symbolic a
runTheMonad (TheMonad r) = runReaderT r
-- Big-endian Words ------------------------------------------------------------
liftSymbolic :: Symbolic a -> TheMonad a
liftSymbolic s = TheMonad (lift s)
-- Values and Thunks -----------------------------------------------------------
data Value
= VRecord [(Name, Thunk)] -- @ { .. } @
| VTuple [Thunk] -- @ ( .. ) @
| VBit SBool -- @ Bit @
| VWord SWord -- @ [n]Bit @
| VNil
| VCons Thunk Thunk -- @ [n]a @ head, tail
| VFun (Thunk -> TheMonad Value) -- functions
| VPoly (TValue -> TheMonad Value) -- polymorphic values (kind *)
data Thunk
= Thunk (IORef (Either (TheMonad Value) Value))
| Ready Value
force :: Thunk -> TheMonad Value
force (Ready v) = return v
force (Thunk ref) = do
r <- liftIO $ readIORef ref
case r of
Left m -> do
v <- m
liftIO $ writeIORef ref (Right v)
return v
Right v -> return v
delay :: TheMonad Value -> TheMonad Thunk
delay m = Thunk <$> liftIO (newIORef (Left m))
ready :: Value -> TheMonad Thunk
ready v = Thunk <$> liftIO (newIORef (Right v))
unpackWord :: SWord -> [SBool]
unpackWord s = [ sbvTestBit s i | i <- reverse [0 .. bitSize s - 1] ]
-- Constructors and Accessors --------------------------------------------------
tlam :: (TValue -> Value) -> Value
tlam f = VPoly (return . f)
fromWord :: Value -> SWord
fromWord (VWord s) = s
fromWord v = Data.SBV.fromBitsBE (map fromVBit (fromSeq v))
vSeq :: [Thunk] -> Value
vSeq [] = VNil
vSeq (x : xs) = VCons x (Ready (vSeq xs))
vApply :: Value -> Value -> TheMonad Value
vApply (VFun f) v = f (Ready v)
vApply _ _ = fail "vApply: not a function"
fromVBit :: Value -> SBool
fromVBit (VBit b) = b
fromVBit _ = error "fromVBit: not a bit"
fromWord :: Value -> TheMonad SWord
fromWord (VWord s) = return s
fromWord v = do
thunks <- fromSeq v
vs <- traverse force thunks
let bs = map fromVBit vs
return $ Data.SBV.fromBitsBE bs
fromSeq :: Value -> TheMonad [Thunk]
fromSeq VNil = return []
fromSeq (VCons x th) = do
v <- force th
xs <- fromSeq v
return (x : xs)
fromSeq (VWord s) = return $ reverse [ Ready (VBit (sbvTestBit s i)) | i <- [0 .. bitSize s - 1] ]
fromSeq _ = error "fromSeq: not a sequence"
fromVCons :: Value -> (Thunk, Thunk)
fromVCons (VCons h t) = (h, t)
fromVCons (VWord s) = fromVCons (foldr (\h t -> VCons (Ready h) (Ready t)) VNil bs)
where bs = reverse [ VBit (sbvTestBit s i) | i <- [0 .. bitSize s - 1] ]
fromVCons _ = error "fromVCons: not a stream"
fromVFun :: Value -> (Thunk -> TheMonad Value)
fromVFun (VFun f) = f
fromVFun _ = error "fromVFun: not a function"
fromVTuple :: Value -> [Thunk]
fromVTuple (VTuple thunks) = thunks
fromVTuple _ = error "fromVTuple: not a tuple"
fromVRecord :: Value -> [(Name, Thunk)]
fromVRecord v = case v of
VRecord fs -> fs
_ -> evalPanic "fromVRecord" ["not a record"]
lookupRecord :: Name -> Value -> Thunk
lookupRecord f rec = case lookup f (fromVRecord rec) of
Just th -> th
Nothing -> error "lookupRecord"
-- | Extract a sequence.
fromSeq :: Value -> [Value]
fromSeq v = case v of
VSeq _ vs -> vs
VWord s -> map VBit (unpackWord s)
VStream vs -> vs
_ -> evalPanic "fromSeq" ["not a sequence"]
-- Errors ----------------------------------------------------------------------

4
src/Cryptol/Testing/Exhaust.hs
View File

@ -88,7 +88,7 @@ typeValues ty =
(TCSeq, ts1) ->
case map tNoUser ts1 of
[ TCon (TC (TCNum n)) _, TCon (TC TCBit) [] ] ->
[ VWord n x | x <- [ 0 .. 2^n - 1 ] ]
[ VWord (BV n x) | x <- [ 0 .. 2^n - 1 ] ]
[ TCon (TC (TCNum n)) _, t ] ->
[ VSeq False xs | xs <- sequence $ genericReplicate n
@ -97,7 +97,7 @@ typeValues ty =
(TCFun, _) -> [] -- We don't generate function values.
(TCTuple n, els) -> [ VTuple n xs | xs <- sequence (map typeValues els)]
(TCTuple _, els) -> [ VTuple xs | xs <- sequence (map typeValues els)]
(TCNewtype _, _) -> []
TCon _ _ -> []

12
src/Cryptol/Testing/Random.hs
View File

@ -11,7 +11,7 @@
{-# LANGUAGE BangPatterns #-}
module Cryptol.Testing.Random where
import Cryptol.Eval.Value (Value(..),ppValue,defaultPPOpts)
import Cryptol.Eval.Value (BV(..),Value,GenValue(..),ppValue,defaultPPOpts)
import Cryptol.Utils.Panic (panic)
import Cryptol.TypeCheck.AST (Name,Type(..),TCon(..),TC(..),tNoUser)
@ -119,7 +119,7 @@ randomWord w sz g =
val = foldl' mk 0 $ genericTake (div (bits + 63) 64) (x' : xs)
finalVal = if sz > 1 && bits > 0 then setBit val (bits - 1) else val
in (VWord w finalVal, g3)
in (VWord (BV w finalVal), g3)
-- | Generate a random infinite stream value.
@ -138,12 +138,12 @@ randomSequence w mkElem sz g =
-- | Generate a random tuple value.
randomTuple :: RandomGen g => [Gen g] -> Gen g
randomTuple gens sz = go 0 [] gens
randomTuple gens sz = go [] gens
where
go !n els [] g = (VTuple n (reverse els), g)
go !n els (mkElem : more) g =
go els [] g = (VTuple (reverse els), g)
go els (mkElem : more) g =
let (v, g1) = mkElem sz g
in go (n+1) (v : els) more g1
in go (v : els) more g1
-- | Generate a random record value.
randomRecord :: RandomGen g => [(Name, Gen g)] -> Gen g

30
src/Cryptol/TypeCheck/AST.hs
View File

@ -290,6 +290,26 @@ tIsVar ty = case tNoUser ty of
TVar x -> Just x
_ -> Nothing
tIsFun :: Type -> Maybe (Type, Type)
tIsFun ty = case tNoUser ty of
TCon (TC TCFun) [a, b] -> Just (a, b)
_ -> Nothing
tIsSeq :: Type -> Maybe (Type, Type)
tIsSeq ty = case tNoUser ty of
TCon (TC TCSeq) [n, a] -> Just (n, a)
_ -> Nothing
tIsBit :: Type -> Bool
tIsBit ty = case tNoUser ty of
TCon (TC TCBit) [] -> True
_ -> False
tIsTuple :: Type -> Maybe [Type]
tIsTuple ty = case tNoUser ty of
TCon (TC (TCTuple _)) ts -> Just ts
_ -> Nothing
pIsFin :: Prop -> Maybe Type
pIsFin ty = case tNoUser ty of
TCon (PC PFin) [t1] -> Just t1
@ -305,6 +325,16 @@ pIsEq ty = case tNoUser ty of
TCon (PC PEqual) [t1,t2] -> Just (t1,t2)
_ -> Nothing
pIsArith :: Prop -> Maybe Type
pIsArith ty = case tNoUser ty of
TCon (PC PArith) [t1] -> Just t1
_ -> Nothing
pIsCmp :: Prop -> Maybe Type
pIsCmp ty = case tNoUser ty of
TCon (PC PCmp) [t1] -> Just t1
_ -> Nothing
pIsNumeric :: Prop -> Bool

4
src/Cryptol/TypeCheck/Solve.hs
View File

@ -250,8 +250,8 @@ exportType ty =
err = panic "exportType" [ "Unexpected type", show ty ]
exportVar :: TVar -> Int
exportVar (TVFree x _ _ _) = x * x
exportVar (TVBound x _) = 2 * x + 1
exportVar (TVFree x _ _ _) = 2 * x -- Free vars are even
exportVar (TVBound x _) = 2 * x + 1 -- Bound vars are odd
--------------------------------------------------------------------------------

96
src/Cryptol/TypeCheck/TypeOf.hs Normal file
View File

@ -0,0 +1,96 @@
-- |
-- Module : $Header$
-- Copyright : (c) 2014 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE Safe #-}
{-# LANGUAGE ViewPatterns #-}
module Cryptol.TypeCheck.TypeOf
( fastTypeOf
, fastSchemaOf
) where
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Subst
import Cryptol.Prims.Types (typeOf)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (fromJust)
-- | Given a typing environment and an expression, compute the type of
-- the expression as quickly as possible, assuming that the expression
-- is well formed with correct type annotations.
fastTypeOf :: Map QName Schema -> Expr -> Type
fastTypeOf tyenv expr =
case expr of
-- Monomorphic fragment
EList es t -> tSeq (tNum (length es)) t
ETuple es -> tTuple (map (fastTypeOf tyenv) es)
ERec fields -> tRec [ (name, fastTypeOf tyenv e) | (name, e) <- fields ]
ESel e sel -> typeSelect (fastTypeOf tyenv e) sel
EIf _ e _ -> fastTypeOf tyenv e
EComp t _ _ -> t
EAbs x t e -> tFun t (fastTypeOf (Map.insert x (Forall [] [] t) tyenv) e)
EApp e _ -> case tIsFun (fastTypeOf tyenv e) of
Just (_, t) -> t
Nothing -> error "internal error"
ECast _ t -> t
-- Polymorphic fragment
ECon {} -> polymorphic
EVar {} -> polymorphic
ETAbs {} -> polymorphic
ETApp {} -> polymorphic
EProofAbs {} -> polymorphic
EProofApp {} -> polymorphic
EWhere {} -> polymorphic
where
polymorphic =
case fastSchemaOf tyenv expr of
Forall [] [] ty -> ty
_ -> error "internal error: unexpected polymorphic type"
fastSchemaOf :: Map QName Schema -> Expr -> Schema
fastSchemaOf tyenv expr =
case expr of
-- Polymorphic fragment
ECon econ -> typeOf econ
EVar x -> fromJust (Map.lookup x tyenv)
ETAbs tparam e -> case fastSchemaOf tyenv e of
Forall tparams props ty -> Forall (tparam : tparams) props ty
ETApp e t -> case fastSchemaOf tyenv e of
Forall (tparam : tparams) props ty -> Forall tparams (apSubst s props) (apSubst s ty)
where s = singleSubst (tpVar tparam) t
_ -> error "internal error"
EProofAbs p e -> case fastSchemaOf tyenv e of
Forall [] props ty -> Forall [] (p : props) ty
_ -> error "internal error"
EProofApp e -> case fastSchemaOf tyenv e of
Forall [] (_ : props) ty -> Forall [] props ty
_ -> error "internal error"
EWhere e dgs -> fastSchemaOf (foldr addDeclGroup tyenv dgs) e
where addDeclGroup (Recursive ds) = flip (foldr addDecl) ds
addDeclGroup (NonRecursive d) = addDecl d
addDecl d = Map.insert (dName d) (dSignature d)
-- Monomorphic fragment
EList {} -> monomorphic
ETuple {} -> monomorphic
ERec {} -> monomorphic
ESel {} -> monomorphic
EIf {} -> monomorphic
EComp {} -> monomorphic
EApp {} -> monomorphic
EAbs {} -> monomorphic
ECast {} -> monomorphic
where
monomorphic = Forall [] [] (fastTypeOf tyenv expr)
-- | Yields the return type of the selector on the given argument type.
typeSelect :: Type -> Selector -> Type
typeSelect (TCon _tctuple ts) (TupleSel i _) = ts !! (i - 1)
typeSelect (TRec fields) (RecordSel n _) = fromJust (lookup n fields)
typeSelect (TCon _tcseq [_, a]) (ListSel _ _) = a
typeSelect _ _ = error "internal error: typeSelect"

2
src/Cryptol/Utils/Panic.hs
View File

@ -26,7 +26,7 @@ data CryptolPanic = CryptolPanic { panicLoc :: String
instance Show CryptolPanic where
show p = unlines $
[ "You have encountered a bug in Cryptol's implementation."
, "*** Please report this problem to cryptol-bugs@galois.com"
, "*** Please create an issue at https://github.com/galoisinc/cryptol/issues"
, ""
, "%< --------------------------------------------------- "
] ++ rev ++

2
tests/issues/issue086.icry.stdout
View File

@ -1,2 +1,2 @@
Loading module Cryptol
&& : {a} a -> a -> a
(&&) : {a} a -> a -> a

2
tests/issues/issue289.icry.stdout
View File

@ -2,5 +2,5 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
Q.E.D.
Q.E.D.
av1 3701879183 3218045100 = False
Q.E.D.

4
tests/regression/r03.icry.stdout
View File

@ -1,5 +1,5 @@
Loading module Cryptol
Loading module Cryptol
Loading module r03
nQueens:Solution 5 [4, 2, 0, 3, 1] = True
(nQueensProve:Solution 4) [2, 0, 3, 1] = False
(nQueens : Solution 5) [4, 2, 0, 3, 1] = True
(nQueensProve : Solution 4) [2, 0, 3, 1] = False