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    Engine (expPathVars, expPathTrace),
  8    newEngine,
  9    explorePath,
 10    exploreFunc,
 11  )
 12where
 13
 14import Control.Monad.IO.Class (liftIO)
 15import Control.Monad.State (StateT, evalStateT, get, lift, modify, put)
 16import Data.Map qualified as Map
 17import Language.QBE.Backend.DFS (PathSel, findUnexplored, newPathSel, trackTrace)
 18import Language.QBE.Backend.Model (Model)
 19import Language.QBE.Backend.Store qualified as ST
 20import Language.QBE.Backend.Tracer qualified as T
 21import Language.QBE.Simulator (execFunc)
 22import Language.QBE.Simulator.Concolic.State (Env (envStore), makeConcolic, runPath)
 23import Language.QBE.Types qualified as QBE
 24import SimpleBV qualified as SMT
 25import System.IO (Handle)
 26
 27logic :: String
 28logic = "QF_BV"
 29
 30defSolver :: IO SMT.Solver
 31defSolver = do
 32  -- l <- SMT.newLogger 0
 33  s <- SMT.newSolver "bitwuzla" [] Nothing
 34  SMT.setLogic s logic
 35  return s
 36
 37logSolver :: Handle -> IO SMT.Solver
 38logSolver handle = do
 39  l <- SMT.newLoggerWithHandle handle 0
 40  s <-
 41    SMT.newSolverWithConfig
 42      (SMT.defaultConfig "bitwuzla" [])
 43        { SMT.solverLogger = SMT.smtSolverLogger l
 44        }
 45  SMT.setLogic s logic
 46  return s
 47
 48------------------------------------------------------------------------
 49
 50data Engine
 51  = Engine
 52  { expSolver :: SMT.Solver,
 53    expPathSel :: PathSel,
 54    expEnv :: Env,
 55    expPathVars :: ST.Assign,
 56    expPathTrace :: T.ExecTrace
 57  }
 58
 59newEngine :: Env -> SMT.Solver -> Engine
 60newEngine env solver =
 61  Engine
 62    { expSolver = solver,
 63      expPathSel = newPathSel,
 64      expEnv = env,
 65      expPathVars = Map.empty,
 66      expPathTrace = []
 67    }
 68
 69findNext :: [SMT.SExpr] -> T.ExecTrace -> StateT Engine IO (Maybe Model)
 70findNext symVars eTrace = do
 71  engine <- get
 72
 73  let pathSel = trackTrace (expPathSel engine) eTrace
 74  (model, nextPathSel) <-
 75    liftIO $ findUnexplored (expSolver engine) symVars pathSel
 76
 77  put $ engine {expPathSel = nextPathSel}
 78  pure model
 79
 80-- TODO: Consider modelling changes of the PathSel (via findNext) and
 81-- changes of the Store (via ST.finalize and ST.setModel) as a StateT.
 82explorePath :: StateT Env IO a -> StateT Engine IO Bool
 83explorePath simState = do
 84  engine@(Engine {expEnv = env}) <- get
 85  (eTrace, nStore) <- lift $ evalStateT (runPath simState) env
 86
 87  -- Before finalizing the store, we can extract the variables we encountered
 88  -- during this concrete execution, as well as the concrete values used for
 89  -- these variables during the execution.
 90  let inputVars = ST.sexprs nStore
 91      varAssign = ST.cValues nStore
 92  put $ engine {expPathVars = varAssign, expPathTrace = eTrace}
 93
 94  -- Finalize the store (declare new symbolic vars in solver) and then,
 95  -- based on the new solver state, solve constraints to find a new input.
 96  store <- liftIO $ ST.finalize (expSolver engine) nStore
 97  model <- findNext inputVars eTrace
 98  case model of
 99    Nothing -> pure False
100    Just newModel -> do
101      let nEnv = env {envStore = ST.setModel store newModel}
102       in modify (\e -> e {expEnv = nEnv})
103      pure True
104
105------------------------------------------------------------------------
106
107exploreFunc ::
108  Engine ->
109  QBE.FuncDef ->
110  [(String, QBE.ExtType)] ->
111  IO [(ST.Assign, T.ExecTrace)]
112exploreFunc engine entry params = do
113  let funcState = mapM (uncurry makeConcolic) params >>= execFunc entry
114  evalStateT (exploreFunc' funcState) engine
115  where
116    exploreFunc' st = do
117      morePaths <- explorePath st
118      curEngine <- get
119      let ret = (expPathVars curEngine, expPathTrace curEngine)
120       in if morePaths
121            then (ret :) <$> exploreFunc' st
122            else pure [ret]