Skip to content

Commit

Permalink
Merge pull request #894 from xldenis/fix-resolve-derive
Browse files Browse the repository at this point in the history 
Dont borrow in the resolve derive
  • Loading branch information
@xldenis
xldenis authored Oct 18, 2023
2 parents ba273c9 + 7b95215 commit d6337fc
Show file tree
Hide file tree
Showing 7 changed files with 226 additions and 63 deletions.
10 changes: 5 additions & 5 deletions creusot-contracts-proc/src/derive/resolve.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,8 +14,8 @@ pub fn derive_resolve(input: proc_macro::TokenStream) -> proc_macro::TokenStream
let expanded = quote! {
#[::creusot_contracts::trusted]
impl #impl_generics ::creusot_contracts::Resolve for #name #ty_generics #where_clause {
#[predicate]
#[open]
#[::creusot_contracts::predicate]
#[::creusot_contracts::open]
fn resolve(self) -> bool {
use ::creusot_contracts::Resolve;
#eq
Expand All @@ -33,7 +33,7 @@ fn resolve(base_ident: &Ident, data: &Data) -> TokenStream {
let recurse = fields.named.iter().map(|f| {
let name = &f.ident;
quote_spanned! {f.span()=>
Resolve::resolve(&self.#name)
Resolve::resolve(self.#name)
}
});
quote! {
Expand All @@ -44,7 +44,7 @@ fn resolve(base_ident: &Ident, data: &Data) -> TokenStream {
let recurse = fields.unnamed.iter().enumerate().map(|(i, f)| {
let index = Index::from(i);
quote_spanned! {f.span()=>
Resolve::resolve(&self.#index)
Resolve::resolve(self.#index)
}
});
quote! {
Expand Down Expand Up @@ -101,7 +101,7 @@ fn gen_match_arm<'a, I: Iterator<Item = &'a syn::Field>>(fields: I) -> ArmAcc {
};
let name_1 = format_ident!("{}_1", name_base);

let call = quote!(Resolve::resolve(&#name_1));
let call = quote!(Resolve::resolve(#name_1));
if named {
acc.fields.push(quote!(#name_base: #name_1));
acc.body.push(quote!(#call));
Expand Down
38 changes: 20 additions & 18 deletions creusot/tests/should_succeed/lang/modules.mlcfg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,33 +6,35 @@ module Modules_Nested_Nested_Type
end
module Modules_Nested_Impl0_Resolve_Stub
use Modules_Nested_Nested_Type as Modules_Nested_Nested_Type
predicate resolve [#"../modules.rs" 15 8 15 32] (self : Modules_Nested_Nested_Type.t_nested)
predicate resolve [#"../modules.rs" 7 13 7 20] (self : Modules_Nested_Nested_Type.t_nested)
end
module Modules_Nested_Impl0_Resolve_Interface
use Modules_Nested_Nested_Type as Modules_Nested_Nested_Type
predicate resolve [#"../modules.rs" 15 8 15 32] (self : Modules_Nested_Nested_Type.t_nested)
val resolve [#"../modules.rs" 15 8 15 32] (self : Modules_Nested_Nested_Type.t_nested) : bool
predicate resolve [#"../modules.rs" 7 13 7 20] (self : Modules_Nested_Nested_Type.t_nested)
val resolve [#"../modules.rs" 7 13 7 20] (self : Modules_Nested_Nested_Type.t_nested) : bool
ensures { result = resolve self }

end
module Modules_Nested_Impl0_Resolve
use Modules_Nested_Nested_Type as Modules_Nested_Nested_Type
predicate resolve [#"../modules.rs" 15 8 15 32] (self : Modules_Nested_Nested_Type.t_nested) =
[#"../modules.rs" 16 12 16 16] true
val resolve [#"../modules.rs" 15 8 15 32] (self : Modules_Nested_Nested_Type.t_nested) : bool
predicate resolve [#"../modules.rs" 7 13 7 20] (self : Modules_Nested_Nested_Type.t_nested) =
[#"../modules.rs" 7 13 7 20] match (self) with
| Modules_Nested_Nested_Type.C_Test -> true
end
val resolve [#"../modules.rs" 7 13 7 20] (self : Modules_Nested_Nested_Type.t_nested) : bool
ensures { result = resolve self }

end
module Modules_Nested_InnerFunc_Interface
val inner_func [#"../modules.rs" 21 4 21 31] (_1 : ()) : bool
ensures { [#"../modules.rs" 20 14 20 28] result = true }
val inner_func [#"../modules.rs" 13 4 13 31] (_1 : ()) : bool
ensures { [#"../modules.rs" 12 14 12 28] result = true }

end
module Modules_Nested_InnerFunc
use Modules_Nested_Nested_Type as Modules_Nested_Nested_Type
clone Modules_Nested_Impl0_Resolve as Resolve0
let rec cfg inner_func [#"../modules.rs" 21 4 21 31] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : ()) : bool
ensures { [#"../modules.rs" 20 14 20 28] result = true }
let rec cfg inner_func [#"../modules.rs" 13 4 13 31] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : ()) : bool
ensures { [#"../modules.rs" 12 14 12 28] result = true }

= [@vc:do_not_keep_trace] [@vc:sp]
var _0 : bool;
Expand All @@ -43,34 +45,34 @@ module Modules_Nested_InnerFunc
BB0 {
_2 <- Modules_Nested_Nested_Type.C_Test;
assume { Resolve0.resolve _2 };
_0 <- ([#"../modules.rs" 23 8 23 12] true);
_0 <- ([#"../modules.rs" 15 8 15 12] true);
return _0
}

end
module Modules_Nested_Further_Another_Interface
val another [#"../modules.rs" 27 8 27 32] (_1 : ()) : bool
val another [#"../modules.rs" 19 8 19 32] (_1 : ()) : bool
end
module Modules_Nested_Further_Another
let rec cfg another [#"../modules.rs" 27 8 27 32] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : ()) : bool
let rec cfg another [#"../modules.rs" 19 8 19 32] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : ()) : bool
= [@vc:do_not_keep_trace] [@vc:sp]
var _0 : bool;
{
goto BB0
}
BB0 {
_0 <- ([#"../modules.rs" 28 12 28 17] false);
_0 <- ([#"../modules.rs" 20 12 20 17] false);
return _0
}

end
module Modules_F_Interface
val f [#"../modules.rs" 33 0 33 10] (_1 : ()) : ()
val f [#"../modules.rs" 25 0 25 10] (_1 : ()) : ()
end
module Modules_F
clone Modules_Nested_Further_Another_Interface as Another0
clone Modules_Nested_InnerFunc_Interface as InnerFunc0
let rec cfg f [#"../modules.rs" 33 0 33 10] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : ()) : ()
let rec cfg f [#"../modules.rs" 25 0 25 10] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : ()) : ()
= [@vc:do_not_keep_trace] [@vc:sp]
var _0 : ();
var _1 : bool;
Expand All @@ -79,11 +81,11 @@ module Modules_F
goto BB0
}
BB0 {
_1 <- ([#"../modules.rs" 34 4 34 24] InnerFunc0.inner_func ());
_1 <- ([#"../modules.rs" 26 4 26 24] InnerFunc0.inner_func ());
goto BB1
}
BB1 {
_2 <- ([#"../modules.rs" 36 4 36 13] Another0.another ());
_2 <- ([#"../modules.rs" 28 4 28 13] Another0.another ());
goto BB2
}
BB2 {
Expand Down
10 changes: 1 addition & 9 deletions creusot/tests/should_succeed/lang/modules.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,19 +4,11 @@ extern crate creusot_contracts;
pub mod nested {
use creusot_contracts::*;

#[derive(Resolve)]
enum Nested {
Test,
}

#[trusted]
impl Resolve for Nested {
#[open]
#[predicate]
fn resolve(self) -> bool {
true
}
}

#[ensures(result == true)]
pub fn inner_func() -> bool {
let _ = Nested::Test;
Expand Down
Binary file modified creusot/tests/should_succeed/lang/modules/why3shapes.gz
View file
Binary file not shown.
189 changes: 183 additions & 6 deletions creusot/tests/should_succeed/syntax/derive_macros.mlcfg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1001,6 +1001,28 @@ module DeriveMacros_Product2_Type
| C_Product2 _ _ a -> a
end
end
module CreusotContracts_Resolve_Impl1_Resolve_Stub
type t
use prelude.Borrow
predicate resolve (self : borrowed t)
end
module CreusotContracts_Resolve_Impl1_Resolve_Interface
type t
use prelude.Borrow
predicate resolve (self : borrowed t)
val resolve (self : borrowed t) : bool
ensures { result = resolve self }

end
module CreusotContracts_Resolve_Impl1_Resolve
type t
use prelude.Borrow
predicate resolve (self : borrowed t) =
[#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self
val resolve (self : borrowed t) : bool
ensures { result = resolve self }

end
module CreusotContracts_Resolve_Impl2_Resolve_Stub
type t
predicate resolve (self : t)
Expand All @@ -1019,6 +1041,163 @@ module CreusotContracts_Resolve_Impl2_Resolve
val resolve (self : t) : bool
ensures { result = resolve self }

end
module Core_Num_Impl11_Max_Stub
use prelude.Int
use prelude.UIntSize
val constant mAX' : usize
end
module Core_Num_Impl11_Max
use prelude.Int
use prelude.UIntSize
let constant mAX' : usize = [@vc:do_not_keep_trace] [@vc:sp]
(18446744073709551615 : usize)
end
module CreusotContracts_Std1_Vec_Impl0_ShallowModel_Stub
type t
type a
use seq.Seq
use prelude.UIntSize
use prelude.Int
use seq.Seq
use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
clone CreusotContracts_Invariant_Inv_Stub as Inv1 with
type t = Seq.seq t
clone Core_Num_Impl11_Max_Stub as Max0
clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
type t = Alloc_Vec_Vec_Type.t_vec t a
function shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t
end
module CreusotContracts_Std1_Vec_Impl0_ShallowModel_Interface
type t
type a
use seq.Seq
use prelude.UIntSize
use prelude.Int
use seq.Seq
use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
clone CreusotContracts_Invariant_Inv_Stub as Inv1 with
type t = Seq.seq t
clone Core_Num_Impl11_Max_Stub as Max0
clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
type t = Alloc_Vec_Vec_Type.t_vec t a
function shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t
val shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t
requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self}
ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length result <= UIntSize.to_int Max0.mAX' }
ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv result }
ensures { result = shallow_model self }

axiom shallow_model_spec : forall self : Alloc_Vec_Vec_Type.t_vec t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv (shallow_model self)) && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model self) <= UIntSize.to_int Max0.mAX')
end
module CreusotContracts_Std1_Vec_Impl0_ShallowModel
type t
type a
use seq.Seq
use prelude.UIntSize
use prelude.Int
use seq.Seq
use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
clone CreusotContracts_Invariant_Inv_Stub as Inv1 with
type t = Seq.seq t
clone Core_Num_Impl11_Max_Stub as Max0
clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
type t = Alloc_Vec_Vec_Type.t_vec t a
function shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t
val shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t
requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self}
ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length result <= UIntSize.to_int Max0.mAX' }
ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv result }
ensures { result = shallow_model self }

axiom shallow_model_spec : forall self : Alloc_Vec_Vec_Type.t_vec t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv (shallow_model self)) && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model self) <= UIntSize.to_int Max0.mAX')
end
module CreusotContracts_Logic_Ops_Impl0_IndexLogic_Stub
type t
type a
use prelude.Int
use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
end
module CreusotContracts_Logic_Ops_Impl0_IndexLogic_Interface
type t
type a
use prelude.Int
use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
ensures { result = index_logic self ix }

end
module CreusotContracts_Logic_Ops_Impl0_IndexLogic
type t
type a
use prelude.Int
use seq.Seq
use seq.Seq
clone CreusotContracts_Invariant_Inv_Stub as Inv1 with
type t = Seq.seq t
clone Core_Num_Impl11_Max_Stub as Max0
use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
type t = Alloc_Vec_Vec_Type.t_vec t a
clone CreusotContracts_Std1_Vec_Impl0_ShallowModel_Stub as ShallowModel0 with
type t = t,
type a = a,
predicate Inv0.inv = Inv0.inv,
val Max0.mAX' = Max0.mAX',
predicate Inv1.inv = Inv1.inv,
axiom .
function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
[#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
ensures { result = index_logic self ix }

end
module CreusotContracts_Std1_Vec_Impl10_Resolve_Stub
type t
use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
predicate resolve (self : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global))
end
module CreusotContracts_Std1_Vec_Impl10_Resolve_Interface
type t
use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
predicate resolve (self : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global))
val resolve (self : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)) : bool
ensures { result = resolve self }

end
module CreusotContracts_Std1_Vec_Impl10_Resolve
type t
use prelude.Int
use seq.Seq
use seq.Seq
clone CreusotContracts_Invariant_Inv_Stub as Inv1 with
type t = Seq.seq t
clone Core_Num_Impl11_Max_Stub as Max0
use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
type t = Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)
clone CreusotContracts_Resolve_Resolve_Resolve_Stub as Resolve0 with
type self = t
clone CreusotContracts_Logic_Ops_Impl0_IndexLogic_Stub as IndexLogic0 with
type t = t,
type a = Alloc_Alloc_Global_Type.t_global
clone CreusotContracts_Std1_Vec_Impl0_ShallowModel_Stub as ShallowModel0 with
type t = t,
type a = Alloc_Alloc_Global_Type.t_global,
predicate Inv0.inv = Inv0.inv,
val Max0.mAX' = Max0.mAX',
predicate Inv1.inv = Inv1.inv,
axiom .
predicate resolve (self : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)) =
[#"../../../../../creusot-contracts/src/std/vec.rs" 51 8 51 85] forall i : int . 0 <= i /\ i < Seq.length (ShallowModel0.shallow_model self) -> Resolve0.resolve (IndexLogic0.index_logic self i)
val resolve (self : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)) : bool
ensures { result = resolve self }

end
module DeriveMacros_Impl6_Resolve_Stub
type a
Expand All @@ -1035,17 +1214,16 @@ module DeriveMacros_Impl6_Resolve_Interface
end
module DeriveMacros_Impl6_Resolve
type a
use prelude.Borrow
use prelude.Int
use prelude.UInt32
use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
clone CreusotContracts_Resolve_Impl2_Resolve_Stub as Resolve2 with
type t = Alloc_Vec_Vec_Type.t_vec uint32 (Alloc_Alloc_Global_Type.t_global)
clone CreusotContracts_Std1_Vec_Impl10_Resolve_Stub as Resolve2 with
type t = uint32
clone CreusotContracts_Resolve_Impl2_Resolve_Stub as Resolve1 with
type t = bool
clone CreusotContracts_Resolve_Resolve_Resolve_Stub as Resolve0 with
type self = borrowed a
clone CreusotContracts_Resolve_Impl1_Resolve_Stub as Resolve0 with
type t = a
use DeriveMacros_Product2_Type as DeriveMacros_Product2_Type
predicate resolve [#"../derive_macros.rs" 49 9 49 16] (self : DeriveMacros_Product2_Type.t_product2 a) =
[#"../derive_macros.rs" 51 4 53 15] Resolve0.resolve (DeriveMacros_Product2_Type.product2_a self) /\ Resolve1.resolve (DeriveMacros_Product2_Type.product2_b self) /\ Resolve2.resolve (DeriveMacros_Product2_Type.product2_c self)
Expand Down Expand Up @@ -1077,7 +1255,6 @@ end
module DeriveMacros_Impl7_Resolve
type a
type b
use prelude.Borrow
clone CreusotContracts_Resolve_Resolve_Resolve_Stub as Resolve2 with
type self = b
clone CreusotContracts_Resolve_Impl2_Resolve_Stub as Resolve1 with
Expand Down
Loading

0 comments on commit d6337fc

Please sign in to comment.