qute

  1-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
  2--
  3-- SPDX-License-Identifier: MIT AND GPL-3.0-only
  4{-# LANGUAGE PatternSynonyms #-}
  5
  6module SimpleBV
  7  ( SExpr,
  8    SMT.Solver (..),
  9    SMT.defaultConfig,
 10    SMT.newLogger,
 11    SMT.newLoggerWithHandle,
 12    SMT.newSolver,
 13    SMT.newSolverWithConfig,
 14    SMT.solverLogger,
 15    SMT.smtSolverLogger,
 16    SMT.setLogic,
 17    SMT.setOption,
 18    SMT.push,
 19    SMT.pop,
 20    SMT.popMany,
 21    SMT.check,
 22    SMT.Result (..),
 23    SMT.Value (..),
 24    pattern W,
 25    pattern Byte,
 26    pattern Half,
 27    pattern Word,
 28    pattern Long,
 29    width,
 30    const,
 31    declareBV,
 32    assert,
 33    sexprToVal,
 34    getValue,
 35    getValues,
 36    toSMT,
 37    ite,
 38    and,
 39    or,
 40    not,
 41    eq,
 42    bvLit,
 43    bvAdd,
 44    bvAShr,
 45    bvLShr,
 46    bvAnd,
 47    bvMul,
 48    bvNeg,
 49    bvOr,
 50    bvSDiv,
 51    bvSLeq,
 52    bvSLt,
 53    bvSGeq,
 54    bvSGt,
 55    bvSRem,
 56    bvShl,
 57    bvSub,
 58    bvUDiv,
 59    bvULeq,
 60    bvUGeq,
 61    bvUGt,
 62    bvULt,
 63    bvURem,
 64    bvXOr,
 65    concat,
 66    extract,
 67    signExtend,
 68    zeroExtend,
 69  )
 70where
 71
 72import Control.DeepSeq (NFData, NFData1)
 73import Data.Bits (shiftL, shiftR, (.&.))
 74import GHC.Generics (Generic, Generic1)
 75import SimpleSMT qualified as SMT
 76import Prelude hiding (and, concat, const, not, or)
 77
 78data Expr a
 79  = Var String
 80  | Int Integer
 81  | And a a
 82  | Or a a
 83  | Neg a
 84  | Not a
 85  | Eq a a
 86  | BvAdd a a
 87  | BvAShr a a
 88  | BvLShr a a
 89  | BvAnd a a
 90  | BvMul a a
 91  | BvOr a a
 92  | BvSDiv a a
 93  | BvSLeq a a
 94  | BvSLt a a
 95  | BvSGeq a a
 96  | BvSGt a a
 97  | BvSRem a a
 98  | BvShl a a
 99  | BvSub a a
100  | BvUDiv a a
101  | BvULeq a a
102  | BvUGeq a a
103  | BvUGt a a
104  | BvULt a a
105  | BvURem a a
106  | BvXOr a a
107  | Concat a a
108  | Ite a a a
109  | Extract Int Int a
110  | SignExtend Integer a
111  | ZeroExtend Integer a
112  deriving (Show, Eq, Generic, Generic1)
113
114instance (NFData a) => NFData (Expr a)
115
116instance NFData1 Expr
117
118data SExpr
119  = SExpr
120  { width :: Int,
121    sexpr :: Expr SExpr
122  }
123  deriving (Show, Eq, Generic)
124
125instance NFData SExpr
126
127toSMT :: SExpr -> SMT.SExpr
128toSMT expr =
129  case sexpr expr of
130    (Var name) -> SMT.const name
131    (Int v) -> SMT.List [SMT.Atom "_", SMT.Atom ("bv" ++ show v), SMT.Atom $ show (width expr)]
132    (Or lhs rhs) -> SMT.or (toSMT lhs) (toSMT rhs)
133    (Ite cond lhs rhs) -> SMT.ite (toSMT cond) (toSMT lhs) (toSMT rhs)
134    (And lhs rhs) -> SMT.and (toSMT lhs) (toSMT rhs)
135    (Not v) -> SMT.not (toSMT v)
136    (Neg v) -> SMT.bvNeg (toSMT v)
137    (SignExtend n v) -> SMT.signExtend n (toSMT v)
138    (ZeroExtend n v) -> SMT.zeroExtend n (toSMT v)
139    (Eq lhs rhs) -> SMT.eq (toSMT lhs) (toSMT rhs)
140    (Concat lhs rhs) -> SMT.concat (toSMT lhs) (toSMT rhs)
141    (Extract o w e) -> SMT.extract (toSMT e) (fromIntegral $ o + w - 1) (fromIntegral o)
142    (BvAnd lhs rhs) -> SMT.bvAnd (toSMT lhs) (toSMT rhs)
143    (BvAShr lhs rhs) -> SMT.bvAShr (toSMT lhs) (toSMT rhs)
144    (BvLShr lhs rhs) -> SMT.bvLShr (toSMT lhs) (toSMT rhs)
145    (BvAdd lhs rhs) -> SMT.bvAdd (toSMT lhs) (toSMT rhs)
146    (BvMul lhs rhs) -> SMT.bvMul (toSMT lhs) (toSMT rhs)
147    (BvOr lhs rhs) -> SMT.bvOr (toSMT lhs) (toSMT rhs)
148    (BvSDiv lhs rhs) -> SMT.bvSDiv (toSMT lhs) (toSMT rhs)
149    (BvSLeq lhs rhs) -> SMT.bvSLeq (toSMT lhs) (toSMT rhs)
150    (BvSLt lhs rhs) -> SMT.bvSLt (toSMT lhs) (toSMT rhs)
151    (BvSGeq lhs rhs) -> SMT.fun "bvsge" [toSMT lhs, toSMT rhs]
152    (BvSGt lhs rhs) -> SMT.fun "bvsgt" [toSMT lhs, toSMT rhs]
153    (BvSRem lhs rhs) -> SMT.bvSRem (toSMT lhs) (toSMT rhs)
154    (BvShl lhs rhs) -> SMT.bvShl (toSMT lhs) (toSMT rhs)
155    (BvSub lhs rhs) -> SMT.bvSub (toSMT lhs) (toSMT rhs)
156    (BvUDiv lhs rhs) -> SMT.bvUDiv (toSMT lhs) (toSMT rhs)
157    (BvULeq lhs rhs) -> SMT.bvULeq (toSMT lhs) (toSMT rhs)
158    (BvUGeq lhs rhs) -> SMT.fun "bvuge" [toSMT lhs, toSMT rhs]
159    (BvUGt lhs rhs) -> SMT.fun "bvugt" [toSMT lhs, toSMT rhs]
160    (BvULt lhs rhs) -> SMT.bvULt (toSMT lhs) (toSMT rhs)
161    (BvURem lhs rhs) -> SMT.bvURem (toSMT lhs) (toSMT rhs)
162    (BvXOr lhs rhs) -> SMT.bvXOr (toSMT lhs) (toSMT rhs)
163
164boolWidth :: Int
165boolWidth = 1
166
167pattern E :: Expr SExpr -> SExpr
168pattern E expr <- SExpr {sexpr = expr, width = _}
169
170pattern W :: Int -> SExpr
171pattern W w <- SExpr {width = w}
172
173pattern Byte :: SExpr
174pattern Byte <- SExpr {width = 8}
175
176pattern Half :: SExpr
177pattern Half <- SExpr {width = 16}
178
179pattern Word :: SExpr
180pattern Word <- SExpr {width = 32}
181
182pattern Long :: SExpr
183pattern Long <- SExpr {width = 64}
184
185------------------------------------------------------------------------
186
187const :: String -> Int -> SExpr
188const name width = SExpr width (Var name)
189
190declareBV :: SMT.Solver -> String -> Int -> IO SExpr
191declareBV solver name width = do
192  let bits = SMT.tBits $ fromIntegral width
193  SMT.declare solver name bits >> pure (const name width)
194
195bvLit :: Int -> Integer -> SExpr
196bvLit width value = SExpr width (Int value)
197
198sexprToVal :: SExpr -> SMT.Value
199sexprToVal (E (Var n)) = SMT.Other $ SMT.Atom n
200sexprToVal e@(E (Int i)) = SMT.Bits (width e) i
201sexprToVal _ = SMT.Other $ SMT.Atom "_"
202
203assert :: SMT.Solver -> SExpr -> IO ()
204assert solver = SMT.assert solver . toSMT
205
206getValue :: SMT.Solver -> SExpr -> IO SMT.Value
207getValue solver = SMT.getExpr solver . toSMT
208
209getValues :: SMT.Solver -> [SExpr] -> IO [(String, SMT.Value)]
210getValues solver exprs = do
211  map go <$> SMT.getExprs solver (map toSMT exprs)
212  where
213    go :: (SMT.SExpr, SMT.Value) -> (String, SMT.Value)
214    go (SMT.Atom name, value) = (name, value)
215    go _ = error "non-atomic variable in inputVars"
216
217---------------------------------------------------------------------------
218
219ite :: SExpr -> SExpr -> SExpr -> SExpr
220ite cond ifT ifF = SExpr (width ifT) (Ite cond ifT ifF)
221
222not :: SExpr -> SExpr
223not (E (Not cond)) = cond
224not expr = expr {sexpr = Not expr}
225
226and :: SExpr -> SExpr -> SExpr
227and lhs rhs = lhs {sexpr = And lhs rhs}
228
229or :: SExpr -> SExpr -> SExpr
230or lhs rhs = lhs {sexpr = Or lhs rhs}
231
232signExtend :: Integer -> SExpr -> SExpr
233signExtend n expr = SExpr (width expr + fromIntegral n) $ SignExtend n expr
234
235zeroExtend :: Integer -> SExpr -> SExpr
236zeroExtend n expr = SExpr (width expr + fromIntegral n) $ ZeroExtend n expr
237
238------------------------------------------------------------------------
239
240eq' :: SExpr -> SExpr -> SExpr
241eq' lhs rhs = SExpr boolWidth $ Eq lhs rhs
242
243-- Eliminates ITE expressions when comparing with constants values, this is
244-- useful in the QBE context to eliminate comparisons with truth values.
245eq :: SExpr -> SExpr -> SExpr
246eq lexpr@(E (Ite cond (E (Int ifT)) (E (Int ifF)))) rexpr@(E (Int other))
247  | other == ifT = cond
248  | other == ifF = not cond
249  | otherwise = eq' lexpr rexpr
250eq lhs rhs = eq' lhs rhs
251
252concat' :: SExpr -> SExpr -> SExpr
253concat' lhs rhs =
254  SExpr (width lhs + width rhs) $ Concat lhs rhs
255
256-- Replace 0 concats with zero extension: (concat (_ bv0 8) buf6)
257concatZeros :: SExpr -> SExpr -> SExpr
258concatZeros lhs@(E (Int 0)) rhs = zeroExtend (fromIntegral $ width lhs) rhs
259concatZeros lhs rhs = concat' lhs rhs
260
261-- Replaces continuous concat expressions with a single extract expression.
262concat :: SExpr -> SExpr -> SExpr
263concat
264  lhs@(E (Extract loff lwidth latom@(E exprLhs)))
265  rhs@(E (Extract roff rwidth (E exprRhs)))
266    | exprLhs == exprRhs && (roff + rwidth) == loff = extract latom roff (lwidth + rwidth)
267    | otherwise = concatZeros lhs rhs
268concat lhs rhs = concatZeros lhs rhs
269
270extract' :: SExpr -> Int -> Int -> SExpr
271extract' expr off w = SExpr w $ Extract off w expr
272
273-- Eliminate extract expression where the value already has the desired bits.
274extractSameWidth :: SExpr -> Int -> Int -> SExpr
275extractSameWidth expr off w
276  | off == 0 && width expr == w = expr
277  | otherwise = extract' expr off w
278
279-- Eliminate nested extract expression of the same width.
280extractNested :: SExpr -> Int -> Int -> SExpr
281extractNested expr@(E (Extract ioff iwidth _)) off width =
282  if ioff == off && iwidth == width
283    then expr
284    else extractSameWidth expr off width
285extractNested expr off width = extractSameWidth expr off width
286
287-- Performs direct extractions of constant immediate values.
288extractConst :: SExpr -> Int -> Int -> SExpr
289extractConst (E (Int value)) off w =
290  SExpr w . Int $ truncTo (value `shiftR` off) w
291  where
292    truncTo v bits = v .&. ((1 `shiftL` bits) - 1)
293extractConst expr off width = extractNested expr off width
294
295-- This performs constant propagation for subtyping of condition values (i.e.
296-- the conversion from long to word).
297extractIte :: SExpr -> Int -> Int -> SExpr
298extractIte (E (Ite cond ifT@(E (Int _)) ifF@(E (Int _)))) off w =
299  let ex x = extractConst x off w
300   in SExpr w $ Ite cond (ex ifT) (ex ifF)
301extractIte expr off width = extractConst expr off width
302
303extractZeros ::
304  SExpr ->
305  Int ->
306  Int ->
307  SExpr
308extractZeros expr@(E (ZeroExtend extBits inner)) exOff exWidth
309  | exOff >= width inner && extBits > 0 = bvLit exWidth 0 -- only extracting zeros
310  | otherwise = extractIte expr exOff exWidth
311extractZeros outer exOff exWidth = extractIte outer exOff exWidth
312
313extractExt' ::
314  (Integer -> SExpr -> Expr SExpr) ->
315  SExpr ->
316  Integer ->
317  SExpr ->
318  Int ->
319  Int ->
320  SExpr
321extractExt' cons outer extBits inner exOff exWidth
322  -- If we are only extracting the non-extended bytes...
323  | width inner >= exOff + exWidth = extractZeros inner exOff exWidth
324  -- Consider: ((_ extract 31 0) ((_ zero_extend 56) byte))
325  | exWidth < fromIntegral extBits && exOff == 0 =
326      SExpr exWidth $ cons (extBits - fromIntegral exWidth) inner
327  -- No folding...
328  | otherwise = extractZeros outer exOff exWidth
329
330-- Remove ZeroExtend and SignExtend expression where we don't use
331-- the extended bits because we extract below the extended size.
332extractExt :: SExpr -> Int -> Int -> SExpr
333extractExt expr@(E (SignExtend extBits inner)) exOff exWidth =
334  extractExt' SignExtend expr extBits inner exOff exWidth
335extractExt expr@(E (ZeroExtend extBits inner)) exOff exWidth =
336  extractExt' ZeroExtend expr extBits inner exOff exWidth
337extractExt expr off w = extractIte expr off w
338
339extract :: SExpr -> Int -> Int -> SExpr
340extract = extractExt
341
342------------------------------------------------------------------------
343
344binOp' :: (SExpr -> SExpr -> Expr SExpr) -> SExpr -> SExpr -> SExpr
345binOp' op lhs rhs = lhs {sexpr = op lhs rhs}
346
347binOp :: (SExpr -> SExpr -> Expr SExpr) -> SExpr -> SExpr -> SExpr
348-- Consider: (bvslt ((_ zero_extend 24) byte0) ((_ zero_extend 24) byte1))
349-- TODO: The following only works if 'op' does not consider sign-bits. Otherwise,
350--       there is no semantic expression equivalence after this folding operation.
351-- binOp op lhs@(E (ZeroExtend _ lhsInner)) rhs@(E (ZeroExtend _ rhsInner)) =
352--   if width lhsInner == width rhsInner
353--     then binOp op lhsInner rhsInner
354--     else binOp' op lhs rhs
355binOp op lhs rhs = binOp' op lhs rhs
356
357-- TODO: Generate these using template-haskell.
358
359bvNeg :: SExpr -> SExpr
360bvNeg x = x {sexpr = Neg x}
361
362bvAdd :: SExpr -> SExpr -> SExpr
363bvAdd = binOp BvAdd
364
365bvAShr :: SExpr -> SExpr -> SExpr
366bvAShr = binOp BvAShr
367
368bvLShr :: SExpr -> SExpr -> SExpr
369bvLShr = binOp BvLShr
370
371bvAnd :: SExpr -> SExpr -> SExpr
372bvAnd = binOp BvAnd
373
374bvMul :: SExpr -> SExpr -> SExpr
375bvMul = binOp BvMul
376
377bvOr :: SExpr -> SExpr -> SExpr
378bvOr = binOp BvOr
379
380bvSDiv :: SExpr -> SExpr -> SExpr
381bvSDiv = binOp BvSDiv
382
383bvSLeq :: SExpr -> SExpr -> SExpr
384bvSLeq = binOp BvSLeq
385
386bvSLt :: SExpr -> SExpr -> SExpr
387bvSLt = binOp BvSLt
388
389bvSGeq :: SExpr -> SExpr -> SExpr
390bvSGeq = binOp BvSGeq
391
392bvSGt :: SExpr -> SExpr -> SExpr
393bvSGt = binOp BvSGt
394
395bvSRem :: SExpr -> SExpr -> SExpr
396bvSRem = binOp BvSRem
397
398bvShl :: SExpr -> SExpr -> SExpr
399bvShl = binOp BvShl
400
401bvSub :: SExpr -> SExpr -> SExpr
402bvSub = binOp BvSub
403
404bvUDiv :: SExpr -> SExpr -> SExpr
405bvUDiv = binOp BvUDiv
406
407bvULeq :: SExpr -> SExpr -> SExpr
408bvULeq = binOp BvULeq
409
410bvUGeq :: SExpr -> SExpr -> SExpr
411bvUGeq = binOp BvUGeq
412
413bvUGt :: SExpr -> SExpr -> SExpr
414bvUGt = binOp BvUGt
415
416bvULt :: SExpr -> SExpr -> SExpr
417bvULt = binOp BvULt
418
419bvURem :: SExpr -> SExpr -> SExpr
420-- Fold constant bvURem operations which are emitted a lot in our generated
421-- SMT-LIB because of QBE's "shift-value modulo bitsize"-semantics.
422bvURem vlhs@(E (Int lhs)) (E (Int rhs)) =
423  SExpr (width vlhs) $
424    -- XXX: On urem-by-zero, SMT-LIB returns the lhs.
425    if rhs == 0
426      then Int lhs
427      else Int $ lhs `rem` rhs
428bvURem lhs rhs = binOp BvURem lhs rhs
429
430bvXOr :: SExpr -> SExpr -> SExpr
431bvXOr = binOp BvXOr