crucible{,-llvm}-syntax: Evaluating programs with syntax extensions

crucible-llvm-syntax/app/Main.hs

@@ -0,0 +1,82 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Main (main) where
+
+import Control.Monad.IO.Class (liftIO)
+
+import Data.Parameterized.NatRepr (knownNat)
+
+import Lang.Crucible.Simulator.OverrideSim (writeGlobal)
+import Lang.Crucible.FunctionHandle (newHandleAllocator)
+
+import Lang.Crucible.Syntax.Prog
+import Lang.Crucible.Syntax.Overrides (setupOverrides)
+
+import Lang.Crucible.LLVM (llvmExtensionImpl)
+import Lang.Crucible.LLVM.DataLayout (EndianForm(LittleEndian))
+import Lang.Crucible.LLVM.MemModel (defaultMemOptions, emptyMem, mkMemVar)
+
+import Lang.Crucible.LLVM.Syntax (emptyParserHooks, llvmParserHooks)
+
+import qualified Options.Applicative as Opt
+import           Options.Applicative ( (<**>) )
+
+file :: String -> Opt.Parser FilePath
+file which = Opt.strArgument (Opt.metavar "FILE" <> Opt.help ("The " <> which <> " file"))
+
+input :: Opt.Parser FilePath
+input = file "input"
+
+output :: Opt.Parser FilePath
+output = file "output"
+
+command :: Opt.Parser Command
+command =
+  Opt.subparser $
+       (Opt.command "check"
+        (Opt.info (CheckCommand <$> parseCheck)
+         (Opt.fullDesc <> Opt.progDesc "Check a file" <> Opt.header "crucibler")))
+    <> (Opt.command "simulate"
+        (Opt.info (SimulateCommand <$> simFile)
+         (Opt.fullDesc <> Opt.progDesc "Simulate a file" <> Opt.header "crucibler")))
+    <> (Opt.command "profile"
+        (Opt.info (ProfileCommand <$> profFile)
+         (Opt.fullDesc <> Opt.progDesc "Simulate a file, with profiling" <> Opt.header "crucibler")))
+    <> (Opt.command "repl"
+        (Opt.info (pure ReplCommand) (Opt.fullDesc <> Opt.progDesc "Open a REPL")))
+
+profFile :: Opt.Parser ProfCmd
+profFile =
+  ProfCmd <$> input <*> output
+
+simFile :: Opt.Parser SimCmd
+simFile =
+  SimCmd <$> input <*> Opt.optional output
+
+parseCheck :: Opt.Parser CheckCmd
+parseCheck =
+  CheckCmd <$> input <*> Opt.optional output <*> Opt.switch (Opt.help "Pretty-print the source file")
+
+main :: IO ()
+main =
+  do cmd <- Opt.customExecParser prefs info
+     ha <- newHandleAllocator
+     mvar <- mkMemVar "llvm_memory" ha
+     let ?ptrWidth = knownNat @64
+     let ?parserHooks = llvmParserHooks emptyParserHooks mvar
+     let simulationHooks =
+           defaultSimulateProgramHooks
+             { setupHook = \_sym _ha -> do
+                 mem <- liftIO (emptyMem LittleEndian)
+                 writeGlobal mvar mem
+             , setupOverridesHook = setupOverrides
+             }
+     let ext _ = let ?recordLLVMAnnotation = \_ _ _ -> pure ()
+                 in llvmExtensionImpl defaultMemOptions
+     execCommand ext simulationHooks cmd
+  where info = Opt.info (command <**> Opt.helper) (Opt.fullDesc)
+        prefs = Opt.prefs $ Opt.showHelpOnError <> Opt.showHelpOnEmpty

crucible-llvm-syntax/crucible-llvm-syntax.cabal

@@ -126,3 +126,19 @@ test-suite crucible-llvm-syntax-tests
     tasty,
     tasty-golden,
     text,
+    what4
+
+executable exec-crucible-llvm
+  import: shared
+  hs-source-dirs: app
+  main-is: Main.hs
+  build-depends:
+    base >= 4.13,
+    crucible,
+    crucible-syntax,
+    crucible-llvm,
+    crucible-llvm-syntax,
+    optparse-applicative,
+    parameterized-utils,
+    text,
+    what4

crucible-llvm-syntax/test-data/ptr.out.good → crucible-llvm-syntax/test-data/parse/ptr.out.good

@@ -52,7 +52,7 @@ test-ptr
   % 12:13
   $11 = bVLit(64, BV 1)
   % 13:12
-  $12 = alloca crucible-llvm-syntax-test-memory $11 Alignment 0 test-data/ptr.cbl:13:12
+  $12 = alloca crucible-llvm-syntax-test-memory $11 Alignment 0 test-data/parse/ptr.cbl:13:12
   % 15:16
   $13 = bVLit(8, BV 255)
   % 16:13

