crucible-llvm-0.7: src/Lang/Crucible/LLVM/Printf.hs
------------------------------------------------------------------------
-- |
-- Module : Lang.Crucible.LLVM.Printf
-- Description : Interpretation of 'printf' style conversion codes
-- Copyright : (c) Galois, Inc 2015-2016
-- License : BSD3
-- Maintainer : Rob Dockins <rdockins@galois.com>
-- Stability : provisional
--
-- A model of C's @printf@ function. This does not entirely conform to the C
-- standard's specification of @printf@; see @doc/limitations.md@ for the
-- specifics.
--
------------------------------------------------------------------------
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
module Lang.Crucible.LLVM.Printf
( PrintfFlag(..)
, PrintfLengthModifier(..)
, Case(..)
, IntFormat(..)
, FloatFormat(..)
, PrintfConversionType(..)
, PrintfDirective(..)
, parseDirectives
, ConversionDirective(..)
, PrintfOperations(..)
, executeDirectives
, formatInteger
, formatRational
) where
import Data.Char (toUpper)
import qualified Numeric as N
import Control.Applicative
import Data.Attoparsec.ByteString.Char8 hiding (take)
import qualified Data.ByteString as BS
import qualified Data.ByteString.Char8 as BSC
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Word
import qualified GHC.Stack as GHC
import Lang.Crucible.Panic (panic)
data PrintfFlag
= PrintfAlternateForm -- #
| PrintfZeroPadding -- 0
| PrintfNegativeWidth -- -
| PrintfPosSpace -- ' '
| PrintfPosPlus -- +
| PrintfThousandsSep -- '
deriving (Eq,Ord,Show)
data PrintfLengthModifier
= Len_Byte -- hh
| Len_Short -- h
| Len_Long -- l
| Len_LongLong -- ll
| Len_LongDouble -- L
| Len_IntMax -- j
| Len_PtrDiff -- t
| Len_Sizet -- z
| Len_NoMod -- <<no length modifier>>
deriving (Eq,Ord,Show)
data Case
= UpperCase
| LowerCase
deriving (Eq,Ord,Show)
data IntFormat
= IntFormat_SignedDecimal -- i,d
| IntFormat_UnsignedDecimal -- u
| IntFormat_Octal -- o
| IntFormat_Hex Case -- x,X
deriving (Eq,Ord,Show)
signedIntFormat :: IntFormat -> Bool
signedIntFormat IntFormat_SignedDecimal = True
signedIntFormat _ = False
data FloatFormat
= FloatFormat_Scientific Case -- e,E
| FloatFormat_Standard Case -- f,F
| FloatFormat_Auto Case -- g,G
| FloatFormat_Hex Case -- a,A
deriving (Eq,Ord,Show)
data PrintfConversionType
= Conversion_Integer IntFormat
| Conversion_Floating FloatFormat
| Conversion_Char -- c
| Conversion_String -- s
| Conversion_Pointer -- p
| Conversion_CountChars -- n
deriving (Eq,Ord,Show)
data PrintfDirective
= StringDirective BS.ByteString
| ConversionDirective ConversionDirective
deriving (Eq,Ord,Show)
data ConversionDirective = Conversion
{ printfAccessField :: Maybe Int
, printfFlags :: Set PrintfFlag
, printfMinWidth :: Int
, printfPrecision :: Maybe Int
, printfLengthMod :: PrintfLengthModifier
, printfType :: PrintfConversionType
}
deriving (Eq,Ord,Show)
data PrintfOperations m
= PrintfOperations
{ printfGetInteger :: Int -- Field number
-> Bool -- is Signed?
-> PrintfLengthModifier
-> m (Maybe Integer)
, printfGetFloat :: Int -- FieldNumber
-> PrintfLengthModifier
-> m (Maybe Rational)
, printfGetPointer :: Int -- FieldNumber
-> m String
, printfGetString :: Int -- FieldNumber
-> Maybe Int -- Number of chars to read; if Nothing, read until null terminator
-> m [Word8]
, printfSetInteger :: Int -- FieldNumber
-> PrintfLengthModifier
-> Int -- value to set
-> m ()
, printfUnsupported :: !(forall a. GHC.HasCallStack => String -> m a)
}
formatInteger
:: Maybe Integer
-> IntFormat
-> Int -- min width
-> Maybe Int -- precision
-> Set PrintfFlag
-> String
formatInteger mi fmt minwidth prec flags =
case mi of
Nothing ->
let n = max 4 (max minwidth (fromMaybe 0 prec))
in replicate n '?'
Just i -> do
case fmt of
IntFormat_SignedDecimal ->
formatSignedDec i minwidth prec flags
IntFormat_UnsignedDecimal ->
formatUnsignedDec i minwidth prec flags
IntFormat_Octal ->
formatOctal i minwidth prec flags
IntFormat_Hex c ->
formatHex i c minwidth prec flags
insertThousands :: Char -> String -> String
insertThousands sep = reverse . go . reverse
where
go (a:b:c:xs@(_:_)) = a:b:c:sep:go xs
go xs = xs
addLeadingZeros ::
Maybe Int -> -- precision
String ->
String
addLeadingZeros Nothing digits = digits
addLeadingZeros (Just p) digits =
let n = max 0 (p - length digits) in
replicate n '0' ++ digits
formatSignedDec
:: Integer -- value to format
-> Int -- minwidth
-> Maybe Int -- precision
-> Set PrintfFlag
-> String
formatSignedDec i minwidth prec flags = do
let sgn = if | i < 0 -> "-"
| Set.member PrintfPosPlus flags -> "+"
| Set.member PrintfPosSpace flags -> " "
| otherwise -> ""
let digits = N.showInt (abs i) []
let precdigits = addLeadingZeros prec digits
let sepdigits = if Set.member PrintfThousandsSep flags then
insertThousands ',' precdigits -- FIXME, get thousands separator from somewhere?
else
precdigits
let pad = max 0 (minwidth - length sepdigits - length sgn)
if | Set.member PrintfNegativeWidth flags ->
sgn ++ sepdigits ++ replicate pad ' '
| Set.member PrintfZeroPadding flags && prec == Nothing ->
-- FIXME? this interacts poorly with the thousands seperation flag...
sgn ++ replicate pad '0' ++ sepdigits
| otherwise ->
replicate pad ' ' ++ sgn ++ sepdigits
formatUnsignedDec
:: Integer -- value to format
-> Int -- minwidth
-> Maybe Int -- precision
-> Set PrintfFlag
-> String
formatUnsignedDec i minwidth prec flags = do
let digits = N.showInt (abs i) []
let precdigits = addLeadingZeros prec digits
let sepdigits = if Set.member PrintfThousandsSep flags then
insertThousands ',' precdigits -- FIXME, get thousands separator from somewhere?
else
precdigits
let pad = max 0 (minwidth - length sepdigits)
if | Set.member PrintfNegativeWidth flags ->
sepdigits ++ replicate pad ' '
| Set.member PrintfZeroPadding flags && prec == Nothing ->
-- FIXME? this interacts poorly with the thousands seperation flag...
replicate pad '0' ++ sepdigits
| otherwise ->
replicate pad ' ' ++ sepdigits
formatOctal
:: Integer -- value to format
-> Int -- minwidth
-> Maybe Int -- precision
-> Set PrintfFlag
-> String
formatOctal i minwidth prec flags = do
let digits = N.showOct (abs i) []
let precdigits = addLeadingZeros prec digits
let leadingPrecDigit =
case precdigits of
d:_ -> d
[] -> panic
"formatOctal"
["Octal-formatted number with no digits"]
let altdigits = if Set.member PrintfAlternateForm flags && leadingPrecDigit /= '0' then
'0':precdigits
else
precdigits
let pad = max 0 (minwidth - length altdigits)
if | Set.member PrintfNegativeWidth flags ->
altdigits ++ replicate pad ' '
| Set.member PrintfZeroPadding flags && prec == Nothing ->
replicate pad '0' ++ altdigits
| otherwise ->
replicate pad ' ' ++ altdigits
formatHex
:: Integer -- value to format
-> Case -- upper or lower case
-> Int -- minwidth
-> Maybe Int -- precision
-> Set PrintfFlag
-> String
formatHex i c minwidth prec flags = do
let digits = N.showHex (abs i) []
let precdigits = addLeadingZeros prec digits
-- Why only add "0x" when i is non-zero? I have no idea,
-- that's just what the docs say...
let altstring = if Set.member PrintfAlternateForm flags && i /= 0 then
"0x"
else
""
let pad = max 0 (minwidth - length precdigits - length altstring)
let padded = if | Set.member PrintfNegativeWidth flags ->
altstring ++ precdigits ++ replicate pad ' '
| Set.member PrintfZeroPadding flags && prec == Nothing ->
altstring ++ replicate pad '0' ++ precdigits
| otherwise ->
replicate pad ' ' ++ altstring ++ precdigits
case c of
UpperCase -> map toUpper padded
LowerCase -> padded
formatRational
:: Maybe Rational
-> FloatFormat
-> Int -- min width
-> Maybe Int -- precision
-> Set PrintfFlag
-> Either String String -- ^ Left indicates an error, right is OK
formatRational mr fmt minwidth prec flags =
case mr of
Nothing ->
let n = max 4 (min minwidth (fromMaybe 0 prec))
in return (replicate n '?')
Just r ->
-- FIXME, we ignore the thousands flag...
do let toCase c x = case c of
UpperCase -> map toUpper x
LowerCase -> x
let sgn = if | r < 0 -> "-"
| Set.member PrintfPosPlus flags -> "+"
| Set.member PrintfPosSpace flags -> " "
| otherwise -> ""
let dbl = N.fromRat (abs r) :: Double
let prec' = case prec of Nothing -> Just 6; _ -> prec
str <- case fmt of
FloatFormat_Scientific c ->
return $ toCase c $ N.showEFloat prec' dbl []
FloatFormat_Standard c ->
return $ toCase c $
if Set.member PrintfAlternateForm flags
then N.showFFloatAlt prec' dbl []
else N.showFFloat prec' dbl []
FloatFormat_Auto c ->
return $ toCase c $
if Set.member PrintfAlternateForm flags
then N.showGFloatAlt prec' dbl []
else N.showGFloat prec' dbl []
FloatFormat_Hex _c ->
-- FIXME, could probably implement this using N.floatToDigits...
Left "'a' and 'A' conversion codes not currently supported"
let pad = max 0 (minwidth - length str - length sgn)
return $
if | Set.member PrintfNegativeWidth flags ->
sgn ++ str ++ replicate pad ' '
| Set.member PrintfZeroPadding flags ->
sgn ++ replicate pad '0' ++ str
| otherwise ->
replicate pad ' ' ++ sgn ++ str
-- | Given a list of 'PrintfDirective's, compute the resulting 'BS.ByteString'
-- and its length.
--
-- We make an effort not to assume a particular text encoding for the
-- 'BS.ByteString' that this returns. Some parts of the implementation do use
-- functionality from "Data.ByteString.Char8", which is limited to the subset
-- of Unicode covered by code points 0-255. We believe these uses are justified,
-- however, and we have left comments explaining the reasoning behind each use.
executeDirectives :: forall m. Monad m
=> PrintfOperations m
-> [PrintfDirective]
-> m (BS.ByteString, Int)
executeDirectives ops = go id 0 0
where
go :: (BS.ByteString -> BS.ByteString) -> Int -> Int -> [PrintfDirective] -> m (BS.ByteString, Int)
go fstr !len !_fld [] = return (fstr BS.empty, len)
go fstr !len !fld ((StringDirective s):xs) = do
let len' = len + BS.length s
let fstr' = fstr . BS.append s
go fstr' len' fld xs
go fstr !len !fld (ConversionDirective d:xs) =
let fld' = fromMaybe (fld+1) (printfAccessField d) in
case printfType d of
Conversion_Integer fmt -> do
let sgn = signedIntFormat fmt
i <- printfGetInteger ops fld' sgn (printfLengthMod d)
-- The use of BSC.pack is fine here, as the output of formatInteger
-- consists solely of ASCII characters.
let istr = BSC.pack $ formatInteger i fmt (printfMinWidth d) (printfPrecision d) (printfFlags d)
let len' = len + BS.length istr
let fstr' = fstr . BS.append istr
go fstr' len' fld' xs
Conversion_Floating fmt -> do
r <- printfGetFloat ops fld' (printfLengthMod d)
-- The use of BSC.pack is fine here, as the output of formatRational
-- consists solely of ASCII characters.
rstr <- BSC.pack <$>
case formatRational r fmt
(printfMinWidth d)
(printfPrecision d)
(printfFlags d) of
Left err -> printfUnsupported ops err
Right a -> return a
let len' = len + BS.length rstr
let fstr' = fstr . BS.append rstr
go fstr' len' fld' xs
Conversion_String -> do
s <- BS.pack <$> printfGetString ops fld' (printfPrecision d)
let len' = len + BS.length s
let fstr' = fstr . BS.append s
go fstr' len' fld' xs
Conversion_Char -> do
let sgn = False -- unsigned
i <- printfGetInteger ops fld' sgn Len_NoMod
let c :: Char = maybe '?' (toEnum . fromInteger) i
let len' = len + 1
-- Note the use of BSC.cons here: this assumes on the assumption
-- that C strings are arrays of 1-byte characters.
let fstr' = fstr . BSC.cons c
go fstr' len' fld' xs
Conversion_Pointer -> do
-- Note the use of BSC.pack here: this assumes that the output of
-- printfGetPointer uses solely ASCII characters. For crux-llvm's
-- printf override, this is always the case, as pointers are
-- pretty-printed using the ppPtr function, which satisfies this
-- criterion.
pstr <- BSC.pack <$> printfGetPointer ops fld'
let len' = len + BS.length pstr
let fstr' = fstr . BS.append pstr
go fstr' len' fld' xs
Conversion_CountChars -> do
printfSetInteger ops fld' (printfLengthMod d) len
go fstr len fld' xs
parseDirectives :: [Word8] -> Either String [PrintfDirective]
parseDirectives xs =
parseOnly (parseFormatString <* endOfInput) (BS.pack xs)
parseFormatString :: Parser [PrintfDirective]
parseFormatString = many $ choice
[ StringDirective <$> takeWhile1 (/= '%')
, string "%%" >> return (StringDirective "%")
, parseConversion
]
parseConversion :: Parser PrintfDirective
parseConversion = do
_ <- char '%'
field <- option Nothing (Just <$>
do d <- decimal
_ <- char '$'
return d)
flags <- parseFlags Set.empty
width <- option 0 decimal
prec <- option Nothing (char '.' >> (Just <$> decimal))
len <- parseLenModifier
typ <- parseConversionType
return $ ConversionDirective $ Conversion
{ printfAccessField = field
, printfFlags = flags
, printfMinWidth = width
, printfPrecision = prec
, printfLengthMod = len
, printfType = typ
}
parseFlags :: Set PrintfFlag -> Parser (Set PrintfFlag)
parseFlags fs = choice
[ char '#' >> parseFlags (Set.insert PrintfAlternateForm fs)
, char '0' >> parseFlags (Set.insert PrintfZeroPadding fs)
, char '-' >> parseFlags (Set.insert PrintfNegativeWidth fs)
, char ' ' >> parseFlags (Set.insert PrintfPosSpace fs)
, char '+' >> parseFlags (Set.insert PrintfPosPlus fs)
, char '\'' >> parseFlags (Set.insert PrintfThousandsSep fs)
, return fs
]
parseLenModifier :: Parser PrintfLengthModifier
parseLenModifier = choice
[ string "hh" >> return Len_Byte
, string "h" >> return Len_Short
, string "ll" >> return Len_LongLong
, string "L" >> return Len_LongDouble
, string "l" >> return Len_Long
, string "j" >> return Len_IntMax
, string "t" >> return Len_PtrDiff
, string "z" >> return Len_Sizet
, return Len_NoMod
]
parseConversionType :: Parser PrintfConversionType
parseConversionType = choice
[ char 'd' >> return (Conversion_Integer IntFormat_SignedDecimal)
, char 'i' >> return (Conversion_Integer IntFormat_SignedDecimal)
, char 'u' >> return (Conversion_Integer IntFormat_UnsignedDecimal)
, char 'o' >> return (Conversion_Integer IntFormat_Octal)
, char 'x' >> return (Conversion_Integer (IntFormat_Hex LowerCase))
, char 'X' >> return (Conversion_Integer (IntFormat_Hex UpperCase))
, char 'e' >> return (Conversion_Floating (FloatFormat_Scientific LowerCase))
, char 'E' >> return (Conversion_Floating (FloatFormat_Scientific UpperCase))
, char 'f' >> return (Conversion_Floating (FloatFormat_Standard LowerCase))
, char 'F' >> return (Conversion_Floating (FloatFormat_Standard UpperCase))
, char 'g' >> return (Conversion_Floating (FloatFormat_Auto LowerCase))
, char 'G' >> return (Conversion_Floating (FloatFormat_Auto UpperCase))
, char 'a' >> return (Conversion_Floating (FloatFormat_Hex LowerCase))
, char 'A' >> return (Conversion_Floating (FloatFormat_Hex UpperCase))
, char 'c' >> return Conversion_Char
, char 's' >> return Conversion_String
, char 'p' >> return Conversion_Pointer
, char 'n' >> return Conversion_CountChars
]