Skip to content

Commit de37e90

Browse files
parnoparno
committed
Apply rust-fmt to clean things up
1 parent 8e6e1ae commit de37e90

17 files changed

+241
-119
lines changed

‎verify/air/src/ast.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
use std::rc::Rc;
21
use std::collections::HashMap;
2+
use std::rc::Rc;
33

44
pub type RawSpan = Rc<dyn std::any::Any>;
55
#[derive(Clone)] // for Debug, see ast_util

‎verify/air/src/context.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
use crate::ast::{Command, CommandX, Decl, Ident, Query, SpanOption, TypeError};
2+
use crate::model::Model;
23
use crate::print_parse::Logger;
34
use crate::typecheck::Typing;
4-
use crate::model::Model;
55
use std::collections::{HashMap, HashSet};
66
use std::rc::Rc;
77
use z3::ast::Dynamic;
@@ -85,7 +85,7 @@ impl<'ctx> Context<'ctx> {
8585
pub fn set_debug(&mut self, debug: bool) {
8686
self.debug = debug;
8787
}
88-
88+
8989
pub fn get_debug(&self) -> bool {
9090
self.debug
9191
}

‎verify/air/src/main.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
use air::ast::{CommandX, Span};
2-
use air::context::{Context,ValidityResult};
2+
use air::context::{Context, ValidityResult};
33
use getopts::Options;
44
use sise::Node;
55
use std::fs::File;

‎verify/air/src/model.rs

+16-20
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
1-
use std::collections::{HashMap};
2-
use std::fmt;
3-
use crate::ast::{Decl, DeclX, Ident,SnapShots, Typ, TypX};
1+
use crate::ast::{Decl, DeclX, Ident, SnapShots, Typ, TypX};
42
use crate::context::Context;
3+
use std::collections::HashMap;
4+
use std::fmt;
55
use z3::ast::{Bool, Dynamic, Int};
66
//use z3::{FuncDecl, Sort};
77

88
#[derive(Debug)]
99
pub struct Model<'a> {
1010
z3_model: z3::Model<'a>,
1111
id_snapshots: SnapShots,
12-
value_snapshots: HashMap<Ident, HashMap<Ident, String>>
12+
value_snapshots: HashMap<Ident, HashMap<Ident, String>>,
1313
}
1414

1515
// TODO: Duplicated from smt_verify
@@ -25,21 +25,16 @@ fn new_const<'ctx>(context: &mut Context<'ctx>, name: &String, typ: &Typ) -> Dyn
2525
}
2626
}
2727

