quebex

 1-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
 2--
 3-- SPDX-License-Identifier: GPL-3.0-only
 4module Language.QBE.Backend.Model
 5  ( Model,
 6    Error (..),
 7    toList,
 8    getModel,
 9  )
10where
11
12import Control.Exception (Exception, throwIO)
13import Language.QBE.Simulator.Default.Expression qualified as DE
14import SimpleSMT qualified as SMT
15
16data Error
17  = NonAtomNameSExpr
18  | UnsupportedValueType
19  | InvalidBitVectorSize
20  deriving (Show)
21
22instance Exception Error
23
24------------------------------------------------------------------------
25
26-- Assignments returned by the Solver for a given query.
27newtype Model = Model [(String, SMT.Value)]
28  deriving (Show, Eq)
29
30-- | Get a new 'Model' for a list of input variables that should be contained in it.
31getModel :: SMT.Solver -> [SMT.SExpr] -> IO Model
32getModel solver inputVars = do
33  lst <- SMT.getExprs solver inputVars >>= mapM go
34  pure $ Model lst
35  where
36    go :: (SMT.SExpr, SMT.Value) -> IO (String, SMT.Value)
37    go (SMT.Atom name, value) = pure (name, value)
38    go _ = throwIO NonAtomNameSExpr
39
40-- | Convert a model to a list of concrete variable assignments.
41toList :: Model -> IO [(String, DE.RegVal)]
42toList (Model lst) = mapM go lst
43  where
44    go :: (String, SMT.Value) -> IO (String, DE.RegVal)
45    go (name, SMT.Bits n v) =
46      case DE.fromBits n v of
47        Just x -> pure (name, x)
48        Nothing -> throwIO InvalidBitVectorSize
49    go _ = throwIO UnsupportedValueType