crucible-syntax 0.4.1 → 0.5.0.0

raw patch · 7 files changed

+150/−59 lines, 7 filesdep ~basedep ~containersdep ~cruciblenew-uploaderPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, containers, crucible

API changes (from Hackage documentation)

Files

• CHANGELOG.md +4/−0
• crucible-syntax.cabal +39/−18
• src/Lang/Crucible/Syntax/Concrete.hs +13/−26
• src/Lang/Crucible/Syntax/ExprParse.hs +4/−3
• src/Lang/Crucible/Syntax/Overrides.hs +43/−11
• src/Lang/Crucible/Syntax/ParsedProgram.hs +46/−0
• src/Lang/Crucible/Syntax/SExpr.hs +1/−1

@@ -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 

@@ -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

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

@@ -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,

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

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

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