diff --git a/.gitignore b/.gitignore
index 786a781cf..0e7e8b826 100644
--- a/.gitignore
+++ b/.gitignore
@@ -83,6 +83,9 @@
 .nra.cache
 .csdp.cache
 rust_projects/*
+/c2rust_testbed/*/*.s
+/c2rust_testbed/*/rust_project/
+/c2rust_testbed/*/tests/
 
 # Dune Build Results
 _build/
diff --git a/cfrontend/ClightCFG.v b/cfrontend/ClightCFG.v
index 1b8800820..cb5db094d 100644
--- a/cfrontend/ClightCFG.v
+++ b/cfrontend/ClightCFG.v
@@ -55,8 +55,6 @@ Module LBLMap := Coq.FSets.FMapList.Make(Positive_as_OT).
 (* set of bb_uids *)
 Module BBSet <: FSets.FSetInterface.S := FSets.FSetPositive.PositiveSet.
 
-
-
 Inductive Instruction :=
   | i_skip : Instruction
   | i_assign : Clight.expr -> Clight.expr -> Instruction
diff --git a/cfrontend/ClightCFGCNS.ml b/cfrontend/ClightCFGCNS.ml
new file mode 100644
index 000000000..056d86a4e
--- /dev/null
+++ b/cfrontend/ClightCFGCNS.ml
@@ -0,0 +1,285 @@
+open AST
+open BinNums
+open BinPos
+open ClightCFG
+open Ctypes
+open Errors
+
+let pos_eq a b =
+  match Pos.compare a b with
+  | Eq -> true
+  | _ -> false
+
+let pos_lt a b =
+  match Pos.compare a b with
+  | Lt -> true
+  | _ -> false
+
+let rec map_switch_targets old_uid new_uid = function
+  | SLnil b ->
+      if pos_eq b old_uid then SLnil new_uid else SLnil b
+  | SLcons (k, b, rest) ->
+      let b' = if pos_eq b old_uid then new_uid else b in
+      SLcons (k, b', map_switch_targets old_uid new_uid rest)
+
+let rec map_switch_targets_with_self old_uid self_uid = function
+  | SLnil b ->
+      if pos_eq b old_uid then SLnil self_uid else SLnil b
+  | SLcons (k, b, rest) ->
+      let b' = if pos_eq b old_uid then self_uid else b in
+      SLcons (k, b', map_switch_targets_with_self old_uid self_uid rest)
+
+let replace_target_in_edge edge old_uid new_uid =
+  match edge with
+  | Coq_direct b ->
+      if pos_eq b old_uid then Coq_direct new_uid else edge
+  | Coq_conditional (c, bt, bf) ->
+      let bt' = if pos_eq bt old_uid then new_uid else bt in
+      let bf' = if pos_eq bf old_uid then new_uid else bf in
+      Coq_conditional (c, bt', bf')
+  | Coq_switch (c, sl) ->
+      Coq_switch (c, map_switch_targets old_uid new_uid sl)
+  | Coq_terminate _ | Coq_stub ->
+      edge
+
+let map_self_target_in_edge edge old_uid self_uid =
+  match edge with
+  | Coq_direct b ->
+      if pos_eq b old_uid then Coq_direct self_uid else edge
+  | Coq_conditional (c, bt, bf) ->
+      let bt' = if pos_eq bt old_uid then self_uid else bt in
+      let bf' = if pos_eq bf old_uid then self_uid else bf in
+      Coq_conditional (c, bt', bf')
+  | Coq_switch (c, sl) ->
+      Coq_switch (c, map_switch_targets_with_self old_uid self_uid sl)
+  | Coq_terminate _ | Coq_stub ->
+      edge
+
+let successors_of_edge = function
+  | Coq_direct b -> [b]
+  | Coq_conditional (_, bt, bf) -> [bt; bf]
+  | Coq_switch (_, sl) ->
+      let rec walk acc = function
+        | SLnil b -> b :: acc
+        | SLcons (_, b, rest) -> walk (b :: acc) rest
+      in
+      walk [] sl
+  | Coq_terminate _ | Coq_stub -> []
+
+let successors_of_node cfg uid =
+  match BBMap.find uid cfg.map with
+  | Some (Coq_bb (_, edge)) -> successors_of_edge edge
+  | None -> []
+
+let add_pred pred target pred_map =
+  let old_preds =
+    match BBMap.find target pred_map with
+    | Some s -> s
+    | None -> BBSet.empty
+  in
+  BBMap.add target (BBSet.add pred old_preds) pred_map
+
+let compute_predecessors cfg =
+  let nodes = BBSet.elements cfg.node_set in
+  List.fold_left
+    (fun pred_map n ->
+      let succs = successors_of_node cfg n in
+      List.fold_left (fun acc s -> add_pred n s acc) pred_map succs)
+    BBMap.empty nodes
+
+let max_uid cfg =
+  let nodes = BBSet.elements cfg.node_set in
+  List.fold_left
+    (fun acc n -> if pos_lt acc n then n else acc)
+    cfg.entry nodes
+
+let dfs_postorder cfg start visited =
+  let rec go node (seen, order) =
+    if BBSet.mem node seen then
+      (seen, order)
+    else
+      let seen' = BBSet.add node seen in
+      let succs = successors_of_node cfg node in
+      let seen'', order' =
+        List.fold_left (fun st s -> go s st) (seen', order) succs
+      in
+      (seen'', node :: order')
+  in
+  go start (visited, [])
+
+let reverse_adj cfg =
+  let preds = compute_predecessors cfg in
+  fun n ->
+    match BBMap.find n preds with
+    | Some s -> BBSet.elements s
+    | None -> []
+
+let find_sccs cfg =
+  let nodes = BBSet.elements cfg.node_set in
+  let _, finishing =
+    List.fold_left
+      (fun (seen, order) n ->
+        if BBSet.mem n seen then
+          (seen, order)
+        else
+          let seen', post = dfs_postorder cfg n seen in
+          (seen', post @ order))
+      (BBSet.empty, []) nodes
+  in
+  let rev_succ = reverse_adj cfg in
+  let rec dfs_rev node seen acc =
+    if BBSet.mem node seen then
+      (seen, acc)
+    else
+      let seen' = BBSet.add node seen in
+      let nexts = rev_succ node in
+      List.fold_left
+        (fun (s, a) n -> dfs_rev n s a)
+        (seen', BBSet.add node acc) nexts
+  in
+  let _, sccs =
+    List.fold_left
+      (fun (seen, acc) n ->
+        if BBSet.mem n seen then
+          (seen, acc)
+        else
+          let seen', scc = dfs_rev n seen BBSet.empty in
+          (seen', scc :: acc))
+      (BBSet.empty, []) finishing
+  in
+  sccs
+
+let instruction_count cfg uid =
+  match BBMap.find uid cfg.map with
+  | Some (Coq_bb (insts, _)) -> List.length insts
+  | None -> 1
+
+let pred_count pred_map uid =
+  match BBMap.find uid pred_map with
+  | Some s -> List.length (BBSet.elements s)
+  | None -> 0
+
+let select_split_candidate cfg =
+  let pred_map = compute_predecessors cfg in
+  let sccs = find_sccs cfg in
+  let choose_better cfg pred_map best candidate =
+    let score n =
+      let q = max 1 (instruction_count cfg n) in
+      let p = max 1 (pred_count pred_map n) in
+      q * max 1 (p - 1)
+    in
+    match best with
+    | None -> Some candidate
+    | Some b ->
+        if score candidate < score b then Some candidate else best
+  in
+  List.fold_left
+    (fun best scc ->
+      let scc_nodes = BBSet.elements scc in
+      if List.length scc_nodes <= 1 then
+        best
+      else
+        let entry_nodes =
+          List.filter
+            (fun n ->
+              let preds =
+                match BBMap.find n pred_map with
+                | Some s -> BBSet.elements s
+                | None -> []
+              in
+              List.exists (fun p -> not (BBSet.mem p scc)) preds)
+            scc_nodes
+        in
+        if List.length entry_nodes <= 1 then
+          best
+        else
+          List.fold_left
+            (fun b n ->
+              if pos_eq n cfg.entry then b
+              else choose_better cfg pred_map b n)
+            best entry_nodes)
+    None sccs
+
+let split_node cfg target_uid =
+  let pred_map = compute_predecessors cfg in
+  let preds =
+    match BBMap.find target_uid pred_map with
+    | Some s -> BBSet.elements s |> List.filter (fun p -> not (pos_eq p target_uid))
+    | None -> []
+  in
+  if List.length preds <= 1 then
+    cfg
+  else
+    match BBMap.find target_uid cfg.map with
+    | None -> cfg
+    | Some (Coq_bb (insts, edge)) ->
+        let base = max_uid cfg in
+        let rec alloc cur ps acc =
+          match ps with
+          | [] -> (List.rev acc, cur)
+          | p :: rest ->
+              let next = Pos.succ cur in
+              alloc next rest ((p, next) :: acc)
+        in
+        let redirects, _ = alloc base preds [] in
+        let new_map =
+          List.fold_left
+            (fun m (pred_uid, new_uid) ->
+              let copied_edge = map_self_target_in_edge edge target_uid new_uid in
+              let m1 = BBMap.add new_uid (Coq_bb (insts, copied_edge)) m in
+              match BBMap.find pred_uid m1 with
+              | Some (Coq_bb (pinsts, pedge)) ->
+                  let pedge' = replace_target_in_edge pedge target_uid new_uid in
+                  BBMap.add pred_uid (Coq_bb (pinsts, pedge')) m1
+              | None -> m1)
+            cfg.map redirects
+        in
+        let new_map = BBMap.remove target_uid new_map in
+        let new_node_set =
+          List.fold_left
+            (fun s (_, u) -> BBSet.add u s)
+            (BBSet.remove target_uid cfg.node_set) redirects
+        in
+        {cfg with map = new_map; node_set = new_node_set}
+
+let make_cfg_reducible cfg =
+  let rec loop cur fuel =
+    if fuel <= 0 then
+      cur
+    else
+      match select_split_candidate cur with
+      | None -> cur
+      | Some uid ->
+          let next = split_node cur uid in
+          if BBSet.equal cur.node_set next.node_set then cur
+          else loop next (fuel - 1)
+  in
+  loop cfg 64
+
+let transl_internal_function (f : coq_function) : coq_function =
+  let cfg, extra = f.fn_body in
+  let cfg' = make_cfg_reducible cfg in
+  { fn_return = f.fn_return;
+    fn_callconv = f.fn_callconv;
+    fn_params = f.fn_params;
+    fn_vars = f.fn_vars;
+    fn_temps = f.fn_temps;
+    fn_body = (cfg', extra) }
+
+let transl_fundef (_id : ident) (fd : clightcfg_fundef) : clightcfg_fundef res =
+  match fd with
+  | Internal f -> OK (Internal (transl_internal_function f))
+  | External (a, b, c, d) -> OK (External (a, b, c, d))
+
+let transl_globvar (_id : ident) (ty : coq_type) : coq_type res = OK ty
+
+let transl_program (p : clightcfg_program) : clightcfg_program res =
+  match AST.transf_globdefs transl_fundef transl_globvar p.prog_defs with
+  | Error msg -> Error msg
+  | OK defs ->
+      OK
+        { prog_defs = defs;
+          prog_public = p.prog_public;
+          prog_main = p.prog_main;
+          prog_types = p.prog_types;
+          prog_comp_env = p.prog_comp_env }
diff --git a/cfrontend/PrintRustLight.ml b/cfrontend/PrintRustLight.ml
index e66aeafd8..523992cfe 100644
--- a/cfrontend/PrintRustLight.ml
+++ b/cfrontend/PrintRustLight.ml
@@ -791,6 +791,10 @@ let rec print_stmt fmt body =
   | S_sequence (RustLight.S_skip, s2) -> print_stmt fmt s2
   | S_sequence (s1, RustLight.S_skip) -> print_stmt fmt s1
   | S_sequence (e1, e2) -> fprintf fmt "%a@;%a" print_stmt e1 print_stmt e2
+  | S_block (Some lbl, stmt) ->
+      fprintf fmt "@[<v 2>'lbl_%ld: {@;%a@;<0 -2>}@]"
+        (camlint_of_coqint lbl) print_stmt stmt
+  | S_block (None, stmt) -> fprintf fmt "@[<v 2>{@;%a@;<0 -2>}@]" print_stmt stmt
   | S_continue None -> fprintf fmt "continue;"
   | S_continue (Some lbl) ->
       fprintf fmt "continue 'lbl_%ld;" (camlint_of_coqint lbl)
diff --git a/cfrontend/RustLight.v b/cfrontend/RustLight.v
index 34cba8acc..58c4b22b7 100644
--- a/cfrontend/RustLight.v
+++ b/cfrontend/RustLight.v
@@ -195,6 +195,7 @@ Inductive rstatement: Type :=
   | S_builtin: option ident -> external_function -> typelist -> list rexpr -> rstatement
   | S_sequence : rstatement -> rstatement -> rstatement
   | S_if_then_else : rexpr  -> rstatement -> rstatement -> rstatement
+  | S_block: option Z -> rstatement -> rstatement
   | S_loop: option Z -> rstatement -> rstatement -> rstatement
   (* outer lbl -> inner lbl -> block 1 -> block 2*)
   (* loop 'outer_lbl {loop 'inner_lbl {block 1; break; } block 2} *)
@@ -393,6 +394,7 @@ Fixpoint walk_r_body_for_symbols
       )
   | S_sequence s_1 s_2 => PositiveSet.union (walk_r_stmt s_1) (walk_r_stmt s_2)
   | S_continue _ => PositiveSet.empty
+  | S_block _ s_1 => walk_r_stmt s_1
   | S_loop _ s_1 s_2 => PositiveSet.union (walk_r_stmt s_1) (walk_r_stmt s_2)
   | S_loop2 _ _ s_1 s_2 => PositiveSet.union (walk_r_stmt s_1) (walk_r_stmt s_2)
   | S_match_int rexpr ls =>
@@ -504,6 +506,8 @@ Fixpoint walk_r_stmt_for_composite_types (stmt: rstatement) : PositiveSet.t :=
   | S_sequence s_1 s_2 =>
       PositiveSet.union (walk_r_stmt_for_composite_types s_1) (walk_r_stmt_for_composite_types s_2)
   | S_continue _ => PositiveSet.empty
+  | S_block _ s_1 =>
+      walk_r_stmt_for_composite_types s_1
   | S_loop _ s_1 s_2 =>
       PositiveSet.union (walk_r_stmt_for_composite_types s_1) (walk_r_stmt_for_composite_types s_2)
   | S_loop2 _ _ s_1 s_2 =>
diff --git a/cfrontend/RustLightInsertTypeCasts.v b/cfrontend/RustLightInsertTypeCasts.v
index 45f9649d0..1c04558a4 100644
--- a/cfrontend/RustLightInsertTypeCasts.v
+++ b/cfrontend/RustLightInsertTypeCasts.v
@@ -468,6 +468,9 @@ Fixpoint insert_cast_stmt (gvt: ident -> res type) (f_rty: type) (stmt: rstateme
       do r_exp1 <- insert_cast_stmt gvt f_rty exp1;
       do r_exp2 <- insert_cast_stmt gvt f_rty exp2;
       ret (S_sequence r_exp1 r_exp2)
+  | S_block l s =>
+      do rs <- insert_cast_stmt gvt f_rty s;
+      ret (S_block l rs)
   | S_return None => ret(stmt)
   | S_return (Some (exp, ty)) =>
     let exp_ty := r_typeof exp in
@@ -590,4 +593,3 @@ Definition transl_program (r_prog: r_program) : res (r_program) :=
       Ctypes.prog_comp_env_eq := r_prog.(prog_comp_env_eq);
     |} in
   OK(r_prog).
-
diff --git a/cfrontend/RustLightSplitExpr.v b/cfrontend/RustLightSplitExpr.v
index 333a315e2..013bdceb4 100644
--- a/cfrontend/RustLightSplitExpr.v
+++ b/cfrontend/RustLightSplitExpr.v
@@ -185,6 +185,9 @@ Fixpoint transl_stmt (s: rstatement) : mon rstatement :=
       gdo tr_s1 <- transl_stmt s1;
       gdo tr_s2 <- transl_stmt s2;
       ret(S_sequence tr_s1 tr_s2)
+  | S_block l s1 =>
+      gdo tr_s1 <- transl_stmt s1;
+      ret (S_block l tr_s1)
   | S_if_then_else cond s1 s2 =>
       gdo tr_s1 <- transl_stmt s1;
       gdo tr_s2 <- transl_stmt s2;
diff --git a/cfrontend/RustLightgen.v b/cfrontend/RustLightgen.v
index 50f5db5f7..523d52f9b 100644
--- a/cfrontend/RustLightgen.v
+++ b/cfrontend/RustLightgen.v
@@ -14,6 +14,7 @@ Import List.ListNotations.
 Notation "'TODO'" := (ltac:(fail "TODO: implement this")) (at level 0).
 
 Open Scope gensym_monad_scope.
+Open Scope gensym_monad_scope_2.
 
 Inductive DominatorSet : Type
   :=
@@ -73,16 +74,19 @@ Fixpoint postorder_traversal_gen_aux
   match fuel with
   | 0 => error(Errors.msg "Out of fuel")
   | S fuel' =>
-    (* add to visitor set*)
-    let new_seen_nodes := BBSet.add cur_node seen_nodes in
-
-    (* obtain children *)
-    do (sn, pot) <-
-      recurse_on_children fuel' cfg new_seen_nodes pot cur_node;
-
-    (* add to postorder traversal *)
-    let final_postorder := cons cur_node pot in
-    ret (sn, final_postorder)
+    if BBSet.mem cur_node seen_nodes
+    then ret (seen_nodes, pot)
+    else
+      (* add to visitor set*)
+      let new_seen_nodes := BBSet.add cur_node seen_nodes in
+
+      (* obtain children *)
+      do (sn, pot) <-
+        recurse_on_children fuel' cfg new_seen_nodes pot cur_node;
+
+      (* add to postorder traversal *)
+      let final_postorder := cons cur_node pot in
+      ret (sn, final_postorder)
   end
 with
   recurse_on_children
@@ -150,16 +154,170 @@ Definition reverse_postorder_traversal_gen
   (cfg: ClightCFG) : mon (list bb_uid * BBMap.t positive)
   :=
   let num_nodes := BBSet.cardinal cfg.(node_set) in
+  (* The DFS helper consumes fuel at multiple recursive layers per visited node
+     (node visit + edge traversal + switch-list traversal). A quadratic budget
+     avoids spurious "Out of fuel" failures on normal CFGs. *)
+  let fuel := S (Nat.mul (S num_nodes) (S num_nodes)) in
   let seen_nodes := BBSet.empty in
   let pot := nil in
   let cur_node := cfg.(entry) in
 
-  do (seen_set, pot) <- postorder_traversal_gen_aux num_nodes cfg seen_nodes pot cur_node;
+  do (seen_set, pot) <- postorder_traversal_gen_aux fuel cfg seen_nodes pot cur_node;
 
   let rpot := rev pot in
 
   ret (rpot, gen_bb_map rpot (BBMap.empty positive) 1).
 
+Definition edge_successors (edge: BBEdge) : list bb_uid :=
+  match edge with
+  | direct nextbb => [nextbb]
+  | conditional _ b_true b_false => [b_true; b_false]
+  | switch _ sl =>
+      let fix sl_successors (sl': switch_list) : list bb_uid :=
+        match sl' with
+        | SLnil b => [b]
+        | SLcons _ b sl'' => b :: sl_successors sl''
+        end
+      in sl_successors sl
+  | terminate _ => []
+  | stub => []
+  end.
+
+Definition add_predecessor
+  (pred succ: bb_uid)
+  (pred_map: BBMap.t BBSet.t)
+  : BBMap.t BBSet.t
+  :=
+  let preds :=
+    match BBMap.find succ pred_map with
+    | Some s => s
+    | None => BBSet.empty
+    end
+  in
+  BBMap.add succ (BBSet.add pred preds) pred_map.
+
+Fixpoint add_predecessors_for_successors
+  (pred: bb_uid)
+  (succs: list bb_uid)
+  (pred_map: BBMap.t BBSet.t)
+  : BBMap.t BBSet.t
+  :=
+  match succs with
+  | [] => pred_map
+  | succ :: rest =>
+      add_predecessors_for_successors pred rest (add_predecessor pred succ pred_map)
+  end.
+
+Definition compute_predecessor_map (cfg: ClightCFG) : BBMap.t BBSet.t :=
+  fold_left
+    (fun (pred_map: BBMap.t BBSet.t) (source: bb_uid) =>
+      match BBMap.find source cfg.(ClightCFG.map) with
+      | Some (bb _ edge) =>
+          add_predecessors_for_successors source (edge_successors edge) pred_map
+      | None => pred_map
+      end)
+    (BBSet.elements cfg.(ClightCFG.node_set))
+    (BBMap.empty BBSet.t).
+
+Definition get_rpo_num (rpo_map: BBMap.t positive) (n: bb_uid) : option positive :=
+  BBMap.find n rpo_map.
+
+Definition is_backward_edge
+  (rpo_map: BBMap.t positive)
+  (source target: bb_uid)
+  : bool
+  :=
+  match get_rpo_num rpo_map source, get_rpo_num rpo_map target with
+  | Some src_num, Some tgt_num => Pos.leb tgt_num src_num
+  | _, _ => false
+  end.
+
+Fixpoint count_forward_predecessors
+  (rpo_map: BBMap.t positive)
+  (node: bb_uid)
+  (preds: list bb_uid)
+  : nat
+  :=
+  match preds with
+  | [] => O
+  | pred :: rest =>
+      let rest_count := count_forward_predecessors rpo_map node rest in
+      if is_backward_edge rpo_map pred node
+      then rest_count
+      else S rest_count
+  end.
+
+Definition is_merge_node
+  (pred_map: BBMap.t BBSet.t)
+  (rpo_map: BBMap.t positive)
+  (node: bb_uid)
+  : bool
+  :=
+  match BBMap.find node pred_map with
+  | Some preds =>
+      let forward_count := count_forward_predecessors rpo_map node (BBSet.elements preds) in
+      Nat.leb 2 forward_count
+  | None => false
+  end.
+
+Definition compute_merge_nodes
+  (cfg: ClightCFG)
+  (pred_map: BBMap.t BBSet.t)
+  (rpo_map: BBMap.t positive)
+  : BBSet.t
+  :=
+  fold_left
+    (fun (merges: BBSet.t) (node: bb_uid) =>
+      if is_merge_node pred_map rpo_map node
+      then BBSet.add node merges
+      else merges)
+    (BBSet.elements cfg.(ClightCFG.node_set))
+    BBSet.empty.
+
+Definition compute_loop_headers
+  (cfg: ClightCFG)
+  (rpo_map: BBMap.t positive)
+  : BBSet.t
+  :=
+  fold_left
+    (fun (headers: BBSet.t) (source: bb_uid) =>
+      match BBMap.find source cfg.(ClightCFG.map) with
+      | Some (bb _ edge) =>
+          fold_left
+            (fun (acc: BBSet.t) (target: bb_uid) =>
+              if is_backward_edge rpo_map source target
+              then BBSet.add target acc
+              else acc)
+            (edge_successors edge)
+            headers
+      | None => headers
+      end)
+    (BBSet.elements cfg.(ClightCFG.node_set))
+    BBSet.empty.
+
+Record StructuredMetadata : Type :=
+  mkStructuredMetadata {
+    sm_rpo_list: list bb_uid;
+    sm_rpo_map: BBMap.t positive;
+    sm_predecessors: BBMap.t BBSet.t;
+    sm_merge_nodes: BBSet.t;
+    sm_loop_headers: BBSet.t;
+  }.
+
+Definition build_structured_metadata (cfg: ClightCFG) : mon StructuredMetadata :=
+  gdo (rpo_list, rpo_map) <- reverse_postorder_traversal_gen cfg;
+  let predecessors := compute_predecessor_map cfg in
+  let merge_nodes := compute_merge_nodes cfg predecessors rpo_map in
+  let loop_headers := compute_loop_headers cfg rpo_map in
+  ret
+    {|
+      sm_rpo_list := rpo_list;
+      sm_rpo_map := rpo_map;
+      sm_predecessors := predecessors;
+      sm_merge_nodes := merge_nodes;
+      sm_loop_headers := loop_headers;
+    |}.
+
 
 (* NOTE: to translate clight expression: Clight.transl_syntax_expr *)
 
@@ -318,6 +476,95 @@ Definition empty_context : TranslContext :=
     fallthrough := None;
   |}.
 
+Definition inside_context
+  (frame: ContainingSyntax)
+  (context: TranslContext)
+  : TranslContext :=
+  {|
+    enclosing := frame :: context.(enclosing);
+    fallthrough := context.(fallthrough);
+  |}.
+
+Definition with_fallthrough
+  (target: bb_uid)
+  (context: TranslContext)
+  : TranslContext :=
+  {|
+    enclosing := context.(enclosing);
+    fallthrough := Some target;
+  |}.
+
+Fixpoint label_in_context_frames
+  (target: bb_uid)
+  (frames: list ContainingSyntax)
+  : bool
+  :=
+  match frames with
+  | [] => false
+  | IfThenElse :: rest => label_in_context_frames target rest
+  | LoopHeadedBy l :: rest =>
+      if Pos.eqb l target then true else label_in_context_frames target rest
+  | BlockFollowedBy l :: rest =>
+      if Pos.eqb l target then true else label_in_context_frames target rest
+  end.
+
+Definition label_in_context (target: bb_uid) (context: TranslContext) : bool :=
+  label_in_context_frames target context.(enclosing).
+
+Definition is_fallthrough_target (target: bb_uid) (context: TranslContext) : bool :=
+  match context.(fallthrough) with
+  | Some lbl => Pos.eqb lbl target
+  | None => false
+  end.
+
+(* Keep control labels and block labels disjoint in emitted Rust:
+   control labels are even, block labels are odd. *)
+Definition encode_control_label (uid: positive) : Z :=
+  Z.mul (Z.pos uid) 2.
+
+Definition encode_block_label (uid: bb_uid) : Z :=
+  Z.succ (encode_control_label uid).
+
+(* Helper used by upcoming structured translation:
+   - backward edge => continue to loop header
+   - forward edge to merge label => break to block
+   - otherwise inline by caller (None) *)
+Definition structured_jump_for_branch
+  (meta: StructuredMetadata)
+  (source target: bb_uid)
+  (context: TranslContext)
+  : option rstatement
+  :=
+  if is_fallthrough_target target context
+  then Some S_skip
+  else if is_backward_edge meta.(sm_rpo_map) source target
+       then Some (S_continue (Some (encode_block_label target)))
+       else if BBSet.mem target meta.(sm_merge_nodes)
+            then Some (S_break (Some (encode_block_label target)))
+            else None.
+
+Definition mk_loop_for_header (header: bb_uid) (body: rstatement) : rstatement :=
+  S_loop (Some (encode_block_label header)) body S_skip.
+
+Definition mk_block_followed_by (label: bb_uid) (body: rstatement) : rstatement :=
+  S_block (Some (encode_block_label label)) body.
+
+Definition choose_structured_branch
+  (meta: StructuredMetadata)
+  (source target: bb_uid)
+  (context: TranslContext)
+  (inline_target: option rstatement)
+  : rstatement
+  :=
+  match structured_jump_for_branch meta source target context with
+  | Some jump_stmt => jump_stmt
+  | None =>
+      match inline_target with
+      | Some stmt => stmt
+      | None => S_skip
+      end
+  end.
+
 (* -------------------- END haskell attempt. Will return to this later -----*)
 
 Local Open Scope gensym_monad_scope_2.
@@ -338,9 +585,170 @@ Definition gen_goto_next_bb
   (cf_lbl_ident: bb_uid) (goto_id: bb_uid) : rstatement :=
   let set_stmt := S_set cf_lbl_ident (bb_to_rexpr goto_id) in
   (* NOTE probably unnecessary in most cases. I could remove it. *)
-  let continue_stmt := S_continue None in
+  let continue_stmt := S_continue (Some (encode_control_label cf_lbl_ident)) in
   S_sequence set_stmt continue_stmt.
 
+Fixpoint bb_uid_in_list (target: bb_uid) (labels: list bb_uid) : bool :=
+  match labels with
+  | [] => false
+  | lbl :: rest => if Pos.eqb lbl target then true else bb_uid_in_list target rest
+  end.
+
+Fixpoint next_in_order (target: bb_uid) (ordered_nodes: list bb_uid) : option bb_uid :=
+  match ordered_nodes with
+  | [] => None
+  | [n] => None
+  | n1 :: (n2 :: rest as tl) =>
+      if Pos.eqb n1 target
+      then Some n2
+      else next_in_order target tl
+  end.
+
+Definition doBranch
+  (cf_lbl_ident source target: bb_uid)
+  (next_node: option bb_uid)
+  (context_labels: list bb_uid)
+  : rstatement :=
+  if
+    match next_node with
+    | Some nextbb => Pos.eqb nextbb target
+    | None => false
+    end
+  then S_skip
+  else if bb_uid_in_list target context_labels
+       then S_break (Some (encode_block_label target))
+       else gen_goto_next_bb cf_lbl_ident target.
+
+Fixpoint selector_cases (entry_uid: bb_uid) (nodes: list bb_uid) : labeled_rstatements :=
+  match nodes with
+  | [] => LSnil S_skip
+  | node :: rest =>
+      let stmt :=
+        if Pos.eqb node entry_uid
+        then S_skip
+        else S_break (Some (encode_block_label node))
+      in
+      LScons (Some (Z.pos node)) stmt (selector_cases entry_uid rest)
+  end.
+
+Fixpoint transl_cfg_to_rustlight_sl_structured
+  (branch_for: bb_uid -> rstatement)
+  (maybe_dflt: option rstatement)
+  (sl: switch_list)
+  : labeled_rstatements :=
+  match sl with
+  | SLnil s' =>
+      LSnil
+        (match maybe_dflt with
+         | Some dflt_stmt => dflt_stmt
+         | None => branch_for s'
+         end)
+  | SLcons maybe_int b sl' =>
+      match maybe_int with
+      | None =>
+          transl_cfg_to_rustlight_sl_structured branch_for (Some (branch_for b)) sl'
+      | Some i =>
+          LScons
+            (Some i)
+            (branch_for b)
+            (transl_cfg_to_rustlight_sl_structured branch_for maybe_dflt sl')
+      end
+  end.
+
+Definition transl_cfg_node_structured
+  (cfg: ClightCFG)
+  (cf_lbl_ident: bb_uid)
+  (cur_node: bb_uid)
+  (next_node: option bb_uid)
+  (context_labels: list bb_uid)
+  (r_ty: type)
+  : SimplExpr.mon rstatement :=
+  gdo block <- get_bb cfg cur_node;
+  match block with
+  | bb insts edge =>
+      gdo transl_insts <- transl_clightcfg_instructions insts;
+      let branch_for := fun target => doBranch cf_lbl_ident cur_node target next_node context_labels in
+      gdo transl_edge <-
+      match edge with
+      | direct target =>
+          ret (branch_for target)
+      | conditional cexp b_true b_false =>
+          gdo r_cexp <- transl_syntax_expr cexp;
+          ret (S_if_then_else r_cexp (branch_for b_true) (branch_for b_false))
+      | terminate maybe_exp =>
+          match maybe_exp with
+          | Some exp =>
+              gdo e <- transl_syntax_expr exp;
+              ret (S_return (Some (e, r_typeof e)))
+          | None =>
+              ret
+                (match r_ty with
+                 | Tvoid => S_return None
+                 | _ => S_skip
+                 end)
+          end
+      | switch cexp sl =>
+          gdo tr_exp <- transl_syntax_expr cexp;
+          let lrs := transl_cfg_to_rustlight_sl_structured branch_for None sl in
+          ret (S_match_int tr_exp lrs)
+      | stub => SimplExpr.error (Errors.msg "stub edge encountered")
+      end;
+      ret (S_sequence transl_insts transl_edge)
+  end.
+
+Fixpoint nodeWithin
+  (cfg: ClightCFG)
+  (cf_lbl_ident: bb_uid)
+  (r_ty: type)
+  (ordered_nodes: list bb_uid)
+  (entry_uid: bb_uid)
+  (follows_desc: list bb_uid)
+  (context_labels: list bb_uid)
+  : SimplExpr.mon rstatement :=
+  match follows_desc with
+  | [] =>
+      gdo base_stmt <-
+        transl_cfg_node_structured
+          cfg
+          cf_lbl_ident
+          entry_uid
+          (next_in_order entry_uid ordered_nodes)
+          context_labels
+          r_ty;
+      let selector :=
+        S_match_int
+          (Etempvar cf_lbl_ident bbuid_ty)
+          (selector_cases entry_uid ordered_nodes)
+      in
+      ret (S_sequence selector base_stmt)
+  | y_n :: ys =>
+      gdo inner <- nodeWithin cfg cf_lbl_ident r_ty ordered_nodes entry_uid ys (y_n :: context_labels);
+      gdo y_stmt <-
+        transl_cfg_node_structured
+          cfg
+          cf_lbl_ident
+          y_n
+          (next_in_order y_n ordered_nodes)
+          context_labels
+          r_ty;
+      ret (S_sequence (S_block (Some (encode_block_label y_n)) inner) y_stmt)
+  end.
+
+Definition doTree
+  (cfg: ClightCFG)
+  (cf_lbl_ident: bb_uid)
+  (r_ty: type)
+  (ordered_nodes: list bb_uid)
+  : SimplExpr.mon rstatement :=
+  let entry_uid := cfg.(entry) in
+  let rest_nodes :=
+    filter
+      (fun n => negb (Pos.eqb n entry_uid))
+      ordered_nodes
+  in
+  let follows_desc := rev rest_nodes in
+  nodeWithin cfg cf_lbl_ident r_ty (entry_uid :: rest_nodes) entry_uid follows_desc [].
+
 Fixpoint transl_cfg_to_rustlight_sl
   (cfg: ClightCFG) (cf_lbl_ident: bb_uid) (maybe_dflt: option rstatement) (sl: switch_list)
   : SimplExpr.mon labeled_rstatements :=
@@ -425,7 +833,7 @@ Fixpoint transl_cfg_nodes_to_rustlight (cfg: ClightCFG) (cf_lbl_ident: bb_uid) (
       ret (LSnil S_skip)
   end.
 
-Definition transl_cfg_to_rustlight (cfg: ClightCFG) (r_ty: type) : SimplExpr.mon rstatement :=
+Definition transl_cfg_to_rustlight_dispatcher (cfg: ClightCFG) (r_ty: type) : SimplExpr.mon rstatement :=
   gdo cf_lbl_ident <- SimplExpr.gensym bbuid_ty;
   let entry_uid := cfg.(entry) in
   let s_stmt := S_set cf_lbl_ident (bb_to_rexpr entry_uid) in
@@ -435,10 +843,24 @@ Definition transl_cfg_to_rustlight (cfg: ClightCFG) (r_ty: type) : SimplExpr.mon
   (*transl_cfg_to_rustlight_aux cfg cfg.(entry) entry_uid.*)
   gdo r_list <- transl_cfg_nodes_to_rustlight cfg cf_lbl_ident (BBSet.elements nodes) r_ty;
   let m_stmt := S_match_int (Etempvar cf_lbl_ident bbuid_ty) r_list in
-  let l_stmt := S_loop None m_stmt S_skip in
+  let l_stmt := S_loop (Some (encode_control_label cf_lbl_ident)) m_stmt S_skip in
   let seq_stmt := S_sequence s_stmt l_stmt in
   ret seq_stmt.
 
+Definition transl_cfg_to_rustlight (cfg: ClightCFG) (r_ty: type) : SimplExpr.mon rstatement :=
+  gdo meta <- build_structured_metadata cfg;
+  gdo cf_lbl_ident <- SimplExpr.gensym bbuid_ty;
+  match meta.(sm_rpo_list) with
+  | [] =>
+      transl_cfg_to_rustlight_dispatcher cfg r_ty
+  | _ =>
+      gdo tree_body <- doTree cfg cf_lbl_ident r_ty meta.(sm_rpo_list);
+      let s_stmt := S_set cf_lbl_ident (bb_to_rexpr cfg.(entry)) in
+      let loop_body := S_sequence tree_body (S_continue (Some (encode_control_label cf_lbl_ident))) in
+      let l_stmt := S_loop (Some (encode_control_label cf_lbl_ident)) loop_body S_skip in
+      ret (S_sequence s_stmt l_stmt)
+  end.
+
 Print calling_convention.
 Print r_calling_convention.
 
@@ -541,3 +963,20 @@ Definition transl_program (cfg: clightcfg_program) : res (r_program)
       Ctypes.prog_comp_env_eq := cfg.(prog_comp_env_eq);
     |} in
   OK(r_prog).
+
+(* ============================================================================= *)
+(* CNS IMPLEMENTATION - Controlled Node Splitting Algorithm                     *)
+(* Implementation of algorithm from Janssen & Corporaal (1997)                  *)
+(* "Making Graphs Reducible with Controlled Node Splitting"                    *)
+(* ============================================================================= *)
+
+(* NOTE: The basic graph analysis functions (get_successors, compute_predecessors, *)
+(* compute_dominators, find_sccs) are now in ClightCFG.v and can be imported.     *)
+
+(* ============================================================================= *)
+(* Phase 1 Complete - Basic graph analysis available from ClightCFG.v:          *)
+(*   - get_edge_successors, get_successors                                       *)
+(*   - compute_predecessors, get_predecessors                                    *)
+(*   - compute_dominators, immediate_dominator, dominates                        *)
+(*   - TarjanState, find_sccs, nodes_in_same_loop                               *)
+(* ============================================================================= *)
diff --git a/driver/Driver.ml b/driver/Driver.ml
index e70ffe636..f40394b70 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -100,14 +100,42 @@ let object_filename sourcename =
 let extract_globals sourcename =
   ensure_inputfile_exists sourcename;
   (* printf "\nPTYPES: %s\n" sourcename; *)
-  let preproname = tmp_file ".i" in
-  let extraflags = find_flags sourcename in
-  preprocess sourcename preproname extraflags;
-  let csyntax = parse_c_file sourcename preproname in
+  let csyntax =
+    if Filename.check_suffix sourcename ".i" || Filename.check_suffix sourcename ".p" then
+      parse_c_file sourcename sourcename
+    else
+      let preproname = tmp_file ".i" in
+      let extraflags = find_flags sourcename in
+      preprocess sourcename preproname extraflags;
+      parse_c_file sourcename preproname
+  in
   Hashtbl.add !csyntax_mapping (remove_c_extension sourcename) csyntax;
 
   Compiler.get_exports csyntax
 
+let run_rust_pipeline_with_cns (csyntax : Csyntax.program) :
+    RustLight.r_program Errors.res =
+  match SimplExpr.transl_program csyntax with
+  | Errors.Error msg -> Errors.Error msg
+  | Errors.OK clight ->
+      match ClightCFG.transl_program clight with
+      | Errors.Error msg -> Errors.Error msg
+      | Errors.OK cfg ->
+          match ClightCFGCNS.transl_program cfg with
+          | Errors.Error msg -> Errors.Error msg
+          | Errors.OK cfg' ->
+              match RustLightgen.transl_program cfg' with
+              | Errors.Error msg -> Errors.Error msg
+              | Errors.OK r_prog ->
+                  match RustLightInsertTypeCasts.transl_program r_prog with
+                  | Errors.Error msg -> Errors.Error msg
+                  | Errors.OK casted_prog ->
+                      match RustLightSplitExpr.transl_program casted_prog with
+                      | Errors.Error msg -> Errors.Error msg
+                      | Errors.OK split_prog ->
+                          let _ = PrintRustLight.print_if split_prog in
+                          Errors.OK split_prog
+
 (* From CompCert C AST to asm *)
 
 let compile_c_file sourcename ifile ofile =
@@ -131,7 +159,11 @@ let compile_c_file sourcename ifile ofile =
   let module_name_string = remove_c_extension sourcename in
   let module_name = module_name_string |> String.to_seq |> List.of_seq in
 
-  let csyntax = Hashtbl.find !csyntax_mapping module_name_string in
+  let csyntax =
+    match Hashtbl.find_opt !csyntax_mapping module_name_string with
+    | Some cached -> cached
+    | None -> parse_c_file sourcename ifile
+  in
 
   let project_name = !option_drustlight_name |> String.to_seq |> List.of_seq in
 
@@ -139,21 +171,19 @@ let compile_c_file sourcename ifile ofile =
   PrintRustLight.proj_name := Some !option_drustlight_name;
   PrintRustLight.mod_name := Some module_name_string;
 
-  (match
-     Compiler.print_r_program_from_cfg !sym_mapping !composite_mapping
-       module_name project_name csyntax
-   with
-  | Errors.OK _rprog -> printf "translated!"
-  | Errors.Error msg ->
-      fatal_error no_loc "error! %s" (C2C.string_of_errmsg msg));
+  if !option_drustlight then (
+    match run_rust_pipeline_with_cns csyntax with
+    | Errors.OK _rprog -> printf "translated!"
+    | Errors.Error msg ->
+        fatal_error no_loc "error! %s" (C2C.string_of_errmsg msg);
 
-  PrintRustLight.destination := Some "inserted_main_module.rs";
+    PrintRustLight.destination := Some "inserted_main_module.rs";
 
-  (if !main_mod_name = module_name_string then
-     match Compiler.print_r_main_from_cfg csyntax with
-     | Errors.OK _ -> printf "created generated main function and module"
-     | Errors.Error msg ->
-         fatal_error no_loc "error! %s" (C2C.string_of_errmsg msg));
+    if !main_mod_name = module_name_string then
+      match Compiler.print_r_main_from_cfg csyntax with
+      | Errors.OK _ -> printf "created generated main function and module"
+      | Errors.Error msg ->
+          fatal_error no_loc "error! %s" (C2C.string_of_errmsg msg));
 
   (* TODO this goes in the garbage*)
   (* Convert to Asm *)
@@ -625,12 +655,14 @@ let cmdline_actions =
       ( Suffix ".i",
         Self
           (fun s ->
+            add_to_list s;
             push_action process_i_file s;
             incr num_source_files;
             incr num_input_files) );
       ( Suffix ".p",
         Self
           (fun s ->
+            add_to_list s;
             push_action process_i_file s;
             incr num_source_files;
             incr num_input_files) );
diff --git a/extraction/compcert/dune b/extraction/compcert/dune
index 76d982019..cc91d883a 100644
--- a/extraction/compcert/dune
+++ b/extraction/compcert/dune
@@ -1,5 +1,19 @@
 (include ../shared.dune)
 
+(ocamllex Lexer Readconfig Responsefile Tokenize)
+
+(rule
+ (deps pre_parser.mly pre_parser_messages.ml)
+ (targets pre_parser.ml pre_parser.mli)
+ (action
+  (run menhir --table -v --no-stdlib -la 1 --explain pre_parser.mly --base pre_parser)))
+
+(rule
+ (targets pre_parser_messages.ml)
+ (action
+  (with-stdout-to %{targets}
+   (run menhir --table pre_parser.mly -v --no-stdlib -la 1 -v -la 2 --compile-errors %{dep:handcrafted.messages}))))
+
 ; copy OCaml files from source files - only those not shared with clightgen already
 ; when trying to move extraction file into platform directory
 (copy_files %{project_root}/platform/backend/*.{ml,mli})
diff --git a/flake.nix b/flake.nix
index c644fc1d1..e703f4f35 100644
--- a/flake.nix
+++ b/flake.nix
@@ -55,6 +55,7 @@
           ];
         };
         baseBuildInputs = with pkgs; [
+          gcc
           llvmPackages_latest.clang-tools
           llvmPackages_latest.clang
           llvmPackages_latest.openmp
diff --git a/platform/dune b/platform/dune
index 5d6cbdf4a..774fdb7b5 100644
--- a/platform/dune
+++ b/platform/dune
@@ -7,55 +7,174 @@
 ; Copy all files from currently selected architecture to "TargetPlatformCopy" directory.
 ; Can't copy processed .vp files from platform directories due to dependency cycle -> generate later in preprocess.dune.
 ; a.d. TODO are these aliases used at all?
-(subdir TargetPlatformCopy
- (copy_files (alias target_platform) (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} ppc)) (files %{project_root}/powerpc/*)))
 
+(subdir
+ TargetPlatformCopy
+ (copy_files
+  (alias target_platform)
+  (only_sources)
+  (enabled_if
+   (= %{env:TARGET_PLATFORM=ppc} ppc))
+  (files %{project_root}/powerpc/*.{v,vp,ml,mli})))
 
-(subdir TargetPlatformCopy
- (copy_files (alias target_platform) (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} x86_32)) (files %{project_root}/x86/*.{v,vp,ml,mli})))
-(subdir TargetPlatformCopy
- (copy_files (alias target_platform) (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} x86_32)) (files %{project_root}/x86_32/*.{v,vp,ml,mli})))
+(subdir
+ TargetPlatformCopy
+ (copy_files
+  (alias target_platform)
+  (only_sources)
+  (enabled_if
+   (= %{env:TARGET_PLATFORM=ppc} x86_32))
+  (files %{project_root}/x86/*.{v,vp,ml,mli})))
 
-(subdir TargetPlatformCopy
- (copy_files (alias target_platform) (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} x86_64)) (files %{project_root}/x86/*.{v,vp,ml,mli})))
-(subdir TargetPlatformCopy
- (copy_files (alias target_platform) (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} x86_64)) (files %{project_root}/x86_64/*.{v,vp,ml,mli})))
+(subdir
+ TargetPlatformCopy
+ (copy_files
+  (alias target_platform)
+  (only_sources)
+  (enabled_if
+   (= %{env:TARGET_PLATFORM=ppc} x86_32))
+  (files %{project_root}/x86_32/*.{v,vp,ml,mli})))
 
+(subdir
+ TargetPlatformCopy
+ (copy_files
+  (alias target_platform)
+  (only_sources)
+  (enabled_if
+   (= %{env:TARGET_PLATFORM=ppc} x86_64))
+  (files %{project_root}/x86/*.{v,vp,ml,mli})))
 
-(subdir TargetPlatformCopy
- (copy_files (alias target_platform) (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} riscV)) (files %{project_root}/riscV/*)))
+(subdir
+ TargetPlatformCopy
+ (copy_files
+  (alias target_platform)
+  (only_sources)
+  (enabled_if
+   (= %{env:TARGET_PLATFORM=ppc} x86_64))
+  (files %{project_root}/x86_64/*.{v,vp,ml,mli})))
 
+(subdir
+ TargetPlatformCopy
+ (copy_files
+  (alias target_platform)
+  (only_sources)
+  (enabled_if
+   (= %{env:TARGET_PLATFORM=ppc} riscV))
+  (files %{project_root}/riscV/*.{v,vp,ml,mli})))
 
-(subdir TargetPlatformCopy
- (copy_files (alias target_platform) (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} arm)) (files %{project_root}/arm/*)))
+(subdir
+ TargetPlatformCopy
+ (copy_files
+  (alias target_platform)
+  (only_sources)
+  (enabled_if
+   (= %{env:TARGET_PLATFORM=ppc} arm))
+  (files %{project_root}/arm/*.{v,vp,ml,mli})))
 
-(subdir TargetPlatformCopy
- (copy_files (alias target_platform) (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} aarch64)) (files %{project_root}/aarch64/*)))
+(subdir
+ TargetPlatformCopy
+ (copy_files
+  (alias target_platform)
+  (only_sources)
+  (enabled_if
+   (= %{env:TARGET_PLATFORM=ppc} aarch64))
+  (files %{project_root}/aarch64/*.{v,vp,ml,mli})))
 
 ; copy files from all other relevant source directories
-(subdir backend (copy_files %{project_root}/backend/*))
-(subdir cfrontend (copy_files %{project_root}/cfrontend/*))
-(subdir common (copy_files %{project_root}/common/*))
-(subdir cparser (copy_files %{project_root}/cparser/*))
-(subdir debug (copy_files %{project_root}/debug/*))
-(subdir driver (copy_files %{project_root}/driver/*))
-(subdir export (copy_files %{project_root}/export/*))
-(subdir lib (copy_files %{project_root}/lib/*))
 
+(subdir
+ backend
+ (copy_files
+  (only_sources)
+  (files %{project_root}/backend/*.{v,vp,ml,mli})))
+
+(subdir
+ backend
+ (rule
+  (action
+   (with-stdout-to SelectDiv.v
+    (run ndfun %{dep:SelectDiv.vp})))))
+
+(subdir
+ backend
+ (rule
+  (action
+   (with-stdout-to SplitLong.v
+    (run ndfun %{dep:SplitLong.vp})))))
+
+(subdir
+ cfrontend
+ (copy_files
+  (only_sources)
+  (files %{project_root}/cfrontend/*.{v,vp,ml,mli,mll,mly})))
+
+(subdir
+ common
+ (copy_files
+  (only_sources)
+  (files %{project_root}/common/*.{v,ml,mli})))
+
+(subdir
+ cparser
+ (copy_files
+  (only_sources)
+  (files %{project_root}/cparser/*.{v,vy,ml,mli,mll,mly,messages})))
+
+(subdir
+ cparser
+ (rule
+  (action
+   (with-stdout-to Parser.v
+    (run menhir --coq --coq-no-version-check %{dep:Parser.vy})))))
+
+(subdir
+ debug
+ (copy_files
+  (only_sources)
+  (files %{project_root}/debug/*.{ml,mli})))
+
+(subdir
+ driver
+ (copy_files
+  (only_sources)
+  (files %{project_root}/driver/*.{v,ml,mli,html})))
+
+(subdir
+ export
+ (copy_files
+  (only_sources)
+  (files %{project_root}/export/*.{v,ml,mli,md})))
+
+(subdir
+ lib
+ (copy_files
+  (only_sources)
+  (files %{project_root}/lib/*.{v,ml,mli,mll})))
 
 ; Run preprocessing directives on .vp files
+
 (include preprocess.dune)
 
 ;Compile theory from all Coq files, excluding extraction code that is run directly during compilation.
+
 (coq.theory
  (name compcert)
  (theories Flocq MenhirLib)
  ; temp flag
  (flags
-  -w -unused-pattern-matching-variable
-  -w -deprecated-since-8.19
-  -w -deprecated-since-8.20)
- (modules :standard \ common.Subtyping TargetPlatformCopy.extractionMachdep TargetPlatformCopy.extractionMachdepClight))
+  -w
+  -unused-pattern-matching-variable
+  -w
+  -deprecated-since-8.19
+  -w
+  -deprecated-since-8.20)
+ (modules
+  :standard
+  \
+  common.Subtyping
+  TargetPlatformCopy.extractionMachdep
+  TargetPlatformCopy.extractionMachdepClight))
 
 ; Our Coq files are in subdirectories of platform/ so we need this for dune to compile them too.
+
 (include_subdirs qualified)