mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-28 09:23:04 +03:00
Merge branch 'master' into abstract-types
This commit is contained in:
Iavor Diatchki
commit
2ef0a67d9b
@ -3,7 +3,7 @@ Status](https://travis-ci.org/GaloisInc/cryptol.svg?branch=master)](https://trav
|
||||
|
||||
# Cryptol, version 2
|
||||
|
||||
This version of Cryptol is (C) 2013-2016 Galois, Inc., and
|
||||
This version of Cryptol is (C) 2013-2017 Galois, Inc., and
|
||||
distributed under a standard, three-clause BSD license. Please see
|
||||
the file LICENSE, distributed with this software, for specific
|
||||
terms and conditions.
|
||||
|
||||
@ -64,7 +64,7 @@ library
|
||||
random >= 1.0.1,
|
||||
sbv >= 7.0,
|
||||
smtLib >= 1.0.7,
|
||||
simple-smt >= 0.7.0,
|
||||
simple-smt >= 0.7.1,
|
||||
strict,
|
||||
syb >= 0.4,
|
||||
text >= 1.1,
|
||||
|
||||
@ -107,12 +107,12 @@ Operator Associativity
|
||||
`==>` right
|
||||
`\/` right
|
||||
`/\` right
|
||||
`||` right
|
||||
`&&` right
|
||||
`->` (types) right
|
||||
`!=` `==` not associative
|
||||
`>` `<` `<=` `>=` `<$` `>$` `<=$` `>=$` not associative
|
||||
`||` right
|
||||
`^` left
|
||||
`&&` right
|
||||
`#` right
|
||||
`>>` `<<` `>>>` `<<<` `>>$` left
|
||||
`+` `-` left
|
||||
@ -168,11 +168,11 @@ Operator Associativity Description
|
||||
`==>` right Short-cut implication
|
||||
`\/` right Short-cut or
|
||||
`/\` right Short-cut and
|
||||
`||` right Logical or
|
||||
`&&` right Logical and
|
||||
`!=` `==` none Not equals, equals
|
||||
`>` `<` `<=` `>=` `<$` `>$` `<=$` `>=$` none Comparisons
|
||||
`||` right Logical or
|
||||
`^` left Exclusive-or
|
||||
`&&` right Logical and
|
||||
`~` right Logical negation
|
||||
|
||||
Table: Bit operations.
|
||||
|
||||
BIN
docs/Syntax.pdf
BIN
docs/Syntax.pdf
Binary file not shown.
94
examples/Karatsuba.cry
Normal file
94
examples/Karatsuba.cry
Normal file
@ -0,0 +1,94 @@
|
||||
/*
|
||||
* Copyright (c) 2017 Galois, Inc.
|
||||
* Distributed under the terms of the BSD3 license (see LICENSE file)
|
||||
*
|
||||
* This module defines a Karatsuba multiplier, which is polymorphic over the
|
||||
* bitwidth of the constituent limbs and the size of the inputs.
|
||||
*
|
||||
* Note the trick of using `make_atleast` in the recursive case to teach the
|
||||
* typecheker that the current bitwidth is long enough for the split multiplier
|
||||
* to be sensible. The minimum width for which the splitting recursive case
|
||||
* works out happens to be 6. This is the smallest width for which the
|
||||
* divide-in-half strategy leaves enough bits left over for the additions
|
||||
* steps not to overflow.
|
||||
*
|
||||
* Note that if one wishes to simulate using a standard CPU to perform Karatsuba
|
||||
* multiplies, the limb width should be set to ONE LESS THAN the standard
|
||||
* machine word size, e.g. 63 bits for a 64 bit machine. This ensures that
|
||||
* the intermediate additions will fit into a machine word. Note that the the
|
||||
* final `2*(limb+1)`-width additions will also have to be assembled manually
|
||||
* using "add with carry" operations or similar.
|
||||
*/
|
||||
|
||||
module Karatsuba where
|
||||
|
||||
// The divide-and-conquer Karatsuba multiplier. If the argument width
|
||||
// is greater than the limb width, then the recursive `splitmult` multiplier
|
||||
// is called; otherwise, a standard multiply is used.
|
||||
|
||||
kmult : {limb,n} (fin n, fin limb, limb >= 6, n >= 1) => [n] -> [n] -> [2*n]
|
||||
|
||||
kmult x y =
|
||||
if `n >= (demote`{limb, max (width limb) (width n)}) then
|
||||
take (splitmult`{limb} (make_atleast`{limb} x) (make_atleast`{limb} y))
|
||||
else
|
||||
(zero#x)*(zero#y)
|
||||
|
||||
|
||||
// Force a bitvector to be at least `n` bits long. As used above, this operation
|
||||
// should always be a no-op, but teaches the typechecker a necessary inequality
|
||||
// to call the `splitmult` operation.
|
||||
|
||||
make_atleast : {n, m, a} (fin n, fin m, Zero a) => [m]a -> [max n m]a
|
||||
make_atleast x = zero#x
|
||||
|
||||
|
||||
|
||||
// Execute the recursive step of Karatsuba's multiplication. Split the
|
||||
// input words into high and low bit portions; then perform three
|
||||
// recursive multiplies using these intermediate, shorter bitsequences.
|
||||
|
||||
splitmult : {limb,n} (fin n, fin limb, limb >= 6, n >= 6)
|
||||
=> [n] -> [n] -> [2*n]
|
||||
|
||||
splitmult x y = (ac # bd) + (zero # ad_bc # (zero:[low]))
|
||||
where
|
||||
type hi = n/2
|
||||
type low = n - hi
|
||||
|
||||
(a,b) = splitAt`{hi} x
|
||||
(c,d) = splitAt`{hi} y
|
||||
|
||||
ac : [2*hi]
|
||||
ac = kmult`{limb,hi} a c
|
||||
|
||||
bd : [2*low]
|
||||
bd = kmult`{limb,low} b d
|
||||
|
||||
a_b = (zext a) + (zext b)
|
||||
c_d = (zext c) + (zext d)
|
||||
|
||||
ad_bc : [2*(low+1)]
|
||||
ad_bc = (kmult`{limb,low+1} a_b c_d) - (zext ac) - (zext bd)
|
||||
|
||||
|
||||
// Verify Karatsuba's algorithm computes the correct answer
|
||||
// for some fixed settings of the parameters.
|
||||
//
|
||||
// SMT solvers have great difficutly with these proofs, and I have
|
||||
// only gotten small bit sizes to return with successful proofs.
|
||||
|
||||
property splitmult_correct_tiny (x:[9]) (y:[9]) =
|
||||
zext x * zext y == splitmult`{limb=7} x y
|
||||
|
||||
property splitmult_correct_small (x:[11]) (y:[11]) =
|
||||
zext x * zext y == splitmult`{limb=7} x y
|
||||
|
||||
property splitmult_correct_medium(x:[17]) (y:[17]) =
|
||||
zext x * zext y == splitmult`{limb=7} x y
|
||||
|
||||
property splitmult_correct_large (x:[59]) (y:[59]) =
|
||||
zext x * zext y == splitmult`{limb=7} x y
|
||||
|
||||
property splitmult_correct_huge (x:[511]) (y:[511]) =
|
||||
zext x * zext y == splitmult`{limb=63} x y
|
||||
271
examples/MD5.cry
Normal file
271
examples/MD5.cry
Normal file
@ -0,0 +1,271 @@
|
||||
// Copyright (c) 2001, 2014 Galois, Inc.
|
||||
// Distributed under the terms of the BSD3 license (see LICENSE file)
|
||||
//
|
||||
// MD5 digest algorithm from RFC 1321
|
||||
// https://www.ietf.org/rfc/rfc1321.txt
|
||||
//
|
||||
// Based on a previous Cryptol 1.* implementation
|
||||
|
||||
// Swap byte order from network to host order (long word)
|
||||
ntohl : [32] -> [32]
|
||||
ntohl w = join (reverse (groupBy`{8} w))
|
||||
|
||||
// Swap byte order from host to network order (long word)
|
||||
htonl : [32] -> [32]
|
||||
htonl w = join (reverse (groupBy`{8} w))
|
||||
|
||||
// Swap byte order from host to network order (long long word)
|
||||
htonll : [64] -> [64]
|
||||
htonll w = join (reverse (groupBy`{8} w))
|
||||
|
||||
// apply a function to every element of a sequence
|
||||
map : {n, a, b} (a -> b) -> [n]a -> [n]b
|
||||
map f xs = [ f x | x <- xs ]
|
||||
|
||||
// fold with left associativity
|
||||
foldl : {n, a, b} (fin n) => a -> (a -> b -> a) -> [n]b -> a
|
||||
foldl seed f xs = res ! 0
|
||||
where res = [seed] # [ f a x | a <- res
|
||||
| x <- xs
|
||||
]
|
||||
|
||||
// Test driver. Given a sequence of bytes, calculate the MD5 sum.
|
||||
test s = md5 (join s)
|
||||
|
||||
// Reference implementation of MD5 on exactly 16 bytes.
|
||||
|
||||
md5_ref : [16][8] -> [16][8]
|
||||
md5_ref msg = map reverse (groupBy`{8} (md5`{p=319} (join (map reverse msg))))
|
||||
|
||||
md5_ref' : [128] -> [128]
|
||||
md5_ref' msg = join (md5_ref (groupBy`{8} msg))
|
||||
|
||||
|
||||
|
||||
// The state of the MD5 algorithm after each 512 bit block
|
||||
// consists of 4 32-bit words.
|
||||
type MD5State = ([32],[32],[32],[32])
|
||||
|
||||
// Main MD5 algorithm.
|
||||
//
|
||||
// First, pad the message to a multiple of 512 bits.
|
||||
// Next, initilize the MD5 state using the fixed values from the RFC.
|
||||
// Then, process each message block in turn by computing
|
||||
// the MD5 rounds using the message block. Add the result
|
||||
// of the final round to the current MD5 state.
|
||||
// Finally, return the current MD5 state after all blocks are processed,
|
||||
// interpreting the 4 32-bit words as a single 128-bit sequence.
|
||||
|
||||
md5 : {a, b, p} (fin p, 512 * b == 65 + (a + p), 64 >= width a, 511 >= p) =>
|
||||
[a] -> [128]
|
||||
md5 msg = md5output finalState
|
||||
where
|
||||
finalState : MD5State
|
||||
finalState = foldl initialMD5State processBlock blocks
|
||||
|
||||
blocks : [b][512]
|
||||
blocks = groupBy`{512} (pad `{a,p} msg)
|
||||
|
||||
add : MD5State -> MD5State -> MD5State
|
||||
add (a, b, c, d) (e, f, g, h) = (a + e, b + f, c + g, d + h)
|
||||
|
||||
processBlock : MD5State -> [512] -> MD5State
|
||||
processBlock st blk = add st (computeRounds (decodeBlock blk) st)
|
||||
|
||||
|
||||
// Initial seed for the digest rounds
|
||||
//
|
||||
// See RFC 1321, section 3.3
|
||||
|
||||
initialMD5State : MD5State
|
||||
initialMD5State = (A, B, C, D)
|
||||
where
|
||||
f x = ntohl (join x)
|
||||
A = f [ 0x01, 0x23, 0x45, 0x67 ]
|
||||
B = f [ 0x89, 0xAB, 0xCD, 0xEF ]
|
||||
C = f [ 0xFE, 0xDC, 0xBA, 0x98 ]
|
||||
D = f [ 0x76, 0x54, 0x32, 0x10 ]
|
||||
|
||||
|
||||
// Each MD5 message block 512 bits long, interpreted as a sequence of 16 32-bit words
|
||||
// Each word is given as a sequence of 4 bytes, with LEAST significant byte first
|
||||
// Each byte is given as a sequence of 8 bits, with MOST significant bit first
|
||||
//
|
||||
// The output of the algorithm is a sequence of 4 words, interpreted as above
|
||||
//
|
||||
// See RFC 1321, section 2
|
||||
|
||||
decodeBlock : [512] -> [16][32]
|
||||
decodeBlock s = map ntohl (groupBy`{32} s)
|
||||
|
||||
|
||||
// Interpret 4 32-bit words as a single 128-bit sequence
|
||||
//
|
||||
// See RFC 1321 section 3.5
|
||||
|
||||
md5output : MD5State -> [128]
|
||||
md5output (a,b,c,d) = htonl a # htonl b # htonl c # htonl d
|
||||
|
||||
|
||||
|
||||
// Given an arbitrary byte sequence whose length can be described
|
||||
// by a 64-bit number, pad the message so it is exactly a multiple of 512.
|
||||
//
|
||||
// This is done by adding a single 1 bit to the end of the message, and
|
||||
// then adding enough zero bits to make the whole message 64 bits shorter
|
||||
// than a multiple of 512. The size (in bits) of the original message is
|
||||
// then appended to complete the padded message.
|
||||
//
|
||||
// See RFC 1321, sections 3.1 and 3.2
|
||||
|
||||
pad : {a, p} (fin p, 64 >= width a) => [a] -> [65 + (a + p)]
|
||||
pad msg =
|
||||
msg # [True] # zero # htonll sz
|
||||
where
|
||||
sz : [64]
|
||||
sz = width msg
|
||||
|
||||
|
||||
|
||||
// Given a message block (interpreted as 16 32-bit words) and a current MD5 state
|
||||
// (as 4 32-bit words) compute the values of all the rounds of the MD5 algorithm.
|
||||
//
|
||||
// In the main MD5 function, the final round will be used to compute the next MD5 state.
|
||||
//
|
||||
// See RFC 1321, section 3.4
|
||||
|
||||
computeRounds : [16][32] -> MD5State -> MD5State
|
||||
computeRounds msg st = rounds (msg,st) @ 64
|
||||
|
||||
rounds : ([16][32], MD5State) -> [65]MD5State
|
||||
rounds (msg, (a0, b0, c0, d0)) =
|
||||
[ (a, b, c, d) | a <- as
|
||||
| b <- bs
|
||||
| c <- cs
|
||||
| d <- ds
|
||||
]
|
||||
where
|
||||
bs =
|
||||
[b0] #
|
||||
[box (i, a, b, c, d, m, t, s) | i <- [0 .. 63]
|
||||
| a <- as
|
||||
| b <- bs
|
||||
| c <- cs
|
||||
| d <- ds
|
||||
| m <- join [m @@ p | m <- [msg, msg, msg, msg]
|
||||
| p <- permutes
|
||||
]
|
||||
| t <- sineTbl
|
||||
| s <- s_constants
|
||||
]
|
||||
cs = [c0] # bs
|
||||
ds = [d0] # cs
|
||||
as = [a0] # ds
|
||||
|
||||
|
||||
// 'S' constants from the MD5 algorithm, used to indicated how many
|
||||
// bits to rotate in the box function.
|
||||
//
|
||||
// See RFC 1321, section 3.4, and the appendix on page 10
|
||||
|
||||
s_constants : [64][6]
|
||||
s_constants =
|
||||
repeat4 [7, 12, 17, 22] #
|
||||
repeat4 [5, 9, 14, 20] #
|
||||
repeat4 [4, 11, 16, 23] #
|
||||
repeat4 [6, 10, 15, 21]
|
||||
where
|
||||
repeat4 abcd = abcd # abcd # abcd # abcd
|
||||
|
||||
|
||||
// This table of permutations indicates which word of the message block to
|
||||
// use in a given MD5 round. Its structure is most evident via observing
|
||||
// the indices of the message block in the order they are used in the MD5
|
||||
// reference implementation.
|
||||
//
|
||||
// See the appendix of RFC 1321, starting on page 13.
|
||||
|
||||
permutes : [4][16][4]
|
||||
permutes =
|
||||
[ [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
|
||||
, [ 1, 6, 11, 0, 5, 10, 15, 4, 9, 14, 3, 8, 13, 2, 7, 12]
|
||||
, [ 5, 8, 11, 14, 1, 4, 7, 10, 13, 0, 3, 6, 9, 12, 15, 2]
|
||||
, [ 0, 7, 14, 5, 12, 3, 10, 1, 8, 15, 6, 13, 4, 11, 2, 9]
|
||||
]
|
||||
|
||||
|
||||
// The main "box" operation. The first argument indicates
|
||||
// the round number, which is used to select between the box
|
||||
// operations, F, G, H, and I.
|
||||
//
|
||||
// See RFC 1321, section 3.4
|
||||
|
||||
box : ([6], [32], [32], [32], [32], [32], [32], [6]) -> [32]
|
||||
box (i, a, b, c, d, m, t, s) =
|
||||
b + (a + boxfunc (i, b, c, d) + m + t <<< s)
|
||||
|
||||
boxfunc : ([6],[32],[32],[32]) -> [32]
|
||||
boxfunc (i, b, c, d) =
|
||||
if i < 16 then F (b, c, d) else
|
||||
if i < 32 then G (b, c, d) else
|
||||
if i < 48 then H (b, c, d) else
|
||||
I (b, c, d)
|
||||
|
||||
F : ([32], [32], [32]) -> [32]
|
||||
F (x, y, z) = x && y || (~x) && z
|
||||
|
||||
G : ([32], [32], [32]) -> [32]
|
||||
G (x, y, z) = x && z || y && ~z
|
||||
|
||||
H : ([32], [32], [32]) -> [32]
|
||||
H (x, y, z) = x ^ y ^ z
|
||||
|
||||
I : ([32], [32], [32]) -> [32]
|
||||
I (x, y, z) = y ^ (x || ~z)
|
||||
|
||||
|
||||
// The table of values generated from the sin function, as described
|
||||
// in RFC 1321, section 3.4. These values are transcribed from
|
||||
// the appendix, starting on page 13.
|
||||
|
||||
sineTbl : [64][32]
|
||||
sineTbl =
|
||||
[0xD76AA478, 0xE8C7B756, 0x242070DB, 0xC1BDCEEE, 0xF57C0FAF,
|
||||
0x4787C62A, 0xA8304613, 0xFD469501, 0x698098D8, 0x8B44F7AF,
|
||||
0xFFFF5BB1, 0x895CD7BE, 0x6B901122, 0xFD987193, 0xA679438E,
|
||||
0x49B40821, 0xF61E2562, 0xC040B340, 0x265E5A51, 0xE9B6C7AA,
|
||||
0xD62F105D, 0x02441453, 0xD8A1E681, 0xE7D3FBC8, 0x21E1CDE6,
|
||||
0xC33707D6, 0xF4D50D87, 0x455A14ED, 0xA9E3E905, 0xFCEFA3F8,
|
||||
0x676F02D9, 0x8D2A4C8A, 0xFFFA3942, 0x8771F681, 0x6D9D6122,
|
||||
0xFDE5380C, 0xA4BEEA44, 0x4BDECFA9, 0xF6BB4B60, 0xBEBFBC70,
|
||||
0x289B7EC6, 0xEAA127FA, 0xD4EF3085, 0x04881D05, 0xD9D4D039,
|
||||
0xE6DB99E5, 0x1FA27CF8, 0xC4AC5665, 0xF4292244, 0x432AFF97,
|
||||
0xAB9423A7, 0xFC93A039, 0x655B59C3, 0x8F0CCC92, 0xFFEFF47D,
|
||||
0x85845DD1, 0x6FA87E4F, 0xFE2CE6E0, 0xA3014314, 0x4E0811A1,
|
||||
0xF7537E82, 0xBD3AF235, 0x2AD7D2BB, 0xEB86D391]
|
||||
|
||||
|
||||
// The MD5 test suite from RFC 1321, appendix A.5
|
||||
|
||||
property r0 = test ""
|
||||
== 0xd41d8cd98f00b204e9800998ecf8427e
|
||||
|
||||
property r1 = test "a"
|
||||
== 0x0cc175b9c0f1b6a831c399e269772661
|
||||
|
||||
property r2 = test "abc"
|
||||
== 0x900150983cd24fb0d6963f7d28e17f72
|
||||
|
||||
property r3 = test "message digest"
|
||||
== 0xf96b697d7cb7938d525a2f31aaf161d0
|
||||
|
||||
property r4 = test "abcdefghijklmnopqrstuvwxyz"
|
||||
== 0xc3fcd3d76192e4007dfb496cca67e13b
|
||||
|
||||
property r5 = test "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789"
|
||||
== 0xd174ab98d277d9f5a5611c2c9f419d9f
|
||||
|
||||
property r6 = test "12345678901234567890123456789012345678901234567890123456789012345678901234567890"
|
||||
== 0x57edf4a22be3c955ac49da2e2107b67a
|
||||
|
||||
alltests = r0 /\ r1 /\ r2 /\ r3 /\ r4 /\ r5 /\ r6
|
||||
@ -10,14 +10,19 @@ module Cryptol where
|
||||
*/
|
||||
primitive demote : {val, bits} (fin val, fin bits, bits >= width val) => [bits]
|
||||
|
||||
/**
|
||||
* The integer value corresponding to a numeric type.
|
||||
*/
|
||||
primitive integer : {val} (fin val) => Integer
|
||||
|
||||
infixr 5 ==>
|
||||
infixr 10 \/
|
||||
infixr 15 /\
|
||||
infixr 20 ||
|
||||
infixr 25 &&
|
||||
infix 30 ==, ===, !=, !==
|
||||
infix 40 >, >=, <, <=, <$, >$, <=$, >=$
|
||||
infixl 50 ^
|
||||
infix 20 ==, ===, !=, !==
|
||||
infix 30 >, >=, <, <=, <$, >$, <=$, >=$
|
||||
infixr 40 ||
|
||||
infixl 45 ^
|
||||
infixr 50 &&
|
||||
infixr 60 #
|
||||
infixl 70 <<, <<<, >>, >>>, >>$
|
||||
infixl 80 +, -
|
||||
@ -277,6 +282,16 @@ primitive (^) : {a} (Logic a) => a -> a -> a
|
||||
*/
|
||||
primitive zero : {a} (Zero a) => a
|
||||
|
||||
/**
|
||||
* Converts a bitvector to a non-negative integer in the range 0 to 2^^n-1.
|
||||
*/
|
||||
primitive toInteger : {a} (fin a) => [a] -> Integer
|
||||
|
||||
/**
|
||||
* Converts an unbounded integer to a finite bitvector, reducing modulo 2^^n.
|
||||
*/
|
||||
primitive fromInteger : {a} (fin a) => Integer -> [a]
|
||||
|
||||
/**
|
||||
* Left shift. The first argument is the sequence to shift, the second is the
|
||||
* number of positions to shift by.
|
||||
|
||||
@ -37,6 +37,7 @@ import Cryptol.Utils.Panic (panic)
|
||||
import Cryptol.Utils.PP
|
||||
|
||||
import Control.Monad
|
||||
import qualified Data.Sequence as Seq
|
||||
import Data.List
|
||||
import Data.Maybe
|
||||
import qualified Data.Map.Strict as Map
|
||||
@ -44,25 +45,25 @@ import qualified Data.Map.Strict as Map
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
|
||||
type EvalEnv = GenEvalEnv Bool BV
|
||||
type EvalEnv = GenEvalEnv Bool BV Integer
|
||||
|
||||
-- Expression Evaluation -------------------------------------------------------
|
||||
|
||||
-- | Extend the given evaluation environment with all the declarations
|
||||
-- contained in the given module.
|
||||
moduleEnv :: EvalPrims b w
|
||||
=> Module -- ^ Module containing declarations to evaluate
|
||||
-> GenEvalEnv b w -- ^ Environment to extend
|
||||
-> Eval (GenEvalEnv b w)
|
||||
moduleEnv :: EvalPrims b w i
|
||||
=> Module -- ^ Module containing declarations to evaluate
|
||||
-> GenEvalEnv b w i -- ^ Environment to extend
|
||||
-> Eval (GenEvalEnv b w i)
|
||||
moduleEnv m env = evalDecls (mDecls m) =<< evalNewtypes (mNewtypes m) env
|
||||
|
||||
-- | Evaluate a Cryptol expression to a value. This evaluator is parameterized
|
||||
-- by the `EvalPrims` class, which defines the behavior of bits and words, in
|
||||
-- addition to providing implementations for all the primitives.
|
||||
evalExpr :: EvalPrims b w
|
||||
=> GenEvalEnv b w -- ^ Evaluation environment
|
||||
evalExpr :: EvalPrims b w i
|
||||
=> GenEvalEnv b w i -- ^ Evaluation environment
|
||||
-> Expr -- ^ Expression to evaluate
|
||||
-> Eval (GenValue b w)
|
||||
-> Eval (GenValue b w i)
|
||||
evalExpr env expr = case expr of
|
||||
|
||||
-- Try to detect when the user has directly written a finite sequence of
|
||||
@ -73,8 +74,10 @@ evalExpr env expr = case expr of
|
||||
| isTBit tyv -> {-# SCC "evalExpr->Elist/bit" #-}
|
||||
return $ VWord len $ return $
|
||||
case tryFromBits vs of
|
||||
Just w | len < largeBitSize -> WordVal w
|
||||
_ -> BitsVal len $ IndexSeqMap $ \i -> genericIndex vs i
|
||||
Just w -> WordVal w
|
||||
Nothing
|
||||
| len < largeBitSize -> BitsVal $ Seq.fromList $ map (fromVBit <$>) vs
|
||||
| otherwise -> LargeBitsVal len $ IndexSeqMap $ \i -> genericIndex vs i
|
||||
| otherwise -> {-# SCC "evalExpr->EList" #-}
|
||||
return $ VSeq len $ finiteSeqMap vs
|
||||
where
|
||||
@ -158,17 +161,17 @@ evalExpr env expr = case expr of
|
||||
|
||||
-- Newtypes --------------------------------------------------------------------
|
||||
|
||||
evalNewtypes :: EvalPrims b w
|
||||
evalNewtypes :: EvalPrims b w i
|
||||
=> Map.Map Name Newtype
|
||||
-> GenEvalEnv b w
|
||||
-> Eval (GenEvalEnv b w)
|
||||
-> GenEvalEnv b w i
|
||||
-> Eval (GenEvalEnv b w i)
|
||||
evalNewtypes nts env = foldM (flip evalNewtype) env $ Map.elems nts
|
||||
|
||||
-- | Introduce the constructor function for a newtype.
|
||||
evalNewtype :: EvalPrims b w
|
||||
evalNewtype :: EvalPrims b w i
|
||||
=> Newtype
|
||||
-> GenEvalEnv b w
|
||||
-> Eval (GenEvalEnv b w)
|
||||
-> GenEvalEnv b w i
|
||||
-> Eval (GenEvalEnv b w i)
|
||||
evalNewtype nt = bindVar (ntName nt) (return (foldr tabs con (ntParams nt)))
|
||||
where
|
||||
tabs _tp body = tlam (\ _ -> body)
|
||||
@ -179,16 +182,16 @@ evalNewtype nt = bindVar (ntName nt) (return (foldr tabs con (ntParams nt)))
|
||||
|
||||
-- | Extend the given evaluation environment with the result of evaluating the
|
||||
-- given collection of declaration groups.
|
||||
evalDecls :: EvalPrims b w
|
||||
evalDecls :: EvalPrims b w i
|
||||
=> [DeclGroup] -- ^ Declaration groups to evaluate
|
||||
-> GenEvalEnv b w -- ^ Environment to extend
|
||||
-> Eval (GenEvalEnv b w)
|
||||
-> GenEvalEnv b w i -- ^ Environment to extend
|
||||
-> Eval (GenEvalEnv b w i)
|
||||
evalDecls dgs env = foldM evalDeclGroup env dgs
|
||||
|
||||
evalDeclGroup :: EvalPrims b w
|
||||
=> GenEvalEnv b w
|
||||
evalDeclGroup :: EvalPrims b w i
|
||||
=> GenEvalEnv b w i
|
||||
-> DeclGroup
|
||||
-> Eval (GenEvalEnv b w)
|
||||
-> Eval (GenEvalEnv b w i)
|
||||
evalDeclGroup env dg = do
|
||||
case dg of
|
||||
Recursive ds -> do
|
||||
@ -221,10 +224,10 @@ evalDeclGroup env dg = do
|
||||
-- binding is indistinguishable from its eta-expanded form. The straightforward solution
|
||||
-- to this is to force an eta-expansion procedure on all recursive definitions.
|
||||
-- However, for the so-called 'Value' types we can instead optimistically use the 'delayFill'
|
||||
-- operation and only fall back on full eta-expansion if the thunk is double-forced.
|
||||
fillHole :: BitWord b w
|
||||
=> GenEvalEnv b w
|
||||
-> (Name, Schema, Eval (GenValue b w), Eval (GenValue b w) -> Eval ())
|
||||
-- operation and only fall back on full eta expansion if the thunk is double-forced.
|
||||
fillHole :: BitWord b w i
|
||||
=> GenEvalEnv b w i
|
||||
-> (Name, Schema, Eval (GenValue b w i), Eval (GenValue b w i) -> Eval ())
|
||||
-> Eval ()
|
||||
fillHole env (nm, sch, _, fill) = do
|
||||
case lookupVar nm env of
|
||||
@ -239,7 +242,7 @@ fillHole env (nm, sch, _, fill) = do
|
||||
-- be implemented rather more efficently than general types because we can
|
||||
-- rely on the 'delayFill' operation to build a thunk that falls back on performing
|
||||
-- eta-expansion rather than doing it eagerly.
|
||||
isValueType :: GenEvalEnv b w -> Schema -> Bool
|
||||
isValueType :: GenEvalEnv b w i -> Schema -> Bool
|
||||
isValueType env Forall{ sVars = [], sProps = [], sType = t0 }
|
||||
= go (evalValType (envTypes env) t0)
|
||||
where
|
||||
@ -253,15 +256,14 @@ isValueType _ _ = False
|
||||
|
||||
|
||||
-- | Eta-expand a word value. This forces an unpacked word representation.
|
||||
etaWord :: BitWord b w
|
||||
etaWord :: BitWord b w i
|
||||
=> Integer
|
||||
-> Eval (GenValue b w)
|
||||
-> Eval (WordValue b w)
|
||||
-> Eval (GenValue b w i)
|
||||
-> Eval (WordValue b w i)
|
||||
etaWord n x = do
|
||||
w <- delay Nothing (fromWordVal "during eta-expansion" =<< x)
|
||||
return $ BitsVal n $ IndexSeqMap $ \i ->
|
||||
do w' <- w
|
||||
VBit <$> indexWordValue w' (toInteger i)
|
||||
return $ BitsVal $ Seq.fromFunction (fromInteger n) $ \i ->
|
||||
do w' <- w; indexWordValue w' (toInteger i)
|
||||
|
||||
|
||||
-- | Given a simulator value and its type, fully eta-expand the value. This
|
||||
@ -270,12 +272,12 @@ etaWord n x = do
|
||||
-- the correct evaluation semantics of recursive definitions. Otherwise,
|
||||
-- expressions that should be expected to produce well-defined values in the
|
||||
-- denotational semantics will fail to terminate instead.
|
||||
etaDelay :: BitWord b w
|
||||
etaDelay :: BitWord b w i
|
||||
=> String
|
||||
-> GenEvalEnv b w
|
||||
-> GenEvalEnv b w i
|
||||
-> Schema
|
||||
-> Eval (GenValue b w)
|
||||
-> Eval (GenValue b w)
|
||||
-> Eval (GenValue b w i)
|
||||
-> Eval (GenValue b w i)
|
||||
etaDelay msg env0 Forall{ sVars = vs0, sType = tp0 } = goTpVars env0 vs0
|
||||
where
|
||||
goTpVars env [] x = go (evalValType (envTypes env) tp0) x
|
||||
@ -289,8 +291,9 @@ etaDelay msg env0 Forall{ sVars = vs0, sType = tp0 } = goTpVars env0 vs0
|
||||
|
||||
go tp (Ready x) =
|
||||
case x of
|
||||
VBit _ -> return x
|
||||
VWord _ _ -> return x
|
||||
VBit _ -> return x
|
||||
VInteger _ -> return x
|
||||
VWord _ _ -> return x
|
||||
VSeq n xs
|
||||
| TVSeq _nt el <- tp
|
||||
-> return $ VSeq n $ IndexSeqMap $ \i -> go el (lookupSeqMap xs i)
|
||||
@ -320,6 +323,7 @@ etaDelay msg env0 Forall{ sVars = vs0, sType = tp0 } = goTpVars env0 vs0
|
||||
go tp x =
|
||||
case tp of
|
||||
TVBit -> x
|
||||
TVInteger -> x
|
||||
|
||||
TVSeq n TVBit ->
|
||||
do w <- delayFill (fromWordVal "during eta-expansion" =<< x) (etaWord n x)
|
||||
@ -358,7 +362,7 @@ etaDelay msg env0 Forall{ sVars = vs0, sType = tp0 } = goTpVars env0 vs0
|
||||
|
||||
|
||||
declHole :: Decl
|
||||
-> Eval (Name, Schema, Eval (GenValue b w), Eval (GenValue b w) -> Eval ())
|
||||
-> Eval (Name, Schema, Eval (GenValue b w i), Eval (GenValue b w i) -> Eval ())
|
||||
declHole d =
|
||||
case dDefinition d of
|
||||
DPrim -> evalPanic "Unexpected primitive declaration in recursive group"
|
||||
@ -379,11 +383,11 @@ declHole d =
|
||||
-- handle the subtle name-binding issues that arise from recursive
|
||||
-- definitions. The 'read only' environment is used to bring recursive
|
||||
-- names into scope while we are still defining them.
|
||||
evalDecl :: EvalPrims b w
|
||||
=> GenEvalEnv b w -- ^ A 'read only' environment for use in declaration bodies
|
||||
-> GenEvalEnv b w -- ^ An evaluation environment to extend with the given declaration
|
||||
-> Decl -- ^ The declaration to evaluate
|
||||
-> Eval (GenEvalEnv b w)
|
||||
evalDecl :: EvalPrims b w i
|
||||
=> GenEvalEnv b w i -- ^ A 'read only' environment for use in declaration bodies
|
||||
-> GenEvalEnv b w i -- ^ An evaluation environment to extend with the given declaration
|
||||
-> Decl -- ^ The declaration to evaluate
|
||||
-> Eval (GenEvalEnv b w i)
|
||||
evalDecl renv env d =
|
||||
case dDefinition d of
|
||||
DPrim -> bindVarDirect (dName d) (evalPrim d) env
|
||||
@ -395,11 +399,11 @@ evalDecl renv env d =
|
||||
-- | Apply the the given "selector" form to the given value. This function pushes
|
||||
-- tuple and record selections pointwise down into other value constructs
|
||||
-- (e.g., streams and functions).
|
||||
evalSel :: forall b w
|
||||
. EvalPrims b w
|
||||
=> GenValue b w
|
||||
evalSel :: forall b w i
|
||||
. EvalPrims b w i
|
||||
=> GenValue b w i
|
||||
-> Selector
|
||||
-> Eval (GenValue b w)
|
||||
-> Eval (GenValue b w i)
|
||||
evalSel val sel = case sel of
|
||||
|
||||
TupleSel n _ -> tupleSel n val
|
||||
@ -447,15 +451,15 @@ evalSel val sel = case sel of
|
||||
-- | Evaluation environments for list comprehensions: Each variable
|
||||
-- name is bound to a list of values, one for each element in the list
|
||||
-- comprehension.
|
||||
data ListEnv b w = ListEnv
|
||||
{ leVars :: !(Map.Map Name (Integer -> Eval (GenValue b w)))
|
||||
data ListEnv b w i = ListEnv
|
||||
{ leVars :: !(Map.Map Name (Integer -> Eval (GenValue b w i)))
|
||||
-- ^ Bindings whose values vary by position
|
||||
, leStatic :: !(Map.Map Name (Eval (GenValue b w)))
|
||||
, leStatic :: !(Map.Map Name (Eval (GenValue b w i)))
|
||||
-- ^ Bindings whose values are constant
|
||||
, leTypes :: !TypeEnv
|
||||
}
|
||||
|
||||
instance Monoid (ListEnv b w) where
|
||||
instance Monoid (ListEnv b w i) where
|
||||
mempty = ListEnv
|
||||
{ leVars = Map.empty
|
||||
, leStatic = Map.empty
|
||||
@ -468,7 +472,7 @@ instance Monoid (ListEnv b w) where
|
||||
, leTypes = Map.union (leTypes l) (leTypes r)
|
||||
}
|
||||
|
||||
toListEnv :: GenEvalEnv b w -> ListEnv b w
|
||||
toListEnv :: GenEvalEnv b w i -> ListEnv b w i
|
||||
toListEnv e =
|
||||
ListEnv
|
||||
{ leVars = mempty
|
||||
@ -479,7 +483,7 @@ toListEnv e =
|
||||
-- | Evaluate a list environment at a position.
|
||||
-- This choses a particular value for the varying
|
||||
-- locations.
|
||||
evalListEnv :: ListEnv b w -> Integer -> GenEvalEnv b w
|
||||
evalListEnv :: ListEnv b w i -> Integer -> GenEvalEnv b w i
|
||||
evalListEnv (ListEnv vm st tm) i =
|
||||
let v = fmap ($i) vm
|
||||
in EvalEnv{ envVars = Map.union v st
|
||||
@ -487,21 +491,21 @@ evalListEnv (ListEnv vm st tm) i =
|
||||
}
|
||||
|
||||
bindVarList :: Name
|
||||
-> (Integer -> Eval (GenValue b w))
|
||||
-> ListEnv b w
|
||||
-> ListEnv b w
|
||||
-> (Integer -> Eval (GenValue b w i))
|
||||
-> ListEnv b w i
|
||||
-> ListEnv b w i
|
||||
bindVarList n vs lenv = lenv { leVars = Map.insert n vs (leVars lenv) }
|
||||
|
||||
-- List Comprehensions ---------------------------------------------------------
|
||||
|
||||
-- | Evaluate a comprehension.
|
||||
evalComp :: EvalPrims b w
|
||||
=> GenEvalEnv b w -- ^ Starting evaluation environment
|
||||
-> Nat' -- ^ Length of the comprehension
|
||||
-> TValue -- ^ Type of the comprehension elements
|
||||
-> Expr -- ^ Head expression of the comprehension
|
||||
-> [[Match]] -- ^ List of parallel comprehension branches
|
||||
-> Eval (GenValue b w)
|
||||
evalComp :: EvalPrims b w i
|
||||
=> GenEvalEnv b w i -- ^ Starting evaluation environment
|
||||
-> Nat' -- ^ Length of the comprehension
|
||||
-> TValue -- ^ Type of the comprehension elements
|
||||
-> Expr -- ^ Head expression of the comprehension
|
||||
-> [[Match]] -- ^ List of parallel comprehension branches
|
||||
-> Eval (GenValue b w i)
|
||||
evalComp env len elty body ms =
|
||||
do lenv <- mconcat <$> mapM (branchEnvs (toListEnv env)) ms
|
||||
mkSeq len elty <$> memoMap (IndexSeqMap $ \i -> do
|
||||
@ -509,17 +513,17 @@ evalComp env len elty body ms =
|
||||
|
||||
-- | Turn a list of matches into the final environments for each iteration of
|
||||
-- the branch.
|
||||
branchEnvs :: EvalPrims b w
|
||||
=> ListEnv b w
|
||||
branchEnvs :: EvalPrims b w i
|
||||
=> ListEnv b w i
|
||||
-> [Match]
|
||||
-> Eval (ListEnv b w)
|
||||
-> Eval (ListEnv b w i)
|
||||
branchEnvs env matches = foldM evalMatch env matches
|
||||
|
||||
-- | Turn a match into the list of environments it represents.
|
||||
evalMatch :: EvalPrims b w
|
||||
=> ListEnv b w
|
||||
evalMatch :: EvalPrims b w i
|
||||
=> ListEnv b w i
|
||||
-> Match
|
||||
-> Eval (ListEnv b w)
|
||||
-> Eval (ListEnv b w i)
|
||||
evalMatch lenv m = case m of
|
||||
|
||||
-- many envs
|
||||
|
||||
@ -33,12 +33,12 @@ import Prelude.Compat
|
||||
|
||||
-- Evaluation Environment ------------------------------------------------------
|
||||
|
||||
data GenEvalEnv b w = EvalEnv
|
||||
{ envVars :: !(Map.Map Name (Eval (GenValue b w)))
|
||||
data GenEvalEnv b w i = EvalEnv
|
||||
{ envVars :: !(Map.Map Name (Eval (GenValue b w i)))
|
||||
, envTypes :: !TypeEnv
|
||||
} deriving (Generic, NFData)
|
||||
|
||||
instance Monoid (GenEvalEnv b w) where
|
||||
instance Monoid (GenEvalEnv b w i) where
|
||||
mempty = EvalEnv
|
||||
{ envVars = Map.empty
|
||||
, envTypes = Map.empty
|
||||
@ -49,21 +49,21 @@ instance Monoid (GenEvalEnv b w) where
|
||||
, envTypes = Map.union (envTypes l) (envTypes r)
|
||||
}
|
||||
|
||||
ppEnv :: BitWord b w => PPOpts -> GenEvalEnv b w -> Eval Doc
|
||||
ppEnv :: BitWord b w i => PPOpts -> GenEvalEnv b w i -> Eval Doc
|
||||
ppEnv opts env = brackets . fsep <$> mapM bind (Map.toList (envVars env))
|
||||
where
|
||||
bind (k,v) = do vdoc <- ppValue opts =<< v
|
||||
return (pp k <+> text "->" <+> vdoc)
|
||||
|
||||
-- | Evaluation environment with no bindings
|
||||
emptyEnv :: GenEvalEnv b w
|
||||
emptyEnv :: GenEvalEnv b w i
|
||||
emptyEnv = mempty
|
||||
|
||||
-- | Bind a variable in the evaluation environment.
|
||||
bindVar :: Name
|
||||
-> Eval (GenValue b w)
|
||||
-> GenEvalEnv b w
|
||||
-> Eval (GenEvalEnv b w)
|
||||
-> Eval (GenValue b w i)
|
||||
-> GenEvalEnv b w i
|
||||
-> Eval (GenEvalEnv b w i)
|
||||
bindVar n val env = do
|
||||
let nm = show $ ppLocName n
|
||||
val' <- delay (Just nm) val
|
||||
@ -72,24 +72,24 @@ bindVar n val env = do
|
||||
-- | Bind a variable to a value in the evaluation environment, without
|
||||
-- creating a thunk.
|
||||
bindVarDirect :: Name
|
||||
-> GenValue b w
|
||||
-> GenEvalEnv b w
|
||||
-> Eval (GenEvalEnv b w)
|
||||
-> GenValue b w i
|
||||
-> GenEvalEnv b w i
|
||||
-> Eval (GenEvalEnv b w i)
|
||||
bindVarDirect n val env = do
|
||||
return $ env{ envVars = Map.insert n (ready val) (envVars env) }
|
||||
|
||||
-- | Lookup a variable in the environment.
|
||||
{-# INLINE lookupVar #-}
|
||||
lookupVar :: Name -> GenEvalEnv b w -> Maybe (Eval (GenValue b w))
|
||||
lookupVar :: Name -> GenEvalEnv b w i -> Maybe (Eval (GenValue b w i))
|
||||
lookupVar n env = Map.lookup n (envVars env)
|
||||
|
||||
-- | Bind a type variable of kind *.
|
||||
{-# INLINE bindType #-}
|
||||
bindType :: TVar -> Either Nat' TValue -> GenEvalEnv b w -> GenEvalEnv b w
|
||||
bindType :: TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
|
||||
bindType p ty env = env { envTypes = Map.insert p ty (envTypes env) }
|
||||
|
||||
-- | Lookup a type variable.
|
||||
{-# INLINE lookupType #-}
|
||||
lookupType :: TVar -> GenEvalEnv b w -> Maybe (Either Nat' TValue)
|
||||
lookupType :: TVar -> GenEvalEnv b w i -> Maybe (Either Nat' TValue)
|
||||
lookupType p env = Map.lookup p (envTypes env)
|
||||
|
||||
|
||||
@ -24,6 +24,7 @@ module Cryptol.Eval.Monad
|
||||
, evalPanic
|
||||
, typeCannotBeDemoted
|
||||
, divideByZero
|
||||
, negativeExponent
|
||||
, wordTooWide
|
||||
, cryUserError
|
||||
, cryLoopError
|
||||
@ -166,6 +167,7 @@ data EvalError
|
||||
= InvalidIndex Integer -- ^ Out-of-bounds index
|
||||
| TypeCannotBeDemoted Type -- ^ Non-numeric type passed to demote function
|
||||
| DivideByZero -- ^ Division or modulus by 0
|
||||
| NegativeExponent -- ^ Exponentiation by negative integer
|
||||
| WordTooWide Integer -- ^ Bitvector too large
|
||||
| UserError String -- ^ Call to the Cryptol @error@ primitive
|
||||
| LoopError String -- ^ Detectable nontermination
|
||||
@ -176,6 +178,7 @@ instance PP EvalError where
|
||||
InvalidIndex i -> text "invalid sequence index:" <+> integer i
|
||||
TypeCannotBeDemoted t -> text "type cannot be demoted:" <+> pp t
|
||||
DivideByZero -> text "division by 0"
|
||||
NegativeExponent -> text "negative exponent"
|
||||
WordTooWide w ->
|
||||
text "word too wide for memory:" <+> integer w <+> text "bits"
|
||||
UserError x -> text "Run-time error:" <+> text x
|
||||
@ -191,6 +194,10 @@ typeCannotBeDemoted t = X.throw (TypeCannotBeDemoted t)
|
||||
divideByZero :: Eval a
|
||||
divideByZero = Thunk (X.throwIO DivideByZero)
|
||||
|
||||
-- | For exponentiation by a negative integer.
|
||||
negativeExponent :: Eval a
|
||||
negativeExponent = Thunk (X.throwIO NegativeExponent)
|
||||
|
||||
-- | For when we know that a word is too wide and will exceed gmp's
|
||||
-- limits (though words approaching this size will probably cause the
|
||||
-- system to crash anyway due to lack of memory).
|
||||
|
||||
@ -110,6 +110,7 @@ terms by providing an evaluator to an appropriate `Value` type.
|
||||
> -- | Value type for the reference evaluator.
|
||||
> data Value
|
||||
> = VBit (Either EvalError Bool) -- ^ @ Bit @ booleans
|
||||
> | VInteger (Either EvalError Integer) -- ^ @ Integer @ integers
|
||||
> | VList [Value] -- ^ @ [n]a @ finite or infinite lists
|
||||
> | VTuple [Value] -- ^ @ ( .. ) @ tuples
|
||||
> | VRecord [(Ident, Value)] -- ^ @ { .. } @ records
|
||||
@ -118,13 +119,13 @@ terms by providing an evaluator to an appropriate `Value` type.
|
||||
> | VNumPoly (Nat' -> Value) -- ^ polymorphic values (kind #)
|
||||
|
||||
Invariant: Undefinedness and run-time exceptions are only allowed
|
||||
inside the argument of a `VBit` constructor. All other `Value` and
|
||||
list constructors should evaluate without error. For example, a
|
||||
non-terminating computation at type `(Bit,Bit)` must be represented as
|
||||
`VTuple [VBit undefined, VBit undefined]`, and not simply as
|
||||
`undefined`. Similarly, an expression like `1/0:[2]` that raises a
|
||||
run-time error must be encoded as `VList [VBit (Left e), VBit (Left
|
||||
e)]` where `e = DivideByZero`.
|
||||
inside the argument of a `VBit` or `VInteger` constructor. All other
|
||||
`Value` and list constructors should evaluate without error. For
|
||||
example, a non-terminating computation at type `(Bit,Bit)` must be
|
||||
represented as `VTuple [VBit undefined, VBit undefined]`, and not
|
||||
simply as `undefined`. Similarly, an expression like `1/0:[2]` that
|
||||
raises a run-time error must be encoded as `VList [VBit (Left e), VBit
|
||||
(Left e)]` where `e = DivideByZero`.
|
||||
|
||||
Copy Functions
|
||||
--------------
|
||||
@ -161,6 +162,7 @@ cpo that represents any given schema.
|
||||
> go ty val =
|
||||
> case ty of
|
||||
> TVBit -> VBit (fromVBit val)
|
||||
> TVInteger -> VInteger (fromVInteger val)
|
||||
> TVSeq w ety -> VList (map (go ety) (copyList w (fromVList val)))
|
||||
> TVStream ety -> VList (map (go ety) (copyStream (fromVList val)))
|
||||
> TVTuple etys -> VTuple (zipWith go etys (copyList (genericLength etys) (fromVTuple val)))
|
||||
@ -182,6 +184,11 @@ Operations on Values
|
||||
> fromVBit (VBit b) = b
|
||||
> fromVBit _ = evalPanic "fromVBit" ["Expected a bit"]
|
||||
>
|
||||
> -- | Destructor for @VInteger@.
|
||||
> fromVInteger :: Value -> Either EvalError Integer
|
||||
> fromVInteger (VInteger i) = i
|
||||
> fromVInteger _ = evalPanic "fromVInteger" ["Expected an integer"]
|
||||
>
|
||||
> -- | Destructor for @VList@.
|
||||
> fromVList :: Value -> [Value]
|
||||
> fromVList (VList vs) = vs
|
||||
@ -351,6 +358,7 @@ down to the individual bits.
|
||||
> condValue c l r =
|
||||
> case l of
|
||||
> VBit b -> VBit (condBit c b (fromVBit r))
|
||||
> VInteger i -> VInteger (condBit c i (fromVInteger r))
|
||||
> VList vs -> VList (zipWith (condValue c) vs (fromVList r))
|
||||
> VTuple vs -> VTuple (zipWith (condValue c) vs (fromVTuple r))
|
||||
> VRecord fs -> VRecord [ (f, condValue c v (lookupRecord f r)) | (f, v) <- fs ]
|
||||
@ -361,7 +369,7 @@ down to the individual bits.
|
||||
Conditionals are explicitly lazy: Run-time errors in an untaken branch
|
||||
are ignored.
|
||||
|
||||
> condBit :: Either e Bool -> Either e Bool -> Either e Bool -> Either e Bool
|
||||
> condBit :: Either e Bool -> Either e a -> Either e a -> Either e a
|
||||
> condBit (Left e) _ _ = Left e
|
||||
> condBit (Right b) x y = if b then x else y
|
||||
|
||||
@ -503,17 +511,25 @@ Cryptol primitives fall into several groups:
|
||||
> , ("False" , VBit (Right False))
|
||||
>
|
||||
> -- Arithmetic:
|
||||
> , ("+" , binary (arithBinary (\_ x y -> Right (x + y))))
|
||||
> , ("-" , binary (arithBinary (\_ x y -> Right (x - y))))
|
||||
> , ("*" , binary (arithBinary (\_ x y -> Right (x * y))))
|
||||
> , ("/" , binary (arithBinary (const divWrap)))
|
||||
> , ("%" , binary (arithBinary (const modWrap)))
|
||||
> , ("^^" , binary (arithBinary (\_ x y -> Right (x ^ y))))
|
||||
> , ("lg2" , unary (arithUnary (const lg2)))
|
||||
> , ("negate" , unary (arithUnary (const negate)))
|
||||
> , ("+" , binary (arithBinary (\x y -> Right (x + y))))
|
||||
> , ("-" , binary (arithBinary (\x y -> Right (x - y))))
|
||||
> , ("*" , binary (arithBinary (\x y -> Right (x * y))))
|
||||
> , ("/" , binary (arithBinary divWrap))
|
||||
> , ("%" , binary (arithBinary modWrap))
|
||||
> , ("^^" , binary (arithBinary expWrap))
|
||||
> , ("lg2" , unary (arithUnary lg2))
|
||||
> , ("negate" , unary (arithUnary negate))
|
||||
> , ("demote" , vFinPoly $ \val ->
|
||||
> vFinPoly $ \bits ->
|
||||
> vWordValue bits val)
|
||||
> , ("integer" , vFinPoly $ \val ->
|
||||
> VInteger (Right val))
|
||||
> , ("toInteger" , vFinPoly $ \_bits ->
|
||||
> VFun $ \x ->
|
||||
> VInteger (fromVWord x))
|
||||
> , ("fromInteger", vFinPoly $ \bits ->
|
||||
> VFun $ \x ->
|
||||
> vWord bits (fromVInteger x))
|
||||
>
|
||||
> -- Comparison:
|
||||
> , ("<" , binary (cmpOrder (\o -> o == LT)))
|
||||
@ -741,6 +757,7 @@ at the same positions.
|
||||
> logicNullary b = go
|
||||
> where
|
||||
> go TVBit = VBit b
|
||||
> go TVInteger = VInteger (fmap (\c -> if c then -1 else 0) b)
|
||||
> go (TVSeq n ety) = VList (genericReplicate n (go ety))
|
||||
> go (TVStream ety) = VList (repeat (go ety))
|
||||
> go (TVTuple tys) = VTuple (map go tys)
|
||||
@ -754,6 +771,7 @@ at the same positions.
|
||||
> go ty val =
|
||||
> case ty of
|
||||
> TVBit -> VBit (fmap op (fromVBit val))
|
||||
> TVInteger -> VInteger (Left (UserError "FIXME: logicBinary Integer"))
|
||||
> TVSeq _w ety -> VList (map (go ety) (fromVList val))
|
||||
> TVStream ety -> VList (map (go ety) (fromVList val))
|
||||
> TVTuple etys -> VTuple (zipWith go etys (fromVTuple val))
|
||||
@ -767,6 +785,7 @@ at the same positions.
|
||||
> go ty l r =
|
||||
> case ty of
|
||||
> TVBit -> VBit (liftA2 op (fromVBit l) (fromVBit r))
|
||||
> TVInteger -> VInteger (Left (UserError "FIXME: logicBinary Integer"))
|
||||
> TVSeq _w ety -> VList (zipWith (go ety) (fromVList l) (fromVList r))
|
||||
> TVStream ety -> VList (zipWith (go ety) (fromVList l) (fromVList r))
|
||||
> TVTuple etys -> VTuple (zipWith3 go etys (fromVTuple l) (fromVTuple r))
|
||||
@ -784,7 +803,7 @@ all input bits, as indicated by the definition of `fromVWord`. For
|
||||
example, `[error "foo", True] * 2` does not evaluate to `[True,
|
||||
False]`, but to `[error "foo", error "foo"]`.
|
||||
|
||||
> arithUnary :: (Integer -> Integer -> Integer)
|
||||
> arithUnary :: (Integer -> Integer)
|
||||
> -> TValue -> Value -> Value
|
||||
> arithUnary op = go
|
||||
> where
|
||||
@ -793,8 +812,10 @@ False]`, but to `[error "foo", error "foo"]`.
|
||||
> case ty of
|
||||
> TVBit ->
|
||||
> evalPanic "arithUnary" ["Bit not in class Arith"]
|
||||
> TVInteger ->
|
||||
> VInteger (op <$> fromVInteger val)
|
||||
> TVSeq w a
|
||||
> | isTBit a -> vWord w (op w <$> fromVWord val)
|
||||
> | isTBit a -> vWord w (op <$> fromVWord val)
|
||||
> | otherwise -> VList (map (go a) (fromVList val))
|
||||
> TVStream a ->
|
||||
> VList (map (go a) (fromVList val))
|
||||
@ -805,7 +826,7 @@ False]`, but to `[error "foo", error "foo"]`.
|
||||
> TVRec fs ->
|
||||
> VRecord [ (f, go fty (lookupRecord f val)) | (f, fty) <- fs ]
|
||||
>
|
||||
> arithBinary :: (Integer -> Integer -> Integer -> Either EvalError Integer)
|
||||
> arithBinary :: (Integer -> Integer -> Either EvalError Integer)
|
||||
> -> TValue -> Value -> Value -> Value
|
||||
> arithBinary op = go
|
||||
> where
|
||||
@ -814,6 +835,14 @@ False]`, but to `[error "foo", error "foo"]`.
|
||||
> case ty of
|
||||
> TVBit ->
|
||||
> evalPanic "arithBinary" ["Bit not in class Arith"]
|
||||
> TVInteger ->
|
||||
> VInteger $
|
||||
> case fromVInteger l of
|
||||
> Left e -> Left e
|
||||
> Right i ->
|
||||
> case fromVInteger r of
|
||||
> Left e -> Left e
|
||||
> Right j -> op i j
|
||||
> TVSeq w a
|
||||
> | isTBit a -> vWord w $
|
||||
> case fromVWord l of
|
||||
@ -821,7 +850,7 @@ False]`, but to `[error "foo", error "foo"]`.
|
||||
> Right i ->
|
||||
> case fromVWord r of
|
||||
> Left e -> Left e
|
||||
> Right j -> op w i j
|
||||
> Right j -> op i j
|
||||
> | otherwise -> VList (zipWith (go a) (fromVList l) (fromVList r))
|
||||
> TVStream a ->
|
||||
> VList (zipWith (go a) (fromVList l) (fromVList r))
|
||||
@ -839,6 +868,9 @@ False]`, but to `[error "foo", error "foo"]`.
|
||||
> modWrap :: Integer -> Integer -> Either EvalError Integer
|
||||
> modWrap _ 0 = Left DivideByZero
|
||||
> modWrap x y = Right (x `mod` y)
|
||||
>
|
||||
> expWrap :: Integer -> Integer -> Either EvalError Integer
|
||||
> expWrap x y = if y < 0 then Left NegativeExponent else Right (x ^ y)
|
||||
|
||||
|
||||
Comparison
|
||||
@ -865,6 +897,8 @@ bits to the *left* of that position are equal.
|
||||
> case ty of
|
||||
> TVBit ->
|
||||
> compare <$> fromVBit l <*> fromVBit r
|
||||
> TVInteger ->
|
||||
> compare <$> fromVInteger l <*> fromVInteger r
|
||||
> TVSeq _w ety ->
|
||||
> lexList (zipWith (lexCompare ety) (fromVList l) (fromVList r))
|
||||
> TVStream _ ->
|
||||
@ -1068,6 +1102,7 @@ Pretty Printing
|
||||
> ppValue val =
|
||||
> case val of
|
||||
> VBit b -> text (either show show b)
|
||||
> VInteger i -> text (either show show i)
|
||||
> VList vs -> brackets (fsep (punctuate comma (map ppValue vs)))
|
||||
> VTuple vs -> parens (sep (punctuate comma (map ppValue vs)))
|
||||
> VRecord fs -> braces (sep (punctuate comma (map ppField fs)))
|
||||
|
||||
@ -28,6 +28,7 @@ import Control.DeepSeq
|
||||
-- These types do not contain type variables, type synonyms, or type functions.
|
||||
data TValue
|
||||
= TVBit -- ^ @ Bit @
|
||||
| TVInteger -- ^ @ Integer @
|
||||
| TVSeq Integer TValue -- ^ @ [n]a @
|
||||
| TVStream TValue -- ^ @ [inf]t @
|
||||
| TVTuple [TValue] -- ^ @ (a, b, c )@
|
||||
@ -40,6 +41,7 @@ tValTy :: TValue -> Type
|
||||
tValTy tv =
|
||||
case tv of
|
||||
TVBit -> tBit
|
||||
TVInteger -> tInteger
|
||||
TVSeq n t -> tSeq (tNum n) (tValTy t)
|
||||
TVStream t -> tSeq tInf (tValTy t)
|
||||
TVTuple ts -> tTuple (map tValTy ts)
|
||||
@ -90,6 +92,7 @@ evalType env ty =
|
||||
TCon (TC c) ts ->
|
||||
case (c, ts) of
|
||||
(TCBit, []) -> Right $ TVBit
|
||||
(TCInteger, []) -> Right $ TVInteger
|
||||
(TCSeq, [n, t]) -> Right $ tvSeq (num n) (val t)
|
||||
(TCFun, [a, b]) -> Right $ TVFun (val a) (val b)
|
||||
(TCTuple _, _) -> Right $ TVTuple (map val ts)
|
||||
|
||||
@ -25,6 +25,7 @@ module Cryptol.Eval.Value where
|
||||
import Data.Bits
|
||||
import Data.IORef
|
||||
import qualified Data.Sequence as Seq
|
||||
import qualified Data.Foldable as Fold
|
||||
import Data.Map.Strict (Map)
|
||||
import qualified Data.Map.Strict as Map
|
||||
import MonadLib
|
||||
@ -74,58 +75,58 @@ mkBv w i = BV w (mask w i)
|
||||
|
||||
-- | A sequence map represents a mapping from nonnegative integer indices
|
||||
-- to values. These are used to represent both finite and infinite sequences.
|
||||
data SeqMap b w
|
||||
= IndexSeqMap !(Integer -> Eval (GenValue b w))
|
||||
| UpdateSeqMap !(Map Integer (Eval (GenValue b w)))
|
||||
!(Integer -> Eval (GenValue b w))
|
||||
data SeqMap b w i
|
||||
= IndexSeqMap !(Integer -> Eval (GenValue b w i))
|
||||
| UpdateSeqMap !(Map Integer (Eval (GenValue b w i)))
|
||||
!(Integer -> Eval (GenValue b w i))
|
||||
|
||||
lookupSeqMap :: SeqMap b w -> Integer -> Eval (GenValue b w)
|
||||
lookupSeqMap :: SeqMap b w i -> Integer -> Eval (GenValue b w i)
|
||||
lookupSeqMap (IndexSeqMap f) i = f i
|
||||
lookupSeqMap (UpdateSeqMap m f) i =
|
||||
case Map.lookup i m of
|
||||
Just x -> x
|
||||
Nothing -> f i
|
||||
|
||||
type SeqValMap = SeqMap Bool BV
|
||||
type SeqValMap = SeqMap Bool BV Integer
|
||||
|
||||
instance NFData (SeqMap b w) where
|
||||
instance NFData (SeqMap b w i) where
|
||||
rnf x = seq x ()
|
||||
|
||||
-- | Generate a finite sequence map from a list of values
|
||||
finiteSeqMap :: [Eval (GenValue b w)] -> SeqMap b w
|
||||
finiteSeqMap :: [Eval (GenValue b w i)] -> SeqMap b w i
|
||||
finiteSeqMap xs =
|
||||
UpdateSeqMap
|
||||
(Map.fromList (zip [0..] xs))
|
||||
invalidIndex
|
||||
|
||||
-- | Generate an infinite sequence map from a stream of values
|
||||
infiniteSeqMap :: [Eval (GenValue b w)] -> Eval (SeqMap b w)
|
||||
infiniteSeqMap :: [Eval (GenValue b w i)] -> Eval (SeqMap b w i)
|
||||
infiniteSeqMap xs =
|
||||
-- TODO: use an int-trie?
|
||||
memoMap (IndexSeqMap $ \i -> genericIndex xs i)
|
||||
|
||||
-- | Create a finite list of length `n` of the values from [0..n-1] in
|
||||
-- the given the sequence emap.
|
||||
enumerateSeqMap :: (Integral n) => n -> SeqMap b w -> [Eval (GenValue b w)]
|
||||
enumerateSeqMap :: (Integral n) => n -> SeqMap b w i -> [Eval (GenValue b w i)]
|
||||
enumerateSeqMap n m = [ lookupSeqMap m i | i <- [0 .. (toInteger n)-1] ]
|
||||
|
||||
-- | Create an infinite stream of all the values in a sequence map
|
||||
streamSeqMap :: SeqMap b w -> [Eval (GenValue b w)]
|
||||
streamSeqMap :: SeqMap b w i -> [Eval (GenValue b w i)]
|
||||
streamSeqMap m = [ lookupSeqMap m i | i <- [0..] ]
|
||||
|
||||
-- | Reverse the order of a finite sequence map
|
||||
reverseSeqMap :: Integer -- ^ Size of the sequence map
|
||||
-> SeqMap b w
|
||||
-> SeqMap b w
|
||||
-> SeqMap b w i
|
||||
-> SeqMap b w i
|
||||
reverseSeqMap n vals = IndexSeqMap $ \i -> lookupSeqMap vals (n - 1 - i)
|
||||
|
||||
updateSeqMap :: SeqMap b w -> Integer -> Eval (GenValue b w) -> SeqMap b w
|
||||
updateSeqMap :: SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i
|
||||
updateSeqMap (UpdateSeqMap m sm) i x = UpdateSeqMap (Map.insert i x m) sm
|
||||
updateSeqMap (IndexSeqMap f) i x = UpdateSeqMap (Map.singleton i x) f
|
||||
|
||||
-- | Concatenate the first `n` values of the first sequence map onto the
|
||||
-- beginning of the second sequence map.
|
||||
concatSeqMap :: Integer -> SeqMap b w -> SeqMap b w -> SeqMap b w
|
||||
concatSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i -> SeqMap b w i
|
||||
concatSeqMap n x y =
|
||||
IndexSeqMap $ \i ->
|
||||
if i < n
|
||||
@ -135,20 +136,20 @@ concatSeqMap n x y =
|
||||
-- | Given a number `n` and a sequence map, return two new sequence maps:
|
||||
-- the first containing the values from `[0..n-1]` and the next containing
|
||||
-- the values from `n` onward.
|
||||
splitSeqMap :: Integer -> SeqMap b w -> (SeqMap b w, SeqMap b w)
|
||||
splitSeqMap :: Integer -> SeqMap b w i -> (SeqMap b w i, SeqMap b w i)
|
||||
splitSeqMap n xs = (hd,tl)
|
||||
where
|
||||
hd = xs
|
||||
tl = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)
|
||||
|
||||
-- | Drop the first @n@ elements of the given @SeqMap@.
|
||||
dropSeqMap :: Integer -> SeqMap b w -> SeqMap b w
|
||||
dropSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i
|
||||
dropSeqMap 0 xs = xs
|
||||
dropSeqMap n xs = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)
|
||||
|
||||
-- | Given a sequence map, return a new sequence map that is memoized using
|
||||
-- a finite map memo table.
|
||||
memoMap :: SeqMap b w -> Eval (SeqMap b w)
|
||||
memoMap :: SeqMap b w i -> Eval (SeqMap b w i)
|
||||
memoMap x = do
|
||||
cache <- io $ newIORef $ Map.empty
|
||||
return $ IndexSeqMap (memo cache)
|
||||
@ -167,16 +168,16 @@ memoMap x = do
|
||||
|
||||
-- | Apply the given evaluation function pointwise to the two given
|
||||
-- sequence maps.
|
||||
zipSeqMap :: (GenValue b w -> GenValue b w -> Eval (GenValue b w))
|
||||
-> SeqMap b w
|
||||
-> SeqMap b w
|
||||
-> Eval (SeqMap b w)
|
||||
zipSeqMap :: (GenValue b w i -> GenValue b w i -> Eval (GenValue b w i))
|
||||
-> SeqMap b w i
|
||||
-> SeqMap b w i
|
||||
-> Eval (SeqMap b w i)
|
||||
zipSeqMap f x y =
|
||||
memoMap (IndexSeqMap $ \i -> join (f <$> lookupSeqMap x i <*> lookupSeqMap y i))
|
||||
|
||||
-- | Apply the given function to each value in the given sequence map
|
||||
mapSeqMap :: (GenValue b w -> Eval (GenValue b w))
|
||||
-> SeqMap b w -> Eval (SeqMap b w)
|
||||
mapSeqMap :: (GenValue b w i -> Eval (GenValue b w i))
|
||||
-> SeqMap b w i -> Eval (SeqMap b w i)
|
||||
mapSeqMap f x =
|
||||
memoMap (IndexSeqMap $ \i -> f =<< lookupSeqMap x i)
|
||||
|
||||
@ -189,10 +190,11 @@ mapSeqMap f x =
|
||||
-- However, if we cannot be sure all the bits of the sequence
|
||||
-- will eventually be forced, we must instead rely on an explicit sequence of bits
|
||||
-- representation.
|
||||
data WordValue b w
|
||||
= WordVal !w -- ^ Packed word representation for bit sequences.
|
||||
| BitsVal !Integer !(SeqMap b w) -- ^ A bitvector sequence, represented as a
|
||||
-- @SeqMap@ of bits.
|
||||
data WordValue b w i
|
||||
= WordVal !w -- ^ Packed word representation for bit sequences.
|
||||
| BitsVal !(Seq.Seq (Eval b)) -- ^ Sequence of thunks representing bits.
|
||||
| LargeBitsVal !Integer !(SeqMap b w i ) -- ^ A large bitvector sequence, represented as a
|
||||
-- @SeqMap@ of bits.
|
||||
deriving (Generic, NFData)
|
||||
|
||||
-- | An arbitrarily-chosen number of elements where we switch from a dense
|
||||
@ -201,31 +203,36 @@ largeBitSize :: Integer
|
||||
largeBitSize = 1 `shiftL` 16
|
||||
|
||||
-- | Force a word value into packed word form
|
||||
asWordVal :: BitWord b w => WordValue b w -> Eval w
|
||||
asWordVal (WordVal w) = return w
|
||||
asWordVal (BitsVal n xs) = packWord <$> traverse (fromBit =<<) (enumerateSeqMap n xs)
|
||||
asWordVal :: BitWord b w i => WordValue b w i -> Eval w
|
||||
asWordVal (WordVal w) = return w
|
||||
asWordVal (BitsVal bs) = packWord <$> sequence (Fold.toList bs)
|
||||
asWordVal (LargeBitsVal n xs) = packWord <$> traverse (fromBit =<<) (enumerateSeqMap n xs)
|
||||
|
||||
-- | Force a word value into a sequence of bits
|
||||
asBitsMap :: BitWord b w => WordValue b w -> SeqMap b w
|
||||
asBitsMap (WordVal w) = IndexSeqMap $ \i -> ready $ VBit $ wordBit w i
|
||||
asBitsMap (BitsVal _ xs) = xs
|
||||
asBitsMap :: BitWord b w i => WordValue b w i -> SeqMap b w i
|
||||
asBitsMap (WordVal w) = IndexSeqMap $ \i -> ready $ VBit $ wordBit w i
|
||||
asBitsMap (BitsVal bs) = IndexSeqMap $ \i -> VBit <$> join (checkedSeqIndex bs i)
|
||||
asBitsMap (LargeBitsVal _ xs) = xs
|
||||
|
||||
-- | Turn a word value into a sequence of bits, forcing each bit.
|
||||
-- The sequence is returned in big-endian order.
|
||||
enumerateWordValue :: BitWord b w => WordValue b w -> Eval [b]
|
||||
enumerateWordValue (WordVal w) = return $ unpackWord w
|
||||
enumerateWordValue (BitsVal n xs) = traverse (fromBit =<<) (enumerateSeqMap n xs)
|
||||
enumerateWordValue :: BitWord b w i => WordValue b w i -> Eval [b]
|
||||
enumerateWordValue (WordVal w) = return $ unpackWord w
|
||||
enumerateWordValue (BitsVal bs) = sequence (Fold.toList bs)
|
||||
enumerateWordValue (LargeBitsVal n xs) = traverse (fromBit =<<) (enumerateSeqMap n xs)
|
||||
|
||||
-- | Turn a word value into a sequence of bits, forcing each bit.
|
||||
-- The sequence is returned in reverse of the usual order, which is little-endian order.
|
||||
enumerateWordValueRev :: BitWord b w => WordValue b w -> Eval [b]
|
||||
enumerateWordValueRev (WordVal w) = return $ reverse $ unpackWord w
|
||||
enumerateWordValueRev (BitsVal n xs) = traverse (fromBit =<<) (enumerateSeqMap n (reverseSeqMap n xs))
|
||||
enumerateWordValueRev :: BitWord b w i => WordValue b w i -> Eval [b]
|
||||
enumerateWordValueRev (WordVal w) = return $ reverse $ unpackWord w
|
||||
enumerateWordValueRev (BitsVal bs) = sequence (Fold.toList $ Seq.reverse bs)
|
||||
enumerateWordValueRev (LargeBitsVal n xs) = traverse (fromBit =<<) (enumerateSeqMap n (reverseSeqMap n xs))
|
||||
|
||||
-- | Compute the size of a word value
|
||||
wordValueSize :: BitWord b w => WordValue b w -> Integer
|
||||
wordValueSize (WordVal w) = wordLen w
|
||||
wordValueSize (BitsVal n _) = n
|
||||
wordValueSize :: BitWord b w i => WordValue b w i -> Integer
|
||||
wordValueSize (WordVal w) = wordLen w
|
||||
wordValueSize (BitsVal bs) = toInteger $ Seq.length bs
|
||||
wordValueSize (LargeBitsVal n _) = n
|
||||
|
||||
checkedSeqIndex :: Seq.Seq a -> Integer -> Eval a
|
||||
checkedSeqIndex xs i =
|
||||
@ -240,27 +247,29 @@ checkedIndex xs i =
|
||||
_ -> invalidIndex i
|
||||
|
||||
-- | Select an individual bit from a word value
|
||||
indexWordValue :: BitWord b w => WordValue b w -> Integer -> Eval b
|
||||
indexWordValue :: BitWord b w i => WordValue b w i -> Integer -> Eval b
|
||||
indexWordValue (WordVal w) idx
|
||||
| idx < wordLen w = return $ wordBit w idx
|
||||
| otherwise = invalidIndex idx
|
||||
indexWordValue (BitsVal n xs) idx
|
||||
indexWordValue (BitsVal bs) idx = join (checkedSeqIndex bs idx)
|
||||
indexWordValue (LargeBitsVal n xs) idx
|
||||
| idx < n = fromBit =<< lookupSeqMap xs idx
|
||||
| otherwise = invalidIndex idx
|
||||
|
||||
-- | Produce a new @WordValue@ from the one given by updating the @i@th bit with the
|
||||
-- given bit value.
|
||||
updateWordValue :: BitWord b w => WordValue b w -> Integer -> Eval b -> Eval (WordValue b w)
|
||||
updateWordValue :: BitWord b w i => WordValue b w i -> Integer -> Eval b -> Eval (WordValue b w i)
|
||||
updateWordValue (WordVal w) idx (Ready b)
|
||||
| idx < wordLen w = return $ WordVal $ wordUpdate w idx b
|
||||
| otherwise = invalidIndex idx
|
||||
updateWordValue (WordVal w) idx b
|
||||
| idx < wordLen w =
|
||||
let bs = Seq.update (fromInteger idx) b $ Seq.fromList $ map ready $ unpackWord w
|
||||
in return $ BitsVal (wordLen w) $ IndexSeqMap $ \i -> VBit <$> Seq.index bs (fromInteger i)
|
||||
| idx < wordLen w = return $ BitsVal $ Seq.update (fromInteger idx) b $ Seq.fromList $ map ready $ unpackWord w
|
||||
| otherwise = invalidIndex idx
|
||||
updateWordValue (BitsVal n xs) idx b
|
||||
| idx < n = return $ BitsVal n $ updateSeqMap xs idx (VBit <$> b)
|
||||
updateWordValue (BitsVal bs) idx b
|
||||
| idx < toInteger (Seq.length bs) = return $ BitsVal $ Seq.update (fromInteger idx) b bs
|
||||
| otherwise = invalidIndex idx
|
||||
updateWordValue (LargeBitsVal n xs) idx b
|
||||
| idx < n = return $ LargeBitsVal n $ updateSeqMap xs idx (VBit <$> b)
|
||||
| otherwise = invalidIndex idx
|
||||
|
||||
-- | Generic value type, parameterized by bit and word types.
|
||||
@ -269,32 +278,35 @@ updateWordValue (BitsVal n xs) idx b
|
||||
-- `VSeq` must never be used for finite sequences of bits.
|
||||
-- Always use the `VWord` constructor instead! Infinite sequences of bits
|
||||
-- are handled by the `VStream` constructor, just as for other types.
|
||||
data GenValue b w
|
||||
= VRecord ![(Ident, Eval (GenValue b w))] -- ^ @ { .. } @
|
||||
| VTuple ![Eval (GenValue b w)] -- ^ @ ( .. ) @
|
||||
| VBit !b -- ^ @ Bit @
|
||||
| VSeq !Integer !(SeqMap b w) -- ^ @ [n]a @
|
||||
-- Invariant: VSeq is never a sequence of bits
|
||||
| VWord !Integer !(Eval (WordValue b w)) -- ^ @ [n]Bit @
|
||||
| VStream !(SeqMap b w) -- ^ @ [inf]a @
|
||||
| VFun (Eval (GenValue b w) -> Eval (GenValue b w)) -- ^ functions
|
||||
| VPoly (TValue -> Eval (GenValue b w)) -- ^ polymorphic values (kind *)
|
||||
| VNumPoly (Nat' -> Eval (GenValue b w)) -- ^ polymorphic values (kind #)
|
||||
data GenValue b w i
|
||||
= VRecord ![(Ident, Eval (GenValue b w i))] -- ^ @ { .. } @
|
||||
| VTuple ![Eval (GenValue b w i)] -- ^ @ ( .. ) @
|
||||
| VBit !b -- ^ @ Bit @
|
||||
| VInteger !i -- ^ @ Integer @
|
||||
| VSeq !Integer !(SeqMap b w i) -- ^ @ [n]a @
|
||||
-- Invariant: VSeq is never a sequence of bits
|
||||
| VWord !Integer !(Eval (WordValue b w i)) -- ^ @ [n]Bit @
|
||||
| VStream !(SeqMap b w i) -- ^ @ [inf]a @
|
||||
| VFun (Eval (GenValue b w i) -> Eval (GenValue b w i)) -- ^ functions
|
||||
| VPoly (TValue -> Eval (GenValue b w i)) -- ^ polymorphic values (kind *)
|
||||
| VNumPoly (Nat' -> Eval (GenValue b w i)) -- ^ polymorphic values (kind #)
|
||||
deriving (Generic, NFData)
|
||||
|
||||
|
||||
-- | Force the evaluation of a word value
|
||||
forceWordValue :: WordValue b w -> Eval ()
|
||||
forceWordValue (WordVal _w) = return ()
|
||||
forceWordValue (BitsVal n xs) = mapM_ (\x -> const () <$> x) (enumerateSeqMap n xs)
|
||||
forceWordValue :: WordValue b w i -> Eval ()
|
||||
forceWordValue (WordVal _w) = return ()
|
||||
forceWordValue (BitsVal bs) = mapM_ (\b -> const () <$> b) bs
|
||||
forceWordValue (LargeBitsVal n xs) = mapM_ (\x -> const () <$> x) (enumerateSeqMap n xs)
|
||||
|
||||
-- | Force the evaluation of a value
|
||||
forceValue :: GenValue b w -> Eval ()
|
||||
forceValue :: GenValue b w i -> Eval ()
|
||||
forceValue v = case v of
|
||||
VRecord fs -> mapM_ (\x -> forceValue =<< snd x) fs
|
||||
VTuple xs -> mapM_ (forceValue =<<) xs
|
||||
VSeq n xs -> mapM_ (forceValue =<<) (enumerateSeqMap n xs)
|
||||
VBit _b -> return ()
|
||||
VInteger _i -> return ()
|
||||
VWord _ wv -> forceWordValue =<< wv
|
||||
VStream _ -> return ()
|
||||
VFun _ -> return ()
|
||||
@ -302,11 +314,12 @@ forceValue v = case v of
|
||||
VNumPoly _ -> return ()
|
||||
|
||||
|
||||
instance (Show b, Show w) => Show (GenValue b w) where
|
||||
instance (Show b, Show w, Show i) => Show (GenValue b w i) where
|
||||
show v = case v of
|
||||
VRecord fs -> "record:" ++ show (map fst fs)
|
||||
VTuple xs -> "tuple:" ++ show (length xs)
|
||||
VBit b -> show b
|
||||
VInteger i -> show i
|
||||
VSeq n _ -> "seq:" ++ show n
|
||||
VWord n _ -> "word:" ++ show n
|
||||
VStream _ -> "stream"
|
||||
@ -314,7 +327,7 @@ instance (Show b, Show w) => Show (GenValue b w) where
|
||||
VPoly _ -> "poly"
|
||||
VNumPoly _ -> "numpoly"
|
||||
|
||||
type Value = GenValue Bool BV
|
||||
type Value = GenValue Bool BV Integer
|
||||
|
||||
|
||||
-- Pretty Printing -------------------------------------------------------------
|
||||
@ -334,14 +347,14 @@ atFst f (x,y) = fmap (,y) $ f x
|
||||
atSnd :: Functor f => (a -> f b) -> (c, a) -> f (c, b)
|
||||
atSnd f (x,y) = fmap (x,) $ f y
|
||||
|
||||
ppValue :: forall b w
|
||||
. BitWord b w
|
||||
ppValue :: forall b w i
|
||||
. BitWord b w i
|
||||
=> PPOpts
|
||||
-> GenValue b w
|
||||
-> GenValue b w i
|
||||
-> Eval Doc
|
||||
ppValue opts = loop
|
||||
where
|
||||
loop :: GenValue b w -> Eval Doc
|
||||
loop :: GenValue b w i -> Eval Doc
|
||||
loop val = case val of
|
||||
VRecord fs -> do fs' <- traverse (atSnd (>>=loop)) $ fs
|
||||
return $ braces (sep (punctuate comma (map ppField fs')))
|
||||
@ -350,6 +363,7 @@ ppValue opts = loop
|
||||
VTuple vals -> do vals' <- traverse (>>=loop) vals
|
||||
return $ parens (sep (punctuate comma vals'))
|
||||
VBit b -> return $ ppBit b
|
||||
VInteger i -> return $ ppInteger opts i
|
||||
VSeq sz vals -> ppWordSeq sz vals
|
||||
VWord _ wv -> ppWordVal =<< wv
|
||||
VStream vals -> do vals' <- traverse (>>=loop) $ enumerateSeqMap (useInfLength opts) vals
|
||||
@ -361,10 +375,10 @@ ppValue opts = loop
|
||||
VPoly _ -> return $ text "<polymorphic value>"
|
||||
VNumPoly _ -> return $ text "<polymorphic value>"
|
||||
|
||||
ppWordVal :: WordValue b w -> Eval Doc
|
||||
ppWordVal :: WordValue b w i -> Eval Doc
|
||||
ppWordVal w = ppWord opts <$> asWordVal w
|
||||
|
||||
ppWordSeq :: Integer -> SeqMap b w -> Eval Doc
|
||||
ppWordSeq :: Integer -> SeqMap b w i -> Eval Doc
|
||||
ppWordSeq sz vals = do
|
||||
ws <- sequence (enumerateSeqMap sz vals)
|
||||
case ws of
|
||||
@ -415,13 +429,16 @@ ppBV opts (BV width i)
|
||||
-- | This type class defines a collection of operations on bits and words that
|
||||
-- are necessary to define generic evaluator primitives that operate on both concrete
|
||||
-- and symbolic values uniformly.
|
||||
class BitWord b w | b -> w, w -> b where
|
||||
class BitWord b w i | b -> w, w -> i, i -> b where
|
||||
-- | Pretty-print an individual bit
|
||||
ppBit :: b -> Doc
|
||||
|
||||
-- | Pretty-print a word value
|
||||
ppWord :: PPOpts -> w -> Doc
|
||||
|
||||
-- | Pretty-print an integer value
|
||||
ppInteger :: PPOpts -> i -> Doc
|
||||
|
||||
-- | Attempt to render a word value as an ASCII character. Return `Nothing`
|
||||
-- if the character value is unknown (e.g., for symbolic values).
|
||||
wordAsChar :: w -> Maybe Char
|
||||
@ -437,6 +454,10 @@ class BitWord b w | b -> w, w -> b where
|
||||
-> Integer -- ^ Value
|
||||
-> w
|
||||
|
||||
-- | Construct a literal integer value from the given integer.
|
||||
integerLit :: Integer -- ^ Value
|
||||
-> i
|
||||
|
||||
-- | Extract the numbered bit from the word.
|
||||
--
|
||||
-- NOTE: this assumes that the sequence of bits is big-endian and finite, so the
|
||||
@ -499,19 +520,24 @@ class BitWord b w | b -> w, w -> b where
|
||||
-- multiplication are silently discarded.
|
||||
wordMult :: w -> w -> w
|
||||
|
||||
-- | Construct an integer value from the given packed word.
|
||||
wordToInt :: w -> i
|
||||
|
||||
-- | Construct a packed word of the specified width from an integer value.
|
||||
wordFromInt :: Integer -> i -> w
|
||||
|
||||
-- | This class defines additional operations necessary to define generic evaluation
|
||||
-- functions.
|
||||
class BitWord b w => EvalPrims b w where
|
||||
class BitWord b w i => EvalPrims b w i where
|
||||
-- | Eval prim binds primitive declarations to the primitive values that implement them.
|
||||
evalPrim :: Decl -> GenValue b w
|
||||
evalPrim :: Decl -> GenValue b w i
|
||||
|
||||
-- | if/then/else operation. Choose either the 'then' value or the 'else' value depending
|
||||
-- on the value of the test bit.
|
||||
iteValue :: b -- ^ Test bit
|
||||
-> Eval (GenValue b w) -- ^ 'then' value
|
||||
-> Eval (GenValue b w) -- ^ 'else' value
|
||||
-> Eval (GenValue b w)
|
||||
iteValue :: b -- ^ Test bit
|
||||
-> Eval (GenValue b w i) -- ^ 'then' value
|
||||
-> Eval (GenValue b w i) -- ^ 'else' value
|
||||
-> Eval (GenValue b w i)
|
||||
|
||||
|
||||
-- Concrete Big-endian Words ------------------------------------------------------------
|
||||
@ -522,7 +548,7 @@ mask :: Integer -- ^ Bit-width
|
||||
mask w i | w >= Arch.maxBigIntWidth = wordTooWide w
|
||||
| otherwise = i .&. ((1 `shiftL` fromInteger w) - 1)
|
||||
|
||||
instance BitWord Bool BV where
|
||||
instance BitWord Bool BV Integer where
|
||||
wordLen (BV w _) = w
|
||||
wordAsChar (BV _ x) = Just $ integerToChar x
|
||||
|
||||
@ -536,8 +562,11 @@ instance BitWord Bool BV where
|
||||
|
||||
ppWord = ppBV
|
||||
|
||||
ppInteger _opts i = integer i
|
||||
|
||||
bitLit b = b
|
||||
wordLit = mkBv
|
||||
integerLit i = i
|
||||
|
||||
packWord bits = BV (toInteger w) a
|
||||
where
|
||||
@ -572,35 +601,37 @@ instance BitWord Bool BV where
|
||||
| i == j = mkBv i (x*y)
|
||||
| otherwise = panic "Attempt to multiply words of different sizes: wordMult" []
|
||||
|
||||
wordToInt (BV _ x) = x
|
||||
wordFromInt w x = mkBv w x
|
||||
|
||||
-- Value Constructors ----------------------------------------------------------
|
||||
|
||||
-- | Create a packed word of n bits.
|
||||
word :: BitWord b w => Integer -> Integer -> GenValue b w
|
||||
word :: BitWord b w i => Integer -> Integer -> GenValue b w i
|
||||
word n i = VWord n $ ready $ WordVal $ wordLit n i
|
||||
|
||||
lam :: (Eval (GenValue b w) -> Eval (GenValue b w)) -> GenValue b w
|
||||
lam :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
|
||||
lam = VFun
|
||||
|
||||
-- | Functions that assume word inputs
|
||||
wlam :: BitWord b w => (w -> Eval (GenValue b w)) -> GenValue b w
|
||||
wlam :: BitWord b w i => (w -> Eval (GenValue b w i)) -> GenValue b w i
|
||||
wlam f = VFun (\x -> x >>= fromVWord "wlam" >>= f)
|
||||
|
||||
-- | A type lambda that expects a @Type@.
|
||||
tlam :: (TValue -> GenValue b w) -> GenValue b w
|
||||
tlam :: (TValue -> GenValue b w i) -> GenValue b w i
|
||||
tlam f = VPoly (return . f)
|
||||
|
||||
-- | A type lambda that expects a @Type@ of kind #.
|
||||
nlam :: (Nat' -> GenValue b w) -> GenValue b w
|
||||
nlam :: (Nat' -> GenValue b w i) -> GenValue b w i
|
||||
nlam f = VNumPoly (return . f)
|
||||
|
||||
-- | Generate a stream.
|
||||
toStream :: [GenValue b w] -> Eval (GenValue b w)
|
||||
toStream :: [GenValue b w i] -> Eval (GenValue b w i)
|
||||
toStream vs =
|
||||
VStream <$> infiniteSeqMap (map ready vs)
|
||||
|
||||
toFinSeq :: BitWord b w
|
||||
=> Integer -> TValue -> [GenValue b w] -> GenValue b w
|
||||
toFinSeq :: BitWord b w i
|
||||
=> Integer -> TValue -> [GenValue b w i] -> GenValue b w i
|
||||
toFinSeq len elty vs
|
||||
| isTBit elty = VWord len $ ready $ WordVal $ packWord $ map fromVBit vs
|
||||
| otherwise = VSeq len $ finiteSeqMap (map ready vs)
|
||||
@ -611,8 +642,8 @@ boolToWord bs = VWord (genericLength bs) $ ready $ WordVal $ packWord bs
|
||||
|
||||
-- | 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 :: BitWord b w
|
||||
=> Nat' -> TValue -> [GenValue b w] -> Eval (GenValue b w)
|
||||
toSeq :: BitWord b w i
|
||||
=> Nat' -> TValue -> [GenValue b w i] -> Eval (GenValue b w i)
|
||||
toSeq len elty vals = case len of
|
||||
Nat n -> return $ toFinSeq n elty vals
|
||||
Inf -> toStream vals
|
||||
@ -620,10 +651,11 @@ toSeq len elty vals = case len of
|
||||
|
||||
-- | Construct either a finite sequence, or a stream. In the finite case,
|
||||
-- record whether or not the elements were bits, to aid pretty-printing.
|
||||
mkSeq :: Nat' -> TValue -> SeqMap b w -> GenValue b w
|
||||
mkSeq :: Nat' -> TValue -> SeqMap b w i -> GenValue b w i
|
||||
mkSeq len elty vals = case len of
|
||||
Nat n
|
||||
| isTBit elty -> VWord n $ return $ BitsVal n vals
|
||||
| isTBit elty -> VWord n $ return $ BitsVal $ Seq.fromFunction (fromInteger n) $ \i ->
|
||||
fromVBit <$> lookupSeqMap vals (toInteger i)
|
||||
| otherwise -> VSeq n vals
|
||||
Inf -> VStream vals
|
||||
|
||||
@ -631,13 +663,19 @@ mkSeq len elty vals = case len of
|
||||
-- Value Destructors -----------------------------------------------------------
|
||||
|
||||
-- | Extract a bit value.
|
||||
fromVBit :: GenValue b w -> b
|
||||
fromVBit :: GenValue b w i -> b
|
||||
fromVBit val = case val of
|
||||
VBit b -> b
|
||||
_ -> evalPanic "fromVBit" ["not a Bit"]
|
||||
|
||||
-- | Extract an integer value.
|
||||
fromVInteger :: GenValue b w i -> i
|
||||
fromVInteger val = case val of
|
||||
VInteger i -> i
|
||||
_ -> evalPanic "fromVInteger" ["not an Integer"]
|
||||
|
||||
-- | Extract a sequence.
|
||||
fromSeq :: forall b w. BitWord b w => String -> GenValue b w -> Eval (SeqMap b w)
|
||||
fromSeq :: forall b w i. BitWord b w i => String -> GenValue b w i -> Eval (SeqMap b w i)
|
||||
fromSeq msg val = case val of
|
||||
VSeq _ vs -> return vs
|
||||
VStream vs -> return vs
|
||||
@ -648,20 +686,20 @@ fromStr (VSeq n vals) =
|
||||
traverse (\x -> toEnum . fromInteger <$> (fromWord "fromStr" =<< x)) (enumerateSeqMap n vals)
|
||||
fromStr _ = evalPanic "fromStr" ["Not a finite sequence"]
|
||||
|
||||
fromBit :: GenValue b w -> Eval b
|
||||
fromBit :: GenValue b w i -> Eval b
|
||||
fromBit (VBit b) = return b
|
||||
fromBit _ = evalPanic "fromBit" ["Not a bit value"]
|
||||
|
||||
fromWordVal :: String -> GenValue b w -> Eval (WordValue b w)
|
||||
fromWordVal :: String -> GenValue b w i -> Eval (WordValue b w i)
|
||||
fromWordVal _msg (VWord _ wval) = wval
|
||||
fromWordVal msg _ = evalPanic "fromWordVal" ["not a word value", msg]
|
||||
|
||||
-- | Extract a packed word.
|
||||
fromVWord :: BitWord b w => String -> GenValue b w -> Eval w
|
||||
fromVWord _msg (VWord _ wval) = wval >>= asWordVal
|
||||
fromVWord :: BitWord b w i => String -> GenValue b w i -> Eval w
|
||||
fromVWord _msg (VWord _ wval) = wval >>= asWordVal
|
||||
fromVWord msg _ = evalPanic "fromVWord" ["not a word", msg]
|
||||
|
||||
vWordLen :: BitWord b w => GenValue b w -> Maybe Integer
|
||||
vWordLen :: BitWord b w i => GenValue b w i -> Maybe Integer
|
||||
vWordLen val = case val of
|
||||
VWord n _wv -> Just n
|
||||
_ -> Nothing
|
||||
@ -669,7 +707,7 @@ vWordLen val = case val of
|
||||
-- | If the given list of values are all fully-evaluated thunks
|
||||
-- containing bits, return a packed word built from the same bits.
|
||||
-- However, if any value is not a fully-evaluated bit, return `Nothing`.
|
||||
tryFromBits :: BitWord b w => [Eval (GenValue b w)] -> Maybe w
|
||||
tryFromBits :: BitWord b w i => [Eval (GenValue b w i)] -> Maybe w
|
||||
tryFromBits = go id
|
||||
where
|
||||
go f [] = Just (packWord (f []))
|
||||
@ -681,37 +719,37 @@ fromWord :: String -> Value -> Eval Integer
|
||||
fromWord msg val = bvVal <$> fromVWord msg val
|
||||
|
||||
-- | Extract a function from a value.
|
||||
fromVFun :: GenValue b w -> (Eval (GenValue b w) -> Eval (GenValue b w))
|
||||
fromVFun :: GenValue b w i -> (Eval (GenValue b w i) -> Eval (GenValue b w i))
|
||||
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 -> Eval (GenValue b w))
|
||||
fromVPoly :: GenValue b w i -> (TValue -> Eval (GenValue b w i))
|
||||
fromVPoly val = case val of
|
||||
VPoly f -> f
|
||||
_ -> evalPanic "fromVPoly" ["not a polymorphic value"]
|
||||
|
||||
-- | Extract a polymorphic function from a value.
|
||||
fromVNumPoly :: GenValue b w -> (Nat' -> Eval (GenValue b w))
|
||||
fromVNumPoly :: GenValue b w i -> (Nat' -> Eval (GenValue b w i))
|
||||
fromVNumPoly val = case val of
|
||||
VNumPoly f -> f
|
||||
_ -> evalPanic "fromVNumPoly" ["not a polymorphic value"]
|
||||
|
||||
-- | Extract a tuple from a value.
|
||||
fromVTuple :: GenValue b w -> [Eval (GenValue b w)]
|
||||
fromVTuple :: GenValue b w i -> [Eval (GenValue b w i)]
|
||||
fromVTuple val = case val of
|
||||
VTuple vs -> vs
|
||||
_ -> evalPanic "fromVTuple" ["not a tuple"]
|
||||
|
||||
-- | Extract a record from a value.
|
||||
fromVRecord :: GenValue b w -> [(Ident, Eval (GenValue b w))]
|
||||
fromVRecord :: GenValue b w i -> [(Ident, Eval (GenValue b w i))]
|
||||
fromVRecord val = case val of
|
||||
VRecord fs -> fs
|
||||
_ -> evalPanic "fromVRecord" ["not a record"]
|
||||
|
||||
-- | Lookup a field in a record.
|
||||
lookupRecord :: Ident -> GenValue b w -> Eval (GenValue b w)
|
||||
lookupRecord :: Ident -> GenValue b w i -> Eval (GenValue b w i)
|
||||
lookupRecord f rec = case lookup f (fromVRecord rec) of
|
||||
Just val -> val
|
||||
Nothing -> evalPanic "lookupRecord" ["malformed record"]
|
||||
@ -740,6 +778,8 @@ toExpr prims t0 v0 = findOne (go t0 v0)
|
||||
ETuple `fmap` (zipWithM go ts =<< lift (sequence tvs))
|
||||
(TCon (TC TCBit) [], VBit True ) -> return (prim "True")
|
||||
(TCon (TC TCBit) [], VBit False) -> return (prim "False")
|
||||
(TCon (TC TCInteger) [], VInteger i) ->
|
||||
return $ ETApp (prim "integer") (tNum i)
|
||||
(TCon (TC TCSeq) [a,b], VSeq 0 _) -> do
|
||||
guard (a == tZero)
|
||||
return $ EList [] b
|
||||
|
||||
@ -163,8 +163,10 @@ instance PP RenamerWarning where
|
||||
ppPrec _ (DangerousFixity o1 o2 disp) = fixNameDisp disp $
|
||||
hang (text "[warning] at" <+> pp (srcRange o1))
|
||||
4 $ fsep [ text "Using fixity to resolve the parsing of operators" <+> pp (thing o1) <+> text "and" <+> pp (thing o2) <> text ";"
|
||||
, text "the relative fixity of these operators is planned to change in a future Cryptol release."
|
||||
, text "the relative fixity of these operators has recently changed!"
|
||||
, text "Use parentheses to disambiguate this parse, or consider replacing (&&) with (/\\), or (||) with (\\/)."
|
||||
, text "Ignore this message if you are confident this expression is parsing correctly; it will be removed"
|
||||
, text "in a future release."
|
||||
]
|
||||
|
||||
-- Renaming Monad --------------------------------------------------------------
|
||||
@ -560,6 +562,7 @@ instance Rename Type where
|
||||
go (TFun a b) = TFun <$> go a <*> go b
|
||||
go (TSeq n a) = TSeq <$> go n <*> go a
|
||||
go TBit = return TBit
|
||||
go TInteger = return TInteger
|
||||
go (TNum c) = return (TNum c)
|
||||
go (TChar c) = return (TChar c)
|
||||
go TInf = return TInf
|
||||
@ -615,6 +618,7 @@ resolveTypeFixity = go
|
||||
mkTInfix a' op b'
|
||||
|
||||
TBit -> return t
|
||||
TInteger -> return t
|
||||
TNum _ -> return t
|
||||
TChar _ -> return t
|
||||
TInf -> return t
|
||||
@ -902,6 +906,7 @@ patternEnv = go
|
||||
typeEnv (TSeq a b) = bindTypes [a,b]
|
||||
|
||||
typeEnv TBit = return mempty
|
||||
typeEnv TInteger = return mempty
|
||||
typeEnv TNum{} = return mempty
|
||||
typeEnv TChar{} = return mempty
|
||||
typeEnv TInf = return mempty
|
||||
|
||||
@ -353,6 +353,7 @@ data TParam n = TParam { tpName :: n
|
||||
data Type n = TFun (Type n) (Type n) -- ^ @[8] -> [8]@
|
||||
| TSeq (Type n) (Type n) -- ^ @[8] a@
|
||||
| TBit -- ^ @Bit@
|
||||
| TInteger -- ^ @Integer@
|
||||
| TNum Integer -- ^ @10@
|
||||
| TChar Char -- ^ @'a'@
|
||||
| TInf -- ^ @inf@
|
||||
@ -369,6 +370,7 @@ data Type n = TFun (Type n) (Type n) -- ^ @[8] -> [8]@
|
||||
tconNames :: Map.Map PName (Type PName)
|
||||
tconNames = Map.fromList
|
||||
[ (mkUnqual (packIdent "Bit"), TBit)
|
||||
, (mkUnqual (packIdent "Integer"), TInteger)
|
||||
, (mkUnqual (packIdent "inf"), TInf)
|
||||
]
|
||||
|
||||
@ -824,6 +826,7 @@ instance PPName name => PP (Type name) where
|
||||
TTuple ts -> parens $ commaSep $ map pp ts
|
||||
TRecord fs -> braces $ commaSep $ map (ppNamed ":") fs
|
||||
TBit -> text "Bit"
|
||||
TInteger -> text "Integer"
|
||||
TInf -> text "inf"
|
||||
TNum x -> integer x
|
||||
TChar x -> text (show x)
|
||||
@ -1026,6 +1029,7 @@ instance NoPos (Type name) where
|
||||
TFun x y -> TFun (noPos x) (noPos y)
|
||||
TSeq x y -> TSeq (noPos x) (noPos y)
|
||||
TBit -> TBit
|
||||
TInteger -> TInteger
|
||||
TInf -> TInf
|
||||
TNum n -> TNum n
|
||||
TChar n -> TChar n
|
||||
|
||||
@ -148,6 +148,7 @@ namesT vs = go
|
||||
TFun t1 t2 -> Set.union (go t1) (go t2)
|
||||
TSeq t1 t2 -> Set.union (go t1) (go t2)
|
||||
TBit -> Set.empty
|
||||
TInteger -> Set.empty
|
||||
TNum _ -> Set.empty
|
||||
TChar _ -> Set.empty
|
||||
TInf -> Set.empty
|
||||
@ -292,6 +293,7 @@ tnamesT ty =
|
||||
TFun t1 t2 -> Set.union (tnamesT t1) (tnamesT t2)
|
||||
TSeq t1 t2 -> Set.union (tnamesT t1) (tnamesT t2)
|
||||
TBit -> Set.empty
|
||||
TInteger -> Set.empty
|
||||
TNum _ -> Set.empty
|
||||
TChar __ -> Set.empty
|
||||
TInf -> Set.empty
|
||||
|
||||
@ -183,6 +183,7 @@ validDemotedType rng ty =
|
||||
TFun {} -> bad "Function types"
|
||||
TSeq {} -> bad "Sequence types"
|
||||
TBit -> bad "Type bit"
|
||||
TInteger -> bad "Type integer"
|
||||
TNum {} -> ok
|
||||
TChar {} -> ok
|
||||
TInf -> bad "Infinity type"
|
||||
@ -447,6 +448,7 @@ mkProp ty =
|
||||
TFun{} -> err
|
||||
TSeq{} -> err
|
||||
TBit{} -> err
|
||||
TInteger -> err
|
||||
TNum{} -> err
|
||||
TChar{} -> err
|
||||
TInf{} -> err
|
||||
|
||||
@ -33,7 +33,9 @@ import Cryptol.ModuleSystem.Name (asPrim)
|
||||
import Cryptol.Utils.Ident (Ident,mkIdent)
|
||||
import Cryptol.Utils.PP
|
||||
|
||||
import qualified Data.Foldable as Fold
|
||||
import Data.List (sortBy)
|
||||
import qualified Data.Sequence as Seq
|
||||
import Data.Ord (comparing)
|
||||
import Data.Bits (Bits(..))
|
||||
|
||||
@ -44,7 +46,7 @@ import System.Random.TF.Gen (seedTFGen)
|
||||
|
||||
-- Primitives ------------------------------------------------------------------
|
||||
|
||||
instance EvalPrims Bool BV where
|
||||
instance EvalPrims Bool BV Integer where
|
||||
evalPrim Decl { dName = n, .. }
|
||||
| Just prim <- asPrim n, Just val <- Map.lookup prim primTable = val
|
||||
|
||||
@ -57,21 +59,21 @@ instance EvalPrims Bool BV where
|
||||
primTable :: Map.Map Ident Value
|
||||
primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
|
||||
[ ("+" , {-# SCC "Prelude::(+)" #-}
|
||||
binary (arithBinary (liftBinArith (+))))
|
||||
binary (arithBinary (liftBinArith (+)) (liftBinInteger (+))))
|
||||
, ("-" , {-# SCC "Prelude::(-)" #-}
|
||||
binary (arithBinary (liftBinArith (-))))
|
||||
binary (arithBinary (liftBinArith (-)) (liftBinInteger (-))))
|
||||
, ("*" , {-# SCC "Prelude::(*)" #-}
|
||||
binary (arithBinary (liftBinArith (*))))
|
||||
binary (arithBinary (liftBinArith (*)) (liftBinInteger (*))))
|
||||
, ("/" , {-# SCC "Prelude::(/)" #-}
|
||||
binary (arithBinary (liftDivArith div)))
|
||||
binary (arithBinary (liftDivArith div) (liftDivInteger div)))
|
||||
, ("%" , {-# SCC "Prelude::(%)" #-}
|
||||
binary (arithBinary (liftDivArith mod)))
|
||||
binary (arithBinary (liftDivArith mod) (liftDivInteger mod)))
|
||||
, ("^^" , {-# SCC "Prelude::(^^)" #-}
|
||||
binary (arithBinary modExp))
|
||||
binary (arithBinary modExp integerExp))
|
||||
, ("lg2" , {-# SCC "Prelude::lg2" #-}
|
||||
unary (arithUnary (liftUnaryArith lg2)))
|
||||
unary (arithUnary (liftUnaryArith lg2) lg2))
|
||||
, ("negate" , {-# SCC "Prelude::negate" #-}
|
||||
unary (arithUnary (liftUnaryArith negate)))
|
||||
unary (arithUnary (liftUnaryArith negate) negate))
|
||||
, ("<" , {-# SCC "Prelude::(<)" #-}
|
||||
binary (cmpOrder "<" (\o -> o == LT )))
|
||||
, (">" , {-# SCC "Prelude::(>)" #-}
|
||||
@ -87,27 +89,29 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
|
||||
, ("<$" , {-# SCC "Prelude::(<$)" #-}
|
||||
binary (signedCmpOrder "<$" (\o -> o == LT)))
|
||||
, ("/$" , {-# SCC "Prelude::(/$)" #-}
|
||||
binary (arithBinary (liftSigned bvSdiv)))
|
||||
binary (arithBinary (liftSigned bvSdiv) (liftDivInteger div)))
|
||||
, ("%$" , {-# SCC "Prelude::(%$)" #-}
|
||||
binary (arithBinary (liftSigned bvSrem)))
|
||||
binary (arithBinary (liftSigned bvSrem) (liftDivInteger mod)))
|
||||
, (">>$" , {-# SCC "Prelude::(>>$)" #-}
|
||||
sshrV)
|
||||
, ("&&" , {-# SCC "Prelude::(&&)" #-}
|
||||
binary (logicBinary (.&.) (binBV (.&.))))
|
||||
binary (logicBinary (.&.) (binBV (.&.)) (.&.)))
|
||||
, ("||" , {-# SCC "Prelude::(||)" #-}
|
||||
binary (logicBinary (.|.) (binBV (.|.))))
|
||||
binary (logicBinary (.|.) (binBV (.|.)) (.|.)))
|
||||
, ("^" , {-# SCC "Prelude::(^)" #-}
|
||||
binary (logicBinary xor (binBV xor)))
|
||||
binary (logicBinary xor (binBV xor) xor))
|
||||
, ("complement" , {-# SCC "Prelude::complement" #-}
|
||||
unary (logicUnary complement (unaryBV complement)))
|
||||
unary (logicUnary complement (unaryBV complement) complement))
|
||||
, ("toInteger" , ecToIntegerV)
|
||||
, ("fromInteger", ecFromIntegerV)
|
||||
, ("<<" , {-# SCC "Prelude::(<<)" #-}
|
||||
logicShift shiftLW shiftLS)
|
||||
logicShift shiftLW shiftLB shiftLS)
|
||||
, (">>" , {-# SCC "Prelude::(>>)" #-}
|
||||
logicShift shiftRW shiftRS)
|
||||
logicShift shiftRW shiftRB shiftRS)
|
||||
, ("<<<" , {-# SCC "Prelude::(<<<)" #-}
|
||||
logicShift rotateLW rotateLS)
|
||||
logicShift rotateLW rotateLB rotateLS)
|
||||
, (">>>" , {-# SCC "Prelude::(>>>)" #-}
|
||||
logicShift rotateRW rotateRS)
|
||||
logicShift rotateRW rotateRB rotateRS)
|
||||
, ("True" , VBit True)
|
||||
, ("False" , VBit False)
|
||||
|
||||
@ -117,6 +121,8 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
|
||||
scarryV)
|
||||
, ("demote" , {-# SCC "Prelude::demote" #-}
|
||||
ecDemoteV)
|
||||
, ("integer" , {-# SCC "Prelude::integer" #-}
|
||||
ecIntegerV)
|
||||
|
||||
, ("#" , {-# SCC "Prelude::(#)" #-}
|
||||
nlam $ \ front ->
|
||||
@ -239,7 +245,7 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
|
||||
|
||||
|
||||
-- | Make a numeric constant.
|
||||
ecDemoteV :: BitWord b w => GenValue b w
|
||||
ecDemoteV :: BitWord b w i => GenValue b w i
|
||||
ecDemoteV = nlam $ \valT ->
|
||||
nlam $ \bitT ->
|
||||
case (valT, bitT) of
|
||||
@ -250,6 +256,32 @@ ecDemoteV = nlam $ \valT ->
|
||||
, show bitT
|
||||
]
|
||||
|
||||
-- | Make an integer constant.
|
||||
ecIntegerV :: BitWord b w i => GenValue b w i
|
||||
ecIntegerV = nlam $ \valT ->
|
||||
case valT of
|
||||
Nat v -> VInteger (integerLit v)
|
||||
_ -> evalPanic "Cryptol.Eval.Prim.evalConst"
|
||||
[ "Unexpected Inf in constant."
|
||||
, show valT
|
||||
]
|
||||
|
||||
-- | Convert a word to a non-negative integer.
|
||||
ecToIntegerV :: BitWord b w i => GenValue b w i
|
||||
ecToIntegerV =
|
||||
nlam $ \ _ ->
|
||||
wlam $ \ w -> return $ VInteger (wordToInt w)
|
||||
|
||||
-- | Convert an unbounded integer to a packed bitvector.
|
||||
ecFromIntegerV :: BitWord b w i => GenValue b w i
|
||||
ecFromIntegerV =
|
||||
nlam $ \ a ->
|
||||
lam $ \ x -> do
|
||||
val <- x
|
||||
case (a, val) of
|
||||
(Nat n, VInteger i) -> return $ VWord n $ ready $ WordVal $ wordFromInt n i
|
||||
_ -> evalPanic "fromInteger" ["Invalid arguments"]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
divModPoly :: Integer -> Int -> Integer -> Int -> (Integer, Integer)
|
||||
divModPoly xs xsLen ys ysLen
|
||||
@ -294,6 +326,10 @@ modExp bits (BV _ base) (BV _ e)
|
||||
where
|
||||
modulus = 0 `setBit` fromInteger bits
|
||||
|
||||
integerExp :: Integer -> Integer -> Eval Integer
|
||||
integerExp x y
|
||||
| y < 0 = negativeExponent
|
||||
| otherwise = ready $ x ^ y
|
||||
|
||||
doubleAndAdd :: Integer -- ^ base
|
||||
-> Integer -- ^ exponent mask
|
||||
@ -316,18 +352,18 @@ doubleAndAdd base0 expMask modulus = go 1 base0 expMask
|
||||
|
||||
-- Operation Lifting -----------------------------------------------------------
|
||||
|
||||
type Binary b w = TValue -> GenValue b w -> GenValue b w -> Eval (GenValue b w)
|
||||
type Binary b w i = TValue -> GenValue b w i -> GenValue b w i -> Eval (GenValue b w i)
|
||||
|
||||
binary :: Binary b w -> GenValue b w
|
||||
binary :: Binary b w i -> GenValue b w i
|
||||
binary f = tlam $ \ ty ->
|
||||
lam $ \ a -> return $
|
||||
lam $ \ b -> do
|
||||
--io $ putStrLn "Entering a binary function"
|
||||
join (f ty <$> a <*> b)
|
||||
|
||||
type Unary b w = TValue -> GenValue b w -> Eval (GenValue b w)
|
||||
type Unary b w i = TValue -> GenValue b w i -> Eval (GenValue b w i)
|
||||
|
||||
unary :: Unary b w -> GenValue b w
|
||||
unary :: Unary b w i -> GenValue b w i
|
||||
unary f = tlam $ \ ty ->
|
||||
lam $ \ a -> f ty =<< a
|
||||
|
||||
@ -352,32 +388,47 @@ liftDivArith op w (BV _ x) (BV _ y) = ready $ mkBv w $ op x y
|
||||
|
||||
type BinArith w = Integer -> w -> w -> Eval w
|
||||
|
||||
arithBinary :: forall b w
|
||||
. BitWord b w
|
||||
liftBinInteger :: (Integer -> Integer -> Integer) -> Integer -> Integer -> Eval Integer
|
||||
liftBinInteger op x y = ready $ op x y
|
||||
|
||||
liftDivInteger :: (Integer -> Integer -> Integer) -> Integer -> Integer -> Eval Integer
|
||||
liftDivInteger _ _ 0 = divideByZero
|
||||
liftDivInteger op x y = ready $ op x y
|
||||
|
||||
modWrap :: Integral a => a -> a -> Eval a
|
||||
modWrap _ 0 = divideByZero
|
||||
modWrap x y = return (x `mod` y)
|
||||
|
||||
arithBinary :: forall b w i
|
||||
. BitWord b w i
|
||||
=> BinArith w
|
||||
-> Binary b w
|
||||
arithBinary op = loop
|
||||
-> (i -> i -> Eval i)
|
||||
-> Binary b w i
|
||||
arithBinary opw opi = loop
|
||||
where
|
||||
loop' :: TValue
|
||||
-> Eval (GenValue b w)
|
||||
-> Eval (GenValue b w)
|
||||
-> Eval (GenValue b w)
|
||||
-> Eval (GenValue b w i)
|
||||
-> Eval (GenValue b w i)
|
||||
-> Eval (GenValue b w i)
|
||||
loop' ty l r = join (loop ty <$> l <*> r)
|
||||
|
||||
loop :: TValue
|
||||
-> GenValue b w
|
||||
-> GenValue b w
|
||||
-> Eval (GenValue b w)
|
||||
-> GenValue b w i
|
||||
-> GenValue b w i
|
||||
-> Eval (GenValue b w i)
|
||||
loop ty l r = case ty of
|
||||
TVBit ->
|
||||
evalPanic "arithBinary" ["Bit not in class Arith"]
|
||||
|
||||
TVInteger ->
|
||||
VInteger <$> opi (fromVInteger l) (fromVInteger r)
|
||||
|
||||
TVSeq w a
|
||||
-- words and finite sequences
|
||||
| isTBit a -> do
|
||||
lw <- fromVWord "arithLeft" l
|
||||
rw <- fromVWord "arithRight" r
|
||||
return $ VWord w (WordVal <$> op w lw rw)
|
||||
return $ VWord w (WordVal <$> opw w lw rw)
|
||||
| otherwise -> VSeq w <$> (join (zipSeqMap (loop a) <$>
|
||||
(fromSeq "arithBinary left" l) <*>
|
||||
(fromSeq "arithBinary right" r)))
|
||||
@ -411,26 +462,30 @@ type UnaryArith w = Integer -> w -> Eval w
|
||||
liftUnaryArith :: (Integer -> Integer) -> UnaryArith BV
|
||||
liftUnaryArith op w (BV _ x) = ready $ mkBv w $ op x
|
||||
|
||||
arithUnary :: forall b w
|
||||
. BitWord b w
|
||||
arithUnary :: forall b w i
|
||||
. BitWord b w i
|
||||
=> UnaryArith w
|
||||
-> Unary b w
|
||||
arithUnary op = loop
|
||||
-> (i -> i)
|
||||
-> Unary b w i
|
||||
arithUnary opw opi = loop
|
||||
where
|
||||
loop' :: TValue -> Eval (GenValue b w) -> Eval (GenValue b w)
|
||||
loop' :: TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
|
||||
loop' ty x = loop ty =<< x
|
||||
|
||||
loop :: TValue -> GenValue b w -> Eval (GenValue b w)
|
||||
loop :: TValue -> GenValue b w i -> Eval (GenValue b w i)
|
||||
loop ty x = case ty of
|
||||
|
||||
TVBit ->
|
||||
evalPanic "arithUnary" ["Bit not in class Arith"]
|
||||
|
||||
TVInteger ->
|
||||
return $ VInteger $ opi (fromVInteger x)
|
||||
|
||||
TVSeq w a
|
||||
-- words and finite sequences
|
||||
| isTBit a -> do
|
||||
wx <- fromVWord "arithUnary" x
|
||||
return $ VWord w (WordVal <$> op w wx)
|
||||
return $ VWord w (WordVal <$> opw w wx)
|
||||
| otherwise -> VSeq w <$> (mapSeqMap (loop a) =<< fromSeq "arithUnary" x)
|
||||
|
||||
TVStream a ->
|
||||
@ -464,11 +519,12 @@ lg2 i = case genLog i 2 of
|
||||
|
||||
-- Cmp -------------------------------------------------------------------------
|
||||
|
||||
cmpValue :: BitWord b w
|
||||
cmpValue :: BitWord b w i
|
||||
=> (b -> b -> Eval a -> Eval a)
|
||||
-> (w -> w -> Eval a -> Eval a)
|
||||
-> (GenValue b w -> GenValue b w -> Eval a -> Eval a)
|
||||
cmpValue fb fw = cmp
|
||||
-> (i -> i -> Eval a -> Eval a)
|
||||
-> (GenValue b w i -> GenValue b w i -> Eval a -> Eval a)
|
||||
cmpValue fb fw fi = cmp
|
||||
where
|
||||
cmp v1 v2 k =
|
||||
case (v1, v2) of
|
||||
@ -476,6 +532,7 @@ cmpValue fb fw = cmp
|
||||
in cmpValues (vals fs1) (vals fs2) k
|
||||
(VTuple vs1 , VTuple vs2 ) -> cmpValues vs1 vs2 k
|
||||
(VBit b1 , VBit b2 ) -> fb b1 b2 k
|
||||
(VInteger i1, VInteger i2) -> fi i1 i2 k
|
||||
(VWord _ w1 , VWord _ w2 ) -> join (fw <$> (asWordVal =<< w1)
|
||||
<*> (asWordVal =<< w2)
|
||||
<*> return k)
|
||||
@ -498,7 +555,7 @@ cmpValue fb fw = cmp
|
||||
|
||||
|
||||
lexCompare :: Value -> Value -> Eval Ordering
|
||||
lexCompare a b = cmpValue op opw a b (return EQ)
|
||||
lexCompare a b = cmpValue op opw op a b (return EQ)
|
||||
where
|
||||
opw :: BV -> BV -> Eval Ordering -> Eval Ordering
|
||||
opw x y k = op (bvVal x) (bvVal y) k
|
||||
@ -509,7 +566,7 @@ lexCompare a b = cmpValue op opw a b (return EQ)
|
||||
cmp -> return cmp
|
||||
|
||||
signedLexCompare :: Value -> Value -> Eval Ordering
|
||||
signedLexCompare a b = cmpValue opb opw a b (return EQ)
|
||||
signedLexCompare a b = cmpValue opb opw opi a b (return EQ)
|
||||
where
|
||||
opb :: Bool -> Bool -> Eval Ordering -> Eval Ordering
|
||||
opb _x _y _k = panic "signedLexCompare"
|
||||
@ -520,12 +577,16 @@ signedLexCompare a b = cmpValue opb opw a b (return EQ)
|
||||
EQ -> k
|
||||
cmp -> return cmp
|
||||
|
||||
opi :: Integer -> Integer -> Eval Ordering -> Eval Ordering
|
||||
opi _x _y _k = panic "signedLexCompare"
|
||||
["Attempted to perform signed comparisons on Integer type"]
|
||||
|
||||
-- | Process two elements based on their lexicographic ordering.
|
||||
cmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV
|
||||
cmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV Integer
|
||||
cmpOrder _nm op _ty l r = VBit . op <$> lexCompare l r
|
||||
|
||||
-- | Process two elements based on their lexicographic ordering, using signed comparisons
|
||||
signedCmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV
|
||||
signedCmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV Integer
|
||||
signedCmpOrder _nm op _ty l r = VBit . op <$> signedLexCompare l r
|
||||
|
||||
|
||||
@ -533,9 +594,9 @@ signedCmpOrder _nm op _ty l r = VBit . op <$> signedLexCompare l r
|
||||
|
||||
-- | Lifted operation on finite bitsequences. Used
|
||||
-- for signed comparisons and arithemtic.
|
||||
liftWord :: BitWord b w
|
||||
=> (w -> w -> Eval (GenValue b w))
|
||||
-> GenValue b w
|
||||
liftWord :: BitWord b w i
|
||||
=> (w -> w -> Eval (GenValue b w i))
|
||||
-> GenValue b w i
|
||||
liftWord op =
|
||||
nlam $ \_n ->
|
||||
wlam $ \w1 -> return $
|
||||
@ -609,16 +670,20 @@ carryV =
|
||||
|
||||
-- Logic -----------------------------------------------------------------------
|
||||
|
||||
zeroV :: forall b w
|
||||
. BitWord b w
|
||||
zeroV :: forall b w i
|
||||
. BitWord b w i
|
||||
=> TValue
|
||||
-> GenValue b w
|
||||
-> GenValue b w i
|
||||
zeroV ty = case ty of
|
||||
|
||||
-- bits
|
||||
TVBit ->
|
||||
VBit (bitLit False)
|
||||
|
||||
-- integers
|
||||
TVInteger ->
|
||||
VInteger (integerLit 0)
|
||||
|
||||
-- sequences
|
||||
TVSeq w ety
|
||||
| isTBit ety -> word w 0
|
||||
@ -642,28 +707,37 @@ zeroV ty = case ty of
|
||||
-- | otherwise = evalPanic "zeroV" ["invalid type for zero"]
|
||||
|
||||
|
||||
joinWordVal :: BitWord b w =>
|
||||
WordValue b w -> WordValue b w -> WordValue b w
|
||||
joinWordVal :: BitWord b w i =>
|
||||
WordValue b w i -> WordValue b w i -> WordValue b w i
|
||||
joinWordVal (WordVal w1) (WordVal w2)
|
||||
| wordLen w1 + wordLen w2 < largeBitSize
|
||||
= WordVal $ joinWord w1 w2
|
||||
joinWordVal (BitsVal xs) (WordVal w2)
|
||||
| toInteger (Seq.length xs) + wordLen w2 < largeBitSize
|
||||
= BitsVal (xs Seq.>< Seq.fromList (map ready $ unpackWord w2))
|
||||
joinWordVal (WordVal w1) (BitsVal ys)
|
||||
| wordLen w1 + toInteger (Seq.length ys) < largeBitSize
|
||||
= BitsVal (Seq.fromList (map ready $ unpackWord w1) Seq.>< ys)
|
||||
joinWordVal (BitsVal xs) (BitsVal ys)
|
||||
| toInteger (Seq.length xs) + toInteger (Seq.length ys) < largeBitSize
|
||||
= BitsVal (xs Seq.>< ys)
|
||||
joinWordVal w1 w2
|
||||
= BitsVal (n1+n2) (concatSeqMap n1 (asBitsMap w1) (asBitsMap w2))
|
||||
= LargeBitsVal (n1+n2) (concatSeqMap n1 (asBitsMap w1) (asBitsMap w2))
|
||||
where n1 = wordValueSize w1
|
||||
n2 = wordValueSize w2
|
||||
|
||||
|
||||
joinWords :: forall b w
|
||||
. BitWord b w
|
||||
joinWords :: forall b w i
|
||||
. BitWord b w i
|
||||
=> Integer
|
||||
-> Integer
|
||||
-> SeqMap b w
|
||||
-> Eval (GenValue b w)
|
||||
-> SeqMap b w i
|
||||
-> Eval (GenValue b w i)
|
||||
joinWords nParts nEach xs =
|
||||
loop (ready $ WordVal (wordLit 0 0)) (enumerateSeqMap nParts xs)
|
||||
|
||||
where
|
||||
loop :: Eval (WordValue b w) -> [Eval (GenValue b w)] -> Eval (GenValue b w)
|
||||
loop :: Eval (WordValue b w i) -> [Eval (GenValue b w i)] -> Eval (GenValue b w i)
|
||||
loop !wv [] = return $ VWord (nParts * nEach) wv
|
||||
loop !wv (w : ws) = do
|
||||
w >>= \case
|
||||
@ -671,12 +745,12 @@ joinWords nParts nEach xs =
|
||||
_ -> evalPanic "joinWords: expected word value" []
|
||||
|
||||
|
||||
joinSeq :: BitWord b w
|
||||
joinSeq :: BitWord b w i
|
||||
=> Nat'
|
||||
-> Integer
|
||||
-> TValue
|
||||
-> SeqMap b w
|
||||
-> Eval (GenValue b w)
|
||||
-> SeqMap b w i
|
||||
-> Eval (GenValue b w i)
|
||||
|
||||
-- Special case for 0 length inner sequences.
|
||||
joinSeq _parts 0 a _xs
|
||||
@ -691,7 +765,7 @@ joinSeq (Nat parts) each TVBit xs
|
||||
do let (q,r) = divMod i each
|
||||
ys <- fromWordVal "join seq" =<< lookupSeqMap xs q
|
||||
VBit <$> indexWordValue ys (fromInteger r)
|
||||
return $ VWord (parts * each) $ ready $ BitsVal (parts * each) zs
|
||||
return $ VWord (parts * each) $ ready $ LargeBitsVal (parts * each) zs
|
||||
|
||||
-- infinite sequence of words
|
||||
joinSeq Inf each TVBit xs
|
||||
@ -714,33 +788,36 @@ joinSeq parts each _a xs
|
||||
|
||||
|
||||
-- | Join a sequence of sequences into a single sequence.
|
||||
joinV :: BitWord b w
|
||||
joinV :: BitWord b w i
|
||||
=> Nat'
|
||||
-> Integer
|
||||
-> TValue
|
||||
-> GenValue b w
|
||||
-> Eval (GenValue b w)
|
||||
-> GenValue b w i
|
||||
-> Eval (GenValue b w i)
|
||||
joinV parts each a val = joinSeq parts each a =<< fromSeq "joinV" val
|
||||
|
||||
|
||||
splitWordVal :: BitWord b w
|
||||
splitWordVal :: BitWord b w i
|
||||
=> Integer
|
||||
-> Integer
|
||||
-> WordValue b w
|
||||
-> (WordValue b w, WordValue b w)
|
||||
-> WordValue b w i
|
||||
-> (WordValue b w i, WordValue b w i)
|
||||
splitWordVal leftWidth rightWidth (WordVal w) =
|
||||
let (lw, rw) = splitWord leftWidth rightWidth w
|
||||
in (WordVal lw, WordVal rw)
|
||||
splitWordVal leftWidth rightWidth (BitsVal _n xs) =
|
||||
splitWordVal leftWidth _rightWidth (BitsVal bs) =
|
||||
let (lbs, rbs) = Seq.splitAt (fromInteger leftWidth) bs
|
||||
in (BitsVal lbs, BitsVal rbs)
|
||||
splitWordVal leftWidth rightWidth (LargeBitsVal _n xs) =
|
||||
let (lxs, rxs) = splitSeqMap leftWidth xs
|
||||
in (BitsVal leftWidth lxs, BitsVal rightWidth rxs)
|
||||
in (LargeBitsVal leftWidth lxs, LargeBitsVal rightWidth rxs)
|
||||
|
||||
splitAtV :: BitWord b w
|
||||
splitAtV :: BitWord b w i
|
||||
=> Nat'
|
||||
-> Nat'
|
||||
-> TValue
|
||||
-> GenValue b w
|
||||
-> Eval (GenValue b w)
|
||||
-> GenValue b w i
|
||||
-> Eval (GenValue b w i)
|
||||
splitAtV front back a val =
|
||||
case back of
|
||||
|
||||
@ -753,9 +830,11 @@ splitAtV front back a val =
|
||||
|
||||
Inf | aBit -> do
|
||||
vs <- delay Nothing (fromSeq "splitAtV" val)
|
||||
ls <- delay Nothing (fst . splitSeqMap leftWidth <$> vs)
|
||||
ls <- delay Nothing (do m <- fst . splitSeqMap leftWidth <$> vs
|
||||
let ms = map (fromVBit <$>) (enumerateSeqMap leftWidth m)
|
||||
return $ Seq.fromList $ ms)
|
||||
rs <- delay Nothing (snd . splitSeqMap leftWidth <$> vs)
|
||||
return $ VTuple [ return $ VWord leftWidth (BitsVal leftWidth <$> ls)
|
||||
return $ VTuple [ return $ VWord leftWidth (BitsVal <$> ls)
|
||||
, VStream <$> rs
|
||||
]
|
||||
|
||||
@ -782,21 +861,24 @@ splitAtV front back a val =
|
||||
-- way, the operation `extractWordVal n i w` is equivelant to
|
||||
-- first shifting `w` right by `i` bits, and then truncating to
|
||||
-- `n` bits.
|
||||
extractWordVal :: BitWord b w
|
||||
extractWordVal :: BitWord b w i
|
||||
=> Integer
|
||||
-> Integer
|
||||
-> WordValue b w
|
||||
-> WordValue b w
|
||||
-> WordValue b w i
|
||||
-> WordValue b w i
|
||||
extractWordVal len start (WordVal w) =
|
||||
WordVal $ extractWord len start w
|
||||
extractWordVal len start (BitsVal n xs) =
|
||||
extractWordVal len start (BitsVal bs) =
|
||||
BitsVal $ Seq.take (fromInteger len) $
|
||||
Seq.drop (Seq.length bs - fromInteger start - fromInteger len) bs
|
||||
extractWordVal len start (LargeBitsVal n xs) =
|
||||
let xs' = dropSeqMap (n - start - len) xs
|
||||
in BitsVal len xs'
|
||||
in LargeBitsVal len xs'
|
||||
|
||||
|
||||
-- | Split implementation.
|
||||
ecSplitV :: BitWord b w
|
||||
=> GenValue b w
|
||||
ecSplitV :: BitWord b w i
|
||||
=> GenValue b w i
|
||||
ecSplitV =
|
||||
nlam $ \ parts ->
|
||||
nlam $ \ each ->
|
||||
@ -810,11 +892,11 @@ ecSplitV =
|
||||
(Inf, Nat e) | isTBit a -> do
|
||||
val' <- delay Nothing (fromSeq "ecSplitV" =<< val)
|
||||
return $ VStream $ IndexSeqMap $ \i ->
|
||||
return $ VWord e $ return $ BitsVal e $ IndexSeqMap $ \j ->
|
||||
return $ VWord e $ return $ BitsVal $ Seq.fromFunction (fromInteger e) $ \j ->
|
||||
let idx = i*e + toInteger j
|
||||
in idx `seq` do
|
||||
xs <- val'
|
||||
lookupSeqMap xs idx
|
||||
fromVBit <$> lookupSeqMap xs idx
|
||||
(Nat p, Nat e) -> do
|
||||
val' <- delay Nothing (fromSeq "ecSplitV" =<< val)
|
||||
return $ VSeq p $ IndexSeqMap $ \i ->
|
||||
@ -830,35 +912,36 @@ ecSplitV =
|
||||
_ -> evalPanic "splitV" ["invalid type arguments to split"]
|
||||
|
||||
|
||||
reverseV :: forall b w
|
||||
. BitWord b w
|
||||
=> GenValue b w
|
||||
-> Eval (GenValue b w)
|
||||
reverseV :: forall b w i
|
||||
. BitWord b w i
|
||||
=> GenValue b w i
|
||||
-> Eval (GenValue b w i)
|
||||
reverseV (VSeq n xs) =
|
||||
return $ VSeq n $ reverseSeqMap n xs
|
||||
reverseV (VWord n wv) = return (VWord n (revword <$> wv))
|
||||
where
|
||||
revword w = BitsVal m (reverseSeqMap m (asBitsMap w))
|
||||
where m = wordValueSize w
|
||||
revword (WordVal w) = BitsVal $ Seq.reverse $ Seq.fromList $ map ready $ unpackWord w
|
||||
revword (BitsVal bs) = BitsVal $ Seq.reverse bs
|
||||
revword (LargeBitsVal m xs) = LargeBitsVal m $ reverseSeqMap m xs
|
||||
reverseV _ =
|
||||
evalPanic "reverseV" ["Not a finite sequence"]
|
||||
|
||||
|
||||
transposeV :: BitWord b w
|
||||
transposeV :: BitWord b w i
|
||||
=> Nat'
|
||||
-> Nat'
|
||||
-> TValue
|
||||
-> GenValue b w
|
||||
-> Eval (GenValue b w)
|
||||
-> GenValue b w i
|
||||
-> Eval (GenValue b w i)
|
||||
transposeV a b c xs
|
||||
| isTBit c, Nat na <- a = -- Fin a => [a][b]Bit -> [b][a]Bit
|
||||
return $ bseq $ IndexSeqMap $ \bi ->
|
||||
return $ VWord na $ return $ BitsVal na $
|
||||
IndexSeqMap $ \ai -> do
|
||||
return $ VWord na $ return $ BitsVal $
|
||||
Seq.fromFunction (fromInteger na) $ \ai -> do
|
||||
ys <- flip lookupSeqMap (toInteger ai) =<< fromSeq "transposeV" xs
|
||||
case ys of
|
||||
VStream ys' -> lookupSeqMap ys' bi
|
||||
VWord _ wv -> VBit <$> (flip indexWordValue bi =<< wv)
|
||||
VStream ys' -> fromVBit <$> lookupSeqMap ys' bi
|
||||
VWord _ wv -> flip indexWordValue bi =<< wv
|
||||
_ -> evalPanic "transpose" ["expected sequence of bits"]
|
||||
|
||||
| isTBit c, Inf <- a = -- [inf][b]Bit -> [b][inf]Bit
|
||||
@ -890,13 +973,13 @@ transposeV a b c xs
|
||||
|
||||
|
||||
|
||||
ccatV :: (Show b, Show w, BitWord b w)
|
||||
ccatV :: (Show b, Show w, BitWord b w i)
|
||||
=> Nat'
|
||||
-> Nat'
|
||||
-> TValue
|
||||
-> (GenValue b w)
|
||||
-> (GenValue b w)
|
||||
-> Eval (GenValue b w)
|
||||
-> (GenValue b w i)
|
||||
-> (GenValue b w i)
|
||||
-> Eval (GenValue b w i)
|
||||
|
||||
ccatV _front _back _elty (VWord m l) (VWord n r) =
|
||||
return $ VWord (m+n) (joinWordVal <$> l <*> r)
|
||||
@ -921,39 +1004,47 @@ ccatV front back elty l r = do
|
||||
rs <- r''
|
||||
lookupSeqMap rs (i-n))
|
||||
|
||||
wordValLogicOp :: BitWord b w
|
||||
wordValLogicOp :: BitWord b w i
|
||||
=> (b -> b -> b)
|
||||
-> (w -> w -> w)
|
||||
-> WordValue b w
|
||||
-> WordValue b w
|
||||
-> WordValue b w
|
||||
-> WordValue b w i
|
||||
-> WordValue b w i
|
||||
-> WordValue b w i
|
||||
wordValLogicOp _ wop (WordVal w1) (WordVal w2) = WordVal (wop w1 w2)
|
||||
wordValLogicOp bop _ w1 w2 = BitsVal (wordValueSize w1) zs
|
||||
wordValLogicOp bop _ (BitsVal xs) (BitsVal ys) =
|
||||
BitsVal $ Seq.zipWith (\x y -> bop <$> x <*> y) xs ys
|
||||
wordValLogicOp bop _ (WordVal w1) (BitsVal ys) =
|
||||
BitsVal $ Seq.zipWith (\x y -> bop <$> x <*> y) (Seq.fromList $ map ready $ unpackWord w1) ys
|
||||
wordValLogicOp bop _ (BitsVal xs) (WordVal w2) =
|
||||
BitsVal $ Seq.zipWith (\x y -> bop <$> x <*> y) xs (Seq.fromList $ map ready $ unpackWord w2)
|
||||
wordValLogicOp bop _ w1 w2 = LargeBitsVal (wordValueSize w1) zs
|
||||
where zs = IndexSeqMap $ \i -> VBit <$> (bop <$> (fromBit =<< lookupSeqMap xs i) <*> (fromBit =<< lookupSeqMap ys i))
|
||||
xs = asBitsMap w1
|
||||
ys = asBitsMap w2
|
||||
|
||||
-- | Merge two values given a binop. This is used for and, or and xor.
|
||||
logicBinary :: forall b w
|
||||
. BitWord b w
|
||||
logicBinary :: forall b w i
|
||||
. BitWord b w i
|
||||
=> (b -> b -> b)
|
||||
-> (w -> w -> w)
|
||||
-> Binary b w
|
||||
logicBinary opb opw = loop
|
||||
-> (i -> i -> i)
|
||||
-> Binary b w i
|
||||
logicBinary opb opw opi = loop
|
||||
where
|
||||
loop' :: TValue
|
||||
-> Eval (GenValue b w)
|
||||
-> Eval (GenValue b w)
|
||||
-> Eval (GenValue b w)
|
||||
-> Eval (GenValue b w i)
|
||||
-> Eval (GenValue b w i)
|
||||
-> Eval (GenValue b w i)
|
||||
loop' ty l r = join (loop ty <$> l <*> r)
|
||||
|
||||
loop :: TValue
|
||||
-> GenValue b w
|
||||
-> GenValue b w
|
||||
-> Eval (GenValue b w)
|
||||
-> GenValue b w i
|
||||
-> GenValue b w i
|
||||
-> Eval (GenValue b w i)
|
||||
|
||||
loop ty l r = case ty of
|
||||
TVBit -> return $ VBit (opb (fromVBit l) (fromVBit r))
|
||||
TVInteger -> return $ VInteger (opi (fromVInteger l) (fromVInteger r))
|
||||
TVSeq w aty
|
||||
-- words
|
||||
| isTBit aty
|
||||
@ -992,29 +1083,33 @@ logicBinary opb opw = loop
|
||||
return $ VRecord fs
|
||||
|
||||
|
||||
wordValUnaryOp :: BitWord b w
|
||||
wordValUnaryOp :: BitWord b w i
|
||||
=> (b -> b)
|
||||
-> (w -> w)
|
||||
-> WordValue b w
|
||||
-> Eval (WordValue b w)
|
||||
-> WordValue b w i
|
||||
-> Eval (WordValue b w i)
|
||||
wordValUnaryOp _ wop (WordVal w) = return $ WordVal (wop w)
|
||||
wordValUnaryOp bop _ (BitsVal n xs) = BitsVal n <$> mapSeqMap f xs
|
||||
wordValUnaryOp bop _ (BitsVal bs) = return $ BitsVal (fmap (bop <$>) bs)
|
||||
wordValUnaryOp bop _ (LargeBitsVal n xs) = LargeBitsVal n <$> mapSeqMap f xs
|
||||
where f x = VBit . bop <$> fromBit x
|
||||
|
||||
logicUnary :: forall b w
|
||||
. BitWord b w
|
||||
logicUnary :: forall b w i
|
||||
. BitWord b w i
|
||||
=> (b -> b)
|
||||
-> (w -> w)
|
||||
-> Unary b w
|
||||
logicUnary opb opw = loop
|
||||
-> (i -> i)
|
||||
-> Unary b w i
|
||||
logicUnary opb opw opi = loop
|
||||
where
|
||||
loop' :: TValue -> Eval (GenValue b w) -> Eval (GenValue b w)
|
||||
loop' :: TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
|
||||
loop' ty val = loop ty =<< val
|
||||
|
||||
loop :: TValue -> GenValue b w -> Eval (GenValue b w)
|
||||
loop :: TValue -> GenValue b w i -> Eval (GenValue b w i)
|
||||
loop ty val = case ty of
|
||||
TVBit -> return . VBit . opb $ fromVBit val
|
||||
|
||||
TVInteger -> return . VInteger . opi $ fromVInteger val
|
||||
|
||||
TVSeq w ety
|
||||
-- words
|
||||
| isTBit ety
|
||||
@ -1047,9 +1142,10 @@ logicUnary opb opw = loop
|
||||
logicShift :: (Integer -> Integer -> Integer -> Integer)
|
||||
-- ^ The function may assume its arguments are masked.
|
||||
-- It is responsible for masking its result if needed.
|
||||
-> (Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool))
|
||||
-> (Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap)
|
||||
-> Value
|
||||
logicShift opW opS
|
||||
logicShift opW obB opS
|
||||
= nlam $ \ a ->
|
||||
nlam $ \ _ ->
|
||||
tlam $ \ c ->
|
||||
@ -1059,7 +1155,8 @@ logicShift opW opS
|
||||
l >>= \case
|
||||
VWord w wv -> return $ VWord w $ wv >>= \case
|
||||
WordVal (BV _ x) -> return $ WordVal (BV w (opW w x i))
|
||||
BitsVal n xs -> return $ BitsVal n $ opS (Nat n) c xs i
|
||||
BitsVal bs -> return $ BitsVal (obB w bs i)
|
||||
LargeBitsVal n xs -> return $ LargeBitsVal n $ opS (Nat n) c xs i
|
||||
|
||||
_ -> mkSeq a c <$> (opS a c <$> (fromSeq "logicShift" =<< l) <*> return i)
|
||||
|
||||
@ -1069,6 +1166,12 @@ shiftLW w ival by
|
||||
| by >= w = 0
|
||||
| otherwise = mask w (shiftL ival (fromInteger by))
|
||||
|
||||
shiftLB :: Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool)
|
||||
shiftLB w bs by =
|
||||
Seq.drop (fromInteger (min w by)) bs
|
||||
Seq.><
|
||||
Seq.replicate (fromInteger (min w by)) (ready False)
|
||||
|
||||
shiftLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
|
||||
shiftLS w ety vs by = IndexSeqMap $ \i ->
|
||||
case w of
|
||||
@ -1083,6 +1186,12 @@ shiftRW w i by
|
||||
| by >= w = 0
|
||||
| otherwise = shiftR i (fromInteger by)
|
||||
|
||||
shiftRB :: Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool)
|
||||
shiftRB w bs by =
|
||||
Seq.replicate (fromInteger (min w by)) (ready False)
|
||||
Seq.><
|
||||
Seq.take (fromInteger (w - min w by)) bs
|
||||
|
||||
shiftRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
|
||||
shiftRS w ety vs by = IndexSeqMap $ \i ->
|
||||
case w of
|
||||
@ -1101,6 +1210,11 @@ rotateLW 0 i _ = i
|
||||
rotateLW w i by = mask w $ (i `shiftL` b) .|. (i `shiftR` (fromInteger w - b))
|
||||
where b = fromInteger (by `mod` w)
|
||||
|
||||
rotateLB :: Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool)
|
||||
rotateLB w bs by =
|
||||
let (hd,tl) = Seq.splitAt (fromInteger (by `mod` w)) bs
|
||||
in tl Seq.>< hd
|
||||
|
||||
rotateLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
|
||||
rotateLS w _ vs by = IndexSeqMap $ \i ->
|
||||
case w of
|
||||
@ -1113,6 +1227,11 @@ rotateRW 0 i _ = i
|
||||
rotateRW w i by = mask w $ (i `shiftR` b) .|. (i `shiftL` (fromInteger w - b))
|
||||
where b = fromInteger (by `mod` w)
|
||||
|
||||
rotateRB :: Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool)
|
||||
rotateRB w bs by =
|
||||
let (hd,tl) = Seq.splitAt (fromInteger (w - (by `mod` w))) bs
|
||||
in tl Seq.>< hd
|
||||
|
||||
rotateRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
|
||||
rotateRS w _ vs by = IndexSeqMap $ \i ->
|
||||
case w of
|
||||
@ -1123,10 +1242,10 @@ rotateRS w _ vs by = IndexSeqMap $ \i ->
|
||||
-- Sequence Primitives ---------------------------------------------------------
|
||||
|
||||
-- | Indexing operations that return one element.
|
||||
indexPrimOne :: BitWord b w
|
||||
=> (Maybe Integer -> TValue -> SeqMap b w -> [b] -> Eval (GenValue b w))
|
||||
-> (Maybe Integer -> TValue -> SeqMap b w -> w -> Eval (GenValue b w))
|
||||
-> GenValue b w
|
||||
indexPrimOne :: BitWord b w i
|
||||
=> (Maybe Integer -> TValue -> SeqMap b w i -> Seq.Seq b -> Eval (GenValue b w i))
|
||||
-> (Maybe Integer -> TValue -> SeqMap b w i -> w -> Eval (GenValue b w i))
|
||||
-> GenValue b w i
|
||||
indexPrimOne bits_op word_op =
|
||||
nlam $ \ n ->
|
||||
tlam $ \ a ->
|
||||
@ -1141,7 +1260,8 @@ indexPrimOne bits_op word_op =
|
||||
r >>= \case
|
||||
VWord _ w -> w >>= \case
|
||||
WordVal w' -> word_op (fromNat n) a vs w'
|
||||
BitsVal m xs -> bits_op (fromNat n) a vs =<< traverse (fromBit =<<) (enumerateSeqMap m xs)
|
||||
BitsVal bs -> bits_op (fromNat n) a vs =<< sequence bs
|
||||
LargeBitsVal m xs -> bits_op (fromNat n) a vs . Seq.fromList =<< traverse (fromBit =<<) (enumerateSeqMap m xs)
|
||||
_ -> evalPanic "Expected word value" ["indexPrimOne"]
|
||||
|
||||
indexFront :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value
|
||||
@ -1150,8 +1270,8 @@ indexFront mblen _a vs (bvVal -> ix) =
|
||||
Just len | len <= ix -> invalidIndex ix
|
||||
_ -> lookupSeqMap vs ix
|
||||
|
||||
indexFront_bits :: Maybe Integer -> TValue -> SeqValMap -> [Bool] -> Eval Value
|
||||
indexFront_bits mblen a vs = indexFront mblen a vs . packWord
|
||||
indexFront_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq.Seq Bool -> Eval Value
|
||||
indexFront_bits mblen a vs = indexFront mblen a vs . packWord . Fold.toList
|
||||
|
||||
indexBack :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value
|
||||
indexBack mblen _a vs (bvVal -> ix) =
|
||||
@ -1161,14 +1281,14 @@ indexBack mblen _a vs (bvVal -> ix) =
|
||||
Nothing -> evalPanic "indexBack"
|
||||
["unexpected infinite sequence"]
|
||||
|
||||
indexBack_bits :: Maybe Integer -> TValue -> SeqValMap -> [Bool] -> Eval Value
|
||||
indexBack_bits mblen a vs = indexBack mblen a vs . packWord
|
||||
indexBack_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq.Seq Bool -> Eval Value
|
||||
indexBack_bits mblen a vs = indexBack mblen a vs . packWord . Fold.toList
|
||||
|
||||
-- | Indexing operations that return many elements.
|
||||
indexPrimMany :: BitWord b w
|
||||
=> (Maybe Integer -> TValue -> SeqMap b w -> [b] -> Eval (GenValue b w))
|
||||
-> (Maybe Integer -> TValue -> SeqMap b w -> w -> Eval (GenValue b w))
|
||||
-> GenValue b w
|
||||
indexPrimMany :: BitWord b w i
|
||||
=> (Maybe Integer -> TValue -> SeqMap b w i -> Seq.Seq b -> Eval (GenValue b w i))
|
||||
-> (Maybe Integer -> TValue -> SeqMap b w i -> w -> Eval (GenValue b w i))
|
||||
-> GenValue b w i
|
||||
indexPrimMany bits_op word_op =
|
||||
nlam $ \ n ->
|
||||
tlam $ \ a ->
|
||||
@ -1186,17 +1306,18 @@ indexPrimMany bits_op word_op =
|
||||
lookupSeqMap ixs i >>= \case
|
||||
VWord _ w -> w >>= \case
|
||||
WordVal w' -> word_op (fromNat n) a vs w'
|
||||
BitsVal o xs -> bits_op (fromNat n) a vs =<< traverse (fromBit =<<) (enumerateSeqMap o xs)
|
||||
BitsVal bs -> bits_op (fromNat n) a vs =<< sequence bs
|
||||
LargeBitsVal o xs -> bits_op (fromNat n) a vs . Seq.fromList =<< traverse (fromBit =<<) (enumerateSeqMap o xs)
|
||||
_ -> evalPanic "Expected word value" ["indexPrimMany"])
|
||||
|
||||
|
||||
updateFront
|
||||
:: Nat'
|
||||
-> TValue
|
||||
-> SeqMap Bool BV
|
||||
-> WordValue Bool BV
|
||||
-> Eval (GenValue Bool BV)
|
||||
-> Eval (SeqMap Bool BV)
|
||||
-> SeqMap Bool BV Integer
|
||||
-> WordValue Bool BV Integer
|
||||
-> Eval (GenValue Bool BV Integer)
|
||||
-> Eval (SeqMap Bool BV Integer)
|
||||
updateFront len _eltTy vs w val = do
|
||||
idx <- bvVal <$> asWordVal w
|
||||
case len of
|
||||
@ -1207,10 +1328,10 @@ updateFront len _eltTy vs w val = do
|
||||
updateFront_word
|
||||
:: Nat'
|
||||
-> TValue
|
||||
-> WordValue Bool BV
|
||||
-> WordValue Bool BV
|
||||
-> Eval (GenValue Bool BV)
|
||||
-> Eval (WordValue Bool BV)
|
||||
-> WordValue Bool BV Integer
|
||||
-> WordValue Bool BV Integer
|
||||
-> Eval (GenValue Bool BV Integer)
|
||||
-> Eval (WordValue Bool BV Integer)
|
||||
updateFront_word _len _eltTy bs w val = do
|
||||
idx <- bvVal <$> asWordVal w
|
||||
updateWordValue bs idx (fromBit =<< val)
|
||||
@ -1218,10 +1339,10 @@ updateFront_word _len _eltTy bs w val = do
|
||||
updateBack
|
||||
:: Nat'
|
||||
-> TValue
|
||||
-> SeqMap Bool BV
|
||||
-> WordValue Bool BV
|
||||
-> Eval (GenValue Bool BV)
|
||||
-> Eval (SeqMap Bool BV)
|
||||
-> SeqMap Bool BV Integer
|
||||
-> WordValue Bool BV Integer
|
||||
-> Eval (GenValue Bool BV Integer)
|
||||
-> Eval (SeqMap Bool BV Integer)
|
||||
updateBack Inf _eltTy _vs _w _val =
|
||||
evalPanic "Unexpected infinite sequence in updateEnd" []
|
||||
updateBack (Nat n) _eltTy vs w val = do
|
||||
@ -1232,10 +1353,10 @@ updateBack (Nat n) _eltTy vs w val = do
|
||||
updateBack_word
|
||||
:: Nat'
|
||||
-> TValue
|
||||
-> WordValue Bool BV
|
||||
-> WordValue Bool BV
|
||||
-> Eval (GenValue Bool BV)
|
||||
-> Eval (WordValue Bool BV)
|
||||
-> WordValue Bool BV Integer
|
||||
-> WordValue Bool BV Integer
|
||||
-> Eval (GenValue Bool BV Integer)
|
||||
-> Eval (WordValue Bool BV Integer)
|
||||
updateBack_word Inf _eltTy _bs _w _val =
|
||||
evalPanic "Unexpected infinite sequence in updateEnd" []
|
||||
updateBack_word (Nat n) _eltTy bs w val = do
|
||||
@ -1251,10 +1372,10 @@ updateBack_word (Nat n) _eltTy bs w val = do
|
||||
|
||||
|
||||
updatePrim
|
||||
:: BitWord b w
|
||||
=> (Nat' -> TValue -> WordValue b w -> WordValue b w -> Eval (GenValue b w) -> Eval (WordValue b w))
|
||||
-> (Nat' -> TValue -> SeqMap b w -> WordValue b w -> Eval (GenValue b w) -> Eval (SeqMap b w))
|
||||
-> GenValue b w
|
||||
:: BitWord b w i
|
||||
=> (Nat' -> TValue -> WordValue b w i -> WordValue b w i -> Eval (GenValue b w i) -> Eval (WordValue b w i))
|
||||
-> (Nat' -> TValue -> SeqMap b w i -> WordValue b w i -> Eval (GenValue b w i) -> Eval (SeqMap b w i))
|
||||
-> GenValue b w i
|
||||
updatePrim updateWord updateSeq =
|
||||
nlam $ \len ->
|
||||
tlam $ \eltTy ->
|
||||
@ -1271,8 +1392,8 @@ updatePrim updateWord updateSeq =
|
||||
_ -> evalPanic "Expected sequence value" ["updatePrim"]
|
||||
|
||||
-- @[ 0, 1 .. ]@
|
||||
fromThenV :: BitWord b w
|
||||
=> GenValue b w
|
||||
fromThenV :: BitWord b w i
|
||||
=> GenValue b w i
|
||||
fromThenV =
|
||||
nlam $ \ first ->
|
||||
nlam $ \ next ->
|
||||
@ -1289,8 +1410,8 @@ fromThenV =
|
||||
_ -> evalPanic "fromThenV" ["invalid arguments"]
|
||||
|
||||
-- @[ 0 .. 10 ]@
|
||||
fromToV :: BitWord b w
|
||||
=> GenValue b w
|
||||
fromToV :: BitWord b w i
|
||||
=> GenValue b w i
|
||||
fromToV =
|
||||
nlam $ \ first ->
|
||||
nlam $ \ lst ->
|
||||
@ -1306,8 +1427,8 @@ fromToV =
|
||||
_ -> evalPanic "fromToV" ["invalid arguments"]
|
||||
|
||||
-- @[ 0, 1 .. 10 ]@
|
||||
fromThenToV :: BitWord b w
|
||||
=> GenValue b w
|
||||
fromThenToV :: BitWord b w i
|
||||
=> GenValue b w i
|
||||
fromThenToV =
|
||||
nlam $ \ first ->
|
||||
nlam $ \ next ->
|
||||
@ -1325,8 +1446,8 @@ fromThenToV =
|
||||
_ -> evalPanic "fromThenToV" ["invalid arguments"]
|
||||
|
||||
|
||||
infFromV :: BitWord b w
|
||||
=> GenValue b w
|
||||
infFromV :: BitWord b w i
|
||||
=> GenValue b w i
|
||||
infFromV =
|
||||
nlam $ \(finNat' -> bits) ->
|
||||
wlam $ \first ->
|
||||
@ -1334,8 +1455,8 @@ infFromV =
|
||||
ready $ VWord bits $ return $
|
||||
WordVal $ wordPlus first (wordLit bits i)
|
||||
|
||||
infFromThenV :: BitWord b w
|
||||
=> GenValue b w
|
||||
infFromThenV :: BitWord b w i
|
||||
=> GenValue b w i
|
||||
infFromThenV =
|
||||
nlam $ \(finNat' -> bits) ->
|
||||
wlam $ \first -> return $
|
||||
@ -1350,7 +1471,7 @@ infFromThenV =
|
||||
-- | Produce a random value with the given seed. If we do not support
|
||||
-- making values of the given type, return zero of that type.
|
||||
-- TODO: do better than returning zero
|
||||
randomV :: BitWord b w => TValue -> Integer -> GenValue b w
|
||||
randomV :: BitWord b w i => TValue -> Integer -> GenValue b w i
|
||||
randomV ty seed =
|
||||
case randomValue (tValTy ty) of
|
||||
Nothing -> zeroV ty
|
||||
@ -1363,18 +1484,20 @@ randomV ty seed =
|
||||
|
||||
-- Miscellaneous ---------------------------------------------------------------
|
||||
|
||||
errorV :: forall b w
|
||||
. BitWord b w
|
||||
errorV :: forall b w i
|
||||
. BitWord b w i
|
||||
=> TValue
|
||||
-> String
|
||||
-> Eval (GenValue b w)
|
||||
-> Eval (GenValue b w i)
|
||||
errorV ty msg = case ty of
|
||||
-- bits
|
||||
TVBit -> cryUserError msg
|
||||
TVInteger -> cryUserError msg
|
||||
|
||||
-- sequences
|
||||
TVSeq w ety
|
||||
| isTBit ety -> return $ VWord w $ return $ BitsVal w $ IndexSeqMap $ \_ -> cryUserError msg
|
||||
| isTBit ety -> return $ VWord w $ return $ BitsVal $
|
||||
Seq.replicate (fromInteger w) (cryUserError msg)
|
||||
| otherwise -> return $ VSeq w (IndexSeqMap $ \_ -> errorV ety msg)
|
||||
|
||||
TVStream ety ->
|
||||
|
||||
@ -279,6 +279,14 @@ evalCmd str = do
|
||||
-- be generalized if mono-binds is enabled
|
||||
replEvalDecl decl
|
||||
|
||||
printCounterexample :: Bool -> P.Expr P.PName -> [E.Value] -> REPL ()
|
||||
printCounterexample isSat pexpr vs =
|
||||
do ppOpts <- getPPValOpts
|
||||
docs <- mapM (io . E.runEval . E.ppValue ppOpts) vs
|
||||
let doc = ppPrec 3 pexpr -- function application has precedence 3
|
||||
rPrint $ hang doc 2 (sep docs) <+>
|
||||
text (if isSat then "= True" else "= False")
|
||||
|
||||
data QCMode = QCRandom | QCExhaust deriving (Eq, Show)
|
||||
|
||||
-- | Randomly test a property, or exhaustively check it if the number
|
||||
@ -314,7 +322,7 @@ qcCmd qcMode str =
|
||||
, testPossible = sz
|
||||
, testRptProgress = ppProgress
|
||||
, testClrProgress = delProgress
|
||||
, testRptFailure = ppFailure
|
||||
, testRptFailure = ppFailure expr
|
||||
, testRptSuccess = do
|
||||
delTesting
|
||||
prtLn $ "passed " ++ show sz ++ " tests."
|
||||
@ -335,7 +343,7 @@ qcCmd qcMode str =
|
||||
, testPossible = sz
|
||||
, testRptProgress = ppProgress
|
||||
, testClrProgress = delProgress
|
||||
, testRptFailure = ppFailure
|
||||
, testRptFailure = ppFailure expr
|
||||
, testRptSuccess = do
|
||||
delTesting
|
||||
prtLn $ "passed " ++ show testNum ++ " tests."
|
||||
@ -381,15 +389,13 @@ qcCmd qcMode str =
|
||||
delTesting = del (length testingMsg)
|
||||
delProgress = del totProgressWidth
|
||||
|
||||
ppFailure failure = do
|
||||
ppFailure pexpr failure = do
|
||||
delTesting
|
||||
opts <- getPPValOpts
|
||||
case failure of
|
||||
FailFalse [] -> do
|
||||
prtLn "FAILED"
|
||||
FailFalse vs -> do
|
||||
prtLn "FAILED for the following inputs:"
|
||||
mapM_ (\v -> rPrint =<< (io $ E.runEval $ E.ppValue opts v)) vs
|
||||
let isSat = False
|
||||
printCounterexample isSat pexpr vs
|
||||
FailError err [] -> do
|
||||
prtLn "ERROR"
|
||||
rPrint (pp err)
|
||||
@ -451,7 +457,6 @@ cmdProveSat isSat str = do
|
||||
Nothing -> rPutStr smtlib
|
||||
_ -> do
|
||||
(firstProver,result,stats) <- onlineProveSat isSat str mfile
|
||||
ppOpts <- getPPValOpts
|
||||
case result of
|
||||
Symbolic.EmptyResult ->
|
||||
panic "REPL.Command" [ "got EmptyResult for online prover query" ]
|
||||
@ -463,13 +468,6 @@ cmdProveSat isSat str = do
|
||||
Symbolic.AllSatResult tevss -> do
|
||||
let tess = map (map $ \(t,e,_) -> (t,e)) tevss
|
||||
vss = map (map $ \(_,_,v) -> v) tevss
|
||||
ppvs vs = do
|
||||
parseExpr <- replParseExpr str
|
||||
docs <- mapM (io . E.runEval . E.ppValue ppOpts) vs
|
||||
let -- function application has precedence 3
|
||||
doc = ppPrec 3 parseExpr
|
||||
rPrint $ hang doc 2 (sep docs) <+>
|
||||
text (if isSat then "= True" else "= False")
|
||||
resultRecs <- mapM (mkSolverResult cexStr isSat . Right) tess
|
||||
let collectTes tes = (t, es)
|
||||
where
|
||||
@ -484,7 +482,8 @@ cmdProveSat isSat str = do
|
||||
[ "no satisfying assignments after mkSolverResult" ]
|
||||
[(t, e)] -> (t, [e])
|
||||
_ -> collectTes resultRecs
|
||||
forM_ vss ppvs
|
||||
pexpr <- replParseExpr str
|
||||
forM_ vss (printCounterexample isSat pexpr)
|
||||
case (ty, exprs) of
|
||||
(t, [e]) -> bindItVariable t e
|
||||
(t, es ) -> bindItVariables t es
|
||||
|
||||
@ -259,6 +259,10 @@ parseValues (t : ts) cws = (v : vs, cws'')
|
||||
parseValue :: FinType -> [SBV.CW] -> (Eval.Value, [SBV.CW])
|
||||
parseValue FTBit [] = panic "Cryptol.Symbolic.parseValue" [ "empty FTBit" ]
|
||||
parseValue FTBit (cw : cws) = (Eval.VBit (SBV.cwToBool cw), cws)
|
||||
parseValue FTInteger cws =
|
||||
case SBV.genParse SBV.KUnbounded cws of
|
||||
Just (x, cws') -> (Eval.VInteger x, cws')
|
||||
Nothing -> panic "Cryptol.Symbolic.parseValue" [ "no integer" ]
|
||||
parseValue (FTSeq 0 FTBit) cws = (Eval.word 0 0, cws)
|
||||
parseValue (FTSeq n FTBit) cws =
|
||||
case SBV.genParse (SBV.KBounded False n) cws of
|
||||
@ -282,6 +286,7 @@ allDeclGroups = concatMap mDecls . M.loadedModules
|
||||
|
||||
data FinType
|
||||
= FTBit
|
||||
| FTInteger
|
||||
| FTSeq Int FinType
|
||||
| FTTuple [FinType]
|
||||
| FTRecord [(Ident, FinType)]
|
||||
@ -295,6 +300,7 @@ finType :: TValue -> Maybe FinType
|
||||
finType ty =
|
||||
case ty of
|
||||
Eval.TVBit -> Just FTBit
|
||||
Eval.TVInteger -> Just FTInteger
|
||||
Eval.TVSeq n t -> FTSeq <$> numType n <*> finType t
|
||||
Eval.TVTuple ts -> FTTuple <$> traverse finType ts
|
||||
Eval.TVRec fields -> FTRecord <$> traverse (traverseSnd finType) fields
|
||||
@ -304,6 +310,7 @@ unFinType :: FinType -> Type
|
||||
unFinType fty =
|
||||
case fty of
|
||||
FTBit -> tBit
|
||||
FTInteger -> tInteger
|
||||
FTSeq l ety -> tSeq (tNum l) (unFinType ety)
|
||||
FTTuple ftys -> tTuple (unFinType <$> ftys)
|
||||
FTRecord fs -> tRec (zip fns tys)
|
||||
@ -328,6 +335,7 @@ forallFinType :: FinType -> SBV.Symbolic Value
|
||||
forallFinType ty =
|
||||
case ty of
|
||||
FTBit -> VBit <$> forallSBool_
|
||||
FTInteger -> VInteger <$> forallSInteger_
|
||||
FTSeq 0 FTBit -> return $ Eval.word 0 0
|
||||
FTSeq n FTBit -> VWord (toInteger n) . return . Eval.WordVal <$> (forallBV_ n)
|
||||
FTSeq n t -> do vs <- replicateM n (forallFinType t)
|
||||
@ -339,6 +347,7 @@ existsFinType :: FinType -> SBV.Symbolic Value
|
||||
existsFinType ty =
|
||||
case ty of
|
||||
FTBit -> VBit <$> existsSBool_
|
||||
FTInteger -> VInteger <$> existsSInteger_
|
||||
FTSeq 0 FTBit -> return $ Eval.word 0 0
|
||||
FTSeq n FTBit -> VWord (toInteger n) . return . Eval.WordVal <$> (existsBV_ n)
|
||||
FTSeq n t -> do vs <- replicateM n (existsFinType t)
|
||||
|
||||
@ -22,6 +22,7 @@ import Control.Monad (unless)
|
||||
import Data.Bits
|
||||
import Data.List (genericTake)
|
||||
import qualified Data.Sequence as Seq
|
||||
import qualified Data.Foldable as Fold
|
||||
|
||||
import Cryptol.Eval.Monad (Eval(..), ready, invalidIndex, cryUserError)
|
||||
import Cryptol.Eval.Type (finNat', TValue(..))
|
||||
@ -37,8 +38,9 @@ import Cryptol.Prims.Eval (binary, unary, arithUnary,
|
||||
reverseV, infFromV, infFromThenV,
|
||||
fromThenV, fromToV, fromThenToV,
|
||||
transposeV, indexPrimOne, indexPrimMany,
|
||||
ecIntegerV, ecToIntegerV, ecFromIntegerV,
|
||||
ecDemoteV, updatePrim, randomV, liftWord,
|
||||
cmpValue)
|
||||
cmpValue, lg2)
|
||||
import Cryptol.Symbolic.Value
|
||||
import Cryptol.TypeCheck.AST (Decl(..))
|
||||
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
|
||||
@ -60,7 +62,7 @@ traverseSnd f (x, y) = (,) x <$> f y
|
||||
|
||||
-- Primitives ------------------------------------------------------------------
|
||||
|
||||
instance EvalPrims SBool SWord where
|
||||
instance EvalPrims SBool SWord SInteger where
|
||||
evalPrim Decl { dName = n, .. }
|
||||
| Just prim <- asPrim n, Just val <- Map.lookup prim primTable = val
|
||||
|
||||
@ -78,30 +80,35 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
|
||||
, ("False" , VBit SBV.svFalse)
|
||||
, ("demote" , ecDemoteV) -- Converts a numeric type into its corresponding value.
|
||||
-- { val, bits } (fin val, fin bits, bits >= width val) => [bits]
|
||||
, ("+" , binary (arithBinary (liftBinArith SBV.svPlus))) -- {a} (Arith a) => a -> a -> a
|
||||
, ("-" , binary (arithBinary (liftBinArith SBV.svMinus))) -- {a} (Arith a) => a -> a -> a
|
||||
, ("*" , binary (arithBinary (liftBinArith SBV.svTimes))) -- {a} (Arith a) => a -> a -> a
|
||||
, ("/" , binary (arithBinary (liftBinArith SBV.svQuot))) -- {a} (Arith a) => a -> a -> a
|
||||
, ("%" , binary (arithBinary (liftBinArith SBV.svRem))) -- {a} (Arith a) => a -> a -> a
|
||||
, ("^^" , binary (arithBinary sExp)) -- {a} (Arith a) => a -> a -> a
|
||||
, ("lg2" , unary (arithUnary sLg2)) -- {a} (Arith a) => a -> a
|
||||
, ("negate" , unary (arithUnary (\_ -> ready . SBV.svUNeg)))
|
||||
, ("<" , binary (cmpBinary cmpLt cmpLt SBV.svFalse))
|
||||
, (">" , binary (cmpBinary cmpGt cmpGt SBV.svFalse))
|
||||
, ("<=" , binary (cmpBinary cmpLtEq cmpLtEq SBV.svTrue))
|
||||
, (">=" , binary (cmpBinary cmpGtEq cmpGtEq SBV.svTrue))
|
||||
, ("==" , binary (cmpBinary cmpEq cmpEq SBV.svTrue))
|
||||
, ("!=" , binary (cmpBinary cmpNotEq cmpNotEq SBV.svFalse))
|
||||
, ("integer" , ecIntegerV) -- Converts a numeric type into its corresponding value.
|
||||
-- { val } (fin val) => Integer
|
||||
, ("+" , binary (arithBinary (liftBinArith SBV.svPlus) (liftBin SBV.svPlus))) -- {a} (Arith a) => a -> a -> a
|
||||
, ("-" , binary (arithBinary (liftBinArith SBV.svMinus) (liftBin SBV.svMinus))) -- {a} (Arith a) => a -> a -> a
|
||||
, ("*" , binary (arithBinary (liftBinArith SBV.svTimes) (liftBin SBV.svTimes))) -- {a} (Arith a) => a -> a -> a
|
||||
, ("/" , binary (arithBinary (liftBinArith SBV.svQuot) (liftBin SBV.svQuot))) -- {a} (Arith a) => a -> a -> a
|
||||
, ("%" , binary (arithBinary (liftBinArith SBV.svRem) (liftBin SBV.svRem))) -- {a} (Arith a) => a -> a -> a
|
||||
, ("^^" , binary (arithBinary sExp (liftBin SBV.svExp))) -- {a} (Arith a) => a -> a -> a
|
||||
, ("lg2" , unary (arithUnary sLg2 svLg2)) -- {a} (Arith a) => a -> a
|
||||
, ("negate" , unary (arithUnary (\_ -> ready . SBV.svUNeg) SBV.svUNeg))
|
||||
, ("<" , binary (cmpBinary cmpLt cmpLt cmpLt SBV.svFalse))
|
||||
, (">" , binary (cmpBinary cmpGt cmpGt cmpGt SBV.svFalse))
|
||||
, ("<=" , binary (cmpBinary cmpLtEq cmpLtEq cmpLtEq SBV.svTrue))
|
||||
, (">=" , binary (cmpBinary cmpGtEq cmpGtEq cmpGtEq SBV.svTrue))
|
||||
, ("==" , binary (cmpBinary cmpEq cmpEq cmpEq SBV.svTrue))
|
||||
, ("!=" , binary (cmpBinary cmpNotEq cmpNotEq cmpNotEq SBV.svFalse))
|
||||
, ("<$" , let boolFail = evalPanic "<$" ["Attempted signed comparison on bare Bit values"]
|
||||
in binary (cmpBinary boolFail cmpSignedLt SBV.svFalse))
|
||||
, ("/$" , binary (arithBinary (liftBinArith signedQuot)))
|
||||
, ("%$" , binary (arithBinary (liftBinArith signedRem)))
|
||||
intFail = evalPanic "<$" ["Attempted signed comparison on Integer values"]
|
||||
in binary (cmpBinary boolFail cmpSignedLt intFail SBV.svFalse))
|
||||
, ("/$" , binary (arithBinary (liftBinArith signedQuot) (liftBin SBV.svQuot)))
|
||||
, ("%$" , binary (arithBinary (liftBinArith signedRem) (liftBin SBV.svRem)))
|
||||
, (">>$" , sshrV)
|
||||
, ("&&" , binary (logicBinary SBV.svAnd SBV.svAnd))
|
||||
, ("||" , binary (logicBinary SBV.svOr SBV.svOr))
|
||||
, ("^" , binary (logicBinary SBV.svXOr SBV.svXOr))
|
||||
, ("complement" , unary (logicUnary SBV.svNot SBV.svNot))
|
||||
, ("&&" , binary (logicBinary SBV.svAnd SBV.svAnd SBV.svAnd))
|
||||
, ("||" , binary (logicBinary SBV.svOr SBV.svOr SBV.svOr))
|
||||
, ("^" , binary (logicBinary SBV.svXOr SBV.svXOr SBV.svXOr))
|
||||
, ("complement" , unary (logicUnary SBV.svNot SBV.svNot SBV.svNot))
|
||||
, ("zero" , tlam zeroV)
|
||||
, ("toInteger" , ecToIntegerV)
|
||||
, ("fromInteger" , ecFromIntegerV)
|
||||
, ("<<" , logicShift "<<"
|
||||
SBV.svShiftLeft
|
||||
(\sz i shft ->
|
||||
@ -187,8 +194,8 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
|
||||
mul as (b:bs) ps = mul (SBV.svFalse : as) bs (ites b (as `addPoly` ps) ps)
|
||||
xs <- enumerateWordValue =<< fromWordVal "pmult 1" =<< v1
|
||||
ys <- enumerateWordValue =<< fromWordVal "pmult 2" =<< v2
|
||||
let zs = Seq.fromList $ genericTake k (mul xs ys [] ++ repeat SBV.svFalse)
|
||||
return $ VWord k $ return $ BitsVal k $ IndexSeqMap (return . VBit . Seq.index zs . fromInteger))
|
||||
let zs = genericTake k (mul xs ys [] ++ repeat SBV.svFalse)
|
||||
return $ VWord k $ return $ BitsVal $ Seq.fromList $ map ready zs)
|
||||
|
||||
, ("pdiv" , -- {a,b} (fin a, fin b) => [a] -> [b] -> [a]
|
||||
nlam $ \(finNat' -> i) ->
|
||||
@ -197,8 +204,8 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
|
||||
VFun $ \v2 -> do
|
||||
xs <- enumerateWordValueRev =<< fromWordVal "pdiv 1" =<< v1
|
||||
ys <- enumerateWordValueRev =<< fromWordVal "pdiv 2" =<< v2
|
||||
let zs = Seq.reverse $ Seq.fromList $ genericTake i (fst (mdp xs ys) ++ repeat SBV.svFalse)
|
||||
return $ VWord i $ return $ BitsVal i $ IndexSeqMap (return . VBit . Seq.index zs . fromInteger))
|
||||
let zs = genericTake i (fst (mdp xs ys) ++ repeat SBV.svFalse)
|
||||
return $ VWord i $ return $ BitsVal $ Seq.reverse $ Seq.fromList $ map ready zs)
|
||||
|
||||
, ("pmod" , -- {a,b} (fin a, fin b) => [a] -> [b+1] -> [b]
|
||||
nlam $ \(finNat' -> _i) ->
|
||||
@ -207,8 +214,8 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
|
||||
VFun $ \v2 -> do
|
||||
xs <- enumerateWordValueRev =<< fromWordVal "pmod 1" =<< v1
|
||||
ys <- enumerateWordValueRev =<< fromWordVal "pmod 2" =<< v2
|
||||
let zs = Seq.reverse $ Seq.fromList $ genericTake j (snd (mdp xs ys) ++ repeat SBV.svFalse)
|
||||
return $ VWord j $ return $ BitsVal j $ IndexSeqMap (return . VBit . Seq.index zs . fromInteger))
|
||||
let zs = genericTake j (snd (mdp xs ys) ++ repeat SBV.svFalse)
|
||||
return $ VWord j $ return $ BitsVal $ Seq.reverse $ Seq.fromList $ map ready zs)
|
||||
|
||||
-- {at,len} (fin len) => [len][8] -> at
|
||||
, ("error" ,
|
||||
@ -266,13 +273,20 @@ logicShift nm wop reindex =
|
||||
return $ VWord w $ do
|
||||
x >>= \case
|
||||
WordVal x' -> WordVal . wop x' <$> asWordVal idx
|
||||
BitsVal n bs0 ->
|
||||
BitsVal bs0 ->
|
||||
do idx_bits <- enumerateWordValue idx
|
||||
let op bs shft = return $ Seq.fromFunction (Seq.length bs) $ \i ->
|
||||
case reindex (Nat w) (toInteger i) shft of
|
||||
Nothing -> return $ bitLit False
|
||||
Just i' -> Seq.index bs (fromInteger i')
|
||||
BitsVal <$> shifter (mergeBits True) op bs0 idx_bits
|
||||
LargeBitsVal n bs0 ->
|
||||
do idx_bits <- enumerateWordValue idx
|
||||
let op bs shft = memoMap $ IndexSeqMap $ \i ->
|
||||
case reindex (Nat w) i shft of
|
||||
Nothing -> return $ VBit $ bitLit False
|
||||
Just i' -> lookupSeqMap bs i'
|
||||
BitsVal n <$> shifter (mergeSeqMap True) op bs0 idx_bits
|
||||
LargeBitsVal n <$> shifter (mergeSeqMap True) op bs0 idx_bits
|
||||
|
||||
VSeq w vs0 ->
|
||||
do idx_bits <- enumerateWordValue idx
|
||||
@ -295,14 +309,15 @@ logicShift nm wop reindex =
|
||||
|
||||
selectV :: forall a
|
||||
. (SBool -> Eval a -> Eval a -> Eval a) -- ^ Mux function on @a@s
|
||||
-> WordValue SBool SWord -- ^ Symbolic index value
|
||||
-> WordValue SBool SWord SInteger -- ^ Symbolic index value
|
||||
-> (Integer -> Eval a) -- ^ Function from concrete indices to answers
|
||||
-> Eval a -- ^ overall answer
|
||||
selectV mux val f =
|
||||
case val of
|
||||
WordVal x | Just idx <- SBV.svAsInteger x -> f idx
|
||||
| otherwise -> sel 0 (unpackWord x)
|
||||
BitsVal n xs -> sel 0 . map fromVBit =<< sequence (enumerateSeqMap n xs)
|
||||
BitsVal bs -> sel 0 =<< sequence (Fold.toList bs)
|
||||
LargeBitsVal n xs -> sel 0 . map fromVBit =<< sequence (enumerateSeqMap n xs)
|
||||
|
||||
where
|
||||
sel offset [] = f offset
|
||||
@ -313,7 +328,7 @@ selectV mux val f =
|
||||
|
||||
indexFront :: Maybe Integer
|
||||
-> TValue
|
||||
-> SeqMap SBool SWord
|
||||
-> SeqMap SBool SWord SInteger
|
||||
-> SWord
|
||||
-> Eval Value
|
||||
indexFront mblen a xs idx
|
||||
@ -340,7 +355,7 @@ indexFront mblen a xs idx
|
||||
|
||||
indexBack :: Maybe Integer
|
||||
-> TValue
|
||||
-> SeqMap SBool SWord
|
||||
-> SeqMap SBool SWord SInteger
|
||||
-> SWord
|
||||
-> Eval Value
|
||||
indexBack (Just n) a xs idx = indexFront (Just n) a (reverseSeqMap n xs) idx
|
||||
@ -348,10 +363,10 @@ indexBack Nothing _ _ _ = evalPanic "Expected finite sequence" ["indexBack"]
|
||||
|
||||
indexFront_bits :: Maybe Integer
|
||||
-> TValue
|
||||
-> SeqMap SBool SWord
|
||||
-> [SBool]
|
||||
-> SeqMap SBool SWord SInteger
|
||||
-> Seq.Seq SBool
|
||||
-> Eval Value
|
||||
indexFront_bits mblen a xs bits0 = go 0 (length bits0) bits0
|
||||
indexFront_bits mblen a xs bits0 = go 0 (length bits0) (Fold.toList bits0)
|
||||
where
|
||||
go :: Integer -> Int -> [SBool] -> Eval Value
|
||||
go i _k []
|
||||
@ -374,8 +389,8 @@ indexFront_bits mblen a xs bits0 = go 0 (length bits0) bits0
|
||||
|
||||
indexBack_bits :: Maybe Integer
|
||||
-> TValue
|
||||
-> SeqMap SBool SWord
|
||||
-> [SBool]
|
||||
-> SeqMap SBool SWord SInteger
|
||||
-> Seq.Seq SBool
|
||||
-> Eval Value
|
||||
indexBack_bits (Just n) a xs idx = indexFront_bits (Just n) a (reverseSeqMap n xs) idx
|
||||
indexBack_bits Nothing _ _ _ = evalPanic "Expected finite sequence" ["indexBack_bits"]
|
||||
@ -384,10 +399,10 @@ indexBack_bits Nothing _ _ _ = evalPanic "Expected finite sequence" ["indexBack_
|
||||
updateFrontSym
|
||||
:: Nat'
|
||||
-> TValue
|
||||
-> SeqMap SBool SWord
|
||||
-> WordValue SBool SWord
|
||||
-> Eval (GenValue SBool SWord)
|
||||
-> Eval (SeqMap SBool SWord)
|
||||
-> SeqMap SBool SWord SInteger
|
||||
-> WordValue SBool SWord SInteger
|
||||
-> Eval (GenValue SBool SWord SInteger)
|
||||
-> Eval (SeqMap SBool SWord SInteger)
|
||||
updateFrontSym len _eltTy vs w val = do
|
||||
-- TODO? alternate handling if w is a list of bits...
|
||||
case w of
|
||||
@ -404,10 +419,10 @@ updateFrontSym len _eltTy vs w val = do
|
||||
updateFrontSym_word
|
||||
:: Nat'
|
||||
-> TValue
|
||||
-> WordValue SBool SWord
|
||||
-> WordValue SBool SWord
|
||||
-> Eval (GenValue SBool SWord)
|
||||
-> Eval (WordValue SBool SWord)
|
||||
-> WordValue SBool SWord SInteger
|
||||
-> WordValue SBool SWord SInteger
|
||||
-> Eval (GenValue SBool SWord SInteger)
|
||||
-> Eval (WordValue SBool SWord SInteger)
|
||||
updateFrontSym_word Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateFrontSym_bits"]
|
||||
updateFrontSym_word (Nat _) _eltTy bs w val =
|
||||
selectV (mergeWord' True) w $ \j -> updateWordValue bs j (fromVBit <$> val)
|
||||
@ -415,10 +430,10 @@ updateFrontSym_word (Nat _) _eltTy bs w val =
|
||||
updateBackSym
|
||||
:: Nat'
|
||||
-> TValue
|
||||
-> SeqMap SBool SWord
|
||||
-> WordValue SBool SWord
|
||||
-> Eval (GenValue SBool SWord)
|
||||
-> Eval (SeqMap SBool SWord)
|
||||
-> SeqMap SBool SWord SInteger
|
||||
-> WordValue SBool SWord SInteger
|
||||
-> Eval (GenValue SBool SWord SInteger)
|
||||
-> Eval (SeqMap SBool SWord SInteger)
|
||||
updateBackSym Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateBackSym"]
|
||||
updateBackSym (Nat n) _eltTy vs w val = do
|
||||
-- TODO? alternate handling if w is a list of bits...
|
||||
@ -434,10 +449,10 @@ updateBackSym (Nat n) _eltTy vs w val = do
|
||||
updateBackSym_word
|
||||
:: Nat'
|
||||
-> TValue
|
||||
-> WordValue SBool SWord
|
||||
-> WordValue SBool SWord
|
||||
-> Eval (GenValue SBool SWord)
|
||||
-> Eval (WordValue SBool SWord)
|
||||
-> WordValue SBool SWord SInteger
|
||||
-> WordValue SBool SWord SInteger
|
||||
-> Eval (GenValue SBool SWord SInteger)
|
||||
-> Eval (WordValue SBool SWord SInteger)
|
||||
updateBackSym_word Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateBackSym_bits"]
|
||||
updateBackSym_word (Nat n) _eltTy bs w val = do
|
||||
selectV (mergeWord' True) w $ \j -> updateWordValue bs (n - j - 1) (fromVBit <$> val)
|
||||
@ -450,16 +465,23 @@ asBitList = go id
|
||||
go _ _ = Nothing
|
||||
|
||||
|
||||
asWordList :: [WordValue SBool SWord] -> Maybe [SWord]
|
||||
asWordList :: [WordValue SBool SWord SInteger] -> Maybe [SWord]
|
||||
asWordList = go id
|
||||
where go :: ([SWord] -> [SWord]) -> [WordValue SBool SWord] -> Maybe [SWord]
|
||||
where go :: ([SWord] -> [SWord]) -> [WordValue SBool SWord SInteger] -> Maybe [SWord]
|
||||
go f [] = Just (f [])
|
||||
go f (WordVal x :vs) = go (f . (x:)) vs
|
||||
go _f (BitsVal _ _ : _) = Nothing
|
||||
go f (BitsVal bs:vs) =
|
||||
case asBitList (Fold.toList bs) of
|
||||
Just xs -> go (f . (packWord xs:)) vs
|
||||
Nothing -> Nothing
|
||||
go _f (LargeBitsVal _ _ : _) = Nothing
|
||||
|
||||
liftBinArith :: (SWord -> SWord -> SWord) -> BinArith SWord
|
||||
liftBinArith op _ x y = ready $ op x y
|
||||
|
||||
liftBin :: (a -> b -> c) -> a -> b -> Eval c
|
||||
liftBin op x y = ready $ op x y
|
||||
|
||||
sExp :: Integer -> SWord -> SWord -> Eval SWord
|
||||
sExp _w x y = ready $ go (reverse (unpackWord y)) -- bits in little-endian order
|
||||
where go [] = literalSWord (SBV.intSizeOf x) 1
|
||||
@ -475,6 +497,13 @@ sLg2 _w x = ready $ go 0
|
||||
go i | i < SBV.intSizeOf x = SBV.svIte (SBV.svLessEq x (lit (2^i))) (lit (toInteger i)) (go (i + 1))
|
||||
| otherwise = lit (toInteger i)
|
||||
|
||||
-- | Ceiling (log_2 x)
|
||||
svLg2 :: SInteger -> SInteger
|
||||
svLg2 x =
|
||||
case SBV.svAsInteger x of
|
||||
Just n -> SBV.svInteger SBV.KUnbounded (lg2 n)
|
||||
Nothing -> evalPanic "cannot compute lg2 of symbolic unbounded integer" []
|
||||
|
||||
-- Cmp -------------------------------------------------------------------------
|
||||
|
||||
cmpEq :: SWord -> SWord -> Eval SBool -> Eval SBool
|
||||
@ -498,8 +527,9 @@ cmpGtEq x y k = SBV.svAnd (SBV.svGreaterEq x y) <$> (cmpNotEq x y k)
|
||||
|
||||
cmpBinary :: (SBool -> SBool -> Eval SBool -> Eval SBool)
|
||||
-> (SWord -> SWord -> Eval SBool -> Eval SBool)
|
||||
-> SBool -> Binary SBool SWord
|
||||
cmpBinary fb fw b _ty v1 v2 = VBit <$> cmpValue fb fw v1 v2 (return b)
|
||||
-> (SInteger -> SInteger -> Eval SBool -> Eval SBool)
|
||||
-> SBool -> Binary SBool SWord SInteger
|
||||
cmpBinary fb fw fi b _ty v1 v2 = VBit <$> cmpValue fb fw fi v1 v2 (return b)
|
||||
|
||||
-- Signed arithmetic -----------------------------------------------------------
|
||||
|
||||
|
||||
@ -13,11 +13,12 @@
|
||||
{-# LANGUAGE TypeSynonymInstances #-}
|
||||
{-# OPTIONS_GHC -fno-warn-orphans #-}
|
||||
module Cryptol.Symbolic.Value
|
||||
( SBool, SWord
|
||||
( SBool, SWord, SInteger
|
||||
, literalSWord
|
||||
, fromBitsLE
|
||||
, forallBV_, existsBV_
|
||||
, forallSBool_, existsSBool_
|
||||
, forallSInteger_, existsSInteger_
|
||||
, Value
|
||||
, TValue, isTBit, tvSeq
|
||||
, GenValue(..), lam, tlam, toStream, toFinSeq, toSeq
|
||||
@ -37,12 +38,12 @@ import Data.SBV.Dynamic
|
||||
|
||||
--import Cryptol.Eval.Monad
|
||||
import Cryptol.Eval.Type (TValue(..), isTBit, tvSeq)
|
||||
import Cryptol.Eval.Monad (Eval)
|
||||
import Cryptol.Eval.Monad (Eval, ready)
|
||||
import Cryptol.Eval.Value ( GenValue(..), BitWord(..), lam, tlam, toStream,
|
||||
toFinSeq, toSeq, WordValue(..),
|
||||
fromSeq, fromVBit, fromVWord, fromVFun, fromVPoly,
|
||||
fromVTuple, fromVRecord, lookupRecord, SeqMap(..),
|
||||
ppBV,BV(..),integerToChar, lookupSeqMap,
|
||||
ppBV, BV(..), integerToChar, lookupSeqMap,
|
||||
wordValueSize, asBitsMap)
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
import Cryptol.Utils.PP
|
||||
@ -54,6 +55,7 @@ import Control.Monad.Trans (liftIO)
|
||||
|
||||
type SBool = SVal
|
||||
type SWord = SVal
|
||||
type SInteger = SVal
|
||||
|
||||
fromBitsLE :: [SBool] -> SWord
|
||||
fromBitsLE bs = foldl' f (literalSWord 0 0) bs
|
||||
@ -74,9 +76,15 @@ forallSBool_ = ask >>= liftIO . svMkSymVar (Just ALL) KBool Nothing
|
||||
existsSBool_ :: Symbolic SBool
|
||||
existsSBool_ = ask >>= liftIO . svMkSymVar (Just EX) KBool Nothing
|
||||
|
||||
forallSInteger_ :: Symbolic SBool
|
||||
forallSInteger_ = ask >>= liftIO . svMkSymVar (Just ALL) KUnbounded Nothing
|
||||
|
||||
existsSInteger_ :: Symbolic SBool
|
||||
existsSInteger_ = ask >>= liftIO . svMkSymVar (Just EX) KUnbounded Nothing
|
||||
|
||||
-- Values ----------------------------------------------------------------------
|
||||
|
||||
type Value = GenValue SBool SWord
|
||||
type Value = GenValue SBool SWord SInteger
|
||||
|
||||
-- Symbolic Conditionals -------------------------------------------------------
|
||||
|
||||
@ -96,19 +104,25 @@ mergeBit f c b1 b2 = svSymbolicMerge KBool f c b1 b2
|
||||
|
||||
mergeWord :: Bool
|
||||
-> SBool
|
||||
-> WordValue SBool SWord
|
||||
-> WordValue SBool SWord
|
||||
-> WordValue SBool SWord
|
||||
-> WordValue SBool SWord SInteger
|
||||
-> WordValue SBool SWord SInteger
|
||||
-> WordValue SBool SWord SInteger
|
||||
mergeWord f c (WordVal w1) (WordVal w2) =
|
||||
WordVal $ svSymbolicMerge (kindOf w1) f c w1 w2
|
||||
mergeWord f c (WordVal w1) (BitsVal ys) =
|
||||
BitsVal $ mergeBits f c (Seq.fromList $ map ready $ unpackWord w1) ys
|
||||
mergeWord f c (BitsVal xs) (WordVal w2) =
|
||||
BitsVal $ mergeBits f c xs (Seq.fromList $ map ready $ unpackWord w2)
|
||||
mergeWord f c (BitsVal xs) (BitsVal ys) =
|
||||
BitsVal $ mergeBits f c xs ys
|
||||
mergeWord f c w1 w2 =
|
||||
BitsVal (wordValueSize w1) (mergeSeqMap f c (asBitsMap w1) (asBitsMap w2))
|
||||
LargeBitsVal (wordValueSize w1) (mergeSeqMap f c (asBitsMap w1) (asBitsMap w2))
|
||||
|
||||
mergeWord' :: Bool
|
||||
-> SBool
|
||||
-> Eval (WordValue SBool SWord)
|
||||
-> Eval (WordValue SBool SWord)
|
||||
-> Eval (WordValue SBool SWord)
|
||||
-> Eval (WordValue SBool SWord SInteger)
|
||||
-> Eval (WordValue SBool SWord SInteger)
|
||||
-> Eval (WordValue SBool SWord SInteger)
|
||||
mergeWord' f c x y = mergeWord f c <$> x <*> y
|
||||
|
||||
mergeBits :: Bool
|
||||
@ -119,12 +133,20 @@ mergeBits :: Bool
|
||||
mergeBits f c bs1 bs2 = Seq.zipWith mergeBit' bs1 bs2
|
||||
where mergeBit' b1 b2 = mergeBit f c <$> b1 <*> b2
|
||||
|
||||
mergeInteger :: Bool
|
||||
-> SBool
|
||||
-> SInteger
|
||||
-> SInteger
|
||||
-> SInteger
|
||||
mergeInteger f c x y = svSymbolicMerge KUnbounded f c x y
|
||||
|
||||
mergeValue :: Bool -> SBool -> Value -> Value -> Value
|
||||
mergeValue f c v1 v2 =
|
||||
case (v1, v2) of
|
||||
(VRecord fs1, VRecord fs2) -> VRecord $ zipWith mergeField fs1 fs2
|
||||
(VTuple vs1 , VTuple vs2 ) -> VTuple $ zipWith (\x y -> mergeValue f c <$> x <*> y) vs1 vs2
|
||||
(VBit b1 , VBit b2 ) -> VBit $ mergeBit f c b1 b2
|
||||
(VInteger i1, VInteger i2) -> VInteger $ mergeInteger f c i1 i2
|
||||
(VWord n1 w1, VWord n2 w2 ) | n1 == n2 -> VWord n1 (mergeWord f c <$> w1 <*> w2)
|
||||
(VSeq n1 vs1, VSeq n2 vs2 ) | n1 == n2 -> VSeq n1 $ mergeSeqMap f c vs1 vs2
|
||||
(VStream vs1, VStream vs2) -> VStream $ mergeSeqMap f c vs1 vs2
|
||||
@ -139,13 +161,13 @@ mergeValue f c v1 v2 =
|
||||
[ "mergeValue.mergeField: incompatible values" ]
|
||||
|
||||
|
||||
mergeSeqMap :: Bool -> SBool -> SeqMap SBool SWord -> SeqMap SBool SWord -> SeqMap SBool SWord
|
||||
mergeSeqMap :: Bool -> SBool -> SeqMap SBool SWord SInteger -> SeqMap SBool SWord SInteger -> SeqMap SBool SWord SInteger
|
||||
mergeSeqMap f c x y =
|
||||
IndexSeqMap $ \i -> mergeValue f c <$> lookupSeqMap x i <*> lookupSeqMap y i
|
||||
|
||||
-- Symbolic Big-endian Words -------------------------------------------------------
|
||||
|
||||
instance BitWord SBool SWord where
|
||||
instance BitWord SBool SWord SInteger where
|
||||
wordLen v = toInteger (intSizeOf v)
|
||||
wordAsChar v = integerToChar <$> svAsInteger v
|
||||
|
||||
@ -155,9 +177,13 @@ instance BitWord SBool SWord where
|
||||
ppWord opts v
|
||||
| Just x <- svAsInteger v = ppBV opts (BV (wordLen v) x)
|
||||
| otherwise = text "[?]"
|
||||
ppInteger _opts v
|
||||
| Just x <- svAsInteger v = integer x
|
||||
| otherwise = text "[?]"
|
||||
|
||||
bitLit b = svBool b
|
||||
wordLit n x = svInteger (KBounded False (fromInteger n)) x
|
||||
integerLit x = svInteger KUnbounded x
|
||||
|
||||
wordBit x idx = svTestBit x (intSizeOf x - 1 - fromIntegral idx)
|
||||
|
||||
@ -184,6 +210,23 @@ instance BitWord SBool SWord where
|
||||
wordMinus = svMinus
|
||||
wordMult = svTimes
|
||||
|
||||
wordToInt = svToInteger
|
||||
wordFromInt = svFromInteger
|
||||
|
||||
-- TODO: implement this properly in SBV using "bv2int"
|
||||
svToInteger :: SWord -> SInteger
|
||||
svToInteger w =
|
||||
case svAsInteger w of
|
||||
Nothing -> svFromIntegral KUnbounded w
|
||||
Just x -> svInteger KUnbounded x
|
||||
|
||||
-- TODO: implement this properly in SBV using "int2bv"
|
||||
svFromInteger :: Integer -> SInteger -> SWord
|
||||
svFromInteger n i =
|
||||
case svAsInteger i of
|
||||
Nothing -> svFromIntegral (KBounded False (fromInteger n)) i
|
||||
Just x -> literalSWord (fromInteger n) x
|
||||
|
||||
-- Errors ----------------------------------------------------------------------
|
||||
|
||||
evalPanic :: String -> [String] -> a
|
||||
|
||||
@ -73,7 +73,7 @@ testableType ty =
|
||||
_ -> Nothing
|
||||
|
||||
{- | Given a fully-evaluated type, try to compute the number of values in it.
|
||||
Returns `Nothing` for infinite types, user-defined types, polymorhic types,
|
||||
Returns `Nothing` for infinite types, user-defined types, polymorphic types,
|
||||
and, currently, function spaces. Of course, we can easily compute the
|
||||
sizes of function spaces, but we can't easily enumerate their inhabitants. -}
|
||||
typeSize :: Type -> Maybe Integer
|
||||
@ -87,6 +87,7 @@ typeSize ty =
|
||||
(TCNum _, _) -> Nothing
|
||||
(TCInf, _) -> Nothing
|
||||
(TCBit, _) -> Just 2
|
||||
(TCInteger, _) -> Nothing
|
||||
(TCSeq, [sz,el]) -> case tNoUser sz of
|
||||
TCon (TC (TCNum n)) _ -> (^ n) <$> typeSize el
|
||||
_ -> Nothing
|
||||
@ -114,6 +115,7 @@ typeValues ty =
|
||||
(TCNum _, _) -> []
|
||||
(TCInf, _) -> []
|
||||
(TCBit, _) -> [ VBit False, VBit True ]
|
||||
(TCInteger, _) -> []
|
||||
(TCSeq, ts1) ->
|
||||
case map tNoUser ts1 of
|
||||
[ TCon (TC (TCNum n)) _, TCon (TC TCBit) [] ] ->
|
||||
|
||||
@ -24,7 +24,7 @@ import Data.List (unfoldr, genericTake, genericIndex)
|
||||
import System.Random (RandomGen, split, random, randomR)
|
||||
import qualified Data.Sequence as Seq
|
||||
|
||||
type Gen g b w = Integer -> g -> (GenValue b w, g)
|
||||
type Gen g b w i = Integer -> g -> (GenValue b w i, g)
|
||||
|
||||
|
||||
{- | Apply a testable value to some randomly-generated arguments.
|
||||
@ -36,7 +36,7 @@ type Gen g b w = Integer -> g -> (GenValue b w, g)
|
||||
-}
|
||||
runOneTest :: RandomGen g
|
||||
=> Value -- ^ Function under test
|
||||
-> [Gen g Bool BV] -- ^ Argument generators
|
||||
-> [Gen g Bool BV Integer] -- ^ Argument generators
|
||||
-> Integer -- ^ Size
|
||||
-> g
|
||||
-> IO (Conc.TestResult, g)
|
||||
@ -49,7 +49,7 @@ runOneTest fun argGens sz g0 = do
|
||||
{- | Given a (function) type, compute generators for
|
||||
the function's arguments. Currently we do not support polymorphic functions.
|
||||
In principle, we could apply these to random types, and test the results. -}
|
||||
testableType :: RandomGen g => Type -> Maybe [Gen g Bool BV]
|
||||
testableType :: RandomGen g => Type -> Maybe [Gen g Bool BV Integer]
|
||||
testableType ty =
|
||||
case tNoUser ty of
|
||||
TCon (TC TCFun) [t1,t2] ->
|
||||
@ -62,7 +62,7 @@ testableType ty =
|
||||
|
||||
{- | A generator for values of the given type. This fails if we are
|
||||
given a type that lacks a suitable random value generator. -}
|
||||
randomValue :: (BitWord b w, RandomGen g) => Type -> Maybe (Gen g b w)
|
||||
randomValue :: (BitWord b w i, RandomGen g) => Type -> Maybe (Gen g b w i)
|
||||
randomValue ty =
|
||||
case ty of
|
||||
TCon tc ts ->
|
||||
@ -93,7 +93,7 @@ randomValue ty =
|
||||
return (randomRecord gs)
|
||||
|
||||
-- | Generate a random bit value.
|
||||
randomBit :: (BitWord b w, RandomGen g) => Gen g b w
|
||||
randomBit :: (BitWord b w i, RandomGen g) => Gen g b w i
|
||||
randomBit _ g =
|
||||
let (b,g1) = random g
|
||||
in (VBit (bitLit b), g1)
|
||||
@ -101,20 +101,20 @@ randomBit _ g =
|
||||
-- | Generate a random word of the given length (i.e., a value of type @[w]@)
|
||||
-- The size parameter is assumed to vary between 1 and 100, and we use
|
||||
-- it to generate smaller numbers first.
|
||||
randomWord :: (BitWord b w, RandomGen g) => Integer -> Gen g b w
|
||||
randomWord :: (BitWord b w i, RandomGen g) => Integer -> Gen g b w i
|
||||
randomWord w _sz g =
|
||||
let (val, g1) = randomR (0,2^w-1) g
|
||||
in (VWord w (ready (WordVal (wordLit w val))), g1)
|
||||
|
||||
-- | Generate a random infinite stream value.
|
||||
randomStream :: RandomGen g => Gen g b w -> Gen g b w
|
||||
randomStream :: RandomGen g => Gen g b w i -> Gen g b w i
|
||||
randomStream mkElem sz g =
|
||||
let (g1,g2) = split g
|
||||
in (VStream $ IndexSeqMap $ genericIndex (map ready (unfoldr (Just . mkElem sz) g1)), g2)
|
||||
|
||||
{- | Generate a random sequence. This should be used for sequences
|
||||
other than bits. For sequences of bits use "randomWord". -}
|
||||
randomSequence :: RandomGen g => Integer -> Gen g b w -> Gen g b w
|
||||
randomSequence :: RandomGen g => Integer -> Gen g b w i -> Gen g b w i
|
||||
randomSequence w mkElem sz g0 = do
|
||||
let (g1,g2) = split g0
|
||||
let f g = let (x,g') = mkElem sz g
|
||||
@ -123,7 +123,7 @@ randomSequence w mkElem sz g0 = do
|
||||
seq xs (VSeq w $ IndexSeqMap $ (Seq.index xs . fromInteger), g2)
|
||||
|
||||
-- | Generate a random tuple value.
|
||||
randomTuple :: RandomGen g => [Gen g b w] -> Gen g b w
|
||||
randomTuple :: RandomGen g => [Gen g b w i] -> Gen g b w i
|
||||
randomTuple gens sz = go [] gens
|
||||
where
|
||||
go els [] g = (VTuple (reverse els), g)
|
||||
@ -132,7 +132,7 @@ randomTuple gens sz = go [] gens
|
||||
in seq v (go (ready v : els) more g1)
|
||||
|
||||
-- | Generate a random record value.
|
||||
randomRecord :: RandomGen g => [(Ident, Gen g b w)] -> Gen g b w
|
||||
randomRecord :: RandomGen g => [(Ident, Gen g b w i)] -> Gen g b w i
|
||||
randomRecord gens sz = go [] gens
|
||||
where
|
||||
go els [] g = (VRecord (reverse els), g)
|
||||
|
||||
@ -316,6 +316,7 @@ doCheckType ty k =
|
||||
P.TFun t1 t2 -> tcon (TC TCFun) [t1,t2] k
|
||||
P.TSeq t1 t2 -> tcon (TC TCSeq) [t1,t2] k
|
||||
P.TBit -> tcon (TC TCBit) [] k
|
||||
P.TInteger -> tcon (TC TCInteger) [] k
|
||||
P.TNum n -> tcon (TC (TCNum n)) [] k
|
||||
P.TChar n -> tcon (TC (TCNum $ fromIntegral $ fromEnum n)) [] k
|
||||
P.TInf -> tcon (TC TCInf) [] k
|
||||
|
||||
@ -42,6 +42,9 @@ solveZeroInst ty = case tNoUser ty of
|
||||
-- Zero Bit
|
||||
TCon (TC TCBit) [] -> SolvedIf []
|
||||
|
||||
-- Zero Integer
|
||||
TCon (TC TCInteger) [] -> SolvedIf []
|
||||
|
||||
-- Zero a => Zero [n]a
|
||||
TCon (TC TCSeq) [_, a] -> SolvedIf [ pZero a ]
|
||||
|
||||
@ -100,6 +103,9 @@ solveArithInst ty = case tNoUser ty of
|
||||
TCon (TC TCBit) [] ->
|
||||
Unsolvable $ TCErrorMessage "Arithmetic cannot be done on individual bits."
|
||||
|
||||
-- Arith Integer
|
||||
TCon (TC TCInteger) [] -> SolvedIf []
|
||||
|
||||
-- (Arith a, Arith b) => Arith { x1 : a, x2 : b }
|
||||
TRec fs -> SolvedIf [ pArith ety | (_,ety) <- fs ]
|
||||
|
||||
@ -130,6 +136,9 @@ solveCmpInst ty = case tNoUser ty of
|
||||
-- Cmp Bit
|
||||
TCon (TC TCBit) [] -> SolvedIf []
|
||||
|
||||
-- Cmp Integer
|
||||
TCon (TC TCInteger) [] -> SolvedIf []
|
||||
|
||||
-- (fin n, Cmp a) => Cmp [n]a
|
||||
TCon (TC TCSeq) [n,a] -> SolvedIf [ pFin n, pCmp a ]
|
||||
|
||||
|
||||
@ -14,9 +14,18 @@ import Cryptol.TypeCheck.TypePat
|
||||
import Cryptol.TypeCheck.Solver.Types
|
||||
import Cryptol.TypeCheck.Solver.InfNat
|
||||
import Cryptol.TypeCheck.Solver.Numeric.Interval
|
||||
import Cryptol.TypeCheck.SimpType
|
||||
import Cryptol.TypeCheck.SimpType as Simp
|
||||
|
||||
{- Convention for comments:
|
||||
|
||||
K1, K2 ... Concrete constants
|
||||
s1, s2, t1, t2 ... Arbitrary type expressions
|
||||
a, b, c ... Type variables
|
||||
|
||||
-}
|
||||
|
||||
|
||||
-- | Try to solve @t1 = t2@
|
||||
cryIsEqual :: Ctxt -> Type -> Type -> Solved
|
||||
cryIsEqual ctxt t1 t2 =
|
||||
matchDefault Unsolved $
|
||||
@ -31,12 +40,14 @@ cryIsEqual ctxt t1 t2 =
|
||||
<|> tryEqMulConst t1 t2
|
||||
<|> tryEqAddInf ctxt t1 t2
|
||||
<|> tryAddConst (=#=) t1 t2
|
||||
<|> tryLinearSolution t1 t2
|
||||
<|> tryLinearSolution t2 t1
|
||||
|
||||
|
||||
|
||||
-- | Try to solve @t1 /= t2@
|
||||
cryIsNotEqual :: Ctxt -> Type -> Type -> Solved
|
||||
cryIsNotEqual _i t1 t2 = matchDefault Unsolved (pBin PNeq (/=) t1 t2)
|
||||
|
||||
-- | Try to solve @t1 >= t2@
|
||||
cryIsGeq :: Ctxt -> Type -> Type -> Solved
|
||||
cryIsGeq i t1 t2 =
|
||||
matchDefault Unsolved $
|
||||
@ -53,10 +64,10 @@ cryIsGeq i t1 t2 =
|
||||
-- XXX: width e >= k
|
||||
|
||||
|
||||
-- XXX: max a 10 >= 2 --> True
|
||||
-- XXX: max a 2 >= 10 --> a >= 10
|
||||
|
||||
-- XXX: max t 10 >= 2 --> True
|
||||
-- XXX: max t 2 >= 10 --> a >= 10
|
||||
|
||||
-- | Try to solve something by evalutaion.
|
||||
pBin :: PC -> (Nat' -> Nat' -> Bool) -> Type -> Type -> Match Solved
|
||||
pBin tf p t1 t2 =
|
||||
Unsolvable <$> anError KNum t1
|
||||
@ -73,9 +84,12 @@ pBin tf p t1 t2 =
|
||||
--------------------------------------------------------------------------------
|
||||
-- GEQ
|
||||
|
||||
-- | Try to solve @K >= t@
|
||||
tryGeqKThan :: Ctxt -> Type -> Nat' -> Match Solved
|
||||
tryGeqKThan _ _ Inf = return (SolvedIf [])
|
||||
tryGeqKThan _ ty (Nat n) =
|
||||
|
||||
-- K1 >= K2 * t
|
||||
do (a,b) <- aMul ty
|
||||
m <- aNat' a
|
||||
return $ SolvedIf
|
||||
@ -84,9 +98,12 @@ tryGeqKThan _ ty (Nat n) =
|
||||
Nat 0 -> []
|
||||
Nat k -> [ tNum (div n k) >== b ]
|
||||
|
||||
-- | Try to solve @t >= K@
|
||||
tryGeqThanK :: Ctxt -> Type -> Nat' -> Match Solved
|
||||
tryGeqThanK _ t Inf = return (SolvedIf [ t =#= tInf ])
|
||||
tryGeqThanK _ t (Nat k) =
|
||||
|
||||
-- K1 + t >= K2
|
||||
do (a,b) <- anAdd t
|
||||
n <- aNat a
|
||||
return $ SolvedIf $ if n >= k
|
||||
@ -94,21 +111,24 @@ tryGeqThanK _ t (Nat k) =
|
||||
else [ b >== tNum (k - n) ]
|
||||
|
||||
|
||||
|
||||
tryGeqThanSub :: Ctxt -> Type -> Type -> Match Solved
|
||||
tryGeqThanSub _ x y =
|
||||
|
||||
-- t1 >= t1 - t2
|
||||
do (a,_) <- (|-|) y
|
||||
guard (x == a)
|
||||
return (SolvedIf [])
|
||||
|
||||
tryGeqThanVar :: Ctxt -> Type -> TVar -> Match Solved
|
||||
tryGeqThanVar _ctxt ty x =
|
||||
-- (t + a) >= a
|
||||
do (a,b) <- anAdd ty
|
||||
let check y = do x' <- aTVar y
|
||||
guard (x == x')
|
||||
return (SolvedIf [])
|
||||
check a <|> check b
|
||||
|
||||
-- | Try to prove GEQ by considering the known intervals for the given types.
|
||||
geqByInterval :: Ctxt -> Type -> Type -> Match Solved
|
||||
geqByInterval ctxt x y =
|
||||
let ix = typeInterval ctxt x
|
||||
@ -117,7 +137,7 @@ geqByInterval ctxt x y =
|
||||
(l,Just n) | l >= n -> return (SolvedIf [])
|
||||
_ -> mzero
|
||||
|
||||
|
||||
-- min K1 t >= K2 ~~> t >= K2, if K1 >= K2; Err otherwise
|
||||
tryMinIsGeq :: Type -> Type -> Match Solved
|
||||
tryMinIsGeq t1 t2 =
|
||||
do (a,b) <- aMin t1
|
||||
@ -131,7 +151,7 @@ tryMinIsGeq t1 t2 =
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
|
||||
-- min a b = a ~> a <= b
|
||||
-- min t1 t2 = t1 ~> t1 <= t2
|
||||
tryEqMin :: Type -> Type -> Match Solved
|
||||
tryEqMin x y =
|
||||
do (a,b) <- aMin x
|
||||
@ -143,7 +163,7 @@ tryEqMin x y =
|
||||
tryEqVar :: Type -> TVar -> Match Solved
|
||||
tryEqVar ty x =
|
||||
|
||||
-- x = K + x --> x = inf
|
||||
-- a = K + a --> x = inf
|
||||
(do (k,tv) <- matches ty (anAdd, aNat, aTVar)
|
||||
guard (tv == x && k >= 1)
|
||||
|
||||
@ -151,7 +171,7 @@ tryEqVar ty x =
|
||||
)
|
||||
<|>
|
||||
|
||||
-- x = min (K + x) y --> x = y
|
||||
-- a = min (K + a) t --> a = t
|
||||
(do (l,r) <- aMin ty
|
||||
let check this other =
|
||||
do (k,x') <- matches this (anAdd, aNat', aTVar)
|
||||
@ -160,7 +180,7 @@ tryEqVar ty x =
|
||||
check l r <|> check r l
|
||||
)
|
||||
<|>
|
||||
-- x = K + min a x
|
||||
-- a = K + min t a
|
||||
(do (k,(l,r)) <- matches ty (anAdd, aNat, aMin)
|
||||
guard (k >= 1)
|
||||
let check a b = do x' <- aTVar a
|
||||
@ -178,12 +198,16 @@ tryEqVar ty x =
|
||||
-- e.g., 10 = t
|
||||
tryEqK :: Ctxt -> Type -> Nat' -> Match Solved
|
||||
tryEqK ctxt ty lk =
|
||||
|
||||
-- (t1 + t2 = inf, fin t1) ~~~> t2 = inf
|
||||
do guard (lk == Inf)
|
||||
(a,b) <- anAdd ty
|
||||
let check x y = do guard (iIsFin (typeInterval ctxt x))
|
||||
return $ SolvedIf [ y =#= tInf ]
|
||||
check a b <|> check b a
|
||||
<|>
|
||||
|
||||
-- (K1 + t = K2, K2 >= K1) ~~~> t = (K2 - K1)
|
||||
do (rk, b) <- matches ty (anAdd, aNat', __)
|
||||
return $
|
||||
case nSub lk rk of
|
||||
@ -195,18 +219,30 @@ tryEqK ctxt ty lk =
|
||||
|
||||
Just r -> SolvedIf [ b =#= tNat' r ]
|
||||
<|>
|
||||
|
||||
do (rk, b) <- matches ty (aMul, aNat', __)
|
||||
return $
|
||||
case (lk,rk) of
|
||||
-- Inf * t = Inf ~~~> t >= 1
|
||||
(Inf,Inf) -> SolvedIf [ b >== tOne ]
|
||||
|
||||
-- K * t = Inf ~~~> t = Inf
|
||||
(Inf,Nat _) -> SolvedIf [ b =#= tInf ]
|
||||
|
||||
-- Inf * t = 0 ~~~> t = 0
|
||||
(Nat 0, Inf) -> SolvedIf [ b =#= tZero ]
|
||||
|
||||
-- Inf * t = K ~~~> ERR (K /= 0)
|
||||
(Nat k, Inf) -> Unsolvable
|
||||
$ TCErrorMessage
|
||||
$ show k ++ " /= inf * anything"
|
||||
|
||||
(Nat lk', Nat rk')
|
||||
-- 0 * t = K2 ~~> K2 = 0
|
||||
| rk' == 0 -> SolvedIf [ tNat' lk =#= tZero ]
|
||||
-- shouldn't happen, as `0 * x = x`
|
||||
-- shouldn't happen, as `0 * t = t` should have been simplified
|
||||
|
||||
-- K1 * t = K2 ~~> t = K2/K1
|
||||
| (q,0) <- divMod lk' rk' -> SolvedIf [ b =#= tNum q ]
|
||||
| otherwise ->
|
||||
Unsolvable
|
||||
@ -219,7 +255,7 @@ tryEqK ctxt ty lk =
|
||||
-- 10 = min (2,y) --> impossible
|
||||
|
||||
|
||||
|
||||
-- | K1 * t1 = K2 * t2
|
||||
tryEqMulConst :: Type -> Type -> Match Solved
|
||||
tryEqMulConst l r =
|
||||
do (l1,l2) <- aMul l
|
||||
@ -254,6 +290,7 @@ tryEqMulConst l r =
|
||||
else (SolvedIf [ tMul (tNum lk') l' =#= tMul (tNum rk') r' ])
|
||||
|
||||
|
||||
-- | @(t1 + t2 = Inf, fin t1) ~~> t2 = Inf@
|
||||
tryEqAddInf :: Ctxt -> Type -> Type -> Match Solved
|
||||
tryEqAddInf ctxt l r = check l r <|> check r l
|
||||
where
|
||||
@ -279,6 +316,7 @@ tryEqAddInf ctxt l r = check l r <|> check r l
|
||||
|
||||
|
||||
-- | Check for addition of constants to both sides of a relation.
|
||||
-- @((K1 + K2) + t1) `R` (K1 + t2) ~~> (K2 + t1) `R` t2@
|
||||
--
|
||||
-- This relies on the fact that constants are floated left during
|
||||
-- simplification.
|
||||
@ -293,3 +331,46 @@ tryAddConst rel l r =
|
||||
if k1 > k2
|
||||
then return (SolvedIf [ tAdd (tNum (k1 - k2)) x2 `rel` y2 ])
|
||||
else return (SolvedIf [ x2 `rel` tAdd (tNum (k2 - k1)) y2 ])
|
||||
|
||||
|
||||
-- | Check for situations where a unification variable is involved in
|
||||
-- a sum of terms not containing additional unification variables,
|
||||
-- and replace it with a solution and an inequality.
|
||||
-- @s1 = ?a + s2 ~~> (?a = s1 - s2, s1 >= s2)@
|
||||
tryLinearSolution :: Type -> Type -> Match Solved
|
||||
tryLinearSolution s1 t =
|
||||
do (a,xs) <- matchLinearUnifier t
|
||||
guard (noFreeVariables s1)
|
||||
|
||||
-- NB: matchLinearUnifier only matches if xs is nonempty
|
||||
let s2 = foldr1 Simp.tAdd xs
|
||||
return (SolvedIf [ TVar a =#= (Simp.tSub s1 s2), s1 >== s2 ])
|
||||
|
||||
|
||||
-- | Match a sum of the form @(s1 + ... + ?a + ... sn)@ where
|
||||
-- @s1@ through @sn@ do not contain any free variables.
|
||||
--
|
||||
-- Note: a successful match should only occur if @s1 ... sn@ is
|
||||
-- not empty.
|
||||
matchLinearUnifier :: Pat Type (TVar,[Type])
|
||||
matchLinearUnifier = go []
|
||||
where
|
||||
go xs t =
|
||||
-- Case where a free variable occurs at the end of a sequence of additions.
|
||||
-- NB: match fails if @xs@ is empty
|
||||
do v <- aFreeTVar t
|
||||
guard (not . null $ xs)
|
||||
return (v, xs)
|
||||
<|>
|
||||
-- Next symbol is an addition
|
||||
do (x, y) <- anAdd t
|
||||
|
||||
-- Case where a free variable occurs in the middle of an expression
|
||||
(do v <- aFreeTVar x
|
||||
guard (noFreeVariables y)
|
||||
return (v, reverse (y:xs))
|
||||
|
||||
<|>
|
||||
-- Non-free-variable recursive case
|
||||
do guard (noFreeVariables x)
|
||||
go (x:xs) y)
|
||||
|
||||
@ -34,7 +34,8 @@ import qualified Data.Map as Map
|
||||
import qualified Data.Set as Set
|
||||
import Data.Maybe(catMaybes)
|
||||
import Data.List(partition)
|
||||
import Control.Monad(msum,zipWithM)
|
||||
import Control.Exception
|
||||
import Control.Monad(msum,zipWithM,void)
|
||||
import Data.Char(isSpace)
|
||||
import Text.Read(readMaybe)
|
||||
import qualified System.IO.Strict as StrictIO
|
||||
@ -62,19 +63,17 @@ data Solver = Solver
|
||||
|
||||
-- | Execute a computation with a fresh solver instance.
|
||||
withSolver :: SolverConfig -> (Solver -> IO a) -> IO a
|
||||
withSolver SolverConfig { .. } k =
|
||||
do logger <- if solverVerbose > 0 then SMT.newLogger 0 else return quietLogger
|
||||
|
||||
let smtDbg = if solverVerbose > 1 then Just logger else Nothing
|
||||
solver <- SMT.newSolver solverPath solverArgs smtDbg
|
||||
_ <- SMT.setOptionMaybe solver ":global-decls" "false"
|
||||
-- SMT.setLogic solver "QF_LIA"
|
||||
let sol = Solver { .. }
|
||||
loadTcPrelude sol solverPreludePath
|
||||
a <- k sol
|
||||
_ <- SMT.stop solver
|
||||
|
||||
return a
|
||||
withSolver SolverConfig{ .. } =
|
||||
bracket
|
||||
(do logger <- if solverVerbose > 0 then SMT.newLogger 0 else return quietLogger
|
||||
let smtDbg = if solverVerbose > 1 then Just logger else Nothing
|
||||
solver <- SMT.newSolver solverPath solverArgs smtDbg
|
||||
_ <- SMT.setOptionMaybe solver ":global-decls" "false"
|
||||
-- SMT.setLogic solver "QF_LIA"
|
||||
let sol = Solver { .. }
|
||||
loadTcPrelude sol solverPreludePath
|
||||
return sol)
|
||||
(\s -> void $ SMT.stop (solver s))
|
||||
|
||||
where
|
||||
quietLogger = SMT.Logger { SMT.logMessage = \_ -> return ()
|
||||
|
||||
@ -140,6 +140,7 @@ data PC = PEqual -- ^ @_ == _@
|
||||
data TC = TCNum Integer -- ^ Numbers
|
||||
| TCInf -- ^ Inf
|
||||
| TCBit -- ^ Bit
|
||||
| TCInteger -- ^ Integer
|
||||
| TCSeq -- ^ @[_] _@
|
||||
| TCFun -- ^ @_ -> _@
|
||||
| TCTuple Int -- ^ @(_, _, _)@
|
||||
@ -208,6 +209,7 @@ instance HasKind TC where
|
||||
TCNum _ -> KNum
|
||||
TCInf -> KNum
|
||||
TCBit -> KType
|
||||
TCInteger -> KType
|
||||
TCSeq -> KNum :-> KType :-> KType
|
||||
TCFun -> KType :-> KType :-> KType
|
||||
TCTuple n -> foldr (:->) KType (replicate n KType)
|
||||
@ -400,6 +402,11 @@ tIsBit ty = case tNoUser ty of
|
||||
TCon (TC TCBit) [] -> True
|
||||
_ -> False
|
||||
|
||||
tIsInteger :: Type -> Bool
|
||||
tIsInteger ty = case tNoUser ty of
|
||||
TCon (TC TCInteger) [] -> True
|
||||
_ -> False
|
||||
|
||||
tIsTuple :: Type -> Maybe [Type]
|
||||
tIsTuple ty = case tNoUser ty of
|
||||
TCon (TC (TCTuple _)) ts -> Just ts
|
||||
@ -494,6 +501,9 @@ tNat' n' = case n' of
|
||||
tBit :: Type
|
||||
tBit = TCon (TC TCBit) []
|
||||
|
||||
tInteger :: Type
|
||||
tInteger = TCon (TC TCInteger) []
|
||||
|
||||
tWord :: Type -> Type
|
||||
tWord a = tSeq a tBit
|
||||
|
||||
@ -655,6 +665,8 @@ pError msg = TCon (TError KProp msg) []
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
noFreeVariables :: FVS t => t -> Bool
|
||||
noFreeVariables = all (not . isFreeTV) . Set.toList . fvs
|
||||
|
||||
class FVS t where
|
||||
fvs :: t -> Set TVar
|
||||
@ -769,6 +781,7 @@ instance PP (WithNames Type) where
|
||||
(TCNum n, []) -> integer n
|
||||
(TCInf, []) -> text "inf"
|
||||
(TCBit, []) -> text "Bit"
|
||||
(TCInteger, []) -> text "Integer"
|
||||
|
||||
(TCSeq, [t1,TCon (TC TCBit) []]) -> brackets (go 0 t1)
|
||||
(TCSeq, [t1,t2]) -> optParens (prec > 3)
|
||||
@ -873,6 +886,7 @@ instance PP TC where
|
||||
TCNum n -> integer n
|
||||
TCInf -> text "inf"
|
||||
TCBit -> text "Bit"
|
||||
TCInteger -> text "Integer"
|
||||
TCSeq -> text "[]"
|
||||
TCFun -> text "(->)"
|
||||
TCTuple 0 -> text "()"
|
||||
|
||||
@ -7,6 +7,7 @@ module Cryptol.TypeCheck.TypePat
|
||||
, aLenFromThen, aLenFromThenTo
|
||||
|
||||
, aTVar
|
||||
, aFreeTVar
|
||||
, aBit
|
||||
, aSeq
|
||||
, aWord
|
||||
@ -112,6 +113,12 @@ aTVar = \a -> case tNoUser a of
|
||||
TVar x -> return x
|
||||
_ -> mzero
|
||||
|
||||
aFreeTVar :: Pat Type TVar
|
||||
aFreeTVar t =
|
||||
do v <- aTVar t
|
||||
guard (isFreeTV v)
|
||||
return v
|
||||
|
||||
aBit :: Pat Type ()
|
||||
aBit = tc TCBit ar0
|
||||
|
||||
|
||||
50
tests/issues/Karatsuba.cry
Normal file
50
tests/issues/Karatsuba.cry
Normal file
@ -0,0 +1,50 @@
|
||||
module Karatsuba where
|
||||
|
||||
kmult : {limb,n} (fin n, fin limb, limb >= 6, n>=1) => [n] -> [n] -> [2*n]
|
||||
kmult x y =
|
||||
if `n <= (demote`{limb, max (width limb) (width n)}) then
|
||||
(zero#x)*(zero#y)
|
||||
else
|
||||
take (splitmult`{limb} (make_atleast`{limb} x) (make_atleast`{limb} y))
|
||||
|
||||
make_atleast : {n, m, a} (fin n, fin m, Zero a) => [m]a -> [max n m]a
|
||||
make_atleast x = zero#x
|
||||
|
||||
splitmult : {limb,n} (fin n, fin limb, limb >= 6, n>=6)
|
||||
=> [n] -> [n] -> [2*n]
|
||||
|
||||
splitmult x y = (ac # bd) + (zero # ad_bc # (zero:[low]))
|
||||
where
|
||||
type hi = n/2
|
||||
type low = n - hi
|
||||
|
||||
(a,b) = splitAt`{hi} x
|
||||
(c,d) = splitAt`{hi} y
|
||||
|
||||
ac : [2*hi]
|
||||
ac = kmult`{limb,hi} a c
|
||||
|
||||
bd : [2*low]
|
||||
bd = kmult`{limb,low} b d
|
||||
|
||||
a_b = (zext a) + (zext b)
|
||||
c_d = (zext c) + (zext d)
|
||||
|
||||
ad_bc : [2*(low+1)]
|
||||
ad_bc = (kmult`{limb,low+1} a_b c_d) - (zext ac) - (zext bd)
|
||||
|
||||
|
||||
property splitmult_correct_tiny (x:[9]) (y:[9]) =
|
||||
zext x * zext y == splitmult`{limb=7} x y
|
||||
|
||||
property splitmult_correct_small (x:[11]) (y:[11]) =
|
||||
zext x * zext y == splitmult`{limb=7} x y
|
||||
|
||||
property splitmult_correct_medium(x:[17]) (y:[17]) =
|
||||
zext x * zext y == splitmult`{limb=7} x y
|
||||
|
||||
property splitmult_correct_large (x:[59]) (y:[59]) =
|
||||
zext x * zext y == splitmult`{limb=7} x y
|
||||
|
||||
property splitmult_correct_huge (x:[511]) (y:[511]) =
|
||||
zext x * zext y == splitmult`{limb=63} x y
|
||||
@ -1 +1,2 @@
|
||||
Known problem. See #146.
|
||||
See also #323, which seems to be another instance of the same problem.
|
||||
|
||||
@ -11,7 +11,7 @@ property t2 Using random testing.
|
||||
testing...passed 100 tests.
|
||||
Coverage: 0.00% (100 of 2^^64 values)
|
||||
property f0 Using exhaustive testing.
|
||||
testing...FAILED
|
||||
testing...f0 = False
|
||||
:prove t0
|
||||
Q.E.D.
|
||||
:prove t1
|
||||
|
||||
@ -1 +0,0 @@
|
||||
Known tc failure. See issue #212.
|
||||
@ -0,0 +1,3 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
@ -58,6 +58,7 @@ Symbols
|
||||
back]elem -> [back]elem
|
||||
error : {at, len} (fin len) => [len][8] -> at
|
||||
foo : {a} a -> a
|
||||
fromInteger : {a} (fin a) => Integer -> [a]
|
||||
fromThen : {first, next, bits, len} (fin first, fin next, fin bits,
|
||||
bits >= width first, bits >= width next,
|
||||
lengthFromThen first next bits == len) => [len][bits]
|
||||
@ -72,6 +73,7 @@ Symbols
|
||||
parts]elem -> [parts][each]elem
|
||||
infFrom : {bits} (fin bits) => [bits] -> [inf][bits]
|
||||
infFromThen : {bits} (fin bits) => [bits] -> [bits] -> [inf][bits]
|
||||
integer : {val} (fin val) => Integer
|
||||
join : {parts, each, a} (fin each) => [parts][each]a -> [parts *
|
||||
each]a
|
||||
lg2 : {a} (Arith a) => a -> a
|
||||
@ -94,6 +96,7 @@ Symbols
|
||||
tail : {a, b} [1 + a]b -> [a]b
|
||||
take : {front, back, elem} (fin front) => [front +
|
||||
back]elem -> [front]elem
|
||||
toInteger : {a} (fin a) => [a] -> Integer
|
||||
trace : {n, a, b} (fin n) => [n][8] -> a -> b -> b
|
||||
traceVal : {n, a} (fin n) => [n][8] -> a -> a
|
||||
transpose : {a, b, c} [a][b]c -> [b][a]c
|
||||
|
||||
@ -4,7 +4,7 @@ Loading module Main
|
||||
|
||||
[error] at ./issue290v2.cry:2:1--2:19:
|
||||
Unsolved constraints:
|
||||
a`356 == 1
|
||||
a`359 == 1
|
||||
arising from
|
||||
checking a pattern: type of 1st argument of Main::minMax
|
||||
at ./issue290v2.cry:2:8--2:11
|
||||
|
||||
3
tests/issues/issue325.icry
Normal file
3
tests/issues/issue325.icry
Normal file
@ -0,0 +1,3 @@
|
||||
:set tests=100
|
||||
:l Karatsuba.cry
|
||||
:check splitmult_correct_large
|
||||
6
tests/issues/issue325.icry.stdout
Normal file
6
tests/issues/issue325.icry.stdout
Normal file
@ -0,0 +1,6 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Karatsuba
|
||||
Using random testing.
|
||||
testing...passed 100 tests.
|
||||
Coverage: 0.00% (100 of 2^^118 values)
|
||||
7
tests/issues/issue389.cry
Normal file
7
tests/issues/issue389.cry
Normal file
@ -0,0 +1,7 @@
|
||||
pad : {n, m, b} (64>=width(n), b==512-((n+65)%512), m==65+n+b) => [n]->[m]
|
||||
pad message = (message#[True])#(0:[b])#sz
|
||||
where
|
||||
sz : [64]
|
||||
sz = width message
|
||||
|
||||
test = pad
|
||||
3
tests/issues/issue389.icry
Normal file
3
tests/issues/issue389.icry
Normal file
@ -0,0 +1,3 @@
|
||||
:l issue389.cry
|
||||
pad (join "a")
|
||||
test (join "a")
|
||||
5
tests/issues/issue389.icry.stdout
Normal file
5
tests/issues/issue389.icry.stdout
Normal file
@ -0,0 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
0x61800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000008
|
||||
0x61800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000008
|
||||
6
tests/issues/issue78.cry
Normal file
6
tests/issues/issue78.cry
Normal file
@ -0,0 +1,6 @@
|
||||
unique : {a,b} (fin a, fin b, a>=1) => [a][b] -> Bit
|
||||
unique xs = [ exist x (i+1) | x <- xs | i <- [0..(a-1)] ] == 0
|
||||
where exist : [b] -> [width a] -> Bit
|
||||
exist x i = if(i>=`a) then False
|
||||
else if(x==(xs@i)) then True
|
||||
else exist x (i+1)
|
||||
2
tests/issues/issue78.icry
Normal file
2
tests/issues/issue78.icry
Normal file
@ -0,0 +1,2 @@
|
||||
:l issue78.cry
|
||||
:t unique
|
||||
4
tests/issues/issue78.icry.stdout
Normal file
4
tests/issues/issue78.icry.stdout
Normal file
@ -0,0 +1,4 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
unique : {a, b} (fin a, fin b, a >= 1) => [a][b] -> Bit
|
||||
@ -25,8 +25,8 @@ Loading module test04
|
||||
[error] at ./test04.cry:3:19--3:21:
|
||||
Type mismatch:
|
||||
Expected type: ()
|
||||
Inferred type: [?g14]
|
||||
Inferred type: [?j14]
|
||||
where
|
||||
?g14 is type parameter 'bits'
|
||||
?j14 is type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./test04.cry:3:19--3:21
|
||||
|
||||
Loading…
Reference in New Issue
Block a user