Skip to content

Commit 2789fda

Browse files
Patrick-6Patrick-6
committed
Fix Format
1 parent 886dae1 commit 2789fda

16 files changed

Lines changed: 121 additions & 80 deletions

File tree

‎prusti-common/src/lib.rs‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@
66

77
#![feature(box_patterns)]
88
#![feature(box_syntax)]
9-
109
#![deny(unused_must_use)]
1110
#![warn(clippy::disallowed_types)]
1211

‎prusti-common/src/vir/fixes/ghost_vars.rs‎

Lines changed: 18 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,7 @@
66

77
//! Fix ghost variables.
88
9-
use super::super::polymorphic_vir::ast;
10-
use super::super::polymorphic_vir::cfg;
9+
use super::super::polymorphic_vir::{ast, cfg};
1110
use fxhash::FxHashSet;
1211
use std::mem;
1312

@@ -18,9 +17,7 @@ use std::mem;
1817
/// creating the encoding. Therefore, we fix this with an additional
1918
/// pass that renames all variables declared inside package statements
2019
/// so that they are unique.
21-
pub fn fix_ghost_vars(
22-
mut method: cfg::CfgMethod
23-
) -> cfg::CfgMethod {
20+
pub fn fix_ghost_vars(mut method: cfg::CfgMethod) -> cfg::CfgMethod {
2421
let mut fixer = GhostVarFixer {
2522
package_stmt_count: 0,
2623
vars: None,
@@ -53,12 +50,12 @@ impl GhostVarFixer {
5350
}
5451

5552
impl ast::ExprFolder for GhostVarFixer {
56-
fn fold_local(&mut self, ast::Local {variable, position}: ast::Local) -> ast::Expr {
53+
fn fold_local(&mut self, ast::Local { variable, position }: ast::Local) -> ast::Expr {
5754
match self.vars {
5855
Some(ref vars) if vars.contains(&variable) => {
5956
ast::Expr::local_with_pos(self.fix_name(variable), position)
6057
}
61-
_ => ast::Expr::local_with_pos(variable, position)
58+
_ => ast::Expr::local_with_pos(variable, position),
6259
}
6360
}
6461
}
@@ -68,11 +65,22 @@ impl ast::StmtFolder for GhostVarFixer {
6865
ast::ExprFolder::fold(self, e)
6966
}
7067

71-
fn fold_package_magic_wand(&mut self, ast::PackageMagicWand {magic_wand, package_stmts, label, variables, position}: ast::PackageMagicWand)
72-
-> ast::Stmt {
68+
fn fold_package_magic_wand(
69+
&mut self,
70+
ast::PackageMagicWand {
71+
magic_wand,
72+
package_stmts,
73+
label,
74+
variables,
75+
position,
76+
}: ast::PackageMagicWand,
77+
) -> ast::Stmt {
7378
let magic_wand = self.fold_expr(magic_wand);
7479
self.vars = Some(variables.into_iter().collect());
75-
let package_stmts = package_stmts.into_iter().map(|stmt| self.fold(stmt)).collect();
80+
let package_stmts = package_stmts
81+
.into_iter()
82+
.map(|stmt| self.fold(stmt))
83+
.collect();
7684
let unfixed_vars = self.vars.take().unwrap();
7785
let variables = unfixed_vars
7886
.into_iter()

‎prusti-common/src/vir/macros/high.rs‎

Lines changed: 11 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,24 @@
11
#[macro_export]
22
macro_rules! vir_high_type {
3-
(Int) => {$crate::vir::vir_high::Type::Int};
4-
(Bool) => {$crate::vir::vir_high::Type::Bool};
5-
({$ty:expr}) => { $ty }
3+
(Int) => {
4+
$crate::vir::vir_high::Type::Int
5+
};
6+
(Bool) => {
7+
$crate::vir::vir_high::Type::Bool
8+
};
9+
({$ty:expr}) => {
10+
$ty
11+
};
612
}
713

814
#[macro_export]
915
macro_rules! vir_high_local {
1016
($name:ident : $type:tt) => {
1117
$crate::vir::vir_high::VariableDecl {
1218
name: stringify!($name).to_string(),
13-
ty: $crate::vir_type!($type)
19+
ty: $crate::vir_type!($type),
1420
}
15-
}
21+
};
1622
}
1723

1824
#[macro_export]

‎prusti-common/src/vir/macros/mod.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
11
pub mod polymorphic;
2-
pub mod high;
2+
pub mod high;

‎prusti-common/src/vir/macros/polymorphic.rs‎

Lines changed: 24 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,27 @@
11
#[macro_export]
22
macro_rules! vir_type {
3-
(Int) => {$crate::vir::polymorphic_vir::Type::Int};
4-
(Ref) => {$crate::vir::polymorphic_vir::Type::Ref};
5-
(Bool) => {$crate::vir::polymorphic_vir::Type::Bool};
6-
({$ty:expr}) => { $ty }
3+
(Int) => {
4+
$crate::vir::polymorphic_vir::Type::Int
5+
};
6+
(Ref) => {
7+
$crate::vir::polymorphic_vir::Type::Ref
8+
};
9+
(Bool) => {
10+
$crate::vir::polymorphic_vir::Type::Bool
11+
};
12+
({$ty:expr}) => {
13+
$ty
14+
};
715
}
816

917
#[macro_export]
1018
macro_rules! vir_local {
1119
($name:ident : $type:tt) => {
1220
$crate::vir::polymorphic_vir::LocalVar {
1321
name: stringify!($name).to_string(),
14-
typ: $crate::vir_type!($type)
22+
typ: $crate::vir_type!($type),
1523
}
16-
}
24+
};
1725
}
1826

1927
#[macro_export]
@@ -149,23 +157,26 @@ mod tests {
149157

150158
#[test]
151159
fn forall() {
152-
let expected = Expr::ForAll( ForAll {
160+
let expected = Expr::ForAll(ForAll {
153161
variables: vec![vir_local!(i: Int), vir_local!(j: Int)],
154-
triggers: vec![Trigger::new(vec![vir_expr!{ true }]), Trigger::new(vec![vir_expr!{ false }])],
155-
body: Box::new(vir_expr!{ true }),
162+
triggers: vec![
163+
Trigger::new(vec![vir_expr! { true }]),
164+
Trigger::new(vec![vir_expr! { false }]),
165+
],
166+
body: Box::new(vir_expr! { true }),
156167
position: Position::default(),
157168
});
158169

159-
let actual = vir_expr!{ forall i: Int, j: Int :: {true, false} true };
170+
let actual = vir_expr! { forall i: Int, j: Int :: {true, false} true };
160171

161172
assert_eq!(expected, actual);
162173
}
163174

164175
#[test]
165176
fn expr_passthrough() {
166-
let expr = vir_stmt!{ assert true };
177+
let expr = vir_stmt! { assert true };
167178

168-
assert_eq!(expr, vir_expr!{ [expr] });
169-
assert_eq!(expr, vir_expr!{ ( [expr] ) });
179+
assert_eq!(expr, vir_expr! { [expr] });
180+
assert_eq!(expr, vir_expr! { ( [expr] ) });
170181
}
171182
}

‎prusti-common/src/vir/mod.rs‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,12 @@
44
// License, v. 2.0. If a copy of the MPL was not distributed with this
55
// file, You can obtain one at http://mozilla.org/MPL/2.0/.
66

7-
pub use self::low_to_viper::{ToViperDecl, ToViper};
8-
pub use self::to_graphviz::ToGraphViz;
9-
pub use vir::legacy::*;
10-
pub use vir::polymorphic as polymorphic_vir;
11-
pub use vir::high as vir_high;
7+
pub use self::{
8+
low_to_viper::{ToViper, ToViperDecl},
9+
to_graphviz::ToGraphViz,
10+
};
1211
pub use low_to_viper::Context as LoweringContext;
12+
pub use vir::{high as vir_high, legacy::*, polymorphic as polymorphic_vir};
1313

1414
pub mod fixes;
1515
pub mod optimizations;

‎prusti-common/src/vir/optimizations/folding/expressions.rs‎

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -17,12 +17,9 @@
1717
//! See: <https://github.com/viperproject/silicon/issues/387>
1818
1919
use crate::vir::polymorphic_vir::{ast, cfg, FallibleExprFolder};
20+
use fxhash::{FxHashMap, FxHashSet};
2021
use log::{debug, trace};
21-
use std::{
22-
cmp::Ordering,
23-
mem,
24-
};
25-
use fxhash::{FxHashSet, FxHashMap};
22+
use std::{cmp::Ordering, mem};
2623

2724
pub trait FoldingOptimizer {
2825
#[must_use]
@@ -456,7 +453,7 @@ impl ast::FallibleExprFolder for ExprOptimizer {
456453
}: ast::BinOp,
457454
) -> Result<ast::Expr, ()> {
458455
trace!("fold_bin_op: {} {} {}", op_kind, left, right);
459-
456+
460457
let first_folded = self.fallible_fold_boxed(left)?;
461458
let first_unfoldings = self.get_unfoldings();
462459
let first_requirements = self.get_requirements();
@@ -530,7 +527,12 @@ impl ast::FallibleExprFolder for ExprOptimizer {
530527
position,
531528
}: ast::Cond,
532529
) -> Result<ast::Expr, ()> {
533-
trace!("\n\nfold_cond:\ng = {}\nt = {}\ne = {}", guard, then_expr, else_expr);
530+
trace!(
531+
"\n\nfold_cond:\ng = {}\nt = {}\ne = {}",
532+
guard,
533+
then_expr,
534+
else_expr
535+
);
534536

535537
let guard_folded = self.fallible_fold_boxed(guard)?;
536538
let guard_unfoldings = self.get_unfoldings();
@@ -544,7 +546,6 @@ impl ast::FallibleExprFolder for ExprOptimizer {
544546
let else_unfoldings = self.get_unfoldings();
545547
let else_requirements = self.get_requirements();
546548

547-
548549
let mut conflicts = check_requirements_conflict(&guard_requirements, &then_requirements);
549550
conflicts.extend(check_requirements_conflict(
550551
&guard_requirements,

‎prusti-common/src/vir/optimizations/functions/inliner.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,9 @@
77
//! Inliner of pure functions.
88
99
use crate::vir::polymorphic_vir::{ast, cfg};
10+
use fxhash::FxHashMap;
1011
use log::trace;
1112
use std::mem;
12-
use fxhash::FxHashMap;
1313

1414
/// Convert functions whose body does not depend on arguments such as
1515
///

‎prusti-common/src/vir/optimizations/methods/purifier.rs‎

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,8 @@ use crate::{
1313
config,
1414
vir::polymorphic_vir::{ast, cfg},
1515
};
16-
use std::{
17-
self,
18-
mem,
19-
};
20-
use fxhash::{FxHashSet, FxHashMap};
16+
use fxhash::{FxHashMap, FxHashSet};
17+
use std::{self, mem};
2118

2219
/// Purify vars.
2320
pub fn purify_vars(mut method: cfg::CfgMethod) -> cfg::CfgMethod {

‎prusti-common/src/vir/optimizations/methods/quantifier_fixer.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,10 @@
55
// file, You can obtain one at http://mozilla.org/MPL/2.0/.
66

77
use crate::vir::polymorphic_vir as vir;
8+
use fxhash::FxHashMap;
89
use itertools::Itertools;
910
use log::debug;
1011
use std::mem;
11-
use fxhash::FxHashMap;
1212

1313
/// Optimizations currently done:
1414
///

0 commit comments

Comments
 (0)