-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathprelude.ml
executable file
·153 lines (141 loc) · 5.95 KB
/
prelude.ml
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
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
(***********************************************************************)
(* *)
(* Event Spaces *)
(* *)
(* Néstor CATAÑO, Lemme project *)
(* INRIA Sophia Antipolis *)
(* 2004 route des Lucioles-B.P. 93 *)
(* 06902 Sophia Antipolis Cedex (France) *)
(* *)
(***********************************************************************)
(***********************************************************************)
(* This module summerize the static information of the Store. **)
(***********************************************************************)
open Javasyntax
open Display
exception Class_Not_Found of string * string
exception Not_Applicable of string * string
type t = { mutable c: compilunit list}
let data = { c =
[ CompilC(
Package("java.lang"),
[],
Class("Object",Extends(""),[],
[ ConstrMem(CId("Object",[]),
BlockIt([(**<<>>**)],
Stack_of_env.createEnv()),
[]);
MethMem(MId("equals",RetType(PrimType(BoolType)),[ClType("Object")]),
BlockIt([(**<<>>**)],Stack_of_env.createEnv()),
["obj"]);
MethMem(MId("notify",Void,[]),
BlockIt([(**<<>>*)],Stack_of_env.createEnv()),
[]);
MethMem(MId("notifyAll",Void,[]),
BlockIt([(**<<>>*)],Stack_of_env.createEnv()),
[]);
MethMem(MId("wait",Void,[]),
BlockIt([(**<<>>*)],Stack_of_env.createEnv()),
[]);
MethMem(MId("finalize",Void,[]),
BlockIt([(**<<>>*)],Stack_of_env.createEnv()),
[]);
]
)
);
CompilC(
Package("java.lang"),
[ Import("java.security.AccessController");Import("java.security.AccessControllerContext");
Import("java.util.Map");Import("java.util.Collections");
],
Class("Thread",Extends("Object"),[],
[ ConstrMem(CId("Thread",[]),
BlockIt([(**<<>>**)],Stack_of_env.createEnv()),
[]);
MethMem(MId("currentThread",RetType(ClType("Thread")),[]),
BlockIt([(**<<>>*)],Stack_of_env.createEnv()),
[]);
MethMem(MId("yield",Void,[]),
BlockIt([(**<<>>*)],Stack_of_env.createEnv()),
[]);
MethMem(MId("sleep",Void,[]),
BlockIt([(**<<>>*)],Stack_of_env.createEnv()),
[]);
MethMem(MId("start",Void,[]),
BlockIt([(**<<>>*)],Stack_of_env.createEnv()),
[]);
MethMem(MId("run",Void,[]),
BlockIt([(**<<>>*)],Stack_of_env.createEnv()),
[]);
MethMem(MId("exit",Void,[]),
BlockIt([(**<<>>*)],Stack_of_env.createEnv()),
[]);
MethMem(MId("stop",Void,[]),
BlockIt([(**<<>>*)],Stack_of_env.createEnv()),
[]);
MethMem(MId("interrupt",Void,[]),
BlockIt([(**<<>>*)],Stack_of_env.createEnv()),
[]);
MethMem(MId("interrupted",RetType(PrimType(BoolType)),[]),
BlockIt([(**<<>>**)],Stack_of_env.createEnv()),
[]);
MethMem(MId("isAlive",RetType(PrimType(BoolType)),[]),
BlockIt([(**<<>>**)],Stack_of_env.createEnv()),
[]);
MethMem(MId("susptend",Void,[]),
BlockIt([(**<<>>*)],Stack_of_env.createEnv()),
[]);
MethMem(MId("resume",Void,[]),
BlockIt([(**<<>>*)],Stack_of_env.createEnv()),
[]);
MethMem(MId("join",Void,[]),
BlockIt([(**<<>>*)],Stack_of_env.createEnv()),
[]);
]
)
);
]
}
(** returns de compilation unit corresponding to the class 'c'. **)
let getCmpUn c =
try
Some (List.find (function CompilC(_,_,Class(cl,_,_,_)) -> if cl=c then true else false | _ -> true) data.c)
with
Not_found -> None
(** returns the list of classes implemented by 'c' **)
let getImp c =
match getCmpUn c with
| Some CompilC(_,_,Class(_,_,impls,_)) -> if impls=[] then None else Some impls
| None -> raise (Class_Not_Found("<getImpl>",(Display.disp_classtype ":" c Plenty)))
| _ -> raise (Not_Applicable("<getImpl,getCmpUn>",(Display.disp_classtype ":" c Plenty)))
(** returns the class which 'c' extends **)
let getSuper c =
match getCmpUn c with
| Some CompilC(_,_,Class(cl,Extends(cc),_,_)) -> if cc="" then None else Some cc
| None -> raise (Class_Not_Found("<getSuper>",(Display.disp_classtype ":" c Plenty)))
| _ -> raise (Not_Applicable("<getSuper,getCmpUn>",(Display.disp_classtype ":" c Plenty)))
(** returns the list of method declarations of the class 'c'. **)
let methoddecl c =
match getCmpUn c with
| Some CompilC(_,_,Class(_,_,_,cml)) ->
(List.fold_left (function a -> function MethMem(md) -> a@[md] | _ -> a) [] cml)
| None -> raise (Class_Not_Found("<methoddecl>",(Display.disp_classtype ":" c Plenty)))
| _ -> raise (Not_Applicable("<methoddecl,getCmpUn>",(Display.disp_classtype ":" c Plenty)))
(** returns the list of constructor declarations of the class 'c'. **)
let constructordecl c =
match getCmpUn c with
| Some CompilC(_,_,Class(_,_,_,cml)) ->
(List.fold_left (function a -> function ConstrMem(cd) -> a@[cd] | _ -> a) [] cml)
| None -> raise (Class_Not_Found("<constructordecl>",(Display.disp_classtype ":" c Plenty)))
| _ -> raise (Not_Applicable("<constructordecl,getCmpUn>",(Display.disp_classtype ":" c Plenty)))
(** returns the list of field declarations of the class 'c'. **)
let fielddecl c =
match getCmpUn c with
| Some CompilC(_,_,Class(_,_,_,cml)) ->
(List.fold_left (function a -> function FldMem(fd) -> a@[fd] | _ -> a) [] cml)
| None -> raise (Class_Not_Found("<fielddecl>",(Display.disp_classtype ":" c Plenty)))
| _ -> raise (Not_Applicable("<fielddecl,getCmpUn>",(Display.disp_classtype ":" c Plenty)))
(** loads the compilation unit 'cu' in the store 's' **)
let load cu =
data.c <- cu::data.c
;;