From 04a48c5d758add6cb3364175a873b092b686dca0 Mon Sep 17 00:00:00 2001
From: Wolfgang Grieskamp <wgrieskamp@gmail.com>
Date: Sun, 1 Sep 2024 23:51:15 -0700
Subject: [PATCH] [compiler-v2] Ast generator from stackless bytecode

Converter from stackless bytecode into Model AST. We already have one from binary format to stackless.

This will be useful in many places in the stack, not at least for debugging, but also as a potential different approach to decompilation. For the later, we still need to create an AST -> Move translator, today we have only debug dump.

Most of the logic is contained in the single new file `ast_generator.rs`. There is some longer module description, and I refer to there for whats provided.

This is still a prototype, but I'd like to land for iteration. There are some tests in a new test crate `ast-generator-tests`. These call the v2 compiler to compile up to file format, then decompile from there into stackless bytecode, and into AST. However, the best way to test this functionality is to actually integrate it into an `compile-execute == compile-decompile-compile-execute` test on many of our existing tests, and even the framework.
---
 Cargo.lock                                    |   20 +
 Cargo.toml                                    |    2 +
 .../src/bytecode_generator.rs                 |    5 +-
 .../src/env_pipeline/inliner.rs               |    4 +-
 .../move/move-model/bytecode/Cargo.toml       |    1 +
 .../bytecode/ast-generator-tests/Cargo.toml   |   23 +
 .../bytecode/ast-generator-tests/src/lib.rs   |    5 +
 .../tests/conditionals.exp                    |  438 ++++
 .../tests/conditionals.move                   |   38 +
 .../ast-generator-tests/tests/loops.exp       |  465 ++++
 .../ast-generator-tests/tests/loops.move      |   34 +
 .../ast-generator-tests/tests/match.exp       |  299 +++
 .../ast-generator-tests/tests/match.move      |   21 +
 .../ast-generator-tests/tests/testsuite.rs    |  115 +
 .../move/move-model/bytecode/src/astifier.rs  | 1998 +++++++++++++++++
 .../bytecode/src/dataflow_domains.rs          |    9 +-
 .../move/move-model/bytecode/src/lib.rs       |    1 +
 .../bytecode/src/stackless_bytecode.rs        |   31 +-
 .../src/stackless_control_flow_graph.rs       |   47 +-
 third_party/move/move-model/src/ast.rs        |  162 +-
 .../move-model/src/builder/exp_builder.rs     |    6 +-
 .../move/move-model/src/exp_builder.rs        |  178 ++
 .../move/move-model/src/exp_rewriter.rs       |    6 +-
 third_party/move/move-model/src/lib.rs        |    1 +
 third_party/move/move-model/src/model.rs      |   10 +-
 25 files changed, 3884 insertions(+), 35 deletions(-)
 create mode 100644 third_party/move/move-model/bytecode/ast-generator-tests/Cargo.toml
 create mode 100644 third_party/move/move-model/bytecode/ast-generator-tests/src/lib.rs
 create mode 100644 third_party/move/move-model/bytecode/ast-generator-tests/tests/conditionals.exp
 create mode 100644 third_party/move/move-model/bytecode/ast-generator-tests/tests/conditionals.move
 create mode 100644 third_party/move/move-model/bytecode/ast-generator-tests/tests/loops.exp
 create mode 100644 third_party/move/move-model/bytecode/ast-generator-tests/tests/loops.move
 create mode 100644 third_party/move/move-model/bytecode/ast-generator-tests/tests/match.exp
 create mode 100644 third_party/move/move-model/bytecode/ast-generator-tests/tests/match.move
 create mode 100644 third_party/move/move-model/bytecode/ast-generator-tests/tests/testsuite.rs
 create mode 100644 third_party/move/move-model/bytecode/src/astifier.rs
 create mode 100644 third_party/move/move-model/src/exp_builder.rs

diff --git a/Cargo.lock b/Cargo.lock
index 5f619517cfcdb..1608bcc5bfe97 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -4868,6 +4868,19 @@ dependencies = [
  "ansi_term",
 ]
 
+[[package]]
+name = "ast-generator-tests"
+version = "0.1.0"
+dependencies = [
+ "anyhow",
+ "codespan-reporting",
+ "datatest-stable",
+ "move-compiler-v2",
+ "move-model",
+ "move-prover-test-utils",
+ "move-stackless-bytecode",
+]
+
 [[package]]
 name = "async-channel"
 version = "1.9.0"
@@ -11398,6 +11411,7 @@ dependencies = [
  "num 0.4.1",
  "paste",
  "petgraph 0.6.5",
+ "topological-sort",
 ]
 
 [[package]]
@@ -16678,6 +16692,12 @@ dependencies = [
  "tonic 0.11.0",
 ]
 
+[[package]]
+name = "topological-sort"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ea68304e134ecd095ac6c3574494fc62b909f416c4fca77e440530221e549d3d"
+
 [[package]]
 name = "tower"
 version = "0.4.13"
