qute-symex-0.1.0: test/Util.hs

-- SPDX-FileCopyrightText: 2025-2026 Sören Tempel <soeren+git@soeren-tempel.net>
--
-- SPDX-License-Identifier: GPL-3.0-only

module Util where

import Data.Bifunctor (second)
import Data.Word (Word64)
import Language.QBE (parseAndFind)
import Language.QBE.Backend.Tracer qualified as T
import Language.QBE.Simulator (execFunc)
import Language.QBE.Simulator.Concolic.Expression qualified as CE
import Language.QBE.Simulator.Concolic.State (mkEnv, run)
import Language.QBE.Simulator.Default.Expression qualified as DE
import Language.QBE.Simulator.Explorer (PathResult, defSolver, exploreFunc, newEngine)
import Language.QBE.Simulator.Expression qualified as E
import Language.QBE.Simulator.Symbolic.Expression qualified as SE
import Language.QBE.Types qualified as QBE
import SimpleBV qualified as SMT

parseAndExec :: QBE.GlobalIdent -> [CE.Concolic DE.RegVal] -> String -> IO T.ExecTrace
parseAndExec funcName params input = do
  (prog, entry) <- parseAndFind funcName input

  env <- mkEnv prog 0 128 Nothing
  fst <$> run env (execFunc entry params)

unconstrained :: SMT.Solver -> Word64 -> String -> QBE.BaseType -> IO (CE.Concolic DE.RegVal)
unconstrained solver initCon name ty = do
  let symbolic = SE.symbolic name (QBE.Base ty)
  -- XXX: This is a hack, normally the Store does this for us.
  _ <- SMT.declareBV solver name $ SE.bitSize symbolic

  let concrete = E.fromLit (QBE.Base ty) initCon
  pure $ CE.Concolic concrete (Just symbolic)

explore' :: String -> String -> [(String, QBE.BaseType)] -> IO [PathResult]
explore' input funcName params = do
  (prog, entry) <- parseAndFind (QBE.GlobalIdent funcName) input

  defEnv <- mkEnv prog 0 128 Nothing
  engine <- newEngine defEnv <$> defSolver
  exploreFunc engine entry $
    map (second QBE.Base) params