Skip to content

Commit 9315177

Browse files
vecchiot-awstedinski
vecchiot-aws
authored and
tedinski
committed
Added Location to stmt constructors(rust-lang#139)
1 parent 93fea95 commit 9315177

File tree

12 files changed

+296
-210
lines changed

12 files changed

+296
-210
lines changed

‎compiler/rustc_codegen_llvm/src/gotoc/assumptions.rs

Lines changed: 42 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ impl<'tcx> GotocCtx<'tcx> {
5454
.dereference()
5555
.ge(Expr::int_constant(below, Type::signed_int(32)))
5656
.and(ptr.dereference().le(Expr::int_constant(above, Type::signed_int(32))))
57-
.ret();
57+
.ret(Location::none());
5858
body.push(exp)
5959
})
6060
});
@@ -69,7 +69,7 @@ impl<'tcx> GotocCtx<'tcx> {
6969
.dereference()
7070
.eq(Expr::c_true())
7171
.or(ptr.dereference().eq(Expr::c_false()))
72-
.ret();
72+
.ret(Location::none());
7373
body.push(exp)
7474
})
7575
});
@@ -221,22 +221,29 @@ impl<'tcx> GotocCtx<'tcx> {
221221
//CHECKME: why is this 2?
222222
let idx = tcx.gen_function_local_variable(2, &fname, Type::size_t()).to_expr();
223223
body.push(Stmt::decl(idx.clone(), Some(Type::size_t().zero()), Location::none()));
224-
let lbody = Stmt::block(vec![
225-
data.clone()
226-
.neq(data.typ().null())
227-
.implies(f.call(vec![data.plus(idx.clone())]))
228-
.not()
229-
.if_then_else(Expr::bool_false().ret(), None, Location::none()),
230-
]);
224+
let lbody = Stmt::block(
225+
vec![
226+
data.clone()
227+
.neq(data.typ().null())
228+
.implies(f.call(vec![data.plus(idx.clone())]))
229+
.not()
230+
.if_then_else(
231+
Expr::bool_false().ret(Location::none()),
232+
None,
233+
Location::none(),
234+
),
235+
],
236+
Location::none(),
237+
);
231238
body.push(Stmt::for_loop(
232239
Stmt::skip(Location::none()),
233240
idx.clone().lt(len),
234-
idx.postincr().as_stmt(),
241+
idx.postincr().as_stmt(Location::none()),
235242
lbody,
236243
Location::none(),
237244
));
238245
}
239-
body.push(fold_invariants(invariants).ret());
246+
body.push(fold_invariants(invariants).ret(Location::none()));
240247
})
241248
}
242249

@@ -260,7 +267,7 @@ impl<'tcx> GotocCtx<'tcx> {
260267
if let Some(f) = f {
261268
invarints.push(x.clone().neq(x.typ().null()).implies(f.call(vec![x])));
262269
}
263-
body.push(fold_invariants(invarints).ret());
270+
body.push(fold_invariants(invarints).ret(Location::none()));
264271
})
265272
}
266273

@@ -296,7 +303,7 @@ impl<'tcx> GotocCtx<'tcx> {
296303
) -> Symbol {
297304
self.codegen_assumption_genfunc(fname, t, |tcx, ptr, body| {
298305
let invariants = tcx.codegen_assumption_struct_invariant(ptr, variant, subst);
299-
body.push(fold_invariants(invariants).ret());
306+
body.push(fold_invariants(invariants).ret(Location::none()));
300307
})
301308
}
302309

@@ -336,7 +343,7 @@ impl<'tcx> GotocCtx<'tcx> {
336343
) -> Symbol {
337344
self.codegen_assumption_genfunc(fname, t, |tcx, ptr, body| {
338345
let invariants = tcx.codegen_assumption_struct_invariant(ptr, variant, subst);
339-
body.push(fold_invariants(invariants).ret());
346+
body.push(fold_invariants(invariants).ret(Location::none()));
340347
})
341348
}
342349

@@ -382,7 +389,7 @@ impl<'tcx> GotocCtx<'tcx> {
382389

383390
let data_invar = tcx.codegen_assumption_struct_invariant(ptr, variant, subst);
384391
invariants.push(fold_invariants(data_invar));
385-
body.push(fold_invariants_or(invariants).ret());
392+
body.push(fold_invariants_or(invariants).ret(Location::none()));
386393
})
387394
}
388395

@@ -486,7 +493,7 @@ impl<'tcx> GotocCtx<'tcx> {
486493
}
487494
}
488495

489-
body.push(fold_invariants(invariants).ret());
496+
body.push(fold_invariants(invariants).ret(Location::none()));
490497
})
491498
}
492499

