Skip to content

Commit 72337b7

Browse files
xldenisxldenis
authored
Merge pull request #857 from xldenis/dummy-deep-model
Add deep model derive in dummy contracts
2 parents a72577f + c4a6e4e commit 72337b7

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

54 files changed

+109
-94
lines changed

‎creusot-contracts-dummy/src/lib.rs‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -76,3 +76,8 @@ pub fn maintains(_: TS1, tokens: TS1) -> TS1 {
7676
pub fn open(_: TS1, tokens: TS1) -> TS1 {
7777
tokens
7878
}
79+
80+
#[proc_macro_derive(DeepModel, attributes(DeepModelTy))]
81+
pub fn derive_deep_model(_: TS1) -> TS1 {
82+
TS1::new()
83+
}

‎creusot-contracts-proc/src/derive/deep_model.rs‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,13 +35,20 @@ pub fn derive_deep_model(input: proc_macro::TokenStream) -> proc_macro::TokenStr
3535

3636
let eq = deep_model(&name, &deep_model_ty_name, &input.data);
3737

38+
let open = match vis {
39+
syn::Visibility::Public(_) => quote! {#[open]},
40+
syn::Visibility::Restricted(res) => quote! { #[open(#res)] },
41+
syn::Visibility::Inherited => quote! { #[open(self)] },
42+
};
43+
3844
let expanded = quote! {
3945
#ty
4046

4147
impl #impl_generics ::creusot_contracts::DeepModel for #name #ty_generics #where_clause {
4248
type DeepModelTy = #deep_model_ty_name;
4349

4450
#[ghost]
51+
#open
4552
fn deep_model(self) -> Self::DeepModelTy {
4653
#eq
4754
}

‎creusot-contracts/src/model.rs‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,9 @@ pub trait ShallowModel {
1515
#[cfg(creusot)]
1616
pub use creusot_contracts_proc::DeepModel;
1717

18+
#[cfg(not(creusot))]
19+
pub use creusot_contracts_dummy::DeepModel;
20+
1821
/// The deep model corresponds to the model used for specifying
1922
/// operations such as equality, hash function or ordering, which are
2023
/// computed deeply in a data structure.

‎creusot/tests/should_fail/bug/01_resolve_unsoundness.mlcfg‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -188,7 +188,7 @@ module CreusotContracts_Model_Impl7_ShallowModel
188188
type self = t,
189189
type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
190190
function shallow_model (self : borrowed t) : ShallowModelTy0.shallowModelTy =
191-
[#"../../../../../creusot-contracts/src/model.rs" 98 8 98 31] ShallowModel0.shallow_model ( * self)
191+
[#"../../../../../creusot-contracts/src/model.rs" 101 8 101 31] ShallowModel0.shallow_model ( * self)
192192
val shallow_model (self : borrowed t) : ShallowModelTy0.shallowModelTy
193193
ensures { result = shallow_model self }
194194

‎creusot/tests/should_succeed/100doors.mlcfg‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -549,7 +549,7 @@ module CreusotContracts_Model_Impl5_ShallowModel
549549
type self = t,
550550
type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
551551
function shallow_model (self : t) : ShallowModelTy0.shallowModelTy =
552-
[#"../../../../creusot-contracts/src/model.rs" 80 8 80 31] ShallowModel0.shallow_model self
552+
[#"../../../../creusot-contracts/src/model.rs" 83 8 83 31] ShallowModel0.shallow_model self
553553
val shallow_model (self : t) : ShallowModelTy0.shallowModelTy
554554
ensures { result = shallow_model self }
555555

@@ -686,7 +686,7 @@ module CreusotContracts_Model_Impl7_ShallowModel
686686
type self = t,
687687
type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
688688
function shallow_model (self : borrowed t) : ShallowModelTy0.shallowModelTy =
689-
[#"../../../../creusot-contracts/src/model.rs" 98 8 98 31] ShallowModel0.shallow_model ( * self)
689+
[#"../../../../creusot-contracts/src/model.rs" 101 8 101 31] ShallowModel0.shallow_model ( * self)
690690
val shallow_model (self : borrowed t) : ShallowModelTy0.shallowModelTy
691691
ensures { result = shallow_model self }
692692

‎creusot/tests/should_succeed/bdd.mlcfg‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -170,7 +170,7 @@ module CreusotContracts_Model_Impl7_ShallowModel
170170
type self = t,
171171
type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
172172
function shallow_model (self : borrowed t) : ShallowModelTy0.shallowModelTy =
173-
[#"../../../../creusot-contracts/src/model.rs" 98 8 98 31] ShallowModel0.shallow_model ( * self)
173+
[#"../../../../creusot-contracts/src/model.rs" 101 8 101 31] ShallowModel0.shallow_model ( * self)
174174
val shallow_model (self : borrowed t) : ShallowModelTy0.shallowModelTy
175175
ensures { result = shallow_model self }
176176

@@ -237,7 +237,7 @@ module CreusotContracts_Model_Impl5_ShallowModel
237237
type self = t,
238238
type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
239239
function shallow_model (self : t) : ShallowModelTy0.shallowModelTy =
240-
[#"../../../../creusot-contracts/src/model.rs" 80 8 80 31] ShallowModel0.shallow_model self
240+
[#"../../../../creusot-contracts/src/model.rs" 83 8 83 31] ShallowModel0.shallow_model self
241241
val shallow_model (self : t) : ShallowModelTy0.shallowModelTy
242242
ensures { result = shallow_model self }
243243

@@ -268,7 +268,7 @@ module CreusotContracts_Model_Impl4_DeepModel
268268
type self = t,
269269
type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy
270270
function deep_model (self : t) : DeepModelTy0.deepModelTy =
271-
[#"../../../../creusot-contracts/src/model.rs" 71 8 71 28] DeepModel0.deep_model self
271+
[#"../../../../creusot-contracts/src/model.rs" 74 8 74 28] DeepModel0.deep_model self
272272
val deep_model (self : t) : DeepModelTy0.deepModelTy
273273
ensures { result = deep_model self }
274274

‎creusot/tests/should_succeed/bug/766.mlcfg‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,7 @@ module CreusotContracts_Model_Impl6_DeepModel
100100
type self = t,
101101
type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy
102102
function deep_model (self : borrowed t) : DeepModelTy0.deepModelTy =
103-
[#"../../../../../creusot-contracts/src/model.rs" 89 8 89 28] DeepModel0.deep_model ( * self)
103+
[#"../../../../../creusot-contracts/src/model.rs" 92 8 92 28] DeepModel0.deep_model ( * self)
104104
val deep_model (self : borrowed t) : DeepModelTy0.deepModelTy
105105
ensures { result = deep_model self }
106106

‎creusot/tests/should_succeed/bug/eq_panic.mlcfg‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,7 @@ module CreusotContracts_Model_Impl4_DeepModel
9090
type self = t,
9191
type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy
9292
function deep_model (self : t) : DeepModelTy0.deepModelTy =
93-
[#"../../../../../creusot-contracts/src/model.rs" 71 8 71 28] DeepModel0.deep_model self
93+
[#"../../../../../creusot-contracts/src/model.rs" 74 8 74 28] DeepModel0.deep_model self
9494
val deep_model (self : t) : DeepModelTy0.deepModelTy
9595
ensures { result = deep_model self }
9696

‎creusot/tests/should_succeed/bug/two_phase.mlcfg‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ module CreusotContracts_Model_Impl7_ShallowModel
5353
type self = t,
5454
type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
5555
function shallow_model (self : borrowed t) : ShallowModelTy0.shallowModelTy =
56-
[#"../../../../../creusot-contracts/src/model.rs" 98 8 98 31] ShallowModel0.shallow_model ( * self)
56+
[#"../../../../../creusot-contracts/src/model.rs" 101 8 101 31] ShallowModel0.shallow_model ( * self)
5757
val shallow_model (self : borrowed t) : ShallowModelTy0.shallowModelTy
5858
ensures { result = shallow_model self }
5959

@@ -261,7 +261,7 @@ module CreusotContracts_Model_Impl5_ShallowModel
261261
type self = t,
262262
type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
263263
function shallow_model (self : t) : ShallowModelTy0.shallowModelTy =
264-
[#"../../../../../creusot-contracts/src/model.rs" 80 8 80 31] ShallowModel0.shallow_model self
264+
[#"../../../../../creusot-contracts/src/model.rs" 83 8 83 31] ShallowModel0.shallow_model self
265265
val shallow_model (self : t) : ShallowModelTy0.shallowModelTy
266266
ensures { result = shallow_model self }
267267

‎creusot/tests/should_succeed/cell/02.mlcfg‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -505,7 +505,7 @@ module CreusotContracts_Model_Impl5_ShallowModel
505505
type self = t,
506506
type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
507507
function shallow_model (self : t) : ShallowModelTy0.shallowModelTy =
508-
[#"../../../../../creusot-contracts/src/model.rs" 80 8 80 31] ShallowModel0.shallow_model self
508+
[#"../../../../../creusot-contracts/src/model.rs" 83 8 83 31] ShallowModel0.shallow_model self
509509
val shallow_model (self : t) : ShallowModelTy0.shallowModelTy
510510
ensures { result = shallow_model self }
511511

0 commit comments

Comments
 (0)