From 6b54f20a5b2d011d2a8564ec7d0a61892ed70978 Mon Sep 17 00:00:00 2001 From: Xavier Denis Date: Thu, 9 Nov 2023 16:53:32 +0100 Subject: [PATCH] Adjust behavior of associated types --- creusot/src/backend/clone_map.rs | 12 +- .../should_succeed/lang/assoc_type.mlcfg | 248 +----------------- .../tests/should_succeed/lang/assoc_type.rs | 46 ++-- .../should_succeed/lang/assoc_type.stderr | 10 + .../lang/assoc_type/why3session.xml | 19 +- .../lang/assoc_type/why3shapes.gz | Bin 112 -> 224 bytes 6 files changed, 66 insertions(+), 269 deletions(-) create mode 100644 creusot/tests/should_succeed/lang/assoc_type.stderr diff --git a/creusot/src/backend/clone_map.rs b/creusot/src/backend/clone_map.rs index 1f1636d6bd..51e6d65c23 100644 --- a/creusot/src/backend/clone_map.rs +++ b/creusot/src/backend/clone_map.rs @@ -478,8 +478,16 @@ impl<'tcx> CloneMap<'tcx> { ctx, CloneNode::new(ctx.tcx, (p.def_id, p.substs)).subst(ctx.tcx, key), ); - self.insert(node).public |= key_public; - self.add_graph_edge(key, node); + + let is_type = self + .self_did() + .map(|did| util::item_type(self.tcx, did) == ItemType::Type) + .unwrap_or(false); + + if !is_type { + self.insert(node).public |= key_public; + self.add_graph_edge(key, node); + } } } diff --git a/creusot/tests/should_succeed/lang/assoc_type.mlcfg b/creusot/tests/should_succeed/lang/assoc_type.mlcfg index 53970d661a..2e604e0c6d 100644 --- a/creusot/tests/should_succeed/lang/assoc_type.mlcfg +++ b/creusot/tests/should_succeed/lang/assoc_type.mlcfg @@ -22,6 +22,12 @@ module AssocType_Assoc_Type type t_assoc 'u 'proj0 = | C_Assoc 'proj0 +end +module AssocType_Nested_Type + use AssocType_Assoc_Type as AssocType_Assoc_Type + type t_nested 't 'proj0 = + | C_Nested (AssocType_Assoc_Type.t_assoc 't 'proj0) + end module AssocType_Tr_A_Type type self @@ -51,152 +57,6 @@ module TyInv_Trivial type t = t axiom inv_trivial : forall self : t . Inv0.inv self = true end -module AssocType_Uses_Interface - type a - clone AssocType_Tr_A_Type as A0 with - type self = a - use AssocType_Assoc_Type as AssocType_Assoc_Type - clone CreusotContracts_Invariant_Inv_Stub as Inv0 with - type t = AssocType_Assoc_Type.t_assoc a A0.a - val uses [#"../assoc_type.rs" 12 0 12 31] (_1 : AssocType_Assoc_Type.t_assoc a A0.a) : () - requires {[#"../assoc_type.rs" 1 0 1 0] Inv0.inv _1} - -end -module AssocType_Uses - type a - clone AssocType_Tr_A_Type as A0 with - type self = a - use AssocType_Assoc_Type as AssocType_Assoc_Type - clone AssocType_Tr_A_Type as A1 with - type self = AssocType_Assoc_Type.t_assoc a A0.a - clone CreusotContracts_Invariant_Inv_Interface as Inv0 with - type t = AssocType_Assoc_Type.t_assoc a A0.a - clone TyInv_Trivial as TyInv_Trivial0 with - type t = AssocType_Assoc_Type.t_assoc a A0.a, - predicate Inv0.inv = Inv0.inv, - axiom . - clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve0 with - type self = AssocType_Assoc_Type.t_assoc a A0.a - let rec cfg uses [#"../assoc_type.rs" 12 0 12 31] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : AssocType_Assoc_Type.t_assoc a A0.a) : () - requires {[#"../assoc_type.rs" 1 0 1 0] Inv0.inv _1} - - = [@vc:do_not_keep_trace] [@vc:sp] - var _0 : (); - var _1 : AssocType_Assoc_Type.t_assoc a A0.a = _1; - { - goto BB0 - } - BB0 { - _0 <- (); - assert { [@expl:type invariant] Inv0.inv _1 }; - assume { Resolve0.resolve _1 }; - goto BB1 - } - BB1 { - return _0 - } - -end -module AssocType_Assoc2_Type - type t_assoc2 'u 'f 'b 'proj0 = - | C_Assoc2 'f 'proj0 'b - -end -module AssocType_Uses2_Interface - type c - type x - type y - clone AssocType_Tr_A_Type as A0 with - type self = c - use AssocType_Assoc2_Type as AssocType_Assoc2_Type - clone CreusotContracts_Invariant_Inv_Stub as Inv0 with - type t = AssocType_Assoc2_Type.t_assoc2 c x y A0.a - val uses2 [#"../assoc_type.rs" 20 0 20 45] (_1 : AssocType_Assoc2_Type.t_assoc2 c x y A0.a) : () - requires {[#"../assoc_type.rs" 1 0 1 0] Inv0.inv _1} - -end -module AssocType_Uses2 - type c - type x - type y - clone AssocType_Tr_A_Type as A0 with - type self = c - use AssocType_Assoc2_Type as AssocType_Assoc2_Type - clone AssocType_Tr_A_Type as A1 with - type self = AssocType_Assoc2_Type.t_assoc2 c x y A0.a - clone CreusotContracts_Invariant_Inv_Interface as Inv0 with - type t = AssocType_Assoc2_Type.t_assoc2 c x y A0.a - clone TyInv_Trivial as TyInv_Trivial0 with - type t = AssocType_Assoc2_Type.t_assoc2 c x y A0.a, - predicate Inv0.inv = Inv0.inv, - axiom . - clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve0 with - type self = AssocType_Assoc2_Type.t_assoc2 c x y A0.a - let rec cfg uses2 [#"../assoc_type.rs" 20 0 20 45] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : AssocType_Assoc2_Type.t_assoc2 c x y A0.a) : () - requires {[#"../assoc_type.rs" 1 0 1 0] Inv0.inv _1} - - = [@vc:do_not_keep_trace] [@vc:sp] - var _0 : (); - var _1 : AssocType_Assoc2_Type.t_assoc2 c x y A0.a = _1; - { - goto BB0 - } - BB0 { - _0 <- (); - assert { [@expl:type invariant] Inv0.inv _1 }; - assume { Resolve0.resolve _1 }; - goto BB1 - } - BB1 { - return _0 - } - -end -module AssocType_Fix_Type - use prelude.Int - use prelude.UIntSize - type t_fix = - | C_Fix usize - -end -module AssocType_Mono_Interface - use AssocType_Fix_Type as AssocType_Fix_Type - clone CreusotContracts_Invariant_Inv_Stub as Inv0 with - type t = AssocType_Fix_Type.t_fix - val mono [#"../assoc_type.rs" 30 0 30 19] (_1 : AssocType_Fix_Type.t_fix) : () - requires {[#"../assoc_type.rs" 1 0 1 0] Inv0.inv _1} - -end -module AssocType_Mono - use AssocType_Fix_Type as AssocType_Fix_Type - clone CreusotContracts_Invariant_Inv_Interface as Inv0 with - type t = AssocType_Fix_Type.t_fix - clone TyInv_Trivial as TyInv_Trivial0 with - type t = AssocType_Fix_Type.t_fix, - predicate Inv0.inv = Inv0.inv, - axiom . - let rec cfg mono [#"../assoc_type.rs" 30 0 30 19] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : AssocType_Fix_Type.t_fix) : () - requires {[#"../assoc_type.rs" 1 0 1 0] Inv0.inv _1} - - = [@vc:do_not_keep_trace] [@vc:sp] - var _0 : (); - { - goto BB0 - } - BB0 { - _0 <- (); - return _0 - } - -end -module AssocType_Nested_Type - clone AssocType_Tr_A_Type as A0 with - type self = t - use AssocType_Assoc_Type as AssocType_Assoc_Type - type t_nested 't 'proj0 = - | C_Nested (AssocType_Assoc_Type.t_assoc 't 'proj0) - -end module AssocType_Uses3_Interface type t clone AssocType_Tr_A_Type as A0 with @@ -243,99 +103,3 @@ module AssocType_Uses3 } end -module AssocType_Nested2_Type - use AssocType_Assoc_Type as AssocType_Assoc_Type - type t_nested2 'proj0 = - | C_Nested2 (AssocType_Assoc_Type.t_assoc () 'proj0) - -end -module AssocType_Uses4_Interface - use prelude.Int - use prelude.UIntSize - use AssocType_Nested2_Type as AssocType_Nested2_Type - clone CreusotContracts_Invariant_Inv_Stub as Inv0 with - type t = AssocType_Nested2_Type.t_nested2 usize - val uses4 [#"../assoc_type.rs" 42 0 42 24] (_1 : AssocType_Nested2_Type.t_nested2 usize) : () - requires {[#"../assoc_type.rs" 1 0 1 0] Inv0.inv _1} - -end -module AssocType_Uses4 - use prelude.Int - use prelude.UIntSize - use AssocType_Nested2_Type as AssocType_Nested2_Type - clone CreusotContracts_Invariant_Inv_Interface as Inv0 with - type t = AssocType_Nested2_Type.t_nested2 usize - clone TyInv_Trivial as TyInv_Trivial0 with - type t = AssocType_Nested2_Type.t_nested2 usize, - predicate Inv0.inv = Inv0.inv, - axiom . - let rec cfg uses4 [#"../assoc_type.rs" 42 0 42 24] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : AssocType_Nested2_Type.t_nested2 usize) : () - requires {[#"../assoc_type.rs" 1 0 1 0] Inv0.inv _1} - - = [@vc:do_not_keep_trace] [@vc:sp] - var _0 : (); - { - goto BB0 - } - BB0 { - _0 <- (); - return _0 - } - -end -module AssocType_Map_Type - use prelude.Ghost - use seq.Seq - type t_map 'i 'proj0 = - | C_Map 'i (Ghost.ghost_ty (Seq.seq 'proj0)) - -end -module AssocType_UseMap_Interface - type i - clone AssocType_Tr_A_Type as A0 with - type self = i - use AssocType_Map_Type as AssocType_Map_Type - clone CreusotContracts_Invariant_Inv_Stub as Inv0 with - type t = AssocType_Map_Type.t_map i A0.a - val use_map [#"../assoc_type.rs" 49 0 49 33] (_1 : AssocType_Map_Type.t_map i A0.a) : () - requires {[#"../assoc_type.rs" 1 0 1 0] Inv0.inv _1} - -end -module AssocType_UseMap - type i - clone AssocType_Tr_A_Type as A0 with - type self = i - use AssocType_Map_Type as AssocType_Map_Type - clone AssocType_Tr_A_Type as A1 with - type self = AssocType_Map_Type.t_map i A0.a - clone CreusotContracts_Invariant_Inv_Interface as Inv0 with - type t = AssocType_Map_Type.t_map i A0.a - clone TyInv_Trivial as TyInv_Trivial0 with - type t = AssocType_Map_Type.t_map i A0.a, - predicate Inv0.inv = Inv0.inv, - axiom . - clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve0 with - type self = AssocType_Map_Type.t_map i A0.a - let rec cfg use_map [#"../assoc_type.rs" 49 0 49 33] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : AssocType_Map_Type.t_map i A0.a) : () - requires {[#"../assoc_type.rs" 1 0 1 0] Inv0.inv _1} - - = [@vc:do_not_keep_trace] [@vc:sp] - var _0 : (); - var _1 : AssocType_Map_Type.t_map i A0.a = _1; - { - goto BB0 - } - BB0 { - _0 <- (); - assert { [@expl:type invariant] Inv0.inv _1 }; - assume { Resolve0.resolve _1 }; - goto BB1 - } - BB1 { - return _0 - } - -end -module AssocType_Impl0 - -end diff --git a/creusot/tests/should_succeed/lang/assoc_type.rs b/creusot/tests/should_succeed/lang/assoc_type.rs index a067641524..f738dba4f5 100644 --- a/creusot/tests/should_succeed/lang/assoc_type.rs +++ b/creusot/tests/should_succeed/lang/assoc_type.rs @@ -9,25 +9,25 @@ pub struct Assoc { pub item: U::A, } -pub fn uses(_: Assoc) {} +// pub fn uses(_: Assoc) {} -pub struct Assoc2 { - pub x: F, - pub item: U::A, - pub y: B, -} +// pub struct Assoc2 { +// pub x: F, +// pub item: U::A, +// pub y: B, +// } -pub fn uses2(_: Assoc2) {} +// pub fn uses2(_: Assoc2) {} -impl Tr for () { - type A = usize; -} +// impl Tr for () { +// type A = usize; +// } -pub struct Fix { - pub item: <() as Tr>::A, -} +// pub struct Fix { +// pub item: <() as Tr>::A, +// } -pub fn mono(_: Fix) {} +// pub fn mono(_: Fix) {} pub struct Nested { pub item: Assoc, @@ -35,15 +35,15 @@ pub struct Nested { pub fn uses3(_: Nested) {} -pub struct Nested2 { - pub item: Assoc<()>, -} +// pub struct Nested2 { +// pub item: Assoc<()>, +// } -pub fn uses4(_: Nested2) {} +// pub fn uses4(_: Nested2) {} -pub struct Map { - pub iter: I, - pub produced: Ghost>, -} +// pub struct Map { +// pub iter: I, +// pub produced: Ghost>, +// } -pub fn use_map(_: Map) {} +// pub fn use_map(_: Map) {} diff --git a/creusot/tests/should_succeed/lang/assoc_type.stderr b/creusot/tests/should_succeed/lang/assoc_type.stderr new file mode 100644 index 0000000000..8a540e7a17 --- /dev/null +++ b/creusot/tests/should_succeed/lang/assoc_type.stderr @@ -0,0 +1,10 @@ +warning: unused import: `creusot_contracts::*` + --> assoc_type.rs:2:5 + | +2 | use creusot_contracts::*; + | ^^^^^^^^^^^^^^^^^^^^ + | + = note: `#[warn(unused_imports)]` on by default + +warning: 1 warning emitted + diff --git a/creusot/tests/should_succeed/lang/assoc_type/why3session.xml b/creusot/tests/should_succeed/lang/assoc_type/why3session.xml index 7197f9776e..582474cb26 100644 --- a/creusot/tests/should_succeed/lang/assoc_type/why3session.xml +++ b/creusot/tests/should_succeed/lang/assoc_type/why3session.xml @@ -2,12 +2,27 @@ - + + + + + + - + + + + + + + + + + + diff --git a/creusot/tests/should_succeed/lang/assoc_type/why3shapes.gz b/creusot/tests/should_succeed/lang/assoc_type/why3shapes.gz index 188d45829334071a6c64fbdc63c7989e8fba8670..4dc2c67463d9f4c6d89cda553988491ba31e8972 100644 GIT binary patch literal 224 zcmV<603ZJ!iwFP!00000|8N}k=m@|Zw*P7L?L|oYCSQr2P z95x0Al4@p{$9q}n{z>QB^|fC5VLH9(pjWSI{-VR_I-0GzCGO_ky}Z+AzwUkF5w>dF z=r&#Scdz}16xZ7xD2GAk^6PYi9