diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,7 @@ +# 0.5 -- 2025-11-09 + +* Add `parsedProgramFnBindings` to a new module, + `Lang.Crucible.Syntax.ParsedProgram`. # 0.4.1 -- 2025-03-21 diff --git a/crucible-syntax.cabal b/crucible-syntax.cabal --- a/crucible-syntax.cabal +++ b/crucible-syntax.cabal @@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: crucible-syntax -Version: 0.4.1 +Version: 0.5.0.0 Author: Galois Inc. Maintainer: dtc@galois.com Build-type: Simple @@ -30,71 +30,91 @@ -- available here: -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html - -- Since GHC 8.10 or earlier: + -- Since GHC 9.6 or earlier: ghc-options: -Wall + -Werror=ambiguous-fields -Werror=compat-unqualified-imports -Werror=deferred-type-errors -Werror=deprecated-flags -Werror=deprecations -Werror=deriving-defaults + -Werror=deriving-typeable -Werror=dodgy-foreign-imports -Werror=duplicate-exports -Werror=empty-enumerations + -Werror=gadt-mono-local-binds -Werror=identities -Werror=inaccessible-code -Werror=incomplete-patterns -Werror=incomplete-record-updates -Werror=incomplete-uni-patterns -Werror=inline-rule-shadowing + -Werror=misplaced-pragmas -Werror=missed-extra-shared-lib -Werror=missing-exported-signatures -Werror=missing-fields -Werror=missing-home-modules -Werror=missing-methods + -Werror=missing-pattern-synonym-signatures + -Werror=missing-signatures + -Werror=name-shadowing + -Werror=noncanonical-monad-instances + -Werror=noncanonical-monoid-instances + -Werror=operator-whitespace + -Werror=operator-whitespace-ext-conflict + -Werror=orphans -Werror=overflowed-literals -Werror=overlapping-patterns -Werror=partial-fields -Werror=partial-type-signatures + -Werror=redundant-bang-patterns + -Werror=redundant-record-wildcards + -Werror=redundant-strictness-flags -Werror=simplifiable-class-constraints -Werror=star-binder -Werror=star-is-type -Werror=tabs + -Werror=type-defaults -Werror=typed-holes + -Werror=type-equality-out-of-scope + -Werror=type-equality-requires-operators + -Werror=unicode-bidirectional-format-characters -Werror=unrecognised-pragmas -Werror=unrecognised-warning-flags -Werror=unsupported-calling-conventions -Werror=unsupported-llvm-version - -Werror=unticked-promoted-constructors + -Werror=unused-do-bind -Werror=unused-imports + -Werror=unused-record-wildcards -Werror=warnings-deprecations -Werror=wrong-do-bind - if impl(ghc >= 9.2) + if impl(ghc < 9.8) ghc-options: - -Werror=ambiguous-fields - -Werror=operator-whitespace - -Werror=operator-whitespace-ext-conflict - -Werror=redundant-bang-patterns + -Werror=forall-identifier - if impl(ghc >= 9.4) + if impl(ghc >= 9.8) ghc-options: - -Werror=forall-identifier - -Werror=misplaced-pragmas - -Werror=redundant-strictness-flags - -Werror=type-equality-out-of-scope - -Werror=type-equality-requires-operators + -Werror=incomplete-export-warnings + -Werror=inconsistent-flags + if impl(ghc >= 9.10) + ghc-options: + -Werror=badly-staged-types + -Werror=data-kinds-tc + -Werror=deprecated-type-abstractions + -Werror=incomplete-record-selectors + ghc-prof-options: -O2 -fprof-auto-top default-language: Haskell2010 library - default-language: Haskell2010 - + import: shared build-depends: - base >= 4.9 && < 4.20, + base >= 4.9 && < 4.21, bv-sized >= 1.0.0, - containers, + containers >= 0.6.0.1, crucible >= 0.1, lens, mtl, @@ -115,6 +135,7 @@ Lang.Crucible.Syntax.Overrides Lang.Crucible.Syntax.ExprParse Lang.Crucible.Syntax.Monad + Lang.Crucible.Syntax.ParsedProgram Lang.Crucible.Syntax.Prog ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns diff --git a/src/Lang/Crucible/Syntax/Concrete.hs b/src/Lang/Crucible/Syntax/Concrete.hs --- a/src/Lang/Crucible/Syntax/Concrete.hs +++ b/src/Lang/Crucible/Syntax/Concrete.hs @@ -98,6 +98,7 @@ import What4.Symbol import What4.Utils.StringLiteral +import Lang.Crucible.Syntax.ParsedProgram (ParsedProgram(..)) import Lang.Crucible.Syntax.SExpr (Syntax, pattern L, pattern A, toText, PrintRules(..), PrintStyle(..), syntaxPos, withPosFrom, showAtom) import Lang.Crucible.Syntax.Atoms hiding (atom) @@ -211,23 +212,6 @@ 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)) @@ -593,7 +577,7 @@ 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 + Pair notRef _ -> later $ describe ("reference type (provided a " <> T.pack (show notRef) <> ")") empty globRef :: m (SomeExpr ext s) globRef = @@ -796,7 +780,7 @@ 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) + do let ty = MaybeRepr (ts ^. ixF' idx) return $ SomeE ty $ EApp $ ProjectVariant ts idx e _ -> describe ("variant type (got " <> T.pack (show t) <> ")") empty @@ -1044,7 +1028,7 @@ 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 + do let ty = ts ^. ixF' idx return $ SomeE ty $ EApp $ GetStruct e idx ty _ -> describe ("struct type (got " <> T.pack (show t) <> ")") empty))) @@ -1058,7 +1042,7 @@ 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 + 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)))) @@ -2090,11 +2074,14 @@ => 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 + case ast of + L (A (Kw Defun):_) -> Just <$> functionHeader ast + L (A (Kw Declare):_) -> declare ast $> Nothing + L (A (Kw DefGlobal):_) -> global ast $> Nothing + L (A (Kw Extern):_) -> extern ast $> Nothing + _ -> do + loc <- liftSyntaxParse position ast + throwError (TrivialErr loc) argTypes :: Ctx.Assignment Arg init -> Ctx.Assignment TypeRepr init argTypes = fmapFC (\(Arg _ _ t) -> t) diff --git a/src/Lang/Crucible/Syntax/ExprParse.hs b/src/Lang/Crucible/Syntax/ExprParse.hs --- a/src/Lang/Crucible/Syntax/ExprParse.hs +++ b/src/Lang/Crucible/Syntax/ExprParse.hs @@ -34,8 +34,9 @@ import Control.Monad.Reader (MonadReader(..), ReaderT(..)) import qualified Control.Monad.State.Strict as Strict +import Data.Containers.ListUtils (nubOrd) import Data.Foldable as Foldable -import Data.List +import qualified Data.List as List import qualified Data.List.NonEmpty as NE import Data.List.NonEmpty (NonEmpty(..)) import Data.String @@ -234,7 +235,7 @@ -- humans to read. printSyntaxError :: IsAtom atom => SyntaxError atom -> Text printSyntaxError (SyntaxError rs) = - T.intercalate "\n\tor\n" $ nub $ map printGroup $ groupReasons rs + T.intercalate "\n\tor\n" $ nubOrd $ map printGroup $ groupReasons rs where reasonPos (Reason found _) = syntaxPos found groupReasons reasons = @@ -244,7 +245,7 @@ printGroup (p, r@(Reason found _) :| more) = T.concat [ "At ", T.pack (show p) - , ", expected ", T.intercalate " or " (nub $ sort [ wanted | Reason _ wanted <- r:more ]) + , ", expected ", T.intercalate " or " (nubOrd $ List.sort [ wanted | Reason _ wanted <- r:more ]) , " but got ", toText mempty found] -- | Attempt to parse the given piece of syntax, returning the first success found, diff --git a/src/Lang/Crucible/Syntax/Overrides.hs b/src/Lang/Crucible/Syntax/Overrides.hs --- a/src/Lang/Crucible/Syntax/Overrides.hs +++ b/src/Lang/Crucible/Syntax/Overrides.hs @@ -1,3 +1,9 @@ +{-| +Module : Lang.Crucible.Syntax.Overrides + +A collection of overrides that are useful in testing and debugging Crucible. +-} + {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} @@ -9,9 +15,11 @@ ( setupOverrides ) where +import qualified Control.Lens as Lens import Control.Lens hiding ((:>), Empty) import Control.Monad.Except (runExceptT) import Control.Monad.IO.Class +import qualified Control.Monad.State.Strict as State import System.IO import Data.Parameterized.Context hiding (view) @@ -22,27 +30,38 @@ import What4.Solver.Z3 (z3Adapter) import Lang.Crucible.Backend +import qualified Lang.Crucible.Backend as CB import qualified Lang.Crucible.Backend.Prove as CB import Lang.Crucible.Types import Lang.Crucible.FunctionHandle import Lang.Crucible.Simulator +import qualified Lang.Crucible.Simulator as CS import qualified Lang.Crucible.Utils.Seconds as Sec import qualified Lang.Crucible.Utils.Timeout as CTO +import qualified Prettyprinter as PP +import qualified Prettyprinter.Render.Text as PP 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)] + ( IsSymBackend sym bak + , sym ~ ExprBuilder t st fs + ) => + bak -> + HandleAllocator -> + IO [(FnBinding p sym ext, Position)] +setupOverrides bak ha = + do let sym = backendGetSym bak + f1 <- FnBinding <$> mkHandle ha "proveObligations" + <*> pure (UseOverride (mkOverride "proveObligations" (proveObligations (Just sym)))) + f2 <- FnBinding <$> mkHandle ha "crucible-print-assumption-state" + <*> pure (UseOverride (mkOverride "crucible-print-assumption-state" (printAssumptionState (Just sym)))) + return [(f1, InternalPos), (f2, InternalPos)] proveObligations :: (IsSymInterface sym, sym ~ (ExprBuilder t st fs)) => + proxy sym -> OverrideSim p sym ext r EmptyCtx UnitType (RegValue sym UnitType) -proveObligations = +proveObligations _proxy = ovrWithBackend $ \bak -> do let sym = backendGetSym bak h <- printHandle <$> getContext @@ -56,9 +75,9 @@ 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] + 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 @@ -66,3 +85,16 @@ Right () -> pure () clearProofObligations bak + +printAssumptionState :: + IsSymInterface sym => + proxy sym -> + OverrideSim p sym ext r EmptyCtx UnitType (RegValue sym UnitType) +printAssumptionState _proxy = do + ctx <- State.gets (Lens.view stateContext) + let hdl = printHandle ctx + CS.ovrWithBackend $ \bak -> liftIO $ do + let render = PP.renderIO hdl . PP.layoutSmart PP.defaultLayoutOptions + let sym = CB.backendGetSym bak + state <- getBackendState bak + render (ppAssumptionState (Just sym) state) diff --git a/src/Lang/Crucible/Syntax/ParsedProgram.hs b/src/Lang/Crucible/Syntax/ParsedProgram.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Syntax/ParsedProgram.hs @@ -0,0 +1,46 @@ +module Lang.Crucible.Syntax.ParsedProgram + ( ParsedProgram(..) + , parsedProgramFnBindings + ) where + +import Data.Map.Strict (Map) +import Data.Parameterized.Some (Some) +import Lang.Crucible.Analysis.Postdom (postdomInfo) +import Lang.Crucible.CFG.Core (SomeCFG(SomeCFG), cfgHandle) +import Lang.Crucible.CFG.Extension (IsSyntaxExtension) +import Lang.Crucible.CFG.Generator (GlobalVar) +import Lang.Crucible.CFG.Reg (AnyCFG(AnyCFG)) +import Lang.Crucible.CFG.SSAConversion (toSSA) +import Lang.Crucible.FunctionHandle (SomeHandle) +import Lang.Crucible.Simulator (FnBinding (FnBinding)) +import Lang.Crucible.Simulator.ExecutionTree (FnState(UseCFG)) +import Lang.Crucible.Syntax.Atoms (GlobalName) +import What4.FunctionName (FunctionName) + +-- | 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'. + } + +-- | Create a 'FnBinding' for each @defun@ CFG in the 'ParsedProgram'. +parsedProgramFnBindings :: + IsSyntaxExtension ext => + ParsedProgram ext -> + [FnBinding p sym ext] +parsedProgramFnBindings prog = map mkBinding (parsedProgCFGs prog) + where + mkBinding (AnyCFG defCfg) = + case toSSA defCfg of + SomeCFG defSsa -> + FnBinding (cfgHandle defSsa) (UseCFG defSsa (postdomInfo defSsa)) diff --git a/src/Lang/Crucible/Syntax/SExpr.hs b/src/Lang/Crucible/Syntax/SExpr.hs --- a/src/Lang/Crucible/Syntax/SExpr.hs +++ b/src/Lang/Crucible/Syntax/SExpr.hs @@ -132,7 +132,7 @@ -- | Parse an identifier. identifier :: Parser Text identifier = T.pack <$> identString - where letterLike x = isLetter x || elem x ("<>=+-*/!_\\?" :: [Char]) + where letterLike x = isLetter x || elem x (".<>=+-*/!_\\?" :: [Char]) nameChar x = letterLike x || isDigit x || elem x ("$" :: [Char]) identString = (:) <$> satisfy letterLike <*> many (satisfy nameChar)