diff --git a/Cargo.toml b/Cargo.toml
index f58a1e238a281..d47d1cc3f8670 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -220,6 +220,7 @@ members = [
     "third_party/move/move-model",
     "third_party/move/move-model/bytecode",
     "third_party/move/move-model/bytecode-test-utils",
+    "third_party/move/move-model/bytecode/ast-generator-tests",
     "third_party/move/move-prover",
     "third_party/move/move-prover/boogie-backend",
     "third_party/move/move-prover/bytecode-pipeline",
@@ -786,6 +787,7 @@ tonic = { version = "0.11.0", features = [
     "zstd",
 ] }
 tonic-reflection = "0.11.0"
+topological-sort = "0.2.2"
 triomphe = "0.1.9"
 tui = "0.19.0"
 typed-arena = "2.0.2"
diff --git a/third_party/move/move-compiler-v2/src/bytecode_generator.rs b/third_party/move/move-compiler-v2/src/bytecode_generator.rs
index e20f3b09bf19e..16248e056d369 100644
--- a/third_party/move/move-compiler-v2/src/bytecode_generator.rs
+++ b/third_party/move/move-compiler-v2/src/bytecode_generator.rs
@@ -447,7 +447,7 @@ impl<'env> Generator<'env> {
                 self.emit_with(*id, |attr| Bytecode::Jump(attr, continue_label));
                 self.emit_with(*id, |attr| Bytecode::Label(attr, break_label));
             },
-            ExpData::LoopCont(id, do_continue) => {
+            ExpData::LoopCont(id, 0, do_continue) => {
                 if let Some(LoopContext {
                     continue_label,
                     break_label,
@@ -463,6 +463,9 @@ impl<'env> Generator<'env> {
                     self.error(*id, "missing enclosing loop statement")
                 }
             },
+            ExpData::LoopCont(_, _, _) => {
+                unimplemented!("continue/break with nesting")
+            },
             ExpData::SpecBlock(id, spec) => {
                 // Map locals in spec to assigned temporaries.
                 let mut replacer = |id, target| {
diff --git a/third_party/move/move-compiler-v2/src/env_pipeline/inliner.rs b/third_party/move/move-compiler-v2/src/env_pipeline/inliner.rs
index 6047eae1a82ab..77a4ce7eefede 100644
--- a/third_party/move/move-compiler-v2/src/env_pipeline/inliner.rs
+++ b/third_party/move/move-compiler-v2/src/env_pipeline/inliner.rs
@@ -800,7 +800,7 @@ impl<'env, 'rewriter> InlinedRewriter<'env, 'rewriter> {
                          (lambda expressions)",
                     )
                 },
-                ExpData::LoopCont(node_id, is_continue) if !post && in_loop == 0 => {
+                ExpData::LoopCont(node_id, _, is_continue) if !post && in_loop == 0 => {
                     let node_loc = env.get_node_loc(*node_id);
                     env.error(
                         &node_loc,
@@ -1046,7 +1046,7 @@ impl<'env, 'rewriter> ExpRewriterFunctions for InlinedRewriter<'env, 'rewriter>
                 self.in_loop += 1;
                 true
             },
-            ExpData::LoopCont(node_id, is_continue) if self.in_loop == 0 => {
+            ExpData::LoopCont(node_id, _, is_continue) if self.in_loop == 0 => {
                 let node_loc = self.env.get_node_loc(*node_id);
                 self.env.error(
                     &node_loc,
diff --git a/third_party/move/move-model/bytecode/Cargo.toml b/third_party/move/move-model/bytecode/Cargo.toml
index 43e0ed1ef7a07..ae85ec999da93 100644
--- a/third_party/move/move-model/bytecode/Cargo.toml
+++ b/third_party/move/move-model/bytecode/Cargo.toml
@@ -24,6 +24,7 @@ log = { workspace = true }
 num = { workspace = true }
 paste = { workspace = true }
 petgraph = { workspace = true }
+topological-sort = { workspace = true }
 
 [dev-dependencies]
 anyhow = { workspace = true }
diff --git a/third_party/move/move-model/bytecode/ast-generator-tests/Cargo.toml b/third_party/move/move-model/bytecode/ast-generator-tests/Cargo.toml
new file mode 100644
index 0000000000000..cb0a9218559ac
--- /dev/null
+++ b/third_party/move/move-model/bytecode/ast-generator-tests/Cargo.toml
@@ -0,0 +1,23 @@
+[package]
+name = "ast-generator-tests"
+version = "0.1.0"
+edition = "2021"
+license = { workspace = true }
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dev-dependencies]
+anyhow = { workspace = true }
+codespan-reporting = { workspace = true, features = ["serde", "serialization"] }
+datatest-stable = { workspace = true }
+move-compiler-v2 = { workspace = true }
+move-model = { workspace = true }
+move-prover-test-utils = { workspace = true }
+
+move-stackless-bytecode = { path = ".." }
+
+[[test]]
+name = "testsuite"
+harness = false
+
+[lib]
+doctest = false
diff --git a/third_party/move/move-model/bytecode/ast-generator-tests/src/lib.rs b/third_party/move/move-model/bytecode/ast-generator-tests/src/lib.rs
new file mode 100644
index 0000000000000..dd271f8c0ff7b
--- /dev/null
+++ b/third_party/move/move-model/bytecode/ast-generator-tests/src/lib.rs
@@ -0,0 +1,5 @@
+// Copyright © Aptos Foundation
+// Parts of the project are originally copyright © Meta Platforms, Inc.
+// SPDX-License-Identifier: Apache-2.0
+
+//! Intentionally empty
diff --git a/third_party/move/move-model/bytecode/ast-generator-tests/tests/conditionals.exp b/third_party/move/move-model/bytecode/ast-generator-tests/tests/conditionals.exp
new file mode 100644
index 0000000000000..ea46a4810faa1
--- /dev/null
+++ b/third_party/move/move-model/bytecode/ast-generator-tests/tests/conditionals.exp
@@ -0,0 +1,438 @@
+
+=== Processing m::if_1 =====================================================
+--- Source
+fun if_1(c: bool): u8 {
+        let result = 0;
+        if (c) {
+            result = 1;
+        };
+        result
+    }
+
+--- Stackless Bytecode
+fun m::if_1($t0|c: bool): u8 {
+     var $t1|result: u8
+     var $t2: u8
+     var $t3: bool
+     var $t4: u8
+     var $t5: u8
+  0: $t2 := 0
+  1: $t1 := $t2
+  2: $t3 := move($t0)
+  3: if ($t3) goto 4 else goto 8
+  4: label L1
+  5: $t4 := 1
+  6: $t1 := $t4
+  7: goto 8
+  8: label L0
+  9: $t5 := move($t1)
+ 10: return $t5
+}
+
+--- Raw Generated AST
+_t2: u8 = 0;
+_t1: u8 = _t2;
+_t3: bool = c;
+loop {
+  if (Not(_t3)) break;
+  _t4: u8 = 1;
+  _t1: u8 = _t4;
+  break
+};
+_t5: u8 = _t1;
+return _t5
+
+--- If-Transformed Generated AST
+_t2: u8 = 0;
+_t1: u8 = _t2;
+_t3: bool = c;
+if _t3 {
+  _t4: u8 = 1;
+  _t1: u8 = _t4
+};
+_t5: u8 = _t1;
+return _t5
+
+--- Assign-Transformed Generated AST
+{
+  let _t1: u8 = 0;
+  if c {
+    _t1: u8 = 1
+  };
+  return _t1
+}
+
+
+=== Processing m::if_else_1 =====================================================
+--- Source
+fun if_else_1(c: bool): u8 {
+        if (c) 1 else 2
+    }
+
+--- Stackless Bytecode
+fun m::if_else_1($t0|c: bool): u8 {
+     var $t1|return: u8
+     var $t2: bool
+     var $t3: u8
+     var $t4: u8
+     var $t5: u8
+  0: $t2 := move($t0)
+  1: if ($t2) goto 2 else goto 6
+  2: label L1
+  3: $t3 := 1
+  4: $t1 := $t3
+  5: goto 10
+  6: label L0
+  7: $t4 := 2
+  8: $t1 := $t4
+  9: goto 10
+ 10: label L2
+ 11: $t5 := move($t1)
+ 12: return $t5
+}
+
+--- Raw Generated AST
+_t2: bool = c;
+loop {
+  loop {
+    if (Not(_t2)) break;
+    _t3: u8 = 1;
+    _t1: u8 = _t3;
+    break[1]
+  };
+  _t4: u8 = 2;
+  _t1: u8 = _t4;
+  break
+};
+_t5: u8 = _t1;
+return _t5
+
+--- If-Transformed Generated AST
+_t2: bool = c;
+if _t2 {
+  _t3: u8 = 1;
+  _t1: u8 = _t3
+} else {
+  _t4: u8 = 2;
+  _t1: u8 = _t4
+};
+_t5: u8 = _t1;
+return _t5
+
+--- Assign-Transformed Generated AST
+{
+  let _t1: u8;
+  if c {
+    _t1: u8 = 1
+  } else {
+    _t1: u8 = 2
+  };
+  return _t1
+}
+
+
+=== Processing m::if_else_2 =====================================================
+--- Source
+fun if_else_2(c: bool, d: bool): u8 {
+        if (c) {
+            if (d) {
+                1
+            } else {
+                2
+            }
+        } else {
+            3
+        }
+    }
+
+--- Stackless Bytecode
+fun m::if_else_2($t0|c: bool, $t1|d: bool): u8 {
+     var $t2|return: u8
+     var $t3: bool
+     var $t4: bool
+     var $t5: u8
+     var $t6: u8
+     var $t7: u8
+     var $t8: u8
+  0: $t3 := move($t0)
+  1: if ($t3) goto 2 else goto 15
+  2: label L1
+  3: $t4 := move($t1)
+  4: if ($t4) goto 5 else goto 9
+  5: label L3
+  6: $t5 := 1
+  7: $t2 := $t5
+  8: goto 13
+  9: label L2
+ 10: $t6 := 2
+ 11: $t2 := $t6
+ 12: goto 13
+ 13: label L4
+ 14: goto 19
+ 15: label L0
+ 16: $t7 := 3
+ 17: $t2 := $t7
+ 18: goto 19
+ 19: label L5
+ 20: $t8 := move($t2)
+ 21: return $t8
+}
+
+--- Raw Generated AST
+_t3: bool = c;
+loop {
+  loop {
+    if (_t3) break;
+    _t7: u8 = 3;
+    _t2: u8 = _t7;
+    break[1]
+  };
+  _t4: bool = d;
+  loop {
+    loop {
+      if (Not(_t4)) break;
+      _t5: u8 = 1;
+      _t2: u8 = _t5;
+      break[1]
+    };
+    _t6: u8 = 2;
+    _t2: u8 = _t6;
+    break
+  };
+  break
+};
+_t8: u8 = _t2;
+return _t8
+
+--- If-Transformed Generated AST
+_t3: bool = c;
+if _t3 {
+  _t4: bool = d;
+  if _t4 {
+    _t5: u8 = 1;
+    _t2: u8 = _t5
+  } else {
+    _t6: u8 = 2;
+    _t2: u8 = _t6
+  }
+} else {
+  _t7: u8 = 3;
+  _t2: u8 = _t7
+};
+_t8: u8 = _t2;
+return _t8
+
+--- Assign-Transformed Generated AST
+{
+  let _t2: u8;
+  if c {
+    if d {
+      _t2: u8 = 1
+    } else {
+      _t2: u8 = 2
+    }
+  } else {
+    _t2: u8 = 3
+  };
+  return _t2
+}
+
+
+=== Processing m::if_else_3 =====================================================
+--- Source
+fun if_else_3(c: bool): u64 {
+        let r = if (c) 1 else 2;
+        r
+    }
+
+--- Stackless Bytecode
+fun m::if_else_3($t0|c: bool): u64 {
+     var $t1|r: u64
+     var $t2: bool
+     var $t3: u64
+     var $t4: u64
+     var $t5: u64
+  0: $t2 := move($t0)
+  1: if ($t2) goto 2 else goto 6
+  2: label L1
+  3: $t3 := 1
+  4: $t1 := $t3
+  5: goto 10
+  6: label L0
+  7: $t4 := 2
+  8: $t1 := $t4
+  9: goto 10
+ 10: label L2
+ 11: $t5 := move($t1)
+ 12: return $t5
+}
+
+--- Raw Generated AST
+_t2: bool = c;
+loop {
+  loop {
+    if (Not(_t2)) break;
+    _t3: u64 = 1;
+    _t1: u64 = _t3;
+    break[1]
+  };
+  _t4: u64 = 2;
+  _t1: u64 = _t4;
+  break
+};
+_t5: u64 = _t1;
+return _t5
+
+--- If-Transformed Generated AST
+_t2: bool = c;
+if _t2 {
+  _t3: u64 = 1;
+  _t1: u64 = _t3
+} else {
+  _t4: u64 = 2;
+  _t1: u64 = _t4
+};
+_t5: u64 = _t1;
+return _t5
+
+--- Assign-Transformed Generated AST
+{
+  let _t1: u64;
+  if c {
+    _t1: u64 = 1
+  } else {
+    _t1: u64 = 2
+  };
+  return _t1
+}
+
+
+=== Processing m::if_else_with_shard_exp =====================================================
+--- Source
+fun if_else_with_shard_exp(x: u64): u64 {
+        let y = x + x;
+        let z = y * y;
+        if (z > 0) z + 1 else z - 1
+    }
+
+--- Stackless Bytecode
+fun m::if_else_with_shard_exp($t0|x: u64): u64 {
+     var $t1|$t5: u64
+     var $t2|$t7: u64 [unused]
+     var $t3: u64
+     var $t4: u64
+     var $t5: u64
+     var $t6: u64
+     var $t7: u64
+     var $t8: u64
+     var $t9: u64
+     var $t10: u64
+     var $t11: bool
+     var $t12: u64
+     var $t13: u64
+     var $t14: u64
+     var $t15: u64
+     var $t16: u64
+     var $t17: u64
+     var $t18: u64
+  0: $t3 := copy($t0)
+  1: $t4 := move($t0)
+  2: $t5 := +($t3, $t4)
+  3: $t0 := $t5
+  4: $t6 := copy($t0)
+  5: $t7 := move($t0)
+  6: $t8 := *($t6, $t7)
+  7: $t0 := $t8
+  8: $t9 := copy($t0)
+  9: $t10 := 0
+ 10: $t11 := >($t9, $t10)
+ 11: if ($t11) goto 12 else goto 18
+ 12: label L1
+ 13: $t12 := move($t0)
+ 14: $t13 := 1
+ 15: $t14 := +($t12, $t13)
+ 16: $t1 := $t14
+ 17: goto 24
+ 18: label L0
+ 19: $t15 := move($t0)
+ 20: $t16 := 1
+ 21: $t17 := -($t15, $t16)
+ 22: $t1 := $t17
+ 23: goto 24
+ 24: label L2
+ 25: $t18 := move($t1)
+ 26: return $t18
+}
+
+--- Raw Generated AST
+_t3: u64 = x;
+_t4: u64 = x;
+_t5: u64 = Add(_t3, _t4);
+x: u64 = _t5;
+_t6: u64 = x;
+_t7: u64 = x;
+_t8: u64 = Mul(_t6, _t7);
+x: u64 = _t8;
+_t9: u64 = x;
+_t10: u64 = 0;
+_t11: bool = Gt(_t9, _t10);
+loop {
+  loop {
+    if (Not(_t11)) break;
+    _t12: u64 = x;
+    _t13: u64 = 1;
+    _t14: u64 = Add(_t12, _t13);
+    _t1: u64 = _t14;
+    break[1]
+  };
+  _t15: u64 = x;
+  _t16: u64 = 1;
+  _t17: u64 = Sub(_t15, _t16);
+  _t1: u64 = _t17;
+  break
+};
+_t18: u64 = _t1;
+return _t18
+
+--- If-Transformed Generated AST
+_t3: u64 = x;
+_t4: u64 = x;
+_t5: u64 = Add(_t3, _t4);
+x: u64 = _t5;
+_t6: u64 = x;
+_t7: u64 = x;
+_t8: u64 = Mul(_t6, _t7);
+x: u64 = _t8;
+_t9: u64 = x;
+_t10: u64 = 0;
+_t11: bool = Gt(_t9, _t10);
+if _t11 {
+  _t12: u64 = x;
+  _t13: u64 = 1;
+  _t14: u64 = Add(_t12, _t13);
+  _t1: u64 = _t14
+} else {
+  _t15: u64 = x;
+  _t16: u64 = 1;
+  _t17: u64 = Sub(_t15, _t16);
+  _t1: u64 = _t17
+};
+_t18: u64 = _t1;
+return _t18
+
+--- Assign-Transformed Generated AST
+{
+  let _t1: u64;
+  {
+    let x: u64 = Add(x, x);
+    {
+      let x: u64 = Mul(x, x);
+      if Gt(x, 0) {
+        _t1: u64 = Add(x, 1)
+      } else {
+        _t1: u64 = Sub(x, 1)
+      };
+      return _t1
+    }
+  }
+}
diff --git a/third_party/move/move-model/bytecode/ast-generator-tests/tests/conditionals.move b/third_party/move/move-model/bytecode/ast-generator-tests/tests/conditionals.move
new file mode 100644
index 0000000000000..f7b1261d66cb7
--- /dev/null
+++ b/third_party/move/move-model/bytecode/ast-generator-tests/tests/conditionals.move
@@ -0,0 +1,38 @@
+module 0x815::m {
+
+    fun if_else_1(c: bool): u8 {
+        if (c) 1 else 2
+    }
+
+    fun if_else_2(c: bool, d: bool): u8 {
+        if (c) {
+            if (d) {
+                1
+            } else {
+                2
+            }
+        } else {
+            3
+        }
+    }
+
+
+    fun if_1(c: bool): u8 {
+        let result = 0;
+        if (c) {
+            result = 1;
+        };
+        result
+    }
+
+    fun if_else_3(c: bool): u64 {
+        let r = if (c) 1 else 2;
+        r
+    }
+
+    fun if_else_with_shard_exp(x: u64): u64 {
+        let y = x + x;
+        let z = y * y;
+        if (z > 0) z + 1 else z - 1
+    }
+}
diff --git a/third_party/move/move-model/bytecode/ast-generator-tests/tests/loops.exp b/third_party/move/move-model/bytecode/ast-generator-tests/tests/loops.exp
new file mode 100644
index 0000000000000..7437f0f349ad5
--- /dev/null
+++ b/third_party/move/move-model/bytecode/ast-generator-tests/tests/loops.exp
@@ -0,0 +1,465 @@
+
+=== Processing m::loop_1 =====================================================
+--- Source
+fun loop_1(c: u64): u64 {
+        loop {
+            c = c + 1;
+            if (c % 2 == 0) continue;
+            c = c + 3;
+            if (c % 2 == 1) break;
+        };
+        c
+    }
+
+--- Stackless Bytecode
+fun m::loop_1($t0|c: u64): u64 {
+     var $t1|$t3: u64 [unused]
+     var $t2: u64
+     var $t3: u64
+     var $t4: u64
+     var $t5: u64
+     var $t6: u64
+     var $t7: u64
+     var $t8: u64
+     var $t9: bool
+     var $t10: u64
+     var $t11: u64
+     var $t12: u64
+     var $t13: u64
+     var $t14: u64
+     var $t15: u64
+     var $t16: u64
+     var $t17: bool
+     var $t18: u64
+  0: label L2
+  1: $t2 := move($t0)
+  2: $t3 := 1
+  3: $t4 := +($t2, $t3)
+  4: $t0 := $t4
+  5: $t5 := copy($t0)
+  6: $t6 := 2
+  7: $t7 := %($t5, $t6)
+  8: $t8 := 0
+  9: $t9 := ==($t7, $t8)
+ 10: if ($t9) goto 11 else goto 13
+ 11: label L1
+ 12: goto 0
+ 13: label L0
+ 14: $t10 := move($t0)
+ 15: $t11 := 3
+ 16: $t12 := +($t10, $t11)
+ 17: $t0 := $t12
+ 18: $t13 := copy($t0)
+ 19: $t14 := 2
+ 20: $t15 := %($t13, $t14)
+ 21: $t16 := 1
+ 22: $t17 := ==($t15, $t16)
+ 23: if ($t17) goto 24 else goto 26
+ 24: label L4
+ 25: goto 28
+ 26: label L3
+ 27: goto 0
+ 28: label L5
+ 29: $t18 := move($t0)
+ 30: return $t18
+}
+
+--- Raw Generated AST
+loop {
+  _t2: u64 = c;
+  _t3: u64 = 1;
+  _t4: u64 = Add(_t2, _t3);
+  c: u64 = _t4;
+  _t5: u64 = c;
+  _t6: u64 = 2;
+  _t7: u64 = Mod(_t5, _t6);
+  _t8: u64 = 0;
+  _t9: bool = Eq(_t7, _t8);
+  if (_t9) continue;
+  _t10: u64 = c;
+  _t11: u64 = 3;
+  _t12: u64 = Add(_t10, _t11);
+  c: u64 = _t12;
+  _t13: u64 = c;
+  _t14: u64 = 2;
+  _t15: u64 = Mod(_t13, _t14);
+  _t16: u64 = 1;
+  _t17: bool = Eq(_t15, _t16);
+  if (Not(_t17)) continue;
+  break
+};
+_t18: u64 = c;
+return _t18
+
+--- If-Transformed Generated AST
+loop {
+  _t2: u64 = c;
+  _t3: u64 = 1;
+  _t4: u64 = Add(_t2, _t3);
+  c: u64 = _t4;
+  _t5: u64 = c;
+  _t6: u64 = 2;
+  _t7: u64 = Mod(_t5, _t6);
+  _t8: u64 = 0;
+  _t9: bool = Eq(_t7, _t8);
+  if (_t9) continue;
+  _t10: u64 = c;
+  _t11: u64 = 3;
+  _t12: u64 = Add(_t10, _t11);
+  c: u64 = _t12;
+  _t13: u64 = c;
+  _t14: u64 = 2;
+  _t15: u64 = Mod(_t13, _t14);
+  _t16: u64 = 1;
+  _t17: bool = Eq(_t15, _t16);
+  if (Not(_t17)) continue;
+  break
+};
+_t18: u64 = c;
+return _t18
+
+--- Assign-Transformed Generated AST
+loop {
+  c: u64 = Add(c, 1);
+  if (Eq(Mod(c, 2), 0)) continue;
+  c: u64 = Add(c, 3);
+  if (Not(Eq(Mod(c, 2), 1))) continue;
+  break
+};
+return c
+
+
+=== Processing m::while_1 =====================================================
+--- Source
+fun while_1(c: u64) {
+        while (c > 0) c = c - 1
+    }
+
+--- Stackless Bytecode
+fun m::while_1($t0|c: u64) {
+     var $t1|$t2: u64 [unused]
+     var $t2: u64
+     var $t3: u64
+     var $t4: bool
+     var $t5: u64
+     var $t6: u64
+     var $t7: u64
+  0: label L4
+  1: $t2 := copy($t0)
+  2: $t3 := 0
+  3: $t4 := >($t2, $t3)
+  4: if ($t4) goto 5 else goto 11
+  5: label L1
+  6: $t5 := move($t0)
+  7: $t6 := 1
+  8: $t7 := -($t5, $t6)
+  9: $t0 := $t7
+ 10: goto 13
+ 11: label L0
+ 12: goto 15
+ 13: label L2
+ 14: goto 0
+ 15: label L3
+ 16: return ()
+}
+
+--- Raw Generated AST
+loop {
+  _t2: u64 = c;
+  _t3: u64 = 0;
+  _t4: bool = Gt(_t2, _t3);
+  loop {
+    if (Not(_t4)) break;
+    _t5: u64 = c;
+    _t6: u64 = 1;
+    _t7: u64 = Sub(_t5, _t6);
+    c: u64 = _t7;
+    continue[1]
+  };
+  break
+};
+return Tuple()
+
+--- If-Transformed Generated AST
+loop {
+  _t2: u64 = c;
+  _t3: u64 = 0;
+  _t4: bool = Gt(_t2, _t3);
+  if _t4 {
+    _t5: u64 = c;
+    _t6: u64 = 1;
+    _t7: u64 = Sub(_t5, _t6);
+    c: u64 = _t7;
+    continue
+  };
+  break
+};
+return Tuple()
+
+--- Assign-Transformed Generated AST
+loop {
+  if Gt(c, 0) {
+    {
+      let c: u64 = Sub(c, 1);
+      continue
+    }
+  };
+  break
+};
+return Tuple()
+
+
+=== Processing m::while_2 =====================================================
+--- Source
+fun while_2(c: u64): u64 {
+        while (c > 0) {
+            if (c >= 10) {
+                c = c - 10
+            }
+        };
+        c = c + 1;
+        c
+    }
+
+--- Stackless Bytecode
+fun m::while_2($t0|c: u64): u64 {
+     var $t1|$t3: u64 [unused]
+     var $t2: u64
+     var $t3: u64
+     var $t4: bool
+     var $t5: u64
+     var $t6: u64
+     var $t7: bool
+     var $t8: u64
+     var $t9: u64
+     var $t10: u64
+     var $t11: u64
+     var $t12: u64
+     var $t13: u64
+  0: label L6
+  1: $t2 := copy($t0)
+  2: $t3 := 0
+  3: $t4 := >($t2, $t3)
+  4: if ($t4) goto 5 else goto 18
+  5: label L1
+  6: $t5 := copy($t0)
+  7: $t6 := 10
+  8: $t7 := >=($t5, $t6)
+  9: if ($t7) goto 10 else goto 16
+ 10: label L3
+ 11: $t8 := move($t0)
+ 12: $t9 := 10
+ 13: $t10 := -($t8, $t9)
+ 14: $t0 := $t10
+ 15: goto 16
+ 16: label L2
+ 17: goto 20
+ 18: label L0
+ 19: goto 22
+ 20: label L4
+ 21: goto 0
+ 22: label L5
+ 23: $t11 := move($t0)
+ 24: $t12 := 1
+ 25: $t13 := +($t11, $t12)
+ 26: return $t13
+}
+
+--- Raw Generated AST
+loop {
+  _t2: u64 = c;
+  _t3: u64 = 0;
+  _t4: bool = Gt(_t2, _t3);
+  loop {
+    if (Not(_t4)) break;
+    _t5: u64 = c;
+    _t6: u64 = 10;
+    _t7: bool = Ge(_t5, _t6);
+    if (Not(_t7)) continue[1];
+    _t8: u64 = c;
+    _t9: u64 = 10;
+    _t10: u64 = Sub(_t8, _t9);
+    c: u64 = _t10;
+    continue[1]
+  };
+  break
+};
+_t11: u64 = c;
+_t12: u64 = 1;
+_t13: u64 = Add(_t11, _t12);
+return _t13
+
+--- If-Transformed Generated AST
+loop {
+  _t2: u64 = c;
+  _t3: u64 = 0;
+  _t4: bool = Gt(_t2, _t3);
+  if _t4 {
+    _t5: u64 = c;
+    _t6: u64 = 10;
+    _t7: bool = Ge(_t5, _t6);
+    if (Not(_t7)) continue;
+    _t8: u64 = c;
+    _t9: u64 = 10;
+    _t10: u64 = Sub(_t8, _t9);
+    c: u64 = _t10;
+    continue
+  };
+  break
+};
+_t11: u64 = c;
+_t12: u64 = 1;
+_t13: u64 = Add(_t11, _t12);
+return _t13
+
+--- Assign-Transformed Generated AST
+loop {
+  if Gt(c, 0) {
+    if (Not(Ge(c, 10))) continue;
+    c: u64 = Sub(c, 10);
+    continue
+  };
+  break
+};
+return Add(c, 1)
+
+
+=== Processing m::while_3 =====================================================
+--- Source
+fun while_3(c: u64): u64 {
+        while (c > 0) {
+            while (c > 10) c = c - 10;
+            c = c - 1;
+        };
+        c
+    }
+
+--- Stackless Bytecode
+fun m::while_3($t0|c: u64): u64 {
+     var $t1|$t3: u64 [unused]
+     var $t2: u64
+     var $t3: u64
+     var $t4: bool
+     var $t5: u64
+     var $t6: u64
+     var $t7: bool
+     var $t8: u64
+     var $t9: u64
+     var $t10: u64
+     var $t11: u64
+     var $t12: u64
+     var $t13: u64
+     var $t14: u64
+  0: label L8
+  1: $t2 := copy($t0)
+  2: $t3 := 0
+  3: $t4 := >($t2, $t3)
+  4: if ($t4) goto 5 else goto 26
+  5: label L1
+  6: $t5 := copy($t0)
+  7: $t6 := 10
+  8: $t7 := >($t5, $t6)
+  9: if ($t7) goto 10 else goto 16
+ 10: label L3
+ 11: $t8 := move($t0)
+ 12: $t9 := 10
+ 13: $t10 := -($t8, $t9)
+ 14: $t0 := $t10
+ 15: goto 18
+ 16: label L2
+ 17: goto 20
+ 18: label L4
+ 19: goto 5
+ 20: label L5
+ 21: $t11 := move($t0)
+ 22: $t12 := 1
+ 23: $t13 := -($t11, $t12)
+ 24: $t0 := $t13
+ 25: goto 28
+ 26: label L0
+ 27: goto 30
+ 28: label L6
+ 29: goto 0
+ 30: label L7
+ 31: $t14 := move($t0)
+ 32: return $t14
+}
+
+--- Raw Generated AST
+loop {
+  _t2: u64 = c;
+  _t3: u64 = 0;
+  _t4: bool = Gt(_t2, _t3);
+  loop {
+    if (Not(_t4)) break;
+    loop {
+      _t5: u64 = c;
+      _t6: u64 = 10;
+      _t7: bool = Gt(_t5, _t6);
+      loop {
+        if (Not(_t7)) break;
+        _t8: u64 = c;
+        _t9: u64 = 10;
+        _t10: u64 = Sub(_t8, _t9);
+        c: u64 = _t10;
+        continue[1]
+      };
+      break
+    };
+    _t11: u64 = c;
+    _t12: u64 = 1;
+    _t13: u64 = Sub(_t11, _t12);
+    c: u64 = _t13;
+    continue[1]
+  };
+  break
+};
+_t14: u64 = c;
+return _t14
+
+--- If-Transformed Generated AST
+loop {
+  _t2: u64 = c;
+  _t3: u64 = 0;
+  _t4: bool = Gt(_t2, _t3);
+  if _t4 {
+    loop {
+      _t5: u64 = c;
+      _t6: u64 = 10;
+      _t7: bool = Gt(_t5, _t6);
+      if _t7 {
+        _t8: u64 = c;
+        _t9: u64 = 10;
+        _t10: u64 = Sub(_t8, _t9);
+        c: u64 = _t10;
+        continue
+      };
+      break
+    };
+    _t11: u64 = c;
+    _t12: u64 = 1;
+    _t13: u64 = Sub(_t11, _t12);
+    c: u64 = _t13;
+    continue
+  };
+  break
+};
+_t14: u64 = c;
+return _t14
+
+--- Assign-Transformed Generated AST
+loop {
+  if Gt(c, 0) {
+    loop {
+      if Gt(c, 10) {
+        c: u64 = Sub(c, 10);
+        continue
+      };
+      break
+    };
+    c: u64 = Sub(c, 1);
+    continue
+  };
+  break
+};
+return c
diff --git a/third_party/move/move-model/bytecode/ast-generator-tests/tests/loops.move b/third_party/move/move-model/bytecode/ast-generator-tests/tests/loops.move
new file mode 100644
index 0000000000000..95a671341c962
--- /dev/null
+++ b/third_party/move/move-model/bytecode/ast-generator-tests/tests/loops.move
@@ -0,0 +1,34 @@
+module 0x815::m {
+
+    fun while_1(c: u64) {
+        while (c > 0) c = c - 1
+    }
+
+    fun while_2(c: u64): u64 {
+        while (c > 0) {
+            if (c >= 10) {
+                c = c - 10
+            }
+        };
+        c = c + 1;
+        c
+    }
+
+    fun while_3(c: u64): u64 {
+        while (c > 0) {
+            while (c > 10) c = c - 10;
+            c = c - 1;
+        };
+        c
+    }
+
+    fun loop_1(c: u64): u64 {
+        loop {
+            c = c + 1;
+            if (c % 2 == 0) continue;
+            c = c + 3;
+            if (c % 2 == 1) break;
+        };
+        c
+    }
+}
diff --git a/third_party/move/move-model/bytecode/ast-generator-tests/tests/match.exp b/third_party/move/move-model/bytecode/ast-generator-tests/tests/match.exp
new file mode 100644
index 0000000000000..e8a60a0487de5
--- /dev/null
+++ b/third_party/move/move-model/bytecode/ast-generator-tests/tests/match.exp
@@ -0,0 +1,299 @@
+
+=== Processing m::id =====================================================
+--- Source
+fun id(self: &Entity): u64 {
+        match (self) {
+            Person{id} => *id,
+            Institution{id, ..} => *id
+        }
+    }
+
+--- Stackless Bytecode
+fun m::id($t0|self: &m::Entity): u64 {
+     var $t1|return: u64
+     var $t2: &m::Entity
+     var $t3: bool
+     var $t4: &m::Entity
+     var $t5: &u64
+     var $t6: u64
+     var $t7: &m::Entity
+     var $t8: bool
+     var $t9: &m::Entity
+     var $t10: &u64
+     var $t11: u64
+     var $t12: &m::Entity
+     var $t13: u64
+     var $t14: u64
+  0: $t2 := copy($t0)
+  1: $t3 := test_variant m::Entity::Person($t2)
+  2: if ($t3) goto 3 else goto 9
+  3: label L1
+  4: $t4 := move($t0)
+  5: $t5 := borrow_variant_field<m::Entity::Person>.id($t4)
+  6: $t6 := read_ref($t5)
+  7: $t1 := $t6
+  8: goto 24
+  9: label L0
+ 10: $t7 := copy($t0)
+ 11: $t8 := test_variant m::Entity::Institution($t7)
+ 12: if ($t8) goto 13 else goto 19
+ 13: label L4
+ 14: $t9 := move($t0)
+ 15: $t10 := borrow_variant_field<m::Entity::Institution>.id($t9)
+ 16: $t11 := read_ref($t10)
+ 17: $t1 := $t11
+ 18: goto 24
+ 19: label L3
+ 20: $t12 := move($t0)
+ 21: drop($t12)
+ 22: $t13 := 14566554180833181697
+ 23: abort($t13)
+ 24: label L2
+ 25: $t14 := move($t1)
+ 26: return $t14
+}
+
+--- Raw Generated AST
+_t2: &m::Entity = self;
+_t3: bool = test_variants m::Entity::Person(_t2);
+loop {
+  loop {
+    if (Not(_t3)) break;
+    _t4: &m::Entity = self;
+    _t5: &u64 = select_variants m::Entity.id(_t4);
+    _t6: u64 = Deref(_t5);
+    _t1: u64 = _t6;
+    break[1]
+  };
+  _t7: &m::Entity = self;
+  _t8: bool = test_variants m::Entity::Institution(_t7);
+  loop {
+    loop {
+      if (Not(_t8)) break;
+      _t9: &m::Entity = self;
+      _t10: &u64 = select_variants m::Entity.id(_t9);
+      _t11: u64 = Deref(_t10);
+      _t1: u64 = _t11;
+      break[1]
+    };
+    _t12: &m::Entity = self;
+    _t13: u64 = 14566554180833181697;
+    Abort(_t13)
+  };
+  break
+};
+_t14: u64 = _t1;
+return _t14
+
+--- If-Transformed Generated AST
+_t2: &m::Entity = self;
+_t3: bool = test_variants m::Entity::Person(_t2);
+if _t3 {
+  _t4: &m::Entity = self;
+  _t5: &u64 = select_variants m::Entity.id(_t4);
+  _t6: u64 = Deref(_t5);
+  _t1: u64 = _t6
+} else {
+  _t7: &m::Entity = self;
+  _t8: bool = test_variants m::Entity::Institution(_t7);
+  if _t8 {
+    _t9: &m::Entity = self;
+    _t10: &u64 = select_variants m::Entity.id(_t9);
+    _t11: u64 = Deref(_t10);
+    _t1: u64 = _t11
+  } else {
+    _t12: &m::Entity = self;
+    _t13: u64 = 14566554180833181697;
+    Abort(_t13)
+  }
+};
+_t14: u64 = _t1;
+return _t14
+
+--- Assign-Transformed Generated AST
+{
+  let _t1: u64;
+  if test_variants m::Entity::Person(self) {
+    _t1: u64 = Deref(select_variants m::Entity.id(self))
+  } else {
+    if test_variants m::Entity::Institution(self) {
+      _t1: u64 = Deref(select_variants m::Entity.id(self))
+    } else {
+      Abort(14566554180833181697)
+    }
+  };
+  return _t1
+}
+
+
+=== Processing m::id2 =====================================================
+--- Source
+fun id2(self: Entity): u64 {
+        match (self) {
+            Person{id} if id > 0 => id,
+            Institution{id, ..} => id,
+            _ => 0
+        }
+    }
+
+--- Stackless Bytecode
+fun m::id2($t0|self: m::Entity): u64 {
+     var $t1|$t2: &m::Entity
+     var $t2|$t5: u64
+     var $t3: &m::Entity
+     var $t4: &m::Entity
+     var $t5: bool
+     var $t6: &m::Entity
+     var $t7: &u64
+     var $t8: u64
+     var $t9: u64
+     var $t10: bool
+     var $t11: &m::Entity
+     var $t12: m::Entity
+     var $t13: u64
+     var $t14: &m::Entity
+     var $t15: bool
+     var $t16: m::Entity
+     var $t17: u64
+     var $t18: u64
+     var $t19: u64
+     var $t20: u64
+  0: $t3 := borrow_local($t0)
+  1: $t1 := $t3
+  2: $t4 := copy($t1)
+  3: $t5 := test_variant m::Entity::Person($t4)
+  4: if ($t5) goto 5 else goto 19
+  5: label L1
+  6: $t6 := copy($t1)
+  7: $t7 := borrow_variant_field<m::Entity::Person>.id($t6)
+  8: $t8 := read_ref($t7)
+  9: $t9 := 0
+ 10: $t10 := >($t8, $t9)
+ 11: if ($t10) goto 12 else goto 19
+ 12: label L2
+ 13: $t11 := move($t1)
+ 14: drop($t11)
+ 15: $t12 := move($t0)
+ 16: $t13 := unpack_variant m::Entity::Person($t12)
+ 17: $t2 := $t13
+ 18: goto 33
+ 19: label L0
+ 20: $t14 := move($t1)
+ 21: $t15 := test_variant m::Entity::Institution($t14)
+ 22: if ($t15) goto 23 else goto 29
+ 23: label L5
+ 24: $t16 := move($t0)
+ 25: ($t17, $t18) := unpack_variant m::Entity::Institution($t16)
+ 26: drop($t18)
+ 27: $t2 := $t17
+ 28: goto 33
+ 29: label L4
+ 30: $t19 := 0
+ 31: $t2 := $t19
+ 32: goto 33
+ 33: label L3
+ 34: $t20 := move($t2)
+ 35: return $t20
+}
+
+--- Raw Generated AST
+_t3: &m::Entity = Borrow(Immutable)(self);
+_t1: &m::Entity = _t3;
+_t4: &m::Entity = _t1;
+_t5: bool = test_variants m::Entity::Person(_t4);
+loop {
+  loop {
+    if (Not(_t5)) break;
+    _t6: &m::Entity = _t1;
+    _t7: &u64 = select_variants m::Entity.id(_t6);
+    _t8: u64 = Deref(_t7);
+    _t9: u64 = 0;
+    _t10: bool = Gt(_t8, _t9);
+    if (Not(_t10)) break;
+    _t11: &m::Entity = _t1;
+    _t12: m::Entity = self;
+    m::Entity::Person{ id: _t13 } = _t12;
+    _t2: u64 = _t13;
+    break[1]
+  };
+  _t14: &m::Entity = _t1;
+  _t15: bool = test_variants m::Entity::Institution(_t14);
+  loop {
+    loop {
+      if (Not(_t15)) break;
+      _t16: m::Entity = self;
+      m::Entity::Institution{ id: _t17, admin: _t18 } = _t16;
+      _t2: u64 = _t17;
+      break[1]
+    };
+    _t19: u64 = 0;
+    _t2: u64 = _t19;
+    break
+  };
+  break
+};
+_t20: u64 = _t2;
+return _t20
+
+--- If-Transformed Generated AST
+_t3: &m::Entity = Borrow(Immutable)(self);
+_t1: &m::Entity = _t3;
+_t4: &m::Entity = _t1;
+_t5: bool = test_variants m::Entity::Person(_t4);
+loop {
+  loop {
+    if (Not(_t5)) break;
+    _t6: &m::Entity = _t1;
+    _t7: &u64 = select_variants m::Entity.id(_t6);
+    _t8: u64 = Deref(_t7);
+    _t9: u64 = 0;
+    _t10: bool = Gt(_t8, _t9);
+    if (Not(_t10)) break;
+    _t11: &m::Entity = _t1;
+    _t12: m::Entity = self;
+    m::Entity::Person{ id: _t13 } = _t12;
+    _t2: u64 = _t13;
+    break[1]
+  };
+  _t14: &m::Entity = _t1;
+  _t15: bool = test_variants m::Entity::Institution(_t14);
+  if _t15 {
+    _t16: m::Entity = self;
+    m::Entity::Institution{ id: _t17, admin: _t18 } = _t16;
+    _t2: u64 = _t17
+  } else {
+    _t19: u64 = 0;
+    _t2: u64 = _t19
+  };
+  break
+};
+_t20: u64 = _t2;
+return _t20
+
+--- Assign-Transformed Generated AST
+{
+  let _t2: u64;
+  {
+    let _t1: &m::Entity = Borrow(Immutable)(self);
+    loop {
+      loop {
+        if (Not(test_variants m::Entity::Person(_t1))) break;
+        if (Not(Gt(Deref(select_variants m::Entity.id(_t1)), 0))) break;
+        {
+          let m::Entity::Person{ id: _t13 } = self;
+          break[1]
+        }
+      };
+      if test_variants m::Entity::Institution(_t1) {
+        {
+          let m::Entity::Institution{ id: _t17, admin: _t18 } = self;
+          _t2: u64 = _t17
+        }
+      } else {
+        _t2: u64 = 0
+      };
+      break
+    };
+    return _t2
+  }
+}
diff --git a/third_party/move/move-model/bytecode/ast-generator-tests/tests/match.move b/third_party/move/move-model/bytecode/ast-generator-tests/tests/match.move
new file mode 100644
index 0000000000000..451429e02f126
--- /dev/null
+++ b/third_party/move/move-model/bytecode/ast-generator-tests/tests/match.move
@@ -0,0 +1,21 @@
+module 0x815::m {
+    enum Entity has drop {
+        Person { id: u64 },
+        Institution { id: u64, admin: u64 }
+    }
+
+    fun id(self: &Entity): u64 {
+        match (self) {
+            Person{id} => *id,
+            Institution{id, ..} => *id
+        }
+    }
+
+    fun id2(self: Entity): u64 {
+        match (self) {
+            Person{id} if id > 0 => id,
+            Institution{id, ..} => id,
+            _ => 0
+        }
+    }
+}
diff --git a/third_party/move/move-model/bytecode/ast-generator-tests/tests/testsuite.rs b/third_party/move/move-model/bytecode/ast-generator-tests/tests/testsuite.rs
new file mode 100644
index 0000000000000..a4b78b63a7759
--- /dev/null
+++ b/third_party/move/move-model/bytecode/ast-generator-tests/tests/testsuite.rs
@@ -0,0 +1,115 @@
+// Copyright © Aptos Foundation
+// Parts of the project are originally copyright © Meta Platforms, Inc.
+// SPDX-License-Identifier: Apache-2.0
+
+use codespan_reporting::term::termcolor::Buffer;
+use move_compiler_v2::{logging, run_move_compiler_for_analysis, Options};
+use move_model::{metadata::LanguageVersion, model::GlobalEnv};
+use move_prover_test_utils::{baseline_test, extract_test_directives};
+use move_stackless_bytecode::{
+    astifier,
+    function_target::FunctionTarget,
+    function_target_pipeline::{FunctionTargetsHolder, FunctionVariant},
+};
+use std::path::{Path, PathBuf};
+
+/// Extension for expected output files
+pub const EXP_EXT: &str = "exp";
+
+datatest_stable::harness!(test_runner, "tests", r".*\.move$");
+
+fn test_runner(path: &Path) -> datatest_stable::Result<()> {
+    logging::setup_logging_for_testing();
+    let path_str = path.display().to_string();
+    let mut options = Options {
+        sources_deps: extract_test_directives(path, "// dep:")?,
+        sources: vec![path_str.clone()],
+        dependencies: if extract_test_directives(path, "// no-stdlib")?.is_empty() {
+            vec![path_from_crate_root("../../../move-stdlib/sources")]
+        } else {
+            vec![]
+        },
+        named_address_mapping: vec!["std=0x1".to_string()],
+        ..Options::default()
+    };
+    options = options.set_language_version(LanguageVersion::V2_1);
+    let mut test_output = String::new();
+    let mut error_writer = Buffer::no_color();
+    match run_move_compiler_for_analysis(&mut error_writer, options) {
+        Err(_) => {
+            test_output.push_str(&format!(
+                "--- Aborting with compilation errors:\n{}\n",
+                String::from_utf8_lossy(&error_writer.into_inner())
+            ));
+        },
+        Ok(env) => {
+            let targets = create_targets(&env);
+            for fun_id in targets.get_funs() {
+                generate_output(
+                    &targets.get_target(&env.get_function(fun_id), &FunctionVariant::Baseline),
+                    &mut test_output,
+                )
+            }
+        },
+    }
+    // Generate/check baseline.
+    let baseline_path = path.with_extension(EXP_EXT);
+    baseline_test::verify_or_update_baseline(baseline_path.as_path(), &test_output)?;
+    Ok(())
+}
+
+fn generate_output(target: &FunctionTarget, test_output: &mut String) {
+    *test_output += &format!(
+        "\n=== Processing {} ===================================================== \n",
+        target.func_env.get_full_name_str()
+    );
+    *test_output += &format!(
+        "--- Source\n{}\n",
+        target
+            .global_env()
+            .get_source(&target.get_loc())
+            .unwrap_or("UNKNOWN")
+    );
+
+    *test_output += &format!("\n--- Stackless Bytecode\n{}\n", target);
+
+    let Some(exp) = astifier::generate_ast_raw(target) else {
+        *test_output += "--- Raw Generated AST\nFAILED\n";
+        return;
+    };
+    *test_output += &format!(
+        "--- Raw Generated AST\n{}\n\n",
+        exp.display_for_fun(target.func_env.clone())
+    );
+    let exp = astifier::transform_conditionals(target, exp);
+    *test_output += &format!(
+        "--- If-Transformed Generated AST\n{}\n\n",
+        exp.display_for_fun(target.func_env.clone())
+    );
+    let exp = astifier::transform_assigns(target, exp);
+    *test_output += &format!(
+        "--- Assign-Transformed Generated AST\n{}\n\n",
+        exp.display_for_fun(target.func_env.clone())
+    );
+}
+
+/// Create function targets with stackless bytecode for modules which are target.
+/// This decompiles Move binary format into stackless bytecode.
+fn create_targets(env: &GlobalEnv) -> FunctionTargetsHolder {
+    let mut targets = FunctionTargetsHolder::default();
+    for module_env in env.get_modules() {
+        if module_env.is_primary_target() {
+            for func_env in module_env.get_functions() {
+                targets.add_target(&func_env)
+            }
+        }
+    }
+    targets
+}
+
+/// Returns a path relative to the crate root.
+fn path_from_crate_root(path: &str) -> String {
+    let mut buf = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
+    buf.push(path);
+    buf.to_string_lossy().to_string()
+}
diff --git a/third_party/move/move-model/bytecode/src/astifier.rs b/third_party/move/move-model/bytecode/src/astifier.rs
new file mode 100644
index 0000000000000..f3b0e2e6002ec
--- /dev/null
+++ b/third_party/move/move-model/bytecode/src/astifier.rs
@@ -0,0 +1,1998 @@
+// Copyright © Aptos Foundation
+// Parts of the project are originally copyright © Meta Platforms, Inc.
+// SPDX-License-Identifier: Apache-2.0
+
+//! Converts stackless bytecode into Model AST.
+//!
+//! See [this article](https://medium.com/leaningtech/solving-the-structured-control-flow-problem-once-and-for-all-5123117b1ee2)
+//! for an introduction into how this code works. This is an excellent high-level overview of
+//! the decompilation problem and the solution which is adapted here. The article is a relative
+//! light read and hence leaves many details open, which an implementation has to determine.
+//!
+//! In a nutshell, the decompilation fromm stackless bytecode into the Model AST here
+//! works in the steps outlined below
+//!
+//! # 1. Cleanup
+//!
+//! The code is cleaned up such that there are no jump proxies if the form `label L; goto L1`.
+//! Also, adjacent sequential blocks are merged, and fallthroughs extended by explicit jumps.
+//! It is important for the algorithm to work that all those intermediate blocks are removed
+//! and all remaining blocks represent a true branching structure.
+//!
+//! # 2. Loop Analysis
+//!
+//! Compute loop information using the `fat_loop` module. This allows to distinguish
+//! backward jumps from forward jumps. The fat_loop bails out if the control graph is
+//! not reducible.
+//!
+//! # 3. Topological Sorting
+//!
+//! Topological sort the blocks using forward edges only. For those blocks which are not related
+//! in the partial order, prioritize that for a branch `if c goto L1 else goto L2`, target
+//! blocks follow after the branch. Moreover, for any blocks belonging to a loop, ensure that
+//! they are all appear before any blocks which are part of the loop.
+//!
+//! # 4. Raw AST Generation
+//!
+//! The article linked above describes well how blocks can be used to synthesize structured
+//! code. However, it leaves open when to open blocks and when to close them.
+//!
+//! First, in Move, we express blocks (whether they have back jumps and are proper loops or not)
+//! by `loop { ..; break }`. Now, in the presence of nested `break[n]` and `continue[n]`, any
+//! forward (via break) and backward (via continue) jump can be modelled.
+//!
+//! ## 4.1 Opening Loops
+//!
+//! Loops are opened when we either encounter a loop header or a branch. We know what block
+//! a loop header is and what are the back edges from (2) above. tIn the case of
+//! branches we need two loops. Consider bytecode for an if-then-else
+//!
+//! ```ignore
+//!   if c goto L1 else goto L2
+//!   label L1
+//!   .. then ..
+//!   goto L3
+//!   label L2
+//!   .. else ..
+//!   goto L3
+//!   label L3
+//!   .. end ..
+//! ```
+//!
+//! This is translated to:
+//!
+//! ```ignore
+//! loop {
+//!   loop {
+//!     if !c break;
+//!     .. then ..
+//!     break[1]
+//!   } // L2 jumps here
+//!   .. else ..
+//!   break
+//! } // L3 jumps here
+//! ```
+//!
+//! Notice at the point when those two loops are opened (on encountering
+//! `if c goto L1 else goto L2`), the label `L3` is not known. It appears
+//! somewhere later in the sequence of blocks, with an arbitrary number
+//! of other blocks in between resulting from nested control flows.
+//! The algorithm continues to process the blocks in topological
+//! order, opening sub-blocks as needed, until it encounters a jump
+//! to a label which is not yet associated with any loop, which is then
+//! associated with the unbound loop label. In the above bytecode example, this
+//! would be the first `jump L3` in sequence. This is sound
+//! because of the way how the blocks were sorted in (3): there are no
+//! "interleaving" control flows (as also mentioned in the linked article),
+//! and at the moment `L3` is encountered, no other sub-graphs of the control flow
+//! have still open blocks.
+//!
+//! ## 4.2 Closing Loops
+//!
+//! Loops are closed when their exit label is reached. For the above
+//! example, the inner loop is closed on bytecode `label L2` and the
+//! outer on `label 3`. Some loops which have been opened may never
+//! be associated with a label (for example, in an
+//! `if goto L1 else goto L2` where one of the targets is a back jump
+//! in a loop). Those are closed when an enclosing loop's label
+//! is reached.
+//!
+//! # 5. AST Transformations
+//!
+//! Once the raw AST has been generated as described above, it is
+//! run through a few transformation steps:
+//!
+//! 1. *Conditional Transformation* discovers if-then-else
+//!    expressions from the nested loops as generated by the core
+//!    algorithm. This is based on pattern matching against the AST.
+//!    It is possible that the rules used here need to be extended
+//!    over time, as it is kind of heuristic.
+//! 2. *Assignment Transformation* removes obsoletes assignments
+//!    by propagating reaching definitions. It also introduces
+//!    `let` declarations for temporaries scoped to a block.
+//!
+//! A number of tools are defined in this module to perform AST
+//! transformations, including a data flow analysis
+//! framework for ASTs in the form as generated by the core
+//! algorithms. They are kept local here but can be pulled
+//! out of this module if more general use cases arise.
+
+use crate::{
+    dataflow_domains::{AbstractDomain, JoinResult, MapDomain, SetDomain},
+    fat_loop::{build_loop_info, FatLoopFunctionInfo},
+    function_target::FunctionTarget,
+    stackless_bytecode::{AttrId, Bytecode, Label, Operation as BytecodeOperation},
+    stackless_control_flow_graph::{BlockId, StacklessControlFlowGraph},
+};
+use abstract_domain_derive::AbstractDomain;
+use itertools::Itertools;
+use log::{debug, log_enabled, Level};
+use move_binary_format::file_format::CodeOffset;
+use move_model::{
+    ast::{Exp, ExpData, Operation, Pattern, TempIndex},
+    exp_builder::ExpBuilder,
+    exp_rewriter::ExpRewriterFunctions,
+    model::{GlobalEnv, Loc, NodeId, QualifiedInstId, StructId},
+    symbol::Symbol,
+    ty::{ReferenceKind, Type},
+};
+use std::collections::{BTreeMap, BTreeSet};
+use topological_sort::TopologicalSort;
+
+const DEBUG: bool = false;
+
+// ===========================================================================================
+// Ast Generator
+
+/// Main entry point for generating AST for a given function target with associated stackless
+/// bytecode.
+pub fn generate_ast(target: &FunctionTarget) -> Option<Exp> {
+    let exp = generate_ast_raw(target)?;
+    Some(transform_assigns(
+        target,
+        transform_conditionals(target, exp),
+    ))
+}
+
+/// Entry point for raw generation, without prettifying the AST.
+pub fn generate_ast_raw(target: &FunctionTarget) -> Option<Exp> {
+    // First cleanup the code. In order to make the algorithm work, unnecessary blocks need to
+    // be eliminated.
+    let cleanup_context = Context::new(target);
+    let cleaned_code = cleanup_context.clean_bytecode();
+    let mut new_data = target.data.clone();
+    new_data.code = cleaned_code;
+    let target = FunctionTarget::new(target.func_env, &new_data);
+
+    // Now create a new context for working with the cleaned code.
+    let mut ctx = Context::new(&target);
+
+    let unreached_labels = ctx
+        // All labels with corresponding blocks in code.
+        .forward_cfg
+        .blocks()
+        .iter()
+        .filter_map(|blk_id| ctx.label_of_block(*blk_id))
+        .collect();
+
+    let fat_loop_info = match build_loop_info(&target) {
+        // Compute the fat loops of this code. A fat loop is a loop with multiple back-edges all
+        // sharing the same loop header.
+        Ok(loop_info) => loop_info,
+        Err(err) => {
+            // This happens if the cfg is not reducible.
+            // TODO: we may want to have a fallback strategy for this case. We can generate
+            //   a big outer loop with a case for each block and a variable holding the current
+            //   block number.
+            target.global_env().error(
+                &target.get_loc(),
+                &format!("cannot decompile function: {}", err),
+            );
+            return None;
+        },
+    };
+    ctx.compute_loop_info(&fat_loop_info);
+
+    // Create the generator and run it.
+    let mut gen = Generator {
+        block_stack: vec![],
+        unreached_labels,
+        used_labels: BTreeSet::new(),
+        current_attr: None,
+    };
+    Some(gen.gen(&ctx))
+}
+
+// -------------------------------------------------------------------------------------------
+// Data Types
+
+/// Immutable context used for generation.
+struct Context<'a> {
+    /// The function target.
+    target: &'a FunctionTarget<'a>,
+    /// Forward control flow graph of the given code.
+    forward_cfg: StacklessControlFlowGraph,
+    /// Expression builder.
+    builder: ExpBuilder<'a>,
+    /// Mapping from labels to the code offset they are associated with.
+    label_offsets: BTreeMap<Label, CodeOffset>,
+    /// Loop headers. These are the labels of the blocks which dominate all other blocks
+    /// in a loop.
+    loop_headers: BTreeSet<Label>,
+    /// A mapping from block label to the associated loop headers, if the block is part of a loop.
+    block_to_header: BTreeMap<Label, Label>,
+    /// All block labels belonging to a given loop, indexed by the loop header.
+    loop_labels: BTreeMap<Label, BTreeSet<Label>>,
+    /// All block labels for a given loop header which are _after_ any block in the loop.
+    after_loop_labels: BTreeMap<Label, BTreeSet<Label>>,
+    /// Back edges, defined by the code offset where the branch or jump is found, and the label
+    /// of the loop header.
+    back_edges: BTreeSet<(CodeOffset, Label)>,
+}
+
+/// Mutable state of the ast generator.
+struct Generator {
+    /// A stack of blocks which are currently open.
+    block_stack: Vec<BlockInfo>,
+    /// The labels for forward jumps which are not yet reached.
+    unreached_labels: BTreeSet<Label>,
+    /// The labels which have been used so far in jumps or branches.
+    used_labels: BTreeSet<Label>,
+    /// The attribute of the current bytecode instruction processed.
+    current_attr: Option<AttrId>,
+}
+
+/// Information about a block currently processed.
+#[derive(Clone)]
+struct BlockInfo {
+    /// Statements accumulated so far.
+    stms: Vec<Exp>,
+    /// A break label (forward jump) assigned to this block.
+    break_label: Option<Label>,
+    /// A continue label (backward jump) assigned to this block.
+    continue_label: Option<Label>,
+}
+
+// -------------------------------------------------------------------------------------------
+// Generator Context
+
+impl<'a> Context<'a> {
+    fn new(target: &'a FunctionTarget) -> Self {
+        let code = target.get_bytecode();
+        Self {
+            target,
+            forward_cfg: StacklessControlFlowGraph::new_forward(code),
+            builder: ExpBuilder::new(target.global_env()),
+            label_offsets: Bytecode::label_offsets(code),
+            loop_headers: Default::default(),
+            block_to_header: Default::default(),
+            loop_labels: Default::default(),
+            after_loop_labels: Default::default(),
+            back_edges: Default::default(),
+        }
+    }
+
+    /// Cleans up the bytecode. To make the algorithm work, the following requirements
+    /// have to be met:
+    /// 1. There must be no directly adjacent blocks B1 -> B2 such that B1 has no
+    ///    other outgoing edges, and B2 has no other incoming. Rather those blocks
+    ///    need to be merged into one. Otherwise, the algorithm runs into trouble with
+    ///    unwanted interleaving of such blocks if they are not produced adjacently in
+    ///    the topological order.
+    /// 2. There must be no fallthrough blocks. Rather each block must be terminated
+    ///    by one of branch, jump, return, or abort. This is more for help of the code
+    ///    here to simplify the viewpoint on the resulting CFG.
+    /// 3. There must not be stub blocks which just forward a jump, as in
+    ///    `label L1; goto L2`. In this case, we substitute `L1` by `L2`.
+    fn clean_bytecode(self) -> Vec<Bytecode> {
+        // Compute # of incoming edges for each block.
+        let mut incoming_count = BTreeMap::<BlockId, usize>::new();
+        for blk_id in self.forward_cfg.blocks() {
+            for succ in self.forward_cfg.successors(blk_id) {
+                *incoming_count.entry(*succ).or_default() += 1
+            }
+        }
+        // Build a label substitution for stubs.
+        let mut label_subst = BTreeMap::new();
+        for blk_id in self.forward_cfg.blocks() {
+            let block_code = self.code_for_block(blk_id);
+            if block_code.len() == 2 {
+                if let (Bytecode::Label(_, label1), Bytecode::Jump(_, label2)) =
+                    (&block_code[0], &block_code[1])
+                {
+                    label_subst.insert(*label1, *label2);
+                }
+            }
+        }
+        let substitute_label = |mut label: Label| {
+            let mut visited = BTreeSet::new();
+            while let Some(s) = label_subst.get(&label) {
+                assert!(
+                    visited.insert(label),
+                    "unexpected cyclic label substitution"
+                );
+                label = *s;
+            }
+            label
+        };
+        // Traverse all blocks and merge them as needed.
+        let mut todo = vec![self.forward_cfg.entry_block()];
+        let mut done = BTreeSet::new();
+        let mut result = vec![];
+        while let Some(mut blk_id) = todo.pop() {
+            if !done.insert(blk_id) {
+                continue;
+            }
+            let mut block_code = self.code_for_block(blk_id);
+            loop {
+                result.extend(block_code.iter().cloned());
+                let succs = self.forward_cfg.successors(blk_id);
+                if succs.len() == 1 {
+                    let succ = *succs.first().unwrap();
+                    if incoming_count[&succ] == 1 {
+                        // Fold this block into previous one
+                        if matches!(result.last(), Some(Bytecode::Jump(..))) {
+                            // Remove the now unnecessary Jump
+                            result.pop();
+                        }
+                        // Continue with this block.
+                        blk_id = succ;
+                        block_code = self.code_for_block(blk_id);
+                        if matches!(block_code.first(), Some(Bytecode::Label(..))) {
+                            // Skip label as it is not needed any more
+                            block_code = &block_code[1..];
+                        }
+                        continue;
+                    }
+
+                    // If the result doesn't terminate with a branch, add a Jump to make
+                    // the fallthrough explicit, but only if it is not an empty block
+                    if !block_code.is_empty() {
+                        let last = result.last().expect("expected non empty block");
+                        if !last.is_branching() {
+                            if let Some(label) = self.label_of_block(succ) {
+                                result.push(Bytecode::Jump(last.get_attr_id(), label))
+                            }
+                        }
+                    }
+                }
+                // Substitute any labels in the block terminator
+                match result.last_mut() {
+                    Some(Bytecode::Jump(_, label)) => *label = substitute_label(*label),
+                    Some(Bytecode::Branch(_, if_true, if_false, _)) => {
+                        *if_true = substitute_label(*if_true);
+                        *if_false = substitute_label(*if_false);
+                    },
+                    _ => {},
+                }
+                // Map the successors to those implied by label substitution, and add
+                // them to the top of the work stack.
+                todo.extend(
+                    succs
+                        .iter()
+                        .filter_map(|b| {
+                            self.label_of_block(*b)
+                                .map(|l| self.block_of_label(substitute_label(l)))
+                        })
+                        // revert so first in succs order processed first
+                        .rev(),
+                );
+                break;
+            }
+        }
+        result
+    }
+
+    /// Helper to compute information about loops.
+    fn compute_loop_info(&mut self, loop_info: &FatLoopFunctionInfo) {
+        let backward_cfg = StacklessControlFlowGraph::new_backward(self.code(), true);
+        for (header, fat_loop) in &loop_info.fat_loops {
+            self.loop_headers.insert(*header);
+            // Compute all blocks which are part of this loop. For this we exploit
+            // that the loop header dominates all blocks of the loop.
+            let mut todo = vec![];
+            for code_offset in &fat_loop.back_edges {
+                self.back_edges.insert((*code_offset, *header));
+                // Collect the block ids of the blocks which have back edges.
+                // This is from where traversal is started.
+                todo.push(backward_cfg.enclosing_block(*code_offset));
+            }
+            let mut loop_blocks = BTreeSet::<Label>::new();
+            // Include the header in the result/visited set. Since all paths are
+            // dominated by the header, the search is terminated via the
+            // header.
+            loop_blocks.insert(*header);
+            self.block_to_header.insert(*header, *header);
+            while let Some(blk_id) = todo.pop() {
+                let label = self
+                    .label_of_block(blk_id)
+                    .expect("expected block to have a label");
+                if loop_blocks.insert(label) {
+                    self.block_to_header.insert(label, *header);
+                    todo.extend(backward_cfg.successors(blk_id))
+                }
+            }
+            // Now compute all blocks after this loop
+            let mut after_loop_blocks = BTreeSet::new();
+            for blk_label in &loop_blocks {
+                let outside_succs = self
+                    .successor_labels(*blk_label)
+                    .filter(|l| !loop_blocks.contains(l));
+                after_loop_blocks.extend(outside_succs);
+            }
+            // Store result
+            self.loop_labels.insert(*header, loop_blocks);
+            self.after_loop_labels.insert(*header, after_loop_blocks);
+        }
+    }
+
+    /// Return global env.
+    fn env(&self) -> &GlobalEnv {
+        self.target.global_env()
+    }
+
+    /// Determine the reference kind of a temporary.
+    fn ref_kind(&self, temp: TempIndex) -> ReferenceKind {
+        self.target
+            .get_local_type(temp)
+            .ref_kind()
+            .unwrap_or(ReferenceKind::Immutable)
+    }
+
+    /// Return the code of the current function.
+    fn code(&self) -> &[Bytecode] {
+        self.target.get_bytecode()
+    }
+
+    /// Return the code for the block of the function.
+    fn code_for_block(&self, id: BlockId) -> &[Bytecode] {
+        &self.code()[self.forward_cfg.code_range(id)]
+    }
+
+    /// Returns the block in which the label is defined.
+    fn block_of_label(&self, label: Label) -> BlockId {
+        self.forward_cfg.enclosing_block(
+            *self
+                .label_offsets
+                .get(&label)
+                .expect("expected label has code offset"),
+        )
+    }
+
+    /// Returns the label of the block, if available.
+    fn label_of_block(&self, block_id: BlockId) -> Option<Label> {
+        Self::get_label_of_block_from_code(self.code_for_block(block_id))
+    }
+
+    fn get_label_of_block_from_code(code: &[Bytecode]) -> Option<Label> {
+        if let Some(Bytecode::Label(_, label)) = code.first() {
+            Some(*label)
+        } else {
+            None
+        }
+    }
+
+    /// Returns labels of successor blocks.
+    fn successor_labels(&self, label: Label) -> impl Iterator<Item = Label> + '_ {
+        self.forward_cfg
+            .successors(self.block_of_label(label))
+            .iter()
+            .filter_map(|b| self.label_of_block(*b))
+    }
+}
+
+// -------------------------------------------------------------------------------------------
+// Generator Core Logic
+
+impl Generator {
+    /// Run the generator.
+    fn gen(&mut self, ctx: &Context) -> Exp {
+        let mut blocks = ctx.forward_cfg.blocks();
+        // Sort blocks topologically.
+        self.sort_blocks(ctx, &mut blocks);
+        // Push a virtual block onto the stack to collect outer statements.
+        self.block_stack.push(BlockInfo {
+            stms: vec![],
+            break_label: None,
+            continue_label: None,
+        });
+        // Process blocks in the determined order.
+        for i in 0..blocks.len() {
+            let blk_id = blocks[i];
+            if ctx.code_for_block(blk_id).is_empty() {
+                // Dummy block, just continue.
+                continue;
+            }
+            self.gen_block(ctx, blk_id, &blocks[i + 1..])
+        }
+        /*
+        while self.block_stack.len() > 1 {
+            self.close_block(ctx)
+        }
+         */
+        let BlockInfo { stms, .. } = self.block_stack.pop().unwrap();
+        ctx.builder.seq(&self.current_loc(ctx), stms)
+    }
+
+    /// Topological sort blocks using forward dependencies only, and
+    /// ignoring any back jumps. We need to use a sort algorithm here which
+    /// produces the sets of independent blocks as we still need to
+    /// make a good choice within those blocks. Apparently, `petgraph` does not
+    /// give this functionality, so we use crate `topological_sort`.
+    fn sort_blocks(&self, ctx: &Context, blocks: &mut Vec<BlockId>) {
+        // Construct the partial order derived from the control flow graph.
+        let mut top_sort = TopologicalSort::<BlockId>::new();
+        let original_blocks = std::mem::take(blocks);
+        for blk_id in original_blocks {
+            for succ in ctx.forward_cfg.successors(blk_id) {
+                let range = ctx.forward_cfg.code_range(blk_id);
+                if !range.is_empty() {
+                    let code_offset = (range.end - 1) as CodeOffset;
+                    if let Some(label) = ctx.label_of_block(*succ) {
+                        if ctx.back_edges.contains(&(code_offset, label)) {
+                            // This is a back edge, ignore for ordering
+                            continue;
+                        }
+                    }
+                }
+                top_sort.add_dependency(blk_id, *succ)
+            }
+        }
+        // Add virtual edges to ensure that all blocks of a given loop are before
+        // any blocks after that loop. This is a requirement for the algorithm to work.
+        for header in &ctx.loop_headers {
+            for after_loop_label in &ctx.after_loop_labels[header] {
+                for loop_block_label in &ctx.loop_labels[header] {
+                    top_sort.add_dependency(
+                        ctx.block_of_label(*loop_block_label),
+                        ctx.block_of_label(*after_loop_label),
+                    )
+                }
+            }
+        }
+        // Repeatedly pull blocks which do not have any successors left.
+        loop {
+            let mut group = top_sort.pop_all();
+            if group.is_empty() {
+                break;
+            }
+            // Sort the members of the group (1) by priority of the block terminator. We want
+            // to have jumps and other exits first (2) by code offset as it was determined
+            // by the DFS ordering of blocks in cleanup.
+            let terminator_priority = |blk: BlockId| -> isize {
+                use Bytecode::*;
+                match ctx.code_for_block(blk).last() {
+                    None => 0,
+                    Some(Jump(..)) => 1,
+                    Some(Abort(..)) => 2,
+                    Some(Ret(..)) => 3,
+                    Some(Branch(..)) => 4,
+                    _ => panic!("unexpected block terminator"),
+                }
+            };
+            group.sort_by(|b1, b2| {
+                let c = terminator_priority(*b1).cmp(&terminator_priority(*b2));
+                if c.is_eq() {
+                    // Use code offset
+                    ctx.forward_cfg
+                        .code_range(*b1)
+                        .start
+                        .cmp(&ctx.forward_cfg.code_range(*b2).start)
+                } else {
+                    c
+                }
+            });
+            blocks.append(&mut group)
+        }
+        assert!(top_sort.is_empty(), "unexpected cycle in forward jumps");
+        if DEBUG {
+            self.dprint_blocks(ctx, "sorted", blocks.iter().copied())
+        }
+    }
+
+    /// Process the given block, with subsequent blocks in the topological order in
+    /// the `rest` parameter.
+    fn gen_block(&mut self, ctx: &Context, block_id: BlockId, rest: &[BlockId]) {
+        use Bytecode::*;
+
+        let block_code = ctx.code_for_block(block_id);
+        let next_block_label = rest.first().and_then(|id| ctx.label_of_block(*id));
+        if let Some(loop_label) = ctx
+            .label_of_block(block_id)
+            .filter(|label| ctx.loop_headers.contains(label))
+        {
+            // This is the header of a loop, open a loop block
+            self.block_stack.push(BlockInfo {
+                stms: vec![],
+                break_label: None,
+                continue_label: Some(loop_label),
+            });
+        }
+
+        for bc in block_code.iter() {
+            self.set_current_attr(ctx, bc.get_attr_id());
+            match bc {
+                // Instructions dealing with control flow
+                Label(_, label) => {
+                    // Mark the label as reached.
+                    self.label_reached(ctx, *label)
+                },
+                Ret(_, temps) => {
+                    let stm = ExpData::Return(
+                        self.new_stm_node_id(ctx),
+                        self.make_temp_tuple(ctx, temps),
+                    );
+                    self.add_stm(stm);
+                },
+                Abort(_, temp) => {
+                    let temp = self.make_temp(ctx, *temp);
+                    let stm =
+                        ExpData::Call(self.new_stm_node_id(ctx), Operation::Abort, vec![temp]);
+                    self.add_stm(stm);
+                },
+                Branch(_, if_true, if_false, cond) => {
+                    self.gen_branch(ctx, next_block_label, *cond, *if_true, *if_false);
+                },
+                Jump(_, target) => {
+                    self.gen_jump(ctx, next_block_label, *target);
+                },
+                // Other instructions
+                Nop(_) => {},
+                Assign(_, lhs, rhs, _) => {
+                    let stm = ExpData::Assign(
+                        self.new_stm_node_id(ctx),
+                        self.make_temp_pat(ctx, *lhs),
+                        self.make_temp(ctx, *rhs),
+                    );
+                    self.add_stm(stm)
+                },
+                Call(_, dests, oper, srcs, _) => self.gen_call(ctx, dests, oper, srcs),
+                Load(_, temp, value) => {
+                    let value_id = self.new_node_id(ctx, ctx.target.get_local_type(*temp).clone());
+                    let stm = ExpData::Assign(
+                        self.new_stm_node_id(ctx),
+                        self.make_temp_pat(ctx, *temp),
+                        ExpData::Value(value_id, value.to_model_value()).into_exp(),
+                    )
+                    .into_exp();
+                    self.add_stm(stm)
+                },
+                SpecBlock(_, _) | SaveMem(_, _, _) | SaveSpecVar(_, _, _) | Prop(_, _, _) => {
+                    unimplemented!("ast generation of specs")
+                },
+            }
+        }
+    }
+
+    /// Process a branch instruction.
+    fn gen_branch(
+        &mut self,
+        ctx: &Context,
+        next_block_label: Option<Label>,
+        cond: TempIndex,
+        if_true: Label,
+        if_false: Label,
+    ) {
+        let cond = self.make_temp(ctx, cond);
+        if let Some(nest) = self.find_continue_nest(ctx, if_true) {
+            // This a `continue` of an outer loop
+            self.used_labels.insert(if_true);
+            self.add_stm(
+                ctx.builder
+                    .if_(cond, ctx.builder.continue_(&self.current_loc(ctx), nest)),
+            );
+            // Do the `else` as jump
+            self.gen_jump(ctx, next_block_label, if_false)
+        } else if let Some(nest) = self.find_continue_nest(ctx, if_false) {
+            // Continue with negated condition
+            self.used_labels.insert(if_false);
+            self.add_stm(ctx.builder.if_(
+                ctx.builder.not(cond),
+                ctx.builder.continue_(&self.current_loc(ctx), nest),
+            ));
+            // Do the `if` as jump
+            self.gen_jump(ctx, next_block_label, if_true)
+        } else if let Some(nest) = self.find_break_nest(ctx, if_true) {
+            self.used_labels.insert(if_true);
+            self.add_stm(
+                ctx.builder
+                    .if_(cond, ctx.builder.break_(&self.current_loc(ctx), nest)),
+            );
+            // Do the `else` as jump
+            self.gen_jump(ctx, next_block_label, if_false)
+        } else if let Some(nest) = self.find_break_nest(ctx, if_false) {
+            self.used_labels.insert(if_false);
+            self.add_stm(ctx.builder.if_(
+                ctx.builder.not(cond),
+                ctx.builder.break_(&self.current_loc(ctx), nest),
+            ));
+            // Do the `if` as jump
+            self.gen_jump(ctx, next_block_label, if_true)
+        } else {
+            // Both are forward jumps. Determine which is fall through and swap
+            // branches if needed.
+            let (negated_cond, if_true, if_false) = if Some(if_false) == next_block_label {
+                (cond, if_false, if_true)
+            } else {
+                assert_eq!(
+                    Some(if_true),
+                    next_block_label,
+                    "at least one target must fall-through \
+                    (unexpected divergence of control flow)"
+                );
+                (self.make_not(ctx, cond), if_true, if_false)
+            };
+            // Push two blocks such we generate code as follows:
+            // ```
+            //    cond = ...
+            //    block {
+            //      block {
+            //        if !cond break;
+            //        ..
+            //        break[2]
+            //      } // if_false target
+            //      ..
+            //      break
+            //    } // exit from inner computation
+            //
+            // The outer block serves as a target for any jumps exiting these blocks. At
+            // the point the block is pushed, the target is unbound, and will bound later
+            // during processing of blocks in topological order.
+            self.block_stack.push(BlockInfo {
+                stms: vec![],
+                break_label: None,
+                continue_label: None,
+            });
+            self.block_stack.push(BlockInfo {
+                stms: vec![],
+                break_label: Some(if_false),
+                continue_label: None,
+            });
+            self.used_labels.insert(if_false);
+            self.add_stm(
+                ctx.builder
+                    .if_(negated_cond, ctx.builder.break_(&self.current_loc(ctx), 0)),
+            );
+            self.gen_jump(ctx, next_block_label, if_true)
+        }
+    }
+
+    fn gen_jump(&mut self, ctx: &Context, next_block_label: Option<Label>, target: Label) {
+        self.used_labels.insert(target);
+        if next_block_label != Some(target) {
+            if let Some(nest) = self.find_continue_nest(ctx, target) {
+                // continue loop
+                self.add_stm(ctx.builder.continue_(&self.current_loc(ctx), nest))
+            } else {
+                // must bind to an outer block for forward jump
+                let nest = self.find_or_bind_break_nest(ctx, target);
+                self.add_stm(ctx.builder.break_(&self.current_loc(ctx), nest));
+            }
+        }
+    }
+
+    fn find_or_bind_break_nest(&mut self, _ctx: &Context, label: Label) -> usize {
+        let len = self.block_stack.len();
+        for (nest, info) in self.block_stack.iter_mut().rev().enumerate() {
+            if nest >= len - 1 {
+                // Can't bind to outer virtual block
+                break;
+            }
+            match &info.break_label {
+                Some(l) if &label == l => return nest,
+                Some(_) => continue,
+                None => {
+                    // Label for this block not assigned, assign it now.
+                    info.break_label = Some(label);
+                    return nest;
+                },
+            }
+        }
+        panic!("label not found and all blocks are bound: {}", label);
+    }
+
+    fn find_continue_nest(&self, _ctx: &Context, label: Label) -> Option<usize> {
+        for (nest, info) in self.block_stack.iter().rev().enumerate() {
+            if info.continue_label.map(|l| l == label).unwrap_or(false) {
+                return Some(nest);
+            }
+        }
+        None
+    }
+
+    fn find_break_nest(&self, _ctx: &Context, label: Label) -> Option<usize> {
+        for (nest, info) in self.block_stack.iter().rev().enumerate() {
+            if info.break_label.map(|l| l == label).unwrap_or(false) {
+                return Some(nest);
+            }
+        }
+        None
+    }
+
+    fn close_block(&mut self, ctx: &Context) {
+        if DEBUG {
+            self.dprint_stack(ctx, "closing", self.block_stack.iter().rev().take(1));
+        }
+        let info = self.top_block();
+        // Check whether this is an obsolete block. Such a block has not been
+        // referenced via break or continue and can be eliminated.
+        if (info.break_label.is_none() || !self.used_labels.contains(&info.break_label.unwrap()))
+            && (info.continue_label.is_none()
+                || !self.used_labels.contains(&info.continue_label.unwrap()))
+        {
+            let stms = self.block_stack.pop().unwrap().stms;
+            for stm in stms {
+                // Need to adjust the nest of break/continue statements by -1, as we are not
+                // actually creating a loop block.
+                self.add_stm(rewrite_loop_nest(ctx.env(), stm, -1))
+            }
+            return;
+        }
+
+        // The last statement of a block which is not already terminated must have a break
+        let needs_break = info.stms.is_empty()
+            || !matches!(
+                info.stms.last().unwrap().as_ref(),
+                ExpData::LoopCont(..)
+                    | ExpData::Return(..)
+                    | ExpData::Call(_, Operation::Abort, ..)
+            );
+        if needs_break {
+            self.add_stm(ctx.builder.break_(&self.current_loc(ctx), 0))
+        }
+        // Create a loop and add to parent
+        let stms = self.block_stack.pop().unwrap().stms;
+        let body = ctx.builder.seq(&self.current_loc(ctx), stms);
+        let stm = ExpData::Loop(self.new_stm_node_id(ctx), body).into_exp();
+        self.add_stm(stm)
+    }
+
+    /// Mark the given label as reached and close all blocks effected by this.
+    /// Once a label is reached, it cannot be referenced after this point
+    /// with a forward jump.
+    ///
+    /// A block is closed under the following conditions:
+    /// 1. It's a loop header and the reached label is not part of the loop blocks
+    /// 2. Its break label is set to one of the reached labels.
+    /// 2. It has an unbound break label and is enclosed by a block as in (1)
+    fn label_reached(&mut self, ctx: &Context, label: Label) {
+        self.unreached_labels.remove(&label);
+        if DEBUG {
+            self.dprint_stack(
+                ctx,
+                &format!("reaching {}", label),
+                self.block_stack.iter().rev(),
+            );
+        }
+        if ctx.loop_headers.contains(&label) {
+            return;
+        }
+        // Compute the blocks to close as a result of this label being reached.
+        let mut new_stack_level = self.block_stack.len() - 1;
+        let mut skipping_unbound = true;
+        while new_stack_level > 0 {
+            match &self.block_stack[new_stack_level] {
+                BlockInfo {
+                    continue_label: Some(header),
+                    ..
+                } if !ctx.loop_labels[header].contains(&label) => {
+                    // The block is close because the reached label is not part of it
+                    new_stack_level -= 1;
+                    skipping_unbound = false;
+                },
+                BlockInfo {
+                    break_label: None,
+                    continue_label: None,
+                    ..
+                } => {
+                    // The block has no binding yet, if an outer block is closed, we can
+                    // close it.
+                    new_stack_level -= 1;
+                    if self.unreached_labels.is_empty() {
+                        // The break label is not bound, but there is no more label to reach,
+                        // so we can close this block
+                        skipping_unbound = false;
+                    }
+                },
+                BlockInfo {
+                    break_label: Some(label),
+                    ..
+                } if !self.unreached_labels.contains(label) => {
+                    // The block is actually reached
+                    new_stack_level -= 1;
+                    skipping_unbound = false;
+                },
+                _ => break,
+            }
+        }
+        if !skipping_unbound {
+            while new_stack_level < self.block_stack.len() - 1 {
+                self.close_block(ctx)
+            }
+        }
+        if DEBUG {
+            self.dprint_stack(
+                ctx,
+                &format!("after reaching {}", label),
+                self.block_stack.iter().rev(),
+            );
+        }
+    }
+
+    fn gen_call(
+        &mut self,
+        ctx: &Context,
+        dests: &[TempIndex],
+        oper: &BytecodeOperation,
+        srcs: &[TempIndex],
+    ) {
+        use BytecodeOperation::*;
+        match oper {
+            Function(mid, fid, inst) => self.gen_call_stm(
+                ctx,
+                Some(inst),
+                dests,
+                Operation::MoveFunction(*mid, *fid),
+                srcs,
+            ),
+            Pack(mid, sid, inst) => {
+                self.gen_call_stm(
+                    ctx,
+                    Some(inst),
+                    dests,
+                    Operation::Pack(*mid, *sid, None),
+                    srcs,
+                );
+            },
+            Unpack(mid, sid, inst) => {
+                let qsid = mid.qualified_inst(*sid, inst.clone());
+                let rhs = self.make_temp(ctx, srcs[0]);
+                self.gen_match(ctx, dests, qsid, None, rhs);
+            },
+            MoveTo(_, _, inst) => {
+                self.gen_call_stm(ctx, Some(inst), dests, Operation::MoveTo, srcs);
+            },
+            MoveFrom(_, _, inst) => {
+                self.gen_call_stm(ctx, Some(inst), dests, Operation::MoveFrom, srcs);
+            },
+            Exists(_, _, inst) => {
+                self.gen_call_stm(ctx, Some(inst), dests, Operation::Exists(None), srcs);
+            },
+            TestVariant(mid, sid, variant, inst) => {
+                self.gen_call_stm(
+                    ctx,
+                    Some(inst),
+                    dests,
+                    Operation::TestVariants(*mid, *sid, vec![*variant]),
+                    srcs,
+                );
+            },
+            PackVariant(mid, sid, variant, inst) => {
+                self.gen_call_stm(
+                    ctx,
+                    Some(inst),
+                    dests,
+                    Operation::Pack(*mid, *sid, Some(*variant)),
+                    srcs,
+                );
+            },
+            UnpackVariant(mid, sid, variant, inst) => {
+                let qsid = mid.qualified_inst(*sid, inst.clone());
+                let rhs = self.make_temp(ctx, srcs[0]);
+                self.gen_match(ctx, dests, qsid, Some(*variant), rhs);
+            },
+            BorrowGlobal(_, _, inst) => self.gen_call_stm(
+                ctx,
+                Some(inst),
+                dests,
+                Operation::BorrowGlobal(ctx.ref_kind(dests[0])),
+                srcs,
+            ),
+            BorrowLoc => self.gen_call_stm(
+                ctx,
+                None,
+                dests,
+                Operation::Borrow(ctx.ref_kind(dests[0])),
+                srcs,
+            ),
+            BorrowField(mid, sid, _, field_offset) => {
+                let struct_env = ctx.env().get_struct(mid.qualified(*sid));
+                let field_id = struct_env.get_field_by_offset(*field_offset).get_id();
+                self.gen_call_stm(
+                    ctx,
+                    None,
+                    dests,
+                    Operation::Select(*mid, *sid, field_id),
+                    dests,
+                )
+            },
+            BorrowVariantField(mid, sid, variants, _inst, field_offset) => {
+                let struct_env = ctx.env().get_struct(mid.qualified(*sid));
+                let field_ids = variants
+                    .iter()
+                    .map(|v| {
+                        struct_env
+                            .get_field_by_offset_optional_variant(Some(*v), *field_offset)
+                            .get_id()
+                    })
+                    .collect();
+                self.gen_call_stm(
+                    ctx,
+                    None,
+                    dests,
+                    Operation::SelectVariants(*mid, *sid, field_ids),
+                    srcs,
+                )
+            },
+            Drop | Release => {
+                // Do nothing
+            },
+            ReadRef => self.gen_call_stm(ctx, None, dests, Operation::Deref, srcs),
+            WriteRef => {
+                let stm = ExpData::Mutate(
+                    self.new_stm_node_id(ctx),
+                    self.make_temp(ctx, dests[0]),
+                    self.make_temp(ctx, srcs[0]),
+                );
+                self.add_stm(stm)
+            },
+            FreezeRef(explicit) => {
+                self.gen_call_stm(ctx, None, dests, Operation::Freeze(*explicit), srcs)
+            },
+            Vector => self.gen_call_stm(ctx, None, dests, Operation::Vector, srcs),
+            CastU8 | CastU16 | CastU32 | CastU64 | CastU128 | CastU256 => {
+                self.gen_call_stm(ctx, None, dests, Operation::Cast, srcs)
+            },
+            Not => self.gen_call_stm(ctx, None, dests, Operation::Not, srcs),
+            Add => self.gen_call_stm(ctx, None, dests, Operation::Add, srcs),
+            Sub => self.gen_call_stm(ctx, None, dests, Operation::Sub, srcs),
+            Mul => self.gen_call_stm(ctx, None, dests, Operation::Mul, srcs),
+            Div => self.gen_call_stm(ctx, None, dests, Operation::Div, srcs),
+            Mod => self.gen_call_stm(ctx, None, dests, Operation::Mod, srcs),
+            BitAnd => self.gen_call_stm(ctx, None, dests, Operation::BitAnd, srcs),
+            BitOr => self.gen_call_stm(ctx, None, dests, Operation::BitOr, srcs),
+            Xor => self.gen_call_stm(ctx, None, dests, Operation::Xor, srcs),
+            Shl => self.gen_call_stm(ctx, None, dests, Operation::Shl, srcs),
+            Shr => self.gen_call_stm(ctx, None, dests, Operation::Shr, srcs),
+            Lt => self.gen_call_stm(ctx, None, dests, Operation::Lt, srcs),
+            Gt => self.gen_call_stm(ctx, None, dests, Operation::Gt, srcs),
+            Le => self.gen_call_stm(ctx, None, dests, Operation::Le, srcs),
+            Ge => self.gen_call_stm(ctx, None, dests, Operation::Ge, srcs),
+            Or => self.gen_call_stm(ctx, None, dests, Operation::Or, srcs),
+            And => self.gen_call_stm(ctx, None, dests, Operation::And, srcs),
+            Eq => self.gen_call_stm(ctx, None, dests, Operation::Eq, srcs),
+            Neq => self.gen_call_stm(ctx, None, dests, Operation::Neq, srcs),
+
+            OpaqueCallBegin(_, _, _)
+            | OpaqueCallEnd(_, _, _)
+            | IsParent(_, _)
+            | WriteBack(_, _)
+            | UnpackRef
+            | PackRef
+            | UnpackRefDeep
+            | PackRefDeep
+            | GetField(_, _, _, _)
+            | GetVariantField(_, _, _, _, _)
+            | GetGlobal(_, _, _)
+            | Uninit
+            | Havoc(_)
+            | Stop
+            | TraceLocal(_)
+            | TraceReturn(_)
+            | TraceAbort
+            | TraceExp(_, _)
+            | TraceGlobalMem(_)
+            | EmitEvent
+            | EventStoreDiverge => {
+                panic!("specification operation not supported: {:?}", oper)
+            },
+        }
+    }
+
+    fn gen_call_stm(
+        &mut self,
+        ctx: &Context,
+        inst: Option<&Vec<Type>>,
+        dests: &[TempIndex],
+        oper: Operation,
+        srcs: &[TempIndex],
+    ) {
+        let ty = Type::tuple(
+            dests
+                .iter()
+                .map(|d| ctx.target.get_local_type(*d).clone())
+                .collect(),
+        );
+        let call_id = self.new_node_id(ctx, ty);
+        if let Some(inst) = inst {
+            ctx.env().set_node_instantiation(call_id, inst.to_vec())
+        }
+        let call = ExpData::Call(call_id, oper, self.make_temps(ctx, srcs.iter().copied()));
+        self.gen_assign(ctx, dests, call)
+    }
+
+    fn gen_match(
+        &mut self,
+        ctx: &Context,
+        dests: &[TempIndex],
+        qsid: QualifiedInstId<StructId>,
+        variant: Option<Symbol>,
+        rhs: Exp,
+    ) {
+        let pat_id = self.new_node_id(ctx, qsid.to_type());
+        let pat = Pattern::Struct(
+            pat_id,
+            qsid,
+            variant,
+            dests.iter().map(|d| self.make_temp_pat(ctx, *d)).collect(),
+        );
+        let stm = ExpData::Assign(self.new_stm_node_id(ctx), pat, rhs);
+        self.add_stm(stm)
+    }
+
+    fn gen_assign(&mut self, ctx: &Context, dests: &[TempIndex], exp: impl Into<Exp>) {
+        let stm = ExpData::Assign(
+            self.new_stm_node_id(ctx),
+            self.make_temp_pat_tuple(ctx, dests),
+            exp.into(),
+        );
+        self.add_stm(stm)
+    }
+
+    fn top_block_mut(&mut self) -> &mut BlockInfo {
+        self.block_stack
+            .last_mut()
+            .expect("expected block stack not be empty")
+    }
+
+    fn top_block(&self) -> &BlockInfo {
+        self.block_stack
+            .last()
+            .expect("expected block stack not be empty")
+    }
+
+    fn add_stm(&mut self, exp: impl Into<Exp>) {
+        self.top_block_mut().stms.push(exp.into())
+    }
+
+    fn make_var_decl(&mut self, ctx: &Context, temp: TempIndex) -> (NodeId, Symbol) {
+        let name = if temp < ctx.target.get_parameter_count() {
+            ctx.target.get_local_name(temp)
+        } else {
+            ctx.env().symbol_pool().make(&format!("_t{}", temp))
+        };
+        let ty = ctx.target.get_local_type(temp);
+        let id = self.new_node_id(ctx, ty.clone());
+        (id, name)
+    }
+
+    fn make_temp(&mut self, ctx: &Context, temp: TempIndex) -> Exp {
+        let (id, name) = self.make_var_decl(ctx, temp);
+        ExpData::LocalVar(id, name).into_exp()
+    }
+
+    fn make_temps(&mut self, ctx: &Context, temps: impl Iterator<Item = TempIndex>) -> Vec<Exp> {
+        temps.map(|temp| self.make_temp(ctx, temp)).collect()
+    }
+
+    fn make_temp_pat(&mut self, ctx: &Context, temp: TempIndex) -> Pattern {
+        let (id, name) = self.make_var_decl(ctx, temp);
+        Pattern::Var(id, name)
+    }
+
+    fn make_temp_tuple(&mut self, ctx: &Context, temps: &[TempIndex]) -> Exp {
+        let mut exps = temps
+            .iter()
+            .map(|temp| self.make_temp(ctx, *temp))
+            .collect_vec();
+        if exps.len() == 1 {
+            exps.pop().unwrap()
+        } else {
+            let ty = Type::Tuple(
+                exps.iter()
+                    .map(|e| ctx.env().get_node_type(e.node_id()))
+                    .collect(),
+            );
+            let node_id = self.new_node_id(ctx, ty);
+            ExpData::Call(node_id, Operation::Tuple, exps).into_exp()
+        }
+    }
+
+    fn make_temp_pat_tuple(&mut self, ctx: &Context, temps: &[TempIndex]) -> Pattern {
+        let mut pats = temps
+            .iter()
+            .map(|temp| self.make_temp_pat(ctx, *temp))
+            .collect_vec();
+        if pats.len() == 1 {
+            pats.pop().unwrap()
+        } else {
+            let ty = Type::Tuple(
+                pats.iter()
+                    .map(|p| ctx.env().get_node_type(p.node_id()))
+                    .collect(),
+            );
+            let node_id = self.new_node_id(ctx, ty);
+            Pattern::Tuple(node_id, pats)
+        }
+    }
+
+    fn make_not(&self, ctx: &Context, exp: Exp) -> Exp {
+        let node_id = self.clone_node_id(ctx, exp.node_id());
+        ExpData::Call(node_id, Operation::Not, vec![exp]).into_exp()
+    }
+
+    fn new_node_id(&self, ctx: &Context, ty: Type) -> NodeId {
+        ctx.builder.new_node_id(self.current_loc(ctx), ty)
+    }
+
+    fn new_stm_node_id(&self, ctx: &Context) -> NodeId {
+        self.new_node_id(ctx, Type::unit())
+    }
+
+    fn clone_node_id(&self, ctx: &Context, id: NodeId) -> NodeId {
+        ctx.builder.clone_node_id(id)
+    }
+
+    fn set_current_attr(&mut self, _ctx: &Context, attr_id: AttrId) {
+        self.current_attr = Some(attr_id)
+    }
+
+    fn current_loc(&self, ctx: &Context) -> Loc {
+        self.current_attr
+            .map(|attr| ctx.target.get_bytecode_loc(attr))
+            .unwrap_or_else(|| ctx.target.get_loc())
+    }
+
+    // ----------------------------------------------------------------------------------------
+    // Debugging
+
+    fn dprint_blocks(&self, ctx: &Context, note: &str, blocks: impl Iterator<Item = BlockId>) {
+        if log_enabled!(Level::Debug) {
+            debug!(">> {}", note);
+            for blk_id in blocks {
+                debug!(
+                    "Block #{}{} successors {}",
+                    blk_id,
+                    if blk_id == ctx.forward_cfg.entry_block() {
+                        " entry "
+                    } else {
+                        ""
+                    },
+                    ctx.forward_cfg
+                        .successors(blk_id)
+                        .iter()
+                        .map(|s| format!("Block #{}", s))
+                        .join(",")
+                );
+                if ctx.code_for_block(blk_id).is_empty() {
+                    debug!("no code")
+                } else {
+                    debug!(
+                        "code range {}..{}",
+                        ctx.forward_cfg.code_range(blk_id).start,
+                        ctx.forward_cfg.code_range(blk_id).end
+                    );
+                }
+
+                for bc in ctx.code_for_block(blk_id) {
+                    debug!("  {}", bc.display(ctx.target, &BTreeMap::new()))
+                }
+            }
+        }
+    }
+
+    fn dprint_stack<'a>(
+        &self,
+        _ctx: &Context,
+        note: &str,
+        stack: impl Iterator<Item = &'a BlockInfo>,
+    ) {
+        if log_enabled!(Level::Debug) {
+            debug!(">> {}", note);
+            for BlockInfo {
+                break_label,
+                continue_label,
+                ..
+            } in stack
+            {
+                debug!(
+                    "  break = {}, continue = {} {{ .. }}",
+                    break_label
+                        .map(|l| l.to_string())
+                        .unwrap_or_else(|| "?".to_string()),
+                    continue_label
+                        .map(|l| l.to_string())
+                        .unwrap_or_else(|| "?".to_string()),
+                );
+            }
+            debug!(
+                "  used labels {}, unreached labels {}",
+                self.used_labels.iter().map(|l| l.to_string()).join(","),
+                self.unreached_labels
+                    .iter()
+                    .map(|l| l.to_string())
+                    .join(",")
+            )
+        }
+    }
+}
+
+// =====================================================================================
+
+/// A rewriter which detects if-then and if-then-else patterns in generated
+/// loops.
+pub fn transform_conditionals(target: &FunctionTarget, exp: Exp) -> Exp {
+    let loop_to_cont = exp.compute_loop_bindings().0;
+    let builder = ExpBuilder::new(target.global_env());
+    IfElseTransformer {
+        loop_to_cont,
+        builder,
+    }
+    .rewrite_exp(exp)
+}
+
+struct IfElseTransformer<'a> {
+    /// Contains bindings of break/continue statements to `loop` expressions in the code.
+    /// This maps from the node id to a map of the node ids of such statements, the boolean
+    /// indicating whether it is a `continue` (true) or `break`.
+    loop_to_cont: BTreeMap<NodeId, BTreeMap<NodeId, bool>>,
+    /// The expression builder.
+    builder: ExpBuilder<'a>,
+}
+
+impl<'a> ExpRewriterFunctions for IfElseTransformer<'a> {
+    fn rewrite_exp(&mut self, exp: Exp) -> Exp {
+        if let Some(result) = self.try_make_if_else(exp.clone()) {
+            self.rewrite_exp_descent(result)
+        } else if let Some(result) = self.try_make_if(exp.clone()) {
+            self.rewrite_exp_descent(result)
+        } else if let Some(result) = self.try_make_if_continue(exp.clone()) {
+            self.rewrite_exp_descent(result)
+        } else {
+            self.rewrite_exp_descent(exp)
+        }
+    }
+}
+
+impl<'a> IfElseTransformer<'a> {
+    /// Attempts to create an if-then-else from the given expression.
+    /// This recognizes the pattern below, as produced by the AST
+    /// generator:
+    ///
+    /// ```move
+    /// loop {
+    ///   loop {
+    ///     if (c) break; // exclusive binding to inner loop
+    ///     <else-branch>
+    ///     break[1]; // 1st binding to outer loop
+    ///   }
+    ///   <then-branch> // must not reference outer loop
+    ///   break | abort | return; // 2nd binding to outer loop or exit
+    /// }
+    /// ```
+    ///
+    /// The comment at the break indicates that both loops
+    /// must have exactly one associated break statement.
+    fn try_make_if_else(&self, exp: Exp) -> Option<Exp> {
+        let node_id = exp.node_id();
+        let default_loc = self.builder.env().get_node_loc(node_id);
+        let (outer_id, outer_body) = self.builder.match_loop(exp)?;
+        /*
+        if self.loop_to_cont[&outer_id].len() != 2 {
+            // not exactly two bindings to outer loop
+            return None;
+        }
+         */
+        let (outer_first, outer_rest) = self.builder.extract_first(outer_body);
+        let (mut outer_rest, outer_break) = self
+            .builder
+            .extract_last(self.builder.seq(&default_loc, outer_rest));
+
+        let mut loop_binding_count = self.loop_to_cont[&outer_id].len();
+        if self.builder.is_loop_cont(&outer_break, 0, false) {
+            // This is a break against the outer loop, count
+            loop_binding_count -= 1
+        } else if matches!(
+            outer_break.as_ref(),
+            ExpData::Call(_, Operation::Abort, ..) | ExpData::Return(..)
+        ) {
+            // Not counting for loop bindings, and put expression
+            // back
+            outer_rest.push(outer_break)
+        } else {
+            return None;
+        }
+
+        let (inner_id, inner_body) = self.builder.match_loop(outer_first)?;
+        if self.loop_to_cont[&inner_id].len() != 1 {
+            return None;
+        }
+        let (inner_first, mut inner_rest) = self.builder.extract_first(inner_body);
+        let inner_last = inner_rest.pop()?;
+        let cond = self.builder.match_if_loop_cont(inner_first, 0, false)?;
+        // If this break addresses the outer loop, and this one and the
+        // exit `outer_break` are all existing loop bindings, we found if-then-else.
+        if self.builder.is_loop_cont(&inner_last, 1, false) && loop_binding_count == 1 {
+            // found if-then-else
+            let if_true = rewrite_loop_nest(
+                self.builder.env(),
+                self.builder.seq(&default_loc, outer_rest),
+                -1,
+            );
+            let if_false = rewrite_loop_nest(
+                self.builder.env(),
+                self.builder.seq(&default_loc, inner_rest),
+                -2,
+            );
+            let (cond, if_true, if_false) =
+                if let ExpData::Call(_, Operation::Not, args) = cond.as_ref() {
+                    (args[0].clone(), if_false, if_true)
+                } else {
+                    (cond, if_true, if_false)
+                };
+            Some(self.builder.if_else(cond, if_true, if_false))
+        } else {
+            None
+        }
+    }
+
+    /// Attempts to create an if-then (without else) from the given expression.
+    /// This recognizes the pattern below, as produced by the AST
+    /// generator:
+    ///
+    /// ```move
+    ///   loop {
+    ///     if (c) break; // 1st binding to loop
+    ///     <then-branch>
+    ///     break         // 2nd binding to loop
+    ///   }
+    /// ```
+    fn try_make_if(&self, exp: Exp) -> Option<Exp> {
+        let node_id = exp.node_id();
+        let default_loc = self.builder.env().get_node_loc(node_id);
+        let (loop_id, body) = self.builder.match_loop(exp)?;
+        if self.loop_to_cont[&loop_id].len() != 2 {
+            return None;
+        }
+        let (first, rest) = self.builder.extract_first(body);
+        let cond = self.builder.match_if_loop_cont(first, 0, false)?;
+        let (rest, last) = self
+            .builder
+            .extract_last(self.builder.seq(&default_loc, rest));
+        if !self.builder.is_loop_cont(&last, 0, false) {
+            return None;
+        }
+        Some(self.builder.if_else(
+            self.builder.not(cond),
+            rewrite_loop_nest(self.builder.env(), self.builder.seq(&default_loc, rest), -1),
+            self.builder.nop(&default_loc),
+        ))
+    }
+
+    /// Attempts to create an if-then-continue from the given expression.
+    /// This recognizes the pattern below, as produced by the AST
+    /// generator for while loop style code:
+    ///
+    /// ```move
+    ///   loop {
+    ///     if (c) break; // exclusive binding to loop
+    ///     <then-branch>
+    ///     continue[n]   // continue in outer loop with n > 0
+    ///   }
+    /// ```
+    fn try_make_if_continue(&self, exp: Exp) -> Option<Exp> {
+        let node_id = exp.node_id();
+        let default_loc = self.builder.env().get_node_loc(node_id);
+        let (loop_id, body) = self.builder.match_loop(exp)?;
+        if self.loop_to_cont[&loop_id].len() != 1 {
+            return None;
+        }
+        let (first, rest) = self.builder.extract_first(body);
+        let cond = self.builder.match_if_loop_cont(first, 0, false)?;
+        if rest.is_empty() {
+            return None;
+        }
+        if matches!(rest.last().unwrap().as_ref(), ExpData::LoopCont(_, _, true)) {
+            Some(self.builder.if_else(
+                self.builder.not(cond),
+                rewrite_loop_nest(self.builder.env(), self.builder.seq(&default_loc, rest), -1),
+                self.builder.nop(&default_loc),
+            ))
+        } else {
+            None
+        }
+    }
+}
+
+// ===================================================================================
+
+/// A rewriter which eliminates useless assignments and introduces lets
+/// for all free variables.
+pub fn transform_assigns(target: &FunctionTarget, exp: Exp) -> Exp {
+    let usage = analyze_usage(target, exp.as_ref());
+    let builder = ExpBuilder::new(target.global_env());
+    let exp = AssignTransformer { usage, builder }.rewrite_exp(exp);
+    let usage = analyze_usage(target, exp.as_ref());
+    let builder = ExpBuilder::new(target.global_env());
+    FreeVariableBinder {
+        usage,
+        builder,
+        parameter_names: target
+            .get_parameters()
+            .map(|temp| target.get_local_name(temp))
+            .collect(),
+    }
+    .rewrite_exp(exp)
+}
+
+struct AssignTransformer<'a> {
+    /// Usage information about variables in the expression
+    usage: BTreeMap<NodeId, UsageInfo>,
+    /// The expression builder.
+    builder: ExpBuilder<'a>,
+}
+
+struct FreeVariableBinder<'a> {
+    /// Usage information about variables in the expression
+    usage: BTreeMap<NodeId, UsageInfo>,
+    /// The expression builder.
+    builder: ExpBuilder<'a>,
+    /// The symbolic names of function parameters
+    parameter_names: BTreeSet<Symbol>,
+}
+
+impl<'a> ExpRewriterFunctions for AssignTransformer<'a> {
+    fn rewrite_exp(&mut self, exp: Exp) -> Exp {
+        if let ExpData::Sequence(id, stms) = exp.as_ref() {
+            // If this is a sequence, simplify.
+            ExpData::Sequence(*id, self.simplify_seq(*id, stms)).into_exp()
+        } else {
+            self.rewrite_exp_descent(exp)
+        }
+    }
+}
+
+impl<'a> AssignTransformer<'a> {
+    fn simplify_seq(&mut self, seq_id: NodeId, stms: &[Exp]) -> Vec<Exp> {
+        let seq_usage = self.usage[&seq_id].clone();
+        let mut blocks = vec![];
+        let mut new_stms = vec![];
+        let mut substitution: BTreeMap<Symbol, Exp> = BTreeMap::new();
+        for stm in stms {
+            let stm_usage = self.usage[&stm.node_id()].clone();
+            match stm.as_ref() {
+                // Check whether an assignment can be eliminated because it is used only once.
+                // This is often the case with stackless bytecode generated
+                // from stack code.
+                ExpData::Assign(id, Pattern::Var(_, var), rhs)
+                if
+                // Cannot be read outside this block
+                seq_usage.read_count(*var) == 0 &&
+                    // Must be read zero or once inside the block
+                    stm_usage.read_count(*var) <= 1 &&
+                    // If it's been written to after, only via this exact statement (this
+                    // happens if we are in a loop).
+                    stm_usage.is_single_assignment(*var, id) &&
+                    // Must not be borrowed after this statement
+                    !stm_usage.is_borrowed(*var)
+                =>
+                    {
+                        substitution.insert(
+                            *var,
+                            self.rewrite_exp(self.builder.unfold(&substitution, rhs.clone())));
+                    },
+                // Check whether an assignment can be transformed into a let
+                ExpData::Assign(_, pat, rhs)
+                // None of the variables in the pattern is used after the block
+                if pat.vars().into_iter().all(|(_, var)| seq_usage.read_count(var) == 0) => {
+                    // Save building the block for later when we have the rest of the sequence
+                    blocks.push((new_stms, pat.clone(),
+                                 self.rewrite_exp(
+                                     self.builder.unfold(&substitution, rhs.clone()))));
+                    new_stms = vec![];
+                }
+                _ => {
+                    new_stms.push(self.rewrite_exp(
+                        self.builder.unfold(&substitution, stm.clone())))
+                },
+            }
+        }
+        let default_loc = self.builder.env().get_node_loc(seq_id);
+        // Process all blocks which have been saved for later
+        while let Some((prev_stms, pat, def)) = blocks.pop() {
+            let block =
+                self.builder
+                    .block(pat, Some(def), self.builder.seq(&default_loc, new_stms));
+            new_stms = prev_stms;
+            new_stms.push(block)
+        }
+        new_stms
+    }
+}
+
+impl<'a> ExpRewriterFunctions for FreeVariableBinder<'a> {
+    fn rewrite_exp(&mut self, exp: Exp) -> Exp {
+        let last = self.builder.extract_last(exp.clone()).1;
+        let last_id = last.node_id();
+        let exp = self.rewrite_exp_descent(exp);
+        if matches!(exp.as_ref(), ExpData::Sequence(..) | ExpData::Block(..)) {
+            if let Some(usage) = self.usage.get(&last_id) {
+                // Bind any locals which are still free and not used after this expression,
+                // and are not parameters.
+                let mut locals = vec![];
+                exp.visit_free_local_vars(|node_id, var| locals.push((node_id, var)));
+                let mut bound = BTreeSet::new();
+                for (node_id, var) in locals {
+                    if self.parameter_names.contains(&var) {
+                        // Do not bind parameters
+                        continue;
+                    }
+                    if bound.insert(var)
+                        // Check whether the variable is not used after this block
+                        && usage.read_count(var) == 0
+                    {
+                        return self.builder.block(
+                            Pattern::Var(self.builder.clone_node_id(node_id), var),
+                            None,
+                            exp.clone(),
+                        );
+                    }
+                }
+            }
+        }
+        exp
+    }
+}
+
+// ===================================================================================
+
+/// Rewrite an expression such that any break/continue nests referring to outer loops
+/// have the given delta added to their nesting. This simulates removing or adding a loop to
+/// the given expression. Nests bound to loops of the given expression are not effected.
+///
+/// If this is needed elsewhere we can move it out, currently it's a local helper.
+fn rewrite_loop_nest(_env: &GlobalEnv, exp: Exp, delta: isize) -> Exp {
+    LoopLifter {
+        loop_depth: 0,
+        delta,
+    }
+    .rewrite_exp(exp)
+}
+
+struct LoopLifter {
+    loop_depth: usize,
+    delta: isize,
+}
+
+impl ExpRewriterFunctions for LoopLifter {
+    fn rewrite_exp(&mut self, exp: Exp) -> Exp {
+        match exp.as_ref() {
+            ExpData::LoopCont(id, nest, cont) if *nest >= self.loop_depth => {
+                let new_nest = (*nest as isize) + self.delta;
+                assert!(
+                    new_nest >= 0,
+                    "loop removed which has break/continue references?"
+                );
+                ExpData::LoopCont(*id, new_nest as usize, *cont).into_exp()
+            },
+            ExpData::Loop(_, _) => {
+                self.loop_depth += 1;
+                let result = self.rewrite_exp_descent(exp);
+                self.loop_depth -= 1;
+                result
+            },
+            _ => self.rewrite_exp_descent(exp),
+        }
+    }
+}
+
+// ===================================================================================
+
+/// Usage information about variables in an expression.
+#[derive(Default, Clone, AbstractDomain)]
+struct UsageInfo {
+    /// Variables which are read by and after this expression.
+    reads: MapDomain<Symbol, SetDomain<NodeId>>,
+    /// Variables which are written by or after this expression.
+    writes: MapDomain<Symbol, SetDomain<NodeId>>,
+    /// Variables which are borrowed by or after this expression, immutable or mutable.
+    borrows: MapDomain<Symbol, SetDomain<NodeId>>,
+}
+
+/// Analyze the expression for variable usage and returns a map from node id
+/// to the info.
+fn analyze_usage(_target: &FunctionTarget, exp: &ExpData) -> BTreeMap<NodeId, UsageInfo> {
+    let mut step_fun = |state: &mut UsageInfo, e: &ExpData| {
+        use ExpData::*;
+        match e {
+            Assign(id, pat, rhs) => {
+                for (_, var) in pat.vars() {
+                    state.add_write(var, *id)
+                }
+                rhs.visit_free_local_vars(|id, var| state.add_read(var, id))
+            },
+            Block(id, pat, binding, body) => {
+                if let Some(b) = binding {
+                    b.visit_free_local_vars(|id, var| state.add_read(var, id))
+                }
+                for (_, var) in pat.vars() {
+                    state.add_write(var, *id)
+                }
+                body.visit_free_local_vars(|id, var| state.add_read(var, id))
+            },
+            Call(_, Operation::Borrow(kind), args) => args[0].visit_free_local_vars(|id, var| {
+                // Args supposed to be only a single variable, and marking everything in
+                // this exp as borrowed is safe.
+                if *kind == ReferenceKind::Mutable {
+                    state.add_write(var, id)
+                }
+                state.add_borrow(var, id);
+            }),
+            _ => e.visit_free_local_vars(|id, var| state.add_read(var, id)),
+        }
+    };
+    let mut analyzer = FixpointAnalyser::new(false, &mut step_fun);
+    analyzer.run_until_fixpoint(exp);
+    let mut post_state = BTreeMap::new();
+    analyzer.compute_post_state(&mut post_state, exp, UsageInfo::default());
+    if DEBUG {
+        debug!(
+            "usage: {}",
+            exp.display_with_annotator(_target.global_env(), &|id| {
+                if let Some(u) = post_state.get(&id) {
+                    u.debug_print(_target.global_env())
+                } else {
+                    "".to_string()
+                }
+            })
+        );
+    }
+    post_state
+}
+
+impl UsageInfo {
+    fn add_read(&mut self, var: Symbol, id: NodeId) {
+        self.reads.entry(var).or_default().insert(id);
+    }
+
+    fn add_borrow(&mut self, var: Symbol, id: NodeId) {
+        self.borrows.entry(var).or_default().insert(id);
+    }
+
+    fn add_write(&mut self, var: Symbol, id: NodeId) {
+        self.reads.remove(&var);
+        self.borrows.remove(&var);
+        self.writes.entry(var).or_default().insert(id);
+    }
+
+    fn read_count(&self, var: Symbol) -> usize {
+        self.reads.get(&var).map(|s| s.len()).unwrap_or(0)
+    }
+
+    /// Interpreting this as the post state, check whether a write
+    /// at the `at_id` is a single assignment. This is the
+    /// case if there is no further assignment after, or if the only
+    /// assignment is via the given `at_id` and reached via a loop.
+    ///
+    /// Notice that this is currently an over-approximation, it
+    /// would be perfectly valid to have multiple assignments
+    /// if the reaching definitions are unique.
+    fn is_single_assignment(&self, var: Symbol, at_id: &NodeId) -> bool {
+        self.writes
+            .get(&var)
+            .map(|s| s.is_empty() || s.len() == 1 && s.contains(at_id))
+            .unwrap_or(true)
+    }
+
+    fn is_borrowed(&self, var: Symbol) -> bool {
+        self.borrows
+            .get(&var)
+            .map(|s| !s.is_empty())
+            .unwrap_or(false)
+    }
+
+    #[allow(unused)]
+    fn debug_print(&self, env: &GlobalEnv) -> String {
+        let disp = |s: &str, d: &MapDomain<Symbol, SetDomain<NodeId>>| {
+            if d.is_empty() {
+                "".to_string()
+            } else {
+                format!(
+                    "{}={}",
+                    s,
+                    d.iter()
+                        .map(|(v, s)| format!("{}:{}", v.display(env.symbol_pool()), s.len()))
+                        .join(",")
+                )
+            }
+        };
+        format!(
+            "{}{}{}",
+            disp("r", &self.reads),
+            disp(",w", &self.writes),
+            disp(",b", &self.borrows)
+        )
+    }
+}
+
+// ===================================================================================
+
+// A small dataflow analysis framework for ASTs in the form as generated by the
+// AST generator:
+//
+// 1. All control structures (IfElse, Loop, LoopCont) are on top-level and not
+//    nested inside expressions.
+// 2. There are no Block (let) bindings but just assignments.
+//
+// We may want to pull this out as a general tool for arbitrary expressions, but right
+// now it's tailored for the use case here if we consider this normal form useful
+// for other use cases as well.
+
+struct FixpointAnalyser<'a, D, F> {
+    forward: bool,
+    state: BTreeMap<NodeId, D>,
+    changed: JoinResult,
+    cont_to_loop: BTreeMap<NodeId, NodeId>,
+    loop_to_cont: BTreeMap<NodeId, BTreeMap<NodeId, bool>>,
+    step_fun: &'a mut F,
+}
+
+impl<'a, D, F> FixpointAnalyser<'a, D, F>
+where
+    D: AbstractDomain + Default + Clone,
+    F: FnMut(&mut D, &ExpData),
+{
+    fn new(forward: bool, step_fun: &'a mut F) -> Self {
+        Self {
+            forward,
+            state: BTreeMap::new(),
+            changed: JoinResult::Unchanged,
+            cont_to_loop: BTreeMap::new(),
+            loop_to_cont: BTreeMap::new(),
+            step_fun,
+        }
+    }
+
+    fn run_until_fixpoint(&mut self, exp: &ExpData) {
+        (self.loop_to_cont, self.cont_to_loop) = exp.compute_loop_bindings();
+        loop {
+            let mut state = D::default();
+            self.changed = JoinResult::Unchanged;
+            self.run(&mut state, exp);
+            if self.changed == JoinResult::Unchanged {
+                break;
+            }
+        }
+    }
+
+    /// Compute a post-state mapping for each node, that is associate the D
+    /// of the node following in the control flow.
+    fn compute_post_state(
+        &self,
+        post_state_map: &mut BTreeMap<NodeId, D>,
+        exp: &ExpData,
+        mut post_state: D,
+    ) {
+        post_state_map.insert(exp.node_id(), post_state.clone());
+        match exp {
+            ExpData::Sequence(_, stms) if !stms.is_empty() => {
+                for stm in stms.iter().rev() {
+                    self.compute_post_state(post_state_map, stm.as_ref(), post_state);
+                    post_state = self.state[&stm.node_id()].clone();
+                }
+            },
+            ExpData::Loop(_, body) => self.compute_post_state(post_state_map, body, post_state),
+            ExpData::IfElse(_, _, if_true, if_false) => {
+                self.compute_post_state(post_state_map, if_true, post_state.clone());
+                self.compute_post_state(post_state_map, if_false, post_state.clone())
+            },
+            _ => {
+                // leaf
+            },
+        }
+    }
+
+    fn run(&mut self, state: &mut D, exp: &ExpData) {
+        use ExpData::*;
+        match exp {
+            IfElse(id, cond, true_branch, false_branch) => {
+                if self.forward {
+                    (self.step_fun)(state, cond.as_ref());
+                }
+                let mut false_state = state.clone();
+                self.run(state, true_branch);
+                self.run(&mut false_state, false_branch);
+                state.join(&false_state);
+                if !self.forward {
+                    (self.step_fun)(state, cond.as_ref());
+                }
+                self.join(state, id)
+            },
+            Sequence(id, stms) => {
+                if self.forward {
+                    for stm in stms {
+                        self.run(state, stm)
+                    }
+                } else {
+                    for stm in stms.iter().rev() {
+                        self.run(state, stm)
+                    }
+                }
+                self.join(state, id)
+            },
+            Loop(id, body) => {
+                if !self.forward {
+                    // On backward analysis, we first need to push the current state to the
+                    // breaks of the loops, then analyse the body, and push back
+                    // end state to continues. Because the loop has no backwards
+                    // entry, clear the state before entering the body.
+                    for (cont_id, is_cont) in &self.loop_to_cont[id].clone() {
+                        if !*is_cont {
+                            self.join(state, cont_id)
+                        }
+                    }
+                    *state = D::default();
+                    self.run(state, body.as_ref());
+                    for (cont_id, is_cont) in &self.loop_to_cont[id].clone() {
+                        if *is_cont {
+                            self.join(state, cont_id)
+                        }
+                    }
+                    self.join(state, id)
+                } else {
+                    // On forward analysis, we need to merge the state of the continues
+                    // into the current state, then analyze the body, and then push
+                    // the state of the loop breaks into the end state.
+                    for (cont_id, is_cont) in &self.loop_to_cont[id].clone() {
+                        if *is_cont {
+                            self.join(state, cont_id)
+                        }
+                    }
+                    self.run(state, body.as_ref());
+                    for (cont_id, is_cont) in &self.loop_to_cont[id].clone() {
+                        if !*is_cont {
+                            self.join(state, cont_id)
+                        }
+                    }
+                    self.join(state, id)
+                }
+            },
+            _ => {
+                // All other expressions are treated as "flat", that is, we directly
+                // call the step function on them.
+                if !self.forward && self.is_terminator(exp) {
+                    // Input state is empty
+                    *state = D::default();
+                }
+                (self.step_fun)(state, exp);
+                self.join(state, &exp.node_id());
+                if self.forward && self.is_terminator(exp) {
+                    // Output state is empty
+                    *state = D::default();
+                }
+            },
+        }
+    }
+
+    #[allow(unused)]
+    fn state(&self, id: &NodeId) -> Option<&D> {
+        self.state.get(id)
+    }
+
+    fn join(&mut self, state: &mut D, id: &NodeId) {
+        if let Some(old_state) = self.state.get_mut(id) {
+            self.changed |= old_state.join(state);
+            *state = old_state.clone()
+        } else {
+            self.state.insert(*id, state.clone());
+            self.changed = JoinResult::Changed
+        }
+    }
+
+    pub fn is_terminator(&self, exp: &ExpData) -> bool {
+        matches!(
+            exp,
+            ExpData::LoopCont(..) | ExpData::Return(..) | ExpData::Call(_, Operation::Abort, ..)
+        )
+    }
+}
diff --git a/third_party/move/move-model/bytecode/src/dataflow_domains.rs b/third_party/move/move-model/bytecode/src/dataflow_domains.rs
index dd5d6b6d6d5e9..d7881dbf3946a 100644
--- a/third_party/move/move-model/bytecode/src/dataflow_domains.rs
+++ b/third_party/move/move-model/bytecode/src/dataflow_domains.rs
@@ -10,9 +10,8 @@ use std::{
     borrow::Borrow,
     collections::{BTreeMap, BTreeSet},
     fmt::Debug,
-    ops::{Deref, DerefMut},
+    ops::{BitOrAssign, Deref, DerefMut},
 };
-
 // ================================================================================================
 // Abstract Domains
 
@@ -39,6 +38,12 @@ impl JoinResult {
     }
 }
 
+impl BitOrAssign for JoinResult {
+    fn bitor_assign(&mut self, rhs: Self) {
+        *self = self.combine(rhs)
+    }
+}
+
 /// A trait to be implemented by domains which support a join.
 pub trait AbstractDomain {
     fn join(&mut self, other: &Self) -> JoinResult;
diff --git a/third_party/move/move-model/bytecode/src/lib.rs b/third_party/move/move-model/bytecode/src/lib.rs
index efaf6a670dfce..3a5ba5eae3fc4 100644
--- a/third_party/move/move-model/bytecode/src/lib.rs
+++ b/third_party/move/move-model/bytecode/src/lib.rs
@@ -9,6 +9,7 @@ use move_model::model::GlobalEnv;
 use std::fmt::Write;
 
 pub mod annotations;
+pub mod astifier;
 pub mod borrow_analysis;
 pub mod compositional_analysis;
 pub mod dataflow_analysis;
diff --git a/third_party/move/move-model/bytecode/src/stackless_bytecode.rs b/third_party/move/move-model/bytecode/src/stackless_bytecode.rs
index e94cbf55f89b4..0fc475a821a39 100644
--- a/third_party/move/move-model/bytecode/src/stackless_bytecode.rs
+++ b/third_party/move/move-model/bytecode/src/stackless_bytecode.rs
@@ -9,12 +9,13 @@ use move_binary_format::file_format::CodeOffset;
 use move_core_types::{u256, value::MoveValue};
 use move_model::{
     ast,
-    ast::{Address, Exp, ExpData, MemoryLabel, Spec, TempIndex, TraceKind},
+    ast::{Address, Exp, ExpData, MemoryLabel, Spec, TempIndex, TraceKind, Value},
     exp_rewriter::{ExpRewriter, ExpRewriterFunctions, RewriteTarget},
     model::{FunId, GlobalEnv, ModuleId, NodeId, QualifiedInstId, SpecVarId, StructId},
     symbol::Symbol,
     ty::{Type, TypeDisplayContext},
 };
+use num::{bigint::Sign, BigInt};
 use std::{
     collections::{BTreeMap, BTreeSet},
     fmt,
@@ -35,6 +36,12 @@ impl Label {
     }
 }
 
+impl fmt::Display for Label {
+    fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
+        write!(f, "L{}", self.0)
+    }
+}
+
 /// An id for an attribute attached to an instruction.
 #[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Clone, Copy)]
 pub struct AttrId(u16);
@@ -139,6 +146,28 @@ impl Constant {
             Constant::Vector(v) => MoveValue::Vector(v.iter().map(|x| x.to_move_value()).collect()),
         }
     }
