Merge pull request #87 from GaloisInc/structured-names

Structured names

cryptol-saw-core/cryptol-saw-core.cabal

@@ -31,6 +31,7 @@ library
     cryptol >= 2.3.0,
     data-inttrie >= 0.1.4,
     integer-gmp,
+    modern-uri,
     panic,
     saw-core,
     saw-core-aig,

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

@@ -1,4 +1,5 @@
 {-# OPTIONS_GHC -Wall #-}
+{-# LANGUAGE DoAndIfThenElse #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE ViewPatterns #-}
@@ -19,13 +20,18 @@ import Control.Monad (foldM, join, unless)
 import Data.Bifunctor (first)
 import qualified Data.Foldable as Fold
 import Data.List
+import Data.List.NonEmpty (NonEmpty(..))
+import Data.Maybe (fromMaybe)
 import qualified Data.IntTrie as IntTrie
 import Data.Map (Map)
 import qualified Data.Map as Map
 import qualified Data.Set as Set
+import Data.Text (Text)
+import qualified Data.Text as Text
 import qualified Data.Vector as Vector
 import Prelude ()
 import Prelude.Compat
+import Text.URI
 
 import qualified Cryptol.Eval.Type as TV
 import qualified Cryptol.Backend.Monad as V
@@ -34,8 +40,12 @@ import qualified Cryptol.Eval.Concrete as V
 import Cryptol.Eval.Type (evalValType)
 import qualified Cryptol.TypeCheck.AST as C
 import qualified Cryptol.TypeCheck.Subst as C (Subst, apSubst, singleTParamSubst)
-import qualified Cryptol.ModuleSystem.Name as C (asPrim, nameIdent)
-import qualified Cryptol.Utils.Ident as C (Ident, PrimIdent(..), packIdent, unpackIdent, prelPrim, floatPrim, arrayPrim)
+import qualified Cryptol.ModuleSystem.Name as C
+  (asPrim, nameUnique, nameIdent, nameInfo, NameInfo(..))
+import qualified Cryptol.Utils.Ident as C
+  ( Ident, PrimIdent(..), packIdent, unpackIdent, prelPrim, floatPrim, arrayPrim
+  , modNameToText, identText, interactiveName
+  )
 import qualified Cryptol.Utils.RecordMap as C
 import Cryptol.TypeCheck.TypeOf (fastTypeOf, fastSchemaOf)
 import Cryptol.Utils.PP (pretty)
@@ -1071,6 +1081,52 @@ plainSubst s ty =
     C.TRec fs      -> C.TRec (fmap (plainSubst s) fs)
     C.TVar x       -> C.apSubst s (C.TVar x)
 
+
+cryptolURI :: [Text] -> Maybe Int -> URI
+cryptolURI [] _ = panic "cryptolURI" ["Could not make URI from empty path"]
+cryptolURI (p:ps) Nothing =
+  fromMaybe (panic "cryptolURI" ["Could not make URI from the given path", show (p:ps)]) $
+  do sch <- mkScheme "cryptol"
+     path' <- mapM mkPathPiece (p:|ps)
+     pure URI
+       { uriScheme = Just sch
+       , uriAuthority = Left True -- absolute path
+       , uriPath = Just (False, path')
+       , uriQuery = []
+       , uriFragment = Nothing
+       }
+cryptolURI (p:ps) (Just uniq) =
+  fromMaybe (panic "cryptolURI" ["Could not make URI from the given path", show (p:ps), show uniq]) $
+  do sch <- mkScheme "cryptol"
+     path' <- mapM mkPathPiece (p:|ps)
+     frag <- mkFragment (Text.pack (show uniq))
+     pure URI
+       { uriScheme = Just sch
+       , uriAuthority = Left False -- relative path
+       , uriPath = Just (False, path')
+       , uriQuery = []
+       , uriFragment = Just frag
+       }
+
+importName :: C.Name -> IO NameInfo
+importName cnm =
+  case C.nameInfo cnm of
+    C.Parameter -> fail ("Cannot import non-top-level name: " ++ show cnm)
+    C.Declared modNm _
+      | modNm == C.interactiveName ->
+          let shortNm = C.identText (C.nameIdent cnm)
+              aliases = [shortNm]
+              uri = cryptolURI [shortNm] (Just (C.nameUnique cnm))
+           in pure (ImportedName uri aliases)
+
+      | otherwise ->
+          let modNmTxt  = C.modNameToText modNm
+              modNms = Text.splitOn "::" modNmTxt
+              shortNm = C.identText (C.nameIdent cnm)
+              aliases = [shortNm, modNmTxt <> "::" <> shortNm]
+              uri = cryptolURI (modNms ++ [shortNm]) Nothing
+           in pure (ImportedName uri aliases)
+
 -- | Currently this imports declaration groups by inlining all the
 -- definitions. (With subterm sharing, this is not as bad as it might
 -- seem.) We might want to think about generating let or where
@@ -1088,7 +1144,11 @@ importDeclGroup isTopLevel sc env (C.Recursive [decl]) =
          let x = nameToString (C.dName decl)
          f' <- scLambda sc x t' e'
          rhs <- scGlobalApply sc "Prelude.fix" [t', f']
-         rhs' <- if not isTopLevel then return rhs else scConstant sc x rhs t'
+         rhs' <- if isTopLevel then
+                    do nmi <- importName (C.dName decl)
+                       scConstant' sc nmi rhs t'
+                 else
+                   return rhs
          let env' = env { envE = Map.insert (C.dName decl) (rhs', 0) (envE env)
                         , envC = Map.insert (C.dName decl) (C.dSignature decl) (envC env) }
          return env'
@@ -1145,7 +1205,11 @@ importDeclGroup isTopLevel sc env (C.Recursive decls) =
      let mkRhs d t =
            do let s = nameToString (C.dName d)
               r <- scRecordSelect sc rhs s
-              if isTopLevel then scConstant sc s r t else return r
+              if isTopLevel then
+                do nmi <- importName (C.dName d)
+                   scConstant' sc nmi r t
+              else
+                return r
      rhss <- sequence (Map.intersectionWith mkRhs dm tm)
 
      let env' = env { envE = Map.union (fmap (\v -> (v, 0)) rhss) (envE env)
@@ -1167,8 +1231,9 @@ importDeclGroup isTopLevel sc env (C.NonRecursive decl) =
     C.DExpr expr -> do
      rhs <- importExpr' sc env (C.dSignature decl) expr
      rhs' <- if not isTopLevel then return rhs else do
+       nmi <- importName (C.dName decl)
        t <- importSchema sc env (C.dSignature decl)
-       scConstant sc (nameToString (C.dName decl)) rhs t
+       scConstant' sc nmi rhs t
      let env' = env { envE = Map.insert (C.dName decl) (rhs', 0) (envE env)
                     , envC = Map.insert (C.dName decl) (C.dSignature decl) (envC env) }
      return env'

cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs

@@ -30,6 +30,7 @@ module Verifier.SAW.CryptolEnv
   , getAllIfaceDecls
   , InputText(..)
   , lookupIn
+  , resolveIdentifier
   )
   where
 
@@ -39,7 +40,7 @@ import Data.Map (Map)
 import qualified Data.Map as Map
 import qualified Data.Set as Set
 import Data.Maybe (fromMaybe)
-import Data.Text (Text, pack)
+import Data.Text (Text, pack, splitOn)
 import Control.Monad(when)
 
 #if !MIN_VERSION_base(4,8,0)
@@ -77,6 +78,8 @@ import qualified Cryptol.ModuleSystem.NamingEnv as MN
 import qualified Cryptol.ModuleSystem.Name as MN
 import qualified Cryptol.ModuleSystem.Renamer as MR
 
+import qualified Cryptol.Utils.Ident as C
+
 import Cryptol.Utils.PP
 import Cryptol.Utils.Ident (Ident, preludeName, preludeReferenceName
                            , packIdent, interactiveName, identText
@@ -448,6 +451,27 @@ bindInteger (ident, n) env =
 
 --------------------------------------------------------------------------------
 
+resolveIdentifier ::
+  (?fileReader :: FilePath -> IO ByteString) =>
+  CryptolEnv -> Text -> IO (Maybe T.Name)
+resolveIdentifier env nm =
+  case splitOn (pack "::") nm of
+    []  -> pure Nothing
+    [i] -> doResolve (P.UnQual (C.mkIdent i))
+    xs  -> let (qs,i) = (init xs, last xs)
+            in doResolve (P.Qual (C.packModName qs) (C.mkIdent i))
+ where
+ modEnv = eModuleEnv env
+ nameEnv = getNamingEnv env
+
+ doResolve pnm =
+    do (res, _ws) <- MM.runModuleM (defaultEvalOpts, ?fileReader, modEnv) $
+          MM.interactive (MB.rename interactiveName nameEnv (MR.renameVar pnm))
+       case res of
+         Left _ -> pure Nothing
+         Right (x,_) -> pure (Just x)
+
+
 parseTypedTerm ::
   (?fileReader :: FilePath -> IO ByteString) =>
   SharedContext -> CryptolEnv -> InputText -> IO TypedTerm

saw-core-aig/saw-core-aig.cabal

@@ -20,6 +20,7 @@ library
     base == 4.*,
     containers,
     saw-core,
+    text,
     vector
   hs-source-dirs: src
   exposed-modules:

saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs

@@ -30,6 +30,7 @@ import Control.Monad ((<=<))
 import Data.IORef
 import Data.Map (Map)
 import qualified Data.Map as Map
+import qualified Data.Text as Text
 import qualified Data.Vector as V
 import Numeric.Natural (Natural)
 
@@ -489,7 +490,7 @@ bitBlastTerm be sc addlPrims t = do
   modmap <- scGetModuleMap sc
   bval <- bitBlastBasic be modmap addlPrims ecMap t
   bval' <- applyAll bval argVars
-  let names =  map fst args ++ map ecName ecs
+  let names =  map fst args ++ map (Text.unpack . toShortName . ecName) ecs
       shapes = argShapes ++ ecShapes
   return (bval', zip names shapes)
 

saw-core-sbv/saw-core-sbv.cabal

@@ -21,6 +21,7 @@ library
     mtl,
     saw-core,
     sbv >= 8.0,
+    text,
     transformers,
     vector
   hs-source-dirs: src

saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs

@@ -47,7 +47,9 @@ import Data.Bits
 import Data.IORef
 import Data.Map (Map)
 import qualified Data.Map as Map
+import Data.Set (Set)
 import qualified Data.Set as Set
+import qualified Data.Text as Text
 import Data.Vector (Vector)
 import qualified Data.Vector as V
 
@@ -65,7 +67,7 @@ import qualified Verifier.SAW.Simulator as Sim
 import qualified Verifier.SAW.Simulator.Prims as Prims
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.Simulator.Value
-import Verifier.SAW.TypedAST (FieldName, ModuleMap, identName)
+import Verifier.SAW.TypedAST (FieldName, identName, toShortName)
 import Verifier.SAW.FiniteValue (FirstOrderType(..), asFirstOrderType)
 
 data SBV
@@ -565,13 +567,14 @@ muxSbvExtra c x y =
 
 -- | Abstract constants with names in the list 'unints' are kept as
 -- uninterpreted constants; all others are unfolded.
-sbvSolveBasic :: ModuleMap -> Map Ident SValue -> [String] -> Term -> IO SValue
-sbvSolveBasic m addlPrims unints t = do
-  let unintSet = Set.fromList unints
-  let extcns (EC ix nm ty) = parseUninterpreted [] (nm ++ "#" ++ show ix) ty
+sbvSolveBasic :: SharedContext -> Map Ident SValue -> Set VarIndex -> Term -> IO SValue
+sbvSolveBasic sc addlPrims unintSet t = do
+  m <- scGetModuleMap sc
+
+  let extcns (EC ix nm ty) = parseUninterpreted [] (Text.unpack (toShortName nm) ++ "#" ++ show ix) ty
   let uninterpreted ec
-        | Set.member (ecName ec) unintSet = Just (extcns ec)
-        | otherwise                       = Nothing
+        | Set.member (ecVarIndex ec) unintSet = Just (extcns ec)
+        | otherwise                           = Nothing
   cfg <- Sim.evalGlobal m (Map.union constMap addlPrims) extcns uninterpreted
   Sim.evalSharedTerm cfg t
 
@@ -660,12 +663,11 @@ vAsFirstOrderType v =
 
 sbvSolve :: SharedContext
          -> Map Ident SValue
-         -> [String]
+         -> Set VarIndex
          -> Term
          -> IO ([Maybe Labeler], Symbolic SBool)
-sbvSolve sc addlPrims unints t = do
-  modmap <- scGetModuleMap sc
-  let eval = sbvSolveBasic modmap addlPrims unints
+sbvSolve sc addlPrims unintSet t = do
+  let eval = sbvSolveBasic sc addlPrims unintSet
   ty <- eval =<< scTypeOf sc t
   let lamNames = map fst (fst (R.asLambdaList t))
   let varNames = [ "var" ++ show (i :: Integer) | i <- [0 ..] ]
@@ -773,17 +775,16 @@ argTypes sc t = do
 sbvCodeGen_definition
   :: SharedContext
   -> Map Ident SValue
-  -> [String]
+  -> Set VarIndex
   -> Term
   -> (Natural -> Bool) -- ^ Allowed word sizes
   -> IO (SBVCodeGen (), [FirstOrderType], FirstOrderType)
-sbvCodeGen_definition sc addlPrims unints t checkSz = do
+sbvCodeGen_definition sc addlPrims unintSet t checkSz = do
   ty <- scTypeOf sc t
   (argTs,resTy) <- argTypes sc ty
   shapes <- traverse (asFirstOrderType sc) argTs
   resultShape <- asFirstOrderType sc resTy
-  modmap <- scGetModuleMap sc
-  bval <- sbvSolveBasic modmap addlPrims unints t
+  bval <- sbvSolveBasic sc addlPrims unintSet t
   vars <- evalStateT (traverse (newCodeGenVars checkSz) shapes) 0
   let codegen = do
         args <- traverse (fmap ready) vars
@@ -862,14 +863,14 @@ sbvSetOutput _checkSz _ft _v _i = do
 
 sbvCodeGen :: SharedContext
            -> Map Ident SValue
-           -> [String]
+           -> Set VarIndex
            -> Maybe FilePath
            -> String
            -> Term
            -> IO ()
-sbvCodeGen sc addlPrims unints path fname t = do
+sbvCodeGen sc addlPrims unintSet path fname t = do
   -- The SBV C code generator expects only these word sizes
   let checkSz n = n `elem` [8,16,32,64]
 
-  (codegen,_,_) <- sbvCodeGen_definition sc addlPrims unints t checkSz
+  (codegen,_,_) <- sbvCodeGen_definition sc addlPrims unintSet t checkSz
   compileToC path fname codegen

saw-core-what4/saw-core-what4.cabal

@@ -25,6 +25,7 @@ library
     what4,
     crucible-saw,
     panic,
+    text,
     transformers,
     vector,
     parameterized-utils >= 1.0.8 && < 2.2,