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.List (find)
 9import Data.Word (Word64)
10import Language.QBE (Program, globalFuncs, parse)
11import Language.QBE.Backend.Store qualified as ST
12import Language.QBE.Backend.Tracer qualified as ST
13import Language.QBE.Backend.Tracer qualified as T
14import Language.QBE.Simulator (execFunc)
15import Language.QBE.Simulator.Concolic.Expression qualified as CE
16import Language.QBE.Simulator.Concolic.State (mkEnv, run)
17import Language.QBE.Simulator.Default.Expression qualified as DE
18import Language.QBE.Simulator.Explorer (defSolver, explore, newEngine)
19import Language.QBE.Simulator.Expression qualified as E
20import Language.QBE.Simulator.Symbolic.Expression qualified as SE
21import Language.QBE.Types qualified as QBE
22import SimpleBV qualified as SMT
23
24parseProg :: String -> IO Program
25parseProg input =
26  case parse "" input of
27    Left e -> fail $ "Unexpected parsing error: " ++ show e
28    Right r -> pure r
29
30findFunc :: Program -> QBE.GlobalIdent -> QBE.FuncDef
31findFunc prog funcName =
32  case find (\f -> QBE.fName f == funcName) (globalFuncs prog) of
33    Just x -> x
34    Nothing -> error $ "Unknown function: " ++ show funcName
35
36-- TODO: Code duplication with quebex/test/Simulator.hs
37parseAndExec :: QBE.GlobalIdent -> [CE.Concolic DE.RegVal] -> String -> IO ST.ExecTrace
38parseAndExec funcName params input = do
39  prog <- parseProg input
40  let func = findFunc prog funcName
41  env <- mkEnv prog 0 128 Nothing
42  fst <$> run env (execFunc func params)
43
44unconstrained :: SMT.Solver -> Word64 -> String -> QBE.BaseType -> IO (CE.Concolic DE.RegVal)
45unconstrained solver initCon name ty = do
46  symbolic <- SMT.declareBV solver name $ QBE.baseTypeBitSize ty
47  let concrete = E.fromLit (QBE.Base ty) initCon
48  pure $ CE.Concolic concrete (Just $ SE.fromSExpr symbolic)
49
50explore' :: Program -> QBE.FuncDef -> [(String, QBE.BaseType)] -> IO [(ST.Assign, T.ExecTrace)]
51explore' prog entry params = do
52  engine <- newEngine <$> defSolver
53  defEnv <- mkEnv prog 0 128 Nothing
54  explore engine defEnv entry $
55    map (second QBE.Base) params