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.Simulator.Symbolic.Folding
 6  ( notExpr,
 7    eqExpr,
 8    extractExpr,
 9    concatExpr,
10  )
11where
12
13import Control.Exception (assert)
14import Data.Bits (shiftL, shiftR, (.&.))
15import SimpleSMT qualified as SMT
16
17-- Performs the following transformation: (not (not X)) → X.
18notExpr :: SMT.SExpr -> SMT.SExpr
19notExpr (SMT.List [SMT.Atom "not", cond]) = cond
20notExpr expr = SMT.not expr
21
22-- Eliminates ITE expressions when comparing with constants values, this is
23-- useful in the QBE context to eliminate comparisons with truth values.
24eqExpr :: SMT.SExpr -> SMT.SExpr -> SMT.SExpr
25eqExpr expr@(SMT.List [SMT.Atom "ite", cond@(SMT.List _), ifT, ifF]) o =
26  case (SMT.sexprToVal ifT, SMT.sexprToVal ifF, SMT.sexprToVal o) of
27    -- XXX: bit sizes must be equal, otherwise it would be invalid SMT-LIB.
28    (SMT.Bits _ tv, SMT.Bits _ fv, SMT.Bits _ ov) ->
29      if ov == tv
30        then cond
31        else
32          if ov == fv
33            then SMT.not cond
34            else SMT.eq expr o
35    _ -> SMT.eq expr o
36eqExpr expr o = SMT.eq expr o
37
38-- Replaces continuous concat expressions with a single extract expression.
39concatExpr :: SMT.SExpr -> SMT.SExpr -> SMT.SExpr
40concatExpr
41  lhs@(SMT.List [SMT.List [SMT.Atom "_", SMT.Atom "extract", lx, ly], varLhs])
42  rhs@(SMT.List [SMT.List [SMT.Atom "_", SMT.Atom "extract", rx, ry], varRhs])
43    | varLhs == varRhs =
44        case (SMT.sexprToVal lx, SMT.sexprToVal ly, SMT.sexprToVal rx, SMT.sexprToVal ry) of
45          (SMT.Int lx', SMT.Int ly', SMT.Int rx', SMT.Int ry') ->
46            if ly' == rx' + 1
47              then extractExpr varLhs (fromIntegral ry') $ assert (lx' > ry') (fromIntegral $ lx' - ry' + 1)
48              else SMT.concat lhs rhs
49          _ -> error "unreachable" -- invalid SMT-LIB
50    | otherwise = SMT.concat lhs rhs
51concatExpr lhs rhs = SMT.concat lhs rhs
52
53-- Alternative creation of `SMT.extract` expressions.
54extract :: SMT.SExpr -> Int -> Int -> SMT.SExpr
55extract expr off width =
56  SMT.extract expr (fromIntegral $ off + width - 1) $ fromIntegral off
57
58-- Eliminate nested extract expression fo the same width.
59extractNested :: SMT.SExpr -> Int -> Int -> SMT.SExpr
60extractNested
61  expr@(SMT.List [SMT.List [SMT.Atom "_", SMT.Atom "extract", ix, iy], _])
62  off
63  width =
64    case (SMT.sexprToVal ix, SMT.sexprToVal iy) of
65      (SMT.Int ix', SMT.Int iy') ->
66        if (fromIntegral ix' == off + width - 1) && fromIntegral iy' == off
67          then expr
68          else extract expr off width
69      _ -> error "unreachable" -- invalid SMT-LIB
70extractNested expr off width = extract expr off width
71
72-- Performs direct extractions of constant immediate values.
73extractConst :: SMT.SExpr -> Int -> Int -> SMT.SExpr
74extractConst expr off width =
75  case SMT.sexprToVal expr of
76    SMT.Bits _ value ->
77      SMT.bvBin width $ truncTo (value `shiftR` off) width
78    _ -> extractNested expr off width
79  where
80    truncTo value bits = value .&. ((1 `shiftL` bits) - 1)
81
82-- This performs constant propagation for subtyping of condition values (i.e.
83-- the conversion from long to word).
84extractITE :: SMT.SExpr -> Int -> Int -> SMT.SExpr
85extractITE expr@(SMT.List [SMT.Atom "ite", cond@(SMT.List _), ifT, ifF]) off width =
86  case (SMT.sexprToVal ifT, SMT.sexprToVal ifF) of
87    (SMT.Bits _ _, SMT.Bits _ _) ->
88      let ex x = extractConst x off width
89       in SMT.List [SMT.Atom "ite", cond, ex ifT, ex ifF]
90    _ -> extractNested expr off width -- not constant, skip extractConst
91extractITE expr off width = extractConst expr off width
92
93-- Chaining of multiple extract expression folding schemes.
94extractExpr :: SMT.SExpr -> Int -> Int -> SMT.SExpr
95extractExpr = extractITE