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::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/// Flow-state between facts.
33#[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    // We only persist flag state for one instruction, because we
47    // can't exhaustively enumerate all flags-effecting ops; so take
48    // the `cmp_state` here and perhaps use it below but don't let it
49    // remain.
50    let _cmp_flags = state.cmp_flags.take();
51
52    match vcode[inst_idx] {
53        Inst::Args { .. } => {
54            // Defs on the args have "axiomatic facts": we trust the
55            // ABI code to pass through the values unharmed, so the
56            // facts given to us in the CLIF should still be true.
57            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(()), // TODO: unsure what to do about this!
215    }
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}