Atoms.hs

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings#-}

-- | Atoms used by the Crucible CFG concrete syntax.
module Lang.Crucible.Syntax.Atoms
  (
    -- * The atom datatype
    Atomic(..)
  , atom
    -- * Individual atoms
  , AtomName(..)
  , LabelName(..)
  , RegName(..)
  , FunName(..)
  , GlobalName(..)
  , Keyword(..)
  ) where

import Control.Applicative

import Data.Char
import Data.Functor
import Data.Ratio
import Data.Text (Text)
import qualified Data.Text as T

import Lang.Crucible.Syntax.SExpr
import Numeric
import qualified Prettyprinter as PP

import Text.Megaparsec as MP hiding (many, some)
import Text.Megaparsec.Char

-- | The name of an atom (non-keyword identifier)
newtype AtomName = AtomName Text deriving (Eq, Ord, PP.Pretty, Show)
-- | The name of a label (identifier followed by colon)
newtype LabelName = LabelName Text deriving (Eq, Ord, PP.Pretty, Show)
-- | The name of a register (dollar sign followed by identifier)
newtype RegName = RegName Text deriving (Eq, Ord, PP.Pretty, Show)
-- | The name of a function (at-sign followed by identifier)
newtype FunName = FunName Text deriving (Eq, Ord, PP.Pretty, Show)
-- | The name of a global variable (two dollar signs followed by identifier)
newtype GlobalName = GlobalName Text deriving (Eq, Ord, PP.Pretty, Show)

-- | Individual language keywords (reserved identifiers)
data Keyword = Defun | DefBlock | DefGlobal | Declare | Extern
             | Registers
             | Start
             | SetGlobal
             | SetRef | DropRef_
             | Plus | Minus | Times | Div | Negate | Abs
             | Just_ | Nothing_ | FromJust
             | Inj | Proj
             | AnyT | UnitT | BoolT | NatT | IntegerT | RealT | ComplexRealT | CharT | StringT
             | BitvectorT | VectorT | SequenceT | FPT | FunT | MaybeT | VariantT | StructT | RefT
             | Half_ | Float_ | Double_ | Quad_ | X86_80_ | DoubleDouble_
             | Unicode_ | Char8_ | Char16_
             | The
             | Equalp | Integerp
             | If
             | Not_ | And_ | Or_ | Xor_
             | Mod
             | Lt | Le
             | Show
             | StringConcat_ | StringEmpty_ | StringLength_
             | ToAny | FromAny
             | VectorLit_ | VectorReplicate_ | VectorIsEmpty_ | VectorSize_
             | VectorGetEntry_ | VectorSetEntry_ | VectorCons_
             | MkStruct_ | GetField_ | SetField_
             | SequenceNil_ | SequenceCons_ | SequenceAppend_
             | SequenceIsNil_ | SequenceLength_
             | SequenceHead_ | SequenceTail_ | SequenceUncons_
             | Deref | Ref | EmptyRef
             | Jump_ | Return_ | Branch_ | MaybeBranch_ | TailCall_ | Error_ | Output_ | Case
             | Print_ | PrintLn_
             | Let | Fresh
             | Assert_ | Assume_
             | SetRegister
             | Funcall
             | Breakpoint_
             | BV | BVConcat_ | BVSelect_ | BVTrunc_
             | BVZext_ | BVSext_ | BVNonzero_ | BoolToBV_
             | BVCarry_ | BVSCarry_ | BVSBorrow_
             | BVNot_ | BVAnd_ | BVOr_ | BVXor_ | BVShl_ | BVLshr_ | BVAshr_
             | Sle | Slt | Sdiv | Smod | ZeroExt | SignExt
             | RNE_ | RNA_ | RTP_ | RTN_ | RTZ_
             | FPToUBV_ | FPToSBV_ | UBVToFP_ | SBVToFP_ | BinaryToFP_ | FPToBinary_
             | FPToReal_ | RealToFP_
  deriving (Eq, Ord)