+
+    pub fn to_model_value(&self) -> Value {
+        match self {
+            Constant::Bool(x) => Value::Bool(*x),
+            Constant::U8(x) => Value::Number((*x).into()),
+            Constant::U16(x) => Value::Number((*x).into()),
+            Constant::U32(x) => Value::Number((*x).into()),
+            Constant::U64(x) => Value::Number((*x).into()),
+            Constant::U128(x) => Value::Number((*x).into()),
+            Constant::U256(x) => {
+                Value::Number(BigInt::from_bytes_le(Sign::NoSign, &x.to_le_bytes()))
+            },
+            Constant::Address(a) => Value::Address(a.clone()),
+            Constant::Vector(v) => Value::Vector(v.iter().map(|x| x.to_model_value()).collect()),
+            Constant::ByteArray(v) => {
+                Value::Vector(v.iter().map(|x| Value::Number((*x).into())).collect())
+            },
+            Constant::AddressArray(v) => {
+                Value::Vector(v.iter().map(|x| Value::Address(x.clone())).collect())
+            },
+        }
+    }
 }
 
 /// An operation -- target of a call. This contains user functions, builtin functions, and
diff --git a/third_party/move/move-model/bytecode/src/stackless_control_flow_graph.rs b/third_party/move/move-model/bytecode/src/stackless_control_flow_graph.rs
index 0a3be0beaf245..2cbc584d557e0 100644
--- a/third_party/move/move-model/bytecode/src/stackless_control_flow_graph.rs
+++ b/third_party/move/move-model/bytecode/src/stackless_control_flow_graph.rs
@@ -11,7 +11,10 @@ use crate::{
 };
 use move_binary_format::file_format::CodeOffset;
 use petgraph::{dot::Dot, graph::Graph};
