Skip to content

Commit

Permalink
Added Location to Expr::ret
Browse files Browse the repository at this point in the history 
Added Location to Expr::assign

Added Location to Expr::as_stmt

Added Location to Stmt::atomic_block

Added Location to Stmt::block

Fixed move errors.
  • Loading branch information
@vecchiot-aws
vecchiot-aws committed May 21, 2021
1 parent 662d19b commit f2073fa
Show file tree
Hide file tree
Showing 12 changed files with 305 additions and 210 deletions.
73 changes: 42 additions & 31 deletions compiler/rustc_codegen_llvm/src/gotoc/assumptions.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ impl<'tcx> GotocCtx<'tcx> {
.dereference()
.ge(Expr::int_constant(below, Type::signed_int(32)))
.and(ptr.dereference().le(Expr::int_constant(above, Type::signed_int(32))))
.ret();
.ret(Location::none());
body.push(exp)
})
});
Expand All @@ -69,7 +69,7 @@ impl<'tcx> GotocCtx<'tcx> {
.dereference()
.eq(Expr::c_true())
.or(ptr.dereference().eq(Expr::c_false()))
.ret();
.ret(Location::none());
body.push(exp)
})
});
Expand Down Expand Up @@ -221,22 +221,29 @@ impl<'tcx> GotocCtx<'tcx> {
//CHECKME: why is this 2?
let idx = tcx.gen_function_local_variable(2, &fname, Type::size_t()).to_expr();
body.push(Stmt::decl(idx.clone(), Some(Type::size_t().zero()), Location::none()));
let lbody = Stmt::block(vec![
data.clone()
.neq(data.typ().null())
.implies(f.call(vec![data.plus(idx.clone())]))
.not()
.if_then_else(Expr::bool_false().ret(), None, Location::none()),
]);
let lbody = Stmt::block(
vec![
data.clone()
.neq(data.typ().null())
.implies(f.call(vec![data.plus(idx.clone())]))
.not()
.if_then_else(
Expr::bool_false().ret(Location::none()),
None,
Location::none(),
),
],
Location::none(),
);
body.push(Stmt::for_loop(
Stmt::skip(Location::none()),
idx.clone().lt(len),
idx.postincr().as_stmt(),
idx.postincr().as_stmt(Location::none()),
lbody,
Location::none(),
));
}
body.push(fold_invariants(invariants).ret());
body.push(fold_invariants(invariants).ret(Location::none()));
})
}

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

Expand Down Expand Up @@ -296,7 +303,7 @@ impl<'tcx> GotocCtx<'tcx> {
) -> Symbol {
self.codegen_assumption_genfunc(fname, t, |tcx, ptr, body| {
let invariants = tcx.codegen_assumption_struct_invariant(ptr, variant, subst);
body.push(fold_invariants(invariants).ret());
body.push(fold_invariants(invariants).ret(Location::none()));
})
}

Expand Down Expand Up @@ -336,7 +343,7 @@ impl<'tcx> GotocCtx<'tcx> {
) -> Symbol {
self.codegen_assumption_genfunc(fname, t, |tcx, ptr, body| {
let invariants = tcx.codegen_assumption_struct_invariant(ptr, variant, subst);
body.push(fold_invariants(invariants).ret());
body.push(fold_invariants(invariants).ret(Location::none()));
})
}

Expand Down Expand Up @@ -382,7 +389,7 @@ impl<'tcx> GotocCtx<'tcx> {

let data_invar = tcx.codegen_assumption_struct_invariant(ptr, variant, subst);
invariants.push(fold_invariants(data_invar));
body.push(fold_invariants_or(invariants).ret());
body.push(fold_invariants_or(invariants).ret(Location::none()));
})
}

Expand Down Expand Up @@ -486,7 +493,7 @@ impl<'tcx> GotocCtx<'tcx> {
}
}

body.push(fold_invariants(invariants).ret());
body.push(fold_invariants(invariants).ret(Location::none()));
})
}

