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    toList,
 7    getModel,
 8  )
 9where
10
11import Language.QBE.Simulator.Default.Expression qualified as DE
12import SimpleBV qualified as SMT
13
14-- Assignments returned by the Solver for a given query.
15newtype Model = Model [(String, SMT.Value)]
16  deriving (Show, Eq)
17
18-- | Get a new 'Model' for a list of input variables that should be contained in it.
19getModel :: SMT.Solver -> [SMT.SExpr] -> IO Model
20getModel solver inputVars = Model <$> SMT.getValues solver inputVars
21
22-- | Convert a model to a list of concrete variable assignments.
23toList :: Model -> [(String, DE.RegVal)]
24toList (Model lst) = map go lst
25  where
26    go :: (String, SMT.Value) -> (String, DE.RegVal)
27    go (name, SMT.Bits n v) =
28      case DE.fromBits n v of
29        Just x -> (name, x)
30        Nothing -> error "invalid bitvector size"
31    go _ = error "unsupported value type"