28-
2928
impl<'a> Model<'a> {
30-
pub fn new(model: z3::Model<'a>, snapshots:SnapShots) -> Model<'a> {
29+
pub fn new(model: z3::Model<'a>, snapshots: SnapShots) -> Model<'a> {
3130
println!("Creating a new model with {} snapshots", snapshots.len());
32-
Model {
33-
z3_model: model,
34-
id_snapshots: snapshots,
35-
value_snapshots: HashMap::new(),
36-
}
31+
Model { z3_model: model, id_snapshots: snapshots, value_snapshots: HashMap::new() }
3732
}
3833

39-
// pub fn save_snapshots(&self, snapshots: SnapShots) {
40-
// self.snapshots = snapshots.clone();
41-
// }
42-
fn lookup_z3_var(&self, var_name:&String, var_smt:&Dynamic) -> String {
34+
// pub fn save_snapshots(&self, snapshots: SnapShots) {
35+
// self.snapshots = snapshots.clone();
36+
// }
37+
fn lookup_z3_var(&self, var_name: &String, var_smt: &Dynamic) -> String {
4338
if let Some(x) = self.z3_model.eval(var_smt) {
4439
if let Some(b) = x.as_bool() {
4540
format!("{}", b)
@@ -55,17 +50,19 @@ impl<'a> Model<'a> {
5550
}
5651
}
5752

58-
5953
/// Reconstruct an AIR-level model based on the Z3 model
6054
pub fn build(&mut self, context: &mut Context, local_vars: Vec<Decl>) {
61-
println!("Building the AIR model");
55+
println!("Building the AIR model");
6256
for (snap_id, id_snapshot) in &self.id_snapshots {
6357
let mut value_snapshot = HashMap::new();
6458
println!("Snapshot {} has {} variables", snap_id, id_snapshot.len());
6559
for (var_id, var_count) in &*id_snapshot {
6660
let var_name = crate::var_to_const::rename_var(&*var_id, *var_count);
6761
println!("\t{}", var_name);
68-
let var_smt = context.vars.get(&var_name).unwrap_or_else(|| panic!("internal error: variable {} not found", var_name));
62+
let var_smt = context
63+
.vars
64+
.get(&var_name)
65+
.unwrap_or_else(|| panic!("internal error: variable {} not found", var_name));
6966
let val = self.lookup_z3_var(&var_name, var_smt);
7067
value_snapshot.insert(var_id.clone(), val);
7168
}
@@ -86,7 +83,7 @@ impl<'a> Model<'a> {
8683
}
8784
}
8885

89-
pub fn query_variable(&self, snapshot: Ident, name:Ident) -> Option<String> {
86+
pub fn query_variable(&self, snapshot: Ident, name: Ident) -> Option<String> {
9087
Some(self.value_snapshots.get(&snapshot)?.get(&name)?.to_string())
9188
}
9289
}
@@ -103,4 +100,3 @@ impl<'a> fmt::Display for Model<'a> {
103100
Ok(())
104101
}
105102
}
106-

‎verify/air/src/print_parse.rs

+20-2
Original file line numberDiff line numberDiff line change
@@ -513,7 +513,16 @@ pub(crate) fn node_to_expr(node: &Node) -> Result<Expr, String> {
513513
let raw_span = Rc::new(());
514514
let as_string = label[1..label.len() - 1].to_string();
515515
// TODO: Update AIR syntax to support file info
516-
let span = Rc::new(Some(Span { description: None, raw_span, as_string, filename:"".to_string(), start_row:0, start_col: 0, end_row: 0, end_col: 0 }));
516+
let span = Rc::new(Some(Span {
517+
description: None,
518+
raw_span,
519+
as_string,
520+
filename: "".to_string(),
521+
start_row: 0,
522+
start_col: 0,
523+
end_row: 0,
524+
end_col: 0,
525+
}));
517526
let expr = node_to_expr(e)?;
518527
return Ok(Rc::new(ExprX::LabeledAssertion(span, expr)));
519528
}
@@ -716,7 +725,16 @@ pub(crate) fn node_to_stmt(node: &Node) -> Result<Stmt, String> {
716725
let raw_span = Rc::new(());
717726
let as_string = label[1..label.len() - 1].to_string();
718727
// TODO: Update AIR syntax to support file info
719-
let span = Span { description: None, raw_span, as_string, filename:"".to_string(), start_row:0, start_col: 0, end_row: 0, end_col: 0 };
728+
let span = Span {
729+
description: None,
730+
raw_span,
731+
as_string,
732+
filename: "".to_string(),
733+
start_row: 0,
734+
start_col: 0,
735+
end_row: 0,
736+
end_col: 0,
737+
};
720738
let expr = node_to_expr(&e)?;
721739
Ok(Rc::new(StmtX::Assert(Rc::new(Some(span)), expr)))
722740
}

‎verify/air/src/smt_verify.rs

+9-4
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
use crate::ast::{
2-
BinaryOp, BindX, Constant, Decl, DeclX, Expr, ExprX, Ident, MultiOp, Quant, Query, SnapShots, Span, StmtX,
3-
Typ, TypX, UnaryOp,
2+
BinaryOp, BindX, Constant, Decl, DeclX, Expr, ExprX, Ident, MultiOp, Quant, Query, SnapShots,
3+
Span, StmtX, Typ, TypX, UnaryOp,
44
};
55
use crate::context::{AssertionInfo, Context, ValidityResult};
66
use crate::def::{GLOBAL_PREFIX_LABEL, PREFIX_LABEL};
@@ -364,7 +364,7 @@ fn smt_check_assertion<'ctx>(
364364
context: &mut Context<'ctx>,
365365
infos: &Vec<AssertionInfo>,
366366
snapshots: SnapShots,
367-
local_vars: Vec<Decl>, // Expected to be entirely DeclX::Const
367+
local_vars: Vec<Decl>, // Expected to be entirely DeclX::Const
368368
expr: &Expr,
369369
) -> ValidityResult<'ctx> {
370370
let mut discovered_span = Rc::new(None);
@@ -435,7 +435,12 @@ fn smt_check_assertion<'ctx>(
435435
}
436436
}
437437

438-
pub(crate) fn smt_check_query<'ctx>(context: &mut Context<'ctx>, query: &Query, snapshots: SnapShots, local_vars: Vec<Decl>) -> ValidityResult<'ctx> {
438+
pub(crate) fn smt_check_query<'ctx>(
439+
context: &mut Context<'ctx>,
440+
query: &Query,
441+
snapshots: SnapShots,
442+
local_vars: Vec<Decl>,
443+
) -> ValidityResult<'ctx> {
439444
context.smt_log.log_push();
440445
context.solver.push();
441446
context.push_name_scope();

‎verify/air/src/var_to_const.rs

+5-11
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
// Replace declare-var and assign with declare-const and assume
2-
use crate::ast::{BinaryOp, Decl, DeclX, Expr, ExprX, Ident, Query, QueryX, SnapShots, Stmt, StmtX, Typ};
2+
use crate::ast::{
3+
BinaryOp, Decl, DeclX, Expr, ExprX, Ident, Query, QueryX, SnapShots, Stmt, StmtX, Typ,
4+
};
35
use crate::ast_util::string_var;
46
use std::collections::{HashMap, HashSet};
57
use std::rc::Rc;
@@ -12,11 +14,7 @@ pub fn rename_var(x: &String, n: u32) -> String {
1214
if x.ends_with("@") { format!("{}{}", x, n) } else { format!("{}@{}", x, n) }
1315
}
1416

15-
fn lower_expr_visitor(
16-
versions: &HashMap<Ident, u32>,
17-
snapshots: &SnapShots,
18-
expr: &Expr,
19-
) -> Expr {
17+
fn lower_expr_visitor(versions: &HashMap<Ident, u32>, snapshots: &SnapShots, expr: &Expr) -> Expr {
2018
match &**expr {
2119
ExprX::Var(x) if versions.contains_key(x) => {
2220
let xn = rename_var(x, find_version(&versions, x));
@@ -31,11 +29,7 @@ fn lower_expr_visitor(
3129
}
3230
}
3331

34-
fn lower_expr(
35-
versions: &HashMap<Ident, u32>,
36-
snapshots: &SnapShots,
37-
expr: &Expr,
38-
) -> Expr {
32+
fn lower_expr(versions: &HashMap<Ident, u32>, snapshots: &SnapShots, expr: &Expr) -> Expr {
3933
crate::visitor::map_expr_visitor(&expr, &mut |e| lower_expr_visitor(versions, snapshots, e))
4034
}
4135

‎verify/rust_verify/src/context.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
use rustc_middle::ty::TyCtxt;
21
use rustc_hir::Crate;
2+
use rustc_middle::ty::TyCtxt;
33
use rustc_span::source_map::SourceMap;
44

5-
pub struct Context<'tcx,'sm> {
5+
pub struct Context<'tcx, 'sm> {
66
pub(crate) tcx: TyCtxt<'tcx>,
77
pub(crate) krate: &'tcx Crate<'tcx>,
88
pub(crate) source_map: &'sm SourceMap,

‎verify/rust_verify/src/rust_to_vir.rs

+35-11
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,8 @@ use rustc_span::def_id::LocalDefId;
2222
use std::rc::Rc;
2323
use vir::ast::{Krate, KrateX, VirErr};
2424

25-
fn check_item<'tcx,'sm>(
26-
ctxt: &Context<'tcx,'sm>,
25+
fn check_item<'tcx, 'sm>(
26+
ctxt: &Context<'tcx, 'sm>,
2727
vir: &mut KrateX,
2828
id: &ItemId,
2929
item: &'tcx Item<'tcx>,
@@ -58,16 +58,30 @@ fn check_item<'tcx,'sm>(
5858
if let Some(TraitRef { path, hir_ref_id: _ }) = impll.of_trait {
5959
unsupported_err_unless!(
6060
ctxt,
61-
hack_check_def_name(ctxt.tcx, path.res.def_id(), "core", "marker::StructuralEq")
62-
|| hack_check_def_name(ctxt.tcx, path.res.def_id(), "core", "cmp::Eq")
61+
hack_check_def_name(
62+
ctxt.tcx,
63+
path.res.def_id(),
64+
"core",
65+
"marker::StructuralEq"
66+
) || hack_check_def_name(ctxt.tcx, path.res.def_id(), "core", "cmp::Eq")
6367
|| hack_check_def_name(
6468
ctxt.tcx,
6569
path.res.def_id(),
6670
"core",
6771
"marker::StructuralPartialEq"
6872
)
69-
|| hack_check_def_name(ctxt.tcx, path.res.def_id(), "core", "cmp::PartialEq")
70-
|| hack_check_def_name(ctxt.tcx, path.res.def_id(), "builtin", "Structural"),
73+
|| hack_check_def_name(
74+
ctxt.tcx,
75+
path.res.def_id(),
76+
"core",
77+
"cmp::PartialEq"
78+
)
79+
|| hack_check_def_name(
80+
ctxt.tcx,
81+
path.res.def_id(),
82+
"builtin",
83+
"Structural"
84+
),
7185
item.span,
7286
"non_eq_trait_impl",
7387
path
@@ -132,11 +146,21 @@ fn check_item<'tcx,'sm>(
132146
TyKind::Path(QPath::Resolved(_, _path)) => {
133147
for impl_item in impll.items {
134148
// TODO once we have references
135-
unsupported_err!(ctxt, item.span, "unsupported method in impl", impl_item);
149+
unsupported_err!(
150+
ctxt,
151+
item.span,
152+
"unsupported method in impl",
153+
impl_item
154+
);
136155
}
137156
}
138157
_ => {
139-
unsupported_err!(ctxt, item.span, "unsupported impl of non-path type", item);
158+
unsupported_err!(
159+
ctxt,
160+
item.span,
161+
"unsupported impl of non-path type",
162+
item
163+
);
140164
}
141165
}
142166
}
@@ -190,8 +214,8 @@ fn check_module<'tcx>(
190214
Ok(())
191215
}
192216

193-
fn check_foreign_item<'tcx,'sm>(
194-
ctxt: &Context<'tcx,'sm>,
217+
fn check_foreign_item<'tcx, 'sm>(
218+
ctxt: &Context<'tcx, 'sm>,
195219
vir: &mut KrateX,
196220
_id: &ForeignItemId,
197221
item: &'tcx ForeignItem<'tcx>,
@@ -225,7 +249,7 @@ fn check_attr<'tcx>(
225249
Ok(())
226250
}
227251

228-
pub fn crate_to_vir<'tcx,'sm>(ctxt: &Context<'tcx,'sm>) -> Result<Krate, VirErr> {
252+
pub fn crate_to_vir<'tcx, 'sm>(ctxt: &Context<'tcx, 'sm>) -> Result<Krate, VirErr> {
229253
let Crate {
230254
item: _,
231255
exported_macros,

‎verify/rust_verify/src/rust_to_vir_adts.rs

+6-6
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,8 @@ use vir::ast::{DatatypeX, Ident, KrateX, Mode, Variant, VirErr};
1111
use vir::ast_util::{ident_binder, str_ident};
1212
use vir::def::{variant_field_ident, variant_ident, variant_positional_field_ident};
1313

14-
fn check_variant_data<'tcx,'sm>(
15-
ctxt: &Context<'tcx,'sm>,
14+
fn check_variant_data<'tcx, 'sm>(
15+
ctxt: &Context<'tcx, 'sm>,
1616
name: &Ident,
1717
variant_data: &'tcx VariantData<'tcx>,
1818
) -> Variant {
@@ -58,8 +58,8 @@ fn check_variant_data<'tcx,'sm>(
5858
)
5959
}
6060

61-
pub fn check_item_struct<'tcx,'sm>(
62-
ctxt: &Context<'tcx,'sm>,
61+
pub fn check_item_struct<'tcx, 'sm>(
62+
ctxt: &Context<'tcx, 'sm>,
6363
vir: &mut KrateX,
6464
span: Span,
6565
id: &ItemId,
@@ -75,8 +75,8 @@ pub fn check_item_struct<'tcx,'sm>(
7575
Ok(())
7676
}
7777

78-
pub fn check_item_enum<'tcx,'sm>(
79-
ctxt: &Context<'tcx,'sm>,
78+
pub fn check_item_enum<'tcx, 'sm>(
79+
ctxt: &Context<'tcx, 'sm>,
8080
vir: &mut KrateX,
8181
span: Span,
8282
id: &ItemId,

0 commit comments

Comments
 (0)