Merge pull request #825 from xldenis/resolution-order

Change resolution order

Author: voidc

creusot/src/translation/function.rs

@@ -285,7 +285,9 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
     fn resolve_locals(&mut self, mut locals: BitSet<Local>) {
         locals.subtract(&self.erased_locals.to_hybrid());
 
-        for local in locals.iter() {
+        // TODO determine resolution order based on outlives relation
+        let locals = locals.iter().collect::<Vec<_>>();
+        for local in locals.into_iter().rev() {
             self.emit_resolve(local.into());
         }
     }

creusot/tests/should_fail/bug/692.mlcfg

@@ -539,7 +539,7 @@ module C692_Incorrect
   clone CreusotContracts_Std1_Ops_Impl1_Unnest_Interface as Unnest0 with
     type args = (),
     type f = c
-  clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve0 with
+  clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve1 with
     type self = c
   clone CreusotContracts_Std1_Ops_Impl1_PostconditionMut_Interface as PostconditionMut0 with
     type args = (),
@@ -554,7 +554,7 @@ module C692_Incorrect
     type f = c,
     predicate PostconditionOnce0.postcondition_once = PostconditionOnce0.postcondition_once,
     predicate PostconditionMut0.postcondition_mut = PostconditionMut0.postcondition_mut,
-    predicate Resolve0.resolve = Resolve0.resolve,
+    predicate Resolve0.resolve = Resolve1.resolve,
     type Output0.output = bool,
     axiom .
   clone CreusotContracts_Std1_Ops_Impl1_UnnestTrans_Interface as UnnestTrans0 with
@@ -584,7 +584,7 @@ module C692_Incorrect
     type args = (),
     type f = c,
     predicate PostconditionOnce0.postcondition_once = PostconditionOnce0.postcondition_once,
-    predicate Resolve0.resolve = Resolve0.resolve,
+    predicate Resolve0.resolve = Resolve1.resolve,
     predicate Postcondition0.postcondition = Postcondition0.postcondition,
     type Output0.output = bool,
     axiom .
@@ -602,7 +602,7 @@ module C692_Incorrect
   clone CreusotContracts_Std1_Ops_Impl0_Precondition_Interface as Precondition0 with
     type args = (),
     type f = c
-  clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve1 with
+  clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve0 with
     type self = b
   let rec cfg incorrect [#"../692.rs" 8 0 8 76] [@cfg:stackify] [@cfg:subregion_analysis] (cond : c) (branch : b) : ()
     requires {[#"../692.rs" 5 0 6 87] Precondition0.precondition cond () /\ (forall b : bool . Precondition1.precondition branch (b) /\ (exists b : bool . forall b0 : bool . Postcondition0.postcondition cond () b0 -> b0 = b))}
@@ -616,8 +616,8 @@ module C692_Incorrect
     goto BB0
   }
   BB0 {
-    assume { Resolve0.resolve cond };
-    assume { Resolve1.resolve branch };
+    assume { Resolve0.resolve branch };
+    assume { Resolve1.resolve cond };
     goto BB1
   }
   BB1 {

creusot/tests/should_succeed/bdd.mlcfg

@@ -3910,13 +3910,13 @@ module Bdd_Impl10_And
     return _0
   }
   BB37 {
-    assume { Resolve2.resolve self };
     assume { Resolve1.resolve _25 };
+    assume { Resolve2.resolve self };
     goto BB4
   }
   BB38 {
-    assume { Resolve2.resolve self };
     assume { Resolve1.resolve _25 };
+    assume { Resolve2.resolve self };
     goto BB4
   }
   BB39 {

creusot/tests/should_succeed/bdd/why3shapes.gz

@@ -134,8 +134,8 @@ module EqPanic_Omg
     goto BB1
   }
   BB1 {
-    assume { Resolve0.resolve x };
     assume { Resolve0.resolve y };
+    assume { Resolve0.resolve x };
     return _0
   }
 

creusot/tests/should_succeed/bug/eq_panic.mlcfg

@@ -713,9 +713,9 @@ module C04GenericClosure_Mapper_Closure0
   use export C04GenericClosure_Mapper_Closure0_Type
   use prelude.Borrow
   clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve1 with
-    type self = a
-  clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve0 with
     type self = c04genericclosure_mapper_closure0 a
+  clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve0 with
+    type self = a
   predicate resolve [#"../04_generic_closure.rs" 8 28 8 32] (_1 : c04genericclosure_mapper_closure0 a) =
     [#"../04_generic_closure.rs" 1 0 1 0] true
   predicate unnest [#"../04_generic_closure.rs" 8 28 8 32] (self : c04genericclosure_mapper_closure0 a) (_2 : c04genericclosure_mapper_closure0 a)
@@ -748,8 +748,8 @@ module C04GenericClosure_Mapper_Closure0
   }
   BB0 {
     _0 <- ();
-    assume { Resolve0.resolve _1 };
-    assume { Resolve1.resolve _a };
+    assume { Resolve0.resolve _a };
+    assume { Resolve1.resolve _1 };
     goto BB1
   }
   BB1 {

creusot/tests/should_succeed/closures/04_generic_closure.mlcfg

@@ -23,6 +23,24 @@ module Core_Option_Option_Type
       | C_Some a -> a
       end
 end
+module CreusotContracts_Resolve_Resolve_Resolve_Stub
+  type self
+  predicate resolve (self : self)
+end
+module CreusotContracts_Resolve_Resolve_Resolve_Interface
+  type self
+  predicate resolve (self : self)
+  val resolve (self : self) : bool
+    ensures { result = resolve self }
+    
+end
+module CreusotContracts_Resolve_Resolve_Resolve
+  type self
+  predicate resolve (self : self)
+  val resolve (self : self) : bool
+    ensures { result = resolve self }
+    
+end
 module CreusotContracts_Resolve_Impl1_Resolve_Stub
   type t
   use prelude.Borrow
@@ -44,24 +62,6 @@ module CreusotContracts_Resolve_Impl1_Resolve
   val resolve (self : borrowed t) : bool
     ensures { result = resolve self }
 
-end
-module CreusotContracts_Resolve_Resolve_Resolve_Stub
-  type self
-  predicate resolve (self : self)
-end
-module CreusotContracts_Resolve_Resolve_Resolve_Interface
-  type self
-  predicate resolve (self : self)
-  val resolve (self : self) : bool
-    ensures { result = resolve self }
-    
-end
-module CreusotContracts_Resolve_Resolve_Resolve
-  type self
-  predicate resolve (self : self)
-  val resolve (self : self) : bool
-    ensures { result = resolve self }
-    
 end
 module C05Map_FakeIterator_Item_Type
   type self
@@ -690,11 +690,11 @@ module C05Map_Impl0_Next
     predicate Precondition0.precondition = Precondition0.precondition,
     predicate Postcondition0.postcondition = Postcondition0.postcondition,
     type Output0.output = b
-  clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve1 with
-    type self = Core_Option_Option_Type.t_option a
   use C05Map_Map_Type as C05Map_Map_Type
-  clone CreusotContracts_Resolve_Impl1_Resolve as Resolve0 with
+  clone CreusotContracts_Resolve_Impl1_Resolve as Resolve1 with
     type t = C05Map_Map_Type.t_map i f
+  clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve0 with
+    type self = Core_Option_Option_Type.t_option a
   clone C05Map_FakeIterator_Next_Interface as Next0 with
     type self = i,
     type Item0.item = a
@@ -728,25 +728,25 @@ module C05Map_Impl0_Next
   BB3 {
     e <- Core_Option_Option_Type.some_0 _2;
     _2 <- (let Core_Option_Option_Type.C_Some a = _2 in Core_Option_Option_Type.C_Some (any a));
-    assume { Resolve1.resolve _2 };
+    assume { Resolve0.resolve _2 };
     goto BB6
   }
   BB4 {
-    assume { Resolve0.resolve self };
-    assume { Resolve1.resolve _2 };
+    assume { Resolve0.resolve _2 };
+    assume { Resolve1.resolve self };
     absurd
   }
   BB5 {
-    assume { Resolve0.resolve self };
-    assume { Resolve1.resolve _2 };
+    assume { Resolve0.resolve _2 };
+    assume { Resolve1.resolve self };
     _0 <- Core_Option_Option_Type.C_None;
     goto BB10
   }
   BB6 {
     goto BB7
   }
   BB7 {
-    assume { Resolve0.resolve self };
+    assume { Resolve1.resolve self };
     _0 <- Core_Option_Option_Type.C_Some ([#"../05_map.rs" 20 28 20 42] Call0.call (C05Map_Map_Type.map_func ( * self)) (e));
     e <- any a;
     goto BB8

creusot/tests/should_succeed/closures/05_map.mlcfg

@@ -353,8 +353,8 @@ module ConstrainedTypes_UsesConcreteInstance
     goto BB1
   }
   BB1 {
-    assume { Resolve0.resolve x };
     assume { Resolve0.resolve y };
+    assume { Resolve0.resolve x };
     return _0
   }
 

creusot/tests/should_succeed/constrained_types.mlcfg

@@ -1508,15 +1508,15 @@ module Hashmap_Impl5_Add
       end
   }
   BB12 {
-    assume { Resolve3.resolve key };
     assume { Resolve8.resolve tl1 };
+    assume { Resolve3.resolve key };
     assume { Resolve4.resolve val' };
     v <- { v with current = val' };
     assume { Resolve4.resolve ( * v) };
     assume { Resolve9.resolve v };
-    assume { Resolve6.resolve self };
-    assume { Resolve1.resolve l };
     assume { Resolve1.resolve _19 };
+    assume { Resolve1.resolve l };
+    assume { Resolve6.resolve self };
     assert { [@expl:assertion] [#"../hashmap.rs" 126 32 126 52] HashmapInv0.hashmap_inv ( * self) };
     _0 <- ();
     goto BB20
@@ -1552,8 +1552,8 @@ module Hashmap_Impl5_Add
     goto BB19
   }
   BB19 {
-    assume { Resolve6.resolve self };
     assume { Resolve1.resolve _19 };
+    assume { Resolve6.resolve self };
     assert { [@expl:assertion] [#"../hashmap.rs" 134 24 134 44] HashmapInv0.hashmap_inv ( * self) };
     _0 <- ();
     goto BB20
@@ -1823,8 +1823,8 @@ module Hashmap_Impl5_Get
       end
   }
   BB10 {
-    assume { Resolve2.resolve key };
     assume { Resolve4.resolve tl };
+    assume { Resolve2.resolve key };
     assume { Resolve5.resolve v };
     _0 <- Core_Option_Option_Type.C_Some v;
     goto BB13
@@ -1838,8 +1838,8 @@ module Hashmap_Impl5_Get
     goto BB5
   }
   BB12 {
-    assume { Resolve2.resolve key };
     assume { Resolve1.resolve l };
+    assume { Resolve2.resolve key };
     _0 <- Core_Option_Option_Type.C_None;
     goto BB13
   }
@@ -2161,8 +2161,8 @@ module Hashmap_Impl5_Resize
     goto BB11
   }
   BB11 {
-    assume { Resolve1.resolve _28 };
     assume { Resolve1.resolve _29 };
+    assume { Resolve1.resolve _28 };
     goto BB12
   }
   BB12 {

creusot/tests/should_succeed/hashmap.mlcfg

@@ -71,7 +71,7 @@
     </transf>
     </goal>
     <goal name="add&#39;vc.12.0.2" expl="VC for add" proved="true">
-    <proof prover="1"><result status="valid" time="0.280094" steps="38343"/></proof>
+    <proof prover="1"><result status="valid" time="0.446058" steps="38360"/></proof>
     </goal>
    </transf>
    </goal>
@@ -125,15 +125,15 @@
   </transf>
   </goal>
   <goal name="add&#39;vc.24" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.216853" steps="362156"/></proof>
+  <proof prover="0"><result status="valid" time="0.216853" steps="362150"/></proof>
   </goal>
   <goal name="add&#39;vc.25" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="add&#39;vc.25.0" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.818853" steps="97240"/></proof>
+   <proof prover="1"><result status="valid" time="1.561048" steps="97240"/></proof>
    </goal>
    <goal name="add&#39;vc.25.1" expl="postcondition" proved="true">
-   <proof prover="6"><result status="valid" time="0.411522" steps="7645"/></proof>
+   <proof prover="6"><result status="valid" time="0.829766" steps="7644"/></proof>
    </goal>
   </transf>
   </goal>
@@ -142,7 +142,7 @@
 </theory>
 <theory name="Hashmap_Impl5_Get" proved="true">
  <goal name="get&#39;vc" expl="VC for get" proved="true">
- <proof prover="6"><result status="valid" time="0.155181" steps="4545"/></proof>
+ <proof prover="6"><result status="valid" time="0.622829" steps="4521"/></proof>
  </goal>
 </theory>
 <theory name="Hashmap_Impl5_Resize" proved="true">
@@ -188,7 +188,7 @@
   <proof prover="6"><result status="valid" time="0.020000" steps="106"/></proof>
   </goal>
   <goal name="resize&#39;vc.13" expl="loop invariant init" proved="true">
-  <proof prover="0"><result status="valid" time="0.367055" steps="558331"/></proof>
+  <proof prover="0"><result status="valid" time="0.562446" steps="558331"/></proof>
   </goal>
   <goal name="resize&#39;vc.14" expl="loop invariant init" proved="true">
   <proof prover="6"><result status="valid" time="0.020000" steps="251"/></proof>
@@ -203,19 +203,19 @@
   <proof prover="6"><result status="valid" time="0.010000" steps="97"/></proof>
   </goal>
   <goal name="resize&#39;vc.18" expl="loop invariant preservation" proved="true">
-  <proof prover="6"><result status="valid" time="0.050000" steps="957"/></proof>
+  <proof prover="6"><result status="valid" time="0.174886" steps="957"/></proof>
   </goal>
   <goal name="resize&#39;vc.19" expl="loop invariant preservation" proved="true">
-  <proof prover="6"><result status="valid" time="0.050000" steps="968"/></proof>
+  <proof prover="6"><result status="valid" time="0.174438" steps="969"/></proof>
   </goal>
   <goal name="resize&#39;vc.20" expl="loop invariant preservation" proved="true">
-  <proof prover="1"><result status="valid" time="0.210000" steps="33698"/></proof>
+  <proof prover="1"><result status="valid" time="0.459211" steps="33696"/></proof>
   </goal>
   <goal name="resize&#39;vc.21" expl="loop invariant preservation" proved="true">
   <proof prover="0"><result status="valid" time="0.030000" steps="112407"/></proof>
   </goal>
   <goal name="resize&#39;vc.22" expl="loop invariant preservation" proved="true">
-  <proof prover="6"><result status="valid" time="0.060000" steps="1193"/></proof>
+  <proof prover="6"><result status="valid" time="0.224581" steps="1193"/></proof>
   </goal>
   <goal name="resize&#39;vc.23" expl="unreachable point" proved="true">
   <proof prover="6"><result status="valid" time="0.020000" steps="124"/></proof>
@@ -227,13 +227,13 @@
   <proof prover="6"><result status="valid" time="0.010000" steps="272"/></proof>
   </goal>
   <goal name="resize&#39;vc.26" expl="loop invariant preservation" proved="true">
-  <proof prover="6"><result status="valid" time="0.020000" steps="144"/></proof>
+  <proof prover="6"><result status="valid" time="0.020000" steps="145"/></proof>
   </goal>
   <goal name="resize&#39;vc.27" expl="loop invariant preservation" proved="true">
   <proof prover="6"><result status="valid" time="0.020000" steps="122"/></proof>
   </goal>
   <goal name="resize&#39;vc.28" expl="loop invariant preservation" proved="true">
-  <proof prover="6"><result status="valid" time="0.020000" steps="286"/></proof>
+  <proof prover="6"><result status="valid" time="0.020000" steps="287"/></proof>
   </goal>
   <goal name="resize&#39;vc.29" expl="loop invariant preservation" proved="true">
   <proof prover="6"><result status="valid" time="0.010000" steps="79"/></proof>