Skip to content

Commit

Permalink
crucible-syntax: Share more code between CLI frontends
Browse files Browse the repository at this point in the history
  • Loading branch information
@langston-barrett
langston-barrett committed Nov 8, 2023
1 parent cff4513 commit de32bb5
Show file tree
Hide file tree
Showing 4 changed files with 94 additions and 155 deletions.
94 changes: 12 additions & 82 deletions crucible-llvm-syntax/app/Main.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,85 +7,47 @@
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 FilePath
file which = Opt.strArgument (Opt.metavar "FILE" <> Opt.help ("The " <> which <> " file"))

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 :: (?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 name)))
(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 name)))
(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 name)))
(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")))
where name = "exec-crucible-llvm"

profFile :: Opt.Parser ProfCmd
profFile =
Expand All @@ -95,13 +57,9 @@ 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 =
Expand All @@ -117,36 +75,8 @@ main =
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)

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
1 change: 1 addition & 0 deletions crucible-syntax/crucible-syntax.cabal
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,7 @@ library
executable crucibler
build-depends:
base >= 4.9 && < 4.19,
crucible,
crucible-syntax,
optparse-applicative,
text,
Expand Down
80 changes: 8 additions & 72 deletions crucible-syntax/crucible-syntax/Main.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,59 +2,24 @@
{-# 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
let ?parserHooks = defaultParserHooks
doParseCheck fn l True stdout
repl f

command :: Opt.Parser Command
command =
Opt.subparser $
Expand All @@ -78,46 +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
let ?parserHooks = defaultParserHooks
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)

execCommand (\_ -> emptyExtensionImpl) simulationHooks cmd
where info = Opt.info (command <**> Opt.helper) (Opt.fullDesc)
prefs = Opt.prefs $ Opt.showHelpOnError <> Opt.showHelpOnEmpty

simulationHooks =
defaultSimulateProgramHooks
{ setupOverridesHook = setupOverrides
Expand Down
74 changes: 73 additions & 1 deletion crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,13 @@ module Lang.Crucible.Syntax.Prog
, simulateProgram
, SimulateProgramHooks(..)
, defaultSimulateProgramHooks
, repl
-- * CLI helpers
, CheckCmd(..)
, SimCmd(..)
, ProfCmd(..)
, Command(..)
, execCommand
) where

import Control.Lens (view)
Expand Down Expand Up @@ -53,7 +60,7 @@ import What4.Expr (ExprBuilder, newExprBuilder, EmptyExprBuilderState(..))
import What4.FunctionName
import What4.ProgramLoc
import What4.SatResult
import What4.Solver (defaultLogData, runZ3InOverride)
import What4.Solver (defaultLogData, runZ3InOverride, z3Options)


-- | The main loop body, useful for both the program and for testing.
Expand Down Expand Up @@ -250,3 +257,68 @@ simulateProgram fn theInput outh profh opts hooks = do
let ?parserHooks = defaultParserHooks
let ext = const emptyExtensionImpl
simulateProgramWithExtension ext fn theInput outh profh opts hooks

repl ::
(IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) =>
FilePath ->
IO ()
repl f =
do putStr "> "
l <- T.getLine
doParseCheck f l True stdout
repl f

data CheckCmd
= CheckCmd { chkInFile :: FilePath
, chkOutFile :: Maybe FilePath
, chkPrettyPrint :: Bool
}

data SimCmd
= SimCmd { _simInFile :: FilePath
, _simOutFile :: Maybe FilePath
}

data ProfCmd
= ProfCmd { _profInFile :: FilePath
, _profOutFile :: FilePath
}

data Command
= CheckCommand CheckCmd
| SimulateCommand SimCmd
| ProfileCommand ProfCmd
| ReplCommand

execCommand ::
(IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) =>
(forall sym. IsSymInterface sym => sym -> ExtensionImpl () sym ext) ->
SimulateProgramHooks ext ->
Command ->
IO ()
execCommand ext simulationHooks =
\case
ReplCommand -> hSetBuffering stdout NoBuffering >> repl "stdin"

CheckCommand (CheckCmd inputFile out pp) ->
do contents <- T.readFile inputFile
case out of
Nothing ->
doParseCheck inputFile contents pp stdout
Just outputFile ->
withFile outputFile WriteMode (doParseCheck inputFile contents pp)

SimulateCommand (SimCmd inputFile out) ->
do contents <- T.readFile inputFile
case out of
Nothing -> sim inputFile contents stdout Nothing configOptions simulationHooks
Just outputFile ->
withFile outputFile WriteMode
(\outh -> sim inputFile contents outh Nothing configOptions simulationHooks)

ProfileCommand (ProfCmd inputFile outputFile) ->
do contents <- T.readFile inputFile
withFile outputFile WriteMode
(\outh -> sim inputFile contents stdout (Just outh) configOptions simulationHooks)
where configOptions = z3Options
sim = simulateProgramWithExtension ext

0 comments on commit de32bb5

Please sign in to comment.