-----------------------------------------------------------------------
-- |
-- Module           : What4.ProgramLoc
-- Description      : Datatype for handling program locations
-- Copyright        : (c) Galois, Inc 2014-2020
-- License          : BSD3
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
-- Stability        : provisional
--
-- This module primarily defines the `Position` datatype for
-- handling program location data.  A program location may refer
-- either to a source file location (file name, line and column number),
-- a binary file location (file name and byte offset) or be a dummy
-- "internal" location assigned to generated program fragments.
------------------------------------------------------------------------
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
module What4.ProgramLoc
  ( Position(..)
  , sourcePos
  , startOfFile
  , ppNoFileName
  , Posd(..)
  , ProgramLoc
  , mkProgramLoc
  , initializationLoc
  , plFunction
  , plSourceLoc
    -- * Objects with a program location associated.
  , HasProgramLoc(..)
  ) where

import           Control.DeepSeq
import           Control.Lens
import           Data.Text (Text)
import qualified Data.Text as Text
import           Data.Word
import           Numeric (showHex)
import qualified Prettyprinter as PP

import           What4.FunctionName

------------------------------------------------------------------------
-- Position

data Position
     -- | A source position containing filename, line, and column.
   = SourcePos !Text !Int !Int
     -- | A binary position containing a filename and address in memory.
   | BinaryPos !Text !Word64
     -- | Some unstructured position information that doesn't fit into the other categories.
   | OtherPos !Text
     -- | Generated internally by the simulator, or otherwise unknown.
   | InternalPos
  deriving (Position -> Position -> Bool
(Position -> Position -> Bool)
-> (Position -> Position -> Bool) -> Eq Position
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Position -> Position -> Bool
$c/= :: Position -> Position -> Bool
== :: Position -> Position -> Bool
$c== :: Position -> Position -> Bool
Eq, Eq Position
Eq Position
-> (Position -> Position -> Ordering)
-> (Position -> Position -> Bool)
-> (Position -> Position -> Bool)
-> (Position -> Position -> Bool)
-> (Position -> Position -> Bool)
-> (Position -> Position -> Position)
-> (Position -> Position -> Position)
-> Ord Position
Position -> Position -> Bool
Position -> Position -> Ordering
Position -> Position -> Position
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Position -> Position -> Position
$cmin :: Position -> Position -> Position
max :: Position -> Position -> Position
$cmax :: Position -> Position -> Position
>= :: Position -> Position -> Bool
$c>= :: Position -> Position -> Bool
> :: Position -> Position -> Bool
$c> :: Position -> Position -> Bool
<= :: Position -> Position -> Bool
$c<= :: Position -> Position -> Bool
< :: Position -> Position -> Bool
$c< :: Position -> Position -> Bool
compare :: Position -> Position -> Ordering
$ccompare :: Position -> Position -> Ordering
$cp1Ord :: Eq Position
Ord)

instance Show Position where
  show :: Position -> String
show Position
p = Doc Any -> String
forall a. Show a => a -> String
show (Position -> Doc Any
forall a ann. Pretty a => a -> Doc ann
PP.pretty Position
p)

instance NFData Position where
  rnf :: Position -> ()
rnf (SourcePos Text
t Int
l Int
c) = (Text, Int, Int) -> ()
forall a. NFData a => a -> ()
rnf (Text
t,Int
l,Int
c)
  rnf (BinaryPos Text
t Word64
a)   = (Text, Word64) -> ()
forall a. NFData a => a -> ()
rnf (Text
t,Word64
a)
  rnf (OtherPos Text
t)      = Text -> ()
forall a. NFData a => a -> ()
rnf Text
t
  rnf Position
InternalPos       = ()

sourcePos :: FilePath -> Int -> Int -> Position
sourcePos :: String -> Int -> Int -> Position
sourcePos String
p Int
l Int
c = Text -> Int -> Int -> Position
SourcePos (String -> Text
Text.pack String
p) Int
l Int
c

startOfFile :: FilePath -> Position
startOfFile :: String -> Position
startOfFile String
path = String -> Int -> Int -> Position
sourcePos String
path Int
1 Int
0

