Thread positions of monadic binds through CrucibleSetup

saw/SAWScript/REPL/Command.hs

@@ -32,7 +32,7 @@ module SAWScript.REPL.Command (
 
 import SAWScript.REPL.Monad
 import SAWScript.REPL.Trie
-import SAWScript.Utils (getPos)
+import SAWScript.Position (getPos)
 
 import Cryptol.Parser (ParseError())
 import Cryptol.Utils.PP

src/SAWScript/CrucibleBuiltins.hs

@@ -68,7 +68,6 @@ import           Data.List
 import           Data.List.Extra (groupOn, nubOrd)
 import qualified Data.List.NonEmpty as NE
 import           Data.Maybe
-import           Data.Monoid ((<>))
 import           Data.String
 import           Data.Map (Map)
 import qualified Data.Map as Map
@@ -270,7 +269,8 @@ createMethodSpec verificationArgs bic opts lm nm setup = do
     let sym = cc^.ccBackend
     let llmod = cc^.ccLLVMModule
 
-    setupLoc <- toW4Loc "_SAW_verify_prestate" <$> getPosition
+    pos <- getPosition
+    let setupLoc = toW4Loc "_SAW_verify_prestate" pos
 
     let est0 = case defOrDecl of
                  Left def -> initialCrucibleSetupState cc def setupLoc parent
@@ -279,6 +279,7 @@ createMethodSpec verificationArgs bic opts lm nm setup = do
 
     -- execute commands of the method spec
     liftIO $ W4.setCurrentProgramLoc sym setupLoc
+
     methodSpec <- view csMethodSpec <$> execStateT (runCrucibleSetupM setup) st0
 
     void $ io $ checkSpecReturnType cc methodSpec
@@ -1225,7 +1226,7 @@ crucible_fresh_expanded_val ::
 crucible_fresh_expanded_val bic _opts lty = CrucibleSetupM $
   do let sc = biSharedContext bic
      lty' <- memTypeForLLVMType bic lty
-     loc <- toW4Loc "crucible_fresh_expanded_val" <$> lift getPosition
+     loc <- getW4Position "crucible_fresh_expanded_val"
      constructExpandedSetupValue sc loc lty'
 
 
@@ -1292,7 +1293,7 @@ crucible_alloc ::
   CrucibleSetupM SetupValue
 crucible_alloc _bic _opt lty = CrucibleSetupM $
   do let ?dl = Crucible.llvmDataLayout ?lc
-     loc <- toW4Loc "crucible_alloc" <$> lift getPosition
+     loc <- getW4Position "crucible_alloc"
      memTy <- case Crucible.liftMemType lty of
        Right s -> return s
        Left err -> fail $ unlines [ "unsupported type in crucible_alloc: " ++ show (L.ppType lty)
@@ -1314,7 +1315,7 @@ crucible_alloc_readonly ::
   CrucibleSetupM SetupValue
 crucible_alloc_readonly _bic _opt lty = CrucibleSetupM $
   do let ?dl = Crucible.llvmDataLayout ?lc
-     loc <- toW4Loc "crucible_alloc_readonly" <$> lift getPosition
+     loc <- getW4Position "crucible_alloc_readonly"
      memTy <- case Crucible.liftMemType lty of
        Right s -> return s
        Left err -> fail $ unlines [ "unsupported type in crucible_alloc: " ++ show (L.ppType lty)
@@ -1335,7 +1336,7 @@ crucible_fresh_pointer ::
   CrucibleSetupM SetupValue
 crucible_fresh_pointer bic _opt lty = CrucibleSetupM $
   do memTy <- memTypeForLLVMType bic lty
-     loc <- toW4Loc "crucible_fresh_pointer" <$> lift getPosition
+     loc <- getW4Position "crucible_fresh_pointer"
      constructFreshPointer (llvmTypeAlias lty) loc memTy
 
 constructFreshPointer :: Maybe Crucible.Ident -> W4.ProgramLoc -> Crucible.MemType -> CrucibleSetup arch SetupValue
@@ -1357,7 +1358,7 @@ crucible_points_to ::
   CrucibleSetupM ()
 crucible_points_to typed _bic _opt ptr val = CrucibleSetupM $
   do cc <- getCrucibleContext
-     loc <- toW4Loc "crucible_points_to" <$> lift getPosition
+     loc <- getW4Position "crucible_points_to"
      Crucible.llvmPtrWidth (cc^.ccLLVMContext) $ \wptr -> Crucible.withPtrWidth wptr $
        do let ?lc = cc^.ccTypeCtx
           st <- get
@@ -1382,12 +1383,6 @@ crucible_points_to typed _bic _opt ptr val = CrucibleSetupM $
           when typed (checkMemTypeCompatibility lhsTy valTy)
           addPointsTo (PointsTo loc ptr val)
 
-toW4Loc :: Text.Text -> SS.Pos -> W4.ProgramLoc
-toW4Loc fnm SS.Unknown          = W4.mkProgramLoc (W4.functionNameFromText fnm) W4.InternalPos
-toW4Loc fnm SS.PosREPL          = W4.mkProgramLoc (W4.functionNameFromText (fnm <> " <REPL>")) W4.InternalPos
-toW4Loc fnm (SS.PosInternal nm) = W4.mkProgramLoc (W4.functionNameFromText (fnm <> " " <> fromString nm)) W4.InternalPos
-toW4Loc fnm (SS.Range file sl sc _el _ec) = W4.mkProgramLoc (W4.functionNameFromText fnm) (W4.SourcePos (fromString file) sl sc)
-
 crucible_equal ::
   BuiltinContext ->
   Options        ->
@@ -1407,7 +1402,7 @@ crucible_equal _bic _opt val1 val2 = CrucibleSetupM $
        , show ty1
        , show ty2
        ]
-     loc <- toW4Loc "crucible_equal" <$> lift getPosition
+     loc <- getW4Position "crucible_equal"
      addCondition (SetupCond_Equal loc val1 val2)
 
 crucible_precond ::
@@ -1417,7 +1412,7 @@ crucible_precond p = CrucibleSetupM $ do
   st <- get
   when (st^.csPrePost == PostState) $
     fail "attempt to use `crucible_precond` in post state"
-  loc <- toW4Loc "crucible_precond" <$> lift getPosition
+  loc <- getW4Position "crucible_precond"
   addCondition (SetupCond_Pred loc p)
 
 crucible_postcond ::
@@ -1427,7 +1422,7 @@ crucible_postcond p = CrucibleSetupM $ do
   st <- get
   when (st^.csPrePost == PreState) $
     fail "attempt to use `crucible_postcond` in pre state"
-  loc <- toW4Loc "crucible_postcond" <$> lift getPosition
+  loc <- getW4Position "crucible_postcond"
   addCondition (SetupCond_Pred loc p)
 
 crucible_execute_func :: BuiltinContext
@@ -1472,7 +1467,7 @@ crucible_ghost_value ::
   TypedTerm                           ->
   CrucibleSetupM ()
 crucible_ghost_value _bic _opt ghost val = CrucibleSetupM $
-  do loc <- toW4Loc "crucible_ghost_value" <$> lift getPosition
+  do loc <- getW4Position "crucible_ghost_value"
      addCondition (SetupCond_Ghost loc ghost val)
 
 crucible_spec_solvers :: CrucibleMethodSpecIR -> [String]

src/SAWScript/Interpreter.hs

@@ -45,7 +45,7 @@ import System.FilePath (takeDirectory)
 import System.Process (readProcess)
 
 import qualified SAWScript.AST as SS
-import qualified SAWScript.Utils as SS
+import qualified SAWScript.Position as SS
 import SAWScript.AST (Located(..),Import(..))
 import SAWScript.Builtins
 import SAWScript.Exceptions (failTypecheck)
@@ -251,10 +251,10 @@ locToInput l = CEnv.InputText { CEnv.inpText = getVal l
   where
   (file,ln,col) =
     case locatedPos l of
-      Range f sl sc _ _ -> (f,sl, sc)
-      PosInternal s -> (s,1,1)
-      PosREPL       -> ("<interactive>", 1, 1)
-      Unknown       -> ("Unknown", 1, 1)
+      SS.Range f sl sc _ _ -> (f,sl, sc)
+      SS.PosInternal s -> (s,1,1)
+      SS.PosREPL       -> ("<interactive>", 1, 1)
+      SS.Unknown       -> ("Unknown", 1, 1)
 
 interpretDecl :: LocalEnv -> SS.Decl -> TopLevel LocalEnv
 interpretDecl env (SS.Decl _ pat mt expr) = do
@@ -281,10 +281,10 @@ interpretStmts env stmts =
     case stmts of
       [] -> fail "empty block"
       [SS.StmtBind _ (SS.PWild _) _ e] -> interpret env e
-      SS.StmtBind _ pat _ e : ss ->
+      SS.StmtBind pos pat _ e : ss ->
           do v1 <- interpret env e
              let f v = interpretStmts (bindPatternLocal pat Nothing v env) ss
-             bindValue v1 (VLambda f)
+             bindValue pos v1 (VLambda f)
       SS.StmtLet _ bs : ss -> interpret env (SS.Let bs (SS.Block ss))
       SS.StmtCode _ s : ss ->
           do sc <- getSharedContext
@@ -309,13 +309,13 @@ processStmtBind printBinds pat _mc expr = do -- mx mt
         SS.PWild t -> (Nothing, t)
         SS.PVar x t -> (Just x, t)
         _ -> (Nothing, Nothing)
-  let it = SS.Located "it" "it" PosREPL
+  let it = SS.Located "it" "it" SS.PosREPL
   let lname = maybe it id mx
   let ctx = SS.tContext SS.TopLevel
   let expr' = case mt of
                 Nothing -> expr
                 Just t -> SS.TSig expr (SS.tBlock ctx t)
-  let decl = SS.Decl (getPos expr) pat Nothing expr'
+  let decl = SS.Decl (SS.getPos expr) pat Nothing expr'
   rw <- getTopLevelRW
   let opts = rwPPOpts rw
 
@@ -392,7 +392,7 @@ interpretFile file = do
   mapM_ stmtWithPrint stmts
   where
     stmtWithPrint s = do let withPos str = unlines $
-                                           ("[output] at " ++ show (getPos s) ++ ": ") :
+                                           ("[output] at " ++ show (SS.getPos s) ++ ": ") :
                                              map (\l -> "\t"  ++ l) (lines str)
                          showLoc <- printShowPos <$> getOptions
                          if showLoc
@@ -405,7 +405,7 @@ interpretFile file = do
 interpretMain :: TopLevel ()
 interpretMain = do
   rw <- getTopLevelRW
-  let mainName = Located "main" "main" (PosInternal "entry")
+  let mainName = Located "main" "main" (SS.PosInternal "entry")
   case Map.lookup mainName (rwValues rw) of
     Nothing -> return () -- fail "No 'main' defined"
     Just v -> fromValue v
@@ -2154,7 +2154,7 @@ primitives = Map.fromList
 filterAvail ::
   Set PrimitiveLifecycle ->
   Map SS.LName Primitive ->
-  Map SS.LName Primitive 
+  Map SS.LName Primitive
 filterAvail primsAvail =
   Map.filter (\p -> primLife p `Set.member` primsAvail)
 
@@ -2186,4 +2186,4 @@ primDocEnv primsAvail =
                 ] ++ primDoc p
 
 qualify :: String -> Located SS.Name
-qualify s = Located s s (PosInternal "coreEnv")
+qualify s = Located s s (SS.PosInternal "coreEnv")

src/SAWScript/Position.hs

@@ -9,6 +9,8 @@ Stability   : provisional
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
 module SAWScript.Position where
@@ -19,8 +21,12 @@ import Data.List (intercalate)
 import GHC.Generics (Generic)
 import System.Directory (makeRelativeToCurrentDirectory)
 import System.FilePath (makeRelative, isAbsolute, (</>), takeDirectory)
+import qualified Data.Text as Text
 import qualified Text.PrettyPrint.ANSI.Leijen as PP hiding ((</>), (<$>))
 
+import qualified What4.ProgramLoc as W4
+import qualified What4.FunctionName as W4
+
 -- Pos ------------------------------------------------------------------------
 
 data Pos = Range !FilePath -- file
@@ -90,6 +96,17 @@ instance Show Pos where
   show Unknown               = "unknown"
   show (PosInternal s)       = "[internal:" ++ s ++ "]"
   show PosREPL               = "REPL"
+
+
+toW4Loc :: Text.Text -> Pos -> W4.ProgramLoc
+toW4Loc fnm =
+  \case
+    Unknown -> mkLoc fnm W4.InternalPos
+    PosREPL -> mkLoc (fnm <> " <REPL>") W4.InternalPos
+    PosInternal nm -> mkLoc (fnm <> " " <> Text.pack nm) W4.InternalPos
+    Range file sl sc _el _ec ->
+      mkLoc fnm (W4.SourcePos (Text.pack file) sl sc)
+  where mkLoc nm = W4.mkProgramLoc (W4.functionNameFromText nm)
 
 -- Positioned -----------------------------------------------------------------