GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-05 23:17:42 +03:00
Code Issues Projects Releases Wiki Activity

Enforce a canonical field ordering in the field type constructor for FinType

Browse Source 
This solves another manifestation of issue #702.
This commit is contained in:
Rob Dockins 2020-04-17 15:14:36 -07:00
parent 194d02d06d
commit 9434236cbd
2 changed files with 7 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/Cryptol/Symbolic.hs
View File

@ -41,7 +41,7 @@ import Cryptol.Utils.PP
import Prelude ()
import Prelude.Compat
import qualified Data.Map as Map
import Data.Time (NominalDiffTime)
type SatResult = [(Type, Expr, Concrete.Value)]
@ -105,7 +105,7 @@ data FinType
| FTIntMod Integer
| FTSeq Int FinType
| FTTuple [FinType]
| FTRecord [(Ident, FinType)]
| FTRecord (Map.Map Ident FinType)
numType :: Integer -> Maybe Int
numType n
@ -123,7 +123,7 @@ finType ty =
TVIntMod n -> Just (FTIntMod n)
TVSeq n t -> FTSeq <$> numType n <*> finType t
TVTuple ts -> FTTuple <$> traverse finType ts
TVRec fields -> FTRecord <$> traverse (traverseSnd finType) fields
TVRec fields -> FTRecord . Map.fromList <$> traverse (traverseSnd finType) fields
TVAbstract {} -> Nothing
_ -> Nothing
@ -135,7 +135,4 @@ unFinType fty =
FTIntMod n -> tIntMod (tNum n)
FTSeq l ety -> tSeq (tNum l) (unFinType ety)
FTTuple ftys -> tTuple (unFinType <$> ftys)
FTRecord fs -> tRec (zip fns tys)
where
fns = fst <$> fs
tys = unFinType . snd <$> fs
FTRecord fs -> tRec (Map.toList (fmap unFinType fs))

6
src/Cryptol/Symbolic/SBV.hs
View File

@ -274,7 +274,7 @@ parseValue (FTSeq n t) cvs =
parseValue (FTTuple ts) cvs = (Eval.VTuple (map Eval.ready vs), cvs')
where (vs, cvs') = parseValues ts cvs
parseValue (FTRecord fs) cvs = (Eval.VRecord (Map.fromList (zip ns (map Eval.ready vs))), cvs')
where (ns, ts) = unzip fs
where (ns, ts) = unzip (Map.toList fs)
(vs, cvs') = parseValues ts cvs
inBoundsIntMod :: Integer -> Eval.SInteger SBV -> Eval.SBit SBV
@ -296,7 +296,7 @@ forallFinType ty =
FTSeq n t -> do vs <- replicateM n (forallFinType t)
return $ Eval.VSeq (toInteger n) $ Eval.finiteSeqMap SBV (map pure vs)
FTTuple ts -> Eval.VTuple <$> mapM (fmap pure . forallFinType) ts
FTRecord fs -> Eval.VRecord <$> mapM (fmap pure . forallFinType) (Map.fromList fs)
FTRecord fs -> Eval.VRecord <$> mapM (fmap pure . forallFinType) fs
existsFinType :: FinType -> WriterT [Eval.SBit SBV] SBV.Symbolic Value
existsFinType ty =
@ -311,4 +311,4 @@ existsFinType ty =
FTSeq n t -> do vs <- replicateM n (existsFinType t)
return $ Eval.VSeq (toInteger n) $ Eval.finiteSeqMap SBV (map pure vs)
FTTuple ts -> Eval.VTuple <$> mapM (fmap pure . existsFinType) ts
FTRecord fs -> Eval.VRecord <$> mapM (fmap pure . existsFinType) (Map.fromList fs)
FTRecord fs -> Eval.VRecord <$> mapM (fmap pure . existsFinType) fs