Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unreachable code detection #1385

Open
wants to merge 42 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
42 commits
Select commit Hold shift + click to select a range
9ac293b
Add prusti_refute! macro
Feb 6, 2023
2c4fb37
Merge branch 'master' of github.com:simon-hrabec/prusti-dev into feat…
Feb 15, 2023
c49f9a7
Add macro to generate getters/setters for fields via JNI
Feb 21, 2023
6c3d955
Resolve fmt-check and clippy errors, simplify naming, small refactoring
Feb 21, 2023
bee6c22
Merge branch 'master' of github.com:viperproject/prusti-dev into feat…
Feb 21, 2023
a896d5a
Add test for field! macro
Feb 26, 2023
ec17da5
Update field! macro to not ask for signature (WIP)
Feb 26, 2023
dc8642c
Update field! macro to search all the class hierarchy for the field t…
Feb 27, 2023
019f222
Merge pull request #2 from simon-hrabec/feature/jni-field-getter-sett…
simon-hrabec Feb 27, 2023
608c4aa
Rename variables, add comments, delete leftover commented code
Feb 27, 2023
0c2ecc8
Merge branch 'feature/refute_macro' into combined
Feb 27, 2023
a60bb1e
Merge branch 'master' of github.com:viperproject/prusti-dev into comb…
Feb 27, 2023
542d905
Merge branch 'master' of github.com:viperproject/prusti-dev into comb…
simon-hrabec Feb 27, 2023
667c3b6
Follow update in master branch
simon-hrabec Feb 27, 2023
864c896
current code, just a snapshot of my working dir
simon-hrabec Mar 6, 2023
b9796a6
fix bug with env/ast_utils with_local_frame - calling wrong function
simon-hrabec Mar 13, 2023
a490f2f
Merge branch 'master' of github.com:viperproject/prusti-dev into comb…
simon-hrabec Mar 13, 2023
0d48d5a
add
simon-hrabec Mar 13, 2023
ea965ab
Remove unecessary changes
simon-hrabec Mar 13, 2023
76e0376
additional temporary code removal
simon-hrabec Mar 13, 2023
8117694
Add "refute.failed:refutation.true" into error_manager
simon-hrabec Mar 13, 2023
e6b5692
Remove unnecessary code, fmt-all
simon-hrabec Mar 13, 2023
7443fd2
Merge branch 'master' of github.com:viperproject/prusti-dev into comb…
simon-hrabec Mar 13, 2023
cc7bb62
cargo lock update
simon-hrabec Mar 13, 2023
fc2bda8
add frotend support also for carbon
simon-hrabec Mar 17, 2023
d0ad6a6
add assert.failed:assertion.false-PanicCause::Refute entry to the err…
simon-hrabec Mar 19, 2023
6867a3b
Add field access via Scala methods, use SilFrontend wrapper and remov…
simon-hrabec Mar 20, 2023
0415395
Remove empty line - fmt-all error
simon-hrabec Mar 20, 2023
2695baf
add tests for prusti_refute!
simon-hrabec Mar 21, 2023
a207e10
update docs (user guide) - add mention to refute
simon-hrabec Mar 21, 2023
e6897da
trying to figure out positions for added refutes
simon-hrabec Mar 27, 2023
e71787a
use terminator span
simon-hrabec Mar 28, 2023
31bc7d9
Update unreachable message
simon-hrabec Mar 29, 2023
bdfcd24
delete lefrover code
simon-hrabec Mar 29, 2023
b66210e
make code unreachable errors just warnings
simon-hrabec Apr 3, 2023
7592282
change detection of assert/panic terminators
simon-hrabec Apr 3, 2023
ca94f92
remove unecessary case in the error manager
simon-hrabec Apr 3, 2023
27ecb2e
make line/column numbers unique for code reachability refute statements
simon-hrabec Apr 4, 2023
b9cb939
remove unecessary member variable, use just position id
simon-hrabec Apr 4, 2023
d7deab6
Merge branch 'master' of github.com:viperproject/prusti-dev into feat…
simon-hrabec Apr 4, 2023
5cd88f5
make position manager return positions with unique line/column
simon-hrabec Apr 5, 2023
8433a89
rely on the change in position manager for unique line/column numbers…
simon-hrabec Apr 6, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
use terminator span
simon-hrabec committed Mar 28, 2023
commit e71787af1047cf2ed85f2664e4254605cf935a79
286 changes: 216 additions & 70 deletions prusti-viper/src/encoder/procedure_encoder.rs
Original file line number Diff line number Diff line change
@@ -135,77 +135,188 @@ pub struct ProcedureEncoder<'p, 'v: 'p, 'tcx: 'v> {
substs: SubstsRef<'tcx>,
}