@@ -510,25 +517,29 @@ impl<'tcx> GotocCtx<'tcx> {
510517
let idx = tcx.gen_function_local_variable(2, &fname, Type::size_t());
511518
body.push(Stmt::decl(idx.to_expr(), Some(Type::size_t().zero()), Location::none()));
512519
let idxe = idx.to_expr();
513-
let lbody = Stmt::block(vec![
514-
f.call(vec![
515-
tcx.codegen_idx_array(ptr.clone().dereference(), idxe.clone()).address_of(),
516-
])
517-
.not()
518-
.if_then_else(
519-
Expr::bool_false().ret(),
520-
None,
521-
Location::none(),
522-
),
523-
]);
520+
let lbody = Stmt::block(
521+
vec![
522+
f.call(vec![
523+
tcx.codegen_idx_array(ptr.clone().dereference(), idxe.clone())
524+
.address_of(),
525+
])
526+
.not()
527+
.if_then_else(
528+
Expr::bool_false().ret(Location::none()),
529+
None,
530+
Location::none(),
531+
),
532+
],
533+
Location::none(),
534+
);
524535
body.push(Stmt::for_loop(
525536
Stmt::skip(Location::none()),
526537
idxe.clone().lt(tcx.codegen_const(c, None)),
527-
idxe.postincr().as_stmt(),
538+
idxe.postincr().as_stmt(Location::none()),
528539
lbody,
529540
Location::none(),
530541
));
531-
body.push(Expr::bool_true().ret());
542+
body.push(Expr::bool_true().ret(Location::none()));
532543
}
533544
})
534545
}
@@ -553,7 +564,7 @@ impl<'tcx> GotocCtx<'tcx> {
553564
invariants.push(f.call(vec![field]));
554565
}
555566
}
556-
body.push(fold_invariants(invariants).ret());
567+
body.push(fold_invariants(invariants).ret(Location::none()));
557568
})
558569
}
559570

@@ -570,7 +581,7 @@ impl<'tcx> GotocCtx<'tcx> {
570581
let mut stmts = vec![];
571582
//let mut body = Stmt::block(vec![]);
572583
f(self, ptr, &mut stmts);
573-
let body = Stmt::block(stmts);
584+
let body = Stmt::block(stmts, Location::none());
574585
Symbol::function(
575586
fname,
576587
Type::code(vec![var.to_function_parameter()], Type::bool()),

‎compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1172,14 +1172,12 @@ impl Expr {
11721172
/// The statement constructors do typechecking, so we don't redundantly do that here.
11731173
impl Expr {
11741174
/// `self;`
1175-
pub fn as_stmt(self) -> Stmt {
1176-
let loc = self.location.clone();
1175+
pub fn as_stmt(self, loc: Location) -> Stmt {
11771176
Stmt::code_expression(self, loc)
11781177
}
11791178

11801179
/// `self = rhs;`
1181-
pub fn assign(self, rhs: Expr) -> Stmt {
1182-
let loc = rhs.location.clone();
1180+
pub fn assign(self, rhs: Expr, loc: Location) -> Stmt {
11831181
Stmt::assign(self, rhs, loc)
11841182
}
11851183

@@ -1189,8 +1187,7 @@ impl Expr {
11891187
}
11901188

11911189
/// `return self;`
1192-
pub fn ret(self) -> Stmt {
1193-
let loc = self.location.clone();
1190+
pub fn ret(self, loc: Location) -> Stmt {
11941191
Stmt::ret(Some(self), loc)
11951192
}
11961193

‎compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/stmt.rs

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -170,15 +170,17 @@ impl Stmt {
170170
);
171171
let nondet_value = lhs.typ().nondet();
172172
let nondet_assign_stmt = stmt!(Assign { lhs, rhs: nondet_value }, loc.clone());
173-
return Stmt::block(vec![assert_stmt, nondet_assign_stmt]);
173+
return Stmt::block(vec![assert_stmt, nondet_assign_stmt], loc);
174174
}
175175
stmt!(Assign { lhs, rhs }, loc)
176176
}
177177

178178
/// `__CPROVER_assert(cond, msg);`
179179
pub fn assert(cond: Expr, msg: &str, loc: Location) -> Self {
180180
assert!(cond.typ().is_bool());
181-
BuiltinFn::CProverAssert.call(vec![cond, Expr::string_constant(msg)], loc).as_stmt()
181+
BuiltinFn::CProverAssert
182+
.call(vec![cond, Expr::string_constant(msg)], loc.clone())
183+
.as_stmt(loc)
182184
}
183185

184186
pub fn assert_false(msg: &str, loc: Location) -> Self {
@@ -192,14 +194,12 @@ impl Stmt {
192194
}
193195

194196
/// { ATOMIC_BEGIN stmt1; stmt2; ... ATOMIC_END }
195-
pub fn atomic_block(stmts: Vec<Stmt>) -> Self {
196-
let loc = if stmts.is_empty() { Location::none() } else { stmts[0].location().clone() };
197+
pub fn atomic_block(stmts: Vec<Stmt>, loc: Location) -> Self {
197198
stmt!(AtomicBlock(stmts), loc)
198199
}
199200

200201
/// `{ stmt1; stmt2; ... }`
201-
pub fn block(stmts: Vec<Stmt>) -> Self {
202-
let loc = if stmts.is_empty() { Location::none() } else { stmts[0].location().clone() };
202+
pub fn block(stmts: Vec<Stmt>, loc: Location) -> Self {
203203
stmt!(Block(stmts), loc)
204204
}
205205

‎compiler/rustc_codegen_llvm/src/gotoc/cbmc/irep/to_irep.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -237,7 +237,7 @@ impl ToIrep for ExprValue {
237237
ExprValue::SelfOp { op, e } => side_effect_irep(op.to_irep_id(), vec![e.to_irep(mm)]),
238238
ExprValue::StatementExpression { statements: ops } => side_effect_irep(
239239
IrepId::StatementExpression,
240-
vec![Stmt::block(ops.to_vec()).to_irep(mm)],
240+
vec![Stmt::block(ops.to_vec(), Location::none()).to_irep(mm)],
241241
),
242242
ExprValue::StringConstant { s } => Irep {
243243
id: IrepId::StringConstant,

0 commit comments

Comments
 (0)