crucible-llvm-syntax/test-data/simulate/ptr.cbl

@@ -0,0 +1,24 @@
+(defun @main () Unit
+  (start start:
+    (let blk0 (the Nat 0))
+    (let off0 (bv 64 0))
+    (let p0 (ptr 64 blk0 off0))
+    (let p (ptr-ite 64 #t p0 p0))
+    (let blk (ptr-block 64 p))
+    (let off (ptr-offset 64 p))
+    (assert! (equal? blk0 blk) "block numbers equal")
+    (assert! (equal? off0 off) "offsets equal")
+
+    (let sz (bv 64 1))
+    (let a (alloca none sz))
+    (let vblk0 (the Nat 0))
+    (let voff0 (bv 8 255))
+    (let v0 (ptr 8 vblk0 voff0))
+    (store none i8 a v0)
+    (let v (load none i8 a))
+    (let vblk (ptr-block 8 v))
+    (let voff (ptr-offset 8 v))
+    (assert! (equal? vblk0 vblk) "stored block numbers equal")
+    (assert! (equal? voff0 voff) "stored offsets equal")
+
+    (return ())))

crucible-llvm-syntax/test-data/simulate/ptr.out.good

@@ -0,0 +1,4 @@
+==== Begin Simulation ====
+
+==== Finish Simulation ====
+==== No proof obligations ====

crucible-llvm-syntax/test/Test.hs

@@ -6,6 +6,7 @@
 
 module Main (main) where
 
+import Control.Monad.IO.Class (liftIO)
 import Data.List (sort)
 import Data.Text.IO qualified as T
 import System.FilePath
@@ -16,21 +17,27 @@ import Test.Tasty.Golden
 
 import Data.Parameterized.NatRepr (knownNat)
 
+import What4.Solver.Z3 (z3Options)
+
+import Lang.Crucible.Simulator.OverrideSim (writeGlobal)
 import Lang.Crucible.FunctionHandle (newHandleAllocator)
 
+import Lang.Crucible.LLVM (llvmExtensionImpl)
+import Lang.Crucible.LLVM.DataLayout (EndianForm(LittleEndian))
 import Lang.Crucible.LLVM.Extension (LLVM)
-import Lang.Crucible.LLVM.MemModel (mkMemVar)
+import Lang.Crucible.LLVM.MemModel (defaultMemOptions, emptyMem, mkMemVar)
 
 import Lang.Crucible.Syntax.Concrete (ParserHooks)
-import Lang.Crucible.Syntax.Prog (doParseCheck)
+import Lang.Crucible.Syntax.Prog (SimulateProgramHooks(setupHook), defaultSimulateProgramHooks, doParseCheck, simulateProgramWithExtension)
 
-import Lang.Crucible.LLVM.Syntax (llvmParserHooks)
+import Lang.Crucible.LLVM.Syntax (emptyParserHooks, llvmParserHooks)
 import Lang.Crucible.LLVM.Syntax.TypeAlias (typeAliasParserHooks, x86_64LinuxTypes)
 
 main :: IO ()
 main = do
-  parseTests <- findTests "Parse tests" "test-data" testParser
-  defaultMain $ testGroup "Tests" [parseTests]
+  parseTests <- findTests "Parse tests" "test-data/parse" testParser
+  simTests <- findTests "LLVM simulation" "test-data/simulate" testSimulator
+  defaultMain $ testGroup "Tests" [parseTests, simTests]
 
 findTests :: String -> FilePath -> (FilePath -> FilePath -> IO ()) -> IO TestTree
 findTests groupName testDir testAction =
@@ -67,3 +74,22 @@ testParser inFile outFile =
      let ?parserHooks = hooks
      withFile outFile WriteMode $ doParseCheck inFile contents True
 
+testSimulator :: FilePath -> FilePath -> IO ()
+testSimulator inFile outFile =
+  do contents <- T.readFile inFile
+     ha <- newHandleAllocator
+     mvar <- mkMemVar "llvm_memory" ha
+     let ?ptrWidth = knownNat @64
+     let ?parserHooks = llvmParserHooks emptyParserHooks mvar
+     withFile outFile WriteMode $ \outh -> do
+       let ext _ =
+             let ?recordLLVMAnnotation = \_ _ _ -> pure ()
+             in llvmExtensionImpl defaultMemOptions
+       simulateProgramWithExtension ext inFile contents outh Nothing z3Options $
+         defaultSimulateProgramHooks
+           { setupHook = \_sym _ha -> do
+               mem <- liftIO (emptyMem LittleEndian)
+               writeGlobal mvar mem
+           }
+
+

crucible-syntax/crucible-syntax.cabal

@@ -47,6 +47,7 @@ library
 executable crucibler
   build-depends:
     base >= 4.9 && < 4.19,
+    crucible,
     crucible-syntax,
     optparse-applicative,
     text,

crucible-syntax/crucible-syntax/Main.hs

@@ -1,57 +1,25 @@
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ImplicitParams #-}
 module Main where
 
-import System.IO
-import qualified Data.Text.IO as T
+import Lang.Crucible.Simulator.ExecutionTree (emptyExtensionImpl)
 
+import Lang.Crucible.Syntax.Concrete (defaultParserHooks)
 import Lang.Crucible.Syntax.Prog
 import Lang.Crucible.Syntax.Overrides (setupOverrides)
 
-import What4.Config
-import What4.Solver.Z3 ( z3Options )
-
 import qualified Options.Applicative as Opt
 import           Options.Applicative ( (<**>) )
 
-data Check = Check { chkInFile :: TheFile
-                   , chkOutFile :: Maybe TheFile
-                   , chkPrettyPrint :: Bool
-                   }
-
-data SimCmd = SimCmd { simInFile :: TheFile
-                     , simOutFile :: Maybe TheFile
-                     }
-
-data ProfCmd =
-  ProfCmd { profInFile :: TheFile
-          , profOutFile :: TheFile
-          }
-
-data Command = CheckCommand Check
-             | SimulateCommand SimCmd
-             | ProfileCommand ProfCmd
-             | ReplCommand
+file :: String -> Opt.Parser FilePath
+file which = Opt.strArgument (Opt.metavar "FILE" <> Opt.help ("The " <> which <> " file"))
 
-newtype TheFile = TheFile FilePath
-  deriving (Eq, Show, Ord)
-
-
-file :: String -> Opt.Parser TheFile
-file which = TheFile <$> Opt.strArgument (Opt.metavar "FILE" <> Opt.help ("The " <> which <> " file"))
-
-input :: Opt.Parser TheFile
+input :: Opt.Parser FilePath
 input = file "input"
 
-output :: Opt.Parser TheFile
+output :: Opt.Parser FilePath
 output = file "output"
 
-repl :: TheFile -> IO ()
-repl f@(TheFile fn) =
-  do putStr "> "
-     l <- T.getLine
-     doParseCheck fn l True stdout
-     repl f
-
 command :: Opt.Parser Command
 command =
   Opt.subparser $
@@ -75,45 +43,17 @@ simFile :: Opt.Parser SimCmd
 simFile =
   SimCmd <$> input <*> Opt.optional output
 
-parseCheck :: Opt.Parser Check
+parseCheck :: Opt.Parser CheckCmd
 parseCheck =
-  Check <$> input <*> Opt.optional output <*> Opt.switch (Opt.help "Pretty-print the source file")
-
-configOptions :: [ConfigDesc]
-configOptions = z3Options
-
+  CheckCmd <$> input <*> Opt.optional output <*> Opt.switch (Opt.help "Pretty-print the source file")
 
 main :: IO ()
 main =
   do cmd <- Opt.customExecParser prefs info
-     case cmd of
-       ReplCommand -> hSetBuffering stdout NoBuffering >> repl (TheFile "stdin")
-
-       CheckCommand (Check (TheFile inputFile) out pp) ->
-         do contents <- T.readFile inputFile
-            case out of
-              Nothing ->
-                doParseCheck inputFile contents pp stdout
-              Just (TheFile outputFile) ->
-                withFile outputFile WriteMode (doParseCheck inputFile contents pp)
-
-       SimulateCommand (SimCmd (TheFile inputFile) out) ->
-         do contents <- T.readFile inputFile
-            case out of
-              Nothing ->
-                simulateProgram inputFile contents stdout Nothing configOptions simulationHooks
-              Just (TheFile outputFile) ->
-                withFile outputFile WriteMode
-                  (\outh -> simulateProgram inputFile contents outh Nothing configOptions simulationHooks)
-
-       ProfileCommand (ProfCmd (TheFile inputFile) (TheFile outputFile)) ->
-         do contents <- T.readFile inputFile
-            withFile outputFile WriteMode
-               (\outh -> simulateProgram inputFile contents stdout (Just outh) configOptions simulationHooks)
-
+     let ?parserHooks = defaultParserHooks
+     execCommand (\_ -> emptyExtensionImpl) simulationHooks cmd
   where info = Opt.info (command <**> Opt.helper) (Opt.fullDesc)
         prefs = Opt.prefs $ Opt.showHelpOnError <> Opt.showHelpOnEmpty
-
         simulationHooks =
           defaultSimulateProgramHooks
             { setupOverridesHook = setupOverrides