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
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
|
open Cabs
open Cil_types
let rec init_exn exn init acc =
match init with
| SingleInit init ->
Cil.mkStmtOneInstr (Set(exn,init,Cil_datatype.Location.unknown))
:: acc
| CompoundInit (ct,initl) ->
Cil.foldLeftCompound
~implicit:false
~doinit:(fun off' i' _ acc ->
init_exn (Cil.addOffsetLval off' exn) i' acc)
~ct ~initl ~acc
let add_throw_test f exn_type test init =
let throw_block = Cil.mkBlock [] in
let exn = Cil.makeLocalVar f ~scope:throw_block "exn" exn_type in
let valid_sid = true in
let set_exn_stmts = init_exn (Var exn, NoOffset) init [] in
let loc = Cil_datatype.Location.unknown in
let throw_stmt =
Cil.mkStmt
~valid_sid
(Throw (Some (Cil.evar ~loc exn, exn_type), loc))
in
throw_block.bstmts <- List.rev (throw_stmt :: set_exn_stmts);
let new_body = Cil.mkStmt ~valid_sid (If(test, throw_block, f.sbody,loc)) in
f.sbody <- Cil.mkBlock [ new_body ]
let add_my_exn my_exn f =
let c = Cil.evar (List.hd f.sformals) in
let exn_type = TComp(my_exn,{ scache = Not_Computed},[]) in
let loc = Cil_datatype.Location.unknown in
let init =
CompoundInit(
exn_type,
[Field(List.hd my_exn.cfields, NoOffset), SingleInit (Cil.zero ~loc)])
in
add_throw_test f exn_type c init
let add_int_exn f =
let c = Cil.evar (List.hd f.sformals) in
let loc = Cil_datatype.Location.unknown in
let test =
Cil.new_exp ~loc (BinOp (Lt,c,Cil.kinteger ~loc IInt 50,Cil.intType))
in
add_throw_test f Cil.intType test (SingleInit (Cil.zero ~loc))
let add_int_ptr_exn glob f =
let c = Cil.evar (List.hd f.sformals) in
let loc = Cil_datatype.Location.unknown in
let test =
Cil.new_exp ~loc (BinOp (Gt,c,Cil.kinteger ~loc IInt 150, Cil.intType))
in
let init =
SingleInit (Cil.new_exp ~loc (AddrOf(Var glob,NoOffset)))
in
add_throw_test f Cil.intPtrType test init
let add_catch my_exn my_exn2 f =
let exn_type = TComp(my_exn, { scache = Not_Computed }, []) in
let exn_type2 = TComp(my_exn2, {scache = Not_Computed }, []) in
let exn_field = Field (List.hd my_exn.cfields, NoOffset) in
let exn2_field = Field (List.hd my_exn2.cfields, NoOffset) in
let loc = Cil_datatype.Location.unknown in
let real_locals = f.sbody.blocals in
let v1 = Cil.makeLocalVar f "exn" exn_type in
let v2 = Cil.makeLocalVar f "y" Cil.intType in
let v3 = Cil.makeLocalVar f "exn_aux" exn_type in
let v4 = Cil.makeLocalVar f "exn2" exn_type2 in
let v5 = Cil.makeLocalVar f "not_thrown" Cil.doubleType in
f.sbody.blocals <- real_locals;
let id_block =
Cil.mkBlock [Cil.mkStmtOneInstr (Set (Cil.var v1, Cil.evar ~loc v3, loc))]
in
let convert_exn_block =
Cil.mkBlock
[ Cil.mkStmtOneInstr
(Set ((Var v1, exn_field),
Cil.new_exp ~loc (Lval (Var v4, exn2_field)),
loc))]
in
let catch_stmt =
Cil.mkStmt
(TryCatch(
f.sbody,
[ Catch_exn (v1,[(v3,id_block); (v4, convert_exn_block)]),
Cil.mkBlock
[ Cil.mkStmt
(Return
(Some (Cil.new_exp ~loc (Lval (Var v1, exn_field))),
loc))];
Catch_exn (v2,[]),
Cil.mkBlock
[ Cil.mkStmt (Return (Some (Cil.evar ~loc v2),loc))];
Catch_exn (v5,[]),
Cil.mkBlock
[ Cil.mkStmt (Return (Some (Cil.mone ~loc), loc))];
Catch_all, Cil.mkBlock [ Cil.mkStmt (Throw (None, loc)) ]
],
loc))
in
f.sbody <- Cil.mkBlock [ catch_stmt ]
let change_body my_exn my_exn2 glob f =
match f.svar.vname with
| "f1" -> add_my_exn my_exn f; File.must_recompute_cfg f
| "f2" -> add_int_exn f; File.must_recompute_cfg f
| "f3" -> add_int_ptr_exn glob f; File.must_recompute_cfg f
| "f4" -> add_my_exn my_exn2 f; File.must_recompute_cfg f
| "h" -> add_catch my_exn my_exn2 f; File.must_recompute_cfg f
| _ -> ()
let add_exn ast =
let my_exn = ref None in
let my_exn2 = ref None in
let glob = ref None in
let treat_glob =
function
| GCompTag(ci,_) ->
(match !my_exn with
| None -> my_exn := Some ci
| Some _ -> my_exn2 := Some ci)
| GVar(v,_,_) when v.vname = "x" -> glob := Some v
| GFun(f,_) ->
change_body
(Extlib.the !my_exn) (Extlib.the !my_exn2) (Extlib.the !glob) f
| _ -> ()
in
List.iter treat_glob ast.globals
let loc = Cil_datatype.Location.unknown
let stmt stmt_node = { stmt_ghost = false; stmt_node }
let var v = { expr_loc = loc; expr_node = VARIABLE v }
let mk_exn_cabs b =
{ blabels = []; Cabs.battrs = [];
Cabs.bstmts =
[ stmt
(IF (var "c",
stmt (THROW (Some (var "x"),loc)),
stmt (BLOCK (b,loc,loc)),loc))] }
let mk_catch_cabs b =
{ blabels = []; Cabs.battrs = [];
Cabs.bstmts =
[ stmt
(TRY_CATCH
(stmt (BLOCK (b,loc,loc)),
[Some ([SpecType Tint],("x",JUSTBASE,[],loc)),
stmt (
RETURN (
{ expr_loc = loc; expr_node = CONSTANT (CONST_INT "3")}, loc));
None,
stmt (
RETURN (
{ expr_loc = loc; expr_node = CONSTANT (CONST_INT "4")}, loc))],
loc))]}
let add_exn_cabs (f,l) =
let treat_one_global (b,d) =
let d =
match d with
| FUNDEF (s,(t,("f",dt,a,l)),b,l1,l2) ->
FUNDEF (s,(t,("f",dt,a,l)), mk_exn_cabs b,l1,l2)
| FUNDEF (s,(t,("g",dt,a,l)),b,l1,l2) ->
FUNDEF (s,(t,("g",dt,a,l)), mk_catch_cabs b,l1,l2)
| _ -> d
in
b,d
in
(f, List.map treat_one_global l)
let () = Frontc.add_syntactic_transformation add_exn_cabs
let add_exn_cat = File.register_code_transformation_category "add_exn"
let () = File.add_code_transformation_before_cleanup add_exn_cat add_exn
|
