Better line number reporting for monadic binds

saw-script.cabal

@@ -123,6 +123,7 @@ library
     SAWScript.Parser
     SAWScript.PathVC
     SAWScript.Proof
+    SAWScript.Position
     SAWScript.SBVParser
     SAWScript.SBVModel
     SAWScript.SAWCorePrimitives

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/AST.hs

@@ -37,7 +37,7 @@ module SAWScript.AST
        ) where
 
 import SAWScript.Token
-import SAWScript.Utils
+import SAWScript.Position (Pos(..), Positioned(..), maxSpan)
 
 import Data.Map (Map)
 import qualified Data.Map as Map

src/SAWScript/AutoMatch.hs

@@ -39,7 +39,7 @@ import qualified Cryptol.Parser.Position as Cryptol
 import qualified Cryptol.Utils.PP        as Cryptol
 import qualified Cryptol.Utils.Ident     as Cryptol (packIdent)
 import SAWScript.Builtins
---import SAWScript.Options
+import SAWScript.Position
 import SAWScript.Utils
 import SAWScript.TopLevel
 import SAWScript.Value

src/SAWScript/Builtins.hs

@@ -69,6 +69,8 @@ import Verifier.SAW.Rewriter
 import Verifier.SAW.Testing.Random (scRunTestsTFIO, scTestableType)
 import Verifier.SAW.TypedAST
 
+import SAWScript.Position
+
 -- cryptol-verifier
 import qualified Verifier.SAW.CryptolEnv as CEnv
 
@@ -115,7 +117,6 @@ import SAWScript.AST (getVal, pShow, Located(..))
 import SAWScript.Options as Opts
 import SAWScript.Proof
 import SAWScript.TopLevel
-import SAWScript.Utils
 import SAWScript.SAWCorePrimitives( bitblastPrimitives, sbvPrimitives, concretePrimitives )
 import qualified SAWScript.Value as SV
 import SAWScript.Value (ProofScript, printOutLnTop, AIGNetwork)

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
@@ -134,7 +133,7 @@ import SAWScript.Prover.SolverStats
 import SAWScript.Prover.Versions
 import SAWScript.TopLevel
 import SAWScript.Value
-import SAWScript.Utils as SS
+import SAWScript.Position as SS
 import SAWScript.Options
 
 import SAWScript.CrucibleMethodSpecIR
@@ -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/Exceptions.hs

@@ -3,9 +3,9 @@ module SAWScript.Exceptions (TypeErrors(..), failTypecheck) where
 
 import Control.Exception
 
+import SAWScript.Position (Pos(..), Positioned(..))
 import SAWScript.Utils
 
-
 newtype TypeErrors = TypeErrors [(Pos, String)]
 
 instance Show TypeErrors where

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/JVM/CrucibleBuiltins.hs

@@ -111,6 +111,7 @@ import SAWScript.Prover.SolverStats
 import SAWScript.TopLevel
 import SAWScript.Value
 import SAWScript.Utils as SS
+import qualified SAWScript.Position as SS
 import SAWScript.Options
 import SAWScript.CrucibleBuiltinsJVM (prepareClassTopLevel)
 
@@ -507,7 +508,7 @@ registerOverride opts cc _ctx top_loc cs =
      let c0 = head cs
      let cname = c0^.csClassName
      let mname = c0^.csMethodName
-     let pos = PosInternal "registerOverride"
+     let pos = SS.PosInternal "registerOverride"
      sc <- Crucible.saw_ctx <$> liftIO (readIORef (W4.sbStateManager sym))
 
      (mcls, meth) <- liftIO $ findMethod cb pos mname =<< lookupClass cb pos cname
@@ -547,7 +548,7 @@ verifySimulate opts cc mspec args assumes top_loc lemmas globals checkSat =
      let mname = mspec^.csMethodName
      let verbosity = simVerbose opts
      let personality = Crucible.SAWCruciblePersonality
-     let pos = PosInternal "verifySimulate"
+     let pos = SS.PosInternal "verifySimulate"
      let halloc = cc^.ccHandleAllocator
 
      -- executeCrucibleJVM

src/SAWScript/JavaBuiltins.hs

@@ -50,6 +50,7 @@ import SAWScript.JavaUtils
 
 import SAWScript.Builtins
 import SAWScript.Options
+import SAWScript.Position (Pos(..), renderDoc)
 import SAWScript.Proof
 import SAWScript.Utils
 import SAWScript.Value as SS

src/SAWScript/JavaExpr.hs

@@ -79,6 +79,7 @@ import Verifier.SAW.Recognizer
 import Verifier.SAW.SharedTerm
 
 import qualified SAWScript.CongruenceClosure as CC
+import SAWScript.Position
 import SAWScript.Utils
 
 import qualified Cryptol.TypeCheck.AST as Cryptol

src/SAWScript/JavaMethodSpec.hs

@@ -65,6 +65,7 @@ import SAWScript.JavaMethodSpecIR
 import SAWScript.JavaMethodSpec.Evaluator
 import SAWScript.JavaUtils
 import SAWScript.PathVC
+import SAWScript.Position (Pos(..))
 import SAWScript.Value (TopLevel, TopLevelRW(rwPPOpts), getTopLevelRW, io, printOutTop, printOutLnTop)
 import SAWScript.VerificationCheck
 

src/SAWScript/JavaMethodSpecIR.hs

@@ -79,6 +79,7 @@ import Verifier.SAW.TypedAST (ppTerm, defaultPPOpts)
 import qualified SAWScript.CongruenceClosure as CC
 import SAWScript.CongruenceClosure (CCSet)
 import SAWScript.JavaExpr
+import SAWScript.Position (Pos(..), Positioned(..))
 import SAWScript.Utils
 
 -- ExprActualTypeMap {{{1

src/SAWScript/Lexer.x

@@ -14,6 +14,7 @@ module SAWScript.Lexer
   ) where
 
 import SAWScript.Token
+import SAWScript.Position
 import SAWScript.Utils
 
 import Numeric

src/SAWScript/MGU.hs

@@ -18,7 +18,7 @@ module SAWScript.MGU
        ) where
 
 import SAWScript.AST
-import SAWScript.Utils (Pos(..), Positioned(..))
+import SAWScript.Position (Pos(..), Positioned(..))
 
 #if !MIN_VERSION_base(4,8,0)
 import Control.Applicative

src/SAWScript/Parser.y

@@ -21,6 +21,7 @@ import Data.Text (pack)
 import SAWScript.Token
 import SAWScript.Lexer
 import SAWScript.AST
+import SAWScript.Position
 import SAWScript.Utils
 
 import qualified Cryptol.Parser.AST as P