Merge pull request #99 from GaloisInc/what4-eval3

What4 eval3

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

@@ -44,7 +44,7 @@ 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
+  , ModName, modNameToText, identText, interactiveName
   )
 import qualified Cryptol.Utils.RecordMap as C
 import Cryptol.TypeCheck.TypeOf (fastTypeOf, fastSchemaOf)
@@ -1082,7 +1082,25 @@ plainSubst s ty =
     C.TVar x       -> C.apSubst s (C.TVar x)
 
 
-cryptolURI :: [Text] -> Maybe Int -> URI
+-- | Generate a URI representing a cryptol name from a sequence of 
+--   name parts representing the fully-qualified name.  If a \"unique\"
+--   value is given, this represents a dynamically bound name in
+--   the \"\<interactive\>\" pseudo-module, and the unique value will
+--   be incorporated into the name as a fragment identifier.
+--   At least one name component must be supplied.
+--
+--   Some examples:
+--
+--   * @Cryptol::foldl@ ---> @cryptol:\/Cryptol\/foldl@
+--   * @MyModule::SubModule::name@ ---> @cryptol:\/MyModule\/SubModule\/name@
+--   * @\<interactive\>::f@ ---> @cryptol:f#1234@
+--
+--   In the above example, 1234 is the unique integer value provided with the name.
+
+cryptolURI ::
+  [Text] {- ^ Name components  -} ->
+  Maybe Int {- ^ unique integer for dynamic names -} ->
+  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)]) $
@@ -1108,6 +1126,46 @@ cryptolURI (p:ps) (Just uniq) =
        , uriFragment = Just frag
        }
 
+-- | Tests if the given 'NameInfo' represents a name imported
+--   from the given Cryptol module name.  If so, it returns
+--   the identifier within that module.  Note, this does
+--   not match dynamic identifiers from the \"\<interactive\>\"
+--   pseudo-module.
+isCryptolModuleName :: C.ModName -> NameInfo -> Maybe Text
+isCryptolModuleName modNm (ImportedName uri _)
+  | Just sch <- uriScheme uri
+  , unRText sch == "cryptol"
+  , Left True <- uriAuthority uri
+  , Just (False, x :| xs) <- uriPath uri
+  , [] <- uriQuery uri
+  , Nothing <- uriFragment uri
+  = checkModName (x:xs) (Text.splitOn "::" (C.modNameToText modNm))
+
+ where
+ checkModName [i] [] = Just (unRText i)
+ checkModName (x:xs) (m:ms) | unRText x == m = checkModName xs ms
+ checkModName _ _ = Nothing
+
+isCryptolModuleName _ _ = Nothing
+
+
+-- | Tests if the given `NameInfo` represents a name
+--   from the special \<interactive\> cryptol module.
+--   If so, returns the base identifier name.
+isCryptolInteractiveName :: NameInfo -> Maybe Text
+isCryptolInteractiveName (ImportedName uri _)
+  | Just sch <- uriScheme uri
+  , unRText sch == "cryptol"
+  , Left False <- uriAuthority uri
+  , Just (False, i :| []) <- uriPath uri
+  , [] <- uriQuery uri
+  , Just _ <- uriFragment uri
+  = Just (unRText i)
+
+isCryptolInteractiveName _ = Nothing
+
+
+
 importName :: C.Name -> IO NameInfo
 importName cnm =
   case C.nameInfo cnm of

saw-core-what4/src/Verifier/SAW/Simulator/What4.hs

@@ -50,6 +50,9 @@ module Verifier.SAW.Simulator.What4
   , w4EvalAny
   , w4EvalBasic
   , getLabelValues
+
+  , w4SimulatorEval
+  , NeutralTermException(..)
   ) where
 
 
@@ -71,6 +74,7 @@ import Data.Traversable as T
 #if !MIN_VERSION_base(4,8,0)
 import Control.Applicative
 #endif
+import qualified Control.Exception as X
 import Control.Monad.State as ST
 import Numeric.Natural (Natural)
 
@@ -430,10 +434,8 @@ bvSShROp = bvShiftOp (SW.bvAshr given)
 bvForall :: W.IsSymExprBuilder sym =>
   sym -> Natural -> (SWord sym -> IO (Pred sym)) -> IO (Pred sym)
 bvForall sym n f =
-  case W.userSymbol "i" of
-    Left err -> fail $ show err
-    Right indexSymbol ->
-      case mkNatRepr n of
+  do let indexSymbol = W.safeSymbol "i"
+     case mkNatRepr n of
         Some w
           | Just LeqProof <- testLeq (knownNat @1) w ->
             withKnownNat w $ do
@@ -706,16 +708,14 @@ mkSymFn ::
   String -> Assignment BaseTypeRepr args -> BaseTypeRepr ret ->
   IO (W.SymFn sym args ret)
 mkSymFn sym ref nm args ret =
