From 6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 30 Dec 2008 14:48:33 +0000
Subject: Reorganized the development, modularizing away machine-dependent
 parts. Started to merge the ARM code generator. Started to add support for
 PowerPC/EABI. Use ocamlbuild to construct executable from Caml files.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/Linearizeaux.ml | 85 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 85 insertions(+)
 create mode 100644 backend/Linearizeaux.ml

(limited to 'backend/Linearizeaux.ml')

diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
new file mode 100644
index 00000000..2f2333fb
--- /dev/null
+++ b/backend/Linearizeaux.ml
@@ -0,0 +1,85 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open BinPos
+open Coqlib
+open Datatypes
+open LTL
+open Lattice
+open CList
+open Maps
+open Camlcoq
+
+(* Trivial enumeration, in decreasing order of PC *)
+
+(***
+let enumerate_aux f reach =
+  positive_rec
+    Coq_nil
+    (fun pc nodes ->
+      if PMap.get pc reach
+      then Coq_cons (pc, nodes)
+      else nodes) 
+    f.fn_nextpc
+***)
+
+(* More clever enumeration that flattens basic blocks *)
+
+let rec int_of_pos = function
+  | Coq_xI p -> (int_of_pos p lsl 1) + 1
+  | Coq_xO p -> int_of_pos p lsl 1
+  | Coq_xH -> 1
+
+let rec pos_of_int n =
+  if n = 0 then assert false else
+  if n = 1 then Coq_xH else
+  if n land 1 = 0
+  then Coq_xO (pos_of_int (n lsr 1))
+  else Coq_xI (pos_of_int (n lsr 1))
+
+(* Build the enumeration *)
+
+module IntSet = Set.Make(struct type t = int let compare = compare end)
+
+let enumerate_aux f reach =
+  let enum = ref [] in
+  let emitted = Array.make (int_of_pos f.fn_nextpc) false in
+  let rec emit_block pending pc =
+    let npc = int_of_pos pc in
+    if emitted.(npc)
+    then emit_restart pending
+    else begin
+      enum := pc :: !enum;
+      emitted.(npc) <- true;
+      match PTree.get pc f.fn_code with
+      | None -> assert false
+      | Some i ->
+         match i with
+           | Lnop s -> emit_block pending s
+           | Lop (op, args, res, s) -> emit_block pending s
+           | Lload (chunk, addr, args, dst, s) -> emit_block pending s
+           | Lstore (chunk, addr, args, src, s) -> emit_block pending s
+           | Lcall (sig0, ros, args, res, s) -> emit_block pending s
+           | Ltailcall (sig0, ros, args) -> emit_restart pending
+           | Lalloc (arg, res, s) -> emit_block pending s
+           | Lcond (cond, args, ifso, ifnot) ->
+               emit_restart (IntSet.add (int_of_pos ifso)
+                             (IntSet.add (int_of_pos ifnot) pending))
+           | Lreturn optarg -> emit_restart pending
+    end
+  and emit_restart pending =
+    if not (IntSet.is_empty pending) then begin
+      let npc = IntSet.max_elt pending in
+      emit_block (IntSet.remove npc pending) (pos_of_int npc)
+    end in
+  emit_block IntSet.empty f.fn_entrypoint;
+  CList.rev !enum
-- 
cgit