keywords :: [(Text, Keyword)]
keywords =
    -- function/block defintion
  [ ("defun" , Defun)
  , ("start" , Start)
  , ("defblock", DefBlock)
  , ("defglobal", DefGlobal)
  , ("declare", Declare)
  , ("extern", Extern)
  , ("registers", Registers)

    -- statements
  , ("let", Let)
  , ("set-global!", SetGlobal)
  , ("set-ref!", SetRef)
  , ("drop-ref!", DropRef_)
  , ("fresh", Fresh)
  , ("jump" , Jump_)
  , ("case", Case)
  , ("return" , Return_)
  , ("branch" , Branch_)
  , ("maybe-branch" , MaybeBranch_)
  , ("tail-call" , TailCall_)
  , ("error", Error_)
  , ("output", Output_)
  , ("print" , Print_)
  , ("println" , PrintLn_)
  , ("Ref", RefT)
  , ("deref", Deref)
  , ("ref", Ref)
  , ("empty-ref", EmptyRef)
  , ("set-register!", SetRegister)
  , ("assert!", Assert_)
  , ("assume!", Assume_)
  , ("funcall", Funcall)
  , ("breakpoint", Breakpoint_)

    -- types
  , ("Any" , AnyT)
  , ("Unit" , UnitT)
  , ("Bool" , BoolT)
  , ("Nat" , NatT)
  , ("Integer" , IntegerT)
  , ("FP", FPT)
  , ("Real" , RealT)
  , ("ComplexReal" , ComplexRealT)
  , ("Char" , CharT)
  , ("String" , StringT)
  , ("Bitvector" , BitvectorT)
  , ("Vector", VectorT)
  , ("Sequence", SequenceT)
  , ("->", FunT)
  , ("Maybe", MaybeT)
  , ("Variant", VariantT)
  , ("Struct", StructT)

    -- string sorts
  , ("Unicode", Unicode_)
  , ("Char16", Char16_)
  , ("Char8", Char8_)

    -- floating-point variants
  , ("Half", Half_)
  , ("Float", Float_)
  , ("Double", Double_)
  , ("Quad", Quad_)
  , ("X86_80", X86_80_)
  , ("DoubleDouble", DoubleDouble_)

    -- misc
  , ("the" , The)
  , ("equal?" , Equalp)
  , ("if" , If)

    -- ANY types
  , ("to-any", ToAny)
  , ("from-any", FromAny)

    -- booleans
  , ("not" , Not_)
  , ("and" , And_)
  , ("or" , Or_)
  , ("xor" , Xor_)

    -- arithmetic
  , ("+" , Plus)
  , ("-" , Minus)
  , ("*" , Times)
  , ("/" , Div)
  , ("<" , Lt)
  , ("<=" , Le)
  , ("<=$" , Sle)
  , ("<$" , Slt)
  , ("/$" , Sdiv)
  , ("smod", Smod)
  , ("negate", Negate)
  , ("abs", Abs)
  , ("mod" , Mod)
  , ("integer?" , Integerp)

    -- Variants
  , ("inj", Inj)
  , ("proj", Proj)

    -- Structs
  , ("struct", MkStruct_)
  , ("get-field", GetField_)
  , ("set-field", SetField_)

    -- Maybe
  , ("just" , Just_)
  , ("nothing" , Nothing_)
  , ("from-just" , FromJust)

    -- Vectors
  , ("vector", VectorLit_)
  , ("vector-replicate", VectorReplicate_)
  , ("vector-empty?", VectorIsEmpty_)
  , ("vector-size", VectorSize_)
  , ("vector-get", VectorGetEntry_)
  , ("vector-set", VectorSetEntry_)
  , ("vector-cons", VectorCons_)

    -- Sequences
  , ("seq-nil", SequenceNil_)
  , ("seq-cons", SequenceCons_)
  , ("seq-append", SequenceAppend_)
  , ("seq-nil?", SequenceIsNil_)
  , ("seq-length", SequenceLength_)
  , ("seq-head", SequenceHead_)
  , ("seq-tail", SequenceTail_)
  , ("seq-uncons", SequenceUncons_)

    -- strings
  , ("show", Show)
  , ("string-concat", StringConcat_)
  , ("string-empty", StringEmpty_)
  , ("string-length", StringLength_)

    -- bitvector
  , ("bv", BV)
  , ("bv-concat", BVConcat_)
  , ("bv-select", BVSelect_)
  , ("bv-trunc", BVTrunc_)
  , ("zero-extend", BVZext_)
  , ("sign-extend", BVSext_)
  , ("bv-nonzero", BVNonzero_)
  , ("bool-to-bv", BoolToBV_)
  , ("bv-carry", BVCarry_)
  , ("bv-scarry", BVSCarry_)
  , ("bv-sborrow", BVSBorrow_)
  , ("bv-not", BVNot_)
  , ("bv-and", BVAnd_)
  , ("bv-or", BVOr_)
  , ("bv-xor", BVXor_)
  , ("shl", BVShl_)
  , ("lshr", BVLshr_)
  , ("ashr", BVAshr_)

    -- floating-point
  , ("fp-to-ubv", FPToUBV_)
  , ("fp-to-sbv", FPToSBV_)
  , ("ubv-to-fp", UBVToFP_)
  , ("sbv-to-fp", SBVToFP_)
  , ("fp-to-binary", FPToBinary_)
  , ("binary-to-fp", BinaryToFP_)
  , ("real-to-fp", RealToFP_)
  , ("fp-to-real", FPToReal_)
  , ("rne" , RNE_)
  , ("rna" , RNA_)
  , ("rtp" , RTP_)
  , ("rtn" , RTN_)
  , ("rtz" , RTZ_)
  ]

