crucible-syntax (empty) → 0.4.1
raw patch · 12 files changed
+4366/−0 lines, 12 filesdep +basedep +bv-sizeddep +containers
Dependencies added: base, bv-sized, containers, crucible, crucible-syntax, directory, filepath, lens, megaparsec, mtl, parameterized-utils, prettyprinter, tasty, tasty-golden, tasty-hunit, text, transformers, vector, what4
Files
- CHANGELOG.md +83/−0
- LICENSE +30/−0
- README.txt +135/−0
- crucible-syntax.cabal +142/−0
- src/Lang/Crucible/Syntax/Atoms.hs +344/−0
- src/Lang/Crucible/Syntax/Concrete.hs +2280/−0
- src/Lang/Crucible/Syntax/ExprParse.hs +282/−0
- src/Lang/Crucible/Syntax/Monad.hs +524/−0
- src/Lang/Crucible/Syntax/Overrides.hs +68/−0
- src/Lang/Crucible/Syntax/Prog.hs +87/−0
- src/Lang/Crucible/Syntax/SExpr.hs +192/−0
- test/Tests.hs +199/−0
+ CHANGELOG.md view
@@ -0,0 +1,83 @@++# 0.4.1 -- 2025-03-21++* Add a `Pretty` instance for ExprError.++* Allow exotic characters (including Unicode symbols) in fresh atom+names instead of having them be restricted to plain text identifiers.++# 0.4 -- 2024-02-05++* The type `ACFG` has been removed in favor of `Lang.Crucible.CFG.Reg.AnyCFG`,+ which serves a similar purpose (hiding the argument and return types). The+ CFG argument and return types can be recovered via+ `Lang.Crucible.CFG.Reg.{cfgArgTypes,cfgReturnType}`.+* `crucible-syntax` now supports simulating CFGs with language-specific syntax+ extensions:++ * `SimulateProgramHooks` now has a `setupHook` field that can run an arbitrary+ override action before simulation. (For example, this is used in+ `crucible-llvm-syntax` to initialize the LLVM memory global variable.)+ * `SimulateProgramHooks` now has an extra `ext` type variable so that hooks+ can be extension-specific.+* `execCommand` and related data types in `Lang.Crucible.Syntax.Prog` have been+ split off into a separate `crucible-cli` library.++# 0.3++* The return type of `prog`:++ ```hs+ TopParser s (Map GlobalName (Pair TypeRepr GlobalVar), [ACFG ext])+ ```++ Has been changed to:++ ```hs+ TopParser s (ParsedProgram ext)+ ```++ Where the `parsedProgGlobals :: Map GlobalName (Some GlobalVar)` and+ `parsedProgCFGs :: [ACFG ext]` fields of `ParsedProgram` now serve the roles+ previously filled by the first and second fields of the returned tuple. (Note+ that `Pair TypeRepr GlobalVar` has been simplified to `Some GlobalVar`, as+ the `TypeRepr` of a `GlobalVar` can be retrieved through its `globalType`+ field.)+* The type of `simulateProgram`'s last argument:++ ```hs+ simulateProgram+ :: ...+ -> (forall p sym ext t st fs. (IsSymInterface sym, sym ~ (ExprBuilder t st fs)) =>+ sym -> HandleAllocator -> IO [(FnBinding p sym ext,Position)])+ -> ...+ ```++ Has changed to the following:++ ```hs+ simulateProgram+ :: ...+ -> SimulateProgramHooks+ -> ...+ ```++ Where the `setupOverridesHook` field of `SimulateProgramHooks` now serves the+ role previously filled by the function argument.++* `crucible-syntax` now supports _forward declarations_. A forward declaration+ is like a function, but lacking a body, and is useful for situations where+ one does not know what the implementation of a function will be until after+ the `.cbl` file is parsed. See the `crucible-syntax` `README` for more+ information.++ There is also now an `extern` keyword, that acts like a forward declaration+ for global variables.++# 0.2++* Various functions now take a `?parserHooks :: ParserHooks ext` implicit+ argument, which supports arbitrary syntax extensions. Various data types now+ also have an additional `ext` type parameter, which represents the type of+ the parser extension being used. If you do not care about parser extensions,+ a reasonable default choice is `?parserHooks = defaultParserHooks`.
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2013-2022 Galois Inc.+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above copyright+ notice, this list of conditions and the following disclaimer in+ the documentation and/or other materials provided with the+ distribution.++ * Neither the name of Galois, Inc. nor the names of its contributors+ may be used to endorse or promote products derived from this+ software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER+OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.txt view
@@ -0,0 +1,135 @@+This project defines a concrete syntax for a certain subset of the+registerized Crucible CFGs.++Some features are intentionally omitted, because they require+compile-time additions to Crucible in the form of type class+instances. In particular, there is no syntax for:++ * Recursive types++ * Extensions++ * Concrete types+++How to use+++General syntax++The basic syntax is based on a simplified variant of Lisp+S-expressions, without support for dotted pairs or special syntax for+quote or quasiquote. A syntactic form is either an atom or matching+opening and closing parentheses with a whitespace-delimited sequence+of syntactic forms between them.+++The atoms are as follows:++ * Identifiers are either keywords or Crucible atom names. Every+ identifier that is not a language keyword is a Crucible atom+ name. Identifiers consist of a letter-like character followed by+ zero or more digits or letter-like characters. Letter-like+ characters are those considered letters by Unicode, or any of the+ characters <, >, =, +, -, *, /, !, _, \, or ?.++ The keywords are documented below, under each special form.++ * Function names consist of an @ character followed by an identifier.++ * Register names consist of a $ character followed by an identifier.++ * Numbers consist of an optional '+' or '-' followed by an unsigned+ number and an optional denominator. Unsigned numbers are either+ decimal literals, octal literals, or hexadecimal literals, using+ the typical syntax with a 0-prefix. A denominator is a '/'+ character followed by an unsigned number.++ * Boolean literals are #t or #T and #f or #F.++ * String literals are delimited by double-quotes, and support+ escaping with \.+++Line comments are preceded by ;, and block comments are delimited by+#| and |#.+++Functions++A program consists of a sequence of function definitions. A function+definition is a form that begins with the keyword "defun", followed by+a function name, argument list, return type, and body. A function name+is a function name atom. An argument list is a form that contains zero+or more argument specs. An argument spec is a two-element form, where+the first is a Crucible atom name, and the second is a form that+denotes a type. A return type is a form that denotes a type.++A function body consists of an optional list of registers, a start+block, and zero or more further blocks. A list of registers is a form+that begins with the keyword "registers" and is followed by zero or+more register specifications. A register specification is a form+containing an atom name and a type.++Blocks consist of the defblock keyword followed by a block body. Block+bodies are zero or more ordinary statements followed by a terminating+statement. The first block must begin with "start" instead of+"defblock". In the future, the restriction that the start block comes+first may be relaxed.++Forward declarations++A forward declaration is a form that begins with the keyword "declare",+followed by a function name, argument list, and return type. A forward+declaration is like a function but without the function body. Forward+declarations are useful in situations where you do not know the definition+of a function ahead of time, but you will know it at some point after parsing+the program. It is the responsibility of the client to ensure that forward+declarations are resolved to Crucible definitions before being invoked.++Global variables++A global variable is a form that begins with the keyword "defglobal", followed+by an identifier prefixed with two dollar signs (e.g., $$global-name) as well+as a type. A global variable is a mutable reference that scopes over all of the+functions defined in the program. The value of a global variable can be set+with the "set-global!" form.++A program can reference a global variable defined externally by using an extern+declaration. An extern declaration is exactly like a "defglobal" declaration,+but using the "extern" keyword instead of "defglobal". The difference between+an extern and a normal global variable is that the value of an extern may+already have been set by the time that the .cbl file which declares the extern+uses it. It is the responsibility of the client to ensure that externs are+inserted into the Crucible symbolic global state before being accessed.++Types++si ::= 'Unicode' | 'Char16' | 'Char8'++fi ::= 'Half' | 'Float' | 'Double' | 'Quad'+ | 'X86_80' | 'DoubleDouble'++t ::= 'Any' | 'Unit' | 'Bool' | 'Nat' | 'Integer' | 'Real'+ | 'ComplexReal' | 'Char' | '(' 'String' si ')'+ | '(' 'FP' fi ')' | '(' 'BitVector' n ')'+ | '(' '->' t ... t ')' | '(' 'Maybe' t ')'+ | '(' 'Sequence' t ')' | '(' 'Vector' t ')' | '(' 'Ref' t ')'+ | '(' 'Struct' t ... t ')' | '(' 'Variant' t ... t ')'+++Expressions++++Registers+++Blocks+++Statements++++
+ crucible-syntax.cabal view
@@ -0,0 +1,142 @@+Cabal-version: 2.2+Name: crucible-syntax+Version: 0.4.1+Author: Galois Inc.+Maintainer: dtc@galois.com+Build-type: Simple+License: BSD-3-Clause+License-file: LICENSE+Category: Language+Synopsis: A syntax for reading and writing Crucible control-flow graphs+Description:+ This package provides a syntax for directly constructing Crucible+ control-flow graphs, as well as for observing them.++extra-doc-files: README.txt, CHANGELOG.md+extra-source-files:++common shared+ -- Specifying -Wall and -Werror can cause the project to fail to build on+ -- newer versions of GHC simply due to new warnings being added to -Wall. To+ -- prevent this from happening we manually list which warnings should be+ -- considered errors. We also list some warnings that are not in -Wall, though+ -- try to avoid "opinionated" warnings (though this judgement is clearly+ -- subjective).+ --+ -- Warnings are grouped by the GHC version that introduced them, and then+ -- alphabetically.+ --+ -- A list of warnings and the GHC version in which they were introduced is+ -- available here:+ -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html++ -- Since GHC 8.10 or earlier:+ ghc-options:+ -Wall+ -Werror=compat-unqualified-imports+ -Werror=deferred-type-errors+ -Werror=deprecated-flags+ -Werror=deprecations+ -Werror=deriving-defaults+ -Werror=dodgy-foreign-imports+ -Werror=duplicate-exports+ -Werror=empty-enumerations+ -Werror=identities+ -Werror=inaccessible-code+ -Werror=incomplete-patterns+ -Werror=incomplete-record-updates+ -Werror=incomplete-uni-patterns+ -Werror=inline-rule-shadowing+ -Werror=missed-extra-shared-lib+ -Werror=missing-exported-signatures+ -Werror=missing-fields+ -Werror=missing-home-modules+ -Werror=missing-methods+ -Werror=overflowed-literals+ -Werror=overlapping-patterns+ -Werror=partial-fields+ -Werror=partial-type-signatures+ -Werror=simplifiable-class-constraints+ -Werror=star-binder+ -Werror=star-is-type+ -Werror=tabs+ -Werror=typed-holes+ -Werror=unrecognised-pragmas+ -Werror=unrecognised-warning-flags+ -Werror=unsupported-calling-conventions+ -Werror=unsupported-llvm-version+ -Werror=unticked-promoted-constructors+ -Werror=unused-imports+ -Werror=warnings-deprecations+ -Werror=wrong-do-bind++ if impl(ghc >= 9.2)+ ghc-options:+ -Werror=ambiguous-fields+ -Werror=operator-whitespace+ -Werror=operator-whitespace-ext-conflict+ -Werror=redundant-bang-patterns++ if impl(ghc >= 9.4)+ ghc-options:+ -Werror=forall-identifier+ -Werror=misplaced-pragmas+ -Werror=redundant-strictness-flags+ -Werror=type-equality-out-of-scope+ -Werror=type-equality-requires-operators++ ghc-prof-options: -O2 -fprof-auto-top+ default-language: Haskell2010++library+ default-language: Haskell2010++ build-depends:+ base >= 4.9 && < 4.20,+ bv-sized >= 1.0.0,+ containers,+ crucible >= 0.1,+ lens,+ mtl,+ parameterized-utils >= 0.1.7,+ prettyprinter >= 1.7.0,+ megaparsec >= 7.0 && < 9.7,+ text,+ transformers,+ vector,+ what4++ hs-source-dirs: src++ exposed-modules:+ Lang.Crucible.Syntax.Atoms+ Lang.Crucible.Syntax.Concrete+ Lang.Crucible.Syntax.SExpr+ Lang.Crucible.Syntax.Overrides+ Lang.Crucible.Syntax.ExprParse+ Lang.Crucible.Syntax.Monad+ Lang.Crucible.Syntax.Prog++ ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns+ ghc-prof-options: -O2 -fprof-auto-top++test-suite crucible-syntax-tests+ import: shared+ type: exitcode-stdio-1.0+ main-is: Tests.hs+ hs-source-dirs: test+ build-depends:+ base,+ containers,+ crucible,+ crucible-syntax,+ directory,+ filepath,+ megaparsec,+ parameterized-utils,+ tasty,+ tasty-golden,+ tasty-hunit,+ text,+ what4+
+ src/Lang/Crucible/Syntax/Atoms.hs view
@@ -0,0 +1,344 @@+{-# 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
+ src/Lang/Crucible/Syntax/Concrete.hs view
@@ -0,0 +1,2280 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE LiberalTypeSynonyms #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}++module Lang.Crucible.Syntax.Concrete+ ( -- * Errors+ ExprErr(..)+ -- * Parsing and Results+ , ParserHooks(..)+ , ParsedProgram(..)+ , defaultParserHooks+ , top+ , cfgs+ , prog+ -- * Low level parsing operations+ , SyntaxState(..)+ , atomName+ , freshAtom+ , nat+ , string+ , isType+ , operands+ , BoundedNat(..)+ , PosNat+ , posNat+ , someAssign+ -- * Rules for pretty-printing language syntax+ , printExpr+ )+where++import Prelude hiding (fail)++import Control.Lens hiding (cons, backwards)+import Control.Applicative+import Control.Monad (MonadPlus(..), forM, join)+import Control.Monad.Error.Class (MonadError(..))+import Control.Monad.Identity ()+import Control.Monad.IO.Class (MonadIO(..))+import Control.Monad.Reader (MonadReader, ReaderT(..))+import Control.Monad.State.Strict (MonadState(..), StateT(..))+import Control.Monad.Trans.Class (MonadTrans(..))+import Control.Monad.Trans.Except (ExceptT(..))+import Control.Monad.Writer.Strict (MonadWriter(..), WriterT(..))++import Lang.Crucible.Types++import qualified Data.BitVector.Sized as BV+import Data.Foldable+import Data.Functor+import qualified Data.Functor.Product as Functor+import Data.Kind (Type)+import Data.Maybe+import Data.Parameterized.Some(Some(..))+import Data.Parameterized.Pair (Pair(..))+import Data.Parameterized.TraversableFC+import Data.Parameterized.Classes+import Data.Parameterized.Nonce ( NonceGenerator, Nonce+ , freshNonce )+import qualified Data.Parameterized.Context as Ctx+import Data.Map (Map)+import qualified Data.Map as Map+import qualified Data.Sequence as Seq+import Data.Text (Text)+import qualified Data.Text as T+import qualified Data.Vector as V+import Numeric.Natural+import qualified Prettyprinter as PP++import Lang.Crucible.Syntax.ExprParse hiding (SyntaxError)+import qualified Lang.Crucible.Syntax.ExprParse as SP+import Lang.Crucible.Syntax.Monad++import What4.ProgramLoc+import What4.FunctionName+import What4.Symbol+import What4.Utils.StringLiteral++import Lang.Crucible.Syntax.SExpr (Syntax, pattern L, pattern A, toText, PrintRules(..), PrintStyle(..), syntaxPos, withPosFrom, showAtom)+import Lang.Crucible.Syntax.Atoms hiding (atom)++import Lang.Crucible.CFG.Reg hiding (globalName)+import Lang.Crucible.CFG.Expr++import Lang.Crucible.FunctionHandle++import Numeric.Natural ()+import qualified Data.Set as Set++liftSyntaxParse :: (MonadError (ExprErr s) m, MonadIO m)+ => SyntaxParse Atomic a -> AST s -> m a+liftSyntaxParse p ast =+ liftIO (syntaxParseIO p ast) >>= \case+ Left e -> throwError (SyntaxParseError e)+ Right v -> return v++type AST s = Syntax Atomic++++printExpr :: AST s -> Text+printExpr = toText (PrintRules rules)+ where rules (Kw Defun) = Just (Special 3)+ rules (Kw DefBlock) = Just (Special 1)+ rules (Kw Start) = Just (Special 1)+ rules (Kw Registers) = Just (Special 0)+ rules _ = Nothing++data E ext s t where+ EAtom :: !(Atom s t) -> E ext s t+ EReg :: !Position -> !(Reg s t) -> E ext s t+ EGlob :: !Position -> !(GlobalVar t) -> E ext s t+ EDeref :: !Position -> !(E ext s (ReferenceType t)) -> E ext s t+ EApp :: !(App ext (E ext s) t) -> E ext s t++data SomeExpr ext s where+ SomeE :: TypeRepr t -> E ext s t -> SomeExpr ext s+ SomeOverloaded :: AST s -> Keyword -> [SomeExpr ext s] -> SomeExpr ext s+ SomeIntLiteral :: AST s -> Integer -> SomeExpr ext s++data SomeBVExpr ext s where+ SomeBVExpr :: (1 <= w) => NatRepr w -> E ext s (BVType w) -> SomeBVExpr ext s++data ExprErr s where+ TrivialErr :: Position -> ExprErr s+ Errs :: ExprErr s -> ExprErr s -> ExprErr s+ DuplicateAtom :: Position -> AtomName -> ExprErr s+ DuplicateLabel :: Position -> LabelName -> ExprErr s+ EmptyBlock :: Position -> ExprErr s+ NotGlobal :: Position -> AST s -> ExprErr s+ InvalidRegister :: Position -> AST s -> ExprErr s+ SyntaxParseError :: SP.SyntaxError Atomic -> ExprErr s++deriving instance Show (ExprErr s)++instance Semigroup (ExprErr s) where+ (<>) = Errs++instance Monoid (ExprErr s) where+ mempty = TrivialErr (OtherPos "mempty")++instance PP.Pretty (ExprErr s) where+ pretty =+ \case+ TrivialErr p ->+ "Trivial error at" PP.<+> PP.viaShow p+ Errs e1 e2 ->+ PP.vcat ["Multiple errors:" , PP.pretty e1 , PP.pretty e2]+ DuplicateAtom p a ->+ PP.hsep ["Duplicate atom", backticks (PP.pretty a), "at", PP.viaShow p]+ DuplicateLabel p l ->+ PP.hsep ["Duplicate label", backticks (PP.pretty l), "at", PP.viaShow p]+ EmptyBlock p ->+ "Empty block at" PP.<+> PP.viaShow p+ NotGlobal p _ast ->+ "Expected a global at" PP.<+> PP.viaShow p+ InvalidRegister p _ast ->+ "Expected a register at" PP.<+> PP.viaShow p+ SyntaxParseError err ->+ PP.pretty (printSyntaxError err)+ where backticks = PP.enclose "`" "`"++-- | ParserHooks enables support for arbitrary syntax extensions by allowing+-- users to supply their own parsers for types and syntax extensions.+data ParserHooks ext = ParserHooks {+ -- | extensionTypeParser is called for all type specifications and enables+ -- the addition of new types to crucible-syntax.+ extensionTypeParser :: forall m. MonadSyntax Atomic m => m (Some TypeRepr)++ -- | extensionParser is called when parsing statements and let bindings+ -- (everywhere function calls are supported) and enables the addition of+ -- syntax extensions to crucible-syntax.+ , extensionParser+ :: forall s m+ . ( MonadSyntax Atomic m+ , MonadWriter [Posd (Stmt ext s)] m+ , MonadState (SyntaxState s) m+ , MonadIO m+ , IsSyntaxExtension ext+ , ?parserHooks :: ParserHooks ext+ -- ParserHooks instance to use recursively when parsing.+ )+ => m (Some (Atom s))+ -- ^ The atom computed from evaluating the syntax extension.+}++-- | A ParserHooks instance that adds no extensions to the crucible-syntax+-- language.+defaultParserHooks :: ParserHooks ()+defaultParserHooks = ParserHooks empty empty++-- | The results of parsing a program.+data ParsedProgram ext = ParsedProgram+ { parsedProgGlobals :: Map GlobalName (Some GlobalVar)+ -- ^ The parsed @defglobal@s.+ , parsedProgExterns :: Map GlobalName (Some GlobalVar)+ -- ^ For each parsed @extern@, map its name to its global variable. It is+ -- the responsibility of the caller to insert each global variable into+ -- the 'SymGlobalState' alongside an appropriate 'RegValue'.+ , parsedProgCFGs :: [AnyCFG ext]+ -- ^ The CFGs for each parsed @defun@.+ , parsedProgForwardDecs :: Map FunctionName SomeHandle+ -- ^ For each parsed @declare@, map its name to its function handle. It is+ -- the responsibility of the caller to register each handle with an+ -- appropriate 'FnState'.+ }+++kw :: MonadSyntax Atomic m => Keyword -> m ()+kw k = describe ("the keyword " <> showAtom (Kw k)) (atom (Kw k))++int :: MonadSyntax Atomic m => m Integer+int = sideCondition "integer literal" numeric atomic+ where numeric (Int i) = Just i+ numeric _ = Nothing++nat :: MonadSyntax Atomic m => m Natural+nat = sideCondition "natural literal" isNat atomic+ where isNat (Int i) | i >= 0 = Just (fromInteger i)+ isNat _ = Nothing++labelName :: MonadSyntax Atomic m => m LabelName+labelName = sideCondition "label name" lbl atomic+ where lbl (Lbl l) = Just l+ lbl _ = Nothing++regName :: MonadSyntax Atomic m => m RegName+regName = sideCondition "register name" reg atomic+ where reg (Rg rn) = Just rn+ reg _ = Nothing++globalName :: MonadSyntax Atomic m => m GlobalName+globalName = sideCondition "name of global variable" glob atomic+ where glob (Gl x) = Just x+ glob _ = Nothing+++rational :: MonadSyntax Atomic m => m Rational+rational = sideCondition "rational number literal" numeric atomic+ where numeric (Rat r) = Just r+ numeric _ = Nothing+++string :: MonadSyntax Atomic m => m Text+string = sideCondition "string literal" stringy atomic+ where stringy (StrLit t) = Just t+ stringy _ = Nothing++atomName :: MonadSyntax Atomic m => m AtomName+atomName = sideCondition "Crucible atom literal" isCAtom atomic+ where isCAtom (At a) = Just a+ isCAtom _ = Nothing++roundingMode :: MonadSyntax Atomic m => m RoundingMode+roundingMode = describe "rounding mode" $+ asum [ kw RNE_ $> RNE+ , kw RNA_ $> RNA+ , kw RTP_ $> RTP+ , kw RTN_ $> RTN+ , kw RTZ_ $> RTZ+ ]++fpinfo :: MonadSyntax Atomic m => m (Some FloatInfoRepr)+fpinfo = asum [ kw Half_ $> Some HalfFloatRepr+ , kw Float_ $> Some SingleFloatRepr+ , kw Double_ $> Some DoubleFloatRepr+ , kw Quad_ $> Some QuadFloatRepr+ , kw X86_80_ $> Some X86_80FloatRepr+ , kw DoubleDouble_ $> Some DoubleDoubleFloatRepr+ ]++bool :: MonadSyntax Atomic m => m Bool+bool = sideCondition "Boolean literal" isBool atomic+ where isBool (Bool b) = Just b+ isBool _ = Nothing++funName :: MonadSyntax Atomic m => m FunctionName+funName = functionNameFromText <$> sideCondition "function name literal" isFn atomic+ where isFn (Fn (FunName n)) = Just n+ isFn _ = Nothing++toCtx :: forall f . [Some f] -> Some (Ctx.Assignment f)+toCtx fs = toCtx' (reverse fs)+ where toCtx' :: [Some f] -> Some (Ctx.Assignment f)+ toCtx' [] = Some Ctx.empty+ toCtx' (Some x : (toCtx' -> Some xs)) =+ Some $ Ctx.extend xs x++unary :: MonadSyntax Atomic m => Keyword -> m a -> m a+unary k p = followedBy (kw k) (commit *> cons p emptyList) <&> fst++binary :: MonadSyntax Atomic m => Keyword -> m a -> m b -> m (a, b)+binary k p1 p2 = followedBy (kw k) (commit *> cons p1 (cons p2 emptyList)) <&> \(x, (y, ())) -> (x, y)+++mkFunRepr :: [Some TypeRepr] -> Some TypeRepr -> Some TypeRepr+mkFunRepr (toCtx -> Some doms) (Some ran) = Some $ FunctionHandleRepr doms ran++repUntilLast :: MonadSyntax Atomic m => m a -> m ([a], a)+repUntilLast sp = describe "zero or more followed by one" $ repUntilLast' sp+ where repUntilLast' p =+ (cons p emptyList <&> \(x, ()) -> ([], x)) <|>+ (cons p (repUntilLast' p) <&> \(x, (xs, lst)) -> (x:xs, lst))++_isBaseType :: ( ?parserHooks :: ParserHooks ext, MonadSyntax Atomic m )+ => m (Some BaseTypeRepr)+_isBaseType =+ describe "base type" $+ do Some tp <- isType+ case asBaseType tp of+ NotBaseType -> empty+ AsBaseType bt -> return (Some bt)++_isFloatingType :: ( ?parserHooks :: ParserHooks ext, MonadSyntax Atomic m )+ => m (Some FloatInfoRepr)+_isFloatingType =+ describe "floating-point type" $+ do Some tp <- isType+ case tp of+ FloatRepr fi -> return (Some fi)+ _ -> empty++data BoundedNat bnd =+ forall w. (bnd <= w) => BoundedNat (NatRepr w)++type PosNat = BoundedNat 1++posNat :: MonadSyntax Atomic m => m PosNat+posNat =+ do i <- sideCondition "positive nat literal" checkPosNat nat+ maybe empty return $ do Some x <- return $ mkNatRepr i+ LeqProof <- isPosNat x+ return $ BoundedNat x+ where checkPosNat i | i > 0 = Just i+ checkPosNat _ = Nothing++natRepr :: MonadSyntax Atomic m => m (Some NatRepr)+natRepr = mkNatRepr <$> nat++stringSort :: MonadSyntax Atomic m => m (Some StringInfoRepr)+stringSort =+ later $ describe "string sort" $+ asum [ kw Unicode_ $> Some UnicodeRepr+ , kw Char16_ $> Some Char16Repr+ , kw Char8_ $> Some Char8Repr+ ]++isType :: ( ?parserHooks :: ParserHooks ext, MonadSyntax Atomic m )+ => m (Some TypeRepr)+isType =+ describe "type" $ call+ (atomicType <|> stringT <|> vector <|> seqt <|> ref <|> bv <|> fp <|> fun <|> maybeT <|> var <|> struct <|> (extensionTypeParser ?parserHooks))++ where+ atomicType =+ later $ describe "atomic type" $+ asum [ kw AnyT $> Some AnyRepr+ , kw UnitT $> Some UnitRepr+ , kw BoolT $> Some BoolRepr+ , kw NatT $> Some NatRepr+ , kw IntegerT $> Some IntegerRepr+ , kw RealT $> Some RealValRepr+ , kw ComplexRealT $> Some ComplexRealRepr+ , kw CharT $> Some CharRepr+ ]+ vector = unary VectorT isType <&> \(Some t) -> Some (VectorRepr t)+ seqt = unary SequenceT isType <&> \(Some t) -> Some (SequenceRepr t)+ ref = unary RefT isType <&> \(Some t) -> Some (ReferenceRepr t)+ bv :: MonadSyntax Atomic m => m (Some TypeRepr)+ bv = do BoundedNat len <- unary BitvectorT posNat+ return $ Some $ BVRepr len++ fp :: MonadSyntax Atomic m => m (Some TypeRepr)+ fp = do Some fpi <- unary FPT fpinfo+ return $ Some $ FloatRepr fpi++ fun :: MonadSyntax Atomic m => m (Some TypeRepr)+ fun = cons (kw FunT) (repUntilLast isType) <&> \((), (args, ret)) -> mkFunRepr args ret++ stringT :: MonadSyntax Atomic m => m (Some TypeRepr)+ stringT = unary StringT stringSort <&> \(Some si) -> Some (StringRepr si)++ maybeT = unary MaybeT isType <&> \(Some t) -> Some (MaybeRepr t)++ var :: MonadSyntax Atomic m => m (Some TypeRepr)+ var = cons (kw VariantT) (rep isType) <&> \((), toCtx -> Some tys) -> Some (VariantRepr tys)++ struct :: MonadSyntax Atomic m => m (Some TypeRepr)+ struct = cons (kw StructT) (rep isType) <&> \((), toCtx -> Some tys) -> Some (StructRepr tys)++someExprType :: SomeExpr ext s -> Maybe (Some TypeRepr)+someExprType (SomeE tpr _) = Just (Some tpr)+someExprType _ = Nothing+++findJointType :: Maybe (Some TypeRepr) -> [SomeExpr ext s] -> Maybe (Some TypeRepr)+findJointType = foldr (\y x -> f x (someExprType y))+ where+ f Nothing y = y+ f x@(Just _) _ = x++evalOverloaded :: forall m s t ext. MonadSyntax Atomic m => AST s -> TypeRepr t -> Keyword -> [SomeExpr ext s] -> m (E ext s t)+evalOverloaded ast tpr k = withFocus ast .+ case (k, tpr) of+ (Plus, NatRepr) -> nary NatAdd (NatLit 0)+ (Plus, IntegerRepr) -> nary IntAdd (IntLit 0)+ (Plus, RealValRepr) -> nary RealAdd (RationalLit 0)+ (Plus, BVRepr w) -> nary (BVAdd w) (BVLit w (BV.zero w))++ (Times, NatRepr) -> nary NatMul (NatLit 1)+ (Times, IntegerRepr) -> nary IntMul (IntLit 1)+ (Times, RealValRepr) -> nary RealMul (RationalLit 1)+ (Times, BVRepr w) -> nary (BVMul w) (BVLit w (BV.one w))++ (Minus, NatRepr) -> bin NatSub+ (Minus, IntegerRepr) -> bin IntSub+ (Minus, RealValRepr) -> bin RealSub+ (Minus, BVRepr w) -> bin (BVSub w)++ (Div, NatRepr) -> bin NatDiv+ (Div, IntegerRepr) -> bin IntDiv+ (Div, RealValRepr) -> bin RealDiv+ (Div, BVRepr w) -> bin (BVUdiv w)++ (Mod, NatRepr) -> bin NatMod+ (Mod, IntegerRepr) -> bin IntMod+ (Mod, RealValRepr) -> bin RealMod+ (Mod, BVRepr w) -> bin (BVUrem w)++ (Negate, IntegerRepr) -> u IntNeg+ (Negate, RealValRepr) -> u RealNeg+ (Negate, BVRepr w) -> u (BVNeg w)++ (Abs, IntegerRepr) -> u IntAbs++ _ -> \_ -> later $ describe ("operation at type " <> T.pack (show tpr)) $ empty+ where+ u :: (E ext s t -> App ext (E ext s) t) -> [SomeExpr ext s] -> m (E ext s t)+ u f [x] = EApp . f <$> evalSomeExpr tpr x+ u _ _ = later $ describe "one argument" $ empty++ bin :: (E ext s t -> E ext s t -> App ext (E ext s) t) -> [SomeExpr ext s] -> m (E ext s t)+ bin f [x,y] = EApp <$> (f <$> evalSomeExpr tpr x <*> evalSomeExpr tpr y)+ bin _ _ = later $ describe "two arguments" $ empty++ nary :: (E ext s t -> E ext s t -> App ext (E ext s) t) -> App ext (E ext s) t -> [SomeExpr ext s] -> m (E ext s t)+ nary _ z [] = return $ EApp z+ nary _ _ [x] = evalSomeExpr tpr x+ nary f _ (x:xs) = go f <$> evalSomeExpr tpr x <*> mapM (evalSomeExpr tpr) xs++ go f x (y:ys) = go f (EApp $ f x y) ys+ go _ x [] = x+++evalSomeExpr :: MonadSyntax Atomic m => TypeRepr t -> SomeExpr ext s -> m (E ext s t)+evalSomeExpr tpr (SomeE tpr' e)+ | Just Refl <- testEquality tpr tpr' = return e+ | otherwise = later $ describe ("matching types (" <> T.pack (show tpr)+ <> " /= " <> T.pack (show tpr') <> ")") empty+evalSomeExpr tpr (SomeOverloaded ast k args) = evalOverloaded ast tpr k args+evalSomeExpr tpr (SomeIntLiteral ast i) = evalIntLiteral ast tpr i++applyOverloaded ::+ MonadSyntax Atomic m => AST s -> Keyword -> Maybe (Some TypeRepr) -> [SomeExpr ext s] -> m (SomeExpr ext s)+applyOverloaded ast k mtp args =+ case findJointType mtp args of+ Nothing -> return $ SomeOverloaded ast k args+ Just (Some tp) -> SomeE tp <$> evalOverloaded ast tp k args++evalIntLiteral :: MonadSyntax Atomic m => AST s -> TypeRepr tpr -> Integer -> m (E ext s tpr)+evalIntLiteral _ NatRepr i | i >= 0 = return $ EApp $ NatLit (fromInteger i)+evalIntLiteral _ IntegerRepr i = return $ EApp $ IntLit i+evalIntLiteral _ RealValRepr i = return $ EApp $ RationalLit (fromInteger i)+evalIntLiteral ast tpr _i =+ withFocus ast $ later $ describe ("literal " <> T.pack (show tpr) <> " value") empty++forceSynth :: MonadSyntax Atomic m => SomeExpr ext s -> m (Pair TypeRepr (E ext s))+forceSynth (SomeE tp e) = return $ Pair tp e+forceSynth (SomeOverloaded ast _ _) =+ withFocus ast $ later (describe "unambiguous expression (add type annotation to disambiguate)" empty)+forceSynth (SomeIntLiteral ast _) =+ withFocus ast $ later (describe "unambiguous numeric literal (add type annotation to disambiguate)" empty)++synth+ :: forall m s ext+ . ( MonadReader (SyntaxState s) m+ , MonadSyntax Atomic m+ , ?parserHooks :: ParserHooks ext )+ => m (Pair TypeRepr (E ext s))+synth = forceSynth =<< synth'++synth' :: forall m s ext+ . ( MonadReader (SyntaxState s) m+ , MonadSyntax Atomic m+ , ?parserHooks :: ParserHooks ext )+ => m (SomeExpr ext s)+synth' = synthExpr Nothing++synthExpr :: forall m s ext+ . ( MonadReader (SyntaxState s) m+ , MonadSyntax Atomic m+ , ?parserHooks :: ParserHooks ext )+ => Maybe (Some TypeRepr)+ -> m (SomeExpr ext s)+synthExpr typeHint =+ describe "expression" $+ call (the <|> crucibleAtom <|> regRef <|> globRef <|> deref <|>+ bvExpr <|>+ naryBool And_ And True <|> naryBool Or_ Or False <|> naryBool Xor_ BoolXor False <|>+ unaryArith Negate <|> unaryArith Abs <|>+ naryArith Plus <|> binaryArith Minus <|> naryArith Times <|> binaryArith Div <|> binaryArith Mod <|>+ unitCon <|> boolLit <|> stringLit <|> funNameLit <|>+ notExpr <|> equalp <|> lessThan <|> lessThanEq <|>+ toAny <|> fromAny <|> stringAppend <|> stringEmpty <|> stringLength <|> showExpr <|>+ just <|> nothing <|> fromJust_ <|> injection <|> projection <|>+ vecLit <|> vecCons <|> vecRep <|> vecLen <|> vecEmptyP <|> vecGet <|> vecSet <|>+ struct <|> getField <|> setField <|>+ seqNil <|> seqCons <|> seqAppend <|> seqNilP <|> seqLen <|>+ seqHead <|> seqTail <|> seqUncons <|>+ ite <|> intLit <|> rationalLit <|> intp <|>+ binaryToFp <|> fpToBinary <|> realToFp <|> fpToReal <|>+ ubvToFloat <|> floatToUBV <|> sbvToFloat <|> floatToSBV <|>+ unaryBV BVNonzero_ BVNonzero <|> compareBV BVCarry_ BVCarry <|>+ compareBV BVSCarry_ BVSCarry <|> compareBV BVSBorrow_ BVSBorrow <|>+ compareBV Slt BVSlt <|> compareBV Sle BVSle)++-- Syntactic constructs still to add (see issue #74)++-- BvToInteger, SbvToInteger, BvToNat+-- NatToInteger, IntegerToReal+-- RealRound, RealFloor, RealCeil+-- IntegerToBV, RealToNat++-- EmptyWordMap, InsertWordMap, LookupWordMap, LookupWordMapWithDefault+-- EmptyStringMap, LookupStringMapEntry, InsertStringMapEntry+-- SymArrayLookup, SymArrayUpdate+-- Complex, RealPart, ImagPart+-- IsConcrete+-- Closure+-- All the floating-point operations+-- What to do about RollRecursive, UnrollRecursive?+-- AddSideCondition????+-- BVUndef ????++ where+ the :: m (SomeExpr ext s)+ the = do describe "type-annotated expression" $+ kw The `followedBy`+ (depCons isType $+ \(Some t) ->+ do (e, ()) <- cons (check t) emptyList+ return $ SomeE t e)++ okAtom theAtoms x =+ case Map.lookup x theAtoms of+ Nothing -> Nothing+ Just (Some anAtom) -> Just $ SomeE (typeOfAtom anAtom) (EAtom anAtom)++ regRef :: m (SomeExpr ext s)+ regRef =+ do Some r <- regRef'+ loc <- position+ return (SomeE (typeOfReg r) (EReg loc r))++ deref :: m (SomeExpr ext s)+ deref =+ do let newhint = case typeHint of+ Just (Some t) -> Just (Some (ReferenceRepr t))+ _ -> Nothing+ unary Deref (forceSynth =<< synthExpr newhint) >>= \case+ Pair (ReferenceRepr t') e ->+ do loc <- position+ return (SomeE t' (EDeref loc e))+ Pair notRef _ -> later $ describe ("reference type (provided a "<> T.pack (show notRef) <>")") empty++ globRef :: m (SomeExpr ext s)+ globRef =+ do Some g <- globRef'+ loc <- position+ return (SomeE (globalType g) (EGlob loc g))++ crucibleAtom :: m (SomeExpr ext s)+ crucibleAtom =+ do theAtoms <- view stxAtoms+ sideCondition "known atom" (okAtom theAtoms) atomName++ unitCon = describe "unit constructor" (emptyList $> SomeE UnitRepr (EApp EmptyApp))++ boolLit = bool <&> SomeE BoolRepr . EApp . BoolLit++ stringLit = string <&> SomeE (StringRepr UnicodeRepr) . EApp . StringLit . UnicodeLiteral++ intLit =+ do ast <- anything+ case typeHint of+ Just (Some tpr) -> SomeE tpr <$> (evalIntLiteral ast tpr =<< int)+ Nothing -> SomeIntLiteral ast <$> int++ rationalLit = rational <&> SomeE RealValRepr . EApp . RationalLit++ naryBool k f u =+ do ((), args) <- cons (kw k) (rep (check BoolRepr))+ case args of+ [] -> return $ SomeE BoolRepr $ EApp (BoolLit u)+ (x:xs) -> go x xs++ where+ go x [] = return $ SomeE BoolRepr x+ go x (y:ys) = go (EApp $ f x y) ys++ bvExpr :: m (SomeExpr ext s)+ bvExpr =+ do let nathint = case typeHint of Just (Some (BVRepr w)) -> NatHint w; _ -> NoHint+ SomeBVExpr w x <- synthBV nathint+ return $ SomeE (BVRepr w) x++ intp =+ do e <- unary Integerp (check RealValRepr)+ return $ SomeE BoolRepr $ EApp $ RealIsInteger e++ funNameLit =+ do fn <- funName+ fh <- view $ stxFunctions . at fn+ dh <- view $ stxForwardDecs . at fn+ describe "known function name" $+ -- First look for a function with the given name, and failing that,+ -- look for a forward declaration with the given name.+ case fh <|> dh of+ Nothing -> empty+ Just (FunctionHeader _ funArgs ret handle _) ->+ return $ SomeE (FunctionHandleRepr (argTypes funArgs) ret) (EApp $ HandleLit handle)++ notExpr =+ do e <- describe "negation expression" $ unary Not_ (check BoolRepr)+ return $ SomeE BoolRepr $ EApp $ Not e++ matchingExprs ::+ Maybe (Some TypeRepr) -> SomeExpr ext s -> SomeExpr ext s ->+ (forall tp. TypeRepr tp -> E ext s tp -> E ext s tp -> m a) ->+ m a+ matchingExprs h e1 e2 k =+ case findJointType h [e1,e2] of+ Just (Some tp) ->+ do e1' <- evalSomeExpr tp e1+ e2' <- evalSomeExpr tp e2+ k tp e1' e2'+ Nothing ->+ later $ describe ("type annotation required to disambiguate types") empty++ equalp :: m (SomeExpr ext s)+ equalp =+ do (e1, e2) <- describe "equality test" $ binary Equalp synth' synth'+ matchingExprs Nothing e1 e2 $ \tp e1' e2' ->+ case tp of+ FloatRepr _fi ->+ return $ SomeE BoolRepr $ EApp $ FloatEq e1' e2'+ ReferenceRepr rtp ->+ return $ SomeE BoolRepr $ EApp $ ReferenceEq rtp e1' e2'+ NatRepr ->+ return $ SomeE BoolRepr $ EApp $ NatEq e1' e2'+ (asBaseType -> AsBaseType bt) ->+ return $ SomeE BoolRepr $ EApp $ BaseIsEq bt e1' e2'+ _ ->+ later $ describe ("a base type or floating point type or reference type (got " <> T.pack (show tp) <> ")") empty++ compareBV ::+ Keyword ->+ (forall w. (1 <= w) => NatRepr w -> E ext s (BVType w) -> E ext s (BVType w) -> App ext (E ext s) BoolType) ->+ m (SomeExpr ext s)+ compareBV k f =+ do (e1, e2) <- describe "bitvector compaprison" $ binary k synth' synth'+ matchingExprs Nothing e1 e2 $ \tp e1' e2' ->+ case tp of+ BVRepr w ->+ return $ SomeE BoolRepr $ EApp $ f w e1' e2'+ _ ->+ later $ describe ("a bitvector type (got " <> T.pack (show tp) <> ")") empty++ lessThan :: m (SomeExpr ext s)+ lessThan =+ do (e1, e2) <- describe "less-than test" $ binary Lt synth' synth'+ matchingExprs Nothing e1 e2 $ \tp e1' e2' ->+ case tp of+ NatRepr -> return $ SomeE BoolRepr $ EApp $ NatLt e1' e2'+ IntegerRepr -> return $ SomeE BoolRepr $ EApp $ IntLt e1' e2'+ RealValRepr -> return $ SomeE BoolRepr $ EApp $ RealLt e1' e2'+ BVRepr w -> return $ SomeE BoolRepr $ EApp $ BVUlt w e1' e2'+ other ->+ describe ("valid comparison type (got " <> T.pack (show other) <> ")") empty++ lessThanEq :: m (SomeExpr ext s)+ lessThanEq =+ do (e1, e2) <- describe "less-than-or-equal test" $ binary Le synth' synth'+ matchingExprs Nothing e1 e2 $ \tp e1' e2' ->+ case tp of+ NatRepr -> return $ SomeE BoolRepr $ EApp $ NatLe e1' e2'+ IntegerRepr -> return $ SomeE BoolRepr $ EApp $ IntLe e1' e2'+ RealValRepr -> return $ SomeE BoolRepr $ EApp $ RealLe e1' e2'+ BVRepr w -> return $ SomeE BoolRepr $ EApp $ BVUle w e1' e2'+ other ->+ describe ("valid comparison type (got " <> T.pack (show other) <> ")") empty++ naryArith :: Keyword -> m (SomeExpr ext s)+ naryArith k =+ do ast <- anything+ args <- followedBy (kw k) (commit *> (rep (synthExpr typeHint)))+ applyOverloaded ast k typeHint args++ binaryArith :: Keyword -> m (SomeExpr ext s)+ binaryArith k =+ do ast <- anything+ (x, y) <- binary k (synthExpr typeHint) (synthExpr typeHint)+ applyOverloaded ast k typeHint [x,y]++ unaryArith :: Keyword -> m (SomeExpr ext s)+ unaryArith k =+ do ast <- anything+ x <- unary k (synthExpr typeHint)+ applyOverloaded ast k typeHint [x]++ unaryBV ::+ Keyword ->+ (forall w. (1 <= w) => NatRepr w -> E ext s (BVType w) -> App ext (E ext s) BoolType) ->+ m (SomeExpr ext s)+ unaryBV k f =+ do Pair t x <- unary k synth+ case t of+ BVRepr w ->return $ SomeE BoolRepr $ EApp $ f w x+ _ -> later $ describe "bitvector argument" empty++ just :: m (SomeExpr ext s)+ just =+ do let newhint = case typeHint of+ Just (Some (MaybeRepr t)) -> Just (Some t)+ _ -> Nothing+ Pair t x <- unary Just_ (forceSynth =<< synthExpr newhint)+ return $ SomeE (MaybeRepr t) $ EApp $ JustValue t x++ nothing :: m (SomeExpr ext s)+ nothing =+ do Some t <- unary Nothing_ isType+ return $ SomeE (MaybeRepr t) $ EApp $ NothingValue t+ <|>+ kw Nothing_ *>+ case typeHint of+ Just (Some (MaybeRepr t)) ->+ return $ SomeE (MaybeRepr t) $ EApp $ NothingValue t+ Just (Some t) ->+ later $ describe ("value of type " <> T.pack (show t)) empty+ Nothing ->+ later $ describe ("unambiguous nothing value") empty++ fromJust_ :: m (SomeExpr ext s)+ fromJust_ =+ do let newhint = case typeHint of+ Just (Some t) -> Just (Some (MaybeRepr t))+ _ -> Nothing+ describe "coercion from Maybe (fromJust-expression)" $+ followedBy (kw FromJust) $+ depCons (forceSynth =<< synthExpr newhint) $ \(Pair t e) ->+ case t of+ MaybeRepr elemT ->+ depCons (check (StringRepr UnicodeRepr)) $ \str ->+ do emptyList+ return $ SomeE elemT $ EApp $ FromJustValue elemT e str+ _ -> later $ describe "maybe expression" nothing++ projection :: m (SomeExpr ext s)+ projection =+ do (n, Pair t e) <- describe "projection from variant type" $ binary Proj int synth+ case t of+ VariantRepr ts ->+ case Ctx.intIndex (fromInteger n) (Ctx.size ts) of+ Nothing ->+ describe (T.pack (show n) <> " is an invalid index into " <> T.pack (show ts)) empty+ Just (Some idx) ->+ do let ty = MaybeRepr (ts^.ixF' idx)+ return $ SomeE ty $ EApp $ ProjectVariant ts idx e+ _ -> describe ("variant type (got " <> T.pack (show t) <> ")") empty++ injection :: m (SomeExpr ext s)+ injection =+ do (n, e) <- describe "injection into variant type" $ binary Inj int anything+ case typeHint of+ Just (Some (VariantRepr ts)) ->+ case Ctx.intIndex (fromInteger n) (Ctx.size ts) of+ Nothing ->+ describe (T.pack (show n) <> " is an invalid index into " <> T.pack (show ts)) empty+ Just (Some idx) ->+ do let ty = view (ixF' idx) ts+ out <- withProgressStep Rest $ withProgressStep Rest $ withProgressStep First $+ parse e (check ty)+ return $ SomeE (VariantRepr ts) $ EApp $ InjectVariant ts idx out+ Just (Some t) ->+ describe ("context expecting variant type (got " <> T.pack (show t) <> ")") empty+ Nothing ->+ describe ("unambiguous variant") empty++ fpToBinary :: m (SomeExpr ext s)+ fpToBinary =+ kw FPToBinary_ `followedBy`+ (depConsCond synth $ \(Pair tp x) ->+ case tp of+ FloatRepr fpi+ | BaseBVRepr w <- floatInfoToBVTypeRepr fpi+ , Just LeqProof <- isPosNat w ->+ emptyList $> (Right $ SomeE (BVRepr w) $ EApp $ FloatToBinary fpi x)+ _ -> pure $ Left $ "floating-point value")++ binaryToFp :: m (SomeExpr ext s)+ binaryToFp =+ kw BinaryToFP_ `followedBy`+ (depCons fpinfo $ \(Some fpi) ->+ depCons (check (baseToType (floatInfoToBVTypeRepr fpi))) $ \x ->+ emptyList $> (SomeE (FloatRepr fpi) $ EApp $ FloatFromBinary fpi x))++ fpToReal :: m (SomeExpr ext s)+ fpToReal =+ kw FPToReal_ `followedBy`+ (depConsCond synth $ \(Pair tp x) ->+ case tp of+ FloatRepr _fpi -> emptyList $> (Right $ SomeE RealValRepr $ EApp $ FloatToReal x)+ _ -> pure $ Left "floating-point value")++ realToFp :: m (SomeExpr ext s)+ realToFp =+ kw RealToFP_ `followedBy`+ (depCons fpinfo $ \(Some fpi) ->+ depCons roundingMode $ \rm ->+ depCons (check RealValRepr) $ \x ->+ emptyList $> (SomeE (FloatRepr fpi) $ EApp $ FloatFromReal fpi rm x))++ ubvToFloat :: m (SomeExpr ext s)+ ubvToFloat =+ kw UBVToFP_ `followedBy`+ (depCons fpinfo $ \(Some fpi) ->+ depCons roundingMode $ \rm ->+ depConsCond synth $ \(Pair tp x) ->+ case tp of+ BVRepr _w ->+ emptyList $> (Right $ SomeE (FloatRepr fpi) $ EApp $ FloatFromBV fpi rm x)+ _ -> pure $ Left $ "bitvector value"+ )++ sbvToFloat :: m (SomeExpr ext s)+ sbvToFloat =+ kw SBVToFP_ `followedBy`+ (depCons fpinfo $ \(Some fpi) ->+ depCons roundingMode $ \rm ->+ depConsCond synth $ \(Pair tp x) ->+ case tp of+ BVRepr _w ->+ emptyList $> (Right $ SomeE (FloatRepr fpi) $ EApp $ FloatFromSBV fpi rm x)+ _ -> pure $ Left $ "bitvector value"+ )++ floatToUBV :: m (SomeExpr ext s)+ floatToUBV =+ kw FPToUBV_ `followedBy`+ (depCons posNat $ \(BoundedNat w) ->+ depCons roundingMode $ \rm ->+ depConsCond synth $ \(Pair tp x) ->+ case tp of+ FloatRepr _fpi ->+ emptyList $> (Right $ SomeE (BVRepr w) $ EApp $ FloatToBV w rm x)+ _ -> pure $ Left $ "floating-point value")++ floatToSBV :: m (SomeExpr ext s)+ floatToSBV =+ kw FPToSBV_ `followedBy`+ (depCons posNat $ \(BoundedNat w) ->+ depCons roundingMode $ \rm ->+ depConsCond synth $ \(Pair tp x) ->+ case tp of+ FloatRepr _fpi ->+ emptyList $> (Right $ SomeE (BVRepr w) $ EApp $ FloatToSBV w rm x)+ _ -> pure $ Left $ "floating-point value")++ ite :: m (SomeExpr ext s)+ ite =+ do (c, (et, (ef, ()))) <-+ followedBy (kw If) $+ cons (check BoolRepr) $+ cons (synthExpr typeHint) $+ cons (synthExpr typeHint) $+ emptyList+ matchingExprs typeHint et ef $ \tp t f ->+ case tp of+ FloatRepr fi ->+ return $ SomeE tp $ EApp $ FloatIte fi c t f+ NatRepr ->+ return $ SomeE tp $ EApp $ NatIte c t f+ (asBaseType -> AsBaseType bty) ->+ return $ SomeE tp $ EApp $ BaseIte bty c t f+ _ ->+ let msg = T.concat [ "conditional where branches have base or floating point type, but got "+ , T.pack (show tp)+ ]+ in later $ describe msg empty++ toAny =+ do Pair tp e <- unary ToAny synth+ return $ SomeE AnyRepr (EApp (PackAny tp e))+ fromAny =+ (binary FromAny isType (check AnyRepr)) <&>+ \(Some ty, e) -> SomeE (MaybeRepr ty) (EApp (UnpackAny ty e))++ stringLength :: m (SomeExpr ext s)+ stringLength =+ do unary StringLength_+ (do (Pair ty e) <- forceSynth =<< synthExpr Nothing+ case ty of+ StringRepr _si -> return $ SomeE IntegerRepr $ EApp (StringLength e)+ _ -> later $ describe "string expression" empty)++ stringEmpty =+ unary StringEmpty_ stringSort <&> \(Some si) -> SomeE (StringRepr si) $ EApp $ StringEmpty si++ stringAppend :: m (SomeExpr ext s)+ stringAppend =+ do (e1,(e2,())) <-+ followedBy (kw StringConcat_) $+ cons (synthExpr typeHint) $+ cons (synthExpr typeHint) $+ emptyList+ matchingExprs typeHint e1 e2 $ \tp s1 s2 ->+ case tp of+ StringRepr si -> return $ SomeE (StringRepr si) $ EApp $ StringConcat si s1 s2+ _ -> later $ describe "string expressions" empty++ vecRep :: m (SomeExpr ext s)+ vecRep =+ do let newhint = case typeHint of+ Just (Some (VectorRepr t)) -> Just (Some t)+ _ -> Nothing+ (n, Pair t e) <-+ binary VectorReplicate_ (check NatRepr) (forceSynth =<< synthExpr newhint)+ return $ SomeE (VectorRepr t) $ EApp $ VectorReplicate t n e++ vecLen :: m (SomeExpr ext s)+ vecLen =+ do Pair t e <- unary VectorSize_ synth+ case t of+ VectorRepr _ -> return $ SomeE NatRepr $ EApp $ VectorSize e+ other -> later $ describe ("vector (found " <> T.pack (show other) <> ")") empty++ vecEmptyP :: m (SomeExpr ext s)+ vecEmptyP =+ do Pair t e <- unary VectorIsEmpty_ synth+ case t of+ VectorRepr _ -> return $ SomeE BoolRepr $ EApp $ VectorIsEmpty e+ other -> later $ describe ("vector (found " <> T.pack (show other) <> ")") empty++ vecLit :: m (SomeExpr ext s)+ vecLit =+ let newhint = case typeHint of+ Just (Some (VectorRepr t)) -> Just (Some t)+ _ -> Nothing+ in describe "vector literal" $+ do ((),ls) <- cons (kw VectorLit_) (commit *> rep (synthExpr newhint))+ case findJointType newhint ls of+ Nothing -> later $ describe "unambiguous vector literal (add a type ascription to disambiguate)" empty+ Just (Some t) ->+ SomeE (VectorRepr t) . EApp . VectorLit t . V.fromList+ <$> mapM (evalSomeExpr t) ls++ vecCons :: m (SomeExpr ext s)+ vecCons =+ do let newhint = case typeHint of+ Just (Some (VectorRepr t)) -> Just (Some t)+ _ -> Nothing+ (a, d) <- binary VectorCons_ (later (synthExpr newhint)) (later (synthExpr typeHint))+ let g Nothing = Nothing+ g (Just (Some t)) = Just (Some (VectorRepr t))+ case join (find isJust [ typeHint, g (someExprType a), someExprType d ]) of+ Just (Some (VectorRepr t)) ->+ SomeE (VectorRepr t) . EApp <$> (VectorCons t <$> evalSomeExpr t a <*> evalSomeExpr (VectorRepr t) d)+ _ -> later $ describe "unambiguous vector cons (add a type ascription to disambiguate)" empty++ vecGet :: m (SomeExpr ext s)+ vecGet =+ do let newhint = case typeHint of+ Just (Some t) -> Just (Some (VectorRepr t))+ _ -> Nothing+ (Pair t e, n) <-+ binary VectorGetEntry_ (forceSynth =<< synthExpr newhint) (check NatRepr)+ case t of+ VectorRepr elemT -> return $ SomeE elemT $ EApp $ VectorGetEntry elemT e n+ other -> later $ describe ("vector (found " <> T.pack (show other) <> ")") empty++ vecSet :: m (SomeExpr ext s)+ vecSet =+ do (kw VectorSetEntry_) `followedBy` (+ depCons (forceSynth =<< synthExpr typeHint) $+ \ (Pair t vec) ->+ case t of+ VectorRepr elemT ->+ do (n, (elt, ())) <- cons (check NatRepr) $+ cons (check elemT) $+ emptyList+ return $ SomeE (VectorRepr elemT) $ EApp $ VectorSetEntry elemT vec n elt+ _ -> later $ describe "argument with vector type" empty)++ struct :: m (SomeExpr ext s)+ struct = describe "struct literal" $ followedBy (kw MkStruct_) (commit *>+ do ls <- case typeHint of+ Just (Some (StructRepr ctx)) ->+ list (toListFC (\t -> forceSynth =<< synthExpr (Just (Some t))) ctx)+ Just (Some t) -> later $ describe ("value of type " <> T.pack (show t) <> " but got struct") empty+ Nothing -> rep (forceSynth =<< synthExpr Nothing)+ pure $! buildStruct ls)++ getField :: m (SomeExpr ext s)+ getField =+ describe "struct field projection" $+ followedBy (kw GetField_) (commit *>+ depCons int (\n ->+ depCons synth (\(Pair t e) ->+ case t of+ StructRepr ts ->+ case Ctx.intIndex (fromInteger n) (Ctx.size ts) of+ Nothing ->+ describe (T.pack (show n) <> " is an invalid index into " <> T.pack (show ts)) empty+ Just (Some idx) ->+ do let ty = ts^.ixF' idx+ return $ SomeE ty $ EApp $ GetStruct e idx ty+ _ -> describe ("struct type (got " <> T.pack (show t) <> ")") empty)))++ setField :: m (SomeExpr ext s)+ setField = describe "update to a struct type" $+ followedBy (kw SetField_) (commit *>+ depConsCond (forceSynth =<< synthExpr typeHint) (\ (Pair tp e) ->+ case tp of+ StructRepr ts -> Right <$>+ depConsCond int (\n ->+ case Ctx.intIndex (fromInteger n) (Ctx.size ts) of+ Nothing -> pure (Left (T.pack (show n) <> " is an invalid index into " <> T.pack (show ts)))+ Just (Some idx) -> Right <$>+ do let ty = ts^.ixF' idx+ (v,()) <- cons (check ty) emptyList+ pure $ SomeE (StructRepr ts) $ EApp $ SetStruct ts e idx v)+ _ -> pure $ Left $ ("struct type, but got " <> T.pack (show tp))))++ seqNil :: m (SomeExpr ext s)+ seqNil =+ do Some t <- unary SequenceNil_ isType+ return $ SomeE (SequenceRepr t) $ EApp $ SequenceNil t+ <|>+ kw SequenceNil_ *>+ case typeHint of+ Just (Some (SequenceRepr t)) ->+ return $ SomeE (SequenceRepr t) $ EApp $ SequenceNil t+ Just (Some t) ->+ later $ describe ("value of type " <> T.pack (show t)) empty+ Nothing ->+ later $ describe ("unambiguous nil value") empty++ seqCons :: m (SomeExpr ext s)+ seqCons =+ do let newhint = case typeHint of+ Just (Some (SequenceRepr t)) -> Just (Some t)+ _ -> Nothing+ (a, d) <- binary SequenceCons_ (later (synthExpr newhint)) (later (synthExpr typeHint))+ let g Nothing = Nothing+ g (Just (Some t)) = Just (Some (SequenceRepr t))+ case join (find isJust [ typeHint, g (someExprType a), someExprType d ]) of+ Just (Some (SequenceRepr t)) ->+ SomeE (SequenceRepr t) . EApp <$> (SequenceCons t <$> evalSomeExpr t a <*> evalSomeExpr (SequenceRepr t) d)+ _ -> later $ describe "unambiguous sequence cons (add a type ascription to disambiguate)" empty++ seqAppend :: m (SomeExpr ext s)+ seqAppend =+ do (x, y) <- binary SequenceAppend_ (later (synthExpr typeHint)) (later (synthExpr typeHint))+ case join (find isJust [ typeHint, someExprType x, someExprType y ]) of+ Just (Some (SequenceRepr t)) ->+ SomeE (SequenceRepr t) . EApp <$>+ (SequenceAppend t <$> evalSomeExpr (SequenceRepr t) x <*> evalSomeExpr (SequenceRepr t) y)+ _ -> later $ describe "unambiguous sequence append (add a type ascription to disambiguate)" empty++ seqNilP :: m (SomeExpr ext s)+ seqNilP =+ do Pair t e <- unary SequenceIsNil_ synth+ case t of+ SequenceRepr t' -> return $ SomeE BoolRepr $ EApp $ SequenceIsNil t' e+ other -> later $ describe ("sequence (found " <> T.pack (show other) <> ")") empty++ seqLen :: m (SomeExpr ext s)+ seqLen =+ do Pair t e <- unary SequenceLength_ synth+ case t of+ SequenceRepr t' -> return $ SomeE NatRepr $ EApp $ SequenceLength t' e+ other -> later $ describe ("sequence (found " <> T.pack (show other) <> ")") empty++ seqHead :: m (SomeExpr ext s)+ seqHead =+ do let newhint = case typeHint of+ Just (Some (MaybeRepr t)) -> Just (Some (SequenceRepr t))+ _ -> Nothing+ (Pair t e) <-+ unary SequenceHead_ (forceSynth =<< synthExpr newhint)+ case t of+ SequenceRepr elemT -> return $ SomeE (MaybeRepr elemT) $ EApp $ SequenceHead elemT e+ other -> later $ describe ("sequence (found " <> T.pack (show other) <> ")") empty++ seqTail :: m (SomeExpr ext s)+ seqTail =+ do let newhint = case typeHint of+ Just (Some (MaybeRepr t)) -> Just (Some t)+ _ -> Nothing+ (Pair t e) <-+ unary SequenceTail_ (forceSynth =<< synthExpr newhint)+ case t of+ SequenceRepr elemT -> return $ SomeE (MaybeRepr (SequenceRepr elemT)) $ EApp $ SequenceTail elemT e+ other -> later $ describe ("sequence (found " <> T.pack (show other) <> ")") empty++ seqUncons :: m (SomeExpr ext s)+ seqUncons =+ do let newhint = case typeHint of+ Just (Some (MaybeRepr (StructRepr (Ctx.Empty Ctx.:> t Ctx.:> _)))) ->+ Just (Some (SequenceRepr t))+ _ -> Nothing+ (Pair t e) <-+ unary SequenceUncons_ (forceSynth =<< synthExpr newhint)+ case t of+ SequenceRepr elemT ->+ return $ SomeE (MaybeRepr (StructRepr (Ctx.Empty Ctx.:> elemT Ctx.:> SequenceRepr elemT))) $+ EApp $ SequenceUncons elemT e+ other -> later $ describe ("sequence (found " <> T.pack (show other) <> ")") empty++ showExpr :: m (SomeExpr ext s)+ showExpr =+ do Pair t1 e <- unary Show synth+ case t1 of+ FloatRepr fi ->+ return $ SomeE (StringRepr UnicodeRepr) $ EApp $ ShowFloat fi e+ NatRepr ->+ let toint = EApp $ NatToInteger e+ showint = EApp $ ShowValue BaseIntegerRepr toint+ in return $ SomeE (StringRepr UnicodeRepr) showint+ (asBaseType -> AsBaseType bt) ->+ return $ SomeE (StringRepr UnicodeRepr) $ EApp $ ShowValue bt e+ _ -> later $ describe ("base or floating point type, but got " <> T.pack (show t1)) empty+++buildStruct :: [Pair TypeRepr (E ext s)] -> SomeExpr ext s+buildStruct = loop Ctx.Empty Ctx.Empty+ where+ loop :: Ctx.Assignment TypeRepr ctx -> Ctx.Assignment (E ext s) ctx -> [Pair TypeRepr (E ext s)] -> SomeExpr ext s+ loop tps vs [] = SomeE (StructRepr tps) (EApp (MkStruct tps vs))+ loop tps vs (Pair tp x:xs) = loop (tps Ctx.:> tp) (vs Ctx.:> x) xs++data NatHint+ = NoHint+ | forall w. (1 <= w) => NatHint (NatRepr w)++synthBV :: forall m s ext.+ ( MonadReader (SyntaxState s) m+ , MonadSyntax Atomic m+ , ?parserHooks :: ParserHooks ext ) =>+ NatHint ->+ m (SomeBVExpr ext s)+synthBV widthHint =+ bvLit <|> bvConcat <|> bvSelect <|> bvTrunc <|>+ bvZext <|> bvSext <|> boolToBV <|>+ naryBV BVAnd_ BVAnd 1 <|> naryBV BVOr_ BVOr 0 <|> naryBV BVXor_ BVXor 0 <|>+ binaryBV Sdiv BVSdiv <|> binaryBV Smod BVSrem <|>+ binaryBV BVShl_ BVShl <|> binaryBV BVLshr_ BVLshr <|> binaryBV BVAshr_ BVAshr <|>+ unaryBV Negate BVNeg <|> unaryBV BVNot_ BVNot++ where+ bvSubterm :: NatHint -> m (SomeBVExpr ext s)+ bvSubterm hint =+ do let newhint = case hint of+ NatHint w -> Just (Some (BVRepr w))+ _ -> Nothing+ (Pair t x) <- forceSynth =<< synthExpr newhint+ case t of+ BVRepr w -> return (SomeBVExpr w x)+ _ -> later $ describe "bitvector expression" $ empty++ bvLit :: m (SomeBVExpr ext s)+ bvLit =+ describe "bitvector literal" $+ do (BoundedNat w, i) <- binary BV posNat int+ return $ SomeBVExpr w $ EApp $ BVLit w (BV.mkBV w i)++ unaryBV :: Keyword+ -> (forall w. (1 <= w) => NatRepr w -> E ext s (BVType w) -> App ext (E ext s) (BVType w))+ -> m (SomeBVExpr ext s)+ unaryBV k f =+ do SomeBVExpr wx x <- unary k (bvSubterm widthHint)+ return $ SomeBVExpr wx $ EApp $ f wx x++ binaryBV :: Keyword+ -> (forall w. (1 <= w) => NatRepr w -> E ext s (BVType w) -> E ext s (BVType w) -> App ext (E ext s) (BVType w))+ -> m (SomeBVExpr ext s)+ binaryBV k f =+ do (SomeBVExpr wx x, SomeBVExpr wy y) <- binary k (bvSubterm widthHint) (bvSubterm widthHint)+ case testEquality wx wy of+ Just Refl -> return $ SomeBVExpr wx $ EApp $ f wx x y+ Nothing -> later $+ describe ("bitwise expression arguments with matching widths (" <>+ T.pack (show wx) <> " /= " <> T.pack (show wy) <> ")")+ empty++ naryBV :: Keyword+ -> (forall w. (1 <= w) => NatRepr w -> E ext s (BVType w) -> E ext s (BVType w) -> App ext (E ext s) (BVType w))+ -> Integer+ -> m (SomeBVExpr ext s)+ naryBV k f u =+ do args <- kw k `followedBy` rep (later (bvSubterm widthHint))+ case args of+ [] -> case widthHint of+ NoHint -> later $ describe "ambiguous width" empty+ NatHint w -> return $ SomeBVExpr w $ EApp $ BVLit w (BV.mkBV w u)+ (SomeBVExpr wx x:xs) -> SomeBVExpr wx <$> go wx x xs++ where+ go :: forall w. NatRepr w -> E ext s (BVType w) -> [SomeBVExpr ext s] -> m (E ext s (BVType w))+ go _wx x [] = return x+ go wx x (SomeBVExpr wy y : ys) =+ case testEquality wx wy of+ Just Refl -> go wx (EApp $ f wx x y) ys+ Nothing -> later $+ describe ("bitwise expression arguments with matching widths (" <>+ T.pack (show wx) <> " /= " <> T.pack (show wy) <> ")")+ empty++ boolToBV :: m (SomeBVExpr ext s)+ boolToBV =+ do (BoundedNat w, x) <- binary BoolToBV_ posNat (check BoolRepr)+ return $ SomeBVExpr w $ EApp $ BoolToBV w x++ bvSelect :: m (SomeBVExpr ext s)+ bvSelect =+ do (Some idx, (BoundedNat len, (SomeBVExpr w x, ()))) <-+ followedBy (kw BVSelect_) (commit *> cons natRepr (cons posNat (cons (bvSubterm NoHint) emptyList)))+ case testLeq (addNat idx len) w of+ Just LeqProof -> return $ SomeBVExpr len $ EApp $ BVSelect idx len w x+ _ -> later $ describe ("valid bitvector select") $ empty++ bvConcat :: m (SomeBVExpr ext s)+ bvConcat =+ do (SomeBVExpr wx x, SomeBVExpr wy y) <- binary BVConcat_ (bvSubterm NoHint) (bvSubterm NoHint)+ withLeqProof (leqAdd (leqProof (knownNat @1) wx) wy) $+ return $ SomeBVExpr (addNat wx wy) (EApp $ BVConcat wx wy x y)++ bvTrunc :: m (SomeBVExpr ext s)+ bvTrunc =+ do (BoundedNat r, SomeBVExpr w x) <- binary BVTrunc_ posNat (bvSubterm NoHint)+ case testLeq (incNat r) w of+ Just LeqProof -> return $ SomeBVExpr r (EApp $ BVTrunc r w x)+ _ -> later $ describe "valid bitvector truncation" $ empty++ bvZext :: m (SomeBVExpr ext s)+ bvZext =+ do (BoundedNat r, SomeBVExpr w x) <- binary BVZext_ posNat (bvSubterm NoHint)+ case testLeq (incNat w) r of+ Just LeqProof -> return $ SomeBVExpr r (EApp $ BVZext r w x)+ _ -> later $ describe "valid zero extension" $ empty++ bvSext :: m (SomeBVExpr ext s)+ bvSext =+ do (BoundedNat r, SomeBVExpr w x) <- binary BVSext_ posNat (bvSubterm NoHint)+ case testLeq (incNat w) r of+ Just LeqProof -> return $ SomeBVExpr r (EApp $ BVSext r w x)+ _ -> later $ describe "valid zero extension" $ empty+++check :: forall m t s ext+ . ( MonadReader (SyntaxState s) m+ , MonadSyntax Atomic m+ , ?parserHooks :: ParserHooks ext )+ => TypeRepr t -> m (E ext s t)+check t =+ describe ("inhabitant of " <> T.pack (show t)) $+ do Pair t' e <- forceSynth =<< synthExpr (Just (Some t))+ later $ describe ("a " <> T.pack (show t) <> " rather than a " <> T.pack (show t')) $+ case testEquality t t' of+ Nothing -> later empty+ Just Refl -> return e++-------------------------------------------------------------------------++data LabelInfo :: Type -> Type where+ NoArgLbl :: Label s -> LabelInfo s+ ArgLbl :: forall s ty . LambdaLabel s ty -> LabelInfo s++data ProgramState s =+ ProgramState { _progFunctions :: Map FunctionName FunctionHeader+ , _progForwardDecs :: Map FunctionName FunctionHeader+ , _progGlobals :: Map GlobalName (Some GlobalVar)+ , _progExterns :: Map GlobalName (Some GlobalVar)+ , _progHandleAlloc :: HandleAllocator+ }++progFunctions :: Simple Lens (ProgramState s) (Map FunctionName FunctionHeader)+progFunctions = lens _progFunctions (\s v -> s { _progFunctions = v })++progForwardDecs :: Simple Lens (ProgramState s) (Map FunctionName FunctionHeader)+progForwardDecs = lens _progForwardDecs (\s v -> s { _progForwardDecs = v })++progGlobals :: Simple Lens (ProgramState s) (Map GlobalName (Some GlobalVar))+progGlobals = lens _progGlobals (\s v -> s { _progGlobals = v })++progExterns :: Simple Lens (ProgramState s) (Map GlobalName (Some GlobalVar))+progExterns = lens _progExterns (\s v -> s { _progExterns = v })++progHandleAlloc :: Simple Lens (ProgramState s) HandleAllocator+progHandleAlloc = lens _progHandleAlloc (\s v -> s { _progHandleAlloc = v })+++data SyntaxState s =+ SyntaxState { _stxLabels :: Map LabelName (LabelInfo s)+ , _stxAtoms :: Map AtomName (Some (Atom s))+ , _stxRegisters :: Map RegName (Some (Reg s))+ , _stxNonceGen :: NonceGenerator IO s+ , _stxProgState :: ProgramState s+ }++initProgState :: [(SomeHandle,Position)] -> HandleAllocator -> ProgramState s+initProgState builtIns ha = ProgramState fns Map.empty Map.empty Map.empty ha+ where+ f tps = Ctx.generate+ (Ctx.size tps)+ (\i -> Arg (AtomName ("arg" <> (T.pack (show i)))) InternalPos (tps Ctx.! i))+ fns = Map.fromList+ [ (handleName h,+ FunctionHeader+ (handleName h)+ (f (handleArgTypes h))+ (handleReturnType h)+ h+ p+ )+ | (SomeHandle h,p) <- builtIns+ ]++initSyntaxState :: NonceGenerator IO s -> ProgramState s -> SyntaxState s+initSyntaxState =+ SyntaxState Map.empty Map.empty Map.empty++stxLabels :: Simple Lens (SyntaxState s) (Map LabelName (LabelInfo s))+stxLabels = lens _stxLabels (\s v -> s { _stxLabels = v })++stxAtoms :: Simple Lens (SyntaxState s) (Map AtomName (Some (Atom s)))+stxAtoms = lens _stxAtoms (\s v -> s { _stxAtoms = v })++stxRegisters :: Simple Lens (SyntaxState s) (Map RegName (Some (Reg s)))+stxRegisters = lens _stxRegisters (\s v -> s { _stxRegisters = v })++stxNonceGen :: Getter (SyntaxState s) (NonceGenerator IO s)+stxNonceGen = to _stxNonceGen++stxProgState :: Simple Lens (SyntaxState s) (ProgramState s)+stxProgState = lens _stxProgState (\s v -> s { _stxProgState = v })++stxFunctions :: Simple Lens (SyntaxState s) (Map FunctionName FunctionHeader)+stxFunctions = stxProgState . progFunctions++stxForwardDecs :: Simple Lens (SyntaxState s) (Map FunctionName FunctionHeader)+stxForwardDecs = stxProgState . progForwardDecs++stxGlobals :: Simple Lens (SyntaxState s) (Map GlobalName (Some GlobalVar))+stxGlobals = stxProgState . progGlobals++stxExterns :: Simple Lens (SyntaxState s) (Map GlobalName (Some GlobalVar))+stxExterns = stxProgState . progExterns++newtype CFGParser s ret a =+ CFGParser { runCFGParser :: (?returnType :: TypeRepr ret)+ => ExceptT (ExprErr s)+ (StateT (SyntaxState s) IO)+ a+ }+ deriving (Functor)++instance Applicative (CFGParser s ret) where+ pure x = CFGParser (pure x)+ (CFGParser f) <*> (CFGParser x) = CFGParser (f <*> x)++instance Alternative (CFGParser s ret) where+ empty = CFGParser $ throwError $ TrivialErr InternalPos+ (CFGParser x) <|> (CFGParser y) = CFGParser (x <|> y)++instance Semigroup (CFGParser s ret a) where+ (<>) = (<|>)++instance Monoid (CFGParser s ret a) where+ mempty = empty++instance Monad (CFGParser s ret) where+ (CFGParser m) >>= f = CFGParser $ m >>= \a -> runCFGParser (f a)++instance MonadError (ExprErr s) (CFGParser s ret) where+ throwError e = CFGParser $ throwError e+ catchError m h = CFGParser $ catchError (runCFGParser m) (\e -> runCFGParser $ h e)++instance MonadState (SyntaxState s) (CFGParser s ret) where+ get = CFGParser get+ put s = CFGParser $ put s++instance MonadIO (CFGParser s ret) where+ liftIO io = CFGParser $ lift $ lift io+++freshId :: (MonadState (SyntaxState s) m, MonadIO m) => m (Nonce s tp)+freshId =+ do ng <- use stxNonceGen+ liftIO $ freshNonce ng++freshLabel :: (MonadState (SyntaxState s) m, MonadIO m) => m (Label s)+freshLabel = Label <$> freshId++freshAtom :: ( MonadWriter [Posd (Stmt ext s)] m+ , MonadState (SyntaxState s) m+ , MonadIO m+ , IsSyntaxExtension ext )+ => Position -> AtomValue ext s t -> m (Atom s t)+freshAtom loc v =+ do i <- freshId+ let theAtom = Atom { atomPosition = OtherPos "Parser internals"+ , atomId = i+ , atomSource = Assigned+ , typeOfAtom = typeOfAtomValue v+ }+ stmt = DefineAtom theAtom v+ tell [Posd loc stmt]+ pure theAtom++++newLabel :: (MonadState (SyntaxState s) m, MonadIO m) => LabelName -> m (Label s)+newLabel x =+ do theLbl <- freshLabel+ stxLabels %= Map.insert x (NoArgLbl theLbl)+ return theLbl++freshLambdaLabel :: (MonadState (SyntaxState s) m, MonadIO m) => TypeRepr tp -> m (LambdaLabel s tp, Atom s tp)+freshLambdaLabel t =+ do n <- freshId+ i <- freshId+ let lbl = LambdaLabel n a+ a = Atom { atomPosition = OtherPos "Parser internals"+ , atomId = i+ , atomSource = LambdaArg lbl+ , typeOfAtom = t+ }+ return (lbl, a)++with :: MonadState s m => Lens' s a -> (a -> m b) -> m b+with l act = do x <- use l; act x+++lambdaLabelBinding :: ( MonadSyntax Atomic m+ , MonadState (SyntaxState s) m+ , MonadIO m+ , ?parserHooks :: ParserHooks ext )+ => m (LabelName, Some (LambdaLabel s))+lambdaLabelBinding =+ call $+ depCons uniqueLabel $+ \l ->+ depCons uniqueAtom $+ \x ->+ depCons isType $+ \(Some t) ->+ do (lbl, anAtom) <- freshLambdaLabel t+ stxLabels %= Map.insert l (ArgLbl lbl)+ stxAtoms %= Map.insert x (Some anAtom)+ return (l, Some lbl)++ where uniqueLabel =+ do labels <- use stxLabels+ sideCondition "unique label"+ (\l -> case Map.lookup l labels of+ Nothing -> Just l+ Just _ -> Nothing)+ labelName+++uniqueAtom :: (MonadSyntax Atomic m, MonadState (SyntaxState s) m) => m AtomName+uniqueAtom =+ do atoms <- use stxAtoms+ sideCondition "unique Crucible atom"+ (\x -> case Map.lookup x atoms of+ Nothing -> Just x+ Just _ -> Nothing)+ atomName++newUnassignedReg :: (MonadState (SyntaxState s) m, MonadIO m) => TypeRepr t -> m (Reg s t)+newUnassignedReg t =+ do i <- freshId+ let fakePos = OtherPos "Parser internals"+ return $! Reg { regPosition = fakePos+ , regId = i+ , typeOfReg = t+ }++regRef' :: (MonadSyntax Atomic m, MonadReader (SyntaxState s) m) => m (Some (Reg s))+regRef' =+ describe "known register name" $+ do rn <- regName+ perhapsReg <- view (stxRegisters . at rn)+ case perhapsReg of+ Just reg -> return reg+ Nothing -> empty++globRef' :: (MonadSyntax Atomic m, MonadReader (SyntaxState s) m) => m (Some GlobalVar)+globRef' =+ describe "known global variable name" $+ do x <- globalName+ perhapsGlobal <- view (stxGlobals . at x)+ perhapsExtern <- view (stxExterns . at x)+ case perhapsGlobal <|> perhapsExtern of+ Just glob -> return glob+ Nothing -> empty++++reading :: MonadState r m => ReaderT r m b -> m b+reading m = get >>= runReaderT m++--------------------------------------------------------------------------++atomSetter :: forall m ext s+ . ( MonadSyntax Atomic m+ , MonadWriter [Posd (Stmt ext s)] m+ , MonadState (SyntaxState s) m+ , MonadIO m+ , IsSyntaxExtension ext+ , ?parserHooks :: ParserHooks ext )+ => AtomName -- ^ The name of the atom being set, used for fresh name internals+ -> m (Some (Atom s))+atomSetter (AtomName anText) =+ call ( newref+ <|> emptyref+ <|> fresh+ <|> funcall+ <|> evaluated+ <|> (extensionParser ?parserHooks) )+ where+ fresh, emptyref, newref+ :: ( MonadSyntax Atomic m+ , MonadWriter [Posd (Stmt ext s)] m+ , MonadState (SyntaxState s) m+ , MonadIO m+ , IsSyntaxExtension ext+ )+ => m (Some (Atom s))++ newref =+ do Pair _ e <- reading $ unary Ref synth+ loc <- position+ anAtom <- eval loc e+ anotherAtom <- freshAtom loc (NewRef anAtom)+ return $ Some anotherAtom++ emptyref =+ do Some t' <- reading $ unary EmptyRef isType+ loc <- position+ anAtom <- freshAtom loc (NewEmptyRef t')+ return $ Some anAtom++ fresh =+ do t <- reading (unary Fresh isType)+ -- Note that we are using safeSymbol below to create a What4 symbol+ -- name, which will Z-encode names that aren't legal solver names. This+ -- includes names that include hyphens, which are very common in+ -- S-expression syntax. This is fine to do, since the Z-encoded name+ -- name is only used for solver purposes; the original, unencoded name+ -- is recorded separately.+ let nm = safeSymbol (T.unpack anText)+ loc <- position+ case t of+ Some (FloatRepr fi) ->+ Some <$>+ freshAtom loc (FreshFloat fi (Just nm))+ Some NatRepr ->+ Some <$> freshAtom loc (FreshNat (Just nm))+ Some tp+ | AsBaseType bt <- asBaseType tp ->+ Some <$> freshAtom loc (FreshConstant bt (Just nm))+ | otherwise -> describe "atomic type" $ empty++ evaluated =+ do Pair _ e' <- reading synth+ loc <- position+ anAtom <- eval loc e'+ return $ Some anAtom++-- | Parse a list of operands (for example, the arguments to a function)+operands :: forall s ext m tps+ . ( MonadState (SyntaxState s) m+ , MonadWriter [Posd (Stmt ext s)] m+ , MonadIO m+ , MonadSyntax Atomic m+ , IsSyntaxExtension ext+ , ?parserHooks :: ParserHooks ext )+ -- ParserHooks to use for syntax extensions+ => Ctx.Assignment TypeRepr tps+ -- ^ Types of the operands+ -> m (Ctx.Assignment (Atom s) tps)+ -- ^ Atoms for the operands+operands args = do+ operandExprs <- backwards $ go $ Ctx.viewAssign args+ traverseFC (\(Rand a ex) -> eval (syntaxPos a) ex) operandExprs+ where+ go :: (MonadState (SyntaxState s) m, MonadSyntax Atomic m)+ => Ctx.AssignView TypeRepr args+ -> m (Ctx.Assignment (Rand ext s) args)+ go Ctx.AssignEmpty = emptyList *> pure Ctx.empty+ go (Ctx.AssignExtend ctx' ty) =+ depCons (reading $ check ty) $ \e ->+ do rest <- go (Ctx.viewAssign ctx')+ this <- anything+ return $ Ctx.extend rest $ Rand this e++funcall+ :: forall ext s m+ . ( MonadSyntax Atomic m+ , MonadWriter [Posd (Stmt ext s)] m+ , MonadState (SyntaxState s) m+ , MonadIO m+ , IsSyntaxExtension ext+ , ?parserHooks :: ParserHooks ext+ )+ => m (Some (Atom s))+funcall =+ followedBy (kw Funcall) $+ depConsCond (reading synth) $+ \x ->+ case x of+ (Pair (FunctionHandleRepr funArgs ret) fun) ->+ do loc <- position+ funAtom <- eval loc fun+ operandAtoms <- operands funArgs+ endAtom <- freshAtom loc $ Call funAtom operandAtoms ret+ return $ Right $ Some endAtom+ _ -> return $ Left "a function"+++located :: MonadSyntax atom m => m a -> m (Posd a)+located p = Posd <$> position <*> p++normStmt' :: forall s m ext+ . ( MonadWriter [Posd (Stmt ext s)] m+ , MonadSyntax Atomic m+ , MonadState (SyntaxState s) m+ , MonadIO m+ , IsSyntaxExtension ext+ , ?parserHooks :: ParserHooks ext) =>+ m ()+normStmt' =+ call (printStmt <|> printLnStmt <|> letStmt <|> (void funcall) <|>+ setGlobal <|> setReg <|> setRef <|> dropRef <|>+ assertion <|> assumption <|> breakpoint <|>+ (void (extensionParser ?parserHooks)))++ where+ printStmt, printLnStmt, letStmt, setGlobal, setReg, setRef, dropRef, assertion, breakpoint :: m ()+ printStmt =+ do Posd loc e <- unary Print_ (located $ reading $ check (StringRepr UnicodeRepr))+ strAtom <- eval loc e+ tell [Posd loc (Print strAtom)]++ printLnStmt =+ do Posd loc e <- unary PrintLn_ (located $ reading $ check (StringRepr UnicodeRepr))+ strAtom <- eval loc (EApp (StringConcat UnicodeRepr e (EApp (StringLit "\n"))))+ tell [Posd loc (Print strAtom)]++ letStmt =+ followedBy (kw Let) $+ depCons uniqueAtom $+ \x ->+ do setter <- fst <$> cons (atomSetter x) emptyList+ stxAtoms %= Map.insert x setter++ setGlobal =+ followedBy (kw SetGlobal) $+ depConsCond globalName $+ \g ->+ use (stxGlobals . at g) >>=+ \case+ Nothing -> return $ Left "known global variable name"+ Just (Some var) ->+ do (Posd loc e) <- fst <$> cons (located $ reading $ check $ globalType var) emptyList+ a <- eval loc e+ tell [Posd loc $ WriteGlobal var a]+ return (Right ())++ setReg =+ followedBy (kw SetRegister) $+ depCons (reading regRef') $+ \(Some r) ->+ depCons (reading $ located $ check $ typeOfReg r) $+ \(Posd loc e) ->+ do emptyList+ v <- eval loc e+ tell [Posd loc $ SetReg r v]++ setRef =+ do stmtLoc <- position+ followedBy (kw SetRef) $+ depConsCond (located $ reading $ synth) $+ \case+ (Posd refLoc (Pair (ReferenceRepr t') refE)) ->+ depCons (located $ reading $ check t') $+ \(Posd valLoc valE) ->+ do emptyList+ refAtom <- eval refLoc refE+ valAtom <- eval valLoc valE+ tell [Posd stmtLoc $ WriteRef refAtom valAtom]+ return (Right ())+ (Posd _ _) ->+ return $ Left "expression with reference type"++ dropRef =+ do loc <- position+ followedBy (kw DropRef_) $+ depConsCond (located $ reading synth) $+ \(Posd eLoc (Pair t refE)) ->+ emptyList *>+ case t of+ ReferenceRepr _ ->+ do refAtom <- eval eLoc refE+ tell [Posd loc $ DropRef refAtom]+ return $ Right ()+ _ -> return $ Left "expression with reference type"++ assertion =+ do (Posd loc (Posd cLoc cond, Posd mLoc msg)) <-+ located $+ binary Assert_+ (located $ reading $ check BoolRepr)+ (located $ reading $ check (StringRepr UnicodeRepr))+ cond' <- eval cLoc cond+ msg' <- eval mLoc msg+ tell [Posd loc $ Assert cond' msg']++ assumption =+ do (Posd loc (Posd cLoc cond, Posd mLoc msg)) <-+ located $+ binary Assume_+ (located $ reading $ check BoolRepr)+ (located $ reading $ check (StringRepr UnicodeRepr))+ cond' <- eval cLoc cond+ msg' <- eval mLoc msg+ tell [Posd loc $ Assume cond' msg']++ breakpoint =+ do (Posd loc (nm, arg_list)) <-+ located $ binary Breakpoint_+ (string <&> BreakpointName)+ (rep ra_value)+ case toCtx arg_list of+ Some args -> tell [Posd loc $ Breakpoint nm args]+ where+ ra_value :: m (Some (Value s))+ ra_value = (reading synth) >>= \case+ Pair _ (EReg _ reg) -> pure $ Some $ RegValue reg+ Pair _ (EAtom atm) -> pure $ Some $ AtomValue atm+ _ -> empty+++blockBody' :: forall s ret m ext+ . ( MonadSyntax Atomic m+ , MonadState (SyntaxState s) m+ , MonadIO m+ , IsSyntaxExtension ext+ , ?parserHooks :: ParserHooks ext )+ => TypeRepr ret+ -> m (Posd (TermStmt s ret), [Posd (Stmt ext s)])+blockBody' ret = runWriterT go+ where+ go :: WriterT [Posd (Stmt ext s)] m (Posd (TermStmt s ret))+ go = (fst <$> (cons (later (termStmt' ret)) emptyList)) <|>+ (snd <$> (cons (later normStmt') go))++termStmt' :: forall m s ret ext.+ ( MonadWriter [Posd (Stmt ext s)] m+ , MonadSyntax Atomic m+ , MonadState (SyntaxState s) m+ , MonadIO m+ , IsSyntaxExtension ext+ , ?parserHooks :: ParserHooks ext ) =>+ TypeRepr ret -> m (Posd (TermStmt s ret))+termStmt' retTy =+ do stx <- anything+ call (withPosFrom stx <$>+ (jump <|> branch <|> maybeBranch <|> cases <|> ret <|> err <|> tailCall <|> out))++ where+ normalLabel =+ do x <- labelName+ l <- use (stxLabels . at x)+ later $ describe "known label with no arguments" $+ case l of+ Nothing -> empty+ Just (ArgLbl _) -> empty+ Just (NoArgLbl lbl) -> pure lbl++ lambdaLabel :: m (Some (LambdaLabel s))+ lambdaLabel =+ do x <- labelName+ l <- use (stxLabels . at x)+ later $ describe "known label with an argument" $+ case l of+ Nothing -> empty+ Just (ArgLbl lbl) -> pure $ Some lbl+ Just (NoArgLbl _) -> empty++ typedLambdaLabel :: TypeRepr t -> m (LambdaLabel s t)+ typedLambdaLabel t =+ do x <- labelName+ l <- use (stxLabels . at x)+ later $ describe ("known label with an " <> T.pack (show t) <> " argument") $+ case l of+ Nothing -> empty+ Just (ArgLbl lbl) ->+ case testEquality (typeOfAtom (lambdaAtom lbl)) t of+ Nothing -> empty+ Just Refl -> pure lbl+ Just (NoArgLbl _) -> empty++ jump = unary Jump_ normalLabel <&> Jump++ branch = kw Branch_ `followedBy`+ (depCons (located (reading (check BoolRepr))) $+ \ (Posd eloc cond) ->+ cons normalLabel (cons normalLabel emptyList) >>=+ \(l1, (l2, ())) -> do+ c <- eval eloc cond+ return (Br c l1 l2))++ maybeBranch :: m (TermStmt s ret)+ maybeBranch =+ followedBy (kw MaybeBranch_) $+ describe "valid arguments to maybe-branch" $+ depCons (located (reading synth)) $+ \(Posd sloc (Pair ty scrut)) ->+ case ty of+ MaybeRepr ty' ->+ depCons (typedLambdaLabel ty') $+ \lbl1 ->+ depCons normalLabel $+ \ lbl2 ->+ do s <- eval sloc scrut+ return $ MaybeBranch ty' s lbl1 lbl2+ _ -> empty++ cases :: m (TermStmt s ret)+ cases =+ followedBy (kw Case) $+ depCons (located (reading synth)) $+ \(Posd tgtloc (Pair ty tgt)) ->+ describe ("cases for variant type " <> T.pack (show ty)) $+ case ty of+ VariantRepr ctx ->+ do t <- eval tgtloc tgt+ VariantElim ctx t <$> backwards (go (Ctx.viewAssign ctx))+ _ -> empty+ where+ go :: forall cases+ . Ctx.AssignView TypeRepr cases+ -> m (Ctx.Assignment (LambdaLabel s) cases)+ go Ctx.AssignEmpty = emptyList $> Ctx.empty+ go (Ctx.AssignExtend ctx' t) =+ depCons (typedLambdaLabel t) $+ \ lbl -> Ctx.extend <$>+ go (Ctx.viewAssign ctx') <*>+ pure lbl++ ret :: m (TermStmt s ret)+ ret =+ do Posd loc e <- unary Return_ (located (reading (check retTy)))+ Return <$> eval loc e++ tailCall :: m (TermStmt s ret)+ tailCall =+ followedBy (kw TailCall_) $+ describe "function atom and arguments" $+ do -- commit+ depCons (located (reading synth)) $+ \case+ Posd loc (Pair (FunctionHandleRepr argumentTypes retTy') funExpr) ->+ case testEquality retTy retTy' of+ Nothing -> empty+ Just Refl ->+ do funAtom <- eval loc funExpr+ describe ("arguments with types " <> T.pack (show argumentTypes)) $+ TailCall funAtom argumentTypes <$> backwards (go (Ctx.viewAssign argumentTypes))+ _ -> empty+ where+ go :: forall argTypes+ . Ctx.AssignView TypeRepr argTypes+ -> m (Ctx.Assignment (Atom s) argTypes)+ go Ctx.AssignEmpty = emptyList *> pure Ctx.empty+ go (Ctx.AssignExtend tys ty) =+ depCons (located (reading (check ty))) $+ \(Posd loc arg) ->+ Ctx.extend <$> go (Ctx.viewAssign tys) <*> eval loc arg++ err :: m (TermStmt s ret)+ err =+ do Posd loc e <- unary Error_ (located (reading (check (StringRepr UnicodeRepr))))+ ErrorStmt <$> eval loc e++ out :: m (TermStmt s ret)+ out = followedBy (kw Output_) $+ do -- commit+ depCons lambdaLabel $+ \(Some lbl) ->+ depCons (located (reading (check (typeOfAtom (lambdaAtom lbl))))) $+ \(Posd loc arg) ->+ emptyList *>+ (Output lbl <$> eval loc arg)++++data Rand ext s t = Rand (AST s) (E ext s t)+++++--------------------------------------------------------------------------++data Arg t = Arg AtomName Position (TypeRepr t)++someAssign ::+ forall m ext a.+ ( MonadSyntax Atomic m+ , ?parserHooks :: ParserHooks ext+ ) =>+ Text ->+ m (Some a) ->+ m (Some (Ctx.Assignment a))+someAssign desc sub = call (go (Some Ctx.empty))+ where+ go :: Some (Ctx.Assignment a) -> m (Some (Ctx.Assignment a))+ go args@(Some prev) =+ describe desc $+ (emptyList *> pure args) <|>+ (depCons sub $+ \(Some a) ->+ go (Some $ Ctx.extend prev a))++arguments' :: forall m ext+ . ( MonadSyntax Atomic m, ?parserHooks :: ParserHooks ext )+ => m (Some (Ctx.Assignment Arg))+arguments' = someAssign "argument list" oneArg+ where oneArg =+ (describe "argument" $+ located $+ cons atomName (cons isType emptyList)) <&>+ \(Posd loc (x, (Some t, ()))) -> Some (Arg x loc t)+++saveArgs :: (MonadState (SyntaxState s) m, MonadError (ExprErr s) m)+ => Ctx.Assignment Arg init+ -> Ctx.Assignment (Atom s) init+ -> m ()+saveArgs ctx1 ctx2 =+ let combined = Ctx.zipWith+ (\(Arg x p _) argAtom ->+ (Const (Some (Functor.Pair (Const x) (Functor.Pair (Const p) argAtom)))))+ ctx1 ctx2+ in forFC_ combined $+ \(Const (Some (Functor.Pair (Const x) (Functor.Pair (Const argPos) y)))) ->+ with (stxAtoms . at x) $+ \case+ Just _ -> throwError $ DuplicateAtom argPos x+ Nothing ->+ do stxAtoms %= Map.insert x (Some y)++data FunctionHeader =+ forall args ret .+ FunctionHeader { _headerName :: FunctionName+ , _headerArgs :: Ctx.Assignment Arg args+ , _headerReturnType :: TypeRepr ret+ , _headerHandle :: FnHandle args ret+ , _headerLoc :: Position+ }++data FunctionSource s =+ FunctionSource { _functionRegisters :: [AST s]+ , _functionBody :: AST s+ }++functionHeader' :: ( MonadSyntax Atomic m, ?parserHooks :: ParserHooks ext )+ => m ( (FunctionName, Some (Ctx.Assignment Arg), Some TypeRepr, Position)+ , FunctionSource s+ )+functionHeader' =+ do (fnName, (Some theArgs, (Some ret, (regs, body)))) <-+ followedBy (kw Defun) $+ cons funName $+ cons arguments' $+ cons isType $+ cons registers anything <|> ([], ) <$> anything+ loc <- position+ return ((fnName, Some theArgs, Some ret, loc), FunctionSource regs body)+ where+ registers = call $ kw Registers `followedBy` anyList++functionHeader :: (?parserHooks :: ParserHooks ext)+ => AST s+ -> TopParser s (FunctionHeader, FunctionSource s)+functionHeader defun =+ do ((fnName, Some theArgs, Some ret, loc), src) <- liftSyntaxParse functionHeader' defun+ ha <- use $ stxProgState . progHandleAlloc+ handle <- liftIO $ mkHandle' ha fnName (argTypes theArgs) ret+ let header = FunctionHeader fnName theArgs ret handle loc++ saveHeader fnName header+ return $ (header, src)+ where+ saveHeader n h =+ stxFunctions %= Map.insert n h+++++global :: (?parserHooks :: ParserHooks ext)+ => AST s+ -> TopParser s (Some GlobalVar)+global stx =+ do (var@(GlobalName varName), Some t) <- liftSyntaxParse (call (binary DefGlobal globalName isType)) stx+ ha <- use $ stxProgState . progHandleAlloc+ v <- liftIO $ freshGlobalVar ha varName t+ let sv = Some v+ stxGlobals %= Map.insert var sv+ return sv++-- | Parse a forward declaration.+declare :: (?parserHooks :: ParserHooks ext)+ => AST t+ -> TopParser s FunctionHeader+declare stx =+ do ((fnName, (Some theArgs, (Some ret, ()))), loc) <-+ liftSyntaxParse (do r <- followedBy (kw Declare) $+ cons funName $+ cons arguments' $+ cons isType emptyList+ loc <- position+ pure (r, loc))+ stx+ ha <- use $ stxProgState . progHandleAlloc+ handle <- liftIO $ mkHandle' ha fnName (argTypes theArgs) ret++ let header = FunctionHeader fnName theArgs ret handle loc+ stxForwardDecs %= Map.insert fnName header+ pure header++-- | Parse an extern.+extern :: (?parserHooks :: ParserHooks ext)+ => AST s+ -> TopParser s (Some GlobalVar)+extern stx =+ do (var@(GlobalName varName), Some t) <- liftSyntaxParse (call (binary Extern globalName isType)) stx+ ha <- use $ stxProgState . progHandleAlloc+ v <- liftIO $ freshGlobalVar ha varName t+ let sv = Some v+ stxExterns %= Map.insert var sv+ return sv++topLevel :: (?parserHooks :: ParserHooks ext)+ => AST s+ -> TopParser s (Maybe (FunctionHeader, FunctionSource s))+topLevel ast =+ (Just <$> functionHeader ast) `catchError` \e ->+ (global ast $> Nothing) `catchError` \_ ->+ (declare ast $> Nothing) `catchError` \_ ->+ (extern ast $> Nothing) `catchError` \_ ->+ throwError e++argTypes :: Ctx.Assignment Arg init -> Ctx.Assignment TypeRepr init+argTypes = fmapFC (\(Arg _ _ t) -> t)+++type BlockTodo s ret =+ (LabelName, BlockID s, Progress, AST s)++blocks :: forall s ret m ext+ . ( MonadState (SyntaxState s) m+ , MonadSyntax Atomic m+ , MonadIO m+ , TraverseExt ext+ , IsSyntaxExtension ext+ , ?parserHooks :: ParserHooks ext )+ => TypeRepr ret+ -> m [Block ext s ret]+blocks ret =+ depCons startBlock' $+ \ startContents ->+ do todo <- rep blockLabel'+ forM (startContents : todo) $ \(_, bid, pr, stmts) ->+ do (term, stmts') <- withProgress (const pr) $ parse stmts (call (blockBody' ret))+ pure $ mkBlock bid mempty (Seq.fromList stmts') term+++ where++ startBlock' :: (MonadState (SyntaxState s) m, MonadSyntax Atomic m, MonadIO m) => m (BlockTodo s ret)+ startBlock' =+ call $+ describe "starting block" $+ followedBy (kw Start) $+ depCons labelName $+ \l ->+ do lbl <- newLabel l+ pr <- progress+ rest <- anything+ return (l, LabelID lbl, pr, rest)++ blockLabel' :: m (BlockTodo s ret)+ blockLabel' =+ call $+ followedBy (kw DefBlock) $+ simpleBlock <|> argBlock+ where+ simpleBlock, argBlock :: m (BlockTodo s ret)+ simpleBlock =+ depConsCond labelName $+ \ l ->+ do lbls <- use stxLabels+ pr <- progress+ body <- anything+ case Map.lookup l lbls of+ Just _ -> return $ Left "unique label"+ Nothing ->+ do theLbl <- newLabel l+ return $ Right (l, LabelID theLbl, pr, body)+ argBlock =+ call $+ depConsCond lambdaLabelBinding $+ \ (l, (Some lbl)) ->+ do pr <- progress+ body <- anything+ return $ Right (l, LambdaID lbl, pr, body)++eval :: (MonadWriter [Posd (Stmt ext s)] m, MonadState (SyntaxState s) m, MonadIO m, IsSyntaxExtension ext)+ => Position -> E ext s t -> m (Atom s t)+eval _ (EAtom theAtom) = pure theAtom -- The expression is already evaluated+eval loc (EApp e) = freshAtom loc . EvalApp =<< traverseFC (eval loc) e+eval _ (EReg loc reg) = freshAtom loc (ReadReg reg)+eval _ (EGlob loc glob) = freshAtom loc (ReadGlobal glob)+eval loc (EDeref eloc e) = freshAtom loc . ReadRef =<< eval eloc e++newtype TopParser s a =+ TopParser { runTopParser :: ExceptT (ExprErr s)+ (StateT (SyntaxState s) IO)+ a+ }+ deriving (Functor)++top :: NonceGenerator IO s -> HandleAllocator -> [(SomeHandle,Position)] -> TopParser s a -> IO (Either (ExprErr s) a)+top ng ha builtIns (TopParser (ExceptT (StateT act))) =+ fst <$> act (initSyntaxState ng (initProgState builtIns ha))++instance Applicative (TopParser s) where+ pure x = TopParser (pure x)+ (TopParser f) <*> (TopParser x) = TopParser (f <*> x)++instance Alternative (TopParser s) where+ empty = TopParser $ throwError (TrivialErr InternalPos)+ (TopParser x) <|> (TopParser y) = TopParser (x <|> y)++instance MonadPlus (TopParser s) where+ mzero = empty+ mplus = (<|>)++instance Semigroup (TopParser s a) where+ (<>) = (<|>)++instance Monoid (TopParser s a) where+ mempty = empty++instance Monad (TopParser s) where+ (TopParser m) >>= f = TopParser $ m >>= runTopParser . f++instance MonadError (ExprErr s) (TopParser s) where+ throwError = TopParser . throwError+ catchError m h = TopParser $ catchError (runTopParser m) (runTopParser . h)++instance MonadState (SyntaxState s) (TopParser s) where+ get = TopParser get+ put = TopParser . put++instance MonadIO (TopParser s) where+ liftIO = TopParser . lift . lift+++initParser :: forall s m ext+ . ( MonadState (SyntaxState s) m+ , MonadError (ExprErr s) m+ , MonadIO m+ , ?parserHooks :: ParserHooks ext )+ => FunctionHeader+ -> FunctionSource s+ -> m ()+initParser (FunctionHeader _ (funArgs :: Ctx.Assignment Arg init) _ _ _) (FunctionSource regs _) =+ do ng <- use stxNonceGen+ progState <- use stxProgState+ put $ initSyntaxState ng progState+ let types = argTypes funArgs+ inputAtoms <- liftIO $ mkInputAtoms ng (OtherPos "args") types+ saveArgs funArgs inputAtoms+ forM_ regs saveRegister++ where+ saveRegister :: Syntax Atomic -> m ()+ saveRegister (L [A (Rg x), t]) =+ do Some ty <- liftSyntaxParse isType t+ r <- newUnassignedReg ty+ stxRegisters %= Map.insert x (Some r)+ saveRegister other = throwError $ InvalidRegister (syntaxPos other) other++cfgs :: ( IsSyntaxExtension ext+ , ?parserHooks :: ParserHooks ext )+ => [AST s]+ -> TopParser s [AnyCFG ext]+cfgs = fmap parsedProgCFGs <$> prog++prog :: ( TraverseExt ext+ , IsSyntaxExtension ext+ , ?parserHooks :: ParserHooks ext )+ => [AST s]+ -> TopParser s (ParsedProgram ext)+prog defuns =+ do headers <- catMaybes <$> traverse topLevel defuns+ cs <- forM headers $+ \(hdr@(FunctionHeader _ _ ret handle _), src@(FunctionSource _ body)) ->+ do initParser hdr src+ args <- toList <$> use stxAtoms+ let ?returnType = ret+ st <- get+ (theBlocks, st') <- liftSyntaxParse (runStateT (blocks ret) st) body+ put st'+ let vs = Set.fromList [ Some (AtomValue a) | Some a <- args ]+ case theBlocks of+ [] -> error "found no blocks"+ (e:rest) ->+ do let entry = case blockID e of+ LabelID lbl -> lbl+ LambdaID {} -> error "initial block is lambda"+ e' = mkBlock (blockID e) vs (blockStmts e) (blockTerm e)+ return $ AnyCFG (CFG handle entry (e' : rest))+ gs <- use stxGlobals+ externs <- use stxExterns+ fds <- uses stxForwardDecs $ fmap $+ \(FunctionHeader _ _ _ handle _) -> SomeHandle handle+ return $ ParsedProgram+ { parsedProgGlobals = gs+ , parsedProgExterns = externs+ , parsedProgCFGs = cs+ , parsedProgForwardDecs = fds+ }
+ src/Lang/Crucible/Syntax/ExprParse.hs view
@@ -0,0 +1,282 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}++module Lang.Crucible.Syntax.ExprParse+ ( SyntaxParse+ , syntaxParseIO++ -- * Errors+ , SyntaxError(..)+ , printSyntaxError++ -- * Testing utilities+ , TrivialAtom(..)+ , test+ ) where++import Control.Applicative+import Control.Lens hiding (List, cons, backwards)+import Control.Monad (MonadPlus(..), ap)+import Control.Monad.IO.Class (MonadIO)+import Control.Monad.Reader (MonadReader(..), ReaderT(..))+import qualified Control.Monad.State.Strict as Strict++import Data.Foldable as Foldable+import Data.List+import qualified Data.List.NonEmpty as NE+import Data.List.NonEmpty (NonEmpty(..))+import Data.String+import Data.Text (Text)+import qualified Data.Text as T+import qualified Data.Text.IO as T++import GHC.Stack++import Lang.Crucible.Syntax.SExpr++import qualified Text.Megaparsec as MP++import Lang.Crucible.Syntax.Monad++data Search a = Try a (Search a) | Fail | Cut+ deriving Functor++instance Applicative Search where+ pure x = Try x Fail+ (<*>) = ap++instance Alternative Search where+ empty = Fail+ x <|> y =+ case x of+ Try first rest -> Try first (rest <|> y)+ Fail -> y+ Cut -> Cut++instance Monad Search where+ m >>= f =+ case m of+ Try x more -> f x <|> (more >>= f)+ Fail -> Fail+ Cut -> Fail++instance MonadPlus Search where+ mzero = empty+ mplus = (<|>)++instance Semigroup (Search a) where+ (<>) = (<|>)++instance Monoid (Search a) where+ mempty = empty++instance Foldable Search where+ foldMap f (Try x xs) = f x `mappend` foldMap f xs+ foldMap _ _ = mempty++ toList (Try x xs) = x : toList xs+ toList _ = []++instance Traversable Search where+ traverse f (Try x xs) = Try <$> f x <*> traverse f xs+ traverse _ Fail = pure Fail+ traverse _ Cut = pure Cut++delimitSearch :: Search a -> Search a+delimitSearch (Try first rest) = Try first $ delimitSearch rest+delimitSearch Fail = Fail+delimitSearch Cut = Fail++cutSearch :: Search a+cutSearch = Cut++data Failure atom = Ok | Oops Progress (NonEmpty (Reason atom))+ deriving (Functor, Show)++instance Semigroup (Failure atom) where+ Ok <> e2 = e2+ e1@(Oops _ _) <> Ok = e1+ e1@(Oops p1 r1) <> e2@(Oops p2 r2) =+ case compare p1 p2 of+ LT -> e2+ GT -> e1+ EQ -> Oops p1 (r1 <> r2)++instance Monoid (Failure atom) where+ mempty = Ok++data P atom a = P { _success :: Search a+ , _failure :: Failure atom+ }+ deriving Functor++instance Semigroup (P atom a) where+ P s1 f1 <> P s2 f2 = P (s1 <> s2) (f1 <> f2)++instance Monoid (P atom a) where+ mempty = P mempty mempty++instance Applicative (P atom) where+ pure x = P (pure x) mempty+ f <*> x = ap f x++instance Alternative (P atom) where+ empty = mempty+ (<|>) = mappend++instance Monad (P atom) where+ (P xs e) >>= f = mappend (foldMap f xs) (P empty e)++instance MonadPlus (P atom) where+ mzero = empty+ mplus = (<|>)++newtype STP atom a = STP { runSTP :: IO (P atom a) }+ deriving (Functor, Semigroup, Monoid)++instance Applicative (STP atom) where+ pure = STP . pure . pure+ (<*>) = ap++instance Monad (STP atom) where+ STP m >>= f = STP $ do+ P xs e <- m+ mappend (runSTP (foldMap f xs)) (return $ P empty e)++instance MonadIO (STP atom) where+ liftIO m = STP $ return <$> m++data SyntaxParseCtx atom =+ SyntaxParseCtx { _parseProgress :: Progress+ , _parseReason :: Reason atom+ , _parseFocus :: Syntax atom+ }+ deriving Show++parseProgress :: Simple Lens (SyntaxParseCtx atom) Progress+parseProgress = lens _parseProgress (\s v -> s { _parseProgress = v })++parseReason :: Simple Lens (SyntaxParseCtx atom) (Reason atom)+parseReason = lens _parseReason (\s v -> s { _parseReason = v })++parseFocus :: Simple Lens (SyntaxParseCtx atom) (Syntax atom)+parseFocus = lens _parseFocus (\s v -> s { _parseFocus = v })++-- | The default parsing monad. Use its 'MonadSyntax' instance to write parsers.+newtype SyntaxParse atom a =+ SyntaxParse { runSyntaxParse :: ReaderT (SyntaxParseCtx atom)+ (STP atom)+ a }+ deriving ( Functor, Applicative, Monad+ , MonadReader (SyntaxParseCtx atom), MonadIO+ )++instance Alternative (SyntaxParse atom) where+ empty =+ SyntaxParse $ ReaderT $ \(SyntaxParseCtx p r _) ->+ STP $ return $ P empty (Oops p (pure r))+ (SyntaxParse (ReaderT x)) <|> (SyntaxParse (ReaderT y)) =+ SyntaxParse $ ReaderT $ \ctx -> STP $ do+ a <- runSTP $ x ctx+ b <- runSTP $ y ctx+ return $ a <|> b++instance MonadPlus (SyntaxParse atom) where+ mzero = empty+ mplus = (<|>)++instance MonadSyntax atom (SyntaxParse atom) where+ anything = view parseFocus+ progress = view parseProgress+ withFocus stx = local $ set parseFocus stx+ withProgress f = local $ over parseProgress f+ withReason r = local $ set parseReason r+ cut =+ SyntaxParse $+ ReaderT $+ \(SyntaxParseCtx p r _) ->+ STP $ return $+ P cutSearch (Oops p (pure r))+ delimit (SyntaxParse (ReaderT f)) =+ SyntaxParse $+ ReaderT $+ \r -> STP $ do+ P s e <- runSTP $ f r+ return $ P (delimitSearch s) e+ call (SyntaxParse (ReaderT p)) =+ SyntaxParse $+ ReaderT $+ \r -> STP $ do+ P s e <- runSTP $ p r+ return $ case s of+ Try x _ -> P (Try x Fail) Ok+ Cut -> P Cut e+ Fail -> P Fail e++-- | Syntax errors explain why the error occurred.+data SyntaxError atom = SyntaxError (NonEmpty (Reason atom))+ deriving (Show, Eq)++-- | Convert an internal error structure into a form suitable for+-- humans to read.+printSyntaxError :: IsAtom atom => SyntaxError atom -> Text+printSyntaxError (SyntaxError rs) =+ T.intercalate "\n\tor\n" $ nub $ map printGroup $ groupReasons rs+ where+ reasonPos (Reason found _) = syntaxPos found+ groupReasons reasons =+ [ (reasonPos repr, g)+ | g@(repr :| _) <- NE.groupBy (\x y -> reasonPos x == reasonPos y) (NE.toList reasons)+ ]+ printGroup (p, r@(Reason found _) :| more) =+ T.concat+ [ "At ", T.pack (show p)+ , ", expected ", T.intercalate " or " (nub $ sort [ wanted | Reason _ wanted <- r:more ])+ , " but got ", toText mempty found]++-- | Attempt to parse the given piece of syntax, returning the first success found,+-- or the error(s) with the greatest progress otherwise.+syntaxParseIO :: IsAtom atom => SyntaxParse atom a -> Syntax atom -> IO (Either (SyntaxError atom) a)+syntaxParseIO p stx = do+ (P yes no) <-+ runSTP $ runReaderT (runSyntaxParse p) $+ SyntaxParseCtx emptyProgress (Reason stx (T.pack "bad syntax")) stx+ case Foldable.toList yes of+ [] ->+ return $ Left $ SyntaxError $+ case no of+ Ok -> error "Internal error: no reason provided, yet no successful parse found."+ Oops _ rs -> rs+ (r:_) -> return $ Right r++-- | A trivial atom, which is a wrapper around 'Text', for use when testing the library.+newtype TrivialAtom = TrivialAtom Text deriving (Show, Eq)++instance IsAtom TrivialAtom where+ showAtom (TrivialAtom x) = x++instance IsString TrivialAtom where+ fromString x = TrivialAtom (fromString x)++-- | Test a parser on some input, displaying the result.+test :: (HasCallStack, Show a) => Text -> SyntaxParse TrivialAtom a -> IO ()+test txt p =+ case MP.parse (skipWhitespace *> sexp (TrivialAtom <$> identifier) <* MP.eof) "input" txt of+ Left err -> putStrLn "Reader error: " >> putStrLn (MP.errorBundlePretty err)+ Right sexpr ->+ syntaxParseIO p sexpr >>= \case+ Left e -> T.putStrLn (printSyntaxError e)+ Right ok -> print ok
+ src/Lang/Crucible/Syntax/Monad.hs view
@@ -0,0 +1,524 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}++module Lang.Crucible.Syntax.Monad+ ( MonadSyntax(..)++ -- * Describing syntax+ , describe+ , atom+ , cons+ , depCons+ , depConsCond+ , followedBy+ , rep+ , list+ , backwards+ , emptyList+ , atomic+ , anyList+ , sideCondition+ , sideCondition'+ , satisfy++ -- * Eliminating location information+ , syntaxToDatum+ , datum++ -- * Parsing context+ , position+ , withProgressStep++ -- * Control structures+ , commit+ , parse++ -- * Progress through a parsing problem+ , ProgressStep(..)+ , Progress+ , emptyProgress+ , pushProgress++ -- * Errors+ , later+ , Reason(..)+ ) where++import Control.Applicative+import Control.Monad (MonadPlus(..), ap)+import Control.Monad.Reader (MonadReader(..), ReaderT(..))+import qualified Control.Monad.State.Strict as Strict+import qualified Control.Monad.State.Lazy as Lazy+import Control.Monad.State.Class+import Control.Monad.Trans.Class (MonadTrans(..))+import qualified Control.Monad.Writer.Strict as Strict+import qualified Control.Monad.Writer.Lazy as Lazy+import Control.Monad.Writer.Class++import Data.Foldable as Foldable+import Data.List.NonEmpty (NonEmpty(..))+import Data.Text (Text)+import qualified Data.Text as T++import Lang.Crucible.Syntax.SExpr++import What4.ProgramLoc (Posd(..), Position)++data Search a = Try a (Search a) | Fail | Cut+ deriving Functor++instance Applicative Search where+ pure x = Try x Fail+ (<*>) = ap++instance Alternative Search where+ empty = Fail+ x <|> y =+ case x of+ Try first rest -> Try first (rest <|> y)+ Fail -> y+ Cut -> Cut++instance Monad Search where+ m >>= f =+ case m of+ Try x more -> f x <|> (more >>= f)+ Fail -> Fail+ Cut -> Fail++instance MonadPlus Search where+ mzero = empty+ mplus = (<|>)++instance Semigroup (Search a) where+ (<>) = (<|>)++instance Monoid (Search a) where+ mempty = empty++instance Foldable Search where+ foldMap f (Try x xs) = f x `mappend` foldMap f xs+ foldMap _ _ = mempty++ toList (Try x xs) = x : toList xs+ toList _ = []++instance Traversable Search where+ traverse f (Try x xs) = Try <$> f x <*> traverse f xs+ traverse _ Fail = pure Fail+ traverse _ Cut = pure Cut++-- | Components of a path taken through a syntax object to reach the+-- current focus.+data ProgressStep =+ First -- ^ The head of a list was followed+ | Rest -- ^ The tail of a list was followed+ | Late -- ^ The path was annotated as 'later'+ deriving (Eq, Show)++instance Ord ProgressStep where+ compare First First = EQ+ compare First _ = LT+ compare Rest First = GT+ compare Rest Rest = EQ+ compare Rest _ = LT+ compare Late Late = EQ+ compare Late _ = GT++-- | The path taken through a syntax object to reach the current+-- focus.+newtype Progress = Progress [ProgressStep]+ deriving (Eq, Show)++-- | An empty path, used to initialize parsers+emptyProgress :: Progress+emptyProgress = Progress []++-- | Add a step to a progress path+pushProgress :: ProgressStep -> Progress -> Progress+pushProgress p (Progress ps) = Progress (p : ps)++instance Ord Progress where+ compare (Progress xs) (Progress ys) =+ case (xs, ys) of+ ([], []) -> EQ+ ([], _:_) -> LT+ (_:_, []) -> GT+ (x:xs', y:ys') ->+ case compare (Progress xs') (Progress ys') of+ LT -> LT+ GT -> GT+ EQ -> compare x y+++-- | The reason why a failure has occurred, consisting of description+-- 'message' combined with the focus that was described.+data Reason atom = Reason { expr :: Syntax atom+ , message :: Text+ }+ deriving (Functor, Show, Eq)++data Failure atom = Ok | Oops Progress (NonEmpty (Reason atom))+ deriving (Functor, Show)++instance Semigroup (Failure atom) where+ Ok <> e2 = e2+ e1@(Oops _ _) <> Ok = e1+ e1@(Oops p1 r1) <> e2@(Oops p2 r2) =+ case compare p1 p2 of+ LT -> e2+ GT -> e1+ EQ -> Oops p1 (r1 <> r2)++instance Monoid (Failure atom) where+ mempty = Ok++data P atom a = P { _success :: Search a+ , _failure :: Failure atom+ }+ deriving Functor++-- | Monads that can parse syntax need a few fundamental operations.+-- A parsing monad maintains an implicit "focus", which is the syntax+-- currently being matched, as well as the progress, which is the path+-- taken through the surrounding syntactic context to reach the+-- current focus. Additionally, the reason for a failure will always+-- be reported with respect to explicit descriptions - these are+-- inserted through 'withReason'.+class (Alternative m, Monad m) => MonadSyntax atom m | m -> atom where+ -- | Succeed with the current focus.+ anything :: m (Syntax atom)+ -- | Succeed with the current progress.+ progress :: m Progress+ -- | Run a new parser with a different focus.+ withFocus :: Syntax atom -> m a -> m a+ -- | Run a parser in a modified notion of progress.+ withProgress :: (Progress -> Progress) -> m a -> m a+ -- | Run a parser with a new reason for failure.+ withReason :: Reason atom -> m a -> m a+ -- | Fail, and additionally prohibit backtracking across the failure.+ cut :: m a+ -- | Delimit the dynamic extent of a 'cut'.+ delimit :: m a -> m a+ -- | Make the first solution reported by a computation into the only+ -- solution reported, eliminating further backtracking and previous+ -- errors. This allows syntax to be matched in exclusive "layers",+ -- reminiscent of the effect of trampolining through a macro+ -- expander. Use when solutions are expected to be unique.+ call :: m a -> m a++instance MonadSyntax atom m => MonadSyntax atom (ReaderT r m) where+ anything = lift anything+ cut = lift cut+ progress = lift progress+ delimit m =+ do r <- ask+ lift $ delimit (runReaderT m r)+ call m =+ do r <- ask+ lift $ call (runReaderT m r)+ withFocus stx m =+ do r <- ask+ lift $ withFocus stx (runReaderT m r)+ withProgress p m =+ do r <- ask+ lift $ withProgress p (runReaderT m r)+ withReason why m =+ do r <- ask+ lift $ withReason why (runReaderT m r)++instance (MonadPlus m, MonadSyntax atom m) => MonadSyntax atom (Strict.StateT s m) where+ anything = lift anything+ cut = lift cut+ progress = lift progress+ delimit m =+ do st <- get+ (s, st') <- lift $ delimit (Strict.runStateT m st)+ put st'+ return s+ call m =+ do st <- get+ (s, st') <- lift $ call (Strict.runStateT m st)+ put st'+ return s+ withFocus stx m =+ do st <- get+ (s, st') <- lift $ withFocus stx (Strict.runStateT m st)+ put st'+ return s+ withProgress p m =+ do st <- get+ (s, st') <- lift $ withProgress p (Strict.runStateT m st)+ put st'+ return s+ withReason why m =+ do st <- get+ (s, st') <- lift $ withReason why (Strict.runStateT m st)+ put st'+ return s++instance (MonadPlus m, MonadSyntax atom m) => MonadSyntax atom (Lazy.StateT s m) where+ anything = lift anything+ cut = lift cut+ progress = lift progress+ delimit m =+ do st <- get+ (s, st') <- lift $ delimit (Lazy.runStateT m st)+ put st'+ return s+ call m =+ do st <- get+ (s, st') <- lift $ call (Lazy.runStateT m st)+ put st'+ return s+ withFocus stx m =+ do st <- get+ (s, st') <- lift $ withFocus stx (Lazy.runStateT m st)+ put st'+ return s+ withProgress p m =+ do st <- get+ (s, st') <- lift $ withProgress p (Lazy.runStateT m st)+ put st'+ return s+ withReason why m =+ do st <- get+ (s, st') <- lift $ withReason why (Lazy.runStateT m st)+ put st'+ return s++instance (Monoid w, MonadSyntax atom m) => MonadSyntax atom (Strict.WriterT w m) where+ anything = lift anything+ cut = lift cut+ progress = lift progress+ delimit m =+ do (x, w) <- lift $ delimit $ Strict.runWriterT m+ tell w+ return x+ call m =+ do (x, w) <- lift $ call $ Strict.runWriterT m+ tell w+ return x+ withFocus stx m =+ do (x, w) <- lift $ withFocus stx $ Strict.runWriterT m+ tell w+ return x+ withProgress p m =+ do (x, w) <- lift $ withProgress p $ Strict.runWriterT m+ tell w+ return x+ withReason why m =+ do (x, w) <- lift $ withReason why $ Strict.runWriterT m+ tell w+ return x++instance (Monoid w, MonadSyntax atom m) => MonadSyntax atom (Lazy.WriterT w m) where+ anything = lift anything+ cut = lift cut+ progress = lift progress+ delimit m =+ do (x, w) <- lift $ delimit $ Lazy.runWriterT m+ tell w+ return x+ call m =+ do (x, w) <- lift $ call $ Lazy.runWriterT m+ tell w+ return x+ withFocus stx m =+ do (x, w) <- lift $ withFocus stx $ Lazy.runWriterT m+ tell w+ return x+ withProgress p m =+ do (x, w) <- lift $ withProgress p $ Lazy.runWriterT m+ tell w+ return x+ withReason why m =+ do (x, w) <- lift $ withReason why $ Lazy.runWriterT m+ tell w+ return x++-- | Strip location information from a syntax object+syntaxToDatum :: Syntactic expr atom => expr -> Datum atom+syntaxToDatum (A x) = Datum $ Atom x+syntaxToDatum (L ls) = Datum $ List $ map syntaxToDatum ls+syntaxToDatum _ = error "syntaxToDatum: impossible case - bad Syntactic instance"++-- | Succeed if and only if the focus satisfies a Boolean predicate.+satisfy :: MonadSyntax atom m => (Syntax atom -> Bool) -> m (Syntax atom)+satisfy p =+ do foc <- anything+ if p foc+ then pure foc+ else empty++-- | Succeed only if the focus, having been stripped of position+-- information, is structurally equal to some datum.+datum :: (MonadSyntax atom m, IsAtom atom, Eq atom) => Datum atom -> m ()+datum dat =+ describe (datumToText mempty dat) $+ satisfy (\stx -> dat == syntaxToDatum stx) *> pure ()++-- | Succeed if and only if the focus is some particular given atom.+atom :: (MonadSyntax atom m, IsAtom atom, Eq atom) => atom -> m ()+atom a = datum (Datum (Atom a))++-- | Succeed if and only if the focus is any atom, returning the atom.+atomic :: MonadSyntax atom m => m atom+atomic = sideCondition "an atom" perhapsAtom (syntaxToDatum <$> anything)+ where perhapsAtom (Datum (Atom a)) = Just a+ perhapsAtom _ = Nothing++-- | Annotate a parser with a description, documenting its role in the+-- grammar. These descriptions are used to construct error messages.+describe :: MonadSyntax atom m => Text -> m a -> m a+describe !d p =+ do foc <- anything+ withReason (Reason foc d) p++-- | Succeed if and only if the focus is the empty list.+emptyList :: MonadSyntax atom m => m ()+emptyList = describe (T.pack "empty expression ()") (satisfy (isNil . syntaxToDatum) *> pure ())+ where isNil (Datum (List [])) = True+ isNil _ = False++-- | Succeed if and only if the focus is a list, returning its contents.+anyList :: MonadSyntax atom m => m [Syntax atom]+anyList = sideCondition "zero or more expressions, in parentheses" isList anything+ where isList (Syntax (pos_val -> List xs)) = Just xs+ isList _ = Nothing++-- | If the current focus is a list, apply one parser to its head and+-- another to its tail.+cons :: MonadSyntax atom m => m a -> m b -> m (a, b)+cons a d = depCons a (\x -> d >>= \y -> pure (x, y))++-- | If the current focus is a list, apply one parser to its head and+-- another to its tail, ignoring the result of the head.+followedBy :: MonadSyntax atom m => m a -> m b -> m b+followedBy a d = depCons a (const d)++-- | Return the source position of the focus.+position :: MonadSyntax atom m => m Position+position = syntaxPos <$> anything++-- | Manually add a progress step to the current path through the+-- context. Use this to appropriately guard calls to 'parse'.+withProgressStep :: (MonadSyntax atom m) => ProgressStep -> m a -> m a+withProgressStep s = withProgress (pushProgress s)++-- | A dependent cons (see 'depcons') that can impose a validation+-- step on the head of a list focus. If the head fails the validation+-- (that is, the second action returns 'Left'), the error is reported+-- in the head position.+depConsCond :: MonadSyntax atom m => m a -> (a -> m (Either Text b)) -> m b+depConsCond a d =+ do focus <- anything+ case focus of+ L (e:es) ->+ do x <- withFocus e $ withProgressStep First $ a+ let cdr = Syntax (Posd (syntaxPos focus) (List es))+ res <- withFocus cdr $ withProgressStep Rest $ d x+ case res of+ Right answer -> return answer+ Left what -> withFocus e $ withProgressStep First $ later $ describe what empty+ _ -> empty++-- | Use the result of parsing the head of the current-focused list to+-- compute a parsing action to use for the tail of the list.+depCons :: MonadSyntax atom m => m a -> (a -> m b) -> m b+depCons a d =+ do focus <- anything+ case focus of+ L (e:es) ->+ do x <- withFocus e $ withProgressStep First $ a+ let cdr = Syntax (Posd (syntaxPos focus) (List es))+ withFocus cdr $ withProgressStep Rest $ d x+ _ -> empty++-- | Produce a parser that matches a list of things matched by another+-- parser.+rep :: MonadSyntax atom m => m a -> m [a]+rep p =+ do focus <- anything+ case focus of+ L [] ->+ pure []+ L (e:es) ->+ do x <- withFocus e $ withProgressStep First p+ let cdr = Syntax (Posd (syntaxPos focus) (List es))+ xs <- withFocus cdr $ withProgressStep Rest $ rep p+ pure (x : xs)+ _ -> empty++-- | Manually override the focus. Use this with care - it can lead to+-- bogus error selection unless 'withProgress' is used to provide an+-- appropriate path.+parse :: MonadSyntax atom m => Syntax atom -> m a -> m a+parse = withFocus++-- | Match a list focus elementwise.+list :: MonadSyntax atom m => [m a] -> m [a]+list parsers = describe desc $ list' parsers+ where desc =+ mappend (T.pack (show (length parsers))) (T.pack " expressions")+ list' ps =+ do focus <- anything+ case focus of+ L es -> go (syntaxPos focus) ps es+ _ -> empty++ go _ [] [] = pure []+ go _ (_:_) [] = empty+ go _ [] (_:_) = empty+ go loc (p:ps) (e:es) =+ do x <- withFocus e $ withProgressStep First p+ xs <- withFocus (Syntax (Posd loc (List es))) $+ withProgressStep Rest $+ list' ps+ pure (x : xs)++-- | Transform a parser such that its errors are considered to occur+-- after others, and thus be reported with a higher priority.+later :: MonadSyntax atom m => m a -> m a+later = withProgressStep Late++-- | Impose a side condition on a parser, failing with the given+-- description if the side condition is 'Nothing'.+sideCondition :: MonadSyntax atom m => Text -> (a -> Maybe b) -> m a -> m b+sideCondition !msg ok p =+ do x <- p+ case ok x of+ Just y -> pure y+ Nothing ->+ later $ describe msg empty++-- | Impose a Boolean side condition on a parser, failing with the+-- given description if the side condition is 'False'.+sideCondition' :: MonadSyntax atom m => Text -> (a -> Bool) -> m a -> m a+sideCondition' !msg ok p = sideCondition msg (\x -> if ok x then Just x else Nothing) p++-- | When the current focus is a list, reverse its contents while+-- invoking another parser. If it is not a list, fail.+backwards :: MonadSyntax atom m => m a -> m a+backwards p =+ do foc <- anything+ case foc of+ l@(L xs) -> withFocus (Syntax (Posd (syntaxPos l) (List (reverse xs)))) p+ _ -> empty++-- | Trivially succeed, but prevent backtracking.+commit :: MonadSyntax atom m => m ()+commit = pure () <|> cut
+ src/Lang/Crucible/Syntax/Overrides.hs view
@@ -0,0 +1,68 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeOperators #-}++module Lang.Crucible.Syntax.Overrides+ ( setupOverrides+ ) where++import Control.Lens hiding ((:>), Empty)+import Control.Monad.Except (runExceptT)+import Control.Monad.IO.Class+import System.IO++import Data.Parameterized.Context hiding (view)++import What4.Expr.Builder+import What4.ProgramLoc+import What4.Solver (LogData(..), defaultLogData)+import What4.Solver.Z3 (z3Adapter)++import Lang.Crucible.Backend+import qualified Lang.Crucible.Backend.Prove as CB+import Lang.Crucible.Types+import Lang.Crucible.FunctionHandle+import Lang.Crucible.Simulator+import qualified Lang.Crucible.Utils.Seconds as Sec+import qualified Lang.Crucible.Utils.Timeout as CTO+++setupOverrides ::+ (IsSymInterface sym, sym ~ (ExprBuilder t st fs)) =>+ sym -> HandleAllocator -> IO [(FnBinding p sym ext, Position)]+setupOverrides _ ha =+ do f1 <- FnBinding <$> mkHandle ha "proveObligations"+ <*> pure (UseOverride (mkOverride "proveObligations" proveObligations))++ return [(f1, InternalPos)]+++proveObligations :: (IsSymInterface sym, sym ~ (ExprBuilder t st fs)) =>+ OverrideSim p sym ext r EmptyCtx UnitType (RegValue sym UnitType)+proveObligations =+ ovrWithBackend $ \bak ->+ do let sym = backendGetSym bak+ h <- printHandle <$> getContext+ liftIO $ do+ hPutStrLn h "Attempting to prove all outstanding obligations!\n"++ let logData = defaultLogData { logCallbackVerbose = \_ -> hPutStrLn h+ , logReason = "assertion proof" }+ let timeout = CTO.Timeout (Sec.secondsFromInt 5)+ let prover = CB.offlineProver timeout sym logData z3Adapter+ let strat = CB.ProofStrategy prover CB.keepGoing+ let ppResult o =+ \case+ CB.Proved {} -> unlines ["Proof Succeeded!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]+ CB.Disproved {} -> unlines ["Proof failed!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]+ CB.Unknown {} -> unlines ["Proof inconclusive!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]+ let printer = CB.ProofConsumer $ \o r -> hPutStrLn h (ppResult o r)+ runExceptT (CB.proveCurrentObligations bak strat printer) >>=+ \case+ Left CTO.TimedOut -> hPutStrLn h "Proof timed out!"+ Right () -> pure ()++ clearProofObligations bak
+ src/Lang/Crucible/Syntax/Prog.hs view
@@ -0,0 +1,87 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++module Lang.Crucible.Syntax.Prog+ ( assertNoExterns+ , assertNoForwardDecs+ , doParseCheck+ ) where++import Control.Monad++import qualified Data.Map as Map+import Data.Map (Map)+import Data.Text (Text)+import qualified Data.Text.IO as T+import qualified Prettyprinter as PP+import System.IO+import System.Exit+import Text.Megaparsec as MP++import Data.Parameterized.Nonce+import Data.Parameterized.Some (Some(Some))++import qualified Lang.Crucible.CFG.Core as C+import Lang.Crucible.CFG.Extension (IsSyntaxExtension)+import Lang.Crucible.CFG.Reg+import Lang.Crucible.CFG.SSAConversion++import Lang.Crucible.Syntax.Concrete+import Lang.Crucible.Syntax.SExpr+import Lang.Crucible.Syntax.Atoms++import Lang.Crucible.Analysis.Postdom+import Lang.Crucible.FunctionHandle++import What4.FunctionName++assertNoExterns :: Map GlobalName (Some GlobalVar) -> IO ()+assertNoExterns externs =+ unless (Map.null externs) $+ do putStrLn "Externs not currently supported"+ exitFailure++assertNoForwardDecs :: Map FunctionName SomeHandle -> IO ()+assertNoForwardDecs fds =+ unless (Map.null fds) $+ do putStrLn "Forward declarations not currently supported"+ exitFailure++-- | The main loop body, useful for both the program and for testing.+doParseCheck+ :: (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext)+ => FilePath -- ^ The name of the input (appears in source locations)+ -> Text -- ^ The contents of the input+ -> Bool -- ^ Whether to pretty-print the input data as well+ -> Handle -- ^ A handle that will receive the output+ -> IO ()+doParseCheck fn theInput pprint outh =+ do Some ng <- newIONonceGenerator+ ha <- newHandleAllocator+ case MP.parse (skipWhitespace *> many (sexp atom) <* eof) fn theInput of+ Left err ->+ do putStrLn $ errorBundlePretty err+ exitFailure+ Right v ->+ do when pprint $+ forM_ v $+ \e -> T.hPutStrLn outh (printExpr e) >> hPutStrLn outh ""+ cs <- top ng ha [] $ prog v+ case cs of+ Left err -> hPutStrLn outh (show (PP.pretty err))+ Right (ParsedProgram{ parsedProgCFGs = ok+ , parsedProgExterns = externs+ , parsedProgForwardDecs = fds+ }) -> do+ assertNoExterns externs+ assertNoForwardDecs fds+ forM_ ok $+ \(AnyCFG theCfg) ->+ do C.SomeCFG ssa <- return $ toSSA theCfg+ hPutStrLn outh $ show $ cfgHandle theCfg+ hPutStrLn outh $ show $ C.ppCFG' True (postdomInfo ssa) ssa+
+ src/Lang/Crucible/Syntax/SExpr.hs view
@@ -0,0 +1,192 @@+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ViewPatterns #-}+module Lang.Crucible.Syntax.SExpr+ ( pattern A+ , pattern L+ , pattern (:::)+ , Syntax(..)+ , Datum(..)+ , Syntactic(..)+ , Parser+ , syntaxPos+ , withPosFrom+ , sexp+ , identifier+ , toText+ , datumToText+ , skipWhitespace+ , PrintRules(..)+ , PrintStyle(..)+ , Layer(..)+ , IsAtom(..)+ ) where++import Data.Char (isDigit, isLetter)+import Data.Text (Text)+import qualified Data.Text as T+import Data.Void+import What4.ProgramLoc as C++import Text.Megaparsec as MP+import Text.Megaparsec.Char+import qualified Text.Megaparsec.Char.Lexer as L+import qualified Prettyprinter as PP+import qualified Prettyprinter.Render.Text as PP (renderStrict)+++-- | Syntax objects, in which each layer is annotated with a source position.+newtype Syntax a = Syntax { unSyntax :: Posd (Layer Syntax a) }+ deriving (Show, Functor, Eq)++-- | Syntax objects divorced of their source-code context, without source positions.+newtype Datum a = Datum { unDatum :: Layer Datum a}+ deriving (Show, Functor, Eq)++-- | Extract the source position from a 'Syntax' object.+syntaxPos :: Syntax a -> Position+syntaxPos (Syntax (Posd p _)) = p++-- | Use the position from a syntax object around something else.+withPosFrom :: Syntax a -> b -> Posd b+withPosFrom stx x = Posd (syntaxPos stx) x++-- | Instances of 'Syntactic' support observations using the 'L' and 'A' patterns.+class Syntactic a b | a -> b where+ syntaxE :: a -> Layer Syntax b++instance Syntactic (Layer Syntax a) a where+ syntaxE = id+++instance Syntactic (Syntax a) a where+ syntaxE (Syntax (Posd _ e)) = e++-- | Match an atom from a syntactic structure+pattern A :: Syntactic a b => b -> a+pattern A x <- (syntaxE -> Atom x)++-- | Match a list from a syntactic structure+pattern L :: Syntactic a b => [Syntax b] -> a+pattern L xs <- (syntaxE -> List xs)++-- | Match the head and tail of a list-like structure+pattern (:::) :: Syntactic a b => Syntax b -> [Syntax b] -> a+pattern x ::: xs <- (syntaxE -> List (x : xs))++-- | The pattern functor for syntax, used both for 'Syntax' and+-- 'Datum'. In 'Syntax', it is composed with another structure that+-- adds source positions.+data Layer f a = List [f a] | Atom a+ deriving (Show, Functor, Eq)++-- | Convert any syntactic structure to its simplest description.+syntaxToDatum :: Syntactic expr atom => expr -> Datum atom+syntaxToDatum (A x) = Datum (Atom x)+syntaxToDatum (L xs) = Datum (List (map syntaxToDatum xs))+syntaxToDatum _ = error "impossible - bad Syntactic instance"++-- | A parser for s-expressions.+type Parser = Parsec Void Text++-- | Skip whitespace.+skipWhitespace :: Parser ()+skipWhitespace = L.space space1 lineComment blockComment+ where lineComment = L.skipLineComment ";"+ blockComment = L.skipBlockComment "#|" "|#"++-- | Skip the whitespace after a token.+lexeme :: Parser a -> Parser a+lexeme = L.lexeme skipWhitespace++-- | Parse something with its location.+withPos :: Parser a -> Parser (Posd a)+withPos p =+ do MP.SourcePos file line col <- getSourcePos+ let loc = C.SourcePos (T.pack file) (unPos line) (unPos col)+ res <- p+ return $ Posd loc res++-- | Parse a particular string.+symbol :: Text -> Parser Text+symbol = L.symbol skipWhitespace++-- | Parse a parenthesized list.+list :: Parser (Syntax a) -> Parser (Syntax a)+list p =+ do Posd loc _ <- withPos (symbol "(")+ xs <- many p+ _ <- lexeme $ symbol ")"+ return $ Syntax (Posd loc (List xs))++-- | Given a parser for atoms, parse an s-expression that contains them.+sexp :: Parser a -> Parser (Syntax a)+sexp atom =+ (Syntax . fmap Atom <$> lexeme (withPos atom)) <|>+ list (sexp atom)++-- | Parse an identifier.+identifier :: Parser Text+identifier = T.pack <$> identString+ where letterLike x = isLetter x || elem x ("<>=+-*/!_\\?" :: [Char])+ nameChar x = letterLike x || isDigit x || elem x ("$" :: [Char])+ identString = (:) <$> satisfy letterLike <*> many (satisfy nameChar)++-- | Styles of printing+data PrintStyle =+ -- | Special forms should treat the first n subforms as special, and+ -- the remaining as a body. For instance, for a Lisp-like+ -- let-expression, use 'Special 1' for indentation.+ Special Int++-- | Printing rules describe how to specially format expressions that+-- begin with particular atoms.+newtype PrintRules a = PrintRules (a -> Maybe PrintStyle)++instance Semigroup (PrintRules a) where+ PrintRules f <> PrintRules g = PrintRules $ \z -> f z <|> g z++instance Monoid (PrintRules a) where+ mempty = PrintRules $ const Nothing+++class IsAtom a where+ showAtom :: a -> Text++pprint :: (Syntactic expr a, IsAtom a) => PrintRules a -> expr -> PP.Doc ann+pprint rules expr = pprintDatum rules (syntaxToDatum expr)++pprintDatum :: IsAtom a => PrintRules a -> Datum a -> PP.Doc ann+pprintDatum rules@(PrintRules getLayout) stx =+ case unDatum stx of+ Atom at -> ppAtom at+ List lst ->+ PP.parens . PP.group $+ case lst of+ [] -> mempty+ [x] -> pprintDatum rules x+ ((unDatum -> Atom car) : xs) ->+ case getLayout car of+ Nothing -> ppAtom car <> PP.space <> PP.align (PP.vsep $ pprintDatum rules <$> xs)+ Just (Special i) ->+ let (special, rest) = splitAt i xs+ in PP.hang 2 $ PP.vsep $+ PP.group (PP.hang 2 $ PP.vsep $ ppAtom car : (map (pprintDatum rules) special)) :+ map (pprintDatum rules) rest+ xs -> PP.vsep $ pprintDatum rules <$> xs++ where ppAtom = PP.pretty . showAtom++-- | Render a syntactic structure to text, according to rules.+toText :: (Syntactic expr a, IsAtom a) => PrintRules a -> expr -> Text+toText rules stx = PP.renderStrict (PP.layoutSmart opts $ pprint rules stx)+ where opts = PP.LayoutOptions (PP.AvailablePerLine 80 0.8)++-- | Render a datum to text according to rules.+datumToText :: IsAtom a => PrintRules a -> Datum a -> Text+datumToText rules dat = PP.renderStrict (PP.layoutSmart opts $ pprintDatum rules dat)+ where opts = PP.LayoutOptions (PP.AvailablePerLine 80 0.8)
+ test/Tests.hs view
@@ -0,0 +1,199 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE RankNTypes #-}+module Main (main) where++import qualified Data.List as List+import Data.Text (Text)+import qualified Data.Text as T+import qualified Data.Text.IO as T++import System.IO++import Lang.Crucible.Syntax.Concrete (defaultParserHooks)+import Lang.Crucible.Syntax.ExprParse+import Lang.Crucible.Syntax.Monad+import Lang.Crucible.Syntax.Prog (doParseCheck)+import Lang.Crucible.Syntax.SExpr++import Test.Tasty (defaultMain, TestTree, testGroup)+import Test.Tasty.Golden+import Test.Tasty.HUnit+import qualified Text.Megaparsec as MP+import System.FilePath+import System.Directory++import What4.ProgramLoc (Position(SourcePos), Posd(..))++main :: IO ()+main = do wd <- getCurrentDirectory+ putStrLn $ "Looking for tests in " ++ wd+ parseTests <- findTests "Parsing round-trips" "test-data" testParser+ let allTests = testGroup "Tests" [syntaxParsing, parseTests]+ defaultMain allTests++findTests :: String -> FilePath -> (FilePath -> FilePath -> IO ()) -> IO TestTree+findTests group_name test_dir test_action =+ do inputs <- findByExtension [".cbl"] test_dir+ return $ testGroup group_name+ [ goldenFileTestCase input test_action+ | input <- List.sort inputs+ ]++goldenFileTestCase :: FilePath -> (FilePath -> FilePath -> IO ()) -> TestTree+goldenFileTestCase input test_action =+ goldenVsFileDiff+ (takeBaseName input) -- test name+ (\x y -> ["diff", "-u", x, y])+ goodFile -- golden file path+ outFile+ (test_action input outFile) -- action whose result is tested+ where+ outFile = replaceExtension input ".out"+ goodFile = replaceExtension input ".out.good"++testParser :: FilePath -> FilePath -> IO ()+testParser inFile outFile =+ do contents <- T.readFile inFile+ let ?parserHooks = defaultParserHooks+ withFile outFile WriteMode $ doParseCheck inFile contents True++data Lam = Lam [Text] (Datum TrivialAtom) deriving (Eq, Show)++syntaxParsing :: TestTree+syntaxParsing =+ let+ anyUnit :: SyntaxParse TrivialAtom ()+ anyUnit = anything *> pure ()+ vars :: SyntaxParse TrivialAtom [TrivialAtom]+ vars = describe "sequence of variable bindings" $ rep atomic+ distinctVars :: SyntaxParse TrivialAtom [TrivialAtom]+ distinctVars = sideCondition' "sequence of distinct variable bindings" (\xs -> List.nub xs == xs) vars+ lambda =+ fmap (\(_, (xs, (body, ()))) -> Lam [x | TrivialAtom x <- xs] (syntaxToDatum body))+ (cons (atom "lambda") $+ cons distinctVars $+ cons anything $ emptyList)+ in testGroup "Syntax parsing lib"+ [ testCase "Empty list is empty list" $+ do x <- syntaxTest "()" emptyList+ x @?= Right ()+ , testCase "Empty list is not atom" $+ do x <- syntaxTest "()" (atom ("foo" :: TrivialAtom))+ x @?= Left+ (SyntaxError $ pure $+ Reason { expr = Syntax {unSyntax = Posd {pos = fakeFilePos 1 1, pos_val = List []}}+ , message = "foo"+ })+ , testCase "Atom is not empty list" $+ do x <- syntaxTest "foo" emptyList+ x @?= Left+ (SyntaxError $ pure $+ Reason { expr = Syntax {unSyntax = Posd {pos = fakeFilePos 1 1, pos_val = Atom (TrivialAtom "foo")}}+ , message = "empty expression ()"+ })+ , testCase "Three element list of whatever" $+ do x <- syntaxTest "(delicious avocado toast)" (list [anyUnit, anyUnit, anyUnit])+ x @?= Right [(), (), ()]+ , testCase "Three element list of whatever, again" $+ do x <- syntaxTest "(delicious (avocado and tomato) toast)" (list [anyUnit, anyUnit, anyUnit])+ x @?= Right [(), (), ()]+ , testCase "Three element list of atoms" $+ do x <- syntaxTest "(delicious avocado toast)" (list [atomic, atomic, atomic])+ x @?= Right [TrivialAtom "delicious", TrivialAtom "avocado", TrivialAtom "toast"]+ , testCase "Three element list of non-atoms isn't atoms" $+ do x <- syntaxTest "((delicious) avocado toast)" (list [atomic, atomic, atomic])+ x @?= Left+ (SyntaxError $ pure $+ Reason { expr =+ Syntax $+ Posd { pos = fakeFilePos 1 2+ , pos_val =+ List [ Syntax (Posd (fakeFilePos 1 3)+ (Atom (TrivialAtom "delicious")))+ ]+ }+ , message = "an atom"+ })+ , testCase "Three element list of non-atoms still isn't atoms" $+ do x <- syntaxTest "(delicious (avocado) toast)" (list [atomic, atomic, atomic])+ x @?= Left+ (SyntaxError $ pure $+ Reason { expr =+ Syntax $+ Posd { pos = fakeFilePos 1 12+ , pos_val =+ List [ Syntax (Posd (fakeFilePos 1 13)+ (Atom (TrivialAtom "avocado")))+ ]+ }+ , message = "an atom"+ })+ , testCase "Many three-element lists of whatever (1)" $+ do x <- syntaxTest "((delicious avocado toast))" (rep $ list [anything, anything, anything] *> pure ())+ x @?= Right [()]+ , testCase "Many three-element lists of whatever (0)" $+ do x <- syntaxTest "()" (rep $ list [anything, anything, anything] *> pure ())+ x @?= Right []+ , testCase "Many three-element lists of whatever (4)" $+ do x <- syntaxTest "((programming is fun) (a b c) (x y z) (hello (more stuff) fits))" (rep $ list [anything, anything, anything] *> pure ())+ x @?= Right [(), (), (), ()]+ , testCase "Many three-element lists of whatever failing on third sublist" $+ do x <- syntaxTest "((programming is fun) (a b c) (x y) (hello (more stuff) fits))" (rep $ list [anything, anything, anything] *> pure ())+ x @?= Left+ (SyntaxError $ pure $+ Reason { expr = Syntax (Posd (fakeFilePos 1 31)+ (List [ Syntax (Posd (fakeFilePos 1 32)+ (Atom (TrivialAtom "x")))+ , Syntax (Posd (fakeFilePos 1 34)+ (Atom (TrivialAtom "y")))]))+ , message = "3 expressions"+ })+ , testCase "Realistic example 1" $+ do x <- syntaxTest "(lambda (x y z) y)" lambda+ x @?= Right (Lam ["x", "y", "z"] (Datum (Atom "y")))+ , testCase "Realistic example 2" $+ do x <- syntaxTest "(lambda (x y (z)) y)" lambda+ x @?= Left+ (SyntaxError $ pure $+ Reason { expr = Syntax (Posd (fakeFilePos 1 14)+ (List [Syntax {unSyntax = Posd {pos = fakeFilePos 1 15, pos_val = Atom (TrivialAtom "z")}}]))+ , message = "an atom"+ })+ , testCase "Realistic example 3" $+ do x <- syntaxTest "(lambda x x)" lambda+ x @?= Left+ (SyntaxError $ pure $+ Reason { expr = Syntax (Posd (fakeFilePos 1 9)+ (Atom "x"))+ , message = "sequence of variable bindings"+ })+ , testCase "Realistic example 4" $+ do x <- syntaxTest "(lambda (x y x) y)" lambda+ x @?= Left+ (SyntaxError $ pure $+ Reason { expr =+ Syntax (Posd (fakeFilePos 1 9)+ (List [ Syntax {unSyntax = Posd {pos = fakeFilePos 1 10, pos_val = Atom (TrivialAtom "x")}}+ , Syntax {unSyntax = Posd {pos = fakeFilePos 1 12, pos_val = Atom (TrivialAtom "y")}}+ , Syntax {unSyntax = Posd {pos = fakeFilePos 1 14, pos_val = Atom (TrivialAtom "x")}}+ ]))+ , message = "sequence of distinct variable bindings"+ })+ ]++fakeFile :: Text+fakeFile = "test input"++fakeFilePos :: Int -> Int -> Position+fakeFilePos = SourcePos fakeFile++syntaxTest :: Text -> SyntaxParse TrivialAtom a -> IO (Either (SyntaxError TrivialAtom) a)+syntaxTest txt p =+ case MP.parse (skipWhitespace *> sexp (TrivialAtom <$> identifier) <* MP.eof) (T.unpack fakeFile) txt of+ Left err -> error $ "Reader error: " ++ MP.errorBundlePretty err+ Right sexpr -> syntaxParseIO p sexpr+