Skip to content

Commit

Permalink
misc cleanups
Browse files Browse the repository at this point in the history
  • Loading branch information
@chanheec
chanheec committed Mar 27, 2024
1 parent b154561 commit 4b98f2d
Show file tree
Hide file tree
Showing 5 changed files with 84 additions and 102 deletions.
44 changes: 15 additions & 29 deletions crates/ide-assists/src/handlers/proof_action/apply_induction.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,21 +4,17 @@ use itertools::Itertools;
use syntax::{ast::{self, vst::*}, AstNode,};


// TODO: maybe autogen decreases clause.
// TODO: remove all panics -- verus-analyzer shouldn't panic on proof-action failure
// TODO: verus-analyzer shouldn't panic on proof-action failure
pub(crate) fn apply_induction(acc: &mut Assists, ctx: &AssistContext<'_>) -> Option<()> {
let func: ast::Fn = ctx.find_node_at_offset::<ast::Fn>()?;
let body: ast::BlockExpr = func.body()?;
let func: Fn = Fn::try_from(func).ok()?;
if func.signature_decreases.is_none() {
dbg!("no decreases vst");
return None;
}


let mut new_fn = func.clone();
let param_list = &(*func.param_list?).params;

let param_names: Option<Vec<String>> = param_list
.iter()
.map(|p| {
Expand All @@ -37,37 +33,28 @@ pub(crate) fn apply_induction(acc: &mut Assists, ctx: &AssistContext<'_>) -> Opt
p.cst.as_ref().unwrap().syntax().text_range().contains_range(ctx.selection_trimmed())
})?;

let fn_name = func.name.to_string();

let pty = param_list[index].ty.as_ref().unwrap();
let pty = param_list[index].ty.as_ref()?;
let mut result = BlockExpr::new(StmtList::new());

// better way to type check?
if pty.to_string().trim() == "nat" {
result = apply_induction_on_nat(ctx, fn_name, param_names, index)?;
result = apply_induction_on_nat(ctx, func.name.to_string(), param_names, index)?;
} else {
let p = param_list[index].pat.as_ref().unwrap().as_ref();
let p = param_list[index].pat.as_ref()?.as_ref();
if let Some(en) = ctx.type_of_pat_enum(p) {
let bty = format!("Box<{}>", param_list[index].ty.as_ref().unwrap().to_string().trim());
result = apply_induction_on_enum(ctx, fn_name, param_names, index, &en, bty)?;
let bty = format!("Box<{}>", param_list[index].ty.as_ref()?.to_string().trim());
result = apply_induction_on_enum(ctx, func.name.to_string(), param_names, index, &en, bty)?;
}
}

// now check if proof now goes thorugh, and make sure it is fast
new_fn.body = Some(Box::new(result.clone()));
let verif_result = ctx.try_verus(&new_fn)?;
if !verif_result.is_success {
if !verif_result.is_success || verif_result.time > 10 {
return None;
} else {
if verif_result.time > 10 {
return None;
}
}


dbg!("{}", &result.to_string());
let result = ctx.fmt(body.clone(),result.to_string())?;

return acc.add(
AssistId("apply_induction", AssistKind::RefactorRewrite),
"Apply Induction",
Expand Down Expand Up @@ -107,8 +94,7 @@ fn apply_induction_on_nat(
// return if-else as a block
let mut stmtlist = StmtList::new();
stmtlist.statements.push(ifexpr.into());
let block = BlockExpr::new(stmtlist);
Some(block)
Some(BlockExpr::new(stmtlist))
}

fn apply_induction_on_enum(
Expand All @@ -129,25 +115,22 @@ fn apply_induction_on_enum(
continue;
}

match &**fields.unwrap() {
match &**fields? {
FieldList::RecordFieldList(fields) => {
let names =
fields.as_ref().fields.iter().map(|f| f.name.as_ref().to_string()).join(",");

let calls = fields
.as_ref()
.fields
.iter()
.filter(|f| {
// TODO: this is awful
let fty = f.ty.as_ref().to_string().replace(" ", "");
fty == bty
f.ty.to_string().replace(" ", "") == bty
})
.map(|f| {
let mut args = vec![];
param_names.iter().enumerate().for_each(|(i, name)| {
if i == index {
args.push(format!("*{}", f.name.as_ref().to_string()));
args.push(format!("*{}", f.name.to_string()));
} else {
args.push(name.clone());
}
Expand All @@ -159,7 +142,10 @@ fn apply_induction_on_enum(
let arm = format!("{}::{}{{{}}} => {{{};}}", en.name, variant.name, names, calls);
match_arms.push(arm);
}
FieldList::TupleFieldList(_) => panic!("not supported yet"),
FieldList::TupleFieldList(_) => {
// not yet supported
return None
},
}
}
let m = format!("match {} {{\n{}\n}}", param_names[index], match_arms.join(",\n"));
Expand Down
124 changes: 62 additions & 62 deletions crates/ide-assists/src/handlers/proof_action/localize_error.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,10 +101,9 @@ fn split_expr(ctx: &AssistContext<'_>, exp: &Expr) -> Option<Vec<Expr>> {
_ => return None,
}
},
Expr::MatchExpr(me) => {
// is the enum does not have #[is_variant], return None
// for now, assume #[is_variant]
// TODO: update to `is` syntax
Expr::MatchExpr(_me) => {
// #[is_variant] is now deprecated in Verus
// TODO: update grammar and parser, and utilize `is` syntax
return None;
},
Expr::CallExpr(call) => {
Expand Down Expand Up @@ -260,64 +259,6 @@ fn main() {}
);
}

// TEST: match
#[test]
fn decompose_match_failure() {
check_assist(
localize_error,
// before
r#"
use vstd::prelude::*;
#[derive(PartialEq, Eq)]
#[is_variant]
pub enum Message {
Quit(bool),
Move { x: i32, y: i32 },
Write(bool),
}
proof fn test_expansion_multiple_call() {
let x = Message::Move{x: 5, y:6};
as$0sert(match x {
Message::Quit(b) => b,
Message::Move{x, y} => false,
Message::Write(b) => b,
});
}
fn main() {}
"#,
// after
r#"
use vstd::prelude::*;
#[derive(PartialEq, Eq)]
#[is_variant]
pub enum Message {
Quit(bool),
Move { x: i32, y: i32 },
Write(bool),
}
proof fn test_expansion_multiple_call() {
let x = Message::Move{x: 5, y:6};
assert(x.is_Quit() ==> x.get_Quit_0());
assert(x.is_Move() ==> x.get_Move_x() > x.get_Move_y());
assert(x.is_Write() ==> x.get_Write_0());
assert(match x {
Message::Quit(b) => b,
Message::Move{x, y} => x > y,
Message::Write(b) => b,
});
}
fn main() {}
"#,
);
}


// TEST: inline
#[test]
fn decompose_function_inline() {
Expand Down Expand Up @@ -380,4 +321,63 @@ fn main() {}
"#,
);
}

// TEST: match (deprecated verus syntax)
// #[test]
// fn decompose_match_failure() {
// check_assist(
// localize_error,
// // before
// r#"
// use vstd::prelude::*;

// #[derive(PartialEq, Eq)]
// #[is_variant]
// pub enum Message {
// Quit(bool),
// Move { x: i32, y: i32 },
// Write(bool),
// }

// proof fn test_expansion_multiple_call() {
// let x = Message::Move{x: 5, y:6};
// as$0sert(match x {
// Message::Quit(b) => b,
// Message::Move{x, y} => false,
// Message::Write(b) => b,
// });
// }

// fn main() {}
// "#,
// // after
// r#"
// use vstd::prelude::*;

// #[derive(PartialEq, Eq)]
// #[is_variant]
// pub enum Message {
// Quit(bool),
// Move { x: i32, y: i32 },
// Write(bool),
// }

// proof fn test_expansion_multiple_call() {
// let x = Message::Move{x: 5, y:6};
// assert(x.is_Quit() ==> x.get_Quit_0());
// assert(x.is_Move() ==> x.get_Move_x() > x.get_Move_y());
// assert(x.is_Write() ==> x.get_Write_0());
// assert(match x {
// Message::Quit(b) => b,
// Message::Move{x, y} => x > y,
// Message::Write(b) => b,
// });
// }

// fn main() {}
// "#,
// );
// }


}
14 changes: 4 additions & 10 deletions crates/ide-assists/src/handlers/proof_action/remove_dead_assertion.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,8 @@ use crate::{
assist_context::{AssistContext, Assists}, vst_api::run_verus::VerifResult, AssistId, AssistKind
};
use ide_db::syntax_helpers::vst_ext::vst_map_expr_visitor;
use syntax::{
ast::{self, vst::{self, *}, AstNode},
T,
};
use syntax::{ast::{self, vst::{self, *}, AstNode},T,};


// This version does not comment out dead assertions
// instead, it deletes all of them
Expand Down Expand Up @@ -49,24 +47,20 @@ pub(crate) fn vst_rewriter_remove_dead_assertions(ctx: &AssistContext<'_>, func:
if let vst::Stmt::ExprStmt(ref e) = st {
if let vst::Expr::AssertExpr(_) = *e.expr {
// try if this is redundant
dbg!("lets check of this is redundant", st.to_string());
redundant_assertions.push(st.clone());
let modified_fn = rewriter_rm_assertions(&func, &redundant_assertions)?;
dbg!("trying out on", modified_fn.to_string());
let verif_result = ctx.try_verus(&modified_fn)?;
if !verif_result.is_success {
dbg!("verif fails without this assertion");
// verification failed without this assertion
// remove this assertion from the list
redundant_assertions.pop();
} else {
dbg!("verif succeeds without this assertion");
// verif succeeds without this assertion
if verif_result.time > initial_verif_result.time * 2 {
dbg!("verification time takes a lot longer without this assertion");
// verification time takes a lot longer without this assertion
redundant_assertions.pop();
}
}
dbg!("redundant assertions", redundant_assertions.len());
}
}
}
Expand Down
3 changes: 2 additions & 1 deletion crates/ide-assists/src/vst_api/run_verus.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -146,7 +146,8 @@ impl<'a> AssistContext<'a> {
#[derive(Debug)]
pub(crate) struct VerifResult {
pub(crate) is_success: bool,
// TODO: properly parse json using serde and store the list of assertion/ensures/requires
// FIXME: properly parse json using serde and store the list of assertion/ensures/requires
#[allow(dead_code)]
pub(crate) stdout: String ,
pub(crate) stderr: String,
pub(crate) time: u64,
Expand Down
1 change: 1 addition & 0 deletions crates/syntax/src/ast/generated.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ pub(crate) mod nodes;
#[rustfmt::skip]
pub(crate) mod tokens;
#[rustfmt::skip]
#[allow(unused_mut)]
pub mod vst_nodes;

use crate::{
Expand Down

0 comments on commit 4b98f2d

Please sign in to comment.