From 83537045c0866cd5586136e522d93256648c0bae Mon Sep 17 00:00:00 2001 From: ByronLi8565 Date: Fri, 31 Oct 2025 04:13:57 -0400 Subject: [PATCH 1/7] init cns --- cfrontend/ClightCFG.v | 333 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 333 insertions(+) diff --git a/cfrontend/ClightCFG.v b/cfrontend/ClightCFG.v index 1b8800820..63e24e79c 100644 --- a/cfrontend/ClightCFG.v +++ b/cfrontend/ClightCFG.v @@ -55,6 +55,339 @@ Module LBLMap := Coq.FSets.FMapList.Make(Positive_as_OT). (* set of bb_uids *) Module BBSet <: FSets.FSetInterface.S := FSets.FSetPositive.PositiveSet. +(* Helper function to get successors of a node from its edge *) +Definition get_edge_successors (edge: BBEdge) : list bb_uid := + match edge with + | direct uid => [uid] + | conditional _ uid1 uid2 => [uid1; uid2] + | switch _ sl => + let fix get_switch_targets (s: switch_list) : list bb_uid := + match s with + | SLnil uid => [uid] + | SLcons _ uid rest => uid :: get_switch_targets rest + end + in get_switch_targets sl + | terminate _ => [] + | stub => [] + end. + +(* Get all successors of a basic block *) +Definition get_successors (cfg: ClightCFG) (uid: bb_uid) : list bb_uid := + match BBMap.find uid (map cfg) with + | None => [] + | Some (bb _ edge) => get_edge_successors edge + end. + +(* Build predecessor map: for each node, list of nodes that point to it *) +Definition compute_predecessors (cfg: ClightCFG) : BBMap.t (list bb_uid) := + BBSet.fold + (fun node acc => + let succs := get_successors cfg node in + List.fold_left + (fun acc' succ => + let existing := match BBMap.find succ acc' with + | None => [] + | Some preds => preds + end in + BBMap.add succ (node :: existing) acc') + succs + acc) + (node_set cfg) + (BBMap.empty (list bb_uid)). + +(* Get predecessors of a node *) +Definition get_predecessors (pred_map: BBMap.t (list bb_uid)) (uid: bb_uid) : list bb_uid := + match BBMap.find uid pred_map with + | None => [] + | Some preds => preds + end. + +(* Check if a node is in a set *) +Definition uid_in_set (uid: bb_uid) (s: BBSet.t) : bool := + BBSet.mem uid s. + +(* Compute dominator sets using iterative dataflow *) +(* Dom(n) = {n} ∪ (∩ Dom(p) for all predecessors p of n) *) +(* For entry node: Dom(entry) = {entry} *) +Fixpoint compute_dominators_fixpoint + (cfg: ClightCFG) + (pred_map: BBMap.t (list bb_uid)) + (dom_map: BBMap.t BBSet.t) (* Current dominator sets *) + (fuel: nat) + : BBMap.t BBSet.t := + match fuel with + | O => dom_map (* Ran out of fuel, return current state *) + | S fuel' => + let (new_dom_map, changed) := + BBSet.fold + (fun node (acc_pair: BBMap.t BBSet.t * bool) => + let (acc, has_changed) := acc_pair in + if Pos.eqb node (entry cfg) then + (* Entry node dominates only itself *) + (acc, has_changed) + else + let preds := get_predecessors pred_map node in + let new_dom := + match preds with + | [] => BBSet.singleton node (* No predecessors, only self *) + | p :: rest => + (* Start with dominators of first predecessor *) + let init_dom := match BBMap.find p acc with + | None => BBSet.empty + | Some d => d + end in + (* Intersect with dominators of remaining predecessors *) + let dom_inter := List.fold_left + (fun d_acc pred => + match BBMap.find pred acc with + | None => BBSet.empty + | Some pred_dom => BBSet.inter d_acc pred_dom + end) + rest + init_dom in + (* Add node itself *) + BBSet.add node dom_inter + end in + let old_dom := match BBMap.find node acc with + | None => BBSet.empty + | Some d => d + end in + (* Check if changed *) + if BBSet.equal new_dom old_dom then + (acc, has_changed) + else + (BBMap.add node new_dom acc, true)) + (node_set cfg) + (dom_map, false) in + if changed then + compute_dominators_fixpoint cfg pred_map new_dom_map fuel' + else + new_dom_map + end. + +(* Initialize dominator map: entry dominates only itself, others dominate all *) +Definition init_dominator_map (cfg: ClightCFG) : BBMap.t BBSet.t := + let all_nodes := node_set cfg in + BBSet.fold + (fun node acc => + if Pos.eqb node (entry cfg) then + BBMap.add node (BBSet.singleton node) acc + else + BBMap.add node all_nodes acc) + all_nodes + (BBMap.empty BBSet.t). + +(* Main entry point for computing dominators *) +Definition compute_dominators (cfg: ClightCFG) : BBMap.t BBSet.t := + let pred_map := compute_predecessors cfg in + let init_dom := init_dominator_map cfg in + compute_dominators_fixpoint cfg pred_map init_dom 100. + +(* Get immediate dominator of a node *) +(* ID(n) = the dominator of n that is dominated by all other dominators of n *) +Definition immediate_dominator + (dom_map: BBMap.t BBSet.t) + (entry: bb_uid) + (n: bb_uid) + : option bb_uid := + match BBMap.find n dom_map with + | None => None + | Some doms => + (* Remove n itself from its dominators *) + let doms_without_n := BBSet.remove n doms in + (* Entry has no immediate dominator *) + if Pos.eqb n entry then None + else if BBSet.is_empty doms_without_n then None + else + (* Find the dominator that is dominated by no other dominator of n *) + (* This is the one closest to n in the dominator tree *) + let candidates := BBSet.elements doms_without_n in + let rec find_idom (cands: list bb_uid) : option bb_uid := + match cands with + | [] => None + | [single] => Some single + | c :: rest => + (* Check if c is dominated by any other dominator *) + let is_idom := List.forallb + (fun other => + if Pos.eqb c other then true + else + (* c is idom if other doesn't dominate c, or c dominates other *) + match BBMap.find c dom_map with + | None => true + | Some c_doms => negb (BBSet.mem other c_doms) + end) + rest in + if is_idom then Some c + else find_idom rest + end in + find_idom candidates + end. + +(* Check if node u dominates node v *) +Definition dominates (dom_map: BBMap.t BBSet.t) (u v: bb_uid) : bool := + match BBMap.find v dom_map with + | None => false + | Some doms => BBSet.mem u doms + end. + +(* ============================================================================= *) +(* SCC Detection - Tarjan's Algorithm (Phase 1.3) *) +(* ============================================================================= *) + +(* State for Tarjan's SCC algorithm *) +Record TarjanState : Type := mkTarjanState { + (* Index counter *) + t_index: nat; + (* Stack of nodes *) + t_stack: list bb_uid; + (* Nodes currently on stack *) + t_on_stack: BBSet.t; + (* Index of each node (when first visited) *) + t_indices: BBMap.t nat; + (* Lowlink value of each node *) + t_lowlinks: BBMap.t nat; + (* Discovered SCCs *) + t_sccs: list BBSet.t; +}. + +Definition init_tarjan_state : TarjanState := + mkTarjanState 0 [] BBSet.empty (BBMap.empty nat) (BBMap.empty nat) []. + +(* Helper: get index of node, returns None if not yet visited *) +Definition get_index (state: TarjanState) (n: bb_uid) : option nat := + BBMap.find n (t_indices state). + +(* Helper: get lowlink of node *) +Definition get_lowlink (state: TarjanState) (n: bb_uid) : option nat := + BBMap.find n (t_lowlinks state). + +(* Helper: set index and lowlink for node *) +Definition set_index_lowlink (state: TarjanState) (n: bb_uid) (idx: nat) : TarjanState := + mkTarjanState + (S idx) + (n :: t_stack state) + (BBSet.add n (t_on_stack state)) + (BBMap.add n idx (t_indices state)) + (BBMap.add n idx (t_lowlinks state)) + (t_sccs state). + +(* Helper: update lowlink *) +Definition update_lowlink (state: TarjanState) (n: bb_uid) (new_low: nat) : TarjanState := + mkTarjanState + (t_index state) + (t_stack state) + (t_on_stack state) + (t_indices state) + (BBMap.add n new_low (t_lowlinks state)) + (t_sccs state). + +(* Helper: pop SCC from stack *) +Fixpoint pop_scc_from_stack + (stack: list bb_uid) + (on_stack: BBSet.t) + (root: bb_uid) + (acc: BBSet.t) + : (BBSet.t * list bb_uid * BBSet.t) := + match stack with + | [] => (acc, [], on_stack) + | w :: rest => + let new_acc := BBSet.add w acc in + let new_on_stack := BBSet.remove w on_stack in + if Pos.eqb w root then + (new_acc, rest, new_on_stack) + else + pop_scc_from_stack rest new_on_stack root new_acc + end. + +(* Tarjan's strongconnect procedure *) +Fixpoint tarjan_strongconnect + (cfg: ClightCFG) + (v: bb_uid) + (state: TarjanState) + (fuel: nat) + : TarjanState := + match fuel with + | O => state + | S fuel' => + (* Set index and lowlink for v *) + let state1 := set_index_lowlink state v (t_index state) in + + (* Process all successors *) + let succs := get_successors cfg v in + let state2 := List.fold_left + (fun st w => + match get_index st w with + | None => + (* Successor w has not been visited; recurse *) + let st' := tarjan_strongconnect cfg w st fuel' in + (* Update v's lowlink *) + match get_lowlink st' v, get_lowlink st' w with + | Some v_low, Some w_low => + if Nat.ltb w_low v_low then + update_lowlink st' v w_low + else + st' + | _, _ => st' + end + | Some _ => + (* Successor w has been visited *) + if BBSet.mem w (t_on_stack st) then + (* w is on stack, part of current SCC *) + match get_lowlink st v, get_index st w with + | Some v_low, Some w_idx => + if Nat.ltb w_idx v_low then + update_lowlink st v w_idx + else + st + | _, _ => st + end + else + st + end) + succs + state1 in + + (* If v is a root node, pop the stack and create SCC *) + match get_lowlink state2 v, get_index state2 v with + | Some v_low, Some v_idx => + if Nat.eqb v_low v_idx then + (* v is root of SCC *) + let (scc, new_stack, new_on_stack) := + pop_scc_from_stack (t_stack state2) (t_on_stack state2) v BBSet.empty in + mkTarjanState + (t_index state2) + new_stack + new_on_stack + (t_indices state2) + (t_lowlinks state2) + (scc :: t_sccs state2) + else + state2 + | _, _ => state2 + end + end. + +(* Main SCC finder *) +Definition find_sccs (cfg: ClightCFG) : list BBSet.t := + let nodes := BBSet.elements (node_set cfg) in + let final_state := List.fold_left + (fun state v => + match get_index state v with + | None => tarjan_strongconnect cfg v state 100 + | Some _ => state + end) + nodes + init_tarjan_state in + t_sccs final_state. + +(* Check if two nodes are in the same SCC (loop) *) +Definition nodes_in_same_loop (sccs: list BBSet.t) (u v: bb_uid) : bool := + List.existsb + (fun scc => + andb (BBSet.mem u scc) (BBSet.mem v scc)) + sccs. + Inductive Instruction := From 127b596577f39e995a472db380597e102b239c50 Mon Sep 17 00:00:00 2001 From: ByronLi8565 Date: Fri, 31 Oct 2025 15:40:27 -0400 Subject: [PATCH 2/7] init cns --- cfrontend/ClightCFG.v | 335 --------------------------------------- cfrontend/RustLightgen.v | 17 ++ platform/dune | 138 ++++++++++++---- 3 files changed, 127 insertions(+), 363 deletions(-) diff --git a/cfrontend/ClightCFG.v b/cfrontend/ClightCFG.v index 63e24e79c..cb5db094d 100644 --- a/cfrontend/ClightCFG.v +++ b/cfrontend/ClightCFG.v @@ -55,341 +55,6 @@ Module LBLMap := Coq.FSets.FMapList.Make(Positive_as_OT). (* set of bb_uids *) Module BBSet <: FSets.FSetInterface.S := FSets.FSetPositive.PositiveSet. -(* Helper function to get successors of a node from its edge *) -Definition get_edge_successors (edge: BBEdge) : list bb_uid := - match edge with - | direct uid => [uid] - | conditional _ uid1 uid2 => [uid1; uid2] - | switch _ sl => - let fix get_switch_targets (s: switch_list) : list bb_uid := - match s with - | SLnil uid => [uid] - | SLcons _ uid rest => uid :: get_switch_targets rest - end - in get_switch_targets sl - | terminate _ => [] - | stub => [] - end. - -(* Get all successors of a basic block *) -Definition get_successors (cfg: ClightCFG) (uid: bb_uid) : list bb_uid := - match BBMap.find uid (map cfg) with - | None => [] - | Some (bb _ edge) => get_edge_successors edge - end. - -(* Build predecessor map: for each node, list of nodes that point to it *) -Definition compute_predecessors (cfg: ClightCFG) : BBMap.t (list bb_uid) := - BBSet.fold - (fun node acc => - let succs := get_successors cfg node in - List.fold_left - (fun acc' succ => - let existing := match BBMap.find succ acc' with - | None => [] - | Some preds => preds - end in - BBMap.add succ (node :: existing) acc') - succs - acc) - (node_set cfg) - (BBMap.empty (list bb_uid)). - -(* Get predecessors of a node *) -Definition get_predecessors (pred_map: BBMap.t (list bb_uid)) (uid: bb_uid) : list bb_uid := - match BBMap.find uid pred_map with - | None => [] - | Some preds => preds - end. - -(* Check if a node is in a set *) -Definition uid_in_set (uid: bb_uid) (s: BBSet.t) : bool := - BBSet.mem uid s. - -(* Compute dominator sets using iterative dataflow *) -(* Dom(n) = {n} ∪ (∩ Dom(p) for all predecessors p of n) *) -(* For entry node: Dom(entry) = {entry} *) -Fixpoint compute_dominators_fixpoint - (cfg: ClightCFG) - (pred_map: BBMap.t (list bb_uid)) - (dom_map: BBMap.t BBSet.t) (* Current dominator sets *) - (fuel: nat) - : BBMap.t BBSet.t := - match fuel with - | O => dom_map (* Ran out of fuel, return current state *) - | S fuel' => - let (new_dom_map, changed) := - BBSet.fold - (fun node (acc_pair: BBMap.t BBSet.t * bool) => - let (acc, has_changed) := acc_pair in - if Pos.eqb node (entry cfg) then - (* Entry node dominates only itself *) - (acc, has_changed) - else - let preds := get_predecessors pred_map node in - let new_dom := - match preds with - | [] => BBSet.singleton node (* No predecessors, only self *) - | p :: rest => - (* Start with dominators of first predecessor *) - let init_dom := match BBMap.find p acc with - | None => BBSet.empty - | Some d => d - end in - (* Intersect with dominators of remaining predecessors *) - let dom_inter := List.fold_left - (fun d_acc pred => - match BBMap.find pred acc with - | None => BBSet.empty - | Some pred_dom => BBSet.inter d_acc pred_dom - end) - rest - init_dom in - (* Add node itself *) - BBSet.add node dom_inter - end in - let old_dom := match BBMap.find node acc with - | None => BBSet.empty - | Some d => d - end in - (* Check if changed *) - if BBSet.equal new_dom old_dom then - (acc, has_changed) - else - (BBMap.add node new_dom acc, true)) - (node_set cfg) - (dom_map, false) in - if changed then - compute_dominators_fixpoint cfg pred_map new_dom_map fuel' - else - new_dom_map - end. - -(* Initialize dominator map: entry dominates only itself, others dominate all *) -Definition init_dominator_map (cfg: ClightCFG) : BBMap.t BBSet.t := - let all_nodes := node_set cfg in - BBSet.fold - (fun node acc => - if Pos.eqb node (entry cfg) then - BBMap.add node (BBSet.singleton node) acc - else - BBMap.add node all_nodes acc) - all_nodes - (BBMap.empty BBSet.t). - -(* Main entry point for computing dominators *) -Definition compute_dominators (cfg: ClightCFG) : BBMap.t BBSet.t := - let pred_map := compute_predecessors cfg in - let init_dom := init_dominator_map cfg in - compute_dominators_fixpoint cfg pred_map init_dom 100. - -(* Get immediate dominator of a node *) -(* ID(n) = the dominator of n that is dominated by all other dominators of n *) -Definition immediate_dominator - (dom_map: BBMap.t BBSet.t) - (entry: bb_uid) - (n: bb_uid) - : option bb_uid := - match BBMap.find n dom_map with - | None => None - | Some doms => - (* Remove n itself from its dominators *) - let doms_without_n := BBSet.remove n doms in - (* Entry has no immediate dominator *) - if Pos.eqb n entry then None - else if BBSet.is_empty doms_without_n then None - else - (* Find the dominator that is dominated by no other dominator of n *) - (* This is the one closest to n in the dominator tree *) - let candidates := BBSet.elements doms_without_n in - let rec find_idom (cands: list bb_uid) : option bb_uid := - match cands with - | [] => None - | [single] => Some single - | c :: rest => - (* Check if c is dominated by any other dominator *) - let is_idom := List.forallb - (fun other => - if Pos.eqb c other then true - else - (* c is idom if other doesn't dominate c, or c dominates other *) - match BBMap.find c dom_map with - | None => true - | Some c_doms => negb (BBSet.mem other c_doms) - end) - rest in - if is_idom then Some c - else find_idom rest - end in - find_idom candidates - end. - -(* Check if node u dominates node v *) -Definition dominates (dom_map: BBMap.t BBSet.t) (u v: bb_uid) : bool := - match BBMap.find v dom_map with - | None => false - | Some doms => BBSet.mem u doms - end. - -(* ============================================================================= *) -(* SCC Detection - Tarjan's Algorithm (Phase 1.3) *) -(* ============================================================================= *) - -(* State for Tarjan's SCC algorithm *) -Record TarjanState : Type := mkTarjanState { - (* Index counter *) - t_index: nat; - (* Stack of nodes *) - t_stack: list bb_uid; - (* Nodes currently on stack *) - t_on_stack: BBSet.t; - (* Index of each node (when first visited) *) - t_indices: BBMap.t nat; - (* Lowlink value of each node *) - t_lowlinks: BBMap.t nat; - (* Discovered SCCs *) - t_sccs: list BBSet.t; -}. - -Definition init_tarjan_state : TarjanState := - mkTarjanState 0 [] BBSet.empty (BBMap.empty nat) (BBMap.empty nat) []. - -(* Helper: get index of node, returns None if not yet visited *) -Definition get_index (state: TarjanState) (n: bb_uid) : option nat := - BBMap.find n (t_indices state). - -(* Helper: get lowlink of node *) -Definition get_lowlink (state: TarjanState) (n: bb_uid) : option nat := - BBMap.find n (t_lowlinks state). - -(* Helper: set index and lowlink for node *) -Definition set_index_lowlink (state: TarjanState) (n: bb_uid) (idx: nat) : TarjanState := - mkTarjanState - (S idx) - (n :: t_stack state) - (BBSet.add n (t_on_stack state)) - (BBMap.add n idx (t_indices state)) - (BBMap.add n idx (t_lowlinks state)) - (t_sccs state). - -(* Helper: update lowlink *) -Definition update_lowlink (state: TarjanState) (n: bb_uid) (new_low: nat) : TarjanState := - mkTarjanState - (t_index state) - (t_stack state) - (t_on_stack state) - (t_indices state) - (BBMap.add n new_low (t_lowlinks state)) - (t_sccs state). - -(* Helper: pop SCC from stack *) -Fixpoint pop_scc_from_stack - (stack: list bb_uid) - (on_stack: BBSet.t) - (root: bb_uid) - (acc: BBSet.t) - : (BBSet.t * list bb_uid * BBSet.t) := - match stack with - | [] => (acc, [], on_stack) - | w :: rest => - let new_acc := BBSet.add w acc in - let new_on_stack := BBSet.remove w on_stack in - if Pos.eqb w root then - (new_acc, rest, new_on_stack) - else - pop_scc_from_stack rest new_on_stack root new_acc - end. - -(* Tarjan's strongconnect procedure *) -Fixpoint tarjan_strongconnect - (cfg: ClightCFG) - (v: bb_uid) - (state: TarjanState) - (fuel: nat) - : TarjanState := - match fuel with - | O => state - | S fuel' => - (* Set index and lowlink for v *) - let state1 := set_index_lowlink state v (t_index state) in - - (* Process all successors *) - let succs := get_successors cfg v in - let state2 := List.fold_left - (fun st w => - match get_index st w with - | None => - (* Successor w has not been visited; recurse *) - let st' := tarjan_strongconnect cfg w st fuel' in - (* Update v's lowlink *) - match get_lowlink st' v, get_lowlink st' w with - | Some v_low, Some w_low => - if Nat.ltb w_low v_low then - update_lowlink st' v w_low - else - st' - | _, _ => st' - end - | Some _ => - (* Successor w has been visited *) - if BBSet.mem w (t_on_stack st) then - (* w is on stack, part of current SCC *) - match get_lowlink st v, get_index st w with - | Some v_low, Some w_idx => - if Nat.ltb w_idx v_low then - update_lowlink st v w_idx - else - st - | _, _ => st - end - else - st - end) - succs - state1 in - - (* If v is a root node, pop the stack and create SCC *) - match get_lowlink state2 v, get_index state2 v with - | Some v_low, Some v_idx => - if Nat.eqb v_low v_idx then - (* v is root of SCC *) - let (scc, new_stack, new_on_stack) := - pop_scc_from_stack (t_stack state2) (t_on_stack state2) v BBSet.empty in - mkTarjanState - (t_index state2) - new_stack - new_on_stack - (t_indices state2) - (t_lowlinks state2) - (scc :: t_sccs state2) - else - state2 - | _, _ => state2 - end - end. - -(* Main SCC finder *) -Definition find_sccs (cfg: ClightCFG) : list BBSet.t := - let nodes := BBSet.elements (node_set cfg) in - let final_state := List.fold_left - (fun state v => - match get_index state v with - | None => tarjan_strongconnect cfg v state 100 - | Some _ => state - end) - nodes - init_tarjan_state in - t_sccs final_state. - -(* Check if two nodes are in the same SCC (loop) *) -Definition nodes_in_same_loop (sccs: list BBSet.t) (u v: bb_uid) : bool := - List.existsb - (fun scc => - andb (BBSet.mem u scc) (BBSet.mem v scc)) - sccs. - - - Inductive Instruction := | i_skip : Instruction | i_assign : Clight.expr -> Clight.expr -> Instruction diff --git a/cfrontend/RustLightgen.v b/cfrontend/RustLightgen.v index 50f5db5f7..cb326df51 100644 --- a/cfrontend/RustLightgen.v +++ b/cfrontend/RustLightgen.v @@ -541,3 +541,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/platform/dune b/platform/dune index 5d6cbdf4a..3b37e708c 100644 --- a/platform/dune +++ b/platform/dune @@ -7,55 +7,137 @@ ; 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/*))) -(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/*))) -(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/*))) -(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/*))) ; 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 %{project_root}/backend/*)) + +(subdir + cfrontend + (copy_files %{project_root}/cfrontend/*.{v,vp,ml,mli,mll,mly}*)) + +(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/*)) ; 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) From 41d963a0e201e1eca2eabeffb892acd6c0bc03cf Mon Sep 17 00:00:00 2001 From: ByronLi8565 Date: Wed, 25 Feb 2026 12:34:06 -0500 Subject: [PATCH 3/7] Integration + testing --- cfrontend/PrintRustLight.ml | 4 + cfrontend/RustLight.v | 4 + cfrontend/RustLightInsertTypeCasts.v | 4 +- cfrontend/RustLightSplitExpr.v | 3 + cfrontend/RustLightgen.v | 442 ++++++++++++++++++++++++++- driver/Driver.ml | 68 +++-- flake.nix | 1 + 7 files changed, 493 insertions(+), 33 deletions(-) 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 "@['lbl_%ld: {@;%a@;<0 -2>}@]" + (camlint_of_coqint lbl) print_stmt stmt + | S_block (None, stmt) -> fprintf fmt "@[{@;%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 cb326df51..062abef55 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,87 @@ 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. + +(* 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 (Z.pos target))) + else if BBSet.mem target meta.(sm_merge_nodes) + then Some (S_break (Some (Z.pos target))) + else None. + +Definition mk_loop_for_header (header: bb_uid) (body: rstatement) : rstatement := + S_loop (Some (Z.pos header)) body S_skip. + +Definition mk_block_followed_by (label: bb_uid) (body: rstatement) : rstatement := + S_block (Some (Z.pos 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 +577,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 (Z.pos 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 (Z.pos 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 (Z.pos 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 (Z.pos 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 +825,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 +835,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 (Z.pos 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 (Z.pos cf_lbl_ident))) in + let l_stmt := S_loop (Some (Z.pos cf_lbl_ident)) loop_body S_skip in + ret (S_sequence s_stmt l_stmt) + end. + Print calling_convention. Print r_calling_convention. 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/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 From 8e0a9d8259177671f11ed4b04cf9e7530cf41e3b Mon Sep 17 00:00:00 2001 From: ByronLi8565 Date: Thu, 5 Mar 2026 01:17:59 -0500 Subject: [PATCH 4/7] Fix Rust label collisions in structured CFG translation --- cfrontend/RustLightgen.v | 30 +++++++++++++++++++----------- 1 file changed, 19 insertions(+), 11 deletions(-) diff --git a/cfrontend/RustLightgen.v b/cfrontend/RustLightgen.v index 062abef55..523d52f9b 100644 --- a/cfrontend/RustLightgen.v +++ b/cfrontend/RustLightgen.v @@ -517,6 +517,14 @@ Definition is_fallthrough_target (target: bb_uid) (context: TranslContext) : boo | 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 @@ -530,16 +538,16 @@ Definition structured_jump_for_branch 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 (Z.pos target))) + then Some (S_continue (Some (encode_block_label target))) else if BBSet.mem target meta.(sm_merge_nodes) - then Some (S_break (Some (Z.pos target))) + 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 (Z.pos header)) body S_skip. + S_loop (Some (encode_block_label header)) body S_skip. Definition mk_block_followed_by (label: bb_uid) (body: rstatement) : rstatement := - S_block (Some (Z.pos label)) body. + S_block (Some (encode_block_label label)) body. Definition choose_structured_branch (meta: StructuredMetadata) @@ -577,7 +585,7 @@ 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 (Some (Z.pos cf_lbl_ident)) 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 := @@ -608,7 +616,7 @@ Definition doBranch end then S_skip else if bb_uid_in_list target context_labels - then S_break (Some (Z.pos target)) + 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 := @@ -618,7 +626,7 @@ Fixpoint selector_cases (entry_uid: bb_uid) (nodes: list bb_uid) : labeled_rstat let stmt := if Pos.eqb node entry_uid then S_skip - else S_break (Some (Z.pos node)) + else S_break (Some (encode_block_label node)) in LScons (Some (Z.pos node)) stmt (selector_cases entry_uid rest) end. @@ -723,7 +731,7 @@ Fixpoint nodeWithin (next_in_order y_n ordered_nodes) context_labels r_ty; - ret (S_sequence (S_block (Some (Z.pos y_n)) inner) y_stmt) + ret (S_sequence (S_block (Some (encode_block_label y_n)) inner) y_stmt) end. Definition doTree @@ -835,7 +843,7 @@ Definition transl_cfg_to_rustlight_dispatcher (cfg: ClightCFG) (r_ty: type) : Si (*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 (Some (Z.pos cf_lbl_ident)) 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. @@ -848,8 +856,8 @@ Definition transl_cfg_to_rustlight (cfg: ClightCFG) (r_ty: type) : SimplExpr.mon | _ => 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 (Z.pos cf_lbl_ident))) in - let l_stmt := S_loop (Some (Z.pos cf_lbl_ident)) loop_body S_skip 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. From 1bc76ea1f5c29d2151416b97fafae25963533f06 Mon Sep 17 00:00:00 2001 From: ByronLi8565 Date: Tue, 10 Mar 2026 10:01:55 -0400 Subject: [PATCH 5/7] SplitLong.v --- .gitignore | 1 - backend/SplitLong.v | 487 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 487 insertions(+), 1 deletion(-) create mode 100644 backend/SplitLong.v diff --git a/.gitignore b/.gitignore index 786a781cf..69f556278 100644 --- a/.gitignore +++ b/.gitignore @@ -49,7 +49,6 @@ /aarch64/SelectOp.v /aarch64/SelectLong.v /backend/SelectDiv.v -/backend/SplitLong.v /cparser/Parser.v /cparser/Lexer.ml /cparser/pre_parser.ml diff --git a/backend/SplitLong.v b/backend/SplitLong.v new file mode 100644 index 000000000..47daaa807 --- /dev/null +++ b/backend/SplitLong.v @@ -0,0 +1,487 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Instruction selection for 64-bit integer operations *) + +Require String. +Require Import Coqlib. +Require Import AST Integers Floats. +Require Import Op CminorSel. +Require Import SelectOp. + +Local Open Scope cminorsel_scope. +Local Open Scope string_scope. + +(** Some operations on 64-bit integers are transformed into calls to + runtime library functions. The following type class collects + the names of these functions. *) + +Class helper_functions := mk_helper_functions { + i64_dtos: ident; (**r float64 -> signed long *) + i64_dtou: ident; (**r float64 -> unsigned long *) + i64_stod: ident; (**r signed long -> float64 *) + i64_utod: ident; (**r unsigned long -> float64 *) + i64_stof: ident; (**r signed long -> float32 *) + i64_utof: ident; (**r unsigned long -> float32 *) + i64_sdiv: ident; (**r signed division *) + i64_udiv: ident; (**r unsigned division *) + i64_smod: ident; (**r signed remainder *) + i64_umod: ident; (**r unsigned remainder *) + i64_shl: ident; (**r shift left *) + i64_shr: ident; (**r shift right unsigned *) + i64_sar: ident; (**r shift right signed *) + i64_umulh: ident; (**r unsigned multiply high *) + i64_smulh: ident; (**r signed multiply high *) +}. + +Definition sig_l_l := mksignature (Tlong :: nil) Tlong cc_default. +Definition sig_l_f := mksignature (Tlong :: nil) Tfloat cc_default. +Definition sig_l_s := mksignature (Tlong :: nil) Tsingle cc_default. +Definition sig_f_l := mksignature (Tfloat :: nil) Tlong cc_default. +Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) Tlong cc_default. +Definition sig_li_l := mksignature (Tlong :: Tint :: nil) Tlong cc_default. +Definition sig_ii_l := mksignature (Tint :: Tint :: nil) Tlong cc_default. + +Section SELECT. + +Context {hf: helper_functions}. + +Definition makelong (h l: expr): expr := + Eop Omakelong (h ::: l ::: Enil). + +(** Original definition: +<< +Nondetfunction splitlong (e: expr) (f: expr -> expr -> expr) := + match e with + | Eop Omakelong (h ::: l ::: Enil) => f h l + | _ => Elet e (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))) + end. +>> +*) + +Inductive splitlong_cases: forall (e: expr) , Type := + | splitlong_case1: forall h l, splitlong_cases (Eop Omakelong (h ::: l ::: Enil)) + | splitlong_default: forall (e: expr) , splitlong_cases e. + +Definition splitlong_match (e: expr) := + match e as zz1 return splitlong_cases zz1 with + | Eop Omakelong (h ::: l ::: Enil) => splitlong_case1 h l + | e => splitlong_default e + end. + +Definition splitlong (e: expr) (f: expr -> expr -> expr) := + match splitlong_match e with + | splitlong_case1 h l => (* Eop Omakelong (h ::: l ::: Enil) *) + f h l + | splitlong_default e => + Elet e (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))) + end. + + +(** Original definition: +<< +Nondetfunction splitlong2 (e1 e2: expr) (f: expr -> expr -> expr -> expr -> expr) := + match e1, e2 with + | Eop Omakelong (h1 ::: l1 ::: Enil), Eop Omakelong (h2 ::: l2 ::: Enil) => + f h1 l1 h2 l2 + | Eop Omakelong (h1 ::: l1 ::: Enil), t2 => + Elet t2 (f (lift h1) (lift l1) + (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))) + | t1, Eop Omakelong (h2 ::: l2 ::: Enil) => + Elet t1 (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)) + (lift h2) (lift l2)) + | _, _ => + Elet e1 (Elet (lift e2) + (f (Eop Ohighlong (Eletvar 1 ::: Enil)) (Eop Olowlong (Eletvar 1 ::: Enil)) + (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)))) + end. +>> +*) + +Inductive splitlong2_cases: forall (e1 e2: expr) , Type := + | splitlong2_case1: forall h1 l1 h2 l2, splitlong2_cases (Eop Omakelong (h1 ::: l1 ::: Enil)) (Eop Omakelong (h2 ::: l2 ::: Enil)) + | splitlong2_case2: forall h1 l1 t2, splitlong2_cases (Eop Omakelong (h1 ::: l1 ::: Enil)) (t2) + | splitlong2_case3: forall t1 h2 l2, splitlong2_cases (t1) (Eop Omakelong (h2 ::: l2 ::: Enil)) + | splitlong2_default: forall (e1 e2: expr) , splitlong2_cases e1 e2. + +Definition splitlong2_match (e1 e2: expr) := + match e1 as zz1, e2 as zz2 return splitlong2_cases zz1 zz2 with + | Eop Omakelong (h1 ::: l1 ::: Enil), Eop Omakelong (h2 ::: l2 ::: Enil) => splitlong2_case1 h1 l1 h2 l2 + | Eop Omakelong (h1 ::: l1 ::: Enil), t2 => splitlong2_case2 h1 l1 t2 + | t1, Eop Omakelong (h2 ::: l2 ::: Enil) => splitlong2_case3 t1 h2 l2 + | e1, e2 => splitlong2_default e1 e2 + end. + +Definition splitlong2 (e1 e2: expr) (f: expr -> expr -> expr -> expr -> expr) := + match splitlong2_match e1 e2 with + | splitlong2_case1 h1 l1 h2 l2 => (* Eop Omakelong (h1 ::: l1 ::: Enil), Eop Omakelong (h2 ::: l2 ::: Enil) *) + f h1 l1 h2 l2 + | splitlong2_case2 h1 l1 t2 => (* Eop Omakelong (h1 ::: l1 ::: Enil), t2 *) + Elet t2 (f (lift h1) (lift l1) (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))) + | splitlong2_case3 t1 h2 l2 => (* t1, Eop Omakelong (h2 ::: l2 ::: Enil) *) + Elet t1 (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)) (lift h2) (lift l2)) + | splitlong2_default e1 e2 => + Elet e1 (Elet (lift e2) (f (Eop Ohighlong (Eletvar 1 ::: Enil)) (Eop Olowlong (Eletvar 1 ::: Enil)) (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)))) + end. + + +(** Original definition: +<< +Nondetfunction lowlong (e: expr) := + match e with + | Eop Omakelong (e1 ::: e2 ::: Enil) => e2 + | _ => Eop Olowlong (e ::: Enil) + end. +>> +*) + +Inductive lowlong_cases: forall (e: expr), Type := + | lowlong_case1: forall e1 e2, lowlong_cases (Eop Omakelong (e1 ::: e2 ::: Enil)) + | lowlong_default: forall (e: expr), lowlong_cases e. + +Definition lowlong_match (e: expr) := + match e as zz1 return lowlong_cases zz1 with + | Eop Omakelong (e1 ::: e2 ::: Enil) => lowlong_case1 e1 e2 + | e => lowlong_default e + end. + +Definition lowlong (e: expr) := + match lowlong_match e with + | lowlong_case1 e1 e2 => (* Eop Omakelong (e1 ::: e2 ::: Enil) *) + e2 + | lowlong_default e => + Eop Olowlong (e ::: Enil) + end. + + +(** Original definition: +<< +Nondetfunction highlong (e: expr) := + match e with + | Eop Omakelong (e1 ::: e2 ::: Enil) => e1 + | _ => Eop Ohighlong (e ::: Enil) + end. +>> +*) + +Inductive highlong_cases: forall (e: expr), Type := + | highlong_case1: forall e1 e2, highlong_cases (Eop Omakelong (e1 ::: e2 ::: Enil)) + | highlong_default: forall (e: expr), highlong_cases e. + +Definition highlong_match (e: expr) := + match e as zz1 return highlong_cases zz1 with + | Eop Omakelong (e1 ::: e2 ::: Enil) => highlong_case1 e1 e2 + | e => highlong_default e + end. + +Definition highlong (e: expr) := + match highlong_match e with + | highlong_case1 e1 e2 => (* Eop Omakelong (e1 ::: e2 ::: Enil) *) + e1 + | highlong_default e => + Eop Ohighlong (e ::: Enil) + end. + + +Definition longconst (n: int64) : expr := + makelong (Eop (Ointconst (Int64.hiword n)) Enil) + (Eop (Ointconst (Int64.loword n)) Enil). + +(** Original definition: +<< +Nondetfunction is_longconst (e: expr) := + match e with + | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => + Some(Int64.ofwords h l) + | _ => + None + end. +>> +*) + +Inductive is_longconst_cases: forall (e: expr), Type := + | is_longconst_case1: forall h l, is_longconst_cases (Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil)) + | is_longconst_default: forall (e: expr), is_longconst_cases e. + +Definition is_longconst_match (e: expr) := + match e as zz1 return is_longconst_cases zz1 with + | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => is_longconst_case1 h l + | e => is_longconst_default e + end. + +Definition is_longconst (e: expr) := + match is_longconst_match e with + | is_longconst_case1 h l => (* Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) *) + Some(Int64.ofwords h l) + | is_longconst_default e => + None + end. + + +Definition is_longconst_zero (e: expr) := + match is_longconst e with + | Some n => Int64.eq n Int64.zero + | None => false + end. + +Definition intoflong (e: expr) := lowlong e. + +(** Original definition: +<< +Nondetfunction longofint (e: expr) := + match e with + | Eop (Ointconst n) Enil => longconst (Int64.repr (Int.signed n)) + | _ => Elet e (makelong (shrimm (Eletvar O) (Int.repr 31)) (Eletvar O)) + end. +>> +*) + +Inductive longofint_cases: forall (e: expr), Type := + | longofint_case1: forall n, longofint_cases (Eop (Ointconst n) Enil) + | longofint_default: forall (e: expr), longofint_cases e. + +Definition longofint_match (e: expr) := + match e as zz1 return longofint_cases zz1 with + | Eop (Ointconst n) Enil => longofint_case1 n + | e => longofint_default e + end. + +Definition longofint (e: expr) := + match longofint_match e with + | longofint_case1 n => (* Eop (Ointconst n) Enil *) + longconst (Int64.repr (Int.signed n)) + | longofint_default e => + Elet e (makelong (shrimm (Eletvar O) (Int.repr 31)) (Eletvar O)) + end. + + +Definition longofintu (e: expr) := + makelong (Eop (Ointconst Int.zero) Enil) e. + +Definition negl (e: expr) := + match is_longconst e with + | Some n => longconst (Int64.neg n) + | None => Ebuiltin (EF_builtin "__builtin_negl" sig_l_l) (e ::: Enil) + end. + +Definition notl (e: expr) := + splitlong e (fun h l => makelong (notint h) (notint l)). + +Definition longoffloat (arg: expr) := + Eexternal i64_dtos sig_f_l (arg ::: Enil). +Definition longuoffloat (arg: expr) := + Eexternal i64_dtou sig_f_l (arg ::: Enil). +Definition floatoflong (arg: expr) := + Eexternal i64_stod sig_l_f (arg ::: Enil). +Definition floatoflongu (arg: expr) := + Eexternal i64_utod sig_l_f (arg ::: Enil). +Definition longofsingle (arg: expr) := + longoffloat (floatofsingle arg). +Definition longuofsingle (arg: expr) := + longuoffloat (floatofsingle arg). +Definition singleoflong (arg: expr) := + Eexternal i64_stof sig_l_s (arg ::: Enil). +Definition singleoflongu (arg: expr) := + Eexternal i64_utof sig_l_s (arg ::: Enil). + +Definition andl (e1 e2: expr) := + splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (and h1 h2) (and l1 l2)). + +Definition orl (e1 e2: expr) := + splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (or h1 h2) (or l1 l2)). + +Definition xorl (e1 e2: expr) := + splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (xor h1 h2) (xor l1 l2)). + +Definition shllimm (e1: expr) (n: int) := + if Int.eq n Int.zero then e1 else + if Int.ltu n Int.iwordsize then + splitlong e1 (fun h l => + makelong (or (shlimm h n) (shruimm l (Int.sub Int.iwordsize n))) + (shlimm l n)) + else if Int.ltu n Int64.iwordsize' then + makelong (shlimm (lowlong e1) (Int.sub n Int.iwordsize)) + (Eop (Ointconst Int.zero) Enil) + else + Eexternal i64_shl sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). + +Definition shrluimm (e1: expr) (n: int) := + if Int.eq n Int.zero then e1 else + if Int.ltu n Int.iwordsize then + splitlong e1 (fun h l => + makelong (shruimm h n) + (or (shruimm l n) (shlimm h (Int.sub Int.iwordsize n)))) + else if Int.ltu n Int64.iwordsize' then + makelong (Eop (Ointconst Int.zero) Enil) + (shruimm (highlong e1) (Int.sub n Int.iwordsize)) + else + Eexternal i64_shr sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). + +Definition shrlimm (e1: expr) (n: int) := + if Int.eq n Int.zero then e1 else + if Int.ltu n Int.iwordsize then + splitlong e1 (fun h l => + makelong (shrimm h n) + (or (shruimm l n) (shlimm h (Int.sub Int.iwordsize n)))) + else if Int.ltu n Int64.iwordsize' then + Elet (highlong e1) + (makelong (shrimm (Eletvar 0) (Int.repr 31)) + (shrimm (Eletvar 0) (Int.sub n Int.iwordsize))) + else + Eexternal i64_sar sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). + +Definition is_intconst (e: expr) := + match e with + | Eop (Ointconst n) Enil => Some n + | _ => None + end. + +Definition shll (e1 e2: expr) := + match is_intconst e2 with + | Some n => shllimm e1 n + | None => Eexternal i64_shl sig_li_l (e1 ::: e2 ::: Enil) + end. + +Definition shrlu (e1 e2: expr) := + match is_intconst e2 with + | Some n => shrluimm e1 n + | None => Eexternal i64_shr sig_li_l (e1 ::: e2 ::: Enil) + end. + +Definition shrl (e1 e2: expr) := + match is_intconst e2 with + | Some n => shrlimm e1 n + | None => Eexternal i64_sar sig_li_l (e1 ::: e2 ::: Enil) + end. + +Definition addl (e1 e2: expr) := + let default := Ebuiltin (EF_builtin "__builtin_addl" sig_ll_l) (e1 ::: e2 ::: Enil) in + match is_longconst e1, is_longconst e2 with + | Some n1, Some n2 => longconst (Int64.add n1 n2) + | Some n1, _ => if Int64.eq n1 Int64.zero then e2 else default + | _, Some n2 => if Int64.eq n2 Int64.zero then e1 else default + | _, _ => default + end. + +Definition subl (e1 e2: expr) := + let default := Ebuiltin (EF_builtin "__builtin_subl" sig_ll_l) (e1 ::: e2 ::: Enil) in + match is_longconst e1, is_longconst e2 with + | Some n1, Some n2 => longconst (Int64.sub n1 n2) + | Some n1, _ => if Int64.eq n1 Int64.zero then negl e2 else default + | _, Some n2 => if Int64.eq n2 Int64.zero then e1 else default + | _, _ => default + end. + +Definition mull_base (e1 e2: expr) := + splitlong2 e1 e2 (fun h1 l1 h2 l2 => + Elet (Ebuiltin (EF_builtin "__builtin_mull" sig_ii_l) (l1 ::: l2 ::: Enil)) + (makelong + (add (add (Eop Ohighlong (Eletvar O ::: Enil)) + (mul (lift l1) (lift h2))) + (mul (lift h1) (lift l2))) + (Eop Olowlong (Eletvar O ::: Enil)))). + +Definition mullimm (n: int64) (e: expr) := + if Int64.eq n Int64.zero then longconst Int64.zero else + if Int64.eq n Int64.one then e else + match Int64.is_power2' n with + | Some l => shllimm e l + | None => mull_base e (longconst n) + end. + +Definition mull (e1 e2: expr) := + match is_longconst e1, is_longconst e2 with + | Some n1, Some n2 => longconst (Int64.mul n1 n2) + | Some n1, _ => mullimm n1 e2 + | _, Some n2 => mullimm n2 e1 + | _, _ => mull_base e1 e2 + end. + +Definition mullhu (e1: expr) (n2: int64) := + Eexternal i64_umulh sig_ll_l (e1 ::: longconst n2 ::: Enil). +Definition mullhs (e1: expr) (n2: int64) := + Eexternal i64_smulh sig_ll_l (e1 ::: longconst n2 ::: Enil). + +Definition shrxlimm (e: expr) (n: int) := + if Int.eq n Int.zero then e else + Elet e (shrlimm (addl (Eletvar O) + (shrluimm (shrlimm (Eletvar O) (Int.repr 63)) + (Int.sub (Int.repr 64) n))) + n). + +Definition divlu_base (e1 e2: expr) := Eexternal i64_udiv sig_ll_l (e1 ::: e2 ::: Enil). +Definition modlu_base (e1 e2: expr) := Eexternal i64_umod sig_ll_l (e1 ::: e2 ::: Enil). +Definition divls_base (e1 e2: expr) := Eexternal i64_sdiv sig_ll_l (e1 ::: e2 ::: Enil). +Definition modls_base (e1 e2: expr) := Eexternal i64_smod sig_ll_l (e1 ::: e2 ::: Enil). + +Definition cmpl_eq_zero (e: expr) := + splitlong e (fun h l => comp Ceq (or h l) (Eop (Ointconst Int.zero) Enil)). + +Definition cmpl_ne_zero (e: expr) := + splitlong e (fun h l => comp Cne (or h l) (Eop (Ointconst Int.zero) Enil)). + +Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) := + splitlong2 e1 e2 (fun h1 l1 h2 l2 => + Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) + (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) + (Eop (Ocmp (Ccompu ch)) (h1:::h2:::Enil))). + +Definition cmplu (c: comparison) (e1 e2: expr) := + match c with + | Ceq => + cmpl_eq_zero (xorl e1 e2) + | Cne => + cmpl_ne_zero (xorl e1 e2) + | Clt => + cmplu_gen Clt Clt e1 e2 + | Cle => + cmplu_gen Clt Cle e1 e2 + | Cgt => + cmplu_gen Cgt Cgt e1 e2 + | Cge => + cmplu_gen Cgt Cge e1 e2 + end. + +Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) := + splitlong2 e1 e2 (fun h1 l1 h2 l2 => + Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) + (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) + (Eop (Ocmp (Ccomp ch)) (h1:::h2:::Enil))). + +Definition cmpl (c: comparison) (e1 e2: expr) := + match c with + | Ceq => + cmpl_eq_zero (xorl e1 e2) +(* + (if is_longconst_zero e2 then e1 + else if is_longconst_zero e1 then e2 + else xorl e1 e2) *) + | Cne => + cmpl_ne_zero (xorl e1 e2) +(* (if is_longconst_zero e2 then e1 + else if is_longconst_zero e1 then e2 + else xorl e1 e2) *) + | Clt => + if is_longconst_zero e2 + then comp Clt (highlong e1) (Eop (Ointconst Int.zero) Enil) + else cmpl_gen Clt Clt e1 e2 + | Cle => + cmpl_gen Clt Cle e1 e2 + | Cgt => + cmpl_gen Cgt Cgt e1 e2 + | Cge => + if is_longconst_zero e2 + then comp Cge (highlong e1) (Eop (Ointconst Int.zero) Enil) + else cmpl_gen Cgt Cge e1 e2 + end. + +End SELECT. From 7873a223f4aab0d0a2a6f95b5bc58b2976f225cb Mon Sep 17 00:00:00 2001 From: ByronLi8565 Date: Tue, 10 Mar 2026 10:31:54 -0400 Subject: [PATCH 6/7] build fixes --- .gitignore | 4 + backend/SplitLong.v | 487 --------------------------------------- extraction/compcert/dune | 14 ++ platform/dune | 61 ++++- 4 files changed, 67 insertions(+), 499 deletions(-) delete mode 100644 backend/SplitLong.v diff --git a/.gitignore b/.gitignore index 69f556278..0e7e8b826 100644 --- a/.gitignore +++ b/.gitignore @@ -49,6 +49,7 @@ /aarch64/SelectOp.v /aarch64/SelectLong.v /backend/SelectDiv.v +/backend/SplitLong.v /cparser/Parser.v /cparser/Lexer.ml /cparser/pre_parser.ml @@ -82,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/backend/SplitLong.v b/backend/SplitLong.v deleted file mode 100644 index 47daaa807..000000000 --- a/backend/SplitLong.v +++ /dev/null @@ -1,487 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Instruction selection for 64-bit integer operations *) - -Require String. -Require Import Coqlib. -Require Import AST Integers Floats. -Require Import Op CminorSel. -Require Import SelectOp. - -Local Open Scope cminorsel_scope. -Local Open Scope string_scope. - -(** Some operations on 64-bit integers are transformed into calls to - runtime library functions. The following type class collects - the names of these functions. *) - -Class helper_functions := mk_helper_functions { - i64_dtos: ident; (**r float64 -> signed long *) - i64_dtou: ident; (**r float64 -> unsigned long *) - i64_stod: ident; (**r signed long -> float64 *) - i64_utod: ident; (**r unsigned long -> float64 *) - i64_stof: ident; (**r signed long -> float32 *) - i64_utof: ident; (**r unsigned long -> float32 *) - i64_sdiv: ident; (**r signed division *) - i64_udiv: ident; (**r unsigned division *) - i64_smod: ident; (**r signed remainder *) - i64_umod: ident; (**r unsigned remainder *) - i64_shl: ident; (**r shift left *) - i64_shr: ident; (**r shift right unsigned *) - i64_sar: ident; (**r shift right signed *) - i64_umulh: ident; (**r unsigned multiply high *) - i64_smulh: ident; (**r signed multiply high *) -}. - -Definition sig_l_l := mksignature (Tlong :: nil) Tlong cc_default. -Definition sig_l_f := mksignature (Tlong :: nil) Tfloat cc_default. -Definition sig_l_s := mksignature (Tlong :: nil) Tsingle cc_default. -Definition sig_f_l := mksignature (Tfloat :: nil) Tlong cc_default. -Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) Tlong cc_default. -Definition sig_li_l := mksignature (Tlong :: Tint :: nil) Tlong cc_default. -Definition sig_ii_l := mksignature (Tint :: Tint :: nil) Tlong cc_default. - -Section SELECT. - -Context {hf: helper_functions}. - -Definition makelong (h l: expr): expr := - Eop Omakelong (h ::: l ::: Enil). - -(** Original definition: -<< -Nondetfunction splitlong (e: expr) (f: expr -> expr -> expr) := - match e with - | Eop Omakelong (h ::: l ::: Enil) => f h l - | _ => Elet e (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))) - end. ->> -*) - -Inductive splitlong_cases: forall (e: expr) , Type := - | splitlong_case1: forall h l, splitlong_cases (Eop Omakelong (h ::: l ::: Enil)) - | splitlong_default: forall (e: expr) , splitlong_cases e. - -Definition splitlong_match (e: expr) := - match e as zz1 return splitlong_cases zz1 with - | Eop Omakelong (h ::: l ::: Enil) => splitlong_case1 h l - | e => splitlong_default e - end. - -Definition splitlong (e: expr) (f: expr -> expr -> expr) := - match splitlong_match e with - | splitlong_case1 h l => (* Eop Omakelong (h ::: l ::: Enil) *) - f h l - | splitlong_default e => - Elet e (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))) - end. - - -(** Original definition: -<< -Nondetfunction splitlong2 (e1 e2: expr) (f: expr -> expr -> expr -> expr -> expr) := - match e1, e2 with - | Eop Omakelong (h1 ::: l1 ::: Enil), Eop Omakelong (h2 ::: l2 ::: Enil) => - f h1 l1 h2 l2 - | Eop Omakelong (h1 ::: l1 ::: Enil), t2 => - Elet t2 (f (lift h1) (lift l1) - (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))) - | t1, Eop Omakelong (h2 ::: l2 ::: Enil) => - Elet t1 (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)) - (lift h2) (lift l2)) - | _, _ => - Elet e1 (Elet (lift e2) - (f (Eop Ohighlong (Eletvar 1 ::: Enil)) (Eop Olowlong (Eletvar 1 ::: Enil)) - (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)))) - end. ->> -*) - -Inductive splitlong2_cases: forall (e1 e2: expr) , Type := - | splitlong2_case1: forall h1 l1 h2 l2, splitlong2_cases (Eop Omakelong (h1 ::: l1 ::: Enil)) (Eop Omakelong (h2 ::: l2 ::: Enil)) - | splitlong2_case2: forall h1 l1 t2, splitlong2_cases (Eop Omakelong (h1 ::: l1 ::: Enil)) (t2) - | splitlong2_case3: forall t1 h2 l2, splitlong2_cases (t1) (Eop Omakelong (h2 ::: l2 ::: Enil)) - | splitlong2_default: forall (e1 e2: expr) , splitlong2_cases e1 e2. - -Definition splitlong2_match (e1 e2: expr) := - match e1 as zz1, e2 as zz2 return splitlong2_cases zz1 zz2 with - | Eop Omakelong (h1 ::: l1 ::: Enil), Eop Omakelong (h2 ::: l2 ::: Enil) => splitlong2_case1 h1 l1 h2 l2 - | Eop Omakelong (h1 ::: l1 ::: Enil), t2 => splitlong2_case2 h1 l1 t2 - | t1, Eop Omakelong (h2 ::: l2 ::: Enil) => splitlong2_case3 t1 h2 l2 - | e1, e2 => splitlong2_default e1 e2 - end. - -Definition splitlong2 (e1 e2: expr) (f: expr -> expr -> expr -> expr -> expr) := - match splitlong2_match e1 e2 with - | splitlong2_case1 h1 l1 h2 l2 => (* Eop Omakelong (h1 ::: l1 ::: Enil), Eop Omakelong (h2 ::: l2 ::: Enil) *) - f h1 l1 h2 l2 - | splitlong2_case2 h1 l1 t2 => (* Eop Omakelong (h1 ::: l1 ::: Enil), t2 *) - Elet t2 (f (lift h1) (lift l1) (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))) - | splitlong2_case3 t1 h2 l2 => (* t1, Eop Omakelong (h2 ::: l2 ::: Enil) *) - Elet t1 (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)) (lift h2) (lift l2)) - | splitlong2_default e1 e2 => - Elet e1 (Elet (lift e2) (f (Eop Ohighlong (Eletvar 1 ::: Enil)) (Eop Olowlong (Eletvar 1 ::: Enil)) (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)))) - end. - - -(** Original definition: -<< -Nondetfunction lowlong (e: expr) := - match e with - | Eop Omakelong (e1 ::: e2 ::: Enil) => e2 - | _ => Eop Olowlong (e ::: Enil) - end. ->> -*) - -Inductive lowlong_cases: forall (e: expr), Type := - | lowlong_case1: forall e1 e2, lowlong_cases (Eop Omakelong (e1 ::: e2 ::: Enil)) - | lowlong_default: forall (e: expr), lowlong_cases e. - -Definition lowlong_match (e: expr) := - match e as zz1 return lowlong_cases zz1 with - | Eop Omakelong (e1 ::: e2 ::: Enil) => lowlong_case1 e1 e2 - | e => lowlong_default e - end. - -Definition lowlong (e: expr) := - match lowlong_match e with - | lowlong_case1 e1 e2 => (* Eop Omakelong (e1 ::: e2 ::: Enil) *) - e2 - | lowlong_default e => - Eop Olowlong (e ::: Enil) - end. - - -(** Original definition: -<< -Nondetfunction highlong (e: expr) := - match e with - | Eop Omakelong (e1 ::: e2 ::: Enil) => e1 - | _ => Eop Ohighlong (e ::: Enil) - end. ->> -*) - -Inductive highlong_cases: forall (e: expr), Type := - | highlong_case1: forall e1 e2, highlong_cases (Eop Omakelong (e1 ::: e2 ::: Enil)) - | highlong_default: forall (e: expr), highlong_cases e. - -Definition highlong_match (e: expr) := - match e as zz1 return highlong_cases zz1 with - | Eop Omakelong (e1 ::: e2 ::: Enil) => highlong_case1 e1 e2 - | e => highlong_default e - end. - -Definition highlong (e: expr) := - match highlong_match e with - | highlong_case1 e1 e2 => (* Eop Omakelong (e1 ::: e2 ::: Enil) *) - e1 - | highlong_default e => - Eop Ohighlong (e ::: Enil) - end. - - -Definition longconst (n: int64) : expr := - makelong (Eop (Ointconst (Int64.hiword n)) Enil) - (Eop (Ointconst (Int64.loword n)) Enil). - -(** Original definition: -<< -Nondetfunction is_longconst (e: expr) := - match e with - | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => - Some(Int64.ofwords h l) - | _ => - None - end. ->> -*) - -Inductive is_longconst_cases: forall (e: expr), Type := - | is_longconst_case1: forall h l, is_longconst_cases (Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil)) - | is_longconst_default: forall (e: expr), is_longconst_cases e. - -Definition is_longconst_match (e: expr) := - match e as zz1 return is_longconst_cases zz1 with - | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => is_longconst_case1 h l - | e => is_longconst_default e - end. - -Definition is_longconst (e: expr) := - match is_longconst_match e with - | is_longconst_case1 h l => (* Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) *) - Some(Int64.ofwords h l) - | is_longconst_default e => - None - end. - - -Definition is_longconst_zero (e: expr) := - match is_longconst e with - | Some n => Int64.eq n Int64.zero - | None => false - end. - -Definition intoflong (e: expr) := lowlong e. - -(** Original definition: -<< -Nondetfunction longofint (e: expr) := - match e with - | Eop (Ointconst n) Enil => longconst (Int64.repr (Int.signed n)) - | _ => Elet e (makelong (shrimm (Eletvar O) (Int.repr 31)) (Eletvar O)) - end. ->> -*) - -Inductive longofint_cases: forall (e: expr), Type := - | longofint_case1: forall n, longofint_cases (Eop (Ointconst n) Enil) - | longofint_default: forall (e: expr), longofint_cases e. - -Definition longofint_match (e: expr) := - match e as zz1 return longofint_cases zz1 with - | Eop (Ointconst n) Enil => longofint_case1 n - | e => longofint_default e - end. - -Definition longofint (e: expr) := - match longofint_match e with - | longofint_case1 n => (* Eop (Ointconst n) Enil *) - longconst (Int64.repr (Int.signed n)) - | longofint_default e => - Elet e (makelong (shrimm (Eletvar O) (Int.repr 31)) (Eletvar O)) - end. - - -Definition longofintu (e: expr) := - makelong (Eop (Ointconst Int.zero) Enil) e. - -Definition negl (e: expr) := - match is_longconst e with - | Some n => longconst (Int64.neg n) - | None => Ebuiltin (EF_builtin "__builtin_negl" sig_l_l) (e ::: Enil) - end. - -Definition notl (e: expr) := - splitlong e (fun h l => makelong (notint h) (notint l)). - -Definition longoffloat (arg: expr) := - Eexternal i64_dtos sig_f_l (arg ::: Enil). -Definition longuoffloat (arg: expr) := - Eexternal i64_dtou sig_f_l (arg ::: Enil). -Definition floatoflong (arg: expr) := - Eexternal i64_stod sig_l_f (arg ::: Enil). -Definition floatoflongu (arg: expr) := - Eexternal i64_utod sig_l_f (arg ::: Enil). -Definition longofsingle (arg: expr) := - longoffloat (floatofsingle arg). -Definition longuofsingle (arg: expr) := - longuoffloat (floatofsingle arg). -Definition singleoflong (arg: expr) := - Eexternal i64_stof sig_l_s (arg ::: Enil). -Definition singleoflongu (arg: expr) := - Eexternal i64_utof sig_l_s (arg ::: Enil). - -Definition andl (e1 e2: expr) := - splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (and h1 h2) (and l1 l2)). - -Definition orl (e1 e2: expr) := - splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (or h1 h2) (or l1 l2)). - -Definition xorl (e1 e2: expr) := - splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (xor h1 h2) (xor l1 l2)). - -Definition shllimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else - if Int.ltu n Int.iwordsize then - splitlong e1 (fun h l => - makelong (or (shlimm h n) (shruimm l (Int.sub Int.iwordsize n))) - (shlimm l n)) - else if Int.ltu n Int64.iwordsize' then - makelong (shlimm (lowlong e1) (Int.sub n Int.iwordsize)) - (Eop (Ointconst Int.zero) Enil) - else - Eexternal i64_shl sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). - -Definition shrluimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else - if Int.ltu n Int.iwordsize then - splitlong e1 (fun h l => - makelong (shruimm h n) - (or (shruimm l n) (shlimm h (Int.sub Int.iwordsize n)))) - else if Int.ltu n Int64.iwordsize' then - makelong (Eop (Ointconst Int.zero) Enil) - (shruimm (highlong e1) (Int.sub n Int.iwordsize)) - else - Eexternal i64_shr sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). - -Definition shrlimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else - if Int.ltu n Int.iwordsize then - splitlong e1 (fun h l => - makelong (shrimm h n) - (or (shruimm l n) (shlimm h (Int.sub Int.iwordsize n)))) - else if Int.ltu n Int64.iwordsize' then - Elet (highlong e1) - (makelong (shrimm (Eletvar 0) (Int.repr 31)) - (shrimm (Eletvar 0) (Int.sub n Int.iwordsize))) - else - Eexternal i64_sar sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). - -Definition is_intconst (e: expr) := - match e with - | Eop (Ointconst n) Enil => Some n - | _ => None - end. - -Definition shll (e1 e2: expr) := - match is_intconst e2 with - | Some n => shllimm e1 n - | None => Eexternal i64_shl sig_li_l (e1 ::: e2 ::: Enil) - end. - -Definition shrlu (e1 e2: expr) := - match is_intconst e2 with - | Some n => shrluimm e1 n - | None => Eexternal i64_shr sig_li_l (e1 ::: e2 ::: Enil) - end. - -Definition shrl (e1 e2: expr) := - match is_intconst e2 with - | Some n => shrlimm e1 n - | None => Eexternal i64_sar sig_li_l (e1 ::: e2 ::: Enil) - end. - -Definition addl (e1 e2: expr) := - let default := Ebuiltin (EF_builtin "__builtin_addl" sig_ll_l) (e1 ::: e2 ::: Enil) in - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => longconst (Int64.add n1 n2) - | Some n1, _ => if Int64.eq n1 Int64.zero then e2 else default - | _, Some n2 => if Int64.eq n2 Int64.zero then e1 else default - | _, _ => default - end. - -Definition subl (e1 e2: expr) := - let default := Ebuiltin (EF_builtin "__builtin_subl" sig_ll_l) (e1 ::: e2 ::: Enil) in - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => longconst (Int64.sub n1 n2) - | Some n1, _ => if Int64.eq n1 Int64.zero then negl e2 else default - | _, Some n2 => if Int64.eq n2 Int64.zero then e1 else default - | _, _ => default - end. - -Definition mull_base (e1 e2: expr) := - splitlong2 e1 e2 (fun h1 l1 h2 l2 => - Elet (Ebuiltin (EF_builtin "__builtin_mull" sig_ii_l) (l1 ::: l2 ::: Enil)) - (makelong - (add (add (Eop Ohighlong (Eletvar O ::: Enil)) - (mul (lift l1) (lift h2))) - (mul (lift h1) (lift l2))) - (Eop Olowlong (Eletvar O ::: Enil)))). - -Definition mullimm (n: int64) (e: expr) := - if Int64.eq n Int64.zero then longconst Int64.zero else - if Int64.eq n Int64.one then e else - match Int64.is_power2' n with - | Some l => shllimm e l - | None => mull_base e (longconst n) - end. - -Definition mull (e1 e2: expr) := - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => longconst (Int64.mul n1 n2) - | Some n1, _ => mullimm n1 e2 - | _, Some n2 => mullimm n2 e1 - | _, _ => mull_base e1 e2 - end. - -Definition mullhu (e1: expr) (n2: int64) := - Eexternal i64_umulh sig_ll_l (e1 ::: longconst n2 ::: Enil). -Definition mullhs (e1: expr) (n2: int64) := - Eexternal i64_smulh sig_ll_l (e1 ::: longconst n2 ::: Enil). - -Definition shrxlimm (e: expr) (n: int) := - if Int.eq n Int.zero then e else - Elet e (shrlimm (addl (Eletvar O) - (shrluimm (shrlimm (Eletvar O) (Int.repr 63)) - (Int.sub (Int.repr 64) n))) - n). - -Definition divlu_base (e1 e2: expr) := Eexternal i64_udiv sig_ll_l (e1 ::: e2 ::: Enil). -Definition modlu_base (e1 e2: expr) := Eexternal i64_umod sig_ll_l (e1 ::: e2 ::: Enil). -Definition divls_base (e1 e2: expr) := Eexternal i64_sdiv sig_ll_l (e1 ::: e2 ::: Enil). -Definition modls_base (e1 e2: expr) := Eexternal i64_smod sig_ll_l (e1 ::: e2 ::: Enil). - -Definition cmpl_eq_zero (e: expr) := - splitlong e (fun h l => comp Ceq (or h l) (Eop (Ointconst Int.zero) Enil)). - -Definition cmpl_ne_zero (e: expr) := - splitlong e (fun h l => comp Cne (or h l) (Eop (Ointconst Int.zero) Enil)). - -Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) := - splitlong2 e1 e2 (fun h1 l1 h2 l2 => - Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) - (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) - (Eop (Ocmp (Ccompu ch)) (h1:::h2:::Enil))). - -Definition cmplu (c: comparison) (e1 e2: expr) := - match c with - | Ceq => - cmpl_eq_zero (xorl e1 e2) - | Cne => - cmpl_ne_zero (xorl e1 e2) - | Clt => - cmplu_gen Clt Clt e1 e2 - | Cle => - cmplu_gen Clt Cle e1 e2 - | Cgt => - cmplu_gen Cgt Cgt e1 e2 - | Cge => - cmplu_gen Cgt Cge e1 e2 - end. - -Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) := - splitlong2 e1 e2 (fun h1 l1 h2 l2 => - Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) - (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) - (Eop (Ocmp (Ccomp ch)) (h1:::h2:::Enil))). - -Definition cmpl (c: comparison) (e1 e2: expr) := - match c with - | Ceq => - cmpl_eq_zero (xorl e1 e2) -(* - (if is_longconst_zero e2 then e1 - else if is_longconst_zero e1 then e2 - else xorl e1 e2) *) - | Cne => - cmpl_ne_zero (xorl e1 e2) -(* (if is_longconst_zero e2 then e1 - else if is_longconst_zero e1 then e2 - else xorl e1 e2) *) - | Clt => - if is_longconst_zero e2 - then comp Clt (highlong e1) (Eop (Ointconst Int.zero) Enil) - else cmpl_gen Clt Clt e1 e2 - | Cle => - cmpl_gen Clt Cle e1 e2 - | Cgt => - cmpl_gen Cgt Cgt e1 e2 - | Cge => - if is_longconst_zero e2 - then comp Cge (highlong e1) (Eop (Ointconst Int.zero) Enil) - else cmpl_gen Cgt Cge e1 e2 - end. - -End SELECT. 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/platform/dune b/platform/dune index 3b37e708c..774fdb7b5 100644 --- a/platform/dune +++ b/platform/dune @@ -15,7 +15,7 @@ (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} ppc)) - (files %{project_root}/powerpc/*))) + (files %{project_root}/powerpc/*.{v,vp,ml,mli}))) (subdir TargetPlatformCopy @@ -60,7 +60,7 @@ (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} riscV)) - (files %{project_root}/riscV/*))) + (files %{project_root}/riscV/*.{v,vp,ml,mli}))) (subdir TargetPlatformCopy @@ -69,7 +69,7 @@ (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} arm)) - (files %{project_root}/arm/*))) + (files %{project_root}/arm/*.{v,vp,ml,mli}))) (subdir TargetPlatformCopy @@ -78,41 +78,78 @@ (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} aarch64)) - (files %{project_root}/aarch64/*))) + (files %{project_root}/aarch64/*.{v,vp,ml,mli}))) ; copy files from all other relevant source directories (subdir backend - (copy_files %{project_root}/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 %{project_root}/cfrontend/*.{v,vp,ml,mli,mll,mly}*)) + (copy_files + (only_sources) + (files %{project_root}/cfrontend/*.{v,vp,ml,mli,mll,mly}))) (subdir common - (copy_files %{project_root}/common/*)) + (copy_files + (only_sources) + (files %{project_root}/common/*.{v,ml,mli}))) (subdir cparser - (copy_files %{project_root}/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 %{project_root}/debug/*)) + (copy_files + (only_sources) + (files %{project_root}/debug/*.{ml,mli}))) (subdir driver - (copy_files %{project_root}/driver/*)) + (copy_files + (only_sources) + (files %{project_root}/driver/*.{v,ml,mli,html}))) (subdir export - (copy_files %{project_root}/export/*)) + (copy_files + (only_sources) + (files %{project_root}/export/*.{v,ml,mli,md}))) (subdir lib - (copy_files %{project_root}/lib/*)) + (copy_files + (only_sources) + (files %{project_root}/lib/*.{v,ml,mli,mll}))) ; Run preprocessing directives on .vp files From 6ec275ffca14cc6f78f045d551347992a7b17643 Mon Sep 17 00:00:00 2001 From: ByronLi8565 Date: Tue, 10 Mar 2026 10:33:16 -0400 Subject: [PATCH 7/7] Add node splitting ocaml --- cfrontend/ClightCFGCNS.ml | 285 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 285 insertions(+) create mode 100644 cfrontend/ClightCFGCNS.ml 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 }