instance PP.Pretty Position where
  pretty :: Position -> Doc ann
pretty (SourcePos Text
path Int
l Int
c) =
    Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Text
path
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Doc ann
forall ann. Doc ann
PP.colon Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Int
l
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Doc ann
forall ann. Doc ann
PP.colon Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Int
c
  pretty (BinaryPos Text
path Word64
addr) =
    Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Text
path Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Doc ann
forall ann. Doc ann
PP.colon Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<>
      String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"0x" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (Word64 -> ShowS
forall a. (Integral a, Show a) => a -> ShowS
showHex Word64
addr String
"")
  pretty (OtherPos Text
txt) = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Text
txt
  pretty Position
InternalPos = String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"internal"

ppNoFileName :: Position -> PP.Doc ann
ppNoFileName :: Position -> Doc ann
ppNoFileName (SourcePos Text
_ Int
l Int
c) =
  Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Int
l Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Doc ann
forall ann. Doc ann
PP.colon Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Int
c
ppNoFileName (BinaryPos Text
_ Word64
addr) =
  String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (Word64 -> ShowS
forall a. (Integral a, Show a) => a -> ShowS
showHex Word64
addr String
"")
ppNoFileName (OtherPos Text
msg) =
  Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Text
msg
ppNoFileName Position
InternalPos = String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"internal"

------------------------------------------------------------------------
-- Posd

