aboutsummaryrefslogtreecommitdiffstats
path: root/common
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-05-20 11:58:40 +0200
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-05-20 11:58:40 +0200
commit2408dd1aecf8d8c3bfd3b24a65f7f57cf602cb10 (patch)
treeb997c709ea92723f55b23b9b2eb23235b6e70dd6 /common
parentf37547880890ec7ff2acfba89848944d492ce9ad (diff)
downloadcompcert-kvx-2408dd1aecf8d8c3bfd3b24a65f7f57cf602cb10.tar.gz
compcert-kvx-2408dd1aecf8d8c3bfd3b24a65f7f57cf602cb10.zip
Changing to an opaq record in BTL info, this is a broken commit
Diffstat (limited to 'common')
-rw-r--r--common/AuxTools.ml49
1 files changed, 0 insertions, 49 deletions
diff --git a/common/AuxTools.ml b/common/AuxTools.ml
deleted file mode 100644
index a667044f..00000000
--- a/common/AuxTools.ml
+++ /dev/null
@@ -1,49 +0,0 @@
-open RTL
-open Maps
-
-let get_some = function
- | None -> failwith "Got None instead of Some _"
- | Some thing -> thing
-
-let successors_inst = function
- | Inop n
- | Iop (_, _, _, n)
- | Iload (_, _, _, _, _, n)
- | Istore (_, _, _, _, n)
- | Icall (_, _, _, _, n)
- | Ibuiltin (_, _, _, n) ->
- [ n ]
- | Icond (_, _, n1, n2, _) -> [ n1; n2 ]
- | Ijumptable (_, l) -> l
- | Itailcall _ | Ireturn _ -> []
-
-let predicted_successor = function
- | Inop n | Iop (_, _, _, n) | Iload (_, _, _, _, _, n) | Istore (_, _, _, _, n)
- ->
- Some n
- | Icall (_, _, _, _, n) | Ibuiltin (_, _, _, n) -> None
- | Icond (_, _, n1, n2, p) -> (
- match p with Some true -> Some n1 | Some false -> Some n2 | None -> None)
- | Ijumptable _ | Itailcall _ | Ireturn _ -> None
-
-let non_predicted_successors i = function
- | None -> successors_inst i
- | Some ps -> List.filter (fun s -> s != ps) (successors_inst i)
-
-(* adapted from Linearizeaux.get_join_points *)
-let get_join_points code entry =
- let reached = ref (PTree.map (fun n i -> false) code) in
- let reached_twice = ref (PTree.map (fun n i -> false) code) in
- let rec traverse pc =
- if get_some @@ PTree.get pc !reached then begin
- if not (get_some @@ PTree.get pc !reached_twice) then
- reached_twice := PTree.set pc true !reached_twice
- end else begin
- reached := PTree.set pc true !reached;
- traverse_succs (successors_inst @@ get_some @@ PTree.get pc code)
- end
- and traverse_succs = function
- | [] -> ()
- | [pc] -> traverse pc
- | pc :: l -> traverse pc; traverse_succs l
- in traverse entry; !reached_twice