1use std::fmt::Debug;
2
3use mck::{abstr::AbstractValue, refin::RefinementValue};
4use serde::{Deserialize, Serialize};
5
6use crate::{
7 iir::{join_limited, variable::IVarId, IAbstr, IRefin},
8 ir_common::{IrMckBinaryOp, IrMckUnaryOp},
9};
10
11#[derive(Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
12pub struct IMckUnary {
13 pub op: IrMckUnaryOp,
14 pub operand: IVarId,
15}
16
17impl IMckUnary {
18 pub(super) fn forward_interpret(&self, abstr: &IAbstr) -> AbstractValue {
19 let operand = abstr.value(self.operand).clone();
20 match self.op {
21 IrMckUnaryOp::Not => mck::forward::Bitwise::bit_not(operand),
22 IrMckUnaryOp::Neg => mck::forward::HwArith::arith_neg(operand),
23 }
24 }
25
26 pub(super) fn backward_interpret(
27 &self,
28 abstr: &IAbstr,
29 refin: &mut IRefin,
30 later: RefinementValue,
31 ) {
32 let operand = abstr.value(self.operand).clone();
33 let earlier = match self.op {
34 IrMckUnaryOp::Not => mck::backward::Bitwise::bit_not((operand,), later).0,
35
36 IrMckUnaryOp::Neg => mck::backward::HwArith::arith_neg((operand,), later).0,
37 };
38
39 join_limited(abstr, refin, self.operand, earlier);
40 }
41}
42
43impl Debug for IMckUnary {
44 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
45 write!(f, "{}({:?})", self.op, self.operand)
46 }
47}
48
49#[derive(Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
50pub struct IMckBinary {
51 pub op: IrMckBinaryOp,
52 pub a: IVarId,
53 pub b: IVarId,
54}
55
56impl IMckBinary {
57 pub(super) fn forward_interpret(&self, inter: &IAbstr) -> AbstractValue {
58 let a = inter.value(self.a).clone();
59 let b = inter.value(self.b).clone();
60
61 match self.op {
62 IrMckBinaryOp::BitAnd => mck::forward::Bitwise::bit_and(a, b),
63 IrMckBinaryOp::BitOr => mck::forward::Bitwise::bit_or(a, b),
64 IrMckBinaryOp::BitXor => mck::forward::Bitwise::bit_xor(a, b),
65
66 IrMckBinaryOp::LogicShl => mck::forward::HwShift::logic_shl(a, b),
67 IrMckBinaryOp::LogicShr => mck::forward::HwShift::logic_shr(a, b),
68 IrMckBinaryOp::ArithShr => mck::forward::HwShift::arith_shr(a, b),
69
70 IrMckBinaryOp::Add => mck::forward::HwArith::add(a, b),
71 IrMckBinaryOp::Sub => mck::forward::HwArith::sub(a, b),
72 IrMckBinaryOp::Mul => mck::forward::HwArith::mul(a, b),
73 IrMckBinaryOp::Udiv => mck::forward::HwArith::udiv(a, b),
74 IrMckBinaryOp::Urem => mck::forward::HwArith::urem(a, b),
75 IrMckBinaryOp::Sdiv => mck::forward::HwArith::sdiv(a, b),
76 IrMckBinaryOp::Srem => mck::forward::HwArith::srem(a, b),
77
78 IrMckBinaryOp::Eq => mck::forward::TypedEq::eq(a, b),
79 IrMckBinaryOp::Ne => mck::forward::TypedEq::ne(a, b),
80
81 IrMckBinaryOp::Ult => mck::forward::TypedCmp::ult(a, b),
82 IrMckBinaryOp::Ule => mck::forward::TypedCmp::ule(a, b),
83 IrMckBinaryOp::Slt => mck::forward::TypedCmp::slt(a, b),
84 IrMckBinaryOp::Sle => mck::forward::TypedCmp::sle(a, b),
85 }
86 }
87
88 pub(super) fn backward_interpret(
89 &self,
90 abstr: &IAbstr,
91 refin: &mut IRefin,
92 later: RefinementValue,
93 ) {
94 let a = abstr.value(self.a).clone();
95 let b = abstr.value(self.b).clone();
96
97 let (earlier_a, earlier_b) = match self.op {
98 IrMckBinaryOp::BitAnd => mck::backward::Bitwise::bit_and((a, b), later),
99 IrMckBinaryOp::BitOr => mck::backward::Bitwise::bit_or((a, b), later),
100 IrMckBinaryOp::BitXor => mck::backward::Bitwise::bit_xor((a, b), later),
101
102 IrMckBinaryOp::LogicShl => mck::backward::HwShift::logic_shl((a, b), later),
103 IrMckBinaryOp::LogicShr => mck::backward::HwShift::logic_shr((a, b), later),
104 IrMckBinaryOp::ArithShr => mck::backward::HwShift::arith_shr((a, b), later),
105
106 IrMckBinaryOp::Add => mck::backward::HwArith::add((a, b), later),
107 IrMckBinaryOp::Sub => mck::backward::HwArith::sub((a, b), later),
108 IrMckBinaryOp::Mul => mck::backward::HwArith::mul((a, b), later),
109 IrMckBinaryOp::Udiv => mck::backward::HwArith::udiv((a, b), later),
110 IrMckBinaryOp::Urem => mck::backward::HwArith::urem((a, b), later),
111 IrMckBinaryOp::Sdiv => mck::backward::HwArith::sdiv((a, b), later),
112 IrMckBinaryOp::Srem => mck::backward::HwArith::srem((a, b), later),
113
114 IrMckBinaryOp::Eq => mck::backward::TypedEq::eq((a, b), later),
115 IrMckBinaryOp::Ne => mck::backward::TypedEq::ne((a, b), later),
116
117 IrMckBinaryOp::Ult => mck::backward::TypedCmp::ult((a, b), later),
118 IrMckBinaryOp::Ule => mck::backward::TypedCmp::ule((a, b), later),
119 IrMckBinaryOp::Slt => mck::backward::TypedCmp::slt((a, b), later),
120 IrMckBinaryOp::Sle => mck::backward::TypedCmp::sle((a, b), later),
121 };
122
123 join_limited(abstr, refin, self.a, earlier_a);
124 join_limited(abstr, refin, self.b, earlier_b);
125 }
126}
127
128impl Debug for IMckBinary {
129 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
130 write!(f, "{}({:?}, {:?})", self.op, self.a, self.b)
131 }
132}
133
134#[derive(Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
135pub struct IMckExt {
136 pub signed: bool,
137 pub width: u32,
138 pub inner: IVarId,
139}
140impl IMckExt {
141 pub(super) fn forward_interpret(&self, inter: &IAbstr) -> AbstractValue {
142 let inner = inter.value(self.inner).clone();
143
144 if self.signed {
145 inner.sext(self.width)
146 } else {
147 inner.uext(self.width)
148 }
149 }
150
151 pub(super) fn backward_interpret(
152 &self,
153 abstr: &IAbstr,
154 refin: &mut IRefin,
155 later: RefinementValue,
156 ) {
157 let later = *later.expect_bitvector();
158 let inner = *abstr.value(self.inner).expect_bitvector();
159
160 let earlier = RefinementValue::Bitvector(
161 if self.signed {
162 mck::backward::RExt::sext((inner,), later)
163 } else {
164 mck::backward::RExt::uext((inner,), later)
165 }
166 .0,
167 );
168
169 join_limited(abstr, refin, self.inner, earlier);
170 }
171}
172
173impl Debug for IMckExt {
174 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
175 let op_str = if self.signed { "Sext" } else { "Uext" };
176 write!(f, "{}({:?}, {})", op_str, self.inner, self.width)
177 }
178}