diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-12-30 14:48:33 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-12-30 14:48:33 +0000 |
commit | 6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9 (patch) | |
tree | f7adbc5ec8accc4bec3e38939bdf570a266f0e83 /caml/Linearizeaux.ml | |
parent | 1bce6b0f9f8cd614038a6e7fc21fb984724204a4 (diff) | |
download | compcert-6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9.tar.gz compcert-6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9.zip |
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
Diffstat (limited to 'caml/Linearizeaux.ml')
-rw-r--r-- | caml/Linearizeaux.ml | 85 |
1 files changed, 0 insertions, 85 deletions
diff --git a/caml/Linearizeaux.ml b/caml/Linearizeaux.ml deleted file mode 100644 index 2f2333fb..00000000 --- a/caml/Linearizeaux.ml +++ /dev/null @@ -1,85 +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. *) -(* *) -(* *********************************************************************) - -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 |