[Prover] Fix bug in loop unrolling (#15136)

* fix bug in loop unrolling

* ast generator tests

* decompiler tests

* fix

third_party/move/move-compiler-v2/src/lib.rs

@@ -162,7 +162,6 @@ pub fn run_move_compiler_for_analysis(
     options.whole_program = true; // will set `treat_everything_as_target`
     options = options.set_experiment(Experiment::SPEC_REWRITE, true);
     options = options.set_experiment(Experiment::ATTACH_COMPILED_MODULE, true);
-    options = options.set_experiment(Experiment::CFG_SIMPLIFICATION, false);
     let (env, _units) = run_move_compiler(error_writer, options)?;
     // Reset for subsequent analysis
     env.treat_everything_as_target(false);

third_party/move/move-model/bytecode/ast-generator-tests/tests/abort_example.exp

@@ -18,58 +18,50 @@ public fun m::f($t0|length: u64): u64 {
      var $t5: bool
      var $t6: u64
      var $t7: u64
-     var $t8: u64
-     var $t9: bool
+     var $t8: bool
+     var $t9: u64
      var $t10: u64
      var $t11: u64
-     var $t12: u64
+     var $t12: bool
      var $t13: u64
-     var $t14: bool
+     var $t14: u64
      var $t15: u64
      var $t16: u64
      var $t17: u64
      var $t18: u64
   0: $t3 := copy($t0)
   1: $t4 := 0
   2: $t5 := >($t3, $t4)
-  3: if ($t5) goto 4 else goto 6
+  3: if ($t5) goto 4 else goto 30
   4: label L1
-  5: goto 9
-  6: label L0
-  7: $t6 := 1
-  8: abort($t6)
-  9: label L2
- 10: $t7 := copy($t0)
- 11: $t8 := 100
- 12: $t9 := <($t7, $t8)
- 13: if ($t9) goto 14 else goto 16
- 14: label L4
- 15: goto 19
- 16: label L3
- 17: $t10 := 2
- 18: abort($t10)
- 19: label L5
- 20: $t11 := 0
- 21: $t1 := $t11
- 22: goto 23
- 23: label L10
- 24: $t12 := copy($t1)
- 25: $t13 := copy($t0)
- 26: $t14 := <($t12, $t13)
- 27: if ($t14) goto 28 else goto 34
- 28: label L7
- 29: $t15 := move($t1)
- 30: $t16 := 1
- 31: $t17 := +($t15, $t16)
- 32: $t1 := $t17
- 33: goto 36
- 34: label L6
- 35: goto 38
- 36: label L8
- 37: goto 23
- 38: label L9
- 39: $t18 := move($t1)
- 40: return $t18
+  5: $t6 := copy($t0)
+  6: $t7 := 100
+  7: $t8 := <($t6, $t7)
+  8: if ($t8) goto 9 else goto 27
+  9: label L3
+ 10: $t9 := 0
+ 11: $t1 := $t9
+ 12: goto 13
+ 13: label L6
+ 14: $t10 := copy($t1)
+ 15: $t11 := copy($t0)
+ 16: $t12 := <($t10, $t11)
+ 17: if ($t12) goto 18 else goto 24
+ 18: label L5
+ 19: $t13 := move($t1)
+ 20: $t14 := 1
+ 21: $t15 := +($t13, $t14)
+ 22: $t1 := $t15
+ 23: goto 13
+ 24: label L4
+ 25: $t16 := move($t1)
+ 26: return $t16
+ 27: label L2
+ 28: $t17 := 2
+ 29: abort($t17)
+ 30: label L0
+ 31: $t18 := 1
+ 32: abort($t18)
 }
 
 --- Raw Generated AST
@@ -78,32 +70,32 @@ _t4: u64 = 0;
 _t5: bool = Gt(_t3, _t4);
 loop {
   if (_t5) break;
-  _t6: u64 = 1;
-  Abort(_t6)
+  _t18: u64 = 1;
+  Abort(_t18)
 };
-_t7: u64 = length;
-_t8: u64 = 100;
-_t9: bool = Lt(_t7, _t8);
+_t6: u64 = length;
+_t7: u64 = 100;
+_t8: bool = Lt(_t6, _t7);
 loop {
-  if (_t9) break;
-  _t10: u64 = 2;
-  Abort(_t10)
+  if (_t8) break;
+  _t17: u64 = 2;
+  Abort(_t17)
 };
-_t11: u64 = 0;
-_t1: u64 = _t11;
+_t9: u64 = 0;
+_t1: u64 = _t9;
 loop {
-  _t12: u64 = _t1;
-  _t13: u64 = length;
-  _t14: bool = Lt(_t12, _t13);
-  if (Not(_t14)) break;
-  _t15: u64 = _t1;
-  _t16: u64 = 1;
-  _t17: u64 = Add(_t15, _t16);
-  _t1: u64 = _t17;
+  _t10: u64 = _t1;
+  _t11: u64 = length;
+  _t12: bool = Lt(_t10, _t11);
+  if (Not(_t12)) break;
+  _t13: u64 = _t1;
+  _t14: u64 = 1;
+  _t15: u64 = Add(_t13, _t14);
+  _t1: u64 = _t15;
   continue
 };
-_t18: u64 = _t1;
-return _t18
+_t16: u64 = _t1;
+return _t16
 
 --- Assign-Transformed Generated AST
 loop {