Skip to content

Commit

Permalink
crucible-go: Adapt to recent Crux API changes (hooks)
Browse files Browse the repository at this point in the history
See #899. This was broken since f328d93.
  • Loading branch information
langston-barrett committed Nov 1, 2021
1 parent 7176af5 commit 6f70994
Showing 1 changed file with 32 additions and 22 deletions.
54 changes: 32 additions & 22 deletions crucible-go/tool/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ import Lang.Crucible.Simulator
-- crux
import qualified Crux
import qualified Crux.Config.Common as Crux
import qualified Crux.Types as Crux (CruxSimulationResult)

-- Go
import Language.Go.Parser
Expand All @@ -38,28 +39,37 @@ cruxGoConfig = Crux.Config
, Crux.cfgCmdLineFlag = []
}

simulateGo :: Crux.CruxOptions -> GoOptions -> Crux.SimulatorCallback msgs
simulateGo copts _opts = Crux.SimulatorCallback $ \sym _maybeOnline -> do
let files = Crux.inputFiles copts
let verbosity = Crux.simVerbose (Crux.outputOptions copts)
file <- case files of
[f] -> return f
_ -> fail "crux-go requires a single file name as an argument"

-- Load the file
json <- BS.readFile file
let fwi = either error id $ parseMain json

-- Initialize arguments to the function
let regmap = RegMap Ctx.Empty

-- Set up initial crucible execution state
initSt <- setupCrucibleGoCrux 32 fwi verbosity sym Crux.CruxPersonality regmap

-- TODO: add failure explanations
let explainFailure _evalFn _gl = return mempty

return (Crux.RunnableState initSt, explainFailure)
simulateGo ::
Crux.CruxOptions ->
GoOptions ->
Crux.SimulatorCallbacks msgs Crux.CruxSimulationResult
simulateGo copts _opts =
Crux.SimulatorCallbacks $
return $
Crux.SimulatorHooks
{ Crux.setupHook =
\sym _maybeOnline -> do
let files = Crux.inputFiles copts
let verbosity = Crux.simVerbose (Crux.outputOptions copts)
file <- case files of
[f] -> return f
_ -> fail "crux-go requires a single file name as an argument"

-- Load the file
json <- BS.readFile file
let fwi = either error id $ parseMain json

-- Initialize arguments to the function
let regmap = RegMap Ctx.Empty

-- Set up initial crucible execution state
Crux.RunnableState <$>
setupCrucibleGoCrux 32 fwi verbosity sym Crux.CruxPersonality regmap

-- TODO add failure explanations
, Crux.onErrorHook = \_sym -> return (\_ _ -> return mempty)
, Crux.resultHook = \_sym result -> return result
}


-- | Entry point, parse command line options
Expand Down

0 comments on commit 6f70994

Please sign in to comment.