cranelift_codegen/isa/x64/
pcc.rs

1//! Proof-carrying-code validation for x64 VCode.
2
3use crate::ir::pcc::*;
4use crate::ir::types::*;
5use crate::isa::x64::args::AvxOpcode;
6use crate::isa::x64::inst::args::{
7    AluRmiROpcode, Amode, Gpr, Imm8Reg, RegMem, RegMemImm, ShiftKind, SseOpcode, SyntheticAmode,
8    ToWritableReg, CC,
9};
10use crate::isa::x64::inst::Inst;
11use crate::machinst::pcc::*;
12use crate::machinst::{InsnIndex, VCode, VCodeConstantData};
13use crate::machinst::{Reg, Writable};
14use crate::trace;
15
16fn undefined_result(
17    ctx: &FactContext,
18    vcode: &mut VCode<Inst>,
19    dst: Writable<Gpr>,
20    reg_bits: u16,
21    result_bits: u16,
22) -> PccResult<()> {
23    check_output(ctx, vcode, dst.to_writable_reg(), &[], |_vcode| {
24        clamp_range(ctx, reg_bits, result_bits, None)
25    })
26}
27
28fn ensure_no_fact(vcode: &VCode<Inst>, reg: Reg) -> PccResult<()> {
29    if vcode.vreg_fact(reg.into()).is_some() {
30        Err(PccError::UnsupportedFact)
31    } else {
32        Ok(())
33    }
34}
35
36/// Flow-state between facts.
37#[derive(Clone, Debug, Default)]
38pub(crate) struct FactFlowState {
39    cmp_flags: Option<(Fact, Fact)>,
40}
41
42pub(crate) fn check(
43    ctx: &FactContext,
44    vcode: &mut VCode<Inst>,
45    inst_idx: InsnIndex,
46    state: &mut FactFlowState,
47) -> PccResult<()> {
48    trace!("Checking facts on inst: {:?}", vcode[inst_idx]);
49
50    // We only persist flag state for one instruction, because we
51    // can't exhaustively enumerate all flags-effecting ops; so take
52    // the `cmp_state` here and perhaps use it below but don't let it
53    // remain.
54    let cmp_flags = state.cmp_flags.take();
55
56    match vcode[inst_idx] {
57        Inst::Nop { .. } => Ok(()),
58
59        Inst::Args { .. } => {
60            // Defs on the args have "axiomatic facts": we trust the
61            // ABI code to pass through the values unharmed, so the
62            // facts given to us in the CLIF should still be true.
63            Ok(())
64        }
65
66        Inst::AluRmiR {
67            size,
68            op: AluRmiROpcode::Add,
69            src1,
70            ref src2,
71            dst,
72        } => match *<&RegMemImm>::from(src2) {
73            RegMemImm::Reg { reg: src2 } => {
74                let bits = size.to_bits().into();
75                check_binop(
76                    ctx,
77                    vcode,
78                    64,
79                    dst.to_writable_reg(),
80                    src1.to_reg(),
81                    src2,
82                    |src1, src2| clamp_range(ctx, 64, bits, ctx.add(src1, src2, bits)),
83                )
84            }
85            RegMemImm::Imm { simm32 } => {
86                let bits = size.to_bits().into();
87                check_unop(
88                    ctx,
89                    vcode,
90                    64,
91                    dst.to_writable_reg(),
92                    src1.to_reg(),
93                    |src1| {
94                        let simm32: i64 = simm32.into();
95                        clamp_range(ctx, 64, bits, ctx.offset(src1, bits, simm32))
96                    },
97                )
98            }
99            RegMemImm::Mem { ref addr } => {
100                let bits: u16 = size.to_bits().into();
101                let loaded = check_load(ctx, None, addr, vcode, size.to_type(), bits)?;
102                check_unop(ctx, vcode, 64, dst.to_writable_reg(), src1.into(), |src1| {
103                    let sum = loaded.and_then(|loaded| ctx.add(src1, &loaded, bits));
104                    clamp_range(ctx, 64, bits, sum)
105                })
106            }
107        },
108
109        Inst::AluRmiR {
110            size,
111            op: AluRmiROpcode::Sub,
112            src1,
113            ref src2,
114            dst,
115        } => match *<&RegMemImm>::from(src2) {
116            RegMemImm::Imm { simm32 } => {
117                let bits = size.to_bits().into();
118                check_unop(
119                    ctx,
120                    vcode,
121                    64,
122                    dst.to_writable_reg(),
123                    src1.to_reg(),
124                    |src1| {
125                        let simm32: i64 = simm32.into();
126                        clamp_range(ctx, 64, bits, ctx.offset(src1, bits, -simm32))
127                    },
128                )
129            }
130            RegMemImm::Reg { .. } => {
131                let bits: u16 = size.to_bits().into();
132                check_output(ctx, vcode, dst.to_writable_reg(), &[], |_vcode| {
133                    clamp_range(ctx, 64, bits, None)
134                })
135            }
136            RegMemImm::Mem { ref addr } => {
137                let loaded = check_load(ctx, None, addr, vcode, size.to_type(), 64)?;
138                check_output(ctx, vcode, dst.to_writable_reg(), &[], |_vcode| {
139                    clamp_range(ctx, 64, size.to_bits().into(), loaded)
140                })
141            }
142        },
143
144        Inst::AluRmiR {
145            size,
146            ref src2,
147            dst,
148            ..
149        } => match <&RegMemImm>::from(src2) {
150            RegMemImm::Mem { addr } => {
151                let loaded = check_load(ctx, None, addr, vcode, size.to_type(), 64)?;
152                check_output(ctx, vcode, dst.to_writable_reg(), &[], |_vcode| {
153                    clamp_range(ctx, 64, size.to_bits().into(), loaded)
154                })
155            }
156            RegMemImm::Reg { .. } | RegMemImm::Imm { .. } => {
157                undefined_result(ctx, vcode, dst, 64, size.to_bits().into())
158            }
159        },
160
161        Inst::AluRM {
162            size,
163            op: _,
164            ref src1_dst,
165            src2: _,
166            lock: _,
167        } => {
168            check_load(ctx, None, src1_dst, vcode, size.to_type(), 64)?;
169            check_store(ctx, None, src1_dst, vcode, size.to_type())
170        }
171
172        Inst::AluRmRVex {
173            size,
174            ref src2,
175            dst,
176            ..
177        } => match <&RegMem>::from(src2) {
178            RegMem::Mem { addr } => {
179                let loaded = check_load(ctx, None, addr, vcode, size.to_type(), 64)?;
180                check_output(ctx, vcode, dst.to_writable_reg(), &[], |_vcode| {
181                    clamp_range(ctx, 64, size.to_bits().into(), loaded)
182                })
183            }
184            RegMem::Reg { .. } => undefined_result(ctx, vcode, dst, 64, size.to_bits().into()),
185        },
186
187        Inst::AluConstOp {
188            op: AluRmiROpcode::Xor,
189            dst,
190            ..
191        } => check_output(ctx, vcode, dst.to_writable_reg(), &[], |_vcode| {
192            Ok(Some(Fact::constant(64, 0)))
193        }),
194
195        Inst::AluConstOp { dst, .. } => undefined_result(ctx, vcode, dst, 64, 64),
196
197        Inst::UnaryRmR {
198            size, ref src, dst, ..
199        }
200        | Inst::UnaryRmRVex {
201            size, ref src, dst, ..
202        }
203        | Inst::UnaryRmRImmVex {
204            size, ref src, dst, ..
205        } => match <&RegMem>::from(src) {
206            RegMem::Mem { addr } => {
207                check_load(ctx, None, addr, vcode, size.to_type(), 64)?;
208                check_output(ctx, vcode, dst.to_writable_reg(), &[], |_vcode| {
209                    clamp_range(ctx, 64, size.to_bits().into(), None)
210                })
211            }
212            RegMem::Reg { .. } => undefined_result(ctx, vcode, dst, 64, size.to_bits().into()),
213        },
214
215        Inst::Not { size, dst, .. } | Inst::Neg { size, dst, .. } => {
216            undefined_result(ctx, vcode, dst, 64, size.to_bits().into())
217        }
218
219        Inst::Div {
220            size,
221            ref divisor,
222            dst_quotient,
223            dst_remainder,
224            ..
225        } => {
226            match <&RegMem>::from(divisor) {
227                RegMem::Mem { addr } => {
228                    check_load(ctx, None, addr, vcode, size.to_type(), 64)?;
229                }
230                RegMem::Reg { .. } => {}
231            }
232            undefined_result(ctx, vcode, dst_quotient, 64, 64)?;
233            undefined_result(ctx, vcode, dst_remainder, 64, 64)?;
234            Ok(())
235        }
236        Inst::Div8 {
237            dst, ref divisor, ..
238        } => {
239            match <&RegMem>::from(divisor) {
240                RegMem::Mem { addr } => {
241                    check_load(ctx, None, addr, vcode, I8, 64)?;
242                }
243                RegMem::Reg { .. } => {}
244            }
245            // 64-bit result width because result may be negative
246            // hence high bits set.
247            undefined_result(ctx, vcode, dst, 64, 64)?;
248            Ok(())
249        }
250        Inst::Mul {
251            size,
252            dst_lo,
253            dst_hi,
254            ref src2,
255            ..
256        }
257        | Inst::MulX {
258            size,
259            dst_lo,
260            dst_hi,
261            ref src2,
262            ..
263        } => {
264            match <&RegMem>::from(src2) {
265                RegMem::Mem { addr } => {
266                    check_load(ctx, None, addr, vcode, size.to_type(), 64)?;
267                }
268                RegMem::Reg { .. } => {}
269            }
270            undefined_result(ctx, vcode, dst_lo, 64, size.to_bits().into())?;
271            undefined_result(ctx, vcode, dst_hi, 64, size.to_bits().into())?;
272            Ok(())
273        }
274        Inst::Mul8 { dst, ref src2, .. } => {
275            match <&RegMem>::from(src2) {
276                RegMem::Mem { addr } => {
277                    check_load(ctx, None, addr, vcode, I8, 64)?;
278                }
279                RegMem::Reg { .. } => {}
280            }
281            undefined_result(ctx, vcode, dst, 64, 16)?;
282            Ok(())
283        }
284        Inst::IMul {
285            size,
286            dst,
287            ref src2,
288            ..
289        } => {
290            match <&RegMem>::from(src2) {
291                RegMem::Mem { addr } => {
292                    check_load(ctx, None, addr, vcode, size.to_type(), 64)?;
293                }
294                RegMem::Reg { .. } => {}
295            }
296            undefined_result(ctx, vcode, dst, 64, size.to_bits().into())?;
297            Ok(())
298        }
299        Inst::IMulImm {
300            size,
301            dst,
302            ref src1,
303            ..
304        } => {
305            match <&RegMem>::from(src1) {
306                RegMem::Mem { addr } => {
307                    check_load(ctx, None, addr, vcode, size.to_type(), 64)?;
308                }
309                RegMem::Reg { .. } => {}
310            }
311            undefined_result(ctx, vcode, dst, 64, size.to_bits().into())?;
312            Ok(())
313        }
314        Inst::CheckedSRemSeq {
315            dst_quotient,
316            dst_remainder,
317            ..
318        } => {
319            undefined_result(ctx, vcode, dst_quotient, 64, 64)?;
320            undefined_result(ctx, vcode, dst_remainder, 64, 64)?;
321            Ok(())
322        }
323
324        Inst::CheckedSRemSeq8 { dst, .. } => undefined_result(ctx, vcode, dst, 64, 64),
325
326        Inst::SignExtendData { dst, .. } => undefined_result(ctx, vcode, dst, 64, 64),
327
328        Inst::Imm { simm64, dst, .. } => {
329            check_output(ctx, vcode, dst.to_writable_reg(), &[], |_vcode| {
330                Ok(Some(Fact::constant(64, simm64)))
331            })
332        }
333
334        Inst::MovRR { size, dst, .. } => {
335            undefined_result(ctx, vcode, dst, 64, size.to_bits().into())
336        }
337
338        Inst::MovFromPReg { dst, .. } => undefined_result(ctx, vcode, dst, 64, 64),
339        Inst::MovToPReg { .. } => Ok(()),
340
341        Inst::MovzxRmR {
342            ref ext_mode,
343            ref src,
344            dst,
345        } => {
346            let from_bytes: u16 = ext_mode.src_size().into();
347            let to_bytes: u16 = ext_mode.dst_size().into();
348            match <&RegMem>::from(src) {
349                RegMem::Reg { reg } => {
350                    check_unop(ctx, vcode, 64, dst.to_writable_reg(), *reg, |src| {
351                        clamp_range(ctx, 64, from_bytes * 8, Some(src.clone()))
352                    })
353                }
354                RegMem::Mem { addr } => {
355                    let loaded = check_load(
356                        ctx,
357                        Some(dst.to_writable_reg()),
358                        addr,
359                        vcode,
360                        ext_mode.src_type(),
361                        64,
362                    )?;
363                    check_output(ctx, vcode, dst.to_writable_reg(), &[], |_vcode| {
364                        let extended = loaded
365                            .and_then(|loaded| ctx.uextend(&loaded, from_bytes * 8, to_bytes * 8));
366                        clamp_range(ctx, 64, from_bytes * 8, extended)
367                    })
368                }
369            }
370        }
371
372        Inst::Mov64MR { ref src, dst } => {
373            check_load(ctx, Some(dst.to_writable_reg()), src, vcode, I64, 64)?;
374            Ok(())
375        }
376
377        Inst::LoadEffectiveAddress {
378            ref addr,
379            dst,
380            size,
381        } => {
382            let addr = addr.clone();
383            let bits: u16 = size.to_bits().into();
384            check_output(ctx, vcode, dst.to_writable_reg(), &[], |vcode| {
385                let fact = if let SyntheticAmode::Real(amode) = &addr {
386                    compute_addr(ctx, vcode, amode, bits)
387                } else {
388                    None
389                };
390                clamp_range(ctx, 64, bits, fact)
391            })
392        }
393
394        Inst::MovsxRmR {
395            ref ext_mode,
396            ref src,
397            dst,
398        } => {
399            match <&RegMem>::from(src) {
400                RegMem::Mem { addr } => {
401                    check_load(ctx, None, addr, vcode, ext_mode.src_type(), 64)?;
402                }
403                RegMem::Reg { .. } => {}
404            }
405            undefined_result(ctx, vcode, dst, 64, 64)
406        }
407
408        Inst::MovImmM { size, ref dst, .. } => check_store(ctx, None, dst, vcode, size.to_type()),
409
410        Inst::MovRM { size, src, ref dst } => {
411            check_store(ctx, Some(src.to_reg()), dst, vcode, size.to_type())
412        }
413
414        Inst::ShiftR {
415            size,
416            kind: ShiftKind::ShiftLeft,
417            src,
418            ref num_bits,
419            dst,
420        } => match num_bits.as_imm8_reg() {
421            &Imm8Reg::Imm8 { imm } => {
422                check_unop(ctx, vcode, 64, dst.to_writable_reg(), src.to_reg(), |src| {
423                    clamp_range(
424                        ctx,
425                        64,
426                        size.to_bits().into(),
427                        ctx.shl(src, size.to_bits().into(), imm.into()),
428                    )
429                })
430            }
431            Imm8Reg::Reg { .. } => undefined_result(ctx, vcode, dst, 64, size.to_bits().into()),
432        },
433
434        Inst::ShiftR { size, dst, .. } => {
435            undefined_result(ctx, vcode, dst, 64, size.to_bits().into())
436        }
437
438        Inst::XmmRmiReg { dst, ref src2, .. } => {
439            match <&RegMemImm>::from(src2) {
440                RegMemImm::Mem { addr } => {
441                    check_load(ctx, None, addr, vcode, I8X16, 128)?;
442                }
443                _ => {}
444            }
445            ensure_no_fact(vcode, dst.to_writable_reg().to_reg())
446        }
447
448        Inst::CmpRmiR {
449            size,
450            src1,
451            ref src2,
452            ..
453        } => match <&RegMemImm>::from(src2) {
454            RegMemImm::Mem {
455                addr: SyntheticAmode::ConstantOffset(k),
456            } => {
457                match vcode.constants.get(*k) {
458                    VCodeConstantData::U64(bytes) => {
459                        let value = u64::from_le_bytes(*bytes);
460                        let lhs = get_fact_or_default(vcode, src1.to_reg(), 64);
461                        let rhs = Fact::constant(64, value);
462                        state.cmp_flags = Some((lhs, rhs));
463                    }
464                    _ => {}
465                }
466                Ok(())
467            }
468            RegMemImm::Mem { addr } => {
469                if let Some(rhs) = check_load(ctx, None, addr, vcode, size.to_type(), 64)? {
470                    let lhs = get_fact_or_default(vcode, src1.to_reg(), 64);
471                    state.cmp_flags = Some((lhs, rhs));
472                }
473                Ok(())
474            }
475            RegMemImm::Reg { reg } => {
476                let rhs = get_fact_or_default(vcode, *reg, 64);
477                let lhs = get_fact_or_default(vcode, src1.to_reg(), 64);
478                state.cmp_flags = Some((lhs, rhs));
479                Ok(())
480            }
481            RegMemImm::Imm { simm32 } => {
482                let lhs = get_fact_or_default(vcode, src1.to_reg(), 64);
483                let rhs = Fact::constant(64, (*simm32 as i32) as i64 as u64);
484                state.cmp_flags = Some((lhs, rhs));
485                Ok(())
486            }
487        },
488
489        Inst::Setcc { dst, .. } => undefined_result(ctx, vcode, dst, 64, 64),
490
491        Inst::Bswap { dst, .. } => undefined_result(ctx, vcode, dst, 64, 64),
492
493        Inst::Cmove {
494            size,
495            dst,
496            ref consequent,
497            alternative,
498            cc,
499            ..
500        } => match <&RegMem>::from(consequent) {
501            RegMem::Mem { addr } => {
502                check_load(ctx, None, addr, vcode, size.to_type(), 64)?;
503                Ok(())
504            }
505            RegMem::Reg { reg } if (cc == CC::NB || cc == CC::NBE) && cmp_flags.is_some() => {
506                let (cmp_lhs, cmp_rhs) = cmp_flags.unwrap();
507                trace!("lhs = {:?} rhs = {:?}", cmp_lhs, cmp_rhs);
508                let reg = *reg;
509                check_output(ctx, vcode, dst.to_writable_reg(), &[], |vcode| {
510                    // See comments in aarch64::pcc CSel for more details on this.
511                    let in_true = get_fact_or_default(vcode, reg, 64);
512                    let in_true_kind = match cc {
513                        CC::NB => InequalityKind::Loose,
514                        CC::NBE => InequalityKind::Strict,
515                        _ => unreachable!(),
516                    };
517                    let in_true = ctx.apply_inequality(&in_true, &cmp_lhs, &cmp_rhs, in_true_kind);
518                    let in_false = get_fact_or_default(vcode, alternative.to_reg(), 64);
519                    let in_false_kind = match cc {
520                        CC::NB => InequalityKind::Strict,
521                        CC::NBE => InequalityKind::Loose,
522                        _ => unreachable!(),
523                    };
524                    let in_false =
525                        ctx.apply_inequality(&in_false, &cmp_rhs, &cmp_lhs, in_false_kind);
526                    let union = ctx.union(&in_true, &in_false);
527                    clamp_range(ctx, 64, 64, union)
528                })
529            }
530            _ => undefined_result(ctx, vcode, dst, 64, 64),
531        },
532
533        Inst::XmmCmove { dst, .. } => ensure_no_fact(vcode, dst.to_writable_reg().to_reg()),
534
535        Inst::Push64 { ref src } => match <&RegMemImm>::from(src) {
536            RegMemImm::Mem { addr } => {
537                check_load(ctx, None, addr, vcode, I64, 64)?;
538                Ok(())
539            }
540            RegMemImm::Reg { .. } | RegMemImm::Imm { .. } => Ok(()),
541        },
542
543        Inst::Pop64 { dst } => undefined_result(ctx, vcode, dst, 64, 64),
544
545        Inst::StackProbeLoop { tmp, .. } => ensure_no_fact(vcode, tmp.to_reg()),
546
547        Inst::XmmRmR { dst, ref src2, .. }
548        | Inst::XmmRmRBlend { dst, ref src2, .. }
549        | Inst::XmmUnaryRmR {
550            dst, src: ref src2, ..
551        }
552        | Inst::XmmUnaryRmRImm {
553            dst, src: ref src2, ..
554        } => {
555            match <&RegMem>::from(src2) {
556                RegMem::Mem { addr } => {
557                    check_load(ctx, None, addr, vcode, I8X16, 128)?;
558                }
559                RegMem::Reg { .. } => {}
560            }
561            ensure_no_fact(vcode, dst.to_writable_reg().to_reg())
562        }
563
564        Inst::XmmUnaryRmRUnaligned {
565            dst,
566            ref src,
567            op: SseOpcode::Movss,
568            ..
569        } => {
570            match <&RegMem>::from(src) {
571                RegMem::Mem { addr } => {
572                    check_load(ctx, None, addr, vcode, F32, 32)?;
573                }
574                RegMem::Reg { .. } => {}
575            }
576            ensure_no_fact(vcode, dst.to_writable_reg().to_reg())
577        }
578        Inst::XmmUnaryRmRUnaligned {
579            dst,
580            ref src,
581            op: SseOpcode::Movsd,
582            ..
583        } => {
584            match <&RegMem>::from(src) {
585                RegMem::Mem { addr } => {
586                    check_load(ctx, None, addr, vcode, F64, 64)?;
587                }
588                RegMem::Reg { .. } => {}
589            }
590            ensure_no_fact(vcode, dst.to_writable_reg().to_reg())
591        }
592
593        // NOTE: it's assumed that all of these cases perform 128-bit loads, but this hasn't been
594        // verified. The effect of this will be spurious PCC failures when these instructions are
595        // involved.
596        Inst::XmmRmRUnaligned { dst, ref src2, .. }
597        | Inst::XmmRmREvex { dst, ref src2, .. }
598        | Inst::XmmUnaryRmRImmEvex {
599            dst, src: ref src2, ..
600        }
601        | Inst::XmmUnaryRmRUnaligned {
602            dst, src: ref src2, ..
603        }
604        | Inst::XmmUnaryRmREvex {
605            dst, src: ref src2, ..
606        }
607        | Inst::XmmRmREvex3 {
608            dst,
609            src3: ref src2,
610            ..
611        } => {
612            match <&RegMem>::from(src2) {
613                RegMem::Mem { addr } => {
614                    check_load(ctx, None, addr, vcode, I8X16, 128)?;
615                }
616                RegMem::Reg { .. } => {}
617            }
618            ensure_no_fact(vcode, dst.to_writable_reg().to_reg())
619        }
620
621        Inst::XmmRmRImmVex {
622            op, dst, ref src2, ..
623        }
624        | Inst::XmmRmRVex3 {
625            op,
626            dst,
627            src3: ref src2,
628            ..
629        }
630        | Inst::XmmRmRBlendVex {
631            op, dst, ref src2, ..
632        }
633        | Inst::XmmUnaryRmRVex {
634            op,
635            dst,
636            src: ref src2,
637            ..
638        }
639        | Inst::XmmUnaryRmRImmVex {
640            op,
641            dst,
642            src: ref src2,
643            ..
644        } => {
645            let (ty, size) = match op {
646                AvxOpcode::Vmovss => (F32, 32),
647                AvxOpcode::Vmovsd => (F64, 64),
648                AvxOpcode::Vpinsrb => (I8, 8),
649                AvxOpcode::Vpinsrw => (I16, 16),
650                AvxOpcode::Vpinsrd => (I32, 32),
651                AvxOpcode::Vpinsrq => (I64, 64),
652
653                // We assume all other operations happen on 128-bit values.
654                _ => (I8X16, 128),
655            };
656
657            match <&RegMem>::from(src2) {
658                RegMem::Mem { addr } => {
659                    check_load(ctx, None, addr, vcode, ty, size)?;
660                }
661                RegMem::Reg { .. } => {}
662            }
663            ensure_no_fact(vcode, dst.to_writable_reg().to_reg())
664        }
665
666        Inst::XmmRmiRVex { dst, ref src2, .. } => {
667            match <&RegMemImm>::from(src2) {
668                RegMemImm::Mem { addr } => {
669                    check_load(ctx, None, addr, vcode, I8X16, 128)?;
670                }
671                RegMemImm::Reg { .. } | RegMemImm::Imm { .. } => {}
672            }
673            ensure_no_fact(vcode, dst.to_writable_reg().to_reg())
674        }
675
676        Inst::XmmVexPinsr { dst, ref src2, .. } => {
677            match <&RegMem>::from(src2) {
678                RegMem::Mem { addr } => {
679                    check_load(ctx, None, addr, vcode, I64, 64)?;
680                }
681                RegMem::Reg { .. } => {}
682            }
683            ensure_no_fact(vcode, dst.to_writable_reg().to_reg())
684        }
685
686        Inst::XmmMovRMVex { ref dst, .. } | Inst::XmmMovRMImmVex { ref dst, .. } => {
687            check_store(ctx, None, dst, vcode, I8X16)
688        }
689
690        Inst::XmmToGprImmVex { dst, .. } => ensure_no_fact(vcode, dst.to_writable_reg().to_reg()),
691
692        Inst::GprToXmmVex { dst, ref src, .. } | Inst::GprToXmm { dst, ref src, .. } => {
693            match <&RegMem>::from(src) {
694                RegMem::Mem { addr } => {
695                    check_load(ctx, None, addr, vcode, I64, 64)?;
696                }
697                RegMem::Reg { .. } => {}
698            }
699            ensure_no_fact(vcode, dst.to_writable_reg().to_reg())
700        }
701
702        Inst::XmmToGprVex { dst, .. } => undefined_result(ctx, vcode, dst, 64, 64),
703
704        Inst::XmmMovRM {
705            ref dst,
706            op: SseOpcode::Movss,
707            ..
708        } => {
709            check_store(ctx, None, dst, vcode, F32)?;
710            Ok(())
711        }
712
713        Inst::XmmMovRM {
714            ref dst,
715            op: SseOpcode::Movsd,
716            ..
717        } => {
718            check_store(ctx, None, dst, vcode, F64)?;
719            Ok(())
720        }
721
722        Inst::XmmMovRM { ref dst, .. } | Inst::XmmMovRMImm { ref dst, .. } => {
723            check_store(ctx, None, dst, vcode, I8X16)?;
724            Ok(())
725        }
726
727        Inst::XmmToGpr { dst, .. } | Inst::XmmToGprImm { dst, .. } => {
728            undefined_result(ctx, vcode, dst, 64, 64)
729        }
730
731        Inst::CvtIntToFloat { dst, ref src2, .. }
732        | Inst::CvtIntToFloatVex { dst, ref src2, .. } => {
733            match <&RegMem>::from(src2) {
734                RegMem::Mem { addr } => {
735                    check_load(ctx, None, addr, vcode, I64, 64)?;
736                }
737                RegMem::Reg { .. } => {}
738            }
739            ensure_no_fact(vcode, dst.to_writable_reg().to_reg())
740        }
741
742        Inst::CvtUint64ToFloatSeq {
743            dst,
744            tmp_gpr1,
745            tmp_gpr2,
746            ..
747        } => {
748            ensure_no_fact(vcode, dst.to_writable_reg().to_reg())?;
749            ensure_no_fact(vcode, tmp_gpr1.to_writable_reg().to_reg())?;
750            ensure_no_fact(vcode, tmp_gpr2.to_writable_reg().to_reg())?;
751            Ok(())
752        }
753
754        Inst::CvtFloatToSintSeq {
755            dst,
756            tmp_gpr,
757            tmp_xmm,
758            ..
759        } => {
760            undefined_result(ctx, vcode, dst, 64, 64)?;
761            ensure_no_fact(vcode, tmp_gpr.to_writable_reg().to_reg())?;
762            ensure_no_fact(vcode, tmp_xmm.to_writable_reg().to_reg())?;
763            Ok(())
764        }
765
766        Inst::CvtFloatToUintSeq {
767            dst,
768            tmp_gpr,
769            tmp_xmm,
770            tmp_xmm2,
771            ..
772        } => {
773            undefined_result(ctx, vcode, dst, 64, 64)?;
774            ensure_no_fact(vcode, tmp_gpr.to_writable_reg().to_reg())?;
775            ensure_no_fact(vcode, tmp_xmm.to_writable_reg().to_reg())?;
776            ensure_no_fact(vcode, tmp_xmm2.to_writable_reg().to_reg())?;
777            Ok(())
778        }
779
780        Inst::XmmMinMaxSeq { dst, .. } => ensure_no_fact(vcode, dst.to_writable_reg().to_reg()),
781
782        Inst::XmmCmpRmR {
783            ref src1, ref src2, ..
784        } => {
785            match <&RegMem>::from(src2) {
786                RegMem::Mem { addr } => {
787                    check_load(ctx, None, addr, vcode, I8X16, 128)?;
788                }
789                RegMem::Reg { .. } => {}
790            }
791            ensure_no_fact(vcode, src1.to_reg())
792        }
793
794        Inst::XmmRmRImm {
795            dst,
796            ref src2,
797            size,
798            op,
799            ..
800        } if op.has_scalar_src2() => {
801            match <&RegMem>::from(src2) {
802                RegMem::Mem { addr } => {
803                    check_load(
804                        ctx,
805                        None,
806                        addr,
807                        vcode,
808                        size.to_type(),
809                        size.to_bits().into(),
810                    )?;
811                }
812                RegMem::Reg { .. } => {}
813            }
814            ensure_no_fact(vcode, dst.to_reg())
815        }
816
817        Inst::XmmRmRImm { dst, ref src2, .. } => {
818            match <&RegMem>::from(src2) {
819                RegMem::Mem { addr } => {
820                    check_load(ctx, None, addr, vcode, I8X16, 128)?;
821                }
822                RegMem::Reg { .. } => {}
823            }
824            ensure_no_fact(vcode, dst.to_reg())
825        }
826
827        Inst::XmmCmpRmRVex {
828            ref src1, ref src2, ..
829        } => {
830            match <&RegMem>::from(src2) {
831                RegMem::Mem { addr } => {
832                    check_load(ctx, None, addr, vcode, F32, 32)?;
833                }
834                RegMem::Reg { .. } => {}
835            }
836            ensure_no_fact(vcode, src1.to_reg())
837        }
838
839        Inst::CallKnown { .. }
840        | Inst::ReturnCallKnown { .. }
841        | Inst::JmpKnown { .. }
842        | Inst::Ret { .. }
843        | Inst::WinchJmpIf { .. }
844        | Inst::JmpCond { .. }
845        | Inst::JmpCondOr { .. }
846        | Inst::TrapIf { .. }
847        | Inst::TrapIfAnd { .. }
848        | Inst::TrapIfOr { .. }
849        | Inst::Hlt {}
850        | Inst::Ud2 { .. } => Ok(()),
851        Inst::Rets { .. } => Ok(()),
852
853        Inst::ReturnCallUnknown { .. } => Ok(()),
854
855        Inst::CallUnknown { ref info } => match <&RegMem>::from(&info.dest) {
856            RegMem::Mem { addr } => {
857                check_load(ctx, None, addr, vcode, I64, 64)?;
858                Ok(())
859            }
860            RegMem::Reg { .. } => Ok(()),
861        },
862        Inst::JmpUnknown {
863            target: ref dest, ..
864        } => match <&RegMem>::from(dest) {
865            RegMem::Mem { addr } => {
866                check_load(ctx, None, addr, vcode, I64, 64)?;
867                Ok(())
868            }
869            RegMem::Reg { .. } => Ok(()),
870        },
871
872        Inst::JmpTableSeq { tmp1, tmp2, .. } => {
873            ensure_no_fact(vcode, tmp1.to_reg())?;
874            ensure_no_fact(vcode, tmp2.to_reg())?;
875            Ok(())
876        }
877
878        Inst::LoadExtName { dst, .. } => {
879            ensure_no_fact(vcode, dst.to_reg())?;
880            Ok(())
881        }
882
883        Inst::LockCmpxchg {
884            ref mem, dst_old, ..
885        } => {
886            ensure_no_fact(vcode, dst_old.to_reg())?;
887            check_store(ctx, None, mem, vcode, I64)?;
888            Ok(())
889        }
890
891        Inst::LockCmpxchg16b {
892            ref mem,
893            dst_old_low,
894            dst_old_high,
895            ..
896        } => {
897            ensure_no_fact(vcode, dst_old_low.to_reg())?;
898            ensure_no_fact(vcode, dst_old_high.to_reg())?;
899            check_store(ctx, None, mem, vcode, I128)?;
900            Ok(())
901        }
902
903        Inst::LockXadd {
904            size,
905            ref mem,
906            dst_old,
907            operand: _,
908        } => {
909            ensure_no_fact(vcode, dst_old.to_reg())?;
910            check_store(ctx, None, mem, vcode, size.to_type())?;
911            Ok(())
912        }
913
914        Inst::Xchg {
915            size,
916            ref mem,
917            dst_old,
918            operand: _,
919        } => {
920            ensure_no_fact(vcode, dst_old.to_reg())?;
921            check_store(ctx, None, mem, vcode, size.to_type())?;
922            Ok(())
923        }
924
925        Inst::AtomicRmwSeq {
926            ref mem,
927            temp,
928            dst_old,
929            ..
930        } => {
931            ensure_no_fact(vcode, dst_old.to_reg())?;
932            ensure_no_fact(vcode, temp.to_reg())?;
933            check_store(ctx, None, mem, vcode, I64)?;
934            Ok(())
935        }
936
937        Inst::Atomic128RmwSeq {
938            ref mem,
939            temp_low,
940            temp_high,
941            dst_old_low,
942            dst_old_high,
943            ..
944        } => {
945            ensure_no_fact(vcode, dst_old_low.to_reg())?;
946            ensure_no_fact(vcode, dst_old_high.to_reg())?;
947            ensure_no_fact(vcode, temp_low.to_reg())?;
948            ensure_no_fact(vcode, temp_high.to_reg())?;
949            check_store(ctx, None, mem, vcode, I128)?;
950            Ok(())
951        }
952
953        Inst::Atomic128XchgSeq {
954            ref mem,
955            dst_old_low,
956            dst_old_high,
957            ..
958        } => {
959            ensure_no_fact(vcode, dst_old_low.to_reg())?;
960            ensure_no_fact(vcode, dst_old_high.to_reg())?;
961            check_store(ctx, None, mem, vcode, I128)?;
962            Ok(())
963        }
964
965        Inst::Fence { .. } => Ok(()),
966
967        Inst::XmmUninitializedValue { dst } => {
968            ensure_no_fact(vcode, dst.to_writable_reg().to_reg())
969        }
970
971        Inst::ElfTlsGetAddr { dst, .. } | Inst::MachOTlsGetAddr { dst, .. } => {
972            ensure_no_fact(vcode, dst.to_writable_reg().to_reg())
973        }
974        Inst::CoffTlsGetAddr { dst, tmp, .. } => {
975            ensure_no_fact(vcode, dst.to_writable_reg().to_reg())?;
976            ensure_no_fact(vcode, tmp.to_writable_reg().to_reg())?;
977            Ok(())
978        }
979
980        Inst::Unwind { .. } | Inst::DummyUse { .. } => Ok(()),
981
982        Inst::StackSwitchBasic { .. } => Err(PccError::UnimplementedInst),
983
984        Inst::External { .. } => Ok(()), // TODO: unsure what to do about this!
985    }
986}
987
988fn check_load(
989    ctx: &FactContext,
990    dst: Option<Writable<Reg>>,
991    src: &SyntheticAmode,
992    vcode: &VCode<Inst>,
993    ty: Type,
994    to_bits: u16,
995) -> PccResult<Option<Fact>> {
996    let result_fact = dst.and_then(|dst| vcode.vreg_fact(dst.to_reg().into()));
997    let from_bits = u16::try_from(ty.bits()).unwrap();
998    check_mem(
999        ctx,
1000        src,
1001        vcode,
1002        ty,
1003        LoadOrStore::Load {
1004            result_fact,
1005            from_bits,
1006            to_bits,
1007        },
1008    )
1009}
1010
1011fn check_store(
1012    ctx: &FactContext,
1013    data: Option<Reg>,
1014    dst: &SyntheticAmode,
1015    vcode: &VCode<Inst>,
1016    ty: Type,
1017) -> PccResult<()> {
1018    let stored_fact = data.and_then(|data| vcode.vreg_fact(data.into()));
1019    check_mem(ctx, dst, vcode, ty, LoadOrStore::Store { stored_fact }).map(|_| ())
1020}
1021
1022fn check_mem<'a>(
1023    ctx: &FactContext,
1024    amode: &SyntheticAmode,
1025    vcode: &VCode<Inst>,
1026    ty: Type,
1027    op: LoadOrStore<'a>,
1028) -> PccResult<Option<Fact>> {
1029    let addr = match amode {
1030        SyntheticAmode::Real(amode) if amode.get_flags().checked() => {
1031            compute_addr(ctx, vcode, amode, 64).ok_or(PccError::MissingFact)?
1032        }
1033        _ => return Ok(None),
1034    };
1035
1036    match op {
1037        LoadOrStore::Load {
1038            result_fact,
1039            from_bits,
1040            to_bits,
1041        } => {
1042            let loaded_fact = clamp_range(ctx, to_bits, from_bits, ctx.load(&addr, ty)?.cloned())?;
1043            trace!(
1044                "loaded_fact = {:?} result_fact = {:?}",
1045                loaded_fact,
1046                result_fact
1047            );
1048            if ctx.subsumes_fact_optionals(loaded_fact.as_ref(), result_fact) {
1049                Ok(loaded_fact.clone())
1050            } else {
1051                Err(PccError::UnsupportedFact)
1052            }
1053        }
1054        LoadOrStore::Store { stored_fact } => {
1055            ctx.store(&addr, ty, stored_fact)?;
1056            Ok(None)
1057        }
1058    }
1059}
1060
1061fn compute_addr(ctx: &FactContext, vcode: &VCode<Inst>, amode: &Amode, bits: u16) -> Option<Fact> {
1062    trace!("compute_addr: {:?}", amode);
1063    match *amode {
1064        Amode::ImmReg { simm32, base, .. } => {
1065            let base = get_fact_or_default(vcode, base, bits);
1066            trace!("base = {:?}", base);
1067            let simm32: i64 = simm32.into();
1068            let simm32: u64 = simm32 as u64;
1069            let offset = Fact::constant(bits, simm32);
1070            let sum = ctx.add(&base, &offset, bits)?;
1071            trace!("sum = {:?}", sum);
1072            Some(sum)
1073        }
1074        Amode::ImmRegRegShift {
1075            simm32,
1076            base,
1077            index,
1078            shift,
1079            ..
1080        } => {
1081            let base = get_fact_or_default(vcode, base.into(), bits);
1082            let index = get_fact_or_default(vcode, index.into(), bits);
1083            trace!("base = {:?} index = {:?}", base, index);
1084            let shifted = ctx.shl(&index, bits, shift.into())?;
1085            let sum = ctx.add(&base, &shifted, bits)?;
1086            let simm32: i64 = simm32.into();
1087            let simm32: u64 = simm32 as u64;
1088            let offset = Fact::constant(bits, simm32);
1089            let sum = ctx.add(&sum, &offset, bits)?;
1090            trace!("sum = {:?}", sum);
1091            Some(sum)
1092        }
1093        Amode::RipRelative { .. } => None,
1094    }
1095}