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.Tracer qualified as ST
11import Language.QBE.Simulator (execFunc)
12import Language.QBE.Simulator.Concolic.Expression qualified as CE
13import Language.QBE.Simulator.Concolic.State (run)
14import Language.QBE.Simulator.Default.Expression qualified as DE
15import Language.QBE.Simulator.Expression qualified as E
16import Language.QBE.Simulator.Symbolic.Expression qualified as SE
17import Language.QBE.Types qualified as QBE
18import SimpleSMT qualified as SMT
19
20parseProg :: String -> IO Program
21parseProg input =
22  case parse "" input of
23    Left e -> fail $ "Unexpected parsing error: " ++ show e
24    Right r -> pure r
25
26findFunc :: Program -> QBE.GlobalIdent -> QBE.FuncDef
27findFunc prog funcName =
28  case find (\f -> QBE.fName f == funcName) (globalFuncs prog) of
29    Just x -> x
30    Nothing -> error $ "Unknown function: " ++ show funcName
31
32-- TODO: Code duplication with quebex/test/Simulator.hs
33parseAndExec :: QBE.GlobalIdent -> [CE.Concolic DE.RegVal] -> String -> IO ST.ExecTrace
34parseAndExec funcName params input = do
35  prog <- parseProg input
36  let func = findFunc prog funcName
37  run prog (execFunc func params)
38
39unconstrained :: SMT.Solver -> Word64 -> String -> QBE.BaseType -> IO (CE.Concolic DE.RegVal)
40unconstrained solver initCon name ty = do
41  let concrete = E.fromLit ty initCon
42  symbolic <- SE.symbolic solver name ty
43  pure $ CE.Concolic concrete (Just symbolic)