quebex - Util.hs

 1-- SPDX-FileCopyrightText: 2025-2026 Sören Tempel <soeren+git@soeren-tempel.net>
 2--
 3-- SPDX-License-Identifier: GPL-3.0-only
 4
 5module Util where
 6
 7import Data.Bifunctor (second)
 8import Data.Word (Word64)
 9import Language.QBE (parseAndFind)
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 (mkEnv, run)
14import Language.QBE.Simulator.Default.Expression qualified as DE
15import Language.QBE.Simulator.Explorer (PathResult, defSolver, exploreFunc, newEngine)
16import Language.QBE.Simulator.Expression qualified as E
17import Language.QBE.Simulator.Symbolic.Expression qualified as SE
18import Language.QBE.Types qualified as QBE
19import SimpleBV qualified as SMT
20
21parseAndExec :: QBE.GlobalIdent -> [CE.Concolic DE.RegVal] -> String -> IO T.ExecTrace
22parseAndExec funcName params input = do
23  (prog, entry) <- parseAndFind funcName input
24
25  env <- mkEnv prog 0 128 Nothing
26  fst <$> run env (execFunc entry params)
27
28unconstrained :: SMT.Solver -> Word64 -> String -> QBE.BaseType -> IO (CE.Concolic DE.RegVal)
29unconstrained solver initCon name ty = do
30  let symbolic = SE.symbolic name (QBE.Base ty)
31  -- XXX: This is a hack, normally the Store does this for us.
32  _ <- SMT.declareBV solver name $ SE.bitSize symbolic
33
34  let concrete = E.fromLit (QBE.Base ty) initCon
35  pure $ CE.Concolic concrete (Just symbolic)
36
37explore' :: String -> String -> [(String, QBE.BaseType)] -> IO [PathResult]
38explore' input funcName params = do
39  (prog, entry) <- parseAndFind (QBE.GlobalIdent funcName) input
40
41  defEnv <- mkEnv prog 0 128 Nothing
42  engine <- newEngine defEnv <$> defSolver
43  exploreFunc engine entry $
44    map (second QBE.Base) params