instance Show Keyword where
  show k = case [str | (str, k') <- keywords, k == k'] of
             [] -> "UNKNOWN KW"
             (s:_) -> T.unpack s


-- | The atoms of the language
data Atomic = Kw !Keyword -- ^ Keywords are all the built-in operators and expression formers
            | Lbl !LabelName -- ^ Labels, but not the trailing colon
            | At !AtomName -- ^ Atom names (which look like Scheme symbols)
            | Rg !RegName -- ^ Registers, whose names have a leading single $
            | Gl !GlobalName -- ^ Global variables, whose names have a leading double $$
            | Fn !FunName -- ^ Function names, minus the leading @
            | Int !Integer -- ^ Literal integers
            | Rat !Rational -- ^ Literal rational numbers
            | Bool !Bool   -- ^ Literal Booleans
            | StrLit !Text -- ^ Literal strings
  deriving (Eq, Ord, Show)


instance IsAtom Atomic where
  showAtom (Kw s) = T.pack (show s)
  showAtom (Lbl (LabelName l)) = l <> ":"
  showAtom (Rg (RegName r)) = "$" <> r
  showAtom (Gl (GlobalName r)) = "$$" <> r
  showAtom (At (AtomName a)) = a
  showAtom (Fn (FunName a)) = "@" <> a
  showAtom (Int i) = T.pack (show i)
  showAtom (Rat r) = T.pack (show (numerator r) ++ "/" ++ show (denominator r))
  showAtom (Bool b) = if b then "#t" else "#f"
  showAtom (StrLit s) = T.pack $ show s

-- | Parse an atom
atom :: Parser Atomic
atom =  try (Lbl . LabelName <$> identifier <* char ':')
    <|> Fn . FunName <$> (char '@' *> identifier)
    <|> (char '$' *> ((char '$' *> (Gl . GlobalName <$> identifier)) <|> Rg . RegName <$> identifier))
    <|> try (mkNum <$> signedPrefixedNumber <*> ((Just <$> (try (char '/') *> prefixedNumber)) <|> pure Nothing))
    <|> kwOrAtom
    <|> char '#' *>  ((char 't' <|> char 'T') $> Bool True <|> (char 'f' <|> char 'F') $> Bool False)
    <|> char '"' *> (StrLit . T.pack <$> stringContents)
  where
    mkNum x Nothing = Int x
    mkNum x (Just y) = Rat (x % y)

stringContents :: Parser [Char]
stringContents =  (char '\\' *> ((:) <$> escapeChar <*> stringContents))
              <|> (char '"' $> [])
              <|> ((:) <$> satisfy (const True) <*> stringContents)

escapeChar :: Parser Char
escapeChar =  (char '\\' *> pure '\\')
          <|> (char '"' *> pure '"')
          <|> (char 'n' *> pure '\n')
          <|> (char 't' *> pure '\t')
          <?> "valid escape character"

kwOrAtom :: Parser Atomic
kwOrAtom = do x <- identifier
              return $ maybe (At (AtomName x)) Kw (lookup x keywords)


signedPrefixedNumber :: (Eq a, Num a) => Parser a
signedPrefixedNumber =
  char '+' *> prefixedNumber <|>
  char '-' *> (negate <$> prefixedNumber) <|>
  prefixedNumber

prefixedNumber :: (Eq a, Num a) => Parser a
prefixedNumber = try (char '0' *> maybehex) <|> decimal
  where decimal = fromInteger . read <$> some (satisfy isDigit <?> "decimal digit")
        maybehex = char 'x' *> hex <|> return 0
        hex = reading $ readHex <$> some (satisfy (\c -> isDigit c || elem c ("abcdefABCDEF" :: String)) <?> "hex digit")
        reading p =
          p >>=
            \case
              [(x, "")] -> pure x
              _ -> empty