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