quebex - Util.hs

 1-- SPDX-FileCopyrightText: 2025 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.Store qualified as ST
11import Language.QBE.Backend.Tracer qualified as ST
12import Language.QBE.Backend.Tracer qualified as T
13import Language.QBE.Simulator (execFunc)
14import Language.QBE.Simulator.Concolic.Expression qualified as CE
15import Language.QBE.Simulator.Concolic.State (mkEnv, run)
16import Language.QBE.Simulator.Default.Expression qualified as DE
17import Language.QBE.Simulator.Explorer (defSolver, explore, newEngine)
18import Language.QBE.Simulator.Expression qualified as E
19import Language.QBE.Simulator.Symbolic.Expression qualified as SE
20import Language.QBE.Types qualified as QBE
21import SimpleBV qualified as SMT
22
23parseAndExec :: QBE.GlobalIdent -> [CE.Concolic DE.RegVal] -> String -> IO ST.ExecTrace
24parseAndExec funcName params input = do
25  (prog, entry) <- parseAndFind funcName input
26
27  env <- mkEnv prog 0 128 Nothing
28  fst <$> run env (execFunc entry params)
29
30unconstrained :: SMT.Solver -> Word64 -> String -> QBE.BaseType -> IO (CE.Concolic DE.RegVal)
31unconstrained solver initCon name ty = do
32  let symbolic = SE.symbolic name (QBE.Base ty)
33  -- XXX: This is a hack, normally the Store does this for us.
34  _ <- SMT.declareBV solver name $ SE.bitSize symbolic
35
36  let concrete = E.fromLit (QBE.Base ty) initCon
37  pure $ CE.Concolic concrete (Just symbolic)
38
39explore' :: String -> String -> [(String, QBE.BaseType)] -> IO [(ST.Assign, T.ExecTrace)]
40explore' input funcName params = do
41  (prog, entry) <- parseAndFind (QBE.GlobalIdent funcName) input
42
43  engine <- newEngine <$> defSolver
44  defEnv <- mkEnv prog 0 128 Nothing
45  explore engine defEnv entry $
46    map (second QBE.Base) params