From c1bdd77ff0979c65e5a9a11a13365ff3a5dce1c0 Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Tue, 2 Jun 2020 15:00:25 -0700 Subject: [PATCH] Add SMT Array primitives. (#732) * Add SMT Array primitives. * Move SMT Array primitives in Array.cry. * Minor. --- lib/Array.cry | 15 +++++++++++++++ src/Cryptol/Eval.hs | 1 + src/Cryptol/Eval/Generic.hs | 15 +++++++++++++++ src/Cryptol/Eval/Reference.lhs | 15 +++++++++++++++ src/Cryptol/Eval/Type.hs | 3 +++ src/Cryptol/ModuleSystem/Base.hs | 5 +++-- src/Cryptol/ModuleSystem/Name.hs | 6 +++++- src/Cryptol/Prelude.hs | 9 ++++++++- src/Cryptol/Testing/Random.hs | 2 ++ src/Cryptol/TypeCheck/TCon.hs | 9 +++++++++ src/Cryptol/TypeCheck/Type.hs | 3 +++ src/Cryptol/Utils/Ident.hs | 4 ++++ 12 files changed, 83 insertions(+), 4 deletions(-) create mode 100644 lib/Array.cry diff --git a/lib/Array.cry b/lib/Array.cry new file mode 100644 index 00000000..c455395d --- /dev/null +++ b/lib/Array.cry @@ -0,0 +1,15 @@ +/* + * Copyright (c) 2020 Galois, Inc. + * Distributed under the terms of the BSD3 license (see LICENSE file) + */ + +/** The type and operations of the theory of arrays. */ + +module Array where + +primitive type Array : * -> * -> * + +primitive arrayConstant : {a, b} b -> (Array a b) +primitive arrayLookup : {a, b} (Array a b) -> a -> b +primitive arrayUpdate : {a, b} (Array a b) -> a -> b -> (Array a b) + diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs index b73caa58..c104155b 100644 --- a/src/Cryptol/Eval.hs +++ b/src/Cryptol/Eval.hs @@ -426,6 +426,7 @@ etaDelay sym msg env0 Forall{ sVars = vs0, sType = tp0 } = goTpVars env0 vs0 TVBit -> v TVInteger -> v TVIntMod _ -> v + TVArray{} -> v TVSeq n TVBit -> do w <- sDelayFill sym (fromWordVal "during eta-expansion" =<< v) (etaWord sym n v) diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs index 89ae000b..0533b0b8 100644 --- a/src/Cryptol/Eval/Generic.hs +++ b/src/Cryptol/Eval/Generic.hs @@ -164,6 +164,9 @@ arithBinary sym opw opi opz = loop TVIntMod n -> VInteger <$> opz n (fromVInteger l) (fromVInteger r) + TVArray{} -> + evalPanic "arithBinary" ["Array not in class Arith"] + TVSeq w a -- words and finite sequences | isTBit a -> do @@ -235,6 +238,9 @@ arithUnary sym opw opi opz = loop TVIntMod n -> VInteger <$> opz n (fromVInteger v) + TVArray{} -> + evalPanic "arithUnary" ["Array not in class Arith"] + TVSeq w a -- words and finite sequences | isTBit a -> do @@ -292,6 +298,8 @@ arithNullary sym opw opi opz = loop TVIntMod n -> VInteger <$> opz n + TVArray{} -> evalPanic "arithNullary" ["Array not in class Arith"] + TVSeq w a -- words and finite sequences | isTBit a -> pure $ VWord w $ (WordVal <$> opw w) @@ -445,6 +453,8 @@ cmpValue sym fb fw fi fz = cmp TVBit -> fb (fromVBit v1) (fromVBit v2) k TVInteger -> fi (fromVInteger v1) (fromVInteger v2) k TVIntMod n -> fz n (fromVInteger v1) (fromVInteger v2) k + TVArray{} -> panic "Cryptol.Prims.Value.cmpValue" + [ "Arrays are not comparable" ] TVSeq n t | isTBit t -> do w1 <- fromVWord sym "cmpValue" v1 w2 <- fromVWord sym "cmpValue" v2 @@ -608,6 +618,8 @@ zeroV sym ty = case ty of TVIntMod _ -> VInteger <$> integerLit sym 0 + TVArray{} -> evalPanic "zeroV" ["Array not in class Zero"] + -- sequences TVSeq w ety | isTBit ety -> pure $ word sym w 0 @@ -1010,6 +1022,7 @@ logicBinary sym opb opw = loop TVBit -> VBit <$> (opb (fromVBit l) (fromVBit r)) TVInteger -> evalPanic "logicBinary" ["Integer not in class Logic"] TVIntMod _ -> evalPanic "logicBinary" ["Z not in class Logic"] + TVArray{} -> evalPanic "logicBinary" ["Array not in class Logic"] TVSeq w aty -- words | isTBit aty @@ -1085,6 +1098,7 @@ logicUnary sym opb opw = loop TVInteger -> evalPanic "logicUnary" ["Integer not in class Logic"] TVIntMod _ -> evalPanic "logicUnary" ["Z not in class Logic"] + TVArray{} -> evalPanic "logicUnary" ["Array not in class Logic"] TVSeq w ety -- words @@ -1420,6 +1434,7 @@ errorV sym ty msg = case ty of TVBit -> cryUserError sym msg TVInteger -> cryUserError sym msg TVIntMod _ -> cryUserError sym msg + TVArray{} -> cryUserError sym msg -- sequences TVSeq w ety diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs index af117e07..11e0eba0 100644 --- a/src/Cryptol/Eval/Reference.lhs +++ b/src/Cryptol/Eval/Reference.lhs @@ -66,6 +66,7 @@ are as follows: |:----------------- |:-------------- |:--------------------------- | | `Bit` | booleans | `TVBit` | | `Integer` | integers | `TVInteger` | +| `Array` | arrays | `TVArray` | | `[n]a` | finite lists | `TVSeq n a` | | `[inf]a` | infinite lists | `TVStream a` | | `(a, b, c)` | tuples | `TVTuple [a,b,c]` | @@ -171,6 +172,7 @@ cpo that represents any given schema. > TVBit -> VBit (fromVBit val) > TVInteger -> VInteger (fromVInteger val) > TVIntMod _ -> VInteger (fromVInteger val) +> TVArray{} -> evalPanic "copyByTValue" ["Unsupported Array type"] > TVSeq w ety -> VList (Nat w) (map (go ety) (copyList w (fromVList val))) > TVStream ety -> VList Inf (map (go ety) (copyStream (fromVList val))) > TVTuple etys -> VTuple (zipWith go etys (copyList (genericLength etys) (fromVTuple val))) @@ -751,6 +753,7 @@ at the same positions. > go TVBit = VBit b > go TVInteger = VInteger (fmap (\c -> if c then -1 else 0) b) > go (TVIntMod _) = VInteger (fmap (const 0) b) +> go (TVArray{}) = evalPanic "logicNullary" ["Array not in class Logic"] > go (TVSeq n ety) = VList (Nat n) (genericReplicate n (go ety)) > go (TVStream ety) = VList Inf (repeat (go ety)) > go (TVTuple tys) = VTuple (map go tys) @@ -768,6 +771,7 @@ at the same positions. > TVBit -> VBit (fmap op (fromVBit val)) > TVInteger -> evalPanic "logicUnary" ["Integer not in class Logic"] > TVIntMod _ -> evalPanic "logicUnary" ["Z not in class Logic"] +> TVArray{} -> evalPanic "logicUnary" ["Array not in class Logic"] > TVSeq w ety -> VList (Nat w) (map (go ety) (fromVList val)) > TVStream ety -> VList Inf (map (go ety) (fromVList val)) > TVTuple etys -> VTuple (zipWith go etys (fromVTuple val)) @@ -785,6 +789,7 @@ at the same positions. > TVBit -> VBit (liftA2 op (fromVBit l) (fromVBit r)) > TVInteger -> evalPanic "logicBinary" ["Integer not in class Logic"] > TVIntMod _ -> evalPanic "logicBinary" ["Z not in class Logic"] +> TVArray{} -> evalPanic "logicBinary" ["Array not in class Logic"] > TVSeq w ety -> VList (Nat w) (zipWith (go ety) (fromVList l) (fromVList r)) > TVStream ety -> VList Inf (zipWith (go ety) (fromVList l) (fromVList r)) > TVTuple etys -> VTuple (zipWith3 go etys (fromVTuple l) (fromVTuple r)) @@ -819,6 +824,8 @@ up of non-empty finite bitvectors. > VInteger i > TVIntMod n -> > VInteger (flip mod n <$> i) +> TVArray{} -> +> evalPanic "arithNullary" ["Array not in class Arith"] > TVSeq w a > | isTBit a -> vWord w i > | otherwise -> VList (Nat w) (genericReplicate w (go a)) @@ -852,6 +859,8 @@ up of non-empty finite bitvectors. > case fromVInteger val of > Left e -> Left e > Right i -> flip mod n <$> op i +> TVArray{} -> +> evalPanic "arithUnary" ["Array not in class Arith"] > TVSeq w a > | isTBit a -> vWord w (op =<< fromVWord val) > | otherwise -> VList (Nat w) (map (go a) (fromVList val)) @@ -900,6 +909,8 @@ up of non-empty finite bitvectors. > case fromVInteger r of > Left e -> Left e > Right j -> flip mod n <$> op i j +> TVArray{} -> +> evalPanic "arithBinary" ["Array not in class Arith"] > TVSeq w a > | isTBit a -> vWord w $ > case fromWord l of @@ -968,6 +979,8 @@ bits to the *left* of that position are equal. > compare <$> fromVInteger l <*> fromVInteger r > TVIntMod _ -> > compare <$> fromVInteger l <*> fromVInteger r +> TVArray{} -> +> evalPanic "lexCompare" ["invalid type"] > TVSeq _w ety -> > lexList (zipWith (lexCompare ety) (fromVList l) (fromVList r)) > TVStream _ -> @@ -1011,6 +1024,8 @@ fields are compared in alphabetical order. > evalPanic "lexSignedCompare" ["invalid type"] > TVIntMod _ -> > evalPanic "lexSignedCompare" ["invalid type"] +> TVArray{} -> +> evalPanic "lexSignedCompare" ["invalid type"] > TVSeq _w ety > | isTBit ety -> > case fromSignedVWord l of diff --git a/src/Cryptol/Eval/Type.hs b/src/Cryptol/Eval/Type.hs index 9206b0d9..70d195bb 100644 --- a/src/Cryptol/Eval/Type.hs +++ b/src/Cryptol/Eval/Type.hs @@ -30,6 +30,7 @@ data TValue = TVBit -- ^ @ Bit @ | TVInteger -- ^ @ Integer @ | TVIntMod Integer -- ^ @ Z n @ + | TVArray TValue TValue -- ^ @ Array a b @ | TVSeq Integer TValue -- ^ @ [n]a @ | TVStream TValue -- ^ @ [inf]t @ | TVTuple [TValue] -- ^ @ (a, b, c )@ @@ -45,6 +46,7 @@ tValTy tv = TVBit -> tBit TVInteger -> tInteger TVIntMod n -> tIntMod (tNum n) + TVArray a b -> tArray (tValTy a) (tValTy b) TVSeq n t -> tSeq (tNum n) (tValTy t) TVStream t -> tSeq tInf (tValTy t) TVTuple ts -> tTuple (map tValTy ts) @@ -105,6 +107,7 @@ evalType env ty = (TCIntMod, [n]) -> case num n of Inf -> evalPanic "evalType" ["invalid type Z inf"] Nat m -> Right $ TVIntMod m + (TCArray, [a, b]) -> Right $ TVArray (val a) (val b) (TCSeq, [n, t]) -> Right $ tvSeq (num n) (val t) (TCFun, [a, b]) -> Right $ TVFun (val a) (val b) (TCTuple _, _) -> Right $ TVTuple (map val ts) diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 857c8d45..5fc49454 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -42,14 +42,14 @@ import qualified Cryptol.TypeCheck.AST as T import qualified Cryptol.TypeCheck.PP as T import qualified Cryptol.TypeCheck.Sanity as TcSanity import Cryptol.Transform.AddModParams (addModParams) -import Cryptol.Utils.Ident (preludeName, interactiveName +import Cryptol.Utils.Ident (preludeName, arrayName, interactiveName , modNameChunks, notParamInstModName , isParamInstModName ) import Cryptol.Utils.PP (pretty) import Cryptol.Utils.Panic (panic) import Cryptol.Utils.Logger(logPutStrLn, logPrint) -import Cryptol.Prelude (preludeContents) +import Cryptol.Prelude (preludeContents, arrayContents) import Cryptol.Transform.MonoValues (rewModule) @@ -259,6 +259,7 @@ findModule n = do handleNotFound = case n of m | m == preludeName -> pure (InMem "Cryptol" preludeContents) + | m == arrayName -> pure (InMem "Array" arrayContents) _ -> moduleNotFound n =<< getSearchPath -- generate all possible search paths diff --git a/src/Cryptol/ModuleSystem/Name.hs b/src/Cryptol/ModuleSystem/Name.hs index 06f055bd..4f98e22f 100644 --- a/src/Cryptol/ModuleSystem/Name.hs +++ b/src/Cryptol/ModuleSystem/Name.hs @@ -13,6 +13,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} -- for the instances of RunM and BaseM {-# LANGUAGE UndecidableInstances #-} @@ -221,7 +222,10 @@ nameFixity = nFixity asPrim :: Name -> Maybe Ident asPrim Name { .. } = case nInfo of - Declared p _ | p == preludeName -> Just nIdent + Declared p _ + | p == preludeName -> Just nIdent + | p == arrayName -> + Just $ mkIdent $ modNameToText p <> "::" <> identText nIdent _ -> Nothing toParamInstName :: Name -> Name diff --git a/src/Cryptol/Prelude.hs b/src/Cryptol/Prelude.hs index 773fe961..70d0fb6e 100644 --- a/src/Cryptol/Prelude.hs +++ b/src/Cryptol/Prelude.hs @@ -13,7 +13,11 @@ {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE OverloadedStrings #-} -module Cryptol.Prelude (preludeContents,cryptolTcContents) where +module Cryptol.Prelude + ( preludeContents + , arrayContents + , cryptolTcContents + ) where import Data.ByteString(ByteString) @@ -23,6 +27,9 @@ import Text.Heredoc (there) preludeContents :: ByteString preludeContents = B.pack [there|lib/Cryptol.cry|] +arrayContents :: ByteString +arrayContents = B.pack [there|lib/Array.cry|] + cryptolTcContents :: String cryptolTcContents = [there|lib/CryptolTC.z3|] diff --git a/src/Cryptol/Testing/Random.hs b/src/Cryptol/Testing/Random.hs index 95ab9d74..ec8d7a48 100644 --- a/src/Cryptol/Testing/Random.hs +++ b/src/Cryptol/Testing/Random.hs @@ -348,6 +348,7 @@ typeSize ty = TCon (TC (TCNum n)) _ -> Just n _ -> Nothing (TCIntMod, _) -> Nothing + (TCArray, _) -> Nothing (TCSeq, [sz,el]) -> case tNoUser sz of TCon (TC (TCNum n)) _ -> (^ n) <$> typeSize el _ -> Nothing @@ -381,6 +382,7 @@ typeValues ty = [ TCon (TC (TCNum n)) _ ] | 0 < n -> [ VInteger x | x <- [ 0 .. n - 1 ] ] _ -> [] + TCArray -> [] TCSeq -> case map tNoUser ts of [ TCon (TC (TCNum n)) _, TCon (TC TCBit) [] ] -> diff --git a/src/Cryptol/TypeCheck/TCon.hs b/src/Cryptol/TypeCheck/TCon.hs index 82a5fa38..7a110dd1 100644 --- a/src/Cryptol/TypeCheck/TCon.hs +++ b/src/Cryptol/TypeCheck/TCon.hs @@ -42,6 +42,7 @@ builtInType nm = case M.nameInfo nm of M.Declared m _ | m == preludeName -> Map.lookup (M.nameIdent nm) builtInTypes + | m == arrayName -> Map.lookup (M.nameIdent nm) builtInArray _ -> Nothing where @@ -81,6 +82,11 @@ builtInType nm = , "lengthFromThenTo" ~> TF TCLenFromThenTo ] + -- Built-in types from Array.cry + builtInArray = Map.fromList + [ "Array" ~> TC TCArray + ] + @@ -115,6 +121,7 @@ instance HasKind TC where TCBit -> KType TCInteger -> KType TCIntMod -> KNum :-> KType + TCArray -> KType :-> KType :-> KType TCSeq -> KNum :-> KType :-> KType TCFun -> KType :-> KType :-> KType TCTuple n -> foldr (:->) KType (replicate n KType) @@ -190,6 +197,7 @@ data TC = TCNum Integer -- ^ Numbers | TCBit -- ^ Bit | TCInteger -- ^ Integer | TCIntMod -- ^ @Z _@ + | TCArray -- ^ @Array _ _@ | TCSeq -- ^ @[_] _@ | TCFun -- ^ @_ -> _@ | TCTuple Int -- ^ @(_, _, _)@ @@ -286,6 +294,7 @@ instance PP TC where TCBit -> text "Bit" TCInteger -> text "Integer" TCIntMod -> text "Z" + TCArray -> text "Array" TCSeq -> text "[]" TCFun -> text "(->)" TCTuple 0 -> text "()" diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index 43e0ae46..6625b350 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -489,6 +489,9 @@ tInteger = TCon (TC TCInteger) [] tIntMod :: Type -> Type tIntMod n = TCon (TC TCIntMod) [n] +tArray :: Type -> Type -> Type +tArray a b = TCon (TC TCArray) [a, b] + tWord :: Type -> Type tWord a = tSeq a tBit diff --git a/src/Cryptol/Utils/Ident.hs b/src/Cryptol/Utils/Ident.hs index c4abf3d6..b147d268 100644 --- a/src/Cryptol/Utils/Ident.hs +++ b/src/Cryptol/Utils/Ident.hs @@ -16,6 +16,7 @@ module Cryptol.Utils.Ident , modNameChunks , packModName , preludeName + , arrayName , interactiveName , noModuleName , exprModName @@ -100,6 +101,9 @@ modInstPref = "`" preludeName :: ModName preludeName = packModName ["Cryptol"] +arrayName :: ModName +arrayName = packModName ["Array"] + interactiveName :: ModName interactiveName = packModName [""]