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

crucible-llvm-syntax/app/Main.hs

@@ -0,0 +1,151 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Main (main) where
+
+import Control.Monad.IO.Class (liftIO)
+import System.IO
+import qualified Data.Text.IO as T
+
+import Data.Parameterized.NatRepr (knownNat)
+
+import Lang.Crucible.Simulator.OverrideSim (writeGlobal)
+import Lang.Crucible.FunctionHandle (newHandleAllocator)
+
+import Lang.Crucible.Syntax.Concrete (ParserHooks)
+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.Extension (LLVM)
+import Lang.Crucible.LLVM.MemModel (defaultMemOptions, emptyMem, mkMemVar)
+
+import Lang.Crucible.LLVM.Syntax (emptyParserHooks, llvmParserHooks)
+
+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
+
+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 = file "input"
+
+output :: Opt.Parser TheFile
+output = file "output"
+
+repl :: (?parserHooks :: ParserHooks LLVM) => 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 $
+       (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 Check
+parseCheck =
+  Check <$> input <*> Opt.optional output <*> Opt.switch (Opt.help "Pretty-print the source file")
+
+configOptions :: [ConfigDesc]
+configOptions = z3Options
+
+
+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
+             }
+     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
+            let sim =
+                  simulateProgramWithExtension
+                    (\_ -> let ?recordLLVMAnnotation = \_ _ _ -> pure ()
+                           in llvmExtensionImpl defaultMemOptions)
+                    inputFile
+                    contents
+            case out of
+              Nothing ->
+                 sim stdout Nothing configOptions simulationHooks
+              Just (TheFile outputFile) ->
+                withFile outputFile WriteMode
+                  (\outh -> sim 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)
+
+  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/Main.hs

@@ -1,9 +1,11 @@
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ImplicitParams #-}
 module Main where
 
 import System.IO
 import qualified Data.Text.IO as T
 
+import Lang.Crucible.Syntax.Concrete (defaultParserHooks)
 import Lang.Crucible.Syntax.Prog
 import Lang.Crucible.Syntax.Overrides (setupOverrides)
 
@@ -49,6 +51,7 @@ repl :: TheFile -> IO ()
 repl f@(TheFile fn) =
   do putStr "> "
      l <- T.getLine
+     let ?parserHooks = defaultParserHooks
      doParseCheck fn l True stdout
      repl f
 
@@ -86,6 +89,7 @@ configOptions = z3Options
 main :: IO ()
 main =
   do cmd <- Opt.customExecParser prefs info
+     let ?parserHooks = defaultParserHooks
      case cmd of
        ReplCommand -> hSetBuffering stdout NoBuffering >> repl (TheFile "stdin")