-use std::collections::{BTreeMap, BTreeSet};
+use std::{
+    collections::{BTreeMap, BTreeSet},
+    ops::Range,
+};
 
 type Map<K, V> = BTreeMap<K, V>;
 type Set<V> = BTreeSet<V>;
@@ -52,6 +55,8 @@ impl StacklessControlFlowGraph {
 
     /// If from_all_blocks is false, perform backward analysis only from blocks that may exit.
     /// If from_all_blocks is true, perform backward analysis from all blocks.
+    /// Notice that it is guaranteed that forward and backward graphs use the
+    /// same block numbering.
     pub fn new_backward(code: &[Bytecode], from_all_blocks: bool) -> Self {
         let blocks = Self::collect_blocks(code);
         let mut block_id_to_predecessors: Map<BlockId, Vec<BlockId>> =
@@ -216,10 +221,36 @@ impl StacklessControlFlowGraph {
         &self.blocks[&block_id].content
     }
 
+    pub fn code_range(&self, block_id: BlockId) -> Range<usize> {
+        match self.content(block_id) {
+            BlockContent::Basic { lower, upper } => *lower as usize..(*upper as usize + 1),
+            BlockContent::Dummy => 0..0,
+        }
+    }
+
     pub fn blocks(&self) -> Vec<BlockId> {
         self.blocks.keys().cloned().collect()
     }
 
+    pub fn reachable_blocks(
+        &self,
+        from: BlockId,
+        mut edge_filter: impl FnMut(BlockId, BlockId) -> bool,
+    ) -> BTreeSet<BlockId> {
+        let mut result = BTreeSet::new();
+        let mut todo = vec![from];
+        while let Some(blk_id) = todo.pop() {
+            if result.insert(blk_id) {
+                for succ in self.successors(blk_id) {
+                    if edge_filter(blk_id, *succ) {
+                        todo.push(*succ)
+                    }
+                }
+            }
+        }
+        result
+    }
+
     pub fn entry_block(&self) -> BlockId {
         self.entry_block_id
     }
@@ -232,6 +263,20 @@ impl StacklessControlFlowGraph {
         }
     }
 
+    pub fn enclosing_block(&self, code_offset: CodeOffset) -> BlockId {
+        for (blk_id, block) in &self.blocks {
+            match &block.content {
+                BlockContent::Basic { lower, upper }
+                    if (*lower..=*upper).contains(&code_offset) =>
+                {
+                    return *blk_id
+                },
+                _ => {},
+            }
+        }
+        panic!("code offset not in the control flow graph")
+    }
+
     pub fn instr_indexes(
         &self,
         block_id: BlockId,
diff --git a/third_party/move/move-model/src/ast.rs b/third_party/move/move-model/src/ast.rs
index d0c762a3b4ae9..4449fadd47d74 100644
--- a/third_party/move/move-model/src/ast.rs
+++ b/third_party/move/move-model/src/ast.rs
@@ -626,11 +626,14 @@ pub enum ExpData {
     Return(NodeId, Exp),
     /// Represents a sequence of effects, the last value also being the result.
     Sequence(NodeId, Vec<Exp>),
-    /// Represents a loop, with a body expression.
+    /// Represents a loop.
     Loop(NodeId, Exp),
-    /// Represents a loop continuation for the enclosing loop. The bool indicates whether the
-    /// loop is continued (true) or broken (false).
-    LoopCont(NodeId, bool),
+    /// Represents a loop continuation, as in `LoopCont(id, nest, is_continue)`. `nest`
+    /// determines how many nesting levels the associated loop is away from the given
+    /// expression. For example, `0` means the directly enclosing loop, `1` the
+    /// loop enclosing that inner loop, and so on. `is_continue` indicates whether
+    /// the loop is continued or broken.
+    LoopCont(NodeId, usize, bool),
     /// Assignment to a pattern. Can be a tuple pattern and a tuple expression.  Note that Assign
     /// does *not* introduce new variables; they apparently be introduced by a Block or Lambda, or
     /// as a function formal parameter.
@@ -734,7 +737,7 @@ impl ExpData {
             self,
             ExpData::Sequence(_, _)
                 | ExpData::Loop(_, _)
-                | ExpData::LoopCont(_, _)
+                | ExpData::LoopCont(_, _, _)
                 | ExpData::Return(_, _)
         )
     }
@@ -825,7 +828,7 @@ impl ExpData {
     }
 
     /// Visits free local variables with node id in this expression.
-    fn visit_free_local_vars<F>(&self, mut node_symbol_visitor: F)
+    pub fn visit_free_local_vars<F>(&self, mut node_symbol_visitor: F)
     where
         F: FnMut(NodeId, Symbol),
     {
@@ -994,11 +997,19 @@ impl ExpData {
 
     /// Returns the temporaries used in this expression, with types. Result is ordered by occurrence.
     pub fn used_temporaries_with_types(&self, env: &GlobalEnv) -> Vec<(TempIndex, Type)> {
+        self.used_temporaries_with_ids()
+            .into_iter()
+            .map(|(t, i)| (t, env.get_node_type(i)))
+            .collect()
+    }
+
+    /// Returns the temporaries used in this expression, together with the node id of their usage.
+    pub fn used_temporaries_with_ids(&self) -> Vec<(TempIndex, NodeId)> {
         let mut temps = vec![];
         let mut visitor = |e: &ExpData| {
             if let ExpData::Temporary(id, idx) = e {
                 if !temps.iter().any(|(i, _)| i == idx) {
-                    temps.push((*idx, env.get_node_type(*id)));
+                    temps.push((*idx, *id));
                 }
             }
             true // keep going
@@ -1080,8 +1091,14 @@ impl ExpData {
         let mut has_exit = false;
         let mut visitor = |post: bool, e: &ExpData| {
             match e {
-                ExpData::Loop(_, _) => loop_count += if post { -1 } else { 1 },
-                ExpData::LoopCont(_, _) if loop_count == 0 => {
+                ExpData::Loop(_, _) => {
+                    if post {
+                        loop_count -= 1
+                    } else {
+                        loop_count += 1
+                    }
+                },
+                ExpData::LoopCont(_, nest, _) if loop_count == *nest => {
                     has_exit = true;
                     return false; // found an exit, exit visit early
                 },
@@ -1093,6 +1110,54 @@ impl ExpData {
         has_exit
     }
 
+    /// Compute the bindings of break/continue expressions to the associated loop. This
+    /// returns two maps: the first maps loop ids to the ids of the loop-cont statements,
+    /// together with whether they are break or continue. The 2nd maps loop-cont ids
+    /// to the associated loop ids.
+    pub fn compute_loop_bindings(
+        &self,
+    ) -> (
+        BTreeMap<NodeId, BTreeMap<NodeId, bool>>,
+        BTreeMap<NodeId, NodeId>,
+    ) {
+        let mut loop_to_cont = BTreeMap::<NodeId, BTreeMap<NodeId, bool>>::new();
+        let mut cont_to_loop = BTreeMap::<NodeId, NodeId>::new();
+        let mut loop_stack = vec![];
+        let mut visit_binding = |post: bool, exp: &ExpData| {
+            use ExpData::*;
+            match exp {
+                Loop(id, _) => {
+                    if !post {
+                        loop_to_cont.insert(*id, BTreeMap::new());
+                        loop_stack.push(*id);
+                    } else {
+                        loop_stack.pop().unwrap();
+                    }
+                },
+                LoopCont(id, nest, is_continue) => {
+                    if !post && *nest < loop_stack.len() {
+                        assert!(
+                            *nest < loop_stack.len(),
+                            "nest={} out of range for len={}",
+                            nest,
+                            loop_stack.len()
+                        );
+                        let loop_id = loop_stack[loop_stack.len() - nest - 1];
+                        loop_to_cont
+                            .get_mut(&loop_id)
+                            .unwrap()
+                            .insert(*id, *is_continue);
+                        cont_to_loop.insert(*id, loop_id);
+                    }
+                },
+                _ => {},
+            }
+            true
+        };
+        self.visit_pre_post(&mut visit_binding);
+        (loop_to_cont, cont_to_loop)
+    }
+
     /// Returns true of the given expression is valid for a constant expression.
     /// If not valid, then returns false and adds reasons why not to the argument reasons.
     ///
@@ -2912,6 +2977,7 @@ impl ExpData {
             exp: self,
             fun_env: None,
             verbose: false,
+            annotator: None,
         }
     }
 
@@ -2923,6 +2989,7 @@ impl ExpData {
             exp: self,
             fun_env: Some(fun_env),
             verbose: false,
+            annotator: None,
         }
     }
 
@@ -2932,16 +2999,34 @@ impl ExpData {
             exp: self,
             fun_env: other.fun_env.clone(),
             verbose: other.verbose,
+            annotator: other.annotator,
         }
     }
 
-    #[allow(unused)]
     pub fn display_verbose<'a>(&'a self, env: &'a GlobalEnv) -> ExpDisplay<'a> {
         ExpDisplay {
             env,
             exp: self,
             fun_env: None,
             verbose: true,
+            annotator: None,
+        }
+    }
+
+    pub fn display_with_annotator<'a, F>(
+        &'a self,
+        env: &'a GlobalEnv,
+        annotator: &'a F,
+    ) -> ExpDisplay<'a>
+    where
+        F: Fn(NodeId) -> String,
+    {
+        ExpDisplay {
+            env,
+            exp: self,
+            fun_env: None,
+            verbose: false,
+            annotator: Some(annotator),
         }
     }
 }
@@ -2952,6 +3037,7 @@ pub struct ExpDisplay<'a> {
     exp: &'a ExpData,
     fun_env: Option<FunctionEnv<'a>>,
     verbose: bool,
+    annotator: Option<&'a dyn Fn(NodeId) -> String>,
 }
 
 impl<'a> fmt::Display for ExpDisplay<'a> {
@@ -2961,6 +3047,13 @@ impl<'a> fmt::Display for ExpDisplay<'a> {
             let node_id = self.exp.node_id();
             write!(f, "{}:(", node_id.as_usize())?;
         }
+        if let Some(an) = &self.annotator {
+            let node_id = self.exp.node_id();
+            let s = (*an)(node_id);
+            if !s.is_empty() {
+                write!(f, "{{{}}} ", s)?;
+            }
+        }
         match self.exp {
             Invalid(_) => write!(f, "*invalid*"),
             Value(_, v) => write!(f, "{}", self.env.display(v)),
@@ -3061,13 +3154,34 @@ impl<'a> fmt::Display for ExpDisplay<'a> {
                 write!(f, "({})({})", fun.display_cont(self), self.fmt_exps(args))
             },
             IfElse(_, cond, if_exp, else_exp) => {
-                write!(
-                    f,
-                    "if {} {{\n  {}\n}} else {{\n  {}\n}}",
-                    cond.display_cont(self),
-                    indent(if_exp.display_cont(self)),
-                    indent(else_exp.display_cont(self))
-                )
+                // Special case `if (c) simple_exp`
+                match (if_exp.as_ref(), else_exp.as_ref()) {
+                    (e, Sequence(_, stms)) if !matches!(e, Sequence(..)) && stms.is_empty() => {
+                        write!(
+                            f,
+                            "if ({}) {}",
+                            cond.display_cont(self),
+                            if_exp.display_cont(self)
+                        )
+                    },
+                    (_, Sequence(_, stms)) if stms.is_empty() => {
+                        write!(
+                            f,
+                            "if {} {{\n  {}\n}}",
+                            cond.display_cont(self),
+                            indent(if_exp.display_cont(self)),
+                        )
+                    },
+                    _ => {
+                        write!(
+                            f,
+                            "if {} {{\n  {}\n}} else {{\n  {}\n}}",
+                            cond.display_cont(self),
+                            indent(if_exp.display_cont(self)),
+                            indent(else_exp.display_cont(self))
+                        )
+                    },
+                }
             },
             Match(_, discriminator, arms) => {
                 writeln!(f, "match ({}) {{", discriminator.display_cont(self))?;
@@ -3094,8 +3208,18 @@ impl<'a> fmt::Display for ExpDisplay<'a> {
             Loop(_, e) => {
                 write!(f, "loop {{\n  {}\n}}", indent(e.display_cont(self)))
             },
-            LoopCont(_, true) => write!(f, "continue"),
-            LoopCont(_, false) => write!(f, "break"),
+            LoopCont(_, nest, continues) => {
+                write!(
+                    f,
+                    "{}{}",
+                    if *continues { "continue" } else { "break" },
+                    if *nest > 0 {
+                        format!("[{}]", nest)
+                    } else {
+                        "".to_string()
+                    }
+                )
+            },
             Return(_, e) => write!(f, "return {}", e.display_cont(self)),
             Assign(_, lhs, rhs) => {
                 write!(
diff --git a/third_party/move/move-model/src/builder/exp_builder.rs b/third_party/move/move-model/src/builder/exp_builder.rs
index 21e7e4369562c..2045cecf55314 100644
--- a/third_party/move/move-model/src/builder/exp_builder.rs
+++ b/third_party/move/move-model/src/builder/exp_builder.rs
@@ -1563,7 +1563,7 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo
                         id,
                         cond.into_exp(),
                         body.into_exp(),
-                        ExpData::LoopCont(id, false).into_exp(),
+                        ExpData::LoopCont(id, 0, false).into_exp(),
                     )
                     .into_exp(),
                 )
@@ -1583,12 +1583,12 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo
             EA::Exp_::Break => {
                 // Type of `break` is arbitrary
                 let id = self.new_node_id_with_type_loc(expected_type, &loc);
-                ExpData::LoopCont(id, false)
+                ExpData::LoopCont(id, 0, false)
             },
             EA::Exp_::Continue => {
                 // Type of `continue` is arbitrary
                 let id = self.new_node_id_with_type_loc(expected_type, &loc);
-                ExpData::LoopCont(id, true)
+                ExpData::LoopCont(id, 0, true)
             },
             EA::Exp_::Block(seq) => self.translate_seq(&loc, seq, expected_type, context),
             EA::Exp_::Lambda(bindings, exp) => {
diff --git a/third_party/move/move-model/src/exp_builder.rs b/third_party/move/move-model/src/exp_builder.rs
new file mode 100644
index 0000000000000..fd3aa479ef05d
--- /dev/null
+++ b/third_party/move/move-model/src/exp_builder.rs
@@ -0,0 +1,178 @@
+// Copyright © Aptos Foundation
+// Parts of the project are originally copyright © Meta Platforms, Inc.
+// SPDX-License-Identifier: Apache-2.0
+
+//! A helper for building expressions
+
+use crate::{
+    ast::{Exp, ExpData, Operation, Pattern, RewriteResult},
+    model::{GlobalEnv, Loc, NodeId},
+    symbol::Symbol,
+    ty::Type,
+};
+use itertools::Itertools;
+use std::collections::BTreeMap;
+
+/// Represents an expression builder.
+pub struct ExpBuilder<'a> {
+    env: &'a GlobalEnv,
+}
+
+impl<'a> ExpBuilder<'a> {
+    pub fn new(env: &'a GlobalEnv) -> Self {
+        Self { env }
+    }
+
+    pub fn env(&self) -> &GlobalEnv {
+        self.env
+    }
+
+    pub fn not(&self, exp: Exp) -> Exp {
+        if let ExpData::Call(_, Operation::Not, args) = exp.as_ref() {
+            args.last().expect("malformed expression").clone()
+        } else {
+            ExpData::Call(self.clone_node_id(exp.node_id()), Operation::Not, vec![exp]).into_exp()
+        }
+    }
+
+    pub fn if_else(&self, cond: Exp, if_true: Exp, if_false: Exp) -> Exp {
+        let loc = self.enclosing_loc([&cond, &if_true, &if_false].into_iter());
+        let ty = self.env.get_node_type(if_true.node_id());
+        let id = self.new_node_id(loc, ty);
+        ExpData::IfElse(id, cond, if_true, if_false).into_exp()
+    }
+
+    pub fn if_(&self, cond: Exp, then: Exp) -> Exp {
+        let loc = self.enclosing_loc([&cond, &then].into_iter());
+        ExpData::IfElse(
+            self.new_node_id(loc.clone(), Type::unit()),
+            cond,
+            then,
+            self.nop(&loc),
+        )
+        .into_exp()
+    }
+
+    pub fn break_(&self, loc: &Loc, nest: usize) -> Exp {
+        ExpData::LoopCont(self.new_node_id(loc.clone(), Type::unit()), nest, false).into_exp()
+    }
+
+    pub fn continue_(&self, loc: &Loc, nest: usize) -> Exp {
+        ExpData::LoopCont(self.new_node_id(loc.clone(), Type::unit()), nest, true).into_exp()
+    }
+
+    pub fn seq(&self, nop_loc: &Loc, stms: Vec<Exp>) -> Exp {
+        if stms.is_empty() {
+            self.nop(nop_loc)
+        } else {
+            let ty = if let Some(last) = stms.last() {
+                self.env.get_node_type(last.node_id())
+            } else {
+                Type::unit()
+            };
+            let loc = self.enclosing_loc(stms.iter());
+            ExpData::Sequence(self.new_node_id(loc, ty), stms).into_exp()
+        }
+    }
+
+    pub fn block(&self, pat: Pattern, def: Option<Exp>, body: Exp) -> Exp {
+        let node_id = self.clone_node_id(body.node_id());
+        ExpData::Block(node_id, pat, def, body).into_exp()
+    }
+
+    pub fn nop(&self, loc: &Loc) -> Exp {
+        ExpData::Sequence(self.new_node_id(loc.clone(), Type::unit()), vec![]).into_exp()
+    }
+
+    pub fn unfold(&self, substitution: &BTreeMap<Symbol, Exp>, exp: Exp) -> Exp {
+        ExpData::rewrite(exp, &mut |e: Exp| {
+            if let ExpData::LocalVar(_, name) = e.as_ref() {
+                if let Some(r) = substitution.get(name) {
+                    return RewriteResult::Rewritten(ExpData::rewrite_node_id(
+                        r.clone(),
+                        &mut |id| Some(self.clone_node_id(id)),
+                    ));
+                }
+            }
+            RewriteResult::Unchanged(e)
+        })
+    }
+
+    pub fn match_loop(&self, exp: Exp) -> Option<(NodeId, Exp)> {
+        if let ExpData::Loop(id, body) = exp.as_ref() {
+            Some((*id, body.clone()))
+        } else {
+            None
+        }
+    }
+
+    pub fn extract_first(&self, exp: Exp) -> (Exp, Vec<Exp>) {
+        match exp.as_ref() {
+            ExpData::Sequence(_, exps) if !exps.is_empty() => {
+                (exps[0].clone(), exps.iter().skip(1).cloned().collect())
+            },
+            _ => (exp, vec![]),
+        }
+    }
+
+    pub fn extract_last(&self, exp: Exp) -> (Vec<Exp>, Exp) {
+        match exp.as_ref() {
+            ExpData::Sequence(_, exps) if !exps.is_empty() => {
+                let n = exps.len();
+                (
+                    exps.iter().take(n - 1).cloned().collect(),
+                    exps[n - 1].clone(),
+                )
+            },
+            _ => (vec![], exp),
+        }
+    }
+
+    pub fn match_if(&self, exp: Exp) -> Option<(Exp, Exp)> {
+        match exp.as_ref() {
+            ExpData::IfElse(_, cond, if_true, if_false) if self.is_empty_exp(if_false) => {
+                Some((cond.clone(), if_true.clone()))
+            },
+            _ => None,
+        }
+    }
+
+    pub fn match_if_loop_cont(&self, exp: Exp, nest: usize, is_continue: bool) -> Option<Exp> {
+        let (cond, if_true) = self.match_if(exp)?;
+        if self.is_loop_cont(&if_true, nest, is_continue) {
+            Some(cond)
+        } else {
+            None
+        }
+    }
+
+    pub fn is_loop_cont(&self, exp: &Exp, nest: usize, is_continue: bool) -> bool {
+        matches!(exp.as_ref(),
+            ExpData::LoopCont(_, nest1, is_continue1) if *nest1 == nest && *is_continue1 == is_continue)
+    }
+
+    pub fn is_empty_exp(&self, exp: &Exp) -> bool {
+        matches!(exp.as_ref(), ExpData::Sequence(_, stms) if stms.is_empty())
+    }
+
+    pub fn new_node_id(&self, loc: Loc, ty: Type) -> NodeId {
+        self.env.new_node(loc, ty)
+    }
+
+    pub fn clone_node_id(&self, id: NodeId) -> NodeId {
+        let env = self.env;
+        let new_id = env.new_node(env.get_node_loc(id), env.get_node_type(id));
+        if let Some(inst) = env.get_node_instantiation_opt(id) {
+            env.set_node_instantiation(new_id, inst.clone())
+        }
+        new_id
+    }
+
+    fn enclosing_loc<'b>(&self, exps: impl Iterator<Item = &'b Exp>) -> Loc {
+        Loc::enclosing(
+            exps.map(|e| self.env.get_node_loc(e.node_id()))
+                .collect_vec()
+                .as_slice(),
+        )
+    }
+}
diff --git a/third_party/move/move-model/src/exp_rewriter.rs b/third_party/move/move-model/src/exp_rewriter.rs
index 21b33132f475f..d55b7842c3e1f 100644
--- a/third_party/move/move-model/src/exp_rewriter.rs
+++ b/third_party/move/move-model/src/exp_rewriter.rs
@@ -518,10 +518,10 @@ pub trait ExpRewriterFunctions {
                     exp
                 }
             },
-            LoopCont(id, do_cont) => {
+            LoopCont(id, nest, do_cont) => {
                 let (id_changed, new_id) = self.internal_rewrite_id(*id);
                 if id_changed {
-                    LoopCont(new_id, *do_cont).into_exp()
+                    LoopCont(new_id, *nest, *do_cont).into_exp()
                 } else {
                     exp
                 }
@@ -729,8 +729,6 @@ pub trait ExpRewriterFunctions {
     }
 
     fn internal_rewrite_vec(&mut self, exps: &[Exp]) -> Option<Vec<Exp>> {
-        // The vector rewrite works a bit different as we try to avoid constructing
-        // new vectors if nothing changed, and optimize common cases of 0-3 arguments.
         let (changevec, resvec): (Vec<_>, Vec<_>) = exps
             .iter()
             .map(|exp| self.internal_rewrite_exp(exp))
diff --git a/third_party/move/move-model/src/lib.rs b/third_party/move/move-model/src/lib.rs
index 3fa833f86f9a0..1c3f757298919 100644
--- a/third_party/move/move-model/src/lib.rs
+++ b/third_party/move/move-model/src/lib.rs
@@ -52,6 +52,7 @@ pub mod ast;
 mod builder;
 pub mod code_writer;
 pub mod constant_folder;
+pub mod exp_builder;
 pub mod exp_generator;
 pub mod exp_rewriter;
 pub mod intrinsics;
diff --git a/third_party/move/move-model/src/model.rs b/third_party/move/move-model/src/model.rs
index a03fc714e1674..6a6373df041e3 100644
--- a/third_party/move/move-model/src/model.rs
+++ b/third_party/move/move-model/src/model.rs
@@ -179,9 +179,9 @@ impl Loc {
 
     /// Creates a location which encloses all the locations in the provided slice,
     /// which must not be empty. All locations are expected to be in the same file.
-    pub fn enclosing(locs: &[&Loc]) -> Loc {
+    pub fn enclosing(locs: &[Loc]) -> Loc {
         assert!(!locs.is_empty());
-        let loc = locs[0];
+        let loc = &locs[0];
         let mut start = loc.span.start();
         let mut end = loc.span.end();
         for l in locs.iter().skip(1) {
@@ -379,6 +379,12 @@ impl NodeId {
     }
 }
 
+impl AsRef<NodeId> for NodeId {
+    fn as_ref(&self) -> &NodeId {
+        self
+    }
+}
+
 impl ModuleId {
     pub fn new(idx: usize) -> Self {
         Self(idx as RawIndex)