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 Control.Monad.State (gets)
 8import Data.List (find)
 9import Data.Word (Word64)
10import Language.QBE (Program, globalFuncs, parse)
11import Language.QBE.Simulator (execFunc, runExec)
12import Language.QBE.Simulator.Concolic.Expression qualified as CE
13import Language.QBE.Simulator.Expression qualified as E
14import Language.QBE.Simulator.State (envTracer)
15import Language.QBE.Simulator.Symbolic.Expression qualified as SE
16import Language.QBE.Simulator.Symbolic.Tracer qualified as ST
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] -> String -> IO ST.ExecTrace
34parseAndExec funcName params input = do
35  prog <- parseProg input
36  let func = findFunc prog funcName
37
38  sTrace <- runExec prog (execFunc func params >> gets envTracer) ST.newExecTrace
39  case sTrace of
40    Left e -> fail $ "Unexpected evaluation error: " ++ show e
41    Right r -> pure r
42
43unconstrained :: SMT.Solver -> Word64 -> String -> QBE.BaseType -> IO CE.Concolic
44unconstrained solver initCon name ty = do
45  let concrete = E.fromLit ty initCon
46  symbolic <- SE.symbolic solver name ty
47  pure $ CE.Concolic concrete (Just symbolic)