-----------------------------------------------------------------------
-- |
-- 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
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
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
Ord)

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

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

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

-- | A value with a source position associated.
data Posd v = Posd { forall v. Posd v -> Position
pos :: !Position
                   , forall v. Posd v -> v
pos_val :: !v
                   }
  deriving (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
<$ :: forall a b. a -> Posd b -> Posd a
$c<$ :: forall a b. a -> Posd b -> Posd a
fmap :: forall a b. (a -> b) -> Posd a -> Posd b
$cfmap :: forall a b. (a -> b) -> Posd a -> Posd b
Functor, 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 :: forall a. Num a => Posd a -> a
$cproduct :: forall a. Num a => Posd a -> a
sum :: forall a. Num a => Posd a -> a
$csum :: forall a. Num a => Posd a -> a
minimum :: forall a. Ord a => Posd a -> a
$cminimum :: forall a. Ord a => Posd a -> a
maximum :: forall a. Ord a => Posd a -> a
$cmaximum :: forall a. Ord a => Posd a -> a
elem :: forall a. Eq a => a -> Posd a -> Bool
$celem :: forall a. Eq a => a -> Posd a -> Bool
length :: forall a. Posd a -> Int
$clength :: forall a. Posd a -> Int
null :: forall a. Posd a -> Bool
$cnull :: forall a. Posd a -> Bool
toList :: forall a. Posd a -> [a]
$ctoList :: forall a. Posd a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Posd a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Posd a -> a
foldr1 :: forall a. (a -> a -> a) -> Posd a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Posd a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Posd a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Posd a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Posd a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Posd a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Posd a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Posd a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Posd a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Posd a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Posd a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Posd a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Posd a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Posd a -> m
fold :: forall m. Monoid m => Posd m -> m
$cfold :: forall m. Monoid m => Posd m -> m
Foldable, Functor Posd
Foldable Posd
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 :: forall (m :: Type -> Type) a. Monad m => Posd (m a) -> m (Posd a)
$csequence :: forall (m :: Type -> Type) a. Monad m => Posd (m a) -> m (Posd a)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(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 :: forall (f :: Type -> Type) a.
Applicative f =>
Posd (f a) -> f (Posd a)
$csequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
Posd (f a) -> f (Posd a)
traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(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)
Traversable, Int -> Posd v -> ShowS
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
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 = forall a. NFData a => a -> ()
rnf (forall v. Posd v -> Position
pos Posd v
p, 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
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
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
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
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