1use crate::ir::pcc::*;
4use crate::ir::types::*;
5use crate::isa::x64::inst::Inst;
6use crate::isa::x64::inst::args::{Amode, Gpr, RegMem, SyntheticAmode, ToWritableReg};
7use crate::machinst::pcc::*;
8use crate::machinst::{InsnIndex, VCode};
9use crate::machinst::{Reg, Writable};
10use crate::trace;
11
12fn undefined_result(
13 ctx: &FactContext,
14 vcode: &mut VCode<Inst>,
15 dst: Writable<Gpr>,
16 reg_bits: u16,
17 result_bits: u16,
18) -> PccResult<()> {
19 check_output(ctx, vcode, dst.to_writable_reg(), &[], |_vcode| {
20 clamp_range(ctx, reg_bits, result_bits, None)
21 })
22}
23
24fn ensure_no_fact(vcode: &VCode<Inst>, reg: Reg) -> PccResult<()> {
25 if vcode.vreg_fact(reg.into()).is_some() {
26 Err(PccError::UnsupportedFact)
27 } else {
28 Ok(())
29 }
30}
31
32#[derive(Clone, Debug, Default)]
34pub(crate) struct FactFlowState {
35 cmp_flags: Option<(Fact, Fact)>,
36}
37
38pub(crate) fn check(
39 ctx: &FactContext,
40 vcode: &mut VCode<Inst>,
41 inst_idx: InsnIndex,
42 state: &mut FactFlowState,
43) -> PccResult<()> {
44 trace!("Checking facts on inst: {:?}", vcode[inst_idx]);
45
46 let _cmp_flags = state.cmp_flags.take();
51
52 match vcode[inst_idx] {
53 Inst::Args { .. } => {
54 Ok(())
58 }
59
60 Inst::CheckedSRemSeq {
61 dst_quotient,
62 dst_remainder,
63 ..
64 } => {
65 undefined_result(ctx, vcode, dst_quotient, 64, 64)?;
66 undefined_result(ctx, vcode, dst_remainder, 64, 64)?;
67 Ok(())
68 }
69
70 Inst::CheckedSRemSeq8 { dst, .. } => undefined_result(ctx, vcode, dst, 64, 64),
71
72 Inst::MovFromPReg { dst, .. } => undefined_result(ctx, vcode, dst, 64, 64),
73 Inst::MovToPReg { .. } => Ok(()),
74
75 Inst::XmmCmove { dst, .. } => ensure_no_fact(vcode, dst.to_writable_reg().to_reg()),
76
77 Inst::StackProbeLoop { tmp, .. } => ensure_no_fact(vcode, tmp.to_reg()),
78
79 Inst::CvtUint64ToFloatSeq {
80 dst,
81 tmp_gpr1,
82 tmp_gpr2,
83 ..
84 } => {
85 ensure_no_fact(vcode, dst.to_writable_reg().to_reg())?;
86 ensure_no_fact(vcode, tmp_gpr1.to_writable_reg().to_reg())?;
87 ensure_no_fact(vcode, tmp_gpr2.to_writable_reg().to_reg())?;
88 Ok(())
89 }
90
91 Inst::CvtFloatToSintSeq {
92 dst,
93 tmp_gpr,
94 tmp_xmm,
95 ..
96 } => {
97 undefined_result(ctx, vcode, dst, 64, 64)?;
98 ensure_no_fact(vcode, tmp_gpr.to_writable_reg().to_reg())?;
99 ensure_no_fact(vcode, tmp_xmm.to_writable_reg().to_reg())?;
100 Ok(())
101 }
102
103 Inst::CvtFloatToUintSeq {
104 dst,
105 tmp_gpr,
106 tmp_xmm,
107 tmp_xmm2,
108 ..
109 } => {
110 undefined_result(ctx, vcode, dst, 64, 64)?;
111 ensure_no_fact(vcode, tmp_gpr.to_writable_reg().to_reg())?;
112 ensure_no_fact(vcode, tmp_xmm.to_writable_reg().to_reg())?;
113 ensure_no_fact(vcode, tmp_xmm2.to_writable_reg().to_reg())?;
114 Ok(())
115 }
116
117 Inst::XmmMinMaxSeq { dst, .. } => ensure_no_fact(vcode, dst.to_writable_reg().to_reg()),
118
119 Inst::CallKnown { .. }
120 | Inst::ReturnCallKnown { .. }
121 | Inst::JmpKnown { .. }
122 | Inst::WinchJmpIf { .. }
123 | Inst::JmpCond { .. }
124 | Inst::JmpCondOr { .. }
125 | Inst::TrapIf { .. }
126 | Inst::TrapIfAnd { .. }
127 | Inst::TrapIfOr { .. } => Ok(()),
128 Inst::Rets { .. } => Ok(()),
129
130 Inst::ReturnCallUnknown { .. } => Ok(()),
131
132 Inst::CallUnknown { ref info } => match &info.dest {
133 RegMem::Mem { addr } => {
134 check_load(ctx, None, addr, vcode, I64, 64)?;
135 Ok(())
136 }
137 RegMem::Reg { .. } => Ok(()),
138 },
139
140 Inst::JmpTableSeq { tmp1, tmp2, .. } => {
141 ensure_no_fact(vcode, tmp1.to_reg())?;
142 ensure_no_fact(vcode, tmp2.to_reg())?;
143 Ok(())
144 }
145
146 Inst::LoadExtName { dst, .. } => {
147 ensure_no_fact(vcode, *dst.to_reg())?;
148 Ok(())
149 }
150
151 Inst::AtomicRmwSeq {
152 ref mem,
153 temp,
154 dst_old,
155 ..
156 } => {
157 ensure_no_fact(vcode, *dst_old.to_reg())?;
158 ensure_no_fact(vcode, *temp.to_reg())?;
159 check_store(ctx, None, mem, vcode, I64)?;
160 Ok(())
161 }
162
163 Inst::Atomic128RmwSeq {
164 ref mem,
165 temp_low,
166 temp_high,
167 dst_old_low,
168 dst_old_high,
169 ..
170 } => {
171 ensure_no_fact(vcode, *dst_old_low.to_reg())?;
172 ensure_no_fact(vcode, *dst_old_high.to_reg())?;
173 ensure_no_fact(vcode, *temp_low.to_reg())?;
174 ensure_no_fact(vcode, *temp_high.to_reg())?;
175 check_store(ctx, None, mem, vcode, I128)?;
176 Ok(())
177 }
178
179 Inst::Atomic128XchgSeq {
180 ref mem,
181 dst_old_low,
182 dst_old_high,
183 ..
184 } => {
185 ensure_no_fact(vcode, *dst_old_low.to_reg())?;
186 ensure_no_fact(vcode, *dst_old_high.to_reg())?;
187 check_store(ctx, None, mem, vcode, I128)?;
188 Ok(())
189 }
190
191 Inst::XmmUninitializedValue { dst } => {
192 ensure_no_fact(vcode, dst.to_writable_reg().to_reg())
193 }
194
195 Inst::GprUninitializedValue { dst } => {
196 ensure_no_fact(vcode, dst.to_writable_reg().to_reg())
197 }
198
199 Inst::ElfTlsGetAddr { dst, .. } | Inst::MachOTlsGetAddr { dst, .. } => {
200 ensure_no_fact(vcode, dst.to_writable_reg().to_reg())
201 }
202 Inst::CoffTlsGetAddr { dst, tmp, .. } => {
203 ensure_no_fact(vcode, dst.to_writable_reg().to_reg())?;
204 ensure_no_fact(vcode, tmp.to_writable_reg().to_reg())?;
205 Ok(())
206 }
207
208 Inst::Unwind { .. } | Inst::DummyUse { .. } => Ok(()),
209
210 Inst::StackSwitchBasic { .. } => Err(PccError::UnimplementedInst),
211
212 Inst::LabelAddress { .. } => Err(PccError::UnimplementedInst),
213
214 Inst::External { .. } => Ok(()), }
216}
217
218fn check_load(
219 ctx: &FactContext,
220 dst: Option<Writable<Reg>>,
221 src: &SyntheticAmode,
222 vcode: &VCode<Inst>,
223 ty: Type,
224 to_bits: u16,
225) -> PccResult<Option<Fact>> {
226 let result_fact = dst.and_then(|dst| vcode.vreg_fact(dst.to_reg().into()));
227 let from_bits = u16::try_from(ty.bits()).unwrap();
228 check_mem(
229 ctx,
230 src,
231 vcode,
232 ty,
233 LoadOrStore::Load {
234 result_fact,
235 from_bits,
236 to_bits,
237 },
238 )
239}
240
241fn check_store(
242 ctx: &FactContext,
243 data: Option<Reg>,
244 dst: &SyntheticAmode,
245 vcode: &VCode<Inst>,
246 ty: Type,
247) -> PccResult<()> {
248 let stored_fact = data.and_then(|data| vcode.vreg_fact(data.into()));
249 check_mem(ctx, dst, vcode, ty, LoadOrStore::Store { stored_fact }).map(|_| ())
250}
251
252fn check_mem<'a>(
253 ctx: &FactContext,
254 amode: &SyntheticAmode,
255 vcode: &VCode<Inst>,
256 ty: Type,
257 op: LoadOrStore<'a>,
258) -> PccResult<Option<Fact>> {
259 let addr = match amode {
260 SyntheticAmode::Real(amode) if amode.get_flags().checked() => {
261 compute_addr(ctx, vcode, amode, 64).ok_or(PccError::MissingFact)?
262 }
263 _ => return Ok(None),
264 };
265
266 match op {
267 LoadOrStore::Load {
268 result_fact,
269 from_bits,
270 to_bits,
271 } => {
272 let loaded_fact = clamp_range(ctx, to_bits, from_bits, ctx.load(&addr, ty)?.cloned())?;
273 trace!(
274 "loaded_fact = {:?} result_fact = {:?}",
275 loaded_fact, result_fact
276 );
277 if ctx.subsumes_fact_optionals(loaded_fact.as_ref(), result_fact) {
278 Ok(loaded_fact.clone())
279 } else {
280 Err(PccError::UnsupportedFact)
281 }
282 }
283 LoadOrStore::Store { stored_fact } => {
284 ctx.store(&addr, ty, stored_fact)?;
285 Ok(None)
286 }
287 }
288}
289
290fn compute_addr(ctx: &FactContext, vcode: &VCode<Inst>, amode: &Amode, bits: u16) -> Option<Fact> {
291 trace!("compute_addr: {:?}", amode);
292 match *amode {
293 Amode::ImmReg { simm32, base, .. } => {
294 let base = get_fact_or_default(vcode, base, bits);
295 trace!("base = {:?}", base);
296 let simm32: i64 = simm32.into();
297 let simm32: u64 = simm32 as u64;
298 let offset = Fact::constant(bits, simm32);
299 let sum = ctx.add(&base, &offset, bits)?;
300 trace!("sum = {:?}", sum);
301 Some(sum)
302 }
303 Amode::ImmRegRegShift {
304 simm32,
305 base,
306 index,
307 shift,
308 ..
309 } => {
310 let base = get_fact_or_default(vcode, base.into(), bits);
311 let index = get_fact_or_default(vcode, index.into(), bits);
312 trace!("base = {:?} index = {:?}", base, index);
313 let shifted = ctx.shl(&index, bits, shift.into())?;
314 let sum = ctx.add(&base, &shifted, bits)?;
315 let simm32: i64 = simm32.into();
316 let simm32: u64 = simm32 as u64;
317 let offset = Fact::constant(bits, simm32);
318 let sum = ctx.add(&sum, &offset, bits)?;
319 trace!("sum = {:?}", sum);
320 Some(sum)
321 }
322 Amode::RipRelative { .. } => None,
323 }
324}