1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
(* Note: this file is used by SliceToString, so it must not include it *)
open Camlcoq
open BinNums
open BinPos
open Maps
open Gible
open GibleSeq
open GibleSeq
open BourdoncleIterator
module B = Bourdoncle
type node = P.t
let int_of_positive p =
let i = P.to_int p in
i - 1
let positive_of_int n = P.of_int (n+1)
(* Functions copied from SliceToString to avoid mutual inclusion *)
let nodeToString (p : P.t) : string =
string_of_int (P.to_int p)
let rec cleanListToString' (aToString: 'a -> string) (l : 'a list) =
match l with
| [] -> ""
| e :: r -> " " ^ (aToString e) ^ (cleanListToString' aToString r)
let cleanListToString (aToString: 'a -> string) (l : 'a list) =
match l with
| [] -> "[]"
| [e] -> "(" ^ (aToString e) ^ ")"
| e :: r -> "(" ^ (aToString e) ^ (cleanListToString' aToString r) ^ ")"
let rec bourdoncleToString (b : B.bourdoncle) : string =
match b with
| B.I n -> (nodeToString n)
| B.L (h, lb) -> cleanListToString bourdoncleToString ((B.I h) :: lb)
let bourdoncleListToString (l : B.bourdoncle list) : string =
cleanListToString bourdoncleToString l
(* Dummy type to avoid redefining existing functions *)
type instr = | Inop
let rec get_exits = function
| RBgoto j -> [(int_of_positive j, Inop)]
| RBcall (_,_,_,dst,j) -> [(int_of_positive j, Inop)]
| RBtailcall _ -> []
| RBbuiltin (_,_,dst,j) -> [(int_of_positive j, Inop)]
| RBcond (c,args,j,k) -> [(int_of_positive j, Inop);(int_of_positive k, Inop)]
| RBjumptable (_,tbl) -> List.map (fun j -> (int_of_positive j, Inop)) tbl
| RBreturn _ -> []
let build_cfg f =
let entry = int_of_positive f.fn_entrypoint in
let max = PTree.fold (fun m n _ -> max m (int_of_positive n)) f.fn_code 0 in
(* nodes are between 1 and max+1 *)
let succ = Array.make (max+1) [] in
let _ = PTree.fold (fun () n ins ->
succ.(int_of_positive n) <- List.map (fun j -> (int_of_positive j, Inop))
(all_successors ins)) f.fn_code () in
{ entry = entry; succ = succ }
let rec build_bourdoncle' (bl : bourdoncle list) : B.bourdoncle list =
match bl with
| [] -> []
| (I i) :: r -> B.I (positive_of_int i) :: (build_bourdoncle' r)
| (L ((I h) :: l, _)) :: r -> B.L (positive_of_int h, build_bourdoncle' l) :: (build_bourdoncle' r)
| _ -> failwith "Assertion error: invalid bourdoncle ist"
let build_bourdoncle'' (f : coq_function) : B.bourdoncle =
let cfg = build_cfg f in
match build_bourdoncle' (get_bourdoncle cfg) with
| [] -> failwith "assertion error: empty bourdoncle"
| l ->
begin
match l with
| B.I h :: r -> B.L (h, r)
| B.L (_, _) :: _ ->
begin
Printf.printf "ASSERTION ERROR: invalid program structure (too many bourdoncles)\n";
Printf.printf "Head should be an element, but it is a list\n";
Printf.printf "Failed at: %s\n" (bourdoncleListToString l);
failwith "assertion error"
end
| _ -> failwith "assertion error : ???"
end
(* Auxiliary function for build_order *)
let rec linearize (b : B.bourdoncle) : node list =
match b with
| B.I n -> [n]
| B.L (h, l) -> List.fold_left (fun l0 b' -> l0 @ (linearize b')) [h] l
let succ_pos = function
| N0 -> Npos Coq_xH
| Npos p -> Npos (Pos.succ p)
let rec build_order' (l : node list) (count : coq_N) : coq_N PTree.t =
match l with
| [] -> PTree.empty
| n :: r -> PTree.set n count (build_order' r (succ_pos count))
let build_order (b : B.bourdoncle) : coq_N PMap.t =
let bo = build_order' (linearize b) (succ_pos N0) in
(succ_pos N0, bo)
let build_bourdoncle (f : coq_function) : (B.bourdoncle * coq_N PMap.t) =
let b = build_bourdoncle'' f in
let bo = build_order b in
(b, bo)
|
