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  s <-
 66    SMT.newSolverWithConfig
 67      (SMT.defaultConfig "bitwuzla" [])
 68        { SMT.solverLogger = SMT.smtSolverLogger l
 69        }
 70  SMT.setLogic s logic
 71  return s
 72
 73------------------------------------------------------------------------
 74
 75data PathResult
 76  = PathResult
 77  { pathErr :: Maybe EvalError,
 78    pathTrace :: T.ExecTrace,
 79    pathVars :: ST.Assign
 80  }
 81  deriving (Show, Eq)
 82
 83initPath :: PathResult
 84initPath = PathResult Nothing [] Map.empty
 85
 86data Engine
 87  = Engine
 88  { expSolver :: SMT.Solver,
 89    expPathSel :: PathSel,
 90    expEnv :: Env,
 91    expLastPath :: PathResult
 92  }
 93
 94newEngine :: Env -> SMT.Solver -> Engine
 95newEngine env solver =
 96  Engine
 97    { expSolver = solver,
 98      expPathSel = newPathSel,
 99      expEnv = env,
100      expLastPath = initPath
101    }
102
103findNext :: [SMT.SExpr] -> T.ExecTrace -> StateT Engine IO (Maybe Model)
104findNext symVars eTrace = do
105  engine <- get
106
107  let pathSel = trackTrace (expPathSel engine) eTrace
108  (model, nextPathSel) <-
109    liftIO $ findUnexplored (expSolver engine) symVars pathSel
110
111  put $ engine {expPathSel = nextPathSel}
112  pure model
113
114-- TODO: Consider modelling changes of the PathSel (via findNext) and
115-- changes of the Store (via ST.finalize and ST.setModel) as a StateT.
116explorePath :: SimState a -> StateT Engine IO Bool
117explorePath simState = do
118  engine@(Engine {expEnv = env}) <- get
119  maybePath <- try $ run env
120  let (mayErr, eTrace, nStore) =
121        case maybePath of
122          Left (err :: ErrorPath) ->
123            let st = pathInput err
124             in (Just $ pathError err, errTracer st, errStore st)
125          Right (t, s) -> (Nothing, t, s)
126
127  -- Before finalizing the store, we can extract the variables we encountered
128  -- during this concrete execution, as well as the concrete values used for
129  -- these variables during the execution.
130  let inputVars = ST.sexprs nStore
131      varAssign = ST.cValues nStore
132  put $ engine {expLastPath = PathResult mayErr eTrace varAssign}
133
134  -- Finalize the store (declare new symbolic vars in solver) and then,
135  -- based on the new solver state, solve constraints to find a new input.
136  store <- liftIO $ ST.finalize (expSolver engine) nStore
137  model <- findNext inputVars eTrace
138  case model of
139    Nothing -> pure False
140    Just newModel -> do
141      let nEnv = env {envStore = ST.setModel store newModel}
142       in modify (\e -> e {expEnv = nEnv})
143      pure True
144  where
145    run env = lift $ evalStateT (unSimState $ runPath simState) env
146
147------------------------------------------------------------------------
148
149exploreFunc ::
150  Engine ->
151  QBE.FuncDef ->
152  [(String, QBE.ExtType)] ->
153  IO [PathResult]
154exploreFunc engine entry params = do
155  let funcState = mapM (uncurry makeConcolic) params >>= execFunc entry
156  evalStateT (exploreFunc' funcState) engine
157  where
158    exploreFunc' st = do
159      morePaths <- explorePath st
160      curEngine <- get
161
162      let ret = expLastPath curEngine
163       in if morePaths
164            then (ret :) <$> exploreFunc' st
165            else pure [ret]