fn get_first_position(statements: &Vec<Stmt>) -> Option<Position> {
for statement in statements {
match statement {
Stmt::Comment(_) => (),
Stmt::Label(_) => (),
Stmt::Inhale(inhale) => return Some(inhale.expr.pos()),
Stmt::Exhale(exhale) => return Some(exhale.position),
Stmt::Assert(assert) => return Some(assert.position),
Stmt::Refute(refute) => return Some(refute.position),
// Stmt::MethodCall(method_call) => {
// for expression in method_call.arguments {
// if expression.pos() != Position::default() {
// return Some(expression.pos());
// }
// }
// None
// },
Stmt::Assign(assign) => return Some(assign.target.pos()),
Stmt::Fold(fold) => return Some(fold.position),
// Stmt::Unfold(_) => todo!(),
// Stmt::Obtain(_) => todo!(),
// Stmt::BeginFrame(_) => todo!(),
// Stmt::EndFrame(_) => todo!(),
// Stmt::TransferPerm(_) => todo!(),
// Stmt::PackageMagicWand(_) => todo!(),
// Stmt::ApplyMagicWand(_) => todo!(),
// Stmt::ExpireBorrows(_) => todo!(),
// Stmt::If(_) => todo!(),
// Stmt::Downcast(_) => todo!(),
_ => (),
}
}
None
}

