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 (explore, z3Solver) where
 5
 6import Language.QBE (Program)
 7import Language.QBE.Backend.DFS (PathSel, findUnexplored, newPathSel, trackTrace)
 8import Language.QBE.Backend.Model (Model)
 9import Language.QBE.Backend.Store qualified as ST
10import Language.QBE.Backend.Tracer qualified as T
11import Language.QBE.Simulator (execFunc)
12import Language.QBE.Simulator.Concolic.Expression qualified as CE
13import Language.QBE.Simulator.Concolic.State (run)
14import Language.QBE.Simulator.Default.Expression qualified as DE
15import Language.QBE.Types qualified as QBE
16import SimpleSMT qualified as SMT
17
18z3Solver :: IO SMT.Solver
19z3Solver = do
20  -- l <- SMT.newLogger 0
21  s <- SMT.newSolver "z3" ["-in", "-smt2"] Nothing
22  SMT.setLogic s "QF_BV"
23  return s
24
25------------------------------------------------------------------------
26
27data Engine
28  = Engine
29  { expSolver :: SMT.Solver,
30    expPathSel :: PathSel,
31    expStore :: ST.Store
32  }
33
34newEngine :: IO Engine
35newEngine = do
36  solver <- z3Solver -- TODO: Make this configurable
37  Engine solver newPathSel <$> ST.empty
38
39findNext :: Engine -> T.ExecTrace -> IO (Maybe Model, Engine)
40findNext e@(Engine {expStore = store}) eTrace = do
41  let pathSel = trackTrace (expPathSel e) eTrace
42  symVars <- ST.sexprs store
43  (model, nextPathSel) <- findUnexplored (expSolver e) symVars pathSel
44
45  let ne = e {expPathSel = nextPathSel}
46  case model of
47    Nothing ->
48      pure (model, ne)
49    Just nm ->
50      ST.setModel store nm >> pure (Just nm, ne)
51
52------------------------------------------------------------------------
53
54traceFunc :: Program -> QBE.FuncDef -> [CE.Concolic DE.RegVal] -> IO T.ExecTrace
55traceFunc prog func params = run prog (execFunc func params)
56
57explore :: Program -> QBE.FuncDef -> [(String, QBE.BaseType)] -> IO [(ST.Assign, T.ExecTrace)]
58explore prog entryPoint entryParams = newEngine >>= explore'
59  where
60    explore' :: Engine -> IO [(ST.Assign, T.ExecTrace)]
61    explore' engine@Engine {expSolver = solver, expStore = store} = do
62      varAssign <- ST.assign store
63      values <- mapM (uncurry (ST.getConcolic solver store)) entryParams
64      eTrace <- traceFunc prog entryPoint values
65
66      (model, nEngine) <- findNext engine eTrace
67      case model of
68        Nothing -> pure [(varAssign, eTrace)]
69        Just _m -> (:) (varAssign, eTrace) <$> explore' nEngine