quebex

  1-- SPDX-FileCopyrightText: 2025-2026 Sören Tempel <soeren+git@soeren-tempel.net>
  2--
  3-- SPDX-License-Identifier: GPL-3.0-only
  4module Language.QBE.Simulator.Explorer
  5  ( defSolver,
  6    logSolver,
  7    PathResult (..),
  8    Engine (expLastPath),
  9    newEngine,
 10    explorePath,
 11    exploreFunc,
 12  )
 13where
 14
 15import Control.Applicative (empty, (<|>))
 16import Control.Monad.Catch (try)
 17import Control.Monad.IO.Class (liftIO)
 18import Control.Monad.State.Strict (StateT, evalStateT, get, lift, modify, put)
 19import Data.Map qualified as Map
 20import Language.QBE.Backend.DFS (PathSel, findUnexplored, newPathSel, trackTrace)
 21import Language.QBE.Backend.Model (Model)
 22import Language.QBE.Backend.Store qualified as ST
 23import Language.QBE.Backend.Tracer qualified as T
 24import Language.QBE.Simulator (execFunc)
 25import Language.QBE.Simulator.Concolic.State
 26  ( Env (envStore),
 27    ErrorPath (pathError, pathInput),
 28    ErrorState (errStore, errTracer),
 29    SimState (..),
 30    makeConcolic,
 31    runPath,
 32  )
 33import Language.QBE.Simulator.Error (EvalError)
 34import Language.QBE.Types qualified as QBE
 35import SimpleBV qualified as SMT
 36import System.Directory (findExecutable)
 37import System.IO (Handle)
 38
 39logic :: String
 40logic = "QF_BV"
 41
 42findSolver :: IO (String, [String])
 43findSolver =
 44  solver "bitwuzla" []
 45    <|> solver "z3" ["-smt2", "-in"]
 46    <|> solver "cvc5" ["--incremental"]
 47    <|> fail "no suitable sover found in PATH"
 48  where
 49    solver :: String -> [String] -> IO (String, [String])
 50    solver exec args = do
 51      r <- findExecutable exec
 52      maybe empty (\_ -> pure (exec, args)) r
 53
 54defSolver :: IO SMT.Solver
 55defSolver = do
 56  -- l <- SMT.newLogger 0
 57  (solver, args) <- findSolver
 58  s <- SMT.newSolver solver args Nothing
 59  SMT.setLogic s logic
 60  return s
 61
 62logSolver :: Handle -> IO SMT.Solver
 63logSolver handle = do
 64  l <- SMT.newLoggerWithHandle handle 0
 65  (solver, args) <- findSolver
 66  s <-
 67    SMT.newSolverWithConfig
 68      (SMT.defaultConfig solver args)
 69        { SMT.solverLogger = SMT.smtSolverLogger l
 70        }
 71  SMT.setLogic s logic
 72  return s
 73
 74------------------------------------------------------------------------
 75
 76data PathResult
 77  = PathResult
 78  { pathErr :: Maybe EvalError,
 79    pathTrace :: T.ExecTrace,
 80    pathVars :: ST.Assign
 81  }
 82  deriving (Show, Eq)
 83
 84initPath :: PathResult
 85initPath = PathResult Nothing [] Map.empty
 86
 87data Engine
 88  = Engine
 89  { expSolver :: SMT.Solver,
 90    expPathSel :: PathSel,
 91    expEnv :: Env,
 92    expLastPath :: PathResult
 93  }
 94
 95newEngine :: Env -> SMT.Solver -> Engine
 96newEngine env solver =
 97  Engine
 98    { expSolver = solver,
 99      expPathSel = newPathSel,
100      expEnv = env,
101      expLastPath = initPath
102    }
103
104findNext :: [SMT.SExpr] -> T.ExecTrace -> StateT Engine IO (Maybe Model)
105findNext symVars eTrace = do
106  engine <- get
107
108  let pathSel = trackTrace (expPathSel engine) eTrace
109  (model, nextPathSel) <-
110    liftIO $ findUnexplored (expSolver engine) symVars pathSel
111
112  put $ engine {expPathSel = nextPathSel}
113  pure model
114
115-- TODO: Consider modelling changes of the PathSel (via findNext) and
116-- changes of the Store (via ST.finalize and ST.setModel) as a StateT.
117explorePath :: SimState a -> StateT Engine IO Bool
118explorePath simState = do
119  engine@(Engine {expEnv = env}) <- get
120  maybePath <- try $ run env
121  let (mayErr, eTrace, nStore) =
122        case maybePath of
123          Left (err :: ErrorPath) ->
124            let st = pathInput err
125             in (Just $ pathError err, errTracer st, errStore st)
126          Right (t, s) -> (Nothing, t, s)
127
128  -- Before finalizing the store, we can extract the variables we encountered
129  -- during this concrete execution, as well as the concrete values used for
130  -- these variables during the execution.
131  let inputVars = ST.sexprs nStore
132      varAssign = ST.cValues nStore
133  put $ engine {expLastPath = PathResult mayErr eTrace varAssign}
134
135  -- Finalize the store (declare new symbolic vars in solver) and then,
136  -- based on the new solver state, solve constraints to find a new input.
137  store <- liftIO $ ST.finalize (expSolver engine) nStore
138  model <- findNext inputVars eTrace
139  case model of
140    Nothing -> pure False
141    Just newModel -> do
142      let nEnv = env {envStore = ST.setModel store newModel}
143       in modify (\e -> e {expEnv = nEnv})
144      pure True
145  where
146    run env = lift $ evalStateT (unSimState $ runPath simState) env
147
148------------------------------------------------------------------------
149
150exploreFunc ::
151  Engine ->
152  QBE.FuncDef ->
153  [(String, QBE.ExtType)] ->
154  IO [PathResult]
155exploreFunc engine entry params = do
156  let funcState = mapM (uncurry makeConcolic) params >>= execFunc entry
157  evalStateT (exploreFunc' funcState) engine
158  where
159    exploreFunc' st = do
160      morePaths <- explorePath st
161      curEngine <- get
162
163      let ret = expLastPath curEngine
164       in if morePaths
165            then (ret :) <$> exploreFunc' st
166            else pure [ret]