Skip to content

Commit 5996109

Browse files
coord-ecoord-e
committed
Introduce PlaceTypeBuilder to simplify PlaceType construction
1 parent 43ba71b commit 5996109

File tree

3 files changed

+206
-347
lines changed

3 files changed

+206
-347
lines changed

‎src/analyze/basic_block.rs‎

Lines changed: 80 additions & 70 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ use crate::analyze;
1313
use crate::chc;
1414
use crate::pretty::PrettyDisplayExt as _;
1515
use crate::refine::{
16-
self, Assumption, BasicBlockType, Env, PlaceType, PlaceTypeVar, TempVarIdx,
16+
self, Assumption, BasicBlockType, Env, PlaceType, PlaceTypeBuilder, PlaceTypeVar, TempVarIdx,
1717
TemplateTypeGenerator, UnrefinedTypeGenerator, Var,
1818
};
1919
use crate::rty::{
@@ -138,12 +138,15 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
138138
Rvalue::Use(operand) => self.operand_type(operand),
139139
Rvalue::UnaryOp(op, operand) => {
140140
let operand_ty = self.operand_type(operand);
141-
match (&operand_ty.ty, op) {
141+
142+
let mut builder = PlaceTypeBuilder::default();
143+
let (operand_ty, operand_term) = builder.subsume(operand_ty);
144+
match (&operand_ty, op) {
142145
(rty::Type::Bool, mir::UnOp::Not) => {
143-
operand_ty.replace(|_, term| (rty::Type::Bool, term.not()))
146+
builder.build(rty::Type::Bool, operand_term.not())
144147
}
145148
(rty::Type::Int, mir::UnOp::Neg) => {
146-
operand_ty.replace(|_, term| (rty::Type::Int, term.neg()))
149+
builder.build(rty::Type::Int, operand_term.neg())
147150
}
148151
_ => unimplemented!("ty={}, op={:?}", operand_ty.display(), op),
149152
}
@@ -152,51 +155,47 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
152155
let (lhs, rhs) = *operands;
153156
let lhs_ty = self.operand_type(lhs);
154157
let rhs_ty = self.operand_type(rhs);
155-
match (&lhs_ty.ty, op) {
156-
(rty::Type::Int, mir::BinOp::Add) => lhs_ty
157-
.merge(rhs_ty, |(lhs_ty, lhs_term), (_, rhs_term)| {
158-
(lhs_ty, lhs_term.add(rhs_term))
159-
}),
160-
(rty::Type::Int, mir::BinOp::Sub) => lhs_ty
161-
.merge(rhs_ty, |(lhs_ty, lhs_term), (_, rhs_term)| {
162-
(lhs_ty, lhs_term.sub(rhs_term))
163-
}),
164-
(rty::Type::Int, mir::BinOp::Mul) => lhs_ty
165-
.merge(rhs_ty, |(lhs_ty, lhs_term), (_, rhs_term)| {
166-
(lhs_ty, lhs_term.mul(rhs_term))
167-
}),
168-
(rty::Type::Int | rty::Type::Bool, mir::BinOp::Ge) => lhs_ty
169-
.merge(rhs_ty, |(_, lhs_term), (_, rhs_term)| {
170-
(rty::Type::Bool, lhs_term.ge(rhs_term))
171-
}),
172-
(rty::Type::Int | rty::Type::Bool, mir::BinOp::Gt) => lhs_ty
173-
.merge(rhs_ty, |(_, lhs_term), (_, rhs_term)| {
174-
(rty::Type::Bool, lhs_term.gt(rhs_term))
175-
}),
176-
(rty::Type::Int | rty::Type::Bool, mir::BinOp::Le) => lhs_ty
177-
.merge(rhs_ty, |(_, lhs_term), (_, rhs_term)| {
178-
(rty::Type::Bool, lhs_term.le(rhs_term))
179-
}),
180-
(rty::Type::Int | rty::Type::Bool, mir::BinOp::Lt) => lhs_ty
181-
.merge(rhs_ty, |(_, lhs_term), (_, rhs_term)| {
182-
(rty::Type::Bool, lhs_term.lt(rhs_term))
183-
}),
184-
(rty::Type::Int | rty::Type::Bool, mir::BinOp::Eq) => lhs_ty
185-
.merge(rhs_ty, |(_, lhs_term), (_, rhs_term)| {
186-
(rty::Type::Bool, lhs_term.eq(rhs_term))
187-
}),
188-
(rty::Type::Int | rty::Type::Bool, mir::BinOp::Ne) => lhs_ty
189-
.merge(rhs_ty, |(_, lhs_term), (_, rhs_term)| {
190-
(rty::Type::Bool, lhs_term.ne(rhs_term))
191-
}),
158+
159+
let mut builder = PlaceTypeBuilder::default();
160+
let (lhs_ty, lhs_term) = builder.subsume(lhs_ty);
161+
let (_rhs_ty, rhs_term) = builder.subsume(rhs_ty);
162+
match (&lhs_ty, op) {
163+
(rty::Type::Int, mir::BinOp::Add) => {
164+
builder.build(lhs_ty, rhs_term.add(lhs_term))
165+
}
166+
(rty::Type::Int, mir::BinOp::Sub) => {
167+
builder.build(lhs_ty, lhs_term.sub(rhs_term))
168+
}
169+
(rty::Type::Int, mir::BinOp::Mul) => {
170+
builder.build(lhs_ty, lhs_term.mul(rhs_term))
171+
}
172+
(rty::Type::Int | rty::Type::Bool, mir::BinOp::Ge) => {
173+
builder.build(rty::Type::Bool, lhs_term.ge(rhs_term))
174+
}
175+
(rty::Type::Int | rty::Type::Bool, mir::BinOp::Gt) => {
176+
builder.build(rty::Type::Bool, lhs_term.gt(rhs_term))
177+
}
178+
(rty::Type::Int | rty::Type::Bool, mir::BinOp::Le) => {
179+
builder.build(rty::Type::Bool, lhs_term.le(rhs_term))
180+
}
181+
(rty::Type::Int | rty::Type::Bool, mir::BinOp::Lt) => {
182+
builder.build(rty::Type::Bool, lhs_term.lt(rhs_term))
183+
}
184+
(rty::Type::Int | rty::Type::Bool, mir::BinOp::Eq) => {
185+
builder.build(rty::Type::Bool, lhs_term.eq(rhs_term))
186+
}
187+
(rty::Type::Int | rty::Type::Bool, mir::BinOp::Ne) => {
188+
builder.build(rty::Type::Bool, lhs_term.ne(rhs_term))
189+
}
192190
_ => unimplemented!("ty={}, op={:?}", lhs_ty.display(), op),
193191
}
194192
}
195193
Rvalue::Ref(_, mir::BorrowKind::Shared, place) => {
196194
let ty = self.env.place_type(self.elaborate_place(&place));
197-
ty.replace(|ty, term| {
198-
(rty::PointerType::immut_to(ty).into(), chc::Term::box_(term))
199-
})
195+
196+
let mut builder = PlaceTypeBuilder::default();
197+
let (ty, term) = builder.subsume(ty);
198+
builder.build(rty::PointerType::immut_to(ty).into(), chc::Term::box_(term))
200199
}
201200
Rvalue::Aggregate(kind, fields) => {
202201
// elaboration: all fields are boxed
@@ -240,12 +239,16 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
240239

241240
let sort_args: Vec<_> = params.iter().map(|rty| rty.ty.to_sort()).collect();
242241
let ty = rty::EnumType::new(ty_sym.clone(), params).into();
243-
PlaceType::aggregate(
244-
field_tys,
245-
|_| ty,
246-
|fields_term| {
247-
chc::Term::datatype_ctor(ty_sym, sort_args, v_sym, fields_term)
248-
},
242+
243+
let mut builder = PlaceTypeBuilder::default();
244+
let mut field_terms = Vec::new();
245+
for field_ty in field_tys {
246+
let (_, field_term) = builder.subsume(field_ty);
247+
field_terms.push(field_term);
248+
}
249+
builder.build(
250+
ty,
251+
chc::Term::datatype_ctor(ty_sym, sort_args, v_sym, field_terms),
249252
)
250253
}
251254
_ => PlaceType::tuple(field_tys),
@@ -276,7 +279,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
276279
.expect("discriminant of non-enum")
277280
.symbol
278281
.clone();
279-
ty.replace(|_ty, term| (rty::Type::Int, chc::Term::datatype_discr(sym, term)))
282+
283+
let mut builder = PlaceTypeBuilder::default();
284+
let (_, term) = builder.subsume(ty);
285+
builder.build(rty::Type::Int, chc::Term::datatype_discr(sym, term))
280286
}
281287
_ => unimplemented!(
282288
"rvalue={:?} ({:?})",
@@ -383,20 +389,23 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
383389
_ => unimplemented!(),
384390
};
385391

386-
self.with_assumption(
387-
discr_ty
388-
.clone()
389-
.into_assumption(|term| term.equal_to(target_term.clone())),
390-
|ecx| {
391-
callback(ecx, bb);
392-
ecx.type_goto(bb, expected_ret);
393-
},
394-
);
395-
negations.push(
396-
discr_ty
397-
.clone()
398-
.into_assumption(|term| term.not_equal_to(target_term)),
399-
);
392+
let pos_assumption = {
393+
let mut builder = PlaceTypeBuilder::default();
394+
let (_, discr_term) = builder.subsume(discr_ty.clone());
395+
builder.push_formula(discr_term.equal_to(target_term.clone()));
396+
builder.build_assumption()
397+
};
398+
self.with_assumption(pos_assumption, |ecx| {
399+
callback(ecx, bb);
400+
ecx.type_goto(bb, expected_ret);
401+
});
402+
let neg_assumption = {
403+
let mut builder = PlaceTypeBuilder::default();
404+
let (_, discr_term) = builder.subsume(discr_ty.clone());
405+
builder.push_formula(discr_term.not_equal_to(target_term.clone()));
406+
builder.build_assumption()
407+
};
408+
negations.push(neg_assumption);
400409
}
401410
self.with_assumptions(negations, |ecx| {
402411
callback(ecx, targets.otherwise());
@@ -508,11 +517,12 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
508517
let local_ty = self.env.local_type(local);
509518
let rvalue_ty = self.rvalue_type(rvalue);
510519
if !rvalue_ty.ty.to_sort().is_singleton() {
511-
self.env.assume(
512-
local_ty.merge_into_assumption(rvalue_ty, |local_term, rvalue_term| {
513-
local_term.mut_final().equal_to(rvalue_term)
514-
}),
515-
);
520+
let mut builder = PlaceTypeBuilder::default();
521+
let (_, local_term) = builder.subsume(local_ty);
522+
let (_, rvalue_term) = builder.subsume(rvalue_ty);
523+
builder.push_formula(local_term.mut_final().equal_to(rvalue_term));
524+
let assumption = builder.build_assumption();
525+
self.env.assume(assumption);
516526
}
517527
}
518528

‎src/refine.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ mod basic_block;
55
pub use basic_block::BasicBlockType;
66

77
mod env;
8-
pub use env::{Assumption, Env, PlaceType, PlaceTypeVar, TempVarIdx, Var};
8+
pub use env::{Assumption, Env, PlaceType, PlaceTypeBuilder, PlaceTypeVar, TempVarIdx, Var};
99

1010
use crate::chc::DatatypeSymbol;
1111
use rustc_middle::ty as mir_ty;

0 commit comments

Comments
 (0)