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.List (find)
 8import Data.Word (Word64)
 9import Language.QBE (Program, globalFuncs, parse)
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 (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 SimpleSMT qualified as SMT
22
23parseProg :: String -> IO Program
24parseProg input =
25  case parse "" input of
26    Left e -> fail $ "Unexpected parsing error: " ++ show e
27    Right r -> pure r
28
29findFunc :: Program -> QBE.GlobalIdent -> QBE.FuncDef
30findFunc prog funcName =
31  case find (\f -> QBE.fName f == funcName) (globalFuncs prog) of
32    Just x -> x
33    Nothing -> error $ "Unknown function: " ++ show funcName
34
35-- TODO: Code duplication with quebex/test/Simulator.hs
36parseAndExec :: QBE.GlobalIdent -> [CE.Concolic DE.RegVal] -> String -> IO ST.ExecTrace
37parseAndExec funcName params input = do
38  prog <- parseProg input
39  let func = findFunc prog funcName
40  run prog (execFunc func params)
41
42unconstrained :: SMT.Solver -> Word64 -> String -> QBE.BaseType -> IO (CE.Concolic DE.RegVal)
43unconstrained solver initCon name ty = do
44  let concrete = E.fromLit ty initCon
45  symbolic <- SE.symbolic solver name ty
46  pure $ CE.Concolic concrete (Just symbolic)
47
48explore' :: Program -> QBE.FuncDef -> [(String, QBE.BaseType)] -> IO [(ST.Assign, T.ExecTrace)]
49explore' prog entry params = do
50  engine <- defSolver >>= newEngine
51  explore engine prog entry params