qute

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