-- | A value with a source position associated.
data Posd v = Posd { Posd v -> Position
pos :: !Position
                   , Posd v -> v
pos_val :: !v
                   }
  deriving (a -> Posd b -> Posd a
(a -> b) -> Posd a -> Posd b
(forall a b. (a -> b) -> Posd a -> Posd b)
-> (forall a b. a -> Posd b -> Posd a) -> Functor Posd
forall a b. a -> Posd b -> Posd a
forall a b. (a -> b) -> Posd a -> Posd b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Posd b -> Posd a
$c<$ :: forall a b. a -> Posd b -> Posd a
fmap :: (a -> b) -> Posd a -> Posd b
$cfmap :: forall a b. (a -> b) -> Posd a -> Posd b
Functor, Posd a -> Bool
(a -> m) -> Posd a -> m
(a -> b -> b) -> b -> Posd a -> b
(forall m. Monoid m => Posd m -> m)
-> (forall m a. Monoid m => (a -> m) -> Posd a -> m)
-> (forall m a. Monoid m => (a -> m) -> Posd a -> m)
-> (forall a b. (a -> b -> b) -> b -> Posd a -> b)
-> (forall a b. (a -> b -> b) -> b -> Posd a -> b)
-> (forall b a. (b -> a -> b) -> b -> Posd a -> b)
-> (forall b a. (b -> a -> b) -> b -> Posd a -> b)
-> (forall a. (a -> a -> a) -> Posd a -> a)
-> (forall a. (a -> a -> a) -> Posd a -> a)
-> (forall a. Posd a -> [a])
-> (forall a. Posd a -> Bool)
-> (forall a. Posd a -> Int)
-> (forall a. Eq a => a -> Posd a -> Bool)
-> (forall a. Ord a => Posd a -> a)
-> (forall a. Ord a => Posd a -> a)
-> (forall a. Num a => Posd a -> a)
-> (forall a. Num a => Posd a -> a)
-> Foldable Posd
forall a. Eq a => a -> Posd a -> Bool
forall a. Num a => Posd a -> a
forall a. Ord a => Posd a -> a
forall m. Monoid m => Posd m -> m
forall a. Posd a -> Bool
forall a. Posd a -> Int
forall a. Posd a -> [a]
forall a. (a -> a -> a) -> Posd a -> a
forall m a. Monoid m => (a -> m) -> Posd a -> m
forall b a. (b -> a -> b) -> b -> Posd a -> b
forall a b. (a -> b -> b) -> b -> Posd a -> b
forall (t :: Type -> Type).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Posd a -> a
$cproduct :: forall a. Num a => Posd a -> a
sum :: Posd a -> a
$csum :: forall a. Num a => Posd a -> a
minimum :: Posd a -> a
$cminimum :: forall a. Ord a => Posd a -> a
maximum :: Posd a -> a
$cmaximum :: forall a. Ord a => Posd a -> a
elem :: a -> Posd a -> Bool
$celem :: forall a. Eq a => a -> Posd a -> Bool
length :: Posd a -> Int
$clength :: forall a. Posd a -> Int
null :: Posd a -> Bool
$cnull :: forall a. Posd a -> Bool
toList :: Posd a -> [a]
$ctoList :: forall a. Posd a -> [a]
foldl1 :: (a -> a -> a) -> Posd a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Posd a -> a
foldr1 :: (a -> a -> a) -> Posd a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Posd a -> a
foldl' :: (b -> a -> b) -> b -> Posd a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Posd a -> b
foldl :: (b -> a -> b) -> b -> Posd a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Posd a -> b
foldr' :: (a -> b -> b) -> b -> Posd a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Posd a -> b
foldr :: (a -> b -> b) -> b -> Posd a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Posd a -> b
foldMap' :: (a -> m) -> Posd a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Posd a -> m
foldMap :: (a -> m) -> Posd a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Posd a -> m
fold :: Posd m -> m
$cfold :: forall m. Monoid m => Posd m -> m
Foldable, Functor Posd
Foldable Posd
Functor Posd
-> Foldable Posd
-> (forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> Posd a -> f (Posd b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    Posd (f a) -> f (Posd a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Posd a -> m (Posd b))
-> (forall (m :: Type -> Type) a.
    Monad m =>
    Posd (m a) -> m (Posd a))
-> Traversable Posd
(a -> f b) -> Posd a -> f (Posd b)
forall (t :: Type -> Type).
Functor t
-> Foldable t
-> (forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    t (f a) -> f (t a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: Type -> Type) a. Monad m => Posd (m a) -> m (Posd a)
forall (f :: Type -> Type) a.
Applicative f =>
Posd (f a) -> f (Posd a)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Posd a -> m (Posd b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Posd a -> f (Posd b)
sequence :: Posd (m a) -> m (Posd a)
$csequence :: forall (m :: Type -> Type) a. Monad m => Posd (m a) -> m (Posd a)
mapM :: (a -> m b) -> Posd a -> m (Posd b)
$cmapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Posd a -> m (Posd b)
sequenceA :: Posd (f a) -> f (Posd a)
$csequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
Posd (f a) -> f (Posd a)
traverse :: (a -> f b) -> Posd a -> f (Posd b)
$ctraverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Posd a -> f (Posd b)
$cp2Traversable :: Foldable Posd
$cp1Traversable :: Functor Posd
Traversable, Int -> Posd v -> ShowS
[Posd v] -> ShowS
Posd v -> String
(Int -> Posd v -> ShowS)
-> (Posd v -> String) -> ([Posd v] -> ShowS) -> Show (Posd v)
forall v. Show v => Int -> Posd v -> ShowS
forall v. Show v => [Posd v] -> ShowS
forall v. Show v => Posd v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Posd v] -> ShowS
$cshowList :: forall v. Show v => [Posd v] -> ShowS
show :: Posd v -> String
$cshow :: forall v. Show v => Posd v -> String
showsPrec :: Int -> Posd v -> ShowS
$cshowsPrec :: forall v. Show v => Int -> Posd v -> ShowS
Show, Posd v -> Posd v -> Bool
(Posd v -> Posd v -> Bool)
-> (Posd v -> Posd v -> Bool) -> Eq (Posd v)
forall v. Eq v => Posd v -> Posd v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Posd v -> Posd v -> Bool
$c/= :: forall v. Eq v => Posd v -> Posd v -> Bool
== :: Posd v -> Posd v -> Bool
$c== :: forall v. Eq v => Posd v -> Posd v -> Bool
Eq)

instance NFData v => NFData (Posd v) where
  rnf :: Posd v -> ()
rnf Posd v
p = (Position, v) -> ()
forall a. NFData a => a -> ()
rnf (Posd v -> Position
forall v. Posd v -> Position
pos Posd v
p, Posd v -> v
forall v. Posd v -> v
pos_val Posd v
p)

------------------------------------------------------------------------
-- ProgramLoc

-- | A very small type that contains a function and PC identifier.
data ProgramLoc
   = ProgramLoc { ProgramLoc -> FunctionName
plFunction :: {-# UNPACK #-} !FunctionName
                , ProgramLoc -> Position
plSourceLoc :: !Position
                }
 deriving (Int -> ProgramLoc -> ShowS
[ProgramLoc] -> ShowS
ProgramLoc -> String
(Int -> ProgramLoc -> ShowS)
-> (ProgramLoc -> String)
-> ([ProgramLoc] -> ShowS)
-> Show ProgramLoc
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProgramLoc] -> ShowS
$cshowList :: [ProgramLoc] -> ShowS
show :: ProgramLoc -> String
$cshow :: ProgramLoc -> String
showsPrec :: Int -> ProgramLoc -> ShowS
$cshowsPrec :: Int -> ProgramLoc -> ShowS
Show, ProgramLoc -> ProgramLoc -> Bool
(ProgramLoc -> ProgramLoc -> Bool)
-> (ProgramLoc -> ProgramLoc -> Bool) -> Eq ProgramLoc
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProgramLoc -> ProgramLoc -> Bool
$c/= :: ProgramLoc -> ProgramLoc -> Bool
== :: ProgramLoc -> ProgramLoc -> Bool
$c== :: ProgramLoc -> ProgramLoc -> Bool
Eq, Eq ProgramLoc
Eq ProgramLoc
-> (ProgramLoc -> ProgramLoc -> Ordering)
-> (ProgramLoc -> ProgramLoc -> Bool)
-> (ProgramLoc -> ProgramLoc -> Bool)
-> (ProgramLoc -> ProgramLoc -> Bool)
-> (ProgramLoc -> ProgramLoc -> Bool)
-> (ProgramLoc -> ProgramLoc -> ProgramLoc)
-> (ProgramLoc -> ProgramLoc -> ProgramLoc)
-> Ord ProgramLoc
ProgramLoc -> ProgramLoc -> Bool
ProgramLoc -> ProgramLoc -> Ordering
ProgramLoc -> ProgramLoc -> ProgramLoc
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ProgramLoc -> ProgramLoc -> ProgramLoc
$cmin :: ProgramLoc -> ProgramLoc -> ProgramLoc
max :: ProgramLoc -> ProgramLoc -> ProgramLoc
$cmax :: ProgramLoc -> ProgramLoc -> ProgramLoc
>= :: ProgramLoc -> ProgramLoc -> Bool
$c>= :: ProgramLoc -> ProgramLoc -> Bool
> :: ProgramLoc -> ProgramLoc -> Bool
$c> :: ProgramLoc -> ProgramLoc -> Bool
<= :: ProgramLoc -> ProgramLoc -> Bool
$c<= :: ProgramLoc -> ProgramLoc -> Bool
< :: ProgramLoc -> ProgramLoc -> Bool
$c< :: ProgramLoc -> ProgramLoc -> Bool
compare :: ProgramLoc -> ProgramLoc -> Ordering
$ccompare :: ProgramLoc -> ProgramLoc -> Ordering
$cp1Ord :: Eq ProgramLoc
Ord)

-- | Location for initialization code
initializationLoc :: ProgramLoc
initializationLoc :: ProgramLoc
initializationLoc = FunctionName -> Position -> ProgramLoc
ProgramLoc FunctionName
startFunctionName (String -> Position
startOfFile String
"")

-- | Make a program loc
mkProgramLoc :: FunctionName
             -> Position
             -> ProgramLoc
mkProgramLoc :: FunctionName -> Position -> ProgramLoc
mkProgramLoc = FunctionName -> Position -> ProgramLoc
ProgramLoc

------------------------------------------------------------------------
-- HasProgramLoc

class HasProgramLoc v where
  programLoc :: Lens' v ProgramLoc