-  case W.userSymbol nm of
-    Left err -> fail $ show err ++ ": Cannot create uninterpreted constant " ++ nm
-    Right s  ->
-      do cache <- readIORef ref
-         case lookupSymFn s args ret cache of
-           Just fn -> return fn
-           Nothing ->
-             do fn <- W.freshTotalUninterpFn sym s args ret
-                writeIORef ref (insertSymFn s args ret fn cache)
-                return fn
+  do let s = W.safeSymbol nm
+     cache <- readIORef ref
+     case lookupSymFn s args ret cache of
+       Just fn -> return fn
+       Nothing ->
+         do fn <- W.freshTotalUninterpFn sym s args ret
+            writeIORef ref (insertSymFn s args ret fn cache)
+            return fn
 
 ----------------------------------------------------------------------
 -- Given a constant nm of (saw-core) type ty, construct an uninterpreted
@@ -1128,6 +1128,39 @@ w4EvalBasic sym sc m addlPrims ref unintSet t =
      cfg <- Sim.evalGlobal' m (give sym constMap `Map.union` addlPrims) extcns uninterpreted
      Sim.evalSharedTerm cfg t
 
+
+-- | Evaluate a saw-core term to a What4 value for the purposes of
+--   using it as an input for symbolic simulation.  This will evaluate
+--   primitives, but will cancel evaluation and return the associated
+--   'NameInfo' if it encounters a constant value with an 'ExtCns'
+--   that is not accepted by the filter.
+w4SimulatorEval ::
+  forall n solver fs.
+  CS.SAWCoreBackend n solver fs ->
+  SharedContext ->
+  ModuleMap ->
+  Map Ident (SValue (CS.SAWCoreBackend n solver fs)) {- ^ additional primitives -} ->
+  IORef (SymFnCache (CS.SAWCoreBackend n solver fs)) {- ^ cache for uninterpreted function symbols -} ->
+  (ExtCns (TValue (What4 (CS.SAWCoreBackend n solver fs))) -> Bool)
+    {- ^ Filter for constant values.  True means unfold, false means halt evaluation. -} ->
+  Term {- ^ term to simulate -} ->
+  IO (Either NameInfo (SValue (CS.SAWCoreBackend n solver fs)))
+w4SimulatorEval sym sc m addlPrims ref constantFilter t =
+  do let extcns tf (EC ix nm ty) =
+           do trm <- ArgTermConst <$> scTermF sc tf
+              parseUninterpretedSAW sym sc ref trm (mkUnintApp (Text.unpack (toShortName nm) ++ "_" ++ show ix)) ty
+     let uninterpreted _tf ec =
+          if constantFilter ec then Nothing else Just (X.throwIO (NeutralTermEx (ecName ec)))
+     res <- X.try $ do
+              cfg <- Sim.evalGlobal' m (give sym constMap `Map.union` addlPrims) extcns uninterpreted
+              Sim.evalSharedTerm cfg t
+     case res of
+       Left (NeutralTermEx nmi) -> pure (Left nmi)
+       Right x -> pure (Right x)
+
+data NeutralTermException = NeutralTermEx NameInfo deriving Show
+instance X.Exception NeutralTermException
+
 -- | Given a constant nm of (saw-core) type ty, construct an
 -- uninterpreted constant with that type. The 'Term' argument should
 -- be an open term, which should have the designated return type when

saw-core/src/Verifier/SAW/SharedTerm.hs

@@ -354,13 +354,13 @@ scFreshNameURI :: Text -> VarIndex -> URI
 scFreshNameURI nm i = fromMaybe (panic "scFreshNameURI" ["Failed to constructed name URI", show nm, show i]) $
   do sch <- mkScheme "fresh"
      nm' <- mkPathPiece (if Text.null nm then "_" else nm)
-     i'  <- mkPathPiece (Text.pack (show i))
+     i'  <- mkFragment (Text.pack (show i))
      pure URI
        { uriScheme = Just sch
-       , uriAuthority = Left True -- absolute path
-       , uriPath   = Just (False, (nm' :| [i']))
+       , uriAuthority = Left False -- relative path
+       , uriPath   = Just (False, (nm' :| []))
        , uriQuery  = []
-       , uriFragment = Nothing
+       , uriFragment = Just i'
        }
 
 moduleIdentToURI :: Ident -> URI

saw-core/src/Verifier/SAW/Term/Pretty.hs

@@ -39,10 +39,12 @@ import Control.Monad.State.Strict as State
 import Data.Foldable (Foldable)
 #endif
 import qualified Data.Foldable as Fold
+import qualified Data.Text as Text
 import qualified Data.Vector as V
 import Numeric (showIntAtBase)
 import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 import qualified Text.PrettyPrint.ANSI.Leijen as PPL ((<$>))
+import Text.URI
 
 import Data.IntMap.Strict (IntMap)
 import qualified Data.IntMap.Strict as IntMap
@@ -426,7 +428,7 @@ ppFlatTermF prec tf =
 
 ppName :: NameInfo -> Doc
 ppName (ModuleIdentifier i) = ppIdent i
-ppName (ImportedName absName _) = text (show absName)
+ppName (ImportedName absName _) = text (Text.unpack (render absName))
 
 -- | Pretty-print a non-shared term
 ppTermF :: Prec -> TermF Term -> PPM Doc