quebex

 1-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
 2--
 3-- SPDX-License-Identifier: GPL-3.0-only
 4
 5module Language.QBE.Backend.Store
 6  ( Store,
 7    Assign,
 8    empty,
 9    sexprs,
10    assign,
11    setModel,
12    getConcolic,
13  )
14where
15
16import Data.Functor (($>))
17import Data.IORef (IORef, newIORef, readIORef, writeIORef)
18import Data.Map qualified as Map
19import Language.QBE.Backend.Model qualified as Model
20import Language.QBE.Simulator.Concolic.Expression qualified as CE
21import Language.QBE.Simulator.Default.Expression qualified as DE
22import Language.QBE.Simulator.Expression qualified as E
23import Language.QBE.Simulator.Symbolic.Expression qualified as SE
24import Language.QBE.Types qualified as QBE
25import SimpleSMT qualified as SMT
26import System.Random.Stateful (IOGenM, StdGen, initStdGen, newIOGenM, uniformWord64)
27
28-- | Concrete variable assignment.
29type Assign = Map.Map String DE.RegVal
30
31-- A variable store mapping variable names to concrete values.
32data Store
33  = Store
34  { cValues :: IORef Assign,
35    sValues :: IORef (Map.Map String SE.BitVector),
36    randGen :: IOGenM StdGen
37  }
38
39-- | Create a new (empty) store.
40empty :: IO Store
41empty = do
42  ranGen <- initStdGen >>= newIOGenM
43  conMap <- newIORef Map.empty
44  symMap <- newIORef Map.empty
45  pure $ Store conMap symMap ranGen
46
47-- | Obtain symbolic values as a list of 'SimpleSMT' expressions.
48sexprs :: Store -> IO [SMT.SExpr]
49sexprs Store {sValues = m} =
50  map SE.toSExpr <$> (Map.elems <$> readIORef m)
51
52-- | Obtain a list of concrete variable assignments.
53assign :: Store -> IO Assign
54assign store = readIORef (cValues store)
55
56-- | Create a variable store from a 'Model'.
57setModel :: Store -> Model.Model -> IO ()
58setModel store model = do
59  modelMap <- Map.fromList <$> Model.toList model
60  writeIORef (cValues store) modelMap
61
62-- | Lookup the variable name in the store, if it doesn't exist return
63-- an unconstrained 'CE.Concolic' value with a random concrete part.
64getConcolic :: SMT.Solver -> Store -> String -> QBE.BaseType -> IO CE.Concolic
65getConcolic solver store@Store {cValues = con, sValues = sym} name ty = do
66  concreteMap <- readIORef con
67  concrete <-
68    case Map.lookup name concreteMap of
69      Just x -> pure x
70      Nothing ->
71        -- TODO: The uniform generator must consider the bounds of QBE.BaseType.
72        E.fromLit ty <$> uniformWord64 (randGen store)
73
74  symbolicMap <- readIORef sym
75  symbolic <-
76    case Map.lookup name symbolicMap of
77      Just x -> pure x
78      Nothing -> do
79        s <- SE.symbolic solver name ty
80        writeIORef sym (Map.insert name s symbolicMap) $> s
81
82  pure $ CE.Concolic concrete (Just symbolic)