Expand All @@ -510,25 +517,29 @@ impl<'tcx> GotocCtx<'tcx> {
let idx = tcx.gen_function_local_variable(2, &fname, Type::size_t());
body.push(Stmt::decl(idx.to_expr(), Some(Type::size_t().zero()), Location::none()));
let idxe = idx.to_expr();
let lbody = Stmt::block(vec![
f.call(vec![
tcx.codegen_idx_array(ptr.clone().dereference(), idxe.clone()).address_of(),
])
.not()
.if_then_else(
Expr::bool_false().ret(),
None,
Location::none(),
),
]);
let lbody = Stmt::block(
vec![
f.call(vec![
tcx.codegen_idx_array(ptr.clone().dereference(), idxe.clone())
.address_of(),
])
.not()
.if_then_else(
Expr::bool_false().ret(Location::none()),
None,
Location::none(),
),
],
Location::none(),
);
body.push(Stmt::for_loop(
Stmt::skip(Location::none()),
idxe.clone().lt(tcx.codegen_const(c, None)),
idxe.postincr().as_stmt(),
idxe.postincr().as_stmt(Location::none()),
lbody,
Location::none(),
));
body.push(Expr::bool_true().ret());
body.push(Expr::bool_true().ret(Location::none()));
}
})
}
Expand All @@ -553,7 +564,7 @@ impl<'tcx> GotocCtx<'tcx> {
invariants.push(f.call(vec![field]));
}
}
body.push(fold_invariants(invariants).ret());
body.push(fold_invariants(invariants).ret(Location::none()));
})
}

Expand All @@ -570,7 +581,7 @@ impl<'tcx> GotocCtx<'tcx> {
let mut stmts = vec![];
//let mut body = Stmt::block(vec![]);
f(self, ptr, &mut stmts);
let body = Stmt::block(stmts);
let body = Stmt::block(stmts, Location::none());
Symbol::function(
fname,
Type::code(vec![var.to_function_parameter()], Type::bool()),
Expand Down
9 changes: 3 additions & 6 deletions compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1173,14 +1173,12 @@ impl Expr {
/// The statement constructors do typechecking, so we don't redundantly do that here.
impl Expr {
/// `self;`
pub fn as_stmt(self) -> Stmt {
let loc = self.location.clone();
pub fn as_stmt(self, loc: Location) -> Stmt {
Stmt::code_expression(self, loc)
}

/// `self = rhs;`
pub fn assign(self, rhs: Expr) -> Stmt {
let loc = rhs.location.clone();
pub fn assign(self, rhs: Expr, loc: Location) -> Stmt {
Stmt::assign(self, rhs, loc)
}

Expand All @@ -1190,8 +1188,7 @@ impl Expr {
}

/// `return self;`
pub fn ret(self) -> Stmt {
let loc = self.location.clone();
pub fn ret(self, loc: Location) -> Stmt {
Stmt::ret(Some(self), loc)
}

Expand Down
12 changes: 6 additions & 6 deletions compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/stmt.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -170,15 +170,17 @@ impl Stmt {
);
let nondet_value = lhs.typ().nondet();
let nondet_assign_stmt = stmt!(Assign { lhs, rhs: nondet_value }, loc.clone());
return Stmt::block(vec![assert_stmt, nondet_assign_stmt]);
return Stmt::block(vec![assert_stmt, nondet_assign_stmt], loc);
}
stmt!(Assign { lhs, rhs }, loc)
}

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

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

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

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

Expand Down
2 changes: 1 addition & 1 deletion compiler/rustc_codegen_llvm/src/gotoc/cbmc/irep/to_irep.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -237,7 +237,7 @@ impl ToIrep for ExprValue {
ExprValue::SelfOp { op, e } => side_effect_irep(op.to_irep_id(), vec![e.to_irep(mm)]),
ExprValue::StatementExpression { statements: ops } => side_effect_irep(
IrepId::StatementExpression,
vec![Stmt::block(ops.to_vec()).to_irep(mm)],
vec![Stmt::block(ops.to_vec(), Location::none()).to_irep(mm)],
),
ExprValue::StringConstant { s } => Irep {
id: IrepId::StringConstant,
Expand Down
Loading

0 comments on commit f2073fa

Please sign in to comment.