// fn add_unreachable_code_check(&mut self) {
fn add_unreachable_code_check(mut method: vir::CfgMethod, encoder: &Encoder, mir_encorder: &MirEncoder) -> vir::CfgMethod {
for block in method.basic_blocks.iter_mut() {
if let Some(position) = get_first_position(&block.stmts) {
// let span: Span = encoder.error_manager().position_manager().get_span(position).unwrap().primary_span().unwrap();
// let position = Position::new(4, 17, 11);
let position = encoder.error_manager().duplicate_position(position);
encoder.error_manager().set_error(position, ErrorCtxt::Panic(PanicCause::Refute));
// let a = self.encoder.error_manager();
// let b = a.position_manager();
// let c = b.duplicate(position);
// let position_copy = self.encoder.error_manager().position_manager().duplicate(position);
// fn statement_position(statement: &Stmt) -> Option<Position> {
// match statement {
// vir::Stmt::Comment(_) => None,
// vir::Stmt::Label(_) => None,
// vir::Stmt::Inhale(inhale) => Some(inhale.expr.pos()),
// vir::Stmt::Exhale(exhale) => Some(exhale.position),
// vir::Stmt::Assert(assert) => Some(assert.position),
// vir::Stmt::Refute(refute) => Some(refute.position),
// // vir::Stmt::MethodCall(method_call) => {
// // for expression in method_call.arguments {
// // if expression.pos() != Position::default() {
// // return Some(expression.pos());
// // }
// // }
// // None
// // },
// vir::Stmt::Assign(assign) => Some(assign.target.pos()),
// vir::Stmt::Fold(fold) => Some(fold.position),
// // vir::Stmt::Unfold(_) => todo!(),
// // vir::Stmt::Obtain(_) => todo!(),
// // vir::Stmt::BeginFrame(_) => todo!(),
// // vir::Stmt::EndFrame(_) => todo!(),
// // vir::Stmt::TransferPerm(_) => todo!(),
// // vir::Stmt::PackageMagicWand(_) => todo!(),
// // vir::Stmt::ApplyMagicWand(_) => todo!(),
// // vir::Stmt::ExpireBorrows(_) => todo!(),
// // vir::Stmt::If(_) => todo!(),
// // vir::Stmt::Downcast(_) => todo!(),
// _ => None,
// }
// }


// let span = self
// .encoder
// .get_definition_span(refutation.refutation.to_def_id());

// let refute_expr = self.encoder.encode_invariant(self.mir, bb, self.proc_def_id, cl_substs)?;
// println!("refute expression: {:?}", refute_expr);

// let refute_stmt = vir::Stmt::Refute(
// vir::Refute {
// expr: refute_expr,
// position: self.register_error(span, ErrorCtxt::Panic(PanicCause::Refute))
// }
// );

// encoded_statements.push(refute_stmt);

// return Ok(true);

// pub fn insert_refutes(mut method: vir::CfgMethod) -> vir::CfgMethod {
// let mut first_position: Option<Position> = None;
// for block in method.basic_blocks.iter_mut() {
// // for statement in block.stmts {
// // if let Some(pos) = statement_position(&statement) {
// // first_position = Some(pos);
// // }
// // }
// // if first_position == None {
// // continue;
// // }
// // let first_position = first_position.unwrap();

// println!("Before reverse {:?}", block.stmts);
// block.stmts.reverse();

// let comment = block.stmts.pop().unwrap();

// // let xxx :vir_crate::polymorphic::ast::Stmt = vir_crate::polymorphic::ast::Stmt::Refute();
// // let yyy: vir::Expr::Const()
// // let zzz:
// let expr = vir::ast::Expr::Const(vir::ast::expr::ConstExpr{
// value: vir::ast::expr::Const::Bool(false),
// position: vir::ast::common::Position::new(23, 17, 61),
// // position: vir::ast::common::Position::default(),
// });



// // Expr::Const(ConstExpr {
// // value: val.into(),
// // position: Position::default(),
// // })
// let refute_stmt = vir::Stmt::Refute(
// vir::Refute {
// expr,
// position: vir::ast::common::Position::new(23, 17, 61),
// // position: vir::ast::common::Position::default(),
// }
// );

// // refute_stmt.
// block.stmts.push(refute_stmt);
// // let mut vvv = vec![refute_stmt];
// // block.stmts.append(&mut vvv);
// block.stmts.push(comment);
// // println!("After append {:?}", block.stmts);


// block.stmts.reverse();
// // println!("Dereversed {:?}", block.stmts);

// // let vir_create::gen::polymorphic::ast::stmt::Stmt x = ;
// // vir::gen::polymorphic::ast::stmt::Stmt
// // vir::gen::polymorphic::ast::stmt
// // block.stmts.append(other)
// }
// method
// }

// fn get_first_position(statements: &Vec<Stmt>) -> Option<Position> {
// for statement in statements {
// match statement {
// Stmt::Comment(_) => (),
// Stmt::Label(_) => (),
// Stmt::Inhale(inhale) => return Some(inhale.expr.pos()),
// Stmt::Exhale(exhale) => return Some(exhale.position),
// Stmt::Assert(assert) => return Some(assert.position),
// Stmt::Refute(refute) => return Some(refute.position),
// // Stmt::MethodCall(method_call) => {
// // for expression in method_call.arguments {
// // if expression.pos() != Position::default() {
// // return Some(expression.pos());
// // }
// // }
// // None
// // },
// Stmt::Assign(assign) => return Some(assign.target.pos()),
// Stmt::Fold(fold) => return Some(fold.position),
// // Stmt::Unfold(_) => todo!(),
// // Stmt::Obtain(_) => todo!(),
// // Stmt::BeginFrame(_) => todo!(),
// // Stmt::EndFrame(_) => todo!(),
// // Stmt::TransferPerm(_) => todo!(),
// // Stmt::PackageMagicWand(_) => todo!(),
// // Stmt::ApplyMagicWand(_) => todo!(),
// // Stmt::ExpireBorrows(_) => todo!(),
// // Stmt::If(_) => todo!(),
// // Stmt::Downcast(_) => todo!(),
// _ => (),
// }
// }
// None
// }

// // fn add_unreachable_code_check(&mut self) {
// fn add_unreachable_code_check(mut method: vir::CfgMethod, encoder: &Encoder, mir_encorder: &MirEncoder) -> vir::CfgMethod {
// for block in method.basic_blocks.iter_mut() {
// if let Some(position) = get_first_position(&block.stmts) {
// // let span: Span = encoder.error_manager().position_manager().get_span(position).unwrap().primary_span().unwrap();
// // let position = Position::new(4, 17, 11);
// let position = encoder.error_manager().duplicate_position(position);
// encoder.error_manager().set_error(position, ErrorCtxt::Panic(PanicCause::Refute));
// // let a = self.encoder.error_manager();
// // let b = a.position_manager();
// // let c = b.duplicate(position);
// // let position_copy = self.encoder.error_manager().position_manager().duplicate(position);

// let position = mir_encorder.register_error(span, ErrorCtxt::Panic(PanicCause::Refute));
let refute_expr = vir::ast::Expr::Const(vir::ast::expr::ConstExpr{
value: vir::ast::expr::Const::Bool(false),
position,
});

let refute_stmt = vir::Stmt::Refute(
vir::Refute {
expr: refute_expr,
position,
}
);
// // let position = mir_encorder.register_error(span, ErrorCtxt::Panic(PanicCause::Refute));
// let refute_expr = vir::ast::Expr::Const(vir::ast::expr::ConstExpr{
// value: vir::ast::expr::Const::Bool(false),
// position,
// });

// let refute_stmt = vir::Stmt::Refute(
// vir::Refute {
// expr: refute_expr,
// position,
// }
// );

block.stmts.reverse();
let comment = block.stmts.pop().unwrap();
block.stmts.push(refute_stmt);
block.stmts.push(comment);
block.stmts.reverse();
println!("After reverse {:?}\n", block.stmts);
}
}
method
}
// block.stmts.reverse();
// let comment = block.stmts.pop().unwrap();
// block.stmts.push(refute_stmt);
// block.stmts.push(comment);
// block.stmts.reverse();
// println!("After reverse {:?}\n", block.stmts);
// }
// }
// method
// }

impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
#[tracing::instrument(name = "ProcedureEncoder::new", level = "debug", skip_all, fields(proc_def_id = ?procedure.get_id()))]
@@ -571,6 +682,28 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
));
}

if config::detect_unreachable_code() {
for bbi in self.procedure.get_reachable_nonspec_cfg_blocks() {
let cfg_block_indices = &self.cfg_blocks_map[&bbi];
for cfg_block_index in cfg_block_indices {
let span = self.mir_encoder.get_span_of_basic_block(bbi);
// let bb_pos_expr = self.mir_encoder.register_span(span);
let bb_pos_expr = self.register_error(span, ErrorCtxt::UnreachableCode("Err 1".to_string()));
let bb_pos_stmt = self.register_error(span, ErrorCtxt::UnreachableCode("Err 2".to_string()));
// let bb_pos_stmt = self.mir_encoder.register_span();

let refute_expr = vir::ast::Expr::Const(vir::ast::expr::ConstExpr{value: vir::ast::expr::Const::Bool(false), position: bb_pos_expr});
let refute_stmt = vir::Stmt::Refute(vir::Refute {expr: refute_expr, position: bb_pos_stmt});

self.cfg_method.basic_blocks[cfg_block_index.block_index].stmts.reverse();
let comment = self.cfg_method.basic_blocks[cfg_block_index.block_index].stmts.pop().unwrap();
self.cfg_method.add_stmt(*cfg_block_index, refute_stmt);
self.cfg_method.basic_blocks[cfg_block_index.block_index].stmts.push(comment);
self.cfg_method.basic_blocks[cfg_block_index.block_index].stmts.reverse();
}
}
}

// Set the first CFG block
self.cfg_method.set_successor(
start_cfg_block,
@@ -620,6 +753,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
self.cfg_method = self.encoder.patch_snapshots_method(self.cfg_method)
.with_span(mir_span)?;

// let method_with_fold_unfold = self.add_unreachable_code_check(method_with_fold_unfold);
// add_unreachable_code_check(&mut self.cfg_method, &self.encoder, &self.mir_encoder);

// Add fold/unfold
let loan_locations = self
.polonius_info()
@@ -656,7 +792,17 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
// Fix variable declarations.
let method_with_fold_unfold = fix_ghost_vars(method_with_fold_unfold);

let method_with_fold_unfold = add_unreachable_code_check(method_with_fold_unfold, &self.encoder, &self.mir_encoder);
// let method_with_fold_unfold = add_unreachable_code_check(method_with_fold_unfold, &self.encoder, &self.mir_encoder);

// let x = self.add_unreachable_code_check(method_with_fold_unfold);
// let method_with_fold_unfold = if config::detect_unreachable_code() {
// method_with_fold_unfold
// } else {
// self.add_unreachable_code_check(method_with_fold_unfold)
// };

// let method_with_fold_unfold = insert_refutes(method_with_fold_unfold);

// Dump final CFG
if config::dump_debug_info() {
prusti_common::report::log::report_with_writer(