Implement changes to incorporate the new structure name conventions

from SAWCore (CF GaloisInc/saw-core#87).

Add logic for first attempting to resolve user-supplied names
using the Cryptol interactive scope, then fall back on the SAWCore
naming environment.

saw-script.cabal

@@ -58,6 +58,7 @@ library
     , lens
     , llvm-pretty >= 0.8
     , llvm-pretty-bc-parser >= 0.1.3.1
+    , modern-uri >= 0.3.2 && < 0.4
     , mtl >= 2.1
     , old-locale
     , old-time

src/SAWScript/Builtins.hs

@@ -35,9 +35,12 @@ import qualified Data.ByteString.Lazy.UTF8 as B
 import qualified Data.IntMap as IntMap
 import Data.List (isPrefixOf, isInfixOf)
 import qualified Data.Map as Map
+import Data.Set (Set)
+import qualified Data.Set as Set
 import Data.Maybe
 import Data.Time.Clock
 import Data.Typeable
+import qualified Data.Text as Text
 import System.Directory
 import qualified System.Environment
 import qualified System.Exit as Exit
@@ -457,7 +460,10 @@ print_goal_depth n =
 printGoalConsts :: ProofScript ()
 printGoalConsts =
   withFirstGoal $ \goal ->
-  do mapM_ (printOutLnTop Info) $ Map.keys (getConstantSet (unProp (goalProp goal)))
+  do mapM_ (printOutLnTop Info) $
+       [ show nm
+       | (_,(nm,_,_)) <- Map.toList (getConstantSet (unProp (goalProp goal)))
+       ]
      return ((), mempty, Just goal)
 
 printGoalSize :: ProofScript ()
@@ -468,12 +474,38 @@ printGoalSize =
      printOutLnTop Info $ "Goal unshared size: " ++ show (scTreeSize t)
      return ((), mempty, Just goal)
 
+resolveNames :: SharedContext -> [String] -> TopLevel (Set VarIndex)
+resolveNames sc nms = Set.fromList <$> mapM (resolveName sc) nms
+
+resolveName :: SharedContext -> String -> TopLevel VarIndex
+resolveName sc nm =
+  do cenv <- rwCryptol <$> getTopLevelRW
+     let ?fileReader = StrictBS.readFile
+     res <- io $ CEnv.resolveIdentifier cenv tnm
+     case res of
+       Just cnm ->
+         do x <- io $ Cryptol.importName cnm
+            case x of
+              ImportedName uri _ ->
+                do y <- io $ scResolveNameByURI sc uri
+                   case y of
+                     Just vi -> pure vi
+                     Nothing -> fallback
+              _ -> fallback
+       Nothing -> fallback
+
+ where
+ tnm = Text.pack nm
+ fallback = fst <$> io (scResolveUnambiguous sc tnm)
+
+
 unfoldGoal :: [String] -> ProofScript ()
 unfoldGoal names =
   withFirstGoal $ \goal ->
   do sc <- getSharedContext
      let Prop trm = goalProp goal
-     trm' <- io $ scUnfoldConstants sc names trm
+     nms <- mapM (resolveName sc) names
+     trm' <- io $ scUnfoldConstants sc nms trm
      return ((), mempty, Just (goal { goalProp = Prop trm' }))
 
 simplifyGoal :: Simpset -> ProofScript ()
@@ -488,10 +520,11 @@ goal_eval :: [String] -> ProofScript ()
 goal_eval unints =
   withFirstGoal $ \goal ->
   do sc <- getSharedContext
+     unintSet <- resolveNames sc unints
      t0 <- liftIO $ propToPredicate sc (goalProp goal)
      let gen = globalNonceGenerator
      sym <- liftIO $ Crucible.newSAWCoreBackend FloatRealRepr sc gen
-     (_names, (_mlabels, p)) <- liftIO $ W4Sim.w4Eval sym sc Map.empty unints t0
+     (_names, (_mlabels, p)) <- liftIO $ W4Sim.w4Eval sym sc Map.empty unintSet t0
      t1 <- liftIO $ Crucible.toSC sym p
      t2 <- liftIO $ scEqTrue sc t1
      return ((), mempty, Just (goal { goalProp = Prop t2 }))
@@ -675,11 +708,11 @@ writeSAIGComputedPrim f t n = do
 proveRME :: ProofScript SV.SatResult
 proveRME = wrapProver Prover.proveRME
 
-codegenSBV :: SharedContext -> FilePath -> [String] -> String -> TypedTerm -> IO ()
+codegenSBV :: SharedContext -> FilePath -> [String] -> String -> TypedTerm -> TopLevel ()
 codegenSBV sc path unints fname (TypedTerm _schema t) =
-  SBVSim.sbvCodeGen sc mempty unints mpath fname t
-  where mpath = if null path then Nothing else Just path
-
+  do unintSet <- resolveNames sc unints
+     let mpath = if null path then Nothing else Just path
+     io $ SBVSim.sbvCodeGen sc mempty unintSet mpath fname t
 
 -- | Bit-blast a proposition and check its validity using SBV.
 -- (Currently ignores satisfying assignments.)
@@ -692,7 +725,9 @@ proveSBV conf = proveUnintSBV conf []
 proveUnintSBV :: SBV.SMTConfig -> [String] -> ProofScript SV.SatResult
 proveUnintSBV conf unints =
   do timeout <- psTimeout <$> get
-     wrapProver (Prover.proveUnintSBV conf unints timeout)
+     sc <- lift $ SV.getSharedContext
+     unintSet <- lift $ resolveNames sc unints
+     wrapProver (Prover.proveUnintSBV conf unintSet timeout)
 
 applyProverToGoal :: (SharedContext
                       -> Prop -> IO (Maybe [(String, FirstOrderValue)], SolverStats))
@@ -775,40 +810,58 @@ proveUnintYices = proveUnintSBV SBV.yices
 
 --------------------------------------------------
 w4_boolector :: ProofScript SV.SatResult
-w4_boolector = wrapW4Prover $ Prover.proveWhat4_boolector []
+w4_boolector = wrapW4Prover $ Prover.proveWhat4_boolector mempty
 
 w4_z3 :: ProofScript SV.SatResult
-w4_z3 = wrapW4Prover $ Prover.proveWhat4_z3 []
+w4_z3 = wrapW4Prover $ Prover.proveWhat4_z3 mempty
 
 w4_cvc4 :: ProofScript SV.SatResult
-w4_cvc4 = wrapW4Prover $ Prover.proveWhat4_cvc4 []
+w4_cvc4 = wrapW4Prover $ Prover.proveWhat4_cvc4 mempty
 
 w4_yices :: ProofScript SV.SatResult
-w4_yices = wrapW4Prover $ Prover.proveWhat4_yices []
+w4_yices = wrapW4Prover $ Prover.proveWhat4_yices mempty
 
 w4_unint_boolector :: [String] -> ProofScript SV.SatResult
-w4_unint_boolector = wrapW4Prover . Prover.proveWhat4_boolector
+w4_unint_boolector unints =
+  do sc <- lift $ SV.getSharedContext
+     unintSet <- lift $ resolveNames sc unints
+     wrapW4Prover (Prover.proveWhat4_boolector unintSet)
 
 w4_unint_z3 :: [String] -> ProofScript SV.SatResult
-w4_unint_z3 = wrapW4Prover . Prover.proveWhat4_z3
+w4_unint_z3 unints =
+  do sc <- lift $ SV.getSharedContext
+     unintSet <- lift $ resolveNames sc unints
+     wrapW4Prover (Prover.proveWhat4_z3 unintSet)
 
 w4_unint_cvc4 :: [String] -> ProofScript SV.SatResult
-w4_unint_cvc4 = wrapW4Prover . Prover.proveWhat4_cvc4
+w4_unint_cvc4 unints =
+  do sc <- lift $ SV.getSharedContext
+     unintSet <- lift $ resolveNames sc unints
+     wrapW4Prover (Prover.proveWhat4_cvc4 unintSet)
 
 w4_unint_yices :: [String] -> ProofScript SV.SatResult
-w4_unint_yices = wrapW4Prover . Prover.proveWhat4_yices
+w4_unint_yices unints =
+  do sc <- lift $ SV.getSharedContext
+     unintSet <- lift $ resolveNames sc unints
+     wrapW4Prover (Prover.proveWhat4_yices unintSet)
 
 offline_w4_unint_z3 :: [String] -> String -> ProofScript SV.SatResult
 offline_w4_unint_z3 unints path =
-  wrapW4ProveExporter (Prover.proveExportWhat4_z3 unints) path ".smt2"
+  do sc <- lift $ SV.getSharedContext
+     unintSet <- lift $ resolveNames sc unints
+     wrapW4ProveExporter (Prover.proveExportWhat4_z3 unintSet) path ".smt2"
 
 offline_w4_unint_cvc4 :: [String] -> String -> ProofScript SV.SatResult
 offline_w4_unint_cvc4 unints path =
-  wrapW4ProveExporter (Prover.proveExportWhat4_cvc4 unints) path ".smt2"
+  do sc <- lift $ SV.getSharedContext
+     unintSet <- lift $ resolveNames sc unints
+     wrapW4ProveExporter (Prover.proveExportWhat4_cvc4 unintSet) path ".smt2"
 
 offline_w4_unint_yices :: [String] -> String -> ProofScript SV.SatResult
 offline_w4_unint_yices unints path =
-  wrapW4ProveExporter (Prover.proveExportWhat4_yices unints) path ".smt2"
+  do sc <- lift $ SV.getSharedContext
+     unintSet <- lift $ resolveNames sc unints
+     wrapW4ProveExporter (Prover.proveExportWhat4_yices unintSet) path ".smt2"
 
 proveWithExporter ::
   (SharedContext -> FilePath -> Prop -> IO ()) ->
@@ -842,7 +895,10 @@ offline_smtlib2 :: FilePath -> ProofScript SV.SatResult
 offline_smtlib2 path = proveWithExporter Prover.writeSMTLib2 path ".smt2"
 
 offline_unint_smtlib2 :: [String] -> FilePath -> ProofScript SV.SatResult
-offline_unint_smtlib2 unints path = proveWithExporter (Prover.writeUnintSMTLib2 unints) path ".smt2"
+offline_unint_smtlib2 unints path =
+  do sc <- lift $ SV.getSharedContext
+     unintSet <- lift $ resolveNames sc unints
+     proveWithExporter (Prover.writeUnintSMTLib2 unintSet) path ".smt2"
 
 set_timeout :: Integer -> ProofScript ()
 set_timeout to = modify (\ps -> ps { psTimeout = Just to })
@@ -958,7 +1014,8 @@ rewritePrim ss (TypedTerm schema t) = do
 unfold_term :: [String] -> TypedTerm -> TopLevel TypedTerm
 unfold_term names (TypedTerm schema t) = do
   sc <- getSharedContext
-  t' <- io $ scUnfoldConstants sc names t
+  nms <- mapM (resolveName sc) names
+  t' <- io $ scUnfoldConstants sc nms t
   return (TypedTerm schema t')
 
 beta_reduce_term :: TypedTerm -> TopLevel TypedTerm

src/SAWScript/Crucible/Common/MethodSpec.hs

@@ -149,7 +149,7 @@ ppTypedTerm (TypedTerm tp tm) =
 
 ppTypedExtCns :: TypedExtCns -> PP.Doc
 ppTypedExtCns (TypedExtCns tp ec) =
-  PP.text (ecName ec)
+  ppName (ecName ec)
   PP.<+> PP.text ":" PP.<+>
   PP.text (show (Cryptol.ppPrec 0 tp))
 

src/SAWScript/Crucible/Common/Setup/Type.hs

@@ -39,7 +39,7 @@ import           Control.Monad.IO.Class (MonadIO(liftIO))
 import qualified Cryptol.TypeCheck.Type as Cryptol (Type)
 import qualified Verifier.SAW.Cryptol as Cryptol (importType, emptyEnv)
 import           Verifier.SAW.TypedTerm (TypedTerm, TypedExtCns(..), typedTermOfExtCns)
-import           Verifier.SAW.SharedTerm (SharedContext, scFreshGlobalVar, ExtCns(..))
+import           Verifier.SAW.SharedTerm (SharedContext, scFreshEC)
 
 import qualified SAWScript.Crucible.Common.MethodSpec as MS
 
@@ -106,8 +106,8 @@ freshTypedExtCns ::
   CrucibleSetupT arch m TypedExtCns
 freshTypedExtCns sc name cty =
   do ty <- liftIO $ Cryptol.importType sc Cryptol.emptyEnv cty
-     i <- liftIO $ scFreshGlobalVar sc
-     let tt = TypedExtCns cty (EC i name ty)
+     ec <- liftIO $ scFreshEC sc name ty
+     let tt = TypedExtCns cty ec
      currentState . MS.csFreshVars %= cons tt
      return tt
 

src/SAWScript/Crucible/JVM/Override.hs

@@ -373,7 +373,8 @@ refreshTerms sc ss =
      OM (termSub %= Map.union extension)
   where
     freshenTerm (TypedExtCns _cty ec) =
-      do new <- liftIO (scFreshGlobal sc (ecName ec) (ecType ec))
+      do new <- liftIO $ do i <- scFreshGlobalVar sc
+                            scExtCns sc (EC i (ecName ec) (ecType ec))
          return (ecVarIndex ec, new)
 
 ------------------------------------------------------------------------

src/SAWScript/Crucible/JVM/ResolveSetupValue.hs

@@ -229,8 +229,7 @@ resolveBitvectorTerm sym w tm =
      mx <- case getAllExts tm' of
              [] ->
                do -- Evaluate in SBV to test whether 'tm' is a concrete value
-                  modmap <- scGetModuleMap sc
-                  sbv <- SBV.toWord =<< SBV.sbvSolveBasic modmap Map.empty [] tm'
+                  sbv <- SBV.toWord =<< SBV.sbvSolveBasic sc Map.empty mempty tm'
                   return (SBV.svAsInteger sbv)
              _ -> return Nothing
      case mx of
@@ -246,8 +245,7 @@ resolveBoolTerm sym tm =
      mx <- case getAllExts tm' of
              [] ->
                do -- Evaluate in SBV to test whether 'tm' is a concrete value
-                  modmap <- scGetModuleMap sc
-                  sbv <- SBV.toBool <$> SBV.sbvSolveBasic modmap Map.empty [] tm'
+                  sbv <- SBV.toBool <$> SBV.sbvSolveBasic sc Map.empty mempty tm'
                   return (SBV.svAsBool sbv)
              _ -> return Nothing
      case mx of

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -103,11 +103,11 @@ import qualified Data.Sequence as Seq
 import qualified Data.Text as Text
 import qualified Data.Vector as V
 import           System.IO
-
 import qualified Text.LLVM.AST as L
 import qualified Text.LLVM.PP as L (ppType, ppSymbol)
 import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>), (<>))
 import qualified Text.PrettyPrint.ANSI.Leijen as PP
+import           Text.URI
 import qualified Control.Monad.Trans.Maybe as MaybeT
 
 -- parameterized-utils
@@ -304,6 +304,22 @@ crucible_llvm_array_size_profile assume bic opts (Some lm) nm lemmas setup = do
     profiles <- io $ readIORef cell
     pure . fmap (\(fnm, prof) -> (Text.unpack fnm, prof)) $ Map.toList profiles
 
+llvmURI :: String -> URI
+llvmURI symbol_name =
+  fromMaybe (error $ unwords ["mkLLVMName", "Could not create LLVM symbol name", symbol_name]) $
+  do sch <- mkScheme "llvm"
+     p   <- mkPathPiece (Text.pack symbol_name)
+     pure URI
+       { uriScheme = Just sch
+       , uriAuthority = Left True -- absolute path
+       , uriPath = Just (False, p NE.:| [])
+       , uriQuery = []
+       , uriFragment = Nothing
+       }
+
+llvmNameInfo :: String -> NameInfo
+llvmNameInfo symbol_name = ImportedName (llvmURI symbol_name) [ Text.pack symbol_name ]
+
 crucible_llvm_compositional_extract ::
   BuiltinContext ->
   Options ->
@@ -373,8 +389,10 @@ crucible_llvm_compositional_extract bic opts (Some lm) nm func_name lemmas check
           when ([] /= getAllExts extracted_func) $
             fail "Non-functional simulation summary."
 
+          let nmi = llvmNameInfo func_name
+
           extracted_func_const <-
-            io $ scConstant shared_context func_name extracted_func
+            io $ scConstant' shared_context nmi extracted_func
             =<< scTypeOf shared_context extracted_func
           input_terms <- io $ traverse (scExtCns shared_context) input_parameters
           applied_extracted_func <- io $ scApplyAll shared_context extracted_func_const input_terms
@@ -1346,10 +1364,9 @@ setupArg sc sym ecRef tp =
       fail $ unwords ["Crucible extraction currently only supports Crucible base types", show tp]
   where
     freshGlobal cty sc_tp =
-      do i     <- scFreshGlobalVar sc
-         ecs   <- readIORef ecRef
+      do ecs <- readIORef ecRef
          let len = Seq.length ecs
-         let ec = EC i ("arg_"++show len) sc_tp
+         ec <- scFreshEC sc ("arg_"++show len) sc_tp
          writeIORef ecRef (ecs Seq.|> TypedExtCns cty ec)
          scFlatTermF sc (ExtCns ec)
 

src/SAWScript/Crucible/LLVM/MethodSpecIR.hs

@@ -120,8 +120,8 @@ import           Data.Parameterized.Some (Some(Some))
 import qualified Data.Parameterized.Map as MapF
 
 import qualified What4.Expr.Builder as B
-import           What4.Protocol.Online (OnlineSolver)
 import           What4.ProgramLoc (ProgramLoc)
+import           What4.Protocol.Online (OnlineSolver)
 
 import qualified Lang.Crucible.Backend.SAWCore as Crucible
   (SAWCoreBackend, saw_ctx, toSC, SAWCruciblePersonality)

src/SAWScript/Crucible/LLVM/Override.hs

@@ -684,7 +684,8 @@ refreshTerms sc ss =
      OM (termSub %= Map.union extension)
   where
     freshenTerm (TypedExtCns _cty ec) =
-      do new <- liftIO (scFreshGlobal sc (ecName ec) (ecType ec))
+      do new <- liftIO $ do i <- scFreshGlobalVar sc
+                            scExtCns sc (EC i (ecName ec) (ecType ec))
          return (ecVarIndex ec, new)
 
 ------------------------------------------------------------------------

src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

@@ -360,8 +360,7 @@ resolveSAWPred cc tm = do
      mx <- case getAllExts tm' of
              [] -> do
                -- Evaluate in SBV to test whether 'tm' is a concrete value
-               modmap <- scGetModuleMap sc
-               sbv <- SBV.toBool <$> SBV.sbvSolveBasic modmap Map.empty [] tm'
+               sbv <- SBV.toBool <$> SBV.sbvSolveBasic sc Map.empty mempty tm'
                return (SBV.svAsBool sbv)
              _ -> return Nothing
      case mx of
@@ -382,8 +381,7 @@ resolveSAWSymBV cc w tm =
      mx <- case getAllExts tm' of
              [] -> do
                -- Evaluate in SBV to test whether 'tm' is a concrete value
-               modmap <- scGetModuleMap sc
-               sbv <- SBV.toWord =<< SBV.sbvSolveBasic modmap Map.empty [] tm'
+               sbv <- SBV.toWord =<< SBV.sbvSolveBasic sc Map.empty mempty tm'
                return (SBV.svAsInteger sbv)
              _ -> return Nothing
      case mx of

src/SAWScript/JavaBuiltins.hs

@@ -26,6 +26,7 @@ import Data.Maybe (mapMaybe)
 import Data.IORef
 import qualified Data.Map as Map
 import Data.Time.Clock
+import qualified Data.Text as Text
 import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 
 import Language.JVM.Common
@@ -40,6 +41,7 @@ import Verifier.SAW.FiniteValue (FirstOrderValue)
 import Verifier.SAW.SCTypeCheck hiding (TypedTerm)
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.TypedTerm
+import Verifier.SAW.TypedAST (toShortName)
 import Verifier.SAW.CryptolEnv (schemaNoUser)
 
 import qualified SAWScript.CongruenceClosure as CC
@@ -327,7 +329,7 @@ mkMixedExpr t = do
   sc <- lift getSharedContext
   let exts = getAllExts t
       extNames = map ecName exts
-  jes <- mapM (getJavaExpr "mkMixedExpr") extNames
+  jes <- mapM (getJavaExpr "mkMixedExpr" . Text.unpack . toShortName) extNames -- TODO?????
   fn <- liftIO $ scAbstractExts sc exts t
   return $ LE $ LogicExpr fn (map fst jes)