Skip to content

Commit 095e469

Browse files
committed
Enable to handle some promoted constants
1 parent ad2262c commit 095e469

File tree

2 files changed

+110
-45
lines changed

2 files changed

+110
-45
lines changed

src/analyze/basic_block.rs

Lines changed: 101 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -125,11 +125,111 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
125125
clauses
126126
}
127127

128+
fn const_bytes_ty(
129+
&self,
130+
ty: mir_ty::Ty<'tcx>,
131+
alloc: mir::interpret::ConstAllocation,
132+
range: std::ops::Range<usize>,
133+
) -> PlaceType {
134+
let alloc = alloc.inner();
135+
let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter(range);
136+
match ty.kind() {
137+
mir_ty::TyKind::Str => {
138+
let content = std::str::from_utf8(bytes).unwrap();
139+
PlaceType::with_ty_and_term(
140+
rty::Type::string(),
141+
chc::Term::string(content.to_owned()),
142+
)
143+
}
144+
mir_ty::TyKind::Bool => {
145+
PlaceType::with_ty_and_term(rty::Type::bool(), chc::Term::bool(bytes[0] != 0))
146+
}
147+
mir_ty::Int(_) => {
148+
// TODO: see target endianess
149+
let val = match bytes.len() {
150+
1 => i8::from_ne_bytes(bytes.try_into().unwrap()) as i64,
151+
2 => i16::from_ne_bytes(bytes.try_into().unwrap()) as i64,
152+
4 => i32::from_ne_bytes(bytes.try_into().unwrap()) as i64,
153+
8 => i64::from_ne_bytes(bytes.try_into().unwrap()),
154+
_ => unimplemented!("const int bytes len: {}", bytes.len()),
155+
};
156+
PlaceType::with_ty_and_term(rty::Type::int(), chc::Term::int(val))
157+
}
158+
_ => unimplemented!("const bytes ty: {:?}", ty),
159+
}
160+
}
161+
162+
fn const_value_ty(&self, val: &mir::ConstValue<'tcx>, ty: &mir_ty::Ty<'tcx>) -> PlaceType {
163+
use mir::{interpret::Scalar, ConstValue, Mutability};
164+
match (ty.kind(), val) {
165+
(mir_ty::TyKind::Int(_), ConstValue::Scalar(Scalar::Int(val))) => {
166+
let val = val.try_to_int(val.size()).unwrap();
167+
PlaceType::with_ty_and_term(
168+
rty::Type::int(),
169+
chc::Term::int(val.try_into().unwrap()),
170+
)
171+
}
172+
(mir_ty::TyKind::Bool, ConstValue::Scalar(Scalar::Int(val))) => {
173+
PlaceType::with_ty_and_term(
174+
rty::Type::bool(),
175+
chc::Term::bool(val.try_to_bool().unwrap()),
176+
)
177+
}
178+
(
179+
mir_ty::TyKind::Ref(_, elem, Mutability::Not),
180+
ConstValue::Scalar(Scalar::Ptr(ptr, _)),
181+
) => {
182+
// Pointer::into_parts is OK for CtfeProvenance
183+
// in later version of rustc it has prov_and_relative_offset that ensures this
184+
let (prov, offset) = ptr.into_parts();
185+
let global_alloc = self.tcx.global_alloc(prov.alloc_id());
186+
match global_alloc {
187+
mir::interpret::GlobalAlloc::Memory(alloc) => {
188+
let layout = self
189+
.tcx
190+
.layout_of(mir_ty::ParamEnv::reveal_all().and(*elem))
191+
.unwrap();
192+
let size = layout.size;
193+
let range =
194+
offset.bytes() as usize..(offset.bytes() + size.bytes()) as usize;
195+
self.const_bytes_ty(*elem, alloc, range).immut()
196+
}
197+
_ => unimplemented!("const ptr alloc: {:?}", global_alloc),
198+
}
199+
}
200+
(mir_ty::TyKind::Ref(_, elem, Mutability::Not), ConstValue::Slice { data, meta }) => {
201+
let end = (*meta).try_into().unwrap();
202+
self.const_bytes_ty(*elem, *data, 0..end).immut()
203+
}
204+
_ => unimplemented!("const: {:?}, ty: {:?}", val, ty),
205+
}
206+
}
207+
208+
fn const_ty(&self, const_: &mir::Const<'tcx>) -> PlaceType {
209+
match const_ {
210+
mir::Const::Val(val, ty) => self.const_value_ty(val, ty),
211+
mir::Const::Unevaluated(unevaluated, ty) => {
212+
// since all constants are immutable in current setup,
213+
// it should be okay to evaluate them here on-the-fly
214+
let param_env = self.tcx.param_env(self.local_def_id);
215+
let val = self
216+
.tcx
217+
.const_eval_resolve(param_env, *unevaluated, None)
218+
.unwrap();
219+
self.const_value_ty(&val, ty)
220+
}
221+
_ => unimplemented!("const: {:?}", const_),
222+
}
223+
}
224+
128225
fn operand_type(&self, mut operand: Operand<'tcx>) -> PlaceType {
129226
if let Operand::Copy(p) | Operand::Move(p) = &mut operand {
130227
*p = self.elaborate_place(p);
131228
}
132-
let ty = self.env.operand_type(operand.clone());
229+
let ty = match &operand {
230+
Operand::Copy(place) | Operand::Move(place) => self.env.place_type(*place),
231+
Operand::Constant(operand) => self.const_ty(&operand.const_),
232+
};
133233
tracing::debug!(operand = ?operand, ty = %ty.display(), "operand_type");
134234
ty
135235
}

