quebex

 1-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
 2--
 3-- SPDX-License-Identifier: GPL-3.0-only
 4module Language.QBE.Simulator.Explorer
 5  ( newEngine,
 6    explore,
 7    defSolver,
 8    logSolver,
 9  )
10where
11
12import Language.QBE.Backend.DFS (PathSel, findUnexplored, newPathSel, trackTrace)
13import Language.QBE.Backend.Model (Model)
14import Language.QBE.Backend.Store qualified as ST
15import Language.QBE.Backend.Tracer qualified as T
16import Language.QBE.Simulator (execFunc)
17import Language.QBE.Simulator.Concolic.State (Env (envStore), makeConcolic, run)
18import Language.QBE.Types qualified as QBE
19import SimpleBV qualified as SMT
20import System.IO (Handle)
21
22logic :: String
23logic = "QF_BV"
24
25defSolver :: IO SMT.Solver
26defSolver = do
27  -- l <- SMT.newLogger 0
28  s <- SMT.newSolver "bitwuzla" [] Nothing
29  SMT.setLogic s logic
30  return s
31
32logSolver :: Handle -> IO SMT.Solver
33logSolver handle = do
34  l <- SMT.newLoggerWithHandle handle 0
35  s <-
36    SMT.newSolverWithConfig
37      (SMT.defaultConfig "bitwuzla" [])
38        { SMT.solverLogger = SMT.smtSolverLogger l
39        }
40  SMT.setLogic s logic
41  return s
42
43------------------------------------------------------------------------
44
45data Engine
46  = Engine
47  { expSolver :: SMT.Solver,
48    expPathSel :: PathSel
49  }
50
51newEngine :: SMT.Solver -> Engine
52newEngine solver = Engine solver newPathSel
53
54findNext :: Engine -> [SMT.SExpr] -> T.ExecTrace -> IO (Maybe Model, Engine)
55findNext e symVars eTrace = do
56  let pathSel = trackTrace (expPathSel e) eTrace
57  (model, nextPathSel) <- findUnexplored (expSolver e) symVars pathSel
58
59  let ne = e {expPathSel = nextPathSel}
60  case model of
61    Nothing ->
62      pure (model, ne)
63    Just nm ->
64      pure (Just nm, ne)
65
66explore ::
67  Engine ->
68  Env ->
69  QBE.FuncDef ->
70  [(String, QBE.ExtType)] ->
71  IO [(ST.Assign, T.ExecTrace)]
72explore engine@(Engine {expSolver = solver}) env entry params = do
73  (eTrace, nStore) <- run env (mapM (uncurry makeConcolic) params >>= execFunc entry)
74
75  -- Before finalizing the store, we can extract the variables we encountered
76  -- during this concrete execution, as well as the concrete values used for
77  -- these variables during the execution.
78  let inputVars = ST.sexprs nStore
79      varAssign = ST.cValues nStore
80  finalStore <- ST.finalize solver nStore
81
82  (model, nEngine) <- findNext engine inputVars eTrace
83  case model of
84    Nothing -> pure [(varAssign, eTrace)]
85    Just newModel -> do
86      let nEnv = env {envStore = ST.setModel finalStore newModel}
87      (:) (varAssign, eTrace) <$> explore nEngine nEnv entry params