Skip to content

Commit

Permalink
Adjust behavior of associated types
Browse files Browse the repository at this point in the history
  • Loading branch information
@xldenis
xldenis committed Nov 9, 2023
1 parent 193ba00 commit 6b54f20
Show file tree
Hide file tree
Showing 6 changed files with 66 additions and 269 deletions.
12 changes: 10 additions & 2 deletions creusot/src/backend/clone_map.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
}
}

Expand Down
248 changes: 6 additions & 242 deletions creusot/tests/should_succeed/lang/assoc_type.mlcfg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
46 changes: 23 additions & 23 deletions creusot/tests/should_succeed/lang/assoc_type.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,41 +9,41 @@ pub struct Assoc<U: Tr> {
pub item: U::A,
}

pub fn uses<A: Tr>(_: Assoc<A>) {}
// pub fn uses<A: Tr>(_: Assoc<A>) {}

pub struct Assoc2<U: Tr, F, B> {
pub x: F,
pub item: U::A,
pub y: B,
}
// pub struct Assoc2<U: Tr, F, B> {
// pub x: F,
// pub item: U::A,
// pub y: B,
// }

pub fn uses2<C: Tr, X, Y>(_: Assoc2<C, X, Y>) {}
// pub fn uses2<C: Tr, X, Y>(_: Assoc2<C, X, Y>) {}

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<T: Tr> {
pub item: Assoc<T>,
}

pub fn uses3<T: Tr>(_: Nested<T>) {}

pub struct Nested2 {
pub item: Assoc<()>,
}
// pub struct Nested2 {
// pub item: Assoc<()>,
// }

pub fn uses4(_: Nested2) {}
// pub fn uses4(_: Nested2) {}

pub struct Map<I: Tr> {
pub iter: I,
pub produced: Ghost<Seq<I::A>>,
}
// pub struct Map<I: Tr> {
// pub iter: I,
// pub produced: Ghost<Seq<I::A>>,
// }

pub fn use_map<I: Tr>(_: Map<I>) {}
// pub fn use_map<I: Tr>(_: Map<I>) {}
10 changes: 10 additions & 0 deletions creusot/tests/should_succeed/lang/assoc_type.stderr
View file
Original file line number Diff line number Diff line change
@@ -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

19 changes: 17 additions & 2 deletions creusot/tests/should_succeed/lang/assoc_type/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,27 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="0" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.4.3" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="mlcfg" proved="true">
<path name=".."/><path name="assoc_type.mlcfg"/>
<theory name="AssocType_Uses" proved="true">
<goal name="uses&#39;vc" expl="VC for uses" proved="true">
<proof prover="1"><result status="valid" time="0.005281" steps="0"/></proof>
</goal>
</theory>
<theory name="AssocType_Uses2" proved="true">
<goal name="uses2&#39;vc" expl="VC for uses2" proved="true">
<proof prover="0"><result status="valid" time="0.008846" steps="0"/></proof>
<proof prover="1"><result status="valid" time="0.008846" steps="0"/></proof>
</goal>
</theory>
<theory name="AssocType_Uses3" proved="true">
<goal name="uses3&#39;vc" expl="VC for uses3" proved="true">
<proof prover="1"><result status="valid" time="0.004414" steps="0"/></proof>
</goal>
</theory>
<theory name="AssocType_UseMap" proved="true">
<goal name="use_map&#39;vc" expl="VC for use_map" proved="true">
<proof prover="1"><result status="valid" time="0.004615" steps="0"/></proof>
</goal>
</theory>
</file>
Expand Down
Binary file modified creusot/tests/should_succeed/lang/assoc_type/why3shapes.gz
View file
Binary file not shown.

0 comments on commit 6b54f20

Please sign in to comment.