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
110
111
112
113
114
115
|
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2013-present Institut National de Recherche en Informatique et *)
(* en Automatique and the authors. All rights reserved. *)
(* *)
(* This software is governed by the CeCILL-B license under French law and *)
(* abiding by the rules of distribution of free software. You can use, *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
(****************************************************************************)
open Printf
let _dbg = false
(* To disable checks that I do not understand yet -> false *)
let _docheck = true
(*************)
(* For tests *)
(*************)
type mem_space_map = (string * string list) list
let pp_mem_map m =
String.concat ","
(List.map (fun (n,r) ->
let pp = String.concat " " r in
sprintf "%s: %s" n pp) m)
type scopes =
| Tree of string * int list * scopes list
type levels = scopes
let pp_int_list il = String.concat " " (List.map (sprintf "%i") il)
let rec pp_scopes_rec s = match s with
| Tree (s,ps,ts) ->
sprintf "(%s %s%s)" s
(match ps with
| [] -> ""
| _ -> pp_int_list ps)
(pp_scopes_recs ts)
and pp_scopes_recs ts = String.concat " " (List.map pp_scopes_rec ts)
let pp_scopes = function
| Tree ("",[],ts) -> pp_scopes_recs ts
| t -> pp_scopes_rec t
let contract_ps = function
| Tree (sc0,[p0],[])::rem ->
begin try
let ps =
List.fold_right
(fun t ps -> match t with
| Tree (sc1,[p1],[]) when String.compare sc0 sc1 = 0 ->
p1::ps
| _ -> raise Exit)
rem [] in
Some (p0::ps)
with Exit -> None
end
| _ -> None
let rec do_contract st = match st with
| Tree (_,_,[]) -> st
| Tree (sc,_,ts) -> do_children sc sc ts
and do_children sc0 sc1 ts = match ts with
| [t] -> do_contract t
| _ ->
let ts = List.map do_contract ts in
begin match contract_ps ts with
| Some ps -> Tree (sc0,ps,[])
| None -> Tree (sc1,[],ts)
end
let contract st = match st with
| Tree (_,_,[]) -> st
| Tree ("",[],[t]) -> do_contract t
| Tree ("",[],ts) ->
let ts = List.map do_contract ts in
Tree ("",[],ts)
| Tree (sc,[],ts) -> do_children sc "" ts
| Tree (_,_::_,_) -> assert false
type test = {
regions : mem_space_map option;
scopes : scopes option;
levels : scopes option ;
}
let is_none = function
| {regions=None; scopes=None; levels=None; } -> true
| _ -> false
let pp t = begin match t.scopes with
| None -> ""
| Some sc ->
sprintf "scopes: %s\n" (pp_scopes sc)
end ^
begin match t.regions with
| None -> ""
| Some m ->
sprintf "regions: %s\n" (pp_mem_map m) ;
end
|
