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 (cValues),
 7    Assign,
 8    empty,
 9    sexprs,
10    finalize,
11    setModel,
12    getConcolic,
13  )
14where
15
16import Data.Map qualified as Map
17import Language.QBE.Backend.Model qualified as Model
18import Language.QBE.Simulator.Concolic.Expression qualified as CE
19import Language.QBE.Simulator.Default.Expression qualified as DE
20import Language.QBE.Simulator.Expression qualified as E
21import Language.QBE.Simulator.Symbolic.Expression qualified as SE
22import Language.QBE.Types qualified as QBE
23import SimpleBV qualified as SMT
24import System.Random (StdGen, genWord64)
25
26-- | Concrete variable assignment.
27type Assign = Map.Map String DE.RegVal
28
29-- A variable store mapping variable names to concrete values.
30data Store
31  = Store
32  { cValues :: Assign,
33    sValues :: Map.Map String SE.BitVector,
34    defined :: Map.Map String SE.BitVector,
35    randGen :: StdGen
36  }
37
38-- | Create a new (empty) store.
39empty :: StdGen -> Store
40empty = Store Map.empty Map.empty Map.empty
41
42-- | Obtain symbolic values as a list of 'SimpleBV' expressions.
43sexprs :: Store -> [SMT.SExpr]
44sexprs = map SE.toSExpr . Map.elems . sValues
45
46-- | Finalize all pending symbolic variable declarations.
47finalize :: SMT.Solver -> Store -> IO Store
48finalize solver store@(Store {sValues = m, defined = defs}) = do
49  let new = m `Map.difference` defs
50  mapM_ (uncurry declareSymbolic) $ Map.toList new
51
52  pure
53    store
54      { defined = Map.union m new,
55        sValues = Map.empty
56      }
57  where
58    declareSymbolic n v =
59      SMT.declareBV solver n $ SE.bitSize v
60
61-- | Create a variable store from a 'Model'.
62setModel :: Store -> Model.Model -> Store
63setModel store model =
64  store {cValues = Map.fromList $ Model.toList model}
65
66-- | Lookup the variable name in the store, if it doesn't exist return
67-- an unconstrained 'CE.Concolic' value with a random concrete part.
68getConcolic :: Store -> String -> QBE.ExtType -> (Store, CE.Concolic DE.RegVal)
69getConcolic store@Store {randGen = rand} name ty =
70  ( store {sValues = newSymVars, randGen = nextRand},
71    CE.Concolic concrete (Just symbolic)
72  )
73  where
74    (symbolic, newSymVars) =
75      let bv = SE.symbolic name ty
76       in (bv, Map.insert name bv $ sValues store)
77
78    (concrete, nextRand) =
79      case Map.lookup name (cValues store) of
80        Just cv -> (cv, rand)
81        Nothing ->
82          -- TODO: The generator should consider the bounds of QBE.BaseType.
83          let (rv, nr) = genWord64 rand
84              conValue = E.fromLit ty rv
85           in (conValue, nr)