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 (Program)
13import Language.QBE.Backend.DFS (PathSel, findUnexplored, newPathSel, trackTrace)
14import Language.QBE.Backend.Model (Model)
15import Language.QBE.Backend.Store qualified as ST
16import Language.QBE.Backend.Tracer qualified as T
17import Language.QBE.Simulator (execFunc)
18import Language.QBE.Simulator.Concolic.Expression qualified as CE
19import Language.QBE.Simulator.Concolic.State (run)
20import Language.QBE.Simulator.Default.Expression qualified as DE
21import Language.QBE.Types qualified as QBE
22import SimpleSMT qualified as SMT
23import System.IO (Handle)
24
25logic :: String
26logic = "QF_BV"
27
28defSolver :: IO SMT.Solver
29defSolver = do
30  -- l <- SMT.newLogger 0
31  s <- SMT.newSolver "bitwuzla" [] Nothing
32  SMT.setLogic s logic
33  return s
34
35logSolver :: Handle -> IO SMT.Solver
36logSolver handle = do
37  l <- SMT.newLoggerWithHandle handle 0
38  s <-
39    SMT.newSolverWithConfig
40      (SMT.defaultConfig "bitwuzla" [])
41        { SMT.solverLogger = SMT.smtSolverLogger l
42        }
43  SMT.setLogic s logic
44  return s
45
46------------------------------------------------------------------------
47
48data Engine
49  = Engine
50  { expSolver :: SMT.Solver,
51    expPathSel :: PathSel,
52    expStore :: ST.Store
53  }
54
55newEngine :: SMT.Solver -> IO Engine
56newEngine solver = Engine solver newPathSel <$> ST.empty
57
58findNext :: Engine -> T.ExecTrace -> IO (Maybe Model, Engine)
59findNext e@(Engine {expStore = store}) eTrace = do
60  let pathSel = trackTrace (expPathSel e) eTrace
61  symVars <- ST.sexprs store
62  (model, nextPathSel) <- findUnexplored (expSolver e) symVars pathSel
63
64  let ne = e {expPathSel = nextPathSel}
65  case model of
66    Nothing ->
67      pure (model, ne)
68    Just nm ->
69      ST.setModel store nm >> pure (Just nm, ne)
70
71------------------------------------------------------------------------
72
73traceFunc :: Program -> QBE.FuncDef -> [CE.Concolic DE.RegVal] -> IO T.ExecTrace
74traceFunc prog func params = run prog (execFunc func params)
75
76explore ::
77  Engine ->
78  Program ->
79  QBE.FuncDef ->
80  [(String, QBE.BaseType)] ->
81  IO [(ST.Assign, T.ExecTrace)]
82explore engine@Engine {expSolver = solver, expStore = store} prog entry params = do
83  varAssign <- ST.assign store
84  values <- mapM (uncurry (ST.getConcolic solver store)) params
85  eTrace <- traceFunc prog entry values
86
87  (model, nEngine) <- findNext engine eTrace
88  case model of
89    Nothing -> pure [(varAssign, eTrace)]
90    Just _m -> (:) (varAssign, eTrace) <$> explore nEngine prog entry params