GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-28 09:23:04 +03:00
Code Issues Projects Releases Wiki Activity

Merge module Cryptol.Symbolic.BitVector into Cryptol.Symbolic.Value

Browse Source
This commit is contained in:
Brian Huffman 2015-04-09 10:57:42 -07:00 committed by Adam C. Foltzer
parent c710239bdb
commit ba91e37a5d
5 changed files with 38 additions and 57 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
cryptol.cabal
View File

@ -138,7 +138,6 @@ library
Cryptol.Testing.Random,
Cryptol.Symbolic,
Cryptol.Symbolic.BitVector,
Cryptol.Symbolic.Prims,
Cryptol.Symbolic.Value,

1
src/Cryptol/Symbolic.hs
View File

@ -27,7 +27,6 @@ import qualified Data.SBV.Dynamic as SBV
import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem.Env as M
import Cryptol.Symbolic.BitVector
import Cryptol.Symbolic.Prims
import Cryptol.Symbolic.Value

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

@ -1,48 +0,0 @@
-- |
-- Module : $Header$
-- Copyright : (c) 2013-2015 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ViewPatterns #-}
module Cryptol.Symbolic.BitVector
( SBool, SWord
, literalSWord
, fromBitsLE
, forallBV_, existsBV_
, forallSBool_, existsSBool_
) where
import Data.List (foldl')
import Data.SBV.Dynamic
type SBool = SVal
type SWord = SVal
fromBitsLE :: [SVal] -> SWord
fromBitsLE bs = foldl' f (literalSWord 0 0) bs
where f w b = svJoin (svToWord1 b) w
literalSWord :: Int -> Integer -> SWord
literalSWord w i = svInteger (KBounded False w) i
forallBV_ :: Int -> Symbolic SWord
forallBV_ w = svMkSymVar (Just ALL) (KBounded False w) Nothing
existsBV_ :: Int -> Symbolic SWord
existsBV_ w = svMkSymVar (Just EX) (KBounded False w) Nothing
forallSBool_ :: Symbolic SBool
forallSBool_ = svMkSymVar (Just ALL) KBool Nothing
existsSBool_ :: Symbolic SBool
existsSBool_ = svMkSymVar (Just EX) KBool Nothing

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

@ -18,7 +18,6 @@ import Data.Ord (comparing)
import Cryptol.Eval.Value (BitWord(..))
import Cryptol.Prims.Eval (binary, unary, tlamN)
import Cryptol.Prims.Syntax (ECon(..))
import Cryptol.Symbolic.BitVector
import Cryptol.Symbolic.Value
import Cryptol.TypeCheck.AST (Name)
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..), nMul)

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

@ -12,7 +12,12 @@
{-# LANGUAGE TypeSynonymInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Cryptol.Symbolic.Value
( Value
( SBool, SWord
, literalSWord
, fromBitsLE
, forallBV_, existsBV_
, forallSBool_, existsSBool_
, Value
, TValue, numTValue, toNumTValue, finTValue, isTBit, isTFun, isTSeq, isTTuple, isTRec, tvSeq
, GenValue(..), lam, tlam, toStream, toFinSeq, toSeq
, fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord
@ -22,14 +27,41 @@ module Cryptol.Symbolic.Value
)
where
import Cryptol.Eval.Value (TValue, numTValue, toNumTValue, finTValue, isTBit, isTFun, isTSeq, isTTuple, isTRec, tvSeq,
GenValue(..), BitWord(..), lam, tlam, toStream, toFinSeq, toSeq, fromSeq,
fromVBit, fromVWord, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord)
import Cryptol.Symbolic.BitVector
import Cryptol.Utils.Panic (panic)
import Data.List (foldl')
import Data.SBV.Dynamic
import Cryptol.Eval.Value (TValue, numTValue, toNumTValue, finTValue, isTBit,
isTFun, isTSeq, isTTuple, isTRec, tvSeq, GenValue(..),
BitWord(..), lam, tlam, toStream, toFinSeq, toSeq,
fromSeq, fromVBit, fromVWord, fromVFun, fromVPoly,
fromVTuple, fromVRecord, lookupRecord)
import Cryptol.Utils.Panic (panic)
-- SBool and SWord -------------------------------------------------------------
type SBool = SVal
type SWord = SVal
fromBitsLE :: [SBool] -> SWord
fromBitsLE bs = foldl' f (literalSWord 0 0) bs
where f w b = svJoin (svToWord1 b) w
literalSWord :: Int -> Integer -> SWord
literalSWord w i = svInteger (KBounded False w) i
forallBV_ :: Int -> Symbolic SWord
forallBV_ w = svMkSymVar (Just ALL) (KBounded False w) Nothing
existsBV_ :: Int -> Symbolic SWord
existsBV_ w = svMkSymVar (Just EX) (KBounded False w) Nothing
forallSBool_ :: Symbolic SBool
forallSBool_ = svMkSymVar (Just ALL) KBool Nothing
existsSBool_ :: Symbolic SBool
existsSBool_ = svMkSymVar (Just EX) KBool Nothing
-- Values ----------------------------------------------------------------------
type Value = GenValue SBool SWord