src/refine/env.rs

Lines changed: 9 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,7 @@ use std::collections::{BTreeMap, HashMap};
22

33
use pretty::{termcolor, Pretty};
44
use rustc_index::IndexVec;
5-
use rustc_middle::mir::{self, Local, Operand, Place, PlaceElem};
6-
use rustc_middle::ty as mir_ty;
5+
use rustc_middle::mir::{Local, Place, PlaceElem};
76
use rustc_target::abi::{FieldIdx, VariantIdx};
87

98
use crate::chc;
@@ -454,6 +453,14 @@ impl PlaceType {
454453
builder.build(ty, term)
455454
}
456455

456+
pub fn immut(self) -> PlaceType {
457+
let mut builder = PlaceTypeBuilder::default();
458+
let (inner_ty, inner_term) = builder.subsume(self);
459+
let ty = rty::PointerType::immut_to(inner_ty).into();
460+
let term = chc::Term::box_(inner_term);
461+
builder.build(ty, term)
462+
}
463+
457464
pub fn tuple(ptys: Vec<PlaceType>) -> PlaceType {
458465
let mut builder = PlaceTypeBuilder::default();
459466
let mut tys = Vec::new();
@@ -951,48 +958,6 @@ impl Env {
951958
self.var_type(local.into())
952959
}
953960

954-
pub fn operand_type(&self, operand: Operand<'_>) -> PlaceType {
955-
use mir::{interpret::Scalar, Const, ConstValue, Mutability};
956-
match operand {
957-
Operand::Copy(place) | Operand::Move(place) => self.place_type(place),
958-
Operand::Constant(operand) => {
959-
let Const::Val(val, ty) = operand.const_ else {
960-
unimplemented!("const: {:?}", operand.const_);
961-
};
962-
match (ty.kind(), val) {
963-
(mir_ty::TyKind::Int(_), ConstValue::Scalar(Scalar::Int(val))) => {
964-
let val = val.try_to_int(val.size()).unwrap();
965-
PlaceType::with_ty_and_term(
966-
rty::Type::int(),
967-
chc::Term::int(val.try_into().unwrap()),
968-
)
969-
}
970-
(mir_ty::TyKind::Bool, ConstValue::Scalar(Scalar::Int(val))) => {
971-
PlaceType::with_ty_and_term(
972-
rty::Type::bool(),
973-
chc::Term::bool(val.try_to_bool().unwrap()),
974-
)
975-
}
976-
(
977-
mir_ty::TyKind::Ref(_, elem, Mutability::Not),
978-
ConstValue::Slice { data, meta },
979-
) if matches!(elem.kind(), mir_ty::TyKind::Str) => {
980-
let end = meta.try_into().unwrap();
981-
let content = data
982-
.inner()
983-
.inspect_with_uninit_and_ptr_outside_interpreter(0..end);
984-
let content = std::str::from_utf8(content).unwrap();
985-
PlaceType::with_ty_and_term(
986-
rty::PointerType::immut_to(rty::Type::string()).into(),
987-
chc::Term::box_(chc::Term::string(content.to_owned())),
988-
)
989-
}
990-
_ => unimplemented!("const: {:?}, ty: {:?}", val, ty),
991-
}
992-
}
993-
}
994-
}
995-
996961
fn borrow_var(&mut self, var: Var, prophecy: TempVarIdx) -> PlaceType {
997962
match *self.flow_binding(var).expect("borrowing unbound var") {
998963
FlowBinding::Box(x) => {

0 commit comments

Comments
 (0)